1	import Base
2	import ../lib/common.bend as C
3	import ./bitset.bend as BS
4	import ../../src/containers/types/bitlist.bend as E
5	import ../lib/sequence.bend as V
6	
7	# Independent model of a bit list: a sequence of Booleans (bit 0 first), an
8	# optional maximum length and the capacity exponent of the storage (a bit
9	# list holds at most 32 * 2^cexp bits). Nothing here refers to words,
10	# shifts, masks or arrays.
11	#
12	# Shape of the specification, following verified bit-sequence developments:
13	#   * SSZ Bitlist[N] as in the ConsenSys eth2.0-dafny SSZ proofs
14	#     (src/dafny/ssz/BitListSeDes.dfy, wiki/ssz-notes.md): a bitlist is a
15	#     sequence of booleans whose length is bounded by N; appending past N
16	#     is not allowed.
17	#   * Lean 4 core `List Bool` / `BitVec` lemmas (Init.Data.BitVec.Lemmas,
18	#     getLsbD_concat / getLsbD_cons, List.getElem_set): reading bit i after
19	#     writing bit j is the written bit when i = j and the old bit otherwise;
20	#     appending one bit extends the sequence by exactly that bit.
21	#   * SPARK Ada formal vectors (Formal_Vectors: Length / Element /
22	#     Replace_Element / Append postconditions): every operation is stated by
23	#     its effect on the whole model plus frame conditions (proofs/containers
24	#     /bitlist/proof.bend).
25	
26	type Model is Data:
27	  M{limit: Maybe<&2, Nat>, cexp: Nat, bits: List<&2, Bool>}
28	
29	def new() -> Model:
30	  M{None{}, 31n, Nil{}}
31	
32	def with_limit(+n: Nat) -> Model:
33	  M{Some{n}, 31n, Nil{}}
34	
35	# One more bit fits under the limit and in the storage.
36	def below(lim: Maybe<&2, Nat>, +n: Nat) -> Bool:
37	  match lim:
38	    case None{}:
39	      True{}
40	    case Some{k}:
41	      Nat.is_lt(n, k)
42	
43	def room(lim: Maybe<&2, Nat>, +c: Nat, +n: Nat) -> Bool:
44	  Bool.and(below(lim, n), Nat.is_lt(n, Nat.mul(C.pow2(c), 32n)))
45	
46	# Number of True bits (the popcount of the bitset specification).
47	def count(xs: List<&2, Bool>) -> Nat:
48	  BS.count(xs)
49	
50	def bit(x: Maybe<&2, Bool>) -> Result<&2, &2, E.Error, Bool>:
51	  match x:
52	    case None{}:
53	      Fail{E.IndexOutOfRange{}}
54	    case Some{b}:
55	      Done{b}
56	
57	def last_bit(x: Maybe<&2, Bool>) -> Result<&2, &2, E.Error, Bool>:
58	  match x:
59	    case None{}:
60	      Fail{E.Empty{}}
61	    case Some{b}:
62	      Done{b}
63	
64	# Assign bit i; out of range leaves the list unchanged and fails.
65	def assign_at(x: Maybe<&2, Bool>, +l: Maybe<&2, Nat>, +c: Nat, +xs: List<&2, Bool>, i: Nat, v: Bool) -> Model & E.Obs:
66	  match x:
67	    case None{}:
68	      (M{l, c, xs}, E.OUnit{Fail{E.IndexOutOfRange{}}})
69	    case Some{b}:
70	      (M{l, c, C.update(Bool, xs, i, v)}, E.OUnit{Done{Unit{}}})
71	
72	def push_if(ok: Bool, +l: Maybe<&2, Nat>, +c: Nat, +xs: List<&2, Bool>, v: Bool) -> Model & E.Obs:
73	  match ok:
74	    case True{}:
75	      (M{l, c, C.snoc(Bool, xs, v)}, E.OUnit{Done{Unit{}}})
76	    case False{}:
77	      (M{l, c, xs}, E.OUnit{Fail{E.Full{}}})
78	
79	def pop(+l: Maybe<&2, Nat>, +c: Nat, xs: List<&2, Bool>) -> Model & E.Obs:
80	  match xs:
81	    case Nil{}:
82	      (M{l, c, Nil{}}, E.OBit{Fail{E.Empty{}}})
83	    case Con{+h, +t}:
84	      (M{l, c, C.init(Bool, Con{h, t})}, E.OBit{last_bit(C.last(Bool, Con{h, t}))})
85	
86	def step_parts(+l: Maybe<&2, Nat>, +c: Nat, +xs: List<&2, Bool>, op: E.Op) -> Model & E.Obs:
87	  match op:
88	    case E.Length{}:
89	      (M{l, c, xs}, E.ONat{C.length(Bool, xs)})
90	    case E.Limit{}:
91	      (M{l, c, xs}, E.OLimit{l})
92	    case E.Get{+i}:
93	      (M{l, c, xs}, E.OBit{bit(C.nth(Bool, xs, i))})
94	    case E.Assign{+i, +v}:
95	      assign_at(C.nth(Bool, xs, i), l, c, xs, i, v)
96	    case E.Push{+v}:
97	      push_if(room(l, c, C.length(Bool, xs)), l, c, xs, v)
98	    case E.Pop{}:
99	      pop(l, c, xs)
100	    case E.Clear{}:
101	      (M{l, c, Nil{}}, E.OUnit{Done{Unit{}}})
102	    case E.Count{}:
103	      (M{l, c, xs}, E.ONat{count(xs)})
104	    case E.ToList{}:
105	      (M{l, c, xs}, E.OBits{xs})
106	
107	# Every operation: the next model and the observation.
108	def step(m: Model, op: E.Op) -> Model & E.Obs:
109	  M{+l, +c, +xs} = m
110	  step_parts(l, c, xs, op)
111	
112	def cons_obs(o: E.Obs, r: Model & List<&2, E.Obs>) -> Model & List<&2, E.Obs>:
113	  (m, os) = r
114	  (m, Con{o, os})
115	
116	def run(ops: List<&2, E.Op>, +m: Model) -> Model & List<&2, E.Obs>:
117	  match ops:
118	    case Nil{}:
119	      (m, Nil{})
120	    case Con{+op, rest}:
121	      cons_obs(Pair.snd(Model, E.Obs, step(m, op)), run(rest, Pair.fst(Model, E.Obs, step(m, op))))
122	
123	# from_bools: the bits pushed one by one onto the unbounded list.
124	def push_all(bs: List<&2, Bool>, +m: Model) -> Model:
125	  match bs:
126	    case Nil{}:
127	      m
128	    case Con{+b, t}:
129	      push_all(t, Pair.fst(Model, E.Obs, step(m, E.Push{b})))
130	
131	def from_bools(+bs: List<&2, Bool>) -> Model:
132	  push_all(bs, new())
133	
134	# ---- contract (SPARK formal containers) ----
135	# Each `<Subprogram>.<clause>` definition below states one Post clause of
136	# that SPARK subprogram, as a proposition on this model; the table names the
137	# clauses. proofs/containers/bitlist/ proves every clause under its clause name,
138	# and its `impl` lemma carries them to the implementation.
139	#
140	# Contracts of the specification, in the style of the SPARK formal vector
141	# postconditions (Replace_Element: Element(Container, I) = New_Item and every
142	# other element unchanged; Append: Length + 1 and Last_Element = New_Item)
143	# and of the Lean 4 List lemmas (List.getElem_set_self / getElem_set_ne,
144	# List.length_concat, List.dropLast_concat): each law is about the model
145	# step, and proofs/containers/bitlist/steps.bend makes the implementation
146	# step equal to step on every good bitlist, so each law holds for the
147	# implementation.
148	#
149	#   SPARK subprogram (.ads line)   ours    clauses
150	#   Replace_Element (384)          assign  get_assign_same, get_assign_other, length_assign
151	#   Append (706)                   push    length_push, get_push_last, count_push
152	#   Delete_Last (866)              pop     pop_push
153	
154	def bits(m: Model) -> List<&2, Bool>:
155	  match m:
156	    case M{l, c, xs}:
157	      xs
158	
159	# Replace_Element (384)
160	def Replace_Element.get_assign_same(+l: Maybe<&2, Nat>, +c: Nat, +xs: List<&2, Bool>, +i: Nat, +v: Bool, +h: {Nat.is_lt(i, C.length(Bool, xs)) == True{} : Bool}) -> Type:
161	  {Pair.snd(Model, E.Obs, step(Pair.fst(Model, E.Obs, step(M{l, c, xs}, E.Assign{i, v})), E.Get{i})) == E.OBit{Done{v}} : E.Obs}
162	
163	# Replace_Element (384)
164	def Replace_Element.get_assign_other(+l: Maybe<&2, Nat>, +c: Nat, +xs: List<&2, Bool>, +i: Nat, +j: Nat, +v: Bool, +h: {Nat.is_lt(i, C.length(Bool, xs)) == True{} : Bool}, +ne: {Nat.is_eq(i, j) == False{} : Bool}) -> Type:
165	  {Pair.snd(Model, E.Obs, step(Pair.fst(Model, E.Obs, step(M{l, c, xs}, E.Assign{i, v})), E.Get{j})) == Pair.snd(Model, E.Obs, step(M{l, c, xs}, E.Get{j})) : E.Obs}
166	
167	# Replace_Element (384)
168	def Replace_Element.length_assign(+l: Maybe<&2, Nat>, +c: Nat, +xs: List<&2, Bool>, +i: Nat, +v: Bool, +h: {Nat.is_lt(i, C.length(Bool, xs)) == True{} : Bool}) -> Type:
169	  {C.length(Bool, bits(Pair.fst(Model, E.Obs, step(M{l, c, xs}, E.Assign{i, v})))) == C.length(Bool, xs) : Nat}
170	
171	# Append (706)
172	def Append.length_push(+l: Maybe<&2, Nat>, +c: Nat, +xs: List<&2, Bool>, +v: Bool, +h: {room(l, c, C.length(Bool, xs)) == True{} : Bool}) -> Type:
173	  {C.length(Bool, bits(Pair.fst(Model, E.Obs, step(M{l, c, xs}, E.Push{v})))) == 1n+C.length(Bool, xs) : Nat}
174	
175	# Append (706)
176	def Append.get_push_last(+l: Maybe<&2, Nat>, +c: Nat, +xs: List<&2, Bool>, +v: Bool, +h: {room(l, c, C.length(Bool, xs)) == True{} : Bool}) -> Type:
177	  {Pair.snd(Model, E.Obs, step(Pair.fst(Model, E.Obs, step(M{l, c, xs}, E.Push{v})), E.Get{C.length(Bool, xs)})) == E.OBit{Done{v}} : E.Obs}
178	
179	# Delete_Last (866)
180	def Delete_Last.pop_push(+l: Maybe<&2, Nat>, +c: Nat, +xs: List<&2, Bool>, +v: Bool, +h: {room(l, c, C.length(Bool, xs)) == True{} : Bool}) -> Type:
181	  {step(Pair.fst(Model, E.Obs, step(M{l, c, xs}, E.Push{v})), E.Pop{}) == (M{l, c, xs}, E.OBit{Done{v}}) : Model & E.Obs}
182	
183	# Append (706)
184	def Append.count_push(+l: Maybe<&2, Nat>, +c: Nat, +xs: List<&2, Bool>, +v: Bool, +h: {room(l, c, C.length(Bool, xs)) == True{} : Bool}) -> Type:
185	  {count(bits(Pair.fst(Model, E.Obs, step(M{l, c, xs}, E.Push{v})))) == Nat.add(count(xs), count(Con{v, Nil{}})) : Nat}
186	
187	# ---- contract (SPARK formal containers) ----
188	# Each `<Subprogram>.<clause>` definition below states one Post clause of
189	# that SPARK subprogram, as a proposition on this model; the table names the
190	# clauses. proofs/containers/bitlist/ proves every clause under its clause name,
191	# and its `impl` lemma carries them to the implementation.
192	#
193	# The bit list against the complete SPARK formal-vector contract set
194	# (SPARKlib src/spark-containers-formal-vectors.ads, AdaCore/SPARKlib
195	# 46ec319; model predicates in spec/lib/sequence.bend), on top of the
196	# read-back laws above. Each lemma is one Post clause of
197	# step; `impl` (via P.step_ok) carries every clause to the
198	# implementation: BLI.step on the bit list of a good shadow lands on the
199	# bit list of a good shadow whose model satisfies it.
200	#
201	#   SPARK subprogram (.ads line)   ours              clauses
202	#   Length (284)                   length            length_result, length_frame
203	#   Capacity (322)                 limit             limit_result, limit_frame
204	#   Empty_Vector (292)             new, with_limit   new_empty, with_limit_empty, new_impl
205	#   Clear (341)                    clear             clear_length, clear_limit
206	#   Element (373)                  get               get_element, get_frame, get_outside
207	#   Replace_Element (384)          assign/set/unset  assign_length, assign_element,
208	#                                                    assign_except, assign_outside
209	#   Append (706)                   push              push_length, push_prefix,
210	#                                                    push_element, push_full
211	#   Delete_Last (866)              pop               pop_length, pop_prefix, pop_result, pop_empty
212	#   Last_Element (923)             pop's result      pop_result
213	#   iteration (Iter_Model, 1193)   to_list           to_list_model, to_list_frame
214	#   To_Vector (308)                from_bools        from_bools_model (the model spells the input)
215	#   implementation                 BLI.step          impl
216	# count has no SPARK counterpart (count_result: the number of set bits).
217	# Not in this API: Is_Empty, "=", Assign/Copy/Move, Reserve_Capacity,
218	# Reference, Insert*, Prepend*, Append_Vector/Count, Delete (at an index),
219	# Delete_First, Delete_Last with Count, First_Element, Reverse_Elements,
220	# Swap, Find_Index, Reverse_Find_Index, Contains, Has_Element.
221	
222	def nx(+m: Model, +op: E.Op) -> Model:
223	  Pair.fst(Model, E.Obs, step(m, op))
224	
225	def ob(+m: Model, +op: E.Op) -> E.Obs:
226	  Pair.snd(Model, E.Obs, step(m, op))
227	
228	def limit(m: Model) -> Maybe<&2, Nat>:
229	  match m:
230	    case M{l, c, xs}:
231	      l
232	
233	# Length (284)
234	def Length.length_result(+l: Maybe<&2, Nat>, +c: Nat, +xs: List<&2, Bool>) -> Type:
235	  {ob(M{l, c, xs}, E.Length{}) == E.ONat{C.length(Bool, xs)} : E.Obs}
236	
237	# Length (284)
238	def Length.length_frame(+l: Maybe<&2, Nat>, +c: Nat, +xs: List<&2, Bool>) -> Type:
239	  {nx(M{l, c, xs}, E.Length{}) == M{l, c, xs} : Model}
240	
241	# Capacity (322)
242	def Capacity.limit_result(+l: Maybe<&2, Nat>, +c: Nat, +xs: List<&2, Bool>) -> Type:
243	  {ob(M{l, c, xs}, E.Limit{}) == E.OLimit{l} : E.Obs}
244	
245	# Capacity (322)
246	def Capacity.limit_frame(+l: Maybe<&2, Nat>, +c: Nat, +xs: List<&2, Bool>) -> Type:
247	  {nx(M{l, c, xs}, E.Limit{}) == M{l, c, xs} : Model}
248	
249	# implementation
250	def Implementation.count_result(+l: Maybe<&2, Nat>, +c: Nat, +xs: List<&2, Bool>) -> Type:
251	  {ob(M{l, c, xs}, E.Count{}) == E.ONat{count(xs)} : E.Obs}
252	
253	# iteration (Iter_Model, 1193)
254	def Iteration.to_list_model(+l: Maybe<&2, Nat>, +c: Nat, +xs: List<&2, Bool>) -> Type:
255	  {ob(M{l, c, xs}, E.ToList{}) == E.OBits{xs} : E.Obs}
256	
257	# iteration (Iter_Model, 1193)
258	def Iteration.to_list_frame(+l: Maybe<&2, Nat>, +c: Nat, +xs: List<&2, Bool>) -> Type:
259	  {nx(M{l, c, xs}, E.ToList{}) == M{l, c, xs} : Model}
260	
261	# Empty_Vector (292)
262	def Empty_Vector.new_empty() -> Type:
263	  {C.length(Bool, bits(new())) == 0n : Nat}
264	
265	# Empty_Vector (292)
266	def Empty_Vector.with_limit_empty(+n: Nat) -> Type:
267	  {C.length(Bool, bits(with_limit(n))) == 0n : Nat}
268	
269	# To_Vector (308)
270	def To_Vector.from_bools_model(+bs: List<&2, Bool>, +c: Nat, +hc: {c == 31n : Nat}, +h: {Nat.is_le(C.length(Bool, bs), Nat.mul(C.pow2(c), 32n)) == True{} : Bool}) -> Type:
271	  {push_all(bs, M{None{}, c, Nil{}}) == M{None{}, c, bs} : Model}
272	
273	# Clear (341)
274	def Clear.clear_length(+l: Maybe<&2, Nat>, +c: Nat, +xs: List<&2, Bool>) -> Type:
275	  {C.length(Bool, bits(nx(M{l, c, xs}, E.Clear{}))) == 0n : Nat}
276	
277	# Clear (341)
278	def Clear.clear_limit(+l: Maybe<&2, Nat>, +c: Nat, +xs: List<&2, Bool>) -> Type:
279	  {limit(nx(M{l, c, xs}, E.Clear{})) == l : Maybe<&2, Nat>}
280	
281	# Element (373)
282	def Element.get_element(+l: Maybe<&2, Nat>, +c: Nat, +xs: List<&2, Bool>, +i: Nat, +v: Bool, +h: {C.nth(Bool, xs, i) == Some{v} : Maybe<&2, Bool>}) -> Type:
283	  {ob(M{l, c, xs}, E.Get{i}) == E.OBit{Done{v}} : E.Obs}
284	
285	# Element (373)
286	def Element.get_frame(+l: Maybe<&2, Nat>, +c: Nat, +xs: List<&2, Bool>, +i: Nat) -> Type:
287	  {nx(M{l, c, xs}, E.Get{i}) == M{l, c, xs} : Model}
288	
289	# Element (373)
290	def Element.get_outside(+l: Maybe<&2, Nat>, +c: Nat, +xs: List<&2, Bool>, +i: Nat, +h: {Nat.is_le(C.length(Bool, xs), i) == True{} : Bool}) -> Type:
291	  {ob(M{l, c, xs}, E.Get{i}) == E.OBit{Fail{E.IndexOutOfRange{}}} : E.Obs}
292	
293	# Replace_Element (384)
294	def Replace_Element.assign_length(+l: Maybe<&2, Nat>, +c: Nat, +xs: List<&2, Bool>, +i: Nat, +v: Bool, +h: {Nat.is_lt(i, C.length(Bool, xs)) == True{} : Bool}) -> Type:
295	  {C.length(Bool, bits(nx(M{l, c, xs}, E.Assign{i, v}))) == C.length(Bool, xs) : Nat}
296	
297	# Replace_Element (384)
298	def Replace_Element.assign_element(+l: Maybe<&2, Nat>, +c: Nat, +xs: List<&2, Bool>, +i: Nat, +v: Bool, +h: {Nat.is_lt(i, C.length(Bool, xs)) == True{} : Bool}) -> Type:
299	  {C.nth(Bool, bits(nx(M{l, c, xs}, E.Assign{i, v})), i) == Some{v} : Maybe<&2, Bool>}
300	
301	# Replace_Element (384)
302	def Replace_Element.assign_except(+l: Maybe<&2, Nat>, +c: Nat, +xs: List<&2, Bool>, +i: Nat, +v: Bool, +h: {Nat.is_lt(i, C.length(Bool, xs)) == True{} : Bool}) -> Type:
303	  V.EqualExcept(Bool, xs, bits(nx(M{l, c, xs}, E.Assign{i, v})), i)
304	
305	# Replace_Element (384)
306	def Replace_Element.assign_outside(+l: Maybe<&2, Nat>, +c: Nat, +xs: List<&2, Bool>, +i: Nat, +v: Bool, +h: {Nat.is_le(C.length(Bool, xs), i) == True{} : Bool}) -> Type:
307	  {step(M{l, c, xs}, E.Assign{i, v}) == (M{l, c, xs}, E.OUnit{Fail{E.IndexOutOfRange{}}}) : Model & E.Obs}
308	
309	# Append (706)
310	def Append.push_length(+l: Maybe<&2, Nat>, +c: Nat, +xs: List<&2, Bool>, +v: Bool, +h: {room(l, c, C.length(Bool, xs)) == True{} : Bool}) -> Type:
311	  {C.length(Bool, bits(nx(M{l, c, xs}, E.Push{v}))) == 1n+C.length(Bool, xs) : Nat}
312	
313	# Append (706)
314	def Append.push_prefix(+l: Maybe<&2, Nat>, +c: Nat, +xs: List<&2, Bool>, +v: Bool, +h: {room(l, c, C.length(Bool, xs)) == True{} : Bool}) -> Type:
315	  V.EqualPrefix(Bool, xs, bits(nx(M{l, c, xs}, E.Push{v})))
316	
317	# Append (706)
318	def Append.push_element(+l: Maybe<&2, Nat>, +c: Nat, +xs: List<&2, Bool>, +v: Bool, +h: {room(l, c, C.length(Bool, xs)) == True{} : Bool}) -> Type:
319	  {C.nth(Bool, bits(nx(M{l, c, xs}, E.Push{v})), C.length(Bool, xs)) == Some{v} : Maybe<&2, Bool>}
320	
321	# Append (706)
322	def Append.push_full(+l: Maybe<&2, Nat>, +c: Nat, +xs: List<&2, Bool>, +v: Bool, +h: {room(l, c, C.length(Bool, xs)) == False{} : Bool}) -> Type:
323	  {step(M{l, c, xs}, E.Push{v}) == (M{l, c, xs}, E.OUnit{Fail{E.Full{}}}) : Model & E.Obs}
324	
325	# Delete_Last (866)
326	def Delete_Last.pop_length(+l: Maybe<&2, Nat>, +c: Nat, +h: Bool, +t: List<&2, Bool>) -> Type:
327	  {C.length(Bool, bits(nx(M{l, c, Con{h, t}}, E.Pop{}))) == C.length(Bool, t) : Nat}
328	
329	# Delete_Last (866)
330	def Delete_Last.pop_prefix(+l: Maybe<&2, Nat>, +c: Nat, +h: Bool, +t: List<&2, Bool>) -> Type:
331	  V.EqualPrefix(Bool, bits(nx(M{l, c, Con{h, t}}, E.Pop{})), Con{h, t})
332	
333	# Delete_Last (866)
334	def Delete_Last.pop_result(+l: Maybe<&2, Nat>, +c: Nat, +h: Bool, +t: List<&2, Bool>) -> Type:
335	  {ob(M{l, c, Con{h, t}}, E.Pop{}) == E.OBit{last_bit(V.last_elem(Bool, Con{h, t}))} : E.Obs}
336	
337	# Delete_Last (866)
338	def Delete_Last.pop_empty(+l: Maybe<&2, Nat>, +c: Nat) -> Type:
339	  {step(M{l, c, Nil{}}, E.Pop{}) == (M{l, c, Nil{}}, E.OBit{Fail{E.Empty{}}}) : Model & E.Obs}