Skip to content

BS-08 (#92): the last-use moves of the lowering, first pass of the function bodies (draft) - #282

Closed
afflom wants to merge 10 commits into
claude/issue-92-rust-lower-typesfrom
claude/issue-92-rust-lower-bodies
Closed

afflom wants to merge 10 commits into
claude/issue-92-rust-lower-typesfrom
claude/issue-92-rust-lower-bodies

Conversation

@afflom

@afflom afflom commented Oct 22, 2026 •

Copy link
Copy Markdown
Member

BS-08 (#92): the last-use moves of the lowering, first pass of the function bodies (third slice of the lowering, re-registered from BS-07 as you decided on #282/#92). Draft; stacked on #266 (base claude/issue-92-rust-lower-types, which carries #258).

applyMoves of RustMoves (module RustMoves), the oracle calculus::rust::moves::apply (public, 218 lines): a read of a binding that nothing after it reads becomes a move, and the projection of a pair component that nothing after it reads moves that component out of the pair, over the function bodies of a RustAst crate. Held to the oracle directly, to the byte. BS-07 is untouched except for its recount (VECTORS 310 to 311, with the package of this root) and two visibility changes so this case can reuse its eligibility helpers.

Register: BS-08 (model/ids.toml, SPEC.md §31 and the total 447, features/suites/bootstrap.feature, conformance_bs_08, the bdd part bootstrap-moves in .github/bdd-parts.json and .github/vv-rows.json, xtask and the repository case at 447, README, CHANGELOG, SPEC.md §17.23's eighth component, VERIFICATION's record). check-test-inventory: 777 tests, 12 parts. validate-model and validate-spec-links clean; clippy -D warnings clean.

Certificate part, measured (limit 4,194,304; the budget the case asserts is 75% = 3,145,728): parts A 551,083, B 565,927 (the largest, 13.5% of the limit), E 164,725; exact axioms observed Classical.choice, Quot.sound, propext; export 19 min 46 s. (I first reported 551,083 as the largest; that is part A. The rows of slices 1 and 2 are unchanged: siteTrees 3,144,673, deadFunctions 1,273,118, fallibleFunctions 1,058,398, lowerTypes 1,535,849.) The typing-root rule holds: siteTrees is untouched.

Case (conformance_bs_08, 29 min on this host, 4.7 GB resident): 352 crates agree under rustc on every host (21 harness binaries, 263 s); on the normative host the evaluator agrees on 317 of them (at most 400 expressions) and 150 seeded mutants of crates of at most 80 expressions as BS-05 draws them; 1,500 seeded mutants agree under rustc; eight planted defects in RustMoves.lex.tex are each detected (five first drafts were equivalent or too weak and were fixed with rule crates, listed in VERIFICATION); then the case stops at the committed-package comparison, as for #258/#266. Not re-run in full on this tree: BS-07, BS-05, BS-06 (their counts were recomputed by running their count assertions on this tree with the packages regenerated, as #266 did: 260 manifests and packages, 177 programs, 236 crates; BS-05 456 and 319 vectors; BS-06 615 printCrate vectors, 472 committed distinct, 544 evaluator crates; BS-07 311 vectors).

What fails here until the maintainer's regeneration (identity-bound, not committed): the package apply_moves and the others of BS-07 under tests/production-export/bootstrap/packages/rust-std/; the PD-08 row bootstrap/apply_moves (6,029,312 bytes, measured in a debug build here); bootstrap/expected/{build,verify}; both locks. roots.json names applyMoves.

https://claude.ai/code/session_0163mCfJeketviuEBiXJ1sQY


Generated by Claude Code

RustMoves ports calculus::rust::moves::apply over the function bodies of a
RustAst crate; the case holds it to the public oracle. The export check also
maps every root to its own lowered program (lowerTypes was compared to the
program of fallibleFunctions).

Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_0163mCfJeketviuEBiXJ1sQY
…r-bodies

Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_0163mCfJeketviuEBiXJ1sQY
Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_0163mCfJeketviuEBiXJ1sQY
…ost 80 expressions

The first full run was killed for memory (14 GB resident) in the seeded leg.

Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_0163mCfJeketviuEBiXJ1sQY
…ises its rule

Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_0163mCfJeketviuEBiXJ1sQY
The first pass of the function bodies leaves BS-07 and is registered as BS-08
(row, section 31, scenario, test, bdd part, 447 IDs); its case holds
applyMoves to calculus::rust::moves::apply, with eight plants and mutation
bases of at most 80 expressions. BS-05, BS-06 and BS-07 are recounted on the
tree with the package of applyMoves.

Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_0163mCfJeketviuEBiXJ1sQY
…e (565,927 bytes, part B)

Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_0163mCfJeketviuEBiXJ1sQY
@afflom afflom changed the title BS-07 (#92): the function bodies by pass, first pass applyMoves (third slice, draft) BS-08 (#92): the last-use moves of the lowering, first pass of the function bodies (draft) Oct 22, 2026

afflom commented Oct 22, 2026

Copy link
Copy Markdown
Member Author

Maintainer review of 4aff495 (read-only; cargo fmt --check, validate-model 447, validate-spec-links 447, check-test-inventory (777 = 285 + 492, 12 parts with bootstrap-moves), clippy -D warnings on both crates, the renderer unit test, the 16 record tests, and no file under calculus/rust/ changed: all green). applyMoves follows moves::apply rule for rule (reads and moves per constructor, the per-key maxima of the merge, the loop's state read whole, the projection rule), the case holds it to the oracle to the byte on the 352 crates with the evaluator, rustc and the 1,500 mutants, the eight plants are each a real defect with its first-disagreement run as recorded, the budget is asserted for the root, the bdd part is registered consistently, and BS-07's three-line change is exactly the recount and the two pub(super). Nothing blocks; one round of figures:

Round

  1. VERIFICATION's BS-06 paragraph is half recounted: 472/236/177/260 are new, "613 vectors" and "545 + 1,955" are old; the register, SPEC and rust_print.rs say 615 and 544.
  2. VERIFICATION's BS-07 paragraph says 310 vectors per root and 1,240 runs; SPEC §17.23, the register row and rust_lower.rs say 311 and 1,244. Update it, or mark it as the measurement on BS-07 (#92): lowerTypes, the types of the lowered crate (second slice, draft) #266's tree the way the later lines do.
  3. README's bootstrap row text gained "and its last-use moves" but its ID column still reads BS-01..BS-07.

Nits (same push)

  1. The PR body's "recomputed by running their count assertions on this tree: 260 manifests" holds only with the regenerated packages present (the committed tree has 250); say "with the packages regenerated", as BS-07 (#92): lowerTypes, the types of the lowered crate (second slice, draft) #266 did.
  2. RustMoves' local idKey folds every exported name into one key, which is why the statement carves out an exported name in a read position; RustValidate.idEq compares tag, number and name bytes and would remove the carve-out. Honest as stated and the lowering never emits an export in a read position, so this may stay; your call.

After that push #282 is accepted and lands with #258 and #266 after #253 and the heap stack, with its package, its PD-08 row bootstrap/apply_moves, the locks and the bootstrap records in my regeneration. The next pass continues under the decisions on #92.


Generated by Claude Code

615 printCrate vectors and 544 evaluator crates in the BS-06 record; the BS-07
record marks its measurement as the tree of its own slice; the README names
BS-01 to BS-08.

Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_0163mCfJeketviuEBiXJ1sQY

afflom commented Oct 22, 2026

Copy link
Copy Markdown
Member Author

Maintainer: the round at 8403bad is verified by reading (615 and 544 + 1,955 in the BS-06 paragraph; the BS-07 record marks 310/1,240 as #266's tree and states 311 and 1,244 with the package of applyMoves; README BS-01..BS-08; the body's wording; the idKey carve-out stays as stated). #282 is accepted at 8403bad and lands with #258 and #266 after #253 and the heap stack. Hold pushes to this branch unless I ask.


Generated by Claude Code

afflom commented Oct 25, 2026

Copy link
Copy Markdown
Member Author

Maintainer: closed as a stacked draft whose commits are contained in #315 (86cdaf047a; the review-round commit 8403bad0c was merged there as 6edc8fb8c2), which lands the whole bootstrap stack as one regeneration (owner direction, #15: one PR per landing). Nothing is lost; the review record stays here.


Generated by Claude Code

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants