1	import Base
2	import ../lib/common.bend as C
3	import ../../src/containers/types/doubly_linked_list.bend as E
4	import ../lib/sequence.bend as V
5	
6	# Independent model of the doubly linked list with generational handles.
7	#
8	# A list is its elements' ids in order, and for every id ever issued its value
9	# (None once removed) and its generation. Removed ids are kept on a stack and
10	# reissued last-removed first; an id whose generation reached 2^32 - 1 is
11	# retired instead (never reissued). A new id, when none is free, is the next
12	# one, at generation 0. A handle names the list's tag, an id and a
13	# generation: it is foreign when the tag differs, and stale when its id is
14	# not live or its generation is not the id's current one.
15	#
16	# Nothing here refers to the arenas, links or free chain of the
17	# implementation.
18	
19	type DS<-T: Data> is Data:
20	  DS{tag: U32, order: List<&2, Nat>, vals: List<&2, Maybe<&2, T>>, gens: List<&2, U32>, free: List<&2, Nat>}
21	
22	def pick_list(+b: Bool, xs: List<&2, Nat>, ys: List<&2, Nat>) -> List<&2, Nat>:
23	  match b:
24	    case True{}:
25	      xs
26	    case False{}:
27	      ys
28	
29	def pick_maybe(+b: Bool, x: Maybe<&2, Nat>, y: Maybe<&2, Nat>) -> Maybe<&2, Nat>:
30	  match b:
31	    case True{}:
32	      x
33	    case False{}:
34	      y
35	
36	def cons_some(-T: Data, m: Maybe<&2, T>, xs: List<&2, T>) -> List<&2, T>:
37	  match m:
38	    case None{}:
39	      xs
40	    case Some{v}:
41	      Con{v, xs}
42	
43	def maybe_done(-T: Data, e: E.Error, m: Maybe<&2, T>) -> Result<&2, &2, E.Error, T>:
44	  match m:
45	    case None{}:
46	      Fail{e}
47	    case Some{v}:
48	      Done{v}
49	
50	def gen_of(+gens: List<&2, U32>, +i: Nat) -> U32:
51	  match gens i:
52	    case Nil{} _:
53	      0
54	    case Con{g, t} 0n:
55	      g
56	    case Con{g, t} 1n+p:
57	      gen_of(t, p)
58	
59	def val_of(-T: Data, +vals: List<&2, Maybe<&2, T>>, +i: Nat) -> Maybe<&2, T>:
60	  match vals i:
61	    case Nil{} _:
62	      None{}
63	    case Con{v, t} 0n:
64	      v
65	    case Con{v, t} 1n+p:
66	      val_of(T, t, p)
67	
68	def handle(+tag: U32, +gens: List<&2, U32>, +i: Nat) -> E.Handle:
69	  E.H{tag, U32.from_nat(i), gen_of(gens, i)}
70	
71	# ---- validity ----
72	
73	def live_gen(-T: Data, m: Maybe<&2, T>, +same: Bool) -> Maybe<&2, E.Error>:
74	  match m same:
75	    case None{} _:
76	      Some{E.StaleHandle{}}
77	    case Some{v} True{}:
78	      None{}
79	    case Some{v} False{}:
80	      Some{E.StaleHandle{}}
81	
82	def valid_own(-T: Data, +vals: List<&2, Maybe<&2, T>>, +gens: List<&2, U32>, +i: Nat, +g: U32, mine: Bool) -> Maybe<&2, E.Error>:
83	  match mine:
84	    case False{}:
85	      Some{E.ForeignHandle{}}
86	    case True{}:
87	      live_gen(T, val_of(T, vals, i), U32.is_eq(gen_of(gens, i), g))
88	
89	# None when h names a live element of the list at its current generation
90	def validate(-T: Data, +s: DS<T>, +h: E.Handle) -> Maybe<&2, E.Error>:
91	  match s h:
92	    case DS{+tag, +order, +vals, +gens, +free} E.H{+owner, +id, +g}:
93	      valid_own(T, vals, gens, U32.to_nat(id), g, U32.is_eq(owner, tag))
94	
95	# ---- positions in the order ----
96	
97	def ins_before(xs: List<&2, Nat>, +i: Nat, +n: Nat) -> List<&2, Nat>:
98	  match xs:
99	    case Nil{}:
100	      Nil{}
101	    case Con{+x, +t}:
102	      pick_list(Nat.is_eq(x, i), Con{n, Con{x, t}}, Con{x, ins_before(t, i, n)})
103	
104	def ins_after(xs: List<&2, Nat>, +i: Nat, +n: Nat) -> List<&2, Nat>:
105	  match xs:
106	    case Nil{}:
107	      Nil{}
108	    case Con{+x, +t}:
109	      pick_list(Nat.is_eq(x, i), Con{x, Con{n, t}}, Con{x, ins_after(t, i, n)})
110	
111	def delete(xs: List<&2, Nat>, +i: Nat) -> List<&2, Nat>:
112	  match xs:
113	    case Nil{}:
114	      Nil{}
115	    case Con{+x, +t}:
116	      pick_list(Nat.is_eq(x, i), t, Con{x, delete(t, i)})
117	
118	def first(xs: List<&2, Nat>) -> Maybe<&2, Nat>:
119	  match xs:
120	    case Nil{}:
121	      None{}
122	    case Con{x, t}:
123	      Some{x}
124	
125	# the element after i
126	def after(xs: List<&2, Nat>, +i: Nat) -> Maybe<&2, Nat>:
127	  match xs:
128	    case Nil{}:
129	      None{}
130	    case Con{+x, +t}:
131	      pick_maybe(Nat.is_eq(x, i), first(t), after(t, i))
132	
133	# the element before i (p: the element before the list)
134	def before(xs: List<&2, Nat>, +i: Nat, p: Maybe<&2, Nat>) -> Maybe<&2, Nat>:
135	  match xs:
136	    case Nil{}:
137	      None{}
138	    case Con{+x, +t}:
139	      pick_maybe(Nat.is_eq(x, i), p, before(t, i, Some{x}))
140	
141	def values(-T: Data, +vals: List<&2, Maybe<&2, T>>, xs: List<&2, Nat>) -> List<&2, T>:
142	  match xs:
143	    case Nil{}:
144	      Nil{}
145	    case Con{+x, +t}:
146	      cons_some(T, val_of(T, vals, x), values(T, vals, t))
147	
148	# ---- issuing an id ----
149	
150	# the id a new element takes, the list with the id reserved
151	def alloc(-T: Data, s: DS<T>) -> DS<T> & Nat:
152	  match s:
153	    case DS{+tag, +order, +vals, +gens, free}:
154	      match free:
155	        case Con{+i, rest}:
156	          (DS{tag, order, vals, gens, rest}, i)
157	        case Nil{}:
158	          (DS{tag, order, C.snoc(Maybe<&2, T>, vals, None{}), C.snoc(U32, gens, 0), Nil{}}, C.length(Maybe<&2, T>, vals))
159	
160	# where a new element goes
161	type Pos is Data:
162	  PFront{}
163	  PBack{}
164	  PBefore{i: Nat}
165	  PAfter{i: Nat}
166	
167	def place_order(pos: Pos, xs: List<&2, Nat>, +n: Nat) -> List<&2, Nat>:
168	  match pos:
169	    case PFront{}:
170	      Con{n, xs}
171	    case PBack{}:
172	      C.snoc(Nat, xs, n)
173	    case PBefore{+i}:
174	      ins_before(xs, i, n)
175	    case PAfter{+i}:
176	      ins_after(xs, i, n)
177	
178	# store x at the reserved id n and place n in the order
179	def place(-T: Data, s: DS<T>, +n: Nat, x: T, pos: Pos) -> DS<T> & E.Handle:
180	  match s:
181	    case DS{+tag, order, +vals, +gens, free}:
182	      (DS{tag, place_order(pos, order, n), C.update(Maybe<&2, T>, vals, n, Some{x}), gens, free}, handle(tag, gens, n))
183	
184	def inserted(-T: Data, r: DS<T> & Nat, x: T, pos: Pos) -> DS<T> & E.Handle:
185	  match r:
186	    case Tuple{s, +n}:
187	      place(T, s, n, x, pos)
188	
189	def push_front(-T: Data, s: DS<T>, x: T) -> DS<T> & E.Handle:
190	  inserted(T, alloc(T, s), x, PFront{})
191	
192	def push_back(-T: Data, s: DS<T>, x: T) -> DS<T> & E.Handle:
193	  inserted(T, alloc(T, s), x, PBack{})
194	
195	# ---- removal ----
196	
197	def retire(+gens: List<&2, U32>, +i: Nat, +free: List<&2, Nat>, +g: U32, exhausted: Bool) -> List<&2, U32> & List<&2, Nat>:
198	  match exhausted:
199	    case True{}:
200	      (gens, free)
201	    case False{}:
202	      (C.update(U32, gens, i, U32.inc(g)), Con{i, free})
203	
204	def removed(-T: Data, +tag: U32, +order: List<&2, Nat>, +vals: List<&2, Maybe<&2, T>>, +i: Nat, +v: T, r: List<&2, U32> & List<&2, Nat>) -> DS<T> & E.Obs<T>:
205	  match r:
206	    case Tuple{gens, free}:
207	      (DS{tag, delete(order, i), C.update(Maybe<&2, T>, vals, i, None{}), gens, free}, E.OVal{Done{v}})
208	
209	def remove_m(-T: Data, +tag: U32, +order: List<&2, Nat>, +vals: List<&2, Maybe<&2, T>>, +gens: List<&2, U32>, +free: List<&2, Nat>, +i: Nat, m: Maybe<&2, T>) -> DS<T> & E.Obs<T>:
210	  match m:
211	    case Some{+v}:
212	      removed(T, tag, order, vals, i, v, retire(gens, i, free, gen_of(gens, i), U32.is_eq(gen_of(gens, i), 4294967295)))
213	    case None{}:
214	      (DS{tag, order, vals, gens, free}, E.OVal{Fail{E.StaleHandle{}}})
215	
216	def remove_live(-T: Data, s: DS<T>, +i: Nat) -> DS<T> & E.Obs<T>:
217	  match s:
218	    case DS{+tag, +order, +vals, +gens, +free}:
219	      remove_m(T, tag, order, vals, gens, free, i, val_of(T, vals, i))
220	
221	# ---- one operation on a valid handle ----
222	
223	def get_live(-T: Data, s: DS<T>, +i: Nat) -> DS<T> & E.Obs<T>:
224	  match s:
225	    case DS{+tag, +order, +vals, +gens, +free}:
226	      (DS{tag, order, vals, gens, free}, E.OVal{maybe_done(T, E.StaleHandle{}, val_of(T, vals, i))})
227	
228	def set_live(-T: Data, s: DS<T>, +i: Nat, x: T) -> DS<T> & E.Obs<T>:
229	  match s:
230	    case DS{+tag, +order, +vals, +gens, +free}:
231	      (DS{tag, order, C.update(Maybe<&2, T>, vals, i, Some{x}), gens, free}, E.OUnit{Done{Unit{}}})
232	
233	def nbr(+tag: U32, +gens: List<&2, U32>, m: Maybe<&2, Nat>) -> Maybe<&2, E.Handle>:
234	  match m:
235	    case None{}:
236	      None{}
237	    case Some{+j}:
238	      Some{handle(tag, gens, j)}
239	
240	def next_live(-T: Data, s: DS<T>, +i: Nat) -> DS<T> & E.Obs<T>:
241	  match s:
242	    case DS{+tag, +order, +vals, +gens, +free}:
243	      (DS{tag, order, vals, gens, free}, E.ONbr{Done{nbr(tag, gens, after(order, i))}})
244	
245	def prev_live(-T: Data, s: DS<T>, +i: Nat) -> DS<T> & E.Obs<T>:
246	  match s:
247	    case DS{+tag, +order, +vals, +gens, +free}:
248	      (DS{tag, order, vals, gens, free}, E.ONbr{Done{nbr(tag, gens, before(order, i, None{}))}})
249	
250	def ins_obs(-T: Data, r: DS<T> & E.Handle) -> DS<T> & E.Obs<T>:
251	  match r:
252	    case Tuple{s, h}:
253	      (s, E.OInsert{Done{h}})
254	
255	def live_op(-T: Data, s: DS<T>, +op: E.Op<T>, +i: Nat) -> DS<T> & E.Obs<T>:
256	  match op:
257	    case E.InsertBefore{h, x}:
258	      ins_obs(T, inserted(T, alloc(T, s), x, PBefore{i}))
259	    case E.InsertAfter{h, x}:
260	      ins_obs(T, inserted(T, alloc(T, s), x, PAfter{i}))
261	    case E.Remove{h}:
262	      remove_live(T, s, i)
263	    case E.Get{h}:
264	      get_live(T, s, i)
265	    case E.Set{h, x}:
266	      set_live(T, s, i, x)
267	    case E.Next{h}:
268	      next_live(T, s, i)
269	    case E.Prev{h}:
270	      prev_live(T, s, i)
271	    case E.Length{}:
272	      (s, E.ONat{0n})
273	    case E.PushFront{x}:
274	      (s, E.ONat{0n})
275	    case E.PushBack{x}:
276	      (s, E.ONat{0n})
277	    case E.ToList{}:
278	      (s, E.ONat{0n})
279	
280	# the observation of op failing with e (the list is unchanged)
281	def failed(-T: Data, op: E.Op<T>, e: E.Error) -> E.Obs<T>:
282	  match op:
283	    case E.InsertBefore{h, x}:
284	      E.OInsert{Fail{e}}
285	    case E.InsertAfter{h, x}:
286	      E.OInsert{Fail{e}}
287	    case E.Remove{h}:
288	      E.OVal{Fail{e}}
289	    case E.Get{h}:
290	      E.OVal{Fail{e}}
291	    case E.Set{h, x}:
292	      E.OUnit{Fail{e}}
293	    case E.Next{h}:
294	      E.ONbr{Fail{e}}
295	    case E.Prev{h}:
296	      E.ONbr{Fail{e}}
297	    case E.Length{}:
298	      E.ONat{0n}
299	    case E.PushFront{x}:
300	      E.ONat{0n}
301	    case E.PushBack{x}:
302	      E.ONat{0n}
303	    case E.ToList{}:
304	      E.ONat{0n}
305	
306	def handle_id(+h: E.Handle) -> Nat:
307	  match h:
308	    case E.H{+owner, +id, +g}:
309	      U32.to_nat(id)
310	
311	def checked(-T: Data, +s: DS<T>, +op: E.Op<T>, +h: E.Handle, m: Maybe<&2, E.Error>) -> DS<T> & E.Obs<T>:
312	  match m:
313	    case Some{e}:
314	      (s, failed(T, op, e))
315	    case None{}:
316	      live_op(T, s, op, handle_id(h))
317	
318	def with_handle(-T: Data, +s: DS<T>, +op: E.Op<T>, +h: E.Handle) -> DS<T> & E.Obs<T>:
319	  checked(T, s, op, h, validate(T, s, h))
320	
321	def len_of(-T: Data, s: DS<T>) -> Nat:
322	  match s:
323	    case DS{+tag, +order, +vals, +gens, +free}:
324	      C.length(Nat, order)
325	
326	def list_of(-T: Data, s: DS<T>) -> List<&2, T>:
327	  match s:
328	    case DS{+tag, +order, +vals, +gens, +free}:
329	      values(T, vals, order)
330	
331	def pushed(-T: Data, r: DS<T> & E.Handle) -> DS<T> & E.Obs<T>:
332	  match r:
333	    case Tuple{s, h}:
334	      (s, E.OHandle{h})
335	
336	def step(-T: Data, +s: DS<T>, op: E.Op<T>) -> DS<T> & E.Obs<T>:
337	  match op:
338	    case E.Length{}:
339	      (s, E.ONat{len_of(T, s)})
340	    case E.PushFront{x}:
341	      pushed(T, push_front(T, s, x))
342	    case E.PushBack{x}:
343	      pushed(T, push_back(T, s, x))
344	    case E.InsertBefore{+h, +x}:
345	      with_handle(T, s, E.InsertBefore{h, x}, h)
346	    case E.InsertAfter{+h, +x}:
347	      with_handle(T, s, E.InsertAfter{h, x}, h)
348	    case E.Remove{+h}:
349	      with_handle(T, s, E.Remove{h}, h)
350	    case E.Get{+h}:
351	      with_handle(T, s, E.Get{h}, h)
352	    case E.Set{+h, +x}:
353	      with_handle(T, s, E.Set{h, x}, h)
354	    case E.Next{+h}:
355	      with_handle(T, s, E.Next{h}, h)
356	    case E.Prev{+h}:
357	      with_handle(T, s, E.Prev{h}, h)
358	    case E.ToList{}:
359	      (s, E.OList{list_of(T, s)})
360	
361	def empty(-T: Data, +tag: U32) -> DS<T>:
362	  DS{tag, Nil{}, Nil{}, Nil{}, Nil{}}
363	
364	def cons_obs(-T: Data, o: E.Obs<T>, r: DS<T> & List<&2, E.Obs<T>>) -> DS<T> & List<&2, E.Obs<T>>:
365	  match r:
366	    case Tuple{m, os}:
367	      (m, Con{o, os})
368	
369	def run(-T: Data, ops: List<&2, E.Op<T>>, +s: DS<T>) -> DS<T> & List<&2, E.Obs<T>>:
370	  match ops:
371	    case Nil{}:
372	      (s, Nil{})
373	    case Con{+op, rest}:
374	      cons_obs(T, Pair.snd(DS<T>, E.Obs<T>, step(T, s, op)), run(T, rest, Pair.fst(DS<T>, E.Obs<T>, step(T, s, op))))
375	
376	# ---- contract (SPARK formal containers) ----
377	# Each `<Subprogram>.<clause>` definition below states one Post clause of
378	# that SPARK subprogram, as a proposition on this model; the table names the
379	# clauses. proofs/containers/doubly_linked_list/ proves every clause under its clause name,
380	# and its `impl` lemma carries them to the implementation.
381	#
382	# Contracts of the doubly linked list in the style of SPARK's formal doubly
383	# linked lists (SPARKlib src/spark-containers-formal-doubly_linked_lists.ads,
384	# AdaCore/SPARKlib 46ec319; model predicates in spec/lib/sequence.bend).
385	# SPARK's cursors are our handles; Has_Element (Container, Position) is
386	# S.validate (s, h) = None; Positions is the order (the ids of the live
387	# elements, first to last: a handle's position is the index of its id);
388	# Model is S.list_of (the values along the order). Position clauses are
389	# stated on the order, split at the handle's id: order = a ++ [id] ++ b
390	# with id not in a (fsplit), so Position (h) = Length (a). A valid handle's
391	# id is in the order in every good list (doubly_linked_list/hlive.src,
392	# mem_of), which is the premise of fsplit. Each lemma is one Post clause of
393	# step; `impl` (via P.step_ok) carries every clause to the implementation.
394	#
395	#   SPARK subprogram (.ads line)   ours           clauses
396	#   Length (78)                    length         length_result, length_frame
397	#   Empty_List (71)                new            new_empty
398	#   Has_Element (1814)             validate       has_element (definition), valid_live
399	#   Element (419)                  get            get_frame, get_element
400	#   Replace_Element (430)          set            set_positions, set_element, set_others, set_gens
401	#   Prepend (836)                  push_front     push_front_positions, push_front_first, push_front_length
402	#   Append (905)                   push_back      push_back_positions, push_back_last, push_back_length
403	#   Insert Before (523)            insert_before  insert_before_equal, insert_before_at,
404	#                                                 insert_before_shifted, insert_before_length
405	#   Insert after (Next (Before))   insert_after   insert_after_equal, insert_after_at,
406	#                                                 insert_after_shifted, insert_after_length
407	#   Delete (978)                   remove         remove_equal, remove_shifted, remove_length,
408	#                                                 remove_result, remove_stale
409	#   Next (1614)                    next           next_result, next_position, next_frame
410	#   Previous (1652)                prev           prev_result, prev_first, prev_position, prev_frame
411	#   iteration (Iter_Model)         to_list        to_list_model, to_list_frame
412	#   implementation                 D.step         impl
413	# Not in this API: "=", Is_Empty, Clear, Assign/Copy/Move, Reference,
414	# Insert with Count, Delete with Count, Delete_First/Delete_Last,
415	# First/First_Element/Last/Last_Element (the ends are reached by the
416	# handles push returns), Reverse_Elements, Swap, Swap_Links, Splice, Find,
417	# Reverse_Find, Contains. SPARK's Pre (Has_Element) is a defensive check:
418	# a foreign or stale handle returns ForeignHandle / StaleHandle and changes
419	# nothing (the refinement proof's failed case).
420	
421	def nx(-T: Data, +s: DS<T>, +op: E.Op<T>) -> DS<T>:
422	  Pair.fst(DS<T>, E.Obs<T>, step(T, s, op))
423	
424	def ob(-T: Data, +s: DS<T>, +op: E.Op<T>) -> E.Obs<T>:
425	  Pair.snd(DS<T>, E.Obs<T>, step(T, s, op))
426	
427	def ord(-T: Data, s: DS<T>) -> List<&2, Nat>:
428	  match s:
429	    case DS{tag, order, vals, gens, free}:
430	      order
431	
432	def vls(-T: Data, s: DS<T>) -> List<&2, Maybe<&2, T>>:
433	  match s:
434	    case DS{tag, order, vals, gens, free}:
435	      vals
436	
437	def gns(-T: Data, s: DS<T>) -> List<&2, U32>:
438	  match s:
439	    case DS{tag, order, vals, gens, free}:
440	      gens
441	
442	# Has_Element (Container, Position)
443	def has_of(m: Maybe<&2, E.Error>) -> Bool:
444	  match m:
445	    case None{}:
446	      True{}
447	    case Some{e}:
448	      False{}
449	
450	def has_element(-T: Data, +s: DS<T>, +h: E.Handle) -> Bool:
451	  has_of(validate(T, s, h))
452	
453	# Previous: the last element of a, or p when a is empty
454	def lastm(xs: List<&2, Nat>, p: Maybe<&2, Nat>) -> Maybe<&2, Nat>:
455	  match xs:
456	    case Nil{}:
457	      p
458	    case Con{+x, t}:
459	      lastm(t, Some{x})
460	
461	# ---- the order split at a live id ----
462	def FSplit(+i: Nat, +xs: List<&2, Nat>) -> Type:
463	  Sigma<&1, &1, List<&2, Nat>, a => Sigma<&1, &1, List<&2, Nat>, b => {xs == C.append(Nat, a, Con{i, b}) : List<&2, Nat>} & {C.memn(i, a) == False{} : Bool}>>
464	
465	# Next (1614)
466	def Next.next_position(+a: List<&2, Nat>, +i: Nat, +b: List<&2, Nat>) -> Type:
467	  {C.nth(Nat, C.append(Nat, a, Con{i, b}), 1n+C.length(Nat, a)) == first(b) : Maybe<&2, Nat>}
468	
469	# Previous (1652)
470	def Previous.prev_position(+t: List<&2, Nat>, +x: Nat, +i: Nat, +b: List<&2, Nat>, +p: Maybe<&2, Nat>) -> Type:
471	  {lastm(Con{x, t}, p) == C.nth(Nat, C.append(Nat, Con{x, t}, Con{i, b}), C.length(Nat, t)) : Maybe<&2, Nat>}
472	
473	# Has_Element (1814)
474	def Has_Element.valid_live(-T: Data, +tag: U32, +order: List<&2, Nat>, +vals: List<&2, Maybe<&2, T>>, +gens: List<&2, U32>, +free: List<&2, Nat>, +h: E.Handle, +hv: {validate(T, DS{tag, order, vals, gens, free}, h) == None{} : Maybe<&2, E.Error>}) -> Type:
475	  Sigma<&1, &1, T, v => {val_of(T, vals, handle_id(h)) == Some{v} : Maybe<&2, T>}>
476	
477	# Length (78)
478	def Length.length_result(-T: Data, +s: DS<T>) -> Type:
479	  {ob(T, s, E.Length{}) == E.ONat{len_of(T, s)} : E.Obs<T>}
480	
481	# Length (78)
482	def Length.length_frame(-T: Data, +s: DS<T>) -> Type:
483	  {nx(T, s, E.Length{}) == s : DS<T>}
484	
485	# iteration (Iter_Model)
486	def Iteration.to_list_model(-T: Data, +s: DS<T>) -> Type:
487	  {ob(T, s, E.ToList{}) == E.OList{list_of(T, s)} : E.Obs<T>}
488	
489	# iteration (Iter_Model)
490	def Iteration.to_list_frame(-T: Data, +s: DS<T>) -> Type:
491	  {nx(T, s, E.ToList{}) == s : DS<T>}
492	
493	# Empty_List (71)
494	def Empty_List.new_empty(-T: Data, +tag: U32) -> Type:
495	  {len_of(T, empty(T, tag)) == 0n : Nat}
496	
497	# Element (419)
498	def Element.get_frame(-T: Data, +tag: U32, +order: List<&2, Nat>, +vals: List<&2, Maybe<&2, T>>, +gens: List<&2, U32>, +free: List<&2, Nat>, +h: E.Handle, +hv: {validate(T, DS{tag, order, vals, gens, free}, h) == None{} : Maybe<&2, E.Error>}) -> Type:
499	  {nx(T, DS{tag, order, vals, gens, free}, E.Get{h}) == DS{tag, order, vals, gens, free} : DS<T>}
500	
501	# Element (419)
502	def Element.get_element(-T: Data, +tag: U32, +order: List<&2, Nat>, +vals: List<&2, Maybe<&2, T>>, +gens: List<&2, U32>, +free: List<&2, Nat>, +h: E.Handle, +hv: {validate(T, DS{tag, order, vals, gens, free}, h) == None{} : Maybe<&2, E.Error>}, +v: T, +hval: {val_of(T, vals, handle_id(h)) == Some{v} : Maybe<&2, T>}) -> Type:
503	  {ob(T, DS{tag, order, vals, gens, free}, E.Get{h}) == E.OVal{Done{v}} : E.Obs<T>}
504	
505	# Replace_Element (430)
506	def Replace_Element.set_positions(-T: Data, +tag: U32, +order: List<&2, Nat>, +vals: List<&2, Maybe<&2, T>>, +gens: List<&2, U32>, +free: List<&2, Nat>, +h: E.Handle, +x: T, +hv: {validate(T, DS{tag, order, vals, gens, free}, h) == None{} : Maybe<&2, E.Error>}) -> Type:
507	  {ord(T, nx(T, DS{tag, order, vals, gens, free}, E.Set{h, x})) == order : List<&2, Nat>}
508	
509	# Replace_Element (430)
510	def Replace_Element.set_gens(-T: Data, +tag: U32, +order: List<&2, Nat>, +vals: List<&2, Maybe<&2, T>>, +gens: List<&2, U32>, +free: List<&2, Nat>, +h: E.Handle, +x: T, +hv: {validate(T, DS{tag, order, vals, gens, free}, h) == None{} : Maybe<&2, E.Error>}) -> Type:
511	  {gns(T, nx(T, DS{tag, order, vals, gens, free}, E.Set{h, x})) == gens : List<&2, U32>}
512	
513	# Replace_Element (430)
514	def Replace_Element.set_element(-T: Data, +tag: U32, +order: List<&2, Nat>, +vals: List<&2, Maybe<&2, T>>, +gens: List<&2, U32>, +free: List<&2, Nat>, +h: E.Handle, +x: T, +hv: {validate(T, DS{tag, order, vals, gens, free}, h) == None{} : Maybe<&2, E.Error>}, +v: T, +hval: {val_of(T, vals, handle_id(h)) == Some{v} : Maybe<&2, T>}) -> Type:
515	  {val_of(T, vls(T, nx(T, DS{tag, order, vals, gens, free}, E.Set{h, x})), handle_id(h)) == Some{x} : Maybe<&2, T>}
516	
517	# Replace_Element (430)
518	def Replace_Element.set_others(-T: Data, +tag: U32, +order: List<&2, Nat>, +vals: List<&2, Maybe<&2, T>>, +gens: List<&2, U32>, +free: List<&2, Nat>, +h: E.Handle, +x: T, +hv: {validate(T, DS{tag, order, vals, gens, free}, h) == None{} : Maybe<&2, E.Error>}, +j: Nat, +ne: {Nat.is_eq(handle_id(h), j) == False{} : Bool}) -> Type:
519	  {val_of(T, vls(T, nx(T, DS{tag, order, vals, gens, free}, E.Set{h, x})), j) == val_of(T, vals, j) : Maybe<&2, T>}
520	
521	# Prepend (836)
522	def Prepend.push_front_positions(-T: Data, +tag: U32, +order: List<&2, Nat>, +vals: List<&2, Maybe<&2, T>>, +gens: List<&2, U32>, +free: List<&2, Nat>, +x: T) -> Type:
523	  V.RangeShifted(Nat, order, ord(T, nx(T, DS{tag, order, vals, gens, free}, E.PushFront{x})), 0n, C.length(Nat, order), 1n)
524	
525	# Prepend (836)
526	def Prepend.push_front_first(-T: Data, +tag: U32, +order: List<&2, Nat>, +vals: List<&2, Maybe<&2, T>>, +gens: List<&2, U32>, +free: List<&2, Nat>, +x: T) -> Type:
527	  {C.nth(Nat, ord(T, nx(T, DS{tag, order, vals, gens, free}, E.PushFront{x})), 0n) == Some{Pair.snd(DS<T>, Nat, alloc(T, DS{tag, order, vals, gens, free}))} : Maybe<&2, Nat>}
528	
529	# Prepend (836)
530	def Prepend.push_front_length(-T: Data, +tag: U32, +order: List<&2, Nat>, +vals: List<&2, Maybe<&2, T>>, +gens: List<&2, U32>, +free: List<&2, Nat>, +x: T) -> Type:
531	  {C.length(Nat, ord(T, nx(T, DS{tag, order, vals, gens, free}, E.PushFront{x}))) == 1n+C.length(Nat, order) : Nat}
532	
533	# Append (905)
534	def Append.push_back_positions(-T: Data, +tag: U32, +order: List<&2, Nat>, +vals: List<&2, Maybe<&2, T>>, +gens: List<&2, U32>, +free: List<&2, Nat>, +x: T) -> Type:
535	  V.EqualPrefix(Nat, order, ord(T, nx(T, DS{tag, order, vals, gens, free}, E.PushBack{x})))
536	
537	# Append (905)
538	def Append.push_back_last(-T: Data, +tag: U32, +order: List<&2, Nat>, +vals: List<&2, Maybe<&2, T>>, +gens: List<&2, U32>, +free: List<&2, Nat>, +x: T) -> Type:
539	  {C.nth(Nat, ord(T, nx(T, DS{tag, order, vals, gens, free}, E.PushBack{x})), C.length(Nat, order)) == Some{Pair.snd(DS<T>, Nat, alloc(T, DS{tag, order, vals, gens, free}))} : Maybe<&2, Nat>}
540	
541	# Append (905)
542	def Append.push_back_length(-T: Data, +tag: U32, +order: List<&2, Nat>, +vals: List<&2, Maybe<&2, T>>, +gens: List<&2, U32>, +free: List<&2, Nat>, +x: T) -> Type:
543	  {C.length(Nat, ord(T, nx(T, DS{tag, order, vals, gens, free}, E.PushBack{x}))) == 1n+C.length(Nat, order) : Nat}
544	
545	# Insert Before (523)
546	def Insert.insert_before_equal(-T: Data, +tag: U32, +a: List<&2, Nat>, +b: List<&2, Nat>, +vals: List<&2, Maybe<&2, T>>, +gens: List<&2, U32>, +free: List<&2, Nat>, +h: E.Handle, +x: T, +hv: {validate(T, DS{tag, C.append(Nat, a, Con{handle_id(h), b}), vals, gens, free}, h) == None{} : Maybe<&2, E.Error>}, +hn: {C.memn(handle_id(h), a) == False{} : Bool}) -> Type:
547	  V.RangeEqual(Nat, C.append(Nat, a, Con{handle_id(h), b}), ord(T, nx(T, DS{tag, C.append(Nat, a, Con{handle_id(h), b}), vals, gens, free}, E.InsertBefore{h, x})), 0n, C.length(Nat, a))
548	
549	# Insert Before (523)
550	def Insert.insert_before_at(-T: Data, +tag: U32, +a: List<&2, Nat>, +b: List<&2, Nat>, +vals: List<&2, Maybe<&2, T>>, +gens: List<&2, U32>, +free: List<&2, Nat>, +h: E.Handle, +x: T, +hv: {validate(T, DS{tag, C.append(Nat, a, Con{handle_id(h), b}), vals, gens, free}, h) == None{} : Maybe<&2, E.Error>}, +hn: {C.memn(handle_id(h), a) == False{} : Bool}) -> Type:
551	  {C.nth(Nat, ord(T, nx(T, DS{tag, C.append(Nat, a, Con{handle_id(h), b}), vals, gens, free}, E.InsertBefore{h, x})), C.length(Nat, a)) == Some{Pair.snd(DS<T>, Nat, alloc(T, DS{tag, C.append(Nat, a, Con{handle_id(h), b}), vals, gens, free}))} : Maybe<&2, Nat>}
552	
553	# Insert Before (523)
554	def Insert.insert_before_shifted(-T: Data, +tag: U32, +a: List<&2, Nat>, +b: List<&2, Nat>, +vals: List<&2, Maybe<&2, T>>, +gens: List<&2, U32>, +free: List<&2, Nat>, +h: E.Handle, +x: T, +hv: {validate(T, DS{tag, C.append(Nat, a, Con{handle_id(h), b}), vals, gens, free}, h) == None{} : Maybe<&2, E.Error>}, +hn: {C.memn(handle_id(h), a) == False{} : Bool}) -> Type:
555	  V.RangeShifted(Nat, C.append(Nat, a, Con{handle_id(h), b}), ord(T, nx(T, DS{tag, C.append(Nat, a, Con{handle_id(h), b}), vals, gens, free}, E.InsertBefore{h, x})), C.length(Nat, a), C.length(Nat, C.append(Nat, a, Con{handle_id(h), b})), 1n)
556	
557	# Insert Before (523)
558	def Insert.insert_before_length(-T: Data, +tag: U32, +a: List<&2, Nat>, +b: List<&2, Nat>, +vals: List<&2, Maybe<&2, T>>, +gens: List<&2, U32>, +free: List<&2, Nat>, +h: E.Handle, +x: T, +hv: {validate(T, DS{tag, C.append(Nat, a, Con{handle_id(h), b}), vals, gens, free}, h) == None{} : Maybe<&2, E.Error>}, +hn: {C.memn(handle_id(h), a) == False{} : Bool}) -> Type:
559	  {C.length(Nat, ord(T, nx(T, DS{tag, C.append(Nat, a, Con{handle_id(h), b}), vals, gens, free}, E.InsertBefore{h, x}))) == 1n+C.length(Nat, C.append(Nat, a, Con{handle_id(h), b})) : Nat}
560	
561	# Insert after (Next (Before))
562	def Insert.insert_after_equal(-T: Data, +tag: U32, +a: List<&2, Nat>, +b: List<&2, Nat>, +vals: List<&2, Maybe<&2, T>>, +gens: List<&2, U32>, +free: List<&2, Nat>, +h: E.Handle, +x: T, +hv: {validate(T, DS{tag, C.append(Nat, a, Con{handle_id(h), b}), vals, gens, free}, h) == None{} : Maybe<&2, E.Error>}, +hn: {C.memn(handle_id(h), a) == False{} : Bool}) -> Type:
563	  V.RangeEqual(Nat, C.append(Nat, a, Con{handle_id(h), b}), ord(T, nx(T, DS{tag, C.append(Nat, a, Con{handle_id(h), b}), vals, gens, free}, E.InsertAfter{h, x})), 0n, 1n+C.length(Nat, a))
564	
565	# Insert after (Next (Before))
566	def Insert.insert_after_at(-T: Data, +tag: U32, +a: List<&2, Nat>, +b: List<&2, Nat>, +vals: List<&2, Maybe<&2, T>>, +gens: List<&2, U32>, +free: List<&2, Nat>, +h: E.Handle, +x: T, +hv: {validate(T, DS{tag, C.append(Nat, a, Con{handle_id(h), b}), vals, gens, free}, h) == None{} : Maybe<&2, E.Error>}, +hn: {C.memn(handle_id(h), a) == False{} : Bool}) -> Type:
567	  {C.nth(Nat, ord(T, nx(T, DS{tag, C.append(Nat, a, Con{handle_id(h), b}), vals, gens, free}, E.InsertAfter{h, x})), 1n+C.length(Nat, a)) == Some{Pair.snd(DS<T>, Nat, alloc(T, DS{tag, C.append(Nat, a, Con{handle_id(h), b}), vals, gens, free}))} : Maybe<&2, Nat>}
568	
569	# Insert after (Next (Before))
570	def Insert.insert_after_shifted(-T: Data, +tag: U32, +a: List<&2, Nat>, +b: List<&2, Nat>, +vals: List<&2, Maybe<&2, T>>, +gens: List<&2, U32>, +free: List<&2, Nat>, +h: E.Handle, +x: T, +hv: {validate(T, DS{tag, C.append(Nat, a, Con{handle_id(h), b}), vals, gens, free}, h) == None{} : Maybe<&2, E.Error>}, +hn: {C.memn(handle_id(h), a) == False{} : Bool}) -> Type:
571	  V.RangeShifted(Nat, C.append(Nat, a, Con{handle_id(h), b}), ord(T, nx(T, DS{tag, C.append(Nat, a, Con{handle_id(h), b}), vals, gens, free}, E.InsertAfter{h, x})), 1n+C.length(Nat, a), C.length(Nat, C.append(Nat, a, Con{handle_id(h), b})), 1n)
572	
573	# Insert after (Next (Before))
574	def Insert.insert_after_length(-T: Data, +tag: U32, +a: List<&2, Nat>, +b: List<&2, Nat>, +vals: List<&2, Maybe<&2, T>>, +gens: List<&2, U32>, +free: List<&2, Nat>, +h: E.Handle, +x: T, +hv: {validate(T, DS{tag, C.append(Nat, a, Con{handle_id(h), b}), vals, gens, free}, h) == None{} : Maybe<&2, E.Error>}, +hn: {C.memn(handle_id(h), a) == False{} : Bool}) -> Type:
575	  {C.length(Nat, ord(T, nx(T, DS{tag, C.append(Nat, a, Con{handle_id(h), b}), vals, gens, free}, E.InsertAfter{h, x}))) == 1n+C.length(Nat, C.append(Nat, a, Con{handle_id(h), b})) : Nat}
576	
577	# Delete (978)
578	def Delete.remove_result(-T: Data, +tag: U32, +a: List<&2, Nat>, +b: List<&2, Nat>, +vals: List<&2, Maybe<&2, T>>, +gens: List<&2, U32>, +free: List<&2, Nat>, +h: E.Handle, +hv: {validate(T, DS{tag, C.append(Nat, a, Con{handle_id(h), b}), vals, gens, free}, h) == None{} : Maybe<&2, E.Error>}, +v: T, +hval: {val_of(T, vals, handle_id(h)) == Some{v} : Maybe<&2, T>}) -> Type:
579	  {ob(T, DS{tag, C.append(Nat, a, Con{handle_id(h), b}), vals, gens, free}, E.Remove{h}) == E.OVal{Done{v}} : E.Obs<T>}
580	
581	# Delete (978)
582	def Delete.remove_equal(-T: Data, +tag: U32, +a: List<&2, Nat>, +b: List<&2, Nat>, +vals: List<&2, Maybe<&2, T>>, +gens: List<&2, U32>, +free: List<&2, Nat>, +h: E.Handle, +hv: {validate(T, DS{tag, C.append(Nat, a, Con{handle_id(h), b}), vals, gens, free}, h) == None{} : Maybe<&2, E.Error>}, +hn: {C.memn(handle_id(h), a) == False{} : Bool}, +v: T, +hval: {val_of(T, vals, handle_id(h)) == Some{v} : Maybe<&2, T>}) -> Type:
583	  V.RangeEqual(Nat, ord(T, nx(T, DS{tag, C.append(Nat, a, Con{handle_id(h), b}), vals, gens, free}, E.Remove{h})), C.append(Nat, a, Con{handle_id(h), b}), 0n, C.length(Nat, a))
584	
585	# Delete (978)
586	def Delete.remove_shifted(-T: Data, +tag: U32, +a: List<&2, Nat>, +b: List<&2, Nat>, +vals: List<&2, Maybe<&2, T>>, +gens: List<&2, U32>, +free: List<&2, Nat>, +h: E.Handle, +hv: {validate(T, DS{tag, C.append(Nat, a, Con{handle_id(h), b}), vals, gens, free}, h) == None{} : Maybe<&2, E.Error>}, +hn: {C.memn(handle_id(h), a) == False{} : Bool}, +v: T, +hval: {val_of(T, vals, handle_id(h)) == Some{v} : Maybe<&2, T>}) -> Type:
587	  V.RangeShifted(Nat, ord(T, nx(T, DS{tag, C.append(Nat, a, Con{handle_id(h), b}), vals, gens, free}, E.Remove{h})), C.append(Nat, a, Con{handle_id(h), b}), C.length(Nat, a), C.length(Nat, ord(T, nx(T, DS{tag, C.append(Nat, a, Con{handle_id(h), b}), vals, gens, free}, E.Remove{h}))), 1n)
588	
589	# Delete (978)
590	def Delete.remove_length(-T: Data, +tag: U32, +a: List<&2, Nat>, +b: List<&2, Nat>, +vals: List<&2, Maybe<&2, T>>, +gens: List<&2, U32>, +free: List<&2, Nat>, +h: E.Handle, +hv: {validate(T, DS{tag, C.append(Nat, a, Con{handle_id(h), b}), vals, gens, free}, h) == None{} : Maybe<&2, E.Error>}, +hn: {C.memn(handle_id(h), a) == False{} : Bool}, +v: T, +hval: {val_of(T, vals, handle_id(h)) == Some{v} : Maybe<&2, T>}) -> Type:
591	  {C.length(Nat, C.append(Nat, a, Con{handle_id(h), b})) == 1n+C.length(Nat, ord(T, nx(T, DS{tag, C.append(Nat, a, Con{handle_id(h), b}), vals, gens, free}, E.Remove{h}))) : Nat}
592	
593	# Delete (978)
594	def Delete.remove_stale(-T: Data, +tag: U32, +a: List<&2, Nat>, +b: List<&2, Nat>, +vals: List<&2, Maybe<&2, T>>, +gens: List<&2, U32>, +free: List<&2, Nat>, +h: E.Handle, +hv: {validate(T, DS{tag, C.append(Nat, a, Con{handle_id(h), b}), vals, gens, free}, h) == None{} : Maybe<&2, E.Error>}, +v: T, +hval: {val_of(T, vals, handle_id(h)) == Some{v} : Maybe<&2, T>}) -> Type:
595	  {has_element(T, nx(T, DS{tag, C.append(Nat, a, Con{handle_id(h), b}), vals, gens, free}, E.Remove{h}), h) == False{} : Bool}
596	
597	# Next (1614)
598	def Next.next_result(-T: Data, +tag: U32, +a: List<&2, Nat>, +b: List<&2, Nat>, +vals: List<&2, Maybe<&2, T>>, +gens: List<&2, U32>, +free: List<&2, Nat>, +h: E.Handle, +hv: {validate(T, DS{tag, C.append(Nat, a, Con{handle_id(h), b}), vals, gens, free}, h) == None{} : Maybe<&2, E.Error>}, +hn: {C.memn(handle_id(h), a) == False{} : Bool}) -> Type:
599	  {ob(T, DS{tag, C.append(Nat, a, Con{handle_id(h), b}), vals, gens, free}, E.Next{h}) == E.ONbr{Done{nbr(tag, gens, first(b))}} : E.Obs<T>}
600	
601	# Next (1614)
602	def Next.next_frame(-T: Data, +tag: U32, +a: List<&2, Nat>, +b: List<&2, Nat>, +vals: List<&2, Maybe<&2, T>>, +gens: List<&2, U32>, +free: List<&2, Nat>, +h: E.Handle, +hv: {validate(T, DS{tag, C.append(Nat, a, Con{handle_id(h), b}), vals, gens, free}, h) == None{} : Maybe<&2, E.Error>}) -> Type:
603	  {nx(T, DS{tag, C.append(Nat, a, Con{handle_id(h), b}), vals, gens, free}, E.Next{h}) == DS{tag, C.append(Nat, a, Con{handle_id(h), b}), vals, gens, free} : DS<T>}
604	
605	# Previous (1652)
606	def Previous.prev_result(-T: Data, +tag: U32, +a: List<&2, Nat>, +b: List<&2, Nat>, +vals: List<&2, Maybe<&2, T>>, +gens: List<&2, U32>, +free: List<&2, Nat>, +h: E.Handle, +hv: {validate(T, DS{tag, C.append(Nat, a, Con{handle_id(h), b}), vals, gens, free}, h) == None{} : Maybe<&2, E.Error>}, +hn: {C.memn(handle_id(h), a) == False{} : Bool}) -> Type:
607	  {ob(T, DS{tag, C.append(Nat, a, Con{handle_id(h), b}), vals, gens, free}, E.Prev{h}) == E.ONbr{Done{nbr(tag, gens, lastm(a, None{}))}} : E.Obs<T>}
608	
609	# Previous (1652)
610	def Previous.prev_first(-T: Data, +tag: U32, +b: List<&2, Nat>, +vals: List<&2, Maybe<&2, T>>, +gens: List<&2, U32>, +free: List<&2, Nat>, +h: E.Handle, +hv: {validate(T, DS{tag, Con{handle_id(h), b}, vals, gens, free}, h) == None{} : Maybe<&2, E.Error>}) -> Type:
611	  {ob(T, DS{tag, Con{handle_id(h), b}, vals, gens, free}, E.Prev{h}) == E.ONbr{Done{None{}}} : E.Obs<T>}
612	
613	# Previous (1652)
614	def Previous.prev_frame(-T: Data, +tag: U32, +a: List<&2, Nat>, +b: List<&2, Nat>, +vals: List<&2, Maybe<&2, T>>, +gens: List<&2, U32>, +free: List<&2, Nat>, +h: E.Handle, +hv: {validate(T, DS{tag, C.append(Nat, a, Con{handle_id(h), b}), vals, gens, free}, h) == None{} : Maybe<&2, E.Error>}) -> Type:
615	  {nx(T, DS{tag, C.append(Nat, a, Con{handle_id(h), b}), vals, gens, free}, E.Prev{h}) == DS{tag, C.append(Nat, a, Con{handle_id(h), b}), vals, gens, free} : DS<T>}