1	import Base
2	import ../../../src/containers/bitset.bend as B
3	
4	# The word-list model of the packed representation.
5	#
6	# src/bitset.bend stores the words in a native Base.Array and addresses them
7	# by index; the mathematics of "what the words mean" is easier to state over
8	# the list of stored words, so these are the list-level counterparts of the
9	# runtime walks. proofs/bitset/arr.bend proves that each runtime operation
10	# does exactly what the corresponding function here says, on the list of the
11	# array's slots, and proofs/bitset/state.bend then relates that list to the
12	# independent bit-sequence specification.
13	#
14	# These definitions are the ones src/bitset.bend used before it moved to
15	# Base.Array, so every lemma of proofs/bitset/state.bend about them is the
16	# retained one.
17	
18	# Zero words covering n more bits; `free` counts unused bits left in the
19	# last emitted word, so exactly ceil(n/32) words are produced from free = 0.
20	def zeros(n: Nat, free: Nat) -> List<&2, U32>:
21	  match n free:
22	    case 0n _:
23	      Nil{}
24	    case 1n+p 0n:
25	      Con{0, zeros(p, 31n)}
26	    case 1n+p 1n+f:
27	      zeros(p, f)
28	
29	def get_pick(b: Bool, w: U32, +i: Nat, r: Bool) -> Bool:
30	  match b:
31	    case True{}:
32	      B.word_get(w, i)
33	    case False{}:
34	      r
35	
36	def get_walk(ws: List<&2, U32>, +i: Nat) -> Bool:
37	  match ws:
38	    case Nil{}:
39	      False{}
40	    case Con{w, t}:
41	      get_pick(Nat.is_lt(i, 32n), w, i, get_walk(t, Nat.sub(i, 32n)))
42	
43	def put_pick(b: Bool, +v: Bool, +w: U32, +i: Nat, t: List<&2, U32>, r: List<&2, U32>) -> List<&2, U32>:
44	  match b:
45	    case True{}:
46	      Con{B.word_put(v, w, i), t}
47	    case False{}:
48	      Con{w, r}
49	
50	def put_walk(+ws: List<&2, U32>, +i: Nat, +v: Bool) -> List<&2, U32>:
51	  match ws:
52	    case Nil{}:
53	      Nil{}
54	    case Con{+w, +t}:
55	      put_pick(Nat.is_lt(i, 32n), v, w, i, t, put_walk(t, Nat.sub(i, 32n), v))
56	
57	def zip_words(+k: B.WordOp, ws: List<&2, U32>, vs: List<&2, U32>) -> List<&2, U32>:
58	  match ws vs:
59	    case Con{a, s} Con{b, t}:
60	      Con{B.word_op(k, a, b), zip_words(k, s, t)}
61	    case _ _:
62	      Nil{}
63	
64	def count_words(ws: List<&2, U32>) -> Nat:
65	  match ws:
66	    case Nil{}:
67	      0n
68	    case Con{w, t}:
69	      Nat.add(B.word_count(32n, w), count_words(t))
70	
71	def members_words(ws: List<&2, U32>, +off: Nat) -> List<&2, Nat>:
72	  match ws:
73	    case Nil{}:
74	      Nil{}
75	    case Con{w, t}:
76	      B.word_members(32n, w, off, members_words(t, Nat.add(32n, off)))
77