~/bend-docscommunity

proofs/math/number/proof.bend checks

raw source on the hub · import bend-collections-laws-math@1.0.0.0/proofs/math/number/proof.bend as Proof

15 imports
import Base
import ../../../spec/lib/common.bend as C
import ../../../spec/math/generic.bend as SG
import ../../../spec/math/number.bend as SN
import ../../../spec/math/fixed.bend as SF
import ../../../src/math/u64.bend as WU
import ../../../src/math/fixed.bend as F
import ./egcd.bend as EG
import ./bitcount.bend as BC
import ./prime.bend as PR
import ./fixprime.bend as FP
import ../typed/fix32.bend as P32
import ../typed/fix64.bend as P64
import ../typed/fixbits.bend as FBI
import ../typed/fixbytes.bend as FBY

Definitions

def bit_count source · line 28 · raw

@+n:Nat -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/number.BitCount.value(n)

def egcd_gcd source · line 31 · raw

@+a:Nat -> @+b:Nat -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/number.Egcd.gcd(a, b)

def egcd_bezout source · line 34 · raw

@+a:Nat -> @+b:Nat -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/number.Egcd.bezout(a, b)

def is_prime source · line 37 · raw

@+n:Nat -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/number.IsPrime.value(n)

def u32_checked_add source · line 42 · 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 u32_checked_sub source · line 45 · 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 u32_checked_mul source · line 48 · 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 u32_checked_div source · line 51 · 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 u32_checked_rem source · line 54 · 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 u32_checked_pow source · line 57 · 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 u32_checked_shl source · line 60 · 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 u32_checked_shr source · line 63 · 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 u32_wrapping_add source · line 66 · 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 u32_wrapping_sub source · line 69 · 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 u32_wrapping_mul source · line 72 · 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 u32_wrapping_pow source · line 75 · 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 u32_wrapping_shl source · line 78 · 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 u32_wrapping_shr source · line 81 · 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 u32_saturating_add source · line 84 · 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 u32_saturating_sub source · line 87 · 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 u32_saturating_mul source · line 90 · 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 u32_saturating_pow source · line 93 · 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 u32_overflowing_add_value source · line 96 · 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 u32_overflowing_add_flag source · line 99 · 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 u32_overflowing_sub_value source · line 102 · 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 u32_overflowing_sub_flag source · line 105 · 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 u32_overflowing_mul_value source · line 108 · 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 u32_overflowing_mul_flag source · line 111 · 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 u32_overflowing_pow_value source · line 114 · 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)

def u32_overflowing_pow_flag source · line 117 · 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 u32_overflowing_shl_value source · line 120 · 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 u32_overflowing_shl_flag source · line 123 · raw

@+a:U32 -> @+s:U32 -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/fixed.OverflowingShl.flag(U32, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/fixed.u32_overflowing_shl, a, s, 32n)

def u32_overflowing_shr_value source · line 126 · 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 u32_overflowing_shr_flag source · line 129 · raw

@+a:U32 -> @+s:U32 -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/fixed.OverflowingShr.flag(U32, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/fixed.u32_overflowing_shr, a, s, 32n)

def u32_bit_count source · line 132 · raw

@+a:U32 -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/fixed.BitCount.value(U32, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_val, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/fixed.u32_bit_count, 32n, a)

def u32_to_bytes_le source · line 135 · raw

@+a:U32 -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/fixed.ToBytes.le(U32, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_val, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/fixed.u32_to_bytes_le, 4n, a)

def u32_to_bytes_be source · line 138 · raw

@+a:U32 -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/fixed.ToBytes.be(U32, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_val, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/fixed.u32_to_bytes_be, 4n, a)

def u32_from_bytes_le source · line 141 · raw

@bs:List<&2, U32> -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/fixed.FromBytes.le(U32, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_val, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/fixed.u32_from_bytes_le, 4n, bs)

def u32_from_bytes_be source · line 144 · raw

@bs:List<&2, U32> -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/fixed.FromBytes.be(U32, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_val, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/fixed.u32_from_bytes_be, 4n, bs)

def u32_is_prime source · line 147 · raw

@+a:U32 -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/fixed.IsPrime.value(a)

def u32_next_prime_found source · line 150 · raw

@+n:U32 -> @+p:U32 -> @+h:{0xf86f5f1d9a594d5a5cff999100e01d03/src/math/fixed.u32_next_prime(n) == Some{p} : Maybe<&2, U32>} -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/fixed.NextPrime.found(n, p, h)

def u32_next_prime_none source · line 153 · raw

@+n:U32 -> @+h:{0xf86f5f1d9a594d5a5cff999100e01d03/src/math/fixed.u32_next_prime(n) == None{} : Maybe<&2, U32>} -> @+m:Nat -> @+hm:{Nat.is_lt(U32.to_nat(n), m) == True{} : Bool} -> @+hf:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(32n, m) == True{} : Bool} -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/fixed.NextPrime.none(n, h, m, hm, hf)

def u64_checked_add source · line 158 · raw

@+a:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+b:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/fixed.CheckedAdd.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u64_val, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/fixed.u64_checked_add, 64n, a, b)

def u64_checked_sub source · line 161 · raw

@+a:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+b:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/fixed.CheckedSub.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u64_val, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/fixed.u64_checked_sub, a, b)

def u64_checked_mul source · line 164 · raw

@+a:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+b:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/fixed.CheckedMul.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u64_val, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/fixed.u64_checked_mul, 64n, a, b)

def u64_checked_div source · line 167 · raw

@+a:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+b:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/fixed.CheckedDiv.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u64_val, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/fixed.u64_checked_div, a, b)

def u64_checked_rem source · line 170 · raw

@+a:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+b:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/fixed.CheckedRem.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u64_val, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/fixed.u64_checked_rem, a, b)

