law hchacha_length

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

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

150law hchacha_length:
151  for +r: Nat
152  for +key: List<&2, U32>
153  for +nonce: List<&2, U32>
154  {List.length(&2, U32, R.hchacha_rounds(r, key, nonce)) == 32n : Nat}