import Base
import ../../lib/logic.bend as L
import ../../../src/crypto/aes/types.bend as T
import ../../../src/crypto/aes/aes.bend as A
import ../../../src/crypto/aes/gcm.bend as GI
import ../../../src/crypto/aesgcm.bend as GCM
import ../../../spec/crypto/aes/aes.bend as S
import ../../../spec/crypto/aes/gcm.bend as G
import ./laws.bend as Laws
import ./sbox.bend as SB
import ./inverse.bend as INV
import ./cipher.bend as C
import ./gcm.bend as GP
import ./aead.bend as AD
import ./api.bend as API

# Generated by tools/generators/aes/proof.py.

# Gate for AES and AES-GCM: `bend proofs/crypto/aes/proof.bend` checks every
# clause of laws.bend, for every input:
#   sbox.bend    the S-box circuit and the doublings, on all 256 bytes
#   cipher.bend  SubBytes .. AddRoundKey, the rounds, KeyExpansion, Cipher
#   gf.bend      polynomial product mod m == Algorithm 1 (any modulus)
#   ghash*.bend  the word-level GHASH == SP 800-38D's GHASH
#   gcm.bend     GCTR, the tag, GCM-AE and GCM-AD == SP 800-38D
#   aead.bend    open(seal(x)) == Some(x); a wrong tag gives None
# The key size stays symbolic (Nk = length/4) so that no key expansion is
# ever unfolded at a concrete size.

# A nonce that is not 12 bytes long: None.
def seal_nonce_bad(+sched: A.Schedule, +nonce: List<&2, U32>, +h: {Nat.is_eq(List.length(&2, U32, nonce), 12n) == False{} : Bool}, +aad: List<&2, U32>, +pt: List<&2, U32>) -> {GI.seal_nonce(sched, nonce, aad, pt) == None{} : Maybe<&2, List<&2, U32>>}:
  match nonce:
    case Nil{}:
      {==}
    case n0 <> Nil{}:
      {==}
    case n0 <> n1 <> Nil{}:
      {==}
    case n0 <> n1 <> n2 <> Nil{}:
      {==}
    case n0 <> n1 <> n2 <> n3 <> Nil{}:
      {==}
    case n0 <> n1 <> n2 <> n3 <> n4 <> Nil{}:
      {==}
    case n0 <> n1 <> n2 <> n3 <> n4 <> n5 <> Nil{}:
      {==}
    case n0 <> n1 <> n2 <> n3 <> n4 <> n5 <> n6 <> Nil{}:
      {==}
    case n0 <> n1 <> n2 <> n3 <> n4 <> n5 <> n6 <> n7 <> Nil{}:
      {==}
    case n0 <> n1 <> n2 <> n3 <> n4 <> n5 <> n6 <> n7 <> n8 <> Nil{}:
      {==}
    case n0 <> n1 <> n2 <> n3 <> n4 <> n5 <> n6 <> n7 <> n8 <> n9 <> Nil{}:
      {==}
    case n0 <> n1 <> n2 <> n3 <> n4 <> n5 <> n6 <> n7 <> n8 <> n9 <> n10 <> Nil{}:
      {==}
    case n0 <> n1 <> n2 <> n3 <> n4 <> n5 <> n6 <> n7 <> n8 <> n9 <> n10 <> n11 <> Nil{}:
      Empty.absurd({GI.seal_nonce(sched, [n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11], aad, pt) == None{} : Maybe<&2, List<&2, U32>>}, L.true_false(h))
    case n0 <> n1 <> n2 <> n3 <> n4 <> n5 <> n6 <> n7 <> n8 <> n9 <> n10 <> n11 <> n12 <> rest:
      {==}

