proof: Stage 4 (honest) — isolate CollisionResistant as the irreducible crypto assumption#57
Merged
Merged
Conversation
…rreducible assumption
"Discharging" CollisionResistant for the real combiner is impossible: it is full
pairwise injectivity of a HashBytes->HashBytes->HashBytes function (64 bytes -> 32),
which the pigeonhole principle makes FALSE for every total combiner. Constructing a
term of that type would require believe_me/postulate, which this codebase forbids.
Real collision resistance is computational ("no efficient adversary finds a
collision"), not expressible as a pure type-theoretic proposition.
So Stage 4, honestly: isolate CR as the irreducible cryptographic trust root, and
PROVE it is not vacuous — it has teeth.
New module Ochrance.Filesystem.MerkleAssumption:
- constCombiner — a degenerate combiner that ignores its inputs.
- constNotCollisionResistant : Not (CollisionResistant constCombiner) — distinct
inputs collide under it, so it provably fails CR. Confirms merkleBinding's
hypothesis is a genuine constraint, satisfied only by a good combiner (and a real
compressing combiner can only ever assume it).
Also corrects the inaccurate "Stage 4 discharges it for the concrete combiner"
wording in MerkleBinding (module doc + CR doc-comment), PROOFS.adoc, and STATE.a2ml
to "isolated as the irreducible assumption (pigeonhole-false)".
Verified: idris2 0.8.0, --build (--total), 29/29 modules, no warnings, 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 12:08
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 4 (honest) — isolate
CollisionResistantas the irreducible assumptionYou chose honest isolation. "Discharging"
CollisionResistantfor the real combiner is impossible, and this PR records why instead of faking it. Verified with idris2 0.8.0,--build(--total): 29/29 modules, no warnings, axiom-free.Why it can't be discharged
CollisionResistant his full pairwise injectivity of a combinerHashBytes -> HashBytes -> HashBytes— i.e. 64 bytes → 32 bytes. By pigeonhole, two distinct input pairs must collide, soCollisionResistant his false for every total combiner. Constructing a term of that type would requirebelieve_me/postulate(forbidden here). Real collision resistance is computational ("no efficient adversary finds a collision"), which isn't a pure type-theoretic proposition. So CR is the irreducible cryptographic trust root — it stays an explicit hypothesis, supplied at the verification boundary.What this PR proves — the hypothesis has teeth
New module
Ochrance.Filesystem.MerkleAssumption:constCombiner— a degenerate combiner that ignores its inputs.constNotCollisionResistant : Not (CollisionResistant constCombiner)— distinct inputs (zerosH/onesH) collide under it, so it provably fails CR.This confirms
merkleBinding's hypothesis is a genuine constraint (not vacuously satisfiable) — binding really does require a good combiner, and a real compressing one can only ever assume CR.Wording corrected
The inaccurate "Stage 4 discharges it for the concrete combiner" claim is fixed in
MerkleBinding(module doc + theCollisionResistantdoc-comment),docs/PROOFS.adoc, andSTATE.a2ml→ "isolated as the irreducible assumption (pigeonhole-false)".Optional follow-on (not in scope)
Wire the real Zig/FFI combiner in and declare CR as its explicit, documented assumption (touches the FFI stubs CLAUDE.md flags as pending).
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