[humuhumu33]

What

A ready pull request whose generated files were not regenerated runs the whole gate (about $29, 2.2 h) and fails deep in the fan-out. This adds a fail-fast precondition to honesty, which runs before every expensive root:

cargo xtask check-freshness (new; crates/conformance/src/freshness.rs) needs no Lean and reads only committed files:

• every input that a committed build oracle (*/expected/build/manifest.json, 23 projects) records still has its recorded SHA-256 and length (262 inputs: sources, lexlean.toml, lexlean.lock, model artifacts, source-package files such as std:src/Text.lex.tex). Lexicon inputs are left to the next two checks;
• every such project's lock passes lexlean lock --check (library call, no network);
• every oracle names this compiler's semantics ID for its language;
• every committed package under tests/production-export/ (139) names this compiler's semantics and, in sources, its project's committed semantic_id.

honesty runs it as a step before just fmt-check model spec-links bdd. SPEC.md §9.4 states it, and RP-14 requires it in honesty before the gate command. It adds a precondition and replaces no check: golden, examples, PX-01 and the bootstrap cases still compare every byte.

Slices stay draft until regenerated (regenerate.yml, #467), and only ready PRs into release/* run the full gate (already true).

Measured locally (WSL, release/v0.4 7eb8162)

• Clean tree: check-freshness: 23 build oracles (262 recorded inputs), their locks, and 139 committed export packages are current, 2.5 s, with Lean removed from PATH.
• Plants, each refused: a line appended to bootstrap/src/TokenAudit.lex.tex (the oracle input changed, and the 37 bootstrap packages lose their semantic ID); one stdlib package's sources replaced; the stdlib lock's compiler semantics altered (the input digest changed, and lock --check fails).
• fmt, clippy, the new unit test, validate-model, validate-spec-links, all 17 RP cases.

Measurement in CI

Draft run 43142198451 on 834522b (this change merged with release/v0.4 5dccf9e; the only conflict was CHANGELOG.md). In CI it printed: check-freshness: 23 build oracles (262 recorded inputs), their locks, and 139 committed export packages are current (§9.4).

honesty	baseline 43046966603	this PR, 43142198451
freshness step	n/a	83 s (mostly the xtask build the recipes then reuse)
fmt-check model spec-links bdd	105 s	57 s
job	2.4 min	3.1 min

Cost: about +35 s of one Linux job per run, which is +$0.004 per run. A ready PR with stale generated files now fails at about 5 min, before the fan-out, instead of paying for a whole gate (~$29, 1,800-1,900 runner-min, 2+ h) that fails in its later jobs. No full-gate dispatch was made for this change; it touches only honesty.

Not verified: a real stale slice branch in CI (the plants above are local). How many of November's 84 failed runs were caused by stale generated files was not counted.

🤖 Generated with Claude Code

[afflom]

[P2] Record the already performed freshness plants in VERIFICATION.md. AGENTS.md's gate rule requires planting the defect, confirming the failure, then recording it in the falsifiability table. The PR body reports three direct check-freshness plants, but this eight-file delta leaves VERIFICATION.md unchanged and it has no record for this new detector. Please record those existing commands, observed refusals, restoration and scope; no new runtime, per-line plant or additional RP-14 mutation is requested.

The bounded source review found no demonstrated current-tree regression in recorded-input hashing, source-package path resolution, language-specific identities or the offline check-only lock call. The original full golden/examples/PX/bootstrap checks remain. This is an early check over discovered committed records, not a complete regeneration/completeness proof; new/unrecorded inputs and every output byte still belong to the original gates.

The reported 2.5s timing and plant results remain owner evidence, not measurements repeated by this review. Final exact-head qualification remains with the existing owner. Independent receipt d8166fbd records the inspected source and limitations.