val lemma_expand_key_256_i (key: aes_key_LE AES_256) (i: nat)
    : Lemma (requires 1 < i /\ i < 15)
      (ensures
        (let m = 4 * (i - 2) in
          let n = 4 * i in
          let v = expand_key AES_256 key n in
          let w = expand_key AES_256 key (n + 4) in
          let prev0 = Mkfour v.[ m + 0 ] v.[ m + 1 ] v.[ m + 2 ] v.[ m + 3 ] in
          let prev1 = Mkfour v.[ m + 4 ] v.[ m + 5 ] v.[ m + 6 ] v.[ m + 7 ] in
          round_key_256 prev0 prev1 i == Mkfour w.[ n + 0 ] w.[ n + 1 ] w.[ n + 2 ] w.[ n + 3 ]))
let lemma_expand_key_256_i (key:aes_key_LE AES_256) (i:nat) : Lemma
  (requires
    1 < i /\ i < 15
  )
  (ensures (
    let m = 4 * (i - 2) in
    let n = 4 * i in
    let v = expand_key AES_256 key n in          // Current
    let w = expand_key AES_256 key (n + 4) in    // Next 4 words
    let prev0 =                    Mkfour v.[m + 0] v.[m + 1] v.[m + 2] v.[m + 3] in  // Penultimate 4 words in Current
    let prev1 =                    Mkfour v.[m + 4] v.[m + 5] v.[m + 6] v.[m + 7] in  // Ultimate 4 words in Current
    round_key_256 prev0 prev1 i == Mkfour w.[n + 0] w.[n + 1] w.[n + 2] w.[n + 3]  // NextQuad == Next 4 words
  ))
  =
  expand_key_reveal ();
  let n = 4 * i in
  // unfold expand_key 8 times (could use fuel, but that unfolds everything):
  let _ = expand_key AES_256 key (n + 1) in
  let _ = expand_key AES_256 key (n + 2) in
  let _ = expand_key AES_256 key (n + 3) in
  let _ = expand_key AES_256 key (n + 4) in
  if i < 14 then (
    let _ = expand_key AES_256 key (n + 5) in
    let _ = expand_key AES_256 key (n + 6) in
    let _ = expand_key AES_256 key (n + 7) in
    ()
  ) else ();
  ()
val lemma_expand_key_256_i (key: aes_key_LE AES_256) (i: nat)
    : Lemma (requires 1 < i /\ i < 15)
      (ensures
        (let m = 4 * (i - 2) in
          let n = 4 * i in
          let v = expand_key AES_256 key n in
          let w = expand_key AES_256 key (n + 4) in
          let prev0 = Mkfour v.[ m + 0 ] v.[ m + 1 ] v.[ m + 2 ] v.[ m + 3 ] in
          let prev1 = Mkfour v.[ m + 4 ] v.[ m + 5 ] v.[ m + 6 ] v.[ m + 7 ] in
          round_key_256 prev0 prev1 i == Mkfour w.[ n + 0 ] w.[ n + 1 ] w.[ n + 2 ] w.[ n + 3 ]))
let lemma_expand_key_256_i (key: aes_key_LE AES_256) (i: nat)
    : Lemma (requires 1 < i /\ i < 15)
      (ensures
        (let m = 4 * (i - 2) in
          let n = 4 * i in
          let v = expand_key AES_256 key n in
          let w = expand_key AES_256 key (n + 4) in
          let prev0 = Mkfour v.[ m + 0 ] v.[ m + 1 ] v.[ m + 2 ] v.[ m + 3 ] in
          let prev1 = Mkfour v.[ m + 4 ] v.[ m + 5 ] v.[ m + 6 ] v.[ m + 7 ] in
          round_key_256 prev0 prev1 i == Mkfour w.[ n + 0 ] w.[ n + 1 ] w.[ n + 2 ] w.[ n + 3 ])) =
expand_key_reveal ();
let n = 4 * i in
let _ = expand_key AES_256 key (n + 1) in
let _ = expand_key AES_256 key (n + 2) in
let _ = expand_key AES_256 key (n + 3) in
let _ = expand_key AES_256 key (n + 4) in
if i < 14
then
  (let _ = expand_key AES_256 key (n + 5) in
    let _ = expand_key AES_256 key (n + 6) in
    let _ = expand_key AES_256 key (n + 7) in
    ());
