~/bend-docscommunity

proofs/math/typed/u64laws.bend checks

raw source on the hub · import bend-collections-laws-math@1.0.0.0/proofs/math/typed/u64laws.bend as U64laws

18 imports
import Base
import ../../../spec/lib/common.bend as C
import ../../../spec/math/instances.bend as SI
import ../../../spec/math/generic.bend as SG
import ../../../src/math/instances.bend as I
import ../../../src/math/num.bend as NM
import ../../../src/math/w64.bend as X
import ../../../src/math/u64.bend as WU
import ../../lib/nat.bend as N
import ../../lib/logic.bend as L
import ./width.bend as WW
import ./u32laws.bend as LW
import ./w64add.bend as WA
import ./w64dmtop.bend as DT
import ./w64dmrem.bend as DR
import ./w64mmtop.bend as MMT
import ./w64isq.bend as ISQ
import ./w64sh.bend as SH

Definitions

def v source · line 24 · raw

@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> Nat

def true_ne_false source · line 27 · raw

@+h:{True{} == False{} : Bool} -> Empty

def vb source · line 30 · raw

@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(64n, v(x)) == True{} : Bool}

def val_lt source · line 35 · raw

@+K:Nat -> @+hK:{K == 64n : Nat} -> @+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> {Nat.is_lt(v(x), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.pow2(K)) == True{} : Bool}

def rt source · line 38 · raw

@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u64_of(v(x)) == x : 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64}

def vo source · line 47 · raw

@+n:Nat -> @+h:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(64n, n) == True{} : Bool} -> {v(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u64_of(n)) == n : Nat}

def ops_zero source · line 56 · raw

0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/instances.Ops.zero(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u64_op, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u64_val)

def ops_one source · line 59 · raw

0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/instances.Ops.one(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u64_op, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u64_val)

def ops_abs source · line 62 · raw

@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/instances.Ops.abs(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u64_op, x)

def tests_lt source · line 65 · raw

@+a:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+b:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/instances.Tests.lt(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u64_is, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u64_val, a, b)

def tests_is_zero source · line 68 · raw

@+a:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/instances.Tests.is_zero(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u64_is, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u64_val, a)

def tests_odd source · line 71 · raw

@+a:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/instances.Tests.odd(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u64_is, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u64_val, a)

def tests_add_over source · line 74 · raw

@+a:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+b:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/instances.Tests.add_over(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u64_is, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u64_val, 64n, a, b)

def tests_mul_over source · line 77 · raw

@+a:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+b:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/instances.Tests.mul_over(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u64_is, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u64_val, 64n, a, b)

def ops_sub source · line 80 · raw

@+a:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+b:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+h:{Nat.is_le(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u64_val(b), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u64_val(a)) == True{} : Bool} -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/instances.Ops.sub(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u64_op, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u64_val, a, b, h)

def ops_half source · line 83 · raw

@+a:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/instances.Ops.half(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u64_op, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u64_val, a)

def nzb source · line 86 · raw

@+b:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+h:{Nat.is_eq(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u64_val(b), 0n) == False{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.is_zero(b) == False{} : Bool}

def ops_quot source · line 89 · raw

@+a:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+b:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+h:{Nat.is_eq(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u64_val(b), 0n) == False{} : Bool} -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/instances.Ops.quot(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u64_op, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u64_val, a, b, h)

def ops_rem source · line 92 · raw

@+a:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+b:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+h:{Nat.is_eq(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u64_val(b), 0n) == False{} : Bool} -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/instances.Ops.rem(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u64_op, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u64_val, a, b, h)

def not_f source · line 95 · raw

@+x:Bool -> @+h:{Bool.not(x) == False{} : Bool} -> {x == True{} : Bool}

def ops_add source · line 102 · raw

@+a:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+b:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+h:{0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u64_is(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.AddOver{a, b}) == False{} : Bool} -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/instances.Ops.add(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u64_op, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u64_is, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u64_val, a, b, h)

def ops_mul source · line 106 · raw

@+a:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+b:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+h:{0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u64_is(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.MulOver{a, b}) == False{} : Bool} -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/instances.Ops.mul(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u64_op, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u64_is, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u64_val, a, b, h)

def ops_mulmod source · line 110 · raw

@+a:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+b:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+m:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+ha:{Nat.is_lt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u64_val(a), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u64_val(m)) == True{} : Bool} -> @+hb:{Nat.is_lt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u64_val(b), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u64_val(m)) == True{} : Bool} -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/instances.Ops.mulmod(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u64_op, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u64_val, a, b, m, ha, hb)

def ops_sqrt source · line 113 · raw

@+a:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/instances.Ops.sqrt(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u64_op, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u64_val, a)

def pow2_c source · line 116 · raw

@+k:Nat -> @+hk:{Nat.is_lt(k, 64n) == True{} : Bool} -> @+c:Bool -> @+hc:{Nat.is_lt(k, 32n) == c : Bool} -> {v(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.w_pow2(k, c)) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.pow2(k) : Nat}

def ops_pow2 source · line 127 · raw

@+k:Nat -> @+hk:{Nat.is_lt(k, 64n) == True{} : Bool} -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/instances.Ops.pow2(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u64_op, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u64_val, 64n, k, hk)