val finish_cipher_opt (alg:algorithm) (input plain t0 t1 out:quad32) (round_keys:seq quad32) : Lemma
  (requires length round_keys == (nr alg) + 1 /\
            length round_keys > 0 /\ nr alg > 1 /\   // REVIEW: Why are these needed?
            t0 = quad32_xor input (index round_keys 0) /\
            t1 = eval_rounds t0 round_keys (nr alg - 1) /\
            out = quad32_xor (sub_bytes (shift_rows_LE t1)) (quad32_xor plain (index round_keys (nr alg))))
  (ensures out == quad32_xor plain (eval_cipher alg input round_keys))
let finish_cipher_opt (alg:algorithm) (input plain t0 t1 out:quad32) (round_keys:seq quad32) : Lemma
  (requires length round_keys == (nr alg) + 1 /\
            length round_keys > 0 /\ nr alg > 1 /\   // REVIEW: Why are these needed?
            t0 = quad32_xor input (index round_keys 0) /\
            t1 = eval_rounds t0 round_keys (nr alg - 1) /\
            out = quad32_xor (sub_bytes (shift_rows_LE t1)) (quad32_xor plain (index round_keys (nr alg))))
  (ensures out == quad32_xor plain (eval_cipher alg input round_keys))
  =
  calc (==) {
    out;
    == {} // From requires
    quad32_xor (sub_bytes (shift_rows_LE t1)) (quad32_xor plain (index round_keys (nr alg)));
    == { Vale.Arch.TypesNative.lemma_quad32_xor_commutes plain (index round_keys (nr alg)) }
    quad32_xor (sub_bytes (shift_rows_LE t1)) (quad32_xor (index round_keys (nr alg)) plain);
    == { Vale.Arch.TypesNative.lemma_quad32_xor_associates (sub_bytes (shift_rows_LE t1)) (index round_keys (nr alg)) plain }
    quad32_xor (quad32_xor (sub_bytes (shift_rows_LE t1)) (index round_keys (nr alg))) plain;
    == { eval_rounds_reveal ();
         eval_cipher_reveal ();
         commute_sub_bytes_shift_rows_forall();
         quad32_xor_reveal ()
       }
    quad32_xor (eval_cipher alg input round_keys) plain;
    == { Vale.Arch.TypesNative.lemma_quad32_xor_commutes plain (eval_cipher alg input round_keys) }
    quad32_xor plain (eval_cipher alg input round_keys);
  };
  ()
val finish_cipher_opt (alg:algorithm) (input plain t0 t1 out:quad32) (round_keys:seq quad32) : Lemma
  (requires length round_keys == (nr alg) + 1 /\
            length round_keys > 0 /\ nr alg > 1 /\   // REVIEW: Why are these needed?
            t0 = quad32_xor input (index round_keys 0) /\
            t1 = eval_rounds t0 round_keys (nr alg - 1) /\
            out = quad32_xor (sub_bytes (shift_rows_LE t1)) (quad32_xor plain (index round_keys (nr alg))))
  (ensures out == quad32_xor plain (eval_cipher alg input round_keys))
let finish_cipher_opt (alg: algorithm) (input plain t0 t1 out: quad32) (round_keys: seq quad32)
    : Lemma
      (requires
        length round_keys == (nr alg) + 1 /\ length round_keys > 0 /\ nr alg > 1 /\
        t0 = quad32_xor input (index round_keys 0) /\ t1 = eval_rounds t0 round_keys (nr alg - 1) /\
        out =
        quad32_xor (sub_bytes (shift_rows_LE t1)) (quad32_xor plain (index round_keys (nr alg))))
      (ensures out == quad32_xor plain (eval_cipher alg input round_keys)) =
