Skip to content

Commit 1b6e767

Browse files
hyperpolymathclaude
hyperpolymath
and
claude
authored
docs(proofs): reconcile PROOF-NEEDS and the proof-debt ledger with the tree (#163)
## Why Both proof ledgers had drifted from the code. - **`PROOF-NEEDS.adoc`** said PanLL has "no Idris2 files" and listed a "PCC ReScript scanner". In fact the panel-clades ABI has about 1,300 lines of total Idris2 with no escape hatches. The `panel-clades-abi` CI job enforces this through `check-abi.sh`. - **`docs/proof-debt.adoc`** said "(d) Debt: None". But `src-gossamer` has 15 Rust `unsafe` sites, and none has a `TRUSTED:` annotation or a test budget. The standards policy treats those as debt. The estate checker only scans proof languages, not Rust, which is why it passed. ## What changes **`PROOF-NEEDS.adoc`** (rewritten): - **Current state**: what the CI gate enforces, and what each module proves, by lemma name (`resultRoundTrip`, `alignUpCorrect`, `calcStructSizeAligned`, `phasesWithin`, `crossTwice`, `betterOfTwo`, …). The six reject fixtures are also listed. - **Not proved**: the three limits the modules state themselves: - struct size ≥ end of the last field (checked only at run time); - the Zig side matching the Idris declarations; - grades reaching the runtime. - **Still owed**: a table with status and tracking issue for each item: - the layout lemma; - the callback wrapper (#149); - the FFI agreement check; - the grade-kernel identity (#143); - more clade budgets; - IPC dispatch; - PCC soundness, the dashboard, provenance, the cartridge schema and the Wiring Inspector. Items that depended on the deleted ReScript frontend are marked blocked on #148. **`docs/proof-debt.adoc`** (same standards schema, headings unchanged): - **(a)–(c)**: stay "None". That was already correct, because the ledger records escape hatches, and none was ever discharged, budgeted or axiomatised here. (a) now says why. - **(d)**: lists the Rust `unsafe` sites, grouped by kind: coprocessor `libloading`, `libc::kill` in `llm_coding` and `game_preview`, `statvfs`, and `gossamer_tray_destroy`. The owner is you, and the deadline is INDEFINITE until you decide each group. One entry notes that the coprocessor `SAFETY` comment relies on `copro_free`, which currently frees nothing (#149). ## Verification - I checked every lemma name, line number and claim against the code on `main` (`1937c6b`). - standards' `scripts/check-trusted-base.sh` still passes. It finds 2 signatures, both documented. - The changed files contain no unlinked debt markers (`TODO`/`FIXME`). Docs only; no code changes. --- _Generated by [Claude Code](https://claude.ai/code/session_01BCQeL169ZnUirUVaDXQLA3)_ Co-authored-by: Claude <noreply@anthropic.com>
1 parent 1937c6b commit 1b6e767

2 files changed

Lines changed: 217 additions & 36 deletions

File tree

‎PROOF-NEEDS.adoc‎

Lines changed: 166 additions & 34 deletions
Original file line numberDiff line numberDiff line change
@@ -1,50 +1,182 @@
1-
== PROOF-NEEDS.md — panll
1+
// SPDX-License-Identifier: CC-BY-SA-4.0
2+
= Proof needs — PanLL
3+
:toc: macro
24

3-
=== Current State
5+
What PanLL proves today, what it deliberately does not, and what is still
6+
owed. Escape hatches and their dispositions are tracked separately in
7+
link:docs/proof-debt.adoc[`docs/proof-debt.adoc`].
48

5-
* *src/abi/*: YES — contains `+cartridge-schema.json+` and `+README.md+`
6-
(no Idris2 files)
7-
* *Dangerous patterns*: 0 in own code (164 references are all in UI
8-
display code that shows believe_me/Admitted counts from OTHER repos)
9-
* *LOC*: ~138,000 (ReScript + Rust)
10-
* *ABI layer*: Schema-only, no Idris2 proofs
9+
Last reconciled against the tree: 2026-10-26 (`main` at `1937c6b`).
1110

12-
=== What Needs Proving
11+
toc::[]
1312

14-
[width="100%",cols="51%,27%,22%",options="header",]
13+
== Current state
14+
15+
The only machine-checked proofs live in the panel-clades ABI,
16+
`panel-clades/src/abi/PanelClades/ABI/` (Idris2 0.8.0, `%default total`,
17+
about 1,300 lines). There are no holes, `believe_me`, `assert_total`,
18+
`assert_smaller`, `idris_crash` or `postulate` in any `.idr` file.
19+
20+
The CI job `panel-clades-abi` in `.github/workflows/build-validation.yml`
21+
runs `panel-clades/scripts/check-abi.sh`, which:
22+
23+
* builds typed-wasm's grade kernel at the pin in
24+
`panel-clades/scripts/fetch-siblings.sh` (`117bbf8`);
25+
* builds `panel-clades/src/abi/panel-clades-grades.ipkg` against it and
26+
fails on any `Error:` line, even when `idris2` exits 0;
27+
* fails if any module under `PanelClades/` is missing from the ipkg, or
28+
uses an escape hatch;
29+
* fails if `Budgets.idr` is stale against the clade configs
30+
(`scripts/gen-budgets.sh --check`);
31+
* requires each of the six fixtures in `panel-clades/tests/reject/` to be
32+
refused at its `invalid` declaration, with the expected message.
33+
34+
=== What is proved
35+
36+
[cols="1,3",options="header"]
37+
|===
38+
|Module |Proved
39+
40+
|`Types.idr`
41+
|The C tag encodings of `Result` and `CladeKind` round-trip, so they are
42+
injective (`resultRoundTrip`, `cladeKindRoundTrip`). Equality on both is
43+
decidable without a catch-all `absurd` (`decEqViaTag`). `allCladeKinds`
44+
lists every kind (`cladeKindExhaustive`) and has length `cladeKindCount`.
45+
A `Handle` is never null and a `CladeId` is never empty, by construction.
46+
47+
|`Layout.idr`
48+
|Rounding up to an alignment lands on a multiple of it (`alignUpCorrect`).
49+
Every computed struct size is a multiple of its alignment
50+
(`calcStructSizeAligned`). Field alignment is decided by an equation on
51+
`Nat` (`decDivides`, `proveFieldsAligned`), not by a Boolean test.
52+
53+
|`Grades.idr`
54+
|Clade resource contracts are graded in typed-wasm's kernel (transcribed
55+
from hyperpolymath/resource-algebra), not re-declared. Occupancy composes
56+
within a bound (`phasesWithin`). Loss adds across two crossings
57+
(`crossTwice`), and the better of two alternatives stays within a shared
58+
bound (`betterOfTwo`). Occupancy and cost are kept apart
59+
(`panelPhasesOccupancy` vs `panelPhasesCost`). The neurosym-bridge
60+
contract typechecks against its declared budget
61+
(`neurosymBridgeContract`).
62+
63+
|`Budgets.idr`
64+
|Generated from the clades' `config.k9.ncl` resource blocks. It proves
65+
nothing itself; it is the input `Grades.idr` checks against. Only
66+
neurosym-bridge declares a budget so far.
67+
68+
|`Foreign.idr`
69+
|Typechecks only. It declares the Zig FFI surface; it proves nothing.
1570
|===
16-
|Component |What |Why
17-
|Cartridge schema validation |Cartridge loading validates against schema
18-
correctly |Malformed cartridges crash panels or produce wrong output
1971

20-
|PCC constraint propagator |Constraint propagation is sound and complete
21-
|PanLL Constraint Checker is the build-time safety net
72+
The reject fixtures pin down what the types refuse: `BudgetTooSmall`,
73+
`CollapseWithinTolerance`, `MisalignedField`, `NullHandle`, `OverBudget`
74+
and `WasmPointerIsEightBytes`.
75+
76+
=== What is not proved
77+
78+
These limits are stated in the modules themselves.
79+
80+
* *Struct size covers the last field.* `Layout.idr` does not prove that a
81+
computed size is at least the end of the last field; `verifyLayout`
82+
checks it at run time and refuses a layout that fails.
83+
* *The Zig side matches.* Nothing checks that `panel-clades/ffi/zig/`
84+
exports the symbols `Foreign.idr` declares, with those types, or uses
85+
the sizes and tags `Types.idr` proves. `ffi/zig/src/main.zig` restates
86+
them by hand.
87+
* *Grades reach the runtime.* The budgets are DESIGNED values from the
88+
configs, not measurements, and nothing in the panel runtime emits or
89+
checks these grades yet.
90+
91+
== What needs proving
92+
93+
[cols="2,3,2,1",options="header"]
94+
|===
95+
|Item |What |Status |Tracked
96+
97+
|Struct size lower bound
98+
|Prove `calcStructSize` is at least the end of the last field, and drop
99+
the run-time check in `verifyLayout`.
100+
|Not started. Induction over the field list plus a lemma about rounding
101+
up.
102+
|—
103+
104+
|Safe callback registration
105+
|A safe wrapper for `prim__registerCallback` in `Foreign.idr`, using
106+
Idris2's FFI callback mechanism (`cast` is banned).
107+
|Not started.
108+
|#149
109+
110+
|Zig/Idris FFI agreement
111+
|Check that the Zig exports match `Foreign.idr` and the proven sizes and
112+
tags. This is a CI check, not a proof.
113+
|Not started.
114+
|—
115+
116+
|Grade kernel identity
117+
|Confirm typed-wasm's transcription matches resource-algebra's Agda
118+
`MaxPlus` kernel, which is now the family instance.
119+
|Open question; PanLL already imports the kernel through typed-wasm.
120+
|#143
121+
122+
|More clade budgets
123+
|As clade configs declare resource blocks, `gen-budgets.sh` emits them
124+
and their contracts need to typecheck.
125+
|One clade so far (neurosym-bridge).
126+
|—
127+
128+
|IPC dispatch is total
129+
|Every command the frontend invokes has a registered handler.
130+
|Partly covered by tests: `src-gossamer/src/ipc.rs` checks every table
131+
entry and that the table and `main.rs` never register the same name
132+
twice. Completing it needs the frontend's `invoke` names, which wait on
133+
the AffineScript port.
134+
|#148
22135

23-
|PCC ReScript scanner |Scanner correctly identifies all constraint
24-
violations |Missed violations bypass safety checks
136+
|PCC soundness
137+
|The PanLL Constraint Checker (`tools/pcc`) propagates constraints soundly
138+
and finds every violation.
139+
|Blocked: `tools/pcc` still scans ReScript `.res` sources, which #107
140+
removed. It must be rebuilt for AffineScript before a proof means
141+
anything, and it needs a written specification first.
142+
|#148
25143

26-
|Verification Dashboard accuracy |Dashboard accurately reflects actual
27-
proof state |Displaying wrong verification state gives false confidence
144+
|Verification Dashboard accuracy
145+
|The dashboard reports the real proof state of the repos it inspects.
146+
|Better served by fixture tests than by proof. Waits on the frontend
147+
port.
148+
|#148
28149

29-
|Provenance engine |Provenance tracking is complete and unforgeable
30-
|Provenance gaps break audit trail
150+
|Provenance engine
151+
|Provenance tracking is complete (every action is recorded). "Unforgeable"
152+
is a cryptographic claim and needs a threat model first.
153+
|Not started; needs a specification.
154+
|—
31155

32-
|Gossamer coprocessor commands |Command dispatch is total (no unhandled
33-
commands) |Unhandled commands silently fail
156+
|Cartridge schema validation
157+
|Loading a cartridge validates it against `src/abi/cartridge-schema.json`.
158+
|Schema only; no validator to prove against yet.
159+
|—
34160

35-
|Wiring Inspector |Wiring analysis correctly identifies all connections
36-
|Missing wires mean broken panel communication
161+
|Wiring Inspector
162+
|Wiring analysis finds every panel connection.
163+
|Waits on the frontend port.
164+
|#148
37165
|===
38166

39-
=== Recommended Prover
167+
== Recommended prover
40168

41-
*Idris2* — Replace schema-only ABI with proper Idris2 types. PCC
42-
constraint propagation is a natural fit for formal verification. The
43-
Rust PCC tool (`+tools/pcc/+`) should have soundness proofs.
169+
*Idris2 0.8.0* for anything at the ABI or grade level, matching the
170+
existing modules and the typed-wasm kernel they import. Rust-side
171+
properties (IPC dispatch, PCC) are better served first by tests with a
172+
stated budget; a mechanised proof only pays once each has a written
173+
specification.
44174

45-
=== Priority
175+
== Priority
46176

47-
*MEDIUM* — PanLL is the developer panel system. PCC soundness is the
48-
highest-value proof (it checks constraints across the ecosystem). The
49-
Verification Dashboard must accurately reflect proof state to avoid
50-
false confidence.
177+
. Struct size lower bound and the safe callback wrapper (#149): small,
178+
local, and they close the two gaps the modules admit to.
179+
. Zig/Idris FFI agreement check: cheap, and it removes the largest
180+
unchecked assumption under the proofs.
181+
. PCC soundness: the highest-value proof, but only after the AffineScript
182+
port (#148) gives it something to check.

‎docs/proof-debt.adoc‎

Lines changed: 51 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,9 +1,26 @@
11
// SPDX-License-Identifier: CC-BY-SA-4.0
22
= Proof Debt
33

4+
Schema: hyperpolymath/standards
5+
`docs/TRUSTED-BASE-REDUCTION-POLICY.adoc`. This ledger records every
6+
soundness-relevant escape hatch and its disposition. What PanLL proves, and
7+
what it still needs to prove, is in link:../PROOF-NEEDS.adoc[`PROOF-NEEDS.adoc`].
8+
9+
Last reconciled: 2026-10-26 (`main` at `1937c6b`).
10+
11+
* *Idris2* (`panel-clades/src/abi/`): no `believe_me`, `assert_total`,
12+
`assert_smaller`, `idris_crash`, `postulate` or holes. `check-abi.sh`
13+
fails CI if one appears.
14+
* *Estate check*: standards' `scripts/check-trusted-base.sh` finds 2
15+
escape-hatch signatures, both documented below as not proof debt.
16+
* *Rust*: the estate check does not scan Rust. The `unsafe` blocks in
17+
`src-gossamer/` are listed under (d) because none carries a `TRUSTED:`
18+
annotation or a refutation budget yet.
19+
420
== (a) Discharged in this repository
521

6-
* None.
22+
* None. No escape hatch has been replaced by a proof here; the
23+
panel-clades ABI was written without any.
724

825
== (b) Budgeted — tested with a refutation budget
926

@@ -15,7 +32,39 @@
1532

1633
== (d) Debt — actively to be closed
1734

18-
* None.
35+
Each entry is a Rust `unsafe` block at an FFI or system-call boundary.
36+
None is annotated with `// TRUSTED:`, and none has a stated test budget, so
37+
none qualifies as (b) yet.
38+
39+
*Owner*: @hyperpolymath. *Deadline*: INDEFINITE — the disposition of each
40+
group (annotate and budget as (b), or remove the `unsafe`) is an owner
41+
decision. *Plan* for each: add a `// TRUSTED: <kind>; <budget>` annotation
42+
and the test that sets the budget, then move the entry to (b).
43+
44+
* `src-gossamer/src/coprocessor/commands.rs:238`, `:242`, `:244`, `:327` —
45+
`libloading` load of the Zig coprocessor library and calls to
46+
`copro_init`, `copro_dispatch` and `copro_free`.
47+
** *Kind*: extraction boundary (Rust → Zig, dynamic library).
48+
** *Note*: the `SAFETY` comment at `:322` says the result is freed by
49+
`copro_free`, but the Zig `copro_free` currently frees nothing (#149),
50+
so every dispatch result leaks.
51+
* `src-gossamer/src/coprocessor/mod.rs:114`, `:117`, `:120`, `:123` — the
52+
`unsafe extern "C" fn` types for those symbols. These are declarations;
53+
they share the entry above.
54+
* `src-gossamer/src/llm_coding/commands.rs:197`, `:217`, `:237` —
55+
`libc::kill` sending `SIGSTOP` / `SIGCONT` / `SIGTERM` to a session's
56+
process.
57+
** *Kind*: system call. No `SAFETY` comment.
58+
* `src-gossamer/src/game_preview/commands.rs:203`, `:206` — `libc::kill`
59+
sending `SIGTERM` to a preview's process group, then its pid.
60+
** *Kind*: system call. No `SAFETY` comment.
61+
* `src-gossamer/src/workspace/sysinfo.rs:113` — `libc::statvfs` into a
62+
zeroed struct.
63+
** *Kind*: system call. Has a `SAFETY` comment.
64+
* `src-gossamer/src/system_tray/mod.rs:101` — `gossamer_tray_destroy` on a
65+
tray handle.
66+
** *Kind*: extraction boundary (Rust → Gossamer C ABI). No `SAFETY`
67+
comment. Compiled only with `--features gossamer`.
1968

2069
== Scanner signatures that are not proof debt
2170

0 commit comments

Comments
 (0)