Wrappers.wgo: def of bend-collections-laws-math@1.0.0.0
Import: import bend-collections-laws-math@1.0.0.0/proofs/math/random/wrappers.bend as Wrappers
Lines 178-204 of bend-collections-laws-math@1.0.0.0/proofs/math/random/wrappers.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/random/wrappers.bend&start_line=178&end_line=204

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/src/math/w64.bend as X
import bend-collections-laws-math@1.0.0.0/src/math/random/rand.bend as R
import bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend as N
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/width.bend as WW
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64add.bend as WA
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64bits.bend as FB
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64sh.bend as SH
import bend-collections-laws-math@1.0.0.0/proofs/math/natural/arith.bend as AR
import bend-collections-laws-math@1.0.0.0/proofs/math/random/lemire.bend as LE

# the words of w_go are the low 8k bits, for 8k <= 32
def wgo(+k: Nat, +n: Nat, +hk: {Nat.is_le(sh8(k), 32n) == True{} : Bool}) -> {v(R.w_go(k, n)) == C.low(sh8(k), n) : Nat}:
  match k:
    case 0n:
      {==}
    case 1n+j:
      +d = C.high(8n, n)
      +hj = N.le_trans(sh8(j), Nat.add(8n, sh8(j)), 32n, LE.le_plus(8n, sh8(j)), hk)
      +hj24 = Equal.trans(Bool, Nat.is_le(sh8(j), 24n), Nat.is_le(Nat.add(8n, sh8(j)), 32n), True{}, Equal.sym(Bool, Nat.is_le(Nat.add(8n, sh8(j)), 32n), Nat.is_le(sh8(j), 24n), AR.le_add_cancel(8n, sh8(j), 24n)), hk)
      +ih = Equal.trans(Nat, v(R.w_go(j, Nat.div(n, 256n))), C.low(sh8(j), Nat.div(n, 256n)), C.low(sh8(j), d), wgo(j, Nat.div(n, 256n), hj), Equal.cong(Nat, Nat, z => C.low(sh8(j), z), Nat.div(n, 256n), d, div256(n)))
      +lw = C.low(sh8(j), d)
      +f24 = SH.fits_mono(sh8(j), 24n, lw, hj24, WW.low_fits(sh8(j), d))
      +f32s = fits_shift(8n, 24n, lw, f24)
      +em = Equal.trans(Nat, v(U32.mul(R.w_go(j, Nat.div(n, 256n)), X.pow2(8n))), C.low(32n, C.shift(8n, v(R.w_go(j, Nat.div(n, 256n))))), C.shift(8n, lw),
        SH.mul_p2(R.w_go(j, Nat.div(n, 256n)), 8n, {==}),
        Equal.trans(Nat, C.low(32n, C.shift(8n, v(R.w_go(j, Nat.div(n, 256n))))), C.low(32n, C.shift(8n, lw)), C.shift(8n, lw), Equal.cong(Nat, Nat, z => C.low(32n, C.shift(8n, z)), v(R.w_go(j, Nat.div(n, 256n))), lw, ih), WW.low_fit(32n, C.shift(8n, lw), f32s)))
      +sum = Nat.add(C.low(8n, n), C.shift(8n, lw))
      +es = Equal.sym(Nat, C.low(Nat.add(8n, sh8(j)), n), sum, FB.low_split(8n, sh8(j), n))
      +fsum = SH.fits_mono(Nat.add(8n, sh8(j)), 32n, sum, hk, Equal.trans(Bool, C.fits(Nat.add(8n, sh8(j)), sum), C.fits(Nat.add(8n, sh8(j)), C.low(Nat.add(8n, sh8(j)), n)), True{}, Equal.cong(Nat, Bool, z => C.fits(Nat.add(8n, sh8(j)), z), sum, C.low(Nat.add(8n, sh8(j)), n), es), WW.low_fits(Nat.add(8n, sh8(j)), n)))
      +bv = byte_v(n)
      +vsum = Equal.trans(Nat, Nat.add(v(U32.from_nat(Nat.mod(n, 256n))), v(U32.mul(R.w_go(j, Nat.div(n, 256n)), X.pow2(8n)))), Nat.add(C.low(8n, n), v(U32.mul(R.w_go(j, Nat.div(n, 256n)), X.pow2(8n)))), sum,
        Equal.cong(Nat, Nat, z => Nat.add(z, v(U32.mul(R.w_go(j, Nat.div(n, 256n)), X.pow2(8n)))), v(U32.from_nat(Nat.mod(n, 256n))), C.low(8n, n), bv),
        Equal.cong(Nat, Nat, z => Nat.add(C.low(8n, n), z), v(U32.mul(R.w_go(j, Nat.div(n, 256n)), X.pow2(8n))), C.shift(8n, lw), em))
      +hf = Equal.trans(Bool, C.fits(32n, Nat.add(v(U32.from_nat(Nat.mod(n, 256n))), v(U32.mul(R.w_go(j, Nat.div(n, 256n)), X.pow2(8n))))), C.fits(32n, sum), True{}, Equal.cong(Nat, Bool, z => C.fits(32n, z), Nat.add(v(U32.from_nat(Nat.mod(n, 256n))), v(U32.mul(R.w_go(j, Nat.div(n, 256n)), X.pow2(8n)))), sum, vsum), fsum)
      Equal.trans(Nat, v(U32.add(U32.from_nat(Nat.mod(n, 256n)), U32.mul(R.w_go(j, Nat.div(n, 256n)), X.pow2(8n)))), Nat.add(v(U32.from_nat(Nat.mod(n, 256n))), v(U32.mul(R.w_go(j, Nat.div(n, 256n)), X.pow2(8n)))), C.low(Nat.add(8n, sh8(j)), n),
        WA.add_exact(1n, {==}, U32.from_nat(Nat.mod(n, 256n)), U32.mul(R.w_go(j, Nat.div(n, 256n)), X.pow2(8n)), hf),
        Equal.trans(Nat, Nat.add(v(U32.from_nat(Nat.mod(n, 256n))), v(U32.mul(R.w_go(j, Nat.div(n, 256n)), X.pow2(8n)))), sum, C.low(Nat.add(8n, sh8(j)), n), vsum, es))

Uses (32):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.cong
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.trans
  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.div
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_le
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.mod
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.add
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.from_nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.mul
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend&name=le_trans
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/natural/arith.bend&name=le_add_cancel
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/random/lemire.bend&name=le_plus
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/random/wrappers.bend&name=byte_v
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/random/wrappers.bend&name=div256
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/random/wrappers.bend&name=fits_shift
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/random/wrappers.bend&name=sh8
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/random/wrappers.bend&name=v
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64bits.bend&name=low_split
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64add.bend&name=add_exact
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64sh.bend&name=fits_mono
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64sh.bend&name=mul_p2
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/width.bend&name=low_fit
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/width.bend&name=low_fits
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/lib/common.bend&name=fits
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/lib/common.bend&name=high
  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/src/math/random/rand.bend&name=w_go
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/src/math/w64.bend&name=pow2