The Map is a Swiss table

TODO.org

@@ -1271,10 +1271,13 @@ value an unsigned compare waves through.
 lock the agent's listener thread may hold inside =dlopen=, so a program that
 should die could hang. Unconditionally rather than only under =--dev=.
 
-** TODO A Map's bounds check and the stale-container failure still die
+** DONE A Map's bounds check and the stale-container failure still die
-Deliberate for the stale case — the region the container lived in was released and
+CLOSED: [2026-09-25]
-there is no frame to go back to that would not read freed memory. The Map path was
+A Map has no bounds check: =get= and =map-remove= answer =None= for an absent key
-left alone rather than converted half-way.
+and nothing on the map path indexes by a number, so there was nothing to convert.
+The stale-container failure keeps dying — the region was released and there is no
+frame to go back to that would not read freed memory. Rules out a signalled
+condition on the stale path.
 
 ** DONE Six trap paths park instead of killing the session
 CLOSED: [2026-09-18]
@@ -1334,15 +1337,17 @@ docs/BUILT.md, "Three amendments to a frozen spec".
 ** DONE Map removal costs a backward-shift loop
 Removal landed, with the loop the spec predicted as its cost. Deferring it was
 what had kept the implementation free of tombstones and of Odin's
-backward-shift loop; taking it is taking the loop.
+backward-shift loop; taking it is taking the loop. Superseded by the Swiss table,
+which removes by tombstone and moves nothing.
 
-** NEXT The Map is slower than CPython's dict at a million entries
+** DONE The Map is slower than CPython's dict at a million entries
-Decided 2026-09-25: build the Swiss-table layout, one metadata byte a slot. Measured against the current Map at small, game and large sizes before and after.
+CLOSED: [2026-09-25]
-Keys, values and hashes are three separate runs, so a lookup that misses
+The Map is a Swiss table: one control byte a slot, key and value side by side,
-everything costs three cache misses where a compact dict costs two. One byte of
+groups of eight probed as one 64-bit word, seven-eighths load, removal by
-metadata a slot — the Swiss-table arrangement — is the known answer and is not
+tombstone with a same-capacity rebuild to sweep them. Header, entry points and
-built. The crossover is somewhere between ten thousand and a million and nobody
+iteration contract unchanged. Rules out Robin Hood, the backward shift and
-has found it.
+separate key and value runs; SSE2 groups are not built. See docs/BUILT.md, "The
+Map is a Swiss table".
 
 ** DONE dyn maps and interned keywords
 CLOSED: [2026-09-20]

docs/BUILT.md

@@ -3088,6 +3088,10 @@ restriction under it.
 
 ### The three properties that were the point
 
+**Superseded.** The table below is no longer a Robin Hood map: it is a Swiss table, and "The Map is a Swiss table"
+further down says what replaced what and why. This section and the next are kept for the reasoning they record; the
+hash-and-equality pair, the key restrictions and the header are unchanged.
+
 Odin's header states them and they are why it was the thing to follow (`base/runtime/dynamic_map_internal.odin`).
 
 - **Open-addressed Robin Hood hashing at a 75% load factor.** No buckets and no per-entry allocation: one block holds
@@ -3104,14 +3108,11 @@ Odin's header states them and they are why it was the thing to follow (`base/run
 
 ### Two departures from Odin, both deliberate
 
-**There are still no tombstones, now that removal exists.** A slot is empty or occupied and nothing else, and
+**Removal was a backward shift, and is now a tombstone.** While the table was Robin Hood, a slot was empty or occupied
-`flan_map_remove` keeps it that way by shifting the run back over the hole rather than marking it. Odin does the
+and `flan_map_remove` shifted the run back over the hole. The Swiss table has a third control state, deleted, and
-opposite, and this paragraph used to say otherwise: read out of
+empties a slot outright only where no probe can have passed through it; see "The Map is a Swiss table". What
-`base/runtime/dynamic_map_internal.odin`, `map_erase_dynamic` sets a tombstone bit and leaves the repair to the next
+`spec-memory.md` still defers is unchanged: move-aware lookup and owned entries. A removed value is copied out, and
-insert, which is why Odin's *insert* carries a backward-shift loop and its every lookup tests for a tombstone. The
+nothing is dropped.
-trade is the usual one — erase is O(1) there and the shift is here, and the lookups, which outnumber the removals,
-pay nothing. What `spec-memory.md` still defers is the rest of its sentence: move-aware lookup and owned entries. A
-removed value is copied out, and nothing is dropped.
 
 **The header does not tag the capacity into the data pointer.** Odin stuffs `log2cap` into the low six bits because
 its `Raw_Map` must be three words. This header already carries an allocator, a generation and an epoch, so the tagging
