Algebraic UC Emulation: Explicit Simulator Constructions

This file upgrades existential UC emulation (∀ A, ∃ S, ...) to a version that records the simulator as an explicit function A ↦ Sim(A) of the adversary. Most concrete UC proofs already build S as a concrete function of A, so this is the natural formulation; UCEmulatesAlg.forget re-extracts the existential UCEmulates when needed.

Main definitions

• SimConstruction — function (leak → SPComp view) → (sim_if → SPComp view) mapping each adversary to a simulator.
• UCEmulatesAlg — UC emulation with the explicit SimConstruction witness.

Main results

• UCEmulatesAlg.forget — algebraic implies existential (→ UCEmulates)
• UCEmulatesAlg_of_sdist — from sdist (same-interface, Sim = id)
• UCEmulatesAlg.refl — reflexivity (Sim = id)
• UCEmulatesAlg.trans — same-interface transitivity (composition of Sim)
• UCEmulatesAlg.trans_general — general transitivity through different interfaces
• SimConstruction.id_comp, comp_id, comp_assoc — composition laws (all rfl)

Composition structure

SimConstruction.id and SimConstruction.comp give a unit and an associative composition with both unit laws — these hold by rfl because SimConstruction is just a function and comp is function composition. Errors compose additively under the ℝ≥0∞ grading via UCEmulatesAlg.trans.

The earlier framing of this structure as an "approximate algebraic weak factorization system" was rhetorical: the small-object argument and genuine algebra structure of an AWFS are not used here — the content is "explicit simulator + sdist bound, composed pointwise".

Simulator Construction

def CatCrypt.Crypto.UCAlg.SimConstruction (spec : UCSpec) : Type

A simulator construction: a function from adversaries to simulators.

Given an adversary A : leak → SPComp view, produces a simulator Sim(A) : sim_if → SPComp view.

Equations

• CatCrypt.Crypto.UCAlg.SimConstruction spec = ((spec.leak → CatCrypt.Core.SPComp spec.view) → spec.sim_if → CatCrypt.Core.SPComp spec.view)

def CatCrypt.Crypto.UCAlg.SimConstruction.id {hon out leak view : Type} : SimConstruction { hon := hon, out := out, leak := leak, sim_if := leak, view := view }

Identity simulator construction (same-interface: leak = sim_if). The adversary IS the simulator.

Equations

• CatCrypt.Crypto.UCAlg.SimConstruction.id = id

def CatCrypt.Crypto.UCAlg.SimConstruction.comp {hon out leak₁ leak₂ leak₃ view : Type} (Sim₁ : SimConstruction { hon := hon, out := out, leak := leak₁, sim_if := leak₂, view := view }) (Sim₂ : SimConstruction { hon := hon, out := out, leak := leak₂, sim_if := leak₃, view := view }) : SimConstruction { hon := hon, out := out, leak := leak₁, sim_if := leak₃, view := view }

Composition of simulator constructions. comp Sim₁ Sim₂ first applies Sim₁ then Sim₂: given adversary A, the composed simulator is Sim₂(Sim₁(A)).

Equations

• Sim₁.comp Sim₂ = Sim₂ ∘ Sim₁

Composition Laws (all rfl since SimConstruction is a function)

@[simp]

theorem CatCrypt.Crypto.UCAlg.SimConstruction.id_comp {hon out leak₁ leak₂ view : Type} (Sim : SimConstruction { hon := hon, out := out, leak := leak₁, sim_if := leak₂, view := view }) : id.comp Sim = Sim

@[simp]

theorem CatCrypt.Crypto.UCAlg.SimConstruction.comp_id {hon out leak₁ leak₂ view : Type} (Sim : SimConstruction { hon := hon, out := out, leak := leak₁, sim_if := leak₂, view := view }) : Sim.comp id = Sim

theorem CatCrypt.Crypto.UCAlg.SimConstruction.comp_assoc {hon out leak₁ leak₂ leak₃ leak₄ view : Type} (Sim₁ : SimConstruction { hon := hon, out := out, leak := leak₁, sim_if := leak₂, view := view }) (Sim₂ : SimConstruction { hon := hon, out := out, leak := leak₂, sim_if := leak₃, view := view }) (Sim₃ : SimConstruction { hon := hon, out := out, leak := leak₃, sim_if := leak₄, view := view }) : (Sim₁.comp Sim₂).comp Sim₃ = Sim₁.comp (Sim₂.comp Sim₃)

Algebraic UC Emulation

def CatCrypt.Crypto.UCAlg.UCEmulatesAlg (ε : ENNReal) (spec : UCSpec) (π : spec.hon → Core.SPComp (spec.out ⊕ spec.leak)) (F : spec.hon → Core.SPComp (spec.out ⊕ spec.sim_if)) (Sim : SimConstruction spec) : Prop

UC emulation with explicit simulator construction.

Upgrades the existential ∀ A, ∃ S in UCEmulates to a concrete witness Sim : A ↦ S(A) satisfying the sdist bound uniformly.

Equations

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

Basic Properties

theorem CatCrypt.Crypto.UCAlg.UCEmulatesAlg.forget {ε : ENNReal} {spec : UCSpec} {π : spec.hon → Core.SPComp (spec.out ⊕ spec.leak)} {F : spec.hon → Core.SPComp (spec.out ⊕ spec.sim_if)} {Sim : SimConstruction spec} (h : UCEmulatesAlg ε spec π F Sim) : UCEmulates ε spec π F

Forget the algebraic witness: UCEmulatesAlg → UCEmulates.

theorem CatCrypt.Crypto.UCAlg.UCEmulatesAlg.mono {ε₁ ε₂ : ENNReal} {spec : UCSpec} {π : spec.hon → Core.SPComp (spec.out ⊕ spec.leak)} {F : spec.hon → Core.SPComp (spec.out ⊕ spec.sim_if)} {Sim : SimConstruction spec} (h : UCEmulatesAlg ε₁ spec π F Sim) (hle : ε₁ ≤ ε₂) : UCEmulatesAlg ε₂ spec π F Sim

Monotonicity: tighter bound implies looser bound (same simulator).

Same-Interface Constructions

theorem CatCrypt.Crypto.UCAlg.UCEmulatesAlg.refl {hon out leak view : Type} (π : hon → Core.SPComp (out ⊕ leak)) : UCEmulatesAlg 0 { hon := hon, out := out, leak := leak, sim_if := leak, view := view } π π SimConstruction.id

Reflexivity: any protocol emulates itself with Sim = id.

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

From sdist: same-interface with Sim = id.

Transitivity (Simulator Composition)

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

Same-interface transitivity via simulator composition. Errors compose additively: ε₁ + ε₂.

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

General transitivity through different interface types.

Chains π₁ ⟶^{Sim₁} π₂ ⟶^{Sim₂} π₃ via SimConstruction.comp.