census: count a declared negative control as a control, not an axiom

docs/atlas/census/rows.jsonl

@@ -24,10 +24,10 @@
 {"axioms":0,"censused_at":"2026-11-10T21:47:20Z","class":"engineering","commit":"46b4b8b3db767d69658daf62b6bbe45474b1094b","declarations":60,"fixture_files":0,"holes":3,"own_files":3,"policy":0,"provers":"idris2 3","repo":"hyperpolymath/Cliodynamics.jl","status_doc":"","unsafe":0}
 {"axioms":0,"censused_at":"2026-11-10T21:47:22Z","class":"engineering","commit":"065abbeab23e694f9a46f00683a8ece26d04c1ac","declarations":60,"fixture_files":0,"holes":3,"own_files":3,"policy":0,"provers":"idris2 3","repo":"hyperpolymath/Cliometrics.jl","status_doc":"","unsafe":0}
 {"axioms":0,"censused_at":"2026-11-10T21:47:23Z","class":"theory","commit":"0c868315a7985d1a3409c523a2ff616acb2763c4","declarations":184,"fixture_files":0,"holes":0,"own_files":10,"policy":0,"provers":"agda 10","repo":"hyperpolymath/CompositionalCounts.jl","status_doc":"","unsafe":0}
-{"axioms":1,"censused_at":"2026-11-10T21:47:27Z","class":"theory","commit":"9903e7694418c3017c54806e8558bdf5414b8f37","declarations":63,"fixture_files":0,"holes":0,"own_files":15,"policy":0,"provers":"agda 15","repo":"hyperpolymath/CompositionalDA.jl","status_doc":"proofs/PROOF-STATUS.md","unsafe":0}
-{"axioms":1,"censused_at":"2026-11-10T21:47:42Z","class":"theory","commit":"08c5c641775bf96508d1ee845e580c88c6d8e29a","declarations":236,"fixture_files":0,"holes":0,"own_files":15,"policy":6,"provers":"agda 15","repo":"hyperpolymath/ExactCounts.jl","status_doc":"proofs/PROOF-STATUS.md","unsafe":0}
-{"axioms":1,"censused_at":"2026-11-10T21:47:47Z","class":"theory","commit":"cf0a5e8b02c90ea64d34ff3c7c1fae161bb0f8d2","declarations":44,"fixture_files":0,"holes":0,"own_files":9,"policy":1,"provers":"agda 9","repo":"hyperpolymath/ExactTests.jl","status_doc":"","unsafe":0}
-{"axioms":1,"censused_at":"2026-11-10T21:47:57Z","class":"theory","commit":"dd00204ace097ae4eccad7448f6505bbc2d44ad9","declarations":87,"fixture_files":12,"holes":1,"own_files":17,"policy":1,"provers":"agda 17","repo":"hyperpolymath/JuliaPackageSpitter.jl","status_doc":"PROOF-NEEDS.adoc","unsafe":1}
+{"axioms":0,"censused_at":"2026-11-13T18:29:20Z","class":"theory","commit":"93fbfaf1dfa08ac9e48137bc22d99c6909986d68","declarations":63,"fixture_files":0,"holes":0,"own_files":15,"policy":0,"provers":"agda 15","repo":"hyperpolymath/CompositionalDA.jl","status_doc":"proofs/PROOF-STATUS.md","unsafe":0}
+{"axioms":0,"censused_at":"2026-11-13T18:29:28Z","class":"theory","commit":"08c5c641775bf96508d1ee845e580c88c6d8e29a","declarations":236,"fixture_files":0,"holes":0,"own_files":15,"policy":0,"provers":"agda 15","repo":"hyperpolymath/ExactCounts.jl","status_doc":"proofs/PROOF-STATUS.md","unsafe":0}
+{"axioms":0,"censused_at":"2026-11-13T18:29:34Z","class":"theory","commit":"cf0a5e8b02c90ea64d34ff3c7c1fae161bb0f8d2","declarations":44,"fixture_files":0,"holes":0,"own_files":9,"policy":0,"provers":"agda 9","repo":"hyperpolymath/ExactTests.jl","status_doc":"","unsafe":0}
+{"axioms":1,"censused_at":"2026-11-13T18:29:37Z","class":"theory","commit":"dd00204ace097ae4eccad7448f6505bbc2d44ad9","declarations":87,"fixture_files":12,"holes":1,"own_files":17,"policy":1,"provers":"agda 17","repo":"hyperpolymath/JuliaPackageSpitter.jl","status_doc":"PROOF-NEEDS.adoc","unsafe":1}
 {"axioms":0,"censused_at":"2026-11-10T22:40:18Z","class":"theory","commit":"4dbd1adc08e50fb526eb756519634e67c63ac492","declarations":107,"fixture_files":0,"holes":0,"own_files":13,"policy":0,"provers":"agda 13","repo":"hyperpolymath/MetaManifold-WebUI","status_doc":"proofs/PROOF-STATUS.md","unsafe":0}
 {"axioms":0,"censused_at":"2026-11-10T21:48:16Z","class":"theory","commit":"a92a9e2fd5f0b43d0209ad92f1076aef2bddf520","declarations":1,"fixture_files":1,"holes":0,"own_files":1,"policy":0,"provers":"agda 1","repo":"hyperpolymath/ResidualEvidenceTypes.jl","status_doc":"","unsafe":0}
 {"axioms":0,"censused_at":"2026-11-10T21:48:22Z","class":"engineering","commit":"84b6e3644840233c02e660612fccc539cb66ddd2","declarations":60,"fixture_files":0,"holes":3,"own_files":3,"policy":0,"provers":"idris2 3","repo":"hyperpolymath/SMTLib.jl","status_doc":"","unsafe":0}

