Deep/Shallow Bridge Library

This file provides systematic support for moving between the deep embedding (RawCode, DeepPackage) and the shallow embedding (SPComp).

Main definitions

• DeepPackage.evalOp - Evaluate a single operation from a deep package
• rHoare_of_code_eq - Derive rHoare from code equality in deep embedding
• rHoare_of_eval_eq - Derive rHoare from evaluation equality

Tactics

• ssprove_deep_to_shallow - Unfold DeepRHoare and simplify eval
• ssprove_eval - Simplify eval expressions using the ssprove_eval simp set

Simp set

• ssprove_eval - Named simp set collecting all eval lemmas

Design rationale

The bridge serves multiple purposes:

1. Move to shallow for distribution reasoning: After defining games in the deep embedding, use eval to move to SPComp for coupling proofs.

2. Structural equality → rHoare: When two deep programs are syntactically equal, this immediately gives an rHoare judgment after evaluation.

3. Package-level evaluation: Evaluate all implementations in a deep package to SPComp functions, enabling reasoning about whole packages.

References

• Larsen and Schürmann, Nominal State-Separating Proofs
• Dupressoir et al., How Hard Can It Be?

Eval Simp Set

The ssprove_eval simp set collects all lemmas for evaluating deep embedding code into the shallow embedding.

Package-Level Evaluation

noncomputable def CatCrypt.Deep.DeepPackage.evalOp (p : DeepPackage) (op : ℕ) (dom codom : Type u) (h : (op, dom, codom) ∈ p.exports.ops) (x : dom) : Core.SPComp codom

Evaluate a single operation from a deep package to an SPComp function.

Given a package p with an exported operation (op, dom, codom), this evaluates the implementation code to a shallow SPComp computation.

Equations

• p.evalOp op dom codom h x = (p.impl op dom codom h x).code.eval

Code Equality → rHoare

theorem CatCrypt.Deep.rHoare_of_code_eq {α : Type u_1} (c₁ c₂ : RawCode α) (h : c₁ = c₂) : Relational.rHoare Relational.eqPre c₁.eval c₂.eval Relational.eqPost

Code equality gives eqPost from eqPre.

This is the key bridge lemma: if two RawCode programs are syntactically equal, their evaluations produce equal results from equal heaps.

For custom pre/post conditions, use rHoare_conseq after this lemma.

theorem CatCrypt.Deep.rHoare_of_eval_eq {α : Type u_1} (c₁ c₂ : RawCode α) (h : c₁.eval = c₂.eval) : Relational.rHoare Relational.eqPre c₁.eval c₂.eval Relational.eqPost

If two evaluations are equal as SPComp functions, rHoare holds.

@[simp]

theorem CatCrypt.Deep.eval_congr {α : Type u_1} (c₁ c₂ : RawCode α) (h : c₁ = c₂) : c₁.eval = c₂.eval

Code equality lifts to eval equality.

Package Operation Evaluation Lemmas

theorem CatCrypt.Deep.evalOp_par_left (p₁ p₂ : DeepPackage) (h_sep : p₁.sep p₂) (op : ℕ) (dom codom : Type u) (h₁ : (op, dom, codom) ∈ p₁.exports.ops) (x : dom) : (p₁.par p₂ h_sep).evalOp op dom codom ⋯ x = p₁.evalOp op dom codom h₁ x

Evaluating an operation from a parallel composition (left component).

Bridge Lemmas for Common Patterns

theorem CatCrypt.Deep.DeepRHoare_of_eq {α : Type u_1} (c₁ c₂ : RawCode α) (h : c₁ = c₂) : DeepRHoare Relational.eqPre c₁ c₂ Relational.eqPost

DeepRHoare from code equality (the most common bridge pattern).

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

DeepRHoare unfolds to rHoare on eval.

Bridge Tactics

def CatCrypt.Deep.tacticSsprove_deep_to_shallow : Lean.ParserDescr

ssprove_deep_to_shallow unfolds DeepRHoare to rHoare and simplifies eval.

This is the main entry point for moving from deep to shallow embedding. After applying this tactic, the goal will be a standard rHoare judgment on SPComp terms.

Example:

theorem example : DeepRHoare eqPre code₁ code₂ eqPost := by
  ssprove_deep_to_shallow
  -- Goal is now: rHoare eqPre (eval₁) (eval₂) eqPost
  -- where eval₁, eval₂ are simplified SPComp terms

Equations

• CatCrypt.Deep.tacticSsprove_deep_to_shallow = Lean.ParserDescr.node `CatCrypt.Deep.tacticSsprove_deep_to_shallow 1024 (Lean.ParserDescr.nonReservedSymbol "ssprove_deep_to_shallow" false)

def CatCrypt.Deep.tacticSsprove_eval : Lean.ParserDescr

ssprove_eval simplifies eval expressions in the goal.

This applies all evaluation lemmas to normalize deep embedding terms that have been evaluated into the shallow embedding.

Equations

• CatCrypt.Deep.tacticSsprove_eval = Lean.ParserDescr.node `CatCrypt.Deep.tacticSsprove_eval 1024 (Lean.ParserDescr.nonReservedSymbol "ssprove_eval" false)