Skip to content

Commit 02ba7ec

Browse files
claudehyperpolymath
claude
authored and
hyperpolymath
committed
proof(merkle): Stage 1.3 — IO<->pure bridge (decompose: proven Either-monad mirror + thin FFI assumption)
Connect the proven Merkle theorems to the production IO crypto path without faking the FFI. IO is opaque, so the bridge is decomposed: - rootHashBytesE / verifyProofE: pure Either-monad mirrors of rootHashBytesIO / verifyProofIO (same control flow; a pure failing combiner cf models hashPairBlake3). - rootHashBytesE_spec / verifyProofE_spec (PROVEN): when cf models a pure combiner h with no failure, the Either-monad folds compute exactly the proven pure spec (Right (rootHashWith h t) / Right (verifyProofWith h ...)). This is the "modulo the Either allocation-failure plumbing" content, fully machine-checked. - rootHashBytesIO_spec / verifyProofIO_spec (PROVEN conditionally): the production IO folds compute the proven result, GIVEN the sole assumed boundary -- the IO fold equals `pure` of its pure mirror -- passed as an explicit `reflect` hypothesis. No postulate / believe_me; the trust boundary is named, not hidden. New module Ochrance.Filesystem.MerkleIO (added to ipkg). Clean --total build, 20/20. PROOFS.adoc: Stage 1.3 marked DONE; proven surface + optimisation ledger updated (root combiner now unlocked given the FFI-reflection hypothesis). https://claude.ai/code/session_011z2t8zAxfcCNLJzU7YdpBQ
1 parent db0f830 commit 02ba7ec

3 files changed

Lines changed: 136 additions & 6 deletions

File tree

‎docs/PROOFS.adoc‎

