fix(proofs): fail the proof gate on Admitted, sorry and postulate (WO 1.3)

.github/workflows/agda-proof-policy.yml

@@ -6,12 +6,16 @@ on:
   pull_request:
     paths:
       - 'scripts/check-proofs.sh'
+      - 'scripts/scan-postulates.sh'
+      - 'tests/proofs/**'
       - 'verification/proofs/agda/**'
       - '.github/workflows/agda-proof-policy.yml'
   push:
     branches: [main]
     paths:
       - 'scripts/check-proofs.sh'
+      - 'scripts/scan-postulates.sh'
+      - 'tests/proofs/**'
       - 'verification/proofs/agda/**'
       - '.github/workflows/agda-proof-policy.yml'
   workflow_dispatch:
@@ -58,3 +62,6 @@ jobs:
 
       - name: Run manifest-driven Agda proof gate
         run: bash scripts/check-proofs.sh agda
+
+      - name: Proof gate fails a planted postulate and passes a clean module
+        run: bash tests/proofs/gate_controls_test.sh agda

docs/status/ROADMAP.adoc

@@ -29,11 +29,14 @@ Initial development phase.
 * Next: CI lanes for Rocq and Lean. Only the Agda gate runs in CI, so
   each witness has a current receipt only from a local run, and `PWG-1`
   needs one per commit.
-* Gate gap: `scripts/check-proofs.sh` passes a Rocq file with `Admitted`
-  and a Lean file with `sorry`, because it checks only the compiler's
-  exit and error lines. Both compile, and the axiom reports name them.
-  The Rocq and Lean gates should also fail when `Print Assumptions` or
-  `#print axioms` lists an axiom for a gated theorem.
+* Gate gap closed (2026-11-10, re-anchoring plan WO 1.3):
+  `scripts/check-proofs.sh` now audits each gated module after it compiles.
+  Rocq: `Print Assumptions` for each declared theorem. Lean: every declared
+  theorem must depend on no axiom. Agda: the postulate scan of januskey over
+  the first-party import cone. `tests/proofs/gate_controls_test.sh` plants an
+  `Admitted`, a `sorry` and a `postulate`; each fails the gate, and each fails
+  to fail on the old gate. Under Lean 4.29.0 `simp` brought `propext` into
+  `ApiTypes.lean`, which now proves both laws by `rfl`.
 
 === Open census work
 

scripts/check-proofs.sh

@@ -92,6 +92,96 @@
   LAST_OUT="$out"; return 1
 }
 