()
Vale.AES.AES256_helpers.fst.checked
Vale.Arch.Types.fsti.checked prims.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked
Vale.AES.AES256_helpers.fst
Vale.AES.AES_s.aes_key_LE Vale.AES.AES_common_s.AES_256 Prims.nat Prims.unit Prims.op_LessThan 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.bool Prims.int FStar.Mul.op_Star Vale.AES.AES_s.expand_key_reveal Prims.l_and Prims.b2t Prims.squash Vale.Def.Words_s.four Vale.Def.Types_s.nat32 Vale.AES.AES256_helpers.round_key_256 Vale.Def.Words_s.Mkfour Vale.AES.AES256_helpers.op_String_Access Prims.op_Subtraction Prims.Nil FStar.Pervasives.pattern
module Vale.AES.AES256_helpers

let lemma_reveal_expand_key_256 (key:aes_key_LE AES_256) (round:nat) : Lemma
  (expand_key_256 key round == (
    if round = 0 then Mkfour key.[0] key.[1] key.[2] key.[3]
    else if round = 1 then Mkfour key.[4] key.[5] key.[6] key.[7]
    else round_key_256 (expand_key_256 key (round - 2)) (expand_key_256 key (round - 1)) round
  ))
  =
  expand_key_256_reveal ()

#reset-options "--initial_fuel 8 --max_fuel 8 --max_ifuel 0"
let lemma_expand_key_256_0 (key:aes_key_LE AES_256) : Lemma
  (equal key (expand_key AES_256 key 8))
  =
  expand_key_reveal ()

open FStar.Mul
#reset-options "--initial_fuel 1 --max_fuel 1 --max_ifuel 0 --z3rlimit 40 --using_facts_from '* -FStar.Seq.Properties'"
let lemma_expand_key_256_i (key:aes_key_LE AES_256) (i:nat) : Lemma
  (requires
    1 < i /\ i < 15
  )
  (ensures (
    let m = 4 * (i - 2) in
    let n = 4 * i in
    let v = expand_key AES_256 key n in          // Current
    let w = expand_key AES_256 key (n + 4) in    // Next 4 words
    let prev0 =                    Mkfour v.[m + 0] v.[m + 1] v.[m + 2] v.[m + 3] in  // Penultimate 4 words in Current
    let prev1 =                    Mkfour v.[m + 4] v.[m + 5] v.[m + 6] v.[m + 7] in  // Ultimate 4 words in Current
    round_key_256 prev0 prev1 i == Mkfour w.[n + 0] w.[n + 1] w.[n + 2] w.[n + 3]  // NextQuad == Next 4 words
  ))
val lemma_expand_key_256_i (key: aes_key_LE AES_256) (i: nat)
    : Lemma (requires 1 < i /\ i < 15)
      (ensures
        (let m = 4 * (i - 2) in
          let n = 4 * i in
          let v = expand_key AES_256 key n in
          let w = expand_key AES_256 key (n + 4) in
          let prev0 = Mkfour v.[ m + 0 ] v.[ m + 1 ] v.[ m + 2 ] v.[ m + 3 ] in
          let prev1 = Mkfour v.[ m + 4 ] v.[ m + 5 ] v.[ m + 6 ] v.[ m + 7 ] in
          round_key_256 prev0 prev1 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_256 -> i: Prims.nat
  -> FStar.Pervasives.Lemma (requires 1 < i /\ i < 15)
      (ensures
        (let m = 4 * (i - 2) in
          let n = 4 * i in
          let v = Vale.AES.AES_s.expand_key Vale.AES.AES_common_s.AES_256 key n in
          let w = Vale.AES.AES_s.expand_key Vale.AES.AES_common_s.AES_256 key (n + 4) in
          let prev0 = Vale.Def.Words_s.Mkfour v.[ m + 0 ] v.[ m + 1 ] v.[ m + 2 ] v.[ m + 3 ] in
          let prev1 = Vale.Def.Words_s.Mkfour v.[ m + 4 ] v.[ m + 5 ] v.[ m + 6 ] v.[ m + 7 ] in
          Vale.AES.AES256_helpers.round_key_256 prev0 prev1 i ==
          Vale.Def.Words_s.Mkfour w.[ n + 0 ] w.[ n + 1 ] w.[ n + 2 ] w.[ n + 3 ]))