~/jendhub

proofs/math/typed/fix64.bend

bend-collections-laws-math@1.0.0.0 · 368 lines · 61 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/u64.bend as WU
7import bend-collections-laws-math@1.0.0.0/src/math/fixed.bend as F
8import bend-collections-laws-math@1.0.0.0/src/math/generic.bend as GN
9import bend-collections-laws-math@1.0.0.0/src/math/instances.bend as I
10import bend-collections-laws-math@1.0.0.0/src/math/num.bend as NM
11import bend-collections-laws-math@1.0.0.0/src/math/natural.bend as M
12import bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend as N
13import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend as NA
14import bend-collections-laws-math@1.0.0.0/proofs/math/natural/modpow.bend as MP
15import bend-collections-laws-math@1.0.0.0/proofs/math/natural/bits.bend as B
16import bend-collections-laws-math@1.0.0.0/proofs/math/typed/u32laws.bend as LW
17import bend-collections-laws-math@1.0.0.0/proofs/math/typed/shrn.bend as SHN
18import bend-collections-laws-math@1.0.0.0/proofs/lib/u32.bend as U3
19import bend-collections-laws-math@1.0.0.0/proofs/lib/arith.bend as AR
20import bend-collections-laws-math@1.0.0.0/proofs/math/natural/arith.bend as R
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/typed/w64sh.bend as SH
24import bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64dmtop.bend as DT
25import bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64dmrem.bend as DR
26import bend-collections-laws-math@1.0.0.0/proofs/math/typed/u64laws.bend as LV
27import bend-collections-laws-math@1.0.0.0/proofs/math/typed/u64int.bend as UI
28import bend-collections-laws-math@1.0.0.0/proofs/math/typed/u64mont.bend as MT
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
31import bend-collections-laws-math@1.0.0.0/proofs/lib/word.bend as WD
32import bend-collections-laws-math@1.0.0.0/proofs/lib/logic.bend as L
33
34# The U64 clauses of spec/math/fixed.bend (Rust's u64 checked_*, wrapping_*,
35# saturating_*, overflowing_* families) from the proved two-limb clauses of
36# spec/math/w64.bend (proofs/math/typed/w64add.bend, w64sh.bend,
37# w64dmtop.bend, w64dmrem.bend) and the generic pow of u64int.bend, as
38# HACL*'s Hacl.Spec.Bignum proves each word operation through its value.
39
40def vs(+s: U32) -> Nat:
41  U32.to_nat(s)
42
43# ---- the largest value ----
44
45def zero_add(+x: Nat) -> {Nat.add(0n, x) == x : Nat}:
46  Equal.trans(Nat, Nat.add(0n, x), Nat.add(x, 0n), x, N.add_comm(0n, x), N.add_zero(x))
47
48# The largest value 2^64 - 1 is built with its limbs abstract (w, the
49# all-ones U32) and 1 kept as one: the checker must never unfold 2^64, and
50# closed 64-bit values are only ever compared as U64s.
51
52def top1w(+one: Nat, +h1: {one == 1n : Nat}, +w: U32, +pw: {w == U32{WD.mask(32n, 32n)} : U32}) -> {1n+SG.u64_val(WU.U64{w, w}) == C.shift(64n, one) : Nat}:
53  MT.ones_v(one, h1, w, pw)
54
55def top1(+one: Nat, +h1: {one == 1n : Nat}) -> {1n+SG.u64_val(F.u64_max()) == C.shift(64n, one) : Nat}:
56  L.subst(WU.U64, t => {1n+SG.u64_val(t) == C.shift(64n, one) : Nat}, WU.U64{4294967295, 4294967295}, F.u64_max(), {==}, top1w(one, h1, 4294967295, {==}))
57
58def topw(+one: Nat, +h1: {one == 1n : Nat}, +w: U32, +pw: {w == U32{WD.mask(32n, 32n)} : U32}) -> {Bool.and(C.fits(64n, SG.u64_val(WU.U64{w, w})), Bool.not(C.fits(64n, 1n+SG.u64_val(WU.U64{w, w})))) == True{} : Bool}:
59  +m = {WU.U64{w, w} : WU.U64}
60  +S = C.shift(64n, one)
61  +e1 = Equal.cong(Nat, Bool, t => C.fits(64n, t), 1n+SG.u64_val(m), S, top1w(one, h1, w, pw))
62  +e2 = Equal.cong(Nat, Bool, t => C.fits(64n, t), S, Nat.add(0n, S), Equal.sym(Nat, Nat.add(0n, S), S, zero_add(S)))
63  G.top_ok(64n, SG.u64_val(m), LV.vb(m), Equal.trans(Bool, C.fits(64n, 1n+SG.u64_val(m)), C.fits(64n, S), False{}, e1, Equal.trans(Bool, C.fits(64n, S), C.fits(64n, Nat.add(0n, S)), False{}, e2, WW.unfit_one(64n, one, h1, 0n))))
64
65def top(+one: Nat, +h1: {one == 1n : Nat}) -> {Bool.and(C.fits(64n, SG.u64_val(F.u64_max())), Bool.not(C.fits(64n, 1n+SG.u64_val(F.u64_max())))) == True{} : Bool}:
66  L.subst(WU.U64, t => {Bool.and(C.fits(64n, SG.u64_val(t)), Bool.not(C.fits(64n, 1n+SG.u64_val(t)))) == True{} : Bool}, WU.U64{4294967295, 4294967295}, F.u64_max(), {==}, topw(one, h1, 4294967295, {==}))
67
68# ---- add, mul ----
69
70def checked_add(+a: WU.U64, +b: WU.U64) -> SF.CheckedAdd.value(~WU.U64, ~SG.u64_val, ~F.u64_checked_add, 64n, a, b):
71  G.chk_fit(~WU.U64, ~SG.u64_val, 64n, Nat.add(SG.u64_val(a), SG.u64_val(b)), X.add(a, b), X.add_over(a, b), WA.add_over_value(a, b), WA.add_value(a, b), C.fits(64n, Nat.add(SG.u64_val(a), SG.u64_val(b))), {==})
72
73def wrapping_add(+a: WU.U64, +b: WU.U64) -> SF.WrappingAdd.value(~WU.U64, ~SG.u64_val, ~F.u64_wrapping_add, 64n, a, b):
74  WA.add_value(a, b)
75
76def saturating_add(+a: WU.U64, +b: WU.U64) -> SF.SaturatingAdd.value(~WU.U64, ~SG.u64_val, ~F.u64_saturating_add, 64n, a, b):
77  G.sat_fit(~WU.U64, ~SG.u64_val, 64n, Nat.add(SG.u64_val(a), SG.u64_val(b)), X.add(a, b), F.u64_max(), X.add_over(a, b), WA.add_over_value(a, b), WA.add_value(a, b), top(1n, {==}), C.fits(64n, Nat.add(SG.u64_val(a), SG.u64_val(b))), {==})
78
79def overflowing_add_value(+a: WU.U64, +b: WU.U64) -> SF.OverflowingAdd.value(~WU.U64, ~SG.u64_val, ~F.u64_overflowing_add, 64n, a, b):
80  WA.add_value(a, b)
81
82def overflowing_add_flag(+a: WU.U64, +b: WU.U64) -> SF.OverflowingAdd.flag(~WU.U64, ~SG.u64_val, ~F.u64_overflowing_add, 64n, a, b):
83  WA.add_over_value(a, b)
84
85def checked_mul(+a: WU.U64, +b: WU.U64) -> SF.CheckedMul.value(~WU.U64, ~SG.u64_val, ~F.u64_checked_mul, 64n, a, b):
86  G.chk_fit(~WU.U64, ~SG.u64_val, 64n, Nat.mul(SG.u64_val(a), SG.u64_val(b)), X.mul(a, b), X.mul_over(a, b), WA.mul_over_value(a, b), WA.mul_value(a, b), C.fits(64n, Nat.mul(SG.u64_val(a), SG.u64_val(b))), {==})
87
88def wrapping_mul(+a: WU.U64, +b: WU.U64) -> SF.WrappingMul.value(~WU.U64, ~SG.u64_val, ~F.u64_wrapping_mul, 64n, a, b):
89  WA.mul_value(a, b)
90
91def saturating_mul(+a: WU.U64, +b: WU.U64) -> SF.SaturatingMul.value(~WU.U64, ~SG.u64_val, ~F.u64_saturating_mul, 64n, a, b):
92  G.sat_fit(~WU.U64, ~SG.u64_val, 64n, Nat.mul(SG.u64_val(a), SG.u64_val(b)), X.mul(a, b), F.u64_max(), X.mul_over(a, b), WA.mul_over_value(a, b), WA.mul_value(a, b), top(1n, {==}), C.fits(64n, Nat.mul(SG.u64_val(a), SG.u64_val(b))), {==})
93
94def overflowing_mul_value(+a: WU.U64, +b: WU.U64) -> SF.OverflowingMul.value(~WU.U64, ~SG.u64_val, ~F.u64_overflowing_mul, 64n, a, b):
95  WA.mul_value(a, b)
96
97def overflowing_mul_flag(+a: WU.U64, +b: WU.U64) -> SF.OverflowingMul.flag(~WU.U64, ~SG.u64_val, ~F.u64_overflowing_mul, 64n, a, b):
98  WA.mul_over_value(a, b)
99
100# ---- sub ----
101
102def csub(+a: WU.U64, +b: WU.U64, +ok: Bool, +hok: {Nat.is_le(SG.u64_val(b), SG.u64_val(a)) == ok : Bool}) -> {SF.mval(~WU.U64, ~SG.u64_val, F.opt(WU.U64, X.lt(a, b), X.sub(a, b))) == SF.keep(ok, Nat.sub(SG.u64_val(a), SG.u64_val(b))) : Maybe<&2, Nat>}:
103  match ok:
104    case True{}:
105      G.some_of(~WU.U64, ~SG.u64_val, X.lt(a, b), Equal.trans(Bool, X.lt(a, b), Nat.is_lt(SG.u64_val(a), SG.u64_val(b)), False{}, WA.lt_value(a, b), N.le_not_lt(SG.u64_val(a), SG.u64_val(b), hok)), X.sub(a, b), Nat.sub(SG.u64_val(a), SG.u64_val(b)), WA.sub_value(a, b, hok))
106    case False{}:
107      G.none_of(~WU.U64, ~SG.u64_val, X.lt(a, b), Equal.trans(Bool, X.lt(a, b), Nat.is_lt(SG.u64_val(a), SG.u64_val(b)), True{}, WA.lt_value(a, b), N.not_le_lt(SG.u64_val(b), SG.u64_val(a), hok)), X.sub(a, b))
108
109def checked_sub(+a: WU.U64, +b: WU.U64) -> SF.CheckedSub.value(~WU.U64, ~SG.u64_val, ~F.u64_checked_sub, a, b):
110  csub(a, b, Nat.is_le(SG.u64_val(b), SG.u64_val(a)), {==})
111
112def sub_big(+n: Nat, +d: Nat, +h: {Nat.is_le(n, d) == True{} : Bool}) -> {Nat.sub(n, d) == 0n : Nat}:
113  match n d:
114    case 0n _:
115      R.zsub(d)
116    case 1n+np 0n:
117      Empty.absurd({Nat.sub(1n+np, 0n) == 0n : Nat}, L.false_true(h))
118    case 1n+ +np 1n+ +dp:
119      sub_big(np, dp, h)
120
121def ssub(+a: WU.U64, +b: WU.U64, +c: Bool, +hn: {Nat.is_lt(SG.u64_val(a), SG.u64_val(b)) == c : Bool}) -> {SG.u64_val(F.pick(WU.U64, c, F.u64_zero(), X.sub(a, b))) == Nat.sub(SG.u64_val(a), SG.u64_val(b)) : Nat}:
122  match c:
123    case True{}:
124      Equal.sym(Nat, Nat.sub(SG.u64_val(a), SG.u64_val(b)), 0n, sub_big(SG.u64_val(a), SG.u64_val(b), N.lt_le(SG.u64_val(a), SG.u64_val(b), hn)))
125    case False{}:
126      WA.sub_value(a, b, N.not_lt_le(SG.u64_val(a), SG.u64_val(b), hn))
127
128def saturating_sub(+a: WU.U64, +b: WU.U64) -> SF.SaturatingSub.value(~WU.U64, ~SG.u64_val, ~F.u64_saturating_sub, a, b):
129  ssub(a, b, X.lt(a, b), Equal.sym(Bool, X.lt(a, b), Nat.is_lt(SG.u64_val(a), SG.u64_val(b)), WA.lt_value(a, b)))
130
131def overflowing_sub_flag(+a: WU.U64, +b: WU.U64) -> SF.OverflowingSub.flag(~WU.U64, ~SG.u64_val, ~F.u64_overflowing_sub, a, b):
132  WA.lt_value(a, b)
133
134# ---- div, rem ----
135
136def cdiv(+a: WU.U64, +b: WU.U64, +z: Bool, +hz: {X.is_zero(b) == z : Bool}) -> {SF.mval(~WU.U64, ~SG.u64_val, F.u64_cdiv(z, a, b)) == SF.keep(Bool.not(Nat.is_eq(SG.u64_val(b), 0n)), Nat.div(SG.u64_val(a), SG.u64_val(b))) : Maybe<&2, Nat>}:
137  match z:
138    case False{}:
139      +ez = Equal.trans(Bool, Nat.is_eq(SG.u64_val(b), 0n), X.is_zero(b), z, Equal.sym(Bool, X.is_zero(b), Nat.is_eq(SG.u64_val(b), 0n), WA.is_zero_value(b)), hz)
140      %Equal.sym(Bool, Nat.is_eq(SG.u64_val(b), 0n), False{}, ez) : {SF.mval(~WU.U64, ~SG.u64_val, F.u64_cdiv(False{}, a, b)) == SF.keep(Bool.not(_), Nat.div(SG.u64_val(a), SG.u64_val(b))) : Maybe<&2, Nat>}
141      Equal.cong(Nat, Maybe<&2, Nat>, t => Some{t}, SG.u64_val(X.quot(a, b)), Nat.div(SG.u64_val(a), SG.u64_val(b)), DT.divmod_quot(a, b, hz))
142    case True{}:
143      +ez = Equal.trans(Bool, Nat.is_eq(SG.u64_val(b), 0n), X.is_zero(b), z, Equal.sym(Bool, X.is_zero(b), Nat.is_eq(SG.u64_val(b), 0n), WA.is_zero_value(b)), hz)
144      %Equal.sym(Bool, Nat.is_eq(SG.u64_val(b), 0n), True{}, ez) : {SF.mval(~WU.U64, ~SG.u64_val, F.u64_cdiv(True{}, a, b)) == SF.keep(Bool.not(_), Nat.div(SG.u64_val(a), SG.u64_val(b))) : Maybe<&2, Nat>}
145      {==}
146
147def checked_div(+a: WU.U64, +b: WU.U64) -> SF.CheckedDiv.value(~WU.U64, ~SG.u64_val, ~F.u64_checked_div, a, b):
148  cdiv(a, b, X.is_zero(b), {==})
149
150def crem(+a: WU.U64, +b: WU.U64, +z: Bool, +hz: {X.is_zero(b) == z : Bool}) -> {SF.mval(~WU.U64, ~SG.u64_val, F.u64_crem(z, a, b)) == SF.keep(Bool.not(Nat.is_eq(SG.u64_val(b), 0n)), Nat.mod(SG.u64_val(a), SG.u64_val(b))) : Maybe<&2, Nat>}:
151  match z:
152    case False{}:
153      +ez = Equal.trans(Bool, Nat.is_eq(SG.u64_val(b), 0n), X.is_zero(b), z, Equal.sym(Bool, X.is_zero(b), Nat.is_eq(SG.u64_val(b), 0n), WA.is_zero_value(b)), hz)
154      %Equal.sym(Bool, Nat.is_eq(SG.u64_val(b), 0n), False{}, ez) : {SF.mval(~WU.U64, ~SG.u64_val, F.u64_crem(False{}, a, b)) == SF.keep(Bool.not(_), Nat.mod(SG.u64_val(a), SG.u64_val(b))) : Maybe<&2, Nat>}
155      Equal.cong(Nat, Maybe<&2, Nat>, t => Some{t}, SG.u64_val(X.rem(a, b)), Nat.mod(SG.u64_val(a), SG.u64_val(b)), DR.divmod_rem(a, b, hz))
156    case True{}:
157      +ez = Equal.trans(Bool, Nat.is_eq(SG.u64_val(b), 0n), X.is_zero(b), z, Equal.sym(Bool, X.is_zero(b), Nat.is_eq(SG.u64_val(b), 0n), WA.is_zero_value(b)), hz)
158      %Equal.sym(Bool, Nat.is_eq(SG.u64_val(b), 0n), True{}, ez) : {SF.mval(~WU.U64, ~SG.u64_val, F.u64_crem(True{}, a, b)) == SF.keep(Bool.not(_), Nat.mod(SG.u64_val(a), SG.u64_val(b))) : Maybe<&2, Nat>}
159      {==}
160
161def checked_rem(+a: WU.U64, +b: WU.U64) -> SF.CheckedRem.value(~WU.U64, ~SG.u64_val, ~F.u64_checked_rem, a, b):
162  crem(a, b, X.is_zero(b), {==})
163
164# ---- shifts: the amount masked to s mod 64 ----
165
166def am(+s: U32) -> {U32.to_nat(U32.and(s, 63)) == Nat.mod(vs(s), 64n) : Nat}:
167  Equal.trans(Nat, U32.to_nat(U32.and(s, 63)), C.low(6n, vs(s)), Nat.mod(vs(s), 64n), FB.andm(s, 6n, 63, {==}), G.low_mod(6n, vs(s), 63n, {==}))
168
169def am_small(+s: U32, +h: {Nat.is_lt(vs(s), 64n) == True{} : Bool}) -> {U32.to_nat(U32.and(s, 63)) == vs(s) : Nat}:
170  Equal.trans(Nat, U32.to_nat(U32.and(s, 63)), Nat.mod(vs(s), 64n), vs(s), am(s), R.mod_of(0n, 63n, vs(s), h))
171
172def lt64(+s: U32) -> {U32.is_lt(s, 64) == Nat.is_lt(vs(s), 64n) : Bool}:
173  U3.is_lt_nat(s, 64)
174
175def wrapping_shl(+a: WU.U64, +s: U32) -> SF.WrappingShl.value(~WU.U64, ~SG.u64_val, ~F.u64_wrapping_shl, 64n, a, s):
176  %Equal.sym(Nat, U32.to_nat(U32.and(s, 63)), Nat.mod(vs(s), 64n), am(s)) : {SG.u64_val(X.shl(a, _)) == C.low(64n, C.shift(Nat.mod(vs(s), 64n), SG.u64_val(a))) : Nat}
177  SH.shl_value(a, Nat.mod(vs(s), 64n), R.dm_lt(63n, vs(s)))
178
179def wrapping_shr(+a: WU.U64, +s: U32) -> SF.WrappingShr.value(~WU.U64, ~SG.u64_val, ~F.u64_wrapping_shr, 64n, a, s):
180  %Equal.sym(Nat, U32.to_nat(U32.and(s, 63)), Nat.mod(vs(s), 64n), am(s)) : {SG.u64_val(X.shr(a, _)) == C.high(Nat.mod(vs(s), 64n), SG.u64_val(a)) : Nat}
181  SH.shr_value(a, Nat.mod(vs(s), 64n))
182
183def overflowing_shl_value(+a: WU.U64, +s: U32) -> SF.OverflowingShl.value(~WU.U64, ~SG.u64_val, ~F.u64_overflowing_shl, 64n, a, s):
184  wrapping_shl(a, s)
185
186def overflowing_shr_value(+a: WU.U64, +s: U32) -> SF.OverflowingShr.value(~WU.U64, ~SG.u64_val, ~F.u64_overflowing_shr, 64n, a, s):
187  wrapping_shr(a, s)
188
189def overflowing_shl_flag(+a: WU.U64, +s: U32) -> SF.OverflowingShl.flag(~WU.U64, ~F.u64_overflowing_shl, a, s, 64n):
190  G.bnot_eq(U32.is_lt(s, 64), Nat.is_lt(vs(s), 64n), lt64(s))
191
192def overflowing_shr_flag(+a: WU.U64, +s: U32) -> SF.OverflowingShr.flag(~WU.U64, ~F.u64_overflowing_shr, a, s, 64n):
193  G.bnot_eq(U32.is_lt(s, 64), Nat.is_lt(vs(s), 64n), lt64(s))
194
195def cshl(+a: WU.U64, +s: U32, +ok: Bool, +hok: {Nat.is_lt(vs(s), 64n) == ok : Bool}) -> {SF.mval(~WU.U64, ~SG.u64_val, F.opt(WU.U64, Bool.not(U32.is_lt(s, 64)), X.shl(a, U32.to_nat(U32.and(s, 63))))) == SF.keep(ok, C.low(64n, C.shift(vs(s), SG.u64_val(a)))) : Maybe<&2, Nat>}:
196  match ok:
197    case True{}:
198      +hb = Equal.trans(Bool, U32.is_lt(s, 64), Nat.is_lt(vs(s), 64n), ok, lt64(s), hok)
199      +ev = Equal.trans(Nat, SG.u64_val(X.shl(a, U32.to_nat(U32.and(s, 63)))), SG.u64_val(X.shl(a, vs(s))), C.low(64n, C.shift(vs(s), SG.u64_val(a))), Equal.cong(Nat, Nat, t => SG.u64_val(X.shl(a, t)), U32.to_nat(U32.and(s, 63)), vs(s), am_small(s, hok)), SH.shl_value(a, vs(s), hok))
200      G.some_of(~WU.U64, ~SG.u64_val, Bool.not(U32.is_lt(s, 64)), G.bnot_eq(U32.is_lt(s, 64), True{}, hb), X.shl(a, U32.to_nat(U32.and(s, 63))), C.low(64n, C.shift(vs(s), SG.u64_val(a))), ev)
201    case False{}:
202      +hb = Equal.trans(Bool, U32.is_lt(s, 64), Nat.is_lt(vs(s), 64n), ok, lt64(s), hok)
203      G.none_of(~WU.U64, ~SG.u64_val, Bool.not(U32.is_lt(s, 64)), G.bnot_eq(U32.is_lt(s, 64), False{}, hb), X.shl(a, U32.to_nat(U32.and(s, 63))))
204
205def checked_shl(+a: WU.U64, +s: U32) -> SF.CheckedShl.value(~WU.U64, ~SG.u64_val, ~F.u64_checked_shl, 64n, a, s):
206  cshl(a, s, Nat.is_lt(vs(s), 64n), {==})
207
208def cshr(+a: WU.U64, +s: U32, +ok: Bool, +hok: {Nat.is_lt(vs(s), 64n) == ok : Bool}) -> {SF.mval(~WU.U64, ~SG.u64_val, F.opt(WU.U64, Bool.not(U32.is_lt(s, 64)), X.shr(a, U32.to_nat(U32.and(s, 63))))) == SF.keep(ok, C.high(vs(s), SG.u64_val(a))) : Maybe<&2, Nat>}:
209  match ok:
210    case True{}:
211      +hb = Equal.trans(Bool, U32.is_lt(s, 64), Nat.is_lt(vs(s), 64n), ok, lt64(s), hok)
212      +ev = Equal.trans(Nat, SG.u64_val(X.shr(a, U32.to_nat(U32.and(s, 63)))), SG.u64_val(X.shr(a, vs(s))), C.high(vs(s), SG.u64_val(a)), Equal.cong(Nat, Nat, t => SG.u64_val(X.shr(a, t)), U32.to_nat(U32.and(s, 63)), vs(s), am_small(s, hok)), SH.shr_value(a, vs(s)))
213      G.some_of(~WU.U64, ~SG.u64_val, Bool.not(U32.is_lt(s, 64)), G.bnot_eq(U32.is_lt(s, 64), True{}, hb), X.shr(a, U32.to_nat(U32.and(s, 63))), C.high(vs(s), SG.u64_val(a)), ev)
214    case False{}:
215      +hb = Equal.trans(Bool, U32.is_lt(s, 64), Nat.is_lt(vs(s), 64n), ok, lt64(s), hok)
216      G.none_of(~WU.U64, ~SG.u64_val, Bool.not(U32.is_lt(s, 64)), G.bnot_eq(U32.is_lt(s, 64), False{}, hb), X.shr(a, U32.to_nat(U32.and(s, 63))))
217
218def checked_shr(+a: WU.U64, +s: U32) -> SF.CheckedShr.value(~WU.U64, ~SG.u64_val, ~F.u64_checked_shr, 64n, a, s):
219  cshr(a, s, Nat.is_lt(vs(s), 64n), {==})
220
221# ---- pow through the generic checked pow ----
222
223def pw(+a: WU.U64, +e: U32) -> Nat:
224  Nat.pow(SG.u64_val(a), vs(e))
225
226def gpow(+a: WU.U64, +e: U32) -> Result<&2, &2, NM.NumError, WU.U64>:
227  GN.pow(~WU.U64, ~I.u64_op, ~I.u64_is, a, vs(e))
228
229def cpow(+a: WU.U64, +e: U32, +ok: Bool, +hok: {C.fits(64n, pw(a, e)) == ok : Bool}) -> {SF.mval(~WU.U64, ~SG.u64_val, F.res_opt(WU.U64, gpow(a, e))) == SF.keep(ok, pw(a, e)) : Maybe<&2, Nat>}:
230  match ok:
231    case True{}:
232      %Equal.sym(Result<&2, &2, NM.NumError, WU.U64>, gpow(a, e), SG.checked(~WU.U64, ~SG.u64_of, 64n, pw(a, e)), UI.pow_checked(a, vs(e))) : {SF.mval(~WU.U64, ~SG.u64_val, F.res_opt(WU.U64, _)) == Some{pw(a, e)} : Maybe<&2, Nat>}
233      %Equal.sym(Bool, C.fits(64n, pw(a, e)), True{}, hok) : {SF.mval(~WU.U64, ~SG.u64_val, F.res_opt(WU.U64, SG.checked_pick(~WU.U64, ~SG.u64_of, pw(a, e), _))) == Some{pw(a, e)} : Maybe<&2, Nat>}
234      Equal.cong(Nat, Maybe<&2, Nat>, t => Some{t}, SG.u64_val(SG.u64_of(pw(a, e))), pw(a, e), LV.vo(pw(a, e), hok))
235    case False{}:
236      %Equal.sym(Result<&2, &2, NM.NumError, WU.U64>, gpow(a, e), SG.checked(~WU.U64, ~SG.u64_of, 64n, pw(a, e)), UI.pow_checked(a, vs(e))) : {SF.mval(~WU.U64, ~SG.u64_val, F.res_opt(WU.U64, _)) == None{} : Maybe<&2, Nat>}
237      %Equal.sym(Bool, C.fits(64n, pw(a, e)), False{}, hok) : {SF.mval(~WU.U64, ~SG.u64_val, F.res_opt(WU.U64, SG.checked_pick(~WU.U64, ~SG.u64_of, pw(a, e), _))) == None{} : Maybe<&2, Nat>}
238      {==}
239
240def checked_pow(+a: WU.U64, +e: U32) -> SF.CheckedPow.value(~WU.U64, ~SG.u64_val, ~F.u64_checked_pow, 64n, a, e):
241  cpow(a, e, C.fits(64n, pw(a, e)), {==})
242
243def spow(+top: WU.U64, +ht: {Bool.and(C.fits(64n, SG.u64_val(top)), Bool.not(C.fits(64n, 1n+SG.u64_val(top)))) == True{} : Bool}, +a: WU.U64, +e: U32, +ok: Bool, +hok: {C.fits(64n, pw(a, e)) == ok : Bool}) -> {SF.saturated(64n, pw(a, e), SG.u64_val(F.or_top(WU.U64, top, F.res_opt(WU.U64, gpow(a, e)))), ok) == True{} : Bool}:
244  match ok:
245    case True{}:
246      %Equal.sym(Result<&2, &2, NM.NumError, WU.U64>, gpow(a, e), SG.checked(~WU.U64, ~SG.u64_of, 64n, pw(a, e)), UI.pow_checked(a, vs(e))) : {SF.saturated(64n, pw(a, e), SG.u64_val(F.or_top(WU.U64, top, F.res_opt(WU.U64, _))), True{}) == True{} : Bool}
247      %Equal.sym(Bool, C.fits(64n, pw(a, e)), True{}, hok) : {SF.saturated(64n, pw(a, e), SG.u64_val(F.or_top(WU.U64, top, F.res_opt(WU.U64, SG.checked_pick(~WU.U64, ~SG.u64_of, pw(a, e), _)))), True{}) == True{} : Bool}
248      %Equal.sym(Nat, SG.u64_val(SG.u64_of(pw(a, e))), pw(a, e), LV.vo(pw(a, e), hok)) : {Nat.is_eq(_, pw(a, e)) == True{} : Bool}
249      N.is_eq_refl(pw(a, e))
250    case False{}:
251      %Equal.sym(Result<&2, &2, NM.NumError, WU.U64>, gpow(a, e), SG.checked(~WU.U64, ~SG.u64_of, 64n, pw(a, e)), UI.pow_checked(a, vs(e))) : {SF.saturated(64n, pw(a, e), SG.u64_val(F.or_top(WU.U64, top, F.res_opt(WU.U64, _))), False{}) == True{} : Bool}
252      %Equal.sym(Bool, C.fits(64n, pw(a, e)), False{}, hok) : {SF.saturated(64n, pw(a, e), SG.u64_val(F.or_top(WU.U64, top, F.res_opt(WU.U64, SG.checked_pick(~WU.U64, ~SG.u64_of, pw(a, e), _)))), False{}) == True{} : Bool}
253      ht
254
255def saturating_pow(+a: WU.U64, +e: U32) -> SF.SaturatingPow.value(~WU.U64, ~SG.u64_val, ~F.u64_saturating_pow, 64n, a, e):
256  spow(F.u64_max(), top(1n, {==}), a, e, C.fits(64n, pw(a, e)), {==})
257
258def opow(+a: WU.U64, +e: U32, +ok: Bool, +hok: {C.fits(64n, pw(a, e)) == ok : Bool}) -> {F.res_bad(WU.U64, gpow(a, e)) == Bool.not(ok) : Bool}:
259  match ok:
260    case True{}:
261      %Equal.sym(Result<&2, &2, NM.NumError, WU.U64>, gpow(a, e), SG.checked(~WU.U64, ~SG.u64_of, 64n, pw(a, e)), UI.pow_checked(a, vs(e))) : {F.res_bad(WU.U64, _) == False{} : Bool}
262      %Equal.sym(Bool, C.fits(64n, pw(a, e)), True{}, hok) : {F.res_bad(WU.U64, SG.checked_pick(~WU.U64, ~SG.u64_of, pw(a, e), _)) == False{} : Bool}
263      {==}
264    case False{}:
265      %Equal.sym(Result<&2, &2, NM.NumError, WU.U64>, gpow(a, e), SG.checked(~WU.U64, ~SG.u64_of, 64n, pw(a, e)), UI.pow_checked(a, vs(e))) : {F.res_bad(WU.U64, _) == True{} : Bool}
266      %Equal.sym(Bool, C.fits(64n, pw(a, e)), False{}, hok) : {F.res_bad(WU.U64, SG.checked_pick(~WU.U64, ~SG.u64_of, pw(a, e), _)) == True{} : Bool}
267      {==}
268
269def overflowing_pow_flag(+a: WU.U64, +e: U32) -> SF.OverflowingPow.flag(~WU.U64, ~SG.u64_val, ~F.u64_overflowing_pow, 64n, a, e):
270  opow(a, e, C.fits(64n, pw(a, e)), {==})
271
272# ---- wrapping pow: right-to-left binary exponentiation mod 2^64 ----
273# (natural.bend's pow_mod_go step, proved in proofs/math/natural/modpow.bend,
274# run on the values with m = 2^64 = 1 + mp; e halves each step, so 32 steps
275# cover every U32 exponent)
276
277def lt_m(+mp: Nat, +hp: {C.pow2(64n) == 1n+mp : Nat}, +x: WU.U64) -> {Nat.is_lt(SG.u64_val(x), 1n+mp) == True{} : Bool}:
278  Equal.trans(Bool, Nat.is_lt(SG.u64_val(x), 1n+mp), Nat.is_lt(SG.u64_val(x), C.pow2(64n)), True{}, Equal.cong(Nat, Bool, t => Nat.is_lt(SG.u64_val(x), t), 1n+mp, C.pow2(64n), Equal.sym(Nat, C.pow2(64n), 1n+mp, hp)), WW.lt_of_fits(64n, SG.u64_val(x), LV.vb(x)))
279
280def mul_m(+mp: Nat, +hp: {C.pow2(64n) == 1n+mp : Nat}, +x: WU.U64, +y: WU.U64) -> {SG.u64_val(X.mul(x, y)) == Nat.mod(Nat.mul(SG.u64_val(x), SG.u64_val(y)), 1n+mp) : Nat}:
281  Equal.trans(Nat, SG.u64_val(X.mul(x, y)), C.low(64n, Nat.mul(SG.u64_val(x), SG.u64_val(y))), Nat.mod(Nat.mul(SG.u64_val(x), SG.u64_val(y)), 1n+mp), WA.mul_value(x, y), G.low_mod(64n, Nat.mul(SG.u64_val(x), SG.u64_val(y)), mp, hp))
282
283def wp_base(+mp: Nat, +hp: {C.pow2(64n) == 1n+mp : Nat}, +e: U32, +b: WU.U64, +acc: WU.U64, +h0: {vs(e) == 0n : Nat}) -> {SG.u64_val(acc) == Nat.mod(Nat.mul(SG.u64_val(acc), Nat.pow(SG.u64_val(b), vs(e))), 1n+mp) : Nat}:
284  %Equal.sym(Nat, vs(e), 0n, h0) : {SG.u64_val(acc) == Nat.mod(Nat.mul(SG.u64_val(acc), Nat.pow(SG.u64_val(b), _)), 1n+mp) : Nat}
285  %Equal.sym(Nat, Nat.mul(SG.u64_val(acc), 1n), SG.u64_val(acc), NA.mul_one(SG.u64_val(acc))) : {SG.u64_val(acc) == Nat.mod(_, 1n+mp) : Nat}
286  Equal.sym(Nat, Nat.mod(SG.u64_val(acc), 1n+mp), SG.u64_val(acc), R.mod_of(0n, mp, SG.u64_val(acc), lt_m(mp, hp, acc)))
287
288# the odd bit multiplies acc by b (pow_mod_odd on the values)
289def wp_odd(+mp: Nat, +hp: {C.pow2(64n) == 1n+mp : Nat}, +e: U32, +b: WU.U64, +acc: WU.U64, +r: Nat, +hodd: {I.u32_odd(e) == Nat.is_eq(r, 1n) : Bool}, +hr: {Nat.is_lt(r, 2n) == True{} : Bool}) -> {SG.u64_val(F.pick(WU.U64, I.u32_odd(e), X.mul(acc, b), acc)) == M.pow_mod_odd(1n+mp, r, SG.u64_val(b), SG.u64_val(acc)) : Nat}:
290  match r:
291    case 0n:
292      %Equal.sym(Bool, I.u32_odd(e), False{}, hodd) : {SG.u64_val(F.pick(WU.U64, _, X.mul(acc, b), acc)) == SG.u64_val(acc) : Nat}
293      {==}
294    case 1n:
295      %Equal.sym(Bool, I.u32_odd(e), True{}, hodd) : {SG.u64_val(F.pick(WU.U64, _, X.mul(acc, b), acc)) == Nat.mod(Nat.mul(SG.u64_val(acc), SG.u64_val(b)), 1n+mp) : Nat}
296      mul_m(mp, hp, acc, b)
297    case 2n+ +q:
298      Empty.absurd({SG.u64_val(F.pick(WU.U64, I.u32_odd(e), X.mul(acc, b), acc)) == M.pow_mod_odd(1n+mp, 2n+q, SG.u64_val(b), SG.u64_val(acc)) : Nat}, N.lt_zero_absurd(q, hr))
299
300def half_e(+e: U32) -> {vs(U32.shr(e)) == Nat.div(vs(e), 2n) : Nat}:
301  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)))
302
303def wp_go(fuel: Nat, +mp: Nat, +hp: {C.pow2(64n) == 1n+mp : Nat}, +e: U32, +b: WU.U64, +acc: WU.U64, +z: Bool, +hz: {U32.is_zero(e) == z : Bool}, +he: {Nat.is_lt(vs(e), C.pow2(fuel)) == True{} : Bool}) -> {SG.u64_val(F.u64_wpow(fuel, e, b, acc, z)) == Nat.mod(Nat.mul(SG.u64_val(acc), Nat.pow(SG.u64_val(b), vs(e))), 1n+mp) : Nat}:
304  match fuel z:
305    case 0n _:
306      wp_base(mp, hp, e, b, acc, G.lt1(vs(e), he))
307    case 1n+f True{}:
308      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)))
309    case 1n+ +f False{}:
310      +ve = vs(e)
311      +e2 = Nat.div(ve, 2n)
312      +bit = Nat.mod(ve, 2n)
313      +m = {1n+mp : Nat}
314      +acc2 = F.pick(WU.U64, I.u32_odd(e), X.mul(acc, b), acc)
315      +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))
316      +ih = wp_go(f, mp, hp, U32.shr(e), X.mul(b, b), acc2, U32.is_zero(U32.shr(e)), {==}, he2)
317      +ea = wp_odd(mp, hp, e, b, acc, bit, LW.tests_odd(e), B.half_rem(ve))
318      +eb = mul_m(mp, hp, b, b)
319      +x1 = Equal.cong(Nat, Nat, t => Nat.mod(Nat.mul(t, Nat.pow(SG.u64_val(X.mul(b, b)), vs(U32.shr(e)))), m), SG.u64_val(acc2), M.pow_mod_odd(m, bit, SG.u64_val(b), SG.u64_val(acc)), ea)
320      +x2 = Equal.cong(Nat, Nat, t => Nat.mod(Nat.mul(M.pow_mod_odd(m, bit, SG.u64_val(b), SG.u64_val(acc)), Nat.pow(t, vs(U32.shr(e)))), m), SG.u64_val(X.mul(b, b)), Nat.mod(Nat.mul(SG.u64_val(b), SG.u64_val(b)), m), eb)
321      +x3 = Equal.cong(Nat, Nat, t => Nat.mod(Nat.mul(M.pow_mod_odd(m, bit, SG.u64_val(b), SG.u64_val(acc)), Nat.pow(Nat.mod(Nat.mul(SG.u64_val(b), SG.u64_val(b)), m), t)), m), vs(U32.shr(e)), e2, half_e(e))
322      +x4 = MP.pm_bit(mp, e2, bit, B.half_rem(ve), SG.u64_val(b), SG.u64_val(acc))
323      +x5 = Equal.cong(Nat, Nat, t => Nat.mod(Nat.mul(SG.u64_val(acc), Nat.pow(SG.u64_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)))
324      +L0 = Nat.mod(Nat.mul(SG.u64_val(acc2), Nat.pow(SG.u64_val(X.mul(b, b)), vs(U32.shr(e)))), m)
325      +L1 = Nat.mod(Nat.mul(M.pow_mod_odd(m, bit, SG.u64_val(b), SG.u64_val(acc)), Nat.pow(SG.u64_val(X.mul(b, b)), vs(U32.shr(e)))), m)
326      +L2 = Nat.mod(Nat.mul(M.pow_mod_odd(m, bit, SG.u64_val(b), SG.u64_val(acc)), Nat.pow(Nat.mod(Nat.mul(SG.u64_val(b), SG.u64_val(b)), m), vs(U32.shr(e)))), m)
327      +L3 = Nat.mod(Nat.mul(M.pow_mod_odd(m, bit, SG.u64_val(b), SG.u64_val(acc)), Nat.pow(Nat.mod(Nat.mul(SG.u64_val(b), SG.u64_val(b)), m), e2)), m)
328      +L4 = Nat.mod(Nat.mul(SG.u64_val(acc), Nat.pow(SG.u64_val(b), Nat.add(Nat.double(e2), bit))), m)
329      +L5 = Nat.mod(Nat.mul(SG.u64_val(acc), Nat.pow(SG.u64_val(b), ve)), m)
330      Equal.trans(Nat, SG.u64_val(F.u64_wpow(f, U32.shr(e), X.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)))))
331
332def wp_top(+mp: Nat, +hp: {C.pow2(64n) == 1n+mp : Nat}, +a: WU.U64, +e: U32) -> {SG.u64_val(F.u64_wrapping_pow(a, e)) == C.low(64n, pw(a, e)) : Nat}:
333  +ih = wp_go(32n, mp, hp, e, a, WU.U64{1, 0}, U32.is_zero(e), {==}, WW.lt_of_fits(32n, vs(e), LW.vb(e)))
334  +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)))
335  Equal.trans(Nat, SG.u64_val(F.u64_wrapping_pow(a, e)), Nat.mod(Nat.mul(1n, pw(a, e)), 1n+mp), C.low(64n, 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(64n, pw(a, e)), e1, Equal.sym(Nat, C.low(64n, pw(a, e)), Nat.mod(pw(a, e), 1n+mp), G.low_mod(64n, pw(a, e), mp, hp))))
336
337def wrapping_pow(+a: WU.U64, +e: U32) -> SF.WrappingPow.value(~WU.U64, ~SG.u64_val, ~F.u64_wrapping_pow, 64n, a, e):
338  wp_top(Nat.sub(C.pow2(64n), 1n), SH.pow2_eq(64n), a, e)
339
340def overflowing_pow_value(+a: WU.U64, +e: U32) -> SF.OverflowingPow.value(~WU.U64, ~SG.u64_val, ~F.u64_overflowing_pow, 64n, a, e):
341  wrapping_pow(a, e)
342
343# ---- wrapping sub: a + (2^64 - 1 - b) + 1, with m == 2^64 - 1 abstract ----
344
345def wsub_val(+m: WU.U64, +one: Nat, +h1: {one == 1n : Nat}, +hmo: {1n+SG.u64_val(m) == C.shift(64n, one) : Nat}, +a: WU.U64, +b: WU.U64) -> {SG.u64_val(X.add(X.add(a, X.sub(m, b)), WU.U64{1, 0})) == C.low(64n, Nat.add(Nat.add(SG.u64_val(a), Nat.sub(SG.u64_val(m), SG.u64_val(b))), 1n)) : Nat}:
346  +S = C.shift(64n, one)
347  +hlt = Equal.trans(Bool, Nat.is_lt(SG.u64_val(b), 1n+SG.u64_val(m)), Nat.is_lt(SG.u64_val(b), S), True{}, Equal.cong(Nat, Bool, t => Nat.is_lt(SG.u64_val(b), t), 1n+SG.u64_val(m), S, hmo), WW.lt_one(64n, one, h1, SG.u64_val(b), LV.vb(b)))
348  +e2 = Equal.cong(Nat, Nat, t => C.low(64n, Nat.add(t, 1n)), SG.u64_val(X.add(a, X.sub(m, b))), C.low(64n, Nat.add(SG.u64_val(a), SG.u64_val(X.sub(m, b)))), WA.add_value(a, X.sub(m, b)))
349  +e3 = G.low_add_low(64n, Nat.add(SG.u64_val(a), SG.u64_val(X.sub(m, b))), 1n)
350  +e4 = Equal.cong(Nat, Nat, t => C.low(64n, Nat.add(Nat.add(SG.u64_val(a), t), 1n)), SG.u64_val(X.sub(m, b)), Nat.sub(SG.u64_val(m), SG.u64_val(b)), WA.sub_value(m, b, N.lt_succ_le(SG.u64_val(b), SG.u64_val(m), hlt)))
351  Equal.trans(Nat, SG.u64_val(X.add(X.add(a, X.sub(m, b)), WU.U64{1, 0})), C.low(64n, Nat.add(SG.u64_val(X.add(a, X.sub(m, b))), 1n)), C.low(64n, Nat.add(Nat.add(SG.u64_val(a), Nat.sub(SG.u64_val(m), SG.u64_val(b))), 1n)), WA.add_value(X.add(a, X.sub(m, b)), WU.U64{1, 0}), Equal.trans(Nat, C.low(64n, Nat.add(SG.u64_val(X.add(a, X.sub(m, b))), 1n)), C.low(64n, Nat.add(C.low(64n, Nat.add(SG.u64_val(a), SG.u64_val(X.sub(m, b)))), 1n)), C.low(64n, Nat.add(Nat.add(SG.u64_val(a), Nat.sub(SG.u64_val(m), SG.u64_val(b))), 1n)), e2, Equal.trans(Nat, C.low(64n, Nat.add(C.low(64n, Nat.add(SG.u64_val(a), SG.u64_val(X.sub(m, b)))), 1n)), C.low(64n, Nat.add(Nat.add(SG.u64_val(a), SG.u64_val(X.sub(m, b))), 1n)), C.low(64n, Nat.add(Nat.add(SG.u64_val(a), Nat.sub(SG.u64_val(m), SG.u64_val(b))), 1n)), e3, e4)))
352
353def wsub_g(+one: Nat, +h1: {one == 1n : Nat}, +m: WU.U64, +hmo: {1n+SG.u64_val(m) == C.shift(64n, one) : Nat}, +a: WU.U64, +b: WU.U64) -> {Nat.add(SG.u64_val(X.add(X.add(a, X.sub(m, b)), WU.U64{1, 0})), SG.u64_val(b)) == Nat.add(SG.u64_val(a), C.shift(64n, SF.bn(Nat.is_lt(SG.u64_val(a), SG.u64_val(b))))) : Nat}:
354  +S = C.shift(64n, one)
355  +d = Nat.add(Nat.add(SG.u64_val(a), Nat.sub(SG.u64_val(m), SG.u64_val(b))), 1n)
356  +hlt = Equal.trans(Bool, Nat.is_lt(SG.u64_val(b), 1n+SG.u64_val(m)), Nat.is_lt(SG.u64_val(b), S), True{}, Equal.cong(Nat, Bool, t => Nat.is_lt(SG.u64_val(b), t), 1n+SG.u64_val(m), S, hmo), WW.lt_one(64n, one, h1, SG.u64_val(b), LV.vb(b)))
357  +ed = G.plus_one(SG.u64_val(a), Nat.sub(SG.u64_val(m), SG.u64_val(b)), SG.u64_val(b), SG.u64_val(m), S, N.sub_add(SG.u64_val(m), SG.u64_val(b), N.lt_succ_le(SG.u64_val(b), SG.u64_val(m), hlt)), hmo)
358  %Equal.sym(Nat, SG.u64_val(X.add(X.add(a, X.sub(m, b)), WU.U64{1, 0})), C.low(64n, d), wsub_val(m, one, h1, hmo, a, b)) : {Nat.add(_, SG.u64_val(b)) == Nat.add(SG.u64_val(a), C.shift(64n, SF.bn(Nat.is_lt(SG.u64_val(a), SG.u64_val(b))))) : Nat}
359  G.wsub(64n, one, h1, SG.u64_val(a), SG.u64_val(b), d, ed, LV.vb(a), Nat.is_lt(SG.u64_val(a), SG.u64_val(b)), {==})
360
361def wsub_eq(+a: WU.U64, +b: WU.U64) -> {Nat.add(SG.u64_val(F.u64_wsub(a, b)), SG.u64_val(b)) == Nat.add(SG.u64_val(a), C.shift(64n, SF.bn(Nat.is_lt(SG.u64_val(a), SG.u64_val(b))))) : Nat}:
362  wsub_g(1n, {==}, F.u64_max(), top1(1n, {==}), a, b)
363
364def wrapping_sub(+a: WU.U64, +b: WU.U64) -> SF.WrappingSub.value(~WU.U64, ~SG.u64_val, ~F.u64_wrapping_sub, 64n, a, b):
365  wsub_eq(a, b)
366
367def overflowing_sub_value(+a: WU.U64, +b: WU.U64) -> SF.OverflowingSub.value(~WU.U64, ~SG.u64_val, ~F.u64_overflowing_sub, 64n, a, b):
368  wsub_eq(a, b)