fix(proofs): align proof artefacts with the estate PROOF-POLICY

.github/workflows/actions.lock

@@ -1,4 +1,4 @@
 # This file is machine-generated by `gh actions-lock`.
 # Do not edit by hand; run `gh actions-lock` to update.
 # Docs: https://gh.io/actions-lockfile
 version: 'v0.0.3'
@@ -24,7 +24,7 @@
     '.github/workflows/labels.yml': []
     '.github/workflows/lock-sync-gate.yml': []
     '.github/workflows/main-estate-audit.yml':
-        - 'hyperpolymath/cicd-suite@354c425571c1f27b66dd141daeb0e90fa0c26dd9'
+        - 'hyperpolymath/proven-cicd-and-workflows@354c425571c1f27b66dd141daeb0e90fa0c26dd9'
     '.github/workflows/mirror.yml':
         - 'actions/checkout@v7.0.1'
         - 'dtolnay/rust-toolchain@master'
@@ -114,16 +114,6 @@
         commit: 'sha1-cdf488f595d80d6e07e03d4674febd5ab45fa938'
         owner_id: 9919
         repo_id: 259445878
-    'hyperpolymath/cicd-suite@354c425571c1f27b66dd141daeb0e90fa0c26dd9':
-        ref: '354c425571c1f27b66dd141daeb0e90fa0c26dd9'
-        commit: 'sha1-354c425571c1f27b66dd141daeb0e90fa0c26dd9'
-        owner_id: 6759885
-        repo_id: 1326697643
-        uses:
-            - 'actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1'
-            - 'hyperpolymath/cicd-suite@35868f090e4e42b142374d156f2d49a22ad577fd'
-            - 'hyperpolymath/cicd-suite@88c55e28f37b8dfc5a435e86f548737997746cc9'
-            - 'hyperpolymath/cicd-suite@c519c4520afbfe48f16aceb0706d7cfb1d649994'
     'hyperpolymath/cicd-suite@35868f090e4e42b142374d156f2d49a22ad577fd':
         ref: '35868f090e4e42b142374d156f2d49a22ad577fd'
         commit: 'sha1-35868f090e4e42b142374d156f2d49a22ad577fd'
@@ -152,6 +142,16 @@
         commit: 'sha1-2155aa26a21758f2ba119f61bc7e0e1981c106fb'
         owner_id: 6759885
         repo_id: 1275650185
+    'hyperpolymath/proven-cicd-and-workflows@354c425571c1f27b66dd141daeb0e90fa0c26dd9':
+        ref: '354c425571c1f27b66dd141daeb0e90fa0c26dd9'
+        commit: 'sha1-354c425571c1f27b66dd141daeb0e90fa0c26dd9'
+        owner_id: 6759885
+        repo_id: 1326697643
+        uses:
+            - 'actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1'
+            - 'hyperpolymath/cicd-suite@35868f090e4e42b142374d156f2d49a22ad577fd'
+            - 'hyperpolymath/cicd-suite@88c55e28f37b8dfc5a435e86f548737997746cc9'
+            - 'hyperpolymath/cicd-suite@c519c4520afbfe48f16aceb0706d7cfb1d649994'
     'hyperpolymath/smtp-notify-action@v0.5.0':
         ref: 'v0.5.0'
         commit: 'sha1-c1c9fa07992a02c1fd3d67a0dc1b08cccb852aef'

.github/workflows/main-estate-audit.yml

@@ -32,4 +32,4 @@ permissions:
 
 jobs:
   estate:
-    uses: hyperpolymath/cicd-suite/.github/workflows/main-estate-audit.yml@354c425571c1f27b66dd141daeb0e90fa0c26dd9 # cicd-suite main
+    uses: hyperpolymath/proven-cicd-and-workflows/.github/workflows/main-estate-audit.yml@354c425571c1f27b66dd141daeb0e90fa0c26dd9 # proven-cicd-and-workflows (formerly cicd-suite)

CHANGELOG.adoc

@@ -33,6 +33,18 @@ https://semver.org/spec/v2.0.0.html[Semantic Versioning].
 * `tools/environments/` — `environments.kyaml` (environment classes with a
   `measured` block), `probe-reachability.sh` and `hosts.txt` (experiment
   X1: reachability probe, HEAD by default, one-byte GET with `--get`).
