From 7415a1d5ca44db1c90c3f23f01df13f0985319a9 Mon Sep 17 00:00:00 2001 From: Claude Date: Wed, 11 Nov 2026 17:28:07 +0000 Subject: [PATCH] docs: rewrite the entry documents to the standard (re-anchoring WO 3.4) Owner rulings 2026-11-11: the proof lists hold true obligations only; EXPLAINME moves to the root; a status document may cite a CI run read in the session, labelled as such. - README.adoc: overview, what it does, a planned note, quick start, layout, documentation and licence, per the README and EXPLAINME authoring standard. Each claim has an EXPLAINME entry. - EXPLAINME.adoc (moved from docs/): a claim map, a dogfooding table, known gaps, an evidence index and the proof ledger (3 proven of 5; 1 argued, 1 open). docs/EXPLAINME.adoc is a pointer. The root allow-list and the deed's root-cleaner rules admit it. - ROADMAP.adoc: the stages, the rulings (D-10 recorded), stage 3 progress and the new findings; the template milestones go. - PROOF-NEEDS.adoc and PROOF-STATUS.adoc: THY-1 discharged, the token-lattice theorems and the applied invariants open; the template obligations ABI-1 to ABI-5, TP-1 and TP-2 leave. The THY-1 record is unchanged. - READINESS.adoc (grade D, provisional) and TEST-NEEDS.adoc: from runs. - usage, contributing and troubleshooting: real content. - Deed (variant (paths)): records the move, and restores the two label files that the merge of WO 3.2 and WO 3.5 dropped from :diverged. Observed in this session on main f778a19 plus this change: just check-views (census 8 files, atlas 13 tests, registry 14 tests), validate-repo-map, validate-claude-md, validate-coapt, validate-state, validate-rsr, the canon deed lint, check-adoc-renders (180 files clean, asciidoctor 2.0.26), check-no-placeholders, the invisible-character check, the root shape and both shape tests pass. The proof figures cite CI run 43057783538 (main at b2cf524), read in this session. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_0136P7Zo9dheFQzYYWV49hAk --- .machine_readable/root-allow.txt | 1 + EXPLAINME.adoc | 279 ++++++++++++++++++++++++++ README.adoc | 202 ++++++++++--------- docs/AFFIRMATION.adoc | 2 +- docs/EXPLAINME.adoc | 120 +---------- docs/README.adoc | 2 +- docs/architecture/REPOSITORY-MAP.adoc | 4 + docs/contributing.adoc | 113 ++++------- docs/onboarding/QUICKSTART-DEV.adoc | 2 +- docs/onboarding/QUICKSTART-USER.adoc | 2 +- docs/status/PROOF-NEEDS.adoc | 166 ++++++--------- docs/status/PROOF-STATUS.adoc | 125 ++++-------- docs/status/READINESS.adoc | 243 ++++++++-------------- docs/status/ROADMAP.adoc | 108 ++++++++-- docs/status/TEST-NEEDS.adoc | 170 +++++----------- docs/troubleshooting.adoc | 80 ++++---- docs/usage.adoc | 105 ++++------ mathesis_chora.deed | 14 +- 18 files changed, 869 insertions(+), 869 deletions(-) create mode 100644 EXPLAINME.adoc diff --git a/.machine_readable/root-allow.txt b/.machine_readable/root-allow.txt index ac7e3aaf..2691ee8b 100644 --- a/.machine_readable/root-allow.txt +++ b/.machine_readable/root-allow.txt @@ -28,6 +28,7 @@ # ─── Baseline: every RSR repo has these ────────────────────────────────────── README.adoc +EXPLAINME.adoc # the evidence for each README claim; the README and EXPLAINME authoring standard puts it at the root LICENSE LICENSES/ # REUSE licence texts, dual-licence model (code MPL-2.0 / docs CC-BY-SA-4.0) CHANGELOG.adoc # AsciiDoc is the estate-standard documentation format diff --git a/EXPLAINME.adoc b/EXPLAINME.adoc new file mode 100644 index 00000000..cbc1d2a9 --- /dev/null +++ b/EXPLAINME.adoc @@ -0,0 +1,279 @@ +// SPDX-License-Identifier: CC-BY-SA-4.0 +// Copyright (c) Jonathan D.A. Jewell += Mathesis: EXPLAINME +:toc: preamble +:icons: font + +This file backs each claim of link:README.adoc[the README] with the files +that implement it and an honest caveat. It is for a reader who wants the +evidence before they rely on Mathesis. + +Each result below names how it was observed: "run on 2026-11-11" is a local +run in the session that wrote this file, on `main` at `f778a19`; "CI run" is +a GitHub Actions run whose result that session read. + +== A census of proof files + +[quote, README.adoc] +____ +It reads each public repository in the frame +(`docs/atlas/census/repos.jsonl`) and records one row of counts for each +repository that has proof files of its own: provers, declarations, holes, +axioms. Each row names the commit that the census read and when. +____ + +How this is implemented:: +`link:scripts/census/run-census.sh[]` censuses the whole frame, and +`link:scripts/census/update-rows.sh[]` refreshes named repositories or, with +`--frame`, drops entries outside the public frame. `census-repo.sh` clones +each repository blobless and checks out its proof files only; +`build-rows.sh` folds the raw output into one row per repository. The frame +holds 465 public repositories; 249 have rows (54 theory, 195 engineering). +The method and the one-writer rule are in +link:docs/atlas/README.adoc[the atlas README]. + +Caveat:: +Counts are textual: declarations are found by keyword and signature rules, +and hole and axiom counts come from proof-craft's `proof-holes.sh`. The +kernel of each home repository is the authority. "Theory" and "engineering" +is a first-pass heuristic by prover. One public repository could not be +cloned in the last census. + +== Generated atlas views + +[quote, README.adoc] +____ +A catalogue split into theory and engineering, an A-Z view, an organisation +view and a machine-readable index, all generated from the census rows. +____ + +How this is implemented:: +`link:scripts/census/render-catalogue.sh[]` writes +`docs/atlas/generated/catalogue.adoc`; `link:scripts/atlas/census-atlas.mjs[]` +writes `az.adoc`, `organisations.adoc` and `index.json`, and its `check` fails +on a stale view, a non-public frame record or a malformed private count. +`just check-views` passed (run on 2026-11-11), with the 13 atlas tests of +`link:tests/atlas/census-atlas.test.mjs[]`. + +Caveat:: +None currently known. + +== A claims registry + +[quote, README.adoc] +____ +Claim pins point at one theorem in its home repository, +at a commit and a receipt digest. The canon receipt reader of PROOF-POLICY +§8.5.1 derives each Proof Witness Grade. No grade is typed by hand. +____ + +How this is implemented:: +Pins are authored in `docs/atlas/claims/claims.jsonl` (18 claims from 3 +repositories). `link:scripts/registry/claims-registry.mjs[]` fetches each +receipt at its pinned commit, checks its digest, and calls `readProofReceipt` +from a standards checkout whose file digest it also checks. The view is +`docs/atlas/generated/registry.adoc`; ADR 0004 records the design. +`just registry-check` passed with 14 tests (run on 2026-11-11). The `must` +contract clause `no-hand-typed-grade` checks that no pin carries a grade. + +Caveat:: +Of 13 theorems, 1 is at `PWG-1` (THY-1) and 12 are `ungraded`. The canon +reader refuses the current receipts of two home repositories, so their pins +derive no grade until one side changes (an open finding in +link:docs/status/ROADMAP.adoc[the roadmap]). + +== Bridge candidates + +[quote, README.adoc] +____ +Recorded relations between artefacts in two +repositories, generated into one view. +____ + +How this is implemented:: +`docs/atlas/claims/bridges.jsonl` holds 2 candidate records; +`claims-registry.mjs` renders `docs/atlas/generated/bridges.adoc`, and +`just registry-check` fails on a stale view. + +Caveat:: +These are candidates. The bridge lock of the re-anchoring plan (WO 5.2) does +not exist yet, so no bridge is checked against both homes. + +== Home theory + +[quote, README.adoc] +____ +THY-1, reachability is monotone under additive features, is +proved in Agda and re-proved in Rocq and Lean. CI checks all three in a +pinned Guix shell. +____ + +How this is implemented:: +The sources are `link:verification/proofs/agda/FeatureReachability.agda[]`, +`link:verification/proofs/coq/FeatureReachability.v[]` and +`link:verification/proofs/lean4/FeatureReachability.lean[]`. The receipt is +`link:verification/receipts/theory_praxis.deed[]`. +`link:scripts/check-proofs.sh[]` compiles each module and audits its axioms; +`.github/workflows/agda-proof-policy.yml` runs it in the Guix shell pinned by +`build/channels.scm` and `build/manifest.scm`, with planted controls +(`tests/proofs/gate_controls_test.sh`). CI run 43057783538 on `main` at +`b2cf524` passed. See the <>. + +Caveat:: +The proof is about a graph model. That the model matches Cargo's feature +resolution is argued, not proved. + +== Applied systems + +[quote, README.adoc] +____ +Methods that apply mathematics to decisions, starting +with accounting and finance. Design documents only so far. +____ + +How this is implemented:: +`link:applied-systems/README.adoc[]` and its subdirectories: a management +accounting design, a decision record, an event map and evidence guidance. + +Caveat:: +No executable model, data schema or worked example exists yet (WO 4.2). + +== Privacy by count + +[quote, README.adoc] +____ +The frame names public repositories only. The number of +private repositories in the listing is kept as one number. +____ + +How this is implemented:: +`docs/atlas/census/private-count.json` records 40 private repositories in +the listing of 2026-11-09. Both census writers drop any entry outside the +public frame, and `census-atlas.mjs check` refuses a non-public frame record +(`link:tests/census/update_rows_frame_test.sh[]`, 6 cases, passed on +2026-11-11). The `must` clause `no-private-name` states the rule. + +Caveat:: +The git history still holds the names (owner ruling D-2 (a): no rewrite). + +== Dogfooded across the account + +[cols="1,2,2",options="header"] +|=== +|Technology or pattern |Used here |Also used in + +|Repository deed (`*_chora.deed`) with one reader and one writer +|`mathesis_chora.deed`, read by `scripts/deed-field.sh`, written only by +`scripts/deed-clause.sh` +|link:https://github.com/hyperpolymath/rsr-template-repo[rsr-template-repo] + +|k9 contractiles and the coaptation receipt +|`.machine_readable/contractiles/`, `.machine_readable/coaptation/` +|link:https://github.com/hyperpolymath/rsr-template-repo[rsr-template-repo] + +|Proof receipts read by the canon reader (PROOF-POLICY §8.5.1) +|`verification/receipts/theory_praxis.deed`, `scripts/registry/` +|link:https://github.com/metadatastician/standards[standards] + +|I-JSON/JCS data, one record per line +|`docs/atlas/census/*.jsonl`, `docs/atlas/claims/*.jsonl` +|link:https://github.com/hyperpolymath/ijson-jcs[ijson-jcs] + +|The postulate scan over the import cone of an Agda module +|`scripts/scan-postulates.sh`, called by `scripts/check-proofs.sh` +|link:https://github.com/hyperpolymath/januskey[januskey] +|=== + +== Known gaps + +[CAUTION] +==== +Badges: the authoring standard asks for OpenSSF Best Practices and Scorecard +badges on a public repository. The README carries none, because no Best +Practices project identifier is recorded for Mathesis. +==== + +[CAUTION] +==== +Template example proofs: `verification/proofs/idris2/`, +`verification/proofs/tlaplus/`, `verification/proofs/agda/Properties.agda`, +`verification/proofs/coq/TypeSafety.v` and +`verification/proofs/lean4/ApiTypes.lean` come from the RSR template. They +are not Mathesis obligations. WO 4.1 of the re-anchoring plan removes them. +==== + +[CAUTION] +==== +Contract probes: the `must` contract states six Mathesis invariants with +probes, but no runner executes `must` probes yet. CI enforces the same rules +through `just check`. +==== + +== Evidence index + +[cols="2,3",options="header"] +|=== +|Path |Proves + +|`tests/census/` +|Row folding, status-document ranking, the proof-holes scanner, the update +guard and the public frame (8 test files, all passed on 2026-11-11) + +|`tests/atlas/census-atlas.test.mjs` +|View determinism, row validation, the public frame (13 tests) + +|`tests/registry/` +|Registry derivation through fixture receipts (14 tests) + +|`tests/proofs/gate_controls_test.sh` +|A planted `postulate`, `Admitted` and `sorry` each fail the proof gate (CI) + +|`tests/golden/check_controls_test.sh` +|`just check` fails on a stale view and on a failing proof (CI) +|=== + +[[proof-ledger]] +== Proof ledger + +The receipt `verification/receipts/theory_praxis.deed` is the +machine-readable ledger; this table cites it. + +[cols="2,1,2,2,2",options="header"] +|=== +|Obligation |Status |Checker (version, flags) |Where |Trust boundary + +|THY-1: reachability is monotone under additive features (Agda leg) +|proven +|Agda 2.7.0.1, `--safe --without-K --cubical-compatible` +|`verification/proofs/agda/FeatureReachability.agda:Cargo.absent-under-all-features` +|The graph model only. `Agda.Primitive` postulates `Level`, `lzero`, `lsuc` +and `_⊔_` as builtins. + +|THY-1, Rocq leg (re-proved, correspondence `RECONCILED`) +|proven +|Rocq 8.18.0, `coqc`; `Print Assumptions` closed +|`verification/proofs/coq/FeatureReachability.v:absent_under_all_features` +|The graph model only + +|THY-1, Lean leg (re-proved, correspondence `RECONCILED`) +|proven +|Lean 4.29.0, `lean`; no axiom +|`verification/proofs/lean4/FeatureReachability.lean:absentUnderAllFeatures` +|The graph model only + +|The graph model matches Cargo's feature resolution +|argued +|- +|`docs/status/PROOF-STATUS.adoc`, THY-1 "Why" +|Not formalised + +|The token-lattice theorems (owner ruling D-10: their home is Mathesis) +|open +|- +|`docs/proposals/mathesis-research-programme.adoc` +|Not yet stated in a prover (WO 4.1) +|=== + +Proofs: 3 proven of 5; 1 argued, 1 open. The registry derives `PWG-1` for +THY-1 from the receipt. The checker versions are those that CI asserts in the +Guix shell (CI run 43057783538). diff --git a/README.adoc b/README.adoc index 09bd96b0..dd5df8cb 100644 --- a/README.adoc +++ b/README.adoc @@ -1,105 +1,123 @@ // SPDX-License-Identifier: CC-BY-SA-4.0 -= mathesis -:toc: - -The estate's maths section. It answers "where does that proof live?" for -every hyperpolymath repository: which repos carry proofs, in which prover, -whether the work reads as theory or engineering, which have holes or -axioms, and where each repo's proof-status file is. += Mathesis +:toc: preamble +:icons: font + +Mathesis is the maths section of the hyperpolymath estate. It keeps an atlas +of the mathematics in other repositories, the theory that no single system +owns, and methods that apply mathematics to decisions. Each statement carries +its evidence: Mathesis derives status from the receipts of the home +repositories, and does not assert it. + +The standards repository prescribes what must be proved +(https://github.com/metadatastician/standards/blob/main/3-practice/PROOF-POLICY.adoc[PROOF-POLICY]). +Each home repository proves its own claims and keeps their receipts. Mathesis +describes what is proved, where, and how strongly. + +== What it does + +* *A census of proof files.* It reads each public repository in the frame + (`docs/atlas/census/repos.jsonl`) and records one row of counts for each + repository that has proof files of its own: provers, declarations, holes, + axioms. Each row names the commit that the census read and when. +* *Generated atlas views.* A catalogue split into theory and engineering, an + A-Z view, an organisation view and a machine-readable index, all generated + from the census rows. +* *A claims registry.* Claim pins point at one theorem in its home repository, + at a commit and a receipt digest. The canon receipt reader of PROOF-POLICY + §8.5.1 derives each Proof Witness Grade. No grade is typed by hand. +* *Bridge candidates.* Recorded relations between artefacts in two + repositories, generated into one view. +* *Home theory.* THY-1, reachability is monotone under additive features, is + proved in Agda and re-proved in Rocq and Lean. CI checks all three in a + pinned Guix shell. +* *Applied systems.* Methods that apply mathematics to decisions, starting + with accounting and finance. Design documents only so far. +* *Privacy by count.* The frame names public repositories only. The number of + private repositories in the listing is kept as one number. + +[NOTE] +.Planned +==== +The theory shelf's admission rule and the token-lattice theorems, the applied +shelf tied to the evidence rules, a published atlas, receipts in more home +repositories, and a scheduled census. See +link:docs/status/ROADMAP.adoc[the roadmap]. +==== + +== Quick start + +The views check needs Bun, network access for the receipts, and a checkout of +`metadatastician/standards` at the reader pin named in +`scripts/registry/claims-registry.mjs`. + +[source,bash] +---- +export MATHESIS_STANDARDS=/path/to/standards +just check-views +bun scripts/atlas/census-atlas.mjs find agda +---- + +The proof checks need Agda, Rocq and Lean. CI runs them in the pinned Guix +shell; `just check` runs both halves. + +[source,bash] +---- +guix time-machine -C build/channels.scm -- shell -m build/manifest.scm -- just check +---- + +Wondering how this works? See link:EXPLAINME.adoc[]. + +== Repository layout + +[cols="1,3",options="header"] +|=== +|Path |Purpose -Proofs stay in their home repositories. mathesis points at them. Later it -will also hold the Agda sources for theory that has no other natural home. +|`docs/atlas/` +|The atlas shelf: census data (`census/`), authored claim pins and bridge +records (`claims/`), and generated views (`generated/`) -The rules for where a proof *should* live are not here: they are -https://github.com/metadatastician/standards/blob/main/3-practice/PROOF-POLICY.adoc[the canonical standards/3-practice/PROOF-POLICY.adoc] (Creusot with Pearlite contracts, and Verus, for Rust; SPARK for Ada; -Idris2 for APIs, ABIs and engineering properties, Agda for theory rechecked -in Rocq and Lean). The working method is the proof-craft skill. +|`scripts/census/`, `scripts/atlas/`, `scripts/registry/` +|The census, the atlas views and the claims registry -== Where authority lives +|`tests/census/`, `tests/atlas/`, `tests/registry/`, `tests/proofs/` +|Their tests, with negative controls -* link:docs/standards/README.adoc[Standards and authority map] — estate proof policy, proof/test evidence ownership, and Mathesis's limits. -* link:docs/atlas/README.adoc[Discovery atlas] — the current generated, read-only first slice (repository index, not theorem-level certification). -* link:docs/atlas/generated/registry.adoc[Claims registry, pilot slice]: theorem-level, grades *derived* from home-repository receipts at pinned commits; accepted in link:docs/decisions/0004-claims-registry.adoc[ADR 0004]; the canon reader of PROOF-POLICY §8.5.1 derives each grade. -* link:docs/proposals/estate-mathematical-architecture.adoc[Estate mathematical architecture proposal] — the original long-term design brief, preserved but *not ratified*. Its proposed proof grades do not override the standards policy. -* link:docs/proposals/proof-receipts-as-data.adoc[Proof receipts as data] — proposed, not adopted: machine-readable proof ledgers and CI receipts in home repositories, so Mathesis can derive Proof Witness Grades instead of transcribing them. -* link:docs/architecture/REPOSITORY-MAP.adoc[Generated repository map] — current path inventory, not the mathematical architecture specification. +|`verification/proofs/` +|Home theory sources: Agda, Rocq and Lean -Mathesis references proofs in their home repositories. A census row or a green CI badge does not independently verify a theorem. Pin claims to source commits, checker versions, assumptions and verification receipts; report missing or inaccessible evidence explicitly. +|`verification/receipts/` +|The proof receipt of Mathesis -== What is here +|`applied-systems/` +|The applied shelf -link:applied-systems/README.adoc[Applied Systems] holds reusable applications of -mathematical ideas to decisions, organisations and designed systems, starting -with accounting and finance. It contains methods and synthetic examples; -organisation-specific working material belongs in separate protected repositories. +|`docs/status/` +|Roadmap, proof needs, proof status, readiness and test needs -[cols="1,3"] -|=== -|`docs/atlas/generated/catalogue.adoc` |The catalogue: one row per repository with proof files of its own, split into theory and engineering. Generated; do not edit by hand. -|`docs/atlas/census/` |What the catalogue is rendered from: `rows.jsonl` (one row of counts per repository, no file paths), `repos.jsonl` (the census input), `unreachable.jsonl`, `template-paths.txt` and `forks-with-own-proofs.txt`. Each `.jsonl` file is JSON Lines: one I-JSON/JCS record on each line, so a change to one row changes one line. Each row also names `commit`, the commit that the census read, and `censused_at`, the UTC time it read it. -|`scripts/census/` |`run-census.sh` (whole census), `update-rows.sh` (refresh named repositories' rows only), `census-repo.sh` (one repo), `summarise.sh`, `build-rows.sh` (raw census to rows), `render-catalogue.sh` (rows to catalogue), and proof-craft's `proof-holes.sh`. -|`Justfile` |`just check` (the golden path: every generated view matches its data, and the Agda, Rocq and Lean gates pass; `just test` runs it first), `just census`, `just catalogue`, `just catalogue-check` (the committed catalogue matches the committed data). +|`mathesis_chora.deed` +|The repository deed: identity, boundaries, golden path |=== -== How the census works - -. *List repositories.* `docs/atlas/census/repos.jsonl` is the input. Agent sessions build - it with the Claude Code remote `list_repos` tool, because the GitHub API is - not reachable from them. -. *List proof files cheaply.* Each repository is cloned blobless with - `--no-checkout`, and its file names are filtered by prover extension: - Agda, Idris2, Lean, Rocq, Isabelle, TLA+, Dedukti/Lambdapi, SMT-LIB, TPTP, - SPARK, Why3, F*, Dafny and Alloy. -. *Read only the proof files.* Only those files are checked out. Top-level - declaration names go to `decls.jsonl`, and proof-craft's `proof-holes.sh` - inventories holes, axioms, disabled checkers and policy breaches - (`holes.jsonl`). -. *Set the template aside.* Files the RSR template ships - (`docs/atlas/census/template-paths.txt`) are boilerplate wherever they appear. The - catalogue counts only a repo's *own* files. -. *Skip forks, unless their proofs are first-party.* A fork normally carries - someone else's work, so the census leaves forks out. A fork whose proof - files are the owner's own is named in - `docs/atlas/census/forks-with-own-proofs.txt`, with its reason, and is - censused like any other repository. -. *Keep rows, not paths.* The raw, path-level census (clones, every proof file, every declaration, every hole finding, and a `summary.md`) goes to a scratch directory (`MATHESIS_WORK`) and is not committed. `build-rows.sh` folds it into one row of counts per repository, and only those rows are committed, so the data stays small and does not repeat other repositories' file paths. - -== Reading the catalogue (first pass, 2026-10-26) - -The first census covered 476 repositories: - -* *Scope:* 462 repositories were cloned; 5 forks and 9 awesome-lists were - skipped. 275 have proof files, and 239 still have them once template - boilerplate is set aside. -* *Unreached:* 37 private repositories could not be cloned. The catalogue - now gives the number of private repositories only, not their names. -* *Possibly missing:* the listing returned only repositories pushed since - 2026-09-15, so older, untouched repos may be absent. Add them to - `docs/atlas/census/repos.jsonl` and rerun. -* *Theory or engineering* is a heuristic: more Agda, Lean, Rocq or Isabelle - files than Idris2 or SPARK files reads as theory. Confirm each row against - PROOF-POLICY. -* *Hole, axiom, unsafe and policy counts* are textual candidates, not kernel - verdicts. The kernel is the authority. `import Mathlib` shows under - policy. -* *Declaration counts* overcount Agda and Idris2: - every column-0 type signature counts, helpers included. -* *Older template copies* survive as "own" files in some repos: for example - asdf-tool-plugins, whose plugins each carry a stubbed `Layout.idr`. -* *Fixtures:* files under `tests/`, `fixtures/`, `corpus/` or `benches/` are - counted as fixtures. `examples/` is not, because some verifiers (Atoma) - keep real verification conditions there. - -== Next steps - -* Confirm the theory/engineering split per row, and record each repo's - obligations with the status vocabulary of PROOF-POLICY §5. -* Theorem-level rows for the theory repos: statement, Agda source, Rocq - leg, Lean leg, route. -* A scheduled CI job that reruns the census and fails on catalogue drift. -* Reconcile the existing `mathesis_chora.deed` with the current estate conventions; it is already present, not a future placeholder. - -== Licence +== Documentation + +* link:EXPLAINME.adoc[EXPLAINME]: the evidence for each claim above, and the + proof ledger. +* link:docs/atlas/README.adoc[Atlas]: the pipeline, the public frame and the + one-writer rule for census data. +* link:docs/decisions/0004-claims-registry.adoc[ADR 0004]: the claims + registry. +* link:docs/standards/README.adoc[Standards and authority map]: the limits of + Mathesis. +* link:docs/status/ROADMAP.adoc[Roadmap] and + link:docs/status/PROOF-STATUS.adoc[proof status]. +* link:docs/proposals/mathesis-re-anchoring.adoc[Re-anchoring plan]: the + identity and the stages of work. +* link:docs/contributing.adoc[Contributing] and + link:.github/SECURITY.md[security policy]. + +== License Code (`scripts/`, `Justfile`): MPL-2.0. Documentation and the catalogue: -CC-BY-SA-4.0. See `LICENSES/`. +CC-BY-SA-4.0. See link:LICENSE[] and `LICENSES/`. diff --git a/docs/AFFIRMATION.adoc b/docs/AFFIRMATION.adoc index 20b13e06..14866b0d 100644 --- a/docs/AFFIRMATION.adoc +++ b/docs/AFFIRMATION.adoc @@ -139,7 +139,7 @@ contradict it*. A contradiction named here is honest; one the reader finds for themselves is not. * `README.adoc` — the aspirational claims this file is measured against. -* `docs/EXPLAINME.adoc` — the mechanism. +* `EXPLAINME.adoc`: the mechanism. * `docs/AUDIT.adoc` — the standing conformance audit. * `*_chora.deed` (repo deed) — machine-readable repo metadata (AI allocation + ply tree). * ` -= RSR Template Repo - Explainme -image:https://img.shields.io/badge/License-MPL_2.0-blue.svg[License: MPL-2.0,link="https://opensource.org/licenses/MPL-2.0"] += EXPLAINME has moved -:toc: -:icons: font - -This file explains how the key template claims map to real files. - -== Central Session Protocol Authority - -Claim: -Session protocols are centrally maintained and not duplicated in this template. - -How this is implemented: - -* The local dispatcher (`session/dispatch.sh`) maps canonical commands to central - protocol paths in `standards/3-practice/session-management-standards`. -* Local files (`session/custom-checks.k9`, `session/local-hooks.sh`, - `coordination.k9`) are integration-only. - -Caveat: - -* If `SESSION_STANDARDS_DIR` is unset and no adjacent standards checkout exists, - the dispatcher records the command but cannot resolve central checklist paths. - -== Canonical Command Surface - -Claim: -Template bindings align to one canonical command model. - -How this is implemented: - -* `Justfile` provides thin aliases (`intake-repo`, `checkpoint-change`, - `verify-maintenance`, `verify-substantial`, `verify-release`, `close-planned`, - `close-urgent`, `recover-repo`, `handover-*`). -* Every alias calls `session/dispatch.sh` with canonical verb-object pairs. - -Caveat: - -* Recipes are wrappers only. They do not replace protocol content from - the central standards repo. - -== Runtime State Is Local - -Claim: -Session state is per-repository runtime output, not standards text. - -How this is implemented: - -* `session/dispatch.sh` writes command and continuity-core capture stubs to - `.session/LAST-CANONICAL-COMMAND.md` in the target repository path. - -Caveat: - -* Runtime files are intentionally lightweight and require human/agent completion. - -== Template Token Policy - -Claim: -Placeholders are explicit template content until initialization. - -How this is implemented: - -* `README.adoc` and bootstrap recipes keep `{{TOKEN}}` placeholders visible. -* `just init` performs token replacement. - -Caveat: - -* Uninitialized placeholders must not be treated as project-specific truth. - -== Dependency Updates (Dependabot) - -Claim: -Dependency bumps land fast and safely, without manual chasing. - -How this is implemented: - -* `dependabot.yml` watches the Dependabot-supported ecosystems the estate - actually uses: `github-actions`, `cargo`, `mix` (Elixir), `docker`. -* `dependabot-automerge.yml` auto-merges *every* bump (patch/minor/major, - security or routine) **once the required checks are green** — a broken bump - fails CI and stays open (you get an email); it never lands on a red `main`. - -Caveat: - -* Dependabot has **no or Bun ecosystem**, and `pnpm` only rides under the - `npm` ecosystem (itself banned). For this -first estate Dependabot cannot - watch the runtime dependencies; the `npm`/`pip` entries are retained only for - transitional/legacy manifests and are otherwise inert. dependency - currency is managed via `.json`/`.lock`, not Dependabot. -* Do **not** add Dependabot as a ruleset *bypass* actor: that lets bumps skip - the required checks (secret-scanning, SAST), removing the safety gate and the - "it broke" signal. Auto-merge-on-green gives fast merges without it. - -== Julia Registry Packages — Standalone Repo Requirement - -Claim: -If this template is used to create a Julia package, it must remain a standalone repository registered with the Julia package registry. - -How this is implemented: - -* Julia's package registry (General.jl or other) expects each package to be a standalone GitHub repository with `Project.toml` at the repository root. -* Installation via `Pkg.add()`, dependency resolution, and automated CI/CD all depend on this canonical structure. - -Caveat: - -* Do NOT move this repository into a monorepo or subdirectory, as this breaks registry registration and package discoverability. -* Julia packages published to a registry must each remain a standalone top-level repository (registry registration and package discovery require it). -* Non-registry Julia packages can be organized differently if they are not published to any registry. - - -== License - -This project is licensed under the Mozilla Public License, v. 2.0. See the `LICENSE` file for details. - -SPDX-License-Identifier: CC-BY-SA-4.0 +The EXPLAINME of Mathesis is at the repository root: +link:../EXPLAINME.adoc[EXPLAINME.adoc]. The README and EXPLAINME authoring +standard puts it there (re-anchoring plan WO 3.4, owner ruling 2026-11-11). diff --git a/docs/README.adoc b/docs/README.adoc index dc7274f0..b038a460 100644 --- a/docs/README.adoc +++ b/docs/README.adoc @@ -12,7 +12,7 @@ and CI fails if it goes stale, so prefer it over any hand-written listing. * link:onboarding/QUICKSTART-DEV.adoc[QUICKSTART-DEV] — developing in one. * link:onboarding/QUICKSTART-MAINTAINER.adoc[QUICKSTART-MAINTAINER] — maintaining one. * link:AI_INSTALLATION_GUIDE.adoc[AI_INSTALLATION_GUIDE] — for an AI agent instantiating the template. -* link:EXPLAINME.adoc[EXPLAINME] — how the pieces actually work. +* link:../EXPLAINME.adoc[EXPLAINME]: how the pieces actually work. == The tracks diff --git a/docs/architecture/REPOSITORY-MAP.adoc b/docs/architecture/REPOSITORY-MAP.adoc index 8f1c87c9..11ac0219 100644 --- a/docs/architecture/REPOSITORY-MAP.adoc +++ b/docs/architecture/REPOSITORY-MAP.adoc @@ -97,6 +97,10 @@ predecessors did. | optional | estate docs gate (standards scripts/check-docs-presence.sh) requires CONTRIBUTING at the ROOT; this is the copy it verifies +| `EXPLAINME.adoc` +| yes +| the evidence for each README claim; the README and EXPLAINME authoring standard puts it at the root + | `GEMINI.md` | optional | pointer to CLAUDE.md for repos without AGENTS.md yet diff --git a/docs/contributing.adoc b/docs/contributing.adoc index a256fdee..83a36d62 100644 --- a/docs/contributing.adoc +++ b/docs/contributing.adoc @@ -1,91 +1,60 @@ // SPDX-License-Identifier: CC-BY-SA-4.0 // Copyright (c) Jonathan D.A. Jewell // SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) <6759885+hyperpolymath@users.noreply.github.com> -= Contributing — Mathesis -:revdate: 2026-MM-DD += Contributing to Mathesis -== Audience +This guide is for a person or an agent who changes Mathesis. To read the +atlas, see link:usage.adoc[usage]. Read `CLAUDE.md` and the deed +`mathesis_chora.deed` first: they state the identity, the boundaries and the +golden path. -Developers working *on* `Mathesis`. For consumers (people calling -or depending on it) see link:./usage.adoc[usage.adoc]. +== Tools -== Local-dev setup +* `just` 1.56.0 and the other tools that `mise.lock` pins, each with its + checksum. +* Bun, for the atlas and the registry. +* Nickel 1.18.0, for `just validate-claude-md` and `just validate-coapt`. +* Agda, Rocq and Lean for the proof checks. CI takes them from the Guix + revision that `build/channels.scm` pins (`build/manifest.scm`). -Prerequisites — the minimum versions and where to get them: - -* `` v`` — ``. -* `` v`` — ``. -* GPG signing key configured (estate policy — all commits must be - signed). See - link:https://github.com/hyperpolymath/standards/blob/main/docs/secure-coding-training.md[standards/docs/secure-coding-training.md]. - -One-shot setup: +== The golden path [source,bash] ---- -git clone git@github.com:hyperpolymath/Mathesis.git -cd Mathesis -just setup # installs deps, sets up hooks -just test # runs the full test suite +export MATHESIS_STANDARDS=/path/to/standards +just check-views +guix time-machine -C build/channels.scm -- shell -m build/manifest.scm -- just check-proofs ---- -== Running tests - -* **Unit**: `just test-unit` — fast, no I/O. -* **Integration**: `just test-int` — uses real services (database, - HTTP, etc.). Estate policy: prefer real over mocked - (see `feedback_integration_tests_real_db` in maintainer's memory). -* **Property**: `just test-prop` — randomised, slower; budget - documented in `docs/proof-debt.md` if applicable. -* **Full**: `just test` — runs all of the above. - -== Code style - -We enforce style via CI (governance-reusable.yml from hyperpolymath/standards). -Locally: - -[source,bash] ----- -just fmt # auto-format -just lint # static checks ----- - -* All commits must be **GPG-signed** (CI enforces; see - link:https://github.com/hyperpolymath/standards[standards]). -* All source files must carry an **SPDX-License-Identifier** header - (CI enforces). -* Conventional commits — `feat`, `fix`, `chore`, `refactor`, `docs`, - `test`, `ci`, `revert` (CHANGELOG is auto-generated from these - via link:https://github.com/hyperpolymath/standards/blob/main/.github/workflows/changelog-reusable.yml[`changelog-reusable.yml`]). - -== Branching & PR workflow - -. Branch off `main` as `claude/` (for AI agents) or - `/` (for humans). -. Make focused, narrow commits — one logical change per commit. -. Open a PR against `main`. -. **Enable auto-merge immediately** on every PR you open - (`gh pr merge --auto --squash`) — estate standing policy - (see standards#196 audit and policies). -. CI must be green. The PR auto-merges when checks pass + reviews land. - -== Adding a new dependency +`just check` runs both halves; CI runs it in the pinned Guix shell. A stale +view or a failing proof fails it. -. State the *why* in the PR body — what does this dependency unlock? -. Check provenance (maintained, audited, no malicious history). -. Pin to a SHA, not a tag. -. Update `docs/architecture.adoc#Dependencies`. +== Rules of this repository -== Adding an ADR +* *One writer for census data.* Only `just census` and `just update-rows` + write rows and the not-reached list; record open census work in + `docs/status/ROADMAP.adoc` first (see `docs/atlas/README.adoc`). +* *A public frame.* `docs/atlas/census/repos.jsonl` holds public + repositories only. Never write the name of a private repository anywhere. +* *No grade by hand.* Claim pins carry no grade; the registry derives each + grade from a receipt. +* *The deed has one writer.* Change `mathesis_chora.deed` only with + `scripts/deed-clause.sh`, then run `just claude-md` and `just coapt`. +* *Contractiles are sensitive.* The owner reviews each clause before it + lands. +* *Signed commits.* Every commit is signed. +* *Generated files.* Regenerate `CLAUDE.md`, the coaptation receipt, the + views and `docs/architecture/REPOSITORY-MAP.adoc` with their tools; never + edit them by hand. -When you make a non-obvious design decision, write it down: +== Decisions -. Copy `docs/decisions/0001-template.adoc` → `0002-.adoc`. -. Fill in: Context, Decision, Consequences, Alternatives. -. Link the ADR from the README or relevant code as a comment. +Record a non-obvious design decision as an ADR in `docs/decisions/`, from +`0001-template.adoc`. Decisions that are the owner's go to the owner first. == Reporting issues -* Bugs in `Mathesis`: file at `hyperpolymath/Mathesis/issues`. -* Estate-wide concerns (policy, conventions, CI): file at - `hyperpolymath/standards/issues`. +* Mathesis: https://github.com/hyperpolymath/mathesis/issues. +* Estate policy and canon: https://github.com/metadatastician/standards/issues. +* Security: see link:../.github/SECURITY.md[SECURITY.md]; do not file a + public issue. diff --git a/docs/onboarding/QUICKSTART-DEV.adoc b/docs/onboarding/QUICKSTART-DEV.adoc index 04e3e31a..0d306d08 100644 --- a/docs/onboarding/QUICKSTART-DEV.adoc +++ b/docs/onboarding/QUICKSTART-DEV.adoc @@ -99,6 +99,6 @@ Or read the repo deed (`*_chora.deed` at root) and `.claude/CLAUDE.md` directly. == Get Help -* **Architecture**: link:EXPLAINME.adoc[EXPLAINME.adoc] +* **Architecture**: link:../../EXPLAINME.adoc[EXPLAINME.adoc] * **Wiki**: https://github.com/hyperpolymath/mathesis/wiki * **Report issue**: `just help-me` diff --git a/docs/onboarding/QUICKSTART-USER.adoc b/docs/onboarding/QUICKSTART-USER.adoc index e6063058..0de6a0ff 100644 --- a/docs/onboarding/QUICKSTART-USER.adoc +++ b/docs/onboarding/QUICKSTART-USER.adoc @@ -121,5 +121,5 @@ You will be asked: == Next Steps * Read the link:README.adoc[README] for full feature overview -* Read the link:EXPLAINME.adoc[EXPLAINME] for architecture and design decisions +* Read the link:../../EXPLAINME.adoc[EXPLAINME] for architecture and design decisions * Try `just tour` for a guided walkthrough diff --git a/docs/status/PROOF-NEEDS.adoc b/docs/status/PROOF-NEEDS.adoc index 25212634..8daa8b2a 100644 --- a/docs/status/PROOF-NEEDS.adoc +++ b/docs/status/PROOF-NEEDS.adoc @@ -1,122 +1,86 @@ // SPDX-License-Identifier: CC-BY-SA-4.0 // Copyright (c) Jonathan D.A. Jewell -// Template: rsr-template-repo/docs/status/PROOF-NEEDS.adoc -// Authoritative master list: ~/Desktop/PROOF-REQUIREMENTS-MASTER.adoc -= Proof Requirements — MATHESIS += Proof needs of Mathesis -== Proof Tier +The proof obligations whose home is Mathesis. The rules for where a proof +lives and which prover carries it are in +https://github.com/metadatastician/standards/blob/main/3-practice/PROOF-POLICY.adoc[PROOF-POLICY] +§1: Agda for theory, re-checked in Rocq and Lean. Progress is in +link:PROOF-STATUS.adoc[PROOF-STATUS]; the evidence is in the +link:../../EXPLAINME.adoc#proof-ledger[proof ledger]. -// Assign one: T1 (Critical), T2 (High), T3 (Standard), T4 (Light), T5 (Exempt) -*Tier*: T3 — Standard +== Proof tier -== Proof Categories +*Tier*: T3, Standard. -[cols="1,3,1", options="header"] -|=== -| Code | Meaning | Applies? - -| *TP* | Typing Proofs (type soundness, type safety) | Yes -| *INV* | Invariant Proofs (state machines, monotonicity, bounds) | -| *SEC* | Security Proofs (crypto, injection freedom, access control) | -| *CONC* | Concurrency Proofs (linearizability, deadlock freedom) | -| *ALG* | Algorithm Proofs (termination, correctness, bounds) | -| *ABI* | ABI/FFI Proofs (memory layout, pointer safety, platform compat) | Yes -| *DOM* | Domain-Specific Proofs (bespoke to this project) | -|=== - -== Mandatory Proofs (All RSR Repos) - -These proofs come from the mathesis and MUST be present in every repo: +== Obligations -=== ABI/FFI Boundary Proofs (Idris2) - -[cols="1,3,1,3", options="header"] +[cols="1,3,1,1,2",options="header"] |=== -| # | Proof | Status | File - -| ABI-1 | Non-null pointer proofs (`So (ptr /= 0)`) | Needed | `verification/proofs/idris2/ABI/Pointers.idr` -| ABI-2 | Memory layout correctness (`HasSize`, `HasAlignment`) | Needed | `verification/proofs/idris2/ABI/Layout.idr` -| ABI-3 | Platform type size proofs (per platform) | Needed | `verification/proofs/idris2/ABI/Platform.idr` -| ABI-4 | FFI function return type proofs | Needed | `verification/proofs/idris2/ABI/Foreign.idr` -| ABI-5 | C ABI compliance (`CABICompliant`, `FieldsAligned`) | Needed | `verification/proofs/idris2/ABI/Compliance.idr` +|Id |Obligation |Prover |Status |Where + +|THY-1 +|Reachability in a dependency graph is monotone under additive features +(backs the `--all-features` rule of the standards upstream dependency +watch) +|Agda, re-proved in Rocq and Lean +|Discharged: the receipt derives `PWG-1` +|`verification/proofs/agda/FeatureReachability.agda`, +`verification/receipts/theory_praxis.deed` + +|To be allocated +|The token-lattice theorems: rows 2 and 12 of the ECHIDNA proof-route +ladder, starting with the chain of PROOF-POLICY §5. Ruling D-10 puts their +home in Mathesis. +|Agda, re-checked in Rocq and Lean +|Open (WO 4.1) +|Statements: `docs/proposals/mathesis-research-programme.adoc` + +|To be allocated +|The invariants of the applied shelf that merit a proof +|Not chosen +|Open: not yet stated (WO 4.2) +|`applied-systems/` |=== -=== Typing Proofs (Prover Varies) - -[cols="1,3,1,3", options="header"] -|=== -| # | Proof | Status | File +No Mathesis obligation concerns an ABI or an FFI: since WO 3.2 the deed +declares neither capability. -| 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` -|=== +[NOTE] +.Template example proofs +==== +`verification/proofs/idris2/`, `verification/proofs/tlaplus/`, +`verification/proofs/agda/Properties.agda`, +`verification/proofs/coq/TypeSafety.v` and +`verification/proofs/lean4/ApiTypes.lean` come from the RSR template. They +are examples, not Mathesis obligations. WO 4.1 of the re-anchoring plan +removes them. +==== -== Project-Specific Proofs +== Banned patterns -// Fill in proofs specific to this project. Copy from PROOF-REQUIREMENTS-MASTER.adoc -// Delete this section for T4/T5 repos +No proof file may contain an unproven escape: `postulate` (Agda), +`Admitted` (Rocq), `sorry` (Lean), `believe_me` or `assert_total` +(Idris2). For Agda, Rocq and Lean, `scripts/check-proofs.sh` enforces this +in CI: it compiles each gated module, then audits its axioms, and +`tests/proofs/gate_controls_test.sh` shows that a planted escape fails. -[cols="1,3,1,1,1,2", options="header"] -|=== -| # | Proof Needed | Category | Prover | Priority | File(s) +== Proof file locations -| | | | | | +[cols="1,3",options="header"] |=== +|Path |Contents -== Dangerous Patterns (BANNED) - -The following MUST NOT appear anywhere in proof files: - -[cols="2,2,3", options="header"] -|=== -| Pattern | Language | Meaning - -| `believe_me` | Idris2 | Unsafe cast / trust-me -| `assert_total` | Idris2 | Skip totality check -| `postulate` | Idris2/Agda | Unproven axiom -| `sorry` | Lean4 | Incomplete proof -| `Admitted` | Coq | Incomplete proof -| `unsafeCoerce` | Haskell | Unsafe type cast -| `Obj.magic` | OCaml/ | Unsafe type cast -| `unsafe` (unaudited) | Rust | Unsafe block without safety comment -|=== +|`verification/proofs/agda/` +|The Agda sources of the home theory -CI will reject any PR introducing these patterns (enforced by `panic-attack assail`). +|`verification/proofs/coq/` +|The Rocq re-proofs -== Prover Selection Guide +|`verification/proofs/lean4/` +|The Lean re-proofs; `lean-toolchain` names Lean 4.29.0, the version that +CI takes from Guix and asserts -[cols="2,2,3", options="header"] +|`verification/receipts/` +|The proof receipt of Mathesis (PROOF-POLICY §8.5.1) |=== -| 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 -|=== - -== Proof File Locations - ----- -verification/proofs/ -├── idris2/ # Idris2 proofs (ABI, dependent types) -│ ├── ABI/ # ABI-specific proofs -│ └── *.idr # Project-specific Idris2 proofs -├── lean4/ # Lean4 proofs (algebra, lattices) -│ └── *.lean -├── agda/ # Agda proofs (induction, metatheory) -│ └── *.agda -├── coq/ # Coq proofs (type systems, compilation) -│ └── *.v -└── tlaplus/ # TLA+ specs (distributed protocols) - └── *.tla ----- - -== References - -* Master list: `~/Desktop/PROOF-REQUIREMENTS-MASTER.adoc` -* Proof status tracking: `PROOF-STATUS.adoc` (this repo) -* Proven library: `proven` repo (Idris2 verified foundations) -* Template: `rsr-template-repo/docs/status/PROOF-NEEDS.adoc` diff --git a/docs/status/PROOF-STATUS.adoc b/docs/status/PROOF-STATUS.adoc index c7ba05c2..6d1e69ae 100644 --- a/docs/status/PROOF-STATUS.adoc +++ b/docs/status/PROOF-STATUS.adoc @@ -1,73 +1,38 @@ // SPDX-License-Identifier: CC-BY-SA-4.0 // 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 — MATHESIS += Proof status of Mathesis -== Summary - -[cols="2,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* -|=== - -*Overall*: 0 of 7 tracked obligations proven. (Counts, not a percentage: -PROOF-POLICY §8 grades are derived from receipts and are never flattened.) - -== Proofs Done - -// Format: -// | ID | Proof | Prover | File | Date | Verified By | -// | ABI-1 | Non-null pointer proofs | Idris2 | verification/proofs/idris2/ABI/Pointers.idr | 2026-XX-XX | idris2 --check | - -[cols="1,3,1,3,1,2", options="header"] -|=== -| ID | Proof | Prover | File | Date | Verified By - -| — | No proofs completed yet | — | — | — | — -|=== - -== Proofs In Progress - -[cols="1,3,1,2,1,2", options="header"] -|=== -| ID | Proof | Prover | Assignee | Started | Blocker - -| — | — | — | — | — | — -|=== +The obligations are listed in link:PROOF-NEEDS.adoc[PROOF-NEEDS]. A grade is +derived from a receipt and is never typed by hand: the claims registry +(`docs/atlas/generated/registry.adoc`) derives each grade through the canon +reader of PROOF-POLICY §8.5.1. -== Proofs Blocked +== Summary -[cols="1,3,2,3", options="header"] +[cols="2,1,1,1",options="header"] |=== -| ID | Proof | Blocked By | Notes - -| — | — | — | — +|Obligation |Status |Derived grade |Evidence + +|THY-1 +|Discharged +|`PWG-1` +|The receipt `verification/receipts/theory_praxis.deed`; the record below + +|The token-lattice theorems (WO 4.1) +|Open +|- +|Not yet stated in a prover + +|The applied invariants (WO 4.2) +|Open +|- +|Not yet stated |=== -== Proofs Remaining - -[cols="1,3,1,1,1,1", options="header"] -|=== -| ID | Proof | Category | Prover | Priority | Est. Effort - -| ABI-1 | Non-null pointer proofs | ABI | Idris2 | P1 | 2h -| ABI-2 | Memory layout correctness | ABI | Idris2 | P1 | 4h -| ABI-3 | Platform type size proofs | ABI | Idris2 | P1 | 2h -| 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 -|=== +*Overall*: 1 of 3 obligations discharged; 2 open. These are counts, not a +percentage: PROOF-POLICY §8 grades are derived from receipts and are never +flattened. The template example proofs are not obligations (see +link:PROOF-NEEDS.adoc[PROOF-NEEDS]). == Theory theorems @@ -244,34 +209,30 @@ dependency units unify features separately, and the theorem applies to each unit's graph. |=== -== Verification Commands +== Verification commands [source,bash] ---- -# Check all Idris2 proofs -just proof-check-idris2 - -# Check all Lean4 proofs -just proof-check-lean4 - -# Check all Agda proofs -just proof-check-agda +# The Agda, Rocq and Lean gates, with the axiom audit (needs the provers; +# CI runs them in the pinned Guix shell) +guix time-machine -C build/channels.scm -- shell -m build/manifest.scm -- just check-proofs -# Check all Coq proofs -just proof-check-coq - -# Run all proof checks -just proof-check-all - -# Scan for dangerous patterns -panic-attack assail --proofs-only +# The planted controls: each must fail the gate +bash tests/proofs/gate_controls_test.sh agda ---- == Changelog -[cols="1,3,1", options="header"] +[cols="1,3",options="header"] |=== -| Date | Change | By +|Date |Change + +|2026-11-10 +|THY-1 receipts earned again at Agda 2.7.0.1 and Lean 4.29.0 in the pinned +Guix shell; the receipt derives `PWG-1`. -| 2026-04-04 | Initial proof status tracking | Template +|2026-11-11 +|The template obligations ABI-1 to ABI-5, TP-1 and TP-2 leave the lists: +they never applied to Mathesis (re-anchoring plan WO 3.4, owner ruling +2026-11-11). |=== diff --git a/docs/status/READINESS.adoc b/docs/status/READINESS.adoc index dc305f58..7754a954 100644 --- a/docs/status/READINESS.adoc +++ b/docs/status/READINESS.adoc @@ -1,188 +1,109 @@ // SPDX-License-Identifier: CC-BY-SA-4.0 // Copyright (c) Jonathan D.A. Jewell -= Mathesis Component Readiness Assessment += Mathesis component readiness assessment *Standard:* link:https://github.com/hyperpolymath/standards/tree/main/component-readiness-grades[Component Readiness Grades (CRG) v2.0 STRICT] + -*Assessed:* 2026-10-29 + -*Assessor:* Jonathan D.A. Jewell + -*Previous assessment:* __ +*Assessed:* 2026-11-11 + +*Assessor:* a Claude Code session (re-anchoring plan WO 3.4); provisional +until the owner confirms it + +*Previous assessment:* none (the file of 2026-10-29 was an unfilled form) -*Current Grade:* X +*Current Grade:* D -This line is parsed by `just crg-grade` / `just crg-badge`. The grade above is -the worst-graded in-scope component — *the project's weakest link sets its -grade*. See the per-component table in §3. +The grade is that of the weakest graded component in §2. `just crg-grade` +and `just crg-badge` do not read this file: the template recipes look for +`READINESS.md` at the root, which does not exist, so both print `X`. -[NOTE] -==== -*Honest grading.* Per CRG v2.0 Principle 4: grade as-is today, not -aspirationally. Long alpha is discipline, not shame. Demote immediately if -evidence doesn't support the claim. -==== +== 1. Evidence -''' +Each value below was observed on 2026-11-11, on `main` at `f778a19`, unless +it names a CI run. -== 1. CRG v2.0 Grade Reference - -[cols="1,2,2,3,2", options="header"] -|=== -| Grade | Name | Release Stage | Stability Posture | Shorthand - -| X | Untested | — | — | — -| F | Harmful / Wasteful | — | — | reject/delegate -| E | Minimal / Salvageable | Pre-alpha | Unstable | `pre-alpha` -| D | Partial / Inconsistent| Alpha | Unstable | `alpha-unstable` -| C | Self-Validated | Alpha | Stable in home context | `alpha-stable` -| B | Broadly Validated | Beta | Stable for broad trial | `beta-stable` -| A | Field-Proven | Stable | Stable | `stable` +[cols="2,3,3",options="header"] |=== +|Metric |Value |Source -*Evidence gates (v2.0 is stricter than v1.0):* +|Census tests +|8 test files pass (21 named cases, and 2 files that report by exit status) +|`tests/census/*.sh`, run locally -* *D*: RSR-compliant + per-capability tests + documented scope. Test matrix - must cite counts and live in `docs/status/ROADMAP.adoc` or CI. -* *C*: All of D, plus active dogfooding in home context with *no known - home-context failures over an evidence window*, plus *deep per-file and - per-directory annotation* (purpose, boundaries, invariants, - execution/test/proof surfaces, per-directory orientation READMEs). - `docs/status/ROADMAP.adoc` `== Dogfooding status` populated with concrete - "done — " entries. -* *B*: All of C, plus *six genuinely diverse external targets* with - feedback fed back. ROADMAP.adoc `== External targets` holds target identities - + dates + outcomes; `== Issues fed back` holds the closed-issue trail. - Internal-capability items do *not* count. -* *A*: All of B, plus multi-source real-world external feedback confirming - value, no harm in the wild. ROADMAP.adoc `== Field signal` populated. +|Atlas tests +|13 pass, 0 fail +|`bun test tests/atlas/census-atlas.test.mjs`, in `just check-views` -*Publication gate:* non-abstract implementation claims require *B+*. -Below B, any publication must be explicitly abstract or provisional. +|Registry tests +|14 pass, 0 fail +|`bun test tests/registry/`, in `just check-views` -''' +|Views current +|`just check-views` passes +|run locally -== 2. Headline Evidence (as of 2026-10-29) +|Proof gate (Agda, Rocq, Lean, with axiom audit and planted controls) +|Pass +|CI run 43057783538, `main` at `b2cf524` (read in this session) -[cols="2,3,3", options="header"] -|=== -| Metric | Value | Source - -| Test count | __ | `docs/status/ROADMAP.adoc` or CI -| Formal-verification posture | __ | grep of proof dirs -| Dangerous patterns (`assert_total`, `unsafeCoerce`, `Obj.magic`) | __ | grep 2026-10-29 -| Per-unit README coverage | __ | filesystem scan of unit dirs -| CI status | __ | `.github/workflows/` -| RSR mandatory workflows | __ | `.github/workflows/` -| Third-party badges (if any) | __ | external -| LIVE deployment (if any) | __ | production -|=== +|Escapes in proof code (`postulate`, `Admitted`, `sorry`, `believe_me`, +`assert_total`, `unsafeCoerce`) +|0. The only matches are comments and the README that forbid them. +|`git grep -w` over `verification/proofs/` -''' - -== 3. Component Assessment +|RSR scaffold +|`just validate-rsr` passes; the canon `check-rsr-profile.sh` reports that +the scaffold matches the declared capabilities +|run locally; the canon check at standards `e2a03dc` +|=== -All components graded *as-is today*, per CRG v2.0 Principle 4. Stability -posture reflects the component's state *within its home context only* -unless noted. +== 2. Component assessment -[cols="2,1,1,3,3,2", options="header"] +[cols="2,1,1,3,3",options="header"] |=== -| Component | Grade | Posture | Evidence Summary | Promotion blocker | Last Assessed - -| __ | X/F/E/D/C/B/A | __ | __ | __ | 2026-10-29 -| __ | … | … | … | … | 2026-10-29 -| __ | … | … | … | … | 2026-10-29 +|Component |Grade |Posture |Evidence summary |Promotion blocker + +|Census (`scripts/census/`) +|D +|alpha-unstable +|8 test files pass; the scope and the one-writer rule are in +`docs/atlas/README.adoc`; 249 rows from a frame of 465 public repositories +|A dated dogfood log over an evidence window; per-file annotation; one +public repository is not reached + +|Atlas views (`scripts/atlas/`) +|D +|alpha-unstable +|13 tests pass; `just check-views` passes; CI runs `just check` +|A dated dogfood log; per-file annotation + +|Claims registry (`scripts/registry/`) +|D +|alpha-unstable +|14 tests pass; ADR 0004; 18 claim pins, 13 theorems, 1 graded `PWG-1` +|The canon reader refuses the receipts of two homes; a dogfood log + +|Proof gate and home theory (`scripts/check-proofs.sh`, +`verification/`) +|D +|alpha-unstable +|CI passes with controls; THY-1 at `PWG-1` in three provers +|A dogfood log; the template example proofs still sit in the gate (WO 4.1) |=== -*Rules of thumb for populating this table:* - -* One row per independently-gradable unit. If a subsystem can ship or break - independently, it gets its own row. -* Evidence Summary must cite *numbers* (test counts, LOC, file counts) or - *paths* (e.g. `src/interface/Abi/Module.idr`), never vague claims. -* Promotion blocker must be *actionable* — "add external consumer in home - context, then annotate" beats "needs more validation". -* Re-assess every release cycle; date-stamp each row. - -''' - -== 4. What's Needed for D → C - -CRG v2.0 requires two new pieces of evidence on top of D: - -. *Active dogfooding in home context with no known home-context failures.* -** Start date: __. -** Home context: __. -** "No known failures" is a moving claim — must hold continuously across - the evidence window (recommended: 4 weeks, daily use). -** Populate `== Dogfooding status` in `docs/status/ROADMAP.adoc` with one entry - per capability: ` — done — `. - -. *Deep code and folder annotation.* -** Per-directory orientation READMEs in every non-trivial source subtree. -** Per-file header comments: purpose, boundaries, invariants, - execution/test/proof surface. -** Per-unit (cartridge/panel/plugin/module) README covering: purpose, - tools, architecture-at-a-glance, build steps. Overview-level alone is - not sufficient — depth is required where a reviewer would otherwise - have to read source to orient. - -*Minimum first-ring targets for C promotion:* list the trunk components -here. If these aren't C, nothing else can be. - -''' - -== 5. What's Needed for C → B - -Six *genuinely diverse* external targets with feedback fed back into the -component. Candidate diversity axes: - -* Different language runtime (not just variants of the same one). -* Different OS family (at least one must not be Linux). -* Different hardware class (cloud / server / desktop / embedded / mobile). -* Different auth posture (unauthenticated, API-key, vault-brokered, mTLS). -* Different topology (star, mesh, peer-to-peer). -* Different trust model (same-org, federated, adversarial). - -Populate `docs/status/ROADMAP.adoc`: - -* `== External targets` — target-id → ` — — `. -* `== Issues fed back` — issue-id → ` — — `. - -Six variations of the same use case do *not* count. Re-classify any items -currently under other roadmap sections and move external-eligible ones -into `== External targets`. - -''' - -== 6. What's Needed for B → A - -Real-world external feedback confirming value. Populate -`== Field signal` in `docs/status/ROADMAP.adoc` with multi-source entries: - -* External users beyond the six B-targets. -* Third-party writeups, talks, papers, or testimonials. -* No unresolved safety / correctness incidents in the last 90 days. - -''' - -== 7. Summary (2026-10-29) +The applied shelf (`applied-systems/`) is not graded: it holds design +documents and no executable component (WO 4.2). -* Project grade: __. Why: _<1-2 line justification>_. -* Delta since last assessment: __. -* Next milestone: __. -* Machine-readable grade line present (§ header) for `just crg-grade` / `just crg-badge`. +== 3. What C needs -''' +CRG C adds two pieces of evidence to D: -== 8. Companion Artefacts +. Active dogfooding in the home context with no known failure over an + evidence window. Mathesis keeps no dated dogfood log yet, and + `docs/status/ROADMAP.adoc` has no `== Dogfooding status` section. +. Deep per-file and per-directory annotation. The census, atlas and registry + directories have no per-directory orientation README yet. -* `docs/governance/CRG-CRITERIA.adoc` — grade definitions (boilerplate). -* `docs/governance/CRG-AUDIT-.adoc` — formal audit (populate from - `mathesis/docs/governance/CRG-AUDIT-TEMPLATE.adoc`). -* `docs/practice/DOGFOOD-LOG.adoc` — dated dogfood evidence (required for C). -* `docs/status/ROADMAP.adoc` — evidence journal (sections - `== Dogfooding status`, `== External targets`, `== Issues fed back`, - `== Field signal`, and a `Declared CRG grade:` line). -* `*_chora.deed` (repo deed) — authoritative phase and maturity (`(status)`, - `(maturity)`). +== 4. Summary -_Run `just crg-badge` to generate the shields.io badge for your README._ +* Project grade: D. Each graded component has tests that pass, a documented + scope, and an RSR-conformant scaffold; none has a dogfood evidence window. +* Delta: first assessment. +* Next: a dated dogfood log and per-directory annotation, then C. diff --git a/docs/status/ROADMAP.adoc b/docs/status/ROADMAP.adoc index 5b310d73..ea956beb 100644 --- a/docs/status/ROADMAP.adoc +++ b/docs/status/ROADMAP.adoc @@ -4,7 +4,11 @@ == Current Status -Initial development phase. +Phase `incubating`, maturity `experimental` (the deed's `(status)` and +`(maturity)`). The re-anchoring plan +(`docs/proposals/mathesis-re-anchoring.adoc`) is at stage 3, "tell the +truth". The stages are under <>; the rulings that steer them are +under <>. === Applied Systems (2026-11-07) @@ -113,19 +117,89 @@ One pull request that changes census rows is open at a time (atlas README, `repos.jsonl` keeps its 465 public records. `private-count.json` records that the listing of 2026-11-09 counted 40 private repositories. The 40 private entries leave `unreachable.jsonl` and the catalogue. No row changes. - -== Milestones - -=== v0.1.0 - Foundation -* [ ] Core functionality -* [ ] Basic documentation -* [ ] CI/CD pipeline - -=== v1.0.0 - Stable Release -* [ ] Full feature set -* [ ] Comprehensive tests -* [ ] Production ready - -== Future Directions - -_To be determined based on community feedback._ + Merged (pull request 74). + +=== Re-anchoring: stage 3 (2026-11-11) + +* WO 3.1, the deed: merged (pull request 73). The owner reviewed the clause + text first. +* WO 3.2, capabilities: merged (pull request 75), done by a Sonnet session + under doctrine 16. Seven vestigial modules left; `validate-rsr` took the + template's own fix (rsr-template-repo `fb4f67e`). +* WO 3.5, private names: merged (pull request 74), before WO 3.3 by owner + ruling. The template leak in `.github/labels.json` is reported as + rsr-template-repo issue 326. +* WO 3.3, contracts: merged (pull request 76). The coaptation band reads + amber: three committed stages are open. The owner accepted that reading. +* WO 3.4, entry documents: this change. Next: WO 3.6, the affirmation. +* New findings, each for the owner: +** The `dust` contract keeps a clause damaged by the template's name pass + ("No references to mathesis in generic template files"). Its probe passes + vacuously: the directory that it searches does not exist. +** `build/container/compose.yaml` still names the Containerfile that WO 3.2 + removed. +** `scripts/merge-actions-lock.rs` lost its only CI check when WO 3.2 + removed `rust-ci.yml` (owner ruling in that session). +** The coaptation advice text in `.machine_readable/coaptation/coapt.ncl` + carries a U+2014 character into each generated receipt. +** The merge that joined WO 3.2 and WO 3.5 dropped two entries of + `(variant (paths :diverged))`. WO 3.4 restores them. + +[[stages]] +== Stages + +The stages of the re-anchoring plan. Each status comes from a merged pull +request or a run named in it. + +[cols="1,3,1",options="header"] +|=== +|Stage |Goal |Status + +|0 +|Stop the conflicts: triage the open pull requests, one writer for census +data +|Done + +|1 +|Close the holes: gate the catalogue and the arrival pack, close the proof +gate gap, Agda, Rocq and Lean in CI, the receipt of Mathesis +|Done + +|2 +|One pipeline: JSON Lines with provenance, the canon reader, the +`docs/atlas/` paths, the bridge view, `just check` +|Done + +|3 +|Tell the truth: deed, capabilities, contracts, entry documents, no private +names, affirmation +|In progress: WO 3.1, 3.2, 3.3 and 3.5 merged; WO 3.4 in review; WO 3.6 +next + +|4 +|The three shelves: the theory admission rule and the token-lattice +theorems, the applied shelf tied to the evidence spine, the published atlas +(needs a ruling) +|Declared + +|5 +|Scale: receipts in the home repositories, the bridge lock pilot, a +scheduled census, a view of what each repository owes +|Declared +|=== + +[[rulings]] +== Rulings + +* D-1 to D-8 (2026-11-10): the decisions of the re-anchoring plan, each ruled + arm (a). The plan records them under "Decisions for the owner". +* D-10 (2026-11-09, ECHIDNA proof-route plan in the standards repository): + the token-lattice theory lives in Mathesis. Its theorems are the next + content of the theory shelf (WO 4.1); their statements are in + `docs/proposals/mathesis-research-programme.adoc`. +* Stage 3 (2026-11-11), through the selector: the WO 3.1 clause text; `(meta + :type)` stays `library` and the `groove` integration stays; WO 3.2 on a + Sonnet session; the census writers enforce the public frame; WO 3.5 before + WO 3.3; the contract text, `must` severity `critical`, probes with + "probe-deferred" accepted, amber band accepted; WO 3.4: true proof + obligations only, EXPLAINME at the root, CI runs may be cited when labelled. diff --git a/docs/status/TEST-NEEDS.adoc b/docs/status/TEST-NEEDS.adoc index bce3988e..a09b2dc8 100644 --- a/docs/status/TEST-NEEDS.adoc +++ b/docs/status/TEST-NEEDS.adoc @@ -1,126 +1,60 @@ // SPDX-License-Identifier: CC-BY-SA-4.0 // Copyright (c) Jonathan D.A. Jewell -= TEST-NEEDS: mathesis += Test needs of Mathesis -== CRG Grade: C — ACHIEVED 2026-04-04 +The tests of the Mathesis parts, what they show, and what is still missing. +The readiness grade that rests on them is in link:READINESS.adoc[READINESS]. +Each result was observed on 2026-11-11, on `main` at `f778a19`, unless it +names a CI run. -== Current State (Updated 2026-04-04) +== Current state -[cols="2,1,4", options="header"] +[cols="2,1,3",options="header"] |=== -| Category | Count | Details - -| *Source modules* | 6 | 3 Idris2 ABI (Foreign, Layout, Types), 2 Zig FFI (build, main), 1 Zig integration test template -| *Unit tests* | 0 | None in main source (inline tests in main.zig) -| *Integration tests* | 1 | `test/integration_test.zig` (documented template, 1 placeholder test) -| *E2E tests* | 1 | `tests/e2e/template_instantiation_test.sh` (full instantiation + validation) -| *Workflow tests* | 1 | `tests/workflows/validate_workflows_test.sh` (21 workflows validated) -| *Validation tests* | 1 | `scripts/validate-template.sh` (8-phase comprehensive validation) -| *Benchmarks* | 5 | `benches/template_bench.sh` (validation, Zig build, tests, workflows, instantiation) -| *Fuzz tests* | 0 | `README.adoc` scaffold with harness instructions +|Suite |Result |What it shows + +|`tests/census/` (8 files) +|All pass: 21 named cases, and 2 files that report by exit status +|Row folding, status-document ranking, the proof-holes scanner, the guard +of `update-rows.sh`, and the public frame (`update_rows_frame_test.sh`) + +|`tests/atlas/census-atlas.test.mjs` +|13 pass +|Row validation, view determinism, the bounded context pack, and the public +frame, each with negative controls + +|`tests/registry/` (2 files) +|14 pass +|Registry derivation through fixture receipts in the §8.5.1 shape + +|`tests/proofs/gate_controls_test.sh` +|Pass in CI run 43057783538 (`main` at `b2cf524`) +|A planted `postulate`, `Admitted` and `sorry` each fail the proof gate + +|`tests/golden/check_controls_test.sh` +|Pass in the same CI run +|`just check` fails on a stale view and on a failing proof + +|`tests/shape/` (2 files) +|Both pass +|The root matches its allow-list; the repository map is deterministic and +current |=== -== Completed Work (CRG C - Testing & Benchmarking) - -=== Template Validation Script ✅ - -* [x] `scripts/validate-template.sh` — 8-phase validation -** Phase 1: Core repository structure (root files, directories) -** Phase 2: Machine-readable metadata (`.machine_readable/`) -** Phase 3: GitHub Actions workflows (17 required + all present) -** Phase 4: Idris2 ABI and Zig FFI source files -** Phase 5: Placeholder token replacement (skipped in template) -** Phase 6: SPDX license headers (100% coverage, 6/6 files) -** Phase 7: Build system verification (`zig build` + `idris2` syntax check) -** Phase 8: Documentation requirements (TOPOLOGY, ABI-FFI-README, etc) -* Status: *PASSING* (0 errors, 3 warnings about template placeholders) - -=== E2E Template Instantiation Test ✅ - -* [x] `tests/e2e/template_instantiation_test.sh` — full workflow -** Clones template to temp directory -** Runs the real `just repo-init` (never a second copy of its substitution list) -** Validates resulting structure with `scripts/validate-template.sh` -** Verifies Zig build works after instantiation -** Checks no placeholder survives, via `scripts/check-no-placeholders.sh` -** Cleans up temp directory - -NOTE: this entry read `[x]` from the day it was written until 2026-07-17, while -the test aborted at its first substitution line (`file: unbound variable`) on -every invocation. Nothing noticed: CI ran `tests/e2e.sh`, which did not call it, -and its only caller — `benches/template_bench.sh` — pipes it to `/dev/null` and -appends `|| true`, so it was timing a script that died instantly. The tick was -copied from the test's intent, not from a run. Tick these boxes from observed -output only. -* Status: *READY TO TEST* (can be verified by CI) - -=== Workflow Validation Test ✅ - -* [x] `tests/workflows/validate_workflows_test.sh` -** Validates all 21 workflows exist and have proper structure -** Checks SPDX headers, `name` field -** Verifies all 15 required workflows present -* Status: *PASSING* (0 errors, 15/15 required workflows found) - -=== Zig FFI Tests ✅ - -* [x] `src/interface/ffi/test/integration_test.zig` — template with examples -** Converted from `mathesis` placeholders to "template" namespace -** Added comprehensive comments for how to instantiate -** Tests grouped by category (lifecycle, operations, strings, errors, version, memory safety, threading) -** Compiles and passes placeholder test -* Status: *PASSING* (1 test: `placeholder_test_implementation_required` passes) - -=== Benchmarks ✅ - -* [x] `benches/template_bench.sh` — 5 benchmark suites -** Validation script: ~5.8s average (3 runs) -** Zig build: ~19ms (clean build) -** Zig tests: ~20ms -** Workflow validation: ~117ms -** Template instantiation: ~427ms -* Formats: human, json, csv -* Status: *PASSING* (all benchmarks execute) - -=== Build System ✅ - -* [x] `src/interface/ffi/build.zig` — updated for Zig 0.15.2 -** Simplified to test-only configuration -** Supports both unit tests and integration tests -** Works with `zig build` without errors -* Status: *PASSING* (builds successfully) - -== Test Results Summary - ----- -Validation Script: PASS (0 errors, 3 warnings) -Workflow Validation: PASS (21/21 workflows valid) -Integration Tests: PASS (1/1 placeholder test) -E2E Instantiation: READY (needs CI confirmation) -Benchmarks: PASS (5/5 benchmark suites) -Build System: PASS (zig build succeeds) ----- - -== CRG C Compliance - -* *Coverage*: 6/6 test categories (unit, integration, E2E, workflow, validation, benchmarks) -* *Documentation*: All test files have SPDX headers + inline documentation -* *Author Attribution*: Jonathan D.A. Jewell <6759885+hyperpolymath@users.noreply.github.com> -* *License*: MPL-2.0 on all new files -* *Automation*: All scripts executable + working - -== FLAGGED ISSUES - ALL RESOLVED - -* [.line-through]#*Template repo used by ALL new repos has 0 validation tests*# → FIXED: 4 test suites + validation script -* [.line-through]#*fuzz/placeholder.txt*# → FIXED: replaced with `README.adoc` containing real harness instructions -* [.line-through]#*No E2E tests for template instantiation*# → FIXED: full E2E test suite -* [.line-through]#*Zig FFI integration tests are placeholders*# → FIXED: converted to documented template format - -== Next Steps (Future Sessions) - -* [ ] Integrate test scripts into CI/CD workflows -* [ ] Generate test coverage reports -* [ ] Add more specialized benchmarks (memory, threading stress) -* [ ] Document test instantiation patterns for new repos - -== Priority: P0 (COMPLETE) ✅ +`just check-views` runs the census, atlas and registry suites; CI runs +`just check` and both control tests in the pinned Guix shell +(`.github/workflows/agda-proof-policy.yml`). The other tests under `tests/` +(`workflows/`, `e2e/`, the proven suite) check the template scaffold, not a +Mathesis part. + +== Needs + +* *A dogfood log.* No dated record shows the census and the registry in use + over an evidence window (needed for CRG C). +* *A live census test.* Every census test is offline. No test clones a real + repository, so a change in the GitHub clone behaviour shows only in the + next full census. +* *Applied shelf.* No test exists, because no executable component exists + (WO 4.2). +* *Contract probes.* The six `must` probes have no runner; a test that runs + them in CI would turn the contract into a gate. diff --git a/docs/troubleshooting.adoc b/docs/troubleshooting.adoc index 8d591680..4d0fc95e 100644 --- a/docs/troubleshooting.adoc +++ b/docs/troubleshooting.adoc @@ -1,58 +1,62 @@ // SPDX-License-Identifier: CC-BY-SA-4.0 // Copyright (c) Jonathan D.A. Jewell // SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) <6759885+hyperpolymath@users.noreply.github.com> -= Troubleshooting — Mathesis -:revdate: 2026-MM-DD += Troubleshooting Mathesis -This file is a *living FAQ* — known failure modes and recovery paths. -Add a new entry every time you debug something that took more than 15 -minutes; future-you (and other maintainers) will thank you. +Known failures and their fixes. Each entry was met in practice; add one when +a failure takes real time to diagnose. -== Known failure modes +== `just` fails on `provision::build` -=== `` +*Symptom*: `error: Expected '&&', comment, end of file, ... but found '::'`. -**Symptom**: short reproduction. What does the user see? +*Cause*: an old `just` that does not know module paths. -**Cause**: root cause (one or two sentences). +*Fix*: use the version that `mise.lock` pins (1.56.0), and check its +checksum against `mise.lock`. -**Fix**: -[source,bash] ----- - ----- +== `validate-claude-md` or `validate-coapt` fails with `nickel: command not found` -**Avoidance**: how to not hit this again (config setting, doc link, etc.). +*Fix*: install Nickel 1.18.0. CI checks the release binary against the +SHA-256 in `.github/workflows/dogfood-gate.yml`. ---- +== `validate-coapt` reports `DRIFT` -=== `` +*Cause*: a contractile or a deed clause changed, and the receipt was not +regenerated. -(Replace this and the above example with real entries as you encounter -them.) +*Fix*: run `just coapt` and commit the receipt. Never edit the receipt by +hand. -== Diagnostic toolkit +== The registry stops with `set MATHESIS_STANDARDS` -When something is wrong, run these first: +*Fix*: point `MATHESIS_STANDARDS` at a `metadatastician/standards` checkout +whose reader file has the digest that `READER` in +`scripts/registry/claims-registry.mjs` names. -[source,bash] ----- -just doctor # runs all available self-checks -just version # prints the version & build hash -just log-tail # last N lines of logs ----- +== The canon capability checker reports `no profile at .../rsr-profile.a2ml` -== When to escalate +*Cause*: the copy of `check-rsr-profile.sh` at the CI pin of `standards` +still reads the retired `.a2ml` profile. -. Filed an issue with: version, OS, exact command, full error output, - and the symptom in plain English. -. Linked from the issue: the relevant ADR(s) and any related issues. -. For *security*-relevant findings, see - link:./../SECURITY.md[SECURITY.md] — do **not** file public issues. +*Fix*: run the checker from `standards` main, which reads the deed's +`(rsr-profile)` clause. Without network access to the Actions API, omit the +`owner/repo` argument; the checker then skips its live step. -== Where to look for more help +== `scripts/check-proofs.sh agda` fails on `--print-agda-data-dir` -* `docs/architecture.adoc` — internals. -* `docs/decisions/` — historical record of why things are this shape. -* `https://github.com/hyperpolymath/Mathesis/issues?q=is%3Aissue+` — has anyone hit this before? -* `https://github.com/hyperpolymath/standards/issues` — for estate-wide problems. +*Cause*: Agda older than 2.7.0.1. + +*Fix*: run the proof checks in the pinned Guix shell (see +link:contributing.adoc[contributing]). + +== `just validate-repo-map` reports a stale map + +*Cause*: a tracked path was added, moved or removed. + +*Fix*: run `just repo-map` and commit `docs/architecture/REPOSITORY-MAP.adoc`. + +== `just crg-grade` prints `X` + +*Cause*: the template recipe reads `READINESS.md` at the root, which does +not exist. The grade is in `docs/status/READINESS.adoc`. diff --git a/docs/usage.adoc b/docs/usage.adoc index 3c2497fc..5ec4395a 100644 --- a/docs/usage.adoc +++ b/docs/usage.adoc @@ -1,82 +1,57 @@ // SPDX-License-Identifier: CC-BY-SA-4.0 // Copyright (c) Jonathan D.A. Jewell // SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) <6759885+hyperpolymath@users.noreply.github.com> -= Usage — Mathesis -:revdate: 2026-MM-DD += Using Mathesis -== Audience +This guide is for a reader who wants to find proofs in the estate, or an +agent that needs a small, sourced context. To work on Mathesis itself, see +link:contributing.adoc[contributing]. -This document is for *consumers* of `Mathesis` — people who depend -on it, call it, or include it. For developers working *on* it, see -link:./contributing.adoc[contributing.adoc]. +== Read the atlas -== Quickstart +The views are generated files; read them in place. -The shortest path from zero to a working call: +* `docs/atlas/generated/catalogue.adoc`: one row for each repository with + proof files of its own, split into theory and engineering. +* `docs/atlas/generated/az.adoc` and `organisations.adoc`: the same rows by + name and by owner. +* `docs/atlas/generated/registry.adoc`: theorem-level claims, each with the + grade that the canon reader derives from its home's receipt. +* `docs/atlas/generated/bridges.adoc`: candidate relations between two + repositories. +* `docs/atlas/generated/index.json`: the rows as one I-JSON/JCS document. -[source,bash] ----- -# 1. Install -just install # or: cargo install --path . / task install - -# 2. Configure -cp examples/config.example.toml ./config.toml -# Edit minimal required fields. +== Find a source -# 3. Run -just run # or the equivalent for your language ----- - -Expected output: +`find` lists the rows that match every word of a query, in repository name, +class, provers or status document. -[source] +[source,bash] ---- -Mathesis v0.0.0 -Listening on 127.0.0.1:8080 +bun scripts/atlas/census-atlas.mjs find agda ---- -== Common use cases - -For each canonical use case, give: - -. A one-line statement of the goal. -. The minimal invocation. -. Expected output / side effect. - -=== Use case 1: - -(Replace with real content.) - -=== Use case 2: +The output is a JSON array of rows (57 for `agda` on 2026-11-11). -== Configuration reference +== Build a bounded context -Document every configurable field. Keep this section authoritative — if -the code grows a new option, this table must grow too (CI can be wired -to enforce this). +`context` returns the matching rows as a JSON document no longer than +`MATHESIS_CONTEXT_CHARS` characters (default 5000). It always carries a +caveat that counts are not verification. -[cols="1,1,1,3", options="header"] -|=== -| Field | Type | Default | Meaning - -| `` | `` | `` | -|=== - -== Stability guarantees - -Be explicit: - -* **Stable**: API surfaces that follow SemVer (breaking change = major bump). -* **Unstable**: behind a flag / pre-1.0 / explicitly marked. -* **Internal**: documented for reference but no compatibility promise. - -== Limits & known constraints - -* Maximum supported ``: ``. -* `` is not yet implemented; track at issue `#`. -* On ``, `` behaves differently because ``. - -== See also +[source,bash] +---- +MATHESIS_CONTEXT_CHARS=1200 bun scripts/atlas/census-atlas.mjs context lean +---- -* link:./architecture.adoc[Architecture] — how it works internally. -* link:./troubleshooting.adoc[Troubleshooting] — when things go wrong. +== Limits + +* Counts are textual: the census finds declarations by keyword, and holes + and axioms by pattern. The kernel of each home repository is the + authority. +* A row is as fresh as its `censused_at` time; the source commit is in + `commit`. +* The frame holds public repositories only. Private repositories are a + count in `docs/atlas/census/private-count.json`. +* No grade in the atlas is typed by hand. A theorem without a receipt that + the canon reader accepts reads `ungraded`. diff --git a/mathesis_chora.deed b/mathesis_chora.deed index b5cecd0c..5c70f37f 100644 --- a/mathesis_chora.deed +++ b/mathesis_chora.deed @@ -633,14 +633,16 @@ :strictness "high") ; Files that are strictly allowed to exist at the root. CLAUDE.md is the ; generated arrival pack; git/Claude/pre-commit all read it from the ROOT. + ; EXPLAINME.adoc sits at the root by the README and EXPLAINME authoring + ; standard (owner ruling 2026-11-11, re-anchoring plan WO 3.4). ; The pattern ".*" allows hidden dotfiles implicitly; RRA checks specific ; dotfile rules below. (allow-list - :files ("README.adoc" "CHANGELOG.adoc" "Justfile" "LICENSE" "mathesis_chora.deed" "CITATION.cff" "CLAUDE.md") + :files ("README.adoc" "EXPLAINME.adoc" "CHANGELOG.adoc" "Justfile" "LICENSE" "mathesis_chora.deed" "CITATION.cff" "CLAUDE.md") :patterns (".*")) ; Relocation rules: move heavy prose out of the root (relocations - (move :pattern "*.adoc" :dest "docs/" :except ("README.adoc" "CHANGELOG.adoc")) + (move :pattern "*.adoc" :dest "docs/" :except ("README.adoc" "EXPLAINME.adoc" "CHANGELOG.adoc")) (move :pattern "GOVERNANCE.*" :dest "docs/") (move :pattern "ARCHITECTURE.*" :dest "docs/") (move :file "MAINTAINERS.adoc" :dest "docs/")) @@ -1025,12 +1027,18 @@ "tests/golden/check_controls_test.sh" "verification/proofs/agda/FeatureReachability.agda" "verification/proofs/coq/FeatureReachability.v" - "verification/proofs/lean4/FeatureReachability.lean") + "verification/proofs/lean4/FeatureReachability.lean" + "EXPLAINME.adoc") :removed ("archetypes/" "build/docs-seed/" "build/templates/" "rsr-template-repo_chora.deed" "src/interface/" "benches/" "build/container/Containerfile" "tests/ffi_strings_test.sh" ".github/workflows/rust-ci.yml" ".github/workflows/release.yml") + ; .github/labels.json and .github/label-classifier.json: their + ; _generated_from no longer names a private repository (WO 3.5). + ; docs/EXPLAINME.adoc is a pointer to the root EXPLAINME (WO 3.4). :diverged ("mathesis_chora.deed" "docs/status/ROADMAP.adoc" + ".github/labels.json" ".github/label-classifier.json" + "docs/EXPLAINME.adoc" ".machine_readable/root-allow.txt" "Justfile" "scripts/run-proven-suite.sh" "tests/run_proven_suite_test.sh" "tests/proven_suite_test.sh" ".github/workflows/actions.lock")))