Statistical Distance on Kleisli Morphisms

This file defines statistical distance (sdist) between Kleisli morphisms of SPComp, based on a distinguisher-supremum formulation. This avoids needing TV distance on SDistr and directly reuses the existing prTrue infrastructure.

Main definitions

• absDiff — unsigned difference in ℝ≥0∞
• sdist — statistical distance between Kleisli morphisms

Main results

• sdist_self, sdist_sym, sdist_triangle — pseudometric properties
• sdist_comp_right — right post-processing lemma (PPL, post-composition)
• sdist_comp_left — left post-processing lemma (PPL, pre-composition)
• sdist_wkR_le, sdist_wkL_le — tensor doesn't increase distance
• sdist_comp_add — composition of ε-close morphisms

Sub-SMC structure

The composition bound sdist_comp_add and the tensor bound sdist_mapSum_le (in RC.lean) together establish that sdist-bounded pairs form a wide sub-SMC of Kl(SPComp):

• Objects: all types (same as Kl(SPComp))
• Morphisms from α to β: pairs (f, g) with sdist f g ≤ ε
• Composition: sdist_comp_add — (ε₁, ε₂) compose to ε₁ + ε₂
• Tensor: sdist_mapSum_le — (ε₁, ε₂) tensor to max(ε₁, ε₂)
• Identity: sdist_self — (id, id) has distance 0

This sub-SMC is the semantic foundation for game-hopping proofs: each hop replaces one morphism with an ε-close one, and the total distance is bounded by the sum of hops.

Design: distinguisher-supremum formulation

We define sdist via ⨆ D a h₀, absDiff(prTrue(bind(f a) D, h₀), prTrue(bind(g a) D, h₀)) rather than via TV distance on SDistr. This makes the right PPL trivial (compose D with g to get a new distinguisher) and matches the game-hopping methodology directly. The left PPL requires a convexity/weighted-average argument (absDiff_prTrue_bind_le).

Absolute Difference

noncomputable def CatCrypt.Crypto.absDiff (a b : ENNReal) : ENNReal

Unsigned difference in ℝ≥0∞: absDiff a b = max(a - b, b - a).

Equations

• CatCrypt.Crypto.absDiff a b = max (a - b) (b - a)

@[simp]

theorem CatCrypt.Crypto.absDiff_self (a : ENNReal) : absDiff a a = 0

@[simp]

theorem CatCrypt.Crypto.absDiff_comm (a b : ENNReal) : absDiff a b = absDiff b a

theorem CatCrypt.Crypto.absDiff_triangle (a b c : ENNReal) : absDiff a c ≤ absDiff a b + absDiff b c

Statistical Distance

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

Statistical distance between Kleisli morphisms, defined as the supremum over all distinguishers, inputs, and initial heaps of the absolute difference in probability of returning true.

Equations

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

Pseudometric Properties

@[simp]

theorem CatCrypt.Crypto.sdist_self {α : Type u_1} {β : Type u_2} (f : α → Core.SPComp β) : sdist f f = 0

theorem CatCrypt.Crypto.sdist_sym {α : Type u_1} {β : Type u_2} (f g : α → Core.SPComp β) : sdist f g = sdist g f

theorem CatCrypt.Crypto.sdist_triangle {α : Type u_1} {β : Type u_2} (f g h : α → Core.SPComp β) : sdist f h ≤ sdist f g + sdist g h

Post-Processing Lemmas

theorem CatCrypt.Crypto.sdist_precomp_le {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f g : β → Core.SPComp γ) (h : α → β) : sdist (f ∘ h) (g ∘ h) ≤ sdist f g

Pre-composition with a pure function doesn't increase sdist. The sup over h(a) for a : α is ≤ the sup over all b : β.

theorem CatCrypt.Crypto.sdist_comp_right {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f₁ f₂ : α → Core.SPComp β) (g : β → Core.SPComp γ) : (sdist (fun (a : α) => (f₁ a).bind g) fun (a : α) => (f₂ a).bind g) ≤ sdist f₁ f₂

Right PPL: post-composition doesn't increase distance. This is immediate because D ∘ g is just another distinguisher.

theorem CatCrypt.Crypto.le_add_of_absDiff_le {a b ε : ENNReal} (h : absDiff a b ≤ ε) : a ≤ b + ε

Auxiliary: absDiff a b ≤ ε implies a ≤ b + ε.