+* `scripts/proof-check.sh`, called by every `proof-check-*` recipe, and
+  `tests/proof_check_test.sh`. Agda runs with PROOF-POLICY §2.1's
+  `--safe --without-K --cubical-compatible`. A missing checker is reported
+  `UNAVAILABLE` and the run exits 3, never a pass. The escape-hatch scan
+  reads code only, so comments and strings no longer trip it. Checkers run
+  on a copy, so they write nothing into the tree.
+* `verification/proofs/agda/bofj-kitt-proofs.agda-lib`, so Agda can find
+  the standard library through its registered libraries. `AGDA_STDLIB`
+  overrides this with an explicit path.
+* A `verus` entry in `tools/proof-toolchain/toolchain.kyaml`. The owner
+  ruling of 2026-11-07 made Verus a default Rust verifier beside Creusot
+  (PROOF-POLICY §1.2).
 
 ==== Fixed
 
@@ -59,6 +71,47 @@ addressed:
 * `Justfile` `container-init` renders the `VERSION` placeholder; the dogfood gate's
   summary counts the K9 files the hook validated, not every `*.k9` path.
 
+Proof artefacts brought in line with PROOF-POLICY (metadatastician/standards
+at `9bdf864`):
+
+* `just proof-check-all` could never pass. Its escape-hatch scan matched the
+  template's own "no postulate" and "NO Admitted" comments in all 8 proof
+  files. No CI job ran it.
+* The Agda recipe ran `agda --safe` without the §2.1 flags, and every recipe
+  exited 0 when its prover was missing.
+* `docs/status/PROOF-STATUS.adoc` now uses the §5 vocabulary with no
+  percentage. It records the 2026-11-09 session results (Agda 2.6.3 and
+  Coq 8.18 check their template files, ACL2 8.5 and HOL Light pass their
+  smoke fixtures, and the rest are not run). It also lists the obligations
+  the proposals name for other repositories.
+* `docs/status/PROOF-NEEDS.adoc` withdraws the template's ABI and typing
+  obligations, since this repository has no ABI, FFI or typed API. TP-2 had
+  put API typing in Lean, but §1 puts it in Idris2. The prover guide
+  recommended Lean for its Mathlib, which §2 forbids; it now summarises §1.
+* `tools/proof-toolchain/DESIGN.adoc` states the §6 deviation records the
+  installer must write for every entry installed other than through Guix or
+  the container.
+* The cartridge proposal now keeps the §5 status, the §2.2 correspondence
+  state and the §8 grade as three separate fields. The cartridges never
+  write a grade: Mathesis derives grades from their receipts. An Agda
+  receipt also carries its library pin and import cone.
+* Review of the new escape-hatch scan found three cases it missed or
+  misreported, all fixed with regression tests:
+  ** a Lean character literal such as `'"'` opened a phantom string that
+     hid a later `sorry`;
+  ** an Agda identifier containing `--` was read as a comment that hid a
+     later `postulate`;
+  ** `admit` was flagged in Agda, where it is an ordinary name. Patterns are
+     now chosen per language.
+* `scripts/proof-check.sh` also makes a relative `AGDA_STDLIB` absolute and
+  copies a linked proof directory as its contents.
+* `toolchain.kyaml` gives Verus's own Z3 a `verus-z3` entry. The deviation
+  records are written by the bundle build that owns the lock, and the
+  exemption from them follows the install route rather than the tool.
+* `.github/workflows/main-estate-audit.yml` calls the audit under cicd-suite's
+  new name, `hyperpolymath/proven-cicd-and-workflows`. Since the rename on
+  2026-11-09 the old name failed at startup with zero jobs.
+
 ==== Changed
 
 * `build/setup.sh` — when no system package provides `just`, setup runs

build/just/proofs.just

@@ -4,151 +4,40 @@
 # FORMAL VERIFICATION (PROOFS)
 #
 # Imported by ../../Justfile via `import? "build/just/proofs.just"`.
-# Recipes here check formal proofs across Idris2, Lean4, Agda, and Coq, plus
-# scan for dangerous/unsafe constructs and report status. Run via
-# `just proof-check-all` for the full sweep.
+# The recipes call scripts/proof-check.sh, which follows the estate
+# PROOF-POLICY (metadatastician/standards, 3-practice/PROOF-POLICY.adoc):
+# Agda runs with the canonical `--safe --without-K --cubical-compatible`
+# invocation (§2.1), and a missing checker is reported UNAVAILABLE and fails
+# the run instead of passing (exit 3). Set AGDA_STDLIB to the standard
+# library's source directory if it is not a registered Agda library.
+#
+# The proof files here are RSR template material, not obligations of this
+# repository; docs/status/PROOF-STATUS.adoc records their status.
 
