From 8d4128d0e609ce2e678655f71472a578331f5c0c Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 9 Nov 2026 13:32:03 +0000 Subject: [PATCH 01/11] feat(verification): canonical machine proof ledger; PROOF-STATUS table rendered from it README-EXPLAINME section 5 requires a proof ledger with one row per obligation and a closed status vocabulary. Where a machine ledger exists, it is canonical and the table is derived from it. Hypatia's PROOF-STATUS was a set of hand-written tables, and those had drifted from estate policy. What this adds: - verification/proof-ledger.jsonl: 42 rows, one I-JSON/JCS object per line. Each row records kind (engineering|theory), obligation, status, checker, file and names, axioms, bounds and trust_boundary. Theory rows also record pwg, foundation_diverse and legs (PROOF-POLICY 8.5). - scripts/proof-ledger.sh: - `check` enforces the vocabulary, the status rules and the byte profile, and checks every named identifier against the tree. The status rules are: proven carries no axioms; proven-with-postulates names its axioms; tested-only gives bounds; a PWG appears only on a theory row, needs the PROOF-POLICY 2.1 Agda invocation, and above PWG-3 needs a counted leg. - `render` emits the table and a census line (counts, never a percentage). `render --check` and `render --write` keep the PROOF-STATUS block current. - tests/proof-ledger-test.sh: 15 contracts, each planting a defect the check exists to catch. - verify-proofs: the PROOF-STATUS currency job also runs the three steps above. Corrections the receipts forced, re-run locally at c639c46: - Lean 4.30.0, lake build plus Lean.collectAxioms: 44 of the 114 theorems rest on propext, or on propext and Quot.sound. RateLimiting, BayesianUpdate, ParserTotality and the ESN preconditions are therefore proven-with-postulates, with the axioms named. The PageRank preconditions use no axioms and are proven. - TLC 2.19: KinGate is a bounded model check, so it is tested-only with its bounds. Those bounds are 444715 distinct states at depth 13. The old row's "1,778,860 distinct states" was TLC's temporal-graph total across 4 branches. - Agda 2.8.0.2 under --safe --without-K --cubical-compatible: the LogtalkMigration source digest still matches. It is proven, at PWG-3, with both recheck legs owed. - PageRank convergence and the ESN echo-state property are theory. Each is an open, ungraded row: Agda statement first, no Mathlib. - New rows record the model-to-runtime link and VCL query correctness, both open. The Coverage Map, which marked models "Full" without that evidence, is retired. - COMPLETE and PARTIAL are gone. "Grade 3" is now written PWG-3. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01CYR5bf5FBLS7cXQK72aVNM --- .github/workflows/verify-proofs.yml | 18 + .reuse/dep5 | 7 + scripts/proof-ledger.sh | 195 +++++++++ tests/proof-ledger-test.sh | 73 ++++ verification/PROOF-STATUS.adoc | 607 ++++++++++++++-------------- verification/proof-ledger.jsonl | 42 ++ 6 files changed, 630 insertions(+), 312 deletions(-) create mode 100755 scripts/proof-ledger.sh create mode 100755 tests/proof-ledger-test.sh create mode 100644 verification/proof-ledger.jsonl diff --git a/.github/workflows/verify-proofs.yml b/.github/workflows/verify-proofs.yml index 9628701a..a274e16e 100644 --- a/.github/workflows/verify-proofs.yml +++ b/.github/workflows/verify-proofs.yml @@ -17,6 +17,9 @@ on: - verification/proofs/agda/** - verification/PROOF-STATUS.adoc - scripts/check-proof-status.sh + - verification/proof-ledger.jsonl + - scripts/proof-ledger.sh + - tests/proof-ledger-test.sh - scripts/check-trusted-base.sh - docs/proof-debt.adoc - test/soundness/** @@ -42,6 +45,9 @@ on: - verification/proofs/agda/** - verification/PROOF-STATUS.adoc - scripts/check-proof-status.sh + - verification/proof-ledger.jsonl + - scripts/proof-ledger.sh + - tests/proof-ledger-test.sh - scripts/check-trusted-base.sh - docs/proof-debt.adoc - test/soundness/** @@ -426,6 +432,18 @@ jobs: - name: PROOF-STATUS.adoc agrees with the tree run: bash scripts/check-proof-status.sh + # The machine ledger is canonical (README-EXPLAINME section 5): it must + # obey its rules and the tree, and the Proof Ledger table must be its + # rendering. The contracts plant each defect the check exists to catch. + - name: Proof ledger is valid and agrees with the tree + run: bash scripts/proof-ledger.sh check + + - name: Proof Ledger table is the ledger's rendering + run: bash scripts/proof-ledger.sh render --check + + - name: Proof ledger contracts (planted defects) + run: bash tests/proof-ledger-test.sh + check-trusted-base: name: check-trusted-base runs-on: ubuntu-latest diff --git a/.reuse/dep5 b/.reuse/dep5 index 97db7052..a06444c7 100644 --- a/.reuse/dep5 +++ b/.reuse/dep5 @@ -28,3 +28,10 @@ Comment: Verbatim `gh actions-lock` output, copied byte-for-byte from the hyperpolymath/standards .github/workflows/actions.lock at b3ce78e). These are tool-owned files: never hand-edit or reformat them; replace them with a fresh copy instead. + +Files: verification/proof-ledger.jsonl +Copyright: 2026 Jonathan D.A. Jewell +License: MPL-2.0 +Comment: The machine proof ledger: one JCS object per line, so it cannot + carry an SPDX comment. Machine-readable specification data, licensed as + code. diff --git a/scripts/proof-ledger.sh b/scripts/proof-ledger.sh new file mode 100755 index 00000000..d6db08d6 --- /dev/null +++ b/scripts/proof-ledger.sh @@ -0,0 +1,195 @@ +#!/usr/bin/env bash +# SPDX-License-Identifier: MPL-2.0 +# SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) +# +# proof-ledger.sh — the machine proof ledger (verification/proof-ledger.jsonl) +# is canonical; the Proof Ledger table in verification/PROOF-STATUS.adoc is +# rendered from it (README-EXPLAINME-STANDARD section 5, rule 1). +# +# proof-ledger.sh check validate the ledger against its rules and the tree +# proof-ledger.sh render print the AsciiDoc block for PROOF-STATUS.adoc +# proof-ledger.sh render --check fail if PROOF-STATUS.adoc holds a different block +# proof-ledger.sh render --write replace the block in PROOF-STATUS.adoc +# +# One JSON object per line, I-JSON serialised as JCS (RFC 8785): keys sorted, +# no insignificant whitespace, one final LF. The ledger is held to a profile +# in which `jq -cS` output IS the JCS form: ASCII strings and no numbers. +# +# Status vocabulary (closed; PROOF-POLICY section 5 gives the upper-case +# labels): proven, proven-with-postulates, argued, tested-only, open. +# Proof Witness Grades (PROOF-POLICY section 8) are recorded for theory rows +# only: 3, 2i, 2ii, 1 or ungraded. Grades are derived from receipts; this +# check refuses a grade the row's own evidence cannot support. +# +# Exit: 0 = ledger valid (and the block current, for render --check); +# 1 = invalid or stale; 2 = usage or IO error. + +set -euo pipefail + +LEDGER="${PROOF_LEDGER:-verification/proof-ledger.jsonl}" +DOC="${PROOF_STATUS_DOC:-verification/PROOF-STATUS.adoc}" +BEGIN_MARK='// BEGIN GENERATED: scripts/proof-ledger.sh render (do not edit by hand)' +END_MARK='// END GENERATED: proof ledger' +AGDA_PROFILE='--safe --without-K --cubical-compatible' + +[ -f "$LEDGER" ] || { echo "::error::proof-ledger: $LEDGER not found"; exit 2; } + +check() { + local fails=0 n=0 line id + # Byte profile: every line is its own `jq -cS` rendering, ASCII only, and + # the file ends in exactly one LF. + if LC_ALL=C grep -nP '[^\x00-\x7F]' "$LEDGER" >/dev/null; then + echo "::error::proof-ledger: non-ASCII byte in $LEDGER (the profile is ASCII so that jq -cS is JCS)"; fails=$((fails + 1)) + fi + if [ -n "$(tail -c1 "$LEDGER")" ] || [ -z "$(tail -c2 "$LEDGER" | head -c1)" ]; then + echo "::error::proof-ledger: $LEDGER must end in exactly one LF"; fails=$((fails + 1)) + fi + while IFS= read -r line; do + n=$((n + 1)) + if ! canon=$(jq -cS . <<<"$line" 2>/dev/null) || [ "$canon" != "$line" ]; then + echo "::error::proof-ledger: line $n is not in canonical (jq -cS / JCS) form"; fails=$((fails + 1)) + fi + done < "$LEDGER" + [ "$n" -gt 0 ] || { echo "::error::proof-ledger: $LEDGER has no rows"; exit 1; } + + # Schema and status rules, one message per broken rule. + local errs + errs=$(jq -r --arg agda "$AGDA_PROFILE" ' + def need(k; t): if (has(k) and (.[k] | type) == t) then empty else "\(.id // "?"): field \(k) must be a \(t)" end; + . as $r + | ( need("id"; "string"), need("kind"; "string"), need("obligation"; "string"), + need("status"; "string"), need("checker"; "string"), need("file"; "string"), + need("names"; "array"), need("axioms"; "array"), need("bounds"; "string"), + need("trust_boundary"; "string") ), + ( [keys[] | select(IN("id","kind","obligation","status","checker","file","names","axioms","bounds","trust_boundary","pwg","foundation_diverse","legs") | not)] + | if length > 0 then "\($r.id): unknown field(s) \(join(", "))" else empty end ), + ( if (.id | test("^[a-z0-9]+(-[a-z0-9]+)*$")) then empty else "\(.id): id must be lower-case words joined by -" end ), + ( if IN(.kind; "engineering", "theory") then empty else "\(.id): kind must be engineering or theory" end ), + ( if IN(.status; "proven", "proven-with-postulates", "argued", "tested-only", "open") then empty + else "\(.id): status \(.status) is outside the closed vocabulary" end ), + ( if any(.names[], .axioms[]; type != "string") then "\(.id): names and axioms hold strings" else empty end ), + ( if (.status == "proven" or .status == "proven-with-postulates") and .checker == "-" then "\(.id): a proven row names its checker" else empty end ), + ( if .status == "proven" and (.axioms | length) > 0 then "\(.id): proven rests on no axioms; with \(.axioms | join(", ")) it is proven-with-postulates" else empty end ), + ( if .status == "proven-with-postulates" and (.axioms | length) == 0 then "\(.id): proven-with-postulates lists its axioms" else empty end ), + ( if .status != "proven" and .status != "proven-with-postulates" and (.axioms | length) > 0 then "\(.id): only a proven row carries axioms" else empty end ), + ( if .status == "tested-only" and .bounds == "" then "\(.id): tested-only gives its bounds" else empty end ), + ( if .status != "tested-only" and .bounds != "" then "\(.id): only a tested-only row has bounds" else empty end ), + ( if .status != "open" and .file == "-" then "\(.id): only an open row may have no file" else empty end ), + ( if .file != "-" and (.names | length) == 0 then "\(.id): a row with a file names what it rests on in that file" else empty end ), + ( if .kind == "theory" then + ( if IN(.pwg; "3", "2i", "2ii", "1", "ungraded") then empty else "\(.id): a theory row records pwg as 3, 2i, 2ii, 1 or ungraded" end ), + ( if (.foundation_diverse | type) == "boolean" then empty else "\(.id): a theory row records foundation_diverse" end ), + ( if (.legs | type) == "array" then empty else "\(.id): a theory row records its legs" end ), + ( if .pwg != "ungraded" and ((.status == "proven" or .status == "proven-with-postulates") | not) + then "\(.id): PWG-\(.pwg) needs an Agda proof that is proven or proven-with-postulates" else empty end ), + ( if .pwg != "ungraded" and ((.checker | contains("Agda")) and (.checker | contains($agda)) | not) + then "\(.id): PWG-\(.pwg) needs the PROOF-POLICY 2.1 invocation (\($agda)) in its checker" else empty end ), + ( if IN(.pwg; "2i", "2ii", "1") and ([.legs[]? | select(.counts == true)] | length) == 0 + then "\(.id): PWG-\(.pwg) needs a counted recheck leg" else empty end ) + else + ( if has("pwg") or has("legs") or has("foundation_diverse") then "\(.id): pwg, legs and foundation_diverse belong to theory rows" else empty end ) + end ) + ' "$LEDGER") + if [ -n "$errs" ]; then + while IFS= read -r e; do echo "::error::proof-ledger: $e"; done <<<"$errs" + fails=$((fails + $(wc -l <<<"$errs"))) + fi + local dups + dups=$(jq -r '.id' "$LEDGER" | sort | uniq -d) + if [ -n "$dups" ]; then echo "::error::proof-ledger: duplicate id(s): $dups"; fails=$((fails + 1)); fi + + # Currency against the tree: the file exists, and every name it rests on + # is in it (a renamed proof turns this red). + local file name + while IFS=$'\t' read -r id file name; do + if [ ! -f "$file" ]; then + echo "::error::proof-ledger: $id names $file, which does not exist"; fails=$((fails + 1)); continue + fi + if [ -n "$name" ] && ! grep -qwF -- "$name" "$file"; then + echo "::error::proof-ledger: $id says $file holds '$name', and it does not (renamed or removed?)"; fails=$((fails + 1)) + fi + done < <(jq -r 'select(.file != "-") | .id as $i | .file as $f | if (.names | length) == 0 then [$i, $f, ""] else (.names[] | [$i, $f, .]) end | @tsv' "$LEDGER") + + if [ "$fails" -gt 0 ]; then + echo "proof-ledger: INVALID ($fails problem(s)) in $LEDGER" + return 1 + fi + echo "proof-ledger: $n rows valid; $(census)" +} + +# A census, never a percentage (PROOF-POLICY 8.4, README-EXPLAINME 5 rule 2). +census() { + jq -rs ' + def c(s): [.[] | select(.status == s)] | length; + def g(p): [.[] | select(.kind == "theory" and .pwg == p)] | length; + "\(c("proven")) proven of \(length); \(c("proven-with-postulates")) proven-with-postulates, \(c("tested-only")) tested-only, \(c("argued")) argued, \(c("open")) open. Theory rows: \([.[] | select(.kind == "theory")] | length) (PWG-1 \(g("1")), PWG-2ii \(g("2ii")), PWG-2i \(g("2i")), PWG-3 \(g("3")), ungraded \(g("ungraded")))." + ' "$LEDGER" +} + +render() { + printf '%s\n' "$BEGIN_MARK" + printf '%s\n' '[[proof-ledger]]' + printf '%s\n' '=== Proof Ledger' + printf '\n' + # shellcheck disable=SC2016 # the backticks are AsciiDoc, printed literally + printf 'Rendered from `+%s+`, which is canonical: where this table and the\n' "$LEDGER" + printf 'ledger disagree, the ledger wins and this table is regenerated.\n' + printf '\n' + printf '*Census:* %s\n' "$(census)" + printf '\n' + printf '%s\n' '[cols="3,1,2,2,2",options="header"]' + printf '%s\n' '|===' + printf '%s\n' '|Obligation |Status |Checker (version, flags) |Where |Trust boundary' + jq -r ' + def esc: gsub("\\|"; "{vbar}"); + def code: "`+" + . + "+`"; + "\n|" + (.obligation | esc) + + "\n|" + .status + + (if (.axioms | length) > 0 then " (" + (.axioms | join(", ")) + ")" else "" end) + + (if .kind == "theory" then (if .pwg == "ungraded" then ", ungraded" else ", PWG-" + .pwg end) + + (if .foundation_diverse then " +foundation-diverse" else "" end) else "" end) + + "\n|" + (if .checker == "-" then "-" else (.checker | esc) end) + + "\n|" + (if .file == "-" then "-" else (.file | code) + (if (.names | length) > 0 then ": " + (.names | map(code) | join(", ")) else "" end) end) + + "\n|" + (.trust_boundary | esc) + + (if .bounds != "" then ". Bounds: " + (.bounds | esc) else "" end) + ' "$LEDGER" + printf '%s\n' '|===' + printf '%s\n' "$END_MARK" +} + +doc_block() { + awk -v b="$BEGIN_MARK" -v e="$END_MARK" '$0 == b { on = 1 } on { print } $0 == e { exit }' "$DOC" +} + +case "${1:-}" in + check) check ;; + render) + case "${2:-}" in + "") render ;; + --check) + [ -f "$DOC" ] || { echo "::error::proof-ledger: $DOC not found"; exit 2; } + if ! diff -u <(doc_block) <(render); then + echo "::error::proof-ledger: the Proof Ledger block in $DOC is not the rendering of $LEDGER; run scripts/proof-ledger.sh render --write" + exit 1 + fi + echo "proof-ledger: $DOC block is current" ;; + --write) + [ -f "$DOC" ] || { echo "::error::proof-ledger: $DOC not found"; exit 2; } + if ! grep -qxF -- "$BEGIN_MARK" "$DOC" || ! grep -qxF -- "$END_MARK" "$DOC"; then + echo "::error::proof-ledger: $DOC lacks the generated-block markers"; exit 2 + fi + tmp=$(mktemp); blk=$(mktemp) + render > "$blk" + # The block is read from a file, not passed with -v: awk would + # process backslash escapes in a -v value. + awk -v b="$BEGIN_MARK" -v e="$END_MARK" ' + NR == FNR { block = block $0 "\n"; next } + $0 == b { printf "%s", block; skip = 1; next } + $0 == e { skip = 0; next } + !skip { print }' "$blk" "$DOC" > "$tmp" + cat "$tmp" > "$DOC"; rm -f "$tmp" "$blk" + echo "proof-ledger: wrote the block into $DOC" ;; + *) echo "usage: $0 render [--check|--write]" >&2; exit 2 ;; + esac ;; + *) echo "usage: $0 check | render [--check|--write]" >&2; exit 2 ;; +esac diff --git a/tests/proof-ledger-test.sh b/tests/proof-ledger-test.sh new file mode 100755 index 00000000..622081f1 --- /dev/null +++ b/tests/proof-ledger-test.sh @@ -0,0 +1,73 @@ +#!/usr/bin/env bash +# SPDX-License-Identifier: MPL-2.0 +# Contracts of scripts/proof-ledger.sh: the real ledger passes, and every +# planted defect (an overclaim, a vocabulary escape, a renamed proof, a +# non-canonical line, a hand-edited table) turns it red. +set -euo pipefail + +repo_root="$(cd "$(dirname "${BASH_SOURCE[0]}")/.." && pwd)" +cd "$repo_root" +work="$(mktemp -d)" +trap 'rm -rf -- "$work"' EXIT +script="scripts/proof-ledger.sh" +pass=0; fail=0 + +expect() { #