proofs/math/typed/fix32.bend checks
raw source on the hub · import bend-collections-laws-math@1.0.0.0/proofs/math/typed/fix32.bend as Fix32
30 imports
import Base import ../../../spec/lib/common.bend as C import ../../../spec/math/generic.bend as SG import ../../../spec/math/fixed.bend as SF import ../../../src/math/w64.bend as X import ../../../src/math/fixed.bend as F import ../../../src/math/generic.bend as GN import ../../../src/math/instances.bend as I import ../../../src/math/num.bend as NM import ../../../src/math/natural.bend as M import ../../lib/nat.bend as N import ../../lib/logic.bend as L import ../../lib/arith.bend as AR import ../../lib/word.bend as WD import ../../lib/u32.bend as U3 import ../../lib/u32div.bend as UD import ../../lib/lemmas/proofs/nat_algebra.bend as NA import ../natural/arith.bend as R import ../natural/modpow.bend as MP import ../natural/bits.bend as B import ./width.bend as WW import ./w64add.bend as WA import ../u64/u64.bend as P64 import ./w64sh.bend as SH import ./w64est.bend as WE import ./shrn.bend as SHN import ./u32laws.bend as LW import ./u32int.bend as UI import ./f64bits.bend as FB import ./fixgen.bend as G
Definitions
def vs source · line 39 · raw
@+s:U32 -> Nat
def zero_add source · line 44 · raw
@+x:Nat -> {Nat.add(0n, x) == x : Nat}
def topw source · line 47 · raw
@+one:Nat -> @+h1:{one == 1n : Nat} -> @+w:U32 -> @+pw:{w == U32{0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/word.mask(32n, 32n)} : U32} -> {Bool.and(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(32n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_val(w)), Bool.not(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(32n, 1n+0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_val(w)))) == True{} : Bool}
def top source · line 53 · raw
@+one:Nat -> @+h1:{one == 1n : Nat} -> {Bool.and(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(32n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_val(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/fixed.u32_max)), Bool.not(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(32n, 1n+0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_val(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/fixed.u32_max)))) == True{} : Bool}
def add_low source · line 58 · raw
@+x:U32 -> @+y:U32 -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_val(U32.add(x, y)) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.low(32n, Nat.add(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_val(x), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_val(y))) : Nat}
def mul_low source · line 63 · raw
@+x:U32 -> @+y:U32 -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_val(U32.mul(x, y)) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.low(32n, Nat.mul(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_val(x), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_val(y))) : Nat}
def add_over source · line 66 · raw
@+a:U32 -> @+b:U32 -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/fixed.u32_add_over(a, b) == Bool.not(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(32n, Nat.add(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_val(a), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_val(b)))) : Bool}
def mul_over source · line 69 · raw
@+a:U32 -> @+b:U32 -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/fixed.u32_mul_over(a, b) == Bool.not(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(32n, Nat.mul(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_val(a), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_val(b)))) : Bool}
def lt_nat source · line 72 · raw
@+a:U32 -> @+b:U32 -> {U32.is_lt(a, b) == Nat.is_lt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_val(a), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_val(b)) : Bool}
def checked_add source · line 77 · raw
@+a:U32 -> @+b:U32 -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/fixed.CheckedAdd.value(U32, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_val, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/fixed.u32_checked_add, 32n, a, b)
def wrapping_add source · line 80 · raw
@+a:U32 -> @+b:U32 -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/fixed.WrappingAdd.value(U32, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_val, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/fixed.u32_wrapping_add, 32n, a, b)
def saturating_add source · line 83 · raw
@+a:U32 -> @+b:U32 -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/fixed.SaturatingAdd.value(U32, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_val, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/fixed.u32_saturating_add, 32n, a, b)
def overflowing_add_value source · line 86 · raw
@+a:U32 -> @+b:U32 -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/fixed.OverflowingAdd.value(U32, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_val, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/fixed.u32_overflowing_add, 32n, a, b)
def overflowing_add_flag source · line 89 · raw
@+a:U32 -> @+b:U32 -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/fixed.OverflowingAdd.flag(U32, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_val, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/fixed.u32_overflowing_add, 32n, a, b)
def checked_mul source · line 92 · raw
@+a:U32 -> @+b:U32 -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/fixed.CheckedMul.value(U32, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_val, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/fixed.u32_checked_mul, 32n, a, b)
def wrapping_mul source · line 95 · raw
@+a:U32 -> @+b:U32 -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/fixed.WrappingMul.value(U32, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_val, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/fixed.u32_wrapping_mul, 32n, a, b)
def saturating_mul source · line 98 · raw
@+a:U32 -> @+b:U32 -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/fixed.SaturatingMul.value(U32, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_val, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/fixed.u32_saturating_mul, 32n, a, b)
def overflowing_mul_value source · line 101 · raw
@+a:U32 -> @+b:U32 -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/fixed.OverflowingMul.value(U32, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_val, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/fixed.u32_overflowing_mul, 32n, a, b)
def overflowing_mul_flag source · line 104 · raw
@+a:U32 -> @+b:U32 -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/fixed.OverflowingMul.flag(U32, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_val, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/fixed.u32_overflowing_mul, 32n, a, b)
def sub_exact source · line 109 · raw
@+a:U32 -> @+b:U32 -> @+h:{Nat.is_le(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_val(b), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_val(a)) == True{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_val(U32.sub(a, b)) == Nat.sub(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_val(a), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_val(b)) : Nat}
def csub source · line 112 · raw
@+a:U32 -> @+b:U32 -> @+ok:Bool -> @+hok:{Nat.is_le(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_val(b), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_val(a)) == ok : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/fixed.mval(U32, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_val, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/fixed.opt(U32, U32.is_lt(a, b), U32.sub(a, b))) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/fixed.keep(ok, Nat.sub(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_val(a), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_val(b))) : Maybe<&2, Nat>}
def checked_sub source · line 119 · raw
@+a:U32 -> @+b:U32 -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/fixed.CheckedSub.value(U32, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_val, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/fixed.u32_checked_sub, a, b)
def sub_big source · line 122 · raw
@+n:Nat -> @+d:Nat -> @+h:{Nat.is_le(n, d) == True{} : Bool} -> {Nat.sub(n, d) == 0n : Nat}
def ssub source · line 131 · raw
@+a:U32 -> @+b:U32 -> @+c:Bool -> @+hn:{Nat.is_lt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_val(a), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_val(b)) == c : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_val(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/fixed.pick(U32, c, 0, U32.sub(a, b))) == Nat.sub(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_val(a), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_val(b)) : Nat}
def saturating_sub source · line 138 · raw
@+a:U32 -> @+b:U32 -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/fixed.SaturatingSub.value(U32, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_val, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/fixed.u32_saturating_sub, a, b)
def overflowing_sub_flag source · line 141 · raw
@+a:U32 -> @+b:U32 -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/fixed.OverflowingSub.flag(U32, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_val, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/fixed.u32_overflowing_sub, a, b)
def bo_bn source · line 144 · raw
@+one:Nat -> @+h1:{one == 1n : Nat} -> @+c:Bool -> {0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/word.bo(c, one) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/fixed.bn(c) : Nat}
def wsub_g source · line 151 · raw
@+one:Nat -> @+h1:{one == 1n : Nat} -> @+a:U32 -> @+b:U32 -> {Nat.add(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_val(U32.sub(a, b)), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_val(b)) == Nat.add(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_val(a), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(32n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/fixed.bn(Nat.is_lt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_val(a), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_val(b))))) : Nat}
def wrapping_sub source · line 156 · raw
@+a:U32 -> @+b:U32 -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/fixed.WrappingSub.value(U32, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_val, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/fixed.u32_wrapping_sub, 32n, a, b)
def overflowing_sub_value source · line 159 · raw
@+a:U32 -> @+b:U32 -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/fixed.OverflowingSub.value(U32, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_val, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/fixed.u32_overflowing_sub, 32n, a, b)
def cdiv source · line 164 · raw
@+a:U32 -> @+b:U32 -> @+z:Bool -> @+hz:{U32.is_zero(b) == z : Bool} -> @+ez:{Nat.is_eq(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_val(b), 0n) == z : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/fixed.mval(U32, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_val, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/fixed.opt(U32, z, U32.div(a, b))) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/fixed.keep(Bool.not(Nat.is_eq(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_val(b), 0n)), Nat.div(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_val(a), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_val(b))) : Maybe<&2, Nat>}
def checked_div source · line 173 · raw
@+a:U32 -> @+b:U32 -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/fixed.CheckedDiv.value(U32, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_val, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/fixed.u32_checked_div, a, b)
def crem source · line 176 · raw
@+a:U32 -> @+b:U32 -> @+z:Bool -> @+hz:{U32.is_zero(b) == z : Bool} -> @+ez:{Nat.is_eq(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_val(b), 0n) == z : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/fixed.mval(U32, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_val, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/fixed.opt(U32, z, U32.mod(a, b))) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/fixed.keep(Bool.not(Nat.is_eq(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_val(b), 0n)), Nat.mod(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_val(a), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_val(b))) : Maybe<&2, Nat>}
def checked_rem source · line 185 · raw
@+a:U32 -> @+b:U32 -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/fixed.CheckedRem.value(U32, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_val, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/fixed.u32_checked_rem, a, b)
def am source · line 190 · raw
@+s:U32 -> {U32.to_nat(U32.and(s, 31)) == Nat.mod(vs(s), 32n) : Nat}
def am_small source · line 193 · raw
@+s:U32 -> @+h:{Nat.is_lt(vs(s), 32n) == True{} : Bool} -> {U32.to_nat(U32.and(s, 31)) == vs(s) : Nat}
def lt32 source · line 196 · raw
@+s:U32 -> {U32.is_lt(s, 32) == Nat.is_lt(vs(s), 32n) : Bool}
def wrapping_shl source · line 199 · raw
@+a:U32 -> @+s:U32 -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/fixed.WrappingShl.value(U32, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_val, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/fixed.u32_wrapping_shl, 32n, a, s)
def wrapping_shr source · line 203 · raw
@+a:U32 -> @+s:U32 -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/fixed.WrappingShr.value(U32, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_val, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/fixed.u32_wrapping_shr, 32n, a, s)
def overflowing_shl_value source · line 207 · raw
@+a:U32 -> @+s:U32 -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/fixed.OverflowingShl.value(U32, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_val, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/fixed.u32_overflowing_shl, 32n, a, s)
def overflowing_shr_value source · line 210 · raw
@+a:U32 -> @+s:U32 -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/fixed.OverflowingShr.value(U32, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_val, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/fixed.u32_overflowing_shr, 32n, a, s)
def overflowing_shl_flag source · line 213 · raw
@+a:U32 -> @+s:U32 -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/fixed.OverflowingShl.flag(U32, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/fixed.u32_overflowing_shl, a, s, 32n)
def overflowing_shr_flag source · line 216 · raw
@+a:U32 -> @+s:U32 -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/fixed.OverflowingShr.flag(U32, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/fixed.u32_overflowing_shr, a, s, 32n)
def cshl source · line 219 · raw
@+a:U32 -> @+s:U32 -> @+ok:Bool -> @+hok:{Nat.is_lt(vs(s), 32n) == ok : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/fixed.mval(U32, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_val, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/fixed.opt(U32, Bool.not(U32.is_lt(s, 32)), U32.mul(a, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.pow2(U32.to_nat(U32.and(s, 31)))))) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/fixed.keep(ok, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.low(32n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(vs(s), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_val(a)))) : Maybe<&2, Nat>}
def checked_shl source · line 229 · raw
@+a:U32 -> @+s:U32 -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/fixed.CheckedShl.value(U32, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_val, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/fixed.u32_checked_shl, 32n, a, s)
def cshr source · line 232 · raw
@+a:U32 -> @+s:U32 -> @+ok:Bool -> @+hok:{Nat.is_lt(vs(s), 32n) == ok : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/fixed.mval(U32, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_val, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/fixed.opt(U32, Bool.not(U32.is_lt(s, 32)), U32.shrn(a, U32.to_nat(U32.and(s, 31))))) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/fixed.keep(ok, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.high(vs(s), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_val(a))) : Maybe<&2, Nat>}
def checked_shr source · line 242 · raw
@+a:U32 -> @+s:U32 -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/fixed.CheckedShr.value(U32, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_val, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/fixed.u32_checked_shr, 32n, a, s)
def pw source · line 247 · raw
@+a:U32 -> @+e:U32 -> Nat
def gpow source · line 250 · raw
@+a:U32 -> @+e:U32 -> Result<&2, &2, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.NumError, U32>
def cpow source · line 253 · raw
@+a:U32 -> @+e:U32 -> @+ok:Bool -> @+hok:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(32n, pw(a, e)) == ok : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/fixed.mval(U32, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_val, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/fixed.res_opt(U32, gpow(a, e))) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/fixed.keep(ok, pw(a, e)) : Maybe<&2, Nat>}
def checked_pow source · line 264 · raw
@+a:U32 -> @+e:U32 -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/fixed.CheckedPow.value(U32, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_val, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/fixed.u32_checked_pow, 32n, a, e)
def spow source · line 267 · raw
@+top:U32 -> @+ht:{Bool.and(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(32n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_val(top)), Bool.not(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(32n, 1n+0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_val(top)))) == True{} : Bool} -> @+a:U32 -> @+e:U32 -> @+ok:Bool -> @+hok:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(32n, pw(a, e)) == ok : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/fixed.saturated(32n, pw(a, e), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_val(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/fixed.or_top(U32, top, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/fixed.res_opt(U32, gpow(a, e)))), ok) == True{} : Bool}
def saturating_pow source · line 279 · raw
@+a:U32 -> @+e:U32 -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/fixed.SaturatingPow.value(U32, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_val, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/fixed.u32_saturating_pow, 32n, a, e)
def overflowing_pow_flag source · line 282 · raw
@+a:U32 -> @+e:U32 -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/fixed.OverflowingPow.flag(U32, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_val, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/fixed.u32_overflowing_pow, 32n, a, e)
def lt_m source · line 287 · raw
@+mp:Nat -> @+hp:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.pow2(32n) == 1n+mp : Nat} -> @+x:U32 -> {Nat.is_lt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_val(x), 1n+mp) == True{} : Bool}
def mul_m source · line 290 · raw
@+mp:Nat -> @+hp:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.pow2(32n) == 1n+mp : Nat} -> @+x:U32 -> @+y:U32 -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_val(U32.mul(x, y)) == Nat.mod(Nat.mul(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_val(x), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_val(y)), 1n+mp) : Nat}
def wp_base source · line 293 · raw
@+mp:Nat -> @+hp:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.pow2(32n) == 1n+mp : Nat} -> @+e:U32 -> @+b:U32 -> @+acc:U32 -> @+h0:{vs(e) == 0n : Nat} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_val(acc) == Nat.mod(Nat.mul(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_val(acc), Nat.pow(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_val(b), vs(e))), 1n+mp) : Nat}
def wp_odd source · line 298 · raw
@+mp:Nat -> @+hp:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.pow2(32n) == 1n+mp : Nat} -> @+e:U32 -> @+b:U32 -> @+acc:U32 -> @+r:Nat -> @+hodd:{0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_odd(e) == Nat.is_eq(r, 1n) : Bool} -> @+hr:{Nat.is_lt(r, 2n) == True{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_val(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/fixed.pick(U32, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_odd(e), U32.mul(acc, b), acc)) == 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.pow_mod_odd(1n+mp, r, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_val(b), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_val(acc)) : Nat}
def half_e source · line 309 · raw
@+e:U32 -> {vs(U32.shr(e)) == Nat.div(vs(e), 2n) : Nat}
def wp_go source · line 312 · raw
@fuel:Nat -> @+mp:Nat -> @+hp:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.pow2(32n) == 1n+mp : Nat} -> @+e:U32 -> @+b:U32 -> @+acc:U32 -> @+z:Bool -> @+hz:{U32.is_zero(e) == z : Bool} -> @+he:{Nat.is_lt(vs(e), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.pow2(fuel)) == True{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_val(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/fixed.u32_wpow(fuel, e, b, acc, z)) == Nat.mod(Nat.mul(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_val(acc), Nat.pow(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_val(b), vs(e))), 1n+mp) : Nat}
def wp_top source · line 341 · raw
@+mp:Nat -> @+hp:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.pow2(32n) == 1n+mp : Nat} -> @+a:U32 -> @+e:U32 -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_val(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/fixed.u32_wrapping_pow(a, e)) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.low(32n, pw(a, e)) : Nat}
def wrapping_pow source · line 346 · raw
@+a:U32 -> @+e:U32 -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/fixed.WrappingPow.value(U32, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_val, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/fixed.u32_wrapping_pow, 32n, a, e)
def overflowing_pow_value source · line 349 · raw
@+a:U32 -> @+e:U32 -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/fixed.OverflowingPow.value(U32, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_val, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/fixed.u32_overflowing_pow, 32n, a, e)