From 47700b7116e0458a9c381b849f34c138d973f764 Mon Sep 17 00:00:00 2001
From: Claude <noreply@anthropic.com>
Date: Mon, 9 Nov 2026 13:04:51 +0000
Subject: [PATCH 1/5] =?UTF-8?q?proofs:=20record=20theory=20grades=20as=20P?=
 =?UTF-8?q?ROOF-POLICY=20=C2=A78=20PWG;=20scan=20the=20import=20cone?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

The grade records were written against the mathesis brief on 2026-11-01,
before the owner ruling of 2026-11-04 made PROOF-POLICY §8 normative:

- The five theory rows (G-1, T-1, T-2, T-3, E-1m) are PWG-3, written with
  the prefix. The brief's "2ii needs Isabelle/HOL" is replaced by §8.3's
  +foundation-diverse tag.
- The receipt is the current green agda-proofs run 42076969251 at 23bc8c3,
  covering all three modules under the §2.1 canonical invocation, with
  library pin, flags, import cone and axioms recorded. Runs 41687715055 and
  40867211509 are kept as state: superseded. The page had still cited the
  pre-flag receipt it said it would replace.
- The duplicated row counts, which had drifted (23 against 27 TESTED), are
  removed from PROOF-GRADES; PROOF-NEEDS stays the only count.
- Rust's verifiers read Creusot/Pearlite and Verus (§1.2, 2026-11-07).

§8.4 asks for a comment-aware postulate scan of the import cone beside
--safe. scripts/scan-postulates.sh does that, and check-agda.sh runs it on
the proofs and the pinned resource-algebra sibling with a negative and a
positive control written at run time. Verified locally: cone 10 files, 0
postulates; a mutant scan that reports nothing fails the gate.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01GVPPsHYqVJSoPzdNYD9tRg
---
 PROOF-NEEDS.adoc              |  55 ++++++-----
 docs/theory/PROOF-GRADES.adoc | 169 +++++++++++++++++++---------------
 scripts/check-agda.sh         |  19 ++++
 scripts/scan-postulates.sh    |  40 ++++++++
 4 files changed, 183 insertions(+), 100 deletions(-)
 create mode 100644 scripts/scan-postulates.sh

diff --git a/PROOF-NEEDS.adoc b/PROOF-NEEDS.adoc
index 9ea6b33..d0d73b4 100644
--- a/PROOF-NEEDS.adoc
+++ b/PROOF-NEEDS.adoc
@@ -110,46 +110,45 @@ IO do-notation at all.
 The dashboards (README, TOPOLOGY, READINESS) carry the proof count that
 `+dashboard-check+` measures from the PROVEN rows of the ledger below.
 
-=== Proof grades under mathesis (2026-11-01)
+=== Proof Witness Grades (PROOF-POLICY §8)
 
 The five statuses above are this repository's claim vocabulary — the estate's
-README-EXPLAINME ledger, as used across it. A *proof grade* is a second,
-orthogonal axis, governed by `+hyperpolymath/mathesis+`
-(`+estate-mathematical-architecture+` §5 and §6) and by
-`+hyperpolymath/standards+` `+3-practice/PROOF-POLICY.adoc+`. Neither uses a
-confidence percentage and this repository does not publish one.
+README-EXPLAINME ledger, as used across it. A *Proof Witness Grade* is a second,
+orthogonal axis, governed by `+hyperpolymath/standards+`
+`+3-practice/PROOF-POLICY.adoc+` §8 (owner ruling 2026-11-04). The mathesis
+brief (`+estate-mathematical-architecture+` §5 and §6) first proposed the ladder
+and is kept for provenance only. Neither uses a confidence percentage and this
+repository does not publish one.
 
 Of the 12 PROVEN rows, five are the theory rows — **G-1, T-1, T-2, T-3, E-1m** — and
-their artefact is Agda (`+verification/proofs/agda/+`). They are **Grade 3**:
-each type-checks in Agda and none has been translated to an independent
-foundational system, which is mathesis §5's definition as written. The receipt
-is a green `+agda-proofs.yml+` run
-(https://github.com/hyperpolymath/januskey/actions/runs/41687715055[41687715055])
-at commit `+fc188c4+`, Agda 2.6.4.3, with `+resource-algebra+` pinned at
-`+cf9235c+`. That run used the current gate (`+Reversibility+`,
-`+TransactionAtomicity+` and `+Epistemic+` under `+--safe --without-K
---cubical-compatible+`), and the modules, the gate script, the sibling fetch and
-the workflow are byte-identical at that commit and at this one, so the receipt
-covers these rows, E-1m included, as they stand. (An earlier receipt cited here,
-run 40867211509 at `+4afb710+`, predates `+Epistemic.agda+` and the
-`+--cubical-compatible+` flag, so it never covered E-1m.) Mathesis status for them:
-`+AGDA-VERIFIED+`.
+their artefact is Agda (`+verification/proofs/agda/+`). They are **`+PWG-3+`**
+(PROOF-POLICY §8, owner ruling 2026-11-04, which governs over the mathesis brief):
+each is `+PROVEN+` under the §2.1 invocation and no Rocq or Lean leg exists. The
+receipt is a green `+agda-proofs.yml+` run
+(https://github.com/hyperpolymath/januskey/actions/runs/42076969251[42076969251])
+at commit `+23bc8c3+`, Agda 2.6.4.3, with `+resource-algebra+` pinned at
+`+cf9235c+`, running `+Reversibility+`, `+TransactionAtomicity+` and
+`+Epistemic+` under `+--safe --without-K --cubical-compatible+`. Its import cone,
+axioms (none) and the receipts it supersedes (runs 41687715055 at `+fc188c4+`
+and 40867211509 at `+4afb710+`) are recorded in
+link:docs/theory/PROOF-GRADES.adoc[`+docs/theory/PROOF-GRADES.adoc+`].
+Correspondence state for them: `+AGDA-VERIFIED+`.
 
 The other seven PROVEN rows — A-1, A-2, C-1 to C-5 — are Idris2 theorems. Under
 PROOF-POLICY §1 those are interface and ABI contracts, so the theory ladder does
 not grade them: they are PROVEN in the vocabulary above and nothing more. The
-same holds for the 27 TESTED rows, which record observed behaviour and never
-grading. First-party Rust behaviour belongs to **Creusot** (not SPARK, and not
-Idris2); no Creusot contract exists in this tree, which is why no Rust row is
-graded.
+same holds for the TESTED rows, which record observed behaviour and never
+grading. First-party Rust behaviour belongs to **Creusot** with **Pearlite**
+contracts, and **Verus** (PROOF-POLICY §1.2, owner ruling 2026-11-07; not SPARK,
+and not Idris2); neither verifier has a contract or proof in this tree yet,
+which is why no Rust row is proved.
 
-No row of this ledger is Grade 2i, Grade 2ii or Grade 1, and none is claimed to
+No row of this ledger is `+PWG-2i+`, `+PWG-2ii+` or `+PWG-1+`, and none is claimed to
 be. The row-by-row mapping and the receipt in full are in
 `+docs/theory/PROOF-GRADES.adoc+`. Since 2026-11-01 the gate runs
 PROOF-POLICY §2.1's canonical invocation
-(`+--safe --without-K --cubical-compatible …+`), which was verified locally
-with Agda 2.6.4.3 before being committed; the CI receipt for that flag set is
-the next `+agda-proofs.yml+` run, not the older one.
+(`+--safe --without-K --cubical-compatible …+`); the CI receipt for that flag
+set is run 42076969251 above.
 
 === Current State
 
diff --git a/docs/theory/PROOF-GRADES.adoc b/docs/theory/PROOF-GRADES.adoc
index 6fed117..60e6367 100644
--- a/docs/theory/PROOF-GRADES.adoc
+++ b/docs/theory/PROOF-GRADES.adoc
@@ -12,32 +12,42 @@ repository, and none is introduced here.
 
 == What governs the grades
 
-Two owner documents, both read at HEAD on 2026-11-01:
+Since the owner ruling of 2026-11-04, `PROOF-POLICY.adoc` §8 is normative for
+grades, and they are written with their prefix: `PWG-3`, `PWG-2i`, `PWG-2ii`,
+`PWG-1`, or `ungraded`. The mathesis brief that first proposed the ladder is
+kept for provenance only; where the two differ, §8 governs. This page was first
+written against the brief (2026-11-01) and was brought in line with §8 on
+2026-11-09.
 
 [cols="1,2,3",options="header"]
 |===
 | Source | Section | Rule taken from it
 
-| `hyperpolymath/mathesis`,
-  file `estate-mathematical-architecture`
-| §5 grades
-| **Grade 3** — "a proof is Grade 3 if it type-checks locally in Agda but has
-  not been translated to an independent foundational system". Grade 2i adds one
-  translation, Grade 2ii two *foundationally distinct* ones (Agda, Rocq and
-  Lean are all dependent type theory, so 2ii needs Isabelle/HOL), Grade 1 is a
-  check served to headless CI tooling (AXLE, isabelle server, coq-lsp REST).
-
-| mathesis, same file
-| §6 reporting
-| No percentage; every axiom the development relies on is tracked; a grade
-  receipt records the **commit hash** it was produced at; a grade that stops
-  applying is marked `Superseded` or `Regressed`, never quietly deleted.
+| `hyperpolymath/standards`,
+  `3-practice/PROOF-POLICY.adoc`
+| §8 Proof Witness Grades
+| `PWG-3`: the Agda proof is `PROVEN` under the §2.1 invocation, with the
+  receipt recording the Agda version, library pin, flags and import cone.
+  `PWG-2i`: plus one counted Rocq or Lean leg (`RECONCILED`). `PWG-2ii`: plus
+  both. `PWG-1`: plus current receipts per commit for every counted witness. A
+  witness in a different foundation (Isabelle/HOL and the like) is the tag
+  `+foundation-diverse`, never a grade: the brief's "2ii needs Isabelle/HOL"
+  reading is corrected by §8.3.
+
+| PROOF-POLICY
+| §8.4 rules
+| A grade is derived from receipts, never asserted; no percentage, only a
+  census with its denominator; every counted witness lists its axioms (for
+  Agda: `--safe`, a comment-aware postulate scan of the import cone, and the
+  recorded cone); a receipt no longer current carries `state: superseded` or
+  `state: regressed`, never deleted.
 
 | `hyperpolymath/standards`,
   `3-practice/PROOF-POLICY.adoc`
 | §1 mapping
 | Theory is proved in **Agda** and rechecked in Rocq and Lean; the behaviour of
-  first-party Rust is **Creusot** on that code; API, ABI and wire-format
+  first-party Rust is **Creusot** with **Pearlite** contracts, and **Verus**
+  (§1.2, owner ruling 2026-11-07), on that code; API, ABI and wire-format
   contracts are **Idris2**. The earlier "Rust always means Rust/SPARK" note is
   withdrawn (owner ruling 2026-04-10): Rust is Creusot.
 
@@ -59,11 +69,11 @@ januskey's own five-status ledger vocabulary (`PROVEN`, `TESTED`, `ASSUMED`,
 `DESIGNED`, `OPEN`) is the estate's claim vocabulary and is unchanged by any of
 this. A grade is a second axis laid over it, not a replacement: a row is
 `PROVEN` *because* a named artefact checks it, and separately has (or has not) a
-mathesis grade.
+Proof Witness Grade.
 
-== The Grade 3 receipt
+== The PWG-3 receipt
 
-The theory artefacts are two Agda modules:
+The theory artefacts are three Agda modules:
 
 * `verification/proofs/agda/Reversibility.agda` — the Loss grade algebra:
   lossless traces have only lossless steps, obliteration absorbs, and a
@@ -72,51 +82,70 @@ The theory artefacts are two Agda modules:
   state the transaction began in; the `TransactionManager` lifecycle keeps its
   log invariant under begin, add_operation, commit and mark_rolled_back, and at
   most one transaction is Active.
+* `verification/proofs/agda/Epistemic.agda` — the model-level half of E-1
+  (row E-1m, §The epistemic rewrite below).
 
-Both are checked by `scripts/check-agda.sh` (`just test-agda`), which is also
-the ledger's recorded checker for rows G-1, T-1, T-2 and T-3. The receipt:
+All three are checked by `scripts/check-agda.sh` (`just test-agda`), which is
+also the ledger's recorded checker for rows G-1, T-1, T-2, T-3 and E-1m. The
+current receipt (PROOF-POLICY §8.2, `PWG-3`):
 
 [cols="1,3",options="header"]
 |===
 | Field | Value
 
 | Workflow, run | `agda-proofs.yml`, run
-  https://github.com/hyperpolymath/januskey/actions/runs/40867211509[40867211509],
-  branch `main`, conclusion **success**
-| Commit | `4afb710e86646658f667f10bd6274ee47416bfc7` (started 2026-10-29T11:40:36Z)
+  https://github.com/hyperpolymath/januskey/actions/runs/42076969251[42076969251],
+  branch `main`, conclusion **success**, `state: current`
+| Commit | `23bc8c38160a25c37917bce69cf05d91899b07e5` (started 2026-11-05T17:40:46Z)
 | Prover | `agda-bin=2.6.4.3-1+b2` on Debian trixie-slim
   (`@sha256:a29215f6…`), asserted by a passing step:
   `test "$(agda --version)" = 'Agda version 2.6.4.3'`
-| Flags | `--safe --without-K --no-libraries --ignore-interfaces --double-check`
-  at the receipt commit; the gate now runs PROOF-POLICY §2.1's canonical form
-  with `--cubical-compatible` added (see §The §2.1 invocation below)
-| Sibling | `resource-algebra` at
+| Library pin | none: `--no-libraries`; the only import outside this tree is the
+  sibling below
+| Flags | `--safe --without-K --cubical-compatible --no-libraries
+  --ignore-interfaces --double-check`: the §2.1 canonical invocation, plus two
+  stricter options
+| Import cone | roots `Reversibility`, `TransactionAtomicity`, `Epistemic`; the
+  cone is those modules and `resource-algebra` at
   `cf9235c532712a783a404c359a1055f40134794a`, fetched by
-  `scripts/fetch-siblings.sh`; consumed by pin, not re-declared here
-| Result | The two modules in this receipt type-check; the fixtures under
+  `scripts/fetch-siblings.sh` and re-checked from source under the same flags
+  (`--ignore-interfaces`); consumed by pin, not re-declared here
+| Axioms | none. `--safe` refuses `postulate`; postulate count 0. The
+  comment-aware scan of the cone (`scripts/scan-postulates.sh`, wired into the
+  gate with a positive and a negative control on every run) was added after this
+  run, so its first CI receipt is the next `agda-proofs.yml` run on `main`;
+  a local run at this receipt's sources reported 10 files, 0 postulates
+| Result | The three modules type-check; the fixtures under
   `tests/reject-agda/` are refused *with the message each fixture names*, so a
   fixture that starts passing, or starts failing for the wrong reason, fails the
-  gate
-| Transfer | `Reversibility.agda`, `TransactionAtomicity.agda`,
-  `scripts/fetch-siblings.sh` and `agda-proofs.yml` are byte-identical at that
-  commit and at this branch's HEAD (blobs `0d30206…`, `38c9b06…`, `9b66a48…`,
-  `7c7e653…`), so the receipt covers those two rows as they stand. It does
-  **not** cover `Epistemic.agda` (new) or the changed `check-agda.sh`: their
-  first CI evidence is the run on this branch's pull request
+  gate. Agda reports `UnsupportedIndexedMatch` warnings (§The §2.1 invocation
+  below): they concern computation under cubical transports, not the
+  propositions, and are kept visible
 |===
 
-That is a Grade 3 receipt in mathesis terms: the propositions type-check in
-Agda, in CI, at a named commit, with the prover version pinned and recorded.
-mathesis §5 illustrates "strict solver flags" with `--safe --erasure`;
-januskey's strictness is `--safe --without-K` plus `--double-check`, which is
-the same family and stricter than bare `--safe` (no K, no trusted compiled
-interfaces, a second checking pass).
-Nothing here has been translated to Rocq, Lean or Isabelle, so it is not
-Grade 2i, and no headless proof service is involved, so it is not Grade 1.
+Earlier receipts, kept with their lineage (§8.4):
 
-=== Why it stops at Grade 3
+[cols="1,1,3",options="header"]
+|===
+| Run, commit | State | Why
+
+| https://github.com/hyperpolymath/januskey/actions/runs/41687715055[41687715055], `fc188c4`
+| `superseded`
+| Canonical flags and all three modules; replaced by the run above at a later commit
+| https://github.com/hyperpolymath/januskey/actions/runs/40867211509[40867211509], `4afb710`
+| `superseded`
+| Before `--cubical-compatible` and before `Epistemic.agda`; it never covered E-1m
+|===
+
+That is a `PWG-3` receipt: the propositions type-check in Agda under the §2.1
+invocation, in CI, at a named commit, with the prover version pinned and the
+import cone recorded. Nothing here has been translated to Rocq or Lean, so no
+recheck leg counts and the grade is not `PWG-2i`; no witness in another
+foundation exists, so `foundation_diverse` is false.
 
-Grade 2i and above would require an Agda → Dedukti → Rocq/Lean transport or a
+=== Why it stops at PWG-3
+
+PWG-2i and above would require an Agda → Dedukti → Rocq/Lean transport or a
 re-proof, with the outcome recorded as `transported`, `re-proved` or
 `unavailable` (PROOF-POLICY §2). That work has not been done, is not claimed,
 and would not change what these modules prove: §2.2 is explicit that compiling
@@ -168,16 +197,12 @@ re-checks the sibling from source instead of trusting compiled interfaces;
 
 === Receipt bookkeeping for that change
 
