From 770e56558e01f0bc2cf1e6d48257584b66daabe9 Mon Sep 17 00:00:00 2001 From: Claude Date: Tue, 10 Nov 2026 18:28:08 +0000 Subject: [PATCH] fix(proofs): fail the proof gate on Admitted, sorry and postulate (WO 1.3) scripts/check-proofs.sh passed a Rocq file with Admitted and a Lean file with sorry, because it checked only that the file compiled. Each gated module that compiles is now audited as well (PROOF-POLICY 8.4, "Axioms travel with the grade"), and each audit fails closed when it cannot show that it ran: - Rocq: Print Assumptions for every Theorem, Lemma, Corollary, Proposition, Fact and Remark the file declares must print "Closed under the global context". - Lean: every theorem the source declares must depend on no axiom (Lean.collectAxioms, behind #print axioms). The lemmas Lean generates for an inductive (injEq, inj, sizeOf_spec) have no declaration range and are not witnesses. - Agda: --safe already refuses postulate. The comment-aware postulate scan of hyperpolymath/januskey (989a747, scripts/scan-postulates.sh, the reference gate PROOF-POLICY 8.4 names) now runs over the first-party modules of the import cone that agda --dependency-graph reports. tests/proofs/gate_controls_test.sh plants an Admitted, a sorry and a postulate. Each fails the new gate, and the Rocq and Lean ones pass the old gate, so the test detects the gap. A clean module passes. The Agda lane runs the Agda controls; the Rocq and Lean lanes come with WO 1.4. Checked locally with Rocq 8.18.0 and Lean 4.29.0 (the versions the pinned Guix gives) and Agda 2.6.3 with its distribution stdlib: all gated modules pass. Under Lean 4.29.0, simp brought propext into the two ApiResult laws of ApiTypes.lean, a template file; both now hold by rfl after cases. The gate and ApiTypes.lean are template files: the same fix belongs in rsr-template-repo. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_0136P7ZnDRsCLfZcFcEzvPcM --- .github/workflows/agda-proof-policy.yml | 7 ++ docs/status/ROADMAP.adoc | 13 ++-- scripts/check-proofs.sh | 96 ++++++++++++++++++++++++- scripts/scan-postulates.sh | 82 +++++++++++++++++++++ tests/proofs/gate_controls_test.sh | 42 +++++++++++ verification/proofs/lean4/ApiTypes.lean | 9 +-- verification/proofs/lean4/MANIFEST | 2 +- 7 files changed, 238 insertions(+), 13 deletions(-) create mode 100644 scripts/scan-postulates.sh create mode 100755 tests/proofs/gate_controls_test.sh diff --git a/.github/workflows/agda-proof-policy.yml b/.github/workflows/agda-proof-policy.yml index ebac73cb..cf5004e3 100644 --- a/.github/workflows/agda-proof-policy.yml +++ b/.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 diff --git a/docs/status/ROADMAP.adoc b/docs/status/ROADMAP.adoc index 0a4c6e82..8a59be5e 100644 --- a/docs/status/ROADMAP.adoc +++ b/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 diff --git a/scripts/check-proofs.sh b/scripts/check-proofs.sh index 5eba30f3..0107cdb2 100755 --- a/scripts/check-proofs.sh +++ b/scripts/check-proofs.sh @@ -92,6 +92,96 @@ check_one() { 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 @@ while IFS='|' read -r root rel status note; do 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)" diff --git a/scripts/scan-postulates.sh b/scripts/scan-postulates.sh new file mode 100644 index 00000000..4d6fd6c6 --- /dev/null +++ b/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 diff --git a/tests/proofs/gate_controls_test.sh b/tests/proofs/gate_controls_test.sh new file mode 100755 index 00000000..27a4fb1f --- /dev/null +++ b/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" diff --git a/verification/proofs/lean4/ApiTypes.lean b/verification/proofs/lean4/ApiTypes.lean index f02f259c..8997f2b6 100644 --- a/verification/proofs/lean4/ApiTypes.lean +++ b/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) diff --git a/verification/proofs/lean4/MANIFEST b/verification/proofs/lean4/MANIFEST index d32aa6d5..5708f1b4 100644 --- a/verification/proofs/lean4/MANIFEST +++ b/verification/proofs/lean4/MANIFEST @@ -1,5 +1,5 @@ # Lean4 proof manifest — read by scripts/check-proofs.sh lean4 # Format: ||gated|quarantine| # 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