~/bend-docscommunity

proofs/math/typed/fix64.bend source

proofs/math/typed/fix64.bend on the hub · documented module

import Baseimport ../../../spec/lib/common.bend as Cimport ../../../spec/math/generic.bend as SGimport ../../../spec/math/fixed.bend as SFimport ../../../src/math/w64.bend as Ximport ../../../src/math/u64.bend as WUimport ../../../src/math/fixed.bend as Fimport ../../../src/math/generic.bend as GNimport ../../../src/math/instances.bend as Iimport ../../../src/math/num.bend as NMimport ../../../src/math/natural.bend as Mimport ../../lib/nat.bend as Nimport ../../lib/lemmas/proofs/nat_algebra.bend as NAimport ../natural/modpow.bend as MPimport ../natural/bits.bend as Bimport ./u32laws.bend as LWimport ./shrn.bend as SHNimport ../../lib/u32.bend as U3import ../../lib/arith.bend as ARimport ../natural/arith.bend as Rimport ./width.bend as WWimport ./w64add.bend as WAimport ./w64sh.bend as SHimport ./w64dmtop.bend as DTimport ./w64dmrem.bend as DRimport ./u64laws.bend as LVimport ./u64int.bend as UIimport ./u64mont.bend as MTimport ./f64bits.bend as FBimport ./fixgen.bend as Gimport ../../lib/word.bend as WDimport ../../lib/logic.bend as L# The U64 clauses of spec/math/fixed.bend (Rust's u64 checked_*, wrapping_*,# saturating_*, overflowing_* families) from the proved two-limb clauses of# spec/math/w64.bend (proofs/math/typed/w64add.bend, w64sh.bend,# w64dmtop.bend, w64dmrem.bend) and the generic pow of u64int.bend, as# HACL*'s Hacl.Spec.Bignum proves each word operation through its value.def vs(+s: U32) -> Nat:  U32.to_nat(s)# ---- the largest value ----def zero_add(+x: Nat) -> {Nat.add(0n, x) == x : Nat}:  Equal.trans(Nat, Nat.add(0n, x), Nat.add(x, 0n), x, N.add_comm(0n, x), N.add_zero(x))# The largest value 2^64 - 1 is built with its limbs abstract (w, the# all-ones U32) and 1 kept as one: the checker must never unfold 2^64, and# closed 64-bit values are only ever compared as U64s.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}:  MT.ones_v(one, h1, w, pw)def top1(+one: Nat, +h1: {one == 1n : Nat}) -> {1n+SG.u64_val(F.u64_max()) == C.shift(64n, one) : Nat}:  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, {==}))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}:  +m = {WU.U64{w, w} : WU.U64}  +S = C.shift(64n, one)  +e1 = Equal.cong(Nat, Bool, t => C.fits(64n, t), 1n+SG.u64_val(m), S, top1w(one, h1, w, pw))  +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)))  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))))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}:  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, {==}))# ---- add, mul ----def checked_add(+a: WU.U64, +b: WU.U64) -> SF.CheckedAdd.value(~WU.U64, ~SG.u64_val, ~F.u64_checked_add, 64n, a, b):  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))), {==})def wrapping_add(+a: WU.U64, +b: WU.U64) -> SF.WrappingAdd.value(~WU.U64, ~SG.u64_val, ~F.u64_wrapping_add, 64n, a, b):  WA.add_value(a, b)def saturating_add(+a: WU.U64, +b: WU.U64) -> SF.SaturatingAdd.value(~WU.U64, ~SG.u64_val, ~F.u64_saturating_add, 64n, a, b):  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))), {==})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):  WA.add_value(a, b)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):  WA.add_over_value(a, b)def checked_mul(+a: WU.U64, +b: WU.U64) -> SF.CheckedMul.value(~WU.U64, ~SG.u64_val, ~F.u64_checked_mul, 64n, a, b):  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))), {==})def wrapping_mul(+a: WU.U64, +b: WU.U64) -> SF.WrappingMul.value(~WU.U64, ~SG.u64_val, ~F.u64_wrapping_mul, 64n, a, b):  WA.mul_value(a, b)def saturating_mul(+a: WU.U64, +b: WU.U64) -> SF.SaturatingMul.value(~WU.U64, ~SG.u64_val, ~F.u64_saturating_mul, 64n, a, b):  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))), {==})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):  WA.mul_value(a, b)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):  WA.mul_over_value(a, b)# ---- sub ----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>}:  match ok:    case True{}:      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))    case False{}:      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))def checked_sub(+a: WU.U64, +b: WU.U64) -> SF.CheckedSub.value(~WU.U64, ~SG.u64_val, ~F.u64_checked_sub, a, b):  csub(a, b, Nat.is_le(SG.u64_val(b), SG.u64_val(a)), {==})def sub_big(+n: Nat, +d: Nat, +h: {Nat.is_le(n, d) == True{} : Bool}) -> {Nat.sub(n, d) == 0n : Nat}:  match n d:    case 0n _:      R.zsub(d)    case 1n+np 0n:      Empty.absurd({Nat.sub(1n+np, 0n) == 0n : Nat}, L.false_true(h))    case 1n+ +np 1n+ +dp:      sub_big(np, dp, h)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}:  match c:    case True{}:      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)))    case False{}:      WA.sub_value(a, b, N.not_lt_le(SG.u64_val(a), SG.u64_val(b), hn))def saturating_sub(+a: WU.U64, +b: WU.U64) -> SF.SaturatingSub.value(~WU.U64, ~SG.u64_val, ~F.u64_saturating_sub, a, b):  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)))def overflowing_sub_flag(+a: WU.U64, +b: WU.U64) -> SF.OverflowingSub.flag(~WU.U64, ~SG.u64_val, ~F.u64_overflowing_sub, a, b):  WA.lt_value(a, b)# ---- div, rem ----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>}:  match z:    case False{}:      +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)      %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>}      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))    case True{}:      +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)      %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>}      {==}def checked_div(+a: WU.U64, +b: WU.U64) -> SF.CheckedDiv.value(~WU.U64, ~SG.u64_val, ~F.u64_checked_div, a, b):  cdiv(a, b, X.is_zero(b), {==})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>}:  match z:    case False{}:      +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)      %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>}      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))    case True{}:      +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)      %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>}      {==}def checked_rem(+a: WU.U64, +b: WU.U64) -> SF.CheckedRem.value(~WU.U64, ~SG.u64_val, ~F.u64_checked_rem, a, b):  crem(a, b, X.is_zero(b), {==})# ---- shifts: the amount masked to s mod 64 ----def am(+s: U32) -> {U32.to_nat(U32.and(s, 63)) == Nat.mod(vs(s), 64n) : Nat}:  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, {==}))def am_small(+s: U32, +h: {Nat.is_lt(vs(s), 64n) == True{} : Bool}) -> {U32.to_nat(U32.and(s, 63)) == vs(s) : Nat}:  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))def lt64(+s: U32) -> {U32.is_lt(s, 64) == Nat.is_lt(vs(s), 64n) : Bool}:  U3.is_lt_nat(s, 64)def wrapping_shl(+a: WU.U64, +s: U32) -> SF.WrappingShl.value(~WU.U64, ~SG.u64_val, ~F.u64_wrapping_shl, 64n, a, s):  %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}  SH.shl_value(a, Nat.mod(vs(s), 64n), R.dm_lt(63n, vs(s)))def wrapping_shr(+a: WU.U64, +s: U32) -> SF.WrappingShr.value(~WU.U64, ~SG.u64_val, ~F.u64_wrapping_shr, 64n, a, s):  %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}  SH.shr_value(a, Nat.mod(vs(s), 64n))def overflowing_shl_value(+a: WU.U64, +s: U32) -> SF.OverflowingShl.value(~WU.U64, ~SG.u64_val, ~F.u64_overflowing_shl, 64n, a, s):  wrapping_shl(a, s)def overflowing_shr_value(+a: WU.U64, +s: U32) -> SF.OverflowingShr.value(~WU.U64, ~SG.u64_val, ~F.u64_overflowing_shr, 64n, a, s):  wrapping_shr(a, s)def overflowing_shl_flag(+a: WU.U64, +s: U32) -> SF.OverflowingShl.flag(~WU.U64, ~F.u64_overflowing_shl, a, s, 64n):  G.bnot_eq(U32.is_lt(s, 64), Nat.is_lt(vs(s), 64n), lt64(s))def overflowing_shr_flag(+a: WU.U64, +s: U32) -> SF.OverflowingShr.flag(~WU.U64, ~F.u64_overflowing_shr, a, s, 64n):  G.bnot_eq(U32.is_lt(s, 64), Nat.is_lt(vs(s), 64n), lt64(s))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>}:  match ok:    case True{}:      +hb = Equal.trans(Bool, U32.is_lt(s, 64), Nat.is_lt(vs(s), 64n), ok, lt64(s), hok)      +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))      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)    case False{}:      +hb = Equal.trans(Bool, U32.is_lt(s, 64), Nat.is_lt(vs(s), 64n), ok, lt64(s), hok)      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))))def checked_shl(+a: WU.U64, +s: U32) -> SF.CheckedShl.value(~WU.U64, ~SG.u64_val, ~F.u64_checked_shl, 64n, a, s):  cshl(a, s, Nat.is_lt(vs(s), 64n), {==})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>}:  match ok:    case True{}:      +hb = Equal.trans(Bool, U32.is_lt(s, 64), Nat.is_lt(vs(s), 64n), ok, lt64(s), hok)      +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)))      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)    case False{}:      +hb = Equal.trans(Bool, U32.is_lt(s, 64), Nat.is_lt(vs(s), 64n), ok, lt64(s), hok)      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))))def checked_shr(+a: WU.U64, +s: U32) -> SF.CheckedShr.value(~WU.U64, ~SG.u64_val, ~F.u64_checked_shr, 64n, a, s):  cshr(a, s, Nat.is_lt(vs(s), 64n), {==})# ---- pow through the generic checked pow ----def pw(+a: WU.U64, +e: U32) -> Nat:  Nat.pow(SG.u64_val(a), vs(e))def gpow(+a: WU.U64, +e: U32) -> Result<&2, &2, NM.NumError, WU.U64>:  GN.pow(~WU.U64, ~I.u64_op, ~I.u64_is, a, vs(e))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>}:  match ok:    case True{}:      %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>}      %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>}      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))    case False{}:      %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>}      %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>}      {==}def checked_pow(+a: WU.U64, +e: U32) -> SF.CheckedPow.value(~WU.U64, ~SG.u64_val, ~F.u64_checked_pow, 64n, a, e):  cpow(a, e, C.fits(64n, pw(a, e)), {==})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}:  match ok:    case True{}:      %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}      %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}      %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}      N.is_eq_refl(pw(a, e))    case False{}:      %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}      %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}      htdef saturating_pow(+a: WU.U64, +e: U32) -> SF.SaturatingPow.value(~WU.U64, ~SG.u64_val, ~F.u64_saturating_pow, 64n, a, e):  spow(F.u64_max(), top(1n, {==}), a, e, C.fits(64n, pw(a, e)), {==})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}:  match ok:    case True{}:      %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}      %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}      {==}    case False{}:      %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}      %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}      {==}def overflowing_pow_flag(+a: WU.U64, +e: U32) -> SF.OverflowingPow.flag(~WU.U64, ~SG.u64_val, ~F.u64_overflowing_pow, 64n, a, e):  opow(a, e, C.fits(64n, pw(a, e)), {==})# ---- wrapping pow: right-to-left binary exponentiation mod 2^64 ----# (natural.bend's pow_mod_go step, proved in proofs/math/natural/modpow.bend,# run on the values with m = 2^64 = 1 + mp; e halves each step, so 32 steps# cover every U32 exponent)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}:  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)))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}:  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))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}:  %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}  %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}  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)))# the odd bit multiplies acc by b (pow_mod_odd on the values)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}:  match r:    case 0n:      %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}      {==}    case 1n:      %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}      mul_m(mp, hp, acc, b)    case 2n+ +q:      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))def half_e(+e: U32) -> {vs(U32.shr(e)) == Nat.div(vs(e), 2n) : Nat}:  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)))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}:  match fuel z:    case 0n _:      wp_base(mp, hp, e, b, acc, G.lt1(vs(e), he))    case 1n+f True{}:      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)))    case 1n+ +f False{}:      +ve = vs(e)      +e2 = Nat.div(ve, 2n)      +bit = Nat.mod(ve, 2n)      +m = {1n+mp : Nat}      +acc2 = F.pick(WU.U64, I.u32_odd(e), X.mul(acc, b), acc)      +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))      +ih = wp_go(f, mp, hp, U32.shr(e), X.mul(b, b), acc2, U32.is_zero(U32.shr(e)), {==}, he2)      +ea = wp_odd(mp, hp, e, b, acc, bit, LW.tests_odd(e), B.half_rem(ve))      +eb = mul_m(mp, hp, b, b)      +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)      +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)      +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))      +x4 = MP.pm_bit(mp, e2, bit, B.half_rem(ve), SG.u64_val(b), SG.u64_val(acc))      +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)))      +L0 = Nat.mod(Nat.mul(SG.u64_val(acc2), Nat.pow(SG.u64_val(X.mul(b, b)), vs(U32.shr(e)))), m)      +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)      +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)      +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)      +L4 = Nat.mod(Nat.mul(SG.u64_val(acc), Nat.pow(SG.u64_val(b), Nat.add(Nat.double(e2), bit))), m)      +L5 = Nat.mod(Nat.mul(SG.u64_val(acc), Nat.pow(SG.u64_val(b), ve)), m)      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)))))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}:  +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)))  +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)))  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))))def wrapping_pow(+a: WU.U64, +e: U32) -> SF.WrappingPow.value(~WU.U64, ~SG.u64_val, ~F.u64_wrapping_pow, 64n, a, e):  wp_top(Nat.sub(C.pow2(64n), 1n), SH.pow2_eq(64n), a, e)def overflowing_pow_value(+a: WU.U64, +e: U32) -> SF.OverflowingPow.value(~WU.U64, ~SG.u64_val, ~F.u64_overflowing_pow, 64n, a, e):  wrapping_pow(a, e)# ---- wrapping sub: a + (2^64 - 1 - b) + 1, with m == 2^64 - 1 abstract ----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}:  +S = C.shift(64n, one)  +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)))  +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)))  +e3 = G.low_add_low(64n, Nat.add(SG.u64_val(a), SG.u64_val(X.sub(m, b))), 1n)  +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)))  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)))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}:  +S = C.shift(64n, one)  +d = Nat.add(Nat.add(SG.u64_val(a), Nat.sub(SG.u64_val(m), SG.u64_val(b))), 1n)  +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)))  +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)  %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}  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)), {==})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}:  wsub_g(1n, {==}, F.u64_max(), top1(1n, {==}), a, b)def wrapping_sub(+a: WU.U64, +b: WU.U64) -> SF.WrappingSub.value(~WU.U64, ~SG.u64_val, ~F.u64_wrapping_sub, 64n, a, b):  wsub_eq(a, b)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):  wsub_eq(a, b)