def open_nonce_bad(+sched: A.Schedule, +nonce: List<&2, U32>, +h: {Nat.is_eq(List.length(&2, U32, nonce), 12n) == False{} : Bool}, +aad: List<&2, U32>, +ct: List<&2, U32>) -> {GI.open_nonce(sched, nonce, aad, ct) == None{} : Maybe<&2, List<&2, U32>>}:
  match nonce:
    case Nil{}:
      {==}
    case n0 <> Nil{}:
      {==}
    case n0 <> n1 <> Nil{}:
      {==}
    case n0 <> n1 <> n2 <> Nil{}:
      {==}
    case n0 <> n1 <> n2 <> n3 <> Nil{}:
      {==}
    case n0 <> n1 <> n2 <> n3 <> n4 <> Nil{}:
      {==}
    case n0 <> n1 <> n2 <> n3 <> n4 <> n5 <> Nil{}:
      {==}
    case n0 <> n1 <> n2 <> n3 <> n4 <> n5 <> n6 <> Nil{}:
      {==}
    case n0 <> n1 <> n2 <> n3 <> n4 <> n5 <> n6 <> n7 <> Nil{}:
      {==}
    case n0 <> n1 <> n2 <> n3 <> n4 <> n5 <> n6 <> n7 <> n8 <> Nil{}:
      {==}
    case n0 <> n1 <> n2 <> n3 <> n4 <> n5 <> n6 <> n7 <> n8 <> n9 <> Nil{}:
      {==}
    case n0 <> n1 <> n2 <> n3 <> n4 <> n5 <> n6 <> n7 <> n8 <> n9 <> n10 <> Nil{}:
      {==}
    case n0 <> n1 <> n2 <> n3 <> n4 <> n5 <> n6 <> n7 <> n8 <> n9 <> n10 <> n11 <> Nil{}:
      Empty.absurd({GI.open_nonce(sched, [n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11], aad, ct) == None{} : Maybe<&2, List<&2, U32>>}, L.true_false(h))
    case n0 <> n1 <> n2 <> n3 <> n4 <> n5 <> n6 <> n7 <> n8 <> n9 <> n10 <> n11 <> n12 <> rest:
      {==}

def seal_key_bad(+m: Maybe<&2, A.Schedule>, +nonce: List<&2, U32>, +h: {Nat.is_eq(List.length(&2, U32, nonce), 12n) == False{} : Bool}, +aad: List<&2, U32>, +pt: List<&2, U32>) -> {GI.seal_key(m, nonce, aad, pt) == None{} : Maybe<&2, List<&2, U32>>}:
  match m:
    case None{}:
      {==}
    case Some{s}:
      seal_nonce_bad(s, nonce, h, aad, pt)

def open_key_bad(+m: Maybe<&2, A.Schedule>, +nonce: List<&2, U32>, +h: {Nat.is_eq(List.length(&2, U32, nonce), 12n) == False{} : Bool}, +aad: List<&2, U32>, +ct: List<&2, U32>) -> {GI.open_key(m, nonce, aad, ct) == None{} : Maybe<&2, List<&2, U32>>}:
  match m:
    case None{}:
      {==}
    case Some{s}:
      open_nonce_bad(s, nonce, h, aad, ct)

# A key of w bytes, w one of 16, 24, 32, passes the length check.
def valid_of(+key: List<&2, U32>, +w: Nat, +h: {List.length(&2, U32, key) == w : Nat}, +v: {A.valid_length(w) == True{} : Bool}) -> {A.valid_length(List.length(&2, U32, key)) == True{} : Bool}:
  %Equal.sym(Nat, List.length(&2, U32, key), w, h) : {A.valid_length(_) == True{} : Bool}
  v

def Laws.Sbox.value(x):
  SB.sbox_ok(x)

def Laws.Inverse.unit(x, h):
  INV.inverse_unit(x, h)

def Laws.Inverse.zero():
  INV.inverse_zero()

def Laws.Cipher.value(nk, nr, key, s):
  C.encrypt_ok(nk, nr, key, s)

