def interleave

bend-collections-laws-crypto@1.0.0.0 · spec/math/random/chacha8rand.bend:130

import Base

130# C2SP: "for each sequence of four blocks, first we output the first four
131# bytes of each block, then the next four bytes of each block, and so on"
132def interleave(k: Nat, +i: Nat, +b0: List<&2, U32>, +b1: List<&2, U32>, +b2: List<&2, U32>, +b3: List<&2, U32>) -> List<&2, U32>:
133  match k:
134    case 0n:
135      []
136    case 1n+p:
137      Con{get(b0, i), Con{get(b1, i), Con{get(b2, i), Con{get(b3, i), interleave(p, Nat.add(i, 1n), b0, b1, b2, b3)}}}}