From 3f2015e157035b9122cedfeb4a718761be7021b9 Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com> Date: Sat, 7 Nov 2026 19:18:16 +0000 Subject: [PATCH 1/2] docs(proofs): allocate provenance Creusot and Verus obligations --- PROOF-NEEDS.adoc | 44 ++++++++++++++++++++++++++++++++++++++++---- 1 file changed, 40 insertions(+), 4 deletions(-) diff --git a/PROOF-NEEDS.adoc b/PROOF-NEEDS.adoc index 9521720..f0ff7f5 100644 --- a/PROOF-NEEDS.adoc +++ b/PROOF-NEEDS.adoc @@ -185,10 +185,46 @@ prevent tail truncation without a checkpoint, or prove cryptographic hardness. == 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. +existing modules and the typed-wasm kernel they import. + +First-party Rust follows standards `3-practice/PROOF-POLICY.adoc` ยง1.2 +(owner ruling 2026-11-07): *Creusot* with *Pearlite* contracts, plus *Verus*. +Tests and the bounded TLA+ model do not discharge implementation obligations. +Pearlite is Creusot's specification language, not an independent prover. + +[cols="2,2,3,3",options="header"] +|=== +|Implementation entrypoint |Verifier and status |Planned obligation |Trust boundary / next action +|`crates/provenance/src/lib.rs`: `Registry::new`, `verify_chain` +|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. +|`crates/provenance/src/lib.rs`: `verify_entry`, `verify_witnesses` +|Verus: OPEN +|A verified verdict requires 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 +|Dependency boundary: ASSUMED +|JCS encoding, SHA3-256, ML-DSA-65, OS entropy and time parsing behave as specified. +|Third-party crates remain unmodified. Record the exact locked versions and +extern contracts 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 +|Allocate implementation contracts after writing the dispatch/propagation +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. +|=== + +Any future proof receipt must name source/tool/solver versions, invocation, +discharged obligations and assumptions. Shared SMT solvers or specifications +do not establish independent witnesses. Approved contributor keys, independent +witnesses and trusted checkpoints remain separate operational requirements. == Priority From 351f9b4c6a9fe94529aa470aa7a6d5bcee469a1b Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com> Date: Sat, 7 Nov 2026 19:34:43 +0000 Subject: [PATCH 2/2] Specify recording completeness and first-party wrapper proofs --- PROOF-NEEDS.adoc | 21 ++++++++++++++++----- 1 file changed, 16 insertions(+), 5 deletions(-) diff --git a/PROOF-NEEDS.adoc b/PROOF-NEEDS.adoc index f0ff7f5..cfadd97 100644 --- a/PROOF-NEEDS.adoc +++ b/PROOF-NEEDS.adoc @@ -201,16 +201,27 @@ Pearlite is Creusot's specification language, not an independent prover. 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) +|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 -|A verified verdict requires valid author binding and every declared independent -witness; rejected or missing evidence cannot promote a verdict. +|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 -|Dependency boundary: ASSUMED -|JCS encoding, SHA3-256, ML-DSA-65, OS entropy and time parsing behave as specified. -|Third-party crates remain unmodified. Record the exact locked versions and +|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. |`src-gossamer/src/ipc.rs` dispatch and `tools/pcc` propagation