Repository navigation
docs(proofs): allocate provenance obligations to Creusot and Verus #179
There are no files selected for viewing
| Original file line number | Diff line number | Diff line change |
|---|---|---|
|
|
@@ -185,10 +185,57 @@ 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. | ||
|
|
||
| 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 | ||
|
Comment on lines
+198
to
+200
There was a problem hiding this comment.
The desktop's actual verification path is Useful? React with 👍 / 👎. |
||
| claimed ancestry to later verdicts. | ||
|
hyperpolymath marked this conversation as resolved.
Resolved
|
||
| |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 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 | ||
| |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 | ||
|
hyperpolymath marked this conversation as resolved.
Resolved
|
||
| 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. | ||
|
Comment on lines
+216
to
+219
There was a problem hiding this comment.
The total-dispatch obligation is not solely a property of the Rust implementation: it asserts that every AffineScript frontend invocation matches a registered Rust handler, so it is an interface/protocol invariant shared across languages. The cited policy assigns such API, dispatch, and ordering contracts to Idris2 while reserving Creusot for behavior on first-party Rust code; assigning this entire obligation only to Rust verifiers leaves the frontend-to-backend correspondence without its required proof. Split out an Idris2 interface contract and retain Creusot only for implementation-level properties of the Rust dispatcher. See the policy's interface-versus-implementation mapping. Useful? React with 👍 / 👎. |
||
| |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 | ||
|
|
||
|
|
||
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.
This allocation contradicts the cited normative policy:
PROOF-POLICY.adocmaps first-party Rust exclusively to Creusot, contains no §1.2, and explicitly states that Verus is not a standing exception because it shares Creusot's SMT trust base. Unless a separately recorded §4 exception exists, the Verus rows therefore direct future work toward a noncompliant proof strategy rather than following the claimed owner ruling. See the policy's Rust mapping and exception rules.Useful? React with 👍 / 👎.