let eval_cipher_reveal = opaque_revealer (`%eval_cipher) eval_cipher eval_cipher_def
let eval_cipher_reveal =
opaque_revealer (`%eval_cipher) eval_cipher eval_cipher_def
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.Opaque_s.opaque_revealer Vale.AES.AES_common_s.algorithm Vale.Def.Types_s.quad32 FStar.Seq.Base.seq Prims.eq2 Prims.int FStar.Seq.Base.length Prims.op_Addition Vale.AES.AES_common_s.nr Prims.l_True Vale.AES.AES_BE_s.eval_cipher Vale.AES.AES_BE_s.eval_cipher_def
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}

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 rec eval_rounds_def (init:quad32) (round_keys:seq quad32) (n:nat{n < length round_keys}) : quad32 =
  if n = 0 then
    init
  else
    eval_round (eval_rounds_def init round_keys (n - 1)) (index round_keys n)
[@"opaque_to_smt"] let eval_rounds = opaque_make eval_rounds_def
irreducible let eval_rounds_reveal = opaque_revealer (`%eval_rounds) eval_rounds eval_rounds_def

let eval_cipher_def (alg:algorithm) (input:quad32) (round_keys:seq quad32) : Pure quad32
  (requires length round_keys == nr alg + 1)
  (ensures fun _ -> True)
  =
  let state = quad32_xor input (index round_keys 0) in
  let state = eval_rounds_def state round_keys (nr alg - 1) in
  let state = sub_bytes state in
  let state = shift_rows state in
  let state = quad32_xor state (index round_keys (nr alg)) in
  state
val eval_cipher_reveal : _: Prims.unit
  -> FStar.Pervasives.Lemma
    (ensures Vale.AES.AES_BE_s.eval_cipher == Vale.AES.AES_BE_s.eval_cipher_def)
_: Prims.unit
  -> FStar.Pervasives.Lemma
    (ensures Vale.AES.AES_BE_s.eval_cipher == Vale.AES.AES_BE_s.eval_cipher_def)