~/jendhub

proofs/math/typed/fix32.bend

bend-collections-laws-math@1.0.0.0 · 350 lines · 63 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/generic.bend as SG
4import bend-collections-laws-math@1.0.0.0/spec/math/fixed.bend as SF
5import bend-collections-laws-math@1.0.0.0/src/math/w64.bend as X
6import bend-collections-laws-math@1.0.0.0/src/math/fixed.bend as F
7import bend-collections-laws-math@1.0.0.0/src/math/generic.bend as GN
8import bend-collections-laws-math@1.0.0.0/src/math/instances.bend as I
9import bend-collections-laws-math@1.0.0.0/src/math/num.bend as NM
10import bend-collections-laws-math@1.0.0.0/src/math/natural.bend as M
11import bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend as N
12import bend-collections-laws-math@1.0.0.0/proofs/lib/logic.bend as L
13import bend-collections-laws-math@1.0.0.0/proofs/lib/arith.bend as AR
14import bend-collections-laws-math@1.0.0.0/proofs/lib/word.bend as WD
15import bend-collections-laws-math@1.0.0.0/proofs/lib/u32.bend as U3
16import bend-collections-laws-math@1.0.0.0/proofs/lib/u32div.bend as UD
17import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend as NA
18import bend-collections-laws-math@1.0.0.0/proofs/math/natural/arith.bend as R
19import bend-collections-laws-math@1.0.0.0/proofs/math/natural/modpow.bend as MP
20import bend-collections-laws-math@1.0.0.0/proofs/math/natural/bits.bend as B
21import bend-collections-laws-math@1.0.0.0/proofs/math/typed/width.bend as WW
22import bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64add.bend as WA
23import bend-collections-laws-math@1.0.0.0/proofs/math/u64/u64.bend as P64
24import bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64sh.bend as SH
25import bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64est.bend as WE
26import bend-collections-laws-math@1.0.0.0/proofs/math/typed/shrn.bend as SHN
27import bend-collections-laws-math@1.0.0.0/proofs/math/typed/u32laws.bend as LW
28import bend-collections-laws-math@1.0.0.0/proofs/math/typed/u32int.bend as UI
29import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64bits.bend as FB
30import bend-collections-laws-math@1.0.0.0/proofs/math/typed/fixgen.bend as G
31
32# The U32 clauses of spec/math/fixed.bend (Rust's u32 checked_*,
33# wrapping_*, saturating_*, overflowing_* families) from Base's U32
34# operations through their values: U32.add and U32.sub with their carry
35# (w64add.bend's acons / sub_cons, HACL*'s addcarry / subborrow lemmas),
36# U32.mul modulo 2^32 (w64sh.bend's mul_low), the long division of
37# proofs/lib/u32div.bend and the generic pow of u32int.bend.
38
39def vs(+s: U32) -> Nat:
40  U32.to_nat(s)
41
42# ---- the largest value 2^32 - 1 (1 kept as one, compared as a U32) ----
43
44def zero_add(+x: Nat) -> {Nat.add(0n, x) == x : Nat}:
45  Equal.trans(Nat, Nat.add(0n, x), Nat.add(x, 0n), x, N.add_comm(0n, x), N.add_zero(x))
46
47def topw(+one: Nat, +h1: {one == 1n : Nat}, +w: U32, +pw: {w == U32{WD.mask(32n, 32n)} : U32}) -> {Bool.and(C.fits(32n, SG.u32_val(w)), Bool.not(C.fits(32n, 1n+SG.u32_val(w)))) == True{} : Bool}:
48  +S = C.shift(32n, one)
49  +e1 = Equal.cong(Nat, Bool, t => C.fits(32n, t), 1n+SG.u32_val(w), S, WE.m32(one, h1, w, pw))
50  +e2 = Equal.cong(Nat, Bool, t => C.fits(32n, t), S, Nat.add(0n, S), Equal.sym(Nat, Nat.add(0n, S), S, zero_add(S)))
51  G.top_ok(32n, SG.u32_val(w), LW.vb(w), Equal.trans(Bool, C.fits(32n, 1n+SG.u32_val(w)), C.fits(32n, S), False{}, e1, Equal.trans(Bool, C.fits(32n, S), C.fits(32n, Nat.add(0n, S)), False{}, e2, WW.unfit_one(32n, one, h1, 0n))))
52
53def top(+one: Nat, +h1: {one == 1n : Nat}) -> {Bool.and(C.fits(32n, SG.u32_val(F.u32_max())), Bool.not(C.fits(32n, 1n+SG.u32_val(F.u32_max())))) == True{} : Bool}:
54  L.subst(U32, t => {Bool.and(C.fits(32n, SG.u32_val(t)), Bool.not(C.fits(32n, 1n+SG.u32_val(t)))) == True{} : Bool}, 4294967295, F.u32_max(), {==}, topw(one, h1, 4294967295, {==}))
55
56# ---- the operations modulo 2^32 ----
57
58def add_low(+x: U32, +y: U32) -> {SG.u32_val(U32.add(x, y)) == C.low(32n, Nat.add(SG.u32_val(x), SG.u32_val(y))) : Nat}:
59  +c = WA.bv(P64.carry32(x, y))
60  +e = Equal.cong(Nat, Nat, t => C.low(32n, t), Nat.add(SG.u32_val(x), SG.u32_val(y)), Nat.add(SG.u32_val(U32.add(x, y)), C.shift(32n, c)), Equal.sym(Nat, Nat.add(SG.u32_val(U32.add(x, y)), C.shift(32n, c)), Nat.add(SG.u32_val(x), SG.u32_val(y)), WA.acons(x, y)))
61  Equal.sym(Nat, C.low(32n, Nat.add(SG.u32_val(x), SG.u32_val(y))), SG.u32_val(U32.add(x, y)), Equal.trans(Nat, C.low(32n, Nat.add(SG.u32_val(x), SG.u32_val(y))), C.low(32n, Nat.add(SG.u32_val(U32.add(x, y)), C.shift(32n, c))), SG.u32_val(U32.add(x, y)), e, WW.low_u(32n, SG.u32_val(U32.add(x, y)), c, LW.vb(U32.add(x, y)))))
62
63def mul_low(+x: U32, +y: U32) -> {SG.u32_val(U32.mul(x, y)) == C.low(32n, Nat.mul(SG.u32_val(x), SG.u32_val(y))) : Nat}:
64  SH.mul_low(x, y)
65
66def add_over(+a: U32, +b: U32) -> {F.u32_add_over(a, b) == Bool.not(C.fits(32n, Nat.add(SG.u32_val(a), SG.u32_val(b)))) : Bool}:
67  LW.tests_add_over(a, b)
68
69def mul_over(+a: U32, +b: U32) -> {F.u32_mul_over(a, b) == Bool.not(C.fits(32n, Nat.mul(SG.u32_val(a), SG.u32_val(b)))) : Bool}:
70  LW.tests_mul_over(a, b)
71
72def lt_nat(+a: U32, +b: U32) -> {U32.is_lt(a, b) == Nat.is_lt(SG.u32_val(a), SG.u32_val(b)) : Bool}:
73  U3.is_lt_nat(a, b)
74
75# ---- add, mul ----
76
77def checked_add(+a: U32, +b: U32) -> SF.CheckedAdd.value(~U32, ~SG.u32_val, ~F.u32_checked_add, 32n, a, b):
78  G.chk_fit(~U32, ~SG.u32_val, 32n, Nat.add(SG.u32_val(a), SG.u32_val(b)), U32.add(a, b), F.u32_add_over(a, b), add_over(a, b), add_low(a, b), C.fits(32n, Nat.add(SG.u32_val(a), SG.u32_val(b))), {==})
79
80def wrapping_add(+a: U32, +b: U32) -> SF.WrappingAdd.value(~U32, ~SG.u32_val, ~F.u32_wrapping_add, 32n, a, b):
81  add_low(a, b)
82
83def saturating_add(+a: U32, +b: U32) -> SF.SaturatingAdd.value(~U32, ~SG.u32_val, ~F.u32_saturating_add, 32n, a, b):
84  G.sat_fit(~U32, ~SG.u32_val, 32n, Nat.add(SG.u32_val(a), SG.u32_val(b)), U32.add(a, b), F.u32_max(), F.u32_add_over(a, b), add_over(a, b), add_low(a, b), top(1n, {==}), C.fits(32n, Nat.add(SG.u32_val(a), SG.u32_val(b))), {==})
85
86def overflowing_add_value(+a: U32, +b: U32) -> SF.OverflowingAdd.value(~U32, ~SG.u32_val, ~F.u32_overflowing_add, 32n, a, b):
87  add_low(a, b)
88
89def overflowing_add_flag(+a: U32, +b: U32) -> SF.OverflowingAdd.flag(~U32, ~SG.u32_val, ~F.u32_overflowing_add, 32n, a, b):
90  add_over(a, b)
91
92def checked_mul(+a: U32, +b: U32) -> SF.CheckedMul.value(~U32, ~SG.u32_val, ~F.u32_checked_mul, 32n, a, b):
93  G.chk_fit(~U32, ~SG.u32_val, 32n, Nat.mul(SG.u32_val(a), SG.u32_val(b)), U32.mul(a, b), F.u32_mul_over(a, b), mul_over(a, b), mul_low(a, b), C.fits(32n, Nat.mul(SG.u32_val(a), SG.u32_val(b))), {==})
94
95def wrapping_mul(+a: U32, +b: U32) -> SF.WrappingMul.value(~U32, ~SG.u32_val, ~F.u32_wrapping_mul, 32n, a, b):
96  mul_low(a, b)
97
98def saturating_mul(+a: U32, +b: U32) -> SF.SaturatingMul.value(~U32, ~SG.u32_val, ~F.u32_saturating_mul, 32n, a, b):
99  G.sat_fit(~U32, ~SG.u32_val, 32n, Nat.mul(SG.u32_val(a), SG.u32_val(b)), U32.mul(a, b), F.u32_max(), F.u32_mul_over(a, b), mul_over(a, b), mul_low(a, b), top(1n, {==}), C.fits(32n, Nat.mul(SG.u32_val(a), SG.u32_val(b))), {==})
100
101def overflowing_mul_value(+a: U32, +b: U32) -> SF.OverflowingMul.value(~U32, ~SG.u32_val, ~F.u32_overflowing_mul, 32n, a, b):
102  mul_low(a, b)
103
104def overflowing_mul_flag(+a: U32, +b: U32) -> SF.OverflowingMul.flag(~U32, ~SG.u32_val, ~F.u32_overflowing_mul, 32n, a, b):
105  mul_over(a, b)
106
107# ---- sub ----
108
109def sub_exact(+a: U32, +b: U32, +h: {Nat.is_le(SG.u32_val(b), SG.u32_val(a)) == True{} : Bool}) -> {SG.u32_val(U32.sub(a, b)) == Nat.sub(SG.u32_val(a), SG.u32_val(b)) : Nat}:
110  LW.ops_sub(a, b, h)
111
112def csub(+a: U32, +b: U32, +ok: Bool, +hok: {Nat.is_le(SG.u32_val(b), SG.u32_val(a)) == ok : Bool}) -> {SF.mval(~U32, ~SG.u32_val, F.opt(U32, U32.is_lt(a, b), U32.sub(a, b))) == SF.keep(ok, Nat.sub(SG.u32_val(a), SG.u32_val(b))) : Maybe<&2, Nat>}:
113  match ok:
114    case True{}:
115      G.some_of(~U32, ~SG.u32_val, U32.is_lt(a, b), Equal.trans(Bool, U32.is_lt(a, b), Nat.is_lt(SG.u32_val(a), SG.u32_val(b)), False{}, lt_nat(a, b), N.le_not_lt(SG.u32_val(a), SG.u32_val(b), hok)), U32.sub(a, b), Nat.sub(SG.u32_val(a), SG.u32_val(b)), sub_exact(a, b, hok))
116    case False{}:
117      G.none_of(~U32, ~SG.u32_val, U32.is_lt(a, b), Equal.trans(Bool, U32.is_lt(a, b), Nat.is_lt(SG.u32_val(a), SG.u32_val(b)), True{}, lt_nat(a, b), N.not_le_lt(SG.u32_val(b), SG.u32_val(a), hok)), U32.sub(a, b))
118
119def checked_sub(+a: U32, +b: U32) -> SF.CheckedSub.value(~U32, ~SG.u32_val, ~F.u32_checked_sub, a, b):
120  csub(a, b, Nat.is_le(SG.u32_val(b), SG.u32_val(a)), {==})
121
122def sub_big(+n: Nat, +d: Nat, +h: {Nat.is_le(n, d) == True{} : Bool}) -> {Nat.sub(n, d) == 0n : Nat}:
123  match n d:
124    case 0n _:
125      R.zsub(d)
126    case 1n+np 0n:
127      Empty.absurd({Nat.sub(1n+np, 0n) == 0n : Nat}, L.false_true(h))
128    case 1n+ +np 1n+ +dp:
129      sub_big(np, dp, h)
130
131def ssub(+a: U32, +b: U32, +c: Bool, +hn: {Nat.is_lt(SG.u32_val(a), SG.u32_val(b)) == c : Bool}) -> {SG.u32_val(F.pick(U32, c, 0, U32.sub(a, b))) == Nat.sub(SG.u32_val(a), SG.u32_val(b)) : Nat}:
132  match c:
133    case True{}:
134      Equal.sym(Nat, Nat.sub(SG.u32_val(a), SG.u32_val(b)), 0n, sub_big(SG.u32_val(a), SG.u32_val(b), N.lt_le(SG.u32_val(a), SG.u32_val(b), hn)))
135    case False{}:
136      sub_exact(a, b, N.not_lt_le(SG.u32_val(a), SG.u32_val(b), hn))
137
138def saturating_sub(+a: U32, +b: U32) -> SF.SaturatingSub.value(~U32, ~SG.u32_val, ~F.u32_saturating_sub, a, b):
139  ssub(a, b, U32.is_lt(a, b), Equal.sym(Bool, U32.is_lt(a, b), Nat.is_lt(SG.u32_val(a), SG.u32_val(b)), lt_nat(a, b)))
140
141def overflowing_sub_flag(+a: U32, +b: U32) -> SF.OverflowingSub.flag(~U32, ~SG.u32_val, ~F.u32_overflowing_sub, a, b):
142  lt_nat(a, b)
143
144def bo_bn(+one: Nat, +h1: {one == 1n : Nat}, +c: Bool) -> {WD.bo(c, one) == SF.bn(c) : Nat}:
145  match c:
146    case True{}:
147      h1
148    case False{}:
149      {==}
150
151def wsub_g(+one: Nat, +h1: {one == 1n : Nat}, +a: U32, +b: U32) -> {Nat.add(SG.u32_val(U32.sub(a, b)), SG.u32_val(b)) == Nat.add(SG.u32_val(a), C.shift(32n, SF.bn(Nat.is_lt(SG.u32_val(a), SG.u32_val(b))))) : Nat}:
152  +e1 = Equal.cong(Bool, Nat, t => Nat.add(SG.u32_val(a), C.shift(32n, WD.bo(t, one))), U32.is_lt(a, b), Nat.is_lt(SG.u32_val(a), SG.u32_val(b)), lt_nat(a, b))
153  +e2 = Equal.cong(Nat, Nat, t => Nat.add(SG.u32_val(a), C.shift(32n, t)), WD.bo(Nat.is_lt(SG.u32_val(a), SG.u32_val(b)), one), SF.bn(Nat.is_lt(SG.u32_val(a), SG.u32_val(b))), bo_bn(one, h1, Nat.is_lt(SG.u32_val(a), SG.u32_val(b))))
154  Equal.trans(Nat, Nat.add(SG.u32_val(U32.sub(a, b)), SG.u32_val(b)), Nat.add(SG.u32_val(a), C.shift(32n, WD.bo(U32.is_lt(a, b), one))), Nat.add(SG.u32_val(a), C.shift(32n, SF.bn(Nat.is_lt(SG.u32_val(a), SG.u32_val(b))))), WA.sub_cons(one, h1, a, b), Equal.trans(Nat, Nat.add(SG.u32_val(a), C.shift(32n, WD.bo(U32.is_lt(a, b), one))), Nat.add(SG.u32_val(a), C.shift(32n, WD.bo(Nat.is_lt(SG.u32_val(a), SG.u32_val(b)), one))), Nat.add(SG.u32_val(a), C.shift(32n, SF.bn(Nat.is_lt(SG.u32_val(a), SG.u32_val(b))))), e1, e2))
155
156def wrapping_sub(+a: U32, +b: U32) -> SF.WrappingSub.value(~U32, ~SG.u32_val, ~F.u32_wrapping_sub, 32n, a, b):
157  wsub_g(1n, {==}, a, b)
158
159def overflowing_sub_value(+a: U32, +b: U32) -> SF.OverflowingSub.value(~U32, ~SG.u32_val, ~F.u32_overflowing_sub, 32n, a, b):
160  wsub_g(1n, {==}, a, b)
161
162# ---- div, rem ----
163
164def cdiv(+a: U32, +b: U32, +z: Bool, +hz: {U32.is_zero(b) == z : Bool}, +ez: {Nat.is_eq(SG.u32_val(b), 0n) == z : Bool}) -> {SF.mval(~U32, ~SG.u32_val, F.opt(U32, z, U32.div(a, b))) == SF.keep(Bool.not(Nat.is_eq(SG.u32_val(b), 0n)), Nat.div(SG.u32_val(a), SG.u32_val(b))) : Maybe<&2, Nat>}:
165  match z:
166    case False{}:
167      %Equal.sym(Bool, Nat.is_eq(SG.u32_val(b), 0n), False{}, ez) : {SF.mval(~U32, ~SG.u32_val, F.opt(U32, False{}, U32.div(a, b))) == SF.keep(Bool.not(_), Nat.div(SG.u32_val(a), SG.u32_val(b))) : Maybe<&2, Nat>}
168      G.some_of(~U32, ~SG.u32_val, False{}, {==}, U32.div(a, b), Nat.div(SG.u32_val(a), SG.u32_val(b)), UD.div_nat(a, b, hz))
169    case True{}:
170      %Equal.sym(Bool, Nat.is_eq(SG.u32_val(b), 0n), True{}, ez) : {SF.mval(~U32, ~SG.u32_val, F.opt(U32, True{}, U32.div(a, b))) == SF.keep(Bool.not(_), Nat.div(SG.u32_val(a), SG.u32_val(b))) : Maybe<&2, Nat>}
171      {==}
172
173def checked_div(+a: U32, +b: U32) -> SF.CheckedDiv.value(~U32, ~SG.u32_val, ~F.u32_checked_div, a, b):
174  cdiv(a, b, U32.is_zero(b), {==}, Equal.sym(Bool, U32.is_zero(b), Nat.is_eq(SG.u32_val(b), 0n), LW.zero_nat(b)))
175
176def crem(+a: U32, +b: U32, +z: Bool, +hz: {U32.is_zero(b) == z : Bool}, +ez: {Nat.is_eq(SG.u32_val(b), 0n) == z : Bool}) -> {SF.mval(~U32, ~SG.u32_val, F.opt(U32, z, U32.mod(a, b))) == SF.keep(Bool.not(Nat.is_eq(SG.u32_val(b), 0n)), Nat.mod(SG.u32_val(a), SG.u32_val(b))) : Maybe<&2, Nat>}:
177  match z:
178    case False{}:
179      %Equal.sym(Bool, Nat.is_eq(SG.u32_val(b), 0n), False{}, ez) : {SF.mval(~U32, ~SG.u32_val, F.opt(U32, False{}, U32.mod(a, b))) == SF.keep(Bool.not(_), Nat.mod(SG.u32_val(a), SG.u32_val(b))) : Maybe<&2, Nat>}
180      G.some_of(~U32, ~SG.u32_val, False{}, {==}, U32.mod(a, b), Nat.mod(SG.u32_val(a), SG.u32_val(b)), UD.mod_nat(a, b, hz))
181    case True{}:
182      %Equal.sym(Bool, Nat.is_eq(SG.u32_val(b), 0n), True{}, ez) : {SF.mval(~U32, ~SG.u32_val, F.opt(U32, True{}, U32.mod(a, b))) == SF.keep(Bool.not(_), Nat.mod(SG.u32_val(a), SG.u32_val(b))) : Maybe<&2, Nat>}
183      {==}
184
185def checked_rem(+a: U32, +b: U32) -> SF.CheckedRem.value(~U32, ~SG.u32_val, ~F.u32_checked_rem, a, b):
186  crem(a, b, U32.is_zero(b), {==}, Equal.sym(Bool, U32.is_zero(b), Nat.is_eq(SG.u32_val(b), 0n), LW.zero_nat(b)))
187
188# ---- shifts: the amount masked to s mod 32 ----
189
190def am(+s: U32) -> {U32.to_nat(U32.and(s, 31)) == Nat.mod(vs(s), 32n) : Nat}:
191  Equal.trans(Nat, U32.to_nat(U32.and(s, 31)), C.low(5n, vs(s)), Nat.mod(vs(s), 32n), FB.andm(s, 5n, 31, {==}), G.low_mod(5n, vs(s), 31n, {==}))
192
193def am_small(+s: U32, +h: {Nat.is_lt(vs(s), 32n) == True{} : Bool}) -> {U32.to_nat(U32.and(s, 31)) == vs(s) : Nat}:
194  Equal.trans(Nat, U32.to_nat(U32.and(s, 31)), Nat.mod(vs(s), 32n), vs(s), am(s), R.mod_of(0n, 31n, vs(s), h))
195
196def lt32(+s: U32) -> {U32.is_lt(s, 32) == Nat.is_lt(vs(s), 32n) : Bool}:
197  U3.is_lt_nat(s, 32)
198
199def wrapping_shl(+a: U32, +s: U32) -> SF.WrappingShl.value(~U32, ~SG.u32_val, ~F.u32_wrapping_shl, 32n, a, s):
200  %Equal.sym(Nat, U32.to_nat(U32.and(s, 31)), Nat.mod(vs(s), 32n), am(s)) : {SG.u32_val(U32.mul(a, X.pow2(_))) == C.low(32n, C.shift(Nat.mod(vs(s), 32n), SG.u32_val(a))) : Nat}
201  SH.mul_p2(a, Nat.mod(vs(s), 32n), R.dm_lt(31n, vs(s)))
202
203def wrapping_shr(+a: U32, +s: U32) -> SF.WrappingShr.value(~U32, ~SG.u32_val, ~F.u32_wrapping_shr, 32n, a, s):
204  %Equal.sym(Nat, U32.to_nat(U32.and(s, 31)), Nat.mod(vs(s), 32n), am(s)) : {SG.u32_val(U32.shrn(a, _)) == C.high(Nat.mod(vs(s), 32n), SG.u32_val(a)) : Nat}
205  SHN.shrn_high(a, Nat.mod(vs(s), 32n))
206
207def overflowing_shl_value(+a: U32, +s: U32) -> SF.OverflowingShl.value(~U32, ~SG.u32_val, ~F.u32_overflowing_shl, 32n, a, s):
208  wrapping_shl(a, s)
209
210def overflowing_shr_value(+a: U32, +s: U32) -> SF.OverflowingShr.value(~U32, ~SG.u32_val, ~F.u32_overflowing_shr, 32n, a, s):
211  wrapping_shr(a, s)
212
213def overflowing_shl_flag(+a: U32, +s: U32) -> SF.OverflowingShl.flag(~U32, ~F.u32_overflowing_shl, a, s, 32n):
214  G.bnot_eq(U32.is_lt(s, 32), Nat.is_lt(vs(s), 32n), lt32(s))
215
216def overflowing_shr_flag(+a: U32, +s: U32) -> SF.OverflowingShr.flag(~U32, ~F.u32_overflowing_shr, a, s, 32n):
217  G.bnot_eq(U32.is_lt(s, 32), Nat.is_lt(vs(s), 32n), lt32(s))
218
219def cshl(+a: U32, +s: U32, +ok: Bool, +hok: {Nat.is_lt(vs(s), 32n) == ok : Bool}) -> {SF.mval(~U32, ~SG.u32_val, F.opt(U32, Bool.not(U32.is_lt(s, 32)), U32.mul(a, X.pow2(U32.to_nat(U32.and(s, 31)))))) == SF.keep(ok, C.low(32n, C.shift(vs(s), SG.u32_val(a)))) : Maybe<&2, Nat>}:
220  match ok:
221    case True{}:
222      +hb = Equal.trans(Bool, U32.is_lt(s, 32), Nat.is_lt(vs(s), 32n), True{}, lt32(s), hok)
223      +ev = Equal.trans(Nat, SG.u32_val(U32.mul(a, X.pow2(U32.to_nat(U32.and(s, 31))))), SG.u32_val(U32.mul(a, X.pow2(vs(s)))), C.low(32n, C.shift(vs(s), SG.u32_val(a))), Equal.cong(Nat, Nat, t => SG.u32_val(U32.mul(a, X.pow2(t))), U32.to_nat(U32.and(s, 31)), vs(s), am_small(s, hok)), SH.mul_p2(a, vs(s), hok))
224      G.some_of(~U32, ~SG.u32_val, Bool.not(U32.is_lt(s, 32)), G.bnot_eq(U32.is_lt(s, 32), True{}, hb), U32.mul(a, X.pow2(U32.to_nat(U32.and(s, 31)))), C.low(32n, C.shift(vs(s), SG.u32_val(a))), ev)
225    case False{}:
226      +hb = Equal.trans(Bool, U32.is_lt(s, 32), Nat.is_lt(vs(s), 32n), False{}, lt32(s), hok)
227      G.none_of(~U32, ~SG.u32_val, Bool.not(U32.is_lt(s, 32)), G.bnot_eq(U32.is_lt(s, 32), False{}, hb), U32.mul(a, X.pow2(U32.to_nat(U32.and(s, 31)))))
228
229def checked_shl(+a: U32, +s: U32) -> SF.CheckedShl.value(~U32, ~SG.u32_val, ~F.u32_checked_shl, 32n, a, s):
230  cshl(a, s, Nat.is_lt(vs(s), 32n), {==})
231
232def cshr(+a: U32, +s: U32, +ok: Bool, +hok: {Nat.is_lt(vs(s), 32n) == ok : Bool}) -> {SF.mval(~U32, ~SG.u32_val, F.opt(U32, Bool.not(U32.is_lt(s, 32)), U32.shrn(a, U32.to_nat(U32.and(s, 31))))) == SF.keep(ok, C.high(vs(s), SG.u32_val(a))) : Maybe<&2, Nat>}:
233  match ok:
234    case True{}:
235      +hb = Equal.trans(Bool, U32.is_lt(s, 32), Nat.is_lt(vs(s), 32n), True{}, lt32(s), hok)
236      +ev = Equal.trans(Nat, SG.u32_val(U32.shrn(a, U32.to_nat(U32.and(s, 31)))), SG.u32_val(U32.shrn(a, vs(s))), C.high(vs(s), SG.u32_val(a)), Equal.cong(Nat, Nat, t => SG.u32_val(U32.shrn(a, t)), U32.to_nat(U32.and(s, 31)), vs(s), am_small(s, hok)), SHN.shrn_high(a, vs(s)))
237      G.some_of(~U32, ~SG.u32_val, Bool.not(U32.is_lt(s, 32)), G.bnot_eq(U32.is_lt(s, 32), True{}, hb), U32.shrn(a, U32.to_nat(U32.and(s, 31))), C.high(vs(s), SG.u32_val(a)), ev)
238    case False{}:
239      +hb = Equal.trans(Bool, U32.is_lt(s, 32), Nat.is_lt(vs(s), 32n), False{}, lt32(s), hok)
240      G.none_of(~U32, ~SG.u32_val, Bool.not(U32.is_lt(s, 32)), G.bnot_eq(U32.is_lt(s, 32), False{}, hb), U32.shrn(a, U32.to_nat(U32.and(s, 31))))
241
242def checked_shr(+a: U32, +s: U32) -> SF.CheckedShr.value(~U32, ~SG.u32_val, ~F.u32_checked_shr, 32n, a, s):
243  cshr(a, s, Nat.is_lt(vs(s), 32n), {==})
244
245# ---- pow through the generic checked pow ----
246
247def pw(+a: U32, +e: U32) -> Nat:
248  Nat.pow(SG.u32_val(a), vs(e))
249
250def gpow(+a: U32, +e: U32) -> Result<&2, &2, NM.NumError, U32>:
251  GN.pow(~U32, ~I.u32_op, ~I.u32_is, a, vs(e))
252
253def cpow(+a: U32, +e: U32, +ok: Bool, +hok: {C.fits(32n, pw(a, e)) == ok : Bool}) -> {SF.mval(~U32, ~SG.u32_val, F.res_opt(U32, gpow(a, e))) == SF.keep(ok, pw(a, e)) : Maybe<&2, Nat>}:
254  match ok:
255    case True{}:
256      %Equal.sym(Result<&2, &2, NM.NumError, U32>, gpow(a, e), SG.checked(~U32, ~SG.u32_of, 32n, pw(a, e)), UI.pow_checked(a, vs(e))) : {SF.mval(~U32, ~SG.u32_val, F.res_opt(U32, _)) == Some{pw(a, e)} : Maybe<&2, Nat>}
257      %Equal.sym(Bool, C.fits(32n, pw(a, e)), True{}, hok) : {SF.mval(~U32, ~SG.u32_val, F.res_opt(U32, SG.checked_pick(~U32, ~SG.u32_of, pw(a, e), _))) == Some{pw(a, e)} : Maybe<&2, Nat>}
258      Equal.cong(Nat, Maybe<&2, Nat>, t => Some{t}, SG.u32_val(SG.u32_of(pw(a, e))), pw(a, e), LW.vo(pw(a, e), hok))
259    case False{}:
260      %Equal.sym(Result<&2, &2, NM.NumError, U32>, gpow(a, e), SG.checked(~U32, ~SG.u32_of, 32n, pw(a, e)), UI.pow_checked(a, vs(e))) : {SF.mval(~U32, ~SG.u32_val, F.res_opt(U32, _)) == None{} : Maybe<&2, Nat>}
261      %Equal.sym(Bool, C.fits(32n, pw(a, e)), False{}, hok) : {SF.mval(~U32, ~SG.u32_val, F.res_opt(U32, SG.checked_pick(~U32, ~SG.u32_of, pw(a, e), _))) == None{} : Maybe<&2, Nat>}
262      {==}
263
264def checked_pow(+a: U32, +e: U32) -> SF.CheckedPow.value(~U32, ~SG.u32_val, ~F.u32_checked_pow, 32n, a, e):
265  cpow(a, e, C.fits(32n, pw(a, e)), {==})
266
267def spow(+top: U32, +ht: {Bool.and(C.fits(32n, SG.u32_val(top)), Bool.not(C.fits(32n, 1n+SG.u32_val(top)))) == True{} : Bool}, +a: U32, +e: U32, +ok: Bool, +hok: {C.fits(32n, pw(a, e)) == ok : Bool}) -> {SF.saturated(32n, pw(a, e), SG.u32_val(F.or_top(U32, top, F.res_opt(U32, gpow(a, e)))), ok) == True{} : Bool}:
268  match ok:
269    case True{}:
270      %Equal.sym(Result<&2, &2, NM.NumError, U32>, gpow(a, e), SG.checked(~U32, ~SG.u32_of, 32n, pw(a, e)), UI.pow_checked(a, vs(e))) : {SF.saturated(32n, pw(a, e), SG.u32_val(F.or_top(U32, top, F.res_opt(U32, _))), True{}) == True{} : Bool}
271      %Equal.sym(Bool, C.fits(32n, pw(a, e)), True{}, hok) : {SF.saturated(32n, pw(a, e), SG.u32_val(F.or_top(U32, top, F.res_opt(U32, SG.checked_pick(~U32, ~SG.u32_of, pw(a, e), _)))), True{}) == True{} : Bool}
272      %Equal.sym(Nat, SG.u32_val(SG.u32_of(pw(a, e))), pw(a, e), LW.vo(pw(a, e), hok)) : {Nat.is_eq(_, pw(a, e)) == True{} : Bool}
273      N.is_eq_refl(pw(a, e))
274    case False{}:
275      %Equal.sym(Result<&2, &2, NM.NumError, U32>, gpow(a, e), SG.checked(~U32, ~SG.u32_of, 32n, pw(a, e)), UI.pow_checked(a, vs(e))) : {SF.saturated(32n, pw(a, e), SG.u32_val(F.or_top(U32, top, F.res_opt(U32, _))), False{}) == True{} : Bool}
276      %Equal.sym(Bool, C.fits(32n, pw(a, e)), False{}, hok) : {SF.saturated(32n, pw(a, e), SG.u32_val(F.or_top(U32, top, F.res_opt(U32, SG.checked_pick(~U32, ~SG.u32_of, pw(a, e), _)))), False{}) == True{} : Bool}
277      ht
278
279def saturating_pow(+a: U32, +e: U32) -> SF.SaturatingPow.value(~U32, ~SG.u32_val, ~F.u32_saturating_pow, 32n, a, e):
280  spow(F.u32_max(), top(1n, {==}), a, e, C.fits(32n, pw(a, e)), {==})
281
282def overflowing_pow_flag(+a: U32, +e: U32) -> SF.OverflowingPow.flag(~U32, ~SG.u32_val, ~F.u32_overflowing_pow, 32n, a, e):
283  G.bad_res(~U32, ~SG.u32_of, 32n, pw(a, e), gpow(a, e), UI.pow_checked(a, vs(e)), C.fits(32n, pw(a, e)), {==})
284
285# ---- wrapping pow: right-to-left binary exponentiation mod 2^32 ----
286
287def lt_m(+mp: Nat, +hp: {C.pow2(32n) == 1n+mp : Nat}, +x: U32) -> {Nat.is_lt(SG.u32_val(x), 1n+mp) == True{} : Bool}:
288  Equal.trans(Bool, Nat.is_lt(SG.u32_val(x), 1n+mp), Nat.is_lt(SG.u32_val(x), C.pow2(32n)), True{}, Equal.cong(Nat, Bool, t => Nat.is_lt(SG.u32_val(x), t), 1n+mp, C.pow2(32n), Equal.sym(Nat, C.pow2(32n), 1n+mp, hp)), WW.lt_of_fits(32n, SG.u32_val(x), LW.vb(x)))
289
290def mul_m(+mp: Nat, +hp: {C.pow2(32n) == 1n+mp : Nat}, +x: U32, +y: U32) -> {SG.u32_val(U32.mul(x, y)) == Nat.mod(Nat.mul(SG.u32_val(x), SG.u32_val(y)), 1n+mp) : Nat}:
291  Equal.trans(Nat, SG.u32_val(U32.mul(x, y)), C.low(32n, Nat.mul(SG.u32_val(x), SG.u32_val(y))), Nat.mod(Nat.mul(SG.u32_val(x), SG.u32_val(y)), 1n+mp), mul_low(x, y), G.low_mod(32n, Nat.mul(SG.u32_val(x), SG.u32_val(y)), mp, hp))
292
293def wp_base(+mp: Nat, +hp: {C.pow2(32n) == 1n+mp : Nat}, +e: U32, +b: U32, +acc: U32, +h0: {vs(e) == 0n : Nat}) -> {SG.u32_val(acc) == Nat.mod(Nat.mul(SG.u32_val(acc), Nat.pow(SG.u32_val(b), vs(e))), 1n+mp) : Nat}:
294  %Equal.sym(Nat, vs(e), 0n, h0) : {SG.u32_val(acc) == Nat.mod(Nat.mul(SG.u32_val(acc), Nat.pow(SG.u32_val(b), _)), 1n+mp) : Nat}
295  %Equal.sym(Nat, Nat.mul(SG.u32_val(acc), 1n), SG.u32_val(acc), NA.mul_one(SG.u32_val(acc))) : {SG.u32_val(acc) == Nat.mod(_, 1n+mp) : Nat}
296  Equal.sym(Nat, Nat.mod(SG.u32_val(acc), 1n+mp), SG.u32_val(acc), R.mod_of(0n, mp, SG.u32_val(acc), lt_m(mp, hp, acc)))
297
298def wp_odd(+mp: Nat, +hp: {C.pow2(32n) == 1n+mp : Nat}, +e: U32, +b: U32, +acc: U32, +r: Nat, +hodd: {I.u32_odd(e) == Nat.is_eq(r, 1n) : Bool}, +hr: {Nat.is_lt(r, 2n) == True{} : Bool}) -> {SG.u32_val(F.pick(U32, I.u32_odd(e), U32.mul(acc, b), acc)) == M.pow_mod_odd(1n+mp, r, SG.u32_val(b), SG.u32_val(acc)) : Nat}:
299  match r:
300    case 0n:
301      %Equal.sym(Bool, I.u32_odd(e), False{}, hodd) : {SG.u32_val(F.pick(U32, _, U32.mul(acc, b), acc)) == SG.u32_val(acc) : Nat}
302      {==}
303    case 1n:
304      %Equal.sym(Bool, I.u32_odd(e), True{}, hodd) : {SG.u32_val(F.pick(U32, _, U32.mul(acc, b), acc)) == Nat.mod(Nat.mul(SG.u32_val(acc), SG.u32_val(b)), 1n+mp) : Nat}
305      mul_m(mp, hp, acc, b)
306    case 2n+ +q:
307      Empty.absurd({SG.u32_val(F.pick(U32, I.u32_odd(e), U32.mul(acc, b), acc)) == M.pow_mod_odd(1n+mp, 2n+q, SG.u32_val(b), SG.u32_val(acc)) : Nat}, N.lt_zero_absurd(q, hr))
308
309def half_e(+e: U32) -> {vs(U32.shr(e)) == Nat.div(vs(e), 2n) : Nat}:
310  Equal.trans(Nat, vs(U32.shr(e)), C.half(vs(e)), Nat.div(vs(e), 2n), SHN.shrn_high(e, 1n), WA.half_div(vs(e)))
311
312def wp_go(fuel: Nat, +mp: Nat, +hp: {C.pow2(32n) == 1n+mp : Nat}, +e: U32, +b: U32, +acc: U32, +z: Bool, +hz: {U32.is_zero(e) == z : Bool}, +he: {Nat.is_lt(vs(e), C.pow2(fuel)) == True{} : Bool}) -> {SG.u32_val(F.u32_wpow(fuel, e, b, acc, z)) == Nat.mod(Nat.mul(SG.u32_val(acc), Nat.pow(SG.u32_val(b), vs(e))), 1n+mp) : Nat}:
313  match fuel z:
314    case 0n _:
315      wp_base(mp, hp, e, b, acc, G.lt1(vs(e), he))
316    case 1n+f True{}:
317      wp_base(mp, hp, e, b, acc, N.eq_from_is_eq(vs(e), 0n, Equal.trans(Bool, Nat.is_eq(vs(e), 0n), U32.is_zero(e), True{}, Equal.sym(Bool, U32.is_zero(e), Nat.is_eq(vs(e), 0n), LW.zero_nat(e)), hz)))
318    case 1n+ +f False{}:
319      +ve = vs(e)
320      +e2 = Nat.div(ve, 2n)
321      +bit = Nat.mod(ve, 2n)
322      +m = {1n+mp : Nat}
323      +acc2 = F.pick(U32, I.u32_odd(e), U32.mul(acc, b), acc)
324      +he2 = Equal.trans(Bool, Nat.is_lt(vs(U32.shr(e)), C.pow2(f)), Nat.is_lt(C.half(ve), C.pow2(f)), True{}, Equal.cong(Nat, Bool, t => Nat.is_lt(t, C.pow2(f)), vs(U32.shr(e)), C.half(ve), SHN.shrn_high(e, 1n)), Equal.trans(Bool, Nat.is_lt(C.half(ve), C.pow2(f)), Nat.is_lt(ve, Nat.double(C.pow2(f))), True{}, WW.lt_half(ve, C.pow2(f)), he))
325      +ih = wp_go(f, mp, hp, U32.shr(e), U32.mul(b, b), acc2, U32.is_zero(U32.shr(e)), {==}, he2)
326      +ea = wp_odd(mp, hp, e, b, acc, bit, LW.tests_odd(e), B.half_rem(ve))
327      +eb = mul_m(mp, hp, b, b)
328      +x1 = Equal.cong(Nat, Nat, t => Nat.mod(Nat.mul(t, Nat.pow(SG.u32_val(U32.mul(b, b)), vs(U32.shr(e)))), m), SG.u32_val(acc2), M.pow_mod_odd(m, bit, SG.u32_val(b), SG.u32_val(acc)), ea)
329      +x2 = Equal.cong(Nat, Nat, t => Nat.mod(Nat.mul(M.pow_mod_odd(m, bit, SG.u32_val(b), SG.u32_val(acc)), Nat.pow(t, vs(U32.shr(e)))), m), SG.u32_val(U32.mul(b, b)), Nat.mod(Nat.mul(SG.u32_val(b), SG.u32_val(b)), m), eb)
330      +x3 = Equal.cong(Nat, Nat, t => Nat.mod(Nat.mul(M.pow_mod_odd(m, bit, SG.u32_val(b), SG.u32_val(acc)), Nat.pow(Nat.mod(Nat.mul(SG.u32_val(b), SG.u32_val(b)), m), t)), m), vs(U32.shr(e)), e2, half_e(e))
331      +x4 = MP.pm_bit(mp, e2, bit, B.half_rem(ve), SG.u32_val(b), SG.u32_val(acc))
332      +x5 = Equal.cong(Nat, Nat, t => Nat.mod(Nat.mul(SG.u32_val(acc), Nat.pow(SG.u32_val(b), t)), m), Nat.add(Nat.double(e2), bit), ve, Equal.sym(Nat, ve, Nat.add(Nat.double(e2), bit), B.half_eq(ve)))
333      +L0 = Nat.mod(Nat.mul(SG.u32_val(acc2), Nat.pow(SG.u32_val(U32.mul(b, b)), vs(U32.shr(e)))), m)
334      +L1 = Nat.mod(Nat.mul(M.pow_mod_odd(m, bit, SG.u32_val(b), SG.u32_val(acc)), Nat.pow(SG.u32_val(U32.mul(b, b)), vs(U32.shr(e)))), m)
335      +L2 = Nat.mod(Nat.mul(M.pow_mod_odd(m, bit, SG.u32_val(b), SG.u32_val(acc)), Nat.pow(Nat.mod(Nat.mul(SG.u32_val(b), SG.u32_val(b)), m), vs(U32.shr(e)))), m)
336      +L3 = Nat.mod(Nat.mul(M.pow_mod_odd(m, bit, SG.u32_val(b), SG.u32_val(acc)), Nat.pow(Nat.mod(Nat.mul(SG.u32_val(b), SG.u32_val(b)), m), e2)), m)
337      +L4 = Nat.mod(Nat.mul(SG.u32_val(acc), Nat.pow(SG.u32_val(b), Nat.add(Nat.double(e2), bit))), m)
338      +L5 = Nat.mod(Nat.mul(SG.u32_val(acc), Nat.pow(SG.u32_val(b), ve)), m)
339      Equal.trans(Nat, SG.u32_val(F.u32_wpow(f, U32.shr(e), U32.mul(b, b), acc2, U32.is_zero(U32.shr(e)))), L0, L5, ih, Equal.trans(Nat, L0, L1, L5, x1, Equal.trans(Nat, L1, L2, L5, x2, Equal.trans(Nat, L2, L3, L5, x3, Equal.trans(Nat, L3, L4, L5, x4, x5)))))
340
341def wp_top(+mp: Nat, +hp: {C.pow2(32n) == 1n+mp : Nat}, +a: U32, +e: U32) -> {SG.u32_val(F.u32_wrapping_pow(a, e)) == C.low(32n, pw(a, e)) : Nat}:
342  +ih = wp_go(32n, mp, hp, e, a, 1, U32.is_zero(e), {==}, WW.lt_of_fits(32n, vs(e), LW.vb(e)))
343  +e1 = Equal.cong(Nat, Nat, t => Nat.mod(t, 1n+mp), Nat.mul(1n, pw(a, e)), pw(a, e), AR.one_mul(pw(a, e)))
344  Equal.trans(Nat, SG.u32_val(F.u32_wrapping_pow(a, e)), Nat.mod(Nat.mul(1n, pw(a, e)), 1n+mp), C.low(32n, pw(a, e)), ih, Equal.trans(Nat, Nat.mod(Nat.mul(1n, pw(a, e)), 1n+mp), Nat.mod(pw(a, e), 1n+mp), C.low(32n, pw(a, e)), e1, Equal.sym(Nat, C.low(32n, pw(a, e)), Nat.mod(pw(a, e), 1n+mp), G.low_mod(32n, pw(a, e), mp, hp))))
345
346def wrapping_pow(+a: U32, +e: U32) -> SF.WrappingPow.value(~U32, ~SG.u32_val, ~F.u32_wrapping_pow, 32n, a, e):
347  wp_top(Nat.sub(C.pow2(32n), 1n), SH.pow2_eq(32n), a, e)
348
349def overflowing_pow_value(+a: U32, +e: U32) -> SF.OverflowingPow.value(~U32, ~SG.u32_val, ~F.u32_overflowing_pow, 32n, a, e):
350  wrapping_pow(a, e)