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

[hyperpolymath]

This is the full auto-run: Part A (Stage 3.2, clean proof) and Part B (the architectural live-verifier redesign — its soundness, proven). Verified with idris2 0.8.0, --build (--total): 27/27 modules, no warnings, axiom-free. (Repo CI is a static scan, not a full type-check — proved with a real bootstrapped compiler before pushing.)

---

Part A — Stage 3.2: whole-manifest repair ⇒ verify

Ties 2.2 (verifier soundness) to 3.1 (pure repair): after repairing every ref, the verifier accepts.

repairThenVerify : (s : FSState) -> (refs : List Ref) ->
  GoodRefs (numBlocks s) refs -> (hashRefl : (h : Hash) -> (h == h) = True) ->
  verifyRefsHelper (repairRefsPure s refs) refs = Right ()

New module Ochrance.Filesystem.RepairVerify:

• repairRefsPure — pure whole-manifest repair; folds 3.1's repairBlockPure.
• verifyRefsComplete (Lemma A) — completeness, exact converse of verifyRefsSound.
• repairRefsConsistent (Lemma B) — repair installs each ref's hash (repairBlockSets) and protects it from later repairs (repairRefsPurePreserves, the no-clobber lemma where distinctness is consumed).
• repairThenVerify = Lemma B ∘ Lemma A.

Named boundaries: GoodRefs (distinct in-range names — else a later repair clobbers an earlier ref, so the theorem would be false) and hashRefl (primitive Hash == reflexivity, same wall as merkleCorrect's residual step).

---

Part B — live-verifier Merkle redesign (soundness)

Proves the theorem a redesigned root-comparing verifyRefsHelper rests on: two block-hash vectors that decode and build trees with equal Merkle roots are equal — carrying rootVerifySound up to the live A2ML Hash level across the decoder bridge.

merkleRootVerifyHashSound :
  (h : Combiner) -> CollisionResistant h ->
  (dec : Hash -> Maybe HashBytes) -> DecodeInjective dec -> {n : Nat} ->
  (xs, ys : Vect (power 2 n) Hash) -> (xb, yb : Vect (power 2 n) HashBytes) ->
  decAll dec xs = map Just xb -> decAll dec ys = map Just yb ->
  rootHashWith h (buildMerkleTree {n} xb) = rootHashWith h (buildMerkleTree {n} yb) ->
  xs = ys

Added to Ochrance.Filesystem.VerifyMerkle: decAll (structural decode), DecodeInjective (named hypothesis — the live counterpart of CollisionResistant), mapDecodeInjective, and the theorem. Stated for an arbitrary decoder dec (as rootVerifySound is for an arbitrary Combiner), instantiated at hashToBytes.

What's left is plumbing, not a proof: padding an arbitrary-length block list to a power-of-two leaf Vect and switching the runtime verify path over.

---

Campaign status after this PR

Proven bottom-up, each layer machine-checked: 1.1/1.4 Merkle (correct + binding) · 2.1 validator · 2.2 verifier · 2.3 hex · 2.4 verify↔Merkle (3 modes + live root soundness) · 3.1 repair · 3.2 repair⇒verify. Remaining: the layout plumbing above, and Stage 4 (discharge CollisionResistant against the real combiner).

🤖 Generated with Claude Code