val compute_iv_lemma'
      (iv: Ghost.erased supported_iv_LE)
      (code: V.va_code)
      (_win: bool)
      (iv_b: b128)
      (num_bytes len: uint64)
      (j0_b iv_extra_b hkeys_b: b128)
      (va_s0: V.va_state)
    : Ghost (V.va_state & V.va_fuel)
      (requires compute_iv_pre iv code iv_b num_bytes len j0_b iv_extra_b hkeys_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 /\
            compute_iv_post iv code iv_b num_bytes len j0_b iv_extra_b hkeys_b va_s0 va_s1 f /\
            ME.buffer_writeable (as_vale_buffer iv_b) /\
            ME.buffer_writeable (as_vale_buffer hkeys_b) /\
            ME.buffer_writeable (as_vale_buffer iv_extra_b) /\
            ME.buffer_writeable (as_vale_buffer j0_b)))
let compute_iv_lemma'
    (iv:Ghost.erased supported_iv_LE)
    (code:V.va_code)
    (_win:bool)
    (iv_b:b128)
    (num_bytes:uint64)
    (len:uint64)
    (j0_b:b128)
    (iv_extra_b:b128)
    (hkeys_b:b128)
    (va_s0:V.va_state)
  : Ghost (V.va_state & V.va_fuel)
    (requires compute_iv_pre iv code iv_b num_bytes len j0_b iv_extra_b hkeys_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 /\
      compute_iv_post iv code iv_b num_bytes len j0_b iv_extra_b hkeys_b va_s0 va_s1 f /\      
      ME.buffer_writeable (as_vale_buffer iv_b) /\
      ME.buffer_writeable (as_vale_buffer hkeys_b) /\
      ME.buffer_writeable (as_vale_buffer iv_extra_b) /\
      ME.buffer_writeable (as_vale_buffer j0_b))
   ) = let va_s1, f = GC.va_lemma_Compute_iv_stdcall code va_s0 IA.win (Ghost.reveal iv)
        (as_vale_buffer iv_b) (UInt64.v num_bytes)
        (UInt64.v len) (as_vale_buffer j0_b)
        (as_vale_buffer iv_extra_b) (as_vale_buffer hkeys_b) in
     Vale.AsLowStar.MemoryHelpers.buffer_writeable_reveal ME.TUInt8 ME.TUInt128 iv_b;
     Vale.AsLowStar.MemoryHelpers.buffer_writeable_reveal ME.TUInt8 ME.TUInt128 iv_extra_b;
     Vale.AsLowStar.MemoryHelpers.buffer_writeable_reveal ME.TUInt8 ME.TUInt128 j0_b; 
     Vale.AsLowStar.MemoryHelpers.buffer_writeable_reveal ME.TUInt8 ME.TUInt128 hkeys_b;
     va_s1, f
val compute_iv_lemma'
      (iv: Ghost.erased supported_iv_LE)
      (code: V.va_code)
      (_win: bool)
      (iv_b: b128)
      (num_bytes len: uint64)
      (j0_b iv_extra_b hkeys_b: b128)
      (va_s0: V.va_state)
    : Ghost (V.va_state & V.va_fuel)
      (requires compute_iv_pre iv code iv_b num_bytes len j0_b iv_extra_b hkeys_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 /\
            compute_iv_post iv code iv_b num_bytes len j0_b iv_extra_b hkeys_b va_s0 va_s1 f /\
            ME.buffer_writeable (as_vale_buffer iv_b) /\
            ME.buffer_writeable (as_vale_buffer hkeys_b) /\
            ME.buffer_writeable (as_vale_buffer iv_extra_b) /\
            ME.buffer_writeable (as_vale_buffer j0_b)))
