Skip to content

Commit 0785a9f

Browse files
claudehyperpolymath
claude
authored and
hyperpolymath
committed
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
1 parent 81a11e2 commit 0785a9f

2 files changed

Lines changed: 135 additions & 25 deletions

File tree

‎TOPOLOGY.md‎

Lines changed: 29 additions & 15 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
<!-- SPDX-License-Identifier: MPL-2.0 -->
22
<!-- TOPOLOGY.md — Project architecture map and completion dashboard -->
3-
<!-- Last updated: 2026-02-19 -->
3+
<!-- Last updated: 2026-06-17 -->
44

55
# Ochránce — Project Topology
66

@@ -51,27 +51,36 @@
5151

5252
## Completion Dashboard
5353

54+
> Percentages track **proof / verification completeness** — the honest axis for a
55+
> verification framework — **not** "code exists". `docs/PROOFS.adoc` is the
56+
> authoritative ledger; this dashboard only summarises it. Where an implementation
57+
> exists but its correctness is unproven (or is a stub), the bar reflects the
58+
> *proof*, not the code.
59+
5460
```
55-
COMPONENT STATUS NOTES
56-
───────────────────────────────── ────────────────── ─────────────────────────────────
61+
COMPONENT STATUS NOTES (proof / verification axis)
62+
─────────────────────────────────── ────────────── ────────────────────────────────────────────
5763
CORE VERIFICATION (IDRIS2)
58-
Merkle Tree Implementation ██████████ 100% Size-indexed proofs stable
59-
Linear Type Repair ████████░░ 80% Use-after-repair prevention
60-
A2ML Parser ██████████ 100% Attestation DSL verified
61-
VerifiedSubsystem Interface ██████████ 100% Abstract interface stable
64+
Merkle soundness + round-trip ███████░░░ 70% merkleCorrect(With) + buildGetLeaf proven
65+
Merkle completeness + binding ░░░░░░░░░░ 0% converse + CollisionResistant (Stage 1.4/4)
66+
A2ML parser + reference round-trip ███████░░░ 70% total; ref-codec proven; prod pipeline runtime-only
67+
Verify soundness ░░░░░░░░░░ 0% verify success ⇏ a proof yet (Stage 2)
68+
Linear-type Repair ██░░░░░░░░ 20% IMPL IS A STUB (no block I/O); unproven (Stage 3)
69+
VerifiedSubsystem law █████░░░░░ 50% interface + FSState instance; law unproven (Stage 3)
70+
Progressive assurance ███████░░░ 70% attestedSatisfiesLax proven; monotonicity (Stage 4)
6271
6372
SYSTEM & EXTERNAL
64-
Zig FFI Bridge ██████████ 100% Stable C ABI bridge
65-
ECHIDNA Integration ██████░░░░ 60% Proof synthesis refining
66-
Filesystem Module ████████░░ 80% Reference implementation stable
73+
Zig crypto (BLAKE3/SHA/Ed25519) ███████░░░ 70% implemented + known-answer-vector tested in Zig
74+
Crypto linked into verify flow ██░░░░░░░░ 20% NOT linked; Idris-side stubs still live (#39)
75+
ECHIDNA integration █░░░░░░░░░ 10% design types only; FFI entirely stubbed
6776
6877
REPO INFRASTRUCTURE
69-
Justfile Automation ██████████ 100% Standard build/verify tasks
70-
.machine_readable/ ██████████ 100% STATE tracking active
71-
Idris2 .ipkg ██████████ 100% Package definitions verified
78+
Justfile automation ██████████ 100% build / verify tasks
79+
.machine_readable/ ██████████ 100% STATE tracking active
80+
Idris2 .ipkg / totality gate ██████████ 100% 19 core modules; --total build green
7281
73-
─────────────────────────────────────────────────────────────────────────────
74-
OVERALL: ████████░░ ~80% Framework stable, ML maturing
82+
────────────────────────────────────────────────────────────────────────────────────────────────
83+
OVERALL (proof axis): ████░░░░░░ ~40% Stage 1.1 done; 1.2–4 open. See docs/PROOFS.adoc.
7584
```
7685

7786
## Key Dependencies
@@ -94,3 +103,8 @@ This file is maintained by both humans and AI agents. When updating:
94103

95104
Progress bars use: `█` (filled) and `░` (empty), 10 characters wide.
96105
Percentages: 0%, 10%, 20%, ... 100% (in 10% increments).
106+
107+
The bars track **proof / verification completeness** against `docs/PROOFS.adoc`
108+
(the authoritative ledger), not whether code merely exists. Do not raise a bar to
109+
100% on the strength of an implementation alone — a component is "done" only when
110+
its correctness is proven or honestly bounded per the ledger.

