diff --git a/CHANGELOG.adoc b/CHANGELOG.adoc index ca1c652..92b1e3c 100644 --- a/CHANGELOG.adoc +++ b/CHANGELOG.adoc @@ -7,3 +7,47 @@ Changelog], and this project adheres to https://semver.org/spec/v2.0.0.html[Semantic Versioning]. === [Unreleased] + +==== Fixed + +* *The `+proof-check-idris2+` account was wrong (2026-11-09).* Review found it, + and it was right. `+docs/status/PROOF-STATUS.adoc+` said that with a toolchain + present every individual `+proof-check-*+` recipe would report green on + template boilerplate, and that only the aggregate fails, "because of comment + text, not because it checked anything". That holds for Coq and Lean, and for + Agda only if its standard library is configured (`+proof-check-agda+` does not + configure it), but is false for Idris2: the recipe runs `+idris2 --check+` from + the repository root with no `+--source-dir+` and there is no `+.ipkg+` in the + tree, so every file under `+verification/proofs/idris2/+` declares a module name + (`+Types+`, `+ABI.Compliance+`, …) that cannot match the name Idris2 derives + from its path. Idris2 rejects the header before elaborating anything, and + because `+proof-check-all+` runs its dependencies in order it would stop there + and never reach `+proof-scan-dangerous+`. The entry now states both failure + paths and which one applies when. NOT RUN: Idris2 is unavailable in this + session, so the Idris2 path is read from the recipe and from Idris2's own + header check in `+src/Idris/ProcessIdr.idr+`, not executed — and that is said + in the document rather than left implied. + +==== 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. +The same line ships in `+rsr-template-repo+`'s `+PROOF-STATUS.adoc+`, so fixing +it there is the solution at source. +* *`+docs/status/PROOF-STATUS.adoc+` title was an unfilled mint placeholder +(2026-11-09).* Its title carried the mint's unfilled project-name token; it now reads +`+VOCARIUM+`, matching haec and hermeneia. The repository's placeholder gate +(`+.github/workflows/openssf-compliance.yml+`) checks a fixed list of required +files that does not include the status surfaces, which is why this passed CI. + +==== Added + +* *A note saying what `+verification/proofs/+` actually contains (2026-11-09).* +Every file there is an unmodified mint template that states nothing about +vocarium, so the 0%-proven summary is accurate rather than a backlog. The note +also records that `+build/just/proofs.just+`'s `+proof-check-*+` recipes report +`+SKIP+` and continue, against this repository's `+no-silent-skip+` constraint, +and that they are not reachable from the golden path. diff --git a/docs/status/PROOF-STATUS.adoc b/docs/status/PROOF-STATUS.adoc index aca702c..4098806 100644 --- a/docs/status/PROOF-STATUS.adoc +++ b/docs/status/PROOF-STATUS.adoc @@ -2,7 +2,7 @@ // Copyright (c) Jonathan D.A. Jewell // Template: rsr-template-repo/docs/status/PROOF-STATUS.adoc // Tracks proof completion. Requirements defined in PROOF-NEEDS.adoc -= Proof Status — {{PROJECT}} += Proof Status — VOCARIUM == Summary @@ -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 @@ -68,6 +77,70 @@ | TP-2 | Public API type safety | TP | Lean4 | P2 | 4h |=== +== What `verification/proofs/` currently contains + +NOTE: as of 2026-11-09 every file under `verification/proofs/` is an *unmodified +mint template*. Each still carries its "Replace with your project's …" header, and +none of them states anything about vocarium: `coq/TypeSafety.v` is a toy expression +language, `agda/Properties.agda` proves `length (xs ++ ys) ≡ length xs + length ys`, +`lean4/ApiTypes.lean` proves the functor laws for a template `ApiResult`, and +`tlaplus/StateMachine.tla` models a placeholder request pipeline. They are +therefore *not* evidence for anything, which is why the census above correctly +reads 0 done of 7 — that count is not a backlog against those files, it is +accurate. + +Two consequences worth stating rather than leaving implicit: + +* The individual `proof-check-*` recipes in `build/just/proofs.just` print + `SKIP: not installed` and continue. That contradicts this repository's + own `no-silent-skip` constraint, and with a Coq or Lean toolchain present each + would report green on template boilerplate. Agda would do so only if its + standard library is configured; `proof-check-agda` does not configure it. + `proof-check-idris2` is the exception among the individual recipes: it runs + `idris2 --check` from the repository root with no `--source-dir`, and there is + no `.ipkg` anywhere in this repository, so for every file under + `verification/proofs/idris2/` the declared module name (`Types`, + `ABI.Compliance`, …) cannot match the name Idris2 derives from the path. + Idris2 rejects the header before elaborating anything — `Module name Types + does not match file name "verification/proofs/idris2/Types.idr"`. + The aggregate `proof-check-all` therefore fails for one of two reasons + depending on the environment: with Idris2 installed it stops at + `proof-check-idris2`, its first dependency, and never reaches + `proof-scan-dangerous`; with no prover installed every `proof-check-*` recipe + skips and the failure comes from `proof-scan-dangerous`, whose pattern matches + the words `postulate` and `Admitted` *in the templates' own comments*. Either + way the failure says nothing about whether any proof was checked. (NOT RUN + here: Idris2 is unavailable in this session, so the first path is read from the + recipe and from Idris2's own header check in `src/Idris/ProcessIdr.idr`, not + executed. Agda is not affected the same way: it adds the file's own directory + to the include path, where Idris2 keys off the source dir.) + The recipes are not reachable from the + golden path (`just test && just quality`), so no gate is currently affected. + `hyperpolymath/trope-checker`'s `build/just/proofs.just` carries the estate's + reference treatment: it refuses to report a skip as a pass. +* `hyperpolymath/trope-checker` removed the identical never-instantiated templates + under ADR 0005 D5. Whether vocarium does the same is an owner decision (doctrine + 7: cold is not disposable), so nothing is deleted here. + +No escape hatch is present: 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. That scan does +return one real policy finding: `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`. As the file +is mint boilerplate rather than a theory entrypoint of this repository, the +defensible fix is removal rather than adding flags to a template. + +Under PROOF-POLICY §8.1 these files support no Proof Witness Grade: they are not +theory obligations of this repository at all. Nor does `PROOF-NEEDS.adoc` yet +list vocarium's own obligations — its project-specific table is empty, and the +seven rows the summary counts are the mint's ABI/FFI and typing categories, which +sit oddly beside ADR-0002's pure-Zig wire boundary (no C-ABI structs, no +bindings). The obligations this store actually owes — append-only JSONL replay, +index reconstruction on open, use-model relativity, warrant checking — are +described in `README.adoc` and the ADR, and are not yet written down as proof +obligations anywhere. + == Verification Commands [source,bash]