proof(merkle): Stage 1 — buildMerkleTree correctness (WIP)#46
Merged
Conversation
Reusable, total Vect/Fin lemmas underpinning buildMerkleTree correctness: indexAppendLeft, indexAppendRight, indexReplace (transport cancellation), finToNatReplace, splitAtConcat. idris2 0.8.0 --check green. The buildGetLeaf assembly that consumes them is in progress. https://claude.ai/code/session_011z2t8zAxfcCNLJzU7YdpBQ
hyperpolymath
marked this pull request as ready for review
June 15, 2026 17:48
hyperpolymath
added a commit
that referenced
this pull request
Jun 15, 2026
Re-lands the Stage 1.1 proof that PR #46's merge dropped: buildGetLeaf (getLeafHash (buildMerkleTree hs) (finToNat i) = Just (index i hs)), Ochrance.Util.VectLemmas (helpers), Merkle.idr visibility bumps, and ipkg module registration. Total, machine-checked, idris2 0.8.0 build 19/19.
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 — Merkle closure (proof campaign; see
docs/PROOFS.adoc)Proof-first work toward
buildMerkleTreecorrectness:getLeafHash (buildMerkleTree hs) (finToNat i) = Just (index i hs).Landed (this commit): five reusable, total helper lemmas (
ochrance-core/Ochrance/Scratch.idr), allidris2 0.8.0 --checkgreen:indexAppendLeft/indexAppendRight—indexover++viaweakenN/shiftindexReplace— transport cancellation (tamesbuildMerkleTree'sreplaceoverpowerTwoSucc)finToNatReplace— transport preservesfinToNatsplitAtConcat—splitAt's two halves re-append to the originalIn progress: the
buildGetLeafassembly consuming them (induction +splitSum+ the<-Bool /minusbranch bridge), agetLeafHashexport→public exportvisibility bump, and integration intoochrance.ipkgso CI type-checks it.Proof-first discipline: only proven lemmas + a visibility change are added; no code is allowed ahead of its proof. Draft / WIP. Verified locally on idris2 0.8.0 (built from source per #44).
https://claude.ai/code/session_011z2t8zAxfcCNLJzU7YdpBQ
Generated by Claude Code