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

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

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 ../../../../src/math/u64.bend as WU
import ../../../../src/math/w64.bend as X
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/u32alg.bend as A
import ../../typed/width.bend as WW
import ../../typed/w64add.bend as WA
import ../../typed/w64m128.bend as M128
import ../../typed/w64mul.bend as W64M
import ../../typed/w64sh.bend as SH
import ./step.bend as ST
import ../../../../spec/math/random.bend as SR

Definitions

def eqm_of source · line 22 · raw

@+v:Nat -> @+x:Nat -> @+e:{v == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.low(64n, x) : Nat} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.low(64n, v) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.low(64n, x) : Nat}

def v source · line 27 · raw

@+x:U32 -> Nat

def carry_value source · line 30 · raw

@+c:Bool -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.b32(c), 0}) == 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/spec/numeric.bit_value(c) : Nat}

def fT source · line 34 · raw

@+hi:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+lo:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+ml:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+mh:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.low(64n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.add(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.mul(hi, ml), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.mul(lo, mh)))) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.low(64n, Nat.add(Nat.mul(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(hi), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(ml)), Nat.mul(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(lo), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(mh)))) : Nat}

the cross products mod 2^64

def fS source · line 42 · raw

@+a:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+b:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.low(64n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.add(a, b))) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.low(64n, Nat.add(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(a), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(b))) : Nat}

a sum mod 2^64

def fV source · line 46 · raw

@+a:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+cb:Bool -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.add(a, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.b32(cb), 0})) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.low(64n, Nat.add(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(a), 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/spec/numeric.bit_value(cb))) : Nat}

adding the carry

def step_pair source · line 53 · 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 -> @+hi:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+lo:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @pr:Pair(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64) -> @+h1:{Nat.add(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.pfst(pr)), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(64n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.psnd(pr)))) == Nat.mul(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(lo), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(ml)) : Nat} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/random.value128(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/random/pcg.step_mul(mh, ml, ih, il, hi, lo, pr)) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.low(Nat.add(64n, 64n), Nat.add(Nat.mul(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/random.value128(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/random/pcg.P{hi, lo}), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/random.value128(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/random/pcg.P{mh, ml})), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/random.value128(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/random/pcg.P{ih, il}))) : Nat}

one step for any product pair (l, h) with l + 2^64 h == lo * ml (the pair is abstract here, so the checker never unfolds the 128-bit product)

def m128 source · line 65 · raw

@+a:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+b:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> {Nat.add(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.pfst(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.mul128(a, b))), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(64n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.psnd(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.mul128(a, b))))) == Nat.mul(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(a), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(b)) : Nat}