Deep Embedding: ProofFrog-Style Transformations

This file provides ProofFrog-style code transformations for the deep embedding. Unlike the shallow embedding tactics in CatCrypt/Tactics/ProofFrog.lean, these operate directly on RawCode syntax trees, matching ProofFrog's approach.

Overview

ProofFrog performs automatic game transformations by:

1. Parsing games into ASTs
2. Applying canonicalization and simplification passes
3. Using Z3 to check equivalence

Our deep embedding (RawCode) similarly represents code as syntax trees, enabling structural transformations with machine-checked proofs.

Important: Semantic vs Syntactic Equality

RawCode is a free monad where bind is a constructor, not a function. This means the monad laws do NOT hold syntactically:

• RawCode.bind (RawCode.ret x) f ≠ f x (syntactically)
• They ARE equal after eval to distributions

All transformations in this file are proven at the evaluation level, which is the correct semantics for game-based cryptographic proofs.

Main Theorems

Monad Laws (Semantic)

• eval_ret_bind - Left identity at evaluation level
• eval_bind_ret - Right identity at evaluation level
• eval_bind_assoc - Associativity at evaluation level

Dead Code Elimination (Semantic)

• dead_sample_eval - Unused sample can be eliminated
• dead_ret_eval - Unused pure value can be eliminated

Copy Propagation (Semantic)

• copy_ret_eval - Pure value substitution

Comparison with ProofFrog

ProofFrog	Deep Embedding
AST in Python	RawCode inductive
Automatic passes	Explicit lemmas
Z3 for equivalence	Lean's kernel
Syntactic rewriting	Semantic (eval) equality

References

• ProofFrog: https://github.com/ProofFrog/ProofFrog
• [Barbosa et al., "Mechanizing Proofs about Adversaries"]

Semantic Monad Laws

Since RawCode.bind is a constructor (free monad), monad laws only hold after evaluation to distributions. These are the fundamental laws for reasoning.

theorem CatCrypt.Deep.RawCode.eval_ret_bind {α β : Type} (x : α) (f : α → RawCode β) : ((ret x).bind f).eval = (f x).eval

Left identity: (ret x >>= f).eval = (f x).eval

Uses the simp lemmas eval_ret and eval_bind from Eval.lean.

theorem CatCrypt.Deep.RawCode.eval_bind_ret {α : Type} (m : RawCode α) : (m.bind ret).eval = m.eval

Right identity: (m >>= ret).eval = m.eval

Uses the axioms from Eval.lean and SPComp.bind_pure.

theorem CatCrypt.Deep.RawCode.eval_bind_assoc {α β γ : Type} (m : RawCode α) (f : α → RawCode β) (g : β → RawCode γ) : ((m.bind f).bind g).eval = (m.bind fun (x : α) => (f x).bind g).eval

Associativity: ((m >>= f) >>= g).eval = (m >>= (λ x => f x >>= g)).eval

Uses the axioms from Eval.lean and SPComp.bind_assoc.

Dead Code Elimination

When a computation's result is not used, it can be eliminated (for pure/terminating computations). All results are at the evaluation level.

theorem CatCrypt.Deep.RawCode.dead_sample_eval {α β : Type} [Fintype α] [Nonempty α] (k : RawCode β) : ((sample α).bind fun (x : α) => k).eval = k.eval

Dead sample at evaluation level: unused sample produces same distribution.

Key insight: sample returns (uniform α).bind (fun a => pure (a, h)), so when we ignore the result and continue with k, we get: (uniform α).bind (fun _ => k.eval h) = k.eval h by uniform_bind_const

theorem CatCrypt.Deep.RawCode.dead_ret_eval {α β : Type} (v : α) (k : RawCode β) : ((ret v).bind fun (x : α) => k).eval = k.eval

Dead ret elimination at evaluation level: (ret v >>= λ _ => k).eval = k.eval

Copy Propagation

When a value is bound and then used, substitute directly.

theorem CatCrypt.Deep.RawCode.copy_ret_eval {α β : Type} (v : α) (f : α → RawCode β) : ((ret v).bind f).eval = (f v).eval

After let x ← ret v, uses of x become v at evaluation level.

Structural Equality Lemmas

These help prove two RawCode values have equal evaluations.

theorem CatCrypt.Deep.RawCode.eval_bind_congr {α β : Type} (m₁ m₂ : RawCode α) (f₁ f₂ : α → RawCode β) (hm : m₁.eval = m₂.eval) (hf : ∀ (a : α), (f₁ a).eval = (f₂ a).eval) : (m₁.bind f₁).eval = (m₂.bind f₂).eval

Two binds have equal evaluations if their components have equal evaluations.

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

Evaluation is preserved by code equality.

Canonicalization

Put code into a standard form for easier comparison.

theorem CatCrypt.Deep.RawCode.canonicalize_bind {α β γ : Type} (m : RawCode α) (f : α → RawCode β) (g : β → RawCode γ) : ((m.bind f).bind g).eval = (m.bind fun (x : α) => (f x).bind g).eval

Canonical form has binds right-associated (at evaluation level).

theorem CatCrypt.Deep.RawCode.inline_ret {α β : Type} (x : α) (f : α → RawCode β) : ((ret x).bind f).eval = (f x).eval

Inline pure values (at evaluation level).

Summary

This file provides the deep embedding counterparts to ProofFrog's transformations:

ProofFrog Pass	Deep Embedding Lemma
Inline	RawCode.eval_ret_bind
Dead code	RawCode.dead_sample_eval, RawCode.dead_ret_eval
Copy propagation	RawCode.copy_ret_eval
Canonicalize	RawCode.eval_bind_assoc, RawCode.eval_bind_ret

Key difference from ProofFrog:

ProofFrog operates on ASTs where Seq(Return x, k) = k(x) syntactically. CatCrypt's RawCode is a free monad where bind (ret x) k ≠ k x syntactically. All equalities are at the semantic (evaluation/distribution) level.

This is actually more correct for cryptographic proofs:

• What matters is that games produce the same distribution, not that they have identical syntax
• Semantic equality captures the security-relevant notion of indistinguishability

Line Count Comparison

Component	ProofFrog	CatCrypt Deep
Dead code elimination	~20 lines Python	~20 lines Lean
Copy propagation	~15 lines Python	~10 lines Lean
Canonicalization	~25 lines Python	~15 lines Lean
Total	~60 lines	~45 lines

The line counts are comparable because we prove semantic equivalence directly, avoiding the need for complex syntactic transformations. CatCrypt provides machine-checked soundness for each transformation.

Proof basis

The soundness theorems rest on:

• the axioms eval_ret, eval_bind, eval_sample from Eval.lean
• the SPComp monad laws: pure_bind, bind_pure, bind_assoc
• the SDistr lemma: uniform_bind_const