val lemma_expand_append (key:aes_key_LE AES_128) (size1:nat) (size2:nat) : Lemma
  (requires size1 <= size2 /\ size2 <= 44)
  (ensures equal (expand_key AES_128 key size1) (slice (expand_key AES_128 key size2) 0 size1))
  (decreases size2)
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)
val lemma_expand_append (key:aes_key_LE AES_128) (size1:nat) (size2:nat) : Lemma
  (requires size1 <= size2 /\ size2 <= 44)
  (ensures equal (expand_key AES_128 key size1) (slice (expand_key AES_128 key size2) 0 size1))
  (decreases size2)
let rec lemma_expand_append (key: aes_key_LE AES_128) (size1 size2: nat) =
expand_key_reveal ();
if size1 < size2 then lemma_expand_append key size1 (size2 - 1)
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_s.aes_key_LE Vale.AES.AES_common_s.AES_128 Prims.nat Prims.op_LessThan Vale.AES.AES_helpers.lemma_expand_append Prims.op_Subtraction Prims.bool Prims.unit Vale.AES.AES_s.expand_key_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
val lemma_expand_append (key:aes_key_LE AES_128) (size1:nat) (size2:nat) : Lemma
  (requires size1 <= size2 /\ size2 <= 44)
  (ensures equal (expand_key AES_128 key size1) (slice (expand_key AES_128 key size2) 0 size1))
  (decreases size2)
key: Vale.AES.AES_s.aes_key_LE Vale.AES.AES_common_s.AES_128 -> size1: Prims.nat -> size2: Prims.nat
  -> FStar.Pervasives.Lemma (requires size1 <= size2 /\ size2 <= 44)
      (ensures
        FStar.Seq.Base.equal (Vale.AES.AES_s.expand_key Vale.AES.AES_common_s.AES_128 key size1)
          (FStar.Seq.Base.slice (Vale.AES.AES_s.expand_key Vale.AES.AES_common_s.AES_128 key size2)
              0
              size1))
      (decreases size2)