def dr_correct

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

import Base
import bend-collections-laws-crypto@1.0.0.0/src/math/random/chacha8/block.bend as B
import bend-collections-laws-crypto@1.0.0.0/spec/math/random/chacha8rand.bend as S

21# one double round is RFC 8439's inner_block
22def dr_correct(+v: B.Vector) -> {vec(B.dr(v)) == S.double_round(vec(v)) : List<&2,U32>}:
23  match v:
24    case B.V{a0,a1,a2,a3,a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a14,a15}: {==}