Skip to content

Commit 648de4d

Browse files
docs(planning): 2026-06-13 session artifacts — proof checkpoint + owner-decision batch (#217)
Docs-only. Two related planning/verification artifacts from the 2026-06-13 session. ## 1. `PROOF-NEEDS.md` — build-backed checkpoint A dated re-verification on a from-source toolchain (Idris2 0.8.0 via Chez 9.5.8 + libgmp), so the next reader gets a built number, not a desk-read: | Check | Result | |---|---| | `idris2 --typecheck src/abi/boj.ipkg` | 17/17, exit 0 | | `scripts/typecheck-proofs.sh` | **PASS=105 FAIL=0** (core + all 104 cartridge ABIs) | | `scripts/check-trusted-base.sh` | PASS — exactly 5 class-(J) axioms | Independently corroborated by a `panic-attack assail` scan (MPL-2.0, built from source) flagging the same 5 `believe_me` and nothing else proof-shaped. Broader than the 2026-06-03 entry (core-only). Axiom budget and theorems unchanged. ## 2. `docs/planning/owner-decisions-2026-06-13.adoc` — six rulings Frames the critical-chain plan's §13 decision batch as a single rule-on-it document — each blocked on owner judgement, each with options + recommendation + the gate it unblocks: - **D1** licence drift (`package.json` AGPL vs MPL-2.0 everywhere else; #186) — held flag-only per the estate licence guardrail - **D2** auth posture (G3) — dual loopback/gateway model recommended - **D3** tier vocabulary (G5) — two repos define Teranga/Shield/Ayo incompatibly; `feedback-mcp` (the one real cartridge) is mislabelled `Ayo` - **D4** Golden Dozen slate (G2 keystone) — confirm/swap the 12 - **D5** version reset (G6) — `0.4.6/0.4.7/1.1.0-wip` split → `0.9.0 "honest beta"` - **D6** GEMINI.md — **resolved to confirm-only**: it IS referenced by `gemini-extension.json:17` (`contextFileName`), so #199's "delete" is a false positive Facts were verified against `main` first so each is a decision, not homework. Nothing in the batch is acted on until ruled; D1 specifically stays a flag, never an auto-PR. https://claude.ai/code/session_01PRi6uSn6qucCMCCy7mqUr4 --------- Co-authored-by: Claude <noreply@anthropic.com>
1 parent cb021c4 commit 648de4d

2 files changed

Lines changed: 241 additions & 0 deletions

File tree

PROOF-NEEDS.md

Lines changed: 23 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -10,6 +10,29 @@
1010
> greps. Keep both in sync when the marker count in
1111
> `src/abi/Boj/SafetyLemmas.idr` changes.
1212
13+
## Build Verification (2026-06-13) — full sweep, freshly built toolchain
14+
15+
Re-verified end-to-end on a clean machine with a from-source toolchain
16+
(Idris2 0.8.0 bootstrapped via Chez Scheme 9.5.8 + libgmp), not a
17+
desk-read of the prior entry. Three checks, all green:
18+
19+
- **Core ABI:** `cd src/abi && idris2 --typecheck boj.ipkg` → 17/17
20+
modules clean, exit 0 (~6.5 s).
21+
- **Full proof gate:** `bash scripts/typecheck-proofs.sh`**PASS=105
22+
FAIL=0** (core package + all 104 cartridge ABIs) under the pinned
23+
toolchain (~80 s). This is broader than the 2026-06-03 entry, which
24+
exercised only the core package.
25+
- **Trusted base:** `bash scripts/check-trusted-base.sh` → PASS,
26+
**exactly 5** sanctioned class-(J) axioms in `SafetyLemmas.idr`, zero
27+
undocumented unsound constructs. Independently corroborated by a
28+
`panic-attack assail` scan (MPL-2.0, built from source), which flags
29+
the same 5 `believe_me` as `ProofDrift` and nothing else proof-shaped.
30+
31+
The axiom budget and theorem statements are unchanged from the
32+
2026-06-03 entry; this checkpoint records that the **full cartridge
33+
sweep** (not just the core package) compiles, so a future reader sees a
34+
build-backed number rather than an inherited claim.
35+
1336
## Build Verification (2026-06-03)
1437

1538
The full core ABI package now type-checks under the pinned toolchain
Lines changed: 218 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,218 @@
1+
// SPDX-License-Identifier: MPL-2.0
2+
// SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
3+
4+
= Owner-decision batch — six rulings that unblock v1 gates
5+
:toc: preamble
6+
:icons: font
7+
8+
*Date:* 2026-06-13 ·
9+
*Source:* `docs/planning/v1-critical-chain-2026-06-11.adoc` §13 (the
10+
≤2-hour decision batch). ·
11+
*Purpose:* each item below is blocked on a judgement only the owner can
12+
make. They are framed — options, recommendation, and what each unblocks
13+
— so they can be ruled on in one sitting. Four are confirm-or-adjust;
14+
two (D1 licence, D3 tiers) genuinely need the owner's intent.
15+
16+
*How to use:* write your call on the `RULE:` line of each. Nothing in
17+
this batch is acted on until you do — D1 in particular is held under the
18+
estate licence guardrail (flag-only, never auto-PR).
19+
20+
[NOTE]
21+
====
22+
Facts verified on `main` @ 2026-06-13 so these are decisions, not
23+
homework: `package.json:5` = `AGPL-3.0-or-later`; versions split
24+
`0.4.6` (CITATION.cff) / `0.4.7` (package/jsr/gemini-extension) /
25+
`1.1.0-wip` (STATE); `gemini-extension.json:17` *does* set
26+
`"contextFileName": "GEMINI.md"`; cartridges-repo tiers = 129 Ayo / 10
27+
Teranga / 0 Shield, and `feedback-mcp` (the one verified-real cartridge)
28+
is labelled `Ayo`.
29+
====
30+
31+
== D1 — Licence drift (`package.json`) — unblocks G6
32+
33+
*Question.* `package.json` declares `AGPL-3.0-or-later`; the root
34+
`LICENSE`, every SPDX header, and the README badge say `MPL-2.0`. Which
35+
is correct for boj-server?
36+
37+
*Why owner-only.* The estate licence policy is the highest-priority
38+
guardrail: licence changes are manual, owner-approved, never
39+
agent-swept. This is a flag, not a PR. The classification turns on one
40+
fact only you hold: *did anyone other than you author boj-server?*
41+
42+
[cols="1,4"]
43+
|===
44+
| ▶ *A (recommended)* | boj-server is sole-owner ⇒ `MPL-2.0`. Fix the
45+
single outlier line in `package.json`. Matches LICENSE + all SPDX +
46+
badge + estate default for sole repos.
47+
| B | boj-server is shared-with-Joshua ⇒ `AGPL-3.0-or-later`. Then the
48+
*rest* of the repo (LICENSE, ~all headers) is the drift, not
49+
package.json — a much larger correction.
50+
|===
51+
52+
Recommendation A: nothing in the repo's history or `CODEOWNERS` suggests
53+
co-authorship, and AGPL is the estate's "shared with son" category
54+
(idaptik, paint-type), which boj-server is not listed under.
55+
56+
`RULE: _______________________________________________`
57+
58+
== D2 — Auth posture for v1 — unblocks G3
59+
60+
*Question.* `POST /cartridge/:name/invoke` has no HTTP-layer caller auth
61+
(`docs/AUTH-DESIGN.adoc`, open since April). Confirm the v1 model.
62+
63+
*Why owner-only.* It sets what "exposed boj-server" means for every
64+
operator and what credentials can cross a node boundary — a product +
65+
trust decision, not an implementation detail.
66+
67+
[cols="1,4"]
68+
|===
69+
| ▶ *A (recommended)* | *Dual posture.* (a) Local/single-user default:
70+
loopback bind (already landed, three independent layers) + no ceremony.
71+
(b) Exposed/operator mode: the HCG tier-2 sidecar derives
72+
`X-Trust-Level` (mTLS or bearer); BoJ enforces via the existing
73+
`TrustPolicy`, flipped from "read" to "require" for non-loopback
74+
callers. Credential forwarding capped at *Options A+B* — keyed
75+
cartridges stay local; volunteer nodes never receive your tokens
76+
(privacy by construction). RGTV broker (Option C) is post-v1.
77+
| B | Same, but pull credential-forwarding Option C (RGTV) into v1 —
78+
adds a broker build to the critical path; lets keyed cartridges run on
79+
remote nodes.
80+
| C | Loopback-only for v1; defer all exposed-mode auth. Simplest, but
81+
drops the "host for your community" story to local-only.
82+
|===
83+
84+
Recommendation A: no new mechanism needed (HCG + TrustPolicy exist); the
85+
honest limitation ("keyed cartridges aren't delegatable in v1") is a
86+
feature to advertise, not a gap to hide.
87+
88+
`RULE: _______________________________________________`
89+
90+
== D3 — Tier vocabulary — unblocks G5 (and must precede community open)
91+
92+
*Question.* What do Teranga / Shield / Ayo *mean*? Two repos define them
93+
incompatibly, and the flagship cartridge is mislabelled under either
94+
reading.
95+
96+
* boj-server README + ADR-0008: an *assurance* ladder — Teranga =
97+
formally verified, Shield = security-reviewed, Ayo = community/unverified
98+
(promotion Ayo→Shield→Teranga).
99+
* cartridges-repo de facto: 129 `Ayo` / 10 `Teranga` / 0 `Shield`, used
100+
as *provenance/default* — and `feedback-mcp`, the only proof-carrying,
101+
verified-real cartridge, sits in `Ayo` (the lowest tier). Backwards
102+
under the README's own "trust tiers" wording.
103+
104+
*Why owner-only.* The tier names are cultural terms (Yoruba/Swahili) with
105+
intended meaning per `docs/CULTURAL-RESPECT.adoc`; the canonical
106+
semantics are yours to set.
107+
108+
[cols="1,4"]
109+
|===
110+
| ▶ *A (recommended)* | *Assurance semantics* (adopt the README/ADR-0008
111+
ladder as canonical). Tier == how verified. Mechanical fix: `feedback-mcp`
112+
→ Teranga; all others stay Ayo until they earn promotion through the
113+
truthfulness + proof gates. Tier then carries the *same truth the
114+
honesty programme already enforces*, and Teranga = "the proven work we
115+
offer as hospitality" keeps the cultural reading.
116+
| B | *Provenance semantics* (first-party vs community), assurance tracked
117+
on a separate field. More relabelling; divorces the tier badge from
118+
trust.
119+
| C | *Two orthogonal axes* (provenance × assurance). Cleanest
120+
conceptually, but a schema change + full re-tagging — heavier than v1
121+
needs.
122+
|===
123+
124+
Recommendation A: it makes the tier field mean what users assume it
125+
means, matches the one promotion ladder already written down, and is a
126+
near-mechanical relabel rather than a schema change. Canonicalise in
127+
`hyperpolymath/standards`, mirror into both repos.
128+
129+
`RULE: _______________________________________________`
130+
131+
== D4 — The Golden Dozen slate — unblocks G2 (the keystone)
132+
133+
*Question.* Confirm or swap the 12 cartridges that become the v1 product
134+
surface (made real via the Foundry, gated by the truthfulness probe).
135+
136+
[cols="1,4"]
137+
|===
138+
| ▶ *Proposed (recommended)* |
139+
*Wave 1 — credential-free, CI-provable in plain runners:* `duckdb-mcp`,
140+
`local-memory-mcp`, `hesiod-mcp`, `model-router-mcp` (canonical JS-only
141+
path), `container-mcp` (local Podman), `git-mcp` (local repo ops). +
142+
*Wave 2 — token/secret-gated, E2E via CI secrets/service containers:*
143+
`github-api-mcp`, `gitlab-api-mcp`, `research-mcp`, `cloudflare-mcp`,
144+
`postgresql-mcp`, `browser-mcp` (headless Firefox; demote to Wave 3 if
145+
flaky).
146+
| adjust | Swap any cartridge; the only hard constraints are
147+
*credential-free first* (so the probe runs in CI without secrets) and
148+
*both dispatch paths covered* (Zig `.so` + JS `mod.js`).
149+
|===
150+
151+
Selection criteria, in order: credential-free first · highest MCP-user
152+
demand · cover both dispatch paths · ≤ one per domain. `feedback-mcp` +
153+
`boj-health` remain the gold references (not counted in the twelve).
154+
155+
`RULE (confirm / swaps): ______________________________`
156+
157+
== D5 — Version reset — unblocks G6
158+
159+
*Question.* One version story to replace the `0.4.6 / 0.4.7 / 1.1.0-wip`
160+
split and ROADMAP's premature "v1.1.0 Active".
161+
162+
[cols="1,4"]
163+
|===
164+
| ▶ *A (recommended)* | Next public release is *0.9.0 "honest beta"* (cut
165+
at G1+G2 — installs everywhere + Golden Dozen real). *1.0.0* is cut at
166+
G6. Reset all manifests (package/jsr/gemini-extension/glama/smithery/
167+
CITATION) + STATE to `0.9.0-wip` now; announce the reset once in the
168+
changelog.
169+
| B | Keep climbing from 0.4.x — next release 0.5.0, 1.0.0 later. Avoids a
170+
"backwards" version optics but keeps the manifest/STATE split unless
171+
also reconciled.
172+
| C | Declare current state 1.0.0. *Not recommended* — contradicts
173+
`cartridges-available-real = 1` and the whole truthfulness posture.
174+
|===
175+
176+
Recommendation A: "0.9.0 honest beta → 1.0.0 at real v1" tells the
177+
truth and gives the launch a clean story; the one-count-one-place rule
178+
(plan §7 E2) keeps it from re-drifting.
179+
180+
`RULE: _______________________________________________`
181+
182+
== D6 — GEMINI.md — RESOLVED to a one-liner (confirm only)
183+
184+
*Status.* No longer a contradiction. `gemini-extension.json:17` sets
185+
`"contextFileName": "GEMINI.md"`, so the file *is* load-bearing
186+
(STATE 2026-05-26 was right; the #199 "stale → delete" finding is a
187+
Hypatia `root_hygiene` false positive that doesn't know the
188+
gemini-extension contract).
189+
190+
*Action (recommended):* keep `GEMINI.md`; add a Hypatia ignore/exemption
191+
so the false positive stops recurring on every scan; close that line of
192+
#199. No owner judgement needed unless you *want* to drop Gemini support
193+
(then delete both the file and the `contextFileName` line).
194+
195+
`RULE (default = keep + exempt): ______________________`
196+
197+
== After the rulings
198+
199+
Each ruling converts directly into mechanical work that needs no further
200+
decision:
201+
202+
[cols="1,3"]
203+
|===
204+
| D1 | one-line `package.json` edit (per ruling) + close #186
205+
| D2 | flip `TrustPolicy` non-loopback path read→require; finish HCG D-4
206+
baselines → E rollout
207+
| D3 | canonical tier doc in `standards`; relabel manifests (A = just
208+
`feedback-mcp`→Teranga to start)
209+
| D4 | point the Foundry at Wave 1; one fresh mint proves the factory
210+
(plan A1) → batch
211+
| D5 | sweep version fields to `0.9.0-wip`; changelog note; fix ROADMAP
212+
status line
213+
| D6 | keep file + add Hypatia exemption
214+
|===
215+
216+
I can take any/all of these from "ruled" to "PR" on your word — they are
217+
deliberately scoped so none needs a second decision once you've marked
218+
the lines above.

0 commit comments

Comments
 (0)