Skip to content

Commit 04b5da9

Browse files
claudehyperpolymath
claude
authored and
hyperpolymath
committed
proof(verify): Stage 2.4 — verify↔Merkle wiring (root is a faithful fingerprint of the blocks)
rootFaithful proves the Merkle root is a faithful fingerprint of the block-hash vector: equal roots <-> equal leaves. The forward direction (no two distinct block-sets share a root) is merkleBindingTree against CollisionResistant h (Stage 1.4); the backward direction is congruence. rootVerifySound is the security reading — a matching committed root implies identical blocks. This is the theorem that licenses root-based verification, carrying Stage 1.4's binding guarantee into the verification use-case. Ochrance.Filesystem.VerifyMerkle. Builds entirely on the secured base — no new walls, no postulate/believe_me. Verified: idris2 0.8.0, --build (--total), 26/26 modules, axiom-free. REMAINING (documented, architectural): connecting this to the live Hash-based verifyRefsHelper (Stage 2.2) needs the hex Hash<->HashBytes conversion (Stage 2.3, bounded by unpack/pack + Bits8) and a power-of-two leaf layout — a verify-path change, not a proof. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_011z2t8zAxfcCNLJzU7YdpBQ
1 parent 93181d1 commit 04b5da9

4 files changed

Lines changed: 77 additions & 7 deletions

File tree

‎.machine_readable/6a2/STATE.a2ml‎

Lines changed: 5 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -7,12 +7,12 @@ project = "ochrance"
77
version = "0.1.0"
88
last-updated = "2026-06-18"
99
status = "active"
10-
session = "machine-readable checkpoint — 2026-06-18 (Stage 1 complete; Stage 2 provable core complete; Stage 3.1 pure repair correctness done)"
10+
session = "machine-readable checkpoint — 2026-06-18 (Stage 1 complete; Stage 2 core + 2.4 verify↔Merkle wiring; Stage 3.1 pure repair correctness)"
1111

