def PCG.step

bend-collections-laws-crypto@1.0.0.0 · spec/math/random.bend:88

import Base
import bend-collections-laws-crypto@1.0.0.0/src/math/u64.bend as W
import bend-collections-laws-crypto@1.0.0.0/src/math/random/pcg.bend as P
import bend-collections-laws-crypto@1.0.0.0/spec/math/random/pcg.bend as SP

88def PCG.step(+mh: W.U64, +ml: W.U64, +ih: W.U64, +il: W.U64, +p: P.PCG) -> Type:
89  {value128(P.step_with(mh, ml, ih, il, p)) == SP.lcg(value128(P.P{mh, ml}), value128(P.P{ih, il}), value128(p)) : Nat}