Skip to content

Commit e7adf72

Browse files
author
Claude
committed
refactor(merkle): generalize root/verify/soundness over the hash combiner
Parameterize the Merkle construction, verification, and inclusion-proof soundness proof over an arbitrary pure combiner `Combiner = HashBytes -> HashBytes -> HashBytes`: * rootHashWith, verifyProofWith, generateProofWith, reconstructWith, reconstructAppendWith, verifyProofReconstructsWith * merkleCorrectWith : the soundness theorem, which uses NO property of the combiner (combination is an opaque black box) and so holds for every hash function. The existing pure XOR API (rootHashBytes, verifyProof, generateProof, reconstruct, verifyProofReconstructs, merkleCorrect) is recovered as the `hashPairStub` instance of the generic family — definitional aliases, so behavior is byte-identical. XOR is no longer a special case but one point of a universally-quantified result; the BLAKE3 path's soundness is the same theorem at the BLAKE3 combiner, with only its allocation-failure plumbing remaining in the separate ...IO functions. All total, no believe_me/assert_*/postulate. Verified: full core builds from scratch (17/17); property 47/47, integration 55/55, A2ML suite green.
1 parent 7bba163 commit e7adf72

1 file changed

Lines changed: 149 additions & 72 deletions

File tree

‎ochrance-core/Ochrance/Filesystem/Merkle.idr‎

Lines changed: 149 additions & 72 deletions
Original file line numberDiff line numberDiff line change
@@ -6,6 +6,17 @@
66
||| compile time. The `merkleCorrect` theorem proves inclusion-proof soundness:
77
||| every proof produced by `generateProof` for an in-range leaf reconstructs
88
||| the tree's true root (a machine-checked propositional equality).
9+
|||
10+
||| The construction, verification, and soundness proof are *parametric in the
11+
||| hash combiner* (`Combiner = HashBytes -> HashBytes -> HashBytes`): see the
12+
||| `...With` family and the `merkleCorrectWith` theorem, whose proof uses no
13+
||| property of the combiner whatsoever (combination is an opaque black box).
14+
||| The pure XOR API (`rootHashBytes`, `verifyProof`, `generateProof`,
15+
||| `reconstruct`, `merkleCorrect`) is recovered as the `hashPairStub` instance,
16+
||| so XOR is no longer a special case but one point of a universally-quantified
17+
||| result; the cryptographic BLAKE3 path's soundness is the same theorem at the
18+
||| BLAKE3 combiner, with only its allocation-failure plumbing living in the
19+
||| separate `...IO` functions.
920

1021
module Ochrance.Filesystem.Merkle
1122

@@ -30,6 +41,14 @@ public export
3041
emptyHash : HashBytes
3142
emptyHash = replicate 32 0
3243

44+
||| A pure two-input hash combiner over 32-byte digests. The Merkle
45+
||| construction and its soundness proof are universally quantified over this
46+
||| function, so every concrete hash (the XOR placeholder `hashPairStub`, or a
47+
||| cryptographic BLAKE3/SHA-256 combiner) is one instance of the same theorem.
48+
public export
49+
Combiner : Type
50+
Combiner = HashBytes -> HashBytes -> HashBytes
51+
3352
--------------------------------------------------------------------------------
3453
-- Merkle Tree (height-indexed)
3554
--------------------------------------------------------------------------------
@@ -43,15 +62,22 @@ data MerkleTree : Nat -> Type where
4362
||| An internal node combining two subtrees of equal height
4463
Node : MerkleTree n -> MerkleTree n -> MerkleTree (S n)
4564

65+
||| Root hash under an arbitrary combiner: a leaf is its own hash; a node
66+
||| combines its children's roots with `h`.
67+
public export
68+
rootHashWith : Combiner -> MerkleTree n -> HashBytes
69+
rootHashWith h (Leaf x) = x
70+
rootHashWith h (Node l r) = h (rootHashWith h l) (rootHashWith h r)
71+
4672
||| Extract the root hash of a Merkle tree (pure placeholder version).
4773
||| For leaves, this is the leaf hash itself.
48-
||| For nodes, this combines the children's hashes using XOR placeholder.
74+
||| For nodes, this combines the children's hashes using the XOR placeholder.
4975
|||
50-
||| NOTE: This uses XOR for totality. Use rootHashBytesIO for cryptographic hashing.
76+
||| NOTE: This is `rootHashWith hashPairStub`. Use rootHashBytesIO for
77+
||| cryptographic hashing.
5178
public export
5279
rootHashBytes : MerkleTree n -> HashBytes
53-
rootHashBytes (Leaf h) = h
54-
rootHashBytes (Node l r) = hashPairStub (rootHashBytes l) (rootHashBytes r)
80+
rootHashBytes t = rootHashWith hashPairStub t
5581

