|
| 1 | +||| SPDX-License-Identifier: MPL-2.0 |
| 2 | +||| |
| 3 | +||| Ochrance.Filesystem.VerifyRoot - the root-comparing verify path (executable). |
| 4 | +||| |
| 5 | +||| This is the *plumbing* that the soundness theorem `merkleRootVerifyHashSound` |
| 6 | +||| licenses: pad an arbitrary-length block-hash list to a power-of-two leaf `Vect`, |
| 7 | +||| build the Merkle tree, and compare its root to a committed root (e.g. |
| 8 | +||| `FSSnapshot.rootHash`). Engineering, not a proof - the *soundness* of accepting on |
| 9 | +||| a root match is `Ochrance.Filesystem.VerifyMerkle.merkleRootVerifyHashSound` |
| 10 | +||| (modulo its named `CollisionResistant` / `DecodeInjective` boundaries and the |
| 11 | +||| primitive `==`). All total. |
| 12 | +module Ochrance.Filesystem.VerifyRoot |
| 13 | + |
| 14 | +import Data.Vect |
| 15 | + |
| 16 | +import Ochrance.A2ML.Types |
| 17 | +import Ochrance.Filesystem.Types |
| 18 | +import Ochrance.Filesystem.Merkle |
| 19 | +import Ochrance.Filesystem.VerifyMerkle |
| 20 | + |
| 21 | +%default total |
| 22 | + |
| 23 | +-------------------------------------------------------------------------------- |
| 24 | +-- Power-of-two leaf layout |
| 25 | +-------------------------------------------------------------------------------- |
| 26 | + |
| 27 | +||| Pad (or truncate) a list to an exact length, filling any shortfall with `pad`. |
| 28 | +||| Structural on the target length; the layout below always calls it with a target |
| 29 | +||| >= the list length, so it never truncates in practice. |
| 30 | +public export |
| 31 | +padToLength : (m : Nat) -> a -> List a -> Vect m a |
| 32 | +padToLength Z _ _ = [] |
| 33 | +padToLength (S k) pad [] = pad :: padToLength k pad [] |
| 34 | +padToLength (S k) pad (x :: xs) = x :: padToLength k pad xs |
| 35 | + |
| 36 | +||| Smallest exponent `n` with `k <= 2^n`, by doubling (fuelled by `k` for totality). |
| 37 | +nextPow2ExpGo : (fuel, n, acc, k : Nat) -> Nat |
| 38 | +nextPow2ExpGo Z n _ _ = n |
| 39 | +nextPow2ExpGo (S f) n acc k = if k <= acc then n else nextPow2ExpGo f (S n) (acc + acc) k |
| 40 | + |
| 41 | +public export |
| 42 | +nextPow2Exp : Nat -> Nat |
| 43 | +nextPow2Exp k = nextPow2ExpGo k 0 1 k |
| 44 | + |
| 45 | +||| Lay an arbitrary-length block-hash list out as a power-of-two leaf vector, padding |
| 46 | +||| with `emptyHash`. The dependent pair carries the chosen height `n`. |
| 47 | +public export |
| 48 | +layoutLeaves : List HashBytes -> (n : Nat ** Vect (power 2 n) HashBytes) |
| 49 | +layoutLeaves xs = let n = nextPow2Exp (length xs) |
| 50 | + in (n ** padToLength (power 2 n) emptyHash xs) |
| 51 | + |
| 52 | +-------------------------------------------------------------------------------- |
| 53 | +-- Root-comparing verify path |
| 54 | +-------------------------------------------------------------------------------- |
| 55 | + |
| 56 | +||| Root-based block verification: build the padded Merkle tree from the block hashes |
| 57 | +||| and compare its root to the expected (committed) root. `True` iff they match. |
| 58 | +public export |
| 59 | +verifyByRoot : Combiner -> List HashBytes -> HashBytes -> Bool |
| 60 | +verifyByRoot h blocks expectedRoot = |
| 61 | + let (n ** leaves) = layoutLeaves blocks |
| 62 | + in rootHashWith h (buildMerkleTree {n} leaves) == expectedRoot |
| 63 | + |
| 64 | +||| The fully live version: decode A2ML `Hash`es to bytes (via `hashToBytes`), then |
| 65 | +||| root-verify. `Nothing` if any hash is malformed; `Just b` with the match result. |
| 66 | +public export |
| 67 | +verifyByRootHash : Combiner -> List Hash -> Hash -> Maybe Bool |
| 68 | +verifyByRootHash h blocks expected = |
| 69 | + do blockBytes <- traverse hashToBytes blocks |
| 70 | + expBytes <- hashToBytes expected |
| 71 | + pure (verifyByRoot h blockBytes expBytes) |
| 72 | + |
| 73 | +-------------------------------------------------------------------------------- |
| 74 | +-- Wiring to FSState / FSSnapshot |
| 75 | +-------------------------------------------------------------------------------- |
| 76 | + |
| 77 | +||| Indices `[0, 1, ..., n-1]`. |
| 78 | +upTo : Nat -> List Nat |
| 79 | +upTo Z = [] |
| 80 | +upTo (S k) = upTo k ++ [k] |
| 81 | + |
| 82 | +||| Collect a filesystem's block hashes in index order; `Nothing` if any is absent. |
| 83 | +public export |
| 84 | +fsBlockHashes : FSState -> Maybe (List Hash) |
| 85 | +fsBlockHashes fs = traverse fs.blockHash (upTo fs.numBlocks) |
| 86 | + |
| 87 | +||| The runtime root-verify path: check a filesystem against a snapshot's committed |
| 88 | +||| Merkle root. `Nothing` if a block is missing or a hash is malformed; otherwise |
| 89 | +||| `Just` the match decision. Soundness: `merkleRootVerifyHashSound`. |
| 90 | +public export |
| 91 | +verifySnapshotRoot : Combiner -> FSState -> FSSnapshot -> Maybe Bool |
| 92 | +verifySnapshotRoot h fs snap = |
| 93 | + do blocks <- fsBlockHashes fs |
| 94 | + verifyByRootHash h blocks snap.rootHash |
0 commit comments