~/bend-docscommunity

proofs/math/random/pcg/xor.bend checks

raw source on the hub · import bend-collections-laws-math@1.0.0.0/proofs/math/random/pcg/xor.bend as Xor

13 imports
import Base
import ../../../../spec/lib/common.bend as C
import ../../../../spec/math/w64.bend as SW
import ../../../../spec/math/random/pcg.bend as SP
import ../../../../src/math/u64.bend as WU
import ../../../../src/math/random/pcg.bend as P
import ../../../lib/lemmas/spec/numeric.bend as S
import ../../../lib/lemmas/proofs/nat_algebra.bend as NA
import ../../../lib/word.bend as WD
import ../../../lib/u32div.bend as UD
import ../../../lib/logic.bend as L
import ../../typed/width.bend as WW
import ../../typed/w64sh.bend as SH

Definitions

def v source · line 19 · raw

@+x:U32 -> Nat

def bit_bvd source · line 23 · raw

@+b:Bool -> @+u:Nat -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.bit(Nat.add(0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/spec/numeric.bit_value(b), Nat.double(u))) == 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/spec/numeric.bit_value(b) : Nat}

the low bit and the rest of bv(b) + 2 u

def xbit source · line 30 · raw

@+a:Bool -> @+b:Bool -> {0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/spec/numeric.bit_value(Bool.xor(a, b)) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/random/pcg.b2n(Bool.not(Nat.is_eq(0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/spec/numeric.bit_value(a), 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/spec/numeric.bit_value(b)))) : Nat}

def step_eq source · line 42 · raw

@+p:Nat -> @+ba:Bool -> @+ua:Nat -> @+bb:Bool -> @+ub:Nat -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/random/pcg.xor_bits(1n+p, Nat.add(0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/spec/numeric.bit_value(ba), Nat.double(ua)), Nat.add(0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/spec/numeric.bit_value(bb), Nat.double(ub))) == Nat.add(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/random/pcg.b2n(Bool.not(Nat.is_eq(0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/spec/numeric.bit_value(ba), 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/spec/numeric.bit_value(bb)))), Nat.double(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/random/pcg.xor_bits(p, ua, ub))) : Nat}

one step of xor_bits on two values written bit + 2 rest

def xor_word source · line 52 · raw

@+n:Nat -> @+x:Word(n) -> @+y:Word(n) -> {0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/word.uw(n, Word.xor(n, x, y)) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/random/pcg.xor_bits(n, 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/word.uw(n, x), 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/word.uw(n, y)) : Nat}

the value of a word xor is xor_bits of the values

def xor32 source · line 64 · raw

@+x:U32 -> @+y:U32 -> {v(U32.xor(x, y)) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/random/pcg.xor_bits(32n, v(x), v(y)) : Nat}

def fits0 source · line 71 · raw

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

def xsplit source · line 79 · raw

@+k:Nat -> @+j:Nat -> @+al:Nat -> @+ah:Nat -> @+bl:Nat -> @+bh:Nat -> @+ha:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(k, al) == True{} : Bool} -> @+hb:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(k, bl) == True{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/random/pcg.xor_bits(Nat.add(k, j), Nat.add(al, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(k, ah)), Nat.add(bl, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(k, bh))) == Nat.add(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/random/pcg.xor_bits(k, al, bl), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(k, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/random/pcg.xor_bits(j, ah, bh))) : Nat}

xor_bits splits at bit k when the low parts fit k bits

def xor64_value source · line 100 · raw

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

THEOREM: the value of xor64 is xor_bits(64) of the values