proof: Stage 3.1 repair correctness + Stage 2.4 verify↔Merkle wiring

.machine_readable/6a2/STATE.a2ml

@@ -7,12 +7,12 @@ 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 provable core complete: validator, verifier, hex)"
+session = "machine-readable checkpoint — 2026-06-18 (Stage 1 complete; Stage 2 core + 2.4 verify↔Merkle wiring; Stage 3.1 pure repair correctness)"
 
 [project-context]
 name = "Ochránce"
 purpose = """Neurosymbolic filesystem verification framework in Idris2 dependent types: a pluggable VerifiedSubsystem interface, A2ML attestation/audit markup, a verified Merkle tree with a combiner-generic soundness theorem, and ECHIDNA integration."""
-completion-percentage = 58
+completion-percentage = 66
 
 [position]
 phase = "implementation"   # design | implementation | testing | maintenance | archived
@@ -30,6 +30,8 @@ theorems = [
   "validateManifestSound (Stage 2.1) — validator soundness: accepted manifest ⇒ supported version, non-empty subsystem, All RefValid refs (Bool-level, Either-pipeline inversion)",
   "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",
   "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",
@@ -57,7 +59,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 (Opus) — repair correctness (L3 linear types). PRECONDITION: repair is a stub; introduce a pure repairPure that genuinely reconstructs the hash map and prove over that (IO↔pure pattern), else the theorem is vacuous",
+  "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 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)",
   "Sync .machine_readable scaffold to rsr-template (ai/, compliance/, configs/, policies/, scripts/, 0.1-AI-MANIFEST, ENSAID_CONFIG, root README, root-allow) — pending template access",
 ]

docs/PROOFS.adoc

@@ -111,6 +111,15 @@ The core is *clean*: all 19 `ochrance-core` modules carry `%default total` (the
 | verifier soundness: `verifyRefsHelper fs refs = Right ()` ⇒ `All (RefMatches fs) refs`
   — every accepted ref names an in-range block whose stored hash equals the ref's
   (four-guard per-ref inversion, Bool-level).
+| `repairBlock{Sets,Preserves,NumBlocks,Idempotent}` (Stage 3.1)
+| 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.
 | `roundtripManifest` + sub-codecs (`algoRT`, `modeRT`, `refsRT`, `mpolRT`, …)
 | grammar invertibility: `decodeManifest (encodeManifest m) = Just m`.
 | `SatisfiesMinimum` / `attestedSatisfiesLax`
@@ -189,10 +198,17 @@ not the nested `isValidHexString`.
   block-present, hash-equal). `Ochrance.Filesystem.VerifyProof`. Machine-checked,
   axiom-free.
 +
-STILL OPEN (architectural, by design): "wired to `merkleCorrect`". The verifier
-compares per-ref hashes and never builds a Merkle tree, so checking against a Merkle
-*root* is a verify-path redesign, not a proof. Deferred to a design decision (would
-let `merkleBinding` carry the no-collision guarantee into verification).
+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.
++
+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.
 
 . *[DONE — 2.3]* Hex codec structural round-trip. The full
   `hexStringToBytes (bytesToHex bs) = Just bs` crosses two primitive walls —
@@ -208,19 +224,30 @@ let `merkleBinding` carry the no-collision guarantee into verification).
 
 === Stage 3 — Repair correctness (L3, linear types)  [model: Opus]
 
-PRECONDITION (surfaced at Compaction 2): `repair` is currently a *stub* —
-`repairBlock` (`Repair.idr`) updates the hash map but does **not** read or write
-block data. Proving `verify (repair s) = Valid` against a no-op would be vacuous or
-false. DECISION (recommended): introduce a pure
-`repairPure : FSState -> Manifest -> FSState` that genuinely reconstructs the hash
-map, prove correctness over *that*, and make the IO `repair` a proven-equivalent
-shell (the IO↔pure pattern). Alternative: leave repair honestly-bounded until real
-block-I/O lands (defers the linear-type theorem).
-
-. `verifyPure (repairPure s m) m = True` — the meaty (now well-founded) theorem.
-. Repair idempotence as a *proof* (today only a property test).
-. Harvest framework's mode-indexed Interface; state the `VerifiedSubsystem` law
-  `verify (repair s m) m = Right …` and prove the FSState instance satisfies it.
+RESOLVED (was PRECONDITION): the pure repair core is now factored out —
+`repairBlockPure : FSState -> BlockIndex -> Hash -> FSState` installs a hash in the
+map, and the IO `repairBlock` is `repairBlockPure` + the range check (IO↔pure
+pattern). Because FSState's verifiable content *is* its hash map (it carries no
+separate block data), this is the genuine repair semantics, so the theorems are
+well-founded, not vacuous.
+
+. *[DONE — 3.1]* Pure repair primitive correctness, machine-checked
+  (`Ochrance.Filesystem.RepairProof`, axiom-free): `repairBlockSets` (the repaired
+  index now holds the new hash), `repairBlockPreserves` (every other index
+  untouched), `repairBlockNumBlocks` (block count preserved), and
+  `repairBlockIdempotent` (repairing the same (index, hash) twice = once) — the
+  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.
+. Harvest framework's mode-indexed Interface; state the `VerifiedSubsystem` law and
+  prove the FSState instance satisfies it.
 +
 WATCH-FOR: may need proof witnesses threaded through the `1`-quantified API —
 possible signature changes to `Repair.idr`.

