From a11e82d3ce1e109faf4afac9a2a53b8c811c6501 Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 9 Nov 2026 14:11:56 +0000 Subject: [PATCH 1/2] fix(proofs): reconcile the proof ledger with PROOF-POLICY; make the gates check what they claim MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit - panel-clades: new scripts/scan-escape-hatches.sh, run by check-abi.sh over the whole import cone (PanelClades and typed-wasm's kernel at 117bbf8). It fails on escape hatches, holes (`?name`: idris2 --build accepts them, so a theorem body `?todo` passed before), partial/covering, and a module without %default total. Comments are ignored. Checked both ways: both trees pass; planted hole, believe_me, assert_total, partial and a missing %default total each fail. - docs/models/Provenance.tla: the old Sign action let any party sign any payload, so Binding held by definition. The model now separates the honest author and witness from an attacker who supplies any chain and content, reuses published signatures, and signs with a leaked author key. New CI job provenance-model runs docs/models/check-models.sh (TLC 2.19, jar SHA-256 pinned): Unforgeable and Linked must hold, a forgery must be found with the witness check removed, and a verified state must be reachable. The 2026-11-06 TLC receipt is marked superseded. - PROOF-NEEDS.adoc: closed §5 status tokens on every row; import cone record (§1.1); TLA+ §4 exception record; §6 toolchain deviations for the Idris2 and TLC lanes; PWG not applicable (no theory obligations, §8.1); locked versions of ASSUMED crypto/JCS dependencies; PanLL's provenance profile stated as narrower than Exhibit B (ML-DSA-65 only, witness required, .well-known/keys/ only), which the #172 review asked for; decDivides described as a semi-decision; the struct-size bound needs align >= 1. Receipts: Build Validation 42408104327 (panel-clades-abi green on 7d1feaa); cargo test -p panll-provenance --locked: 7 passed. The new scan and TLC job get their first receipts from this change's CI run. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01SJtjqoZaSQo7uBwvwVMA9G --- .github/workflows/build-validation.yml | 30 +- CHANGELOG.adoc | 17 ++ PROOF-NEEDS.adoc | 299 +++++++++++++++----- docs/PROVENANCE-EXHIBIT-B.adoc | 14 +- docs/models/Provenance.cfg | 8 +- docs/models/Provenance.tla | 141 +++++++-- docs/models/ProvenanceNoWitness.cfg | 8 + docs/models/ProvenanceReachable.cfg | 8 + docs/models/check-models.sh | 59 ++++ panel-clades/scripts/check-abi.sh | 22 +- panel-clades/scripts/scan-escape-hatches.sh | 41 +++ 11 files changed, 537 insertions(+), 110 deletions(-) create mode 100644 docs/models/ProvenanceNoWitness.cfg create mode 100644 docs/models/ProvenanceReachable.cfg create mode 100755 docs/models/check-models.sh create mode 100755 panel-clades/scripts/scan-escape-hatches.sh diff --git a/.github/workflows/build-validation.yml b/.github/workflows/build-validation.yml index 96cb85b1..83421eac 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,28 @@ 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 + 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 --retry 3 -o "$RUNNER_TEMP/tla2tools.jar" "$TLA2TOOLS_URL" + + - 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 4f23bd0d..a1b2258c 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 cfadd97a..fd12f42f 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 a364e1ce..7138360f 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 a67c6463..5a449644 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 6ac5f4e1..9f543fc2 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 00000000..fdc6085a --- /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 00000000..2795bf5e --- /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 00000000..5562bd4a --- /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 9a189b21..d366932a 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 00000000..39ed7f9c --- /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" From 66fb64df6bc3598e4b540065d6410612ea569638 Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 9 Nov 2026 14:14:28 +0000 Subject: [PATCH 2/2] ci(provenance-model): fetch TLC over HTTPS only and check its digest in the fetch step SonarCloud rated the new job's `curl -L` C for security: following redirects without --proto lets a redirect downgrade the protocol. Restrict both the request and redirects to HTTPS (TLS 1.2+), and verify the pinned SHA-256 in the same step as the download; check-models.sh still checks it again before running TLC. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01SJtjqoZaSQo7uBwvwVMA9G --- .github/workflows/build-validation.yml | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/.github/workflows/build-validation.yml b/.github/workflows/build-validation.yml index 83421eac..e20e3104 100644 --- a/.github/workflows/build-validation.yml +++ b/.github/workflows/build-validation.yml @@ -101,6 +101,7 @@ jobs: 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 @@ -108,7 +109,10 @@ jobs: persist-credentials: false - name: Fetch TLC 2.19 (tla2tools v1.7.4) - run: curl -fsSL --retry 3 -o "$RUNNER_TEMP/tla2tools.jar" "$TLA2TOOLS_URL" + 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"