hyperpolymath · hyperpolymath · Jun 18, 2026 · Jun 18, 2026 · Jun 18, 2026
@@ -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; Stage 2.1 validator soundness done)"
+session = "machine-readable checkpoint — 2026-06-18 (Stage 1 complete; Stage 2 provable core complete: validator, verifier, hex)"
 
 [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 = 52
+completion-percentage = 58
 
 [position]
 phase = "implementation"   # design | implementation | testing | maintenance | archived
@@ -28,6 +28,8 @@ theorems = [
   "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)",
+  "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)",
   "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",
@@ -54,7 +56,8 @@ 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.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",
+  "Stage 2 provable core COMPLETE — 2.1 validateManifestSound, 2.2 verifyRefsSound, 2.3 parsePairsRoundtrip; all machine-checked. DEFERRED (architectural decision): wire verify to merkleCorrect — the verify path builds no Merkle tree today",
+  "Stage 3 (Opus) — repair correctness (L3 linear types). PRECONDITION: repair is a stub; introduce a pure repairPure that genuinely reconstructs the hash map and prove over that (IO↔pure pattern), else the theorem is vacuous",
   "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",
 ]

@@ -103,6 +103,14 @@ The core is *clean*: all 19 `ochrance-core` modules carry `%default total` (the
 | 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.
+| `parsePairsRoundtrip` (Stage 2.3)
+| hex codec structural soundness: `parsePairs (bytesToHexChars bs) = Just bs`, given
+  the isolated per-byte `Bits8` hypothesis `HexByteRoundtrip` (`String` pack/unpack
+  wall left explicit).
+| `verifyRefsSound` (Stage 2.2)
+| verifier soundness: `verifyRefsHelper fs refs = Right ()` ⇒ `All (RefMatches fs) refs`
+  — every accepted ref names an in-range block whose stored hash equals the ref's
+  (four-guard per-ref inversion, Bool-level).
 | `roundtripManifest` + sub-codecs (`algoRT`, `modeRT`, `refsRT`, `mpolRT`, …)
 | grammar invertibility: `decodeManifest (encodeManifest m) = Just m`.
 | `SatisfiesMinimum` / `attestedSatisfiesLax`
@@ -172,24 +180,31 @@ on the head outcome *and* the tail fold, keeping each step definitional; (ii) `w
 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.
+. *[DONE — 2.2 (inversion); merkle-wiring deferred]* `verify` soundness. Lifted
+  `verifyRefsHelper` / `parseBlockIdx` out of the instance `where` to top-level
+  `public export`, then proved `verifyRefsSound`:
+  `verifyRefsHelper fs refs = Right () -> All (RefMatches fs) refs` — acceptance ⇒
+  every ref names an in-range block whose stored hash equals the ref's (Bool-level
+  `h == ref.hash = True`), by inverting the four per-ref guards (name-parse, range,
+  block-present, hash-equal). `Ochrance.Filesystem.VerifyProof`. Machine-checked,
+  axiom-free.
++
+STILL OPEN (architectural, by design): "wired to `merkleCorrect`". The verifier
+compares per-ref hashes and never builds a Merkle tree, so checking against a Merkle
+*root* is a verify-path redesign, not a proof. Deferred to a design decision (would
+let `merkleBinding` carry the no-collision guarantee into verification).
+
+. *[DONE — 2.3]* Hex codec structural round-trip. The full
+  `hexStringToBytes (bytesToHex bs) = Just bs` crosses two primitive walls —
+  `unpack∘pack` (no equational theory; the lexer-round-trip wall) and per-byte
+  `Bits8` `div`/`mod`. The honest, axiom-free *core* is now proven:
+  `parsePairsRoundtrip` shows `parsePairs (bytesToHexChars bs) = Just bs` —
+  `parsePairs` inverts `bytesToHexChars` exactly — *given* the isolated per-byte
+  hypothesis `HexByteRoundtrip` (the `Bits8` boundary, named not faked,
+  IO↔pure-bridge style). Required lifting `toPair`→`toHexPair` and `bytesToHexChars`
+  to top-level (the builder recurses explicitly, dodging the non-reducing
+  `concatMap` Monoid layer — same hazard as `traverse_`) and exposing `parsePairs`.
+  `Ochrance.Util.HexProof`. Machine-checked.
 
 === Stage 3 — Repair correctness (L3, linear types)  [model: Opus]
 

@@ -191,6 +191,56 @@ verify fs validManifest = do
     head' [] = Nothing
     head' (x :: _) = Just x
 
+--------------------------------------------------------------------------------
+-- Pure ref-checking (top-level so it can be reasoned about; see VerifyProof)
+--------------------------------------------------------------------------------
+
+||| Split a string on a separator character.
+splitOn : Char -> String -> List String
+splitOn sep s = splitHelper (unpack s) [] []
+  where
+    splitHelper : List Char -> List Char -> List String -> List String
+    splitHelper [] acc res = reverse (pack (reverse acc) :: res)
+    splitHelper (c :: cs) acc res =
+      if c == sep
+         then splitHelper cs [] (pack (reverse acc) :: res)
+         else splitHelper cs (c :: acc) res
+
+||| Parse a string of digits to a Nat.
+parseNatHelper : String -> Maybe Nat
+parseNatHelper s = case all isDigit (unpack s) of
+  False => Nothing
+  True => Just (cast s)
+
+||| Parse a "block_N" ref name to its block index.
+public export
+parseBlockIdx : String -> Maybe BlockIndex
+parseBlockIdx name =
+  let parts = filter (\str => str /= "") (splitOn '_' name) in
+  case parts of
+    ["block", numStr] => parseNatHelper numStr
+    _ => Nothing
+
+||| Check every manifest ref against the filesystem's pre-computed block hashes:
+||| each ref name must parse to an in-range block index whose stored hash equals
+||| the ref's hash. `Right ()` iff all refs match. (`VerifyProof.verifyRefsSound`
+||| inverts this to the per-ref match witness.)
+public export
+verifyRefsHelper : FSState -> List Ref -> Either OchranceError ()
+verifyRefsHelper _ [] = Right ()
+verifyRefsHelper st (ref :: refs) =
+  case parseBlockIdx ref.name of
+    Nothing => Left (QError (InvalidManifestPath ("Invalid ref name: " ++ ref.name)))
+    Just idx =>
+      if idx >= st.numBlocks
+         then Left (QError (InvalidManifestPath ("Block index out of range: " ++ show idx)))
+         else case st.blockHash idx of
+           Nothing => Left (ZError (FileNotFound ("Block " ++ show idx)))
+           Just actualHash =>
+             if actualHash == ref.hash
+                then verifyRefsHelper st refs
+                else Left (PError (HashMismatch ref.name (show ref.hash) (show actualHash)))
+
 --------------------------------------------------------------------------------
 -- VerifiedSubsystem Instance
 --------------------------------------------------------------------------------
@@ -239,43 +289,6 @@ implementation VerifiedSubsystem FSState where
       head' [] = Nothing
       head' (x :: _) = Just x
 
-      splitOn : Char -> String -> List String
-      splitOn sep s = splitHelper (unpack s) [] []
-        where
-          splitHelper : List Char -> List Char -> List String -> List String
-          splitHelper [] acc res = reverse (pack (reverse acc) :: res)
-          splitHelper (c :: cs) acc res =
-            if c == sep
-               then splitHelper cs [] (pack (reverse acc) :: res)
-               else splitHelper cs (c :: acc) res
-
-      parseNatHelper : String -> Maybe Nat
-      parseNatHelper s = case all isDigit (unpack s) of
-        False => Nothing
-        True => Just (cast s)
-
-      parseBlockIdx : String -> Maybe BlockIndex
-      parseBlockIdx name =
-        let parts = filter (\str => str /= "") (splitOn '_' name) in
-        case parts of
-          ["block", numStr] => parseNatHelper numStr
-          _ => Nothing
-
-      verifyRefsHelper : FSState -> List Ref -> Either OchranceError ()
-      verifyRefsHelper _ [] = Right ()
-      verifyRefsHelper st (ref :: refs) =
-        case parseBlockIdx ref.name of
-          Nothing => Left (QError (InvalidManifestPath ("Invalid ref name: " ++ ref.name)))
-          Just idx =>
-            if idx >= st.numBlocks
-               then Left (QError (InvalidManifestPath ("Block index out of range: " ++ show idx)))
-               else case st.blockHash idx of
-                 Nothing => Left (ZError (FileNotFound ("Block " ++ show idx)))
-                 Just actualHash =>
-                   if actualHash == ref.hash
-                      then verifyRefsHelper st refs
-                      else Left (PError (HashMismatch ref.name (show ref.hash) (show actualHash)))
-
   -- Repair implementation: delegates to linearRepairFromManifest
   repair = \fs, manifest => do
     result <- linearRepairFromManifest fs manifest

@@ -0,0 +1,60 @@
+||| SPDX-License-Identifier: MPL-2.0
+|||
+||| Ochrance.Filesystem.VerifyProof - Stage 2.2: soundness of ref-checking.
+|||
+||| The pure verifier `verifyRefsHelper` (the core of the FSState
+||| `VerifiedSubsystem.verify`) accepts a manifest's refs only if every ref names an
+||| in-range block whose pre-computed hash equals the ref's hash. This module proves
+||| the direction trust depends on: *acceptance is sound* - if `verifyRefsHelper`
+||| returns `Right ()`, then every ref genuinely matches the filesystem state
+||| (`All (RefMatches fs)`). Proved by inverting the verifier's four guards
+||| (name-parse, range, block-present, hash-equal) per ref - a failure in any one
+||| would have short-circuited to `Left`.
+|||
+||| Equality facts are stated at the wall-free Bool level (`h == ref.hash = True`),
+||| since `Hash`/`String` equality bottoms out in primitives. No `believe_me`,
+||| no `postulate`.
+|||
+||| SCOPE: this is soundness of the *current* hash-comparison verifier. Wiring it to
+||| `merkleCorrect` (checking against a Merkle root rather than per-ref hashes) is a
+||| separate architectural step - the verify path does not build a tree today.
+module Ochrance.Filesystem.VerifyProof
+
+import Data.List
+import Data.List.Quantifiers
+
+import Ochrance.A2ML.Types
+import Ochrance.Framework.Error
+import Ochrance.Filesystem.Types
+import Ochrance.Filesystem.Verify
+
+%default total
+
+||| What it means for one ref to match the filesystem: its name parses to a block
+||| index, in range, whose stored hash equals the ref's hash (Bool form).
+public export
+RefMatches : FSState -> Ref -> Type
+RefMatches fs ref =
+  ( idx : BlockIndex
+  ** ( parseBlockIdx ref.name = Just idx
+     , (idx >= fs.numBlocks) = False
+     , ( h : Hash ** (fs.blockHash idx = Just h, (h == ref.hash) = True) )
+     ) )
+
+||| SOUNDNESS (Stage 2.2): if the pure verifier accepts all refs, every ref matches
+||| the filesystem state. Inverts the four guards per ref (each guard's failure path
+||| is a `Left`, contradicting the `Right ()` hypothesis).
+export
+verifyRefsSound : (fs : FSState) -> (refs : List Ref) ->
+                  verifyRefsHelper fs refs = Right () -> All (RefMatches fs) refs
+verifyRefsSound fs []            _   = []
+verifyRefsSound fs (ref :: refs) prf with (parseBlockIdx ref.name) proof pbi
+  verifyRefsSound fs (ref :: refs) prf | Nothing  = absurd prf
+  verifyRefsSound fs (ref :: refs) prf | Just idx with (idx >= fs.numBlocks) proof geq
+    verifyRefsSound fs (ref :: refs) prf | Just idx | True  = absurd prf
+    verifyRefsSound fs (ref :: refs) prf | Just idx | False with (fs.blockHash idx) proof bh
+      verifyRefsSound fs (ref :: refs) prf | Just idx | False | Nothing  = absurd prf
+      verifyRefsSound fs (ref :: refs) prf | Just idx | False | Just h with (h == ref.hash) proof heq
+        verifyRefsSound fs (ref :: refs) prf | Just idx | False | Just h | False = absurd prf
+        verifyRefsSound fs (ref :: refs) prf | Just idx | False | Just h | True  =
+          (idx ** (pbi, geq, (h ** (bh, heq)))) :: verifyRefsSound fs refs prf
@@ -43,6 +43,7 @@ hexPairToByte hi lo = do
 --------------------------------------------------------------------------------
 
 ||| Parse pairs of characters from a list
+public export
 parsePairs : List Char -> Maybe (List Bits8)
 parsePairs [] = Just []
 parsePairs [_] = Nothing  -- Odd number of chars
@@ -93,13 +94,25 @@ byteToHexPair b =
       lo = b `mod` 16
   in (nibbleToHexChar hi, nibbleToHexChar lo)
 
+||| The two hex characters of a single byte, as a list. Top-level (not a
+||| `where`-local) and inlined to `[c1, c2]` so it reduces definitionally - this
+||| is what `HexProof` reasons about.
+public export
+toHexPair : Bits8 -> List Char
+toHexPair b = [nibbleToHexChar (b `div` 16), nibbleToHexChar (b `mod` 16)]
+
+||| Bytes to hex characters, by explicit structural recursion (rather than
+||| `concatMap`, whose Foldable/Monoid layer does not reduce definitionally - the
+||| same hazard as `traverse_`). This is the round-trip partner of `parsePairs`.
+public export
+bytesToHexChars : List Bits8 -> List Char
+bytesToHexChars []        = []
+bytesToHexChars (b :: bs) = toHexPair b ++ bytesToHexChars bs
+
 ||| Convert bytes to hex string
 export
 bytesToHex : List Bits8 -> String
-bytesToHex bytes = pack $ concatMap toPair bytes
-  where
-    toPair : Bits8 -> List Char
-    toPair b = let (hi, lo) = byteToHexPair b in [hi, lo]
+bytesToHex bytes = pack (bytesToHexChars bytes)
 
 ||| Convert a vector of bytes to hex string
 export

@@ -0,0 +1,43 @@
+||| SPDX-License-Identifier: MPL-2.0
+|||
+||| Ochrance.Util.HexProof - Stage 2.3: structural soundness of the hex codec.
+|||
+||| The full round-trip `hexStringToBytes (bytesToHex bs) = Just bs` cannot carry a
+||| compile-time theorem: it threads through `pack`/`unpack` (primitives with no
+||| equational theory - the same wall as the production lexer round-trip) and, per
+||| byte, through primitive `Bits8` `div`/`mod`/`*`/`+`. What IS provable, axiom-free,
+||| is the *structural* core at the `List Char` level - that `parsePairs` inverts
+||| `bytesToHexChars` exactly, GIVEN the one irreducible per-byte fact: that a byte's
+||| two hex characters parse back to it. That per-byte fact (the `Bits8` boundary) is
+||| isolated as an explicit hypothesis `HexByteRoundtrip`, never assumed silently -
+||| the IO<->pure-bridge discipline of Stage 1.3. No `believe_me`, no `postulate`.
+module Ochrance.Util.HexProof
+
+import Data.List
+import Ochrance.Util.Hex
+
+%default total
+
+||| The isolated primitive-`Bits8` boundary: a byte's two hex characters parse back
+||| to the byte. Discharging it needs the `Bits8` div/mod + nibble round-trip, which
+||| rests on primitive machine arithmetic with no equational theory - so it is named
+||| as an explicit hypothesis here rather than faked. (A concrete combiner would
+||| discharge it by 256-way computation, outside the type theory.)
+public export
+HexByteRoundtrip : Type
+HexByteRoundtrip =
+  (b : Bits8) ->
+  hexPairToByte (nibbleToHexChar (b `div` 16)) (nibbleToHexChar (b `mod` 16)) = Just b
+
+||| STRUCTURAL SOUNDNESS (Stage 2.3): `parsePairs` inverts `bytesToHexChars` exactly,
+||| given the per-byte boundary `hyp`. The list recursion is fully machine-checked;
+||| only the `Bits8` per-byte step is assumed (and isolated in `hyp`). This is the
+||| honest core of `hexStringToBytes (bytesToHex bs) = Just bs`, modulo the
+||| `pack`/`unpack` primitive wall that the `String` form would additionally cross.
+export
+parsePairsRoundtrip : (hyp : HexByteRoundtrip) -> (bs : List Bits8) ->
+                      parsePairs (bytesToHexChars bs) = Just bs
+parsePairsRoundtrip hyp []          = Refl
+parsePairsRoundtrip hyp (b :: rest) =
+  rewrite hyp b in
+  rewrite parsePairsRoundtrip hyp rest in Refl
@@ -22,13 +22,15 @@ modules = Ochrance.A2ML.Types
         , Ochrance.Framework.Progressive
         , Ochrance.FFI.Crypto
         , Ochrance.Util.Hex
+        , Ochrance.Util.HexProof
         , Ochrance.Filesystem.Types
         , Ochrance.Filesystem.Merkle
         , Ochrance.Util.VectLemmas
         , Ochrance.Filesystem.MerkleBuild
         , Ochrance.Filesystem.MerkleIO
         , Ochrance.Filesystem.MerkleBinding
         , Ochrance.Filesystem.Verify
+        , Ochrance.Filesystem.VerifyProof
         , Ochrance.Filesystem.Repair
         , Ochrance.FFI.Echidna