fix(proofs): DOM-1/DOM-2 corrected, checked in CI with pinned Agda, graded PWG-3 from receipts

.github/workflows/proof-safety.yml

@@ -64,3 +64,40 @@ jobs:
           ECHIDNA_BIN: ${{ github.workspace }}/_echidna/target/debug/echidna
         run: |
           bash tests/e2e.sh
+  agda:
+    # DOM-1/DOM-2 (Agda theory). The check-run name agda-proofs is the
+    # contract echidna's W0 gate (check 12) reads. PROOF-POLICY §2.1 invocation with the
+    # pinned Agda 2.7.0.1 and agda-stdlib 2.1 (digests in setup-agda.sh),
+    # then the §8.2 cone receipt each theorem's PWG is derived from. A
+    # missing or wrong toolchain fails the job; it never skips.
+    name: agda-proofs
+    runs-on: ubuntu-24.04
+    timeout-minutes: 20
+    steps:
+      - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1
+        with:
+          persist-credentials: false
+      - name: Install pinned Agda and standard library
+        run: bash scripts/ci/setup-agda.sh
+      - name: Type-check under the §2.1 invocation (through the wrapper)
+        run: |
+          set -euo pipefail
+          stdlib_src="$(dirname "$(head -n 1 "$AGDA_LIBRARIES_FILE")")/src"
+          AGDA_LIBRARY_INCLUDE="$stdlib_src" bash scripts/agda-safe-check.sh \
+            verification/proofs/agda/Burrow/Trust.agda verification/proofs/agda/Burrow/Ledger.agda
+      - name: Record the §8.2 cone receipts
+        env:
+          AGDA_STDLIB_SHA256: 72ca3ea25094efa0439e106f0d949330414232ec4cc5c3c3316e7e70dd06d431
+        run: |
+          set -euo pipefail
+          bash scripts/ci/test-agda-cone-receipt.sh
+          receipts="$RUNNER_TEMP/agda-cone-receipts.jsonl"
+          : > "$receipts"
+          for m in Burrow/Trust.agda Burrow/Ledger.agda; do
+            (cd verification/proofs/agda && bash ../../../scripts/ci/agda-cone-receipt.sh "$m") >> "$receipts"
+          done
+          cat "$receipts"
+          {
+            echo '## PROOF-POLICY §8.2 cone receipts (DOM-1, DOM-2)'
+            jq -r '"\(.source.entrypoint) at \(.source.commit): \(.toolchain.agda), \(.import_cone.count) modules, scan \(.postulate_scan.result)"' "$receipts"
+          } >> "$GITHUB_STEP_SUMMARY"

CLAUDE.md

@@ -45,26 +45,31 @@ file, not this summary.
 
 | Obligation | Verifier |
 |------------|----------|
-| First-party Rust (`burrower-core`, `-cli`, `-wasm`) | Creusot |
+| First-party Rust (`burrower-core`, `-cli`, `-wasm`) | Creusot with Pearlite contracts, and Verus (§1.2) |
 | APIs, ABIs, wire formats, engineering properties | Idris2 |
 | Theory (anything true of any implementation) | Agda, rechecked in Rocq and Lean |
 
 - Canonical Agda invocation, in recipes and CI alike:
   `agda --safe --without-K --cubical-compatible <module.agda>`.
   `--cubical-compatible` is not full `--cubical`. Pin and record the Agda
   version and standard library with each source commit and proof result.
