proof: Stage 3.1 repair correctness + Stage 2.4 verify↔Merkle wiring#53
Merged
Conversation
…ence proved)
FSState's verifiable content is its hash map (no separate block data), so the pure
repairBlockPure — installing a hash at one index — is the genuine repair semantics,
not a no-op. Factored it out of the IO repairBlock (IO↔pure pattern: repairBlock =
repairBlockPure + range check), making the correctness theorems well-founded.
RepairProof (axiom-free, machine-checked):
- 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 = once
(the ledger's "idempotence as a proof", delivered).
Index test is Nat == (structural reflexivity eqNatReflTrue / neqNatFalse), so
wall-free — unlike the primitive Hash ==. Idempotence decided via decEq to avoid the
with-on-(==) asymmetric-reduction trap.
NEXT (3.2): whole-manifest repair ⇒ verifyRefsHelper passes — builds on 2.2 + these
lemmas, needs a distinct-in-range ref-name precondition and the isolated
Hash-reflexivity hypothesis (documented).
Verified: idris2 0.8.0, --build (--total), 25/25 modules, axiom-free.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_011z2t8zAxfcCNLJzU7YdpBQ
…ingerprint of the blocks) rootFaithful proves the Merkle root is a faithful fingerprint of the block-hash vector: equal roots <-> equal leaves. The forward direction (no two distinct block-sets share a root) is merkleBindingTree against CollisionResistant h (Stage 1.4); the backward direction is congruence. rootVerifySound is the security reading — a matching committed root implies identical blocks. This is the theorem that licenses root-based verification, carrying Stage 1.4's binding guarantee into the verification use-case. Ochrance.Filesystem.VerifyMerkle. Builds entirely on the secured base — no new walls, no postulate/believe_me. Verified: idris2 0.8.0, --build (--total), 26/26 modules, axiom-free. REMAINING (documented, architectural): connecting this to the live Hash-based verifyRefsHelper (Stage 2.2) needs the hex Hash<->HashBytes conversion (Stage 2.3, bounded by unpack/pack + Bits8) and a power-of-two leaf layout — a verify-path change, not a proof. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_011z2t8zAxfcCNLJzU7YdpBQ
hyperpolymath
changed the title
hyperpolymath
marked this pull request as ready for review
June 18, 2026 07:02
hyperpolymath
pushed a commit
that referenced
this pull request
Jun 18, 2026
… proof + live Hash bridge) Rounds out the verify↔Merkle wiring to all three modes (generic→granular): - inclusionVerifySound — inclusion-proof verification soundness: a generated (leaf, proof) reconstructs the tree's true root (merkleCorrect, Stage 1.1, read as a per-leaf verification guarantee). The propositional reconstruct = root is the wall-free core; the residual root == root Bool step is the documented Bits8 wall. - hashToBytes — the live bridge decoding an A2ML Hash (hex string) to 32 Merkle HashBytes (via the proven Stage 2.3 hex codec); snapshot-root verification composes it with rootVerifySound. Conversion correctness is the hex boundary (2.3-bounded), surfaced as an explicit partial decode, not asserted. (Mode 1, rootFaithful/rootVerifySound, landed in the previous commit / PR #53.) Verified: idris2 0.8.0, --build (--total), 26/26 modules, axiom-free. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_011z2t8zAxfcCNLJzU7YdpBQ
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Repairs, then verify wiring — both machine-checked
Two related capstone pieces, bottom-up. Verified with idris2 0.8.0,
--build(--total): 26/26 modules, axiom-free.Stage 3.1 — pure repair primitive correctness
FSState's verifiable content is its hash map (no separate block data), so installing a hash is the genuine repair — the stub-vacuity precondition is resolved. Factored the pure core out of the IO path (repairBlock=repairBlockPure+ range check), then proved (Ochrance.Filesystem.RepairProof):repairBlockSets— repaired index now holds exactly the new hash.repairBlockPreserves— every other index untouched.repairBlockNumBlocks— block count unchanged.repairBlockIdempotent— repairing the same(index, hash)twice = once. (Delivers the ledger's "idempotence as a proof".)Index test is
Nat==— structurally reflexive (eqNatReflTrue/neqNatFalse), wall-free, unlike the primitiveHash==. Idempotence viadecEq(avoids thewith-on-(==)asymmetric-reduction trap).Stage 2.4 — verify↔Merkle wiring
Ochrance.Filesystem.VerifyMerkle: the Merkle root is a faithful fingerprint of the block-hash vector.rootFaithful— equal roots<->equal leaves. Forward =merkleBindingTree(Stage 1.4, againstCollisionResistant h); backward = congruence.rootVerifySound— security reading: a matching committed root ⇒ identical blocks; no collision substitutes different data under the same root.This is the theorem that licenses root-based verification, carrying Stage 1.4's binding guarantee into the verify use-case — built entirely on the already-secured base, no new walls.
Remaining (documented in
docs/PROOFS.adoc, not faked)repairPure⇒verifyRefsHelperaccepts (distinct-in-range ref-name precondition + isolatedHash-reflexivity hypothesis).rootFaithfulto the liveHash-based verifier needs the hexHash↔HashBytesconversion (2.3-bounded) + a power-of-two leaf layout — a verify-path change.Verification note
The repo's Idris2 CI is a static scan, not a full type-check — verified with a real bootstrapped compiler before pushing.
🤖 Generated with Claude Code