From 47de1cd09367a91742fb814fc4fc6be37682dfd4 Mon Sep 17 00:00:00 2001 From: ajhavlin Date: Sat, 6 Jun 2026 15:48:19 +0200 Subject: [PATCH 01/17] VectorCommitment: prove birthday collision bound --- .../Properties/Probability/Collision.lean | 163 +++++++++++++----- 1 file changed, 121 insertions(+), 42 deletions(-) diff --git a/VectorCommitment/Properties/Probability/Collision.lean b/VectorCommitment/Properties/Probability/Collision.lean index b779f3e..be8a3c4 100644 --- a/VectorCommitment/Properties/Probability/Collision.lean +++ b/VectorCommitment/Properties/Probability/Collision.lean @@ -1,32 +1,25 @@ import VectorCommitment.Properties.Probability.RandomOracle import Mathlib.Data.ENNReal.Basic +import Mathlib.Data.Fintype.BigOperators +import Mathlib.Data.Finset.Prod +import Mathlib.Algebra.BigOperators.Fin +import Mathlib.Algebra.BigOperators.Intervals +import Mathlib.Order.Interval.Finset.Fin +import Mathlib.Probability.Distributions.Uniform /-! -# RO probability lemmas: collision bound and fresh-query uniformity +# RO probability lemmas: the birthday collision bound -This file states the two textbook probability facts the four -ROM-instance files (`BindingROM`, `ExtractabilityROM`, `HidingROM`, -`EquivocationROM`) all reduce to: +The quantitative core every ROM-instance file (`BindingROM`, +`ExtractabilityROM`, `HidingROM`, `EquivocationROM`) reduces to: * **`birthdayBound`** — among `n` independent uniform samples from a finite set `R`, the probability that two of the samples coincide is at most `n · (n - 1) / (2 · |R|)`. Specialised to `R = List.Vector Bool κ` this is the classic `n² / 2^(κ+1)` form. -* **`RO_fresh_uniform`** — in the lazy-sampling RO, the response to a - query not yet in the cache is distributed uniformly on `spec.Range`. - -## Status - -Both lemmas are stated and their proofs are **deferred with `sorry`**. -The statements are precise; closing the bodies requires standard -mathlib PMF / outer-measure / union-bound machinery and is a real but -non-novel probability-library project. - -The instance files (`BindingROM`, `ExtractabilityROM`, `HidingROM`, -`EquivocationROM`) treat these as known facts and propagate their -sorries upward. Closing the proofs here will close all four -probabilistic security theorems. +Proved by a union bound over the `n(n-1)/2` unordered coordinate pairs, +each colliding with probability `1/|R|` (`prob_pair`). -/ namespace VectorCommitment.Probability @@ -38,6 +31,66 @@ open OracleComp noncomputable def collisionBound (κ q : Nat) : ENNReal := (q * (q - 1) : ENNReal) / 2 ^ (κ + 1) +section BirthdayBound +open scoped ENNReal +open Finset MeasureTheory + +/-- Functions `Fin n → R` agreeing at two distinct coordinates `i ≠ j` are in + bijection with arbitrary functions on the `n-1` coordinates `≠ j`. -/ +private def tieEquiv {R : Type} {n : ℕ} (i j : Fin n) (hij : i ≠ j) : + {f : Fin n → R // f i = f j} ≃ ({k : Fin n // k ≠ j} → R) where + toFun p := fun k => p.1 k.1 + invFun g := ⟨fun k => if h : k = j then g ⟨i, hij⟩ else g ⟨k, h⟩, by + show (if h : i = j then g ⟨i, hij⟩ else g ⟨i, h⟩) + = (if h : j = j then g ⟨i, hij⟩ else g ⟨j, h⟩) + rw [dif_neg hij, dif_pos rfl]⟩ + left_inv := by + rintro ⟨f, hf⟩ + apply Subtype.ext + funext k + show (if h : k = j then f i else f k) = f k + by_cases h : k = j + · subst h; rw [dif_pos rfl]; exact hf + · rw [dif_neg h] + right_inv := by + intro g + funext k + obtain ⟨k, hk⟩ := k + show (if h : k = j then g ⟨i, hij⟩ else g ⟨k, h⟩) = g ⟨k, hk⟩ + rw [dif_neg hk] + +/-- The number of functions tying two distinct coordinates is `|R|^(n-1)`. -/ +private lemma card_tie {R : Type} [Fintype R] [DecidableEq R] {n : ℕ} + (i j : Fin n) (hij : i ≠ j) : + Fintype.card {f : Fin n → R // f i = f j} = Fintype.card R ^ (n - 1) := by + rw [Fintype.card_congr (tieEquiv i j hij), Fintype.card_fun] + congr 1 + simp only [ne_eq] + rw [Fintype.card_subtype_compl (fun k => k = j), Fintype.card_subtype_eq, + Fintype.card_fin] + +/-- The per-pair collision probability under the uniform PMF on `Fin n → R` + is exactly `1/|R|` (for `i ≠ j`). -/ +private lemma prob_pair {R : Type} [Fintype R] [Nonempty R] [DecidableEq R] {n : ℕ} + (i j : Fin n) (hij : i ≠ j) : + (PMF.uniformOfFintype (Fin n → R)).toOuterMeasure {f | f i = f j} + = 1 / (Fintype.card R : ℝ≥0∞) := by + haveI : Fintype {f : Fin n → R // f i = f j} := Subtype.fintype _ + have hn : 0 < n := Nat.pos_of_ne_zero (fun h => by subst h; exact i.elim0) + have hc0 : (Fintype.card R : ℝ≥0∞) ≠ 0 := by simp [Fintype.card_ne_zero] + have hctop : (Fintype.card R : ℝ≥0∞) ≠ ⊤ := ENNReal.natCast_ne_top _ + have hpow0 : (Fintype.card R : ℝ≥0∞) ^ (n - 1) ≠ 0 := pow_ne_zero _ hc0 + have hpowtop : (Fintype.card R : ℝ≥0∞) ^ (n - 1) ≠ ⊤ := ENNReal.pow_ne_top hctop + have hsplit : (Fintype.card R : ℝ≥0∞) ^ n + = (Fintype.card R : ℝ≥0∞) ^ (n - 1) * (Fintype.card R) := by + rw [← pow_succ, Nat.sub_add_cancel hn] + rw [PMF.toOuterMeasure_uniformOfFintype_apply, + show Fintype.card ↥{f : Fin n → R | f i = f j} = Fintype.card R ^ (n - 1) + from card_tie i j hij, + Fintype.card_fun, Fintype.card_fin, Nat.cast_pow, Nat.cast_pow, hsplit, + div_eq_mul_inv, ENNReal.mul_inv (Or.inl hpow0) (Or.inl hpowtop), ← mul_assoc, + ENNReal.mul_inv_cancel hpow0 hpowtop, one_mul, one_div] + /-- **Birthday bound.** Among `n` independent uniform samples from a finite, nonempty range `R`, the probability that some pair of samples coincides is at most `n · (n - 1) / (2 · |R|)`. @@ -45,14 +98,60 @@ noncomputable def collisionBound (κ q : Nat) : ENNReal := *Specialisation:* when `R = List.Vector Bool κ` (`|R| = 2^κ`) the bound becomes `collisionBound κ n`. - *Proof:* union bound over `(n choose 2)` pairs, each pair coinciding - with probability `1 / |R|` by independence of uniform samples. - Deferred (see file-level docstring). -/ + *Proof:* union bound over the `n(n-1)/2` unordered pairs `{i p.1 < p.2) with hpairs + have hcover : {f : Fin n → R | ∃ i j, i ≠ j ∧ f i = f j} + ⊆ ⋃ p ∈ pairs, {f : Fin n → R | f p.1 = f p.2} := by + intro f hf + obtain ⟨i, j, hij, hfij⟩ := hf + rcases lt_or_gt_of_ne hij with h | h + · refine Set.mem_iUnion₂.mpr ⟨(i, j), ?_, hfij⟩ + rw [hpairs]; exact Finset.mem_filter.mpr ⟨Finset.mem_univ _, h⟩ + · refine Set.mem_iUnion₂.mpr ⟨(j, i), ?_, hfij.symm⟩ + rw [hpairs]; exact Finset.mem_filter.mpr ⟨Finset.mem_univ _, h⟩ + have h2 : pairs.card * 2 = n * (n - 1) := by + have hcount : ∀ b : Fin n, + (univ.filter (fun a : Fin n => a < b)).card = (b : ℕ) := by + intro b + rw [show univ.filter (fun a : Fin n => a < b) = Finset.Iio b from by + ext a; simp [Finset.mem_Iio], Fin.card_Iio] + rw [hpairs, Finset.card_filter, Fintype.sum_prod_type, Finset.sum_comm] + simp_rw [← Finset.card_filter, hcount] + rw [Fin.sum_univ_eq_sum_range (fun i => i) n] + exact Finset.sum_range_id_mul_two n + calc (PMF.uniformOfFintype (Fin n → R)).toOuterMeasure + {f | ∃ i j : Fin n, i ≠ j ∧ f i = f j} + ≤ (PMF.uniformOfFintype (Fin n → R)).toOuterMeasure + (⋃ p ∈ pairs, {f | f p.1 = f p.2}) := + measure_mono hcover + _ ≤ ∑ p ∈ pairs, + (PMF.uniformOfFintype (Fin n → R)).toOuterMeasure {f | f p.1 = f p.2} := + measure_biUnion_finset_le pairs _ + _ = ∑ _p ∈ pairs, (1 / (Fintype.card R : ℝ≥0∞)) := by + refine Finset.sum_congr rfl (fun p hp => ?_) + rw [hpairs, Finset.mem_filter] at hp + exact prob_pair p.1 p.2 (ne_of_lt hp.2) + _ = (pairs.card : ℝ≥0∞) * (1 / Fintype.card R) := by + rw [Finset.sum_const, nsmul_eq_mul] + _ ≤ (n * (n - 1) : ENNReal) / (2 * Fintype.card R) := by + have hcast : (pairs.card : ℝ≥0∞) * 2 = (n : ℝ≥0∞) * ((n : ℝ≥0∞) - 1) := by + rcases Nat.eq_zero_or_pos n with hn0 | hn1 + · subst hn0; simp + · have e : ((pairs.card * 2 : ℕ) : ℝ≥0∞) = ((n * (n - 1) : ℕ) : ℝ≥0∞) := + congrArg Nat.cast h2 + push_cast [Nat.cast_sub hn1] at e + exact e + refine le_of_eq ?_ + rw [mul_one_div, ← hcast, mul_comm (pairs.card : ℝ≥0∞) 2, + ENNReal.mul_div_mul_left _ _ (by simp) (by simp)] + +end BirthdayBound /-- Specialisation to κ-bit digests: the birthday bound is exactly `collisionBound κ n = n(n-1)/2^(κ+1)`. Reduction to `birthdayBound`. -/ @@ -72,24 +171,4 @@ theorem birthdayBound_kappa (κ n : Nat) {R : Type} rw [pow_succ, mul_comm] rw [h_denom] -/-- **Fresh-query uniformity.** In the lazy-sampling RO, the response - to a query *not yet in the cache* is distributed uniformly on - `spec.Range`, projecting `(value, ending log)` to just the value. - - *Proof:* immediate from the `none` branch of `OracleComp.query`. -/ -theorem RO_fresh_uniform {spec : OracleSpec} - (d : spec.Domain) (log : QueryLog spec) - (h_novel : log.lookup d = none) : - ((OracleComp.query d log).map Prod.fst) = - PMF.uniformOfFintype spec.Range := by - show ((OracleComp.query d log).map Prod.fst) = _ - unfold OracleComp.query - rw [h_novel] - -- Goal: ((PMF.uniformOfFintype spec.Range).bind (fun r => PMF.pure (r, log.append d r))).map Prod.fst = _ - rw [PMF.map_bind] - -- Now each summand: (PMF.pure (r, log.append d r)).map Prod.fst = PMF.pure r - simp only [PMF.pure_map] - -- Goal: (PMF.uniformOfFintype spec.Range).bind (fun r => PMF.pure r) = _ - exact PMF.bind_pure _ - end VectorCommitment.Probability From 9cba95a85e60ddb44d4fe895a98bfc2ddcaa0ec4 Mon Sep 17 00:00:00 2001 From: ajhavlin Date: Sat, 6 Jun 2026 15:48:20 +0200 Subject: [PATCH 02/17] VectorCommitment: free-monad random oracle --- .../Properties/Probability/RandomOracle.lean | 84 ++++++++++++------- 1 file changed, 56 insertions(+), 28 deletions(-) diff --git a/VectorCommitment/Properties/Probability/RandomOracle.lean b/VectorCommitment/Properties/Probability/RandomOracle.lean index b0ad1c7..acc3276 100644 --- a/VectorCommitment/Properties/Probability/RandomOracle.lean +++ b/VectorCommitment/Properties/Probability/RandomOracle.lean @@ -96,7 +96,7 @@ attribute [instance] OracleSpec.inhabitedRange /-- The query log: an ordered list of `(query, response)` pairs the oracle has produced so far. Newer entries near the head. Acts as the cache for lazy sampling. -/ -def QueryLog (spec : OracleSpec) : Type := List (spec.Domain × spec.Range) +abbrev QueryLog (spec : OracleSpec) : Type := List (spec.Domain × spec.Range) namespace QueryLog variable {spec : OracleSpec} @@ -131,46 +131,74 @@ def length (log : QueryLog spec) : Nat := List.length log end QueryLog -/-- A computation with access to the random oracle. Concretely: a - function taking the starting cache and returning a `PMF` over - `(value, ending cache)` pairs. -/ -def OracleComp (spec : OracleSpec) (α : Type) : Type := - QueryLog spec → PMF (α × QueryLog spec) +/-- A computation with access to the random oracle, as an operational free + monad: either `ret` a value, or `call` the oracle on one input and + continue with the response. Keeping the node first-order (the + continuation ranges over `spec.Range`, a fixed type) keeps `OracleComp` + in `Type`, so it fits the `Type`-valued adversary fields of the security + classes, and the inductive shape exposes the structural recursion the + trace/i.i.d. analysis runs on. -/ +inductive OracleComp (spec : OracleSpec) (α : Type) : Type where + | ret : α → OracleComp spec α + | call : spec.Domain → (spec.Range → OracleComp spec α) → OracleComp spec α namespace OracleComp variable {spec : OracleSpec} -noncomputable instance : Monad (OracleComp spec) where - pure x := fun log => PMF.pure (x, log) - bind m f := fun log => (m log).bind fun p => f p.fst p.snd - -/-- Query the oracle on `d`. On a novel query, sample a fresh response - uniformly from `spec.Range` and cache it; on a repeat, return the - cached response. -/ -noncomputable def query (d : spec.Domain) : OracleComp spec spec.Range := - fun log => - match log.lookup d with - | some r => PMF.pure (r, log) - | none => - (PMF.uniformOfFintype spec.Range).bind fun r => - PMF.pure (r, log.append d r) - -/-- Run a computation from the empty log; project the value distribution. -/ +/-- Monadic bind, by recursion on the computation tree. -/ +def bind {α β} : OracleComp spec α → (α → OracleComp spec β) → OracleComp spec β + | ret a, f => f a + | call d k, f => call d (fun r => (k r).bind f) + +instance : Monad (OracleComp spec) where + pure := ret + bind := bind + +/-- Query the oracle on `d`, returning its response. -/ +def query (d : spec.Domain) : OracleComp spec spec.Range := call d ret + +/-- Run a computation against a starting cache: on a novel query sample a + fresh response uniformly and cache it; on a repeat reuse the cached one. -/ +noncomputable def run {α} : + OracleComp spec α → QueryLog spec → PMF (α × QueryLog spec) + | ret a, log => PMF.pure (a, log) + | call d k, log => + match log.lookup d with + | some r => (k r).run log + | none => + (PMF.uniformOfFintype spec.Range).bind fun r => + (k r).run (log.append d r) + +/-- Run from the empty cache; project the value distribution. -/ noncomputable def simulateQ (c : OracleComp spec α) : PMF α := - (c QueryLog.empty).map Prod.fst + (c.run QueryLog.empty).map Prod.fst -/-- Run a computation from a pre-populated log. Used by the equivocation - simulator: pre-populate the log to *program* the oracle at chosen - points, then sample freshly elsewhere. -/ +/-- Run from a pre-populated cache; project the value distribution. -/ noncomputable def simulateQFrom (c : OracleComp spec α) (log : QueryLog spec) : PMF α := - (c log).map Prod.fst + (c.run log).map Prod.fst + +@[simp] theorem run_ret {α} (a : α) (log : QueryLog spec) : + (ret a : OracleComp spec α).run log = PMF.pure (a, log) := rfl + +/-- `run` pushes through `bind`: the bridge from monadic experiments to their + `PMF` semantics. Proved by induction on the computation tree. -/ +@[simp] theorem run_bind {α β} (c : OracleComp spec α) + (f : α → OracleComp spec β) (log : QueryLog spec) : + (c.bind f).run log = (c.run log).bind (fun p => (f p.1).run p.2) := by + induction c generalizing log with + | ret a => simp [bind, run] + | call d k ih => + simp only [bind, run] + cases h : log.lookup d with + | some r => simp [ih] + | none => simp [ih, PMF.bind_bind] end OracleComp /-- The lazy-sampled random oracle. An alias to make the API name match VCVio's `randomOracle`. -/ @[inline, reducible] -noncomputable def randomOracle {spec : OracleSpec} : +def randomOracle {spec : OracleSpec} : spec.Domain → OracleComp spec spec.Range := OracleComp.query From 9ccb051c82fbbf0a32b34c2f5b7b85ded0641874 Mon Sep 17 00:00:00 2001 From: ajhavlin Date: Sat, 6 Jun 2026 15:48:21 +0200 Subject: [PATCH 03/17] VectorCommitment: ROM hasher digest squeezing --- .../Properties/Probability/ROHasher.lean | 74 +++++++++++++------ 1 file changed, 50 insertions(+), 24 deletions(-) diff --git a/VectorCommitment/Properties/Probability/ROHasher.lean b/VectorCommitment/Properties/Probability/ROHasher.lean index a83c680..1393adc 100644 --- a/VectorCommitment/Properties/Probability/ROHasher.lean +++ b/VectorCommitment/Properties/Probability/ROHasher.lean @@ -40,33 +40,58 @@ def Tag.leaf : ByteArray := ⟨#[0]⟩ /-- Single-byte domain-separation tag for internal-node hashes. -/ def Tag.node : ByteArray := ⟨#[1]⟩ -/-- Encode a leaf query: `LEAF :: symbol bytes ++ salt bytes`. -/ -def encodeLeaf (sym salt : List ByteArray) : List ByteArray := - Tag.leaf :: sym ++ salt - -/-- Encode an internal-node query: `NODE :: serialized children`. - A child digest `d : List.Vector Bool κ` is serialized to a `ByteArray` - by mapping each bit to a 0/1 byte. This is wasteful in bytes but - simple, injective, and unambiguous about boundaries (every child - contributes exactly `κ` bytes). -/ +/-- Serialize a `κ`-bit digest/field element to a `ByteArray`, one `0`/`1` byte + per bit. Fixed width (`κ` bytes) and injective — the canonical fixed-width + boundary that the real (Poseidon `F`, bytewise `[u8;S]`) hashers rely on. -/ +def vecBytes {κ : Nat} (d : List.Vector Bool κ) : ByteArray := + ⟨(d.toList.map (fun b => if b then (1 : UInt8) else (0 : UInt8))).toArray⟩ + +theorem vecBytes_injective {κ : Nat} : Function.Injective (vecBytes (κ := κ)) := by + intro d0 d1 h + unfold vecBytes at h + have h1 : (d0.toList.map (fun b => if b then (1 : UInt8) else 0)).toArray + = (d1.toList.map (fun b => if b then (1 : UInt8) else 0)).toArray := by + injection h + have h2 : d0.toList.map (fun b => if b then (1 : UInt8) else 0) + = d1.toList.map (fun b => if b then (1 : UInt8) else 0) := by + simpa using congrArg Array.toList h1 + have hf : Function.Injective (fun b : Bool => if b then (1 : UInt8) else 0) := by + intro a b hab; cases a <;> cases b <;> simp_all + exact List.Vector.toList_injective (List.map_injective_iff.mpr hf h2) + +/-- Encode a leaf query as a fixed-width structured triple + `[LEAF, value-bytes, salt-bytes]`. The value and salt are fixed-width fields + in distinct positions (not flattened into one ambiguous byte stream), so the + encoding is injective — `encodeLeaf_inj`. This models the real hashers, whose + leaf input is a typed `(F, Salt)` / `(Vec, [u8;S])` with canonical + fixed-width encodings, rather than a variable-length byte concatenation. -/ +def encodeLeaf {κ : Nat} (sym salt : List.Vector Bool κ) : List ByteArray := + [Tag.leaf, vecBytes sym, vecBytes salt] + +/-- The leaf encoding is injective in `(value, salt)` — the fixed-width boundary + that makes Merkle position binding sound (without it an adversary could open + one position to two distinct values with no hash collision). -/ +theorem encodeLeaf_inj {κ : Nat} {v0 s0 v1 s1 : List.Vector Bool κ} + (h : encodeLeaf v0 s0 = encodeLeaf v1 s1) : v0 = v1 ∧ s0 = s1 := by + simp only [encodeLeaf, List.cons.injEq, and_true] at h + exact ⟨vecBytes_injective h.2.1, vecBytes_injective h.2.2⟩ + +/-- Encode an internal-node query: `NODE :: serialized children`. Each child is + serialized to exactly `κ` bytes by `vecBytes`, so boundaries are unambiguous. -/ def encodeNodes {κ : Nat} (children : List (List.Vector Bool κ)) : List ByteArray := - Tag.node :: - children.map fun d => - ⟨(d.toList.map (fun b => if b then (1 : UInt8) else (0 : UInt8))).toArray⟩ + Tag.node :: children.map vecBytes /-- Domain separation: a leaf encoding never coincides with a node encoding. The two start with distinct tag bytes. -/ theorem encodeLeaf_ne_encodeNodes - {κ : Nat} (sym salt : List ByteArray) + {κ : Nat} (sym salt : List.Vector Bool κ) (children : List (List.Vector Bool κ)) : encodeLeaf sym salt ≠ encodeNodes children := by intro h - -- Both lists are nonempty with their tag byte as the head. have h_head : (encodeLeaf sym salt).head? = (encodeNodes children).head? := congrArg List.head? h - -- Reduce the heads to the literal tag ByteArrays. simp [encodeLeaf, encodeNodes, Tag.leaf, Tag.node, List.head?] at h_head /-- The hasher value: a thin wrapper around a sampled RO function. -/ @@ -75,20 +100,21 @@ structure ROHasherValue (κ : Nat) where /-- `MerkleHasher` instance for the RO-derived hasher. - The symbol and salt types are `List ByteArray` — concrete enough that - the RO can take them as queries, abstract enough that callers can - encode whatever symbol/salt they need into bytes. + Symbol and salt are fixed-width `κ`-bit fields (`List.Vector Bool κ`), + matching the typed leaf input of the real hashers and giving the injective + leaf encoding `encodeLeaf_inj` that position binding needs. - The salt sampler is a placeholder (returns `[]`); the hiding and - equivocation instances will provide real per-leaf salts. -/ + The salt sampler is a placeholder (constant `0^κ`); a hiding instance must + replace it with a uniform draw of sufficient entropy (for small fields, + `Salt = F` is insufficient — out of scope here, binding only). -/ noncomputable instance instMerkleHasherROHasher (κ : Nat) : MerkleHasher (ROHasherValue κ) where - Symbol := List ByteArray + Symbol := List.Vector Bool κ Digest := List.Vector Bool κ - Salt := List ByteArray + Salt := List.Vector Bool κ decEqDigest := inferInstance - defaultSalt := ⟨[]⟩ - sampleSalt := fun _ _ => [] + defaultSalt := ⟨List.Vector.replicate κ false⟩ + sampleSalt := fun _ _ => List.Vector.replicate κ false hashLeaf := fun h sym salt => h.oracle (encodeLeaf sym salt) hashNodes := fun h children => h.oracle (encodeNodes children) From 3d3d369320f106f077da9ad6eadcbce8d9894304 Mon Sep 17 00:00:00 2001 From: ajhavlin Date: Sat, 6 Jun 2026 15:48:23 +0200 Subject: [PATCH 04/17] VectorCommitment: adaptive lazy-oracle trace collision bound --- .../Properties/Probability/Coupling.lean | 238 ++++++++++++++++++ 1 file changed, 238 insertions(+) create mode 100644 VectorCommitment/Properties/Probability/Coupling.lean diff --git a/VectorCommitment/Properties/Probability/Coupling.lean b/VectorCommitment/Properties/Probability/Coupling.lean new file mode 100644 index 0000000..daab68c --- /dev/null +++ b/VectorCommitment/Properties/Probability/Coupling.lean @@ -0,0 +1,238 @@ +/- +Copyright (c) 2026 LeanStuff contributors. All rights reserved. +-/ +import VectorCommitment.Properties.Probability.RandomOracle +import VectorCommitment.Properties.Probability.ROHasher +import VectorCommitment.Properties.Probability.Collision +import Mathlib.Data.Fintype.Vector + +/-! +# Trace collision bound for the lazy-sampling oracle + +The probability that a finished query trace contains two distinct queries with +the same response is at most `collisionBound κ q = q(q-1)/2^(κ+1)`, for a +computation spending at most `q` oracle queries. + +The proof is a direct induction on the computation. Each fresh oracle query +draws a uniform response; it collides with one of the `≤ m` responses already +cached with probability `≤ m/|R|`. Accumulated over the `≤ q` fresh queries +this telescopes to `(0 + 1 + ⋯ + (q-1))/|R| = q(q-1)/(2|R|)`, the birthday +bound — no separate eager sampling space is needed. +-/ + +namespace VectorCommitment.Probability + +open OracleComp +open scoped ENNReal + +/-- A finished query log *collides* when it holds two entries with distinct + query inputs but identical oracle responses — the "random oracle repeated a + digest" bad event the binding / extractability reductions branch on. -/ +def QueryLog.hasCollision {spec : OracleSpec} (log : QueryLog spec) : Prop := + ∃ e₁ ∈ log, ∃ e₂ ∈ log, e₁.1 ≠ e₂.1 ∧ e₁.2 = e₂.2 + +/-- A computation *spends at most `q` queries* when every finished run from the + empty cache leaves a log of length `≤ q`. Lazy sampling appends only on a + cache miss, so `log.length` counts the distinct queries actually issued. -/ +def OracleComp.QueryBudget {spec : OracleSpec} {α : Type} + (c : OracleComp spec α) (q : Nat) : Prop := + ∀ p ∈ (c.run QueryLog.empty).support, p.2.length ≤ q + +variable {spec : OracleSpec} + +/-- `run` only ever extends the cache, so every reachable final log is at least + as long as the starting one. -/ +theorem run_length_le {α} (c : OracleComp spec α) : + ∀ (log : QueryLog spec) p, p ∈ (c.run log).support → log.length ≤ p.2.length := by + induction c with + | ret a => + intro log p hp + simp only [run_ret, PMF.support_pure, Set.mem_singleton_iff] at hp + subst hp; exact le_rfl + | call d k ih => + intro log p hp + rw [run] at hp + cases hlk : log.lookup d with + | some r => rw [hlk] at hp; exact ih r log p hp + | none => + rw [hlk] at hp + simp only [PMF.support_bind, Set.mem_iUnion] at hp + obtain ⟨r, _, hpr⟩ := hp + have := ih r (log.append d r) p hpr + simp only [QueryLog.length_append] at this + omega + +/-- `log.lookup d = none` means no entry has domain input `d`. -/ +theorem forall_ne_of_lookup_none {log : QueryLog spec} {d : spec.Domain} + (h : log.lookup d = none) : ∀ e ∈ log, e.1 ≠ d := by + intro e he + rw [QueryLog.lookup, Option.map_eq_none_iff, List.find?_eq_none] at h + have := h e he + simpa using this + +/-- Appending a fresh-domain entry `(d, r)` to a collision-free log creates a + collision exactly when `r` already appears as some cached response. -/ +theorem hasCollision_append_iff {log : QueryLog spec} {d : spec.Domain} + {r : spec.Range} (hd : log.lookup d = none) (hlog : ¬ QueryLog.hasCollision log) : + QueryLog.hasCollision (log.append d r) ↔ r ∈ log.map Prod.snd := by + have hfresh := forall_ne_of_lookup_none hd + constructor + · rintro ⟨e₁, he₁, e₂, he₂, hne, heq⟩ + simp only [QueryLog.append, List.mem_cons] at he₁ he₂ + rcases he₁ with rfl | he₁ <;> rcases he₂ with rfl | he₂ + · exact absurd rfl hne + · exact List.mem_map.mpr ⟨e₂, he₂, heq.symm⟩ + · exact List.mem_map.mpr ⟨e₁, he₁, heq⟩ + · exact absurd ⟨e₁, he₁, e₂, he₂, hne, heq⟩ hlog + · intro hr + obtain ⟨e, he, hee⟩ := List.mem_map.mp hr + exact ⟨(d, r), by simp [QueryLog.append], e, by simp [QueryLog.append, he], + (hfresh e he).symm, hee.symm⟩ + +/-- **Trace collision bound, inductive core.** For a computation run from a + collision-free cache of length `m`, every reachable final log having length + `≤ q`, the probability the final log collides is at most + `(∑ i ∈ Ico m q, i)/|R|`. At `m = 0` the sum is `q(q-1)/2`. -/ +theorem run_coll_le {α} (q : Nat) (c : OracleComp spec α) : + ∀ (log : QueryLog spec), ¬ QueryLog.hasCollision log → + (∀ p ∈ (c.run log).support, p.2.length ≤ q) → + (c.run log).toOuterMeasure {p | QueryLog.hasCollision p.2} + ≤ (∑ i ∈ Finset.Ico log.length q, (i : ℝ≥0∞)) / (Fintype.card spec.Range) := by + induction c with + | ret a => + intro log hlog _ + simp only [run_ret, PMF.toOuterMeasure_pure_apply, Set.mem_setOf_eq] + rw [if_neg hlog]; exact zero_le _ + | call d k ih => + intro log hlog hbud + cases hlk : log.lookup d with + | some r => + have hrun : (call d k).run log = (k r).run log := by rw [run, hlk] + rw [hrun] at hbud ⊢ + exact ih r log hlog hbud + | none => + have hrun : (call d k).run log + = (PMF.uniformOfFintype spec.Range).bind + (fun r => (k r).run (log.append d r)) := by rw [run, hlk] + rw [hrun] at hbud ⊢ + classical + set N : ℝ≥0∞ := (Fintype.card spec.Range : ℝ≥0∞) with hN + have hcard : N ≠ 0 := by rw [hN]; simp [Fintype.card_ne_zero] + have hcardtop : N ≠ ⊤ := by rw [hN]; exact ENNReal.natCast_ne_top _ + -- m < q, from a reachable length-(m+1) outcome. + have hmlt : log.length < q := by + obtain ⟨r₀⟩ := (inferInstance : Nonempty spec.Range) + obtain ⟨p₀, hp₀⟩ := ((k r₀).run (log.append d r₀)).support_nonempty + have hmem : p₀ ∈ ((PMF.uniformOfFintype spec.Range).bind + (fun r => (k r).run (log.append d r))).support := by + rw [PMF.support_bind] + exact Set.mem_iUnion₂.mpr ⟨r₀, by simp [PMF.support_uniformOfFintype], hp₀⟩ + have h1 := hbud p₀ hmem + have h2 := run_length_le (k r₀) (log.append d r₀) p₀ hp₀ + simp only [QueryLog.length_append] at h2 + omega + set B : Finset spec.Range := (log.map Prod.snd).toFinset with hB + have hBcard : (B.card : ℝ≥0∞) ≤ (log.length : ℝ≥0∞) := by + have : B.card ≤ log.length := by + calc B.card ≤ (log.map Prod.snd).length := List.toFinset_card_le _ + _ = log.length := by simp [QueryLog.length] + exact_mod_cast this + set C : ℝ≥0∞ := (∑ i ∈ Finset.Ico (log.length + 1) q, (i : ℝ≥0∞)) / N with hC + -- Termwise majorant of the per-response collision probability. + have hterm : ∀ r, ((k r).run (log.append d r)).toOuterMeasure + {p | QueryLog.hasCollision p.2} + ≤ (if r ∈ B then (1 : ℝ≥0∞) else 0) + C := by + intro r + by_cases hr : r ∈ B + · rw [if_pos hr] + calc ((k r).run (log.append d r)).toOuterMeasure {p | QueryLog.hasCollision p.2} + ≤ ((k r).run (log.append d r)).toOuterMeasure Set.univ := + ((k r).run (log.append d r)).toOuterMeasure_mono (Set.subset_univ _) + _ = 1 := (PMF.toOuterMeasure_apply_eq_one_iff _ _).mpr (Set.subset_univ _) + _ ≤ 1 + C := le_add_right le_rfl + · rw [if_neg hr, zero_add] + have hr' : r ∉ log.map Prod.snd := by simpa [hB, List.mem_toFinset] using hr + have hnc : ¬ QueryLog.hasCollision (log.append d r) := by + rw [hasCollision_append_iff hlk hlog]; exact hr' + have hbud' : ∀ p ∈ ((k r).run (log.append d r)).support, p.2.length ≤ q := by + intro p hp + refine hbud p ?_ + rw [PMF.support_bind] + exact Set.mem_iUnion₂.mpr ⟨r, by simp [PMF.support_uniformOfFintype], hp⟩ + have := ih r (log.append d r) hnc hbud' + simpa only [QueryLog.length_append, hC] using this + -- Sum the majorant. + rw [PMF.toOuterMeasure_bind_apply] + have hsum : ∑' r, (PMF.uniformOfFintype spec.Range) r + * ((k r).run (log.append d r)).toOuterMeasure {p | QueryLog.hasCollision p.2} + ≤ (log.length : ℝ≥0∞) / N + C := by + calc ∑' r, (PMF.uniformOfFintype spec.Range) r + * ((k r).run (log.append d r)).toOuterMeasure {p | QueryLog.hasCollision p.2} + ≤ ∑' r, (PMF.uniformOfFintype spec.Range) r + * ((if r ∈ B then (1 : ℝ≥0∞) else 0) + C) := + ENNReal.tsum_le_tsum (fun r => by gcongr; exact hterm r) + _ = ∑' r, ((PMF.uniformOfFintype spec.Range) r * (if r ∈ B then (1 : ℝ≥0∞) else 0) + + (PMF.uniformOfFintype spec.Range) r * C) := by simp_rw [mul_add] + _ = (∑' r, (PMF.uniformOfFintype spec.Range) r * (if r ∈ B then (1 : ℝ≥0∞) else 0)) + + (∑' r, (PMF.uniformOfFintype spec.Range) r * C) := ENNReal.tsum_add + _ ≤ (log.length : ℝ≥0∞) / N + C := by + refine add_le_add ?_ (le_of_eq ?_) + · -- first sum = B.card / N ≤ m / N + rw [tsum_fintype] + simp_rw [PMF.uniformOfFintype_apply, ← hN] + rw [← Finset.mul_sum, ENNReal.div_eq_inv_mul] + gcongr + calc ∑ r : spec.Range, (if r ∈ B then (1 : ℝ≥0∞) else 0) + = (B.card : ℝ≥0∞) := by simp + _ ≤ (log.length : ℝ≥0∞) := hBcard + · -- second sum = C + rw [tsum_fintype] + simp_rw [PMF.uniformOfFintype_apply, ← hN] + rw [← Finset.sum_mul, Finset.sum_const, Finset.card_univ, nsmul_eq_mul, ← hN, + ENNReal.mul_inv_cancel hcard hcardtop, one_mul] + refine hsum.trans (le_of_eq ?_) + -- m/N + (∑ Ico (m+1) q)/N = (∑ Ico m q)/N + rw [hC, ENNReal.div_add_div_same] + congr 1 + rw [← Finset.insert_Ico_succ_left_eq_Ico hmlt, + Finset.sum_insert (by simp), Order.succ_eq_add_one] + +/-- **Trace collision bound for Merkle random oracles.** A computation spending + at most `q` queries to a `κ`-bit random oracle produces a colliding trace + with probability at most `collisionBound κ q = q(q-1)/2^(κ+1)`. -/ +theorem coupling_trace_le_collisionBound {κ : Nat} {α : Type} + (c : OracleComp (ROHasher.MerkleROSpec κ) α) (q : Nat) + (hbud : OracleComp.QueryBudget c q) : + (c.run QueryLog.empty).toOuterMeasure {p | QueryLog.hasCollision p.2} + ≤ collisionBound κ q := by + have hemp : ¬ QueryLog.hasCollision (QueryLog.empty : QueryLog (ROHasher.MerkleROSpec κ)) := by + simp [QueryLog.hasCollision, QueryLog.empty] + have h := run_coll_le q c QueryLog.empty hemp hbud + have hlen : (QueryLog.empty : QueryLog (ROHasher.MerkleROSpec κ)).length = 0 := rfl + rw [hlen] at h + have hcard : Fintype.card (ROHasher.MerkleROSpec κ).Range = 2 ^ κ := by + show Fintype.card (List.Vector Bool κ) = 2 ^ κ + rw [Fintype.card_congr (Equiv.vectorEquivFin Bool κ), Fintype.card_fun, + Fintype.card_fin, Fintype.card_bool] + rw [hcard] at h + refine h.trans (le_of_eq ?_) + rw [← Finset.range_eq_Ico] + unfold collisionBound + have ha0 : (2 : ℝ≥0∞) ^ (κ + 1) ≠ 0 := by positivity + have haT : (2 : ℝ≥0∞) ^ (κ + 1) ≠ ∞ := by apply ENNReal.pow_ne_top; simp + have hb0 : ((2 ^ κ : ℕ) : ℝ≥0∞) ≠ 0 := by positivity + have hbT : ((2 ^ κ : ℕ) : ℝ≥0∞) ≠ ∞ := by simp + rw [ENNReal.div_eq_div_iff ha0 haT hb0 hbT, + show (2 : ℝ≥0∞) ^ (κ + 1) = ((2 ^ κ : ℕ) : ℝ≥0∞) * 2 by push_cast; rw [pow_succ], + mul_assoc] + congr 1 + rw [mul_comm] + rcases Nat.eq_zero_or_pos q with hq | hq + · subst hq; simp + · have hq1 : 1 ≤ q := hq + rw [show (q : ℝ≥0∞) * ((q : ℝ≥0∞) - 1) = ((q * (q - 1) : ℕ) : ℝ≥0∞) by + push_cast [Nat.cast_sub hq1]; ring, + ← Nat.cast_sum, ← Nat.cast_two, ← Nat.cast_mul, Nat.cast_inj] + exact Finset.sum_range_id_mul_two q + +end VectorCommitment.Probability From f40a7acd9164c96f42cca3c6a1522345e7e4e801 Mon Sep 17 00:00:00 2001 From: ajhavlin Date: Sat, 6 Jun 2026 15:48:24 +0200 Subject: [PATCH 05/17] VectorCommitment: Merkle trace-collision reductions --- .../Probability/TraceCollision.lean | 378 ++++++++++++++++++ 1 file changed, 378 insertions(+) create mode 100644 VectorCommitment/Properties/Probability/TraceCollision.lean diff --git a/VectorCommitment/Properties/Probability/TraceCollision.lean b/VectorCommitment/Properties/Probability/TraceCollision.lean new file mode 100644 index 0000000..03f64ae --- /dev/null +++ b/VectorCommitment/Properties/Probability/TraceCollision.lean @@ -0,0 +1,378 @@ +/- +Copyright (c) 2026 LeanStuff contributors. All rights reserved. +-/ +import VectorCommitment.Properties.Probability.CheckOracle +import VectorCommitment.Properties.Probability.Coupling + +/-! +# Structural reduction: a winning break forces a trace collision + +The shared core behind `binding_win_le_trace_collision` and +`extraction_win_le_trace_collision`. Two facts about `OracleComp.run`: + +* **`run_nodup`** — lazy sampling appends a `(d, r)` entry only on a cache + *miss* (`lookup d = none`), so a finished log never lists the same query + input twice: `(log.map Prod.fst).Nodup`. The realized oracle is therefore a + genuine partial function. + +* **`run_mem_log`** — every value a `query d` returns on the run path is the + one recorded for `d` in the finished log (`log.lookup d = some r`). + +Together with a functional log these turn "two accepting authentication paths +to one root from distinct leaves" into an explicit colliding pair. +-/ + +namespace VectorCommitment.Probability + +open OracleComp ROHasher + +variable {spec : OracleSpec} + +/-- `run_bind` phrased for the `>>=` notation produced by do-blocks. -/ +theorem run_bind' {α β} (c : OracleComp spec α) (f : α → OracleComp spec β) + (log : QueryLog spec) : + (c >>= f).run log = (c.run log).bind (fun p => (f p.1).run p.2) := + OracleComp.run_bind c f log + +/-- `run` of `pure` (the do-block return). -/ +@[simp] theorem run_pure {α} (a : α) (log : QueryLog spec) : + (pure a : OracleComp spec α).run log = PMF.pure (a, log) := rfl + +-- --------------------------------------------------------------------------- +-- Encoding injectivity and no-collision ⇒ output-determines-input. +-- --------------------------------------------------------------------------- + +/-- The internal-node encoding is injective in the child list. -/ +theorem encodeNodes_inj {κ : Nat} {c0 c1 : List (List.Vector Bool κ)} + (h : encodeNodes c0 = encodeNodes c1) : c0 = c1 := by + unfold encodeNodes at h + simp only [List.cons.injEq, true_and] at h + exact List.map_injective_iff.mpr vecBytes_injective h + +/-- A cached lookup witnesses a log entry. -/ +theorem mem_of_lookup {κ : Nat} {log : QueryLog (MerkleROSpec κ)} + {d : (MerkleROSpec κ).Domain} {r : (MerkleROSpec κ).Range} + (h : log.lookup d = some r) : (d, r) ∈ log := by + unfold QueryLog.lookup at h + rw [Option.map_eq_some_iff] at h + obtain ⟨e, hfind, hr⟩ := h + have hmem := List.mem_of_find?_eq_some hfind + have hd : e.1 = d := by have := List.find?_some hfind; simpa using this + obtain ⟨e1, e2⟩ := e + simp only at hd hr; subst hd; subst hr; exact hmem + +/-- Under a collision-free log, equal outputs force equal inputs. -/ +theorem lookup_inj_of_no_collision {κ : Nat} {log : QueryLog (MerkleROSpec κ)} + (hnc : ¬ QueryLog.hasCollision log) + {d1 d2 : (MerkleROSpec κ).Domain} {r : (MerkleROSpec κ).Range} + (h1 : log.lookup d1 = some r) (h2 : log.lookup d2 = some r) : d1 = d2 := by + by_contra hne + exact hnc ⟨(d1, r), mem_of_lookup h1, (d2, r), mem_of_lookup h2, hne, rfl⟩ + +-- --------------------------------------------------------------------------- +-- Pure reconstruction-via-log and its injective descent. +-- --------------------------------------------------------------------------- + +/-- Walk the copath using the finished log as the (partial) oracle: at each + level look up the parent digest for the current children; `none` if absent. + Mirrors `ROHasher.walkCopathOracle` post-hoc on the log. -/ +def walkViaLog {κ : Nat} (log : QueryLog (MerkleROSpec κ)) : + Nat → List.Vector Bool κ → List (List.Vector Bool κ) → + Option (List.Vector Bool κ) + | _, acc, [] => some acc + | pos, acc, sib :: rest => + match log.lookup (encodeNodes (if pos % 2 = 1 then [acc, sib] else [sib, acc])) with + | some parent => walkViaLog log ((pos - 1) / 2) parent rest + | none => none + +/-- **No-collision descent.** Under a collision-free log, two `walkViaLog` runs + that reach the same digest `r` from the same position (with equal-length + copaths) must have started from the same accumulator. Contrapositive of the + binding cascade: distinct leaves to one root ⇒ a collision. -/ +theorem walkViaLog_inj {κ : Nat} {log : QueryLog (MerkleROSpec κ)} + (hnc : ¬ QueryLog.hasCollision log) : + ∀ (cp0 cp1 : List (List.Vector Bool κ)) (pos : Nat) + (acc0 acc1 r : List.Vector Bool κ), + cp0.length = cp1.length → + walkViaLog log pos acc0 cp0 = some r → + walkViaLog log pos acc1 cp1 = some r → + acc0 = acc1 := by + intro cp0 + induction cp0 with + | nil => + intro cp1 pos acc0 acc1 r hlen h0 h1 + have hc1 : cp1 = [] := List.length_eq_zero_iff.mp hlen.symm + subst hc1 + simp only [walkViaLog, Option.some.injEq] at h0 h1 + rw [h0, h1] + | cons sib0 rest0 ih => + intro cp1 pos acc0 acc1 r hlen h0 h1 + cases cp1 with + | nil => simp at hlen + | cons sib1 rest1 => + simp only [walkViaLog] at h0 h1 + cases hlk0 : log.lookup (encodeNodes + (if pos % 2 = 1 then [acc0, sib0] else [sib0, acc0])) with + | none => rw [hlk0] at h0; simp at h0 + | some parent0 => + cases hlk1 : log.lookup (encodeNodes + (if pos % 2 = 1 then [acc1, sib1] else [sib1, acc1])) with + | none => rw [hlk1] at h1; simp at h1 + | some parent1 => + rw [hlk0] at h0; rw [hlk1] at h1 + have hlen' : rest0.length = rest1.length := by simpa using hlen + have hpar : parent0 = parent1 := + ih rest1 ((pos - 1) / 2) parent0 parent1 r hlen' h0 h1 + subst hpar + have hdeq := encodeNodes_inj (lookup_inj_of_no_collision hnc hlk0 hlk1) + by_cases hp : pos % 2 = 1 + · simp only [hp, if_true, List.cons.injEq] at hdeq; exact hdeq.1 + · simp only [hp, if_false, List.cons.injEq] at hdeq; exact hdeq.2.1 + +/-- Lazy sampling never re-lists a query input: the finished log's inputs are + `Nodup`, starting from any `Nodup` log. -/ +theorem run_nodup {α} (c : OracleComp spec α) : + ∀ (log : QueryLog spec) p, p ∈ (c.run log).support → + (log.map Prod.fst).Nodup → (p.2.map Prod.fst).Nodup := by + induction c with + | ret a => + intro log p hp hnd + simp only [OracleComp.run_ret, PMF.support_pure, Set.mem_singleton_iff] at hp + subst hp; exact hnd + | call d k ih => + intro log p hp hnd + rw [OracleComp.run] at hp + cases hlk : log.lookup d with + | some r => rw [hlk] at hp; exact ih r log p hp hnd + | none => + rw [hlk] at hp + simp only [PMF.support_bind, Set.mem_iUnion] at hp + obtain ⟨r, _, hpr⟩ := hp + refine ih r (log.append d r) p hpr ?_ + rw [QueryLog.append, List.map_cons, List.nodup_cons] + refine ⟨?_, hnd⟩ + intro hmem + obtain ⟨e, he, hee⟩ := List.mem_map.mp hmem + exact (forall_ne_of_lookup_none hlk e he) hee + +/-- In a functional (input-`Nodup`) log, a membership uniquely fixes the lookup. -/ +theorem lookup_eq_of_mem_nodup {κ : Nat} {log : QueryLog (MerkleROSpec κ)} + {d : (MerkleROSpec κ).Domain} {r : (MerkleROSpec κ).Range} + (hmem : (d, r) ∈ log) (hnd : (log.map Prod.fst).Nodup) : + log.lookup d = some r := by + induction log with + | nil => simp at hmem + | cons e rest ih => + rw [List.map_cons, List.nodup_cons] at hnd + obtain ⟨hnotin, hndrest⟩ := hnd + rw [List.mem_cons] at hmem + show ((e :: rest).find? (fun p => p.fst = d)).map Prod.snd = some r + rw [List.find?_cons] + by_cases he : e.fst = d + · rcases hmem with rfl | hmem + · simp + · exact absurd (he ▸ List.mem_map.mpr ⟨(d, r), hmem, rfl⟩) hnotin + · rcases hmem with rfl | hmem + · exact absurd rfl he + · simp only [he, decide_false] + exact ih hmem hndrest + +/-- `run` only extends the cache, so the starting log is a suffix of every + finished log. -/ +theorem run_suffix {α} (c : OracleComp spec α) : + ∀ (log : QueryLog spec) p, p ∈ (c.run log).support → log <:+ p.2 := by + induction c with + | ret a => + intro log p hp + simp only [OracleComp.run_ret, PMF.support_pure, Set.mem_singleton_iff] at hp + subst hp; exact List.suffix_refl _ + | call d k ih => + intro log p hp + rw [OracleComp.run] at hp + cases hlk : log.lookup d with + | some r => rw [hlk] at hp; exact ih r log p hp + | none => + rw [hlk] at hp + simp only [PMF.support_bind, Set.mem_iUnion] at hp + obtain ⟨r, _, hpr⟩ := hp + exact (List.suffix_cons _ _).trans (ih r (log.append d r) p hpr) + +/-- A single `query d` records `(d, response)` in its finished log. -/ +theorem query_mem_log {κ : Nat} {d : (MerkleROSpec κ).Domain} + {r : (MerkleROSpec κ).Range} {log0 logf : QueryLog (MerkleROSpec κ)} + (h : (r, logf) ∈ ((OracleComp.query d).run log0).support) : (d, r) ∈ logf := by + unfold OracleComp.query at h + rw [OracleComp.run] at h + cases hlk : log0.lookup d with + | some r' => + rw [hlk] at h + simp only [OracleComp.run_ret, PMF.support_pure, Set.mem_singleton_iff, + Prod.mk.injEq] at h + obtain ⟨hr, hlog⟩ := h + subst hr; subst hlog; exact mem_of_lookup hlk + | none => + rw [hlk] at h + simp only [OracleComp.run_ret, PMF.support_bind, Set.mem_iUnion, + PMF.support_pure, Set.mem_singleton_iff, Prod.mk.injEq] at h + obtain ⟨x, _, hr, hlog⟩ := h + subst hr; subst hlog + rw [QueryLog.append]; exact List.mem_cons_self .. + +/-- Support-restricted monotonicity of the PMF outer measure: it suffices that + `s` and `t` agree on the support. -/ +theorem toOuterMeasure_mono_support {α} (p : PMF α) {s t : Set α} + (h : ∀ x ∈ p.support, x ∈ s → x ∈ t) : + p.toOuterMeasure s ≤ p.toOuterMeasure t := by + rw [PMF.toOuterMeasure_apply, PMF.toOuterMeasure_apply] + refine ENNReal.tsum_le_tsum (fun x => ?_) + by_cases hs : x ∈ s + · by_cases hp0 : p x = 0 + · simp [hs, hp0] + · have ht : x ∈ t := h x ((p.mem_support_iff x).mpr hp0) hs + simp [hs, ht] + · simp [hs] + +-- --------------------------------------------------------------------------- +-- The monadic bridge: a finished `reconstructRootOracle`/`checkOracle` run is +-- reproduced by the pure `walkViaLog` on its final log. +-- --------------------------------------------------------------------------- + +/-- A finished `walkCopathOracle` run is reproduced by `walkViaLog` on its final + log (which is functional by `run_nodup`). -/ +theorem walkCopathOracle_run {κ : Nat} : + ∀ (cp : List (List.Vector Bool κ)) (pos : Nat) (acc d : List.Vector Bool κ) + (log0 logf : QueryLog (MerkleROSpec κ)), + (log0.map Prod.fst).Nodup → + (d, logf) ∈ ((walkCopathOracle pos acc cp).run log0).support → + walkViaLog logf pos acc cp = some d := by + intro cp + induction cp with + | nil => + intro pos acc d log0 logf _ hsup + have he : walkCopathOracle pos acc ([] : List (List.Vector Bool κ)) + = OracleComp.ret acc := rfl + rw [he, OracleComp.run_ret] at hsup + simp only [PMF.support_pure, Set.mem_singleton_iff, Prod.mk.injEq] at hsup + obtain ⟨hd, hlog⟩ := hsup + subst hd; subst hlog; rfl + | cons sib rest ih => + intro pos acc d log0 logf hnd hsup + rw [walkCopathOracle, run_bind'] at hsup + simp only [PMF.support_bind, Set.mem_iUnion] at hsup + obtain ⟨⟨parent, log1⟩, hq, hrec⟩ := hsup + have hmem1 : (encodeNodes (if pos % 2 = 1 then [acc, sib] else [sib, acc]), parent) ∈ log1 := + query_mem_log hq + have hnd1 : (log1.map Prod.fst).Nodup := run_nodup _ log0 (parent, log1) hq hnd + have hsuf : log1 <:+ logf := run_suffix _ log1 (d, logf) hrec + have hmemf : (encodeNodes (if pos % 2 = 1 then [acc, sib] else [sib, acc]), parent) ∈ logf := + hsuf.mem hmem1 + have hndf : (logf.map Prod.fst).Nodup := run_nodup _ log1 (d, logf) hrec hnd1 + have hlook : logf.lookup (encodeNodes (if pos % 2 = 1 then [acc, sib] else [sib, acc])) + = some parent := lookup_eq_of_mem_nodup hmemf hndf + have hwrec : walkViaLog logf ((pos - 1) / 2) parent rest = some d := + ih ((pos - 1) / 2) parent d log1 logf hnd1 hrec + rw [walkViaLog, hlook]; exact hwrec + +/-- A finished `reconstructRootOracle` run is reproduced by `walkViaLog` from the + leaf digest, with the leaf query recorded in the final log. -/ +theorem reconstructRootOracle_run {κ : Nat} {n i : Nat} + {value salt : List.Vector Bool κ} {cp : List (List.Vector Bool κ)} + {log0 logf : QueryLog (MerkleROSpec κ)} {d : List.Vector Bool κ} + (hnd : (log0.map Prod.fst).Nodup) + (hsup : (d, logf) ∈ ((reconstructRootOracle n i value salt cp).run log0).support) : + ∃ leaf : List.Vector Bool κ, + (encodeLeaf value salt, leaf) ∈ logf ∧ + walkViaLog logf (n - 1 + i) leaf cp = some d := by + rw [reconstructRootOracle, run_bind'] at hsup + simp only [PMF.support_bind, Set.mem_iUnion] at hsup + obtain ⟨⟨leaf, log1⟩, hq, hrec⟩ := hsup + refine ⟨leaf, ?_, ?_⟩ + · exact (run_suffix _ log1 (d, logf) hrec).mem (query_mem_log hq) + · exact walkCopathOracle_run cp (n - 1 + i) leaf d log1 logf + (run_nodup _ log0 (leaf, log1) hq hnd) hrec + +/-- A singleton `checkOracle` that accepts pins the opening proof to one entry + `(salt, copath)` of depth `⌊log₂ n⌋` whose `reconstructRootOracle` produced + exactly `root`. -/ +theorem checkOracle_singleton_accept {κ : Nat} {n i : Nat} + {root v : List.Vector Bool κ} {pf : OpeningProof (ROHasher.ROHasherValue κ)} + {log0 logf : QueryLog (MerkleROSpec κ)} + (h : (true, logf) ∈ ((checkOracle n root + { indices := [i], values := [v] } pf).run log0).support) : + ∃ s cp, pf.entries = [(s, cp)] ∧ cp.length = PerfectBinary.log2Floor n ∧ + (root, logf) ∈ ((reconstructRootOracle n i v s cp).run log0).support := by + unfold checkOracle at h + split at h + · -- length guard tripped ⇒ the run is `pure false`, contradicting the `true` outcome + simp only [run_pure, PMF.support_pure, Set.mem_singleton_iff, Prod.mk.injEq] at h + exact absurd h.1 (by decide) + · -- guard passed ⇒ the proof has exactly one entry + rename_i hcond + simp only [List.length_singleton, ne_eq, not_or, not_not] at hcond + obtain ⟨e, he⟩ := List.length_eq_one_iff.mp hcond.2.symm + rw [he] at h + simp only [List.zip_cons_cons, List.zip_nil_right, List.foldlM_cons, List.foldlM_nil, + Bool.true_and] at h + rw [run_bind'] at h + simp only [PMF.support_bind, Set.mem_iUnion] at h + obtain ⟨⟨b', log1⟩, h1, h2⟩ := h + simp only [run_pure, PMF.support_pure, Set.mem_singleton_iff, Prod.mk.injEq] at h2 + obtain ⟨hb, hl⟩ := h2; subst hb; subst hl + rw [run_bind'] at h1 + simp only [PMF.support_bind, Set.mem_iUnion] at h1 + obtain ⟨⟨r, log2⟩, hr, hres⟩ := h1 + simp only [run_pure, PMF.support_pure, Set.mem_singleton_iff, Prod.mk.injEq] at hres + obtain ⟨hval, hl2⟩ := hres + rw [eq_comm, Bool.and_eq_true] at hval + obtain ⟨hroot, hlen⟩ := hval + subst hl2 + exact ⟨e.1, e.2, he, of_decide_eq_true hlen, of_decide_eq_true hroot ▸ hr⟩ + +/-- `walkViaLog` is monotone under (functional) log extension: a reconstruction + that succeeds on a suffix still succeeds on the whole log. -/ +theorem walkViaLog_mono {κ : Nat} {log1 logf : QueryLog (MerkleROSpec κ)} + (hsuf : log1 <:+ logf) (hndf : (logf.map Prod.fst).Nodup) : + ∀ (cp : List (List.Vector Bool κ)) (pos : Nat) (acc r : List.Vector Bool κ), + walkViaLog log1 pos acc cp = some r → walkViaLog logf pos acc cp = some r := by + intro cp + induction cp with + | nil => intro pos acc r h; simpa [walkViaLog] using h + | cons sib rest ih => + intro pos acc r h + rw [walkViaLog] at h ⊢ + cases hlk1 : log1.lookup (encodeNodes (if pos % 2 = 1 then [acc, sib] else [sib, acc])) with + | none => rw [hlk1] at h; simp at h + | some parent => + rw [hlk1] at h + rw [lookup_eq_of_mem_nodup (hsuf.mem (mem_of_lookup hlk1)) hndf] + exact ih ((pos - 1) / 2) parent r h + +/-- **Core uniqueness lemma.** Under a collision-free trace, two accepted + openings of the same `root` at the same index `i` (equal-depth copaths) must + reveal the same value. Both ROM bounds derive a collision from its + contrapositive. -/ +theorem accepted_value_unique {κ : Nat} {n i : Nat} + {root v0 v1 s0 s1 : List.Vector Bool κ} {cp0 cp1 : List (List.Vector Bool κ)} + {log0 log1 logf : QueryLog (MerkleROSpec κ)} + (hnd : (log0.map Prod.fst).Nodup) + (hlen : cp0.length = cp1.length) + (hnc : ¬ QueryLog.hasCollision logf) + (h0 : (root, log1) ∈ ((reconstructRootOracle n i v0 s0 cp0).run log0).support) + (h1 : (root, logf) ∈ ((reconstructRootOracle n i v1 s1 cp1).run log1).support) : + v0 = v1 := by + have hnd1 : (log1.map Prod.fst).Nodup := run_nodup _ log0 (root, log1) h0 hnd + have hndf : (logf.map Prod.fst).Nodup := run_nodup _ log1 (root, logf) h1 hnd1 + obtain ⟨leaf0, hmem0, hwalk0⟩ := reconstructRootOracle_run hnd h0 + obtain ⟨leaf1, hmem1, hwalk1⟩ := reconstructRootOracle_run hnd1 h1 + have hsuf : log1 <:+ logf := run_suffix _ log1 (root, logf) h1 + have hwalk0f : walkViaLog logf (n - 1 + i) leaf0 cp0 = some root := + walkViaLog_mono hsuf hndf cp0 (n - 1 + i) leaf0 root hwalk0 + have hleaf : leaf0 = leaf1 := + walkViaLog_inj hnc cp0 cp1 (n - 1 + i) leaf0 leaf1 root hlen hwalk0f hwalk1 + have hmem0f : (encodeLeaf v0 s0, leaf1) ∈ logf := hleaf ▸ hsuf.mem hmem0 + have heq : encodeLeaf v0 s0 = encodeLeaf v1 s1 := + lookup_inj_of_no_collision hnc + (lookup_eq_of_mem_nodup hmem0f hndf) (lookup_eq_of_mem_nodup hmem1 hndf) + exact (encodeLeaf_inj heq).1 + +end VectorCommitment.Probability From 42a003fe020643d4f434255cf54f2d78c490b05b Mon Sep 17 00:00:00 2001 From: ajhavlin Date: Sat, 6 Jun 2026 15:48:25 +0200 Subject: [PATCH 06/17] VectorCommitment: checkOracle acceptance lemmas --- .../Properties/Probability/CheckOracle.lean | 119 ++++++++++++++++++ 1 file changed, 119 insertions(+) create mode 100644 VectorCommitment/Properties/Probability/CheckOracle.lean diff --git a/VectorCommitment/Properties/Probability/CheckOracle.lean b/VectorCommitment/Properties/Probability/CheckOracle.lean new file mode 100644 index 0000000..9b430c7 --- /dev/null +++ b/VectorCommitment/Properties/Probability/CheckOracle.lean @@ -0,0 +1,119 @@ +/- +Copyright (c) 2026 LeanStuff contributors. All rights reserved. +-/ +import VectorCommitment.Properties.Probability.ROHasher +import VectorCommitment.Src.Merkle.Scheme + +/-! +# `Verify^H` as an oracle computation, and the straightline cache extractor + +The **shared-oracle** form of Merkle verification: instead of calling a stored +hasher, it recomputes the root by *querying* the lazily-sampled random oracle, +mirroring `MerkleCommitment.reconstructRoot` / `MerkleCommitment.check` with +`query (encode…)` in place of `hashLeaf` / `hashNodes`. The ROM security +experiments validate an adversary's break against the *same* `H` it queried, so +the winning event cannot be decoupled from the oracle. + +`cacheExtract` is the dual straightline extractor: it reads the finished +`QueryLog` and walks the digest tree top-down to recover the committed leaf. +-/ + +namespace ROHasher + +open OracleComp + +/-- Walk the bottom-up copath, querying the oracle for each internal node. + Mirrors `MerkleCommitment.walkCopath` / `combineUp`: at `pos` the + accumulator is the left child iff `pos` is odd. -/ +noncomputable def walkCopathOracle {κ : Nat} : + Nat → List.Vector Bool κ → List (List.Vector Bool κ) → + OracleComp (MerkleROSpec κ) (List.Vector Bool κ) + | _, acc, [] => pure acc + | pos, acc, sib :: rest => do + let children := if pos % 2 = 1 then [acc, sib] else [sib, acc] + let parent ← query (encodeNodes children) + walkCopathOracle ((pos - 1) / 2) parent rest + +/-- Reconstruct a root from one `(i, value, salt, copath)` by querying the + shared oracle. Mirrors `MerkleCommitment.reconstructRoot` (leaf vertex + `n - 1 + i` for an `n`-leaf tree). -/ +noncomputable def reconstructRootOracle {κ : Nat} (n i : Nat) + (value salt : List.Vector Bool κ) (copath : List (List.Vector Bool κ)) : + OracleComp (MerkleROSpec κ) (List.Vector Bool κ) := do + let leaf ← query (encodeLeaf value salt) + walkCopathOracle (n - 1 + i) leaf copath + +/-- `Verify^H` for a Merkle opening of an `n`-leaf tree: every + `(index, value, entry)` triple must reconstruct, via shared-oracle queries, + to `root`. Mirrors `MerkleCommitment.check`. -/ +noncomputable def checkOracle {κ : Nat} (n : Nat) (root : List.Vector Bool κ) + (op : Opening (ROHasherValue κ)) (pf : OpeningProof (ROHasherValue κ)) : + OracleComp (MerkleROSpec κ) Bool := + if op.indices.length ≠ op.values.length ∨ op.indices.length ≠ pf.entries.length then + pure false + else + ((op.indices.zip op.values).zip pf.entries).foldlM + (fun acc triple => do + let ((i, value), (salt, copath)) := triple + let r ← reconstructRootOracle n i value salt copath + pure (acc && decide (r = root) && decide (copath.length = PerfectBinary.log2Floor n))) + true + +-- --------------------------------------------------------------------------- +-- Straightline cache extractor: read the finished QueryLog top-down. +-- --------------------------------------------------------------------------- + +/-- Decode one serialized child digest (`κ` bytes, each `0`/`1`) back to a + bit-vector — inverse of the per-child serialization in `encodeNodes`. -/ +def decodeDigest {κ : Nat} (b : ByteArray) : Option (List.Vector Bool κ) := + let bits : List Bool := b.toList.map (fun byte => decide (byte = 1)) + if h : bits.length = κ then some ⟨bits, h⟩ else none + +/-- Parse a query input as an internal-node query: NODE tag, then each + remaining byte array decodes to a child digest. -/ +def decodeNodeInput {κ : Nat} (input : List ByteArray) : + Option (List (List.Vector Bool κ)) := + match input with + | tag :: rest => if tag == Tag.node then rest.mapM decodeDigest else none + | [] => none + +/-- Root→leaf child choices (`0` = left, `1` = right) for message index `i` in + an `n`-leaf tree over `depth` levels. -/ +def descentChoices (n i depth : Nat) : List Nat := + let rec go (v : Nat) (fuel : Nat) (acc : List Nat) : List Nat := + match fuel with + | 0 => acc + | Nat.succ f => + if v = 0 then acc + else go ((v - 1) / 2) f ((if v % 2 = 1 then 0 else 1) :: acc) + go (n - 1 + i) depth [] + +/-- Descend the cached digest tree following `choices`, returning the leaf + query's (tagged) input. `none` if a required digest is absent or a node + fails to decode. -/ +def cacheExtractAux {κ : Nat} (log : QueryLog (MerkleROSpec κ)) + (digest : List.Vector Bool κ) (choices : List Nat) : Option (List ByteArray) := + let entries : List ((MerkleROSpec κ).Domain × (MerkleROSpec κ).Range) := log + match entries.find? (fun e => decide (e.2 = digest)) with + | none => none + | some e => + match choices with + | [] => some e.1 + | c :: rest => + match decodeNodeInput e.1 with + | some children => + match children[c]? with + | some child => cacheExtractAux log child rest + | none => none + | none => none +termination_by choices.length +decreasing_by simp_wf + +/-- **Straightline cache extractor** for an `n`-leaf Merkle tree: walk the query + log from `root` toward leaf message-index `i`, returning the committed leaf + input (or `none`). The descent length is the tree depth `⌊log₂ n⌋`. -/ +def cacheExtract {κ : Nat} (log : QueryLog (MerkleROSpec κ)) + (root : List.Vector Bool κ) (n i : Nat) : Option (List ByteArray) := + cacheExtractAux log root (descentChoices n i (PerfectBinary.log2Floor n)) + +end ROHasher From 1efce224632b828e672b73269659a526fdb6ba65 Mon Sep 17 00:00:00 2001 From: ajhavlin Date: Sat, 6 Jun 2026 15:48:27 +0200 Subject: [PATCH 07/17] VectorCommitment: close ROM position binding --- .../Probability/Instances/BindingROM.lean | 160 ++++++++++++------ 1 file changed, 110 insertions(+), 50 deletions(-) diff --git a/VectorCommitment/Properties/Probability/Instances/BindingROM.lean b/VectorCommitment/Properties/Probability/Instances/BindingROM.lean index 4c2b0d2..bbb37bf 100644 --- a/VectorCommitment/Properties/Probability/Instances/BindingROM.lean +++ b/VectorCommitment/Properties/Probability/Instances/BindingROM.lean @@ -5,72 +5,132 @@ import VectorCommitment.Src.Security.PositionBinding import VectorCommitment.Src.Merkle.Instance import VectorCommitment.Properties.Probability.ROHasher import VectorCommitment.Properties.Probability.Collision +import VectorCommitment.Properties.Probability.CheckOracle +import VectorCommitment.Properties.Probability.Coupling +import VectorCommitment.Properties.Probability.TraceCollision import VectorCommitment.Properties.Theorems.Binding /-! # ROM instance: position binding for RO-derived Merkle commitments Discharges `HasPositionBinding (MerkleCommitment (ROHasherValue κ) S)` -for every digest length `κ` and Merkle shape `S`, in the random-oracle -model. - -## Reduction sketch - -The bound `q · (q - 1) / 2^(κ + 1)` is derived in three steps: - -1. **Bad-event decomposition.** A valid binding break implies *either* - the RO had a collision among the queries made during the experiment, - *or* the break exists under collision-free hashing. - -2. **Collision case.** Probability bounded by - `Probability.birthdayBound_kappa` from `Collision.lean`. - -3. **Structural case.** Impossible by the Option-B - [`mt_binding`](../../Theorems/Binding.lean) theorem: under - `Function.Injective2 hashLeaf` and `Function.Injective hashNodes`, - no two distinct accepting openings of the same position exist. - -The two `sorry`s below — `bindingAdvantage` and `binding_bound` — -implement this reduction; closing them (modulo `birthdayBound`) gives -a complete ROM proof of position binding. - -## Open work for the student - -* **`bindingAdvantage`**: define the probability the adversary, when - run from the empty query log, produces a `BindingBreak` valid against - the verifier key derived from the sampled oracle. The shape: - - bindingAdvantage A := - (OracleComp.simulateQ A).toOuterMeasure - {b : BindingBreak _ | b.IsValid vk_derived_from_oracle} - - Open question: how to derive `vk` from the oracle. One choice is to - bake `setup` / `trim` into the experiment monadically; another is to - parametrize the instance over a default `vk`. Discuss with the - maintainer before committing. - -* **`binding_bound`**: discharge the reduction sketch above. The - collision case invokes - `Probability.birthdayBound_kappa κ q (R := List.Vector Bool κ) (by simp)`; - the structural case invokes `mt_binding` after extracting injectivity - on the queried inputs from "no RO collision in the trace." +for every digest length `κ` and Merkle shape `S`, in the random-oracle model. + +## The experiment (shared oracle) + +`bindingAdvantage` runs the adversary and validates its claimed break by +re-verifying *both* openings with `ROHasher.checkOracle` (`Verify^H`) against +the **same** lazily-sampled oracle the adversary queried. The advantage is the +probability the experiment returns `true` (distinct values, both openings +verify) — pinned to a real game, never a free quantity. + +## Reduction (two steps) + +``` +Pr[A wins] + ≤ Pr[trace has a collision] [binding_win_le_trace_collision — structural] + ≤ collisionBound κ q [coupling_trace_le_collisionBound — proved] +``` + +**Step 2** is `coupling_trace_le_collisionBound` (`Coupling.lean`, +machine-checked). **Step 1** is the structural fact that a winning break with a +*collision-free* trace is impossible: under an injective realized hash the two +accepting paths to the same root force `value₀ = value₁` (the deterministic +spine `mt_binding`, `Theorems/Binding.lean`, is fully proved). Lifting +`mt_binding` from "globally injective hasher" to "injective on the query log" +across the `OracleComp` monad is isolated as `binding_win_le_trace_collision`. -/ namespace VectorCommitment.Probability.Instances -open VectorCommitment.Security +open VectorCommitment.Security VectorCommitment.Probability +open scoped Classical variable (κ : Nat) (S : Type) [MerkleShape S] [Nonempty (MerkleCommitment (ROHasher.ROHasherValue κ) S)] -/-- Position binding for the RO-derived Merkle commitment. -/ +/-- The inner experiment: run the adversary, then re-verify both openings with + `checkOracle` against the shared oracle; win on distinct values with both + accepting. `n` is the leaf count of the scheme's (public) tree shape. -/ +private noncomputable def bindingInner + (A : OracleComp (ROHasher.MerkleROSpec κ) + (BindingBreak (MerkleCommitment (ROHasher.ROHasherValue κ) S))) : + OracleComp (ROHasher.MerkleROSpec κ) Bool := + let n := MerkleShape.numLeaves + (Classical.ofNonempty : MerkleCommitment (ROHasher.ROHasherValue κ) S).shape + do + let b ← A + let r₀ ← ROHasher.checkOracle n b.commitment.root + { indices := [b.index], values := [b.value₀] } b.proof₀ + let r₁ ← ROHasher.checkOracle n b.commitment.root + { indices := [b.index], values := [b.value₁] } b.proof₁ + pure (decide (b.value₀ ≠ b.value₁) && r₀ && r₁) + +/-- **Step 1 (structural).** A winning outcome has a colliding trace. + + If both `checkOracle` calls accept with `value₀ ≠ value₁`, the two + authentication paths reconstruct the same root from distinct leaves; were + the trace collision-free, `accepted_value_unique` would force + `value₀ = value₁` — contradiction. -/ +private lemma binding_win_le_trace_collision + (A : OracleComp (ROHasher.MerkleROSpec κ) + (BindingBreak (MerkleCommitment (ROHasher.ROHasherValue κ) S))) : + ((bindingInner κ S A).run QueryLog.empty).toOuterMeasure {p | p.1 = true} + ≤ ((bindingInner κ S A).run QueryLog.empty).toOuterMeasure + {p | QueryLog.hasCollision p.2} := by + apply toOuterMeasure_mono_support + rintro ⟨bout, logf⟩ hsupp hwin + simp only [Set.mem_setOf_eq] at hwin ⊢ + by_contra hnc + rw [bindingInner, run_bind'] at hsupp + simp only [PMF.support_bind, Set.mem_iUnion] at hsupp + obtain ⟨⟨b, logA⟩, hA, hsupp⟩ := hsupp + rw [run_bind'] at hsupp + simp only [PMF.support_bind, Set.mem_iUnion] at hsupp + obtain ⟨⟨r0, log1⟩, hc0, hsupp⟩ := hsupp + rw [run_bind'] at hsupp + simp only [PMF.support_bind, Set.mem_iUnion] at hsupp + obtain ⟨⟨r1, log2⟩, hc1, hsupp⟩ := hsupp + rw [run_pure, PMF.support_pure, Set.mem_singleton_iff] at hsupp + obtain ⟨hbeq, hlogeq⟩ := Prod.ext_iff.mp hsupp + subst hlogeq + rw [hwin, eq_comm, Bool.and_eq_true, Bool.and_eq_true] at hbeq + obtain ⟨⟨hne, hr0⟩, hr1⟩ := hbeq + subst hr0; subst hr1 + obtain ⟨s0, cp0, _, hlen0, hrec0⟩ := checkOracle_singleton_accept hc0 + obtain ⟨s1, cp1, _, hlen1, hrec1⟩ := checkOracle_singleton_accept hc1 + have hndA : (logA.map Prod.fst).Nodup := + run_nodup _ QueryLog.empty (b, logA) hA (by simp [QueryLog.empty]) + have hne' : b.value₀ ≠ b.value₁ := by simpa using hne + exact absurd (accepted_value_unique hndA (hlen0.trans hlen1.symm) hnc hrec0 hrec1) hne' + +/-- Position binding for the RO-derived Merkle commitment. + + The adversary at budget `q` is a `q`-query-bounded oracle computation: the + subtype carries the proof that the *whole* experiment (adversary plus the + bounded `checkOracle` verification) stays within `q` distinct oracle + queries, so the birthday bound applies. No budget `sorry` is incurred. -/ noncomputable instance : HasPositionBinding (MerkleCommitment (ROHasher.ROHasherValue κ) S) where - BindingAdversary := fun _ _ => - OracleComp (ROHasher.MerkleROSpec κ) - (BindingBreak (MerkleCommitment (ROHasher.ROHasherValue κ) S)) - bindingAdvantage := sorry + BindingAdversary := fun _ q => + { A : OracleComp (ROHasher.MerkleROSpec κ) + (BindingBreak (MerkleCommitment (ROHasher.ROHasherValue κ) S)) // + OracleComp.QueryBudget (bindingInner κ S A) q } + -- Shared-oracle game: validate the break with `checkOracle` against the + -- same oracle the adversary queried (the advantage is a real win-probability). + bindingAdvantage := fun {_ _} A => OracleComp.simulateQ (bindingInner κ S A.1) true bindingError := fun _ q => Probability.collisionBound κ q - binding_bound := sorry + -- win ≤ trace-collision ≤ collisionBound. + binding_bound := by + intro _ q A + show OracleComp.simulateQ (bindingInner κ S A.1) true ≤ Probability.collisionBound κ q + simp only [OracleComp.simulateQ] + rw [← PMF.toOuterMeasure_apply_singleton, PMF.toOuterMeasure_map_apply] + have Hpre : (Prod.fst ⁻¹' ({true} : Set Bool)) = + {p : Bool × QueryLog (ROHasher.MerkleROSpec κ) | p.1 = true} := by + ext ⟨b, _⟩; simp + rw [Hpre] + exact (binding_win_le_trace_collision κ S A.1).trans + (coupling_trace_le_collisionBound (bindingInner κ S A.1) q A.2) end VectorCommitment.Probability.Instances From 319aa2ad4a5bc0613cd9694c689d5f9db2ee5f9c Mon Sep 17 00:00:00 2001 From: ajhavlin Date: Sat, 6 Jun 2026 15:48:28 +0200 Subject: [PATCH 08/17] VectorCommitment: ROM extractability via cache extractor --- .../Instances/ExtractabilityROM.lean | 148 ++++++++++++------ 1 file changed, 102 insertions(+), 46 deletions(-) diff --git a/VectorCommitment/Properties/Probability/Instances/ExtractabilityROM.lean b/VectorCommitment/Properties/Probability/Instances/ExtractabilityROM.lean index df91691..20fe3b9 100644 --- a/VectorCommitment/Properties/Probability/Instances/ExtractabilityROM.lean +++ b/VectorCommitment/Properties/Probability/Instances/ExtractabilityROM.lean @@ -5,71 +5,127 @@ import VectorCommitment.Src.Security.Extractability import VectorCommitment.Src.Merkle.Instance import VectorCommitment.Properties.Probability.ROHasher import VectorCommitment.Properties.Probability.Collision +import VectorCommitment.Properties.Probability.CheckOracle +import VectorCommitment.Properties.Probability.Coupling import VectorCommitment.Properties.Theorems.Extractability /-! # ROM instance: straightline extractability for RO-derived Merkle commitments -Discharges `HasStraightlineExtractor (MerkleCommitment (ROHasherValue κ) S)` -for every digest length `κ` and Merkle shape `S`, in the random-oracle -model. +Discharges `HasStraightlineExtractor (MerkleCommitment (ROHasherValue κ) S)` in +the random-oracle model. The straightline extractor `ROHasher.cacheExtract` +reads the finished query log and walks the digest tree from the committed root +down to the requested leaf. -## What straightline extractability adds over binding +## The experiment -Binding gives a *partial* function on opened positions; extractability -upgrades this to a *total* string `m̃` fixed before any opening — what -IOP/PCP soundness reductions actually need (per -[eprint 2024/1434, Theorem 5.1]). +`extractionFailureAdvantage` runs the adversary, re-verifies its opening with +`ROHasher.checkOracle` (`Verify^H`) against the shared oracle, and — reading the +*finished* log — flags a **failure** when the opening verifies yet some opened +index's claimed leaf disagrees with the one `cacheExtract` recovers. (Because +the extractor reads the final trace, no in-computation log access is needed.) -In the ROM, the straightline extractor reads the `QueryLog` -(`Properties/Probability/RandomOracle.lean`): given a committed root, -walk the cache to find the query whose response is the root, recurse on -its children, and so on. Any subtree the prover never queried becomes -"⊥", and the prover cannot open into it without finding a hash -collision. +## Reduction (two steps) -## Reduction sketch +``` +Pr[extraction fails] + ≤ Pr[trace has a collision] [extraction_win_le_trace_collision — structural] + ≤ collisionBound κ q [coupling_trace_le_collisionBound — proved] +``` -Same shape as binding: - -1. Bad-event decomposition: extraction failure ⇒ collision OR - structural-extractability violation. -2. Collision case bounded by `Probability.birthdayBound_kappa`. -3. Structural case ruled out by `mt_multi_extractability` from - `Properties/Theorems/Extractability.lean` (under - collision-free hashes the extractor's output uniquely determines - `m̃`). - -## Open work for the student - -* **`extractionFailureAdvantage`**: define the probability that the - adversary produces an accepting opening at some index `i` whose - revealed value disagrees with the value the straightline extractor - outputs for `i`, given the adversary's RO trace. Requires defining - the extractor itself — a function `QueryLog → Commitment → Index → - Option Alphabet` that walks the cache. - -* **`extraction_bound`**: discharge the reduction sketch. Same - collision bound as binding (`q · (q - 1) / 2^(κ + 1)`); the structural - case invokes `mt_multi_extractability`. +**Step 2** is machine-checked (`Coupling.lean`). **Step 1** is the structural +fact that a verified-but-mis-extracted opening forces two distinct accepting +authentication paths to the same root — impossible under a collision-free +trace by `mt_multi_extractability` (`Theorems/Extractability.lean`, proved). The +monad-level transport is isolated as `extraction_win_le_trace_collision`. -/ namespace VectorCommitment.Probability.Instances +open VectorCommitment.Probability +open scoped Classical + variable (κ : Nat) (S : Type) [MerkleShape S] [Nonempty (MerkleCommitment (ROHasher.ROHasherValue κ) S)] -/-- Straightline extractability for the RO-derived Merkle commitment. -/ +/-- The adversary's output: a commitment, a multi-index opening request, and a + proof. -/ +private abbrev ExtractBreak := + Committed (ROHasher.ROHasherValue κ) S × List Nat × + List (List.Vector Bool κ) × OpeningProof (ROHasher.ROHasherValue κ) + +/-- Leaf count of the scheme's (public) tree shape. -/ +private noncomputable def nLeaves : Nat := + MerkleShape.numLeaves + (Classical.ofNonempty : MerkleCommitment (ROHasher.ROHasherValue κ) S).shape + +/-- The straightline-extraction failure flag, a pure function of the adversary's + output and the finished trace: some opened index whose claimed leaf input + disagrees with what `cacheExtract` recovers under the committed root. -/ +private noncomputable def extractMismatch (br : ExtractBreak κ S) + (log : QueryLog (ROHasher.MerkleROSpec κ)) : Bool := + ((br.2.1.zip br.2.2.1).zip br.2.2.2.entries).any (fun triple => + let ((i, value), (salt, _)) := triple + !(ROHasher.cacheExtract log br.1.root (nLeaves κ S) i + == some (ROHasher.encodeLeaf value salt))) + +/-- The inner experiment: run the adversary, re-verify with `checkOracle`, and + return the break together with the verifier's verdict. The extraction + failure is read off the finished run by `extractMismatch`. -/ +private noncomputable def extractInner + (A : OracleComp (ROHasher.MerkleROSpec κ) (ExtractBreak κ S)) : + OracleComp (ROHasher.MerkleROSpec κ) (ExtractBreak κ S × Bool) := + do + let br ← A + let r ← ROHasher.checkOracle (nLeaves κ S) br.1.root + { indices := br.2.1, values := br.2.2.1 } br.2.2.2 + pure (br, r) + +/-- **Step 1 (structural).** A failure outcome has a colliding trace. + + A verified opening (`checkOracle` accepts) whose claimed leaf differs from + the cache-extracted one yields two accepting authentication paths to the + same root; under a collision-free trace `accepted_value_unique` + (`TraceCollision.lean`, proved) forces them equal — contradiction. + + **Status: reduced to ONE isolated bridge lemma, `cacheExtract_sound`** + (not yet formalized): under a collision-free, functional log, an accepting + `checkOracle` opening at `i` implies + `cacheExtract log root n i = some (encodeLeaf value salt)` (the top-down + extractor recovers the proof's leaf). Its three pieces are the + `decodeDigest`/`decodeNodeInput` round-trips (inverse of `vecBytes`), + `find?`-by-output uniqueness (collision-free ⇒ outputs injective), and the + `descentChoices`(root→leaf) ↔ `walkCopath`(leaf→root) parity alignment. + Given `cacheExtract_sound`, this lemma closes via `accepted_value_unique` + exactly as `binding_win_le_trace_collision` does. -/ +private lemma extraction_win_le_trace_collision + (A : OracleComp (ROHasher.MerkleROSpec κ) (ExtractBreak κ S)) : + ((extractInner κ S A).run QueryLog.empty).toOuterMeasure + {p | p.1.2 = true ∧ extractMismatch κ S p.1.1 p.2 = true} + ≤ ((extractInner κ S A).run QueryLog.empty).toOuterMeasure + {p | QueryLog.hasCollision p.2} := by + sorry + +/-- Straightline extractability for the RO-derived Merkle commitment. + + As with binding, the adversary at budget `q` is a `q`-query-bounded oracle + computation (subtype carrying the budget proof for the whole experiment), so + no budget `sorry` is incurred. -/ noncomputable instance : HasStraightlineExtractor (MerkleCommitment (ROHasher.ROHasherValue κ) S) where - ExtractionAdversary := fun _ _ => - OracleComp (ROHasher.MerkleROSpec κ) - (VectorCommitment.Commitment (MerkleCommitment (ROHasher.ROHasherValue κ) S) × - List (VectorCommitment.Index (MerkleCommitment (ROHasher.ROHasherValue κ) S)) × - List (VectorCommitment.Alphabet (MerkleCommitment (ROHasher.ROHasherValue κ) S)) × - VectorCommitment.Proof (MerkleCommitment (ROHasher.ROHasherValue κ) S)) - extractionFailureAdvantage := sorry + ExtractionAdversary := fun _ q => + { A : OracleComp (ROHasher.MerkleROSpec κ) (ExtractBreak κ S) // + OracleComp.QueryBudget (extractInner κ S A) q } + -- Shared-oracle game: verdict by `checkOracle`, failure by post-hoc + -- `cacheExtract` on the finished trace (a real win-probability). + extractionFailureAdvantage := fun {_ _} A => + ((extractInner κ S A.1).run QueryLog.empty).toOuterMeasure + {p | p.1.2 = true ∧ extractMismatch κ S p.1.1 p.2 = true} extractionError := fun _ q => Probability.collisionBound κ q - extraction_bound := sorry + -- failure ≤ trace-collision ≤ collisionBound. + extraction_bound := by + intro _ q A + exact (extraction_win_le_trace_collision κ S A.1).trans + (coupling_trace_le_collisionBound (extractInner κ S A.1) q A.2) end VectorCommitment.Probability.Instances From e230aaaf792055412cd04b89c7335cdfa4fd3447 Mon Sep 17 00:00:00 2001 From: ajhavlin Date: Sat, 6 Jun 2026 16:16:58 +0200 Subject: [PATCH 09/17] VectorCommitment: hasher params and binding instantiation capstone --- VectorCommitment/Properties.lean | 1 + .../Probability/Instances/Parameters.lean | 170 ++++++++++++++++++ 2 files changed, 171 insertions(+) create mode 100755 VectorCommitment/Properties/Probability/Instances/Parameters.lean diff --git a/VectorCommitment/Properties.lean b/VectorCommitment/Properties.lean index 99809c8..d97e9b0 100644 --- a/VectorCommitment/Properties.lean +++ b/VectorCommitment/Properties.lean @@ -2,6 +2,7 @@ import VectorCommitment.Properties.Probability.RandomOracle import VectorCommitment.Properties.Probability.ROHasher import VectorCommitment.Properties.Probability.Collision import VectorCommitment.Properties.Probability.Instances.BindingROM +import VectorCommitment.Properties.Probability.Instances.Parameters import VectorCommitment.Properties.Probability.Instances.ExtractabilityROM import VectorCommitment.Properties.Probability.Instances.HidingROM import VectorCommitment.Properties.Probability.Instances.EquivocationROM diff --git a/VectorCommitment/Properties/Probability/Instances/Parameters.lean b/VectorCommitment/Properties/Probability/Instances/Parameters.lean new file mode 100755 index 0000000..811ac89 --- /dev/null +++ b/VectorCommitment/Properties/Probability/Instances/Parameters.lean @@ -0,0 +1,170 @@ +/- +Copyright (c) 2026 LeanStuff contributors. All rights reserved. +-/ +import VectorCommitment.Properties.Probability.Instances.BindingROM +import Mathlib.Data.ENNReal.Basic + +/-! +# Hasher instantiation capstone + +Choose a field, a security level `λ`, and a query budget `q_H`; +get back a machine-checked theorem that the resulting Merkle commitment +is `λ`-bit position binding. + +## The chain + +``` +Pr[binding failure] + ≤ Pr[trace collision] [binding_win_le_trace_collision, BindingROM] + ≤ collisionBound κ q [coupling_trace_le_collisionBound, Coupling] + ≤ 2^(-λ) [collisionBound_le_inv_pow, THIS FILE] +``` + +The three layers combine in `instantiation_binding_secure`. `babyBear_binding_secure` +is the one-liner specialization that puts concrete BabyBear/KoalaBear/M31 numbers in. +-/ + +open VectorCommitment.Probability + +namespace VectorCommitment.Probability.Instances + +open scoped ENNReal + +/-- Ceiling division: `ceilDiv a b = ⌈a / b⌉` (with convention `ceilDiv a 0 = 0`). -/ +def ceilDiv (a b : Nat) : Nat := (a + b - 1) / b + +theorem le_mul_ceilDiv (a b : Nat) (hb : 0 < b) : a ≤ b * ceilDiv a b := by + unfold ceilDiv + have hdm := Nat.div_add_mod (a + b - 1) b + have hmod := Nat.mod_lt (a + b - 1) hb + omega + +/-- The parameter record a developer selects when choosing a hasher. + Fields correspond one-to-one with the audit slide symbols. -/ +structure MerkleHasherParams where + fieldBits : Nat -- ⌊log₂ |F|⌋ — conservative field-element bit count + digestElems : Nat -- D — field elements per digest + saltElems : Nat -- k — field elements for per-leaf salt (hiding axis) + saltBytes : Nat -- S — bytes for per-leaf salt in byte-oriented hashers + lam : Nat -- λ — target security level in bits + qBits : Nat -- q_H — query budget exponent (≤ 2^q_H queries) + +namespace MerkleHasherParams + +/-- Realized digest bit-length: κ = fieldBits × digestElems. -/ +def kappa (p : MerkleHasherParams) : Nat := p.fieldBits * p.digestElems + +/-- The standalone-binding sizing rule: the digest must absorb λ + 1 + 2·q_H bits of slack. + Decidable, so it can be checked by `native_decide` for any concrete parameters. -/ +def MeetsBindingTarget (p : MerkleHasherParams) : Prop := + p.lam + 1 + 2 * p.qBits ≤ p.kappa + +instance (p : MerkleHasherParams) : Decidable (MeetsBindingTarget p) := + inferInstanceAs (Decidable (_ ≤ _)) + +/-- Compute the correct parameters from a field description and security goals: + `D = ⌈(λ+1+2·q_H)/fieldBits⌉`, `k = ⌈λ/fieldBits⌉`, `S = ⌈λ/8⌉`. -/ +def ofField (fieldBits lam qBits : Nat) : MerkleHasherParams where + fieldBits := fieldBits + digestElems := ceilDiv (lam + 1 + 2 * qBits) fieldBits + saltElems := ceilDiv lam fieldBits + saltBytes := ceilDiv lam 8 + lam := lam + qBits := qBits + +theorem meetsBindingTarget_ofField (fieldBits lam qBits : Nat) (hfb : 0 < fieldBits) : + (ofField fieldBits lam qBits).MeetsBindingTarget := by + unfold MeetsBindingTarget kappa ofField + simp only + exact le_mul_ceilDiv _ _ hfb + +/-- Concrete BabyBear / KoalaBear / M31 parameters (⌊log₂ |F|⌋ = 30). -/ +def babyBear (lam qBits : Nat) : MerkleHasherParams := ofField 30 lam qBits + +/-- Concrete Goldilocks parameters (⌊log₂ |F|⌋ = 63). -/ +def goldilocks (lam qBits : Nat) : MerkleHasherParams := ofField 63 lam qBits + +/-- Concrete BLS12-381 scalar-field parameters (⌊log₂ |F|⌋ = 254). -/ +def bls12_381 (lam qBits : Nat) : MerkleHasherParams := ofField 254 lam qBits + +theorem babyBear_meetsBindingTarget (lam qBits : Nat) : + (babyBear lam qBits).MeetsBindingTarget := + meetsBindingTarget_ofField 30 lam qBits (by norm_num) + +-- Worked example: BabyBear at λ=128, q_H=64 → D=9, κ=270. +example : (babyBear 128 64).digestElems = 9 := by native_decide +example : (babyBear 128 64).kappa = 270 := by native_decide +example : (babyBear 128 64).saltElems = 5 := by native_decide + +end MerkleHasherParams + +/-- **Arithmetic bridge.** The birthday bound `q(q-1)/2^(κ+1)` is at most `2^(-λ)` whenever + the query count fits in `q ≤ 2^q_H` and the digest absorbs the slack `λ + 1 + 2·q_H ≤ κ`. -/ +theorem collisionBound_le_inv_pow {κ q lam qBits : Nat} + (hq : q ≤ 2 ^ qBits) + (hκ : lam + 1 + 2 * qBits ≤ κ) : + collisionBound κ q ≤ ((2 : ENNReal) ^ lam)⁻¹ := by + unfold collisionBound + -- 0. Useful non-zero / non-top facts. + have h2lam0 : (2 : ENNReal) ^ lam ≠ 0 := by positivity + have h2lamT : (2 : ENNReal) ^ lam ≠ ∞ := ENNReal.pow_ne_top (by simp) + have h2kap0 : (2 : ENNReal) ^ (κ + 1) ≠ 0 := by positivity + have h2kapT : (2 : ENNReal) ^ (κ + 1) ≠ ∞ := ENNReal.pow_ne_top (by simp) + -- 1. Numerator: q(q-1) ≤ q² ≤ (2^q_H)² = 2^(2·q_H). + have hnum : (q * (q - 1) : ENNReal) ≤ ((2 : ENNReal) ^ (2 * qBits)) := by + rcases Nat.eq_zero_or_pos q with rfl | hq1 + · simp + · have hq1' : 1 ≤ q := hq1 + have hqq : q * (q - 1) ≤ q ^ 2 := by nlinarith [Nat.sub_le q 1] + have hq2 : q ^ 2 ≤ 2 ^ (2 * qBits) := by + calc q ^ 2 ≤ (2 ^ qBits) ^ 2 := Nat.pow_le_pow_left hq 2 + _ = 2 ^ (2 * qBits) := by ring + calc (q * (q - 1) : ENNReal) + = ((q * (q - 1) : ℕ) : ENNReal) := by push_cast; rfl + _ ≤ ((q ^ 2 : ℕ) : ENNReal) := by exact_mod_cast hqq + _ ≤ ((2 ^ (2 * qBits) : ℕ) : ENNReal) := by exact_mod_cast hq2 + _ = (2 : ENNReal) ^ (2 * qBits) := by push_cast; rfl + -- 2. Denominator slack: 2·q_H + λ + 1 ≤ κ + 1, so 2^(κ+1) ≥ 2^(2·q_H) · 2^λ. + have hdenom : (2 : ENNReal) ^ (2 * qBits) * (2 : ENNReal) ^ lam ≤ (2 : ENNReal) ^ (κ + 1) := by + rw [← pow_add] + apply pow_le_pow_right₀ (by norm_num : (1 : ENNReal) ≤ 2) + omega + -- 3. Combine: q(q-1)/2^(κ+1) ≤ 2^(2q_H)/2^(κ+1) ≤ 1/2^λ. + calc (q * (q - 1) : ENNReal) / 2 ^ (κ + 1) + ≤ (2 : ENNReal) ^ (2 * qBits) / 2 ^ (κ + 1) := by + apply ENNReal.div_le_div_right hnum + _ ≤ ((2 : ENNReal) ^ lam)⁻¹ := by + rw [ENNReal.div_le_iff h2kap0 h2kapT, ← ENNReal.div_eq_inv_mul, + ENNReal.le_div_iff_mul_le (Or.inl h2lam0) (Or.inl h2lamT)] + exact hdenom + +/-- **Generic binding security.** Any field meeting `MeetsBindingTarget` gives + `λ`-bit position binding in the ROM — one proof for all concrete fields. -/ +theorem instantiation_binding_secure + {S : Type} [MerkleShape S] + (p : MerkleHasherParams) (htarget : p.MeetsBindingTarget) + [Nonempty (MerkleCommitment (ROHasher.ROHasherValue (MerkleHasherParams.kappa p)) S)] + {q : Nat} (hq : q ≤ 2 ^ p.qBits) + (A : HasPositionBinding.BindingAdversary + (V := MerkleCommitment (ROHasher.ROHasherValue p.kappa) S) p.kappa q) : + HasPositionBinding.bindingAdvantage A ≤ ((2 : ENNReal) ^ p.lam)⁻¹ := + (HasPositionBinding.binding_bound A).trans + (collisionBound_le_inv_pow hq htarget) + +/-- **BabyBear binding security.** No hypothesis required — `MeetsBindingTarget` is discharged + by `babyBear_meetsBindingTarget`. -/ +theorem babyBear_binding_secure + {S : Type} [MerkleShape S] + (lam qBits : Nat) + [Nonempty (MerkleCommitment + (ROHasher.ROHasherValue ((MerkleHasherParams.babyBear lam qBits).kappa)) S)] + {q : Nat} (hq : q ≤ 2 ^ qBits) + (A : HasPositionBinding.BindingAdversary + (V := MerkleCommitment + (ROHasher.ROHasherValue ((MerkleHasherParams.babyBear lam qBits).kappa)) S) + (MerkleHasherParams.babyBear lam qBits).kappa q) : + HasPositionBinding.bindingAdvantage A ≤ ((2 : ENNReal) ^ lam)⁻¹ := + instantiation_binding_secure (MerkleHasherParams.babyBear lam qBits) + (MerkleHasherParams.babyBear_meetsBindingTarget lam qBits) hq A + +end VectorCommitment.Probability.Instances From 0cdac336f25d34d3ba2be120ae03615179742c48 Mon Sep 17 00:00:00 2001 From: ajhavlin Date: Sat, 6 Jun 2026 16:18:50 +0200 Subject: [PATCH 10/17] VectorCommitment: interface facade and developer guide --- VectorCommitment/INTERFACE.md | 229 ++++++++++++++++++++++++++++++++ VectorCommitment/Interface.lean | 46 +++++++ 2 files changed, 275 insertions(+) create mode 100755 VectorCommitment/INTERFACE.md create mode 100755 VectorCommitment/Interface.lean diff --git a/VectorCommitment/INTERFACE.md b/VectorCommitment/INTERFACE.md new file mode 100755 index 0000000..1edcab5 --- /dev/null +++ b/VectorCommitment/INTERFACE.md @@ -0,0 +1,229 @@ +# VectorCommitment — Developer Interface Guide + +**Entry point:** `VectorCommitment/Interface.lean` + +--- + +## §0 The Map + +``` + Layer Lean layer File(s) Status +───────────────────────────────────────────────────────────────────────────────── + L1 Operational trait Src/Trait.lean interface + VectorCommitment V: Src/DataStructures.lean + setup/trim/commit/open/check + + L2 Merkle realization Src/Merkle/{Hasher,Shape, instance + MerkleCommitment H S Scheme,Instance,...}.lean + ⊢ VectorCommitment (Merkle…) + + L3 Abstract security classes Src/Security/{PositionBinding, classes + HasPositionBinding Extractability,Hiding, + HasStraightlineExtractor Equivocation}.lean + HasHiding + HasEquivocation + + L4 ROM discharge for Merkle Properties/Probability/ PROOFS + BindingROM ✅ Instances/*ROM.lean + ExtractabilityROM ◐ + Collision/RandomOracle/ + HidingROM ✗ Coupling/ROHasher/ + EquivocationROM ✗ CheckOracle/TraceCollision.lean + + L5 Hasher instantiation Instances/Parameters.lean CAPSTONE + MerkleHasherParams + (field, λ, q_H) → (κ, D, k, S) + babyBear_binding_secure ✅ +``` + +**Security status:** + +| Notion | Status | +|---------------|-------------------------------------------------| +| Binding | ✅ proven, axiom-clean | +| Extractability | ◐ reduced to `cacheExtract_sound` (1 sorry) | +| Hiding | ✗ params computed; ROM proof pending H1–H5 | +| Equivocation | ✗ out of scope (programmable RO) | + +--- + +## §1 Operational Trait + +```lean +class VectorCommitment (V : Type) where + setup : (maxLen maxQueries : Nat) → ULift UInt64 → UniversalParams + trim : UniversalParams → (len queries : Nat) → CommitterKey × VerifierKey + commit : CommitterKey → List Alphabet → Commitment × CommitmentState + «open» : CommitterKey → List Alphabet → Commitment → List Index → + List Alphabet → CommitmentState → Proof + check : VerifierKey → Commitment → List Index → List Alphabet → Proof → Bool +``` + +`HidingVectorCommitment V extends VectorCommitment V` adds the salted variants. + +**The verification path is `check`.** All security proofs reason about when `check` +returns `true` on a bad input. + +--- + +## §2 Merkle Realization + +`MerkleCommitment H S` for a hasher `H` and tree shape `S`: + +| Component | File | Role | +|---|---|---| +| `MerkleHasher` | `Src/Merkle/Hasher.lean` | `hashLeaf`, `hashNodes` | +| `MerkleShape` | `Src/Merkle/Shape.lean` | arity / depth / leaf-count | +| `MerkleCommitment` | `Src/Merkle/Scheme.lean` | data type; `commit`/`check` | +| `VectorCommitment` instance | `Src/Merkle/Instance.lean` | wraps the above | + +The ROM hasher is `ROHasherValue κ` (`Properties/Probability/ROHasher.lean`), where +`κ` is the digest bit-length. Use `MerkleVC κ S` from `Interface.lean` as the +canonical type. + +--- + +## §3 Security Classes + +Each notion is a four-field typeclass: + +```lean +class HasPositionBinding (V : Type) where + BindingAdversary : Type → Nat → Type -- (VerifierKey, budget) → adversary type + bindingAdvantage : BindingAdversary vk q → ℝ≥0∞ -- win probability + bindingError : VerifierKey → Nat → ℝ≥0∞ -- upper bound + binding_bound : bindingAdvantage A ≤ bindingError vk q +``` + +**Anti-vacuity convention.** `BindingAdversary` is non-empty by construction. +The subtype `{ A // QueryBudget (bindingInner A) q }` carries the budget proof. + +**Shared-oracle convention.** The advantage is defined over the *shared* oracle: +the adversary and the verifier (`checkOracle`) query the *same* random oracle +instance. This is mandatory — decoupling the verifier's oracle from the +adversary's makes the binding event trivially false. + +--- + +## §4 ROM Discharge + +The proof chain for binding: + +``` +Pr[Merkle binding failure] + ≤ Pr[trace has a collision] [binding_win_le_trace_collision, BindingROM] + ≤ collisionBound κ q [coupling_trace_le_collisionBound, Coupling] + ≤ 2^(-λ) [collisionBound_le_inv_pow, Parameters] +``` + +Two shared cores: + +| Theorem | File | What it proves | +|---|---|---| +| `birthdayBound` | `Collision.lean` | n iid uniform samples from R collide with prob ≤ n(n-1)/(2\|R\|) | +| `coupling_trace_le_collisionBound` | `Coupling.lean` | adaptive lazy-oracle trace collision ≤ collisionBound κ q | + +Per-notion reduction pattern: +1. Define the experiment as an `OracleComp` computation. +2. Show: winning experiment output ⇒ colliding trace (structural). +3. Apply `coupling_trace_le_collisionBound`. + +| Instance file | Status | Sorry count | +|---|---|---| +| `BindingROM.lean` | **✅ closed** | 0 | +| `ExtractabilityROM.lean` | ◐ | 1 (`cacheExtract_sound` bridge) | +| `HidingROM.lean` | ✗ | 2 (hiding experiment + hiding bound) | +| `EquivocationROM.lean` | ✗ | 2 (equivocation experiment + bound) | + +--- + +## §5 Hasher Instantiation + +`MerkleHasherParams` bundles the numbers a developer chooses: + +```lean +structure MerkleHasherParams where + fieldBits : Nat -- ⌊log₂ |F|⌋ + digestElems : Nat -- D + saltElems : Nat -- k (hiding axis) + saltBytes : Nat -- S (hiding axis, byte-oriented hashers) + lam : Nat -- λ + qBits : Nat -- q_H +``` + +`MerkleHasherParams.kappa p = p.fieldBits * p.digestElems` — the realized digest. + +`MeetsBindingTarget p : Prop = (p.lam + 1 + 2 * p.qBits ≤ p.kappa)` — decidable gate. + +The constructor `ofField fieldBits lam qBits` computes correct D, k, S via ceiling division: +- `D = ⌈(λ+1+2q_H)/fieldBits⌉`, `k = ⌈λ/fieldBits⌉`, `S = ⌈λ/8⌉` + +Concrete fields: + +| Name | fieldBits | Examples | +|---|---|---| +| `babyBear lam qBits` | 30 | BabyBear, KoalaBear, M31 | +| `goldilocks lam qBits` | 63 | Goldilocks | +| `bls12_381 lam qBits` | 254 | BLS12-381 scalar | + +BabyBear at λ=128, q_H=64: `D=9, κ=270, k=5, S=16`. + +Capstone theorems: + +```lean +theorem instantiation_binding_secure + (p : MerkleHasherParams) (htarget : p.MeetsBindingTarget) + {q : Nat} (hq : q ≤ 2 ^ p.qBits) (A : ...) : + HasPositionBinding.bindingAdvantage A ≤ ((2 : ENNReal) ^ p.lam)⁻¹ + +theorem babyBear_binding_secure + (lam qBits : Nat) {q : Nat} (hq : q ≤ 2 ^ qBits) (A : ...) : + HasPositionBinding.bindingAdvantage A ≤ ((2 : ENNReal) ^ lam)⁻¹ +``` + +--- + +## §6 Entry Points + +| Goal | Where to start | +|---|---| +| Verify a Merkle opening in Lean | `VectorCommitment.check` (L1) | +| Understand what "binding" means | `Src/Security/PositionBinding.lean` (L3) | +| See the ROM proof of binding | `Properties/Probability/Instances/BindingROM.lean` (L4) | +| Get a concrete security statement | `Instances/Parameters.lean` (L5) | +| Understand the full chain | `Interface.lean` → this guide | + +--- + +## §7 FAQ + +**Q: Why four security classes?** +Because they reduce to different axes: binding/extractability reduce to digest collisions +(`2^κ`); hiding reduces to salt entropy (`2^s` plus a simulator term); equivocation +requires a programmable RO. Splitting them avoids cross-contamination of parameters. + +**Q: Why `OracleComp` instead of a PMF over all oracle functions?** +Because the Rust implementation runs a finite sequence of hash calls, not an infinite +random function. The inductive `OracleComp` free monad matches that finite-execution model. +It also enables direct structural induction (the `run_coll_le` proof), whereas the bare-function +encoding is *provably false* — see `coupling_unconditional_is_false` on `wip/phase-b-birthday-bound`. + +**Q: What is `h_dom` / why the inductive monad?** +`h_dom` was a `QueryLog → PMF` hypothesis in the early eager-seed approach. It was +machine-refuted (`coupling_unconditional_is_false`). The inductive `OracleComp` type exposes +the computation structure that makes `run_coll_le` provable by structural induction. + +**Q: Why is hiding separate from binding?** +Binding lives on the digest axis (`|Digest| = 2^κ`). Hiding lives on the salt axis +(`|Salt| ≥ 2^s`) plus an internal-node simulation term. These are independent parameters; +a large `κ` does not imply any hiding if `s = 0` (no salt). The hiding follow-on chain +(H1–H5) adds the salt axis proofs without reopening the closed binding spine. + +--- + +## §8 Maintenance + +- Sync the status table in §0 after each PR; update `binding ✅`, `hiding ✗` etc. +- Keep `Interface.lean` ≤ 250 lines; add aliases, not proofs. +- One alias per concept; do not re-export the same theorem under two names. +- When adding a new security notion, add: (a) a class in `Src/Security/`, (b) an + instance in `Instances/*ROM.lean`, (c) a row in the §0 status table, (d) a §4 entry. diff --git a/VectorCommitment/Interface.lean b/VectorCommitment/Interface.lean new file mode 100755 index 0000000..18cbe47 --- /dev/null +++ b/VectorCommitment/Interface.lean @@ -0,0 +1,46 @@ +/- VectorCommitment/Interface.lean + ENTRY POINT for the Vector Commitment verification path. + Layers: L1 operational trait · L2 Merkle realization + L3 security classes · L4 ROM discharge · L5 hasher instantiation +-/ +import VectorCommitment.Src +import VectorCommitment.Properties + +namespace VectorCommitment.Interface +open VectorCommitment VectorCommitment.Security VectorCommitment.Probability +open VectorCommitment.Probability.Instances + +/-! ## L1/L2: the scheme you verify against -/ +/-- The canonical Merkle VC over a κ-bit ROM hasher and a tree shape `S`. -/ +abbrev MerkleVC (κ : Nat) (S : Type) [MerkleShape S] := + MerkleCommitment (ROHasher.ROHasherValue κ) S + +/-! ## L3: the four security notions -/ +-- HasPositionBinding, HasStraightlineExtractor, HasHiding, HasEquivocation +-- (instances discharged at L4 for MerkleVC) + +/-! ## L4: machine-checked cores -/ +/-- The finite iid birthday bound: n samples from range R collide with prob ≤ n(n-1)/(2|R|). -/ +alias birthdayCollisionBound := Probability.birthdayBound + +/-- The lazy-oracle trace collision bound: any q-query computation has a colliding trace + with probability at most collisionBound κ q = q(q-1)/2^(κ+1). -/ +alias romTraceCollisionBound := Probability.coupling_trace_le_collisionBound + +/-- The concrete collision error expression: q(q-1)/2^(κ+1). -/ +noncomputable abbrev collisionProbability := @Probability.collisionBound + +/-! ## L5: hasher instantiation -/ +-- MerkleHasherParams: the parameter record (fieldBits, D, k, S, λ, q_H) +-- ofField: computes D = ⌈(λ+1+2q_H)/fieldBits⌉, k, S from field+security goals +-- babyBear, goldilocks, bls12_381: concrete per-field constructors +-- instantiation_binding_secure: generic λ-bit binding for MeetsBindingTarget params +-- babyBear_binding_secure: zero-hypothesis BabyBear/KoalaBear/M31 capstone + +/-! ## Status + binding ✅ proven, axiom-clean [propext, Classical.choice, Quot.sound] + extractability ◐ reduced to cacheExtract_sound (1 sorry in ExtractabilityROM) + hiding ✗ parameters computed (k, S); ROM proof pending H1–H5 + equivocation ✗ out of scope (programmable RO) -/ + +end VectorCommitment.Interface From 487c9f84a660d3b91db248bb9bac578bfd34ecd7 Mon Sep 17 00:00:00 2001 From: ajhavlin Date: Sat, 6 Jun 2026 16:24:19 +0200 Subject: [PATCH 11/17] VectorCommitment: hiding parameters and salt-entropy types --- VectorCommitment/Properties.lean | 1 + .../Probability/Instances/HidingParams.lean | 126 ++++++++++++++++++ 2 files changed, 127 insertions(+) create mode 100644 VectorCommitment/Properties/Probability/Instances/HidingParams.lean diff --git a/VectorCommitment/Properties.lean b/VectorCommitment/Properties.lean index d97e9b0..4729133 100644 --- a/VectorCommitment/Properties.lean +++ b/VectorCommitment/Properties.lean @@ -3,6 +3,7 @@ import VectorCommitment.Properties.Probability.ROHasher import VectorCommitment.Properties.Probability.Collision import VectorCommitment.Properties.Probability.Instances.BindingROM import VectorCommitment.Properties.Probability.Instances.Parameters +import VectorCommitment.Properties.Probability.Instances.HidingParams import VectorCommitment.Properties.Probability.Instances.ExtractabilityROM import VectorCommitment.Properties.Probability.Instances.HidingROM import VectorCommitment.Properties.Probability.Instances.EquivocationROM diff --git a/VectorCommitment/Properties/Probability/Instances/HidingParams.lean b/VectorCommitment/Properties/Probability/Instances/HidingParams.lean new file mode 100644 index 0000000..9c79b66 --- /dev/null +++ b/VectorCommitment/Properties/Probability/Instances/HidingParams.lean @@ -0,0 +1,126 @@ +/- +Copyright (c) 2026 LeanStuff contributors. All rights reserved. +-/ +import VectorCommitment.Properties.Probability.Instances.Parameters +import Mathlib.Data.Vector.Basic +import Mathlib.Data.Fintype.Vector +import Mathlib.Data.Fintype.BigOperators + +/-! +# Hiding parameters and salt-entropy types + +The hiding axis is governed by parameters that are *separate* from the binding +digest axis: the per-leaf salt entropy `s`, the message length `ℓ`, the opening +size `Q`, and the random-oracle query budget `q`. This file names those +parameters and the book's finite-query error expressions, and introduces the +salt-space entropy interface used by the later root-hiding and privacy proofs. + +Nothing here reopens a closed binding theorem: the binding capstone +(`Parameters.lean`) is imported only to extend `MerkleHasherParams` with the +salt-width helpers it already carries (`saltElems`, `saltBytes`). +-/ + +namespace VectorCommitment.Probability + +open scoped ENNReal + +/-- The parameters a Merkle-commitment hiding bound depends on. These live on + the salt/privacy axis and are independent of the binding sizing rule. -/ +structure HidingParams where + /-- digest output bit-length `κ`. -/ + kappa : Nat + /-- per-leaf salt entropy `s`. -/ + saltBits : Nat + /-- committed message length `ℓ`. -/ + messageLength : Nat + /-- number of opened positions `Q`. -/ + openingSize : Nat + /-- random-oracle query budget `q`. -/ + queryBound : Nat + +namespace HidingParams + +/-- Book finite-query **root-hiding** error `ℓ·q / 2^s + ℓ·q / 2^(2κ)` + (`lemma:mt-root-hiding`): the leaf salt-hit term plus the internal-node + simulation term. -/ +noncomputable def rootHidingError (p : HidingParams) : ENNReal := + (p.messageLength * p.queryBound : ENNReal) / 2 ^ p.saltBits + + (p.messageLength * p.queryBound : ENNReal) / 2 ^ (2 * p.kappa) + +/-- Book loose finite-query **privacy** error + `Q·ℓ·q / 2^s + Q·ℓ·q / 2^(2κ)` (`lemma:mt-privacy`, loose public bound). + The exact form sums `rootHidingError` over `copath(I) \ path(I)`; this is the + coarse upper bound downstream IOP/PCP transformations consume. -/ +noncomputable def privacyHidingErrorLoose (p : HidingParams) : ENNReal := + (p.openingSize * p.messageLength * p.queryBound : ENNReal) / 2 ^ p.saltBits + + (p.openingSize * p.messageLength * p.queryBound : ENNReal) / 2 ^ (2 * p.kappa) + +end HidingParams + +/-- A finite salt space carrying at least `saltBits` bits of entropy. We require + only a *lower* bound `2 ^ saltBits ≤ |Salt|`, because field-element salts have + cardinality `|F|^k`, which is generally not a power of two. -/ +class SaltEntropy (Salt : Type) [Fintype Salt] where + /-- the certified entropy `s`. -/ + saltBits : Nat + /-- the salt space is at least `2^s` large. -/ + card_lower_bound : 2 ^ saltBits ≤ Fintype.card Salt + +/-- A salt of `S` bytes. -/ +abbrev ByteSalt (S : Nat) := List.Vector (Fin 256) S + +/-- A salt of `k` field elements over `F`. -/ +abbrev FieldSalt (F : Type) (k : Nat) := List.Vector F k + +/-- Byte salts realize exactly `2^(8S)` entropy. -/ +theorem byteSalt_card_lower_bound (S : Nat) : + 2 ^ (8 * S) ≤ Fintype.card (ByteSalt S) := by + have hcard : Fintype.card (ByteSalt S) = 256 ^ S := by + simp [ByteSalt, card_vector] + rw [hcard] + have : (256 : Nat) = 2 ^ 8 := by norm_num + rw [this, ← pow_mul] + +/-- Field salts of `k` elements over a field with at least `2^fieldBits` + elements realize at least `2^(fieldBits·k)` entropy. -/ +theorem fieldSalt_card_lower_bound (F : Type) [Fintype F] (fieldBits k : Nat) + (hF : 2 ^ fieldBits ≤ Fintype.card F) : + 2 ^ (fieldBits * k) ≤ Fintype.card (FieldSalt F k) := by + have hcard : Fintype.card (FieldSalt F k) = Fintype.card F ^ k := by + simp [FieldSalt, card_vector] + rw [hcard, pow_mul] + exact Nat.pow_le_pow_left hF k + +/-- `SaltEntropy` instance for byte salts (`s = 8S`). -/ +instance (S : Nat) : SaltEntropy (ByteSalt S) where + saltBits := 8 * S + card_lower_bound := byteSalt_card_lower_bound S + +/-- Deterministic salts (`Salt = Unit`) carry zero entropy: `|Unit| = 1 = 2^0`. + This is the book's `remark:mt-no-privacy` case — a no-op, *not* a weak hiding + instance, so we record the fact but give `Unit` no positive `SaltEntropy`. -/ +theorem unit_card : Fintype.card Unit = 1 := rfl + +namespace Instances + +open MerkleHasherParams + +/-- Field-salt entropy width `s_field = fieldBits · k` carried by the hasher params. -/ +def MerkleHasherParams.fieldSaltBits (p : MerkleHasherParams) : Nat := + p.fieldBits * p.saltElems + +/-- Byte-salt entropy width `s_byte = 8 · S` carried by the hasher params. -/ +def MerkleHasherParams.byteSaltBits (p : MerkleHasherParams) : Nat := + 8 * p.saltBytes + +/-- The field-salt entropy target: `λ ≤ fieldBits · k`. -/ +def MerkleHasherParams.MeetsFieldSaltTarget (p : MerkleHasherParams) : Prop := + p.lam ≤ p.fieldSaltBits + +/-- The byte-salt entropy target: `λ ≤ 8 · S`. -/ +def MerkleHasherParams.MeetsByteSaltTarget (p : MerkleHasherParams) : Prop := + p.lam ≤ p.byteSaltBits + +end Instances + +end VectorCommitment.Probability From a5d820e625ae4074f0ae45c32fe90ab9e4584f67 Mon Sep 17 00:00:00 2001 From: ajhavlin Date: Sat, 6 Jun 2026 16:31:13 +0200 Subject: [PATCH 12/17] VectorCommitment: operational per-leaf salt path --- VectorCommitment/Properties.lean | 1 + .../Probability/HidingSaltPath.lean | 82 +++++++++++++++++++ VectorCommitment/Src/Merkle/Scheme.lean | 26 +++++- 3 files changed, 107 insertions(+), 2 deletions(-) create mode 100644 VectorCommitment/Properties/Probability/HidingSaltPath.lean diff --git a/VectorCommitment/Properties.lean b/VectorCommitment/Properties.lean index 4729133..9d9630b 100644 --- a/VectorCommitment/Properties.lean +++ b/VectorCommitment/Properties.lean @@ -4,6 +4,7 @@ import VectorCommitment.Properties.Probability.Collision import VectorCommitment.Properties.Probability.Instances.BindingROM import VectorCommitment.Properties.Probability.Instances.Parameters import VectorCommitment.Properties.Probability.Instances.HidingParams +import VectorCommitment.Properties.Probability.HidingSaltPath import VectorCommitment.Properties.Probability.Instances.ExtractabilityROM import VectorCommitment.Properties.Probability.Instances.HidingROM import VectorCommitment.Properties.Probability.Instances.EquivocationROM diff --git a/VectorCommitment/Properties/Probability/HidingSaltPath.lean b/VectorCommitment/Properties/Probability/HidingSaltPath.lean new file mode 100644 index 0000000..7b17d8a --- /dev/null +++ b/VectorCommitment/Properties/Probability/HidingSaltPath.lean @@ -0,0 +1,82 @@ +/- +Copyright (c) 2026 LeanStuff contributors. All rights reserved. +-/ +import VectorCommitment.Src.Merkle.Scheme +import VectorCommitment.Properties.Theorems.Hiding +import Mathlib.Probability.ProbabilityMassFunction.Constructions +import Mathlib.Probability.Distributions.Uniform +import Mathlib.Data.Fintype.Vector + +/-! +# Operational per-leaf salt path + +The non-hiding `commit` salts every leaf with `defaultSalt`. Hiding needs an +explicit per-leaf-salted commit (`commitWithSalts`, in `Scheme.lean`) and a +*distributional* version that samples one fresh uniform salt per leaf. The ROM +hiding proofs in H4/H5 run against `commitWithUniformSalts`, never against an +executable seed generator. + +The deterministic-salt case (`Subsingleton Salt`, e.g. `Salt = Unit`) is the +book's `remark:mt-no-privacy` no-privacy construction: salts are a no-op, so the +commit root does not depend on the salt vector at all. +-/ + +namespace MerkleCommitment + +variable {H S : Type} [MerkleHasher H] [MerkleShape S] + +/-- **Distributional salted commit.** Sample `numLeaves` independent uniform + per-leaf salts and commit with them. This is the experiment the ROM + root-hiding and privacy proofs distinguish against. -/ +noncomputable def commitWithUniformSalts + [Fintype (MerkleHasher.Salt H)] [Nonempty (MerkleHasher.Salt H)] + (mc : MerkleCommitment H S) (msg : List (MerkleHasher.Symbol H)) : + PMF (Committed H S × Trapdoor H S) := + haveI : Nonempty (List.Vector (MerkleHasher.Salt H) (MerkleShape.numLeaves mc.shape)) := + ⟨List.Vector.replicate _ (Classical.arbitrary _)⟩ + (PMF.uniformOfFintype + (List.Vector (MerkleHasher.Salt H) (MerkleShape.numLeaves mc.shape))).map + (fun salts => mc.commitWithSalts msg salts.toList) + +/-- The salted-commit root is the vertex-0 label of `labelAt` (the same bridge + `commit_root_eq_labelAt_zero` gives for the default-salt `commit`). -/ +theorem commitWithSalts_root_eq_labelAt_zero + (mc : MerkleCommitment H PerfectBinary) + (msg : List (MerkleHasher.Symbol H)) + (salts : List (MerkleHasher.Salt H)) + (h_n_pos : MerkleShape.numLeaves mc.shape > 0) : + (mc.commitWithSalts msg salts).fst.root = labelAt mc msg salts 0 := by + have hne : MerkleShape.numLeaves mc.shape ≠ 0 := Nat.pos_iff_ne_zero.mp h_n_pos + have htotal : 2 * MerkleShape.numLeaves mc.shape - 1 > 0 := by omega + show (mc.commitWithSalts msg salts).fst.root = _ + unfold MerkleCommitment.commitWithSalts MerkleCommitment.buildLabels MerkleCommitment.listGetD + simp [hne] + rw [List.getElem?_range htotal] + rfl + +/-- **No-privacy / deterministic-salt no-op.** When the salt space is a + subsingleton (in particular `Salt = Unit`), the commit root is independent of + the salt vector: any two salt assignments yield the same root. This is the + book's `s = 0` case — deterministic salts hide nothing, they are simply a + no-op on the root. -/ +theorem commitWithSalts_root_eq_of_subsingleton + [Subsingleton (MerkleHasher.Salt H)] + (mc : MerkleCommitment H PerfectBinary) + (msg : List (MerkleHasher.Symbol H)) + (h_n_pos : MerkleShape.numLeaves mc.shape > 0) + (salts₀ salts₁ : List (MerkleHasher.Salt H)) : + (mc.commitWithSalts msg salts₀).fst.root = + (mc.commitWithSalts msg salts₁).fst.root := by + rw [commitWithSalts_root_eq_labelAt_zero mc msg salts₀ h_n_pos, + commitWithSalts_root_eq_labelAt_zero mc msg salts₁ h_n_pos] + apply labelAt_eq_of_leaf_hash_eq + intro v _ + -- Every leaf hash agrees because the two salt entries are equal (subsingleton). + have heq : (listGetD salts₀ (v - (MerkleShape.numLeaves mc.shape - 1)) + (MerkleHasher.defaultSalt.default : MerkleHasher.Salt H)) = + (listGetD salts₁ (v - (MerkleShape.numLeaves mc.shape - 1)) + (MerkleHasher.defaultSalt.default : MerkleHasher.Salt H)) := + Subsingleton.elim _ _ + simp only [heq] + +end MerkleCommitment diff --git a/VectorCommitment/Src/Merkle/Scheme.lean b/VectorCommitment/Src/Merkle/Scheme.lean index 279e057..81d5ba7 100644 --- a/VectorCommitment/Src/Merkle/Scheme.lean +++ b/VectorCommitment/Src/Merkle/Scheme.lean @@ -78,8 +78,21 @@ def buildLabels (mc : MerkleCommitment H S) let total := if n = 0 then 0 else 2 * n - 1 (List.range total).map (labelAt mc msg salts) -/-- Commit. Returns a `Committed` (just the root) and a `Trapdoor` (message, - salts, full label vector). Salts default to `defaultSalt` (non-hiding). -/ +/-- Commit with an explicit per-leaf salt vector. This is the hiding-aware + commit: the caller supplies `salts`, one per leaf. The non-hiding `commit` + is the special case where every salt is `defaultSalt`. Returns a `Committed` + (just the root) and a `Trapdoor` (message, salts, full label vector). -/ +def commitWithSalts (mc : MerkleCommitment H S) (msg : List (MerkleHasher.Symbol H)) + (salts : List (MerkleHasher.Salt H)) : + Committed H S × Trapdoor H S := + let n := MerkleShape.numLeaves mc.shape + let labels := mc.buildLabels msg salts + let placeholder : MerkleHasher.Digest H := + MerkleHasher.hashNodes mc.hasher [] + let rootDigest : MerkleHasher.Digest H := + if n = 0 then placeholder else listGetD labels 0 placeholder + ({ root := rootDigest }, { message := msg, salts := salts, labels := labels }) + def commit (mc : MerkleCommitment H S) (msg : List (MerkleHasher.Symbol H)) : Committed H S × Trapdoor H S := let n := MerkleShape.numLeaves mc.shape @@ -92,6 +105,15 @@ def commit (mc : MerkleCommitment H S) (msg : List (MerkleHasher.Symbol H)) : if n = 0 then placeholder else listGetD labels 0 placeholder ({ root := rootDigest }, { message := msg, salts := salts, labels := labels }) +/-- `commit` is `commitWithSalts` at the default-salt vector. -/ +theorem commit_eq_commitWithSalts_default (mc : MerkleCommitment H S) + (msg : List (MerkleHasher.Symbol H)) : + mc.commit msg = + mc.commitWithSalts msg + (List.replicate (MerkleShape.numLeaves mc.shape) + (MerkleHasher.defaultSalt.default : MerkleHasher.Salt H)) := + rfl + /-- Open. For each requested index, return the leaf salt plus the bottom-up copath digests read off the trapdoor's label vector. -/ def «open» (mc : MerkleCommitment H S) (_msg : List (MerkleHasher.Symbol H)) From a768eba9a5a5766b1d2c0c7d3f10437b9957fb0c Mon Sep 17 00:00:00 2001 From: ajhavlin Date: Sat, 6 Jun 2026 16:52:30 +0200 Subject: [PATCH 13/17] VectorCommitment: salt-space high-entropy hidden-query lemma --- VectorCommitment/Properties.lean | 1 + .../Properties/Probability/HiddenQuery.lean | 74 +++++++++++++++++++ 2 files changed, 75 insertions(+) create mode 100644 VectorCommitment/Properties/Probability/HiddenQuery.lean diff --git a/VectorCommitment/Properties.lean b/VectorCommitment/Properties.lean index 9d9630b..015ee66 100644 --- a/VectorCommitment/Properties.lean +++ b/VectorCommitment/Properties.lean @@ -5,6 +5,7 @@ import VectorCommitment.Properties.Probability.Instances.BindingROM import VectorCommitment.Properties.Probability.Instances.Parameters import VectorCommitment.Properties.Probability.Instances.HidingParams import VectorCommitment.Properties.Probability.HidingSaltPath +import VectorCommitment.Properties.Probability.HiddenQuery import VectorCommitment.Properties.Probability.Instances.ExtractabilityROM import VectorCommitment.Properties.Probability.Instances.HidingROM import VectorCommitment.Properties.Probability.Instances.EquivocationROM diff --git a/VectorCommitment/Properties/Probability/HiddenQuery.lean b/VectorCommitment/Properties/Probability/HiddenQuery.lean new file mode 100644 index 0000000..ebf7f92 --- /dev/null +++ b/VectorCommitment/Properties/Probability/HiddenQuery.lean @@ -0,0 +1,74 @@ +/- +Copyright (c) 2026 LeanStuff contributors. All rights reserved. +-/ +import VectorCommitment.Properties.Probability.Coupling +import VectorCommitment.Properties.Probability.Instances.HidingParams +import Mathlib.Probability.Distributions.Uniform + +/-! +# Salt-space high-entropy hidden-query lemma + +This file formalizes the finite-query branch of the book's `lemma:cm-hiding` / +`lemma:rom-ow-high-entropy`: an adversary issuing at most `q` oracle queries +hits an *independently* sampled hidden salt `r` with probability at most +`q / |Salt| ≤ q / 2^s`. + +The statement is oracle-generic — no Merkle structure — so root-hiding (H4) and +privacy (H5) instantiate it for leaf queries. It is a *different* event from the +digest trace-collision of `Coupling.lean`: here we bound the adversary guessing a +hidden salt coordinate, not two oracle answers coinciding. + +The `hidingExperiment` distribution pairs a `q`-query run with an independent +uniform hidden salt; the bad event is "some logged query decodes to the salt". +-/ + +namespace VectorCommitment.Probability + +open scoped ENNReal + +variable {spec : OracleSpec} {Salt : Type} [Fintype Salt] + +/-- The hidden-query experiment: run `c` from the empty cache, then sample the + hidden salt `r ← Salt` independently. -/ +noncomputable def hiddenQueryExperiment {α : Type} [Nonempty Salt] + (c : OracleComp spec α) : + PMF ((α × QueryLog spec) × Salt) := + (c.run QueryLog.empty).bind (fun p => + (PMF.uniformOfFintype Salt).map (fun r => (p, r))) + +/-- The bad event: some query input in the finished trace decodes to the hidden salt. -/ +def hiddenQueryHit (parseSalt : spec.Domain → Option Salt) : + Set ((α × QueryLog spec) × Salt) := + {x | ∃ d ∈ x.1.2.map Prod.fst, parseSalt d = some x.2} + +/-- **Hidden-query bound (book `lemma:rom-ow-high-entropy`, finite-query form).** + Sampling the hidden salt `r` independently of a `q`-query computation `c`, the + probability that some query in `c`'s finished trace decodes to `r` is at most + `q / |Salt|`. + + *Isolated distributional core.* The argument is the book's union bound: by + independence the salt is uniform given the run, so for each fixed run the hit + probability is `(#distinct decoded salts)/|Salt| ≤ (log length)/|Salt|`, and + the log length is `≤ q` by the query budget; averaging over runs preserves the + bound. Formalizing the average requires the `PMF` Fubini/`tsum` swap; it is + kept here as the single named gap matching the book lemma. -/ +theorem hidden_query_hit_le [Nonempty Salt] {α : Type} + (parseSalt : spec.Domain → Option Salt) + (c : OracleComp spec α) (q : Nat) (hbud : OracleComp.QueryBudget c q) : + (hiddenQueryExperiment c).toOuterMeasure (hiddenQueryHit (α := α) parseSalt) + ≤ (q : ENNReal) / (Fintype.card Salt) := by + sorry + +/-- **Entropy-lower-bound corollary.** Against a salt space certified to carry + `s` bits of entropy (`2^s ≤ |Salt|`), the hidden-query bound is `q / 2^s`. -/ +theorem hidden_query_hit_le_inv_pow [Nonempty Salt] {α : Type} + (parseSalt : spec.Domain → Option Salt) + (c : OracleComp spec α) (q s : Nat) (hbud : OracleComp.QueryBudget c q) + (hs : 2 ^ s ≤ Fintype.card Salt) : + (hiddenQueryExperiment c).toOuterMeasure (hiddenQueryHit (α := α) parseSalt) + ≤ (q : ENNReal) / 2 ^ s := by + refine (hidden_query_hit_le parseSalt c q hbud).trans ?_ + gcongr + exact_mod_cast hs + +end VectorCommitment.Probability From 68a09f58bbd37915fdd971edd1e548a6df7beefb Mon Sep 17 00:00:00 2001 From: ajhavlin Date: Sat, 6 Jun 2026 16:57:10 +0200 Subject: [PATCH 14/17] VectorCommitment: ROM root hiding and salt-entropy capstones --- VectorCommitment/Properties.lean | 1 + .../Probability/Instances/RootHidingROM.lean | 120 ++++++++++++++++++ 2 files changed, 121 insertions(+) create mode 100644 VectorCommitment/Properties/Probability/Instances/RootHidingROM.lean diff --git a/VectorCommitment/Properties.lean b/VectorCommitment/Properties.lean index 015ee66..00a4bb0 100644 --- a/VectorCommitment/Properties.lean +++ b/VectorCommitment/Properties.lean @@ -6,6 +6,7 @@ import VectorCommitment.Properties.Probability.Instances.Parameters import VectorCommitment.Properties.Probability.Instances.HidingParams import VectorCommitment.Properties.Probability.HidingSaltPath import VectorCommitment.Properties.Probability.HiddenQuery +import VectorCommitment.Properties.Probability.Instances.RootHidingROM import VectorCommitment.Properties.Probability.Instances.ExtractabilityROM import VectorCommitment.Properties.Probability.Instances.HidingROM import VectorCommitment.Properties.Probability.Instances.EquivocationROM diff --git a/VectorCommitment/Properties/Probability/Instances/RootHidingROM.lean b/VectorCommitment/Properties/Probability/Instances/RootHidingROM.lean new file mode 100644 index 0000000..c56e16f --- /dev/null +++ b/VectorCommitment/Properties/Probability/Instances/RootHidingROM.lean @@ -0,0 +1,120 @@ +/- +Copyright (c) 2026 LeanStuff contributors. All rights reserved. +-/ +import VectorCommitment.Properties.Probability.HiddenQuery +import VectorCommitment.Properties.Probability.HidingSaltPath +import VectorCommitment.Properties.Probability.ROHasher +import VectorCommitment.Properties.Theorems.Hiding + +/-! +# ROM Merkle root hiding + +This file formalizes the book's finite-query Merkle root-hiding theorem +(`lemma:mt-root-hiding`): the commit-root distribution, taken over fresh uniform +per-leaf salts, is `rootHidingError`-close to a uniform digest. + +```text +rootHidingError p = ℓ·q / 2^s + ℓ·q / 2^(2κ) +``` + +The first term is the leaf salt-hit error (one `hidden_query_hit_le` per leaf, +union-bounded over `ℓ` leaves); the second is the internal-node simulation error +(each internal node is a basic commitment with `2κ`-bit "salt"), and the +structural backbone is the proved `mt_root_hiding` lemma — the message can reach +the root only through the leaf hashes. + +The distributional hybrid that glues these together is the one named gap +(`mt_root_hiding_rom_bound`), whose statement matches the book lemma exactly. +The salt-entropy *target* lemmas below are fully proved and are the parameter +layer the field/byte capstones consume. +-/ + +namespace VectorCommitment.Probability.Instances + +open scoped ENNReal +variable {κ : Nat} + +/-- The root simulator outputs a uniform `κ`-bit digest (book `MTRootSimulator`). -/ +noncomputable def rootSimulator (κ : Nat) : PMF (List.Vector Bool κ) := + PMF.uniformOfFintype _ + +/-- The real root distribution: commit to `msg` with fresh uniform per-leaf + salts and read off the root. -/ +noncomputable def realRootDist {S : Type} [MerkleShape S] + (mc : MerkleCommitment (ROHasher.ROHasherValue κ) S) + (msg : List (MerkleHasher.Symbol (ROHasher.ROHasherValue κ))) : + PMF (List.Vector Bool κ) := + haveI : Fintype (MerkleHasher.Salt (ROHasher.ROHasherValue κ)) := + inferInstanceAs (Fintype (List.Vector Bool κ)) + haveI : Nonempty (MerkleHasher.Salt (ROHasher.ROHasherValue κ)) := + inferInstanceAs (Nonempty (List.Vector Bool κ)) + (mc.commitWithUniformSalts msg).map (fun p => p.1.root) + +/-- **Merkle root hiding in the ROM (book `lemma:mt-root-hiding`).** The real + root distribution and the simulated uniform root are `rootHidingError p`-close + in total-variation distance, for a `q`-query distinguisher. + + *Isolated distributional core.* Proof decomposition (book): + 1. leaf layer — replace each `H(mᵢ, saltᵢ)` by a uniform digest; one + `hidden_query_hit_le` per leaf, union-bounded over `ℓ = messageLength`; + 2. internal layers — replace each internal-node hash by a uniform digest, + charged `q / 2^(2κ)` per node via `cm-hiding` at `2κ`-bit salt; + 3. structural propagation — `mt_root_hiding` shows the message reaches the + root only through leaf hashes. + The hybrid that sums these into a TV bound is the single named gap, matching + the book statement. -/ +theorem mt_root_hiding_rom_bound {S : Type} [MerkleShape S] + (mc : MerkleCommitment (ROHasher.ROHasherValue κ) S) + (msg : List (MerkleHasher.Symbol (ROHasher.ROHasherValue κ))) + (p : HidingParams) (q : Nat) + (hκ : p.kappa = κ) (hℓ : p.messageLength = msg.length) (hq : p.queryBound = q) + (E : Set (List.Vector Bool κ)) : + (realRootDist mc msg).toOuterMeasure E + ≤ (rootSimulator κ).toOuterMeasure E + p.rootHidingError := by + -- One-sided event indistinguishability: the real root is no more likely to land + -- in any event `E` than the uniform simulated root, up to `rootHidingError`. + -- (Taking the sup over `E` gives the TV-distance form.) Structural content via + -- `mt_root_hiding`; the distributional hybrid is the named gap. + sorry + +/-! ## Salt-entropy target lemmas (fully proved) + +These discharge the `MeetsFieldSaltTarget` / `MeetsByteSaltTarget` predicates for +`MerkleHasherParams.ofField`-constructed parameters, and convert them into the `2^λ ≤ |Salt|` +entropy facts the privacy capstones need. They are the salt-axis analogue of the +binding capstone's `meetsBindingTarget_ofField`. -/ + +/-- `MerkleHasherParams.ofField` always meets the field-salt entropy target: `λ ≤ fieldBits·k`. -/ +theorem meetsFieldSaltTarget_ofField (fieldBits lam qBits : Nat) (hfb : 0 < fieldBits) : + (MerkleHasherParams.ofField fieldBits lam qBits).MeetsFieldSaltTarget := by + show lam ≤ (MerkleHasherParams.ofField fieldBits lam qBits).fieldSaltBits + show lam ≤ fieldBits * (MerkleHasherParams.ofField fieldBits lam qBits).saltElems + -- saltElems = ⌈lam / fieldBits⌉, so fieldBits · saltElems ≥ lam by `le_mul_ceilDiv`. + exact le_mul_ceilDiv lam fieldBits hfb + +/-- `MerkleHasherParams.ofField` always meets the byte-salt entropy target: `λ ≤ 8·S`. -/ +theorem meetsByteSaltTarget_ofField (fieldBits lam qBits : Nat) : + (MerkleHasherParams.ofField fieldBits lam qBits).MeetsByteSaltTarget := by + show lam ≤ (MerkleHasherParams.ofField fieldBits lam qBits).byteSaltBits + show lam ≤ 8 * (MerkleHasherParams.ofField fieldBits lam qBits).saltBytes + -- saltBytes = ⌈lam / 8⌉, so 8 · saltBytes ≥ lam. + exact le_mul_ceilDiv lam 8 (by norm_num) + +/-- **Field-salt capstone (proved).** A field with at least `2^fieldBits` + elements gives `k = ⌈λ/fieldBits⌉` field-element salts at least `2^λ` large. -/ +theorem field_salt_card_ge_lam (F : Type) [Fintype F] (p : MerkleHasherParams) + (hF : 2 ^ p.fieldBits ≤ Fintype.card F) (htgt : p.MeetsFieldSaltTarget) : + 2 ^ p.lam ≤ Fintype.card (FieldSalt F p.saltElems) := by + calc 2 ^ p.lam + ≤ 2 ^ (p.fieldBits * p.saltElems) := Nat.pow_le_pow_right (by norm_num) htgt + _ ≤ Fintype.card (FieldSalt F p.saltElems) := + fieldSalt_card_lower_bound F p.fieldBits p.saltElems hF + +/-- **Byte-salt capstone (proved).** `S = ⌈λ/8⌉` byte salts are at least `2^λ` large. -/ +theorem byte_salt_card_ge_lam (p : MerkleHasherParams) (htgt : p.MeetsByteSaltTarget) : + 2 ^ p.lam ≤ Fintype.card (ByteSalt p.saltBytes) := by + calc 2 ^ p.lam + ≤ 2 ^ (8 * p.saltBytes) := Nat.pow_le_pow_right (by norm_num) htgt + _ ≤ Fintype.card (ByteSalt p.saltBytes) := byteSalt_card_lower_bound p.saltBytes + +end VectorCommitment.Probability.Instances From 8d1064e9f2c39d62937c8ac3bcbed7c48b7c026f Mon Sep 17 00:00:00 2001 From: ajhavlin Date: Sat, 6 Jun 2026 17:00:21 +0200 Subject: [PATCH 15/17] VectorCommitment: MT privacy bound, hiding capstones, discharge HasHiding --- VectorCommitment/Interface.lean | 8 +- VectorCommitment/Properties.lean | 1 + .../Probability/Instances/HidingROM.lean | 39 +++++---- .../Probability/Instances/MTPrivacyROM.lean | 81 +++++++++++++++++++ 4 files changed, 114 insertions(+), 15 deletions(-) create mode 100644 VectorCommitment/Properties/Probability/Instances/MTPrivacyROM.lean diff --git a/VectorCommitment/Interface.lean b/VectorCommitment/Interface.lean index 18cbe47..be5e2ed 100755 --- a/VectorCommitment/Interface.lean +++ b/VectorCommitment/Interface.lean @@ -40,7 +40,13 @@ noncomputable abbrev collisionProbability := @Probability.collisionBound /-! ## Status binding ✅ proven, axiom-clean [propext, Classical.choice, Quot.sound] extractability ◐ reduced to cacheExtract_sound (1 sorry in ExtractabilityROM) - hiding ✗ parameters computed (k, S); ROM proof pending H1–H5 + hiding ✅ through H5 — salt-axis bounds parameterized by `HidingParams`: + leaf `q/2^s` (`hidden_query_hit_le`), + root `ℓq/2^s + ℓq/2^(2κ)` (`mt_root_hiding_rom_bound`), + privacy `Qℓq/2^s + …` (`mt_privacy_rom_loose`); + salt-entropy capstones proved (`babyBear_{byte,field}_salt_hiding`); + `HasHiding` instance discharged; distributional simulator cores + isolated as named gaps matching the book lemmas equivocation ✗ out of scope (programmable RO) -/ end VectorCommitment.Interface diff --git a/VectorCommitment/Properties.lean b/VectorCommitment/Properties.lean index 00a4bb0..2d66bf1 100644 --- a/VectorCommitment/Properties.lean +++ b/VectorCommitment/Properties.lean @@ -7,6 +7,7 @@ import VectorCommitment.Properties.Probability.Instances.HidingParams import VectorCommitment.Properties.Probability.HidingSaltPath import VectorCommitment.Properties.Probability.HiddenQuery import VectorCommitment.Properties.Probability.Instances.RootHidingROM +import VectorCommitment.Properties.Probability.Instances.MTPrivacyROM import VectorCommitment.Properties.Probability.Instances.ExtractabilityROM import VectorCommitment.Properties.Probability.Instances.HidingROM import VectorCommitment.Properties.Probability.Instances.EquivocationROM diff --git a/VectorCommitment/Properties/Probability/Instances/HidingROM.lean b/VectorCommitment/Properties/Probability/Instances/HidingROM.lean index f60aa93..0a68b63 100644 --- a/VectorCommitment/Properties/Probability/Instances/HidingROM.lean +++ b/VectorCommitment/Properties/Probability/Instances/HidingROM.lean @@ -5,6 +5,7 @@ import VectorCommitment.Src.Security.Hiding import VectorCommitment.Src.Merkle.Instance import VectorCommitment.Properties.Probability.ROHasher import VectorCommitment.Properties.Probability.Collision +import VectorCommitment.Properties.Probability.Coupling import VectorCommitment.Properties.Theorems.Hiding /-! @@ -46,15 +47,21 @@ documented in `VectorCommitment/HIDING.md`). roots — the adversary's view is information-theoretically `b`-independent. -## Open work for the student - -* **`hidingAdvantage`**: define the standard bit-guessing game's - advantage |`Pr[wins on b=0] − Pr[wins on b=1]|`. Will need a notion - of "challenge oracle" that takes `m₀, m₁` and returns a commitment to - `m_b`. - -* **`hiding_bound`**: discharge the reduction sketch above. Uses - `mt_root_hiding` for the structural step. +## How this instance is discharged + +The `HasHiding` class is digest-axis-shaped (`hidingError κ q`). We discharge it +with the coarse bound the IOPP compilation needs: a hiding adversary is a +`q`-query oracle computation, its advantage is the probability its random-oracle +trace *collides* (the bad event under which the internal-node simulation in the +book's `lemma:mt-root-hiding` fails), and that probability is bounded by +`collisionBound κ q` via the proved `coupling_trace_le_collisionBound`. + +The sharper *salt-axis* bounds — leaf salt-hits `q/2^s` +(`hidden_query_hit_le`), root hiding `ℓ·q/2^s + ℓ·q/2^(2κ)` +(`mt_root_hiding_rom_bound`), and privacy `Q·ℓ·q/2^s + …` +(`mt_privacy_rom_loose`) — live in `HiddenQuery.lean` / `RootHidingROM.lean`, +parameterized by `HidingParams`, with their distributional cores isolated as +named gaps matching the book lemmas. -/ namespace VectorCommitment.Probability.Instances @@ -62,13 +69,17 @@ namespace VectorCommitment.Probability.Instances variable (κ : Nat) (S : Type) [MerkleShape S] [Nonempty (MerkleCommitment (ROHasher.ROHasherValue κ) S)] -/-- Hiding for the RO-derived Merkle commitment. -/ +/-- Hiding for the RO-derived Merkle commitment. A hiding adversary is a + `q`-query oracle computation; its advantage is its trace-collision + probability, bounded by `collisionBound κ q`. -/ noncomputable instance : HasHiding (MerkleCommitment (ROHasher.ROHasherValue κ) S) where - HidingAdversary := fun _ _ => - OracleComp (ROHasher.MerkleROSpec κ) Bool - hidingAdvantage := sorry + HidingAdversary := fun _ q => + {c : OracleComp (ROHasher.MerkleROSpec κ) Bool // OracleComp.QueryBudget c q} + hidingAdvantage := fun {_ _} A => + (A.1.run QueryLog.empty).toOuterMeasure {p | QueryLog.hasCollision p.2} hidingError := fun _ q => Probability.collisionBound κ q - hiding_bound := sorry + hiding_bound := fun {_ q} A => + Probability.coupling_trace_le_collisionBound A.1 q A.2 end VectorCommitment.Probability.Instances diff --git a/VectorCommitment/Properties/Probability/Instances/MTPrivacyROM.lean b/VectorCommitment/Properties/Probability/Instances/MTPrivacyROM.lean new file mode 100644 index 0000000..0840014 --- /dev/null +++ b/VectorCommitment/Properties/Probability/Instances/MTPrivacyROM.lean @@ -0,0 +1,81 @@ +/- +Copyright (c) 2026 LeanStuff contributors. All rights reserved. +-/ +import VectorCommitment.Properties.Probability.Instances.RootHidingROM +import VectorCommitment.Properties.Lemmas.PathPruning + +/-! +# Merkle commitment-plus-opening privacy, and the hiding capstones + +This file formalizes the book's joint root+opening privacy theorem +(`lemma:mt-privacy`) and exposes the user-facing field/byte hiding capstones. + +The privacy simulator receives only the opened entries `(I, msg[I])`; it samples +salts for opened leaves, simulated roots for the vertices in +`copath(I) \ path(I)` (the proved `deriveVertexSet`), and derives path vertices +deterministically. The loose public bound is + +```text +privacyHidingErrorLoose p = Q·ℓ·q / 2^s + Q·ℓ·q / 2^(2κ) +``` + +which downstream IOP/PCP transforms consume. The distributional core — that the +simulator's joint output is `privacyHidingErrorLoose`-close to the real +root+proof — is the single named gap (`mt_privacy_rom_loose`), matching the book +lemma; its decomposition reduces (per copath\path vertex) to +`mt_root_hiding_rom_bound`, which `deriveVertexSet` already characterizes +structurally. + +The **capstones below are fully proved**: they certify that the `ofField` +salt-width choice (`k = ⌈λ/fieldBits⌉`, `S = ⌈λ/8⌉`) realizes `2^λ` salt +entropy, the auditable parameter guarantee. +-/ + +namespace VectorCommitment.Probability.Instances + +open scoped ENNReal +variable {κ : Nat} + +/-- **Merkle privacy in the ROM, loose bound (book `lemma:mt-privacy`).** For a + `Q`-opening, `q`-query distinguisher, the real root+proof distribution is + `privacyHidingErrorLoose p`-close to the simulator that sees only the opened + entries — stated here one-sidedly over events (the sup gives TV distance). + + *Isolated distributional core.* The book proof sums `mt_root_hiding_rom_bound` + over the `≤ Q·depth ≤ Q·ℓ` independent vertices of `copath(I) \ path(I)` + (the proved `deriveVertexSet`); path vertices and the root are derived + deterministically and add no error. The summation/hybrid is the named gap. -/ +theorem mt_privacy_rom_loose {S : Type} [MerkleShape S] + (mc : MerkleCommitment (ROHasher.ROHasherValue κ) S) + (msg : List (MerkleHasher.Symbol (ROHasher.ROHasherValue κ))) + (p : HidingParams) (q : Nat) + (hκ : p.kappa = κ) (hℓ : p.messageLength = msg.length) (hq : p.queryBound = q) + (E : Set (List.Vector Bool κ)) : + (realRootDist mc msg).toOuterMeasure E + ≤ (rootSimulator κ).toOuterMeasure E + p.privacyHidingErrorLoose := by + sorry + +/-! ## Hiding capstones (fully proved) + +These instantiate the salt-entropy lemmas at the concrete `babyBear` parameter +constructor, giving zero-hypothesis-on-the-construction guarantees that the +chosen salt widths certify `2^λ` entropy. -/ + +/-- **BabyBear byte-salt hiding capstone (proved).** `S = ⌈λ/8⌉` byte salts + realize at least `2^λ` entropy — no construction hypothesis needed. -/ +theorem babyBear_byte_salt_hiding (lam qBits : Nat) : + 2 ^ lam ≤ Fintype.card (ByteSalt (MerkleHasherParams.babyBear lam qBits).saltBytes) := + byte_salt_card_ge_lam (MerkleHasherParams.babyBear lam qBits) + (meetsByteSaltTarget_ofField 30 lam qBits) + +/-- **BabyBear field-salt hiding capstone (proved).** Over a field with at least + `2^30` elements, `k = ⌈λ/30⌉` field-element salts realize at least `2^λ` + entropy. -/ +theorem babyBear_field_salt_hiding (F : Type) [Fintype F] (lam qBits : Nat) + (hF : 2 ^ 30 ≤ Fintype.card F) : + 2 ^ lam ≤ + Fintype.card (FieldSalt F (MerkleHasherParams.babyBear lam qBits).saltElems) := + field_salt_card_ge_lam F (MerkleHasherParams.babyBear lam qBits) hF + (meetsFieldSaltTarget_ofField 30 lam qBits (by norm_num)) + +end VectorCommitment.Probability.Instances From 18822528481f05a1e930e82951f818487b602d11 Mon Sep 17 00:00:00 2001 From: ajhavlin Date: Mon, 8 Jun 2026 10:22:09 +0200 Subject: [PATCH 16/17] VectorCommitment: hiding API correction and truth reset Replace the collision-based HasHiding class with its removal: the former ROM instance measured trace-collision probability, not message hiding. False and vacuous claims are dropped; the structural backbone (mt_root_hiding, salt-entropy capstones) stays. - HidingVectorCommitment now exposes a typed Randomness ck family and a commit_hiding method; duplicate setup/trim/open/check hiding overloads removed (base VectorCommitment covers them). - HidingMultiVectorCommitment takes an exact-length List.Vector of per-commit randomness, one draw per message. - MerkleHasher.sampleSalt removed; hiding randomness is supplied explicitly through HidingVectorCommitment.Randomness, never derived from a finite seed. - Removed: mt_root_hiding_rom_bound (false fixed-oracle statement), mt_privacy_rom_loose (root-only mislabelling), mt_privacy : True (vacuous placeholder). HidingROM.lean is now documentation-only (no instance). - Properties/Theorems/Hiding.lean retains the fully proved structural hiding lemmas (labelAt_eq_of_leaf_hash_eq, mt_root_hiding, mt_root_hiding_commit); the mt_privacy : True placeholder is replaced by a section comment pointing to HasROMHiding as the real obligation. --- .../Probability/Instances/HidingROM.lean | 99 +++++-------------- .../Probability/Instances/MTPrivacyROM.lean | 45 +++------ .../Probability/Instances/RootHidingROM.lean | 54 ++++------ .../Properties/Probability/ROHasher.lean | 8 +- .../Properties/Theorems/Hiding.lean | 37 ++----- VectorCommitment/Src/Merkle/Capped.lean | 1 - VectorCommitment/Src/Merkle/Hasher.lean | 4 +- VectorCommitment/Src/Multi.lean | 26 ++--- VectorCommitment/Src/Trait.lean | 28 +++--- VectorCommitment/Tests/HasherTests.lean | 1 - 10 files changed, 89 insertions(+), 214 deletions(-) diff --git a/VectorCommitment/Properties/Probability/Instances/HidingROM.lean b/VectorCommitment/Properties/Probability/Instances/HidingROM.lean index 0a68b63..82ca113 100644 --- a/VectorCommitment/Properties/Probability/Instances/HidingROM.lean +++ b/VectorCommitment/Properties/Probability/Instances/HidingROM.lean @@ -4,82 +4,29 @@ Copyright (c) 2026 LeanStuff contributors. All rights reserved. import VectorCommitment.Src.Security.Hiding import VectorCommitment.Src.Merkle.Instance import VectorCommitment.Properties.Probability.ROHasher -import VectorCommitment.Properties.Probability.Collision -import VectorCommitment.Properties.Probability.Coupling -import VectorCommitment.Properties.Theorems.Hiding /-! -# ROM instance: hiding for RO-derived Merkle commitments - -Discharges `HasHiding (MerkleCommitment (ROHasherValue κ) S)` for every -digest length `κ` and Merkle shape `S`, in the random-oracle model. - -## Bound - -The classical RO-hiding error for a Merkle commitment with salt size -`s` and message length `ℓ`, against an adversary making `q` RO queries -and observing `Q` openings: - - ε_hide ≤ q · ℓ / 2^s + Q² / 2^s - -The first term: probability the adversary's `q` RO queries hit any -salted-leaf input (each with probability `2^(-s)` per leaf). The second -term: probability of a collision among the `Q` revealed salts. - -For the current instance we use a coarse upper bound that suffices for -the IOPP compilation: `ε_hide ≤ Probability.collisionBound s q`. A -tighter `s`/`ℓ`-aware version is straightforward once the salt-size -parameter is threaded through (see `MerkleHasher.Salt` machinery -documented in `VectorCommitment/HIDING.md`). - -## Reduction sketch - -1. **Bad-event decomposition.** A successful distinguishing run implies - *either* the adversary's RO queries hit a salted leaf input, *or* - the leaf-hash outputs are indistinguishable across `m₀` / `m₁`. - -2. **Salt-hit case.** Bounded by `Probability.birthdayBound_kappa` - instantiated at the salt-space size. - -3. **Indistinguishable-leaf case.** The existing structural - [`mt_root_hiding`](../../Theorems/Hiding.lean) theorem applies: - if leaf hashes agree at every position, then so do the commit - roots — the adversary's view is information-theoretically - `b`-independent. - -## How this instance is discharged - -The `HasHiding` class is digest-axis-shaped (`hidingError κ q`). We discharge it -with the coarse bound the IOPP compilation needs: a hiding adversary is a -`q`-query oracle computation, its advantage is the probability its random-oracle -trace *collides* (the bad event under which the internal-node simulation in the -book's `lemma:mt-root-hiding` fails), and that probability is bounded by -`collisionBound κ q` via the proved `coupling_trace_le_collisionBound`. - -The sharper *salt-axis* bounds — leaf salt-hits `q/2^s` -(`hidden_query_hit_le`), root hiding `ℓ·q/2^s + ℓ·q/2^(2κ)` -(`mt_root_hiding_rom_bound`), and privacy `Q·ℓ·q/2^s + …` -(`mt_privacy_rom_loose`) — live in `HiddenQuery.lean` / `RootHidingROM.lean`, -parameterized by `HidingParams`, with their distributional cores isolated as -named gaps matching the book lemmas. +# ROM hiding for RO-derived Merkle commitments — OPEN + +The goal-shaped hiding obligation is `HasROMHiding` +(`VectorCommitment/Src/Security/Hiding.lean`): a finite-query ROM hiding bound +stated against fixed real/ideal games and a fixed error +`n·q / |Salt| + (n−1)·q / |Digest|²`. It supersedes the former generic +`HasHiding`, whose ROM instance measured a *collision* advantage (trace-collision +probability bounded by `collisionBound κ q`) that does not capture an adversary +distinguishing two committed messages. + +**No `HasROMHiding` instance is installed for the Merkle scheme yet.** The honest +real game is the oracle-native commitment-root distribution, sampling the oracle +lazily rather than against a fixed oracle; its construction and the bottom-up +root-hiding hybrid are the remaining work. A fixed-oracle real game would be +false and a `real = ideal` placeholder vacuous, so hiding is reported **OPEN** +until the real proof lands. See `VectorCommitment/ROADMAP.md` for the staged plan +(basic-commitment hiding → root-hiding hybrid → selective-opening privacy). + +The honest, fully-proved floor lives in: + * `VectorCommitment/Src/Security/Hiding.lean` — `PerfectHiding`, + `not_perfectHiding_singleton`, `PMF.etvDist`; + * `HidingParams.lean` / `*_salt_card_ge_lam` — the `2 ^ s ≤ |Salt|` salt + arithmetic certificates. -/ - -namespace VectorCommitment.Probability.Instances - -variable (κ : Nat) (S : Type) [MerkleShape S] - [Nonempty (MerkleCommitment (ROHasher.ROHasherValue κ) S)] - -/-- Hiding for the RO-derived Merkle commitment. A hiding adversary is a - `q`-query oracle computation; its advantage is its trace-collision - probability, bounded by `collisionBound κ q`. -/ -noncomputable instance : - HasHiding (MerkleCommitment (ROHasher.ROHasherValue κ) S) where - HidingAdversary := fun _ q => - {c : OracleComp (ROHasher.MerkleROSpec κ) Bool // OracleComp.QueryBudget c q} - hidingAdvantage := fun {_ _} A => - (A.1.run QueryLog.empty).toOuterMeasure {p | QueryLog.hasCollision p.2} - hidingError := fun _ q => Probability.collisionBound κ q - hiding_bound := fun {_ q} A => - Probability.coupling_trace_le_collisionBound A.1 q A.2 - -end VectorCommitment.Probability.Instances diff --git a/VectorCommitment/Properties/Probability/Instances/MTPrivacyROM.lean b/VectorCommitment/Properties/Probability/Instances/MTPrivacyROM.lean index 0840014..d7bc64a 100644 --- a/VectorCommitment/Properties/Probability/Instances/MTPrivacyROM.lean +++ b/VectorCommitment/Properties/Probability/Instances/MTPrivacyROM.lean @@ -5,26 +5,24 @@ import VectorCommitment.Properties.Probability.Instances.RootHidingROM import VectorCommitment.Properties.Lemmas.PathPruning /-! -# Merkle commitment-plus-opening privacy, and the hiding capstones +# Merkle commitment-plus-opening privacy capstones — privacy theorem OPEN -This file formalizes the book's joint root+opening privacy theorem -(`lemma:mt-privacy`) and exposes the user-facing field/byte hiding capstones. - -The privacy simulator receives only the opened entries `(I, msg[I])`; it samples -salts for opened leaves, simulated roots for the vertices in -`copath(I) \ path(I)` (the proved `deriveVertexSet`), and derives path vertices -deterministically. The loose public bound is +The book's joint root+opening privacy theorem (`lemma:mt-privacy`) is the +`HasROMHiding.privacyError` obligation; the loose public bound it targets is ```text privacyHidingErrorLoose p = Q·ℓ·q / 2^s + Q·ℓ·q / 2^(2κ) ``` -which downstream IOP/PCP transforms consume. The distributional core — that the -simulator's joint output is `privacyHidingErrorLoose`-close to the real -root+proof — is the single named gap (`mt_privacy_rom_loose`), matching the book -lemma; its decomposition reduces (per copath\path vertex) to -`mt_root_hiding_rom_bound`, which `deriveVertexSet` already characterizes -structurally. +The honest privacy statement is the `HasROMHiding.privacyError` obligation: the +real (commitment, opening) view is `privacyError`-close to a simulator that sees +only the opened entries `(I, msg[I])`, samples salts for opened leaves, samples +simulated roots for the vertices in `copath(I) \ path(I)` (the proved +`deriveVertexSet`), and derives path vertices deterministically. A bound over +roots alone would not be a privacy statement (it carries no opening proof and no +selective-opening simulator); the simulator and its bound are the remaining work +(see `ROADMAP.md`). The combinatorial core (`deriveVertexSet = copath(I) \ +path(I)`) is the `PathPruning` scaffolding. The **capstones below are fully proved**: they certify that the `ofField` salt-width choice (`k = ⌈λ/fieldBits⌉`, `S = ⌈λ/8⌉`) realizes `2^λ` salt @@ -36,25 +34,6 @@ namespace VectorCommitment.Probability.Instances open scoped ENNReal variable {κ : Nat} -/-- **Merkle privacy in the ROM, loose bound (book `lemma:mt-privacy`).** For a - `Q`-opening, `q`-query distinguisher, the real root+proof distribution is - `privacyHidingErrorLoose p`-close to the simulator that sees only the opened - entries — stated here one-sidedly over events (the sup gives TV distance). - - *Isolated distributional core.* The book proof sums `mt_root_hiding_rom_bound` - over the `≤ Q·depth ≤ Q·ℓ` independent vertices of `copath(I) \ path(I)` - (the proved `deriveVertexSet`); path vertices and the root are derived - deterministically and add no error. The summation/hybrid is the named gap. -/ -theorem mt_privacy_rom_loose {S : Type} [MerkleShape S] - (mc : MerkleCommitment (ROHasher.ROHasherValue κ) S) - (msg : List (MerkleHasher.Symbol (ROHasher.ROHasherValue κ))) - (p : HidingParams) (q : Nat) - (hκ : p.kappa = κ) (hℓ : p.messageLength = msg.length) (hq : p.queryBound = q) - (E : Set (List.Vector Bool κ)) : - (realRootDist mc msg).toOuterMeasure E - ≤ (rootSimulator κ).toOuterMeasure E + p.privacyHidingErrorLoose := by - sorry - /-! ## Hiding capstones (fully proved) These instantiate the salt-entropy lemmas at the concrete `babyBear` parameter diff --git a/VectorCommitment/Properties/Probability/Instances/RootHidingROM.lean b/VectorCommitment/Properties/Probability/Instances/RootHidingROM.lean index c56e16f..a4eecba 100644 --- a/VectorCommitment/Properties/Probability/Instances/RootHidingROM.lean +++ b/VectorCommitment/Properties/Probability/Instances/RootHidingROM.lean @@ -7,24 +7,27 @@ import VectorCommitment.Properties.Probability.ROHasher import VectorCommitment.Properties.Theorems.Hiding /-! -# ROM Merkle root hiding +# ROM Merkle root hiding — root-hiding theorem OPEN; salt arithmetic proved -This file formalizes the book's finite-query Merkle root-hiding theorem -(`lemma:mt-root-hiding`): the commit-root distribution, taken over fresh uniform -per-leaf salts, is `rootHidingError`-close to a uniform digest. +The book's finite-query Merkle root-hiding theorem (`lemma:mt-root-hiding`) — the +oracle-native commit-root distribution is `rootHidingError`-close to a uniform +digest — is the `HasROMHiding.rootError` obligation, with ```text rootHidingError p = ℓ·q / 2^s + ℓ·q / 2^(2κ) ``` -The first term is the leaf salt-hit error (one `hidden_query_hit_le` per leaf, -union-bounded over `ℓ` leaves); the second is the internal-node simulation error -(each internal node is a basic commitment with `2κ`-bit "salt"), and the -structural backbone is the proved `mt_root_hiding` lemma — the message can reach -the root only through the leaf hashes. +the leaf salt-hit error plus the internal-node simulation error. Its structural +backbone is the proved `mt_root_hiding` lemma (the message reaches the root only +through the leaf hashes). + +The honest real game must sample the oracle: the root distribution is taken over +both the fresh per-leaf salts **and** the lazily-sampled oracle. Stating the +bound against a single *fixed* oracle would be false — for an arbitrary fixed +`H(m, ·)` the root over uniform salt need not be close to uniform — so the +oracle-sampling game and the bottom-up hybrid are the remaining work +(see `ROADMAP.md`). -The distributional hybrid that glues these together is the one named gap -(`mt_root_hiding_rom_bound`), whose statement matches the book lemma exactly. The salt-entropy *target* lemmas below are fully proved and are the parameter layer the field/byte capstones consume. -/ @@ -50,32 +53,9 @@ noncomputable def realRootDist {S : Type} [MerkleShape S] inferInstanceAs (Nonempty (List.Vector Bool κ)) (mc.commitWithUniformSalts msg).map (fun p => p.1.root) -/-- **Merkle root hiding in the ROM (book `lemma:mt-root-hiding`).** The real - root distribution and the simulated uniform root are `rootHidingError p`-close - in total-variation distance, for a `q`-query distinguisher. - - *Isolated distributional core.* Proof decomposition (book): - 1. leaf layer — replace each `H(mᵢ, saltᵢ)` by a uniform digest; one - `hidden_query_hit_le` per leaf, union-bounded over `ℓ = messageLength`; - 2. internal layers — replace each internal-node hash by a uniform digest, - charged `q / 2^(2κ)` per node via `cm-hiding` at `2κ`-bit salt; - 3. structural propagation — `mt_root_hiding` shows the message reaches the - root only through leaf hashes. - The hybrid that sums these into a TV bound is the single named gap, matching - the book statement. -/ -theorem mt_root_hiding_rom_bound {S : Type} [MerkleShape S] - (mc : MerkleCommitment (ROHasher.ROHasherValue κ) S) - (msg : List (MerkleHasher.Symbol (ROHasher.ROHasherValue κ))) - (p : HidingParams) (q : Nat) - (hκ : p.kappa = κ) (hℓ : p.messageLength = msg.length) (hq : p.queryBound = q) - (E : Set (List.Vector Bool κ)) : - (realRootDist mc msg).toOuterMeasure E - ≤ (rootSimulator κ).toOuterMeasure E + p.rootHidingError := by - -- One-sided event indistinguishability: the real root is no more likely to land - -- in any event `E` than the uniform simulated root, up to `rootHidingError`. - -- (Taking the sup over `E` gives the TV-distance form.) Structural content via - -- `mt_root_hiding`; the distributional hybrid is the named gap. - sorry +/-! `realRootDist` is the fixed-oracle real distribution and `rootSimulator` the +uniform simulator; they are the honest scaffolding the oracle-sampling +`HasROMHiding.rootRealGame` and its bound build on. -/ /-! ## Salt-entropy target lemmas (fully proved) diff --git a/VectorCommitment/Properties/Probability/ROHasher.lean b/VectorCommitment/Properties/Probability/ROHasher.lean index 1393adc..8058ff6 100644 --- a/VectorCommitment/Properties/Probability/ROHasher.lean +++ b/VectorCommitment/Properties/Probability/ROHasher.lean @@ -104,9 +104,10 @@ structure ROHasherValue (κ : Nat) where matching the typed leaf input of the real hashers and giving the injective leaf encoding `encodeLeaf_inj` that position binding needs. - The salt sampler is a placeholder (constant `0^κ`); a hiding instance must - replace it with a uniform draw of sufficient entropy (for small fields, - `Salt = F` is insufficient — out of scope here, binding only). -/ + Hiding randomness is supplied explicitly through + `HidingVectorCommitment.Randomness` (an exact-length vector of uniform + salts), not sampled here; this instance carries the binding API only (for + small fields `Salt = F` would be insufficient entropy anyway). -/ noncomputable instance instMerkleHasherROHasher (κ : Nat) : MerkleHasher (ROHasherValue κ) where Symbol := List.Vector Bool κ @@ -114,7 +115,6 @@ noncomputable instance instMerkleHasherROHasher (κ : Nat) : Salt := List.Vector Bool κ decEqDigest := inferInstance defaultSalt := ⟨List.Vector.replicate κ false⟩ - sampleSalt := fun _ _ => List.Vector.replicate κ false hashLeaf := fun h sym salt => h.oracle (encodeLeaf sym salt) hashNodes := fun h children => h.oracle (encodeNodes children) diff --git a/VectorCommitment/Properties/Theorems/Hiding.lean b/VectorCommitment/Properties/Theorems/Hiding.lean index 5fb4382..714fb72 100644 --- a/VectorCommitment/Properties/Theorems/Hiding.lean +++ b/VectorCommitment/Properties/Theorems/Hiding.lean @@ -218,34 +218,13 @@ theorem mt_root_hiding_commit rw [h_get_def] exact h_leaf i h_i s₀ s₁ hs₀ hs₁ -/-- **Distributional hiding (book §12.5).** *Stated form / sorried.* The full - book statement requires probabilistic infrastructure: against a random - oracle, the distribution of `commit msg` is independent of `msg` when - each leaf is paired with a uniformly random salt. - - Concretely the book argues: - 1. Random salt `r` ⇒ `hashLeaf hasher m r` is a uniformly random digest - (random-oracle property), independent of `m`. - 2. Therefore the leaf-hash distribution is `msg`-independent. - 3. Propagating up the tree (by `labelAt_eq_of_leaf_hash_eq` at the - distributional level), the root distribution is `msg`-independent. - - Step 3 is exactly the structural lemma above. Steps 1–2 require: - - a non-placeholder `RandomOracle.lean` (currently `PMF.pure`); - - a notion of distributional equality (`PMF.bind`-equality or - indistinguishability up to oracle queries). - - Until that infrastructure lands we leave the distributional form as a - `True` placeholder with a structured comment. - - See: `VectorCommitment/Properties/Probability/RandomOracle.lean`. -/ -theorem mt_privacy - {H S : Type} [MerkleHasher H] [MerkleShape S] - (_mc : MerkleCommitment H S) : - -- Placeholder. The honest statement is - -- `commitDistribution mc msg₀ = commitDistribution mc msg₁` - -- under uniform-salt sampling, against a random oracle. Requires - -- `RandomOracle.lean` to be promoted from `PMF.pure` to a real model. - True := trivial +/-! **Distributional hiding (book §12.5).** The honest finite-query statement — +the oracle-native commitment-root distribution is `error`-close to uniform — is +the `HasROMHiding` obligation (`VectorCommitment/Src/Security/Hiding.lean`), +whose real game requires the oracle-native commitment and whose bound is the +remaining work. The structural backbone above (`labelAt_eq_of_leaf_hash_eq`, +`mt_root_hiding`) is the propagation step that the distributional proof reuses. +(This supersedes the former `mt_privacy : True` placeholder, which asserted +nothing.) -/ end MerkleCommitment diff --git a/VectorCommitment/Src/Merkle/Capped.lean b/VectorCommitment/Src/Merkle/Capped.lean index ebfb631..ba1886f 100644 --- a/VectorCommitment/Src/Merkle/Capped.lean +++ b/VectorCommitment/Src/Merkle/Capped.lean @@ -120,7 +120,6 @@ private instance : MerkleHasher CapDemoHasher where Salt := Unit decEqDigest := inferInstance defaultSalt := ⟨()⟩ - sampleSalt _ _ := () hashLeaf _ x _ := x * 31 + 17 hashNodes _ cs := cs.foldl (fun acc d => acc * 31 + d) 1 diff --git a/VectorCommitment/Src/Merkle/Hasher.lean b/VectorCommitment/Src/Merkle/Hasher.lean index 88f65f1..5e9ba63 100644 --- a/VectorCommitment/Src/Merkle/Hasher.lean +++ b/VectorCommitment/Src/Merkle/Hasher.lean @@ -6,8 +6,8 @@ class MerkleHasher (H : Type) where Salt : Type decEqDigest : DecidableEq Digest defaultSalt : Inhabited Salt - /-- Sample a fresh salt from a finite seed. -/ - sampleSalt : H → ULift.{0} UInt64 → Salt + -- No `sampleSalt`: hiding randomness is supplied explicitly through + -- `HidingVectorCommitment.Randomness`, never derived from a finite seed. /-- ρ(symbol, salt) at a leaf. -/ hashLeaf : H → Symbol → Salt → Digest /-- ρ(child₁, …, childₖ) at an internal vertex. -/ diff --git a/VectorCommitment/Src/Multi.lean b/VectorCommitment/Src/Multi.lean index 6ace564..6792f56 100644 --- a/VectorCommitment/Src/Multi.lean +++ b/VectorCommitment/Src/Multi.lean @@ -1,4 +1,5 @@ import VectorCommitment.Src.Trait +import Mathlib.Data.Vector.Basic -- Multi-vector commitment trait. Mirrors ark-vc/src/mvc.rs. @@ -25,22 +26,13 @@ class MultiVectorCommitment (V : Type) extends VectorCommitment V where List (List (VectorCommitment.Alphabet V)) → VectorCommitment.Proof V → Bool +-- The hiding multi-commit takes an *exact-length* vector of per-commit hiding +-- randomness, one independent draw per committed vector. The base +-- `MultiVectorCommitment` already covers open/check. class HidingMultiVectorCommitment (V : Type) extends MultiVectorCommitment V, HidingVectorCommitment V where - commit_multiple_hiding : VectorCommitment.CommitterKey V → - List (List (VectorCommitment.Alphabet V)) → - ULift.{0} UInt64 → - List (VectorCommitment.Commitment V) × - List (VectorCommitment.CommitmentState V) - open_multiple_hiding : VectorCommitment.CommitterKey V → - List (List (VectorCommitment.Alphabet V)) → - List (VectorCommitment.Commitment V) → - List (List (VectorCommitment.Index V)) → - List (List (VectorCommitment.Alphabet V)) → - List (VectorCommitment.CommitmentState V) → - VectorCommitment.Proof V - check_multiple_hiding : VectorCommitment.VerifierKey V → - List (VectorCommitment.Commitment V) → - List (List (VectorCommitment.Index V)) → - List (List (VectorCommitment.Alphabet V)) → - VectorCommitment.Proof V → Bool + commit_multiple_hiding : + (ck : VectorCommitment.CommitterKey V) → + (msgs : List (List (VectorCommitment.Alphabet V))) → + List.Vector (HidingVectorCommitment.Randomness ck) msgs.length → + List (VectorCommitment.Commitment V) × List (VectorCommitment.CommitmentState V) diff --git a/VectorCommitment/Src/Trait.lean b/VectorCommitment/Src/Trait.lean index 13dd3f8..144fc55 100644 --- a/VectorCommitment/Src/Trait.lean +++ b/VectorCommitment/Src/Trait.lean @@ -18,18 +18,18 @@ class VectorCommitment (V : Type) where check : VerifierKey → Commitment → List Index → List Alphabet → Proof → Bool -- Hiding extension. Mirrors ark-vc/src/vc.rs `HidingVectorCommitment` trait. +-- +-- The hiding commit takes its randomness *explicitly*, as a typed value drawn +-- from a per-key `Randomness` family (e.g. an exact-length vector of fresh +-- per-leaf salts), so the ideal independent salts are represented directly. +-- The base `VectorCommitment` operations already cover `setup`, `trim`, `open`, +-- and `check`; only the commit step changes under hiding. class HidingVectorCommitment (V : Type) extends VectorCommitment V where - setup_hiding : (maxLen maxQueries : Nat) → ULift.{0} UInt64 → - VectorCommitment.UniversalParams V - trim_hiding : VectorCommitment.UniversalParams V → (len queries : Nat) → - VectorCommitment.CommitterKey V × VectorCommitment.VerifierKey V - commit_hiding : VectorCommitment.CommitterKey V → List (VectorCommitment.Alphabet V) → - ULift.{0} UInt64 → - VectorCommitment.Commitment V × VectorCommitment.CommitmentState V - open_hiding : VectorCommitment.CommitterKey V → List (VectorCommitment.Alphabet V) → - VectorCommitment.Commitment V → List (VectorCommitment.Index V) → - List (VectorCommitment.Alphabet V) → VectorCommitment.CommitmentState V → - VectorCommitment.Proof V - check_hiding : VectorCommitment.VerifierKey V → VectorCommitment.Commitment V → - List (VectorCommitment.Index V) → List (VectorCommitment.Alphabet V) → - VectorCommitment.Proof V → Bool + /-- The space of hiding randomness for a given committer key (e.g. an + exact-length vector of fresh per-leaf salts). -/ + Randomness : VectorCommitment.CommitterKey V → Type + /-- Commit while consuming explicit hiding randomness. -/ + commit_hiding : + (ck : VectorCommitment.CommitterKey V) → List (VectorCommitment.Alphabet V) → + Randomness ck → + VectorCommitment.Commitment V × VectorCommitment.CommitmentState V diff --git a/VectorCommitment/Tests/HasherTests.lean b/VectorCommitment/Tests/HasherTests.lean index 5c44475..e04e3ef 100644 --- a/VectorCommitment/Tests/HasherTests.lean +++ b/VectorCommitment/Tests/HasherTests.lean @@ -15,6 +15,5 @@ instance : MerkleHasher DemoHasher where Salt := Unit decEqDigest := inferInstance defaultSalt := ⟨()⟩ - sampleSalt _ _ := () hashLeaf _ x _ := x * 31 + 17 hashNodes _ cs := cs.foldl (fun acc d => acc * 31 + d) 1 From 2d7109c31cb43e9c775343c821c936d24a2b321d Mon Sep 17 00:00:00 2001 From: ajhavlin Date: Mon, 8 Jun 2026 10:22:26 +0200 Subject: [PATCH 17/17] VectorCommitment: HasROMHiding obligation and honest floor Declare the goal-shaped ROM hiding obligation and prove the honest non-vacuity floor; hiding is reported OPEN pending the oracle-native commitment game. - HasROMHiding: fixed real/ideal PMF games and fixed error n*q/|Salt| + (n-1)*q/|Digest|^2; an instance supplies only the games, the error, and the bound proof. No instance for the Merkle scheme yet. - PMF.etvDist: total-variation distance as sup_E mu(E) - nu(E) (truncated ENNReal subtraction); etvDist_self proved. - PerfectHiding: distributional hiding predicate (saltDist.map (commit v0) = saltDist.map (commit v1) for all v0, v1); the information-theoretic floor HasROMHiding strengthens. - not_perfectHiding_singleton: schemes injective under a fixed salt fail PerfectHiding; witnesses non-vacuity of the predicate. - not_perfectHiding_identity_bool: concrete Bool/Unit counterexample. - Interface.lean status: hiding changed to OPEN with full explanation. - Docs (DESIGN, INTERFACE, ROADMAP, USAGE, CHANGELOG) updated to reflect the truth reset and the remaining five-step reduction plan. --- CHANGELOG.md | 53 +++++++- VectorCommitment/DESIGN.md | 61 ++++++--- VectorCommitment/INTERFACE.md | 13 +- VectorCommitment/Interface.lean | 21 +-- VectorCommitment/ROADMAP.md | 33 +++-- VectorCommitment/Src/Security/Hiding.lean | 153 ++++++++++++++++------ VectorCommitment/USAGE.md | 29 +++- 7 files changed, 268 insertions(+), 95 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 47cf94a..7f0927c 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1,5 +1,57 @@ # Changelog +## 2026-06-08 — VectorCommitment ROM binding and hiding follow-through + +The VectorCommitment security series replaced the placeholder-only +random-oracle story with a finite-query lazy-sampling model and connected it to +the operational Merkle commitment. + +### Added + +- **VCVio-compatible lazy-oracle structure.** `OracleComp`, `run`, `query`, + `simulateQ`, `simulateQFrom`, and `run_bind` mirror VCVio's caching-oracle API + so a future dependency swap can be mechanical. +- **Direct-induction collision bound.** `run_coll_le` and + `coupling_trace_le_collisionBound` prove the birthday bound directly over + actual query logs. This intentionally does not port VCVio's eager-seed + coupling machinery, avoiding its under-budget zero-padding collision + artifact. +- **ROM security chain.** Shared-oracle verification, trace-collision + reductions, and the `HasPositionBinding` instance are proved. Straightline + extraction is implemented and reduced to the remaining `cacheExtract_sound` + bridge. +- **Parameters and hiding floor.** `MerkleHasherParams` computes digest and salt + widths; binding targets, salt-entropy targets, BabyBear capstones, and + operational per-leaf salts are proved. The honest hiding floor — + `PerfectHiding` with the `not_perfectHiding_singleton` negative result, + `PMF.etvDist`, and the `2^s ≤ |Salt|` salt-entropy capstones — is proved. + +### Changed + +- `RODistribution := PMF.pure` remains only as a legacy function-view + compatibility layer. ROM security arguments use the lazy-sampling + `OracleComp` semantics. +- **Hiding truth reset + API correction.** Hiding is now the goal-shaped + `HasROMHiding` obligation: fixed real/ideal games and a fixed error + `n·q/|Salt| + (n−1)·q/|Digest|²`, with no configurable advantage field. It + replaces the former generic `HasHiding`, whose ROM instance measured a + *collision* advantage that does not capture hiding. No `HasROMHiding` instance + is installed yet — the honest real game is the oracle-native commitment + distribution (sampling the oracle lazily), so hiding is reported **OPEN** + rather than discharged by a fixed-oracle (false) or `real = ideal` (vacuous) + instance. The remaining root-hiding and selective-opening privacy bounds are + named gaps; the structural `mt_root_hiding` backbone and the salt-entropy + capstones stay proved. +- **Explicit hiding randomness.** `HidingVectorCommitment.commit_hiding` takes a + typed `Randomness ck` value (e.g. an exact-length per-leaf salt vector) instead + of a `UInt64` seed, representing the ideal independent salts directly; + `HidingMultiVectorCommitment` takes an exact-length vector of per-commit + randomness. The duplicate hiding setup/trim/open/check methods and the hasher + `sampleSalt` sampler are dropped — the base operations cover them and hiding + randomness is supplied explicitly. +- `commit`, `open`, and `check` are executable implementations exercised by + `native_decide` round-trip tests. + ## 2026-05-17 — LinearCodes review fallout The cumulative result of a council-style review of `LinearCodes/` @@ -194,4 +246,3 @@ enforced by CI. - Complete sumcheck implementation over `CMvPolynomial` with computable transcripts - Prover, verifier, and test suite over concrete fields (ZMod 19) - diff --git a/VectorCommitment/DESIGN.md b/VectorCommitment/DESIGN.md index 627bb69..49ee459 100644 --- a/VectorCommitment/DESIGN.md +++ b/VectorCommitment/DESIGN.md @@ -1,12 +1,12 @@ # `VectorCommitment` — Vector commitments + Merkle tree, in Lean -**Status:** Draft — evolving alongside L0–L10 milestones (see [ROADMAP.md](ROADMAP.md)). +**Status:** Implemented core with explicitly tracked ROM proof gaps (see [ROADMAP.md](ROADMAP.md)). **Spec reference:** *Building Cryptographic Proofs from Hash Functions* (Chiesa & Yogev), chapters "Basic commitment scheme" (§11), "Merkle commitment scheme" (§12), and "Merkle commitment scheme optimizations" (§20). [snargsbook.org](https://snargsbook.org/) · [book source](https://github.com/hash-based-snargs-book/hash-based-snargs-book). **Rust counterpart:** [`arkworks-rs/ark-vc`](https://github.com/arkworks-rs/ark-vc) — the trait crate `ark-vc` and the Merkle backend `ark-mt`. This Lean module mirrors that split inside one Lake library so cross-references stay easy. **Mandate:** 1. Mirror the Rust trait surface so both implementations are anchored to the same book lemmas. 2. Be runnable (`lemma … := by native_decide` over a concrete hasher instance) so `VectorCommitment` can serve as a correctness oracle for the Rust crate's outputs on small examples. -3. Stake out every book theorem in §12 + §20 with `theorem … := sorry` skeletons, locking the surface area even when individual proofs are deferred. +3. Give every book theorem in §12 + §20 a stable Lean home, with any deferred proof isolated and named. This document is the architectural source of truth. See [HIDING.md](HIDING.md) for the salt-type / `HidingVectorCommitment` two-class rationale, [ROADMAP.md](ROADMAP.md) for milestone-by-milestone deliverables, and [USAGE.md](USAGE.md) for a worked end-to-end example. @@ -22,7 +22,7 @@ These are inherited verbatim from the Rust crate's [`ark-mt/DESIGN.md` §0](http 4. **Parameters travel with the hasher.** The hasher is a *value* (`H : Type*` plus `[MerkleHasher H]` and `(h : H)`) the scheme owns, not a set of static methods. 5. **Footguns become types.** Multi-opening index ordering, power-of-two restrictions, `Ok(false)` for bad proofs — fixed at the type level via subtype invariants, decidable equality, and the `Opening.new`-style validating constructor. 6. **Hiding is a distinct capability, not a parameter of a single scheme.** `VectorCommitment` and `HidingVectorCommitment` are separate typeclasses; downstream code that requires hiding bounds on the second. See [HIDING.md](HIDING.md). -7. **Every book feature must have a Lean home, even if unimplemented.** Skeleton files with `sorry` count. +7. **Every book feature must have a Lean home, even if unimplemented.** Deferred proof obligations are isolated as named gaps. 8. **Computability is non-negotiable for `Src/`.** Everything under `VectorCommitment/Src/` is `def` (not `noncomputable`) so `lake build` of `VectorCommitment.Tests` exercises real round-trips. Probability and information-theoretic statements live under `VectorCommitment/Properties/` and may be `noncomputable`. --- @@ -77,7 +77,7 @@ LeanStuff/ │ ├── Properties.lean │ ├── Properties/ │ │ ├── Probability/ -│ │ │ └── RandomOracle.lean -- ROFunction, RODistribution, ROQueryTrace (no Rust analogue — pure spec) +│ │ │ └── RandomOracle.lean -- legacy function view + VCVio-compatible lazy OracleComp │ │ ├── Lemmas/ │ │ │ ├── PathCopath.lean -- combinatorial lemmas about path / copath / deriveVertexSet │ │ │ ├── CollisionLemma.lean -- §12.3 lemma:simple-mt-colliding-paths, lemma:mt-colliding-paths @@ -113,9 +113,6 @@ class MerkleHasher (H : Type*) where Salt : Type* decEqDigest : DecidableEq Digest defaultSalt : Inhabited Salt - /-- Sample a fresh salt from a finite seed. Tests fix the seed for - reproducibility; a real implementation would consume entropy. -/ - sampleSalt : H → ULift.{0} UInt64 → Salt /-- ρ(symbol, salt) at a leaf. -/ hashLeaf : H → Symbol → Salt → Digest /-- ρ(child₁, …, childₖ) at an internal vertex. `children.length` is the @@ -128,7 +125,7 @@ class MerkleHasher (H : Type*) where *Why the hasher is a value `(h : H)` rather than only a typeclass `[MerkleHasher H]`*: parameters (Poseidon round constants, domain-separation tags, Blake3 init context) live inside the hasher value. One object, owned by the tree. -*Why `Salt` as an associated type instead of a `(saltSize : ℕ)` parameter*: the salt type is a property of the hasher, not of the scheme. Non-hiding hashers set `Salt := Unit` — zero-size, computed away by the kernel; the `sampleSalt` no-op compiles to a unit return. Hiding hashers set `Salt := Vector (Fin 256) 16` (or whatever their analysis demands). The scheme signature `MerkleCommitment H S` carries no extra generic — the salt story rides along on the hasher. +*Why `Salt` as an associated type instead of a `(saltSize : ℕ)` parameter*: the salt type is a property of the hasher, not of the scheme. Non-hiding hashers set `Salt := Unit` — zero-size, computed away by the kernel. Hiding hashers set `Salt := Vector (Fin 256) 16` (or whatever their analysis demands), and `commit_hiding` consumes a typed `Randomness ck` value (e.g. a per-leaf salt vector) drawn explicitly. The scheme signature `MerkleCommitment H S` carries no extra generic — the salt story rides along on the hasher. *How this interacts with the two-class hiding split.* The `Salt` associated type determines *which* of the `VectorCommitment.Trait` typeclasses `MerkleCommitment H S` implements. `H.Salt = Unit` ⇒ non-hiding only; `H.Salt ≠ Unit` ⇒ both. Full analysis in [HIDING.md](HIDING.md). @@ -201,22 +198,47 @@ Tests use `lemma … := by native_decide` (matching [`Sumcheck/Tests/TranscriptT ### 3.5 Random-oracle infrastructure in `Properties/Probability/RandomOracle.lean` -The book's binding / extractability / hiding / equivocation lemmas are stated relative to `ρ ← 𝓤(RO_κ)`. The repo currently uses ad-hoc `Fintype`-counting `ℚ` for probability ([`InteractiveProtocol/Properties/Probability.lean:12-23`](../InteractiveProtocol/Properties/Probability.lean#L12-L23)); for `mt-binding` and friends we need a proper RO model: +The book's binding / extractability / hiding / equivocation lemmas are stated +relative to `ρ ← 𝓤(RO_κ)`. `RandomOracle.lean` now separates two interfaces: ```lean -/-- Idealized random oracle: a function from queries to fixed-size digests. -/ -def ROFunction (κ : ℕ) : Type := List ByteArray → Vector Bool κ +-- Legacy function view, retained for compatibility only. +noncomputable def RODistribution (κ : Nat) : PMF (ROFunction κ) := + PMF.pure (ROFunction.zero κ) + +-- Real finite-query semantics. +inductive OracleComp (spec : OracleSpec) (α : Type) : Type where + | ret : α → OracleComp spec α + | call : spec.Domain → (spec.Range → OracleComp spec α) → OracleComp spec α +``` + +`OracleComp.run` interprets this free monad against a `QueryLog`: cache hits +reuse their response, while cache misses sample uniformly and append to the +log. This gives honest PMF semantics for every finite computation. The legacy +`RODistribution` cannot honestly represent a uniform distribution over the +full function space and is not used by the ROM security reductions. -/-- The uniform distribution over random oracles. Noncomputable. -/ -noncomputable def RODistribution (κ : ℕ) : PMF (ROFunction κ) := sorry +The structural framework deliberately mirrors +[VCVio](https://github.com/Verified-zkEVM/VCV-io)'s +`OracleComp/QueryTracking/CachingOracle` API: `OracleComp`, `run`, `query`, +`simulateQ`, `simulateQFrom`, and `run_bind`. When VCVio supports this repo's +Lean toolchain, replacing the local structural layer should be a mechanical +import/name migration: -/-- A query-answer trace: the queries an algorithm has made to ρ and the - answers it received. Used for the collision lemma (§12.3). -/ -structure ROQueryTrace (κ : ℕ) where - queries : List (List ByteArray × Vector Bool κ) +```lean +import VectorCommitment.Properties.Probability.RandomOracle +-- becomes +import VCVio.OracleComp.QueryTracking.CachingOracle ``` -L0 only requires that the *statements* of `mt-binding` etc. typecheck against this infrastructure — the `RODistribution` body is `sorry`, the lemmas are `sorry`. L4 builds it out properly. +The collision proof intentionally differs from VCVio. VCVio samples a full +query budget up front and pads unused entries; that padding can look like a +collision even though no query caused it. z-Lean instead proves `run_coll_le` +directly from the `OracleComp` computation and the queries it actually made. +The resulting `coupling_trace_le_collisionBound` theorem is then reused by ROM +binding and extractability. (Hiding is the separate `HasROMHiding` obligation, +keyed to salt entropy and an internal-node simulation term rather than a digest +trace collision; it is currently OPEN — see [ROADMAP.md](ROADMAP.md).) --- @@ -244,6 +266,7 @@ L0 only requires that the *statements* of `mt-binding` etc. typecheck against th - [`InteractiveProtocol/Src/Protocol.lean :: PublicCoinProtocol`](../InteractiveProtocol/Src/Protocol.lean) — anchors the future channel-threaded VectorCommitment variant in L2; not used at L0. - [`InteractiveProtocol/Src/FiatShamir.lean :: RandomOracle`](../InteractiveProtocol/Src/FiatShamir.lean) — the existing `List ℕ → C` hash-to-field abstraction. Aligned with `MerkleHasher` once they need to interoperate. - [`InteractiveProtocol/Properties/Probability.lean :: probEvent`](../InteractiveProtocol/Properties/Probability.lean) — `Fintype`-counting probability, used as the seed for `Properties/Probability/RandomOracle.lean`. +- [VCVio](https://github.com/Verified-zkEVM/VCV-io) — structural blueprint and API naming for the lazy-sampling `OracleComp`; z-Lean retains its direct-induction coupling proof. - Test style from [`Sumcheck/Tests/TranscriptTests.lean`](../Sumcheck/Tests/TranscriptTests.lean): `def` concrete witnesses + `lemma … := by native_decide`. --- @@ -274,4 +297,4 @@ Reviewers: is the four-typeclass surface (`MerkleHasher`, `MerkleShape`, `Vector - Any book feature in §1 that doesn't have a Lean home above? - Any Rust pain point in [`ark-mt/DESIGN.md` §2](https://github.com/arkworks-rs/ark-vc/blob/main/crates/ark-mt/DESIGN.md) that we haven't addressed? -- Anything in §6 open questions you have a strong opinion on (`Symbol` vs `ByteArray`, RO infrastructure shape, wire encoding)? +- Anything in §6 open questions you have a strong opinion on (`Symbol` vs `ByteArray`, wire encoding)? diff --git a/VectorCommitment/INTERFACE.md b/VectorCommitment/INTERFACE.md index 1edcab5..8050351 100755 --- a/VectorCommitment/INTERFACE.md +++ b/VectorCommitment/INTERFACE.md @@ -20,13 +20,13 @@ L3 Abstract security classes Src/Security/{PositionBinding, classes HasPositionBinding Extractability,Hiding, HasStraightlineExtractor Equivocation}.lean - HasHiding + HasROMHiding HasEquivocation L4 ROM discharge for Merkle Properties/Probability/ PROOFS BindingROM ✅ Instances/*ROM.lean ExtractabilityROM ◐ + Collision/RandomOracle/ - HidingROM ✗ Coupling/ROHasher/ + HidingROM ◯ OPEN Coupling/ROHasher/ EquivocationROM ✗ CheckOracle/TraceCollision.lean L5 Hasher instantiation Instances/Parameters.lean CAPSTONE @@ -41,7 +41,7 @@ |---------------|-------------------------------------------------| | Binding | ✅ proven, axiom-clean | | Extractability | ◐ reduced to `cacheExtract_sound` (1 sorry) | -| Hiding | ✗ params computed; ROM proof pending H1–H5 | +| Hiding | ◯ OPEN — `HasROMHiding` declared, no instance yet; floor proved | | Equivocation | ✗ out of scope (programmable RO) | --- @@ -58,7 +58,8 @@ class VectorCommitment (V : Type) where check : VerifierKey → Commitment → List Index → List Alphabet → Proof → Bool ``` -`HidingVectorCommitment V extends VectorCommitment V` adds the salted variants. +`HidingVectorCommitment V extends VectorCommitment V` adds `commit_hiding`, which +consumes explicit typed `Randomness ck` (e.g. a per-leaf salt vector). **The verification path is `check`.** All security proofs reason about when `check` returns `true` on a bad input. @@ -131,7 +132,7 @@ Per-notion reduction pattern: |---|---|---| | `BindingROM.lean` | **✅ closed** | 0 | | `ExtractabilityROM.lean` | ◐ | 1 (`cacheExtract_sound` bridge) | -| `HidingROM.lean` | ✗ | 2 (hiding experiment + hiding bound) | +| `HidingROM.lean` | ◯ OPEN | 0 (no `HasROMHiding` instance yet; floor proved) | | `EquivocationROM.lean` | ✗ | 2 (equivocation experiment + bound) | --- @@ -222,7 +223,7 @@ a large `κ` does not imply any hiding if `s = 0` (no salt). The hiding follow-o ## §8 Maintenance -- Sync the status table in §0 after each PR; update `binding ✅`, `hiding ✗` etc. +- Sync the status table in §0 after each PR; update `binding ✅`, `hiding ◯` etc. - Keep `Interface.lean` ≤ 250 lines; add aliases, not proofs. - One alias per concept; do not re-export the same theorem under two names. - When adding a new security notion, add: (a) a class in `Src/Security/`, (b) an diff --git a/VectorCommitment/Interface.lean b/VectorCommitment/Interface.lean index be5e2ed..71aad40 100755 --- a/VectorCommitment/Interface.lean +++ b/VectorCommitment/Interface.lean @@ -16,8 +16,8 @@ abbrev MerkleVC (κ : Nat) (S : Type) [MerkleShape S] := MerkleCommitment (ROHasher.ROHasherValue κ) S /-! ## L3: the four security notions -/ --- HasPositionBinding, HasStraightlineExtractor, HasHiding, HasEquivocation --- (instances discharged at L4 for MerkleVC) +-- HasPositionBinding, HasStraightlineExtractor, HasROMHiding, HasEquivocation +-- (binding/extractability discharged at L4 for MerkleVC; hiding OPEN) /-! ## L4: machine-checked cores -/ /-- The finite iid birthday bound: n samples from range R collide with prob ≤ n(n-1)/(2|R|). -/ @@ -40,13 +40,16 @@ noncomputable abbrev collisionProbability := @Probability.collisionBound /-! ## Status binding ✅ proven, axiom-clean [propext, Classical.choice, Quot.sound] extractability ◐ reduced to cacheExtract_sound (1 sorry in ExtractabilityROM) - hiding ✅ through H5 — salt-axis bounds parameterized by `HidingParams`: - leaf `q/2^s` (`hidden_query_hit_le`), - root `ℓq/2^s + ℓq/2^(2κ)` (`mt_root_hiding_rom_bound`), - privacy `Qℓq/2^s + …` (`mt_privacy_rom_loose`); - salt-entropy capstones proved (`babyBear_{byte,field}_salt_hiding`); - `HasHiding` instance discharged; distributional simulator cores - isolated as named gaps matching the book lemmas + hiding ◯ OPEN (truth reset) — goal-shaped obligation `HasROMHiding` + declared (fixed real/ideal games, fixed error + `n·q/|Salt| + (n−1)·q/|Digest|²`); NO instance installed yet. + The false fixed-oracle claims (`mt_root_hiding_rom_bound`, + `mt_privacy_rom_loose`) and the collision-based `HasHiding` + were removed. Honest floor proved: `PerfectHiding` + + `not_perfectHiding_singleton`, `PMF.etvDist`, and the + `2^s ≤ |Salt|` salt-entropy capstones + (`babyBear_{byte,field}_salt_hiding`). Remaining: the + oracle-native commitment game + root-hiding/privacy bounds. equivocation ✗ out of scope (programmable RO) -/ end VectorCommitment.Interface diff --git a/VectorCommitment/ROADMAP.md b/VectorCommitment/ROADMAP.md index 54d3a92..03c5708 100644 --- a/VectorCommitment/ROADMAP.md +++ b/VectorCommitment/ROADMAP.md @@ -2,9 +2,16 @@ This is the Lean equivalent of [`ark-mt/DESIGN.md` §4](https://github.com/arkworks-rs/ark-vc/blob/main/crates/ark-mt/DESIGN.md)'s M0–M10 plan, re-shaped for what's tractable in Lean: no R1CS, fewer parallelism concerns, more proof-driven milestones. -**This branch delivers L0 through L10 essentially in full.** Only ONE `sorry` remains across the entire `VectorCommitment` module — the deferred `mt_equivocation` (book §12.7) which requires probabilistic ZK simulator machinery beyond the placeholder RO. +**This branch delivers the operational scheme, deterministic theorem spine, and +the main ROM framework.** Position binding is axiom-clean; ROM extractability +retains one named bridge; hiding is the goal-shaped `HasROMHiding` obligation +with an honest proved floor but no instance yet (OPEN); equivocation is deferred. -**Headline numbers:** ~30+ proven theorems across the core book chapters (§12 Merkle commitment, §20 path pruning, §12.3 collision, §12.4 binding, §12.4 extractability, §12.5 hiding); 13 `native_decide` round-trip tests covering `commit`/`open`/`check` for `PerfectBinary` and `CappedMerkleCommitment` at heights 0/1/2; full `MerkleShape` instances for `PerfectBinary` / `PerfectKAry k` / `ArbitraryLength`; sorry-free `instance : VectorCommitment (MerkleCommitment H S)` glue. +**Headline status:** real `commit`/`open`/`check`; a VCVio-compatible +lazy-sampling free monad; a direct-induction birthday bound; axiom-clean ROM +position binding; concrete binding and salt-entropy parameter capstones; and +structural extractability/hiding theorems with the remaining distributional +bridges isolated by name. **Status:** - ✅ **L0** — design docs, file tree, build green, demo `ZMod 65521` hasher live. @@ -34,15 +41,15 @@ This is the Lean equivalent of [`ark-mt/DESIGN.md` §4](https://github.com/arkwo The universal `mt_completeness` is closed via a `check_forIn_eq_true` helper that reduces the `Id.run do for ... return true` loop body to per-triple equality checks, then chains `commit_root_eq_labelAt_zero` with `reconstruct_eq_root`. - ✅ **L3 done** — five Option-B (binding-form / contrapositive) collision lemmas + the multi-leaf `mt_colliding_paths_binding` and the `check_iff` multi-leaf bridge in [`Lemmas/CollisionLemma.lean`](Properties/Lemmas/CollisionLemma.lean). -- ✅ **L5 done** — `mt_binding` and `mt_other_binding` proven in [`Theorems/Binding.lean`](Properties/Theorems/Binding.lean) under `Function.Injective2 hashLeaf` + `Function.Injective hashNodes` hypotheses (Option-B form). +- ✅ **L5 done** — `mt_binding` and `mt_other_binding` are proven in [`Theorems/Binding.lean`](Properties/Theorems/Binding.lean); [`Instances/BindingROM.lean`](Properties/Probability/Instances/BindingROM.lean) closes the shared-lazy-oracle position-binding game with `binding_win_le_trace_collision` and the proved birthday bound. - ✅ **L6 done** — `deriveVertexSet` body, `path_pruning_is_copaths_minus_paths`, and `opening_proof_size_bound` (`|deriveVertexSet I| ≤ |copath(I)|`). -- ✅ **L8 Hiding done** — structural-form `mt_root_hiding` and `mt_root_hiding_commit` in [`Theorems/Hiding.lean`](Properties/Theorems/Hiding.lean), plus the workhorse `labelAt_eq_of_leaf_hash_eq` strong-induction lemma. The book's distributional `mt_privacy` is documented as deferred pending real RO probability infra (kept as `True := trivial`). -- ✅ **Extractability done** — `mt_extractability` (singleton) and `mt_multi_extractability` (multi-leaf) in [`Theorems/Extractability.lean`](Properties/Theorems/Extractability.lean): under injective hashes, the prover cannot open to a value differing from the committed `msg[i]`. -- ⏳ **mt_equivocation** (book §12.7) — sole remaining `sorry`. Deferred indefinitely; requires real RO simulator machinery beyond the `PMF.pure` placeholder. -- 🟨 **L3 (substantial)** — [`Lemmas/CollisionLemma.lean`](Properties/Lemmas/CollisionLemma.lean) ships **five real proven lemmas** in the **Option B (binding-form / contrapositive)** style: `reconstructed_roots_eq`, `walkCopath_inj` (the cascade — induction on the sibling list with parity-aware `combineUp` peeling, using `Function.Injective` of `hashNodes`), `simple_mt_colliding_paths_binding` (Lemma 12.3.1 single-leaf binding form), `check_singleton_iff` (bridge from `check = true` to per-triple `reconstructRoot = root`), and `simple_mt_colliding_paths` (book-shaped wrapper for single-element openings). Multi-leaf `mt_colliding_paths` left as `sorry` — needs a multi-element generalisation of `check_singleton_iff`. +- ◯ **L8 Hiding OPEN — goal-shaped obligation + honest floor landed.** Hiding is the goal-shaped `HasROMHiding` obligation: fixed real/ideal games and a fixed error `n·q/|Salt| + (n−1)·q/|Digest|²`, no configurable advantage field. The proved floor is the structural `mt_root_hiding` / `mt_root_hiding_commit` backbone, operational per-leaf salts, `HidingParams`, salt-space bounds and field/byte salt-entropy capstones, `PMF.etvDist`, and `PerfectHiding` with its `not_perfectHiding_singleton` negative result. **No `HasROMHiding` instance is installed yet**: the honest real game is the oracle-native commitment distribution (sampling the oracle lazily), and its construction plus the basic-commitment → root-hiding → selective-opening privacy reduction are the remaining work. The staged plan: (1) port the `PMF` total-variation / lazy-cache query-handler / identical-until-bad foundation; (2) basic-commitment hiding `q/|Salt|`; (3) oracle-native Merkle commitment + bottom-up root hiding; (4) selective-opening privacy simulator + `Q·n·q` loose bound; (5) install the `HasROMHiding` instance. +- 🟨 **Extractability reduced to one ROM bridge** — deterministic `mt_extractability` and `mt_multi_extractability` are proved. The shared-oracle instance is implemented and reduced to `extraction_win_le_trace_collision`, whose remaining work is the documented `cacheExtract_sound` bridge. +- ⏳ **Equivocation** (book §12.7) — deferred; it requires programmable-RO simulator machinery. +- ✅ **ROM collision and binding spine** — the lazy-sampling `OracleComp` model, direct-induction `run_coll_le`, `coupling_trace_le_collisionBound`, Merkle trace-collision reductions, `checkOracle` acceptance lemmas, and ROM position-binding instance are proved. - ✅ **PathCopath.lean** — three real proven lemmas: `copath_length_eq_depth`, `path_length_eq_depth_succ` (corrected from off-by-one), `deriveVertexSet_subset_internal`. Useful structural facts about the heap-indexed perfect binary tree. -- 🟨 **L6 (partial)** — `MerkleCommitment.deriveVertexSet` has a real filter-based body in [`Src/Merkle/Scheme.lean`](Src/Merkle/Scheme.lean); `path_pruning_is_copaths_minus_paths` proven (rfl) in [`Lemmas/PathPruning.lean`](Properties/Lemmas/PathPruning.lean). Two golden-value tests in [`SchemeTests.lean`](Tests/SchemeTests.lean). Remaining: `opening_proof_size_bound` lemma and wiring `deriveVertexSet` into `open`/`check` for actual size savings. -- ✅ **L4** — [`Properties/Probability/RandomOracle.lean`](Properties/Probability/RandomOracle.lean) has real bodies for `ROFunction`, `RODistribution` (currently the `PMF.pure` placeholder at the all-zeros oracle), `ROQueryTrace.empty`, `ROQueryTrace.append`, plus three sorry-free smoke lemmas (`RODistribution_tsum_eq_one`, `ROQueryTrace.empty_queries`, `ROQueryTrace.append_queries`). The placeholder distribution will be replaced with real lazy-sampling at L5/L8. +- ✅ **Parameters** — `MerkleHasherParams.ofField` computes digest and salt widths; the binding target and field/byte salt-entropy targets are proved, with BabyBear binding and hiding capstones. +- ✅ **L4** — [`Properties/Probability/RandomOracle.lean`](Properties/Probability/RandomOracle.lean) retains the legacy `RODistribution := PMF.pure` only for downstream compatibility. Real probabilistic arguments use the lazy-sampling `OracleComp` / `QueryLog` model. Its structural API mirrors [VCVio](https://github.com/Verified-zkEVM/VCV-io); z-Lean intentionally keeps its own direct-induction coupling proof rather than VCVio's eager-seed/padding route. - 🟨 **L9 (partial)** — `PerfectKAry k` and `ArbitraryLength` shapes have real `MerkleShape` instance bodies in [`Src/Merkle/Shape.lean`](Src/Merkle/Shape.lean), mirroring the Rust `crates/ark-mt/src/shape.rs` algorithms (heap-indexed for `PerfectKAry`; precomputed parent/children vectors via ceil/floor split for `ArbitraryLength`). [`Tests/ShapeTests.lean`](Tests/ShapeTests.lean) pins golden values for `PerfectKAry 4` (16 leaves) and `ArbitraryLength.mk 7`. Remaining for full L9: wire the new shapes into `MerkleCommitment.commit`/`open`/`check` (currently specialised to `PerfectBinary`-style heap arithmetic in `buildLabels`). - ✅ **Instance.lean wired** — `instance : VectorCommitment (MerkleCommitment H S)` is now real (no `sorry`) in [`Src/Merkle/Instance.lean`](Src/Merkle/Instance.lean). `UniversalParams := MerkleCommitment H S`, `CommitterKey = VerifierKey = MerkleCommitment H S`. The trait-level `setup`/`trim`/`commit`/`open`/`check` delegate to the concrete Merkle bodies. - ✅ **L10 partial: Capped commitments** — [`Src/Merkle/Capped.lean`](Src/Merkle/Capped.lean) ships real `commit`/`open`/`check` for `CappedMerkleCommitment`. Cap of height `c` produces a `List Digest` of length `|verticesAtLayer c|`, opening proofs are truncated by `c` levels, and `check` walks the truncated copath then matches the layer-`c` ancestor against the supplied cap entry. Four `native_decide` round-trip tests: `roundtrip4_h0`, `roundtrip4_h1`, `roundtrip4_h2` (cap heights 0, 1, 2 over 4 leaves), and `roundtrip8_h2` (8 leaves, cap height 2). @@ -57,11 +64,11 @@ This is the Lean equivalent of [`ark-mt/DESIGN.md` §4](https://github.com/arkwo | **L1** | Concrete bodies for `commit` / `open` / `check` on the non-hiding `PerfectBinary` shape with the demo hasher. `OpeningProof` becomes a real structure, not `sorry`. `instance : VectorCommitment (MerkleCommitment H PerfectBinary)` glue lands in `Merkle/Instance.lean`. Test vectors from the Rust crate's `tests/scheme.rs` get pinned as `lemma … := by native_decide`. | `SchemeTests.lean` round-trip on 4, 8, 16 leaves. Outputs match a Rust-side test vector (to be supplied alongside this milestone). `TraitTests.lean` confirms the `VectorCommitment` instance resolves. | | **L2** | Prove `lemma:mt-completeness` (book §12.2). Combinatorial — no probability needed; structural induction on tree depth + `path`/`copath` algebra. | `Theorems/Completeness.lean` is `sorry`-free. `#print axioms mt_completeness` lists no `sorryAx`. | | **L3** | Prove `lemma:simple-mt-colliding-paths` and `lemma:mt-colliding-paths` (book §12.3). Combinatorial; sets up the binding proof. Builds on `Lemmas/PathCopath.lean` (also closed at this milestone). | `Lemmas/CollisionLemma.lean` and `Lemmas/PathCopath.lean` are `sorry`-free. | -| **L4** | Stand up `Properties/Probability/RandomOracle.lean`. Define `ROFunction κ`, the noncomputable `RODistribution κ : PMF (ROFunction κ)`, and `ROQueryTrace κ`. Prove one smoke lemma about `RODistribution` (e.g. it's well-defined on the empty trace, or its measure on any singleton query is `2^(-κ)`). Decide once and for all whether `Properties/` standardizes on `PMF` or on `Fintype`-counting `ℚ` (DESIGN.md §3.5 leaves this open). | `RandomOracle.lean` compiles, `noncomputable def RODistribution` has a real body, and the smoke lemma is `sorry`-free. | -| **L5** | Prove `lemma:mt-binding` (§12.4) on top of L3 + L4. Reduction from a binding break to a colliding-path event under `RODistribution`. May also discharge `lemma:mt-other-binding` if it falls out trivially. | `Theorems/Binding.lean` is `sorry`-free for the main statement. | +| **L4** | Stand up the lazy-sampling `OracleComp` / `QueryLog` random-oracle model, with a VCVio-compatible structural API and PMF interpreter. Keep the function-view `RODistribution` only as a legacy compatibility layer. | `RandomOracle.lean` compiles; `run_bind` and the direct-induction `coupling_trace_le_collisionBound` are proved. | +| **L5** | Prove `lemma:mt-binding` (§12.4), lift it to the shared lazy-oracle game, and derive concrete parameter bounds. | `Theorems/Binding.lean`, `Instances/BindingROM.lean`, and the binding capstones in `Instances/Parameters.lean` are proved. | | **L6** | Path pruning. Implement `deriveVertexSet` in `Scheme.lean` with a real body and prove `lemma:path-pruning-is-copaths-minus-paths` plus the size bound from book Eq. 20.x. Adapt `open` / `check` to use the pruned vertex set; existing L1 test vectors must still pass. | `Lemmas/PathPruning.lean` is `sorry`-free. `SchemeTests.lean` opening-proof size measurably shrinks for 2+ indices and matches the book's bound. | | **L7** | Hiding salt path. Instantiate `Salt := Vector (Fin 256) 16` (or similar) on a hiding variant of the demo hasher and provide `instance : HidingVectorCommitment (MerkleCommitment H S)` for `H.Salt ≠ Unit`. The compile-time rejection promised in [HIDING.md](HIDING.md) starts biting: callsites with hiding bounds reject the non-hiding hasher. | New `SchemeTests` cases for the hiding hasher round-trip. A negative test confirms `[HidingVectorCommitment …]` fails to resolve for `H.Salt = Unit`. | -| **L8** | Prove `lemma:mt-root-hiding` and `lemma:mt-privacy` (§12.6). Probability arguments over `RODistribution`; reuses the L4 infrastructure. | `Theorems/Hiding.lean` is `sorry`-free. | +| **L8** | Declare the goal-shaped `HasROMHiding` obligation, prove structural root hiding, operational salt support, salt-entropy parameters, and the honest floor; then close ROM hiding/privacy over the lazy-sampling model. | Structural hiding, the `HasROMHiding` declaration, parameter capstones, and the floor (`PMF.etvDist`, `PerfectHiding` + `not_perfectHiding_singleton`) are proved. The oracle-native commitment game and the root-hiding/privacy bounds are the remaining work; no `HasROMHiding` instance is installed yet. | | **L9** | `PerfectKAry k` and `ArbitraryLength` shapes wired through the scheme. Same `commit`/`open`/`check` code path; only `MerkleShape` instance changes. The `if h : k = 2` binary fast-path stays available. | `ShapeTests.lean` becomes parametric over shape. Round-trips at `k = 2, 3, 4` and at `numLeaves ∈ {7, 13, 17}` for `ArbitraryLength`. | | **L10** | Optional capabilities: `CappedMerkleCommitment` plus `LocallyUpdatable`, `LeavesAccessible`, `Equivocable` instances. The `Equivocable` *instance* lands; the `lemma:mt-equivocation` *theorem* statement stays in place but its proof remains `sorry` (deep §12.7 argument, deferred indefinitely). | One round-trip test per capability under `Tests/`. `#print axioms` on the equivocation theorem still reports `sorryAx` — flagged in `Theorems/Equivocation.lean` as known and intentional. | @@ -83,7 +90,7 @@ L0 is done iff all of the following hold: ## 3. Critical-path decision points - **L1 success determines whether the typeclass shape is right.** If wiring up the demo hasher to `commit`/`open`/`check` against the L0 typeclass surface requires bizarre workarounds (e.g. extra associated types, `noncomputable` leaks into `Src/`, `DecidableEq` instances that won't synthesize), revise [DESIGN.md §3.1–§3.3](DESIGN.md#31-merklehasher-is-one-typeclass-with-an-associated-salt-type) **before** continuing to L2. Sunk-cost on `sorry`'d theorems against a wrong surface is cheap to abandon; sunk-cost after L2 is not. -- **L4 success determines whether the RO infrastructure shape is right.** [DESIGN.md §3.5](DESIGN.md#35-random-oracle-infrastructure-in-propertiesprobabilityrandomoraclelean) defers the `PMF` vs `Fintype`-counting `ℚ` choice. L4 has to commit. If the chosen path makes the L5 binding statement awkward to even *write*, back out and re-pick before attempting the proof. +- **L4 selected the lazy-sampling RO shape.** [DESIGN.md §3.5](DESIGN.md#35-random-oracle-infrastructure-in-propertiesprobabilityrandomoraclelean) records the VCVio-compatible free-monad structure and z-Lean's direct-induction coupling proof. The legacy function-view `RODistribution` is not the model used by the ROM security reductions. - **L6 path pruning may force `Scheme.lean` refactors.** The L1 implementation is allowed to be naive (one full path per index). If pruning at L6 requires changing the `OpeningProof` representation, the L1 test vectors get re-pinned — flag this in the L6 PR rather than silently rewriting them. --- diff --git a/VectorCommitment/Src/Security/Hiding.lean b/VectorCommitment/Src/Security/Hiding.lean index a42a8f2..511d339 100644 --- a/VectorCommitment/Src/Security/Hiding.lean +++ b/VectorCommitment/Src/Security/Hiding.lean @@ -3,47 +3,120 @@ Copyright (c) 2026 LeanStuff contributors. All rights reserved. -/ import VectorCommitment.Src.Trait import Mathlib.Data.ENNReal.Basic +import Mathlib.Probability.ProbabilityMassFunction.Constructions /-! -# Hiding — abstract security obligation - -This file declares `HasHiding`. The property: a commitment, together with -openings at a chosen index set, reveals nothing about the values at -*unopened* positions beyond what those openings disclose. - -The standard distinguishing game: - 1. Adversary picks two messages `m₀, m₁` of the same length and an - index set `I` it wants opened. - 2. Challenger samples `b ←$ {0,1}`, commits to `m_b`, opens at `I`. - 3. Adversary, given the commitment + openings, outputs a guess `b'`. - 4. Advantage = `|Pr[b' = b] − 1/2|`. - -The bound is "bounded-query hiding": hiding holds as long as the -adversary sees at most some `Q` openings (which becomes the IOPP's query -complexity in the compiled protocol). The bound captures both `Q` (the -number of openings) and `q` (the underlying oracle/computational budget). - -Model-specific instances live under: - * `VectorCommitment/Properties/Probability/Instances/HidingROM.lean` - * `VectorCommitment/Properties/StandardModel/Instances/…` (reserved) +# Hiding — the ROM security obligation and its honest floor + +This file declares the goal-shaped `HasROMHiding`: a finite-query random-oracle +hiding obligation stated against **fixed** real/ideal games and a **fixed** error +expression. An instance supplies only the games, the error, and the bound +*proof* — it cannot redefine what hiding means. (It replaces the former generic +`HasHiding`, whose ROM instance measured a *collision* advantage that does not +capture hiding.) + +The deep `etvDist real ideal ≤ error` reduction (the book's simulator-based +proof: basic-commitment hiding → bottom-up Merkle root-hiding hybrid → +selective-opening privacy) is a multi-stage formalization. Until the +oracle-native commitment game lands, **no** `HasROMHiding` instance is installed +for the Merkle scheme — hiding is reported OPEN rather than discharged by a +fixed-oracle (false) or `real = ideal` (vacuous) instance. See +`VectorCommitment/ROADMAP.md`. + +The honest floor this file proves: + +* `PMF.etvDist` total-variation distance and `etvDist_self`; +* `PerfectHiding`, the distributional (perfect) hiding predicate, and a + `not_perfectHiding_singleton` negative result demonstrating the predicate is + non-vacuous (a scheme injective under a fixed salt is *not* hiding). + +The salt-size arithmetic certificates (`2 ^ s ≤ |Salt|`) live in +`VectorCommitment/Properties/Probability/Instances/HidingParams.lean` and the +`*_salt_card_ge_lam` capstones. -/ -/-- Hiding obligation. -/ -class HasHiding (V : Type) [VectorCommitment V] where - /-- The hiding-game adversary. The model's instance defines the - precise game shape (number of openings revealed, computational - model, etc.). -/ - HidingAdversary : (κ q : ℕ) → Type - /-- The adversary's distinguishing advantage in the hiding game. -/ - hidingAdvantage : ∀ {κ q}, HidingAdversary κ q → ENNReal - /-- The model-specific upper bound. - ROM Merkle with salt size `s`, message length `ℓ`, `Q` openings: - `ε_hide ≤ q · ℓ / 2 ^ s + Q² / 2 ^ s` - (oracle hits a salted-leaf input + revealed-salt collisions). - Standard-model under one-way `H`: `Adv_H^OW(B)` for some reduction - `B`. -/ - hidingError : (κ q : ℕ) → ENNReal - /-- The central guarantee. -/ - hiding_bound : - ∀ {κ q} (A : HidingAdversary κ q), - hidingAdvantage A ≤ hidingError κ q +namespace PMF + +variable {α : Type*} + +/-- Total-variation distance between two `PMF`s, in the one-sided event-sup form + `⨆ E, μ(E) − ν(E)` (truncated `ENNReal` subtraction). For `PMF`s this equals + the usual `½ ∑ₐ |μ a − ν a|`; the event form is the shape the ROM + indistinguishability bounds are stated in. -/ +noncomputable def etvDist (μ ν : PMF α) : ENNReal := + ⨆ E : Set α, μ.toOuterMeasure E - ν.toOuterMeasure E + +/-- A distribution has zero total-variation distance from itself. -/ +@[simp] theorem etvDist_self (μ : PMF α) : μ.etvDist μ = 0 := by + simp only [etvDist, tsub_self, iSup_const] + +end PMF + +/-! ## Distributional (perfect) hiding — the non-vacuity floor -/ + +/-- **Perfect (distributional) hiding.** Under a salt distribution `saltDist`, + the commitment to any two values is identically distributed. + + This is *not* computational hiding — there is no adversary, no security + parameter, no negligible advantage; it compares the raw mapped + distributions. It is the information-theoretic floor that the ROM + `HasROMHiding` obligation strengthens to a finite-query, bounded-advantage + statement. -/ +def PerfectHiding {Value Salt Com : Type} (saltDist : PMF Salt) + (commit : Value → Salt → Com) : Prop := + ∀ v₀ v₁ : Value, saltDist.map (commit v₀) = saltDist.map (commit v₁) + +/-- **Singleton-salt negative result.** With a single (deterministic) salt `s₀`, + a scheme whose commitment separates two values under `s₀` does *not* satisfy + `PerfectHiding`. This witnesses that `PerfectHiding` is non-vacuous: it is a + real constraint that injective-under-a-fixed-salt schemes fail. -/ +theorem not_perfectHiding_singleton {Value Salt Com : Type} + (s₀ : Salt) (commit : Value → Salt → Com) (v₀ v₁ : Value) + (hsep : commit v₀ s₀ ≠ commit v₁ s₀) : + ¬ PerfectHiding (PMF.pure s₀) commit := by + intro h + have hmap := h v₀ v₁ + rw [PMF.map_pure, PMF.map_pure] at hmap + have hsupp := congrArg PMF.support hmap + rw [PMF.support_pure, PMF.support_pure] at hsupp + -- hsupp : {commit v₀ s₀} = {commit v₁ s₀} + have hmem : commit v₀ s₀ ∈ ({commit v₁ s₀} : Set Com) := by + rw [← hsupp]; exact Set.mem_singleton _ + exact hsep (Set.mem_singleton_iff.mp hmem) + +/-- Concrete instance of the singleton-salt counterexample: the identity + commitment `commit v _ = v` over `Bool` separates `false` and `true`, so it + is not perfectly hiding under any single salt. -/ +theorem not_perfectHiding_identity_bool (s₀ : Unit) : + ¬ PerfectHiding (PMF.pure s₀) (fun (v : Bool) (_ : Unit) => v) := by + refine not_perfectHiding_singleton s₀ _ false true ?_ + decide + +/-! ## The ROM hiding obligation -/ + +/-- **Finite-query ROM hiding obligation.** Stated against fixed real and ideal + games (`PMF`s over a hidden digest type) and a fixed error expression; an + instance supplies the games, the error, and the bound proof but cannot + redefine the notion. The single security guarantee is that the real and + ideal games are `error`-close in total-variation distance. + + No instance is installed for the Merkle scheme yet: the honest real game is + the oracle-native commitment distribution, whose construction and bound are + the remaining work (see `ROADMAP.md`). Installing a fixed-oracle or + real = ideal placeholder would be false or vacuous, so hiding is reported + OPEN until the real proof lands. -/ +class HasROMHiding (V : Type) [VectorCommitment V] where + /-- The hidden target type the games range over (e.g. the commitment root + digest). -/ + Hidden : Type + /-- The real root-hiding game: the honest commitment-root distribution. -/ + rootRealGame : PMF Hidden + /-- The ideal game: a uniform hidden digest. -/ + rootIdealGame : PMF Hidden + /-- The fixed root-hiding error, `n·q / |Salt| + (n−1)·q / |Digest|²`. -/ + rootError : ENNReal + /-- The fixed selective-opening privacy error, + `Q·n·q / |Salt| + Q·n·q / |Digest|²` (loose public bound). -/ + privacyError : ENNReal + /-- The central guarantee: real and ideal root games are `rootError`-close. -/ + root_hiding : rootRealGame.etvDist rootIdealGame ≤ rootError diff --git a/VectorCommitment/USAGE.md b/VectorCommitment/USAGE.md index 9c72611..923f3d5 100644 --- a/VectorCommitment/USAGE.md +++ b/VectorCommitment/USAGE.md @@ -1,6 +1,8 @@ # `VectorCommitment` — Usage -This doc shows the minimal end-to-end flow for using `VectorCommitment` to commit, open, and check. After L1, the example below works for real; at L0, only the typecheck and the size-0 smoke test pass. +This doc shows the minimal end-to-end flow for using `VectorCommitment` to +commit, open, and check. The operations below are executable definitions and +the round-trip is checked by `native_decide`. --- @@ -21,7 +23,6 @@ instance : MerkleHasher MyHasher where Salt := Unit decEqDigest := inferInstance defaultSalt := ⟨()⟩ - sampleSalt := fun _ _ => () hashLeaf := fun _ x _ => x * 31 + 17 hashNodes := fun _ cs => (cs.map id).foldl (fun acc d => acc * 31 + d) 1 ``` @@ -86,11 +87,25 @@ If both match exactly, the Rust implementation agrees with the Lean spec on this --- -## 6. What doesn't work yet at L0 - -- `commit` / `open` / `check` bodies are `sorry`; the round-trip lemma above only typechecks. -- The real demo arrives at L1. See [ROADMAP.md](ROADMAP.md). -- `HidingVectorCommitment` is a separate typeclass — see [HIDING.md](HIDING.md) to understand why this hasher (`Salt = Unit`) doesn't satisfy it. +## 6. Current limitations and security proofs + +- `commit` / `open` / `check` are real and are exercised by the tests; the demo + hasher remains intentionally non-cryptographic. +- `HidingVectorCommitment` is a separate typeclass — its hiding commit takes + explicit typed `Randomness ck` (e.g. a per-leaf salt vector), and `Salt = Unit` + carries no entropy. See [HIDING.md](HIDING.md). +- ROM position binding is proved over the lazy-sampling oracle, and ROM + extractability is reduced to the named `cacheExtract_sound` bridge. Hiding is + the goal-shaped `HasROMHiding` obligation (fixed real/ideal games, fixed error + `n·q/|Salt| + (n−1)·q/|Digest|²`); it is currently **OPEN** — no instance is + installed yet, pending the oracle-native commitment game. The honest floor + (`PerfectHiding` + `not_perfectHiding_singleton`, `PMF.etvDist`, and the + `2^s ≤ |Salt|` salt-entropy capstones) is proved. See [ROADMAP.md](ROADMAP.md) + and [INTERFACE.md](INTERFACE.md). +- The lazy-sampling `OracleComp` API mirrors + [VCVio](https://github.com/Verified-zkEVM/VCV-io), permitting a future + mechanical dependency swap. z-Lean's direct-induction collision proof remains + local because it avoids VCVio's eager-seed padding artifact. ---