proof(merkle): Stage 1.1 — buildMerkleTree/getLeafHash soundness (re-land after #46)

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

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

ochrance-core/Ochrance/Scratch.idr → 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

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