Skip to content

std.arena

A generational arena: values live in one owned array and are named by a copyable Handle instead of a borrow, which is how CAIRN expresses graphs and cycles. Removing a value bumps its slot's generation, so every handle to it stops resolving - a use-after-free becomes a None instead of a dangling pointer. Cost: insert is amortized O(1) and reuses removed slots; find and remove are O(1). Growth reallocates and moves elements with swap, so alloc and free are in the caller's row.

pub struct Handle { slot:usize; generation:u64; }
pub struct Arena[T:affine] { items:Buf[T]; gen:Buf[u64]; live:Buf[u8]; free:Vec[usize]; used:usize; count:usize; }
pub fn new[T:affine]() -> Arena[T]  // effects: alloc, free, trap, zero_init
pub fn count[T:affine](a:ro<Arena[T]>) -> usize  // effects: read:a
pub fn slots[T:affine](a:ro<Arena[T]>) -> usize  // effects: read:a
pub fn alive[T:affine](a:ro<Arena[T]>, slot:usize) -> bool  // effects: read:a, trap

// The handle a live slot currently answers to; pairs with `slots` to iterate an arena.
pub fn handle[T:affine](a:ro<Arena[T]>, slot:usize) -> Handle  // effects: read:a, trap

// effects: alloc, free, local_read, local_write, read:a, trap, write:a, zero_init
pub fn insert[T:affine](a:rw<Arena[T]>, value:T) -> Handle

// None when the handle is stale: wrong slot, removed value, or an older generation.
pub fn find[T:affine](a:ro<Arena[T]>, h:Handle) -> Option[usize]  // effects: read:a, trap

// effects: alloc, ffi_precondition, free, local_read, local_write, read:a, trap, write:a, zero_init
pub fn remove[T:affine](a:rw<Arena[T]>, h:Handle) -> Option[T]

A generic function's effects are what it may do for any arguments within its bounds, besides what their own trait members do.