let vale_sig_stdcall #dom = vale_sig #dom IX64.regs_modified_stdcall IX64.xmms_modified_stdcall
let vale_sig_stdcall #dom =
vale_sig #dom IX64.regs_modified_stdcall IX64.xmms_modified_stdcall
Vale.AsLowStar.ValeSig.fst.checked
Vale.X64.State.fsti.checked Vale.X64.MemoryAdapters.fsti.checked Vale.X64.Memory.fsti.checked Vale.X64.Machine_Semantics_s.fst.checked Vale.X64.Machine_s.fst.checked Vale.X64.Decls.fsti.checked Vale.Lib.Map16.fsti.checked Vale.Interop.X64.fsti.checked Vale.Interop.Base.fst.checked Vale.Interop.Assumptions.fst.checked Vale.Arch.HeapImpl.fsti.checked prims.fst.checked LowStar.BufferView.fsti.checked LowStar.Buffer.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.List.Tot.fst.checked FStar.HyperStack.fst.checked FStar.BigOps.fsti.checked
Vale.AsLowStar.ValeSig.fst
Prims.list Vale.Interop.Base.td Vale.AsLowStar.ValeSig.vale_sig Vale.Interop.X64.regs_modified_stdcall Vale.Interop.X64.xmms_modified_stdcall Vale.AsLowStar.ValeSig.vale_pre Vale.AsLowStar.ValeSig.vale_post
module Vale.AsLowStar.ValeSig
open FStar.Mul
open Vale.Arch.HeapImpl
open Vale.Interop.Base
module B = LowStar.Buffer
module BS = Vale.X64.Machine_Semantics_s
module BV = LowStar.BufferView
module HS = FStar.HyperStack
module ME = Vale.X64.Memory
module MS = Vale.X64.Machine_s
module IA = Vale.Interop.Assumptions
module V = Vale.X64.Decls
module VS = Vale.X64.State
module IX64 = Vale.Interop.X64
module List = FStar.List.Tot
module Map16 = Vale.Lib.Map16
open Vale.X64.MemoryAdapters

[@__reduce__]
let vale_pre_tl (dom:list td) =
    n_arrow dom (V.va_state -> prop)

[@__reduce__]
let vale_pre (dom:list td) =
    code:V.va_code ->
    vale_pre_tl dom

[@__reduce__]
let vale_post_tl (dom:list td) =
    n_arrow dom
            (s0:V.va_state -> s1:V.va_state -> f:V.va_fuel -> prop)

[@__reduce__]
let vale_post (dom:list td) =
    code:V.va_code ->
    vale_post_tl dom

let vale_save_reg (r:MS.reg_64) (s0 s1:V.va_state) =
  VS.eval_reg_64 r s0 == VS.eval_reg_64 r s1

let vale_save_xmm (r:MS.reg_xmm) (s0 s1:V.va_state) =
  VS.eval_reg_xmm r s0 == VS.eval_reg_xmm r s1

let vale_calling_conventions
  (s0 s1:V.va_state)
  (regs_modified:MS.reg_64 -> bool)
  (xmms_modified:MS.reg_xmm -> bool) =
  let open MS in
  s1.VS.vs_ok /\
  vale_save_reg MS.rRsp s0 s1 /\
  (forall (r:MS.reg_64).
    not (regs_modified r) ==> vale_save_reg r s0 s1) /\
  (forall (x:MS.reg_xmm).
    not (xmms_modified x) ==> vale_save_xmm x s0 s1)

