From 0c75f67c3b3ba796089ae67da18064eebcb5295b Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 9 Nov 2026 13:42:22 +0000 Subject: [PATCH 1/7] =?UTF-8?q?docs(proofs):=20bring=20PROOF-STATUS=20up?= =?UTF-8?q?=20to=20PROOF-POLICY=20=C2=A71.2,=20=C2=A76=20and=20=C2=A78?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit PROOF-STATUS predated two policy amendments (§8 Proof Witness Grades, 2026-11-04; §1.2 Creusot, Pearlite and Verus, 2026-11-07) and understated two legs that CI already proves. - Grades: replace the bare "Mathesis Grade 3" wording, which §8 forbids, with a PWG table. Only theory theorems are graded; Receipt is PWG-3 with both recheck legs open. - R1: name Creusot, Pearlite and Verus, with the status of each. - R2 (Idris 2): proven, citing the Dogfood "Idris2 (verification)" job, which builds all eleven modules of echidna-verif-proofs.ipkg. - R3 (Lean): proven-with-postulates, citing the "Lean 4 (verification)" job and a local Lean 4.13.0 recheck. Of 167 theorems, 109 use no axiom and 58 use only propext, Quot.sound and Classical.choice. The Mathlib question is closed by §2. - R4: cite the hosted Agda Meta-Checker run on 2ab7574 (exact commit), corroborated locally, and record the owner's §1 decision to split the meta-checker (theory to Agda, echidna types to Idris 2, Rust verified with Creusot/Pearlite and Verus). - R10: no clamp_trust exists in the Rust, so the row is model-only; the module header's "no idris2 in CI" reason is out of date. - §6: add the missing deviation records for the Agda, Idris 2 and Lean lanes, in PROOF-STATUS and as comments in the installing scripts and workflows. Comments only; no uses: changes. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_015jzCHZx4Rt65NDaGLDrjLp --- .github/workflows/dogfood-proofs-ci.yml | 9 + .github/workflows/idris2-abi-ci.yml | 3 + docs/PROOF-STATUS.adoc | 237 ++++++++++++++++++------ scripts/ci/setup-agda.sh | 3 + 4 files changed, 197 insertions(+), 55 deletions(-) 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/docs/PROOF-STATUS.adoc b/docs/PROOF-STATUS.adoc index bcf6c700..22bcec0b 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 moves each statement to its mapped home. == 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,19 @@ 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 specifications that the R4 split produces. The row stays `+open+` +until each verifier yields a receipt with a commit hash. |=== @@ -118,17 +140,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 +168,27 @@ 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 move to Idris 2 when next touched, unless a §4 exception +is recorded. Until then they stay, labelled with their prover. |=== @@ -159,7 +202,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 +252,16 @@ 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. What holds for any implementation (orders, +lattices) becomes parametric Agda theory. The echidna-specific instances +move to Idris 2 under `+verification/proofs/idris2/+`. The Rust is then +verified against those specifications with Creusot/Pearlite and Verus (R1). +Until that lands, these rows keep their `+proven+` token. They carry no PWG. + |R9. E11 solver-integrity soundness |`+proven+` |`+meta-checker/src/Echidna/Integrity.agda+`, inside the R4 receipt. States the @@ -233,6 +300,14 @@ 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-only:** no `+clamp_trust+` function exists in the Rust +(`+src/rust/verification/confidence.rs+` derives a `+TrustLevel+` from +`+TrustFactors+` and never clamps a number). This is therefore a property of a +specified function, not of shipped code. 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. The split recorded under R4 returns this obligation +to Idris 2. |R11. Epistemic separation: receipt vs warrant |`+proven+` @@ -260,9 +335,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 +368,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 +384,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 +478,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/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 From 7a375dad12f13642fe323901cc28b4703029d0a6 Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 9 Nov 2026 13:44:19 +0000 Subject: [PATCH 2/7] docs(meta-checker): make the README match the checked modules MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The README claimed one postulate (funext), which --safe rules out and which no module contains. It also listed four of the nine modules, counted "30+ properties" that nobody had counted, gave run steps without the PROOF-POLICY §2.1 flags, and said a green check guarantees that the system's invariants hold. It now lists all nine modules, says they prove properties of a model rather than of the Rust, records that only Receipt is theory under §1, documents the pinned setup and check scripts, and points to PROOF-STATUS for receipts. Mathesis's reconciliation register cites the stale funext note as an open ECHIDNA item; this removes it. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_015jzCHZx4Rt65NDaGLDrjLp --- meta-checker/README.adoc | 164 +++++++++++++++++++++++---------------- 1 file changed, 98 insertions(+), 66 deletions(-) diff --git a/meta-checker/README.adoc b/meta-checker/README.adoc index 8b7ce9ac..e94ff1ca 100644 --- a/meta-checker/README.adoc +++ b/meta-checker/README.adoc @@ -7,93 +7,125 @@ 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. +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+`]. -== Verified Properties (30+) +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. -=== Trust Level System (`TrustLevel.agda`) +== Modules -* 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`) - -* **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 - -=== Dispatch Pipeline (`Dispatch.agda`) +[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+`. No such function exists in the Rust (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. +|=== -* **Failed integrity always produces Level1** -* **Dangerous axioms always produce Level1** -* Maximum trust (Level5) requires all positive factors -* Pipeline is monotonically degrading -* Pipeline is deterministic +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 +becomes parametric Agda, and the echidna-specific instances move to +`+verification/proofs/idris2/+`. See R4 in `+docs/PROOF-STATUS.adoc+`. -== Zero Unsafe Constructs +== Escape hatches -[cols="1,1"] -|=== -| Construct | Count +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. -| `postulate` | 1 (funext — standard, provable in HoTT) -| `sorry` | 0 -| `believe_me` | 0 -| `Admitted` | 0 -| `TRUSTME` | 0 -|=== +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. == Running +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: + [source,bash] ---- -# Install Agda (requires GHC) -cabal install Agda +bash scripts/ci/setup-agda.sh # prints the paths to export +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. From ddb234e3cdce88db6a19eb007fae587146038225 Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 9 Nov 2026 13:46:44 +0000 Subject: [PATCH 3/7] docs(proofs): record the meta-checker design review in PROOF-STATUS A statement-by-statement comparison of the Agda meta-checker with the Rust, the Idris 2 corpus and the Lean corpus found problems that a passing kernel check does not reveal: - Dispatch.compute-trust gives Level 2 for a cross-checked result without a certificate; the Rust and Idris 2 give Level 3. - Integrity.check maps an uninitialised manifest to Missing; the Rust and Lean give Uninitialized. - Portfolio.portfolio-trust and ClampTrust.clamp-trust have no Rust counterpart. - comment-skip-sound ignores its hypothesis, real-pattern-classified only proves totality, and two "determinism" theorems are cong. - Idris 2 lacks Level 5 necessity and clamp idempotence. The rows keep their proven token (the kernel did accept these proofs); the review lists what the planned split must fix. The README now points readers to it instead of implying the names are the guarantees. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_015jzCHZx4Rt65NDaGLDrjLp --- docs/PROOF-STATUS.adoc | 27 +++++++++++++++++++++++++++ meta-checker/README.adoc | 6 ++++++ 2 files changed, 33 insertions(+) diff --git a/docs/PROOF-STATUS.adoc b/docs/PROOF-STATUS.adoc index 22bcec0b..59363f4e 100644 --- a/docs/PROOF-STATUS.adoc +++ b/docs/PROOF-STATUS.adoc @@ -262,6 +262,33 @@ move to Idris 2 under `+verification/proofs/idris2/+`. The Rust is then verified against those specifications with Creusot/Pearlite and Verus (R1). Until that lands, these rows keep their `+proven+` token. 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 diff --git a/meta-checker/README.adoc b/meta-checker/README.adoc index e94ff1ca..8b891ddf 100644 --- a/meta-checker/README.adoc +++ b/meta-checker/README.adoc @@ -18,6 +18,12 @@ 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. The planned +split fixes them; until then, read each statement, not its name. + == Modules [cols="1,3",options="header"] From 45c0c93a8f8c3dd0d08460aceeabca01970c65d9 Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 9 Nov 2026 14:09:59 +0000 Subject: [PATCH 4/7] fix(deps): bump rmcp 3.5.0 -> 3.9.0 for RUSTSEC-2026-0457/0461/0462 Port of the rmcp lockfile change from #465 so this docs PR's dependency audit is not red for a reason unrelated to it. Regenerated with `cargo update -p rmcp --precise 3.9.0`; the windows-sys lines are resolver output, identical to #465. No-op once #465 lands. Verified locally: scripts/ci/audit-dependencies.sh passes for both lockfiles; `cargo check -p echidna-mcp` builds. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_015jzCHZx4Rt65NDaGLDrjLp --- Cargo.lock | 30 ++++++++++++++++-------------- 1 file changed, 16 insertions(+), 14 deletions(-) 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]] From e0e21c088d9862271180c70514f943f8870bd75a Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 9 Nov 2026 14:12:26 +0000 Subject: [PATCH 5/7] =?UTF-8?q?docs(proofs):=20record=20the=20strict=20?= =?UTF-8?q?=C2=A71=20ruling=20for=20the=20meta-checker=20split?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The owner chose #477's reading of PROOF-POLICY §1 for the split. Generic theory (Receipt; E9 composition in #471) stays in Agda. Echidna-specific statements are verified on the Rust with Creusot/Pearlite and Verus, not restated in Idris 2. Each meta-checker module retires once its Rust contracts carry a receipt. R1 now points at #477's trust kernel as the first Creusot target. R10 has no Rust target (there is no clamp_trust), so it retires with its module. The Lean re-homing note distinguishes Rust behaviour (Creusot/Verus) from API/ABI properties (Idris 2). Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_015jzCHZx4Rt65NDaGLDrjLp --- docs/PROOF-STATUS.adoc | 30 +++++++++++++++++++----------- meta-checker/README.adoc | 12 +++++++----- 2 files changed, 26 insertions(+), 16 deletions(-) diff --git a/docs/PROOF-STATUS.adoc b/docs/PROOF-STATUS.adoc index 59363f4e..f3e6c34f 100644 --- a/docs/PROOF-STATUS.adoc +++ b/docs/PROOF-STATUS.adoc @@ -95,7 +95,7 @@ on `+2ab7574+`. *Rocq*: `+open+`, `+BRIDGE-PENDING+`, no receipt. *Lean*: 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 moves each statement to its mapped home. +R4 replaces each with Creusot/Verus contracts on the Rust (R1). == Obligations @@ -121,7 +121,9 @@ 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 specifications that the R4 split produces. The row stays `+open+` +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. |=== @@ -187,8 +189,10 @@ 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 move to Idris 2 when next touched, unless a §4 exception -is recorded. Until then they stay, labelled with their prover. +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. |=== @@ -256,11 +260,14 @@ for the current `+proven+` row; the source-bound 2026-11-04 receipt replaces it. `+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. What holds for any implementation (orders, -lattices) becomes parametric Agda theory. The echidna-specific instances -move to Idris 2 under `+verification/proofs/idris2/+`. The Rust is then -verified against those specifications with Creusot/Pearlite and Verus (R1). -Until that lands, these rows keep their `+proven+` token. They carry no PWG. +*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 @@ -333,8 +340,9 @@ rather than the Idris2 file's decision table. specified function, not of shipped code. 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. The split recorded under R4 returns this obligation -to Idris 2. +included, building in CI. Because no Rust `+clamp_trust+` exists, the R4 split +gives this obligation no Creusot/Verus target: it is retired with the module +unless a clamp is added to the code. |R11. Epistemic separation: receipt vs warrant |`+proven+` diff --git a/meta-checker/README.adoc b/meta-checker/README.adoc index 8b891ddf..20d43312 100644 --- a/meta-checker/README.adoc +++ b/meta-checker/README.adoc @@ -21,8 +21,8 @@ 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. The planned -split fixes them; until then, read each statement, not its name. +gives Level 3, and `+comment-skip-sound+` ignores its hypothesis. Until the +Rust contracts replace these modules, read each statement, not its name. == Modules @@ -73,9 +73,11 @@ comparison soundness is a record field, not a postulate. 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 -becomes parametric Agda, and the echidna-specific instances move to -`+verification/proofs/idris2/+`. See R4 in `+docs/PROOF-STATUS.adoc+`. +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+`. == Escape hatches From d4ef769802d66cc08cd6a03566a0e111ea343f18 Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 9 Nov 2026 14:44:36 +0000 Subject: [PATCH 6/7] fix(ci): port #465's Hypatia Zig-cast annotations and rustfmt fix Validate Hypatia Baseline fails on this PR. It reports four unannotated zig_ptr_cast/zig_align_cast findings in src/zig_ffi/, which are also red on main and unrelated to this docs PR. This ports #465's fix unchanged: - inline `hypatia: allow` annotations with a justification on each cast (comments only; the code is unchanged); - its rustfmt reflow of src/rust/proof_search.rs. Both become no-ops once #465 lands. `rustfmt --check` passes on proof_search.rs. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_015jzCHZx4Rt65NDaGLDrjLp --- src/rust/proof_search.rs | 25 +++++++++++-------------- src/zig_ffi/chapel_bridge.zig | 15 ++++++++++----- src/zig_ffi/runtime_owner.zig | 12 ++++++++---- 3 files changed, 29 insertions(+), 23 deletions(-) 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(); From f8acbaaf90fb4ac2d34942090640b5f707d80b31 Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 9 Nov 2026 15:43:05 +0000 Subject: [PATCH 7/7] docs(proofs): correct R10 for the Rust clamp_trust; fix the local Agda recipe MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Fixes two Codex review findings on #474: - R10 said no Rust clamp_trust exists. One does: echidna_core_creusot::clamp_trust(level, min, max), with a written but undischarged Creusot bounds contract and the exhaustive unit test PO-7. R10 now records how it corresponds to the Agda model. Only the bounds statement carries over; the Agda model clamps ℕ, so its ℕ-specific statements do not. The split targets the Rust function, not retirement. - The README's local recipe did not work. Outside Actions, setup-agda.sh only prints the paths. The recipe now provides GITHUB_ENV/GITHUB_PATH files and loads them, so it goes through the script's own export code. The loading step was tested here with values in the script's format. The full setup was not run locally, because the agda-stdlib archive host is blocked in this sandbox. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_015jzCHZx4Rt65NDaGLDrjLp --- docs/PROOF-STATUS.adoc | 25 ++++++++++++++++--------- meta-checker/README.adoc | 14 +++++++++++--- 2 files changed, 27 insertions(+), 12 deletions(-) diff --git a/docs/PROOF-STATUS.adoc b/docs/PROOF-STATUS.adoc index f3e6c34f..f8b1591d 100644 --- a/docs/PROOF-STATUS.adoc +++ b/docs/PROOF-STATUS.adoc @@ -334,15 +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-only:** no `+clamp_trust+` function exists in the Rust -(`+src/rust/verification/confidence.rs+` derives a `+TrustLevel+` from -`+TrustFactors+` and never clamps a number). This is therefore a property of a -specified function, not of shipped code. 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. Because no Rust `+clamp_trust+` exists, the R4 split -gives this obligation no Creusot/Verus target: it is retired with the module -unless a clamp is added to the code. +**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+` diff --git a/meta-checker/README.adoc b/meta-checker/README.adoc index 20d43312..f578b70c 100644 --- a/meta-checker/README.adoc +++ b/meta-checker/README.adoc @@ -61,7 +61,9 @@ comparison soundness is a record field, not a postulate. |`+Echidna.ClampTrust+` |Bounds, monotonicity, fixed points and idempotence of a modelled -`+clamp-trust : ℕ → TrustLevel+`. No such function exists in the Rust (R10). +`+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 @@ -99,10 +101,16 @@ 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: +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] ---- -bash scripts/ci/setup-agda.sh # prints the paths to export -bash scripts/ci/check-agda.sh # runs from meta-checker/ +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/ ---- `+check-agda.sh+` runs: