ci(proofs): run the Agda core in CI under the PROOF-POLICY §2.1 invocation

.github/workflows/proofs.yml

@@ -1,4 +1,4 @@
 # SPDX-License-Identifier: MPL-2.0
 # SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath)
 #
 # proofs.yml — the R0-B / R1 proof rungs that cannot run in the authoring
@@ -13,6 +13,8 @@
 #   stackcert — Lean 4, toolchain pinned by src/stackcert/lean-toolchain.
 #               `bash tests/run_stackcert.sh` = core `#print axioms cert_sound`
 #               + `lake build` + positive fixture + four negative controls.
+#   agda      — the core Agda proofs (R-1..R-6) and expected rejections,
+#               `bash scripts/check-agda.sh` on Agda 2.6.4.3.
 #   occ-idris — Idris 2 v0.7.0 built from source over Chez Scheme.
 #               `bash src/occ/check-rejections.sh` = the accepts compile and
 #               the four expected-rejection controls are rejected.
@@ -21,19 +23,35 @@
 # because this repository's Actions allow-list posture is under investigation
 # (issue #6) and a step referencing a non-allow-listed action dies at startup
 # with jobs=0 — a gate that cannot start must not be trusted to say "green".
-name: Proofs (R0-B Occ, R1 stackcert)
+name: Proofs (Agda core, R0-B Occ, R1 stackcert)
 
 on:
   workflow_dispatch:
   push:
     branches: [main, master]
     paths:
+      - 'src/OccupancyTypes/**'
+      - 'tests/reject/**'
+      - 'scripts/check-agda.sh'
+      - 'scripts/scan-postulates.pl'
+      - 'tests/scan_postulates_test.sh'
+      - 'tests/check_agda_find_failure_test.sh'
+      - 'scripts/fetch-siblings.sh'
+      - 'occupancy-types.agda-lib'
       - 'src/stackcert/**'
       - 'src/occ/**'
       - 'tests/run_stackcert.sh'
       - '.github/workflows/proofs.yml'
   pull_request:
     paths:
+      - 'src/OccupancyTypes/**'
+      - 'tests/reject/**'
+      - 'scripts/check-agda.sh'
+      - 'scripts/scan-postulates.pl'
+      - 'tests/scan_postulates_test.sh'
+      - 'tests/check_agda_find_failure_test.sh'
+      - 'scripts/fetch-siblings.sh'
+      - 'occupancy-types.agda-lib'
       - 'src/stackcert/**'
       - 'src/occ/**'
       - 'tests/run_stackcert.sh'
@@ -48,6 +66,32 @@
   contents: read
 
 jobs:
+  agda:
+    name: Agda core proofs and expected rejections
+    # The reclamation law (R-1..R-6) had no CI here: typed-wasm's kernel
+    # gate was the only runner. Same prover as resource-algebra's proofs.yml:
+    # the Debian agda-bin package at the pinned version, under the
+    # PROOF-POLICY §2.1 invocation in scripts/check-agda.sh.
+    runs-on: ubuntu-latest
+    container: debian:trixie-slim
+    timeout-minutes: 30
+    steps:
+      - name: Install the pinned prover
+        run: |
+          apt-get update
+          apt-get install --no-install-recommends -y ca-certificates git agda-bin=2.6.4.3-1+b2
+      - uses: actions/checkout@v7.0.1
+        with:
+          persist-credentials: false
+      - name: Verify the checked Agda version
+        run: test "$(agda --version)" = 'Agda version 2.6.4.3'
+      - name: Postulate scanner tests
+        run: bash tests/scan_postulates_test.sh
+      - name: Gate stops when find cannot list the import cone
+        run: bash tests/check_agda_find_failure_test.sh
+      - name: Core proofs and expected rejections (fetches resource-algebra at its pin)
+        run: bash scripts/check-agda.sh
+
   stackcert:
     name: R1 stackcert (Lean 4)
     runs-on: ubuntu-latest