def Laws.Block.value(key, h, b0, b1, b2, b3, b4, b5, b6, b7, b8, b9, b10, b11, b12, b13, b14, b15):
  %Equal.sym(Bool, A.valid_length(List.length(&2, U32, key)), True{}, h) : {Laws.block_with(A.schedule_if(_, Nat.div(List.length(&2, U32, key), 4n), key), [b0, b1, b2, b3, b4, b5, b6, b7, b8, b9, b10, b11, b12, b13, b14, b15]) == Some{S.bytes_of(S.aes(key, S.state_of([b0, b1, b2, b3, b4, b5, b6, b7, b8, b9, b10, b11, b12, b13, b14, b15])))} : Maybe<&2, List<&2, U32>>}
  %C.encrypt_ok(S.nk(key), S.nr(key), key, T.S{T.W{b0, b1, b2, b3}, T.W{b4, b5, b6, b7}, T.W{b8, b9, b10, b11}, T.W{b12, b13, b14, b15}}) : {Laws.block_with(A.schedule_if(True{}, Nat.div(List.length(&2, U32, key), 4n), key), [b0, b1, b2, b3, b4, b5, b6, b7, b8, b9, b10, b11, b12, b13, b14, b15]) == Some{S.bytes_of(_)} : Maybe<&2, List<&2, U32>>}
  %GP.bytes_of_ok(A.encrypt(S.nk(key), S.nr(key), key, T.S{T.W{b0, b1, b2, b3}, T.W{b4, b5, b6, b7}, T.W{b8, b9, b10, b11}, T.W{b12, b13, b14, b15}})) : {Laws.block_with(A.schedule_if(True{}, Nat.div(List.length(&2, U32, key), 4n), key), [b0, b1, b2, b3, b4, b5, b6, b7, b8, b9, b10, b11, b12, b13, b14, b15]) == Some{_} : Maybe<&2, List<&2, U32>>}
  {==}

def Laws.Block.aes128(key, h):
  %Equal.sym(Nat, List.length(&2, U32, key), 16n, h) : {Nat.div(_, 4n) == 4n : Nat}
  {==}

def Laws.Block.aes192(key, h):
  %Equal.sym(Nat, List.length(&2, U32, key), 24n, h) : {Nat.div(_, 4n) == 6n : Nat}
  {==}

def Laws.Block.aes256(key, h):
  %Equal.sym(Nat, List.length(&2, U32, key), 32n, h) : {Nat.div(_, 4n) == 8n : Nat}
  {==}

def Laws.Gcm.seal(nk, nr, key, n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11, aad, pt):
  GP.seal_ok(nk, nr, key, T.W{n0, n1, n2, n3}, T.W{n4, n5, n6, n7}, T.W{n8, n9, n10, n11}, aad, pt)

def Laws.Gcm.open(nk, nr, key, n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11, aad, input):
  GP.open_ok(nk, nr, key, T.W{n0, n1, n2, n3}, T.W{n4, n5, n6, n7}, T.W{n8, n9, n10, n11}, aad, input)

def Laws.Aead.roundtrip(nk, nr, key, iv, aad, pt):
  AD.roundtrip(nk, nr, key, iv, aad, pt)

def Laws.Aead.forgery(nk, nr, key, iv, aad, c, t0, t1, t2, t3, t4, t5, t6, t7, t8, t9, t10, t11, t12, t13, t14, t15, ne):
  AD.forgery(nk, nr, key, iv, aad, c, t0, t1, t2, t3, t4, t5, t6, t7, t8, t9, t10, t11, t12, t13, t14, t15, ne)

def Laws.Api128.encrypt(key, h, n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11, aad, pt):
  API.aes128_encrypt(key, h, n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11, aad, pt)

def Laws.Api128.decrypt(key, h, n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11, aad, ct):
  API.aes128_decrypt(key, h, n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11, aad, ct)

law open128_same:
  for +key: List<&2, U32>
  for +nonce: List<&2, U32>
  for +aad: List<&2, U32>
  for +m: Maybe<&2, List<&2, U32>>
  {Laws.open128(key, nonce, aad, m) == API.open128(key, nonce, aad, m) : Maybe<&2, List<&2, U32>>}

def open128_same(key, nonce, aad, m):
  match m:
    case None{}: {==}
    case Some{c}: {==}

def Laws.Api128.roundtrip(key, h, n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11, aad, pt):
  +m = GCM.aes128_gcm_encrypt(key, [n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11], aad, pt)
  Equal.trans(Maybe<&2, List<&2, U32>>, Laws.open128(key, [n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11], aad, m), API.open128(key, [n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11], aad, m), Some{pt}, open128_same(key, [n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11], aad, m), API.aes128_roundtrip(key, h, n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11, aad, pt))

