Follow-up from #473 (Bolton's suggestion), also touching the point Quang raised there: the Merkle uniqueness results in
VCVio/CryptoFoundations/MerkleTree/Inductive/Uniqueness.lean (single opening), andVCVio/CryptoFoundations/MerkleTree/Inductive/Batch/Uniqueness.lean (batch openings)
are currently stated under global Function.Injective2 h. That is fine as a structural sanity check, but it is not a realistic assumption for a compressing hash, and it doesn't connect to the query-transcript world where the cryptographic argument actually lives.
Proposed refinement (Bolton's "Option Injective2"): treat the hash as partial on the queried domain — e.g. a query log L : Finset (α × α) (or an (α × α) →? α partial function / Option-valued map that is none off the log) — and restate uniqueness as:
if two openings (resp. batch openings) verify against the same root and every hash evaluation they induce lies in the queried domain, then either the openings agree, or there is a collision among the queried pairs.
Concretely:
- Define injectivity-on-a-log:
∀ p q ∈ L, h p = h q → p = q (no global assumption).
- Prove the single-opening uniqueness theorem in this form; the existing constructive collision kernel (
findCollision*) already produces the disagreeing pair, so the content is locating that pair inside the induced query set.
- Do the same for the batch version (the pruned
BatchProof induces a query set that is the union over selected leaves).
- Keep (or demote to
deprecated-style doc note) the current global-Injective2 statements as corollaries at L = univ, so nothing downstream breaks.
This gives the uniqueness lemmas the shape a game-level extractability/query-bound argument can consume directly (the collision lands in the adversary's transcript), matching the direction discussed for the addressed-tree work in #474.
Not urgent; both statements are internally consistent today. Filed so the two files get upgraded together in one later PR.
Follow-up from #473 (Bolton's suggestion), also touching the point Quang raised there: the Merkle uniqueness results in
VCVio/CryptoFoundations/MerkleTree/Inductive/Uniqueness.lean(single opening), andVCVio/CryptoFoundations/MerkleTree/Inductive/Batch/Uniqueness.lean(batch openings)are currently stated under global
Function.Injective2 h. That is fine as a structural sanity check, but it is not a realistic assumption for a compressing hash, and it doesn't connect to the query-transcript world where the cryptographic argument actually lives.Proposed refinement (Bolton's "Option Injective2"): treat the hash as partial on the queried domain — e.g. a query log
L : Finset (α × α)(or an(α × α) →? αpartial function /Option-valued map that isnoneoff the log) — and restate uniqueness as:Concretely:
∀ p q ∈ L, h p = h q → p = q(no global assumption).findCollision*) already produces the disagreeing pair, so the content is locating that pair inside the induced query set.BatchProofinduces a query set that is the union over selected leaves).deprecated-style doc note) the current global-Injective2statements as corollaries atL = univ, so nothing downstream breaks.This gives the uniqueness lemmas the shape a game-level extractability/query-bound argument can consume directly (the collision lands in the adversary's transcript), matching the direction discussed for the addressed-tree work in #474.
Not urgent; both statements are internally consistent today. Filed so the two files get upgraded together in one later PR.