calc ( == ) {
  out;
  ( == ) { () }
  quad32_xor (sub_bytes (shift_rows_LE t1)) (quad32_xor plain (index round_keys (nr alg)));
  ( == ) { Vale.Arch.TypesNative.lemma_quad32_xor_commutes plain (index round_keys (nr alg)) }
  quad32_xor (sub_bytes (shift_rows_LE t1)) (quad32_xor (index round_keys (nr alg)) plain);
  ( == ) { Vale.Arch.TypesNative.lemma_quad32_xor_associates (sub_bytes (shift_rows_LE t1))
    (index round_keys (nr alg))
    plain }
  quad32_xor (quad32_xor (sub_bytes (shift_rows_LE t1)) (index round_keys (nr alg))) plain;
  ( == ) { (eval_rounds_reveal ();
    eval_cipher_reveal ();
    commute_sub_bytes_shift_rows_forall ();
    quad32_xor_reveal ()) }
  quad32_xor (eval_cipher alg input round_keys) plain;
  ( == ) { Vale.Arch.TypesNative.lemma_quad32_xor_commutes plain (eval_cipher alg input round_keys) }
  quad32_xor plain (eval_cipher alg input round_keys);
};
()
Vale.AES.AES_helpers.fst.checked
Vale.Lib.Seqs_s.fst.checked Vale.Def.Words_s.fsti.checked Vale.Def.Words.Seq_s.fsti.checked Vale.Def.Words.Four_s.fsti.checked Vale.Def.Types_s.fst.checked Vale.Def.Opaque_s.fsti.checked Vale.Arch.TypesNative.fsti.checked Vale.Arch.Types.fsti.checked Vale.AES.GCTR_s.fst.checked Vale.AES.AES_s.fst.checked prims.fst.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.Classical.fsti.checked FStar.Calc.fsti.checked
Vale.AES.AES_helpers.fst
Vale.AES.AES_common_s.algorithm Vale.Def.Types_s.quad32 FStar.Seq.Base.seq Prims.unit FStar.Calc.calc_finish Prims.eq2 Vale.Def.Types_s.quad32_xor Vale.AES.AES_s.eval_cipher Prims.Cons FStar.Preorder.relation Prims.Nil FStar.Calc.calc_step Vale.AES.AES_common_s.sub_bytes Vale.AES.AES_s.shift_rows_LE FStar.Seq.Base.index Vale.AES.AES_common_s.nr FStar.Calc.calc_init FStar.Calc.calc_pack Prims.squash Vale.Arch.TypesNative.lemma_quad32_xor_commutes Vale.Arch.TypesNative.lemma_quad32_xor_associates Vale.Def.Types_s.quad32_xor_reveal Vale.AES.AES_helpers.commute_sub_bytes_shift_rows_forall Vale.AES.AES_s.eval_cipher_reveal Vale.AES.AES_s.eval_rounds_reveal Prims.l_and Prims.int FStar.Seq.Base.length Prims.op_Addition Prims.b2t Prims.op_GreaterThan Prims.op_Equality Vale.AES.AES_s.eval_rounds Prims.op_Subtraction FStar.Pervasives.pattern
module Vale.AES.AES_helpers

open Vale.Def.Opaque_s
open Vale.Def.Words_s
open Vale.Def.Types_s
open FStar.Seq
open Vale.AES.AES_s
open FStar.Mul

#reset-options "--initial_fuel 4 --max_fuel 4 --max_ifuel 0"
let lemma_expand_key_128_0 (key:aes_key_LE AES_128) =
  expand_key_reveal ()

#reset-options "--initial_fuel 1 --max_fuel 1 --max_ifuel 0 --z3rlimit 10"
let lemma_expand_key_128_i (key:aes_key_LE AES_128) (i:nat) =
  expand_key_reveal ();
  let n = 4 * i in
  // unfold expand_key 4 times (could use fuel, but that unfolds everything):
  let _ = expand_key AES_128 key (n + 1) in
  let _ = expand_key AES_128 key (n + 2) in
  let _ = expand_key AES_128 key (n + 3) in
  ()
#reset-options

// expand_key for large 'size' argument agrees with expand_key for smaller 'size' argument
let rec lemma_expand_append (key:aes_key_LE AES_128) (size1:nat) (size2:nat) =
  expand_key_reveal ();
  if size1 < size2 then lemma_expand_append key size1 (size2 - 1)

