Aead.gctr_part15: def of bend-collections-laws-crypto@1.0.0.0
Import: import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aes/aead.bend as Aead
Lines 300-302 of bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aes/aead.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aes/aead.bend&start_line=300&end_line=302

import Base
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/aes/aes.bend as S
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/aes/gcm.bend as G

def gctr_part15(+nk: Nat, +nr: Nat, +key: List<&2, U32>, +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, +cb: List<&2, U32>) -> {G.gctr(nk, nr, key, [x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14], cb) == [U32.xor(x0, kb(nk, nr, key, cb, 0n)), U32.xor(x1, kb(nk, nr, key, cb, 1n)), U32.xor(x2, kb(nk, nr, key, cb, 2n)), U32.xor(x3, kb(nk, nr, key, cb, 3n)), U32.xor(x4, kb(nk, nr, key, cb, 4n)), U32.xor(x5, kb(nk, nr, key, cb, 5n)), U32.xor(x6, kb(nk, nr, key, cb, 6n)), U32.xor(x7, kb(nk, nr, key, cb, 7n)), U32.xor(x8, kb(nk, nr, key, cb, 8n)), U32.xor(x9, kb(nk, nr, key, cb, 9n)), U32.xor(x10, kb(nk, nr, key, cb, 10n)), U32.xor(x11, kb(nk, nr, key, cb, 11n)), U32.xor(x12, kb(nk, nr, key, cb, 12n)), U32.xor(x13, kb(nk, nr, key, cb, 13n)), U32.xor(x14, kb(nk, nr, key, cb, 14n))] : List<&2, U32>}:
  %Equal.sym(List<&2, U32>, S.bytes_of(S.encrypt(nk, nr, key, S.state_of(cb))), [S.nth_byte(S.bytes_of(S.encrypt(nk, nr, key, S.state_of(cb))), 0n), S.nth_byte(S.bytes_of(S.encrypt(nk, nr, key, S.state_of(cb))), 1n), S.nth_byte(S.bytes_of(S.encrypt(nk, nr, key, S.state_of(cb))), 2n), S.nth_byte(S.bytes_of(S.encrypt(nk, nr, key, S.state_of(cb))), 3n), S.nth_byte(S.bytes_of(S.encrypt(nk, nr, key, S.state_of(cb))), 4n), S.nth_byte(S.bytes_of(S.encrypt(nk, nr, key, S.state_of(cb))), 5n), S.nth_byte(S.bytes_of(S.encrypt(nk, nr, key, S.state_of(cb))), 6n), S.nth_byte(S.bytes_of(S.encrypt(nk, nr, key, S.state_of(cb))), 7n), S.nth_byte(S.bytes_of(S.encrypt(nk, nr, key, S.state_of(cb))), 8n), S.nth_byte(S.bytes_of(S.encrypt(nk, nr, key, S.state_of(cb))), 9n), S.nth_byte(S.bytes_of(S.encrypt(nk, nr, key, S.state_of(cb))), 10n), S.nth_byte(S.bytes_of(S.encrypt(nk, nr, key, S.state_of(cb))), 11n), S.nth_byte(S.bytes_of(S.encrypt(nk, nr, key, S.state_of(cb))), 12n), S.nth_byte(S.bytes_of(S.encrypt(nk, nr, key, S.state_of(cb))), 13n), S.nth_byte(S.bytes_of(S.encrypt(nk, nr, key, S.state_of(cb))), 14n), S.nth_byte(S.bytes_of(S.encrypt(nk, nr, key, S.state_of(cb))), 15n)], ks_ok(S.encrypt(nk, nr, key, S.state_of(cb)))) : {G.xor_bytes([x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14], _) == [U32.xor(x0, kb(nk, nr, key, cb, 0n)), U32.xor(x1, kb(nk, nr, key, cb, 1n)), U32.xor(x2, kb(nk, nr, key, cb, 2n)), U32.xor(x3, kb(nk, nr, key, cb, 3n)), U32.xor(x4, kb(nk, nr, key, cb, 4n)), U32.xor(x5, kb(nk, nr, key, cb, 5n)), U32.xor(x6, kb(nk, nr, key, cb, 6n)), U32.xor(x7, kb(nk, nr, key, cb, 7n)), U32.xor(x8, kb(nk, nr, key, cb, 8n)), U32.xor(x9, kb(nk, nr, key, cb, 9n)), U32.xor(x10, kb(nk, nr, key, cb, 10n)), U32.xor(x11, kb(nk, nr, key, cb, 11n)), U32.xor(x12, kb(nk, nr, key, cb, 12n)), U32.xor(x13, kb(nk, nr, key, cb, 13n)), U32.xor(x14, kb(nk, nr, key, cb, 14n))] : List<&2, U32>}
  {==}

Uses (13):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.xor
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aes/aead.bend&name=kb
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aes/aead.bend&name=ks_ok
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/aes/aes.bend&name=bytes_of
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/aes/aes.bend&name=encrypt
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/aes/aes.bend&name=nth_byte
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/aes/aes.bend&name=state_of
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/aes/gcm.bend&name=gctr
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/aes/gcm.bend&name=xor_bytes