Enhanced UC DSL (v2)

Extended notation and proof combinators for the UC factorization framework, eliminating boilerplate in UC proofs.

Component A: Protocol definition helpers

• UCProtocol.ofGame — wrap a game into UC protocol (the .inr boilerplate)
• UCSpec.ofGame — standard UC spec for game-to-game reductions

Component B: One-shot UC proof combinators

• UCEmulates_of_isPure_advantage — computational UC from IsPure + advantage bound
• UCEmulates_of_game_eq — perfect UC from program equality
• UCEmulates_of_game_sdist — sdist at game level implies UC

Component C: Game-hop chaining

• sdist_game_hop₂ — 2-step game hop
• sdist_game_hop₃ — 3-step game hop

Component D: Mixed Trans instances

• Trans for exact followed by approximate
• Trans for approximate followed by exact

Component E: Algebraic UC combinators

• UCEmulatesAlg composition tracking simulators
• Trans instance for algebraic calc-style proofs

Component A: Protocol Definition Helpers

noncomputable def CatCrypt.Crypto.UCDSL.UCProtocol.ofGame {hon leak : Type} (G : hon → Core.SPComp leak) : hon → Core.SPComp (Unit ⊕ leak)

Wrap a game into UC protocol form.

Eliminates the repetitive .inr wrapping pattern found in every *_UC.lean file. The game output goes through the .inr (leak/adversary) channel, while the honest output channel .inl carries Unit.

Equations

• CatCrypt.Crypto.UCDSL.UCProtocol.ofGame G x = (G x).bind fun (o : leak) => CatCrypt.Core.SPComp.pure (Sum.inr o)

@[reducible, inline]

abbrev CatCrypt.Crypto.UCDSL.UCSpec.ofGame (hon leak V : Type) : UCSpec

Standard UC specification for game-to-game reductions.

When reducing game G_real to G_ideal with the same leak type, the UC spec has out = Unit and leak = sim_if.

Equations

• CatCrypt.Crypto.UCDSL.UCSpec.ofGame hon leak V = { hon := hon, out := Unit, leak := leak, sim_if := leak, view := V }

Component B: One-Shot UC Proof Combinators

theorem CatCrypt.Crypto.UCDSL.UCEmulates_of_isPure_advantage {hon leak V : Type} {ε : ENNReal} {G_real G_ideal : hon → Core.SPComp leak} (hPure_r : ∀ (x : hon), (G_real x).IsPure) (hPure_i : ∀ (x : hon), (G_ideal x).IsPure) (hAdv : ∀ (D : leak → Core.SPComp Bool) (x : hon), absDiff (prTrue ((G_real x).bind D) Core.Heap.empty) (prTrue ((G_ideal x).bind D) Core.Heap.empty) ≤ ε) : UCEmulates ε (UCSpec.ofGame hon leak V) (UCProtocol.ofGame G_real) (UCProtocol.ofGame G_ideal)

Computational UC emulation from IsPure + advantage bound.

This is the most common pattern in UC proofs:

1. Both games are IsPure (built from sample/pure)
2. The advantage is bounded by ε
3. sdist_isPure_le reduces sdist to advantage
4. sdist_comp_right handles the .inr wrapping
5. UCEmulates_of_sdist gives UC security

Before (PRF_UC.lean, ~25 lines of IsPure proofs + sdist helper + UC theorem):

theorem prf_uc_secure ... := by
  apply UCEmulates_of_sdist
  exact le_trans (sdist_comp_right _ _ _) (prf_sdist F ε hAdv)

After (single application):

exact UCEmulates_of_isPure_advantage hPure_r hPure_i hAdv

theorem CatCrypt.Crypto.UCDSL.UCEmulates_of_game_eq {hon leak V : Type} {G_real G_ideal : hon → Core.SPComp leak} (h : G_real = G_ideal) : UCEmulates 0 (UCSpec.ofGame hon leak V) (UCProtocol.ofGame G_real) (UCProtocol.ofGame G_ideal)

Perfect UC emulation from program equality.

When the real and ideal games are extensionally equal, UC emulation holds with ε = 0. This covers the OTP pattern.

Before (OTP_UC.lean):

