proofs/containers/dynamic_array/proof.bend
bend-collections-laws-containers@1.0.0.0 · 305 lines · 0 definitions
1import Base
2import bend-collections-laws-containers@1.0.0.0/proofs/lib/logic.bend as L
3import bend-collections-laws-containers@1.0.0.0/proofs/lib/list.bend as LL
4import bend-collections-laws-containers@1.0.0.0/proofs/lib/nat.bend as N
5import bend-collections-laws-containers@1.0.0.0/proofs/lib/array.bend as AR
6import bend-collections-laws-containers@1.0.0.0/spec/containers/dynamic_array.bend as S
7import bend-collections-laws-containers@1.0.0.0/src/containers/dynamic_array.bend as DA
8import bend-collections-laws-containers@1.0.0.0/src/containers/types/dynamic_array.bend as E
9import bend-collections-laws-containers@1.0.0.0/proofs/containers/dynamic_array/state.bend as ST
10import bend-collections-laws-containers@1.0.0.0/proofs/containers/dynamic_array/steps.bend as SP
11import bend-collections-laws-containers@1.0.0.0/proofs/containers/dynamic_array/trace.bend as TR
12import bend-collections-laws-containers@1.0.0.0/proofs/containers/dynamic_array/closed.bend as CL
13import bend-collections-laws-containers@1.0.0.0/proofs/containers/dynamic_array/owned_instances.bend as OWN
14import bend-collections-laws-containers@1.0.0.0/proofs/containers/dynamic_array/owned_swap.bend as OS
15import bend-collections-laws-containers@1.0.0.0/spec/lib/common.bend as SC
16import bend-collections-laws-containers@1.0.0.0/spec/lib/sequence.bend as V
17import bend-collections-laws-containers@1.0.0.0/proofs/lib/sequence.bend as VL
18
19# Dynamic array: public proof entry point.
20# abstraction ST.abs (Base.Array slots -> item sequence, via AR.freeze)
21# invariant ST.Inv (the array realizes a shadow satisfying ST.good)
22# operations SP.step_ok (every operation, errors included)
23# traces trace_new / trace_with_limit (arbitrary finite op lists)
24# The element type T is an arbitrary Data type (parametric; no template).
25
26def view(-T: Data, r: DA.DynArray<&2, T> & List<&2, E.Obs<T>>) -> S.Model<T> & List<&2, E.Obs<T>>:
27 match r:
28 case Tuple{da, os}:
29 (ST.abs(T, da), os)
30
31def view1(-T: Data, r: DA.DynArray<&2, T> & E.Obs<T>) -> S.Model<T> & E.Obs<T>:
32 match r:
33 case Tuple{da, o}:
34 (ST.abs(T, da), o)
35
36# ---- initialization ----
37
38def new_inv(-T: Data) -> ST.Inv(T, DA.new(T)):
39 (TR.initial(T), ({==}, TR.new_good(T)))
40
41def new_abs(-T: Data) -> {ST.abs(T, DA.new(T)) == S.new(T) : S.Model<T>}:
42 {==}
43
44def limit_good(-T: Data, +k: Nat) -> {ST.good(T, TR.limited(T, k)) == True{} : Bool}:
45 ST.good_intro(T, DA.clamp_limit(k, Nat.is_lt(k, 31n)), 0n, 0n, AR.TLeaf{None{}}, Pair.fst({Nat.is_le(DA.clamp_limit(k, Nat.is_lt(k, 31n)), 31n) == True{} : Bool}, {DA.clamp_limit(k, Nat.is_lt(k, 31n)) == Nat.min(k, 31n) : Nat}, TR.clamp_case(k, Nat.is_lt(k, 31n), {==})), N.zero_le(DA.clamp_limit(k, Nat.is_lt(k, 31n))), {==}, {==})
46
47def with_limit_inv(-T: Data, +k: Nat) -> ST.Inv(T, DA.with_limit(T, k)):
48 (TR.limited(T, k), ({==}, limit_good(T, k)))
49
50def with_limit_abs(-T: Data, +k: Nat) -> {ST.abs(T, DA.with_limit(T, k)) == S.with_limit(T, k) : S.Model<T>}:
51 %Equal.sym(Nat, DA.clamp_limit(k, Nat.is_lt(k, 31n)), Nat.min(k, 31n), Pair.snd({Nat.is_le(DA.clamp_limit(k, Nat.is_lt(k, 31n)), 31n) == True{} : Bool}, {DA.clamp_limit(k, Nat.is_lt(k, 31n)) == Nat.min(k, 31n) : Nat}, TR.clamp_case(k, Nat.is_lt(k, 31n), {==}))) : {S.M{_, 0n, Nil{}} == S.M{Nat.min(k, 31n), 0n, Nil{}} : S.Model<T>}
52 {==}
53
54# ---- every operation (errors included), on every reachable representation ----
55
56def step_refines(-T: Data, +sh: ST.Shadow<T>, +op: E.Op<T>, +g: {ST.good(T, sh) == True{} : Bool}) -> {view1(T, DA.step(T, ST.real(T, sh), op)) == S.step(T, ST.abs(T, ST.real(T, sh)), op) : S.Model<T> & E.Obs<T>}:
57 +sh2 = TR.so_sh(T, sh, op, SP.step_ok(T, sh, op, g))
58 +o = TR.so_obs(T, sh, op, SP.step_ok(T, sh, op, g))
59 %Equal.sym(DA.DynArray<&2, T> & E.Obs<T>, DA.step(T, ST.real(T, sh), op), (ST.real(T, sh2), o), TR.so_step(T, sh, op, SP.step_ok(T, sh, op, g))) : {view1(T, _) == S.step(T, ST.abs(T, ST.real(T, sh)), op) : S.Model<T> & E.Obs<T>}
60 %Equal.sym(S.Model<T>, ST.abs(T, ST.real(T, sh2)), ST.model(T, sh2), ST.abs_real(T, sh2)) : {(_, o) == S.step(T, ST.abs(T, ST.real(T, sh)), op) : S.Model<T> & E.Obs<T>}
61 %Equal.sym(S.Model<T>, ST.abs(T, ST.real(T, sh)), ST.model(T, sh), ST.abs_real(T, sh)) : {(ST.model(T, sh2), o) == S.step(T, _, op) : S.Model<T> & E.Obs<T>}
62 TR.so_spec(T, sh, op, SP.step_ok(T, sh, op, g))
63
64def step_preserves(-T: Data, +sh: ST.Shadow<T>, +op: E.Op<T>, +g: {ST.good(T, sh) == True{} : Bool}) -> ST.Inv(T, Pair.fst(DA.DynArray<&2, T>, E.Obs<T>, DA.step(T, ST.real(T, sh), op))):
65 +sh2 = TR.so_sh(T, sh, op, SP.step_ok(T, sh, op, g))
66 (sh2, (Equal.cong(DA.DynArray<&2, T> & E.Obs<T>, DA.DynArray<&2, T>, r => Pair.fst(DA.DynArray<&2, T>, E.Obs<T>, r), DA.step(T, ST.real(T, sh), op), (ST.real(T, sh2), TR.so_obs(T, sh, op, SP.step_ok(T, sh, op, g))), TR.so_step(T, sh, op, SP.step_ok(T, sh, op, g))), TR.so_good(T, sh, op, SP.step_ok(T, sh, op, g))))
67
68# ---- arbitrary finite traces from a constructor ----
69
70def run_from(-T: Data, +ops: List<&2, E.Op<T>>, +sh0: ST.Shadow<T>, +g0: {ST.good(T, sh0) == True{} : Bool}) -> {DA.run(T, ops, ST.real(T, sh0)) == (ST.real(T, TR.ro_sh(T, ops, sh0, Nil{}, TR.run_ok(T, ops, sh0, Nil{}, g0))), TR.srun_obs(T, ops, ST.model(T, sh0))) : DA.DynArray<&2, T> & List<&2, E.Obs<T>>}:
71 +sh2 = TR.ro_sh(T, ops, sh0, Nil{}, TR.run_ok(T, ops, sh0, Nil{}, g0))
72 +os = TR.srun_obs(T, ops, ST.model(T, sh0))
73 %Equal.sym(DA.DynArray<&2, T> & List<&2, E.Obs<T>>, DA.run_acc(T, ops, (ST.real(T, sh0), Nil{})), (ST.real(T, sh2), List.reverse.go(&2, E.Obs<T>, os, Nil{})), TR.ro_run(T, ops, sh0, Nil{}, TR.run_ok(T, ops, sh0, Nil{}, g0))) : {DA.finish(T, _) == (ST.real(T, sh2), os) : DA.DynArray<&2, T> & List<&2, E.Obs<T>>}
74 %Equal.sym(List<&2, E.Obs<T>>, List.reverse(&2, E.Obs<T>, List.reverse.go(&2, E.Obs<T>, os, Nil{})), os, LL.rev_rev(E.Obs<T>, os)) : {(ST.real(T, sh2), _) == (ST.real(T, sh2), os) : DA.DynArray<&2, T> & List<&2, E.Obs<T>>}
75 {==}
76
77def trace_from(-T: Data, +ops: List<&2, E.Op<T>>, +sh0: ST.Shadow<T>, +g0: {ST.good(T, sh0) == True{} : Bool}) -> {view(T, DA.run(T, ops, ST.real(T, sh0))) == S.run(T, ops, ST.model(T, sh0)) : S.Model<T> & List<&2, E.Obs<T>>}:
78 +sh2 = TR.ro_sh(T, ops, sh0, Nil{}, TR.run_ok(T, ops, sh0, Nil{}, g0))
79 +os = TR.srun_obs(T, ops, ST.model(T, sh0))
80 %Equal.sym(DA.DynArray<&2, T> & List<&2, E.Obs<T>>, DA.run(T, ops, ST.real(T, sh0)), (ST.real(T, sh2), os), run_from(T, ops, sh0, g0)) : {view(T, _) == S.run(T, ops, ST.model(T, sh0)) : S.Model<T> & List<&2, E.Obs<T>>}
81 %Equal.sym(S.Model<T>, ST.abs(T, ST.real(T, sh2)), ST.model(T, sh2), ST.abs_real(T, sh2)) : {(_, os) == S.run(T, ops, ST.model(T, sh0)) : S.Model<T> & List<&2, E.Obs<T>>}
82 %Equal.sym(S.Model<T>, ST.model(T, sh2), TR.srun_state(T, ops, ST.model(T, sh0)), TR.ro_model(T, ops, sh0, Nil{}, TR.run_ok(T, ops, sh0, Nil{}, g0))) : {(_, os) == S.run(T, ops, ST.model(T, sh0)) : S.Model<T> & List<&2, E.Obs<T>>}
83 Equal.sym(S.Model<T> & List<&2, E.Obs<T>>, S.run(T, ops, ST.model(T, sh0)), (TR.srun_state(T, ops, ST.model(T, sh0)), os), L.pair_eta(S.Model<T>, List<&2, E.Obs<T>>, S.run(T, ops, ST.model(T, sh0))))
84
85def inv_from(-T: Data, +ops: List<&2, E.Op<T>>, +sh0: ST.Shadow<T>, +g0: {ST.good(T, sh0) == True{} : Bool}) -> ST.Inv(T, Pair.fst(DA.DynArray<&2, T>, List<&2, E.Obs<T>>, DA.run(T, ops, ST.real(T, sh0)))):
86 +sh2 = TR.ro_sh(T, ops, sh0, Nil{}, TR.run_ok(T, ops, sh0, Nil{}, g0))
87 (sh2, (Equal.cong(DA.DynArray<&2, T> & List<&2, E.Obs<T>>, DA.DynArray<&2, T>, r => Pair.fst(DA.DynArray<&2, T>, List<&2, E.Obs<T>>, r), DA.run(T, ops, ST.real(T, sh0)), (ST.real(T, sh2), TR.srun_obs(T, ops, ST.model(T, sh0))), run_from(T, ops, sh0, g0)), TR.ro_good(T, ops, sh0, Nil{}, TR.run_ok(T, ops, sh0, Nil{}, g0))))
88
89# Public trace laws: every finite op list run from DA.new / DA.with_limit
90# through the actual DA.run equals the specification run, and the final
91# array satisfies the invariant.
92def trace_new(-T: Data, +ops: List<&2, E.Op<T>>) -> {view(T, DA.run(T, ops, DA.new(T))) == S.run(T, ops, S.new(T)) : S.Model<T> & List<&2, E.Obs<T>>}:
93 trace_from(T, ops, TR.initial(T), TR.new_good(T))
94
95def trace_new_inv(-T: Data, +ops: List<&2, E.Op<T>>) -> ST.Inv(T, Pair.fst(DA.DynArray<&2, T>, List<&2, E.Obs<T>>, DA.run(T, ops, DA.new(T)))):
96 inv_from(T, ops, TR.initial(T), TR.new_good(T))
97
98def trace_with_limit(-T: Data, +k: Nat, +ops: List<&2, E.Op<T>>) -> {view(T, DA.run(T, ops, DA.with_limit(T, k))) == S.run(T, ops, S.with_limit(T, k)) : S.Model<T> & List<&2, E.Obs<T>>}:
99 %with_limit_abs(T, k) : {view(T, DA.run(T, ops, DA.with_limit(T, k))) == S.run(T, ops, _) : S.Model<T> & List<&2, E.Obs<T>>}
100 trace_from(T, ops, TR.limited(T, k), limit_good(T, k))
101
102def trace_with_limit_inv(-T: Data, +k: Nat, +ops: List<&2, E.Op<T>>) -> ST.Inv(T, Pair.fst(DA.DynArray<&2, T>, List<&2, E.Obs<T>>, DA.run(T, ops, DA.with_limit(T, k)))):
103 inv_from(T, ops, TR.limited(T, k), limit_good(T, k))
104
105# ---- the executable specializations (closed element type) ----
106#
107# DA.*_at is what tests and benchmarks run (see src/dynamic_array.bend for
108# why a closed element type is required by the native backend). CL.*_eq
109# proves each specialization equal to the parametric definition, so every
110# law above holds verbatim of the executed code.
111
112def new_at_abs(~T: Data) -> {ST.abs(T, DA.new_at(~T)) == S.new(T) : S.Model<T>}:
113 %Equal.sym(DA.DynArray<&2, T>, DA.new_at(~T), DA.new(T), CL.new_eq(~T)) : {ST.abs(T, _) == S.new(T) : S.Model<T>}
114 new_abs(T)
115
116def new_at_inv(~T: Data) -> ST.Inv(T, DA.new_at(~T)):
117 %Equal.sym(DA.DynArray<&2, T>, DA.new_at(~T), DA.new(T), CL.new_eq(~T)) : ST.Inv(T, _)
118 new_inv(T)
119
120def with_limit_at_abs(~T: Data, +k: Nat) -> {ST.abs(T, DA.with_limit_at(~T, k)) == S.with_limit(T, k) : S.Model<T>}:
121 %Equal.sym(DA.DynArray<&2, T>, DA.with_limit_at(~T, k), DA.with_limit(T, k), CL.with_limit_eq(~T, k)) : {ST.abs(T, _) == S.with_limit(T, k) : S.Model<T>}
122 with_limit_abs(T, k)
123
124def step_at_refines(~T: Data, +sh: ST.Shadow<T>, +op: E.Op<T>, +g: {ST.good(T, sh) == True{} : Bool}) -> {view1(T, DA.step_at(~T, ST.real(T, sh), op)) == S.step(T, ST.abs(T, ST.real(T, sh)), op) : S.Model<T> & E.Obs<T>}:
125 %Equal.sym(DA.DynArray<&2, T> & E.Obs<T>, DA.step_at(~T, ST.real(T, sh), op), DA.step(T, ST.real(T, sh), op), CL.step_eq(~T, sh, op, g)) : {view1(T, _) == S.step(T, ST.abs(T, ST.real(T, sh)), op) : S.Model<T> & E.Obs<T>}
126 step_refines(T, sh, op, g)
127
128def step_at_preserves(~T: Data, +sh: ST.Shadow<T>, +op: E.Op<T>, +g: {ST.good(T, sh) == True{} : Bool}) -> ST.Inv(T, Pair.fst(DA.DynArray<&2, T>, E.Obs<T>, DA.step_at(~T, ST.real(T, sh), op))):
129 %Equal.sym(DA.DynArray<&2, T> & E.Obs<T>, DA.step_at(~T, ST.real(T, sh), op), DA.step(T, ST.real(T, sh), op), CL.step_eq(~T, sh, op, g)) : ST.Inv(T, Pair.fst(DA.DynArray<&2, T>, E.Obs<T>, _))
130 step_preserves(T, sh, op, g)
131
132def trace_new_at(~T: Data, +ops: List<&2, E.Op<T>>) -> {view(T, DA.run_at(~T, ops, DA.new_at(~T))) == S.run(T, ops, S.new(T)) : S.Model<T> & List<&2, E.Obs<T>>}:
133 %Equal.sym(DA.DynArray<&2, T>, DA.new_at(~T), DA.new(T), CL.new_eq(~T)) : {view(T, DA.run_at(~T, ops, _)) == S.run(T, ops, S.new(T)) : S.Model<T> & List<&2, E.Obs<T>>}
134 %Equal.sym(DA.DynArray<&2, T> & List<&2, E.Obs<T>>, DA.run_at(~T, ops, ST.real(T, TR.initial(T))), DA.run(T, ops, ST.real(T, TR.initial(T))), CL.run_eq(~T, ops, TR.initial(T), TR.new_good(T))) : {view(T, _) == S.run(T, ops, S.new(T)) : S.Model<T> & List<&2, E.Obs<T>>}
135 trace_new(T, ops)
136
137def trace_new_at_inv(~T: Data, +ops: List<&2, E.Op<T>>) -> ST.Inv(T, Pair.fst(DA.DynArray<&2, T>, List<&2, E.Obs<T>>, DA.run_at(~T, ops, DA.new_at(~T)))):
138 %Equal.sym(DA.DynArray<&2, T>, DA.new_at(~T), DA.new(T), CL.new_eq(~T)) : ST.Inv(T, Pair.fst(DA.DynArray<&2, T>, List<&2, E.Obs<T>>, DA.run_at(~T, ops, _)))
139 %Equal.sym(DA.DynArray<&2, T> & List<&2, E.Obs<T>>, DA.run_at(~T, ops, ST.real(T, TR.initial(T))), DA.run(T, ops, ST.real(T, TR.initial(T))), CL.run_eq(~T, ops, TR.initial(T), TR.new_good(T))) : ST.Inv(T, Pair.fst(DA.DynArray<&2, T>, List<&2, E.Obs<T>>, _))
140 trace_new_inv(T, ops)
141
142def trace_with_limit_at(~T: Data, +k: Nat, +ops: List<&2, E.Op<T>>) -> {view(T, DA.run_at(~T, ops, DA.with_limit_at(~T, k))) == S.run(T, ops, S.with_limit(T, k)) : S.Model<T> & List<&2, E.Obs<T>>}:
143 %Equal.sym(DA.DynArray<&2, T>, DA.with_limit_at(~T, k), DA.with_limit(T, k), CL.with_limit_eq(~T, k)) : {view(T, DA.run_at(~T, ops, _)) == S.run(T, ops, S.with_limit(T, k)) : S.Model<T> & List<&2, E.Obs<T>>}
144 %Equal.sym(DA.DynArray<&2, T> & List<&2, E.Obs<T>>, DA.run_at(~T, ops, ST.real(T, TR.limited(T, k))), DA.run(T, ops, ST.real(T, TR.limited(T, k))), CL.run_eq(~T, ops, TR.limited(T, k), limit_good(T, k))) : {view(T, _) == S.run(T, ops, S.with_limit(T, k)) : S.Model<T> & List<&2, E.Obs<T>>}
145 trace_with_limit(T, k, ops)
146
147def trace_with_limit_at_inv(~T: Data, +k: Nat, +ops: List<&2, E.Op<T>>) -> ST.Inv(T, Pair.fst(DA.DynArray<&2, T>, List<&2, E.Obs<T>>, DA.run_at(~T, ops, DA.with_limit_at(~T, k)))):
148 %Equal.sym(DA.DynArray<&2, T>, DA.with_limit_at(~T, k), DA.with_limit(T, k), CL.with_limit_eq(~T, k)) : ST.Inv(T, Pair.fst(DA.DynArray<&2, T>, List<&2, E.Obs<T>>, DA.run_at(~T, ops, _)))
149 %Equal.sym(DA.DynArray<&2, T> & List<&2, E.Obs<T>>, DA.run_at(~T, ops, ST.real(T, TR.limited(T, k))), DA.run(T, ops, ST.real(T, TR.limited(T, k))), CL.run_eq(~T, ops, TR.limited(T, k), limit_good(T, k))) : ST.Inv(T, Pair.fst(DA.DynArray<&2, T>, List<&2, E.Obs<T>>, _))
150 trace_with_limit_inv(T, k, ops)
151
152# ==== the contract of dynamic_array (stated in spec/containers/dynamic_array.bend) ====================
153
154# ---- the implementation ----
155# every Post below is a property of S.step; it holds of DA.step read back
156# through the abstraction (view1), on every good array
157def impl(-T: Data, +sh: ST.Shadow<T>, +op: E.Op<T>, +g: {ST.good(T, sh) == True{} : Bool}, -Post: (S.Model<T> & E.Obs<T>) -> Type, pf: Post(S.step(T, ST.abs(T, ST.real(T, sh)), op))) -> Post(view1(T, DA.step(T, ST.real(T, sh), op))):
158 L.subst(S.Model<T> & E.Obs<T>, Post, S.step(T, ST.abs(T, ST.real(T, sh)), op), view1(T, DA.step(T, ST.real(T, sh), op)), Equal.sym(S.Model<T> & E.Obs<T>, view1(T, DA.step(T, ST.real(T, sh), op)), S.step(T, ST.abs(T, ST.real(T, sh)), op), step_refines(T, sh, op, g)), pf)
159
160# ---- Length, Capacity, iteration: the value, and nothing changes ----
161def length_result(-T: Data, +l: Nat, +d: Nat, +xs: List<&2, T>) -> S.Length.length_result(T, l, d, xs):
162 {==}
163
164def length_frame(-T: Data, +l: Nat, +d: Nat, +xs: List<&2, T>) -> S.Length.length_frame(T, l, d, xs):
165 {==}
166
167def capacity_result(-T: Data, +l: Nat, +d: Nat, +xs: List<&2, T>) -> S.Capacity.capacity_result(T, l, d, xs):
168 {==}
169
170def capacity_frame(-T: Data, +l: Nat, +d: Nat, +xs: List<&2, T>) -> S.Capacity.capacity_frame(T, l, d, xs):
171 {==}
172
173def to_list_model(-T: Data, +l: Nat, +d: Nat, +xs: List<&2, T>) -> S.Iteration.to_list_model(T, l, d, xs):
174 {==}
175
176def to_list_frame(-T: Data, +l: Nat, +d: Nat, +xs: List<&2, T>) -> S.Iteration.to_list_frame(T, l, d, xs):
177 {==}
178
179# ---- Empty_Vector: Length 0 (the default capacity is 2^0) ----
180def new_empty(-T: Data) -> S.Empty_Vector.new_empty(T):
181 {==}
182
183def new_capacity(-T: Data) -> S.Empty_Vector.new_capacity(T):
184 {==}
185
186def new_impl(-T: Data) -> {ST.abs(T, DA.new(T)) == S.new(T) : S.Model<T>}:
187 new_abs(T)
188
189def with_limit_empty(-T: Data, +k: Nat) -> S.Empty_Vector.with_limit_empty(T, k):
190 {==}
191
192def with_limit_impl(-T: Data, +k: Nat) -> {ST.abs(T, DA.with_limit(T, k)) == S.with_limit(T, k) : S.Model<T>}:
193 with_limit_abs(T, k)
194
195# ---- Reserve_Capacity: M.Equal (Model, Model'Old) ----
196def re_c(-T: Data, +l: Nat, +d: Nat, +xs: List<&2, T>, +n: Nat, +c1: Bool, +h1: {Nat.is_le(n, SC.pow2(d)) == c1 : Bool}, +c2: Bool, +h2: {Nat.is_le(n, SC.pow2(l)) == c2 : Bool}) -> {S.items(T, S.nx(T, S.M{l, d, xs}, E.Reserve{n})) == xs : List<&2, T>}:
197 match c1 c2:
198 case True{} _:
199 %Equal.sym(Bool, Nat.is_le(n, SC.pow2(d)), True{}, h1) : {S.items(T, Pair.fst(S.Model<T>, E.Obs<T>, Bool.pick(S.Model<T> & E.Obs<T>, _, (S.M{l, d, xs}, E.OUnit{S.ok_unit()}), Bool.pick(S.Model<T> & E.Obs<T>, Nat.is_le(n, SC.pow2(l)), (S.M{l, S.fit(n, d, n), xs}, E.OUnit{S.ok_unit()}), (S.M{l, d, xs}, E.OUnit{Fail{E.CapacityExceeded{}}}))))) == xs : List<&2, T>}
200 {==}
201 case False{} True{}:
202 %Equal.sym(Bool, Nat.is_le(n, SC.pow2(d)), False{}, h1) : {S.items(T, Pair.fst(S.Model<T>, E.Obs<T>, Bool.pick(S.Model<T> & E.Obs<T>, _, (S.M{l, d, xs}, E.OUnit{S.ok_unit()}), Bool.pick(S.Model<T> & E.Obs<T>, Nat.is_le(n, SC.pow2(l)), (S.M{l, S.fit(n, d, n), xs}, E.OUnit{S.ok_unit()}), (S.M{l, d, xs}, E.OUnit{Fail{E.CapacityExceeded{}}}))))) == xs : List<&2, T>}
203 %Equal.sym(Bool, Nat.is_le(n, SC.pow2(l)), True{}, h2) : {S.items(T, Pair.fst(S.Model<T>, E.Obs<T>, Bool.pick(S.Model<T> & E.Obs<T>, False{}, (S.M{l, d, xs}, E.OUnit{S.ok_unit()}), Bool.pick(S.Model<T> & E.Obs<T>, _, (S.M{l, S.fit(n, d, n), xs}, E.OUnit{S.ok_unit()}), (S.M{l, d, xs}, E.OUnit{Fail{E.CapacityExceeded{}}}))))) == xs : List<&2, T>}
204 {==}
205 case False{} False{}:
206 %Equal.sym(Bool, Nat.is_le(n, SC.pow2(d)), False{}, h1) : {S.items(T, Pair.fst(S.Model<T>, E.Obs<T>, Bool.pick(S.Model<T> & E.Obs<T>, _, (S.M{l, d, xs}, E.OUnit{S.ok_unit()}), Bool.pick(S.Model<T> & E.Obs<T>, Nat.is_le(n, SC.pow2(l)), (S.M{l, S.fit(n, d, n), xs}, E.OUnit{S.ok_unit()}), (S.M{l, d, xs}, E.OUnit{Fail{E.CapacityExceeded{}}}))))) == xs : List<&2, T>}
207 %Equal.sym(Bool, Nat.is_le(n, SC.pow2(l)), False{}, h2) : {S.items(T, Pair.fst(S.Model<T>, E.Obs<T>, Bool.pick(S.Model<T> & E.Obs<T>, False{}, (S.M{l, d, xs}, E.OUnit{S.ok_unit()}), Bool.pick(S.Model<T> & E.Obs<T>, _, (S.M{l, S.fit(n, d, n), xs}, E.OUnit{S.ok_unit()}), (S.M{l, d, xs}, E.OUnit{Fail{E.CapacityExceeded{}}}))))) == xs : List<&2, T>}
208 {==}
209
210def reserve_equal(-T: Data, +l: Nat, +d: Nat, +xs: List<&2, T>, +n: Nat) -> S.Reserve_Capacity.reserve_equal(T, l, d, xs, n):
211 re_c(T, l, d, xs, n, Nat.is_le(n, SC.pow2(d)), {==}, Nat.is_le(n, SC.pow2(l)), {==})
212
213# ---- Clear: Length 0 (the capacity is kept) ----
214def clear_length(-T: Data, +l: Nat, +d: Nat, +xs: List<&2, T>) -> S.Clear.clear_length(T, l, d, xs):
215 {==}
216
217def clear_capacity(-T: Data, +l: Nat, +d: Nat, +xs: List<&2, T>) -> S.Clear.clear_capacity(T, l, d, xs):
218 {==}
219
220# ---- Element / First_Element / Last_Element ----
221def get_element(-T: Data, +l: Nat, +d: Nat, +xs: List<&2, T>, +i: Nat, +v: T, +h: {SC.nth(T, xs, i) == Some{v} : Maybe<&2, T>}) -> S.Element.get_element(T, l, d, xs, i, v, h):
222 %Equal.sym(Maybe<&2, T>, SC.nth(T, xs, i), Some{v}, h) : {E.OItem{S.item_result(T, _)} == E.OItem{Done{v}} : E.Obs<T>}
223 {==}
224
225def get_frame(-T: Data, +l: Nat, +d: Nat, +xs: List<&2, T>, +i: Nat) -> S.Element.get_frame(T, l, d, xs, i):
226 {==}
227
228def get_outside(-T: Data, +l: Nat, +d: Nat, +xs: List<&2, T>, +i: Nat, +h: {Nat.is_le(SC.length(T, xs), i) == True{} : Bool}) -> S.Element.get_outside(T, l, d, xs, i, h):
229 %Equal.sym(Maybe<&2, T>, SC.nth(T, xs, i), None{}, LL.nth_none(T, xs, i, h)) : {E.OItem{S.item_result(T, _)} == E.OItem{Fail{E.IndexOutOfRange{}}} : E.Obs<T>}
230 {==}
231
232def first_element(-T: Data, +l: Nat, +d: Nat, +h: T, +t: List<&2, T>) -> S.First_Element.first_element(T, l, d, h, t):
233 {==}
234
235def last_element(-T: Data, +l: Nat, +d: Nat, +xs: List<&2, T>) -> S.Last_Element.last_element(T, l, d, xs):
236 {==}
237
238# ---- Replace_Element: Length kept, Element (Index) = New_Item, Equal_Except elsewhere ----
239def set_step(-T: Data, +l: Nat, +d: Nat, +xs: List<&2, T>, +i: Nat, +v: T, +h: {Nat.is_lt(i, SC.length(T, xs)) == True{} : Bool}) -> {S.step(T, S.M{l, d, xs}, E.Set{i, v}) == (S.M{l, d, SC.update(T, xs, i, v)}, E.OUnit{Done{Unit{}}}) : S.Model<T> & E.Obs<T>}:
240 %Equal.sym(Bool, Nat.is_lt(i, SC.length(T, xs)), True{}, h) : {Bool.pick(S.Model<T> & E.Obs<T>, _, (S.M{l, d, SC.update(T, xs, i, v)}, E.OUnit{S.ok_unit()}), (S.M{l, d, xs}, E.OUnit{Fail{E.IndexOutOfRange{}}})) == (S.M{l, d, SC.update(T, xs, i, v)}, E.OUnit{Done{Unit{}}}) : S.Model<T> & E.Obs<T>}
241 {==}
242
243def set_items(-T: Data, +l: Nat, +d: Nat, +xs: List<&2, T>, +i: Nat, +v: T, +h: {Nat.is_lt(i, SC.length(T, xs)) == True{} : Bool}) -> {S.items(T, S.nx(T, S.M{l, d, xs}, E.Set{i, v})) == SC.update(T, xs, i, v) : List<&2, T>}:
244 %Equal.sym(S.Model<T> & E.Obs<T>, S.step(T, S.M{l, d, xs}, E.Set{i, v}), (S.M{l, d, SC.update(T, xs, i, v)}, E.OUnit{Done{Unit{}}}), set_step(T, l, d, xs, i, v, h)) : {S.items(T, Pair.fst(S.Model<T>, E.Obs<T>, _)) == SC.update(T, xs, i, v) : List<&2, T>}
245 {==}
246
247def set_length(-T: Data, +l: Nat, +d: Nat, +xs: List<&2, T>, +i: Nat, +v: T, +h: {Nat.is_lt(i, SC.length(T, xs)) == True{} : Bool}) -> S.Replace_Element.set_length(T, l, d, xs, i, v, h):
248 %Equal.sym(List<&2, T>, S.items(T, S.nx(T, S.M{l, d, xs}, E.Set{i, v})), SC.update(T, xs, i, v), set_items(T, l, d, xs, i, v, h)) : {SC.length(T, _) == SC.length(T, xs) : Nat}
249 VL.update_length(T, xs, i, v)
250
251def set_element(-T: Data, +l: Nat, +d: Nat, +xs: List<&2, T>, +i: Nat, +v: T, +h: {Nat.is_lt(i, SC.length(T, xs)) == True{} : Bool}) -> S.Replace_Element.set_element(T, l, d, xs, i, v, h):
252 %Equal.sym(List<&2, T>, S.items(T, S.nx(T, S.M{l, d, xs}, E.Set{i, v})), SC.update(T, xs, i, v), set_items(T, l, d, xs, i, v, h)) : {SC.nth(T, _, i) == Some{v} : Maybe<&2, T>}
253 VL.update_at(T, xs, i, v, h)
254
255def set_except(-T: Data, +l: Nat, +d: Nat, +xs: List<&2, T>, +i: Nat, +v: T, +h: {Nat.is_lt(i, SC.length(T, xs)) == True{} : Bool}) -> S.Replace_Element.set_except(T, l, d, xs, i, v, h):
256 L.subst(List<&2, T>, z => V.EqualExcept(T, xs, z, i), SC.update(T, xs, i, v), S.items(T, S.nx(T, S.M{l, d, xs}, E.Set{i, v})), Equal.sym(List<&2, T>, S.items(T, S.nx(T, S.M{l, d, xs}, E.Set{i, v})), SC.update(T, xs, i, v), set_items(T, l, d, xs, i, v, h)), VL.update_except(T, xs, i, v))
257
258def set_outside(-T: Data, +l: Nat, +d: Nat, +xs: List<&2, T>, +i: Nat, +v: T, +h: {Nat.is_lt(i, SC.length(T, xs)) == False{} : Bool}) -> S.Replace_Element.set_outside(T, l, d, xs, i, v, h):
259 %Equal.sym(Bool, Nat.is_lt(i, SC.length(T, xs)), False{}, h) : {Bool.pick(S.Model<T> & E.Obs<T>, _, (S.M{l, d, SC.update(T, xs, i, v)}, E.OUnit{S.ok_unit()}), (S.M{l, d, xs}, E.OUnit{Fail{E.IndexOutOfRange{}}})) == (S.M{l, d, xs}, E.OUnit{Fail{E.IndexOutOfRange{}}}) : S.Model<T> & E.Obs<T>}
260 {==}
261
262def pi_c(-T: Data, +l: Nat, +d: Nat, +xs: List<&2, T>, +v: T, +c1: Bool, +h1: {Nat.is_lt(SC.length(T, xs), SC.pow2(d)) == c1 : Bool}, +c2: Bool, +h2: {Nat.is_lt(d, l) == c2 : Bool}, +hr: {Bool.or(c1, c2) == True{} : Bool}) -> {S.items(T, S.nx(T, S.M{l, d, xs}, E.Push{v})) == SC.snoc(T, xs, v) : List<&2, T>}:
263 match c1 c2:
264 case True{} _:
265 %Equal.sym(Bool, Nat.is_lt(SC.length(T, xs), SC.pow2(d)), True{}, h1) : {S.items(T, Pair.fst(S.Model<T>, E.Obs<T>, Bool.pick(S.Model<T> & E.Obs<T>, _, (S.M{l, d, SC.snoc(T, xs, v)}, E.OUnit{S.ok_unit()}), Bool.pick(S.Model<T> & E.Obs<T>, Nat.is_lt(d, l), (S.M{l, 1n+d, SC.snoc(T, xs, v)}, E.OUnit{S.ok_unit()}), (S.M{l, d, xs}, E.OUnit{Fail{E.CapacityExceeded{}}}))))) == SC.snoc(T, xs, v) : List<&2, T>}
266 {==}
267 case False{} True{}:
268 %Equal.sym(Bool, Nat.is_lt(SC.length(T, xs), SC.pow2(d)), False{}, h1) : {S.items(T, Pair.fst(S.Model<T>, E.Obs<T>, Bool.pick(S.Model<T> & E.Obs<T>, _, (S.M{l, d, SC.snoc(T, xs, v)}, E.OUnit{S.ok_unit()}), Bool.pick(S.Model<T> & E.Obs<T>, Nat.is_lt(d, l), (S.M{l, 1n+d, SC.snoc(T, xs, v)}, E.OUnit{S.ok_unit()}), (S.M{l, d, xs}, E.OUnit{Fail{E.CapacityExceeded{}}}))))) == SC.snoc(T, xs, v) : List<&2, T>}
269 %Equal.sym(Bool, Nat.is_lt(d, l), True{}, h2) : {S.items(T, Pair.fst(S.Model<T>, E.Obs<T>, Bool.pick(S.Model<T> & E.Obs<T>, False{}, (S.M{l, d, SC.snoc(T, xs, v)}, E.OUnit{S.ok_unit()}), Bool.pick(S.Model<T> & E.Obs<T>, _, (S.M{l, 1n+d, SC.snoc(T, xs, v)}, E.OUnit{S.ok_unit()}), (S.M{l, d, xs}, E.OUnit{Fail{E.CapacityExceeded{}}}))))) == SC.snoc(T, xs, v) : List<&2, T>}
270 {==}
271 case False{} False{}:
272 Empty.absurd({S.items(T, S.nx(T, S.M{l, d, xs}, E.Push{v})) == SC.snoc(T, xs, v) : List<&2, T>}, L.false_true(hr))
273
274def push_items(-T: Data, +l: Nat, +d: Nat, +xs: List<&2, T>, +v: T, +hr: {S.room(T, l, d, xs) == True{} : Bool}) -> {S.items(T, S.nx(T, S.M{l, d, xs}, E.Push{v})) == SC.snoc(T, xs, v) : List<&2, T>}:
275 pi_c(T, l, d, xs, v, Nat.is_lt(SC.length(T, xs), SC.pow2(d)), {==}, Nat.is_lt(d, l), {==}, hr)
276
277def push_length(-T: Data, +l: Nat, +d: Nat, +xs: List<&2, T>, +v: T, +hr: {S.room(T, l, d, xs) == True{} : Bool}) -> S.Append.push_length(T, l, d, xs, v, hr):
278 %Equal.sym(List<&2, T>, S.items(T, S.nx(T, S.M{l, d, xs}, E.Push{v})), SC.snoc(T, xs, v), push_items(T, l, d, xs, v, hr)) : {SC.length(T, _) == 1n+SC.length(T, xs) : Nat}
279 VL.snoc_length(T, xs, v)
280
281def push_prefix(-T: Data, +l: Nat, +d: Nat, +xs: List<&2, T>, +v: T, +hr: {S.room(T, l, d, xs) == True{} : Bool}) -> S.Append.push_prefix(T, l, d, xs, v, hr):
282 L.subst(List<&2, T>, z => V.EqualPrefix(T, xs, z), SC.snoc(T, xs, v), S.items(T, S.nx(T, S.M{l, d, xs}, E.Push{v})), Equal.sym(List<&2, T>, S.items(T, S.nx(T, S.M{l, d, xs}, E.Push{v})), SC.snoc(T, xs, v), push_items(T, l, d, xs, v, hr)), VL.snoc_prefix(T, xs, v))
283
284def push_element(-T: Data, +l: Nat, +d: Nat, +xs: List<&2, T>, +v: T, +hr: {S.room(T, l, d, xs) == True{} : Bool}) -> S.Append.push_element(T, l, d, xs, v, hr):
285 %Equal.sym(List<&2, T>, S.items(T, S.nx(T, S.M{l, d, xs}, E.Push{v})), SC.snoc(T, xs, v), push_items(T, l, d, xs, v, hr)) : {SC.nth(T, _, SC.length(T, xs)) == Some{v} : Maybe<&2, T>}
286 VL.snoc_last(T, xs, v)
287
288def push_full(-T: Data, +l: Nat, +d: Nat, +xs: List<&2, T>, +v: T, +h1: {Nat.is_lt(SC.length(T, xs), SC.pow2(d)) == False{} : Bool}, +h2: {Nat.is_lt(d, l) == False{} : Bool}) -> S.Append.push_full(T, l, d, xs, v, h1, h2):
289 %Equal.sym(Bool, Nat.is_lt(SC.length(T, xs), SC.pow2(d)), False{}, h1) : {Bool.pick(S.Model<T> & E.Obs<T>, _, (S.M{l, d, SC.snoc(T, xs, v)}, E.OUnit{S.ok_unit()}), Bool.pick(S.Model<T> & E.Obs<T>, Nat.is_lt(d, l), (S.M{l, 1n+d, SC.snoc(T, xs, v)}, E.OUnit{S.ok_unit()}), (S.M{l, d, xs}, E.OUnit{Fail{E.CapacityExceeded{}}}))) == (S.M{l, d, xs}, E.OUnit{Fail{E.CapacityExceeded{}}}) : S.Model<T> & E.Obs<T>}
290 %Equal.sym(Bool, Nat.is_lt(d, l), False{}, h2) : {Bool.pick(S.Model<T> & E.Obs<T>, False{}, (S.M{l, d, SC.snoc(T, xs, v)}, E.OUnit{S.ok_unit()}), Bool.pick(S.Model<T> & E.Obs<T>, _, (S.M{l, 1n+d, SC.snoc(T, xs, v)}, E.OUnit{S.ok_unit()}), (S.M{l, d, xs}, E.OUnit{Fail{E.CapacityExceeded{}}}))) == (S.M{l, d, xs}, E.OUnit{Fail{E.CapacityExceeded{}}}) : S.Model<T> & E.Obs<T>}
291 {==}
292
293# ---- Delete_Last: Length - 1, Equal_Prefix (Model, Model'Old); pop returns Last_Element'Old ----
294def pop_length(-T: Data, +l: Nat, +d: Nat, +h: T, +t: List<&2, T>) -> S.Delete_Last.pop_length(T, l, d, h, t):
295 VL.init_length(T, t, h)
296
297def pop_prefix(-T: Data, +l: Nat, +d: Nat, +h: T, +t: List<&2, T>) -> S.Delete_Last.pop_prefix(T, l, d, h, t):
298 VL.init_prefix(T, t, h)
299
300def pop_result(-T: Data, +l: Nat, +d: Nat, +h: T, +t: List<&2, T>) -> S.Delete_Last.pop_result(T, l, d, h, t):
301 %Equal.sym(Maybe<&2, T>, SC.last(T, Con{h, t}), V.last_elem(T, Con{h, t}), VL.last_is_elem(T, t, h)) : {E.OItem{S.item_result(T, _)} == E.OItem{S.item_result(T, V.last_elem(T, Con{h, t}))} : E.Obs<T>}
302 {==}
303
304def pop_empty(-T: Data, +l: Nat, +d: Nat) -> S.Delete_Last.pop_empty(T, l, d):
305 {==}