Documentation

CatCryptCore.Deep.MonadNormalize

Reflective normalization for the RawCode free monad #

This file gives a reflective normalizer for the deep embedding RawCode, in exactly the sense that ring normalizes commutative-ring expressions and Mathlib's monoidal tactic normalizes monoidal-category coherence terms: we compute a canonical normal form on the syntax tree and prove once that the interpretation is invariant under normalization. Equalities that hold by the monad laws then reduce to a single normal-form comparison.

The key observation is that RawCode is already the reflected syntax tree of the free monad on the signature {sample, get, put, fail, oracleCall, embed} — there is no need for a separate MonExpr reflection layer. We normalize RawCode directly. The interpretation RawCode.eval : RawCode α → SPComp α (CatCryptCore/Deep/Eval.lean) is a monad morphism into SPComp, and SPComp is a lawful monad: SPComp.bind_assoc, SPComp.pure_bind, SPComp.bind_pure hold as proved lemmas (CatCryptCore/Core/Code.lean). Those shallow laws are what make the soundness lemma go through — even though the same laws are not definitional on RawCode itself (its Monad instance is deliberately unlawful, the associativity/unit tax that sp_normalize_deep currently pays by hand with simp).

Pipeline #

Intended use #

mon_coherence is the reflective (ring / monoidal-coherence) analog for the Kleisli bind of SPComp. It is intended to replace the simp-based sp_normalize_deep as the leaf normalizer inside pkg_coherence!: instead of paying the non-definitional-bind_assoc tax with a simp set on every leaf, the normal form is computed once and the goal closes by a definitional comparison.

References #

Smart bind and normal form #

source
def CatCrypt.Deep.RawCode.appendNF {α β : Type u} (c : RawCode α) (k : α → RawCode β) :
RawCode β

Smart bind on RawCode: append the continuation k to c, reassociating to the right and eliminating a leading ret (left unit).

  • appendNF (.ret a) k = k a (left unit / pure-elim)
  • appendNF (.bind c k') k = .bind c (fun x => appendNF (k' x) k) (reassociate right)
  • appendNF op k = .bind op k for an atomic op (sample/get/put/fail/…)

The recursion is structural under the bind continuation k' — this is the same shape as RawCode.substOracle, which recurses under its continuation.

Equations
Instances For
    source
    def CatCrypt.Deep.RawCode.normalize {α : Type u} (c : RawCode α) :
    RawCode α

    Normalize a RawCode tree to right-nested, pure-eliminated normal form.

    Atomic constructors map to themselves; a bind is normalized recursively and then reassociated with appendNF.

    Equations
    Instances For

      Soundness #

      The single soundness induction: eval is invariant under appendNF/normalize. This is the crux, exactly analogous to ring's soundness lemma. The proof uses the shallow monad laws of SPComp (pure_bind, bind_assoc) — precisely the laws that are not definitional on RawCode.

      source
      theorem CatCrypt.Deep.RawCode.eval_appendNF {α β : Type u} (c : RawCode α) (k : α → RawCode β) :
      (c.appendNF k).eval = c.eval.bind fun (x : α) => (k x).eval

      appendNF computes the Kleisli bind of the interpretations: (appendNF c k).eval = c.eval.bind (fun x => (k x).eval).

      Proof by induction on c, using SPComp.pure_bind (left-unit case) and SPComp.bind_assoc (reassociation case).

      source
      theorem CatCrypt.Deep.RawCode.eval_normalize {α : Type u} (c : RawCode α) :
      c.normalize.eval = c.eval

      Soundness of normalize: interpretation is invariant under normalization, (normalize c).eval = c.eval. Proof by induction on c, using eval_appendNF.

      The reflective closer #

      source
      theorem CatCrypt.Deep.RawCode.eval_eq_of_normalize_eq {α : Type u} {a b : RawCode α} (h : a.normalize = b.normalize) :
      a.eval = b.eval

      Payoff: if two RawCode trees have the same normal form, their interpretations are equal. Rewrite both sides through eval_normalize, then the syntactic hypothesis h finishes.

      source
      def CatCrypt.Deep.tacticMon_coherence :
      Lean.ParserDescr

      Reflective closer for SPComp-level Kleisli-bind equalities. Closes a goal a.eval = b.eval by comparing the normal forms of the deep terms a and b: exact RawCode.eval_eq_of_normalize_eq (by rfl).

      This is the ring / monoidal-coherence analog for the deep-embedding monad; it is meant to replace the simp-based sp_normalize_deep as the leaf normalizer inside pkg_coherence!.

      Equations
      Instances For

        Demonstration #

        Bind associativity / left-unit equalities at the eval level, each closed in a single mon_coherence step. These would otherwise need several eval_bind/SPComp.bind_assoc (i.e. sp_normalize_deep) simp steps.