5682
||| Extract the root hash using BLAKE3 (IO version).
5783
||| This is the cryptographically secure version that should be used in production.
@@ -116,17 +142,23 @@ buildMerkleTree {n = S k} hashes =
116142
in case splitAt (power 2 k) hashes' of
117143
(left, right) => Node (buildMerkleTree left) (buildMerkleTree right)
118144

145+
||| Verify a Merkle inclusion proof against a known root, under combiner `h`.
146+
||| Folds each sibling into the running hash and tests equality with the root.
147+
public export
148+
verifyProofWith : (h : Combiner) -> (root : HashBytes) -> (leaf : HashBytes)
149+
-> MerkleProof -> Bool
150+
verifyProofWith h root leaf [] = root == leaf
151+
verifyProofWith h root leaf ((GoLeft, sibling) :: rest) =
152+
verifyProofWith h root (h leaf sibling) rest
153+
verifyProofWith h root leaf ((GoRight, sibling) :: rest) =
154+
verifyProofWith h root (h sibling leaf) rest
155+
119156
||| Verify a Merkle inclusion proof against a known root (placeholder version).
120-
||| Uses XOR for totality. Use verifyProofIO for cryptographic verification.
157+
||| This is `verifyProofWith hashPairStub`. Use verifyProofIO for cryptographic
158+
||| verification.
121159
public export
122160
verifyProof : (root : HashBytes) -> (leaf : HashBytes) -> MerkleProof -> Bool
123-
verifyProof root leaf [] = root == leaf
124-
verifyProof root leaf ((GoLeft, sibling) :: rest) =
125-
let parent = hashPairStub leaf sibling
126-
in verifyProof root parent rest
127-
verifyProof root leaf ((GoRight, sibling) :: rest) =
128-
let parent = hashPairStub sibling leaf
129-
in verifyProof root parent rest
161+
verifyProof root leaf prf = verifyProofWith hashPairStub root leaf prf
130162

131163
||| Verify a Merkle inclusion proof using BLAKE3 (IO version).
132164
||| This is the cryptographically secure version for production use.
@@ -157,27 +189,36 @@ export
157189
hashLeafIO : HasIO io => List Bits8 -> io (Either OchranceError HashBytes)
158190
hashLeafIO bytes = blake3 bytes
159191

160-
||| Generate a Merkle inclusion proof from a tree (pure XOR version).
192+
||| Generate a Merkle inclusion proof from a tree under combiner `h`.
161193
||| Given a leaf index (0-based, left-to-right), extracts the path from
162-
||| leaf to root with sibling hashes at each level.
194+
||| leaf to root with sibling hashes (computed via `rootHashWith h`) at each level.
163195
|||
164196
||| Returns Nothing if the index is out of range.
165197
export
166-
generateProof : {n : Nat} -> MerkleTree n -> (leafIdx : Nat) -> Maybe MerkleProof
167-
generateProof {n = Z} (Leaf _) Z = Just []
168-
generateProof {n = Z} (Leaf _) (S _) = Nothing
169-
generateProof {n = S k} (Node l r) idx =
198+
generateProofWith : {n : Nat} -> (h : Combiner) -> MerkleTree n
199+
-> (leafIdx : Nat) -> Maybe MerkleProof
200+
generateProofWith {n = Z} h (Leaf _) Z = Just []
201+
generateProofWith {n = Z} h (Leaf _) (S _) = Nothing
202+
generateProofWith {n = S k} h (Node l r) idx =
170203
let halfSize = power 2 k in
171204
if idx < halfSize
172205
then do -- Leaf is in the left subtree
173-
subProof <- generateProof l idx
174-
let siblingHash = rootHashBytes r
206+
subProof <- generateProofWith h l idx
207+
let siblingHash = rootHashWith h r
175208
Just (subProof ++ [(GoLeft, siblingHash)])
176209
else do -- Leaf is in the right subtree
177-
subProof <- generateProof r (idx `minus` halfSize)
178-
let siblingHash = rootHashBytes l
210+
subProof <- generateProofWith h r (idx `minus` halfSize)
211+
let siblingHash = rootHashWith h l
179212
Just (subProof ++ [(GoRight, siblingHash)])
180213