docs/atlas/generated/catalogue.adoc

@@ -83,9 +83,9 @@ than one.
 
 |https://github.com/hyperpolymath/nextgen-typing[hyperpolymath/nextgen-typing] |16 |11 |agda 3, lean 6, rocq 7 |118 |4 |0 |0 |0 |`PROOF-STATUS.adoc`
 
-|https://github.com/hyperpolymath/CompositionalDA.jl[hyperpolymath/CompositionalDA.jl] |15 |0 |agda 15 |63 |0 |1 |0 |0 |`proofs/PROOF-STATUS.md`
+|https://github.com/hyperpolymath/CompositionalDA.jl[hyperpolymath/CompositionalDA.jl] |15 |0 |agda 15 |63 |0 |0 |0 |0 |`proofs/PROOF-STATUS.md`
 
-|https://github.com/hyperpolymath/ExactCounts.jl[hyperpolymath/ExactCounts.jl] |15 |0 |agda 15 |236 |0 |1 |0 |6 |`proofs/PROOF-STATUS.md`
+|https://github.com/hyperpolymath/ExactCounts.jl[hyperpolymath/ExactCounts.jl] |15 |0 |agda 15 |236 |0 |0 |0 |0 |`proofs/PROOF-STATUS.md`
 
 |https://github.com/hyperpolymath/gitbot-fleet[hyperpolymath/gitbot-fleet] |15 |3 |agda 2, lean 4, rocq 3, idris2 6 |82 |5 |0 |0 |0 |`PROOF-NEEDS.adoc`
 
@@ -103,7 +103,7 @@ than one.
 
 |https://github.com/hyperpolymath/CompositionalCounts.jl[hyperpolymath/CompositionalCounts.jl] |10 |0 |agda 10 |184 |0 |0 |0 |0 |—
 
-|https://github.com/hyperpolymath/ExactTests.jl[hyperpolymath/ExactTests.jl] |9 |0 |agda 9 |44 |0 |1 |0 |1 |—
+|https://github.com/hyperpolymath/ExactTests.jl[hyperpolymath/ExactTests.jl] |9 |0 |agda 9 |44 |0 |0 |0 |0 |—
 
 |https://github.com/hyperpolymath/boinc-boinc[hyperpolymath/boinc-boinc] |8 |0 |lean 8 |46 |0 |0 |0 |0 |`PROOF-NEEDS.adoc`
 

scripts/census/proof-holes.sh

@@ -11,6 +11,12 @@
 #   axiom   trusted base grows (postulate, Axiom, #[trusted], pragma Assume, …)
 #   unsafe  a checker is switched off (TERMINATING, Unset Guard Checking, SPARK_Mode Off, …)
 #   policy  estate rule broken (import Mathlib, Agda file without --safe)
+#   control a finding inside a declared negative control: a file whose own header
+#           carries a line comment `EXPECT: <pattern>`, the home repository's
+#           statement that the checker must reject it for that reason (for
+#           example CompositionalDA.jl proofs/agda/reject/). It is reported, not
+#           dropped, but it is not a hole, axiom, unsafe or policy count and does
+#           not affect --fail-on: the home gate is what rejects it.
 #
 # This is a textual scan: it finds candidates, it does not decide them. A
 # kernel-level audit (#print axioms, Print Assumptions, gnatprove report,
@@ -34,7 +40,7 @@ while [ $# -gt 0 ]; do
     --fail-on) FAIL_ON=${2:-}; shift 2 ;;
     --summary) SUMMARY=1; shift ;;
     --exclude) EXTRA_EX+=("$2"); shift 2 ;;
-    -h|--help) sed -n '3,22p' "$0"; exit 0 ;;
+    -h|--help) sed -n '3,28p' "$0"; exit 0 ;;
     -*) echo "unknown option: $1" >&2; exit 2 ;;
     *) DIR=$1; shift ;;
   esac
