Repository navigation
docs(proofs): reconcile PROOF-NEEDS and the proof-debt ledger with the tree #163
There are no files selected for viewing
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -1,50 +1,182 @@ | ||
| // SPDX-License-Identifier: CC-BY-SA-4.0 | ||
| = Proof needs — PanLL | ||
| :toc: macro | ||
|
|
||
| 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`]. | ||
|
|
||
| Last reconciled against the tree: 2026-10-26 (`main` at `1937c6b`). | ||
|
|
||
| toc::[] | ||
|
|
||
| == 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. | ||
| |=== | ||
|
|
||
| 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 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 | ||
| |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 (every action is recorded). "Unforgeable" | ||
| is a cryptographic claim and needs a threat model first. | ||
| |Not started; needs a specification. | ||
| |— | ||
|
|
||
| |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 finds every panel connection. | ||
| |Waits on the frontend port. | ||
| |#148 | ||
| |=== | ||
|
|
||
| == Recommended prover | ||
|
|
||
| *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 | ||
|
|
||
| . 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. | ||
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Oops, something went wrong.
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
For any nonempty field list with
align = 0,Layout.idrdefinesalignUnits _ 0 = 0, socalcStructSize fields 0is 0 whilestructEnd fieldscan be positive. The proposed unconditional lower-bound theorem is therefore false, and the runtime check cannot be dropped merely by induction; this item must either require a positive alignment or first change the zero-alignment behavior.Useful? React with 👍 / 👎.