~/bend-docscommunity

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)