val lemma_expand_key_256_0 (key: aes_key_LE AES_256) : Lemma (equal key (expand_key AES_256 key 8))
let lemma_expand_key_256_0 (key:aes_key_LE AES_256) : Lemma
  (equal key (expand_key AES_256 key 8))
  =
  expand_key_reveal ()
val lemma_expand_key_256_0 (key: aes_key_LE AES_256) : Lemma (equal key (expand_key AES_256 key 8))
let lemma_expand_key_256_0 (key: aes_key_LE AES_256) : Lemma (equal key (expand_key AES_256 key 8)) =
expand_key_reveal ()
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 Vale.AES.AES_s.expand_key_reveal Prims.unit Prims.l_True Prims.squash FStar.Seq.Base.equal Vale.Def.Types_s.nat32 Vale.AES.AES_s.expand_key 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))
val lemma_expand_key_256_0 (key: aes_key_LE AES_256) : Lemma (equal key (expand_key AES_256 key 8))
key: Vale.AES.AES_s.aes_key_LE Vale.AES.AES_common_s.AES_256
  -> FStar.Pervasives.Lemma
    (ensures
      FStar.Seq.Base.equal key (Vale.AES.AES_s.expand_key Vale.AES.AES_common_s.AES_256 key 8))