Documentation

CatCryptCore.Deep.Eval

Interpretation from Deep to Shallow Embedding #

This file defines the interpretation of the deep embedding (RawCode) into the shallow embedding (SPComp). This bridges structural reasoning in the deep embedding with probabilistic reasoning in the shallow embedding.

Main definitions #

Theorems #

Design rationale #

The interpretation serves multiple purposes:

  1. Semantic interpretation: Give meaning to deep code via the shallow embedding
  2. Soundness: Show that structural transformations preserve semantics
  3. Completeness: Any shallow computation can be represented deeply
  4. Bridging: Connect structural proofs (deep) with distribution proofs (shallow)

Unified Heap Model #

Both the deep embedding (RawCode) and shallow embedding (SPComp) now use the same heap model (Core.Heap) and location type (Core.Location). This eliminates the need for any heap translation axioms.

The key insight is that RawCode.get and RawCode.put use Core.Location directly, so evaluation is a simple mapping:

References #

Evaluation: Deep to Shallow #

The main interpretation function that gives semantics to deep code. Since RawCode now uses Core.Location directly, no heap translation is needed.

source
noncomputable def CatCrypt.Deep.RawCode.eval {α : Type u_4} :
RawCode α → Core.SPComp α

Interpret a RawCode computation into the shallow SPComp monad.

This is the semantic interpretation that gives meaning to deep code. Each constructor of RawCode is mapped to the corresponding SPComp operation.

The interpretation is noncomputable because:

  1. Sample uses uniform distribution (noncomputable)
  2. Heap operations use classical choice for encoding/decoding

Key insight: Since RawCode uses Core.Location directly, get and put operations map directly to SPComp.get and SPComp.set with no translation needed.