-# Check all formal proofs (Idris2 + Lean4 + Agda + Coq)
-proof-check-all: proof-check-idris2 proof-check-lean4 proof-check-agda proof-check-coq proof-scan-dangerous
-    @echo "=== All proof checks complete ==="
+# Check every proof file and scan for escape hatches
+proof-check-all:
+    scripts/proof-check.sh all
 
-# Check Idris2 proofs (ABI, types, dependent type proofs)
+# Check Idris2 proofs
 proof-check-idris2:
-    #!/usr/bin/env bash
-    set -euo pipefail
-    echo "=== Checking Idris2 proofs ==="
-    if ! command -v idris2 &>/dev/null; then
-        echo "SKIP: idris2 not installed"
-        exit 0
-    fi
-    ERRORS=0
-    for f in $(find verification/proofs/idris2 -name '*.idr' 2>/dev/null); do
-        echo -n "  Checking $f ... "
-        if idris2 --check "$f" 2>/dev/null; then
-            echo "OK"
-        else
-            echo "FAIL"
-            ERRORS=$((ERRORS + 1))
-        fi
-    done
-    if [ "$ERRORS" -gt 0 ]; then
-        echo "FAIL: $ERRORS Idris2 proof(s) failed"
-        exit 1
-    fi
-    echo "PASS: All Idris2 proofs verified"
+    scripts/proof-check.sh idris2
 
-# Check Lean4 proofs
+# Check Lean 4 proofs
 proof-check-lean4:
-    #!/usr/bin/env bash
-    set -euo pipefail
-    echo "=== Checking Lean4 proofs ==="
-    if ! command -v lean &>/dev/null; then
-        echo "SKIP: lean not installed"
-        exit 0
-    fi
-    ERRORS=0
-    for f in $(find verification/proofs/lean4 -name '*.lean' 2>/dev/null); do
-        echo -n "  Checking $f ... "
-        if lean "$f" 2>/dev/null; then
-            echo "OK"
-        else
-            echo "FAIL"
-            ERRORS=$((ERRORS + 1))
-        fi
-    done
-    if [ "$ERRORS" -gt 0 ]; then
-        echo "FAIL: $ERRORS Lean4 proof(s) failed"
-        exit 1
-    fi
-    echo "PASS: All Lean4 proofs verified"
+    scripts/proof-check.sh lean4
 
-# Check Agda proofs
+# Check Agda proofs (PROOF-POLICY §2.1 invocation)
 proof-check-agda:
-    #!/usr/bin/env bash
-    set -euo pipefail
-    echo "=== Checking Agda proofs ==="
-    if ! command -v agda &>/dev/null; then
-        echo "SKIP: agda not installed"
-        exit 0
-    fi
-    ERRORS=0
-    for f in $(find verification/proofs/agda -name '*.agda' 2>/dev/null); do
-        echo -n "  Checking $f ... "
-        if agda --safe "$f" 2>/dev/null; then
-            echo "OK"
-        else
-            echo "FAIL"
-            ERRORS=$((ERRORS + 1))
-        fi
-    done
-    if [ "$ERRORS" -gt 0 ]; then
-        echo "FAIL: $ERRORS Agda proof(s) failed"
-        exit 1
-    fi
-    echo "PASS: All Agda proofs verified"
+    scripts/proof-check.sh agda
 
-# Check Coq proofs
+# Check Coq (Rocq) proofs
 proof-check-coq:
-    #!/usr/bin/env bash
-    set -euo pipefail
-    echo "=== Checking Coq proofs ==="
-    if ! command -v coqc &>/dev/null; then
-        echo "SKIP: coqc not installed"
-        exit 0
-    fi
-    ERRORS=0
-    for f in $(find verification/proofs/coq -name '*.v' 2>/dev/null); do
-        echo -n "  Checking $f ... "
-        if coqc "$f" 2>/dev/null; then
-            echo "OK"
-        else
-            echo "FAIL"
-            ERRORS=$((ERRORS + 1))
-        fi
-    done
-    if [ "$ERRORS" -gt 0 ]; then
-        echo "FAIL: $ERRORS Coq proof(s) failed"
-        exit 1
-    fi
-    echo "PASS: All Coq proofs verified"
+    scripts/proof-check.sh coq
 
