From b966f94960780b21c8f4d8858c3fee6a59ad6a90 Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 9 Nov 2026 13:25:49 +0000 Subject: [PATCH 1/3] Say what verification/proofs/ actually contains MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit docs/status/PROOF-STATUS.adoc reads 0% proven while verification/proofs/ holds ten prover files, which invites the reading that the figure is a backlog against them. It is not. The whole directory is the unmodified mint set: five files still carry an explicit "Replace with your project's …" marker, and ABI/Pointers.idr still says "Template proof". None states a property of HAEC — the Agda proves length (xs ++ ys) ≡ length xs + length ys, the Lean the functor laws for a template ApiResult, the Coq a toy expression language, the TLA+ a placeholder request pipeline. So 0% is the accurate count, and the note now says so. Recorded with it: - no escape hatch is present in any body (no believe_me, assert_total, postulate, sorry, Axiom or Admitted), verified with mathesis scripts/census/proof-holes.sh over this tree on 2026-11-09: no hole, axiom or unsafe record. - one real policy finding from that same scan, which had not been stated anywhere: verification/proofs/agda/Properties.agda carries no OPTIONS pragma at all, so it does not set --safe, let alone the PROOF-POLICY §2.1 invocation. As the file is mint boilerplate and not a theory entrypoint of this repository, the defensible fix is removal rather than adding flags to a template. - under PROOF-POLICY §8.1 none of this supports a Proof Witness Grade, because none of it is a theory obligation of this repository. - trope-checker removed the identical never-instantiated templates under ADR 0005 D5. Whether HAEC does the same is the owner's call (doctrine 7: cold is not disposable), so nothing is deleted here. Documentation only. Verified here: asciidoctor 2.0.26 --failure-level=WARN clean on both changed files. NOT RUN here: Agda, Coq, Lean, Idris2, TLA+ (no toolchain, and nothing in the tree would be worth checking if there were). Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01J4QvDh3p24SCUjyM9HHT31 --- CHANGELOG.adoc | 10 ++++++++++ docs/status/PROOF-STATUS.adoc | 33 +++++++++++++++++++++++++++++++++ 2 files changed, 43 insertions(+) diff --git a/CHANGELOG.adoc b/CHANGELOG.adoc index ca1c652..208d4e1 100644 --- a/CHANGELOG.adoc +++ b/CHANGELOG.adoc @@ -7,3 +7,13 @@ Changelog], and this project adheres to https://semver.org/spec/v2.0.0.html[Semantic Versioning]. === [Unreleased] + +==== Added + +* *A note saying what `+verification/proofs/+` actually contains (2026-11-09).* +`+docs/status/PROOF-STATUS.adoc+` now records that the directory is the unmodified +mint set, that none of it states a property of HAEC, and that the 0%-proven summary +is therefore the accurate count rather than a backlog against those files. Also +records that nothing there supports a Proof Witness Grade under PROOF-POLICY §8.1, +and that removing the templates (as trope-checker did under ADR 0005 D5) is an +owner decision. diff --git a/docs/status/PROOF-STATUS.adoc b/docs/status/PROOF-STATUS.adoc index 21299fb..368b9e0 100644 --- a/docs/status/PROOF-STATUS.adoc +++ b/docs/status/PROOF-STATUS.adoc @@ -68,6 +68,39 @@ | TP-2 | Public API type safety | TP | Lean4 | P2 | 4h |=== +== What `verification/proofs/` currently contains + +NOTE: as of 2026-11-09 the whole of `verification/proofs/` is the *unmodified mint +set*. Five files still carry an explicit marker — `coq/TypeSafety.v`, +`agda/Properties.agda`, `lean4/ApiTypes.lean`, `idris2/Types.idr` and +`tlaplus/StateMachine.tla` all say "Replace with your project's …" — and the +`idris2/ABI/` modules are from the same mint (`ABI/Pointers.idr`: "Template proof +— customise for your project's pointer types"). None of them states a property of +HAEC: the Agda proves `length (xs ++ ys) ≡ length xs + length ys`, the Lean proves +the functor laws for a template `ApiResult`, the Coq is a toy expression language, +and the TLA+ models a placeholder request pipeline. + +They are therefore not evidence for anything, which is why the summary above +correctly reads 0% proven: that figure is the accurate count, not a backlog against +these files. No escape hatch is present either: no `believe_me`, `assert_total`, +`postulate`, `sorry`, `Axiom` or `Admitted` occurs in any body — verified by +`hyperpolymath/mathesis`, `scripts/census/proof-holes.sh`, run over this tree on +2026-11-09, which reports no hole, axiom or unsafe record. + +One policy finding does come back from that same scan, and it is real: +`verification/proofs/agda/Properties.agda` carries *no* `OPTIONS` pragma at all, so +it does not set `--safe`, let alone the PROOF-POLICY §2.1 invocation +`--safe --without-K --cubical-compatible`. Since §2.1 binds first-party Agda theory +entrypoints and this file is not a theory entrypoint of this repository but mint +boilerplate, the defensible fix is removal rather than adding flags to a template — +which is the owner decision noted below. Until then the finding stands. + +Under PROOF-POLICY §8.1 none of this supports a Proof Witness Grade, because none of +it is a theory obligation of this repository. `hyperpolymath/trope-checker` removed +the identical never-instantiated templates under ADR 0005 D5; whether HAEC does the +same is an owner decision (doctrine 7: cold is not disposable), so nothing is +deleted here. The real obligations are the ones named in `PROOF-NEEDS.adoc`. + == Verification Commands [source,bash] From 0895f39c16b0cbba7e2799224098e6f9df6066df Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 9 Nov 2026 13:44:29 +0000 Subject: [PATCH 2/3] Replace the forbidden "0% proven" line with a census MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit docs/status/PROOF-STATUS.adoc published: *Overall*: 0% proven PROOF-POLICY §8.4 rule 7 forbids exactly that form: "Never publish 'X% proved', an average grade, or a single confidence score." It asks for a census instead — a count per category with the denominator. The figure was accurate; the shape was the prohibited one, and a percentage invites being averaged or trended, which is what the rule exists to prevent. It now reads as a census (0 done, 0 in progress, 0 blocked, 7 remaining, of 7 recorded obligations), with a note recording what changed and why, and the fact that no obligation here carries a Proof Witness Grade because none is a theory obligation of this repository under §8.1. The same line ships in rsr-template-repo's PROOF-STATUS.adoc, so every repository minted from it carries the same breach. The note says so: fixing it there is the solution at source, and this change is the downstream symptom being treated only because the surface is published today. Documentation only. Verified here: asciidoctor 2.0.26 --failure-level=WARN clean on both changed files; no percentage-of-proved claim remains in the file. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01J4QvDh3p24SCUjyM9HHT31 --- CHANGELOG.adoc | 11 +++++++++++ docs/status/PROOF-STATUS.adoc | 17 +++++++++++++---- 2 files changed, 24 insertions(+), 4 deletions(-) diff --git a/CHANGELOG.adoc b/CHANGELOG.adoc index 208d4e1..6604f66 100644 --- a/CHANGELOG.adoc +++ b/CHANGELOG.adoc @@ -8,6 +8,17 @@ https://semver.org/spec/v2.0.0.html[Semantic Versioning]. === [Unreleased] +==== Fixed + +* *`+docs/status/PROOF-STATUS.adoc+` published a percentage, which PROOF-POLICY +forbids (2026-11-09).* The summary read `+*Overall*: 0% proven+`. §8.4 rule 7 is +explicit — "Never publish 'X% proved', an average grade, or a single confidence +score" — and asks for a count per category with the denominator instead. The +figure was accurate; the form was the forbidden one. It now reads as a census, +with a note recording why. The same line ships in `+rsr-template-repo+`'s +`+PROOF-STATUS.adoc+`, so every repository minted from it carries the same +breach; fixing it there is the solution at source. + ==== Added * *A note saying what `+verification/proofs/+` actually contains (2026-11-09).* diff --git a/docs/status/PROOF-STATUS.adoc b/docs/status/PROOF-STATUS.adoc index 368b9e0..9634185 100644 --- a/docs/status/PROOF-STATUS.adoc +++ b/docs/status/PROOF-STATUS.adoc @@ -20,7 +20,16 @@ | *Total* | *7* | *0* | *0* | *0* | *7* |=== -*Overall*: 0% proven +*Census.* Of 7 recorded obligations: 0 done, 0 in progress, 0 blocked, 7 +remaining. No obligation here carries a Proof Witness Grade, because none is a +theory obligation of this repository under PROOF-POLICY §8.1. + +NOTE: this line used to read "*Overall*: 0% proven". PROOF-POLICY §8.4 rule 7 is +explicit — "Never publish 'X% proved', an average grade, or a single confidence +score" — and requires a count per category with the denominator instead. The +figure was accurate; the *form* was the one the policy forbids. The same line +ships in `rsr-template-repo`'s `PROOF-STATUS.adoc`, so every repository minted +from it carries it; fixing it there is the solution at source. == Proofs Done @@ -80,9 +89,9 @@ HAEC: the Agda proves `length (xs ++ ys) ≡ length xs + length ys`, the Lean pr the functor laws for a template `ApiResult`, the Coq is a toy expression language, and the TLA+ models a placeholder request pipeline. -They are therefore not evidence for anything, which is why the summary above -correctly reads 0% proven: that figure is the accurate count, not a backlog against -these files. No escape hatch is present either: no `believe_me`, `assert_total`, +They are therefore not evidence for anything, which is why the census above +correctly reads 0 done of 7: that count is accurate, not a backlog against these +files. No escape hatch is present either: no `believe_me`, `assert_total`, `postulate`, `sorry`, `Axiom` or `Admitted` occurs in any body — verified by `hyperpolymath/mathesis`, `scripts/census/proof-holes.sh`, run over this tree on 2026-11-09, which reports no hole, axiom or unsafe record. From db444daf1ab6dce9bcfda728a5c031cff6154f9b Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 9 Nov 2026 14:33:36 +0000 Subject: [PATCH 3/3] Say that the template paths remain proof targets even once the files go MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The review found a real way to misread the note this PR adds. Saying the files are not evidence, and that removing them is an owner decision, leaves open whether the OBLIGATIONS would go with them. They would not, and the distinction matters precisely to whoever acts on that decision. Checked against docs/status/PROOF-NEEDS.adoc: it assigns all seven of this repository's required proofs to paths inside verification/proofs/ — ABI-1 to ABI-5 to idris2/ABI/{Pointers,Layout,Platform,Foreign,Compliance}.idr, TP-1 to idris2/Types.idr, TP-2 to lean4/ApiTypes.lean. So the files are not proofs, but the paths are still targets: deleting the boilerplate removes placeholder content, never the obligation that something eventually goes there. The note now says that. Documentation only. Verified here: asciidoctor 2.0.26 --failure-level=WARN clean. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01J4QvDh3p24SCUjyM9HHT31 --- docs/status/PROOF-STATUS.adoc | 10 +++++++++- 1 file changed, 9 insertions(+), 1 deletion(-) diff --git a/docs/status/PROOF-STATUS.adoc b/docs/status/PROOF-STATUS.adoc index 9634185..aa88d7b 100644 --- a/docs/status/PROOF-STATUS.adoc +++ b/docs/status/PROOF-STATUS.adoc @@ -108,7 +108,15 @@ Under PROOF-POLICY §8.1 none of this supports a Proof Witness Grade, because no it is a theory obligation of this repository. `hyperpolymath/trope-checker` removed the identical never-instantiated templates under ADR 0005 D5; whether HAEC does the same is an owner decision (doctrine 7: cold is not disposable), so nothing is -deleted here. The real obligations are the ones named in `PROOF-NEEDS.adoc`. +deleted here. + +One distinction matters if the templates ever are removed: *the files are not +proofs, but the paths are still targets.* `PROOF-NEEDS.adoc` assigns all seven of +this repository's required proofs to paths inside `verification/proofs/` — ABI-1 +to ABI-5 to `idris2/ABI/{Pointers,Layout,Platform,Foreign,Compliance}.idr`, TP-1 to +`idris2/Types.idr` and TP-2 to `lean4/ApiTypes.lean`. Deleting the boilerplate at +those paths removes placeholder content, never the obligation that something +eventually goes there. == Verification Commands