val expand_key_128_reveal : _: Prims.unit
  -> FStar.Pervasives.Lemma
    (ensures Vale.AES.AES_helpers_BE.expand_key_128 == Vale.AES.AES_helpers_BE.expand_key_128_def)
let expand_key_128_reveal = opaque_revealer (`%expand_key_128) expand_key_128 expand_key_128_def
module Vale.AES.AES_helpers_BE

open Vale.Def.Opaque_s
open Vale.Def.Words_s
open Vale.Def.Types_s
open FStar.Seq
open Vale.AES.AES_BE_s
open FStar.Mul
open Vale.Arch.Types
open Vale.Def.Words.Seq_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

unfold let be_quad32_to_seq (q:quad32) : seq nat32 = four_to_seq_BE q

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


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

let round_key_128_rcon (prev:quad32) (rcon:nat32) : quad32 =
  let Mkfour v0 v1 v2 v3 = prev in
  let w3 = v3 *^ (sub_word (rot_word v0) *^ rcon) in
  let w2 = v2 *^ w3 in
  let w1 = v1 *^ w2 in
  let w0 = v0 *^ w1 in
  Mkfour w0 w1 w2 w3

let round_key_128 (prev:quad32) (round:nat) : quad32 =
  round_key_128_rcon prev (aes_rcon (round - 1))

let rec expand_key_128_def (key:seq nat32) (round:nat) : Pure quad32
  (requires is_aes_key_word AES_128 key)
  (ensures fun _ -> True)
  =
  if round = 0 then Mkfour key.[3] key.[2] key.[1] key.[0]
  else round_key_128 (expand_key_128_def key (round - 1)) round
/
Vale.Def.Words_s.fsti.checked Vale.Def.Words.Seq_s.fsti.checked Vale.Def.Types_s.fst.checked Vale.Def.Opaque_s.fsti.checked Vale.Arch.Types.fsti.checked Vale.AES.AES_BE_s.fst.checked prims.fst.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked
Vale.AES.AES_helpers_BE.fsti
_: Prims.unit
  -> FStar.Pervasives.Lemma
    (ensures Vale.AES.AES_helpers_BE.expand_key_128 == Vale.AES.AES_helpers_BE.expand_key_128_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_BE_s.is_aes_key_word Vale.AES.AES_common_s.AES_128 Prims.l_True Vale.AES.AES_helpers_BE.expand_key_128 Vale.AES.AES_helpers_BE.expand_key_128_def
let expand_key_128_reveal =
  
opaque_revealer (`%expand_key_128) expand_key_128 expand_key_128_def