-The CI receipt in the table above was produced **before** the flag changed.
-Changing a graded artefact's checker invalidates its receipt's exactness, so:
-
-* the local run above is recorded as **reproduction** — same prover version,
-  PyPI provenance instead of Debian, and no CI provenance at all (PROOF-POLICY
-  §2.3: receipts of execution come from CI);
-* the next `agda-proofs.yml` run on `main` is the new receipt, and this page
-  must cite it in place of the local run once it exists. Until then the rows
-  stay `AGDA-VERIFIED` on the strength of the four artefacts being unchanged
-  plus a matching local run, and that is the strongest claim available.
+The local run above is recorded as **reproduction** only: same prover version,
+PyPI provenance instead of Debian, and no CI provenance (PROOF-POLICY §2.3:
+receipts of execution come from CI). The CI receipt it was waiting for now
+exists: the table in §The PWG-3 receipt cites run 42076969251, which ran the
+canonical invocation on all three modules, and the receipts from before the
+flag changed are marked `superseded` there.
 
 One related inconsistency is an open obligation, not a claim: the Agda version
 is pinned twice in CI and the two pins differ — `agda-proofs.yml` installs
@@ -200,11 +225,11 @@ Idris2, are recorded in `docs/estate/environment-toolchains.md`.
 
 == Grades, ledger row by ledger row
 
-The 47 ledger rows fall into three classes under PROOF-POLICY §1. Counts are
-from `PROOF-NEEDS.adoc` at this commit and are `PROVEN` 12, `TESTED` 23,
-`ASSUMED` 4, `DESIGNED` 3, `OPEN` 5.
+The ledger rows fall into three classes under PROOF-POLICY §1. `PROOF-NEEDS.adoc`
+is the only place the rows are counted: an earlier revision of this page
+repeated the counts, and the two copies drifted apart.
 
-=== Grade 3 — theory, proved in Agda
+=== PWG-3 — theory, proved in Agda
 
 [cols="1,3,2",options="header"]
 |===
@@ -227,7 +252,7 @@ from `PROOF-NEEDS.adoc` at this commit and are `PROVEN` 12, `TESTED` 23,
   `obliterate-ignorance`, `rotate-forgets-old`
 |===
 
-These five are the only rows in this repository with a mathesis grade. Each
+These five are the only rows in this repository with a Proof Witness Grade (PWG). Each
 rests on a premise it names rather than assumes silently — the per-step
 cancellation law (`undoes`, TESTED as `execute_then_undo_is_identity`), the
 freshness of the transaction id (T-7, `ASSUMED`, probabilistic), the absence of
@@ -235,7 +260,7 @@ I/O, and, for E-1m, that the modelled channels are the only ones an attacker
 has (X-1). §6 asks for the axioms to be tracked; they are, in the modules'
 own "What is NOT claimed" blocks and in the ledger's T-6, T-7, G-2, X-1 rows.
 
-=== Engineering contracts — no mathesis grade applies
+=== Engineering contracts — no Proof Witness Grade applies
 
 Seven `PROVEN` rows are Idris2 theorems about this ABI: A-1, A-2, C-1, C-2,
 C-3, C-4, C-5, checked by
@@ -336,12 +361,12 @@ PROOF-POLICY §1 and the ABI belongs in Idris2.
 * Every grade names its receipt: commit, prover, prover version, flags,
   sibling pin. The receipt above is the only one of its kind here.
 * A receipt is invalidated by a change to a graded artefact, to its checker or
-  to its pin, and is then re-earned by the next run, not carried forward. The
-  blob comparison in §The Grade 3 receipt exists precisely to show which
-  changes do and do not invalidate it.
-* When a graded artefact is replaced, the grade is marked `Superseded`; when a
-  green receipt goes red and is not immediately fixed, `Regressed`. Neither is
-  deleted from the history.
-* `AGDA-PENDING` is the correct status for a module committed but not yet
-  checked. No row in this repository is in that state today: the four graded
-  rows are `AGDA-VERIFIED` at the commit above.
+  to its pin, and is then re-earned by the next run, not carried forward.
+* A receipt that is no longer current carries `state: superseded` (a newer
+  receipt replaced it) or `state: regressed` (the source no longer checks), with
+  the reason (PROOF-POLICY §8.4). These are receipt states, not status tokens,
+  and neither receipt is deleted from the history.
+* `AGDA-PENDING` is the correct correspondence state for a module committed but
+  not yet checked. No row in this repository is in that state today: the five
+  graded rows are `AGDA-VERIFIED` at the commit above, and their Rocq and Lean
+  legs are `unavailable`, so the grade is `PWG-3`.
diff --git a/scripts/check-agda.sh b/scripts/check-agda.sh
index 27862c0..2683b79 100755
--- a/scripts/check-agda.sh
+++ b/scripts/check-agda.sh
@@ -20,6 +20,25 @@ bash scripts/fetch-siblings.sh
 # them visible rather than silencing them with -WnoUnsupportedIndexedMatch.
 flags=(--safe --without-K --cubical-compatible --no-libraries --ignore-interfaces --double-check
        -i verification/proofs/agda -i _build/dependencies/resource-algebra/src)
+# PROOF-POLICY §8.4: a comment-aware postulate scan of the import cone (the
+# proofs and the pinned sibling), proved to work both ways on every run.
+bash scripts/scan-postulates.sh verification/proofs/agda _build/dependencies/resource-algebra/src
+# The controls are written at run time, so no file in the tree carries a real
+# postulate for another scanner to count.
+controls="$(mktemp -d)"
+trap 'rm -rf -- "$controls"' EXIT
+mkdir -p "$controls/comments-only" "$controls/planted"
+printf '%s\n' 'module CommentsOnly where' '-- postulate in a line comment' \
+  '{- postulate {- nested postulate -} postulate -}' 'x-postulate : Set₁' \
+  'x-postulate = Set' > "$controls/comments-only/CommentsOnly.agda"
+printf '%s\n' 'module Planted where' '{- c -} postulate X : Set' \
+  > "$controls/planted/Planted.agda"
+bash scripts/scan-postulates.sh "$controls/comments-only" >/dev/null \
+  || { echo "ERROR: postulate scan reported a postulate that is only in comments" >&2; exit 1; }
+if bash scripts/scan-postulates.sh "$controls/planted" >/dev/null; then
+  echo "ERROR: postulate scan missed the planted postulate" >&2; exit 1
+fi
+echo "[PASS] postulate scan: cone clean, both controls behave"
 for module in Reversibility TransactionAtomicity Epistemic; do
   "$prover" "${flags[@]}" "verification/proofs/agda/$module.agda"
 done
diff --git a/scripts/scan-postulates.sh b/scripts/scan-postulates.sh
new file mode 100644
index 0000000..1e4d77d
--- /dev/null
+++ b/scripts/scan-postulates.sh
@@ -0,0 +1,40 @@
+#!/usr/bin/env bash
+# SPDX-License-Identifier: MPL-2.0
+# SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell
+# Comment-aware postulate scan of an Agda import cone (PROOF-POLICY §8.4,
+# "Axioms travel with the grade"): --safe already refuses `postulate`, and this
+# scan is the second of the three parts that make the absence of axioms visible
+# on a receipt. Text inside nested {- -} comments and after a `--` line comment
+# is ignored; pragmas ({-# … #-}) are treated as code. A `--` that starts an
+# operator (`-->`) is not a comment, so the scan errs towards reporting.
+#
+# Usage: scan-postulates.sh DIR...   Prints each hit as path:line: text and the
+# count; exits 1 if there is any hit, 2 if no .agda file was found.
+set -euo pipefail
+[ "$#" -gt 0 ] || { echo "usage: $0 DIR..." >&2; exit 2; }
+mapfile -t files < <(find "$@" -name '*.agda' -type f | LC_ALL=C sort)
+[ "${#files[@]}" -gt 0 ] || { echo "ERROR: no .agda files under: $*" >&2; exit 2; }
+hits="$(awk '
+  FNR == 1 { depth = 0 }
+  {
+    line = $0; code = ""; i = 1; n = length(line)
+    while (i <= n) {
+      two = substr(line, i, 2)
+      if (depth == 0 && two == "{-" && substr(line, i + 2, 1) == "#") {
+        code = code "{-#"; i += 3; continue
+      }
+      if (two == "{-") { depth++; i += 2; continue }
+      if (depth > 0 && two == "-}") { depth--; i += 2; continue }
+      if (depth > 0) { i++; continue }
+      if (two == "--" && (i + 2 > n || substr(line, i + 2, 1) ~ /[ \t]/)) break
+      code = code substr(line, i, 1); i++
+    }
+    if (code ~ /(^|[^A-Za-z0-9_-])postulate([^A-Za-z0-9_-]|$)/)
+      printf "%s:%d: %s\n", FILENAME, FNR, line
+  }
+' "${files[@]}")"
+count=0
+[ -n "$hits" ] && count="$(printf '%s\n' "$hits" | wc -l | tr -d ' ')"
+[ -n "$hits" ] && printf '%s\n' "$hits"
+echo "postulate scan: ${#files[@]} files, $count postulate(s)"
+[ "$count" -eq 0 ]

From 77fcedbff8668b13efacfe7c9f74a0c84cc32c3a Mon Sep 17 00:00:00 2001
From: Claude <noreply@anthropic.com>
Date: Mon, 9 Nov 2026 13:18:25 +0000
Subject: [PATCH 2/5] proofs: scan the import cone Agda reports; mark the
 receipt pending re-run
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Review on #170 (Codex, CodeRabbit), each finding checked:

