From e866bf329df5b9f79bc9031b03f470e6f5900d52 Mon Sep 17 00:00:00 2001 From: Claude Date: Thu, 18 Jun 2026 06:07:50 +0000 Subject: [PATCH 1/2] =?UTF-8?q?proof(repair):=20Stage=203.1=20=E2=80=94=20?= =?UTF-8?q?pure=20repair=20primitive=20correctness=20(idempotence=20proved?= =?UTF-8?q?)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit FSState's verifiable content is its hash map (no separate block data), so the pure repairBlockPure — installing a hash at one index — is the genuine repair semantics, not a no-op. Factored it out of the IO repairBlock (IO↔pure pattern: repairBlock = repairBlockPure + range check), making the correctness theorems well-founded. RepairProof (axiom-free, machine-checked): - repairBlockSets — the repaired index now holds exactly the new hash; - repairBlockPreserves — every other index is untouched; - repairBlockNumBlocks — the block count is unchanged; - repairBlockIdempotent — repairing the same (index, hash) twice = once (the ledger's "idempotence as a proof", delivered). Index test is Nat == (structural reflexivity eqNatReflTrue / neqNatFalse), so wall-free — unlike the primitive Hash ==. Idempotence decided via decEq to avoid the with-on-(==) asymmetric-reduction trap. NEXT (3.2): whole-manifest repair ⇒ verifyRefsHelper passes — builds on 2.2 + these lemmas, needs a distinct-in-range ref-name precondition and the isolated Hash-reflexivity hypothesis (documented). Verified: idris2 0.8.0, --build (--total), 25/25 modules, axiom-free. Co-Authored-By: Claude Opus 4.8 Claude-Session: https://claude.ai/code/session_011z2t8zAxfcCNLJzU7YdpBQ --- .machine_readable/6a2/STATE.a2ml | 8 +- docs/PROOFS.adoc | 41 +++++++--- ochrance-core/Ochrance/Filesystem/Repair.idr | 33 ++++---- .../Ochrance/Filesystem/RepairProof.idr | 79 +++++++++++++++++++ ochrance.ipkg | 1 + 5 files changed, 132 insertions(+), 30 deletions(-) create mode 100644 ochrance-core/Ochrance/Filesystem/RepairProof.idr diff --git a/.machine_readable/6a2/STATE.a2ml b/.machine_readable/6a2/STATE.a2ml index 2c1522a..4cb3de5 100644 --- a/.machine_readable/6a2/STATE.a2ml +++ b/.machine_readable/6a2/STATE.a2ml @@ -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 provable core complete: validator, verifier, hex)" +session = "machine-readable checkpoint — 2026-06-18 (Stage 1 complete; Stage 2 provable core complete; Stage 3.1 pure repair correctness 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 = 58 +completion-percentage = 62 [position] phase = "implementation" # design | implementation | testing | maintenance | archived @@ -30,6 +30,7 @@ theorems = [ "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)", + "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)", "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", @@ -57,7 +58,8 @@ issues = [ 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 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", + "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)", + "Then: verify→merkleCorrect wiring (architectural — verify builds no Merkle tree today; would carry merkleBinding's no-collision guarantee into verification)", "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", ] diff --git a/docs/PROOFS.adoc b/docs/PROOFS.adoc index 70cec88..859046e 100644 --- a/docs/PROOFS.adoc +++ b/docs/PROOFS.adoc @@ -111,6 +111,10 @@ The core is *clean*: all 19 `ochrance-core` modules carry `%default total` (the | 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). +| `repairBlock{Sets,Preserves,NumBlocks,Idempotent}` (Stage 3.1) +| pure repair primitive correctness over `repairBlockPure`: installs the hash at the + index, preserves other indices and the count, idempotent. Wall-free (`Nat` + structural `==`: `eqNatReflTrue` / `neqNatFalse`). | `roundtripManifest` + sub-codecs (`algoRT`, `modeRT`, `refsRT`, `mpolRT`, …) | grammar invertibility: `decodeManifest (encodeManifest m) = Just m`. | `SatisfiesMinimum` / `attestedSatisfiesLax` @@ -208,19 +212,30 @@ let `merkleBinding` carry the no-collision guarantee into verification). === Stage 3 — Repair correctness (L3, linear types) [model: Opus] -PRECONDITION (surfaced at Compaction 2): `repair` is currently a *stub* — -`repairBlock` (`Repair.idr`) updates the hash map but does **not** read or write -block data. Proving `verify (repair s) = Valid` against a no-op would be vacuous or -false. DECISION (recommended): introduce a pure -`repairPure : FSState -> Manifest -> FSState` that genuinely reconstructs the hash -map, prove correctness over *that*, and make the IO `repair` a proven-equivalent -shell (the IO↔pure pattern). Alternative: leave repair honestly-bounded until real -block-I/O lands (defers the linear-type theorem). - -. `verifyPure (repairPure s m) m = True` — the meaty (now well-founded) theorem. -. Repair idempotence as a *proof* (today only a property test). -. Harvest framework's mode-indexed Interface; state the `VerifiedSubsystem` law - `verify (repair s m) m = Right …` and prove the FSState instance satisfies it. +RESOLVED (was PRECONDITION): the pure repair core is now factored out — +`repairBlockPure : FSState -> BlockIndex -> Hash -> FSState` installs a hash in the +map, and the IO `repairBlock` is `repairBlockPure` + the range check (IO↔pure +pattern). Because FSState's verifiable content *is* its hash map (it carries no +separate block data), this is the genuine repair semantics, so the theorems are +well-founded, not vacuous. + +. *[DONE — 3.1]* Pure repair primitive correctness, machine-checked + (`Ochrance.Filesystem.RepairProof`, axiom-free): `repairBlockSets` (the repaired + index now holds the new hash), `repairBlockPreserves` (every other index + untouched), `repairBlockNumBlocks` (block count preserved), and + `repairBlockIdempotent` (repairing the same (index, hash) twice = once) — the + ledger's "idempotence as a proof", delivered. The index test is `Nat` `==` + (structural — `eqNatReflTrue` / `neqNatFalse`), so wall-free, unlike the primitive + `Hash` `==`. +. *[3.2 — next]* Whole-manifest repair ⇒ verify: + `verifyRefsHelper (repairPure s m) m.refs = Right ()`. Builds on 2.2's + `verifyRefsHelper` and the 3.1 lemmas, but needs (a) a precondition that ref names + parse to *distinct* in-range indices (so the rebuilt map is per-ref consistent), + and (b) the isolated `Hash`-reflexivity hypothesis `(h == h) = True` — the same + primitive `==` wall as `merkleCorrect`'s residual step — named explicitly, never + faked. +. Harvest framework's mode-indexed Interface; state the `VerifiedSubsystem` law and + prove the FSState instance satisfies it. + WATCH-FOR: may need proof witnesses threaded through the `1`-quantified API — possible signature changes to `Repair.idr`. diff --git a/ochrance-core/Ochrance/Filesystem/Repair.idr b/ochrance-core/Ochrance/Filesystem/Repair.idr index 3e3ff1c..fbdd8ce 100644 --- a/ochrance-core/Ochrance/Filesystem/Repair.idr +++ b/ochrance-core/Ochrance/Filesystem/Repair.idr @@ -27,6 +27,19 @@ import Ochrance.FFI.Crypto -- Linear Repair Operations -------------------------------------------------------------------------------- +||| Pure core of a single-block repair: install `expectedHash` at `blockIdx` in the +||| state's hash map, leaving every other block and the block count untouched. The +||| filesystem state's verifiable content *is* this hash map (FSState carries no +||| separate block data), so this is the genuine repair semantics, not a no-op - the +||| IO `repairBlock` is this plus the range check. Correctness is proved in +||| `Ochrance.Filesystem.RepairProof`. +public export +repairBlockPure : FSState -> BlockIndex -> Hash -> FSState +repairBlockPure s blockIdx expectedHash = + MkFSState s.numBlocks + (\idx => if idx == blockIdx then Just expectedHash else s.blockHash idx) + s.metadata + ||| Repair a single block in the filesystem. ||| Uses linear types to ensure oldState is consumed exactly once. ||| @@ -46,20 +59,12 @@ repairBlock oldState blockIdx expectedHash = do -- Check if block index is valid if blockIdx >= numBlocks then pure (Left (QError (InvalidManifestPath ("Block index out of range: " ++ show blockIdx)))) - else do - -- In a real implementation, this would: - -- 1. Read the corrupted block - -- 2. Attempt to repair from redundancy/parity data - -- 3. Verify the repaired block matches expectedHash - -- 4. Write the repaired block back to disk - - -- For now, we create a new state with the hash updated - let newState = MkFSState - numBlocks - (\idx => if idx == blockIdx then Just expectedHash else blockHashFunc idx) - metadata - - pure (Right newState) + else + -- The verifiable state is the hash map; repairBlockPure installs the hash. + -- (A real backend would also read/repair/write block bytes; FSState models + -- only the hashes, so this is the complete pure repair of the modelled state.) + pure (Right (repairBlockPure (MkFSState numBlocks blockHashFunc metadata) + blockIdx expectedHash)) ||| Repair filesystem from a snapshot (linear version). ||| Consumes the old state and produces a new state matching the snapshot. diff --git a/ochrance-core/Ochrance/Filesystem/RepairProof.idr b/ochrance-core/Ochrance/Filesystem/RepairProof.idr new file mode 100644 index 0000000..f9634b6 --- /dev/null +++ b/ochrance-core/Ochrance/Filesystem/RepairProof.idr @@ -0,0 +1,79 @@ +||| SPDX-License-Identifier: MPL-2.0 +||| +||| Ochrance.Filesystem.RepairProof - Stage 3: pure repair correctness. +||| +||| FSState's verifiable content is its hash map (`BlockIndex -> Maybe Hash`); there +||| is no separate block data. So `repairBlockPure` - which installs a hash at one +||| index - is the genuine repair semantics (not a no-op against which a theorem +||| would be vacuous), and these lemmas pin it down: +||| +||| * `repairBlockSets` - the repaired index now holds exactly the new hash; +||| * `repairBlockPreserves` - every other index is untouched; +||| * `repairBlockNumBlocks` - the block count is unchanged; +||| * `repairBlockIdempotent` - repairing the same (index, hash) twice equals once. +||| +||| All axiom-free: the index test is `Nat` `==`, whose reflexivity is *structural* +||| (`eqNatReflTrue`) - unlike the primitive `Hash`/`String` `==`. No `believe_me`, +||| no `postulate`. +module Ochrance.Filesystem.RepairProof + +import Decidable.Equality + +import Ochrance.A2ML.Types +import Ochrance.Filesystem.Types +import Ochrance.Filesystem.Repair + +%default total + +||| `Nat` equality is reflexively `True` - provable because `Eq Nat` is structural +||| (the wall-free counterpart of the primitive `String`/`Bits8` reflexivity that +||| the `Hash` comparison would need). +public export +eqNatReflTrue : (n : Nat) -> (n == n) = True +eqNatReflTrue Z = Refl +eqNatReflTrue (S k) = eqNatReflTrue k + +||| Repair installs the requested hash at the repaired index. +export +repairBlockSets : (s : FSState) -> (i : BlockIndex) -> (h : Hash) -> + blockHash (repairBlockPure s i h) i = Just h +repairBlockSets s i h = rewrite eqNatReflTrue i in Refl + +||| Repair leaves every other index untouched. +export +repairBlockPreserves : (s : FSState) -> (i : BlockIndex) -> (h : Hash) -> + (j : BlockIndex) -> (j == i) = False -> + blockHash (repairBlockPure s i h) j = blockHash s j +repairBlockPreserves s i h j neq = rewrite neq in Refl + +||| Repair preserves the block count. +export +repairBlockNumBlocks : (s : FSState) -> (i : BlockIndex) -> (h : Hash) -> + numBlocks (repairBlockPure s i h) = numBlocks s +repairBlockNumBlocks s i h = Refl + +||| `Nat` inequality reflects as `== = False` (structural counterpart of the +||| primitive-equality wall). Used to drive `repairBlockPreserves` on the `j /= i` +||| branch of idempotence. +neqNatFalse : (m, n : Nat) -> Not (m = n) -> (m == n) = False +neqNatFalse Z Z ctra = absurd (ctra Refl) +neqNatFalse Z (S _) _ = Refl +neqNatFalse (S _) Z _ = Refl +neqNatFalse (S k) (S l) ctra = neqNatFalse k l (\p => ctra (cong S p)) + +||| Repair idempotence: repairing the same index with the same hash twice agrees +||| with doing it once, at every index (extensional equality of the hash maps). +||| Decided on `j` vs `i`: at `i`, both sides read `Just h` (`repairBlockSets`); +||| elsewhere, both read the original (`repairBlockPreserves`). Uses `decEq` rather +||| than a `with` on `j == i` (whose reduct `equalNat` collapses the two `if`s +||| asymmetrically). +export +repairBlockIdempotent : (s : FSState) -> (i : BlockIndex) -> (h : Hash) -> + (j : BlockIndex) -> + blockHash (repairBlockPure (repairBlockPure s i h) i h) j + = blockHash (repairBlockPure s i h) j +repairBlockIdempotent s i h j = case decEq j i of + Yes prf => rewrite prf in + trans (repairBlockSets (repairBlockPure s i h) i h) + (sym (repairBlockSets s i h)) + No ctra => repairBlockPreserves (repairBlockPure s i h) i h j (neqNatFalse j i ctra) diff --git a/ochrance.ipkg b/ochrance.ipkg index 8a9333c..a296c92 100644 --- a/ochrance.ipkg +++ b/ochrance.ipkg @@ -32,6 +32,7 @@ modules = Ochrance.A2ML.Types , Ochrance.Filesystem.Verify , Ochrance.Filesystem.VerifyProof , Ochrance.Filesystem.Repair + , Ochrance.Filesystem.RepairProof , Ochrance.FFI.Echidna opts = "--total" From d4ea8afe967990a899de529af6187363efabb3c1 Mon Sep 17 00:00:00 2001 From: Claude Date: Thu, 18 Jun 2026 06:59:10 +0000 Subject: [PATCH 2/2] =?UTF-8?q?proof(verify):=20Stage=202.4=20=E2=80=94=20?= =?UTF-8?q?verify=E2=86=94Merkle=20wiring=20(root=20is=20a=20faithful=20fi?= =?UTF-8?q?ngerprint=20of=20the=20blocks)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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 Claude-Session: https://claude.ai/code/session_011z2t8zAxfcCNLJzU7YdpBQ --- .machine_readable/6a2/STATE.a2ml | 8 ++- docs/PROOFS.adoc | 20 +++++-- .../Ochrance/Filesystem/VerifyMerkle.idr | 55 +++++++++++++++++++ ochrance.ipkg | 1 + 4 files changed, 77 insertions(+), 7 deletions(-) create mode 100644 ochrance-core/Ochrance/Filesystem/VerifyMerkle.idr diff --git a/.machine_readable/6a2/STATE.a2ml b/.machine_readable/6a2/STATE.a2ml index 4cb3de5..1cc912e 100644 --- a/.machine_readable/6a2/STATE.a2ml +++ b/.machine_readable/6a2/STATE.a2ml @@ -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 provable core complete; Stage 3.1 pure repair correctness done)" +session = "machine-readable checkpoint — 2026-06-18 (Stage 1 complete; Stage 2 core + 2.4 verify↔Merkle wiring; Stage 3.1 pure repair correctness)" [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 = 62 +completion-percentage = 66 [position] phase = "implementation" # design | implementation | testing | maintenance | archived @@ -31,6 +31,7 @@ theorems = [ "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)", "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)", + "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", "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", @@ -59,7 +60,8 @@ 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 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.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)", - "Then: verify→merkleCorrect wiring (architectural — verify builds no Merkle tree today; would carry merkleBinding's no-collision guarantee into verification)", + "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)", + "Stage 3.2 (next provable): whole-manifest repairPure ⇒ verifyRefsHelper accepts (distinct-in-range ref-name precondition + isolated Hash-reflexivity hypothesis)", "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", ] diff --git a/docs/PROOFS.adoc b/docs/PROOFS.adoc index 859046e..fcf5cec 100644 --- a/docs/PROOFS.adoc +++ b/docs/PROOFS.adoc @@ -115,6 +115,11 @@ The core is *clean*: all 19 `ochrance-core` modules carry `%default total` (the | pure repair primitive correctness over `repairBlockPure`: installs the hash at the index, preserves other indices and the count, idempotent. Wall-free (`Nat` structural `==`: `eqNatReflTrue` / `neqNatFalse`). +| `rootFaithful` / `rootVerifySound` (Stage 2.4) +| verify↔Merkle wiring: the Merkle root is a faithful fingerprint of the block-hash + vector — equal roots `<->` equal leaves (forward = `merkleBindingTree`; backward = + congruence). Licenses root-based verification; binding (1.4) carried into the verify + use-case. | `roundtripManifest` + sub-codecs (`algoRT`, `modeRT`, `refsRT`, `mpolRT`, …) | grammar invertibility: `decodeManifest (encodeManifest m) = Just m`. | `SatisfiesMinimum` / `attestedSatisfiesLax` @@ -193,10 +198,17 @@ not the nested `isValidHexString`. 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). +PARTLY WIRED (Stage 2.4): the *proof-level* wiring is done - +`Ochrance.Filesystem.VerifyMerkle` proves the root is a FAITHFUL fingerprint of the +block-hash vector: `rootFaithful` gives equal roots `<->` equal leaves (forward = +`merkleBindingTree` / `CollisionResistant h`; backward = congruence), and +`rootVerifySound` is the security reading - matching committed root ⇒ identical +blocks. This is the theorem that *licenses* root-based verification, carrying Stage +1.4's binding guarantee into the verification use-case. ++ +STILL OPEN (architectural): connecting that to the *live* `Hash`-based +`verifyRefsHelper` needs the hex `Hash` <-> `HashBytes` conversion (Stage 2.3, +bounded) and a power-of-two leaf layout - a verify-path change, not a proof. . *[DONE — 2.3]* Hex codec structural round-trip. The full `hexStringToBytes (bytesToHex bs) = Just bs` crosses two primitive walls — diff --git a/ochrance-core/Ochrance/Filesystem/VerifyMerkle.idr b/ochrance-core/Ochrance/Filesystem/VerifyMerkle.idr new file mode 100644 index 0000000..5556dbb --- /dev/null +++ b/ochrance-core/Ochrance/Filesystem/VerifyMerkle.idr @@ -0,0 +1,55 @@ +||| SPDX-License-Identifier: MPL-2.0 +||| +||| Ochrance.Filesystem.VerifyMerkle - wiring verification to the Merkle proofs. +||| +||| Root-based verification - trusting a single Merkle root instead of checking every +||| block hash - is sound and complete *exactly* because the root is a FAITHFUL +||| fingerprint of the leaf vector: two block-hash vectors build trees with equal +||| roots iff the vectors are equal. The forward (no-collision / binding) direction is +||| `merkleBindingTree` (Stage 1.4, discharged against `CollisionResistant h`); the +||| backward direction is congruence. This is the theorem that licenses a verifier to +||| trust a root, and it carries Stage 1.4's binding guarantee into the verification +||| use-case. +||| +||| NOTE (remaining bridge): this connects the proven Merkle layer (`HashBytes` +||| leaves) to the verification use-case. Connecting it the rest of the way to the +||| *live* A2ML-`Hash`-based verifier (`verifyRefsHelper`, Stage 2.2) additionally +||| needs the hex `Hash` <-> `HashBytes` conversion (Stage 2.3, bounded by the +||| `unpack`/`pack` + `Bits8` walls) and a power-of-two leaf layout - a verify-path +||| change, documented in docs/PROOFS.adoc, not faked here. +module Ochrance.Filesystem.VerifyMerkle + +import Data.Vect + +import Ochrance.Filesystem.Merkle +import Ochrance.Filesystem.MerkleBinding + +%default total + +||| The Merkle root is a faithful fingerprint of the block-hash vector: equal roots +||| iff equal leaves. Backward is congruence (same leaves => same root); forward is +||| binding (`merkleBindingTree` against the typed `CollisionResistant h`). Checking +||| one root is therefore *equivalent* to checking every block hash - the +||| justification for root-based verification. +export +rootFaithful : (h : Combiner) -> CollisionResistant h -> {n : Nat} -> + (xs, ys : Vect (power 2 n) HashBytes) -> + ( (rootHashWith h (buildMerkleTree {n} xs) = rootHashWith h (buildMerkleTree {n} ys)) -> xs = ys + , (xs = ys) -> (rootHashWith h (buildMerkleTree {n} xs) = rootHashWith h (buildMerkleTree {n} ys)) + ) +rootFaithful h cr xs ys = + ( merkleBindingTree h cr xs ys + , \eq => cong (\v => rootHashWith h (buildMerkleTree {n} v)) eq + ) + +||| The verifier's security guarantee, as the forward direction in verification terms: +||| if the actual blocks build a tree whose root matches the expected (manifest) root, +||| the actual blocks ARE the expected blocks - no collision can substitute different +||| data under the same committed root. (First projection of `rootFaithful`.) +export +rootVerifySound : (h : Combiner) -> CollisionResistant h -> {n : Nat} -> + (actual, expected : Vect (power 2 n) HashBytes) -> + rootHashWith h (buildMerkleTree {n} actual) + = rootHashWith h (buildMerkleTree {n} expected) -> + actual = expected +rootVerifySound h cr actual expected = merkleBindingTree h cr actual expected diff --git a/ochrance.ipkg b/ochrance.ipkg index a296c92..0607ea1 100644 --- a/ochrance.ipkg +++ b/ochrance.ipkg @@ -31,6 +31,7 @@ modules = Ochrance.A2ML.Types , Ochrance.Filesystem.MerkleBinding , Ochrance.Filesystem.Verify , Ochrance.Filesystem.VerifyProof + , Ochrance.Filesystem.VerifyMerkle , Ochrance.Filesystem.Repair , Ochrance.Filesystem.RepairProof , Ochrance.FFI.Echidna