def u64_checked_pow source · line 173 · raw

@+a:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+e:U32 -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/fixed.CheckedPow.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u64_val, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/fixed.u64_checked_pow, 64n, a, e)

def u64_checked_shl source · line 176 · raw

@+a:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+s:U32 -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/fixed.CheckedShl.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u64_val, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/fixed.u64_checked_shl, 64n, a, s)

def u64_checked_shr source · line 179 · raw

@+a:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+s:U32 -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/fixed.CheckedShr.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u64_val, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/fixed.u64_checked_shr, 64n, a, s)

def u64_wrapping_add source · line 182 · raw

@+a:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+b:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/fixed.WrappingAdd.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u64_val, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/fixed.u64_wrapping_add, 64n, a, b)

def u64_wrapping_sub source · line 185 · raw

@+a:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+b:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/fixed.WrappingSub.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u64_val, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/fixed.u64_wrapping_sub, 64n, a, b)

def u64_wrapping_mul source · line 188 · raw

@+a:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+b:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/fixed.WrappingMul.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u64_val, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/fixed.u64_wrapping_mul, 64n, a, b)

def u64_wrapping_pow source · line 191 · raw

@+a:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+e:U32 -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/fixed.WrappingPow.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u64_val, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/fixed.u64_wrapping_pow, 64n, a, e)

def u64_wrapping_shl source · line 194 · raw

@+a:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+s:U32 -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/fixed.WrappingShl.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u64_val, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/fixed.u64_wrapping_shl, 64n, a, s)

def u64_wrapping_shr source · line 197 · raw

@+a:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+s:U32 -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/fixed.WrappingShr.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u64_val, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/fixed.u64_wrapping_shr, 64n, a, s)

def u64_saturating_add source · line 200 · raw

@+a:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+b:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/fixed.SaturatingAdd.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u64_val, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/fixed.u64_saturating_add, 64n, a, b)

def u64_saturating_sub source · line 203 · raw

@+a:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+b:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/fixed.SaturatingSub.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u64_val, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/fixed.u64_saturating_sub, a, b)

def u64_saturating_mul source · line 206 · raw

@+a:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+b:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/fixed.SaturatingMul.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u64_val, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/fixed.u64_saturating_mul, 64n, a, b)

def u64_saturating_pow source · line 209 · raw

@+a:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+e:U32 -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/fixed.SaturatingPow.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u64_val, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/fixed.u64_saturating_pow, 64n, a, e)

def u64_overflowing_add_value source · line 212 · raw

@+a:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+b:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/fixed.OverflowingAdd.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u64_val, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/fixed.u64_overflowing_add, 64n, a, b)

def u64_overflowing_add_flag source · line 215 · raw

@+a:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+b:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/fixed.OverflowingAdd.flag(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u64_val, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/fixed.u64_overflowing_add, 64n, a, b)

def u64_overflowing_sub_value source · line 218 · raw

@+a:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+b:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/fixed.OverflowingSub.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u64_val, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/fixed.u64_overflowing_sub, 64n, a, b)

def u64_overflowing_sub_flag source · line 221 · raw

@+a:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+b:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/fixed.OverflowingSub.flag(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u64_val, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/fixed.u64_overflowing_sub, a, b)

def u64_overflowing_mul_value source · line 224 · raw

@+a:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+b:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/fixed.OverflowingMul.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u64_val, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/fixed.u64_overflowing_mul, 64n, a, b)

def u64_overflowing_mul_flag source · line 227 · raw

@+a:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+b:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/fixed.OverflowingMul.flag(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u64_val, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/fixed.u64_overflowing_mul, 64n, a, b)

def u64_overflowing_pow_value source · line 230 · raw

@+a:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+e:U32 -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/fixed.OverflowingPow.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u64_val, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/fixed.u64_overflowing_pow, 64n, a, e)

def u64_overflowing_pow_flag source · line 233 · raw

@+a:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+e:U32 -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/fixed.OverflowingPow.flag(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u64_val, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/fixed.u64_overflowing_pow, 64n, a, e)

def u64_overflowing_shl_value source · line 236 · raw

@+a:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+s:U32 -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/fixed.OverflowingShl.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u64_val, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/fixed.u64_overflowing_shl, 64n, a, s)

def u64_overflowing_shl_flag source · line 239 · raw

@+a:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+s:U32 -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/fixed.OverflowingShl.flag(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/fixed.u64_overflowing_shl, a, s, 64n)

def u64_overflowing_shr_value source · line 242 · raw

@+a:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+s:U32 -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/fixed.OverflowingShr.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u64_val, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/fixed.u64_overflowing_shr, 64n, a, s)

def u64_overflowing_shr_flag source · line 245 · raw

@+a:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+s:U32 -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/fixed.OverflowingShr.flag(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/fixed.u64_overflowing_shr, a, s, 64n)

def u64_bit_count source · line 248 · raw

@+a:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/fixed.BitCount.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u64_val, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/fixed.u64_bit_count, 64n, a)

def u64_to_bytes_le source · line 251 · raw

@+a:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/fixed.ToBytes.le(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u64_val, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/fixed.u64_to_bytes_le, 8n, a)

def u64_to_bytes_be source · line 254 · raw

@+a:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/fixed.ToBytes.be(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u64_val, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/fixed.u64_to_bytes_be, 8n, a)

def u64_from_bytes_le source · line 257 · raw

@bs:List<&2, U32> -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/fixed.FromBytes.le(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u64_val, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/fixed.u64_from_bytes_le, 8n, bs)

def u64_from_bytes_be source · line 260 · raw

@bs:List<&2, U32> -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/fixed.FromBytes.be(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u64_val, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/fixed.u64_from_bytes_be, 8n, bs)