proofs/math/typed/u32laws.bend
bend-collections-laws-math@1.0.0.0 · 361 lines · 45 definitions
1import Base
2import bend-collections-laws-math@1.0.0.0/spec/lib/common.bend as C
3import bend-collections-laws-math@1.0.0.0/spec/math/instances.bend as SI
4import bend-collections-laws-math@1.0.0.0/spec/math/generic.bend as SG
5import bend-collections-laws-math@1.0.0.0/src/math/instances.bend as I
6import bend-collections-laws-math@1.0.0.0/src/math/num.bend as NM
7import bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend as N
8import bend-collections-laws-math@1.0.0.0/proofs/lib/u32.bend as U
9import bend-collections-laws-math@1.0.0.0/proofs/lib/u32div.bend as UD
10import bend-collections-laws-math@1.0.0.0/proofs/lib/u32half.bend as UH
11import bend-collections-laws-math@1.0.0.0/proofs/lib/u32alg.bend as A
12import bend-collections-laws-math@1.0.0.0/proofs/lib/word.bend as WD
13import bend-collections-laws-math@1.0.0.0/proofs/lib/logic.bend as L
14import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/spec/numeric.bend as S
15import bend-collections-laws-math@1.0.0.0/proofs/math/u64/u64.bend as P64
16import bend-collections-laws-math@1.0.0.0/proofs/math/typed/u32.bend as U32P
17import bend-collections-laws-math@1.0.0.0/proofs/math/typed/width.bend as WW
18import bend-collections-laws-math@1.0.0.0/proofs/math/u64/u64div.bend as PD
19import bend-collections-laws-math@1.0.0.0/proofs/math/natural/arith.bend as NA
20import bend-collections-laws-math@1.0.0.0/proofs/lib/arith.bend as AR
21import bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64mul.bend as W64M
22import bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64div.bend as W64D
23import bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64sqrt.bend as W64S
24import bend-collections-laws-math@1.0.0.0/src/math/w64.bend as X
25import bend-collections-laws-math@1.0.0.0/spec/math/w64.bend as SW
26
27
28
29
30
31
32
33def v(+x: U32) -> Nat:
34 U32.to_nat(x)
35
36
37
38def vb_k(+k: Nat, +hk: {k == 32n : Nat}, +x: U32) -> {C.fits(k, v(x)) == True{} : Bool}:
39 %Equal.sym(Bool, C.fits(k, v(x)), Nat.is_lt(v(x), C.pow2(k)), WW.fits_lt(k, v(x))) : {_ == True{} : Bool}
40 U32P.val_lt(1n, {==}, k, hk, x)
41
42
43def vb(+x: U32) -> {C.fits(32n, v(x)) == True{} : Bool}:
44 vb_k(32n, {==}, x)
45
46def lt_k(+k: Nat, +n: Nat, +h: {C.fits(k, n) == True{} : Bool}) -> {Nat.is_lt(n, C.pow2(k)) == True{} : Bool}:
47 %WW.fits_lt(k, n) : {_ == True{} : Bool}
48 h
49
50def vo_k(+k: Nat, +hk: {k == 32n : Nat}, +n: Nat, +h: {C.fits(k, n) == True{} : Bool}) -> {v(U32.from_nat(n)) == n : Nat}:
51 U.to_nat_from_nat(n, k, U32P.le_k(k, hk), lt_k(k, n, h))
52
53
54def vo(+n: Nat, +h: {C.fits(32n, n) == True{} : Bool}) -> {v(U32.from_nat(n)) == n : Nat}:
55 vo_k(32n, {==}, n, h)
56
57def rt(+x: U32) -> {U32.from_nat(v(x)) == x : U32}:
58 U32P.round_trip(x)
59
60
61
62def true_ne_false(+h: {True{} == False{} : Bool}) -> Empty:
63 U32P.true_ne_false(h)
64
65def is_zero_c(+a: U32, +c: Bool, +hc: {U32.is_zero(a) == c : Bool}, +n: Nat, +hn: {v(a) == n : Nat}) -> {c == Nat.is_eq(v(a), 0n) : Bool}:
66 match c:
67 case True{}:
68 %Equal.sym(U32, a, 0, A.eq_of(a, 0, hc)) : {True{} == Nat.is_eq(v(_), 0n) : Bool}
69 {==}
70 case False{}:
71 match n:
72 case 0n:
73 +hz = L.subst(U32, z => {U32.is_zero(z) == True{} : Bool}, 0, a, Equal.sym(U32, a, 0, U.injective(a, 0, hn)), {==})
74 Empty.absurd({False{} == Nat.is_eq(v(a), 0n) : Bool}, true_ne_false(Equal.trans(Bool, True{}, U32.is_zero(a), False{}, Equal.sym(Bool, U32.is_zero(a), True{}, hz), hc)))
75 case 1n+ +p:
76 %Equal.sym(Nat, v(a), 1n+p, hn) : {False{} == Nat.is_eq(_, 0n) : Bool}
77 {==}
78
79
80def zero_nat(+a: U32) -> {U32.is_zero(a) == Nat.is_eq(v(a), 0n) : Bool}:
81 is_zero_c(a, U32.is_zero(a), {==}, v(a), {==})
82
83
84def eq_c(+x: U32, +y: U32, +c: Bool, +hc: {U32.is_eq(x, y) == c : Bool}, +d: Bool, +hd: {Nat.is_eq(v(x), v(y)) == d : Bool}) -> {c == d : Bool}:
85 match c d:
86 case True{} True{}:
87 {==}
88 case False{} False{}:
89 {==}
90 case True{} False{}:
91 +e = A.eq_of(x, y, hc)
92 +hd2 = L.subst(U32, z => {Nat.is_eq(v(x), v(z)) == False{} : Bool}, y, x, Equal.sym(U32, x, y, e), hd)
93 Empty.absurd({True{} == False{} : Bool}, true_ne_false(Equal.trans(Bool, True{}, Nat.is_eq(v(x), v(x)), False{}, Equal.sym(Bool, Nat.is_eq(v(x), v(x)), True{}, N.is_eq_refl(v(x))), hd2)))
94 case False{} True{}:
95 +e = U.injective(x, y, N.eq_from_is_eq(v(x), v(y), hd))
96 +hc2 = L.subst(U32, z => {U32.is_eq(x, z) == False{} : Bool}, y, x, Equal.sym(U32, x, y, e), hc)
97 Empty.absurd({False{} == True{} : Bool}, true_ne_false(Equal.trans(Bool, True{}, U32.is_eq(x, x), False{}, Equal.sym(Bool, U32.is_eq(x, x), True{}, A.eq_refl(x)), hc2)))
98
99def eq_nat(+x: U32, +y: U32) -> {U32.is_eq(x, y) == Nat.is_eq(v(x), v(y)) : Bool}:
100 eq_c(x, y, U32.is_eq(x, y), {==}, Nat.is_eq(v(x), v(y)), {==})
101
102
103def carry_fits(+k: Nat, +s: Nat, +n: Nat, +c: Bool, +e: {Nat.add(s, WD.sc(k, S.bit_value(c))) == n : Nat}, +hs: {Nat.is_lt(s, C.pow2(k)) == True{} : Bool}) -> {c == Bool.not(C.fits(k, n)) : Bool}:
104 match c:
105 case False{}:
106 %Equal.sym(Bool, C.fits(k, n), Nat.is_lt(n, C.pow2(k)), WW.fits_lt(k, n)) : {False{} == Bool.not(_) : Bool}
107 %e : {False{} == Bool.not(Nat.is_lt(_, C.pow2(k))) : Bool}
108 %Equal.sym(Nat, WD.sc(k, 0n), 0n, A.sc_zero(k)) : {False{} == Bool.not(Nat.is_lt(Nat.add(s, _), C.pow2(k))) : Bool}
109 %Equal.sym(Nat, Nat.add(s, 0n), s, N.add_zero(s)) : {False{} == Bool.not(Nat.is_lt(_, C.pow2(k))) : Bool}
110 %Equal.sym(Bool, Nat.is_lt(s, C.pow2(k)), True{}, hs) : {False{} == Bool.not(_) : Bool}
111 {==}
112 case True{}:
113 %Equal.sym(Bool, C.fits(k, n), Nat.is_lt(n, C.pow2(k)), WW.fits_lt(k, n)) : {True{} == Bool.not(_) : Bool}
114 %e : {True{} == Bool.not(Nat.is_lt(_, C.pow2(k))) : Bool}
115 %U.pow2_scale(k) : {True{} == Bool.not(Nat.is_lt(Nat.add(s, _), C.pow2(k))) : Bool}
116 +le = L.subst(Nat, z => {Nat.is_le(C.pow2(k), z) == True{} : Bool}, Nat.add(C.pow2(k), s), Nat.add(s, C.pow2(k)), N.add_comm(C.pow2(k), s), N.le_add_right(C.pow2(k), s))
117 %Equal.sym(Bool, Nat.is_lt(Nat.add(s, C.pow2(k)), C.pow2(k)), False{}, N.le_not_lt(Nat.add(s, C.pow2(k)), C.pow2(k), le)) : {True{} == Bool.not(_) : Bool}
118 {==}
119
120
121
122def ops_zero() -> SI.Ops.zero(~U32, ~I.u32_op, ~SG.u32_val):
123 {==}
124
125def ops_one() -> SI.Ops.one(~U32, ~I.u32_op, ~SG.u32_val):
126 {==}
127
128def ops_abs(+a: U32) -> SI.Ops.abs(~U32, ~I.u32_op, a):
129 {==}
130
131def tests_lt(+a: U32, +b: U32) -> SI.Tests.lt(~U32, ~I.u32_is, ~SG.u32_val, a, b):
132 U.is_lt_nat(a, b)
133
134def tests_is_zero(+a: U32) -> SI.Tests.is_zero(~U32, ~I.u32_is, ~SG.u32_val, a):
135 zero_nat(a)
136
137def ops_sub(+a: U32, +b: U32, +h: {Nat.is_le(SG.u32_val(b), SG.u32_val(a)) == True{} : Bool}) -> SI.Ops.sub(~U32, ~I.u32_op, ~SG.u32_val, a, b, h):
138 U.sub_nat(a, b, h)
139
140def nz(+b: U32, +h: {Nat.is_eq(SG.u32_val(b), 0n) == False{} : Bool}) -> {U32.is_zero(b) == False{} : Bool}:
141 Equal.trans(Bool, U32.is_zero(b), Nat.is_eq(v(b), 0n), False{}, zero_nat(b), h)
142
143def ops_quot(+a: U32, +b: U32, +h: {Nat.is_eq(SG.u32_val(b), 0n) == False{} : Bool}) -> SI.Ops.quot(~U32, ~I.u32_op, ~SG.u32_val, a, b, h):
144 UD.div_nat(a, b, nz(b, h))
145
146def ops_rem(+a: U32, +b: U32, +h: {Nat.is_eq(SG.u32_val(b), 0n) == False{} : Bool}) -> SI.Ops.rem(~U32, ~I.u32_op, ~SG.u32_val, a, b, h):
147 UD.mod_nat(a, b, nz(b, h))
148
149def hlf_div2(+n: Nat) -> {UH.hlf(n) == Nat.div(n, 2n) : Nat}:
150 match n:
151 case 0n:
152 {==}
153 case 1n:
154 {==}
155 case 2n+ +q:
156 %Equal.sym(Nat, Nat.div(Nat.add(2n, q), 2n), 1n+Nat.div(q, 2n), N.div2_step(q)) : {1n+UH.hlf(q) == _ : Nat}
157 N.succ_cong(UH.hlf(q), Nat.div(q, 2n), hlf_div2(q))
158
159def ops_half(+a: U32) -> SI.Ops.half(~U32, ~I.u32_op, ~SG.u32_val, a):
160 Equal.trans(Nat, v(U32.shr(a)), UH.hlf(v(a)), Nat.div(v(a), 2n), UH.shr_value(a), hlf_div2(v(a)))
161
162def carry_of(+a: U32, +b: U32, +h: {I.u32_is(NM.AddOver{a, b}) == False{} : Bool}) -> {P64.carry32(a, b) == False{} : Bool}:
163 Equal.trans(Bool, P64.carry32(a, b), U32.is_lt(U32.add(a, b), a), False{}, Equal.sym(Bool, U32.is_lt(U32.add(a, b), a), P64.carry32(a, b), P64.add_lt(a, b)), h)
164
165def ops_add(+a: U32, +b: U32, +h: {I.u32_is(NM.AddOver{a, b}) == False{} : Bool}) -> SI.Ops.add(~U32, ~I.u32_op, ~I.u32_is, ~SG.u32_val, a, b, h):
166 +e = L.subst(Bool, c => {Nat.add(UD.v(U32.add(a, b)), WD.sc(32n, S.bit_value(c))) == Nat.add(UD.v(a), UD.v(b)) : Nat}, P64.carry32(a, b), False{}, carry_of(a, b, h), P64.add_cons(a, b))
167 Equal.trans(Nat, v(U32.add(a, b)), Nat.add(v(U32.add(a, b)), 0n), Nat.add(v(a), v(b)), Equal.sym(Nat, Nat.add(v(U32.add(a, b)), 0n), v(U32.add(a, b)), N.add_zero(v(U32.add(a, b)))), e)
168
169def add_over_k(+k: Nat, +hk: {k == 32n : Nat}, +a: U32, +b: U32) -> {P64.carry32(a, b) == Bool.not(C.fits(k, Nat.add(v(a), v(b)))) : Bool}:
170 +e = L.subst(Nat, z => {Nat.add(UD.v(U32.add(a, b)), WD.sc(z, S.bit_value(P64.carry32(a, b)))) == Nat.add(UD.v(a), UD.v(b)) : Nat}, 32n, k, Equal.sym(Nat, k, 32n, hk), P64.add_cons(a, b))
171 carry_fits(k, v(U32.add(a, b)), Nat.add(v(a), v(b)), P64.carry32(a, b), e, U32P.val_lt(1n, {==}, k, hk, U32.add(a, b)))
172
173def tests_add_over(+a: U32, +b: U32) -> SI.Tests.add_over(~U32, ~I.u32_is, ~SG.u32_val, 32n, a, b):
174 %Equal.sym(Bool, U32.is_lt(U32.add(a, b), a), P64.carry32(a, b), P64.add_lt(a, b)) : {_ == Bool.not(C.fits(32n, Nat.add(v(a), v(b)))) : Bool}
175 add_over_k(32n, {==}, a, b)
176
177
178
179def dbl(+h: Nat) -> {Nat.mul(h, 2n) == Nat.double(h) : Nat}:
180 match h:
181 case 0n:
182 {==}
183 case 1n+ +p:
184 %Equal.sym(Nat, Nat.mul(p, 2n), Nat.double(p), dbl(p)) : {Nat.add(2n, _) == Nat.double(1n+p) : Nat}
185 {==}
186
187
188def mod2_bit(+r: Nat, +h: Nat, +hr: {Nat.is_lt(r, 2n) == True{} : Bool}) -> {r == Nat.mod(Nat.add(r, Nat.double(h)), 2n) : Nat}:
189 match r:
190 case 0n:
191 %dbl(h) : {0n == Nat.mod(_, 2n) : Nat}
192 %N.add_zero(Nat.mul(h, 2n)) : {0n == Nat.mod(_, 2n) : Nat}
193 Equal.sym(Nat, Nat.mod(Nat.add(Nat.mul(h, 2n), 0n), 2n), 0n, NA.absorb(1n, h, 0n))
194 case 1n:
195 %dbl(h) : {1n == Nat.mod(1n+_, 2n) : Nat}
196 %N.add_zero(Nat.mul(h, 2n)) : {1n == Nat.mod(1n+_, 2n) : Nat}
197 %N.add_succ(Nat.mul(h, 2n), 0n) : {1n == Nat.mod(_, 2n) : Nat}
198 Equal.sym(Nat, Nat.mod(Nat.add(Nat.mul(h, 2n), 1n), 2n), 1n, NA.absorb(1n, h, 1n))
199 case 2n+ +q:
200 Empty.absurd({2n+q == Nat.mod(Nat.add(2n+q, Nat.double(h)), 2n) : Nat}, N.lt_zero_absurd(q, hr))
201
202def odd_val(+a: U32) -> {v(U32.and(a, 1)) == Nat.mod(v(a), 2n) : Nat}:
203 +e = PD.and32(1n, a, 1, {==})
204 %Equal.sym(Nat, v(a), Nat.add(v(U32.and(a, 1)), Nat.double(PD.hp32(1n, a))), e) : {v(U32.and(a, 1)) == Nat.mod(_, 2n) : Nat}
205 mod2_bit(v(U32.and(a, 1)), PD.hp32(1n, a), PD.and32_lt(1n, 1n, {==}, a, 1, {==}))
206
207def tests_odd(+a: U32) -> SI.Tests.odd(~U32, ~I.u32_is, ~SG.u32_val, a):
208 %Equal.sym(Bool, U32.is_eq(U32.and(a, 1), 1), Nat.is_eq(v(U32.and(a, 1)), v(1)), eq_nat(U32.and(a, 1), 1)) : {_ == Nat.is_eq(Nat.mod(v(a), 2n), 1n) : Bool}
209 %Equal.sym(Nat, v(U32.and(a, 1)), Nat.mod(v(a), 2n), odd_val(a)) : {Nat.is_eq(_, 1n) == Nat.is_eq(Nat.mod(v(a), 2n), 1n) : Bool}
210 {==}
211
212
213
214def not_false(+b: Bool, +h: {Bool.not(b) == False{} : Bool}) -> {b == True{} : Bool}:
215 match b:
216 case True{}:
217 {==}
218 case False{}:
219 Empty.absurd({False{} == True{} : Bool}, true_ne_false(h))
220
221
222def fits_split(+k: Nat, +lo: Nat, +hi: Nat, +hl: {Nat.is_lt(lo, C.pow2(k)) == True{} : Bool}) -> {C.fits(k, Nat.add(lo, WD.sc(k, hi))) == Nat.is_eq(hi, 0n) : Bool}:
223 match hi:
224 case 0n:
225 %Equal.sym(Nat, WD.sc(k, 0n), 0n, A.sc_zero(k)) : {C.fits(k, Nat.add(lo, _)) == True{} : Bool}
226 %Equal.sym(Nat, Nat.add(lo, 0n), lo, N.add_zero(lo)) : {C.fits(k, _) == True{} : Bool}
227 %Equal.sym(Bool, C.fits(k, lo), Nat.is_lt(lo, C.pow2(k)), WW.fits_lt(k, lo)) : {_ == True{} : Bool}
228 hl
229 case 1n+ +h:
230 %Equal.sym(Bool, C.fits(k, Nat.add(lo, WD.sc(k, 1n+h))), Nat.is_lt(Nat.add(lo, WD.sc(k, 1n+h)), C.pow2(k)), WW.fits_lt(k, Nat.add(lo, WD.sc(k, 1n+h)))) : {_ == False{} : Bool}
231 +p1 = L.subst(Nat, z => {Nat.is_le(z, WD.sc(k, 1n+h)) == True{} : Bool}, WD.sc(k, 1n), C.pow2(k), Equal.sym(Nat, C.pow2(k), WD.sc(k, 1n), U.pow2_scale(k)), AR.sc_le(k, 1n, 1n+h, N.zero_le(h)))
232 +p2 = L.subst(Nat, z => {Nat.is_le(WD.sc(k, 1n+h), z) == True{} : Bool}, Nat.add(WD.sc(k, 1n+h), lo), Nat.add(lo, WD.sc(k, 1n+h)), N.add_comm(WD.sc(k, 1n+h), lo), N.le_add_right(WD.sc(k, 1n+h), lo))
233 N.le_not_lt(Nat.add(lo, WD.sc(k, 1n+h)), C.pow2(k), N.le_trans(C.pow2(k), WD.sc(k, 1n+h), Nat.add(lo, WD.sc(k, 1n+h)), p1, p2))
234
235def hi_zero(+a: U32, +b: U32, +h: {I.u32_is(NM.MulOver{a, b}) == False{} : Bool}) -> {v(X.hi(X.mul32(a, b))) == 0n : Nat}:
236 +z = not_false(U32.is_zero(X.hi(X.mul32(a, b))), h)
237 N.eq_from_is_eq(v(X.hi(X.mul32(a, b))), 0n, Equal.trans(Bool, Nat.is_eq(v(X.hi(X.mul32(a, b))), 0n), U32.is_zero(X.hi(X.mul32(a, b))), True{}, Equal.sym(Bool, U32.is_zero(X.hi(X.mul32(a, b))), Nat.is_eq(v(X.hi(X.mul32(a, b))), 0n), zero_nat(X.hi(X.mul32(a, b)))), z))
238
239
240def prod_limbs(+a: U32, +b: U32) -> {Nat.add(v(X.lo(X.mul32(a, b))), WD.sc(32n, v(X.hi(X.mul32(a, b))))) == Nat.mul(v(a), v(b)) : Nat}:
241 e = W64M.mul32_value(a, b)
242 +lo = X.lo(X.mul32(a, b))
243 +hi = X.hi(X.mul32(a, b))
244 Equal.trans(Nat, Nat.add(v(lo), WD.sc(32n, v(hi))), Nat.add(v(lo), C.shift(32n, v(hi))), Nat.mul(v(a), v(b)), W64M.cong_r(v(lo), WD.sc(32n, v(hi)), C.shift(32n, v(hi)), Equal.sym(Nat, C.shift(32n, v(hi)), WD.sc(32n, v(hi)), W64M.shift_sc(32n, v(hi)))), e)
245
246def ops_mul_one(+one: Nat, +h1: {one == 1n : Nat}, +a: U32, +b: U32, +h: {I.u32_is(NM.MulOver{a, b}) == False{} : Bool}) -> {v(U32.mul(a, b)) == Nat.mul(v(a), v(b)) : Nat}:
247 +lo = X.lo(X.mul32(a, b))
248 +hi = X.hi(X.mul32(a, b))
249 +e0 = Equal.trans(Nat, v(lo), Nat.add(v(lo), 0n), Nat.add(v(lo), WD.sc(32n, v(hi))), Equal.sym(Nat, Nat.add(v(lo), 0n), v(lo), N.add_zero(v(lo))), W64M.cong_r(v(lo), 0n, WD.sc(32n, v(hi)), Equal.trans(Nat, 0n, WD.sc(32n, 0n), WD.sc(32n, v(hi)), Equal.sym(Nat, WD.sc(32n, 0n), 0n, A.sc_zero(32n)), W64M.cong_sc(32n, 0n, v(hi), Equal.sym(Nat, v(hi), 0n, hi_zero(a, b, h))))))
250 +ep = Equal.trans(Nat, v(lo), Nat.add(v(lo), WD.sc(32n, v(hi))), Nat.mul(v(a), v(b)), e0, prod_limbs(a, b))
251 +lt = L.subst(Nat, z => {Nat.is_lt(z, WD.sc(32n, one)) == True{} : Bool}, v(lo), Nat.mul(v(a), v(b)), ep, UD.vb(one, h1, lo))
252 PD.mul32(one, h1, a, b, lt)
253
254def ops_mul(+a: U32, +b: U32, +h: {I.u32_is(NM.MulOver{a, b}) == False{} : Bool}) -> SI.Ops.mul(~U32, ~I.u32_op, ~I.u32_is, ~SG.u32_val, a, b, h):
255 ops_mul_one(1n, {==}, a, b, h)
256
257def mul_over_k(+k: Nat, +hk: {k == 32n : Nat}, +a: U32, +b: U32) -> {U32.is_zero(X.hi(X.mul32(a, b))) == C.fits(k, Nat.mul(v(a), v(b))) : Bool}:
258 +lo = X.lo(X.mul32(a, b))
259 +hi = X.hi(X.mul32(a, b))
260 +ek = L.subst(Nat, z => {Nat.add(v(lo), WD.sc(z, v(hi))) == Nat.mul(v(a), v(b)) : Nat}, 32n, k, Equal.sym(Nat, k, 32n, hk), prod_limbs(a, b))
261 %ek : {U32.is_zero(hi) == C.fits(k, _) : Bool}
262 %Equal.sym(Bool, C.fits(k, Nat.add(v(lo), WD.sc(k, v(hi)))), Nat.is_eq(v(hi), 0n), fits_split(k, v(lo), v(hi), U32P.val_lt(1n, {==}, k, hk, lo))) : {U32.is_zero(hi) == _ : Bool}
263 zero_nat(hi)
264
265def tests_mul_over(+a: U32, +b: U32) -> SI.Tests.mul_over(~U32, ~I.u32_is, ~SG.u32_val, 32n, a, b):
266 Equal.cong(Bool, Bool, t => Bool.not(t), U32.is_zero(X.hi(X.mul32(a, b))), C.fits(32n, Nat.mul(v(a), v(b))), mul_over_k(32n, {==}, a, b))
267
268
269
270def pos_nz(+x: Nat, +y: Nat, +h: {Nat.is_lt(x, y) == True{} : Bool}) -> {Nat.is_eq(y, 0n) == False{} : Bool}:
271 match y:
272 case 0n:
273 Empty.absurd({Nat.is_eq(0n, 0n) == False{} : Bool}, N.lt_zero_absurd(x, h))
274 case 1n+yp:
275 {==}
276
277def ops_mulmod(+a: U32, +b: U32, +m: U32, +ha: {Nat.is_lt(SG.u32_val(a), SG.u32_val(m)) == True{} : Bool}, +hb: {Nat.is_lt(SG.u32_val(b), SG.u32_val(m)) == True{} : Bool}) -> SI.Ops.mulmod(~U32, ~I.u32_op, ~SG.u32_val, a, b, m, ha, hb):
278 e1 = W64D.mod32_value(X.mul32(a, b), m, nz(m, pos_nz(v(a), v(m), ha)))
279 e2 = W64M.mul32_value(a, b)
280 Equal.trans(Nat, v(X.mod32(X.mul32(a, b), m)), Nat.mod(SW.value(X.mul32(a, b)), v(m)), Nat.mod(Nat.mul(v(a), v(b)), v(m)), e1, Equal.cong(Nat, Nat, t => Nat.mod(t, v(m)), SW.value(X.mul32(a, b)), Nat.mul(v(a), v(b)), e2))
281
282
283
284def pw_table(+k: Nat, +hk: {Nat.is_lt(k, 32n) == True{} : Bool}) -> {X.pow2(k) == U32{WD.pw(32n, k)} : U32}:
285 match k:
286 case 0n:
287 {==}
288 case 1n:
289 {==}
290 case 2n:
291 {==}
292 case 3n:
293 {==}
294 case 4n:
295 {==}
296 case 5n:
297 {==}
298 case 6n:
299 {==}
300 case 7n:
301 {==}
302 case 8n:
303 {==}
304 case 9n:
305 {==}
306 case 10n:
307 {==}
308 case 11n:
309 {==}
310 case 12n:
311 {==}
312 case 13n:
313 {==}
314 case 14n:
315 {==}
316 case 15n:
317 {==}
318 case 16n:
319 {==}
320 case 17n:
321 {==}
322 case 18n:
323 {==}
324 case 19n:
325 {==}
326 case 20n:
327 {==}
328 case 21n:
329 {==}
330 case 22n:
331 {==}
332 case 23n:
333 {==}
334 case 24n:
335 {==}
336 case 25n:
337 {==}
338 case 26n:
339 {==}
340 case 27n:
341 {==}
342 case 28n:
343 {==}
344 case 29n:
345 {==}
346 case 30n:
347 {==}
348 case 31n:
349 {==}
350 case 32n+ +j:
351 Empty.absurd({X.pow2(32n+j) == U32{WD.pw(32n, 32n+j)} : U32}, N.lt_zero_absurd(j, hk))
352
353def ops_pow2(+k: Nat, +hk: {Nat.is_lt(k, 32n) == True{} : Bool}) -> SI.Ops.pow2(~U32, ~I.u32_op, ~SG.u32_val, 32n, k, hk):
354 %Equal.sym(U32, X.pow2(k), U32{WD.pw(32n, k)}, pw_table(k, hk)) : {v(_) == C.pow2(k) : Nat}
355 %Equal.sym(Nat, C.pow2(k), WD.sc(k, 1n), U.pow2_scale(k)) : {v(U32{WD.pw(32n, k)}) == _ : Nat}
356 PD.pow32(k, hk, 1n, {==}, U32{WD.pw(32n, k)}, {==})
357
358
359
360def ops_sqrt(+a: U32) -> SI.Ops.sqrt(~U32, ~I.u32_op, ~SG.u32_val, a):
361 W64S.isqrt32_value(a)