proofs/containers/doubly_linked_list/proof.bend
bend-collections-laws-containers@1.0.0.0 · 512 lines · 0 definitions
1import Base
2import bend-collections-laws-containers@1.0.0.0/spec/containers/doubly_linked_list.bend as S
3import bend-collections-laws-containers@1.0.0.0/src/containers/doubly_linked_list.bend as D
4import bend-collections-laws-containers@1.0.0.0/src/containers/types/doubly_linked_list.bend as E
5import bend-collections-laws-containers@1.0.0.0/proofs/containers/doubly_linked_list/state.bend as ST
6import bend-collections-laws-containers@1.0.0.0/proofs/containers/doubly_linked_list/ok.bend as OK
7import bend-collections-laws-containers@1.0.0.0/proofs/containers/doubly_linked_list/trace.bend as TR
8import bend-collections-laws-containers@1.0.0.0/proofs/containers/doubly_linked_list/api.bend as API
9import bend-collections-laws-containers@1.0.0.0/proofs/lib/logic.bend as L
10import bend-collections-laws-containers@1.0.0.0/proofs/lib/list.bend as LL
11import bend-collections-laws-containers@1.0.0.0/spec/lib/common.bend as SC
12import bend-collections-laws-containers@1.0.0.0/proofs/lib/nat.bend as N
13import bend-collections-laws-containers@1.0.0.0/proofs/lib/nat_list.bend as NL
14import bend-collections-laws-containers@1.0.0.0/spec/lib/sequence.bend as V
15import bend-collections-laws-containers@1.0.0.0/proofs/lib/sequence.bend as VL
16
17# Doubly linked list with generational handles
18# (src/containers/doubly_linked_list.bend over
19# src/containers/internal/dlist_storage.bend): public proof entry point.
20# shadow ST.Sh: the list's U32 fields and depth, a mirror tree for
21# each block (values, prev links, next links, generations),
22# and two ghost lists: the ids of the list in order and the
23# free stack; ST.real(sh) is the list
24# abstraction ST.model(sh): the order, the values and generations of the
25# issued ids, and the free stack, as a
26# proofs/spec/doubly_linked_list.bend list
27# invariant ST.good(sh): the blocks perfect at the depth, the capacity
28# 2^depth (depth < 30) and the counter within it; the order
29# linked both ways with its head and tail, live, below the
30# counter and without repeats; every live slot on the order;
31# the free stack chained through the next links, vacant and
32# without repeats; the generations of unissued ids 0
33# (proofs/doubly_linked_list/state.bend, generated by
34# tools/generators/dll_state.py)
35#
36# Proved for every shadow satisfying the invariant, every value type T
37# (Data), every handle (foreign, stale by capacity, generation, counter or
38# vacancy, or live) and every operation:
39# new a good shadow whose model is the specification's empty list
40# step every trace operation refines the specification's step
41# trace/run every trace refines the specification's run, so a new
42# list observes exactly what the specification does
43# get, set, remove, next, prev, insert_before, insert_after
44# the direct operation returns the projection of the
45# specification's step (and the new shadow is good)
46# push_front, push_back
47# the specification's push
48# length, to_list
49# the specification's length and values, list unchanged
50# Allocating operations (push, insert) assume fewer than 2^29 issued ids
51# before the operation (TR.room / TR.fits over the specification's state):
52# the blocks then stay below 2^30 slots, and links never wrap.
53
54def new_ok(~T: Data, +tag: U32) -> {ST.real(~T, TR.new_sh(T, tag)) == D.new(~T, tag) : D.DList<T>} & ({ST.model(~T, TR.new_sh(T, tag)) == S.empty(T, tag) : S.DS<T>} & {ST.good(~T, TR.new_sh(T, tag)) == True{} : Bool}):
55 TR.new_ok(~T, tag)
56
57def step_ok(~T: Data, +cz: Nat, +hcz: {cz == 29n : Nat}, +sh: ST.Sh<T>, +hg: {ST.good(~T, sh) == True{} : Bool}, +hr: {TR.room(T, ST.model(~T, sh), cz) == True{} : Bool}, +op: E.Op<T>) -> OK.POK(~T, E.Obs<T>, S.step(T, ST.model(~T, sh), op), D.step(~T, ST.real(~T, sh), op)):
58 TR.step_sh(~T, 1n, {==}, cz, hcz, sh, hg, hr, op)
59
60def trace_ok(~T: Data, +cz: Nat, +hcz: {cz == 29n : Nat}, +ops: List<&2, E.Op<T>>, +sh: ST.Sh<T>, +hg: {ST.good(~T, sh) == True{} : Bool}, +hf: {TR.fits(T, ops, ST.model(~T, sh), cz) == True{} : Bool}) -> TR.TraceOK(~T, ops, sh):
61 TR.trace_ok(~T, 1n, {==}, cz, hcz, ops, sh, hg, hf)
62
63def run_ok(~T: Data, +cz: Nat, +hcz: {cz == 29n : Nat}, +tag: U32, +ops: List<&2, E.Op<T>>, +hf: {TR.fits(T, ops, S.empty(T, tag), cz) == True{} : Bool}) -> {Pair.snd(D.DList<T>, List<&2, E.Obs<T>>, D.run(~T, ops, D.new(~T, tag))) == Pair.snd(S.DS<T>, List<&2, E.Obs<T>>, S.run(T, ops, S.empty(T, tag))) : List<&2, E.Obs<T>>}:
64 API.obs_eq(~T, ops, TR.new_sh(T, tag), TR.run_new(~T, 1n, {==}, cz, hcz, tag, ops, hf))
65
66def get_ok(~T: Data, +sh: ST.Sh<T>, +hg: {ST.good(~T, sh) == True{} : Bool}, +h: E.Handle) -> API.DOK(~T, Result<&2, &2, E.Error, T>, r => D.project_value(~T, r), D.get(~T, ST.real(~T, sh), h), S.step(T, ST.model(~T, sh), E.Get{h})):
67 API.get_ok(~T, 1n, {==}, sh, hg, h)
68
69def set_ok(~T: Data, +sh: ST.Sh<T>, +hg: {ST.good(~T, sh) == True{} : Bool}, +h: E.Handle, +x: T) -> API.DOK(~T, Result<&2, &2, E.Error, Unit>, r => D.project_unit(~T, r), D.set(~T, ST.real(~T, sh), h, x), S.step(T, ST.model(~T, sh), E.Set{h, x})):
70 API.set_ok(~T, 1n, {==}, sh, hg, h, x)
71
72def remove_ok(~T: Data, +sh: ST.Sh<T>, +hg: {ST.good(~T, sh) == True{} : Bool}, +h: E.Handle) -> API.DOK(~T, Result<&2, &2, E.Error, T>, r => D.project_value(~T, r), D.remove(~T, ST.real(~T, sh), h), S.step(T, ST.model(~T, sh), E.Remove{h})):
73 API.remove_ok(~T, 1n, {==}, sh, hg, h)
74
75def next_ok(~T: Data, +sh: ST.Sh<T>, +hg: {ST.good(~T, sh) == True{} : Bool}, +h: E.Handle) -> API.DOK(~T, Result<&2, &2, E.Error, Maybe<&2, E.Handle>>, r => D.project_neighbour(~T, r), D.next(~T, ST.real(~T, sh), h), S.step(T, ST.model(~T, sh), E.Next{h})):
76 API.next_ok(~T, 1n, {==}, sh, hg, h)
77
78def prev_ok(~T: Data, +sh: ST.Sh<T>, +hg: {ST.good(~T, sh) == True{} : Bool}, +h: E.Handle) -> API.DOK(~T, Result<&2, &2, E.Error, Maybe<&2, E.Handle>>, r => D.project_neighbour(~T, r), D.prev(~T, ST.real(~T, sh), h), S.step(T, ST.model(~T, sh), E.Prev{h})):
79 API.prev_ok(~T, 1n, {==}, sh, hg, h)
80
81def insert_before_ok(~T: Data, +cz: Nat, +hcz: {cz == 29n : Nat}, +sh: ST.Sh<T>, +hg: {ST.good(~T, sh) == True{} : Bool}, +hr: {TR.room(T, ST.model(~T, sh), cz) == True{} : Bool}, +h: E.Handle, +x: T) -> API.DOK(~T, Result<&2, &2, E.Error, E.Handle>, r => D.project_insert(~T, r), D.insert_before(~T, ST.real(~T, sh), h, x), S.step(T, ST.model(~T, sh), E.InsertBefore{h, x})):
82 API.before_ok(~T, 1n, {==}, cz, hcz, sh, hg, hr, h, x)
83
84def insert_after_ok(~T: Data, +cz: Nat, +hcz: {cz == 29n : Nat}, +sh: ST.Sh<T>, +hg: {ST.good(~T, sh) == True{} : Bool}, +hr: {TR.room(T, ST.model(~T, sh), cz) == True{} : Bool}, +h: E.Handle, +x: T) -> API.DOK(~T, Result<&2, &2, E.Error, E.Handle>, r => D.project_insert(~T, r), D.insert_after(~T, ST.real(~T, sh), h, x), S.step(T, ST.model(~T, sh), E.InsertAfter{h, x})):
85 API.after_ok(~T, 1n, {==}, cz, hcz, sh, hg, hr, h, x)
86
87def push_front_ok(~T: Data, +cz: Nat, +hcz: {cz == 29n : Nat}, +sh: ST.Sh<T>, +hg: {ST.good(~T, sh) == True{} : Bool}, +hr: {TR.room(T, ST.model(~T, sh), cz) == True{} : Bool}, +x: T) -> OK.POK(~T, E.Handle, S.push_front(T, ST.model(~T, sh), x), D.push_front(~T, ST.real(~T, sh), x)):
88 API.front_ok(~T, 1n, {==}, cz, hcz, sh, hg, hr, x)
89
90def push_back_ok(~T: Data, +cz: Nat, +hcz: {cz == 29n : Nat}, +sh: ST.Sh<T>, +hg: {ST.good(~T, sh) == True{} : Bool}, +hr: {TR.room(T, ST.model(~T, sh), cz) == True{} : Bool}, +x: T) -> OK.POK(~T, E.Handle, S.push_back(T, ST.model(~T, sh), x), D.push_back(~T, ST.real(~T, sh), x)):
91 API.back_ok(~T, 1n, {==}, cz, hcz, sh, hg, hr, x)
92
93def length_ok(~T: Data, +sh: ST.Sh<T>) -> {D.length(~T, ST.real(~T, sh)) == (ST.real(~T, sh), S.len_of(T, ST.model(~T, sh))) : D.DList<T> & Nat}:
94 API.length_ok(~T, sh)
95
96def to_list_ok(~T: Data, +sh: ST.Sh<T>, +hg: {ST.good(~T, sh) == True{} : Bool}) -> {D.to_list(~T, ST.real(~T, sh)) == (ST.real(~T, sh), S.list_of(T, ST.model(~T, sh))) : D.DList<T> & List<&2, T>}:
97 API.to_list_ok(~T, 1n, {==}, sh, hg)
98
99# ==== the contract of doubly_linked_list (stated in spec/containers/doubly_linked_list.bend) ====================
100
101# ---- the implementation ----
102def Impl(~T: Data, sh: ST.Sh<T>, op: E.Op<T>, Post: (S.DS<T> & E.Obs<T>) -> Type) -> Type:
103 Sigma<&1, &1, ST.Sh<T>, sh2 => Sigma<&1, &1, E.Obs<T>, o => {D.step(~T, ST.real(~T, sh), op) == (ST.real(~T, sh2), o) : D.DList<T> & E.Obs<T>} & ({ST.good(~T, sh2) == True{} : Bool} & Post((ST.model(~T, sh2), o)))>>
104
105def impl_of(~T: Data, -sh: ST.Sh<T>, -op: E.Op<T>, -Post: (S.DS<T> & E.Obs<T>) -> Type, k: OK.POK(~T, E.Obs<T>, S.step(T, ST.model(~T, sh), op), D.step(~T, ST.real(~T, sh), op)), pf: Post(S.step(T, ST.model(~T, sh), op))) -> Impl(~T, sh, op, Post):
106 match k:
107 case Tuple{sh2, Tuple{o, Tuple{er, Tuple{es, g2}}}}:
108 (sh2, (o, (er, (g2, L.subst(S.DS<T> & E.Obs<T>, Post, S.step(T, ST.model(~T, sh), op), (ST.model(~T, sh2), o), es, pf)))))
109
110# a good list with room for one more element (TR.room, 2^29 ids)
111def impl(~T: Data, +cz: Nat, +hcz: {cz == 29n : Nat}, +sh: ST.Sh<T>, +hg: {ST.good(~T, sh) == True{} : Bool}, +hr: {TR.room(T, ST.model(~T, sh), cz) == True{} : Bool}, +op: E.Op<T>, -Post: (S.DS<T> & E.Obs<T>) -> Type, pf: Post(S.step(T, ST.model(~T, sh), op))) -> Impl(~T, sh, op, Post):
112 impl_of(~T, sh, op, Post, step_ok(~T, cz, hcz, sh, hg, hr, op), pf)
113
114def fs_up(+x: Nat, +i: Nat, +t: List<&2, Nat>, +hx: {Nat.is_eq(x, i) == False{} : Bool}, r: S.FSplit(i, t)) -> S.FSplit(i, Con{x, t}):
115 match r:
116 case Tuple{+a, Tuple{+b, Tuple{e, +hn}}}:
117 (Con{x, a}, (b, (LL.cons_cong(Nat, x, t, SC.append(Nat, a, Con{i, b}), e), L.subst(Bool, z => {Bool.or(z, SC.memn(i, a)) == False{} : Bool}, False{}, Nat.is_eq(x, i), Equal.sym(Bool, Nat.is_eq(x, i), False{}, hx), hn))))
118
119def fs_c(+x: Nat, +i: Nat, +t: List<&2, Nat>, +c: Bool, +hc: {Nat.is_eq(x, i) == c : Bool}, +hm: {Bool.or(c, SC.memn(i, t)) == True{} : Bool}, rec: @h: {SC.memn(i, t) == True{} : Bool} -> S.FSplit(i, t)) -> S.FSplit(i, Con{x, t}):
120 match c:
121 case True{}:
122 (Nil{}, (t, (Equal.cong(Nat, List<&2, Nat>, z => Con{z, t}, x, i, N.eq_from_is_eq(x, i, hc)), {==})))
123 case False{}:
124 fs_up(x, i, t, hc, rec(hm))
125
126def fsplit(+i: Nat, +xs: List<&2, Nat>, +hm: {SC.memn(i, xs) == True{} : Bool}) -> S.FSplit(i, xs):
127 match xs:
128 case Nil{}:
129 Empty.absurd(S.FSplit(i, Nil{}), L.false_true(hm))
130 case Con{+x, +t}:
131 fs_c(x, i, t, Nat.is_eq(x, i), {==}, hm, h => fsplit(i, t, h))
132
133# ---- the order operations on a split order ----
134def ib_app(+a: List<&2, Nat>, +i: Nat, +b: List<&2, Nat>, +n: Nat, +hn: {SC.memn(i, a) == False{} : Bool}) -> {S.ins_before(SC.append(Nat, a, Con{i, b}), i, n) == SC.append(Nat, a, Con{n, Con{i, b}}) : List<&2, Nat>}:
135 match a:
136 case Nil{}:
137 %Equal.sym(Bool, Nat.is_eq(i, i), True{}, N.is_eq_refl(i)) : {S.pick_list(_, Con{n, Con{i, b}}, Con{i, S.ins_before(b, i, n)}) == Con{n, Con{i, b}} : List<&2, Nat>}
138 {==}
139 case Con{+x, +t}:
140 %Equal.sym(Bool, Nat.is_eq(x, i), False{}, NL.or_ff_l(Nat.is_eq(x, i), SC.memn(i, t), hn)) : {S.pick_list(_, Con{n, Con{x, SC.append(Nat, t, Con{i, b})}}, Con{x, S.ins_before(SC.append(Nat, t, Con{i, b}), i, n)}) == Con{x, SC.append(Nat, t, Con{n, Con{i, b}})} : List<&2, Nat>}
141 LL.cons_cong(Nat, x, S.ins_before(SC.append(Nat, t, Con{i, b}), i, n), SC.append(Nat, t, Con{n, Con{i, b}}), ib_app(t, i, b, n, NL.or_ff_r(Nat.is_eq(x, i), SC.memn(i, t), hn)))
142
143def ia_app(+a: List<&2, Nat>, +i: Nat, +b: List<&2, Nat>, +n: Nat, +hn: {SC.memn(i, a) == False{} : Bool}) -> {S.ins_after(SC.append(Nat, a, Con{i, b}), i, n) == SC.append(Nat, a, Con{i, Con{n, b}}) : List<&2, Nat>}:
144 match a:
145 case Nil{}:
146 %Equal.sym(Bool, Nat.is_eq(i, i), True{}, N.is_eq_refl(i)) : {S.pick_list(_, Con{i, Con{n, b}}, Con{i, S.ins_after(b, i, n)}) == Con{i, Con{n, b}} : List<&2, Nat>}
147 {==}
148 case Con{+x, +t}:
149 %Equal.sym(Bool, Nat.is_eq(x, i), False{}, NL.or_ff_l(Nat.is_eq(x, i), SC.memn(i, t), hn)) : {S.pick_list(_, Con{x, Con{n, SC.append(Nat, t, Con{i, b})}}, Con{x, S.ins_after(SC.append(Nat, t, Con{i, b}), i, n)}) == Con{x, SC.append(Nat, t, Con{i, Con{n, b}})} : List<&2, Nat>}
150 LL.cons_cong(Nat, x, S.ins_after(SC.append(Nat, t, Con{i, b}), i, n), SC.append(Nat, t, Con{i, Con{n, b}}), ia_app(t, i, b, n, NL.or_ff_r(Nat.is_eq(x, i), SC.memn(i, t), hn)))
151
152def del_app(+a: List<&2, Nat>, +i: Nat, +b: List<&2, Nat>, +hn: {SC.memn(i, a) == False{} : Bool}) -> {S.delete(SC.append(Nat, a, Con{i, b}), i) == SC.append(Nat, a, b) : List<&2, Nat>}:
153 match a:
154 case Nil{}:
155 %Equal.sym(Bool, Nat.is_eq(i, i), True{}, N.is_eq_refl(i)) : {S.pick_list(_, b, Con{i, S.delete(b, i)}) == b : List<&2, Nat>}
156 {==}
157 case Con{+x, +t}:
158 %Equal.sym(Bool, Nat.is_eq(x, i), False{}, NL.or_ff_l(Nat.is_eq(x, i), SC.memn(i, t), hn)) : {S.pick_list(_, SC.append(Nat, t, Con{i, b}), Con{x, S.delete(SC.append(Nat, t, Con{i, b}), i)}) == Con{x, SC.append(Nat, t, b)} : List<&2, Nat>}
159 LL.cons_cong(Nat, x, S.delete(SC.append(Nat, t, Con{i, b}), i), SC.append(Nat, t, b), del_app(t, i, b, NL.or_ff_r(Nat.is_eq(x, i), SC.memn(i, t), hn)))
160
161def after_app(+a: List<&2, Nat>, +i: Nat, +b: List<&2, Nat>, +hn: {SC.memn(i, a) == False{} : Bool}) -> {S.after(SC.append(Nat, a, Con{i, b}), i) == S.first(b) : Maybe<&2, Nat>}:
162 match a:
163 case Nil{}:
164 %Equal.sym(Bool, Nat.is_eq(i, i), True{}, N.is_eq_refl(i)) : {S.pick_maybe(_, S.first(b), S.after(b, i)) == S.first(b) : Maybe<&2, Nat>}
165 {==}
166 case Con{+x, +t}:
167 %Equal.sym(Bool, Nat.is_eq(x, i), False{}, NL.or_ff_l(Nat.is_eq(x, i), SC.memn(i, t), hn)) : {S.pick_maybe(_, S.first(SC.append(Nat, t, Con{i, b})), S.after(SC.append(Nat, t, Con{i, b}), i)) == S.first(b) : Maybe<&2, Nat>}
168 after_app(t, i, b, NL.or_ff_r(Nat.is_eq(x, i), SC.memn(i, t), hn))
169
170def before_app(+a: List<&2, Nat>, +i: Nat, +b: List<&2, Nat>, +p: Maybe<&2, Nat>, +hn: {SC.memn(i, a) == False{} : Bool}) -> {S.before(SC.append(Nat, a, Con{i, b}), i, p) == S.lastm(a, p) : Maybe<&2, Nat>}:
171 match a:
172 case Nil{}:
173 %Equal.sym(Bool, Nat.is_eq(i, i), True{}, N.is_eq_refl(i)) : {S.pick_maybe(_, p, S.before(b, i, Some{i})) == p : Maybe<&2, Nat>}
174 {==}
175 case Con{+x, +t}:
176 %Equal.sym(Bool, Nat.is_eq(x, i), False{}, NL.or_ff_l(Nat.is_eq(x, i), SC.memn(i, t), hn)) : {S.pick_maybe(_, p, S.before(SC.append(Nat, t, Con{i, b}), i, Some{x})) == S.lastm(t, Some{x}) : Maybe<&2, Nat>}
177 before_app(t, i, b, Some{x}, NL.or_ff_r(Nat.is_eq(x, i), SC.memn(i, t), hn))
178
179# Next is the element at Position + 1
180def next_position(+a: List<&2, Nat>, +i: Nat, +b: List<&2, Nat>) -> S.Next.next_position(a, i, b):
181 match a:
182 case Nil{}:
183 match b:
184 case Nil{}:
185 {==}
186 case Con{y, r}:
187 {==}
188 case Con{+x, +t}:
189 next_position(t, i, b)
190
191# Previous is the element at Position - 1 (none at the first position)
192def prev_position(+t: List<&2, Nat>, +x: Nat, +i: Nat, +b: List<&2, Nat>, +p: Maybe<&2, Nat>) -> S.Previous.prev_position(t, x, i, b, p):
193 match t:
194 case Nil{}:
195 {==}
196 case Con{+y, +r}:
197 prev_position(r, y, i, b, Some{x})
198
199# ---- values by id ----
200def val_update_same(-T: Data, +vs: List<&2, Maybe<&2, T>>, +i: Nat, +m: Maybe<&2, T>, +h: {Nat.is_lt(i, SC.length(Maybe<&2, T>, vs)) == True{} : Bool}) -> {S.val_of(T, SC.update(Maybe<&2, T>, vs, i, m), i) == m : Maybe<&2, T>}:
201 match vs i:
202 case Nil{} _:
203 Empty.absurd({S.val_of(T, SC.update(Maybe<&2, T>, Nil{}, i, m), i) == m : Maybe<&2, T>}, N.lt_zero_absurd(i, h))
204 case Con{v, t} 0n:
205 {==}
206 case Con{v, +t} 1n+ +p:
207 val_update_same(T, t, p, m, h)
208
209def val_update_other(-T: Data, +vs: List<&2, Maybe<&2, T>>, +i: Nat, +j: Nat, +m: Maybe<&2, T>, +ne: {Nat.is_eq(i, j) == False{} : Bool}) -> {S.val_of(T, SC.update(Maybe<&2, T>, vs, i, m), j) == S.val_of(T, vs, j) : Maybe<&2, T>}:
210 match vs i j:
211 case Nil{} _ _:
212 {==}
213 case Con{v, t} 0n 0n:
214 Empty.absurd({S.val_of(T, SC.update(Maybe<&2, T>, Con{v, t}, 0n, m), 0n) == S.val_of(T, Con{v, t}, 0n) : Maybe<&2, T>}, L.true_false(ne))
215 case Con{v, t} 0n 1n+q:
216 {==}
217 case Con{v, t} 1n+p 0n:
218 {==}
219 case Con{v, +t} 1n+ +p 1n+ +q:
220 val_update_other(T, t, p, q, m, ne)
221
222def val_lt(-T: Data, +vs: List<&2, Maybe<&2, T>>, +i: Nat, +v: T, +h: {S.val_of(T, vs, i) == Some{v} : Maybe<&2, T>}) -> {Nat.is_lt(i, SC.length(Maybe<&2, T>, vs)) == True{} : Bool}:
223 match vs i:
224 case Nil{} _:
225 Empty.absurd({Nat.is_lt(i, 0n) == True{} : Bool}, L.none_some(T, v, h))
226 case Con{w, t} 0n:
227 {==}
228 case Con{w, +t} 1n+ +p:
229 val_lt(T, t, p, v, h)
230
231# a valid handle names a live element (Has_Element => Element is defined)
232def vl_m(-T: Data, +m: Maybe<&2, T>, +same: Bool, +hv: {S.live_gen(T, m, same) == None{} : Maybe<&2, E.Error>}) -> Sigma<&1, &1, T, v => {m == Some{v} : Maybe<&2, T>}>:
233 match m same:
234 case None{} _:
235 Empty.absurd(Sigma<&1, &1, T, v => {None{} == Some{v} : Maybe<&2, T>}>, L.none_some(E.Error, E.StaleHandle{}, Equal.sym(Maybe<&2, E.Error>, Some{E.StaleHandle{}}, None{}, hv)))
236 case Some{+v} True{}:
237 (v, {==})
238 case Some{v} False{}:
239 Empty.absurd(Sigma<&1, &1, T, w => {Some{v} == Some{w} : Maybe<&2, T>}>, L.none_some(E.Error, E.StaleHandle{}, Equal.sym(Maybe<&2, E.Error>, Some{E.StaleHandle{}}, None{}, hv)))
240
241def vl_own(-T: Data, +vals: List<&2, Maybe<&2, T>>, +gens: List<&2, U32>, +i: Nat, +g: U32, +mine: Bool, +hv: {S.valid_own(T, vals, gens, i, g, mine) == None{} : Maybe<&2, E.Error>}) -> Sigma<&1, &1, T, v => {S.val_of(T, vals, i) == Some{v} : Maybe<&2, T>}>:
242 match mine:
243 case False{}:
244 Empty.absurd(Sigma<&1, &1, T, v => {S.val_of(T, vals, i) == Some{v} : Maybe<&2, T>}>, L.none_some(E.Error, E.ForeignHandle{}, Equal.sym(Maybe<&2, E.Error>, Some{E.ForeignHandle{}}, None{}, hv)))
245 case True{}:
246 vl_m(T, S.val_of(T, vals, i), U32.is_eq(S.gen_of(gens, i), g), hv)
247
248def 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: {S.validate(T, S.DS{tag, order, vals, gens, free}, h) == None{} : Maybe<&2, E.Error>}) -> S.Has_Element.valid_live(T, tag, order, vals, gens, free, h, hv):
249 match h:
250 case E.H{+owner, +id, +g}:
251 vl_own(T, vals, gens, U32.to_nat(id), g, U32.is_eq(owner, tag), hv)
252
253# ---- the step on a valid handle is the live operation ----
254def live(-T: Data, +s: S.DS<T>, +op: E.Op<T>, +h: E.Handle, +hv: {S.validate(T, s, h) == None{} : Maybe<&2, E.Error>}) -> {S.checked(T, s, op, h, S.validate(T, s, h)) == S.live_op(T, s, op, S.handle_id(h)) : S.DS<T> & E.Obs<T>}:
255 %Equal.sym(Maybe<&2, E.Error>, S.validate(T, s, h), None{}, hv) : {S.checked(T, s, op, h, _) == S.live_op(T, s, op, S.handle_id(h)) : S.DS<T> & E.Obs<T>}
256 {==}
257
258# ---- Length, iteration, Empty_List ----
259def length_result(-T: Data, +s: S.DS<T>) -> S.Length.length_result(T, s):
260 {==}
261
262def length_frame(-T: Data, +s: S.DS<T>) -> S.Length.length_frame(T, s):
263 {==}
264
265def to_list_model(-T: Data, +s: S.DS<T>) -> S.Iteration.to_list_model(T, s):
266 {==}
267
268def to_list_frame(-T: Data, +s: S.DS<T>) -> S.Iteration.to_list_frame(T, s):
269 {==}
270
271def new_empty(-T: Data, +tag: U32) -> S.Empty_List.new_empty(T, tag):
272 {==}
273
274# ---- Element: the value of the handle's element; nothing changes ----
275def get_step(-T: Data, +s: S.DS<T>, +h: E.Handle, +hv: {S.validate(T, s, h) == None{} : Maybe<&2, E.Error>}) -> {S.step(T, s, E.Get{h}) == S.get_live(T, s, S.handle_id(h)) : S.DS<T> & E.Obs<T>}:
276 live(T, s, E.Get{h}, h, hv)
277
278def 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: {S.validate(T, S.DS{tag, order, vals, gens, free}, h) == None{} : Maybe<&2, E.Error>}) -> S.Element.get_frame(T, tag, order, vals, gens, free, h, hv):
279 %Equal.sym(S.DS<T> & E.Obs<T>, S.step(T, S.DS{tag, order, vals, gens, free}, E.Get{h}), S.get_live(T, S.DS{tag, order, vals, gens, free}, S.handle_id(h)), get_step(T, S.DS{tag, order, vals, gens, free}, h, hv)) : {Pair.fst(S.DS<T>, E.Obs<T>, _) == S.DS{tag, order, vals, gens, free} : S.DS<T>}
280 {==}
281
282def 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: {S.validate(T, S.DS{tag, order, vals, gens, free}, h) == None{} : Maybe<&2, E.Error>}, +v: T, +hval: {S.val_of(T, vals, S.handle_id(h)) == Some{v} : Maybe<&2, T>}) -> S.Element.get_element(T, tag, order, vals, gens, free, h, hv, v, hval):
283 %Equal.sym(S.DS<T> & E.Obs<T>, S.step(T, S.DS{tag, order, vals, gens, free}, E.Get{h}), S.get_live(T, S.DS{tag, order, vals, gens, free}, S.handle_id(h)), get_step(T, S.DS{tag, order, vals, gens, free}, h, hv)) : {Pair.snd(S.DS<T>, E.Obs<T>, _) == E.OVal{Done{v}} : E.Obs<T>}
284 %Equal.sym(Maybe<&2, T>, S.val_of(T, vals, S.handle_id(h)), Some{v}, hval) : {E.OVal{S.maybe_done(T, E.StaleHandle{}, _)} == E.OVal{Done{v}} : E.Obs<T>}
285 {==}
286
287# ---- Replace_Element: positions and generations kept, the handle's value is x, others kept ----
288def set_step(-T: Data, +s: S.DS<T>, +h: E.Handle, +x: T, +hv: {S.validate(T, s, h) == None{} : Maybe<&2, E.Error>}) -> {S.step(T, s, E.Set{h, x}) == S.set_live(T, s, S.handle_id(h), x) : S.DS<T> & E.Obs<T>}:
289 live(T, s, E.Set{h, x}, h, hv)
290
291def set_is(-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: {S.validate(T, S.DS{tag, order, vals, gens, free}, h) == None{} : Maybe<&2, E.Error>}) -> {S.nx(T, S.DS{tag, order, vals, gens, free}, E.Set{h, x}) == S.DS{tag, order, SC.update(Maybe<&2, T>, vals, S.handle_id(h), Some{x}), gens, free} : S.DS<T>}:
292 %Equal.sym(S.DS<T> & E.Obs<T>, S.step(T, S.DS{tag, order, vals, gens, free}, E.Set{h, x}), S.set_live(T, S.DS{tag, order, vals, gens, free}, S.handle_id(h), x), set_step(T, S.DS{tag, order, vals, gens, free}, h, x, hv)) : {Pair.fst(S.DS<T>, E.Obs<T>, _) == S.DS{tag, order, SC.update(Maybe<&2, T>, vals, S.handle_id(h), Some{x}), gens, free} : S.DS<T>}
293 {==}
294
295def 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: {S.validate(T, S.DS{tag, order, vals, gens, free}, h) == None{} : Maybe<&2, E.Error>}) -> S.Replace_Element.set_positions(T, tag, order, vals, gens, free, h, x, hv):
296 %Equal.sym(S.DS<T>, S.nx(T, S.DS{tag, order, vals, gens, free}, E.Set{h, x}), S.DS{tag, order, SC.update(Maybe<&2, T>, vals, S.handle_id(h), Some{x}), gens, free}, set_is(T, tag, order, vals, gens, free, h, x, hv)) : {S.ord(T, _) == order : List<&2, Nat>}
297 {==}
298
299def 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: {S.validate(T, S.DS{tag, order, vals, gens, free}, h) == None{} : Maybe<&2, E.Error>}) -> S.Replace_Element.set_gens(T, tag, order, vals, gens, free, h, x, hv):
300 %Equal.sym(S.DS<T>, S.nx(T, S.DS{tag, order, vals, gens, free}, E.Set{h, x}), S.DS{tag, order, SC.update(Maybe<&2, T>, vals, S.handle_id(h), Some{x}), gens, free}, set_is(T, tag, order, vals, gens, free, h, x, hv)) : {S.gns(T, _) == gens : List<&2, U32>}
301 {==}
302
303def 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: {S.validate(T, S.DS{tag, order, vals, gens, free}, h) == None{} : Maybe<&2, E.Error>}, +v: T, +hval: {S.val_of(T, vals, S.handle_id(h)) == Some{v} : Maybe<&2, T>}) -> S.Replace_Element.set_element(T, tag, order, vals, gens, free, h, x, hv, v, hval):
304 %Equal.sym(S.DS<T>, S.nx(T, S.DS{tag, order, vals, gens, free}, E.Set{h, x}), S.DS{tag, order, SC.update(Maybe<&2, T>, vals, S.handle_id(h), Some{x}), gens, free}, set_is(T, tag, order, vals, gens, free, h, x, hv)) : {S.val_of(T, S.vls(T, _), S.handle_id(h)) == Some{x} : Maybe<&2, T>}
305 val_update_same(T, vals, S.handle_id(h), Some{x}, val_lt(T, vals, S.handle_id(h), v, hval))
306
307def 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: {S.validate(T, S.DS{tag, order, vals, gens, free}, h) == None{} : Maybe<&2, E.Error>}, +j: Nat, +ne: {Nat.is_eq(S.handle_id(h), j) == False{} : Bool}) -> S.Replace_Element.set_others(T, tag, order, vals, gens, free, h, x, hv, j, ne):
308 %Equal.sym(S.DS<T>, S.nx(T, S.DS{tag, order, vals, gens, free}, E.Set{h, x}), S.DS{tag, order, SC.update(Maybe<&2, T>, vals, S.handle_id(h), Some{x}), gens, free}, set_is(T, tag, order, vals, gens, free, h, x, hv)) : {S.val_of(T, S.vls(T, _), j) == S.val_of(T, vals, j) : Maybe<&2, T>}
309 val_update_other(T, vals, S.handle_id(h), j, Some{x}, ne)
310
311# ---- inserting: the order gains the new id n at its place ----
312def alloc_order(-T: Data, +tag: U32, +order: List<&2, Nat>, +vals: List<&2, Maybe<&2, T>>, +gens: List<&2, U32>, +free: List<&2, Nat>, +x: T, +pos: S.Pos) -> {S.ord(T, Pair.fst(S.DS<T>, E.Handle, S.inserted(T, S.alloc(T, S.DS{tag, order, vals, gens, free}), x, pos))) == S.place_order(pos, order, Pair.snd(S.DS<T>, Nat, S.alloc(T, S.DS{tag, order, vals, gens, free}))) : List<&2, Nat>}:
313 match free:
314 case Nil{}:
315 {==}
316 case Con{+i, +rest}:
317 {==}
318
319def push_front_order(-T: Data, +tag: U32, +order: List<&2, Nat>, +vals: List<&2, Maybe<&2, T>>, +gens: List<&2, U32>, +free: List<&2, Nat>, +x: T) -> {S.ord(T, S.nx(T, S.DS{tag, order, vals, gens, free}, E.PushFront{x})) == Con{Pair.snd(S.DS<T>, Nat, S.alloc(T, S.DS{tag, order, vals, gens, free})), order} : List<&2, Nat>}:
320 match free:
321 case Nil{}:
322 {==}
323 case Con{+i, +rest}:
324 {==}
325
326def 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) -> S.Prepend.push_front_positions(T, tag, order, vals, gens, free, x):
327 L.subst(List<&2, Nat>, z => V.RangeShifted(Nat, order, z, 0n, SC.length(Nat, order), 1n), Con{Pair.snd(S.DS<T>, Nat, S.alloc(T, S.DS{tag, order, vals, gens, free})), order}, S.ord(T, S.nx(T, S.DS{tag, order, vals, gens, free}, E.PushFront{x})), Equal.sym(List<&2, Nat>, S.ord(T, S.nx(T, S.DS{tag, order, vals, gens, free}, E.PushFront{x})), Con{Pair.snd(S.DS<T>, Nat, S.alloc(T, S.DS{tag, order, vals, gens, free})), order}, push_front_order(T, tag, order, vals, gens, free, x)), VL.cons_shifted(Nat, order, Pair.snd(S.DS<T>, Nat, S.alloc(T, S.DS{tag, order, vals, gens, free}))))
328
329def 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) -> S.Prepend.push_front_first(T, tag, order, vals, gens, free, x):
330 %Equal.sym(List<&2, Nat>, S.ord(T, S.nx(T, S.DS{tag, order, vals, gens, free}, E.PushFront{x})), Con{Pair.snd(S.DS<T>, Nat, S.alloc(T, S.DS{tag, order, vals, gens, free})), order}, push_front_order(T, tag, order, vals, gens, free, x)) : {SC.nth(Nat, _, 0n) == Some{Pair.snd(S.DS<T>, Nat, S.alloc(T, S.DS{tag, order, vals, gens, free}))} : Maybe<&2, Nat>}
331 {==}
332
333def 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) -> S.Prepend.push_front_length(T, tag, order, vals, gens, free, x):
334 %Equal.sym(List<&2, Nat>, S.ord(T, S.nx(T, S.DS{tag, order, vals, gens, free}, E.PushFront{x})), Con{Pair.snd(S.DS<T>, Nat, S.alloc(T, S.DS{tag, order, vals, gens, free})), order}, push_front_order(T, tag, order, vals, gens, free, x)) : {SC.length(Nat, _) == 1n+SC.length(Nat, order) : Nat}
335 {==}
336
337def push_back_order(-T: Data, +tag: U32, +order: List<&2, Nat>, +vals: List<&2, Maybe<&2, T>>, +gens: List<&2, U32>, +free: List<&2, Nat>, +x: T) -> {S.ord(T, S.nx(T, S.DS{tag, order, vals, gens, free}, E.PushBack{x})) == SC.snoc(Nat, order, Pair.snd(S.DS<T>, Nat, S.alloc(T, S.DS{tag, order, vals, gens, free}))) : List<&2, Nat>}:
338 match free:
339 case Nil{}:
340 {==}
341 case Con{+i, +rest}:
342 {==}
343
344def 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) -> S.Append.push_back_positions(T, tag, order, vals, gens, free, x):
345 L.subst(List<&2, Nat>, z => V.EqualPrefix(Nat, order, z), SC.snoc(Nat, order, Pair.snd(S.DS<T>, Nat, S.alloc(T, S.DS{tag, order, vals, gens, free}))), S.ord(T, S.nx(T, S.DS{tag, order, vals, gens, free}, E.PushBack{x})), Equal.sym(List<&2, Nat>, S.ord(T, S.nx(T, S.DS{tag, order, vals, gens, free}, E.PushBack{x})), SC.snoc(Nat, order, Pair.snd(S.DS<T>, Nat, S.alloc(T, S.DS{tag, order, vals, gens, free}))), push_back_order(T, tag, order, vals, gens, free, x)), VL.snoc_prefix(Nat, order, Pair.snd(S.DS<T>, Nat, S.alloc(T, S.DS{tag, order, vals, gens, free}))))
346
347def 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) -> S.Append.push_back_last(T, tag, order, vals, gens, free, x):
348 %Equal.sym(List<&2, Nat>, S.ord(T, S.nx(T, S.DS{tag, order, vals, gens, free}, E.PushBack{x})), SC.snoc(Nat, order, Pair.snd(S.DS<T>, Nat, S.alloc(T, S.DS{tag, order, vals, gens, free}))), push_back_order(T, tag, order, vals, gens, free, x)) : {SC.nth(Nat, _, SC.length(Nat, order)) == Some{Pair.snd(S.DS<T>, Nat, S.alloc(T, S.DS{tag, order, vals, gens, free}))} : Maybe<&2, Nat>}
349 VL.snoc_last(Nat, order, Pair.snd(S.DS<T>, Nat, S.alloc(T, S.DS{tag, order, vals, gens, free})))
350
351def 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) -> S.Append.push_back_length(T, tag, order, vals, gens, free, x):
352 %Equal.sym(List<&2, Nat>, S.ord(T, S.nx(T, S.DS{tag, order, vals, gens, free}, E.PushBack{x})), SC.snoc(Nat, order, Pair.snd(S.DS<T>, Nat, S.alloc(T, S.DS{tag, order, vals, gens, free}))), push_back_order(T, tag, order, vals, gens, free, x)) : {SC.length(Nat, _) == 1n+SC.length(Nat, order) : Nat}
353 VL.snoc_length(Nat, order, Pair.snd(S.DS<T>, Nat, S.alloc(T, S.DS{tag, order, vals, gens, free})))
354
355# ---- Insert (Before) ----
356def ib_free(-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, +hn: {SC.memn(S.handle_id(h), a) == False{} : Bool}) -> {S.ord(T, Pair.fst(S.DS<T>, E.Obs<T>, S.live_op(T, S.DS{tag, SC.append(Nat, a, Con{S.handle_id(h), b}), vals, gens, free}, E.InsertBefore{h, x}, S.handle_id(h)))) == SC.append(Nat, a, Con{Pair.snd(S.DS<T>, Nat, S.alloc(T, S.DS{tag, SC.append(Nat, a, Con{S.handle_id(h), b}), vals, gens, free})), Con{S.handle_id(h), b}}) : List<&2, Nat>}:
357 match free:
358 case Nil{}:
359 ib_app(a, S.handle_id(h), b, SC.length(Maybe<&2, T>, vals), hn)
360 case Con{+i, +rest}:
361 ib_app(a, S.handle_id(h), b, i, hn)
362
363def insert_before_order(-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: {S.validate(T, S.DS{tag, SC.append(Nat, a, Con{S.handle_id(h), b}), vals, gens, free}, h) == None{} : Maybe<&2, E.Error>}, +hn: {SC.memn(S.handle_id(h), a) == False{} : Bool}) -> {S.ord(T, S.nx(T, S.DS{tag, SC.append(Nat, a, Con{S.handle_id(h), b}), vals, gens, free}, E.InsertBefore{h, x})) == SC.append(Nat, a, Con{Pair.snd(S.DS<T>, Nat, S.alloc(T, S.DS{tag, SC.append(Nat, a, Con{S.handle_id(h), b}), vals, gens, free})), Con{S.handle_id(h), b}}) : List<&2, Nat>}:
364 %Equal.sym(S.DS<T> & E.Obs<T>, S.checked(T, S.DS{tag, SC.append(Nat, a, Con{S.handle_id(h), b}), vals, gens, free}, E.InsertBefore{h, x}, h, S.validate(T, S.DS{tag, SC.append(Nat, a, Con{S.handle_id(h), b}), vals, gens, free}, h)), S.live_op(T, S.DS{tag, SC.append(Nat, a, Con{S.handle_id(h), b}), vals, gens, free}, E.InsertBefore{h, x}, S.handle_id(h)), live(T, S.DS{tag, SC.append(Nat, a, Con{S.handle_id(h), b}), vals, gens, free}, E.InsertBefore{h, x}, h, hv)) : {S.ord(T, Pair.fst(S.DS<T>, E.Obs<T>, _)) == SC.append(Nat, a, Con{Pair.snd(S.DS<T>, Nat, S.alloc(T, S.DS{tag, SC.append(Nat, a, Con{S.handle_id(h), b}), vals, gens, free})), Con{S.handle_id(h), b}}) : List<&2, Nat>}
365 ib_free(T, tag, a, b, vals, gens, free, h, x, hn)
366
367# positions before the new element are unchanged
368def 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: {S.validate(T, S.DS{tag, SC.append(Nat, a, Con{S.handle_id(h), b}), vals, gens, free}, h) == None{} : Maybe<&2, E.Error>}, +hn: {SC.memn(S.handle_id(h), a) == False{} : Bool}) -> S.Insert.insert_before_equal(T, tag, a, b, vals, gens, free, h, x, hv, hn):
369 %Equal.sym(List<&2, Nat>, S.ord(T, S.nx(T, S.DS{tag, SC.append(Nat, a, Con{S.handle_id(h), b}), vals, gens, free}, E.InsertBefore{h, x})), SC.append(Nat, a, Con{Pair.snd(S.DS<T>, Nat, S.alloc(T, S.DS{tag, SC.append(Nat, a, Con{S.handle_id(h), b}), vals, gens, free})), Con{S.handle_id(h), b}}), insert_before_order(T, tag, a, b, vals, gens, free, h, x, hv, hn)) : V.RangeEqual(Nat, SC.append(Nat, a, Con{S.handle_id(h), b}), _, 0n, SC.length(Nat, a))
370 VL.mid_equal(Nat, a, Con{S.handle_id(h), b}, Pair.snd(S.DS<T>, Nat, S.alloc(T, S.DS{tag, SC.append(Nat, a, Con{S.handle_id(h), b}), vals, gens, free})))
371
372# the new element is at Before's old position
373def 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: {S.validate(T, S.DS{tag, SC.append(Nat, a, Con{S.handle_id(h), b}), vals, gens, free}, h) == None{} : Maybe<&2, E.Error>}, +hn: {SC.memn(S.handle_id(h), a) == False{} : Bool}) -> S.Insert.insert_before_at(T, tag, a, b, vals, gens, free, h, x, hv, hn):
374 %Equal.sym(List<&2, Nat>, S.ord(T, S.nx(T, S.DS{tag, SC.append(Nat, a, Con{S.handle_id(h), b}), vals, gens, free}, E.InsertBefore{h, x})), SC.append(Nat, a, Con{Pair.snd(S.DS<T>, Nat, S.alloc(T, S.DS{tag, SC.append(Nat, a, Con{S.handle_id(h), b}), vals, gens, free})), Con{S.handle_id(h), b}}), insert_before_order(T, tag, a, b, vals, gens, free, h, x, hv, hn)) : {SC.nth(Nat, _, SC.length(Nat, a)) == Some{Pair.snd(S.DS<T>, Nat, S.alloc(T, S.DS{tag, SC.append(Nat, a, Con{S.handle_id(h), b}), vals, gens, free}))} : Maybe<&2, Nat>}
375 VL.mid_at(Nat, a, Con{S.handle_id(h), b}, Pair.snd(S.DS<T>, Nat, S.alloc(T, S.DS{tag, SC.append(Nat, a, Con{S.handle_id(h), b}), vals, gens, free})))
376
377# Before and the positions after it move up by one
378def 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: {S.validate(T, S.DS{tag, SC.append(Nat, a, Con{S.handle_id(h), b}), vals, gens, free}, h) == None{} : Maybe<&2, E.Error>}, +hn: {SC.memn(S.handle_id(h), a) == False{} : Bool}) -> S.Insert.insert_before_shifted(T, tag, a, b, vals, gens, free, h, x, hv, hn):
379 %Equal.sym(List<&2, Nat>, S.ord(T, S.nx(T, S.DS{tag, SC.append(Nat, a, Con{S.handle_id(h), b}), vals, gens, free}, E.InsertBefore{h, x})), SC.append(Nat, a, Con{Pair.snd(S.DS<T>, Nat, S.alloc(T, S.DS{tag, SC.append(Nat, a, Con{S.handle_id(h), b}), vals, gens, free})), Con{S.handle_id(h), b}}), insert_before_order(T, tag, a, b, vals, gens, free, h, x, hv, hn)) : V.RangeShifted(Nat, SC.append(Nat, a, Con{S.handle_id(h), b}), _, SC.length(Nat, a), SC.length(Nat, SC.append(Nat, a, Con{S.handle_id(h), b})), 1n)
380 VL.mid_shifted(Nat, a, Con{S.handle_id(h), b}, Pair.snd(S.DS<T>, Nat, S.alloc(T, S.DS{tag, SC.append(Nat, a, Con{S.handle_id(h), b}), vals, gens, free})))
381
382def 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: {S.validate(T, S.DS{tag, SC.append(Nat, a, Con{S.handle_id(h), b}), vals, gens, free}, h) == None{} : Maybe<&2, E.Error>}, +hn: {SC.memn(S.handle_id(h), a) == False{} : Bool}) -> S.Insert.insert_before_length(T, tag, a, b, vals, gens, free, h, x, hv, hn):
383 %Equal.sym(List<&2, Nat>, S.ord(T, S.nx(T, S.DS{tag, SC.append(Nat, a, Con{S.handle_id(h), b}), vals, gens, free}, E.InsertBefore{h, x})), SC.append(Nat, a, Con{Pair.snd(S.DS<T>, Nat, S.alloc(T, S.DS{tag, SC.append(Nat, a, Con{S.handle_id(h), b}), vals, gens, free})), Con{S.handle_id(h), b}}), insert_before_order(T, tag, a, b, vals, gens, free, h, x, hv, hn)) : {SC.length(Nat, _) == 1n+SC.length(Nat, SC.append(Nat, a, Con{S.handle_id(h), b})) : Nat}
384 VL.mid_length(Nat, a, Con{S.handle_id(h), b}, Pair.snd(S.DS<T>, Nat, S.alloc(T, S.DS{tag, SC.append(Nat, a, Con{S.handle_id(h), b}), vals, gens, free})))
385
386# ---- Insert after (SPARK: Insert before Next (Position)) ----
387def ia_free(-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, +hn: {SC.memn(S.handle_id(h), a) == False{} : Bool}) -> {S.ord(T, Pair.fst(S.DS<T>, E.Obs<T>, S.live_op(T, S.DS{tag, SC.append(Nat, a, Con{S.handle_id(h), b}), vals, gens, free}, E.InsertAfter{h, x}, S.handle_id(h)))) == SC.append(Nat, a, Con{S.handle_id(h), Con{Pair.snd(S.DS<T>, Nat, S.alloc(T, S.DS{tag, SC.append(Nat, a, Con{S.handle_id(h), b}), vals, gens, free})), b}}) : List<&2, Nat>}:
388 match free:
389 case Nil{}:
390 ia_app(a, S.handle_id(h), b, SC.length(Maybe<&2, T>, vals), hn)
391 case Con{+i, +rest}:
392 ia_app(a, S.handle_id(h), b, i, hn)
393
394def insert_after_order(-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: {S.validate(T, S.DS{tag, SC.append(Nat, a, Con{S.handle_id(h), b}), vals, gens, free}, h) == None{} : Maybe<&2, E.Error>}, +hn: {SC.memn(S.handle_id(h), a) == False{} : Bool}) -> {S.ord(T, S.nx(T, S.DS{tag, SC.append(Nat, a, Con{S.handle_id(h), b}), vals, gens, free}, E.InsertAfter{h, x})) == SC.append(Nat, SC.snoc(Nat, a, S.handle_id(h)), Con{Pair.snd(S.DS<T>, Nat, S.alloc(T, S.DS{tag, SC.append(Nat, a, Con{S.handle_id(h), b}), vals, gens, free})), b}) : List<&2, Nat>}:
395 %Equal.sym(S.DS<T> & E.Obs<T>, S.checked(T, S.DS{tag, SC.append(Nat, a, Con{S.handle_id(h), b}), vals, gens, free}, E.InsertAfter{h, x}, h, S.validate(T, S.DS{tag, SC.append(Nat, a, Con{S.handle_id(h), b}), vals, gens, free}, h)), S.live_op(T, S.DS{tag, SC.append(Nat, a, Con{S.handle_id(h), b}), vals, gens, free}, E.InsertAfter{h, x}, S.handle_id(h)), live(T, S.DS{tag, SC.append(Nat, a, Con{S.handle_id(h), b}), vals, gens, free}, E.InsertAfter{h, x}, h, hv)) : {S.ord(T, Pair.fst(S.DS<T>, E.Obs<T>, _)) == SC.append(Nat, SC.snoc(Nat, a, S.handle_id(h)), Con{Pair.snd(S.DS<T>, Nat, S.alloc(T, S.DS{tag, SC.append(Nat, a, Con{S.handle_id(h), b}), vals, gens, free})), b}) : List<&2, Nat>}
396 %Equal.sym(List<&2, Nat>, SC.append(Nat, SC.snoc(Nat, a, S.handle_id(h)), Con{Pair.snd(S.DS<T>, Nat, S.alloc(T, S.DS{tag, SC.append(Nat, a, Con{S.handle_id(h), b}), vals, gens, free})), b}), SC.append(Nat, a, Con{S.handle_id(h), Con{Pair.snd(S.DS<T>, Nat, S.alloc(T, S.DS{tag, SC.append(Nat, a, Con{S.handle_id(h), b}), vals, gens, free})), b}}), LL.snoc_append_cons(Nat, a, S.handle_id(h), Con{Pair.snd(S.DS<T>, Nat, S.alloc(T, S.DS{tag, SC.append(Nat, a, Con{S.handle_id(h), b}), vals, gens, free})), b})) : {S.ord(T, Pair.fst(S.DS<T>, E.Obs<T>, S.live_op(T, S.DS{tag, SC.append(Nat, a, Con{S.handle_id(h), b}), vals, gens, free}, E.InsertAfter{h, x}, S.handle_id(h)))) == _ : List<&2, Nat>}
397 ia_free(T, tag, a, b, vals, gens, free, h, x, hn)
398
399# the old order split after Position
400def split_after(+a: List<&2, Nat>, +i: Nat, +b: List<&2, Nat>) -> {SC.append(Nat, a, Con{i, b}) == SC.append(Nat, SC.snoc(Nat, a, i), b) : List<&2, Nat>}:
401 Equal.sym(List<&2, Nat>, SC.append(Nat, SC.snoc(Nat, a, i), b), SC.append(Nat, a, Con{i, b}), LL.snoc_append_cons(Nat, a, i, b))
402
403# Position and the positions before it are unchanged
404def 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: {S.validate(T, S.DS{tag, SC.append(Nat, a, Con{S.handle_id(h), b}), vals, gens, free}, h) == None{} : Maybe<&2, E.Error>}, +hn: {SC.memn(S.handle_id(h), a) == False{} : Bool}) -> S.Insert.insert_after_equal(T, tag, a, b, vals, gens, free, h, x, hv, hn):
405 %Equal.sym(List<&2, Nat>, S.ord(T, S.nx(T, S.DS{tag, SC.append(Nat, a, Con{S.handle_id(h), b}), vals, gens, free}, E.InsertAfter{h, x})), SC.append(Nat, SC.snoc(Nat, a, S.handle_id(h)), Con{Pair.snd(S.DS<T>, Nat, S.alloc(T, S.DS{tag, SC.append(Nat, a, Con{S.handle_id(h), b}), vals, gens, free})), b}), insert_after_order(T, tag, a, b, vals, gens, free, h, x, hv, hn)) : V.RangeEqual(Nat, SC.append(Nat, a, Con{S.handle_id(h), b}), _, 0n, 1n+SC.length(Nat, a))
406 %Equal.sym(List<&2, Nat>, SC.append(Nat, a, Con{S.handle_id(h), b}), SC.append(Nat, SC.snoc(Nat, a, S.handle_id(h)), b), split_after(a, S.handle_id(h), b)) : V.RangeEqual(Nat, _, SC.append(Nat, SC.snoc(Nat, a, S.handle_id(h)), Con{Pair.snd(S.DS<T>, Nat, S.alloc(T, S.DS{tag, SC.append(Nat, a, Con{S.handle_id(h), b}), vals, gens, free})), b}), 0n, 1n+SC.length(Nat, a))
407 %LL.length_snoc(Nat, a, S.handle_id(h)) : V.RangeEqual(Nat, SC.append(Nat, SC.snoc(Nat, a, S.handle_id(h)), b), SC.append(Nat, SC.snoc(Nat, a, S.handle_id(h)), Con{Pair.snd(S.DS<T>, Nat, S.alloc(T, S.DS{tag, SC.append(Nat, a, Con{S.handle_id(h), b}), vals, gens, free})), b}), 0n, _)
408 VL.mid_equal(Nat, SC.snoc(Nat, a, S.handle_id(h)), b, Pair.snd(S.DS<T>, Nat, S.alloc(T, S.DS{tag, SC.append(Nat, a, Con{S.handle_id(h), b}), vals, gens, free})))
409
410# the new element is right after Position
411def 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: {S.validate(T, S.DS{tag, SC.append(Nat, a, Con{S.handle_id(h), b}), vals, gens, free}, h) == None{} : Maybe<&2, E.Error>}, +hn: {SC.memn(S.handle_id(h), a) == False{} : Bool}) -> S.Insert.insert_after_at(T, tag, a, b, vals, gens, free, h, x, hv, hn):
412 %Equal.sym(List<&2, Nat>, S.ord(T, S.nx(T, S.DS{tag, SC.append(Nat, a, Con{S.handle_id(h), b}), vals, gens, free}, E.InsertAfter{h, x})), SC.append(Nat, SC.snoc(Nat, a, S.handle_id(h)), Con{Pair.snd(S.DS<T>, Nat, S.alloc(T, S.DS{tag, SC.append(Nat, a, Con{S.handle_id(h), b}), vals, gens, free})), b}), insert_after_order(T, tag, a, b, vals, gens, free, h, x, hv, hn)) : {SC.nth(Nat, _, 1n+SC.length(Nat, a)) == Some{Pair.snd(S.DS<T>, Nat, S.alloc(T, S.DS{tag, SC.append(Nat, a, Con{S.handle_id(h), b}), vals, gens, free}))} : Maybe<&2, Nat>}
413 %LL.length_snoc(Nat, a, S.handle_id(h)) : {SC.nth(Nat, SC.append(Nat, SC.snoc(Nat, a, S.handle_id(h)), Con{Pair.snd(S.DS<T>, Nat, S.alloc(T, S.DS{tag, SC.append(Nat, a, Con{S.handle_id(h), b}), vals, gens, free})), b}), _) == Some{Pair.snd(S.DS<T>, Nat, S.alloc(T, S.DS{tag, SC.append(Nat, a, Con{S.handle_id(h), b}), vals, gens, free}))} : Maybe<&2, Nat>}
414 VL.mid_at(Nat, SC.snoc(Nat, a, S.handle_id(h)), b, Pair.snd(S.DS<T>, Nat, S.alloc(T, S.DS{tag, SC.append(Nat, a, Con{S.handle_id(h), b}), vals, gens, free})))
415
416# the positions after Position move up by one
417def 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: {S.validate(T, S.DS{tag, SC.append(Nat, a, Con{S.handle_id(h), b}), vals, gens, free}, h) == None{} : Maybe<&2, E.Error>}, +hn: {SC.memn(S.handle_id(h), a) == False{} : Bool}) -> S.Insert.insert_after_shifted(T, tag, a, b, vals, gens, free, h, x, hv, hn):
418 %Equal.sym(List<&2, Nat>, S.ord(T, S.nx(T, S.DS{tag, SC.append(Nat, a, Con{S.handle_id(h), b}), vals, gens, free}, E.InsertAfter{h, x})), SC.append(Nat, SC.snoc(Nat, a, S.handle_id(h)), Con{Pair.snd(S.DS<T>, Nat, S.alloc(T, S.DS{tag, SC.append(Nat, a, Con{S.handle_id(h), b}), vals, gens, free})), b}), insert_after_order(T, tag, a, b, vals, gens, free, h, x, hv, hn)) : V.RangeShifted(Nat, SC.append(Nat, a, Con{S.handle_id(h), b}), _, 1n+SC.length(Nat, a), SC.length(Nat, SC.append(Nat, a, Con{S.handle_id(h), b})), 1n)
419 %Equal.sym(List<&2, Nat>, SC.append(Nat, a, Con{S.handle_id(h), b}), SC.append(Nat, SC.snoc(Nat, a, S.handle_id(h)), b), split_after(a, S.handle_id(h), b)) : V.RangeShifted(Nat, _, SC.append(Nat, SC.snoc(Nat, a, S.handle_id(h)), Con{Pair.snd(S.DS<T>, Nat, S.alloc(T, S.DS{tag, SC.append(Nat, a, Con{S.handle_id(h), b}), vals, gens, free})), b}), 1n+SC.length(Nat, a), SC.length(Nat, _), 1n)
420 %LL.length_snoc(Nat, a, S.handle_id(h)) : V.RangeShifted(Nat, SC.append(Nat, SC.snoc(Nat, a, S.handle_id(h)), b), SC.append(Nat, SC.snoc(Nat, a, S.handle_id(h)), Con{Pair.snd(S.DS<T>, Nat, S.alloc(T, S.DS{tag, SC.append(Nat, a, Con{S.handle_id(h), b}), vals, gens, free})), b}), _, SC.length(Nat, SC.append(Nat, SC.snoc(Nat, a, S.handle_id(h)), b)), 1n)
421 VL.mid_shifted(Nat, SC.snoc(Nat, a, S.handle_id(h)), b, Pair.snd(S.DS<T>, Nat, S.alloc(T, S.DS{tag, SC.append(Nat, a, Con{S.handle_id(h), b}), vals, gens, free})))
422
423def 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: {S.validate(T, S.DS{tag, SC.append(Nat, a, Con{S.handle_id(h), b}), vals, gens, free}, h) == None{} : Maybe<&2, E.Error>}, +hn: {SC.memn(S.handle_id(h), a) == False{} : Bool}) -> S.Insert.insert_after_length(T, tag, a, b, vals, gens, free, h, x, hv, hn):
424 %Equal.sym(List<&2, Nat>, S.ord(T, S.nx(T, S.DS{tag, SC.append(Nat, a, Con{S.handle_id(h), b}), vals, gens, free}, E.InsertAfter{h, x})), SC.append(Nat, SC.snoc(Nat, a, S.handle_id(h)), Con{Pair.snd(S.DS<T>, Nat, S.alloc(T, S.DS{tag, SC.append(Nat, a, Con{S.handle_id(h), b}), vals, gens, free})), b}), insert_after_order(T, tag, a, b, vals, gens, free, h, x, hv, hn)) : {SC.length(Nat, _) == 1n+SC.length(Nat, SC.append(Nat, a, Con{S.handle_id(h), b})) : Nat}
425 %Equal.sym(List<&2, Nat>, SC.append(Nat, a, Con{S.handle_id(h), b}), SC.append(Nat, SC.snoc(Nat, a, S.handle_id(h)), b), split_after(a, S.handle_id(h), b)) : {SC.length(Nat, SC.append(Nat, SC.snoc(Nat, a, S.handle_id(h)), Con{Pair.snd(S.DS<T>, Nat, S.alloc(T, S.DS{tag, SC.append(Nat, a, Con{S.handle_id(h), b}), vals, gens, free})), b})) == 1n+SC.length(Nat, _) : Nat}
426 VL.mid_length(Nat, SC.snoc(Nat, a, S.handle_id(h)), b, Pair.snd(S.DS<T>, Nat, S.alloc(T, S.DS{tag, SC.append(Nat, a, Con{S.handle_id(h), b}), vals, gens, free})))
427
428# ---- Delete ----
429def remove_step(-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: {S.validate(T, S.DS{tag, SC.append(Nat, a, Con{S.handle_id(h), b}), vals, gens, free}, h) == None{} : Maybe<&2, E.Error>}, +v: T, +hval: {S.val_of(T, vals, S.handle_id(h)) == Some{v} : Maybe<&2, T>}) -> {S.step(T, S.DS{tag, SC.append(Nat, a, Con{S.handle_id(h), b}), vals, gens, free}, E.Remove{h}) == S.removed(T, tag, SC.append(Nat, a, Con{S.handle_id(h), b}), vals, S.handle_id(h), v, S.retire(gens, S.handle_id(h), free, S.gen_of(gens, S.handle_id(h)), U32.is_eq(S.gen_of(gens, S.handle_id(h)), 4294967295))) : S.DS<T> & E.Obs<T>}:
430 %Equal.sym(S.DS<T> & E.Obs<T>, S.checked(T, S.DS{tag, SC.append(Nat, a, Con{S.handle_id(h), b}), vals, gens, free}, E.Remove{h}, h, S.validate(T, S.DS{tag, SC.append(Nat, a, Con{S.handle_id(h), b}), vals, gens, free}, h)), S.live_op(T, S.DS{tag, SC.append(Nat, a, Con{S.handle_id(h), b}), vals, gens, free}, E.Remove{h}, S.handle_id(h)), live(T, S.DS{tag, SC.append(Nat, a, Con{S.handle_id(h), b}), vals, gens, free}, E.Remove{h}, h, hv)) : {_ == S.removed(T, tag, SC.append(Nat, a, Con{S.handle_id(h), b}), vals, S.handle_id(h), v, S.retire(gens, S.handle_id(h), free, S.gen_of(gens, S.handle_id(h)), U32.is_eq(S.gen_of(gens, S.handle_id(h)), 4294967295))) : S.DS<T> & E.Obs<T>}
431 %Equal.sym(Maybe<&2, T>, S.val_of(T, vals, S.handle_id(h)), Some{v}, hval) : {S.remove_m(T, tag, SC.append(Nat, a, Con{S.handle_id(h), b}), vals, gens, free, S.handle_id(h), _) == S.removed(T, tag, SC.append(Nat, a, Con{S.handle_id(h), b}), vals, S.handle_id(h), v, S.retire(gens, S.handle_id(h), free, S.gen_of(gens, S.handle_id(h)), U32.is_eq(S.gen_of(gens, S.handle_id(h)), 4294967295))) : S.DS<T> & E.Obs<T>}
432 {==}
433
434def rm_ord(-T: Data, +tag: U32, +o: List<&2, Nat>, +vals: List<&2, Maybe<&2, T>>, +i: Nat, +v: T, r: List<&2, U32> & List<&2, Nat>) -> {S.ord(T, Pair.fst(S.DS<T>, E.Obs<T>, S.removed(T, tag, o, vals, i, v, r))) == S.delete(o, i) : List<&2, Nat>}:
435 match r:
436 case Tuple{g, f}:
437 {==}
438
439def rm_obs(-T: Data, +tag: U32, +o: List<&2, Nat>, +vals: List<&2, Maybe<&2, T>>, +i: Nat, +v: T, r: List<&2, U32> & List<&2, Nat>) -> {Pair.snd(S.DS<T>, E.Obs<T>, S.removed(T, tag, o, vals, i, v, r)) == E.OVal{Done{v}} : E.Obs<T>}:
440 match r:
441 case Tuple{g, f}:
442 {==}
443
444def remove_order(-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: {S.validate(T, S.DS{tag, SC.append(Nat, a, Con{S.handle_id(h), b}), vals, gens, free}, h) == None{} : Maybe<&2, E.Error>}, +hn: {SC.memn(S.handle_id(h), a) == False{} : Bool}, +v: T, +hval: {S.val_of(T, vals, S.handle_id(h)) == Some{v} : Maybe<&2, T>}) -> {S.ord(T, S.nx(T, S.DS{tag, SC.append(Nat, a, Con{S.handle_id(h), b}), vals, gens, free}, E.Remove{h})) == SC.append(Nat, a, b) : List<&2, Nat>}:
445 %Equal.sym(S.DS<T> & E.Obs<T>, S.step(T, S.DS{tag, SC.append(Nat, a, Con{S.handle_id(h), b}), vals, gens, free}, E.Remove{h}), S.removed(T, tag, SC.append(Nat, a, Con{S.handle_id(h), b}), vals, S.handle_id(h), v, S.retire(gens, S.handle_id(h), free, S.gen_of(gens, S.handle_id(h)), U32.is_eq(S.gen_of(gens, S.handle_id(h)), 4294967295))), remove_step(T, tag, a, b, vals, gens, free, h, hv, v, hval)) : {S.ord(T, Pair.fst(S.DS<T>, E.Obs<T>, _)) == SC.append(Nat, a, b) : List<&2, Nat>}
446 %Equal.sym(List<&2, Nat>, S.ord(T, Pair.fst(S.DS<T>, E.Obs<T>, S.removed(T, tag, SC.append(Nat, a, Con{S.handle_id(h), b}), vals, S.handle_id(h), v, S.retire(gens, S.handle_id(h), free, S.gen_of(gens, S.handle_id(h)), U32.is_eq(S.gen_of(gens, S.handle_id(h)), 4294967295))))), S.delete(SC.append(Nat, a, Con{S.handle_id(h), b}), S.handle_id(h)), rm_ord(T, tag, SC.append(Nat, a, Con{S.handle_id(h), b}), vals, S.handle_id(h), v, S.retire(gens, S.handle_id(h), free, S.gen_of(gens, S.handle_id(h)), U32.is_eq(S.gen_of(gens, S.handle_id(h)), 4294967295)))) : {_ == SC.append(Nat, a, b) : List<&2, Nat>}
447 del_app(a, S.handle_id(h), b, hn)
448
449# the returned element is the deleted one
450def 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: {S.validate(T, S.DS{tag, SC.append(Nat, a, Con{S.handle_id(h), b}), vals, gens, free}, h) == None{} : Maybe<&2, E.Error>}, +v: T, +hval: {S.val_of(T, vals, S.handle_id(h)) == Some{v} : Maybe<&2, T>}) -> S.Delete.remove_result(T, tag, a, b, vals, gens, free, h, hv, v, hval):
451 %Equal.sym(S.DS<T> & E.Obs<T>, S.step(T, S.DS{tag, SC.append(Nat, a, Con{S.handle_id(h), b}), vals, gens, free}, E.Remove{h}), S.removed(T, tag, SC.append(Nat, a, Con{S.handle_id(h), b}), vals, S.handle_id(h), v, S.retire(gens, S.handle_id(h), free, S.gen_of(gens, S.handle_id(h)), U32.is_eq(S.gen_of(gens, S.handle_id(h)), 4294967295))), remove_step(T, tag, a, b, vals, gens, free, h, hv, v, hval)) : {Pair.snd(S.DS<T>, E.Obs<T>, _) == E.OVal{Done{v}} : E.Obs<T>}
452 rm_obs(T, tag, SC.append(Nat, a, Con{S.handle_id(h), b}), vals, S.handle_id(h), v, S.retire(gens, S.handle_id(h), free, S.gen_of(gens, S.handle_id(h)), U32.is_eq(S.gen_of(gens, S.handle_id(h)), 4294967295)))
453
454# positions before Position are unchanged
455def 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: {S.validate(T, S.DS{tag, SC.append(Nat, a, Con{S.handle_id(h), b}), vals, gens, free}, h) == None{} : Maybe<&2, E.Error>}, +hn: {SC.memn(S.handle_id(h), a) == False{} : Bool}, +v: T, +hval: {S.val_of(T, vals, S.handle_id(h)) == Some{v} : Maybe<&2, T>}) -> S.Delete.remove_equal(T, tag, a, b, vals, gens, free, h, hv, hn, v, hval):
456 %Equal.sym(List<&2, Nat>, S.ord(T, S.nx(T, S.DS{tag, SC.append(Nat, a, Con{S.handle_id(h), b}), vals, gens, free}, E.Remove{h})), SC.append(Nat, a, b), remove_order(T, tag, a, b, vals, gens, free, h, hv, hn, v, hval)) : V.RangeEqual(Nat, _, SC.append(Nat, a, Con{S.handle_id(h), b}), 0n, SC.length(Nat, a))
457 VL.mid_equal(Nat, a, b, S.handle_id(h))
458
459# the positions after it move down by one
460def 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: {S.validate(T, S.DS{tag, SC.append(Nat, a, Con{S.handle_id(h), b}), vals, gens, free}, h) == None{} : Maybe<&2, E.Error>}, +hn: {SC.memn(S.handle_id(h), a) == False{} : Bool}, +v: T, +hval: {S.val_of(T, vals, S.handle_id(h)) == Some{v} : Maybe<&2, T>}) -> S.Delete.remove_shifted(T, tag, a, b, vals, gens, free, h, hv, hn, v, hval):
461 %Equal.sym(List<&2, Nat>, S.ord(T, S.nx(T, S.DS{tag, SC.append(Nat, a, Con{S.handle_id(h), b}), vals, gens, free}, E.Remove{h})), SC.append(Nat, a, b), remove_order(T, tag, a, b, vals, gens, free, h, hv, hn, v, hval)) : V.RangeShifted(Nat, _, SC.append(Nat, a, Con{S.handle_id(h), b}), SC.length(Nat, a), SC.length(Nat, _), 1n)
462 VL.mid_shifted(Nat, a, b, S.handle_id(h))
463
464def 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: {S.validate(T, S.DS{tag, SC.append(Nat, a, Con{S.handle_id(h), b}), vals, gens, free}, h) == None{} : Maybe<&2, E.Error>}, +hn: {SC.memn(S.handle_id(h), a) == False{} : Bool}, +v: T, +hval: {S.val_of(T, vals, S.handle_id(h)) == Some{v} : Maybe<&2, T>}) -> S.Delete.remove_length(T, tag, a, b, vals, gens, free, h, hv, hn, v, hval):
465 %Equal.sym(List<&2, Nat>, S.ord(T, S.nx(T, S.DS{tag, SC.append(Nat, a, Con{S.handle_id(h), b}), vals, gens, free}, E.Remove{h})), SC.append(Nat, a, b), remove_order(T, tag, a, b, vals, gens, free, h, hv, hn, v, hval)) : {SC.length(Nat, SC.append(Nat, a, Con{S.handle_id(h), b})) == 1n+SC.length(Nat, _) : Nat}
466 VL.mid_length(Nat, a, b, S.handle_id(h))
467
468# the handle no longer designates an element (SPARK: Position = No_Element)
469def stale_own(-T: Data, +vals: List<&2, Maybe<&2, T>>, +gens: List<&2, U32>, +i: Nat, +g: U32, +mine: Bool, +hl: {Nat.is_lt(i, SC.length(Maybe<&2, T>, vals)) == True{} : Bool}) -> {S.has_of(S.valid_own(T, SC.update(Maybe<&2, T>, vals, i, None{}), gens, i, g, mine)) == False{} : Bool}:
470 match mine:
471 case False{}:
472 {==}
473 case True{}:
474 %Equal.sym(Maybe<&2, T>, S.val_of(T, SC.update(Maybe<&2, T>, vals, i, None{}), i), None{}, val_update_same(T, vals, i, None{}, hl)) : {S.has_of(S.live_gen(T, _, U32.is_eq(S.gen_of(gens, i), g))) == False{} : Bool}
475 {==}
476
477def stale_h(-T: Data, +h: E.Handle, +tag: U32, +o: List<&2, Nat>, +vals: List<&2, Maybe<&2, T>>, +g2: List<&2, U32>, +f2: List<&2, Nat>, +hl: {Nat.is_lt(S.handle_id(h), SC.length(Maybe<&2, T>, vals)) == True{} : Bool}) -> {S.has_element(T, S.DS{tag, S.delete(o, S.handle_id(h)), SC.update(Maybe<&2, T>, vals, S.handle_id(h), None{}), g2, f2}, h) == False{} : Bool}:
478 match h:
479 case E.H{+owner, +id, +g}:
480 stale_own(T, vals, g2, U32.to_nat(id), g, U32.is_eq(owner, tag), hl)
481
482def stale_r(-T: Data, +tag: U32, +o: List<&2, Nat>, +vals: List<&2, Maybe<&2, T>>, +h: E.Handle, +v: T, +hl: {Nat.is_lt(S.handle_id(h), SC.length(Maybe<&2, T>, vals)) == True{} : Bool}, r: List<&2, U32> & List<&2, Nat>) -> {S.has_element(T, Pair.fst(S.DS<T>, E.Obs<T>, S.removed(T, tag, o, vals, S.handle_id(h), v, r)), h) == False{} : Bool}:
483 match r:
484 case Tuple{+g2, +f2}:
485 stale_h(T, h, tag, o, vals, g2, f2, hl)
486
487def 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: {S.validate(T, S.DS{tag, SC.append(Nat, a, Con{S.handle_id(h), b}), vals, gens, free}, h) == None{} : Maybe<&2, E.Error>}, +v: T, +hval: {S.val_of(T, vals, S.handle_id(h)) == Some{v} : Maybe<&2, T>}) -> S.Delete.remove_stale(T, tag, a, b, vals, gens, free, h, hv, v, hval):
488 %Equal.sym(S.DS<T> & E.Obs<T>, S.step(T, S.DS{tag, SC.append(Nat, a, Con{S.handle_id(h), b}), vals, gens, free}, E.Remove{h}), S.removed(T, tag, SC.append(Nat, a, Con{S.handle_id(h), b}), vals, S.handle_id(h), v, S.retire(gens, S.handle_id(h), free, S.gen_of(gens, S.handle_id(h)), U32.is_eq(S.gen_of(gens, S.handle_id(h)), 4294967295))), remove_step(T, tag, a, b, vals, gens, free, h, hv, v, hval)) : {S.has_element(T, Pair.fst(S.DS<T>, E.Obs<T>, _), h) == False{} : Bool}
489 stale_r(T, tag, SC.append(Nat, a, Con{S.handle_id(h), b}), vals, h, v, val_lt(T, vals, S.handle_id(h), v, hval), S.retire(gens, S.handle_id(h), free, S.gen_of(gens, S.handle_id(h)), U32.is_eq(S.gen_of(gens, S.handle_id(h)), 4294967295)))
490
491# ---- Next / Previous ----
492def 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: {S.validate(T, S.DS{tag, SC.append(Nat, a, Con{S.handle_id(h), b}), vals, gens, free}, h) == None{} : Maybe<&2, E.Error>}, +hn: {SC.memn(S.handle_id(h), a) == False{} : Bool}) -> S.Next.next_result(T, tag, a, b, vals, gens, free, h, hv, hn):
493 %Equal.sym(S.DS<T> & E.Obs<T>, S.checked(T, S.DS{tag, SC.append(Nat, a, Con{S.handle_id(h), b}), vals, gens, free}, E.Next{h}, h, S.validate(T, S.DS{tag, SC.append(Nat, a, Con{S.handle_id(h), b}), vals, gens, free}, h)), S.live_op(T, S.DS{tag, SC.append(Nat, a, Con{S.handle_id(h), b}), vals, gens, free}, E.Next{h}, S.handle_id(h)), live(T, S.DS{tag, SC.append(Nat, a, Con{S.handle_id(h), b}), vals, gens, free}, E.Next{h}, h, hv)) : {Pair.snd(S.DS<T>, E.Obs<T>, _) == E.ONbr{Done{S.nbr(tag, gens, S.first(b))}} : E.Obs<T>}
494 %Equal.sym(Maybe<&2, Nat>, S.after(SC.append(Nat, a, Con{S.handle_id(h), b}), S.handle_id(h)), S.first(b), after_app(a, S.handle_id(h), b, hn)) : {E.ONbr{Done{S.nbr(tag, gens, _)}} == E.ONbr{Done{S.nbr(tag, gens, S.first(b))}} : E.Obs<T>}
495 {==}
496
497def 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: {S.validate(T, S.DS{tag, SC.append(Nat, a, Con{S.handle_id(h), b}), vals, gens, free}, h) == None{} : Maybe<&2, E.Error>}) -> S.Next.next_frame(T, tag, a, b, vals, gens, free, h, hv):
498 %Equal.sym(S.DS<T> & E.Obs<T>, S.checked(T, S.DS{tag, SC.append(Nat, a, Con{S.handle_id(h), b}), vals, gens, free}, E.Next{h}, h, S.validate(T, S.DS{tag, SC.append(Nat, a, Con{S.handle_id(h), b}), vals, gens, free}, h)), S.live_op(T, S.DS{tag, SC.append(Nat, a, Con{S.handle_id(h), b}), vals, gens, free}, E.Next{h}, S.handle_id(h)), live(T, S.DS{tag, SC.append(Nat, a, Con{S.handle_id(h), b}), vals, gens, free}, E.Next{h}, h, hv)) : {Pair.fst(S.DS<T>, E.Obs<T>, _) == S.DS{tag, SC.append(Nat, a, Con{S.handle_id(h), b}), vals, gens, free} : S.DS<T>}
499 {==}
500
501def 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: {S.validate(T, S.DS{tag, SC.append(Nat, a, Con{S.handle_id(h), b}), vals, gens, free}, h) == None{} : Maybe<&2, E.Error>}, +hn: {SC.memn(S.handle_id(h), a) == False{} : Bool}) -> S.Previous.prev_result(T, tag, a, b, vals, gens, free, h, hv, hn):
502 %Equal.sym(S.DS<T> & E.Obs<T>, S.checked(T, S.DS{tag, SC.append(Nat, a, Con{S.handle_id(h), b}), vals, gens, free}, E.Prev{h}, h, S.validate(T, S.DS{tag, SC.append(Nat, a, Con{S.handle_id(h), b}), vals, gens, free}, h)), S.live_op(T, S.DS{tag, SC.append(Nat, a, Con{S.handle_id(h), b}), vals, gens, free}, E.Prev{h}, S.handle_id(h)), live(T, S.DS{tag, SC.append(Nat, a, Con{S.handle_id(h), b}), vals, gens, free}, E.Prev{h}, h, hv)) : {Pair.snd(S.DS<T>, E.Obs<T>, _) == E.ONbr{Done{S.nbr(tag, gens, S.lastm(a, None{}))}} : E.Obs<T>}
503 %Equal.sym(Maybe<&2, Nat>, S.before(SC.append(Nat, a, Con{S.handle_id(h), b}), S.handle_id(h), None{}), S.lastm(a, None{}), before_app(a, S.handle_id(h), b, None{}, hn)) : {E.ONbr{Done{S.nbr(tag, gens, _)}} == E.ONbr{Done{S.nbr(tag, gens, S.lastm(a, None{}))}} : E.Obs<T>}
504 {==}
505
506# the first element has no previous one
507def 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: {S.validate(T, S.DS{tag, Con{S.handle_id(h), b}, vals, gens, free}, h) == None{} : Maybe<&2, E.Error>}) -> S.Previous.prev_first(T, tag, b, vals, gens, free, h, hv):
508 prev_result(T, tag, Nil{}, b, vals, gens, free, h, hv, {==})
509
510def 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: {S.validate(T, S.DS{tag, SC.append(Nat, a, Con{S.handle_id(h), b}), vals, gens, free}, h) == None{} : Maybe<&2, E.Error>}) -> S.Previous.prev_frame(T, tag, a, b, vals, gens, free, h, hv):
511 %Equal.sym(S.DS<T> & E.Obs<T>, S.checked(T, S.DS{tag, SC.append(Nat, a, Con{S.handle_id(h), b}), vals, gens, free}, E.Prev{h}, h, S.validate(T, S.DS{tag, SC.append(Nat, a, Con{S.handle_id(h), b}), vals, gens, free}, h)), S.live_op(T, S.DS{tag, SC.append(Nat, a, Con{S.handle_id(h), b}), vals, gens, free}, E.Prev{h}, S.handle_id(h)), live(T, S.DS{tag, SC.append(Nat, a, Con{S.handle_id(h), b}), vals, gens, free}, E.Prev{h}, h, hv)) : {Pair.fst(S.DS<T>, E.Obs<T>, _) == S.DS{tag, SC.append(Nat, a, Con{S.handle_id(h), b}), vals, gens, free} : S.DS<T>}
512 {==}