~/bend-docscommunity

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

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

15 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

Definitions

def low_l source · line 26 · raw

@+k:Nat -> @+a:Nat -> @+b:Nat -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.low(k, Nat.add(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.low(k, a), b)) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.low(k, Nat.add(a, b)) : Nat}

def low_r source · line 37 · raw

@+k:Nat -> @+a:Nat -> @+b:Nat -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.low(k, Nat.add(a, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.low(k, b))) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.low(k, Nat.add(a, b)) : Nat}

def low_add source · line 45 · raw

@+k:Nat -> @+x:Nat -> @+x2:Nat -> @+y:Nat -> @+y2:Nat -> @+hx:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.low(k, x) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.low(k, x2) : Nat} -> @+hy:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.low(k, y) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.low(k, y2) : Nat} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.low(k, Nat.add(x, y)) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.low(k, Nat.add(x2, y2)) : Nat}

congruence mod 2^k is kept by sums

def low_low source · line 58 · raw

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

def low_hi source · line 62 · raw

@+k:Nat -> @+a:Nat -> @+b:Nat -> @+lb:Nat -> @+hlb:{lb == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.low(k, b) : Nat} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.low(Nat.add(k, k), Nat.add(a, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(k, b))) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.low(Nat.add(k, k), Nat.add(a, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(k, lb))) : Nat}

mod 2^128, a + 2^64 b depends on b mod 2^64 = lb only

def perm7 source · line 84 · raw

@+a:Nat -> @+b:Nat -> @+c:Nat -> @+d:Nat -> @+e:Nat -> @+f:Nat -> @+g:Nat -> {Nat.add(Nat.add(Nat.add(Nat.add(a, c), d), Nat.add(e, g)), Nat.add(b, f)) == Nat.add(Nat.add(a, b), Nat.add(Nat.add(Nat.add(c, Nat.add(e, d)), f), g)) : Nat}

(((a + c) + d) + (e + g)) + (b + f) == (a + b) + (((c + (e + d)) + f) + g)

def swap3 source · line 124 · raw

@+L:Nat -> @+x:Nat -> @+y:Nat -> @+z:Nat -> {Nat.add(Nat.add(L, x), Nat.add(y, z)) == Nat.add(L, Nat.add(Nat.add(y, x), z)) : Nat}

(L + x) + (y + z) == L + ((y + x) + z)

def shx source · line 133 · raw

@+k:Nat -> @+h:Nat -> @+p2:Nat -> @+p1:Nat -> @+i:Nat -> @+c:Nat -> @+p3:Nat -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(k, Nat.add(Nat.add(Nat.add(Nat.add(h, Nat.add(p2, p1)), i), c), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(k, p3))) == Nat.add(Nat.add(Nat.add(Nat.add(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(k, h), Nat.add(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(k, p2), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(k, p1))), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(k, i)), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(k, c)), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(k, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(k, p3))) : Nat}

2^64 ((((h + (p2 + p1)) + i) + c) + 2^64 p3), distributed

def expand source · line 151 · raw

@+k:Nat -> @+vlo:Nat -> @+vhi:Nat -> @+vml:Nat -> @+vmh:Nat -> @+vil:Nat -> @+vih:Nat -> @+vl:Nat -> @+vh:Nat -> @+L:Nat -> @+c:Nat -> @+h1:{Nat.add(vl, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(k, vh)) == Nat.mul(vlo, vml) : Nat} -> @+h3:{Nat.add(vl, vil) == Nat.add(L, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(k, c)) : Nat} -> {Nat.add(Nat.mul(Nat.add(vlo, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(k, vhi)), Nat.add(vml, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(k, vmh))), Nat.add(vil, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(k, vih))) == Nat.add(L, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(k, Nat.add(Nat.add(Nat.add(Nat.add(vh, Nat.add(Nat.mul(vhi, vml), Nat.mul(vlo, vmh))), vih), c), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(k, Nat.mul(vhi, vmh))))) : Nat}

s * M + I == L + 2^64 Z for Z = ((((h + (P2 + P1)) + i) + c) + 2^64 P3)

def eqm_of source · line 176 · raw

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

def high_word source · line 180 · raw

@+k:Nat -> @+vh:Nat -> @+p2:Nat -> @+p1:Nat -> @+p3:Nat -> @+vih:Nat -> @+c:Nat -> @+t:Nat -> @+vH:Nat -> @+u:Nat -> @+vH2:Nat -> @+hT:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.low(k, t) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.low(k, Nat.add(p2, p1)) : Nat} -> @+hH:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.low(k, vH) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.low(k, Nat.add(vh, t)) : Nat} -> @+hU:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.low(k, u) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.low(k, Nat.add(vH, vih)) : Nat} -> @+hV:{vH2 == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.low(k, Nat.add(u, c)) : Nat} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.low(k, Nat.add(Nat.add(Nat.add(Nat.add(vh, Nat.add(p2, p1)), vih), c), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(k, p3))) == vH2 : Nat}

the new high word is Z mod 2^64 (t, vH, u: the sums of the implementation)

def step_value source · line 193 · raw

@+k:Nat -> @+vlo:Nat -> @+vhi:Nat -> @+vml:Nat -> @+vmh:Nat -> @+vil:Nat -> @+vih:Nat -> @+vl:Nat -> @+vh:Nat -> @+t:Nat -> @+vH:Nat -> @+u:Nat -> @+L:Nat -> @+c:Nat -> @+vH2:Nat -> @+s:Nat -> @+mul:Nat -> @+inc:Nat -> @+hs:{s == Nat.add(vlo, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(k, vhi)) : Nat} -> @+hm:{mul == Nat.add(vml, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(k, vmh)) : Nat} -> @+hi:{inc == Nat.add(vil, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(k, vih)) : Nat} -> @+h1:{Nat.add(vl, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(k, vh)) == Nat.mul(vlo, vml) : Nat} -> @+hT:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.low(k, t) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.low(k, Nat.add(Nat.mul(vhi, vml), Nat.mul(vlo, vmh))) : Nat} -> @+hH:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.low(k, vH) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.low(k, Nat.add(vh, t)) : Nat} -> @+hU:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.low(k, u) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.low(k, Nat.add(vH, vih)) : Nat} -> @+hV:{vH2 == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.low(k, Nat.add(u, c)) : Nat} -> @+h3:{Nat.add(vl, vil) == Nat.add(L, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(k, c)) : Nat} -> @+hL:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(k, L) == True{} : Bool} -> @+hH2:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(k, vH2) == True{} : Bool} -> {Nat.add(L, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(k, vH2)) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.low(Nat.add(k, k), Nat.add(Nat.mul(s, mul), inc)) : Nat}

THEOREM on values: the limb results are the LCG step mod 2^128 (the state s, multiplier mul and increment inc given by their limbs)