From d8afda3564edcb86ef6343cd0d01c87b2d499cd1 Mon Sep 17 00:00:00 2001 From: Claude Date: Wed, 17 Jun 2026 21:42:17 +0000 Subject: [PATCH] docs(proofs): record Stage 1.1; add optimisation ledger + build-with-proofs discipline; truth-fix TOPOLOGY PROOFS.adoc: - Mark Stage 1.1 (buildGetLeaf) DONE; add buildGetLeaf + Util.VectLemmas to the proven surface; flip the powerTwoSucc transport WATCH-FOR -> RESOLVED. - Split remaining Stage 1 into 1.2 root-fold law / 1.3 IO<->pure bridge / 1.4 D2. - Surface the Repair-is-a-stub precondition + recommended pure-model decision (Stage 3). - Add three sections: the IO<->pure bridge (estate-wide spine), the build-with-proofs discipline, and the optimisation ledger (against the proven backdrop). - Reconcile module count: 19 core modules (+ separate src/abi tree). TOPOLOGY.md: - Regrade the dashboard onto the honest proof axis: Merkle 70%, Repair 20% (stub), ECHIDNA 10% (stubbed), crypto-not-yet-linked 20%. Replaces the inflated 80-100% bars that contradicted the ledger. - Point to docs/PROOFS.adoc as authoritative; clarify bars track proof completeness. https://claude.ai/code/session_011z2t8zAxfcCNLJzU7YdpBQ --- TOPOLOGY.md | 44 ++++++++++++------ docs/PROOFS.adoc | 116 +++++++++++++++++++++++++++++++++++++++++++---- 2 files changed, 135 insertions(+), 25 deletions(-) diff --git a/TOPOLOGY.md b/TOPOLOGY.md index 3d83fa2..1ebcb06 100644 --- a/TOPOLOGY.md +++ b/TOPOLOGY.md @@ -1,6 +1,6 @@ - + # Ochránce — Project Topology @@ -51,27 +51,36 @@ ## Completion Dashboard +> Percentages track **proof / verification completeness** — the honest axis for a +> verification framework — **not** "code exists". `docs/PROOFS.adoc` is the +> authoritative ledger; this dashboard only summarises it. Where an implementation +> exists but its correctness is unproven (or is a stub), the bar reflects the +> *proof*, not the code. + ``` -COMPONENT STATUS NOTES -───────────────────────────────── ────────────────── ───────────────────────────────── +COMPONENT STATUS NOTES (proof / verification axis) +─────────────────────────────────── ────────────── ──────────────────────────────────────────── CORE VERIFICATION (IDRIS2) - Merkle Tree Implementation ██████████ 100% Size-indexed proofs stable - Linear Type Repair ████████░░ 80% Use-after-repair prevention - A2ML Parser ██████████ 100% Attestation DSL verified - VerifiedSubsystem Interface ██████████ 100% Abstract interface stable + Merkle soundness + round-trip ███████░░░ 70% merkleCorrect(With) + buildGetLeaf proven + Merkle completeness + binding ░░░░░░░░░░ 0% converse + CollisionResistant (Stage 1.4/4) + A2ML parser + reference round-trip ███████░░░ 70% total; ref-codec proven; prod pipeline runtime-only + Verify soundness ░░░░░░░░░░ 0% verify success ⇏ a proof yet (Stage 2) + Linear-type Repair ██░░░░░░░░ 20% IMPL IS A STUB (no block I/O); unproven (Stage 3) + VerifiedSubsystem law █████░░░░░ 50% interface + FSState instance; law unproven (Stage 3) + Progressive assurance ███████░░░ 70% attestedSatisfiesLax proven; monotonicity (Stage 4) SYSTEM & EXTERNAL - Zig FFI Bridge ██████████ 100% Stable C ABI bridge - ECHIDNA Integration ██████░░░░ 60% Proof synthesis refining - Filesystem Module ████████░░ 80% Reference implementation stable + Zig crypto (BLAKE3/SHA/Ed25519) ███████░░░ 70% implemented + known-answer-vector tested in Zig + Crypto linked into verify flow ██░░░░░░░░ 20% NOT linked; Idris-side stubs still live (#39) + ECHIDNA integration █░░░░░░░░░ 10% design types only; FFI entirely stubbed REPO INFRASTRUCTURE - Justfile Automation ██████████ 100% Standard build/verify tasks - .machine_readable/ ██████████ 100% STATE tracking active - Idris2 .ipkg ██████████ 100% Package definitions verified + Justfile automation ██████████ 100% build / verify tasks + .machine_readable/ ██████████ 100% STATE tracking active + Idris2 .ipkg / totality gate ██████████ 100% 19 core modules; --total build green -───────────────────────────────────────────────────────────────────────────── -OVERALL: ████████░░ ~80% Framework stable, ML maturing +──────────────────────────────────────────────────────────────────────────────────────────────── +OVERALL (proof axis): ████░░░░░░ ~40% Stage 1.1 done; 1.2–4 open. See docs/PROOFS.adoc. ``` ## Key Dependencies @@ -94,3 +103,8 @@ This file is maintained by both humans and AI agents. When updating: Progress bars use: `█` (filled) and `░` (empty), 10 characters wide. Percentages: 0%, 10%, 20%, ... 100% (in 10% increments). + +The bars track **proof / verification completeness** against `docs/PROOFS.adoc` +(the authoritative ledger), not whether code merely exists. Do not raise a bar to +100% on the strength of an implementation alone — a component is "done" only when +its correctness is proven or honestly bounded per the ledger. diff --git a/docs/PROOFS.adoc b/docs/PROOFS.adoc index 3f9a068..fc8247d 100644 --- a/docs/PROOFS.adoc +++ b/docs/PROOFS.adoc @@ -68,7 +68,8 @@ Three repositories are in scope. "Verification" means something different in eac == Current proof state (ochrance, canonical) -The core is *clean*: all 24 modules carry `%default total`; zero +The core is *clean*: all 19 `ochrance-core` modules carry `%default total` (the +`src/abi/` tree adds the ABI modules separately); zero `believe_me` / `assert_*` / `postulate` / holes / `partial` on any proof symbol. .Proven, machine-checked (axiom-free) @@ -83,6 +84,11 @@ The core is *clean*: all 24 modules carry `%default total`; zero | `verifyProofWith h root leaf prf = (root == reconstructWith h leaf prf)`. | `reconstructAppendWith`, `powerTwoSucc`, `justInj` | supporting lemmas. +| `buildGetLeaf` (Stage 1.1) +| constructor round-trip: `getLeafHash (buildMerkleTree hs) (finToNat i) = Just (index i hs)`. +| `Ochrance.Util.VectLemmas` (×5) +| reusable transport/append lemmas: `indexAppendLeft` / `indexAppendRight`, + `indexReplace`, `finToNatReplace`, `splitAtConcat`. | `roundtripManifest` + sub-codecs (`algoRT`, `modeRT`, `refsRT`, `mpolRT`, …) | grammar invertibility: `decodeManifest (encodeManifest m) = Just m`. | `SatisfiesMinimum` / `attestedSatisfiesLax` @@ -99,15 +105,24 @@ design change or a model downshift mid-stage. === Stage 1 — Merkle closure + crypto-binding interface [model: Opus] -. `buildMerkleTree` correctness: `getLeafHash (buildMerkleTree hs) i = Just (index i hs)`, - and the root-fold law relating `rootHashWith h (buildMerkleTree hs)` to `hs`. -. *IO↔pure bridge*: prove `verifyProofIO` / `rootHashBytesIO` compute the - `…With (blake3 combiner)` spec modulo the `Either` allocation-failure plumbing — - connecting the proven theorem to the *production* crypto path. -. *D2*: introduce `CollisionResistant h` and `merkleBinding` (stub/interface). +. *[DONE — 1.1]* `buildMerkleTree` ↔ `getLeafHash` round-trip: + `getLeafHash (buildMerkleTree hs) (finToNat i) = Just (index i hs)` + (`buildGetLeaf` in `Ochrance.Filesystem.MerkleBuild`, on the reusable + `Ochrance.Util.VectLemmas` lemmas). Machine-checked, axiom-free, on `main`. +. *[1.2] Root-fold law*: characterise `rootHashWith h (buildMerkleTree hs)` as a + deterministic fold over `hs` — "the root is a function of the leaves". Pure; + prerequisite of the binding argument. +. *[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".) +. *[1.4] D2*: introduce `CollisionResistant h` and state `merkleBinding` + (typed hypothesis / interface; discharged in Stage 4). + -WATCH-FOR: the `replace`-by-`powerTwoSucc` transport in `buildMerkleTree` may fight -the index lemma; if it forces a builder/API reshape, stop and surface the fork. +RESOLVED (was WATCH-FOR): the `replace`-by-`powerTwoSucc` transport in +`buildMerkleTree` was discharged *without* reshaping the builder — via the +`indexReplace` / `finToNatReplace` / `splitAtConcat` transport-cancellation lemmas +in `VectLemmas`. No API change was forced. === Stage 2 — Verify + Validator soundness [model: Opus → Sonnet if mechanical] @@ -122,7 +137,16 @@ propositional-over-decidable (document the boundary; do *not* reach for === Stage 3 — Repair correctness (L3, linear types) [model: Opus] -. `verify (repair s) = Valid` — the meaty linear-type theorem. +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. @@ -140,6 +164,78 @@ possible signature changes to `Repair.idr`. CLEAR = every intended theorem proven *or honestly bounded* (primitive walls documented, never faked), disposed tracks handed off, PRs landed. +== The IO↔pure bridge (estate-wide spine) + +The same device recurs at *every* IO boundary — Merkle (1.3), Verify (2.2), +Repair (3), signatures (4 / bounded). The shape is always: + + pure spec (proven) --[extensional-equality lemma]--> IO production path + (modulo `Either` + allocation-failure + + a typed crypto hypothesis) + +Treating this as *one* architectural pattern — not four ad-hoc stage items — is what +lets the proven backdrop reach production code *without ever faking the FFI*. The +typed crypto hypotheses (`CollisionResistant h`; `hashPairBlake3 a b` equals the +spec combiner) are introduced in Stage 1.4 and discharged-or-assumed explicitly, +never silently. It is also the mechanism that licenses optimisation (below). + +== Build-with-proofs discipline + +The invariant: *code never outstrips proofs*. Operationally — + +. A correctness-claiming `public export` symbol lands only when (a) it carries its + lemma in the same PR, or (b) it is explicitly `-- UNPROVEN:`-marked with a tracking + issue, or (c) it is a documented honestly-bounded wall. No silent (d). +. The `--total` CI build *is* the totality proof (already enforced) — a green build + is the floor, not the ceiling. +. *No proving stubs.* If an implementation is a placeholder (Repair today), make it + real or model it purely *first* — never point a theorem at a no-op. +. This ledger's proven-surface table is the source of truth; `README` / `TOPOLOGY` + must not claim beyond it. + +== Optimisation ledger (against the proven backdrop) + +Governing principle: *the proven surface is exactly the code you may optimise* — the +proof is the optimisation's regression contract. Keep the simple reference `R` +(proven), introduce optimised `F`, discharge `F x = R x`, and every theorem about `R` +transports to `F` by `rewrite`. Never optimise unproven code (nothing guards it). + +[cols="1,2,2,1",options="header"] +|=== +| Target | Optimisation | Guard | Status + +| `buildMerkleTree` +| bottom-up O(n) fold from the flat vector (vs. per-level `replace`/`splitAt`) +| `buildFast hs = buildMerkleTree hs` ⇒ `buildGetLeaf` transports +| unlocked now + +| `getLeafHash` +| thread a `Fin` index; drop Nat `minus`/`<` +| `getLeafFast t i = getLeafHash t (finToNat i)` +| unlocked now + +| `generateProof` / `reconstruct` +| difference-list / vector path (vs. List append per step) +| `reconstructAppendWith` + `merkleCorrectWith` +| unlocked now + +| root combiner +| real BLAKE3 in IO (vs. abstract `h`) +| the Stage 1.3 bridge lemma +| after 1.3 + +| A2ML production parser +| any fast String parser +| `roundtripManifest` + runtime `roundtripProperty` net +| bounded (prim. wall) + +| Repair (incremental / CoW) +| touch only broken blocks +| `verify (repair s) = Valid` +| after Stage 3 +|=== + == Honestly-bounded items (NOT failures — boundaries by design) * *Production-pipeline round-trip* (`parse . lex . serialize = Right m`) cannot