proofs/math/random/bits.bend checks

raw source on the hub · import bend-collections-laws-math@1.0.0.0/proofs/math/random/bits.bend as Bits

11 imports

import Base
import ../../../spec/lib/common.bend as C
import ../../../spec/math/w64.bend as SW
import ../../../spec/math/random/rand.bend as SR
import ../../../src/math/u64.bend as WU
import ../../../src/math/w64.bend as X
import ../../../src/math/random/rand.bend as R
import ../../lib/nat.bend as N
import ../../lib/logic.bend as L
import ../typed/width.bend as WI
import ../typed/w64add.bend as WA

Definitions

def bv source · line 16 · raw

@b:Bool -> Nat

def and_step source · line 24 · raw

@+p:Nat -> @+b:Nat -> @+a:Nat -> @+c:Nat -> @+d:Nat -> @+hb:{Nat.is_le(b, 1n) == True{} : Bool} -> @+hc:{Nat.is_le(c, 1n) == True{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/random/rand.and_bits(1n+p, Nat.add(b, Nat.double(a)), Nat.add(c, Nat.double(d))) == Nat.add(Nat.mul(b, c), Nat.double(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/random/rand.and_bits(p, a, d))) : Nat}

one bit and the rest: (b + 2a) & (c + 2d) = b c + 2 (a & d)

def bv_le source · line 53 · raw

@+b:Bool -> {Nat.is_le(bv(b), 1n) == True{} : Bool}

def bv_and source · line 60 · raw

@+x:Bool -> @+y:Bool -> {bv(Bool.and(x, y)) == Nat.mul(bv(x), bv(y)) : Nat}

def to_nat_con source · line 70 · raw

@+p:Nat -> @+x:Bool -> @+t:Word(p) -> {Word.to_nat(1n+p, WCon{x, t}) == Nat.add(bv(x), Nat.double(Word.to_nat(p, t))) : Nat}

a word's value, its low bit first

def wand source · line 78 · raw

@+n:Nat -> @+a:Word(n) -> @+b:Word(n) -> {Word.to_nat(n, Word.and(n, a, b)) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/random/rand.and_bits(n, Word.to_nat(n, a), Word.to_nat(n, b)) : Nat}

THEOREM: Word.and is and_bits on the values

def uand source · line 93 · raw

@+x:U32 -> @+y:U32 -> {U32.to_nat(U32.and(x, y)) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/random/rand.and_bits(32n, U32.to_nat(x), U32.to_nat(y)) : Nat}

def and_join source · line 99 · raw

@+k:Nat -> @+j:Nat -> @+a1:Nat -> @+b1:Nat -> @+a2:Nat -> @+b2:Nat -> @+h1:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(k, a1) == True{} : Bool} -> @+h2:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(k, a2) == True{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/random/rand.and_bits(Nat.add(k, j), Nat.add(a1, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(k, b1)), Nat.add(a2, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(k, b2))) == Nat.add(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/random/rand.and_bits(k, a1, a2), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(k, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/random/rand.and_bits(j, b1, b2))) : Nat}

THEOREM: and on two limbs, (a1 + 2^k b1) & (a2 + 2^k b2) = a1 & a2 + 2^k (b1 & b2)

def and64_value source · line 120 · raw

@+a:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+b:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/random/rand.and64(a, b)) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/random/rand.and_bits(64n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(a), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(b)) : Nat}

THEOREM: the 64-bit and of rand.bend is and_bits on the values