law involution

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

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

117# Decryption is encryption: applying the cipher twice is the identity.
118law involution:
119  for +r: Nat
120  for +key: List<&2, U32>
121  for +counter: U32
122  for +nonce: List<&2, U32>
123  for +plaintext: List<&2, U32>
124  {I.encrypt_rounds(r, key, counter, nonce, I.encrypt_rounds(r, key, counter, nonce, plaintext)) == plaintext : List<&2, U32>}