Skip to content

Commit 205df0a

Browse files
hyperpolymathhyperpolymath
authored
proof(merkle): Stage 1.1 — buildMerkleTree/getLeafHash soundness (#47)
Re-lands the Stage 1.1 proof that PR #46's merge dropped: buildGetLeaf (getLeafHash (buildMerkleTree hs) (finToNat i) = Just (index i hs)), Ochrance.Util.VectLemmas (helpers), Merkle.idr visibility bumps, and ipkg module registration. Total, machine-checked, idris2 0.8.0 build 19/19.
1 parent 03ce34f commit 205df0a

4 files changed

Lines changed: 140 additions & 4 deletions

File tree

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

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -119,6 +119,7 @@ MerkleProof = List (Direction, HashBytes)
119119
||| By definition: power 2 (S k) = 2 * power 2 k = power 2 k + power 2 k
120120
||| We prove this by showing that n + 0 = n (plusZeroRightNeutral) and then
121121
||| using the fact that power 2 (S k) reduces to (power 2 k) + (power 2 k + 0).
122+
public export
122123
powerTwoSucc : (k : Nat) -> power 2 (S k) = power 2 k + power 2 k
123124
powerTwoSucc k =
124125
-- power 2 (S k) normalises to: power 2 k + (power 2 k + 0)
@@ -255,7 +256,7 @@ generateProofIO {n = S k} (Node l r) idx =
255256

256257
||| Get a specific leaf hash from a Merkle tree by index (pure version).
257258
||| Returns Nothing if index is out of range.
258-
export
259+
public export
259260
getLeafHash : {n : Nat} -> MerkleTree n -> (leafIdx : Nat) -> Maybe HashBytes
260261
getLeafHash {n = Z} (Leaf h) Z = Just h
261262
getLeafHash {n = Z} (Leaf _) (S _) = Nothing

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

Lines changed: 129 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,129 @@
1+
||| SPDX-License-Identifier: MPL-2.0
2+
|||
3+
||| Ochrance.Filesystem.MerkleBuild - buildMerkleTree / getLeafHash correctness.
4+
|||
5+
||| Proves `buildGetLeaf`: reading leaf `i` back out of `buildMerkleTree hs`
6+
||| returns exactly `index i hs`. This is the round-trip soundness of the
7+
||| balanced Merkle constructor against the by-index leaf accessor.
8+
9+
module Ochrance.Filesystem.MerkleBuild
10+
11+
import Data.Vect
12+
import Data.Fin
13+
import Data.Fin.Split
14+
import Data.Fin.Properties
15+
import Data.Nat
16+
17+
import Ochrance.A2ML.Types
18+
import Ochrance.Filesystem.Merkle
19+
import Ochrance.Util.VectLemmas
20+
21+
%default total
22+
23+
--------------------------------------------------------------------------------
24+
-- Bridging the Bool `idx < power 2 k` to the splitSum case
25+
--
26+
-- For Nat, `(<)` is the Ord-interface default: `x < y = compare x y == LT`,
27+
-- and `compare = compareNat`. So `idx < m` is `compareNat idx m == LT`.
28+
--------------------------------------------------------------------------------
29+
30+
||| `compareNat a b` is `LT` whenever `a` is strictly below `b`.
31+
compareNatLT : (a, b : Nat) -> LT a b -> compareNat a b = LT
32+
compareNatLT Z (S _) _ = Refl
33+
compareNatLT (S a) (S b) (LTESucc p) = compareNatLT a b p
34+
35+
||| Any `Fin m` index is `< m` as a Bool. (`<` here is the Nat Ord default.)
36+
finBoundLT : (a : Fin m) -> (finToNat a < m) = True
37+
finBoundLT a =
38+
rewrite compareNatLT (finToNat a) m (elemSmallerThanBound a) in Refl
39+
40+
||| `compareNat (p + x) p` is never `LT`: `p + x` is at least `p`.
41+
compareNatPlusNotLT : (p, x : Nat) ->
42+
Either (compareNat (p + x) p = EQ) (compareNat (p + x) p = GT)
43+
compareNatPlusNotLT Z Z = Left Refl
44+
compareNatPlusNotLT Z (S _) = Right Refl
45+
compareNatPlusNotLT (S p) x = compareNatPlusNotLT p x
46+
47+
||| `(p + x) < p` is `False`: a left-padded index never falls in the left half.
48+
plusNotLT : (p, x : Nat) -> ((p + x) < p) = False
49+
plusNotLT p x = case compareNatPlusNotLT p x of
50+
Left eq => rewrite eq in Refl
51+
Right eq => rewrite eq in Refl
52+
53+
--------------------------------------------------------------------------------
54+
-- buildMerkleTree / getLeafHash round-trip soundness
55+
--------------------------------------------------------------------------------
56+
57+
||| Core of the inductive step at height `S k`, stated on the *already split*
58+
||| halves so the `splitAt`/`splitSum` reasoning is decoupled from the transport.
59+
|||
60+
||| `left ++ right` is the (transported) leaf vector and `j` is the (transported)
61+
||| index into it; the two IH calls discharge each subtree.
62+
buildGetLeafSplit :
63+
{k : Nat} ->
64+
(left, right : Vect (power 2 k) HashBytes) ->
65+
(j : Fin (power 2 k + power 2 k)) ->
66+
((bl : Vect (power 2 k) HashBytes) -> (a : Fin (power 2 k)) ->
67+
getLeafHash (buildMerkleTree {n = k} bl) (finToNat a) = Just (index a bl)) ->
68+
getLeafHash (Node (buildMerkleTree {n = k} left) (buildMerkleTree {n = k} right))
69+
(finToNat j)
70+
= Just (index j (left ++ right))
71+
buildGetLeafSplit {k} left right j ih with (splitSum {m = power 2 k} {n = power 2 k} j)
72+
proof splitEq
73+
_ | Left a =
74+
-- j = weakenN (power 2 k) a ; index lands in `left`, THEN branch taken.
75+
let jIs : (j = weakenN (power 2 k) a)
76+
jIs = trans (sym (indexOfSplitSumInverse {m = power 2 k} {n = power 2 k} j))
77+
(cong indexSum splitEq)
78+
finEq : (finToNat j = finToNat a)
79+
finEq = trans (cong finToNat jIs) (finToNatWeakenNNeutral (power 2 k) a)
80+
idxEq : (index j (left ++ right) = index a left)
81+
idxEq = trans (cong (\z => index z (left ++ right)) jIs)
82+
(indexAppendLeft a left right)
83+
in rewrite finEq in
84+
rewrite finBoundLT a in
85+
rewrite idxEq in
86+
ih left a
87+
_ | Right b =
88+
-- j = shift (power 2 k) b ; index lands in `right`, ELSE branch taken.
89+
let jIs : (j = shift (power 2 k) b)
90+
jIs = trans (sym (indexOfSplitSumInverse {m = power 2 k} {n = power 2 k} j))
91+
(cong indexSum splitEq)
92+
finEq : (finToNat j = power 2 k + finToNat b)
93+
finEq = trans (cong finToNat jIs) (finToNatShift (power 2 k) b)
94+
idxEq : (index j (left ++ right) = index b right)
95+
idxEq = trans (cong (\z => index z (left ++ right)) jIs)
96+
(indexAppendRight b left right)
97+
in rewrite finEq in
98+
rewrite plusNotLT (power 2 k) (finToNat b) in
99+
rewrite minusPlus {n = finToNat b} (power 2 k) in
100+
rewrite idxEq in
101+
ih right b
102+
103+
||| Reading leaf `i` back out of `buildMerkleTree hs` returns `index i hs`.
104+
||| The constructor places leaf `i` at exactly position `finToNat i`.
105+
export
106+
buildGetLeaf : {n : Nat} -> (hs : Vect (power 2 n) HashBytes) -> (i : Fin (power 2 n)) ->
107+
getLeafHash (buildMerkleTree {n} hs) (finToNat i) = Just (index i hs)
108+
buildGetLeaf {n = Z} [h] FZ = Refl
109+
buildGetLeaf {n = S k} hs i with (splitAt (power 2 k)
110+
(replace {p = \x => Vect x HashBytes} (powerTwoSucc k) hs))
111+
proof splitPrf
112+
_ | (left, right) =
113+
let i' : Fin (power 2 k + power 2 k)
114+
i' = replace {p = Fin} (powerTwoSucc k) i
115+
hs' : Vect (power 2 k + power 2 k) HashBytes
116+
hs' = replace {p = \x => Vect x HashBytes} (powerTwoSucc k) hs
117+
-- The two split halves re-append to the transported vector.
118+
catEq : (left ++ right = hs')
119+
catEq = trans (sym (cong (\z => fst z ++ snd z) splitPrf))
120+
(splitAtConcat (power 2 k) hs')
121+
-- index/finToNat are preserved by the transport.
122+
finEq : (finToNat i = finToNat i')
123+
finEq = sym (finToNatReplace (powerTwoSucc k) i)
124+
idxEq : (index i hs = index i' (left ++ right))
125+
idxEq = trans (sym (indexReplace (powerTwoSucc k) i hs))
126+
(sym (cong (index i') catEq))
127+
in rewrite finEq in
128+
rewrite idxEq in
129+
buildGetLeafSplit left right i' buildGetLeaf

ochrance-core/Ochrance/Scratch.idr renamed to ochrance-core/Ochrance/Util/VectLemmas.idr

Lines changed: 7 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,10 @@
1-
||| Stage-1 scratch: helper lemmas for buildMerkleTree correctness.
2-
||| Iterated here (no Ochrance deps) before folding into Merkle.
3-
module Ochrance.Scratch
1+
||| SPDX-License-Identifier: MPL-2.0
2+
|||
3+
||| Ochrance.Util.VectLemmas - reusable Vect/Fin lemmas for the Merkle proofs.
4+
|||
5+
||| index-over-append (both halves), transport cancellation for `replace`,
6+
||| finToNat under transport, and the splitAt re-append law.
7+
module Ochrance.Util.VectLemmas
48

59
import Data.Vect
610
import Data.Fin

‎ochrance.ipkg‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -23,6 +23,8 @@ modules = Ochrance.A2ML.Types
2323
, Ochrance.Util.Hex
2424
, Ochrance.Filesystem.Types
2525
, Ochrance.Filesystem.Merkle
26+
, Ochrance.Util.VectLemmas
27+
, Ochrance.Filesystem.MerkleBuild
2628
, Ochrance.Filesystem.Verify
2729
, Ochrance.Filesystem.Repair
2830
, Ochrance.FFI.Echidna

0 commit comments

Comments
 (0)