214+
||| Generate a Merkle inclusion proof from a tree (pure XOR version).
215+
||| This is `generateProofWith hashPairStub`.
216+
|||
217+
||| Returns Nothing if the index is out of range.
218+
export
219+
generateProof : {n : Nat} -> MerkleTree n -> (leafIdx : Nat) -> Maybe MerkleProof
220+
generateProof t i = generateProofWith hashPairStub t i
221+
181222
||| Generate a Merkle inclusion proof using BLAKE3 for sibling hashes (IO version).
182223
||| This produces a cryptographically secure proof path.
183224
||| Returns Left on FFI/allocation failure, Right Nothing if index is out of range.
@@ -228,40 +269,101 @@ getLeafHash {n = S k} (Node l r) idx =
228269
-- Inclusion-Proof Soundness (merkleCorrect)
229270
--------------------------------------------------------------------------------
230271

231-
||| The hash an inclusion proof reconstructs: start from a leaf hash and fold in
232-
||| each sibling, left or right, exactly as `verifyProof` does. This is the value
233-
||| `verifyProof` compares against the root (see `verifyProofReconstructs`).
272+
||| The hash an inclusion proof reconstructs under combiner `h`: start from a
273+
||| leaf hash and fold in each sibling, left or right, exactly as `verifyProofWith
274+
||| h` does. This is the value `verifyProofWith h` compares against the root
275+
||| (see `verifyProofReconstructsWith`).
276+
public export
277+
reconstructWith : Combiner -> HashBytes -> MerkleProof -> HashBytes
278+
reconstructWith h acc [] = acc
279+
reconstructWith h acc ((GoLeft, sib) :: rest) = reconstructWith h (h acc sib) rest
280+
reconstructWith h acc ((GoRight, sib) :: rest) = reconstructWith h (h sib acc) rest
281+
282+
||| Reconstruct under the XOR placeholder. This is `reconstructWith hashPairStub`.
234283
public export
235284
reconstruct : HashBytes -> MerkleProof -> HashBytes
236-
reconstruct acc [] = acc
237-
reconstruct acc ((GoLeft, sib) :: rest) = reconstruct (hashPairStub acc sib) rest
238-
reconstruct acc ((GoRight, sib) :: rest) = reconstruct (hashPairStub sib acc) rest
239-
240-
||| `reconstruct` distributes over path concatenation: folding `p ++ q` equals
241-
||| folding `p`, then folding `q` from that result.
242-
reconstructAppend : (acc : HashBytes) -> (p, q : MerkleProof)
243-
-> reconstruct acc (p ++ q) = reconstruct (reconstruct acc p) q
244-
reconstructAppend acc [] q = Refl
245-
reconstructAppend acc ((GoLeft, sib) :: rest) q = reconstructAppend (hashPairStub acc sib) rest q
246-
reconstructAppend acc ((GoRight, sib) :: rest) q = reconstructAppend (hashPairStub sib acc) rest q
247-
248-
||| `verifyProof` is exactly a root-equality test on the reconstructed hash.
249-
||| This bridges the propositional soundness theorem below to the Bool API.
285+
reconstruct acc prf = reconstructWith hashPairStub acc prf
286+
287+
||| `reconstructWith h` distributes over path concatenation: folding `p ++ q`
288+
||| equals folding `p`, then folding `q` from that result.
289+
reconstructAppendWith : (h : Combiner) -> (acc : HashBytes) -> (p, q : MerkleProof)
290+
-> reconstructWith h acc (p ++ q)
291+
= reconstructWith h (reconstructWith h acc p) q
292+
reconstructAppendWith h acc [] q = Refl
293+
reconstructAppendWith h acc ((GoLeft, sib) :: rest) q =
294+
reconstructAppendWith h (h acc sib) rest q
295+
reconstructAppendWith h acc ((GoRight, sib) :: rest) q =
296+
reconstructAppendWith h (h sib acc) rest q
297+
298+
||| `verifyProofWith h` is exactly a root-equality test on the reconstructed
299+
||| hash. This bridges the propositional soundness theorem below to the Bool API.
300+
export
301+
verifyProofReconstructsWith : (h : Combiner) -> (root, leaf : HashBytes)
302+
-> (prf : MerkleProof)
303+
-> verifyProofWith h root leaf prf
304+
= (root == reconstructWith h leaf prf)
305+
verifyProofReconstructsWith h root leaf [] = Refl
306+
verifyProofReconstructsWith h root leaf ((GoLeft, sib) :: rest) =
307+
verifyProofReconstructsWith h root (h leaf sib) rest
308+
verifyProofReconstructsWith h root leaf ((GoRight, sib) :: rest) =
309+
verifyProofReconstructsWith h root (h sib leaf) rest
310+
311+
||| `verifyProof` (XOR API) is a root-equality test on `reconstruct`.
312+
||| The `hashPairStub` instance of `verifyProofReconstructsWith`.
250313
export
251314
verifyProofReconstructs : (root, leaf : HashBytes) -> (prf : MerkleProof)
252315
-> verifyProof root leaf prf = (root == reconstruct leaf prf)
253-
verifyProofReconstructs root leaf [] = Refl
254-
verifyProofReconstructs root leaf ((GoLeft, sib) :: rest) =
255-
verifyProofReconstructs root (hashPairStub leaf sib) rest
256-
verifyProofReconstructs root leaf ((GoRight, sib) :: rest) =
257-
verifyProofReconstructs root (hashPairStub sib leaf) rest
316+
verifyProofReconstructs root leaf prf =
317+
verifyProofReconstructsWith hashPairStub root leaf prf
258318

