From 820a77ef5b610016921208e498532b49d6ba5fbd Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 9 Nov 2026 14:41:49 +0000 Subject: [PATCH 1/3] fix(proofs): stop claiming SPARK proofs that do not exist; resync the proof scaffold so it compiles and cannot report a false green MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit SPARK: no .ads/.adb in runners/must/src or mustfile/src contains SPARK_Mode or any contract aspect (Pre, Post, Global, Depends, Contract_Cases, Loop_Invariant), so gnatprove has nothing to analyse. The seven runners/must/SPARK-*.md documents that call the conversion complete now open with a status correction and are kept as history. PROOF-STATUS records the obligation as SPARK-1, OPEN, with the evidence. Proof scaffold, resynced from rsr-template-repo (as verified in hyperpolymath/rsr-template-repo#310): - build/just/proofs.just: the old recipes printed "SKIP: idris2 not installed" and exited 0. They now delegate to scripts/check-proofs.sh, where a missing toolchain fails. - verification/proofs: the stale copies did not compile (Types.idr, ApiTypes.lean); the resynced set does, with MANIFESTs (gated or quarantined), Agda under the PROOF-POLICY §2.1 invocation, and a bounded TLA+ model (TESTED). - PROOF-STATUS / PROOF-NEEDS: §5 status tokens and a census, no percentage; the prover guide mirrors PROOF-POLICY. Checked 2026-11-09: check-proofs.sh passes for idris2 0.7.0, Agda 2.6.3 (stdlib 1.7.3), Coq 8.18.0 and Lean 4.15.0. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01Rp1Fti9phnCG3qrvQJkYEh --- build/just/proofs.just | 129 ++---------- docs/status/PROOF-NEEDS.adoc | 31 +-- docs/status/PROOF-STATUS.adoc | 46 +++-- runners/must/SPARK-CLI-PARSER-COMPLETE.md | 2 + runners/must/SPARK-CONVERSION-COMPLETE.md | 2 + .../SPARK-CONVERSION-SESSION-2026-02-05.md | 2 + .../must/SPARK-MUSTACHE-ENGINE-COMPLETE.md | 2 + .../SPARK-REQUIREMENT-CHECKER-COMPLETE.md | 2 + runners/must/SPARK-STATUS.md | 2 + runners/must/SPARK-TASK-RUNNER-COMPLETE.md | 2 + scripts/check-proofs.sh | 186 ++++++++++++++++++ verification/proofs/README.adoc | 116 +++++++++-- verification/proofs/agda/MANIFEST | 7 + verification/proofs/coq/MANIFEST | 4 + verification/proofs/idris2/ABI/Compliance.idr | 2 +- verification/proofs/idris2/ABI/Foreign.idr | 2 +- verification/proofs/idris2/ABI/Layout.idr | 2 +- verification/proofs/idris2/ABI/Platform.idr | 2 +- verification/proofs/idris2/ABI/Pointers.idr | 2 +- verification/proofs/idris2/MANIFEST | 11 ++ verification/proofs/idris2/Types.idr | 6 +- verification/proofs/lean4/ApiTypes.lean | 5 +- verification/proofs/lean4/MANIFEST | 5 + verification/proofs/lean4/lean-toolchain | 1 + verification/proofs/tlaplus/MC.cfg | 10 + verification/proofs/tlaplus/MC.tla | 14 ++ verification/proofs/tlaplus/StateMachine.tla | 7 +- 27 files changed, 436 insertions(+), 166 deletions(-) create mode 100755 scripts/check-proofs.sh create mode 100644 verification/proofs/agda/MANIFEST create mode 100644 verification/proofs/coq/MANIFEST create mode 100644 verification/proofs/idris2/MANIFEST create mode 100644 verification/proofs/lean4/MANIFEST create mode 100644 verification/proofs/lean4/lean-toolchain create mode 100644 verification/proofs/tlaplus/MC.cfg create mode 100644 verification/proofs/tlaplus/MC.tla diff --git a/build/just/proofs.just b/build/just/proofs.just index b124d7a..dfd6334 100644 --- a/build/just/proofs.just +++ b/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- 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//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: diff --git a/docs/status/PROOF-NEEDS.adoc b/docs/status/PROOF-NEEDS.adoc index 9f62bc5..e85fe80 100644 --- a/docs/status/PROOF-NEEDS.adoc +++ b/docs/status/PROOF-NEEDS.adoc @@ -1,6 +1,6 @@ // SPDX-License-Identifier: CC-BY-SA-4.0 // Copyright (c) Jonathan D.A. Jewell -// 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,7 +77,7 @@ 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 |=== @@ -85,16 +85,17 @@ CI will reject any PR introducing these patterns (enforced by `panic-attack assa == 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` diff --git a/docs/status/PROOF-STATUS.adoc b/docs/status/PROOF-STATUS.adoc index 13c9815..6e3838d 100644 --- a/docs/status/PROOF-STATUS.adoc +++ b/docs/status/PROOF-STATUS.adoc @@ -1,26 +1,27 @@ // SPDX-License-Identifier: CC-BY-SA-4.0 // Copyright (c) Jonathan D.A. Jewell -// 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`, duplicated in `mustfile/src`): absence of run-time errors and its declared contracts | SPARK | SPARK | P2 | not estimated |=== == Verification Commands @@ -99,3 +101,19 @@ 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` or +`.adb` file in `runners/must/src` or `mustfile/src` contains `SPARK_Mode`, and +none carries a contract aspect (`Pre`, `Post`, `Global`, `Depends`, +`Contract_Cases`) or a `Loop_Invariant`; comments that say "SPARK contracts" +have no contract under them. Without `SPARK_Mode`, `gnatprove` has nothing to +analyse, 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` hold two copies of the same Ada runner. +Which one survives belongs to the runner-only consolidation of this repository +(standards ultraplan Q8). diff --git a/runners/must/SPARK-CLI-PARSER-COMPLETE.md b/runners/must/SPARK-CLI-PARSER-COMPLETE.md index 67b58a4..2fd6792 100644 --- a/runners/must/SPARK-CLI-PARSER-COMPLETE.md +++ b/runners/must/SPARK-CLI-PARSER-COMPLETE.md @@ -1,3 +1,5 @@ +> **Status correction (2026-11-09).** No Ada source in this repository contains `SPARK_Mode` or any contract aspect (`Pre`, `Post`, `Global`, `Depends`, `Loop_Invariant`), so `gnatprove` has nothing to analyse and nothing here is proved. 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 diff --git a/runners/must/SPARK-CONVERSION-COMPLETE.md b/runners/must/SPARK-CONVERSION-COMPLETE.md index f65917c..6eb15b1 100644 --- a/runners/must/SPARK-CONVERSION-COMPLETE.md +++ b/runners/must/SPARK-CONVERSION-COMPLETE.md @@ -1,3 +1,5 @@ +> **Status correction (2026-11-09).** No Ada source in this repository contains `SPARK_Mode` or any contract aspect (`Pre`, `Post`, `Global`, `Depends`, `Loop_Invariant`), so `gnatprove` has nothing to analyse and nothing here is proved. 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 diff --git a/runners/must/SPARK-CONVERSION-SESSION-2026-02-05.md b/runners/must/SPARK-CONVERSION-SESSION-2026-02-05.md index ac8aab6..1810dea 100644 --- a/runners/must/SPARK-CONVERSION-SESSION-2026-02-05.md +++ b/runners/must/SPARK-CONVERSION-SESSION-2026-02-05.md @@ -1,3 +1,5 @@ +> **Status correction (2026-11-09).** No Ada source in this repository contains `SPARK_Mode` or any contract aspect (`Pre`, `Post`, `Global`, `Depends`, `Loop_Invariant`), so `gnatprove` has nothing to analyse and nothing here is proved. 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 diff --git a/runners/must/SPARK-MUSTACHE-ENGINE-COMPLETE.md b/runners/must/SPARK-MUSTACHE-ENGINE-COMPLETE.md index a8eef95..d6ac495 100644 --- a/runners/must/SPARK-MUSTACHE-ENGINE-COMPLETE.md +++ b/runners/must/SPARK-MUSTACHE-ENGINE-COMPLETE.md @@ -1,3 +1,5 @@ +> **Status correction (2026-11-09).** No Ada source in this repository contains `SPARK_Mode` or any contract aspect (`Pre`, `Post`, `Global`, `Depends`, `Loop_Invariant`), so `gnatprove` has nothing to analyse and nothing here is proved. 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 diff --git a/runners/must/SPARK-REQUIREMENT-CHECKER-COMPLETE.md b/runners/must/SPARK-REQUIREMENT-CHECKER-COMPLETE.md index 895e816..922bdd8 100644 --- a/runners/must/SPARK-REQUIREMENT-CHECKER-COMPLETE.md +++ b/runners/must/SPARK-REQUIREMENT-CHECKER-COMPLETE.md @@ -1,3 +1,5 @@ +> **Status correction (2026-11-09).** No Ada source in this repository contains `SPARK_Mode` or any contract aspect (`Pre`, `Post`, `Global`, `Depends`, `Loop_Invariant`), so `gnatprove` has nothing to analyse and nothing here is proved. 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 diff --git a/runners/must/SPARK-STATUS.md b/runners/must/SPARK-STATUS.md index 7cbb6ba..07dfc3f 100644 --- a/runners/must/SPARK-STATUS.md +++ b/runners/must/SPARK-STATUS.md @@ -1,3 +1,5 @@ +> **Status correction (2026-11-09).** No Ada source in this repository contains `SPARK_Mode` or any contract aspect (`Pre`, `Post`, `Global`, `Depends`, `Loop_Invariant`), so `gnatprove` has nothing to analyse and nothing here is proved. 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 diff --git a/runners/must/SPARK-TASK-RUNNER-COMPLETE.md b/runners/must/SPARK-TASK-RUNNER-COMPLETE.md index b6f754d..0fe922f 100644 --- a/runners/must/SPARK-TASK-RUNNER-COMPLETE.md +++ b/runners/must/SPARK-TASK-RUNNER-COMPLETE.md @@ -1,3 +1,5 @@ +> **Status correction (2026-11-09).** No Ada source in this repository contains `SPARK_Mode` or any contract aspect (`Pre`, `Post`, `Global`, `Depends`, `Loop_Invariant`), so `gnatprove` has nothing to analyse and nothing here is proved. 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 diff --git a/scripts/check-proofs.sh b/scripts/check-proofs.sh new file mode 100755 index 0000000..80d1914 --- /dev/null +++ b/scripts/check-proofs.sh @@ -0,0 +1,186 @@ +#!/usr/bin/env bash +# SPDX-License-Identifier: MPL-2.0 +# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +# +# check-proofs.sh prover in: idris2 | lean4 | agda | coq +# +# The single source of truth for "do the proofs in this repo compile?". +# build/just/proofs.just calls this (`just proof-check-`), and CI should +# too, so a green local run and a green CI run mean the same thing. +# +# It replaces four separate "checks that could not fail" that let non-compiling +# proofs sit in estate repos for months while every status file said "proved": +# +# 1. `command -v || { echo SKIP; exit 0; }` — a MISSING TOOLCHAIN +# reported success. A gate that cannot run must never report OK: it +# manufactures false confidence, which is worse than having no gate. +# 2. ` --check ` — Idris2 (and friends) derive the +# expected module name from the path they are handed, so a module checked +# from the wrong directory fails on a name mismatch rather than its real +# errors, and verdicts invert. Every module here is checked from its own +# SOURCE ROOT (declared in the MANIFEST). +# 3. Path-filtered CI that only looked at one directory — nothing checked the +# rest. Here, a proof file present on disk but absent from the MANIFEST is +# an ERROR, so new proofs are gated by default, not by remembering. +# 4. `idris2 --check X && ok` — `idris2 --check` EXITS 0 ON A MISSING IMPORT +# (verified against 0.7.0) while printing `Error: ...`. Testing the exit +# code alone is unsound; for idris2 we require exit 0 AND no `Error:` line. +# +# They share one shape: a null check that emits reassuring text. If you extend +# this script, the test to apply is not "does it pass?" but "have I watched it +# fail?". +# +# CONVENTION: proofs live under verification/proofs// ; the MANIFEST for +# a prover is verification/proofs//MANIFEST, one entry per line: +# +# ||gated|quarantine| +# +# source-root : directory the prover is invoked from, chosen so the module's +# declared name matches its path (getting this wrong is hole #2). +# gated : MUST compile. A failure fails this script and CI. +# quarantine : known-broken, tracked in docs/status/ROADMAP.adoc. Must CONTINUE to fail; +# if one starts compiling the script fails and tells you to +# promote it, so the list cannot rot into a permanent excuse. +# +# Blank lines and lines starting with # are ignored. +# +# Exit: 0 = every gated module compiles AND every quarantined module still fails +# AND every proof file on disk is listed; 1 = otherwise; 2 = misuse. + +set -euo pipefail + +PROVER="${1:-}" +case "$PROVER" in + idris2|lean4|agda|coq) ;; + *) echo "usage: $(basename "$0") " >&2; exit 2 ;; +esac + +# This script lives in /scripts/ ; run everything from the repo root. +cd "$(dirname "${BASH_SOURCE[0]}")/.." +ROOT="$PWD" +PROOF_DIR="verification/proofs/$PROVER" +MANIFEST_FILE="$PROOF_DIR/MANIFEST" + +# --- per-prover configuration ------------------------------------------------- +# CMD : executable that must be on PATH (absent => FAIL, never skip). +# EXT : file extension, for the "unlisted proof" coverage scan. +# ERROR_RE : if non-empty, output must not match it even when the exit code is 0. +# Only idris2 needs this (its --check exits 0 on a missing import); +# for lean4 it is a harmless belt-and-braces guard. +case "$PROVER" in + idris2) CMD=idris2; EXT=idr; ERROR_RE='^Error:' ;; + lean4) CMD=lean; EXT=lean; ERROR_RE='error:' ;; + agda) CMD=agda; EXT=agda; ERROR_RE='' ;; + coq) CMD=coqc; EXT=v; ERROR_RE='' ;; +esac + +check_one() { + # $1 source-root (rel to ROOT), $2 module (rel to source-root). + # Sets LAST_OUT to the tool output on failure; returns 0 iff the module compiles. + local root="$1" rel="$2" out rc + set +e + case "$PROVER" in + idris2) out="$(cd "$ROOT/$root" && idris2 --check "$rel" 2>&1)"; rc=$? ;; + lean4) out="$(cd "$ROOT/$root" && lean "$rel" 2>&1)"; rc=$? ;; + # Canonical theory invocation, PROOF-POLICY §2.1 (standards). Do not weaken. + agda) out="$(cd "$ROOT/$root" && agda --safe --without-K --cubical-compatible "$rel" 2>&1)"; rc=$? ;; + coq) out="$(cd "$ROOT/$root" && coqc "$rel" 2>&1)"; rc=$? ;; + esac + set -e + if [ "$rc" -eq 0 ] && { [ -z "$ERROR_RE" ] || ! grep -qE "$ERROR_RE" <<<"$out"; }; then + LAST_OUT=""; return 0 + fi + LAST_OUT="$out"; return 1 +} + +echo "=== $PROVER proof check ===" + +# --- toolchain: absent means FAIL, never skip --------------------------------- +if ! command -v "$CMD" >/dev/null 2>&1; then + { + echo "FAIL: '$CMD' not found on PATH." + echo + echo "This is deliberately fatal. The previous recipe did 'exit 0' here with" + echo "\"SKIP: $CMD not installed\", so every $PROVER proof reported green on any" + echo "machine that could not check it. Install the $PROVER toolchain, or run" + echo "this in CI where the workflow installs it." + } >&2 + exit 1 +fi +"$CMD" --version 2>/dev/null | head -1 || true +echo + +# --- a repo with proofs but no MANIFEST is itself a failure ------------------- +if [ ! -f "$MANIFEST_FILE" ]; then + if [ -d "$PROOF_DIR" ] && [ -n "$(find "$PROOF_DIR" -name "*.$EXT" 2>/dev/null)" ]; then + echo "FAIL: $PROOF_DIR contains .$EXT proofs but has no MANIFEST." >&2 + echo " Create $MANIFEST_FILE listing each as 'gated' or 'quarantine'." >&2 + exit 1 + fi + echo "no $PROOF_DIR/*.$EXT proofs and no MANIFEST — nothing to check." + exit 0 +fi + +fails=0 +unexpected_pass=0 +listed_tmp="$(mktemp)" +trap 'rm -f "$listed_tmp"' EXIT + +while IFS='|' read -r root rel status note; do + # skip blank lines and comments + [ -z "${root// }" ] && continue + case "${root#"${root%%[![:space:]]*}"}" in \#*) continue ;; esac + printf ' %-30s %-24s ' "$root" "$rel" + echo "$root/$rel" >>"$listed_tmp" + if check_one "$root" "$rel"; then + if [ "$status" = gated ]; then + echo "PASS" + else + echo "PASS -- UNEXPECTED (quarantined module now compiles)" + echo " Promote '$rel' to 'gated' in $MANIFEST_FILE and update docs/status/ROADMAP.adoc." + unexpected_pass=$((unexpected_pass + 1)) + fi + else + if [ "$status" = gated ]; then + echo "FAIL" + printf '%s\n' "${LAST_OUT//$'\n'/$'\n '}" | sed '1s/^/ /' + fails=$((fails + 1)) + else + echo "fail (quarantined, expected)" + [ -n "${note// }" ] && echo " reason:$note" + fi + fi +done < "$MANIFEST_FILE" + +# --- coverage: every proof on disk must be listed ----------------------------- +# The anti-recurrence rule: proofs went unchecked for months because nothing +# forced them onto anyone's list. A file absent from the MANIFEST is an error. +echo +echo "=== manifest coverage ($PROOF_DIR) ===" +listed="$(sort -u "$listed_tmp")" +found="$(cd "$ROOT" && find "$PROOF_DIR" -name "*.$EXT" -not -path '*/build/*' 2>/dev/null | sort)" +unlisted="$(comm -13 <(printf '%s\n' "$listed") <(printf '%s\n' "$found") || true)" +# A listed module is stale when its file is absent. Entries may sit outside +# $PROOF_DIR (for example the coaptation core), so test the path itself. +missing="$(while IFS= read -r p; do [ -n "$p" ] && [ ! -f "$ROOT/$p" ] && echo "$p"; done <<<"$listed" || true)" + +if [ -n "${unlisted//[[:space:]]/}" ]; then + echo "FAIL: .$EXT proofs on disk but absent from $MANIFEST_FILE:" + printf ' %s\n' $unlisted + echo " List each as 'gated' or 'quarantine'; new proofs are gated by default." + fails=$((fails + 1)) +fi +if [ -n "${missing//[[:space:]]/}" ]; then + echo "FAIL: MANIFEST lists modules that do not exist (stale entries):" + printf ' %s\n' $missing + fails=$((fails + 1)) +fi +[ -z "${unlisted//[[:space:]]/}${missing//[[:space:]]/}" ] && \ + echo " all $(printf '%s\n' "$found" | grep -c .) .$EXT file(s) accounted for" + +echo +if [ "$fails" -gt 0 ] || [ "$unexpected_pass" -gt 0 ]; then + echo "RESULT: FAIL ($fails failure(s), $unexpected_pass unexpected pass(es))" + exit 1 +fi +echo "RESULT: PASS -- gated modules compile; quarantined modules still fail as recorded" diff --git a/verification/proofs/README.adoc b/verification/proofs/README.adoc index eb22d4c..b228c0f 100644 --- a/verification/proofs/README.adoc +++ b/verification/proofs/README.adoc @@ -2,14 +2,85 @@ // Copyright (c) Jonathan D.A. Jewell = Formal Verification Proofs -This directory contains formal proofs organised by proof assistant. +Which prover carries which obligation is set estate-wide by the proof policy, +`3-practice/PROOF-POLICY.adoc` in `hyperpolymath/standards`. Read it there; +this page only maps it onto this directory. -== Directory Structure +== Which prover for which obligation + +[cols="1,1,2",options="header"] +|=== +|Code or obligation |Verifier |Where it lives + +|Rust code +|*Creusot* +|On the Rust code itself (contracts in the crate), not in this directory. + +|Ada code +|*SPARK* +|On the Ada code itself, checked by `gnatprove`. + +|APIs, ABIs and engineering properties +|*Idris2* +|`idris2/` (the ABI proofs are mandatory). + +|Theory +|*Agda*, rechecked in *Rocq* and *Lean* +|`agda/` is the source of truth; `coq/` and `lean4/` hold the recheck legs +(Dedukti transport first, hand re-proof as the fallback; no Mathlib). +|=== + +Statements about one repository's types, functions or wire formats are +engineering (Idris2). Statements that would hold for any implementation are +theory (Agda). Behaviour of first-party Rust or Ada code (pre- and +postconditions, loop invariants, absence of run-time errors) is proved with +Creusot or SPARK on that code, not restated in Idris2. + +Another tool only where it is plainly the right one, recorded beside the +artefact and in `docs/status/PROOF-STATUS.adoc` (policy §4). `tlaplus/` is +such an exception: a finite model check is reported as `TESTED`, with its +bounds. For Rust, *Kani* (unsafe and FFI seams, reported `TESTED` with +bounds) and *Aeneas* (Rust that implements an Agda-proved theorem) are +standing exceptions that run alongside Creusot, never instead of it. + +== Proof grades + +The only estate proof grade is the *Proof Witness Grade* (PWG) of policy §8. +It applies to theory theorems: + +* `PWG-3` means the Agda proof checks under the canonical invocation. +* `PWG-2i` adds one recheck leg (Rocq or Lean) that counts. +* `PWG-2ii` means both legs count, which discharges the policy's recheck + obligation. +* `PWG-1` adds a current receipt, per commit, from a pinned headless + checker for every witness. + +A leg counts only when it is kernel-checked and its statement +correspondence is `RECONCILED`. Grades are derived from receipts and the +correspondence records, never asserted. Record them in +`docs/status/PROOF-STATUS.adoc` beside the §5 status tokens, in a separate +field. + +Always write the `PWG-` prefix. A bare "Grade 2" collides with the CRG, +TRG, ARG and FRG letter grades. Publish counts as a census with their +denominator, never as a percentage. + +== Third-party code + +Dependencies (crates, libraries, vendored or forked code) are not converted, +re-proved or annotated to meet this policy. Where a proof here relies on a +dependency's behaviour, state that reliance as a trusted boundary +specification and record it as `ASSUMED`, with the dependency and version, +in `docs/status/PROOF-STATUS.adoc`. When choosing between dependencies that +fit equally well, prefer one that carries its own verification. This is a +preference, not a gate. + +== Directory structure [source] ---- proofs/ -├── idris2/ # Idris2 proofs (ABI, dependent types) +├── idris2/ # Engineering: ABI and interface contracts │ ├── ABI/ # ABI-specific proofs (mandatory) │ │ ├── Pointers.idr # Non-null pointer safety │ │ ├── Layout.idr # Memory layout correctness @@ -17,17 +88,27 @@ proofs/ │ │ ├── Foreign.idr # FFI return type proofs │ │ └── Compliance.idr # C ABI compliance │ └── Types.idr # Core data type well-formedness -├── lean4/ # Lean4 proofs (algebra, lattices) -│ └── ApiTypes.lean -├── agda/ # Agda proofs (induction, metatheory) +├── agda/ # Theory: the source of truth goes here │ └── Properties.agda -├── coq/ # Coq proofs (type systems, compilation) +├── coq/ # Theory: Rocq recheck legs of agda/ go here │ └── TypeSafety.v -└── tlaplus/ # TLA+ specs (distributed protocols) +├── lean4/ # Theory: Lean recheck legs of agda/ go here +│ └── ApiTypes.lean +└── tlaplus/ # Recorded exception: protocol model checks (TESTED) └── StateMachine.tla ---- -== Verification Commands +Each prover directory carries a `MANIFEST` read by `scripts/check-proofs.sh`. + +The files the template ships in these directories (`Properties.agda`, +`TypeSafety.v`, `ApiTypes.lean`, `Types.idr`, the `ABI/` modules, +`StateMachine.tla`) are *layout examples, not evidence*. Several have never +compiled and sit as `quarantine` in their `MANIFEST`; `TypeSafety.v` and +`ApiTypes.lean` are not rechecks of `Properties.agda`. A repository created +from the template replaces them with its own proofs or deletes them, and +never counts them in `docs/status/PROOF-STATUS.adoc`. + +== Verification commands [source,bash] ---- @@ -38,7 +119,7 @@ just proof-check-agda # Agda only just proof-check-coq # Coq only ---- -== Banned Patterns +== Banned patterns The following MUST NOT appear in any proof file: @@ -51,10 +132,13 @@ The following MUST NOT appear in any proof file: CI enforces this via `panic-attack assail --proofs-only`. -== Adding New Proofs +== Adding new proofs -1. Choose the appropriate prover (see PROOF-NEEDS.md) -2. Create the `.idr`/`.lean`/`.agda`/`.v`/`.tla` file in the right directory -3. Ensure `%default total` (Idris2) or equivalent -4. Run the verification command -5. Update PROOF-STATUS.md +1. Classify the obligation with the table above and record it in + `docs/status/PROOF-NEEDS.adoc`. +2. Put Rust and Ada proofs on the code; put the rest in the matching + directory here. +3. Ensure `%default total` (Idris2) or the equivalent. +4. Run the verification command. +5. Update `docs/status/PROOF-STATUS.adoc`, including the recheck legs of any + theory proof and any `ASSUMED` boundary specifications. diff --git a/verification/proofs/agda/MANIFEST b/verification/proofs/agda/MANIFEST new file mode 100644 index 0000000..90c2b15 --- /dev/null +++ b/verification/proofs/agda/MANIFEST @@ -0,0 +1,7 @@ +# Agda proof manifest — read by scripts/check-proofs.sh agda +# Format: ||gated|quarantine| +# Invocation: agda --safe --without-K --cubical-compatible (PROOF-POLICY §2.1). +# Ground-truthed 2026-11-09 with Agda 2.6.3 and agda-stdlib 1.7.3 (Ubuntu 24.04 +# packages). The earlier 2026-07-17 `agda --safe` result is historical evidence +# only (§2.1), not a receipt for this profile. +verification/proofs/agda|Properties.agda|gated| compiles under the §2.1 canonical invocation diff --git a/verification/proofs/coq/MANIFEST b/verification/proofs/coq/MANIFEST new file mode 100644 index 0000000..aa71524 --- /dev/null +++ b/verification/proofs/coq/MANIFEST @@ -0,0 +1,4 @@ +# Coq proof manifest — read by scripts/check-proofs.sh coq +# Format: ||gated|quarantine| +# Ground-truthed 2026-07-17 with coqc. +verification/proofs/coq|TypeSafety.v|gated| compiles under `coqc` diff --git a/verification/proofs/idris2/ABI/Compliance.idr b/verification/proofs/idris2/ABI/Compliance.idr index b94a5db..ee5efdd 100644 --- a/verification/proofs/idris2/ABI/Compliance.idr +++ b/verification/proofs/idris2/ABI/Compliance.idr @@ -3,7 +3,7 @@ -- -- ABI Proof: C ABI compliance -- Proves that struct layouts are C ABI compliant. --- All proofs MUST be constructive (no believe_me, no assert_total). +-- All proofs MUST be constructive and total; proof escape hatches are forbidden. module ABI.Compliance diff --git a/verification/proofs/idris2/ABI/Foreign.idr b/verification/proofs/idris2/ABI/Foreign.idr index 1e550dd..6c83435 100644 --- a/verification/proofs/idris2/ABI/Foreign.idr +++ b/verification/proofs/idris2/ABI/Foreign.idr @@ -3,7 +3,7 @@ -- -- ABI Proof: FFI function return type proofs -- Proves that all FFI functions return expected types. --- All proofs MUST be constructive (no believe_me, no assert_total). +-- All proofs MUST be constructive and total; proof escape hatches are forbidden. module ABI.Foreign diff --git a/verification/proofs/idris2/ABI/Layout.idr b/verification/proofs/idris2/ABI/Layout.idr index 9040a5e..f0935ae 100644 --- a/verification/proofs/idris2/ABI/Layout.idr +++ b/verification/proofs/idris2/ABI/Layout.idr @@ -3,7 +3,7 @@ -- -- ABI Proof: Memory layout correctness -- Proves struct size, alignment, and padding properties. --- All proofs MUST be constructive (no believe_me, no assert_total). +-- All proofs MUST be constructive and total; proof escape hatches are forbidden. module ABI.Layout diff --git a/verification/proofs/idris2/ABI/Platform.idr b/verification/proofs/idris2/ABI/Platform.idr index a8d6b94..0b5ab10 100644 --- a/verification/proofs/idris2/ABI/Platform.idr +++ b/verification/proofs/idris2/ABI/Platform.idr @@ -3,7 +3,7 @@ -- -- ABI Proof: Platform-specific type size proofs -- Proves that C type sizes are correct per platform. --- All proofs MUST be constructive (no believe_me, no assert_total). +-- All proofs MUST be constructive and total; proof escape hatches are forbidden. module ABI.Platform diff --git a/verification/proofs/idris2/ABI/Pointers.idr b/verification/proofs/idris2/ABI/Pointers.idr index 31b6c5f..310c484 100644 --- a/verification/proofs/idris2/ABI/Pointers.idr +++ b/verification/proofs/idris2/ABI/Pointers.idr @@ -3,7 +3,7 @@ -- -- ABI Proof: Non-null pointer safety -- Template proof — customise for your project's pointer types. --- All proofs MUST be constructive (no believe_me, no assert_total). +-- All proofs MUST be constructive and total; proof escape hatches are forbidden. module ABI.Pointers diff --git a/verification/proofs/idris2/MANIFEST b/verification/proofs/idris2/MANIFEST new file mode 100644 index 0000000..1b85506 --- /dev/null +++ b/verification/proofs/idris2/MANIFEST @@ -0,0 +1,11 @@ +# Idris2 proof manifest — read by scripts/check-proofs.sh idris2 +# Format: ||gated|quarantine| +# gated = must compile. quarantine = known-broken, must keep failing. +# Ground-truthed 2026-07-17 with idris2 0.7.0 (developer/tools/opt/pack); +# re-checked 2026-11-09 with idris2 0.7.0 built from the v0.7.0 tag. +verification/proofs/idris2|ABI/Foreign.idr|gated| the one shipped Idris2 module that compiles — real content, not a stub +verification/proofs/idris2|Types.idr|gated| compiles since it imports Data.Nat (re-checked 2026-11-09) +verification/proofs/idris2|ABI/Layout.idr|quarantine| Undefined name NonZero (needs Data.Nat); then a genuine unification failure (S ?x vs f .fieldAlignment) +verification/proofs/idris2|ABI/Platform.idr|quarantine| Undefined name LTE (needs Data.Nat); then Undefined name lteRefl +verification/proofs/idris2|ABI/Pointers.idr|quarantine| .nonNull declared at quantity 0 (erased) yet projected into a value position, plus a unification failure — design decision, not a typo +verification/proofs/idris2|ABI/Compliance.idr|quarantine| depends on quarantined ABI.Layout / ABI.Platform diff --git a/verification/proofs/idris2/Types.idr b/verification/proofs/idris2/Types.idr index cc7cce8..e89a852 100644 --- a/verification/proofs/idris2/Types.idr +++ b/verification/proofs/idris2/Types.idr @@ -3,10 +3,12 @@ -- -- Typing Proof: Core data type well-formedness -- Template — replace with your project's core types. --- All proofs MUST be constructive (no believe_me, no assert_total). +-- All proofs MUST be constructive and total; proof escape hatches are forbidden. module Types +import Data.Nat + %default total ||| Example: A bounded natural number (0 to max). @@ -15,7 +17,7 @@ public export record Bounded (max : Nat) where constructor MkBounded value : Nat - {auto 0 inBounds : LTE value max} + {auto inBounds : LTE value max} ||| Proof that a Bounded value is always <= max. export diff --git a/verification/proofs/lean4/ApiTypes.lean b/verification/proofs/lean4/ApiTypes.lean index 9ed78b7..f02f259 100644 --- a/verification/proofs/lean4/ApiTypes.lean +++ b/verification/proofs/lean4/ApiTypes.lean @@ -29,6 +29,7 @@ namespace ApiResult cases r with | ok v => simp [map, Function.comp] | error c m => simp [map] +end ApiResult -- Example: Bounded confidence value (0.0 to 1.0 modelled as Nat/1000) -- Replace with your project's numeric invariants @@ -36,9 +37,9 @@ structure BoundedNat (max : Nat) where val : Nat le_max : val ≤ max -theorem bounded_nat_le (b : BoundedNat max) : b.val ≤ max := +theorem bounded_nat_le {max : Nat} (b : BoundedNat max) : b.val ≤ max := b.le_max -- Proof: zero is always bounded -def zeroBounded (h : 0 < max) : BoundedNat max := +def zeroBounded {max : Nat} (h : 0 < max) : BoundedNat max := ⟨0, Nat.zero_le max⟩ diff --git a/verification/proofs/lean4/MANIFEST b/verification/proofs/lean4/MANIFEST new file mode 100644 index 0000000..7069431 --- /dev/null +++ b/verification/proofs/lean4/MANIFEST @@ -0,0 +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); +# re-checked 2026-11-09 with the v4.15.0 release archive. +verification/proofs/lean4|ApiTypes.lean|gated| compiles (a layout example; not a recheck leg of agda/Properties.agda) diff --git a/verification/proofs/lean4/lean-toolchain b/verification/proofs/lean4/lean-toolchain new file mode 100644 index 0000000..d0eb99f --- /dev/null +++ b/verification/proofs/lean4/lean-toolchain @@ -0,0 +1 @@ +leanprover/lean4:v4.15.0 diff --git a/verification/proofs/tlaplus/MC.cfg b/verification/proofs/tlaplus/MC.cfg new file mode 100644 index 0000000..f01ba02 --- /dev/null +++ b/verification/proofs/tlaplus/MC.cfg @@ -0,0 +1,10 @@ +\* SPDX-License-Identifier: MPL-2.0 +\* Run: java -cp tla2tools.jar tlc2.TLC -workers auto MC +SPECIFICATION Spec +CONSTANT MaxRequests = 3 +CONSTRAINT Bound +INVARIANT TypeInvariant +INVARIANT ProcessedMonotonic +INVARIANT QueueBounded +PROPERTY NoSkipStates +PROPERTY EventualCompletion diff --git a/verification/proofs/tlaplus/MC.tla b/verification/proofs/tlaplus/MC.tla new file mode 100644 index 0000000..75feb1e --- /dev/null +++ b/verification/proofs/tlaplus/MC.tla @@ -0,0 +1,14 @@ +---------------------------- MODULE MC ---------------------------- +(* SPDX-License-Identifier: MPL-2.0 *) +(* Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) *) +(* *) +(* Bounded model for TLC. StateMachine's `processed` counter grows *) +(* without limit, so TLC cannot finish on the spec alone. This module *) +(* bounds it. A result here is TESTED with these bounds (PROOF-POLICY *) +(* §5), never PROVEN. Liveness checked under a state constraint is a *) +(* weak result: TLC prunes behaviours at the bound. *) +EXTENDS StateMachine + +MaxProcessed == 6 +Bound == processed <= MaxProcessed +===================================================================== diff --git a/verification/proofs/tlaplus/StateMachine.tla b/verification/proofs/tlaplus/StateMachine.tla index f348494..fdbc902 100644 --- a/verification/proofs/tlaplus/StateMachine.tla +++ b/verification/proofs/tlaplus/StateMachine.tla @@ -4,7 +4,12 @@ (* *) (* TLA+ Specification Template: State Machine *) (* Replace with your project's distributed protocol or state machine. *) -(* Use TLC model checker to verify properties. *) +(* Use TLC model checker to verify properties: see MC.tla and MC.cfg. *) +(* *) +(* PROOF-POLICY §4 exception (standards): TLA+ is used because these *) +(* obligations are temporal properties of a state machine, which a finite *) +(* model check states directly; Idris2 would need a trace semantics first. *) +(* Results are TESTED with the bounds in MC.tla / MC.cfg, never PROVEN. *) (* *) (* Example: A simple request pipeline with safety properties. *) (* Replace States, Init, Next with your project's actual states. *) From 8d2be1159ad6f6c51c6b34de82a5c7bd8514ad49 Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 9 Nov 2026 15:31:27 +0000 Subject: [PATCH 2/3] fix(proofs): correct the SPARK wording (twelve Pre/Post aspects exist); close the gate's fail-open paths Review (CodeRabbit) on this PR, each finding checked against the code: - The correction banners and PROOF-STATUS said no contract aspect exists. That was wrong: runners/must/src/must_types.ads has four Pre and eight Post aspects on its eight bounded-string conversion functions. Nothing sets SPARK_Mode (no .ads/.adb/.gpr, no .adc), so gnatprove analyses none of it and SPARK-1 stays OPEN; the wording now says exactly that. - runners/must/src and mustfile/src are diverging implementations, not copies (bounded strings vs indefinite containers and unbounded strings; must.adb and must_types.* differ). PROOF-STATUS and the SPARK-1 row now say so and require SPARK work to name its tree. - proof-scan-dangerous called scripts/scan-dangerous.sh, which the resync left out; added from the template. - Ported from hyperpolymath/rsr-template-repo#310 (d887c48): every gated module must also pass scan-dangerous.sh (lean exits 0 on `sorry`, coqc on `Admitted`); an unknown MANIFEST status fails instead of reading as quarantine; ProcessedMonotonic is now an action property ([][processed' >= processed]_processed) with ProcessedNonNegative kept as the invariant; EventualCompletion no longer claims per-request completion; README maps Rust to Creusot/Pearlite and Verus and gives the TLC command, since check-proofs.sh does not run tlaplus/. - .gitignore: the template's Coq and Agda build-artifact entries. Checked: all four prover gates and scan-dangerous.sh pass; TLC 1.8.0 passes MC.cfg. The negative controls were run on the template copy of the same scripts. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01Rp1Fti9phnCG3qrvQJkYEh --- .gitignore | 9 +++ docs/status/PROOF-STATUS.adoc | 32 +++++--- runners/must/SPARK-CLI-PARSER-COMPLETE.md | 2 +- runners/must/SPARK-CONVERSION-COMPLETE.md | 2 +- .../SPARK-CONVERSION-SESSION-2026-02-05.md | 2 +- .../must/SPARK-MUSTACHE-ENGINE-COMPLETE.md | 2 +- .../SPARK-REQUIREMENT-CHECKER-COMPLETE.md | 2 +- runners/must/SPARK-STATUS.md | 2 +- runners/must/SPARK-TASK-RUNNER-COMPLETE.md | 2 +- scripts/check-proofs.sh | 33 +++++--- scripts/scan-dangerous.sh | 80 +++++++++++++++++++ verification/proofs/README.adoc | 26 +++++- verification/proofs/tlaplus/MC.cfg | 5 +- verification/proofs/tlaplus/StateMachine.tla | 12 ++- 14 files changed, 174 insertions(+), 37 deletions(-) create mode 100755 scripts/scan-dangerous.sh diff --git a/.gitignore b/.gitignore index 87e91e8..3e2a163 100644 --- a/.gitignore +++ b/.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 diff --git a/docs/status/PROOF-STATUS.adoc b/docs/status/PROOF-STATUS.adoc index 6e3838d..e07fc75 100644 --- a/docs/status/PROOF-STATUS.adoc +++ b/docs/status/PROOF-STATUS.adoc @@ -67,7 +67,7 @@ | 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 | Idris2 | P2 | 4h -| SPARK-1 | `must` runner (`runners/must/src`, duplicated in `mustfile/src`): absence of run-time errors and its declared contracts | SPARK | SPARK | P2 | not estimated +| 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 @@ -106,14 +106,22 @@ panic-attack assail --proofs-only `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` or -`.adb` file in `runners/must/src` or `mustfile/src` contains `SPARK_Mode`, and -none carries a contract aspect (`Pre`, `Post`, `Global`, `Depends`, -`Contract_Cases`) or a `Loop_Invariant`; comments that say "SPARK contracts" -have no contract under them. Without `SPARK_Mode`, `gnatprove` has nothing to -analyse, 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` hold two copies of the same Ada runner. -Which one survives belongs to the runner-only consolidation of this repository -(standards ultraplan Q8). +`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). diff --git a/runners/must/SPARK-CLI-PARSER-COMPLETE.md b/runners/must/SPARK-CLI-PARSER-COMPLETE.md index 2fd6792..2e9389e 100644 --- a/runners/must/SPARK-CLI-PARSER-COMPLETE.md +++ b/runners/must/SPARK-CLI-PARSER-COMPLETE.md @@ -1,4 +1,4 @@ -> **Status correction (2026-11-09).** No Ada source in this repository contains `SPARK_Mode` or any contract aspect (`Pre`, `Post`, `Global`, `Depends`, `Loop_Invariant`), so `gnatprove` has nothing to analyse and nothing here is proved. 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. +> **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 diff --git a/runners/must/SPARK-CONVERSION-COMPLETE.md b/runners/must/SPARK-CONVERSION-COMPLETE.md index 6eb15b1..f195b95 100644 --- a/runners/must/SPARK-CONVERSION-COMPLETE.md +++ b/runners/must/SPARK-CONVERSION-COMPLETE.md @@ -1,4 +1,4 @@ -> **Status correction (2026-11-09).** No Ada source in this repository contains `SPARK_Mode` or any contract aspect (`Pre`, `Post`, `Global`, `Depends`, `Loop_Invariant`), so `gnatprove` has nothing to analyse and nothing here is proved. 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. +> **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 diff --git a/runners/must/SPARK-CONVERSION-SESSION-2026-02-05.md b/runners/must/SPARK-CONVERSION-SESSION-2026-02-05.md index 1810dea..2d905ca 100644 --- a/runners/must/SPARK-CONVERSION-SESSION-2026-02-05.md +++ b/runners/must/SPARK-CONVERSION-SESSION-2026-02-05.md @@ -1,4 +1,4 @@ -> **Status correction (2026-11-09).** No Ada source in this repository contains `SPARK_Mode` or any contract aspect (`Pre`, `Post`, `Global`, `Depends`, `Loop_Invariant`), so `gnatprove` has nothing to analyse and nothing here is proved. 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. +> **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 diff --git a/runners/must/SPARK-MUSTACHE-ENGINE-COMPLETE.md b/runners/must/SPARK-MUSTACHE-ENGINE-COMPLETE.md index d6ac495..5e6f0ec 100644 --- a/runners/must/SPARK-MUSTACHE-ENGINE-COMPLETE.md +++ b/runners/must/SPARK-MUSTACHE-ENGINE-COMPLETE.md @@ -1,4 +1,4 @@ -> **Status correction (2026-11-09).** No Ada source in this repository contains `SPARK_Mode` or any contract aspect (`Pre`, `Post`, `Global`, `Depends`, `Loop_Invariant`), so `gnatprove` has nothing to analyse and nothing here is proved. 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. +> **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 diff --git a/runners/must/SPARK-REQUIREMENT-CHECKER-COMPLETE.md b/runners/must/SPARK-REQUIREMENT-CHECKER-COMPLETE.md index 922bdd8..7d42c44 100644 --- a/runners/must/SPARK-REQUIREMENT-CHECKER-COMPLETE.md +++ b/runners/must/SPARK-REQUIREMENT-CHECKER-COMPLETE.md @@ -1,4 +1,4 @@ -> **Status correction (2026-11-09).** No Ada source in this repository contains `SPARK_Mode` or any contract aspect (`Pre`, `Post`, `Global`, `Depends`, `Loop_Invariant`), so `gnatprove` has nothing to analyse and nothing here is proved. 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. +> **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 diff --git a/runners/must/SPARK-STATUS.md b/runners/must/SPARK-STATUS.md index 07dfc3f..0a6ed62 100644 --- a/runners/must/SPARK-STATUS.md +++ b/runners/must/SPARK-STATUS.md @@ -1,4 +1,4 @@ -> **Status correction (2026-11-09).** No Ada source in this repository contains `SPARK_Mode` or any contract aspect (`Pre`, `Post`, `Global`, `Depends`, `Loop_Invariant`), so `gnatprove` has nothing to analyse and nothing here is proved. 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. +> **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 diff --git a/runners/must/SPARK-TASK-RUNNER-COMPLETE.md b/runners/must/SPARK-TASK-RUNNER-COMPLETE.md index 0fe922f..acc2500 100644 --- a/runners/must/SPARK-TASK-RUNNER-COMPLETE.md +++ b/runners/must/SPARK-TASK-RUNNER-COMPLETE.md @@ -1,4 +1,4 @@ -> **Status correction (2026-11-09).** No Ada source in this repository contains `SPARK_Mode` or any contract aspect (`Pre`, `Post`, `Global`, `Depends`, `Loop_Invariant`), so `gnatprove` has nothing to analyse and nothing here is proved. 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. +> **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 diff --git a/scripts/check-proofs.sh b/scripts/check-proofs.sh index 80d1914..4cccc13 100755 --- a/scripts/check-proofs.sh +++ b/scripts/check-proofs.sh @@ -65,18 +65,21 @@ MANIFEST_FILE="$PROOF_DIR/MANIFEST" # CMD : executable that must be on PATH (absent => FAIL, never skip). # EXT : file extension, for the "unlisted proof" coverage scan. # ERROR_RE : if non-empty, output must not match it even when the exit code is 0. -# Only idris2 needs this (its --check exits 0 on a missing import); -# for lean4 it is a harmless belt-and-braces guard. +# idris2 needs it (its --check exits 0 on a missing import), and so +# does lean4: `lean` exits 0 on `sorry`, reporting only a warning. +# coqc exits 0, silently, on `Admitted`, so no pattern can catch it; +# check_one therefore also runs scripts/scan-dangerous.sh on every +# module, for every prover. case "$PROVER" in idris2) CMD=idris2; EXT=idr; ERROR_RE='^Error:' ;; - lean4) CMD=lean; EXT=lean; ERROR_RE='error:' ;; + lean4) CMD=lean; EXT=lean; ERROR_RE="error:|declaration uses 'sorry'" ;; agda) CMD=agda; EXT=agda; ERROR_RE='' ;; coq) CMD=coqc; EXT=v; ERROR_RE='' ;; esac check_one() { # $1 source-root (rel to ROOT), $2 module (rel to source-root). - # Sets LAST_OUT to the tool output on failure; returns 0 iff the module compiles. + # Sets LAST_OUT to the tool output on failure; returns 0 iff the module compiles and uses no escape hatch in code. local root="$1" rel="$2" out rc set +e case "$PROVER" in @@ -87,10 +90,15 @@ check_one() { coq) out="$(cd "$ROOT/$root" && coqc "$rel" 2>&1)"; rc=$? ;; esac set -e - if [ "$rc" -eq 0 ] && { [ -z "$ERROR_RE" ] || ! grep -qE "$ERROR_RE" <<<"$out"; }; then - LAST_OUT=""; return 0 + if [[ "$rc" -ne 0 ]] || { [[ -n "$ERROR_RE" ]] && grep -qE "$ERROR_RE" <<<"$out"; }; then + LAST_OUT="$out"; return 1 fi - LAST_OUT="$out"; return 1 + # A module that compiles but uses an escape hatch (believe_me, sorry, + # Admitted, ...) in code is not a proof. Comments are ignored. + if ! out="$(bash "$ROOT/scripts/scan-dangerous.sh" "$root/$rel" 2>&1)"; then + LAST_OUT="$out"; return 1 + fi + LAST_OUT=""; return 0 } echo "=== $PROVER proof check ===" @@ -130,8 +138,15 @@ while IFS='|' read -r root rel status note; do # skip blank lines and comments [ -z "${root// }" ] && continue case "${root#"${root%%[![:space:]]*}"}" in \#*) continue ;; esac - printf ' %-30s %-24s ' "$root" "$rel" echo "$root/$rel" >>"$listed_tmp" + # Fail closed on a mistyped status: anything but these two would otherwise + # be read as quarantine, letting a failing module pass unnoticed. + if [[ "$status" != gated && "$status" != quarantine ]]; then + echo " FAIL: $MANIFEST_FILE entry '$root|$rel' has status '$status' (expected gated or quarantine)" + fails=$((fails + 1)) + continue + fi + printf ' %-30s %-24s ' "$root" "$rel" if check_one "$root" "$rel"; then if [ "$status" = gated ]; then echo "PASS" @@ -162,7 +177,7 @@ found="$(cd "$ROOT" && find "$PROOF_DIR" -name "*.$EXT" -not -path '*/build/*' 2 unlisted="$(comm -13 <(printf '%s\n' "$listed") <(printf '%s\n' "$found") || true)" # A listed module is stale when its file is absent. Entries may sit outside # $PROOF_DIR (for example the coaptation core), so test the path itself. -missing="$(while IFS= read -r p; do [ -n "$p" ] && [ ! -f "$ROOT/$p" ] && echo "$p"; done <<<"$listed" || true)" +missing="$(while IFS= read -r p; do [[ -n "$p" && ! -f "$ROOT/$p" ]] && echo "$p"; done <<<"$listed" || true)" if [ -n "${unlisted//[[:space:]]/}" ]; then echo "FAIL: .$EXT proofs on disk but absent from $MANIFEST_FILE:" diff --git a/scripts/scan-dangerous.sh b/scripts/scan-dangerous.sh new file mode 100755 index 0000000..770ce66 --- /dev/null +++ b/scripts/scan-dangerous.sh @@ -0,0 +1,80 @@ +#!/usr/bin/env bash +# SPDX-License-Identifier: MPL-2.0 +# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +# +# scan-dangerous.sh — flag dangerous/unsafe constructs USED in proof code. +# +# Dangerous constructs (believe_me, assert_total, postulate, sorry, Admitted, +# unsafeCoerce, Obj.magic) escape the proof obligation and must not appear in +# real proofs. BUT the previous `proof-scan-dangerous` recipe grepped raw +# lines, so a comment that merely NAMED a banned construct — +# -- All proofs MUST be constructive (no believe_me, no assert_total). +# — tripped the gate. A check that fires on its own documentation is a +# false-positive gate: it cries wolf, trains people to override it (violating +# "squabble, don't bypass"), and wired into CI it turns the tree red for +# nothing. This version strips comments first, so only real usage is flagged. +# +# Comment syntax handled: `--` line + `{- -}` block (Idris2/Lean4/Agda), +# `(* *)` block (Coq). Comment bodies are blanked in place, so reported line +# numbers still match the source. +# +# Usage: scan-dangerous.sh [FILE...] (paths relative to the repo root) +# With no arguments it scans every proof file under verification/proofs/. +# check-proofs.sh passes each gated module, so files outside that tree +# (the coaptation core) are scanned too. +# +# Exit: 0 = clean; 1 = a proof uses a dangerous construct in code. + +set -euo pipefail +cd "$(dirname "${BASH_SOURCE[0]}")/.." + +PATTERNS='believe_me|assert_total|postulate|sorry|Admitted|unsafeCoerce|Obj\.magic' +dangerous=0 + +# Blank comment content while preserving line count (so grep -n stays accurate). +strip_comments() { + local ext="${1##*.}" lc bo bc + case "$ext" in + idr|lean|agda) lc='--'; bo='{-'; bc='-}' ;; # line + block comments + v) lc=''; bo='(*'; bc='*)' ;; # Coq block comments only + *) lc=''; bo=''; bc='' ;; + esac + awk -v lc="$lc" -v bo="$bo" -v bc="$bc" ' + BEGIN { inblk = 0 } + { + line = $0; out = ""; i = 1; n = length(line) + while (i <= n) { + if (inblk) { + if (bc != "" && substr(line,i,length(bc)) == bc) { inblk = 0; i += length(bc) } + else { i++ } + } else if (bo != "" && substr(line,i,length(bo)) == bo) { + inblk = 1; i += length(bo) + } else if (lc != "" && substr(line,i,length(lc)) == lc) { + break # rest of the line is a line-comment + } else { + out = out substr(line,i,1); i++ + } + } + print out + }' "$1" +} + +while IFS= read -r f; do + [ -z "$f" ] && continue + matches="$(strip_comments "$f" | grep -nE "$PATTERNS" || true)" + if [ -n "$matches" ]; then + echo " DANGEROUS (used in code): $f" + printf '%s\n' "$matches" | sed 's/^/ /' + dangerous=$((dangerous + 1)) + fi +done < <(if [[ $# -gt 0 ]]; then printf '%s\n' "$@"; else + find verification/proofs \ + \( -name '*.idr' -o -name '*.lean' -o -name '*.agda' -o -name '*.v' \) \ + -not -path '*/build/*' 2>/dev/null | sort; fi) + +echo +if [ "$dangerous" -gt 0 ]; then + echo "FAIL: $dangerous file(s) use dangerous constructs in proof CODE (not comments)" + exit 1 +fi +echo "PASS: no dangerous constructs used in proof code" diff --git a/verification/proofs/README.adoc b/verification/proofs/README.adoc index b228c0f..15c5417 100644 --- a/verification/proofs/README.adoc +++ b/verification/proofs/README.adoc @@ -13,8 +13,8 @@ this page only maps it onto this directory. |Code or obligation |Verifier |Where it lives |Rust code -|*Creusot* -|On the Rust code itself (contracts in the crate), not in this directory. +|*Creusot* with *Pearlite* contracts, and *Verus* (policy §1.2) +|On the Rust code itself (contracts in the crate), not in this directory. Plan a scope for both verifiers and record unsupported or pending work explicitly. |Ada code |*SPARK* @@ -34,14 +34,14 @@ Statements about one repository's types, functions or wire formats are engineering (Idris2). Statements that would hold for any implementation are theory (Agda). Behaviour of first-party Rust or Ada code (pre- and postconditions, loop invariants, absence of run-time errors) is proved with -Creusot or SPARK on that code, not restated in Idris2. +Creusot/Pearlite and Verus, or SPARK, on that code, not restated in Idris2. Another tool only where it is plainly the right one, recorded beside the artefact and in `docs/status/PROOF-STATUS.adoc` (policy §4). `tlaplus/` is such an exception: a finite model check is reported as `TESTED`, with its bounds. For Rust, *Kani* (unsafe and FFI seams, reported `TESTED` with bounds) and *Aeneas* (Rust that implements an Agda-proved theorem) are -standing exceptions that run alongside Creusot, never instead of it. +standing exceptions that run alongside Creusot and Verus, never instead of them. == Proof grades @@ -119,6 +119,24 @@ just proof-check-agda # Agda only just proof-check-coq # Coq only ---- +Each gated module must compile *and* use no escape hatch in code (comments are +ignored): `lean` exits 0 on `sorry` and `coqc` exits 0 on `Admitted`, so the +compiler alone cannot tell a proof from a placeholder. `check-proofs.sh` runs +`scripts/scan-dangerous.sh` on every gated module, including ones outside +`verification/proofs/` such as the coaptation core. + +`tlaplus/` is *not* covered by `check-proofs.sh` or `just proof-check-all`. +Run TLC on the bounded model yourself (TLA+ tools 1.8.0 or later): + +[source,bash] +---- +cd verification/proofs/tlaplus +java -cp tla2tools.jar tlc2.TLC -workers auto -config MC.cfg MC +---- + +A pass is `TESTED` with the bounds in `MC.tla` (`MaxProcessed`) and `MC.cfg` +(`MaxRequests`), never `PROVEN`. + == Banned patterns The following MUST NOT appear in any proof file: diff --git a/verification/proofs/tlaplus/MC.cfg b/verification/proofs/tlaplus/MC.cfg index f01ba02..6fb2315 100644 --- a/verification/proofs/tlaplus/MC.cfg +++ b/verification/proofs/tlaplus/MC.cfg @@ -1,10 +1,11 @@ \* SPDX-License-Identifier: MPL-2.0 -\* Run: java -cp tla2tools.jar tlc2.TLC -workers auto MC +\* Run: java -cp tla2tools.jar tlc2.TLC -workers auto -config MC.cfg MC SPECIFICATION Spec CONSTANT MaxRequests = 3 CONSTRAINT Bound INVARIANT TypeInvariant -INVARIANT ProcessedMonotonic +INVARIANT ProcessedNonNegative INVARIANT QueueBounded +PROPERTY ProcessedMonotonic PROPERTY NoSkipStates PROPERTY EventualCompletion diff --git a/verification/proofs/tlaplus/StateMachine.tla b/verification/proofs/tlaplus/StateMachine.tla index fdbc902..932992a 100644 --- a/verification/proofs/tlaplus/StateMachine.tla +++ b/verification/proofs/tlaplus/StateMachine.tla @@ -77,8 +77,12 @@ Spec == Init /\ [][Next]_vars /\ WF_vars(Next) \* State is always valid TypeInvariant == state \in States -\* Processed count never decreases (monotonicity) -ProcessedMonotonic == processed >= 0 +\* Processed count is never negative (a state invariant) +ProcessedNonNegative == processed >= 0 + +\* Processed count never decreases between states (an action property: the +\* invariant above would accept a step from 4 to 3) +ProcessedMonotonic == [][processed' >= processed]_processed \* Queue never exceeds max QueueBounded == Len(queue) <= MaxRequests @@ -90,7 +94,9 @@ NoSkipStates == \* ---- LIVENESS PROPERTIES ---- -\* Every request eventually completes or fails +\* The pipeline eventually reaches a terminal state (done or failed) at least +\* once. This is NOT per-request completion: this template never dequeues, so +\* requests can stay in `queue`. Model per-request progress before claiming it. EventualCompletion == <>(state = "done" \/ state = "failed") ============================================================================ From 94c6a5bcb45fcd8f8dc9eafcc3f7af84ebee14d6 Mon Sep 17 00:00:00 2001 From: "coderabbitai[bot]" <136622811+coderabbitai[bot]@users.noreply.github.com> Date: Mon, 9 Nov 2026 21:30:46 +0000 Subject: [PATCH 3/3] docs(proofs): document comment stripping and bounded natural number declarations --- scripts/scan-dangerous.sh | 5 ++++- verification/proofs/lean4/ApiTypes.lean | 3 ++- 2 files changed, 6 insertions(+), 2 deletions(-) diff --git a/scripts/scan-dangerous.sh b/scripts/scan-dangerous.sh index 770ce66..436da9d 100755 --- a/scripts/scan-dangerous.sh +++ b/scripts/scan-dangerous.sh @@ -31,7 +31,10 @@ cd "$(dirname "${BASH_SOURCE[0]}")/.." PATTERNS='believe_me|assert_total|postulate|sorry|Admitted|unsafeCoerce|Obj\.magic' dangerous=0 -# Blank comment content while preserving line count (so grep -n stays accurate). +# Remove comments from $1, a file path, and write the remaining text to stdout, +# preserving line count. The extension selects Idris2/Lean/Agda or Coq comment +# syntax; other extensions pass through unchanged. Nested comments and quoted +# strings are not recognised. Returns awk's status, including file-read failures. strip_comments() { local ext="${1##*.}" lc bo bc case "$ext" in diff --git a/verification/proofs/lean4/ApiTypes.lean b/verification/proofs/lean4/ApiTypes.lean index f02f259..9e7d128 100644 --- a/verification/proofs/lean4/ApiTypes.lean +++ b/verification/proofs/lean4/ApiTypes.lean @@ -37,9 +37,10 @@ structure BoundedNat (max : Nat) where val : Nat le_max : val ≤ max +/-- A bounded natural number is at most its inclusive upper bound. -/ theorem bounded_nat_le {max : Nat} (b : BoundedNat max) : b.val ≤ max := b.le_max --- Proof: zero is always bounded +/-- Construct a bounded value of zero, requiring a witness that the upper bound is positive. -/ def zeroBounded {max : Nat} (h : 0 < max) : BoundedNat max := ⟨0, Nat.zero_le max⟩