@@ -57,7 +101,7 @@
       - name: Install elan (toolchain resolves from src/stackcert/lean-toolchain)
         run: |
           set -euo pipefail
           curl -sSfL https://elan.lean-lang.org/elan-init.sh | sh -s -- -y --default-toolchain none
           echo "$HOME/.elan/bin" >> "$GITHUB_PATH"
       - name: Run the stackcert harness (core + build + fixture + 4 controls)
         run: |

PROOF-STATUS.adoc

@@ -1,9 +1,12 @@
 // SPDX-License-Identifier: CC-BY-SA-4.0
 = occupancy-types — Proof Status
-:revdate: 2026-10-12
+:revdate: 2026-11-09
 
-Statuses: PROVEN / TESTED / ASSUMED / DESIGNED / OPEN. All modules are
-`--safe --without-K --no-libraries`, `--double-check`, no postulates.
+Statuses are the closed vocabulary of PROOF-POLICY §5 (`metadatastician/standards`
+`3-practice/PROOF-POLICY.adoc`): PROVEN / PROVEN-WITH-AXIOMS / TESTED / ASSUMED /
+OPEN. Every module checks under the §2.1 invocation,
+`--safe --without-K --cubical-compatible`, with `--no-libraries
+--ignore-interfaces --double-check` (`scripts/check-agda.sh`); no postulates.
 Sibling: resource-algebra (same kernel), pinned in `scripts/fetch-siblings.sh`.
 
 == The occupancy algebra
@@ -12,7 +15,7 @@ Sibling: resource-algebra (same kernel), pinned in `scripts/fetch-siblings.sh`.
 |===
 | ID | Claim | Status
 | O-1 | The high-water-mark algebra (peak, drift, drift ≤ peak; sequence = `max (peak a) (drift a + peak b)`) is a resource algebra and a dioid; it has no annihilating zero | PROVEN in resource-algebra (`Instances/HWM.agda`); this repo adopts it as its occupancy algebra
-| O-2 | It is this repo's own R2–R3 definition | DESIGNED — adopted today from the resource-algebra proposal; the operational model's "live bytes" reading is its intended semantics; a signed drift (terms that consume more than they allocate) is the first extension
+| O-2 | It is this repo's own R2–R3 definition | ASSUMED — a definition this repo adopts (`Reclaim.agda` and `Witness.agda` import `Instances.HWM`), not a theorem. That the operational model's "live bytes" reading is its semantics is the v0 → typed bridge, OPEN (see Open); a signed drift (terms that consume more than they allocate) is the first extension
 |===
 
 == Reclamation at a cut (Reclaim.agda)
@@ -25,7 +28,7 @@ Sibling: resource-algebra (same kernel), pinned in `scripts/fetch-siblings.sh`.
 | R-3 | *Occupancy ≤ cost*: `peak (xs ++ ys) ≤ peak xs + peak ys` | PROVEN (`occupancy≤cost`, `protocol-occupancy≤cost`)
 | R-4 | Equality iff nothing is reclaimed: with drift = peak the occupancy is the cost (`no-reclaim`); with drift < peak and a non-trivial suffix it is strictly less (`reclaimed`) | PROVEN
 | R-5 | Two readings of one protocol: occupancy 4, cost 7 (`Witness`) | PROVEN
-| R-6 | Reading occupancy as cost, or drift as peak, is refused (`CostIsOccupancy`, `DriftIsPeak`) | PROVEN
+| R-6 | Reading occupancy as cost, or drift as peak, is refused (`CostIsOccupancy`, `DriftIsPeak`) | TESTED (`tests/reject/`: each is refused at its invalid declaration by `scripts/check-agda.sh`)
 |===
 
 == Separation from siblings (criterion 2 of the family bar)
@@ -52,4 +55,34 @@ threads (choreographic-types A-3), occupancy has two theorems of its own.
   typed bridge).
 * TYPE-CONNECTIONS registration (rows supplied in resource-algebra's
   cross-repo notes).