+# --- axiom audit: a gated module must also be free of axioms -------------------
+# Compiling is not enough (re-anchoring plan WO 1.3): coqc accepts `Admitted`
+# and lean accepts `sorry`; both name the gap only in their axiom reports. So a
+# gated module that compiles is audited as well, and fails if its axiom report
+# names an axiom. PROOF-POLICY §8.4: axioms travel with the grade.
+#   agda : the first-party modules of the import cone that Agda itself reports
+#          go through scan-postulates.sh (the reference gate of januskey).
+#   coq  : `Print Assumptions` for every Theorem, Lemma, Corollary, Proposition,
+#          Fact and Remark of the file must print "Closed under the global
+#          context".
+#   lean4: every theorem the source declares must depend on no axiom
+#          (Lean.collectAxioms, the function behind #print axioms). The
+#          lemmas Lean generates for an inductive are not witnesses.
+# Each audit fails closed: if it cannot show that it ran, the module fails.
+audit_one() {
+  # $1 source-root, $2 module; sets LAST_OUT on failure; returns 0 iff clean.
+  local root="$1" rel="$2" dir out rc base copy names expect got
+  dir="$(mktemp -d)"
+  case "$PROVER" in
+    agda)
+      set +e
+      out="$(cd "$ROOT/$root" && agda --safe --without-K --cubical-compatible \
+              --dependency-graph="$dir/cone.dot" "$rel" 2>&1)"; rc=$?
+      set -e
+      if [ "$rc" -ne 0 ] || [ ! -s "$dir/cone.dot" ]; then
+        LAST_OUT="axiom audit: no import cone from agda --dependency-graph"$'\n'"$out"; rm -rf "$dir"; return 1
+      fi
+      : >"$dir/own"
+      sed -n 's/.*label="\([^"]*\)".*/\1/p' "$dir/cone.dot" | LC_ALL=C sort -u |
+        while IFS= read -r name; do
+          f="$ROOT/$root/${name//.//}.agda"
+          [ -f "$f" ] && echo "$f" >>"$dir/own"
+        done
+      [ -s "$dir/own" ] || { LAST_OUT="axiom audit: no first-party module in the import cone"; rm -rf "$dir"; return 1; }
+      set +e; mapfile -t own <"$dir/own"; out="$(bash "$ROOT/scripts/scan-postulates.sh" "${own[@]}" 2>&1)"; rc=$?; set -e
+      ;;
+    coq)
+      base="$(basename "$rel" .v)"; copy="GateAudit_${base}"
+      names="$(awk '
+        /^[ \t]*Module[ \t]+Type[ \t]/ { split($0, w, /[ \t.]+/); stack[++d] = "T:" w[4]; next }
+        /^[ \t]*Module[ \t]+[A-Za-z_][A-Za-z0-9_'\'']*[ \t]*\.[ \t]*$/ ||
+        /^[ \t]*Module[ \t]+[A-Za-z_][A-Za-z0-9_'\'']*[ \t]*[:(<]/ && !/:=/ {
+          s = $0; sub(/^[ \t]*Module[ \t]+/, "", s); sub(/[^A-Za-z0-9_'\''].*/, "", s); stack[++d] = "M:" s; next }
+        /^[ \t]*Section[ \t]/ { stack[++d] = "S:"; next }
+        /^[ \t]*End[ \t]/ { if (d > 0) d--; next }
+        /^[ \t]*(Theorem|Lemma|Corollary|Proposition|Fact|Remark)[ \t]/ {
+          s = $0; sub(/^[ \t]*[A-Za-z]+[ \t]+/, "", s); sub(/[^A-Za-z0-9_'\''].*/, "", s)
+          q = ""; for (i = 1; i <= d; i++) if (stack[i] ~ /^M:/) q = q substr(stack[i], 3) "."
+          print q s }' "$ROOT/$root/$rel")"
+      if [ -z "$names" ]; then rm -rf "$dir"; LAST_OUT=""; return 0; fi
+      { cat "$ROOT/$root/$rel"; echo; while IFS= read -r n; do echo "Print Assumptions $n."; done <<<"$names"; } \
+        >"$ROOT/$root/$copy.v"
+      set +e; out="$(cd "$ROOT/$root" && coqc "$copy.v" 2>&1)"; rc=$?; set -e
+      rm -f "$ROOT/$root/$copy".{v,vo,vok,vos,glob} "$ROOT/$root/.$copy".aux
+      expect="$(grep -c . <<<"$names")"
+      got="$(grep -c '^Closed under the global context' <<<"$out" || true)"
+      if [ "$rc" -eq 0 ] && [ "$got" -eq "$expect" ]; then rc=0
+      else rc=1; out="axiom audit: $got of $expect theorem(s) closed under the global context"$'\n'"$out"; fi
+      ;;
+    lean4)
+      { echo "import Lean"; cat "$ROOT/$root/$rel"; cat <<'LEAN'
+
+open Lean Elab Command in
+#eval show CommandElabM Unit from do
+  let env ← getEnv
+  let mut n := 0
+  for (name, ci) in env.constants.map₂.toList do
+    -- Only theorems the source declares: the lemmas Lean generates for an
+    -- inductive (injEq, inj, sizeOf_spec) carry no declaration range.
+    if let .thmInfo _ := ci then
+      if (← liftCoreM (findDeclarationRanges? name)).isNone then continue
+      n := n + 1
+      let axs ← Lean.collectAxioms name
+      unless axs.isEmpty do
+        logInfo m!"GATE-AXIOMS {name}: {axs.toList}"
+  logInfo m!"GATE-AUDIT-DONE {n}"
+LEAN
+      } >"$dir/Audit.lean"
+      set +e; out="$(cd "$ROOT/$root" && lean "$dir/Audit.lean" 2>&1)"; rc=$?; set -e
+      if [ "$rc" -ne 0 ] || ! grep -q 'GATE-AUDIT-DONE' <<<"$out" || grep -q 'GATE-AXIOMS' <<<"$out"; then
+        rc=1; out="axiom audit: a theorem depends on an axiom, or the audit did not run"$'\n'"$(grep -E 'GATE-|error' <<<"$out" || printf '%s' "$out")"
+      fi
+      ;;
+    *) rc=0; out="" ;;
+  esac
+  rm -rf "$dir"
+  if [ "$rc" -eq 0 ]; then LAST_OUT=""; return 0; fi
+  LAST_OUT="$out"; return 1
+}
+
 echo "=== $PROVER proof check ==="
 
 # --- toolchain: absent means FAIL, never skip ---------------------------------
