proof(merkle): Stage 1.3 — IO↔pure bridge (proven Either-monad mirror + thin FFI assumption)

docs/PROOFS.adoc

@@ -91,6 +91,9 @@ The core is *clean*: all 19 `ochrance-core` modules carry `%default total` (the
   `indexReplace`, `finToNatReplace`, `splitAtConcat`.
 | `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 on success; production `…IO_spec`
+  theorems hold conditionally on the explicit FFI-reflection hypothesis (`MerkleIO`).
 | `roundtripManifest` + sub-codecs (`algoRT`, `modeRT`, `refsRT`, `mpolRT`, …)
 | grammar invertibility: `decodeManifest (encodeManifest m) = Just m`.
 | `SatisfiesMinimum` / `attestedSatisfiesLax`
@@ -115,10 +118,14 @@ design change or a model downshift mid-stage.
   (`rootFoldLaw` + `foldRoot` in `Ochrance.Filesystem.MerkleBuild`) — the root is a
   deterministic, representation-independent fold over the leaves. Combiner-generic;
   prerequisite of the binding argument. Machine-checked, axiom-free.
-. *[1.3] IO↔pure bridge*: prove `verifyProofIO` / `rootHashBytesIO` compute the
-  `…With (hashPairBlake3 …)` spec modulo the `Either` allocation-failure plumbing,
-  against a typed combiner-equality hypothesis — connecting the proven theorem to
-  the *production* crypto path. (The estate-wide spine; see "The IO↔pure bridge".)
+. *[DONE — 1.3]* IO↔pure bridge (decompose): the pure `Either`-monad mirrors
+  `rootHashBytesE` / `verifyProofE` provably compute the spec — `rootHashBytesE_spec`:
+  `= Right (rootHashWith h t)`, `verifyProofE_spec`: `= Right (verifyProofWith h …)`
+  when `cf` models `h` — fully machine-checked ("modulo the Either plumbing"). The
+  opaque-IO step (IO fold = `pure` of its pure mirror) is the *sole* assumed boundary,
+  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).
 +
@@ -225,8 +232,8 @@ transports to `F` by `rewrite`. Never optimise unproven code (nothing guards it)
 
 | root combiner
 | real BLAKE3 in IO (vs. abstract `h`)
-| the Stage 1.3 bridge lemma
-| after 1.3
+| `rootHashBytesIO_spec` / `verifyProofIO_spec` (given the FFI-reflection hypothesis)
+| unlocked (Stage 1.3)
 
 | A2ML production parser
 | any fast String parser

ochrance-core/Ochrance/Filesystem/MerkleIO.idr

@@ -0,0 +1,122 @@
+||| SPDX-License-Identifier: MPL-2.0
+|||
+||| Ochrance.Filesystem.MerkleIO - Stage 1.3: the IO<->pure bridge.
+|||
+||| The production crypto path (`rootHashBytesIO` / `verifyProofIO`) runs in IO
+||| and returns `Either OchranceError` to absorb BLAKE3 buffer-allocation
+||| failure. IO is opaque, so we *decompose* the bridge:
+|||
+|||   * a pure `Either`-monad mirror of each fold (`rootHashBytesE` /
+|||     `verifyProofE`) whose agreement with the proven pure spec
+|||     (`rootHashWith` / `verifyProofWith`) is fully machine-checked - this is
+|||     the "modulo the Either allocation-failure plumbing" content; and
+|||   * the one assumed, undischargeable step (IO is opaque): that the IO fold
+|||     equals `pure` of its pure mirror. This is supplied as an *explicit
+|||     hypothesis argument* (`reflect`), never a `postulate`/`believe_me`, so the
+|||     production-soundness results are stated honestly *conditionally* on it.
+module Ochrance.Filesystem.MerkleIO
+
+import Data.Vect
+import Ochrance.Framework.Error
+import Ochrance.Filesystem.Merkle
+
+%default total
+
+||| A pure combiner that may fail: the error-monad model of `hashPairBlake3`,
+||| whose `Left` is the BLAKE3 buffer-allocation failure (z/out-of-memory).
+public export
+CombinerE : Type
+CombinerE = HashBytes -> HashBytes -> Either OchranceError HashBytes
+
+--------------------------------------------------------------------------------
+-- Pure error-monad mirrors of the IO folds
+--------------------------------------------------------------------------------
+
+||| Pure `Either`-monad mirror of `rootHashBytesIO`: the same control flow, with
+||| a pure failing combiner `cf` in place of the IO `hashPairBlake3`.
+public export
+rootHashBytesE : CombinerE -> MerkleTree n -> Either OchranceError HashBytes
+rootHashBytesE cf (Leaf x)   = Right x
+rootHashBytesE cf (Node l r) =
+  case rootHashBytesE cf l of
+    Left err    => Left err
+    Right lHash => case rootHashBytesE cf r of
+      Left err    => Left err
+      Right rHash => cf lHash rHash
+
+||| Pure `Either`-monad mirror of `verifyProofIO`.
+public export
+verifyProofE : CombinerE -> (root, leaf : HashBytes) -> MerkleProof -> Either OchranceError Bool
+verifyProofE cf root leaf [] = Right (root == leaf)
+verifyProofE cf root leaf ((GoLeft,  sib) :: rest) =
+  case cf leaf sib of
+    Left err     => Left err
+    Right parent => verifyProofE cf root parent rest
+verifyProofE cf root leaf ((GoRight, sib) :: rest) =
+  case cf sib leaf of
+    Left err     => Left err
+    Right parent => verifyProofE cf root parent rest
+
+--------------------------------------------------------------------------------
+-- Pure bridge (machine-checked): the error-monad fold computes the spec
+--------------------------------------------------------------------------------
+
+||| If `cf` models a pure combiner `h` with no failure (`cf a b = Right (h a b)`),
+||| the error-monad root fold returns exactly the proven pure root. This is the
+||| machine-checked half of the bridge.
+export
+rootHashBytesE_spec : (h : Combiner) -> (cf : CombinerE) ->
+  (model : (a, b : HashBytes) -> cf a b = Right (h a b)) ->
+  (t : MerkleTree n) ->
+  rootHashBytesE cf t = Right (rootHashWith h t)
+rootHashBytesE_spec h cf model (Leaf x)   = Refl
+rootHashBytesE_spec h cf model (Node l r) =
+  rewrite rootHashBytesE_spec h cf model l in
+  rewrite rootHashBytesE_spec h cf model r in
+  model (rootHashWith h l) (rootHashWith h r)
+
+||| Likewise for proof verification: the error-monad check computes the proven
+||| pure Bool verdict when `cf` models `h`.
+export
+verifyProofE_spec : (h : Combiner) -> (cf : CombinerE) ->
+  (model : (a, b : HashBytes) -> cf a b = Right (h a b)) ->
+  (root, leaf : HashBytes) -> (prf : MerkleProof) ->
+  verifyProofE cf root leaf prf = Right (verifyProofWith h root leaf prf)
+verifyProofE_spec h cf model root leaf [] = Refl
+verifyProofE_spec h cf model root leaf ((GoLeft, sib) :: rest) =
+  rewrite model leaf sib in
+  verifyProofE_spec h cf model root (h leaf sib) rest
+verifyProofE_spec h cf model root leaf ((GoRight, sib) :: rest) =
+  rewrite model sib leaf in
+  verifyProofE_spec h cf model root (h sib leaf) rest
+
+--------------------------------------------------------------------------------
+-- Production connection (conditional on the thin FFI reflection hypothesis)
+--------------------------------------------------------------------------------
+
+||| Production root soundness, *conditional* on the FFI reflection hypothesis
+||| `reflect` - the IO fold equals `pure` of its pure mirror. That step is the
+||| sole assumed, undischargeable boundary (IO is opaque); everything else is
+||| machine-checked. Given it and a model `cf` of a pure combiner `h`, the
+||| production `rootHashBytesIO` computes the proven root.
+export
+rootHashBytesIO_spec : {io : Type -> Type} -> HasIO io => {n : Nat} ->
+  (h : Combiner) -> (cf : CombinerE) ->
+  (model : (a, b : HashBytes) -> cf a b = Right (h a b)) ->
+  (t : MerkleTree n) ->
+  (reflect : rootHashBytesIO {io} t = pure (rootHashBytesE cf t)) ->
+  rootHashBytesIO {io} t = pure (Right (rootHashWith h t))
+rootHashBytesIO_spec h cf model t reflect =
+  trans reflect (cong pure (rootHashBytesE_spec h cf model t))
+
+||| Production verification soundness, conditional on the FFI reflection
+||| hypothesis: `verifyProofIO` computes the proven Bool verdict.
+export
+verifyProofIO_spec : {io : Type -> Type} -> HasIO io =>
+  (h : Combiner) -> (cf : CombinerE) ->
+  (model : (a, b : HashBytes) -> cf a b = Right (h a b)) ->
+  (root, leaf : HashBytes) -> (prf : MerkleProof) ->
+  (reflect : verifyProofIO {io} root leaf prf = pure (verifyProofE cf root leaf prf)) ->
+  verifyProofIO {io} root leaf prf = pure (Right (verifyProofWith h root leaf prf))
+verifyProofIO_spec h cf model root leaf prf reflect =
+  trans reflect (cong pure (verifyProofE_spec h cf model root leaf prf))

ochrance.ipkg

@@ -25,6 +25,7 @@ modules = Ochrance.A2ML.Types
         , Ochrance.Filesystem.Merkle
         , Ochrance.Util.VectLemmas
         , Ochrance.Filesystem.MerkleBuild
+        , Ochrance.Filesystem.MerkleIO
         , Ochrance.Filesystem.Verify
         , Ochrance.Filesystem.Repair
         , Ochrance.FFI.Echidna