proof: verify↔Merkle modes 2+3 (inclusion-proof verification + live Hash bridge)#54
Merged
Merged
Conversation
… 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
hyperpolymath
marked this pull request as ready for review
June 18, 2026 07:06
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.
Verify↔Merkle wiring — modes 2 & 3 (completes all three)
Rounds out the verify↔Merkle wiring you asked for ("all three, generic→granular"). Mode 1 (root-equivalence:
rootFaithful/rootVerifySound) landed onmainvia #53; this adds the remaining two. Verified with idris2 0.8.0,--build(--total): 26/26 modules, axiom-free.Mode 3 (granular) — inclusion-proof verification
inclusionVerifySound— for an in-range leaf, the inclusion proof fromgenerateProofreconstructs the tree's true root, so a verifier checking(leaf, proof)against the root accepts exactly the genuine data at that position. This ismerkleCorrect(Stage 1.1) read as a per-leaf verification guarantee. The propositionalreconstruct = rootis the wall-free core; the residualroot == rootBool step in theverifyProofAPI is the documented primitive-Bits8boundary.Mode 2 (live bridge) — A2ML
Hash↔ MerkleHashByteshashToBytes— decodes an A2ML hexHashto 32 raw Merkle bytes (via the proven Stage 2.3 codec). Snapshot-root verification composes it withrootVerifySound: convert the leaves andFSSnapshot.rootHash, build the tree, compare roots, and binding gives "same root ⇒ same blocks." Partial (Nothingon malformed hex); its correctness is the hex boundary (2.3-bounded), so it's surfaced as an explicit decode, not asserted.The three modes, together (
Ochrance.Filesystem.VerifyMerkle)rootFaithful/rootVerifySoundmerkleBindingTree(1.4)inclusionVerifySoundmerkleCorrect(1.1)hashToBytes(+rootVerifySound)Still open (documented, architectural)
Fully replacing the live
Hash-basedverifyRefsHelperwith a tree build needshashToBytes' correctness (2.3, bounded byunpack/pack+Bits8) and a power-of-two leaf layout — a verify-path change, not a proof.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
Generated by Claude Code