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	
9	# Boolean-sequence facts used by the bitset proof: element-wise combination
10	# (zipk, indexed by the implementation's word-operation tag), all-False
11	# tails, counting and member enumeration over take/drop/append.
12	
13	def bop(k: B.WordOp, a: Bool, b: Bool) -> Bool:
14	  match k:
15	    case B.KOr{}:
16	      Bool.or(a, b)
17	    case B.KAnd{}:
18	      Bool.and(a, b)
19	    case B.KDiff{}:
20	      Bool.and(a, Bool.not(b))
21	    case B.KXor{}:
22	      Bool.xor(a, b)
23	
24	def zipk(+k: B.WordOp, xs: List<&2, Bool>, ys: List<&2, Bool>) -> List<&2, Bool>:
25	  match xs ys:
26	    case Nil{} _:
27	      Nil{}
28	    case Con{a, s} Nil{}:
29	      Nil{}
30	    case Con{a, s} Con{b, t}:
31	      Con{bop(k, a, b), zipk(k, s, t)}
32	
33	def allf(xs: List<&2, Bool>) -> Bool:
34	  match xs:
35	    case Nil{}:
36	      True{}
37	    case Con{False{}, t}:
38	      allf(t)
39	    case Con{True{}, t}:
40	      False{}
41	
42	def rep(n: Nat) -> List<&2, Bool>:
43	  SC.replicate(Bool, n, False{})
44	
45	# ---- spec combinators are zipk instances ----
46	
47	def spec_or(+xs: List<&2, Bool>, +ys: List<&2, Bool>) -> {S.zip_or(xs, ys) == zipk(B.KOr{}, xs, ys) : List<&2, Bool>}:
48	  match xs ys:
49	    case Nil{} Nil{}:
50	      {==}
51	    case Nil{} Con{b, t}:
52	      {==}
53	    case Con{a, s} Nil{}:
54	      {==}
55	    case Con{a, s} Con{b, t}:
56	      LL.cons_cong(Bool, Bool.or(a, b), S.zip_or(s, t), zipk(B.KOr{}, s, t), spec_or(s, t))
57	
58	def spec_and(+xs: List<&2, Bool>, +ys: List<&2, Bool>) -> {S.zip_and(xs, ys) == zipk(B.KAnd{}, xs, ys) : List<&2, Bool>}:
59	  match xs ys:
60	    case Nil{} Nil{}:
61	      {==}
62	    case Nil{} Con{b, t}:
63	      {==}
64	    case Con{a, s} Nil{}:
65	      {==}
66	    case Con{a, s} Con{b, t}:
67	      LL.cons_cong(Bool, Bool.and(a, b), S.zip_and(s, t), zipk(B.KAnd{}, s, t), spec_and(s, t))
68	
69	def spec_diff(+xs: List<&2, Bool>, +ys: List<&2, Bool>) -> {S.zip_diff(xs, ys) == zipk(B.KDiff{}, xs, ys) : List<&2, Bool>}:
70	  match xs ys:
71	    case Nil{} Nil{}:
72	      {==}
73	    case Nil{} Con{b, t}:
74	      {==}
75	    case Con{a, s} Nil{}:
76	      {==}
77	    case Con{a, s} Con{b, t}:
78	      LL.cons_cong(Bool, Bool.and(a, Bool.not(b)), S.zip_diff(s, t), zipk(B.KDiff{}, s, t), spec_diff(s, t))
79	
80	def spec_xor(+xs: List<&2, Bool>, +ys: List<&2, Bool>) -> {S.zip_xor(xs, ys) == zipk(B.KXor{}, xs, ys) : List<&2, Bool>}:
81	  match xs ys:
82	    case Nil{} Nil{}:
83	      {==}
84	    case Nil{} Con{b, t}:
85	      {==}
86	    case Con{a, s} Nil{}:
87	      {==}
88	    case Con{a, s} Con{b, t}:
89	      LL.cons_cong(Bool, Bool.xor(a, b), S.zip_xor(s, t), zipk(B.KXor{}, s, t), spec_xor(s, t))
90	
91	# ---- zipk structure ----
92	
93	def zipk_nil_r(+k: B.WordOp, +xs: List<&2, Bool>) -> {zipk(k, xs, Nil{}) == Nil{} : List<&2, Bool>}:
94	  match xs:
95	    case Nil{}:
96	      {==}
97	    case Con{a, s}:
98	      {==}
99	
100	def zipk_append(+k: B.WordOp, +xs: List<&2, Bool>, +ys: List<&2, Bool>, +xs2: List<&2, Bool>, +ys2: List<&2, Bool>, +h: {SC.length(Bool, xs) == SC.length(Bool, ys) : Nat}) -> {zipk(k, SC.append(Bool, xs, xs2), SC.append(Bool, ys, ys2)) == SC.append(Bool, zipk(k, xs, ys), zipk(k, xs2, ys2)) : List<&2, Bool>}:
101	  match xs ys:
102	    case Nil{} Nil{}:
103	      {==}
104	    case Nil{} Con{b, t}:
105	      Empty.absurd({zipk(k, xs2, SC.append(Bool, Con{b, t}, ys2)) == zipk(k, xs2, ys2) : List<&2, Bool>}, N.zero_succ(SC.length(Bool, t), h))
106	    case Con{a, s} Nil{}:
107	      Empty.absurd({zipk(k, SC.append(Bool, Con{a, s}, xs2), ys2) == SC.append(Bool, zipk(k, Con{a, s}, Nil{}), zipk(k, xs2, ys2)) : List<&2, Bool>}, N.succ_zero(SC.length(Bool, s), h))
108	    case Con{a, s} Con{b, t}:
109	      LL.cons_cong(Bool, bop(k, a, b), zipk(k, SC.append(Bool, s, xs2), SC.append(Bool, t, ys2)), SC.append(Bool, zipk(k, s, t), zipk(k, xs2, ys2)), zipk_append(k, s, t, xs2, ys2, N.succ_inj(SC.length(Bool, s), SC.length(Bool, t), h)))
110	
111	def take_zipk(+k: B.WordOp, +xs: List<&2, Bool>, +ys: List<&2, Bool>, +n: Nat) -> {SC.take(Bool, zipk(k, xs, ys), n) == zipk(k, SC.take(Bool, xs, n), SC.take(Bool, ys, n)) : List<&2, Bool>}:
112	  match xs ys n:
113	    case Nil{} _ _:
114	      {==}
115	    case Con{a, s} Nil{} _:
116	      Equal.sym(List<&2, Bool>, zipk(k, SC.take(Bool, Con{a, s}, n), Nil{}), Nil{}, zipk_nil_r(k, SC.take(Bool, Con{a, s}, n)))
117	    case Con{a, s} Con{b, t} 0n:
118	      {==}
119	    case Con{a, s} Con{b, t} 1n+m:
120	      LL.cons_cong(Bool, bop(k, a, b), SC.take(Bool, zipk(k, s, t), m), zipk(k, SC.take(Bool, s, m), SC.take(Bool, t, m)), take_zipk(k, s, t, m))
121	
122	def drop_zipk(+k: B.WordOp, +xs: List<&2, Bool>, +ys: List<&2, Bool>, +n: Nat) -> {SC.drop(Bool, zipk(k, xs, ys), n) == zipk(k, SC.drop(Bool, xs, n), SC.drop(Bool, ys, n)) : List<&2, Bool>}:
123	  match xs ys n:
124	    case Nil{} _ _:
125	      {==}
126	    case Con{a, s} Nil{} _:
127	      Equal.sym(List<&2, Bool>, zipk(k, SC.drop(Bool, Con{a, s}, n), Nil{}), Nil{}, zipk_nil_r(k, SC.drop(Bool, Con{a, s}, n)))
128	    case Con{a, s} Con{b, t} 0n:
129	      {==}
130	    case Con{a, s} Con{b, t} 1n+m:
131	      drop_zipk(k, s, t, m)
132	
133	def bop_ff(+k: B.WordOp) -> {bop(k, False{}, False{}) == False{} : Bool}:
134	  match k:
135	    case B.KOr{}:
136	      {==}
137	    case B.KAnd{}:
138	      {==}
139	    case B.KDiff{}:
140	      {==}
141	    case B.KXor{}:
142	      {==}
143	
144	def allf_zipk(+k: B.WordOp, +xs: List<&2, Bool>, +ys: List<&2, Bool>, +hx: {allf(xs) == True{} : Bool}, +hy: {allf(ys) == True{} : Bool}) -> {allf(zipk(k, xs, ys)) == True{} : Bool}:
145	  match xs ys:
146	    case Nil{} _:
147	      {==}
148	    case Con{a, s} Nil{}:
149	      {==}
150	    case Con{True{}, s} Con{b, t}:
151	      Empty.absurd({allf(zipk(k, Con{True{}, s}, Con{b, t})) == True{} : Bool}, L.false_true(hx))
152	    case Con{False{}, s} Con{True{}, t}:
153	      Empty.absurd({allf(zipk(k, Con{False{}, s}, Con{True{}, t})) == True{} : Bool}, L.false_true(hy))
154	    case Con{False{}, s} Con{False{}, t}:
155	      %Equal.sym(Bool, bop(k, False{}, False{}), False{}, bop_ff(k)) : {allf(Con{_, zipk(k, s, t)}) == True{} : Bool}
156	      allf_zipk(k, s, t, hx, hy)
157	
158	def length_zipk_le(+k: B.WordOp, +xs: List<&2, Bool>, +ys: List<&2, Bool>) -> {Nat.is_le(SC.length(Bool, zipk(k, xs, ys)), SC.length(Bool, xs)) == True{} : Bool}:
159	  match xs ys:
160	    case Nil{} _:
161	      {==}
162	    case Con{a, s} Nil{}:
163	      {==}
164	    case Con{a, s} Con{b, t}:
165	      length_zipk_le(k, s, t)
166	
167	def le_length_zipk(+k: B.WordOp, +n: Nat, +xs: List<&2, Bool>, +ys: List<&2, Bool>, +hx: {Nat.is_le(n, SC.length(Bool, xs)) == True{} : Bool}, +hy: {Nat.is_le(n, SC.length(Bool, ys)) == True{} : Bool}) -> {Nat.is_le(n, SC.length(Bool, zipk(k, xs, ys))) == True{} : Bool}:
168	  match n xs ys:
169	    case 0n _ _:
170	      N.zero_le(SC.length(Bool, zipk(k, xs, ys)))
171	    case 1n+m Nil{} _:
172	      Empty.absurd({Nat.is_le(1n+m, SC.length(Bool, zipk(k, Nil{}, ys))) == True{} : Bool}, L.false_true(hx))
173	    case 1n+m Con{a, s} Nil{}:
174	      Empty.absurd({Nat.is_le(1n+m, SC.length(Bool, zipk(k, Con{a, s}, Nil{}))) == True{} : Bool}, L.false_true(hy))
175	    case 1n+m Con{a, s} Con{b, t}:
176	      le_length_zipk(k, m, s, t, hx, hy)
177	
178	# ---- all-False sequences ----
179	
180	def allf_append(+xs: List<&2, Bool>, +ys: List<&2, Bool>, +hx: {allf(xs) == True{} : Bool}, +hy: {allf(ys) == True{} : Bool}) -> {allf(SC.append(Bool, xs, ys)) == True{} : Bool}:
181	  match xs:
182	    case Nil{}:
183	      hy
184	    case Con{False{}, t}:
185	      allf_append(t, ys, hx, hy)
186	    case Con{True{}, t}:
187	      Empty.absurd({allf(SC.append(Bool, Con{True{}, t}, ys)) == True{} : Bool}, L.false_true(hx))
188	
189	def allf_rep(+n: Nat) -> {allf(rep(n)) == True{} : Bool}:
190	  match n:
191	    case 0n:
192	      {==}
193	    case 1n+m:
194	      allf_rep(m)
195	
196	def drop_allf(+xs: List<&2, Bool>, +n: Nat, +h: {allf(xs) == True{} : Bool}) -> {allf(SC.drop(Bool, xs, n)) == True{} : Bool}:
197	  match xs n:
198	    case Nil{} _:
199	      {==}
200	    case Con{a, t} 0n:
201	      h
202	    case Con{False{}, t} 1n+m:
203	      drop_allf(t, m, h)
204	    case Con{True{}, t} 1n+m:
205	      Empty.absurd({allf(SC.drop(Bool, Con{True{}, t}, 1n+m)) == True{} : Bool}, L.false_true(h))
206	
207	def take_allf(+xs: List<&2, Bool>, +n: Nat, +h: {allf(xs) == True{} : Bool}, +hn: {Nat.is_le(n, SC.length(Bool, xs)) == True{} : Bool}) -> {SC.take(Bool, xs, n) == rep(n) : List<&2, Bool>}:
208	  match xs n:
209	    case Nil{} 0n:
210	      {==}
211	    case Nil{} 1n+m:
212	      Empty.absurd({SC.take(Bool, Nil{}, 1n+m) == rep(1n+m) : List<&2, Bool>}, L.false_true(hn))
213	    case Con{a, t} 0n:
214	      {==}
215	    case Con{False{}, t} 1n+m:
216	      LL.cons_cong(Bool, False{}, SC.take(Bool, t, m), rep(m), take_allf(t, m, h, hn))
217	    case Con{True{}, t} 1n+m:
218	      Empty.absurd({SC.take(Bool, Con{True{}, t}, 1n+m) == rep(1n+m) : List<&2, Bool>}, L.false_true(h))
219	
220	def count_allf(+xs: List<&2, Bool>, +h: {allf(xs) == True{} : Bool}) -> {S.count(xs) == 0n : Nat}:
221	  match xs:
222	    case Nil{}:
223	      {==}
224	    case Con{False{}, t}:
225	      count_allf(t, h)
226	    case Con{True{}, t}:
227	      Empty.absurd({S.count(Con{True{}, t}) == 0n : Nat}, L.false_true(h))
228	
229	def members_allf(+xs: List<&2, Bool>, +off: Nat, +h: {allf(xs) == True{} : Bool}) -> {S.members(xs, off) == Nil{} : List<&2, Nat>}:
230	  match xs:
231	    case Nil{}:
232	      {==}
233	    case Con{False{}, t}:
234	      members_allf(t, 1n+off, h)
235	    case Con{True{}, t}:
236	      Empty.absurd({S.members(Con{True{}, t}, off) == Nil{} : List<&2, Nat>}, L.false_true(h))
237	
238	# ---- count / members over append, take ----
239	
240	def count_append(+xs: List<&2, Bool>, +ys: List<&2, Bool>) -> {S.count(SC.append(Bool, xs, ys)) == Nat.add(S.count(xs), S.count(ys)) : Nat}:
241	  match xs:
242	    case Nil{}:
243	      {==}
244	    case Con{False{}, t}:
245	      count_append(t, ys)
246	    case Con{True{}, t}:
247	      N.succ_cong(S.count(SC.append(Bool, t, ys)), Nat.add(S.count(t), S.count(ys)), count_append(t, ys))
248	
249	def members_append(+xs: List<&2, Bool>, +ys: List<&2, Bool>, +off: Nat) -> {S.members(SC.append(Bool, xs, ys), off) == SC.append(Nat, S.members(xs, off), S.members(ys, Nat.add(SC.length(Bool, xs), off))) : List<&2, Nat>}:
250	  match xs:
251	    case Nil{}:
252	      {==}
253	    case Con{False{}, t}:
254	      %N.add_succ(SC.length(Bool, t), off) : {S.members(SC.append(Bool, t, ys), 1n+off) == SC.append(Nat, S.members(t, 1n+off), S.members(ys, _)) : List<&2, Nat>}
255	      members_append(t, ys, 1n+off)
256	    case Con{True{}, t}:
257	      %N.add_succ(SC.length(Bool, t), off) : {Con{off, S.members(SC.append(Bool, t, ys), 1n+off)} == Con{off, SC.append(Nat, S.members(t, 1n+off), S.members(ys, _))} : List<&2, Nat>}
258	      LL.cons_cong(Nat, off, S.members(SC.append(Bool, t, ys), 1n+off), SC.append(Nat, S.members(t, 1n+off), S.members(ys, Nat.add(SC.length(Bool, t), 1n+off))), members_append(t, ys, 1n+off))
259	
260	def count_take_snoc(+xs: List<&2, Bool>, +m: Nat) -> {S.count(SC.take(Bool, SC.snoc(Bool, xs, False{}), m)) == S.count(SC.take(Bool, xs, m)) : Nat}:
261	  match xs m:
262	    case Nil{} 0n:
263	      {==}
264	    case Nil{} 1n+p:
265	      {==}
266	    case Con{a, t} 0n:
267	      {==}
268	    case Con{False{}, t} 1n+p:
269	      count_take_snoc(t, p)
270	    case Con{True{}, t} 1n+p:
271	      N.succ_cong(S.count(SC.take(Bool, SC.snoc(Bool, t, False{}), p)), S.count(SC.take(Bool, t, p)), count_take_snoc(t, p))
272	
273	def members_take_snoc(+xs: List<&2, Bool>, +m: Nat, +off: Nat) -> {S.members(SC.take(Bool, SC.snoc(Bool, xs, False{}), m), off) == S.members(SC.take(Bool, xs, m), off) : List<&2, Nat>}:
274	  match xs m:
275	    case Nil{} 0n:
276	      {==}
277	    case Nil{} 1n+p:
278	      {==}
279	    case Con{a, t} 0n:
280	      {==}
281	    case Con{False{}, t} 1n+p:
282	      members_take_snoc(t, p, 1n+off)
283	    case Con{True{}, t} 1n+p:
284	      LL.cons_cong(Nat, off, S.members(SC.take(Bool, SC.snoc(Bool, t, False{}), p), 1n+off), S.members(SC.take(Bool, t, p), 1n+off), members_take_snoc(t, p, 1n+off))
285	
286	# ---- take / drop / update ----
287	
288	def take_all(+xs: List<&2, Bool>) -> {SC.take(Bool, xs, SC.length(Bool, xs)) == xs : List<&2, Bool>}:
289	  match xs:
290	    case Nil{}:
291	      {==}
292	    case Con{a, t}:
293	      LL.cons_cong(Bool, a, SC.take(Bool, t, SC.length(Bool, t)), t, take_all(t))
294	
295	def take_drop(+xs: List<&2, Bool>, +n: Nat) -> {SC.append(Bool, SC.take(Bool, xs, n), SC.drop(Bool, xs, n)) == xs : List<&2, Bool>}:
296	  match xs n:
297	    case Nil{} _:
298	      {==}
299	    case Con{a, t} 0n:
300	      {==}
301	    case Con{a, t} 1n+m:
302	      LL.cons_cong(Bool, a, SC.append(Bool, SC.take(Bool, t, m), SC.drop(Bool, t, m)), t, take_drop(t, m))
303	
304	def length_take(+xs: List<&2, Bool>, +n: Nat, +h: {Nat.is_le(n, SC.length(Bool, xs)) == True{} : Bool}) -> {SC.length(Bool, SC.take(Bool, xs, n)) == n : Nat}:
305	  match xs n:
306	    case Nil{} 0n:
307	      {==}
308	    case Nil{} 1n+m:
309	      Empty.absurd({SC.length(Bool, SC.take(Bool, Nil{}, 1n+m)) == 1n+m : Nat}, L.false_true(h))
310	    case Con{a, t} 0n:
311	      {==}
312	    case Con{a, t} 1n+m:
313	      N.succ_cong(SC.length(Bool, SC.take(Bool, t, m)), m, length_take(t, m, h))
314	
315	def nth_take(+xs: List<&2, Bool>, +n: Nat, +i: Nat, +h: {Nat.is_lt(i, n) == True{} : Bool}) -> {SC.nth(Bool, SC.take(Bool, xs, n), i) == SC.nth(Bool, xs, i) : Maybe<&2, Bool>}:
316	  match xs n i:
317	    case Nil{} _ _:
318	      {==}
319	    case Con{a, t} 0n _:
320	      Empty.absurd({SC.nth(Bool, SC.take(Bool, Con{a, t}, 0n), i) == SC.nth(Bool, Con{a, t}, i) : Maybe<&2, Bool>}, N.lt_zero_absurd(i, h))
321	    case Con{a, t} 1n+m 0n:
322	      {==}
323	    case Con{a, t} 1n+m 1n+j:
324	      nth_take(t, m, j, h)
325	
326	def take_update(+xs: List<&2, Bool>, +i: Nat, +v: Bool, +n: Nat) -> {SC.take(Bool, SC.update(Bool, xs, i, v), n) == SC.update(Bool, SC.take(Bool, xs, n), i, v) : List<&2, Bool>}:
327	  match xs i n:
328	    case Nil{} _ _:
329	      {==}
330	    case Con{a, t} 0n 0n:
331	      {==}
332	    case Con{a, t} 1n+j 0n:
333	      {==}
334	    case Con{a, t} 0n 1n+m:
335	      {==}
336	    case Con{a, t} 1n+j 1n+m:
337	      LL.cons_cong(Bool, a, SC.take(Bool, SC.update(Bool, t, j, v), m), SC.update(Bool, SC.take(Bool, t, m), j, v), take_update(t, j, v, m))
338	
339	def drop_update(+xs: List<&2, Bool>, +i: Nat, +v: Bool, +n: Nat, +h: {Nat.is_lt(i, n) == True{} : Bool}) -> {SC.drop(Bool, SC.update(Bool, xs, i, v), n) == SC.drop(Bool, xs, n) : List<&2, Bool>}:
340	  match xs i n:
341	    case Nil{} _ _:
342	      {==}
343	    case Con{a, t} _ 0n:
344	      Empty.absurd({SC.drop(Bool, SC.update(Bool, Con{a, t}, i, v), 0n) == SC.drop(Bool, Con{a, t}, 0n) : List<&2, Bool>}, N.lt_zero_absurd(i, h))
345	    case Con{a, t} 0n 1n+m:
346	      {==}
347	    case Con{a, t} 1n+j 1n+m:
348	      drop_update(t, j, v, m, h)
349	
350	# ---- single-bit masks ----
351	
352	def take_rep_succ(+m: Nat) -> {SC.take(Bool, rep(1n+m), m) == rep(m) : List<&2, Bool>}:
353	  match m:
354	    case 0n:
355	      {==}
356	    case 1n+q:
357	      LL.cons_cong(Bool, False{}, SC.take(Bool, rep(1n+q), q), rep(q), take_rep_succ(q))
358	
359	# Shifting a one-hot mask up by one position.
360	def take_onehot(+m: Nat, +p: Nat, +h: {Nat.is_lt(p, m) == True{} : Bool}) -> {SC.take(Bool, SC.update(Bool, rep(1n+m), p, True{}), m) == SC.update(Bool, rep(m), p, True{}) : List<&2, Bool>}:
361	  match m p:
362	    case 0n _:
363	      Empty.absurd({SC.take(Bool, SC.update(Bool, rep(1n), p, True{}), 0n) == SC.update(Bool, rep(0n), p, True{}) : List<&2, Bool>}, N.lt_zero_absurd(p, h))
364	    case 1n+q 0n:
365	      LL.cons_cong(Bool, True{}, SC.take(Bool, rep(1n+q), q), rep(q), take_rep_succ(q))
366	    case 1n+q 1n+j:
367	      LL.cons_cong(Bool, False{}, SC.take(Bool, SC.update(Bool, rep(1n+q), j, True{}), q), SC.update(Bool, rep(q), j, True{}), take_onehot(q, j, h))
368	
369	def or_rep(+xs: List<&2, Bool>) -> {zipk(B.KOr{}, xs, rep(SC.length(Bool, xs))) == xs : List<&2, Bool>}:
370	  match xs:
371	    case Nil{}:
372	      {==}
373	    case Con{True{}, t}:
374	      LL.cons_cong(Bool, True{}, zipk(B.KOr{}, t, rep(SC.length(Bool, t))), t, or_rep(t))
375	    case Con{False{}, t}:
376	      LL.cons_cong(Bool, False{}, zipk(B.KOr{}, t, rep(SC.length(Bool, t))), t, or_rep(t))
377	
378	def diff_rep(+xs: List<&2, Bool>) -> {zipk(B.KDiff{}, xs, rep(SC.length(Bool, xs))) == xs : List<&2, Bool>}:
379	  match xs:
380	    case Nil{}:
381	      {==}
382	    case Con{True{}, t}:
383	      LL.cons_cong(Bool, True{}, zipk(B.KDiff{}, t, rep(SC.length(Bool, t))), t, diff_rep(t))
384	    case Con{False{}, t}:
385	      LL.cons_cong(Bool, False{}, zipk(B.KDiff{}, t, rep(SC.length(Bool, t))), t, diff_rep(t))
386	
387	# OR with the one-hot mask for k sets bit k.
388	def or_onehot(+xs: List<&2, Bool>, +k: Nat) -> {zipk(B.KOr{}, xs, SC.update(Bool, rep(SC.length(Bool, xs)), k, True{})) == SC.update(Bool, xs, k, True{}) : List<&2, Bool>}:
389	  match xs k:
390	    case Nil{} _:
391	      {==}
392	    case Con{True{}, t} 0n:
393	      LL.cons_cong(Bool, True{}, zipk(B.KOr{}, t, rep(SC.length(Bool, t))), t, or_rep(t))
394	    case Con{False{}, t} 0n:
395	      LL.cons_cong(Bool, True{}, zipk(B.KOr{}, t, rep(SC.length(Bool, t))), t, or_rep(t))
396	    case Con{True{}, t} 1n+j:
397	      LL.cons_cong(Bool, True{}, zipk(B.KOr{}, t, SC.update(Bool, rep(SC.length(Bool, t)), j, True{})), SC.update(Bool, t, j, True{}), or_onehot(t, j))
398	    case Con{False{}, t} 1n+j:
399	      LL.cons_cong(Bool, False{}, zipk(B.KOr{}, t, SC.update(Bool, rep(SC.length(Bool, t)), j, True{})), SC.update(Bool, t, j, True{}), or_onehot(t, j))
400	
401	# AND NOT with the one-hot mask for k clears bit k.
402	def diff_onehot(+xs: List<&2, Bool>, +k: Nat) -> {zipk(B.KDiff{}, xs, SC.update(Bool, rep(SC.length(Bool, xs)), k, True{})) == SC.update(Bool, xs, k, False{}) : List<&2, Bool>}:
403	  match xs k:
404	    case Nil{} _:
405	      {==}
406	    case Con{True{}, t} 0n:
407	      LL.cons_cong(Bool, False{}, zipk(B.KDiff{}, t, rep(SC.length(Bool, t))), t, diff_rep(t))
408	    case Con{False{}, t} 0n:
409	      LL.cons_cong(Bool, False{}, zipk(B.KDiff{}, t, rep(SC.length(Bool, t))), t, diff_rep(t))
410	    case Con{True{}, t} 1n+j:
411	      LL.cons_cong(Bool, True{}, zipk(B.KDiff{}, t, SC.update(Bool, rep(SC.length(Bool, t)), j, True{})), SC.update(Bool, t, j, False{}), diff_onehot(t, j))
412	    case Con{False{}, t} 1n+j:
413	      LL.cons_cong(Bool, False{}, zipk(B.KDiff{}, t, SC.update(Bool, rep(SC.length(Bool, t)), j, True{})), SC.update(Bool, t, j, False{}), diff_onehot(t, j))