EasyCrypt Semantic Bridge

This file bridges EasyCrypt-style reasoning (pRHL judgments, advantage bounds) and CatCrypt's UC security framework (sdist, UCEmulates).

Main results

Semantic Chain: pRHL → sdist → UC

• pRHL_to_UCEmulates — pRHL equality → UCEmulates at ε = 0
• sdist_to_UCEmulates — sdist bound → UCEmulates

Module Refinement

• ModuleRefines_comp_right — Post-composition preserves refinement
• ModuleRefines_to_UCEmulates — Module refinement → UCEmulates
• module_hybrid_bound — n-step hybrid argument

pRHL Vocabulary

@[reducible, inline]

abbrev CatCrypt.Crypto.EasyCryptBridge.pRHL {α : Type u_1} {β : Type u_2} (Φ : Relational.RPre) (c₁ : Core.SPComp α) (c₂ : Core.SPComp β) (Ψ : Relational.RPost α β) : Prop

EasyCrypt-style naming for the pRHL judgment.

Equations

• CatCrypt.Crypto.EasyCryptBridge.pRHL Φ c₁ c₂ Ψ = CatCrypt.Relational.rHoare Φ c₁ c₂ Ψ

Semantic Chain: pRHL → sdist → UC

theorem CatCrypt.Crypto.EasyCryptBridge.pRHL_eq_implies_advantage_zero {α : Type u_1} (G₀ G₁ : Core.SPComp α) (h : pRHL Relational.eqPre G₀ G₁ Relational.eqPost) (A : α → Core.SPComp Bool) : AdvantageA G₀ G₁ A = 0

pRHL with equality pre/postconditions implies zero advantage for all distinguishers.

theorem CatCrypt.Crypto.EasyCryptBridge.lifted_eqPost_eq' {β : Type u_1} : (fun (p₁ p₂ : β × Core.Heap) => Relational.eqPost p₁.1 p₁.2 p₂.1 p₂.2) = Eq

The lifted eqPost relation equals Eq (via Prod.ext).

theorem CatCrypt.Crypto.EasyCryptBridge.pRHL_eq_implies_prog_eq {hon : Type u_1} {β : Type u_2} (π F : hon → Core.SPComp β) (h : ∀ (a : hon), Relational.rHoare Relational.eqPre (π a) (F a) Relational.eqPost) : π = F

pRHL equality at all inputs gives pointwise program equality.

theorem CatCrypt.Crypto.EasyCryptBridge.pRHL_to_UCEmulates {hon : Type u_1} {out : Type u_2} {leak : Type u_3} {view : Type u_4} (π F : hon → Core.SPComp (out ⊕ leak)) (h : ∀ (a : hon), Relational.rHoare Relational.eqPre (π a) (F a) Relational.eqPost) : UCEmulates 0 { hon := hon, out := out, leak := leak, sim_if := leak, view := view } π F

pRHL equality → UCEmulates at ε = 0 (SPComp UC). A trivial same-interface lift (pRHL equality gives π = F, then UCEmulates_refl), so simulator = adversary. (composition plumbing)

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

sdist bound → UCEmulates, same interface, via UCEmulates_of_sdist. (composition plumbing)

theorem CatCrypt.Crypto.EasyCryptBridge.sdist_of_isPure_advantage {α : Type u_1} (f g : Unit → Core.SPComp α) (ε : ENNReal) (hf : (f ()).IsPure) (hg : (g ()).IsPure) (h : ∀ (A : α → Core.SPComp Bool), AdvantageA (f ()) (g ()) A ≤ ε) : sdist f g ≤ ε

IsPure computations with bounded advantage have bounded sdist.

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

sdist bound → UCEmulates, same interface, via UCEmulates_of_sdist. (composition plumbing)

Module Refinement

def CatCrypt.Crypto.EasyCryptBridge.ModuleRefines {α : Type u_1} {β : Type u_2} (ε : ENNReal) (M₁ M₂ : α → Core.SPComp β) : Prop

Two SPComp families (modules) are within sdist ε of each other.

Equations

• CatCrypt.Crypto.EasyCryptBridge.ModuleRefines ε M₁ M₂ = (CatCrypt.Crypto.sdist M₁ M₂ ≤ ε)