-- Grade ladder (Mathesis §5): Grade 3 = type-checks locally in Agda,
-  untranslated; 2i = one independent system; 2ii = two, the second
-  non-DTT (e.g. Isabelle/HOL); 1 = machine-checked via a verified checker
-  API in headless CI. Never flatten this into a confidence percentage.
+- Proof grades are PROOF-POLICY §8 *Proof Witness Grades*, weakest to
+  strongest, always with the
+  prefix: `PWG-3` (Agda checks under §2.1, with a receipt) < `PWG-2i` (one
+  Rocq or Lean leg, kernel-checked and RECONCILED) < `PWG-2ii` (both legs)
+  < `PWG-1` (per-commit receipts from a pinned headless checker). A non-DTT
+  witness such as Isabelle/HOL is the tag `+foundation-diverse`, not a
+  grade. Grades are derived from receipts, never asserted. Report a census
+  with its denominator, never a percentage.
 - Missing tools, incompatible dependencies or failed theorems are open
   obligations. Do not skip proofs or weaken flags to make a check green.
 - Escape hatches follow `docs/TRUSTED-BASE-REDUCTION-POLICY.adoc` and are
   recorded in `docs/proof-debt.adoc`.
 - An ECHIDNA result is *evidence about someone else's proof*. Burrower
   records the grade it was told and never asserts one it derived.
 
-Status for this repo: 0 of 7 obligations proven; no first-party Agda
-theorem yet, so nothing here is at Grade 3. See
+Status for this repo: DOM-1 and DOM-2 (Agda theory) are `PWG-3` (2 of 2),
+derived from `docs/reports/2026-11-09-agda-cone-receipts.jsonl`; no Rocq or
+Lean leg yet. See
 `docs/status/PROOF-STATUS.adoc` and
 `docs/reports/audit/2026-11-01-echidna-topology-audit.adoc`.

Justfile

@@ -1351,8 +1351,10 @@ proof-check-idris2:
     set -euo pipefail
     echo "=== Checking Idris2 proofs ==="
     if ! command -v idris2 &>/dev/null; then
-        echo "SKIP: idris2 not installed"
-        exit 0
+        # A missing prover is an open obligation, never a pass
+        # (PROOF-POLICY §2.1: do not skip proofs to make a check green).
+        echo "NOT RUN: idris2 not installed"
+        exit 1
     fi
     ERRORS=0
     for f in $(find verification/proofs/idris2 -name '*.idr' 2>/dev/null); do
@@ -1376,8 +1378,10 @@ proof-check-lean4:
     set -euo pipefail
     echo "=== Checking Lean4 proofs ==="
     if ! command -v lean &>/dev/null; then
-        echo "SKIP: lean not installed"
-        exit 0
+        # A missing prover is an open obligation, never a pass
+        # (PROOF-POLICY §2.1: do not skip proofs to make a check green).
+        echo "NOT RUN: lean not installed"
+        exit 1
     fi
     ERRORS=0
     for f in $(find verification/proofs/lean4 -name '*.lean' 2>/dev/null); do
@@ -1401,8 +1405,10 @@ proof-check-agda:
     set -euo pipefail
     echo "=== Checking Agda proofs ==="
     if ! command -v agda &>/dev/null; then
-        echo "SKIP: agda not installed"
-        exit 0
+        # A missing prover is an open obligation, never a pass
+        # (PROOF-POLICY §2.1: do not skip proofs to make a check green).
+        echo "NOT RUN: agda not installed"
+        exit 1
     fi
     # Estate canonical invocation (standards 3-practice/PROOF-POLICY.adoc
     # §2.1). `--cubical-compatible` implies `--without-K`; both are named
@@ -1441,8 +1447,10 @@ proof-check-coq:
     set -euo pipefail
     echo "=== Checking Coq proofs ==="
     if ! command -v coqc &>/dev/null; then
-        echo "SKIP: coqc not installed"
-        exit 0
+        # A missing prover is an open obligation, never a pass
+        # (PROOF-POLICY §2.1: do not skip proofs to make a check green).
+        echo "NOT RUN: coqc not installed"
+        exit 1
     fi
     ERRORS=0
     for f in $(find verification/proofs/coq -name '*.v' 2>/dev/null); do
@@ -1460,26 +1468,10 @@ proof-check-coq:
     fi
     echo "PASS: All Coq proofs verified"
 