@@ -3119,10 +3120,10 @@ would buy nothing, cost a mask on every access, and — the part that actually m
 block being 64-byte aligned. Alignment is *requested*; an arena whose base is not cache-aligned now gives a slower map
 rather than a wrong one.
 
-The header is six words, 48 bytes, the same as a `Vec`'s and for the same reason: a layout that changes with a build
+The header is five words, 40 bytes, the same as a `Vec`'s and for the same reason: a layout that changes with a build
 flag can disagree across the reload boundary.
 
-    data  len  log2cap  allocator  gen  epoch
+    data  len  log2cap  allocator  epoch
 
 ### The hash and equality pair, and why most key types do not get one
 
@@ -3232,7 +3233,7 @@ Measured on this machine, `i64` to `i64`, against CPython 3.13's dict on the sam
 left out. Both are waiting on memory there, and this layout waits longer: keys, values and hashes are three separate
 runs, so a lookup that misses everything takes three cache misses where a compact dict takes two, and the hash run is a
 full eight bytes a slot. Cell packing buys probe locality, which is a win while the hash run is resident and a loss
-once nothing is. One byte of metadata a slot — the Swiss-table arrangement — is the known answer and is not built.
+once nothing is. One byte of metadata a slot — the Swiss-table arrangement — is the known answer, and the next section is it being built.
 
 The path from 35 ns to 18 ns (the cache-resident floor, at 500 entries) was **profiled, and the first two guesses were
 both wrong**: the per-slot cell division and the block-size divisions were each replaced first and neither moved the
@@ -3243,10 +3244,80 @@ twice per lookup; and the seed stopped being a five-multiply avalanche on the cr
 again immediately after. `64/size` is a table, which is Odin's `Map_Cell_Info` by another route — Odin precomputes it
 per type because the probe loop must not divide, and here the sizes arrive as ordinary arguments.
 
-What remains at 18 ns is the type erasure itself: a non-inlinable call into the runtime and two non-inlinable indirect
+What remained at 18 ns was the type erasure itself: a non-inlinable call into the runtime and two non-inlinable indirect
 calls to the pair. That is the trade `spec-memory.md` chose deliberately — "It is type-erased on purpose… No generics
 are involved, and none are needed" — and monomorphisation is what would buy it back, at the cost the spec declined.
 
