spec/containers/bitlist.bend
bend-collections-laws-containers@1.0.0.0 · 339 lines · 0 definitions
1import Base
2import bend-collections-laws-containers@1.0.0.0/spec/lib/common.bend as C
3import bend-collections-laws-containers@1.0.0.0/spec/containers/bitset.bend as BS
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/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
26type Model is Data:
27 M{limit: Maybe<&2, Nat>, cexp: Nat, bits: List<&2, Bool>}
28
29def new() -> Model:
30 M{None{}, 31n, Nil{}}
31
32def with_limit(+n: Nat) -> Model:
33 M{Some{n}, 31n, Nil{}}
34
35# One more bit fits under the limit and in the storage.
36def 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
43def 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).
47def count(xs: List<&2, Bool>) -> Nat:
48 BS.count(xs)
49
50def 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
57def 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.
65def 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
72def 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
79def 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
86def 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.
108def step(m: Model, op: E.Op) -> Model & E.Obs:
109 M{+l, +c, +xs} = m
110 step_parts(l, c, xs, op)
111
112def 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
116def 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.
124def 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
131def 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
154def bits(m: Model) -> List<&2, Bool>:
155 match m:
156 case M{l, c, xs}:
157 xs
158
159# Replace_Element (384)
160def 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)
164def 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)
168def 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)
172def 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)
176def 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)
180def 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)
184def 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
222def nx(+m: Model, +op: E.Op) -> Model:
223 Pair.fst(Model, E.Obs, step(m, op))
224
225def ob(+m: Model, +op: E.Op) -> E.Obs:
226 Pair.snd(Model, E.Obs, step(m, op))
227
228def limit(m: Model) -> Maybe<&2, Nat>:
229 match m:
230 case M{l, c, xs}:
231 l
232
233# Length (284)
234def 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)
238def 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)
242def 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)
246def 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
250def 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)
254def 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)
258def 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)
262def Empty_Vector.new_empty() -> Type:
263 {C.length(Bool, bits(new())) == 0n : Nat}
264
265# Empty_Vector (292)
266def Empty_Vector.with_limit_empty(+n: Nat) -> Type:
267 {C.length(Bool, bits(with_limit(n))) == 0n : Nat}
268
269# To_Vector (308)
270def 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)
274def 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)
278def 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)
282def 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)
286def 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)
290def 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)
294def 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)
298def 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)
302def 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)
306def 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)
310def 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)
314def 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)
318def 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)
322def 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)
326def 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)
330def 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)
334def 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)
338def 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}