proof: Stage 3.2 (repair⇒verify) + live-verifier Merkle redesign soundness

.machine_readable/6a2/STATE.a2ml

@@ -7,7 +7,7 @@ project = "ochrance"
 version = "0.1.0"
 last-updated = "2026-06-18"
 status = "active"
-session = "machine-readable checkpoint — 2026-06-18 (Stage 1 complete; Stage 2 core + 2.4 verify↔Merkle wiring; Stage 3.1 pure repair correctness)"
+session = "machine-readable checkpoint — 2026-06-18 (Stage 1 complete; Stage 2 core + 2.4 verify↔Merkle wiring + live root-verify soundness; Stage 3.1 pure repair + 3.2 repair⇒verify)"
 
 [project-context]
 name = "Ochránce"
@@ -31,7 +31,9 @@ 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)",
+  "repairThenVerify (Stage 3.2) — whole-manifest repair ⇒ verify: verifyRefsHelper (repairRefsPure s refs) refs = Right (). Lemma A verifyRefsComplete (completeness, converse of 2.2) ∘ Lemma B repairRefsConsistent (install+no-clobber via repairBlockSets/repairRefsPurePreserves). Honest hyps: GoodRefs (distinct in-range names) + hashRefl (primitive Hash == reflexivity)",
   "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",
+  "merkleRootVerifyHashSound (+ mapDecodeInjective) (Stage 2.4 live) — live root-verification soundness at the Hash level: block-hash vectors that decode (decAll dec) + build equal-rooted trees are equal; carries rootVerifySound up across the decoder bridge. The theorem a redesigned root-comparing verifier rests on. Named boundaries: CollisionResistant h (1.4) + DecodeInjective dec (hex wall 2.3); parametric in dec, used at hashToBytes",
   "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",
