Landin library reference source

core/mem

Shared: available on every enabled target.

Memory providers and typed storage: the foundation for allocation, initialized prefixes and caller-owned backing.

Use allocator evidence to supply storage explicitly. arena is monotonic; failing adds a deterministic allocation budget. Raw descriptors do not establish ownership or prove alias lifetimes. Use the same provider and extent when freeing a block.

Items

Executable example

This complete program is maintained in the repository runtime tests. View source.

import core/mem

exercise: () -> (ok: bool) ! mem.out_of_memory =
    ok = false
    mut backing: [32]u8 = zeroed
    mut state := mem.arena_over_unchecked(addr backing[0], 32)
    address := try mem.allocate(state, usize(4), usize(1))
    address.val = 42
    return when address.val <> 42
    _ = mem.allocate(state, usize(64), usize(1)) else (problem)
        _ = problem
        ok = mem.arena_used(state) == 4
        return
    end
end exercise

public main: () -> (code: i32) =
    code = 1
    ok := exercise() else false
    if ok then
        code = 42
    end if
end main

allocator concept

public allocator: type = concept (provider: type)
    --- Allocate the requested byte extent or report out_of_memory. Return
    --- backing valid until the matching free; honor the requested alignment.
    alloc: (inout state: provider, size: usize, alignment: usize)
           -> (block: ptr mut u8) ! out_of_memory
    --- Extend this same block in place. Return false without changing the
    --- block or provider state when extension is refused.
    grow: (inout state: provider, block: ptr mut u8,
           old_size: usize, new_size: usize, alignment: usize)
          -> (grown: bool)
    --- Return a successful block with its current extent. The caller ends all
    --- uses first and must use the original provider.
    free: (inout state: provider, block: ptr mut u8, size: usize) -> none
end allocator

core/mem/mem.ldn:46

Explicit allocation capability. Free each successful block once through its original provider with its current byte extent. Keep provider state and backing alive until all uses end. Alignment zero or one means byte alignment; zero-byte requests follow the provider's documented policy.

arena type

public arena: type = arena_value

core/mem/mem.ldn:345

Monotonic allocator over caller-owned bytes. Individual frees do not reclaim space; only the most recent allocation can grow in place. Zero-byte requests may consume alignment padding.

byte_buffer type

public byte_buffer: type = buffer

core/mem/bytes.ldn:9

Opaque descriptor for an initialized byte allocation, retaining its full allocation extent.

failing type

public failing: type = failing_value

core/mem/mem.ldn:422

Monotonic arena with a deterministic successful-allocation budget. It never grows blocks in place; frees are counted without reclaiming bytes.

storage type

public storage: type (item: type) = raw(item)

core/mem/mem.ldn:37

Opaque typed storage over caller-owned backing. Tracks capacity and an initialized prefix; it does not own an allocator or prove the backing lifetime.

The alias is the opaque name other core modules can put in fields and signatures. It still normalizes to raw(item), whose private declaration keeps the representation inaccessible outside this module.

empty atom

public empty: atom

core/mem/mem.ldn:14

No initialized item or backing allocation is available for this operation.

out_of_bounds atom

public out_of_bounds: atom

core/mem/mem.ldn:12

The index is outside the initialized prefix.

The two atoms every core container fails with. An index past the initialized prefix is out_of_bounds whether the container is raw storage, a vector, a small vector or a bounded log; taking from a container with nothing to take is empty. Key lookups keep their own atoms, because a missing key is not a bad index.

out_of_memory atom

public out_of_memory: atom

core/mem/mem.ldn:40

The provider cannot satisfy the size or alignment request, or its arithmetic cannot represent the extent.

raw_full atom

public raw_full: atom

core/mem/mem.ldn:16

The target storage has no room for the requested initialized prefix.

raw_not_empty atom

public raw_not_empty: atom

core/mem/mem.ldn:19

Disposal requires an empty prefix; zero-prefix draining also rejects nonzero-sized items.

admit function

public admit: (item: type, inout storage: raw(item), escaping value: item)
              -> (index: usize) ! raw_full

core/mem/mem.ldn:141

Append a complete value into a spare slot and return its index. Reports raw_full without publishing a new prefix when no slot is available.

allocate function

public allocate: (provider: type is allocator, inout state: provider,
                  size: usize, alignment: usize)
                 -> (block: ptr mut u8) ! out_of_memory

