law chacha_sound

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

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

117# Whatever opens to p is the sealing of p.
118law chacha_sound:
119  for +key: List<&2, U32>
120  for +nonce: List<&2, U32>
121  for +aad: List<&2, U32>
122  for +data: List<&2, U32>
123  for +p: List<&2, U32>
124  for +h: {R.open(key, nonce, aad, data) == Some{p} : Maybe<&2, List<&2, U32>>}
125  {R.seal(key, nonce, aad, p) == data : List<&2, U32>}