-# Scan for dangerous patterns in proof files (believe_me, sorry, Admitted, etc.)
+# Scan proof sources for escape hatches (believe_me, postulate, sorry,
+# Admitted, unsafe pragmas, ...), ignoring comments
 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"
+    bash scripts/proof-scan-dangerous.sh verification/proofs
 
 # Show proof status summary
 proof-status:

docs/reports/2026-11-09-agda-cone-receipts.jsonl

@@ -0,0 +1,2 @@
+{"import_cone":{"count":34,"modules":[{"module":"Agda.Builtin.Bool","origin":"agda-kernel","sha256":"514fa25a0df7064cdb213507a0f6332c97288a52d538be3a9df06cc7001ba7f5"},{"module":"Agda.Builtin.Equality","origin":"agda-kernel","sha256":"5735edb0be7e530133814e9431d1466bb1e7892c2a4746c1a0d2a3a0dbea91cd"},{"module":"Agda.Builtin.Maybe","origin":"agda-kernel","sha256":"982f7f2afbfbc4ac41b6bdafddfb5e032a5ddfa71e204f39bbecc23967dc4808"},{"module":"Agda.Builtin.Sigma","origin":"agda-kernel","sha256":"5c393f230b359032f64ff78ad693799a162dbf9cada2089048aedb4c6f669e1f"},{"module":"Agda.Builtin.Unit","origin":"agda-kernel","sha256":"03d06283f9d8005beff99fd42de38b7315aa7697099ea22fc19d060600b16249"},{"module":"Agda.Primitive","origin":"agda-kernel","sha256":"e5e4e04900cf1a28202e2ff26bb20d6fa6401fcc9f4049cd8d14fedd5bd697f8"},{"module":"Burrow.Trust","origin":"first-party","sha256":"5ba1de66b2e4845b7d3663bba338481697e87712cf32da3bb55816da775cce06"},{"module":"Data.Bool.Base","origin":"library","sha256":"124e425ebafee9cbe8fb496b4c8467fdd372b0961ca03e445bfda506738204f6"},{"module":"Data.Empty","origin":"library","sha256":"3a68a9e529c13054202a3892bfcf961bb75db2dc11d63f068189c4cbd48c2cd2"},{"module":"Data.Irrelevant","origin":"library","sha256":"5f225770f471847144eb3908fecb1d4b0a06e7d7b1cb3a12bdebd840bf17a783"},{"module":"Data.Product.Base","origin":"library","sha256":"e2585b0cc6d0c2486cf1f30bd98a3855b00666e8aa8bc0aee5be8253c952a99c"},{"module":"Data.Sum.Base","origin":"library","sha256":"2733ba66eaed94cc0f0b21f2a9ed0533f8a31b5bd487e40384632f1d6204fcfd"},{"module":"Data.Unit","origin":"library","sha256":"320fc4c784fbb6ad847f41ae317f60da346002a119cbca178b2caaa787c2b26c"},{"module":"Data.Unit.Base","origin":"library","sha256":"38cc799f18b6f106336ace8ae66c5a171251c0eb3b6bf32124e33c45d441b2fb"},{"module":"Data.Unit.Polymorphic.Base","origin":"library","sha256":"002ae814be1dafd6f6c4193a2254ee19f7793ffef7dcf1d29f9794db0b19f2a8"},{"module":"Data.Unit.Properties","origin":"library","sha256":"bb9a390596f27739aa9d9c46ef666e42917df4f5000f675ef1042abe3fe2fc62"},{"module":"Function.Base","origin":"library","sha256":"b021bf843c1974a5d50a1a3362f2d6447018629331a3dc2bb0d9ea85ec029e84"},{"module":"Level","origin":"library","sha256":"1168f8373370c10aec0f20bae0cc43db9a34331a49deb4c72efd2574a638a278"},{"module":"Relation.Binary.Bundles","origin":"library","sha256":"fd4b0a832bf9f372d2739668c7e0988e0242519686b69616dc67043923ad88c3"},{"module":"Relation.Binary.Consequences","origin":"library","sha256":"d5f1d178492b9e485a3efdcb16dd18fe623896371e2cae3662d8fde1ff94a455"},{"module":"Relation.Binary.Construct.Composition","origin":"library","sha256":"829ca14501f085b08a0504a61c7874cd20cce07ffc883027ef3465e4f44cf347"},{"module":"Relation.Binary.Core","origin":"library","sha256":"09eda35f4c2f795542f0a2468ade41793e9c9e07889553989e03d343902fcb81"},{"module":"Relation.Binary.Definitions","origin":"library","sha256":"c61495efb42702588229a67461c451dd660bd5d686c244ee1895b9d563547783"},{"module":"Relation.Binary.Properties.Setoid","origin":"library","sha256":"ba05a90fbede6b120c7aefe56944f0c5c772f908a1f60d1644ec4c70c9a93293"},{"module":"Relation.Binary.PropositionalEquality.Core","origin":"library","sha256":"480da0675a0d8ddddcae5c4f74c5526a5da88790fef387aa8b8213dabf842200"},{"module":"Relation.Binary.PropositionalEquality.Properties","origin":"library","sha256":"4ed071c430e9244d3be9b9ca847d74232826c0fed7bf3035da0a6d4a8c7b2137"},{"module":"Relation.Binary.Reasoning.Syntax","origin":"library","sha256":"a7a831d62ed2a3c7d5d0f29521162fbf264d34a48b6c91e9ac9f6168c2067ceb"},{"module":"Relation.Binary.Structures","origin":"library","sha256":"12ccbc4bd7da510ed8edf17018eb10b3d827e08ba1842a623c3370c2cb6ef396"},{"module":"Relation.Nullary","origin":"library","sha256":"56f7f4a54b8d655b0c90dacfd65d29cfc2d7e73d8666bd30a934ae25818a5019"},{"module":"Relation.Nullary.Decidable.Core","origin":"library","sha256":"0082f72e3d2bd247d56d46abf3f70936a08d32c69c3a18cb68f744c8fefb67b8"},{"module":"Relation.Nullary.Negation.Core","origin":"library","sha256":"b848e89c226674f8462c9c5aced87e5aa3fe03fdf9cbaffd0c28e9f87ff6c910"},{"module":"Relation.Nullary.Recomputable","origin":"library","sha256":"cacf1a1d98ceed1571bac2ca9a3c1f9967ea6c91fd0dc0ed35b5fc74657b7ce0"},{"module":"Relation.Nullary.Reflects","origin":"library","sha256":"73ec20b5e43a3903b68b994cd0815b9d0c3dcc9e57dae39b4d8b487904a7eea1"},{"module":"Relation.Unary","origin":"library","sha256":"4960f1b9004f19834cbc0271b80a64281a99ba715ffa125f73df80f205745a71"}]},"kind":"agda-cone-receipt","policy":"standards 3-practice/PROOF-POLICY.adoc §8.2, §8.4","postulate_scan":{"findings":[],"kernel_primitives":[{"line":26,"module":"Agda.Primitive","text":"postulate"},{"line":34,"module":"Agda.Primitive","text":"postulate"}],"method":"comment-aware: nested block and line comments removed, pragmas kept; string literals not lexed","result":"clean"},"schema_version":1,"source":{"commit":"22f6f723fce6e7ae1a1f145b7954f731aa12a033","entrypoint":"Burrow/Trust.agda","repository":"https://github.com/hyperpolymath/proof-burrower","uncommitted_changes_under_entry_dir":false},"toolchain":{"agda":"Agda version 2.7.0.1","agda_executable_sha256":"6de41437c14c05c9fe576d724cc67386444c0fa9fee662a08250fefb91bee8b6","flags":["--safe","--without-K","--cubical-compatible"],"stdlib_archive_sha256":"72ca3ea25094efa0439e106f0d949330414232ec4cc5c3c3316e7e70dd06d431"}}
+{"import_cone":{"count":35,"modules":[{"module":"Agda.Builtin.Bool","origin":"agda-kernel","sha256":"514fa25a0df7064cdb213507a0f6332c97288a52d538be3a9df06cc7001ba7f5"},{"module":"Agda.Builtin.Equality","origin":"agda-kernel","sha256":"5735edb0be7e530133814e9431d1466bb1e7892c2a4746c1a0d2a3a0dbea91cd"},{"module":"Agda.Builtin.Maybe","origin":"agda-kernel","sha256":"982f7f2afbfbc4ac41b6bdafddfb5e032a5ddfa71e204f39bbecc23967dc4808"},{"module":"Agda.Builtin.Sigma","origin":"agda-kernel","sha256":"5c393f230b359032f64ff78ad693799a162dbf9cada2089048aedb4c6f669e1f"},{"module":"Agda.Builtin.Unit","origin":"agda-kernel","sha256":"03d06283f9d8005beff99fd42de38b7315aa7697099ea22fc19d060600b16249"},{"module":"Agda.Primitive","origin":"agda-kernel","sha256":"e5e4e04900cf1a28202e2ff26bb20d6fa6401fcc9f4049cd8d14fedd5bd697f8"},{"module":"Burrow.Ledger","origin":"first-party","sha256":"eaf110f4f0b97fe0ba6d74f21f65881241600ce8299288fe47ba10e6ff45ae64"},{"module":"Burrow.Trust","origin":"first-party","sha256":"5ba1de66b2e4845b7d3663bba338481697e87712cf32da3bb55816da775cce06"},{"module":"Data.Bool.Base","origin":"library","sha256":"124e425ebafee9cbe8fb496b4c8467fdd372b0961ca03e445bfda506738204f6"},{"module":"Data.Empty","origin":"library","sha256":"3a68a9e529c13054202a3892bfcf961bb75db2dc11d63f068189c4cbd48c2cd2"},{"module":"Data.Irrelevant","origin":"library","sha256":"5f225770f471847144eb3908fecb1d4b0a06e7d7b1cb3a12bdebd840bf17a783"},{"module":"Data.Product.Base","origin":"library","sha256":"e2585b0cc6d0c2486cf1f30bd98a3855b00666e8aa8bc0aee5be8253c952a99c"},{"module":"Data.Sum.Base","origin":"library","sha256":"2733ba66eaed94cc0f0b21f2a9ed0533f8a31b5bd487e40384632f1d6204fcfd"},{"module":"Data.Unit","origin":"library","sha256":"320fc4c784fbb6ad847f41ae317f60da346002a119cbca178b2caaa787c2b26c"},{"module":"Data.Unit.Base","origin":"library","sha256":"38cc799f18b6f106336ace8ae66c5a171251c0eb3b6bf32124e33c45d441b2fb"},{"module":"Data.Unit.Polymorphic.Base","origin":"library","sha256":"002ae814be1dafd6f6c4193a2254ee19f7793ffef7dcf1d29f9794db0b19f2a8"},{"module":"Data.Unit.Properties","origin":"library","sha256":"bb9a390596f27739aa9d9c46ef666e42917df4f5000f675ef1042abe3fe2fc62"},{"module":"Function.Base","origin":"library","sha256":"b021bf843c1974a5d50a1a3362f2d6447018629331a3dc2bb0d9ea85ec029e84"},{"module":"Level","origin":"library","sha256":"1168f8373370c10aec0f20bae0cc43db9a34331a49deb4c72efd2574a638a278"},{"module":"Relation.Binary.Bundles","origin":"library","sha256":"fd4b0a832bf9f372d2739668c7e0988e0242519686b69616dc67043923ad88c3"},{"module":"Relation.Binary.Consequences","origin":"library","sha256":"d5f1d178492b9e485a3efdcb16dd18fe623896371e2cae3662d8fde1ff94a455"},{"module":"Relation.Binary.Construct.Composition","origin":"library","sha256":"829ca14501f085b08a0504a61c7874cd20cce07ffc883027ef3465e4f44cf347"},{"module":"Relation.Binary.Core","origin":"library","sha256":"09eda35f4c2f795542f0a2468ade41793e9c9e07889553989e03d343902fcb81"},{"module":"Relation.Binary.Definitions","origin":"library","sha256":"c61495efb42702588229a67461c451dd660bd5d686c244ee1895b9d563547783"},{"module":"Relation.Binary.Properties.Setoid","origin":"library","sha256":"ba05a90fbede6b120c7aefe56944f0c5c772f908a1f60d1644ec4c70c9a93293"},{"module":"Relation.Binary.PropositionalEquality.Core","origin":"library","sha256":"480da0675a0d8ddddcae5c4f74c5526a5da88790fef387aa8b8213dabf842200"},{"module":"Relation.Binary.PropositionalEquality.Properties","origin":"library","sha256":"4ed071c430e9244d3be9b9ca847d74232826c0fed7bf3035da0a6d4a8c7b2137"},{"module":"Relation.Binary.Reasoning.Syntax","origin":"library","sha256":"a7a831d62ed2a3c7d5d0f29521162fbf264d34a48b6c91e9ac9f6168c2067ceb"},{"module":"Relation.Binary.Structures","origin":"library","sha256":"12ccbc4bd7da510ed8edf17018eb10b3d827e08ba1842a623c3370c2cb6ef396"},{"module":"Relation.Nullary","origin":"library","sha256":"56f7f4a54b8d655b0c90dacfd65d29cfc2d7e73d8666bd30a934ae25818a5019"},{"module":"Relation.Nullary.Decidable.Core","origin":"library","sha256":"0082f72e3d2bd247d56d46abf3f70936a08d32c69c3a18cb68f744c8fefb67b8"},{"module":"Relation.Nullary.Negation.Core","origin":"library","sha256":"b848e89c226674f8462c9c5aced87e5aa3fe03fdf9cbaffd0c28e9f87ff6c910"},{"module":"Relation.Nullary.Recomputable","origin":"library","sha256":"cacf1a1d98ceed1571bac2ca9a3c1f9967ea6c91fd0dc0ed35b5fc74657b7ce0"},{"module":"Relation.Nullary.Reflects","origin":"library","sha256":"73ec20b5e43a3903b68b994cd0815b9d0c3dcc9e57dae39b4d8b487904a7eea1"},{"module":"Relation.Unary","origin":"library","sha256":"4960f1b9004f19834cbc0271b80a64281a99ba715ffa125f73df80f205745a71"}]},"kind":"agda-cone-receipt","policy":"standards 3-practice/PROOF-POLICY.adoc §8.2, §8.4","postulate_scan":{"findings":[],"kernel_primitives":[{"line":26,"module":"Agda.Primitive","text":"postulate"},{"line":34,"module":"Agda.Primitive","text":"postulate"}],"method":"comment-aware: nested block and line comments removed, pragmas kept; string literals not lexed","result":"clean"},"schema_version":1,"source":{"commit":"22f6f723fce6e7ae1a1f145b7954f731aa12a033","entrypoint":"Burrow/Ledger.agda","repository":"https://github.com/hyperpolymath/proof-burrower","uncommitted_changes_under_entry_dir":false},"toolchain":{"agda":"Agda version 2.7.0.1","agda_executable_sha256":"6de41437c14c05c9fe576d724cc67386444c0fa9fee662a08250fefb91bee8b6","flags":["--safe","--without-K","--cubical-compatible"],"stdlib_archive_sha256":"72ca3ea25094efa0439e106f0d949330414232ec4cc5c3c3316e7e70dd06d431"}}