def step_value

bend-collections-laws-math@1.0.0.0 · proofs/math/random/pcg/step.bend:191

import Base
import bend-collections-laws-math@1.0.0.0/spec/lib/common.bend as C
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/width.bend as WW

191# THEOREM on values: the limb results are the LCG step mod 2^128 (the state
192# s, multiplier mul and increment inc given by their limbs)
193def step_value(+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, C.shift(k, vhi)) : Nat}, +hm: {mul == Nat.add(vml, C.shift(k, vmh)) : Nat}, +hi: {inc == Nat.add(vil, C.shift(k, vih)) : Nat}, +h1: {Nat.add(vl, C.shift(k, vh)) == Nat.mul(vlo, vml) : Nat}, +hT: {C.low(k, t) == C.low(k, Nat.add(Nat.mul(vhi, vml), Nat.mul(vlo, vmh))) : Nat}, +hH: {C.low(k, vH) == C.low(k, Nat.add(vh, t)) : Nat}, +hU: {C.low(k, u) == C.low(k, Nat.add(vH, vih)) : Nat}, +hV: {vH2 == C.low(k, Nat.add(u, c)) : Nat}, +h3: {Nat.add(vl, vil) == Nat.add(L, C.shift(k, c)) : Nat}, +hL: {C.fits(k, L) == True{} : Bool}, +hH2: {C.fits(k, vH2) == True{} : Bool}) -> {Nat.add(L, C.shift(k, vH2)) == C.low(Nat.add(k, k), Nat.add(Nat.mul(s, mul), inc)) : Nat}:
194  +p1 = Nat.mul(vlo, vmh)
195  +p2 = Nat.mul(vhi, vml)
196  +p3 = Nat.mul(vhi, vmh)
197  +Z = Nat.add(Nat.add(Nat.add(Nat.add(vh, Nat.add(p2, p1)), vih), c), C.shift(k, p3))
198  +SX = Nat.add(Nat.mul(Nat.add(vlo, C.shift(k, vhi)), Nat.add(vml, C.shift(k, vmh))), Nat.add(vil, C.shift(k, vih)))
199  +SMI = Nat.add(Nat.mul(s, mul), inc)
200  +LS = Nat.add(L, C.shift(k, vH2))
201  +eS = Equal.trans(Nat, SMI, Nat.add(Nat.mul(Nat.add(vlo, C.shift(k, vhi)), mul), inc), SX,
202    Equal.cong(Nat, Nat, z => Nat.add(Nat.mul(z, mul), inc), s, Nat.add(vlo, C.shift(k, vhi)), hs),
203    Equal.trans(Nat, Nat.add(Nat.mul(Nat.add(vlo, C.shift(k, vhi)), mul), inc), Nat.add(Nat.mul(Nat.add(vlo, C.shift(k, vhi)), Nat.add(vml, C.shift(k, vmh))), inc), SX,
204      Equal.cong(Nat, Nat, z => Nat.add(Nat.mul(Nat.add(vlo, C.shift(k, vhi)), z), inc), mul, Nat.add(vml, C.shift(k, vmh)), hm),
205      Equal.cong(Nat, Nat, z => Nat.add(Nat.mul(Nat.add(vlo, C.shift(k, vhi)), Nat.add(vml, C.shift(k, vmh))), z), inc, Nat.add(vil, C.shift(k, vih)), hi)))
206  +eZ = Equal.trans(Nat, SMI, SX, Nat.add(L, C.shift(k, Z)), eS, expand(k, vlo, vhi, vml, vmh, vil, vih, vl, vh, L, c, h1, h3))
207  +hw = high_word(k, vh, p2, p1, p3, vih, c, t, vH, u, vH2, hT, hH, hU, hV)
208  +e1 = Equal.trans(Nat, C.low(Nat.add(k, k), SMI), C.low(Nat.add(k, k), Nat.add(L, C.shift(k, Z))), C.low(Nat.add(k, k), LS),
209    Equal.cong(Nat, Nat, z => C.low(Nat.add(k, k), z), SMI, Nat.add(L, C.shift(k, Z)), eZ),
210    low_hi(k, L, Z, vH2, Equal.sym(Nat, C.low(k, Z), vH2, hw)))
211  Equal.sym(Nat, C.low(Nat.add(k, k), SMI), LS, Equal.trans(Nat, C.low(Nat.add(k, k), SMI), C.low(Nat.add(k, k), LS), LS, e1, WW.low_fit(Nat.add(k, k), LS, WW.limbs_fit(k, k, L, vH2, hL, hH2))))