1	import Base
2	import ../math/pow2.bend as P2
3	import ./types/dynamic_array.bend as E
4	
5	# Growable, bounds-checked array over native Base.Array.
6	# DynArray<&2, T> is the existing Data API; DynArray<T> stores owning Type
7	# elements through the _owned API below. See docs/DYNAMIC_ARRAY_OWNERSHIP.md.
8	#
9	# Representation: DA{limit, depth, cap, length, slots} with cap = 2^depth kept
10	# in the record (recomputing 2^depth per operation would make every push,
11	# capacity and reserve cost O(depth)). `slots` is a Base.Array of
12	# 2^depth slots. ALeaf/ANode is the LOGICAL model the checker reasons about;
13	# stock Bend 2.0.16 lowers a Base.Array to one indexed memory block, and
14	# get/set/swap compile to a `blk_at` index computation plus a direct
15	# `blk_read`/`blk_write` (docs/C_EQUIVALENCE.md). Slots [0, length)
16	# hold Some{x}; the rest hold None. Capacity is 2^depth. `limit` (<= 31) caps
17	# depth, so every capacity is representable as the U32 size Base computes, and
18	# every index passed to Base is < 2^depth <= 2^31 (so Base's masking is the
19	# identity). Out-of-range indices never reach Base.
20	#
21	# Errors return the state unchanged (see docs/API.md):
22	#   get/set out of range -> IndexOutOfRange; pop on empty -> EmptyArray;
23	#   push/reserve beyond 2^limit -> CapacityExceeded.
24	# Cost (n = length, c = capacity): get/set/push/pop are one indexed load or
25	# store into the block (no tree descent in the native lowering), growth O(c)
26	# (a fresh half is allocated and the merged block copied, like a C realloc),
27	# reserve O(target capacity), clear O(n), to_list O(c).
28	
29	type DynArray<a, -T: Kind(a)> is Type:
30	  DA{limit: Nat, depth: Nat, cap: Nat, length: Nat, slots: Array<Maybe<a, T>>}
31	
32	def max_depth() -> Nat:
33	  31n
34	
35	# 2^d (structural doubling; Base Nat.pow is avoided, see docs/VALIDATION.md).
36	def pow2(d: Nat) -> Nat:
37	  match d:
38	    case 0n:
39	      1n
40	    case 1n+p:
41	      Nat.double(pow2(p))
42	
43	def empty_slots(-T: Data, +depth: Nat) -> Array<Maybe<&2, T>>:
44	  Array.new(Maybe<&2, T>, depth, None{})
45	
46	def new(-T: Data) -> DynArray<&2, T>:
47	  DA{max_depth(), 0n, 1n, 0n, empty_slots(T, 0n)}
48	
49	# Depth limit min(k, 31). (Written with an explicit match: Base Nat.min is a
50	# Bool.pick over shared arguments, which miscompiled at runtime; docs/VALIDATION.md.)
51	def clamp_limit(k: Nat, small: Bool) -> Nat:
52	  match small:
53	    case True{}:
54	      k
55	    case False{}:
56	      max_depth()
57	
58	# Same as new, with capacity bounded by 2^min(k, 31).
59	def with_limit(-T: Data, +k: Nat) -> DynArray<&2, T>:
60	  DA{clamp_limit(k, Nat.is_lt(k, max_depth())), 0n, 1n, 0n, empty_slots(T, 0n)}
61	
62	def length(-T: Data, da: DynArray<&2, T>) -> DynArray<&2, T> & Nat:
63	  DA{limit, depth, cap, +len, arr} = da
64	  (DA{limit, depth, cap, len, arr}, len)
65	
66	def capacity(-T: Data, da: DynArray<&2, T>) -> DynArray<&2, T> & Nat:
67	  DA{limit, depth, +cap, len, arr} = da
68	  (DA{limit, depth, cap, len, arr}, cap)
69	
70	def slot_result(-T: Data, slot: Maybe<&2, T>) -> Result<&2, &2, E.Error, T>:
71	  match slot:
72	    case None{}:
73	      Fail{E.IndexOutOfRange{}}
74	    case Some{x}:
75	      Done{x}
76	
77	# ---- get ----
78	
79	def get_found(-T: Data, limit: Nat, depth: Nat, +cap: Nat, len: Nat, r: Array<Maybe<&2, T>> & Maybe<&2, T>) -> DynArray<&2, T> & Result<&2, &2, E.Error, T>:
80	  (arr, slot) = r
81	  (DA{limit, depth, cap, len, arr}, slot_result(T, slot))
82	
83	def get_checked(-T: Data, limit: Nat, depth: Nat, +cap: Nat, len: Nat, arr: Array<Maybe<&2, T>>, i: Nat, ok: Bool) -> DynArray<&2, T> & Result<&2, &2, E.Error, T>:
84	  match ok:
85	    case True{}:
86	      get_found(T, limit, depth, cap, len, Array.get(Maybe<&2, T>, arr, U32.from_nat(i)))
87	    case False{}:
88	      (DA{limit, depth, cap, len, arr}, Fail{E.IndexOutOfRange{}})
89	
90	def get(-T: Data, da: DynArray<&2, T>, +i: Nat) -> DynArray<&2, T> & Result<&2, &2, E.Error, T>:
91	  DA{limit, depth, cap, +len, arr} = da
92	  get_checked(T, limit, depth, cap, len, arr, i, Nat.is_lt(i, len))
93	
94	# ---- set ----
95	
96	def set_checked(-T: Data, limit: Nat, depth: Nat, +cap: Nat, len: Nat, arr: Array<Maybe<&2, T>>, i: Nat, v: T, ok: Bool) -> DynArray<&2, T> & Result<&2, &2, E.Error, Unit>:
97	  match ok:
98	    case True{}:
99	      (DA{limit, depth, cap, len, Array.set(Maybe<&2, T>, arr, U32.from_nat(i), Some{v})}, Done{Unit{}})
100	    case False{}:
101	      (DA{limit, depth, cap, len, arr}, Fail{E.IndexOutOfRange{}})
102	
103	def set(-T: Data, da: DynArray<&2, T>, +i: Nat, v: T) -> DynArray<&2, T> & Result<&2, &2, E.Error, Unit>:
104	  DA{limit, depth, cap, +len, arr} = da
105	  set_checked(T, limit, depth, cap, len, arr, i, v, Nat.is_lt(i, len))
106	
107	# ---- growth ----
108	
109	# Doubling: the old tree becomes the left half of a tree one level deeper.
110	def grown(-T: Data, +depth: Nat, arr: Array<Maybe<&2, T>>) -> Array<Maybe<&2, T>>:
111	  ANode{arr, empty_slots(T, depth)}
112	
113	def push_room(-T: Data, limit: Nat, +depth: Nat, +cap: Nat, +len: Nat, arr: Array<Maybe<&2, T>>, v: T, room: Bool, grow: Bool) -> DynArray<&2, T> & Result<&2, &2, E.Error, Unit>:
114	  match room grow:
115	    case True{} _:
116	      (DA{limit, depth, cap, 1n+len, Array.set(Maybe<&2, T>, arr, U32.from_nat(len), Some{v})}, Done{Unit{}})
117	    case False{} True{}:
118	      (DA{limit, 1n+depth, Nat.double(cap), 1n+len, Array.set(Maybe<&2, T>, grown(T, depth, arr), U32.from_nat(len), Some{v})}, Done{Unit{}})
119	    case False{} False{}:
120	      (DA{limit, depth, cap, len, arr}, Fail{E.CapacityExceeded{}})
121	
122	def push(-T: Data, da: DynArray<&2, T>, v: T) -> DynArray<&2, T> & Result<&2, &2, E.Error, Unit>:
123	  DA{+limit, +depth, +cap, +len, arr} = da
124	  push_room(T, limit, depth, cap, len, arr, v, Nat.is_lt(len, cap), Nat.is_lt(depth, limit))
125	
126	# ---- pop ----
127	
128	def pop_found(-T: Data, limit: Nat, depth: Nat, +cap: Nat, m: Nat, r: Array<Maybe<&2, T>> & Maybe<&2, T>) -> DynArray<&2, T> & Result<&2, &2, E.Error, T>:
129	  (arr, old) = r
130	  (DA{limit, depth, cap, m, arr}, slot_result(T, old))
131	
132	def pop_len(-T: Data, limit: Nat, depth: Nat, +cap: Nat, len: Nat, arr: Array<Maybe<&2, T>>) -> DynArray<&2, T> & Result<&2, &2, E.Error, T>:
133	  match len:
134	    case 0n:
135	      (DA{limit, depth, cap, 0n, arr}, Fail{E.EmptyArray{}})
136	    case 1n+ +m:
137	      pop_found(T, limit, depth, cap, m, Array.swap(Maybe<&2, T>, arr, U32.from_nat(m), None{}))
138	
139	def pop(-T: Data, da: DynArray<&2, T>) -> DynArray<&2, T> & Result<&2, &2, E.Error, T>:
140	  DA{limit, depth, cap, len, arr} = da
141	  pop_len(T, limit, depth, cap, len, arr)
142	
143	# ---- reserve ----
144	
145	def grow_if(-T: Data, limit: Nat, +depth: Nat, +cap: Nat, len: Nat, arr: Array<Maybe<&2, T>>, fits: Bool) -> DynArray<&2, T>:
146	  match fits:
147	    case True{}:
148	      DA{limit, depth, cap, len, arr}
149	    case False{}:
150	      DA{limit, 1n+depth, Nat.double(cap), len, grown(T, depth, arr)}
151	
152	def grow_step(-T: Data, +n: Nat, st: DynArray<&2, T>) -> DynArray<&2, T>:
153	  DA{limit, +depth, +cap, len, arr} = st
154	  grow_if(T, limit, depth, cap, len, arr, Nat.is_le(n, cap))
155	
156	# Doubles until n fits; `fuel` = limit - depth bounds the number of doublings.
157	def grow_until(-T: Data, fuel: Nat, +n: Nat, st: DynArray<&2, T>) -> DynArray<&2, T>:
158	  match fuel:
159	    case 0n:
160	      st
161	    case 1n+f:
162	      grow_until(T, f, n, grow_step(T, n, st))
163	
164	# The feasibility test (n <= 2^limit) is only reached when the cached capacity
165	# does not already suffice: computing 2^limit is O(limit) and reserve is
166	# otherwise O(1).
167	def reserve_room(-T: Data, +limit: Nat, +depth: Nat, +cap: Nat, len: Nat, arr: Array<Maybe<&2, T>>, +n: Nat, feasible: Bool) -> DynArray<&2, T> & Result<&2, &2, E.Error, Unit>:
168	  match feasible:
169	    case True{}:
170	      (grow_until(T, Nat.sub(limit, depth), n, DA{limit, depth, cap, len, arr}), Done{Unit{}})
171	    case False{}:
172	      (DA{limit, depth, cap, len, arr}, Fail{E.CapacityExceeded{}})
173	
174	def reserve_checked(-T: Data, +limit: Nat, +depth: Nat, +cap: Nat, len: Nat, arr: Array<Maybe<&2, T>>, +n: Nat, fits: Bool) -> DynArray<&2, T> & Result<&2, &2, E.Error, Unit>:
175	  match fits:
176	    case True{}:
177	      (DA{limit, depth, cap, len, arr}, Done{Unit{}})
178	    case False{}:
179	      reserve_room(T, limit, depth, cap, len, arr, n, Nat.is_le(n, pow2(limit)))
180	
181	# Ensures capacity >= n (new capacity: least 2^k >= n with k >= depth).
182	def reserve(-T: Data, da: DynArray<&2, T>, +n: Nat) -> DynArray<&2, T> & Result<&2, &2, E.Error, Unit>:
183	  DA{+limit, +depth, +cap, len, arr} = da
184	  reserve_checked(T, limit, depth, cap, len, arr, n, Nat.is_le(n, cap))
185	
186	# ---- clear / to_list ----
187	
188	# Keeps the capacity; all slots become None.
189	def clear(-T: Data, da: DynArray<&2, T>) -> DynArray<&2, T>:
190	  DA{limit, +depth, +cap, len, arr} = da
191	  DA{limit, depth, cap, 0n, empty_slots(T, depth)}
192	
193	# to_list walks the occupied slots BY INDEX, newest first, and conses them:
194	# the walk gives the array back, so nothing is cloned, and a `Base.Array` is
195	# never matched structurally (that destroys the flat representation, see
196	# docs/VALIDATION.md).
197	def cons_some(-T: Data, x: Maybe<&2, T>, acc: List<&2, T>) -> List<&2, T>:
198	  match x:
199	    case None{}:
200	      acc
201	    case Some{v}:
202	      Con{v, acc}
203	
204	def dec1(n: Nat) -> Nat:
205	  match n:
206	    case 0n:
207	      0n
208	    case 1n+p:
209	      p
210	
211	# k slots are still to be read, the last of them first: the pair `r` is slot
212	# k - 1, already read.
213	def tl_go(k: Nat, -T: Data, acc: List<&2, T>, r: Array<Maybe<&2, T>> & Maybe<&2, T>) -> Array<Maybe<&2, T>> & List<&2, T>:
214	  match k r:
215	    case 0n Tuple{a, x}:
216	      (a, acc)
217	    case 1n+ +m Tuple{a, x}:
218	      tl_go(m, T, cons_some(T, x, acc), Array.get(Maybe<&2, T>, a, U32.from_nat(dec1(m))))
219	
220	def tl_done(-T: Data, limit: Nat, depth: Nat, +cap: Nat, +len: Nat, r: Array<Maybe<&2, T>> & List<&2, T>) -> DynArray<&2, T> & List<&2, T>:
221	  (a, xs) = r
222	  (DA{limit, depth, cap, len, a}, xs)
223	
224	def tl_start(-T: Data, limit: Nat, depth: Nat, +cap: Nat, len: Nat, arr: Array<Maybe<&2, T>>) -> DynArray<&2, T> & List<&2, T>:
225	  match len:
226	    case 0n:
227	      (DA{limit, depth, cap, 0n, arr}, Nil{})
228	    case 1n+ +m:
229	      tl_done(T, limit, depth, cap, 1n+m, tl_go(1n+m, T, Nil{}, Array.get(Maybe<&2, T>, arr, U32.from_nat(m))))
230	
231	def to_list(-T: Data, da: DynArray<&2, T>) -> DynArray<&2, T> & List<&2, T>:
232	  DA{limit, depth, +cap, len, arr} = da
233	  tl_start(T, limit, depth, cap, len, arr)
234	
235	# ---- operation traces ----
236	
237	def obs_nat(-T: Data, r: DynArray<&2, T> & Nat) -> DynArray<&2, T> & E.Obs<T>:
238	  (d, n) = r
239	  (d, E.ONat{n})
240	
241	def obs_item(-T: Data, r: DynArray<&2, T> & Result<&2, &2, E.Error, T>) -> DynArray<&2, T> & E.Obs<T>:
242	  (d, x) = r
243	  (d, E.OItem{x})
244	
245	def obs_unit(-T: Data, r: DynArray<&2, T> & Result<&2, &2, E.Error, Unit>) -> DynArray<&2, T> & E.Obs<T>:
246	  (d, x) = r
247	  (d, E.OUnit{x})
248	
249	def obs_list(-T: Data, r: DynArray<&2, T> & List<&2, T>) -> DynArray<&2, T> & E.Obs<T>:
250	  (d, xs) = r
251	  (d, E.OList{xs})
252	
253	def step(-T: Data, da: DynArray<&2, T>, op: E.Op<T>) -> DynArray<&2, T> & E.Obs<T>:
254	  match op:
255	    case E.Length{}:
256	      obs_nat(T, length(T, da))
257	    case E.Capacity{}:
258	      obs_nat(T, capacity(T, da))
259	    case E.Get{i}:
260	      obs_item(T, get(T, da, i))
261	    case E.Set{i, v}:
262	      obs_unit(T, set(T, da, i, v))
263	    case E.Push{v}:
264	      obs_unit(T, push(T, da, v))
265	    case E.Pop{}:
266	      obs_item(T, pop(T, da))
267	    case E.Reserve{n}:
268	      obs_unit(T, reserve(T, da, n))
269	    case E.Clear{}:
270	      (clear(T, da), E.OUnit{Done{Unit{}}})
271	    case E.ToList{}:
272	      obs_list(T, to_list(T, da))
273	
274	def record(-T: Data, acc: List<&2, E.Obs<T>>, r: DynArray<&2, T> & E.Obs<T>) -> DynArray<&2, T> & List<&2, E.Obs<T>>:
275	  (da, o) = r
276	  (da, Con{o, acc})
277	
278	def step_acc(-T: Data, op: E.Op<T>, st: DynArray<&2, T> & List<&2, E.Obs<T>>) -> DynArray<&2, T> & List<&2, E.Obs<T>>:
279	  (da, acc) = st
280	  record(T, acc, step(T, da, op))
281	
282	# Runs ops left to right; observations are accumulated newest-first.
283	def run_acc(-T: Data, ops: List<&2, E.Op<T>>, st: DynArray<&2, T> & List<&2, E.Obs<T>>) -> DynArray<&2, T> & List<&2, E.Obs<T>>:
284	  match ops:
285	    case Nil{}:
286	      st
287	    case Con{op, rest}:
288	      run_acc(T, rest, step_acc(T, op, st))
289	
290	def finish(-T: Data, st: DynArray<&2, T> & List<&2, E.Obs<T>>) -> DynArray<&2, T> & List<&2, E.Obs<T>>:
291	  (da, acc) = st
292	  (da, List.reverse(&2, E.Obs<T>, acc))
293	
294	# Final state and the observation of every operation, in order.
295	def run(-T: Data, ops: List<&2, E.Op<T>>, da: DynArray<&2, T>) -> DynArray<&2, T> & List<&2, E.Obs<T>>:
296	  finish(T, run_acc(T, ops, (da, Nil{})))
297	
298	# ---- executable specializations at a closed element type ----
299	#
300	# Bend 2.0.16's native C backend miscompiles Base.Array operations whose
301	# element type is still open (an erased `-T` parameter): `Array.new` at a bare
302	# type variable is rejected outright ("an open Array element type"), and
303	# `Array.get`/`Array.set`/`Array.swap`/`Array.clone` under `Maybe<&2, T>`
304	# silently read back wrong data for any element that is not a machine
305	# immediate. See docs/VALIDATION.md and tests/runtime_defects/.
306	#
307	# The definitions above stay parametric, so their proofs are universal in T.
308	# The `*_at` definitions below are template specializations: `~T` is a
309	# compile-time parameter, so every Base.Array call is compiled at a closed
310	# element type. They are the entry points used by tests and benchmarks, and
311	# proofs/dynamic_array/closed.bend proves each of them equal to the
312	# parametric definition at its instance, so every law above transfers.
313	#
314	# Only the definitions that (transitively) reach a Base.Array call need a
315	# specialization; the purely structural helpers are shared.
316	
317	def empty_slots_at(~T: Data, +depth: Nat) -> Array<Maybe<&2, T>>:
318	  Array.new(Maybe<&2, T>, depth, None{})
319	
320	def new_at(~T: Data) -> DynArray<&2, T>:
321	  DA{max_depth(), 0n, 1n, 0n, empty_slots_at(~T, 0n)}
322	
323	def with_limit_at(~T: Data, +k: Nat) -> DynArray<&2, T>:
324	  DA{clamp_limit(k, Nat.is_lt(k, max_depth())), 0n, 1n, 0n, empty_slots_at(~T, 0n)}
325	
326	# Keep the element type specialized through the returned payload. Calling the
327	# erased generic get_found here boxes composite Data on every indexed read.
328	def get_found_at(~T: Data, limit: Nat, depth: Nat, cap: Nat, len: Nat, r: Array<Maybe<&2, T>> & Maybe<&2, T>) -> DynArray<&2, T> & Result<&2, &2, E.Error, T>:
329	  match r:
330	    case Tuple{arr, None{}}:
331	      (DA{limit, depth, cap, len, arr}, Fail{E.IndexOutOfRange{}})
332	    case Tuple{arr, Some{x}}:
333	      (DA{limit, depth, cap, len, arr}, Done{x})
334	
335	def get_checked_at(~T: Data, limit: Nat, depth: Nat, +cap: Nat, len: Nat, arr: Array<Maybe<&2, T>>, i: Nat, ok: Bool) -> DynArray<&2, T> & Result<&2, &2, E.Error, T>:
336	  match ok:
337	    case True{}:
338	      get_found_at(~T, limit, depth, cap, len, Array.get(Maybe<&2, T>, arr, U32.from_nat(i)))
339	    case False{}:
340	      (DA{limit, depth, cap, len, arr}, Fail{E.IndexOutOfRange{}})
341	
342	def get_at(~T: Data, da: DynArray<&2, T>, +i: Nat) -> DynArray<&2, T> & Result<&2, &2, E.Error, T>:
343	  DA{limit, depth, cap, +len, arr} = da
344	  get_checked_at(~T, limit, depth, cap, len, arr, i, Nat.is_lt(i, len))
345	
346	def set_checked_at(~T: Data, limit: Nat, depth: Nat, +cap: Nat, len: Nat, arr: Array<Maybe<&2, T>>, i: Nat, v: T, ok: Bool) -> DynArray<&2, T> & Result<&2, &2, E.Error, Unit>:
347	  match ok:
348	    case True{}:
349	      (DA{limit, depth, cap, len, Array.set(Maybe<&2, T>, arr, U32.from_nat(i), Some{v})}, Done{Unit{}})
350	    case False{}:
351	      (DA{limit, depth, cap, len, arr}, Fail{E.IndexOutOfRange{}})
352	
353	def set_at(~T: Data, da: DynArray<&2, T>, +i: Nat, v: T) -> DynArray<&2, T> & Result<&2, &2, E.Error, Unit>:
354	  DA{limit, depth, cap, +len, arr} = da
355	  set_checked_at(~T, limit, depth, cap, len, arr, i, v, Nat.is_lt(i, len))
356	
357	def grown_at(~T: Data, +depth: Nat, arr: Array<Maybe<&2, T>>) -> Array<Maybe<&2, T>>:
358	  ANode{arr, empty_slots_at(~T, depth)}
359	
360	def push_room_at(~T: Data, limit: Nat, +depth: Nat, +cap: Nat, +len: Nat, arr: Array<Maybe<&2, T>>, v: T, room: Bool, grow: Bool) -> DynArray<&2, T> & Result<&2, &2, E.Error, Unit>:
361	  match room grow:
362	    case True{} _:
363	      (DA{limit, depth, cap, 1n+len, Array.set(Maybe<&2, T>, arr, U32.from_nat(len), Some{v})}, Done{Unit{}})
364	    case False{} True{}:
365	      (DA{limit, 1n+depth, Nat.double(cap), 1n+len, Array.set(Maybe<&2, T>, grown_at(~T, depth, arr), U32.from_nat(len), Some{v})}, Done{Unit{}})
366	    case False{} False{}:
367	      (DA{limit, depth, cap, len, arr}, Fail{E.CapacityExceeded{}})
368	
369	def push_at(~T: Data, da: DynArray<&2, T>, v: T) -> DynArray<&2, T> & Result<&2, &2, E.Error, Unit>:
370	  DA{+limit, +depth, +cap, +len, arr} = da
371	  push_room_at(~T, limit, depth, cap, len, arr, v, Nat.is_lt(len, cap), Nat.is_lt(depth, limit))
372	
373	def pop_len_at(~T: Data, limit: Nat, depth: Nat, +cap: Nat, len: Nat, arr: Array<Maybe<&2, T>>) -> DynArray<&2, T> & Result<&2, &2, E.Error, T>:
374	  match len:
375	    case 0n:
376	      (DA{limit, depth, cap, 0n, arr}, Fail{E.EmptyArray{}})
377	    case 1n+ +m:
378	      pop_found(T, limit, depth, cap, m, Array.swap(Maybe<&2, T>, arr, U32.from_nat(m), None{}))
379	
380	def pop_at(~T: Data, da: DynArray<&2, T>) -> DynArray<&2, T> & Result<&2, &2, E.Error, T>:
381	  DA{limit, depth, cap, len, arr} = da
382	  pop_len_at(~T, limit, depth, cap, len, arr)
383	
384	def grow_if_at(~T: Data, limit: Nat, +depth: Nat, +cap: Nat, len: Nat, arr: Array<Maybe<&2, T>>, fits: Bool) -> DynArray<&2, T>:
385	  match fits:
386	    case True{}:
387	      DA{limit, depth, cap, len, arr}
388	    case False{}:
389	      DA{limit, 1n+depth, Nat.double(cap), len, grown_at(~T, depth, arr)}
390	
391	def grow_step_at(~T: Data, +n: Nat, st: DynArray<&2, T>) -> DynArray<&2, T>:
392	  DA{limit, +depth, +cap, len, arr} = st
393	  grow_if_at(~T, limit, depth, cap, len, arr, Nat.is_le(n, cap))
394	
395	def grow_until_at(~T: Data, fuel: Nat, +n: Nat, st: DynArray<&2, T>) -> DynArray<&2, T>:
396	  match fuel:
397	    case 0n:
398	      st
399	    case 1n+f:
400	      grow_until_at(~T, f, n, grow_step_at(~T, n, st))
401	
402	# The feasibility test (n <= 2^limit) is only reached when the cached capacity
403	# does not already suffice: computing 2^limit is O(limit) and reserve is
404	# otherwise O(1).
405	def reserve_room_at(~T: Data, +limit: Nat, +depth: Nat, +cap: Nat, len: Nat, arr: Array<Maybe<&2, T>>, +n: Nat, feasible: Bool) -> DynArray<&2, T> & Result<&2, &2, E.Error, Unit>:
406	  match feasible:
407	    case True{}:
408	      (grow_until_at(~T, Nat.sub(limit, depth), n, DA{limit, depth, cap, len, arr}), Done{Unit{}})
409	    case False{}:
410	      (DA{limit, depth, cap, len, arr}, Fail{E.CapacityExceeded{}})
411	
412	def reserve_checked_at(~T: Data, +limit: Nat, +depth: Nat, +cap: Nat, len: Nat, arr: Array<Maybe<&2, T>>, +n: Nat, fits: Bool) -> DynArray<&2, T> & Result<&2, &2, E.Error, Unit>:
413	  match fits:
414	    case True{}:
415	      (DA{limit, depth, cap, len, arr}, Done{Unit{}})
416	    case False{}:
417	      reserve_room_at(~T, limit, depth, cap, len, arr, n, Nat.is_le(n, P2.pow2t(limit)))
418	
419	def reserve_at(~T: Data, da: DynArray<&2, T>, +n: Nat) -> DynArray<&2, T> & Result<&2, &2, E.Error, Unit>:
420	  DA{+limit, +depth, +cap, len, arr} = da
421	  reserve_checked_at(~T, limit, depth, cap, len, arr, n, Nat.is_le(n, cap))
422	
423	# The executable clear resets the occupied slots [0, length) to None, top
424	# down, and keeps the block: O(length), no allocation. Dropping the old block
425	# and allocating a fresh one (what the parametric `clear` describes) walks
426	# every one of the 2^depth slots twice in the runtime. Every slot at or past
427	# the length already holds None, so the result is the same all-None block;
428	# proofs/containers/dynamic_array/clear.bend proves it on every good state.
429	def clear_go_at(~T: Data, k: Nat, arr: Array<Maybe<&2, T>>) -> Array<Maybe<&2, T>>:
430	  match k:
431	    case 0n:
432	      arr
433	    case 1n+ +m:
434	      clear_go_at(~T, m, Array.set(Maybe<&2, T>, arr, U32.from_nat(m), None{}))
435	
436	def clear_at(~T: Data, da: DynArray<&2, T>) -> DynArray<&2, T>:
437	  DA{+limit, +depth, +cap, len, arr} = da
438	  DA{limit, depth, cap, 0n, clear_go_at(~T, len, arr)}
439	
440	# The executable to_list is the same indexed walk, compiled at a closed
441	# element type; proofs/dynamic_array/closed.bend proves the two agree.
442	def tl_go_at(~T: Data, k: Nat, acc: List<&2, T>, r: Array<Maybe<&2, T>> & Maybe<&2, T>) -> Array<Maybe<&2, T>> & List<&2, T>:
443	  match k r:
444	    case 0n Tuple{a, x}:
445	      (a, acc)
446	    case 1n+ +m Tuple{a, x}:
447	      tl_go_at(~T, m, cons_some(T, x, acc), Array.get(Maybe<&2, T>, a, U32.from_nat(dec1(m))))
448	
449	def tl_start_at(~T: Data, limit: Nat, depth: Nat, +cap: Nat, len: Nat, arr: Array<Maybe<&2, T>>) -> DynArray<&2, T> & List<&2, T>:
450	  match len:
451	    case 0n:
452	      (DA{limit, depth, cap, 0n, arr}, Nil{})
453	    case 1n+ +m:
454	      tl_done(T, limit, depth, cap, 1n+m, tl_go_at(~T, 1n+m, Nil{}, Array.get(Maybe<&2, T>, arr, U32.from_nat(m))))
455	
456	def to_list_at(~T: Data, da: DynArray<&2, T>) -> DynArray<&2, T> & List<&2, T>:
457	  DA{limit, depth, +cap, len, arr} = da
458	  tl_start_at(~T, limit, depth, cap, len, arr)
459	
460	def step_at(~T: Data, da: DynArray<&2, T>, op: E.Op<T>) -> DynArray<&2, T> & E.Obs<T>:
461	  match op:
462	    case E.Length{}:
463	      obs_nat(T, length(T, da))
464	    case E.Capacity{}:
465	      obs_nat(T, capacity(T, da))
466	    case E.Get{i}:
467	      obs_item(T, get_at(~T, da, i))
468	    case E.Set{i, v}:
469	      obs_unit(T, set_at(~T, da, i, v))
470	    case E.Push{v}:
471	      obs_unit(T, push_at(~T, da, v))
472	    case E.Pop{}:
473	      obs_item(T, pop_at(~T, da))
474	    case E.Reserve{n}:
475	      obs_unit(T, reserve_at(~T, da, n))
476	    case E.Clear{}:
477	      (clear_at(~T, da), E.OUnit{Done{Unit{}}})
478	    case E.ToList{}:
479	      obs_list(T, to_list_at(~T, da))
480	
481	def step_acc_at(~T: Data, op: E.Op<T>, st: DynArray<&2, T> & List<&2, E.Obs<T>>) -> DynArray<&2, T> & List<&2, E.Obs<T>>:
482	  (da, acc) = st
483	  record(T, acc, step_at(~T, da, op))
484	
485	def run_acc_at(~T: Data, ops: List<&2, E.Op<T>>, st: DynArray<&2, T> & List<&2, E.Obs<T>>) -> DynArray<&2, T> & List<&2, E.Obs<T>>:
486	  match ops:
487	    case Nil{}:
488	      st
489	    case Con{op, rest}:
490	      run_acc_at(~T, rest, step_acc_at(~T, op, st))
491	
492	def run_at(~T: Data, ops: List<&2, E.Op<T>>, da: DynArray<&2, T>) -> DynArray<&2, T> & List<&2, E.Obs<T>>:
493	  finish(T, run_acc_at(~T, ops, (da, Nil{})))
494	
495	# ---- owning elements (Type) ----
496	# Same DA representation and native Base.Array storage. No operation copies T.
497	# Data clients keep their existing get/to_list API at quantity &2. Owning
498	# clients use quantity &1 and move values with pop/swap/update/into_list.
499	# A failed push or swap returns the supplied value in E.Rejected.
500	
501	# Stock Array.new requires Data. This fresh-empty initializer is O(c log c)
502	# in the native backend because ANode merges blocks; see ownership docs.
503	def empty_owned(~T: Type, depth: Nat) -> Array<Maybe<&1, T>>:
504	  match depth:
505	    case 0n:
506	      ALeaf{None{}}
507	    case 1n+ +p:
508	      ANode{empty_owned(~T, p), empty_owned(~T, p)}
509	
510	def new_owned(~T: Type) -> DynArray<&1, T>:
511	  DA{max_depth(), 0n, 1n, 0n, empty_owned(~T, 0n)}
512	
513	def with_limit_owned(~T: Type, +k: Nat) -> DynArray<&1, T>:
514	  DA{clamp_limit(k, Nat.is_lt(k, max_depth())), 0n, 1n, 0n, empty_owned(~T, 0n)}
515	
516	def length_owned(~T: Type, da: DynArray<&1, T>) -> DynArray<&1, T> & Nat:
517	  DA{limit, depth, cap, +len, arr} = da
518	  (DA{limit, depth, cap, len, arr}, len)
519	
520	def capacity_owned(~T: Type, da: DynArray<&1, T>) -> DynArray<&1, T> & Nat:
521	  DA{limit, depth, +cap, len, arr} = da
522	  (DA{limit, depth, cap, len, arr}, cap)
523	
524	def grown_owned(~T: Type, +depth: Nat, arr: Array<Maybe<&1, T>>) -> Array<Maybe<&1, T>>:
525	  ANode{arr, empty_owned(~T, depth)}
526	
527	def push_room_owned(~T: Type, limit: Nat, +depth: Nat, +cap: Nat, +len: Nat, arr: Array<Maybe<&1, T>>, v: T, room: Bool, grow: Bool) -> DynArray<&1, T> & Result<&1, &2, E.Rejected<T>, Unit>:
528	  match room grow:
529	    case True{} _:
530	      (DA{limit, depth, cap, 1n+len, Array.set(Maybe<&1, T>, arr, U32.from_nat(len), Some{v})}, Done{Unit{}})
531	    case False{} True{}:
532	      (DA{limit, 1n+depth, Nat.double(cap), 1n+len, Array.set(Maybe<&1, T>, grown_owned(~T, depth, arr), U32.from_nat(len), Some{v})}, Done{Unit{}})
533	    case False{} False{}:
534	      (DA{limit, depth, cap, len, arr}, Fail{E.Rejected{E.CapacityExceeded{}, v}})
535	
536	def push_owned(~T: Type, da: DynArray<&1, T>, v: T) -> DynArray<&1, T> & Result<&1, &2, E.Rejected<T>, Unit>:
537	  DA{+limit, +depth, +cap, +len, arr} = da
538	  push_room_owned(~T, limit, depth, cap, len, arr, v, Nat.is_lt(len, cap), Nat.is_lt(depth, limit))
539	
540	def owned_result(~T: Type, slot: Maybe<&1, T>) -> Result<&2, &1, E.Error, T>:
541	  match slot:
542	    case None{}:
543	      Fail{E.IndexOutOfRange{}}
544	    case Some{x}:
545	      Done{x}
546	
547	def pop_found_owned(~T: Type, limit: Nat, depth: Nat, cap: Nat, n: Nat, r: Array<Maybe<&1, T>> & Maybe<&1, T>) -> DynArray<&1, T> & Result<&2, &1, E.Error, T>:
548	  (arr, old) = r
549	  (DA{limit, depth, cap, n, arr}, owned_result(~T, old))
550	
551	def pop_len_owned(~T: Type, limit: Nat, depth: Nat, cap: Nat, len: Nat, arr: Array<Maybe<&1, T>>) -> DynArray<&1, T> & Result<&2, &1, E.Error, T>:
552	  match len:
553	    case 0n:
554	      (DA{limit, depth, cap, 0n, arr}, Fail{E.EmptyArray{}})
555	    case 1n+ +n:
556	      pop_found_owned(~T, limit, depth, cap, n, Array.swap(Maybe<&1, T>, arr, U32.from_nat(n), None{}))
557	
558	def pop_owned(~T: Type, da: DynArray<&1, T>) -> DynArray<&1, T> & Result<&2, &1, E.Error, T>:
559	  DA{limit, depth, cap, len, arr} = da
560	  pop_len_owned(~T, limit, depth, cap, len, arr)
561	
562	# The result on success is the previous value. Invalid indices return v.
563	# None can occur only in an invalid externally constructed DA representation.
564	def swap_found_owned(~T: Type, limit: Nat, depth: Nat, cap: Nat, len: Nat, r: Array<Maybe<&1, T>> & Maybe<&1, T>) -> DynArray<&1, T> & Result<&1, &1, E.Rejected<T>, Maybe<&1, T>>:
565	  (arr, old) = r
566	  (DA{limit, depth, cap, len, arr}, Done{old})
567	
568	def swap_checked_owned(~T: Type, limit: Nat, depth: Nat, cap: Nat, len: Nat, arr: Array<Maybe<&1, T>>, i: Nat, v: T, ok: Bool) -> DynArray<&1, T> & Result<&1, &1, E.Rejected<T>, Maybe<&1, T>>:
569	  match ok:
570	    case True{}:
571	      swap_found_owned(~T, limit, depth, cap, len, Array.swap(Maybe<&1, T>, arr, U32.from_nat(i), Some{v}))
572	    case False{}:
573	      (DA{limit, depth, cap, len, arr}, Fail{E.Rejected{E.IndexOutOfRange{}, v}})
574	
575	def swap_owned(~T: Type, da: DynArray<&1, T>, +i: Nat, v: T) -> DynArray<&1, T> & Result<&1, &1, E.Rejected<T>, Maybe<&1, T>>:
576	  DA{limit, depth, cap, +len, arr} = da
577	  swap_checked_owned(~T, limit, depth, cap, len, arr, i, v, Nat.is_lt(i, len))
578	
579	def set_done_owned(~T: Type, r: DynArray<T> & Result<&1, &1, E.Rejected<T>, Maybe<T>>) -> DynArray<T> & Result<&1, &2, E.Rejected<T>, Unit>:
580	  match r:
581	    case Tuple{da, Done{old}}:
582	      (da, Done{Unit{}})
583	    case Tuple{da, Fail{rejected}}:
584	      (da, Fail{rejected})
585	
586	# Replace and release the previous element. Use swap_owned to retain it.
587	def set_owned(~T: Type, da: DynArray<T>, i: Nat, value: T) -> DynArray<T> & Result<&1, &2, E.Rejected<T>, Unit>:
588	  set_done_owned(~T, swap_owned(~T, da, i, value))
589	
590	# Scoped ownership: f receives the element and must return a replacement.
591	# No placeholder escapes the call. f is not called for an invalid index.
592	def update_put_owned(~T: Type, ~R: Type, limit: Nat, depth: Nat, cap: Nat, len: Nat, arr: Array<Maybe<&1, T>>, i: Nat, r: T & R) -> DynArray<&1, T> & Result<&2, &1, E.Error, R>:
593	  (value, result) = r
594	  (DA{limit, depth, cap, len, Array.set(Maybe<&1, T>, arr, U32.from_nat(i), Some{value})}, Done{result})
595	
596	def update_found_owned(~T: Type, ~R: Type, limit: Nat, depth: Nat, cap: Nat, len: Nat, i: Nat, f: T -> T & R, r: Array<Maybe<&1, T>> & Maybe<&1, T>) -> DynArray<&1, T> & Result<&2, &1, E.Error, R>:
597	  match r:
598	    case Tuple{arr, None{}}:
599	      (DA{limit, depth, cap, len, arr}, Fail{E.IndexOutOfRange{}})
600	    case Tuple{arr, Some{x}}:
601	      update_put_owned(~T, ~R, limit, depth, cap, len, arr, i, f(x))
602	
603	def update_checked_owned(~T: Type, ~R: Type, limit: Nat, depth: Nat, cap: Nat, len: Nat, arr: Array<Maybe<&1, T>>, +i: Nat, f: T -> T & R, ok: Bool) -> DynArray<&1, T> & Result<&2, &1, E.Error, R>:
604	  match ok:
605	    case False{}:
606	      (DA{limit, depth, cap, len, arr}, Fail{E.IndexOutOfRange{}})
607	    case True{}:
608	      update_found_owned(~T, ~R, limit, depth, cap, len, i, f, Array.swap(Maybe<&1, T>, arr, U32.from_nat(i), None{}))
609	
610	def update_owned(~T: Type, ~R: Type, da: DynArray<&1, T>, +i: Nat, f: T -> T & R) -> DynArray<&1, T> & Result<&2, &1, E.Error, R>:
611	  DA{limit, depth, cap, +len, arr} = da
612	  update_checked_owned(~T, ~R, limit, depth, cap, len, arr, i, f, Nat.is_lt(i, len))
613	
614	def grow_if_owned(~T: Type, limit: Nat, +depth: Nat, +cap: Nat, len: Nat, arr: Array<Maybe<&1, T>>, fits: Bool) -> DynArray<&1, T>:
615	  match fits:
616	    case True{}:
617	      DA{limit, depth, cap, len, arr}
618	    case False{}:
619	      DA{limit, 1n+depth, Nat.double(cap), len, grown_owned(~T, depth, arr)}
620	
621	def grow_step_owned(~T: Type, +n: Nat, st: DynArray<&1, T>) -> DynArray<&1, T>:
622	  DA{limit, +depth, +cap, len, arr} = st
623	  grow_if_owned(~T, limit, depth, cap, len, arr, Nat.is_le(n, cap))
624	
625	def grow_until_owned(~T: Type, fuel: Nat, +n: Nat, st: DynArray<&1, T>) -> DynArray<&1, T>:
626	  match fuel:
627	    case 0n:
628	      st
629	    case 1n+f:
630	      grow_until_owned(~T, f, n, grow_step_owned(~T, n, st))
631	
632	def reserve_room_owned(~T: Type, +limit: Nat, +depth: Nat, cap: Nat, len: Nat, arr: Array<Maybe<&1, T>>, +n: Nat, feasible: Bool) -> DynArray<&1, T> & Result<&2, &2, E.Error, Unit>:
633	  match feasible:
634	    case False{}:
635	      (DA{limit, depth, cap, len, arr}, Fail{E.CapacityExceeded{}})
636	    case True{}:
637	      (grow_until_owned(~T, Nat.sub(limit, depth), n, DA{limit, depth, cap, len, arr}), Done{Unit{}})
638	
639	def reserve_checked_owned(~T: Type, +limit: Nat, depth: Nat, cap: Nat, len: Nat, arr: Array<Maybe<&1, T>>, +n: Nat, fits: Bool) -> DynArray<&1, T> & Result<&2, &2, E.Error, Unit>:
640	  match fits:
641	    case True{}:
642	      (DA{limit, depth, cap, len, arr}, Done{Unit{}})
643	    case False{}:
644	      reserve_room_owned(~T, limit, depth, cap, len, arr, n, Nat.is_le(n, pow2(limit)))
645	
646	def reserve_owned(~T: Type, da: DynArray<&1, T>, +n: Nat) -> DynArray<&1, T> & Result<&2, &2, E.Error, Unit>:
647	  DA{+limit, depth, +cap, len, arr} = da
648	  reserve_checked_owned(~T, limit, depth, cap, len, arr, n, Nat.is_le(n, cap))
649	
650	def clear_owned(~T: Type, da: DynArray<&1, T>) -> DynArray<&1, T>:
651	  DA{limit, +depth, cap, len, arr} = da
652	  DA{limit, depth, cap, 0n, empty_owned(~T, depth)}
653	
654	def cons_owned(~T: Type, x: Maybe<&1, T>, acc: List<&1, T>) -> List<&1, T>:
655	  match x:
656	    case None{}:
657	      acc
658	    case Some{v}:
659	      Con{v, acc}
660	
661	def drain_go_owned(~T: Type, k: Nat, acc: List<&1, T>, r: Array<Maybe<&1, T>> & Maybe<&1, T>) -> List<&1, T>:
662	  match k r:
663	    case 0n Tuple{arr, x}:
664	      cons_owned(~T, x, acc)
665	    case 1n+ +m Tuple{arr, x}:
666	      drain_go_owned(~T, m, cons_owned(~T, x, acc), Array.swap(Maybe<&1, T>, arr, U32.from_nat(m), None{}))
667	
668	def drain_len_owned(~T: Type, len: Nat, arr: Array<Maybe<&1, T>>) -> List<&1, T>:
669	  match len:
670	    case 0n:
671	      Nil{}
672	    case 1n+ +m:
673	      drain_go_owned(~T, m, Nil{}, Array.swap(Maybe<&1, T>, arr, U32.from_nat(m), None{}))
674	
675	# Consumes the container; values move into the returned list, in order.
676	def into_list_owned(~T: Type, da: DynArray<&1, T>) -> List<&1, T>:
677	  DA{limit, depth, cap, len, arr} = da
678	  drain_len_owned(~T, len, arr)
679	
680	# Copyable-element exchange, used by indexed collection storage. The previous
681	# value is returned and all other slots remain unchanged. Like set_at, an
682	# invalid index leaves the array unchanged and reports IndexOutOfRange.
683	def swap_checked_at(~T: Data, limit: Nat, depth: Nat, cap: Nat, len: Nat, arr: Array<Maybe<&2, T>>, i: Nat, v: T, ok: Bool) -> DynArray<&2, T> & Result<&2, &2, E.Error, T>:
684	  match ok:
685	    case True{}:
686	      get_found_at(~T, limit, depth, cap, len, Array.swap(Maybe<&2, T>, arr, U32.from_nat(i), Some{v}))
687	    case False{}:
688	      (DA{limit, depth, cap, len, arr}, Fail{E.IndexOutOfRange{}})
689	
690	def swap_at(~T: Data, da: DynArray<&2, T>, +i: Nat, v: T) -> DynArray<&2, T> & Result<&2, &2, E.Error, T>:
691	  DA{limit, depth, cap, +len, arr} = da
692	  swap_checked_at(~T, limit, depth, cap, len, arr, i, v, Nat.is_lt(i, len))