#reset-options "--initial_fuel 1 --max_fuel 1 --max_ifuel 0 --z3rlimit 40 --using_facts_from '* -FStar.Seq.Properties'"
#restart-solver
// quad32 key expansion is equivalent to nat32 key expansion
let rec lemma_expand_key_128 (key:seq nat32) (size:nat) =
  expand_key_128_reveal ();
  lemma_expand_append key (4 * size) 44;
  if size = 0 then ()
  else
  (
    let i = size - 1 in
    lemma_expand_append key (4 * i) 44;
    lemma_expand_key_128 key i;
    if i = 0 then lemma_expand_key_128_0 key
    else lemma_expand_key_128_i key i
  )
#reset-options

// SIMD version of round_key_128 is equivalent to scalar round_key_128
#push-options "--max_fuel 3 --initial_fuel 3 --max_ifuel 3 --initial_ifuel 3"  // REVIEW: Why do we need this?
let lemma_simd_round_key (prev:quad32) (rcon:nat32) =
  quad32_xor_reveal ();
  reverse_bytes_nat32_reveal ();
  commute_rot_word_sub_word prev.hi3;
  Vale.Arch.Types.xor_lemmas ()
#pop-options

let commute_sub_bytes_shift_rows_forall () =
  FStar.Classical.forall_intro commute_sub_bytes_shift_rows

let init_rounds_opaque (init:quad32) (round_keys:seq quad32) =
  eval_rounds_reveal ()

#push-options "--max_ifuel 2 --initial_ifuel 2"  // REVIEW: Why do we need this?  Extra inversion to deal with opaque?
let finish_cipher (alg:algorithm) (input:quad32) (round_keys:seq quad32) =
  eval_rounds_reveal ();
  eval_cipher_reveal ();
  commute_sub_bytes_shift_rows_forall()


let finish_cipher_opt (alg:algorithm) (input plain t0 t1 out:quad32) (round_keys:seq quad32) : Lemma
  (requires length round_keys == (nr alg) + 1 /\
            length round_keys > 0 /\ nr alg > 1 /\   // REVIEW: Why are these needed?
            t0 = quad32_xor input (index round_keys 0) /\
            t1 = eval_rounds t0 round_keys (nr alg - 1) /\
            out = quad32_xor (sub_bytes (shift_rows_LE t1)) (quad32_xor plain (index round_keys (nr alg))))
  (ensures out == quad32_xor plain (eval_cipher alg input round_keys))
val finish_cipher_opt (alg:algorithm) (input plain t0 t1 out:quad32) (round_keys:seq quad32) : Lemma
  (requires length round_keys == (nr alg) + 1 /\
            length round_keys > 0 /\ nr alg > 1 /\   // REVIEW: Why are these needed?
            t0 = quad32_xor input (index round_keys 0) /\
            t1 = eval_rounds t0 round_keys (nr alg - 1) /\
            out = quad32_xor (sub_bytes (shift_rows_LE t1)) (quad32_xor plain (index round_keys (nr alg))))
  (ensures out == quad32_xor plain (eval_cipher alg input round_keys))

    alg: Vale.AES.AES_common_s.algorithm ->
    input: Vale.Def.Types_s.quad32 ->
    plain: Vale.Def.Types_s.quad32 ->
    t0: Vale.Def.Types_s.quad32 ->
    t1: Vale.Def.Types_s.quad32 ->
    out: Vale.Def.Types_s.quad32 ->
    round_keys: FStar.Seq.Base.seq Vale.Def.Types_s.quad32
  -> FStar.Pervasives.Lemma
      (requires
        FStar.Seq.Base.length round_keys == Vale.AES.AES_common_s.nr alg + 1 /\
        FStar.Seq.Base.length round_keys > 0 /\ Vale.AES.AES_common_s.nr alg > 1 /\
        t0 = Vale.Def.Types_s.quad32_xor input (FStar.Seq.Base.index round_keys 0) /\
        t1 = Vale.AES.AES_s.eval_rounds t0 round_keys (Vale.AES.AES_common_s.nr alg - 1) /\
        out =
        Vale.Def.Types_s.quad32_xor (Vale.AES.AES_common_s.sub_bytes (Vale.AES.AES_s.shift_rows_LE t1
                ))
          (Vale.Def.Types_s.quad32_xor plain
              (FStar.Seq.Base.index round_keys (Vale.AES.AES_common_s.nr alg))))
      (ensures
        out == Vale.Def.Types_s.quad32_xor plain (Vale.AES.AES_s.eval_cipher alg input round_keys))