From f8393270f2e7cbda1562baf9be05af483f7e67ea Mon Sep 17 00:00:00 2001 From: Claude Date: Thu, 18 Jun 2026 12:03:59 +0000 Subject: [PATCH] =?UTF-8?q?proof(crypto):=20Stage=204=20(honest)=20?= =?UTF-8?q?=E2=80=94=20isolate=20CollisionResistant=20as=20the=20irreducib?= =?UTF-8?q?le=20assumption?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit "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 Claude-Session: https://claude.ai/code/session_011z2t8zAxfcCNLJzU7YdpBQ --- .machine_readable/6a2/STATE.a2ml | 6 +- docs/PROOFS.adoc | 28 +++++--- .../Ochrance/Filesystem/MerkleAssumption.idr | 70 +++++++++++++++++++ .../Ochrance/Filesystem/MerkleBinding.idr | 14 ++-- ochrance.ipkg | 1 + 5 files changed, 104 insertions(+), 15 deletions(-) create mode 100644 ochrance-core/Ochrance/Filesystem/MerkleAssumption.idr diff --git a/.machine_readable/6a2/STATE.a2ml b/.machine_readable/6a2/STATE.a2ml index 774b02a..cd073fb 100644 --- a/.machine_readable/6a2/STATE.a2ml +++ b/.machine_readable/6a2/STATE.a2ml @@ -26,7 +26,8 @@ theorems = [ "buildGetLeaf (Stage 1.1) — buildMerkleTree/getLeafHash round-trip: getLeafHash (buildMerkleTree hs) (finToNat i) = Just (index i hs)", "rootFoldLaw + foldRoot (Stage 1.2) — root characterisation: rootHashWith h (buildMerkleTree hs) = foldRoot h hs (combiner-generic)", "rootHashBytesE_spec / verifyProofE_spec (Stage 1.3) — Either-monad folds compute the pure spec; production …IO_spec conditional on the explicit FFI-reflection hypothesis", - "merkleBinding / merkleBindingTree (Stage 1.4) — binding discharged against the typed CollisionResistant h (combiner injectivity): equal roots ⇒ equal leaves; sole assumption discharged in Stage 4", + "merkleBinding / merkleBindingTree (Stage 1.4) — binding discharged against the typed CollisionResistant h (combiner injectivity): equal roots ⇒ equal leaves; sole assumption, isolated (NOT dischargeable — pigeonhole) in Stage 4", + "constNotCollisionResistant (Stage 4) — the binding hypothesis HAS TEETH: a degenerate combiner provably fails CollisionResistant (Not (CollisionResistant constCombiner)). Full injectivity is pigeonhole-false for any compressing 64→32-byte combiner, so CR is the irreducible cryptographic assumption, never proved (module MerkleAssumption). Inaccurate 'Stage 4 discharges it' wording corrected across MerkleBinding/PROOFS", "validateManifestSound (Stage 2.1) — validator soundness: accepted manifest ⇒ supported version, non-empty subsystem, All RefValid refs (Bool-level, Either-pipeline inversion)", "parsePairsRoundtrip (Stage 2.3) — hex codec structural soundness: parsePairs (bytesToHexChars bs) = Just bs, given isolated per-byte Bits8 hypothesis (pack/unpack wall explicit)", "verifyRefsSound (Stage 2.2) — verifier soundness: verifyRefsHelper fs refs = Right () ⇒ All (RefMatches fs) refs (four-guard per-ref inversion; merkle-root wiring deferred as architectural)", @@ -46,7 +47,7 @@ milestones = [ "Stage 1 — Merkle closure (buildMerkleTree correctness, IO↔pure bridge) + crypto-binding interface (CollisionResistant)", "Stage 2 — Verify + Validator soundness; hex codec round-trip", "Stage 3 — Repair correctness (L3 linear types); harvest framework's mode-indexed Interface", - "Stage 4 — Merkle completeness, binding discharge, progressive monotonicity, write-up", + "Stage 4 — Merkle completeness, binding-assumption ISOLATION (CR is pigeonhole-false, not dischargeable — DONE via constNotCollisionResistant), progressive monotonicity, write-up", ] [blockers-and-issues] @@ -65,6 +66,7 @@ actions = [ "Stage 3.2 DONE — whole-manifest repair ⇒ verify (repairThenVerify, module RepairVerify). repairRefsPure folds repairBlockPure; proof = verifyRefsComplete ∘ repairRefsConsistent; GoodRefs precondition + hashRefl hypothesis, both named", "Live-verifier Merkle redesign SOUNDNESS DONE (merkleRootVerifyHashSound) — root-comparing verifier is sound at the Hash level, modulo named CollisionResistant + DecodeInjective", "Live-verifier PLUMBING DONE (module VerifyRoot) — padToLength/nextPow2Exp/layoutLeaves pad to power-of-2 leaf Vect; verifyByRoot/verifyByRootHash build tree + compare roots; fsBlockHashes/verifySnapshotRoot = runtime path vs FSSnapshot.rootHash. Executable, total; accept-on-match soundness = merkleRootVerifyHashSound", + "Stage 4 DONE (honest isolation) — CollisionResistant cannot be discharged (pigeonhole-false for compressing combiner); isolated as the irreducible crypto assumption + proved it has teeth (constNotCollisionResistant, module MerkleAssumption). Optional follow-on: wire real Zig/FFI combiner + declare CR as its explicit assumption", "Stage 2.4 DONE — verify↔Merkle proof-level wiring (rootFaithful/rootVerifySound): the root is a faithful fingerprint of the blocks (binding). REMAINING: connect to the live Hash-based verifyRefsHelper via hex Hash<->HashBytes conversion (2.3-bounded) + power-of-two layout (verify-path change, not a proof)", "Stage 3.2 (next provable): whole-manifest repairPure ⇒ verifyRefsHelper accepts (distinct-in-range ref-name precondition + isolated Hash-reflexivity hypothesis)", "Remove Idris-side crypto stubs and build + link libochrance.so into the flow (unblocks the crypto-integrity claim)", diff --git a/docs/PROOFS.adoc b/docs/PROOFS.adoc index ab3f005..6849ac7 100644 --- a/docs/PROOFS.adoc +++ b/docs/PROOFS.adoc @@ -52,8 +52,10 @@ Three repositories are in scope. "Verification" means something different in eac | *D2 — Crypto binding as a typed interface* | The security half of the Merkle argument (collision resistance) is modelled as an Idris hypothesis `CollisionResistant h`, and the binding theorem is - discharged against it — not left as prose. Stubbed in Stage 1, discharged in the - final stage. + discharged against it — not left as prose. It is the irreducible cryptographic + trust root (pigeonhole-false for a compressing combiner, so never provable); Stage 4 + isolates it and proves it has teeth (`MerkleAssumption`), rather than faking a + discharge. | *D3 — svalinn: migrate before proving* | Prove where the language is final; migrate-then-prove where it is changing. @@ -98,7 +100,14 @@ The core is *clean*: all 19 `ochrance-core` modules carry `%default total` (the | binding *discharged against* the typed hypothesis `CollisionResistant h` (combiner injectivity): `foldRoot h xs = foldRoot h ys -> xs = ys`, and the built-tree-root corollary. Combiner injectivity lifted through the fold; `CollisionResistant h` the - sole assumption (`MerkleBinding`), discharged for the concrete combiner in Stage 4. + sole assumption (`MerkleBinding`) — the irreducible crypto trust root, isolated (not + dischargeable) in Stage 4 (`MerkleAssumption`). +| `constNotCollisionResistant` (Stage 4) +| the binding hypothesis HAS TEETH: a degenerate combiner (ignores its inputs) provably + fails `CollisionResistant` — `Not (CollisionResistant constCombiner)`. Confirms the + hypothesis is a genuine constraint; full injectivity is pigeonhole-false for any + compressing combiner, so CR is the irreducible cryptographic assumption, never proved + (`MerkleAssumption`). | `validateManifestSound` (Stage 2.1) | validator soundness: `validateManifest m = Right vm` ⇒ supported version, non-empty subsystem, and `All RefValid m.refs` (well-formed-hex hashes). Invariants @@ -173,7 +182,8 @@ design change or a model downshift mid-stage. `merkleBindingTree` the built-tree-root corollary (via `rootFoldLaw`). The proof lifts combiner injectivity through the fold (Stage 1.2 is its prerequisite); `CollisionResistant h` is the *sole* assumed hypothesis — no `postulate` / - `believe_me` — discharged for the concrete combiner in Stage 4. New reusable + `believe_me` — and the irreducible cryptographic trust root (Stage 4 isolates it, + does not discharge it — pigeonhole-false; see `MerkleAssumption`). New reusable lemmas `splitAtEta` / `replaceInj` in `VectLemmas`. `Ochrance.Filesystem.MerkleBinding`. Machine-checked (idris2 0.8.0, `--total`). *This pulls the Stage 4 binding-discharge forward to its hypothesis.* @@ -283,10 +293,12 @@ possible signature changes to `Repair.idr`. === Stage 4 — Completeness, binding discharge, write-up [model: Sonnet; Opus if binding is hard] . Merkle *completeness* (converse of soundness): in-range leaf ⇒ a proof exists. -. *D2 discharge*: the binding argument is *already proven against* - `CollisionResistant h` (Stage 1.4 — `merkleBinding` / `merkleBindingTree`); what - remains is discharging the hypothesis itself for the concrete cryptographic - combiner, or stating it as the explicit, irreducible crypto axiom. +. *[DONE — D2] CR isolated, not discharged*: the binding argument is proven against + `CollisionResistant h` (Stage 1.4). The hypothesis itself CANNOT be discharged — full + injectivity is pigeonhole-false for a compressing combiner — so Stage 4 isolates it + as the irreducible cryptographic trust root and proves it has teeth + (`constNotCollisionResistant`, `MerkleAssumption`). Optional follow-on engineering: + wire the real Zig/FFI combiner in and declare CR as its explicit assumption. . Progressive monotonicity: the remaining `SatisfiesMinimum` cases (all `Refl`). . Final ledger pass; thesis-aligned summary (ICFP/PLDI/SOSP framing). diff --git a/ochrance-core/Ochrance/Filesystem/MerkleAssumption.idr b/ochrance-core/Ochrance/Filesystem/MerkleAssumption.idr new file mode 100644 index 0000000..87b9eda --- /dev/null +++ b/ochrance-core/Ochrance/Filesystem/MerkleAssumption.idr @@ -0,0 +1,70 @@ +||| SPDX-License-Identifier: MPL-2.0 +||| +||| Ochrance.Filesystem.MerkleAssumption - Stage 4 (honest): the collision-resistance +||| assumption, isolated. +||| +||| The binding theorem `merkleBinding` (Stage 1.4) is discharged against the +||| hypothesis `CollisionResistant h` - full pairwise injectivity of the combiner. The +||| roadmap once aimed to *discharge* that hypothesis for the concrete cryptographic +||| combiner in "Stage 4". That is IMPOSSIBLE to do honestly, and this module records +||| why rather than faking it: +||| +||| * A combiner has type `HashBytes -> HashBytes -> HashBytes` - it maps 64 bytes to +||| 32 (it compresses). By the pigeonhole principle two distinct input pairs must +||| share an output - a collision - so `CollisionResistant h` is FALSE for every +||| total combiner. No term of that type exists; constructing one would need +||| `believe_me`/`postulate`, which this codebase forbids. +||| * Real collision resistance is a *computational* statement ("no efficient +||| adversary finds a collision"), not expressible as a pure type-theoretic +||| proposition. So `CollisionResistant h` is the irreducible cryptographic trust +||| root: it stays an explicit hypothesis, threaded through every binding-based +||| result and supplied by the caller at the verification boundary. +||| +||| What we CAN prove - and do here - is that the hypothesis is not vacuous: it has +||| teeth. `constNotCollisionResistant` exhibits a concrete (degenerate) combiner that +||| provably FAILS collision resistance, so the binding theorem genuinely depends on +||| being handed a good combiner. This is the honest content of "Stage 4". +module Ochrance.Filesystem.MerkleAssumption + +import Data.Vect + +import Ochrance.Filesystem.Merkle +import Ochrance.Filesystem.MerkleBinding + +%default total + +||| Two distinguished digests, written as explicit conses so that `head` reduces to a +||| literal `Bits8` (a bare `replicate 32 _` leaves `head` stuck). +public export +zerosH : HashBytes +zerosH = 0 :: replicate 31 0 + +public export +onesH : HashBytes +onesH = 1 :: replicate 31 0 + +||| `True = False` is uninhabited (distinct constructors). +trueNotFalse : Not (True = False) +trueNotFalse Refl impossible + +||| The two digests differ: their first bytes are `0` and `1`. Taking heads turns the +||| assumed `zerosH = onesH` into `(0 : Bits8) = 1`, and `== 0` turns that into the +||| impossible `True = False`. +zerosNotOnes : Not (MerkleAssumption.zerosH = MerkleAssumption.onesH) +zerosNotOnes prf = trueNotFalse (cong (\b => b == 0) (cong Data.Vect.head prf)) + +||| A degenerate combiner that ignores its inputs (always returns `emptyHash`). +public export +constCombiner : Combiner +constCombiner _ _ = emptyHash + +||| THE ASSUMPTION HAS TEETH: a combiner that ignores its inputs provably is NOT +||| collision-resistant - the distinct inputs `zerosH` / `onesH` collide under it. So +||| `merkleBinding`'s hypothesis is a genuine constraint, not vacuously satisfiable; a +||| real (compressing) combiner can only ever *assume* it, never prove it (see the +||| module header). This is the honest content of "Stage 4": isolate the assumption, +||| and show it bites. +export +constNotCollisionResistant : Not (CollisionResistant MerkleAssumption.constCombiner) +constNotCollisionResistant cr = + zerosNotOnes (fst (cr zerosH zerosH onesH zerosH Refl)) diff --git a/ochrance-core/Ochrance/Filesystem/MerkleBinding.idr b/ochrance-core/Ochrance/Filesystem/MerkleBinding.idr index 28884f4..d94ce26 100644 --- a/ochrance-core/Ochrance/Filesystem/MerkleBinding.idr +++ b/ochrance-core/Ochrance/Filesystem/MerkleBinding.idr @@ -9,9 +9,11 @@ ||| Idris hypothesis `CollisionResistant h` (injectivity of the combiner), and the ||| binding theorem `merkleBinding` is *discharged against it*, never asserted. ||| `CollisionResistant h` itself is the sole assumed boundary - no `postulate`, -||| no `believe_me`; it is discharged for the concrete cryptographic combiner in -||| Stage 4. Everything from the hypothesis through `merkleBinding` is fully -||| machine-checked here. +||| no `believe_me`. It is the irreducible cryptographic trust root: full injectivity +||| is pigeonhole-false for a compressing combiner, so it can NEVER be discharged by +||| proof (see `Ochrance.Filesystem.MerkleAssumption`) - it stays an explicit +||| hypothesis, supplied at the verification boundary. Everything from the hypothesis +||| through `merkleBinding` is fully machine-checked here. ||| ||| The proof rides on the root-fold law (Stage 1.2): because the root is a fold ||| over the leaves (`foldRoot`), injectivity of the combiner lifts, level by @@ -34,8 +36,10 @@ import Ochrance.Util.VectLemmas ||| Collision resistance of a combiner, modelled as *injectivity*: equal outputs ||| force equal inputs, pairwise. This is the type-level content of collision ||| resistance - the strongest fact one can name without leaving the model into -||| concrete computation. It is the single assumed hypothesis of the binding -||| theorem; Stage 4 discharges it for the concrete cryptographic combiner. +||| concrete computation. It is the single assumed hypothesis of the binding theorem, +||| and the irreducible cryptographic trust root: full injectivity is pigeonhole-false +||| for a compressing combiner, so it is never dischargeable by proof (see +||| `MerkleAssumption.constNotCollisionResistant`, which shows it has teeth). public export CollisionResistant : Combiner -> Type CollisionResistant h = diff --git a/ochrance.ipkg b/ochrance.ipkg index b82a4a6..c972360 100644 --- a/ochrance.ipkg +++ b/ochrance.ipkg @@ -29,6 +29,7 @@ modules = Ochrance.A2ML.Types , Ochrance.Filesystem.MerkleBuild , Ochrance.Filesystem.MerkleIO , Ochrance.Filesystem.MerkleBinding + , Ochrance.Filesystem.MerkleAssumption , Ochrance.Filesystem.Verify , Ochrance.Filesystem.VerifyProof , Ochrance.Filesystem.VerifyMerkle