Bridge: Connecting Unary Logic to Relational Logic and Probability

This file bridges the unary probabilistic Hoare logic (pHL) with the relational probabilistic Hoare logic (pRHL) and the advantage/probability framework.

Main results

pHL ↔ pRHL connections

• pHoare_of_rHoare_diag - Extract unary facts from a relational judgment on the diagonal
• rHoare_of_pHoare_l - Embed a unary judgment on the left side of a relational judgment

pHL → Probability bounds

• prTrue_eq_one_of_pHoare - If all Boolean outcomes are true and the computation is lossless, then Pr[true] = 1 ("byphoare" direction from EasyCrypt)
• prTrue_eq_zero_of_pHoare - If all Boolean outcomes are false, then Pr[true] = 0
• advantage_zero_of_same_result - Advantage is 0 when both games deterministically return the same Boolean

Failure Event Lemma (FEL)

• failure_event_lemma - The fundamental up-to-bad reasoning technique: |Pr[G₀:A] - Pr[G₁:A]| ≤ Pr[G₀:bad] when G₀ and G₁ agree on non-bad outcomes

References

• EasyCrypt: byphoare, phoare, and fel tactics
• SSProve (Rocq): rhl_semantics, advantage framework
• Barthe et al., "CertiCrypt: Computer-Verified, Implementation-Level Code-Based Cryptographic Proofs" (failure event lemma)

Connecting pHL to pRHL

theorem CatCrypt.Unary.pHoare_of_rHoare_diag {α : Type u_1} {P : UPre} {c : Core.SPComp α} {Q : UPost α} (h : Relational.rHoare (fun (h₁ h₂ : Core.Heap) => h₁ = h₂ ∧ P h₁) c c fun (a₁ : α) (h₁ : Core.Heap) (a₂ : α) (h₂ : Core.Heap) => a₁ = a₂ ∧ h₁ = h₂ ∧ Q a₁ h₁) : pHoare P c Q

From pRHL with same program to unary pHL.

If a relational judgment rHoare establishes properties for (c, c) on the diagonal (i.e., starting from equal heaps), we can extract a unary pHL judgment.

The precondition P on the single heap becomes h₁ = h₂ ∧ P h₁ in the relational setting, and the relational postcondition a₁ = a₂ ∧ h₁ = h₂ ∧ Q a₁ h₁ yields the unary postcondition Q.

theorem CatCrypt.Unary.rHoare_of_pHoare_l {α : Type u_1} {β : Type u_2} {P : UPre} {Q : UPost α} {R : Relational.RPre} {c₁ : Core.SPComp α} {c₂ : Core.SPComp β} {Ψ : Relational.RPost α β} (hph : pHoare P c₁ Q) (hrel : Relational.rHoare R c₁ c₂ Ψ) (hcombine : ∀ (a₁ : α) (h₁ : Core.Heap) (a₂ : β) (h₂ : Core.Heap), Q a₁ h₁ → Ψ a₁ h₁ a₂ h₂ → Ψ a₁ h₁ a₂ h₂) : Relational.rHoare (fun (h₁ h₂ : Core.Heap) => P h₁ ∧ R h₁ h₂) c₁ c₂ Ψ

From unary to relational: embed pHL judgment on left side.

If c₁ satisfies Q unarily (via pHL) and we also have a relational judgment for c₁ ~ c₂, we can combine the preconditions. The key observation is that the relational coupling already provides all needed information; the unary judgment serves as additional documentation that Q holds on the left.

theorem CatCrypt.Unary.rHoare_of_pHoare_r {α : Type u_1} {β : Type u_2} {P : UPre} {Q : UPost β} {R : Relational.RPre} {c₁ : Core.SPComp α} {c₂ : Core.SPComp β} {Ψ : Relational.RPost α β} (hph : pHoare P c₂ Q) (hrel : Relational.rHoare R c₁ c₂ Ψ) : Relational.rHoare (fun (h₁ h₂ : Core.Heap) => R h₁ h₂ ∧ P h₂) c₁ c₂ Ψ

Symmetric variant: embed pHL judgment on right side.

Connecting pHL to probability bounds

theorem CatCrypt.Unary.prTrue_eq_one_of_pHoare (G : Core.SPComp Bool) (h₀ : Core.Heap) (hph : pHoare (fun (h : Core.Heap) => h = h₀) G fun (b : Bool) (x : Core.Heap) => b = true) (hll : isLosslessIf (fun (h : Core.Heap) => h = h₀) G) : Crypto.prTrue G h₀ = 1

Key bridge lemma: if pHoare says all Boolean outcomes are true, and the computation is lossless, then Pr[true] = 1.

This is the "byphoare" direction from EasyCrypt: use a unary Hoare-logic proof to establish a probability fact.

Proof idea: Since the computation is lossless, the total mass is 1. The pHoare judgment ensures every outcome in the support has b = true. Therefore, all mass is concentrated on (true, _) outcomes, and prTrue G h₀ = ∑' h, G h₀ (some (true, h)) = 1.

theorem CatCrypt.Unary.prTrue_eq_zero_of_pHoare (G : Core.SPComp Bool) (h₀ : Core.Heap) (hph : pHoare (fun (h : Core.Heap) => h = h₀) G fun (b : Bool) (x : Core.Heap) => b = false) : Crypto.prTrue G h₀ = 0

If pHoare says all Boolean outcomes are false, then Pr[true] = 0.

Every term G h₀ (some (true, h)) in the sum defining prTrue must be 0: if it were nonzero, pHoare would give true = false, a contradiction.