ochrance-core/Ochrance/Filesystem/Repair.idr

@@ -27,6 +27,19 @@ import Ochrance.FFI.Crypto
 -- Linear Repair Operations
 --------------------------------------------------------------------------------
 
+||| Pure core of a single-block repair: install `expectedHash` at `blockIdx` in the
+||| state's hash map, leaving every other block and the block count untouched. The
+||| filesystem state's verifiable content *is* this hash map (FSState carries no
+||| separate block data), so this is the genuine repair semantics, not a no-op - the
+||| IO `repairBlock` is this plus the range check. Correctness is proved in
+||| `Ochrance.Filesystem.RepairProof`.
+public export
+repairBlockPure : FSState -> BlockIndex -> Hash -> FSState
+repairBlockPure s blockIdx expectedHash =
+  MkFSState s.numBlocks
+            (\idx => if idx == blockIdx then Just expectedHash else s.blockHash idx)
+            s.metadata
+
 ||| Repair a single block in the filesystem.
 ||| Uses linear types to ensure oldState is consumed exactly once.
 |||
@@ -46,20 +59,12 @@ repairBlock oldState blockIdx expectedHash = do
   -- Check if block index is valid
   if blockIdx >= numBlocks
      then pure (Left (QError (InvalidManifestPath ("Block index out of range: " ++ show blockIdx))))
-     else do
-       -- In a real implementation, this would:
-       -- 1. Read the corrupted block
-       -- 2. Attempt to repair from redundancy/parity data
-       -- 3. Verify the repaired block matches expectedHash
-       -- 4. Write the repaired block back to disk
-
-       -- For now, we create a new state with the hash updated
-       let newState = MkFSState
-             numBlocks
-             (\idx => if idx == blockIdx then Just expectedHash else blockHashFunc idx)
-             metadata
-
-       pure (Right newState)
+     else
+       -- The verifiable state is the hash map; repairBlockPure installs the hash.
+       -- (A real backend would also read/repair/write block bytes; FSState models
+       -- only the hashes, so this is the complete pure repair of the modelled state.)
+       pure (Right (repairBlockPure (MkFSState numBlocks blockHashFunc metadata)
+                                    blockIdx expectedHash))
 
 ||| Repair filesystem from a snapshot (linear version).
 ||| Consumes the old state and produces a new state matching the snapshot.

ochrance-core/Ochrance/Filesystem/RepairProof.idr

@@ -0,0 +1,79 @@
+||| SPDX-License-Identifier: MPL-2.0
+|||
+||| Ochrance.Filesystem.RepairProof - Stage 3: pure repair correctness.
+|||
+||| FSState's verifiable content is its hash map (`BlockIndex -> Maybe Hash`); there
+||| is no separate block data. So `repairBlockPure` - which installs a hash at one
+||| index - is the genuine repair semantics (not a no-op against which a theorem
+||| would be vacuous), and these lemmas pin it down:
+|||
+|||   * `repairBlockSets`       - the repaired index now holds exactly the new hash;
+|||   * `repairBlockPreserves`  - every other index is untouched;
+|||   * `repairBlockNumBlocks`  - the block count is unchanged;
+|||   * `repairBlockIdempotent` - repairing the same (index, hash) twice equals once.
+|||
+||| All axiom-free: the index test is `Nat` `==`, whose reflexivity is *structural*
+||| (`eqNatReflTrue`) - unlike the primitive `Hash`/`String` `==`. No `believe_me`,
+||| no `postulate`.
+module Ochrance.Filesystem.RepairProof
+
+import Decidable.Equality
+
+import Ochrance.A2ML.Types
+import Ochrance.Filesystem.Types
+import Ochrance.Filesystem.Repair
+
+%default total
+
+||| `Nat` equality is reflexively `True` - provable because `Eq Nat` is structural
+||| (the wall-free counterpart of the primitive `String`/`Bits8` reflexivity that
+||| the `Hash` comparison would need).
+public export
+eqNatReflTrue : (n : Nat) -> (n == n) = True
+eqNatReflTrue Z     = Refl
+eqNatReflTrue (S k) = eqNatReflTrue k
+
+||| Repair installs the requested hash at the repaired index.
+export
+repairBlockSets : (s : FSState) -> (i : BlockIndex) -> (h : Hash) ->
+                  blockHash (repairBlockPure s i h) i = Just h
+repairBlockSets s i h = rewrite eqNatReflTrue i in Refl
+
+||| Repair leaves every other index untouched.
+export
+repairBlockPreserves : (s : FSState) -> (i : BlockIndex) -> (h : Hash) ->
+                       (j : BlockIndex) -> (j == i) = False ->
+                       blockHash (repairBlockPure s i h) j = blockHash s j
+repairBlockPreserves s i h j neq = rewrite neq in Refl
+
+||| Repair preserves the block count.
+export
+repairBlockNumBlocks : (s : FSState) -> (i : BlockIndex) -> (h : Hash) ->
+                       numBlocks (repairBlockPure s i h) = numBlocks s
+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.
+neqNatFalse : (m, n : Nat) -> Not (m = n) -> (m == n) = False
+neqNatFalse Z     Z     ctra = absurd (ctra Refl)
+neqNatFalse Z     (S _) _    = Refl
+neqNatFalse (S _) Z     _    = Refl
+neqNatFalse (S k) (S l) ctra = neqNatFalse k l (\p => ctra (cong S p))
+
+||| Repair idempotence: repairing the same index with the same hash twice agrees
+||| with doing it once, at every index (extensional equality of the hash maps).
+||| Decided on `j` vs `i`: at `i`, both sides read `Just h` (`repairBlockSets`);
+||| elsewhere, both read the original (`repairBlockPreserves`). Uses `decEq` rather
+||| than a `with` on `j == i` (whose reduct `equalNat` collapses the two `if`s
+||| asymmetrically).
+export
+repairBlockIdempotent : (s : FSState) -> (i : BlockIndex) -> (h : Hash) ->
+  (j : BlockIndex) ->
+  blockHash (repairBlockPure (repairBlockPure s i h) i h) j
+    = blockHash (repairBlockPure s i h) j
+repairBlockIdempotent s i h j = case decEq j i of
+  Yes prf  => rewrite prf in
+              trans (repairBlockSets (repairBlockPure s i h) i h)
+                    (sym (repairBlockSets s i h))
+  No  ctra => repairBlockPreserves (repairBlockPure s i h) i h j (neqNatFalse j i ctra)