@@ -96,9 +102,17 @@ dedukti~*.dk,*.lp~^\s*(//|\(;)~hole~admit~\badmit(ted)?\b
 EOF
 )
 
-emit() { # lang class marker file line text
-  jq -cnS --arg lang "$1" --arg class "$2" --arg marker "$3" --arg file "$4" \
-        --argjson line "$5" --arg text "$6" \
+# A negative control declares itself: a line comment `EXPECT: <pattern>` in the
+# file names the error the home gate expects when it rejects the file.
+is_control() {
+  local path=$1
+  grep -qE '^[[:space:]]*(--|//|#)[[:space:]]*EXPECT:[[:space:]]*[^[:space:]]' "$path" 2>/dev/null
+}
+emit() {
+  local lang=$1 class=$2 marker=$3 file=$4 line=$5 text=$6
+  if [[ $class != control ]] && is_control "$DIR/$file"; then class=control; fi
+  jq -cnS --arg lang "$lang" --arg class "$class" --arg marker "$marker" --arg file "$file" \
+        --argjson line "$line" --arg text "$text" \
         '{lang:$lang,class:$class,marker:$marker,file:$file,line:$line,text:$text}'
 }
 
@@ -211,7 +225,10 @@ if [ "$SUMMARY" = 1 ]; then
   jq -rs 'group_by(.lang+" "+.class) | map("\(.[0].lang) \(.[0].class): \(length)") | .[]' "$OUT" >&2
 fi
 
-count() { jq -s --arg c "$1" '[.[] | select($c=="any" or .class==$c)] | length' "$OUT"; }
+count() {
+  local wanted=$1
+  jq -s --arg c "$wanted" '[.[] | select(.class!="control" and ($c=="any" or .class==$c))] | length' "$OUT"
+}
 case "$FAIL_ON" in
   none) exit 0 ;;
   hole) [ "$(count hole)" -eq 0 ] ;;

scripts/census/summarise.sh

@@ -53,7 +53,7 @@ echo "| proof artefact files | $nfiles |"
 echo "| declarations extracted | $ndecls |"
 echo "| hole-scanner findings | $(wc -l < holes.jsonl) |"
 echo
-echo "Hole classes (from proof-holes.sh): hole = unfinished proof, axiom = trusted base grows, unsafe = checker switched off, policy = estate rule (Agda without --safe, import Mathlib)."
+echo "Hole classes (from proof-holes.sh): hole = unfinished proof, axiom = trusted base grows, unsafe = checker switched off, policy = estate rule (Agda without --safe, import Mathlib), control = a finding inside a declared negative control (a file whose header has an EXPECT: line; reported, not counted)."
 echo
 echo "## Repos with artefacts (sorted by declarations)"
 echo

tests/census/proof_holes_control_test.sh

@@ -0,0 +1,25 @@
+#!/usr/bin/env bash
+# SPDX-License-Identifier: MPL-2.0
+# A file that declares itself a negative control (a header line comment
+# `EXPECT: <pattern>`, as in CompositionalDA.jl proofs/agda/reject/) has its
+# findings reported as class "control", not "axiom"/"policy". The same marker in
+# a file with no EXPECT line is still an axiom, and --fail-on is unaffected by
+# a control. Regression for the CompositionalDA.jl row (axioms 1, 2026-11-10).
+set -euo pipefail
+SCAN="$(cd "$(dirname "${BASH_SOURCE[0]}")/../.." && pwd)/scripts/census/proof-holes.sh"
+F=$(mktemp -d); trap 'rm -rf "$F"' EXIT
+printf '%s\n' '-- Negative control.' '-- EXPECT: [Pp]ostulate' 'module reject.P where' 'postulate z : Set' > "$F/Control.agda"
+printf '%s\n' '{-# OPTIONS --safe #-}' 'module Real where' 'postulate z : Set' > "$F/Real.agda"
+printf '%s\n' '{-# OPTIONS --safe #-}' 'module Prose where' '-- see EXPECT: in the control' 'postulate y : Set' > "$F/Prose.agda"
+got=$(bash "$SCAN" --fail-on none "$F" | jq -r '"\(.file):\(.line) \(.class) \(.marker)"' | sort)
+want=$(sort <<'WANT'
+Control.agda:1 control no --safe
+Control.agda:4 control postulate
+Prose.agda:4 axiom postulate
+Real.agda:3 axiom postulate
+WANT
+)
+[[ "$got" == "$want" ]] || { echo "FAIL: control classification differs"; diff <(printf '%s\n' "$want") <(printf '%s\n' "$got") || true; exit 1; }
+rm "$F/Real.agda" "$F/Prose.agda"
+bash "$SCAN" --fail-on any "$F" >/dev/null || { echo "FAIL: a control alone must not fail --fail-on any"; exit 1; }
+echo "PASS: negative-control findings classed control, real and prose-only files still axioms"