Equations
Instances For

    Evaluation properties #

    These theorems show that evaluation preserves the monad structure and basic operations.

    source
    @[simp]
    theorem CatCrypt.Deep.eval_ret {α : Type u} (x : α) :
    (RawCode.ret x).eval = Core.SPComp.pure x

    Evaluation respects pure/return

    This is definitionally true from the definition of eval.

    source
    @[simp]
    theorem CatCrypt.Deep.eval_bind {α β : Type u} (c : RawCode α) (f : α → RawCode β) :
    (c.bind f).eval = c.eval.bind fun (x : α) => (f x).eval

    Evaluation distributes over bind.

    This is a key property: evaluation is a monad morphism. Definitionally true from the definition of eval.

    source
    @[simp]
    theorem CatCrypt.Deep.eval_sample {T : Type u} [Fintype T] [Nonempty T] :
    (RawCode.sample T).eval = Core.SPComp.sample T

    Evaluation of sample gives uniform distribution

    Definitionally true from the definition of eval.

    source
    @[simp]
    theorem CatCrypt.Deep.eval_fail {α : Type u} :
    RawCode.fail.eval = Core.SPComp.fail

    Evaluation of fail gives SPComp.fail

    Definitionally true from the definition of eval.

    source
    @[simp]
    theorem CatCrypt.Deep.eval_oracleCall {op : ℕ} {dom codom : Type u} {x : dom} :
    (RawCode.oracleCall op dom codom x).eval = Core.SPComp.fail

    Evaluation of oracle call gives SPComp.fail (unlinked oracle)

    Oracle calls that haven't been substituted (via substOracle / link) evaluate to failure. After linking, oracle calls are replaced with concrete implementations and this case never arises.

    source
    @[simp]
    theorem CatCrypt.Deep.eval_get (ℓ : Core.Location) :
    (RawCode.get ℓ).eval = (Core.SPComp.get ℓ).bind fun (v : ℓ.ty) => Core.SPComp.pure { down := v }

    Evaluation of get reads from the heap and lifts to ULift.

    This is definitionally true from the definition of eval.

    source
    @[simp]
    theorem CatCrypt.Deep.eval_put (ℓ : Core.Location) (v : ℓ.ty) :
    (RawCode.put ℓ v).eval = (Core.SPComp.set ℓ v).bind fun (x : Unit) => Core.SPComp.pure { down := () }

    Evaluation of put writes to the heap and returns ULift Unit.

    This is definitionally true from the definition of eval.

    Evaluation with Oracle Handler #

    evalWith generalizes eval by taking an oracle handler instead of mapping all oracle calls to failure. This is the key definition for stating that substOracle commutes with eval.

    source
    noncomputable def CatCrypt.Deep.RawCode.evalWith (oracle : ℕ → (dom codom : Type u) → dom → Core.SPComp codom) {α : Type u} :
    RawCode α → Core.SPComp α

    Interpret RawCode into SPComp, using a custom oracle handler.

    Like eval, but instead of mapping oracleCall to SPComp.fail, it calls the provided oracle function. This allows us to state the semantic correctness of substOracle:

    (code.substOracle env).eval = code.evalWith (fun op dom codom x => (env op dom codom x).eval)

    When oracle maps everything to SPComp.fail, this reduces to eval.

    Equations
    Instances For
      source
      @[simp]
      theorem CatCrypt.Deep.RawCode.evalWith_fail {α : Type u} (c : RawCode α) :
      evalWith (fun (x : ℕ) (x_1 x_2 : Type u) (x_3 : x_1) => Core.SPComp.fail) c = c.eval

      evalWith with the fail oracle is just eval.

      source
      theorem CatCrypt.Deep.RawCode.evalWith_eq_eval_no_oracle {α : Type u} {c : RawCode α} (h : c.NoOracleCall) (oracle : ℕ → (dom codom : Type u) → dom → Core.SPComp codom) :
      evalWith oracle c = c.eval

      evalWith on code without oracle calls equals eval, regardless of oracle handler.

      This is the semantic version of substOracle_eq_self: if the code never invokes any oracle, the oracle handler is irrelevant.

      Correctness of substOracle #

      The central theorem: substituting oracle calls and then evaluating is the same as evaluating with the oracle handler that evaluates the substituted code. This is proved by structural induction on RawCode.

      source
      theorem CatCrypt.Deep.eval_substOracle {α : Type u} (c : RawCode α) (env : ℕ → (dom codom : Type u) → dom → RawCode codom) :
      (c.substOracle env).eval = RawCode.evalWith (fun (op : ℕ) (dom codom : Type u) (x : dom) => (env op dom codom x).eval) c

      Correctness of substOracle: Evaluating code after oracle substitution is the same as evaluating the original code with an oracle handler that evaluates the substituted implementations.

      This is the key semantic theorem for package linking. It says that substOracle (a syntactic operation on the free monad) commutes with eval (the semantic interpretation):

      substOracle env ; eval  =  evalWith (eval ∘ env)

      The proof is by structural induction on RawCode. Each case is straightforward:

      • ret, sample, get, put, fail: substOracle preserves these, so both sides agree definitionally.
      • bind c k: by induction, the substitution distributes through bind.
      • oracleCall op dom codom x: substOracle replaces this with env op dom codom x, and evalWith applies the oracle handler, giving (env op dom codom x).eval on both sides.

      evalWith composition #

      The key theorem for link associativity: composing evalWith through substOracle produces the same result as a single evalWith with the composed handler.

      source
      theorem CatCrypt.Deep.evalWith_substOracle {α : Type u} (c : RawCode α) (env : ℕ → (dom codom : Type u) → dom → RawCode codom) (h : ℕ → (dom codom : Type u) → dom → Core.SPComp codom) :
      RawCode.evalWith h (c.substOracle env) = RawCode.evalWith (fun (op : ℕ) (dom codom : Type u) (x : dom) => RawCode.evalWith h (env op dom codom x)) c

      Composing evalWith through substOracle: evaluating substituted code with a handler is the same as evaluating the original code with a composed handler.

      This generalizes eval_substOracle by using an arbitrary handler instead of eval.

      source
      theorem CatCrypt.Deep.evalWith_congr {α : Type u} (c : RawCode α) (h₁ h₂ : ℕ → (dom codom : Type u) → dom → Core.SPComp codom) (heq : ∀ (op : ℕ) (dom codom : Type u) (x : dom), h₁ op dom codom x = h₂ op dom codom x) :
      RawCode.evalWith h₁ c = RawCode.evalWith h₂ c

      Two evalWith handlers that agree produce the same SPComp.

      This is useful for showing that two different oracle environments produce the same evaluation when they agree on all oracle calls.

      source
      theorem CatCrypt.Deep.RawCode.substOracle_cast {α β : Type u} (h : α = β) (c : RawCode β) (env : ℕ → (dom codom : Type u) → dom → RawCode codom) :
      (⋯ ▸ c).substOracle env = ⋯ ▸ c.substOracle env

      substOracle commutes with type casts (▸).

      When h : α = β and c : RawCode β, substituting oracles in the cast code h ▸ c : RawCode α is the same as casting the substituted code. Proof: subst h makes the cast trivial.

      source
      theorem CatCrypt.Deep.RawCode.eval_cast {α β : Type u} (h : α = β) (c : RawCode β) :
      (⋯ ▸ c).eval = ⋯ ▸ c.eval

      eval commutes with type casts.

      Evaluating cast code is the same as casting the evaluated result. Proof: subst h makes the cast trivial.

      source
      theorem CatCrypt.Deep.RawCode.evalWith_cast {α β : Type u} (h : α = β) (c : RawCode β) (oracle : ℕ → (dom codom : Type u) → dom → Core.SPComp codom) :
      evalWith oracle (⋯ ▸ c) = ⋯ ▸ evalWith oracle c

      evalWith commutes with type casts.

      Like eval_cast but for evalWith with a custom oracle handler. Proof: subst h makes the cast trivial.

      source
      @[simp]
      theorem CatCrypt.Deep.evalWith_fail_code {α : Type u} (h : ℕ → (dom codom : Type u) → dom → Core.SPComp codom) :
      RawCode.evalWith h RawCode.fail = Core.SPComp.fail

      evalWith for fail is just SPComp.fail.

      Relational Hoare logic for deep embedding #

      We define a relational Hoare logic for the deep embedding using the shallow embedding's rHoare. Since both use Core.Heap, no translation is needed.

      source
      @[reducible, inline]
      abbrev CatCrypt.Deep.RPre :
      Type

      Relational precondition (on Core.Heap)

      Equations
      Instances For
        source
        @[reducible, inline]
        abbrev CatCrypt.Deep.RPost (α : Type u_4) (β : Type u_5) :
        Type (max u_4 u_5)

        Relational postcondition

        Equations
        Instances For
          source
          noncomputable def CatCrypt.Deep.DeepRHoare {α : Type u_1} (pre : RPre) (c₁ c₂ : RawCode α) (post : RPost α α) :
          Prop

          Relational Hoare logic for deep embedding.

          DeepRHoare pre c₁ c₂ post means: For all heap pairs (h₁, h₂) satisfying pre, after evaluating c₁ and c₂, the results satisfy post.

          This is defined semantically using the shallow embedding: we evaluate the deep code to shallow code and use the existing rHoare. Since both embeddings use Core.Heap, no heap translation is needed.

          Equations
          Instances For
            source
            theorem CatCrypt.Deep.eval_rHoare {α : Type u_1} (c₁ c₂ : RawCode α) (pre : RPre) (post : RPost α α) :
            DeepRHoare pre c₁ c₂ post ↔ Relational.rHoare pre c₁.eval c₂.eval post

            Deep relational judgments are exactly shallow relational judgments on evaluated code.

            This is the key soundness theorem: proving something in the deep embedding's rHoare is equivalent to proving it in the shallow embedding (after evaluation).

            The proof is immediate since DeepRHoare is defined in terms of rHoare.

            Package evaluation #

            Interpret deep packages to shallow packages.

            NOTE: Package.lean uses a different structure with interfaces and ValidCode. This provides a simplified evaluation focusing on the core concepts. A full evaluation would need to handle interface matching and code validity.

            Examples and Properties #

            The evaluation equations are now proved as theorems using rfl, since the definition of eval directly matches these equalities:

            These are all marked with @[simp] for automatic simplification.

            Design Notes #

            Unified Heap Model #

            The key insight that eliminates all heap translation axioms is using Core.Location and Core.Heap directly in the deep embedding:

            Before (with axioms):

            After (axiom-free):

            Universe Handling #

            Since Core.Location.ty : Type (universe 0) but RawCode : Type u → Type (u+1), we use ULift to bridge the universes:

            The evaluation wraps values in ULift.up and unwraps with .down as needed.