[@__reduce__]
let modified_arg_mloc (x:arg) : GTot ME.loc =
    match x with
    | (|TD_Buffer src t {modified=true}, x|) -> ME.loc_buffer (as_vale_buffer #src #t x)
    | _ -> ME.loc_none

[@__reduce__]
let mloc_modified_args (args:list arg) : GTot ME.loc =
    List.fold_right_gtot (List.map_gtot modified_arg_mloc args) ME.loc_union ME.loc_none

let state_of (x:(V.va_state & V.va_fuel)) = fst x
let fuel_of (x:(V.va_state & V.va_fuel)) = snd x
let sprop = VS.vale_state -> prop


[@__reduce__]
let readable_one (s:ME.vale_heap) (arg:arg) : prop =
  match arg with
  | (|TD_Buffer src bt _, x |) ->
    ME.buffer_readable s (as_vale_buffer #src #bt x) /\
    ME.buffer_writeable (as_vale_buffer #src #bt x)
    /\ True //promote to prop
  | (|TD_ImmBuffer src bt _, x |) ->
    ME.buffer_readable s (as_vale_immbuffer #src #bt x) /\
    True
  | _ -> True

[@__reduce__]
let readable (args:list arg) (s:ME.vale_heap) : prop =
    BigOps.big_and' (readable_one s) args


[@__reduce__]
let disjoint_or_eq_1 (a:arg) (b:arg) =
    match a, b with
    | (| TD_Buffer srcx tx {strict_disjointness=true}, xb |), (| TD_Buffer srcy ty _, yb |)
    | (| TD_Buffer srcx tx _, xb |), (| TD_Buffer srcy ty {strict_disjointness=true}, yb |) ->
      ME.loc_disjoint (ME.loc_buffer (as_vale_buffer #srcx #tx xb)) (ME.loc_buffer (as_vale_buffer #srcy #ty yb))
    | (| TD_ImmBuffer srcx tx {strict_disjointness=true}, xb |), (| TD_ImmBuffer srcy ty _, yb |)
    | (| TD_ImmBuffer srcx tx _, xb |), (| TD_ImmBuffer srcy ty {strict_disjointness=true}, yb |) ->
      ME.loc_disjoint (ME.loc_buffer (as_vale_immbuffer #srcx #tx xb)) (ME.loc_buffer (as_vale_immbuffer #srcy #ty yb))
    // An immutable buffer and a trivial buffer should not be equal
    | (| TD_ImmBuffer srcx tx _, xb |), (| TD_Buffer srcy ty _, yb |) ->
      ME.loc_disjoint (ME.loc_buffer (as_vale_immbuffer #srcx #tx xb)) (ME.loc_buffer (as_vale_buffer #srcy #ty yb))
    | (| TD_Buffer srcx tx _, xb |), (| TD_ImmBuffer srcy ty _, yb |) ->
      ME.loc_disjoint (ME.loc_buffer (as_vale_buffer #srcx #tx xb)) (ME.loc_buffer (as_vale_immbuffer #srcy #ty yb))
    | (| TD_Buffer srcx tx _, xb |), (| TD_Buffer srcy ty _, yb |) ->
      ME.loc_disjoint (ME.loc_buffer (as_vale_buffer #srcx #tx xb)) (ME.loc_buffer (as_vale_buffer #srcy #ty yb)) \/
      xb === yb
    | (| TD_ImmBuffer srcx tx _, xb |), (| TD_ImmBuffer srcy ty _, yb |) ->
      ME.loc_disjoint (ME.loc_buffer (as_vale_immbuffer #srcx #tx xb)) (ME.loc_buffer (as_vale_immbuffer #srcy #ty yb)) \/
      xb === yb
    | _ -> True

[@__reduce__]
let disjoint_or_eq (l:list arg) =
  BigOps.pairwise_and' disjoint_or_eq_1  l

[@__reduce__] unfold
let vale_sig_nil
                 (regs_modified:MS.reg_64 -> bool)
                 (xmms_modified:MS.reg_xmm -> bool)
                 (args:list arg)
                 (code:V.va_code)
                 (pre:vale_pre_tl [])
                 (post:vale_post_tl []) =
    va_s0:V.va_state ->
    Ghost (V.va_state & V.va_fuel)
     (requires
       elim_nil pre va_s0)
     (ensures (fun r ->
       let va_s1 = state_of r in
       let f = fuel_of r in
       V.eval_code code va_s0 f va_s1 /\
       vale_calling_conventions va_s0 va_s1 regs_modified xmms_modified /\
       elim_nil post va_s0 va_s1 f /\
       readable args (ME.get_vale_heap va_s1.VS.vs_heap) /\
       ME.modifies (mloc_modified_args args) (VS.vs_get_vale_heap va_s0) (VS.vs_get_vale_heap va_s1)))

[@__reduce__]
let rec vale_sig_tl (regs_modified:MS.reg_64 -> bool)
                    (xmms_modified:MS.reg_xmm -> bool)
                    (#dom:list td)
                    (args:list arg)
                    (code:V.va_code)
                    (pre:vale_pre_tl dom)
                    (post:vale_post_tl dom)
  : Type =
    match dom with
    | [] ->
      vale_sig_nil regs_modified xmms_modified args code pre post

    | hd::tl ->
      x:td_as_type hd ->
      vale_sig_tl regs_modified xmms_modified #tl ((|hd,x|)::args) code (elim_1 pre x) (elim_1 post x)

[@__reduce__]
let elim_vale_sig_nil  #code
                       (#regs_modified:MS.reg_64 -> bool)
                       (#xmms_modified:MS.reg_xmm -> bool)
                       (#args:list arg)
                       (#pre:vale_pre_tl [])
                       (#post:vale_post_tl [])
                       (v:vale_sig_tl regs_modified xmms_modified #[] args code pre post)
    : vale_sig_nil regs_modified xmms_modified args code pre post
    = v

[@__reduce__]
let elim_vale_sig_cons #code
                       (#regs_modified:MS.reg_64 -> bool)
                       (#xmms_modified:MS.reg_xmm -> bool)
                       (hd:td)
                       (tl:list td)
                       (args:list arg)
                       (pre:vale_pre_tl (hd::tl))
                       (post:vale_post_tl (hd::tl))
                       (v:vale_sig_tl regs_modified xmms_modified args code pre post)
    : x:td_as_type hd
    -> vale_sig_tl regs_modified xmms_modified ((|hd, x|)::args) code (elim_1 pre x) (elim_1 post x)
    = v

[@__reduce__]
let vale_sig (#dom:list td)
             (regs_modified:MS.reg_64 -> bool)
             (xmms_modified:MS.reg_xmm -> bool)
             (pre:vale_pre dom)
             (post:vale_post dom)
  : Type =
    code:V.va_code ->
    win:bool ->
    vale_sig_tl
      regs_modified
      xmms_modified
      []
      code
      (pre code)
      (post code)
val vale_sig_stdcall : pre: Vale.AsLowStar.ValeSig.vale_pre dom -> post: Vale.AsLowStar.ValeSig.vale_post dom -> Type
pre: Vale.AsLowStar.ValeSig.vale_pre dom -> post: Vale.AsLowStar.ValeSig.vale_post dom -> Type