proof: Stage 2 core — verifier soundness (2.2) + hex codec soundness (2.3)#52
Merged
Conversation
…verts bytesToHexChars) The full hexStringToBytes (bytesToHex bs) = Just bs crosses two primitive walls — unpack/pack (no equational theory) and per-byte Bits8 div/mod — so it cannot carry a compile-time theorem in full. The honest, axiom-free core is proven instead: parsePairsRoundtrip shows parsePairs (bytesToHexChars bs) = Just bs (parsePairs inverts the builder exactly), GIVEN the isolated per-byte hypothesis HexByteRoundtrip (the Bits8 boundary, named as an explicit hypothesis — the IO<->pure-bridge discipline — never faked). Refactor to make it stateable and reduce cleanly: - lift bytesToHex's where-local toPair to a top-level toHexPair (inlined to [c1,c2]); - add bytesToHexChars (explicit recursion, dodging the non-reducing concatMap Monoid layer — same hazard as traverse_); bytesToHex = pack . bytesToHexChars; - expose parsePairs (public export). Behaviour of bytesToHex is unchanged. New module Ochrance.Util.HexProof. Verified: idris2 0.8.0, --build (--total), 23/23 modules, axiom-free. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_011z2t8zAxfcCNLJzU7YdpBQ
…h the filesystem) verifyRefsSound proves the direction trust needs: if the pure ref-checker accepts a manifest's refs (verifyRefsHelper fs refs = Right ()), then every ref genuinely matches the filesystem state — All (RefMatches fs) refs — i.e. each ref name parses to an in-range block whose pre-computed hash equals the ref's hash. Proved by inverting the four per-ref guards (name-parse, range, block-present, hash-equal); a failure in any short-circuits to Left. To make it stateable, lifted verifyRefsHelper / parseBlockIdx (and splitOn / parseNatHelper) out of the VerifiedSubsystem instance's where-clause to top-level public export functions; the instance now calls them. Behaviour unchanged. Equality facts at the wall-free Bool level (h == ref.hash = True), since Hash/String equality bottoms out in primitives. No believe_me / postulate. DEFERRED (architectural, documented): "wired to merkleCorrect" — the verifier compares per-ref hashes and builds no Merkle tree, so checking against a Merkle root is a verify-path redesign, not a proof. New module Ochrance.Filesystem.VerifyProof. Verified: idris2 0.8.0, --build (--total), 24/24 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 06:12
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 2 — verifier (2.2) + hex codec (2.3) soundness
Continues the proof campaign bottom-up, securing each layer before building up: hex codec → verifier (which rests on it). Both machine-checked with idris2 0.8.0,
idris2 --build ochrance.ipkg(--total): 24/24 modules, axiom-free. This completes the provable core of Stage 2 (2.1 validator landed previously; 2.2 + 2.3 here).Stage 2.3 — hex codec structural soundness (the more fundamental layer)
parsePairsRoundtrip—parsePairs (bytesToHexChars bs) = Just bs:parsePairsinverts the byte→hex builder exactly, given the isolated per-byte hypothesisHexByteRoundtrip(the primitive-Bits8div/modboundary, named explicitly — the IO↔pure-bridge discipline from Stage 1.3 — never faked).bytesToHex'swhere-localtoPair→ top-leveltoHexPair; addedbytesToHexChars(explicit recursion, dodging the non-reducingconcatMapMonoid layer — same hazard astraverse_); exposedparsePairs.bytesToHexbehaviour unchanged. ModuleOchrance.Util.HexProof.unpack∘packwall (no equational theory) is left explicit — theString-level full round-trip would additionally cross it.Stage 2.2 — verifier soundness
verifyRefsSound—verifyRefsHelper fs refs = Right () → All (RefMatches fs) refs: if the pure verifier accepts a manifest's refs, every ref genuinely matches the filesystem (names an in-range block whose stored hash equals the ref's). Proved by inverting the four per-ref guards (name-parse, range, block-present, hash-equal).verifyRefsHelper/parseBlockIdx(+splitOn/parseNatHelper) out of theVerifiedSubsysteminstance'swhere-clause to top-level; the instance now calls them. Behaviour unchanged. ModuleOchrance.Filesystem.VerifyProof.h == ref.hash = True).Deferred (architectural — needs a design decision, not in this PR)
"Wire verify to
merkleCorrect." The current verifier compares per-ref hashes and never builds a Merkle tree, so checking against a Merkle root is a verify-path redesign. Doing it would letmerkleBinding(Stage 1.4) carry the no-collision guarantee into verification. Documented indocs/PROOFS.adoc; happy to take this on if you want the redesign.Verification note
The repo's Idris2 CI is a static scan (dangerous-pattern grep +
%default total), not a full type-check — both proofs were verified with a real compiler (bootstrapped idris2 0.8.0) before pushing.🤖 Generated with Claude Code
Generated by Claude Code