Chacha20.stream: def of bend-collections-laws-crypto@1.0.0.0
Import: import bend-collections-laws-crypto@1.0.0.0/src/crypto/chacha/chacha20.bend as Chacha20
Lines 78-86 of bend-collections-laws-crypto@1.0.0.0/src/crypto/chacha/chacha20.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/chacha/chacha20.bend&start_line=78&end_line=86

import Base

# Blocks of 64 bytes, block j under counter + j; fuel bounds the number of
# blocks (the length of xs is enough).
def stream(fuel: Nat, +xs: List<&2, U32>, +r: Nat, +k: Key, +counter: U32, +n: Nonce) -> List<&2, U32>:
  match fuel xs:
    case 0n _: Nil{}
    case 1n+p Nil{}: Nil{}
    case 1n+p x <> xt:
      List.append(&2, U32, xor_front(keystream(r, k, counter, n), x <> xt),
        stream(p, skip(64n, x <> xt), r, k, U32.add(counter, 1), n))

Uses (10):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List.append
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.add
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/chacha/chacha20.bend&name=Key
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/chacha/chacha20.bend&name=Nonce
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/chacha/chacha20.bend&name=keystream
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/chacha/chacha20.bend&name=skip
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/chacha/chacha20.bend&name=xor_front