+### The Map is a Swiss table
+
+The Robin Hood table above lost to CPython's dict at a million entries: three separate runs and an eight-byte hash a
+slot. It is replaced by a Swiss table, and the header, every entry point's signature, the hash-and-equality pair and
+the iteration contract are unchanged, so the change is confined to `runtime/flan_rt.c`. The layout and the removal rule
+are described there; what follows is what the code cannot say.
+
+- **Empty is zero** — Zig's encoding (`lib/std/hash_map.zig`, `Metadata`: free 0, tombstone 1, a used bit on top) — so
+  a zeroed control run is an empty map.
+- **Groups are eight bytes read as one integer**, not SSE2's sixteen: portable to every target the runtime compiles
+  for, and nothing measured asks for the wider group.
+- **Key and value share a slot** because a hit then costs two cache misses rather than three. The runtime is not told
+  alignments; the largest power of two dividing each size bounds them.
+- **The head of the block holds three words** — growth left, slot stride, value offset — because the five-word header
+  is the emitter's layout too. The stride is stored rather than recomputed because recomputing it per call cost about a
+  tenth of a cache-resident lookup.
+- **The 25/32 threshold** for sweeping deleted slots at the same capacity rather than doubling, and the rule for
+  emptying a removed slot outright, were written from memory of abseil's table, not read from its source; no abseil
+  clone is on this machine. `map-remove.flan` row 7 is what holds them: it churns a map at a steady size under an
+  allocator budget that a doubling would exceed.
+
+#### Measured
+
+`i64` to `i64`; keys present are `2i`, absent `2i + 1`. *insert* fills a fresh map with no `reserve`, to two million
+inserts; *hit* and *miss* are four million lookups cycling the keys; *remove* removes every key of a filled map, to two
+million. Each pass counts its wrong answers: a map passed by value to a filling function takes its grows in the
+callee's copy of the header, and a benchmark written that way measures an empty map. CPython is Python 3.13.9,
+`dict.get` and `dict.pop`.
+
+The figure is the **minimum of nine runs**, the two Flan binaries run alternately and the Python script in a separate
+nine-run pass, because this machine is shared — it carried a load average near 20 throughout, from other lanes' test
+suites — and a minimum measures the program rather than the neighbours. Both Flan binaries are `-O2`. The magnitudes
+carry that load: across three nine-run passes the Robin Hood column moved by as much as half (a 100k hit read 51, 83
+and 35 ns). What held is the ordering — the Swiss table ahead of the Robin Hood table in every cell of every pass,
+and ahead of CPython in every cell — and that is the claim to reproduce. Nanoseconds per operation:
+
+| Entries | Op | Robin Hood | Swiss | CPython dict |
+|---|---|---|---|---|
+| 16 | insert | 74.5 | 30.5 | 46.3 |
+| | hit | 20.0 | 9.8 | 83.1 |
+| | miss | 16.1 | 8.0 | 100.5 |
+| | remove | 23.3 | 15.4 | 69.0 |
+| 1k | insert | 80.9 | 30.0 | 57.4 |
+| | hit | 22.2 | 9.7 | 124.6 |
+| | miss | 15.9 | 7.8 | 128.3 |
+| | remove | 24.5 | 14.8 | 91.9 |
+| 10k | insert | 112.4 | 45.5 | 85.5 |
+| | hit | 29.6 | 10.5 | 134.9 |
+| | miss | 26.5 | 8.5 | 125.3 |
+| | remove | 33.2 | 17.6 | 99.7 |
+| 100k | insert | 204.4 | 47.6 | 123.6 |
+| | hit | 35.3 | 16.1 | 133.6 |
+| | miss | 30.4 | 14.4 | 128.4 |
+| | remove | 40.6 | 22.9 | 98.4 |
+| 300k | insert | 199.4 | 73.0 | 128.7 |
+| | hit | 69.9 | 25.9 | 118.0 |
+| | miss | 39.8 | 10.9 | 138.2 |
+| | remove | 116.8 | 36.9 | 94.3 |
+| 1M | insert | 454.2 | 138.5 | 151.5 |
+| | hit | 147.1 | 78.4 | 120.3 |
+| | miss | 88.2 | 14.6 | 125.2 |
+| | remove | 152.0 | 74.5 | 91.5 |
+
+**The crossover.** Against CPython the Robin Hood table lost on insert at every size, on remove from between 100k and
+300k, and on hits between 300k and 1M. The Swiss table is ahead of both in every cell. CPython hashes a small integer
+to itself, so this key pattern walks its table in order and the margin at a million is narrower than it looks.
+
+Control bytes over separate key and value runs were measured and not kept: level with the final layout to 100k, behind
+from 300k (100 ns a hit against 78 at a million).
+
 ## Unions, and the tag they carry
 
 `defdata` parsed and its shape was checked long before this; naming the type (`check.ml:312`) and constructing a