core/mem/mem.ldn:64

Request a byte extent with the supplied alignment through the provider. Propagates out_of_memory; the caller owns the resulting allocation obligation.

arena_over function

public arena_over: (escaping base: ptr mut u8, size: usize)
                   -> (state: arena from base)

core/mem/mem.ldn:352

Create an arena over retainable backing without allocating. The range must stay valid for the arena and all allocations made through it.

The independent allocator result may be retained after this call. Only backing which the caller may itself retain can enter the checked arena.

arena_over_unchecked function

public arena_over_unchecked: (base: ptr mut u8, size: usize)
                             -> (state: arena from base)

core/mem/mem.ldn:363

Create an arena over local backing with an explicit lifetime opt-out. The caller must end every allocated view before that backing ends.

Explicit lifetime opt-out for a local extent. The handle still keeps its tracked origin, but allocations do not; users must end every allocation before the backing ends, including allocations retained by helpers.

arena_used function

public arena_used: (state: arena) -> (count: usize)

core/mem/mem.ldn:369

Return consumed arena bytes, including alignment padding.

bytes function

public bytes: (source: buffer) -> (view: []mut u8 from source)

core/mem/bytes.ldn:13

Lend the buffer's mutable initialized bytes. The buffer must remain allocated while the view is used.

capacity function

public capacity: (item: type, storage: raw(item)) -> (count: usize)

core/mem/mem.ldn:122

Return the logical slot capacity, including slots for zero-sized items.

clear function

public clear: (item: type, inout storage: raw(item)) -> none

core/mem/mem.ldn:276

Discard all initialized items while retaining backing and capacity. Resources referred to by those values remain the caller's responsibility.

Forget the initialized prefix without changing the backing allocation. Values in that prefix are discarded; callers remain responsible for any resources those values refer to.

delete function

public delete: (item: type, provider: type is allocator,
                inout state: provider, sink object: ptr mut item) -> none

core/mem/allocation.ldn:19

Free one typed allocation through its original provider. End all aliases first; resources referenced by the item are not released automatically.

Consumption ends this binding only. Copies and outstanding aliases remain the caller's manual-lifetime responsibility, as for the allocator itself.

delete_bytes function

public delete_bytes: (provider: type is allocator, inout state: provider,
                      inout value: buffer) -> none

core/mem/bytes.ldn:48

Free the buffer using its saved extent and reset it. Empty buffers require no provider call. End all byte views before deletion.

dispose function

public dispose: (item: type, inout storage: raw(item))
                -> (released: ptr mut u8 from storage)
                ! raw_not_empty | empty

core/mem/mem.ldn:283

Detach backing from an empty descriptor and reset it. Reports raw_not_empty if items remain, or empty if no allocation exists. The returned pointer must still be freed through its provider.

drain_zero_prefix function

public drain_zero_prefix: (item: type, inout storage: raw(item))
                          -> none ! raw_not_empty

core/mem/mem.ldn:250

Discard a zero-sized initialized prefix in constant time. Reports raw_not_empty for nonzero-sized items before changing storage.

With no payload bytes to destroy, shortening this witness discards all logical items at once. Reject a nonzero-sized item before changing it.

empty_storage function

public empty_storage: (item: type) -> (storage: raw(item))

core/mem/mem.ldn:81

Create an empty descriptor without allocating backing.

A descriptor without an allocation is not a zero-address allocation. It owns no extent, admits no item and cannot yield a pointer on disposal.

failing_allocations function

public failing_allocations: (state: failing) -> (count: usize)

core/mem/mem.ldn:454

Return the number of successful allocations so far.

failing_frees function

public failing_frees: (state: failing) -> (count: usize)

core/mem/mem.ldn:459

Return the number of free calls; these calls do not reclaim arena space.

failing_over function

public failing_over: (escaping base: ptr mut u8, size: usize,
                      successful_allocations: usize)
                     -> (state: failing from base)

core/mem/mem.ldn:427

Create a bounded failing arena over retainable backing. Each successful allocation consumes one permit; exhausted budget or backing reports out_of_memory.

failing_over_unchecked function

public failing_over_unchecked: (base: ptr mut u8, size: usize,
                                successful_allocations: usize)
                               -> (state: failing from base)

core/mem/mem.ldn:436

Create a failing arena with the local-backing lifetime opt-out. The caller must end every allocation before the supplied range ends.