theorem CatCrypt.Unary.advantage_zero_of_both_false (G₀ G₁ : Core.SPComp Bool) (h₀ : pHoare (fun (h : Core.Heap) => h = Core.Heap.empty) G₀ fun (b : Bool) (x : Core.Heap) => b = false) (h₁ : pHoare (fun (h : Core.Heap) => h = Core.Heap.empty) G₁ fun (b : Bool) (x : Core.Heap) => b = false) : Crypto.Advantage G₀ G₁ = 0

Variant of advantage_zero_of_same_result for the false case, which does not require losslessness.

theorem CatCrypt.Unary.advantage_zero_of_same_result (G₀ G₁ : Core.SPComp Bool) (b : Bool) (h₀ : pHoare (fun (h : Core.Heap) => h = Core.Heap.empty) G₀ fun (b' : Bool) (x : Core.Heap) => b' = b) (h₁ : pHoare (fun (h : Core.Heap) => h = Core.Heap.empty) G₁ fun (b' : Bool) (x : Core.Heap) => b' = b) (hll₀ : isLosslessIf (fun (h : Core.Heap) => h = Core.Heap.empty) G₀) (hll₁ : isLosslessIf (fun (h : Core.Heap) => h = Core.Heap.empty) G₁) : Crypto.Advantage G₀ G₁ = 0

Advantage is 0 when both games deterministically return the same Boolean result.

If both G₀ and G₁ always return b (from the empty heap), their prTrue values are equal (both 1 if b = true, both 0 if b = false), so the advantage is 0.

prTrue and prEvent connection

theorem CatCrypt.Unary.prTrue_eq_prEventComp (G : Core.SPComp Bool) (h₀ : Core.Heap) : Crypto.prTrue G h₀ = prEventComp G h₀ fun (b : Bool) (x : Core.Heap) => b = true

prTrue is a special case of prEventComp for the event b = true.

Failure Event Lemma (FEL)

theorem CatCrypt.Unary.failure_event_lemma (G₀ G₁ : Core.SPComp Bool) (h₀ : Core.Heap) (bad : Core.Heap → Prop) (h_agree : ∀ (b : Bool) (h' : Core.Heap), ¬bad h' → (G₀ h₀) (some (b, h')) = (G₁ h₀) (some (b, h'))) (hll₀ : isLosslessIf (fun (h : Core.Heap) => h = h₀) G₀) : max (Crypto.prTrue G₀ h₀ - Crypto.prTrue G₁ h₀) (Crypto.prTrue G₁ h₀ - Crypto.prTrue G₀ h₀) ≤ prEventComp G₀ h₀ fun (x : Bool) (h' : Core.Heap) => bad h'

The Failure Event Lemma (up-to-bad reasoning).

This is a fundamental technique from EasyCrypt and CertiCrypt used in game-hopping proofs. Informally:

|Pr[G₀ : A] - Pr[G₁ : A]| ≤ Pr[G₀ : bad]

when G₀ and G₁ agree on all outcomes where bad does not occur.

Formal statement: Given two games G₀ and G₁ and a "bad event" predicate on the final heap:

• h_agree: For any non-bad initial heap, whenever G₀ assigns nonzero probability to an outcome, G₁ also does (the games have the same support on non-bad heaps).

Then the advantage is bounded by the probability that G₀ sets the bad flag.

Use cases:

• PKEY switching lemmas (bad = collision in random oracle)
• PRF/PRP switching (bad = duplicate query)
• Lazy/eager sampling equivalence (bad = premature evaluation)

Proof sketch:

1. Split prTrue into bad + nonbad parts for both G₀ and G₁
2. The nonbad parts are equal by h_agree
3. Show bad mass of G₁ ≤ bad mass of G₀ (using losslessness)
4. Derive two one-sided bounds: prTrue G₀ ≤ prTrue G₁ + Pr[bad] and vice versa
5. Combine via tsub_le_iff_right and max_le

theorem CatCrypt.Unary.perfect_indist_of_no_bad (G₀ G₁ : Core.SPComp Bool) (h₀ : Core.Heap) (h_agree : ∀ (b : Bool) (h' : Core.Heap), (G₀ h₀) (some (b, h')) = (G₁ h₀) (some (b, h'))) : Crypto.prTrue G₀ h₀ = Crypto.prTrue G₁ h₀

Corollary: If the bad event never happens, the games are perfectly indistinguishable.

Connecting pHL postconditions to advantage bounds

theorem CatCrypt.Unary.advantage_zero_of_pHoare_det (G₀ G₁ : Core.SPComp Bool) (b : Bool) (hph₀ : pHoare (fun (h : Core.Heap) => h = Core.Heap.empty) G₀ fun (b' : Bool) (x : Core.Heap) => b' = b) (hph₁ : pHoare (fun (h : Core.Heap) => h = Core.Heap.empty) G₁ fun (b' : Bool) (x : Core.Heap) => b' = b) (hll₀ : isLosslessIf (fun (h : Core.Heap) => h = Core.Heap.empty) G₀) (hll₁ : isLosslessIf (fun (h : Core.Heap) => h = Core.Heap.empty) G₁) : Crypto.Advantage G₀ G₁ = 0

If two games satisfy the same pHL postcondition that determines the Boolean result, and both are lossless, then their advantage is 0.

This is a unary analogue of advantage_zero_of_rHoare: instead of showing equality via a relational coupling, we show that both games produce outcomes satisfying the same postcondition Q, which determines the Boolean.