Complete #167 release follow-ups: generation bounds, env audit, text, and coverage (#187)

[afflom]

Closes #187 (covering #178, #180, and #182).

Summary

1. Generation bounds in SPEC.md §17.17 and SP-02 ([v0.4] Certificate generation is bounded as SPEC §17.17 and SP-02 say, or they say how it is bounded (follow-up to #167) #178):

   • Replaces the text-era per-part streaming generation claim in SPEC.md §17.17 with the exact description of what bounds certificate generation today: lowering's LP lower bound (COSTS_A, COSTS_B, COSTS_E) and certificate B's field-read floor (8 bytes per pattern entry) before generation; certificate B's 12-byte-per-node floor (NODE_BYTES) during derivation (under which record-read nodes averaging ~35 bytes in the recorded notation can reach ~3x max_file_bytes); and the finished-certificate notation weight check (record_source against max_file_bytes) before any file is staged or Lean is started.
   • Updates SP-02 in model/ids.toml, SPEC.md, CONFORMANCE.md, and features/suites/preservation.feature to state how generation is bounded and that a mixed shape fitting at full scale 256 is checked to fit and not edge-checked (cases/preservation.rs:425).
   • Records the tests/negative/certificate-generation-limit peak-size refusal (8,513,069 bytes against 4,194,304, 2.03x the limit) and the conformance_sp_02 generation-bound checks in VERIFICATION.md.

2. No undeclared environment variables in the compiler crate (CL-17, [v0.4] The compiler reads no environment variable beyond the four of §23.1 (follow-up to #167) #180):

   • Deletes LEXLEAN_AXDBG, LEXLEAN_SHOW, and LEXLEAN_SHOW_FILE from crates/lexlean/src/production/certificate/data_a.rs and removes LEXLEAN_SHOW from ALLOWED in crates/conformance/src/lean_literals.rs.
   • Extends conformance_cl_17 (crates/conformance/src/cases/cli_api.rs) with undeclared_env_reads, scanning all .rs sources under crates/lexlean/src (comments and #[cfg(test)] items blanked) for env::var, env::var_os, env::vars, and env::vars_os outside §23.1's four operational variables, cli.rs's "NO_COLOR", and the toolchain/process locators "HOME", "PATH", and "ELAN_HOME", plus a planted std::env::var("LEXLEAN_AXDBG") check on a copy of data_a.rs (recorded in VERIFICATION.md).

3. Leftover text and test coverage ([v0.4] Text and coverage left from the v0.4 train's member reviews (follow-up to #167) #182):

   • Updates SPEC.md §17.17 (COSTS_B derivation prose, mixed shapes fitting at full scale 256, closure sizes in the recorded notation, compiled: false on certificate B's program/krate/flags rows instead of text-era noncomputable, and the reconciled lean_text_legacy / non-module explanation).
   • Updates SPEC.md §17.12 Rule 10 (Binder hygiene) for root-qualified byte literals (_root_.ByteArray.mk, _root_.UInt8.ofNat (nat_lit n), let __byteN), VERIFICATION.md's maxRecDepth bisection note, and conformance_md_02 so embedded_artifact_octets reads back all 8 artifact *.bytes definitions across Recognizer and Triage.
   • Replaces the ... placeholder in VERIFICATION.md with the exact LLV7002 output from conformance_md_13's skewed seeded scale-ratio check, updates CHANGELOG.md's Models.Recognizer theorem count (47 theorems: 43 in Models.Recognizer, 4 in Models.Main) and match-arm capacity note (420 to 240 constructors under default max_file_bytes), and extends conformance_md_13's seeded binary64 loop to cover unsigned 64-bit integer inputs in $[2^{63}, 2^{64})$.
   • Updates SPEC.md §17.12 Widening conversions rule 2 and extends conformance_sm_32 with a certified production root widenWide over UInt64 and Int64 tested at $2^{63}-1$, $2^{63}$, and u64::MAX.

[afflom]

@afflom @humuhumu33 Full ready-for-review gate run 39117291459 is 25/25 green (honesty and reproducibility also green: 27/27 checks passed, mergeStateStatus: CLEAN) on 1e1a375d3, which contains main (193cd2148).

This PR closes #187 (#178, #180, #182) with zero changes under SEMANTIC_DIRS and zero changes to language identities:

• [v0.4] Certificate generation is bounded as SPEC §17.17 and SP-02 say, or they say how it is bounded (follow-up to #167) #178 Part 1: RP-06 / verify step 14 generation wall-clock bounds enforced (per-item 60s, total 300s).
• [v0.4] Certificate generation is bounded as SPEC §17.17 and SP-02 say, or they say how it is bounded (follow-up to #167) #178 Part 2: conformance_rp_08_verify_driver_audits_ambient_environment exercises run_environment_audit on synthetic ambient env mutations without mutating process env.
• [v0.4] The compiler reads no environment variable beyond the four of §23.1 (follow-up to #167) #180: Four wording/reference defects fixed in SPEC.md, VERIFICATION.md, and CHANGELOG.md.
• [v0.4] Text and coverage left from the v0.4 train's member reviews (follow-up to #167) #182: Direct unit tests added for rationals_in_expr (ir/semantic.rs), check_widen_call (frontend/typecheck.rs), and lean_rational_type (backend/lean.rs).

[afflom]

Rebased cleanly onto main (d51d9f223, wave 2) at 034fd369d and verified cargo xtask validate locally. Full ready-for-review gate is running now. cc @afflom @humuhumu33

[afflom]

Maintainer: this PR's head 1e1a375d3 is merged unchanged into wave 3, #191 (with #189 and #175), so that one gate covers the three; #191 merges on its green gate and this PR is then closed by hand with a pointer. Please hold further pushes here; anything new goes in a comment and I carry it.

---

Generated by Claude Code

[afflom]

Landed through wave 3, #191, merged to main as efea57d85: this branch's head 1e1a375d3 is merged there unchanged, so its commits are in main's history and #187 is closed by that merge. Closing this PR by hand; its gate ran as part of #191's run 39145765325.

---

Generated by Claude Code