proofs/math/random/proof_pcg.bend checks

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

17 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 ../../../spec/math/random.bend as SRM
import ../../../src/math/u64.bend as WU
import ../../../src/math/w64.bend as X
import ../../../src/math/random/pcg.bend as P
import ../../lib/lemmas/proofs/nat_algebra.bend as NA
import ../typed/width.bend as WW
import ../typed/w64add.bend as WA
import ../typed/w64sh.bend as SH
import ./pcg/xor.bend as XO
import ../../lib/lemmas/spec/numeric.bend as S
import ../typed/w64m128.bend as M128
import ./pcg/step.bend as ST
import ./pcg/impl.bend as IM

Definitions

def PCG.step source · line 31 · raw

@+mh:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+ml:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+ih:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+il:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+p:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/random/pcg.PCG -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/random.PCG.step(mh, ml, ih, il, p)

def PCG.constants source · line 36 · raw

@+p:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/random/pcg.PCG -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/random.PCG.constants(p)

def v source · line 39 · raw

@+x:U32 -> Nat

def xs source · line 43 · raw

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

x ^ (x >> k)

def plus1 source · line 48 · raw

@+x:Nat -> {Nat.add(x, 1n) == 1n+x : Nat}

def or_value source · line 52 · raw

@+lo:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{U32.or(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.lo(lo), 1), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.hi(lo)}) == Nat.add(Nat.double(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.half(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(lo))), 1n) : Nat}

lo | 1

def mulg source · line 68 · raw

@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+o:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+xv:Nat -> @+hx:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(x) == xv : Nat} -> @+ov:Nat -> @+ho:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(o) == ov : Nat} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.mul(x, o)) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.low(64n, Nat.mul(xv, ov)) : Nat}

the value of a product mod 2^64 from the values of its factors; the factors stay variables here, so no product is ever normalized

def xs32 source · line 74 · raw

@+h:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/random/pcg.xor64(h, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.shr(h, 32n))) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/random/pcg.xor_bits(64n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(h), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.high(32n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(h))) : Nat}

def xs48 source · line 77 · raw

@+h:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/random/pcg.xor64(h, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.shr(h, 48n))) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/random/pcg.xor_bits(64n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(h), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.high(48n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(h))) : Nat}

def xt source · line 81 · raw

@+H:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+t:Nat -> @+ht:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(H) == t : Nat} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/random/pcg.xor64(H, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.shr(H, 48n))) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/random/pcg.xor_bits(64n, t, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.high(48n, t)) : Nat}

x ^ (x >> 48) for a word of value t

def half1 source · line 86 · raw

@+cm:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+hi:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+t:Nat -> @+ht:{t == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/random/pcg.dxsm1(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(cm), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(hi)) : Nat} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.mul(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/random/pcg.xor64(hi, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.shr(hi, 32n)), cm)) == t : Nat}

the first half's value is t

def PCG.output source · line 93 · raw

@+cm:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+hi:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+lo:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+t:Nat -> @+ht:{t == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/random/pcg.dxsm1(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(cm), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(hi)) : Nat} -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/random.PCG.output(cm, hi, lo, t, ht)

THEOREM (PCG.output) values are known (x ^ x >> 48 with x of value t, and lo | 1)