- The cone is now the module set `agda --dependency-graph` reports for the
  three roots, resolved to files on the include path and in Agda's own
  library; an unresolved module fails the gate. The directory scan both
  missed the 8 prover-supplied modules and swept in unimported ones.
- First-party modules (6) must have no postulate. Agda.Primitive's
  universe-level primitives (Level, lzero, lsuc, _⊔_, bound by BUILTIN)
  are reported as the prover's trusted base; a postulate in any other
  prover-supplied module fails.
- The scanner takes explicit files, refuses unreadable ones, and lexes
  `--` comments with no space, and string and character literals.
- Controls must exit exactly 0 and 1, and the planted one must be named.
- Run 42076969251 predates the changed gate, so it is recorded as the
  last receipt for the modules; the first green run of this gate on main
  replaces it.
- The stale "23 TESTED" is gone; Rust guidance names Creusot/Pearlite and
  Verus throughout.

Verified locally: gate OK (6 first-party, 0 postulates; 2 BUILTIN blocks
in Agda.Primitive); a never-reporting scanner, a comment-blind scanner and
a planted postulate in Epistemic.agda each fail the gate.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01GVPPsHYqVJSoPzdNYD9tRg
---
 PROOF-NEEDS.adoc              | 11 ++++--
 docs/theory/PROOF-GRADES.adoc | 63 ++++++++++++++++++++-----------
 scripts/check-agda.sh         | 71 ++++++++++++++++++++++++++---------
 scripts/scan-postulates.sh    | 50 ++++++++++++++++--------
 4 files changed, 135 insertions(+), 60 deletions(-)

diff --git a/PROOF-NEEDS.adoc b/PROOF-NEEDS.adoc
index d0d73b4..0172a0a 100644
--- a/PROOF-NEEDS.adoc
+++ b/PROOF-NEEDS.adoc
@@ -124,13 +124,16 @@ Of the 12 PROVEN rows, five are the theory rows — **G-1, T-1, T-2, T-3, E-1m**
 their artefact is Agda (`+verification/proofs/agda/+`). They are **`+PWG-3+`**
 (PROOF-POLICY §8, owner ruling 2026-11-04, which governs over the mathesis brief):
 each is `+PROVEN+` under the §2.1 invocation and no Rocq or Lean leg exists. The