failing_remaining function

public failing_remaining: (state: failing) -> (count: usize)

core/mem/mem.ldn:449

Return the number of further successful allocations permitted.

failing_used function

public failing_used: (state: failing) -> (count: usize)

core/mem/mem.ldn:444

Return consumed backing bytes, including alignment padding.

free function

public free: (provider: type is allocator, inout state: provider,
              block: ptr mut u8, size: usize) -> none

core/mem/mem.ldn:72

Return a block to its provider using the allocation's current extent. The caller must end all uses first; no item cleanup runs.

get function

public get: (item: type, storage: raw(item), index: usize)
            -> (value: item from storage) ! out_of_bounds

core/mem/mem.ldn:165

Copy the item at index. Reports out_of_bounds before reading outside the initialized prefix; references inside the copy retain their origin.

grow_storage function

public grow_storage: (item: type, provider: type is allocator,
                      inout storage: raw(item), inout state: provider,
                      old_size: usize, new_size: usize, slots: usize)
                     -> (grown: bool)

core/mem/mem.ldn:103

Attempt to extend the same positive-byte allocation in place. Publishes the new capacity only on success; refusal leaves storage unchanged.

The provider validates the physical extension before the private logical capacity changes. In particular, a zero-byte allocation keeps its usual one-allocation-per-reserve behavior. Callers supply the actual old and requested byte extents after checking capacity arithmetic.

initialized function

public initialized: (item: type, storage: raw(item)) -> (count: usize)

core/mem/mem.ldn:127

Return the number of initialized items in the prefix.

new function

public new: (item: type, provider: type is allocator,
             inout state: provider, escaping value: item)
            -> (object: ptr mut item) ! out_of_memory

core/mem/allocation.ldn:6

Allocate storage for one item and store value in it. Reports out_of_memory without returning a partial allocation.

Allocated objects are published only after their complete initial value has been stored. Reference-containing initial values must be retainable.

new_bytes function

public new_bytes: (provider: type is allocator, inout state: provider,
                   count: usize) -> (result: buffer) ! out_of_memory

core/mem/bytes.ldn:20

Allocate count zero-initialized bytes. A zero count returns an empty buffer without calling the provider; allocation failure reports out_of_memory.

replace function

public replace: (item: type, inout storage: raw(item), index: usize,
                 escaping value: item) -> none ! out_of_bounds

core/mem/mem.ldn:173

Overwrite an initialized item. Reports out_of_bounds before mutation; the caller handles resources held by the replaced value.

reserve function

public reserve: (item: type, base: ptr mut u8, slots: usize)
                -> (storage: raw(item) from base)

core/mem/mem.ldn:90

Describe slots items over an existing byte range without allocating or initializing items. The caller supplies sufficient, correctly aligned backing and keeps it alive; the extent multiplication must be representable.

transfer function

public transfer: (item: type, source: raw(item), index: usize,
                  inout target: raw(item))
                 -> (admitted: usize) ! out_of_bounds | raw_full

core/mem/mem.ldn:184

Copy one initialized source item to the end of the target. Checks source index and target capacity before mutation; the source remains initialized.

Read a complete source value before entering the destination's narrow unchecked append. The new prefix is published only after its typed store.

transfer_zero_prefix function

public transfer_zero_prefix: (item: type, source: raw(item),
                              inout target: raw(item), count: usize)
                             -> none ! out_of_bounds | raw_full

core/mem/mem.ldn:222

Initialize a target prefix from a zero-sized source item. Requires zero-sized items, an empty target, sufficient capacity and a source prefix at least count long.

A zero-byte prefix has one logical item value repeated at the same address. Establish the destination's own initialized witness with a complete typed store before extending it to the requested count. The source and destination counters and the destination allocation remain checked, just as they are for individual transfers.

used function

public used: (item: type, storage: raw(item))
             -> (view: []mut item from storage)

core/mem/mem.ldn:134

Lend a mutable slice of the initialized prefix. End uses of the view before invalidating or freeing its backing.

withdraw function

public withdraw: (item: type, inout storage: raw(item))
                 -> (value: item from storage) ! empty

core/mem/mem.ldn:261

Remove and return the last initialized item. Reports empty when the prefix is empty; backing and capacity remain available.

Take the last initialized item back out of the prefix. This is the raw pop; release is reserved for giving a container's storage back.