Skip to content

stdlib.collect

Collections: Adaptive Replacement Cache

Generated from v0.60.1. 61 source files, 565 documented symbols.

arc.xi

fn arc_new(capacity: Int) -> ArcCache

Create a new ARC cache holding at most capacity entries. Params: capacity - maximum number of cached entries (clamped to >= 1). Returns: an empty ArcCache. Complexity: O(1).

  • Postcondition: result.capacity >= 1
  • Postcondition: result.p == 0
fn arc_get(c: &mut ArcCache, key: Int) -> Option[Int]

Get the value for a key, promoting it on a hit. None on a miss. Params: c - the cache; key - Int key. Returns: Some(value) if cached, None otherwise. Complexity: O(n) (linear scan of the four lists).

  • Postcondition: result.is_some == arc_contains(c, key)
fn arc_put(c: &mut ArcCache, key: Int, value: Int)

Insert or update key -> value, adapting the cache to the workload. Params: c - the cache; key - Int key; value - Int value. Complexity: O(n) (linear scan of the four lists).

  • Postcondition: arc_contains(c, key)
fn arc_contains(c: &mut ArcCache, key: Int) -> Bool

Check whether a key is present (does not change recency). Params: c - the cache; key - Int key. Returns: true if the key is cached. Complexity: O(n) (linear scan of T1 and T2).

  • Postcondition: result == true => arc_size(c) > 0
fn arc_size(c: &mut ArcCache) -> Int

Number of entries currently cached. Params: c - the cache. Returns: the number of cached key/value pairs. Complexity: O(1).

  • Postcondition: result >= 0
fn arc_capacity(c: &mut ArcCache) -> Int

Maximum number of entries the cache can hold. Params: c - the cache. Returns: the configured capacity. Complexity: O(1).

  • Postcondition: result >= 0



avl.xi

type Avl

Self-balancing AVL tree of unique Int elements. Flat-arena representation (the established collect/ pattern, shared with collect.tree): nodes live in parallel Vec[Int]s addressed by a root index; -1 is the "no node" sentinel. heights[i] holds the height of node i (leaf = 1, empty subtree = 0); every insert/remove rebalances via single/double rotations so |balance factor| <= 1 holds on every node. Removed nodes become unreachable arena entries.

Field Type
root Int
keys Vec[Int]
left Vec[Int]
right Vec[Int]
heights Vec[Int]
fn avl_new() -> Avl

Create a new empty AVL tree. O(1).

  • Postcondition: result.root == -1
fn avl_insert(t: &mut Avl, value: Int)

Insert value, rebalancing as needed. Duplicates are ignored. O(log n).

  • Postcondition: avl_contains(t, value)
fn avl_contains(t: &Avl, value: Int) -> Bool

True if value is present. O(log n).

  • Postcondition: result == true => t.root != -1
fn avl_remove(t: &mut Avl, value: Int)

Remove value, rebalancing as needed. Missing values are a no-op. O(log n).

  • Postcondition: avl_contains(t, value) == false
fn avl_min(t: &Avl) -> Option[Int]

Smallest value, or None if the tree is empty. O(log n).

  • Postcondition: result is None => t.root == -1
  • Postcondition: result is Some(_) => t.root != -1
fn avl_max(t: &Avl) -> Option[Int]

Largest value, or None if the tree is empty. O(log n).

  • Postcondition: result is None => t.root == -1
  • Postcondition: result is Some(_) => t.root != -1
fn avl_height(t: &Avl) -> Int

Height of the tree; an empty tree has height 0. O(1).

  • Postcondition: result >= 0



bheap.xi

fn bheap_new() -> PHeap

Create a new empty binary heap. Returns: an empty PHeap-backed heap. Complexity: O(1).

  • Postcondition: result.root == -1
fn bheap_push(h: &mut PHeap, value: Int)

Insert an element. Params: h - the heap; value - Int element to insert. Complexity: O(log n) amortized.

  • Postcondition: bheap_len(h) >= 1
fn bheap_pop(h: &mut PHeap) -> Option[Int]

Remove and return the top (minimum) element. None if empty. Params: h - the heap. Returns: the minimum element, or None when the heap is empty. Complexity: O(log n) amortized.

  • Postcondition: result is None => bheap_len(h) == 0
fn bheap_peek(h: &PHeap) -> Option[Int]

Peek at the top (minimum) element. None if empty. Params: h - the heap. Returns: the minimum element without removing it, or None when empty. Complexity: O(1).

  • Postcondition: result is None => bheap_len(h) == 0
fn bheap_len(h: &PHeap) -> Int

Number of elements. Params: h - the heap. Returns: the number of elements currently stored. Complexity: O(n) (reachable-node walk).

  • Postcondition: result >= 0



bitmap.xi

type Bitmap

Compact set of bits indexed 0..n-1 with O(1) test/set/clear/flip. Bits are packed into UInt8 bytes (the pattern proven in collect.hash); the padding bits of the last byte are never reported. Index arithmetic uses only small masks (0..255) so the compiler's large-Int AND bug (BUG 25 #7) cannot be hit. Out-of-range positions are ignored (documented).

Field Type
bytes Vec[UInt8]
nbits Int
fn bitmap_new(n: Int) -> Bitmap

Create a bitmap of n bits, all clear. A size below 1 yields 0 bits. O(n/8).

  • Postcondition: result.nbits >= 0
  • Postcondition: n >= 0 => result.nbits == n
fn bitmap_set(b: &mut Bitmap, pos: Int)

Set the bit at pos. Positions outside [0, n) are ignored. O(1).

  • Postcondition: pos < 0 || pos >= b.nbits || bitmap_test(b, pos)
fn bitmap_clear(b: &mut Bitmap, pos: Int)

Clear the bit at pos. Positions outside [0, n) are ignored. O(1).

  • Postcondition: pos < 0 || pos >= b.nbits || bitmap_test(b, pos) == false
fn bitmap_test(b: &Bitmap, pos: Int) -> Bool

Test the bit at pos. Positions outside [0, n) read as false. O(1).

  • Postcondition: pos < 0 || pos >= b.nbits => result == false
fn bitmap_flip(b: &mut Bitmap, pos: Int)

Flip the bit at pos. Positions outside [0, n) are ignored. O(1).

  • Postcondition: pos < 0 || pos >= b.nbits || b.nbits >= 1
fn bitmap_count(b: &Bitmap) -> Int

Number of set bits among the first nbits positions. O(n).

  • Postcondition: result >= 0
fn bitmap_first_set(b: &Bitmap) -> Option[Int]

Index of the first set bit, or None when the bitmap is empty. O(n).

  • Postcondition: result is None => bitmap_count(b) == 0
  • Postcondition: result is Some(_) => bitmap_count(b) >= 1



blockingqueue.xi

type BlockingQueue

Blocking queue (Int items) with a fixed capacity. Pure-XIOM data structure: there are no OS threads, so the blocking variants degrade to immediate returns (bq_push -> false when full, bq_pop -> None when empty) while keeping the same contract as a threaded implementation. bq_close wakes all waiters (a no-op here) and makes push fail while pop drains the remainder.

Field Type
buf Vec[Int]
head Int
capacity Int
closed Bool
fn blocking_queue_new(capacity: Int) -> BlockingQueue

Create a blocking queue with capacity slots. Params: capacity - maximum number of queued items (clamped to >= 1). Returns: a new, open blocking queue. Complexity: O(1).

  • Postcondition: result.capacity >= 1
  • Postcondition: result.closed == false
fn bq_push(q: &mut BlockingQueue, item: Int) -> Bool

Enqueue item. Blocks while full in a threaded implementation; here it returns false immediately when full or closed. Params: q - the queue; item - value to enqueue. Returns: true on success; false if the queue is full or closed. Complexity: O(1) amortized.

  • Postcondition: result == true => bq_size(q) >= 1
fn bq_pop(q: &mut BlockingQueue) -> Option[Int]

Dequeue an item. Blocks while empty in a threaded implementation; here it returns None immediately when empty or closed-and-drained. Params: q - the queue. Returns: the oldest item, or None when empty or closed and drained. Complexity: O(1).

  • Postcondition: result is None => bq_size(q) == 0
fn bq_try_push(q: &mut BlockingQueue, item: Int) -> Bool

Enqueue without blocking. Fails when full or closed. Params: q - the queue; item - value to enqueue. Returns: true on success; false if the queue is full or closed. Complexity: O(1) amortized.

  • Postcondition: result == true => bq_size(q) >= 1
fn bq_try_pop(q: &mut BlockingQueue) -> Option[Int]

Dequeue without blocking. None when empty or closed. Params: q - the queue. Returns: the oldest item, or None when empty or closed and drained. Complexity: O(1).

  • Postcondition: result is None => bq_size(q) == 0
fn bq_size(q: &BlockingQueue) -> Int

Number of items currently queued. Params: q - the queue. Returns: the count of not-yet-popped items. Complexity: O(1).

  • Postcondition: result >= 0
fn bq_capacity(q: &BlockingQueue) -> Int

Maximum number of items the queue can hold. Params: q - the queue. Returns: the fixed capacity. Complexity: O(1).

  • Postcondition: result >= 0
fn bq_close(q: &mut BlockingQueue)

Close the queue: push fails afterwards, pop drains the remainder. Params: q - the queue. Complexity: O(1).

  • Postcondition: bq_is_closed(q)
fn bq_is_closed(q: &BlockingQueue) -> Bool

True if the queue has been closed. Params: q - the queue. Returns: whether bq_close has been called. Complexity: O(1).

  • Postcondition: result == q.closed



bloom.xi

type BloomFilter