1212
[project-context]
1313
name = "Ochránce"
1414
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."""
15-
completion-percentage = 62
15+
completion-percentage = 66
1616

1717
[position]
1818
phase = "implementation" # design | implementation | testing | maintenance | archived
@@ -31,6 +31,7 @@ theorems = [
3131
"parsePairsRoundtrip (Stage 2.3) — hex codec structural soundness: parsePairs (bytesToHexChars bs) = Just bs, given isolated per-byte Bits8 hypothesis (pack/unpack wall explicit)",
3232
"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)",
3333
"repairBlock{Sets,Preserves,NumBlocks,Idempotent} (Stage 3.1) — pure repair primitive correctness over repairBlockPure: installs hash at index, preserves others + count, idempotent (wall-free Nat == via eqNatReflTrue/neqNatFalse)",
34+
"rootFaithful / rootVerifySound (Stage 2.4) — verify↔Merkle wiring: Merkle root is a faithful fingerprint of the block-hash vector (equal roots <-> equal leaves; forward = merkleBindingTree, backward = cong). Licenses root-based verification",
3435
"roundtripManifest (+ algoRT/modeRT/refsRT/mpolRT codecs) — decodeManifest (encodeManifest m) = Just m",
3536
"SatisfiesMinimum / attestedSatisfiesLax — progressive-assurance threshold witness",
3637
"ABI Handle / createHandle — So (ptr /= 0) non-null invariant",
@@ -59,7 +60,8 @@ actions = [
5960
"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)",
6061
"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",
6162
"Stage 3.1 DONE — pure repair primitive correctness (repairBlockPure factored out; sets/preserves/numBlocks/idempotent machine-checked). NEXT 3.2: whole-manifest repair ⇒ verifyRefsHelper passes (needs distinct-in-range ref-name precondition + isolated Hash-reflexivity hypothesis)",
62-
"Then: verify→merkleCorrect wiring (architectural — verify builds no Merkle tree today; would carry merkleBinding's no-collision guarantee into verification)",
63+
"Stage 2.4 DONE — verify↔Merkle proof-level wiring (rootFaithful/rootVerifySound): the root is a faithful fingerprint of the blocks (binding). REMAINING: connect to the live Hash-based verifyRefsHelper via hex Hash<->HashBytes conversion (2.3-bounded) + power-of-two layout (verify-path change, not a proof)",
64+
"Stage 3.2 (next provable): whole-manifest repairPure ⇒ verifyRefsHelper accepts (distinct-in-range ref-name precondition + isolated Hash-reflexivity hypothesis)",
6365
"Remove Idris-side crypto stubs and build + link libochrance.so into the flow (unblocks the crypto-integrity claim)",
6466
"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",
6567
]

‎docs/PROOFS.adoc‎

Lines changed: 16 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -115,6 +115,11 @@ The core is *clean*: all 19 `ochrance-core` modules carry `%default total` (the
115115
| pure repair primitive correctness over `repairBlockPure`: installs the hash at the
116116
index, preserves other indices and the count, idempotent. Wall-free (`Nat`
117117
structural `==`: `eqNatReflTrue` / `neqNatFalse`).
118+
| `rootFaithful` / `rootVerifySound` (Stage 2.4)
119+
| verify↔Merkle wiring: the Merkle root is a faithful fingerprint of the block-hash
120+
vector — equal roots `<->` equal leaves (forward = `merkleBindingTree`; backward =
121+
congruence). Licenses root-based verification; binding (1.4) carried into the verify
122+
use-case.
118123
| `roundtripManifest` + sub-codecs (`algoRT`, `modeRT`, `refsRT`, `mpolRT`, …)
119124
| grammar invertibility: `decodeManifest (encodeManifest m) = Just m`.
120125
| `SatisfiesMinimum` / `attestedSatisfiesLax`
@@ -193,10 +198,17 @@ not the nested `isValidHexString`.
193198
block-present, hash-equal). `Ochrance.Filesystem.VerifyProof`. Machine-checked,
194199
axiom-free.
195200
+
196-
STILL OPEN (architectural, by design): "wired to `merkleCorrect`". The verifier
197-
compares per-ref hashes and never builds a Merkle tree, so checking against a Merkle
198-
*root* is a verify-path redesign, not a proof. Deferred to a design decision (would
199-
let `merkleBinding` carry the no-collision guarantee into verification).
201+
PARTLY WIRED (Stage 2.4): the *proof-level* wiring is done -
202+
`Ochrance.Filesystem.VerifyMerkle` proves the root is a FAITHFUL fingerprint of the
203+
block-hash vector: `rootFaithful` gives equal roots `<->` equal leaves (forward =
204+
`merkleBindingTree` / `CollisionResistant h`; backward = congruence), and
205+
`rootVerifySound` is the security reading - matching committed root ⇒ identical
206+
blocks. This is the theorem that *licenses* root-based verification, carrying Stage
207+
1.4's binding guarantee into the verification use-case.
208+
+
209+
STILL OPEN (architectural): connecting that to the *live* `Hash`-based
210+
`verifyRefsHelper` needs the hex `Hash` <-> `HashBytes` conversion (Stage 2.3,
211+
bounded) and a power-of-two leaf layout - a verify-path change, not a proof.
200212

201213
. *[DONE — 2.3]* Hex codec structural round-trip. The full
202214
`hexStringToBytes (bytesToHex bs) = Just bs` crosses two primitive walls —

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

Lines changed: 55 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,55 @@
1+
||| SPDX-License-Identifier: MPL-2.0
2+
|||
3+
||| Ochrance.Filesystem.VerifyMerkle - wiring verification to the Merkle proofs.
4+
|||
5+
||| Root-based verification - trusting a single Merkle root instead of checking every
6+
||| block hash - is sound and complete *exactly* because the root is a FAITHFUL
7+
||| fingerprint of the leaf vector: two block-hash vectors build trees with equal
8+
||| roots iff the vectors are equal. The forward (no-collision / binding) direction is
9+
||| `merkleBindingTree` (Stage 1.4, discharged against `CollisionResistant h`); the
10+
||| backward direction is congruence. This is the theorem that licenses a verifier to
11+
||| trust a root, and it carries Stage 1.4's binding guarantee into the verification
12+
||| use-case.
13+
|||
14+
||| NOTE (remaining bridge): this connects the proven Merkle layer (`HashBytes`
15+
||| leaves) to the verification use-case. Connecting it the rest of the way to the
16+
||| *live* A2ML-`Hash`-based verifier (`verifyRefsHelper`, Stage 2.2) additionally
17+
||| needs the hex `Hash` <-> `HashBytes` conversion (Stage 2.3, bounded by the
18+
||| `unpack`/`pack` + `Bits8` walls) and a power-of-two leaf layout - a verify-path
19+
||| change, documented in docs/PROOFS.adoc, not faked here.
20+
module Ochrance.Filesystem.VerifyMerkle
21+
22+
import Data.Vect
23+
24+
import Ochrance.Filesystem.Merkle
25+
import Ochrance.Filesystem.MerkleBinding
26+
27+
%default total
28+
29+
||| The Merkle root is a faithful fingerprint of the block-hash vector: equal roots
30+
||| iff equal leaves. Backward is congruence (same leaves => same root); forward is
31+
||| binding (`merkleBindingTree` against the typed `CollisionResistant h`). Checking
32+
||| one root is therefore *equivalent* to checking every block hash - the
33+
||| justification for root-based verification.
34+
export
35+
rootFaithful : (h : Combiner) -> CollisionResistant h -> {n : Nat} ->
36+
(xs, ys : Vect (power 2 n) HashBytes) ->
37+
( (rootHashWith h (buildMerkleTree {n} xs) = rootHashWith h (buildMerkleTree {n} ys)) -> xs = ys
38+
, (xs = ys) -> (rootHashWith h (buildMerkleTree {n} xs) = rootHashWith h (buildMerkleTree {n} ys))
39+
)
40+
rootFaithful h cr xs ys =
41+
( merkleBindingTree h cr xs ys
42+
, \eq => cong (\v => rootHashWith h (buildMerkleTree {n} v)) eq
43+
)
44+
45+
||| The verifier's security guarantee, as the forward direction in verification terms:
46+
||| if the actual blocks build a tree whose root matches the expected (manifest) root,
47+
||| the actual blocks ARE the expected blocks - no collision can substitute different
48+
||| data under the same committed root. (First projection of `rootFaithful`.)
49+
export
50+
rootVerifySound : (h : Combiner) -> CollisionResistant h -> {n : Nat} ->
51+
(actual, expected : Vect (power 2 n) HashBytes) ->
52+
rootHashWith h (buildMerkleTree {n} actual)
53+
= rootHashWith h (buildMerkleTree {n} expected) ->
54+
actual = expected
55+
rootVerifySound h cr actual expected = merkleBindingTree h cr actual expected

‎ochrance.ipkg‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -31,6 +31,7 @@ modules = Ochrance.A2ML.Types
3131
, Ochrance.Filesystem.MerkleBinding
3232
, Ochrance.Filesystem.Verify
3333
, Ochrance.Filesystem.VerifyProof
34+
, Ochrance.Filesystem.VerifyMerkle
3435
, Ochrance.Filesystem.Repair
3536
, Ochrance.Filesystem.RepairProof
3637
, Ochrance.FFI.Echidna

0 commit comments

Comments
 (0)