feat: root-comparing verify path + power-of-two leaf layout (VerifyRoot)#56
Merged
Merged
Conversation
…VerifyRoot) The executable plumbing that merkleRootVerifyHashSound licenses: build a Merkle tree from block hashes and compare roots, instead of per-ref hash checks. New module Ochrance.Filesystem.VerifyRoot (all total): - padToLength / nextPow2Exp / layoutLeaves — pad an arbitrary-length block-hash list to a power-of-two leaf Vect (filling with emptyHash). - verifyByRoot — build the padded tree and compare its root to the expected root. - verifyByRootHash — fully live: decode A2ML Hashes via hashToBytes, then root-verify. - fsBlockHashes / verifySnapshotRoot — the runtime path: verify an FSState against an FSSnapshot's committed rootHash. Engineering, not a proof: accept-on-match soundness is the already-proven merkleRootVerifyHashSound (modulo its named CollisionResistant / DecodeInjective boundaries and the primitive ==). Verified: idris2 0.8.0, --build (--total), 28/28 modules, no warnings. 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 11:50
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.
Task 1 — root-comparing verify path + power-of-two leaf layout
The executable plumbing that the proven
merkleRootVerifyHashSoundlicenses: build a Merkle tree from block hashes and compare roots, instead of per-ref hash checks. Verified with idris2 0.8.0,--build(--total): 28/28 modules, no warnings.New module
Ochrance.Filesystem.VerifyRoot(all total)padToLength/nextPow2Exp/layoutLeaves— pad an arbitrary-length block-hash list to a power-of-two leafVect(filling withemptyHash);nextPow2Expis fuel-bounded for totality.verifyByRoot— build the padded tree, compare its root to the expected root (Bool).verifyByRootHash— fully live: decode A2MLHashes viahashToBytes, then root-verify (Maybe Bool).fsBlockHashes/verifySnapshotRoot— the runtime path: verify anFSStateagainst anFSSnapshot's committedrootHash.This is engineering, not a proof: accept-on-match soundness is the already-proven
merkleRootVerifyHashSound(modulo its namedCollisionResistant/DecodeInjectiveboundaries and the primitive==).Note on Task 2 (Stage 4)
Stage 4 ("discharge
CollisionResistant") is paused pending a design decision — full injectivity is unsatisfiable for a compressing combiner (pigeonhole), so it cannot be honestly proven. Raised with the author; not faked here.Verification note
Repo CI is a static scan, not a full type-check — proved with a real bootstrapped compiler before pushing.
🤖 Generated with Claude Code
Generated by Claude Code