ochrance-core/Ochrance/Filesystem/VerifyMerkle.idr

@@ -0,0 +1,55 @@
+||| SPDX-License-Identifier: MPL-2.0
+|||
+||| Ochrance.Filesystem.VerifyMerkle - wiring verification to the Merkle proofs.
+|||
+||| Root-based verification - trusting a single Merkle root instead of checking every
+||| block hash - is sound and complete *exactly* because the root is a FAITHFUL
+||| fingerprint of the leaf vector: two block-hash vectors build trees with equal
+||| roots iff the vectors are equal. The forward (no-collision / binding) direction is
+||| `merkleBindingTree` (Stage 1.4, discharged against `CollisionResistant h`); the
+||| backward direction is congruence. This is the theorem that licenses a verifier to
+||| 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.
+module Ochrance.Filesystem.VerifyMerkle
+
+import Data.Vect
+
+import Ochrance.Filesystem.Merkle
+import Ochrance.Filesystem.MerkleBinding
+
+%default total
+
+||| The Merkle root is a faithful fingerprint of the block-hash vector: equal roots
+||| iff equal leaves. Backward is congruence (same leaves => same root); forward is
+||| binding (`merkleBindingTree` against the typed `CollisionResistant h`). Checking
+||| one root is therefore *equivalent* to checking every block hash - the
+||| justification for root-based verification.
+export
+rootFaithful : (h : Combiner) -> CollisionResistant h -> {n : Nat} ->
+               (xs, ys : Vect (power 2 n) HashBytes) ->
+               ( (rootHashWith h (buildMerkleTree {n} xs) = rootHashWith h (buildMerkleTree {n} ys)) -> xs = ys
+               , (xs = ys) -> (rootHashWith h (buildMerkleTree {n} xs) = rootHashWith h (buildMerkleTree {n} ys))
+               )
+rootFaithful h cr xs ys =
+  ( merkleBindingTree h cr xs ys
+  , \eq => cong (\v => rootHashWith h (buildMerkleTree {n} v)) eq
+  )
+
+||| The verifier's security guarantee, as the forward direction in verification terms:
+||| if the actual blocks build a tree whose root matches the expected (manifest) root,
+||| the actual blocks ARE the expected blocks - no collision can substitute different
+||| data under the same committed root. (First projection of `rootFaithful`.)
+export
+rootVerifySound : (h : Combiner) -> CollisionResistant h -> {n : Nat} ->
+                  (actual, expected : Vect (power 2 n) HashBytes) ->
+                  rootHashWith h (buildMerkleTree {n} actual)
+                    = rootHashWith h (buildMerkleTree {n} expected) ->
+                  actual = expected
+rootVerifySound h cr actual expected = merkleBindingTree h cr actual expected

ochrance.ipkg

@@ -31,7 +31,9 @@ modules = Ochrance.A2ML.Types
         , Ochrance.Filesystem.MerkleBinding
         , Ochrance.Filesystem.Verify
         , Ochrance.Filesystem.VerifyProof
+        , Ochrance.Filesystem.VerifyMerkle
         , Ochrance.Filesystem.Repair
+        , Ochrance.Filesystem.RepairProof
         , Ochrance.FFI.Echidna
 
 opts = "--total"