proof: verify↔Merkle modes 2+3 (inclusion-proof verification + live Hash bridge)

.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",

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 —

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