1	import Base
2	import ../../../spec/lib/common.bend as SC
3	import ../../../src/containers/bitlist.bend as BLI
4	import ../../../src/containers/types/bitlist.bend as E
5	import ../../../spec/containers/bitlist.bend as S
6	import ./state.bend as SS
7	import ./steps.bend as BS
8	import ./trace.bend as TR
9	import ../../lib/list.bend as LL
10	import ../bitset/lists.bend as BL
11	import ../../lib/logic.bend as L
12	import ../../lib/nat.bend as N
13	import ../../../spec/lib/sequence.bend as V
14	import ../../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 ----
19	def 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	
26	def 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	
29	def 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	
34	def 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	
39	def 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	
43	def 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	
50	def 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 ----
60	def 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	
64	def 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	
68	def 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	
73	def 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	
77	def 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 ----
83	def 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	
87	def 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	
91	def 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	
124	def new_real() -> {BLI.new() == SS.real(TR.initial(None{})) : BLI.Bitlist}:
125	  TR.new_real()
126	
127	def new_model() -> {SS.model(TR.initial(None{})) == S.new() : S.Model}:
128	  TR.new_model()
129	
130	def with_limit_real(+n: Nat) -> {BLI.with_limit(n) == SS.real(TR.initial(Some{n})) : BLI.Bitlist}:
131	  TR.with_limit_real(n)
132	
133	def with_limit_model(+n: Nat) -> {SS.model(TR.initial(Some{n})) == S.with_limit(n) : S.Model}:
134	  TR.with_limit_model(n)
135	
136	def initial_good(+l: Maybe<&2, Nat>) -> {SS.good(TR.initial(l)) == True{} : Bool}:
137	  TR.initial_good(l)
138	
139	def 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	
142	def 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	
145	def 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	
148	def 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
152	def 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 ----
158	def 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	
161	def 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	
166	def 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 ----
170	def length_result(+l: Maybe<&2, Nat>, +c: Nat, +xs: List<&2, Bool>) -> S.Length.length_result(l, c, xs):
171	  {==}
172	
173	def length_frame(+l: Maybe<&2, Nat>, +c: Nat, +xs: List<&2, Bool>) -> S.Length.length_frame(l, c, xs):
174	  {==}
175	
176	def limit_result(+l: Maybe<&2, Nat>, +c: Nat, +xs: List<&2, Bool>) -> S.Capacity.limit_result(l, c, xs):
177	  {==}
178	
179	def limit_frame(+l: Maybe<&2, Nat>, +c: Nat, +xs: List<&2, Bool>) -> S.Capacity.limit_frame(l, c, xs):
180	  {==}
181	
182	def count_result(+l: Maybe<&2, Nat>, +c: Nat, +xs: List<&2, Bool>) -> S.Implementation.count_result(l, c, xs):
183	  {==}
184	
185	def to_list_model(+l: Maybe<&2, Nat>, +c: Nat, +xs: List<&2, Bool>) -> S.Iteration.to_list_model(l, c, xs):
186	  {==}
187	
188	def 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 ----
192	def new_empty() -> S.Empty_Vector.new_empty():
193	  {==}
194	
195	def with_limit_empty(+n: Nat) -> S.Empty_Vector.with_limit_empty(n):
196	  {==}
197	
198	def new_impl() -> {BLI.new() == SS.real(TR.initial(None{})) : BLI.Bitlist}:
199	  new_real()
200	
201	def 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) ----
205	def clear_length(+l: Maybe<&2, Nat>, +c: Nat, +xs: List<&2, Bool>) -> S.Clear.clear_length(l, c, xs):
206	  {==}
207	
208	def clear_limit(+l: Maybe<&2, Nat>, +c: Nat, +xs: List<&2, Bool>) -> S.Clear.clear_limit(l, c, xs):
209	  {==}
210	
211	# ---- Element ----
212	def 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	
216	def get_frame(+l: Maybe<&2, Nat>, +c: Nat, +xs: List<&2, Bool>, +i: Nat) -> S.Element.get_frame(l, c, xs, i):
217	  {==}
218	
219	def 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 ----
224	def 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	
228	def 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	
231	def 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	
235	def 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	
238	def 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 ----
243	def 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	
247	def 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	
250	def 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	
253	def 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	
257	def 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 ----
262	def 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	
265	def 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	
268	def 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	
272	def pop_empty(+l: Maybe<&2, Nat>, +c: Nat) -> S.Delete_Last.pop_empty(l, c):
273	  {==}