diff --git a/.github/workflows/build-validation.yml b/.github/workflows/build-validation.yml index 96cb85b..e20e310 100644 --- a/.github/workflows/build-validation.yml +++ b/.github/workflows/build-validation.yml @@ -48,7 +48,10 @@ jobs: # typed-wasm's grade kernel at its pin, and the expected rejections are # refused. Idris2 publishes no binaries, so 0.8.0 is built from source, # fetched by the commit its v0.8.0 tag names (a tag can move; the SHA - # cannot). + # cannot). Deviation (PROOF-POLICY §6): built from upstream source, not a + # Guix manifest or container (PanLL has neither for proof tools yet); + # the commit is asserted here and check-abi.sh asserts version 0.8.0. + # State: open. panel-clades-abi: runs-on: ubuntu-latest timeout-minutes: 40 @@ -84,3 +87,32 @@ jobs: - name: panel-clades ABI run: bash panel-clades/scripts/check-abi.sh + + # Provenance adversary model (PROOF-POLICY §4 exception, TESTED within the + # bounds in docs/models/Provenance.cfg), checked both ways by + # docs/models/check-models.sh. Deviation (PROOF-POLICY §6): TLC is fetched + # from the tlaplus/tlaplus v1.7.4 release, not a Guix manifest or + # container (PanLL has neither for proof tools yet); the script asserts + # the jar's SHA-256 and TLC 2.19 and fails on any mismatch. State: open. + provenance-model: + runs-on: ubuntu-latest + timeout-minutes: 30 + permissions: + contents: read + env: + TLA2TOOLS_URL: https://github.com/tlaplus/tlaplus/releases/download/v1.7.4/tla2tools.jar + TLA2TOOLS_SHA256: 936a262061c914694dfd669a543be24573c45d5aa0ff20a8b96b23d01e050e88 + steps: + - name: Checkout + uses: actions/checkout@v7.0.1 + with: + persist-credentials: false + + - name: Fetch TLC 2.19 (tla2tools v1.7.4) + run: | + curl -fsSL --proto '=https' --proto-redir '=https' --tlsv1.2 --retry 3 \ + -o "$RUNNER_TEMP/tla2tools.jar" "$TLA2TOOLS_URL" + echo "$TLA2TOOLS_SHA256 $RUNNER_TEMP/tla2tools.jar" | sha256sum -c - + + - name: Model-check docs/models/Provenance.tla + run: bash docs/models/check-models.sh "$RUNNER_TEMP/tla2tools.jar" diff --git a/CHANGELOG.adoc b/CHANGELOG.adoc index 4f23bd0..a1b2258 100644 --- a/CHANGELOG.adoc +++ b/CHANGELOG.adoc @@ -9,6 +9,23 @@ https://semver.org/spec/v2.0.0.html[Semantic Versioning]. === https://github.com/hyperpolymath/panll/compare/v0.1.0...HEAD[Unreleased] +==== Fixed (2026-11-09 — proof ledger reconciled with the estate proof policy) + +* *The Idris2 proof gate now covers the whole import cone.* +`panel-clades/scripts/scan-escape-hatches.sh` fails on escape hatches, +holes (`?name`, which `idris2 --build` accepts), `partial`/`covering` and a +missing `%default total`, in PanelClades and in typed-wasm's kernel at its +pin. Before, holes were not checked and the kernel was not scanned. +* *The provenance TLA+ model checks something.* Its `Sign` action let any +party sign any payload, so `Binding` held by definition. It now models a +leaked author key, spliced chains and an honest witness, and CI +(`provenance-model`) checks it both ways: a forgery must be found without +the witness check, and a verified state must be reachable. +* `PROOF-NEEDS.adoc` uses PROOF-POLICY's status tokens, records the import +cone, the §4 exception and the §6 toolchain deviations, states that PanLL's +provenance profile is narrower than Exhibit B, and corrects two overclaims +(`decDivides` is a semi-decision; the struct-size bound needs `align >= 1`). + ==== Removed (2026-11-05) * *The PCC ReScript scanner (`tools/pcc/src/rescript_scanner.rs`) is diff --git a/PROOF-NEEDS.adoc b/PROOF-NEEDS.adoc index cfadd97..fd12f42 100644 --- a/PROOF-NEEDS.adoc +++ b/PROOF-NEEDS.adoc @@ -6,17 +6,27 @@ 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`). +This file follows the estate proof policy, +https://github.com/metadatastician/standards/blob/9bdf864cc7f2c8e24b4df84bf00d04158eee3ad5/3-practice/PROOF-POLICY.adoc[standards `3-practice/PROOF-POLICY.adoc`] +(read at `9bdf864`). Every row carries one of its closed status tokens (§5): +`PROVEN`, `PROVEN-WITH-AXIOMS`, `TESTED` (with bounds), `ASSUMED` or `OPEN`. + +*Proof Witness Grades do not apply.* Every PanLL obligation is engineering: +each names a PanLL type, function, ABI or wire format (PROOF-POLICY §1). PanLL +has no theory obligations of its own, so no row has a PWG (§8.1). The +max-plus/min-plus kernel lemmas it imports are theory owned by +hyperpolymath/resource-algebra; their grade is recorded there. + +Last reconciled against the tree: 2026-11-09 (`main` at `7d1feaa`, plus the +change that added this line). toc::[] == Current state -The only machine-checked proofs live in the panel-clades ABI, +The only kernel-checked proofs live in the panel-clades ABI, `panel-clades/src/abi/PanelClades/ABI/` (Idris2 0.8.0, `%default total`, -about 1,300 lines). As of the date above, no `.idr` file contains a hole, -`believe_me`, `assert_total`, `assert_smaller`, `idris_crash`, -`unsafePerformIO` or `postulate`. +about 1,300 lines). The CI job `panel-clades-abi` in `.github/workflows/build-validation.yml` runs `panel-clades/scripts/check-abi.sh`, which: @@ -25,20 +35,60 @@ runs `panel-clades/scripts/check-abi.sh`, which: `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 - contains `believe_me`, `assert_total`, `assert_smaller`, `idris_crash`, - `unsafePerformIO` or `postulate` (a keyword scan; it does not look for - holes); +* fails if any module under `PanelClades/` is missing from the ipkg; +* runs `panel-clades/scripts/scan-escape-hatches.sh` over the whole import + cone (the five PanelClades modules and every typed-wasm kernel module at + the pin). It fails on `believe_me`, `assert_total`, `assert_smaller`, + `idris_crash`, `unsafePerformIO` or `postulate`, on a hole (`?name`: + `idris2 --build` accepts unsolved holes), on `partial` or `covering`, and + on a module without `%default total`. Comments are ignored; * 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 +=== Import cone (PROOF-POLICY §1.1) + +The kernel is checked, not assumed: [cols="1,3",options="header"] |=== -|Module |Proved +|Field |Value + +|Root +|`panel-clades/src/abi/panel-clades-grades.ipkg` (5 modules) + +|Library +|`hyperpolymath/typed-wasm` `src/abi/typed-wasm.ipkg` at +`117bbf895b513673ba06eb6c4ebb0e26e276e295` (28 modules) + +|Checker and flags +|Idris2 0.8.0 (built from `15a3e4e70843f7a34100f6470c04b791330788df`), +`%default total` in every cone module + +|Escape hatches, holes, opt-outs +|0, enforced by `scan-escape-hatches.sh` on every run + +|Outside the cone +|Idris2's bundled `base`/`contrib` libraries (`Data.List`, `Data.Nat`, +`Data.So`, `Data.Vect`, `Data.Vect.Elem`, `Decidable.Equality`) and the +prelude belong to the toolchain's trusted base: `ASSUMED`, Idris2 +0.8.0. +|=== + +=== What is proved + +Receipt: Build Validation run +https://github.com/hyperpolymath/panll/actions/runs/42408104327[42408104327], +job `panel-clades-abi`, on `main` at +`7d1feaaf112b3d91fd504aaf871be5ae49840434`, 2026-11-07: the package built +with 0 errors and all six fixtures were refused for the expected reasons. +The import-cone scan was added after that run; its first receipt is the CI +run of the change that added it. + +[cols="1,3,1",options="header"] +|=== +|Module |Proved |Status |`Types.idr` |The C tag encodings of `Result` and `CladeKind` round-trip, so they are @@ -46,30 +96,40 @@ 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. +|`PROVEN` |`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. +(`calcStructSizeAligned`). `decDivides` returns a `Divides` witness when an +offset is a multiple of its alignment, and `proveFieldsAligned` builds the +`FieldsAligned` proof from those witnesses. `decDivides` is a semi-decision: +`Nothing` carries no proof that the field is misaligned. +|`PROVEN` |`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`). +|Clade resource contracts are graded in typed-wasm's kernel, 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`). +These hold of the kernel as transcribed in typed-wasm; that the +transcription matches resource-algebra is the separate *Grade kernel +identity* row. +|`PROVEN` |`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. +neurosym-bridge declares a budget so far. The budgets are DESIGNED values, +not measurements. +|— (input) |`Foreign.idr` -|Typechecks only. It declares the Zig FFI surface; it proves nothing. +|Typechecks only. It declares the Zig FFI surface with `%foreign`; the C +side is not checked against it. +|`ASSUMED` |=== The reject fixtures pin down what the types refuse: `BudgetTooSmall`, @@ -93,95 +153,187 @@ These limits are stated in the modules themselves. == What needs proving -[cols="2,3,2,1",options="header"] +[cols="2,3,1,2,1",options="header"] |=== -|Item |What |Status |Tracked +|Item |What |Status |Notes |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. +|Prove `calcStructSize fields align` is at least `structEnd fields`, and +drop the run-time check in `verifyLayout`. +|`OPEN` +|Needs the precondition `align >= 1`: `alignUp` returns 0 for alignment 0, +so the bound is false there. 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. +|`OPEN` +| |#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. +tags. +|`OPEN` +|A CI check, not a proof. Until it exists the FFI contract is `ASSUMED`. |— |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. +|typed-wasm's Idris2 transcription matches resource-algebra's Agda +`MaxPlus`/`Loss` kernel (transcribed at `cf9235c`). +|`ASSUMED` +|A transcription no kernel has compared with its source. |#143 |More clade budgets |As clade configs declare resource blocks, `gen-budgets.sh` emits them and their contracts need to typecheck. +|`OPEN` |One clade so far (neurosym-bridge). |— |IPC dispatch is total |Every command the frontend invokes has a registered handler. -|Backend side covered by tests in `src-gossamer/src/ipc.rs`: -`every_backend_command_is_registered` fails if a public handler in a -command module is reachable from neither the table nor `main.rs`, and -the table and `main.rs` never register the same name twice. Checking the -frontend side needs its `invoke` names, which wait on the AffineScript -port. +|`TESTED` (backend); `OPEN` (frontend) +|`every_backend_command_is_registered` in `src-gossamer/src/ipc.rs` fails +if a public handler in a command module is reachable from neither the table +nor `main.rs`, and the table and `main.rs` never register the same name +twice. Bound: the command modules present at each run. The frontend side +needs its `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`'s ReScript scanner is retired, because #107 removed -the `.res` sources it read. Its frontend-wiring checks now report -"retired" until an AffineScript scanner replaces them. The propagator -itself can be specified and proved first; the scanner proof waits on -the AffineScript port, and it needs a written specification first. +|`OPEN` +|Blocked: the ReScript scanner is retired (#107 removed the `.res` sources +it read), and its frontend-wiring checks report "retired" until an +AffineScript scanner replaces them. The propagator can be specified and +proved first; the scanner proof waits on the port and needs a written +specification. |#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. +|`OPEN` +|Better served by fixture tests than by proof. Waits on the frontend port. |#148 -|Provenance engine -|Provenance tracking is complete (every action is recorded) and -unforgeable. Owner decision (2026-11-05): "unforgeable" means each -provenance record follows `EXHIBIT-B-QUANTUM-SAFE.txt`. The record holds -the author identity, a timestamp, a SHA3-256 content hash and, optionally, -a parent hash. It is serialised as canonical JSON, signed with ML-DSA-65 -and witnessed, and verifies against keys published under -`.well-known/keys/`. Today's engine (git blame plus Co-Authored-By -trailers) is forgeable, so its output counts only as "claimed". -|Implemented in `crates/provenance`: JCS records, ML-DSA-65 signing, -approved public-key registry, independent witnesses, timestamp/content/chain -verification and mutation/property tests. Symbolic binding model: -`docs/models/Provenance.tla`; protocol and limits: -`docs/PROVENANCE-EXHIBIT-B.adoc`. This does not prove every action is recorded, -prevent tail truncation without a checkpoint, or prove cryptographic hardness. +|Provenance: signed records verify only when genuine +|A record is reported `verified` only when its content, metadata and chain +are exactly what an approved author signed and an independent witness +attested. PanLL's profile of `EXHIBIT-B-QUANTUM-SAFE.txt` (owner decision +2026-11-05) is narrower than Exhibit B: ML-DSA-65 only (Exhibit B §2.1 and +§4.1 also allow ML-DSA-87 or an approved alternative), at least one +independent witness is required for `verified` (optional in Exhibit B +§3.2), and keys come only from the verifier's approved `.well-known/keys/` +registry (Exhibit B §5.1 also lists OpenPGP keyservers). Every record PanLL +verifies therefore satisfies Exhibit B; some Exhibit B records verify only +as `claimed`. Protocol: `docs/PROVENANCE-EXHIBIT-B.adoc`. Git blame and +Co-Authored-By trailers stay `claimed`. +|`TESTED` +|`cargo test --manifest-path crates/provenance/Cargo.toml --locked`: 4 +mutation tests and 3 proptest properties (48 cases each) over +content, metadata and chain splices; 7 passed on 2026-11-09 at `7d1feaa`. +The adversary model `docs/models/Provenance.tla` is a §4 exception, below. +Implementation proofs are `OPEN` (Rust table below). +|#173 + +|Provenance: every action is recorded +|Every action that must produce a provenance record does. +|`OPEN` +|Needs the producer inventory and a written recording obligation first. |#173 |Cartridge schema validation |Loading a cartridge validates it against `src/abi/cartridge-schema.json`. +|`OPEN` |Schema only; no validator to prove against yet. |— |Wiring Inspector |Wiring analysis finds every panel connection. +|`OPEN` |Waits on the frontend port. |#148 |=== +== Exceptions (PROOF-POLICY §4) + +[cols="1,3",options="header"] +|=== +|Field |Record + +|Artefact +|`docs/models/Provenance.tla` with `Provenance.cfg`, +`ProvenanceNoWitness.cfg` and `ProvenanceReachable.cfg` (the record is +repeated in the module header) + +|Obligation +|An attacker who can hand the verifier any chain with any content, attach +any published signature, and sign with the author's key once it leaks, +cannot obtain a `verified` verdict for a record the author did not intend, +for content that does not match, or for a broken chain. + +|Tool +|TLA+, checked by TLC + +|Why not the mapped verifiers +|The property is about an adversary interleaving with honest parties. +Creusot/Pearlite and Verus contracts on `verify_chain` state what one call +returns, not what an attacker can reach. Those implementation obligations +remain `OPEN` below. + +|Status +|`TESTED` within the bounds in `Provenance.cfg`: 2 digests, 6 records +(2 roots, 4 children), chains of length 1 or 2, one author and one witness +key. Checked both ways: with the witness requirement removed +(`ProvenanceNoWitness.cfg`) TLC must find a forgery, and +`ProvenanceReachable.cfg` must reach a verified state, so the invariant is +neither vacuous nor true by definition. + +|Trust boundary +|Signatures and hashes are perfectly binding (symbolic); the author and +witness keys are not both compromised. Not a cryptographic proof and not an +implementation-correspondence proof. + +|Receipt +|CI job `provenance-model` in `.github/workflows/build-validation.yml` runs +`docs/models/check-models.sh` (TLC 2.19, jar SHA-256 pinned) on every push +and pull request; its first run is on the change that rewrote the model. It +was rewritten on 2026-11-09 because the earlier model let any party sign +any payload, so its `Binding` invariant held by definition. The receipt in +`docs/PROVENANCE-EXHIBIT-B.adoc` (TLC 2.19, 2026-11-06) is for that earlier +model, `state: superseded`. +|=== + +== Toolchain deviations (PROOF-POLICY §6) + +PanLL has no Guix manifest or container for proof toolchains yet, so both +CI proof lanes install outside them. Each lane asserts its version and fails +on a mismatch; the record is repeated in the workflow. + +[cols="1,1,2,1",options="header"] +|=== +|Leg |Tool and version |Install and digest |State + +|Idris2 ABI (`panel-clades-abi`) +|Idris2 0.8.0 +|Built from `idris-lang/Idris2` at +`15a3e4e70843f7a34100f6470c04b791330788df`; `check-abi.sh` asserts the +version +|`open` + +|Provenance model (`provenance-model`) +|TLC 2.19 (tlaplus v1.7.4) +|`tla2tools.jar` from the GitHub release, SHA-256 +`936a262061c914694dfd669a543be24573c45d5aa0ff20a8b96b23d01e050e88`, +asserted with the version by `check-models.sh` +|`open` +|=== + == Recommended prover *Idris2 0.8.0* for anything at the ABI or grade level, matching the @@ -196,38 +348,39 @@ Pearlite is Creusot's specification language, not an independent prover. |=== |Implementation entrypoint |Verifier and status |Planned obligation |Trust boundary / next action |`crates/provenance/src/lib.rs`: `Registry::new`, `verify_chain` -|Creusot / Pearlite: OPEN +|Creusot / Pearlite: `OPEN` |Registry validity, chain predecessor handling and propagation of invalid or claimed ancestry to later verdicts. |Write contracts on the shipped Rust and qualify supported collection/string operations. No implementation proof has been run for these entrypoints. |Action producers and provenance-recording call sites -|Creusot / Pearlite and Verus: OPEN (specification prerequisite) +|Creusot / Pearlite and Verus: `OPEN` (specification prerequisite) |Define which actions must produce records and establish producer-side coverage, including failure and cancellation paths. Verifying supplied records does not prove that every required action was recorded. |Inventory the producers and specify the recording obligation before assigning implementation contracts; no completeness proof is claimed. |`crates/provenance/src/lib.rs`: `verify_entry`, `verify_witnesses` -|Verus: OPEN +|Verus: `OPEN` |A verified verdict requires the supplied bytes to match the signed content hash, valid author binding and every declared independent witness; rejected or missing evidence cannot promote a verdict. |Specify the production status transitions and establish a checked connection to the shipped functions. No separate model counts as a proof of them. |`canonical`, `hash`, `sign`, `attest`, signature verification and timestamp parsing -|First-party wrappers: Creusot / Pearlite and Verus OPEN +|First-party wrappers: Creusot / Pearlite and Verus `OPEN` |Prove the wrappers preserve their input/output and error contracts, including canonicalisation of `content_hash` and the fields bound by signatures and attestations. Allocate the obligations against the shipped functions. -|Only third-party JCS, SHA3-256, ML-DSA-65, entropy and time-parsing primitives -and their specified behaviour are ASSUMED. Record exact locked versions and -extern contracts when proofs are introduced; cryptographic hardness, civil -identity approval and independent witness judgment are outside these proofs. +|Third-party primitives are `ASSUMED` at their locked versions: `fips204` +0.5.0 (ML-DSA-65 and its RNG), `sha3` 0.10.9, `serde_jcs` 0.2.0 (RFC 8785), +`chrono` 0.4.45 (RFC 3339 parsing), `base64` 0.22.1. Extern contracts are +written when proofs are introduced. Cryptographic hardness, civil identity +approval and independent witness judgment are outside these proofs. |`src-gossamer/src/ipc.rs` dispatch and `tools/pcc` propagation -|Creusot / Pearlite and Verus: OPEN +|Creusot / Pearlite and Verus: `OPEN` |Allocate implementation contracts after writing the dispatch/propagation -specifications; retain current tests as TESTED evidence only. +specifications; retain current tests as `TESTED` evidence only. |PCC frontend scanning remains blocked on the AffineScript port. Neither verifier is silently excluded because that separate dependency is unfinished. |=== diff --git a/docs/PROVENANCE-EXHIBIT-B.adoc b/docs/PROVENANCE-EXHIBIT-B.adoc index a364e1c..7138360 100644 --- a/docs/PROVENANCE-EXHIBIT-B.adoc +++ b/docs/PROVENANCE-EXHIBIT-B.adoc @@ -101,9 +101,13 @@ input returns an empty array, never a batch-level success certification. real ML-DSA signatures, every metadata field, content mutations, witness tampering, identity binding, validity/revocation and chain deletion/splicing. Property tests generate arbitrary content, metadata and parent-hash mutations. -`docs/models/Provenance.tla` models signature binding and chain verification -symbolically. Its invariant is not a cryptographic proof of ML-DSA or SHA3, -nor a proof of all implementation paths. Production adoption requires an +`docs/models/Provenance.tla` models an adversary against chain verification +symbolically: it can supply any chain and content, reuse published +signatures, and sign with a leaked author key, while the honest witness +attests only what the author intended. It is a PROOF-POLICY §4 exception, +reported as `TESTED` within its bounds (see `PROOF-NEEDS.adoc`). It is not a +cryptographic proof of ML-DSA or SHA3, nor a proof of all implementation +paths. Production adoption requires an approved contributor key and independent witness; historical records are never silently re-signed. @@ -124,7 +128,9 @@ the actual hosted runs still determine whether the workflows passed. Validation receipt, 2026-11-06: the Linux workspace suite passed 295 backend tests and seven signature/property tests (two existing documentation examples are ignored). The protocol crate also passed Windows tests and Clippy with -warnings denied. TLC 2.19 from tlaplus/tlaplus release v1.7.4 checked +warnings denied. Superseded 2026-11-09 (the model was rewritten because +its `Sign` action let any party sign any payload, so `Binding` held by +definition): TLC 2.19 from tlaplus/tlaplus release v1.7.4 checked `Provenance.cfg` with `Values = {a, b}`: 18,045,441 generated states, 68,096 distinct states, no invariant violation. SHA-256 of the checked model: `c379ece2393e2cacfffccd6bb0360184ad179c77ae72dc875948a022d123444a`. diff --git a/docs/models/Provenance.cfg b/docs/models/Provenance.cfg index a67c646..5a44964 100644 --- a/docs/models/Provenance.cfg +++ b/docs/models/Provenance.cfg @@ -1,3 +1,7 @@ +\* SPDX-License-Identifier: MPL-2.0 +\* Bounds: 2 digests, 6 records (2 roots, 4 children), chains of length 1-2. SPECIFICATION Spec -CONSTANT Values = {a, b} -INVARIANT Binding +CONSTANTS Digests = {d1, d2} + None = None + RequireWitness = TRUE +INVARIANTS TypeOK Unforgeable Linked diff --git a/docs/models/Provenance.tla b/docs/models/Provenance.tla index 6ac5f4e..9f543fc 100644 --- a/docs/models/Provenance.tla +++ b/docs/models/Provenance.tla @@ -1,31 +1,120 @@ --------------------------- MODULE Provenance --------------------------- -EXTENDS Naturals, Sequences, FiniteSets \* SPDX-License-Identifier: MPL-2.0 -\* Symbolic unforgeability: an attacker may change fields/content/links or -\* remove signatures, but cannot add a signature for a payload not signed. -CONSTANT Values -VARIABLES chain, authorSigned, witnessSigned, content, verified -vars == <> -Payloads == [field: Values, digest: Values, parent: Values] -Init == /\ chain = <<>> /\ authorSigned = {} /\ witnessSigned = {} - /\ content = <<>> /\ verified = FALSE -Sign == \E p \in Payloads: - /\ authorSigned' = authorSigned \cup {p} - /\ witnessSigned' = witnessSigned \cup {p} - /\ UNCHANGED <> -\* Any ordered pair, including a splice or substituted contribution. -Supply == \E a,b \in Payloads, x,y \in Values: - /\ chain' = <> /\ content' = <> - /\ verified' = FALSE - /\ UNCHANGED <> -Valid == /\ Len(chain) = 2 - /\ \A i \in 1..2: /\ chain[i] \in authorSigned - /\ chain[i] \in witnessSigned - /\ chain[i].digest = content[i] - /\ chain[2].parent = chain[1].field +\* +\* PROOF-POLICY section 4 exception record (standards 3-practice/PROOF-POLICY.adoc). +\* Obligation: an attacker who can supply any chain with any content bytes, +\* attach any published signature, and sign with the author's key once it +\* leaks, cannot obtain a "verified" verdict for a record the author did not +\* intend, or for a chain whose links or content do not match. The +\* independent witness required by docs/PROVENANCE-EXHIBIT-B.adoc is what +\* carries this after an author-key compromise. +\* Tool: TLA+ checked by TLC, a finite model check. Status: TESTED with the +\* bounds in Provenance.cfg, never PROVEN. +\* Why not the mapped verifiers: the property concerns an adversary +\* interleaving with honest parties, which pre/postconditions on +\* verify_chain do not state. The implementation obligations stay OPEN for +\* Creusot/Pearlite and Verus in PROOF-NEEDS.adoc. +\* Trust boundary: signatures and hashes are perfectly binding (symbolic +\* model); a record's hash is the record itself. Not a cryptographic proof, +\* not an implementation-correspondence proof. Author and witness keys +\* are not both compromised. +\* +\* Checked both ways: +\* Provenance.cfg RequireWitness = TRUE: Unforgeable, Linked hold. +\* ProvenanceNoWitness.cfg RequireWitness = FALSE: Unforgeable must FAIL +\* (author-key forgery), so the witness check is +\* load-bearing and the invariant is not vacuous. +\* ProvenanceReachable.cfg NeverVerified must FAIL: verified states exist. +EXTENDS Naturals, Sequences + +CONSTANTS Digests, \* content digests (finite set of model values) + None, \* model value: "no parent" + RequireWitness \* does the verifier demand a witness attestation? + +ASSUME None \notin Digests /\ RequireWitness \in BOOLEAN + +Roots == [digest: Digests, parent: {None}] +\* A child names its parent by the parent's hash. A root's hash is +\* determined by its digest (its parent is fixed), so at this depth the +\* parent link is the root's digest. +Children == [digest: Digests, parent: Digests] +Records == Roots \cup Children + +VARIABLES intended, \* records the honest author chose to publish + authorSigs, \* records carrying a valid author signature + witnessSigs, \* records carrying a valid witness attestation + compromised, \* has the author's private key leaked? + chain, \* the chain a verifier is handed + content, \* the content bytes (as digests) handed with it + verified \* the verifier's verdict on (chain, content) +vars == <> + +Init == /\ intended = {} /\ authorSigs = {} /\ witnessSigs = {} + /\ compromised = FALSE /\ chain = <<>> /\ content = <<>> + /\ verified = FALSE + +\* The honest author signs a record it intends. +AuthorSigns == \E r \in Records: + /\ intended' = intended \cup {r} + /\ authorSigs' = authorSigs \cup {r} + /\ UNCHANGED <> + +\* The honest, independent witness attests only records the author intended. +WitnessAttests == \E r \in intended: + /\ witnessSigs' = witnessSigs \cup {r} + /\ UNCHANGED <> + +\* The author's key leaks. +Compromise == /\ ~compromised + /\ compromised' = TRUE + /\ UNCHANGED <> + +\* After the leak the attacker signs anything with the author's key. +ForgeAuthor == /\ compromised + /\ \E r \in Records: authorSigs' = authorSigs \cup {r} + /\ UNCHANGED <> + +\* The attacker hands over any chain of one or two records with any content: +\* reordered, spliced, truncated or substituted. Signatures are public, so +\* every existing one is available to attach. +Supply == /\ \E n \in 1..2: + \E s \in [1..n -> Records], c \in [1..n -> Digests]: + /\ chain' = s + /\ content' = c + /\ verified' = FALSE + /\ UNCHANGED <> + +LinkOK(i) == IF i = 1 THEN chain[1].parent = None + ELSE /\ chain[i - 1].parent = None + /\ chain[i].parent = chain[i - 1].digest + +\* What verify_chain accepts as "verified" (all entries). +Valid == /\ Len(chain) \in 1..2 + /\ \A i \in 1..Len(chain): + /\ chain[i] \in authorSigs + /\ RequireWitness => chain[i] \in witnessSigs + /\ chain[i].digest = content[i] + /\ LinkOK(i) + Check == /\ verified' = Valid - /\ UNCHANGED <> -Next == Sign \/ Supply \/ Check + /\ UNCHANGED <> + +Next == AuthorSigns \/ WitnessAttests \/ Compromise \/ ForgeAuthor \/ Supply \/ Check Spec == Init /\ [][Next]_vars -Binding == verified => Valid + +TypeOK == /\ intended \subseteq Records /\ authorSigs \subseteq Records + /\ witnessSigs \subseteq intended /\ compromised \in BOOLEAN + /\ verified \in BOOLEAN + +\* A verified chain contains only records the author intended, each matching +\* the content it was handed. +Unforgeable == verified => \A i \in 1..Len(chain): + /\ chain[i] \in intended + /\ chain[i].digest = content[i] + +\* A verified chain starts at a root and every link names its predecessor. +Linked == verified => \A i \in 1..Len(chain): LinkOK(i) + +\* Expected to FAIL (ProvenanceReachable.cfg): a verified state is reachable. +NeverVerified == ~verified ============================================================================= diff --git a/docs/models/ProvenanceNoWitness.cfg b/docs/models/ProvenanceNoWitness.cfg new file mode 100644 index 0000000..fdc6085 --- /dev/null +++ b/docs/models/ProvenanceNoWitness.cfg @@ -0,0 +1,8 @@ +\* SPDX-License-Identifier: MPL-2.0 +\* Mutation check: without the witness requirement TLC must report an +\* Unforgeable violation (forgery with the leaked author key). +SPECIFICATION Spec +CONSTANTS Digests = {d1, d2} + None = None + RequireWitness = FALSE +INVARIANTS TypeOK Unforgeable diff --git a/docs/models/ProvenanceReachable.cfg b/docs/models/ProvenanceReachable.cfg new file mode 100644 index 0000000..2795bf5 --- /dev/null +++ b/docs/models/ProvenanceReachable.cfg @@ -0,0 +1,8 @@ +\* SPDX-License-Identifier: MPL-2.0 +\* Non-vacuity check: TLC must report a NeverVerified violation, showing a +\* verified state is reachable under the real verifier. +SPECIFICATION Spec +CONSTANTS Digests = {d1, d2} + None = None + RequireWitness = TRUE +INVARIANT NeverVerified diff --git a/docs/models/check-models.sh b/docs/models/check-models.sh new file mode 100755 index 0000000..5562bd4 --- /dev/null +++ b/docs/models/check-models.sh @@ -0,0 +1,59 @@ +#!/usr/bin/env bash +# SPDX-License-Identifier: MPL-2.0 +# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +# +# check-models.sh TLA2TOOLS_JAR — model-check docs/models/Provenance.tla both +# ways (PROOF-POLICY §4: a finite model check is TESTED, with its bounds): +# +# Provenance.cfg must find no error (Unforgeable, Linked hold); +# ProvenanceNoWitness.cfg must report Unforgeable violated (mutation); +# ProvenanceReachable.cfg must report NeverVerified violated (non-vacuity). +# +# The jar must be TLC 2.19 (tlaplus release v1.7.4) with the pinned digest; +# anything else fails. A missing java or jar is a failure, never a skip. +set -uo pipefail +JAR="${1:?usage: check-models.sh TLA2TOOLS_JAR}" +JAR_SHA256="936a262061c914694dfd669a543be24573c45d5aa0ff20a8b96b23d01e050e88" +cd -- "$(dirname -- "${BASH_SOURCE[0]}")" || exit 1 +fail=0 +die() { printf 'FAIL: %s\n' "$1"; exit 1; } +command -v java >/dev/null || die "java not on PATH" +[ -f "$JAR" ] || die "no jar at $JAR" +got="$(sha256sum "$JAR" | cut -d' ' -f1)" +[ "$got" = "$JAR_SHA256" ] || die "tla2tools.jar digest $got, expected $JAR_SHA256" +echo "model sha256: $(sha256sum Provenance.tla | cut -d' ' -f1)" +OUT="$(mktemp -d)" + +# run CFG LOG: run TLC on Provenance.tla with CFG, output to LOG. +run() { + java -XX:+UseParallelGC -cp "$JAR" tlc2.TLC -workers auto \ + -metadir "$OUT/meta-$1" -config "$1" Provenance > "$2" 2>&1 +} + +run Provenance.cfg "$OUT/holds.log"; st=$? +grep -m1 -E '^TLC2 Version' "$OUT/holds.log" || true +grep -q '^TLC2 Version 2\.19 ' "$OUT/holds.log" || die "TLC is not version 2.19" +if [ "$st" -eq 0 ] && grep -q 'Model checking completed. No error has been found' "$OUT/holds.log"; then + grep -E 'states generated|depth of the complete state graph' "$OUT/holds.log" + echo "PASS: Provenance.cfg — TypeOK, Unforgeable and Linked hold" +else + tail -40 "$OUT/holds.log"; echo "FAIL: Provenance.cfg (exit $st)"; fail=1 +fi + +run ProvenanceNoWitness.cfg "$OUT/nowitness.log" +if grep -q 'Invariant Unforgeable is violated' "$OUT/nowitness.log"; then + echo "PASS: ProvenanceNoWitness.cfg — forgery found without the witness check" +else + tail -40 "$OUT/nowitness.log"; echo "FAIL: ProvenanceNoWitness.cfg found no forgery"; fail=1 +fi + +run ProvenanceReachable.cfg "$OUT/reachable.log" +if grep -q 'Invariant NeverVerified is violated' "$OUT/reachable.log"; then + echo "PASS: ProvenanceReachable.cfg — a verified state is reachable" +else + tail -40 "$OUT/reachable.log"; echo "FAIL: ProvenanceReachable.cfg reached no verified state"; fail=1 +fi + +rm -rf "$OUT" +[ "$fail" -eq 0 ] || { echo "PROVENANCE MODEL CHECK FAILED"; exit 1; } +echo "OK: provenance model checked both ways" diff --git a/panel-clades/scripts/check-abi.sh b/panel-clades/scripts/check-abi.sh index 9a189b2..d366932 100755 --- a/panel-clades/scripts/check-abi.sh +++ b/panel-clades/scripts/check-abi.sh @@ -16,7 +16,9 @@ # # A missing toolchain is a failure, never a skip. Every module under # src/abi/PanelClades/ must be listed in the ipkg (an unlisted one would be -# skipped silently), and none may use an escape hatch. +# skipped silently). No module in the import cone (PanelClades and the +# typed-wasm kernel at its pin) may use an escape hatch, leave a hole or opt +# out of totality: scripts/scan-escape-hatches.sh. set -uo pipefail cd -- "$(dirname -- "${BASH_SOURCE[0]}")/.." || exit 1 ROOT="$(pwd)" @@ -47,10 +49,10 @@ for f in "${abi_files[@]}"; do grep -qE "^[[:space:]]*(modules[[:space:]]*=|,)[[:space:]]*${mod//./\\.}[[:space:]]*$" "$IPKG" \ || err "$mod is not listed in $IPKG (it would never be checked)" done -if grep -nE '\b(believe_me|assert_total|assert_smaller|idris_crash|unsafePerformIO|postulate)\b' "${abi_files[@]}"; then - err "escape hatch in src/abi/PanelClades (lines above)" +if ! bash scripts/scan-escape-hatches.sh "${abi_files[@]}"; then + err "escape hatch, hole or totality opt-out in src/abi/PanelClades (lines above)" fi -[ "$fail" -eq 0 ] && pass "every PanelClades module is listed in the ipkg; no escape hatches" +[ "$fail" -eq 0 ] && pass "every PanelClades module is listed in the ipkg; no escape hatches, holes or partial code" if bash scripts/gen-budgets.sh --check; then pass "Budgets.idr is current with the clade configs" else @@ -59,6 +61,18 @@ fi bash scripts/fetch-siblings.sh || die "could not fetch typed-wasm at its pin" TW="_build/dependencies/typed-wasm/src/abi" +# The kernel is part of the proofs' import cone: it is checked, not assumed, +# only if it is free of escape hatches and holes too. +kernel_list="$OUT/kernel-files" +find "$TW/TypedWasm" -type f -name '*.idr' -print0 > "$kernel_list" \ + || die "could not enumerate typed-wasm kernel sources" +mapfile -d '' -t kernel_files < "$kernel_list" +[ "${#kernel_files[@]}" -gt 0 ] || die "no typed-wasm kernel sources under $TW/TypedWasm" +if bash scripts/scan-escape-hatches.sh "${kernel_files[@]}"; then + pass "typed-wasm import cone (${#kernel_files[@]} modules): no escape hatches, holes or partial code" +else + err "escape hatch, hole or totality opt-out in the typed-wasm kernel (lines above)" +fi rm -rf "$TW/build" if ! (cd "$TW" && idris2 --build typed-wasm.ipkg) > "$OUT/kernel.log" 2>&1 \ || grep -q '^Error' "$OUT/kernel.log"; then diff --git a/panel-clades/scripts/scan-escape-hatches.sh b/panel-clades/scripts/scan-escape-hatches.sh new file mode 100755 index 0000000..39ed7f9 --- /dev/null +++ b/panel-clades/scripts/scan-escape-hatches.sh @@ -0,0 +1,41 @@ +#!/usr/bin/env bash +# SPDX-License-Identifier: MPL-2.0 +# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +# +# scan-escape-hatches.sh FILE.idr... — fail if any Idris2 source in the +# proof's import cone weakens it: +# +# * an escape hatch (believe_me, assert_total, assert_smaller, idris_crash, +# unsafePerformIO, postulate); +# * a hole (`?name`): idris2 --build accepts a module with unsolved holes, +# so a theorem body `?todo` would otherwise pass the gate; +# * a module without `%default total`, or one that opts out with +# `partial` / `covering`. +# +# Comments (`--` to end of line, `|||` doc lines) are ignored, so prose that +# names a hatch is not a finding. Neither tree uses `{- -}` block comments; +# a file that does is refused rather than scanned wrongly. +# Exit 0 when every file is clean, 1 otherwise; a missing file is a failure. +set -uo pipefail +[ "$#" -gt 0 ] || { echo "scan-escape-hatches: no files given" >&2; exit 1; } +HATCH='(^|[^A-Za-z0-9_'"'"'.])(believe_me|assert_total|assert_smaller|idris_crash|unsafePerformIO|postulate)([^A-Za-z0-9_'"'"']|$)' +HOLE='(^|[^A-Za-z0-9_'"'"'?])\?[A-Za-z_]' +OPTOUT='^[[:space:]]*(partial|covering)([[:space:]]|$)|%default[[:space:]]+(partial|covering)' +bad=0 +for f in "$@"; do + if [ ! -f "$f" ]; then echo "MISSING: $f"; bad=1; continue; fi + if grep -q '{-' "$f"; then echo "BLOCK-COMMENT (not scannable): $f"; bad=1; continue; fi + code="$(sed -E -e 's/^[[:space:]]*\|\|\|.*$//' -e 's/--.*$//' "$f")" + if hits="$(printf '%s\n' "$code" | grep -nE "$HATCH")"; then + printf '%s\n' "$hits" | sed "s|^|ESCAPE-HATCH $f:|"; bad=1 + fi + if hits="$(printf '%s\n' "$code" | grep -nE "$HOLE")"; then + printf '%s\n' "$hits" | sed "s|^|HOLE $f:|"; bad=1 + fi + if hits="$(printf '%s\n' "$code" | grep -nE "$OPTOUT")"; then + printf '%s\n' "$hits" | sed "s|^|TOTALITY-OPT-OUT $f:|"; bad=1 + fi + printf '%s\n' "$code" | grep -qE '^[[:space:]]*%default[[:space:]]+total([[:space:]]|$)' \ + || { echo "NOT-TOTAL (no %default total): $f"; bad=1; } +done +exit "$bad"