proofs/containers/bitlist/proof.bend
bend-collections-laws-containers@1.0.0.0 · 273 lines · 0 definitions
1import Base
2import bend-collections-laws-containers@1.0.0.0/spec/lib/common.bend as SC
3import bend-collections-laws-containers@1.0.0.0/src/containers/bitlist.bend as BLI
4import bend-collections-laws-containers@1.0.0.0/src/containers/types/bitlist.bend as E
5import bend-collections-laws-containers@1.0.0.0/spec/containers/bitlist.bend as S
6import bend-collections-laws-containers@1.0.0.0/proofs/containers/bitlist/state.bend as SS
7import bend-collections-laws-containers@1.0.0.0/proofs/containers/bitlist/steps.bend as BS
8import bend-collections-laws-containers@1.0.0.0/proofs/containers/bitlist/trace.bend as TR
9import bend-collections-laws-containers@1.0.0.0/proofs/lib/list.bend as LL
10import bend-collections-laws-containers@1.0.0.0/proofs/containers/bitset/lists.bend as BL
11import bend-collections-laws-containers@1.0.0.0/proofs/lib/logic.bend as L
12import bend-collections-laws-containers@1.0.0.0/proofs/lib/nat.bend as N
13import bend-collections-laws-containers@1.0.0.0/spec/lib/sequence.bend as V
14import bend-collections-laws-containers@1.0.0.0/proofs/lib/sequence.bend as VL
15
16# ==== the contract of bitlist (stated in spec/containers/bitlist.bend) ====================
17
18# ---- assign: the written bit reads back, every other bit is unchanged ----
19def assign_in(+l: Maybe<&2, Nat>, +c: Nat, +xs: List<&2, Bool>, +i: Nat, +v: Bool, +h: {Nat.is_lt(i, SC.length(Bool, xs)) == True{} : Bool}, +y: Maybe<&2, Bool>, +hy: {SC.nth(Bool, xs, i) == y : Maybe<&2, Bool>}) -> {S.assign_at(y, l, c, xs, i, v) == (S.M{l, c, SC.update(Bool, xs, i, v)}, E.OUnit{Done{Unit{}}}) : S.Model & E.Obs}:
20 match y:
21 case None{}:
22 Empty.absurd({S.assign_at(None{}, l, c, xs, i, v) == (S.M{l, c, SC.update(Bool, xs, i, v)}, E.OUnit{Done{Unit{}}}) : S.Model & E.Obs}, LL.sc_nth_some(Bool, xs, i, h, hy))
23 case Some{b}:
24 {==}
25
26def assign_step(+l: Maybe<&2, Nat>, +c: Nat, +xs: List<&2, Bool>, +i: Nat, +v: Bool, +h: {Nat.is_lt(i, SC.length(Bool, xs)) == True{} : Bool}) -> {S.step(S.M{l, c, xs}, E.Assign{i, v}) == (S.M{l, c, SC.update(Bool, xs, i, v)}, E.OUnit{Done{Unit{}}}) : S.Model & E.Obs}:
27 assign_in(l, c, xs, i, v, h, SC.nth(Bool, xs, i), {==})
28
29def get_assign_same(+l: Maybe<&2, Nat>, +c: Nat, +xs: List<&2, Bool>, +i: Nat, +v: Bool, +h: {Nat.is_lt(i, SC.length(Bool, xs)) == True{} : Bool}) -> S.Replace_Element.get_assign_same(l, c, xs, i, v, h):
30 %Equal.sym(S.Model & E.Obs, S.step(S.M{l, c, xs}, E.Assign{i, v}), (S.M{l, c, SC.update(Bool, xs, i, v)}, E.OUnit{Done{Unit{}}}), assign_step(l, c, xs, i, v, h)) : {Pair.snd(S.Model, E.Obs, S.step(Pair.fst(S.Model, E.Obs, _), E.Get{i})) == E.OBit{Done{v}} : E.Obs}
31 %Equal.sym(Maybe<&2, Bool>, SC.nth(Bool, SC.update(Bool, xs, i, v), i), Some{v}, LL.nth_update_same(Bool, xs, i, v, h)) : {E.OBit{S.bit(_)} == E.OBit{Done{v}} : E.Obs}
32 {==}
33
34def get_assign_other(+l: Maybe<&2, Nat>, +c: Nat, +xs: List<&2, Bool>, +i: Nat, +j: Nat, +v: Bool, +h: {Nat.is_lt(i, SC.length(Bool, xs)) == True{} : Bool}, +ne: {Nat.is_eq(i, j) == False{} : Bool}) -> S.Replace_Element.get_assign_other(l, c, xs, i, j, v, h, ne):
35 %Equal.sym(S.Model & E.Obs, S.step(S.M{l, c, xs}, E.Assign{i, v}), (S.M{l, c, SC.update(Bool, xs, i, v)}, E.OUnit{Done{Unit{}}}), assign_step(l, c, xs, i, v, h)) : {Pair.snd(S.Model, E.Obs, S.step(Pair.fst(S.Model, E.Obs, _), E.Get{j})) == E.OBit{S.bit(SC.nth(Bool, xs, j))} : E.Obs}
36 %Equal.sym(Maybe<&2, Bool>, SC.nth(Bool, SC.update(Bool, xs, i, v), j), SC.nth(Bool, xs, j), LL.nth_update_other(Bool, xs, i, j, v, ne)) : {E.OBit{S.bit(_)} == E.OBit{S.bit(SC.nth(Bool, xs, j))} : E.Obs}
37 {==}
38
39def length_assign(+l: Maybe<&2, Nat>, +c: Nat, +xs: List<&2, Bool>, +i: Nat, +v: Bool, +h: {Nat.is_lt(i, SC.length(Bool, xs)) == True{} : Bool}) -> S.Replace_Element.length_assign(l, c, xs, i, v, h):
40 %Equal.sym(S.Model & E.Obs, S.step(S.M{l, c, xs}, E.Assign{i, v}), (S.M{l, c, SC.update(Bool, xs, i, v)}, E.OUnit{Done{Unit{}}}), assign_step(l, c, xs, i, v, h)) : {SC.length(Bool, S.bits(Pair.fst(S.Model, E.Obs, _))) == SC.length(Bool, xs) : Nat}
41 LL.length_update(Bool, xs, i, v)
42
43def nth_snoc_end(+xs: List<&2, Bool>, +v: Bool) -> {SC.nth(Bool, SC.snoc(Bool, xs, v), SC.length(Bool, xs)) == Some{v} : Maybe<&2, Bool>}:
44 match xs:
45 case Nil{}:
46 {==}
47 case Con{+h, +t}:
48 nth_snoc_end(t, v)
49
50def pop_snoc(+l: Maybe<&2, Nat>, +c: Nat, +ys: List<&2, Bool>, +b: Bool) -> {S.pop(l, c, SC.snoc(Bool, ys, b)) == (S.M{l, c, ys}, E.OBit{Done{b}}) : S.Model & E.Obs}:
51 match ys:
52 case Nil{}:
53 {==}
54 case Con{+h, +t}:
55 %Equal.sym(List<&2, Bool>, SC.init(Bool, SC.snoc(Bool, Con{h, t}, b)), Con{h, t}, LL.init_snoc(Bool, Con{h, t}, b)) : {(S.M{l, c, _}, E.OBit{S.last_bit(SC.last(Bool, SC.snoc(Bool, Con{h, t}, b)))}) == (S.M{l, c, Con{h, t}}, E.OBit{Done{b}}) : S.Model & E.Obs}
56 %Equal.sym(Maybe<&2, Bool>, SC.last(Bool, SC.snoc(Bool, Con{h, t}, b)), Some{b}, LL.last_snoc(Bool, Con{h, t}, b)) : {(S.M{l, c, Con{h, t}}, E.OBit{S.last_bit(_)}) == (S.M{l, c, Con{h, t}}, E.OBit{Done{b}}) : S.Model & E.Obs}
57 {==}
58
59# ---- push / pop: append one bit, pop returns it and restores the list ----
60def push_step(+l: Maybe<&2, Nat>, +c: Nat, +xs: List<&2, Bool>, +v: Bool, +h: {S.room(l, c, SC.length(Bool, xs)) == True{} : Bool}) -> {S.step(S.M{l, c, xs}, E.Push{v}) == (S.M{l, c, SC.snoc(Bool, xs, v)}, E.OUnit{Done{Unit{}}}) : S.Model & E.Obs}:
61 %Equal.sym(Bool, S.room(l, c, SC.length(Bool, xs)), True{}, h) : {S.push_if(_, l, c, xs, v) == (S.M{l, c, SC.snoc(Bool, xs, v)}, E.OUnit{Done{Unit{}}}) : S.Model & E.Obs}
62 {==}
63
64def length_push(+l: Maybe<&2, Nat>, +c: Nat, +xs: List<&2, Bool>, +v: Bool, +h: {S.room(l, c, SC.length(Bool, xs)) == True{} : Bool}) -> S.Append.length_push(l, c, xs, v, h):
65 %Equal.sym(S.Model & E.Obs, S.step(S.M{l, c, xs}, E.Push{v}), (S.M{l, c, SC.snoc(Bool, xs, v)}, E.OUnit{Done{Unit{}}}), push_step(l, c, xs, v, h)) : {SC.length(Bool, S.bits(Pair.fst(S.Model, E.Obs, _))) == 1n+SC.length(Bool, xs) : Nat}
66 LL.length_snoc(Bool, xs, v)
67
68def get_push_last(+l: Maybe<&2, Nat>, +c: Nat, +xs: List<&2, Bool>, +v: Bool, +h: {S.room(l, c, SC.length(Bool, xs)) == True{} : Bool}) -> S.Append.get_push_last(l, c, xs, v, h):
69 %Equal.sym(S.Model & E.Obs, S.step(S.M{l, c, xs}, E.Push{v}), (S.M{l, c, SC.snoc(Bool, xs, v)}, E.OUnit{Done{Unit{}}}), push_step(l, c, xs, v, h)) : {Pair.snd(S.Model, E.Obs, S.step(Pair.fst(S.Model, E.Obs, _), E.Get{SC.length(Bool, xs)})) == E.OBit{Done{v}} : E.Obs}
70 %Equal.sym(Maybe<&2, Bool>, SC.nth(Bool, SC.snoc(Bool, xs, v), SC.length(Bool, xs)), Some{v}, nth_snoc_end(xs, v)) : {E.OBit{S.bit(_)} == E.OBit{Done{v}} : E.Obs}
71 {==}
72
73def pop_push(+l: Maybe<&2, Nat>, +c: Nat, +xs: List<&2, Bool>, +v: Bool, +h: {S.room(l, c, SC.length(Bool, xs)) == True{} : Bool}) -> S.Delete_Last.pop_push(l, c, xs, v, h):
74 %Equal.sym(S.Model & E.Obs, S.step(S.M{l, c, xs}, E.Push{v}), (S.M{l, c, SC.snoc(Bool, xs, v)}, E.OUnit{Done{Unit{}}}), push_step(l, c, xs, v, h)) : {S.step(Pair.fst(S.Model, E.Obs, _), E.Pop{}) == (S.M{l, c, xs}, E.OBit{Done{v}}) : S.Model & E.Obs}
75 pop_snoc(l, c, xs, v)
76
77def count_push(+l: Maybe<&2, Nat>, +c: Nat, +xs: List<&2, Bool>, +v: Bool, +h: {S.room(l, c, SC.length(Bool, xs)) == True{} : Bool}) -> S.Append.count_push(l, c, xs, v, h):
78 %Equal.sym(S.Model & E.Obs, S.step(S.M{l, c, xs}, E.Push{v}), (S.M{l, c, SC.snoc(Bool, xs, v)}, E.OUnit{Done{Unit{}}}), push_step(l, c, xs, v, h)) : {S.count(S.bits(Pair.fst(S.Model, E.Obs, _))) == Nat.add(S.count(xs), S.count(Con{v, Nil{}})) : Nat}
79 %Equal.sym(List<&2, Bool>, SC.snoc(Bool, xs, v), SC.append(Bool, xs, Con{v, Nil{}}), LL.snoc_append(Bool, xs, v)) : {S.count(_) == Nat.add(S.count(xs), S.count(Con{v, Nil{}})) : Nat}
80 BL.count_append(xs, Con{v, Nil{}})
81
82# ---- from_bools spells its input ----
83def room_of(+c: Nat, +xs: List<&2, Bool>, +b: Bool, +t: List<&2, Bool>, +h: {Nat.is_le(Nat.add(SC.length(Bool, xs), SC.length(Bool, Con{b, t})), Nat.mul(SC.pow2(c), 32n)) == True{} : Bool}) -> {S.room(None{}, c, SC.length(Bool, xs)) == True{} : Bool}:
84 +h1 = L.subst(Nat, z => {Nat.is_le(z, Nat.mul(SC.pow2(c), 32n)) == True{} : Bool}, Nat.add(SC.length(Bool, xs), 1n+SC.length(Bool, t)), 1n+Nat.add(SC.length(Bool, xs), SC.length(Bool, t)), N.add_succ(SC.length(Bool, xs), SC.length(Bool, t)), h)
85 N.lt_le_trans(SC.length(Bool, xs), 1n+Nat.add(SC.length(Bool, xs), SC.length(Bool, t)), Nat.mul(SC.pow2(c), 32n), N.le_lt_succ(SC.length(Bool, xs), Nat.add(SC.length(Bool, xs), SC.length(Bool, t)), N.le_add_right(SC.length(Bool, xs), SC.length(Bool, t))), h1)
86
87def fits_tail(+c: Nat, +xs: List<&2, Bool>, +b: Bool, +t: List<&2, Bool>, +h: {Nat.is_le(Nat.add(SC.length(Bool, xs), SC.length(Bool, Con{b, t})), Nat.mul(SC.pow2(c), 32n)) == True{} : Bool}) -> {Nat.is_le(Nat.add(SC.length(Bool, SC.snoc(Bool, xs, b)), SC.length(Bool, t)), Nat.mul(SC.pow2(c), 32n)) == True{} : Bool}:
88 %Equal.sym(Nat, SC.length(Bool, SC.snoc(Bool, xs, b)), 1n+SC.length(Bool, xs), LL.length_snoc(Bool, xs, b)) : {Nat.is_le(Nat.add(_, SC.length(Bool, t)), Nat.mul(SC.pow2(c), 32n)) == True{} : Bool}
89 L.subst(Nat, z => {Nat.is_le(z, Nat.mul(SC.pow2(c), 32n)) == True{} : Bool}, Nat.add(SC.length(Bool, xs), 1n+SC.length(Bool, t)), 1n+Nat.add(SC.length(Bool, xs), SC.length(Bool, t)), N.add_succ(SC.length(Bool, xs), SC.length(Bool, t)), h)
90
91def push_all_spells(+bs: List<&2, Bool>, +c: Nat, +xs: List<&2, Bool>, +h: {Nat.is_le(Nat.add(SC.length(Bool, xs), SC.length(Bool, bs)), Nat.mul(SC.pow2(c), 32n)) == True{} : Bool}) -> {S.push_all(bs, S.M{None{}, c, xs}) == S.M{None{}, c, SC.append(Bool, xs, bs)} : S.Model}:
92 match bs:
93 case Nil{}:
94 Equal.sym(S.Model, S.M{None{}, c, SC.append(Bool, xs, Nil{})}, S.M{None{}, c, xs}, Equal.cong(List<&2, Bool>, S.Model, z => S.M{None{}, c, z}, SC.append(Bool, xs, Nil{}), xs, LL.append_nil(Bool, xs)))
95 case Con{+b, +t}:
96 %Equal.sym(S.Model & E.Obs, S.step(S.M{None{}, c, xs}, E.Push{b}), (S.M{None{}, c, SC.snoc(Bool, xs, b)}, E.OUnit{Done{Unit{}}}), push_step(None{}, c, xs, b, room_of(c, xs, b, t, h))) : {S.push_all(t, Pair.fst(S.Model, E.Obs, _)) == S.M{None{}, c, SC.append(Bool, xs, Con{b, t})} : S.Model}
97 %Equal.sym(List<&2, Bool>, SC.append(Bool, xs, Con{b, t}), SC.append(Bool, SC.snoc(Bool, xs, b), t), Equal.sym(List<&2, Bool>, SC.append(Bool, SC.snoc(Bool, xs, b), t), SC.append(Bool, xs, Con{b, t}), LL.snoc_append_cons(Bool, xs, b, t))) : {S.push_all(t, S.M{None{}, c, SC.snoc(Bool, xs, b)}) == S.M{None{}, c, _} : S.Model}
98 push_all_spells(t, c, SC.snoc(Bool, xs, b), fits_tail(c, xs, b, t, h))
99
100
101# Packed bit list (SSZ Bitlist[N]): public proof entry point.
102# specification S.* (a list of Booleans, an optional maximum length and
103# the storage capacity exponent;
104# spec/containers/bitlist.bend)
105# abstraction SS.model(BSh{limit, len, w}) = the first len stored bits
106# invariant SS.good: the word array is a good dynamic array, it holds
107# at least len bits, and every stored bit from len on is
108# zero (the masked tail)
109# word array used only through the proved dynamic-array contract
110# (proofs/containers/dynamic_array), see da.bend
111# operations BS.step_ok: every operation (errors included) refines
112# S.step and keeps the invariant
113# traces trace_new / trace_with_limit: arbitrary finite op lists
114# from_bools builds the unbounded list whose bits are its input
115# contracts *: assign reads back and frames the other bits; push
116# grows the length by one, reads back at the end, and pop
117# undoes it; count adds the pushed bit
118#
119# Specification shape after: ConsenSys eth2.0-dafny SSZ Bitlist
120# (src/dafny/ssz/BitListSeDes.dfy), Lean 4 List Bool / BitVec lemmas
121# (Init.Data.BitVec.Lemmas, List.getElem_set), SPARK Ada Formal_Vectors
122# postconditions.
123
124def new_real() -> {BLI.new() == SS.real(TR.initial(None{})) : BLI.Bitlist}:
125 TR.new_real()
126
127def new_model() -> {SS.model(TR.initial(None{})) == S.new() : S.Model}:
128 TR.new_model()
129
130def with_limit_real(+n: Nat) -> {BLI.with_limit(n) == SS.real(TR.initial(Some{n})) : BLI.Bitlist}:
131 TR.with_limit_real(n)
132
133def with_limit_model(+n: Nat) -> {SS.model(TR.initial(Some{n})) == S.with_limit(n) : S.Model}:
134 TR.with_limit_model(n)
135
136def initial_good(+l: Maybe<&2, Nat>) -> {SS.good(TR.initial(l)) == True{} : Bool}:
137 TR.initial_good(l)
138
139def step_ok(+sh: SS.Sh, +op: E.Op, +g: {SS.good(sh) == True{} : Bool}) -> BS.StepOK(sh, op):
140 BS.step_ok(sh, op, g)
141
142def trace_new(+ops: List<&2, E.Op>) -> TR.TraceOK(ops, TR.initial(None{})):
143 TR.trace_from(ops, TR.initial(None{}), TR.initial_good(None{}))
144
145def trace_with_limit(+n: Nat, +ops: List<&2, E.Op>) -> TR.TraceOK(ops, TR.initial(Some{n})):
146 TR.trace_from(ops, TR.initial(Some{n}), TR.initial_good(Some{n}))
147
148def from_bools(+bs: List<&2, Bool>) -> TR.FromOK(bs, TR.initial(None{})):
149 TR.from_bools_ok(bs)
150
151# with room for every bit, the spec's from_bools is exactly the input
152def from_bools_spells(+bs: List<&2, Bool>, +c: Nat, +hc: {c == 31n : Nat}, +h: {Nat.is_le(SC.length(Bool, bs), Nat.mul(SC.pow2(c), 32n)) == True{} : Bool}) -> {S.push_all(bs, S.M{None{}, c, Nil{}}) == S.M{None{}, c, bs} : S.Model}:
153 push_all_spells(bs, c, Nil{}, h)
154
155# ==== the contract of bitlist (stated in spec/containers/bitlist.bend) ====================
156
157# ---- the implementation ----
158def Impl(sh: SS.Sh, op: E.Op, Post: (S.Model & E.Obs) -> Type) -> Type:
159 Sigma<&1, &1, SS.Sh, sh2 => Sigma<&1, &1, E.Obs, o => {BLI.step(SS.real(sh), op) == (SS.real(sh2), o) : BLI.Bitlist & E.Obs} & ({SS.good(sh2) == True{} : Bool} & Post((SS.model(sh2), o)))>>
160
161def impl_of(-sh: SS.Sh, -op: E.Op, -Post: (S.Model & E.Obs) -> Type, k: BS.StepOK(sh, op), pf: Post(S.step(SS.model(sh), op))) -> Impl(sh, op, Post):
162 match k:
163 case Tuple{sh2, Tuple{o, Tuple{e1, Tuple{g2, e2}}}}:
164 (sh2, (o, (e1, (g2, L.subst(S.Model & E.Obs, Post, S.step(SS.model(sh), op), (SS.model(sh2), o), Equal.sym(S.Model & E.Obs, (SS.model(sh2), o), S.step(SS.model(sh), op), e2), pf)))))
165
166def impl(+sh: SS.Sh, +op: E.Op, +g: {SS.good(sh) == True{} : Bool}, -Post: (S.Model & E.Obs) -> Type, pf: Post(S.step(SS.model(sh), op))) -> Impl(sh, op, Post):
167 impl_of(sh, op, Post, step_ok(sh, op, g), pf)
168
169# ---- Length, Capacity (the S.limit), Count, iteration: the value, and nothing changes ----
170def length_result(+l: Maybe<&2, Nat>, +c: Nat, +xs: List<&2, Bool>) -> S.Length.length_result(l, c, xs):
171 {==}
172
173def length_frame(+l: Maybe<&2, Nat>, +c: Nat, +xs: List<&2, Bool>) -> S.Length.length_frame(l, c, xs):
174 {==}
175
176def limit_result(+l: Maybe<&2, Nat>, +c: Nat, +xs: List<&2, Bool>) -> S.Capacity.limit_result(l, c, xs):
177 {==}
178
179def limit_frame(+l: Maybe<&2, Nat>, +c: Nat, +xs: List<&2, Bool>) -> S.Capacity.limit_frame(l, c, xs):
180 {==}
181
182def count_result(+l: Maybe<&2, Nat>, +c: Nat, +xs: List<&2, Bool>) -> S.Implementation.count_result(l, c, xs):
183 {==}
184
185def to_list_model(+l: Maybe<&2, Nat>, +c: Nat, +xs: List<&2, Bool>) -> S.Iteration.to_list_model(l, c, xs):
186 {==}
187
188def to_list_frame(+l: Maybe<&2, Nat>, +c: Nat, +xs: List<&2, Bool>) -> S.Iteration.to_list_frame(l, c, xs):
189 {==}
190
191# ---- Empty_Vector, To_Vector ----
192def new_empty() -> S.Empty_Vector.new_empty():
193 {==}
194
195def with_limit_empty(+n: Nat) -> S.Empty_Vector.with_limit_empty(n):
196 {==}
197
198def new_impl() -> {BLI.new() == SS.real(TR.initial(None{})) : BLI.Bitlist}:
199 new_real()
200
201def from_bools_model(+bs: List<&2, Bool>, +c: Nat, +hc: {c == 31n : Nat}, +h: {Nat.is_le(SC.length(Bool, bs), Nat.mul(SC.pow2(c), 32n)) == True{} : Bool}) -> S.To_Vector.from_bools_model(bs, c, hc, h):
202 from_bools_spells(bs, c, hc, h)
203
204# ---- Clear: Length 0 (the S.limit is kept) ----
205def clear_length(+l: Maybe<&2, Nat>, +c: Nat, +xs: List<&2, Bool>) -> S.Clear.clear_length(l, c, xs):
206 {==}
207
208def clear_limit(+l: Maybe<&2, Nat>, +c: Nat, +xs: List<&2, Bool>) -> S.Clear.clear_limit(l, c, xs):
209 {==}
210
211# ---- Element ----
212def get_element(+l: Maybe<&2, Nat>, +c: Nat, +xs: List<&2, Bool>, +i: Nat, +v: Bool, +h: {SC.nth(Bool, xs, i) == Some{v} : Maybe<&2, Bool>}) -> S.Element.get_element(l, c, xs, i, v, h):
213 %Equal.sym(Maybe<&2, Bool>, SC.nth(Bool, xs, i), Some{v}, h) : {E.OBit{S.bit(_)} == E.OBit{Done{v}} : E.Obs}
214 {==}
215
216def get_frame(+l: Maybe<&2, Nat>, +c: Nat, +xs: List<&2, Bool>, +i: Nat) -> S.Element.get_frame(l, c, xs, i):
217 {==}
218
219def get_outside(+l: Maybe<&2, Nat>, +c: Nat, +xs: List<&2, Bool>, +i: Nat, +h: {Nat.is_le(SC.length(Bool, xs), i) == True{} : Bool}) -> S.Element.get_outside(l, c, xs, i, h):
220 %Equal.sym(Maybe<&2, Bool>, SC.nth(Bool, xs, i), None{}, LL.nth_none(Bool, xs, i, h)) : {E.OBit{S.bit(_)} == E.OBit{Fail{E.IndexOutOfRange{}}} : E.Obs}
221 {==}
222
223# ---- Replace_Element: Length kept, Element (Index) = New_Item, Equal_Except elsewhere ----
224def assign_bits(+l: Maybe<&2, Nat>, +c: Nat, +xs: List<&2, Bool>, +i: Nat, +v: Bool, +h: {Nat.is_lt(i, SC.length(Bool, xs)) == True{} : Bool}) -> {S.bits(S.nx(S.M{l, c, xs}, E.Assign{i, v})) == SC.update(Bool, xs, i, v) : List<&2, Bool>}:
225 %Equal.sym(S.Model & E.Obs, S.step(S.M{l, c, xs}, E.Assign{i, v}), (S.M{l, c, SC.update(Bool, xs, i, v)}, E.OUnit{Done{Unit{}}}), assign_step(l, c, xs, i, v, h)) : {S.bits(Pair.fst(S.Model, E.Obs, _)) == SC.update(Bool, xs, i, v) : List<&2, Bool>}
226 {==}
227
228def assign_length(+l: Maybe<&2, Nat>, +c: Nat, +xs: List<&2, Bool>, +i: Nat, +v: Bool, +h: {Nat.is_lt(i, SC.length(Bool, xs)) == True{} : Bool}) -> S.Replace_Element.assign_length(l, c, xs, i, v, h):
229 length_assign(l, c, xs, i, v, h)
230
231def assign_element(+l: Maybe<&2, Nat>, +c: Nat, +xs: List<&2, Bool>, +i: Nat, +v: Bool, +h: {Nat.is_lt(i, SC.length(Bool, xs)) == True{} : Bool}) -> S.Replace_Element.assign_element(l, c, xs, i, v, h):
232 %Equal.sym(List<&2, Bool>, S.bits(S.nx(S.M{l, c, xs}, E.Assign{i, v})), SC.update(Bool, xs, i, v), assign_bits(l, c, xs, i, v, h)) : {SC.nth(Bool, _, i) == Some{v} : Maybe<&2, Bool>}
233 VL.update_at(Bool, xs, i, v, h)
234
235def assign_except(+l: Maybe<&2, Nat>, +c: Nat, +xs: List<&2, Bool>, +i: Nat, +v: Bool, +h: {Nat.is_lt(i, SC.length(Bool, xs)) == True{} : Bool}) -> S.Replace_Element.assign_except(l, c, xs, i, v, h):
236 L.subst(List<&2, Bool>, z => V.EqualExcept(Bool, xs, z, i), SC.update(Bool, xs, i, v), S.bits(S.nx(S.M{l, c, xs}, E.Assign{i, v})), Equal.sym(List<&2, Bool>, S.bits(S.nx(S.M{l, c, xs}, E.Assign{i, v})), SC.update(Bool, xs, i, v), assign_bits(l, c, xs, i, v, h)), VL.update_except(Bool, xs, i, v))
237
238def assign_outside(+l: Maybe<&2, Nat>, +c: Nat, +xs: List<&2, Bool>, +i: Nat, +v: Bool, +h: {Nat.is_le(SC.length(Bool, xs), i) == True{} : Bool}) -> S.Replace_Element.assign_outside(l, c, xs, i, v, h):
239 %Equal.sym(Maybe<&2, Bool>, SC.nth(Bool, xs, i), None{}, LL.nth_none(Bool, xs, i, h)) : {S.assign_at(_, l, c, xs, i, v) == (S.M{l, c, xs}, E.OUnit{Fail{E.IndexOutOfRange{}}}) : S.Model & E.Obs}
240 {==}
241
242# ---- Append: Length + 1, Equal_Prefix (Model'Old, Model), Element (Last'Old + 1) = New_Item ----
243def push_bits(+l: Maybe<&2, Nat>, +c: Nat, +xs: List<&2, Bool>, +v: Bool, +h: {S.room(l, c, SC.length(Bool, xs)) == True{} : Bool}) -> {S.bits(S.nx(S.M{l, c, xs}, E.Push{v})) == SC.snoc(Bool, xs, v) : List<&2, Bool>}:
244 %Equal.sym(S.Model & E.Obs, S.step(S.M{l, c, xs}, E.Push{v}), (S.M{l, c, SC.snoc(Bool, xs, v)}, E.OUnit{Done{Unit{}}}), push_step(l, c, xs, v, h)) : {S.bits(Pair.fst(S.Model, E.Obs, _)) == SC.snoc(Bool, xs, v) : List<&2, Bool>}
245 {==}
246
247def push_length(+l: Maybe<&2, Nat>, +c: Nat, +xs: List<&2, Bool>, +v: Bool, +h: {S.room(l, c, SC.length(Bool, xs)) == True{} : Bool}) -> S.Append.push_length(l, c, xs, v, h):
248 length_push(l, c, xs, v, h)
249
250def push_prefix(+l: Maybe<&2, Nat>, +c: Nat, +xs: List<&2, Bool>, +v: Bool, +h: {S.room(l, c, SC.length(Bool, xs)) == True{} : Bool}) -> S.Append.push_prefix(l, c, xs, v, h):
251 L.subst(List<&2, Bool>, z => V.EqualPrefix(Bool, xs, z), SC.snoc(Bool, xs, v), S.bits(S.nx(S.M{l, c, xs}, E.Push{v})), Equal.sym(List<&2, Bool>, S.bits(S.nx(S.M{l, c, xs}, E.Push{v})), SC.snoc(Bool, xs, v), push_bits(l, c, xs, v, h)), VL.snoc_prefix(Bool, xs, v))
252
253def push_element(+l: Maybe<&2, Nat>, +c: Nat, +xs: List<&2, Bool>, +v: Bool, +h: {S.room(l, c, SC.length(Bool, xs)) == True{} : Bool}) -> S.Append.push_element(l, c, xs, v, h):
254 %Equal.sym(List<&2, Bool>, S.bits(S.nx(S.M{l, c, xs}, E.Push{v})), SC.snoc(Bool, xs, v), push_bits(l, c, xs, v, h)) : {SC.nth(Bool, _, SC.length(Bool, xs)) == Some{v} : Maybe<&2, Bool>}
255 VL.snoc_last(Bool, xs, v)
256
257def push_full(+l: Maybe<&2, Nat>, +c: Nat, +xs: List<&2, Bool>, +v: Bool, +h: {S.room(l, c, SC.length(Bool, xs)) == False{} : Bool}) -> S.Append.push_full(l, c, xs, v, h):
258 %Equal.sym(Bool, S.room(l, c, SC.length(Bool, xs)), False{}, h) : {S.push_if(_, l, c, xs, v) == (S.M{l, c, xs}, E.OUnit{Fail{E.Full{}}}) : S.Model & E.Obs}
259 {==}
260
261# ---- Delete_Last: Length - 1, Equal_Prefix (Model, Model'Old); pop returns Last_Element'Old ----
262def pop_length(+l: Maybe<&2, Nat>, +c: Nat, +h: Bool, +t: List<&2, Bool>) -> S.Delete_Last.pop_length(l, c, h, t):
263 VL.init_length(Bool, t, h)
264
265def pop_prefix(+l: Maybe<&2, Nat>, +c: Nat, +h: Bool, +t: List<&2, Bool>) -> S.Delete_Last.pop_prefix(l, c, h, t):
266 VL.init_prefix(Bool, t, h)
267
268def pop_result(+l: Maybe<&2, Nat>, +c: Nat, +h: Bool, +t: List<&2, Bool>) -> S.Delete_Last.pop_result(l, c, h, t):
269 %Equal.sym(Maybe<&2, Bool>, SC.last(Bool, Con{h, t}), V.last_elem(Bool, Con{h, t}), VL.last_is_elem(Bool, t, h)) : {E.OBit{S.last_bit(_)} == E.OBit{S.last_bit(V.last_elem(Bool, Con{h, t}))} : E.Obs}
270 {==}
271
272def pop_empty(+l: Maybe<&2, Nat>, +c: Nat) -> S.Delete_Last.pop_empty(l, c):
273 {==}