diff --git a/.machine_readable/6a2/STATE.a2ml b/.machine_readable/6a2/STATE.a2ml index 1cc912e..a8d57aa 100644 --- a/.machine_readable/6a2/STATE.a2ml +++ b/.machine_readable/6a2/STATE.a2ml @@ -31,7 +31,7 @@ theorems = [ "parsePairsRoundtrip (Stage 2.3) — hex codec structural soundness: parsePairs (bytesToHexChars bs) = Just bs, given isolated per-byte Bits8 hypothesis (pack/unpack wall explicit)", "verifyRefsSound (Stage 2.2) — verifier soundness: verifyRefsHelper fs refs = Right () ⇒ All (RefMatches fs) refs (four-guard per-ref inversion; merkle-root wiring deferred as architectural)", "repairBlock{Sets,Preserves,NumBlocks,Idempotent} (Stage 3.1) — pure repair primitive correctness over repairBlockPure: installs hash at index, preserves others + count, idempotent (wall-free Nat == via eqNatReflTrue/neqNatFalse)", - "rootFaithful / rootVerifySound (Stage 2.4) — verify↔Merkle wiring: Merkle root is a faithful fingerprint of the block-hash vector (equal roots <-> equal leaves; forward = merkleBindingTree, backward = cong). Licenses root-based verification", + "rootFaithful / rootVerifySound / inclusionVerifySound / hashToBytes (Stage 2.4) — verify↔Merkle wiring, 3 modes generic→granular: root-equivalence (faithful fingerprint via merkleBindingTree), inclusion-proof (merkleCorrect per-leaf), live Hash↔HashBytes bridge for snapshot-root", "roundtripManifest (+ algoRT/modeRT/refsRT/mpolRT codecs) — decodeManifest (encodeManifest m) = Just m", "SatisfiesMinimum / attestedSatisfiesLax — progressive-assurance threshold witness", "ABI Handle / createHandle — So (ptr /= 0) non-null invariant", diff --git a/docs/PROOFS.adoc b/docs/PROOFS.adoc index fcf5cec..cd0978a 100644 --- a/docs/PROOFS.adoc +++ b/docs/PROOFS.adoc @@ -115,11 +115,12 @@ The core is *clean*: all 19 `ochrance-core` modules carry `%default total` (the | pure repair primitive correctness over `repairBlockPure`: installs the hash at the index, preserves other indices and the count, idempotent. Wall-free (`Nat` structural `==`: `eqNatReflTrue` / `neqNatFalse`). -| `rootFaithful` / `rootVerifySound` (Stage 2.4) -| verify↔Merkle wiring: the Merkle root is a faithful fingerprint of the block-hash - vector — equal roots `<->` equal leaves (forward = `merkleBindingTree`; backward = - congruence). Licenses root-based verification; binding (1.4) carried into the verify - use-case. +| `rootFaithful` / `rootVerifySound` / `inclusionVerifySound` / `hashToBytes` (Stage 2.4) +| verify↔Merkle wiring, three modes (generic→granular): root-equivalence (faithful + fingerprint, equal roots `<->` equal leaves, via `merkleBindingTree`); + inclusion-proof verification (`merkleCorrect` as a per-leaf guarantee); and the live + `Hash`↔`HashBytes` decode bridge for snapshot-root verification. Binding (1.4) and + inclusion soundness (1.1) carried into the verify use-case. | `roundtripManifest` + sub-codecs (`algoRT`, `modeRT`, `refsRT`, `mpolRT`, …) | grammar invertibility: `decodeManifest (encodeManifest m) = Just m`. | `SatisfiesMinimum` / `attestedSatisfiesLax` @@ -198,17 +199,19 @@ not the nested `isValidHexString`. block-present, hash-equal). `Ochrance.Filesystem.VerifyProof`. Machine-checked, axiom-free. + -PARTLY WIRED (Stage 2.4): the *proof-level* wiring is done - -`Ochrance.Filesystem.VerifyMerkle` proves the root is a FAITHFUL fingerprint of the -block-hash vector: `rootFaithful` gives equal roots `<->` equal leaves (forward = -`merkleBindingTree` / `CollisionResistant h`; backward = congruence), and -`rootVerifySound` is the security reading - matching committed root ⇒ identical -blocks. This is the theorem that *licenses* root-based verification, carrying Stage -1.4's binding guarantee into the verification use-case. +WIRED (Stage 2.4), three modes generic→granular in `Ochrance.Filesystem.VerifyMerkle`: +(1) *root-equivalence* — `rootFaithful` proves the root is a FAITHFUL fingerprint +(equal roots `<->` equal leaves; forward = `merkleBindingTree` / `CollisionResistant +h`, backward = congruence) and `rootVerifySound` is the security reading (matching +committed root ⇒ identical blocks); (2) *inclusion-proof* — `inclusionVerifySound` +re-exposes `merkleCorrect` (1.1) as a per-leaf verification guarantee; (3) *live +bridge* — `hashToBytes` decodes A2ML `Hash` → Merkle `HashBytes` for snapshot-root +verification, composing with `rootVerifySound`. + -STILL OPEN (architectural): connecting that to the *live* `Hash`-based -`verifyRefsHelper` needs the hex `Hash` <-> `HashBytes` conversion (Stage 2.3, -bounded) and a power-of-two leaf layout - a verify-path change, not a proof. +STILL OPEN (architectural): fully *replacing* the live `Hash`-based +`verifyRefsHelper` with a tree build needs `hashToBytes`' correctness (Stage 2.3, +bounded by the `unpack`/`pack` + `Bits8` walls) and a power-of-two leaf layout - a +verify-path change, not a proof. . *[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/VerifyMerkle.idr b/ochrance-core/Ochrance/Filesystem/VerifyMerkle.idr index 5556dbb..dd28a00 100644 --- a/ochrance-core/Ochrance/Filesystem/VerifyMerkle.idr +++ b/ochrance-core/Ochrance/Filesystem/VerifyMerkle.idr @@ -11,16 +11,25 @@ ||| trust a root, and it carries Stage 1.4's binding guarantee into the verification ||| use-case. ||| -||| NOTE (remaining bridge): this connects the proven Merkle layer (`HashBytes` -||| leaves) to the verification use-case. Connecting it the rest of the way to the -||| *live* A2ML-`Hash`-based verifier (`verifyRefsHelper`, Stage 2.2) additionally -||| needs the hex `Hash` <-> `HashBytes` conversion (Stage 2.3, bounded by the -||| `unpack`/`pack` + `Bits8` walls) and a power-of-two leaf layout - a verify-path -||| change, documented in docs/PROOFS.adoc, not faked here. +||| Three verification modes are surfaced, generic -> granular: +||| * `rootFaithful` / `rootVerifySound` - root-equivalence (one root check stands +||| in for every block hash; backed by `merkleBindingTree`, Stage 1.4); +||| * `inclusionVerifySound` - inclusion-proof verification (per-leaf `(leaf, proof)` +||| reconstructs the root; backed by `merkleCorrect`, Stage 1.1); +||| * `hashToBytes` - the live `Hash` <-> `HashBytes` bridge for snapshot-root +||| verification, composing with `rootVerifySound`. +||| +||| NOTE (remaining): fully replacing the *live* A2ML-`Hash`-based verifier +||| (`verifyRefsHelper`, Stage 2.2) with a tree build needs the hex conversion +||| correctness (Stage 2.3, bounded by the `unpack`/`pack` + `Bits8` walls) and a +||| power-of-two leaf layout - a verify-path change, documented in docs/PROOFS.adoc, +||| not faked here. module Ochrance.Filesystem.VerifyMerkle import Data.Vect +import Ochrance.A2ML.Types +import Ochrance.Util.Hex import Ochrance.Filesystem.Merkle import Ochrance.Filesystem.MerkleBinding @@ -53,3 +62,37 @@ rootVerifySound : (h : Combiner) -> CollisionResistant h -> {n : Nat} -> = rootHashWith h (buildMerkleTree {n} expected) -> actual = expected rootVerifySound h cr actual expected = merkleBindingTree h cr actual expected + +-------------------------------------------------------------------------------- +-- Mode 3 (granular): inclusion-proof verification +-------------------------------------------------------------------------------- + +||| GRANULAR (inclusion-proof) verification soundness: for an in-range leaf, the +||| inclusion proof produced by `generateProof` reconstructs the tree's true root. +||| So a verifier presented with `(leaf, proof)` and checking it against the root +||| accepts exactly the genuine data at that position - this is `merkleCorrect` +||| (Stage 1.1) read as a verification guarantee. (The propositional `reconstruct = +||| root` is the wall-free core; the residual `root == root` Bool step in the +||| `verifyProof` API is the documented primitive-`Bits8` boundary.) +export +inclusionVerifySound : {n : Nat} -> (t : MerkleTree n) -> (i : Nat) -> + (leaf : HashBytes) -> (prf : MerkleProof) -> + getLeafHash t i = Just leaf -> generateProof t i = Just prf -> + reconstruct leaf prf = rootHashBytes t +inclusionVerifySound t i leaf prf gl gp = merkleCorrect t i leaf prf gl gp + +-------------------------------------------------------------------------------- +-- Mode 2 (live bridge): A2ML Hash <-> Merkle HashBytes +-------------------------------------------------------------------------------- + +||| The bridge between the `Hash`-typed manifest/snapshot world (hex string + algo) +||| and the `HashBytes`-typed Merkle proofs: decode a hash's 32 raw bytes. Partial - +||| `Nothing` on malformed/short hex. Snapshot-root verification composes this with +||| `rootVerifySound`: convert the leaves and the committed `FSSnapshot.rootHash`, +||| build the tree, compare roots, and binding gives "same root ⇒ same blocks". The +||| conversion's *correctness* is the hex boundary (Stage 2.3, `parsePairsRoundtrip` +||| modulo the per-byte `Bits8` + `unpack`/`pack` walls), so it is surfaced as this +||| explicit decode rather than asserted. +public export +hashToBytes : Hash -> Maybe HashBytes +hashToBytes h = hexStringToVect 32 h.value