feat: root-comparing verify path + power-of-two leaf layout (VerifyRoot)

.machine_readable/6a2/STATE.a2ml

@@ -63,7 +63,8 @@ actions = [
   "Stage 2 provable core COMPLETE — 2.1 validateManifestSound, 2.2 verifyRefsSound, 2.3 parsePairsRoundtrip; all machine-checked. DEFERRED (architectural decision): wire verify to merkleCorrect — the verify path builds no Merkle tree today",
   "Stage 3.1 DONE — pure repair primitive correctness (repairBlockPure factored out; sets/preserves/numBlocks/idempotent machine-checked)",
   "Stage 3.2 DONE — whole-manifest repair ⇒ verify (repairThenVerify, module RepairVerify). repairRefsPure folds repairBlockPure; proof = verifyRefsComplete ∘ repairRefsConsistent; GoodRefs precondition + hashRefl hypothesis, both named",
-  "Live-verifier Merkle redesign SOUNDNESS DONE (merkleRootVerifyHashSound) — root-comparing verifier is sound at the Hash level, modulo named CollisionResistant + DecodeInjective. REMAINING is plumbing only (not a proof): pad arbitrary-length block list to power-of-2 leaf Vect + switch the runtime verify path over. NEXT options: that plumbing, or Stage 4 (discharge CollisionResistant against the real combiner), or harvest the VerifiedSubsystem law",
+  "Live-verifier Merkle redesign SOUNDNESS DONE (merkleRootVerifyHashSound) — root-comparing verifier is sound at the Hash level, modulo named CollisionResistant + DecodeInjective",
+  "Live-verifier PLUMBING DONE (module VerifyRoot) — padToLength/nextPow2Exp/layoutLeaves pad to power-of-2 leaf Vect; verifyByRoot/verifyByRootHash build tree + compare roots; fsBlockHashes/verifySnapshotRoot = runtime path vs FSSnapshot.rootHash. Executable, total; accept-on-match soundness = merkleRootVerifyHashSound",
   "Stage 2.4 DONE — verify↔Merkle proof-level wiring (rootFaithful/rootVerifySound): the root is a faithful fingerprint of the blocks (binding). REMAINING: connect to the live Hash-based verifyRefsHelper via hex Hash<->HashBytes conversion (2.3-bounded) + power-of-two layout (verify-path change, not a proof)",
   "Stage 3.2 (next provable): whole-manifest repairPure ⇒ verifyRefsHelper accepts (distinct-in-range ref-name precondition + isolated Hash-reflexivity hypothesis)",
   "Remove Idris-side crypto stubs and build + link libochrance.so into the flow (unblocks the crypto-integrity claim)",

docs/PROOFS.adoc

@@ -229,8 +229,11 @@ block-hash vectors that decode and yield equal Merkle roots are equal - carrying
 boundaries: `CollisionResistant h` (1.4) and `DecodeInjective dec` (the hex wall,
 2.3); stated for an arbitrary `dec`, instantiated at `hashToBytes`.
 +
-STILL OPEN (plumbing, not a proof): padding an arbitrary-length block list to a
-power-of-two leaf `Vect` and switching the runtime verify path over - engineering.
+DONE (plumbing): `Ochrance.Filesystem.VerifyRoot` - `padToLength` + `nextPow2Exp` +
+`layoutLeaves` pad an arbitrary-length block list to a power-of-two leaf `Vect`;
+`verifyByRoot` / `verifyByRootHash` build the tree and compare roots; `fsBlockHashes`
++ `verifySnapshotRoot` are the runtime path against `FSSnapshot.rootHash`. Executable,
+total; its accept-on-match soundness is `merkleRootVerifyHashSound`.
 
 . *[DONE — 2.3]* Hex codec structural round-trip. The full
   `hexStringToBytes (bytesToHex bs) = Just bs` crosses two primitive walls —

ochrance-core/Ochrance/Filesystem/VerifyRoot.idr

@@ -0,0 +1,94 @@
+||| SPDX-License-Identifier: MPL-2.0
+|||
+||| Ochrance.Filesystem.VerifyRoot - the root-comparing verify path (executable).
+|||
+||| This is the *plumbing* that the soundness theorem `merkleRootVerifyHashSound`
+||| licenses: pad an arbitrary-length block-hash list to a power-of-two leaf `Vect`,
+||| build the Merkle tree, and compare its root to a committed root (e.g.
+||| `FSSnapshot.rootHash`). Engineering, not a proof - the *soundness* of accepting on
+||| a root match is `Ochrance.Filesystem.VerifyMerkle.merkleRootVerifyHashSound`
+||| (modulo its named `CollisionResistant` / `DecodeInjective` boundaries and the
+||| primitive `==`). All total.
+module Ochrance.Filesystem.VerifyRoot
+
+import Data.Vect
+
+import Ochrance.A2ML.Types
+import Ochrance.Filesystem.Types
+import Ochrance.Filesystem.Merkle
+import Ochrance.Filesystem.VerifyMerkle
+
+%default total
+
+--------------------------------------------------------------------------------
+-- Power-of-two leaf layout
+--------------------------------------------------------------------------------
+
+||| Pad (or truncate) a list to an exact length, filling any shortfall with `pad`.
+||| Structural on the target length; the layout below always calls it with a target
+||| >= the list length, so it never truncates in practice.
+public export
+padToLength : (m : Nat) -> a -> List a -> Vect m a
+padToLength Z     _   _         = []
+padToLength (S k) pad []        = pad :: padToLength k pad []
+padToLength (S k) pad (x :: xs) = x :: padToLength k pad xs
+
+||| Smallest exponent `n` with `k <= 2^n`, by doubling (fuelled by `k` for totality).
+nextPow2ExpGo : (fuel, n, acc, k : Nat) -> Nat
+nextPow2ExpGo Z     n _   _ = n
+nextPow2ExpGo (S f) n acc k = if k <= acc then n else nextPow2ExpGo f (S n) (acc + acc) k
+
+public export
+nextPow2Exp : Nat -> Nat
+nextPow2Exp k = nextPow2ExpGo k 0 1 k
+
+||| Lay an arbitrary-length block-hash list out as a power-of-two leaf vector, padding
+||| with `emptyHash`. The dependent pair carries the chosen height `n`.
+public export
+layoutLeaves : List HashBytes -> (n : Nat ** Vect (power 2 n) HashBytes)
+layoutLeaves xs = let n = nextPow2Exp (length xs)
+                  in (n ** padToLength (power 2 n) emptyHash xs)
+
+--------------------------------------------------------------------------------
+-- Root-comparing verify path
+--------------------------------------------------------------------------------
+
+||| Root-based block verification: build the padded Merkle tree from the block hashes
+||| and compare its root to the expected (committed) root. `True` iff they match.
+public export
+verifyByRoot : Combiner -> List HashBytes -> HashBytes -> Bool
+verifyByRoot h blocks expectedRoot =
+  let (n ** leaves) = layoutLeaves blocks
+  in rootHashWith h (buildMerkleTree {n} leaves) == expectedRoot
+
+||| The fully live version: decode A2ML `Hash`es to bytes (via `hashToBytes`), then
+||| root-verify. `Nothing` if any hash is malformed; `Just b` with the match result.
+public export
+verifyByRootHash : Combiner -> List Hash -> Hash -> Maybe Bool
+verifyByRootHash h blocks expected =
+  do blockBytes <- traverse hashToBytes blocks
+     expBytes   <- hashToBytes expected
+     pure (verifyByRoot h blockBytes expBytes)
+
+--------------------------------------------------------------------------------
+-- Wiring to FSState / FSSnapshot
+--------------------------------------------------------------------------------
+
+||| Indices `[0, 1, ..., n-1]`.
+upTo : Nat -> List Nat
+upTo Z     = []
+upTo (S k) = upTo k ++ [k]
+
+||| Collect a filesystem's block hashes in index order; `Nothing` if any is absent.
+public export
+fsBlockHashes : FSState -> Maybe (List Hash)
+fsBlockHashes fs = traverse fs.blockHash (upTo fs.numBlocks)
+
+||| The runtime root-verify path: check a filesystem against a snapshot's committed
+||| Merkle root. `Nothing` if a block is missing or a hash is malformed; otherwise
+||| `Just` the match decision. Soundness: `merkleRootVerifyHashSound`.
+public export
+verifySnapshotRoot : Combiner -> FSState -> FSSnapshot -> Maybe Bool
+verifySnapshotRoot h fs snap =
+  do blocks <- fsBlockHashes fs
+     verifyByRootHash h blocks snap.rootHash

ochrance.ipkg

@@ -32,6 +32,7 @@ modules = Ochrance.A2ML.Types
         , Ochrance.Filesystem.Verify
         , Ochrance.Filesystem.VerifyProof
         , Ochrance.Filesystem.VerifyMerkle
+        , Ochrance.Filesystem.VerifyRoot
         , Ochrance.Filesystem.Repair
         , Ochrance.Filesystem.RepairProof
         , Ochrance.Filesystem.RepairVerify