Lines changed: 13 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -91,6 +91,9 @@ The core is *clean*: all 19 `ochrance-core` modules carry `%default total` (the
9191
`indexReplace`, `finToNatReplace`, `splitAtConcat`.
9292
| `rootFoldLaw` + `foldRoot` (Stage 1.2)
9393
| root characterisation: `rootHashWith h (buildMerkleTree hs) = foldRoot h hs` (combiner-generic).
94+
| `rootHashBytesE_spec` / `verifyProofE_spec` (Stage 1.3)
95+
| Either-monad folds compute the pure spec on success; production `…IO_spec`
96+
theorems hold conditionally on the explicit FFI-reflection hypothesis (`MerkleIO`).
9497
| `roundtripManifest` + sub-codecs (`algoRT`, `modeRT`, `refsRT`, `mpolRT`, …)
9598
| grammar invertibility: `decodeManifest (encodeManifest m) = Just m`.
9699
| `SatisfiesMinimum` / `attestedSatisfiesLax`
@@ -115,10 +118,14 @@ design change or a model downshift mid-stage.
115118
(`rootFoldLaw` + `foldRoot` in `Ochrance.Filesystem.MerkleBuild`) — the root is a
116119
deterministic, representation-independent fold over the leaves. Combiner-generic;
117120
prerequisite of the binding argument. Machine-checked, axiom-free.
118-
. *[1.3] IO↔pure bridge*: prove `verifyProofIO` / `rootHashBytesIO` compute the
119-
`…With (hashPairBlake3 …)` spec modulo the `Either` allocation-failure plumbing,
120-
against a typed combiner-equality hypothesis — connecting the proven theorem to
121-
the *production* crypto path. (The estate-wide spine; see "The IO↔pure bridge".)
121+
. *[DONE — 1.3]* IO↔pure bridge (decompose): the pure `Either`-monad mirrors
122+
`rootHashBytesE` / `verifyProofE` provably compute the spec — `rootHashBytesE_spec`:
123+
`= Right (rootHashWith h t)`, `verifyProofE_spec`: `= Right (verifyProofWith h …)`
124+
when `cf` models `h` — fully machine-checked ("modulo the Either plumbing"). The
125+
opaque-IO step (IO fold = `pure` of its pure mirror) is the *sole* assumed boundary,
126+
passed as an explicit `reflect` hypothesis (no `postulate`/`believe_me`); the
127+
production theorems `rootHashBytesIO_spec` / `verifyProofIO_spec` hold conditionally
128+
on it. `Ochrance.Filesystem.MerkleIO`.
122129
. *[1.4] D2*: introduce `CollisionResistant h` and state `merkleBinding`
123130
(typed hypothesis / interface; discharged in Stage 4).
124131
+
@@ -225,8 +232,8 @@ transports to `F` by `rewrite`. Never optimise unproven code (nothing guards it)
225232

226233
| root combiner
227234
| real BLAKE3 in IO (vs. abstract `h`)
228-
| the Stage 1.3 bridge lemma
229-
| after 1.3
235+
| `rootHashBytesIO_spec` / `verifyProofIO_spec` (given the FFI-reflection hypothesis)
236+
| unlocked (Stage 1.3)
230237

231238
| A2ML production parser
232239
| any fast String parser

‎ochrance-core/Ochrance/Filesystem/MerkleIO.idr‎

Lines changed: 122 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,122 @@
1+
||| SPDX-License-Identifier: MPL-2.0
2+
|||
3+
||| Ochrance.Filesystem.MerkleIO - Stage 1.3: the IO<->pure bridge.
4+
|||
5+
||| The production crypto path (`rootHashBytesIO` / `verifyProofIO`) runs in IO
6+
||| and returns `Either OchranceError` to absorb BLAKE3 buffer-allocation
7+
||| failure. IO is opaque, so we *decompose* the bridge:
8+
|||
9+
||| * a pure `Either`-monad mirror of each fold (`rootHashBytesE` /
10+
||| `verifyProofE`) whose agreement with the proven pure spec
11+
||| (`rootHashWith` / `verifyProofWith`) is fully machine-checked - this is
12+
||| the "modulo the Either allocation-failure plumbing" content; and
13+
||| * the one assumed, undischargeable step (IO is opaque): that the IO fold
14+
||| equals `pure` of its pure mirror. This is supplied as an *explicit
15+
||| hypothesis argument* (`reflect`), never a `postulate`/`believe_me`, so the
16+
||| production-soundness results are stated honestly *conditionally* on it.
17+
module Ochrance.Filesystem.MerkleIO
18+
19+
import Data.Vect
20+
import Ochrance.Framework.Error
21+
import Ochrance.Filesystem.Merkle
22+
23+
%default total
24+
25+
||| A pure combiner that may fail: the error-monad model of `hashPairBlake3`,
26+
||| whose `Left` is the BLAKE3 buffer-allocation failure (z/out-of-memory).
27+
public export
28+
CombinerE : Type
29+
CombinerE = HashBytes -> HashBytes -> Either OchranceError HashBytes
30+
31+
--------------------------------------------------------------------------------
32+
-- Pure error-monad mirrors of the IO folds
33+
--------------------------------------------------------------------------------
34+
35+
||| Pure `Either`-monad mirror of `rootHashBytesIO`: the same control flow, with
36+
||| a pure failing combiner `cf` in place of the IO `hashPairBlake3`.
37+
public export
38+
rootHashBytesE : CombinerE -> MerkleTree n -> Either OchranceError HashBytes
39+
rootHashBytesE cf (Leaf x) = Right x
40+
rootHashBytesE cf (Node l r) =
41+
case rootHashBytesE cf l of
42+
Left err => Left err
43+
Right lHash => case rootHashBytesE cf r of
44+
Left err => Left err
45+
Right rHash => cf lHash rHash
46+
47+
||| Pure `Either`-monad mirror of `verifyProofIO`.
48+
public export
49+
verifyProofE : CombinerE -> (root, leaf : HashBytes) -> MerkleProof -> Either OchranceError Bool
50+
verifyProofE cf root leaf [] = Right (root == leaf)
51+
verifyProofE cf root leaf ((GoLeft, sib) :: rest) =
52+
case cf leaf sib of
53+
Left err => Left err
54+
Right parent => verifyProofE cf root parent rest
55+
verifyProofE cf root leaf ((GoRight, sib) :: rest) =
56+
case cf sib leaf of
57+
Left err => Left err
58+
Right parent => verifyProofE cf root parent rest
59+
60+
--------------------------------------------------------------------------------
61+
-- Pure bridge (machine-checked): the error-monad fold computes the spec
62+
--------------------------------------------------------------------------------
63+
64+
||| If `cf` models a pure combiner `h` with no failure (`cf a b = Right (h a b)`),
65+
||| the error-monad root fold returns exactly the proven pure root. This is the
66+
||| machine-checked half of the bridge.
67+
export
68+
rootHashBytesE_spec : (h : Combiner) -> (cf : CombinerE) ->
69+
(model : (a, b : HashBytes) -> cf a b = Right (h a b)) ->
70+
(t : MerkleTree n) ->
71+
rootHashBytesE cf t = Right (rootHashWith h t)
72+
rootHashBytesE_spec h cf model (Leaf x) = Refl
73+
rootHashBytesE_spec h cf model (Node l r) =
74+
rewrite rootHashBytesE_spec h cf model l in
75+
rewrite rootHashBytesE_spec h cf model r in
76+
model (rootHashWith h l) (rootHashWith h r)
77+
78+
||| Likewise for proof verification: the error-monad check computes the proven
79+
||| pure Bool verdict when `cf` models `h`.
80+
export
81+
verifyProofE_spec : (h : Combiner) -> (cf : CombinerE) ->
82+
(model : (a, b : HashBytes) -> cf a b = Right (h a b)) ->
83+
(root, leaf : HashBytes) -> (prf : MerkleProof) ->
84+
verifyProofE cf root leaf prf = Right (verifyProofWith h root leaf prf)
85+
verifyProofE_spec h cf model root leaf [] = Refl
86+
verifyProofE_spec h cf model root leaf ((GoLeft, sib) :: rest) =
87+
rewrite model leaf sib in
88+
verifyProofE_spec h cf model root (h leaf sib) rest
89+
verifyProofE_spec h cf model root leaf ((GoRight, sib) :: rest) =
90+
rewrite model sib leaf in
91+
verifyProofE_spec h cf model root (h sib leaf) rest
92+
93+
--------------------------------------------------------------------------------
94+
-- Production connection (conditional on the thin FFI reflection hypothesis)
95+
--------------------------------------------------------------------------------
96+
97+
||| Production root soundness, *conditional* on the FFI reflection hypothesis
98+
||| `reflect` - the IO fold equals `pure` of its pure mirror. That step is the
99+
||| sole assumed, undischargeable boundary (IO is opaque); everything else is
100+
||| machine-checked. Given it and a model `cf` of a pure combiner `h`, the
101+
||| production `rootHashBytesIO` computes the proven root.
102+
export
103+
rootHashBytesIO_spec : {io : Type -> Type} -> HasIO io => {n : Nat} ->
104+
(h : Combiner) -> (cf : CombinerE) ->
105+
(model : (a, b : HashBytes) -> cf a b = Right (h a b)) ->
106+
(t : MerkleTree n) ->
107+
(reflect : rootHashBytesIO {io} t = pure (rootHashBytesE cf t)) ->
108+
rootHashBytesIO {io} t = pure (Right (rootHashWith h t))
109+
rootHashBytesIO_spec h cf model t reflect =
110+
trans reflect (cong pure (rootHashBytesE_spec h cf model t))
111+
112+
||| Production verification soundness, conditional on the FFI reflection
113+
||| hypothesis: `verifyProofIO` computes the proven Bool verdict.
114+
export
115+
verifyProofIO_spec : {io : Type -> Type} -> HasIO io =>
116+
(h : Combiner) -> (cf : CombinerE) ->
117+
(model : (a, b : HashBytes) -> cf a b = Right (h a b)) ->
118+
(root, leaf : HashBytes) -> (prf : MerkleProof) ->
119+
(reflect : verifyProofIO {io} root leaf prf = pure (verifyProofE cf root leaf prf)) ->
120+
verifyProofIO {io} root leaf prf = pure (Right (verifyProofWith h root leaf prf))
121+
verifyProofIO_spec h cf model root leaf prf reflect =
122+
trans reflect (cong pure (verifyProofE_spec h cf model root leaf prf))

‎ochrance.ipkg‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -25,6 +25,7 @@ modules = Ochrance.A2ML.Types
2525
, Ochrance.Filesystem.Merkle
2626
, Ochrance.Util.VectLemmas
2727
, Ochrance.Filesystem.MerkleBuild
28+
, Ochrance.Filesystem.MerkleIO
2829
, Ochrance.Filesystem.Verify
2930
, Ochrance.Filesystem.Repair
3031
, Ochrance.FFI.Echidna

0 commit comments

Comments
 (0)