Robust Compilation (RC), RHP, and the UC = RC Equivalence

This file defines three notions of security preservation and establishes their relationships at Level 1 (information-theoretic, no complexity bounds).

Three notions of robust compilation

1. RobustCompilation (our notion, no simulator): ∀ ρ D, sdist(D∘ρ∘π, D∘ρ∘F) ≤ ε Equivalent to sdist ≤ ε and ContextEquiv ε.

2. RHP (paper's notion, with simulator): ∀A ∃S, RobustCompilation ε (bind π (mapSum pure A)) (bind F (mapSum pure S)) Equivalent to UCEmulates ε. Reference: Patrignani, Wahby et al., "UC is RC", TOPLAS 2024.

3. UCEmulates (Canetti-style): ∀A ∃S, sdist(bind π (mapSum pure A), bind F (mapSum pure S)) ≤ ε

Relationship diagram

  sdist ≤ ε  ↔  ContextEquiv ε  ↔  RobustCompilation ε  (no simulator)
      ↓ (one direction only: take S = A)
  UCEmulates ε  ↔  RHP ε  (with ∃ simulator)

The downward arrow is strict: UC/RHP is strictly weaker than sdist/RC. Counterexample: π = pure(.inr true), F = pure(.inr false), S = fun b => pure (not b) gives UC with ε = 0 but sdist π F > 0.

Main definitions

• compile — substitute a subroutine implementation into a protocol
• ContextEquiv — contextual equivalence (all distinguishers bounded)
• RobustCompilation — RC without simulator: all contexts bounded
• RHP — RC with simulator: paper's "Robust Hyperproperties Preservation"

Main results

• contextEquiv_iff_sdist — ContextEquiv ε ↔ sdist ≤ ε
• RC_iff_sdist — RobustCompilation ε ↔ sdist ≤ ε
• UCEmulates_iff_RHP — UCEmulates ε ↔ RHP ε (the paper's main theorem)
• sdist_implies_UCEmulates — sdist ≤ ε → UCEmulates ε (one direction)
• RC_implies_UCEmulates — RC → UC (same-interface)
• sdist_mapSum_le — coproduct tensor: max(ε₁, ε₂) bound

Sub-SMC structure

Our RobustCompilation (equivalently, sdist) forms a wide sub-SMC of Kl(SPComp) via sdist_comp_add (composition) and sdist_mapSum_le (tensor).

UC/RHP inherits this structure in the same-interface case (leak = sim_if) via UCEmulates_trans (simulator chaining) and UCEmulates_of_sdist. For the general case (different interfaces), the categorical structure is richer and involves simulator composition — a 2-categorical notion.

Compile

noncomputable def CatCrypt.Crypto.compile {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (ρ : α → Core.SPComp (β ⊕ γ)) (impl : γ → Core.SPComp δ) : α → Core.SPComp (β ⊕ δ)

Substitute subroutine impl into protocol ρ: compile ρ impl = (id ⊕ impl) ∘ₖ ρ.

Equations

• CatCrypt.Crypto.compile ρ impl a = (ρ a).bind (CatCrypt.Crypto.mapSum CatCrypt.Core.SPComp.pure impl)

Contextual Equivalence

def CatCrypt.Crypto.ContextEquiv {α : Type u_1} {β : Type u_2} (ε : ENNReal) (f g : α → Core.SPComp β) : Prop

Two morphisms are ε-contextually equivalent if no closing context (distinguisher D : β → SPComp Bool) can distinguish them by more than ε.

Equations

• CatCrypt.Crypto.ContextEquiv ε f g = ∀ (D : β → CatCrypt.Core.SPComp Bool), (CatCrypt.Crypto.sdist (fun (a : α) => (f a).bind D) fun (a : α) => (g a).bind D) ≤ ε

theorem CatCrypt.Crypto.contextEquiv_of_sdist {α : Type u_1} {β : Type u_2} {f g : α → Core.SPComp β} {ε : ENNReal} (h : sdist f g ≤ ε) : ContextEquiv ε f g

sdist ≤ ε → ContextEquiv ε via right PPL.

theorem CatCrypt.Crypto.sdist_of_contextEquiv {α : Type u_1} {β : Type u_2} {f g : α → Core.SPComp β} {ε : ENNReal} (h : ContextEquiv ε f g) : sdist f g ≤ ε

ContextEquiv ε → sdist ≤ ε: the identity distinguisher witnesses the bound.

For any f g : α → SPComp β, sdist f g = sup_D sdist (D ∘ f) (D ∘ g). When β = Bool, D = pure gives sdist (pure ∘ f) (pure ∘ g) = sdist f g (by bind_pure). For general β, the sdist already takes the sup over D.

theorem CatCrypt.Crypto.contextEquiv_iff_sdist {α : Type u_1} {β : Type u_2} (f g : α → Core.SPComp β) (ε : ENNReal) : ContextEquiv ε f g ↔ sdist f g ≤ ε

Contextual equivalence iff bounded sdist.

Robust Compilation

def CatCrypt.Crypto.RobustCompilation {I O : Type} (ε : ENNReal) (π F : I → Core.SPComp O) : Prop

Robust Compilation: replacing subroutine F with π preserves security in ALL contexts ρ and for ALL distinguishers.

Equations

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

theorem CatCrypt.Crypto.RC_of_sdist {I O : Type} {π F : I → Core.SPComp O} {ε : ENNReal} (h : sdist π F ≤ ε) : RobustCompilation ε π F

sdist ≤ ε → RC: both PPLs give the bound.

theorem CatCrypt.Crypto.sdist_of_RC {I O : Type} {π F : I → Core.SPComp O} {ε : ENNReal} (h : RobustCompilation ε π F) : sdist π F ≤ ε

RC → sdist ≤ ε: specialize to ρ = pure (identity context).

theorem CatCrypt.Crypto.RC_iff_sdist {I O : Type} (π F : I → Core.SPComp O) (ε : ENNReal) : RobustCompilation ε π F ↔ sdist π F ≤ ε

RC ↔ sdist ≤ ε.

UC from sdist (Same Interface)

theorem CatCrypt.Crypto.sdist_implies_UCEmulates {hon : Type u_1} {out : Type u_2} {leak : Type u_3} {view : Type u_4} (ε : ENNReal) (π F : hon → Core.SPComp (out ⊕ leak)) (h : sdist π F ≤ ε) : UCEmulates ε { hon := hon, out := out, leak := leak, sim_if := leak, view := view } π F

sdist → UC (same-interface): the simulator is the adversary.

When sdist π F ≤ ε, UC emulation holds with S = A for any adversary A. The reverse implication is FALSE: UC emulation allows the simulator to transform F's leak channel, so ∃ S, sdist π (bind F (mapSum pure S)) ≤ ε does not imply sdist π F ≤ ε.

theorem CatCrypt.Crypto.RC_implies_UCEmulates {hon out leak view : Type} (ε : ENNReal) (π F : hon → Core.SPComp (out ⊕ leak)) (h : RobustCompilation ε π F) : UCEmulates ε { hon := hon, out := out, leak := leak, sim_if := leak, view := view } π F

RC → UC (same-interface): since RC ↔ sdist, RC also implies UC.

Robust Hyperproperties Preservation (RHP)

The paper "Universal Composability is Robust Compilation" (Patrignani, Wahby et al., 2024) defines a different notion of Robust Compilation that includes an existential simulator. We call this RHP (Robust Hyperproperties Preservation) to distinguish it from our simulator-free RobustCompilation.

The key difference:

• Our RobustCompilation: ∀ ρ D, dist(D∘ρ∘π, D∘ρ∘F) ≤ ε (no simulator)
• Paper's RHP: ∀A ∃S, ∀ ρ D, dist(D∘ρ∘(id⊕A)∘π, D∘ρ∘(id⊕S)∘F) ≤ ε

Since RobustCompilation ↔ sdist (our RC_iff_sdist), RHP reduces to: ∀A ∃S, sdist(bind π (mapSum pure A), bind F (mapSum pure S)) ≤ ε, which is exactly UCEmulates. Hence UC ↔ RHP at Level 1.

The relationship diagram:

  sdist ≤ ε  ↔  ContextEquiv ε  ↔  RobustCompilation ε  (no simulator)
      ↓ (one direction only: take S = A)
  UCEmulates ε  ↔  RHP ε  (with ∃ simulator)

def CatCrypt.Crypto.RHP (ε : ENNReal) (hon out leak sim_if view : Type) (π : hon → Core.SPComp (out ⊕ leak)) (F : hon → Core.SPComp (out ⊕ sim_if)) : Prop

Robust Hyperproperties Preservation: the paper's notion of Robust Compilation.

Unlike our RobustCompilation (which has no simulator), RHP includes an existential simulator (∀A ∃S), matching the quantifier structure of UC.

RHP says: for all adversaries A, there exists a simulator S such that the post-adversary views are robustly equivalent in ALL contexts.

Reference: Patrignani, Wahby et al., "Universal Composability is Robust Compilation", TOPLAS 2024.

Equations

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

theorem CatCrypt.Crypto.RHP_of_UCEmulates {hon out leak sim_if view : Type} {ε : ENNReal} {π : hon → Core.SPComp (out ⊕ leak)} {F : hon → Core.SPComp (out ⊕ sim_if)} (h : UCEmulates ε { hon := hon, out := out, leak := leak, sim_if := sim_if, view := view } π F) : RHP ε hon out leak sim_if view π F

UC → RHP: UC gives sdist ≤ ε, then RC_of_sdist lifts to all contexts.

theorem CatCrypt.Crypto.UCEmulates_of_RHP {hon out leak sim_if view : Type} {ε : ENNReal} {π : hon → Core.SPComp (out ⊕ leak)} {F : hon → Core.SPComp (out ⊕ sim_if)} (h : RHP ε hon out leak sim_if view π F) : UCEmulates ε { hon := hon, out := out, leak := leak, sim_if := sim_if, view := view } π F

RHP → UC: specializing the RHP contexts recovers sdist ≤ ε.

theorem CatCrypt.Crypto.UCEmulates_iff_RHP {hon out leak sim_if view : Type} (π : hon → Core.SPComp (out ⊕ leak)) (F : hon → Core.SPComp (out ⊕ sim_if)) (ε : ENNReal) : UCEmulates ε { hon := hon, out := out, leak := leak, sim_if := sim_if, view := view } π F ↔ RHP ε hon out leak sim_if view π F

UC ↔ RHP at Level 1 (information-theoretic).

This is the main theorem of Patrignani, Wahby et al. (2024): "Universal Composability is Robust Compilation".

At Level 1 (no complexity bounds), the equivalence is immediate because RobustCompilation ↔ sdist (our RC_iff_sdist), so the ∀-context quantification in RHP adds no strength beyond sdist.

At computational levels (Level 2/3), RHP quantifies over poly-time contexts while sdist takes a sup over ALL distinguishers. The equivalence then requires the dummy adversary theorem and becomes non-trivial.

Tensor Distance Bounds

theorem CatCrypt.Crypto.sdist_mapSum_le {α₁ : Type u_1} {α₂ : Type u_2} {β₁ : Type u_3} {β₂ : Type u_4} (f₁ f₂ : α₁ → Core.SPComp α₂) (g₁ g₂ : β₁ → Core.SPComp β₂) {ε₁ ε₂ : ENNReal} (hf : sdist f₁ f₂ ≤ ε₁) (hg : sdist g₁ g₂ ≤ ε₂) : sdist (mapSum f₁ g₁) (mapSum f₂ g₂) ≤ max ε₁ ε₂

For coproduct tensor: distance is max, not sum, since only one branch runs.

Sequential and Parallel Composition of RC

theorem CatCrypt.Crypto.RobustCompilation_trans {I O : Type} {π₁ π₂ π₃ : I → Core.SPComp O} {ε₁ ε₂ : ENNReal} (h₁ : RobustCompilation ε₁ π₁ π₂) (h₂ : RobustCompilation ε₂ π₂ π₃) : RobustCompilation (ε₁ + ε₂) π₁ π₃

Sequential composition (transitivity) of robust compilation.

If π₁ ≈_{ε₁} π₂ and π₂ ≈_{ε₂} π₃, then π₁ ≈_{ε₁+ε₂} π₃. Proof: RC ↔ sdist + triangle inequality.

theorem CatCrypt.Crypto.RobustCompilation_mapSum {α₁ β₁ α₂ β₂ : Type} {ε₁ ε₂ : ENNReal} {π₁ F₁ : α₁ → Core.SPComp β₁} {π₂ F₂ : α₂ → Core.SPComp β₂} (h₁ : RobustCompilation ε₁ π₁ F₁) (h₂ : RobustCompilation ε₂ π₂ F₂) : RobustCompilation (max ε₁ ε₂) (mapSum π₁ π₂) (mapSum F₁ F₂)

Parallel composition of robust compilation via coproduct tensor.

The max bound (not sum!) reflects the coproduct structure: each input activates exactly one sub-protocol, so the distances don't accumulate.

Parallel UC Composition

theorem CatCrypt.Crypto.UCEmulates_mapSum_of_sdist {α₁ : Type u_1} {β₁ : Type u_2} {α₂ : Type u_3} {β₂ : Type u_4} {V : Type u_5} {ε₁ ε₂ : ENNReal} (π₁ F₁ : α₁ → Core.SPComp β₁) (π₂ F₂ : α₂ → Core.SPComp β₂) (h₁ : sdist π₁ F₁ ≤ ε₁) (h₂ : sdist π₂ F₂ ≤ ε₂) : UCEmulates (max ε₁ ε₂) { hon := α₁ ⊕ α₂, out := Unit, leak := β₁ ⊕ β₂, sim_if := β₁ ⊕ β₂, view := V } (fun (x : { hon := α₁ ⊕ α₂, out := Unit, leak := β₁ ⊕ β₂, sim_if := β₁ ⊕ β₂, view := V }.hon) => (mapSum π₁ π₂ x).bind fun (o : β₁ ⊕ β₂) => Core.SPComp.pure (Sum.inr o)) fun (x : { hon := α₁ ⊕ α₂, out := Unit, leak := β₁ ⊕ β₂, sim_if := β₁ ⊕ β₂, view := V }.hon) => (mapSum F₁ F₂ x).bind fun (o : β₁ ⊕ β₂) => Core.SPComp.pure (Sum.inr o)

Parallel composition of UC-secure protocols (same-interface case).

Given sdist bounds for two protocols, the parallel composition mapSum π₁ π₂ UC-emulates mapSum F₁ F₂ with error max(ε₁, ε₂).

The max bound (not sum!) reflects the coproduct structure: each input activates exactly one sub-protocol, so the distances don't accumulate.

The UC spec treats the combined output β₁ ⊕ β₂ as the leak interface (same-interface: leak = sim_if), with Unit as the honest output.

Practical use: Multi-instance security (n copies of a protocol), or independent sub-protocols running on disjoint message types.