def step_pair

bend-collections-laws-math@1.0.0.0 · proofs/math/random/pcg/impl.bend:51

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/spec/math/w64.bend as SW
import bend-collections-laws-math@1.0.0.0/src/math/u64.bend as WU
import bend-collections-laws-math@1.0.0.0/src/math/w64.bend as X
import bend-collections-laws-math@1.0.0.0/src/math/random/pcg.bend as P
import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/spec/numeric.bend as S
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64m128.bend as M128
import bend-collections-laws-math@1.0.0.0/proofs/math/random/pcg/step.bend as ST
import bend-collections-laws-math@1.0.0.0/spec/math/random.bend as SR

51# one step for any product pair (l, h) with l + 2^64 h == lo * ml (the pair
52# is abstract here, so the checker never unfolds the 128-bit product)
53def step_pair(+mh: WU.U64, +ml: WU.U64, +ih: WU.U64, +il: WU.U64, +hi: WU.U64, +lo: WU.U64, pr: WU.U64 & WU.U64, +h1: {Nat.add(SW.value(X.pfst(pr)), C.shift(64n, SW.value(X.psnd(pr)))) == Nat.mul(SW.value(lo), SW.value(ml)) : Nat}) -> {SR.value128(P.step_mul(mh, ml, ih, il, hi, lo, pr)) == C.low(Nat.add(64n, 64n), Nat.add(Nat.mul(SR.value128(P.P{hi, lo}), SR.value128(P.P{mh, ml})), SR.value128(P.P{ih, il}))) : Nat}:
54  match pr:
55    case Tuple{+l, +h}:
56      +T = X.add(X.mul(hi, ml), X.mul(lo, mh))
57      +H = X.add(h, T)
58      +H1 = X.add(H, ih)
59      +cb = X.add_over(l, il)
60      +H2 = X.add(H1, WU.U64{X.b32(cb), 0})
61      +L = X.add(l, il)
62      ST.step_value(64n, SW.value(lo), SW.value(hi), SW.value(ml), SW.value(mh), SW.value(il), SW.value(ih), SW.value(l), SW.value(h), SW.value(T), SW.value(H), SW.value(H1), SW.value(L), S.bit_value(cb), SW.value(H2), SR.value128(P.P{hi, lo}), SR.value128(P.P{mh, ml}), SR.value128(P.P{ih, il}), {==}, {==}, {==},
63        h1, fT(hi, lo, ml, mh), fS(h, T), fS(H, ih), fV(H1, cb), M128.add_split(l, il), M128.fit64(L), M128.fit64(H2))