theorem CatCrypt.Crypto.EasyCryptBridge.ModuleRefines_refl {α : Type u_1} {β : Type u_2} (M : α → Core.SPComp β) : ModuleRefines 0 M M

theorem CatCrypt.Crypto.EasyCryptBridge.ModuleRefines_sym {α : Type u_1} {β : Type u_2} {M₁ M₂ : α → Core.SPComp β} {ε : ENNReal} (h : ModuleRefines ε M₁ M₂) : ModuleRefines ε M₂ M₁

theorem CatCrypt.Crypto.EasyCryptBridge.ModuleRefines_trans {α : Type u_1} {β : Type u_2} {M₁ M₂ M₃ : α → Core.SPComp β} {ε₁ ε₂ : ENNReal} (h₁ : ModuleRefines ε₁ M₁ M₂) (h₂ : ModuleRefines ε₂ M₂ M₃) : ModuleRefines (ε₁ + ε₂) M₁ M₃

theorem CatCrypt.Crypto.EasyCryptBridge.ModuleRefines_mono {α : Type u_1} {β : Type u_2} {M₁ M₂ : α → Core.SPComp β} {ε₁ ε₂ : ENNReal} (h : ModuleRefines ε₁ M₁ M₂) (hle : ε₁ ≤ ε₂) : ModuleRefines ε₂ M₁ M₂

theorem CatCrypt.Crypto.EasyCryptBridge.ModuleRefines_comp_right {α : Type u_1} {β : Type u_2} {γ : Type u_3} {M₁ M₂ : α → Core.SPComp β} {ε : ENNReal} (h : ModuleRefines ε M₁ M₂) (k : β → Core.SPComp γ) : ModuleRefines ε (fun (a : α) => (M₁ a).bind k) fun (a : α) => (M₂ a).bind k

Post-composition preserves module refinement (right PPL).

theorem CatCrypt.Crypto.EasyCryptBridge.ModuleRefines_comp_left {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → Core.SPComp β) {g₁ g₂ : β → Core.SPComp γ} {ε : ENNReal} (h : ModuleRefines ε g₁ g₂) : ModuleRefines ε (fun (a : α) => (f a).bind g₁) fun (a : α) => (f a).bind g₂

Pre-composition with shared prefix preserves refinement (left PPL).

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

Module refinement (an sdist bound) → UCEmulates, same interface, via UCEmulates_of_sdist. (composition plumbing)

theorem CatCrypt.Crypto.EasyCryptBridge.ModuleRefines_chain {hon : Type u_1} {out : Type u_2} {leak : Type u_3} {view : Type u_4} {π G F : hon → Core.SPComp (out ⊕ leak)} {ε₁ ε₂ : ENNReal} (h₁ : ModuleRefines ε₁ π G) (h₂ : ModuleRefines ε₂ G F) : UCEmulates (ε₁ + ε₂) { hon := hon, out := out, leak := leak, sim_if := leak, view := view } π F

Compose two module-refinement (sdist) steps into a UCEmulates bound, same interface. (composition plumbing)

Pointwise Equality Bridge

theorem CatCrypt.Crypto.EasyCryptBridge.sdist_zero_of_eq {α : Type u_1} {β : Type u_2} (f g : α → Core.SPComp β) (h : ∀ (a : α), f a = g a) : sdist f g = 0

If two computations are pointwise equal, their sdist is 0.

theorem CatCrypt.Crypto.EasyCryptBridge.pRHL_to_ModuleRefines {hon : Type u_1} {β : Type u_2} (π F : hon → Core.SPComp β) (h : ∀ (a : hon), Relational.rHoare Relational.eqPre (π a) (F a) Relational.eqPost) : ModuleRefines 0 π F

pRHL at all inputs → ModuleRefines at 0.

Hybrid Argument Support

theorem CatCrypt.Crypto.EasyCryptBridge.module_hybrid_bound {α : Type u_1} {β : Type u_2} (n : ℕ) (games : Fin (n + 1) → α → Core.SPComp β) (ε : ENNReal) (h_step : ∀ (i : Fin n), ModuleRefines ε (games i.castSucc) (games i.succ)) : ModuleRefines (↑n * ε) (games 0) (games (Fin.last n))

n-step hybrid argument at the module level: if each adjacent pair is within ε, the endpoints are within n * ε.