val lowstar_key256:lowstar_key256_t
let lowstar_key256 : lowstar_key256_t =
  assert_norm (List.length dom + List.length ([]<:list arg) <= 4);
  IX64.wrap_weak_stdcall
    code_key256
    dom
    (W.mk_prediction code_key256 dom [] (key256_lemma code_key256 IA.win))
val lowstar_key256:lowstar_key256_t
let lowstar_key256:lowstar_key256_t =
assert_norm (List.length dom + List.length ([] <: list arg) <= 4);
IX64.wrap_weak_stdcall code_key256
  dom
  (W.mk_prediction code_key256 dom [] (key256_lemma code_key256 IA.win))
Vale.Stdcalls.X64.Aes.fst.checked
Vale.X64.State.fsti.checked Vale.X64.MemoryAdapters.fsti.checked Vale.X64.Memory.fsti.checked Vale.X64.Machine_s.fst.checked Vale.X64.Decls.fsti.checked Vale.Interop.X64.fsti.checked Vale.Interop.Base.fst.checked Vale.Interop.Assumptions.fst.checked Vale.Def.Types_s.fst.checked Vale.AsLowStar.Wrapper.fsti.checked Vale.AsLowStar.ValeSig.fst.checked Vale.AsLowStar.LowStarSig.fst.checked prims.fst.checked LowStar.BufferView.Up.fsti.checked LowStar.BufferView.Down.fsti.checked LowStar.Buffer.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.List.fst.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.fst.checked
Vale.Stdcalls.X64.Aes.fst
Vale.Interop.X64.wrap_weak_stdcall Vale.Stdcalls.X64.Aes.code_key256 Vale.Stdcalls.X64.Aes.dom Vale.AsLowStar.Wrapper.pre_rel_generic Vale.Interop.X64.max_stdcall Vale.Interop.X64.arg_reg_stdcall Prims.Nil Vale.Interop.Base.arg Vale.Stdcalls.X64.Aes.key256_pre Vale.AsLowStar.Wrapper.post_rel_generic Vale.Stdcalls.X64.Aes.key256_post Vale.AsLowStar.Wrapper.mk_prediction Vale.Interop.X64.regs_modified_stdcall Vale.Interop.X64.xmms_modified_stdcall Vale.Stdcalls.X64.Aes.key256_lemma Vale.Interop.Assumptions.win Prims.unit FStar.Pervasives.assert_norm Prims.b2t Prims.op_LessThanOrEqual Prims.op_Addition FStar.List.Tot.Base.length Vale.Interop.Base.td Prims.list
module Vale.Stdcalls.X64.Aes

open FStar.Mul
open FStar.HyperStack.ST
module HS = FStar.HyperStack
module B = LowStar.Buffer
module DV = LowStar.BufferView.Down
module UV = LowStar.BufferView.Up
open Vale.Def.Types_s

open Vale.Interop.Base
module IX64 = Vale.Interop.X64
module VSig = Vale.AsLowStar.ValeSig
module LSig = Vale.AsLowStar.LowStarSig
module ME = Vale.X64.Memory
module V = Vale.X64.Decls
module IA = Vale.Interop.Assumptions
module W = Vale.AsLowStar.Wrapper
open Vale.X64.MemoryAdapters
module VS = Vale.X64.State
module MS = Vale.X64.Machine_s

let lowstar_key128 : lowstar_key128_t  =
  assert_norm (List.length dom + List.length ([]<:list arg) <= 4);
  IX64.wrap_weak_stdcall
    code_key128
    dom
    (W.mk_prediction code_key128 dom [] (key128_lemma code_key128 IA.win))

let aes128_key_expansion //: normal lowstar_key128_t
  = as_normal_t #lowstar_key128_t lowstar_key128
val lowstar_key256:lowstar_key256_t
Vale.Stdcalls.X64.Aes.lowstar_key256_t