-* CI: DESIGNED until first green run on the pinned prover.
+* CI: `proofs.yml` job `agda` runs `scripts/check-agda.sh` on Agda 2.6.4.3
+  (added 2026-11-09). Before, only typed-wasm's kernel gate checked these
+  proofs, at typed-wasm's pin and Agda 2.6.3.
+
+== Proof Witness Grades (PROOF-POLICY §8)
+
+R-1 to R-5 are *theory* (PROOF-POLICY §1): Agda is the source, and §2 owes
+a Rocq recheck and a Lean recheck for each. R-6 is a refusal (TESTED), not
+a theorem, and is not graded.
+
+* *Agda leg.* Route: source. Invocation: `scripts/check-agda.sh`, i.e.
+  `agda --safe --without-K --cubical-compatible --no-libraries
+  --ignore-interfaces --double-check -i src -i <resource-algebra>/src`, on
+  Agda 2.6.4.3 (`proofs.yml`, job `agda`). No standard library. Import cone:
+  `src/OccupancyTypes/` and resource-algebra's `src/` at the commit
+  `scripts/fetch-siblings.sh` pins. Axioms (§8.4.6): `--safe` refuses
+  `postulate`, and `scripts/check-agda.sh` also scans the cone for
+  `postulate` outside comments, so the postulate count is 0. The receipt is
+  the `proofs.yml` run on the commit in question.
+* *Rocq leg.* OPEN for R-1 to R-5: not started.
+* *Lean leg.* OPEN for R-1 to R-5: not started. The Lean files here
+  (`src/stackcert/`, `verification/proofs/lean4/CostStateSeparation.lean`)
+  state other theorems (R1 stackcert, the W2.2 separation); none is a
+  restatement of R-1 to R-5, so none is their Lean leg (§3).
+
+Grade, derived as §8.4 requires: R-1 to R-5 are `PWG-3` at a commit whose
+`proofs.yml` job `agda` passed, and `ungraded` at any commit without that
+receipt. Checks before 2026-11-09 used `--safe --without-K` without
+`--cubical-compatible`, and ran only in typed-wasm; §2.1 counts them as
+historical evidence. None is `PWG-2i` or better, and none is
+`+foundation-diverse`.

occupancy-types.agda-lib

@@ -1,4 +1,4 @@
 name: occupancy-types
 include: src
 depend: resource-algebra
-flags: --safe --without-K
+flags: --safe --without-K --cubical-compatible

scripts/check-agda.sh

@@ -11,7 +11,24 @@ if [ -z "${RESOURCE_ALGEBRA_SRC:-}" ]; then
   bash scripts/fetch-siblings.sh
 fi
 test -d "$ra" || { echo "ERROR: resource-algebra sources not found at $ra" >&2; exit 1; }
