module Spec.Agile.AEAD

open FStar.Integers

module S = FStar.Seq

#set-options "--max_fuel 0 --max_ifuel 0"

let vale_alg_of_alg (a: alg { a = AES128_GCM \/ a = AES256_GCM }) =
  match a with
  | AES128_GCM -> Vale.AES.AES_s.AES_128
  | AES256_GCM -> Vale.AES.AES_s.AES_256

// For gctr_encrypt_recursive and its pattern!
friend Vale.AES.GCTR

#push-options "--max_ifuel 1"
let gcm_encrypt_tag_length alg key iv plain auth: Lemma
  (requires
    Vale.AES.AES_s.is_aes_key alg key /\
    S.length plain < Vale.Def.Words_s.pow2_32 /\
    S.length auth < Vale.Def.Words_s.pow2_32)
  (ensures (
    let c, t = Vale.AES.GCM_s.gcm_encrypt_LE alg key iv plain auth in
    S.length t = 16))
=
  Vale.AES.GCM_s.gcm_encrypt_LE_reveal ()

let gcm_encrypt_cipher_length alg key iv plain auth: Lemma
  (requires
    Vale.AES.AES_s.is_aes_key alg key /\
    S.length plain < Vale.Def.Words_s.pow2_32 /\
    S.length auth < Vale.Def.Words_s.pow2_32)
  (ensures (
    let c, t = Vale.AES.GCM_s.gcm_encrypt_LE alg key iv plain auth in
    S.length c = S.length plain))
=
  Vale.AES.GCM_s.gcm_encrypt_LE_reveal ()
#pop-options

// TODO remove me once seq_uint8_to_seq_nat8 takes Lib.IntTypes.uint8
friend Lib.IntTypes

#push-options "--z3rlimit 20"
let encrypt #a kv iv ad plain =
  match a with
  | CHACHA20_POLY1305 ->
      Spec.Chacha20Poly1305.aead_encrypt kv iv plain ad

  | AES128_GCM | AES256_GCM ->
      // This step needs friend'ing.
      let kv_nat = Vale.Def.Words.Seq_s.seq_uint8_to_seq_nat8 kv in
      // The specification of gcm_encrypt_LE takes care of computing a valid
      // GCM iv from an arbitrary length iv. Hence the iv is the sequence of bytes
      let iv_nat = Vale.Def.Words.Seq_s.seq_uint8_to_seq_nat8 iv in
      // `ad` is called `auth` in Vale world; "additional data", "authenticated
      // data", potato, potato
      let ad_nat = Vale.Def.Words.Seq_s.seq_uint8_to_seq_nat8 ad in
      let plain_nat = Vale.Def.Words.Seq_s.seq_uint8_to_seq_nat8 plain in
      let cipher_nat, tag_nat =
        Vale.AES.GCM_s.gcm_encrypt_LE (vale_alg_of_alg a) kv_nat iv_nat plain_nat ad_nat
      in
      let cipher = Vale.Def.Words.Seq_s.seq_nat8_to_seq_uint8 cipher_nat in
      let tag = Vale.Def.Words.Seq_s.seq_nat8_to_seq_uint8 tag_nat in
      gcm_encrypt_tag_length (vale_alg_of_alg a) kv_nat iv_nat plain_nat ad_nat;
      gcm_encrypt_cipher_length (vale_alg_of_alg a) kv_nat iv_nat plain_nat ad_nat;
      // one more spec discrepancy: Vale returns the cipher and tag separated,
      // while HACL* bundles them together; another arbitrary choice here
      Seq.append cipher tag
#pop-options

#push-options "--max_ifuel 1"
let gcm_decrypt_cipher_length alg key iv plain auth tag: Lemma
  (requires
    Vale.AES.AES_s.is_aes_key alg key /\
    S.length plain < Vale.Def.Words_s.pow2_32 /\
    S.length auth < Vale.Def.Words_s.pow2_32)
  (ensures (
    let c, t = Vale.AES.GCM_s.gcm_decrypt_LE alg key iv plain auth tag in
    S.length c = S.length plain))
=
  Vale.AES.GCM_s.gcm_decrypt_LE_reveal ()
#pop-options

// Note: bundling cipher and tag together is a pain...
#push-options "--z3rlimit 20"
let decrypt #a kv iv ad cipher =
  let tag = S.slice cipher (S.length cipher - tag_length a) (S.length cipher) in
  let cipher = S.slice cipher 0 (S.length cipher - tag_length a) in
  match a with
  | CHACHA20_POLY1305 ->
      Spec.Chacha20Poly1305.aead_decrypt kv iv cipher tag ad

  | AES128_GCM | AES256_GCM ->
      let kv_nat = Vale.Def.Words.Seq_s.seq_uint8_to_seq_nat8 kv in
      let iv_nat = Vale.Def.Words.Seq_s.seq_uint8_to_seq_nat8 iv in
      let ad_nat = Vale.Def.Words.Seq_s.seq_uint8_to_seq_nat8 ad in
      let cipher_nat = Vale.Def.Words.Seq_s.seq_uint8_to_seq_nat8 cipher in
      let tag_nat = Vale.Def.Words.Seq_s.seq_uint8_to_seq_nat8 tag in
      let plain_nat, success =
        Vale.AES.GCM_s.gcm_decrypt_LE (vale_alg_of_alg a) kv_nat iv_nat cipher_nat ad_nat tag_nat
      in
      gcm_decrypt_cipher_length (vale_alg_of_alg a) kv_nat iv_nat cipher_nat ad_nat tag_nat;
      let plain = Vale.Def.Words.Seq_s.seq_nat8_to_seq_uint8 plain_nat in
      if success then Some plain else None
#pop-options

// Admitted until we prove correctness of individual algorithms
let correctness #a k n aad p =
  admit()