‎docs/PROOFS.adoc‎

Lines changed: 106 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -68,7 +68,8 @@ Three repositories are in scope. "Verification" means something different in eac
6868

6969
== Current proof state (ochrance, canonical)
7070

71-
The core is *clean*: all 24 modules carry `%default total`; zero
71+
The core is *clean*: all 19 `ochrance-core` modules carry `%default total` (the
72+
`src/abi/` tree adds the ABI modules separately); zero
7273
`believe_me` / `assert_*` / `postulate` / holes / `partial` on any proof symbol.
7374

7475
.Proven, machine-checked (axiom-free)
@@ -83,6 +84,11 @@ The core is *clean*: all 24 modules carry `%default total`; zero
8384
| `verifyProofWith h root leaf prf = (root == reconstructWith h leaf prf)`.
8485
| `reconstructAppendWith`, `powerTwoSucc`, `justInj`
8586
| supporting lemmas.
87+
| `buildGetLeaf` (Stage 1.1)
88+
| constructor round-trip: `getLeafHash (buildMerkleTree hs) (finToNat i) = Just (index i hs)`.
89+
| `Ochrance.Util.VectLemmas` (×5)
90+
| reusable transport/append lemmas: `indexAppendLeft` / `indexAppendRight`,
91+
`indexReplace`, `finToNatReplace`, `splitAtConcat`.
8692
| `roundtripManifest` + sub-codecs (`algoRT`, `modeRT`, `refsRT`, `mpolRT`, …)
8793
| grammar invertibility: `decodeManifest (encodeManifest m) = Just m`.
8894
| `SatisfiesMinimum` / `attestedSatisfiesLax`
@@ -99,15 +105,24 @@ design change or a model downshift mid-stage.
99105

100106
=== Stage 1 — Merkle closure + crypto-binding interface [model: Opus]
101107

102-
. `buildMerkleTree` correctness: `getLeafHash (buildMerkleTree hs) i = Just (index i hs)`,
103-
and the root-fold law relating `rootHashWith h (buildMerkleTree hs)` to `hs`.
104-
. *IO↔pure bridge*: prove `verifyProofIO` / `rootHashBytesIO` compute the
105-
`…With (blake3 combiner)` spec modulo the `Either` allocation-failure plumbing —
106-
connecting the proven theorem to the *production* crypto path.
107-
. *D2*: introduce `CollisionResistant h` and `merkleBinding` (stub/interface).
108+
. *[DONE — 1.1]* `buildMerkleTree` ↔ `getLeafHash` round-trip:
109+
`getLeafHash (buildMerkleTree hs) (finToNat i) = Just (index i hs)`
110+
(`buildGetLeaf` in `Ochrance.Filesystem.MerkleBuild`, on the reusable
111+
`Ochrance.Util.VectLemmas` lemmas). Machine-checked, axiom-free, on `main`.
112+
. *[1.2] Root-fold law*: characterise `rootHashWith h (buildMerkleTree hs)` as a
113+
deterministic fold over `hs` — "the root is a function of the leaves". Pure;
114+
prerequisite of the binding argument.
115+
. *[1.3] IO↔pure bridge*: prove `verifyProofIO` / `rootHashBytesIO` compute the
116+
`…With (hashPairBlake3 …)` spec modulo the `Either` allocation-failure plumbing,
117+
against a typed combiner-equality hypothesis — connecting the proven theorem to
118+
the *production* crypto path. (The estate-wide spine; see "The IO↔pure bridge".)
119+
. *[1.4] D2*: introduce `CollisionResistant h` and state `merkleBinding`
120+
(typed hypothesis / interface; discharged in Stage 4).
108121
+
109-
WATCH-FOR: the `replace`-by-`powerTwoSucc` transport in `buildMerkleTree` may fight
110-
the index lemma; if it forces a builder/API reshape, stop and surface the fork.
122+
RESOLVED (was WATCH-FOR): the `replace`-by-`powerTwoSucc` transport in
123+
`buildMerkleTree` was discharged *without* reshaping the builder — via the
124+
`indexReplace` / `finToNatReplace` / `splitAtConcat` transport-cancellation lemmas
125+
in `VectLemmas`. No API change was forced.
111126

112127
=== Stage 2 — Verify + Validator soundness [model: Opus → Sonnet if mechanical]
113128

