Demonstration: one-time-pad perfect secrecy via prhl2

The canonical coupling-logic example. Over any finite abelian group G, the one-time pad encrypts a message m as m + k for a uniformly random key k:

enc m := do let k ← uniform; return (m + k)

Perfect secrecy: for any two messages m₀, m₁ the ciphertext distributions coincide. In the coupling logic this is one move — exhibit a coupling of the two key samplings under which the ciphertexts are equal. Couple k₀ (left) with k₁ = k₀ + (m₀ - m₁) (right): this is a translation (an Equiv), so it sends the uniform distribution to itself, and

m₁ + k₁ = m₁ + (k₀ + (m₀ - m₁)) = m₀ + k₀,

i.e. the two ciphertexts agree. The proof is rnd (the uniform rule with the shift bijection) to align the keys, then pure_pure to return.

noncomputable def GaudisCrypt.enc {G : Type} [Fintype G] [Nonempty G] [AddCommGroup G] (m : G) : ProgramDenotation Unit G

The one-time pad over a finite abelian group G.

Equations

• GaudisCrypt.enc m = do let k ← GaudisCrypt.ProgramDenotation.uniform pure (m + k)

theorem GaudisCrypt.otp_perfect_secrecy {G : Type} [Fintype G] [Nonempty G] [AddCommGroup G] (m₀ m₁ : G) : ProgramDenotation.prhl2 (fun (x x_1 : Unit) => True) (enc m₀) (enc m₁) fun (u v : G × Unit) => u.1 = v.1

One-time-pad perfect secrecy. The ciphertexts of any two messages are related by the diagonal (equal-output) coupling — so they have the same distribution.

theorem GaudisCrypt.otp_wp_eq {G : Type} [Fintype G] [Nonempty G] [AddCommGroup G] (m₀ m₁ : G) (F : G → ENNReal) : (enc m₀).wp (fun (u : G × Unit) => F u.1) () = (enc m₁).wp (fun (u : G × Unit) => F u.1) ()

Consequently the two encryptions are wp-indistinguishable: any ciphertext-only observable has equal expectation under enc m₀ and enc m₁. (Bridges the coupling to the probability level via to_relE.)

Demonstration 2: #heads = #tails over n fair coin flips

A longer "game". The state is a counter (ℕ). One loop counts heads, the other counts tails, both over n fair flips:

headBody := do let b ← coin; if b then incr else skip tailBody := do let b ← coin; if b then skip else incr

Their final-count distributions coincide. The coupling flips the coin oppositely on the two sides (b₂ = ¬b₁) — a bijection that preserves the fair coin — so each side increments on exactly the same physical outcome, keeping the two counters equal throughout. The proof chains loop_n, bind, uniform (the ¬ coupling), get, set, a case split, and pure_pure.

def GaudisCrypt.notEquiv : Bool ≃ Bool

The bit-flip bijection Bool ≃ Bool; it preserves the uniform (fair) coin, which is what licenses the opposite-coin coupling.

Equations

• GaudisCrypt.notEquiv = { toFun := not, invFun := not, left_inv := ⋯, right_inv := ⋯ }

noncomputable def GaudisCrypt.incr : ProgramDenotation ℕ Unit

Increment the counter (the whole state, via the identity lens).

Equations

• GaudisCrypt.incr = do let c ← GaudisCrypt.ProgramDenotation.get GaudisCrypt.Lens.id GaudisCrypt.ProgramDenotation.set GaudisCrypt.Lens.id (c + 1)

theorem GaudisCrypt.incr_rel : ProgramDenotation.prhl2 Eq incr incr fun (u v : Unit × ℕ) => u.2 = v.2

Two increments from equal counters end at equal counters.

noncomputable def GaudisCrypt.headBody : ProgramDenotation ℕ Unit

Count a head: increment iff the coin shows true.

Equations

• GaudisCrypt.headBody = do let b ← GaudisCrypt.ProgramDenotation.uniform if b = true then GaudisCrypt.incr else pure ()

noncomputable def GaudisCrypt.tailBody : ProgramDenotation ℕ Unit

Count a tail: increment iff the coin shows false.

Equations

• GaudisCrypt.tailBody = do let b ← GaudisCrypt.ProgramDenotation.uniform if b = true then pure () else GaudisCrypt.incr

theorem GaudisCrypt.body_rel : ProgramDenotation.prhl2 Eq headBody tailBody fun (u v : Unit × ℕ) => u.2 = v.2

One head-step and one tail-step, with the coin coupled oppositely, preserve equality of the counters.

