NomPkg Bridge: Game-Based Security → sdist

This file bridges game-based security (∀ A, Advantage ≤ ε) to the categorical sdist framework, enabling composition via post-processing lemmas.

Main results

• SPComp.NoFail — computation never produces failure
• sdist_le_of_advantage_bool — sdist for Bool-valued IsPure+NoFail SPComps from Advantage
• sdist_of_deepNomAdvantage — bridge for deep nominal packages
• nomPkg_absorb — general absorption of post-processing into the adversary

Key insight

For Bool-valued IsPure+NoFail computations, any post-processing distinguisher D : Bool → SPComp Bool cannot increase the advantage beyond what the identity distinguisher achieves. This is a post-processing lemma for binary channels.

NoFail

def CatCrypt.Crypto.SPComp.NoFail {α : Type u_1} (c : Core.SPComp α) : Prop

A computation never fails: all mass is on successful outcomes.

Equations

• CatCrypt.Crypto.SPComp.NoFail c = ∀ (h : CatCrypt.Core.Heap), (c h) none = 0

theorem CatCrypt.Crypto.SPComp.pure_noFail {α : Type u_1} (a : α) : NoFail (Core.SPComp.pure a)

pure a never fails.

Compositional NoFail helpers

theorem CatCrypt.Crypto.Assumptions.SPComp.bind_noFail {α : Type u_1} {β : Type u_2} {c : Core.SPComp α} {f : α → Core.SPComp β} (hc : SPComp.NoFail c) (hf : ∀ (a : α), SPComp.NoFail (f a)) : SPComp.NoFail (c.bind f)

Bind preserves NoFail: if c is NoFail and every f a is NoFail, then c >>= f is NoFail.

theorem CatCrypt.Crypto.Assumptions.SPComp.sample_noFail {α : Type} [Fintype α] [Nonempty α] : SPComp.NoFail (Core.SPComp.sample α)

SPComp.sample is NoFail: uniform distributions assign 0 mass to the failure slot.

IsPure + NoFail Helpers

theorem CatCrypt.Crypto.isPure_bind_eq {α : Type u_1} {β : Type u_2} {c : Core.SPComp α} {d : Prob.SDistr α} (hc : ∀ (h : Core.Heap), c h = d.bind fun (a : α) => Prob.SDistr.pure (a, h)) (D : α → Core.SPComp β) (h₀ : Core.Heap) : c.bind D h₀ = d.bind fun (a : α) => D a h₀

For IsPure c, the bind c >>= D at h₀ equals d.bind(fun a => D a h₀).

theorem CatCrypt.Crypto.isPure_noFail_d_none {α : Type u_1} {c : Core.SPComp α} {d : Prob.SDistr α} (hc : ∀ (h : Core.Heap), c h = d.bind fun (a : α) => Prob.SDistr.pure (a, h)) (hnf : SPComp.NoFail c) : d none = 0

For IsPure+NoFail, the witness distribution d has d(none) = 0.

theorem CatCrypt.Crypto.isPure_bind_some_ne {c : Core.SPComp Bool} {d : Prob.SDistr Bool} (hc : ∀ (h : Core.Heap), c h = d.bind fun (a : Bool) => Prob.SDistr.pure (a, h)) (h₀ h : Core.Heap) (b : Bool) (hne : h ≠ h₀) : (c h₀) (some (b, h)) = 0

For IsPure c : SPComp Bool with witness d, the bind (d.bind f)(some(b, h₀)) is zero when h ≠ h₀, because d.bind produces outputs only at heap h₀.

theorem CatCrypt.Crypto.prTrue_isPure_eq {c : Core.SPComp Bool} {d : Prob.SDistr Bool} (hc : ∀ (h : Core.Heap), c h = d.bind fun (a : Bool) => Prob.SDistr.pure (a, h)) (h₀ : Core.Heap) : prTrue c h₀ = d (some true)

For IsPure c : SPComp Bool, prTrue c h₀ = d(some true) for any h₀. The heap doesn't affect the output distribution.

theorem CatCrypt.Crypto.isPure_noFail_complement {d : Prob.SDistr Bool} (hnf : d none = 0) : d (some false) = 1 - d (some true)

