diff --git a/.machine_readable/6a2/STATE.a2ml b/.machine_readable/6a2/STATE.a2ml index 744cee9..774b02a 100644 --- a/.machine_readable/6a2/STATE.a2ml +++ b/.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)", diff --git a/docs/PROOFS.adoc b/docs/PROOFS.adoc index 4d0674a..ab3f005 100644 --- a/docs/PROOFS.adoc +++ b/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 — diff --git a/ochrance-core/Ochrance/Filesystem/VerifyRoot.idr b/ochrance-core/Ochrance/Filesystem/VerifyRoot.idr new file mode 100644 index 0000000..14dd19b --- /dev/null +++ b/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 diff --git a/ochrance.ipkg b/ochrance.ipkg index 6ee1d4b..b82a4a6 100644 --- a/ochrance.ipkg +++ b/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