Repository navigation
Conversation
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
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
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
|
Maintainer review of 4aff495 (read-only; Round
Nits (same push)
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 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
|
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 Generated by Claude Code |
|
Maintainer: closed as a stacked draft whose commits are contained in #315 ( Generated by Claude Code |
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-07as you decided on #282/#92). Draft; stacked on #266 (baseclaude/issue-92-rust-lower-types, which carries #258).applyMovesofRustMoves(moduleRustMoves), the oraclecalculus::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 aRustAstcrate. Held to the oracle directly, to the byte.BS-07is untouched except for its recount (VECTORS310 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 partbootstrap-movesin.github/bdd-parts.jsonand.github/vv-rows.json,xtaskand 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-modelandvalidate-spec-linksclean; clippy-D warningsclean.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:siteTrees3,144,673,deadFunctions1,273,118,fallibleFunctions1,058,398,lowerTypes1,535,849.) The typing-root rule holds:siteTreesis 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 asBS-05draws them; 1,500 seeded mutants agree under rustc; eight planted defects inRustMoves.lex.texare 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-05456 and 319 vectors;BS-06615printCratevectors, 472 committed distinct, 544 evaluator crates;BS-07311 vectors).What fails here until the maintainer's regeneration (identity-bound, not committed): the package
apply_movesand the others ofBS-07undertests/production-export/bootstrap/packages/rust-std/; the PD-08 rowbootstrap/apply_moves(6,029,312 bytes, measured in a debug build here);bootstrap/expected/{build,verify}; both locks.roots.jsonnamesapplyMoves.https://claude.ai/code/session_0163mCfJeketviuEBiXJ1sQY
Generated by Claude Code