-flags=(--safe --without-K --no-libraries --ignore-interfaces --double-check -i src -i "$ra")
+flags=(--safe --without-K --cubical-compatible --no-libraries --ignore-interfaces --double-check -i src -i "$ra")
+# PROOF-POLICY §8.4.6: a comment-aware postulate scan of the import cone
+# (src/ and the pinned resource-algebra sources), alongside --safe.
+# scripts/scan-postulates.pl reads each file in source order (nested block
+# comments, line comments, strings) and fails on a file it cannot read.
+# find runs to a file, not a process substitution, so its own failure (a
+# directory it cannot read) stops the gate instead of leaving a partial cone.
+cone_list="$(mktemp)"
+trap 'rm -f "$cone_list"' EXIT
+find src "$ra" -name '*.agda' -print0 > "$cone_list" \
+  || { echo "ERROR: could not list the import cone (src/, $ra)" >&2; exit 1; }
+mapfile -d '' cone < "$cone_list"
+(( ${#cone[@]} > 0 )) || { echo "ERROR: no Agda sources in the import cone" >&2; exit 1; }
+if ! perl scripts/scan-postulates.pl "${cone[@]}"; then
+  echo "ERROR: postulate in the import cone (src/, $ra), or an unreadable file" >&2
+  exit 1
+fi
+echo "PASS: no postulate in the import cone (src/, resource-algebra)"
 "$prover" "${flags[@]}" src/OccupancyTypes/All.agda
 mkdir -p _build/check-logs
 shopt -s nullglob

scripts/check-proofs.sh

@@ -82,7 +82,7 @@ check_one() {
   case "$PROVER" in
     idris2) out="$(cd "$ROOT/$root" && idris2 --check "$rel" 2>&1)"; rc=$? ;;
     lean4)  out="$(cd "$ROOT/$root" && lean          "$rel" 2>&1)"; rc=$? ;;
-    agda)   out="$(cd "$ROOT/$root" && agda --safe    "$rel" 2>&1)"; rc=$? ;;
+    agda)   out="$(cd "$ROOT/$root" && agda --safe --without-K --cubical-compatible "$rel" 2>&1)"; rc=$? ;;
     coq)    out="$(cd "$ROOT/$root" && coqc           "$rel" 2>&1)"; rc=$? ;;
   esac
   set -e

scripts/scan-postulates.pl

@@ -0,0 +1,69 @@
+#!/usr/bin/env perl
+# SPDX-License-Identifier: MPL-2.0
+# scan-postulates.pl FILE...   (PROOF-POLICY §8.4.6)
+#
+# Reports every `postulate` in Agda code, reading each file in source order
+# so a comment cannot hide code: `--` comments run to the end of the line,
+# `{- -}` comments nest, string and character literals are skipped. A
+# `{-` inside a line comment opens nothing, and a `-}` inside a string
+# closes nothing.
+#
+# Exit 0: no postulate. Exit 1: at least one (each printed). Exit 2: a file
+# could not be read, or no file was given. A scan that could not read its
+# input must never pass.
+use strict;
+use warnings;
+
+@ARGV or do { print STDERR "scan-postulates: no files given\n"; exit 2 };
+my $found = 0;
+for my $file (@ARGV) {
+  open(my $fh, '<:raw', $file)
+    or do { print STDERR "scan-postulates: cannot read $file: $!\n"; exit 2 };
+  my $src = do { local $/; <$fh> };
+  defined $src
+    or do { print STDERR "scan-postulates: cannot read $file: $!\n"; exit 2 };
+  close $fh;
+  my ($i, $n, $depth, $line, $code) = (0, length $src, 0, 1, '');
+  while ($i < $n) {
+    my $two = substr($src, $i, 2);
+    my $c = substr($src, $i, 1);
+    $line++ if $c eq "\n";
+    if ($two eq '{-') { $depth++; $i += 2; next }
+    if ($depth > 0) {
+      if ($two eq '-}') { $depth--; $i += 2 } else { $i++ }
+      $code .= "\n" if $c eq "\n";
+      next;
+    }
+    if ($two eq '--') {
+      my $eol = index($src, "\n", $i);
+      $i = $eol < 0 ? $n : $eol;
+      next;
+    }
+    if ($c eq "'" && $i + 2 < $n && substr($src, $i + 2, 1) eq "'") {
+      $code .= ' '; $i += 3; next;       # a character literal such as '"'
+    }
+    if ($c eq '"') {
+      $i++;
+      while ($i < $n) {
+        my $d = substr($src, $i, 1);
+        if ($d eq '\\') { $i += 2; next }
+        $i++;
+        last if $d eq '"';
+        $code .= "\n" if $d eq "\n";
+      }
+      $code .= ' ';
+      next;
+    }
+    $code .= $c;
+    $i++;
+  }
+  my $ln = 1;
+  for my $text (split /\n/, $code, -1) {
+    if ($text =~ /(?<![\w'])postulate(?![\w'])/) {
+      print "$file:$ln: postulate\n";
+      $found = 1;
+    }
+    $ln++;
+  }
+}
+exit $found;

tests/check_agda_find_failure_test.sh

@@ -0,0 +1,29 @@
+#!/usr/bin/env bash
+# SPDX-License-Identifier: MPL-2.0
+# scripts/check-agda.sh must stop when find cannot list the import cone.
+# A stub find on PATH prints one real file of the cone and exits non-zero,
+# as find does when it meets a directory it cannot read; CI can do this even
+# as root. The gate must exit non-zero and must not report the postulate
+# scan as passed. Before the fix, the scan passed on the partial list.
+set -uo pipefail
+cd -- "$(dirname -- "${BASH_SOURCE[0]}")/.."
+stub=$(mktemp -d); trap 'rm -rf "$stub"' EXIT
+cat > "$stub/find" <<'FAKE_FIND'
+#!/usr/bin/env bash
+printf 'src/OccupancyTypes/All.agda\0'
+echo "find: 'src/locked': Permission denied" >&2
+exit 1
+FAKE_FIND
+chmod +x "$stub/find"
+# Point at an existing directory so the gate does not fetch the sibling.
+export RESOURCE_ALGEBRA_SRC="$PWD/src"
+out=$(PATH="$stub:$PATH" bash scripts/check-agda.sh 2>&1); rc=$?
+if [[ $rc -eq 0 ]] || grep -q 'PASS: no postulate' <<<"$out"; then
+  printf 'FAIL: gate passed although find failed (exit %s)\n%s\n' "$rc" "$out" >&2
+  exit 1
+fi
+if ! grep -q 'could not list the import cone' <<<"$out"; then
+  printf 'FAIL: gate stopped for another reason (exit %s)\n%s\n' "$rc" "$out" >&2
+  exit 1
+fi
+echo "PASS: a find failure stops the gate (exit $rc) before the postulate scan passes"

tests/scan_postulates_test.sh

@@ -0,0 +1,28 @@
+#!/usr/bin/env bash
+# SPDX-License-Identifier: MPL-2.0
+# scripts/scan-postulates.pl reads Agda in source order: a comment cannot
+# hide code, a string cannot fake a comment, and an unreadable input fails.
+set -uo pipefail
+cd -- "$(dirname -- "${BASH_SOURCE[0]}")/.."
+scan=scripts/scan-postulates.pl
+d=$(mktemp -d); trap 'rm -rf "$d"' EXIT
+fail=0
+check() { # check WANT-EXIT NAME CONTENT
+  printf '%b' "$3" > "$d/$2"
+  perl "$scan" "$d/$2" >/dev/null 2>&1; got=$?
+  if [[ "$got" -eq "$1" ]]; then echo "PASS: $2 -> $got"; else echo "FAIL: $2 -> $got, want $1"; fail=1; fi
+}
+check 0 clean.agda        'module A where\nx = 1\n'
+check 1 real.agda         'module B where\npostulate p : Set\n'
+check 1 linehide.agda     'module C where\n-- {-\npostulate p : Set\n-- -}\n'
+check 0 nested.agda       'module D where\n{- {- -} postulate -}\n'
+check 0 string.agda       'module E where\ns = "postulate -} {-"\n'
+check 0 comment.agda      'module F where\n{-# OPTIONS --safe #-}\n-- postulate\n'
+check 0 charlit.agda      "module G where\nc = '\"'\n-- \"\nx = 1\n"
+mkdir -p "$d/with space"
+check 1 'with space/s.agda' 'postulate q : Set\n'
+perl "$scan" "$d/missing.agda" >/dev/null 2>&1; got=$?
+if [[ "$got" -eq 2 ]]; then echo "PASS: unreadable file -> 2"; else echo "FAIL: unreadable file -> $got, want 2"; fail=1; fi
+perl "$scan" >/dev/null 2>&1; got=$?
+if [[ "$got" -eq 2 ]]; then echo "PASS: no files -> 2"; else echo "FAIL: no files -> $got, want 2"; fail=1; fi
+exit $fail