def interleave_correct

bend-collections-laws-math@1.0.0.0 · proofs/math/random/chacha8/rounds.bend:50

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/block.bend as B
import bend-collections-laws-math@1.0.0.0/spec/math/random/chacha8rand.bend as S

50# the interleaving is C2SP's permutation read as little-endian 64-bit words
51def interleave_correct(+a: B.Vector, +b: B.Vector, +c: B.Vector, +d: B.Vector) -> {B.interleave(a,b,c,d) == S.words64(S.interleave(16n,0n,vec(a),vec(b),vec(c),vec(d))) : List<&2,W.U64>}:
52  match a b c d:
53    case B.V{a0,a1,a2,a3,a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a14,a15} B.V{b0,b1,b2,b3,b4,b5,b6,b7,b8,b9,b10,b11,b12,b13,b14,b15} B.V{c0,c1,c2,c3,c4,c5,c6,c7,c8,c9,c10,c11,c12,c13,c14,c15} B.V{d0,d1,d2,d3,d4,d5,d6,d7,d8,d9,d10,d11,d12,d13,d14,d15}: {==}