diff --git a/.github/workflows/proven-tests.yml b/.github/workflows/proven-tests.yml index fb802367..7ea8f997 100644 --- a/.github/workflows/proven-tests.yml +++ b/.github/workflows/proven-tests.yml @@ -49,6 +49,14 @@ jobs: run: | bun scripts/atlas/census-atlas.mjs check bun test tests/atlas/census-atlas.test.mjs + # The claims registry (docs/decisions/0004-claims-registry.adoc): re-derive + # every grade from the home repositories' receipts at their pinned commits + # (fetched, digest-checked) and fail if the committed view is stale or a + # receipt asserts a grade its evidence does not support. + - name: Mathesis claims registry derivation and tests + run: | + bun scripts/registry/claims-registry.mjs check + bun test tests/registry/claims-registry.test.mjs - name: Install verified Nickel 1.18.0 (K9 L2 semantics) run: | set -euo pipefail diff --git a/Justfile b/Justfile index aaaeded8..0b8388b9 100644 --- a/Justfile +++ b/Justfile @@ -738,3 +738,13 @@ atlas-check: atlas-find query: bun scripts/atlas/census-atlas.mjs find "{{query}}" + +# Theorem-level claims registry (ADR 0004): fetch each pinned receipt, derive +# Proof Witness Grades, and write docs/registry/registry.adoc +registry: + bun scripts/registry/claims-registry.mjs build + +# Fail if the committed registry view is stale or a receipt overstates its grade +registry-check: + bun scripts/registry/claims-registry.mjs check + bun test tests/registry/claims-registry.test.mjs diff --git a/README.adoc b/README.adoc index 2aec13fe..a189f38d 100644 --- a/README.adoc +++ b/README.adoc @@ -19,6 +19,7 @@ in Rocq and Lean). The working method is the proof-craft skill. * 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/registry/registry.adoc[Claims registry, pilot slice] — theorem-level, grades *derived* from home-repository receipts at pinned commits; proposed in link:docs/decisions/0004-claims-registry.adoc[ADR 0004], not yet ratified. * 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/architecture/REPOSITORY-MAP.adoc[Generated repository map] — current path inventory, not the mathematical architecture specification. diff --git a/docs/architecture/REPOSITORY-MAP.adoc b/docs/architecture/REPOSITORY-MAP.adoc index d28ba7e4..e2cc583c 100644 --- a/docs/architecture/REPOSITORY-MAP.adoc +++ b/docs/architecture/REPOSITORY-MAP.adoc @@ -117,6 +117,10 @@ predecessors did. | yes | - +| `applied-systems/` +| yes +| owner-requested reusable applications area (2026-11-07) + | `benches/` | optional | Cargo-conventional at package root @@ -204,6 +208,11 @@ your own repo - but do not read their emptiness as neglect here. | `.machine_readable/bot_directives/` | `.machine_readable/descriptiles/anchors/` | `.machine_readable/scripts/verification/` +| `applied-systems/decision-science/` +| `applied-systems/finance/` +| `applied-systems/finance/cohort-economics/` +| `applied-systems/finance/liquidity/` +| `applied-systems/organisational-design/` | `docs/governance/audit/` | `docs/governance/audit/compliance/` | `docs/governance/audit/effects/` diff --git a/docs/atlas/README.adoc b/docs/atlas/README.adoc index 52675ae3..4ddd703e 100644 --- a/docs/atlas/README.adoc +++ b/docs/atlas/README.adoc @@ -18,5 +18,7 @@ Proof declarations, axioms and holes are *counts found by the original census*. They are not kernel-check receipts; source files are not included in the summarised rows, so this atlas must not invent per-theorem names, evidence, proof status, assumptions, equivalence, or independent verification. -The next slice requires a separately reviewed, source-anchored claims registry. +The next slice requires a separately reviewed, source-anchored claims registry; +it is proposed in link:../decisions/0004-claims-registry.adoc[ADR 0004] +(pilot view: link:../registry/registry.adoc[`docs/registry/registry.adoc`]). No private-source records are added or published by this generator. diff --git a/docs/decisions/0004-claims-registry.adoc b/docs/decisions/0004-claims-registry.adoc new file mode 100644 index 00000000..76466978 --- /dev/null +++ b/docs/decisions/0004-claims-registry.adoc @@ -0,0 +1,149 @@ +// SPDX-License-Identifier: CC-BY-SA-4.0 +// Copyright (c) Jonathan D.A. Jewell += Architecture Decision Record: 0004-claims-registry + +== 4. A theorem-level claims registry that derives grades and never assigns them + +Date: 2026-11-09 + +=== Status + +*Proposed — awaiting owner ratification.* Nothing here is estate policy until +the owner rules on it. Ratification is the owner's merge of the pull request +that introduces this file, with this Status changed to `Accepted (ratified by +owner )` in the same change. Until then the registry view +(`docs/registry/registry.adoc`) says on its face that the slice is proposed. + +=== Context + +The atlas (`docs/atlas/README.adoc`) stops at repository-level counts and says +so: "The next slice requires a separately reviewed, source-anchored claims +registry." The architecture brief +(`docs/proposals/estate-mathematical-architecture.adoc`) names that slice as +Stage 1 (schema decision) and Stage 4 (proof-level indexing), with `registry/` +and `schemas/` directories; its proof grades were adopted, corrected, as +`PROOF-POLICY.adoc` §8 (owner ruling 2026-11-04), which binds what a registry +may say: + +* §8.4: grades are *derived*, not asserted; a hand-written grade the receipts + do not support is drift; a census, never a percentage. +* §8.5: each theorem's grade is recorded in its *home repository*; "Mathesis + may catalogue grades. It derives them from those receipts and does not assign + them." +* `docs/standards/AUTHORITY.adoc` (this repository): pin claims to source + commits, checker versions, assumptions and receipts; never infer a missing + field from a green badge; proof receipts stay in their home repositories. + +So the registry's job is narrow: point at a claim in its home repository at an +exact commit, fetch that repository's own machine receipt, recompute the grade +by §8.2, and report disagreements. It is a checker of home-repository claims, +not a second ledger. + +=== Decision + +==== Record (the schema) + +`docs/registry/claims.json` is one I-JSON/JCS array. Each record has exactly +these fields; `scripts/registry/claims-registry.mjs` `validate` enforces them +and the tests prove each failure. + +[cols="1,3",options="header"] +|=== +|Field |Meaning + +|`id` |`/#`; unique. +|`repo` |The home repository. It must be `public` in +`docs/catalogue/census/repos.json`: the registry never names a private +repository, so it cannot leak one (brief §7). +|`claim` |The claim's id in the home repository's proof-status file (`N-7`, `L-6`). +|`kind` |`theorem` (graded, §8.1), `demonstration` (a TESTED example) or `assumption` +(an ASSUMED hypothesis). Only theorems are graded. +|`statement` |The statement in the home repository's own wording. Mathesis +does not restate mathematics. +|`status_doc` |The home repository's proof-status file. +|`agda` |For a theorem: `{module, names}`, the Agda source of truth (§1). `null` +otherwise. +|`source_commit` |The full 40-character commit the record describes. +|`receipt` |`{path, sha256}` of the home repository's machine receipt at that +commit, or `null` when it has none. +|=== + +A record holds *no grade, token, leg or flag*. Those are read from the receipt. + +==== Derivation (PROOF-POLICY §8.1–§8.2) + +For each record, the tool fetches the receipt at `source_commit`, refuses it +if its sha256 differs from the pinned digest, and derives: + +. not a theorem → `ungraded` (§8.1); +. no receipt, or the claim absent from it → `ungraded`; +. the receipt's flags lack any of `--safe --without-K --cubical-compatible` → + `ungraded` (§2.1 is a condition of `PWG-3`); +. the Agda token is not `proven` or `proven-with-postulates` → `ungraded`; +. otherwise `PWG-3`, `PWG-2i` or `PWG-2ii` by the number of legs whose §2.2 + state is `RECONCILED`. A leg's route never counts on its own. + +`PWG-1` is never derived in this slice: it needs a current receipt for every +counted witness, and the slice reads only the Agda-side receipt. + +Two kinds of disagreement are reported. A receipt that asserts a `:pwg` its +evidence does not support is *drift* (§8.4) and fails the check. A receipt that +still uses the pre-§8 vocabulary (`:grade "grade-3"`) is a visible *finding*, +not a failure: the vocabulary changed after the receipt was written. + +==== View, gate and tooling + +* `docs/registry/registry.adoc` is generated (`just registry`) and checked + (`just registry-check`, and CI `proven-tests.yml`): stale view, digest + mismatch, or drift fails. The view opens with a §8.4.7 census line. +* The tool is Bun, beside the atlas (`scripts/atlas/census-atlas.mjs`), with + hermetic tests (`tests/registry/claims-registry.test.mjs`, `--receipts-dir` + fixtures): the ladder, each withheld reason, drift versus legacy finding, + digest refusal, validation failures, and "never a percentage". +* Receipts are fetched from `raw.githubusercontent.com` at the pinned commit, + never vendored (AUTHORITY: receipts stay home). + +==== Pilot rows + +Seventeen claims from the two repositories whose proofs this work audited: +`hyperpolymath/secret-types` (N-1 to N-9) and `metadatastician/lintel` (L-1 to +L-7, A-1), each pinned at its `main` of 2026-11-09. At those commits the +derivation gives *0 of 12 theorems graded*, and says why: + +* secret-types `eee4e40`: the receipt records the flag set without + `--cubical-compatible` (waiver W-1), and uses the pre-§8 "grade-3" wording. + hyperpolymath/secret-types#32 puts the flag in force and writes the §8.5 + receipt; once it merges, bumping the pin should derive `PWG-3`. +* Lintel `a0f2bae`: no machine receipt exists in the repository. + +That the pilot reports zero is the point: it is what the evidence supports today. + +=== Alternatives considered + +* *Store grades in the registry.* Rejected: §8.4 and §8.5 forbid assigning + them, and a stored grade drifts silently when the home repository moves. +* *Vendor receipts into Mathesis.* Rejected: AUTHORITY keeps receipts home; + a pinned digest gives the same tamper-evidence without a copy. +* *A JSON Schema file validated by a library.* Deferred: it adds a pinned npm + dependency for checks the 40-line `validate` already makes and tests. A + schema file can be generated from `validate` later if a consumer needs one. +* *A ruling in `standards` first.* Possible, slower: the registry's authority + would sit beside PROOF-POLICY §8.5. Chosen instead: ratify here, because the + registry only *reads* the policy and adds no rule to it. + +=== Consequences + +* Mathesis can answer "which theorems, at which grade, why not higher" for the + piloted repositories, with every answer traceable to a commit and a digest. +* A home repository whose receipt overstates its grade turns this repository's + CI red. That is intended (§8.4.2: "a gate or a bot may recompute it at any + time and reports the computed value"). +* The census rows and the atlas are unchanged; the registry sits beside them. +* After ratification, in order: + . Lintel: move its real ledger into `docs/status/PROOF-STATUS.adoc`, retire + the template boilerplate, adopt the §2.1 invocation and add a receipt; + . `scripts/census/build-rows.sh`: prefer `PROOF-STATUS` over `PROOF-NEEDS` + when choosing a repository's status document, then refresh the two rows; + . list both repositories as the first §2 reconciliation pilot in + `docs/status/CROSS-PROVER-RECONCILIATION.adoc`; + . bump the pilot pins as those changes land. diff --git a/docs/registry/claims.json b/docs/registry/claims.json new file mode 100644 index 00000000..0edce2e4 --- /dev/null +++ b/docs/registry/claims.json @@ -0,0 +1 @@ +[{"agda":{"module":"SecretTypes.Noninterference","names":["tini"]},"claim":"N-1","id":"hyperpolymath/secret-types#N-1","kind":"theorem","receipt":{"path":"verification/receipts/agda-grade3_praxis.deed","sha256":"72525272e723ac23a62ef22914a6b1777b8a6f639682ef2c69c12129c2356025"},"repo":"hyperpolymath/secret-types","source_commit":"eee4e4038503f098c31181e792f66834eda5f523","statement":"TINI at the two-point lattice: two finishing runs of a well-typed command from low-equivalent stores end low-equivalent, fuels independent","status_doc":"PROOF-STATUS.adoc"},{"agda":{"module":"SecretTypes.Noninterference","names":["eval-low"]},"claim":"N-2","id":"hyperpolymath/secret-types#N-2","kind":"theorem","receipt":{"path":"verification/receipts/agda-grade3_praxis.deed","sha256":"72525272e723ac23a62ef22914a6b1777b8a6f639682ef2c69c12129c2356025"},"repo":"hyperpolymath/secret-types","source_commit":"eee4e4038503f098c31181e792f66834eda5f523","statement":"Public expressions read the same in low-equivalent stores","status_doc":"PROOF-STATUS.adoc"},{"agda":{"module":"SecretTypes.Noninterference","names":["confine"]},"claim":"N-3","id":"hyperpolymath/secret-types#N-3","kind":"theorem","receipt":{"path":"verification/receipts/agda-grade3_praxis.deed","sha256":"72525272e723ac23a62ef22914a6b1777b8a6f639682ef2c69c12129c2356025"},"repo":"hyperpolymath/secret-types","source_commit":"eee4e4038503f098c31181e792f66834eda5f523","statement":"Confinement: under a secret program counter the public variable is unchanged, loops included","status_doc":"PROOF-STATUS.adoc"},{"agda":null,"claim":"N-4","id":"hyperpolymath/secret-types#N-4","kind":"demonstration","receipt":{"path":"verification/receipts/agda-grade3_praxis.deed","sha256":"72525272e723ac23a62ef22914a6b1777b8a6f639682ef2c69c12129c2356025"},"repo":"hyperpolymath/secret-types","source_commit":"eee4e4038503f098c31181e792f66834eda5f523","statement":"The typing side-condition is load-bearing: an explicit and an implicit flow are each refused and each actually leaks","status_doc":"PROOF-STATUS.adoc"},{"agda":null,"claim":"N-5","id":"hyperpolymath/secret-types#N-5","kind":"demonstration","receipt":{"path":"verification/receipts/agda-grade3_praxis.deed","sha256":"72525272e723ac23a62ef22914a6b1777b8a6f639682ef2c69c12129c2356025"},"repo":"hyperpolymath/secret-types","source_commit":"eee4e4038503f098c31181e792f66834eda5f523","statement":"Termination-insensitivity is real, not vacuous: a well-typed program spins on one secret and stops on another","status_doc":"PROOF-STATUS.adoc"},{"agda":null,"claim":"N-6","id":"hyperpolymath/secret-types#N-6","kind":"demonstration","receipt":{"path":"verification/receipts/agda-grade3_praxis.deed","sha256":"72525272e723ac23a62ef22914a6b1777b8a6f639682ef2c69c12129c2356025"},"repo":"hyperpolymath/secret-types","source_commit":"eee4e4038503f098c31181e792f66834eda5f523","statement":"Laws census: generic TINI uses exactly the two upper-bound laws and the observer's down-closure (law-ablation certificate)","status_doc":"PROOF-STATUS.adoc"},{"agda":{"module":"SecretTypes.Noninterference.Generic","names":["tini"]},"claim":"N-7","id":"hyperpolymath/secret-types#N-7","kind":"theorem","receipt":{"path":"verification/receipts/agda-grade3_praxis.deed","sha256":"72525272e723ac23a62ef22914a6b1777b8a6f639682ef2c69c12129c2356025"},"repo":"hyperpolymath/secret-types","source_commit":"eee4e4038503f098c31181e792f66834eda5f523","statement":"TINI over the Lattice record: for every variable set with decidable equality, lattice, labelling and down-closed observer, two finishing runs of a well-typed command from stores agreeing on what the observer sees end agreeing on it","status_doc":"PROOF-STATUS.adoc"},{"agda":{"module":"SecretTypes.Countermodels","names":["NoUpper₁.refutes","NoUpper₂.refutes","NoDownClosure.refutes","NoTrans.refutes"]},"claim":"N-8","id":"hyperpolymath/secret-types#N-8","kind":"theorem","receipt":{"path":"verification/receipts/agda-grade3_praxis.deed","sha256":"72525272e723ac23a62ef22914a6b1777b8a6f639682ef2c69c12129c2356025"},"repo":"hyperpolymath/secret-types","source_commit":"eee4e4038503f098c31181e792f66834eda5f523","statement":"Each census law is necessary: dropping an upper-bound law or observer down-closure admits a well-typed leaking program; transitivity is necessary for principal observers","status_doc":"PROOF-STATUS.adoc"},{"agda":{"module":"SecretTypes.Noninterference.OutcomeVisibility","names":["termination-sensitive-fails"]},"claim":"N-9","id":"hyperpolymath/secret-types#N-9","kind":"theorem","receipt":{"path":"verification/receipts/agda-grade3_praxis.deed","sha256":"72525272e723ac23a62ef22914a6b1777b8a6f639682ef2c69c12129c2356025"},"repo":"hyperpolymath/secret-types","source_commit":"eee4e4038503f098c31181e792f66834eda5f523","statement":"If an observer sees finishing versus not finishing, termination-sensitive noninterference is false for the current typing rules","status_doc":"PROOF-STATUS.adoc"},{"agda":{"module":"Lintel.Lattice","names":["⊑-refl","⊑-trans","⊑-antisym","⊔-upper₁","⊔-upper₂","⊔-least","⊓-lower₁","⊓-lower₂","⊓-greatest","anyone-least","no-one-greatest","no-one-⋢-anyone","_⊑?_"]},"claim":"L-1","id":"metadatastician/lintel#L-1","kind":"theorem","receipt":null,"repo":"metadatastician/lintel","source_commit":"a0f2bae9cac07cd97b2395d10d0eb05f8ae1c7d1","statement":"A lattice, not just a poset: ⊑ is a decidable partial order, ⊔ and ⊓ are least upper and greatest lower bounds, anyone is least and no-one greatest","status_doc":"README.adoc"},{"agda":{"module":"Lintel.Lattice","names":["⊑-readers","readers-⊑","observes-flow","flow-observes"]},"claim":"L-2","id":"metadatastician/lintel#L-2","kind":"theorem","receipt":null,"repo":"metadatastician/lintel","source_commit":"a0f2bae9cac07cd97b2395d10d0eb05f8ae1c7d1","statement":"⊑ is reverse inclusion of reader sets; a role sees a label exactly when the label may flow to that role's observer level","status_doc":"README.adoc"},{"agda":{"module":"Lintel.Instance","names":["reader-sets"]},"claim":"L-3","id":"metadatastician/lintel#L-3","kind":"theorem","receipt":null,"repo":"metadatastician/lintel","source_commit":"a0f2bae9cac07cd97b2395d10d0eb05f8ae1c7d1","statement":"The laws secret-types' generic TINI needs hold here, packed as an instance of its Lattice record","status_doc":"README.adoc"},{"agda":{"module":"Lintel.Lattice","names":["address-to-proxy","qname-to-target","link","link-confined"]},"claim":"L-4","id":"metadatastician/lintel#L-4","kind":"theorem","receipt":null,"repo":"metadatastician/lintel","source_commit":"a0f2bae9cac07cd97b2395d10d0eb05f8ae1c7d1","statement":"Address and query name each reach their own role; composed, only the client may observe them","status_doc":"README.adoc"},{"agda":null,"claim":"L-5","id":"metadatastician/lintel#L-5","kind":"demonstration","receipt":null,"repo":"metadatastician/lintel","source_commit":"a0f2bae9cac07cd97b2395d10d0eb05f8ae1c7d1","statement":"The typechecker refuses the self-defeating compositions and accepts the client's","status_doc":"README.adoc"},{"agda":{"module":"Lintel.Instance","names":["tini-per-role","tini-coalition"]},"claim":"L-6","id":"metadatastician/lintel#L-6","kind":"theorem","receipt":null,"repo":"metadatastician/lintel","source_commit":"a0f2bae9cac07cd97b2395d10d0eb05f8ae1c7d1","statement":"tini holds at this lattice over the address, the query name and the client's local state, for each role's observer and for any two roles observing together","status_doc":"README.adoc"},{"agda":{"module":"Lintel.Composition","names":["writes-flow","link-written-to-client","link-written-to-local","link-writable"]},"claim":"L-7","id":"metadatastician/lintel#L-7","kind":"theorem","receipt":null,"repo":"metadatastician/lintel","source_commit":"a0f2bae9cac07cd97b2395d10d0eb05f8ae1c7d1","statement":"Self-defeating privacy compositions cannot be built as programs: a typed command writes a value depending on both fields only into a variable the client alone may read","status_doc":"README.adoc"},{"agda":null,"claim":"A-1","id":"metadatastician/lintel#A-1","kind":"assumption","receipt":null,"repo":"metadatastician/lintel","source_commit":"a0f2bae9cac07cd97b2395d10d0eb05f8ae1c7d1","statement":"Non-collusion: no party holds both the proxy and the target role (the gap is proved: collusion-gap)","status_doc":"README.adoc"}] diff --git a/docs/registry/registry.adoc b/docs/registry/registry.adoc new file mode 100644 index 00000000..750de1f4 --- /dev/null +++ b/docs/registry/registry.adoc @@ -0,0 +1,52 @@ +// SPDX-License-Identifier: CC-BY-SA-4.0 +// GENERATED by scripts/registry/claims-registry.mjs from docs/registry/claims.json and +// the receipts it pins; do not hand-edit. += Claims registry (pilot slice) + +Each row is a claim in its home repository at a pinned commit. The grade is +*derived* here from that repository's receipt by PROOF-POLICY §8.2, never +assigned (§8.5). A grade is not a discharge (§8.4): `PWG-3` theorems still +owe their Rocq and Lean legs. Status of this slice: proposed in +link:../decisions/0004-claims-registry.adoc[ADR 0004], not ratified. + +Census: 0 at `PWG-1`, 0 at `PWG-2ii`, 0 at `PWG-2i`, 0 at `PWG-3`, 12 `ungraded`, of 12 theorems. 5 demonstrations and assumptions are listed and not graded. + +[cols="2,1,1,4,3",options="header"] +|=== +|Claim |Kind |PWG |Statement (home repository's wording) |Why not higher; findings + +|https://github.com/hyperpolymath/secret-types/blob/eee4e4038503f098c31181e792f66834eda5f523/PROOF-STATUS.adoc[hyperpolymath/secret-types#N-1] at `eee4e4038503` |theorem |`ungraded` |TINI at the two-point lattice: two finishing runs of a well-typed command from low-equivalent stores end low-equivalent, fuels independent (`SecretTypes.Noninterference`: `tini`) |not under the §2.1 invocation (missing --cubical-compatible); *Finding:* receipt uses the pre-§8 vocabulary (grade-3); derived ungraded + +|https://github.com/hyperpolymath/secret-types/blob/eee4e4038503f098c31181e792f66834eda5f523/PROOF-STATUS.adoc[hyperpolymath/secret-types#N-2] at `eee4e4038503` |theorem |`ungraded` |Public expressions read the same in low-equivalent stores (`SecretTypes.Noninterference`: `eval-low`) |not under the §2.1 invocation (missing --cubical-compatible); *Finding:* receipt uses the pre-§8 vocabulary (grade-3); derived ungraded + +|https://github.com/hyperpolymath/secret-types/blob/eee4e4038503f098c31181e792f66834eda5f523/PROOF-STATUS.adoc[hyperpolymath/secret-types#N-3] at `eee4e4038503` |theorem |`ungraded` |Confinement: under a secret program counter the public variable is unchanged, loops included (`SecretTypes.Noninterference`: `confine`) |not under the §2.1 invocation (missing --cubical-compatible); *Finding:* receipt uses the pre-§8 vocabulary (grade-3); derived ungraded + +|https://github.com/hyperpolymath/secret-types/blob/eee4e4038503f098c31181e792f66834eda5f523/PROOF-STATUS.adoc[hyperpolymath/secret-types#N-4] at `eee4e4038503` |demonstration |`ungraded` |The typing side-condition is load-bearing: an explicit and an implicit flow are each refused and each actually leaks |demonstration, not a theorem (§8.1) + +|https://github.com/hyperpolymath/secret-types/blob/eee4e4038503f098c31181e792f66834eda5f523/PROOF-STATUS.adoc[hyperpolymath/secret-types#N-5] at `eee4e4038503` |demonstration |`ungraded` |Termination-insensitivity is real, not vacuous: a well-typed program spins on one secret and stops on another |demonstration, not a theorem (§8.1) + +|https://github.com/hyperpolymath/secret-types/blob/eee4e4038503f098c31181e792f66834eda5f523/PROOF-STATUS.adoc[hyperpolymath/secret-types#N-6] at `eee4e4038503` |demonstration |`ungraded` |Laws census: generic TINI uses exactly the two upper-bound laws and the observer's down-closure (law-ablation certificate) |demonstration, not a theorem (§8.1) + +|https://github.com/hyperpolymath/secret-types/blob/eee4e4038503f098c31181e792f66834eda5f523/PROOF-STATUS.adoc[hyperpolymath/secret-types#N-7] at `eee4e4038503` |theorem |`ungraded` |TINI over the Lattice record: for every variable set with decidable equality, lattice, labelling and down-closed observer, two finishing runs of a well-typed command from stores agreeing on what the observer sees end agreeing on it (`SecretTypes.Noninterference.Generic`: `tini`) |not under the §2.1 invocation (missing --cubical-compatible); *Finding:* receipt uses the pre-§8 vocabulary (grade-3); derived ungraded + +|https://github.com/hyperpolymath/secret-types/blob/eee4e4038503f098c31181e792f66834eda5f523/PROOF-STATUS.adoc[hyperpolymath/secret-types#N-8] at `eee4e4038503` |theorem |`ungraded` |Each census law is necessary: dropping an upper-bound law or observer down-closure admits a well-typed leaking program; transitivity is necessary for principal observers (`SecretTypes.Countermodels`: `NoUpper₁.refutes`, `NoUpper₂.refutes`, `NoDownClosure.refutes`, `NoTrans.refutes`) |not under the §2.1 invocation (missing --cubical-compatible); *Finding:* receipt uses the pre-§8 vocabulary (grade-3); derived ungraded + +|https://github.com/hyperpolymath/secret-types/blob/eee4e4038503f098c31181e792f66834eda5f523/PROOF-STATUS.adoc[hyperpolymath/secret-types#N-9] at `eee4e4038503` |theorem |`ungraded` |If an observer sees finishing versus not finishing, termination-sensitive noninterference is false for the current typing rules (`SecretTypes.Noninterference.OutcomeVisibility`: `termination-sensitive-fails`) |not under the §2.1 invocation (missing --cubical-compatible); *Finding:* receipt uses the pre-§8 vocabulary (grade-3); derived ungraded + +|https://github.com/metadatastician/lintel/blob/a0f2bae9cac07cd97b2395d10d0eb05f8ae1c7d1/README.adoc[metadatastician/lintel#A-1] at `a0f2bae9cac0` |assumption |`ungraded` |Non-collusion: no party holds both the proxy and the target role (the gap is proved: collusion-gap) |assumption, not a theorem (§8.1) + +|https://github.com/metadatastician/lintel/blob/a0f2bae9cac07cd97b2395d10d0eb05f8ae1c7d1/README.adoc[metadatastician/lintel#L-1] at `a0f2bae9cac0` |theorem |`ungraded` |A lattice, not just a poset: ⊑ is a decidable partial order, ⊔ and ⊓ are least upper and greatest lower bounds, anyone is least and no-one greatest (`Lintel.Lattice`: `⊑-refl`, `⊑-trans`, `⊑-antisym`, `⊔-upper₁`, `⊔-upper₂`, `⊔-least`, `⊓-lower₁`, `⊓-lower₂`, `⊓-greatest`, `anyone-least`, `no-one-greatest`, `no-one-⋢-anyone`, `_⊑?_`) |no machine receipt in the home repository + +|https://github.com/metadatastician/lintel/blob/a0f2bae9cac07cd97b2395d10d0eb05f8ae1c7d1/README.adoc[metadatastician/lintel#L-2] at `a0f2bae9cac0` |theorem |`ungraded` |⊑ is reverse inclusion of reader sets; a role sees a label exactly when the label may flow to that role's observer level (`Lintel.Lattice`: `⊑-readers`, `readers-⊑`, `observes-flow`, `flow-observes`) |no machine receipt in the home repository + +|https://github.com/metadatastician/lintel/blob/a0f2bae9cac07cd97b2395d10d0eb05f8ae1c7d1/README.adoc[metadatastician/lintel#L-3] at `a0f2bae9cac0` |theorem |`ungraded` |The laws secret-types' generic TINI needs hold here, packed as an instance of its Lattice record (`Lintel.Instance`: `reader-sets`) |no machine receipt in the home repository + +|https://github.com/metadatastician/lintel/blob/a0f2bae9cac07cd97b2395d10d0eb05f8ae1c7d1/README.adoc[metadatastician/lintel#L-4] at `a0f2bae9cac0` |theorem |`ungraded` |Address and query name each reach their own role; composed, only the client may observe them (`Lintel.Lattice`: `address-to-proxy`, `qname-to-target`, `link`, `link-confined`) |no machine receipt in the home repository + +|https://github.com/metadatastician/lintel/blob/a0f2bae9cac07cd97b2395d10d0eb05f8ae1c7d1/README.adoc[metadatastician/lintel#L-5] at `a0f2bae9cac0` |demonstration |`ungraded` |The typechecker refuses the self-defeating compositions and accepts the client's |demonstration, not a theorem (§8.1) + +|https://github.com/metadatastician/lintel/blob/a0f2bae9cac07cd97b2395d10d0eb05f8ae1c7d1/README.adoc[metadatastician/lintel#L-6] at `a0f2bae9cac0` |theorem |`ungraded` |tini holds at this lattice over the address, the query name and the client's local state, for each role's observer and for any two roles observing together (`Lintel.Instance`: `tini-per-role`, `tini-coalition`) |no machine receipt in the home repository + +|https://github.com/metadatastician/lintel/blob/a0f2bae9cac07cd97b2395d10d0eb05f8ae1c7d1/README.adoc[metadatastician/lintel#L-7] at `a0f2bae9cac0` |theorem |`ungraded` |Self-defeating privacy compositions cannot be built as programs: a typed command writes a value depending on both fields only into a variable the client alone may read (`Lintel.Composition`: `writes-flow`, `link-written-to-client`, `link-written-to-local`, `link-writable`) |no machine receipt in the home repository + +|=== diff --git a/scripts/registry/claims-registry.mjs b/scripts/registry/claims-registry.mjs new file mode 100644 index 00000000..7dca65cb --- /dev/null +++ b/scripts/registry/claims-registry.mjs @@ -0,0 +1,237 @@ +// SPDX-License-Identifier: MPL-2.0 +// SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell +// +// The theorem-level claims registry (docs/decisions/0004-claims-registry.adoc). +// +// docs/registry/claims.json records only source-anchored facts about each claim: +// its home repository, its id there, the statement as the home repository +// words it, the Agda names, a full 40-character commit, and the path and +// sha256 of the home repository's machine receipt at that commit. It never +// records a grade. The grade is DERIVED here, from the receipt fetched at the +// pinned commit, by the rules of standards/3-practice/PROOF-POLICY.adoc §8.2, +// and rendered into docs/registry/registry.adoc. PROOF-POLICY §8.5: "Mathesis +// may catalogue grades. It derives them from those receipts and does not +// assign them." +// +// bun scripts/registry/claims-registry.mjs build fetch, derive, render +// bun scripts/registry/claims-registry.mjs check the same, and fail if the +// committed view differs +// +// --receipts-dir DIR reads receipts from DIR/__@/ +// instead of fetching them (the tests use it; CI fetches). +import {readFile, writeFile, mkdir} from 'node:fs/promises'; +import {createHash} from 'node:crypto'; +import {fileURLToPath} from 'node:url'; +import path from 'node:path'; + +const root = path.resolve(path.dirname(fileURLToPath(import.meta.url)), '../..'); +const claimsFile = path.join(root, 'docs/registry/claims.json'); +const reposFile = path.join(root, 'docs/catalogue/census/repos.json'); +const viewFile = path.join(root, 'docs/registry/registry.adoc'); + +const KINDS = new Set(['theorem', 'demonstration', 'assumption']); +const PROVEN = new Set(['proven', 'proven-with-postulates']); +// PROOF-POLICY §2.1: the canonical invocation; every flag must be in force. +const CANONICAL_FLAGS = ['--safe', '--without-K', '--cubical-compatible']; +const PWG = new Set(['3', '2i', '2ii', '1', 'ungraded']); + +// ── Validation of the registry rows ────────────────────────────────────────── + +// Throw unless every row is well formed and its repository is public in the +// census inventory (the registry never names a private repository). +export function validate(rows, inventory) { + if (!Array.isArray(rows)) throw new Error('docs/registry/claims.json must be an array'); + const visibility = new Map(inventory.map(r => [r.full_name, r.visibility])); + const seen = new Set(); + for (const r of rows) { + const where = r && r.id ? r.id : JSON.stringify(r); + if (typeof r.repo !== 'string' || !/^[-\w.]+\/[-\w.]+$/.test(r.repo)) throw new Error(`Invalid repo: ${where}`); + if (typeof r.claim !== 'string' || r.claim === '') throw new Error(`Missing claim id: ${where}`); + if (r.id !== `${r.repo}#${r.claim}`) throw new Error(`id must be repo#claim: ${where}`); + if (seen.has(r.id)) throw new Error(`Duplicate id: ${r.id}`); + seen.add(r.id); + if (!KINDS.has(r.kind)) throw new Error(`Unknown kind ${r.kind}: ${r.id}`); + if (typeof r.statement !== 'string' || r.statement.length < 10) throw new Error(`Missing statement: ${r.id}`); + if (typeof r.status_doc !== 'string' || r.status_doc === '') throw new Error(`Missing status_doc: ${r.id}`); + if (typeof r.source_commit !== 'string' || !/^[0-9a-f]{40}$/.test(r.source_commit)) throw new Error(`source_commit must be 40 lowercase hex: ${r.id}`); + if (r.kind === 'theorem') { + if (!r.agda || typeof r.agda.module !== 'string' || !Array.isArray(r.agda.names) || r.agda.names.length === 0) + throw new Error(`A theorem names its Agda module and names: ${r.id}`); + } + if (r.receipt !== null) { + if (!r.receipt || typeof r.receipt.path !== 'string' || !/^[0-9a-f]{64}$/.test(r.receipt.sha256 ?? '')) + throw new Error(`receipt is null or {path, sha256}: ${r.id}`); + } + if (visibility.get(r.repo) !== 'public') throw new Error(`Nonpublic or unlisted repository: ${r.id}`); + } + return rows; +} + +// ── Reading a home repository's receipt ────────────────────────────────────── + +// Parse a praxis-deed receipt into its flags and its claims. Both the §8.5 +// shape (`:pwg`, per-leg `(leg …)` forms) and the earlier shape (`:grade`, +// `:coq-leg`, `:lean-leg`) are read; nothing absent is invented. +export function parseReceipt(text) { + const flags = (text.match(/:flags "([^"]*)"/) || [, null])[1]; + const claims = new Map(); + const lines = text.split('\n'); + for (let i = 0; i < lines.length; i++) { + const m = lines[i].match(/\(claim :id "([^"]+)" :token "([^"]+)"(.*)$/); + if (!m) continue; + const rest = m[3]; + const field = k => (rest.match(new RegExp(`:${k} "([^"]*)"`)) || [, null])[1]; + const claim = {token: m[2], pwg: field('pwg'), legacyGrade: field('grade'), legs: []}; + for (let j = i + 1; j < lines.length; j++) { + const l = lines[j].match(/^\s*\(leg :prover "([^"]+)" :route "([^"]+)" :token "([^"]+)" :state "([^"]+)"/); + if (!l) break; + claim.legs.push({prover: l[1], route: l[2], token: l[3], state: l[4]}); + } + if (claim.legs.length === 0 && field('coq-leg') !== null) { + // The earlier shape records a route per leg and no §2.2 state. + claim.legs.push({prover: 'rocq', route: field('coq-leg'), token: null, state: null}); + claim.legs.push({prover: 'lean', route: field('lean-leg'), token: null, state: null}); + } + claims.set(m[1], claim); + } + return {flags, claims}; +} + +// ── The derivation: PROOF-POLICY §8.1–§8.2 ─────────────────────────────────── + +// Derive one row's Proof Witness Grade from its parsed receipt (or null). +// Returns {pwg, reasons, findings, legs}. `reasons` say why the grade is not +// higher; `findings` are disagreements between the receipt and the derivation. +export function derive(row, receipt) { + const reasons = [], findings = []; + if (row.kind !== 'theorem') return {pwg: 'ungraded', reasons: [`${row.kind}, not a theorem (§8.1)`], findings, legs: []}; + if (receipt === null) return {pwg: 'ungraded', reasons: ['no machine receipt in the home repository'], findings, legs: []}; + const claim = receipt.claims.get(row.claim); + if (!claim) return {pwg: 'ungraded', reasons: ['claim absent from the receipt'], findings, legs: []}; + const flags = (receipt.flags ?? '').split(/\s+/); + const missing = CANONICAL_FLAGS.filter(f => !flags.includes(f)); + let pwg; + if (missing.length) { + pwg = 'ungraded'; + reasons.push(`not under the §2.1 invocation (missing ${missing.join(' ')})`); + } else if (!PROVEN.has(claim.token)) { + pwg = 'ungraded'; + reasons.push(`Agda token is ${claim.token}, not proven`); + } else { + // A leg counts only when its §2.2 state is RECONCILED (§8.2). + const counted = claim.legs.filter(l => l.state === 'RECONCILED').length; + pwg = counted === 0 ? '3' : counted === 1 ? '2i' : '2ii'; + if (counted < 2) reasons.push(`${2 - counted} of the Rocq and Lean legs not RECONCILED`); + // PWG-1 needs a current per-commit receipt for every counted witness; + // this slice does not read witness receipts, so it never derives PWG-1. + } + if (claim.pwg !== null && claim.pwg !== pwg) + findings.push(`receipt asserts PWG ${claim.pwg}; derived ${pwg} (§8.4 drift)`); + if (claim.pwg === null && claim.legacyGrade !== null) + findings.push(`receipt uses the pre-§8 vocabulary (${claim.legacyGrade}); derived ${pwg === 'ungraded' ? 'ungraded' : 'PWG-' + pwg}`); + return {pwg, reasons, findings, legs: claim.legs}; +} + +// ── Fetching receipts at their pinned commits ──────────────────────────────── + +// Return the receipt text for a row, verified against its sha256, or null. +async function loadReceipt(row, receiptsDir) { + if (row.receipt === null) return null; + let text; + if (receiptsDir) { + text = await readFile(path.join(receiptsDir, `${row.repo.replace('/', '__')}@${row.source_commit}`, row.receipt.path), 'utf8'); + } else { + const url = `https://raw.githubusercontent.com/${row.repo}/${row.source_commit}/${row.receipt.path}`; + const res = await fetch(url); + if (!res.ok) throw new Error(`could not fetch ${url}: HTTP ${res.status}`); + text = await res.text(); + } + const digest = createHash('sha256').update(text).digest('hex'); + if (digest !== row.receipt.sha256) throw new Error(`receipt digest mismatch for ${row.id}: pinned ${row.receipt.sha256}, got ${digest}`); + return text; +} + +// Derive every row, fetching each distinct receipt once. +export async function deriveAll(rows, receiptsDir) { + const cache = new Map(); + const out = []; + for (const row of rows) { + const key = row.receipt === null ? null : `${row.repo}@${row.source_commit}/${row.receipt.path}`; + if (key !== null && !cache.has(key)) cache.set(key, parseReceipt(await loadReceipt(row, receiptsDir))); + out.push({row, ...derive(row, key === null ? null : cache.get(key))}); + } + return out; +} + +// ── Rendering ──────────────────────────────────────────────────────────────── + +const cell = s => String(s).replaceAll('|', String.raw`\|`).replaceAll('\n', ' '); +const label = p => (p === 'ungraded' ? '`ungraded`' : `\`PWG-${p}\``); + +// Render the derived registry as AsciiDoc: a census line (§8.4.7: counts per +// grade with the denominator, never a percentage), then one row per claim. +export function render(derived) { + for (const d of derived) if (!PWG.has(d.pwg)) throw new Error(`internal: bad pwg ${d.pwg}`); + const theorems = derived.filter(d => d.row.kind === 'theorem'); + const count = p => theorems.filter(d => d.pwg === p).length; + const census = ['1', '2ii', '2i', '3'].map(p => `${count(p)} at \`PWG-${p}\``).join(', ') + `, ${count('ungraded')} \`ungraded\`, of ${theorems.length} theorems`; + const ordered = [...derived].sort((a, b) => (a.row.repo + '#' + a.row.claim).localeCompare(b.row.repo + '#' + b.row.claim, 'en', {numeric: true})); + const out = [ + '// SPDX-License-Identifier: CC-BY-SA-4.0', + '// GENERATED by scripts/registry/claims-registry.mjs from docs/registry/claims.json and', + '// the receipts it pins; do not hand-edit.', + '= Claims registry (pilot slice)', + '', + 'Each row is a claim in its home repository at a pinned commit. The grade is', + '*derived* here from that repository\'s receipt by PROOF-POLICY §8.2, never', + 'assigned (§8.5). A grade is not a discharge (§8.4): `PWG-3` theorems still', + 'owe their Rocq and Lean legs. Status of this slice: proposed in', + 'link:../decisions/0004-claims-registry.adoc[ADR 0004], not ratified.', + '', + `Census: ${census}. ${derived.length - theorems.length} demonstrations and assumptions are listed and not graded.`, + '', + '[cols="2,1,1,4,3",options="header"]', + '|===', + '|Claim |Kind |PWG |Statement (home repository\'s wording) |Why not higher; findings', + '', + ]; + for (const d of ordered) { + const r = d.row; + const link = `https://github.com/${r.repo}/blob/${r.source_commit}/${r.status_doc}[${r.repo}#${r.claim}]`; + const at = `at \`${r.source_commit.slice(0, 12)}\``; + const names = r.agda ? ` (\`${cell(r.agda.module)}\`: ${r.agda.names.map(n => '`' + cell(n) + '`').join(', ')})` : ''; + const notes = [...d.reasons, ...d.findings.map(f => `*Finding:* ${f}`)].map(cell).join('; ') || '—'; + out.push(`|${link} ${at} |${r.kind} |${label(d.pwg)} |${cell(r.statement)}${names} |${notes}`, ''); + } + out.push('|===', ''); + return out.join('\n'); +} + +// ── Entry point ────────────────────────────────────────────────────────────── + +async function main() { + const [cmd, ...args] = process.argv.slice(2); + const i = args.indexOf('--receipts-dir'); + const receiptsDir = i >= 0 ? path.resolve(args[i + 1]) : null; + const rows = validate(JSON.parse(await readFile(claimsFile, 'utf8')), JSON.parse(await readFile(reposFile, 'utf8'))); + const derived = await deriveAll(rows, receiptsDir); + const drift = derived.flatMap(d => d.findings.filter(f => f.includes('§8.4 drift')).map(f => `${d.row.id}: ${f}`)); + if (drift.length) throw new Error('a receipt asserts a grade its evidence does not support:\n ' + drift.join('\n ')); + const view = render(derived); + if (cmd === 'build') { + await mkdir(path.dirname(viewFile), {recursive: true}); + await writeFile(viewFile, view); + console.log(`WROTE ${path.relative(root, viewFile)} (${rows.length} claims)`); + } else if (cmd === 'check') { + const committed = await readFile(viewFile, 'utf8').catch(() => ''); + if (committed !== view) throw new Error(`${path.relative(root, viewFile)} is stale; run: bun scripts/registry/claims-registry.mjs build`); + console.log(`PASS: claims registry derived from ${new Set(rows.map(r => r.repo + '@' + r.source_commit)).size} pinned source(s); view matches (${rows.length} claims)`); + } else { + console.error('usage: claims-registry.mjs build|check [--receipts-dir DIR]'); + process.exit(2); + } +} + +if (process.argv[1] && path.resolve(process.argv[1]) === fileURLToPath(import.meta.url)) { + main().catch(e => { console.error('ERROR: ' + e.message); process.exit(1); }); +} diff --git a/tests/registry/claims-registry.test.mjs b/tests/registry/claims-registry.test.mjs new file mode 100644 index 00000000..4f1195aa --- /dev/null +++ b/tests/registry/claims-registry.test.mjs @@ -0,0 +1,89 @@ +// SPDX-License-Identifier: MPL-2.0 +// SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell +import {test, expect} from 'bun:test'; +import {readFileSync, mkdtempSync, mkdirSync, writeFileSync} from 'node:fs'; +import {createHash} from 'node:crypto'; +import {tmpdir} from 'node:os'; +import path from 'node:path'; +import {validate, parseReceipt, derive, deriveAll, render} from '../../scripts/registry/claims-registry.mjs'; + +const rows = JSON.parse(readFileSync(new URL('../../docs/registry/claims.json', import.meta.url), 'utf8')); +const inventory = JSON.parse(readFileSync(new URL('../../docs/catalogue/census/repos.json', import.meta.url), 'utf8')); + +const commit = 'a'.repeat(40); +const theorem = {id: 'o/r#T-1', repo: 'o/r', claim: 'T-1', kind: 'theorem', statement: 'a statement of some length', + status_doc: 'PROOF-STATUS.adoc', source_commit: commit, agda: {module: 'M', names: ['t']}, receipt: null}; +const inv = [{full_name: 'o/r', visibility: 'public'}]; + +// A §8.5-shaped receipt with the given flags, token, asserted pwg and leg states. +const receipt = ({flags = '--safe --without-K --cubical-compatible -W error', token = 'proven', pwg = null, rocq = 'AGDA-VERIFIED', lean = 'AGDA-VERIFIED'} = {}) => + ` (prover\n :flags "${flags}")\n (claims\n` + + ` (claim :id "T-1" :token "${token}" :kind "theorem"${pwg === null ? '' : ` :pwg "${pwg}"`} :foundation-diverse #f\n` + + ` (leg :prover "rocq" :route "re-proved" :token "proven" :state "${rocq}" :receipts ())\n` + + ` (leg :prover "lean" :route "re-proved" :token "proven" :state "${lean}" :receipts ()))\n )\n`; + +test('the committed registry validates against the census inventory', () => { + expect(validate(rows, inventory).length).toBe(rows.length); + expect(rows.every(r => !('pwg' in r) && !('grade' in r))).toBe(true); // grades are derived, never stored +}); + +test('validation fails closed', () => { + expect(() => validate([theorem, theorem], inv)).toThrow(/Duplicate/); + expect(() => validate([{...theorem, source_commit: 'abc'}], inv)).toThrow(/40 lowercase hex/); + expect(() => validate([{...theorem, kind: 'machine-verified'}], inv)).toThrow(/Unknown kind/); + expect(() => validate([{...theorem, agda: null}], inv)).toThrow(/Agda module/); + expect(() => validate([{...theorem, id: 'o/r#X'}], inv)).toThrow(/repo#claim/); + expect(() => validate([theorem], [{full_name: 'o/r', visibility: 'private'}])).toThrow(/Nonpublic/); + expect(() => validate([{...theorem, receipt: {path: 'x', sha256: 'nope'}}], inv)).toThrow(/sha256/); +}); + +test('the ladder is derived from leg states (§8.2)', () => { + expect(derive(theorem, parseReceipt(receipt())).pwg).toBe('3'); + expect(derive(theorem, parseReceipt(receipt({rocq: 'RECONCILED'}))).pwg).toBe('2i'); + expect(derive(theorem, parseReceipt(receipt({rocq: 'RECONCILED', lean: 'RECONCILED'}))).pwg).toBe('2ii'); + // A checked but unbridged leg does not count. + expect(derive(theorem, parseReceipt(receipt({rocq: 'BRIDGE-PENDING', lean: 'COQ-CHECKED'}))).pwg).toBe('3'); + // This slice never derives PWG-1. + expect(derive(theorem, parseReceipt(receipt({rocq: 'RECONCILED', lean: 'RECONCILED'}))).pwg).not.toBe('1'); +}); + +test('each reason a grade is withheld', () => { + const noFlag = derive(theorem, parseReceipt(receipt({flags: '--safe --without-K'}))); + expect(noFlag.pwg).toBe('ungraded'); + expect(noFlag.reasons.join()).toContain('missing --cubical-compatible'); + expect(derive(theorem, parseReceipt(receipt({token: 'open'}))).pwg).toBe('ungraded'); + expect(derive(theorem, null).reasons.join()).toContain('no machine receipt'); + expect(derive({...theorem, claim: 'T-9'}, parseReceipt(receipt())).reasons.join()).toContain('absent'); + expect(derive({...theorem, kind: 'demonstration'}, parseReceipt(receipt())).pwg).toBe('ungraded'); +}); + +test('an asserted grade the evidence does not support is drift; legacy vocabulary is a finding', () => { + const over = derive(theorem, parseReceipt(receipt({pwg: '2i'}))); + expect(over.findings.join()).toContain('§8.4 drift'); + expect(derive(theorem, parseReceipt(receipt({pwg: '3'}))).findings).toEqual([]); + const legacy = parseReceipt(' :flags "--safe --without-K"\n (claim :id "T-1" :token "proven" :grade "grade-3" :coq-leg "unavailable" :lean-leg "unavailable")\n'); + const d = derive(theorem, legacy); + expect(d.pwg).toBe('ungraded'); + expect(d.findings.join()).toContain('pre-§8 vocabulary'); + expect(d.findings.join()).not.toContain('drift'); +}); + +test('a receipt that does not match its pinned digest is refused', async () => { + const dir = mkdtempSync(path.join(tmpdir(), 'registry-')); + const text = receipt(); + mkdirSync(path.join(dir, `o__r@${commit}`), {recursive: true}); + writeFileSync(path.join(dir, `o__r@${commit}`, 'r.deed'), text); + const good = {...theorem, receipt: {path: 'r.deed', sha256: createHash('sha256').update(text).digest('hex')}}; + expect((await deriveAll([good], dir))[0].pwg).toBe('3'); + await expect(deriveAll([{...good, receipt: {path: 'r.deed', sha256: 'b'.repeat(64)}}], dir)).rejects.toThrow(/digest mismatch/); +}); + +test('the view is a census with its denominator, never a percentage, and is deterministic', () => { + const ds = [{row: theorem, pwg: '3', reasons: [], findings: [], legs: []}, + {row: {...theorem, id: 'o/r#T-2', claim: 'T-2'}, pwg: 'ungraded', reasons: ['x'], findings: [], legs: []}]; + const v = render(ds); + expect(v).toContain('1 at `PWG-3`'); + expect(v).toContain('1 `ungraded`, of 2 theorems'); + expect(v).not.toMatch(/\d+(\.\d+)?\s*%/); + expect(render([...ds].reverse())).toEqual(v); +});