-# Scan for dangerous patterns in proof files (believe_me, sorry, Admitted, etc.)
+# Scan proof code (comments and strings ignored) for escape hatches
 proof-scan-dangerous:
-    #!/usr/bin/env bash
-    set -euo pipefail
-    echo "=== Scanning for dangerous patterns in proofs ==="
-    DANGEROUS=0
-    PATTERNS="believe_me|assert_total|postulate|sorry|Admitted|unsafeCoerce|Obj\.magic"
-    for f in $(find verification/proofs -name '*.idr' -o -name '*.lean' -o -name '*.agda' -o -name '*.v' 2>/dev/null); do
-        MATCHES=$(grep -nE "$PATTERNS" "$f" 2>/dev/null || true)
-        if [ -n "$MATCHES" ]; then
-            echo "  DANGEROUS: $f"
-            echo "$MATCHES" | sed 's/^/    /'
-            DANGEROUS=$((DANGEROUS + 1))
-        fi
-    done
-    if [ "$DANGEROUS" -gt 0 ]; then
-        echo "FAIL: $DANGEROUS file(s) contain dangerous patterns"
-        exit 1
-    fi
-    echo "PASS: No dangerous patterns found in proofs"
+    scripts/proof-check.sh scan
 
-# Show proof status summary
+# Show the proof ledger summary
 proof-status:
-    #!/usr/bin/env bash
-    echo "=== Proof Status ==="
-    echo ""
-    echo "Idris2: $(find verification/proofs/idris2 -name '*.idr' 2>/dev/null | wc -l) files"
-    echo "Lean4:  $(find verification/proofs/lean4 -name '*.lean' 2>/dev/null | wc -l) files"
-    echo "Agda:   $(find verification/proofs/agda -name '*.agda' 2>/dev/null | wc -l) files"
-    echo "Coq:    $(find verification/proofs/coq -name '*.v' 2>/dev/null | wc -l) files"
-    echo "TLA+:   $(find verification/proofs/tlaplus -name '*.tla' 2>/dev/null | wc -l) files"
-    echo ""
-    # PROOF-STATUS may live at root, docs/status/ (post-#20), .md or .adoc (post-#23)
-    for candidate in docs/status/PROOF-STATUS.adoc docs/status/PROOF-STATUS.md PROOF-STATUS.adoc PROOF-STATUS.md; do
-        if [ -f "$candidate" ]; then
-            grep -E "^\| \*\*Total\*\*|^\| \*Total\*" "$candidate" 2>/dev/null || echo "(No summary row in $candidate)"
-            exit 0
-        fi
-    done
-    echo "(No PROOF-STATUS file found at root or docs/status/)"
+    @sed -n '/^== Ledger/,/^== /p' docs/status/PROOF-STATUS.adoc | sed '$d'

docs/proposals/awesome-estate-maths-proving.adoc

@@ -270,7 +270,8 @@ Reading the roster against the tools the lists above name shows what
 
 |*PROOF-POLICY names them* (highest priority: the estate's own mapping
 cannot be dispatched through its own prover platform)
