Map needs `remove` and iteration for the kernel subsystem models

[maxinelevesque]

Map needs remove and iteration for the kernel models

The bounded Map lowering ships and works — conformance/map_kv.th is a real Map<u64,u64> over the Vec-of-pairs TMap backing, grounded by forge/tests/map_conformance.rs. This is about what the kernel subsystem models need on top of insert/get/contains_key/len.

Measured rather than guessed: every BTreeMap call site across the 19 model files in thermite-kernel, scored against the shipped surface. 257 sites, 150 covered.

What is not covered, and what that is worth

Four of the uncovered operations are idioms rather than capabilities, and need nothing:

op	sites	why it needs nothing
get_mut	48	read-modify-write on a &mut binding, which is get then insert in a value-semantics language
entry	4	get-or-insert, same
is_empty	2	len() == 0
clear	2	a fresh Map::new()

That leaves two genuine capabilities:

missing	sites	files
remove	24	frame 12, dma 4, irq 2, memory 2, services 2, smp 2
iteration (iter 17, values 8)	25	frame 10, memory 5, scheduler 4, smp 2, sync 2, services 2

Plus two singletons, clone (dma) and take (scheduler), which look like local refactors rather than requests.

Why these two specifically

remove is revocation and free. capability.rs revokes, frame.rs frees, irq.rs unroutes, dma.rs unpins. There is no way to express any of them with the current surface — a tombstone value would change what contains_key means, and len with it.

Iteration is traversal. scheduler.rs picks over its runqueue, frame.rs and memory.rs walk their extents, smp.rs fans out. These are the loops whose invariants are the interesting proofs.

The design question, which is yours rather than ours

remove looks mechanical against a Vec-of-pairs backing — swap-remove plus a spec_dom adjustment.

Iteration may not need an exec-position primitive at all. Every use we have is either a fold whose contract is a forall over the domain, or a search that could be expressed as such. If the spec surface can quantify over the map's domain, the contracts might be writable without an iterator, and the exec side could stay a bounded for over an index. That would be a much smaller change, and it is the kind of thing worth deciding before either of us writes code against the wrong shape.

Consumer-side effect

For a downstream kernel these two decide which subsystems can be modelled at all:

needs	subsystems
neither	the capability ledger — its only uncovered op is get_mut
remove	irq, device, dma
remove and iteration	frame, memory, smp, sync

Note this is independent of #122, which blocks all of them today for a different reason. The two are additive: #122 stops the structs from certifying, and this stops the maps inside them from being manipulated.

Happy to supply the per-call-site breakdown if it is useful for scoping.

🤖 Generated with Claude Code

[maxinelevesque]

Correction: the counts above are 2× too high, and len is not executable

Two errors in the original report, both mine. Corrected figures below.

The call counts were doubled. The script summed two overlapping regexes, so every self.field.method() matched both and counted twice. 130 call sites, not 257, with every per-operation figure exactly halved. Re-measured with receiver-type attribution and position deduplication:

insert 37 · get 27 · get_mut 24 · remove 12 · contains_key 11 · iter 9
values 4 · entry 2 · clone 1 · clear 1 · is_empty 1 · take 1

len is spec-only. I listed it as part of the shipped surface. In emit_one_map_wrapper it is pub open spec fn len(&self) -> nat, so the executable surface is three operations — insert, get, contains_key — not four. That also invalidates one of my "rewritable" claims: is_empty cannot become len() == 0 in exec position, so it is blocked too, though it is a single call site in memory.

What does not change is the shape of the request:

missing	sites	files
remove	12	dma, frame, irq, memory, services, smp
iteration (iter, values)	13	frame, memory, scheduler, services, sync

Together 8 of 19 model files. get_mut (24) and entry (2) remain rewritable as get/modify/insert since insert overwrites, so they are still not requests.

The framing I would use now: this is surface coverage, not existence. Map lowers and works; it is short two operations that the kernel models need.

Apologies for the noise on the original numbers.