For IsPure+NoFail d : SDistr Bool, d(some false) = 1 - d(some true).

theorem CatCrypt.Crypto.isPure_noFail_le_one {d : Prob.SDistr Bool} (hnf : d none = 0) : d (some true) ≤ 1

For IsPure+NoFail, d(some true) ≤ 1.

Algebraic Inequality: Convex Combination Bound

theorem CatCrypt.Crypto.convex_le_add_tsub₁ {x y : ENNReal} (r s : ENNReal) (hrs : r ≤ s) (hs1 : s ≤ 1) (hy : y ≤ 1) : r * x + (1 - r) * y ≤ s * x + (1 - s) * y + (s - r)

Auxiliary: for r ≤ s ≤ 1, the expression with smaller weight r is bounded by the expression with larger weight s plus the weight difference (s - r). This is one direction of the convex bound.

theorem CatCrypt.Crypto.convex_le_add_tsub₂ {x y : ENNReal} (r s : ENNReal) (hrs : r ≤ s) (_hs1 : s ≤ 1) (hx : x ≤ 1) : s * x + (1 - s) * y ≤ r * x + (1 - r) * y + (s - r)

Auxiliary: the reverse direction — the expression with larger weight s is also bounded by the expression with smaller weight r plus (s - r).

theorem CatCrypt.Crypto.absDiff_convex_le (p q x y : ENNReal) (hp : p ≤ 1) (hq : q ≤ 1) (hx : x ≤ 1) (hy : y ≤ 1) : absDiff (p * x + (1 - p) * y) (q * x + (1 - q) * y) ≤ absDiff p q

Key algebraic fact: the absDiff of two convex combinations (with the same endpoints but different weights) is bounded by the absDiff of the weights.

This is the post-processing lemma for binary channels.

prTrue Decomposition for IsPure+NoFail Bool

theorem CatCrypt.Crypto.prTrue_isPure_noFail_bind {c : Core.SPComp Bool} {d : Prob.SDistr Bool} (hc : ∀ (h : Core.Heap), c h = d.bind fun (a : Bool) => Prob.SDistr.pure (a, h)) (hnf : d none = 0) (D : Bool → Core.SPComp Bool) (h₀ : Core.Heap) : prTrue (c.bind D) h₀ = d (some true) * prTrue (D true) h₀ + d (some false) * prTrue (D false) h₀

For IsPure+NoFail c : SPComp Bool, prTrue(c >>= D, h₀) decomposes as p * prTrue(D true, h₀) + (1-p) * prTrue(D false, h₀) where p = d(some true).

D-Absorption for Bool (Post-Processing Lemma)

theorem CatCrypt.Crypto.absDiff_bind_le_advantage {c₁ c₂ : Core.SPComp Bool} (hc₁ : c₁.IsPure) (hc₂ : c₂.IsPure) (hnf₁ : SPComp.NoFail c₁) (hnf₂ : SPComp.NoFail c₂) (D : Bool → Core.SPComp Bool) (h₀ : Core.Heap) : absDiff (prTrue (c₁.bind D) h₀) (prTrue (c₂.bind D) h₀) ≤ Advantage c₁ c₂

Core D-absorption: for IsPure+NoFail c₁, c₂ : SPComp Bool, any D cannot increase the advantage beyond what the identity distinguisher achieves.

Main Bridge: Advantage → sdist

theorem CatCrypt.Crypto.sdist_le_of_advantage_bool {α : Type u_1} {f g : α → Core.SPComp Bool} {ε : ENNReal} (hf_pure : ∀ (a : α), (f a).IsPure) (hg_pure : ∀ (a : α), (g a).IsPure) (hf_nf : ∀ (a : α), SPComp.NoFail (f a)) (hg_nf : ∀ (a : α), SPComp.NoFail (g a)) (hAdv : ∀ (a : α), Advantage (f a) (g a) ≤ ε) : sdist f g ≤ ε

Main bridge theorem: for Bool-valued IsPure+NoFail computations, ∀ a, Advantage(f a)(g a) ≤ ε implies sdist f g ≤ ε.

This combines:

