diff --git a/.machine_readable/coaptation/receipts/latest.toml b/.machine_readable/coaptation/receipts/latest.toml index 6e4e715..a5441ab 100644 --- a/.machine_readable/coaptation/receipts/latest.toml +++ b/.machine_readable/coaptation/receipts/latest.toml @@ -10,9 +10,9 @@ band = "amber" proposed-action = "advisory — soft drift within bands (posture/intend). Open an advisory issue; no re-anchor." [coverage] -clauses-total = 57 +clauses-total = 58 descriptile-witnessed = 2 -probe-deferred-to-hunt = 32 +probe-deferred-to-hunt = 33 must-trust-unmeasured-gaps = 0 note = "Yard sees descriptile evidence only; probe-deferred obligations need a Hunt-tier run for a full hard-gate." @@ -21,7 +21,7 @@ grade = "boolean_gate / boolean_gate_provenance" witnessed = 1 refuted = 0 unmeasured-gaps = 0 -probe-deferred = 32 +probe-deferred = 33 gate = "pass" [reading.adjust] @@ -71,6 +71,7 @@ must.no-hand-typed-grade = "probe-deferred" must.receipts-stay-home = "probe-deferred" must.home-theorem-has-receipt = "probe-deferred" must.rows-have-provenance = "probe-deferred" +must.theory-ledger-current = "probe-deferred" trust.no-secrets-committed = "probe-deferred" trust.no-private-keys = "probe-deferred" trust.no-tokens-in-source = "probe-deferred" @@ -103,5 +104,5 @@ bust.sync-drift-between-repos = "latent" bust.contractile-parse-error = "latent" [provenance] -contractiles = "intend@89c97164fbff must@b2888ac670fb trust@484d6509ce86 adjust@f7e9bafc614e dust@bdb7dea20424 bust@4de1f1b3bc91" +contractiles = "intend@89c97164fbff must@1c538d416df3 trust@484d6509ce86 adjust@f7e9bafc614e dust@bdb7dea20424 bust@4de1f1b3bc91" descriptiles = "deed@7182c2cc6635 anchor@bba9793279e0" diff --git a/.machine_readable/contractiles/must/must.k9.ncl b/.machine_readable/contractiles/must/must.k9.ncl index b57b973..d021cc4 100644 --- a/.machine_readable/contractiles/must/must.k9.ncl +++ b/.machine_readable/contractiles/must/must.k9.ncl @@ -285,6 +285,14 @@ let base = import "../_base.ncl" in severity = 'critical, notes = "Re-anchoring plan WO 2.1. A row without either field makes jq fail, and the probe fails closed.", }, + { + id = "theory-ledger-current", + section = "Mathesis Invariants", + description = "The theory ledger records each home theorem's current admission and receipt pin, and only `just theory-ledger` writes it", + probe = "bun scripts/registry/theory-ledger.mjs verify >/dev/null", + severity = 'critical, + notes = "Owner ruling 2026-11-11. The probe is offline. just registry-check (part of just check) also checks the derived grade, and that the ledger on main is a prefix of this one (append-only).", + }, ], }, diff --git a/Justfile b/Justfile index 3fca090..e41d84f 100644 --- a/Justfile +++ b/Justfile @@ -768,4 +768,11 @@ registry: # Fail if the committed registry view is stale (needs MATHESIS_STANDARDS, as above) registry-check: bun scripts/registry/claims-registry.mjs check + bun scripts/registry/theory-ledger.mjs verify bun test tests/registry/ + +# 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" +theory-ledger note="": + bun scripts/registry/claims-registry.mjs ledger {{ if note == "" { "" } else { "--note " + quote(note) } }} diff --git a/docs/status/ROADMAP.adoc b/docs/status/ROADMAP.adoc index 4f56276..0159fa8 100644 --- a/docs/status/ROADMAP.adoc +++ b/docs/status/ROADMAP.adoc @@ -153,9 +153,14 @@ One pull request that changes census rows is open at a time (atlas README, generates `docs/theory/generated/index.adoc`. All template example proofs and the six template stubs under `docs/theory/` are removed (owner rulings 2026-11-11). -* Next, by owner ruling: an append-only ledger of the theory work, written - only by a `just theory-ledger` recipe and checked in CI, in its own pull - request. +* WO 4.1 merged (pull request 79). +* The theory ledger (owner ruling 2026-11-11): `docs/theory/ledger.jsonl`, + append-only, written only by `just theory-ledger`. `just registry-check` + fails when the ledger is behind or a past entry changed; the `must` clause + `theory-ledger-current` states the invariant (approved by the owner). +* The IANA registration drafts of DEED, K9 and k9-coordination are + corrected in a separate session on the standards repository; filing is + the owner's act. * Finding: the `intend` contract still marks stage 3 `in_progress` and stage 4 `declared`; a contract edit needs owner review. @@ -194,7 +199,7 @@ anchors `c81cb84` |The three shelves: the theory admission rule and the token-lattice theorems, the applied shelf tied to the evidence spine, the published atlas (needs a ruling) -|In progress: WO 4.1 in review +|In progress: WO 4.1 merged; the theory ledger in review |5 |Scale: receipts in the home repositories, the bridge lock pilot, a diff --git a/docs/theory/README.adoc b/docs/theory/README.adoc index 287788b..7755cec 100644 --- a/docs/theory/README.adoc +++ b/docs/theory/README.adoc @@ -39,6 +39,11 @@ holds no grade. |The theorem index, generated by `scripts/registry/claims-registry.mjs` from the admission records, the claim pins and the receipt. Never edit it by hand. +|`ledger.jsonl` +|The story of the theory work: one entry for each admission, withdrawal, or +change of receipt pin, admission or derived grade, with an optional note. +Append-only, and written only by `just theory-ledger`. + |`../../verification/proofs/` |The Agda, Rocq and Lean sources. @@ -49,7 +54,8 @@ the admission records, the claim pins and the receipt. Never edit it by hand. `just registry-check` (part of `just check`) fails when the index is stale, when a home theorem has no admission record, or when an admission names no dependant, a non-public dependant repository, or a theorem with no claim -pin. +pin. It also fails when the ledger is behind the current state, or when the +ledger on `main` is not a prefix of this one (an altered or lost past entry). == Admitting a theorem @@ -57,7 +63,9 @@ pin. . Add each leg to the receipt, from observed checker runs. . Pin the claim in `docs/atlas/claims/claims.jsonl`. . Add its admission record to `admissions.jsonl`. -. Run `bun scripts/registry/claims-registry.mjs build`, then `just check`. +. Run `bun scripts/registry/claims-registry.mjs build`. +. Run `just theory-ledger "a note that tells what happened"`, then + `just check`. The token-lattice theorems are the next candidates (ruling D-10). Their statements are in `docs/proposals/mathesis-research-programme.adoc`. diff --git a/docs/theory/ledger.jsonl b/docs/theory/ledger.jsonl new file mode 100644 index 0000000..93f31e3 --- /dev/null +++ b/docs/theory/ledger.jsonl @@ -0,0 +1 @@ +{"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} diff --git a/mathesis_chora.deed b/mathesis_chora.deed index b91c1a2..147b5ba 100644 --- a/mathesis_chora.deed +++ b/mathesis_chora.deed @@ -1021,7 +1021,8 @@ "verification/proofs/agda/FeatureReachability.agda" "verification/proofs/coq/FeatureReachability.v" "verification/proofs/lean4/FeatureReachability.lean" - "EXPLAINME.adoc") + "EXPLAINME.adoc" + "docs/theory/admissions.jsonl" "docs/theory/ledger.jsonl" "docs/theory/generated/") :removed ("archetypes/" "build/docs-seed/" "build/templates/" "rsr-template-repo_chora.deed" "src/interface/" "benches/" "build/container/Containerfile" "tests/ffi_strings_test.sh" diff --git a/scripts/registry/claims-registry.mjs b/scripts/registry/claims-registry.mjs index c5d76f7..c3801a7 100644 --- a/scripts/registry/claims-registry.mjs +++ b/scripts/registry/claims-registry.mjs @@ -29,6 +29,7 @@ import path from 'node:path'; import {readJsonl} from '../atlas/census-atlas.mjs'; import {validateBridges, renderBridges} from './bridges.mjs'; import {validateAdmissions, renderTheoryIndex} from './theory.mjs'; +import {validateLedger, snapshot, pending, checkAppendOnly, jcs} from './theory-ledger.mjs'; const root = path.resolve(path.dirname(fileURLToPath(import.meta.url)), '../..'); const claimsFile = path.join(root, 'docs/atlas/claims/claims.jsonl'); @@ -38,6 +39,19 @@ const bridgesFile = path.join(root, 'docs/atlas/claims/bridges.jsonl'); const bridgesView = path.join(root, 'docs/atlas/generated/bridges.adoc'); const admissionsFile = path.join(root, 'docs/theory/admissions.jsonl'); const theoryView = path.join(root, 'docs/theory/generated/index.adoc'); +const ledgerFile = path.join(root, 'docs/theory/ledger.jsonl'); + +// The theory ledger as it stands on main, for the append-only check, read +// over HTTPS like the receipts (no subprocess, and the local clone is left +// as it is). A 404 means main has no ledger yet, so every entry is new; any +// other failure stops the check: an unchecked ledger is not a passing one. +const LEDGER_ON_MAIN = 'https://raw.githubusercontent.com/hyperpolymath/mathesis/main/docs/theory/ledger.jsonl'; +async function ledgerOnMain() { + const res = await fetch(LEDGER_ON_MAIN); + if (res.status === 404) return ''; + if (!res.ok) throw new Error(`could not fetch ${LEDGER_ON_MAIN}: HTTP ${res.status}`); + return res.text(); +} const KINDS = new Set(['theorem', 'demonstration', 'assumption']); const PWG = new Set(['PWG-1', 'PWG-2ii', 'PWG-2i', 'PWG-3', 'ungraded']); @@ -216,8 +230,8 @@ export function render(derived) { async function main() { const [cmd, ...args] = process.argv.slice(2); - if (cmd !== 'build' && cmd !== 'check') { - console.error('usage: claims-registry.mjs build|check [--receipts-dir DIR]'); + if (!['build', 'check', 'ledger'].includes(cmd)) { + console.error('usage: claims-registry.mjs build|check|ledger [--receipts-dir DIR] [--note TEXT]'); process.exit(2); } const i = args.indexOf('--receipts-dir'); @@ -227,6 +241,16 @@ async function main() { const bridges = validateBridges(await readJsonl(bridgesFile), inventory); const admissions = validateAdmissions(await readJsonl(admissionsFile), rows, inventory); const derived = await deriveAll(rows, receiptsDir, await loadReader()); + const ledger = validateLedger(await readJsonl(ledgerFile)); + const current = snapshot(rows, admissions, new Map(derived.map(d => [d.row.id, d.pwg]))); + if (cmd === 'ledger') { + const n = args.indexOf('--note'); + const note = n >= 0 ? args[n + 1] : undefined; + const add = pending(ledger, current, new Date().toISOString().slice(0, 10), note); + if (add.length) await writeFile(ledgerFile, [...ledger, ...add].map(e => jcs(e) + '\n').join('')); + console.log(`theory ledger: ${add.length} new entries, ${ledger.length + add.length} in all`); + return; + } const views = [[viewFile, render(derived)], [bridgesView, renderBridges(bridges)], [theoryView, renderTheoryIndex(derived, admissions)]]; if (cmd === 'build') { await Promise.all(views.map(([file]) => mkdir(path.dirname(file), {recursive: true}))); @@ -236,7 +260,10 @@ async function main() { const committed = await Promise.all(views.map(([file]) => readFile(file, 'utf8').catch(() => ''))); const stale = views.filter(([, body], i) => committed[i] !== body).map(([file]) => path.relative(root, file)); if (stale.length) throw new Error(`${stale.join(', ')} stale; run: bun scripts/registry/claims-registry.mjs build`); - console.log(`PASS: claims registry derived from ${new Set(rows.map(r => r.repo + '@' + r.source_commit)).size} pinned source(s); views match (${rows.length} claims, ${bridges.length} bridges, ${admissions.length} admissions)`); + const due = pending(ledger, current, '0000-00-00'); + if (due.length) throw new Error(`docs/theory/ledger.jsonl is behind by ${due.length} entries; run: just theory-ledger`); + checkAppendOnly(await ledgerOnMain(), await readFile(ledgerFile, 'utf8')); + console.log(`PASS: claims registry derived from ${new Set(rows.map(r => r.repo + '@' + r.source_commit)).size} pinned source(s); views match (${rows.length} claims, ${bridges.length} bridges, ${admissions.length} admissions); the theory ledger is current and append-only (${ledger.length} entries)`); } } diff --git a/scripts/registry/theory-ledger.mjs b/scripts/registry/theory-ledger.mjs new file mode 100644 index 0000000..1982188 --- /dev/null +++ b/scripts/registry/theory-ledger.mjs @@ -0,0 +1,186 @@ +// SPDX-License-Identifier: MPL-2.0 +// SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell +// +// The ledger of the theory shelf (owner ruling 2026-11-11, after WO 4.1). +// +// docs/theory/ledger.jsonl tells the story of the theory work: one entry for +// each change to a home theorem's admission, receipt pin or derived grade. +// It is append-only and has one writer: `just theory-ledger`, which folds the +// ledger into the current state of each theorem, compares it with the +// admissions, the claim pins and the derived grades, and appends one entry for +// each difference. The working documents state only the present; the ledger +// keeps the past. A ledger entry holds a grade that the canon reader derived, +// copied at the time of the entry; it never asserts one. +// +// `node theory-ledger.mjs verify` is the offline part of the check (the `must` +// clause theory-ledger-current): the ledger is well formed, and its folded +// state matches each admission and claim pin. The grade needs the canon reader +// and network access, so `just registry-check` checks it. + +import {createHash} from 'node:crypto'; +import {fileURLToPath} from 'node:url'; +import path from 'node:path'; +import {readJsonl} from '../atlas/census-atlas.mjs'; +import {HOME} from './theory.mjs'; + +const EVENTS = new Set(['admitted', 'changed', 'withdrawn']); +const FIELDS = new Set(['seq', 'date', 'event', 'id', 'pwg', 'receipt', 'admission_sha256', 'changes', 'note']); +const CHANGE_KEYS = new Set(['pwg', 'receipt', 'admission']); + +const need = (ok, message) => { + if (!ok) throw new Error(message); +}; + +// UTF-16 code-unit order, the key order of RFC 8785. +function compareUtf16(a, b) { + if (a < b) return -1; + if (a > b) return 1; + return 0; +} + +// RFC 8785 serialisation of parsed JSON. +export function jcs(v) { + if (Array.isArray(v)) return '[' + v.map(jcs).join(',') + ']'; + if (v !== null && typeof v === 'object') { + return '{' + Object.keys(v).sort(compareUtf16).map(k => JSON.stringify(k) + ':' + jcs(v[k])).join(',') + '}'; + } + return JSON.stringify(v); +} + +export const sha256 = s => createHash('sha256').update(s).digest('hex'); + +// The state of one home theorem that the ledger tracks. +const stateOf = (row, admission, pwg) => ({ + pwg, + receipt: row.receipt ? {path: row.receipt.path, sha256: row.receipt.sha256, commit: row.source_commit} : null, + admission_sha256: sha256(jcs(admission)), +}); + +// The current state of each home theorem, from the claim pins, the admissions +// and the derived grade of each pin (a Map id -> pwg). +export function snapshot(rows, admissions, grades) { + const byId = new Map(admissions.map(a => [a.id, a])); + const out = new Map(); + for (const row of rows) { + if (row.repo !== HOME || row.kind !== 'theorem' || !byId.has(row.id)) continue; + need(grades.has(row.id), `No derived grade for ${row.id}`); + out.set(row.id, stateOf(row, byId.get(row.id), grades.get(row.id))); + } + return out; +} + +// A receipt pin: exactly a path, a SHA-256 of the receipt and a git commit. +const isReceipt = r => + r !== null && typeof r === 'object' && !Array.isArray(r) && + jcs(Object.keys(r).sort(compareUtf16)) === '["commit","path","sha256"]' && + typeof r.path === 'string' && r.path !== '' && + /^[0-9a-f]{64}$/.test(r.sha256) && /^[0-9a-f]{40}$/.test(r.commit); + +// Throw unless the ledger is well formed: closed fields, seq 1..n in order, +// a date on each entry, and events that follow the life of each theorem. +export function validateLedger(ledger) { + need(Array.isArray(ledger), 'docs/theory/ledger.jsonl must hold one entry on each line'); + const live = new Set(); + ledger.forEach((e, i) => { + const where = `ledger entry ${i + 1}`; + for (const k of Object.keys(e)) need(FIELDS.has(k), `Unknown ledger field ${k}: ${where}`); + need(e.seq === i + 1, `seq must count 1, 2, 3 ... without a gap: ${where}`); + need(typeof e.date === 'string' && /^\d{4}-\d{2}-\d{2}$/.test(e.date), `date is a date: ${where}`); + need(EVENTS.has(e.event), `Unknown event ${e.event}: ${where}`); + need(typeof e.id === 'string' && e.id.startsWith(HOME + '#'), `id names a home theorem: ${where}`); + need(e.note === undefined || (typeof e.note === 'string' && e.note.trim() !== ''), `note is text: ${where}`); + if (e.event === 'withdrawn') { + need(live.has(e.id), `A withdrawn theorem was not admitted: ${where}`); + live.delete(e.id); + return; + } + need(typeof e.pwg === 'string' && /^(PWG-1|PWG-2ii|PWG-2i|PWG-3|ungraded)$/.test(e.pwg), `pwg is a derived grade: ${where}`); + need(e.receipt === null || isReceipt(e.receipt), `receipt is null or {path, sha256, commit}: ${where}`); + need(typeof e.admission_sha256 === 'string' && /^[0-9a-f]{64}$/.test(e.admission_sha256), `admission_sha256 is a SHA-256: ${where}`); + if (e.event === 'admitted') { + need(!live.has(e.id), `Admitted twice without a withdrawal: ${where}`); + live.add(e.id); + } else { + need(live.has(e.id), `A change to a theorem that is not admitted: ${where}`); + need(Array.isArray(e.changes) && e.changes.length > 0 && e.changes.every(c => CHANGE_KEYS.has(c)), `changes lists pwg, receipt or admission: ${where}`); + } + }); + return ledger; +} + +// Fold the ledger into the last recorded state of each live theorem. +export function fold(ledger) { + const out = new Map(); + for (const e of ledger) { + if (e.event === 'withdrawn') out.delete(e.id); + else out.set(e.id, {pwg: e.pwg, receipt: e.receipt, admission_sha256: e.admission_sha256}); + } + return out; +} + +// The entry that takes one theorem from its recorded state `was` to `now` +// (either may be undefined), or null when nothing changed. +function entryFor(id, was, now) { + if (!was) return {event: 'admitted', id, ...now}; + if (!now) return {event: 'withdrawn', id}; + const changes = []; + if (was.pwg !== now.pwg) changes.push('pwg'); + if (jcs(was.receipt) !== jcs(now.receipt)) changes.push('receipt'); + if (was.admission_sha256 !== now.admission_sha256) changes.push('admission'); + return changes.length ? {event: 'changed', id, ...now, changes} : null; +} + +// The entries that bring the ledger up to `current`, in id order. +export function pending(ledger, current, date, note) { + const before = fold(ledger); + const ids = [...new Set([...before.keys(), ...current.keys()])].sort(compareUtf16); + const out = []; + for (const id of ids) { + const entry = entryFor(id, before.get(id), current.get(id)); + if (entry) out.push({seq: ledger.length + out.length + 1, date, ...entry, ...(note ? {note} : {})}); + } + return out; +} + +// Throw unless `base` (the ledger on main) is a prefix of `ledger`, line for +// line: no past entry may change or disappear. +export function checkAppendOnly(baseText, text) { + const base = baseText.split('\n').filter(Boolean); + const now = text.split('\n').filter(Boolean); + need(now.length >= base.length, `The ledger lost entries: main has ${base.length}, this tree has ${now.length}`); + base.forEach((line, i) => need(now[i] === line, `Ledger entry ${i + 1} differs from main: past entries are append-only`)); +} + +// Offline check: the folded ledger matches each admission and claim pin +// (everything but the derived grade, which needs the canon reader). +export function verifyOffline(ledger, rows, admissions) { + validateLedger(ledger); + const state = fold(ledger); + const byId = new Map(admissions.map(a => [a.id, a])); + for (const row of rows.filter(r => r.repo === HOME && r.kind === 'theorem' && byId.has(r.id))) { + const s = state.get(row.id); + need(s, `The ledger does not record ${row.id}; run: just theory-ledger`); + const now = stateOf(row, byId.get(row.id), s.pwg); + need(jcs(now.receipt) === jcs(s.receipt), `The ledger's receipt for ${row.id} is stale; run: just theory-ledger`); + need(now.admission_sha256 === s.admission_sha256, `The ledger's admission for ${row.id} is stale; run: just theory-ledger`); + } + const pinned = new Set(rows.filter(r => r.repo === HOME && r.kind === 'theorem').map(r => r.id)); + for (const id of state.keys()) { + need(byId.has(id), `The ledger still holds ${id}, which has no admission; run: just theory-ledger`); + need(pinned.has(id), `The ledger still holds ${id}, which has no claim pin; run: just theory-ledger`); + } +} + +const root = path.resolve(path.dirname(fileURLToPath(import.meta.url)), '../..'); +if (process.argv[1] && path.resolve(process.argv[1]) === fileURLToPath(import.meta.url)) { + const [cmd] = process.argv.slice(2); + try { + need(cmd === 'verify', 'usage: theory-ledger.mjs verify'); + const read = p => readJsonl(path.join(root, p)); + verifyOffline(await read('docs/theory/ledger.jsonl'), await read('docs/atlas/claims/claims.jsonl'), await read('docs/theory/admissions.jsonl')); + console.log('PASS: the theory ledger matches the admissions and the claim pins'); + } catch (e) { + console.error('ERROR: ' + e.message); + process.exitCode = 1; + } +} diff --git a/tests/registry/theory-ledger.test.mjs b/tests/registry/theory-ledger.test.mjs new file mode 100644 index 0000000..e2e8d1a --- /dev/null +++ b/tests/registry/theory-ledger.test.mjs @@ -0,0 +1,76 @@ +// SPDX-License-Identifier: MPL-2.0 +// The theory ledger: appends one entry per change, is append-only, and its +// fold matches the admissions and the claim pins. +import {test, expect} from 'bun:test'; +import {readFileSync} from 'node:fs'; +import {validateLedger, snapshot, fold, pending, checkAppendOnly, verifyOffline, jcs, sha256} from '../../scripts/registry/theory-ledger.mjs'; +import {HOME} from '../../scripts/registry/theory.mjs'; +import {parseJsonl} from '../../scripts/atlas/census-atlas.mjs'; + +const read = p => readFileSync(new URL(p, import.meta.url), 'utf8'); +const rows = parseJsonl(read('../../docs/atlas/claims/claims.jsonl')); +const admissions = parseJsonl(read('../../docs/theory/admissions.jsonl')); +const ledgerText = read('../../docs/theory/ledger.jsonl'); +const ledger = parseJsonl(ledgerText); +const homeIds = rows.filter(r => r.repo === HOME && r.kind === 'theorem').map(r => r.id); +// The grades the ledger last recorded: grade currency needs the canon reader, +// so `just registry-check` checks it, not this test. +const grades = new Map([...fold(ledger)].map(([id, s]) => [id, s.pwg])); +const synthetic = new Map(homeIds.map(id => [id, 'PWG-1'])); + +test('the committed ledger is well formed and matches the admissions and pins', () => { + expect(validateLedger(ledger)).toHaveLength(ledger.length); + expect(() => verifyOffline(ledger, rows, admissions)).not.toThrow(); + expect(pending(ledger, snapshot(rows, admissions, grades), 'x')).toEqual([]); +}); + +test('the writer appends admitted, changed and withdrawn entries, and nothing when nothing changed', () => { + const now = snapshot(rows, admissions, synthetic); + const first = pending([], now, '2026-11-11'); + expect(first.map(e => e.event)).toEqual(homeIds.map(() => 'admitted')); + expect(first[0].seq).toBe(1); + expect(pending(first, now, '2026-11-12')).toEqual([]); + const downgraded = snapshot(rows, admissions, new Map(homeIds.map(id => [id, 'ungraded']))); + const changed = pending(first, downgraded, '2026-11-12', 'the receipt went stale'); + expect(changed.map(e => [e.event, e.changes, e.note])).toEqual(homeIds.map(() => ['changed', ['pwg'], 'the receipt went stale'])); + const gone = pending(first, new Map(), '2026-11-12'); + expect(gone.map(e => e.event)).toEqual(homeIds.map(() => 'withdrawn')); + expect(fold([...first, ...gone]).size).toBe(0); +}); + +test('a malformed ledger fails closed', () => { + const [e] = ledger; + const bad = (list, msg) => expect(() => validateLedger(list)).toThrow(msg); + bad([{...e, seq: 2}], /seq must count/); + bad([{...e, grade: 'PWG-1'}], /Unknown ledger field/); + bad([{...e, pwg: 'PWG-0'}], /derived grade/); + bad([{...e, date: 'today'}], /date is a date/); + bad([e, {...e, seq: 2}], /Admitted twice/); + bad([{seq: 1, date: e.date, event: 'withdrawn', id: e.id}], /was not admitted/); + bad([{...e, event: 'changed', changes: ['pwg']}], /not admitted/); + bad([{...e, id: 'o/other#X'}], /names a home theorem/); + bad([{...e, receipt: {}}], /receipt is null/); + bad([{...e, receipt: []}], /receipt is null/); + bad([{...e, receipt: {...e.receipt, sha256: 'x'}}], /receipt is null/); + bad([{...e, receipt: {...e.receipt, extra: 1}}], /receipt is null/); +}); + +test('past entries are append-only', () => { + const extra = jcs({...ledger[0], seq: ledger.length + 1, event: 'changed', changes: ['pwg']}) + '\n'; + expect(() => checkAppendOnly(ledgerText, ledgerText + extra)).not.toThrow(); + expect(() => checkAppendOnly('', ledgerText)).not.toThrow(); + const edited = ledgerText.replace(ledger[0].date, '2000-01-01'); + expect(() => checkAppendOnly(ledgerText, edited)).toThrow(/differs from main/); + expect(() => checkAppendOnly(ledgerText + extra, ledgerText)).toThrow(/lost entries/); +}); + +test('the offline check catches a stale admission, a missing theorem and a leftover one', () => { + const changedAdmission = admissions.map(a => ({...a, admitted: '2027-01-01'})); + expect(() => verifyOffline(ledger, rows, changedAdmission)).toThrow(/admission .* is stale/); + expect(() => verifyOffline([], rows, admissions)).toThrow(/does not record/); + expect(() => verifyOffline(ledger, rows, [])).toThrow(/has no admission/); + const state = fold(ledger); + for (const a of admissions) expect(sha256(jcs(a))).toBe(state.get(a.id).admission_sha256); + const unpinned = rows.filter(r => !(r.repo === HOME && r.kind === 'theorem')); + expect(() => verifyOffline(ledger, unpinned, admissions)).toThrow(/no claim pin/); +});