Reflection → Package → UC: shared lift helpers

Examples/OneTimePad.lean lifts a shallow perfect-security result to a composable statement about deep nominal packages, following the stack shallow game → rawCode% → NomPackage.ofOracle → DeepNomAdvantage → sdist → UC. This file extracts the reusable boilerplate of that lift so each perfect-security example reduces to: reflect the two game bodies, prove their evaluations coincide, and instantiate the ofOracle combinators below.

Main results

• spcomp_eq_of_isPure_coupling — for two IsPure computations, an empty-heap perfect coupling (rHoare eqPre _ _ eqPost) upgrades to full SPComp equality. This is what turns an existing shallow coupling into the .eval equality the ofOracle combinators consume, with no purity bridge on the adversary.
• AdvantageA_pure — AdvantageA g₀ g₁ SPComp.pure = Advantage g₀ g₁.
• UCEmulates_of_boolGame_sdist — from sdist g₀ g₁ ≤ ε on two SPComp Bool game families, conclude UCEmulates ε over the trivial-leak spec via the Sum.inl : Bool → Bool ⊕ Empty wrapper.
• evalOp_singleton_congr — discharges runPkg_link_congr's per-op obligation for a single-oracle ofOracle package.
• runPkg_link_ofOracle_congr — linked runs coincide against every adversary when the two oracle bodies have equal evaluations.
• deepNomAdvantage_ofOracle_zero, sdist_ofOracle_zero, nomPkgSecure_ofOracle, uc_ofOracle — the full perfect stack, each a one-line consequence of body .eval equality.

From a pure coupling to SPComp equality

theorem CatCrypt.Deep.spcomp_eq_of_isPure_coupling {α : Type} {G₀ G₁ : Core.SPComp α} (h₀ : G₀.IsPure) (h₁ : G₁.IsPure) (hc : Relational.rHoare Relational.eqPre G₀ G₁ Relational.eqPost) : G₀ = G₁

For two heap-independent (IsPure) computations, an empty-heap perfect coupling rHoare eqPre G₀ G₁ eqPost upgrades to full SPComp equality G₀ = G₁. The coupling fixes the empty-heap distributions; purity extends that agreement to every heap via push_inj.

This is the bridge that lets a shallow perfect-security coupling feed the ofOracle combinators below without any IsPure/NoFail post-processing hypothesis on the adversary.

Advantage / UC packaging

theorem CatCrypt.Deep.AdvantageA_pure (g₀ g₁ : Core.SPComp Bool) : Crypto.AdvantageA g₀ g₁ Core.SPComp.pure = Crypto.Advantage g₀ g₁

The identity distinguisher is a no-op: AdvantageA g₀ g₁ pure = Advantage g₀ g₁.

theorem CatCrypt.Deep.UCEmulates_of_boolGame_sdist {ι : Type u_1} {ε : ENNReal} (g₀ g₁ : ι → Core.SPComp Bool) (h : Crypto.sdist g₀ g₁ ≤ ε) : Crypto.UCEmulates ε { hon := ι, out := Bool, leak := Empty, sim_if := Empty, view := Bool } (fun (a : { hon := ι, out := Bool, leak := Empty, sim_if := Empty, view := Bool }.hon) => Core.SPComp.map Sum.inl (g₀ a)) fun (a : { hon := ι, out := Bool, leak := Empty, sim_if := Empty, view := Bool }.hon) => Core.SPComp.map Sum.inl (g₁ a)

From a statistical-distance bound on two SPComp Bool game families, conclude UCEmulates over the trivial-leak interface (out = Bool, leak = Empty), wrapping each output through Sum.inl : Bool → Bool ⊕ Empty. Post-composition with the pure injection Sum.inl is non-expansive (sdist_comp_right), so the wrapped distance is still ≤ ε and UCEmulates_of_sdist (identity simulator) applies.

The ofOracle perfect stack

The remaining combinators take two single-oracle ofOracle packages whose oracle bodies have equal evaluations and derive the full package-level perfect-security stack. Feed each with the .eval equality of the reflected game bodies (obtained, for a shallow perfect coupling, via spcomp_eq_of_isPure_coupling).

