proof: Stage 4 (honest) — isolate CollisionResistant as the irreducible crypto assumption

.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)",

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).
 

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))

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 =

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