proof: Stage 1.4 (Merkle binding, D2) + Stage 2.1 (validator soundness)#51
Merged
Conversation
…eBinding, discharged not asserted) Decision D2. Introduce the typed hypothesis CollisionResistant h (combiner injectivity) and *discharge* the binding theorem against it — not merely state it. merkleBinding proves foldRoot h xs = foldRoot h ys -> xs = ys (equal Merkle roots force equal leaves); merkleBindingTree lifts that to the built tree's actual root via rootFoldLaw (Stage 1.2). Injectivity of the opaque combiner is lifted through the leaf fold, level by level. CollisionResistant h is the SOLE assumed boundary — no postulate / believe_me / assert_* / holes — discharged for the concrete cryptographic combiner in Stage 4. Everything from the hypothesis through both theorems is machine-checked. New module Ochrance.Filesystem.MerkleBinding; two reusable lemmas (splitAtEta, replaceInj) added to Ochrance.Util.VectLemmas; registered in ochrance.ipkg. Verified: idris2 0.8.0, `idris2 --build ochrance.ipkg` (--total) — 21/21 modules, axiom-free. Ledger (docs/PROOFS.adoc) + STATE.a2ml updated: Stage 1 complete. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_011z2t8zAxfcCNLJzU7YdpBQ
…st is a real witness) A manifest accepted by validateManifest provably satisfies the three structural invariants the validator enforces: supported version, non-empty subsystem, and well-formed-hex ref hashes (All RefValid). validateManifestSound inverts the Either-monad validation pipeline, so ValidManifest is a genuine validity witness, not a mere wrapper. Invariants are stated at the wall-free decision (Bool) level — isVersionSupported v = True, (sub == "") = False, isValidHexString h = True — not inverted into propositional String facts, since String equality is a primitive with no equational theory (the honest, strongest form). New module Ochrance.A2ML.ValidatorProof (validateManifestSound + traverseRefsSound + validRefSound); isVersionSupported / isValidHexString / validateRef exposed as public export so the theorem can name and reduce them. Registered in ochrance.ipkg. Stage 2.2 (verify) and 2.3 (hex) scoped honestly in docs/PROOFS.adoc: both need buried where/private helpers lifted to top-level before they are even stateable, then hit documented primitive walls (Bits8 div/mod, unpack-pack) or an architectural gap (verify never builds a Merkle tree). Not faked. Verified: idris2 0.8.0, `idris2 --build ochrance.ipkg` (--total) — 22/22 modules, axiom-free. 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 01:53
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.
Stage 1.4 — Merkle crypto-binding interface (D2) + Stage 2.1 — Validator soundness
This branch carries two stages of the proof campaign (single shared dev branch). Both are machine-checked with idris2 0.8.0,
idris2 --build ochrance.ipkg(the package sets--total): 22/22 modules, axiom-free.Stage 1.4 — Merkle binding (Decision D2) — completes Stage 1
CollisionResistant h— typed crypto hypothesis = combiner injectivity (h a b = h c d → a=c, b=d).merkleBinding—foldRoot h xs = foldRoot h ys -> xs = ys(equal roots force equal leaves), discharged against the hypothesis, not merely stated.merkleBindingTree— the same for the built tree's real root, viarootFoldLaw(Stage 1.2).VectLemmas:splitAtEta(split surjective-pairing),replaceInj(transport-back). ModuleOchrance.Filesystem.MerkleBinding.CollisionResistant his the sole assumed boundary (nopostulate/believe_me), discharged for the concrete cryptographic combiner in Stage 4. This completes Stage 1 (1.1 → 1.4).Stage 2.1 — Validator soundness
validateManifestSound— a manifest accepted byvalidateManifestprovably satisfies the structural invariants it checks: supported version, non-empty subsystem, and well-formed-hex ref hashes (All RefValid m.refs).ValidManifestis a genuine validity witness, by inverting the Either-monad validation pipeline. ModuleOchrance.A2ML.ValidatorProof.isVersionSupported v = True,(sub == "") = False,isValidHexString h = True) —Stringequality is primitive, so this is the strongest honest statement.Stage 2.2 / 2.3 — scoped honestly (not in this PR)
Documented in
docs/PROOFS.adoc:verifyRefsHelperis awhere-local inside the instance — must be lifted to top-level before it's even stateable; then the ref-match inversion goes through like 2.1. "Wired tomerkleCorrect" is architectural — the verify path never builds a Merkle tree.unpack∘packhas no equational theory; per-byte fact needs primitiveBits8div/mod/*). Bounded, like the production-pipeline round-trip.Verification note
The repo's Idris2 CI (
echidna-validation.yml) is a static scan (dangerous-pattern grep +%default totalpresence), not a fullidris2 --build. Both stages were therefore verified with a real compiler (bootstrapped idris2 0.8.0 from source) before pushing — a green CI here is necessary but not sufficient for a proof change.🤖 Generated with Claude Code