law block_length

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

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

160law block_length:
161  for +r: Nat
162  for +kb: List<&2, U32>
163  for +c: U32
164  for +nb: List<&2, U32>
165  {List.length(&2, U32, R.block_rounds(r, kb, c, nb)) == 64n : Nat}