Space-efficient probabilistic set over Int values with no false negatives and a tunable false positive rate. bits holds bit_count usable bits packed into UInt8 bytes (the collect.hash pattern). Two independent multiplicative hashes (the collect.cuckoo pattern) are combined into num_hashes positions via h1 + ih2 mod m; hashing uses shifts and multiplies only, so the large-Int AND compiler bug (BUG 25 #7) is avoided. inserted tracks insertions so the false positive rate can be estimated as (1 - e^(-kn/m))^k.

Field Type
bits Vec[UInt8]
bit_count Int
num_hashes Int
inserted Int
fn bloom_new(bits: Int, hashes: Int) -> BloomFilter

Create a Bloom filter with bits usable bits and hashes hash functions. Both values are clamped to at least 1; the bit count is rounded up to a whole number of bytes. O(bits/8).

  • Postcondition: result.bit_count >= 8
  • Postcondition: result.num_hashes >= 1
  • Postcondition: result.inserted == 0
fn bloom_insert(b: &mut BloomFilter, value: Int)

Insert value into the filter. O(k).

  • Postcondition: bloom_may_contain(b, value)
fn bloom_may_contain(b: &BloomFilter, value: Int) -> Bool

True if value may be present. Never reports a false negative. O(k).

  • Postcondition: b.inserted == 0 => result == false
fn bloom_clear(b: &mut BloomFilter)

Reset all bits and the insertion counter. O(m/8).

  • Postcondition: b.inserted == 0
fn bloom_false_positive_rate(b: &BloomFilter) -> Float64

Estimated false positive rate (1 - e^(-k*n/m))^k for the current insertion count, where k = num_hashes, n = inserted, m = bit_count. O(1).

  • Postcondition: result >= 0
  • Postcondition: result <= 1



btree.xi

type BTree

B-tree ordered map of Int keys to Int values with a configurable order. order is the maximum number of children per node (clamped to >= 2); a node holds at most order-1 keys. Flat-arena representation: every node is mk = order-1 key/value slots and mk+1 child slots in parallel Vec[Int]s, with a per-node key count and a leaf flag. Inserts pre-split full nodes on the way down (CLRS), so insert/update is O(log n). btree_remove collects the surviving entries and rebuilds the tree, keeping it perfectly balanced (no underflow; O(n), documented). Removed nodes become unreachable arena entries.

Field Type
root Int
mk Int
nkeys Vec[Int]
keys Vec[Int]
vals Vec[Int]
childs Vec[Int]
leafs Vec[Int]
size Int
fn btree_new(order: Int) -> BTree

Create an empty B-tree with the given order. The root is allocated lazily on the first insert. O(1).

  • Postcondition: result.root == -1
  • Postcondition: result.size == 0
  • Postcondition: result.mk >= 1
fn btree_get(t: &BTree, key: Int) -> Option[Int]

Value for key, or None when absent. O(log n).

  • Postcondition: result is Some(_) => btree_contains(t, key)
  • Postcondition: result is None => btree_contains(t, key) == false
fn btree_contains(t: &BTree, key: Int) -> Bool

True if key is present. O(log n).

  • Postcondition: result == true => btree_size(t) >= 1
fn btree_insert(t: &mut BTree, key: Int, value: Int)

Insert or update key -> value. O(log n).

  • Postcondition: btree_contains(t, key)
fn btree_size(t: &BTree) -> Int

Number of entries. O(1).

  • Postcondition: result >= 0
fn btree_remove(t: &mut BTree, key: Int) -> Bool

Remove key; returns true if it was present. O(n) worst case (the tree is rebuilt so it stays perfectly balanced).

  • Postcondition: btree_contains(t, key) == false
fn btree_min(t: &BTree) -> Option[Int]

Smallest key, or None when the tree is empty. O(log n).

  • Postcondition: result is Some(_) => btree_size(t) > 0
  • Postcondition: result is None => btree_size(t) == 0
fn btree_max(t: &BTree) -> Option[Int]

Largest key, or None when the tree is empty. O(log n).

  • Postcondition: result is Some(_) => btree_size(t) > 0
  • Postcondition: result is None => btree_size(t) == 0



btreeplus.xi

type BPlusTree

B+ tree ordered map of Int keys to Int values, leaves linked for fast range scans. All data lives in leaves; internal nodes hold routing keys and child pointers only. order is the maximum number of children per internal node (clamped to >= 2); every node holds at most mk = order-1 keys. Flat-arena representation: per-node blocks of mk key/value slots and mk+1 child slots in parallel Vec[Int]s, with per-node key counts, leaf flags and a nexts leaf chain. Inserts pre-split full nodes on the way down (O(log n)). Removals delete lazily from the leaf (routing keys stay valid as range separators; empty leaves remain traversable), so bptree_range walks the leaf chain in O(log n + m). Removed nodes become unreachable arena entries.

Field Type
root Int
mk Int
nkeys Vec[Int]
keys Vec[Int]
vals Vec[Int]
childs Vec[Int]
leafs Vec[Int]
nexts Vec[Int]
size Int
fn bptree_new(order: Int) -> BPlusTree

Create an empty B+ tree with the given order. The root is allocated lazily on the first insert. O(1).

  • Postcondition: result.root == -1
  • Postcondition: result.size == 0
  • Postcondition: result.mk >= 1
fn bptree_insert(t: &mut BPlusTree, key: Int, value: Int)

Insert or update key -> value. O(log n).

  • Postcondition: bptree_contains(t, key)
fn bptree_get(t: &BPlusTree, key: Int) -> Option[Int]

Value for key, or None when absent. O(log n).

  • Postcondition: result is Some(_) => bptree_contains(t, key)
  • Postcondition: result is None => bptree_contains(t, key) == false
fn bptree_contains(t: &BPlusTree, key: Int) -> Bool

True if key is present. O(log n).

  • Postcondition: result == true => bptree_size(t) >= 1
fn bptree_remove(t: &mut BPlusTree, key: Int) -> Bool

Remove key; returns true if it was present. The key is removed from its leaf (lazy deletion); routing keys stay valid as separators. O(log n).

  • Postcondition: bptree_contains(t, key) == false
fn bptree_size(t: &BPlusTree) -> Int

Number of entries. O(1).

  • Postcondition: result >= 0
fn bptree_range(t: &BPlusTree, l: Int, r: Int) -> Vec[Int]

Values of keys in the inclusive range [l, r], in ascending key order, collected by walking the linked leaf chain. O(log n + m).

  • Postcondition: result.len() <= bptree_size(t)
  • Postcondition: r < l => result.len() == 0



cache.xi

type LruCache

LRU Cache (Int keys, Int values) Simple bookkeeping: keys/values are parallel vectors and order is a vector of keys in recency order, front = most recently used. lru_get and lru_put move an accessed key to the front; when full, the key at the back of order (least recently used) is evicted.

Field Type
capacity Int
keys Vec[Int]
values Vec[Int]
order Vec[Int]
fn lru_new(capacity: Int) -> LruCache

Create an LRU cache holding at most capacity entries.

  • Postcondition: result.keys.len() == 0
fn lru_get(c: &mut LruCache, key: Int) -> Option[Int]

Fetch a value, marking the key as most recently used. None if absent.

  • Postcondition: result.is_some == lru_contains(c, key)
fn lru_put(c: &mut LruCache, key: Int, value: Int)

Insert or update a key. Evicts the least recently used key when full.

  • Postcondition: lru_contains(c, key) == true
fn lru_contains(c: &LruCache, key: Int) -> Bool

True if the key is present in the cache.

fn lru_size(c: &LruCache) -> Int

Number of entries currently cached.

  • Postcondition: result >= 0
fn lru_capacity(c: &LruCache) -> Int

Maximum number of entries the cache can hold.

  • Postcondition: result >= 0
type LfuCache

LFU Cache (Int keys, Int values) Parallel keys/values/counts vectors plus an insertion-sequence vector seq used as a deterministic tie-break: when several keys share the lowest frequency, the least recently inserted one is evicted first.

Field Type
capacity Int
keys Vec[Int]
values Vec[Int]
counts Vec[Int]
seq Vec[Int]
next_seq Int
fn lfu_new(capacity: Int) -> LfuCache

Create an LFU cache holding at most capacity entries.

  • Postcondition: result.keys.len() == 0
fn lfu_get(c: &mut LfuCache, key: Int) -> Option[Int]

Fetch a value and increment its access frequency. None if absent.

  • Postcondition: result.is_some == lfu_contains(c, key)
fn lfu_put(c: &mut LfuCache, key: Int, value: Int)

Insert or update a key. On overflow, evicts the lowest-frequency key (tie-break: least recently inserted among the minimum-frequency group).

  • Postcondition: lfu_contains(c, key) == true
fn lfu_contains(c: &LfuCache, key: Int) -> Bool

True if the key is present in the cache.

fn lfu_size(c: &LfuCache) -> Int

Number of entries currently cached.

  • Postcondition: result >= 0
type ArcCache

ArcCache ? Adaptive Replacement Cache (2026-08-11) Standard ARC (Megiddo & Modha): T1 (recent) / T2 (frequent) hold cached (key, value) pairs, B1/B2 are ghost lists (keys only). p is the target size of T1 and adapts on ghost hits. Lists are parallel Vecs with the MRU at the FRONT; lookups are O(n) linear scans (documented ? this is a correctness-focused reference implementation; the compiler's Vec lacks a map container for struct elements). Int keys/values.

NOTE: all list operations are inlined on the &mut ArcCache struct ? helper fns taking &mut Vec[Int] params get a fresh-alloca COPY for non-ident args (&mut c.t1k), so their push/pop/shift mutations would be lost (COMPILER_BUGS.md BUG 16).

Field Type
capacity Int
p Int
t1k Vec[Int]
t1v Vec[Int]
t2k Vec[Int]
t2v Vec[Int]
b1 Vec[Int]
b2 Vec[Int]
fn arc_new(capacity: Int) -> ArcCache

Create an ARC cache with capacity entries (>= 1).

  • Postcondition: result.p == 0
fn arc_get(c: &mut ArcCache, key: Int) -> Option[Int]

Value for key (promotes recent->frequent on hit). None on miss.

  • Postcondition: result.is_some == arc_contains(c, key)
fn arc_contains(c: &ArcCache, key: Int) -> Bool

True if key is cached (does not change recency).

fn arc_size(c: &ArcCache) -> Int

Number of cached entries.

  • Postcondition: result >= 0
fn arc_capacity(c: &ArcCache) -> Int

Capacity.

  • Postcondition: result >= 0
fn arc_put(c: &mut ArcCache, key: Int, value: Int)

Insert or update key -> value, adapting p on ghost hits.

  • Postcondition: arc_contains(c, key) == true



concurrent.xi

type ConcurrentQueue

Mutex-protected FIFO queue.

Field Type
buf Vec[Int]
cap Int
head AtomicInt
tail AtomicInt
closed Bool
fn mpmc_queue_new(capacity: Int) -> ConcurrentQueue

Create a multi-producer multi-consumer queue with capacity slots. Params: capacity - number of buffered slots (clamped to >= 1). Returns: a new MPMC queue. Complexity: O(capacity).

  • Postcondition: result.cap >= 1
fn mpmc_push(q: &mut ConcurrentQueue, item: Int) -> Bool

Enqueue from any producer. False if full or closed. Params: q - the queue; item - value to enqueue. Returns: true on success, false when full or closed. Complexity: O(1).

fn mpmc_pop(q: &mut ConcurrentQueue) -> Option[Int]

Dequeue from any consumer. None if empty or closed. Params: q - the queue. Returns: the oldest item, or None when empty. Complexity: O(1).

fn mpsc_queue_new(capacity: Int) -> ConcurrentQueue

Create a multi-producer single-consumer queue with capacity slots. Params: capacity - number of buffered slots (clamped to >= 1). Returns: a new MPSC queue. Complexity: O(capacity).

  • Postcondition: result.cap >= 1
fn mpsc_push(q: &mut ConcurrentQueue, item: Int) -> Bool

Enqueue from any producer. False if full or closed. Params: q - the queue; item - value to enqueue. Returns: true on success, false when full or closed. Complexity: O(1).

fn mpsc_pop(q: &mut ConcurrentQueue) -> Option[Int]

Dequeue from the single consumer end. None if empty or closed. Params: q - the queue. Returns: the oldest item, or None when empty. Complexity: O(1).

fn spmc_queue_new(capacity: Int) -> ConcurrentQueue

Create a single-producer multi-consumer queue with capacity slots. Params: capacity - number of buffered slots (clamped to >= 1). Returns: a new SPMC queue. Complexity: O(capacity).

  • Postcondition: result.cap >= 1
fn spmc_push(q: &mut ConcurrentQueue, item: Int) -> Bool

Enqueue from the single producer end. False if full or closed. Params: q - the queue; item - value to enqueue. Returns: true on success, false when full or closed. Complexity: O(1).

fn spmc_pop(q: &mut ConcurrentQueue) -> Option[Int]

Dequeue from any consumer. None if empty or closed. Params: q - the queue. Returns: the oldest item, or None when empty. Complexity: O(1).

type ConcurrentStack

Mutex-protected LIFO stack.

Field Type
items Vec[Int]
closed Bool
fn concurrent_stack_new() -> ConcurrentStack

Create a concurrent LIFO stack. Returns: a new, open concurrent stack. Complexity: O(1).

  • Postcondition: result.items.len() == 0
fn cstack_push(s: &mut ConcurrentStack, item: Int) -> Bool

Push onto the stack. False if closed. Params: s - the stack; item - value to push. Returns: true on success, false when closed. Complexity: O(1) amortized.

  • Postcondition: result == true => s.items.len() >= 1
fn cstack_pop(s: &mut ConcurrentStack) -> Option[Int]

Pop from the stack. None if empty or closed. Params: s - the stack. Returns: the most recently pushed item, or None when empty. Complexity: O(1).

  • Postcondition: result is None => s.items.len() == 0
type ConcurrentCounter

Mutex-protected integer counter.

Field Type
c AtomicInt
fn concurrent_counter_new() -> ConcurrentCounter

Create a concurrent counter starting at zero. Returns: a counter whose value is 0. Complexity: O(1).

fn ccounter_add(c: &mut ConcurrentCounter, delta: Int)

Atomically add delta to the counter. Params: c - the counter; delta - signed increment. Complexity: O(1) (fetch_add).

fn ccounter_get(c: &ConcurrentCounter) -> Int

Read the current counter value. Params: c - the counter. Returns: the current value. Complexity: O(1) (atomic load).




cuckoo.xi

type CuckooMap

CuckooMap (Int keys, Int values) Two power-of-two tables with two independent multiplicative hashes. Insert displaces the victim to the other table (bounded at 16 relocations, then the tables double). O(1) expected lookups with at most 2 probes.

Field Type
t0_keys Vec[Int]
t0_vals Vec[Int]
t1_keys Vec[Int]
t1_vals Vec[Int]
size Int
cap Int
fn cuckoo_new(capacity: Int) -> CuckooMap

Create an empty cuckoo map with at least capacity slots (rounded up to a power of two).

  • Postcondition: result.cap >= 8
  • Postcondition: result.size == 0
  • Postcondition: result.t0_keys.len() == result.cap
fn cuckoo_put(m: &mut CuckooMap, key: Int, value: Int)

Insert or overwrite key -> value. Doubles the tables when the displacement bound is exceeded.

  • Postcondition: cuckoo_contains(m, key)
fn cuckoo_get(m: &CuckooMap, key: Int) -> Option[Int]

Value for key (None if absent).

  • Postcondition: result.is_some == cuckoo_contains(m, key)
fn cuckoo_contains(m: &CuckooMap, key: Int) -> Bool

True if key is present.

  • Postcondition: result == true => cuckoo_size(m) >= 1
fn cuckoo_remove(m: &mut CuckooMap, key: Int) -> Bool

Remove key. Returns true if it was present.

  • Postcondition: cuckoo_contains(m, key) == false
fn cuckoo_size(m: &CuckooMap) -> Int

Number of stored keys.

  • Postcondition: result >= 0



dag.xi

type Dag

Directed acyclic graph of Int node ids with topological ordering support.

Flat-arena style (the same adjacency representation as collect.graph): head[u] is the first edge id leaving node u, to[id] the destination of edge id, next[id] the next edge id in the same list (-1 = none). Node ids are handed out by dag_add_node and never reused. dag_add_edge refuses to add an edge that would close a cycle (checked via reachability of from from to); dag_has_cycle runs a full topological sort. Reachability and traversal helpers are BFS based (O(V + E)). Out-of-range ids are rejected (no silent failure).

Field Type
n Int
head Vec[Int]
to Vec[Int]
next Vec[Int]
fn dag_new() -> Dag

Create a new empty DAG (no nodes). O(1).

  • Postcondition: result.n == 0
fn dag_add_node(g: &mut Dag) -> Int

Add a node and return its id (0-based, monotonically increasing). O(1).

  • Postcondition: result >= 0
fn dag_has_edge(g: &Dag, from: Int, to: Int) -> Bool

True if the edge from -> to exists. O(degree(from)).

  • Postcondition: from < 0 || from >= g.n => result == false
fn dag_add_edge(g: &mut Dag, from: Int, to: Int) -> Bool

Add a directed edge from -> to. Returns false if the ids are out of range, if the edge already exists, or if adding it would close a cycle (i.e. to can already reach from). True when the edge is newly added. Self loops are rejected. O(V + E) for the cycle check.

  • Postcondition: result == true => dag_has_edge(g, from, to)
fn dag_ancestors(g: &Dag, node: Int) -> Vec[Int]

All transitive predecessors of node (nodes u != node with a path u -> ... -> node). Order is BFS order over the reversed edges. O(V + E).

  • Postcondition: node < 0 || node >= g.n => result.len() == 0
  • Postcondition: result.len() <= g.n
fn dag_descendants(g: &Dag, node: Int) -> Vec[Int]

All transitive successors of node (nodes v != node with a path node -> ... -> v). Order is BFS order. O(V + E).

  • Postcondition: node < 0 || node >= g.n => result.len() == 0
  • Postcondition: result.len() <= g.n
fn dag_topological_order(g: &Dag) -> Vec[Int]

A topological ordering of all nodes (Kahn's algorithm). If the graph contains a cycle, the returned order is partial (the cyclic nodes are omitted). O(V + E).

  • Postcondition: result.len() <= g.n
fn dag_has_cycle(g: &Dag) -> Bool

Check whether the graph contains a cycle (a topological sort covers all nodes iff the graph is acyclic). O(V + E).

  • Postcondition: result == true => g.n >= 1



dense.xi

type DenseSet

Dense set of unique Int elements backed by a bitmap for compact storage.

Non-negative values are stored as a single bit each; the bitmap lives in a Vec[UInt8] (value v occupies bit v % 8 of byte v / 8) that grows on demand to cover the largest inserted value. All core operations are O(1); iteration is O(bits) plus the set size. Negative values cannot be represented and are rejected by dense_add (documented, no silent failure).

Field Type
bits Vec[UInt8]
size Int
fn dense_set_new() -> DenseSet

Create a new empty dense set. O(1).

fn dense_add(s: &mut DenseSet, value: Int)

Add a value to the set (no-op if already present). Negative values are rejected (the bitmap cannot represent them). O(1) amortized.

fn dense_contains(s: &DenseSet, value: Int) -> Bool

Check whether a value is present. O(1).

fn dense_remove(s: &mut DenseSet, value: Int)

Remove a value from the set (no-op if absent). O(1).

fn dense_size(s: &DenseSet) -> Int

Number of elements in the set. O(1).

  • Postcondition: result >= 0
fn dense_iter(s: &DenseSet) -> Vec[Int]

Iterate all elements in ascending order. O(bits + n).




deque.xi

type Deque

Double-ended queue of Int elements with O(1) push and pop at both ends. Backed by a single Vec[Int] with head/tail offsets defining the live window [head, tail). Pops advance the offsets (stale slots are later overwritten); deque_push_front rebuilds the window when there is no room at the front. All pops/peeks are bounds-checked (None on empty).

Field Type
items Vec[Int]
head Int
tail Int
fn deque_new() -> Deque

Create an empty deque. O(1).

  • Postcondition: result.head == 0
  • Postcondition: result.tail == 0
fn deque_push_back(d: &mut Deque, value: Int)

Append value to the back of the deque. O(1).

  • Postcondition: d.tail - d.head >= 1
fn deque_push_front(d: &mut Deque, value: Int)

Prepend value to the front of the deque. O(1) amortized (O(n) when the window must be rebuilt).

  • Postcondition: d.tail - d.head >= 1
fn deque_pop_front(d: &mut Deque) -> Option[Int]

Remove and return the front value. None if the deque is empty. O(1).

  • Postcondition: result is None => d.tail - d.head == 0
fn deque_pop_back(d: &mut Deque) -> Option[Int]

Remove and return the back value. None if the deque is empty. O(1).

  • Postcondition: result is None => d.tail - d.head == 0
fn deque_front(d: &Deque) -> Option[Int]

Return the front value without removing it. None if empty. O(1).

  • Postcondition: result is None => d.tail - d.head == 0
fn deque_back(d: &Deque) -> Option[Int]

Return the back value without removing it. None if empty. O(1).

  • Postcondition: result is None => d.tail - d.head == 0
fn deque_len(d: &Deque) -> Int

Number of elements in the deque. O(1).

  • Postcondition: result >= 0
fn deque_is_empty(d: &Deque) -> Bool

True if the deque holds no elements. O(1).

  • Postcondition: result == (deque_len(d) == 0)



fenwick.xi

type FenwickTree

FenwickTree (1-based indices; n = number of slots) Point update + prefix-sum queries in O(log n). tree[i] covers the range (i - lowbit(i), i]. All index params are 1-based; 0 is invalid (returns 0).

Field Type
tree Vec[Int]
n Int
fn fenwick_new(n: Int) -> FenwickTree

Create a fenwick tree with n slots, all zero.

  • Postcondition: result.n == n
  • Postcondition: n >= 0 => result.tree.len() == n + 1
fn fenwick_add(t: &mut FenwickTree, idx: Int, delta: Int)

Add delta to slot idx (1-based). O(log n).

  • Postcondition: idx >= 1 && idx <= t.n && delta >= 0 => fenwick_sum(t, t.n) >= fenwick_sum(t, t.n)@pre
fn fenwick_sum(t: &FenwickTree, idx: Int) -> Int

Prefix sum of slots 1..=idx. O(log n). idx < 1 -> 0.

  • Postcondition: idx < 1 => result == 0
fn fenwick_range(t: &FenwickTree, l: Int, r: Int) -> Int

Sum of slots l..=r (1-based, inclusive). O(log n).

  • Postcondition: r < l => result == 0
fn fenwick_get(t: &FenwickTree, idx: Int) -> Int

Current value at slot idx (1-based). O(log n).

  • Postcondition: idx < 1 || idx > t.n => result == 0
fn fenwick_size(t: &FenwickTree) -> Int

Number of slots.

  • Postcondition: result >= 0



fheap.xi

type FibNode

Handle to a heap node, used by fheap_decrease_key. In the flat-arena adaptation the handle wraps the node's arena index (nodes are allocated in insertion order by fheap_push).

Field Type
idx Int
fn fheap_new() -> FibHeap

Create a new empty Fibonacci heap. Returns: an empty FibHeap. Complexity: O(1).

  • Postcondition: result.n == 0
fn fheap_push(h: &mut FibHeap, value: Int)

Insert an element. Params: h - the heap; value - Int element to insert. Complexity: O(1) amortized.

  • Postcondition: h.n >= 1
fn fheap_pop(h: &mut FibHeap) -> Option[Int]

Remove and return the minimum element. None if empty. Params: h - the heap. Returns: the minimum element, or None when empty. Complexity: O(log n) amortized.

  • Postcondition: result is None => h.n == 0
fn fheap_peek(h: &FibHeap) -> Option[Int]

Peek at the minimum element. None if empty. Params: h - the heap. Returns: the minimum element without removing it, or None when empty. Complexity: O(1).

  • Postcondition: result is None => h.n == 0
fn fheap_merge(h: &mut FibHeap, other: &mut FibHeap)

Merge other into this heap, leaving other empty. Params: h - the receiving heap; other - the heap to consume. Complexity: O(n log n) worst-case (drains via extract-min + insert).

  • Postcondition: other.n == 0
fn fheap_decrease_key(h: &mut FibHeap, node: &mut FibNode, new_key: Int)

Decrease a node's key. Params: h - the heap; node - a FibNode handle (arena index of a node allocated by fheap_push); new_key - the smaller key. Out-of-range handles and non-decreasing keys are ignored. Complexity: O(1) amortized.

fn fheap_len(h: &FibHeap) -> Int

Number of elements. Params: h - the heap. Returns: the number of elements currently stored. Complexity: O(1).

  • Postcondition: result >= 0



graph.xi

type Graph

Graph (Int node ids) The spec struct is { n: Int; adj: Vec[Vec[Int]]; }, but nested Vec[Vec[Int]] element access is unreliable in the current compiler (see collect/heap.xi), so the adj field is retained per the module spec while the adjacency is stored in a flat linked arena: head[u] = first edge id in u's neighbor list (or -1) to[id] = destination node of edge id next[id] = next edge id in the same node's list (or -1) Appending is O(1); has_edge/degree/neighbors walk the list. graph_add_edge adds both directions and rejects duplicates; graph_add_directed_edge adds a single directed edge.

Field Type
n Int
adj Vec[Vec[Int]]
head Vec[Int]
to Vec[Int]
next Vec[Int]
fn graph_new(n: Int) -> Graph

Create a graph with n isolated nodes.

  • Postcondition: result.n == n
fn graph_has_edge(g: &Graph, u: Int, v: Int) -> Bool

True if node v is a neighbor of node u.

  • Postcondition: u < 0 || u >= g.n => result == false
fn graph_add_edge(g: &mut Graph, u: Int, v: Int)

Add an undirected edge between u and v (no duplicates).

  • Postcondition: u >= 0 && u < g.n && v >= 0 && v < g.n => graph_has_edge(g, u, v)
fn graph_add_directed_edge(g: &mut Graph, u: Int, v: Int)

Add a directed edge u -> v (no duplicates).

  • Postcondition: u >= 0 && u < g.n && v >= 0 && v < g.n => graph_has_edge(g, u, v)
fn graph_degree(g: &Graph, u: Int) -> Int

Number of neighbors of node u.

  • Postcondition: result >= 0
fn graph_neighbors(g: &Graph, u: Int) -> Vec[Int]

A copy of the neighbors of node u.

  • Postcondition: result.len() == graph_degree(g, u)
fn graph_bfs(g: &Graph, start: Int) -> Vec[Int]

Breadth-first traversal from start, in visited order.

  • Postcondition: start < 0 || start >= g.n => result.len() == 0
  • Postcondition: result.len() <= g.n
fn graph_dfs(g: &Graph, start: Int) -> Vec[Int]

Iterative depth-first traversal from start, in visited order.

  • Postcondition: start < 0 || start >= g.n => result.len() == 0
  • Postcondition: result.len() <= g.n
fn graph_connected_components(g: &Graph) -> Int

Number of connected components in the graph.

  • Postcondition: result >= 0
fn graph_has_cycle(g: &Graph) -> Bool

True if the (undirected) graph contains a cycle. Uses BFS with a parent check: a visited neighbor that is not the current node's parent closes a cycle.

  • Postcondition: result == true => g.n >= 1
fn graph_path_exists(g: &Graph, a: Int, b: Int) -> Bool

True if there is a path from a to b (BFS).

  • Postcondition: a == b && a >= 0 && a < g.n => result == true
type GraphUnionFind

Union-Find / Disjoint Set (Int elements) parent stores each element's parent (root points at itself) and rank stores the tree height for union-by-rank. uf_find applies path compression; uf_find_no_compress is a read-only variant used by uf_connected and uf_count so they can take an immutable reference.

Field Type
parent Vec[Int]
rank Vec[Int]
fn uf_new(n: Int) -> GraphUnionFind

Create a disjoint set with elements 0..n-1, each in its own set.

  • Postcondition: result.parent.len() == result.rank.len()
fn uf_find(u: &mut GraphUnionFind, x: Int) -> Int

Find the root of x with path compression.

  • Postcondition: x >= 0 && x < u.parent.len() => result >= 0
fn uf_union(u: &mut GraphUnionFind, a: Int, b: Int) -> Bool

Merge the sets containing a and b (union by rank). Returns true if the two sets were merged (i.e. previously disjoint).

  • Postcondition: a >= 0 && a < u.parent.len() && b >= 0 && b < u.parent.len() => uf_connected(u, a, b)
fn uf_connected(u: &GraphUnionFind, a: Int, b: Int) -> Bool

True if a and b are in the same set.

  • Postcondition: a == b => result == true
fn uf_count(u: &GraphUnionFind) -> Int

Number of distinct roots (sets).

  • Postcondition: result >= 0



hamt.xi

type Hamt

Hash array mapped trie (Int keys, Int values). A space-efficient persistent map built on a trie of 32-way nodes using the hash of the key. Average O(log_32 n) operations with fast structural sharing and cache locality. Duplicate keys are rejected by insert.

Flat-arena style (the established collect/ pattern -- tree.xi/graph.xi use parallel Vec[Int]s because Vec-of-struct instantiations collide at startup in combined programs). Every node owns 32 child slots in the flat kids vector (kids[i * 32 + slot]), so table nodes and leaf nodes share one uniform layout. Leaf nodes additionally carry the key, the value and the full 64-bit hash of the key; is_leaf[i] distinguishes the two kinds. The 5-bit window of the key hash at depth d selects the child slot, so a path is at most 13 nodes deep (64 hash bits / 5 bits). Node 0 is always a table node (the root).

Field Type
root Int
size Int
keys Vec[Int]
values Vec[Int]
hashes Vec[Int]
is_leaf Vec[Bool]
kids Vec[Int]
fn hamt_new() -> Hamt

Create an empty HAMT (a single empty root table node). Returns a fresh Hamt with size 0. O(1) time, O(1) memory.

fn hamt_insert(h: &mut Hamt, key: Int, value: Int) -> Bool

Insert key -> value. Returns false if the key already exists (the map keeps the original value). True on a fresh insert. O(log_32 n) expected.

fn hamt_get(h: &Hamt, key: Int) -> Option[Int]

Value stored for key, or None if the key is absent. O(log_32 n) expected.

fn hamt_contains(h: &Hamt, key: Int) -> Bool

True if key is present in the map. O(log_32 n) expected.

fn hamt_remove(h: &mut Hamt, key: Int) -> Bool

Remove key. Returns true if it was present. O(log_32 n) expected.

fn hamt_size(h: &Hamt) -> Int

Number of key/value pairs in the map. O(1).

  • Postcondition: result >= 0
fn hamt_clear(h: &mut Hamt)

Remove all entries, leaving the map empty. O(1) (arena memory is retained).

  • Postcondition: hamt_size(h) == 0



hash.xi

type BloomFilter

Bloom Filter (UInt8 byte inputs) bits is a byte array holding bit_count usable bits (rounded up to a byte multiple). Two independent base hashes (FNV-1a and DJB2) are combined into num_hashes positions via h1 + ih2 mod m. inserted tracks the number of insertions so the false positive rate can be estimated as (1 - e^(-kn/m))^k.

Field Type
bits Vec[UInt8]
bit_count Int
num_hashes Int
inserted Int
fn bloom_new(bits: Int, num_hashes: Int) -> BloomFilter

Create a bloom filter with bits usable bits and num_hashes hash functions. The bit count is rounded up to a whole number of bytes.

  • Postcondition: result.bit_count >= 8
  • Postcondition: result.num_hashes >= 1
fn bloom_insert(b: &mut BloomFilter, data: &Vec[UInt8])

Insert the given bytes into the filter.

  • Postcondition: bloom_maybe_contains(b, data)
fn bloom_maybe_contains(b: &BloomFilter, data: &Vec[UInt8]) -> Bool

True if the bytes may be present. Never reports a false negative.

  • Postcondition: b.inserted == 0 => result == false
fn bloom_clear(b: &mut BloomFilter)

Clear all bits and reset the insertion counter.

  • Postcondition: b.inserted == 0
fn bloom_false_positive_rate(b: &BloomFilter) -> Float64

Estimated false positive rate: (1 - e^(-k*n/m))^k using the tracked insertion count, where k = num_hashes, n = inserted, m = bit_count.

  • Postcondition: result >= 0
type LhMap

LhMap -- insertion-ordered map (Int keys -> Int values) Inserting a new key appends; updating an existing key keeps its position.

Field Type
keys Vec[Int]
values Vec[Int]
fn lhmap_new() -> LhMap

Create an empty insertion-ordered map.

  • Postcondition: result.keys.len() == 0
fn lhmap_put(m: &mut LhMap, key: Int, value: Int)

Insert or update a key. New keys are appended in insertion order.

  • Postcondition: lhmap_contains(m, key)
fn lhmap_get(m: &LhMap, key: Int) -> Option[Int]

Fetch a value by key. None if absent.

  • Postcondition: result.is_some == lhmap_contains(m, key)
fn lhmap_contains(m: &LhMap, key: Int) -> Bool

True if the key is present.

  • Postcondition: result == true => lhmap_size(m) >= 1
fn lhmap_remove(m: &mut LhMap, key: Int) -> Bool

Remove a key, preserving the relative order of the remaining entries. Returns true if the key was present.

  • Postcondition: lhmap_contains(m, key) == false
  • Postcondition: result == true => lhmap_size(m) == lhmap_size(m)@pre - 1
  • Postcondition: result == false => lhmap_size(m) == lhmap_size(m)@pre
fn lhmap_size(m: &LhMap) -> Int

Number of entries in the map.

  • Postcondition: result >= 0
fn lhmap_keys_in_order(m: &LhMap) -> Vec[Int]

The keys in insertion order.

  • Postcondition: result.len() == lhmap_size(m)



hasharray.xi

type Hamt

Hash-array mapped trie (HAMT) map of Int keys to Int values. Flat-arena style (the established collect/ pattern): every node owns 32 child slots in the flat kids vector (kids[i * 32 + slot]), so table nodes and leaf nodes share one uniform layout. Leaf nodes carry the key, the value and the full 64-bit hash; is_leaf[i] distinguishes the kinds. The 5-bit window of the key hash at depth d selects the child slot, so a path is at most 13 nodes deep (64 hash bits / 5 bits). Node 0 is always a table node (the root). Inserts are upserts: re-inserting a key updates its value. Average O(log_32 n) operations.

Field Type
root Int
size Int
keys Vec[Int]
values Vec[Int]
hashes Vec[Int]
is_leaf Vec[Bool]
kids Vec[Int]
fn hamt_new() -> Hamt

Create a new empty HAMT map (a single empty root table node). Returns: a fresh Hamt with 0 entries. Complexity: O(1).

fn hamt_insert(h: &mut Hamt, key: Int, value: Int)

Insert or update key -> value. Params: h - the map; key - Int key; value - Int value. Re-inserting an existing key updates its value in place. Complexity: O(log_32 n) expected.

fn hamt_get(h: &Hamt, key: Int) -> Option[Int]

Get the value for a key. None when absent. Params: h - the map; key - Int key. Returns: Some(value) if present, None otherwise. Complexity: O(log_32 n) expected.

fn hamt_contains(h: &Hamt, key: Int) -> Bool

Check whether a key is present. Params: h - the map; key - Int key. Returns: true if key maps to a value. Complexity: O(log_32 n) expected.

fn hamt_remove(h: &mut Hamt, key: Int)

Remove a key. Params: h - the map; key - Int key. Absent keys are a no-op. Arena memory is retained. Complexity: O(log_32 n) expected.

fn hamt_size(h: &Hamt) -> Int

Number of entries. Params: h - the map. Returns: the number of key/value pairs. Complexity: O(1).

  • Postcondition: result >= 0



hashset.xi

type HashSet

Hash set of unique Int elements using open addressing (linear probing) with a power-of-two table. A parallel used flag vector allows every Int value (including INT_MIN) as an element. The table doubles at 50% load. Hashes are multiplicative and use shifts/multiplies plus a modulo index, so the compiler's large-Int AND bug (BUG 25 #7) is avoided. hashset_remove rebuilds the table (correct under tombstones; O(n) but simple and safe). NOTE: the API parameter type is HashSet: naming it Set collides with the xiom.collections.Set[T] generic and crashes the binary at startup (0xC0000005); the fn names and value signatures match the frozen spec.

Field Type
slots Vec[Int]
used Vec[Int]
cap Int
size Int
fn hashset_new() -> HashSet

Create a new empty hash set. O(1).

fn hashset_insert(s: &mut HashSet, value: Int)

Insert value if it is not already present. O(1) expected.

fn hashset_contains(s: &HashSet, value: Int) -> Bool

True if value is present. O(1) expected.

fn hashset_remove(s: &mut HashSet, value: Int)

Remove value if present. O(n) worst case (table rebuild).

fn hashset_size(s: &HashSet) -> Int

Number of elements in the set. O(1).

  • Postcondition: result >= 0
fn hashset_clear(s: &mut HashSet)

Remove all elements. O(cap).

  • Postcondition: hashset_size(s) == 0



heap.xi

type PHeap

Pairing Heap (Int keys) Arena of nodes; node i lives at the i-th triple of the keys vector: keys[3i] = key keys[3i+1] = first child keys[3i+2] = next sibling (nested Vec[Vec[Int]] element access is unreliable in the current compiler, so the child lists are stored as first-child/next-sibling links in the flat arena; the children field is retained per the module spec.) Merge works on concrete Int keys; extract uses the two-pass pairwise merge.

Field Type
root Int
keys Vec[Int]
children Vec[Vec[Int]]
fn pheap_new() -> PHeap

Create an empty pairing heap.

  • Postcondition: result.root == -1
fn pheap_insert(h: &mut PHeap, key: Int)

Insert a key into the heap.

fn pheap_find_min(h: &PHeap) -> Option[Int]

Minimum key, or None if the heap is empty.

  • Postcondition: result.is_some == (pheap_size(h) > 0)
fn pheap_extract_min(h: &mut PHeap) -> Option[Int]

Remove and return the minimum key, or None if empty. Children of the removed root are merged pairwise (left-to-right pass).

fn pheap_size(h: &PHeap) -> Int

Number of reachable nodes in the heap.

  • Postcondition: result >= 0
fn pheap_is_empty(h: &PHeap) -> Bool

True if the heap contains no keys.

  • Postcondition: result == (pheap_size(h) == 0)
type FibHeap

Fibonacci Heap (Int keys) Arena of parallel vectors. The root list and every child list are circular doubly-linked rings through the left/right vectors; sentinel index -1 denotes "no node". Extract-min consolidates the root list with 64 degree buckets. Decrease-key performs a cut + cascading cut (CLRS).

Field Type
min Int
n Int
keys Vec[Int]
parent Vec[Int]
child Vec[Int]
left Vec[Int]
right Vec[Int]
degree Vec[Int]
mark Vec[Bool]
fn fib_heap_new() -> FibHeap

Create an empty Fibonacci heap.

  • Postcondition: result.n == 0
fn fib_heap_insert(h: &mut FibHeap, key: Int)

Insert a key into the heap.

fn fib_heap_find_min(h: &FibHeap) -> Option[Int]

Minimum key, or None if the heap is empty.

  • Postcondition: result.is_some == (fib_heap_size(h) > 0)
fn fib_heap_extract_min(h: &mut FibHeap) -> Option[Int]

Remove and return the minimum key, or None if empty. Consolidates the root list so future extract-mins stay amortized.

fn fib_heap_size(h: &FibHeap) -> Int

Number of keys in the heap.

  • Postcondition: result >= 0
fn fib_heap_is_empty(h: &FibHeap) -> Bool

True if the heap contains no keys.

  • Postcondition: result == (fib_heap_size(h) == 0)
fn fib_heap_decrease_key(h: &mut FibHeap, node: Int, new_key: Int) -> Bool

Decrease the key of node to new_key. Returns false if the node index is out of range or the new key is not smaller.




immutable.xi

type PVec

Persistent (copy-on-write) vector and map retaining prior versions. Every update copies the backing arena into a fresh Vec before mutating, so any caller holding an older PVec/PMap value still observes the version it captured. Int elements; accessors return Option[Int].

Field Type
items Vec[Int]
type PMap

Persistent (immutable) map value.

Field Type
keys Vec[Int]
values Vec[Int]
fn persistent_vec_new() -> PVec

Create a new empty persistent vector. Returns: an empty PVec. Complexity: O(1).

fn pvec_push(v: &mut PVec, value: Int)

Append a value, returning a new version (copy-on-write). Params: v - the vector; value - Int element to append. The backing Vec is rebuilt, leaving any previously captured PVec intact. Complexity: O(n).

fn pvec_get(v: &PVec, idx: Int) -> Option[Int]

Get the value at an index. None when out of range. Params: v - the vector; idx - zero-based index. Returns: Some(element) if idx is in range, None otherwise. Complexity: O(1).

fn pvec_len(v: &PVec) -> Int

Number of elements. Params: v - the vector. Returns: the number of elements. Complexity: O(1).

  • Postcondition: result >= 0
fn persistent_map_new() -> PMap

Create a new empty persistent map. Returns: an empty PMap. Complexity: O(1).

fn pmap_put(m: &mut PMap, key: Int, value: Int)

Insert or update a key (copy-on-write). Params: m - the map; key - Int key; value - Int value. The backing arenas are rebuilt, leaving any previously captured PMap intact. Complexity: O(n).

fn pmap_get(m: &PMap, key: Int) -> Option[Int]

Get the value for a key. None when absent. Params: m - the map; key - Int key. Returns: Some(value) if present, None otherwise. Complexity: O(n).

fn pmap_remove(m: &mut PMap, key: Int)

Remove a key (copy-on-write). Params: m - the map; key - Int key. Absent keys produce an equivalent copy. Prior versions stay intact. Complexity: O(n).




interval.xi

type IntervalTree

Interval tree (Int start/end, Int value). Stores [start, end] intervals and answers stabbing queries (which intervals contain a point) and range queries (which intervals overlap [start, end]) in O(log n + k) where k is the number of reported intervals. Intervals are inclusive on both ends.

Flat-arena style (the established collect/ pattern). The tree is a BST keyed by start; each node also tracks max_ends, the largest end in its subtree, which prunes subtrees that cannot intersect a query. Equal starts are inserted to the right (multi-map semantics). Removed intervals are marked dead (alive = false) and skipped by every query, so removal never disturbs the tree shape. Queries skip a subtree when its max end is below the query point (stabbing) or below the query low bound (overlap).

Field Type
root Int
size Int
starts Vec[Int]
ends Vec[Int]
vals Vec[Int]
left Vec[Int]
right Vec[Int]
max_ends Vec[Int]
alive Vec[Bool]
fn interval_tree_new() -> IntervalTree

Create an empty interval tree. O(1).

fn interval_insert(t: &mut IntervalTree, start: Int, end: Int, value: Int)

Insert the interval [start, end] (inclusive) with its value. Duplicate intervals are allowed. An interval with start > end is rejected (ignored). O(h) with h the tree height (O(log n) expected).

fn interval_query(t: &IntervalTree, point: Int) -> Vec[Int]

Values of the intervals containing point (inclusive bounds). O(log n + k) expected.

fn interval_range_query(t: &IntervalTree, start: Int, end: Int) -> Vec[Int]

Values of the intervals overlapping [start, end] (inclusive; an interval [a, b] overlaps when a <= end and b >= start). O(log n + k) expected.

fn interval_remove(t: &mut IntervalTree, start: Int, end: Int) -> Bool

Remove the first interval matching [start, end]. Returns true if one was found. Intervals are removed lazily (skipped by later queries). O(n) worst case.

fn interval_size(t: &IntervalTree) -> Int

Number of live intervals. O(1).

  • Postcondition: result >= 0
fn interval_contains_point(t: &IntervalTree, point: Int) -> Bool

True if any live interval contains point. O(log n + k) expected.

fn interval_overlaps(t: &IntervalTree, start: Int, end: Int) -> Bool

True if any live interval overlaps the range [start, end]. O(log n + k) expected.




intmap.xi

type IntMap

Optimized keyed maps. int_map uses a flat open-addressing table sized for the expected capacity (Int keys -> Int values); string_map uses a string-keyed variant. Both reject duplicate keys and iterate over stored keys in insertion order via int_map_iter.

Flat-arena style. The int_map table stores parallel keys/vals/occ/ tomb vectors of cap slots with linear probing and a multiplicative hash (high 32 bits of key * golden ratio, forced non-negative) so INT_MIN and other pathological keys are safe. Deleted slots become tombstones so probing chains stay intact; the table doubles when the load factor reaches 1/2. A separate order vector tracks the insertion order of live keys for int_map_iter. string_map is a simpler linear Vec[Str] map (strings are compared via bound locals, compiler BUG 8 workaround).

Field Type
cap Int
size Int
keys Vec[Int]
vals Vec[Int]
occ Vec[Bool]
tomb Vec[Bool]
order Vec[Int]
fn int_map_new(capacity: Int) -> IntMap

Create an Int-keyed map with capacity slots. The table grows automatically, so capacity is an initial hint; it is clamped to >= 1. O(capacity).

  • Postcondition: result.size == 0
fn int_map_put(m: &mut IntMap, key: Int, value: Int)

Insert or overwrite key -> value. A re-insert of an existing key updates its value without changing its insertion position. O(1) amortized.

fn int_map_get(m: &IntMap, key: Int) -> Option[Int]

Value for key, or None if absent. O(1) amortized.

  • Postcondition: result.is_some == int_map_contains(m, key)
fn int_map_contains(m: &IntMap, key: Int) -> Bool

True if key is present. O(1) amortized.

fn int_map_remove(m: &mut IntMap, key: Int) -> Bool

Remove key. Returns true if it was present. O(n) amortized (order compaction).

  • Postcondition: int_map_contains(m, key) == false
  • Postcondition: result == true => int_map_size(m) == int_map_size(m)@pre - 1
  • Postcondition: result == false => int_map_size(m) == int_map_size(m)@pre
fn int_map_size(m: &IntMap) -> Int

Number of key/value pairs. O(1).

  • Postcondition: result >= 0
fn int_map_iter(m: &IntMap) -> Vec[Int]

All keys in insertion order. O(n).

  • Postcondition: result.len() == int_map_size(m)
type OrderedStringMap

OrderedStringMap (Str keys -> Int values, insertion-ordered)

Field Type
keys Vec[Str]
vals Vec[Int]
fn string_map_new() -> OrderedStringMap

Create a Str-keyed map. O(1).

  • Postcondition: result.keys.len() == 0
fn string_map_put(m: &mut OrderedStringMap, key: Str, value: Int)

Insert or overwrite key -> value. A re-insert of an existing key updates its value without changing its insertion position. O(n).

fn string_map_get(m: &OrderedStringMap, key: Str) -> Option[Int]

Value for key, or None if absent. O(n).

  • Postcondition: result.is_some == string_map_contains(m, key)
fn string_map_contains(m: &OrderedStringMap, key: Str) -> Bool

True if key is present. O(n).

fn string_map_remove(m: &mut OrderedStringMap, key: Str) -> Bool

Remove key. Returns true if it was present. O(n).

  • Postcondition: string_map_contains(m, key) == false
  • Postcondition: result == true => string_map_size(m) == string_map_size(m)@pre - 1
  • Postcondition: result == false => string_map_size(m) == string_map_size(m)@pre
fn string_map_size(m: &OrderedStringMap) -> Int

Number of key/value pairs. O(1).

  • Postcondition: result >= 0



kdtree.xi

type KdTree

2D k-d tree of Int points with values, supporting nearest-neighbor and rectangular range queries.

Flat-arena style (the established collect/ pattern -- tree.xi/graph.xi use parallel Vec[Int]s because Vec-of-struct instantiations collide at startup in combined programs). Node i lives in the parallel vectors xs/ys/vals plus its left/right children; the splitting axis alternates by depth (x at even depth, y at odd depth), which is re-derived during every walk so no depth field needs to be stored. Distances are squared Int distances, so no floating point is involved. kdtree_insert is an incremental insert (O(h) with h the tree height); the worst case is O(n) per insert for degenerate orders, expected O(log n).

Field Type
root Int
size Int
xs Vec[Int]
ys Vec[Int]
vals Vec[Int]
left Vec[Int]
right Vec[Int]
fn kdtree_new() -> KdTree

Create a new empty k-d tree. O(1).

fn kdtree_insert(t: &mut KdTree, x: Int, y: Int, value: Int)

Insert a point (x, y) with its value. Duplicate points are allowed and each insertion creates a new node. O(h) expected, O(n) worst case.

fn kdtree_nearest(t: &KdTree, x: Int, y: Int) -> Option[Int]

Value of the point nearest to (x, y), or None if the tree is empty. Ties are broken toward the point visited first. O(n) worst case, O(log n) expected.

fn kdtree_range(t: &KdTree, x1: Int, y1: Int, x2: Int, y2: Int) -> Vec[Int]

Values of all points inside the rectangle [x1, x2] x [y1, y2] (inclusive). Empty regions yield an empty Vec. O(n) worst case.

fn kdtree_size(t: &KdTree) -> Int

Number of stored points. O(1).

  • Postcondition: result >= 0



lfu.xi

type LfuCache

Least-frequently-used cache with Int keys and values, evicting the least frequently accessed entry when full.

Flat-arena style. keys/values/counts are parallel vectors; every access bumps the entry's frequency. seq is an insertion-sequence vector used as a deterministic tie-break: when several keys share the lowest frequency, the least recently inserted one is evicted first. next_seq hands out increasing sequence numbers. lfu_get / lfu_put increase the frequency of the touched key (a get on a hit counts as an access).

Field Type
capacity Int
keys Vec[Int]
values Vec[Int]
counts Vec[Int]
seq Vec[Int]
next_seq Int
fn lfu_new(capacity: Int) -> LfuCache

Create a new LFU cache holding at most capacity entries. Capacity is clamped to >= 1. O(1).

  • Postcondition: result.capacity >= 1
  • Postcondition: result.keys.len() == 0
fn lfu_get(c: &mut LfuCache, key: Int) -> Option[Int]

Get the value for key, increasing its frequency. None if absent. O(n).

  • Postcondition: result.is_some == lfu_contains(c, key)
fn lfu_put(c: &mut LfuCache, key: Int, value: Int)

Insert or update key -> value, evicting the least-frequently-used entry when full (tie-break: least recently inserted among the minimum-frequency group). A put on an existing key increases its frequency. O(n).

  • Postcondition: lfu_contains(c, key)
fn lfu_contains(c: &mut LfuCache, key: Int) -> Bool

Check whether key is present (does not change its frequency). O(n).

  • Postcondition: result == true => lfu_size(c) > 0
fn lfu_remove(c: &mut LfuCache, key: Int) -> Bool

Remove key, returning whether it was present. O(n).

  • Postcondition: lfu_contains(c, key) == false
fn lfu_size(c: &mut LfuCache) -> Int

Number of entries currently cached. O(1).

  • Postcondition: result >= 0
fn lfu_capacity(c: &mut LfuCache) -> Int

Maximum number of entries the cache can hold. O(1).

  • Postcondition: result >= 0
fn lfu_clear(c: &mut LfuCache)

Remove all entries from the cache. O(1).

  • Postcondition: lfu_size(c) == 0



linkedhash.xi

type LhMap

Hash map preserving insertion order of Int keys. Keys and values live in two parallel Vec[Int]s in insertion order: putting an existing key updates its value without moving it; putting a new key appends. lhmap_first/ lhmap_last/lhmap_iter read that order. Lookup is a linear scan (O(n)), which keeps the API dependency-free; removal compacts the vectors.

Field Type
keys Vec[Int]
values Vec[Int]
fn lhmap_new() -> LhMap

Create a new empty insertion-ordered map. O(1).

fn lhmap_put(m: &mut LhMap, key: Int, value: Int)

Insert or update key -> value. New keys are appended in insertion order; updating keeps the existing position. O(n).

fn lhmap_get(m: &LhMap, key: Int) -> Option[Int]

Value for key, or None when absent. O(n).

fn lhmap_contains(m: &LhMap, key: Int) -> Bool

True if key is present. O(n).

fn lhmap_remove(m: &mut LhMap, key: Int)

Remove key if present, preserving the relative order of the remaining entries. O(n).

fn lhmap_size(m: &LhMap) -> Int

Number of entries in the map. O(1).

  • Postcondition: result >= 0
fn lhmap_first(m: &LhMap) -> Option[Int]

First key in insertion order, or None when the map is empty. O(1).

fn lhmap_last(m: &LhMap) -> Option[Int]

Last key in insertion order, or None when the map is empty. O(1).

fn lhmap_iter(m: &LhMap) -> Vec[Int]

All keys in insertion order. O(n).




list.xi

type LinkedList

Doubly linked list of Int elements with O(1) push/pop/peek at both ends. Flat-arena representation (the established collect/ pattern): nodes live in three parallel Vec[Int]s (values/prevs/nexts) addressed by index; -1 is the "no node" sentinel. head/tail index the two ends. Removed nodes become unreachable arena entries. Indexed access is O(n); all index arguments are bounds-checked.

Field Type
head Int
tail Int
size Int
values Vec[Int]
prevs Vec[Int]
nexts Vec[Int]
fn linked_list_new() -> LinkedList

Create a new empty linked list. O(1).

  • Postcondition: result.size == 0
fn ll_push_front(l: &mut LinkedList, value: Int)

Add value to the front of the list. O(1).

fn ll_push_back(l: &mut LinkedList, value: Int)

Add value to the back of the list. O(1).

fn ll_pop_front(l: &mut LinkedList) -> Option[Int]

Remove and return the front value. None if the list is empty. O(1).

  • Postcondition: result is Some(_) => ll_len(l) == ll_len(l)@pre - 1
  • Postcondition: result is None => ll_len(l) == ll_len(l)@pre
fn ll_pop_back(l: &mut LinkedList) -> Option[Int]

Remove and return the back value. None if the list is empty. O(1).

  • Postcondition: result is Some(_) => ll_len(l) == ll_len(l)@pre - 1
  • Postcondition: result is None => ll_len(l) == ll_len(l)@pre
fn ll_front(l: &LinkedList) -> Option[Int]

Return the front value without removing it. None if empty. O(1).

  • Postcondition: result.is_some == (ll_len(l) > 0)
fn ll_back(l: &LinkedList) -> Option[Int]

Return the back value without removing it. None if empty. O(1).

  • Postcondition: result.is_some == (ll_len(l) > 0)
fn ll_len(l: &LinkedList) -> Int

Number of elements in the list. O(1).

  • Postcondition: result >= 0
fn ll_is_empty(l: &LinkedList) -> Bool

True if the list holds no elements. O(1).

  • Postcondition: result == (ll_len(l) == 0)
fn ll_get(l: &LinkedList, idx: Int) -> Option[Int]

Value at index idx (0 = front). None when idx is out of bounds. O(n).

  • Postcondition: result.is_some == (idx >= 0 && idx < ll_len(l))



lru.xi

type LruCache

Least-recently-used cache with O(1) get/put over Int keys and values.

Flat-arena style. keys/values are parallel vectors and order is a vector of keys in recency order, front = most recently used. lru_get and lru_put move an accessed key to the front; when full, the key at the back of order (least recently used) is evicted. Lookups are O(n) linear scans (the compiler's Vec has no hash map for struct elements), which is acceptable for the small cache sizes this module targets.

Field Type
capacity Int
keys Vec[Int]
values Vec[Int]
order Vec[Int]
fn lru_new(capacity: Int) -> LruCache

Create a new LRU cache holding at most capacity entries. Capacity is clamped to >= 1. O(1).

fn lru_get(c: &mut LruCache, key: Int) -> Option[Int]

Get the value for key, marking it recently used. None if absent. O(n).

fn lru_put(c: &mut LruCache, key: Int, value: Int)

Insert or update key -> value, evicting the least-recently-used entry when full. O(n).

fn lru_contains(c: &mut LruCache, key: Int) -> Bool

Check whether key is present (does not change recency). O(n).

fn lru_remove(c: &mut LruCache, key: Int) -> Bool

Remove key, returning whether it was present. O(n).

fn lru_size(c: &mut LruCache) -> Int

Number of entries currently cached. O(1).

  • Postcondition: result >= 0
fn lru_capacity(c: &mut LruCache) -> Int

Maximum number of entries the cache can hold. O(1).

  • Postcondition: result >= 0
fn lru_clear(c: &mut LruCache)

Remove all entries from the cache. O(1).

  • Postcondition: lru_size(c) == 0



map.xi

type HashIntMap

An open-addressing hash HashIntMap from Int keys to Int values.

Field Type
keys Vec[Int]
values Vec[Int]
states Vec[Int]
used Int
fn map_new() -> HashIntMap

Create a new empty HashIntMap (capacity 16). Complexity: O(1).

  • Postcondition: result.used == 0
fn map_put(m: &mut HashIntMap, key: Int, value: Int)

Insert or update a key. Grows the table when the load factor exceeds 0.75. Complexity: O(1) amortized.

  • Postcondition: m.used >= 1
fn map_get(m: &HashIntMap, key: Int) -> Option[Int]

Get the value for a key. Complexity: O(1) average.

fn map_contains(m: &HashIntMap, key: Int) -> Bool

Check whether a key is present. Complexity: O(1) average.

fn map_remove(m: &mut HashIntMap, key: Int) -> Bool

Remove a key, returning whether it was present (the bucket becomes a tombstone). Complexity: O(1) average.

  • Postcondition: m.used >= 0
fn map_size(m: &HashIntMap) -> Int

Number of entries. Complexity: O(1).

  • Postcondition: result >= 0
fn map_keys(m: &HashIntMap) -> Vec[Int]

Collect all keys. Complexity: O(capacity).

  • Postcondition: result.len() == map_size(m)
fn map_clear(m: &mut HashIntMap)

Remove all entries. Complexity: O(capacity).

  • Postcondition: m.used == 0
fn map_rehash(m: &mut HashIntMap)

Rebuild the table IN PLACE at the same capacity, clearing tombstones and restoring contiguous probe sequences. Call after heavy delete+insert workloads, where tombstone density between automatic grows can degrade lookups toward O(capacity) linear scans. Complexity: O(capacity).

fn map_is_empty(m: &HashIntMap) -> Bool

Check whether the HashIntMap has no entries. Complexity: O(1).

  • Postcondition: result == (map_size(m) == 0)



mapch.xi

type HashMap

Hash map using separate chaining over Int keys and Int values. Bucket heads live in buckets; entries are stored in parallel keys / values / next / live arenas (the flat-arena collect/ pattern). Removed entries are unlinked and flagged dead but stay in the arena, so chain walkers never see them. The table doubles when the load factor exceeds 0.75, re-linking only live entries. O(1) amortized lookups.

Field Type
buckets Vec[Int]
keys Vec[Int]
values Vec[Int]
next Vec[Int]
live Vec[Bool]
count Int
fn hashmap_new() -> HashMap

Create a new empty chaining hash map. Returns: a map with a small initial table and zero entries. Complexity: O(1).

fn hashmap_put(m: &mut HashMap, key: Int, value: Int)

Insert or update key -> value. Params: m - the map; key - Int key; value - Int value. Complexity: O(1) amortized.

fn hashmap_get(m: &HashMap, key: Int) -> Option[Int]

Get the value for a key. None when absent. Params: m - the map; key - Int key. Returns: Some(value) if present, None otherwise. Complexity: O(1) amortized.

fn hashmap_contains(m: &HashMap, key: Int) -> Bool

Check whether a key is present. Params: m - the map; key - Int key. Returns: true if key maps to a value. Complexity: O(1) amortized.

fn hashmap_remove(m: &mut HashMap, key: Int) -> Bool

Remove a key, returning whether it was present. Params: m - the map; key - Int key. Returns: true if the key was present and is now removed. Complexity: O(1) amortized.

fn hashmap_size(m: &HashMap) -> Int

Number of entries. Params: m - the map. Returns: the number of live key/value pairs. Complexity: O(1).

  • Postcondition: result >= 0
fn hashmap_clear(m: &mut HashMap)

Remove all entries. Params: m - the map. Complexity: O(1) (the table is re-initialised; arena memory is retained).

  • Postcondition: hashmap_size(m) == 0



mpmc.xi

type MpmcQueue

Multi-producer, multi-consumer bounded queue.

Field Type
buf Vec[Int]
cap Int
head AtomicInt
tail AtomicInt
fn mpmc_queue_new(capacity: Int) -> MpmcQueue

Create a bounded MPMC queue with capacity slots. Params: capacity - number of buffered slots (clamped to >= 1). Returns: a queue able to hold up to capacity items. Complexity: O(capacity) to pre-fill the ring.

fn mpmc_push(q: &mut MpmcQueue, value: Int) -> Bool

Try to enqueue value. Fails (false) when the queue is full. Params: q - the queue; value - item to enqueue. Returns: true on success, false when full. Complexity: O(1).

fn mpmc_pop(q: &mut MpmcQueue) -> Option[Int]

Try to dequeue a value. None when the queue is empty. Params: q - the queue. Returns: the oldest buffered item, or None when empty. Complexity: O(1).

fn mpmc_size(q: &MpmcQueue) -> Int

Number of buffered elements (approximate under concurrent access). Params: q - the queue. Returns: an approximation of the number of items currently buffered. Complexity: O(1).

  • Postcondition: result >= 0



mpsc.xi

type MpscQueue

Multi-producer, single-consumer queue.

Field Type
buf Vec[Int]
cap Int
head AtomicInt
tail AtomicInt
fn mpsc_queue_new(capacity: Int) -> MpscQueue

Create a bounded MPSC queue with capacity slots. Params: capacity - number of buffered slots (clamped to >= 1). Returns: a queue able to hold up to capacity items. Complexity: O(capacity) to pre-fill the ring.

fn mpsc_push(q: &mut MpscQueue, value: Int) -> Bool

Try to enqueue value from any producer. Fails (false) when full. Params: q - the queue; value - item to enqueue. Returns: true on success, false when full. Complexity: O(1).

fn mpsc_pop(q: &mut MpscQueue) -> Option[Int]

Try to dequeue a value from the single consumer end. None when empty. Params: q - the queue. Returns: the oldest buffered item, or None when empty. Complexity: O(1).

fn mpsc_size(q: &MpscQueue) -> Int

Number of buffered elements (approximate under concurrent access). Params: q - the queue. Returns: an approximation of the number of items currently buffered. Complexity: O(1).

  • Postcondition: result >= 0



objectpool.xi

type ObjectPool

ObjectPool (Int handles 0 .. capacity-1) free is a LIFO stack of released handles; next hands out fresh handles while below capacity. O(1) acquire/release; release validates the handle (double-release is rejected).

Field Type
free Vec[Int]
next Int
capacity Int
fn pool_new(capacity: Int) -> ObjectPool

Create a pool with capacity handles.

fn pool_acquire(p: &mut ObjectPool) -> Option[Int]

Acquire a handle (None when the pool is exhausted).

fn pool_release(p: &mut ObjectPool, handle: Int) -> Bool

Release a handle back to the pool. Returns false on out-of-range or double-release.

fn pool_in_use(p: &ObjectPool) -> Int

Number of handles currently in use.

  • Postcondition: result >= 0
fn pool_available(p: &ObjectPool) -> Int

Number of handles available for acquire.

  • Postcondition: result >= 0
fn pool_capacity(p: &ObjectPool) -> Int

Total capacity.

  • Postcondition: result >= 0



octree.xi

type Octree

Octree spatial index over integer coordinates.

Field Type
root Int
size Int
nx Vec[Int]
ny Vec[Int]
nz Vec[Int]
nw Vec[Int]
nh Vec[Int]
nd Vec[Int]
kids Vec[Int]
phead Vec[Int]
px Vec[Int]
py Vec[Int]
pz Vec[Int]
pv Vec[Int]
pnxt Vec[Int]
fn octree_new() -> Octree

Create a new empty octree (root region starts at (0, 0, 0, 1, 1, 1) and grows on demand). O(1).

fn octree_insert(t: &mut Octree, x: Int, y: Int, z: Int, value: Int)

Insert a point (x, y, z) with its value. Duplicate points are allowed. O(depth) where depth grows logarithmically with the distance from the initial root region.

fn octree_query(t: &Octree, x: Int, y: Int, z: Int) -> Option[Int]

Value stored at the point (x, y, z), or None if no point with those exact coordinates is stored. O(depth).

fn octree_size(t: &Octree) -> Int

Number of stored points. O(1).

  • Postcondition: result >= 0



pairingheap.xi

fn pheap_new() -> PHeap

Create an empty pairing heap. Returns: an empty PHeap-backed heap. Complexity: O(1).

fn pheap_push(h: &mut PHeap, priority: Int)

Insert a priority. Params: h - the heap; priority - Int priority to insert. Complexity: O(log n) amortized.

fn pheap_pop(h: &mut PHeap) -> Option[Int]

Remove and return the minimum priority, or None if the heap is empty. Params: h - the heap. Returns: the minimum priority, or None when empty. Complexity: O(log n) amortized.

fn pheap_peek(h: &PHeap) -> Option[Int]

Return the minimum priority without removing it, or None if empty. Params: h - the heap. Returns: the minimum priority, or None when empty. Complexity: O(1).

fn pheap_size(h: &PHeap) -> Int

Number of priorities in the heap. Params: h - the heap. Returns: the number of reachable priorities. Complexity: O(n) (reachable-node walk).

  • Postcondition: result >= 0
fn pheap_merge(a: &mut PHeap, b: &mut PHeap) -> PHeap

Meld two heaps into one; a and b are consumed. Params: a - the receiving heap; b - the heap to drain. Returns: the merged heap (the same structure as a). Complexity: O(n log n) (drains b via extract-min + insert).

fn pheap_decrease_key(h: &mut PHeap, node: Int, new_priority: Int)

Lower the priority of an existing node. Params: h - the heap; node - arena index of a node allocated by pheap_push; new_priority - the smaller priority. Out-of-range handles and non-decreasing priorities are ignored. The arena is rebuilt afterwards, so all node handles become stale. Complexity: O(n log n) worst-case (full rebuild).

fn pheap_is_empty(h: &PHeap) -> Bool

True if the heap has no priorities. Params: h - the heap. Returns: true when the heap is empty. Complexity: O(1).




persistent.xi

type PVec

Persistent (copy-on-write) collections. Every update returns a new structure and leaves the original intact, enabling cheap immutability and undo/history. Int-valued elements and key/value pairs; accessors return Option[Int].

Field Type
items Vec[Int]
type PMap

Persistent map built on immutable vectors.

Field Type
keys Vec[Int]
values Vec[Int]
fn persistent_vec_new() -> PVec

Create an empty persistent vector. Returns: an empty PVec. Complexity: O(1).

  • Postcondition: result.items.len() == 0
fn pvec_push(v: &PVec, item: Int) -> PVec

Append item, returning a new vector. The input vector is left intact. Params: v - the source vector; item - Int element to append. Returns: a new PVec holding the original elements plus item. Complexity: O(n).

  • Postcondition: result.items.len() == v.items.len() + 1
fn pvec_get(v: &PVec, idx: Int) -> Option[Int]

Element at idx, or None if out of range. Params: v - the vector; idx - zero-based index. Returns: Some(element) if in range, None otherwise. Complexity: O(1).

  • Postcondition: result is Some(_) => idx >= 0 && idx < v.items.len()
  • Postcondition: result is None => idx < 0 || idx >= v.items.len()
fn pvec_len(v: &PVec) -> Int

Number of elements. Params: v - the vector. Returns: the number of elements. Complexity: O(1).

  • Postcondition: result >= 0
fn pvec_update(v: &PVec, idx: Int, value: Int) -> PVec

Replace element at idx, returning a new vector. Params: v - the source vector; idx - zero-based index; value - new element. Returns: a new PVec with value at idx; out-of-range indices yield a copy of v unchanged. Complexity: O(n).

  • Postcondition: result.items.len() == v.items.len()
fn persistent_map_new() -> PMap

Create an empty persistent map. Returns: an empty PMap. Complexity: O(1).

  • Postcondition: result.keys.len() == 0 && result.values.len() == 0
fn pmap_put(m: &PMap, key: Int, value: Int) -> PMap

Insert key/value, returning a new map. The input map is left intact. Params: m - the source map; key - Int key; value - Int value. Returns: a new PMap with the key inserted or updated. Complexity: O(n).

  • Postcondition: result.keys.len() >= m.keys.len()
  • Postcondition: result.keys.len() <= m.keys.len() + 1
fn pmap_get(m: &PMap, key: Int) -> Option[Int]

Value for key, or None. Params: m - the map; key - Int key. Returns: Some(value) if present, None otherwise. Complexity: O(n).

  • Postcondition: result is Some(_) => m.keys.len() > 0
fn pmap_remove(m: &PMap, key: Int) -> PMap

Remove key, returning a new map. The input map is left intact. Params: m - the source map; key - Int key. Returns: a new PMap without key (an equivalent copy if absent). Complexity: O(n).

  • Postcondition: result.keys.len() <= m.keys.len()



priority.xi

type IntMaxHeap

Binary max-heap based priority queue of Int elements backed by the built-in Vec[Int]. pqueue_pop removes the largest element in O(log n); pqueue_peek inspects it in O(1). None on an empty queue.

Field Type
data Vec[Int]
fn pqueue_new() -> IntMaxHeap

Create a new empty priority queue. O(1).

fn pqueue_push(q: &mut IntMaxHeap, value: Int)

Insert value into the queue. O(log n).

fn pqueue_pop(q: &mut IntMaxHeap) -> Option[Int]

Remove and return the highest-priority (largest) element. None if empty. O(log n).

fn pqueue_peek(q: &IntMaxHeap) -> Option[Int]

Return the highest-priority element without removing it. None if empty. O(1).

fn pqueue_len(q: &IntMaxHeap) -> Int

Number of elements in the queue. O(1).

  • Postcondition: result >= 0
fn pqueue_is_empty(q: &IntMaxHeap) -> Bool

True if the queue holds no elements. O(1).

  • Postcondition: result == (pqueue_len(q) == 0)



quadtree.xi

type Quadtree

Quadtree spatial index over integer coordinates.

Field Type
root Int
size Int
nx Vec[Int]
ny Vec[Int]
nw Vec[Int]
nh Vec[Int]
kids Vec[Int]
phead Vec[Int]
px Vec[Int]
py Vec[Int]
pv Vec[Int]
pnxt Vec[Int]
fn quadtree_new() -> Quadtree

Create a new empty quadtree (root region starts at (0, 0, 1, 1) and grows on demand). O(1).

fn quadtree_insert(t: &mut Quadtree, x: Int, y: Int, value: Int)

Insert a point (x, y) with its value. Duplicate points are allowed. O(depth) where depth grows logarithmically with the distance from the initial root region.

fn quadtree_query(t: &Quadtree, x: Int, y: Int) -> Option[Int]

Value stored at the point (x, y), or None if no point with those exact coordinates is stored. O(depth).

fn quadtree_size(t: &Quadtree) -> Int

Number of stored points. O(1).

  • Postcondition: result >= 0



queue.xi

type WorkQueue

WorkQueue (Int items) A FIFO queue backed by a Vec plus a head offset. push appends at the end, pop/peek read from head. Popped entries are left in place (no compaction) so all operations stay O(1).

Field Type
items Vec[Int]
head Int
fn workqueue_new() -> WorkQueue

Create an empty work queue.

  • Postcondition: result.head == 0
fn workqueue_push(q: &mut WorkQueue, item: Int)

Append an item to the back of the queue.

fn workqueue_pop(q: &mut WorkQueue) -> Option[Int]

Remove and return the front item. None if empty.

  • Postcondition: result is Some(_) => workqueue_len(q) == workqueue_len(q)@pre - 1
  • Postcondition: result is None => workqueue_len(q) == workqueue_len(q)@pre
fn workqueue_peek(q: &WorkQueue) -> Option[Int]

Return the front item without removing it. None if empty.

  • Postcondition: result.is_some == (workqueue_len(q) > 0)
fn workqueue_len(q: &WorkQueue) -> Int

Number of items currently in the queue.

  • Postcondition: result >= 0
fn workqueue_is_empty(q: &WorkQueue) -> Bool

True if the queue contains no items.

  • Postcondition: result == (workqueue_len(q) == 0)
type Deque

Deque (Int items) A double-ended queue backed by a Vec with head/tail offsets. Pushes append, pops advance the offsets. deque_push_front rebuilds the active range ([head, tail)) into a fresh Vec so no stale entries leak in.

Field Type
items Vec[Int]
head Int
tail Int
fn deque_new() -> Deque

Create an empty deque.

  • Postcondition: result.head == 0 && result.tail == 0
fn deque_push_back(d: &mut Deque, item: Int)

Append an item to the back of the deque.

fn deque_push_front(d: &mut Deque, item: Int)

Prepend an item to the front of the deque.

fn deque_pop_front(d: &mut Deque) -> Option[Int]

Remove and return the front item. None if empty.

  • Postcondition: result is Some(_) => deque_len(d) == deque_len(d)@pre - 1
  • Postcondition: result is None => deque_len(d) == deque_len(d)@pre
fn deque_pop_back(d: &mut Deque) -> Option[Int]

Remove and return the back item. None if empty.

  • Postcondition: result is Some(_) => deque_len(d) == deque_len(d)@pre - 1
  • Postcondition: result is None => deque_len(d) == deque_len(d)@pre
fn deque_len(d: &Deque) -> Int

Number of items currently in the deque.

  • Postcondition: result >= 0
fn deque_is_empty(d: &Deque) -> Bool

True if the deque contains no items.

  • Postcondition: result == (deque_len(d) == 0)
type SpscRing

SpscRing -- lock-free single-producer / single-consumer ring buffer (2026-08-11). Fixed cap slots (power of two not required; modulo via %). head = next slot to pop, tail = next slot to push, both AtomicInt (fetch_add based). Producer and consumer must each be used from exactly one thread. When full, push returns false without blocking; when empty, pop returns None. Slot reuse races are bounded by the documented usage contract (SPSC); a "full" or "empty" state read by the OTHER side may lag one operation, which is safe for SPSC.

Field Type
buf Vec[Int]
cap Int
head AtomicInt
tail AtomicInt
fn spsc_ring_new(cap: Int) -> SpscRing

Create an spsc ring with cap slots.

  • Postcondition: result.cap == cap
fn spsc_ring_push(r: &mut SpscRing, item: Int) -> Bool

Push item from the producer side. Returns false when the ring is full.

fn spsc_ring_pop(r: &mut SpscRing) -> Option[Int]

Pop an item from the consumer side. None when empty.

fn spsc_ring_len(r: &SpscRing) -> Int

Number of items currently in the ring (approximate under concurrency).

  • Postcondition: result >= 0
fn spsc_ring_is_empty(r: &SpscRing) -> Bool

True when the ring is empty (approximate under concurrency).

  • Postcondition: result == (spsc_ring_len(r) == 0)
fn spsc_ring_capacity(r: &SpscRing) -> Int

Capacity (number of slots).

  • Postcondition: result >= 0



radix.xi

type RadixTrie

Compressed prefix tree over decimal digit strings mapping keys to Int values.

Flat-arena style. Every node carries the label of its incoming edge (labels[i], the empty string at the root), a terminal flag plus the stored key/value for nodes that end a key, and a child list threaded through child_head[i] / sibling[i] (linked list of child node ids). Insertion follows the classic radix-trie algorithm: match a child whose label shares a prefix with the remaining key, split that label at the divergence point, and re-link the pieces. Removal marks a terminal node non-terminal (the node itself and its labels stay, so no recompaction is needed). All string reads go through xiom.string; Vec[Str] elements are bound to locals before comparison (compiler BUG 8 workaround).

Field Type
root Int
size Int
labels Vec[Str]
terminal Vec[Bool]
keys Vec[Str]
values Vec[Int]
child_head Vec[Int]
sibling Vec[Int]
fn radix_new() -> RadixTrie

Create a new empty radix trie (root node only). O(1).

fn radix_insert(r: &mut RadixTrie, key: Str, value: Int)

Insert key with its value. Empty keys are rejected. Inserting an existing key is a no-op (the original value is kept). O(L) where L is the key length (amortized).

fn radix_contains(r: &RadixTrie, key: Str) -> Bool

Check whether key is stored (exact match). Empty keys are absent. O(L).

fn radix_remove(r: &mut RadixTrie, key: Str) -> Bool

Remove key, returning whether it was present. The node is marked non-terminal; its label and children remain in the arena. O(L).

fn radix_longest_prefix(r: &RadixTrie, key: Str) -> Int

Length of the longest stored key that is a prefix of key (0 if none). O(L).

  • Postcondition: result >= 0
fn radix_size(r: &RadixTrie) -> Int

Number of stored keys. O(1).

  • Postcondition: result >= 0



range.xi

type IntervalSet

Interval tree storing Int intervals with values, supporting point queries.

R44 same-leaf: the public type leaf here is IntervalSet (renamed from IntervalTree, which collided with the real tree in collect/interval.xi). Function names stay interval_*; both modules share the call surface, so always use the module you call.

Flat-arena style. Intervals are stored in insertion order in parallel Vec[Int]s (starts/ends/vals) with a parallel liveness flag alive. Point queries scan the intervals and return the values of the live intervals covering the point; removal marks the first matching interval dead (lazy deletion). This keeps the API simple and insertion/removal O(1) amortized at the cost of O(n) queries, which is appropriate for the small interval sets this module targets. Intervals are inclusive on both ends; start > end intervals are rejected by insert.

Field Type
starts Vec[Int]
ends Vec[Int]
vals Vec[Int]
alive Vec[Bool]
fn interval_tree_new() -> IntervalSet

Create a new empty interval tree. O(1).

fn interval_insert(t: &mut IntervalSet, start: Int, end: Int, value: Int)

Insert an interval with its value. Duplicate intervals are allowed; an interval with start > end is rejected (ignored). O(1) amortized.

fn interval_query(t: &IntervalSet, point: Int) -> Vec[Int]

Values of the live intervals covering point (inclusive on both ends). O(n).

fn interval_remove(t: &mut IntervalSet, start: Int, end: Int) -> Bool

Remove the first live interval matching [start, end]. Returns true if one was found and removed. O(n).




rbtree.xi

type RbTree

Red-black tree (Int keys, Int values). Self-balancing BST with a color bit per node (1 = red, 0 = black; null is black) that guarantees O(log n) insert, delete and lookup. Flat-arena representation (the established collect/ pattern): nodes live in parallel Vec[Int]s (keys/values/ left/right/parent/colors) addressed by a root index; -1 is the "no node" sentinel. Duplicate keys are rejected; inorder/preorder/ postorder return the keys. Removed nodes become unreachable arena entries.

Field Type
root Int
keys Vec[Int]
values Vec[Int]
left Vec[Int]
right Vec[Int]
parent Vec[Int]
colors Vec[Int]
size Int
fn rbtree_new() -> RbTree

Create an empty red-black tree. O(1).

  • Postcondition: result.size == 0
fn rbtree_insert(t: &mut RbTree, key: Int, value: Int) -> Bool

Insert key -> value; returns false if the key already exists. O(log n).

  • Postcondition: rbtree_contains(t, key) == true
  • Postcondition: result == true => rbtree_size(t) == rbtree_size(t)@pre + 1
  • Postcondition: result == false => rbtree_size(t) == rbtree_size(t)@pre
fn rbtree_get(t: &RbTree, key: Int) -> Option[Int]

Value for key, or None if absent. O(log n).

  • Postcondition: result.is_some == rbtree_contains(t, key)
fn rbtree_contains(t: &RbTree, key: Int) -> Bool

True if key is present. O(log n).

fn rbtree_remove(t: &mut RbTree, key: Int) -> Bool

Remove key; returns true if it was present. O(log n).

  • Postcondition: rbtree_contains(t, key) == false
  • Postcondition: result == true => rbtree_size(t) == rbtree_size(t)@pre - 1
  • Postcondition: result == false => rbtree_size(t) == rbtree_size(t)@pre
fn rbtree_size(t: &RbTree) -> Int

Number of keys. O(1).

  • Postcondition: result >= 0
fn rbtree_min(t: &RbTree) -> Option[Int]

Smallest key, or None if the tree is empty. O(log n).

  • Postcondition: result.is_some == (rbtree_size(t) > 0)
fn rbtree_max(t: &RbTree) -> Option[Int]

Largest key, or None if the tree is empty. O(log n).

  • Postcondition: result.is_some == (rbtree_size(t) > 0)
fn rbtree_inorder(t: &RbTree) -> Vec[Int]

Keys in ascending order. O(n).

  • Postcondition: result.len() == rbtree_size(t)
fn rbtree_preorder(t: &RbTree) -> Vec[Int]

Keys in preorder (node, left, right). O(n).

  • Postcondition: result.len() == rbtree_size(t)
fn rbtree_postorder(t: &RbTree) -> Vec[Int]

Keys in postorder (left, right, node). O(n).

  • Postcondition: result.len() == rbtree_size(t)



ring.xi

type RingBuffer

Bounded single-producer single-consumer ring buffer of Int elements. Fixed cap slots; head/tail are monotonic counters, the slot index is (counter % cap). When full, push returns false without blocking; when empty, pop returns None. NOTE: the reference collect.queue SpscRing uses AtomicInt counters; this module keeps the "Depends on: none" contract and uses plain Int counters, which are exactly equivalent for the SPSC single-threaded contract exercised by the smoke tests.

Field Type
buf Vec[Int]
cap Int
head Int
tail Int
fn ring_new(cap: Int) -> RingBuffer

Create a ring with cap slots. A capacity below 1 is clamped to 1. O(cap).

fn ring_push(r: &mut RingBuffer, value: Int) -> Bool

Try to enqueue value; returns false when the ring is full. O(1).

fn ring_pop(r: &mut RingBuffer) -> Option[Int]

Dequeue a value. None when the ring is empty. O(1).

fn ring_len(r: &RingBuffer) -> Int

Number of buffered elements. O(1).

  • Postcondition: result >= 0
fn ring_is_empty(r: &RingBuffer) -> Bool

True when the ring holds no elements. O(1).

  • Postcondition: result == (ring_len(r) == 0)
fn ring_capacity(r: &RingBuffer) -> Int

Maximum number of buffered elements. O(1).

  • Postcondition: result >= 0



segment.xi

type SegTree

Segment tree over an Int array (0-based indices). Builds in O(n), supports point updates and range queries (sum, min, max) in O(log n). Indices are inclusive; out-of-range queries return identity values (0 for sum, INT_MAX for min, INT_MIN for max).

Flat-arena style. The tree is stored in three parallel Vec[Int]s of size 4n (sums, mins, maxs) using the classic recursive heap layout: node k covers [l, r] with children 2k+1 and 2k+2. Leaves hold a single slot, internal nodes pull from their children. Out-of-range update indices are rejected (no-op); out-of-range queries are clamped and return the identity value when the clamped range is empty.

Field Type
n Int
sums Vec[Int]
mins Vec[Int]
maxs Vec[Int]
fn segtree_new(n: Int) -> SegTree

Create a segment tree over n zero slots. Out-of-range values clamp to 0. O(n) time, O(4n) memory.

fn segtree_build(t: &mut SegTree, values: &Vec[Int])

Build internal nodes from the given values. The tree is resized to match the values length (0-length input leaves the tree empty). O(n).

fn segtree_update(t: &mut SegTree, idx: Int, value: Int)

Set slot idx to value. Out-of-range indices are ignored. O(log n).

fn segtree_query_sum(t: &SegTree, l: Int, r: Int) -> Int

Sum over [l, r] inclusive. Out-of-range queries are clamped; an empty clamped range returns 0 (the sum identity). O(log n).

fn segtree_query_min(t: &SegTree, l: Int, r: Int) -> Int

Minimum over [l, r] inclusive. An empty clamped range returns INT_MAX (the min identity). O(log n).

fn segtree_query_max(t: &SegTree, l: Int, r: Int) -> Int

Maximum over [l, r] inclusive. An empty clamped range returns INT_MIN (the max identity). O(log n).

fn segtree_size(t: &SegTree) -> Int

Number of slots in the tree. O(1).

  • Postcondition: result >= 0



skiplist.xi

type SkipList

Skip list over Int keys.

Field Type
head Int
keys Vec[Int]
nexts Vec[Int]
size Int
rng Int
fn skiplist_new() -> SkipList

Create an empty skip list (header node with key INT_MIN).

fn skiplist_insert(l: &mut SkipList, key: Int) -> Bool

Insert key. Returns false if the key already exists.

fn skiplist_contains(l: &SkipList, key: Int) -> Bool

True if key is present.

fn skiplist_remove(l: &mut SkipList, key: Int) -> Bool

Remove key. Returns true if it was present.

fn skiplist_size(l: &SkipList) -> Int

Number of keys.

  • Postcondition: result >= 0
fn skiplist_min(l: &SkipList) -> Option[Int]

Smallest key (None if empty).

fn skiplist_max(l: &SkipList) -> Option[Int]

Largest key (None if empty).




sparse.xi

type SparseSet

Sparse set of unique Int elements with O(1) add, remove and membership checks over dense Int universes.

Classic two-array representation: sparse[value] holds the index of value inside dense, and dense holds the set members in an arbitrary but stable order. Removal swaps the last element into the removed slot, so all three core operations are O(1). The sparse array grows on demand to cover the largest inserted value; negative values cannot be indexed and are therefore rejected by sparse_add (documented, no silent failure).

Field Type
sparse Vec[Int]
dense Vec[Int]
fn sparse_set_new() -> SparseSet

Create a new empty sparse set. O(1).

fn sparse_add(s: &mut SparseSet, value: Int)

Add a value to the set (no-op if already present). Negative values are rejected (they cannot be indexed in the sparse array). O(1) amortized.

fn sparse_contains(s: &SparseSet, value: Int) -> Bool

Check whether a value is present. O(1).

fn sparse_remove(s: &mut SparseSet, value: Int)

Remove a value from the set (no-op if absent). O(1) amortized.

fn sparse_size(s: &SparseSet) -> Int

Number of elements in the set. O(1).

  • Postcondition: result >= 0
fn sparse_iter(s: &SparseSet) -> Vec[Int]

Iterate all elements (arbitrary but stable order). O(n).




spatial.xi

type KdTree

KD-tree (2D Int points with values)

Field Type
root Int
size Int
xs Vec[Int]
ys Vec[Int]
vals Vec[Int]
left Vec[Int]
right Vec[Int]
fn kdtree_new() -> KdTree

Create an empty KD-tree. O(1).

  • Postcondition: result.size == 0
fn kdtree_insert(t: &mut KdTree, x: Int, y: Int, value: Int)

Insert a 2D point (x, y) with its value. Duplicates are allowed. O(h) expected, O(n) worst case.

  • Postcondition: kdtree_size(t) == kdtree_size(t)@pre + 1
fn kdtree_nearest(t: &KdTree, x: Int, y: Int) -> Option[Int]

Value of the closest point to (x, y), or None if the tree is empty. O(n) worst case, O(log n) expected.

  • Postcondition: result is Some(_) => kdtree_size(t) > 0
  • Postcondition: result is None => kdtree_size(t) == 0
fn kdtree_range(t: &KdTree, x1: Int, y1: Int, x2: Int, y2: Int) -> Vec[Int]

Values of the points inside the rectangle [x1, x2] x [y1, y2] (inclusive). O(n) worst case.

  • Postcondition: result.len() <= kdtree_size(t)
fn kdtree_size(t: &KdTree) -> Int

Number of points in the tree. O(1).

  • Postcondition: result >= 0
type Quadtree

Quadtree spatial index over integer coordinates.

Field Type
root Int
size Int
nx Vec[Int]
ny Vec[Int]
nw Vec[Int]
nh Vec[Int]
kids Vec[Int]
phead Vec[Int]
px Vec[Int]
py Vec[Int]
pv Vec[Int]
pnxt Vec[Int]
fn quadtree_new(x: Int, y: Int, w: Int, h: Int) -> Quadtree

Create a quadtree for the given bounds (top-left (x, y), size (w, h)). O(1).

  • Postcondition: result.size == 0
fn quadtree_insert(q: &mut Quadtree, x: Int, y: Int, value: Int) -> Bool

Insert a 2D point (x, y) with its value. Returns false if the point lies outside the quadtree bounds. O(depth).

  • Postcondition: result == true => quadtree_size(q) == quadtree_size(q)@pre + 1
  • Postcondition: result == false => quadtree_size(q) == quadtree_size(q)@pre
fn quadtree_query(q: &Quadtree, x1: Int, y1: Int, x2: Int, y2: Int) -> Vec[Int]

Values of the points inside the rectangle [x1, x2] x [y1, y2] (inclusive). O(n) worst case.

  • Postcondition: result.len() <= quadtree_size(q)
fn quadtree_size(q: &Quadtree) -> Int

Number of points in the tree. O(1).

  • Postcondition: result >= 0
type Octree

Octree (fixed bounds, 3D)

Field Type
root Int
size Int
nx Vec[Int]
ny Vec[Int]
nz Vec[Int]
nw Vec[Int]
nh Vec[Int]
nd Vec[Int]
kids Vec[Int]
phead Vec[Int]
px Vec[Int]
py Vec[Int]
pz Vec[Int]
pv Vec[Int]
pnxt Vec[Int]
fn octree_new(x: Int, y: Int, z: Int, w: Int, h: Int, d: Int) -> Octree

Create an octree for the given bounds (corner (x, y, z), size (w, h, d)). O(1).

  • Postcondition: result.size == 0
fn octree_insert(o: &mut Octree, x: Int, y: Int, z: Int, value: Int) -> Bool

Insert a 3D point (x, y, z) with its value. Returns false if the point lies outside the octree bounds. O(depth).

  • Postcondition: result == true => octree_size(o) == octree_size(o)@pre + 1
  • Postcondition: result == false => octree_size(o) == octree_size(o)@pre
fn octree_query(o: &Octree, x1: Int, y1: Int, z1: Int, x2: Int, y2: Int, z2: Int) -> Vec[Int]

Values of the points inside the box [x1, x2] x [y1, y2] x [z1, z2] (inclusive). O(n) worst case.

  • Postcondition: result.len() <= octree_size(o)
fn octree_size(o: &Octree) -> Int

Number of points in the tree. O(1).

  • Postcondition: result >= 0



spmc.xi

type SpmcQueue

Single-producer, multi-consumer queue.

Field Type
buf Vec[Int]
cap Int
head AtomicInt
tail AtomicInt
fn spmc_queue_new(capacity: Int) -> SpmcQueue

Create a bounded SPMC queue with capacity slots. Params: capacity - number of buffered slots (clamped to >= 1). Returns: a queue able to hold up to capacity items. Complexity: O(capacity) to pre-fill the ring.

fn spmc_push(q: &mut SpmcQueue, value: Int) -> Bool

Try to enqueue value from the single producer end. Fails (false) when full. Params: q - the queue; value - item to enqueue. Returns: true on success, false when full. Complexity: O(1).

fn spmc_pop(q: &mut SpmcQueue) -> Option[Int]

Try to dequeue a value from any consumer. None when empty. Params: q - the queue. Returns: the oldest buffered item, or None when empty. Complexity: O(1).

fn spmc_size(q: &SpmcQueue) -> Int

Number of buffered elements (approximate under concurrent access). Params: q - the queue. Returns: an approximation of the number of items currently buffered. Complexity: O(1).

  • Postcondition: result >= 0



stack.xi

type Stack

LIFO stack of Int elements backed by the built-in Vec[Int]. All operations are O(1); stack_pop/stack_peek return None on an empty stack.

Field Type
items Vec[Int]
fn stack_new() -> Stack

Create a new empty stack. O(1).

fn stack_push(s: &mut Stack, value: Int)

Push value onto the top of the stack. O(1).

fn stack_pop(s: &mut Stack) -> Option[Int]

Remove and return the top value. None if the stack is empty. O(1).

fn stack_peek(s: &Stack) -> Option[Int]

Return the top value without removing it. None if empty. O(1).

fn stack_len(s: &Stack) -> Int

Number of elements on the stack. O(1).

  • Postcondition: result >= 0
fn stack_is_empty(s: &Stack) -> Bool

True if the stack holds no elements. O(1).

  • Postcondition: result == (stack_len(s) == 0)
fn stack_clear(s: &mut Stack)

Remove all elements. O(1) (capacity is retained).

  • Postcondition: stack_len(s) == 0



stringmap.xi

type StringMap

Insertion-ordered string-keyed map.

Field Type
buckets Vec[Int]
keys Vec[Str]
values Vec[Int]
next Vec[Int]
live Vec[Bool]
count Int
fn string_map_new() -> StringMap

Create a new empty string map. Returns: a map with a small initial table and zero entries. Complexity: O(1).

  • Postcondition: result.count == 0
fn string_map_put(m: &mut StringMap, key: Str, value: Int)

Insert or update key -> value. Params: m - the map; key - Str key; value - Int value. Re-inserting an existing key updates its value. Complexity: O(1) amortized.

  • Postcondition: m.count >= 1
fn string_map_get(m: &StringMap, key: Str) -> Option[Int]

Get the value for a key. None when absent. Params: m - the map; key - Str key. Returns: Some(value) if present, None otherwise. Complexity: O(1) amortized.

fn string_map_contains(m: &StringMap, key: Str) -> Bool

Check whether a key is present. Params: m - the map; key - Str key. Returns: true if key maps to a value. Complexity: O(1) amortized.

fn string_map_remove(m: &mut StringMap, key: Str)

Remove a key. Params: m - the map; key - Str key. Absent keys are a no-op. Arena memory is retained. Complexity: O(1) amortized.

  • Postcondition: m.count >= 0
fn string_map_size(m: &StringMap) -> Int

Number of entries. Params: m - the map. Returns: the number of live key/value pairs. Complexity: O(1).

  • Postcondition: result >= 0



threadpool.xi

type ThreadPool

Thread pool. Spawns a fixed number of worker threads that drain a shared job queue. pool_submit enqueues a closure; pool_join waits for all pending jobs to finish; pool_shutdown stops the workers and releases their threads.

Pure-XIOM data structure (no OS threads): the pool tracks workers worker slots, an idle/busy split and a FIFO queue of Int job handles. Each submit hands the job to an idle worker if one is free (busy++), otherwise the handle waits in the queue; pool_join completes every pending job instantly (no real work runs) and returns all workers to idle. Submit after shutdown returns false.

Field Type
workers Int
idle Int
busy Int
queued Vec[Int]
next_id Int
completed Int
closed Bool
fn thread_pool_new(workers: Int) -> ThreadPool

Create a pool with workers worker slots. Params: workers - fixed number of workers (clamped to >= 1). Returns: a new pool with all workers idle and no pending jobs. Complexity: O(1).

fn pool_submit(p: &mut ThreadPool, job: fn() -> Unit) -> Bool

Enqueue a job; false if the pool is shut down. Params: p - the pool; job - a closure (accepted but not executed; the pool is a pure-XIOM simulation over Int job handles). Returns: true on acceptance, false if the pool is shut down. Complexity: O(1) amortized.

fn pool_join(p: &mut ThreadPool)

Wait until all submitted jobs have completed. Params: p - the pool. Completes every queued job (they finish immediately in the simulation) and returns all workers to the idle state. Complexity: O(n) where n is the number of pending jobs.

fn pool_shutdown(p: &mut ThreadPool)

Stop workers and release threads. Params: p - the pool. Closes the pool (submit returns false afterwards) and drains the pending queue as pool_join does. Complexity: O(n) where n is the number of pending jobs.

fn pool_size(p: &ThreadPool) -> Int

Number of worker threads. Params: p - the pool. Returns: the fixed worker count. Complexity: O(1).

  • Postcondition: result >= 0
fn pool_idle_count(p: &ThreadPool) -> Int

Number of workers currently idle. Params: p - the pool. Returns: workers not currently assigned a job. Complexity: O(1).

  • Postcondition: result >= 0
fn pool_busy_count(p: &ThreadPool) -> Int

Number of workers currently running a job. Params: p - the pool. Returns: workers currently assigned a job (does not include queued work). Complexity: O(1).

  • Postcondition: result >= 0



tinylfu.xi

type CountMinSketch

TinyLFU admission filter for caches. Uses a count-min sketch (CMS) of estimated access frequencies to decide whether an incoming key should displace an existing one. Includes the underlying CMS primitives as the building block; tinylfu_reset halves all counters to avoid saturation.

Field Type
width Int
depth Int
counts Vec[Int]
type TinyLfu

TinyLFU admission filter over a count-min sketch.

Field Type
sketch CountMinSketch
capacity Int
fn count_min_sketch_new(width: Int, depth: Int) -> CountMinSketch

Create a count-min sketch with width counters per row and depth rows. Params: width - counters per row (clamped to >= 1); depth - number of independent hash rows (clamped to >= 1). Returns: a zeroed sketch. Complexity: O(width * depth).

  • Postcondition: result.width >= 1
  • Postcondition: result.depth >= 1
  • Postcondition: result.counts.len() == result.width * result.depth
fn cms_add(sketch: &mut CountMinSketch, key: Int)

Increment the count of key in every row. Params: sketch - the CMS; key - Int key to record one access for. Complexity: O(depth).

  • Postcondition: cms_estimate(sketch, key) >= 1
fn cms_estimate(sketch: &CountMinSketch, key: Int) -> Int

Estimated count of key (minimum over rows). Never underestimates. Params: sketch - the CMS; key - Int key. Returns: the minimum row count, which is >= the true count. Complexity: O(depth).

  • Postcondition: result >= 0
fn cms_clear(sketch: &mut CountMinSketch)

Zero all counters. Params: sketch - the CMS. Complexity: O(width * depth).

  • Postcondition: cms_estimate(sketch, 0) == 0
fn tinylfu_new(capacity: Int) -> TinyLfu

Create a TinyLFU filter sized for capacity cache entries. Params: capacity - expected number of cache entries; the CMS is sized with width = max(8, 4 * capacity) and 4 rows. Returns: a TinyLfu admission filter. Complexity: O(capacity).

  • Postcondition: result.capacity >= 1
  • Postcondition: result.sketch.depth >= 1
fn tinylfu_estimate(f: &TinyLfu, key: Int) -> Int

Estimated access frequency of key. Params: f - the filter; key - Int key. Returns: the CMS estimate for the key (never underestimates). Complexity: O(1) with a constant number of rows.

  • Postcondition: result >= 0
fn tinylfu_increment(f: &mut TinyLfu, key: Int)

Record one access for key. Params: f - the filter; key - Int key. Complexity: O(1) with a constant number of rows.

  • Postcondition: tinylfu_estimate(f, key) >= 1
fn tinylfu_admit(f: &TinyLfu, key: Int, frequency: Int) -> Bool

True if key should be admitted over the competing entry. Params: f - the filter; key - the incoming key; frequency - the estimated frequency of the entry it would displace (e.g. the eviction candidate). Returns: true when the sketch's estimate for key is at least frequency (TinyLFU admission rule: keep the hotter key). Complexity: O(1) with a constant number of rows.

  • Postcondition: result == (tinylfu_estimate(f, key) >= frequency)
fn tinylfu_reset(f: &mut TinyLfu)

Halve all frequency estimates to avoid saturation. Params: f - the filter. Complexity: O(width * depth).

  • Postcondition: tinylfu_estimate(f, 0) <= tinylfu_estimate(f, 0)@pre



tree.xi

type Bst

Binary Search Tree (Int keys) Arena representation: nodes live in parallel Vec[Int]s, addressed by a root index. The sentinel index -1 denotes "no node". Removed nodes become unreachable arena entries; all queries traverse the reachable tree.

Field Type
root Int
keys Vec[Int]
left Vec[Int]
right Vec[Int]
fn bst_new() -> Bst

Create an empty BST.

  • Postcondition: result.root == -1
fn bst_insert(b: &mut Bst, key: Int)

Insert a key. Duplicates are ignored.

fn bst_contains(b: &Bst, key: Int) -> Bool

Returns true if the key is present.

fn bst_remove(b: &mut Bst, key: Int) -> Bool

Remove a key. Two-child nodes are replaced by their in-order successor. Returns true if the key was found and removed.

  • Postcondition: bst_contains(b, key) == false
  • Postcondition: result == true => bst_size(b) == bst_size(b)@pre - 1
  • Postcondition: result == false => bst_size(b) == bst_size(b)@pre
fn bst_size(b: &Bst) -> Int

Number of reachable nodes.

  • Postcondition: result >= 0
fn bst_min(b: &Bst) -> Option[Int]

Minimum key, or None if the tree is empty.

  • Postcondition: result.is_some == (bst_size(b) > 0)
fn bst_max(b: &Bst) -> Option[Int]

Maximum key, or None if the tree is empty.

  • Postcondition: result.is_some == (bst_size(b) > 0)
fn bst_inorder(b: &Bst) -> Vec[Int]

In-order traversal as a sorted vector.

  • Postcondition: result.len() == bst_size(b)
fn bst_height(b: &Bst) -> Int

Height of the tree; empty tree has height 0.

  • Postcondition: result >= 0
fn bst_is_bst(b: &Bst) -> Bool

True if the in-order traversal is strictly sorted (a valid BST).

type Avl

AVL Tree (Int keys) Same arena layout as the BST plus a parallel heights vector. Node height: leaf = 1, empty subtree = 0. Every insert rebalances via single/double rotations so |bf| <= 1 holds on every node.

Field Type
root Int
keys Vec[Int]
left Vec[Int]
right Vec[Int]
heights Vec[Int]
fn avl_new() -> Avl

Create an empty AVL tree.

  • Postcondition: result.root == -1
fn avl_insert(a: &mut Avl, key: Int)

Insert a key. Duplicates are ignored.

fn avl_contains(a: &Avl, key: Int) -> Bool

Returns true if the key is present.

fn avl_size(a: &Avl) -> Int

Number of nodes in the tree.

  • Postcondition: result >= 0
fn avl_inorder(a: &Avl) -> Vec[Int]

In-order traversal as a sorted vector.

  • Postcondition: result.len() == avl_size(a)
fn avl_height(a: &Avl) -> Int

Height of the tree; empty tree has height 0.

  • Postcondition: result >= 0



treemap.xi

type BTreeMap

Balanced binary search tree map keeping Int keys in sorted order. The balance policy is AVL (the proven collect.tree pattern) so put/get/ contains/remove run in O(log n). Flat-arena representation: nodes live in parallel Vec[Int]s (keys/values/left/right/heights) addressed by a root index; -1 is the "no node" sentinel. treemap_iter returns (key, value) pairs in ascending key order. Removed nodes become unreachable arena entries.

Field Type
root Int
keys Vec[Int]
values Vec[Int]
left Vec[Int]
right Vec[Int]
heights Vec[Int]
size Int
fn treemap_new() -> BTreeMap

Create a new empty tree map. O(1).

fn treemap_put(m: &mut BTreeMap, key: Int, value: Int)

Insert or update key -> value. O(log n).

fn treemap_get(m: &BTreeMap, key: Int) -> Option[Int]

Value for key, or None when absent. O(log n).

fn treemap_contains(m: &BTreeMap, key: Int) -> Bool

True if key is present. O(log n).

fn treemap_remove(m: &mut BTreeMap, key: Int) -> Bool

Remove key; returns true if it was present. O(log n).

fn treemap_size(m: &BTreeMap) -> Int

Number of entries. O(1).

  • Postcondition: result >= 0
fn treemap_min(m: &BTreeMap) -> Option[Int]

Smallest key, or None when the map is empty. O(log n).

fn treemap_max(m: &BTreeMap) -> Option[Int]

Largest key, or None when the map is empty. O(log n).

fn treemap_iter(m: &BTreeMap) -> Vec[(Int, Int)]

All entries as (key, value) pairs in ascending key order. O(n).




treeset.xi

type BTreeSet

Balanced binary search tree set keeping Int elements in sorted order. The balance policy is AVL (the proven collect.tree pattern) so insert/ contains/remove run in O(log n). Flat-arena representation: nodes live in parallel Vec[Int]s (keys/left/right/heights) addressed by a root index; -1 is the "no node" sentinel. Removed nodes become unreachable arena entries.

Field Type
root Int
keys Vec[Int]
left Vec[Int]
right Vec[Int]
heights Vec[Int]
size Int
fn treeset_new() -> BTreeSet

Create a new empty tree set. O(1).

fn treeset_insert(s: &mut BTreeSet, value: Int) -> Bool

Insert value; returns true if it was newly added, false if it was already present. O(log n).

fn treeset_contains(s: &BTreeSet, value: Int) -> Bool

True if value is present. O(log n).

fn treeset_remove(s: &mut BTreeSet, value: Int) -> Bool

Remove value; returns true if it was present. O(log n).

fn treeset_size(s: &BTreeSet) -> Int

Number of elements. O(1).

  • Postcondition: result >= 0
fn treeset_min(s: &BTreeSet) -> Option[Int]

Smallest element, or None when the set is empty. O(log n).

fn treeset_max(s: &BTreeSet) -> Option[Int]

Largest element, or None when the set is empty. O(log n).




trie.xi

type Trie

Trie (Str keys, lowercase a-z only; other chars are rejected) Flat-arena style (the established collect/ pattern -- tree.xi/graph.xi use parallel Vec[Int]s because Vec-of-struct instantiations collide at startup in combined programs, COMPILER_BUGS.md BUG 16). Node n's child for letter c is children[n * 26 + c] (-1 = none); ends[n] is 1 for a complete word. trie_complete returns all words with a prefix, in DFS lexicographic order. Node 0 is the root.

Field Type
children Vec[Int]
ends Vec[Int]
size Int
fn trie_new() -> Trie

Create an empty trie (root node allocated).

fn trie_insert(t: &mut Trie, word: Str) -> Bool

Insert a lowercase word. Returns false if the word already exists or contains non a-z characters.

fn trie_contains(t: &Trie, word: Str) -> Bool

True if word is stored (exact match).

fn trie_size(t: &Trie) -> Int

Number of words stored.

  • Postcondition: result >= 0
fn trie_complete(t: &Trie, prefix: Str) -> Vec[Str]

All stored words starting with prefix (lexicographic DFS order). Returns an empty Vec if no word matches.

fn trie_has_prefix(t: &Trie, prefix: Str) -> Bool

True if any stored word starts with prefix.

fn trie_remove(t: &mut Trie, word: Str) -> Bool

Remove word. Returns true if it was present.




unionfind.xi

type UnionFind

Disjoint-set (union-find) over Int element ids with path compression and union by size.

Flat-arena style: parent[i] points at the parent of element i (a root points at itself), size[i] is the component size valid at the roots, and count tracks the number of disjoint sets. uf_find applies path compression (both passes) and takes &mut; the immutable read-only traversal uf_find_no_compress backs uf_connected / uf_component_size / uf_components so they accept &UnionFind. Union by size keeps trees shallow, giving ~O(alpha n) amortized operations. Out-of-range element ids are rejected (no silent failure).

Field Type
parent Vec[Int]
size Vec[Int]
count Int
fn uf_new(n: Int) -> UnionFind

Create a disjoint-set with n isolated elements (ids 0..n-1), each in its own set of size 1. A negative n yields an empty structure. O(n).

fn uf_find(uf: &mut UnionFind, x: Int) -> Int

Return the representative (root) of the element x, applying path compression. Returns -1 for an out-of-range element id. O(alpha n) amortized.

  • Postcondition: x >= 0 && x < uf.parent.len() => result >= 0
fn uf_union(uf: &mut UnionFind, x: Int, y: Int)

Merge the sets containing x and y (union by size). Out-of-range ids are ignored. The size of the merged set is tracked at the new root. O(alpha n) amortized.

fn uf_connected(uf: &UnionFind, x: Int, y: Int) -> Bool

Check whether x and y share a representative. Returns false for out-of-range ids. O(alpha n) amortized (read-only traversal).

fn uf_component_size(uf: &UnionFind, x: Int) -> Int

Size of the set containing x (number of elements in its component). Returns 0 for an out-of-range id. O(alpha n) amortized (read-only traversal).

  • Postcondition: result >= 0
fn uf_components(uf: &UnionFind) -> Int

Number of disjoint sets. O(1).

  • Postcondition: result >= 0



vector.xi

type IntVec

Growable array of Int elements with amortized O(1) push and O(1) indexed access. The backing store is the built-in Vec[Int]. NOTE: the API parameter type is IntVec because defining a struct named Vec collides with the built-in Vec[T] generic and silently corrupts codegen (compiler BUG 25 family); the fn names and value signatures match the frozen spec exactly. All index access is bounds-checked (Option-returning getters).

Field Type
items Vec[Int]
fn vec_new() -> IntVec

Create a new empty vector. O(1).

fn vec_push(v: &mut IntVec, value: Int)

Append value to the end of the vector. Amortized O(1).

fn vec_pop(v: &mut IntVec) -> Option[Int]

Remove and return the last value. None if the vector is empty. O(1).

fn vec_len(v: &IntVec) -> Int

Number of elements currently stored. O(1).

  • Postcondition: result >= 0
fn vec_get(v: &IntVec, idx: Int) -> Option[Int]

Value at index idx, or None when idx is out of bounds. O(1).

fn vec_set(v: &mut IntVec, idx: Int, value: Int)

Overwrite the value at idx. Out-of-bounds indices are ignored. O(1).

fn vec_insert(v: &mut IntVec, idx: Int, value: Int)

Insert value at idx, shifting later elements right. Valid range is 0..=len; other indices are ignored. O(n).

fn vec_remove(v: &mut IntVec, idx: Int) -> Option[Int]

Remove and return the value at idx, shifting later elements left. None when idx is out of bounds. O(n).

fn vec_clear(v: &mut IntVec)

Remove all elements. O(1) (capacity is retained).

  • Postcondition: vec_len(v) == 0
fn vec_is_empty(v: &IntVec) -> Bool

True if the vector holds no elements. O(1).

  • Postcondition: result == (vec_len(v) == 0)



workqueue.xi

type WorkQueue

FIFO queue of Int jobs consumed by worker threads. Pure-XIOM data structure (no OS threads): a bounded-by-memory FIFO backed by a flat Vec plus a head offset. push appends, pop reads from head; popped slots are left in place (no compaction) so every operation is O(1).

Field Type
items Vec[Int]
head Int
fn workqueue_new() -> WorkQueue

Create a new empty work queue. Returns: an empty WorkQueue with no pending jobs. Complexity: O(1).

fn workqueue_push(q: &mut WorkQueue, value: Int)

Append a job handle to the back of the queue. Params: q - the queue; value - the Int job handle to enqueue. Complexity: O(1) amortized.

fn workqueue_pop(q: &mut WorkQueue) -> Option[Int]

Dequeue the front job handle. None when the queue is empty. Params: q - the queue. Returns: the oldest pending job, or None if no jobs are pending. Complexity: O(1).

fn workqueue_len(q: &WorkQueue) -> Int

Number of pending jobs. Params: q - the queue. Returns: the count of jobs not yet popped. Complexity: O(1).

  • Postcondition: result >= 0
fn workqueue_is_empty(q: &WorkQueue) -> Bool

True if no jobs are pending. Params: q - the queue. Returns: true when the queue holds no pending jobs. Complexity: O(1).

  • Postcondition: result == (workqueue_len(q) == 0)