law block_correct

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/chacha/core.bend:122

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

122# The block function with n double rounds, serialized, is the RFC's.
123law block_correct:
124  for +n: Nat
125  for +s: C.State
126  {C.bytes(C.block(n, s)) == R.serialize(R.add_words(vec(s), R.inner_blocks(n, vec(s)))) : List<&2, U32>}