~/bend-docscommunity

proofs/math/typed/w64m128.bend checks

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

15 imports
import Base
import ../../../spec/lib/common.bend as C
import ../../../spec/math/w64.bend as SW
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 ../../lib/lemmas/proofs/nat_algebra.bend as NA
import ../../lib/word.bend as WD
import ../../lib/lemmas/spec/numeric.bend as S
import ../u64/u64.bend as P64
import ./w64mul.bend as W64M
import ./w64add.bend as WA
import ./width.bend as WW
import ./u32laws.bend as LW

Definitions

def v source · line 21 · raw

@+x:U32 -> Nat

def vb source · line 24 · raw

@+x:U32 -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(32n, v(x)) == True{} : Bool}

def fit64 source · line 27 · raw

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

def true_ne_false source · line 32 · raw

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

def sum_fits source · line 36 · raw

@+k:Nat -> @+x:Nat -> @+y:Nat -> @+hx:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(k, x) == True{} : Bool} -> @+hy:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(k, y) == True{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(1n+k, Nat.add(x, y)) == True{} : Bool}

x, y fit k bits: x + y fits 1 + k bits

def bit_nz source · line 42 · raw

@+h:Nat -> @+hf:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(1n, h) == True{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/spec/numeric.bit_value(Bool.not(Nat.is_eq(h, 0n))) == h : Nat}

a value below 2 is the bit "is nonzero"

def fits_hi source · line 51 · raw

@+s:Nat -> @+h:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(65n, s) == True{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(1n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.high(64n, s)) == True{} : Bool}

def add_split source · line 55 · raw

@+p:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+q:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> {Nat.add(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(p), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(q)) == Nat.add(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.add(p, q)), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(64n, 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/spec/numeric.bit_value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.add_over(p, q)))) : Nat}

the sum of two 64-bit values: low 64 bits + 2^64 * the overflow bit

def add64_exact source · line 65 · raw

@+p:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+q:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+hf:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(64n, Nat.add(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(p), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(q))) == True{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.add(p, q)) == Nat.add(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(p), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(q)) : Nat}

a 64-bit sum that fits: no wrap

def m128_alg source · line 69 · raw

@+A:Nat -> @+t1:Nat -> @+t2:Nat -> @+hh:Nat -> @+lo00:Nat -> @+hi00:Nat -> @+vm:Nat -> @+lomid:Nat -> @+himid:Nat -> @+c1v:Nat -> @+s:Nat -> @+c2v:Nat -> @+ea:{A == Nat.add(lo00, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(32n, hi00)) : Nat} -> @+et:{Nat.add(t1, t2) == Nat.add(vm, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(32n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(32n, c1v))) : Nat} -> @+em:{vm == Nat.add(lomid, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(32n, himid)) : Nat} -> @+es:{Nat.add(s, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(32n, c2v)) == Nat.add(hi00, lomid) : Nat} -> {Nat.add(Nat.add(A, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(32n, t1)), Nat.add(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(32n, t2), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(32n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(32n, hh)))) == Nat.add(Nat.add(lo00, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(32n, s)), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(32n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(32n, Nat.add(Nat.add(hh, Nat.add(himid, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(32n, c1v))), c2v)))) : Nat}

def fits_lek source · line 72 · raw

@+k:Nat -> @+x:Nat -> @+y:Nat -> @+h:{Nat.is_le(x, y) == True{} : Bool} -> @+hy:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(k, y) == True{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(k, x) == True{} : Bool}

def fits_hk source · line 75 · raw

@+k:Nat -> @+s:Nat -> @+h:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(Nat.add(k, k), s) == True{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(k, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.high(k, s)) == True{} : Bool}

def val0 source · line 78 · raw

@+x:U32 -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{x, 0}) == v(x) : Nat}

def m128_value source · line 82 · raw

@+al:U32 -> @+ah:U32 -> @+bl:U32 -> @+bh:U32 -> {Nat.add(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.pfst(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.mul128(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{al, ah}, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{bl, bh}))), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(64n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.psnd(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.mul128(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{al, ah}, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{bl, bh}))))) == Nat.mul(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{al, ah}), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{bl, bh})) : Nat}

the 128-bit product: low 64 bits + 2^64 * high 64 bits

def QSUB source · line 105 · raw

@+one:Nat -> @+a:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+b:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> Nat

a - b wraps: (a - b mod 2^64) + b == a + 2^64 * qs

def sub_eq source · line 110 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+a:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+b:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> {Nat.add(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.sub(a, b)), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(b)) == Nat.add(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(a), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(64n, QSUB(one, a, b))) : Nat}