From 580f9f9bab304c0b3e281469c40c6a3ba05ad9df Mon Sep 17 00:00:00 2001 From: Claude Date: Fri, 13 Nov 2026 21:41:38 +0000 Subject: [PATCH 1/7] proofs: write the receipt under the new PROOF-POLICY 8.5 and add APP-1 to APP-4 Standards PRs 1534 and 1545 (merged at e5a39d7, owner rulings 2026-11-13) make every current receipt record its inputs manifest, its inputs digest and its axioms, add echo records for squash and rebase merges, and give the home gate and consumers a shared git checker (PROOF-POLICY 8.5.3). - verification/receipts/theory_praxis.deed: written again from CI run 43498592499 on main 034f215. THY-1 is earned again, and APP-1 to APP-4 are added, each with Agda, Rocq and Lean legs. One manifest per prover: the union of the files that the graded roots read. The trusted base gains Char and String, which Applied/IntLaws reaches through Agda.Builtin.Int. The reader at e5a39d7 derives PWG-1 for all five. - just receipt-check (in just check): the home gate runs the shared checker on this receipt against origin/main. CI fetches the history of main, and the pinned Guix shell gains jq, which the checker needs. - The registry pins the reader at e5a39d7 and the checker scripts by digest. It catalogues a PWG-1 only when the git checks hold against a clone of the home repository; otherwise PWG-2ii, with the reason (ADR 0004 amended). - THY-1 shows as ungraded until its claim pin moves to this receipt in the next change; the theory ledger records it. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_0136P7Zo9dheFQzYYWV49hAk --- .github/workflows/agda-proof-policy.yml | 7 +- Justfile | 10 +- build/manifest.scm | 3 + docs/atlas/generated/registry.adoc | 6 +- docs/decisions/0004-claims-registry.adoc | 9 + docs/status/PROOF-NEEDS.adoc | 11 +- docs/status/PROOF-STATUS.adoc | 34 +++- docs/status/ROADMAP.adoc | 15 ++ docs/theory/generated/index.adoc | 2 +- docs/theory/ledger.jsonl | 1 + scripts/registry/claims-registry.mjs | 108 +++++++++- tests/registry/claims-registry.test.mjs | 35 +++- verification/receipts/theory_praxis.deed | 241 +++++++++++++++++++++-- 13 files changed, 432 insertions(+), 50 deletions(-) diff --git a/.github/workflows/agda-proof-policy.yml b/.github/workflows/agda-proof-policy.yml index 1cfb9be..e2f9fd6 100644 --- a/.github/workflows/agda-proof-policy.yml +++ b/.github/workflows/agda-proof-policy.yml @@ -125,8 +125,8 @@ jobs: git init -q "$r" git -C "$r" remote add origin https://github.com/metadatastician/standards.git git -C "$r" config core.sparseCheckout true - printf '1-formats/deed/tools/\n' > "$r/.git/info/sparse-checkout" - git -C "$r" fetch -q --depth 1 origin be39f900665fb7c042c05d1165da018adc1860f4 + printf '1-formats/deed/tools/\nscripts/check-proof-receipt.sh\nscripts/proof-inputs-sha256.sh\n' > "$r/.git/info/sparse-checkout" + git -C "$r" fetch -q --depth 1 origin e5a39d7e5c66f9d24d7e0ffa3f8dbd01f2d42d9d git -C "$r" checkout -q FETCH_HEAD - name: Golden path (just check), then its controls @@ -134,6 +134,9 @@ jobs: env: MATHESIS_STANDARDS: ${{ runner.temp }}/receipt-reader run: | + # The receipt's git checks (PROOF-POLICY §8.5.3) need origin/main with its + # history: the checkout is shallow. + git fetch -q --no-tags --unshallow origin +refs/heads/main:refs/remotes/origin/main guix time-machine -C build/channels.scm -- shell -m build/manifest.scm -- sh -euc ' just --version bun --version diff --git a/Justfile b/Justfile index 141e7d1..b9034c1 100644 --- a/Justfile +++ b/Justfile @@ -707,7 +707,7 @@ uncloak: # The Mathesis golden path (re-anchoring plan WO 2.5). CI runs it in the pinned # Guix (agda-proof-policy.yml). A stale view or a failing proof fails. # Golden path: every generated view matches its data, every gated proof checks -check: check-views site-check check-proofs +check: check-views site-check check-proofs receipt-check # Needs bun, network for the receipts, and MATHESIS_STANDARDS (see `registry`). # Views current: catalogue, census tests, atlas, claims registry, bridges and @@ -772,6 +772,14 @@ registry-check: bun scripts/registry/theory-ledger.mjs verify bun test tests/registry/ +# The git checks of PROOF-POLICY §8.5.3 on the receipt of Mathesis: its +# :source-commit is on origin/main, each current receipt's inputs manifest holds +# at its commit, and each echo's witness holds. The shared checker of the pinned +# standards commit runs them (MATHESIS_STANDARDS, as above). Needs origin/main +# with its history. +receipt-check: + bun scripts/registry/claims-registry.mjs receipt + # Append each change of the theory shelf to docs/theory/ledger.jsonl, the only # way the ledger changes (needs MATHESIS_STANDARDS, as above). A note tells the # story: just theory-ledger "THY-2 admitted after its Lean leg landed" diff --git a/build/manifest.scm b/build/manifest.scm index 34259e6..3a2303d 100644 --- a/build/manifest.scm +++ b/build/manifest.scm @@ -13,6 +13,9 @@ (specifications->manifest (list "git" "bash" "coreutils" "nss-certs" "just" "mise" "shellcheck" "chez-scheme" "gmp" "gcc-toolchain" "zig" + ;; jq: the shared git checker of proof receipts (PROOF-POLICY §8.5.3) reads + ;; the reader's JSON with it. + "jq" ;; Provers for the proof lanes (re-anchoring plan WO 1.4, ruling D-8 (a)). ;; No agda-stdlib: its Guix package does not build, and no proof here ;; imports it (owner ruling 2026-11-10). diff --git a/docs/atlas/generated/registry.adoc b/docs/atlas/generated/registry.adoc index b5904f6..b3c9c42 100644 --- a/docs/atlas/generated/registry.adoc +++ b/docs/atlas/generated/registry.adoc @@ -5,18 +5,18 @@ Each row is a claim in its home repository at a pinned commit. The grade is *derived* here from that repository's receipt by the canon reader of -PROOF-POLICY §8.5.1 (`metadatastician/standards` at `be39f900665f`), never +PROOF-POLICY §8.5.1 (`metadatastician/standards` at `e5a39d7e5c66`), 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: accepted in link:../../decisions/0004-claims-registry.adoc[ADR 0004], ratified by the owner. -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. +Census: 0 at `PWG-1`, 0 at `PWG-2ii`, 0 at `PWG-2i`, 0 at `PWG-3`, 13 `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 -|https://github.com/hyperpolymath/mathesis/blob/9aa1662da5b2ac4a0e37b9f75a151bb312a8cbea/docs/status/PROOF-STATUS.adoc[hyperpolymath/mathesis#THY-1] at `9aa1662da5b2`; the receipt describes `336768958d01` |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/mathesis/blob/9aa1662da5b2ac4a0e37b9f75a151bb312a8cbea/docs/status/PROOF-STATUS.adoc[hyperpolymath/mathesis#THY-1] at `9aa1662da5b2` |theorem |`ungraded` |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`) |the canon reader refuses the receipt: a receipt of the agda leg of claim "THY-1" is current and is missing :inputs-sha256 (§8.5.1) |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 diff --git a/docs/decisions/0004-claims-registry.adoc b/docs/decisions/0004-claims-registry.adoc index a0bc3b1..70614a7 100644 --- a/docs/decisions/0004-claims-registry.adoc +++ b/docs/decisions/0004-claims-registry.adoc @@ -92,6 +92,15 @@ if its sha256 differs from the pinned digest, and derives: `ungraded`; . otherwise the grade that the reader derives for the claim, from `PWG-3` to `PWG-1` (§8.2). +. a `PWG-1` stays only when the git checks of §8.5.3 hold (amendment + 2026-11-13): the shared checker of the pinned standards commit + (`scripts/check-proof-receipt.sh`, pinned by digest with the digest script + that it calls, `CHECKER` in `scripts/registry/claims-registry.mjs`) runs + against a clone of the home repository that holds its pull-request heads. + It checks that the receipt's `:source-commit` is on the default branch, that + each current receipt's inputs manifest holds at its commit, and that each + echo's witness holds at both ends. If a check fails or cannot run, the + registry catalogues `PWG-2ii` and records why (§8.5.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`. diff --git a/docs/status/PROOF-NEEDS.adoc b/docs/status/PROOF-NEEDS.adoc index edf291a..104efd4 100644 --- a/docs/status/PROOF-NEEDS.adoc +++ b/docs/status/PROOF-NEEDS.adoc @@ -42,7 +42,7 @@ missing input is missing, in every period after it too, and never zero. A verdict is "no" on a known breach and otherwise missing when any value it depends on is missing; it is never "yes" then |Agda, re-checked in Rocq and Lean -|Proved in Agda, Rocq and Lean; no receipt yet (WO 4.2) +|Proved in Agda, Rocq and Lean; the receipt derives `PWG-1` (WO 4.2) |`verification/proofs/agda/Applied/Missing.agda`; Rocq and Lean: `Cohort.v`, `Cohort.lean` |APP-2 @@ -50,7 +50,7 @@ depends on is missing; it is never "yes" then plus, summed over the periods, receipts minus payments; when a value is missing, both sides are missing |Agda, re-checked in Rocq and Lean -|Proved in Agda, Rocq and Lean; no receipt yet (WO 4.2) +|Proved in Agda, Rocq and Lean; the receipt derives `PWG-1` (WO 4.2) |`verification/proofs/agda/Applied/Cash.agda` (`cash-identity`); Rocq and Lean: `cash_identity` |APP-3 @@ -58,14 +58,14 @@ missing, both sides are missing keeps every closing balance at or above its floor, and no smaller non-negative amount does |Agda, re-checked in Rocq and Lean -|Proved in Agda, Rocq and Lean; no receipt yet (WO 4.2) +|Proved in Agda, Rocq and Lean; the receipt derives `PWG-1` (WO 4.2) |`verification/proofs/agda/Applied/Cash.agda` (`gap-sound`, `gap-least`); Rocq and Lean: `gap_sound`, `gap_least` |APP-4 |Status never upgrades: the evidence status of an output is never stronger than the weakest status of the inputs that it depends on |Agda, re-checked in Rocq and Lean -|Proved in Agda, Rocq and Lean; no receipt yet (WO 4.2) +|Proved in Agda, Rocq and Lean; the receipt derives `PWG-1` (WO 4.2) |`verification/proofs/agda/Applied/Missing.agda`; Rocq and Lean: `Cohort.v`, `Cohort.lean` |=== @@ -84,7 +84,8 @@ the integer instance of the worked examples is one. The Rocq and Lean legs restate the same definitions and re-prove every theorem, the integer laws included. Every module is gated: no postulate in an Agda import cone, every Rocq theorem closed under the global context, and no axiom in any Lean -theorem. No receipt records these legs yet, so no grade is derived. +theorem. The receipt `verification/receipts/theory_praxis.deed` records the +three legs of each, and the canon reader derives `PWG-1` for each (2026-11-13). No Mathesis obligation concerns an ABI or an FFI: since WO 3.2 the deed declares neither capability. diff --git a/docs/status/PROOF-STATUS.adoc b/docs/status/PROOF-STATUS.adoc index 411ff8e..4e4ade1 100644 --- a/docs/status/PROOF-STATUS.adoc +++ b/docs/status/PROOF-STATUS.adoc @@ -26,7 +26,7 @@ reader of PROOF-POLICY §8.5.1. |APP-1 to APP-4, the cohort model of the applied shelf (WO 4.2) |Proved in Agda, Rocq and Lean |- -|The record below. No receipt yet, so no grade is derived +|The record below. The receipt derives `PWG-1` (2026-11-13) |=== *Overall*: 5 of 6 obligations are proved in all three provers; THY-1 alone has @@ -83,10 +83,13 @@ missing crate as missing from every build. monotonicity step. * Axioms: none. * Receipt state: superseded on 2026-11-10 by the CI receipt below. -* CI receipt (current): Agda 2.7.0.1 in the pinned Guix (`8edb9da`), same - invocation, at commit `336768958d01`, run 42896264290. The file SHA-256 is - unchanged, and the log reports no postulate in the cone (`Agda.Primitive`, - `FeatureReachability`). +* CI receipt (superseded on 2026-11-13): Agda 2.7.0.1 in the pinned Guix + (`8edb9da`), same invocation, at commit `336768958d01`, run 42896264290. + The file SHA-256 is unchanged, and the log reports no postulate in the cone + (`Agda.Primitive`, `FeatureReachability`). +* CI receipt (current, 2026-11-13): the same, at main `034f215`, run + 43498592499. It records the inputs manifest and the axioms (none) that + PROOF-POLICY §8.5.1 now requires (standards `e5a39d7`). |Rocq leg |`PROVEN`, route `re-proved`, correspondence `RECONCILED`. Receipt: @@ -194,7 +197,7 @@ same reader derives |`pwg` |`1` (since 2026-11-10): `PWG-2ii`, and every counted witness has a current receipt from one headless, isolated, pinned CI run on the exact source commit -`336768958d01` (PROOF-POLICY §8.2). The grade holds while those receipts stay +(PROOF-POLICY §8.2): `336768958d01` until 2026-11-13, `034f215` since. The grade holds while those receipts stay current: a later commit that breaks a leg, or a run that cannot be repeated, drops it (§8.4). Before 2026-11-10 it was `2ii`, because each receipt came from a local run. @@ -261,9 +264,14 @@ is `cash_identity`, and so on). The differences are encoding only: Residual assumptions: none in any leg. |Machine receipt (§8.5.1) -|None yet. The receipt `verification/receipts/theory_praxis.deed` records -THY-1 only. Adding APP-1 to APP-4 needs receipts from a CI run on the merged -commit, so no grade is derived for them yet. +|`verification/receipts/theory_praxis.deed`, with THY-1. The current receipts +come from CI run 43498592499 on main `034f215` (Agda 2.7.0.1, Rocq 8.18.0, +Lean 4.29.0, pinned Guix `8edb9da`). Each records the inputs manifest of its +prover and no axiom. The canon reader at standards `e5a39d7` derives `PWG-1` +for each of APP-1 to APP-4, and the shared git checker (`just receipt-check`) +passes. The Rocq and Lean legs are `RECONCILED` by the comparison above, done +by reading. The trusted base gains `Char` and `String`, the postulates that +`Applied/IntLaws` reaches through `Agda.Builtin.Int`. |=== == Verification commands @@ -284,6 +292,14 @@ bash tests/proofs/gate_controls_test.sh agda |=== |Date |Change +|2026-11-13 +|The receipt is written again under PROOF-POLICY §8.5.1 at standards +`e5a39d7`: each current receipt records its inputs manifest and its axioms. +THY-1 is earned again, and APP-1 to APP-4 are added, from CI run 43498592499 +on main `034f215`. The reader derives `PWG-1` for all five. The claims +registry shows THY-1 as `ungraded` until its claim pin moves to the new +receipt (the next change). + |2026-11-10 |THY-1 receipts earned again at Agda 2.7.0.1 and Lean 4.29.0 in the pinned Guix shell; the receipt derives `PWG-1`. diff --git a/docs/status/ROADMAP.adoc b/docs/status/ROADMAP.adoc index c6f9c5d..ab5ec02 100644 --- a/docs/status/ROADMAP.adoc +++ b/docs/status/ROADMAP.adoc @@ -220,6 +220,21 @@ One pull request that changes census rows is open at a time (atlas README, the owner's act. * Finding: the `intend` contract still marks stage 3 `in_progress` and stage 4 `declared`; a contract edit needs owner review. +* Receipts under the new PROOF-POLICY §8.5.1 to §8.5.3 (owner rulings + 2026-11-13; standards PRs 1534 and 1545, merged at `e5a39d7`): every current + receipt records its inputs manifest, its inputs digest and its axioms; an + `(echo …)` record carries a receipt across a squash or rebase; the home gate + and consumers run the shared git checker. +** First change: the Mathesis receipt is written again from CI run + 43498592499 on main `034f215`. It adds APP-1 to APP-4 and earns THY-1 + again; the reader derives `PWG-1` for all five, and `just receipt-check` + (the home gate, in `just check`) passes. The registry pins the new reader + and catalogues a `PWG-1` only when the git checks hold. Until the next + change, the registry shows THY-1 as `ungraded`, because its claim pin names + the old receipt; the theory ledger records this. +** Next change: the claim pins of THY-1 and APP-1 to APP-4 (applied shelf, a + new `shelf` field), and of secret-types at the commit that holds its + manifest receipt (re-anchoring plan WO 5.1). [[stages]] == Stages diff --git a/docs/theory/generated/index.adoc b/docs/theory/generated/index.adoc index 552f85a..cb2cd98 100644 --- a/docs/theory/generated/index.adoc +++ b/docs/theory/generated/index.adoc @@ -13,6 +13,6 @@ Theorems: 1. |=== |Theorem |Statement |PWG |Source and receipt |Dependant -|THY-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. |`PWG-1` |`FeatureReachability`: `Cargo.absent-under-all-features`, `Monotone.reach-mono`; `verification/receipts/theory_praxis.deed` at `9aa1662da5b2` |https://github.com/metadatastician/standards/blob/main/docs/UPSTREAM-DEPENDENCY-WATCH.adoc[metadatastician/standards]: Run cargo tree --target all --workspace --all-features, and read a crate missing there as missing from every build. +|THY-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. |`ungraded` |`FeatureReachability`: `Cargo.absent-under-all-features`, `Monotone.reach-mono`; `verification/receipts/theory_praxis.deed` at `9aa1662da5b2` |https://github.com/metadatastician/standards/blob/main/docs/UPSTREAM-DEPENDENCY-WATCH.adoc[metadatastician/standards]: Run cargo tree --target all --workspace --all-features, and read a crate missing there as missing from every build. |=== diff --git a/docs/theory/ledger.jsonl b/docs/theory/ledger.jsonl index 93f31e3..1a76a90 100644 --- a/docs/theory/ledger.jsonl +++ b/docs/theory/ledger.jsonl @@ -1 +1,2 @@ {"admission_sha256":"91977ed786bb4a63913234167876096bf6e93491e828dcc3e1e7538862349fc5","date":"2026-11-11","event":"admitted","id":"hyperpolymath/mathesis#THY-1","note":"The ledger starts here, on 2026-11-11. THY-1 was proved in Agda on 2026-11-09 and re-proved in Rocq and Lean; it derived PWG-2ii until the CI receipts of run 42896264290 gave PWG-1 on 2026-11-10. Transport from Agda was blocked, because the Lambdapi exports to Rocq and Lean drop rewrite rules. Earlier history is in git and docs/status/PROOF-STATUS.adoc.","pwg":"PWG-1","receipt":{"commit":"9aa1662da5b2ac4a0e37b9f75a151bb312a8cbea","path":"verification/receipts/theory_praxis.deed","sha256":"001903cb2cf4822aa3a8b4d7ff9bbc8cec99a72d73135df71795529272f95101"},"seq":1} +{"admission_sha256":"91977ed786bb4a63913234167876096bf6e93491e828dcc3e1e7538862349fc5","changes":["pwg"],"date":"2026-11-13","event":"changed","id":"hyperpolymath/mathesis#THY-1","note":"The reader pin moved to standards e5a39d7, which requires an inputs manifest, the axioms and the inputs digest on every current receipt. The receipt that THY-1's claim pin names predates them, so the reader refuses it. The Mathesis receipt is regenerated in the same change, and the next change moves THY-1's pin to it.","pwg":"ungraded","receipt":{"commit":"9aa1662da5b2ac4a0e37b9f75a151bb312a8cbea","path":"verification/receipts/theory_praxis.deed","sha256":"001903cb2cf4822aa3a8b4d7ff9bbc8cec99a72d73135df71795529272f95101"},"seq":2} diff --git a/scripts/registry/claims-registry.mjs b/scripts/registry/claims-registry.mjs index c3801a7..fcd10ea 100644 --- a/scripts/registry/claims-registry.mjs +++ b/scripts/registry/claims-registry.mjs @@ -22,7 +22,9 @@ // 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 {readFile, writeFile, mkdir, mkdtemp} from 'node:fs/promises'; +import {spawnSync} from 'node:child_process'; +import {tmpdir} from 'node:os'; import {createHash} from 'node:crypto'; import {fileURLToPath, pathToFileURL} from 'node:url'; import path from 'node:path'; @@ -60,9 +62,19 @@ const PWG = new Set(['PWG-1', 'PWG-2ii', 'PWG-2i', 'PWG-3', 'ungraded']); // that is not this file is refused, so a grade never comes from an unpinned rule. export const READER = { repository: 'metadatastician/standards', - commit: 'be39f900665fb7c042c05d1165da018adc1860f4', + commit: 'e5a39d7e5c66f9d24d7e0ffa3f8dbd01f2d42d9d', path: '1-formats/deed/tools/deed_lint.js', - sha256: 'f7e2b91905f0d99e5cabab59385073afb695be8b9f2d0591257a6a6fd62e25e3', + sha256: '37ff85be499b35dd9d74399e05d9ae1e57ccf095362c355f93e04b3bbf4c9491', +}; + +// The git checks of PROOF-POLICY §8.5.3, from the same standards commit as the +// reader. A PWG-1 is catalogued only when the checker passes against a clone of +// the home repository; the checker calls the digest script, so both are pinned. +export const CHECKER = { + path: 'scripts/check-proof-receipt.sh', + sha256: '831f5a43c906c3edc8cfa68ab5fe13c37e7a41b35e40068481d988d887f4bd3f', + digest: 'scripts/proof-inputs-sha256.sh', + digestSha256: 'dfc6dde01a3a79df638eebe4cad0eae584d8f17280077e149174c0667e9508f4', }; // ── Validation of the registry rows ────────────────────────────────────────── @@ -155,20 +167,82 @@ async function loadReceipt(row, receiptsDir) { return text; } +// ── The git checks of PROOF-POLICY §8.5.3 ──────────────────────────────────── + +// A consumer catalogues a PWG-1 only when the git checks hold against the home +// repository; otherwise it catalogues the grade without PWG-1 (PWG-2ii, §8.5.2) +// and records why. `check` is {ok, reason}. +export function withGitCheck(d, check) { + if (d.pwg !== 'PWG-1' || check.ok) return d; + return {...d, pwg: 'PWG-2ii', reasons: [...d.reasons, `§8.5.3 git checks: ${check.reason}; catalogued without PWG-1`]}; +} + +const run = (cmd, args) => spawnSync(cmd, args, {encoding: 'utf8'}); + +// The path of the pinned checker, after the digest checks of both pinned +// scripts in the standards checkout. +export async function checkerScript(standardsDir = process.env.MATHESIS_STANDARDS) { + const pinned = async (rel, sha) => { + const file = path.resolve(standardsDir, rel); + const digest = createHash('sha256').update(await readFile(file)).digest('hex'); + if (digest !== sha) throw new Error(`${file} is not the pinned script (sha256 ${digest}, pinned ${sha} at ${READER.commit})`); + return file; + }; + await pinned(CHECKER.digest, CHECKER.digestSha256); + return pinned(CHECKER.path, CHECKER.sha256); +} + +// The shared checker of the standards checkout, after the digest checks of both +// pinned scripts. It returns (row, text) => {ok, reason}, cloning each home +// repository once, with the pull-request heads that a squashed echo source needs. +export async function gitChecker(standardsDir = process.env.MATHESIS_STANDARDS) { + const script = await checkerScript(standardsDir); + const work = await mkdtemp(path.join(tmpdir(), 'mathesis-git-')); + const clones = new Map(); + const clone = repo => { + if (!clones.has(repo)) { + const dir = path.join(work, repo.replace('/', '__')); + const steps = [ + ['git', ['clone', '-q', '--filter=blob:none', '--no-checkout', `https://github.com/${repo}`, dir]], + ['git', ['-C', dir, 'fetch', '-q', 'origin', '+refs/pull/*/head:refs/pull/*/head']], + ]; + const failed = steps.map(([c, a]) => run(c, a)).find(r => r.status !== 0); + const head = failed ? null : run('git', ['-C', dir, 'symbolic-ref', '--short', 'refs/remotes/origin/HEAD']); + clones.set(repo, failed || head.status !== 0 + ? {reason: `could not clone ${repo}: ${(failed || head).stderr.trim().split('\n').pop()}`} + : {dir, branch: head.stdout.trim()}); + } + return clones.get(repo); + }; + return async (row, text) => { + const c = clone(row.repo); + if (!c.dir) return {ok: false, reason: c.reason}; + const file = path.join(await mkdtemp(path.join(work, 'r-')), path.basename(row.receipt.path)); + await writeFile(file, text); + const r = run('bash', [script, '--branch', c.branch, file, c.dir]); + if (r.status === 0) return {ok: true}; + const why = `${r.stdout}${r.stderr}`.trim().split('\n').filter(l => !l.startsWith('ok ')).slice(-2).join('; '); + return {ok: false, reason: `check-proof-receipt.sh exit ${r.status}: ${why}`}; + }; +} + // 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) { +// cannot be fetched or fails its digest stops the run. Each receipt that gives +// a PWG-1 goes once through `gitCheck` (§8.5.3); with none, no PWG-1 is +// catalogued. +export async function deriveAll(rows, receiptsDir, readProofReceipt, gitCheck = null) { const cache = new Map(); const out = []; for (const row of rows) { let read = null; + let key = null; if (row.receipt !== null) { - const key = `${row.repo}@${row.source_commit}/${row.receipt.path}`; + 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))}); + cache.set(key, {record: readProofReceipt(text, path.basename(row.receipt.path)), text}); } catch (e) { if (!['LintError', 'ProofReceiptError'].includes(e?.name)) throw e; cache.set(key, {refusal: String(e)}); @@ -176,7 +250,14 @@ export async function deriveAll(rows, receiptsDir, readProofReceipt) { } read = cache.get(key); } - out.push({row, ...derive(row, read)}); + const d = derive(row, read); + if (d.pwg === 'PWG-1') { + const entry = cache.get(key); + entry.git ??= gitCheck ? await gitCheck(row, entry.text) : {ok: false, reason: 'no git check ran'}; + out.push({row, ...withGitCheck(d, entry.git)}); + } else { + out.push({row, ...d}); + } } return out; } @@ -230,8 +311,15 @@ export function render(derived) { async function main() { const [cmd, ...args] = process.argv.slice(2); + if (cmd === 'receipt') { + // The home gate (§8.5.3): the git checks on the receipt of Mathesis itself, + // against this clone. origin/main needs its history (CI fetches it). + const receipt = path.join(root, 'verification/receipts/theory_praxis.deed'); + const r = spawnSync('bash', [await checkerScript(), '--branch', 'origin/main', receipt, root], {stdio: 'inherit'}); + process.exit(r.status ?? 2); + } if (!['build', 'check', 'ledger'].includes(cmd)) { - console.error('usage: claims-registry.mjs build|check|ledger [--receipts-dir DIR] [--note TEXT]'); + console.error('usage: claims-registry.mjs build|check|ledger|receipt [--receipts-dir DIR] [--note TEXT]'); process.exit(2); } const i = args.indexOf('--receipts-dir'); @@ -240,7 +328,7 @@ async function main() { const rows = validate(await readJsonl(claimsFile), inventory); const bridges = validateBridges(await readJsonl(bridgesFile), inventory); const admissions = validateAdmissions(await readJsonl(admissionsFile), rows, inventory); - const derived = await deriveAll(rows, receiptsDir, await loadReader()); + const derived = await deriveAll(rows, receiptsDir, await loadReader(), receiptsDir ? null : await gitChecker()); const ledger = validateLedger(await readJsonl(ledgerFile)); const current = snapshot(rows, admissions, new Map(derived.map(d => [d.row.id, d.pwg]))); if (cmd === 'ledger') { diff --git a/tests/registry/claims-registry.test.mjs b/tests/registry/claims-registry.test.mjs index 92b515d..9516d6a 100644 --- a/tests/registry/claims-registry.test.mjs +++ b/tests/registry/claims-registry.test.mjs @@ -9,7 +9,7 @@ import {readFileSync, mkdtempSync, mkdirSync, writeFileSync, copyFileSync} from import {createHash} from 'node:crypto'; import {tmpdir} from 'node:os'; import path from 'node:path'; -import {validate, loadReader, derive, deriveAll, render, READER} from '../../scripts/registry/claims-registry.mjs'; +import {validate, loadReader, derive, deriveAll, withGitCheck, render, READER} from '../../scripts/registry/claims-registry.mjs'; import {parseJsonl} from '../../scripts/atlas/census-atlas.mjs'; const rows = parseJsonl(readFileSync(new URL('../../docs/atlas/claims/claims.jsonl', import.meta.url), 'utf8')); @@ -28,8 +28,15 @@ beforeAll(async () => { readProofReceipt = await loadReader(); }); // 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`; + // Each current receipt lists its inputs (standards e5a39d7): one manifest line, + // the digest of that manifest, and an empty axioms clause. + const run = (prover, at, inv) => { + const line = `${'c'.repeat(64)} ${prover}/M\n`; + const digest = createHash('sha256').update(line).digest('hex'); + return ` (receipt :run "ci" :commit "${at}" :checker "${prover}" :invocation "${inv}"\n` + + ` :inputs-sha256 "${digest}" :state current (axioms)\n` + + ` (inputs-manifest (file :path "${prover}/M" :sha256 "${'c'.repeat(64)}"))))\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' + @@ -126,3 +133,25 @@ test('a row names the commit that its receipt describes when it differs from the expect(v).toContain(`at \`${at.slice(0, 12)}\`; the receipt describes \`${commit.slice(0, 12)}\``); expect(render([{row: theorem, pwg: 'PWG-1', reasons: [], evidence: commit}])).not.toContain('the receipt describes'); }); + +test('a PWG-1 is catalogued only when the git checks of §8.5.3 hold', async () => { + const one = derive(theorem, read(fixture({pwg: 'PWG-1', rocq: 'RECONCILED', lean: 'RECONCILED'}))); + expect(withGitCheck(one, {ok: true})).toEqual(one); + const capped = withGitCheck(one, {ok: false, reason: 'the source commit is not on origin/main'}); + expect(capped.pwg).toBe('PWG-2ii'); + expect(capped.reasons.join()).toContain('§8.5.3 git checks: the source commit is not on origin/main; catalogued without PWG-1'); + const three = derive(theorem, read(fixture())); + expect(withGitCheck(three, {ok: false, reason: 'x'})).toEqual(three); + // deriveAll runs the check once per receipt, and with no check it catalogues no PWG-1. + const dir = mkdtempSync(path.join(tmpdir(), 'registry-')); + const text = fixture({pwg: 'PWG-1', rocq: 'RECONCILED', lean: 'RECONCILED'}); + mkdirSync(path.join(dir, `o__r@${commit}`), {recursive: true}); + writeFileSync(path.join(dir, `o__r@${commit}`, 'r_praxis.deed'), text); + const row = {...theorem, receipt: {path: 'r_praxis.deed', sha256: createHash('sha256').update(text).digest('hex')}}; + let calls = 0; + const ok = async () => { calls += 1; return {ok: true}; }; + const both = await deriveAll([row, {...row, id: 'o/r#T-1b'}], dir, readProofReceipt, ok); + expect(both.map(d => d.pwg)).toEqual(['PWG-1', 'PWG-1']); + expect(calls).toBe(1); + expect((await deriveAll([row], dir, readProofReceipt))[0].pwg).toBe('PWG-2ii'); +}); diff --git a/verification/receipts/theory_praxis.deed b/verification/receipts/theory_praxis.deed index b336890..64ec114 100644 --- a/verification/receipts/theory_praxis.deed +++ b/verification/receipts/theory_praxis.deed @@ -1,35 +1,61 @@ ;; SPDX-License-Identifier: CC-BY-SA-4.0 ;; SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) -;; The proof receipt of Mathesis (PROOF-POLICY §8.5.1), written from the THY-1 -;; record in docs/status/PROOF-STATUS.adoc (re-anchoring plan WO 1.5). The -;; current receipts come from one CI run of the proof lanes in the pinned Guix -;; (WO 1.4, Guix 8edb9da). Its log records, for each witness, the checker and -;; its version, the invocation, the SHA-256 of the file, the result and the -;; axioms reported. The local runs of 2026-11-09 stay as superseded receipts. -;; The reader in standards 1-formats/deed/tools/deed_lint.js derives the grade: +;; The proof receipt of Mathesis (PROOF-POLICY §8.5.1, standards e5a39d7), +;; written from the records of THY-1 and APP-1 to APP-4 in +;; docs/status/PROOF-STATUS.adoc. The current receipts come from one CI run of +;; the proof lanes in the pinned Guix (Guix 8edb9da) on main 034f215: run +;; 43498592499. Its log records, for each gated module, the checker and its +;; version, the SHA-256 of the file, the result and the axioms reported (none). +;; Each current receipt carries the inputs manifest of its prover: the union of +;; the first-party files that the graded roots read, from +;; standards scripts/proof-inputs-sha256.sh --manifest 034f215 PATH... +;; One manifest per prover, because §8.5.1 allows one digest for one commit and +;; one prover. Earlier receipts stay as superseded receipts, each with a reason. +;; The reader derives the grade, and the shared git checker does the §8.5.3 +;; checks (just receipt-check): ;; bun deed_lint.js --proof-receipt-json verification/receipts/theory_praxis.deed -;; The trusted base is the Agda.Primitive block of the import cone that -;; agda --dependency-graph reports for FeatureReachability; Agda 2.6.3 and -;; 2.7.0.1 postulate the same four names there (checked 2026-11-10). +;; check-proof-receipt.sh --branch origin/main verification/receipts/theory_praxis.deed . +;; The trusted base is each prover-supplied postulate that the Agda import +;; cones reach (agda --dependency-graph): the four of Agda.Primitive, and Char +;; and String, which Applied/IntLaws reaches through Agda.Builtin.Int. Agda +;; 2.7.0.1 postulates these six (its lib/prim sources, read 2026-11-13). (praxis-deed :schema-version "1.0.0" :canonical-name "mathesis-theory-receipt" :beholding-chora #u5"estate/chora" :profile proof-receipt :repository "hyperpolymath/mathesis" - :source-commit "336768958d01257caae14cb81fb54197c2617d97" + :source-commit "034f215b3b601aa6bdde7471bdc650bc62c0f56c" (trusted-base (primitive :prover agda :module "Agda.Primitive" :name "Level" :binding "BUILTIN LEVEL") (primitive :prover agda :module "Agda.Primitive" :name "lzero" :binding "BUILTIN LEVELZERO") (primitive :prover agda :module "Agda.Primitive" :name "lsuc" :binding "BUILTIN LEVELSUC") - (primitive :prover agda :module "Agda.Primitive" :name "_⊔_" :binding "BUILTIN LEVELMAX")) + (primitive :prover agda :module "Agda.Primitive" :name "_⊔_" :binding "BUILTIN LEVELMAX") + (primitive :prover agda :module "Agda.Builtin.Char" :name "Char" :binding "BUILTIN CHAR") + (primitive :prover agda :module "Agda.Builtin.String" :name "String" :binding "BUILTIN STRING")) (claim :id "THY-1" :pwg PWG-1 :foundation-diverse #f (leg :prover agda :route source :token proven :state AGDA-VERIFIED + (receipt :run "https://github.com/hyperpolymath/mathesis/actions/runs/43498592499/job/132138258520" + :commit "034f215b3b601aa6bdde7471bdc650bc62c0f56c" + :checker "agda 2.7.0.1 (Guix 8edb9da)" + :invocation "agda --safe --without-K --cubical-compatible FeatureReachability.agda" + :inputs-sha256 "4db97b78050ef622485ceb179e80ad9f39dbd986cdd6f45af0fd5b32a410c643" + :state current + (axioms) + (inputs-manifest + (file :path "verification/proofs/agda/Applied/Cash.agda" :sha256 "fe231a7679529e7998385d8acdcaf8cde6880e44a5cc5d5cc3c03fd4ac2eea12") + (file :path "verification/proofs/agda/Applied/Cohort.agda" :sha256 "5a485d5fd5329939aa85909e65bc200d886316ebb69e9786b2764dd17eba8d56") + (file :path "verification/proofs/agda/Applied/IntLaws.agda" :sha256 "09285481b29234fced3197b1a4fcd86f284a66f5ce011d23b68bb1aa602c91fb") + (file :path "verification/proofs/agda/Applied/IntNumber.agda" :sha256 "0ba5ca46fd22d0abb4f7ceb0ff73a7857f7a3acc6143a43a68cf5932e8868959") + (file :path "verification/proofs/agda/Applied/Missing.agda" :sha256 "4afb4c82e84bf6411b0f0c19eb6d34869a42bee7d5616624147d1881c78b6fe9") + (file :path "verification/proofs/agda/Applied/Status.agda" :sha256 "d059344565a55b897824b83b4f676b9a7326ba50a5b35a6da49ab72bb40e8a97") + (file :path "verification/proofs/agda/FeatureReachability.agda" :sha256 "4e39d6ae751d97d3edf57720ccf844d90de3e9ee6603901a04f5eb6494d94564"))) (receipt :run "https://github.com/hyperpolymath/mathesis/actions/runs/42896264290/job/130110238086" :commit "336768958d01257caae14cb81fb54197c2617d97" :checker "agda 2.7.0.1 (Guix 8edb9da)" :invocation "agda --safe --without-K --cubical-compatible FeatureReachability.agda" - :state current) + :state superseded + :reason "replaced by the CI receipt of run 43498592499 on 034f215, which records the inputs digest and the axioms (PROOF-POLICY 8.5.1, standards d9b03a3)") (receipt :run "local run, 2026-11-09" :commit "f68b78d6ceb8d3c83f96f5ab8e57779442a8834f" :checker "agda 2.6.3 (Ubuntu 24.04 agda package)" @@ -37,11 +63,22 @@ :state superseded :reason "replaced by the CI receipt in the pinned Guix, Agda 2.7.0.1")) (leg :prover rocq :route re-proved :token proven :state RECONCILED + (receipt :run "https://github.com/hyperpolymath/mathesis/actions/runs/43498592499/job/132138258520" + :commit "034f215b3b601aa6bdde7471bdc650bc62c0f56c" + :checker "coqc 8.18.0 (Guix 8edb9da)" + :invocation "coqc FeatureReachability.v" + :inputs-sha256 "1c5814d6040f119382ebeccffe477cbd7d8485a45cf9e8877782316378e28709" + :state current + (axioms) + (inputs-manifest + (file :path "verification/proofs/coq/Cohort.v" :sha256 "2519cdbdb3b22ee5132e5708bbbeb9e87e3b2d8c2c318329c96c0545863b6260") + (file :path "verification/proofs/coq/FeatureReachability.v" :sha256 "e2f90043366fb8061784da4cd12af3278e8a9ea0af78fdba4490f96f28b68cb1"))) (receipt :run "https://github.com/hyperpolymath/mathesis/actions/runs/42896264290/job/130110238086" :commit "336768958d01257caae14cb81fb54197c2617d97" :checker "coqc 8.18.0 (Guix 8edb9da)" :invocation "coqc FeatureReachability.v" - :state current) + :state superseded + :reason "replaced by the CI receipt of run 43498592499 on 034f215, which records the inputs digest and the axioms (PROOF-POLICY 8.5.1, standards d9b03a3)") (receipt :run "local run, 2026-11-09" :commit "f1be654e69b23873ea40651cb40e0e095ac53680" :checker "coqc 8.18.0 (Ubuntu 24.04 coq package)" @@ -49,14 +86,186 @@ :state superseded :reason "replaced by the CI receipt in the pinned Guix")) (leg :prover lean :route re-proved :token proven :state RECONCILED + (receipt :run "https://github.com/hyperpolymath/mathesis/actions/runs/43498592499/job/132138258520" + :commit "034f215b3b601aa6bdde7471bdc650bc62c0f56c" + :checker "lean 4.29.0 (Guix 8edb9da)" + :invocation "lean FeatureReachability.lean" + :inputs-sha256 "de2e3324f91b25f4a05658dfcfb435c7417709667b8766f7aeaa832fa874c4c1" + :state current + (axioms) + (inputs-manifest + (file :path "verification/proofs/lean4/Cohort.lean" :sha256 "b91e2aa7b1322284d67710ea918858497bc1245a6b941448df2deba4b521ce10") + (file :path "verification/proofs/lean4/FeatureReachability.lean" :sha256 "4158e54f85c8e83e49789869a4e9b12fe4b8d7460981f5c8442479268f17d55a") + (file :path "verification/proofs/lean4/lean-toolchain" :sha256 "651c8accb402b0c071cd336e9d3dc0a55516b1bfb434ddc4801f14936785b1d2"))) (receipt :run "https://github.com/hyperpolymath/mathesis/actions/runs/42896264290/job/130110238086" :commit "336768958d01257caae14cb81fb54197c2617d97" :checker "lean 4.29.0 (Guix 8edb9da)" :invocation "lean FeatureReachability.lean" - :state current) + :state superseded + :reason "replaced by the CI receipt of run 43498592499 on 034f215, which records the inputs digest and the axioms (PROOF-POLICY 8.5.1, standards d9b03a3)") (receipt :run "local run, 2026-11-09" :commit "f1be654e69b23873ea40651cb40e0e095ac53680" :checker "lean 4.15.0 (11651562caae, release archive)" :invocation "lean FeatureReachability.lean" :state superseded - :reason "replaced by the CI receipt in the pinned Guix, Lean 4.29.0")))) + :reason "replaced by the CI receipt in the pinned Guix, Lean 4.29.0"))) + (claim :id "APP-1" :pwg PWG-1 :foundation-diverse #f + (leg :prover agda :route source :token proven :state AGDA-VERIFIED + (receipt :run "https://github.com/hyperpolymath/mathesis/actions/runs/43498592499/job/132138258520" + :commit "034f215b3b601aa6bdde7471bdc650bc62c0f56c" + :checker "agda 2.7.0.1 (Guix 8edb9da)" + :invocation "agda --safe --without-K --cubical-compatible Applied/Missing.agda" + :inputs-sha256 "4db97b78050ef622485ceb179e80ad9f39dbd986cdd6f45af0fd5b32a410c643" + :state current + (axioms) + (inputs-manifest + (file :path "verification/proofs/agda/Applied/Cash.agda" :sha256 "fe231a7679529e7998385d8acdcaf8cde6880e44a5cc5d5cc3c03fd4ac2eea12") + (file :path "verification/proofs/agda/Applied/Cohort.agda" :sha256 "5a485d5fd5329939aa85909e65bc200d886316ebb69e9786b2764dd17eba8d56") + (file :path "verification/proofs/agda/Applied/IntLaws.agda" :sha256 "09285481b29234fced3197b1a4fcd86f284a66f5ce011d23b68bb1aa602c91fb") + (file :path "verification/proofs/agda/Applied/IntNumber.agda" :sha256 "0ba5ca46fd22d0abb4f7ceb0ff73a7857f7a3acc6143a43a68cf5932e8868959") + (file :path "verification/proofs/agda/Applied/Missing.agda" :sha256 "4afb4c82e84bf6411b0f0c19eb6d34869a42bee7d5616624147d1881c78b6fe9") + (file :path "verification/proofs/agda/Applied/Status.agda" :sha256 "d059344565a55b897824b83b4f676b9a7326ba50a5b35a6da49ab72bb40e8a97") + (file :path "verification/proofs/agda/FeatureReachability.agda" :sha256 "4e39d6ae751d97d3edf57720ccf844d90de3e9ee6603901a04f5eb6494d94564")))) + (leg :prover rocq :route re-proved :token proven :state RECONCILED + (receipt :run "https://github.com/hyperpolymath/mathesis/actions/runs/43498592499/job/132138258520" + :commit "034f215b3b601aa6bdde7471bdc650bc62c0f56c" + :checker "coqc 8.18.0 (Guix 8edb9da)" + :invocation "coqc Cohort.v" + :inputs-sha256 "1c5814d6040f119382ebeccffe477cbd7d8485a45cf9e8877782316378e28709" + :state current + (axioms) + (inputs-manifest + (file :path "verification/proofs/coq/Cohort.v" :sha256 "2519cdbdb3b22ee5132e5708bbbeb9e87e3b2d8c2c318329c96c0545863b6260") + (file :path "verification/proofs/coq/FeatureReachability.v" :sha256 "e2f90043366fb8061784da4cd12af3278e8a9ea0af78fdba4490f96f28b68cb1")))) + (leg :prover lean :route re-proved :token proven :state RECONCILED + (receipt :run "https://github.com/hyperpolymath/mathesis/actions/runs/43498592499/job/132138258520" + :commit "034f215b3b601aa6bdde7471bdc650bc62c0f56c" + :checker "lean 4.29.0 (Guix 8edb9da)" + :invocation "lean Cohort.lean" + :inputs-sha256 "de2e3324f91b25f4a05658dfcfb435c7417709667b8766f7aeaa832fa874c4c1" + :state current + (axioms) + (inputs-manifest + (file :path "verification/proofs/lean4/Cohort.lean" :sha256 "b91e2aa7b1322284d67710ea918858497bc1245a6b941448df2deba4b521ce10") + (file :path "verification/proofs/lean4/FeatureReachability.lean" :sha256 "4158e54f85c8e83e49789869a4e9b12fe4b8d7460981f5c8442479268f17d55a") + (file :path "verification/proofs/lean4/lean-toolchain" :sha256 "651c8accb402b0c071cd336e9d3dc0a55516b1bfb434ddc4801f14936785b1d2"))))) + (claim :id "APP-2" :pwg PWG-1 :foundation-diverse #f + (leg :prover agda :route source :token proven :state AGDA-VERIFIED + (receipt :run "https://github.com/hyperpolymath/mathesis/actions/runs/43498592499/job/132138258520" + :commit "034f215b3b601aa6bdde7471bdc650bc62c0f56c" + :checker "agda 2.7.0.1 (Guix 8edb9da)" + :invocation "agda --safe --without-K --cubical-compatible Applied/IntLaws.agda" + :inputs-sha256 "4db97b78050ef622485ceb179e80ad9f39dbd986cdd6f45af0fd5b32a410c643" + :state current + (axioms) + (inputs-manifest + (file :path "verification/proofs/agda/Applied/Cash.agda" :sha256 "fe231a7679529e7998385d8acdcaf8cde6880e44a5cc5d5cc3c03fd4ac2eea12") + (file :path "verification/proofs/agda/Applied/Cohort.agda" :sha256 "5a485d5fd5329939aa85909e65bc200d886316ebb69e9786b2764dd17eba8d56") + (file :path "verification/proofs/agda/Applied/IntLaws.agda" :sha256 "09285481b29234fced3197b1a4fcd86f284a66f5ce011d23b68bb1aa602c91fb") + (file :path "verification/proofs/agda/Applied/IntNumber.agda" :sha256 "0ba5ca46fd22d0abb4f7ceb0ff73a7857f7a3acc6143a43a68cf5932e8868959") + (file :path "verification/proofs/agda/Applied/Missing.agda" :sha256 "4afb4c82e84bf6411b0f0c19eb6d34869a42bee7d5616624147d1881c78b6fe9") + (file :path "verification/proofs/agda/Applied/Status.agda" :sha256 "d059344565a55b897824b83b4f676b9a7326ba50a5b35a6da49ab72bb40e8a97") + (file :path "verification/proofs/agda/FeatureReachability.agda" :sha256 "4e39d6ae751d97d3edf57720ccf844d90de3e9ee6603901a04f5eb6494d94564")))) + (leg :prover rocq :route re-proved :token proven :state RECONCILED + (receipt :run "https://github.com/hyperpolymath/mathesis/actions/runs/43498592499/job/132138258520" + :commit "034f215b3b601aa6bdde7471bdc650bc62c0f56c" + :checker "coqc 8.18.0 (Guix 8edb9da)" + :invocation "coqc Cohort.v" + :inputs-sha256 "1c5814d6040f119382ebeccffe477cbd7d8485a45cf9e8877782316378e28709" + :state current + (axioms) + (inputs-manifest + (file :path "verification/proofs/coq/Cohort.v" :sha256 "2519cdbdb3b22ee5132e5708bbbeb9e87e3b2d8c2c318329c96c0545863b6260") + (file :path "verification/proofs/coq/FeatureReachability.v" :sha256 "e2f90043366fb8061784da4cd12af3278e8a9ea0af78fdba4490f96f28b68cb1")))) + (leg :prover lean :route re-proved :token proven :state RECONCILED + (receipt :run "https://github.com/hyperpolymath/mathesis/actions/runs/43498592499/job/132138258520" + :commit "034f215b3b601aa6bdde7471bdc650bc62c0f56c" + :checker "lean 4.29.0 (Guix 8edb9da)" + :invocation "lean Cohort.lean" + :inputs-sha256 "de2e3324f91b25f4a05658dfcfb435c7417709667b8766f7aeaa832fa874c4c1" + :state current + (axioms) + (inputs-manifest + (file :path "verification/proofs/lean4/Cohort.lean" :sha256 "b91e2aa7b1322284d67710ea918858497bc1245a6b941448df2deba4b521ce10") + (file :path "verification/proofs/lean4/FeatureReachability.lean" :sha256 "4158e54f85c8e83e49789869a4e9b12fe4b8d7460981f5c8442479268f17d55a") + (file :path "verification/proofs/lean4/lean-toolchain" :sha256 "651c8accb402b0c071cd336e9d3dc0a55516b1bfb434ddc4801f14936785b1d2"))))) + (claim :id "APP-3" :pwg PWG-1 :foundation-diverse #f + (leg :prover agda :route source :token proven :state AGDA-VERIFIED + (receipt :run "https://github.com/hyperpolymath/mathesis/actions/runs/43498592499/job/132138258520" + :commit "034f215b3b601aa6bdde7471bdc650bc62c0f56c" + :checker "agda 2.7.0.1 (Guix 8edb9da)" + :invocation "agda --safe --without-K --cubical-compatible Applied/IntLaws.agda" + :inputs-sha256 "4db97b78050ef622485ceb179e80ad9f39dbd986cdd6f45af0fd5b32a410c643" + :state current + (axioms) + (inputs-manifest + (file :path "verification/proofs/agda/Applied/Cash.agda" :sha256 "fe231a7679529e7998385d8acdcaf8cde6880e44a5cc5d5cc3c03fd4ac2eea12") + (file :path "verification/proofs/agda/Applied/Cohort.agda" :sha256 "5a485d5fd5329939aa85909e65bc200d886316ebb69e9786b2764dd17eba8d56") + (file :path "verification/proofs/agda/Applied/IntLaws.agda" :sha256 "09285481b29234fced3197b1a4fcd86f284a66f5ce011d23b68bb1aa602c91fb") + (file :path "verification/proofs/agda/Applied/IntNumber.agda" :sha256 "0ba5ca46fd22d0abb4f7ceb0ff73a7857f7a3acc6143a43a68cf5932e8868959") + (file :path "verification/proofs/agda/Applied/Missing.agda" :sha256 "4afb4c82e84bf6411b0f0c19eb6d34869a42bee7d5616624147d1881c78b6fe9") + (file :path "verification/proofs/agda/Applied/Status.agda" :sha256 "d059344565a55b897824b83b4f676b9a7326ba50a5b35a6da49ab72bb40e8a97") + (file :path "verification/proofs/agda/FeatureReachability.agda" :sha256 "4e39d6ae751d97d3edf57720ccf844d90de3e9ee6603901a04f5eb6494d94564")))) + (leg :prover rocq :route re-proved :token proven :state RECONCILED + (receipt :run "https://github.com/hyperpolymath/mathesis/actions/runs/43498592499/job/132138258520" + :commit "034f215b3b601aa6bdde7471bdc650bc62c0f56c" + :checker "coqc 8.18.0 (Guix 8edb9da)" + :invocation "coqc Cohort.v" + :inputs-sha256 "1c5814d6040f119382ebeccffe477cbd7d8485a45cf9e8877782316378e28709" + :state current + (axioms) + (inputs-manifest + (file :path "verification/proofs/coq/Cohort.v" :sha256 "2519cdbdb3b22ee5132e5708bbbeb9e87e3b2d8c2c318329c96c0545863b6260") + (file :path "verification/proofs/coq/FeatureReachability.v" :sha256 "e2f90043366fb8061784da4cd12af3278e8a9ea0af78fdba4490f96f28b68cb1")))) + (leg :prover lean :route re-proved :token proven :state RECONCILED + (receipt :run "https://github.com/hyperpolymath/mathesis/actions/runs/43498592499/job/132138258520" + :commit "034f215b3b601aa6bdde7471bdc650bc62c0f56c" + :checker "lean 4.29.0 (Guix 8edb9da)" + :invocation "lean Cohort.lean" + :inputs-sha256 "de2e3324f91b25f4a05658dfcfb435c7417709667b8766f7aeaa832fa874c4c1" + :state current + (axioms) + (inputs-manifest + (file :path "verification/proofs/lean4/Cohort.lean" :sha256 "b91e2aa7b1322284d67710ea918858497bc1245a6b941448df2deba4b521ce10") + (file :path "verification/proofs/lean4/FeatureReachability.lean" :sha256 "4158e54f85c8e83e49789869a4e9b12fe4b8d7460981f5c8442479268f17d55a") + (file :path "verification/proofs/lean4/lean-toolchain" :sha256 "651c8accb402b0c071cd336e9d3dc0a55516b1bfb434ddc4801f14936785b1d2"))))) + (claim :id "APP-4" :pwg PWG-1 :foundation-diverse #f + (leg :prover agda :route source :token proven :state AGDA-VERIFIED + (receipt :run "https://github.com/hyperpolymath/mathesis/actions/runs/43498592499/job/132138258520" + :commit "034f215b3b601aa6bdde7471bdc650bc62c0f56c" + :checker "agda 2.7.0.1 (Guix 8edb9da)" + :invocation "agda --safe --without-K --cubical-compatible Applied/Missing.agda" + :inputs-sha256 "4db97b78050ef622485ceb179e80ad9f39dbd986cdd6f45af0fd5b32a410c643" + :state current + (axioms) + (inputs-manifest + (file :path "verification/proofs/agda/Applied/Cash.agda" :sha256 "fe231a7679529e7998385d8acdcaf8cde6880e44a5cc5d5cc3c03fd4ac2eea12") + (file :path "verification/proofs/agda/Applied/Cohort.agda" :sha256 "5a485d5fd5329939aa85909e65bc200d886316ebb69e9786b2764dd17eba8d56") + (file :path "verification/proofs/agda/Applied/IntLaws.agda" :sha256 "09285481b29234fced3197b1a4fcd86f284a66f5ce011d23b68bb1aa602c91fb") + (file :path "verification/proofs/agda/Applied/IntNumber.agda" :sha256 "0ba5ca46fd22d0abb4f7ceb0ff73a7857f7a3acc6143a43a68cf5932e8868959") + (file :path "verification/proofs/agda/Applied/Missing.agda" :sha256 "4afb4c82e84bf6411b0f0c19eb6d34869a42bee7d5616624147d1881c78b6fe9") + (file :path "verification/proofs/agda/Applied/Status.agda" :sha256 "d059344565a55b897824b83b4f676b9a7326ba50a5b35a6da49ab72bb40e8a97") + (file :path "verification/proofs/agda/FeatureReachability.agda" :sha256 "4e39d6ae751d97d3edf57720ccf844d90de3e9ee6603901a04f5eb6494d94564")))) + (leg :prover rocq :route re-proved :token proven :state RECONCILED + (receipt :run "https://github.com/hyperpolymath/mathesis/actions/runs/43498592499/job/132138258520" + :commit "034f215b3b601aa6bdde7471bdc650bc62c0f56c" + :checker "coqc 8.18.0 (Guix 8edb9da)" + :invocation "coqc Cohort.v" + :inputs-sha256 "1c5814d6040f119382ebeccffe477cbd7d8485a45cf9e8877782316378e28709" + :state current + (axioms) + (inputs-manifest + (file :path "verification/proofs/coq/Cohort.v" :sha256 "2519cdbdb3b22ee5132e5708bbbeb9e87e3b2d8c2c318329c96c0545863b6260") + (file :path "verification/proofs/coq/FeatureReachability.v" :sha256 "e2f90043366fb8061784da4cd12af3278e8a9ea0af78fdba4490f96f28b68cb1")))) + (leg :prover lean :route re-proved :token proven :state RECONCILED + (receipt :run "https://github.com/hyperpolymath/mathesis/actions/runs/43498592499/job/132138258520" + :commit "034f215b3b601aa6bdde7471bdc650bc62c0f56c" + :checker "lean 4.29.0 (Guix 8edb9da)" + :invocation "lean Cohort.lean" + :inputs-sha256 "de2e3324f91b25f4a05658dfcfb435c7417709667b8766f7aeaa832fa874c4c1" + :state current + (axioms) + (inputs-manifest + (file :path "verification/proofs/lean4/Cohort.lean" :sha256 "b91e2aa7b1322284d67710ea918858497bc1245a6b941448df2deba4b521ce10") + (file :path "verification/proofs/lean4/FeatureReachability.lean" :sha256 "4158e54f85c8e83e49789869a4e9b12fe4b8d7460981f5c8442479268f17d55a") + (file :path "verification/proofs/lean4/lean-toolchain" :sha256 "651c8accb402b0c071cd336e9d3dc0a55516b1bfb434ddc4801f14936785b1d2")))))) From 733fb8c57ab7659aaeca8b9e8df25d79c20cc8ae Mon Sep 17 00:00:00 2001 From: Claude Date: Fri, 13 Nov 2026 21:42:59 +0000 Subject: [PATCH 2/7] ci(tests): read the receipt with the reader at e5a39d7 in proven-tests The Proven test suite pinned its own checkout of the reader at be39f90, which refuses the new :inputs-sha256 field (run 43513006338). Pin it at e5a39d7, the commit the registry pins, and add the two checker scripts that the registry's git checks need to its sparse checkout. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_0136P7Zo9dheFQzYYWV49hAk --- .github/workflows/proven-tests.yml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/.github/workflows/proven-tests.yml b/.github/workflows/proven-tests.yml index db5f05e..241c96c 100644 --- a/.github/workflows/proven-tests.yml +++ b/.github/workflows/proven-tests.yml @@ -56,8 +56,8 @@ jobs: git init -q "$r" git -C "$r" remote add origin https://github.com/metadatastician/standards.git git -C "$r" config core.sparseCheckout true - printf '1-formats/deed/tools/\n' > "$r/.git/info/sparse-checkout" - git -C "$r" fetch -q --depth 1 origin be39f900665fb7c042c05d1165da018adc1860f4 + printf '1-formats/deed/tools/\nscripts/check-proof-receipt.sh\nscripts/proof-inputs-sha256.sh\n' > "$r/.git/info/sparse-checkout" + git -C "$r" fetch -q --depth 1 origin e5a39d7e5c66f9d24d7e0ffa3f8dbd01f2d42d9d git -C "$r" checkout -q FETCH_HEAD for f in verification/receipts/*_praxis.deed; do bun "$r/1-formats/deed/tools/deed_lint.js" --proof-receipt-json "$f" From bdcc59925030eef68c64b3d8d836de59899d2b8e Mon Sep 17 00:00:00 2001 From: Claude Date: Fri, 13 Nov 2026 21:44:20 +0000 Subject: [PATCH 3/7] registry: run git and bash by absolute path; read receipts without a loop Answers the SonarCloud findings on the git checks: S4036 (a program found through PATH), S3776 (deriveAll too complex) and S9382 (await in a loop). Each program now runs by its absolute path, found in an absolute directory of PATH, as scripts/site/site.mjs does for asciidoctor. deriveAll reads each distinct receipt once, derives, then runs each needed git check once. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_0136P7Zo9dheFQzYYWV49hAk --- scripts/registry/claims-registry.mjs | 62 +++++++++++++------------ tests/registry/claims-registry.test.mjs | 7 ++- 2 files changed, 38 insertions(+), 31 deletions(-) diff --git a/scripts/registry/claims-registry.mjs b/scripts/registry/claims-registry.mjs index fcd10ea..21520e6 100644 --- a/scripts/registry/claims-registry.mjs +++ b/scripts/registry/claims-registry.mjs @@ -23,6 +23,7 @@ // --receipts-dir DIR reads receipts from DIR/__@/ // instead of fetching them (the tests use it; CI fetches). import {readFile, writeFile, mkdir, mkdtemp} from 'node:fs/promises'; +import {existsSync} from 'node:fs'; import {spawnSync} from 'node:child_process'; import {tmpdir} from 'node:os'; import {createHash} from 'node:crypto'; @@ -177,7 +178,16 @@ export function withGitCheck(d, check) { return {...d, pwg: 'PWG-2ii', reasons: [...d.reasons, `§8.5.3 git checks: ${check.reason}; catalogued without PWG-1`]}; } -const run = (cmd, args) => spawnSync(cmd, args, {encoding: 'utf8'}); +// A program in an absolute directory of PATH, run by its absolute path, so that no +// relative PATH entry can pick the program. +export function findTool(name, env = process.env) { + for (const d of (env.PATH || '').split(path.delimiter)) { + if (path.isAbsolute(d) && existsSync(path.join(d, name))) return path.join(d, name); + } + throw new Error(`${name} not found in an absolute directory of PATH`); +} + +const run = (cmd, args) => spawnSync(findTool(cmd), args, {encoding: 'utf8'}); // The path of the pinned checker, after the digest checks of both pinned // scripts in the standards checkout. @@ -226,40 +236,32 @@ export async function gitChecker(standardsDir = process.env.MATHESIS_STANDARDS) }; } +// The reader's record of one receipt text: {record, text} or {refusal}. +function readReceipt(text, row, readProofReceipt) { + try { + return {record: readProofReceipt(text, path.basename(row.receipt.path)), text}; + } catch (e) { + if (!['LintError', 'ProofReceiptError'].includes(e?.name)) throw e; + return {refusal: String(e)}; + } +} + +const receiptKey = row => (row.receipt === null ? null : `${row.repo}@${row.source_commit}/${row.receipt.path}`); + // 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. Each receipt that gives // a PWG-1 goes once through `gitCheck` (§8.5.3); with none, no PWG-1 is // catalogued. export async function deriveAll(rows, receiptsDir, readProofReceipt, gitCheck = null) { - const cache = new Map(); - const out = []; - for (const row of rows) { - let read = null; - let key = null; - if (row.receipt !== null) { - 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)), text}); - } catch (e) { - if (!['LintError', 'ProofReceiptError'].includes(e?.name)) throw e; - cache.set(key, {refusal: String(e)}); - } - } - read = cache.get(key); - } - const d = derive(row, read); - if (d.pwg === 'PWG-1') { - const entry = cache.get(key); - entry.git ??= gitCheck ? await gitCheck(row, entry.text) : {ok: false, reason: 'no git check ran'}; - out.push({row, ...withGitCheck(d, entry.git)}); - } else { - out.push({row, ...d}); - } - } - return out; + const once = list => [...new Map(list.map(row => [receiptKey(row), row]))]; + const reads = new Map(await Promise.all(once(rows.filter(receiptKey)).map(async ([key, row]) => + [key, readReceipt(await loadReceipt(row, receiptsDir), row, readProofReceipt)]))); + const derived = rows.map(row => ({row, ...derive(row, reads.get(receiptKey(row)) ?? null)})); + const graded = derived.filter(d => d.pwg === 'PWG-1').map(d => d.row); + const checks = new Map(await Promise.all(once(graded).map(async ([key, row]) => + [key, gitCheck ? await gitCheck(row, reads.get(key).text) : {ok: false, reason: 'no git check ran'}]))); + return derived.map(d => (d.pwg === 'PWG-1' ? withGitCheck(d, checks.get(receiptKey(d.row))) : d)); } // ── Rendering ──────────────────────────────────────────────────────────────── @@ -315,7 +317,7 @@ async function main() { // The home gate (§8.5.3): the git checks on the receipt of Mathesis itself, // against this clone. origin/main needs its history (CI fetches it). const receipt = path.join(root, 'verification/receipts/theory_praxis.deed'); - const r = spawnSync('bash', [await checkerScript(), '--branch', 'origin/main', receipt, root], {stdio: 'inherit'}); + const r = spawnSync(findTool('bash'), [await checkerScript(), '--branch', 'origin/main', receipt, root], {stdio: 'inherit'}); process.exit(r.status ?? 2); } if (!['build', 'check', 'ledger'].includes(cmd)) { diff --git a/tests/registry/claims-registry.test.mjs b/tests/registry/claims-registry.test.mjs index 9516d6a..69e09fb 100644 --- a/tests/registry/claims-registry.test.mjs +++ b/tests/registry/claims-registry.test.mjs @@ -9,7 +9,7 @@ import {readFileSync, mkdtempSync, mkdirSync, writeFileSync, copyFileSync} from import {createHash} from 'node:crypto'; import {tmpdir} from 'node:os'; import path from 'node:path'; -import {validate, loadReader, derive, deriveAll, withGitCheck, render, READER} from '../../scripts/registry/claims-registry.mjs'; +import {validate, loadReader, derive, deriveAll, withGitCheck, findTool, render, READER} from '../../scripts/registry/claims-registry.mjs'; import {parseJsonl} from '../../scripts/atlas/census-atlas.mjs'; const rows = parseJsonl(readFileSync(new URL('../../docs/atlas/claims/claims.jsonl', import.meta.url), 'utf8')); @@ -155,3 +155,8 @@ test('a PWG-1 is catalogued only when the git checks of §8.5.3 hold', async () expect(calls).toBe(1); expect((await deriveAll([row], dir, readProofReceipt))[0].pwg).toBe('PWG-2ii'); }); + +test('git and bash run only from an absolute directory of PATH', () => { + expect(path.isAbsolute(findTool('bash'))).toBe(true); + expect(() => findTool('bash', {PATH: 'relative/bin'})).toThrow(/not found in an absolute directory/); +}); From 30841ed6945249a3f72ee1e5c820124d13c45f86 Mon Sep 17 00:00:00 2001 From: Claude Date: Sat, 14 Nov 2026 09:01:35 +0000 Subject: [PATCH 4/7] registry: pin the secret-types claims at its main 4ed0672 (WO 5.1) secret-types pull request 42 records inputs manifests and runs the shared git checker. Its receipt at main 4ed0672 names 292d566, with the echo 7dfeab2 -> 292d566 for the squash merge of its pull request 40. The reader at standards e5a39d7 derives PWG-1 for N-1, N-2, N-3, N-7, N-8 and N-9, and the registry's git checks (PROOF-POLICY 8.5.3) hold, so the registry catalogues six PWG-1. The pinned Agda modules and names exist at 4ed0672. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_0136P7Zo9dheFQzYYWV49hAk --- docs/atlas/claims/claims.jsonl | 18 +++++++++--------- docs/atlas/generated/registry.adoc | 20 ++++++++++---------- docs/status/ROADMAP.adoc | 8 ++++++-- 3 files changed, 25 insertions(+), 21 deletions(-) diff --git a/docs/atlas/claims/claims.jsonl b/docs/atlas/claims/claims.jsonl index ac21f92..adcbd1e 100644 --- a/docs/atlas/claims/claims.jsonl +++ b/docs/atlas/claims/claims.jsonl @@ -1,12 +1,12 @@ -{"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":"SecretTypes.Noninterference","names":["tini"]},"claim":"N-1","id":"hyperpolymath/secret-types#N-1","kind":"theorem","receipt":{"path":"verification/receipts/agda_praxis.deed","sha256":"4ed7e550e399074cc8a93bd190f193a0fea78de97d54e27889263b9d386ce9cc"},"repo":"hyperpolymath/secret-types","source_commit":"4ed067220f1357b37f7d54c5ae0690ff35b292bd","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_praxis.deed","sha256":"4ed7e550e399074cc8a93bd190f193a0fea78de97d54e27889263b9d386ce9cc"},"repo":"hyperpolymath/secret-types","source_commit":"4ed067220f1357b37f7d54c5ae0690ff35b292bd","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_praxis.deed","sha256":"4ed7e550e399074cc8a93bd190f193a0fea78de97d54e27889263b9d386ce9cc"},"repo":"hyperpolymath/secret-types","source_commit":"4ed067220f1357b37f7d54c5ae0690ff35b292bd","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_praxis.deed","sha256":"4ed7e550e399074cc8a93bd190f193a0fea78de97d54e27889263b9d386ce9cc"},"repo":"hyperpolymath/secret-types","source_commit":"4ed067220f1357b37f7d54c5ae0690ff35b292bd","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_praxis.deed","sha256":"4ed7e550e399074cc8a93bd190f193a0fea78de97d54e27889263b9d386ce9cc"},"repo":"hyperpolymath/secret-types","source_commit":"4ed067220f1357b37f7d54c5ae0690ff35b292bd","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_praxis.deed","sha256":"4ed7e550e399074cc8a93bd190f193a0fea78de97d54e27889263b9d386ce9cc"},"repo":"hyperpolymath/secret-types","source_commit":"4ed067220f1357b37f7d54c5ae0690ff35b292bd","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_praxis.deed","sha256":"4ed7e550e399074cc8a93bd190f193a0fea78de97d54e27889263b9d386ce9cc"},"repo":"hyperpolymath/secret-types","source_commit":"4ed067220f1357b37f7d54c5ae0690ff35b292bd","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_praxis.deed","sha256":"4ed7e550e399074cc8a93bd190f193a0fea78de97d54e27889263b9d386ce9cc"},"repo":"hyperpolymath/secret-types","source_commit":"4ed067220f1357b37f7d54c5ae0690ff35b292bd","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_praxis.deed","sha256":"4ed7e550e399074cc8a93bd190f193a0fea78de97d54e27889263b9d386ce9cc"},"repo":"hyperpolymath/secret-types","source_commit":"4ed067220f1357b37f7d54c5ae0690ff35b292bd","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"} diff --git a/docs/atlas/generated/registry.adoc b/docs/atlas/generated/registry.adoc index b3c9c42..8d796c6 100644 --- a/docs/atlas/generated/registry.adoc +++ b/docs/atlas/generated/registry.adoc @@ -10,7 +10,7 @@ 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: 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`, 13 `ungraded`, of 13 theorems. 5 demonstrations and assumptions are listed and not graded. +Census: 6 at `PWG-1`, 0 at `PWG-2ii`, 0 at `PWG-2i`, 0 at `PWG-3`, 7 `ungraded`, of 13 theorems. 5 demonstrations and assumptions are listed and not graded. [cols="2,1,1,4,3",options="header"] |=== @@ -18,23 +18,23 @@ Census: 0 at `PWG-1`, 0 at `PWG-2ii`, 0 at `PWG-2i`, 0 at `PWG-3`, 13 `ungraded` |https://github.com/hyperpolymath/mathesis/blob/9aa1662da5b2ac4a0e37b9f75a151bb312a8cbea/docs/status/PROOF-STATUS.adoc[hyperpolymath/mathesis#THY-1] at `9aa1662da5b2` |theorem |`ungraded` |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`) |the canon reader refuses the receipt: a receipt of the agda leg of claim "THY-1" is current and is missing :inputs-sha256 (§8.5.1) -|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/4ed067220f1357b37f7d54c5ae0690ff35b292bd/PROOF-STATUS.adoc[hyperpolymath/secret-types#N-1] at `4ed067220f13`; the receipt describes `292d566a81a9` |theorem |`PWG-1` |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`) |— -|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/4ed067220f1357b37f7d54c5ae0690ff35b292bd/PROOF-STATUS.adoc[hyperpolymath/secret-types#N-2] at `4ed067220f13`; the receipt describes `292d566a81a9` |theorem |`PWG-1` |Public expressions read the same in low-equivalent stores (`SecretTypes.Noninterference`: `eval-low`) |— -|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/4ed067220f1357b37f7d54c5ae0690ff35b292bd/PROOF-STATUS.adoc[hyperpolymath/secret-types#N-3] at `4ed067220f13`; the receipt describes `292d566a81a9` |theorem |`PWG-1` |Confinement: under a secret program counter the public variable is unchanged, loops included (`SecretTypes.Noninterference`: `confine`) |— -|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/4ed067220f1357b37f7d54c5ae0690ff35b292bd/PROOF-STATUS.adoc[hyperpolymath/secret-types#N-4] at `4ed067220f13` |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/4ed067220f1357b37f7d54c5ae0690ff35b292bd/PROOF-STATUS.adoc[hyperpolymath/secret-types#N-5] at `4ed067220f13` |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/4ed067220f1357b37f7d54c5ae0690ff35b292bd/PROOF-STATUS.adoc[hyperpolymath/secret-types#N-6] at `4ed067220f13` |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`) |the canon reader refuses the receipt: unexpected clause (identity) in the receipt +|https://github.com/hyperpolymath/secret-types/blob/4ed067220f1357b37f7d54c5ae0690ff35b292bd/PROOF-STATUS.adoc[hyperpolymath/secret-types#N-7] at `4ed067220f13`; the receipt describes `292d566a81a9` |theorem |`PWG-1` |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`) |— -|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/4ed067220f1357b37f7d54c5ae0690ff35b292bd/PROOF-STATUS.adoc[hyperpolymath/secret-types#N-8] at `4ed067220f13`; the receipt describes `292d566a81a9` |theorem |`PWG-1` |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`) |— -|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/hyperpolymath/secret-types/blob/4ed067220f1357b37f7d54c5ae0690ff35b292bd/PROOF-STATUS.adoc[hyperpolymath/secret-types#N-9] at `4ed067220f13`; the receipt describes `292d566a81a9` |theorem |`PWG-1` |If an observer sees finishing versus not finishing, termination-sensitive noninterference is false for the current typing rules (`SecretTypes.Noninterference.OutcomeVisibility`: `termination-sensitive-fails`) |— |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/ROADMAP.adoc b/docs/status/ROADMAP.adoc index ab5ec02..39b3fda 100644 --- a/docs/status/ROADMAP.adoc +++ b/docs/status/ROADMAP.adoc @@ -232,9 +232,13 @@ One pull request that changes census rows is open at a time (atlas README, and catalogues a `PWG-1` only when the git checks hold. Until the next change, the registry shows THY-1 as `ungraded`, because its claim pin names the old receipt; the theory ledger records this. +** The same change pins the nine secret-types claims at its main `4ed0672` + (re-anchoring plan WO 5.1). Its receipt names `292d566`, with the echo + `7dfeab2` to `292d566` for the squash merge of its pull request 40. The + reader derives `PWG-1` for N-1, N-2, N-3, N-7, N-8 and N-9, and the + registry's git checks hold, so the registry catalogues six `PWG-1`. ** Next change: the claim pins of THY-1 and APP-1 to APP-4 (applied shelf, a - new `shelf` field), and of secret-types at the commit that holds its - manifest receipt (re-anchoring plan WO 5.1). + new `shelf` field). [[stages]] == Stages From 851e6c9c6803543b3b453bd6513ab41a68a1a0b9 Mon Sep 17 00:00:00 2001 From: Claude Date: Sat, 14 Nov 2026 09:13:19 +0000 Subject: [PATCH 5/7] registry: check each row's own receipt pin; fail a git check that cannot run; remove its workspace Answers the CodeRabbit review of 30841ed: - the receipt key now includes the pinned sha256, so a second row with a wrong digest for the same receipt fails instead of hiding behind the first; - a git or bash that cannot be found or launched gives a failed git check (the registry then catalogues PWG-2ii with the reason, ADR 0004) instead of stopping the derivation; - the checker's workspace of clones is removed after the derivation, on success and on failure. Tests cover the first two. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_0136P7Zo9dheFQzYYWV49hAk --- scripts/registry/claims-registry.mjs | 30 ++++++++++++++++++++----- tests/registry/claims-registry.test.mjs | 19 +++++++++++++++- 2 files changed, 43 insertions(+), 6 deletions(-) diff --git a/scripts/registry/claims-registry.mjs b/scripts/registry/claims-registry.mjs index 21520e6..54aea2a 100644 --- a/scripts/registry/claims-registry.mjs +++ b/scripts/registry/claims-registry.mjs @@ -22,7 +22,7 @@ // 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, mkdtemp} from 'node:fs/promises'; +import {readFile, writeFile, mkdir, mkdtemp, rm} from 'node:fs/promises'; import {existsSync} from 'node:fs'; import {spawnSync} from 'node:child_process'; import {tmpdir} from 'node:os'; @@ -187,7 +187,16 @@ export function findTool(name, env = process.env) { throw new Error(`${name} not found in an absolute directory of PATH`); } -const run = (cmd, args) => spawnSync(findTool(cmd), args, {encoding: 'utf8'}); +// A program that cannot be found or launched gives a failed result (status null), +// so the git check reports it instead of stopping the derivation. +const run = (cmd, args) => { + try { + const r = spawnSync(findTool(cmd), args, {encoding: 'utf8'}); + return r.error ? {status: null, stdout: '', stderr: String(r.error.message)} : r; + } catch (e) { + return {status: null, stdout: '', stderr: e.message}; + } +}; // The path of the pinned checker, after the digest checks of both pinned // scripts in the standards checkout. @@ -224,7 +233,7 @@ export async function gitChecker(standardsDir = process.env.MATHESIS_STANDARDS) } return clones.get(repo); }; - return async (row, text) => { + const check = async (row, text) => { const c = clone(row.repo); if (!c.dir) return {ok: false, reason: c.reason}; const file = path.join(await mkdtemp(path.join(work, 'r-')), path.basename(row.receipt.path)); @@ -234,6 +243,9 @@ export async function gitChecker(standardsDir = process.env.MATHESIS_STANDARDS) const why = `${r.stdout}${r.stderr}`.trim().split('\n').filter(l => !l.startsWith('ok ')).slice(-2).join('; '); return {ok: false, reason: `check-proof-receipt.sh exit ${r.status}: ${why}`}; }; + // The clones and receipt copies live in `work` only; remove it when done. + check.cleanup = () => rm(work, {recursive: true, force: true}); + return check; } // The reader's record of one receipt text: {record, text} or {refusal}. @@ -246,7 +258,9 @@ function readReceipt(text, row, readProofReceipt) { } } -const receiptKey = row => (row.receipt === null ? null : `${row.repo}@${row.source_commit}/${row.receipt.path}`); +// The pinned digest is part of the key, so each row is checked against its own pin. +const receiptKey = row => + row.receipt === null ? null : `${row.repo}@${row.source_commit}/${row.receipt.path}#${row.receipt.sha256}`; // Derive every row, reading each distinct receipt once. A receipt that the // reader refuses gives `ungraded` with the reader's reason; a receipt that @@ -330,7 +344,13 @@ async function main() { const rows = validate(await readJsonl(claimsFile), inventory); const bridges = validateBridges(await readJsonl(bridgesFile), inventory); const admissions = validateAdmissions(await readJsonl(admissionsFile), rows, inventory); - const derived = await deriveAll(rows, receiptsDir, await loadReader(), receiptsDir ? null : await gitChecker()); + const gitCheck = receiptsDir ? null : await gitChecker(); + let derived; + try { + derived = await deriveAll(rows, receiptsDir, await loadReader(), gitCheck); + } finally { + await gitCheck?.cleanup(); + } const ledger = validateLedger(await readJsonl(ledgerFile)); const current = snapshot(rows, admissions, new Map(derived.map(d => [d.row.id, d.pwg]))); if (cmd === 'ledger') { diff --git a/tests/registry/claims-registry.test.mjs b/tests/registry/claims-registry.test.mjs index 69e09fb..105d207 100644 --- a/tests/registry/claims-registry.test.mjs +++ b/tests/registry/claims-registry.test.mjs @@ -9,7 +9,7 @@ import {readFileSync, mkdtempSync, mkdirSync, writeFileSync, copyFileSync} from import {createHash} from 'node:crypto'; import {tmpdir} from 'node:os'; import path from 'node:path'; -import {validate, loadReader, derive, deriveAll, withGitCheck, findTool, render, READER} from '../../scripts/registry/claims-registry.mjs'; +import {validate, loadReader, derive, deriveAll, withGitCheck, findTool, gitChecker, render, READER} from '../../scripts/registry/claims-registry.mjs'; import {parseJsonl} from '../../scripts/atlas/census-atlas.mjs'; const rows = parseJsonl(readFileSync(new URL('../../docs/atlas/claims/claims.jsonl', import.meta.url), 'utf8')); @@ -115,6 +115,9 @@ test('deriveAll reads each receipt once, and refuses a receipt that does not mat 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/); + // Each row is checked against its own pin: a second row with a wrong digest for + // the same receipt is not hidden behind the first. + await expect(deriveAll([good, {...good, id: 'o/r#T-1b', 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', () => { @@ -160,3 +163,17 @@ test('git and bash run only from an absolute directory of PATH', () => { expect(path.isAbsolute(findTool('bash'))).toBe(true); expect(() => findTool('bash', {PATH: 'relative/bin'})).toThrow(/not found in an absolute directory/); }); + +test('a git check that cannot run gives a failed result, not a crash', async () => { + const check = await gitChecker(); + const saved = process.env.PATH; + process.env.PATH = ''; + try { + const r = await check({...theorem, receipt: {path: 'r_praxis.deed', sha256: 'a'.repeat(64)}}, fixture()); + expect(r.ok).toBe(false); + expect(r.reason).toMatch(/could not clone o\/r: git not found in an absolute directory of PATH/); + } finally { + process.env.PATH = saved; + await check.cleanup(); + } +}); From 6c63f56889742cc66d722b877d681759c38c7b20 Mon Sep 17 00:00:00 2001 From: Claude Date: Sat, 14 Nov 2026 10:13:17 +0000 Subject: [PATCH 6/7] ci(hypatia): pin the scanner at 6693f9a, which has the js_exec_sync fix The Hypatia Security Scan pinned hyperpolymath/hypatia at d73f76b, whose js_exec_sync rule flagged any import of node:child_process. hypatia#1083 (6693f9a) flags only calls that a shell parses. This moves the pin and its cache key to 6693f9a, matching the same bump in the RSR template (owner ruling 2026-11-14: fix at source, template and mathesis). Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_0136P7Zo9dheFQzYYWV49hAk --- .github/workflows/hypatia-scan.yml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/.github/workflows/hypatia-scan.yml b/.github/workflows/hypatia-scan.yml index a3ff99d..a3ae611 100644 --- a/.github/workflows/hypatia-scan.yml +++ b/.github/workflows/hypatia-scan.yml @@ -31,7 +31,7 @@ jobs: contents: read security-events: write env: - HYPATIA_SHA: 'd73f76b5cb7a35e1aa1024c916aee7cb4f9b141e' + HYPATIA_SHA: '6693f9aed8e4383f78a3d01b600b32663bf7a45c' steps: - name: Checkout repository uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1 @@ -53,7 +53,7 @@ jobs: ~/hypatia ~/.hex ~/.mix - key: hypatia-sarif-${{ runner.os }}-otp28-elx1194-d73f76b5cb7a35e1aa1024c916aee7cb4f9b141e + key: hypatia-sarif-${{ runner.os }}-otp28-elx1194-6693f9aed8e4383f78a3d01b600b32663bf7a45c - name: Build pinned Hypatia scanner run: | From 3e763f4ad7bdee9384e150f65442fa7c4fcb43da Mon Sep 17 00:00:00 2001 From: Claude Date: Sat, 14 Nov 2026 10:20:55 +0000 Subject: [PATCH 7/7] fix(registry): check the canon reader digest before the checker runs it The pinned check-proof-receipt.sh runs deed_lint.js from the same standards checkout. The `receipt` home gate called checkerScript() but never loadReader(), so a changed reader could supply its result. checkerScript() now checks READER.sha256 as well as the two script digests, so the home gate and the registry git checks both run only beside the pinned reader. A new test changes the reader in a copy of the checkout and expects a refusal. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_0136P7Zo9dheFQzYYWV49hAk --- scripts/registry/claims-registry.mjs | 6 ++++-- tests/registry/claims-registry.test.mjs | 13 ++++++++++++- 2 files changed, 16 insertions(+), 3 deletions(-) diff --git a/scripts/registry/claims-registry.mjs b/scripts/registry/claims-registry.mjs index 54aea2a..78dfd32 100644 --- a/scripts/registry/claims-registry.mjs +++ b/scripts/registry/claims-registry.mjs @@ -199,14 +199,16 @@ const run = (cmd, args) => { }; // The path of the pinned checker, after the digest checks of both pinned -// scripts in the standards checkout. +// scripts and of the canon reader that the checker runs, in the standards +// checkout. The `receipt` home gate runs the checker without loadReader(). export async function checkerScript(standardsDir = process.env.MATHESIS_STANDARDS) { const pinned = async (rel, sha) => { const file = path.resolve(standardsDir, rel); const digest = createHash('sha256').update(await readFile(file)).digest('hex'); - if (digest !== sha) throw new Error(`${file} is not the pinned script (sha256 ${digest}, pinned ${sha} at ${READER.commit})`); + if (digest !== sha) throw new Error(`${file} is not the pinned file (sha256 ${digest}, pinned ${sha} at ${READER.commit})`); return file; }; + await pinned(READER.path, READER.sha256); await pinned(CHECKER.digest, CHECKER.digestSha256); return pinned(CHECKER.path, CHECKER.sha256); } diff --git a/tests/registry/claims-registry.test.mjs b/tests/registry/claims-registry.test.mjs index 105d207..27b12b6 100644 --- a/tests/registry/claims-registry.test.mjs +++ b/tests/registry/claims-registry.test.mjs @@ -9,7 +9,7 @@ import {readFileSync, mkdtempSync, mkdirSync, writeFileSync, copyFileSync} from import {createHash} from 'node:crypto'; import {tmpdir} from 'node:os'; import path from 'node:path'; -import {validate, loadReader, derive, deriveAll, withGitCheck, findTool, gitChecker, render, READER} from '../../scripts/registry/claims-registry.mjs'; +import {validate, loadReader, derive, deriveAll, withGitCheck, findTool, gitChecker, checkerScript, render, READER, CHECKER} from '../../scripts/registry/claims-registry.mjs'; import {parseJsonl} from '../../scripts/atlas/census-atlas.mjs'; const rows = parseJsonl(readFileSync(new URL('../../docs/atlas/claims/claims.jsonl', import.meta.url), 'utf8')); @@ -177,3 +177,14 @@ test('a git check that cannot run gives a failed result, not a crash', async () await check.cleanup(); } }); + +test('the checker runs only beside the pinned canon reader', async () => { + const std = mkdtempSync(path.join(tmpdir(), 'mathesis-std-')); + for (const rel of [READER.path, CHECKER.path, CHECKER.digest]) { + mkdirSync(path.dirname(path.join(std, rel)), {recursive: true}); + copyFileSync(path.join(process.env.MATHESIS_STANDARDS, rel), path.join(std, rel)); + } + expect(await checkerScript(std)).toBe(path.resolve(std, CHECKER.path)); + writeFileSync(path.join(std, READER.path), '// changed\n', {flag: 'a'}); + await expect(checkerScript(std)).rejects.toThrow(/is not the pinned file/); +});