val aes_rcon (i: int) : nat32
let aes_rcon (i:int) : nat32 =
  if i = 0 then 0x01 else
  if i = 1 then 0x02 else
  if i = 2 then 0x04 else
  if i = 3 then 0x08 else
  if i = 4 then 0x10 else
  if i = 5 then 0x20 else
  if i = 6 then 0x40 else
  if i = 7 then 0x80 else
  if i = 8 then 0x1b else
  0x36
val aes_rcon (i: int) : nat32
let aes_rcon (i: int) : nat32 =
if i = 0
then 0x01
else
  if i = 1
  then 0x02
  else
    if i = 2
    then 0x04
    else
      if i = 3
      then 0x08
      else
        if i = 4
        then 0x10
        else
          if i = 5
          then 0x20
          else if i = 6 then 0x40 else if i = 7 then 0x80 else if i = 8 then 0x1b else 0x36
Vale.AES.AES_common_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.Types_s.fst.checked Vale.Def.Prop_s.fst.checked Vale.Def.Opaque_s.fsti.checked prims.fst.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked
Vale.AES.AES_common_s.fst
Prims.int Prims.op_Equality Prims.bool Vale.Def.Types_s.nat32
module Vale.AES.AES_common_s

// IMPORTANT: This specification is written assuming a little-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 FStar.Seq
open FStar.Mul

// substitution is endian-neutral;
assume val sub_bytes (q:quad32) : quad32
assume val inv_sub_bytes (q:quad32) : quad32
assume val sub_word (w:nat32) : nat32

type algorithm:eqtype = | AES_128 | AES_192 | AES_256
val aes_rcon (i: int) : nat32
i: Prims.int -> Vale.Def.Types_s.nat32