theorem GaudisCrypt.count_heads_eq_count_tails (n : ℕ) : ProgramDenotation.prhl2 Eq (loop_n n headBody) (loop_n n tailBody) fun (u v : Unit × ℕ) => u.2 = v.2

#heads and #tails have the same distribution after n fair flips: the two counting loops are related by the equal-counter coupling.

Demonstration 3: a reduction step — the adversary frame rule

The workhorse of reductions: a state change outside the adversary's window is invisible to it. This is what licenses inserting bookkeeping, reprogramming a hidden oracle table, or sampling auxiliary randomness between game hops without disturbing the adversary's output.

Setup: an adversary winA.lift P acts only through its window winA. A reduction tweaks some external state winE (disjoint from winA, so winA.get (winE.set v σ) = winA.get σ). Then running the adversary, and running the tweak-then-adversary, produce the same output distribution.

The proof chains four rules: prefix_right (frame the external write off the right side), set_skip_right (relate that write against skip, using the disjointness), the new adversary call rule (the adversary from window-agreeing states returns equal results), and conseq.

theorem GaudisCrypt.external_tweak_invisible {a e s γ : Type} [Countable a] [Countable s] [Countable γ] (winA : Lens a s) (winE : Lens e s) (P : ProgramDenotation a γ) (v : e) (hdisj : ∀ (σ : s), winA.get (winE.set v σ) = winA.get σ) : ProgramDenotation.prhl2 (fun (σ₁ σ₂ : s) => winA.get σ₁ = winA.get σ₂) (winA.lift P) (do ProgramDenotation.set winE v winA.lift P) fun (u v : γ × s) => u.1 = v.1

Demonstration 4: collision resistance of double hashing

A genuine cryptographic reduction. For a pure hash H : α → α, if H is collision-resistant then so is H ∘ H. Given any adversary A producing a candidate collision (x, y), the reduction post-processes it:

rp (x, y) := if H x = H y then (x, y) else (H x, H y).

If (x, y) is an (H∘H)-collision then rp (x, y) is an H-collision — a pure case split. Hence Adv^{CR}_{H∘H}(A) ≤ Adv^{CR}_H(A ∘ rp): every (H∘H)-collision the adversary finds yields an H-collision, so if H is CR (right side small) then H∘H is CR (left side small).

The framework's role: refl runs A as a black box on both sides, pure_pure threads the pure reduction fact through the post-processing, and to_relE turns the coupling into the probability inequality.

@[reducible, inline]

abbrev GaudisCrypt.IsColl {α : Type} (f : α → α) (p : α × α) : Prop

p is an f-collision: two distinct points with the same f-image.

Equations

• GaudisCrypt.IsColl f p = (p.1 ≠ p.2 ∧ f p.1 = f p.2)

def GaudisCrypt.reducePair {α : Type} [DecidableEq α] (H : α → α) (p : α × α) : α × α

The reduction's post-processing of a candidate collision.

Equations

• GaudisCrypt.reducePair H p = if H p.1 = H p.2 then p else (H p.1, H p.2)

theorem GaudisCrypt.reducePair_isColl {α : Type} [DecidableEq α] (H : α → α) (p : α × α) (h : IsColl (fun (x : α) => H (H x)) p) : IsColl H (reducePair H p)

Pure core: an (H∘H)-collision is mapped to an H-collision.

theorem GaudisCrypt.double_hash_reduction {α s : Type} [DecidableEq α] [Countable α] [Countable s] (H : α → α) (A : ProgramDenotation s (α × α)) : ProgramDenotation.prhl2 Eq (A >>= pure) (do let p ← A pure (reducePair H p)) fun (u v : (α × α) × s) => IsColl (fun (x : α) => H (H x)) u.1 → IsColl H v.1

Reduction (relational): a win on the left (an (H∘H)-collision from A) forces a win on the right (an H-collision from the reduction).

theorem GaudisCrypt.double_hash_cr_bound {α s : Type} [DecidableEq α] [Countable α] [Countable s] (H : α → α) (A : ProgramDenotation s (α × α)) (σ : s) : A.wp (fun (pσ : (α × α) × s) => if IsColl (fun (x : α) => H (H x)) pσ.1 then 1 else 0) σ ≤ (do let p ← A pure (reducePair H p)).wp (fun (qσ : (α × α) × s) => if IsColl H qσ.1 then 1 else 0) σ

Concrete-security bound: the (H∘H)-CR advantage of A is at most the H-CR advantage of the reduction A ∘ rp. So H CR ⟹ H∘H CR.