1. sdist_isPure_le — absorbs h₀ into the distinguisher via IsPure
2. absDiff_bind_le_advantage — D-absorption for Bool with NoFail

NomPkg Bridge

theorem CatCrypt.Crypto.sdist_of_deepNomAdvantage {G G' : Deep.NomPackage} {ε : ENNReal} (hPure_r : ∀ (A : Deep.NomPackage), (runPkg (A.pkg.link G.pkg)).IsPure) (hPure_i : ∀ (A : Deep.NomPackage), (runPkg (A.pkg.link G'.pkg)).IsPure) (hNF_r : ∀ (A : Deep.NomPackage), SPComp.NoFail (runPkg (A.pkg.link G.pkg))) (hNF_i : ∀ (A : Deep.NomPackage), SPComp.NoFail (runPkg (A.pkg.link G'.pkg))) (hAdv : ∀ (A : Deep.NomPackage), DeepNomAdvantage G G' A ≤ ε) : (sdist (fun (A : Deep.NomPackage) => runPkg (A.pkg.link G.pkg)) fun (A : Deep.NomPackage) => runPkg (A.pkg.link G'.pkg)) ≤ ε

Bridge for deep nominal packages: game-based security implies sdist bound.

Given ∀ A : NomPkg, DeepNomAdvantage G G' A ≤ ε, this yields sdist (fun A => runPkg(link A G)) (fun A => runPkg(link A G')) ≤ ε.

Requires IsPure+NoFail for the linked computations. Universe parameters are pinned to avoid auto-binding divergence.

General Absorption Bridge

theorem CatCrypt.Crypto.sdist_le_of_advantage_absorb {α : Type u_1} {f g : α → Core.SPComp Bool} {ε : ENNReal} (h_absorb : ∀ (D : Bool → Core.SPComp Bool) (a : α) (h₀ : Core.Heap), ∃ (a' : α), absDiff (prTrue ((f a).bind D) h₀) (prTrue ((g a).bind D) h₀) ≤ Advantage (f a') (g a')) (hAdv : ∀ (a : α), Advantage (f a) (g a) ≤ ε) : sdist f g ≤ ε

General absorption bridge: if for every (D, a, h₀) triple there exists an a' whose Advantage dominates the post-processed advantage, then sdist f g ≤ ε.

This cleanly separates:

• General math (this theorem): absorption implies sdist bound
• Protocol-specific claim (caller-provided): the adversary space can absorb post-processing D and initial heap h₀

NomPkg Absorption via Eval Completeness

The key theorem: for any game pair (G, G'), post-processor D, adversary A, and initial heap h₀, there exists A' such that the post-processed absDiff is bounded by A's Advantage.

This uses RawCode.ofSPComp (from EvalComplete) to embed arbitrary SPComp computations into the deep embedding, enabling construction of A' that wraps A's oracle-calling code with heap reset and post-processing.

noncomputable def CatCrypt.Crypto.heapReset (h₀ : Core.Heap) : Core.SPComp Unit

Reset heap to a target state. All existing heap contents are replaced.

Equations

• CatCrypt.Crypto.heapReset h₀ x✝ = CatCrypt.Prob.SDistr.pure ((), h₀)

theorem CatCrypt.Crypto.heapReset_apply (h₀ h : Core.Heap) : heapReset h₀ h = Prob.SDistr.pure ((), h₀)

heapReset h₀ at any initial heap produces ((), h₀).

theorem CatCrypt.Crypto.bind_heapReset {β : Type u_1} (h₀ : Core.Heap) (f : Unit → Core.SPComp β) (h : Core.Heap) : (heapReset h₀).bind f h = f () h₀

Binding with heapReset shifts the initial heap. SPComp.bind (heapReset h₀) f at any heap h equals f () h₀.

theorem CatCrypt.Crypto.prTrue_bind_heapReset (h₀ : Core.Heap) (c : Core.SPComp Bool) : prTrue ((heapReset h₀).bind fun (x : Unit) => c) Core.Heap.empty = prTrue c h₀

prTrue after heap reset shifts the initial heap.

noncomputable def CatCrypt.Crypto.wrapMainNomPkg (A : Deep.NomPackage) (h_main : (0, Unit, Bool) ∈ A.pkg.exports.ops) (D : Bool → Core.SPComp Bool) (h₀ : Core.Heap) : Deep.NomPackage

Construct a NomPkg that wraps A's main export with heap reset and post-processing D. A' has the same exports, imports, and locations as A, but the (0, Unit, Bool) export is wrapped:

• Phase 1: ofSPComp(heapReset h₀) — reset heap (no oracle calls)
• Phase 2: A's original code (with oracle calls to game)
• Phase 3: ofSPComp(D b) — post-process (no oracle calls)

Equations

• One or more equations did not get rendered due to their size.

theorem CatCrypt.Crypto.wrapMainNomPkg_impl_code (A : Deep.NomPackage) (h_main : (0, Unit, Bool) ∈ A.pkg.exports.ops) (D : Bool → Core.SPComp Bool) (h₀ : Core.Heap) (h' : (0, Unit, Bool) ∈ (wrapMainNomPkg A h_main D h₀).pkg.exports.ops) : ((wrapMainNomPkg A h_main D h₀).pkg.impl 0 Unit Bool h' ()).code = (Deep.RawCode.ofSPComp (heapReset h₀)).bind fun (x : Unit) => (A.pkg.impl 0 Unit Bool h_main ()).code.bind fun (b : Bool) => Deep.RawCode.ofSPComp (D b)

Key evaluation lemma: runPkg(wrapMain(A).link(G)) at Heap.empty equals runPkg(A.link(G)).bind(D) at h₀.

After linking with G, oracle calls in A's code get resolved. The ofSPComp phases (heapReset and D) are transparent to substOracle.

theorem CatCrypt.Crypto.runPkg_wrapMain_eq (A G : Deep.NomPackage) (h_main : (0, Unit, Bool) ∈ A.pkg.exports.ops) (D : Bool → Core.SPComp Bool) (h₀ : Core.Heap) : prTrue (runPkg ((wrapMainNomPkg A h_main D h₀).pkg.link G.pkg)) Core.Heap.empty = prTrue ((runPkg (A.pkg.link G.pkg)).bind D) h₀

theorem CatCrypt.Crypto.nomPkg_absorb (G G' : Deep.NomPackage) (D : Bool → Core.SPComp Bool) (A : Deep.NomPackage) (h₀ : Core.Heap) : ∃ (A' : Deep.NomPackage), absDiff (prTrue ((runPkg (A.pkg.link G.pkg)).bind D) h₀) (prTrue ((runPkg (A.pkg.link G'.pkg)).bind D) h₀) ≤ Advantage (runPkg (A'.pkg.link G.pkg)) (runPkg (A'.pkg.link G'.pkg))

General NomPkg absorption theorem.

For any game pair (G, G'), post-processor D, adversary A, and initial heap h₀, there exists A' whose Advantage dominates the post-processed absDiff. This is the core lemma for lifting game-based security to sdist.

The construction: A' wraps A's main export with heapReset h₀ (to shift the initial heap) and D (to absorb post-processing). After linking with G, the oracle calls in A's code get resolved as before, while the ofSPComp phases are transparent to substOracle.

This eliminates the need for IsPure/NoFail assumptions.

Automation Tactic

def CatCrypt.Crypto.tacticSdist_from_deep : Lean.ParserDescr

Tactic: bridge game-based advantage to sdist bound for NomPkg games.

Equations

• CatCrypt.Crypto.tacticSdist_from_deep = Lean.ParserDescr.node `CatCrypt.Crypto.tacticSdist_from_deep 1024 (Lean.ParserDescr.nonReservedSymbol "sdist_from_deep" false)

def CatCrypt.Crypto.tacticUc_from_deep : Lean.ParserDescr

Tactic: bridge a deep nominal advantage bound to a UCEmulates goal, via UCEmulates_of_sdist then sdist_from_deep.

Equations

• CatCrypt.Crypto.tacticUc_from_deep = Lean.ParserDescr.node `CatCrypt.Crypto.tacticUc_from_deep 1024 (Lean.ParserDescr.nonReservedSymbol "uc_from_deep" false)