theorem CatCrypt.Crypto.weighted_bound {ι : Type u_1} (w f g : ι → ENNReal) (ε : ENNReal) (hfg : ∀ (i : ι), f i ≤ g i + ε) (hw : ∑' (i : ι), w i ≤ 1) : ∑' (i : ι), w i * f i ≤ ∑' (i : ι), w i * g i + ε

Auxiliary: weighted average bound for ENNReal. If ∀ i, f i ≤ g i + ε and ∑ w i ≤ 1, then ∑ w i * f i ≤ ∑ w i * g i + ε.

theorem CatCrypt.Crypto.prTrue_bind_eq_weighted {α : Type u_1} (c : Core.SPComp α) (k : α → Core.SPComp Bool) (h₀ : Core.Heap) : prTrue (c.bind k) h₀ = ∑' (p : Option (α × Core.Heap)), (c h₀) p * match p with | some (a, h') => prTrue (k a) h' | none => 0

Representation: prTrue(bind c k, h₀) = ∑' p, (c h₀)(p) * val(p). This lemma factors out the weighted-sum structure of prTrue(bind ...).

theorem CatCrypt.Crypto.absDiff_prTrue_bind_le {α : Type u_1} (c : Core.SPComp α) (k₁ k₂ : α → Core.SPComp Bool) (h₀ : Core.Heap) (ε : ENNReal) (hk : ∀ (a : α) (h' : Core.Heap), prTrue (k₁ a) h' ≤ prTrue (k₂ a) h' + ε) (hk' : ∀ (a : α) (h' : Core.Heap), prTrue (k₂ a) h' ≤ prTrue (k₁ a) h' + ε) : absDiff (prTrue (c.bind k₁) h₀) (prTrue (c.bind k₂) h₀) ≤ ε

Helper for left PPL: weighted average of ε-close values is ε-close. Uses prTrue_bind_eq_weighted to reduce to a weighted-sum inequality.

theorem CatCrypt.Crypto.absDiff_bind_common {X : Type} (c : Core.SPComp X) (k₁ k₂ : X → Core.SPComp Bool) (h₀ : Core.Heap) (ε : ENNReal) (hk : ∀ (x : X) (h' : Core.Heap), absDiff (prTrue (k₁ x) h') (prTrue (k₂ x) h') ≤ ε) : absDiff (prTrue (c.bind k₁) h₀) (prTrue (c.bind k₂) h₀) ≤ ε

Helper: absDiff of common-prefix bind. If the continuations differ by at most ε pointwise, then the bound propagates through a shared computation prefix.

theorem CatCrypt.Crypto.sdist_comp_left {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → Core.SPComp β) (g₁ g₂ : β → Core.SPComp γ) : (sdist (fun (a : α) => (f a).bind g₁) fun (a : α) => (f a).bind g₂) ≤ sdist g₁ g₂

Left PPL: pre-composition doesn't increase distance. The proof uses the weighted average argument via absDiff_prTrue_bind_le.

theorem CatCrypt.Crypto.sdist_comp_left_two {α : Type u_1} {β₁ : Type u_2} {β₂ : Type u_3} {γ : Type u_4} (f : α → Core.SPComp β₁) (h : β₁ → Core.SPComp β₂) (g₁ g₂ : β₂ → Core.SPComp γ) : (sdist (fun (a : α) => (f a).bind fun (b₁ : β₁) => (h b₁).bind g₁) fun (a : α) => (f a).bind fun (b₁ : β₁) => (h b₁).bind g₂) ≤ sdist g₁ g₂

Two-level sdist_comp_left: pre-composition with two nested binds (shared across both sides) does not increase sdist. Derives from a single sdist_comp_left by collapsing the two binds via associativity.

theorem CatCrypt.Crypto.sdist_comp_left_two_dep {α : Type u_1} {β₁ : Type u_2} {β₂ : Type u_3} {γ : Type u_4} (f : α → Core.SPComp β₁) (h : β₁ → Core.SPComp β₂) (g₁ g₂ : β₁ → β₂ → Core.SPComp γ) (ε : ENNReal) (hbound : ∀ (b₁ : β₁), sdist (g₁ b₁) (g₂ b₁) ≤ ε) : (sdist (fun (a : α) => (f a).bind fun (b₁ : β₁) => (h b₁).bind (g₁ b₁)) fun (a : α) => (f a).bind fun (b₁ : β₁) => (h b₁).bind (g₂ b₁)) ≤ ε

Dependent two-level sdist_comp_left (uniform bound variant): if the innermost continuations g₁ b₁, g₂ b₁ are pointwise-ε-close for every intermediate value b₁, then the full two-bind composition is also ε-close.

The dependent version is needed when the continuation depends on both the intermediate bind value and the sampled one — e.g., when routing ciphertext-output p.1 from an outer epoch ratchet into the final output while an inner sample W supplies the next epoch's chain key.

Tensor (Coproduct) Distance Bounds

theorem CatCrypt.Crypto.sdist_wkR_le {α₁ α₂ : Type} (f₁ f₂ : α₁ → Core.SPComp α₂) (Y : Type) : sdist (Core.KlSPComp.wkR f₁ Y) (Core.KlSPComp.wkR f₂ Y) ≤ sdist f₁ f₂

Distance of right-whiskered morphisms. On .inl, only f runs; on .inr, distance is 0.

theorem CatCrypt.Crypto.sdist_wkL_le (X : Type) {β₁ β₂ : Type} (g₁ g₂ : β₁ → Core.SPComp β₂) : sdist (Core.KlSPComp.wkL X g₁) (Core.KlSPComp.wkL X g₂) ≤ sdist g₁ g₂

Distance of left-whiskered morphisms. On .inr, only g runs; on .inl, distance is 0.

Composition Bound

theorem CatCrypt.Crypto.sdist_comp_add {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f₁ f₂ : α → Core.SPComp β) (g₁ g₂ : β → Core.SPComp γ) {ε₁ ε₂ : ENNReal} (hf : sdist f₁ f₂ ≤ ε₁) (hg : sdist g₁ g₂ ≤ ε₂) : (sdist (fun (a : α) => (f₁ a).bind g₁) fun (a : α) => (f₂ a).bind g₂) ≤ ε₁ + ε₂

Two ε-close morphisms compose to give (ε₁+ε₂)-close morphisms.

Monotonicity

theorem CatCrypt.Crypto.sdist_le_of_forall {α : Type u_1} {β : Type u_2} {f g : α → Core.SPComp β} {ε : ENNReal} (h : sdist f g ≤ ε) (D : β → Core.SPComp Bool) (a : α) (h₀ : Core.Heap) : absDiff (prTrue ((f a).bind D) h₀) (prTrue ((g a).bind D) h₀) ≤ ε

If sdist f g ≤ ε, then for any specific distinguisher, input, and heap, the distinguishing advantage is bounded by ε.

IsPure Bridge: Advantage → sdist

theorem CatCrypt.Crypto.sdist_isPure_le {α : Type u_1} {β : Type u_2} {f g : α → Core.SPComp β} {ε : ENNReal} (hf : ∀ (a : α), (f a).IsPure) (hg : ∀ (a : α), (g a).IsPure) (hε : ∀ (D : β → Core.SPComp Bool) (a : α), absDiff (prTrue ((f a).bind D) Core.Heap.empty) (prTrue ((g a).bind D) Core.Heap.empty) ≤ ε) : sdist f g ≤ ε

For IsPure computations, sdist can be bounded using only Heap.empty.

When f and g are heap-independent, prTrue(f a >>= D, h₀) depends on h₀ only through D. By "shifting" the distinguisher to absorb h₀, we reduce the supremum over all heaps to evaluation at Heap.empty alone.

This bridges the gap between Advantage (defined at Heap.empty) and sdist (which takes the supremum over ALL initial heaps).

AdvantageA Bridge

sdist_isPure_le takes arguments in (D, a) order, but security hypotheses are typically stated in (a, D) order: ∀ x D, AdvantageA (f x) (g x) D ≤ ε. These variants eliminate the manual argument swapping.

theorem CatCrypt.Crypto.sdist_of_isPure_advantageA {α : Type u_1} {β : Type u_2} {f g : α → Core.SPComp β} {ε : ENNReal} (hf : ∀ (a : α), (f a).IsPure) (hg : ∀ (a : α), (g a).IsPure) (hAdv : ∀ (a : α) (D : β → Core.SPComp Bool), AdvantageA (f a) (g a) D ≤ ε) : sdist f g ≤ ε

Bridge sdist from per-input AdvantageA bounds.

This is the most common pattern in protocol security proofs: given IsPure games and a per-input advantage bound, derive sdist.

Compared to sdist_isPure_le, the advantage hypothesis uses (a, D) order matching the convention in security definitions.

Example usage:

exact sdist_of_isPure_advantageA foo_real_isPure foo_ideal_isPure hAdv

replaces the 4-line pattern:

apply sdist_isPure_le
· intro x; exact foo_real_isPure x
· intro x; exact foo_ideal_isPure x
· intro D x; exact hAdv x D

theorem CatCrypt.Crypto.sdist_of_isPure_absDiff {α : Type u_1} {β : Type u_2} {f g : α → Core.SPComp β} {ε : ENNReal} (hf : ∀ (a : α), (f a).IsPure) (hg : ∀ (a : α), (g a).IsPure) (hAdv : ∀ (a : α) (D : β → Core.SPComp Bool), absDiff (prTrue ((f a).bind D) Core.Heap.empty) (prTrue ((g a).bind D) Core.Heap.empty) ≤ ε) : sdist f g ≤ ε

Variant of sdist_of_isPure_advantageA with raw absDiff instead of AdvantageA.

For proofs where the advantage bound is stated as raw absDiff (prTrue ...), with (a, D) argument order.

Oracle-Game sdist Bridge

For oracle-based games where the game just passes an oracle record to the adversary (G b A = A (oracles_b)), we can compute sdist from Advantage.

The key observations:

1. D-absorption: For Bool-valued output, any post-distinguisher D can be absorbed into the adversary: A(o) >>= D = A'(o) where A' o = A o >>= D.
2. Heap absorption: The adversary controls the heap via initHeap. For any initial heap h₀, define A'(o) = initHeap h₀ >> A(o). Then G b A' at Heap.empty = G b A at h₀.

Together these show: sdist G_real G_ideal = ⨆_A Advantage(G_real A, G_ideal A).

noncomputable def CatCrypt.Crypto.SPComp.initHeap (h₀ : Core.Heap) : Core.SPComp Unit

Replace the current heap with h₀, discarding the old heap. (initHeap h₀ >> c) h = c h₀ for any h.

Equations

• CatCrypt.Crypto.SPComp.initHeap h₀ x✝ = CatCrypt.Prob.SDistr.pure ((), h₀)

theorem CatCrypt.Crypto.SPComp.initHeap_bind {α : Type u_1} (h₀ : Core.Heap) (c : Core.SPComp α) (h : Core.Heap) : (initHeap h₀).bind (fun (x : Unit) => c) h = c h₀

Running initHeap h₀ >> c from any heap yields c h₀.

theorem CatCrypt.Crypto.sdist_oracleGame_le {OracleIf : Type u_1} {G_real G_ideal : (OracleIf → Core.SPComp Bool) → Core.SPComp Bool} {or_real or_ideal : OracleIf} (hR : ∀ (A : OracleIf → Core.SPComp Bool), G_real A = A or_real) (hI : ∀ (A : OracleIf → Core.SPComp Bool), G_ideal A = A or_ideal) {ε : ENNReal} (hAdv : ∀ (A : OracleIf → Core.SPComp Bool), Advantage (G_real A) (G_ideal A) ≤ ε) : sdist G_real G_ideal ≤ ε

For games of the form G A = A record (game is pure function application), sdist equals the supremum of Advantage over all adversaries.

This bridges oracle-game security (∀ A, Advantage ≤ ε) to the categorical sdist framework, giving access to PPLs, composition, and tensor bounds.

The hypotheses state that G_real and G_ideal are pure application: G_real A h = A real_oracles h and G_ideal A h = A ideal_oracles h.

PseudoEMetricSpace Instance

The pseudometric properties sdist_self, sdist_sym, sdist_triangle are exactly the axioms of Mathlib's PseudoEMetricSpace. We register this instance on a wrapper type KlMorph α β to make sdist available as edist, gaining automatic triangle-inequality chaining, edist_comm, metric space topology, etc.

def CatCrypt.Crypto.KlMorph (α : Type u_1) (β : Type u_2) : Type (max u_1 u_2)

Wrapper type for Kleisli morphisms α → SPComp β. This is a thin wrapper that exists solely to carry the PseudoEMetricSpace instance using sdist as the extended distance function.

Equations

• CatCrypt.Crypto.KlMorph α β = (α → CatCrypt.Core.SPComp β)

def CatCrypt.Crypto.KlMorph.mk {α : Type u_1} {β : Type u_2} (f : α → Core.SPComp β) : KlMorph α β

Wrap a Kleisli morphism into KlMorph.

Equations

• CatCrypt.Crypto.KlMorph.mk f = f

def CatCrypt.Crypto.KlMorph.run {α : Type u_1} {β : Type u_2} (f : KlMorph α β) : α → Core.SPComp β

Unwrap a KlMorph to the underlying Kleisli morphism.

Equations

• f.run = f

@[implicit_reducible]

noncomputable instance CatCrypt.Crypto.instEDistKlMorph {α : Type u_1} {β : Type u_2} : EDist (KlMorph α β)

Equations

• CatCrypt.Crypto.instEDistKlMorph = { edist := fun (f g : CatCrypt.Crypto.KlMorph α β) => CatCrypt.Crypto.sdist f.run g.run }

@[simp]

theorem CatCrypt.Crypto.sdist_eq_edist {α : Type u_1} {β : Type u_2} (f g : KlMorph α β) : sdist f.run g.run = edist f g

sdist equals edist on KlMorph.

@[implicit_reducible]

noncomputable instance CatCrypt.Crypto.instPseudoEMetricSpaceKlMorph {α : Type u_1} {β : Type u_2} : PseudoEMetricSpace (KlMorph α β)

Kleisli morphisms α → SPComp β form a pseudo-extended-metric space under statistical distance. This is a pseudometric (not a metric) because sdist f g = 0 does not imply f = g — two computationally different programs can have identical output distributions.

Equations

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