let key128_lemma = as_t #(VSig.vale_sig_stdcall key128_pre key128_post) key128_lemma'
let key128_lemma =
as_t #(VSig.vale_sig_stdcall key128_pre key128_post) key128_lemma'
Vale.Stdcalls.X64.Aes.fsti.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.MemoryHelpers.fsti.checked Vale.AsLowStar.LowStarSig.fst.checked Vale.AES.X64.AES.fsti.checked Vale.AES.AES_s.fst.checked prims.fst.checked LowStar.BufferView.Up.fsti.checked LowStar.BufferView.Down.fsti.checked LowStar.Buffer.fst.checked FStar.UInt64.fsti.checked FStar.Pervasives.Native.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.fsti
Vale.Stdcalls.X64.Aes.as_t Vale.AsLowStar.ValeSig.vale_sig_stdcall Vale.Stdcalls.X64.Aes.dom Vale.Stdcalls.X64.Aes.key128_pre Vale.Stdcalls.X64.Aes.key128_post Vale.Stdcalls.X64.Aes.key128_lemma'
module Vale.Stdcalls.X64.Aes

open FStar.HyperStack.ST
module B = LowStar.Buffer
module HS = FStar.HyperStack
open FStar.Mul

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
open Vale.AES.AES_s

module AE = Vale.AES.X64.AES

let uint64 = UInt64.t

(* A little utility to trigger normalization in types *)
noextract
let as_t (#a:Type) (x:normal a) : a = x
noextract
let as_normal_t (#a:Type) (x:a) : normal a = x

[@__reduce__] noextract
let b128 = buf_t TUInt8 TUInt128
[@__reduce__] noextract
let t128_mod = TD_Buffer TUInt8 TUInt128 default_bq
[@__reduce__] noextract
let t128_no_mod = TD_Buffer TUInt8 TUInt128 ({modified=false; strict_disjointness=false; taint=MS.Secret})

[@__reduce__] noextract
let dom: IX64.arity_ok_stdcall td =
  let y = [t128_no_mod; t128_mod] in
  assert_norm (List.length y = 2);
  y

(* Need to rearrange the order of arguments *)
[@__reduce__] noextract
let key128_pre : VSig.vale_pre dom =
  fun (c:V.va_code)
    (input_b:b128)
    (output_b:b128)
    (va_s0:V.va_state) ->
      AE.va_req_KeyExpansionStdcall c va_s0 IA.win AES_128
        (as_vale_buffer input_b) (as_vale_buffer output_b)

[@__reduce__] noextract
let key128_post : VSig.vale_post dom =
  fun (c:V.va_code)
    (input_b:b128)
    (output_b:b128)
    (va_s0:V.va_state)
    (va_s1:V.va_state)
    (f:V.va_fuel) ->
      AE.va_ens_KeyExpansionStdcall c va_s0 IA.win AES_128 (as_vale_buffer input_b) (as_vale_buffer output_b) va_s1 f

#set-options "--z3rlimit 20"

[@__reduce__] noextract
let key128_lemma'
    (code:V.va_code)
    (_win:bool)
    (input_b:b128)
    (output_b:b128)
    (va_s0:V.va_state)
 : Ghost (V.va_state & V.va_fuel)
     (requires
       key128_pre code input_b output_b va_s0)
     (ensures (fun (va_s1, f) ->
       V.eval_code code va_s0 f va_s1 /\
       VSig.vale_calling_conventions_stdcall va_s0 va_s1 /\
       key128_post code input_b output_b va_s0 va_s1 f /\
       ME.buffer_writeable (as_vale_buffer input_b) /\
       ME.buffer_writeable (as_vale_buffer output_b)
 )) =
   let va_s1, f = AE.va_lemma_KeyExpansionStdcall code va_s0 IA.win AES_128
     (as_vale_buffer input_b) (as_vale_buffer output_b) in
   Vale.AsLowStar.MemoryHelpers.buffer_writeable_reveal ME.TUInt8 ME.TUInt128 input_b;
   Vale.AsLowStar.MemoryHelpers.buffer_writeable_reveal ME.TUInt8 ME.TUInt128 output_b;
   (va_s1, f)
val key128_lemma : Vale.AsLowStar.ValeSig.vale_sig_stdcall Vale.Stdcalls.X64.Aes.key128_pre
  Vale.Stdcalls.X64.Aes.key128_post
Vale.AsLowStar.ValeSig.vale_sig_stdcall Vale.Stdcalls.X64.Aes.key128_pre
  Vale.Stdcalls.X64.Aes.key128_post