proof: Stage 1.4 (Merkle binding, D2) + Stage 2.1 (validator soundness)

.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; 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 = 40
+completion-percentage = 52
 
 [position]
 phase = "implementation"   # design | implementation | testing | maintenance | archived
@@ -23,10 +23,15 @@ 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",
+  "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",
-  "supporting lemmas: reconstructAppendWith, powerTwoSucc, justInj",
+  "supporting lemmas: reconstructAppendWith, powerTwoSucc, justInj; VectLemmas (indexAppendLeft/Right, indexReplace, finToNatReplace, splitAtConcat, splitAtEta, replaceInj)",
 ]
 
 [route-to-mvp]
@@ -48,8 +53,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.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",
 ]

docs/PROOFS.adoc

@@ -94,6 +94,15 @@ 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.
+| `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`
@@ -126,8 +135,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
@@ -136,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]
 
@@ -167,7 +213,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).
 

ochrance-core/Ochrance/A2ML/Validator.idr

@@ -44,18 +44,21 @@ 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
     isHexChar : Char -> Bool
     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)

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)