From 98d60645e952f16b973875f27a8189415ad59ad4 Mon Sep 17 00:00:00 2001 From: Claude Date: Tue, 10 Nov 2026 23:06:49 +0000 Subject: [PATCH] feat(registry): derive every grade with the canon reader (WO 2.2) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The registry has no grading rule of its own now. `parseReceipt` and `derive` go. The canon reader of PROOF-POLICY §8.5.1 (`readProofReceipt` in metadatastician/standards 1-formats/deed/tools/deed_lint.js) reads each receipt. The registry pins it by commit (be39f90) and by the sha256 of the file, and refuses any other file. MATHESIS_STANDARDS names the checkout; CI uses the reader checkout that proven-tests already makes. - A receipt that the reader refuses shows as `ungraded`, with the reader's reason. That includes drift (a recorded :pwg that the legs do not support) and the pre-§8.5.1 shape. - The 17 pilot claims still derive `ungraded`: the reader refuses the secret-types receipt at eee4e40, and lintel has none at a0f2bae. - `hyperpolymath/mathesis#THY-1` joins the registry, pinned at 9aa1662. The reader derives `PWG-1`. This is the registry claim that WO 1.5 deferred to WO 2.2. - The hermetic tests use fixture receipts in the §8.5.1 shape, test the reader pin, and fail without MATHESIS_STANDARDS. - ADR 0004 names the canon reader. Its status is Accepted (owner ruling 2026-11-10): the owner's merge of this change is the ratification. - proof-receipts-as-data.adoc: a note that §8.5.1 settles the format and the reader; experiments E1 to E6 stay open. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_0136P7ZnDRsCLfZcFcEzvPcM --- .github/workflows/proven-tests.yml | 11 +- Justfile | 6 +- README.adoc | 2 +- docs/atlas/README.adoc | 4 +- docs/decisions/0004-claims-registry.adoc | 71 +++++---- docs/proposals/proof-receipts-as-data.adoc | 5 + docs/registry/claims.json | 2 +- docs/registry/registry.adoc | 25 +-- docs/status/PROOF-STATUS.adoc | 5 +- scripts/registry/claims-registry.mjs | 176 ++++++++++----------- tests/registry/claims-registry.test.mjs | 113 ++++++++----- 11 files changed, 240 insertions(+), 180 deletions(-) diff --git a/.github/workflows/proven-tests.yml b/.github/workflows/proven-tests.yml index 2462066..583acb8 100644 --- a/.github/workflows/proven-tests.yml +++ b/.github/workflows/proven-tests.yml @@ -70,11 +70,14 @@ jobs: run: | for t in tests/census/*.sh; do bash "$t"; done bash scripts/census/render-catalogue.sh docs/catalogue/census | diff -u docs/catalogue/catalogue.adoc - - # 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. + # The claims registry (docs/decisions/0004-claims-registry.adoc): the canon + # reader re-derives every grade from the home repositories' receipts at + # their pinned commits (fetched, digest-checked). The check fails if the + # committed view is stale (re-anchoring plan WO 2.2). - name: Mathesis claims registry derivation and tests + env: + # The canon reader checked out above, at the pin the registry checks. + MATHESIS_STANDARDS: ${{ runner.temp }}/receipt-reader run: | bun scripts/registry/claims-registry.mjs check bun test tests/registry/claims-registry.test.mjs diff --git a/Justfile b/Justfile index 58b6e8d..6906e00 100644 --- a/Justfile +++ b/Justfile @@ -757,11 +757,13 @@ 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 +# Proof Witness Grades with the canon reader, and write docs/registry/registry.adoc. +# Needs MATHESIS_STANDARDS: a metadatastician/standards checkout at the reader pin +# (READER in scripts/registry/claims-registry.mjs). registry: bun scripts/registry/claims-registry.mjs build -# Fail if the committed registry view is stale or a receipt overstates its grade +# Fail if the committed registry view is stale (needs MATHESIS_STANDARDS, as above) 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 d6e7a7f..c4d277b 100644 --- a/README.adoc +++ b/README.adoc @@ -19,7 +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/registry/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. diff --git a/docs/atlas/README.adoc b/docs/atlas/README.adoc index 53d409b..8f9af22 100644 --- a/docs/atlas/README.adoc +++ b/docs/atlas/README.adoc @@ -20,8 +20,8 @@ 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; -it is proposed in link:../decisions/0004-claims-registry.adoc[ADR 0004] +The next slice is a separately reviewed, source-anchored claims registry, +accepted 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 index 75ba194..5fa1a1e 100644 --- a/docs/decisions/0004-claims-registry.adoc +++ b/docs/decisions/0004-claims-registry.adoc @@ -8,11 +8,12 @@ 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. +*Accepted (ratified by owner 2026-11-10).* The owner ruled through the +selector on 2026-11-10 that the change which amends this record to name the +canon reader (re-anchoring plan WO 2.2) also sets this status, and that the +owner's merge of that change is the ratification. Until then the status was +"Proposed, awaiting owner ratification", and the registry view said that the +slice was proposed. === Context @@ -70,36 +71,45 @@ 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) +==== Derivation (the canon reader, PROOF-POLICY §8.5.1) + +Amended 2026-11-10 (re-anchoring plan WO 2.2, owner ruling D-5 (a)). The +registry has no grading rule of its own. The canon reader of PROOF-POLICY +§8.5.1 derives each grade: `readProofReceipt` in `metadatastician/standards` +`1-formats/deed/tools/deed_lint.js`. The registry pins the reader by its +standards commit and by the sha256 of that file (`READER` in +`scripts/registry/claims-registry.mjs`), and refuses any other file. 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. +. no receipt → `ungraded`; +. the reader refuses the receipt → `ungraded`, with the reader's reason. This + includes a receipt that records a `:pwg` its legs and receipts do not support + (drift, §8.4), and a receipt that is not in the §8.5.1 shape; +. the receipt is for another repository, or the claim is absent from it → + `ungraded`; +. otherwise the grade that the reader derives for the claim, from `PWG-3` to + `PWG-1` (§8.2). + +Until this amendment the registry carried its own copy of the §8.2 rules, read +only the Agda side, and never derived `PWG-1`. ==== 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. + (`just registry-check`, and CI `proven-tests.yml`): a stale view, a digest + mismatch, or a reader that is not the pinned file fails. A receipt that the + reader refuses shows as `ungraded` with the reader's reason. 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". + fixtures in the §8.5.1 shape): the grades that the reader derives, each + withheld reason, a refused receipt, the reader pin, digest refusal, + validation failures, and "never a percentage". The tests and the tool need + `MATHESIS_STANDARDS`, a standards checkout at the reader pin, and fail + without it. * Receipts are fetched from `raw.githubusercontent.com` at the pinned commit, never vendored (AUTHORITY: receipts stay home). @@ -118,6 +128,12 @@ derivation gives *0 of 12 theorems graded*, and says why: That the pilot reports zero is the point: it is what the evidence supports today. +On 2026-11-10 (WO 2.2) the reader still gives 0 of the 12 pilot theorems a +grade. It refuses the secret-types receipt at `eee4e40` ("unexpected clause +(identity) in the receipt"): the receipt predates the §8.5.1 shape. The same +change adds `hyperpolymath/mathesis#THY-1`, pinned at `9aa1662`, the commit +that holds its CI receipts. The reader derives `PWG-1` for it. + === Alternatives considered * *Store grades in the registry.* Rejected: §8.4 and §8.5 forbid assigning @@ -135,9 +151,10 @@ That the pilot reports zero is the point: it is what the evidence supports today * 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"). +* A home repository whose receipt overstates its grade shows as `ungraded`, + with the reader's reason, in the view (§8.4.2: "a gate or a bot may recompute + it at any time and reports the computed value"). Until the WO 2.2 amendment + it turned this repository's CI red instead. * 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 diff --git a/docs/proposals/proof-receipts-as-data.adoc b/docs/proposals/proof-receipts-as-data.adoc index 4d50125..bf4b5d0 100644 --- a/docs/proposals/proof-receipts-as-data.adoc +++ b/docs/proposals/proof-receipts-as-data.adoc @@ -5,6 +5,11 @@ Status: *proposed, not adopted* (2026-11-09). This proposal asks for a decision before anything is built. It changes no gate, schema or catalogue row. +NOTE: 2026-11-10 (re-anchoring plan WO 2.2): PROOF-POLICY §8.5.1 now settles +the receipt format and the reader. The reader is `readProofReceipt` in +standards `1-formats/deed/tools/deed_lint.js`, and the Mathesis claims +registry uses it. Experiments E1 to E6 below stay open. + PROOF-POLICY §8.4 says a Proof Witness Grade is *derived from receipts, never asserted*, and §8.5 says Mathesis may catalogue grades by deriving them from the home repository's receipts. Today no repository's grades can be derived: diff --git a/docs/registry/claims.json b/docs/registry/claims.json index 0edce2e..9ccd6aa 100644 --- a/docs/registry/claims.json +++ b/docs/registry/claims.json @@ -1 +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"}] +[{"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"},{"agda":{"module":"FeatureReachability","names":["Cargo.absent-under-all-features","Monotone.reach-mono"]},"claim":"THY-1","id":"hyperpolymath/mathesis#THY-1","kind":"theorem","receipt":{"path":"verification/receipts/theory_praxis.deed","sha256":"001903cb2cf4822aa3a8b4d7ff9bbc8cec99a72d73135df71795529272f95101"},"repo":"hyperpolymath/mathesis","source_commit":"9aa1662da5b2ac4a0e37b9f75a151bb312a8cbea","statement":"In a dependency graph whose edges are guarded by features closed under Horn rules, and by an arbitrary per-target condition, a node unreachable with every feature requested is unreachable under any request, on each target (`Cargo.absent-under-all-features`). The general form is `Monotone.reach-mono`: reachability over a monotone family of edge sets is monotone.","status_doc":"docs/status/PROOF-STATUS.adoc"}] diff --git a/docs/registry/registry.adoc b/docs/registry/registry.adoc index 750de1f..d80b5eb 100644 --- a/docs/registry/registry.adoc +++ b/docs/registry/registry.adoc @@ -4,22 +4,25 @@ = 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 +*derived* here from that repository's receipt by the canon reader of +PROOF-POLICY §8.5.1 (`metadatastician/standards` at `be39f900665f`), 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. +owe their Rocq and Lean legs. Status of this slice: accepted in +link:../decisions/0004-claims-registry.adoc[ADR 0004], ratified by the owner. -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. +Census: 1 at `PWG-1`, 0 at `PWG-2ii`, 0 at `PWG-2i`, 0 at `PWG-3`, 12 `ungraded`, of 13 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 +|Claim |Kind |PWG |Statement (home repository's wording) |Why not higher -|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/mathesis/blob/9aa1662da5b2ac4a0e37b9f75a151bb312a8cbea/docs/status/PROOF-STATUS.adoc[hyperpolymath/mathesis#THY-1] at `9aa1662da5b2` |theorem |`PWG-1` |In a dependency graph whose edges are guarded by features closed under Horn rules, and by an arbitrary per-target condition, a node unreachable with every feature requested is unreachable under any request, on each target (`Cargo.absent-under-all-features`). The general form is `Monotone.reach-mono`: reachability over a monotone family of edge sets is monotone. (`FeatureReachability`: `Cargo.absent-under-all-features`, `Monotone.reach-mono`) |— -|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-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`) |the canon reader refuses the receipt: unexpected clause (identity) in the receipt -|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-2] at `eee4e4038503` |theorem |`ungraded` |Public expressions read the same in low-equivalent stores (`SecretTypes.Noninterference`: `eval-low`) |the canon reader refuses the receipt: unexpected clause (identity) in the receipt + +|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`) |the canon reader refuses the receipt: unexpected clause (identity) in the receipt |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) @@ -27,11 +30,11 @@ Census: 0 at `PWG-1`, 0 at `PWG-2ii`, 0 at `PWG-2i`, 0 at `PWG-3`, 12 `ungraded` |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-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`) |the canon reader refuses the receipt: unexpected clause (identity) in the receipt -|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-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`) |the canon reader refuses the receipt: unexpected clause (identity) in the receipt -|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/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`) |the canon reader refuses the receipt: unexpected clause (identity) in the receipt |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) diff --git a/docs/status/PROOF-STATUS.adoc b/docs/status/PROOF-STATUS.adoc index 605173c..6cc558b 100644 --- a/docs/status/PROOF-STATUS.adoc +++ b/docs/status/PROOF-STATUS.adoc @@ -220,7 +220,10 @@ Residual assumptions: none in any leg. |Machine receipt (§8.5.1) |`verification/receipts/theory_praxis.deed`. The canon reader (`deed_lint.js --proof-receipt-json`) derives `PWG-1` from it, the grade -below, and CI runs that reader on each change. +below, and CI runs that reader on each change. The claims registry lists +the claim as `hyperpolymath/mathesis#THY-1` and shows the grade that the +same reader derives +(link:../registry/registry.adoc[`docs/registry/registry.adoc`]). |`pwg` |`1` (since 2026-11-10): `PWG-2ii`, and every counted witness has a current diff --git a/scripts/registry/claims-registry.mjs b/scripts/registry/claims-registry.mjs index efdc8f4..dd9d956 100644 --- a/scripts/registry/claims-registry.mjs +++ b/scripts/registry/claims-registry.mjs @@ -7,21 +7,24 @@ // 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." +// records a grade. The grade is DERIVED by the canon reader of +// standards/3-practice/PROOF-POLICY.adoc §8.5.1 (`readProofReceipt` in +// 1-formats/deed/tools/deed_lint.js), from the receipt fetched at the pinned +// commit, 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." This file holds no grading rule of its own. // // 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 // +// MATHESIS_STANDARDS names a checkout of metadatastician/standards that holds +// the reader at READER.commit; the reader's sha256 must equal READER.sha256. // --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 {fileURLToPath, pathToFileURL} from 'node:url'; import path from 'node:path'; import {readJsonl} from '../atlas/census-atlas.mjs'; @@ -31,10 +34,16 @@ const reposFile = path.join(root, 'docs/catalogue/census/repos.jsonl'); 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']); +const PWG = new Set(['PWG-1', 'PWG-2ii', 'PWG-2i', 'PWG-3', 'ungraded']); + +// The canon reader, pinned by commit and by the digest of its file. A reader +// that is not this file is refused, so a grade never comes from an unpinned rule. +export const READER = { + repository: 'metadatastician/standards', + commit: 'be39f900665fb7c042c05d1165da018adc1860f4', + path: '1-formats/deed/tools/deed_lint.js', + sha256: 'f7e2b91905f0d99e5cabab59385073afb695be8b9f2d0591257a6a6fd62e25e3', +}; // ── Validation of the registry rows ────────────────────────────────────────── @@ -68,76 +77,49 @@ export function validate(rows, inventory) { 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); +// ── The canon reader ───────────────────────────────────────────────────────── + +// Load readProofReceipt from a standards checkout, after its digest check. +export async function loadReader(standardsDir = process.env.MATHESIS_STANDARDS) { + if (!standardsDir) { + throw new Error(`set MATHESIS_STANDARDS to a checkout of ${READER.repository} at ${READER.commit}`); } - return {flags, claims}; + const file = path.resolve(standardsDir, READER.path); + const digest = createHash('sha256').update(await readFile(file)).digest('hex'); + if (digest !== READER.sha256) { + throw new Error(`${file} is not the pinned canon reader (sha256 ${digest}, pinned ${READER.sha256} at ${READER.commit})`); + } + const {readProofReceipt} = await import(pathToFileURL(file).href); + if (typeof readProofReceipt !== 'function') throw new Error(`${file} exports no readProofReceipt`); + return readProofReceipt; } -// ── 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. +// ── The derivation: the canon reader, PROOF-POLICY §8.1, §8.2, §8.5.1 ──────── + +// Derive one row's grade from the reader's record of its receipt. `read` is +// {record} when the reader accepted the receipt, {refusal} when it refused it, +// or null when the row pins no receipt. Returns {pwg, reasons}: `reasons` say +// why the grade is not higher. +export function derive(row, read) { + if (row.kind !== 'theorem') return {pwg: 'ungraded', reasons: [`${row.kind}, not a theorem (§8.1)`]}; + if (read === null) return {pwg: 'ungraded', reasons: ['no machine receipt in the home repository']}; + if (read.refusal) return {pwg: 'ungraded', reasons: [`the canon reader refuses the receipt: ${read.refusal}`]}; + const {record} = read; + if (record.repository !== row.repo) { + return {pwg: 'ungraded', reasons: [`the receipt is for ${record.repository}, not ${row.repo}`]}; } - 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}; + const claim = record.claims.find(c => c.id === row.claim); + if (!claim) return {pwg: 'ungraded', reasons: ['claim absent from the receipt']}; + if (!PWG.has(claim.pwg)) throw new Error(`the reader returned an unknown grade ${claim.pwg}: ${row.id}`); + const reasons = []; + if (claim.pwg !== 'PWG-1') reasons.push(`the reader derives ${claim.pwg} from the legs and receipts at \`${record.source_commit.slice(0, 12)}\``); + return {pwg: claim.pwg, reasons}; } // ── Fetching receipts at their pinned commits ──────────────────────────────── -// Return the receipt text for a row, verified against its sha256, or null. +// Return the receipt text for a row, verified against its sha256. 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'); @@ -152,14 +134,28 @@ async function loadReceipt(row, receiptsDir) { return text; } -// Derive every row, fetching each distinct receipt once. -export async function deriveAll(rows, receiptsDir) { +// Derive every row, reading each distinct receipt once. A receipt that the +// reader refuses gives `ungraded` with the reader's reason; a receipt that +// cannot be fetched or fails its digest stops the run. +export async function deriveAll(rows, receiptsDir, readProofReceipt) { 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))}); + let read = null; + if (row.receipt !== null) { + const key = `${row.repo}@${row.source_commit}/${row.receipt.path}`; + if (!cache.has(key)) { + const text = await loadReceipt(row, receiptsDir); + try { + cache.set(key, {record: readProofReceipt(text, path.basename(row.receipt.path))}); + } catch (e) { + if (!['LintError', 'ProofReceiptError'].includes(e?.name)) throw e; + cache.set(key, {refusal: String(e)}); + } + } + read = cache.get(key); + } + out.push({row, ...derive(row, read)}); } return out; } @@ -167,7 +163,7 @@ export async function deriveAll(rows, receiptsDir) { // ── Rendering ──────────────────────────────────────────────────────────────── const cell = s => String(s).replaceAll('|', String.raw`\|`).replaceAll('\n', ' '); -const label = p => (p === 'ungraded' ? '`ungraded`' : `\`PWG-${p}\``); +const label = p => `\`${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. @@ -175,7 +171,7 @@ 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 census = ['PWG-1', 'PWG-2ii', 'PWG-2i', 'PWG-3'].map(p => `${count(p)} at \`${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', @@ -184,16 +180,17 @@ export function render(derived) { '= 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', + '*derived* here from that repository\'s receipt by the canon reader of', + `PROOF-POLICY §8.5.1 (\`${READER.repository}\` at \`${READER.commit.slice(0, 12)}\`), 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.', + 'owe their Rocq and Lean legs. Status of this slice: accepted in', + 'link:../decisions/0004-claims-registry.adoc[ADR 0004], ratified by the owner.', '', `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', + '|Claim |Kind |PWG |Statement (home repository\'s wording) |Why not higher', '', ]; for (const d of ordered) { @@ -201,7 +198,7 @@ export function render(derived) { 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('; ') || '—'; + const notes = d.reasons.map(cell).join('; ') || '—'; out.push(`|${link} ${at} |${r.kind} |${label(d.pwg)} |${cell(r.statement)}${names} |${notes}`, ''); } out.push('|===', ''); @@ -212,24 +209,23 @@ export function render(derived) { async function main() { const [cmd, ...args] = process.argv.slice(2); + if (cmd !== 'build' && cmd !== 'check') { + console.error('usage: claims-registry.mjs build|check [--receipts-dir DIR]'); + process.exit(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')), await readJsonl(reposFile)); - 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 derived = await deriveAll(rows, receiptsDir, await loadReader()); 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') { + } else { 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); } } diff --git a/tests/registry/claims-registry.test.mjs b/tests/registry/claims-registry.test.mjs index 8cb43c4..afc06eb 100644 --- a/tests/registry/claims-registry.test.mjs +++ b/tests/registry/claims-registry.test.mjs @@ -1,11 +1,15 @@ // 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'; +// +// Hermetic tests of the claims registry. The grades come from the canon reader +// (PROOF-POLICY §8.5.1), so the tests need it: set MATHESIS_STANDARDS to a +// checkout of metadatastician/standards at READER.commit. Without it they fail. +import {test, expect, beforeAll} from 'bun:test'; +import {readFileSync, mkdtempSync, mkdirSync, writeFileSync, copyFileSync} 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'; +import {validate, loadReader, derive, deriveAll, render, READER} from '../../scripts/registry/claims-registry.mjs'; import {parseJsonl} from '../../scripts/atlas/census-atlas.mjs'; const rows = JSON.parse(readFileSync(new URL('../../docs/registry/claims.json', import.meta.url), 'utf8')); @@ -16,12 +20,28 @@ const theorem = {id: 'o/r#T-1', repo: 'o/r', claim: 'T-1', kind: 'theorem', stat 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`; +let readProofReceipt; +beforeAll(async () => { readProofReceipt = await loadReader(); }); + +// A receipt in the §8.5.1 shape (the proof-receipt profile of praxis-deed). +// `rocq` and `lean` are leg states, or null for no leg; `*At` is the commit of +// that leg's current receipt. +const fixture = ({repo = 'o/r', pwg = 'PWG-3', invocation = 'agda --safe --without-K --cubical-compatible M.agda', + rocq = null, lean = null, rocqAt = commit, leanAt = commit} = {}) => { + const run = (prover, at, inv) => + ` (receipt :run "ci" :commit "${at}" :checker "${prover}" :invocation "${inv}" :state current))\n`; + const leg = (prover, state, at) => state === null ? '' : + ` (leg :prover ${prover} :route re-proved :token proven :state ${state}\n` + run(prover, at, `${prover} M`); + return ';; SPDX-License-Identifier: CC-BY-SA-4.0\n(praxis-deed\n :schema-version "1.0.0"\n' + + ` :canonical-name "fixture-receipt"\n :profile proof-receipt\n :repository "${repo}"\n :source-commit "${commit}"\n` + + ` (claim :id "T-1" :pwg ${pwg} :foundation-diverse #f\n` + + ' (leg :prover agda :route source :token proven :state AGDA-VERIFIED\n' + run('agda', commit, invocation) + + leg('rocq', rocq, rocqAt) + leg('lean', lean, leanAt) + '))\n'; +}; +// Read a fixture as deriveAll does: {record} or {refusal}. +const read = text => { + try { return {record: readProofReceipt(text, 'fixture_praxis.deed')}; } catch (e) { return {refusal: String(e)}; } +}; test('the committed registry validates against the census inventory', () => { expect(validate(rows, inventory).length).toBe(rows.length); @@ -38,50 +58,61 @@ test('validation fails closed', () => { 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('only the pinned reader is loaded', async () => { + const dir = mkdtempSync(path.join(tmpdir(), 'reader-')); + mkdirSync(path.join(dir, path.dirname(READER.path)), {recursive: true}); + copyFileSync(path.join(process.env.MATHESIS_STANDARDS, READER.path), path.join(dir, READER.path)); + expect(typeof await loadReader(dir)).toBe('function'); + writeFileSync(path.join(dir, READER.path), readFileSync(path.join(dir, READER.path), 'utf8') + '\n// changed\n'); + await expect(loadReader(dir)).rejects.toThrow(/not the pinned canon reader/); + await expect(loadReader('')).rejects.toThrow(/set MATHESIS_STANDARDS/); +}); + +test('the grade is the one the reader derives (§8.2)', () => { + expect(derive(theorem, read(fixture())).pwg).toBe('PWG-3'); + expect(derive(theorem, read(fixture({pwg: 'PWG-2i', rocq: 'RECONCILED'}))).pwg).toBe('PWG-2i'); + // Both legs current, but one receipt names another commit: not PWG-1. + const two = derive(theorem, read(fixture({pwg: 'PWG-2ii', rocq: 'RECONCILED', lean: 'RECONCILED', leanAt: 'b'.repeat(40)}))); + expect(two.pwg).toBe('PWG-2ii'); + expect(two.reasons.join()).toContain('the reader derives PWG-2ii'); + const one = derive(theorem, read(fixture({pwg: 'PWG-1', rocq: 'RECONCILED', lean: 'RECONCILED'}))); + expect(one).toEqual({pwg: 'PWG-1', reasons: []}); }); -test('each reason a grade is withheld', () => { - const noFlag = derive(theorem, parseReceipt(receipt({flags: '--safe --without-K'}))); +test('a receipt the reader refuses is ungraded, with the reader\'s reason', () => { + // A recorded grade the legs do not support (§8.4 drift). + const drift = derive(theorem, read(fixture({pwg: 'PWG-2i'}))); + expect(drift.pwg).toBe('ungraded'); + expect(drift.reasons.join()).toMatch(/^the canon reader refuses the receipt: .*records :pwg PWG-2i, but its legs and receipts support PWG-3/); + // The pre-§8 shape is not a proof receipt. + const legacy = derive(theorem, read(';; SPDX-License-Identifier: CC-BY-SA-4.0\n(praxis-deed\n :schema-version "1.0.0"\n (claim :id "T-1" :token "proven" :grade "grade-3"))\n')); + expect(legacy.pwg).toBe('ungraded'); + expect(legacy.reasons.join()).toContain('the canon reader refuses the receipt'); + // Without the canonical invocation the Agda leg does not count. + const noFlag = derive(theorem, read(fixture({pwg: 'ungraded', invocation: 'agda --safe --without-K M.agda'}))); 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('each other reason a grade is withheld', () => { + expect(derive(theorem, null).reasons.join()).toContain('no machine receipt'); + expect(derive({...theorem, claim: 'T-9'}, read(fixture())).reasons.join()).toContain('absent'); + expect(derive({...theorem, kind: 'demonstration'}, read(fixture())).pwg).toBe('ungraded'); + expect(derive(theorem, read(fixture({repo: 'o/other'}))).reasons.join()).toContain('for o/other, not o/r'); }); -test('a receipt that does not match its pinned digest is refused', async () => { +test('deriveAll reads each receipt once, and refuses a receipt that does not match its pinned digest', async () => { const dir = mkdtempSync(path.join(tmpdir(), 'registry-')); - const text = receipt(); + const text = fixture(); 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/); + writeFileSync(path.join(dir, `o__r@${commit}`, 'r_praxis.deed'), text); + const good = {...theorem, receipt: {path: 'r_praxis.deed', sha256: createHash('sha256').update(text).digest('hex')}}; + expect((await deriveAll([good], dir, readProofReceipt))[0].pwg).toBe('PWG-3'); + await expect(deriveAll([{...good, receipt: {path: 'r_praxis.deed', sha256: 'b'.repeat(64)}}], dir, readProofReceipt)).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 ds = [{row: theorem, pwg: 'PWG-3', reasons: []}, + {row: {...theorem, id: 'o/r#T-2', claim: 'T-2'}, pwg: 'ungraded', reasons: ['x']}]; const v = render(ds); expect(v).toContain('1 at `PWG-3`'); expect(v).toContain('1 `ungraded`, of 2 theorems');