let compute_iv_lemma'
      (iv: Ghost.erased supported_iv_LE)
      (code: V.va_code)
      (_win: bool)
      (iv_b: b128)
      (num_bytes len: uint64)
      (j0_b iv_extra_b hkeys_b: b128)
      (va_s0: V.va_state)
    : Ghost (V.va_state & V.va_fuel)
      (requires compute_iv_pre iv code iv_b num_bytes len j0_b iv_extra_b hkeys_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 /\
            compute_iv_post iv code iv_b num_bytes len j0_b iv_extra_b hkeys_b va_s0 va_s1 f /\
            ME.buffer_writeable (as_vale_buffer iv_b) /\
            ME.buffer_writeable (as_vale_buffer hkeys_b) /\
            ME.buffer_writeable (as_vale_buffer iv_extra_b) /\
            ME.buffer_writeable (as_vale_buffer j0_b))) =
let va_s1, f =
  GC.va_lemma_Compute_iv_stdcall code va_s0 IA.win (Ghost.reveal iv) (as_vale_buffer iv_b)
    (UInt64.v num_bytes) (UInt64.v len) (as_vale_buffer j0_b) (as_vale_buffer iv_extra_b)
    (as_vale_buffer hkeys_b)
in
Vale.AsLowStar.MemoryHelpers.buffer_writeable_reveal ME.TUInt8 ME.TUInt128 iv_b;
Vale.AsLowStar.MemoryHelpers.buffer_writeable_reveal ME.TUInt8 ME.TUInt128 iv_extra_b;
Vale.AsLowStar.MemoryHelpers.buffer_writeable_reveal ME.TUInt8 ME.TUInt128 j0_b;
Vale.AsLowStar.MemoryHelpers.buffer_writeable_reveal ME.TUInt8 ME.TUInt128 hkeys_b;
va_s1, f
Vale.Stdcalls.X64.GCM_IV.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.MemoryHelpers.fsti.checked Vale.AsLowStar.LowStarSig.fst.checked Vale.AES.X64.GCMencryptOpt.fsti.checked Vale.AES.GCM_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 FStar.Ghost.fsti.checked
Vale.Stdcalls.X64.GCM_IV.fst
FStar.Ghost.erased Vale.AES.GCM_s.supported_iv_LE Vale.X64.Decls.va_code Prims.bool Vale.Stdcalls.X64.GCM_IV.b128 Vale.Stdcalls.X64.GCM_IV.uint64 Vale.X64.Decls.va_state Vale.X64.Decls.va_fuel FStar.Pervasives.Native.Mktuple2 Prims.unit Vale.AsLowStar.MemoryHelpers.buffer_writeable_reveal Vale.Arch.HeapTypes_s.TUInt8 Vale.Arch.HeapTypes_s.TUInt128 FStar.Pervasives.Native.tuple2 Vale.X64.State.vale_state Vale.AES.X64.GCMencryptOpt.va_lemma_Compute_iv_stdcall Vale.Interop.Assumptions.win FStar.Ghost.reveal Vale.X64.MemoryAdapters.as_vale_buffer FStar.UInt64.v Vale.Stdcalls.X64.GCM_IV.compute_iv_pre Prims.l_and Vale.X64.Decls.eval_code Vale.AsLowStar.ValeSig.vale_calling_conventions_stdcall Vale.Stdcalls.X64.GCM_IV.compute_iv_post Vale.X64.Memory.buffer_writeable
module Vale.Stdcalls.X64.GCM_IV

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

module GC = Vale.AES.X64.GCMencryptOpt
open Vale.AES.GCM_s

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 tuint64 = TD_Base TUInt64

[@__reduce__] noextract
let (dom: list td{List.length dom <= 20}) =
  let y = [t128_no_mod; tuint64; tuint64; t128_mod; t128_no_mod; t128_no_mod] in
  assert_norm (List.length y = 6);
  y


