Skip to content

Commit 6ac2b0a

Browse files
hyperpolymathclaude
hyperpolymath
and
claude
committed
docs(trunk): deep-annotate Catalogue ABI + FFI
Adds README.adoc at the two trunk layers of the BoJ server: - src/abi/README.adoc — the 15-module Idris2 trunk, organised into four concentric rings: matrix axes (Protocol/Domain/Catalogue/Menu), runtime/cross-cutting (CartridgeDispatch BJ1, CredentialIsolation BJ2, Federation, Guardian), safety proofs (seven Safe*/Safety/SafetyLemmas modules), and the primitives the Zig FFI mirrors. - ffi/zig/src/README.adoc — the 14-file Zig FFI, grouped by function (core, federation/perimeter, reliability, orchestration) with authoritative per-file inline-test counts sourced from `grep -c '^test "'` (216 tests total; bench.zig contributes 0 by design — it is benchmarks, not tests). Both READMEs document: - what this layer means for cartridges downstream (why it is the trunk); - build/type-check entry point; - per-module roles sourced from the actual top-of-file docstrings; - trunk-wide invariants (totality, believe_me = 4 with all four named, mutex discipline, hardened enum conversion, bounds-checks-before- dereference, two-phase lock for blocking I/O); - test/proof surface; - read-first pointer so a reviewer can orient without source archaeology; - concrete D→C promotion gate. The ABI README pins `believe_me = 4` with locations (three in SafetyLemmas, one in SafeAPIKey line 152). The FFI README pins the 216-test count and names `bench.zig` as the intentional zero. These two READMEs close the trunk half of the CRG v2.0 "deep annotation" requirement flagged in docs/READINESS.md §4. The cartridge half landed in 68d6b1c. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
1 parent 68d6b1c commit 6ac2b0a

2 files changed

Lines changed: 260 additions & 0 deletions

File tree

‎ffi/zig/src/README.adoc‎

