[humuhumu33]

Plan item L4.6 of #106; closes nothing on its own, #124 stays open for the per-issue wording the owner applies.

Design

What the corpus is. One registered object: the language-1.2 project examples/performance-corpus (module prefix Corpus) with the manifest corpus.toml (lexlean/performance-corpus/1). A criterion quantifies over it by naming performance-corpus, a kind, or a member by its identifier <kind>/<name>, never a program outside it.

Members. The manifest fixes the closed kinds integer-kernels, byte-parsing, long-folds, maps-and-sets, recursion, compiler, and one [[member]] row per member: identifier, kind, production root, the targets and effects the root declares, and a one-sentence contract (the function over the inputs it admits). Every member is exactly one production root of the project; every root is the root of at most one member.

The compiler kind. It is a registered gap, not a stub: the row states its precondition (the compiler is itself a production root, §17.23, L2.1/#27) and has no member while that precondition does not hold. The check enforces the pair "precondition ⇔ no member", and the set of kinds with a precondition is fixed to compiler by the register, so populating it is a register-visible change.

Mechanical membership (PC-01). The manifest is read against the production roots of the checked project (never against its own text): unknown field, unregistered kind, a root that is not a production root or is declared with other targets or effects, a kind without precondition and without member, or with both, each fails naming the defect.

General, by structure (PC-02, C1). A list of consumer names would itself name a consumer, so "no member is consumer-specific" is a structural rule: no [[source_package]], no lexicon source outside the project (builtin or a path inside it), and no file of the corpus holding a network address or naming a repository. Then every member exports through lexlean::api::production in every declared target with status kernel-checked, one output per member and target, and the bundle replays bindings-verified.

Where it is stated. SPEC.md §28.7 (new), register rows PC-01/PC-02 (new family PC, suite performance-corpus), feature features/suites/performance-corpus.feature, cases crates/conformance/src/cases/performance_corpus.rs. The new family avoids a numbering race with the sibling v0.5 PRs; nothing here needs renumbering on rebase.

Members (one per kind, each a real production root that exports)

Member	Root	Targets	Effects
integer-kernels/requantize	Corpus.IntKernels.requantize	rust-core, rust-std	overflow
byte-parsing/word	Corpus.ByteParse.word	rust-std	allocation, overflow
long-folds/moments	Corpus.LongFolds.moments	rust-std	allocation, overflow
maps-and-sets/tally	Corpus.MapsSets.tally	rust-std	allocation, overflow, recursion
recursion/tree_stats	Corpus.Recursion.treeStats	rust-std	allocation, overflow, recursion
recursion/bisect	Corpus.Recursion.bisect	rust-core, rust-std	overflow
compiler	(precondition: the compiler as a production root, §17.23)

requantize is the general form of the fold-laws kernel (offset, multiplier, divisor, bounds as parameters, no literal from any consumer). word decodes four bytes big-endian through index/to_nat, so its lowered program has no decimal text (the residual afflom recorded on #114). bisect is well-founded recursion with evidence whose self call is a tail call; treeStats is structural recursion that is not.

Register

• PC-01 the corpus definition and its mechanical membership check.
• PC-02 no consumer-specific member, every member exports.

Register 445 (validate-model), §31 bijective (validate-spec-links).

Evidence

Run on WSL Ubuntu, Linux x86-64, with the pinned Lean 4.32.1 and Rust 1.97.1 (details in the VERIFICATION.md record "The performance corpus"):

• cargo xtask validate-model: 445 ids, meta-gate and audits clean; validate-spec-links: 445 rows bijective.
• cargo test -p repo-conformance --test bdd (meta-gate), cargo clippy -p repo-conformance --all-targets --all-features -D warnings, cargo fmt --check, cargo xtask check-test-inventory: pass.
• conformance_pc_01: pass; conformance_pc_02: pass, exporting the 6 members as 8 outputs, each kernel-checked, bundle replayed bindings-verified.
• lexlean verify on the corpus: 5 modules verified; cargo xtask verify-examples --write: 138 normalized records for performance-corpus (attestation f92c50059ffb4f27a91ee7d43d5ca29d4ecd7c7d0e7cff63c1984b54ac344441), compiler/stdlib/bootstrap records unchanged; cargo xtask check-golden --write: oracles for the new example only, no other example changed.
• Planted defects (a kind without a member, a member of the compiler kind, a source package) each fail the case naming the defect; recorded in VERIFICATION.md.

Not verified here

• The full just vv was not run on this host; see the list above for the gates that were.
• Wall time is not measured: the corpus carries no time or effort figure (C8), and any later measurement over it is an open row (C5).

🤖 Generated with Claude Code

[humuhumu33]

Pushed e0ba1cc. It answers both aarch64 failures: conformance_rp_11 ("the README states the exact register size: All 445 registered conformance IDs", README said 443) now reads 445; conformance_ns_01 ("every module of the project is an entrypoint", differing by src/IdsPC.lex.tex) now has that module in spec/lexlean.toml entrypoints between IdsOR and IdsPD, with spec/lexlean.lock regenerated since it pins the project config digest. Locally: validate-model clean at 445 ids, conformance_rp_11 and conformance_ns_01 pass.

[afflom]

Maintainer: read, and in the release/v0.5 queue. The head is green and mergeable; keep it so. The release/v0.4 landings (#255 in regeneration now, then #259, #262, #264, #265, #293, the bootstrap trio #258/#266/#282, #247, #256, and #261) hold the gate and the review agents first, by the owner's direction. The v0.5 lane is reviewed in this order as agents free up: #285, #290, #286, #287, #288, #289. Read e0ba1cc43: the two aarch64 answers (README 445, IdsPC.lex.tex as an entrypoint with the lock regenerated) are the right ones. At 202 files this review is the longest of the lane and comes last.

---

Generated by Claude Code

[humuhumu33]

Merge-line round after #286, #290 and #288 landed. The head is f8a8279 and contains release/v0.5 at 655d9ae; GitHub reports it MERGEABLE.

• 9a16c71 merges release/v0.5 at 655d9ae with a merge commit. Only CHANGELOG.md and VERIFICATION.md conflicted (additions on both sides); each carries both, the line's first. model/ids.toml merged by itself at 447 rows.
• No renumbering: PC is a new family, so PC-01 and PC-02 are its first two numbers; the line's AU-14 (#241 AU-14: locate finds the environment the structural parser opens #287) and RP-17 ([0.5.0] #113: release identity, §2.3 completion release 0.5.0 and §30 for languages 1.0-1.2 (RP-17, CL-18) #288) are in their own families. The README range stays PC-01..PC-02.
• f8a8279 sets the counts to the merged register: README 447, SPEC.md §31 total 447 (regenerated by cargo xtask validate-model --write, which changed nothing else), and the PC CHANGELOG bullet ends "Register 447".
• Nothing else was invalidated: check-golden finds every example's published artifacts equal to their oracles (performance-corpus 31, uor-atlas 431), and verify-examples without the Atlas finds the 19 examples' normalized verification records equal to expected/verify (performance-corpus 138, attestation e6854c43…); the lock is unchanged.

Local, at f8a8279: validate-model (447), validate-spec-links (447 rows bijective with the register), cargo fmt --check, check-test-inventory (783 = 291 + 492), check-golden, verify-examples without the Atlas, and conformance_rp_11, conformance_pc_01, conformance_pc_02 (with the export of every member, kernel-checked), conformance_ns_01: all pass. just vv was not run locally.

CI on f8a8279 is running (honesty, plan, repro pending at this writing). Nothing is marked or merged; this waits for the maintainer's review.

[humuhumu33]

Merged into release/v0.5 at 34cfc1282 (merge commit) on all 30 checks green with the line contained, under Ilya's merge-on-green rule for our own PRs. The macOS host leg's one red was verify::child::timeout_tests::a_timeout_bounds_stderr_inherited_after_the_leader_exits (a timing test in a file this PR does not touch, on the leg #235 documents); it passed on re-run. The line is at register 447 with PC-01 and PC-02. Closing #124 by hand.