Add read-back cards and the testimony validator

[Deicyde]

Part 5 of 8 in the split of #75. Draft; it merges after #215 (based on fix/untrusted-site-pages).

A read-back is an independent model's mathematical-English account of one blind skeleton packet, written without the article or the source. This PR adds the card that stores a read-back in the vault, the library API that files and loads cards, and the validator that decides whether testimony is safe to show. Testimony is plain text with TeX formulas between dollar signs; it is refused if it could hide or reorder what it says, or use TeX outside a flat allowlist. There is no command yet: #284 adds review record and review check on top of this API.

What it adds

• autoform_cli/readback.py, new. A card lives at blueprint/readbacks/<article_id>/<encoded-declaration>.md, schema autoform-readback/v1: frontmatter (article_id, declaration, skeleton and packet hashes, model label), the exact packet in a lean block under ## Skeleton, then the testimony in a text block under ## Read-back. Each block is fenced one backtick longer than its longest run (_fence), so nothing inside can close it.
• API: prepare_readback checks everything and builds a PreparedReadback from a declaration name, skeleton_hash, packet_hash and packet_text (which must hash to packet_hash) without touching the filesystem; publish_readback writes it. load_readbacks, readback_for, readback_keys, readback_path and Readback.validate(expected) load and judge cards; split_testimony is the one reading of where formulas are.
• Loading (load_readbacks, _card_files, _read_card_file): os.walk does not enter linked directories, each card is skipped if it is a link and opened O_NOFOLLOW|O_NONBLOCK, and at most 4 MiB plus one byte is read. A FIFO, directory, unreadable, non-UTF-8 or oversized file at a card path is an invalid card, not skipped. A card is attributed to the declaration its path names; a body that is not one skeleton block then one read-back block, or bytes not in canonical form, make it invalid. An unlistable directory stops loading with an error naming it.
• Publication (publish_readback, _open_card_directory, _publish_card): mkdir each of readbacks/ and readbacks/<id>, refusing a symlink before the next; open the directory O_DIRECTORY|O_NOFOLLOW; flock it (10 s timeout); hash the current card (_card_hash_at) and apply compare-and-swap (_card_conflict); stage .autoform-readback-*.tmp with O_EXCL, fsync, one os.replace; LOCK_UN, then close. Identical content is not rewritten, so it files even in a read-only directory. _require_publication_support refuses before anything is created where fcntl, O_DIRECTORY or O_NOFOLLOW is missing (Windows); cards still load there.
• Validator (_testimony_errors, _formula_errors): 32 KiB and 500 lines; invisible, reordering and unassigned characters, overstacked and baseless combining marks; an unclosed dollar sign ("write $"); TeX outside the flat frozenset _TESTIMONY_TEX, refused by name with a rewrite where _TEX_INSTEAD has one (no spacing, \not, \phantom, \color, macros, array or equation environments); structural rules a flat list cannot see: a bracket right after \begin{aligned}/\begin{gathered}, [ or * right after \\, & and \\ only inside an environment, balanced braces, \left/\right and \begin/\end, depth 16, 2048 UTF-16 units per formula, no TeX comments, no characters MathJax 3.2.2 cannot set, no combining marks in a formula. At least one letter or digit must show. No Markdown is read; text is shown as typed.
• skeleton.py: declaration_filename(name, *, suffix=".lean") replaces the private _packet_filename (same .lean names; refuses an empty name or unsafe suffix); evidence_hash_of is exported.
• render.py skips readbacks/, so cards never become pages, and a link to a card keeps only its text. mathjax.py's version comment names the testimony allowlist. Docs: skills/human-review/references/readback.md (the read-back guide, kept in step with the validator by a test), a card section in autoform_cli/README.md, and readback-faithfulness.md now asks the auditor for plain text with TeX between dollar signs instead of Markdown. The blueprint .gitignore template ignores staging files.

What changed in this revision

Size: +2,947/-8 in 13 files before, +2,984/-9 in 14 files now.

• Restacked on the rebuilt Treat every published page as untrusted #215, now 5e75131 (eebe543, on main ec84968, with main 400eb64 merged for Load a blueprint reached through a link that cannot be read #371). One conflict, in render.py's imports: the rebuild added shown_as_typed to the publishable import and dropped from .snapshot import BlueprintSnapshot, so from .readback import READBACKS_DIR now follows from .publishable import publishable_article, shown_as_typed.
• New: Treat every published page as untrusted #215's polish (eebe543) makes a link to a file the site leaves out keep only its text, so mkdocs build --strict finds nothing missing. The site leaves read-back cards out as well, but they were not in that set, so an article linking to its card published a dangling link and failed the strict build. _publication now puts every file under readbacks/ in left_out, and test_a_link_to_a_read_back_card_keeps_only_its_text (tests/test_site_math.py) fails without it.
• New: Load a blueprint reached through a link that cannot be read #371, which Treat every published page as untrusted #215 brings in, resolves every blueprint root with markdown.blueprint_root. load_readbacks and prepare_readback still used Path.resolve, so for a blueprint behind a link the system follows but will not let anyone read, review record (Add statement-review commands #284) failed with a permission error on Python 3.10 to 3.12 and filed the card under the link's spelling on 3.13. Both now use blueprint_root, and test_cards_file_and_load_in_a_blueprint_behind_a_link_that_cannot_be_read fails without it on 3.10 and 3.13.
• Apart from these, the old and new layer add and remove the same lines. No line of the layer uses an API the rebuild removed or changed (BlueprintSnapshot, graph.article_text, formula_fence, FormulaExtension, the tuple publishable_article returns). The readbacks/ skip in _publication is still needed: the captured files it walks, now a dict[Path, bytes] rather than a BlueprintSnapshot, still include readbacks/, so without the skip a card's .md would become a page.
• The three read-back test files collect 173 cases: f6767bb's 172 and the new link test.
• A card's skeleton: hash is the declaration's statement hash (Extract Lean skeletons one probe per root module #213), so a proof edit leaves the card valid: Readback.validate compares statement_hash, the module docstring says so, tests/skeleton_fixtures.py builds declarations with empty statement fields, and test_readbacks_are_filed_per_declaration_and_validate checks that a declaration that stops using propext keeps its card valid. This came with the previous revision's restack on the reworked Extract Lean skeletons one probe per root module #213 (since merged) and is unchanged.

Review findings it answers

• Add verified statement-review bundles #40 blocker 3, card half: a flock on the card directory in place of a lock file a crash could strand (205fc84), one rename under it so no Autoform write lands between compare and replace (e68a3c1), LOCK_UN before close so a forked child cannot keep the lock (181d83d), no-follow card loading (2b0adf6, now a link-skipping walk plus O_NOFOLLOW leaf opens). 181d83d's post-lock re-walk is dropped: a directory moved while a write waits on the lock is not detected, and the README says so.
• Add verified statement-review bundles #40 blocker 4: zero-width, bidirectional, default-ignorable and unassigned characters and stacked or baseless marks (12ff3b4); TeX outside an allowlist, now flat (b27a900); testimony with no visible letter or digit (4b6289a). b27a900's empty-argument rule is given up: an empty argument hides nothing.
• Add verified statement-review bundles #40 blocker 5: no parser runs; every check scans at most 32 KiB and 500 lines, and a test times five worst cases at the limit. The pre-parse limits of 12ff3b4, 57a3b4a and aa4b010 went with the parser.
• Item 3, card half: a quoted frontmatter field that does not open with " is refused before JSON decoding, so nested [ give an invalid card, not a RecursionError (6dc8f6a, de011d8).
• Item 5: one reading of the dollar signs, split_testimony, which the site will use; GitHub pairs nothing inside a text block. Replaces e220eab's paired-dollar rule.
• Item 8, card half: invisible characters written as escapes in the tests (87bbfa2); FIFO, directory and over-limit card guards for both loader and writer.
• "found no card" instead of found None when a named card is gone (ad2f9a8).
• Moot: item 4's testimony half (\( in code, list markers in the nesting count: no Markdown) and ba25fae (cmarkgfm on Intel Macs: dependency gone).

Until the next layers land

• No command files or checks cards: review record (builds from the packet and manifest hashes, runs no Lean) and review check arrive in Add statement-review commands #284; the site shows cards from Show statement review on the site #217.
• A malformed formula the flat list passes ($x^^y$) will show MathJax's error in its place on the site; GitHub shows its source.
• Only the staged file is flushed. The card committed to Git is the durable copy: a crash just after a write can lose it, and filing it again restores it.
• An editor's save, or a directory moved, during a write is not detected; the README says to edit cards while no write is running.

Validation

Run 39103604181 on 65d13198 passed every job: Windows inspection, subprocess, and publication hardening, real Lean (fixture toolchain), real Lean skeleton suite (fixture toolchain), real REPL (fixture toolchain), test (3.10), test (3.13).

• tests/test_readback.py: 13 tests, 35 cases: filing, path containment, a 21-row hand-edit damage table, frontmatter round trip, crash and replace behaviour.
• tests/test_readback_publication.py: 27 tests, 52 cases: lock with a blocking thread rival, forked child, compare-and-swap table, FIFO and directory under a no-block guard, links, a blueprint behind a link that cannot be read, unlistable directories, the interrupt tables, the Windows-like loader check (O_NOFOLLOW removed, link still skipped), platform refusal.
• tests/test_readback_testimony.py: 7 tests, 86 cases: dollar pairing, accept and refuse tables, writer refusal, message naming, five worst cases timed at the size limit, guide sync.
• tests/test_site_math.py: a link to a read-back card keeps only its text, and no card is published.
• tests/test_scaffold.py: the staging-file ignore; tests/skeleton_fixtures.py: shared skeleton fixture.

Stack

#	PR	Layer
1	#212	Fix roadmap loading, Lean index edge cases and undecodable JSON (merged)
2	#213	Extract Lean skeletons one probe per root module (merged)
3	#214	Run skeleton probes in parallel and isolate probe failures (merged)
4	#215	Treat every published page as untrusted
5	#216	Add read-back cards and the testimony validator
6	#284	Add statement-review commands
7	#217	Show statement review on the site
8	#219	Label statement approvals by the repository's code-owner review policy

[Deicyde]

Review at c479f49

Verdict: Needs a maintainer decision on size, then fixes and a restack. This is layer 5 of the statement-review stack (#212 -> #213 -> #214 -> #215 -> #216 -> #75 -> #217 -> #218 -> #219). It adds autoform_cli/readback.py (3,091 lines): versioned read-back cards under blueprint/readbacks/<article_id>/, a locked compare-and-swap API to prepare, publish and load them, and a 1,883-line testimony validator (readback.py:783-2665) that models MathJax 3.2.2's TeX layout and GitHub's Markdown and formula reading, with cmarkgfm as a new base dependency. Nothing a user can run changes until #75 and #217 land. The storage and publication half is well tested and the defects below are cheap; the open question is whether the GitHub-parity and MathJax-layout code is worth its size.

Fixes before merge

1. Autoform writes a card its own loader rejects when the testimony contains a carriage return (autoform_cli/readback.py:1900). _testimony_errors normalizes \r\n and \r before checking, so CRLF testimony passes prepare_readback, but _card_content writes it unnormalized (:2751). On load, _split rebuilds the body with splitlines() and "\n".join (:3026, :3074), so the canonical comparison fails (:437) and validate() reports a whole-file hash mismatch (:280). The same testimony with LF endings round-trips cleanly. Confirmed by trace and by a pure-function run against the locked dependency versions. Latent today, because Add verified statement-review bundles #75's review record normalizes newlines first (autoform_cli/__main__.py:1257 at Add verified statement-review bundles #75's head), but the library contract is what this PR ships. Fix: normalize newlines once in _validate_readback_fields, or refuse \r, and add a prepare-publish-load test with CRLF testimony.
2. Every card appears as a "prose" row on the site's Vault structure page (autoform_cli/render.py:1177-1182). render.py:428 keeps cards from becoming pages, but _is_published (:816) still captures them, and the structure page's keep() has no readbacks/ clause. Every readbacks/<article_id>/<name>--<64 hex>.md is listed and labelled "prose" (:1225), against the comment at :1223; a project with a few hundred declarations gets a few hundred hash-named rows. Confirmed by trace; still present at the top of the stack. Fix: skip READBACKS_DIR in keep() and add a render test with one card filed.
3. Move planned_readback next to its first caller (autoform_cli/readback.py:671-713). It has no test and no caller here, in Add verified statement-review bundles #75 or in Show statement review on the site #217; its first caller is in Harden card publication and review record #218. Its docstring says its output "must never be published as built here", yet it returns the same PreparedReadback type publish_readback accepts. Confirmed by grep. Fix: land it with its caller, plus a test that planned and prepared cards are byte-identical when the evidence is current.
4. Take Harden card publication and review record #218's card-side pieces when Harden card publication and review record #218 folds into this PR: durability, leftover naming and directory flushes. Drop Harden card publication and review record #218's GitHub-parity hint table and F_FULLFSYNC in the fold.

Optional

• Testimony is validated twice per write (readback.py:638, and :693 through planned_readback) and twice more on valid plus validate() after load (:254), though load_readbacks stored the result (:423). Confirmed by a call count; about 1.2 s per run in the PR's worst case. Validate once in a private helper and reuse validation_errors.
• render.py:40 imports the whole module, and so cmarkgfm, on every autoform invocation just for the string "readbacks". Put the constant in a small module.
• autoform_cli/README.md:600-676 restates limits no test checks there. Link to the guide and module constants, or extend the sync test to the README.
• Existing projects never get the .autoform-readback-*.tmp ignore rule, because autoform init skips an existing blueprint/.gitignore (autoform_cli/scaffold.py:1089-1094). Put blueprint/**/.autoform-readback-*.tmp in the root template, or say "new projects" in the README.
• Plausible, from reading: with Git for Windows' default core.autocrlf=true, every card would load as invalid (tests/test_readback.py:310 makes a rewritten card invalid). A scaffolded .gitattributes line blueprint/readbacks/** -text removes it.

Landing

• The stack sits on 8575a15. Against current main this head conflicts in 14 files, most inherited from Fix roadmap loading, Lean index edge cases and undecodable JSON #212-Treat every published page as untrusted #215; this PR's own conflicts are in autoform_cli/README.md, markdown.py, render.py and skeleton.py.
• Hard dependency on Treat every published page as untrusted #215: the validator imports FormulaExtension, displayed_formula, html_names and entity_name, none of which is on main.
• Merge order: after Fix roadmap loading, Lean index edge cases and undecodable JSON #212-Treat every published page as untrusted #215 are restacked onto main (and after Scale roadmap inventories and the full DAG explorer #90), before Add verified statement-review bundles #75, trimmed and with Harden card publication and review record #218's card half folded in. It needs a fresh CI run on current main.

Decision for the maintainer

• How much of the testimony validator to keep. Add verified statement-review bundles #40's blocker 4 asked to reject control, bidirectional and TeX hiding primitives; the answer grew into models of two more renderers. This layer alone adds about 11% to main's Python, against the size bar Publish blueprint sites transactionally #165 set. Options: (a) keep it as is, with a compiled base dependency, a MathJax pin to re-check on every upgrade, and GitHub formula rules inferred from observed API output that CI cannot re-check; (b) drop GitHub parity: cmarkgfm, _github_errors, _github_formulas, _shown and _paragraphs (roughly 400 lines plus tests), keep the cards, the API, the no-HTML renderer, the Unicode checks and the TeX allowlist, and state that the site (Show statement review on the site #217) is the reviewed rendering; (c) also replace the MathJax layout model with a coarse allowlist that refuses unlisted commands and all spacing except \,, \; and \quad, removing most of another 900 lines. Recommendation: (b); decide (c) together with Label statement approvals by the repository's code-owner review policy #219's trim, since it is the same size-versus-outcome question.
• Intel Macs and a C compiler. uv.lock has no x86_64 macOS wheel for cmarkgfm, and both MCP servers start through uv run --project, so an Intel Mac must compile it before the LSP or REPL server starts, even for users who never file a read-back (confirmed; the PR's own test_intel_macos_source_builds_are_still_needed passes). Main has been wheel-only there since Constrain cryptography below 49 on Intel Macs #56. Option (b) removes this; under (a), make cmarkgfm an optional extra with a lazy import.

This was a static review: no tests were run locally. CI at this head: all 9 checks pass, but on the stack's old base 8575a15.

Posted by PR swarm: PR Swarm Lead