Impl.step_pair: def of bend-collections-laws-math@1.0.0.0
Import: import bend-collections-laws-math@1.0.0.0/proofs/math/random/pcg/impl.bend as Impl
Lines 51-63 of bend-collections-laws-math@1.0.0.0/proofs/math/random/pcg/impl.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/random/pcg/impl.bend&start_line=51&end_line=63

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

# one step for any product pair (l, h) with l + 2^64 h == lo * ml (the pair
# is abstract here, so the checker never unfolds the 128-bit product)
def 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}:
  match pr:
    case Tuple{+l, +h}:
      +T = X.add(X.mul(hi, ml), X.mul(lo, mh))
      +H = X.add(h, T)
      +H1 = X.add(H, ih)
      +cb = X.add_over(l, il)
      +H2 = X.add(H1, WU.U64{X.b32(cb), 0})
      +L = X.add(l, il)
      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}), {==}, {==}, {==},
        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))

Uses (25):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.add
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.mul
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Pair
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Sigma
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/spec/numeric.bend&name=bit_value
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/random/pcg/impl.bend&name=fS
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/random/pcg/impl.bend&name=fT
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/random/pcg/impl.bend&name=fV
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/random/pcg/step.bend&name=step_value
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64m128.bend&name=add_split
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64m128.bend&name=fit64
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/lib/common.bend&name=low
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/lib/common.bend&name=shift
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/math/random.bend&name=value128
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/math/w64.bend&name=value
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/src/math/random/pcg.bend&name=PCG
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/src/math/random/pcg.bend&name=step_mul
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/src/math/u64.bend&name=U64
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/src/math/w64.bend&name=add
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/src/math/w64.bend&name=add_over
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/src/math/w64.bend&name=b32
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/src/math/w64.bend&name=mul
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/src/math/w64.bend&name=pfst
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/src/math/w64.bend&name=psnd