You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
{{ message }}
Repository navigation
Say what verification/proofs/ actually contains - #83
docs/status/PROOF-STATUS.adoc reads 0% proven while verification/proofs/ holds ten prover files. That invites the reading that the figure is a backlog against those files. It is not: the whole directory is the unmodified mint set, so 0% is the accurate count. This PR says so, and records two facts about the tree that were not written down anywhere.
Found while auditing the trope stack against PROOF-POLICY.adoc §8 (Proof Witness Grades, owner ruling 2026-11-04). Documentation only.
Changes
docs/status/PROOF-STATUS.adoc gains one section, "What verification/proofs/ currently contains":
It is all mint boilerplate. 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 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.
No escape hatch is present in any body — no believe_me, assert_total, postulate, sorry, Axiom or Admitted — verified with hyperpolymath/mathesis, scripts/census/proof-holes.sh, run over this tree on 2026-11-09: no hole, axiom or unsafe record.
One real policy finding, from that same scan, which was not 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 --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.
No Proof Witness Grade is supported here. Under §8.1 PWG applies to theory obligations; none of this is one. Hermeneia's real obligations are the ones named in PROOF-NEEDS.adoc — the voking/imminence query semantics, not a template ApiResult functor law.
Nothing is deleted.hyperpolymath/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 this PR only describes.
RSR Quality Checklist
Required
Tests pass (just test or equivalent) — no source or build file changed; AsciiDoc only
Code is formatted (just fmt or equivalent) — AsciiDoc only
Linter is clean (no new warnings or errors) — asciidoctor 2.0.26 --failure-level=WARN clean on both changed files
No banned language patterns (no TypeScript, ReScript, Deno, Node.js/npm, Go or Python)
No unsafe blocks without // SAFETY: comments — n/a
No banned functions (believe_me, unsafeCoerce, Obj.magic, Admitted, sorry) — confirmed absent from every proof body by the scan above
SPDX license headers present on all new/modified source files — existing headers untouched
No secrets, credentials, or .env files included
As Applicable
hermeneia_chora.deed updated — deeds are owner-only; not touched
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 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01J4QvDh3p24SCUjyM9HHT31
File: No configuration file from this repository applied
Commit: Unavailable
Layers: Organization UI
Review profile: ASSERTIVE
Plan: Advanced
Run ID: b166131d-8d0d-4d58-935c-480170fefc62
Commits
Reviewing files that changed from the base of the PR and between bb4a446 and f7ab9a6.
Files selected for processing: 2
CHANGELOG.adoc
docs/status/PROOF-STATUS.adoc
No actionable comments were generated in the recent review.
Summary
Summary by CodeRabbit
Documentation
Clarified that the proof files are unmodified templates and do not establish properties of HERMENEIA; the reported 0% proven is not a backlog against those files.
Documented that the templates do not support Proof Witness Grade, and that the actual proof obligations are listed separately.
Recorded a missing safety pragma in one proof file and the owner’s decision to remove templates rather than add flags. Template removal remains an owner decision.
The status document describes the contents and limitations of the proof files, records an Agda safety-policy finding, and identifies PROOF-NEEDS.adoc as the source of actual obligations. The changelog summarises the update.
Changes: Proof status documentation
Layer / File(s)
Summary
Proof-file status record docs/status/PROOF-STATUS.adoc, CHANGELOG.adoc
The status document describes the proof files as template material, records the safety-policy finding and owner decision, and identifies PROOF-NEEDS.adoc as the source of actual obligations. The changelog documents these statements.
The update documents the proof templates and open obligations. No merge-blocking issue remains.
Pre-merge checks: 5
Check name
Status
Explanation
Title check
The title "Say what verification/proofs/ actually contains" names the main change: the PR documents what the ten files in verification/proofs/ contain (mint template boilerplate, no HERMENEIA property…
Description check
The description follows the repository template's main structure. It has a Summary section explaining the 0% proven context and why the PR exists. It has a Changes section listing the new section's fo…
Docstring Coverage
No eligible functions found in the changed files. Skipping docstring coverage check. Docstring coverage is scoped to functions touched by this diff with cyclomatic complexity of at least 2. Documentat…
Linked Issues check
Check skipped because no linked issues were found for this pull request.
Out of Scope Changes check
Check skipped because no linked issues were found for this pull request.
Full details: Title check
Explanation
The title "Say what verification/proofs/ actually contains" names the main change: the PR documents what the ten files in verification/proofs/ contain (mint template boilerplate, no HERMENEIA property proofs, no escape hatches, one Agda pragma finding). It is specific and matches the changeset, which adds a section to PROOF-STATUS.adoc and a CHANGELOG entry. The title is short, single-sentence and free of noise. It does not mention the 0% proven clarification or the Proof Witness Grade point, but it does not need to cover every detail.
Full details: Description check
Explanation
The description follows the repository template's main structure. It has a Summary section explaining the 0% proven context and why the PR exists. It has a Changes section listing the new section's four points. It has the RSR Quality Checklist with Required and As Applicable items, each marked or left unmarked with reasons. It has a Testing section with commands and results, and a Screenshots section marked n/a. The template's SPDX header comment is not carried over, but that comment is an HTML comment in the template and applies to the template file itself, so its absence is not a material gap. Some checklist items are ticked with explanatory notes. The description is thorough and specific, and it matches the raw summary and objectives.
Full details: Docstring Coverage
Explanation
No eligible functions found in the changed files. Skipping docstring coverage check. Docstring coverage is scoped to functions touched by this diff with cyclomatic complexity of at least 2. Documentation-only edits and deletions within surviving functions are included; unchanged diff context and fully deleted functions are excluded. Analyzed 0 functions across 0 files. (2 skipped: 2 unsupported.)
Autofix · Keep fixing CodeRabbit findings and required CI, and resolving merge conflicts
Thanks for using CodeRabbit! It's free for OSS, and your support helps us grow. If you like it, consider giving us a shout-out.
File: No configuration file from this repository applied
Commit: Unavailable
Layers: Organization UI
Review profile: ASSERTIVE
Plan: Advanced
Run ID: cad58d2e-6b89-4257-b776-e64457448643
Commits
Reviewing files that changed from the base of the PR and between 347e42f and bb4a446.
Files selected for processing: 2
CHANGELOG.adoc
docs/status/PROOF-STATUS.adoc
Included review availability: This review used your included allowance. Your plan provides up to 1 included review per hour; 0 remain after this review.
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 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01J4QvDh3p24SCUjyM9HHT31
Deposit findings for gitbot-fleet failed against bb4a446. This PR's diff is two AsciiDoc files, CHANGELOG.adoc and docs/status/PROOF-STATUS.adoc, and touches nothing under .github/. That check reads repository and workflow configuration, which this PR does not change.
It is failing across the trope stack today. Where the logs are explicit — in trope-checker and mathesis — the root cause is the hyperpolymath/cicd-suite → hyperpolymath/proven-cicd-and-workflows repository transfer: a reusable uses: does not follow the redirect, so calls under the old name fail at startup with zero jobs.
A mechanical fix exists, re-pointing each reference at the same pin, as trope-particularity-workbench#78 did. The tooling's own message also requires this repository's Actions allowlist to admit the new owner, which is an owner-only setting in this session, so I can neither complete the fix nor show the check green. I have not widened this documentation PR with a half-fix, and have raised it with the owner.
Green on the current head
SonarCloud quality gate passed, and CodeRabbit's review of this branch reported no actionable comments. asciidoctor 2.0.26 --failure-level=WARN is clean on both changed files.
Nothing in this PR is waiting on me. It is waiting on review and on the Actions allowlist question above.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
![coderabbitai[bot]](https://avatars.githubusercontent.com/in/347564?s=60&v=4){kind=small}
Summary
docs/status/PROOF-STATUS.adocreads 0% proven whileverification/proofs/holds ten prover files. That invites the reading that the figure is a backlog against those files. It is not: the whole directory is the unmodified mint set, so 0% is the accurate count. This PR says so, and records two facts about the tree that were not written down anywhere.Found while auditing the trope stack against
PROOF-POLICY.adoc§8 (Proof Witness Grades, owner ruling 2026-11-04). Documentation only.Changes
docs/status/PROOF-STATUS.adocgains one section, "Whatverification/proofs/currently contains":coq/TypeSafety.v,agda/Properties.agda,lean4/ApiTypes.lean,idris2/Types.idrandtlaplus/StateMachine.tlaall say "Replace with your project's …" — and theidris2/ABI/modules are from the same mint (ABI/Pointers.idr: "Template proof — customise for your project's pointer types"). None states a property of HERMENEIA: the Agda proveslength (xs ++ ys) ≡ length xs + length ys, the Lean the functor laws for a templateApiResult, the Coq a toy expression language, the TLA+ a placeholder request pipeline.believe_me,assert_total,postulate,sorry,AxiomorAdmitted— verified withhyperpolymath/mathesis,scripts/census/proof-holes.sh, run over this tree on 2026-11-09: no hole, axiom or unsafe record.verification/proofs/agda/Properties.agdacarries noOPTIONSpragma 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.PROOF-NEEDS.adoc— the voking/imminence query semantics, not a templateApiResultfunctor law.hyperpolymath/trope-checkerremoved 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 this PR only describes.RSR Quality Checklist
Required
just testor equivalent) — no source or build file changed; AsciiDoc onlyjust fmtor equivalent) — AsciiDoc onlyasciidoctor 2.0.26 --failure-level=WARNclean on both changed filesunsafeblocks without// SAFETY:comments — n/abelieve_me,unsafeCoerce,Obj.magic,Admitted,sorry) — confirmed absent from every proof body by the scan above.envfiles includedAs Applicable
hermeneia_chora.deedupdated — deeds are owner-only; not toucheddocs/architecture/TOPOLOGY.adocupdated — architecture unchangedCHANGELOGor release notes updatedTesting
Run in this session at
main347e42fplus this commit:NOT RUN here: Agda, Coq, Lean, Idris2, TLA+ — no toolchain in this environment. Nothing in this PR claims a kernel result.
Screenshots
n/a (documentation).
Generated by Claude Code