From bb4a446e8dbb6b3fabbb3783663460dbc1ec3173 Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 9 Nov 2026 13:25:49 +0000 Subject: [PATCH 1/2] 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 HERMENEIA — 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 HERMENEIA 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 79e7e17..7a31e91 100644 --- a/CHANGELOG.adoc +++ b/CHANGELOG.adoc @@ -10,6 +10,16 @@ https://semver.org/spec/v2.0.0.html[Semantic Versioning]. ==== 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 HERMENEIA, 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. + +==== Added + - `coaptation`: `just check-coapt-identity` (`.machine_readable/coaptation/check-identity.sh`) — a toolchain-free identity gate enforcing issue #11's acceptance criterion: no template identity in the coaptation pack, and the committed receipt's `repo` diff --git a/docs/status/PROOF-STATUS.adoc b/docs/status/PROOF-STATUS.adoc index f8728a4..a8b3598 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 +HERMENEIA: 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 HERMENEIA 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 f7ab9a6d65cfc43f73ced0992b44f811baa66457 Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 9 Nov 2026 13:44:29 +0000 Subject: [PATCH 2/2] 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 7a31e91..b567e18 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 a8b3598..583e16d 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 @@ HERMENEIA: the Agda proves `length (xs ++ ys) ≡ length xs + length ys`, the Le 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.