From 2402f000758ea0cab4cfb1a9ea394c0a2cf1717a Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 15 Jun 2026 17:48:20 +0000 Subject: [PATCH] proof(merkle): prove buildMerkleTree/getLeafHash round-trip soundness (Stage 1.1) buildGetLeaf : {n} -> (hs : Vect (power 2 n) HashBytes) -> (i : Fin (power 2 n)) -> getLeafHash (buildMerkleTree hs) (finToNat i) = Just (index i hs). Total, machine-checked, no believe_me/assert/postulate/holes; whole package builds under --total. New Ochrance.Util.VectLemmas (indexAppendLeft/Right, indexReplace transport-cancellation, finToNatReplace, splitAtConcat) and Ochrance.Filesystem.MerkleBuild (buildGetLeaf + buildGetLeafSplit + compareNat bridge lemmas). The replace/powerTwoSucc transport is discharged by indexReplace; split halves by indexAppend*; the Bool 'idx < power 2 k' branch via compareNat (the Ord Nat default, not Data.Nat.lt). Merkle.idr: powerTwoSucc + getLeafHash export->public export (visibility only, no logic change). https://claude.ai/code/session_011z2t8zAxfcCNLJzU7YdpBQ --- ochrance-core/Ochrance/Filesystem/Merkle.idr | 3 +- .../Ochrance/Filesystem/MerkleBuild.idr | 129 ++++++++++++++++++ .../{Scratch.idr => Util/VectLemmas.idr} | 10 +- ochrance.ipkg | 2 + 4 files changed, 140 insertions(+), 4 deletions(-) create mode 100644 ochrance-core/Ochrance/Filesystem/MerkleBuild.idr rename ochrance-core/Ochrance/{Scratch.idr => Util/VectLemmas.idr} (85%) diff --git a/ochrance-core/Ochrance/Filesystem/Merkle.idr b/ochrance-core/Ochrance/Filesystem/Merkle.idr index 7546d80..86d293a 100644 --- a/ochrance-core/Ochrance/Filesystem/Merkle.idr +++ b/ochrance-core/Ochrance/Filesystem/Merkle.idr @@ -119,6 +119,7 @@ MerkleProof = List (Direction, HashBytes) ||| By definition: power 2 (S k) = 2 * power 2 k = power 2 k + power 2 k ||| We prove this by showing that n + 0 = n (plusZeroRightNeutral) and then ||| using the fact that power 2 (S k) reduces to (power 2 k) + (power 2 k + 0). +public export powerTwoSucc : (k : Nat) -> power 2 (S k) = power 2 k + power 2 k powerTwoSucc k = -- 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 = ||| Get a specific leaf hash from a Merkle tree by index (pure version). ||| Returns Nothing if index is out of range. -export +public export getLeafHash : {n : Nat} -> MerkleTree n -> (leafIdx : Nat) -> Maybe HashBytes getLeafHash {n = Z} (Leaf h) Z = Just h getLeafHash {n = Z} (Leaf _) (S _) = Nothing diff --git a/ochrance-core/Ochrance/Filesystem/MerkleBuild.idr b/ochrance-core/Ochrance/Filesystem/MerkleBuild.idr new file mode 100644 index 0000000..143247d --- /dev/null +++ b/ochrance-core/Ochrance/Filesystem/MerkleBuild.idr @@ -0,0 +1,129 @@ +||| SPDX-License-Identifier: MPL-2.0 +||| +||| Ochrance.Filesystem.MerkleBuild - buildMerkleTree / getLeafHash correctness. +||| +||| Proves `buildGetLeaf`: reading leaf `i` back out of `buildMerkleTree hs` +||| returns exactly `index i hs`. This is the round-trip soundness of the +||| balanced Merkle constructor against the by-index leaf accessor. + +module Ochrance.Filesystem.MerkleBuild + +import Data.Vect +import Data.Fin +import Data.Fin.Split +import Data.Fin.Properties +import Data.Nat + +import Ochrance.A2ML.Types +import Ochrance.Filesystem.Merkle +import Ochrance.Util.VectLemmas + +%default total + +-------------------------------------------------------------------------------- +-- Bridging the Bool `idx < power 2 k` to the splitSum case +-- +-- For Nat, `(<)` is the Ord-interface default: `x < y = compare x y == LT`, +-- and `compare = compareNat`. So `idx < m` is `compareNat idx m == LT`. +-------------------------------------------------------------------------------- + +||| `compareNat a b` is `LT` whenever `a` is strictly below `b`. +compareNatLT : (a, b : Nat) -> LT a b -> compareNat a b = LT +compareNatLT Z (S _) _ = Refl +compareNatLT (S a) (S b) (LTESucc p) = compareNatLT a b p + +||| Any `Fin m` index is `< m` as a Bool. (`<` here is the Nat Ord default.) +finBoundLT : (a : Fin m) -> (finToNat a < m) = True +finBoundLT a = + rewrite compareNatLT (finToNat a) m (elemSmallerThanBound a) in Refl + +||| `compareNat (p + x) p` is never `LT`: `p + x` is at least `p`. +compareNatPlusNotLT : (p, x : Nat) -> + Either (compareNat (p + x) p = EQ) (compareNat (p + x) p = GT) +compareNatPlusNotLT Z Z = Left Refl +compareNatPlusNotLT Z (S _) = Right Refl +compareNatPlusNotLT (S p) x = compareNatPlusNotLT p x + +||| `(p + x) < p` is `False`: a left-padded index never falls in the left half. +plusNotLT : (p, x : Nat) -> ((p + x) < p) = False +plusNotLT p x = case compareNatPlusNotLT p x of + Left eq => rewrite eq in Refl + Right eq => rewrite eq in Refl + +-------------------------------------------------------------------------------- +-- buildMerkleTree / getLeafHash round-trip soundness +-------------------------------------------------------------------------------- + +||| Core of the inductive step at height `S k`, stated on the *already split* +||| halves so the `splitAt`/`splitSum` reasoning is decoupled from the transport. +||| +||| `left ++ right` is the (transported) leaf vector and `j` is the (transported) +||| index into it; the two IH calls discharge each subtree. +buildGetLeafSplit : + {k : Nat} -> + (left, right : Vect (power 2 k) HashBytes) -> + (j : Fin (power 2 k + power 2 k)) -> + ((bl : Vect (power 2 k) HashBytes) -> (a : Fin (power 2 k)) -> + getLeafHash (buildMerkleTree {n = k} bl) (finToNat a) = Just (index a bl)) -> + getLeafHash (Node (buildMerkleTree {n = k} left) (buildMerkleTree {n = k} right)) + (finToNat j) + = Just (index j (left ++ right)) +buildGetLeafSplit {k} left right j ih with (splitSum {m = power 2 k} {n = power 2 k} j) + proof splitEq + _ | Left a = + -- j = weakenN (power 2 k) a ; index lands in `left`, THEN branch taken. + let jIs : (j = weakenN (power 2 k) a) + jIs = trans (sym (indexOfSplitSumInverse {m = power 2 k} {n = power 2 k} j)) + (cong indexSum splitEq) + finEq : (finToNat j = finToNat a) + finEq = trans (cong finToNat jIs) (finToNatWeakenNNeutral (power 2 k) a) + idxEq : (index j (left ++ right) = index a left) + idxEq = trans (cong (\z => index z (left ++ right)) jIs) + (indexAppendLeft a left right) + in rewrite finEq in + rewrite finBoundLT a in + rewrite idxEq in + ih left a + _ | Right b = + -- j = shift (power 2 k) b ; index lands in `right`, ELSE branch taken. + let jIs : (j = shift (power 2 k) b) + jIs = trans (sym (indexOfSplitSumInverse {m = power 2 k} {n = power 2 k} j)) + (cong indexSum splitEq) + finEq : (finToNat j = power 2 k + finToNat b) + finEq = trans (cong finToNat jIs) (finToNatShift (power 2 k) b) + idxEq : (index j (left ++ right) = index b right) + idxEq = trans (cong (\z => index z (left ++ right)) jIs) + (indexAppendRight b left right) + in rewrite finEq in + rewrite plusNotLT (power 2 k) (finToNat b) in + rewrite minusPlus {n = finToNat b} (power 2 k) in + rewrite idxEq in + ih right b + +||| Reading leaf `i` back out of `buildMerkleTree hs` returns `index i hs`. +||| The constructor places leaf `i` at exactly position `finToNat i`. +export +buildGetLeaf : {n : Nat} -> (hs : Vect (power 2 n) HashBytes) -> (i : Fin (power 2 n)) -> + getLeafHash (buildMerkleTree {n} hs) (finToNat i) = Just (index i hs) +buildGetLeaf {n = Z} [h] FZ = Refl +buildGetLeaf {n = S k} hs i with (splitAt (power 2 k) + (replace {p = \x => Vect x HashBytes} (powerTwoSucc k) hs)) + proof splitPrf + _ | (left, right) = + let i' : Fin (power 2 k + power 2 k) + i' = replace {p = Fin} (powerTwoSucc k) i + hs' : Vect (power 2 k + power 2 k) HashBytes + hs' = replace {p = \x => Vect x HashBytes} (powerTwoSucc k) hs + -- The two split halves re-append to the transported vector. + catEq : (left ++ right = hs') + catEq = trans (sym (cong (\z => fst z ++ snd z) splitPrf)) + (splitAtConcat (power 2 k) hs') + -- index/finToNat are preserved by the transport. + finEq : (finToNat i = finToNat i') + finEq = sym (finToNatReplace (powerTwoSucc k) i) + idxEq : (index i hs = index i' (left ++ right)) + idxEq = trans (sym (indexReplace (powerTwoSucc k) i hs)) + (sym (cong (index i') catEq)) + in rewrite finEq in + rewrite idxEq in + buildGetLeafSplit left right i' buildGetLeaf diff --git a/ochrance-core/Ochrance/Scratch.idr b/ochrance-core/Ochrance/Util/VectLemmas.idr similarity index 85% rename from ochrance-core/Ochrance/Scratch.idr rename to ochrance-core/Ochrance/Util/VectLemmas.idr index 739d7fa..5e4a613 100644 --- a/ochrance-core/Ochrance/Scratch.idr +++ b/ochrance-core/Ochrance/Util/VectLemmas.idr @@ -1,6 +1,10 @@ -||| Stage-1 scratch: helper lemmas for buildMerkleTree correctness. -||| Iterated here (no Ochrance deps) before folding into Merkle. -module Ochrance.Scratch +||| SPDX-License-Identifier: MPL-2.0 +||| +||| Ochrance.Util.VectLemmas - reusable Vect/Fin lemmas for the Merkle proofs. +||| +||| index-over-append (both halves), transport cancellation for `replace`, +||| finToNat under transport, and the splitAt re-append law. +module Ochrance.Util.VectLemmas import Data.Vect import Data.Fin diff --git a/ochrance.ipkg b/ochrance.ipkg index b669993..ba72800 100644 --- a/ochrance.ipkg +++ b/ochrance.ipkg @@ -23,6 +23,8 @@ modules = Ochrance.A2ML.Types , Ochrance.Util.Hex , Ochrance.Filesystem.Types , Ochrance.Filesystem.Merkle + , Ochrance.Util.VectLemmas + , Ochrance.Filesystem.MerkleBuild , Ochrance.Filesystem.Verify , Ochrance.Filesystem.Repair , Ochrance.FFI.Echidna