val lemma_expand_key_128_i (key:aes_key_LE AES_128) (i:nat) : Lemma
  (requires
    0 < i /\ i < 11
  )
  (ensures (
    let m = 4 * (i - 1) in
    let n = 4 * i in
    let v = expand_key AES_128 key n in
    let w = expand_key AES_128 key (n + 4) in
    let prev =              Mkfour v.[m + 0] v.[m + 1] v.[m + 2] v.[m + 3] in
    round_key_128 prev i == Mkfour w.[n + 0] w.[n + 1] w.[n + 2] w.[n + 3]
  ))
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
  ()
val lemma_expand_key_128_i (key:aes_key_LE AES_128) (i:nat) : Lemma
  (requires
    0 < i /\ i < 11
  )
  (ensures (
    let m = 4 * (i - 1) in
    let n = 4 * i in
    let v = expand_key AES_128 key n in
    let w = expand_key AES_128 key (n + 4) in
    let prev =              Mkfour v.[m + 0] v.[m + 1] v.[m + 2] v.[m + 3] in
    round_key_128 prev i == Mkfour w.[n + 0] w.[n + 1] w.[n + 2] w.[n + 3]
  ))
let lemma_expand_key_128_i (key: aes_key_LE AES_128) (i: nat) =
expand_key_reveal ();
let n = 4 * i in
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
()
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 FStar.Seq.Base.seq Vale.Def.Words_s.nat32 Prims.eq2 FStar.Seq.Base.length Prims.op_Addition Vale.AES.AES_s.expand_key Prims.int FStar.Mul.op_Star 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"
val lemma_expand_key_128_i (key:aes_key_LE AES_128) (i:nat) : Lemma
  (requires
    0 < i /\ i < 11
  )
  (ensures (
    let m = 4 * (i - 1) in
    let n = 4 * i in
    let v = expand_key AES_128 key n in
    let w = expand_key AES_128 key (n + 4) in
    let prev =              Mkfour v.[m + 0] v.[m + 1] v.[m + 2] v.[m + 3] in
    round_key_128 prev i == Mkfour w.[n + 0] w.[n + 1] w.[n + 2] w.[n + 3]
  ))
key: Vale.AES.AES_s.aes_key_LE Vale.AES.AES_common_s.AES_128 -> i: Prims.nat
  -> FStar.Pervasives.Lemma (requires 0 < i /\ i < 11)
      (ensures
        (let m = 4 * (i - 1) in
          let n = 4 * i in
          let v = Vale.AES.AES_s.expand_key Vale.AES.AES_common_s.AES_128 key n in
          let w = Vale.AES.AES_s.expand_key Vale.AES.AES_common_s.AES_128 key (n + 4) in
          let prev = Vale.Def.Words_s.Mkfour v.[ m + 0 ] v.[ m + 1 ] v.[ m + 2 ] v.[ m + 3 ] in
          Vale.AES.AES_helpers.round_key_128 prev i ==
          Vale.Def.Words_s.Mkfour w.[ n + 0 ] w.[ n + 1 ] w.[ n + 2 ] w.[ n + 3 ]))