val make_AES256_key (k0 k1: quad32)
    : Pure (seq nat32) (requires True) (ensures fun key -> is_aes_key_LE AES_256 key)
val make_AES256_key (k0 k1: quad32)
    : Pure (seq nat32) (requires True) (ensures fun key -> is_aes_key_LE AES_256 key)
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)
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
/
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
k0: Vale.Def.Types_s.quad32 -> k1: Vale.Def.Types_s.quad32
  -> Prims.Pure (FStar.Seq.Base.seq Vale.Def.Types_s.nat32)
Vale.Def.Types_s.quad32 FStar.Seq.Base.append Vale.Def.Words_s.nat32 Vale.Arch.Types.quad32_to_seq FStar.Seq.Base.seq Vale.Def.Types_s.nat32 Prims.l_True Vale.AES.AES_s.is_aes_key_LE Vale.AES.AES_common_s.AES_256
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)