let eval_round (state round_key:quad32) =
  let s = sub_bytes state in
  let s = shift_rows s in
  let s = mix_columns s in
  let s = quad32_xor s round_key in
  s
let eval_round (state round_key: quad32) =
let s = sub_bytes state in
let s = shift_rows s in
let s = mix_columns s in
let s = quad32_xor s round_key in
s
Vale.AES.AES_BE_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.TypesNative_s.fst.checked Vale.Def.Types_s.fst.checked Vale.Def.Prop_s.fst.checked Vale.Def.Opaque_s.fsti.checked Vale.Arch.Types.fsti.checked Vale.AES.AES_common_s.fst.checked prims.fst.checked FStar.UInt.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked
Vale.AES.AES_BE_s.fst
Vale.Def.Types_s.quad32 Vale.Def.Types_s.quad32_xor Vale.AES.AES_BE_s.mix_columns Vale.AES.AES_BE_s.shift_rows Vale.AES.AES_common_s.sub_bytes
module Vale.AES.AES_BE_s

// IMPORTANT: This specification is written assuming a big-endian mapping from bytes to quad32s
//            This is explicit in key_schedule_to_round_keys when we construct the round_key rk,
//            but it also applies implicitly to the input quad32

open Vale.Def.Prop_s
open Vale.Def.Opaque_s
open Vale.Def.Words_s
open Vale.Def.Words.Four_s
open Vale.Def.Words.Seq_s
open Vale.Def.Types_s
open Vale.Arch.Types
open FStar.Seq
open FStar.Mul
include Vale.AES.AES_common_s

// operations assume that the quad32 and nat32 values are big-endian interpretations
// of 16-byte and 4-byte sequences
assume val mix_columns (q:quad32) : quad32
assume val inv_mix_columns (q:quad32) : quad32
assume val shift_rows (q:quad32) : quad32
assume val inv_shift_rows (q:quad32) : quad32
assume val rot_word (w:nat32) : nat32

assume val commute_rot_word_sub_word (x:nat32) (rcon:nat32) : Lemma
  (rot_word (sub_word x *^ ishl32 rcon 16) == sub_word (rot_word x) *^ rcon)

let is_aes_key_word (alg:algorithm) (s:seq nat32) : prop0 = length s == nk alg
type aes_key_word (alg:algorithm) : eqtype = s:(seq nat32){is_aes_key_word alg s}
val eval_round : state: Vale.Def.Types_s.quad32 -> round_key: Vale.Def.Types_s.quad32 -> Vale.Def.Types_s.quad32
state: Vale.Def.Types_s.quad32 -> round_key: Vale.Def.Types_s.quad32 -> Vale.Def.Types_s.quad32