From 9564419b1ea17d7f93f70277675138ab6e8beb53 Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 26 Oct 2026 22:11:12 +0000 Subject: [PATCH] docs(proofs): reconcile PROOF-NEEDS and the proof-debt ledger with the tree PROOF-NEEDS.adoc said PanLL has no Idris2 and listed a "PCC ReScript scanner". Since #145-#152 the panel-clades ABI has about 1,300 lines of total Idris2 with no escape hatches, gated in CI by check-abi.sh. The file now states what each module proves (with lemma names), the three limits the modules themselves admit to, and what is still owed, with status and tracking issue. Items that depend on the removed ReScript frontend (PCC soundness, dashboard, wiring) are marked blocked on #148. docs/proof-debt.adoc keeps the standards schema. (a)-(c) stay empty, which was already correct: the ledger records escape hatches, and none was ever discharged, budgeted or axiomatised here. (d) said "None", but src-gossamer has 15 Rust `unsafe` sites at FFI and syscall boundaries with no TRUSTED: annotation or test budget. The estate checker does not scan Rust, so it passed; they are now listed by kind for an owner decision, including the copro_free leak (#149) that contradicts the coprocessor SAFETY comment. standards' check-trusted-base.sh still passes (2 signatures, both documented). Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01BCQeL169ZnUirUVaDXQLA3 --- PROOF-NEEDS.adoc | 200 +++++++++++++++++++++++++++++++++++-------- docs/proof-debt.adoc | 53 +++++++++++- 2 files changed, 217 insertions(+), 36 deletions(-) diff --git a/PROOF-NEEDS.adoc b/PROOF-NEEDS.adoc index 7157c5bc..d43c50e5 100644 --- a/PROOF-NEEDS.adoc +++ b/PROOF-NEEDS.adoc @@ -1,50 +1,182 @@ -== PROOF-NEEDS.md — panll +// SPDX-License-Identifier: CC-BY-SA-4.0 += Proof needs — PanLL +:toc: macro -=== Current State +What PanLL proves today, what it deliberately does not, and what is still +owed. Escape hatches and their dispositions are tracked separately in +link:docs/proof-debt.adoc[`docs/proof-debt.adoc`]. -* *src/abi/*: YES — contains `+cartridge-schema.json+` and `+README.md+` -(no Idris2 files) -* *Dangerous patterns*: 0 in own code (164 references are all in UI -display code that shows believe_me/Admitted counts from OTHER repos) -* *LOC*: ~138,000 (ReScript + Rust) -* *ABI layer*: Schema-only, no Idris2 proofs +Last reconciled against the tree: 2026-10-26 (`main` at `1937c6b`). -=== What Needs Proving +toc::[] -[width="100%",cols="51%,27%,22%",options="header",] +== Current state + +The only machine-checked proofs live in the panel-clades ABI, +`panel-clades/src/abi/PanelClades/ABI/` (Idris2 0.8.0, `%default total`, +about 1,300 lines). There are no holes, `believe_me`, `assert_total`, +`assert_smaller`, `idris_crash` or `postulate` in any `.idr` file. + +The CI job `panel-clades-abi` in `.github/workflows/build-validation.yml` +runs `panel-clades/scripts/check-abi.sh`, which: + +* builds typed-wasm's grade kernel at the pin in + `panel-clades/scripts/fetch-siblings.sh` (`117bbf8`); +* builds `panel-clades/src/abi/panel-clades-grades.ipkg` against it and + fails on any `Error:` line, even when `idris2` exits 0; +* fails if any module under `PanelClades/` is missing from the ipkg, or + uses an escape hatch; +* fails if `Budgets.idr` is stale against the clade configs + (`scripts/gen-budgets.sh --check`); +* requires each of the six fixtures in `panel-clades/tests/reject/` to be + refused at its `invalid` declaration, with the expected message. + +=== What is proved + +[cols="1,3",options="header"] +|=== +|Module |Proved + +|`Types.idr` +|The C tag encodings of `Result` and `CladeKind` round-trip, so they are +injective (`resultRoundTrip`, `cladeKindRoundTrip`). Equality on both is +decidable without a catch-all `absurd` (`decEqViaTag`). `allCladeKinds` +lists every kind (`cladeKindExhaustive`) and has length `cladeKindCount`. +A `Handle` is never null and a `CladeId` is never empty, by construction. + +|`Layout.idr` +|Rounding up to an alignment lands on a multiple of it (`alignUpCorrect`). +Every computed struct size is a multiple of its alignment +(`calcStructSizeAligned`). Field alignment is decided by an equation on +`Nat` (`decDivides`, `proveFieldsAligned`), not by a Boolean test. + +|`Grades.idr` +|Clade resource contracts are graded in typed-wasm's kernel (transcribed +from hyperpolymath/resource-algebra), not re-declared. Occupancy composes +within a bound (`phasesWithin`). Loss adds across two crossings +(`crossTwice`), and the better of two alternatives stays within a shared +bound (`betterOfTwo`). Occupancy and cost are kept apart +(`panelPhasesOccupancy` vs `panelPhasesCost`). The neurosym-bridge +contract typechecks against its declared budget +(`neurosymBridgeContract`). + +|`Budgets.idr` +|Generated from the clades' `config.k9.ncl` resource blocks. It proves +nothing itself; it is the input `Grades.idr` checks against. Only +neurosym-bridge declares a budget so far. + +|`Foreign.idr` +|Typechecks only. It declares the Zig FFI surface; it proves nothing. |=== -|Component |What |Why -|Cartridge schema validation |Cartridge loading validates against schema -correctly |Malformed cartridges crash panels or produce wrong output -|PCC constraint propagator |Constraint propagation is sound and complete -|PanLL Constraint Checker is the build-time safety net +The reject fixtures pin down what the types refuse: `BudgetTooSmall`, +`CollapseWithinTolerance`, `MisalignedField`, `NullHandle`, `OverBudget` +and `WasmPointerIsEightBytes`. + +=== What is not proved + +These limits are stated in the modules themselves. + +* *Struct size covers the last field.* `Layout.idr` does not prove that a + computed size is at least the end of the last field; `verifyLayout` + checks it at run time and refuses a layout that fails. +* *The Zig side matches.* Nothing checks that `panel-clades/ffi/zig/` + exports the symbols `Foreign.idr` declares, with those types, or uses + the sizes and tags `Types.idr` proves. `ffi/zig/src/main.zig` restates + them by hand. +* *Grades reach the runtime.* The budgets are DESIGNED values from the + configs, not measurements, and nothing in the panel runtime emits or + checks these grades yet. + +== What needs proving + +[cols="2,3,2,1",options="header"] +|=== +|Item |What |Status |Tracked + +|Struct size lower bound +|Prove `calcStructSize` is at least the end of the last field, and drop +the run-time check in `verifyLayout`. +|Not started. Induction over the field list plus a lemma about rounding +up. +|— + +|Safe callback registration +|A safe wrapper for `prim__registerCallback` in `Foreign.idr`, using +Idris2's FFI callback mechanism (`cast` is banned). +|Not started. +|#149 + +|Zig/Idris FFI agreement +|Check that the Zig exports match `Foreign.idr` and the proven sizes and +tags. This is a CI check, not a proof. +|Not started. +|— + +|Grade kernel identity +|Confirm typed-wasm's transcription matches resource-algebra's Agda +`MaxPlus` kernel, which is now the family instance. +|Open question; PanLL already imports the kernel through typed-wasm. +|#143 + +|More clade budgets +|As clade configs declare resource blocks, `gen-budgets.sh` emits them +and their contracts need to typecheck. +|One clade so far (neurosym-bridge). +|— + +|IPC dispatch is total +|Every command the frontend invokes has a registered handler. +|Partly covered by tests: `src-gossamer/src/ipc.rs` checks every table +entry and that the table and `main.rs` never register the same name +twice. Completing it needs the frontend's `invoke` names, which wait on +the AffineScript port. +|#148 -|PCC ReScript scanner |Scanner correctly identifies all constraint -violations |Missed violations bypass safety checks +|PCC soundness +|The PanLL Constraint Checker (`tools/pcc`) propagates constraints soundly +and finds every violation. +|Blocked: `tools/pcc` still scans ReScript `.res` sources, which #107 +removed. It must be rebuilt for AffineScript before a proof means +anything, and it needs a written specification first. +|#148 -|Verification Dashboard accuracy |Dashboard accurately reflects actual -proof state |Displaying wrong verification state gives false confidence +|Verification Dashboard accuracy +|The dashboard reports the real proof state of the repos it inspects. +|Better served by fixture tests than by proof. Waits on the frontend +port. +|#148 -|Provenance engine |Provenance tracking is complete and unforgeable -|Provenance gaps break audit trail +|Provenance engine +|Provenance tracking is complete (every action is recorded). "Unforgeable" +is a cryptographic claim and needs a threat model first. +|Not started; needs a specification. +|— -|Gossamer coprocessor commands |Command dispatch is total (no unhandled -commands) |Unhandled commands silently fail +|Cartridge schema validation +|Loading a cartridge validates it against `src/abi/cartridge-schema.json`. +|Schema only; no validator to prove against yet. +|— -|Wiring Inspector |Wiring analysis correctly identifies all connections -|Missing wires mean broken panel communication +|Wiring Inspector +|Wiring analysis finds every panel connection. +|Waits on the frontend port. +|#148 |=== -=== Recommended Prover +== Recommended prover -*Idris2* — Replace schema-only ABI with proper Idris2 types. PCC -constraint propagation is a natural fit for formal verification. The -Rust PCC tool (`+tools/pcc/+`) should have soundness proofs. +*Idris2 0.8.0* for anything at the ABI or grade level, matching the +existing modules and the typed-wasm kernel they import. Rust-side +properties (IPC dispatch, PCC) are better served first by tests with a +stated budget; a mechanised proof only pays once each has a written +specification. -=== Priority +== Priority -*MEDIUM* — PanLL is the developer panel system. PCC soundness is the -highest-value proof (it checks constraints across the ecosystem). The -Verification Dashboard must accurately reflect proof state to avoid -false confidence. +. Struct size lower bound and the safe callback wrapper (#149): small, + local, and they close the two gaps the modules admit to. +. Zig/Idris FFI agreement check: cheap, and it removes the largest + unchecked assumption under the proofs. +. PCC soundness: the highest-value proof, but only after the AffineScript + port (#148) gives it something to check. diff --git a/docs/proof-debt.adoc b/docs/proof-debt.adoc index d2bb869d..57397f2d 100644 --- a/docs/proof-debt.adoc +++ b/docs/proof-debt.adoc @@ -1,9 +1,26 @@ // SPDX-License-Identifier: CC-BY-SA-4.0 = Proof Debt +Schema: hyperpolymath/standards +`docs/TRUSTED-BASE-REDUCTION-POLICY.adoc`. This ledger records every +soundness-relevant escape hatch and its disposition. What PanLL proves, and +what it still needs to prove, is in link:../PROOF-NEEDS.adoc[`PROOF-NEEDS.adoc`]. + +Last reconciled: 2026-10-26 (`main` at `1937c6b`). + +* *Idris2* (`panel-clades/src/abi/`): no `believe_me`, `assert_total`, + `assert_smaller`, `idris_crash`, `postulate` or holes. `check-abi.sh` + fails CI if one appears. +* *Estate check*: standards' `scripts/check-trusted-base.sh` finds 2 + escape-hatch signatures, both documented below as not proof debt. +* *Rust*: the estate check does not scan Rust. The `unsafe` blocks in + `src-gossamer/` are listed under (d) because none carries a `TRUSTED:` + annotation or a refutation budget yet. + == (a) Discharged in this repository -* None. +* None. No escape hatch has been replaced by a proof here; the + panel-clades ABI was written without any. == (b) Budgeted — tested with a refutation budget @@ -15,7 +32,39 @@ == (d) Debt — actively to be closed -* None. +Each entry is a Rust `unsafe` block at an FFI or system-call boundary. +None is annotated with `// TRUSTED:`, and none has a stated test budget, so +none qualifies as (b) yet. + +*Owner*: @hyperpolymath. *Deadline*: INDEFINITE — the disposition of each +group (annotate and budget as (b), or remove the `unsafe`) is an owner +decision. *Plan* for each: add a `// TRUSTED: ; ` annotation +and the test that sets the budget, then move the entry to (b). + +* `src-gossamer/src/coprocessor/commands.rs:238`, `:242`, `:244`, `:327` — + `libloading` load of the Zig coprocessor library and calls to + `copro_init`, `copro_dispatch` and `copro_free`. +** *Kind*: extraction boundary (Rust → Zig, dynamic library). +** *Note*: the `SAFETY` comment at `:322` says the result is freed by + `copro_free`, but the Zig `copro_free` currently frees nothing (#149), + so every dispatch result leaks. +* `src-gossamer/src/coprocessor/mod.rs:114`, `:117`, `:120`, `:123` — the + `unsafe extern "C" fn` types for those symbols. These are declarations; + they share the entry above. +* `src-gossamer/src/llm_coding/commands.rs:197`, `:217`, `:237` — + `libc::kill` sending `SIGSTOP` / `SIGCONT` / `SIGTERM` to a session's + process. +** *Kind*: system call. No `SAFETY` comment. +* `src-gossamer/src/game_preview/commands.rs:203`, `:206` — `libc::kill` + sending `SIGTERM` to a preview's process group, then its pid. +** *Kind*: system call. No `SAFETY` comment. +* `src-gossamer/src/workspace/sysinfo.rs:113` — `libc::statvfs` into a + zeroed struct. +** *Kind*: system call. Has a `SAFETY` comment. +* `src-gossamer/src/system_tray/mod.rs:101` — `gossamer_tray_destroy` on a + tray handle. +** *Kind*: extraction boundary (Rust → Gossamer C ABI). No `SAFETY` + comment. Compiled only with `--features gossamer`. == Scanner signatures that are not proof debt