Lines changed: 135 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,135 @@
1+
// SPDX-License-Identifier: PMPL-1.0-or-later
2+
// Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
3+
= BoJ Server — Catalogue FFI (trunk)
4+
:orientation: deep
5+
6+
== Purpose
7+
8+
This is the **trunk** FFI of the BoJ server — the Zig runtime layer that
9+
mirrors the Idris2 ABI at `src/abi/Boj/` and exposes it over a C ABI so
10+
cartridges, the dynamic loader, and the adapter layer can all talk to the
11+
same facts. Cartridge-local `ffi/` directories (e.g.
12+
`cartridges/database-mcp/ffi/`) handle cartridge-specific state; **this**
13+
directory handles everything shared: the catalogue, cartridge loader,
14+
federation runtime, guardian, safety primitives, SLA tracking, community
15+
submissions, SDP perimeter, seam checks, readiness tests, coprocessor
16+
dispatch, end-to-end orchestration, and VeriSimDB backing store.
17+
18+
14 files, ~216 inline tests. This is where correctness is observed at
19+
runtime, while the proofs live upstairs in `src/abi/`.
20+
21+
== Build
22+
23+
[source,bash]
24+
----
25+
cd ffi/zig
26+
zig build # produces the shared library under zig-out/
27+
zig build test # runs all inline tests
28+
----
29+
30+
== Modules
31+
32+
Grouped by function. Inline test counts in parentheses are authoritative
33+
(`grep -c '^test "'` of the file).
34+
35+
=== Core
36+
37+
[cols="1,3"]
38+
|===
39+
| File | Role
40+
41+
| `catalogue.zig` (13 tests) | C-compatible bridge between the Idris2 proofs and the runtime. The FFI face of `Boj.Catalogue`.
42+
| `loader.zig` (14 tests) | Dynamic cartridge loader — hash verification, mount/unmount of cartridge shared libraries.
43+
| `safety.zig` (10 tests) | C-ABI exports for safe string operations (matches `Boj.Safety` + lemmas).
44+
| `verisimdb.zig` (18 tests) | Backing-store bridge — cartridge catalogue state, federation membership, order-ticket persistence.
45+
|===
46+
47+
=== Federation and perimeter
48+
49+
[cols="1,3"]
50+
|===
51+
| File | Role
52+
53+
| `federation.zig` (40 tests) | Umoja gossip protocol runtime — node handshake, heartbeat, hash attestation.
54+
| `sdp.zig` (10 tests) | Software Defined Perimeter — zero-trust perimeter around federation nodes.
55+
| `community.zig` (11 tests) | Community cartridge submission pipeline (Ayo menu tier).
56+
|===
57+
58+
=== Reliability
59+
60+
[cols="1,3"]
61+
|===
62+
| File | Role
63+
64+
| `guardian.zig` (12 tests) | Resource monitoring, preemptive thresholds, circuit breaker. Mirrors `Boj.Guardian`.
65+
| `sla.zig` (11 tests) | Per-cartridge and system-level SLA metrics.
66+
| `readiness.zig` (28 tests) | Component Readiness Grade verification — runtime evidence for the CRG table in `docs/READINESS.md`.
67+
| `seams.zig` (32 tests) | Integration-seam contract checks (panic-attack-inspired `diagnostics.rs` pattern).
68+
|===
69+
70+
=== Orchestration
71+
72+
[cols="1,3"]
73+
|===
74+
| File | Role
75+
76+
| `coprocessor.zig` (14 tests) | Axiom.jl-style GPU/TPU/FPGA offload dispatch.
77+
| `e2e_order.zig` (3 tests) | End-to-end order-ticket orchestration at the Zig layer (no external server required).
78+
| `bench.zig` (0 tests) | Benchmarks — not tests. Measures cartridge lifecycle latency. Run with `zig build bench`, not `zig build test`.
79+
|===
80+
81+
== Invariants (trunk-wide)
82+
83+
* **Every C-ABI export uses a named error-code enum.** Negative return
84+
values carry documented meanings, matching what the Idris2 ABI expects.
85+
* **Mutex discipline** is file-local — each file owns its own global
86+
`mutex`, acquired at C-ABI entry via `mutex.lock(); defer
87+
mutex.unlock();`. No file holds two mutexes at once.
88+
* **Hardened enum conversions.** C-ABI exports that take `c_int`
89+
enum-valued arguments use `std.meta.intToEnum` (returns an error on
90+
invalid values) rather than `@enumFromInt` (panics). Exceptions must be
91+
justified inline.
92+
* **Bounds checks before dereference.** Every `(ptr, len)` pair is
93+
validated for zero-length and buffer-overflow before any `@memcpy` or
94+
slice access. `SAFETY:` comments annotate the checks.
95+
* **Two-phase lock pattern for blocking I/O.** Functions that call into
96+
`curl` or other blocking FFI release the mutex before the call and
97+
re-validate state on re-acquisition.
98+
* **No allocator leaks.** `defer *.deinit(alloc)` / `defer free(…)` on
99+
every allocation path. Verified by compile with
100+
`-Dstandalone_tests=true`.
101+
102+
== Test/proof surface
103+
104+
216 inline `test "..."` blocks across 13 files (see per-module counts
105+
above). `bench.zig` contributes zero tests by design — its contents are
106+
benchmarks. Run `zig build test` for the whole suite; it is the primary
107+
runtime evidence for Grade D assertions in `docs/READINESS.md`.
108+
109+
End-to-end orchestration lives in `e2e_order.zig` and is run as part of
110+
the same `zig build test` sweep.
111+
112+
== Read-first
113+
114+
. `catalogue.zig` — the runtime face of the Idris2 matrix. Read alongside
115+
`src/abi/Boj/Catalogue.idr`.
116+
. `loader.zig` — cartridge mount/unmount with hash verification; the path
117+
every cartridge travels at boot.
118+
. `safety.zig` — the cross-cutting string-safety primitives the rest of
119+
the FFI imports.
120+
. `federation.zig` — largest module (40 tests) and the richest
121+
concurrency story.
122+
. `readiness.zig` — the tests here are the direct runtime evidence for
123+
`docs/READINESS.md`. Any grade change should be accompanied by a test
124+
change here.
125+
126+
== Promotion gate
127+
128+
This trunk is graded D in `docs/READINESS.md`. Lifting to C requires:
129+
130+
. Active dogfood entries in `docs/practice/DOGFOOD-LOG.adoc` showing
131+
these exports called in anger from a real cartridge load path (not just
132+
from `zig build test`).
133+
. No open `SAFETY:` TODOs in the 14 files.
134+
. A consumer outside the home-context test loop (adapter driving the FFI
135+
under real protocol load).