@@ -132,7 +222,11 @@
   printf '  %-30s %-24s ' "$root" "$rel"
   echo "$root/$rel" >>"$listed_tmp"
   if check_one "$root" "$rel"; then
-    if [ "$status" = gated ]; then
+    if [ "$status" = gated ] && ! audit_one "$root" "$rel"; then
+      echo "FAIL (compiles, but the axiom audit fails)"
+      printf '%s\n' "${LAST_OUT//$'\n'/$'\n        '}" | sed '1s/^/        /'
+      fails=$((fails + 1))
+    elif [ "$status" = gated ]; then
       echo "PASS"
     else
       echo "PASS -- UNEXPECTED (quarantined module now compiles)"

scripts/scan-postulates.sh

@@ -0,0 +1,82 @@
+#!/usr/bin/env bash
+# SPDX-License-Identifier: MPL-2.0
+# SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell
+# 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. check-proofs.sh passes it the first-party modules of the import
+# cone that Agda itself reports, so the files scanned are the files checked.
+#
+# Adopted unchanged in its lexer from hyperpolymath/januskey (989a747,
+# scripts/scan-postulates.sh), the reference gate PROOF-POLICY §8.4 names.
+#
+# 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. 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
+# 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; }
+done
+# 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; 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)
+      # 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
+      }
+      if (depth == 0 && two == "{-" && substr(line, i + 2, 1) == "#") {
+        pragma = 1; i += 3; code = code " "; 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
+        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 ~ /(^|[ \t.;{}()@])postulate([ \t.;{}()@]|$)/)
+      printf "%s:%d: %s\n", FILENAME, FNR, $0
+  }
+' "$@")"
+count=0
+[ -n "$hits" ] && count="$(printf '%s\n' "$hits" | wc -l | tr -d ' ')"
+[ -n "$hits" ] && printf '%s\n' "$hits"
+echo "postulate scan: $# files, $count postulate(s)"
+[ "$count" -eq 0 ] || exit 1

tests/proofs/gate_controls_test.sh