@@ -59,7 +61,9 @@ issues = [
 actions = [
   "Stage 1 COMPLETE — 1.1 buildGetLeaf, 1.2 rootFoldLaw, 1.3 IO↔pure bridge, 1.4 merkleBinding/CollisionResistant — all machine-checked (idris2 0.8.0, --total)",
   "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). NEXT 3.2: whole-manifest repair ⇒ verifyRefsHelper passes (needs distinct-in-range ref-name precondition + isolated Hash-reflexivity hypothesis)",
+  "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",
   "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)",

docs/PROOFS.adoc

@@ -121,6 +121,20 @@ The core is *clean*: all 19 `ochrance-core` modules carry `%default total` (the
   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.
+| `merkleRootVerifyHashSound` (+ `mapDecodeInjective`) (Stage 2.4 live)
+| live root-verification soundness at the A2ML `Hash` level: two block-hash vectors
+  that decode (`decAll dec`) and build trees with equal roots are equal — carries
+  `rootVerifySound` up across the decoder bridge. The theorem a redesigned
+  root-comparing verifier rests on. Named boundaries: `CollisionResistant h` (1.4),
+  `DecodeInjective dec` (hex wall, 2.3); stated for arbitrary `dec`, used at
+  `hashToBytes`.
+| `repairThenVerify` (+ `verifyRefsComplete`, `repairRefsConsistent`) (Stage 3.2)
+| whole-manifest repair ⇒ verify: `verifyRefsHelper (repairRefsPure s refs) refs =
+  Right ()`. Lemma A `verifyRefsComplete` (completeness — exact converse of 2.2) ∘
+  Lemma B `repairRefsConsistent` (repair installs each ref's hash and protects it from
+  later repairs, via `repairBlockSets` / `repairRefsPurePreserves`). Honest hypotheses:
+  `GoodRefs` (distinct in-range parseable names) and `hashRefl` (primitive `Hash` `==`
+  reflexivity).
 | `roundtripManifest` + sub-codecs (`algoRT`, `modeRT`, `refsRT`, `mpolRT`, …)
 | grammar invertibility: `decodeManifest (encodeManifest m) = Just m`.
 | `SatisfiesMinimum` / `attestedSatisfiesLax`
@@ -208,10 +222,15 @@ 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): 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.
+SOUNDNESS PROVEN (`merkleRootVerifyHashSound`): replacing the live `Hash`-based
+`verifyRefsHelper` with a root comparison is now *sound* at the `Hash` level - two
+block-hash vectors that decode and yield equal Merkle roots are equal - carrying
+`rootVerifySound` up across the decoder bridge (`mapDecodeInjective`). Two named
+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 — 2.3]* Hex codec structural round-trip. The full
   `hexStringToBytes (bytesToHex bs) = Just bs` crosses two primitive walls —
@@ -242,13 +261,16 @@ well-founded, not vacuous.
   ledger's "idempotence as a proof", delivered. The index test is `Nat` `==`
   (structural — `eqNatReflTrue` / `neqNatFalse`), so wall-free, unlike the primitive
   `Hash` `==`.
-. *[3.2 — next]* Whole-manifest repair ⇒ verify:
-  `verifyRefsHelper (repairPure s m) m.refs = Right ()`. Builds on 2.2's
-  `verifyRefsHelper` and the 3.1 lemmas, but needs (a) a precondition that ref names
-  parse to *distinct* in-range indices (so the rebuilt map is per-ref consistent),
-  and (b) the isolated `Hash`-reflexivity hypothesis `(h == h) = True` — the same
-  primitive `==` wall as `merkleCorrect`'s residual step — named explicitly, never
-  faked.
+. *[DONE — 3.2]* Whole-manifest repair ⇒ verify:
+  `verifyRefsHelper (repairRefsPure s refs) refs = Right ()`
+  (`Ochrance.Filesystem.RepairVerify`, `repairThenVerify`). Composes 2.2's verifier
+  with the 3.1 lemmas via completeness (`verifyRefsComplete`, the converse of
+  `verifyRefsSound`) ∘ repair-consistency (`repairRefsConsistent`). The two needed
+  boundaries are named, not faked: precondition `GoodRefs` (ref names parse to
+  *distinct* in-range indices — else a later repair clobbers an earlier ref's block,
+  consumed in the no-clobber lemma `repairRefsPurePreserves`), and the isolated
+  `Hash`-reflexivity hypothesis `hashRefl : (h == h) = True` (the primitive `==` wall,
+  as in `merkleCorrect`'s residual step). Machine-checked, totality-clean.
 . Harvest framework's mode-indexed Interface; state the `VerifiedSubsystem` law and
   prove the FSState instance satisfies it.
 +

ochrance-core/Ochrance/Filesystem/RepairProof.idr

@@ -55,6 +55,7 @@ repairBlockNumBlocks s i h = Refl
 ||| `Nat` inequality reflects as `== = False` (structural counterpart of the
 ||| primitive-equality wall). Used to drive `repairBlockPreserves` on the `j /= i`
 ||| branch of idempotence.
+export
 neqNatFalse : (m, n : Nat) -> Not (m = n) -> (m == n) = False
 neqNatFalse Z     Z     ctra = absurd (ctra Refl)
 neqNatFalse Z     (S _) _    = Refl

ochrance-core/Ochrance/Filesystem/RepairVerify.idr

@@ -0,0 +1,185 @@
+||| SPDX-License-Identifier: MPL-2.0
+|||
+||| Ochrance.Filesystem.RepairVerify - Stage 3.2: whole-manifest repair => verify.
+|||
+||| The end-to-end guarantee that ties Stage 2.2 (verifier soundness) to Stage 3.1
+||| (pure repair): after repairing every ref of a manifest, the verifier ACCEPTS
+||| that manifest - `verifyRefsHelper (repairRefsPure s refs) refs = Right ()`.
+|||
+||| `repairRefsPure` folds the 3.1 single-block primitive `repairBlockPure` over the
+||| refs, installing each ref's hash at its parsed index. The proof factors as:
+|||
+|||   * `verifyRefsComplete` (Lemma A) - COMPLETENESS, the exact converse of 2.2's
+|||     `verifyRefsSound`: if every ref matches the state (`All (RefMatches fs)`), the
+|||     verifier accepts. Drives the four guards forward from the witness equalities.
+|||   * `repairRefsConsistent` (Lemma B) - repair ESTABLISHES that match witness for
+|||     every ref, via `repairBlockSets` (the head's index now holds its hash) and
+|||     `repairRefsPurePreserves` (no later repair clobbers it - this is where
+|||     distinctness is consumed).
+|||
+||| Two boundaries are named explicitly, never faked (the house style of
+||| `CollisionResistant` / `HexByteRoundtrip`):
+|||   * `hashRefl : (h : Hash) -> (h == h) = True` - reflexivity of the PRIMITIVE
+|||     `Hash`/`String` `==` (the same wall as `merkleCorrect`'s residual `root==root`
+|||     step; `Nat` reflexivity, by contrast, is structural - `eqNatReflTrue`);
+|||   * `GoodRefs` - the precondition that ref names parse to DISTINCT in-range
+|||     indices. Without distinctness a later repair would overwrite an earlier ref's
+|||     block, so the theorem would be false; it is a genuine hypothesis, not a dodge.
+|||
+||| No `believe_me`, no `assert_total`, no `postulate`.
+module Ochrance.Filesystem.RepairVerify
+
+import Data.List.Quantifiers
+
+import Ochrance.A2ML.Types
+import Ochrance.Framework.Error
+import Ochrance.Filesystem.Types
+import Ochrance.Filesystem.Verify
+import Ochrance.Filesystem.VerifyProof
+import Ochrance.Filesystem.Repair
+import Ochrance.Filesystem.RepairProof
+
+%default total
+
+--------------------------------------------------------------------------------
+-- Pure whole-manifest repair
+--------------------------------------------------------------------------------
+
+||| Repair every ref of a manifest: install each ref's hash at its parsed block
+||| index (refs whose name does not parse are skipped - `GoodRefs` rules that out).
+||| Folds the Stage 3.1 primitive `repairBlockPure`.
+public export
+repairRefsPure : FSState -> List Ref -> FSState
+repairRefsPure s [] = s
+repairRefsPure s (ref :: refs) =
+  case parseBlockIdx ref.name of
+    Nothing  => repairRefsPure s refs
+    Just idx => repairRefsPure (repairBlockPure s idx ref.hash) refs
+
+--------------------------------------------------------------------------------
+-- Precondition: distinct, in-range, parseable ref names
+--------------------------------------------------------------------------------
+
+||| "This ref's name does NOT parse to index `i`." The atom of distinctness.
+public export
+NotParsedAs : BlockIndex -> Ref -> Type
+NotParsedAs i ref = Not (parseBlockIdx ref.name = Just i)
+
+||| Every ref name parses to a distinct, in-range block index. Indexed by the block
+||| count (a `Nat`) rather than the whole state, since repair preserves the count -
+||| so the same `GoodRefs` serves the original and every repaired state.
+public export
+data GoodRefs : Nat -> List Ref -> Type where
+  GoodNil  : GoodRefs nb []
+  GoodCons : {0 ref : Ref} -> {0 refs : List Ref} ->
+             (idx : BlockIndex) ->
+             parseBlockIdx ref.name = Just idx ->
+             (idx >= nb) = False ->
+             All (NotParsedAs idx) refs ->
+             GoodRefs nb refs ->
+             GoodRefs nb (ref :: refs)
+
+--------------------------------------------------------------------------------
+-- Lemma A: completeness (converse of Stage 2.2)
+--------------------------------------------------------------------------------
+
+||| COMPLETENESS: if every ref matches the filesystem state, the verifier accepts.
+||| The exact converse of `verifyRefsSound` - drives the four guards forward from
+||| each ref's `RefMatches` witness (name-parse, range, block-present, hash-equal).
+export
+verifyRefsComplete : (fs : FSState) -> (refs : List Ref) ->
+  All (RefMatches fs) refs -> verifyRefsHelper fs refs = Right ()
+verifyRefsComplete fs []          []                                       = Refl
+verifyRefsComplete fs (ref :: rs) ((idx ** (pi, rng, (h ** (bh, heq)))) :: rest) =
+  rewrite pi  in
+  rewrite rng in
+  rewrite bh  in
+  rewrite heq in
+  verifyRefsComplete fs rs rest
+
+--------------------------------------------------------------------------------
+-- Repair structural lemmas
+--------------------------------------------------------------------------------
+
+||| Whole-manifest repair preserves the block count (folds 3.1's
+||| `repairBlockNumBlocks`).
+export
+repairRefsPureNumBlocks : (s : FSState) -> (refs : List Ref) ->
+  numBlocks (repairRefsPure s refs) = numBlocks s
+repairRefsPureNumBlocks s []          = Refl
+repairRefsPureNumBlocks s (ref :: rs) with (parseBlockIdx ref.name)
+  repairRefsPureNumBlocks s (ref :: rs) | Nothing  = repairRefsPureNumBlocks s rs
+  repairRefsPureNumBlocks s (ref :: rs) | Just idx =
+    repairRefsPureNumBlocks (repairBlockPure s idx ref.hash) rs
+
+||| Repairing a list whose parsed indices all differ from `i` leaves block `i`
+||| untouched - the no-clobber lemma. Folds 3.1's `repairBlockPreserves`; the per-
+||| step inequality comes from `NotParsedAs` via `neqNatFalse`.
+export
+repairRefsPurePreserves : (s : FSState) -> (refs : List Ref) -> (i : BlockIndex) ->
+  All (NotParsedAs i) refs ->
+  blockHash (repairRefsPure s refs) i = blockHash s i
+repairRefsPurePreserves s []          i _                    = Refl
+repairRefsPurePreserves s (ref :: rs) i (notHere :: notRest) with (parseBlockIdx ref.name)
+  repairRefsPurePreserves s (ref :: rs) i (notHere :: notRest) | Nothing  =
+    repairRefsPurePreserves s rs i notRest
+  repairRefsPurePreserves s (ref :: rs) i (notHere :: notRest) | Just j =
+    -- `with` has refined `notHere : Not (Just j = Just i)`
+    let iNotJ : Not (i = j)
+        iNotJ = \p => notHere (cong Just (sym p))
+    in trans (repairRefsPurePreserves (repairBlockPure s j ref.hash) rs i notRest)
+             (repairBlockPreserves s j ref.hash i (neqNatFalse i j iNotJ))
+
+||| Unfold one step of `repairRefsPure` once the head ref's index is known.
+export
+repairRefsUnfold : (s : FSState) -> (ref : Ref) -> (refs : List Ref) ->
+  (idx : BlockIndex) -> parseBlockIdx ref.name = Just idx ->
+  repairRefsPure s (ref :: refs) = repairRefsPure (repairBlockPure s idx ref.hash) refs
+repairRefsUnfold s ref refs idx pi = rewrite pi in Refl
+
+--------------------------------------------------------------------------------
+-- Lemma B: repair establishes the match witness
+--------------------------------------------------------------------------------
+
+||| Repair ESTABLISHES consistency: after `repairRefsPure`, every ref matches the
+||| repaired state. The head's hash is installed (`repairBlockSets`) and protected
+||| from later repairs (`repairRefsPurePreserves`, fed the head's distinctness); the
+||| tail is the induction hypothesis (the repaired state's count equals the
+||| original's, definitionally, so the same `GoodRefs` carries through). The hash
+||| equality of each ref against itself is the named `hashRefl` boundary.
+export
+repairRefsConsistent : (s : FSState) -> (refs : List Ref) ->
+  GoodRefs (numBlocks s) refs ->
+  (hashRefl : (h : Hash) -> (h == h) = True) ->
+  All (RefMatches (repairRefsPure s refs)) refs
+repairRefsConsistent s []          GoodNil                          hashRefl = []
+repairRefsConsistent s (ref :: rs) (GoodCons idx pi rng notI good') hashRefl =
+  let s'     : FSState
+      s'     = repairBlockPure s idx ref.hash
+      bhF    : blockHash (repairRefsPure s' rs) idx = Just ref.hash
+      bhF    = trans (repairRefsPurePreserves s' rs idx notI)
+                     (repairBlockSets s idx ref.hash)
+      rngF   : (idx >= numBlocks (repairRefsPure s' rs)) = False
+      rngF   = rewrite repairRefsPureNumBlocks s' rs in rng
+      headW  : RefMatches (repairRefsPure s' rs) ref
+      headW  = (idx ** (pi, rngF, (ref.hash ** (bhF, hashRefl ref.hash))))
+      tailW  : All (RefMatches (repairRefsPure s' rs)) rs
+      tailW  = repairRefsConsistent s' rs good' hashRefl
+  in rewrite repairRefsUnfold s ref rs idx pi in (headW :: tailW)
+
+--------------------------------------------------------------------------------
+-- Stage 3.2: whole-manifest repair => verify
+--------------------------------------------------------------------------------
+
+||| STAGE 3.2: repairing a manifest's refs makes the verifier accept it. Composes
+||| Lemma B (repair => match witnesses) with Lemma A (witnesses => acceptance).
+||| Honest hypotheses: `GoodRefs` (distinct in-range parseable names) and `hashRefl`
+||| (primitive `Hash` `==` reflexivity).
+export
+repairThenVerify : (s : FSState) -> (refs : List Ref) ->
+  GoodRefs (numBlocks s) refs ->
+  (hashRefl : (h : Hash) -> (h == h) = True) ->
+  verifyRefsHelper (repairRefsPure s refs) refs = Right ()
+repairThenVerify s refs good hashRefl =
+  verifyRefsComplete (repairRefsPure s refs) refs
+    (repairRefsConsistent s refs good hashRefl)