def ks

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/chacha/involution.bend:101

import Base
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/chacha.bend as R

101# The keystream of fuel blocks from counter c.
102def ks(fuel: Nat, +r: Nat, +kb: List<&2, U32>, +c: U32, +nb: List<&2, U32>) -> List<&2, U32>:
103  match fuel:
104    case 0n: Nil{}
105    case 1n+p: List.append(&2, U32, R.block_rounds(r, kb, c, nb), ks(p, r, kb, U32.add(c, 1), nb))