259319
-- Injectivity of `Just`, used to read prf back out of the generated proof.
260320
justInj : {0 a : Type} -> {0 x, y : a} -> Just x = Just y -> x = y
261321
justInj Refl = Refl
262322

263-
||| SOUNDNESS (merkleCorrect): every inclusion proof produced by `generateProof`
264-
||| for an in-range leaf reconstructs the tree's true root.
323+
||| SOUNDNESS, parametric in the combiner `h`: every inclusion proof produced by
324+
||| `generateProofWith h` for an in-range leaf reconstructs (under `reconstructWith
325+
||| h`) the tree's true root (`rootHashWith h`), as a propositional equality on
326+
||| the 32-byte digest.
327+
|||
328+
||| The proof uses no property of `h` at all — combination is treated as an
329+
||| opaque black box — which is precisely why it specialises to *every* hash, the
330+
||| XOR placeholder and a cryptographic BLAKE3 combiner alike.
331+
export
332+
merkleCorrectWith : (h : Combiner) -> {n : Nat} -> (t : MerkleTree n) -> (i : Nat)
333+
-> (leaf : HashBytes) -> (prf : MerkleProof)
334+
-> getLeafHash t i = Just leaf
335+
-> generateProofWith h t i = Just prf
336+
-> reconstructWith h leaf prf = rootHashWith h t
337+
merkleCorrectWith h (Leaf x) Z leaf prf gl gp =
338+
rewrite justInj (sym gl) in rewrite justInj (sym gp) in Refl
339+
merkleCorrectWith h (Leaf x) (S j) leaf prf gl gp = absurd gl
340+
merkleCorrectWith h {n = S k} (Node l r) i leaf prf gl gp with (i < power 2 k) proof pb
341+
merkleCorrectWith h {n = S k} (Node l r) i leaf prf gl gp | True with (generateProofWith h l i) proof ps
342+
merkleCorrectWith h {n = S k} (Node l r) i leaf prf gl gp | True | Just sub =
343+
let prfIs : (prf = sub ++ [(GoLeft, rootHashWith h r)])
344+
prfIs = sym (justInj gp)
345+
ih : (reconstructWith h leaf sub = rootHashWith h l)
346+
ih = merkleCorrectWith h l i leaf sub gl ps
347+
in rewrite prfIs in
348+
rewrite reconstructAppendWith h leaf sub [(GoLeft, rootHashWith h r)] in
349+
rewrite ih in Refl
350+
merkleCorrectWith h {n = S k} (Node l r) i leaf prf gl gp | True | Nothing =
351+
absurd gp
352+
merkleCorrectWith h {n = S k} (Node l r) i leaf prf gl gp | False with (generateProofWith h r (i `minus` power 2 k)) proof ps
353+
merkleCorrectWith h {n = S k} (Node l r) i leaf prf gl gp | False | Just sub =
354+
let prfIs : (prf = sub ++ [(GoRight, rootHashWith h l)])
355+
prfIs = sym (justInj gp)
356+
ih : (reconstructWith h leaf sub = rootHashWith h r)
357+
ih = merkleCorrectWith h r (i `minus` power 2 k) leaf sub gl ps
358+
in rewrite prfIs in
359+
rewrite reconstructAppendWith h leaf sub [(GoRight, rootHashWith h l)] in
360+
rewrite ih in Refl
361+
merkleCorrectWith h {n = S k} (Node l r) i leaf prf gl gp | False | Nothing =
362+
absurd gp
363+
364+
||| SOUNDNESS (merkleCorrect) for the XOR placeholder API: the `hashPairStub`
365+
||| instance of `merkleCorrectWith`. Every inclusion proof produced by
366+
||| `generateProof` for an in-range leaf reconstructs the tree's true root.
265367
|||
266368
||| Stated as a propositional equality on the 32-byte digest — the strongest
267369
||| honest form. `verifyProof` then accepts the proof, because it is exactly
@@ -276,29 +378,4 @@ merkleCorrect : {n : Nat} -> (t : MerkleTree n) -> (i : Nat)
276378
-> getLeafHash t i = Just leaf
277379
-> generateProof t i = Just prf
278380
-> reconstruct leaf prf = rootHashBytes t
279-
merkleCorrect (Leaf h) Z leaf prf gl gp =
280-
rewrite justInj (sym gl) in rewrite justInj (sym gp) in Refl
281-
merkleCorrect (Leaf h) (S j) leaf prf gl gp = absurd gl
282-
merkleCorrect {n = S k} (Node l r) i leaf prf gl gp with (i < power 2 k) proof pb
283-
merkleCorrect {n = S k} (Node l r) i leaf prf gl gp | True with (generateProof l i) proof ps
284-
merkleCorrect {n = S k} (Node l r) i leaf prf gl gp | True | Just sub =
285-
let prfIs : (prf = sub ++ [(GoLeft, rootHashBytes r)])
286-
prfIs = sym (justInj gp)
287-
ih : (reconstruct leaf sub = rootHashBytes l)
288-
ih = merkleCorrect l i leaf sub gl ps
289-
in rewrite prfIs in
290-
rewrite reconstructAppend leaf sub [(GoLeft, rootHashBytes r)] in
291-
rewrite ih in Refl
292-
merkleCorrect {n = S k} (Node l r) i leaf prf gl gp | True | Nothing =
293-
absurd gp
294-
merkleCorrect {n = S k} (Node l r) i leaf prf gl gp | False with (generateProof r (i `minus` power 2 k)) proof ps
295-
merkleCorrect {n = S k} (Node l r) i leaf prf gl gp | False | Just sub =
296-
let prfIs : (prf = sub ++ [(GoRight, rootHashBytes l)])
297-
prfIs = sym (justInj gp)
298-
ih : (reconstruct leaf sub = rootHashBytes r)
299-
ih = merkleCorrect r (i `minus` power 2 k) leaf sub gl ps
300-
in rewrite prfIs in
301-
rewrite reconstructAppend leaf sub [(GoRight, rootHashBytes l)] in
302-
rewrite ih in Refl
303-
merkleCorrect {n = S k} (Node l r) i leaf prf gl gp | False | Nothing =
304-
absurd gp
381+
merkleCorrect t i leaf prf gl gp = merkleCorrectWith hashPairStub t i leaf prf gl gp

0 commit comments

Comments
 (0)