bend-collections-laws-crypto

Releases (1):
  1.0.0.0  0xa7e654f9780078ca65bf9e187da99d3e  indexed  https://jend.leeeet.dev/files.txt?path=bend-collections-laws-crypto@1.0.0.0

Definitions (8881, 1 to 100 shown):
  Chacha20poly1305.poly_key_eq (https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aead/chacha20poly1305.bend&name=poly_key_eq)
   law poly_key_eq:
     for +key: List<&2, U32>
     for +nonce: List<&2, U32>
     {I.poly_key(key, nonce) == R.poly_key(key, nonce) : List<&2, U32>}
  Chacha20poly1305.mac_data_eq (https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aead/chacha20poly1305.bend&name=mac_data_eq)
   law mac_data_eq:
     for +aad: List<&2, U32>
     for +ct: List<&2, U32>
     {I.mac_data(aad, ct) == R.mac_data(aad, ct) : List<&2, U32>}
  Chacha20poly1305.tag_eq (https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aead/chacha20poly1305.bend&name=tag_eq)
   law tag_eq:
     for +key: List<&2, U32>
     for +nonce: List<&2, U32>
     for +aad: List<&2, U32>
     for +ct: List<&2, U32>
     {I.tag(key, nonce, aad, ct) == R.tag(key, nonce, aad, ct) : List<&2, U32>}
  Chacha20poly1305.iseal (https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aead/chacha20poly1305.bend&name=iseal)
   def iseal(+key: List<&2, U32>, +nonce: List<&2, U32>, +aad: List<&2, U32>, +ct: List<&2, U32>) -> List<&2, U32>:
  Chacha20poly1305.seal_eq (https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aead/chacha20poly1305.bend&name=seal_eq)
   law seal_eq:
     for +key: List<&2, U32>
     for +nonce: List<&2, U32>
     for +aad: List<&2, U32>
     for +pt: List<&2, U32>
     {I.seal(key, nonce, aad, pt) == R.seal(key, nonce, aad, pt) : List<&2, U32>}
  Chacha20poly1305.open_tag_eq (https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aead/chacha20poly1305.bend&name=open_tag_eq)
   law open_tag_eq:
     for +ok: Bool
     for +key: List<&2, U32>
     for +nonce: List<&2, U32>
     for +ct: List<&2, U32>
     {I.open_tag(ok, key, nonce, ct) == R.open_tag(ok, key, nonce, ct) : Maybe<&2, List<&2, U32>>}
  Chacha20poly1305.open_split_eq (https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aead/chacha20poly1305.bend&name=open_split_eq)
   law open_split_eq:
     for +key: List<&2, U32>
     for +nonce: List<&2, U32>
     for +aad: List<&2, U32>
     for +ct: List<&2, U32>
     for +t: List<&2, U32>
     {I.open_split(key, nonce, aad, ct, t) == R.open_split(key, nonce, aad, ct, t) : Maybe<&2, List<&2, U32>>}
  Chacha20poly1305.open_len_eq (https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aead/chacha20poly1305.bend&name=open_len_eq)
   law open_len_eq:
     for +short: Bool
     for +key: List<&2, U32>
     for +nonce: List<&2, U32>
     for +aad: List<&2, U32>
     for +data: List<&2, U32>
     {I.open_len(short, key, nonce, aad, data) == R.open_len(short, key, nonce, aad, data) : Maybe<&2, List<&2, U32>>}
  Chacha20poly1305.ospl (https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aead/chacha20poly1305.bend&name=ospl)
   def ospl(+key: List<&2, U32>, +nonce: List<&2, U32>, +aad: List<&2, U32>, +ct: List<&2, U32>, +t: List<&2, U32>) -> Maybe<&2, List<&2, U32>>:
  Chacha20poly1305.open_eq (https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aead/chacha20poly1305.bend&name=open_eq)
   law open_eq:
     for +key: List<&2, U32>
     for +nonce: List<&2, U32>
     for +aad: List<&2, U32>
     for +data: List<&2, U32>
     {I.open(key, nonce, aad, data) == R.open(key, nonce, aad, data) : Maybe<&2, List<&2, U32>>}
  Chacha20poly1305.xkey_eq (https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aead/chacha20poly1305.bend&name=xkey_eq)
   law xkey_eq:
     for +key: List<&2, U32>
     for +nonce: List<&2, U32>
     {I.xkey(key, nonce) == RC.xsubkey(key, nonce) : List<&2, U32>}
  Chacha20poly1305.xnonce_eq (https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aead/chacha20poly1305.bend&name=xnonce_eq)
   law xnonce_eq:
     for +nonce: List<&2, U32>
     {I.xnonce(nonce) == RC.xnonce(nonce) : List<&2, U32>}
  Chacha20poly1305.xseal_eq (https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aead/chacha20poly1305.bend&name=xseal_eq)
   law xseal_eq:
     for +key: List<&2, U32>
     for +nonce: List<&2, U32>
     for +aad: List<&2, U32>
     for +pt: List<&2, U32>
     {I.xseal(key, nonce, aad, pt) == R.xseal(key, nonce, aad, pt) : List<&2, U32>}
  Chacha20poly1305.xopen_eq (https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aead/chacha20poly1305.bend&name=xopen_eq)
   law xopen_eq:
     for +key: List<&2, U32>
     for +nonce: List<&2, U32>
     for +aad: List<&2, U32>
     for +data: List<&2, U32>
     {I.xopen(key, nonce, aad, data) == R.xopen(key, nonce, aad, data) : Maybe<&2, List<&2, U32>>}
  Chacha20poly1305.length_append (https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aead/chacha20poly1305.bend&name=length_append)
   law length_append:
     for +xs: List<&2, U32>
     for +ys: List<&2, U32>
     {List.length(&2, U32, List.append(&2, U32, xs, ys)) == Nat.add(List.length(&2, U32, xs), List.length(&2, U32, ys)) : Nat}
  Chacha20poly1305.prefix_append (https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aead/chacha20poly1305.bend&name=prefix_append)
   law prefix_append:
     for +xs: List<&2, U32>
     for +ys: List<&2, U32>
     {RC.prefix(List.length(&2, U32, xs), List.append(&2, U32, xs, ys)) == xs : List<&2, U32>}
  Chacha20poly1305.suffix_append (https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aead/chacha20poly1305.bend&name=suffix_append)
   law suffix_append:
     for +xs: List<&2, U32>
     for +ys: List<&2, U32>
     {RC.suffix(List.length(&2, U32, xs), List.append(&2, U32, xs, ys)) == ys : List<&2, U32>}
  Chacha20poly1305.add16_not_lt (https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aead/chacha20poly1305.bend&name=add16_not_lt)
   # a + 16 is not below 16, and (a + 16) - 16 == a.
   law add16_not_lt:
     for +a: Nat
     {Nat.is_lt(Nat.add(a, 16n), 16n) == False{} : Bool}
  Chacha20poly1305.add16_sub (https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aead/chacha20poly1305.bend&name=add16_sub)
   law add16_sub:
     for +a: Nat
     {Nat.sub(Nat.add(a, 16n), 16n) == a : Nat}
  Chacha20poly1305.open_append (https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aead/chacha20poly1305.bend&name=open_append)
   # Opening ct || t with a 16-byte t checks t against the tag of ct.
   law open_append:
     for +key: List<&2, U32>
     for +nonce: List<&2, U32>
     for +aad: List<&2, U32>
     for +ct: List<&2, U32>
     for +t: List<&2, U32>
     for +ht: {List.length(&2, U32, t) == 16n : Nat}
     {R.open(key, nonce, aad, List.append(&2, U32, ct, t)) == R.open_split(key, nonce, aad, ct, t) : Maybe<&2, List<&2, U32>>}
  Chacha20poly1305.olen (https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aead/chacha20poly1305.bend&name=olen)
   def olen(+key: List<&2, U32>, +nonce: List<&2, U32>, +aad: List<&2, U32>, +d: List<&2, U32>, short: Bool) -> Maybe<&2, List<&2, U32>>:
  Chacha20poly1305.osplit_at (https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aead/chacha20poly1305.bend&name=osplit_at)
   def osplit_at(+key: List<&2, U32>, +nonce: List<&2, U32>, +aad: List<&2, U32>, +d: List<&2, U32>, +n: Nat) -> Maybe<&2, List<&2, U32>>:
  Chacha20poly1305.roundtrip (https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aead/chacha20poly1305.bend&name=roundtrip)
   # Opening what was sealed gives the plaintext back (for every key, nonce,
   # aad and plaintext list).
   law roundtrip:
     for +key: List<&2, U32>
     for +nonce: List<&2, U32>
     for +aad: List<&2, U32>
     for +pt: List<&2, U32>
     {R.open(key, nonce, aad, R.seal(key, nonce, aad, pt)) == Some{pt} : Maybe<&2, List<&2, U32>>}
  Chacha20poly1305.open_tag_false (https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aead/chacha20poly1305.bend&name=open_tag_false)
   law open_tag_false:
     for +key: List<&2, U32>
     for +nonce: List<&2, U32>
     for +aad: List<&2, U32>
     for +ct: List<&2, U32>
     for +t: List<&2, U32>
     for ne: {t != R.tag(key, nonce, aad, ct) : List<&2, U32>}
     for +b: Bool
     for +hb: {RS.equal(t, R.tag(key, nonce, aad, ct)) == b : Bool}
     {R.open_tag(b, key, nonce, ct) == None{} : Maybe<&2, List<&2, U32>>}
  Chacha20poly1305.forgery (https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aead/chacha20poly1305.bend&name=forgery)
   # Opening ciphertext || t fails for every 16-byte t that is not the tag of
   # the ciphertext (under the key, nonce and aad given).
   law forgery:
     for +key: List<&2, U32>
     for +nonce: List<&2, U32>
     for +aad: List<&2, U32>
     for +ct: List<&2, U32>
     for +t: List<&2, U32>
     for +ht: {List.length(&2, U32, t) == 16n : Nat}
     for ne: {t != R.tag(key, nonce, aad, ct) : List<&2, U32>}
     {R.open(key, nonce, aad, List.append(&2, U32, ct, t)) == None{} : Maybe<&2, List<&2, U32>>}
  Chacha20poly1305.iforgery (https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aead/chacha20poly1305.bend&name=iforgery)
   # The implementation's tag is the specification's, so a t other than the
   # implementation's tag is rejected by the implementation.
   law iforgery:
     for +key: List<&2, U32>
     for +nonce: List<&2, U32>
     for +aad: List<&2, U32>
     for +ct: List<&2, U32>
     for +t: List<&2, U32>
     for +ht: {List.length(&2, U32, t) == 16n : Nat}
     for ne: {t != I.tag(key, nonce, aad, ct) : List<&2, U32>}
     {I.open(key, nonce, aad, List.append(&2, U32, ct, t)) == None{} : Maybe<&2, List<&2, U32>>}
  Chacha20poly1305.iroundtrip (https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aead/chacha20poly1305.bend&name=iroundtrip)
   law iroundtrip:
     for +key: List<&2, U32>
     for +nonce: List<&2, U32>
     for +aad: List<&2, U32>
     for +pt: List<&2, U32>
     {I.open(key, nonce, aad, I.seal(key, nonce, aad, pt)) == Some{pt} : Maybe<&2, List<&2, U32>>}
  Laws.expected_tag (https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aead/laws.bend&name=expected_tag)
   # The tag the specification computes over ciphertext ct: decrypt accepts
   # ct || t exactly for this t.
   def expected_tag(alg: A.Alg, +key: List<&2, U32>, +nonce: List<&2, U32>, +aad: List<&2, U32>, +ct: List<&2, U32>) -> List<&2, U32>:
  Laws.decrypt_sealed (https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aead/laws.bend&name=decrypt_sealed)
   # decrypt applied to what encrypt returned (None stays None).
   def decrypt_sealed(+alg: A.Alg, +key: List<&2, U32>, +nonce: List<&2, U32>, +aad: List<&2, U32>, m: Maybe<&2, List<&2, U32>>) -> Maybe<&2, List<&2, U32>>:
  Laws.chacha20poly1305.seal (https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aead/laws.bend&name=chacha20poly1305.seal)
   law chacha20poly1305.seal:
     for +key: List<&2, U32>
     for +nonce: List<&2, U32>
     for +aad: List<&2, U32>
     for +pt: List<&2, U32>
     {A.seal(A.CHACHA20_POLY1305{}, key, nonce, aad, pt) == Some{R.seal(key, nonce, aad, pt)} : Maybe<&2, List<&2, U32>>}
  Laws.chacha20poly1305.open (https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aead/laws.bend&name=chacha20poly1305.open)
   law chacha20poly1305.open:
     for +key: List<&2, U32>
     for +nonce: List<&2, U32>
     for +aad: List<&2, U32>
     for +data: List<&2, U32>
     {A.open(A.CHACHA20_POLY1305{}, key, nonce, aad, data) == R.open(key, nonce, aad, data) : Maybe<&2, List<&2, U32>>}
  Laws.xchacha20poly1305.seal (https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aead/laws.bend&name=xchacha20poly1305.seal)
   law xchacha20poly1305.seal:
     for +key: List<&2, U32>
     for +nonce: List<&2, U32>
     for +aad: List<&2, U32>
     for +pt: List<&2, U32>
     {A.seal(A.XCHACHA20_POLY1305{}, key, nonce, aad, pt) == Some{R.xseal(key, nonce, aad, pt)} : Maybe<&2, List<&2, U32>>}
  Laws.xchacha20poly1305.open (https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aead/laws.bend&name=xchacha20poly1305.open)
   law xchacha20poly1305.open:
     for +key: List<&2, U32>
     for +nonce: List<&2, U32>
     for +aad: List<&2, U32>
     for +data: List<&2, U32>
     {A.open(A.XCHACHA20_POLY1305{}, key, nonce, aad, data) == R.xopen(key, nonce, aad, data) : Maybe<&2, List<&2, U32>>}
  Laws.aes128gcm.seal (https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aead/laws.bend&name=aes128gcm.seal)
   law aes128gcm.seal:
     for +key: List<&2, U32>
     for +hk: {List.length(&2, U32, key) == 16n : Nat}
     for +nonce: List<&2, U32>
     for +hn: {List.length(&2, U32, nonce) == 12n : Nat}
     for +aad: List<&2, U32>
     for +pt: List<&2, U32>
     {A.seal(A.AES_128_GCM{}, key, nonce, aad, pt) == Some{G.aes_seal(key, nonce, aad, pt)} : Maybe<&2, List<&2, U32>>}
  Laws.aes128gcm.open (https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aead/laws.bend&name=aes128gcm.open)
   law aes128gcm.open:
     for +key: List<&2, U32>
     for +hk: {List.length(&2, U32, key) == 16n : Nat}
     for +nonce: List<&2, U32>
     for +hn: {List.length(&2, U32, nonce) == 12n : Nat}
     for +aad: List<&2, U32>
     for +data: List<&2, U32>
     {A.open(A.AES_128_GCM{}, key, nonce, aad, data) == G.aes_open(key, nonce, aad, data) : Maybe<&2, List<&2, U32>>}
  Laws.aes256gcm.seal (https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aead/laws.bend&name=aes256gcm.seal)
   law aes256gcm.seal:
     for +key: List<&2, U32>
     for +hk: {List.length(&2, U32, key) == 32n : Nat}
     for +nonce: List<&2, U32>
     for +hn: {List.length(&2, U32, nonce) == 12n : Nat}
     for +aad: List<&2, U32>
     for +pt: List<&2, U32>
     {A.seal(A.AES_256_GCM{}, key, nonce, aad, pt) == Some{G.aes_seal(key, nonce, aad, pt)} : Maybe<&2, List<&2, U32>>}
  Laws.aes256gcm.open (https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aead/laws.bend&name=aes256gcm.open)
   law aes256gcm.open:
     for +key: List<&2, U32>
     for +hk: {List.length(&2, U32, key) == 32n : Nat}
     for +nonce: List<&2, U32>
     for +hn: {List.length(&2, U32, nonce) == 12n : Nat}
     for +aad: List<&2, U32>
     for +data: List<&2, U32>
     {A.open(A.AES_256_GCM{}, key, nonce, aad, data) == G.aes_open(key, nonce, aad, data) : Maybe<&2, List<&2, U32>>}
  Laws.chacha20poly1305.encrypt (https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aead/laws.bend&name=chacha20poly1305.encrypt)
   # The per-algorithm checked ChaCha20-Poly1305 API agrees with the facade.
   law chacha20poly1305.encrypt:
     for +key: List<&2, U32>
     for +nonce: List<&2, U32>
     for +aad: List<&2, U32>
     for +pt: List<&2, U32>
     {CP.encrypt(key, nonce, aad, pt) == A.encrypt(A.CHACHA20_POLY1305{}, key, nonce, aad, pt) : Maybe<&2, List<&2, U32>>}
  Laws.chacha20poly1305.decrypt (https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aead/laws.bend&name=chacha20poly1305.decrypt)
   law chacha20poly1305.decrypt:
     for +key: List<&2, U32>
     for +nonce: List<&2, U32>
     for +aad: List<&2, U32>
     for +data: List<&2, U32>
     {CP.decrypt(key, nonce, aad, data) == A.decrypt(A.CHACHA20_POLY1305{}, key, nonce, aad, data) : Maybe<&2, List<&2, U32>>}
  Laws.xchacha20poly1305.encrypt (https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aead/laws.bend&name=xchacha20poly1305.encrypt)
   law xchacha20poly1305.encrypt:
     for +key: List<&2, U32>
     for +nonce: List<&2, U32>
     for +aad: List<&2, U32>
     for +pt: List<&2, U32>
     {CP.xencrypt(key, nonce, aad, pt) == A.encrypt(A.XCHACHA20_POLY1305{}, key, nonce, aad, pt) : Maybe<&2, List<&2, U32>>}
  Laws.xchacha20poly1305.decrypt (https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aead/laws.bend&name=xchacha20poly1305.decrypt)
   law xchacha20poly1305.decrypt:
     for +key: List<&2, U32>
     for +nonce: List<&2, U32>
     for +aad: List<&2, U32>
     for +data: List<&2, U32>
     {CP.xdecrypt(key, nonce, aad, data) == A.decrypt(A.XCHACHA20_POLY1305{}, key, nonce, aad, data) : Maybe<&2, List<&2, U32>>}
  Laws.encrypt.valid (https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aead/laws.bend&name=encrypt.valid)
   law encrypt.valid:
     for +alg: A.Alg
     for +key: List<&2, U32>
     for +nonce: List<&2, U32>
     for +aad: List<&2, U32>
     for +pt: List<&2, U32>
     for +hk: {List.length(&2, U32, key) == A.key_size(alg) : Nat}
     for +hn: {List.length(&2, U32, nonce) == A.nonce_size(alg) : Nat}
     {A.encrypt(alg, key, nonce, aad, pt) == A.seal(alg, key, nonce, aad, pt) : Maybe<&2, List<&2, U32>>}
  Laws.encrypt.invalid (https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aead/laws.bend&name=encrypt.invalid)
   law encrypt.invalid:
     for +alg: A.Alg
     for +key: List<&2, U32>
     for +nonce: List<&2, U32>
     for +aad: List<&2, U32>
     for +pt: List<&2, U32>
     for +h: {A.valid(alg, key, nonce) == False{} : Bool}
     {A.encrypt(alg, key, nonce, aad, pt) == None{} : Maybe<&2, List<&2, U32>>}
  Laws.decrypt.valid (https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aead/laws.bend&name=decrypt.valid)
   law decrypt.valid:
     for +alg: A.Alg
     for +key: List<&2, U32>
     for +nonce: List<&2, U32>
     for +aad: List<&2, U32>
     for +data: List<&2, U32>
     for +hk: {List.length(&2, U32, key) == A.key_size(alg) : Nat}
     for +hn: {List.length(&2, U32, nonce) == A.nonce_size(alg) : Nat}
     {A.decrypt(alg, key, nonce, aad, data) == A.open(alg, key, nonce, aad, data) : Maybe<&2, List<&2, U32>>}
  Laws.decrypt.invalid (https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aead/laws.bend&name=decrypt.invalid)
   law decrypt.invalid:
     for +alg: A.Alg
     for +key: List<&2, U32>
     for +nonce: List<&2, U32>
     for +aad: List<&2, U32>
     for +data: List<&2, U32>
     for +h: {A.valid(alg, key, nonce) == False{} : Bool}
     {A.decrypt(alg, key, nonce, aad, data) == None{} : Maybe<&2, List<&2, U32>>}
  Laws.roundtrip (https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aead/laws.bend&name=roundtrip)
   # decrypt(encrypt(x)) == Some(x).
   law roundtrip:
     for +alg: A.Alg
     for +key: List<&2, U32>
     for +nonce: List<&2, U32>
     for +aad: List<&2, U32>
     for +pt: List<&2, U32>
     for +hk: {List.length(&2, U32, key) == A.key_size(alg) : Nat}
     for +hn: {List.length(&2, U32, nonce) == A.nonce_size(alg) : Nat}
     {decrypt_sealed(alg, key, nonce, aad, A.encrypt(alg, key, nonce, aad, pt)) == Some{pt} : Maybe<&2, List<&2, U32>>}
  Laws.forgery (https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aead/laws.bend&name=forgery)
   # ciphertext || t is rejected for every 16-byte t other than the tag of the
   # ciphertext under this key, nonce and aad.
   law forgery:
     for +alg: A.Alg
     for +key: List<&2, U32>
     for +nonce: List<&2, U32>
     for +aad: List<&2, U32>
     for +ct: List<&2, U32>
     for +t: List<&2, U32>
     for +hk: {List.length(&2, U32, key) == A.key_size(alg) : Nat}
     for +hn: {List.length(&2, U32, nonce) == A.nonce_size(alg) : Nat}
     …
  Laws.seal_layout (https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aead/laws.bend&name=seal_layout)
   # What encrypt returns is a ciphertext followed by its expected tag.
   law seal_layout:
     for +alg: A.Alg
     for +key: List<&2, U32>
     for +nonce: List<&2, U32>
     for +aad: List<&2, U32>
     for +pt: List<&2, U32>
     for +hk: {List.length(&2, U32, key) == A.key_size(alg) : Nat}
     for +hn: {List.length(&2, U32, nonce) == A.nonce_size(alg) : Nat}
     exs ct: List<&2, U32>
     {A.encrypt(alg, key, nonce, aad, pt) == Some{List.append(&2, U32, ct, expected_tag(alg, key, nonce, aad, ct))} : Maybe<&2, List<&2, U32>>}
  Laws.decrypt_sound (https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aead/laws.bend&name=decrypt_sound)
   # Decryption is sound: whatever decrypt accepts is exactly what encrypt
   # produces for the returned plaintext (so every accepted input is the honest
   # ciphertext of its plaintext under this key, nonce and aad).
   law decrypt_sound:
     for +alg: A.Alg
     for +key: List<&2, U32>
     for +nonce: List<&2, U32>
     for +aad: List<&2, U32>
     for +data: List<&2, U32>
     for +p: List<&2, U32>
     for +hk: {List.length(&2, U32, key) == A.key_size(alg) : Nat}
     …
  Proof.when_same (https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aead/proof.bend&name=when_same)
   law when_same:
     for +ok: Bool
     for +x: List<&2, U32>
     {CP.when(ok, x) == A.when_open(ok, Some{x}) : Maybe<&2, List<&2, U32>>}
  Proof.when_open_same (https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aead/proof.bend&name=when_open_same)
   law when_open_same:
     for +ok: Bool
     for +r: Maybe<&2, List<&2, U32>>
     {CP.when_open(ok, r) == A.when_open(ok, r) : Maybe<&2, List<&2, U32>>}
  Proof.valid_true (https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aead/proof.bend&name=valid_true)
   law valid_true:
     for +alg: A.Alg
     for +key: List<&2, U32>
     for +nonce: List<&2, U32>
     for +hk: {List.length(&2, U32, key) == A.key_size(alg) : Nat}
     for +hn: {List.length(&2, U32, nonce) == A.nonce_size(alg) : Nat}
     {A.valid(alg, key, nonce) == True{} : Bool}
  Proof.encrypt_valid (https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aead/proof.bend&name=encrypt_valid)
   law encrypt_valid:
     for +alg: A.Alg
     for +key: List<&2, U32>
     for +nonce: List<&2, U32>
     for +aad: List<&2, U32>
     for +pt: List<&2, U32>
     for +hk: {List.length(&2, U32, key) == A.key_size(alg) : Nat}
     for +hn: {List.length(&2, U32, nonce) == A.nonce_size(alg) : Nat}
     {A.encrypt(alg, key, nonce, aad, pt) == A.seal(alg, key, nonce, aad, pt) : Maybe<&2, List<&2, U32>>}
  Proof.decrypt_valid (https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aead/proof.bend&name=decrypt_valid)
   law decrypt_valid:
     for +alg: A.Alg
     for +key: List<&2, U32>
     for +nonce: List<&2, U32>
     for +aad: List<&2, U32>
     for +data: List<&2, U32>
     for +hk: {List.length(&2, U32, key) == A.key_size(alg) : Nat}
     for +hn: {List.length(&2, U32, nonce) == A.nonce_size(alg) : Nat}
     {A.decrypt(alg, key, nonce, aad, data) == A.open(alg, key, nonce, aad, data) : Maybe<&2, List<&2, U32>>}
  Proof.open_sealed (https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aead/proof.bend&name=open_sealed)
   # decrypt after encrypt is open after seal (on valid lengths).
   def open_sealed(+alg: A.Alg, +key: List<&2, U32>, +nonce: List<&2, U32>, +aad: List<&2, U32>, m: Maybe<&2, List<&2, U32>>) -> Maybe<&2, List<&2, U32>>:
  Proof.ds_open (https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aead/proof.bend&name=ds_open)
   law ds_open:
     for +alg: A.Alg
     for +key: List<&2, U32>
     for +nonce: List<&2, U32>
     for +aad: List<&2, U32>
     for +m: Maybe<&2, List<&2, U32>>
     for +hk: {List.length(&2, U32, key) == A.key_size(alg) : Nat}
     for +hn: {List.length(&2, U32, nonce) == A.nonce_size(alg) : Nat}
     {Laws.decrypt_sealed(alg, key, nonce, aad, m) == open_sealed(alg, key, nonce, aad, m) : Maybe<&2, List<&2, U32>>}
  Proof.os128 (https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aead/proof.bend&name=os128)
   law os128:
     for +key: List<&2, U32>
     for +nonce: List<&2, U32>
     for +aad: List<&2, U32>
     for +m: Maybe<&2, List<&2, U32>>
     {open_sealed(A.AES_128_GCM{}, key, nonce, aad, m) == AE.open128(key, nonce, aad, m) : Maybe<&2, List<&2, U32>>}
  Proof.os256 (https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aead/proof.bend&name=os256)
   law os256:
     for +key: List<&2, U32>
     for +nonce: List<&2, U32>
     for +aad: List<&2, U32>
     for +m: Maybe<&2, List<&2, U32>>
     {open_sealed(A.AES_256_GCM{}, key, nonce, aad, m) == AE.open256(key, nonce, aad, m) : Maybe<&2, List<&2, U32>>}
  Proof.open_seal (https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aead/proof.bend&name=open_seal)
   law open_seal:
     for +alg: A.Alg
     for +key: List<&2, U32>
     for +nonce: List<&2, U32>
     for +aad: List<&2, U32>
     for +pt: List<&2, U32>
     for +hk: {List.length(&2, U32, key) == A.key_size(alg) : Nat}
     for +hn: {List.length(&2, U32, nonce) == A.nonce_size(alg) : Nat}
     {open_sealed(alg, key, nonce, aad, A.seal(alg, key, nonce, aad, pt)) == Some{pt} : Maybe<&2, List<&2, U32>>}
  Proof.open_forged (https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aead/proof.bend&name=open_forged)
   law open_forged:
     for +alg: A.Alg
     for +key: List<&2, U32>
     for +nonce: List<&2, U32>
     for +aad: List<&2, U32>
     for +ct: List<&2, U32>
     for +t: List<&2, U32>
     for +hk: {List.length(&2, U32, key) == A.key_size(alg) : Nat}
     for +hn: {List.length(&2, U32, nonce) == A.nonce_size(alg) : Nat}
     for +ht: {List.length(&2, U32, t) == 16n : Nat}
     for ne: {t != Laws.expected_tag(alg, key, nonce, aad, ct) : List<&2, U32>}
     {A.open(alg, key, nonce, aad, List.append(&2, U32, ct, t)) == None{} : Maybe<&2, List<&2, U32>>}
  Proof.sapp (https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aead/proof.bend&name=sapp)
   def sapp(+ct: List<&2, U32>, +t: List<&2, U32>) -> Maybe<&2, List<&2, U32>>:
  Proof.layout_cp (https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aead/proof.bend&name=layout_cp)
   law layout_cp:
     for +key: List<&2, U32>
     for +nonce: List<&2, U32>
     for +aad: List<&2, U32>
     for +pt: List<&2, U32>
     {A.seal(A.CHACHA20_POLY1305{}, key, nonce, aad, pt) == sapp(CP.encrypt_ct(key, nonce, pt), R.tag(key, nonce, aad, CP.encrypt_ct(key, nonce, pt))) : Maybe<&2, List<&2, U32>>}
  Proof.layout_x (https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aead/proof.bend&name=layout_x)
   law layout_x:
     for +key: List<&2, U32>
     for +nonce: List<&2, U32>
     for +aad: List<&2, U32>
     for +pt: List<&2, U32>
     {A.seal(A.XCHACHA20_POLY1305{}, key, nonce, aad, pt) == sapp(CP.encrypt_ct(CP.xkey(key, nonce), CP.xnonce(nonce), pt), R.tag(RC.xsubkey(key, nonce), RC.xnonce(nonce), aad, CP.encrypt_ct(CP.xkey(key, nonce), CP.xnonce(nonce), pt))) : Maybe<&2, List<&2, U32>>}
  Proof.gct (https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aead/proof.bend&name=gct)
   def gct(+key: List<&2, U32>, +nonce: List<&2, U32>, +pt: List<&2, U32>) -> List<&2, U32>:
  Proof.smaybe (https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aead/proof.bend&name=smaybe)
   def smaybe(+x: List<&2, U32>) -> Maybe<&2, List<&2, U32>>:
  Proof.open_sound (https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aead/proof.bend&name=open_sound)
   law open_sound:
     for +alg: A.Alg
     for +key: List<&2, U32>
     for +nonce: List<&2, U32>
     for +aad: List<&2, U32>
     for +data: List<&2, U32>
     for +p: List<&2, U32>
     for +hk: {List.length(&2, U32, key) == A.key_size(alg) : Nat}
     for +hn: {List.length(&2, U32, nonce) == A.nonce_size(alg) : Nat}
     for +h: {A.open(alg, key, nonce, aad, data) == Some{p} : Maybe<&2, List<&2, U32>>}
     {A.seal(alg, key, nonce, aad, p) == Some{data} : Maybe<&2, List<&2, U32>>}
  Sound.none_some (https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aead/sound.bend&name=none_some)
   law none_some:
     for +p: List<&2, U32>
     for +h: {None{} == Some{p} : Maybe<&2, List<&2, U32>>}
     Empty
  Sound.some_inj (https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aead/sound.bend&name=some_inj)
   law some_inj:
     for +x: List<&2, U32>
     for +p: List<&2, U32>
     for +h: {Some{x} == Some{p} : Maybe<&2, List<&2, U32>>}
     {x == p : List<&2, U32>}
  Sound.prefix_suffix (https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aead/sound.bend&name=prefix_suffix)
   law prefix_suffix:
     for +n: Nat
     for +xs: List<&2, U32>
     {List.append(&2, U32, RC.prefix(n, xs), RC.suffix(n, xs)) == xs : List<&2, U32>}
  Sound.take_drop (https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aead/sound.bend&name=take_drop)
   law take_drop:
     for +xs: List<&2, U32>
     for +n: Nat
     {List.append(&2, U32, List.take(&2, U32, xs, n), List.drop(&2, U32, xs, n)) == xs : List<&2, U32>}
  Sound.csa (https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aead/sound.bend&name=csa)
   def csa(+key: List<&2, U32>, +nonce: List<&2, U32>, +aad: List<&2, U32>, +c: List<&2, U32>) -> List<&2, U32>:
  Sound.c_tag (https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aead/sound.bend&name=c_tag)
   law c_tag:
     for +ok: Bool
     for +key: List<&2, U32>
     for +nonce: List<&2, U32>
     for +aad: List<&2, U32>
     for +ct: List<&2, U32>
     for +t: List<&2, U32>
     for +p: List<&2, U32>
     for +hok: {RS.equal(t, R.tag(key, nonce, aad, ct)) == ok : Bool}
     for +h: {R.open_tag(ok, key, nonce, ct) == Some{p} : Maybe<&2, List<&2, U32>>}
     {R.seal(key, nonce, aad, p) == List.append(&2, U32, ct, t) : List<&2, U32>}
  Sound.c_len (https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aead/sound.bend&name=c_len)
   law c_len:
     for +short: Bool
     for +key: List<&2, U32>
     for +nonce: List<&2, U32>
     for +aad: List<&2, U32>
     for +data: List<&2, U32>
     for +p: List<&2, U32>
     for +h: {R.open_len(short, key, nonce, aad, data) == Some{p} : Maybe<&2, List<&2, U32>>}
     {R.seal(key, nonce, aad, p) == data : List<&2, U32>}
  Sound.chacha_sound (https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aead/sound.bend&name=chacha_sound)
   # Whatever opens to p is the sealing of p.
   law chacha_sound:
     for +key: List<&2, U32>
     for +nonce: List<&2, U32>
     for +aad: List<&2, U32>
     for +data: List<&2, U32>
     for +p: List<&2, U32>
     for +h: {R.open(key, nonce, aad, data) == Some{p} : Maybe<&2, List<&2, U32>>}
     {R.seal(key, nonce, aad, p) == data : List<&2, U32>}
  Sound.gsa (https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aead/sound.bend&name=gsa)
   def gsa(+nk: Nat, +nr: Nat, +key: List<&2, U32>, +iv: List<&2, U32>, +aad: List<&2, U32>, +c: List<&2, U32>) -> List<&2, U32>:
  Sound.g_tag (https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aead/sound.bend&name=g_tag)
   law g_tag:
     for +ok: Bool
     for +nk: Nat
     for +nr: Nat
     for +key: List<&2, U32>
     for +iv: List<&2, U32>
     for +aad: List<&2, U32>
     for +c: List<&2, U32>
     for +t: List<&2, U32>
     for +p: List<&2, U32>
     for +hok: {RS.equal(t, G.tag(nk, nr, key, iv, aad, c)) == ok : Bool}
     …
  Sound.g_len (https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aead/sound.bend&name=g_len)
   law g_len:
     for +short: Bool
     for +nk: Nat
     for +nr: Nat
     for +key: List<&2, U32>
     for +iv: List<&2, U32>
     for +aad: List<&2, U32>
     for +input: List<&2, U32>
     for +p: List<&2, U32>
     for +h: {G.open_split(nk, nr, key, iv, aad, input, List.length(&2, U32, input), short) == Some{p} : Maybe<&2, List<&2, U32>>}
     {G.seal(nk, nr, key, iv, aad, p) == input : List<&2, U32>}
  Sound.gcm_sound (https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aead/sound.bend&name=gcm_sound)
   law gcm_sound:
     for +nk: Nat
     for +nr: Nat
     for +key: List<&2, U32>
     for +iv: List<&2, U32>
     for +aad: List<&2, U32>
     for +input: List<&2, U32>
     for +p: List<&2, U32>
     for +h: {G.open(nk, nr, key, iv, aad, input) == Some{p} : Maybe<&2, List<&2, U32>>}
     {G.seal(nk, nr, key, iv, aad, p) == input : List<&2, U32>}
  SubtleEq.step (https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aead/subtle_eq.bend&name=step)
   law step:
     for +acc: U32
     for +x: U32
     for +y: U32
     for +e: Bool
     {Bool.and(U32.is_eq(U32.or(acc, U32.xor(x, y)), 0), e) == Bool.and(U32.is_eq(acc, 0), Bool.and(U32.is_eq(x, y), e)) : Bool}
  SubtleEq.fold (https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aead/subtle_eq.bend&name=fold)
   law fold:
     for +a: List<&2, U32>
     for +b: List<&2, U32>
     for +acc: U32
     {Bool.and(Nat.is_eq(List.length(&2, U32, a), List.length(&2, U32, b)), U32.is_eq(Subtle.diff(a, b, acc), 0)) ==
       Bool.and(U32.is_eq(acc, 0), SS.equal(a, b)) : Bool}
  SubtleEq.equal_sound (https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aead/subtle_eq.bend&name=equal_sound)
   law equal_sound:
     for +a: List<&2, U32>
     for +b: List<&2, U32>
     for +h: {SS.equal(a, b) == True{} : Bool}
     {a == b : List<&2, U32>}
  SubtleEq.equal_refl (https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aead/subtle_eq.bend&name=equal_refl)
   law equal_refl:
     for +a: List<&2, U32>
     {SS.equal(a, a) == True{} : Bool}
  SubtleEq.eq_value (https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aead/subtle_eq.bend&name=eq_value)
   law eq_value:
     for +a: List<&2, U32>
     for +b: List<&2, U32>
     {Subtle.eq(a, b) == SS.equal(a, b) : Bool}
  Aead.bxor_inv (https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aes/aead.bend&name=bxor_inv)
   def bxor_inv(+x: Bool, +y: Bool) -> {Bool.xor(Bool.xor(x, y), y) == x : Bool}:
  Aead.word_xor_inv (https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aes/aead.bend&name=word_xor_inv)
   def word_xor_inv(+n: Nat, +a: Word(n), +b: Word(n)) -> {Word.xor(n, Word.xor(n, a, b), b) == a : Word(n)}:
  Aead.xor_inv (https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aes/aead.bend&name=xor_inv)
   def xor_inv(+x: U32, +k: U32) -> {U32.xor(U32.xor(x, k), k) == x : U32}:
  Aead.ks_ok (https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aes/aead.bend&name=ks_ok)
   def ks_ok(+st: T.State) -> {S.bytes_of(st) == [S.nth_byte(S.bytes_of(st), 0n), S.nth_byte(S.bytes_of(st), 1n), S.nth_byte(S.bytes_of(st), 2n), S.nth_byte(S.bytes_of(st), 3n), S.nth_byte(S.bytes_of(st), 4n), S.nth_byte(S.bytes_of(st), 5n), S.nth_byte(S.bytes_of(st), 6n), S.nth_byte(S.bytes_of(st), 7n), S.nth_byte(S.bytes_of(st), 8n), S.nth_byte(S.bytes_of(st), 9n), S.nth_byte(S.bytes_of(st), 10n), S.nth_byte(S.bytes_of(st), 11n), S.nth_byte(S.bytes_of(st), 12n), S.nth_byte(S.bytes_of(st), 13n), S.nth_byte(S.bytes_of(st), 14n), S.nth_byte(S.bytes_of(st), 15n)] : List<&2, U32>}:
  Aead.kb (https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aes/aead.bend&name=kb)
   # Byte i of the keystream block of counter block cb.
   def kb(+nk: Nat, +nr: Nat, +key: List<&2, U32>, +cb: List<&2, U32>, +i: Nat) -> U32:
  Aead.cancel16 (https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aes/aead.bend&name=cancel16)
   # (x xor k) xor k == x, position by position.
   def cancel16(+x0: U32, +x1: U32, +x2: U32, +x3: U32, +x4: U32, +x5: U32, +x6: U32, +x7: U32, +x8: U32, +x9: U32, +x10: U32, +x11: U32, +x12: U32, +x13: U32, +x14: U32, +x15: U32, +k0: U32, +k1: U32, +k2: U32, +k3: U32, +k4: U32, +k5: U32, +k6: U32, +k7: U32, +k8: U32, +k9: U32, +k10: U32, +k11: U32, +k12: U32, +k13: U32, +k14: U32, +k15: U32, +r1: List<&2, U32>, +r2: List<&2, U32>, +e: {r1 == r2 : List<&2, U32>}) -> {U32.xor(U32.xor(x0, k0), k0) <> U32.xor(U32.xor(x1, k1), k1) <> U32.xor(U32.xor(x2, k2), k2) <> U32.xor(U32.xor(x3, k3), k3) <> U32.xor(U32.xor(x4, k4), k4) <> U32.xor(U32.xor(x5, k5), k5) <> U32.xor(U32.xor(x6, k6), k6) <> U32.xor(U32.xor(x7, k7), k7) <> U32.xor(U32.xor(x8, k8), k8) <> U32.xor(U32.xor(x9, k9), k9) <> U32.xor(U32.xor(x10, k10), k10) <> U32.xor(U32.xor(x11, k11), k11) <> U32.xor(U32.xor(x12, k12), k12) <> U32.xor(U32.xor(x13, k13), k13) <> U32.xor(U32.xor(x14, k14), k14) <> U32.xor(U32.xor(x15, k15), k15) <> r1 == x0 <> x1 <> x2 <> x3 <> x4 <> x5 <> x6 <> x7 <> x8 <> x9 <> x10 <> x11 <> x12 <> x13 <> x14 <> x15 <> r2 : List<&2, U32>}:
  Aead.cancel1 (https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aes/aead.bend&name=cancel1)
   def cancel1(+x0: U32, +k0: U32) -> {[U32.xor(U32.xor(x0, k0), k0)] == [x0] : List<&2, U32>}:
  Aead.cancel2 (https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aes/aead.bend&name=cancel2)
   def cancel2(+x0: U32, +x1: U32, +k0: U32, +k1: U32) -> {[U32.xor(U32.xor(x0, k0), k0), U32.xor(U32.xor(x1, k1), k1)] == [x0, x1] : List<&2, U32>}:
  Aead.cancel3 (https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aes/aead.bend&name=cancel3)
   def cancel3(+x0: U32, +x1: U32, +x2: U32, +k0: U32, +k1: U32, +k2: U32) -> {[U32.xor(U32.xor(x0, k0), k0), U32.xor(U32.xor(x1, k1), k1), U32.xor(U32.xor(x2, k2), k2)] == [x0, x1, x2] : List<&2, U32>}:
  Aead.cancel4 (https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aes/aead.bend&name=cancel4)
   def cancel4(+x0: U32, +x1: U32, +x2: U32, +x3: U32, +k0: U32, +k1: U32, +k2: U32, +k3: U32) -> {[U32.xor(U32.xor(x0, k0), k0), U32.xor(U32.xor(x1, k1), k1), U32.xor(U32.xor(x2, k2), k2), U32.xor(U32.xor(x3, k3), k3)] == [x0, x1, x2, x3] : List<&2, U32>}:
  Aead.cancel5 (https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aes/aead.bend&name=cancel5)
   def cancel5(+x0: U32, +x1: U32, +x2: U32, +x3: U32, +x4: U32, +k0: U32, +k1: U32, +k2: U32, +k3: U32, +k4: U32) -> {[U32.xor(U32.xor(x0, k0), k0), U32.xor(U32.xor(x1, k1), k1), U32.xor(U32.xor(x2, k2), k2), U32.xor(U32.xor(x3, k3), k3), U32.xor(U32.xor(x4, k4), k4)] == [x0, x1, x2, x3, x4] : List<&2, U32>}:
  Aead.cancel6 (https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aes/aead.bend&name=cancel6)
   def cancel6(+x0: U32, +x1: U32, +x2: U32, +x3: U32, +x4: U32, +x5: U32, +k0: U32, +k1: U32, +k2: U32, +k3: U32, +k4: U32, +k5: U32) -> {[U32.xor(U32.xor(x0, k0), k0), U32.xor(U32.xor(x1, k1), k1), U32.xor(U32.xor(x2, k2), k2), U32.xor(U32.xor(x3, k3), k3), U32.xor(U32.xor(x4, k4), k4), U32.xor(U32.xor(x5, k5), k5)] == [x0, x1, x2, x3, x4, x5] : List<&2, U32>}:
  Aead.cancel7 (https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aes/aead.bend&name=cancel7)
   def cancel7(+x0: U32, +x1: U32, +x2: U32, +x3: U32, +x4: U32, +x5: U32, +x6: U32, +k0: U32, +k1: U32, +k2: U32, +k3: U32, +k4: U32, +k5: U32, +k6: U32) -> {[U32.xor(U32.xor(x0, k0), k0), U32.xor(U32.xor(x1, k1), k1), U32.xor(U32.xor(x2, k2), k2), U32.xor(U32.xor(x3, k3), k3), U32.xor(U32.xor(x4, k4), k4), U32.xor(U32.xor(x5, k5), k5), U32.xor(U32.xor(x6, k6), k6)] == [x0, x1, x2, x3, x4, x5, x6] : List<&2, U32>}:
  Aead.cancel8 (https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aes/aead.bend&name=cancel8)
   def cancel8(+x0: U32, +x1: U32, +x2: U32, +x3: U32, +x4: U32, +x5: U32, +x6: U32, +x7: U32, +k0: U32, +k1: U32, +k2: U32, +k3: U32, +k4: U32, +k5: U32, +k6: U32, +k7: U32) -> {[U32.xor(U32.xor(x0, k0), k0), U32.xor(U32.xor(x1, k1), k1), U32.xor(U32.xor(x2, k2), k2), U32.xor(U32.xor(x3, k3), k3), U32.xor(U32.xor(x4, k4), k4), U32.xor(U32.xor(x5, k5), k5), U32.xor(U32.xor(x6, k6), k6), U32.xor(U32.xor(x7, k7), k7)] == [x0, x1, x2, x3, x4, x5, x6, x7] : List<&2, U32>}:
  Aead.cancel9 (https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aes/aead.bend&name=cancel9)
   def cancel9(+x0: U32, +x1: U32, +x2: U32, +x3: U32, +x4: U32, +x5: U32, +x6: U32, +x7: U32, +x8: U32, +k0: U32, +k1: U32, +k2: U32, +k3: U32, +k4: U32, +k5: U32, +k6: U32, +k7: U32, +k8: U32) -> {[U32.xor(U32.xor(x0, k0), k0), U32.xor(U32.xor(x1, k1), k1), U32.xor(U32.xor(x2, k2), k2), U32.xor(U32.xor(x3, k3), k3), U32.xor(U32.xor(x4, k4), k4), U32.xor(U32.xor(x5, k5), k5), U32.xor(U32.xor(x6, k6), k6), U32.xor(U32.xor(x7, k7), k7), U32.xor(U32.xor(x8, k8), k8)] == [x0, x1, x2, x3, x4, x5, x6, x7, x8] : List<&2, U32>}:
  Aead.cancel10 (https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aes/aead.bend&name=cancel10)
   def cancel10(+x0: U32, +x1: U32, +x2: U32, +x3: U32, +x4: U32, +x5: U32, +x6: U32, +x7: U32, +x8: U32, +x9: U32, +k0: U32, +k1: U32, +k2: U32, +k3: U32, +k4: U32, +k5: U32, +k6: U32, +k7: U32, +k8: U32, +k9: U32) -> {[U32.xor(U32.xor(x0, k0), k0), U32.xor(U32.xor(x1, k1), k1), U32.xor(U32.xor(x2, k2), k2), U32.xor(U32.xor(x3, k3), k3), U32.xor(U32.xor(x4, k4), k4), U32.xor(U32.xor(x5, k5), k5), U32.xor(U32.xor(x6, k6), k6), U32.xor(U32.xor(x7, k7), k7), U32.xor(U32.xor(x8, k8), k8), U32.xor(U32.xor(x9, k9), k9)] == [x0, x1, x2, x3, x4, x5, x6, x7, x8, x9] : List<&2, U32>}:
  Aead.cancel11 (https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aes/aead.bend&name=cancel11)
   def cancel11(+x0: U32, +x1: U32, +x2: U32, +x3: U32, +x4: U32, +x5: U32, +x6: U32, +x7: U32, +x8: U32, +x9: U32, +x10: U32, +k0: U32, +k1: U32, +k2: U32, +k3: U32, +k4: U32, +k5: U32, +k6: U32, +k7: U32, +k8: U32, +k9: U32, +k10: U32) -> {[U32.xor(U32.xor(x0, k0), k0), U32.xor(U32.xor(x1, k1), k1), U32.xor(U32.xor(x2, k2), k2), U32.xor(U32.xor(x3, k3), k3), U32.xor(U32.xor(x4, k4), k4), U32.xor(U32.xor(x5, k5), k5), U32.xor(U32.xor(x6, k6), k6), U32.xor(U32.xor(x7, k7), k7), U32.xor(U32.xor(x8, k8), k8), U32.xor(U32.xor(x9, k9), k9), U32.xor(U32.xor(x10, k10), k10)] == [x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10] : List<&2, U32>}:
More: https://jend.leeeet.dev/packages/bend-collections-laws-crypto.txt?definitions_offset=100