@@ -4488,10 +4559,8 @@ function.
 ```
 
 **The cursor is a slot index the caller owns, and there is no iterator struct** because there is nothing for one to
-hold. A map has no tombstones — removal shifts the run back instead of marking a hole — so a slot is either empty or
+hold: a slot's control byte says whether it is full, and the position is the whole of the state. A removal moves
-occupied and the position is the whole of the state. What a cursor does *not* survive is a removal taken while it is
+nothing, so a cursor survives one; what it does not survive is a put that rebuilds the block. The cursor starts at 0, comes back one past the entry just answered, and is left
-in flight: the shift moves entries to lower slots, and a cursor already past them steps over entries it has not
-answered, the same bargain a put that grows already makes. The cursor starts at 0, comes back one past the entry just answered, and is left
 at `cap` by the call that answers false, so a spent cursor keeps answering false rather than wrapping.
 
 **Three out-pointers and not a returned pair**, because there are no tuples. An `(Option K)` would answer half an
@@ -4501,11 +4570,10 @@ that is written through on the way out.
 **It is the one map entry point that carries neither a hash nor an equality function.** Walking asks nothing about a
 key. The two sizes are still there, because the runtime is type-erased and the block geometry is computed from them.
 
-**The layout, restated, because it is the thing to get wrong here.** `data` is *one* allocation laid out
+**The layout, restated, because it is the thing to get wrong here.** `data` is *one* allocation: a three-word head,
-keys | values | hashes | scratch, each run cell-packed to a cache line — the arrangement the Valgrind lane described
+the control bytes, then the slots, each slot a key and its value side by side at the stride the head records. A slot is
-while explaining why a probe overrun is not observable. A key is reached through `flan_cell_at` and never as
+full when its control byte has the top bit set, and a key is reached as `slots + i * stride`, never as
-`ks + i * ksize`. The hashes are the exception `flan_map_clone` already relies on: an 8-byte element packs 8 to a
+`ks + i * ksize`.
-64-byte cell with nothing left over, so `g.hs[i]` is the right index and a flat one.
 
 **Order is block order**, which is the hash's order and not the insertion's, and it changes when the map grows.
 `programs/map-iter.flan` is therefore written entirely in sums, counts and lengths — every claim in it is order-free,
@@ -5732,10 +5800,10 @@ IR (which is also why `--no-bounds-checks` never reached it), so both grew a tra
 `Emit`'s `Rt` arm guards those two symbols and no others — they are the only ones in that family that can transfer;
 everything else there is arithmetic over a container header.
 
-**A `Map`'s bounds and a `Vec`'s stale-allocator check still die.** `flan_vec_stale_fail` is a different kind of
+**A `Vec`'s stale-allocator check still dies, and so does a `Map`'s.** `flan_vec_stale_fail` is a different kind of
 failure — the region a container lived in was released, and there is no frame to go back to that would not read freed
-memory — and the map path was left alone rather than converted half-way. Written down here so it is a known edge
+memory. A `Map` has no bounds check to convert: `get` and `map-remove` answer `None` for an absent key and nothing on
-rather than a discovery.
+the map path indexes by a number, so the stale check is the only map failure that dies.
 
 
 ## An address answers with a type, and nothing grew a tag word

lib/check.ml

@@ -7629,7 +7629,7 @@ and named_call ?(qualified = false) ctx ~want loc name args =
        let attempt, note =
          match target.Tast.ty with
          (* For a map the number is entries, not slots: the runtime sizes the
-            block so that [n] still sits under the 75% load factor, which is
+            block so that [n] still sits under the load factor, which is
             the only reading of "room for n" that does not reallocate on the
             nth put. *)
          | Types.Map (k, v) ->

lib/emit.ml

@@ -334,7 +334,7 @@ let rec ll (t : Types.t) =
      the Vec's address — so the shape is here only so that a slot, a struct
      field and a copy in the IR are the right number of bytes. *)
   | Types.Vec _ -> "%vec"
-  (* data + len + log2cap + allocator + gen + epoch. Six words, exactly as the
+  (* data + len + log2cap + allocator + epoch. Five words, as many as the
      Vec's, and read here for exactly the same reason: nothing in this file
      touches a field of one — every operation is a runtime call taking the
      map's address — so the shape exists only so that a slot, a struct field
@@ -4379,7 +4379,7 @@ let header = {|; Generated by flan. The layout is C's: no object headers anywher
 ; (Vec T), spec-memory.md. The element type is nowhere in it: the runtime is
 ; type-erased and every operation is handed size and align at its call site.
 %vec = type { ptr, i64, i64, ptr, i64 }
-; (Map K V), spec-memory.md — Odin's open-addressed Robin Hood map. Neither key
+; (Map K V), spec-memory.md — an open-addressed Swiss table. Neither key
 ; nor value type appears in it, for the same reason: one type-erased runtime,
 ; handed the two sizes and a hash/equality pair at each call site.
 %map = type { ptr, i64, i64, ptr, i64 }

spec-memory.md

@@ -20,7 +20,7 @@ facility (see plan.org, "Managed classes").
 | `[n T]`   | n contiguous `T`  | copies     | no (inline)  | —         |
 | `[T]`     | ptr + len         | copies the *view* | no    | —         |
 | `(Vec T)` | ptr + len + cap   | **moves**  | yes          | stored    |
-| `(Map K V)` | open-addressed, flat key/value arrays | **moves** | yes | stored |
+| `(Map K V)` | open-addressed, one control byte a slot, key and value side by side | **moves** | yes | stored |
 
 - `[n T]` is a value. It lives wherever it is declared, copies on assignment and
   on pass-by-value, and is what `defconst colors [4 u32] ...` and

test/programs/map-iter.flan

@@ -82,7 +82,7 @@
       (print chars) (print " ") (print xs) (print " ") (print ys) (println ""))
     (free m)))
 
-;; Growth past the 75% threshold rehashes into a new block, so this walks a map
+;; Growth past the load factor rehashes into a new block, so this walks a map
 ;; whose layout is nothing like its insertion order and at a capacity several
 ;; doublings past the minimum.
 (defn after-growth [] ()

test/programs/map-remove.flan

@@ -1,17 +1,26 @@
 ;;;; (map-remove m k) — the operation a Map has been missing.
 ;;;;
-;;;; Removal is the one map operation that can break the *other* ones: Robin
+;;;; Removal is the one map operation that can break the *other* ones: a
-;;;; Hood lookups stop at the first empty slot, so a hole punched in the middle
+;;;; lookup stops at the first group of slots holding an empty one, so a slot
-;;;; of a probe run hides every entry after it, and the entries it hides are
+;;;; emptied in the middle of a probe sequence hides every entry placed past
-;;;; found by no test that only removes and asks about what it removed. So the
+;;;; it, and the entries it hides are found by no test that only removes and
-;;;; rows below are mostly about the survivors.
+;;;; asks about what it removed. So the rows below are mostly about the
+;;;; survivors.
 ;;;;
-;;;; Odin marks a tombstone and repairs on the next insert; this shifts the run
+;;;; A removed slot is marked deleted, and emptied outright only where no probe
-;;;; back and stays tombstone-free, which is the arrangement the rest of the
+;;;; can have passed through it. A version that emptied every removed slot
-;;;; file already assumed. A version that punched the hole and left it passes
+;;;; passes row 1 and fails row 3; a version whose deleted slots were never
-;;;; row 1 and fails row 3.
+;;;; swept grows without end under row 7.
 (defstruct Cell [x i32 y i32])
 
+;; Row 7's allocator and its count of refusals. Globals, because a handler
+;; cannot see the locals of the function that established it.
+(defonce churn-alloc Allocator)
+(defonce churn-refusals i64)
+;; Row 7's reference: a global array rather than a Vec, because a Vec would
+;; take its block from the same process heap the budget is counting.
+(defonce churn-ref [512 i64])
+
 (defn main [] i32
   ;; (1) The value comes back, the length drops, and the key is gone. An
   ;; absent key is None and changes nothing — the same answer get gives, since
@@ -41,9 +50,8 @@
 
   ;; (3) The survivors, which is the row that matters. 2000 entries is eight
   ;; grows, so the runs are long and interleaved; removing the even keys and
-  ;; then asking after every odd one is asking whether any probe run was cut.
+  ;; then asking after every odd one is asking whether any probe sequence was
-  ;; A backward shift that stopped one slot early loses entries here and
+  ;; cut.
-  ;; nowhere else.
   (let [m (map-new i32 i64)]
     (dotimes [i 2000] (put m i (* (i64 i) 3)))
     (let [taken 0]
@@ -90,9 +98,7 @@
     (print (length s)) (println "")                  ; 1
     (free s))
 
-  ;; (5) Iteration after removals answers exactly the survivors. The cursor is
+  ;; (5) Iteration after removals answers exactly the survivors.
-  ;; started fresh — a cursor held *across* a removal is invalidated by the
-  ;; shift, the same way a put that grows invalidates one.
   (let [m (map-new i32 i32)]
     (dotimes [i 100] (put m i i))
     (dotimes [i 100] (if (= 0 (% i 3)) (map-remove m i)))
@@ -118,4 +124,64 @@
         (match (get t 299) (Some v) (do (print v) (println "")) None (println "?"))  ; 598
         (print (has-key? t 298)) (println "")))      ; false
     (free-all ar))
+
+  ;; (7) Churn at a steady size, checked against a plain array. Keys are drawn
+  ;; from 512 and the map holds about two thirds of them, so removals leave
+  ;; deleted slots that inserts must reuse and rebuilds must sweep. Every get is
+  ;; checked against the array, and at the end so is the length and a full walk.
+  ;;
+  ;; The process heap is given a budget of 20000 bytes, with nothing else of
+  ;; this program's live on it. An i32 key and an i64
+  ;; value make a 16-byte slot, so the 512-slot block is 8768 bytes and a
+  ;; rebuild at that size holds two of them, 17536; a grow to 1024 slots holds
+  ;; 8768 and 17472 at once and goes over. The entries never need more than 512
+  ;; slots, so a refusal means deleted slots were used up and the table doubled
+  ;; instead of sweeping them — which is what a version that never swept them
+  ;; does. The handler lets it through, counts it, and the count is printed.
+  (set churn-alloc (heap-allocator))
+  (set-alloc-budget churn-alloc 20000)
+  (handler-bind
+   [(StorageExhausted [c]
+      (set churn-refusals (+ churn-refusals 1))
+      (set-alloc-budget churn-alloc (* 2 (alloc-budget churn-alloc)))
+      (invoke-restart 'retry))]
+  (let [m (map-new i32 i64 churn-alloc)
+        x (u64 12345)
+        bad 0
+        live 0]
+    (dotimes [i 512] (set (at churn-ref i) (i64 -1)))
+    (dotimes [step 200000]
+      (set x (+ (* x (u64 6364136223846793005)) (u64 1442695040888963407)))
+      (let [k (i32 (% (>> x 33) (u64 512)))
+            op (i32 (% (>> x 20) (u64 4)))]
+        (if (< op 2)
+          (do (if (< (at churn-ref k) 0) (set live (+ live 1)))
+              (put m k (i64 step))
+              (set (at churn-ref k) (i64 step)))
+          (if (= op 2)
+            (match (map-remove m k)
+              (Some v) (do (if (not (= v (at churn-ref k))) (set bad (+ bad 1)))
+                           (set (at churn-ref k) (i64 -1))
+                           (set live (- live 1)))
+              None (if (>= (at churn-ref k) 0) (set bad (+ bad 1))))
+            (match (get m k)
+              (Some v) (if (not (= v (at churn-ref k))) (set bad (+ bad 1)))
+              None (if (>= (at churn-ref k) 0) (set bad (+ bad 1))))))))
+    (print bad) (println "")                         ; 0
+    (print (= (length m) (i64 live))) (println "")   ; true
+    (let [cur (i64 0)  k 0  v (i64 0)  seen 0]
+      (while (map-next m (addr cur) (addr k) (addr v))
+        (set seen (+ seen 1))
+        (if (not (= v (at churn-ref k))) (set bad (+ bad 1))))
+      (print (= seen live)) (println "")             ; true
+      (print bad) (println ""))                      ; 0
+    ;; Removing while walking visits every survivor once: nothing moves.
+    (let [cur (i64 0)  k 0  v (i64 0)  seen 0]
+      (while (map-next m (addr cur) (addr k) (addr v))
+        (set seen (+ seen 1))
+        (map-remove m k))
+      (print (= seen live)) (println "")             ; true
+      (print (length m)) (println ""))               ; 0
+    (free m)))
+  (print churn-refusals) (println "")                ; 0
   0)

test/programs/maps.flan

@@ -1,7 +1,7 @@
 ;;;; (Map K V) — spec-memory.md, step 4 of the container build order.
 ;;;;
-;;;; Odin's map: open-addressed Robin Hood hashing at a 75% load factor, with
+;;;; An open-addressed Swiss table: one control byte a slot, key and value side
-;;;; cache-line cell packing. Every claim below is one a plausible wrong
+;;;; by side. Every claim below is one a plausible wrong
 ;;;; version gets wrong, and the numbers differ per failure so a single wrong
 ;;;; answer names its own cause.
 (defstruct Cell  [x i32 y i32])

test/test_acceptance.ml

@@ -3968,8 +3968,7 @@ level "1"
 
     (* ── (Map K V), spec-memory.md step 4 ──────────────────────────
 
-       Odin's map: open-addressed Robin Hood hashing at a 75% load factor with
+       An open-addressed Swiss table, one control byte a slot. maps.flan is seven claims, each one a plausible
-       cache-line cell packing. maps.flan is seven claims, each one a plausible
        wrong version gets wrong, and the numbers differ per failure.
 
        The two worth naming, because nothing else in the suite would catch
@@ -4008,9 +4007,9 @@ level "1"
     outputs "map iteration" "programs/map-iter.flan" map_iter_out;
     outputs ~opt:"-O0" "map iteration, -O0" "programs/map-iter.flan" map_iter_out;
 
-    (* Removal, which is the operation that can break the others. A Robin Hood
+    (* Removal, which is the operation that can break the others. A probe
-       probe stops at the first empty slot, so a hole left in the middle of a
+       stops at the first group holding an empty slot, so a slot emptied in
-       run hides every entry past it — and the hidden ones are exactly what a
+       the middle of a probe sequence hides every entry past it — and the hidden ones are exactly what a
        test that only asks after what it removed never looks at. Hence the
        third row: 2000 entries, the even keys taken out, and then every odd one
        asked for. A removal that punched the hole and left it answers row one
@@ -4021,7 +4020,8 @@ level "1"
        into the wrong half of it. *)
     let map_remove_out =
       "100\n1\nfalse\ngone\n1\n0\n77\n1\n1000\n1000\n0\n0\n2000\n\
-       709\nfalse\ntrue\n399\n1\ntrue\n1\n66\n0\n66\n150\n598\nfalse\n"
+       709\nfalse\ntrue\n399\n1\ntrue\n1\n66\n0\n66\n150\n598\nfalse\n\
+       0\ntrue\ntrue\n0\ntrue\n0\n0\n"
     in
     outputs "map removal" "programs/map-remove.flan" map_remove_out;
     outputs ~opt:"-O0" "map removal, -O0" "programs/map-remove.flan"

test/test_valgrind.ml

@@ -275,10 +275,11 @@ let corpus =
    down: [check_at] is behind the flag and so is *half* of [check_slice] — the
    [hi <= len] compare — while its [lo <= hi] stays, because that one is the
    claim that a slice's length word is a count and not a bounds check at all.
-   A Vec's and a Map's bounds checks are not behind it either: they live inside
+   A Vec's bounds check is not behind it either: it lives inside flan_vec_at,
-   flan_vec_at and the map probe in flan_rt.c, are plain C, and run in every
+   is plain C, and runs in every build. A Map has no bounds check to lower —
-   build. So the flag lowers the guard on indexing a fixed array or a slice,
+   its probe is masked to the capacity and an absent key is None. So the flag
-   and on nothing else. These are the programs where that distinction reaches
+   lowers the guard on indexing a fixed array or a slice, and on nothing
+   else. These are the programs where that distinction reaches
    heap storage. *)
 let unchecked_subset =
   [ "programs/allocators.flan", [];