diff --git a/README.adoc b/README.adoc index 23225589..796d6971 100644 --- a/README.adoc +++ b/README.adoc @@ -11,7 +11,7 @@ Proofs stay in their home repositories. mathesis points at them. Later it will also hold the Agda sources for theory that has no other natural home. The rules for where a proof *should* live are not here: they are -https://github.com/metadatastician/standards/blob/main/3-practice/PROOF-POLICY.adoc[the canonical standards/3-practice/PROOF-POLICY.adoc] (Creusot for Rust, SPARK for Ada, +https://github.com/metadatastician/standards/blob/main/3-practice/PROOF-POLICY.adoc[the canonical standards/3-practice/PROOF-POLICY.adoc] (Creusot with Pearlite contracts, and Verus, for Rust; SPARK for Ada; Idris2 for APIs, ABIs and engineering properties, Agda for theory rechecked in Rocq and Lean). The working method is the proof-craft skill. diff --git a/docs/proposals/mathesis-re-anchoring.adoc b/docs/proposals/mathesis-re-anchoring.adoc index 3e650954..34ccb82e 100644 --- a/docs/proposals/mathesis-re-anchoring.adoc +++ b/docs/proposals/mathesis-re-anchoring.adoc @@ -1210,89 +1210,99 @@ three different practices (<>). [appendix] [[triage]] -== Provisional triage of the open pull requests +== Triage of the open pull requests (ruled 2026-11-10) -The table comes from commit subjects and file lists at 2026-11-10. Each row -needs a full read of the diff (<>). Each pull request conflicts with -`main`. +The implementation session read each full diff on 2026-11-10 and put each +row to the owner, who approved every row (ruling D-6 (a)). Each pull request +conflicted with `main`. The kept parts land in four landing pull requests from +one branch: A (scanner fixes, hyperpolymath/mathesis#51), B (one refresh tool, +#52), C (frame, #53) and D (documents, the pull request that adds this table). +Each original closes with a pointer to its landing pull request. No other +branch is written. [cols="1,4,4",options="header"] |=== -|PR |Content that `main` does not have |Provisional disposition +|PR |What `main` lacked |Ruled disposition |16 -|An audit report of the ECHIDNA proof route. The record of ruling D-10. -|Keep both as documents. Drop the row changes. +|An audit report of the ECHIDNA proof route, with ruling D-10. +|Report lands in D. Rows and the script change are dropped. Closed. |17 -|Nothing found. The status-document fix and the canon 2.1.5 pin are on -`main`. -|Close as superseded. +|Only its CI step: `main` did not run the census tests. +|CI step lands in A. Closed. |20 -|Template boilerplate matched by blob, first implementation. -|Choose one of 20 and 26. +|Template boilerplate by blob, first design, with a test. +|Test lands in A, adapted to the design of 26. Its refresh script is dropped. +Closed. |22 -|Tests for status-document choice. The trope-checker grades, typed into the -register. -|Keep the tests. Move the grades to the registry (<>). +|Order-independent status tests, two trope-checker register rows, a prose +grade census. +|Tests and rows land in D. The prose grade census is dropped: the registry +derives grades (<>). Closed. |24 -|A partial refresh that records provenance. A finding: one occupancy proof -fails under its pinned Lean. -|Keep the provenance design for <>. Keep the finding. +|Reconnaissance rows for nine repositories and the occupancy finding; a +second refresh mode and a provenance file. +|Rows and finding land in D, without its januskey rows (superseded by CI +rows). The mode and the file are dropped for <>. Closed. |25 -|A fix that keeps rows when the template list is empty. -|Check `main` for the same fix. Then close or rebase that part. +|A fix: on `main` an empty template list dropped every row. +|Fix and test land in A. Closed. |26 -|Template boilerplate matched by path and blob, second implementation. -|Choose one of 20 and 26. +|Template boilerplate by (path, blob), second design. +|The design lands in A. Closed. |27 -|A scanner that skips comments and strings. Idris2 signatures without -clauses, reported as axiom candidates. -|Keep the scanner changes. Send them to the scanner's source. +|A scanner that blanks comments and strings; Idris2 signatures without +clauses as axiom candidates. +|Lands in A. The change goes to the proof-craft source. Closed. |31 -|The census sees proofs written in Rust (Creusot, Pearlite, Verus). -|Keep. PROOF-POLICY §1.2 makes this necessary. +|The census sees Rust proofs (Creusot, Pearlite, Verus); nested status +documents rank last. +|Lands in A. Closed. |34 -|Verus rules. -|Fold into 31. Close the remainder. +|One Verus rule; a proof-burrower register row; the Rust wording; an +ECHIDNA relabel. +|Rule in A; row and wording in D. The relabel waits: the receipt it cites is +not on the `main` of echidna. Closed. |36 -|25 repositories that the frame lacks. A derived row count. -|Keep both. Drop the rerun data. +|A derived row count; the atlas rebuilt with each census. +|Lands in C. The frame was already on `main`. Closed. |39 -|The owner's proofs in one fork, with the fork listed. -|Keep the fork listing. Take the row from the next census. +|A third-party upstream added to `repos.json` by hand. +|Closed. `main` lists the fork; a sync of the fork gives the row. |40 -|A census rerun. -|Close as superseded by the next single run. +|Nothing: a census rerun. +|Closed. |41 -|A row refresh tool with atomic publication and tests. -|Choose one refresh tool among `main`, 24, 41 and 42. +|A public-only check; a repository-map fix; a snapshot step. +|Check and fix land in B. The snapshot step is dropped: it needs +`mv --exchange`, which ubuntu-24.04 does not have. Closed. |42 -|Wording that says the catalogue has no grades. -|Keep the wording. See 41. +|A sentence that the catalogue carries no grades. +|Lands in B. Closed. |44 -|Ada counted as SPARK only where the code opts in. -|Keep the scanner change. Drop the row changes. +|Ada counted as SPARK only where it opts in; the template owns its files. +|Lands in A. Closed. |45 -|Nothing found beyond a rerun. -|Close as superseded. +|Nothing: status-document order and a rerun. +|Closed. |=== `scripts/census/proof-holes.sh` is a copy of the scanner from the proof-craft -skill. Pull requests 27, 31, 34 and 44 change the copy. The same change must -reach the source, or the two will differ. +skill. Landing change A changes the copy. The same change must reach the +source, or the two will differ. diff --git a/docs/reports/audit/echidna-proof-route-2026-11-09.adoc b/docs/reports/audit/echidna-proof-route-2026-11-09.adoc new file mode 100644 index 00000000..4ae39e83 --- /dev/null +++ b/docs/reports/audit/echidna-proof-route-2026-11-09.adoc @@ -0,0 +1,101 @@ +// SPDX-License-Identifier: CC-BY-SA-4.0 += The echidna proof route: theorems, receipts and grades (2026-11-09) +:toc: + +This is a dated, source-anchored record of the proofs the echidna proof route +rests on. It is *not* a claims registry: the atlas README leaves that design +open. Each theorem lives in its home repository, which owns its statement, +receipts and status (PROOF-POLICY §2.2, §8.5). This page points at them. The +Proof Witness Grades (PWG) below are derived from those receipts, not +assigned here. + +An agent drafted this record and the statement comparison it cites. Neither +has been reviewed by the owner yet, so neither counts as independent +corroboration. + +The plan these rows come from is +https://github.com/metadatastician/standards/blob/main/docs/ULTRAPLAN-ECHIDNA-PROOF-ROUTE-2026-11-04.adoc[the echidna proof-route ultraplan] +(ladder rows in brackets; v0.2.4 is metadatastician/standards#1434). + +== Theory theorems + +Census: 4 theory theorems in this route. `PWG-1`: 0. `PWG-2ii`: 0. +`PWG-2i`: 0. `PWG-3`: 1. `ungraded`: 3, all planned with no Agda source yet. + +[cols="2,2,3,2,3",options="header"] +|=== +|Theorem |Home |Legs: §5 token, §2.2 state |Derived PWG |Receipts + +|Receipt boundary, T-RECEIPT: a warrant token does not give its claim +without a soundness map; no unconditional reflection exists (feeds rows 4-5) +|hyperpolymath/echidnabot, `docs/PROOF-STATUS.adoc` +|Agda `proven`. Lean `proven`, re-proved, `BRIDGE-PENDING`. Rocq `proven`, +re-proved, `BRIDGE-PENDING`. No axioms in any leg. +|`PWG-3`. It would become `PWG-2ii` once the drafted statement comparison is +reviewed and both legs are `RECONCILED`. +|Agda 2.8.0.2 (§2.1 profile), Lean 4.35.0, Coq 8.18.0, at echidnabot +`1443adfabb98a9e0daea562bc8dbe764442c14cc`; agent session. The per-commit +CI job is hyperpolymath/echidnabot#195. + +|Token order and weakest-step meet; level monotonicity (row 2) +|hyperpolymath/mathesis (owner ruling D-10, 2026-11-09); no Agda source yet +|`open` +|`ungraded` +|None + +|Retraction never raises a level; name-wise retraction kills exactly its +dependents (row 7) +|hyperpolymath/residual-evidence-types (Agda source of `Revision.agda`) +|`open` for the stated theorem +|`ungraded` +|None for this statement. The Idris2 transcription is below. + +|Status fold is a join on the token lattice (row 12) +|hyperpolymath/mathesis (owner ruling D-10, 2026-11-09); no Agda source yet +|`open` +|`ungraded` +|None +|=== + +== Engineering proofs (not graded, PROOF-POLICY §8.1) + +[cols="2,2,2,3",options="header"] +|=== +|Proof |Home |Token |Receipt + +|`Verdict.idr`: `Sound` only from a confirming prover re-check; level +"sound" only with a witness +|hyperpolymath/hypatia, `verification/PROOF-STATUS.adoc` +|`proven` (Idris2); correspondence with epistemic-types `Warrant.agda` is +`argued` +|Idris2 v0.7.0, `verify-proofs.yml` run 42559874988 at +`c639c465e9bbbd01522f1eae12ac98a071afac13`, with accept and reject fixtures + +|`Retraction.idr`: retraction as a thinning; a finding survives through a +token +|hyperpolymath/hypatia +|`proven` (Idris2); correspondence with residual-evidence-types is `argued`. +It retracts one occurrence by position, while the runtime retracts by name +(ladder row 7). +|Same run + +|echidnabot GraphQL gate, E-AUTH-SCOPE, E-AUTH-ROLE, E-AUTH-GUARD, +E-RATE-BOUND (row 15) +|hyperpolymath/echidnabot, `docs/PROOF-STATUS.adoc` +|`open` under Creusot/Pearlite and Verus (§1.2) +|Tests only, which are not proof receipts +|=== + +== Census corrections made with this record + +* The catalogue rows for echidnabot and hypatia were refreshed from a census + of those two repositories on 2026-11-09. echidnabot now shows its Agda, + Lean and Rocq theory files. +* `scripts/census/build-rows.sh` chose whichever status document sorted + first, so hypatia was listed under `docs/proof-debt.adoc`. It now prefers + a `PROOF-STATUS` file, then `PROOF-NEEDS`, then `proof-debt`, so hypatia's + CI-checked `verification/PROOF-STATUS.adoc` is the one shown. Other rows + pick up this rule at the next full census. +* echidnabot's class is still the heuristic `theory`, from its file counts. + Most of its proof files are prover fixtures (PROOF-POLICY §3); one + theorem is real theory. diff --git a/docs/status/CROSS-PROVER-RECONCILIATION.adoc b/docs/status/CROSS-PROVER-RECONCILIATION.adoc index 58c866bc..9fe01569 100644 --- a/docs/status/CROSS-PROVER-RECONCILIATION.adoc +++ b/docs/status/CROSS-PROVER-RECONCILIATION.adoc @@ -116,6 +116,14 @@ grade field. |Mathesis |Manifest-driven per-prover gate and proof inventory; historical Agda manifest only attested `--safe` |Run full-mode check and attach genuine run receipt; only then advance status |ECHIDNA |Dogfood Agda corpus and meta-checker CI have separate commands; MetaChecker contains at least one stale 'funext' exception comment |Enforce uniform invocation and audit all imports/assumptions before marking Agda verified |januskey |Four theory roots (`Reversibility`, `TransactionAtomicity`, `SingleActiveLog`, `Epistemic`) checked in CI under the canonical flags plus `--no-libraries --ignore-interfaces --double-check`, Agda 2.6.4.3, sibling `resource-algebra` pinned by commit; the gate scans the import cone for postulates and refuses seven expected-rejection fixtures. T-1 is re-proved in core Rocq and Lean with its statement comparison recorded |Recheck the four remaining `PWG-3` rows (G-1, T-2, T-3, E-1m) in Rocq and Lean. The Rust TransactionManager refines the abstract log only by transcription (januskey T-10, OPEN) +|echo-types |Local run 2026-11-09, Agda 2.6.3, cold, under `--safe --without-K --cubical-compatible` (stdlib v2.3 `8326c74`, absolute-zero `f486c29`): all five non-cubical entrypoints pass; the `All` cone is 125 local modules with no escape. Recipes pass no `--cubical-compatible`; file pragmas carry it in 131 of 137 files. `EchoImageFactorizationPropCubical` is checked in full Cubical through its pragma. No Rocq or Lean leg |Put the canonical flags in recipes and CI; give the cubical island a reviewed profile; record receipts in the home `PROOF-STATUS` for the eligible theorems (`Echo-comp-iso`, `cancel-iso`, `Echo-comp-pent-Σ-assoc`, `echo↔fib`, `A↔ΣEcho`, `echo-pullback-univ`, `GCLaws`, `no-section-of-collapsing-map`) +|secret-types |Local run 2026-11-09, Agda 2.6.3, cold, under `--safe --without-K --cubical-compatible` (builtins only): `SecretTypes.All` passes; 2/2 rejection fixtures refused. Its own `-W error` fails under the canonical flags unless `-W noUnsupportedIndexedMatch` is added. Rocq and Lean files present are RSR template files |Adopt the canonical flags; re-run at the pinned Agda 2.6.4.3; record receipts for N-1, N-2, N-3, N-7, N-8 +|epistemic-types |Local run 2026-11-09, Agda 2.6.3, cold, under `--safe --without-K --cubical-compatible`: all 22 `src` modules and `CanonicalEcho` pass; 13/13 rejection fixtures refused |Re-run at the pinned Agda 2.6.4.3; record receipts; refresh the stale module counts in `PROOF-STATUS` +|residual-evidence-types |Local run 2026-11-09, Agda 2.6.3, cold, under `--safe --without-K --cubical-compatible`: `All`, both comparisons and `Correspondence` pass; 9/9 rejection fixtures refused |Re-run at the pinned Agda 2.6.4.3; record receipts for the Core, Context and Composition laws +|choreographic-types |Local run 2026-11-09, Agda 2.6.3, cold, under `--safe --without-K --cubical-compatible`: both roots pass with all `src` modules in cone; 5/5 rejection fixtures refused. The MaxPlus rows are said to equal tropical-types' Lean instance; that is not proved |Re-run at the pinned Agda 2.6.4.3; record receipts; state the MaxPlus correspondence as `BRIDGE-PENDING` +|occupancy-types |Local run 2026-11-09, Agda 2.6.3, cold, under `--safe --without-K --cubical-compatible` (resource-algebra `0b338c9`): passes; 2/2 rejection fixtures refused. The Agda check is not called by any workflow, recipe or script. Under its pinned Lean 4.15.0, `StackcertCore.lean` does not compile (type errors in the proof of `cert_sound`) |Wire the Agda check first; move R-6 to TESTED; repair `stackcert` under Lean 4.15.0 or retract the README claim that it compiles +|absolute-zero |Local run 2026-11-09, Agda 2.6.3, cold, under `--safe --without-K --cubical-compatible`, stdlib 1.7.3 (its CI) and 2.3 (what echo-types consumes): the four modules pass. Most CNO lemmas are vacuous; `cno-composition` and OND1–OND5 carry content. The archived Lean uses Mathlib |Grade only `cno-composition` and OND1–OND5; record the stdlib pin; mark the archived Coq and Lean sections as archived +|affinescript |No Agda source for any theory theorem. Coq 8.18: all 20 `formal/` files build and all 137 assertions are closed under the global context; several hold by definition. Idris2 0.7.0: the Solo core proves progress and preservation. The 23 staged files under `proposals/` pass the canonical flags but are unwired |Owner chooses the Agda home (AffineScript completion plan, question 17); port `QttSemiring` first; compare the Rocq statements and record the bridge. The repo's proof ledger is in `docs/EXPLAINME.adoc` |=== Existing proof statuses in these repos are historical evidence, not @@ -138,6 +146,15 @@ full-mode runs or cross-prover reconciliations were observed during this policy edit**. CI must supply the evidence before any result is relabelled. +On 2026-11-09 the rows for echo-types, secret-types, epistemic-types, +residual-evidence-types, choreographic-types, occupancy-types, absolute-zero and +affinescript were added from local runs (hyperpolymath/mathesis#24, landed +2026-11-10; its januskey rows are not carried, because the januskey rows above +come from CI). Those runs are +reconnaissance: they used Agda 2.6.3, while four of these repositories pin +2.6.4.3, and they are not receipts recorded in the home repositories. So no +of those rows moved past `AGDA-PENDING`, and no grade is derived. + == Register format (initially not reconciled) First populated rows (2026-11-09): the squeakwell recovery ladder, from @@ -170,6 +187,17 @@ not hand-edited here. |januskey |T-2 `lifecycle-preserves-good` |AGDA-VERIFIED |NOT-INVENTORIED |BRIDGE-PENDING |januskey |T-3 `at-most-one-active` |AGDA-VERIFIED |NOT-INVENTORIED |BRIDGE-PENDING |januskey |E-1m epistemic model (`Epistemic.agda`) |AGDA-VERIFIED |NOT-INVENTORIED |BRIDGE-PENDING +|echo-types |Composition and fibration headlines (`All` cone) |AGDA-PENDING |NOT-INVENTORIED |BRIDGE-PENDING +|secret-types |TINI and countermodels (N-1, N-2, N-3, N-7, N-8) |AGDA-PENDING |NOT-INVENTORIED (template files only) |BRIDGE-PENDING +|epistemic-types |Ordered-group and Kripke rows |AGDA-PENDING |NOT-INVENTORIED |BRIDGE-PENDING +|residual-evidence-types |Core, Context and Composition laws |AGDA-PENDING |NOT-INVENTORIED |BRIDGE-PENDING +|choreographic-types |K, W, T, Y, A, B and E rows |AGDA-PENDING |MaxPlus said to match a tropical-types Lean instance; not audited |BRIDGE-PENDING +|occupancy-types |R-1, R-3, R-4 |AGDA-PENDING (unwired) |Lean `stackcert` fails to compile at its 4.15.0 pin |BRIDGE-PENDING +|absolute-zero |`cno-composition`, OND1–OND5 |AGDA-PENDING |Archived; the Lean uses Mathlib |BRIDGE-PENDING +|affinescript |QTT semiring laws, STLC and records progress and preservation, Solo core |INVENTORIED (no Agda source) |COQ-CHECKED (Coq 8.18, 2026-11-09); Lean none; Solo core in Idris2 |BRIDGE-PENDING +|trope-checker |Theorem B, Targets 1–4 |AGDA-VERIFIED: `proofs.yml` run 42623339243 at `c0eb4f1`, log `PASS: All.agda + Smoke.agda typecheck (--safe --without-K --cubical-compatible)`, Agda 2.7.0.1 + stdlib v2.0 pinned by SHA-256 |Rocq: none exists (ADR 0005 D5 removed the template). Lean: states no part of Theorem B |BRIDGE-PENDING (no leg to bridge to) +|trope-checker |O1-carrier atom factorisation, tropical factorisations, grade-algebra boundary |No Agda source states them |LEAN-CHECKED (kernel-accepted; `[propext]` for `GradeR.atom_factorization`). Rocq: none. The whole Lean package imports Mathlib, which PROOF-POLICY §2 forbids for a recheck leg |BRIDGE-PENDING +|proof-burrower |`Burrow/Trust.agda`, `Burrow/Ledger.agda` (DOM-1, DOM-2) |AGDA-PENDING (a 2026-11-09 re-check passed under the policy flags; no receipt is committed in that repository and no CI job runs it) |NOT-INVENTORIED |BRIDGE-PENDING |=== The januskey rows are evidence-backed, not a todo. januskey owns these theorems diff --git a/tests/census/status_doc_cases_test.sh b/tests/census/status_doc_cases_test.sh new file mode 100755 index 00000000..1fcb87a5 --- /dev/null +++ b/tests/census/status_doc_cases_test.sh @@ -0,0 +1,101 @@ +#!/usr/bin/env bash +# SPDX-License-Identifier: MPL-2.0 +# Focused regression tests for census status-document selection. No network used. +# Usage: bash tests/census/status_doc_cases_test.sh +# From hyperpolymath/mathesis#22 (21677f7): the cases that hold whatever the +# order of proof-debt and PROOF-NEEDS. +set -euo pipefail +export LC_ALL=C +repo=$(cd "$(dirname "${BASH_SOURCE[0]}")/../.." && pwd) +work=$(mktemp -d) +trap 'rm -rf "$work"' EXIT +fail() { echo "FAIL: $*" >&2; exit 1; } +command -v jq >/dev/null || fail 'jq is required' + +# Every repo has one non-template file so it produces a catalogue row. +# A nonempty template list also exercises the production filtering contract. +printf '%s\n' 'template/Boilerplate.agda' > "$work/templates.txt" +: > "$work/files.jsonl" +: > "$work/holes.jsonl" +: > "$work/decls.jsonl" +: > "$work/repos-with-status.jsonl" +: > "$work/expected.jsonl" +add_case() { # [candidate paths...] + local name="test/$1" expected=$2 path + shift 2 + jq -cn --arg repo "$name" '{repo:$repo,path:"src/Main.agda",ext:"agda"}' >> "$work/files.jsonl" + jq -cn --arg repo "$name" --arg path "$expected" '{repo:$repo,status_doc:$path}' >> "$work/expected.jsonl" + for path in "$@"; do + jq -cn --arg repo "$name" --arg path "$path" '{repo:$repo,path:$path}' >> "$work/repos-with-status.jsonl" + done +} + +add_case all-ranks docs/status/PROOF-STATUS.adoc \ + docs/proof-debt.adoc docs/PROOF-NEEDS.adoc docs/status/PROOF-STATUS.adoc README.adoc +add_case mixed-case nested/pRoOf-StAtUs.AdOc \ + PROOF-NEEDS.adoc nested/pRoOf-StAtUs.AdOc proof-debt.adoc +# Root paths, ties and duplicates must preserve the selected path. Cases that +# depend on the order of proof-debt and PROOF-NEEDS, or on nesting, are in +# status_doc_rank_test.sh and census_rust_test.sh. +add_case root PROOF-STATUS.adoc PROOF-STATUS.adoc +add_case fallback a/overview.adoc z/overview.adoc a/overview.adoc +add_case same-rank a/PROOF-STATUS.adoc z/PROOF-STATUS.adoc a/PROOF-STATUS.adoc +add_case duplicate PROOF-STATUS.adoc PROOF-STATUS.adoc PROOF-STATUS.adoc +add_case absent '' +# Prefix-related repository names must not share their selected document. +add_case shared docs/PROOF-STATUS.adoc docs/PROOF-STATUS.adoc +add_case shared-child docs/PROOF-DEBT.adoc docs/PROOF-DEBT.adoc +# Status-only repositories do not create census rows. +printf '%s\n' '{"repo":"test/status-only","path":"PROOF-STATUS.adoc"}' >> "$work/repos-with-status.jsonl" + +# Nonzero counters catch accidental changes to the row fold while choosing a +# pointer. Template artefacts contribute neither files nor declarations/holes. +cat >> "$work/files.jsonl" <<'JSONL' +{"repo":"test/all-ranks","path":"tests/Example.lean","ext":"lean"} +{"repo":"test/all-ranks","path":"template/Boilerplate.agda","ext":"agda"} +JSONL +cat >> "$work/decls.jsonl" <<'JSONL' +{"repo":"test/all-ranks","file":"src/Main.agda"} +{"repo":"test/all-ranks","file":"tests/Example.lean"} +{"repo":"test/all-ranks","file":"template/Boilerplate.agda"} +JSONL +for class in hole axiom unsafe policy; do + jq -cn --arg class "$class" '{repo:"test/all-ranks",file:"src/Main.agda",class:$class}' >> "$work/holes.jsonl" + jq -cn --arg class "$class" '{repo:"test/all-ranks",file:"template/Boilerplate.agda",class:$class}' >> "$work/holes.jsonl" +done + +run_rows() { + bash "$repo/scripts/census/build-rows.sh" "$work" "$work/templates.txt" > "$work/actual.json" +} +run_rows +jq -sS 'sort_by(.repo)' "$work/expected.jsonl" > "$work/expected.json" +jq -S 'map({repo,status_doc})' "$work/actual.json" > "$work/pointers.json" +diff -u "$work/expected.json" "$work/pointers.json" || fail 'status precedence or repository isolation' +echo "PASS: $(wc -l < "$work/expected.jsonl") status selection cases, including absent and duplicate candidates" +jq -e ' + (map(.repo) == (map(.repo) | sort)) and + (map(select(.repo == "test/all-ranks")) == [{ + repo:"test/all-ranks", class:"theory", own_files:2, fixture_files:1, + provers:"agda 1, lean 1", declarations:2, holes:1, axioms:1, + unsafe:1, policy:1, status_doc:"docs/status/PROOF-STATUS.adoc" + }]) and + (map(select(.repo != "test/all-ranks")) | all( + .class == "theory" and .own_files == 1 and .fixture_files == 0 and + .provers == "agda 1" and .declarations == 0 and .holes == 0 and + .axioms == 0 and .unsafe == 0 and .policy == 0 + )) +' "$work/actual.json" >/dev/null || fail 'status selection changed census counts or row order' +echo 'PASS: counters, template exclusions, fixtures, and row ordering preserved' +cp "$work/actual.json" "$work/original.json" +# Deliberately reverse all candidates, including ties, to catch first-input wins. +jq -cs '. | reverse[]' "$work/repos-with-status.jsonl" > "$work/reversed.jsonl" +mv "$work/reversed.jsonl" "$work/repos-with-status.jsonl" +run_rows +cmp "$work/original.json" "$work/actual.json" || fail 'candidate input order changed output' +echo 'PASS: reversed status candidates produce byte-identical rows' +: > "$work/repos-with-status.jsonl" +run_rows +jq 'map(.status_doc = "")' "$work/original.json" > "$work/no-status-expected.json" +jq . "$work/actual.json" > "$work/no-status-actual.json" +diff -u "$work/no-status-expected.json" "$work/no-status-actual.json" || fail 'empty status input changed rows' +echo 'PASS: an empty status stream preserves every row with an empty pointer'