-receipt is a green `+agda-proofs.yml+` run
+last receipt for the modules is a green `+agda-proofs.yml+` run
 (https://github.com/hyperpolymath/januskey/actions/runs/42076969251[42076969251])
 at commit `+23bc8c3+`, Agda 2.6.4.3, with `+resource-algebra+` pinned at
 `+cf9235c+`, running `+Reversibility+`, `+TransactionAtomicity+` and
-`+Epistemic+` under `+--safe --without-K --cubical-compatible+`. Its import cone,
-axioms (none) and the receipts it supersedes (runs 41687715055 at `+fc188c4+`
-and 40867211509 at `+4afb710+`) are recorded in
+`+Epistemic+` under `+--safe --without-K --cubical-compatible+`. The gate gained
+an import-cone postulate scan after it, so the first green run of the changed
+gate on `+main+` is the receipt that replaces it. The cone, the axioms (none in
+the development; the prover's universe-level primitives are reported) and the
+superseded receipts (runs 41687715055 at `+fc188c4+` and 40867211509 at
+`+4afb710+`) are recorded in
 link:docs/theory/PROOF-GRADES.adoc[`+docs/theory/PROOF-GRADES.adoc+`].
 Correspondence state for them: `+AGDA-VERIFIED+`.
 
diff --git a/docs/theory/PROOF-GRADES.adoc b/docs/theory/PROOF-GRADES.adoc
index 60e6367..a5d79ef 100644
--- a/docs/theory/PROOF-GRADES.adoc
+++ b/docs/theory/PROOF-GRADES.adoc
@@ -86,8 +86,15 @@ The theory artefacts are three Agda modules:
   (row E-1m, §The epistemic rewrite below).
 
 All three are checked by `scripts/check-agda.sh` (`just test-agda`), which is
-also the ledger's recorded checker for rows G-1, T-1, T-2, T-3 and E-1m. The
-current receipt (PROOF-POLICY §8.2, `PWG-3`):
+also the ledger's recorded checker for rows G-1, T-1, T-2, T-3 and E-1m.
+
+The gate changed in hyperpolymath/januskey#170: it now derives the import cone
+from Agda and scans it for postulates. A changed checker has to re-earn its
+receipt (§8.4), so the receipt below is the **last receipt for the three
+modules**, not yet a receipt for this gate. The first green `agda-proofs.yml` run
+on `main` after #170 is the receipt for the gate, and replaces this row, which
+then becomes `state: superseded`. Until then the grade is `PWG-3`, receipt
+pending re-run.
 
 [cols="1,3",options="header"]
 |===
@@ -95,7 +102,8 @@ current receipt (PROOF-POLICY §8.2, `PWG-3`):
 
 | Workflow, run | `agda-proofs.yml`, run
   https://github.com/hyperpolymath/januskey/actions/runs/42076969251[42076969251],
-  branch `main`, conclusion **success**, `state: current`
+  branch `main`, conclusion **success**; last receipt for the modules, before
+  the gate change above
 | Commit | `23bc8c38160a25c37917bce69cf05d91899b07e5` (started 2026-11-05T17:40:46Z)
 | Prover | `agda-bin=2.6.4.3-1+b2` on Debian trixie-slim
   (`@sha256:a29215f6…`), asserted by a passing step:
@@ -105,16 +113,23 @@ current receipt (PROOF-POLICY §8.2, `PWG-3`):
 | Flags | `--safe --without-K --cubical-compatible --no-libraries
   --ignore-interfaces --double-check`: the §2.1 canonical invocation, plus two
   stricter options
-| Import cone | roots `Reversibility`, `TransactionAtomicity`, `Epistemic`; the
-  cone is those modules and `resource-algebra` at
-  `cf9235c532712a783a404c359a1055f40134794a`, fetched by
+| Import cone | the module set Agda reports with `--dependency-graph` for the
+  roots `Reversibility`, `TransactionAtomicity` and `Epistemic`: 14 modules.
+  First-party (6): the three roots and `ResourceAlgebra.Prelude`,
+  `ResourceAlgebra.Core` and `ResourceAlgebra.Instances.Loss` from
+  `resource-algebra` at `cf9235c532712a783a404c359a1055f40134794a`, fetched by
   `scripts/fetch-siblings.sh` and re-checked from source under the same flags
-  (`--ignore-interfaces`); consumed by pin, not re-declared here
-| Axioms | none. `--safe` refuses `postulate`; postulate count 0. The
-  comment-aware scan of the cone (`scripts/scan-postulates.sh`, wired into the
-  gate with a positive and a negative control on every run) was added after this
-  run, so its first CI receipt is the next `agda-proofs.yml` run on `main`;
-  a local run at this receipt's sources reported 10 files, 0 postulates
+  (`--ignore-interfaces`). Supplied with the prover (8): `Agda.Primitive` and
+  `Agda.Builtin.{Bool,Equality,List,Maybe,Nat,Sigma,Unit}`
+| Axioms | none in the development. `--safe` refuses `postulate`, and the
+  comment-aware scan (`scripts/scan-postulates.sh`) finds 0 postulates in the
+  six first-party modules. The prover-supplied `Agda.Primitive` declares the
+  universe-level primitives (`Level`, `lzero`, `lsuc`, `_⊔_`) by two `postulate`
+  blocks, each bound by a `BUILTIN` pragma: they are the prover's trusted base,
+  not axioms of this development, and the gate reports them rather than hiding
+  them; a postulate in any other prover-supplied module fails it. The scan is
+  new in #170, so its first CI receipt is the run that replaces this row; the
+  figures here are from a local run at this receipt's sources
 | Result | The three modules type-check; the fixtures under
   `tests/reject-agda/` are refused *with the message each fixture names*, so a
   fixture that starts passing, or starts failing for the wrong reason, fails the
@@ -137,9 +152,10 @@ Earlier receipts, kept with their lineage (§8.4):
 | Before `--cubical-compatible` and before `Epistemic.agda`; it never covered E-1m
 |===
 
-That is a `PWG-3` receipt: the propositions type-check in Agda under the §2.1
-invocation, in CI, at a named commit, with the prover version pinned and the
-import cone recorded. Nothing here has been translated to Rocq or Lean, so no
+Those are the `PWG-3` facts: the propositions type-check in Agda under the
+§2.1 invocation, in CI, at a named commit, with the prover version pinned and
+the import cone recorded; the receipt is re-earned by the first run of the
+changed gate, as above. Nothing here has been translated to Rocq or Lean, so no
 recheck leg counts and the grade is not `PWG-2i`; no witness in another
 foundation exists, so `foundation_diverse` is false.
 
@@ -268,10 +284,10 @@ C-3, C-4, C-5, checked by
 are interface and wire-format contracts, so the theory ladder does not grade
 them — they are `PROVEN` in the ledger's own vocabulary and that is the whole
 of the claim. The `Rust/SPARK` shorthand is withdrawn; the mapping that
-replaces it is Rust → **Creusot**, Ada → SPARK, API/ABI → Idris2, theory →
-Agda.
+replaces it is Rust → **Creusot** with **Pearlite** contracts, and **Verus**
+(§1.2), Ada → SPARK, API/ABI → Idris2, theory → Agda.
 
-The same heading covers every `TESTED` row (23): a test proves behaviour was
+The same heading covers every `TESTED` row: a test proves behaviour was
 observed, never that it always holds. G-2 (the Idris2 ↔ Agda correspondence) is
 `ASSUMED` by transcription and would have to become mechanical before any
 "every operation is reversible" theorem could cite both halves.
@@ -291,10 +307,13 @@ observed, never that it always holds. G-2 (the Idris2 ↔ Agda correspondence) i
   this repository would record that as an external assumption with its source.
 
 | `TESTED` rows describing Rust behaviour (T-4, T-5, the property tests)
-| Claimed, tested. No Creusot annotation exists and Creusot is not installed in
-  the session that wrote this file.
-| Creusot contracts on the Rust functions, run in CI: PROOF-POLICY §1 sends
-  first-party Rust behaviour to Creusot, not to Idris2 and not to Agda.
+| Claimed, tested. No Creusot/Pearlite contract or Verus proof exists, and
+  neither verifier is installed in the session that wrote this file.
+| Contracts and proofs on the Rust functions, run in CI: PROOF-POLICY §1.2
+  plans first-party Rust for both Creusot (with Pearlite) and Verus, whose
+  scopes may differ; a property proved by one need not be duplicated in the
+  other, and where both cover it the correspondence is recorded. Not Idris2 and
+  not Agda.
 
 | T-6, T-7, X-1, G-2, E-1, G-3 (`ASSUMED` / `OPEN`)
 | Premises, external assumptions, or filed obligations.
diff --git a/scripts/check-agda.sh b/scripts/check-agda.sh
index 2683b79..33782af 100755
--- a/scripts/check-agda.sh
+++ b/scripts/check-agda.sh
@@ -20,28 +20,63 @@ bash scripts/fetch-siblings.sh
 # them visible rather than silencing them with -WnoUnsupportedIndexedMatch.
 flags=(--safe --without-K --cubical-compatible --no-libraries --ignore-interfaces --double-check
        -i verification/proofs/agda -i _build/dependencies/resource-algebra/src)
-# PROOF-POLICY §8.4: a comment-aware postulate scan of the import cone (the
-# proofs and the pinned sibling), proved to work both ways on every run.
-bash scripts/scan-postulates.sh verification/proofs/agda _build/dependencies/resource-algebra/src
+# The working directory for this run: the dependency graphs Agda writes and the
+# scan's controls. Removed on exit.
+work="$(mktemp -d)"
+trap 'rm -rf -- "$work"' EXIT
+modules=(Reversibility TransactionAtomicity Epistemic)
+for module in "${modules[@]}"; do
+  "$prover" "${flags[@]}" --dependency-graph="$work/$module.dot" "verification/proofs/agda/$module.agda"
+done
+
+# PROOF-POLICY §8.4: a comment-aware postulate scan of the import cone. The cone
+# is the module set Agda itself reports for the three roots (Agda.Primitive and
+# the Agda.Builtin modules included); each module is resolved to its source on
+# the include path or in Agda's own library, and an unresolved module fails.
+agda_prim="$("$prover" --print-agda-dir)/lib/prim"
+own=(); prover_lib=()
+while IFS= read -r name; do
+  found=""
+  for root in verification/proofs/agda _build/dependencies/resource-algebra/src "$agda_prim"; do
+    candidate="$root/${name//.//}.agda"
+    if [ -f "$candidate" ]; then found="$root"; break; fi
+  done
+  [ -n "$found" ] || { echo "ERROR: cannot resolve module $name of the import cone to a source file" >&2; exit 1; }
+  if [ "$found" = "$agda_prim" ]; then prover_lib+=("$candidate"); else own+=("$candidate"); fi
+done < <(sed -n 's/.*label="\([^"]*\)".*/\1/p' "$work"/*.dot | LC_ALL=C sort -u)
+[ "${#own[@]}" -gt 0 ] || { echo "ERROR: Agda reported no first-party module in the import cone" >&2; exit 1; }
+echo "import cone: ${#own[@]} first-party modules, ${#prover_lib[@]} supplied with the prover"
+# The proofs and the pinned sibling: no postulate at all.
+bash scripts/scan-postulates.sh "${own[@]}"
+# Modules supplied with the prover are its trusted base. The only postulates
+# allowed there are Agda.Primitive's universe-level primitives (Level, lzero,
+# lsuc, _⊔_, each bound by a BUILTIN pragma); they are reported, not hidden, and
+# a postulate in any other prover-supplied module of the cone fails the gate.
+if [ "${#prover_lib[@]}" -gt 0 ]; then
+  status=0; bash scripts/scan-postulates.sh "${prover_lib[@]}" >"$work/prover.log" 2>&1 || status=$?
+  [ "$status" -le 1 ] || { cat "$work/prover.log"; exit 1; }
+  if grep -E '^[^ ]+:[0-9]+: ' "$work/prover.log" | grep -vqF -- "/Agda/Primitive.agda:"; then
+    cat "$work/prover.log"; echo "ERROR: a postulate in a prover-supplied module other than Agda.Primitive" >&2; exit 1
+  fi
+  echo "prover-supplied: $(grep -cE '^[^ ]+:[0-9]+: ' "$work/prover.log" || true) postulate block(s), all in Agda.Primitive (universe-level primitives)"
+fi
+
 # The controls are written at run time, so no file in the tree carries a real
-# postulate for another scanner to count.
-controls="$(mktemp -d)"
-trap 'rm -rf -- "$controls"' EXIT
-mkdir -p "$controls/comments-only" "$controls/planted"
+# postulate for another scanner to count. Each must give exactly its exit code.
 printf '%s\n' 'module CommentsOnly where' '-- postulate in a line comment' \
-  '{- postulate {- nested postulate -} postulate -}' 'x-postulate : Set₁' \
-  'x-postulate = Set' > "$controls/comments-only/CommentsOnly.agda"
-printf '%s\n' 'module Planted where' '{- c -} postulate X : Set' \
-  > "$controls/planted/Planted.agda"
-bash scripts/scan-postulates.sh "$controls/comments-only" >/dev/null \
-  || { echo "ERROR: postulate scan reported a postulate that is only in comments" >&2; exit 1; }
-if bash scripts/scan-postulates.sh "$controls/planted" >/dev/null; then
-  echo "ERROR: postulate scan missed the planted postulate" >&2; exit 1
+  '--postulate with no space after the dashes' \
+  '{- postulate {- nested postulate -} postulate -}' \
+  'x--postulate : Set₁' 'x--postulate = Set' \
+  's : String' 's = "a postulate in a string \" still the string"' \
+  > "$work/CommentsOnly.agda"
+printf '%s\n' 'module Planted where' '{- c -} postulate X : Set' > "$work/Planted.agda"
+status=0; bash scripts/scan-postulates.sh "$work/CommentsOnly.agda" >"$work/neg.log" 2>&1 || status=$?
+[ "$status" -eq 0 ] || { cat "$work/neg.log"; echo "ERROR: the comments-only control did not exit 0 (got $status)" >&2; exit 1; }
+status=0; bash scripts/scan-postulates.sh "$work/Planted.agda" >"$work/pos.log" 2>&1 || status=$?
+if [ "$status" -ne 1 ] || ! grep -qF -- "Planted.agda:2:" "$work/pos.log"; then
+  cat "$work/pos.log"; echo "ERROR: the planted control did not exit 1 naming Planted.agda:2 (got $status)" >&2; exit 1
 fi
 echo "[PASS] postulate scan: cone clean, both controls behave"
-for module in Reversibility TransactionAtomicity Epistemic; do
-  "$prover" "${flags[@]}" "verification/proofs/agda/$module.agda"
-done
 mkdir -p _build/check-logs
 shopt -s nullglob
 rejects=(tests/reject-agda/*.agda)
diff --git a/scripts/scan-postulates.sh b/scripts/scan-postulates.sh
index 1e4d77d..8d06ff2 100644
--- a/scripts/scan-postulates.sh
+++ b/scripts/scan-postulates.sh
@@ -1,40 +1,58 @@
 #!/usr/bin/env bash
 # SPDX-License-Identifier: MPL-2.0
 # SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell
-# Comment-aware postulate scan of an Agda import cone (PROOF-POLICY §8.4,
+# Comment-aware postulate scan of Agda source files (PROOF-POLICY §8.4,
 # "Axioms travel with the grade"): --safe already refuses `postulate`, and this
 # scan is the second of the three parts that make the absence of axioms visible
-# on a receipt. Text inside nested {- -} comments and after a `--` line comment
-# is ignored; pragmas ({-# … #-}) are treated as code. A `--` that starts an
-# operator (`-->`) is not a comment, so the scan errs towards reporting.
+# on a receipt. check-agda.sh passes it the exact import cone that Agda itself
+# reports, so the files scanned are the files checked.
 #
-# Usage: scan-postulates.sh DIR...   Prints each hit as path:line: text and the
-# count; exits 1 if there is any hit, 2 if no .agda file was found.
+# Lexing follows Agda closely enough for one keyword: text inside nested
+# {- -} comments, after a `--` that starts a token (with or without a space
+# after it), and inside string or character literals is ignored; pragmas
+# ({-# … #-}) are code. A `--` inside a name such as `x--y` is part of the name.
+#
+# Usage: scan-postulates.sh FILE...   Prints each hit as path:line: text and the
+# count; exits 1 if there is any hit, 2 on a usage error or an unreadable file.
 set -euo pipefail
-[ "$#" -gt 0 ] || { echo "usage: $0 DIR..." >&2; exit 2; }
-mapfile -t files < <(find "$@" -name '*.agda' -type f | LC_ALL=C sort)
-[ "${#files[@]}" -gt 0 ] || { echo "ERROR: no .agda files under: $*" >&2; exit 2; }
+[ "$#" -gt 0 ] || { echo "usage: $0 FILE..." >&2; exit 2; }
+for f in "$@"; do
+  [ -f "$f" ] && [ -r "$f" ] || { echo "ERROR: not a readable file: $f" >&2; exit 2; }
+done
 hits="$(awk '
+  # Agda name characters are everything except whitespace and .;{}()@"
+  function namechar(c) { return c != "" && c !~ /[ \t.;{}()@"]/ }
   FNR == 1 { depth = 0 }
   {
     line = $0; code = ""; i = 1; n = length(line)
     while (i <= n) {
-      two = substr(line, i, 2)
+      c = substr(line, i, 1); two = substr(line, i, 2)
+      prev = (i > 1) ? substr(line, i - 1, 1) : ""
       if (depth == 0 && two == "{-" && substr(line, i + 2, 1) == "#") {
         code = code "{-#"; i += 3; continue
       }
       if (two == "{-") { depth++; i += 2; continue }
       if (depth > 0 && two == "-}") { depth--; i += 2; continue }
       if (depth > 0) { i++; continue }
-      if (two == "--" && (i + 2 > n || substr(line, i + 2, 1) ~ /[ \t]/)) break
-      code = code substr(line, i, 1); i++
+      if (c == "\"") {                     # string literal: skip to the closing quote
+        i++
+        while (i <= n && substr(line, i, 1) != "\"") i += (substr(line, i, 1) == "\\") ? 2 : 1
+        i++; code = code " "; continue
+      }
+      if (c == "'\''" && !namechar(prev)) { # character literal at a token start
+        i++
+        while (i <= n && substr(line, i, 1) != "'\''") i += (substr(line, i, 1) == "\\") ? 2 : 1
+        i++; code = code " "; continue
+      }
+      if (two == "--" && !namechar(prev)) break
+      code = code c; i++
     }
-    if (code ~ /(^|[^A-Za-z0-9_-])postulate([^A-Za-z0-9_-]|$)/)
+    if (code ~ /(^|[ \t.;{}()@])postulate([ \t.;{}()@]|$)/)
       printf "%s:%d: %s\n", FILENAME, FNR, line
   }
-' "${files[@]}")"
+' "$@")"
 count=0
 [ -n "$hits" ] && count="$(printf '%s\n' "$hits" | wc -l | tr -d ' ')"
 [ -n "$hits" ] && printf '%s\n' "$hits"
-echo "postulate scan: ${#files[@]} files, $count postulate(s)"
-[ "$count" -eq 0 ]
+echo "postulate scan: $# files, $count postulate(s)"
+[ "$count" -eq 0 ] || exit 1

From c728a8c8d2d321401283947060ebf913ad7d6c17 Mon Sep 17 00:00:00 2001
From: Claude <noreply@anthropic.com>
Date: Mon, 9 Nov 2026 13:39:04 +0000
Subject: [PATCH 3/5] proofs: Agda whitespace in the postulate scan; check
 Agda.Primitive by name
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

The scanner treated only space and tab as keyword boundaries, so a postulate
next to NO-BREAK SPACE, a Unicode space separator, CR, FF or VT went
unreported. Agda reads every isSpace character other than tab and newline as
a space (Agda.Syntax.Parser.Alex, toASCII); the scanner now does the same,
byte-wise in the C locale so mawk and gawk agree. The planted control gains a
NO-BREAK SPACE case, and the comments-only control `--postulate postulate`.

The prover-supplied allowance was the path Agda/Primitive.agda. The gate now
requires those blocks to declare exactly Level, lzero, lsuc and _⊔_, each with
its BUILTIN binding, so a prover pin that adds a postulate fails.

PROOF-NEEDS states the PWG-3 grade as pending its re-run receipt, and
PROOF-GRADES cites the green branch run of the changed gate as evidence.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01GVPPsHYqVJSoPzdNYD9tRg
---
 PROOF-NEEDS.adoc              | 10 +++++---
 docs/theory/PROOF-GRADES.adoc | 12 ++++++---
 scripts/check-agda.sh         | 46 +++++++++++++++++++++++++++--------
 scripts/scan-postulates.sh    | 17 ++++++++++---
 4 files changed, 63 insertions(+), 22 deletions(-)

diff --git a/PROOF-NEEDS.adoc b/PROOF-NEEDS.adoc
index 0172a0a..38a303a 100644
--- a/PROOF-NEEDS.adoc
+++ b/PROOF-NEEDS.adoc
@@ -121,8 +121,9 @@ and is kept for provenance only. Neither uses a confidence percentage and this
 repository does not publish one.
 
 Of the 12 PROVEN rows, five are the theory rows — **G-1, T-1, T-2, T-3, E-1m** — and
-their artefact is Agda (`+verification/proofs/agda/+`). They are **`+PWG-3+`**
-(PROOF-POLICY §8, owner ruling 2026-11-04, which governs over the mathesis brief):
+their artefact is Agda (`+verification/proofs/agda/+`). They are **`+PWG-3+`,
+receipt pending re-run** (PROOF-POLICY §8, owner ruling 2026-11-04, which
+governs over the mathesis brief):
 each is `+PROVEN+` under the §2.1 invocation and no Rocq or Lean leg exists. The
 last receipt for the modules is a green `+agda-proofs.yml+` run
 (https://github.com/hyperpolymath/januskey/actions/runs/42076969251[42076969251])
@@ -131,8 +132,9 @@ at commit `+23bc8c3+`, Agda 2.6.4.3, with `+resource-algebra+` pinned at
 `+Epistemic+` under `+--safe --without-K --cubical-compatible+`. The gate gained
 an import-cone postulate scan after it, so the first green run of the changed
 gate on `+main+` is the receipt that replaces it. The cone, the axioms (none in
-the development; the prover's universe-level primitives are reported) and the
-superseded receipts (runs 41687715055 at `+fc188c4+` and 40867211509 at
+the development; the prover's four universe-level primitives are checked by
+name and reported) and the superseded receipts (runs 41687715055 at
+`+fc188c4+` and 40867211509 at
 `+4afb710+`) are recorded in
 link:docs/theory/PROOF-GRADES.adoc[`+docs/theory/PROOF-GRADES.adoc+`].
 Correspondence state for them: `+AGDA-VERIFIED+`.
diff --git a/docs/theory/PROOF-GRADES.adoc b/docs/theory/PROOF-GRADES.adoc
index a5d79ef..c9039dc 100644
--- a/docs/theory/PROOF-GRADES.adoc
+++ b/docs/theory/PROOF-GRADES.adoc
@@ -126,10 +126,14 @@ pending re-run.
   six first-party modules. The prover-supplied `Agda.Primitive` declares the
   universe-level primitives (`Level`, `lzero`, `lsuc`, `_⊔_`) by two `postulate`
   blocks, each bound by a `BUILTIN` pragma: they are the prover's trusted base,
-  not axioms of this development, and the gate reports them rather than hiding
-  them; a postulate in any other prover-supplied module fails it. The scan is
-  new in #170, so its first CI receipt is the run that replaces this row; the
-  figures here are from a local run at this receipt's sources
+  not axioms of this development. The gate checks that those blocks declare
+  exactly those four names and that each has its `BUILTIN` binding, and fails on
+  any other prover-supplied postulate, so a prover pin that adds one does not
+  pass. The scan is new in #170, so its first receipt on `main` is the run that
+  replaces this row. The same figures came from the #170 branch in CI under
+  Agda 2.6.4.3 (run
+  https://github.com/hyperpolymath/januskey/actions/runs/42624327510[42624327510]
+  at `77fcedb`; branch evidence, not a receipt)
 | Result | The three modules type-check; the fixtures under
   `tests/reject-agda/` are refused *with the message each fixture names*, so a
   fixture that starts passing, or starts failing for the wrong reason, fails the
diff --git a/scripts/check-agda.sh b/scripts/check-agda.sh
index 33782af..2d98194 100755
--- a/scripts/check-agda.sh
+++ b/scripts/check-agda.sh
@@ -49,32 +49,58 @@ echo "import cone: ${#own[@]} first-party modules, ${#prover_lib[@]} supplied wi
 # The proofs and the pinned sibling: no postulate at all.
 bash scripts/scan-postulates.sh "${own[@]}"
 # Modules supplied with the prover are its trusted base. The only postulates
-# allowed there are Agda.Primitive's universe-level primitives (Level, lzero,
-# lsuc, _⊔_, each bound by a BUILTIN pragma); they are reported, not hidden, and
-# a postulate in any other prover-supplied module of the cone fails the gate.
+# allowed there are Agda.Primitive's universe-level primitives: exactly Level,
+# lzero, lsuc and _⊔_, each bound by its BUILTIN pragma. The gate checks the
+# declared names and the bindings, not the file name, so a prover pin that adds
+# a postulate to Agda.Primitive fails here; a postulate in any other
+# prover-supplied module of the cone fails too.
 if [ "${#prover_lib[@]}" -gt 0 ]; then
   status=0; bash scripts/scan-postulates.sh "${prover_lib[@]}" >"$work/prover.log" 2>&1 || status=$?
   [ "$status" -le 1 ] || { cat "$work/prover.log"; exit 1; }
-  if grep -E '^[^ ]+:[0-9]+: ' "$work/prover.log" | grep -vqF -- "/Agda/Primitive.agda:"; then
-    cat "$work/prover.log"; echo "ERROR: a postulate in a prover-supplied module other than Agda.Primitive" >&2; exit 1
+  grep -E '^[^ ]+:[0-9]+: ' "$work/prover.log" >"$work/prover.hits" || true
+  prim="$agda_prim/Agda/Primitive.agda"
+  # Every hit is in Agda.Primitive and is a bare `postulate` line opening a block,
+  # the only shape the name check below reads.
+  if grep -vqE -- "^$prim:[0-9]+: postulate[[:space:]]*\$" "$work/prover.hits"; then
+    cat "$work/prover.log"; echo "ERROR: a prover-supplied postulate outside the Agda.Primitive level blocks" >&2; exit 1
   fi
-  echo "prover-supplied: $(grep -cE '^[^ ]+:[0-9]+: ' "$work/prover.log" || true) postulate block(s), all in Agda.Primitive (universe-level primitives)"
+  # The names those blocks declare: the indented lines after `postulate`, up to the
+  # next line that is not indented; line comments removed.
+  declared="$(LC_ALL=C awk '
+    { sub(/--.*/, "") }
+    /^postulate[ \t]*$/ { inblock = 1; next }
+    inblock && /^[ \t]*$/ { next }
+    inblock && /^[ \t]/ { split($0, lhs, ":"); n = split(lhs[1], names, /[ \t]+/)
+                          for (k = 1; k <= n; k++) if (names[k] != "") print names[k]; next }
+    { inblock = 0 }
+  ' "$prim" | LC_ALL=C sort | tr '\n' ' ')"
+  expected="Level _⊔_ lsuc lzero "
+  [ "$declared" = "$expected" ] || {
+    echo "ERROR: Agda.Primitive postulates '$declared', expected exactly '$expected'" >&2; exit 1; }
+  for binding in "LEVEL Level" "LEVELZERO lzero" "LEVELSUC lsuc" "LEVELMAX _⊔_"; do
+    LC_ALL=C grep -qE -- "^\{-#[[:space:]]+BUILTIN[[:space:]]+${binding% *}[[:space:]]+${binding#* }[[:space:]]+#-\}" "$prim" || {
+      echo "ERROR: Agda.Primitive does not bind ${binding#* } with BUILTIN ${binding% *}" >&2; exit 1; }
+  done
+  echo "prover-supplied: Agda.Primitive postulates exactly ${expected% }, each bound by its BUILTIN pragma ($(wc -l <"$work/prover.hits" | tr -d ' ') block(s)); no other postulate"
 fi
 
 # The controls are written at run time, so no file in the tree carries a real
 # postulate for another scanner to count. Each must give exactly its exit code.
 printf '%s\n' 'module CommentsOnly where' '-- postulate in a line comment' \
-  '--postulate with no space after the dashes' \
+  '--postulate postulate: no space after the dashes' \
   '{- postulate {- nested postulate -} postulate -}' \
   'x--postulate : Set₁' 'x--postulate = Set' \
   's : String' 's = "a postulate in a string \" still the string"' \
   > "$work/CommentsOnly.agda"
-printf '%s\n' 'module Planted where' '{- c -} postulate X : Set' > "$work/Planted.agda"
+# Line 2: a postulate after a block comment. Line 3: one bounded by NO-BREAK
+# SPACE (U+00A0) on both sides, which Agda reads as whitespace.
+printf '%s\n' 'module Planted where' '{- c -} postulate X : Set' \
+  $'\302\240postulate\302\240Y : Set' > "$work/Planted.agda"
 status=0; bash scripts/scan-postulates.sh "$work/CommentsOnly.agda" >"$work/neg.log" 2>&1 || status=$?
 [ "$status" -eq 0 ] || { cat "$work/neg.log"; echo "ERROR: the comments-only control did not exit 0 (got $status)" >&2; exit 1; }
 status=0; bash scripts/scan-postulates.sh "$work/Planted.agda" >"$work/pos.log" 2>&1 || status=$?
-if [ "$status" -ne 1 ] || ! grep -qF -- "Planted.agda:2:" "$work/pos.log"; then
-  cat "$work/pos.log"; echo "ERROR: the planted control did not exit 1 naming Planted.agda:2 (got $status)" >&2; exit 1
+if [ "$status" -ne 1 ] || ! grep -qF -- "Planted.agda:2:" "$work/pos.log" || ! grep -qF -- "Planted.agda:3:" "$work/pos.log"; then
+  cat "$work/pos.log"; echo "ERROR: the planted control did not exit 1 naming Planted.agda:2 and :3 (got $status)" >&2; exit 1
 fi
 echo "[PASS] postulate scan: cone clean, both controls behave"
 mkdir -p _build/check-logs
diff --git a/scripts/scan-postulates.sh b/scripts/scan-postulates.sh
index 8d06ff2..59154cb 100644
--- a/scripts/scan-postulates.sh
+++ b/scripts/scan-postulates.sh
@@ -11,20 +11,29 @@
 # {- -} comments, after a `--` that starts a token (with or without a space
 # after it), and inside string or character literals is ignored; pragmas
 # ({-# … #-}) are code. A `--` inside a name such as `x--y` is part of the name.
+# Whitespace is Agda's: its lexer reads every character Haskell's isSpace accepts,
+# other than tab and newline, as a space (Agda.Syntax.Parser.Alex, toASCII), so
+# CR, FF, VT, NO-BREAK SPACE and the Unicode space separators (category Zs) are
+# turned into spaces before the line is lexed.
 #
 # Usage: scan-postulates.sh FILE...   Prints each hit as path:line: text and the
 # count; exits 1 if there is any hit, 2 on a usage error or an unreadable file.
 set -euo pipefail
 [ "$#" -gt 0 ] || { echo "usage: $0 FILE..." >&2; exit 2; }
 for f in "$@"; do
-  [ -f "$f" ] && [ -r "$f" ] || { echo "ERROR: not a readable file: $f" >&2; exit 2; }
+  [[ -f $f && -r $f ]] || { echo "ERROR: not a readable file: $f" >&2; exit 2; }
 done
-hits="$(awk '
+# The non-ASCII spaces as UTF-8 byte sequences: U+00A0, U+1680, U+2000-U+200A,
+# U+202F, U+205F, U+3000. awk runs in the C locale, so it matches bytes the same
+# way whichever awk is installed.
+ws="$(printf '\302\240|\341\232\200|\342\200[\200-\212]|\342\200\257|\342\201\237|\343\200\200')"
+hits="$(LC_ALL=C awk -v ws="$ws" '
   # Agda name characters are everything except whitespace and .;{}()@"
   function namechar(c) { return c != "" && c !~ /[ \t.;{}()@"]/ }
   FNR == 1 { depth = 0 }
   {
-    line = $0; code = ""; i = 1; n = length(line)
+    line = $0; gsub(/[\r\f\v]/, " ", line); gsub(ws, " ", line)
+    code = ""; i = 1; n = length(line)
     while (i <= n) {
       c = substr(line, i, 1); two = substr(line, i, 2)
       prev = (i > 1) ? substr(line, i - 1, 1) : ""
@@ -48,7 +57,7 @@ hits="$(awk '
       code = code c; i++
     }
     if (code ~ /(^|[ \t.;{}()@])postulate([ \t.;{}()@]|$)/)
-      printf "%s:%d: %s\n", FILENAME, FNR, line
+      printf "%s:%d: %s\n", FILENAME, FNR, $0
   }
 ' "$@")"
 count=0

From 9ff3043ac70cbd581e66aa990146d7db04052315 Mon Sep 17 00:00:00 2001
From: Claude <noreply@anthropic.com>
Date: Mon, 9 Nov 2026 13:49:31 +0000
Subject: [PATCH 4/5] proofs: comments separate tokens in the scan; skip pragma
 bodies as Agda does

A block comment was removed without leaving a token boundary, so
`postulate{- c -}X : Set`, which Agda reads as a postulate, became
`postulateX` and was not reported; in Agda.Primitive it would also have slipped
past the name check. A comment now leaves a space behind.

A pragma was scanned as code, so a FOREIGN payload using `postulate` as a
Haskell name failed the gate, and a payload holding `{- {-` opened a comment
Agda never sees, hiding a postulate after the pragma. Agda does not nest
comments inside a pragma and closes it at a `#-}` token (Lexer.x); the scan
now skips to the first `#-}`, which can end a pragma early but never late.

Controls: the comments-only file gains a FOREIGN payload; the planted file
gains the comment-separated and after-pragma cases, and must name lines 2-5.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01GVPPsHYqVJSoPzdNYD9tRg
---
 scripts/check-agda.sh      | 16 +++++++++++-----
 scripts/scan-postulates.sh | 20 +++++++++++++++-----
 2 files changed, 26 insertions(+), 10 deletions(-)

diff --git a/scripts/check-agda.sh b/scripts/check-agda.sh
index 2d98194..ee1e8b1 100755
--- a/scripts/check-agda.sh
+++ b/scripts/check-agda.sh
@@ -91,16 +91,22 @@ printf '%s\n' 'module CommentsOnly where' '-- postulate in a line comment' \
   '{- postulate {- nested postulate -} postulate -}' \
   'x--postulate : Set₁' 'x--postulate = Set' \
   's : String' 's = "a postulate in a string \" still the string"' \
+  '{-# FOREIGN GHC postulate = () #-}' \
   > "$work/CommentsOnly.agda"
-# Line 2: a postulate after a block comment. Line 3: one bounded by NO-BREAK
-# SPACE (U+00A0) on both sides, which Agda reads as whitespace.
+# One planted postulate per line, 2 to 5: after a block comment; bounded by
+# NO-BREAK SPACE (U+00A0), which Agda reads as whitespace; separated from its
+# name by a block comment; after a pragma whose payload holds `{- {-`, which Agda
+# does not read as a comment there.
 printf '%s\n' 'module Planted where' '{- c -} postulate X : Set' \
-  $'\302\240postulate\302\240Y : Set' > "$work/Planted.agda"
+  $'\302\240postulate\302\240Y : Set' 'postulate{- c -}Z : Set' \
+  '{-# FOREIGN GHC {- {- #-} postulate W : Set' > "$work/Planted.agda"
 status=0; bash scripts/scan-postulates.sh "$work/CommentsOnly.agda" >"$work/neg.log" 2>&1 || status=$?
 [ "$status" -eq 0 ] || { cat "$work/neg.log"; echo "ERROR: the comments-only control did not exit 0 (got $status)" >&2; exit 1; }
 status=0; bash scripts/scan-postulates.sh "$work/Planted.agda" >"$work/pos.log" 2>&1 || status=$?
-if [ "$status" -ne 1 ] || ! grep -qF -- "Planted.agda:2:" "$work/pos.log" || ! grep -qF -- "Planted.agda:3:" "$work/pos.log"; then
-  cat "$work/pos.log"; echo "ERROR: the planted control did not exit 1 naming Planted.agda:2 and :3 (got $status)" >&2; exit 1
+missed=""
+for line in 2 3 4 5; do grep -qF -- "Planted.agda:$line:" "$work/pos.log" || missed="$missed $line"; done
+if [ "$status" -ne 1 ] || [ -n "$missed" ]; then
+  cat "$work/pos.log"; echo "ERROR: the planted control did not exit 1 naming lines 2-5 (got $status; missed:${missed:- none})" >&2; exit 1
 fi
 echo "[PASS] postulate scan: cone clean, both controls behave"
 mkdir -p _build/check-logs
diff --git a/scripts/scan-postulates.sh b/scripts/scan-postulates.sh
index 59154cb..d20faeb 100644
--- a/scripts/scan-postulates.sh
+++ b/scripts/scan-postulates.sh
@@ -9,8 +9,14 @@
 #
 # Lexing follows Agda closely enough for one keyword: text inside nested
 # {- -} comments, after a `--` that starts a token (with or without a space
-# after it), and inside string or character literals is ignored; pragmas
-# ({-# … #-}) are code. A `--` inside a name such as `x--y` is part of the name.
+# after it), and inside string or character literals is ignored. A `--` inside
+# a name such as `x--y` is part of the name. A comment separates tokens, as it
+# does for Agda, so `postulate{- c -}X` is a postulate.
+# A pragma ({-# … #-}) is skipped to the first `#-}`: its contents are pragma
+# tokens or, for FOREIGN and COMPILE, another language's text, never an Agda
+# declaration, and Agda does not nest comments inside it (Lexer.x). Agda closes
+# a pragma at a `#-}` token, never before the first `#-}` in the text, so this
+# rule can end a pragma early (an extra report) but never late (a missed one).
 # Whitespace is Agda's: its lexer reads every character Haskell's isSpace accepts,
 # other than tab and newline, as a space (Agda.Syntax.Parser.Alex, toASCII), so
 # CR, FF, VT, NO-BREAK SPACE and the Unicode space separators (category Zs) are
@@ -30,17 +36,21 @@ ws="$(printf '\302\240|\341\232\200|\342\200[\200-\212]|\342\200\257|\342\201\23
 hits="$(LC_ALL=C awk -v ws="$ws" '
   # Agda name characters are everything except whitespace and .;{}()@"
   function namechar(c) { return c != "" && c !~ /[ \t.;{}()@"]/ }
-  FNR == 1 { depth = 0 }
+  FNR == 1 { depth = 0; pragma = 0 }
   {
     line = $0; gsub(/[\r\f\v]/, " ", line); gsub(ws, " ", line)
     code = ""; i = 1; n = length(line)
     while (i <= n) {
       c = substr(line, i, 1); two = substr(line, i, 2)
       prev = (i > 1) ? substr(line, i - 1, 1) : ""
+      if (pragma) {                        # inside {-# … #-}: skip to the first #-}
+        if (substr(line, i, 3) == "#-}") { pragma = 0; i += 3; code = code " " } else i++
+        continue
+      }
       if (depth == 0 && two == "{-" && substr(line, i + 2, 1) == "#") {
-        code = code "{-#"; i += 3; continue
+        pragma = 1; i += 3; code = code " "; continue
       }
-      if (two == "{-") { depth++; i += 2; continue }
+      if (two == "{-") { if (depth == 0) code = code " "; depth++; i += 2; continue }
       if (depth > 0 && two == "-}") { depth--; i += 2; continue }
       if (depth > 0) { i++; continue }
       if (c == "\"") {                     # string literal: skip to the closing quote

From 814768b3de25f8323dddec15cf165584946cb81f Mon Sep 17 00:00:00 2001
From: Claude <noreply@anthropic.com>
Date: Mon, 9 Nov 2026 14:50:29 +0000
Subject: [PATCH 5/5] proofs: a token may start after a skipped literal in the
 postulate scan
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

The scanner decided whether `--` or `'` starts a token from the raw
character before it, so in `c = 'x'-- postulate …` the closing quote of
the character literal counted as a name character, the line comment was
not recognised, and a postulate that Agda never sees failed the gate.
It now uses the last character emitted as code: a skipped literal,
comment or pragma leaves a space, as it leaves a token boundary in Agda.
The comments-only control carries the case.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01GVPPsHYqVJSoPzdNYD9tRg
---
 scripts/check-agda.sh      | 2 +-
 scripts/scan-postulates.sh | 4 +++-
 2 files changed, 4 insertions(+), 2 deletions(-)

diff --git a/scripts/check-agda.sh b/scripts/check-agda.sh
index ee1e8b1..98cbc27 100755
--- a/scripts/check-agda.sh
+++ b/scripts/check-agda.sh
@@ -91,7 +91,7 @@ printf '%s\n' 'module CommentsOnly where' '-- postulate in a line comment' \
   '{- postulate {- nested postulate -} postulate -}' \
   'x--postulate : Set₁' 'x--postulate = Set' \
   's : String' 's = "a postulate in a string \" still the string"' \
-  '{-# FOREIGN GHC postulate = () #-}' \
+  '{-# FOREIGN GHC postulate = () #-}' "c = 'x'-- postulate after a character literal" \
   > "$work/CommentsOnly.agda"
 # One planted postulate per line, 2 to 5: after a block comment; bounded by
 # NO-BREAK SPACE (U+00A0), which Agda reads as whitespace; separated from its
diff --git a/scripts/scan-postulates.sh b/scripts/scan-postulates.sh
index d20faeb..5514757 100644
--- a/scripts/scan-postulates.sh
+++ b/scripts/scan-postulates.sh
@@ -42,7 +42,9 @@ hits="$(LC_ALL=C awk -v ws="$ws" '
     code = ""; i = 1; n = length(line)
     while (i <= n) {
       c = substr(line, i, 1); two = substr(line, i, 2)
-      prev = (i > 1) ? substr(line, i - 1, 1) : ""
+      # The last character emitted as code, not the raw one before i: a skipped
+      # literal, comment or pragma leaves a space, so a token may start after it.
+      prev = (code == "") ? "" : substr(code, length(code), 1)
       if (pragma) {                        # inside {-# … #-}: skip to the first #-}
         if (substr(line, i, 3) == "#-}") { pragma = 0; i += 3; code = code " " } else i++
         continue