Bytes.step: def of bend-collections-laws-crypto@1.0.0.0
Import: import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/random/bytes.bend as Bytes
Lines 116-129 of bend-collections-laws-crypto@1.0.0.0/proofs/crypto/random/bytes.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/random/bytes.bend&start_line=116&end_line=129

import Base
import bend-collections-laws-crypto@1.0.0.0/src/math/random/chacha8.bend as C8
import bend-collections-laws-crypto@1.0.0.0/src/crypto/random.bend as CR
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/random.bend as SCR
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend as N

# one byte of the loop against the byte stream
def step(+j: Nat, +f: CR.Fill) -> {SCR.append(rev(facc(CR.take1(f))), SCR.take(j, SCR.append(fpend(CR.take1(f)), SCR.flat(outs(j, fsrc(CR.take1(f))))))) == SCR.append(rev(facc(f)), SCR.take(1n+j, SCR.append(fpend(f), SCR.flat(outs(1n+j, fsrc(f)))))) : List<&2, U32>}:
  match f:
    case CR.FS{+acc, +c, +p}:
      match p:
        case Con{+b, +rest}:
          Equal.trans(List<&2, U32>, SCR.append(rev(Con{b, acc}), SCR.take(j, SCR.append(rest, SCR.flat(outs(j, c))))), SCR.append(rev(acc), Con{b, SCR.take(j, SCR.append(rest, SCR.flat(outs(j, c))))}), SCR.append(rev(acc), Con{b, SCR.take(j, SCR.append(rest, SCR.flat(outs(1n+j, c))))}),
            rev_cons(b, acc, SCR.take(j, SCR.append(rest, SCR.flat(outs(j, c))))),
            Equal.cong(List<&2, U32>, List<&2, U32>, z => SCR.append(rev(acc), Con{b, z}), SCR.take(j, SCR.append(rest, SCR.flat(outs(j, c)))), SCR.take(j, SCR.append(rest, SCR.flat(outs(1n+j, c)))),
              Equal.sym(List<&2, U32>, SCR.take(j, SCR.append(rest, SCR.flat(outs(1n+j, c)))), SCR.take(j, SCR.append(rest, SCR.flat(outs(j, c)))),
                %Equal.trans(Nat, Nat.add(j, 1n), 1n+Nat.add(j, 0n), 1n+j, N.add_succ(j, 0n), Equal.cong(Nat, Nat, z => 1n+z, Nat.add(j, 0n), j, N.add_zero(j))) : {SCR.take(j, SCR.append(rest, SCR.flat(outs(_, c)))) == SCR.take(j, SCR.append(rest, SCR.flat(outs(j, c)))) : List<&2, U32>}
                prefix(j, rest, c, 1n))))
        case Nil{}:
          step_nil(j, acc, C8.next(c))

Uses (23):
  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=List
  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=U32
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/random/bytes.bend&name=facc
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/random/bytes.bend&name=fpend
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/random/bytes.bend&name=fsrc
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/random/bytes.bend&name=outs
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/random/bytes.bend&name=prefix
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/random/bytes.bend&name=rev
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/random/bytes.bend&name=rev_cons
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/random/bytes.bend&name=step_nil
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend&name=add_succ
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend&name=add_zero
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/random.bend&name=append
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/random.bend&name=flat
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/random.bend&name=take
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/random.bend&name=Fill
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/random.bend&name=take1
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/math/random/chacha8.bend&name=next