law c_len

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

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

96law c_len:
97  for +short: Bool
98  for +key: List<&2, U32>
99  for +nonce: List<&2, U32>
100  for +aad: List<&2, U32>
101  for +data: List<&2, U32>
102  for +p: List<&2, U32>
103  for +h: {R.open_len(short, key, nonce, aad, data) == Some{p} : Maybe<&2, List<&2, U32>>}
104  {R.seal(key, nonce, aad, p) == data : List<&2, U32>}