From 1cb3304601415600790aa492458049fa10d4feae Mon Sep 17 00:00:00 2001 From: Claude Date: Thu, 18 Jun 2026 01:08:32 +0000 Subject: [PATCH 1/2] =?UTF-8?q?proof(merkle):=20Stage=201.4=20=E2=80=94=20?= =?UTF-8?q?crypto-binding=20(CollisionResistant=20+=20merkleBinding,=20dis?= =?UTF-8?q?charged=20not=20asserted)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Decision D2. Introduce the typed hypothesis CollisionResistant h (combiner injectivity) and *discharge* the binding theorem against it — not merely state it. merkleBinding proves foldRoot h xs = foldRoot h ys -> xs = ys (equal Merkle roots force equal leaves); merkleBindingTree lifts that to the built tree's actual root via rootFoldLaw (Stage 1.2). Injectivity of the opaque combiner is lifted through the leaf fold, level by level. CollisionResistant h is the SOLE assumed boundary — no postulate / believe_me / assert_* / holes — discharged for the concrete cryptographic combiner in Stage 4. Everything from the hypothesis through both theorems is machine-checked. New module Ochrance.Filesystem.MerkleBinding; two reusable lemmas (splitAtEta, replaceInj) added to Ochrance.Util.VectLemmas; registered in ochrance.ipkg. Verified: idris2 0.8.0, `idris2 --build ochrance.ipkg` (--total) — 21/21 modules, axiom-free. Ledger (docs/PROOFS.adoc) + STATE.a2ml updated: Stage 1 complete. Co-Authored-By: Claude Opus 4.8 Claude-Session: https://claude.ai/code/session_011z2t8zAxfcCNLJzU7YdpBQ --- .machine_readable/6a2/STATE.a2ml | 16 +- docs/PROOFS.adoc | 22 ++- .../Ochrance/Filesystem/MerkleBinding.idr | 151 ++++++++++++++++++ ochrance-core/Ochrance/Util/VectLemmas.idr | 21 ++- ochrance.ipkg | 1 + 5 files changed, 201 insertions(+), 10 deletions(-) create mode 100644 ochrance-core/Ochrance/Filesystem/MerkleBinding.idr diff --git a/.machine_readable/6a2/STATE.a2ml b/.machine_readable/6a2/STATE.a2ml index ef1b1a0..10818be 100644 --- a/.machine_readable/6a2/STATE.a2ml +++ b/.machine_readable/6a2/STATE.a2ml @@ -5,14 +5,14 @@ [metadata] project = "ochrance" version = "0.1.0" -last-updated = "2026-06-05" +last-updated = "2026-06-18" status = "active" -session = "machine-readable checkpoint — 2026-06-05" +session = "machine-readable checkpoint — 2026-06-18 (Stage 1 complete: Merkle closure + crypto-binding interface)" [project-context] name = "Ochránce" purpose = """Neurosymbolic filesystem verification framework in Idris2 dependent types: a pluggable VerifiedSubsystem interface, A2ML attestation/audit markup, a verified Merkle tree with a combiner-generic soundness theorem, and ECHIDNA integration.""" -completion-percentage = 40 +completion-percentage = 48 [position] phase = "implementation" # design | implementation | testing | maintenance | archived @@ -23,10 +23,14 @@ maturity = "experimental" # experimental | alpha | beta | production | lts theorems = [ "merkleCorrect / merkleCorrectWith — inclusion-proof soundness, generic over the hash combiner (XOR & BLAKE3 are instances)", "verifyProofReconstructs(With) — verify ≡ (root == reconstruct leaf prf)", + "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", "roundtripManifest (+ algoRT/modeRT/refsRT/mpolRT codecs) — decodeManifest (encodeManifest m) = Just m", "SatisfiesMinimum / attestedSatisfiesLax — progressive-assurance threshold witness", "ABI Handle / createHandle — So (ptr /= 0) non-null invariant", - "supporting lemmas: reconstructAppendWith, powerTwoSucc, justInj", + "supporting lemmas: reconstructAppendWith, powerTwoSucc, justInj; VectLemmas (indexAppendLeft/Right, indexReplace, finToNatReplace, splitAtConcat, splitAtEta, replaceInj)", ] [route-to-mvp] @@ -48,8 +52,8 @@ issues = [ [critical-next-actions] actions = [ - "Stage 1 (Opus): buildMerkleTree index/root-fold laws; bridge verifyProofIO/rootHashBytesIO to the …With spec", - "Introduce CollisionResistant h + merkleBinding interface (D2)", + "Stage 1 COMPLETE — 1.1 buildGetLeaf, 1.2 rootFoldLaw, 1.3 IO↔pure bridge, 1.4 merkleBinding/CollisionResistant — all machine-checked (idris2 0.8.0, --total)", + "Stage 2 (Opus→Sonnet): Validator soundness; verifyState agrees with the manifest (wired to merkleCorrect); hex codec round-trip (watch the String/Bits8 primitive wall — honest theorem may be propositional-over-decidable)", "Remove Idris-side crypto stubs and build + link libochrance.so into the flow (unblocks the crypto-integrity claim)", "Sync .machine_readable scaffold to rsr-template (ai/, compliance/, configs/, policies/, scripts/, 0.1-AI-MANIFEST, ENSAID_CONFIG, root README, root-allow) — pending template access", ] diff --git a/docs/PROOFS.adoc b/docs/PROOFS.adoc index 9e41a10..b9333ee 100644 --- a/docs/PROOFS.adoc +++ b/docs/PROOFS.adoc @@ -94,6 +94,11 @@ The core is *clean*: all 19 `ochrance-core` modules carry `%default total` (the | `rootHashBytesE_spec` / `verifyProofE_spec` (Stage 1.3) | Either-monad folds compute the pure spec on success; production `…IO_spec` theorems hold conditionally on the explicit FFI-reflection hypothesis (`MerkleIO`). +| `merkleBinding` / `merkleBindingTree` (Stage 1.4) +| 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. | `roundtripManifest` + sub-codecs (`algoRT`, `modeRT`, `refsRT`, `mpolRT`, …) | grammar invertibility: `decodeManifest (encodeManifest m) = Just m`. | `SatisfiesMinimum` / `attestedSatisfiesLax` @@ -126,8 +131,16 @@ design change or a model downshift mid-stage. passed as an explicit `reflect` hypothesis (no `postulate`/`believe_me`); the production theorems `rootHashBytesIO_spec` / `verifyProofIO_spec` hold conditionally on it. `Ochrance.Filesystem.MerkleIO`. -. *[1.4] D2*: introduce `CollisionResistant h` and state `merkleBinding` - (typed hypothesis / interface; discharged in Stage 4). +. *[DONE — 1.4] D2*: `CollisionResistant h` (combiner injectivity) introduced and + `merkleBinding` *discharged against it* — not merely stated. Equal leaf folds + (roots) force equal leaves: `foldRoot h xs = foldRoot h ys -> xs = ys`, with + `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 + 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.* + RESOLVED (was WATCH-FOR): the `replace`-by-`powerTwoSucc` transport in `buildMerkleTree` was discharged *without* reshaping the builder — via the @@ -167,7 +180,10 @@ 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*: prove the binding argument against `CollisionResistant`. +. *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. . 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/MerkleBinding.idr b/ochrance-core/Ochrance/Filesystem/MerkleBinding.idr new file mode 100644 index 0000000..28884f4 --- /dev/null +++ b/ochrance-core/Ochrance/Filesystem/MerkleBinding.idr @@ -0,0 +1,151 @@ +||| SPDX-License-Identifier: MPL-2.0 +||| +||| Ochrance.Filesystem.MerkleBinding - Stage 1.4: the crypto-binding interface. +||| +||| Decision D2. The *security* half of the Merkle argument is binding: the root +||| commits to the leaves, so two leaf vectors with the same root must be the same +||| vector. Computationally this rests on collision resistance of the combiner, +||| which is not a constructive fact - so it is modelled as an explicit, typed +||| 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. +||| +||| 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 +||| level, to injectivity of the whole fold - which is exactly binding. +module Ochrance.Filesystem.MerkleBinding + +import Data.Vect +import Data.Nat + +import Ochrance.Filesystem.Merkle +import Ochrance.Filesystem.MerkleBuild +import Ochrance.Util.VectLemmas + +%default total + +-------------------------------------------------------------------------------- +-- The typed crypto-binding hypothesis (D2) +-------------------------------------------------------------------------------- + +||| 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. +public export +CollisionResistant : Combiner -> Type +CollisionResistant h = + (a, b, c, d : HashBytes) -> h a b = h c d -> (a = c, b = d) + +-------------------------------------------------------------------------------- +-- foldRoot unfolding at a successor height +-------------------------------------------------------------------------------- + +||| `foldRoot` at height `S k`, exposed on an explicit split: when `splitAt` cuts +||| the (transported) leaf vector into `(l, r)`, the fold is exactly +||| `h (foldRoot l) (foldRoot r)`. This is the definitional unfolding of `foldRoot` +||| made usable as an equation to rewrite with (it consumes the *same* split that +||| `rootFoldLaw` does). +foldRootSplitEq : (h : Combiner) -> {k : Nat} -> + (hs : Vect (power 2 (S k)) HashBytes) -> + (l, r : Vect (power 2 k) HashBytes) -> + splitAt (power 2 k) + (replace {p = \w => Vect w HashBytes} (powerTwoSucc k) hs) = (l, r) -> + foldRoot h {n = S k} hs = h (foldRoot h {n = k} l) (foldRoot h {n = k} r) +foldRootSplitEq h hs l r sp + with (splitAt (power 2 k) + (replace {p = \w => Vect w HashBytes} (powerTwoSucc k) hs)) + _ | (l', r') = rewrite cong fst sp in rewrite cong snd sp in Refl + +-------------------------------------------------------------------------------- +-- Binding: equal roots force equal leaves (discharged against CollisionResistant) +-------------------------------------------------------------------------------- + +||| Inductive step on the already-split halves: from injectivity of the combiner +||| (`cr`) applied to the two sub-roots, plus the height-`k` binding IH, conclude +||| both halves coincide. (Mirrors the `*Split` helpers in `MerkleBuild`; the IH +||| is a higher-order argument so the recursion stays structural in the height.) +bindSplit : (h : Combiner) -> CollisionResistant h -> {k : Nat} -> + (l1, r1, l2, r2 : Vect (power 2 k) HashBytes) -> + ((u, v : Vect (power 2 k) HashBytes) -> + foldRoot h {n = k} u = foldRoot h {n = k} v -> u = v) -> + h (foldRoot h {n = k} l1) (foldRoot h {n = k} r1) + = h (foldRoot h {n = k} l2) (foldRoot h {n = k} r2) -> + (l1 = l2, r1 = r2) +bindSplit h cr l1 r1 l2 r2 ih eqRoot = + let (eL, eR) = cr (foldRoot h l1) (foldRoot h r1) + (foldRoot h l2) (foldRoot h r2) eqRoot + in (ih l1 l2 eL, ih r1 r2 eR) + +||| BINDING (Stage 1.4 / D2), discharged against `CollisionResistant h`: two leaf +||| vectors that fold to the same Merkle root are equal. The root therefore +||| *binds* the leaves - the commitment is unequivocal - modulo the single typed +||| hypothesis `cr`, which Stage 4 discharges for the cryptographic combiner. The +||| combiner is otherwise opaque, so this holds at XOR and BLAKE3 alike. +||| +||| Composed with `rootFoldLaw` +||| (`rootHashWith h (buildMerkleTree hs) = foldRoot h hs`), this gives binding for +||| the built tree's actual root for free. +export +merkleBinding : (h : Combiner) -> CollisionResistant h -> {n : Nat} -> + (xs, ys : Vect (power 2 n) HashBytes) -> + foldRoot h {n} xs = foldRoot h {n} ys -> xs = ys +merkleBinding h cr {n = Z} [x] [y] prf = cong (\z => z :: []) prf +merkleBinding h cr {n = S k} xs ys prf = + let eq : (power 2 (S k) = power 2 k + power 2 k) + eq = powerTwoSucc k + xs' : Vect (power 2 k + power 2 k) HashBytes + xs' = replace {p = \w => Vect w HashBytes} eq xs + ys' : Vect (power 2 k + power 2 k) HashBytes + ys' = replace {p = \w => Vect w HashBytes} eq ys + l1 : Vect (power 2 k) HashBytes + l1 = fst (splitAt (power 2 k) xs') + r1 : Vect (power 2 k) HashBytes + r1 = snd (splitAt (power 2 k) xs') + l2 : Vect (power 2 k) HashBytes + l2 = fst (splitAt (power 2 k) ys') + r2 : Vect (power 2 k) HashBytes + r2 = snd (splitAt (power 2 k) ys') + spx : (splitAt (power 2 k) xs' = (l1, r1)) + spx = splitAtEta (power 2 k) xs' + spy : (splitAt (power 2 k) ys' = (l2, r2)) + spy = splitAtEta (power 2 k) ys' + ufx : (foldRoot h {n = S k} xs + = h (foldRoot h {n = k} l1) (foldRoot h {n = k} r1)) + ufx = foldRootSplitEq h xs l1 r1 spx + ufy : (foldRoot h {n = S k} ys + = h (foldRoot h {n = k} l2) (foldRoot h {n = k} r2)) + ufy = foldRootSplitEq h ys l2 r2 spy + eqRoot : (h (foldRoot h {n = k} l1) (foldRoot h {n = k} r1) + = h (foldRoot h {n = k} l2) (foldRoot h {n = k} r2)) + eqRoot = trans (sym ufx) (trans prf ufy) + halves : (l1 = l2, r1 = r2) + halves = bindSplit h cr l1 r1 l2 r2 (merkleBinding h cr {n = k}) eqRoot + catEq : (l1 ++ r1 = l2 ++ r2) + catEq = rewrite fst halves in cong (\z => l2 ++ z) (snd halves) + xs'Cat : (xs' = l1 ++ r1) + xs'Cat = sym (splitAtConcat (power 2 k) xs') + ys'Cat : (ys' = l2 ++ r2) + ys'Cat = sym (splitAtConcat (power 2 k) ys') + transEq : (xs' = ys') + transEq = trans xs'Cat (trans catEq (sym ys'Cat)) + in replaceInj {p = \w => Vect w HashBytes} eq transEq + +||| Binding for the *built tree's* root, as a direct corollary: two leaf vectors +||| whose `buildMerkleTree`s carry the same root are equal. Composes +||| `merkleBinding` with `rootFoldLaw`, which rewrites each tree root to its leaf +||| fold. This is the form a verifier actually holds - "same committed root ⇒ same +||| data" - again modulo only the typed `cr` hypothesis (Stage 4). +export +merkleBindingTree : (h : Combiner) -> CollisionResistant h -> {n : Nat} -> + (xs, ys : Vect (power 2 n) HashBytes) -> + rootHashWith h (buildMerkleTree {n} xs) + = rootHashWith h (buildMerkleTree {n} ys) -> + xs = ys +merkleBindingTree h cr xs ys prf = + merkleBinding h cr xs ys + (trans (sym (rootFoldLaw h xs)) (trans prf (rootFoldLaw h ys))) diff --git a/ochrance-core/Ochrance/Util/VectLemmas.idr b/ochrance-core/Ochrance/Util/VectLemmas.idr index 5e4a613..75da66b 100644 --- a/ochrance-core/Ochrance/Util/VectLemmas.idr +++ b/ochrance-core/Ochrance/Util/VectLemmas.idr @@ -3,7 +3,8 @@ ||| Ochrance.Util.VectLemmas - reusable Vect/Fin lemmas for the Merkle proofs. ||| ||| index-over-append (both halves), transport cancellation for `replace`, -||| finToNat under transport, and the splitAt re-append law. +||| finToNat under transport, the splitAt re-append law, splitAt surjective +||| pairing, and injectivity of `replace`. module Ochrance.Util.VectLemmas import Data.Vect @@ -47,3 +48,21 @@ splitAtConcat : {m : Nat} -> (k : Nat) -> (xs : Vect (k + m) e) -> splitAtConcat Z xs = Refl splitAtConcat (S k) (x :: xs) with (splitAt {m} k xs) proof eq _ | (tk, dr) = cong (x ::) (replace {p = \z => fst z ++ snd z = xs} eq (splitAtConcat k xs)) + +||| Surjective pairing for `splitAt`: it equals the pair of its own projections. +||| Lets a caller name the two halves as `fst`/`snd` of the split and still hand +||| the split *equation* to a lemma that pattern-matches the pair. +public export +splitAtEta : {m : Nat} -> (k : Nat) -> (xs : Vect (k + m) e) -> + splitAt {m} k xs = (fst (splitAt {m} k xs), snd (splitAt {m} k xs)) +splitAtEta k xs with (splitAt {m} k xs) + _ | (l, r) = Refl + +||| `replace` along a (type-level) equality is injective: a transported pair of +||| values is equal only if the originals were. This is the transport-back tool +||| for the Merkle binding proof — having shown two *re-indexed* leaf vectors +||| coincide, it cancels the `powerTwoSucc` transport to conclude the originals do. +public export +replaceInj : {0 p : a -> Type} -> {0 x, y : a} -> (eq : x = y) -> + {v, w : p x} -> replace {p} eq v = replace {p} eq w -> v = w +replaceInj Refl prf = prf diff --git a/ochrance.ipkg b/ochrance.ipkg index a51978c..2243855 100644 --- a/ochrance.ipkg +++ b/ochrance.ipkg @@ -26,6 +26,7 @@ modules = Ochrance.A2ML.Types , Ochrance.Util.VectLemmas , Ochrance.Filesystem.MerkleBuild , Ochrance.Filesystem.MerkleIO + , Ochrance.Filesystem.MerkleBinding , Ochrance.Filesystem.Verify , Ochrance.Filesystem.Repair , Ochrance.FFI.Echidna From fc39988050d434bcbd35bc9dde9f8eafbb964e75 Mon Sep 17 00:00:00 2001 From: Claude Date: Thu, 18 Jun 2026 01:47:16 +0000 Subject: [PATCH 2/2] =?UTF-8?q?proof(validator):=20Stage=202.1=20=E2=80=94?= =?UTF-8?q?=20validateManifest=20soundness=20(ValidManifest=20is=20a=20rea?= =?UTF-8?q?l=20witness)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit A manifest accepted by validateManifest provably satisfies the three structural invariants the validator enforces: supported version, non-empty subsystem, and well-formed-hex ref hashes (All RefValid). validateManifestSound inverts the Either-monad validation pipeline, so ValidManifest is a genuine validity witness, not a mere wrapper. Invariants are stated at the wall-free decision (Bool) level — isVersionSupported v = True, (sub == "") = False, isValidHexString h = True — not inverted into propositional String facts, since String equality is a primitive with no equational theory (the honest, strongest form). New module Ochrance.A2ML.ValidatorProof (validateManifestSound + traverseRefsSound + validRefSound); isVersionSupported / isValidHexString / validateRef exposed as public export so the theorem can name and reduce them. Registered in ochrance.ipkg. Stage 2.2 (verify) and 2.3 (hex) scoped honestly in docs/PROOFS.adoc: both need buried where/private helpers lifted to top-level before they are even stateable, then hit documented primitive walls (Bits8 div/mod, unpack-pack) or an architectural gap (verify never builds a Merkle tree). Not faked. Verified: idris2 0.8.0, `idris2 --build ochrance.ipkg` (--total) — 22/22 modules, axiom-free. Co-Authored-By: Claude Opus 4.8 Claude-Session: https://claude.ai/code/session_011z2t8zAxfcCNLJzU7YdpBQ --- .machine_readable/6a2/STATE.a2ml | 7 +- docs/PROOFS.adoc | 47 +++++++++-- ochrance-core/Ochrance/A2ML/Validator.idr | 3 + .../Ochrance/A2ML/ValidatorProof.idr | 81 +++++++++++++++++++ ochrance.ipkg | 1 + 5 files changed, 129 insertions(+), 10 deletions(-) create mode 100644 ochrance-core/Ochrance/A2ML/ValidatorProof.idr diff --git a/.machine_readable/6a2/STATE.a2ml b/.machine_readable/6a2/STATE.a2ml index 10818be..884db0b 100644 --- a/.machine_readable/6a2/STATE.a2ml +++ b/.machine_readable/6a2/STATE.a2ml @@ -7,12 +7,12 @@ project = "ochrance" version = "0.1.0" last-updated = "2026-06-18" status = "active" -session = "machine-readable checkpoint — 2026-06-18 (Stage 1 complete: Merkle closure + crypto-binding interface)" +session = "machine-readable checkpoint — 2026-06-18 (Stage 1 complete; Stage 2.1 validator soundness done)" [project-context] name = "Ochránce" purpose = """Neurosymbolic filesystem verification framework in Idris2 dependent types: a pluggable VerifiedSubsystem interface, A2ML attestation/audit markup, a verified Merkle tree with a combiner-generic soundness theorem, and ECHIDNA integration.""" -completion-percentage = 48 +completion-percentage = 52 [position] phase = "implementation" # design | implementation | testing | maintenance | archived @@ -27,6 +27,7 @@ theorems = [ "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", + "validateManifestSound (Stage 2.1) — validator soundness: accepted manifest ⇒ supported version, non-empty subsystem, All RefValid refs (Bool-level, Either-pipeline inversion)", "roundtripManifest (+ algoRT/modeRT/refsRT/mpolRT codecs) — decodeManifest (encodeManifest m) = Just m", "SatisfiesMinimum / attestedSatisfiesLax — progressive-assurance threshold witness", "ABI Handle / createHandle — So (ptr /= 0) non-null invariant", @@ -53,7 +54,7 @@ issues = [ [critical-next-actions] actions = [ "Stage 1 COMPLETE — 1.1 buildGetLeaf, 1.2 rootFoldLaw, 1.3 IO↔pure bridge, 1.4 merkleBinding/CollisionResistant — all machine-checked (idris2 0.8.0, --total)", - "Stage 2 (Opus→Sonnet): Validator soundness; verifyState agrees with the manifest (wired to merkleCorrect); hex codec round-trip (watch the String/Bits8 primitive wall — honest theorem may be propositional-over-decidable)", + "Stage 2.1 DONE — validateManifestSound (machine-checked). Stage 2.2 (verify): lift verifyRefsHelper out of the instance where-clause to top-level, then invert; merkle-wiring needs verify to build a tree (architectural). Stage 2.3 (hex): primitive Bits8 + unpack/pack walls — bounded; lift toPair/parsePairs first", "Remove Idris-side crypto stubs and build + link libochrance.so into the flow (unblocks the crypto-integrity claim)", "Sync .machine_readable scaffold to rsr-template (ai/, compliance/, configs/, policies/, scripts/, 0.1-AI-MANIFEST, ENSAID_CONFIG, root README, root-allow) — pending template access", ] diff --git a/docs/PROOFS.adoc b/docs/PROOFS.adoc index b9333ee..c2247b7 100644 --- a/docs/PROOFS.adoc +++ b/docs/PROOFS.adoc @@ -99,6 +99,10 @@ The core is *clean*: all 19 `ochrance-core` modules carry `%default total` (the 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. +| `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 + at the wall-free Bool level; Either-pipeline inversion. | `roundtripManifest` + sub-codecs (`algoRT`, `modeRT`, `refsRT`, `mpolRT`, …) | grammar invertibility: `decodeManifest (encodeManifest m) = Just m`. | `SatisfiesMinimum` / `attestedSatisfiesLax` @@ -149,14 +153,43 @@ in `VectLemmas`. No API change was forced. === Stage 2 — Verify + Validator soundness [model: Opus → Sonnet if mechanical] -. Validator: validated manifest ⇒ structural invariants hold. -. `verifyState` agrees with the manifest, wired to `merkleCorrect`. -. Hex codec: `hexStringToBytes (bytesToHex bs) = Just bs` and the length law. +. *[DONE — 2.1]* Validator soundness: a manifest accepted by `validateManifest` + satisfies the structural invariants it checks — supported version, non-empty + subsystem, and well-formed-hex ref hashes (`All RefValid m.refs`). `ValidManifest` + is therefore a genuine validity witness, proved by inverting the Either-monad + validation pipeline. `validateManifestSound` in `Ochrance.A2ML.ValidatorProof` + (helpers `traverseRefsSound` / `validRefSound`). Machine-checked + (idris2 0.8.0, `--total`), axiom-free. + -WATCH-FOR: `Verify` and `Hex` likely rest on primitive `String`/`Bits8` -comparison — the *same wall* as the lexer round-trip. If so the honest theorem is -propositional-over-decidable (document the boundary; do *not* reach for -`believe_me`). This can shorten Stage 2 and justify a Sonnet downshift. +HONEST FORM (was WATCH-FOR, confirmed): invariants are stated at the *decision +(Bool) level* — `isVersionSupported v = True`, `(sub == "") = False`, +`isValidHexString h = True` — not inverted into propositional `String` facts +(`v = "0.1.0"`, `Not (sub = "")`): `String` equality is primitive, so the Bool +form is the strongest honest statement. Two reduction subtleties recorded for +reuse: (i) `traverse_` for `Either` desugars through `<*>` and `Right () *> y` is +only `map id y` (functor-identity *law*, not definitional) — so invert by casing +on the head outcome *and* the tail fold, keeping each step definitional; (ii) `with` +abstracts only a hypothesis's WHNF, so case on `validateRef ref` (exposed there), +not the nested `isValidHexString`. + +. *[2.2 — prereq refactor]* `verify` agrees with the manifest, wired to + `merkleCorrect`. BLOCKER: `verifyRefsHelper` is a `where`-local inside the + `VerifiedSubsystem` instance method and cannot be named in a theorem — lift it to + a top-level `public export` function first; then the ref-match inversion (success + ⇒ each `blockHash idx = Just h` with `h == ref.hash = True`) goes through like + 2.1. The "wired to `merkleCorrect`" half is *architectural*: the current `verify` + compares ref hashes directly and never builds a Merkle tree, so connecting it to + `merkleCorrect` requires the verify path to construct one (a design change, not a + proof). + +. *[2.3 — bounded]* Hex codec round-trip `hexStringToBytes (bytesToHex bs) = Just bs`. + Primitive-wall-dominated: (a) `unpack (pack xs) = xs` has no equational theory + (the *same wall* as the production lexer round-trip); (b) the per-byte fact rests + on primitive `Bits8` `div`/`mod`/`*`/`+`. The clean content is the List-`Char` + recursion `parsePairs (concatMap toPair bs) = Just bs` *given* an isolated + per-byte hypothesis (the Bits8 boundary, IO↔pure-bridge style) — but + `bytesToHex`'s `toPair` is a `where`-local and `parsePairs` is private, so this + too needs a lift first. Honestly bounded, like the production-pipeline round-trip. === Stage 3 — Repair correctness (L3, linear types) [model: Opus] diff --git a/ochrance-core/Ochrance/A2ML/Validator.idr b/ochrance-core/Ochrance/A2ML/Validator.idr index 668a61f..47cac67 100644 --- a/ochrance-core/Ochrance/A2ML/Validator.idr +++ b/ochrance-core/Ochrance/A2ML/Validator.idr @@ -44,11 +44,13 @@ Show ValidationError where -------------------------------------------------------------------------------- ||| Check if a version string is supported +public export isVersionSupported : String -> Bool isVersionSupported "0.1.0" = True isVersionSupported _ = False ||| Check if a hash value contains only valid hex characters +public export isValidHexString : String -> Bool isValidHexString s = all isHexChar (unpack s) where @@ -56,6 +58,7 @@ isValidHexString s = all isHexChar (unpack s) isHexChar c = isHexDigit c || c == '.' ||| Validate a single reference's hash +public export validateRef : Ref -> Either ValidationError () validateRef ref = if not (isValidHexString ref.hash.value) diff --git a/ochrance-core/Ochrance/A2ML/ValidatorProof.idr b/ochrance-core/Ochrance/A2ML/ValidatorProof.idr new file mode 100644 index 0000000..7bfb9e5 --- /dev/null +++ b/ochrance-core/Ochrance/A2ML/ValidatorProof.idr @@ -0,0 +1,81 @@ +||| SPDX-License-Identifier: MPL-2.0 +||| +||| Ochrance.A2ML.ValidatorProof - Stage 2.1: soundness of validateManifest. +||| +||| A `ValidManifest` is meant to be a *type-level witness* of validity. This +||| module proves it actually is one: every manifest `validateManifest` accepts +||| satisfies the three structural invariants the validator checks - supported +||| version, non-empty subsystem, and well-formed-hex ref hashes. +||| +||| The invariants are stated at the *decision (Bool) level* - `isVersionSupported +||| v = True`, `(sub == "") = False`, `isValidHexString h = True` - rather than +||| inverted into propositional `String` facts (`v = "0.1.0"`, `Not (sub = "")`): +||| `String` equality is a primitive with no equational theory, so the Bool form +||| is the strongest *honest* statement (cf. the documented String/primitive wall +||| in docs/PROOFS.adoc). No `believe_me`, no `postulate`. +module Ochrance.A2ML.ValidatorProof + +import Data.List +import Data.List.Quantifiers + +import Ochrance.A2ML.Types +import Ochrance.A2ML.Validator +import Ochrance.Framework.Error + +%default total + +||| The per-ref invariant a ValidManifest carries: the ref's hash value passed the +||| well-formed-hex check. Wall-free Bool form. +public export +RefValid : Ref -> Type +RefValid ref = isValidHexString ref.hash.value = True + +||| Soundness of the `traverse_ validateRef` phase: if validating every ref +||| succeeded, every ref satisfies `RefValid`. Inverts the Either-applicative fold +||| one element at a time (a `Left` anywhere would have short-circuited the whole). +||| From a successful single-ref validation, recover the wall-free hex invariant. +validRefSound : (ref : Ref) -> validateRef ref = Right () -> + isValidHexString ref.hash.value = True +validRefSound ref vr with (isValidHexString ref.hash.value) + validRefSound ref vr | True = Refl + validRefSound ref vr | False = absurd vr + +||| Soundness of the `traverse_ validateRef` phase: if validating every ref +||| succeeded, every ref satisfies `RefValid`. `traverse_` for `Either` desugars +||| through `<*>` (`Right () *> y` is `map id y`, equal to `y` only by the functor +||| identity *law*, not definitionally), so we case on the head outcome and the +||| tail fold directly: every remaining step (`map g (Left e) = Left e`, +||| `Left e <*> y = Left e`, `Right f <*> Right x = Right (f x)`) is definitional. +traverseRefsSound : (refs : List Ref) -> + the (Either ValidationError ()) (traverse_ Validator.validateRef refs) = Right () -> + All RefValid refs +traverseRefsSound [] _ = [] +traverseRefsSound (ref :: rest) prf with (validateRef ref) proof vrEq + traverseRefsSound (ref :: rest) prf | Left e = absurd prf + traverseRefsSound (ref :: rest) prf | Right () with (traverse_ validateRef rest) proof trEq + traverseRefsSound (ref :: rest) prf | Right () | Left e = absurd prf + traverseRefsSound (ref :: rest) prf | Right () | Right () = + validRefSound ref vrEq :: traverseRefsSound rest trEq + +||| SOUNDNESS (Stage 2.1): a manifest accepted by `validateManifest` satisfies the +||| three structural invariants the validator enforces - supported version, +||| non-empty subsystem, and well-formed ref hashes. `ValidManifest` is therefore a +||| genuine validity witness, not a mere wrapper. +||| +||| Proved by inverting the Either-monad validation pipeline: each guard that could +||| have produced a `Left` is shown to have taken its `Right` branch, since the +||| whole returned `Right`. +export +validateManifestSound : (m : Manifest) -> (vm : ValidManifest) -> + validateManifest m = Right vm -> + ( isVersionSupported m.manifestData.version = True + , (m.manifestData.subsystem == "") = False + , All RefValid m.refs ) +validateManifestSound m vm prf with (isVersionSupported m.manifestData.version) + validateManifestSound m vm prf | False = absurd prf + validateManifestSound m vm prf | True with (m.manifestData.subsystem == "") + validateManifestSound m vm prf | True | True = absurd prf + validateManifestSound m vm prf | True | False with (traverse_ validateRef m.refs) proof trEq + validateManifestSound m vm prf | True | False | Left e = absurd prf + validateManifestSound m vm prf | True | False | Right () = + (Refl, Refl, traverseRefsSound m.refs trEq) diff --git a/ochrance.ipkg b/ochrance.ipkg index 2243855..cd0b7f8 100644 --- a/ochrance.ipkg +++ b/ochrance.ipkg @@ -15,6 +15,7 @@ modules = Ochrance.A2ML.Types , Ochrance.A2ML.Validator , Ochrance.A2ML.Serializer , Ochrance.A2ML.Roundtrip + , Ochrance.A2ML.ValidatorProof , Ochrance.Framework.Interface , Ochrance.Framework.Proof , Ochrance.Framework.Error