Open and answer this issue on GitHub.
ready · opened 2026-10-29 · updated 2026-10-29 · 5 comments
agent: builder model: sonnet max_turns: 100 budget_usd: 20 —
Decided (owner, 2026-10-29, option 1 “full parity”): ADR-collections-1, Part III 17.1 std::collections (first paragraph). The options paper is in this issue’s history.
BTreeMap::entry and BTreeSet::extend are NK1171 today; so is HashSet::extend (the same gap, covered by ADR-collections-1 D2). HashMap::entry / Entry::or_insert, or_insert_with, and_modify and Vec::extend work.BTreeMap::entry has HashMap::entry’s contract (keeps the key; Entry[V] is one type, Rust’s btree_map::Entry below).extend on Vec, HashSet, BTreeSet takes a list, a set or a sequence of owned T, and keeps it; lowered to Rust’s extend.s.extend(xs.clone()) with xs used again lowers to s.extend(xs.iter().cloned()): no list in between.docs/builder-facts.md.crates/nikaia-std/std.contracts: collections::HashMap::entry (~2191), Entry::* (~2564-2586), collections::HashSet::* (~2300-2340), collections::BTreeSet::* (~2345-2390), collections::BTreeMap::* (~2393-2491), Vec::extend (~3368).crates/nikaia-std/src/tools/check_core_method.nika (~69-78, ~755, or_insert on an untyped map, ADR-285 D43), check_core_call_on.nika (~444, ~524, ~611). Check whether they name HashMap only.tests/accepted/700_map_and_modify.nika.Brief A (std, one builder):
std.contracts: collections::BTreeMap::entry (as HashMap::entry), collections::HashSet::extend, collections::BTreeSet::extend (keeps items); widen Vec::extend’s items to D3 (a list, a set or a sequence of owned T). If std.contracts cannot say “list, set or sequence” in one parameter type, report blocked with the probe (do not write three entries around it without saying so).entry/or_insert/and_modify are recognised by the map’s type name, accept collections::BTreeMap beside collections::HashMap.X.extend(Y.clone()) where Y is a list or set writes X.extend(Y.iter().cloned()).tests/compiler/tests/ (with .stdout, run through nikaia test --project tests/compiler):
a_btree_map_entry_or_insert_and_modify.nika: or_insert, or_insert_with, and_modify(..).or_insert(1) counting words, printed in key order.a_set_extends_from_a_list_a_set_and_a_drain.nika: BTreeSet and HashSet (HashSet printed sorted or by len()), extend(xs), extend(other), extend(xs.drain()), extend(xs.clone()) with xs printed after.a_vec_extends_from_a_set.nika: Vec::extend(set)..stderr test: extend(xs) then a use of xs is NK2105 (the set keeps it).lower-std, commit the generated diff with the change. Commit: Part of #950.Brief B (self-hosting rewrite, after A is on develop; may split in two by file):
for x in xs { s.insert(x) } / { s.insert(x.clone()) } in crates/nikaia-std/src/tools/*.nika becomes s.extend(xs) / s.extend(xs.clone()) (also for a Vec target: push loops are out of scope). Found again by the shape: a for NAME in SRC { line, the next line TARGET.insert(NAME) or .insert(NAME.clone()), then }. 158 on 0e644de, in 47 files; the list as of 2026-10-29 (lines move):
bounds_matched 188; bounds_shape 104,114; bounds_walk 2375,3514-3526 (5); buffers 342,906,1052,1071,1227,1243,1377,2004; cexport_model 917; check_access 163,169; check_arm_leaves 127,197,372; check_copies 170; check_core_args 328; check_core_call 389,396,403,422,426; check_core_flow 1122; check_core_pilot 98; check_core_places 334,338,357,361,435,450,454; check_core_stmt 1266,1270; check_function 92,95; check_host 812; check_items 917; check_may_fail 33,75; emit_calls 134; emit_function_body 73; emit_holes 305; emit_needs 82; emit_reach 65,141; emit_seeds 59,62,261; emit_tables 272,304,345; fold_bound 831,1268,1271,1801,1804,1807; keeps 167,171,184,211,223,229,240,256,272,278,290,307,322,694,748,925,934,963,991,1011; ledger_ops 236; lends 186; locks 60,179; logic_horn 193; logic_search 74; maps 237,240,1070,1077; modules 761; project_members 156,453,505,510,513; project_tests 125; prover_scope 237,385; prover_state 793,830; prover_walk 1257,1260,2322; tether 55; text_tiers 3402,3405,4835-4911 (16),5245,5571,5861,5885; throws 123,148,172,194,198,366,766,769; trust 365,479; type_rules 319,322; types 40,43,74,77,117,126,333; view_changes 170,230,233; views 1719,2169,2244,2861.
A source written xs.iter() becomes s.extend(xs.clone()). A loop whose body does more than the insert stays.entry where the key is given away anyway (owned, or a number): if !m.contains_key(k) { m.insert(k, v) } -> m.entry(k).or_insert(v) (or_insert_with(fn() { … }) where v is built or cloned), and the counter check_attributes.nika:316-320 (contains_key + get + insert) -> m.entry(name.clone()).and_modify(fn(n) { n += 1 }).or_insert(1) then read the count. A site that clones the key only on the insert path keeps its form (ADR-collections-1 section 5, Risk). 26 contains_key-then-insert sites on 0e644de: check_core_call_on 834,976; check_program 164; comptime_driver 162; emit_needs 171; fold_bound 621,1171,1461,1469; ledger 254; modules 388,393; prover_passes 152; sharing 510,593,1571,1578; surface 135,162; text_tiers 784,1766,3977,4829,4922; throws 133; ty 1780.lower-std, cargo clippy --all-targets -- -D warnings, tests/compiler tests touching the changed files. The last commit says Fixes #950.CLAUDE.md (commit own files by name, push fast-forward, no version raise, new tests in Nikaia), docs/briefs/common.part (disk, NIKAIA_CACHE_LIMIT=2G, report form).
Sites found by the architect (2026-10-29): a one-statement for x in xs { s.insert(x) } loop, the shape extend replaces. The target’s type is not checked per site (some may be a HashSet, which has the same question). Rewritten once this decision is built; until then a new one is not written (CLAUDE.md A missing form stops the work).
bounds_matched.nika: 188bounds_shape.nika: 104,114bounds_walk.nika: 2375,3514,3517,3520,3523,3526buffers.nika: 342,906,1052,1071,1227,1243,1377,2004cexport_model.nika: 917check_access.nika: 163,169check_arm_leaves.nika: 127,197,372check_copies.nika: 170check_core_args.nika: 328check_core_call.nika: 389,396,403,422,426check_core_flow.nika: 1097check_core_pilot.nika: 98check_core_places.nika: 334,338,357,361,435,450,454check_core_stmt.nika: 1249,1253check_function.nika: 92,95check_host.nika: 812check_items.nika: 917check_may_fail.nika: 33,75emit_calls.nika: 134emit_function_body.nika: 73emit_holes.nika: 305emit_needs.nika: 82emit_reach.nika: 65,141emit_seeds.nika: 59,62,261emit_tables.nika: 272,304,345fold_bound.nika: 831,1268,1271,1801,1804,1807keeps.nika: 167,171,184,211,223,229,240,256,272,278,290,307,322,694,748,925,934,963,991,1011ledger_ops.nika: 236lends.nika: 186locks.nika: 60,179logic_horn.nika: 193logic_search.nika: 74maps.nika: 237,240,1070,1077modules.nika: 761project_members.nika: 156,453,505,510,513project_tests.nika: 125prover_scope.nika: 237,385prover_state.nika: 793,830prover_walk.nika: 1257,1260,2322tether.nika: 55text_tiers.nika: 2980,2983,4317,4325,4335,4338,4341,4344,4350,4353,4356,4371,4374,4377,4384,4387,4390,4720,5037,5327throws.nika: 123,148,172,194,198,366,766,769trust.nika: 365,479type_rules.nika: 319,322types.nika: 40,43,74,77,117,126,333view_changes.nika: 167,227,230views.nika: 1719,2169,2244,2861Generated by Claude Code
Owner decision (2026-10-29): option 1, full parity. BTreeMap / BTreeSet get the same surface as HashMap / HashSet / Vec: extend, and entry with or_insert, or_insert_with, and_modify. The architect writes the ADR/spec sentence and the To build list; afterwards the 156 extend loops and the m[k] = (m[k] ?? 0) + 1 sites are rewritten.
Generated by Claude Code
Owner (2026-10-29): the reading of “full parity” that includes HashSet::extend is confirmed.
Generated by Claude Code
Step 7 (ca687c19, a0b13e61): 10 sites in check_program, fold_bound, throws and text_tiers now use entry. These are still open:
or_insert_with lambda, decision).let mut of a &mut).mut parameter).The sites kept by ADR-collections-1 section 5, and the ones that are not a fit for entry, are listed in docs/briefs/b950d.md.report.md.
Generated by Claude Code
The #949 files are done (d6ffb5bb). Only sharing 510 is left, and it waits on #973. The sites kept, with their reasons, are in docs/briefs/b950d.md.report.md and docs/briefs/b950e.md.report.md.
Generated by Claude Code