Skip to content

docs(proofs): record Stage 1.1; add optimisation ledger + build-with-proofs discipline; truth-fix TOPOLOGY #48

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
hyperpolymath merged 1 commit into from
Jun 17, 2026
Merged

docs(proofs): record Stage 1.1; add optimisation ledger + build-with-proofs discipline; truth-fix TOPOLOGY #48

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
44 changes: 29 additions & 15 deletions TOPOLOGY.md
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
<!-- SPDX-License-Identifier: MPL-2.0 -->
<!-- TOPOLOGY.md — Project architecture map and completion dashboard -->
<!-- Last updated: 2026-02-19 -->
<!-- Last updated: 2026-06-17 -->

# Ochránce — Project Topology

Expand Down Expand Up @@ -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
Expand All @@ -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.
116 changes: 106 additions & 10 deletions docs/PROOFS.adoc
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand All @@ -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`
Expand All @@ -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]

Expand All @@ -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.
Expand All @@ -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
Expand Down
Loading