proofs/math/typed/u32laws.bend checks

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

25 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 ../../lib/nat.bend as N
import ../../lib/u32.bend as U
import ../../lib/u32div.bend as UD
import ../../lib/u32half.bend as UH
import ../../lib/u32alg.bend as A
import ../../lib/word.bend as WD
import ../../lib/logic.bend as L
import ../../lib/lemmas/spec/numeric.bend as S
import ../u64/u64.bend as P64
import ./u32.bend as U32P
import ./width.bend as WW
import ../u64/u64div.bend as PD
import ../natural/arith.bend as NA
import ../../lib/arith.bend as AR
import ./w64mul.bend as W64M
import ./w64div.bend as W64D
import ./w64sqrt.bend as W64S
import ../../../src/math/w64.bend as X
import ../../../spec/math/w64.bend as SW

Definitions

def v source · line 33 · raw

@+x:U32 -> Nat

def vb_k source · line 38 · raw

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

def vb source · line 43 · raw

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

every U32 value fits 32 bits

def lt_k source · line 46 · raw

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

def vo_k source · line 50 · raw

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

def vo source · line 54 · raw

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

a value that fits is the value of its U32

def rt source · line 57 · raw

@+x:U32 -> {U32.from_nat(v(x)) == x : U32}

def true_ne_false source · line 62 · raw

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

def is_zero_c source · line 65 · raw

@+a:U32 -> @+c:Bool -> @+hc:{U32.is_zero(a) == c : Bool} -> @+n:Nat -> @+hn:{v(a) == n : Nat} -> {c == Nat.is_eq(v(a), 0n) : Bool}

def zero_nat source · line 80 · raw

@+a:U32 -> {U32.is_zero(a) == Nat.is_eq(v(a), 0n) : Bool}

U32.is_zero is the zero test on the value

def eq_c source · line 84 · raw

@+x:U32 -> @+y:U32 -> @+c:Bool -> @+hc:{U32.is_eq(x, y) == c : Bool} -> @+d:Bool -> @+hd:{Nat.is_eq(v(x), v(y)) == d : Bool} -> {c == d : Bool}

U32 equality is equality of the values

def eq_nat source · line 99 · raw

@+x:U32 -> @+y:U32 -> {U32.is_eq(x, y) == Nat.is_eq(v(x), v(y)) : Bool}

def carry_fits source · line 103 · raw

@+k:Nat -> @+s:Nat -> @+n:Nat -> @+c:Bool -> @+e:{Nat.add(s, 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/word.sc(k, 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/spec/numeric.bit_value(c))) == n : Nat} -> @+hs:{Nat.is_lt(s, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.pow2(k)) == True{} : Bool} -> {c == Bool.not(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(k, n)) : Bool}

the carry of an addition is "the sum does not fit"

def ops_zero source · line 122 · raw

0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/instances.Ops.zero(U32, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_op, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_val)

def ops_one source · line 125 · raw

0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/instances.Ops.one(U32, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_op, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_val)

def ops_abs source · line 128 · raw

@+a:U32 -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/instances.Ops.abs(U32, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_op, a)

def tests_lt source · line 131 · raw

@+a:U32 -> @+b:U32 -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/instances.Tests.lt(U32, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_is, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_val, a, b)

def tests_is_zero source · line 134 · raw

@+a:U32 -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/instances.Tests.is_zero(U32, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_is, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_val, a)

def ops_sub source · line 137 · 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/instances.Ops.sub(U32, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_op, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_val, a, b, h)

def nz source · line 140 · raw

@+b:U32 -> @+h:{Nat.is_eq(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_val(b), 0n) == False{} : Bool} -> {U32.is_zero(b) == False{} : Bool}

def ops_quot source · line 143 · raw

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

def ops_rem source · line 146 · raw

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

def hlf_div2 source · line 149 · raw

@+n:Nat -> {0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/u32half.hlf(n) == Nat.div(n, 2n) : Nat}

def ops_half source · line 159 · raw

@+a:U32 -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/instances.Ops.half(U32, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_op, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_val, a)

def carry_of source · line 162 · raw