-|Creusot, Kani, Aeneas (with Charon), Lambdapi as a checker (Dedukti has a
+|Creusot, Verus (a default Rust verifier since 2026-11-07), Kani, Aeneas (with
+Charon), Lambdapi as a checker (Dedukti has a
 variant, Lambdapi only an exchange format), agda2dedukti as a translator,
 Yices (in the kit manifest as a backend).
 

docs/proposals/boj-prover-solver-cartridges.adoc

@@ -113,12 +113,21 @@ json`; the five-level trust hierarchy and the axiom scan are echidna's.
 |`provers_portfolio`
 |Same input, two or more provers; returns each verdict and the combined
 trust level (level 5 only when two independent small-kernel systems agree
-with certificates, per echidna's `confidence.rs`).
+with certificates, per echidna's `confidence.rs`). echidna's trust level is
+not a Proof Witness Grade (PROOF-POLICY §8.6) and is never reported as one.
 
 |`provers_recheck`
 |The PROOF-POLICY §2 route: an Agda proof transported through Dedukti to
 Rocq and Lean, with `transported` or `re-proved` recorded per leg and the
 statement comparison named. Needs the kit's `transport` entries present.
+The Agda leg runs as `agda --safe --without-K --cubical-compatible` (§2.1).
+Each leg's record carries the §2.2 fields: the exact proposition,
+assumptions, source revision, checker and library versions by lock hash,
+invocation and observed result. It also carries two separate values: the
+leg's §5 status and its §2.2 correspondence state (`AGDA-PENDING`,
+`AGDA-VERIFIED`, `COQ-CHECKED`, `LEAN-CHECKED`, `BRIDGE-PENDING`,
+`RECONCILED`, `COUNTEREXAMPLE`, `QUARANTINED`). A transported leg stays
+`ASSUMED` until the statement comparison is recorded (§2).
 
 |`provers_exchange`
 |Translate between Dedukti, Lambdapi, TPTP, SMT-LIB, OpenTheory, SMTCoq
@@ -181,7 +190,9 @@ through one implementation.
 Input is a source tree with contracts; the answer is a proof ledger in
 the PROOF-POLICY §5 vocabulary (`PROVEN`, `PROVEN-WITH-AXIOMS`, `TESTED`,
 `ASSUMED`, `OPEN`) with a receipt. This is the cartridge for the tools that
-sit *on* code rather than on proof files: Creusot and Kani for Rust, SPARK
+sit *on* code rather than on proof files: Creusot (with Pearlite contracts)
+and Verus for Rust, the default pair since 2026-11-07 (PROOF-POLICY §1.2),
+with Kani as a standing exception; SPARK
 for Ada, Aeneas for Rust-to-model, Dafny, Why3 and Cameleer, F*, and the
 estate's own verifiers as they arrive: Quintessence (Elixir/OTP, three
 layers, already producing TrustLevel 4 certificates), Apodeixis.jl (Julia;
@@ -195,8 +206,11 @@ bactarin has no repository in the estate listing).
 
 |`verifiers_list`
 |The language-to-verifier mapping this host can serve, from PROOF-POLICY
-§1 and the capability record: Rust → Creusot (+ Kani, Aeneas), Ada → SPARK,
-Elixir → Quintessence, Julia → Apodeixis.jl, and the §4 exceptions.
+§1 and the capability record: Rust → Creusot and Verus (+ Kani, Aeneas),
+Ada → SPARK, Elixir → Quintessence, Julia → Apodeixis.jl, and the §4
+exceptions. Where Creusot and Verus prove the same property, the ledger
+records how the two statements correspond. It does not count them as
+independent results, because they share solver trust (§1.2, §4.1).
 
 |`verifiers_verify`
 |`{path, language?, tool?, obligations?}` → the ledger: one row per
@@ -346,14 +360,31 @@ are Idris2:
   host holds.
 * The ledger row. The §5 vocabulary is a closed sum type; a `TESTED` row
   carries bounds and a `PROVEN` row carries a certificate reference by
-  construction.
+  construction. A recheck row carries the §2.2 correspondence state as a
+  second closed type in its own field, so the two can never be written
+  into each other's place, as §2.2 requires.
+
+Status, correspondence state and Proof Witness Grade are three separate
+fields (PROOF-POLICY §2.2, §8). The cartridges write the first two and never
+the third. Mathesis derives a theorem's grade from the receipts and
+correspondence records these tools emit, and it never assigns one
+(Mathesis `docs/standards/AUTHORITY.adoc`). So every receipt carries what
+that derivation needs: the source commit, each checker's version and lock
+hash, the invocation and safe-mode flags, and the observed result. An Agda
+receipt also carries the library pin (name, version and lock hash of the
+standard library or other library it imports) and its import cone. The cone
+is the root module, the flags in force and the postulate count across
+every transitively imported module (PROOF-POLICY §1.1). Without them, a
+dependency cannot be counted as checked rather than assumed.
 
 One theory statement is worth an Agda file: echidna's five trust levels
 form a chain, and a portfolio's level is the meet of its members' levels
 except for the one case (two independent small-kernel systems, both with
 certificates) that lifts to level 5. Stating that as a lattice property and
 rechecking it in Rocq and Lean per §2 is small, and it is the property an
-agent relies on when it reads `trust_level: 5`.
+agent relies on when it reads `trust_level: 5`. It is theory about echidna,
+so it belongs in `hyperpolymath/echidna`; this repository's
+`docs/status/PROOF-STATUS.adoc` lists it as `OPEN` there.
 
 == Aspects