def rest

bend-collections-laws-math@1.0.0.0 · proofs/math/random/chacha8/stream.bend:30

import Base
import bend-collections-laws-math@1.0.0.0/src/math/u64.bend as W
import bend-collections-laws-math@1.0.0.0/src/math/random/chacha8.bend as C8
import bend-collections-laws-math@1.0.0.0/spec/math/random/chacha8rand.bend as S

30# the outputs of the current iteration after the groups already produced
31def rest(+kl: List<&2, U32>, p: C8.Phase) -> List<&2, W.U64>:
32  match p:
33    case C8.G0{}:
34      []
35    case C8.G1{}:
36      drop64(32n, S.words64(S.output(kl)))
37    case C8.G2{}:
38      drop64(64n, S.words64(S.output(kl)))
39    case C8.G3{}:
40      drop64(96n, S.words64(S.output(kl)))