@@ -122,7 +137,16 @@ propositional-over-decidable (document the boundary; do *not* reach for
122137

123138
=== Stage 3 — Repair correctness (L3, linear types) [model: Opus]
124139

125-
. `verify (repair s) = Valid` — the meaty linear-type theorem.
140+
PRECONDITION (surfaced at Compaction 2): `repair` is currently a *stub* —
141+
`repairBlock` (`Repair.idr`) updates the hash map but does **not** read or write
142+
block data. Proving `verify (repair s) = Valid` against a no-op would be vacuous or
143+
false. DECISION (recommended): introduce a pure
144+
`repairPure : FSState -> Manifest -> FSState` that genuinely reconstructs the hash
145+
map, prove correctness over *that*, and make the IO `repair` a proven-equivalent
146+
shell (the IO↔pure pattern). Alternative: leave repair honestly-bounded until real
147+
block-I/O lands (defers the linear-type theorem).
148+
149+
. `verifyPure (repairPure s m) m = True` — the meaty (now well-founded) theorem.
126150
. Repair idempotence as a *proof* (today only a property test).
127151
. Harvest framework's mode-indexed Interface; state the `VerifiedSubsystem` law
128152
`verify (repair s m) m = Right …` and prove the FSState instance satisfies it.
@@ -140,6 +164,78 @@ possible signature changes to `Repair.idr`.
140164
CLEAR = every intended theorem proven *or honestly bounded* (primitive walls
141165
documented, never faked), disposed tracks handed off, PRs landed.
142166

167+
== The IO↔pure bridge (estate-wide spine)
168+
169+
The same device recurs at *every* IO boundary — Merkle (1.3), Verify (2.2),
170+
Repair (3), signatures (4 / bounded). The shape is always:
171+
172+
pure spec (proven) --[extensional-equality lemma]--> IO production path
173+
(modulo `Either`
174+
allocation-failure +
175+
a typed crypto hypothesis)
176+
177+
Treating this as *one* architectural pattern — not four ad-hoc stage items — is what
178+
lets the proven backdrop reach production code *without ever faking the FFI*. The
179+
typed crypto hypotheses (`CollisionResistant h`; `hashPairBlake3 a b` equals the
180+
spec combiner) are introduced in Stage 1.4 and discharged-or-assumed explicitly,
181+
never silently. It is also the mechanism that licenses optimisation (below).
182+
183+
== Build-with-proofs discipline
184+
185+
The invariant: *code never outstrips proofs*. Operationally —
186+
187+
. A correctness-claiming `public export` symbol lands only when (a) it carries its
188+
lemma in the same PR, or (b) it is explicitly `-- UNPROVEN:`-marked with a tracking
189+
issue, or (c) it is a documented honestly-bounded wall. No silent (d).
190+
. The `--total` CI build *is* the totality proof (already enforced) — a green build
191+
is the floor, not the ceiling.
192+
. *No proving stubs.* If an implementation is a placeholder (Repair today), make it
193+
real or model it purely *first* — never point a theorem at a no-op.
194+
. This ledger's proven-surface table is the source of truth; `README` / `TOPOLOGY`
195+
must not claim beyond it.
196+
197+
== Optimisation ledger (against the proven backdrop)
198+
199+
Governing principle: *the proven surface is exactly the code you may optimise* — the
200+
proof is the optimisation's regression contract. Keep the simple reference `R`
201+
(proven), introduce optimised `F`, discharge `F x = R x`, and every theorem about `R`
202+
transports to `F` by `rewrite`. Never optimise unproven code (nothing guards it).
203+
204+
[cols="1,2,2,1",options="header"]
205+
|===
206+
| Target | Optimisation | Guard | Status
207+
208+
| `buildMerkleTree`
209+
| bottom-up O(n) fold from the flat vector (vs. per-level `replace`/`splitAt`)
210+
| `buildFast hs = buildMerkleTree hs` ⇒ `buildGetLeaf` transports
211+
| unlocked now
212+
213+
| `getLeafHash`
214+
| thread a `Fin` index; drop Nat `minus`/`<`
215+
| `getLeafFast t i = getLeafHash t (finToNat i)`
216+
| unlocked now
217+
218+
| `generateProof` / `reconstruct`
219+
| difference-list / vector path (vs. List append per step)
220+
| `reconstructAppendWith` + `merkleCorrectWith`
221+
| unlocked now
222+
223+
| root combiner
224+
| real BLAKE3 in IO (vs. abstract `h`)
225+
| the Stage 1.3 bridge lemma
226+
| after 1.3
227+
228+
| A2ML production parser
229+
| any fast String parser
230+
| `roundtripManifest` + runtime `roundtripProperty` net
231+
| bounded (prim. wall)
232+
233+
| Repair (incremental / CoW)
234+
| touch only broken blocks
235+
| `verify (repair s) = Valid`
236+
| after Stage 3
237+
|===
238+
143239
== Honestly-bounded items (NOT failures — boundaries by design)
144240

145241
* *Production-pipeline round-trip* (`parse . lex . serialize = Right m`) cannot

0 commit comments

Comments
 (0)