1	import Base
2	import ../../lib/logic.bend as L
3	import ../../lib/nat.bend as N
4	import ../../lib/list.bend as LL
5	import ../../../spec/lib/common.bend as SC
6	import ../../../spec/containers/bitset.bend as S
7	import ../../../src/containers/bitset.bend as B
8	import ./lists.bend as BL
9	
10	# Bit-level meaning of the native U32 operations used by src/bitset.bend,
11	# derived from Base's Word definitions (U32 = U32{Word(32n)}, bit 0 first).
12	
13	def wbits(n: Nat, w: Word(n)) -> List<&2, Bool>:
14	  match n:
15	    case 0n:
16	      Nil{}
17	    case 1n+p:
18	      match w:
19	        case WCon{b, t}:
20	          Con{b, wbits(p, t)}
21	
22	def ubits(x: U32) -> List<&2, Bool>:
23	  match x:
24	    case U32{w}:
25	      wbits(32n, w)
26	
27	def len_wbits(+n: Nat, +w: Word(n)) -> {SC.length(Bool, wbits(n, w)) == n : Nat}:
28	  match n:
29	    case 0n:
30	      {==}
31	    case 1n+p:
32	      match w:
33	        case WCon{b, t}:
34	          N.succ_cong(SC.length(Bool, wbits(p, t)), p, len_wbits(p, t))
35	
36	def ulen(+x: U32) -> {SC.length(Bool, ubits(x)) == 32n : Nat}:
37	  match x:
38	    case U32{w}:
39	      len_wbits(32n, w)
40	
41	# ---- bitwise operations are element-wise ----
42	
43	def w_or(+n: Nat, +a: Word(n), +b: Word(n)) -> {wbits(n, Word.or(n, a, b)) == BL.zipk(B.KOr{}, wbits(n, a), wbits(n, b)) : List<&2, Bool>}:
44	  match n:
45	    case 0n:
46	      {==}
47	    case 1n+p:
48	      match a b:
49	        case WCon{x, s} WCon{y, t}:
50	          LL.cons_cong(Bool, Bool.or(x, y), wbits(p, Word.or(p, s, t)), BL.zipk(B.KOr{}, wbits(p, s), wbits(p, t)), w_or(p, s, t))
51	
52	def w_and(+n: Nat, +a: Word(n), +b: Word(n)) -> {wbits(n, Word.and(n, a, b)) == BL.zipk(B.KAnd{}, wbits(n, a), wbits(n, b)) : List<&2, Bool>}:
53	  match n:
54	    case 0n:
55	      {==}
56	    case 1n+p:
57	      match a b:
58	        case WCon{x, s} WCon{y, t}:
59	          LL.cons_cong(Bool, Bool.and(x, y), wbits(p, Word.and(p, s, t)), BL.zipk(B.KAnd{}, wbits(p, s), wbits(p, t)), w_and(p, s, t))
60	
61	def w_diff(+n: Nat, +a: Word(n), +b: Word(n)) -> {wbits(n, Word.and(n, a, Word.not(n, b))) == BL.zipk(B.KDiff{}, wbits(n, a), wbits(n, b)) : List<&2, Bool>}:
62	  match n:
63	    case 0n:
64	      {==}
65	    case 1n+p:
66	      match a b:
67	        case WCon{x, s} WCon{y, t}:
68	          LL.cons_cong(Bool, Bool.and(x, Bool.not(y)), wbits(p, Word.and(p, s, Word.not(p, t))), BL.zipk(B.KDiff{}, wbits(p, s), wbits(p, t)), w_diff(p, s, t))
69	
70	def w_xor(+n: Nat, +a: Word(n), +b: Word(n)) -> {wbits(n, Word.xor(n, a, b)) == BL.zipk(B.KXor{}, wbits(n, a), wbits(n, b)) : List<&2, Bool>}:
71	  match n:
72	    case 0n:
73	      {==}
74	    case 1n+p:
75	      match a b:
76	        case WCon{x, s} WCon{y, t}:
77	          LL.cons_cong(Bool, Bool.xor(x, y), wbits(p, Word.xor(p, s, t)), BL.zipk(B.KXor{}, wbits(p, s), wbits(p, t)), w_xor(p, s, t))
78	
79	def u_op(+k: B.WordOp, +a: U32, +b: U32) -> {ubits(B.word_op(k, a, b)) == BL.zipk(k, ubits(a), ubits(b)) : List<&2, Bool>}:
80	  match k a b:
81	    case B.KOr{} U32{x} U32{y}:
82	      w_or(32n, x, y)
83	    case B.KAnd{} U32{x} U32{y}:
84	      w_and(32n, x, y)
85	    case B.KDiff{} U32{x} U32{y}:
86	      w_diff(32n, x, y)
87	    case B.KXor{} U32{x} U32{y}:
88	      w_xor(32n, x, y)
89	
90	# ---- low bit ----
91	
92	def and_zero(+n: Nat, +t: Word(n)) -> {Word.and(n, t, Word.zero(n)) == Word.zero(n) : Word(n)}:
93	  match n:
94	    case 0n:
95	      match t:
96	        case WNil{}:
97	          {==}
98	    case 1n+p:
99	      match t:
100	        case WCon{True{}, r}:
101	          %Equal.sym(Word(p), Word.and(p, r, Word.zero(p)), Word.zero(p), and_zero(p, r)) : {WCon{False{}, _} == WCon{False{}, Word.zero(p)} : Word(1n+p)}
102	          {==}
103	        case WCon{False{}, r}:
104	          %Equal.sym(Word(p), Word.and(p, r, Word.zero(p)), Word.zero(p), and_zero(p, r)) : {WCon{False{}, _} == WCon{False{}, Word.zero(p)} : Word(1n+p)}
105	          {==}
106	
107	def low_word(+b: Bool, +t: Word(31n)) -> {B.low(U32{WCon{b, t}}) == b : Bool}:
108	  match b:
109	    case True{}:
110	      %Equal.sym(Word(31n), Word.and(31n, t, Word.zero(31n)), Word.zero(31n), and_zero(31n, t)) : {Bool.not(U32.is_eq(U32{WCon{True{}, _}}, 0)) == True{} : Bool}
111	      {==}
112	    case False{}:
113	      %Equal.sym(Word(31n), Word.and(31n, t, Word.zero(31n)), Word.zero(31n), and_zero(31n, t)) : {Bool.not(U32.is_eq(U32{WCon{False{}, _}}, 0)) == False{} : Bool}
114	      {==}
115	
116	def low_nth(+x: U32) -> {SC.nth(Bool, ubits(x), 0n) == Some{B.low(x)} : Maybe<&2, Bool>}:
117	  match x:
118	    case U32{w}:
119	      match w:
120	        case WCon{b, t}:
121	          %Equal.sym(Bool, B.low(U32{WCon{b, t}}), b, low_word(b, t)) : {Some{b} == Some{_} : Maybe<&2, Bool>}
122	          {==}
123	
124	# ---- shifts ----
125	
126	def pad(+n: Nat, +w: Word(n)) -> {wbits(1n+n, Word.shr.pad(n, w)) == SC.snoc(Bool, wbits(n, w), False{}) : List<&2, Bool>}:
127	  match n:
128	    case 0n:
129	      match w:
130	        case WNil{}:
131	          {==}
132	    case 1n+p:
133	      match w:
134	        case WCon{b, t}:
135	          LL.cons_cong(Bool, b, wbits(1n+p, Word.shr.pad(p, t)), SC.snoc(Bool, wbits(p, t), False{}), pad(p, t))
136	
137	def u_shr(+b: Bool, +t: Word(31n)) -> {ubits(U32.shr(U32{WCon{b, t}})) == SC.snoc(Bool, wbits(31n, t), False{}) : List<&2, Bool>}:
138	  pad(31n, t)
139	
140	def shr_nth(+x: U32, +j: Nat, +h: {Nat.is_lt(j, 31n) == True{} : Bool}) -> {SC.nth(Bool, ubits(U32.shr(x)), j) == SC.nth(Bool, ubits(x), 1n+j) : Maybe<&2, Bool>}:
141	  match x:
142	    case U32{w}:
143	      match w:
144	        case WCon{b, t}:
145	          %Equal.sym(List<&2, Bool>, ubits(U32.shr(U32{WCon{b, t}})), SC.snoc(Bool, wbits(31n, t), False{}), u_shr(b, t)) : {SC.nth(Bool, _, j) == SC.nth(Bool, wbits(31n, t), j) : Maybe<&2, Bool>}
146	          %Equal.sym(List<&2, Bool>, SC.snoc(Bool, wbits(31n, t), False{}), SC.append(Bool, wbits(31n, t), Con{False{}, Nil{}}), LL.snoc_append(Bool, wbits(31n, t), False{})) : {SC.nth(Bool, _, j) == SC.nth(Bool, wbits(31n, t), j) : Maybe<&2, Bool>}
147	          LL.nth_append_left(Bool, wbits(31n, t), Con{False{}, Nil{}}, j, L.subst(Nat, x => {Nat.is_lt(j, x) == True{} : Bool}, 31n, SC.length(Bool, wbits(31n, t)), Equal.sym(Nat, SC.length(Bool, wbits(31n, t)), 31n, len_wbits(31n, t)), h))
148	
149	def shrn_nth(+k: Nat, +x: U32, +j: Nat, +h: {Nat.is_lt(Nat.add(j, k), 32n) == True{} : Bool}) -> {SC.nth(Bool, ubits(U32.shrn(x, k)), j) == SC.nth(Bool, ubits(x), Nat.add(j, k)) : Maybe<&2, Bool>}:
150	  match k:
151	    case 0n:
152	      %Equal.sym(Nat, Nat.add(j, 0n), j, N.add_zero(j)) : {SC.nth(Bool, ubits(x), j) == SC.nth(Bool, ubits(x), _) : Maybe<&2, Bool>}
153	      {==}
154	    case 1n+p:
155	      %Equal.sym(Nat, Nat.add(j, 1n+p), 1n+Nat.add(j, p), N.add_succ(j, p)) : {SC.nth(Bool, ubits(U32.shr(U32.shrn(x, p))), j) == SC.nth(Bool, ubits(x), _) : Maybe<&2, Bool>}
156	      +h1 = L.subst(Nat, v => {Nat.is_lt(v, 32n) == True{} : Bool}, Nat.add(j, 1n+p), 1n+Nat.add(j, p), N.add_succ(j, p), h)
157	      Equal.trans(Maybe<&2, Bool>, SC.nth(Bool, ubits(U32.shr(U32.shrn(x, p))), j), SC.nth(Bool, ubits(U32.shrn(x, p)), 1n+j), SC.nth(Bool, ubits(x), 1n+Nat.add(j, p)),
158	        shr_nth(U32.shrn(x, p), j, N.le_lt_trans(j, Nat.add(j, p), 31n, N.le_add_right(j, p), h1)),
159	        shrn_nth(p, x, 1n+j, h1))
160	
161	def word_get(+w: U32, +k: Nat, +h: {Nat.is_lt(k, 32n) == True{} : Bool}) -> {Some{B.word_get(w, k)} == SC.nth(Bool, ubits(w), k) : Maybe<&2, Bool>}:
162	  Equal.trans(Maybe<&2, Bool>, Some{B.low(U32.shrn(w, k))}, SC.nth(Bool, ubits(U32.shrn(w, k)), 0n), SC.nth(Bool, ubits(w), k),
163	    Equal.sym(Maybe<&2, Bool>, SC.nth(Bool, ubits(U32.shrn(w, k)), 0n), Some{B.low(U32.shrn(w, k))}, low_nth(U32.shrn(w, k))),
164	    shrn_nth(k, w, 0n, h))
165	
166	def shl_put(+n: Nat, +c: Bool, +w: Word(n)) -> {wbits(n, Word.shl.put(n, c, w)) == SC.take(Bool, Con{c, wbits(n, w)}, n) : List<&2, Bool>}:
167	  match n:
168	    case 0n:
169	      {==}
170	    case 1n+p:
171	      match w:
172	        case WCon{b, t}:
173	          LL.cons_cong(Bool, c, wbits(p, Word.shl.put(p, b, t)), SC.take(Bool, Con{b, wbits(p, t)}, p), shl_put(p, b, t))
174	
175	def u_shl(+x: U32) -> {ubits(U32.shl(x)) == SC.take(Bool, Con{False{}, ubits(x)}, 32n) : List<&2, Bool>}:
176	  match x:
177	    case U32{w}:
178	      match w:
179	        case WCon{b, t}:
180	          LL.cons_cong(Bool, False{}, wbits(31n, Word.shl.put(31n, b, t)), SC.take(Bool, Con{b, wbits(31n, t)}, 31n), shl_put(31n, b, t))
181	
182	# 1 << k is the one-hot mask for bit k.
183	def onehot(+k: Nat, +h: {Nat.is_lt(k, 32n) == True{} : Bool}) -> {ubits(U32.shln(1, k)) == SC.update(Bool, BL.rep(32n), k, True{}) : List<&2, Bool>}:
184	  match k:
185	    case 0n:
186	      {==}
187	    case 1n+p:
188	      +hp = N.lt_trans(p, 1n+p, 32n, N.lt_succ(p), h)
189	      %Equal.sym(List<&2, Bool>, ubits(U32.shl(U32.shln(1, p))), SC.take(Bool, Con{False{}, ubits(U32.shln(1, p))}, 32n), u_shl(U32.shln(1, p))) : {_ == SC.update(Bool, BL.rep(32n), 1n+p, True{}) : List<&2, Bool>}
190	      %Equal.sym(List<&2, Bool>, ubits(U32.shln(1, p)), SC.update(Bool, BL.rep(32n), p, True{}), onehot(p, hp)) : {SC.take(Bool, Con{False{}, _}, 32n) == SC.update(Bool, BL.rep(32n), 1n+p, True{}) : List<&2, Bool>}
191	      LL.cons_cong(Bool, False{}, SC.take(Bool, SC.update(Bool, BL.rep(32n), p, True{}), 31n), SC.update(Bool, BL.rep(31n), p, True{}), BL.take_onehot(31n, p, h))
192	
193	def word_put(+v: Bool, +w: U32, +k: Nat, +h: {Nat.is_lt(k, 32n) == True{} : Bool}) -> {ubits(B.word_put(v, w, k)) == SC.update(Bool, ubits(w), k, v) : List<&2, Bool>}:
194	  match v:
195	    case True{}:
196	      %Equal.sym(List<&2, Bool>, ubits(B.word_op(B.KOr{}, w, U32.shln(1, k))), BL.zipk(B.KOr{}, ubits(w), ubits(U32.shln(1, k))), u_op(B.KOr{}, w, U32.shln(1, k))) : {_ == SC.update(Bool, ubits(w), k, True{}) : List<&2, Bool>}
197	      %Equal.sym(List<&2, Bool>, ubits(U32.shln(1, k)), SC.update(Bool, BL.rep(32n), k, True{}), onehot(k, h)) : {BL.zipk(B.KOr{}, ubits(w), _) == SC.update(Bool, ubits(w), k, True{}) : List<&2, Bool>}
198	      %ulen(w) : {BL.zipk(B.KOr{}, ubits(w), SC.update(Bool, BL.rep(_), k, True{})) == SC.update(Bool, ubits(w), k, True{}) : List<&2, Bool>}
199	      BL.or_onehot(ubits(w), k)
200	    case False{}:
201	      %Equal.sym(List<&2, Bool>, ubits(B.word_op(B.KDiff{}, w, U32.shln(1, k))), BL.zipk(B.KDiff{}, ubits(w), ubits(U32.shln(1, k))), u_op(B.KDiff{}, w, U32.shln(1, k))) : {_ == SC.update(Bool, ubits(w), k, False{}) : List<&2, Bool>}
202	      %Equal.sym(List<&2, Bool>, ubits(U32.shln(1, k)), SC.update(Bool, BL.rep(32n), k, True{}), onehot(k, h)) : {BL.zipk(B.KDiff{}, ubits(w), _) == SC.update(Bool, ubits(w), k, False{}) : List<&2, Bool>}
203	      %ulen(w) : {BL.zipk(B.KDiff{}, ubits(w), SC.update(Bool, BL.rep(_), k, True{})) == SC.update(Bool, ubits(w), k, False{}) : List<&2, Bool>}
204	      BL.diff_onehot(ubits(w), k)
205	
206	# ---- counting and enumeration by repeated shifting ----
207	
208	def word_count(+m: Nat, +x: U32) -> {B.word_count(m, x) == S.count(SC.take(Bool, ubits(x), m)) : Nat}:
209	  match m x:
210	    case 0n U32{w}:
211	      match w:
212	        case WCon{b, t}:
213	          {==}
214	    case 1n+p U32{w}:
215	      match w:
216	        case WCon{True{}, t}:
217	          %Equal.sym(Bool, B.low(U32{WCon{True{}, t}}), True{}, low_word(True{}, t)) : {Nat.add(B.bit_value(_), B.word_count(p, U32.shr(U32{WCon{True{}, t}}))) == 1n+S.count(SC.take(Bool, wbits(31n, t), p)) : Nat}
218	          %Equal.sym(Nat, B.word_count(p, U32.shr(U32{WCon{True{}, t}})), S.count(SC.take(Bool, ubits(U32.shr(U32{WCon{True{}, t}})), p)), word_count(p, U32.shr(U32{WCon{True{}, t}}))) : {1n+_ == 1n+S.count(SC.take(Bool, wbits(31n, t), p)) : Nat}
219	          %Equal.sym(List<&2, Bool>, ubits(U32.shr(U32{WCon{True{}, t}})), SC.snoc(Bool, wbits(31n, t), False{}), u_shr(True{}, t)) : {1n+S.count(SC.take(Bool, _, p)) == 1n+S.count(SC.take(Bool, wbits(31n, t), p)) : Nat}
220	          N.succ_cong(S.count(SC.take(Bool, SC.snoc(Bool, wbits(31n, t), False{}), p)), S.count(SC.take(Bool, wbits(31n, t), p)), BL.count_take_snoc(wbits(31n, t), p))
221	        case WCon{False{}, t}:
222	          %Equal.sym(Bool, B.low(U32{WCon{False{}, t}}), False{}, low_word(False{}, t)) : {Nat.add(B.bit_value(_), B.word_count(p, U32.shr(U32{WCon{False{}, t}}))) == S.count(SC.take(Bool, wbits(31n, t), p)) : Nat}
223	          %Equal.sym(Nat, B.word_count(p, U32.shr(U32{WCon{False{}, t}})), S.count(SC.take(Bool, ubits(U32.shr(U32{WCon{False{}, t}})), p)), word_count(p, U32.shr(U32{WCon{False{}, t}}))) : {_ == S.count(SC.take(Bool, wbits(31n, t), p)) : Nat}
224	          %Equal.sym(List<&2, Bool>, ubits(U32.shr(U32{WCon{False{}, t}})), SC.snoc(Bool, wbits(31n, t), False{}), u_shr(False{}, t)) : {S.count(SC.take(Bool, _, p)) == S.count(SC.take(Bool, wbits(31n, t), p)) : Nat}
225	          BL.count_take_snoc(wbits(31n, t), p)
226	
227	def word_members(+m: Nat, +x: U32, +off: Nat, +rest: List<&2, Nat>) -> {B.word_members(m, x, off, rest) == SC.append(Nat, S.members(SC.take(Bool, ubits(x), m), off), rest) : List<&2, Nat>}:
228	  match m x:
229	    case 0n U32{w}:
230	      match w:
231	        case WCon{b, t}:
232	          {==}
233	    case 1n+p U32{w}:
234	      match w:
235	        case WCon{True{}, t}:
236	          %Equal.sym(Bool, B.low(U32{WCon{True{}, t}}), True{}, low_word(True{}, t)) : {B.member_pick(_, off, B.word_members(p, U32.shr(U32{WCon{True{}, t}}), 1n+off, rest)) == Con{off, SC.append(Nat, S.members(SC.take(Bool, wbits(31n, t), p), 1n+off), rest)} : List<&2, Nat>}
237	          %Equal.sym(List<&2, Nat>, B.word_members(p, U32.shr(U32{WCon{True{}, t}}), 1n+off, rest), SC.append(Nat, S.members(SC.take(Bool, ubits(U32.shr(U32{WCon{True{}, t}})), p), 1n+off), rest), word_members(p, U32.shr(U32{WCon{True{}, t}}), 1n+off, rest)) : {Con{off, _} == Con{off, SC.append(Nat, S.members(SC.take(Bool, wbits(31n, t), p), 1n+off), rest)} : List<&2, Nat>}
238	          %Equal.sym(List<&2, Bool>, ubits(U32.shr(U32{WCon{True{}, t}})), SC.snoc(Bool, wbits(31n, t), False{}), u_shr(True{}, t)) : {Con{off, SC.append(Nat, S.members(SC.take(Bool, _, p), 1n+off), rest)} == Con{off, SC.append(Nat, S.members(SC.take(Bool, wbits(31n, t), p), 1n+off), rest)} : List<&2, Nat>}
239	          %Equal.sym(List<&2, Nat>, S.members(SC.take(Bool, SC.snoc(Bool, wbits(31n, t), False{}), p), 1n+off), S.members(SC.take(Bool, wbits(31n, t), p), 1n+off), BL.members_take_snoc(wbits(31n, t), p, 1n+off)) : {Con{off, SC.append(Nat, _, rest)} == Con{off, SC.append(Nat, S.members(SC.take(Bool, wbits(31n, t), p), 1n+off), rest)} : List<&2, Nat>}
240	          {==}
241	        case WCon{False{}, t}:
242	          %Equal.sym(Bool, B.low(U32{WCon{False{}, t}}), False{}, low_word(False{}, t)) : {B.member_pick(_, off, B.word_members(p, U32.shr(U32{WCon{False{}, t}}), 1n+off, rest)) == SC.append(Nat, S.members(SC.take(Bool, wbits(31n, t), p), 1n+off), rest) : List<&2, Nat>}
243	          %Equal.sym(List<&2, Nat>, B.word_members(p, U32.shr(U32{WCon{False{}, t}}), 1n+off, rest), SC.append(Nat, S.members(SC.take(Bool, ubits(U32.shr(U32{WCon{False{}, t}})), p), 1n+off), rest), word_members(p, U32.shr(U32{WCon{False{}, t}}), 1n+off, rest)) : {_ == SC.append(Nat, S.members(SC.take(Bool, wbits(31n, t), p), 1n+off), rest) : List<&2, Nat>}
244	          %Equal.sym(List<&2, Bool>, ubits(U32.shr(U32{WCon{False{}, t}})), SC.snoc(Bool, wbits(31n, t), False{}), u_shr(False{}, t)) : {SC.append(Nat, S.members(SC.take(Bool, _, p), 1n+off), rest) == SC.append(Nat, S.members(SC.take(Bool, wbits(31n, t), p), 1n+off), rest) : List<&2, Nat>}
245	          %Equal.sym(List<&2, Nat>, S.members(SC.take(Bool, SC.snoc(Bool, wbits(31n, t), False{}), p), 1n+off), S.members(SC.take(Bool, wbits(31n, t), p), 1n+off), BL.members_take_snoc(wbits(31n, t), p, 1n+off)) : {SC.append(Nat, _, rest) == SC.append(Nat, S.members(SC.take(Bool, wbits(31n, t), p), 1n+off), rest) : List<&2, Nat>}
246	          {==}