diff --git a/.github/workflows/dogfood-proofs-ci.yml b/.github/workflows/dogfood-proofs-ci.yml index 141953ff..9191997e 100644 --- a/.github/workflows/dogfood-proofs-ci.yml +++ b/.github/workflows/dogfood-proofs-ci.yml @@ -78,6 +78,9 @@ jobs: steps: - uses: actions/checkout@v7.0.1 + # PROOF-POLICY §6 deviation (open): Lean is not in the Guix manifest and the + # container has no Lean stage. Recorded in docs/PROOF-STATUS.adoc, + # "Toolchain deviations". - name: Install elan + pinned Lean toolchain run: | set -euo pipefail @@ -130,6 +133,9 @@ jobs: steps: - uses: actions/checkout@v7.0.1 + # PROOF-POLICY §6 deviation (open): Lean is not in the Guix manifest and the + # container has no Lean stage. Recorded in docs/PROOF-STATUS.adoc, + # "Toolchain deviations". - name: Install elan + pinned Lean toolchain run: | set -euo pipefail @@ -180,6 +186,9 @@ jobs: steps: - uses: actions/checkout@v7.0.1 + # PROOF-POLICY §6 deviation (open): Idris 2 is not in the Guix manifest and no + # container stage installs it. Recorded in docs/PROOF-STATUS.adoc, + # "Toolchain deviations". - name: Install Idris2 run: | set -euo pipefail diff --git a/.github/workflows/idris2-abi-ci.yml b/.github/workflows/idris2-abi-ci.yml index 8ea18c7b..f14898dc 100644 --- a/.github/workflows/idris2-abi-ci.yml +++ b/.github/workflows/idris2-abi-ci.yml @@ -62,6 +62,9 @@ jobs: echo "Non-PR event — running full type-check." fi + # PROOF-POLICY §6 deviation (open): Idris 2 is not in the Guix manifest and no + # container stage installs it. Recorded in docs/PROOF-STATUS.adoc, + # "Toolchain deviations". - name: Install Idris2 if: steps.detect.outputs.relevant == 'true' run: | diff --git a/Cargo.lock b/Cargo.lock index 0bf91e23..0592b0e7 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -133,7 +133,7 @@ version = "1.1.5" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "40c48f72fd53cd289104fc64099abca73db4166ad86ea0b4341abe65af83dadc" dependencies = [ - "windows-sys 0.60.2", + "windows-sys 0.61.2", ] [[package]] @@ -144,7 +144,7 @@ checksum = "291e6a250ff86cd4a820112fb8898808a366d8f9f58ce16d1f538353ad55747d" dependencies = [ "anstyle", "once_cell_polyfill", - "windows-sys 0.60.2", + "windows-sys 0.61.2", ] [[package]] @@ -640,7 +640,7 @@ version = "3.1.1" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "faf9468729b8cbcea668e36183cb69d317348c2e08e994829fb56ebfdfbaac34" dependencies = [ - "windows-sys 0.52.0", + "windows-sys 0.61.2", ] [[package]] @@ -1246,7 +1246,7 @@ source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "39cab71617ae0d63f51a36d69f866391735b51691dbda63cf6f96d042b63efeb" dependencies = [ "libc", - "windows-sys 0.52.0", + "windows-sys 0.61.2", ] [[package]] @@ -2093,7 +2093,7 @@ version = "0.50.3" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "7957b9740744892f114936ab4a57b3f487491bbeafaf8083688b16841a4240e5" dependencies = [ - "windows-sys 0.60.2", + "windows-sys 0.61.2", ] [[package]] @@ -2837,20 +2837,22 @@ dependencies = [ [[package]] name = "rmcp" -version = "3.5.0" +version = "3.9.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "fae7019994ae0fe4ada40b732f798f3ff26f0f04facb1477f1bf37eb4f18a2d3" +checksum = "d24a7e92f4bcaa36b97fa93c4fa7ca8f3e669eced949345b3462dba333c7f909" dependencies = [ "base64 0.23.1", "chrono", "futures", "indexmap", + "libc", "pastey", "pin-project-lite", "rmcp-macros", "schemars", "serde", "serde_json", + "sha2 0.11.0", "thiserror", "tokio", "tokio-util", @@ -2860,9 +2862,9 @@ dependencies = [ [[package]] name = "rmcp-macros" -version = "3.5.0" +version = "3.9.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "c7e66877136e969d5a2d561ee5841b17717a0619aebd64abb47a2a2f46e34683" +checksum = "b3140f24a766f80f9ec1607bde85680959a69b83d46fa9ce87dadab7e67ab029" dependencies = [ "darling 0.24.0", "proc-macro2", @@ -2910,7 +2912,7 @@ dependencies = [ "errno", "libc", "linux-raw-sys", - "windows-sys 0.52.0", + "windows-sys 0.61.2", ] [[package]] @@ -3251,7 +3253,7 @@ source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "52d1cfed4120b4d927bf7c0f86d2087a4a7d6027c906d9f9d525a80573b9be51" dependencies = [ "libc", - "windows-sys 0.60.2", + "windows-sys 0.61.2", ] [[package]] @@ -3391,10 +3393,10 @@ source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "32497e9a4c7b38532efcdebeef879707aa9f794296a4f0244f6f69e9bc8574bd" dependencies = [ "fastrand", - "getrandom 0.4.2", + "getrandom 0.3.4", "once_cell", "rustix", - "windows-sys 0.52.0", + "windows-sys 0.61.2", ] [[package]] @@ -4198,7 +4200,7 @@ version = "0.1.11" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "c2a7b1c03c876122aa43f3020e6c3c3ee5c05081c9a00739faf7503aeba10d22" dependencies = [ - "windows-sys 0.52.0", + "windows-sys 0.61.2", ] [[package]] diff --git a/docs/PROOF-STATUS.adoc b/docs/PROOF-STATUS.adoc index bcf6c700..f8b1591d 100644 --- a/docs/PROOF-STATUS.adoc +++ b/docs/PROOF-STATUS.adoc @@ -3,12 +3,14 @@ = Proof status — policy-vocabulary view -*Status*: reviewed 2026-11-04. Each row is scoped to its recorded source -identity and check; this file does not claim a single revision was checked -for every obligation. +*Status*: reviewed 2026-11-09 against main `+2ab7574ae1e574b0e881422fde6252bf79dea178+`. +Each row is scoped to its recorded source identity and check; this file does +not claim a single revision was checked for every obligation. *Normative policy*: `+3-practice/PROOF-POLICY.adoc+` in -https://github.com/metadatastician/standards[metadatastician/standards] (owner -ruling 2026-10-26). +https://github.com/metadatastician/standards[metadatastician/standards], read +at commit `+b8f60511e76c9015d86990317162dce653c92fe1+` (owner rulings +2026-10-26, 2026-11-04 for §8 Proof Witness Grades, and 2026-11-07 for §1.2 +Creusot, Pearlite and Verus). This is ECHIDNA's *proof-status file* in the sense `+PROOF-POLICY+` uses the term: the place each obligation's ledger row lives, in the closed vocabulary of @@ -62,33 +64,45 @@ CI gate exists and the authors say it passes" when no receipt is cited. |Not done. |=== -=== Relation to the Mathesis grades +=== Proof Witness Grades (`+PROOF-POLICY+` §8) -https://github.com/hyperpolymath/mathesis[mathesis], *Estate-wide Mathematical -Knowledge Architecture* §5, grades a *theorem* by how far its witness has -travelled: **Grade 3** type-checks locally in its home system and is not -translated; **Grade 2i/2ii** one / two independent translations with statement -correspondence recorded; **Grade 1** machine-checked through a verified checker -API in headless CI. +A Proof Witness Grade (`+PWG-3+`, `+PWG-2i+`, `+PWG-2ii+`, `+PWG-1+`; lower is +stronger) counts the independent machine-checked witnesses of a *theory* +theorem. It is not a §5 status token and not a §2.2 correspondence state, and +each record below carries all three separately. It is always written with its +`+PWG-+` prefix; the earlier "Mathesis Grade" wording in this file is retired +because §8 forbids a bare "Grade". -The two vocabularies are orthogonal — one grades a theorem's reach, the other -records whether a repository's obligation was discharged — but they interact: +* PWG applies only to theory obligations (§8.1). Engineering proofs (Idris2, + Creusot/Pearlite and Verus, SPARK) use §5 tokens only and carry no grade. +* A theory theorem below `+PWG-3+` is `+ungraded+`. +* Grades are derived from receipts (§8.4), never asserted. A grade census, if + published, is a count per grade with its denominator, never a percentage. -* A home-system leg may be `+proven+` while every independent leg is `+open+`. - That combination *is* Grade 3, and it is the ceiling for anything in this - repository. -* A translation leg is `+argued+`, not `+proven+`, until the statement - correspondence is recorded (`+PROOF-POLICY+` §2: "`the kernel checks the term - only against the translated statement`"). +[width="100%",cols="22%,10%,12%,56%",options="header"] +|=== +|Theory theorem |`+pwg+` |`+foundation_diverse+` |Legs (route, §5 token, §2.2 state, receipt) + +|Receipt/warrant separation, `+meta-checker/src/Echidna/Receipt.agda+` (R11) +|`+3+` +|`+false+` +|*Agda*: source, `+proven+`, `+AGDA-VERIFIED+`, hosted run +https://github.com/hyperpolymath/echidna/actions/runs/42551607796[42551607796] +on `+2ab7574+`. *Rocq*: `+open+`, `+BRIDGE-PENDING+`, no receipt. *Lean*: +`+open+`, `+BRIDGE-PENDING+`, no receipt. Owes both recheck legs (§8.4.1). +|=== -Mathesis §6 forbids flattening assurance into a percentage. See R5 and R6. +The other meta-checker modules (R4, R9, R10) state properties of this +repository's own types, so under §1 they are engineering, not theory, and are +not graded here. They stay `+proven+` in Agda until the split recorded under +R4 replaces each with Creusot/Verus contracts on the Rust (R1). == Obligations Grouped by the `+PROOF-POLICY+` §1 mapping, because that is what decides which verifier is even allowed to carry the row. -=== Rust — Creusot (§1: first-party Rust) +=== Rust — Creusot with Pearlite, and Verus (§1, §1.2: first-party Rust) [width="100%",cols="24%,13%,38%,25%",options="header"] |=== @@ -96,11 +110,21 @@ verifier is even allowed to carry the row. |R1. Trust pipeline, dispatch, arbitration, Pareto |`+open+` -|`+PROOF-POLICY+` §1 maps first-party Rust to Creusot. -|`+crates/echidna-core-creusot+` describes itself as "`Creusot-annotated (not -yet proved)`"; the `+creusot+` dev-dependency is commented out and the crate -builds on stable Rust behind a `+creusot+` feature. Annotation is not proof. Row -stays `+open+` until a Creusot run yields a receipt with a commit hash. +|`+PROOF-POLICY+` §1 and §1.2 (owner ruling 2026-11-07) make *Creusot*, with +*Pearlite* contracts, and *Verus* the default toolset for first-party Rust. +Pearlite is Creusot's specification language, not a third verifier. +|*Creusot/Pearlite*: `+crates/echidna-core-creusot+` describes itself as +"`Creusot-annotated (not yet proved)`"; the `+creusot+` dev-dependency is +commented out and the crate builds on stable Rust behind a `+creusot+` feature. +The `+formal-verification.yml+` Creusot job runs only on manual dispatch and has +no recorded receipt. Annotation is not proof. *Verus*: not started; no +specification, proof code or toolchain exists in this repository. Next action +for both: contracts on `+src/rust/verification/confidence.rs+`, +`+src/rust/integrity/solver_integrity.rs+` and `+src/rust/dispatch.rs+`, checked +against the statements the R4 design review lists. #477 starts this for +`+compute_trust_level+` (one `+echidna_core::trust+` kernel, Creusot `+ensures+` +TK-4/TK-5, recorded there as `+tested-only+`). The row stays `+open+` +until each verifier yields a receipt with a commit hash. |=== @@ -118,17 +142,26 @@ ABI row and the Stage-8a trio as constructively proved, all in |R2. Idris 2 interface/ABI obligations (E2, E3, E5, E6, E7, E12, Stage 8a, VQL-UT, extensive ABI) -|`+argued+` +|`+proven+` for the eleven `+verification/proofs/idris2+` modules. The +`+src/abi+` modules they import were built in the same job as their dependency; +the rest of `+src/abi+` keeps its `+idris2-abi-ci.yml+` gate and is not +re-scored here. |`+PROOF-POLICY+` §1 maps ABIs and engineering properties to Idris 2. The artefacts exist and are detailed in `+PROOF-NEEDS+`. -|No `+idris2 --build+` receipt for -`+verification/proofs/idris2/echidna-verif-proofs.ipkg+` is cited with a commit -hash. Promote to `+proven+` by citing a green run and its commit — that is a -one-line change, and it is the cheapest upgrade in this file. +|Receipt: the *Idris2 (verification)* job of the Dogfood Proof Corpus workflow, +https://github.com/hyperpolymath/echidna/actions/runs/42100322554/job/127501094018[job +127501094018] on `+a81467bbbf0b142dc016eda7c9b16b55d3962734+`, built +`+echidna-verif-proofs.ipkg+` with all eleven modules listed in it (1/11 to +11/11, `+ClampTrustBounds+` included) and exit 0. No proof source changed between +`+a81467b+` and `+2ab7574+`. The package depends on the installed +`+echidnaabi+` package from `+src/abi+`. A source scan of the eleven modules +finds `+believe_me+`, `+assert_total+` and `+postulate+` only inside strings and +comments. Trust boundary: the Idris 2 compiler installed by that job (Ubuntu +`+idris2+` package, else a v0.8.0 source build; see Toolchain deviations). |=== -=== Lean 4 — cross-checks and algebraic properties (§4 exceptions) +=== Lean 4 — engineering properties held outside Idris 2 (§3 re-homing pending) [width="100%",cols="24%,13%,38%,25%",options="header"] |=== @@ -137,15 +170,29 @@ one-line change, and it is the cheapest upgrade in this file. |R3. Lean 4 legs: E4-L4 `+ConfidenceLattice.lean+`, E10 `+ParetoMaximality.lean+` / `+ParetoStrongMaximality.lean+`, E11 `+IntegrityVerification.lean+`, E13 `+PortfolioCompleteness.lean+` -|`+open+` -|Directly recorded: `+lake build+` run 2026-05-18 (Lean 4.13.0) — *all five -fail to compile*, 49 / 2 / 1 / 5 / 31 errors, three root causes -(`+unfold_let+` removed in 4.13.0; Mathlib tactics under a zero-mathlib -lakefile; instance synthesis and module resolution). -|Nothing. This row is correct and must not be softened. `+PROOF-NEEDS+` records -that `+ConfidenceLattice.lean+` was left byte-identical and that the -`+unfold_let+` token-swap made it worse (104 errors). The open decision is -Mathlib-vs-core, which is an owner call. +|`+proven-with-postulates+` (109 of 167 theorems need no axiom; the other 58 +use only Lean core's standard axioms, listed in the next column) +|Hosted receipt: the *Lean 4 (verification)* job, +https://github.com/hyperpolymath/echidna/actions/runs/42100322554/job/127501093731[job +127501093731] on `+a81467b+`, built all five roots of +`+verification/proofs/lean4/lakefile.lean+` with Lean 4.13.0 and no Mathlib +(`+lake-manifest+` has no packages). No proof source changed up to `+2ab7574+`. +Local recheck on 2026-11-09 with the release archive of Lean 4.13.0 (commit +`+6d22e0e5cc5a+`, archive SHA-256 +`+44ceeac7ee4c98d177bfb4a3e5c210555c87e75b08807b68d523237fe4f09997+`): +`+lake build+` succeeded, and `+Lean.collectAxioms+` over every non-internal +theorem of the five modules found 167 theorems. 109 depend on no axiom. 58 +depend only on `+propext+` (58), `+Quot.sound+` (22) and `+Classical.choice+` +(9). There is no `+sorryAx+` and no project-declared axiom. +|The 2026-05-18 record of five failing files is superseded by these receipts. +Its Mathlib-versus-core question is closed by `+PROOF-POLICY+` §2 ("`No +Mathlib`"), and the corpus builds without Mathlib. *Classification:* these files +state properties of this repository's own types, so under §1 they are +engineering, not theory, and they are not a Lean recheck leg for any Agda +theorem. Under §3 they are re-homed when next touched, unless a §4 exception is +recorded: a statement about Rust behaviour (such as `+ConfidenceLattice+`) goes +to Creusot/Verus on the code, an API or ABI property to Idris 2. Until then they +stay, labelled with their prover. |=== @@ -159,7 +206,21 @@ Mathlib-vs-core, which is an owner call. axiom-tracker completeness, integrity, clamp bounds, receipt/warrant (9 modules) |`+proven+` |First-party Agda in `+meta-checker/src/+`, type-checked with the §2.1 -canonical invocation. The reproducible local receipt is +canonical invocation. +*Current receipt (exact commit):* the scheduled Agda Meta-Checker run +https://github.com/hyperpolymath/echidna/actions/runs/42551607796[42551607796] +on main `+2ab7574ae1e574b0e881422fde6252bf79dea178+` passed, using the pinned +`+scripts/ci/setup-agda.sh+` and `+scripts/ci/check-agda.sh+`. A local recheck of +the same commit on 2026-11-09 also passed: 9 of 9 modules produced fresh +interfaces, the receipt controls accepted the two witnesses and rejected the +three planted claims, and there were 55 `+UnsupportedIndexedMatch+` warnings at +the same six sites. The Agda executable SHA-256 matched +`+6de41437c14c05c9fe576d724cc67386444c0fa9fee662a08250fefb91bee8b6+`. The standard +library came from the `+v2.1+` git tag, commit `+97bc55e+`, because that +session's network refused the archive host; see Toolchain deviations. Every +source digest at `+2ab7574+` equals the corresponding digest in the earlier +receipt below. +*Earlier local receipt:* link:reports/2026-11-04-agda-meta-checker-receipt.json[`+2026-11-04-agda-meta-checker-receipt.json+`]. It records base commit `+9dd7847dfb095f0ddf3d41bac3327fcc4486fb6b+` plus the exact SHA-256 of every checked source and library descriptor, and names @@ -195,6 +256,46 @@ invalidate its use for that changed source until a fresh check is recorded. The earlier 2026-11-01 timing/count report is historical, not the evidence for the current `+proven+` row; the source-bound 2026-11-04 receipt replaces it. +**Classification (§1), decided 2026-11-09:** only `+Receipt+` states theory. +`+TrustLevel+`, `+AxiomSafety+`, `+Portfolio+`, `+Dispatch+`, +`+AxiomTrackerCompleteness+`, `+Integrity+` and `+ClampTrust+` name this +repository's types, and §1 places them as engineering. The owner chose to +*split* the meta-checker. Generic theory stays in Agda: `+Receipt+`, and any +statement that holds for an arbitrary logic or order, such as E9 composition +(#471). The echidna-specific statements are verified *on the Rust* with +Creusot/Pearlite and Verus (R1). They are not restated in Idris 2: the strict +§1 ruling that #477 applies retires Idris restatements of Rust behaviour +(it removes `+TrustKernelMonotonicity.idr+`). Each Agda module retires once its +Rust contracts carry a receipt. Until then these rows keep their `+proven+` +token as statements about a model. They carry no PWG. + +**Design review of the statements (2026-11-09):** the kernel accepting a proof +says nothing about whether the statement models the code or says what its name +claims. A statement-by-statement comparison with the Rust, the Idris 2 corpus +and the Lean corpus found the following. Each is to be fixed in the split, not +by changing a token. + +* *Model diverges from the Rust.* `+Dispatch.compute-trust+` gives Level 2 for a + cross-checked result without a certificate. The Rust + (`+src/rust/verification/confidence.rs+`, the "Cross-checked without + certificate" branch) and Idris 2 `+TrustKernelMonotonicity.computeTrustLevel+` + give Level 3. `+Integrity.check+` maps an uninitialised manifest to `+Missing+`, + where the Rust and Lean `+verify_placeholder+` give `+Uninitialized+`; the model + also has no "file not found" input. +* *No Rust counterpart.* `+Portfolio.portfolio-trust+` (the Rust + `+compute_trust_level+` never reads `+portfolio_confidence+`) and + `+ClampTrust.clamp-trust+` (R10). +* *Statements weaker than their names.* `+AxiomSafety.comment-skip-sound+` + ignores its hypothesis and proves only `+danger-to-policy DC-Safe ≡ Clean+`. + `+AxiomSafety.real-pattern-classified+` proves only that a function has a + value. `+Dispatch.pipeline-deterministic+` and + `+AxiomTrackerCompleteness.scan-deterministic+` are instances of `+cong+`. The + `+classify-*+` stubs always return `+DC-Safe+` and no theorem uses them. +* *Gaps.* Idris 2 proves the sufficiency of the Level 5 conditions + (`+trustMono_level5_exact+`) but not their necessity, which Agda + `+max-trust-requires-all+` states. Idris 2 `+ClampTrustBounds+` lacks + `+clamp-idempotent+`. + |R9. E11 solver-integrity soundness |`+proven+` |`+meta-checker/src/Echidna/Integrity.agda+`, inside the R4 receipt. States the @@ -233,6 +334,22 @@ validate the Idris2 file or its correspondence to runtime code. Existing Idris2 interface and engineering checks remain active under §1; their receipt status is R2. Monotonicity here is by step lemma plus transitivity, rather than the Idris2 file's decision table. +**Model and code differ:** the Rust has +`+echidna_core_creusot::clamp_trust(level, min_level, max_level)+` +(`+crates/echidna-core-creusot/src/lib.rs:274+`). It clamps a `+TrustLevel+` into +a level range. Its bounds contract (`+requires min_level <= max_level+`, +`+ensures min_level <= result <= max_level+`) is written but not discharged, and +unit test PO-7 checks it exhaustively. The Agda model instead clamps a natural +number into the five levels. Only its bounds statement carries over, as a +special case of the Rust contract (range `+[Level1, Level5]+`). Its fixed-point +and monotone-in-ℕ statements have no counterpart. `+src/rust/verification/ +confidence.rs+` does not call `+clamp_trust+`; it derives a level from +`+TrustFactors+`. The module header's reason for restating the obligation in +Agda ("`there is no idris2 binary in CI that runs it`") is out of date: R2 +records the Idris 2 corpus, `+ClampTrustBounds+` included, building in CI. Under +the R4 split, the target is Creusot/Verus on the Rust `+clamp_trust+`: discharge +the written bounds contract, and add idempotence and monotonicity in `+level+` +as level-to-level statements. The ℕ-specific statements retire with the module. |R11. Epistemic separation: receipt vs warrant |`+proven+` @@ -260,9 +377,13 @@ Rocq/Lean rechecks and statement correspondence also remain open in R5. |`+open+` |`+PROOF-POLICY+` §2: every Agda theory proof is rechecked in both, transported through Dedukti or re-proved, with the route recorded per theorem. -|Never attempted. This is what holds the set at Mathesis *Grade 3*: locally -checked, untranslated. ECHIDNA's `+src/rust/exchange/+` speaks Dedukti, so the -transport route exists; using it is unstarted work, not a missing capability. +|Not yet discharged for any theorem. Under the R4 split, the theory theorem +that owes these legs is `+Receipt+` (R11). It is `+PWG-3+` until a leg counts +(§8.2). Owner decision 2026-11-09: try the §2 *transport* route first (Agda → +Dedukti/Lambdapi → Rocq, through the same Dedukti route as echidna's +`+src/rust/exchange/+`), record how it performs, then re-prove in Lean (core +library, no Mathlib) and Rocq where transport fails. Each leg records its route, +§5 token, §2.2 state and receipt in the PWG table. |R6. E9 "proof composition soundness" |`+argued+`, with a location defect @@ -289,10 +410,11 @@ to update, so it is left as a named action rather than done silently. |R7. `+verification/confidence.rs+` 0–1 score; `+DispatchResult.trust_level+` 1–5 |`+tested-only+` (internal ranking) — *not an assurance claim* -|Mathesis §6: "`Do not flatten proof confidence into a percentage.`" +|`+PROOF-POLICY+` §8.4.7: a census, never a percentage or a single confidence +score. §8 also says an ECHIDNA `+TrustLevel+` does not convert into a PWG. |The score ranks backends against each other and is unweighted by any receipt. It is a routing heuristic. Do not publish it as assurance and do not compare it -with a Mathesis grade. +with a PWG. |R8. `+echidna.prove.result/1+` `+trust.confidence+` |`+open+`, correctly @@ -304,6 +426,53 @@ guess. |=== +== Toolchain deviations (`+PROOF-POLICY+` §6) + +§6 requires proof toolchains to install through the repository's Guix manifest +or its container. Where a lane installs another way, it must carry a +`+deviation+` record here and in the installing workflow. These records were +missing until 2026-11-09. All three are `+open+`. + +[width="100%",cols="16%,18%,30%,24%,12%",options="header"] +|=== +|Leg |Tool and digest |How CI installs it |Why not Guix or the container |State + +|R4, R11 (Agda) +|Agda 2.7.0.1, archive SHA-256 +`+975b515a14877ab6bce5bfc641e16c4a3ee52ca5d7f846577dee80aa2145db8a+`; agda-stdlib 2.1, archive SHA-256 `+72ca3ea25094efa0439e106f0d949330414232ec4cc5c3c3316e7e70dd06d431+` +|`+scripts/ci/setup-agda.sh+` downloads both GitHub release archives, checks +them against the pinned digests (including on a cache hit), and +`+check-agda.sh+` asserts the version and fails on a mismatch. +|`+manifests/live-provers.scm+` names `+agda+`, but the lane pins a binary +distribution to avoid a cold GHC bootstrap (comment in `+setup-agda.sh+`). The +Guix `+agda+` package's version and stdlib pin have not been checked against +2.7.0.1 and 2.1. +|`+open+` + +|R2 (Idris 2) +|Ubuntu `+idris2+` package, otherwise the v0.8.0 source tarball; no digest +recorded +|`+dogfood-proofs-ci.yml+` *Idris2 (verification)* job and +`+idris2-abi-ci.yml+` install from apt, falling back to a source build. +|`+manifests/live-provers.scm+` records Idris 2 as absent from its baseline. No +container stage installs it. +|`+open+`; the lane does not yet assert a version or a digest. + +|R3 (Lean 4) +|Lean 4.13.0 through elan; local recheck archive SHA-256 `+44ceeac7ee4c98d177bfb4a3e5c210555c87e75b08807b68d523237fe4f09997+` +|`+dogfood-proofs-ci.yml+` *Lean 4 (verification)* job runs `+elan-init.sh+` and +installs the toolchain pinned by `+verification/proofs/lean4/lean-toolchain+`. +|Not in Guix (`+manifests/live-provers.scm+`). The manifest points to the +Wave-3 container, but `+Containerfile.wave3+` has no Lean stage. +|`+open+`; the lane asserts the version through `+lean-toolchain+`, not a digest. +|=== + +The local rechecks on 2026-11-09 add one more deviation. The agent session's +network refused `+codeload.github.com+`, so it fetched agda-stdlib by the +`+v2.1+` git tag (peeled commit `+97bc55e47367c562b3032bf104f2a00b19716f88+`) +rather than by the archive digest. That affects only the local corroboration +of R4, not the hosted receipt. + == Not obligations `+PROOF-POLICY+` §3: "`Corpora that exist to exercise provers are not @@ -351,13 +520,13 @@ mean "ECHIDNA is verified" — it would mean one named obligation was discharged by one named tool with its boundary written down. Nothing here vouches for a prover backend's own soundness. -Four rows are `+proven+` today — R4, R9, R10, R11 — and each names the kernel, -the flags and the limit that qualify it (R4 carries the -`+UnsupportedIndexedMatch+` caveat, R9 the digest-level scope). Every *independent* -leg is still `+open+`: R5 has never been attempted, which is why the corpus sits -at Mathesis Grade 3 and not above it. Those two facts are not in tension — -proven in one kernel is exactly what Grade 3 means — and neither of them is an -omission. +Six rows are `+proven+` today (R2, R4, R9, R10, R11) or `+proven-with-postulates+` +(R3), and each names the kernel, the receipt and the limit that qualify it: R4 +carries the `+UnsupportedIndexedMatch+` caveat, R9 the digest-level scope, R10 +the model-only scope, and R3 its three Lean core axioms. R1 (Rust) is `+open+`. +One theory theorem is graded: `+Receipt+` at `+PWG-3+`, because both of its +recheck legs (R5) are still `+open+`. Being proven in one kernel is exactly what +`+PWG-3+` means, and a grade is not a discharge of §2 (§8.4.1). == Related diff --git a/meta-checker/README.adoc b/meta-checker/README.adoc index 8b7ce9ac..f578b70c 100644 --- a/meta-checker/README.adoc +++ b/meta-checker/README.adoc @@ -7,93 +7,141 @@ Jonathan D.A. Jewell == Overview -The ECHIDNA meta-checker is an **Agda formalisation** that proves correctness properties -about ECHIDNA's trust-hardening pipeline. When Agda successfully type-checks these modules, -it provides a **machine-verified guarantee** that the system's safety invariants hold. - -== Verified Properties (30+) - -=== Trust Level System (`TrustLevel.agda`) - -* Trust levels form a **total order** (reflexive, antisymmetric, transitive, total) -* `min-trust` correctly computes lower bounds -* **Dangerous axioms always cap trust at Level1** -* Safe axioms preserve trust level -* Capping is monotonic - -=== Axiom Safety (`AxiomSafety.agda`) - -* Axiom policies form a total preorder -* `worst-policy` is commutative, associative, with identity (Clean) -* **Rejected is absorbing** — once rejected, always rejected -* Comment-aware scanning is sound -* Every danger class maps to exactly one policy - -=== Portfolio Verification (`Portfolio.agda`) +The meta-checker is an *Agda model* of ECHIDNA's trust-hardening pipeline. It +states properties of that model and proves them. A successful check means the +model has those properties. It does not establish that the Rust implementation +has them: no refinement between these definitions and the Rust source is proved +here. Verifying the Rust is the job of Creusot with Pearlite contracts and Verus +(`+PROOF-POLICY+` §1.2), recorded as obligation R1 in +link:../docs/PROOF-STATUS.adoc[`+docs/PROOF-STATUS.adoc+`]. + +That file is the authoritative record of what is proved, by which receipt, and +with which limits. This README describes the modules and how to check them. + +The model does not match the Rust everywhere, and some theorem names promise more +than their statements give. The design review under R4 in `+PROOF-STATUS+` +lists each case: for example, the dispatch model gives Level 2 where the Rust +gives Level 3, and `+comment-skip-sound+` ignores its hypothesis. Until the +Rust contracts replace these modules, read each statement, not its name. + +== Modules + +[cols="1,3",options="header"] +|=== +|Module |What it states + +|`+Echidna.TrustLevel+` +|The five trust levels form a total order; `+min-trust+` is a lower bound; +dangerous axioms cap trust at Level 1; capping is monotone. + +|`+Echidna.AxiomSafety+` +|Axiom policies form a total preorder; `+worst-policy+` is commutative and +associative with `+Clean+` as identity; `+Rejected+` is absorbing; every danger +class maps to exactly one policy. + +|`+Echidna.Portfolio+` +|Cross-checking does not lower trust below a single solver; inconclusive and +timed-out results give Level 1; agreement is reflexive and symmetric; unknown +verdicts never count as agreement. + +|`+Echidna.Dispatch+` +|Failed integrity and dangerous axioms each give Level 1; Level 5 needs every +positive factor; the modelled pipeline only degrades trust and is deterministic. + +|`+Echidna.AxiomTrackerCompleteness+` +|Every registered pattern yields exactly one policy; the policy fold +distributes over registry concatenation and is monotone; an empty registry +yields `+Clean+`; a `+Reject+` pattern anywhere forces `+Rejected+`; scanning is +deterministic. + +|`+Echidna.Integrity+` +|Obligation E11 over digests: verification needs an initialised manifest, means +the recorded digest matched, and never accepts a different digest. Digest +comparison soundness is a record field, not a postulate. + +|`+Echidna.ClampTrust+` +|Bounds, monotonicity, fixed points and idempotence of a modelled +`+clamp-trust : ℕ → TrustLevel+`. The Rust `+clamp_trust+` in +`+crates/echidna-core-creusot+` has a different signature (it clamps a level +into a level range), so only the bounds statement carries over (R10). + +|`+Echidna.Receipt+` +|A two-world Kripke countermodel separating receipts (factive) from warrants +(not factive). This is the module's one *theory* statement under §1. + +|`+Echidna.MetaChecker+` +|The entry point that imports the eight modules above. +|=== -* **Cross-checking improves trust** over single-solver -* Inconclusive and timeout always produce Level1 -* Small-kernel provers always have higher trust -* Agreement relation is reflexive and symmetric -* Unknown verdicts never count as agreement +Under `+PROOF-POLICY+` §1 only `+Receipt+` is theory. The other modules state +properties of this repository's own types, which §1 places with Idris 2. The +owner's decision of 2026-11-09 splits them. What holds for any implementation +stays as Agda theory. The echidna-specific statements are verified on the Rust +with Creusot/Pearlite and Verus, not restated in Idris 2, and each module here +retires once its contracts carry a receipt. See R4 in +`+docs/PROOF-STATUS.adoc+`. -=== Dispatch Pipeline (`Dispatch.agda`) +== Escape hatches -* **Failed integrity always produces Level1** -* **Dangerous axioms always produce Level1** -* Maximum trust (Level5) requires all positive factors -* Pipeline is monotonically degrading -* Pipeline is deterministic +The check runs with `+--safe+`, so the compiler refuses `+postulate+`, +`+primTrustMe+` and unsafe options anywhere in the import cone. There are no +postulates in these modules. The kernel enforces that; a text search is not the +evidence. -== Zero Unsafe Constructs +The check reports `+UnsupportedIndexedMatch+` warnings at a few sites. They mean +the flagged functions do not compute under Cubical transports, which is the +difference between `+--cubical-compatible+` and full `+--cubical+` that +`+PROOF-POLICY+` §2.1 draws. They are recorded in `+PROOF-STATUS+`, not +suppressed. -[cols="1,1"] -|=== -| Construct | Count +== Running -| `postulate` | 1 (funext — standard, provable in HoTT) -| `sorry` | 0 -| `believe_me` | 0 -| `Admitted` | 0 -| `TRUSTME` | 0 -|=== +Use the pinned toolchain and the canonical invocation (`+PROOF-POLICY+` §2.1). +The scripts install Agda 2.7.0.1 and agda-stdlib 2.1 from release archives +checked against pinned SHA-256 digests, then check every module and require a +fresh interface for each one: -== Running +Outside GitHub Actions, `+setup-agda.sh+` cannot change the calling shell's +environment. Give it the two files Actions would provide, then load them: [source,bash] ---- -# Install Agda (requires GHC) -cabal install Agda +export GITHUB_ENV=$(mktemp) GITHUB_PATH=$(mktemp) +bash scripts/ci/setup-agda.sh # writes Agda_datadir, AGDA_LIBRARIES_FILE, LC_ALL +set -a; . "$GITHUB_ENV"; set +a # the values are mktemp paths, without spaces +export PATH="$(cat "$GITHUB_PATH"):$PATH" +bash scripts/ci/check-agda.sh # runs from meta-checker/ +---- -# Install standard library -agda-stdlib-utils install +`+check-agda.sh+` runs: -# Type-check all proofs -cd meta-checker -agda src/Echidna/MetaChecker.agda +[source,bash] +---- +agda --no-default-libraries --library-file "$AGDA_LIBRARIES_FILE" \ + --safe --without-K --cubical-compatible src/Echidna/MetaChecker.agda ---- -If the command exits with code 0, all 30+ properties are machine-verified. - -== CI Integration +It then fails if any module under `+src/Echidna/+` produced no interface, and runs +`+scripts/ci/check-receipt-controls.sh+`, whose planted claims must be rejected. -The `.github/workflows/agda-meta-checker.yml` workflow automatically type-checks -the meta-checker on every push. A green badge means all proofs are valid. +== CI -== Architecture +`+.github/workflows/agda-meta-checker.yml+` runs the same two scripts on relevant +pushes and pull requests and on a schedule. A passing run on a commit is that +commit's receipt for the Agda leg; `+PROOF-STATUS+` cites it by run and commit. -The meta-checker mirrors the Rust source structure: +== Rust counterparts -[cols="1,1"] +[cols="1,1",options="header"] |=== -| Agda Module | Rust Source +|Agda module |Rust source it models -| `Echidna.TrustLevel` | `verification/confidence.rs` -| `Echidna.AxiomSafety` | `verification/axiom_tracker.rs` -| `Echidna.Portfolio` | `verification/portfolio.rs` -| `Echidna.Dispatch` | `dispatch.rs` +|`+Echidna.TrustLevel+` |`+src/rust/verification/confidence.rs+` +|`+Echidna.AxiomSafety+` |`+src/rust/verification/axiom_tracker.rs+` +|`+Echidna.Portfolio+` |`+src/rust/verification/portfolio.rs+` +|`+Echidna.Dispatch+` |`+src/rust/dispatch.rs+` +|`+Echidna.Integrity+` |`+src/rust/integrity/solver_integrity.rs+` |=== -Each Agda definition is annotated with which Rust function or type it models. -The proofs verify that the *design* is correct — they do not replace unit tests -which verify that the *implementation* matches the design. +The correspondence is by reading, not by proof. These proofs check the design; +the unit tests and, once R1 lands, the Rust verifiers check the implementation. diff --git a/scripts/ci/setup-agda.sh b/scripts/ci/setup-agda.sh index ba0e4601..3dd1b39b 100644 --- a/scripts/ci/setup-agda.sh +++ b/scripts/ci/setup-agda.sh @@ -2,6 +2,9 @@ # SPDX-License-Identifier: MPL-2.0 # Copyright (c) 2026 Jonathan D.A. Jewell # Pinned upstream binaries: no cold GHC bootstrap and no cached proof results. +# PROOF-POLICY §6 deviation (open): installs from GitHub release archives, not +# the Guix manifest or the container. Recorded in docs/PROOF-STATUS.adoc, +# "Toolchain deviations". set -Eeuo pipefail trap 'echo "::error::Agda setup did not complete; proof check NOT RUN"; exit 2' ERR diff --git a/src/rust/proof_search.rs b/src/rust/proof_search.rs index 3c90d3bf..949b63c9 100644 --- a/src/rust/proof_search.rs +++ b/src/rust/proof_search.rs @@ -384,7 +384,8 @@ mod chapel_ffi { let start = start.clone(); std::thread::spawn(move || { start.wait(); - let strategy = ChapelParallelSearch::new().expect("real Chapel runtime"); + let strategy = + ChapelParallelSearch::new().expect("real Chapel runtime"); assert_eq!(ChapelParallelSearch::available_prover_count(), 0); for _ in 0..2 { assert!(strategy.available()); @@ -414,10 +415,8 @@ mod chapel_ffi { // No global environment mutation races with other Rust tests, and // no external prover can be dispatched by this allocation/free probe. let empty_path = tempfile::tempdir().expect("empty prover search directory"); - let mut command = real_probe_command( - "real_search_without_provers_fails_and_frees_result", - CHILD, - ); + let mut command = + real_probe_command("real_search_without_provers_fails_and_frees_result", CHILD); command.env("PATH", empty_path.path()); run_real_probe( &mut command, @@ -478,7 +477,10 @@ mod chapel_ffi { matches!(stopped_before_cleanup, Ok(true)), "deadline returned with a live or unobservable prover: {stopped_before_cleanup:?}" ); - assert!(elapsed < Duration::from_secs(3), "deadline took {elapsed:?}"); + assert!( + elapsed < Duration::from_secs(3), + "deadline took {elapsed:?}" + ); let result = result.expect("native timeout returns a failed search result"); assert!(!result.success); assert_eq!( @@ -500,17 +502,12 @@ mod chapel_ffi { .expect("write finite prover"); std::fs::set_permissions(&prover, std::fs::Permissions::from_mode(0o700)) .expect("make finite prover executable"); - let mut command = real_probe_command( - "real_search_deadline_stops_the_owned_prover", - CHILD, - ); + let mut command = + real_probe_command("real_search_deadline_stops_the_owned_prover", CHILD); command .env("PATH", fixture.path()) .env(PID_FILE, fixture.path().join("prover.pid")); - run_real_probe( - &mut command, - "ECHIDNA_REAL_CHAPEL_DEADLINE_PROBE_COMPLETED", - ); + run_real_probe(&mut command, "ECHIDNA_REAL_CHAPEL_DEADLINE_PROBE_COMPLETED"); } } } diff --git a/src/zig_ffi/chapel_bridge.zig b/src/zig_ffi/chapel_bridge.zig index 807c23fe..f8d12591 100644 --- a/src/zig_ffi/chapel_bridge.zig +++ b/src/zig_ffi/chapel_bridge.zig @@ -70,7 +70,8 @@ fn callOnOwner(owner: anytype, comptime function: anytype, args: anytype, result result: @TypeOf(result), fn run(raw: *anyopaque) void { - const self: *@This() = @ptrCast(@alignCast(raw)); + // hypatia: allow code_safety/zig_ptr_cast -- raw is the type-erased *@This() this callback was registered with + const self: *@This() = @ptrCast(@alignCast(raw)); // hypatia: allow code_safety/zig_align_cast -- same pointer, so @This() alignment holds self.result.* = @call(.auto, function, self.arguments); } }; @@ -650,7 +651,8 @@ const CallerAllocator = struct { } fn alloc(raw: *anyopaque, len: usize, alignment: std.mem.Alignment, ret_addr: usize) ?[*]u8 { - const self: *@This() = @ptrCast(@alignCast(raw)); + // hypatia: allow code_safety/zig_ptr_cast -- raw is the type-erased *@This() this callback was registered with + const self: *@This() = @ptrCast(@alignCast(raw)); // hypatia: allow code_safety/zig_align_cast -- same pointer, so @This() alignment holds if (!self.record() or self.allocations >= self.fail_after) return null; const pointer = std.heap.c_allocator.rawAlloc(len, alignment, ret_addr) orelse return null; self.allocations += 1; @@ -659,7 +661,8 @@ const CallerAllocator = struct { } fn resize(raw: *anyopaque, memory: []u8, alignment: std.mem.Alignment, new_len: usize, ret_addr: usize) bool { - const self: *@This() = @ptrCast(@alignCast(raw)); + // hypatia: allow code_safety/zig_ptr_cast -- raw is the type-erased *@This() this callback was registered with + const self: *@This() = @ptrCast(@alignCast(raw)); // hypatia: allow code_safety/zig_align_cast -- same pointer, so @This() alignment holds _ = self.record(); _ = memory; _ = alignment; @@ -669,7 +672,8 @@ const CallerAllocator = struct { } fn remap(raw: *anyopaque, memory: []u8, alignment: std.mem.Alignment, new_len: usize, ret_addr: usize) ?[*]u8 { - const self: *@This() = @ptrCast(@alignCast(raw)); + // hypatia: allow code_safety/zig_ptr_cast -- raw is the type-erased *@This() this callback was registered with + const self: *@This() = @ptrCast(@alignCast(raw)); // hypatia: allow code_safety/zig_align_cast -- same pointer, so @This() alignment holds _ = self.record(); _ = memory; _ = alignment; @@ -679,7 +683,8 @@ const CallerAllocator = struct { } fn free(raw: *anyopaque, memory: []u8, alignment: std.mem.Alignment, ret_addr: usize) void { - const self: *@This() = @ptrCast(@alignCast(raw)); + // hypatia: allow code_safety/zig_ptr_cast -- raw is the type-erased *@This() this callback was registered with + const self: *@This() = @ptrCast(@alignCast(raw)); // hypatia: allow code_safety/zig_align_cast -- same pointer, so @This() alignment holds _ = self.record(); // The backing allocator is cross-thread safe so a failed assertion // never requires corrupting memory or leaking the test allocation. diff --git a/src/zig_ffi/runtime_owner.zig b/src/zig_ffi/runtime_owner.zig index 79d9d543..da2f1b8a 100644 --- a/src/zig_ffi/runtime_owner.zig +++ b/src/zig_ffi/runtime_owner.zig @@ -169,7 +169,8 @@ const Probe = struct { } fn work(raw: *anyopaque) void { - const self: *@This() = @ptrCast(@alignCast(raw)); + // hypatia: allow code_safety/zig_ptr_cast -- raw is the type-erased *@This() this callback was registered with + const self: *@This() = @ptrCast(@alignCast(raw)); // hypatia: allow code_safety/zig_align_cast -- same pointer, so @This() alignment holds self.wrong_thread = self.wrong_thread or self.init_id != std.Thread.getCurrentId(); self.calls += 1; } @@ -239,7 +240,8 @@ test "shutdown drains accepted work and refuses new work before joining" { shutdown_failed: bool = false, fn work(raw: *anyopaque) void { - const self: *@This() = @ptrCast(@alignCast(raw)); + // hypatia: allow code_safety/zig_ptr_cast -- raw is the type-erased *@This() this callback was registered with + const self: *@This() = @ptrCast(@alignCast(raw)); // hypatia: allow code_safety/zig_align_cast -- same pointer, so @This() alignment holds self.mutex.lock(); self.entered = true; self.changed.broadcast(); @@ -311,7 +313,8 @@ test "owner callbacks cannot re-enter or finalize themselves" { stop_refused: bool = false, fn work(raw: *anyopaque) void { - const self: *@This() = @ptrCast(@alignCast(raw)); + // hypatia: allow code_safety/zig_ptr_cast -- raw is the type-erased *@This() this callback was registered with + const self: *@This() = @ptrCast(@alignCast(raw)); // hypatia: allow code_safety/zig_align_cast -- same pointer, so @This() alignment holds var nested = Work{ .context = self.probe, .run = Probe.work }; self.call_refused = if (self.owner.call(&nested)) |_| false else |err| err == error.ReentrantCall; self.stop_refused = if (self.owner.shutdown()) |_| false else |err| err == error.ReentrantCall; @@ -358,7 +361,8 @@ test "a nonowner process-exit request refuses active work without a join cycle" exit_refused: bool = false, fn work(raw: *anyopaque) void { - const self: *@This() = @ptrCast(@alignCast(raw)); + // hypatia: allow code_safety/zig_ptr_cast -- raw is the type-erased *@This() this callback was registered with + const self: *@This() = @ptrCast(@alignCast(raw)); // hypatia: allow code_safety/zig_align_cast -- same pointer, so @This() alignment holds self.mutex.lock(); self.entered = true; self.changed.broadcast();