~/bend-docscommunity

proofs/math/typed/fixbits.bend checks

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

14 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 ../../../spec/math/number.bend as SN
import ../../../src/math/u64.bend as WU
import ../../../src/math/fixed.bend as F
import ../../lib/nat.bend as N
import ../../lib/u32div.bend as UD
import ../natural/arith.bend as R
import ./width.bend as WW
import ./shrn.bend as SHN
import ./u32laws.bend as LW
import ./fixgen.bend as G

Definitions

def bit_bit source · line 23 · raw

@+n:Nat -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.bit(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.bit(n)) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.bit(n) : Nat}

def half_bit source · line 32 · raw

@+n:Nat -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.half(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.bit(n)) == 0n : Nat}

def ones_low source · line 42 · raw

@+a:Nat -> @+n:Nat -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/number.ones(a, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.low(a, n)) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/number.ones(a, n) : Nat}

only the a low bits count

def ones_add source · line 54 · raw

@+a:Nat -> @+b:Nat -> @+n:Nat -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/number.ones(Nat.add(a, b), n) == Nat.add(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/number.ones(a, n), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/number.ones(b, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.high(a, n))) : Nat}

def ones4_eq source · line 64 · raw

@+n:Nat -> @+h:{Nat.is_lt(n, 16n) == True{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/fixed.ones4(n) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/number.ones(4n, n) : Nat}

def nib_low source · line 101 · raw

@+x:U32 -> {U32.to_nat(U32.mod(x, 16)) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.low(4n, U32.to_nat(x)) : Nat}

def nib_ones source · line 104 · raw

@+x:U32 -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/fixed.ones4(U32.to_nat(U32.mod(x, 16))) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/number.ones(4n, U32.to_nat(x)) : Nat}

def q4 source · line 109 · raw

@k:Nat -> Nat

4 k

def bc_go source · line 116 · raw

@+k:Nat -> @+x:U32 -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/fixed.u32_bc_go(k, x) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/number.ones(q4(k), U32.to_nat(x)) : Nat}

def u32_bit_count source · line 127 · 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 u64_bit_count source · line 132 · 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)