1 import Base 2 import ../../../spec/lib/common.bend as C 3 import ../../../spec/math/generic.bend as SG 4 import ../../../spec/math/fixed.bend as SF 5 import ../../../src/math/w64.bend as X 6 import ../../../src/math/u64.bend as WU 7 import ../../../src/math/fixed.bend as F 8 import ../../../src/math/generic.bend as GN 9 import ../../../src/math/instances.bend as I 10 import ../../../src/math/num.bend as NM 11 import ../../../src/math/natural.bend as M 12 import ../../lib/nat.bend as N 13 import ../../lib/lemmas/proofs/nat_algebra.bend as NA 14 import ../natural/modpow.bend as MP 15 import ../natural/bits.bend as B 16 import ./u32laws.bend as LW 17 import ./shrn.bend as SHN 18 import ../../lib/u32.bend as U3 19 import ../../lib/arith.bend as AR 20 import ../natural/arith.bend as R 21 import ./width.bend as WW 22 import ./w64add.bend as WA 23 import ./w64sh.bend as SH 24 import ./w64dmtop.bend as DT 25 import ./w64dmrem.bend as DR 26 import ./u64laws.bend as LV 27 import ./u64int.bend as UI 28 import ./u64mont.bend as MT 29 import ./f64bits.bend as FB 30 import ./fixgen.bend as G 31 import ../../lib/word.bend as WD 32 import ../../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 40 def vs(+s: U32) -> Nat: 41 U32.to_nat(s) 42 43 # ---- the largest value ---- 44 45 def 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 52 def 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 55 def 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 58 def 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 65 def 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 70 def 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 73 def 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 76 def 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 79 def 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 82 def 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 85 def 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 88 def 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 91 def 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 94 def 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 97 def 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 102 def 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 109 def 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 112 def 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 121 def 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 128 def 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 131 def 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 136 def 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 147 def 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 150 def 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 161 def 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 166 def 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 169 def 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 172 def lt64(+s: U32) -> {U32.is_lt(s, 64) == Nat.is_lt(vs(s), 64n) : Bool}: 173 U3.is_lt_nat(s, 64) 174 175 def 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 179 def 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 183 def 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 186 def 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 189 def 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 192 def 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 195 def 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 205 def 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 208 def 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 218 def 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 223 def pw(+a: WU.U64, +e: U32) -> Nat: 224 Nat.pow(SG.u64_val(a), vs(e)) 225 226 def 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 229 def 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 240 def 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 243 def 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 255 def 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 258 def 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 269 def 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 277 def 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 280 def 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 283 def 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) 289 def 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 300 def 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 303 def 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 332 def 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 337 def 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 340 def 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 345 def 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 353 def 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 361 def 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 364 def 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 367 def 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)