|
11 | 11 | ||| trust a root, and it carries Stage 1.4's binding guarantee into the verification |
12 | 12 | ||| use-case. |
13 | 13 | ||| |
14 | | -||| Three verification modes are surfaced, generic -> granular: |
| 14 | +||| Verification modes are surfaced, generic -> granular: |
15 | 15 | ||| * `rootFaithful` / `rootVerifySound` - root-equivalence (one root check stands |
16 | 16 | ||| in for every block hash; backed by `merkleBindingTree`, Stage 1.4); |
17 | 17 | ||| * `inclusionVerifySound` - inclusion-proof verification (per-leaf `(leaf, proof)` |
18 | 18 | ||| reconstructs the root; backed by `merkleCorrect`, Stage 1.1); |
19 | | -||| * `hashToBytes` - the live `Hash` <-> `HashBytes` bridge for snapshot-root |
20 | | -||| verification, composing with `rootVerifySound`. |
| 19 | +||| * `hashToBytes` - the live `Hash` <-> `HashBytes` bridge; |
| 20 | +||| * `merkleRootVerifyHashSound` - LIVE root-verification soundness at the A2ML |
| 21 | +||| `Hash` level: two block-hash vectors that decode and yield equal roots are |
| 22 | +||| equal. This is the theorem a redesigned root-comparing `verifyRefsHelper` rests |
| 23 | +||| on; it carries `rootVerifySound` up across the decoder bridge. |
21 | 24 | ||| |
22 | | -||| NOTE (remaining): fully replacing the *live* A2ML-`Hash`-based verifier |
23 | | -||| (`verifyRefsHelper`, Stage 2.2) with a tree build needs the hex conversion |
24 | | -||| correctness (Stage 2.3, bounded by the `unpack`/`pack` + `Bits8` walls) and a |
25 | | -||| power-of-two leaf layout - a verify-path change, documented in docs/PROOFS.adoc, |
26 | | -||| not faked here. |
| 25 | +||| NOTE (remaining): the *soundness* of replacing the live `Hash`-based verifier with |
| 26 | +||| a tree build is now proven (`merkleRootVerifyHashSound`), modulo two named |
| 27 | +||| boundaries - `CollisionResistant h` (1.4) and `DecodeInjective dec` (the hex wall, |
| 28 | +||| 2.3). What is left is purely *plumbing*: padding an arbitrary-length block list to |
| 29 | +||| a power-of-two leaf `Vect` and swapping the verify path over - engineering, not a |
| 30 | +||| proof, and tracked in docs/PROOFS.adoc. |
27 | 31 | module Ochrance.Filesystem.VerifyMerkle |
28 | 32 |
|
29 | 33 | import Data.Vect |
@@ -96,3 +100,61 @@ inclusionVerifySound t i leaf prf gl gp = merkleCorrect t i leaf prf gl gp |
96 | 100 | public export |
97 | 101 | hashToBytes : Hash -> Maybe HashBytes |
98 | 102 | hashToBytes h = hexStringToVect 32 h.value |
| 103 | + |
| 104 | +-------------------------------------------------------------------------------- |
| 105 | +-- Mode 2 (live): root-verification soundness at the A2ML `Hash` level |
| 106 | +-------------------------------------------------------------------------------- |
| 107 | +-- |
| 108 | +-- These are stated for an arbitrary decoder `dec : Hash -> Maybe HashBytes` (exactly |
| 109 | +-- as `rootVerifySound` is stated for an arbitrary `h : Combiner`); the intended |
| 110 | +-- instance is `dec := hashToBytes`, supplied at the call site by a redesigned |
| 111 | +-- verifier. Keeping `dec` an explicit parameter also avoids it being auto-bound as |
| 112 | +-- an unbound implicit in the signatures. |
| 113 | + |
| 114 | +||| Decode every hash in a vector (structural, so it reduces definitionally - unlike |
| 115 | +||| the `Functor` `map`, which the per-element proofs below need to compute through). |
| 116 | +public export |
| 117 | +decAll : (Hash -> Maybe HashBytes) -> Vect k Hash -> Vect k (Maybe HashBytes) |
| 118 | +decAll dec [] = [] |
| 119 | +decAll dec (x :: xs) = dec x :: decAll dec xs |
| 120 | + |
| 121 | +||| A decoder is INJECTIVE - distinct hashes give distinct bytes. True for well-formed |
| 122 | +||| hashes, but bottoms out in the primitive hex/`String` wall (Stage 2.3), so it is |
| 123 | +||| taken as a named hypothesis: the live-verification counterpart of |
| 124 | +||| `CollisionResistant` (named, never faked). |
| 125 | +public export |
| 126 | +DecodeInjective : (Hash -> Maybe HashBytes) -> Type |
| 127 | +DecodeInjective dec = (a, b : Hash) -> dec a = dec b -> a = b |
| 128 | + |
| 129 | +||| Lift decode-injectivity over a vector: two `Hash` vectors whose decodings agree |
| 130 | +||| are equal. |
| 131 | +export |
| 132 | +mapDecodeInjective : (dec : Hash -> Maybe HashBytes) -> DecodeInjective dec -> |
| 133 | + {k : Nat} -> (xs, ys : Vect k Hash) -> decAll dec xs = decAll dec ys -> xs = ys |
| 134 | +mapDecodeInjective dec inj [] [] _ = Refl |
| 135 | +mapDecodeInjective dec inj (x :: xs) (y :: ys) eq = |
| 136 | + rewrite inj x y (cong Data.Vect.head eq) in |
| 137 | + cong (\zs => y :: zs) (mapDecodeInjective dec inj xs ys (cong Data.Vect.tail eq)) |
| 138 | + |
| 139 | +||| LIVE root-verification soundness (Mode 2, full): two block-hash vectors that |
| 140 | +||| decode successfully and yield equal Merkle roots are EQUAL - carrying |
| 141 | +||| `rootVerifySound` (HashBytes level) up to the live A2ML `Hash` level across the |
| 142 | +||| decoder bridge (instantiate `dec := hashToBytes`). This is what a redesigned |
| 143 | +||| `verifyRefsHelper` (one root comparison instead of per-ref hash checks) would rest |
| 144 | +||| on. Honest hypotheses: `CollisionResistant h` (Stage 1.4) and `DecodeInjective dec` |
| 145 | +||| (the hex boundary, Stage 2.3). The `decAll dec xs = map Just xb` premises say "xs |
| 146 | +||| decodes to the leaf bytes xb"; the power-of-two layout is the leaf length index. |
| 147 | +export |
| 148 | +merkleRootVerifyHashSound : |
| 149 | + (h : Combiner) -> CollisionResistant h -> |
| 150 | + (dec : Hash -> Maybe HashBytes) -> DecodeInjective dec -> {n : Nat} -> |
| 151 | + (xs, ys : Vect (power 2 n) Hash) -> (xb, yb : Vect (power 2 n) HashBytes) -> |
| 152 | + decAll dec xs = map Just xb -> decAll dec ys = map Just yb -> |
| 153 | + rootHashWith h (buildMerkleTree {n} xb) = rootHashWith h (buildMerkleTree {n} yb) -> |
| 154 | + xs = ys |
| 155 | +merkleRootVerifyHashSound h cr dec inj xs ys xb yb dx dy roots = |
| 156 | + let bytesEq : (xb = yb) |
| 157 | + bytesEq = rootVerifySound h cr xb yb roots |
| 158 | + decsEq : (decAll dec xs = decAll dec ys) |
| 159 | + decsEq = trans dx (trans (cong (map Just) bytesEq) (sym dy)) |
| 160 | + in mapDecodeInjective dec inj xs ys decsEq |
0 commit comments