fix(census): name a repo's PROOF-STATUS, not its PROOF-NEEDS, as status_doc

Justfile

@@ -739,6 +739,7 @@ atlas-build:
 atlas-check:
     bun scripts/atlas/census-atlas.mjs check
     bun test tests/atlas/census-atlas.test.mjs
+    bash tests/census/build_rows_status_test.sh
 
 atlas-find query:
     bun scripts/atlas/census-atlas.mjs find "{{query}}"

scripts/census/build-rows.sh

@@ -14,6 +14,13 @@
 # tests/, fixtures/, corpus/, benches/ count as fixtures. "theory" is a
 # first-pass heuristic: more Agda/Lean/Rocq/Isabelle files than Idris2/SPARK
 # files. A human confirms each row.
+#
+# status_doc names one document per repository. A repository's proof status
+# lives in its PROOF-STATUS file (standards PROOF-POLICY §8.5); PROOF-NEEDS
+# lists obligations and proof-debt lists holes. So a PROOF-STATUS document
+# wins over a proof-debt one, which wins over a PROOF-NEEDS one; within a
+# rank the first path in sorted order wins. Taking the first sorted path
+# alone named docs/status/PROOF-NEEDS.adoc over docs/status/PROOF-STATUS.adoc.
 set -euo pipefail
 R=$1 T=$2
 tmp=$(mktemp -d); trap 'rm -rf "$tmp"' EXIT
@@ -42,7 +49,11 @@ jq -r '.repo+"\t"+.path' "$R/repos-with-status.jsonl" | sort > "$tmp/status.tsv"
 awk -F'\t' '
   FILENAME ~ /holes\.tsv$/  { h[$1" "$2]++; next }
   FILENAME ~ /decls\.tsv$/  { d[$1]++; next }
-  FILENAME ~ /status\.tsv$/ { if (!($1 in st)) st[$1]=$2; next }
+  FILENAME ~ /status\.tsv$/ {
+    b = tolower($2); sub(/.*\//, "", b)
+    k = (b ~ /^proof-status/) ? 3 : (b ~ /^proof-debt/) ? 2 : 1
+    if (!($1 in st) || k > sk[$1]) { st[$1]=$2; sk[$1]=k }
+    next }
   { n[$1]++; if ($3) fx[$1]++; pc[$1" "$2]++
     if ($2 ~ /agda|lean|rocq|isabelle/) th[$1]++; if ($2 ~ /idris2|spark/) en[$1]++ }
   END {

tests/census/build_rows_status_test.sh

@@ -0,0 +1,49 @@
+#!/usr/bin/env bash
+# SPDX-License-Identifier: MPL-2.0
+#
+# build-rows.sh picks one status_doc per repository: PROOF-STATUS over
+# proof-debt over PROOF-NEEDS, the first sorted path within a rank. The
+# previous rule (first sorted path) named docs/status/PROOF-NEEDS.adoc for
+# repositories whose status lives in docs/status/PROOF-STATUS.adoc.
+# Usage: bash tests/census/build_rows_status_test.sh   (needs jq)
+set -euo pipefail
+ROOT="$(cd "$(dirname "${BASH_SOURCE[0]}")/../.." && pwd)"
+command -v jq >/dev/null || { echo "FAIL: jq is required" >&2; exit 1; }
+raw=$(mktemp -d); trap 'rm -rf "$raw"' EXIT
+
+: > "$raw/holes.jsonl"; : > "$raw/decls.jsonl"
+# A non-empty template list: build-rows.sh reads it with NR==FNR, so an
+# empty list would swallow files.jsonl as template paths and emit no rows.
+echo "verification/proofs/template-only.v" > "$raw/template.txt"
+for r in o/both o/needs-only o/debt-and-needs o/root-status o/none; do
+  printf '{"repo":"%s","path":"src/A.agda","ext":"agda"}\n' "$r"
+done > "$raw/files.jsonl"
+cat > "$raw/repos-with-status.jsonl" <<'J'
+{"repo":"o/both","path":"docs/status/PROOF-NEEDS.adoc"}
+{"repo":"o/both","path":"docs/status/PROOF-STATUS.adoc"}
+{"repo":"o/needs-only","path":"docs/status/PROOF-NEEDS.adoc"}
+{"repo":"o/debt-and-needs","path":"PROOF-NEEDS.md"}
+{"repo":"o/debt-and-needs","path":"docs/proof-debt.adoc"}
+{"repo":"o/root-status","path":"PROOF-NEEDS.adoc"}
+{"repo":"o/root-status","path":"proofs/proof-status.md"}
+{"repo":"o/root-status","path":"PROOF-STATUS.adoc"}
+J
+
+rows=$(bash "$ROOT/scripts/census/build-rows.sh" "$raw" "$raw/template.txt")
+doc() {
+  local repo="$1"
+  jq -r --arg r "$repo" '.[] | select(.repo == $r) | .status_doc' <<< "$rows"
+}
+fail=0
+expect() {
+  local repo="$1" want="$2" got
+  got=$(doc "$repo")
+  if [[ "$got" == "$want" ]]; then echo "PASS: $repo -> ${want:-<none>}"
+  else echo "FAIL: $repo -> '$got', expected '$want'"; fail=1; fi
+}
+expect o/both            docs/status/PROOF-STATUS.adoc
+expect o/needs-only      docs/status/PROOF-NEEDS.adoc
+expect o/debt-and-needs  docs/proof-debt.adoc
+expect o/root-status     PROOF-STATUS.adoc
+expect o/none            ""
+exit "$fail"