1-- The full allocation extent stays private beside the initialized witness.
2-- Borrowed byte views do not replace that allocation identity.
3buffer: type = struct
4 values: storage(u8)
5 extent: usize
6end buffer
7--- Opaque descriptor for an initialized byte allocation, retaining its full
8--- allocation extent.
9public byte_buffer: type = buffer
10
11--- Lend the buffer's mutable initialized bytes. The buffer must remain
12--- allocated while the view is used.
13public bytes: (source: buffer) -> (view: []mut u8 from source) =
14 view = used(source.values)
15end bytes
16
17--- Allocate `count` zero-initialized bytes. A zero count returns an empty
18--- buffer without calling the provider; allocation failure reports
19--- `out_of_memory`.
20public new_bytes: (provider: type is allocator, inout state: provider,
21 count: usize) -> (result: buffer) ! out_of_memory =
22 zero: usize = 0
23 if count == 0 then
24 none_yet := empty_storage(item: u8)
25 result = (values: none_yet, extent: zero)
26 return
27 end if
28 block: ptr mut u8 = try provider.alloc(state, count, alignof u8)
29 mut fresh := reserve(item: u8, base: block, slots: count)
30 mut index: usize = 0
31 initial: u8 = 0
32 while index < count do
33 admitted: usize = admit(fresh, initial) else (problem)
34 -- Refusal is unreachable for this private state. If it occurs,
35 -- release the saved allocation without trusting damaged counts.
36 _ = problem
37 provider.free(state, block, count)
38 fail out_of_memory
39 end
40 _ = admitted
41 inc index
42 end while
43 result = (values: fresh, extent: count)
44end new_bytes
45
46--- Free the buffer using its saved extent and reset it. Empty buffers require
47--- no provider call. End all byte views before deletion.
48public delete_bytes: (provider: type is allocator, inout state: provider,
49 inout value: buffer) -> none =
50 return when value.extent == 0
51 extent: usize = value.extent
52 clear(value.values)
53 block: ptr mut u8 = dispose(value.values) else (problem)
54 _ = problem
55 return
56 end
57 value.extent = 0
58 provider.free(state, block, extent)
59end delete_bytes