law block_rounds

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

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

14# chacha20_block with r double rounds.
15law block_rounds:
16  for +r: Nat
17  for +key: List<&2, U32>
18  for +counter: U32
19  for +nonce: List<&2, U32>
20  {I.block_rounds(r, key, counter, nonce) == R.block_rounds(r, key, counter, nonce) : List<&2, U32>}