def PCG.output

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

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/w64.bend as SW
import bend-collections-laws-crypto@1.0.0.0/spec/math/random/pcg.bend as SP

91# stated through the intermediate value t of the first half (so the
92# checker never compares two copies of the nested 64-bit recursion);
93# t = dxsm1(cm, hi) gives output == dxsm(cm, hi, lo)
94def PCG.output(+cm: W.U64, +hi: W.U64, +lo: W.U64, +t: Nat, +ht: {t == SP.dxsm1(SW.value(cm), SW.value(hi)) : Nat}) -> Type:
95  {SW.value(P.dxsm_with(cm, hi, lo)) == SP.dxsm3(t, SW.value(lo)) : Nat}