1	import Base
2	import ./logic.bend as L
3	import ./nat.bend as N
4	import ../../spec/lib/common.bend as SC
5	import ./lemmas/spec/numeric.bend as S
6	import ./lemmas/proofs/numeric.bend as RN
7	import ./lemmas/proofs/nat_algebra.bend as NA
8	import ./lemmas/proofs/modular_addition.bend as MA
9	import ./lemmas/proofs/word_value.bend as WV
10	import ./lemmas/proofs/word_shift.bend as WS
11	import ./lemmas/proofs/word_comparison.bend as WC
12	import ./lemmas/proofs/subtraction_bounds.bend as SB
13	
14	# U32 facts needed by the new structures, derived from the retained LRU word
15	# interpretation lemmas (reused, not re-derived): unsigned interpretation,
16	# increment/shift/subtraction/comparison refinement and reconstruction.
17	
18	def to_nat_word(+w: Word(32n)) -> {U32.to_nat(U32{w}) == S.unsigned(32n, w) : Nat}:
19	  RN.primitive_word_interpretation(32n, w)
20	
21	def pow2_scale(+k: Nat) -> {SC.pow2(k) == S.scale_binary(k, 1n) : Nat}:
22	  match k:
23	    case 0n:
24	      {==}
25	    case 1n+p:
26	      Equal.cong(Nat, Nat, Nat.double, SC.pow2(p), S.scale_binary(p, 1n), pow2_scale(p))
27	
28	def double_pow(+x: Nat) -> {Nat.double(x) == Nat.add(x, Nat.add(x, 0n)) : Nat}:
29	  %Equal.sym(Nat, Nat.add(x, 0n), x, N.add_zero(x)) : {Nat.double(x) == Nat.add(x, _) : Nat}
30	  NA.double_self(x)
31	
32	def pow2_pow(+k: Nat) -> {SC.pow2(k) == Nat.pow(2n, k) : Nat}:
33	  match k:
34	    case 0n:
35	      {==}
36	    case 1n+p:
37	      %pow2_pow(p) : {Nat.double(SC.pow2(p)) == Nat.add(_, Nat.add(_, 0n)) : Nat}
38	      double_pow(SC.pow2(p))
39	
40	# Every word is recovered from its unsigned interpretation (reconstruct at 0).
41	def word_from_unsigned(+w: Word(32n)) -> {S.from_nat(32n, S.unsigned(32n, w)) == w : Word(32n)}:
42	  %N.add_zero(S.unsigned(32n, w)) : {S.from_nat(32n, _) == w : Word(32n)}
43	  MA.reconstruct(32n, w, 0n)
44	
45	def injective(+a: U32, +b: U32, +e: {U32.to_nat(a) == U32.to_nat(b) : Nat}) -> {a == b : U32}:
46	  match a b:
47	    case U32{+x} U32{+y}:
48	      Equal.cong(Word(32n), U32, w => U32{w}, x, y,
49	        Equal.trans(Word(32n), x, S.from_nat(32n, S.unsigned(32n, x)), y,
50	          Equal.sym(Word(32n), S.from_nat(32n, S.unsigned(32n, x)), x, word_from_unsigned(x)),
51	          Equal.trans(Word(32n), S.from_nat(32n, S.unsigned(32n, x)), S.from_nat(32n, S.unsigned(32n, y)), y,
52	            Equal.cong(Nat, Word(32n), v => S.from_nat(32n, v), S.unsigned(32n, x), S.unsigned(32n, y),
53	              Equal.trans(Nat, S.unsigned(32n, x), U32.to_nat(U32{x}), S.unsigned(32n, y),
54	                Equal.sym(Nat, U32.to_nat(U32{x}), S.unsigned(32n, x), to_nat_word(x)),
55	                Equal.trans(Nat, U32.to_nat(U32{x}), U32.to_nat(U32{y}), S.unsigned(32n, y), e, to_nat_word(y)))),
56	            word_from_unsigned(y))))
57	
58	def pow2_le_pow(+n: Nat, +k: Nat, +hk: {Nat.is_le(k, n) == True{} : Bool}) -> {Nat.is_le(SC.pow2(k), Nat.pow(2n, n)) == True{} : Bool}:
59	  %pow2_pow(n) : {Nat.is_le(SC.pow2(k), _) == True{} : Bool}
60	  N.pow2_mono(k, n, hk)
61	
62	def pow2_le_scale(+n: Nat, +k: Nat, +hk: {Nat.is_le(k, n) == True{} : Bool}) -> {Nat.is_le(SC.pow2(k), S.scale_binary(n, 1n)) == True{} : Bool}:
63	  %pow2_scale(n) : {Nat.is_le(SC.pow2(k), _) == True{} : Bool}
64	  N.pow2_mono(k, n, hk)
65	
66	# Width-generic wrappers: bounds are 2^k with k <= n, never a closed 2^32.
67	def from_nat_value_k(+n: Nat, +k: Nat, +v: Nat, +hk: {Nat.is_le(k, n) == True{} : Bool}, +hv: {Nat.is_lt(v, SC.pow2(k)) == True{} : Bool}) -> {S.unsigned(n, S.from_nat(n, v)) == v : Nat}:
68	  WV.from_nat_value(n, v, N.lt_le_trans(v, SC.pow2(k), Nat.pow(2n, n), hv, pow2_le_pow(n, k, hk)))
69	
70	def shl_exact_k(+n: Nat, +k: Nat, +w: Word(n), +hk: {Nat.is_le(k, n) == True{} : Bool}, +h: {Nat.is_lt(Nat.double(S.unsigned(n, w)), SC.pow2(k)) == True{} : Bool}) -> {S.unsigned(n, Word.shl(n, w)) == Nat.double(S.unsigned(n, w)) : Nat}:
71	  WS.exact(n, w, N.lt_le_trans(Nat.double(S.unsigned(n, w)), SC.pow2(k), S.scale_binary(n, 1n), h, pow2_le_scale(n, k, hk)))
72	
73	# one increment over an abstract width (the checker never expands a
74	# literal-width word here)
75	def inc_from(+n: Nat, +p: Nat, +hv: {S.unsigned(n, S.from_nat(n, p)) == p : Nat}) -> {Word.inc(n, S.from_nat(n, p)) == S.from_nat(n, 1n+p) : Word(n)}:
76	  Equal.trans(Word(n), Word.inc(n, S.from_nat(n, p)), S.from_nat(n, 1n+S.unsigned(n, S.from_nat(n, p))), S.from_nat(n, 1n+p),
77	    MA.increment_refines(n, S.from_nat(n, p)),
78	    Equal.cong(Nat, Word(n), v => S.from_nat(n, 1n+v), S.unsigned(n, S.from_nat(n, p)), p, hv))
79	
80	# the U32 step over abstract words a (for p) and b (for p + 1)
81	def from_nat_step(+p: Nat, +a: Word(32n), +b: Word(32n), +rec: {U32.from_nat(p) == U32{a} : U32}, +hinc: {Word.inc(32n, a) == b : Word(32n)}) -> {U32.from_nat(1n+p) == U32{b} : U32}:
82	  %Equal.sym(U32, U32.from_nat(p), U32{a}, rec) : {U32.inc(_) == U32{b} : U32}
83	  Equal.cong(Word(32n), U32, w => U32{w}, Word.inc(32n, a), b, hinc)
84	
85	def from_nat_word(+i: Nat, +k: Nat, +hk: {Nat.is_le(k, 32n) == True{} : Bool}, +h: {Nat.is_lt(i, SC.pow2(k)) == True{} : Bool}) -> {U32.from_nat(i) == U32{S.from_nat(32n, i)} : U32}:
86	  match i:
87	    case 0n:
88	      {==}
89	    case 1n+p:
90	      +hp = N.lt_trans(p, 1n+p, SC.pow2(k), N.lt_succ(p), h)
91	      from_nat_step(p, S.from_nat(32n, p), S.from_nat(32n, 1n+p), from_nat_word(p, k, hk, hp), inc_from(32n, p, from_nat_value_k(32n, k, p, hk, hp)))
92	
93	def to_nat_from_nat(+i: Nat, +k: Nat, +hk: {Nat.is_le(k, 32n) == True{} : Bool}, +h: {Nat.is_lt(i, SC.pow2(k)) == True{} : Bool}) -> {U32.to_nat(U32.from_nat(i)) == i : Nat}:
94	  %Equal.sym(U32, U32.from_nat(i), U32{S.from_nat(32n, i)}, from_nat_word(i, k, hk, h)) : {U32.to_nat(_) == i : Nat}
95	  Equal.trans(Nat, U32.to_nat(U32{S.from_nat(32n, i)}), S.unsigned(32n, S.from_nat(32n, i)), i, to_nat_word(S.from_nat(32n, i)), from_nat_value_k(32n, k, i, hk, h))
96	
97	def is_lt_nat(+a: U32, +b: U32) -> {U32.is_lt(a, b) == Nat.is_lt(U32.to_nat(a), U32.to_nat(b)) : Bool}:
98	  WC.u32_lt(a, b)
99	
100	def sub_nat(+a: U32, +b: U32, +e: {Nat.is_le(U32.to_nat(b), U32.to_nat(a)) == True{} : Bool}) -> {U32.to_nat(U32.sub(a, b)) == Nat.sub(U32.to_nat(a), U32.to_nat(b)) : Nat}:
101	  SB.u32_exact(a, b, e)
102	
103	def WB_unsigned(+n: Nat, +w: Word(n)) -> {Nat.is_lt(S.unsigned(n, w), S.scale_binary(n, 1n)) == True{} : Bool}:
104	  match n:
105	    case 0n:
106	      {==}
107	    case 1n+p:
108	      match w:
109	        case WCon{b, t}:
110	          N.double_lt_bit(b, S.unsigned(p, t), S.scale_binary(p, 1n), WB_unsigned(p, t))
111	
112	# ---- doubling (shl) and halving (shr) ----
113	
114	def shl_bound(+w: Word(32n), +k: Nat, +h: {Nat.is_lt(Nat.double(U32.to_nat(U32{w})), SC.pow2(k)) == True{} : Bool}) -> {Nat.is_lt(Nat.double(S.unsigned(32n, w)), SC.pow2(k)) == True{} : Bool}:
115	  %to_nat_word(w) : {Nat.is_lt(Nat.double(_), SC.pow2(k)) == True{} : Bool}
116	  h
117	
118	def shl_value(+x: U32, +k: Nat, +hk: {Nat.is_le(k, 32n) == True{} : Bool}, +h: {Nat.is_lt(Nat.double(U32.to_nat(x)), SC.pow2(k)) == True{} : Bool}) -> {U32.to_nat(U32.shl(x)) == Nat.double(U32.to_nat(x)) : Nat}:
119	  match x:
120	    case U32{+w}:
121	      %Equal.sym(Nat, U32.to_nat(U32{w}), S.unsigned(32n, w), to_nat_word(w)) : {U32.to_nat(U32{Word.shl(32n, w)}) == Nat.double(_) : Nat}
122	      Equal.trans(Nat, U32.to_nat(U32{Word.shl(32n, w)}), S.unsigned(32n, Word.shl(32n, w)), Nat.double(S.unsigned(32n, w)), to_nat_word(Word.shl(32n, w)),
123	        shl_exact_k(32n, k, w, hk, shl_bound(w, k, h)))
124	
125	def pad_value(+n: Nat, +w: Word(n)) -> {S.unsigned(1n+n, Word.shr.pad(n, w)) == S.unsigned(n, w) : Nat}:
126	  match n:
127	    case 0n:
128	      match w:
129	        case WNil{}:
130	          {==}
131	    case 1n+p:
132	      match w:
133	        case WCon{b, t}:
134	          Equal.cong(Nat, Nat, v => Nat.add(S.bit_value(b), Nat.double(v)), S.unsigned(1n+p, Word.shr.pad(p, t)), S.unsigned(p, t), pad_value(p, t))
135	
136	def low_bit(x: U32) -> Bool:
137	  match x:
138	    case U32{w}:
139	      match w:
140	        case WCon{b, t}:
141	          b
142	
143	def shr_split(+x: U32) -> {U32.to_nat(x) == Nat.add(S.bit_value(low_bit(x)), Nat.double(U32.to_nat(U32.shr(x)))) : Nat}:
144	  match x:
145	    case U32{w}:
146	      match w:
147	        case WCon{+b, +t}:
148	          %Equal.sym(Nat, U32.to_nat(U32{WCon{b, t}}), S.unsigned(32n, WCon{b, t}), to_nat_word(WCon{b, t})) : {_ == Nat.add(S.bit_value(b), Nat.double(U32.to_nat(U32{Word.shr.pad(31n, t)}))) : Nat}
149	          %Equal.sym(Nat, U32.to_nat(U32{Word.shr.pad(31n, t)}), S.unsigned(32n, Word.shr.pad(31n, t)), to_nat_word(Word.shr.pad(31n, t))) : {S.unsigned(32n, WCon{b, t}) == Nat.add(S.bit_value(b), Nat.double(_)) : Nat}
150	          %Equal.sym(Nat, S.unsigned(32n, Word.shr.pad(31n, t)), S.unsigned(31n, t), pad_value(31n, t)) : {S.unsigned(32n, WCon{b, t}) == Nat.add(S.bit_value(b), Nat.double(_)) : Nat}
151	          {==}
152	
153	# 2^d as the U32 built by Base Array.size (1, then shl per level).
154	def pow2u(d: Nat) -> U32:
155	  match d:
156	    case 0n:
157	      1
158	    case 1n+p:
159	      U32.shl(pow2u(p))
160	
161	def pow2u_shl_bound(+p: Nat, +ih: {U32.to_nat(pow2u(p)) == SC.pow2(p) : Nat}) -> {Nat.is_lt(Nat.double(U32.to_nat(pow2u(p))), SC.pow2(2n+p)) == True{} : Bool}:
162	  %Equal.sym(Nat, U32.to_nat(pow2u(p)), SC.pow2(p), ih) : {Nat.is_lt(Nat.double(_), SC.pow2(2n+p)) == True{} : Bool}
163	  N.pow2_lt_succ(1n+p)
164	
165	def pow2u_value(+d: Nat, +h: {Nat.is_lt(d, 32n) == True{} : Bool}) -> {U32.to_nat(pow2u(d)) == SC.pow2(d) : Nat}:
166	  match d:
167	    case 0n:
168	      {==}
169	    case 1n+p:
170	      +ih = pow2u_value(p, N.lt_trans(p, 1n+p, 32n, N.lt_succ(p), h))
171	      Equal.trans(Nat, U32.to_nat(U32.shl(pow2u(p))), Nat.double(U32.to_nat(pow2u(p))), Nat.double(SC.pow2(p)),
172	        shl_value(pow2u(p), 2n+p, N.lt_succ_le_succ(1n+p, 32n, h), pow2u_shl_bound(p, ih)),
173	        Equal.cong(Nat, Nat, Nat.double, U32.to_nat(pow2u(p)), SC.pow2(p), ih))
174	
175	def shr_pow2u(+p: Nat, +h: {Nat.is_lt(1n+p, 32n) == True{} : Bool}) -> {U32.shr(pow2u(1n+p)) == pow2u(p) : U32}:
176	  injective(U32.shr(pow2u(1n+p)), pow2u(p),
177	    Equal.trans(Nat, U32.to_nat(U32.shr(pow2u(1n+p))), SC.pow2(p), U32.to_nat(pow2u(p)),
178	      N.bit_split_val(low_bit(pow2u(1n+p)), False{}, U32.to_nat(U32.shr(pow2u(1n+p))), SC.pow2(p),
179	        Equal.trans(Nat, Nat.add(S.bit_value(low_bit(pow2u(1n+p))), Nat.double(U32.to_nat(U32.shr(pow2u(1n+p))))), U32.to_nat(pow2u(1n+p)), Nat.double(SC.pow2(p)),
180	          Equal.sym(Nat, U32.to_nat(pow2u(1n+p)), Nat.add(S.bit_value(low_bit(pow2u(1n+p))), Nat.double(U32.to_nat(U32.shr(pow2u(1n+p))))), shr_split(pow2u(1n+p))),
181	          pow2u_value(1n+p, h))),
182	      Equal.sym(Nat, U32.to_nat(pow2u(p)), SC.pow2(p), pow2u_value(p, N.lt_trans(p, 1n+p, 32n, N.lt_succ(p), h)))))
183	
184	# ---- low-bit masks ----
185	
186	def and_true(+b: Bool) -> {Bool.and(b, True{}) == b : Bool}:
187	  match b:
188	    case False{}:
189	      {==}
190	    case True{}:
191	      {==}
192	
193	def lt_one_zero(+v: Nat, +e: {Nat.is_lt(v, 1n) == True{} : Bool}) -> {v == 0n : Nat}:
194	  match v:
195	    case 0n:
196	      {==}
197	    case 1n+p:
198	      Empty.absurd({1n+p == 0n : Nat}, N.lt_zero_absurd(p, e))
199	
200	def and_low_prev(d: Nat) -> Nat:
201	  match d:
202	    case 0n:
203	      0n
204	    case 1n+k:
205	      k
206	
207	def and_low_hy(+m: Nat, +d: Nat, +yb: Bool, +yt: Word(m), +hy: {Nat.add(S.bit_value(yb), Nat.double(S.unsigned(m, yt))) == Nat.sub(SC.pow2(d), 1n) : Nat}) -> {S.unsigned(m, yt) == Nat.sub(SC.pow2(and_low_prev(d)), 1n) : Nat}:
208	  match d:
209	    case 0n:
210	      N.bit_split_val(yb, False{}, S.unsigned(m, yt), 0n, hy)
211	    case 1n+k:
212	      N.bit_split_val(yb, True{}, S.unsigned(m, yt), Nat.sub(SC.pow2(k), 1n), Equal.trans(Nat, Nat.add(S.bit_value(yb), Nat.double(S.unsigned(m, yt))), Nat.sub(Nat.double(SC.pow2(k)), 1n), 1n+Nat.double(Nat.sub(SC.pow2(k), 1n)), hy, N.pred_double(SC.pow2(k), N.pow2_pos(k))))
213	
214	def and_low_hyb(+m: Nat, +d: Nat, +yb: Bool, +yt: Word(m), +hy: {Nat.add(S.bit_value(yb), Nat.double(S.unsigned(m, yt))) == Nat.sub(SC.pow2(d), 1n) : Nat}) -> {yb == Bool.not(N.is_zero(d)) : Bool}:
215	  match d:
216	    case 0n:
217	      N.bit_split_bit(yb, False{}, S.unsigned(m, yt), 0n, hy)
218	    case 1n+k:
219	      N.bit_split_bit(yb, True{}, S.unsigned(m, yt), Nat.sub(SC.pow2(k), 1n), Equal.trans(Nat, Nat.add(S.bit_value(yb), Nat.double(S.unsigned(m, yt))), Nat.sub(Nat.double(SC.pow2(k)), 1n), 1n+Nat.double(Nat.sub(SC.pow2(k), 1n)), hy, N.pred_double(SC.pow2(k), N.pow2_pos(k))))
220	
221	def and_low_hx(+m: Nat, +d: Nat, +xb: Bool, +xt: Word(m), +hx: {Nat.is_lt(Nat.add(S.bit_value(xb), Nat.double(S.unsigned(m, xt))), SC.pow2(d)) == True{} : Bool}) -> {Nat.is_lt(S.unsigned(m, xt), SC.pow2(and_low_prev(d))) == True{} : Bool}:
222	  match d:
223	    case 0n:
224	      %Equal.sym(Nat, S.unsigned(m, xt), 0n, N.bit_split_val(xb, False{}, S.unsigned(m, xt), 0n, lt_one_zero(Nat.add(S.bit_value(xb), Nat.double(S.unsigned(m, xt))), hx))) : {Nat.is_lt(_, 1n) == True{} : Bool}
225	      {==}
226	    case 1n+k:
227	      N.bit_double_lt(xb, S.unsigned(m, xt), SC.pow2(k), hx)
228	
229	def and_low_hxb(+m: Nat, +xb: Bool, +xt: Word(m), +hx: {Nat.is_lt(Nat.add(S.bit_value(xb), Nat.double(S.unsigned(m, xt))), 1n) == True{} : Bool}) -> {xb == False{} : Bool}:
230	  N.bit_split_bit(xb, False{}, S.unsigned(m, xt), 0n, lt_one_zero(Nat.add(S.bit_value(xb), Nat.double(S.unsigned(m, xt))), hx))
231	
232	def and_low_step(+m: Nat, +d: Nat, +xb: Bool, +xt: Word(m), +yb: Bool, +yt: Word(m), +hy: {Nat.add(S.bit_value(yb), Nat.double(S.unsigned(m, yt))) == Nat.sub(SC.pow2(d), 1n) : Nat}, +hx: {Nat.is_lt(Nat.add(S.bit_value(xb), Nat.double(S.unsigned(m, xt))), SC.pow2(d)) == True{} : Bool}, +ih: {Word.and(m, xt, yt) == xt : Word(m)}) -> {WCon{Bool.and(xb, yb), Word.and(m, xt, yt)} == WCon{xb, xt} : Word(1n+m)}:
233	  match d:
234	    case 0n:
235	      %Equal.sym(Word(m), Word.and(m, xt, yt), xt, ih) : {WCon{Bool.and(xb, yb), _} == WCon{xb, xt} : Word(1n+m)}
236	      %Equal.sym(Bool, yb, False{}, and_low_hyb(m, 0n, yb, yt, hy)) : {WCon{Bool.and(xb, _), xt} == WCon{xb, xt} : Word(1n+m)}
237	      %Equal.sym(Bool, xb, False{}, and_low_hxb(m, xb, xt, hx)) : {WCon{Bool.and(_, False{}), xt} == WCon{_, xt} : Word(1n+m)}
238	      {==}
239	    case 1n+k:
240	      %Equal.sym(Word(m), Word.and(m, xt, yt), xt, ih) : {WCon{Bool.and(xb, yb), _} == WCon{xb, xt} : Word(1n+m)}
241	      %Equal.sym(Bool, yb, True{}, and_low_hyb(m, 1n+k, yb, yt, hy)) : {WCon{Bool.and(xb, _), xt} == WCon{xb, xt} : Word(1n+m)}
242	      %Equal.sym(Bool, Bool.and(xb, True{}), xb, and_true(xb)) : {WCon{_, xt} == WCon{xb, xt} : Word(1n+m)}
243	      {==}
244	
245	def and_low(+n: Nat, +d: Nat, +x: Word(n), +y: Word(n), +hy: {S.unsigned(n, y) == Nat.sub(SC.pow2(d), 1n) : Nat}, +hx: {Nat.is_lt(S.unsigned(n, x), SC.pow2(d)) == True{} : Bool}) -> {Word.and(n, x, y) == x : Word(n)}:
246	  match n:
247	    case 0n:
248	      match x y:
249	        case WNil{} WNil{}:
250	          {==}
251	    case 1n+m:
252	      match x y:
253	        case WCon{+xb, +xt} WCon{+yb, +yt}:
254	          and_low_step(m, d, xb, xt, yb, yt, hy, hx, and_low(m, and_low_prev(d), xt, yt, and_low_hy(m, d, yb, yt, hy), and_low_hx(m, d, xb, xt, hx)))
255	
256	def mask_hx(+wx: Word(32n), +d: Nat, +hx: {Nat.is_lt(U32.to_nat(U32{wx}), SC.pow2(d)) == True{} : Bool}) -> {Nat.is_lt(S.unsigned(32n, wx), SC.pow2(d)) == True{} : Bool}:
257	  %to_nat_word(wx) : {Nat.is_lt(_, SC.pow2(d)) == True{} : Bool}
258	  hx
259	
260	def mask_word(+x: U32, +y: U32, +d: Nat, +hy: {U32.to_nat(y) == Nat.sub(SC.pow2(d), 1n) : Nat}, +hx: {Nat.is_lt(U32.to_nat(x), SC.pow2(d)) == True{} : Bool}) -> {U32.and(x, y) == x : U32}:
261	  match x y:
262	    case U32{+wx} U32{+wy}:
263	      Equal.cong(Word(32n), U32, w => U32{w}, Word.and(32n, wx, wy), wx,
264	        and_low(32n, d, wx, wy,
265	          Equal.trans(Nat, S.unsigned(32n, wy), U32.to_nat(U32{wy}), Nat.sub(SC.pow2(d), 1n), Equal.sym(Nat, U32.to_nat(U32{wy}), S.unsigned(32n, wy), to_nat_word(wy)), hy),
266	          mask_hx(wx, d, hx)))
267	
268	# Base Array masks every index with size - 1; below the size this is the identity.
269	def one_le_pow2u(+d: Nat, +hd: {Nat.is_lt(d, 32n) == True{} : Bool}) -> {Nat.is_le(U32.to_nat(1), U32.to_nat(pow2u(d))) == True{} : Bool}:
270	  %Equal.sym(Nat, U32.to_nat(pow2u(d)), SC.pow2(d), pow2u_value(d, hd)) : {Nat.is_le(1n, _) == True{} : Bool}
271	  N.pow2_pos(d)
272	
273	def mask_pow2u(+x: U32, +d: Nat, +hd: {Nat.is_lt(d, 32n) == True{} : Bool}, +hx: {Nat.is_lt(U32.to_nat(x), SC.pow2(d)) == True{} : Bool}) -> {U32.and(x, U32.sub(pow2u(d), 1)) == x : U32}:
274	  mask_word(x, U32.sub(pow2u(d), 1), d,
275	    Equal.trans(Nat, U32.to_nat(U32.sub(pow2u(d), 1)), Nat.sub(U32.to_nat(pow2u(d)), 1n), Nat.sub(SC.pow2(d), 1n),
276	      sub_nat(pow2u(d), 1, one_le_pow2u(d, hd)),
277	      Equal.cong(Nat, Nat, v => Nat.sub(v, 1n), U32.to_nat(pow2u(d)), SC.pow2(d), pow2u_value(d, hd))),
278	    hx)
279	
280	def u32_cmp(+a: U32, +b: U32) -> {U32.cmp(a, b) == Nat.cmp(U32.to_nat(a), U32.to_nat(b)) : Cmp}:
281	  WC.u32_refines(a, b)
282	
283	def fin_refl(+c: Cmp, +b: Bool, +h: {Cmp.is_eq(c) == True{} : Bool}) -> {Cmp.is_eq(Word.cmp.fin(b, b, c)) == True{} : Bool}:
284	  match c b:
285	    case LT{} _:
286	      Empty.absurd({Cmp.is_eq(Word.cmp.fin(b, b, LT{})) == True{} : Bool}, L.false_true(h))
287	    case EQ{} True{}:
288	      {==}
289	    case EQ{} False{}:
290	      {==}
291	    case GT{} _:
292	      Empty.absurd({Cmp.is_eq(Word.cmp.fin(b, b, GT{})) == True{} : Bool}, L.false_true(h))
293	
294	def cmp_refl_eq(+n: Nat, +w: Word(n)) -> {Cmp.is_eq(Word.cmp(n, w, w)) == True{} : Bool}:
295	  match n w:
296	    case 0n WNil{}:
297	      {==}
298	    case 1n+p WCon{b, t}:
299	      fin_refl(Word.cmp(p, t, t), b, cmp_refl_eq(p, t))
300	
301	def u32_eq_refl(+x: U32) -> {U32.is_eq(x, x) == True{} : Bool}:
302	  match x:
303	    case U32{w}:
304	      cmp_refl_eq(32n, w)