1-- Honest typed storage. The representation stays module-internal: callers
2-- can hold an inferred raw(T), but only these operations can expose a value
3-- or change the initialized-prefix count.
4
5--- The index is outside the initialized prefix.
6---
7--- The two atoms every core container fails with. An index past the
8--- initialized prefix is out_of_bounds whether the container is raw
9--- storage, a vector, a small vector or a bounded log; taking from a
10--- container with nothing to take is empty. Key lookups keep their own
11--- atoms, because a missing key is not a bad index.
12public out_of_bounds: atom
13--- No initialized item or backing allocation is available for this operation.
14public empty: atom
15--- The target storage has no room for the requested initialized prefix.
16public raw_full: atom
17--- Disposal requires an empty prefix; zero-prefix draining also rejects
18--- nonzero-sized items.
19public raw_not_empty: atom
20
21no_storage: atom
22allocation: type = no_storage | ptr mut u8
23
24raw: type (item: type) = struct
25 base: allocation
26 capacity_count: usize
27 prefix: []mut item
28end raw
29
30--- Opaque typed storage over caller-owned backing. Tracks capacity and an
31--- initialized prefix; it does not own an allocator or prove the backing
32--- lifetime.
33---
34--- The alias is the opaque name other core modules can put in fields and
35--- signatures. It still normalizes to raw(item), whose private declaration
36--- keeps the representation inaccessible outside this module.
37public storage: type (item: type) = raw(item)
38--- The provider cannot satisfy the size or alignment request, or its
39--- arithmetic cannot represent the extent.
40public out_of_memory: atom
41
42--- Explicit allocation capability. Free each successful block once through
43--- its original provider with its current byte extent. Keep provider state
44--- and backing alive until all uses end. Alignment zero or one means byte
45--- alignment; zero-byte requests follow the provider's documented policy.
46public allocator: type = concept (provider: type)
47 --- Allocate the requested byte extent or report out_of_memory. Return
48 --- backing valid until the matching free; honor the requested alignment.
49 alloc: (inout state: provider, size: usize, alignment: usize)
50 -> (block: ptr mut u8) ! out_of_memory
51 --- Extend this same block in place. Return false without changing the
52 --- block or provider state when extension is refused.
53 grow: (inout state: provider, block: ptr mut u8,
54 old_size: usize, new_size: usize, alignment: usize)
55 -> (grown: bool)
56 --- Return a successful block with its current extent. The caller ends all
57 --- uses first and must use the original provider.
58 free: (inout state: provider, block: ptr mut u8, size: usize) -> none
59end allocator
60
61--- Request a byte extent with the supplied alignment through the provider.
62--- Propagates `out_of_memory`; the caller owns the resulting allocation
63--- obligation.
64public allocate: (provider: type is allocator, inout state: provider,
65 size: usize, alignment: usize)
66 -> (block: ptr mut u8) ! out_of_memory =
67 block = try provider.alloc(state, size, alignment)
68end allocate
69
70--- Return a block to its provider using the allocation's current extent. The
71--- caller must end all uses first; no item cleanup runs.
72public free: (provider: type is allocator, inout state: provider,
73 block: ptr mut u8, size: usize) -> none =
74 provider.free(state, block, size)
75end free
76
77--- Create an empty descriptor without allocating backing.
78---
79--- A descriptor without an allocation is not a zero-address allocation.
80--- It owns no extent, admits no item and cannot yield a pointer on disposal.
81public empty_storage: (item: type) -> (storage: raw(item)) =
82 prefix: []mut item = []
83 storage = (base: no_storage, capacity_count: 0, prefix: prefix)
84end empty_storage
85
86--- Describe `slots` items over an existing byte range without allocating or
87--- initializing items. The caller supplies sufficient, correctly aligned
88--- backing and keeps it alive; the extent multiplication must be
89--- representable.
90public reserve: (item: type, base: ptr mut u8, slots: usize)
91 -> (storage: raw(item) from base) =
92 prefix: []mut item = []
93 storage = (base: base, capacity_count: slots, prefix: prefix)
94end reserve
95
96--- Attempt to extend the same positive-byte allocation in place. Publishes
97--- the new capacity only on success; refusal leaves storage unchanged.
98---
99--- The provider validates the physical extension before the private logical
100--- capacity changes. In particular, a zero-byte allocation keeps its usual
101--- one-allocation-per-reserve behavior. Callers supply the actual old and
102--- requested byte extents after checking capacity arithmetic.
103public grow_storage: (item: type, provider: type is allocator,
104 inout storage: raw(item), inout state: provider,
105 old_size: usize, new_size: usize, slots: usize)
106 -> (grown: bool) =
107 grown = false
108 return when old_size == 0 or new_size <= old_size
109 match storage.base
110 no_storage: return
111 ptr (base): begin
112 grown = provider.grow(state, base, old_size, new_size,
113 alignof item)
114 if grown then
115 storage.capacity_count = slots
116 end if
117 end
118 end match
119end grow_storage
120
121--- Return the logical slot capacity, including slots for zero-sized items.
122public capacity: (item: type, storage: raw(item)) -> (count: usize) =
123 count = storage.capacity_count
124end capacity
125
126--- Return the number of initialized items in the prefix.
127public initialized: (item: type, storage: raw(item)) -> (count: usize) =
128 prefix := storage.prefix
129 count = lenof prefix
130end initialized
131
132--- Lend a mutable slice of the initialized prefix. End uses of the view
133--- before invalidating or freeing its backing.
134public used: (item: type, storage: raw(item))
135 -> (view: []mut item from storage) =
136 view = storage.prefix
137end used
138
139--- Append a complete value into a spare slot and return its index. Reports
140--- `raw_full` without publishing a new prefix when no slot is available.
141public admit: (item: type, inout storage: raw(item), escaping value: item)
142 -> (index: usize) ! raw_full =
143 index = initialized(storage)
144 fail raw_full when index >= storage.capacity_count
145 wanted: usize = index + 1
146 if index == 0 then
147 match storage.base
148 no_storage: fail raw_full
149 ptr (base): begin
150 first: ptr mut [1]item = ptr(usize(base))
151 first.val[0] = value
152 storage.prefix = first.val[0..<1]
153 end
154 end match
155 else
156 unchecked begin
157 storage.prefix[index] = value
158 storage.prefix = storage.prefix[0..<wanted]
159 end unchecked
160 end if
161end admit
162
163--- Copy the item at `index`. Reports `out_of_bounds` before reading outside
164--- the initialized prefix; references inside the copy retain their origin.
165public get: (item: type, storage: raw(item), index: usize)
166 -> (value: item from storage) ! out_of_bounds =
167 fail out_of_bounds when index >= initialized(storage)
168 value = storage.prefix[index]
169end get
170
171--- Overwrite an initialized item. Reports `out_of_bounds` before mutation;
172--- the caller handles resources held by the replaced value.
173public replace: (item: type, inout storage: raw(item), index: usize,
174 escaping value: item) -> none ! out_of_bounds =
175 fail out_of_bounds when index >= initialized(storage)
176 storage.prefix[index] = value
177end replace
178
179--- Copy one initialized source item to the end of the target. Checks source
180--- index and target capacity before mutation; the source remains initialized.
181---
182--- Read a complete source value before entering the destination's narrow
183--- unchecked append. The new prefix is published only after its typed store.
184public transfer: (item: type, source: raw(item), index: usize,
185 inout target: raw(item))
186 -> (admitted: usize) ! out_of_bounds | raw_full =
187 fail out_of_bounds when index >= initialized(source)
188 admitted = initialized(target)
189 fail raw_full when admitted >= target.capacity_count
190 saved: item = source.prefix[index]
191 wanted: usize = admitted + 1
192 if admitted == 0 then
193 match target.base
194 no_storage: fail raw_full
195 ptr (base): begin
196 first: ptr mut [1]item = ptr(usize(base))
197 first.val[0] = saved
198 target.prefix = first.val[0..<1]
199 end
200 end match
201 else
202 unchecked begin
203 -- The private transfer copies an already-retained value into
204 -- independent raw storage, as the first-slot path does above.
205 -- Capture that destination before publishing its new witness.
206 slot: ptr mut item = ptr(usize(addr target.prefix[admitted]))
207 slot.val = saved
208 target.prefix = target.prefix[0..<wanted]
209 end unchecked
210 end if
211end transfer
212
213--- Initialize a target prefix from a zero-sized source item. Requires
214--- zero-sized items, an empty target, sufficient capacity and a source prefix
215--- at least `count` long.
216---
217--- A zero-byte prefix has one logical item value repeated at the same
218--- address. Establish the destination's own initialized witness with a
219--- complete typed store before extending it to the requested count. The
220--- source and destination counters and the destination allocation remain
221--- checked, just as they are for individual transfers.
222public transfer_zero_prefix: (item: type, source: raw(item),
223 inout target: raw(item), count: usize)
224 -> none ! out_of_bounds | raw_full =
225 fail out_of_bounds when sizeof item <> 0
226 fail out_of_bounds when count > initialized(source)
227 fail raw_full when initialized(target) <> 0
228 fail raw_full when count > target.capacity_count
229 return when count == 0
230
231 saved: item = source.prefix[0]
232 match target.base
233 no_storage: fail raw_full
234 ptr (base): begin
235 first: ptr mut [1]item = ptr(usize(base))
236 first.val[0] = saved
237 target.prefix = first.val[0..<1]
238 end
239 end match
240 unchecked begin
241 target.prefix = target.prefix[0..<count]
242 end unchecked
243end transfer_zero_prefix
244
245--- Discard a zero-sized initialized prefix in constant time. Reports
246--- `raw_not_empty` for nonzero-sized items before changing storage.
247---
248--- With no payload bytes to destroy, shortening this witness discards all
249--- logical items at once. Reject a nonzero-sized item before changing it.
250public drain_zero_prefix: (item: type, inout storage: raw(item))
251 -> none ! raw_not_empty =
252 fail raw_not_empty when sizeof item <> 0
253 storage.prefix = storage.prefix[0..<0]
254end drain_zero_prefix
255
256--- Remove and return the last initialized item. Reports `empty` when the
257--- prefix is empty; backing and capacity remain available.
258---
259--- Take the last initialized item back out of the prefix. This is the raw
260--- pop; `release` is reserved for giving a container's storage back.
261public withdraw: (item: type, inout storage: raw(item))
262 -> (value: item from storage) ! empty =
263 count: usize = initialized(storage)
264 fail empty when count == 0
265 tail: usize = count - 1
266 value = storage.prefix[tail]
267 storage.prefix = storage.prefix[0..<tail]
268end withdraw
269
270--- Discard all initialized items while retaining backing and capacity.
271--- Resources referred to by those values remain the caller's responsibility.
272---
273--- Forget the initialized prefix without changing the backing allocation.
274--- Values in that prefix are discarded; callers remain responsible for any
275--- resources those values refer to.
276public clear: (item: type, inout storage: raw(item)) -> none =
277 storage.prefix = storage.prefix[0..<0]
278end clear
279
280--- Detach backing from an empty descriptor and reset it. Reports
281--- `raw_not_empty` if items remain, or `empty` if no allocation exists. The
282--- returned pointer must still be freed through its provider.
283public dispose: (item: type, inout storage: raw(item))
284 -> (released: ptr mut u8 from storage)
285 ! raw_not_empty | empty =
286 fail raw_not_empty when initialized(storage) <> 0
287 match storage.base
288 no_storage: fail empty
289 ptr (base): released = base
290 end match
291 storage.base = no_storage
292 storage.prefix = []
293 storage.capacity_count = 0
294end dispose
295
296-- Find the offset whose absolute address meets the requested alignment.
297-- Zero alignment has the same byte-aligned meaning as one. Every operation
298-- that could overflow is guarded, including the end of a zero- or nonzero-
299-- sized result, so failure leaves allocator state for the caller to retain.
300allocation_offset: (base: ptr mut u8, used: usize, extent: usize,
301 size: usize, alignment: usize)
302 -> (offset: usize) ! out_of_memory =
303 maximum: usize = 0 -% 1
304 fail out_of_memory when used > extent
305
306 base_address: usize = usize(base)
307 fail out_of_memory when used > maximum - base_address
308 current_address: usize = base_address + used
309
310 mut padding: usize = 0
311 if alignment > 1 then
312 -- alignof requests take the mask path; direct calls may need division.
313 mask: usize = alignment - 1
314 mut remainder: usize = 0
315 if (alignment & mask) == 0 then
316 remainder = current_address & mask
317 else
318 remainder = current_address % alignment
319 end if
320 if not (remainder == 0) then
321 padding = alignment - remainder
322 end if
323 end if
324
325 fail out_of_memory when padding > extent - used
326 fail out_of_memory when padding > maximum - current_address
327 offset = used + padding
328 aligned_address: usize = current_address + padding
329 fail out_of_memory when size > extent - offset
330 fail out_of_memory when size > maximum - aligned_address
331end allocation_offset
332
333-- A library arena is a monotonic allocator over a caller-supplied byte
334-- extent. Individual frees deliberately do nothing; ending the extent ends
335-- all of its allocations together.
336arena_value: type = struct
337 base: ptr mut u8
338 size: usize
339 used: usize
340end arena_value
341
342--- Monotonic allocator over caller-owned bytes. Individual frees do not
343--- reclaim space; only the most recent allocation can grow in place.
344--- Zero-byte requests may consume alignment padding.
345public arena: type = arena_value
346
347--- Create an arena over retainable backing without allocating. The range must
348--- stay valid for the arena and all allocations made through it.
349---
350--- The independent allocator result may be retained after this call. Only
351--- backing which the caller may itself retain can enter the checked arena.
352public arena_over: (escaping base: ptr mut u8, size: usize)
353 -> (state: arena from base) =
354 state = (base: base, size: size, used: 0)
355end arena_over
356
357--- Create an arena over local backing with an explicit lifetime opt-out. The
358--- caller must end every allocated view before that backing ends.
359---
360--- Explicit lifetime opt-out for a local extent. The handle still keeps its
361--- tracked origin, but allocations do not; users must end every allocation
362--- before the backing ends, including allocations retained by helpers.
363public arena_over_unchecked: (base: ptr mut u8, size: usize)
364 -> (state: arena from base) =
365 state = (base: base, size: size, used: 0)
366end arena_over_unchecked
367
368--- Return consumed arena bytes, including alignment padding.
369public arena_used: (state: arena) -> (count: usize) =
370 count = state.used
371end arena_used
372
373arena_alloc: (inout state: arena, size: usize, alignment: usize)
374 -> (block: ptr mut u8) ! out_of_memory =
375 offset: usize = try allocation_offset(state.base, state.used, state.size,
376 size, alignment)
377 address: usize = usize(state.base) + offset
378 block = ptr(address)
379 state.used = offset + size
380end arena_alloc
381
382arena_free: (inout state: arena, block: ptr mut u8, size: usize) -> none =
383 _ = state.used
384 _ = block
385 _ = size
386end arena_free
387
388arena_grow: (inout state: arena, block: ptr mut u8,
389 old_size: usize, new_size: usize, alignment: usize)
390 -> (grown: bool) =
391 grown = false
392 return when new_size <= old_size or state.used > state.size
393 base_address: usize = usize(state.base)
394 block_address: usize = usize(block)
395 return when block_address < base_address
396 offset: usize = block_address - base_address
397 return when offset > state.used or old_size <> state.used - offset
398 return when alignment > 1 and block_address % alignment <> 0
399 return when new_size > state.size - offset
400 maximum: usize = 0 -% 1
401 return when new_size > maximum - block_address
402 state.used = offset + new_size
403 grown = true
404end arena_grow
405
406arena is allocator (alloc: arena_alloc, grow: arena_grow, free: arena_free)
407
408-- The same monotonic allocator with a deterministic allocation budget.
409-- Tests can reach a container's out-of-memory edge without relying on the
410-- host or exhausting an actual address space.
411failing_value: type = struct
412 base: ptr mut u8
413 size: usize
414 used: usize
415 remaining: usize
416 allocations: usize
417 frees: usize
418end failing_value
419
420--- Monotonic arena with a deterministic successful-allocation budget. It
421--- never grows blocks in place; frees are counted without reclaiming bytes.
422public failing: type = failing_value
423
424--- Create a bounded failing arena over retainable backing. Each successful
425--- allocation consumes one permit; exhausted budget or backing reports
426--- `out_of_memory`.
427public failing_over: (escaping base: ptr mut u8, size: usize,
428 successful_allocations: usize)
429 -> (state: failing from base) =
430 state = (base: base, size: size, used: 0,
431 remaining: successful_allocations, allocations: 0, frees: 0)
432end failing_over
433
434--- Create a failing arena with the local-backing lifetime opt-out. The caller
435--- must end every allocation before the supplied range ends.
436public failing_over_unchecked: (base: ptr mut u8, size: usize,
437 successful_allocations: usize)
438 -> (state: failing from base) =
439 state = (base: base, size: size, used: 0,
440 remaining: successful_allocations, allocations: 0, frees: 0)
441end failing_over_unchecked
442
443--- Return consumed backing bytes, including alignment padding.
444public failing_used: (state: failing) -> (count: usize) =
445 count = state.used
446end failing_used
447
448--- Return the number of further successful allocations permitted.
449public failing_remaining: (state: failing) -> (count: usize) =
450 count = state.remaining
451end failing_remaining
452
453--- Return the number of successful allocations so far.
454public failing_allocations: (state: failing) -> (count: usize) =
455 count = state.allocations
456end failing_allocations
457
458--- Return the number of free calls; these calls do not reclaim arena space.
459public failing_frees: (state: failing) -> (count: usize) =
460 count = state.frees
461end failing_frees
462
463failing_alloc: (inout state: failing, size: usize, alignment: usize)
464 -> (block: ptr mut u8) ! out_of_memory =
465 fail out_of_memory when state.remaining == 0
466 offset: usize = try allocation_offset(state.base, state.used, state.size,
467 size, alignment)
468 dec state.remaining
469 inc state.allocations
470 address: usize = usize(state.base) + offset
471 block = ptr(address)
472 state.used = offset + size
473end failing_alloc
474
475failing_free: (inout state: failing, block: ptr mut u8, size: usize) -> none =
476 _ = block
477 _ = size
478 inc state.frees
479end failing_free
480
481failing_grow: (inout state: failing, block: ptr mut u8,
482 old_size: usize, new_size: usize, alignment: usize)
483 -> (grown: bool) =
484 _ = state.used
485 _ = block
486 _ = old_size
487 _ = new_size
488 _ = alignment
489 grown = false
490end failing_grow
491
492failing is allocator (alloc: failing_alloc, grow: failing_grow,
493 free: failing_free)