[afflom]

BS-06 (#92 step 4c) and SL-05: the Rust printer calculus::rust::ast::{print, print_expr} as language-1.2 source in bootstrap/ (RustAst, RustPrint), and the standard library's Buffer it writes through. Plan and decisions: #92 (comment). Stacked on #248; draft.

What

• stdlib/src/Buffer.lex.tex (SL-05): new, writeBytes, writeByte, writeDecimal, length, finish; a write past the capacity is a refusal at finish. Chunked (256 bytes) over today's primitives because a chain of append is quadratic (measured; VERIFICATION.md). Roots writeAll, writeEach, writeNumbers; the added roots are in tests/production-export/stdlib/roots.json.
• bootstrap/src/RustAst.lex.tex, RustPrint.lex.tex (BS-06): printCrate (capacity) (header) (krate) and printExpr (capacity) (expr), both rust-std, effects allocation, overflow, recursion.
• Register 445 (SL-05, BS-06), SPEC §31, §17.22, §17.23, scenarios, conformance_sl_05, conformance_bs_06 (R3 order: the rows and the failing tests are the first two commits).

Measured (this host, 4 cores, debug build)

• conformance_bs_06: 1,658 s end to end, Lean export included. Every-host part (rustc, 42 harness binaries, 2,535 vectors): 504 s. Evaluator 539 + 1,937 vectors and 400 + 399 seeded mutants; 2,984 further mutants under rustc (79 s); twelve plants, each detected (first disagreements in VERIFICATION.md).
• Lean: production build of the two print roots 15 min 57 s; certificate parts are within the cap (no split needed for the printer).
• conformance_sl_05: chunk size by measurement on 256,713 bytes (table in VERIFICATION.md); the work of one-byte writes is linear (551k, 2.24M, 9.08M units at 4,096, 16,384, 65,536 bytes); the planted buffer that never seals is caught (8.4M and 134M units).
• Stack bounds (debug, bisected): print_crate 7,077,888 bytes, print_expr 4,259,840.

Not in this PR (the maintainer's records)

Locks, bootstrap/expected, tests/production-export/{bootstrap,stdlib}/packages, tests/stack-bounds.json rows. I relocked locally and copied the two print packages and the two stack rows locally to run the cases; none is committed. Both cases pass every leg up to the comparison with the committed packages. The counts the case asserts (252 manifests, 169 programs, 228 crates, 252 packages) are those of the tree with the two print packages committed.

Boundary and findings

• Outside the claim: a crate whose exported name holds a non-ASCII scalar, a literal wider than 64 bits, a machine call with fewer operands than its primitive (the oracle indexes past it). The header is an argument.
• Committed libraries pin the printed items; the header before them is the runtime of the committed export, which moves with #91 stage 4, PR 4: the width families of the core runtime as source (RB-16, SP-22) #248's runtime.
• Findings for the next components (certificate A cannot name the matched variable inside a branch; bit_and on Nat is refused; id and first are reserved) are in VERIFICATION.md.

https://claude.ai/code/session_0163mCfJeketviuEBiXJ1sQY

---

Generated by Claude Code

[afflom]

Maintainer review of 7bea806 (read-only; validate-model 445 ids, validate-spec-links 445 rows, check-test-inventory 775 tests all green in a worktree). The printer, its differential and the plants are as the plan asked: the twelve BS-06 plants and the two SL-05 plants each name a defect the oracle text distinguishes, the capacity refusals are counted (56) rather than skipped, the live runtime header is passed to the root and never compared with a committed one, no JSON writer is added (BS-08), no lock, export or stack-bound row is committed, and the diff outside bootstrap/, stdlib/ and the register is the two CI part entries, the count bumps and the pub(super) widening in rust_validate.rs. One round is needed before the regeneration, because as committed the regeneration cannot make the case pass:

Blocking

1. tests/production-export/bootstrap/roots.json lists no LexLeanBoot.RustPrint.printCrate or printExpr, yet the case builds the bootstrap export from that application and asserts realized == 2 with the exported keys equal to the committed ones (rust_print.rs:1469-1517). Add the two roots there; the stdlib file already carries its three Buffer roots.
2. The count constants (rust_print.rs:1159-1172, asserted at 1277-1345) assume the tree with only the two print packages added (252/169/228/252). committed() and packaged() walk tests/production-export/ as well as compiler/rust/, and SL-05 in this same PR commits three Buffer packages there (stdlib_buffer.rs:617-630), so the landed tree has 255 manifests and packages, 172 programs, 231 crates, and the dependent vector counts (598/56/1,937/539/400/399/2,984) move with them. Regenerate the figures on a tree with all five packages and change the register row, the §31 row, the scenario, §17.23 (7786-7791) and the constants together.
3. BS-05 asserts 250/167/226 over the same committed() (rust_validate.rs:2937-2940, its register row and scenario). This PR leaves it untouched, so BS-05 and BS-06 cannot both pass on one tree; §17.23 even reads "252 and not the 250 of BS-05". Bump BS-05's counts (and its 446/195/309/82 run figures if they shift) in this PR, as c360875 did for the helpdesk manifests.

Round

4. The SL-05 statement says "a contiguous output buffer" while §17.22 (7389) says it is not contiguous and the realization is chunked. Drop "contiguous" or say "contiguous in interface", byte-equal in model/ids.toml, the §31 row and the scenario.
5. The same statement names "write of bytes"; the member is writeBytes. Spell it as the member.

Nits (carry in the same push)

6. The plan asked for decimal of Nat and Int; writeDecimal is on Nat only, with the printer writing the sign itself. Say so in §17.22.
7. bootstrap/README.md:5 lists RustAst among the modules that import Text; it imports only RustValidate.
8. Run lexlean fmt --check on bootstrap/ and stdlib/ before pushing; the reviewer could not build the binary in time to confirm Buffer.lex.tex is canonical.

I will re-verify the round by reading the diff; please do not merge anything into the branch.

---

Generated by Claude Code

[afflom]

Maintainer: the round at 1ddd494 is accepted (read-only re-verification; validate-model 445, validate-spec-links 445, check-test-inventory 775, cargo fmt --check and clippy green; the three statements byte-equal in their three places). The two print roots are in roots.json; the BS-06 and BS-05 figures are those of the tree with all five packages and are asserted from the committed tree before the first leg, so on this head both cases fail only at the first count (250 against 255) and flip by construction once I commit the five packages at the landing; the SL-05 statement, §17.22 and the README are as asked. The three source files reformatted in the round are canonical layout only. The base's RustValidate.lex.tex line is already canonical on the base branch's head and vanishes on merge (conflict-free).

Lands after #248, #254 and #255 with its own regeneration (five packages, locks, stack-bound rows, bootstrap records).

---

Generated by Claude Code

[humuhumu33]

A read of fe507e42e ahead of its landing (nothing built or run). I raise it now so that anything worth changing goes into your regeneration instead of a second one.

What checked out:

• The printer port. I compared RustPrint.lex.tex with ast.rs construct by construct (literals, patterns, types, reads, wraps, calls, apply, if/match/block/probe/loop and the items). The brace-scrutinee cases, the empty else, ::MIN, the \u{..} escapes and the dropped extra machine operands all agree.
• Generator coverage. The generators reach every AST constructor, every machine at arity and arity+1, and every IntKind edge.
• Buffer capacity. The boundaries are exercised: exact capacity, ±1, 0, and 255/256/257-byte pieces.
• Linear work. It is asserted, not just recorded (proportional, stdlib_buffer.rs:545).
• Plants. None of the fourteen is caught vacuously.

1. SL-05 already exists on release/v0.5, with a different meaning. On v0.5 SL-05 is #234's "the compiler computes its content identities with the standard library's certified Sha256 package". SL-06 and SL-07 are also taken there. This PR adds SL-05 for Buffer on v0.4, so the next forward-merge into v0.5 (as #245 did) would hold two different SL-05 rows. This is the same situation as SP-24 → SP-25 in #254. SL-08 is the first number free on both lines. Renumbering before your landing regeneration would avoid moving the register a second time.

2. The register total will merge silently wrong. The head and release/v0.4 both read "445", but they count different rows: SL-05/BS-06 here, RB-17/SP-25 from #254 there. Because the lines are identical, the merge won't conflict on them, yet the true total is 447 (448 if #261 lands first). validate-model should flag it, so this is a reminder to set the four count places by hand.

3. writeDecimal is wrong from 10^20 up (stdlib/src/Buffer.lex.tex:180). decimal builds 20 digits from place 10^19 down, each taken mod 10, then strips the leading zeros. At 10^20 all 20 digits are 0 and the number is not 0, so the result is empty bytes; at 10^20 + 5 it is "5". Neither the evaluator (Nat as u64) nor rust-std can reach it, and the corpus stops at u64::MAX. The certified Lean definition still says it, and §17.22 promises "the decimal of a Nat". The fix is either to bound it in the statement and SPEC (u64 range) or to refuse above it.

4. The PR body's figures are older than the head. The body says 2,535 vectors, 539 + 1,937 evaluator runs, and 252 / 169 / 228 / 252 manifests, programs, crates and packages. The code, SPEC and VERIFICATION at the head say 2,559, 541 + 1,955, and 255 / 172 / 231 / 255.

Minor, for the record:

• The "outside the claim" boundaries are stated rather than refused. RustPrint prints a machine call with fewer operands (a two-operand NatRem gives u64::checked_rem(v0, v1)) and literals of any width. Only the upstream validator and the test encoder's expect (rust_print.rs:43) stop them.
• catch (rust_print.rs:366) swallows every oracle panic, not only an index past an operand.
• The upper-case-hex plant (rust_print.rs:1062) is first caught on a byte string, so it does not isolate the \u{..} path.

[afflom]

Maintainer: the landing regeneration is pushed (baadfef merges release/v0.4 at f057b83; e99ee47 the five packages, locks, goldens, the stack rows bootstrap/print_crate 7,077,888 and bootstrap/print_expr 4,259,840, the register count 447 after the merge with #254, and the SL-05 case on a thread sized as the differential's, since it overflowed a test thread's stack when it evaluates the chunked buffer; 127a955 the stdlib and bootstrap verification records) and the PR is ready; the full gate is running on 127a955. The compiler-semantics ID does not move; all ten identity cases, including bs_06 and sl_05, pass on the landing tree. The Atlas join, the final gate and the merge follow. No pushes to this branch, please, until it is merged.

---

Generated by Claude Code