law open_tag_false

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/aead/chacha20poly1305.bend:289

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

289law open_tag_false:
290  for +key: List<&2, U32>
291  for +nonce: List<&2, U32>
292  for +aad: List<&2, U32>
293  for +ct: List<&2, U32>
294  for +t: List<&2, U32>
295  for ne: {t != R.tag(key, nonce, aad, ct) : List<&2, U32>}
296  for +b: Bool
297  for +hb: {RS.equal(t, R.tag(key, nonce, aad, ct)) == b : Bool}
298  {R.open_tag(b, key, nonce, ct) == None{} : Maybe<&2, List<&2, U32>>}