v0.4 train: byte literals (#68), widening (#151), dyadic floats (#150), certificates A and B as data, package scaffolding, regenerated once

[afflom]

Closes #114
Closes #118

The v0.4 train: every pull request that moves a language-1.2 identity or a committed record, integrated on current main (including #166) and regenerated once, so that the gate runs once on one tree and each member lands in one merge. Draft until the head is final; marking it ready runs the whole gate once (the plan job of #166).

Members, and what each closes

Member	What it is	On this PR
#68	explicit byte-literal lowering (UInt8.ofNat (nat_lit n), shared octets bound once), SM-19 / MD-02 readers	head is an ancestor; merges with the train
#151 (#114)	to_int / to_nat widening in language 1.2 (SM-32)	content re-applied here (certificates now read elaborated declarations); closes #114; #151 closed by hand with a pointer
#150 (#118)	IEEE-754 bit patterns as exact dyadic rationals (MD-13)	content re-applied here; closes #118; #150 closed by hand with a pointer
#157	certificate A as kernel-term data (SP-15), stage 3 of #89	head is an ancestor; merges with the train
#163	certificate B as kernel-term data (SP-16, stage 2 of #89) and stage 4, no Lean text template remains in the production compiler (SP-17)	head b01a9e0ab is an ancestor
train/package-scaffold	#91 slice 1, #105 3b: the Rust package scaffolding is data read from an embedded language module; effects are the root's to state; review fixes dd8691b96	merged; #91 and #105 stay open for their later stages
fix(#117)	the runtime gates know LexLeanLaws (RT-01, RT-04)	cherry-picked (ddc65e5a1)

Register: 413 required capability IDs (README, SPEC §31, cases/repository.rs, spec_links.rs, model/ids.toml, CONFORMANCE.md agree).

Hand-written on top of the members

• lean_backend identities of the byte-literal lowering: language 1.1 10, 1.2 20.
• Certificate A's data path refuses ToInt/ToNat with the elaboration it is certified through (certificate.rs, data_a/*).
• The preservation library's LexLeanTarget.TargetSemantics.fromOrdering.eq_1 statement follows fix(backend): lower explicit shared byte literals without widening limits #68's spelling (the embedded library checks a stored equation against the elaborator's; 7053b2185).
• tests/negative/lowering-size-limit is a match on 400 constructors: with A and B as kernel data a repeated type is one node and the 16-deep chain it was verifies; the new fixture is refused LLS8002 in lowering (certificate A ≥ 10,200,437 bytes). Recorded in VERIFICATION.md.
• SPEC §17.17 Limits: cost table as COSTS_A/COSTS_B state; the chain verifies 16 deep; A's costs are the largest with five percent to spare, B's and E's half of the greatest; certificate-B paragraph with the B author's measured figures (100 fields: 393,291 bytes; floor 8 bytes a slot).
• From the draft runs: A's eight #[ignore]d developer lenses removed (R4, RP-08, RP-12; A-STATEMENTS.md records the oracle's commit, as E's and B's do); SM-32 before SM-33 (RP-11); one README capability row per prefix; the Lean-literal allow-list entry of the removed printout dropped (SP-17).
• From the integration review (humuhumu33, 5560570236): SP-02 states 240 constructors (FITTING_CONSTRUCTORS); OR-04's plants on Coverage.Prims.text re-anchored to the oracle crate's current locals (_x_67, _x_43; conformance_or_04 passes locally, 169 s); CHANGELOG names fix(backend): lower explicit shared byte literals without widening limits #68's identity moves and drops stale per-member counts; VERIFICATION's text-era chain and arm-pair plants marked superseded with the current evidence; the SP-15 plant record added (20 lowering plants: 14 rejected by the kernel, 6 refused by the generator in lockstep, 0 accepted; five data plants refused).

Regenerated

f1e11576e, by the repository's writers only: both compiler-semantics IDs and every lexlean.lock, golden oracles, calculus fixtures, production export, conformance fixtures, and the normalized verification records of every example that moves, each verified end to end with the pinned Lean 4.32.1 (language-1.0 examples do not move), then validate-model --write.

Evidence

• Locally on the final tree: cargo fmt --check, validate-model, validate-spec-links, check-test-inventory, check-golden, check-calculus pass; check-production-export and clippy -D warnings were passing on the pre-regeneration tree and the regeneration touched no Rust (the read-back check is running as this is written); conformance_rp_08, rp_11, rp_12, or_04 pass.
• conformance_sp_02 passed on A's head 7653ed1e2 (7951 s, the certificate-A session); the train's gate judges it on this tree.
• Item 6 of fix(backend): lower explicit shared byte literals without widening limits #68 (fresh PrismPM qualification) is an owner adoption gate in the PrismPM repository; this PR does not run it.

How this merges

The head contains main (8765feea). Marked ready once, on the final head; merge commit; its push run on main runs nothing when this PR's run passed every job (#166).

🤖 Generated with Claude Code

https://claude.ai/code/session_013QppGKetUURseXowZun9KY

[afflom]

@humuhumu33 the head is final: f1e11576e, marked ready for the one whole-gate run. It contains main 8765feea; every point of your review is in (your member points as dd8691b96, merged 878df445e); the regeneration is f1e11576e; the draft run of this head passed (plan, just vv (rest), honesty, reproducibility), and every local gate passes on it (fmt, model, spec-links, inventory, golden, calculus, production export, clippy). conformance_sp_02 passed on A's head in 7951 s; this run judges it on the integrated tree.

Your formal approval on this head, once the gate is green, is the review the merge waits for (merge commit, sha pinned). I will not push to this branch again unless the gate is red.

---

Generated by Claude Code

[afflom]

just vv (bdd-production) is red on f1e11576e: conformance_px_13 finds 52 eligible outputs of production-coverage and 49 exported. The three are #151's new roots, Coverage.Prims.widenings (rust-core, rust-std) and Coverage.Prims.pixels (rust-std): #151 added them to the source and not to the export request tests/production-export/production-coverage/roots.json, and its own gate never ran this leg (draft). Not a Lean or certificate fault. Fix under way on the train: the two roots join roots.json, the export writer produces their packages, PX-13 is re-run locally, then one push and the gate again. The other legs of this run stand as evidence for this tree (SP-02 among them).

---

Generated by Claude Code

[afflom]

just vv (bdd-verification) is red on f1e11576e as well: conformance_vr_13 finds preserve/LexLeanPreserve/C<hex>/R0.lex.tex outside §22.8's fixed artifact set. The set still names the text certificates (preserve/LexLeanPreserve/*/*.lean); with A and B as kernel data (#157, #163) the records are R<i>.lex.tex (A) and R<i>/<Target>.lex.tex (B) beside E's Compose/*.lex.tex, and neither member PR ran this leg (drafts). Fix on the train: the two slots replace the .lean slot in VR-13 and in the SPEC §22.8 list, in step; conformance_vr_13 is re-running locally. It goes in the same push as the PX-13 fix.

---

Generated by Claude Code

[afflom]

build and non-Lean tests (aarch64-unknown-linux-gnu) is red on f1e11576e: conformance_sp_08 (the 9000-arm match derived on a 2 MiB stack). Not the host and not the stack: the lowering refuses the match before the aligner runs, LLS8002 … its certificate A is at least 5153967937 bytes (27005 program nodes) against the stress harness's lifted limit of 4,000,000,000. With certificate A's cost of a pair of arms at 1018 sixteenths (#157; 180 for the text certificate) the 81 million pairs bound at about 5.2 GB, so the harness's "limits lifted far enough" no longer were. The other host legs will show the same. Fix on the train: stress::project_limited lifts max_file_bytes to 16,000,000,000, with the arithmetic in its comment; conformance_sp_08 is re-running locally. Same push as the PX-13 and VR-13 fixes.

---

Generated by Claude Code

[afflom]

@humuhumu33 the head moved once, to 0c206d983, carrying only the three gate fixes above (roots.json + the two new export packages; VR-13's §22.8 slots for A and B as data; the stress harness's lifted limit at 16,000,000,000), each proven by its case locally (conformance_px_13 885 s, conformance_vr_13 341 s, conformance_sp_08 1612 s). Every other job of run 39088412866 on f1e11576e was green, conformance_sp_02 among them (bdd-preservation: 13 of 14 passed, SP-08 the one). The whole gate is running on 0c206d983 now; your approval on that head is what the merge waits for.

---

Generated by Claude Code

[afflom]

Run 39094595513 on 0c206d983: 24 of 25 jobs green, every previously red leg among them (bdd-production, bdd-verification, bdd-preservation with SP-02 and SP-08, the Linux arm, macOS arm and Windows hosts). The one non-green job is build and non-Lean tests (x86_64-apple-darwin), cancelled at its 120-minute timeout-minutes, not failed: the certificate stress cases now build A and B as kernel data and the non-Lean suite takes 2.9 times as long (1064 s to 3051 s on the arm Linux runner; the host legs went 25/22/41/51 min to 59/74/88/>120), and the Intel runner is the slowest. The head moved once more, to f5748851c: only ci.yml's host-matrix limit, 120 to 300 by the rule its comment already stated (twice the slowest observed), with the observation written in. RP-14 passes (the host matrix is exempt from the gate jobs' limits). The regression itself is filed for the A/B and CI lanes with the measurements and two fixes. The whole gate is running on f5748851c; @humuhumu33, that is the head for your approval.

---

Generated by Claude Code

[afflom]

The whole gate is green on f5748851c: run 39101767733, 25 of 25 jobs (27 check runs) success, including bdd-preservation with conformance_sp_02 on the integrated tree and every host of the matrix; the Intel macOS host finished in 100 min, inside the 300-minute budget of 0c206d983. The head contains main; mergeable is true.

Measured: 730 runner-minutes, 102 min wall. The excess over the 516 runner-minutes measured for #166 is the host matrix (Intel mac 100, arm mac 78, Windows 69, arm Linux 58 min), the regression tracked as #177; the Lean legs are unchanged. The push run on main after the merge should run nothing (#166's plan job), so the merge itself costs no runner time.

@humuhumu33 — this is the head you asked to see after cde36cd4b; every point of that review is addressed in 7053b2185..f5748851c as replied above. It needs a formal approval from someone other than the author to merge; I have requested your review on the PR. Nothing else blocks it.

---

Generated by Claude Code

[humuhumu33]

Approved at f5748851c.

Checked on this head: it contains main 8765feea; every job of the ready run 39101767733 is green, conformance_sp_02, conformance_sp_08 and conformance_or_04 included; the integration points of my review (5560570236) are in, as your disposition lists, and the package-scaffold points are in as dd8691b96 (merged 878df445e), including the two that move the language-1.2 ID, before the regeneration f1e11576e. Since f1e11576e the head changes only the three fixes of the red run (the PX-13 export roots and their writer-produced packages; the VR-13 artifact slots, which replace the *.lean slot with the two data-record slots rather than adding beside it; the stress harness limit of SP-08, which lifts no limit a project sees) and the host matrix's timeout-minutes of f5748851c.

What my member reviews raised and this head does not change, I have reclassified as follow-ups and filed. Two of those reviews (#157, #151) said "request changes"; my reason for approving anyway is that none of the open items lets the compiler accept a wrong program, certificate, or package, or weakens the kernel check, the axiom audit, the statement oracle, or §9.4. Every accepted certificate is still kernel-checked, audited, and size-checked exactly. What remains is normative text that claims more than the code does, test evidence weaker than its record, and debug code §23.1 does not list. Each fix is text, a test, or a deletion, and none needs a regeneration of compiler records:

• #178: how certificate generation is bounded (A is checked once whole; SPEC §17.17 and SP-02 say part by part; B's early abort can overshoot).
• #179: plant evidence states what it shows (the locus of generator refusals, Buffer plants reaching the kernel, SP-16's forged-program plant, the SM-32 records re-run).
• #180: the compiler reads no environment variable beyond the four of §23.1 (data_a.rs debug hooks, the allow-list entry).
• #181: SP-17 writes down what it cannot see and narrows its allow-list.
• #182: text and coverage left from the member reviews (§17.17 B prose, COSTS_B's method, the SP-02 edge skip, #68's binder rule and measurements, #150's dyadicRoundShift and counts, #151's 64-bit root and overflow wording, and a CHANGELOG line that the widest match certificate A fits under the default max_file_bytes falls from about 420 to 240 constructors).

Merge with a merge commit pinned to this head, as you said.

---

Generated by Claude Code