val lemma_expand_key_128 (key:seq nat32) (size:nat) : Lemma
  (requires size <= 11 /\ is_aes_key_LE AES_128 key)
  (ensures (
    let s = key_schedule_to_round_keys size (expand_key AES_128 key 44) in
    (forall (i:nat).{:pattern (expand_key_128 key i) \/ (expand_key_128_def key i)}
      i < size ==> expand_key_128 key i == s.[i])
  ))
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
  )
val lemma_expand_key_128 (key:seq nat32) (size:nat) : Lemma
  (requires size <= 11 /\ is_aes_key_LE AES_128 key)
  (ensures (
    let s = key_schedule_to_round_keys size (expand_key AES_128 key 44) in
    (forall (i:nat).{:pattern (expand_key_128 key i) \/ (expand_key_128_def key i)}
      i < size ==> expand_key_128 key i == s.[i])
  ))
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)
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
FStar.Seq.Base.seq Vale.Def.Types_s.nat32 Prims.nat Prims.op_Equality Prims.int Prims.bool Vale.AES.AES_helpers.lemma_expand_key_128_0 Vale.AES.AES_helpers.lemma_expand_key_128_i Prims.unit Vale.AES.AES_helpers.lemma_expand_key_128 Vale.AES.AES_helpers.lemma_expand_append FStar.Mul.op_Star Prims.op_Subtraction Vale.AES.AES_helpers.expand_key_128_reveal
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
val lemma_expand_key_128 (key:seq nat32) (size:nat) : Lemma
  (requires size <= 11 /\ is_aes_key_LE AES_128 key)
  (ensures (
    let s = key_schedule_to_round_keys size (expand_key AES_128 key 44) in
    (forall (i:nat).{:pattern (expand_key_128 key i) \/ (expand_key_128_def key i)}
      i < size ==> expand_key_128 key i == s.[i])
  ))
key: FStar.Seq.Base.seq Vale.Def.Types_s.nat32 -> size: Prims.nat
  -> FStar.Pervasives.Lemma
      (requires size <= 11 /\ Vale.AES.AES_s.is_aes_key_LE Vale.AES.AES_common_s.AES_128 key)
      (ensures
        (let s =
            Vale.AES.AES_s.key_schedule_to_round_keys size
              (Vale.AES.AES_s.expand_key Vale.AES.AES_common_s.AES_128 key 44)
          in
          forall (i: Prims.nat).
            {:pattern
            Vale.AES.AES_helpers.expand_key_128 key i\/Vale.AES.AES_helpers.expand_key_128_def key i}
            i < size ==> Vale.AES.AES_helpers.expand_key_128 key i == s.[ i ]))