apply UCEmulates_of_sdist
rw [otpReal_eq_otpIdeal]
exact le_of_eq (sdist_self _)

After:

exact UCEmulates_of_game_eq otpReal_eq_otpIdeal

theorem CatCrypt.Crypto.UCDSL.UCEmulates_of_game_sdist {hon leak V : Type} {ε : ENNReal} {G_real G_ideal : hon → Core.SPComp leak} (h : sdist G_real G_ideal ≤ ε) : UCEmulates ε (UCSpec.ofGame hon leak V) (UCProtocol.ofGame G_real) (UCProtocol.ofGame G_ideal)

UC emulation from sdist bound at the game level.

When sdist G_real G_ideal ≤ ε, UC emulation holds. The .inr wrapping is handled automatically via sdist_comp_right.

theorem CatCrypt.Crypto.UCDSL.UCEmulates_of_isPure_advantageA {hon leak V : Type} {ε : ENNReal} {G_real G_ideal : hon → Core.SPComp leak} (hPure_r : ∀ (x : hon), (G_real x).IsPure) (hPure_i : ∀ (x : hon), (G_ideal x).IsPure) (hAdv : ∀ (x : hon) (D : leak → Core.SPComp Bool), AdvantageA (G_real x) (G_ideal x) D ≤ ε) : UCEmulates ε (UCSpec.ofGame hon leak V) (UCProtocol.ofGame G_real) (UCProtocol.ofGame G_ideal)

Variant of UCEmulates_of_isPure_advantage using AdvantageA.

Takes advantage bounds in the form AdvantageA (G_real x) (G_ideal x) D ≤ ε that appears directly in most security definitions.

Component C: Game-Hop Chaining

theorem CatCrypt.Crypto.UCDSL.sdist_game_hop₂ {α β : Type} {ε₁ ε₂ : ENNReal} {G₀ G₁ G₂ : α → Core.SPComp β} (h₁ : sdist G₀ G₁ ≤ ε₁) (h₂ : sdist G₁ G₂ ≤ ε₂) : sdist G₀ G₂ ≤ ε₁ + ε₂

2-step game hop (covers HKDF_UC pattern).

If sdist G₀ G₁ ≤ ε₁ and sdist G₁ G₂ ≤ ε₂, then sdist G₀ G₂ ≤ ε₁ + ε₂.

theorem CatCrypt.Crypto.UCDSL.sdist_game_hop₃ {α β : Type} {ε₁ ε₂ ε₃ : ENNReal} {G₀ G₁ G₂ G₃ : α → Core.SPComp β} (h₁ : sdist G₀ G₁ ≤ ε₁) (h₂ : sdist G₁ G₂ ≤ ε₂) (h₃ : sdist G₂ G₃ ≤ ε₃) : sdist G₀ G₃ ≤ ε₁ + ε₂ + ε₃

3-step game hop (covers CascadePRF_UC pattern).

If sdist Gᵢ Gᵢ₊₁ ≤ εᵢ for i = 0, 1, 2, then sdist G₀ G₃ ≤ ε₁ + ε₂ + ε₃.

theorem CatCrypt.Crypto.UCDSL.sdist_game_hop₄ {α β : Type} {ε₁ ε₂ ε₃ ε₄ : ENNReal} {G₀ G₁ G₂ G₃ G₄ : α → Core.SPComp β} (h₁ : sdist G₀ G₁ ≤ ε₁) (h₂ : sdist G₁ G₂ ≤ ε₂) (h₃ : sdist G₂ G₃ ≤ ε₃) (h₄ : sdist G₃ G₄ ≤ ε₄) : sdist G₀ G₄ ≤ ε₁ + ε₂ + ε₃ + ε₄

4-step game hop (covers Cryptobox compositional decomposition).

If sdist Gᵢ Gᵢ₊₁ ≤ εᵢ for i = 0, 1, 2, 3, then sdist G₀ G₄ ≤ ε₁ + ε₂ + ε₃ + ε₄.

theorem CatCrypt.Crypto.UCDSL.UCEmulates_game_hop₂ {hon leak V : Type} {ε₁ ε₂ : ENNReal} {G₀ G₁ G₂ : hon → Core.SPComp leak} (h₁ : sdist G₀ G₁ ≤ ε₁) (h₂ : sdist G₁ G₂ ≤ ε₂) : UCEmulates (ε₁ + ε₂) (UCSpec.ofGame hon leak V) (UCProtocol.ofGame G₀) (UCProtocol.ofGame G₂)

