Context
Branch ajhavlin/interface-refactor-and-binding-hiding-closures addresses three interconnected needs: a navigable human-readable entry point into the security layer, full closure of the ROM position binding chain, and a correction to make the hiding argument match the book's actual construction rather than a structurally incorrect collision proxy.
Motivation
Human-readable interface
The VectorCommitment security layer had grown across many commits into a collection of files with no single entry point for developers. VectorCommitment.Interface and VectorCommitment/INTERFACE.md provide that entry point: a single import facade listing all four security notions (HasPositionBinding, HasStraightlineExtractor, HasROMHiding, HasEquivocation), their current status, and where the machine-checked cores live.
ROM binding closure
The position binding chain is now fully proved without sorry:
- A successful binding adversary must produce two different messages that open to the same commitment under the same verifier key.
- Running the adversary and verifier against the same lazy-sampled random oracle means the adversary's winning output forces a collision in the oracle query trace.
- The proved adaptive birthday bound (
coupling_trace_le_collisionBound) bounds that collision probability.
- The parameter layer (
MerkleHasherParams.ofField, babyBear_binding_secure) converts this into concrete guarantees: BabyBear/KoalaBear/M31 are binding at the specified security level.
Honest hiding argument
The former HasHiding instance and its ROM discharge were structurally incorrect. The instance defined hidingAdvantage as the probability of a trace collision — the chance that two oracle queries collide in the same output bucket — which is a binding/collision notion, not a hiding notion. A hiding advantage measures an adversary's ability to distinguish a commitment to one message from a commitment to another. These are different security properties.
The replacement is HasROMHiding: a goal-shaped class whose real game is the oracle-native commitment distribution (sampling fresh per-leaf salts and sampling the lazy oracle jointly), whose ideal game is a uniform digest, and whose fixed error expression is n·q/|Salt| + (n−1)·q/|Digest|². An instance provides the real and ideal distributions, the error bound, and a proof that they are within that distance of each other. No instance is installed yet because constructing the oracle-native game requires lazy oracle infrastructure over the commitment distribution; that is the remaining mechanisation work.
Why the open Lean hiding proofs are acceptable
The root-hiding bound and the multi-opening privacy bound are both proved in the textbook via the standard ROM/salt hybrid argument:
- Each leaf salt is drawn uniformly and independently. The probability that any of the adversary's
q oracle queries hits a specific leaf's (value, salt) input is at most q/|Salt| per leaf, giving total error n·q/|Salt| across n leaves.
- The internal-node labels are standard RO outputs over child digests. The probability of a pre-image collision across the
n−1 internal nodes is bounded by (n−1)·q/|Digest|² via the birthday argument.
- The selective-opening privacy statement layers a simulator over this that can reproduce the correct (commitment, opening) view using only the opened leaf values and simulated salts for the remaining copath nodes.
These are standard results; the mathematical content is settled. The open Lean work is mechanising a known proof, not filling a mathematical gap. What is missing is the oracle-native commitment game — a PMF over (oracle, salt-vector) pairs that runs the lazy-sampling monad over the full commitment — and the bottom-up hybrid connecting the real game to the stated error. That is an engineering task, not a mathematical unknown. The five-step remaining plan is recorded in ROADMAP.md.
Current proof status
| Area |
Status |
| Position binding |
✅ Fully proved. HasPositionBinding instance with no sorry. Binding break → trace collision → birthday bound → BabyBear capstone. |
| Hiding (API + floor) |
✅ HidingVectorCommitment takes typed Randomness ck. PMF.etvDist, PerfectHiding, not_perfectHiding_singleton floor, and 2^s ≤ |Salt| salt-entropy capstones all proved. |
| Developer interface |
✅ VectorCommitment.Interface, INTERFACE.md, DESIGN.md, ROADMAP.md, USAGE.md reflect current state. |
| Extractability |
◐ Reduced to one bridge lemma. HasStraightlineExtractor structure proved; extraction_win_le_trace_collision has one sorry pending cacheExtract_sound. |
| Hiding (reduction) |
◯ OPEN. HasROMHiding declared; no instance installed. Oracle-native game and root-hiding/privacy bounds are the remaining work. Proved in the book. |
| Equivocation |
✗ Out of scope of this PR, but needing work (requires programmable random oracle). |
Active sorry inventory
Five sorry terms remain across four declarations (down from seven — see removal note below):
| Declaration |
File |
Status |
hidden_query_hit_le |
HiddenQuery.lean |
Book lemma:rom-ow-high-entropy; mechanisation gap |
extraction_win_le_trace_collision |
ExtractabilityROM.lean |
Reduced to cacheExtract_sound bridge |
equivocationAdvantage, equivocation_bound |
EquivocationROM.lean |
Out of scope of this PR, needing work (programmable RO) |
mt_equivocation |
Theorems/Equivocation.lean |
Out of scope of this PR, needing work (True := sorry placeholder) |
Two previously listed sorry terms were removed because the underlying statements were false or vacuous: mt_root_hiding_rom_bound stated the bound against a fixed oracle rather than the oracle-sampling distribution, which is false; mt_privacy_rom_loose was labelled as a multi-opening privacy theorem but actually only bounded the root distribution. Their structural backbone (mt_root_hiding, labelAt_eq_of_leaf_hash_eq) remains fully proved and is the propagation step the future reduction will reuse.
Follow-up checklist
Context
Branch
ajhavlin/interface-refactor-and-binding-hiding-closuresaddresses three interconnected needs: a navigable human-readable entry point into the security layer, full closure of the ROM position binding chain, and a correction to make the hiding argument match the book's actual construction rather than a structurally incorrect collision proxy.Motivation
Human-readable interface
The VectorCommitment security layer had grown across many commits into a collection of files with no single entry point for developers.
VectorCommitment.InterfaceandVectorCommitment/INTERFACE.mdprovide that entry point: a single import facade listing all four security notions (HasPositionBinding,HasStraightlineExtractor,HasROMHiding,HasEquivocation), their current status, and where the machine-checked cores live.ROM binding closure
The position binding chain is now fully proved without
sorry:coupling_trace_le_collisionBound) bounds that collision probability.MerkleHasherParams.ofField,babyBear_binding_secure) converts this into concrete guarantees: BabyBear/KoalaBear/M31 are binding at the specified security level.Honest hiding argument
The former
HasHidinginstance and its ROM discharge were structurally incorrect. The instance definedhidingAdvantageas the probability of a trace collision — the chance that two oracle queries collide in the same output bucket — which is a binding/collision notion, not a hiding notion. A hiding advantage measures an adversary's ability to distinguish a commitment to one message from a commitment to another. These are different security properties.The replacement is
HasROMHiding: a goal-shaped class whose real game is the oracle-native commitment distribution (sampling fresh per-leaf salts and sampling the lazy oracle jointly), whose ideal game is a uniform digest, and whose fixed error expression isn·q/|Salt| + (n−1)·q/|Digest|². An instance provides the real and ideal distributions, the error bound, and a proof that they are within that distance of each other. No instance is installed yet because constructing the oracle-native game requires lazy oracle infrastructure over the commitment distribution; that is the remaining mechanisation work.Why the open Lean hiding proofs are acceptable
The root-hiding bound and the multi-opening privacy bound are both proved in the textbook via the standard ROM/salt hybrid argument:
qoracle queries hits a specific leaf's(value, salt)input is at mostq/|Salt|per leaf, giving total errorn·q/|Salt|acrossnleaves.n−1internal nodes is bounded by(n−1)·q/|Digest|²via the birthday argument.These are standard results; the mathematical content is settled. The open Lean work is mechanising a known proof, not filling a mathematical gap. What is missing is the oracle-native commitment game — a PMF over
(oracle, salt-vector)pairs that runs the lazy-sampling monad over the full commitment — and the bottom-up hybrid connecting the real game to the stated error. That is an engineering task, not a mathematical unknown. The five-step remaining plan is recorded inROADMAP.md.Current proof status
HasPositionBindinginstance with nosorry. Binding break → trace collision → birthday bound → BabyBear capstone.HidingVectorCommitmenttakes typedRandomness ck.PMF.etvDist,PerfectHiding,not_perfectHiding_singletonfloor, and2^s ≤ |Salt|salt-entropy capstones all proved.VectorCommitment.Interface,INTERFACE.md,DESIGN.md,ROADMAP.md,USAGE.mdreflect current state.HasStraightlineExtractorstructure proved;extraction_win_le_trace_collisionhas onesorrypendingcacheExtract_sound.HasROMHidingdeclared; no instance installed. Oracle-native game and root-hiding/privacy bounds are the remaining work. Proved in the book.Active
sorryinventoryFive
sorryterms remain across four declarations (down from seven — see removal note below):hidden_query_hit_leHiddenQuery.leanlemma:rom-ow-high-entropy; mechanisation gapextraction_win_le_trace_collisionExtractabilityROM.leancacheExtract_soundbridgeequivocationAdvantage,equivocation_boundEquivocationROM.leanmt_equivocationTheorems/Equivocation.leanTrue := sorryplaceholder)Two previously listed
sorryterms were removed because the underlying statements were false or vacuous:mt_root_hiding_rom_boundstated the bound against a fixed oracle rather than the oracle-sampling distribution, which is false;mt_privacy_rom_loosewas labelled as a multi-opening privacy theorem but actually only bounded the root distribution. Their structural backbone (mt_root_hiding,labelAt_eq_of_leaf_hash_eq) remains fully proved and is the propagation step the future reduction will reuse.Follow-up checklist
VectorCommitment.Interface,INTERFACE.md).sorry.HasHidingwith goal-shapedHasROMHidingobligation.PerfectHiding,not_perfectHiding_singleton,PMF.etvDist.babyBear_byte_salt_hiding,babyBear_field_salt_hiding).mt_root_hiding_rom_bound,mt_privacy_rom_loose).DESIGN.md,INTERFACE.md,ROADMAP.md,USAGE.md,CHANGELOG.md.hidden_query_hit_le(booklemma:rom-ow-high-entropy).cacheExtract_soundand closeextraction_win_le_trace_collision.HasROMHidinginstance.lake build VectorCommitment VectorCommitment.Interface.