[@__reduce__] noextract
let compute_iv_pre : (Ghost.erased supported_iv_LE) -> VSig.vale_pre dom =
  fun (iv:Ghost.erased supported_iv_LE)
    (c:V.va_code)
    (iv_b:b128)
    (num_bytes:uint64)
    (len:uint64)
    (j0_b:b128)
    (iv_extra_b:b128)
    (hkeys_b:b128)
    (va_s0:V.va_state) ->
      GC.va_req_Compute_iv_stdcall c va_s0 IA.win (Ghost.reveal iv)
        (as_vale_buffer iv_b) (UInt64.v num_bytes)
        (UInt64.v len) (as_vale_buffer j0_b)
        (as_vale_buffer iv_extra_b) (as_vale_buffer hkeys_b)

[@__reduce__] noextract
let compute_iv_post : (Ghost.erased supported_iv_LE) -> VSig.vale_post dom =
  fun (iv:Ghost.erased supported_iv_LE)
    (c:V.va_code)
    (iv_b:b128)
    (num_bytes:uint64)
    (len:uint64)
    (j0_b:b128)
    (iv_extra_b:b128)
    (hkeys_b:b128)
    (va_s0:V.va_state)
    (va_s1:V.va_state)
    (f:V.va_fuel) ->
      GC.va_ens_Compute_iv_stdcall c va_s0 IA.win (Ghost.reveal iv)
        (as_vale_buffer iv_b) (UInt64.v num_bytes)
        (UInt64.v len) (as_vale_buffer j0_b)
        (as_vale_buffer iv_extra_b) (as_vale_buffer hkeys_b)
        va_s1 f

#set-options "--z3rlimit 50"

[@__reduce__] noextract
let compute_iv_lemma'
    (iv:Ghost.erased supported_iv_LE)
    (code:V.va_code)
    (_win:bool)
    (iv_b:b128)
    (num_bytes:uint64)
    (len:uint64)
    (j0_b:b128)
    (iv_extra_b:b128)
    (hkeys_b:b128)
    (va_s0:V.va_state)
  : Ghost (V.va_state & V.va_fuel)
    (requires compute_iv_pre iv code iv_b num_bytes len j0_b iv_extra_b hkeys_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 /\
      compute_iv_post iv code iv_b num_bytes len j0_b iv_extra_b hkeys_b va_s0 va_s1 f /\      
      ME.buffer_writeable (as_vale_buffer iv_b) /\
      ME.buffer_writeable (as_vale_buffer hkeys_b) /\
      ME.buffer_writeable (as_vale_buffer iv_extra_b) /\
val compute_iv_lemma'
      (iv: Ghost.erased supported_iv_LE)
      (code: V.va_code)
      (_win: bool)
      (iv_b: b128)
      (num_bytes len: uint64)
      (j0_b iv_extra_b hkeys_b: b128)
      (va_s0: V.va_state)
    : Ghost (V.va_state & V.va_fuel)
      (requires compute_iv_pre iv code iv_b num_bytes len j0_b iv_extra_b hkeys_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 /\
            compute_iv_post iv code iv_b num_bytes len j0_b iv_extra_b hkeys_b va_s0 va_s1 f /\
            ME.buffer_writeable (as_vale_buffer iv_b) /\
            ME.buffer_writeable (as_vale_buffer hkeys_b) /\
            ME.buffer_writeable (as_vale_buffer iv_extra_b) /\
            ME.buffer_writeable (as_vale_buffer j0_b)))

    iv: FStar.Ghost.erased Vale.AES.GCM_s.supported_iv_LE ->
    code: Vale.X64.Decls.va_code ->
    _win: Prims.bool ->
    iv_b: Vale.Stdcalls.X64.GCM_IV.b128 ->
    num_bytes: Vale.Stdcalls.X64.GCM_IV.uint64 ->
    len: Vale.Stdcalls.X64.GCM_IV.uint64 ->
    j0_b: Vale.Stdcalls.X64.GCM_IV.b128 ->
    iv_extra_b: Vale.Stdcalls.X64.GCM_IV.b128 ->
    hkeys_b: Vale.Stdcalls.X64.GCM_IV.b128 ->
    va_s0: Vale.X64.Decls.va_state
  -> Prims.Ghost (Vale.X64.Decls.va_state * Vale.X64.Decls.va_fuel)