@+a:U32 -> @+b:U32 -> @+h:{0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_is(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.AddOver{a, b}) == False{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/u64/u64.carry32(a, b) == False{} : Bool}

def ops_add source · line 165 · raw

@+a:U32 -> @+b:U32 -> @+h:{0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_is(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.AddOver{a, b}) == False{} : Bool} -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/instances.Ops.add(U32, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_op, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_is, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_val, a, b, h)

def add_over_k source · line 169 · raw

@+k:Nat -> @+hk:{k == 32n : Nat} -> @+a:U32 -> @+b:U32 -> {0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/u64/u64.carry32(a, b) == Bool.not(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(k, Nat.add(v(a), v(b)))) : Bool}

def tests_add_over source · line 173 · raw

@+a:U32 -> @+b:U32 -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/instances.Tests.add_over(U32, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_is, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_val, 32n, a, b)

def dbl source · line 179 · raw

@+h:Nat -> {Nat.mul(h, 2n) == Nat.double(h) : Nat}

def mod2_bit source · line 188 · raw

@+r:Nat -> @+h:Nat -> @+hr:{Nat.is_lt(r, 2n) == True{} : Bool} -> {r == Nat.mod(Nat.add(r, Nat.double(h)), 2n) : Nat}

r + 2h mod 2 is the bit r

def odd_val source · line 202 · raw

@+a:U32 -> {v(U32.and(a, 1)) == Nat.mod(v(a), 2n) : Nat}

def tests_odd source · line 207 · raw

@+a:U32 -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/instances.Tests.odd(U32, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_is, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_val, a)

def not_false source · line 214 · raw

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

def fits_split source · line 222 · raw

@+k:Nat -> @+lo:Nat -> @+hi:Nat -> @+hl:{Nat.is_lt(lo, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.pow2(k)) == True{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(k, Nat.add(lo, 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/word.sc(k, hi))) == Nat.is_eq(hi, 0n) : Bool}

fits(k, lo + 2^k hi) exactly when hi == 0 (lo < 2^k)

def hi_zero source · line 235 · raw

@+a:U32 -> @+b:U32 -> @+h:{0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_is(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.MulOver{a, b}) == False{} : Bool} -> {v(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.hi(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.mul32(a, b))) == 0n : Nat}

def prod_limbs source · line 240 · raw

@+a:U32 -> @+b:U32 -> {Nat.add(v(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.lo(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.mul32(a, b))), 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/word.sc(32n, v(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.hi(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.mul32(a, b))))) == Nat.mul(v(a), v(b)) : Nat}

the product value as the two limbs of the full product

def ops_mul_one source · line 246 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+a:U32 -> @+b:U32 -> @+h:{0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_is(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.MulOver{a, b}) == False{} : Bool} -> {v(U32.mul(a, b)) == Nat.mul(v(a), v(b)) : Nat}

def ops_mul source · line 254 · raw

@+a:U32 -> @+b:U32 -> @+h:{0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_is(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.MulOver{a, b}) == False{} : Bool} -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/instances.Ops.mul(U32, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_op, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_is, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_val, a, b, h)

def mul_over_k source · line 257 · raw

@+k:Nat -> @+hk:{k == 32n : Nat} -> @+a:U32 -> @+b:U32 -> {U32.is_zero(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.hi(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.mul32(a, b))) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(k, Nat.mul(v(a), v(b))) : Bool}

def tests_mul_over source · line 265 · raw

@+a:U32 -> @+b:U32 -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/instances.Tests.mul_over(U32, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_is, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_val, 32n, a, b)

def pos_nz source · line 270 · raw

@+x:Nat -> @+y:Nat -> @+h:{Nat.is_lt(x, y) == True{} : Bool} -> {Nat.is_eq(y, 0n) == False{} : Bool}

def ops_mulmod source · line 277 · raw

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

def pw_table source · line 284 · raw

@+k:Nat -> @+hk:{Nat.is_lt(k, 32n) == True{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.pow2(k) == U32{0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/word.pw(32n, k)} : U32}

def ops_pow2 source · line 353 · raw

@+k:Nat -> @+hk:{Nat.is_lt(k, 32n) == True{} : Bool} -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/instances.Ops.pow2(U32, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_op, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_val, 32n, k, hk)

def ops_sqrt source · line 360 · raw

@+a:U32 -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/instances.Ops.sqrt(U32, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/instances.u32_op, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_val, a)