val expand_key_256_reveal : _: Prims.unit
  -> FStar.Pervasives.Lemma
    (ensures Vale.AES.AES256_helpers.expand_key_256 == Vale.AES.AES256_helpers.expand_key_256_def)
let expand_key_256_reveal = opaque_revealer (`%expand_key_256) expand_key_256 expand_key_256_def
module Vale.AES.AES256_helpers

open FStar.Mul
open Vale.Def.Opaque_s
open Vale.Def.Words_s
open Vale.Arch.Types
open Vale.Def.Types_s
open FStar.Seq
open Vale.AES.AES_s

// syntax for seq accesses, s.[index] and s.[index] <- value
unfold let (.[]) (#a:Type) (s:seq a) (i:nat{ i < length s}) : Tot a = index s i
unfold let (.[]<-) = Seq.upd

unfold let ( *^ ) = nat32_xor
unfold let ( *^^ ) = quad32_xor

let quad32_shl32 (q:quad32) : quad32 =
  let Mkfour v0 v1 v2 v3 = q in
  Mkfour 0 v0 v1 v2

let make_AES256_key (k0 k1:quad32) : Pure (seq nat32)
  (requires True)
  (ensures fun key -> is_aes_key_LE AES_256 key)
  =
  append (quad32_to_seq k0) (quad32_to_seq k1)

// Redefine key expansion in terms of quad32 values rather than nat32 values,
// then prove both definitions are equivalent.

let round_key_256_rcon (prev0 prev1:quad32) (rcon:nat32) (round:int) : quad32 =
  let Mkfour v0 v1 v2 v3 = prev0 in
  let Mkfour _  _  _  v7 = prev1 in
  let c1 = if round % 2 = 0 then sub_word (rot_word_LE v7) *^ rcon else sub_word v7 in
  let w0 = v0 *^ c1 in
  let w1 = v1 *^ w0 in
  let w2 = v2 *^ w1 in
  let w3 = v3 *^ w2 in
  Mkfour w0 w1 w2 w3

let round_key_256 (prev0 prev1:quad32) (round:nat) : quad32 =
  round_key_256_rcon prev0 prev1 (aes_rcon (round / 2 - 1)) round

let rec expand_key_256_def (key:seq nat32) (round:nat) : Pure quad32
  (requires is_aes_key_LE AES_256 key)
  (ensures fun _ -> True)
  =
  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_def key (round - 2)) (expand_key_256_def key (round - 1)) round
/
Vale.Def.Words_s.fsti.checked Vale.Def.Types_s.fst.checked Vale.Def.Opaque_s.fsti.checked Vale.Arch.Types.fsti.checked Vale.AES.AES_s.fst.checked prims.fst.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked
Vale.AES.AES256_helpers.fsti
_: Prims.unit
  -> FStar.Pervasives.Lemma
    (ensures Vale.AES.AES256_helpers.expand_key_256 == Vale.AES.AES256_helpers.expand_key_256_def)
Vale.Def.Opaque_s.opaque_revealer FStar.Seq.Base.seq Vale.Def.Types_s.nat32 Prims.nat Vale.Def.Types_s.quad32 Vale.AES.AES_s.is_aes_key_LE Vale.AES.AES_common_s.AES_256 Prims.l_True Vale.AES.AES256_helpers.expand_key_256 Vale.AES.AES256_helpers.expand_key_256_def
let expand_key_256_reveal =
  
opaque_revealer (`%expand_key_256) expand_key_256 expand_key_256_def