law encrypt_length

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

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

188# The ciphertext is as long as the plaintext.
189law encrypt_length:
190  for +r: Nat
191  for +kb: List<&2, U32>
192  for +c: U32
193  for +nb: List<&2, U32>
194  for +pt: List<&2, U32>
195  {List.length(&2, U32, R.encrypt_rounds(r, kb, c, nb, pt)) == List.length(&2, U32, pt) : Nat}