Log4Types.Core.Masking

Masking and hiding of sensitive values in log output.

`Masked a` and `Hidden a` mark a value as sensitive in its type: their
`Loggable` instances redact or omit it, so the value cannot reach a log
through its instance. The wrapped value stays available through
`reveal`, which keeps every deliberate unmasking grep-auditable.

Definitions

record Masked : Type -> Type

  Wrap a value to redact it in log output.
  
  The wrapped value remains accessible via `reveal`; only the `Loggable`
  instance redacts it.

Totality: total
Visibility: public export
Constructor: 

MkMasked : a -> Masked a

Projection: 

.reveal : Masked a -> a

Hint: 

Loggable (Masked a)

.reveal : Masked a -> a

Totality: total
Visibility: public export

reveal : Masked a -> a

Totality: total
Visibility: public export

record Hidden : Type -> Type

  Wrap a value to omit it from log output entirely.
  
  The wrapped value remains accessible via `reveal`; the `Loggable`
  instance produces no output for it.

Totality: total
Visibility: public export
Constructor: 

MkHidden : a -> Hidden a

Projection: 

.reveal : Hidden a -> a

Hint: 

Loggable (Hidden a)

.reveal : Hidden a -> a

Totality: total
Visibility: public export

reveal : Hidden a -> a

Totality: total
Visibility: public export

record MaskPolicy : Type -> Type

  A policy describing how to render a masked value.

Totality: total
Visibility: public export
Constructor: 

MkMaskPolicy : (a -> String) -> MaskPolicy a

Projection: 

.mask : MaskPolicy a -> a -> String

.mask : MaskPolicy a -> a -> String

Totality: total
Visibility: public export

mask : MaskPolicy a -> a -> String

Totality: total
Visibility: public export

defaultMask : MaskPolicy a

  Default policy: render as "***", ignoring the value.

Totality: total
Visibility: public export

lastN : Nat -> MaskPolicy String

  Policy: keep the last `n` characters and replace each earlier one with
  "*". A value no longer than `n` is masked entirely as "***", so the
  policy never reveals a whole value.

Totality: total
Visibility: public export

emailDomainOnly : MaskPolicy String

  Policy: keep the domain of an email address and replace each character
  of its local part with "*", so "alice@example.com" renders as
  "*****@example.com". The split is at the last "@"; a value without one
  is masked entirely as "***".

Totality: total
Visibility: public export

addMaskedField : LogRenderer r -> String -> MaskPolicy a -> a -> r -> r

  Add a field rendered by an explicit masking policy, for a per-field
  policy in a hand-written instance such as the last four digits of a
  card number.

Totality: total
Visibility: public export