1	import Base
2	import ../lib/common.bend as C
3	import ../../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	
8	def new(n: Nat) -> List<&2, Bool>:
9	  C.replicate(Bool, n, False{})
10	
11	# Number of True bits.
12	def 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.
22	def 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).
32	def 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	
39	def 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	
46	def 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	
53	def 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	
60	def 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	
67	def 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.
71	def 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	
78	def 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.
83	def 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	
90	def 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	
93	def 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	
116	def 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	
120	def 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	
170	def 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)
178	def inset(xs: List<&2, Bool>, k: Nat) -> Bool:
179	  ins(C.nth(Bool, xs, k))
180	
181	def nx(+xs: List<&2, Bool>, +op: E.Op) -> List<&2, Bool>:
182	  Pair.fst(List<&2, Bool>, E.Obs, step(xs, op))
183	
184	def 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 ----
188	def 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)
196	def 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)
200	def Contains.get_frame(+xs: List<&2, Bool>, +i: Nat) -> Type:
201	  {nx(xs, E.Get{i}) == xs : List<&2, Bool>}
202	
203	# Contains (1717)
204	def 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)
208	def Length.count_result(+xs: List<&2, Bool>) -> Type:
209	  {ob(xs, E.Count{}) == E.ONat{count(xs)} : E.Obs}
210	
211	# Length (112)
212	def Length.count_frame(+xs: List<&2, Bool>) -> Type:
213	  {nx(xs, E.Count{}) == xs : List<&2, Bool>}
214	
215	# Capacity
216	def Capacity.length_result(+xs: List<&2, Bool>) -> Type:
217	  {ob(xs, E.Length{}) == E.ONat{C.length(Bool, xs)} : E.Obs}
218	
219	# Capacity
220	def Capacity.length_frame(+xs: List<&2, Bool>) -> Type:
221	  {nx(xs, E.Length{}) == xs : List<&2, Bool>}
222	
223	# Empty_Set (99)
224	def Empty_Set.new_contains(+n: Nat, +k: Nat) -> Type:
225	  {inset(new(n), k) == False{} : Bool}
226	
227	# Empty_Set (99)
228	def Empty_Set.new_count(+n: Nat) -> Type:
229	  {count(new(n)) == 0n : Nat}
230	
231	# Empty_Set (99)
232	def Empty_Set.new_length(+n: Nat) -> Type:
233	  {C.length(Bool, new(n)) == n : Nat}
234	
235	# Include (831) / Insert (777)
236	def 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)
240	def 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)
244	def 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)
248	def 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)
252	def 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)
256	def 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)
260	def 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)
264	def 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)
268	def 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)
272	def 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)
276	def 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)
280	def 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)
284	def 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)
288	def 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)
292	def 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)
296	def 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)
300	def 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)
304	def 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)
308	def 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)
312	def Elements.to_list_frame(+xs: List<&2, Bool>) -> Type:
313	  {nx(xs, E.ToList{}) == xs : List<&2, Bool>}
314	
315	# Elements / iteration (Iter_Model)
316	def 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)
320	def Elements.elements_length(+xs: List<&2, Bool>, +off: Nat) -> Type:
321	  {C.length(Nat, members(xs, off)) == count(xs) : Nat}