fix(proofs): stop claiming SPARK proofs that do not exist; make the proof scaffold compile and fail closed

.gitignore

@@ -123,3 +123,12 @@ dist/
 # ...but never track Idris2 typecheck output. `idris2 --typecheck src/interface/abi.ipkg`
 # writes compiled .ttc/.ttm under build/ttc/; these are generated artifacts.
 /build/ttc/
+docs/man/*.1
+# Coq compiled proof artifacts
+verification/proofs/coq/*.vo
+verification/proofs/coq/*.vok
+verification/proofs/coq/*.vos
+verification/proofs/coq/*.glob
+verification/proofs/coq/.*.aux
+# Agda compiled proof artifacts
+verification/proofs/agda/*.agdai

build/just/proofs.just

@@ -12,126 +12,33 @@
 proof-check-all: proof-check-idris2 proof-check-lean4 proof-check-agda proof-check-coq proof-scan-dangerous
     @echo "=== All proof checks complete ==="
 
-# Check Idris2 proofs (ABI, types, dependent type proofs)
+# Each proof-check-<prover> delegates to scripts/check-proofs.sh, the single
+# source of truth. A missing toolchain is FATAL (never a skip); every module is
+# checked from its own source root; a proof file absent from the prover's
+# manifest (verification/proofs/<prover>/MANIFEST) is an error. See the script
+# header for the four "checks that could not fail" this replaces.
+
+# Check Idris2 proofs (per MANIFEST; fatal if idris2 absent)
 proof-check-idris2:
-    #!/usr/bin/env bash
-    set -euo pipefail
-    echo "=== Checking Idris2 proofs ==="
-    if ! command -v idris2 &>/dev/null; then
-        echo "SKIP: idris2 not installed"
-        exit 0
-    fi
-    ERRORS=0
-    for f in $(find verification/proofs/idris2 -name '*.idr' 2>/dev/null); do
-        echo -n "  Checking $f ... "
-        if idris2 --check "$f" 2>/dev/null; then
-            echo "OK"
-        else
-            echo "FAIL"
-            ERRORS=$((ERRORS + 1))
-        fi
-    done
-    if [ "$ERRORS" -gt 0 ]; then
-        echo "FAIL: $ERRORS Idris2 proof(s) failed"
-        exit 1
-    fi
-    echo "PASS: All Idris2 proofs verified"
+    @bash scripts/check-proofs.sh idris2
 
-# Check Lean4 proofs
+# Check Lean4 proofs (per MANIFEST; fatal if lean absent)
 proof-check-lean4:
-    #!/usr/bin/env bash
-    set -euo pipefail
-    echo "=== Checking Lean4 proofs ==="
-    if ! command -v lean &>/dev/null; then
-        echo "SKIP: lean not installed"
-        exit 0
-    fi
-    ERRORS=0
-    for f in $(find verification/proofs/lean4 -name '*.lean' 2>/dev/null); do
-        echo -n "  Checking $f ... "
-        if lean "$f" 2>/dev/null; then
-            echo "OK"
-        else
-            echo "FAIL"
-            ERRORS=$((ERRORS + 1))
-        fi
-    done
-    if [ "$ERRORS" -gt 0 ]; then
-        echo "FAIL: $ERRORS Lean4 proof(s) failed"
-        exit 1
-    fi
-    echo "PASS: All Lean4 proofs verified"
+    @bash scripts/check-proofs.sh lean4
 
-# Check Agda proofs
+# Check Agda proofs (per MANIFEST; fatal if agda absent)
 proof-check-agda:
-    #!/usr/bin/env bash
-    set -euo pipefail
-    echo "=== Checking Agda proofs ==="
-    if ! command -v agda &>/dev/null; then
-        echo "SKIP: agda not installed"
-        exit 0
-    fi
-    ERRORS=0
-    for f in $(find verification/proofs/agda -name '*.agda' 2>/dev/null); do
-        echo -n "  Checking $f ... "
-        if agda --safe "$f" 2>/dev/null; then
-            echo "OK"
-        else
-            echo "FAIL"
-            ERRORS=$((ERRORS + 1))
-        fi
-    done
-    if [ "$ERRORS" -gt 0 ]; then
-        echo "FAIL: $ERRORS Agda proof(s) failed"
-        exit 1
-    fi
-    echo "PASS: All Agda proofs verified"
+    @bash scripts/check-proofs.sh agda
 
-# Check Coq proofs
+# Check Coq proofs (per MANIFEST; fatal if coqc absent)
 proof-check-coq:
-    #!/usr/bin/env bash
-    set -euo pipefail
-    echo "=== Checking Coq proofs ==="
-    if ! command -v coqc &>/dev/null; then
-        echo "SKIP: coqc not installed"
-        exit 0
-    fi
-    ERRORS=0
-    for f in $(find verification/proofs/coq -name '*.v' 2>/dev/null); do
-        echo -n "  Checking $f ... "
-        if coqc "$f" 2>/dev/null; then
-            echo "OK"
-        else
-            echo "FAIL"
-            ERRORS=$((ERRORS + 1))
-        fi
-    done
-    if [ "$ERRORS" -gt 0 ]; then
-        echo "FAIL: $ERRORS Coq proof(s) failed"
-        exit 1
-    fi
-    echo "PASS: All Coq proofs verified"
+    @bash scripts/check-proofs.sh coq
 
-# Scan for dangerous patterns in proof files (believe_me, sorry, Admitted, etc.)
+# Scan for dangerous constructs USED in proof code (believe_me, sorry, Admitted,
+# postulate, ...). Comments are ignored — a comment naming a banned construct
+# must not trip the gate. See scripts/scan-dangerous.sh.
 proof-scan-dangerous:
-    #!/usr/bin/env bash
-    set -euo pipefail
-    echo "=== Scanning for dangerous patterns in proofs ==="
-    DANGEROUS=0
-    PATTERNS="believe_me|assert_total|postulate|sorry|Admitted|unsafeCoerce|Obj\.magic"
-    for f in $(find verification/proofs -name '*.idr' -o -name '*.lean' -o -name '*.agda' -o -name '*.v' 2>/dev/null); do
-        MATCHES=$(grep -nE "$PATTERNS" "$f" 2>/dev/null || true)
-        if [ -n "$MATCHES" ]; then
-            echo "  DANGEROUS: $f"
-            echo "$MATCHES" | sed 's/^/    /'
-            DANGEROUS=$((DANGEROUS + 1))
-        fi
-    done
-    if [ "$DANGEROUS" -gt 0 ]; then
-        echo "FAIL: $DANGEROUS file(s) contain dangerous patterns"
-        exit 1
-    fi
-    echo "PASS: No dangerous patterns found in proofs"
+    @bash scripts/scan-dangerous.sh
 
 # Show proof status summary
 proof-status:

docs/status/PROOF-NEEDS.adoc

@@ -1,6 +1,6 @@
 // SPDX-License-Identifier: CC-BY-SA-4.0
 // Copyright (c) Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
-// Template: contractiles/docs/status/PROOF-NEEDS.adoc
+// Template: rsr-template-repo/docs/status/PROOF-NEEDS.adoc
 // Authoritative master list: ~/Desktop/PROOF-REQUIREMENTS-MASTER.adoc
 = Proof Requirements — CONTRACTILES
 
@@ -26,7 +26,7 @@
 
 == Mandatory Proofs (All RSR Repos)
 
-These proofs come from the contractiles and MUST be present in every repo:
+These proofs come from the rsr-template-repo and MUST be present in every repo:
 
 === ABI/FFI Boundary Proofs (Idris2)
 
@@ -48,7 +48,7 @@ These proofs come from the contractiles and MUST be present in every repo:
 | # | Proof | Status | File
 
 | TP-1 | Core data type well-formedness | Needed | `verification/proofs/idris2/Types.idr`
-| TP-2 | Public API type safety (exported functions) | Needed | `verification/proofs/lean4/ApiTypes.lean`
+| TP-2 | Public API type safety (exported functions) | Needed | Idris2 (an interface property, policy §1). The shipped `lean4/ApiTypes.lean` is a layout example, not this proof.
 |===
 
 == Project-Specific Proofs
@@ -77,24 +77,25 @@ The following MUST NOT appear anywhere in proof files:
 | `sorry` | Lean4 | Incomplete proof
 | `Admitted` | Coq | Incomplete proof
 | `unsafeCoerce` | Haskell | Unsafe type cast
-| `Obj.magic` | OCaml/AffineScript | Unsafe type cast
+| `Obj.magic` | OCaml/ | Unsafe type cast
 | `unsafe` (unaudited) | Rust | Unsafe block without safety comment
 |===
 
 CI will reject any PR introducing these patterns (enforced by `panic-attack assail`).
 
 == Prover Selection Guide
 
+This table mirrors `3-practice/PROOF-POLICY.adoc` in `hyperpolymath/standards`, which governs. Another tool needs a recorded §4 exception.
+
 [cols="2,2,3", options="header"]
 |===
 | Use Case | Recommended Prover | Why
 
-| ABI/FFI boundaries | *Idris2* | Dependent types model layouts precisely
-| Type system proofs | *Coq* or *Lean4* | Mature proof assistants for metatheory
-| Algebraic properties | *Lean4* | Good mathlib support
-| Inductive/coinductive | *Agda* | Native support for (co)induction
-| Distributed systems | *TLA+* | Model checking for protocols
-| Numerical properties | *Isabelle* | Strong real analysis library
+| Rust code | *Creusot* with Pearlite contracts, and *Verus* | Policy §1.2: on the implementation itself
+| Ada code | *SPARK* | `gnatprove` on code under `SPARK_Mode`
+| APIs, ABIs, interface and engineering properties | *Idris2* | Policy §1: types, layouts, wire formats, protocols
+| Theory (true of any implementation) | *Agda*, rechecked in *Rocq* and *Lean* | Policy §1–§2: Agda is the source; no Mathlib
+| Protocol model checks | *TLA+* | A recorded §4 exception, reported `TESTED` with its bounds
 |===
 
 == Proof File Locations
@@ -104,13 +105,13 @@ verification/proofs/
 ├── idris2/          # Idris2 proofs (ABI, dependent types)
 │   ├── ABI/         # ABI-specific proofs
 │   └── *.idr        # Project-specific Idris2 proofs
-├── lean4/           # Lean4 proofs (algebra, lattices)
+├── lean4/           # Lean recheck legs of agda/ (theory; no Mathlib)
 │   └── *.lean
-├── agda/            # Agda proofs (induction, metatheory)
+├── agda/            # Theory: the source of truth
 │   └── *.agda
-├── coq/             # Coq proofs (type systems, compilation)
+├── coq/             # Rocq recheck legs of agda/ (theory)
 │   └── *.v
-└── tlaplus/         # TLA+ specs (distributed protocols)
+└── tlaplus/         # Recorded §4 exception: protocol model checks (TESTED)
     └── *.tla
 ----
 
@@ -119,4 +120,4 @@ verification/proofs/
 * Master list: `~/Desktop/PROOF-REQUIREMENTS-MASTER.adoc`
 * Proof status tracking: `PROOF-STATUS.adoc` (this repo)
 * Proven library: `proven` repo (Idris2 verified foundations)
-* Template: `contractiles/docs/status/PROOF-NEEDS.adoc`
+* Template: `rsr-template-repo/docs/status/PROOF-NEEDS.adoc`

docs/status/PROOF-STATUS.adoc

@@ -1,26 +1,27 @@
 // SPDX-License-Identifier: CC-BY-SA-4.0
 // Copyright (c) Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
-// Template: contractiles/docs/status/PROOF-STATUS.adoc
+// Template: rsr-template-repo/docs/status/PROOF-STATUS.adoc
 // Tracks proof completion. Requirements defined in PROOF-NEEDS.adoc
 = Proof Status — CONTRACTILES
 
 == Summary
 
-[cols="2,1,1,1,1,1", options="header"]
+[cols="2,1,1,1,1,1,1", options="header"]
 |===
-| Category | Total | Done | In Progress | Blocked | Remaining
-
-| ABI/FFI (ABI) | 5 | 0 | 0 | 0 | 5
-| Typing (TP) | 2 | 0 | 0 | 0 | 2
-| Invariant (INV) | 0 | 0 | 0 | 0 | 0
-| Security (SEC) | 0 | 0 | 0 | 0 | 0
-| Concurrency (CONC) | 0 | 0 | 0 | 0 | 0
-| Algorithm (ALG) | 0 | 0 | 0 | 0 | 0
-| Domain (DOM) | 0 | 0 | 0 | 0 | 0
-| *Total* | *7* | *0* | *0* | *0* | *7*
+| Category | Total | PROVEN | PROVEN-WITH-AXIOMS | TESTED | ASSUMED | OPEN
+
+| ABI/FFI (ABI) | 5 | 0 | 0 | 0 | 0 | 5
+| Typing (TP) | 2 | 0 | 0 | 0 | 0 | 2
+| Invariant (INV) | 0 | 0 | 0 | 0 | 0 | 0
+| Security (SEC) | 0 | 0 | 0 | 0 | 0 | 0
+| Concurrency (CONC) | 0 | 0 | 0 | 0 | 0 | 0
+| Algorithm (ALG) | 0 | 0 | 0 | 0 | 0 | 0
+| Domain (DOM) | 0 | 0 | 0 | 0 | 0 | 0
+| SPARK (Ada runners) | 1 | 0 | 0 | 0 | 0 | 1
+| *Total* | *8* | *0* | *0* | *0* | *0* | *8*
 |===
 
-*Overall*: 0% proven
+*Census*: 0 of 8 obligations `PROVEN`; 8 `OPEN`. Status tokens are the §5 vocabulary of `3-practice/PROOF-POLICY.adoc` (standards). Report a census with its denominator, never a percentage (policy §8.4). Theory theorems also carry a Proof Witness Grade (`PWG-…` or `ungraded`) in a separate field.
 
 == Proofs Done
 
@@ -65,7 +66,8 @@
 | ABI-4 | FFI function return type proofs | ABI | Idris2 | P1 | 2h
 | ABI-5 | C ABI compliance | ABI | Idris2 | P1 | 4h
 | TP-1 | Core data type well-formedness | TP | Idris2 | P1 | 4h
-| TP-2 | Public API type safety | TP | Lean4 | P2 | 4h
+| TP-2 | Public API type safety | TP | Idris2 | P2 | 4h
+| SPARK-1 | `must` runner, `runners/must/src` tree: absence of run-time errors and its twelve `Pre`/`Post` aspects (the diverging `mustfile/src` tree needs its own row if it is kept) | SPARK | SPARK | P2 | not estimated
 |===
 
 == Verification Commands
@@ -99,3 +101,27 @@ panic-attack assail --proofs-only
 
 | 2026-04-04 | Initial proof status tracking | Template
 |===
+
+== SPARK status (checked 2026-11-09)
+
+`runners/must/` carries documents that call its SPARK conversion complete
+(`SPARK-CONVERSION-COMPLETE.md`, `SPARK-STATUS.md` and five
+`SPARK-*-COMPLETE.md`). The Ada sources do not support that. No `.ads`,
+`.adb` or `.gpr` file in `runners/must/src` or `mustfile/src` sets
+`SPARK_Mode`, and there is no `.adc` configuration file, so `gnatprove`
+analyses none of it. The only contract aspects are four `Pre` and eight `Post`
+aspects on the eight bounded-string conversion functions in
+`runners/must/src/must_types.ads`. There are no `Global`, `Depends`,
+`Contract_Cases` or `Loop_Invariant` aspects. The record types whose comments
+say "with SPARK contracts" (`must_types.ads` lines 66–135) carry none.
+Outside SPARK the twelve aspects are run-time assertions at most, not
+discharged proof obligations, so SPARK-1 is `OPEN`, not `PROVEN`. The
+documents carry a status correction at the top and are kept as history.
+
+`runners/must/src` and `mustfile/src` are two diverging implementations, not
+copies. `must.adb`, `must_types.ads` and `must_types.adb` differ: the
+`runners/must` tree uses `Ada.Strings.Bounded`, while `mustfile/src` uses
+indefinite containers and unbounded strings, and has no contract aspects at
+all. A proof about one tree says nothing about the other, so any SPARK work
+must name its tree. Which tree survives belongs to the runner-only
+consolidation of this repository (standards ultraplan Q8).

runners/must/SPARK-CLI-PARSER-COMPLETE.md

@@ -1,3 +1,5 @@
+> **Status correction (2026-11-09).** No Ada source in this repository sets `SPARK_Mode`, so `gnatprove` analyses none of it and nothing here is proved. The only contract aspects are four `Pre` and eight `Post` aspects on the eight bounded-string conversion functions in `runners/must/src/must_types.ads`; outside SPARK they are run-time assertions at most, not discharged proof obligations. Claims of completion in this document are not supported by the code. The proof obligation is `OPEN`: see `docs/status/PROOF-STATUS.adoc` (SPARK status). This document is kept as history.
+
 # CLI_Parser Conversion Complete
 
 **Date:** 2026-02-05

runners/must/SPARK-CONVERSION-COMPLETE.md

@@ -1,3 +1,5 @@
+> **Status correction (2026-11-09).** No Ada source in this repository sets `SPARK_Mode`, so `gnatprove` analyses none of it and nothing here is proved. The only contract aspects are four `Pre` and eight `Post` aspects on the eight bounded-string conversion functions in `runners/must/src/must_types.ads`; outside SPARK they are run-time assertions at most, not discharged proof obligations. Claims of completion in this document are not supported by the code. The proof obligation is `OPEN`: see `docs/status/PROOF-STATUS.adoc` (SPARK status). This document is kept as history.
+
 # SPARK Bounded String Conversion - COMPLETE
 
 **Date:** 2026-02-05

runners/must/SPARK-CONVERSION-SESSION-2026-02-05.md

@@ -1,3 +1,5 @@
+> **Status correction (2026-11-09).** No Ada source in this repository sets `SPARK_Mode`, so `gnatprove` analyses none of it and nothing here is proved. The only contract aspects are four `Pre` and eight `Post` aspects on the eight bounded-string conversion functions in `runners/must/src/must_types.ads`; outside SPARK they are run-time assertions at most, not discharged proof obligations. Claims of completion in this document are not supported by the code. The proof obligation is `OPEN`: see `docs/status/PROOF-STATUS.adoc` (SPARK status). This document is kept as history.
+
 # SPARK Conversion Session Summary
 
 **Date:** 2026-02-05

runners/must/SPARK-MUSTACHE-ENGINE-COMPLETE.md

@@ -1,3 +1,5 @@
+> **Status correction (2026-11-09).** No Ada source in this repository sets `SPARK_Mode`, so `gnatprove` analyses none of it and nothing here is proved. The only contract aspects are four `Pre` and eight `Post` aspects on the eight bounded-string conversion functions in `runners/must/src/must_types.ads`; outside SPARK they are run-time assertions at most, not discharged proof obligations. Claims of completion in this document are not supported by the code. The proof obligation is `OPEN`: see `docs/status/PROOF-STATUS.adoc` (SPARK status). This document is kept as history.
+
 # mustache_engine Conversion Complete
 
 **Date:** 2026-02-05

runners/must/SPARK-REQUIREMENT-CHECKER-COMPLETE.md

@@ -1,3 +1,5 @@
+> **Status correction (2026-11-09).** No Ada source in this repository sets `SPARK_Mode`, so `gnatprove` analyses none of it and nothing here is proved. The only contract aspects are four `Pre` and eight `Post` aspects on the eight bounded-string conversion functions in `runners/must/src/must_types.ads`; outside SPARK they are run-time assertions at most, not discharged proof obligations. Claims of completion in this document are not supported by the code. The proof obligation is `OPEN`: see `docs/status/PROOF-STATUS.adoc` (SPARK status). This document is kept as history.
+
 # requirement_checker Conversion Complete
 
 **Date:** 2026-02-05

runners/must/SPARK-STATUS.md

@@ -1,3 +1,5 @@
+> **Status correction (2026-11-09).** No Ada source in this repository sets `SPARK_Mode`, so `gnatprove` analyses none of it and nothing here is proved. The only contract aspects are four `Pre` and eight `Post` aspects on the eight bounded-string conversion functions in `runners/must/src/must_types.ads`; outside SPARK they are run-time assertions at most, not discharged proof obligations. Claims of completion in this document are not supported by the code. The proof obligation is `OPEN`: see `docs/status/PROOF-STATUS.adoc` (SPARK status). This document is kept as history.
+
 # SPARK Conversion Status
 
 **Date:** 2026-02-05

runners/must/SPARK-TASK-RUNNER-COMPLETE.md

@@ -1,3 +1,5 @@
+> **Status correction (2026-11-09).** No Ada source in this repository sets `SPARK_Mode`, so `gnatprove` analyses none of it and nothing here is proved. The only contract aspects are four `Pre` and eight `Post` aspects on the eight bounded-string conversion functions in `runners/must/src/must_types.ads`; outside SPARK they are run-time assertions at most, not discharged proof obligations. Claims of completion in this document are not supported by the code. The proof obligation is `OPEN`: see `docs/status/PROOF-STATUS.adoc` (SPARK status). This document is kept as history.
+
 # task_runner Conversion Complete
 
 **Date:** 2026-02-05