[v0.4] Release follow-ups to #167: generation bounds in SPEC, no undeclared environment variables, leftover text and coverage #187

Follow-up to #167, combining #178, #180 and #182 so v0.4 carries one small issue that one PR can close. None of these lets the compiler accept a wrong program, certificate or package; each fix is text, a test, or a deletion, and none moves the language-1.2 identity or needs a regeneration of compiler records. The two test-strengthening follow-ups (#179, #181) move to LexLean v0.5.

1. How certificate generation is bounded (was #178)

• Certificate A is built whole and then weighed once: crates/lexlean/src/production/certificate.rs:539-552, generator.within(source.len(), "certificate A") after module_data.
• B's early abort counts 12 bytes a node (data_b/align.rs:100) while a record read takes about 35, so it can hold about three times the limit before it stops. Its final refusal is exact (data_b.rs:654).

No oversized certificate is accepted. The gap is the work and memory bound the text promises.

Definition of done:

• Either the A data writer and B's aligner count parts against max_file_bytes as they build, with a per-node weight that is a floor of the recorded notation, or §17.17 and the SP-02 statement say exactly what bounds generation (the lowering's lower bound, then a whole-certificate check) and how far past the limit a generator can get.
• A planted defect recorded in VERIFICATION.md: a root whose certificate passes the early bound but exceeds the limit is refused with LLS8002, and the record states the peak size held.
• No weaker gate; just vv green.

For v0.4, the text option is enough: §17.17 and the SP-02 statement say exactly what bounds generation today (the lowering's lower bound, then a whole-certificate check) and how far past the limit a generator can get. Making the generators count part by part can follow in v0.5.

2. The compiler reads no environment variable beyond the four of §23.1 (was #180)

• LEXLEAN_AXDBG (crates/lexlean/src/production/certificate/data_a.rs:366), which prints axioms to stderr;
• LEXLEAN_SHOW (:383), which prints a row;
• LEXLEAN_SHOW_FILE (:385-386), which writes that row to a path the environment names.

The SP-17 allow-list sanctions the printout (crates/conformance/src/lean_literals.rs:73).

Definition of done:

• The three hooks and the allow-list entry are removed.
• A gate fails on any std::env::var in crates/lexlean/src that names a variable outside §23.1's four, with a planted defect recorded in VERIFICATION.md.
• just vv green.

3. Text and coverage left from the train's member reviews (was #182)

• SPEC §17.17, certificate B: "2.4 KB of each certificate B" (SPEC.md:5003), program and crate terms "noncomputable" (:5024; they are not compiled), the B checking times measured on text certificates, and the two reasons given for the missing module header.
• COSTS_B: record how it was derived (SPEC.md:4923 says half of the greatest; the review found the text-era costs divided by four). State in SP-02 that a mixed shape fitting at full scale 256 gets no edge check (cases/preservation.rs:425).
• fix(backend): lower explicit shared byte literals without widening limits #68:
  • The binder-hygiene rule (SPEC.md:2777) still says byte literals are written without qualification; they use _root_. names and bind __byteN.
  • The VERIFICATION measurements describe a scratch file at Lean's default limits, not generated modules (semantic.rs sets maxRecDepth 100000).
  • "MD-02 applies the same reader" is false (models.rs:541-594; 2 of 6 *.bytes definitions checked).
• feat(models): decode IEEE-754 bit patterns as exact dyadic rationals (MD-13, #118) #150:
  • dyadicRoundShift (examples/models/src/Recognizer.lex.tex:356) ignores the done flag of iterate_until and returns a wrong value when exponent plus shift exceeds 512. Return Option, or delete it with the unused dyadicMul.
  • decodeBinary64's unsigned branch is untested.
  • CHANGELOG says "43 theorems (39 + 4)"; there are 47.
  • The skewed-oracle plant's output is "..." in VERIFICATION.md.
• Capacity: CHANGELOG says that, with certificate A as data, a pair of match arms costs about 5.7 times its text cost (1018 against 180 sixteenths), so the widest match that fits the default max_file_bytes falls from about 420 to 240 constructors (SP-02, SPEC §17.17), and that a project with a wider match raises max_file_bytes.
• feat(semantic-ir): byte and fixed-width widening conversions in language 1.2 (SM-32, #114) #151:
  • Add a production root over UInt64/Int64 with an input that reaches to_int's overflow at or above 2^63.
  • SPEC §17.12 rule 2 should say that overflow happens.

Definition of done: each bullet is fixed or answered on this issue; just vv green.

Definition of done for this issue

• Each of the three sections above is fixed or answered here, with section 1 by its text option at least.
• One PR, just vv green, planted defects recorded in VERIFICATION.md where a section asks for one.

Generated by Claude Code