agent: builder model: opus max_turns: 120 budget_usd: 25 —
contracts/{order,locks,sharing,maps,throws,touch}.rs crossings into Nikaia (lane 2, Part #125)Score: the bootstrap (docs/bootstrap.md), lane 2: the crossings of contracts/ after L2-1 (dsl.rs, bounds_report.rs). S=2, C~4-6 M (comparable: P4b). Target: about -370 Rust code lines (self_hosting.py counts code lines): locks.rs and throws.rs deleted, the other four shrink to the forwards their callers in lane 1 and in crates/nikaia/tests/it/ need.
Cut: crates/nikaia/src/contracts/locks.rs:85-145 Cut: crates/nikaia/src/contracts/touch.rs:32-41 Cut: crates/nikaia/src/contracts/touch.rs:170-232 Cut: crates/nikaia/src/contracts/throws.rs:37-248 Cut: crates/nikaia/src/contracts/sharing.rs:170-189 Cut: crates/nikaia/src/contracts/maps.rs:52-113 Cut: crates/nikaia/src/contracts/maps.rs:137-144 Cut: crates/nikaia/src/contracts/order.rs:161-203 Convert: –profile check-free –prefix ledger_infer_
The driver converts these (ranges at acf4f08) before you start and names the draft (.draft.nika, .notes, .rs) in your prompt: start from it, do not cut or convert again. The architect’s trial run of the same cut (479 Rust lines in, 304 out, 2 TODOs): by cut, code lines Rust to draft: locks 55 to 25, touch key 4 to 5, touch infer 45 to 15, throws 186 to 97 (2 TODOs), sharing 8 to 8, maps shape 42 to 28, maps infer 7 to 7, order 26 to 4. Wrong in the draft, fix by hand: every &Parsed typed ref CheckWorld (use the host shape below); the five infers keep the name infer (R245 prefixed only function_key): name them ledger_infer_locks, ledger_infer_touches, ledger_infer_throws, ledger_infer_sharing, ledger_infer_maps, every helper ledger_infer_; order_of came out as a call to emit_order; contribution gained a wrong let given = reach ?? return (null, []) that shadows given; from_given’s params chain ends in .unwrap_or_default(); function_key is dead (#[allow(dead_code)]): drop it; reached is not in Nikaia (see Facts).
If crates/nikaia-compiler/src exists, R0 (#921) has run: read every crates/nikaia-std/src/tools below as crates/nikaia-compiler/src, and nikaia_std::tools:: as nikaia_compiler::.
Owns: crates/nikaia/src/contracts/{order,locks,sharing,maps,throws,touch}.rs (locks.rs, throws.rs deleted), contracts/mod.rs (only the pub mod lines :30-38 and the five calls in infer_package :690, :695, :737, :741, :744, plus one helper there that builds the units’ shape), contracts/send.rs (only :146), check/host.rs (only free_calls :214-216), emit/host.rs (only :196-202 and seeds_shape :262-271), emit/seeds.rs, new crates/nikaia-std/src/tools/ledger_infer.nika, tools/maps.nika (only MpShape’s two counts), tools/order.nika (only overlap_report’s overlaps_in parameter, :680), the generated tools/lowered/*. Not yours: lane 1’s project.rs, modules.rs, comptime_run.rs, build_time.rs (their calls order::overlap_report :1692, sharing::report :1707, maps::keyed_functions modules.rs :859, touch::Touch build_time.rs :19, :385 keep compiling through a one-line Rust forward or re-export with the same signature, bootstrap.md section 6); L2-1’s dsl.rs, bounds_report.rs, check/mod.rs, emit/mod.rs, lib.rs, bounds_report.nika, dsl.nika; contracts/sync.rs, ty.rs and the rest of contracts/mod.rs (later slices).
maps.nika’s MpHeld (:105, units: ref Vec[ref Program], words: ref Vec[ref winnow_grammar::InternerContext]; do not declare a second), built once in contracts/mod.rs as maps.rs :123-128 builds it today. What only Rust can answer per unit is a callback taking the unit’s index: unaliased: fn(i64, ref String) -> String sync (Rust: &|k, name| units[k as usize].unaliased(name)), holes_of: fn(i64, ref Expr) -> Vec[Expr] sync (Rust: crate::emit::literal_expressions(units[k], e), emit/mod.rs :1307); inside the loop for k in 0..held.units.len() hand the per-unit callees fn(name) { unaliased(k, name) }. CheckMethodCalls, CheckStoredCode (check_state.nika :484, :505) and Ledger (ty.nika) are Nikaia’s; the infers take mut ledger: Ledger and write ledger.functions[..], code_locks, code_throws as the Rust does.where.nika): locks.nika free_calls :110, unit_reaches :77, stored_reaches, declared_types, locking_of; touch.nika unit_touches :154, touches_of_graph; throws.nika unit_throws :61, params_as_places, stored_throws, error_sets, throws_published, throws_given, error_type :419; sharing.nika sharing_of :990; maps.nika mp_analyse :1158, MpShape :969, MpFnMaps :990; order.nika overlap_report :680; names.nika names_in :23, names_in_block :195; emit_walk.nika visited_in_block :12.throws’ contribution calls sync::reached (contracts/sync.rs :238, Rust, a later slice). It is calls::callee_of(names, expr, own, library, items) mapped 1:1 onto a Rust enum (:247-253): in Nikaia match calls::Callee (Own, Library { key, never_pauses }, Method, Opaque(name)) directly; sync.rs keeps its own reached for itself. fatal_types moves with it; error_type’s caller emit/host.rs :201 calls nikaia_std::tools::throws::error_type(&parsed.interner, e) directly.sharing::analyse_program (:127, its ty_of callback is Ty::from_ast, contracts/ty.rs, a later slice), analyse, report, the re-exports Class, Count, Decision, Fallback, every_fallback; maps::analyse/analyse_with (their key/arity read emit/seeds.rs’s Rust Seeds) and keyed_functions (lane 1’s caller); order’s re-exports, operation, accounted, Pauses and overlap_report as a forward; touch’s TouchOps, KINDS and its ten #[test]s (:122-149, :234-381; callers build_time.rs, tests/it/touch_sets.rs). ClassOps (sharing.rs :114-123) has no caller: delete it.locks::free_calls’ caller check/host.rs :215 calls nikaia_std::tools::locks::free_calls with its two closures; order::block_mentions/names_in/names_in_block (:127-159) go, emit/host.rs :197 and send.rs :146 call names.nika directly; order::overlap_report’s Overlap-block closure (:192-200) becomes order.nika walking emit_walk::visited_in_block itself (drop the overlaps_in parameter), the Rust keeps the pauses callback; maps::Shape/FnMaps/From (:42-113) go: Seeds stores MpShape/MpFnMaps, own()/fixed() become mp_own/mp_fixed in maps.nika (seeds.rs :151-152), seeds_shape maps MpShape.within’s null to -1. The ledger writes of sharing::infer and maps::infer become ledger_infer_sharing(mut ledger, summaries) and ledger_infer_maps(mut ledger, found), the analyses staying in Rust.crates/nikaia/tests/it/ (they must compile unchanged; every kept forward keeps its signature): touch_sets.rs :18-19, :66-98 (order::{operation, accounted, verdict, Accounted}, touch::TouchOps), foreign_runtime.rs :25, :92-108, send.rs :48, :591-615 (order::accounted, Accounted, verdict), word_locks.rs :9, :19-26, :106, sharing.rs :27-61, :321-424, :741-789, :973 (sharing::{analyse, analyse_program, report, Decision, Count, Fallback, every_fallback}), overlap.rs :346, :385 (order::overlap_report). Grep contracts:: in crates/nikaia/tests/it/ once more after the build: clippy found P4b’s four test files only at the end.std counterparts: collections::BTreeMap/BTreeSet (BTreeSet has no extend, Seq no chain, #924: write loops); the touch order key is the tuple (String, String?, bool) in a BTreeMap, as the draft writes it. Every ledger, .stdout, .stderr and report text stays byte for byte..clone() where rustc asks), #916 (match on the field). Name each use in Body:. Do not touch crates/rs2nika/.locks, touch, throws into ledger_infer.nika (the three infers over CheckMethodCalls), locks.rs and throws.rs deleted, touch.rs keeps what Facts says; callers as above. lower-std: ledger_infer.rs is new, the index lowered.rs gains it. Commit contracts: the lock, touch and throws inference into Nikaia (L2-2), Part: #125.sharing, maps, order as above (ledger_infer_sharing, ledger_infer_maps, MpShape in Seeds, the overlap walk in order.nika). Commit contracts: the sharing, maps and order crossings shrink to forwards (L2-2), Part: #125. Report the self-hosting % (python3 scripts/self_hosting.py | tail -3, after adding ledger_infer.nika to COMPILER_NIKA locally and not committing that edit: name the row under Body:).A lowering defect met is fixed in the compiler as its own commit with a test (Fix, do not work around); if it is more than one step, stop and report it under Needs:.
nikaia test --project tests/compiler once, no --both-settings (no check_*/emit_* .nika changes, bootstrap L4c); cargo test --profile fast -p nikaia --lib contracts:: passes; it tests filtered on touch sharing word_locks overlap locks throws fails_with maps seeds send foreign_runtime plus the guard set of .claude/agents/builder.md, once, at the end, beside clippy; clippy clean; lower-std fixpoint in the worktree after the rebase. Changelog: none (a move).
An open design choice beyond the ones above; a ledger, .stderr, .stdout or report text that would change by one byte; a missing std call; an edit needed in a lane-1 file or in L2-1’s; an error in another lane’s file (docs/bootstrap.md, File ownership).
Read docs/builder-facts.md.
docs/bootstrap.md section 3)docs/builder-facts.md first. You work in the worktree /home/user/nikaia-lane2, not in /home/user/Nikaia (the driver’s builder works there; never edit, build or stage anything in it except your report file). L2-1 ran in this worktree before you: set up with cd /home/user/Nikaia && git fetch origin develop && (test -d /home/user/nikaia-lane2 || git worktree add --detach /home/user/nikaia-lane2 origin/develop); then cd /home/user/nikaia-lane2 && git status (another agent’s files left there are not yours: report them, do not build over them) and git checkout --detach origin/develop when the tree is clean. Build with cargo build --profile fast -p nikaia (incremental on, bootstrap.md section 3; CARGO_INCREMENTAL=0 only under 6 GB free); use only /home/user/nikaia-lane2/target/fast/nikaia, never another checkout’s binary.git add <files> only; commit after each step. Push: git fetch origin develop && git rebase origin/develop, rebuild, lower-std once more, commit any lowered file that changed (lowered: regenerate after rebase), then git push origin HEAD:develop; rejected: again, at most three times, then Pushed: rejected. A conflict in tools/lowered/*.rs or tools/lowered.rs is never merged by hand: git checkout --theirs -- <file>, git rebase --continue, rebuild, lower-std, commit.lower-std changed, yours and others’ (a compiler change re-lowers other files; that is correct in your tree). Do not edit docs/selfhosting-plan.md, docs/architect.md, docs/priorities.md, docs/bootstrap.md or scripts/self_hosting.py: rows for them go into Body: of your report.cargo fmt, cargo clippy --all-targets -- -D warnings, scripts/pre-push-check.sh, and the gate of .claude/agents/builder.md (#852).CHANGELOG.md, badges; no new NK code. New tests in Nikaia only; never the full suite. No foreground sleep, no polling; scripts in files.NIKAIA_CACHE_LIMIT=2G; at most three checkouts with target/ (C1, C2, C3); if df -h /home/user shows under 4 GB free, delete /home/user/nikaia-lane2/target and report blocked. At the end delete /home/user/nikaia-lane2/target/debug and /home/user/nikaia-lane2/target/release/nikaia-scratch (keep /home/user/nikaia-lane2/target/fast for the lane’s next brief) and report GB freed./home/user/Nikaia/docs/briefs/lane2-l22-contracts-crossings.md.report.md)Fields of docs/architect.md, Briefs and reports: Result: done|noop|partial|blocked (the bare word alone on that line: Result: done, never a summary after it, which cuts the batch, b869a 2026-10-27; Owner: is a question for the owner or none, never a role), Files, Commit, Body (optional, one paragraph for the commit message), Fixes, Pushed, Tests, Gate (green|red), Deviation, Found, Needs, Changelog, Owner, Disk freed, and for a move Rs2nika: (the kept N of M lines of rs2nika --score, then the three costliest hand edits; none for a task that moves no Rust). none where nothing, and then the bare word: Deviation: none (a note) cuts the batch (batch.nika compares exactly); a note goes into the commit message. Found: is only for a defect outside your change (it cuts the batch); a converter draft that came out wrong is no Found:, it is one of the costliest edits under Rs2nika:, which the converter lane reads (e12-4b 2026-10-27); how you solved your own step goes into the commit message. Deviation: is only a step of the brief built otherwise than written or not built (a choice the brief left to you, such as keep what X needs and say so, is no deviation: it goes into the commit message; nor is building two steps in one commit when every step is built, e12-3a 2026-10-27, nor a step another commit on develop already built, shown by your test failing with that commit’s change reverted, b889 2026-10-27: name the commit in Body:); how you verified (e.g. a test not run against the unfixed compiler) goes under Tests:. A noop says why under Tests: (what was probed), not under Deviation:. Final answer, one line: done <sha>, report <path> (or BLOCKED: ... / PUSH REJECTED ...).
Attribution: Co-Authored-By: Claude Opus 5.5 noreply@anthropic.com Claude-Session: https://claude.ai/code/session_01GFeMqxRbtUMiGVyDMxsvEq