@@ -0,0 +1,42 @@
+#!/usr/bin/env bash
+# SPDX-License-Identifier: MPL-2.0
+# The proof gate must fail on a planted escape and pass the same module
+# without it (re-anchoring plan WO 1.3): an Agda `postulate`, a Rocq
+# `Admitted`, a Lean `sorry`. Each of these compiled, or would have, before
+# the axiom audit. A decoy in a comment must not fail the gate.
+# Usage: bash tests/proofs/gate_controls_test.sh agda|coq|lean4
+# Needs the prover on PATH; an absent prover fails, as in the gate itself.
+set -euo pipefail
+prover=${1:?usage: gate_controls_test.sh agda|coq|lean4}
+root=$(cd "$(dirname "$0")/../.." && pwd)
+t=$(mktemp -d); trap 'rm -rf "$t"' EXIT
+case "$prover" in
+  agda)  ext=agda; clean='module Clean where
+-- postulate in a comment is not a postulate
+data N : Set where
+  z : N
+  s : N → N'
+         planted='module Planted where
+postulate X : Set' ;;
+  coq)   ext=v; clean='(* Admitted. in a comment *)
+Theorem clean : 1 + 1 = 2. Proof. reflexivity. Qed.'
+         planted='Theorem planted : 2 + 2 = 5. Admitted.' ;;
+  lean4) ext=lean; clean='-- sorry in a comment
+theorem clean : 1 + 1 = 2 := rfl'
+         planted='theorem planted : 2 + 2 = 5 := by sorry' ;;
+  *) echo "unknown prover: $prover" >&2; exit 2 ;;
+esac
+run() { # name body -> exit status of the gate on a tree holding that module
+  local name=$1 body=$2 d=$t/$1
+  mkdir -p "$d/scripts" "$d/verification/proofs/$prover"
+  cp "$root/scripts/check-proofs.sh" "$root/scripts/scan-postulates.sh" "$d/scripts/"
+  printf '%s\n' "$body" > "$d/verification/proofs/$prover/$name.$ext"
+  echo "verification/proofs/$prover|$name.$ext|gated| control" > "$d/verification/proofs/$prover/MANIFEST"
+  bash "$d/scripts/check-proofs.sh" "$prover" > "$d.log" 2>&1
+}
+fail=0
+if run Clean "$clean"; then echo "PASS: $prover clean control passes"
+else echo "FAIL: $prover clean control failed"; cat "$t/Clean.log"; fail=1; fi
+if run Planted "$planted"; then echo "FAIL: $prover planted escape passed the gate"; cat "$t/Planted.log"; fail=1
+else echo "PASS: $prover planted escape fails the gate"; fi
+exit "$fail"

verification/proofs/lean4/ApiTypes.lean

@@ -16,19 +16,16 @@ namespace ApiResult
     | .ok v      => .ok (f v)
     | .error c m => .error c m
 
+  -- By `rfl` after `cases`: under Lean 4.29.0 `simp [map]` brings in `propext`.
   theorem map_id : ∀ (r : ApiResult α), map id r = r := by
     intro r
-    cases r with
-    | ok v => simp [map]
-    | error c m => simp [map]
+    cases r <;> rfl
 
   -- Proof: map composition (functor law: map (g ∘ f) = map g ∘ map f)
   theorem map_comp (f : α → β) (g : β → γ) :
       ∀ (r : ApiResult α), map (g ∘ f) r = map g (map f r) := by
     intro r
-    cases r with
-    | ok v => simp [map, Function.comp]
-    | error c m => simp [map]
+    cases r <;> rfl
 end ApiResult
 
 -- Example: Bounded confidence value (0.0 to 1.0 modelled as Nat/1000)

verification/proofs/lean4/MANIFEST

@@ -1,5 +1,5 @@
 # Lean4 proof manifest — read by scripts/check-proofs.sh lean4
 # Format: <source-root>|<module-relative-to-source-root>|gated|quarantine|<note>
 # Ground-truthed 2026-07-17 with Lean leanprover/lean4:v4.15.0 (via elan).
-verification/proofs/lean4|ApiTypes.lean|gated| compiles under Lean 4.15.0 (rechecked 2026-11-09; the 2026-07-17 Nat.zero_le error no longer reproduces); #print axioms: none
+verification/proofs/lean4|ApiTypes.lean|gated| compiles under Lean 4.29.0 (2026-11-10, axiom audit: none); both laws by rfl, because simp brings in propext under 4.29.0; not rechecked under 4.15.0 since that change
 verification/proofs/lean4|FeatureReachability.lean|gated| THY-1 Lean leg, re-proved; core only; #print axioms: none