proofs/lib/u32.bend

bend-collections-laws-crypto@1.0.0.0 · 304 lines · 43 definitions

1import Base
2import bend-collections-laws-crypto@1.0.0.0/proofs/lib/logic.bend as L
3import bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend as N
4import bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend as SC
5import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/spec/numeric.bend as S
6import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/numeric.bend as RN
7import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend as NA
8import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/modular_addition.bend as MA
9import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/word_value.bend as WV
10import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/word_shift.bend as WS
11import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/word_comparison.bend as WC
12import bend-collections-laws-crypto@1.0.0.0/proofs/lib/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
18def to_nat_word(+w: Word(32n)) -> {U32.to_nat(U32{w}) == S.unsigned(32n, w) : Nat}:
19  RN.primitive_word_interpretation(32n, w)
20
21def 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
28def 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
32def 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).
41def 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
45def 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
58def 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
62def 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.
67def 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
70def 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)
75def 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)
81def 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
85def 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
93def 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
97def 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
100def 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
103def 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
114def 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
118def 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
125def 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
136def low_bit(x: U32) -> Bool:
137  match x:
138    case U32{w}:
139      match w:
140        case WCon{b, t}:
141          b
142
143def 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).
154def pow2u(d: Nat) -> U32:
155  match d:
156    case 0n:
157      1
158    case 1n+p:
159      U32.shl(pow2u(p))
160
161def 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
165def 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
175def 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
186def and_true(+b: Bool) -> {Bool.and(b, True{}) == b : Bool}:
187  match b:
188    case False{}:
189      {==}
190    case True{}:
191      {==}
192
193def 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
200def and_low_prev(d: Nat) -> Nat:
201  match d:
202    case 0n:
203      0n
204    case 1n+k:
205      k
206
207def 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
214def 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
221def 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
229def 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
232def 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
245def 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
256def 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
260def 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.
269def 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
273def 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
280def 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
283def 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
294def 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
301def 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)