‎src/abi/README.adoc‎

Lines changed: 125 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,125 @@
1+
// SPDX-License-Identifier: PMPL-1.0-or-later
2+
// Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
3+
= BoJ Server — Catalogue ABI (trunk)
4+
:orientation: deep
5+
6+
== Purpose
7+
8+
This is the **trunk** ABI of the BoJ server: the formally verified Idris2
9+
layer that every cartridge inherits from. The cartridge-local `abi/`
10+
directories (e.g. `cartridges/database-mcp/abi/`) define per-cartridge state
11+
machines and tool catalogues; **this** directory defines the shared
12+
vocabulary those cartridges compose into — the 2D capability matrix, the
13+
cartridge dispatch proofs, the credential-isolation model, and the safety
14+
lemmas that back every safe-HTTP / safe-WebSocket / safe-API-key /
15+
safe-prompt-injection property in the whole server.
16+
17+
If the cartridge-local ABIs are leaves, this is the stem.
18+
19+
== Package
20+
21+
Defined by `boj.ipkg`. Type-check with:
22+
23+
[source,bash]
24+
----
25+
cd src/abi
26+
idris2 --check boj.ipkg
27+
----
28+
29+
Depends only on `base` and `contrib`. Every module is `%default total`.
30+
31+
== Modules
32+
33+
The 15 modules under `Boj/` fall into four concentric rings.
34+
35+
=== Ring 1 — the matrix (single source of truth)
36+
37+
[cols="1,3"]
38+
|===
39+
| Module | Role
40+
41+
| `Boj.Protocol` | The **columns** of the 2D capability matrix — wire protocols cartridges can expose (MCP, REST, gRPC, GraphQL, etc.).
42+
| `Boj.Domain` | The **rows** — classes of infrastructure capability (database, git, cloud, …).
43+
| `Boj.Catalogue` | The matrix itself. Every cartridge occupies one `(Protocol × Domain)` cell and must pass the `IsUnbreakable` proof before activation.
44+
| `Boj.Menu` | The Teranga menu — public face of the catalogue. AI agents ("the Maitre D'") present this to users.
45+
|===
46+
47+
=== Ring 2 — runtime and cross-cutting concerns
48+
49+
[cols="1,3"]
50+
|===
51+
| Module | Role
52+
53+
| `Boj.CartridgeDispatch` | Requirement **BJ1** — proves three core dispatch invariants (type-safe dispatch, exhaustive routing, no lost traffic). Not yet listed in `boj.ipkg` `modules`; treat as WIP trunk.
54+
| `Boj.CredentialIsolation` | Requirement **BJ2** — per-cartridge credential-store isolation modelled at the type level. Each vault partition is indexed by cartridge name; a token must carry the matching index to read.
55+
| `Boj.Federation` | Umoja federated network protocol. Community nodes volunteer compute (Tor/IPFS-style) and prove identity by hash attestation.
56+
| `Boj.Guardian` | Resource-aware failure tolerance, preemptive thresholds, circuit breaker, self-diagnostics.
57+
|===
58+
59+
=== Ring 3 — safety proofs (every "Safe*" module)
60+
61+
[cols="1,3"]
62+
|===
63+
| Module | Role
64+
65+
| `Boj.Safety` | Top-level formally verified input validation via proven-library patterns.
66+
| `Boj.SafetyLemmas` | Foundational lemmas over `List Char`, `Nat`, `String` that the `Safe*` modules reuse.
67+
| `Boj.SafeHTTP` | HTTP request/response proofs: valid methods, safe headers, status code ranges, content-type validation. Commentary pins "All proofs are constructive. Zero believe_me. Zero postulates." (line 15).
68+
| `Boj.SafeCORS` | CORS policy enforcement.
69+
| `Boj.SafeWebSocket` | WebSocket transport safety.
70+
| `Boj.SafeAPIKey` | API key handling.
71+
| `Boj.SafePromptInjection` | Prompt-injection defences.
72+
|===
73+
74+
=== Ring 4 — FFI primitives
75+
76+
The primitives exported by the trunk that the Zig FFI at `ffi/zig/src/`
77+
mirrors byte-for-byte — transition predicates, tool requirements, and the
78+
matrix-cell identifier scheme.
79+
80+
== Invariants (trunk-wide)
81+
82+
* **`%default total`** at every module top. Partial definitions are a
83+
review blocker across the whole trunk.
84+
* **`believe_me` budget is 4 and declared.** All four live in this trunk:
85+
* `Boj.SafetyLemmas`: `charEqSound`, `charEqSym`, `unpackLength` — three
86+
axiomatic primitives covering discharge of `Char`/`String` equalities
87+
that the Idris2 prelude does not expose constructively.
88+
* `Boj.SafeAPIKey`: `logSafeBounded` at line 152 — bound on logger
89+
safe-substring length.
90+
Any growth in this count triggers the estate-wide believe_me sweep rule.
91+
* **Zero `assert_total`, zero `postulate`, zero `Admitted`, zero `sorry`**
92+
across the trunk (verified by grep: count = 0).
93+
* **Module DAG is acyclic.** `SafeHTTP`/`SafeCORS`/`SafeWebSocket`/
94+
`SafeAPIKey`/`SafePromptInjection`/`Safety` all sit below `SafetyLemmas`;
95+
nothing in `SafetyLemmas` imports back upward.
96+
97+
== Test/proof surface
98+
99+
Type-check only — `idris2 --check boj.ipkg`. The runtime evidence for these
100+
proofs lives in the FFI's test suite at `ffi/zig/src/` (216 inline `test`
101+
blocks across 13 files; see `ffi/zig/src/README.adoc`).
102+
103+
== Read-first
104+
105+
. `Boj/Protocol.idr` + `Boj/Domain.idr` — matrix axes. Short, definitional.
106+
. `Boj/Catalogue.idr` — what it means to be a cartridge cell, and
107+
`IsUnbreakable`.
108+
. `Boj/SafetyLemmas.idr` — the four (three here, one in `SafeAPIKey`)
109+
axiomatic leaves of the proof tree. Everything else refers to them.
110+
. `Boj/CartridgeDispatch.idr` (BJ1) and `Boj/CredentialIsolation.idr` (BJ2)
111+
— the two named requirements; read after you know the matrix.
112+
. Safe* modules last — they are leaves that compose the rest.
113+
114+
== Promotion gate
115+
116+
This trunk is graded D in `docs/READINESS.md`. Lifting to C requires:
117+
118+
. Four `believe_me` sites justified and cross-referenced from
119+
`SafetyLemmas` docstrings (the three lemmas are already documented as
120+
axiomatic primitives; `logSafeBounded` needs the same treatment).
121+
. `CartridgeDispatch.idr` added to `boj.ipkg modules` once BJ1 is ready
122+
to be consumed.
123+
. Dogfood evidence in `docs/practice/DOGFOOD-LOG.adoc` showing the trunk
124+
being used in anger (cartridge load → type-check → matrix lookup round
125+
trip) in the home context.

0 commit comments

Comments
 (0)