spec/containers/bitset.bend
bend-collections-laws-containers@1.0.0.0 · 321 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/src/containers/types/bitset.bend as E
4
5# Independent model: a bitset of logical size n is a sequence of n Booleans
6# (bit 0 first). Nothing here refers to words, shifts or masks.
7
8def new(n: Nat) -> List<&2, Bool>:
9 C.replicate(Bool, n, False{})
10
11# Number of True bits.
12def count(xs: List<&2, Bool>) -> Nat:
13 match xs:
14 case Nil{}:
15 0n
16 case Con{False{}, t}:
17 count(t)
18 case Con{True{}, t}:
19 1n+count(t)
20
21# Indices (offset by off) of True bits, ascending.
22def members(xs: List<&2, Bool>, +off: Nat) -> List<&2, Nat>:
23 match xs:
24 case Nil{}:
25 Nil{}
26 case Con{False{}, t}:
27 members(t, 1n+off)
28 case Con{True{}, t}:
29 Con{off, members(t, 1n+off)}
30
31# Element-wise combination of two sequences (truncates to the shorter one).
32def zip_or(xs: List<&2, Bool>, ys: List<&2, Bool>) -> List<&2, Bool>:
33 match xs ys:
34 case Con{a, s} Con{b, t}:
35 Con{Bool.or(a, b), zip_or(s, t)}
36 case _ _:
37 Nil{}
38
39def zip_and(xs: List<&2, Bool>, ys: List<&2, Bool>) -> List<&2, Bool>:
40 match xs ys:
41 case Con{a, s} Con{b, t}:
42 Con{Bool.and(a, b), zip_and(s, t)}
43 case _ _:
44 Nil{}
45
46def zip_diff(xs: List<&2, Bool>, ys: List<&2, Bool>) -> List<&2, Bool>:
47 match xs ys:
48 case Con{a, s} Con{b, t}:
49 Con{Bool.and(a, Bool.not(b)), zip_diff(s, t)}
50 case _ _:
51 Nil{}
52
53def zip_xor(xs: List<&2, Bool>, ys: List<&2, Bool>) -> List<&2, Bool>:
54 match xs ys:
55 case Con{a, s} Con{b, t}:
56 Con{Bool.xor(a, b), zip_xor(s, t)}
57 case _ _:
58 Nil{}
59
60def bit(x: Maybe<&2, Bool>) -> Result<&2, &2, E.Error, Bool>:
61 match x:
62 case None{}:
63 Fail{E.IndexOutOfRange{}}
64 case Some{b}:
65 Done{b}
66
67def get(xs: List<&2, Bool>, i: Nat) -> Result<&2, &2, E.Error, Bool>:
68 bit(C.nth(Bool, xs, i))
69
70# Assign bit i; out of range leaves the sequence unchanged and fails.
71def assign_at(x: Maybe<&2, Bool>, +xs: List<&2, Bool>, i: Nat, v: Bool) -> List<&2, Bool> & E.Obs:
72 match x:
73 case None{}:
74 (xs, E.OUnit{Fail{E.IndexOutOfRange{}}})
75 case Some{b}:
76 (C.update(Bool, xs, i, v), E.OUnit{Done{Unit{}}})
77
78def assign(+xs: List<&2, Bool>, +i: Nat, v: Bool) -> List<&2, Bool> & E.Obs:
79 assign_at(C.nth(Bool, xs, i), xs, i, v)
80
81# Combine with an operand of the same logical size; a size mismatch leaves
82# the sequence unchanged and fails.
83def combine_if(same: Bool, xs: List<&2, Bool>, r: List<&2, Bool>) -> List<&2, Bool> & E.Obs:
84 match same:
85 case False{}:
86 (xs, E.OUnit{Fail{E.LengthMismatch{}}})
87 case True{}:
88 (r, E.OUnit{Done{Unit{}}})
89
90def combine(+xs: List<&2, Bool>, ys: List<&2, Bool>, r: List<&2, Bool>) -> List<&2, Bool> & E.Obs:
91 combine_if(Nat.is_eq(C.length(Bool, xs), C.length(Bool, ys)), xs, r)
92
93def step(+xs: List<&2, Bool>, op: E.Op) -> List<&2, Bool> & E.Obs:
94 match op:
95 case E.Length{}:
96 (xs, E.ONat{C.length(Bool, xs)})
97 case E.Get{+i}:
98 (xs, E.OBit{get(xs, i)})
99 case E.Set{+i}:
100 assign(xs, i, True{})
101 case E.Clear{+i}:
102 assign(xs, i, False{})
103 case E.Count{}:
104 (xs, E.ONat{count(xs)})
105 case E.Union{+ys}:
106 combine(xs, ys, zip_or(xs, ys))
107 case E.Intersection{+ys}:
108 combine(xs, ys, zip_and(xs, ys))
109 case E.Difference{+ys}:
110 combine(xs, ys, zip_diff(xs, ys))
111 case E.Xor{+ys}:
112 combine(xs, ys, zip_xor(xs, ys))
113 case E.ToList{}:
114 (xs, E.OList{members(xs, 0n)})
115
116def cons_obs(o: E.Obs, r: List<&2, Bool> & List<&2, E.Obs>) -> List<&2, Bool> & List<&2, E.Obs>:
117 (m, os) = r
118 (m, Con{o, os})
119
120def run(ops: List<&2, E.Op>, +xs: List<&2, Bool>) -> List<&2, Bool> & List<&2, E.Obs>:
121 match ops:
122 case Nil{}:
123 (xs, Nil{})
124 case Con{+op, rest}:
125 cons_obs(Pair.snd(List<&2, Bool>, E.Obs, step(xs, op)), run(rest, Pair.fst(List<&2, Bool>, E.Obs, step(xs, op))))
126
127# ---- contract (SPARK formal containers) ----
128# Each `<Subprogram>.<clause>` definition below states one Post clause of
129# that SPARK subprogram, as a proposition on this model; the table names the
130# clauses. proofs/containers/bitset/ proves every clause under its clause name,
131# and its `impl` lemma carries them to the implementation.
132#
133# Contracts of the bitset in the style of SPARK's formal ordered sets
134# (SPARKlib src/full/spark-containers-formal-ordered_sets.ads, AdaCore/SPARKlib
135# 46ec319). A bitset over the universe [0, n) is the set of the indices of
136# its True bits: SPARK's Model (M.Set, membership) is inset, its Length is
137# the number of members (S.count), its Elements (the ascending sequence of
138# members) is S.members, and our length (the universe size n) is the
139# capacity. Each lemma is one Post clause of step; `impl` (via P.step_ok)
140# carries every clause to the implementation.
141#
142# SPARK subprogram (.ads line) ours clauses
143# Length (112) count count_result, count_frame
144# Capacity length length_result, length_frame
145# Empty_Set (99) new n new_contains, new_count, new_length
146# Contains (1717) get get_result, get_frame, get_outside
147# Include (831) / Insert (777) set set_contains, set_others,
148# set_count, set_universe, set_outside
149# Exclude (953) / Delete (1051) clear clear_contains, clear_others,
150# clear_count, clear_universe, clear_outside
151# Union (1235) union union_contains, union_mismatch
152# Intersection (1307) intersection intersection_contains, intersection_mismatch
153# Difference (1369) difference difference_contains, difference_mismatch
154# Symmetric_Difference (1451) xor symmetric_difference_contains, xor_mismatch
155# Elements / iteration (Iter_Model) to_list to_list_result, to_list_frame,
156# elements_contains, elements_length
157# implementation B.step impl
158# Insert's and Delete's Pre (not Contains / Contains) select one case of
159# set_count / clear_count; Include's and Exclude's Contract_Cases are the two
160# cases of the pick. Not in this API: "=", Equivalent_Sets, To_Set,
161# Assign/Copy/Move, Element/Replace_Element/Replace (a member is its index),
162# Delete_First/Delete_Last, the Union/Intersection/... functions that return
163# a new set ("or", "and", "-", "xor": the procedures above), Overlap,
164# Is_Subset, First/First_Element/Last/Last_Element, Next/Previous,
165# Find/Floor/Ceiling (no cursors), Has_Element. SPARK's Pre on the index
166# (in range) is a defensive check: out of range the operation returns
167# IndexOutOfRange and changes nothing; binary operations on sets of
168# different sizes return LengthMismatch and change nothing.
169
170def ins(x: Maybe<&2, Bool>) -> Bool:
171 match x:
172 case None{}:
173 False{}
174 case Some{b}:
175 b
176
177# Contains (Model, k)
178def inset(xs: List<&2, Bool>, k: Nat) -> Bool:
179 ins(C.nth(Bool, xs, k))
180
181def nx(+xs: List<&2, Bool>, +op: E.Op) -> List<&2, Bool>:
182 Pair.fst(List<&2, Bool>, E.Obs, step(xs, op))
183
184def ob(+xs: List<&2, Bool>, +op: E.Op) -> E.Obs:
185 Pair.snd(List<&2, Bool>, E.Obs, step(xs, op))
186
187# ---- Elements: to_list is the ascending sequence of the members ----
188def nmem(+k: Nat, ys: List<&2, Nat>) -> Bool:
189 match ys:
190 case Nil{}:
191 False{}
192 case Con{+h, t}:
193 Bool.or(Nat.is_eq(h, k), nmem(k, t))
194
195# Contains (1717)
196def Contains.get_result(+xs: List<&2, Bool>, +i: Nat, +h: {Nat.is_lt(i, C.length(Bool, xs)) == True{} : Bool}) -> Type:
197 {ob(xs, E.Get{i}) == E.OBit{Done{inset(xs, i)}} : E.Obs}
198
199# Contains (1717)
200def Contains.get_frame(+xs: List<&2, Bool>, +i: Nat) -> Type:
201 {nx(xs, E.Get{i}) == xs : List<&2, Bool>}
202
203# Contains (1717)
204def Contains.get_outside(+xs: List<&2, Bool>, +i: Nat, +h: {Nat.is_le(C.length(Bool, xs), i) == True{} : Bool}) -> Type:
205 {ob(xs, E.Get{i}) == E.OBit{Fail{E.IndexOutOfRange{}}} : E.Obs}
206
207# Length (112)
208def Length.count_result(+xs: List<&2, Bool>) -> Type:
209 {ob(xs, E.Count{}) == E.ONat{count(xs)} : E.Obs}
210
211# Length (112)
212def Length.count_frame(+xs: List<&2, Bool>) -> Type:
213 {nx(xs, E.Count{}) == xs : List<&2, Bool>}
214
215# Capacity
216def Capacity.length_result(+xs: List<&2, Bool>) -> Type:
217 {ob(xs, E.Length{}) == E.ONat{C.length(Bool, xs)} : E.Obs}
218
219# Capacity
220def Capacity.length_frame(+xs: List<&2, Bool>) -> Type:
221 {nx(xs, E.Length{}) == xs : List<&2, Bool>}
222
223# Empty_Set (99)
224def Empty_Set.new_contains(+n: Nat, +k: Nat) -> Type:
225 {inset(new(n), k) == False{} : Bool}
226
227# Empty_Set (99)
228def Empty_Set.new_count(+n: Nat) -> Type:
229 {count(new(n)) == 0n : Nat}
230
231# Empty_Set (99)
232def Empty_Set.new_length(+n: Nat) -> Type:
233 {C.length(Bool, new(n)) == n : Nat}
234
235# Include (831) / Insert (777)
236def Include.set_contains(+xs: List<&2, Bool>, +i: Nat, +h: {Nat.is_lt(i, C.length(Bool, xs)) == True{} : Bool}) -> Type:
237 {inset(nx(xs, E.Set{i}), i) == True{} : Bool}
238
239# Include (831) / Insert (777)
240def Include.set_others(+xs: List<&2, Bool>, +i: Nat, +h: {Nat.is_lt(i, C.length(Bool, xs)) == True{} : Bool}, +j: Nat, +ne: {Nat.is_eq(i, j) == False{} : Bool}) -> Type:
241 {inset(nx(xs, E.Set{i}), j) == inset(xs, j) : Bool}
242
243# Include (831) / Insert (777)
244def Include.set_universe(+xs: List<&2, Bool>, +i: Nat, +h: {Nat.is_lt(i, C.length(Bool, xs)) == True{} : Bool}) -> Type:
245 {C.length(Bool, nx(xs, E.Set{i})) == C.length(Bool, xs) : Nat}
246
247# Include (831) / Insert (777)
248def Include.set_outside(+xs: List<&2, Bool>, +i: Nat, +h: {Nat.is_le(C.length(Bool, xs), i) == True{} : Bool}) -> Type:
249 {step(xs, E.Set{i}) == (xs, E.OUnit{Fail{E.IndexOutOfRange{}}}) : List<&2, Bool> & E.Obs}
250
251# Exclude (953) / Delete (1051)
252def Exclude.clear_contains(+xs: List<&2, Bool>, +i: Nat, +h: {Nat.is_lt(i, C.length(Bool, xs)) == True{} : Bool}) -> Type:
253 {inset(nx(xs, E.Clear{i}), i) == False{} : Bool}
254
255# Exclude (953) / Delete (1051)
256def Exclude.clear_others(+xs: List<&2, Bool>, +i: Nat, +h: {Nat.is_lt(i, C.length(Bool, xs)) == True{} : Bool}, +j: Nat, +ne: {Nat.is_eq(i, j) == False{} : Bool}) -> Type:
257 {inset(nx(xs, E.Clear{i}), j) == inset(xs, j) : Bool}
258
259# Exclude (953) / Delete (1051)
260def Exclude.clear_universe(+xs: List<&2, Bool>, +i: Nat, +h: {Nat.is_lt(i, C.length(Bool, xs)) == True{} : Bool}) -> Type:
261 {C.length(Bool, nx(xs, E.Clear{i})) == C.length(Bool, xs) : Nat}
262
263# Exclude (953) / Delete (1051)
264def Exclude.clear_outside(+xs: List<&2, Bool>, +i: Nat, +h: {Nat.is_le(C.length(Bool, xs), i) == True{} : Bool}) -> Type:
265 {step(xs, E.Clear{i}) == (xs, E.OUnit{Fail{E.IndexOutOfRange{}}}) : List<&2, Bool> & E.Obs}
266
267# Include (831) / Insert (777)
268def Include.set_count(+xs: List<&2, Bool>, +i: Nat, +h: {Nat.is_lt(i, C.length(Bool, xs)) == True{} : Bool}) -> Type:
269 {count(nx(xs, E.Set{i})) == Bool.pick(Nat, inset(xs, i), count(xs), 1n+count(xs)) : Nat}
270
271# Exclude (953) / Delete (1051)
272def Exclude.clear_count(+xs: List<&2, Bool>, +i: Nat, +h: {Nat.is_lt(i, C.length(Bool, xs)) == True{} : Bool}) -> Type:
273 {count(xs) == Bool.pick(Nat, inset(xs, i), 1n+count(nx(xs, E.Clear{i})), count(nx(xs, E.Clear{i}))) : Nat}
274
275# Union (1235)
276def Union.union_contains(+xs: List<&2, Bool>, +ys: List<&2, Bool>, +k: Nat, +h: {C.length(Bool, xs) == C.length(Bool, ys) : Nat}) -> Type:
277 {inset(nx(xs, E.Union{ys}), k) == Bool.or(inset(xs, k), inset(ys, k)) : Bool}
278
279# Union (1235)
280def Union.union_mismatch(+xs: List<&2, Bool>, +ys: List<&2, Bool>, +h: {Nat.is_eq(C.length(Bool, xs), C.length(Bool, ys)) == False{} : Bool}) -> Type:
281 {step(xs, E.Union{ys}) == (xs, E.OUnit{Fail{E.LengthMismatch{}}}) : List<&2, Bool> & E.Obs}
282
283# Intersection (1307)
284def Intersection.intersection_contains(+xs: List<&2, Bool>, +ys: List<&2, Bool>, +k: Nat, +h: {C.length(Bool, xs) == C.length(Bool, ys) : Nat}) -> Type:
285 {inset(nx(xs, E.Intersection{ys}), k) == Bool.and(inset(xs, k), inset(ys, k)) : Bool}
286
287# Intersection (1307)
288def Intersection.intersection_mismatch(+xs: List<&2, Bool>, +ys: List<&2, Bool>, +h: {Nat.is_eq(C.length(Bool, xs), C.length(Bool, ys)) == False{} : Bool}) -> Type:
289 {step(xs, E.Intersection{ys}) == (xs, E.OUnit{Fail{E.LengthMismatch{}}}) : List<&2, Bool> & E.Obs}
290
291# Difference (1369)
292def Difference.difference_contains(+xs: List<&2, Bool>, +ys: List<&2, Bool>, +k: Nat, +h: {C.length(Bool, xs) == C.length(Bool, ys) : Nat}) -> Type:
293 {inset(nx(xs, E.Difference{ys}), k) == Bool.and(inset(xs, k), Bool.not(inset(ys, k))) : Bool}
294
295# Difference (1369)
296def Difference.difference_mismatch(+xs: List<&2, Bool>, +ys: List<&2, Bool>, +h: {Nat.is_eq(C.length(Bool, xs), C.length(Bool, ys)) == False{} : Bool}) -> Type:
297 {step(xs, E.Difference{ys}) == (xs, E.OUnit{Fail{E.LengthMismatch{}}}) : List<&2, Bool> & E.Obs}
298
299# Symmetric_Difference (1451)
300def Symmetric_Difference.symmetric_difference_contains(+xs: List<&2, Bool>, +ys: List<&2, Bool>, +k: Nat, +h: {C.length(Bool, xs) == C.length(Bool, ys) : Nat}) -> Type:
301 {inset(nx(xs, E.Xor{ys}), k) == Bool.xor(inset(xs, k), inset(ys, k)) : Bool}
302
303# Symmetric_Difference (1451)
304def Symmetric_Difference.xor_mismatch(+xs: List<&2, Bool>, +ys: List<&2, Bool>, +h: {Nat.is_eq(C.length(Bool, xs), C.length(Bool, ys)) == False{} : Bool}) -> Type:
305 {step(xs, E.Xor{ys}) == (xs, E.OUnit{Fail{E.LengthMismatch{}}}) : List<&2, Bool> & E.Obs}
306
307# Elements / iteration (Iter_Model)
308def Elements.to_list_result(+xs: List<&2, Bool>) -> Type:
309 {ob(xs, E.ToList{}) == E.OList{members(xs, 0n)} : E.Obs}
310
311# Elements / iteration (Iter_Model)
312def Elements.to_list_frame(+xs: List<&2, Bool>) -> Type:
313 {nx(xs, E.ToList{}) == xs : List<&2, Bool>}
314
315# Elements / iteration (Iter_Model)
316def Elements.elements_contains(+xs: List<&2, Bool>, +k: Nat) -> Type:
317 {nmem(k, members(xs, 0n)) == inset(xs, k) : Bool}
318
319# Elements / iteration (Iter_Model)
320def Elements.elements_length(+xs: List<&2, Bool>, +off: Nat) -> Type:
321 {C.length(Nat, members(xs, off)) == count(xs) : Nat}