UC emulation via 2-step game hop.

Chains two game hops at the UC level.

Component E: Algebraic UC Combinators

def CatCrypt.Crypto.UCDSL.«term_⟶ₐ[_,_]_» : Lean.TrailingParserDescr

Notation for algebraic UC emulation.

Equations

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

theorem CatCrypt.Crypto.UCDSL.uc_alg_comp {hon out leak view : Type} {ε₁ ε₂ : ENNReal} {π₁ π₂ π₃ : hon → Core.SPComp (out ⊕ leak)} {Sim₁ Sim₂ : UCAlg.SimConstruction { hon := hon, out := out, leak := leak, sim_if := leak, view := view }} (h₁ : UCAlg.UCEmulatesAlg ε₁ { hon := hon, out := out, leak := leak, sim_if := leak, view := view } π₁ π₂ Sim₁) (h₂ : UCAlg.UCEmulatesAlg ε₂ { hon := hon, out := out, leak := leak, sim_if := leak, view := view } π₂ π₃ Sim₂) : UCAlg.UCEmulatesAlg (ε₁ + ε₂) { hon := hon, out := out, leak := leak, sim_if := leak, view := view } π₁ π₃ (Sim₂ ∘ Sim₁)

Composition of algebraic UC emulations tracking simulators.

If π₁ ⟶ₐ[ε₁, Sim₁] π₂ and π₂ ⟶ₐ[ε₂, Sim₂] π₃, then π₁ ⟶ₐ[ε₁ + ε₂, Sim₂ ∘ Sim₁] π₃.

theorem CatCrypt.Crypto.UCDSL.uc_alg_of_sdist {hon out leak view : Type} {ε : ENNReal} {G_real G_ideal : hon → Core.SPComp (out ⊕ leak)} (h : sdist G_real G_ideal ≤ ε) : UCAlg.UCEmulatesAlg ε { hon := hon, out := out, leak := leak, sim_if := leak, view := view } G_real G_ideal UCAlg.SimConstruction.id

Algebraic UC from sdist with identity simulator.

@[instance_reducible]

instance CatCrypt.Crypto.UCDSL.ucEmulatesAlg_trans_inst {hon out leak view : Type} {ε₁ ε₂ : ENNReal} {Sim₁ Sim₂ : UCAlg.SimConstruction { hon := hon, out := out, leak := leak, sim_if := leak, view := view }} : Trans (fun (π₁ π₂ : hon → Core.SPComp (out ⊕ leak)) => UCAlg.UCEmulatesAlg ε₁ { hon := hon, out := out, leak := leak, sim_if := leak, view := view } π₁ π₂ Sim₁) (fun (π₂ π₃ : hon → Core.SPComp (out ⊕ leak)) => UCAlg.UCEmulatesAlg ε₂ { hon := hon, out := out, leak := leak, sim_if := leak, view := view } π₂ π₃ Sim₂) fun (π₁ π₃ : hon → Core.SPComp (out ⊕ leak)) => UCAlg.UCEmulatesAlg (ε₁ + ε₂) { hon := hon, out := out, leak := leak, sim_if := leak, view := view } π₁ π₃ (Sim₂ ∘ Sim₁)

Trans instance for algebraic UC calc-style proofs.

Equations

• CatCrypt.Crypto.UCDSL.ucEmulatesAlg_trans_inst = { trans := ⋯ }

Utility: ofGame distributes over function application

@[simp]

theorem CatCrypt.Crypto.UCDSL.UCProtocol.ofGame_apply {hon leak : Type} (G : hon → Core.SPComp leak) (x : hon) : ofGame G x = (G x).bind fun (o : leak) => Core.SPComp.pure (Sum.inr o)

@[simp]

theorem CatCrypt.Crypto.UCDSL.UCSpec.ofGame_eq {hon leak V : Type} : ofGame hon leak V = { hon := hon, out := Unit, leak := leak, sim_if := leak, view := V }

UCSpec.ofGame expands to the expected anonymous constructor.