theorem CatCrypt.Deep.evalOp_singleton_congr {op : ℕ} {dom codom : Type} (impl₀ impl₁ : dom → RawCode codom) [∀ (x : dom), IsValid ∅ (impl₀ x)] [∀ (x : dom), IsValid ∅ (impl₁ x)] (h : ∀ (x : dom), (impl₀ x).eval = (impl₁ x).eval) (op' : ℕ) (dom' codom' : Type) (h₁ : (op', dom', codom') ∈ (NomPackage.ofOracle op dom codom impl₀).pkg.exports.ops) (h₂ : (op', dom', codom') ∈ (NomPackage.ofOracle op dom codom impl₁).pkg.exports.ops) (x : dom') : ((NomPackage.ofOracle op dom codom impl₀).pkg.impl op' dom' codom' h₁ x).code.eval = ((NomPackage.ofOracle op dom codom impl₁).pkg.impl op' dom' codom' h₂ x).code.eval

Discharges runPkg_link_congr's per-op obligation for two ofOracle packages that export the same single oracle (op, dom, codom): singleton membership forces the queried operation to be that oracle, whereupon evalOp_ofOracle reduces both sides to the reflected bodies, equal by hypothesis.

theorem CatCrypt.Deep.runPkg_link_ofOracle_congr {op : ℕ} {dom codom : Type} (impl₀ impl₁ : dom → RawCode codom) [∀ (x : dom), IsValid ∅ (impl₀ x)] [∀ (x : dom), IsValid ∅ (impl₁ x)] (h : ∀ (x : dom), (impl₀ x).eval = (impl₁ x).eval) (A : NomPackage) : Crypto.runPkg (A.pkg.link (NomPackage.ofOracle op dom codom impl₀).pkg) = Crypto.runPkg (A.pkg.link (NomPackage.ofOracle op dom codom impl₁).pkg)

Linking any adversary package A with either of two ofOracle games produces the same SPComp Bool, when the two oracle bodies have equal evaluations. The single per-op obligation of runPkg_link_congr is evalOp_singleton_congr; the interfaces agree by rfl.

theorem CatCrypt.Deep.deepNomAdvantage_ofOracle_zero {op : ℕ} {dom codom : Type} (impl₀ impl₁ : dom → RawCode codom) [∀ (x : dom), IsValid ∅ (impl₀ x)] [∀ (x : dom), IsValid ∅ (impl₁ x)] (h : ∀ (x : dom), (impl₀ x).eval = (impl₁ x).eval) (A : NomPackage) : Crypto.DeepNomAdvantage (NomPackage.ofOracle op dom codom impl₀) (NomPackage.ofOracle op dom codom impl₁) A = 0

Zero deep-nominal advantage against every adversary package: the reflected real/ideal games are perfectly indistinguishable in the deep package model.

theorem CatCrypt.Deep.sdist_ofOracle_zero {op : ℕ} {dom codom : Type} (impl₀ impl₁ : dom → RawCode codom) [∀ (x : dom), IsValid ∅ (impl₀ x)] [∀ (x : dom), IsValid ∅ (impl₁ x)] (h : ∀ (x : dom), (impl₀ x).eval = (impl₁ x).eval) : (Crypto.sdist (fun (A : NomPackage) => Crypto.runPkg (A.pkg.link (NomPackage.ofOracle op dom codom impl₀).pkg)) fun (A : NomPackage) => Crypto.runPkg (A.pkg.link (NomPackage.ofOracle op dom codom impl₁).pkg)) = 0

Statistical distance zero between the two linked-game families. Since the linked runs coincide against every adversary, the two functions are equal, and sdist_self collapses the distance — no purity bridge on the adversary.

theorem CatCrypt.Deep.nomPkgSecure_ofOracle {op : ℕ} {dom codom : Type} (impl₀ impl₁ : dom → RawCode codom) [∀ (x : dom), IsValid ∅ (impl₀ x)] [∀ (x : dom), IsValid ∅ (impl₁ x)] (h : ∀ (x : dom), (impl₀ x).eval = (impl₁ x).eval) : Crypto.NomPkgSecure (NomPackage.ofOracle op dom codom impl₀) (NomPackage.ofOracle op dom codom impl₁) fun (x : NomPackage) => 0

Package-level perfect security (NomPkgSecure): the reflected games emulate each other with zero adversary-dependent error.

theorem CatCrypt.Deep.uc_ofOracle {op : ℕ} {dom codom : Type} (impl₀ impl₁ : dom → RawCode codom) [∀ (x : dom), IsValid ∅ (impl₀ x)] [∀ (x : dom), IsValid ∅ (impl₁ x)] (h : ∀ (x : dom), (impl₀ x).eval = (impl₁ x).eval) : Crypto.UCEmulates 0 { hon := NomPackage, out := Bool, leak := Empty, sim_if := Empty, view := Bool } (fun (A : { hon := NomPackage, out := Bool, leak := Empty, sim_if := Empty, view := Bool }.hon) => Core.SPComp.map Sum.inl (Crypto.runPkg (A.pkg.link (NomPackage.ofOracle op dom codom impl₀).pkg))) fun (A : { hon := NomPackage, out := Bool, leak := Empty, sim_if := Empty, view := Bool }.hon) => Core.SPComp.map Sum.inl (Crypto.runPkg (A.pkg.link (NomPackage.ofOracle op dom codom impl₁).pkg))

Perfect UC emulation of the linked-game families over the trivial-leak interface (out = Bool, leak = Empty): the identity simulator suffices because the linked runs coincide (sdist_ofOracle_zero).