def Laws.Api128.forgery(key, h, n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11, aad, c, t0, t1, t2, t3, t4, t5, t6, t7, t8, t9, t10, t11, t12, t13, t14, t15, ne):
  API.aes128_forgery(key, h, n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11, aad, c, t0, t1, t2, t3, t4, t5, t6, t7, t8, t9, t10, t11, t12, t13, t14, t15, ne)

def Laws.Api128.bad_key(key, h, nonce, aad, pt):
  %Equal.sym(Bool, Nat.is_eq(List.length(&2, U32, key), 16n), False{}, h) : {GI.seal_key(GI.schedule_if(_, key), nonce, aad, pt) == None{} : Maybe<&2, List<&2, U32>>}
  {==}

def Laws.Api128.bad_key_open(key, h, nonce, aad, ct):
  %Equal.sym(Bool, Nat.is_eq(List.length(&2, U32, key), 16n), False{}, h) : {GI.open_key(GI.schedule_if(_, key), nonce, aad, ct) == None{} : Maybe<&2, List<&2, U32>>}
  {==}

def Laws.Api128.bad_nonce(key, nonce, h, aad, pt):
  seal_key_bad(GI.schedule_of(16n, key), nonce, h, aad, pt)

def Laws.Api128.bad_nonce_open(key, nonce, h, aad, ct):
  open_key_bad(GI.schedule_of(16n, key), nonce, h, aad, ct)

def Laws.Api256.encrypt(key, h, n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11, aad, pt):
  API.aes256_encrypt(key, h, n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11, aad, pt)

def Laws.Api256.decrypt(key, h, n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11, aad, ct):
  API.aes256_decrypt(key, h, n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11, aad, ct)

law open256_same:
  for +key: List<&2, U32>
  for +nonce: List<&2, U32>
  for +aad: List<&2, U32>
  for +m: Maybe<&2, List<&2, U32>>
  {Laws.open256(key, nonce, aad, m) == API.open256(key, nonce, aad, m) : Maybe<&2, List<&2, U32>>}

def open256_same(key, nonce, aad, m):
  match m:
    case None{}: {==}
    case Some{c}: {==}

def Laws.Api256.roundtrip(key, h, n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11, aad, pt):
  +m = GCM.aes256_gcm_encrypt(key, [n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11], aad, pt)
  Equal.trans(Maybe<&2, List<&2, U32>>, Laws.open256(key, [n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11], aad, m), API.open256(key, [n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11], aad, m), Some{pt}, open256_same(key, [n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11], aad, m), API.aes256_roundtrip(key, h, n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11, aad, pt))

def Laws.Api256.forgery(key, h, n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11, aad, c, t0, t1, t2, t3, t4, t5, t6, t7, t8, t9, t10, t11, t12, t13, t14, t15, ne):
  API.aes256_forgery(key, h, n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11, aad, c, t0, t1, t2, t3, t4, t5, t6, t7, t8, t9, t10, t11, t12, t13, t14, t15, ne)

def Laws.Api256.bad_key(key, h, nonce, aad, pt):
  %Equal.sym(Bool, Nat.is_eq(List.length(&2, U32, key), 32n), False{}, h) : {GI.seal_key(GI.schedule_if(_, key), nonce, aad, pt) == None{} : Maybe<&2, List<&2, U32>>}
  {==}

def Laws.Api256.bad_key_open(key, h, nonce, aad, ct):
  %Equal.sym(Bool, Nat.is_eq(List.length(&2, U32, key), 32n), False{}, h) : {GI.open_key(GI.schedule_if(_, key), nonce, aad, ct) == None{} : Maybe<&2, List<&2, U32>>}
  {==}

def Laws.Api256.bad_nonce(key, nonce, h, aad, pt):
  seal_key_bad(GI.schedule_of(32n, key), nonce, h, aad, pt)

def Laws.Api256.bad_nonce_open(key, nonce, h, aad, ct):
  open_key_bad(GI.schedule_of(32n, key), nonce, h, aad, ct)