proofs/math/proof.bend checks

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

18 imports

import Base
import ../../src/math/u64.bend as U
import ../../src/math/hash.bend as HS
import ../../src/math/pow2.bend as PW
import ../lib/lemmas/spec/numeric.bend as S
import ../lib/lemmas/types/model.bend as T
import ../../spec/lib/common.bend as SC
import ./pow2/pow2.bend as P2
import ./u64/u64.bend as P
import ./u64/u64div.bend as PD
import ../lib/u32div.bend as UD
import ./hash/hash.bend as PH
import ../lib/word.bend as WD
import ../lib/lemmas/proofs/word_addition.bend as WA
import ./natural/proof.bend as NT
import ../../spec/math/u64.bend as SU
import ../../spec/math/hash.bend as SH
import ../../spec/math/pow2.bend as SP

Definitions

def u32_div source · line 27 · raw

@+a:U32 -> @+b:U32 -> @+hb:{U32.is_zero(b) == False{} : Bool} -> {U32.to_nat(U32.div(a, b)) == Nat.div(U32.to_nat(a), U32.to_nat(b)) : Nat}

U32 long division (Base's U32.div / U32.mod), every nonzero divisor

def u32_mod source · line 30 · raw

@+a:U32 -> @+b:U32 -> @+hb:{U32.is_zero(b) == False{} : Bool} -> {U32.to_nat(U32.mod(a, b)) == Nat.mod(U32.to_nat(a), U32.to_nat(b)) : Nat}

def u64_is_zero source · line 34 · raw

@+a:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/u64.IsZero.value(a)

u64

def u64_le_signed source · line 37 · raw

@+a:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+b:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/u64.LeSigned.value(a, b)

def u64_add source · line 40 · raw

@+a:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+b:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/u64.Add.bits(a, b)

def u64_add_modular source · line 43 · raw

@+a:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+b:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/u64.Add.modular(a, b)

def u64_neg source · line 46 · raw

@+a:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/u64.Neg.bits(a)

def u64_div_small source · line 49 · raw

@+a:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+d:U32 -> @+hd0:{U32.is_zero(d) == False{} : Bool} -> @+hle:{U32.is_le(d, 1048576) == True{} : Bool} -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/u64.DivSmall.quotient(a, d, hd0, hle)

def u64_div_small_signed source · line 52 · raw

@+a:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+d:U32 -> @+hd0:{U32.is_zero(d) == False{} : Bool} -> @+hle:{U32.is_le(d, 1048576) == True{} : Bool} -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/u64.DivSmallSigned.quotient(a, d, hd0, hle)

def u64_milliseconds source · line 55 · raw

@+a:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> {0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/types/model.I64{0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/u64/u64.bits(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.div_small_signed(a, 1000000))} == 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/spec/numeric.milliseconds(0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/types/model.I64{0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/u64/u64.bits(a)}) : 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/types/model.Int64}

def hash_bucket_le source · line 59 · raw

@+w:U32 -> @+mask:U32 -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/hash.Bucket.le(w, mask)

hash

def hash_bucket_lt source · line 62 · raw

@+w:U32 -> @+k:Nat -> @+mask:U32 -> @+hm:{mask == U32{0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/word.mask(32n, k)} : U32} -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/hash.Bucket.lt(w, k, mask, hm)

def pow2 source · line 66 · raw

@+d:Nat -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/pow2.Pow2t.value(d)

pow2