val taint_arg_args_b8_mem (args: arg_list) (a: arg)
    : Lemma
    (List.memP a args /\ Some? (taint_of_arg a) ==> List.memP (taint_arg_b8 a) (args_b8 args))
let rec taint_arg_args_b8_mem (args:arg_list) (a:arg)
  : Lemma (List.memP a args /\ Some? (taint_of_arg a) ==>
           List.memP (taint_arg_b8 a) (args_b8 args))
  = match args with
    | [] -> ()
    | hd::tl ->
      taint_arg_args_b8_mem tl a
val taint_arg_args_b8_mem (args: arg_list) (a: arg)
    : Lemma
    (List.memP a args /\ Some? (taint_of_arg a) ==> List.memP (taint_arg_b8 a) (args_b8 args))
let rec taint_arg_args_b8_mem (args: arg_list) (a: arg)
    : Lemma
    (List.memP a args /\ Some? (taint_of_arg a) ==> List.memP (taint_arg_b8 a) (args_b8 args)) =
match args with
| [] -> ()
| hd :: tl -> taint_arg_args_b8_mem tl a
Vale.Interop.X64.fsti.checked
Vale.X64.Machine_Semantics_s.fst.checked Vale.X64.Machine_s.fst.checked Vale.Interop.Base.fst.checked Vale.Interop.Assumptions.fst.checked Vale.Def.Words_s.fsti.checked Vale.Arch.HeapTypes_s.fst.checked Vale.Arch.Heap.fsti.checked prims.fst.checked LowStar.BufferView.Up.fsti.checked LowStar.BufferView.Down.fsti.checked LowStar.Buffer.fst.checked FStar.UInt8.fsti.checked FStar.UInt64.fsti.checked FStar.UInt32.fsti.checked FStar.UInt16.fsti.checked FStar.StrongExcludedMiddle.fst.checked FStar.Set.fsti.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.Map.fsti.checked FStar.List.Tot.fst.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.fst.checked FStar.Ghost.fsti.checked FStar.FunctionalExtensionality.fsti.checked FStar.BigOps.fsti.checked
Vale.Interop.X64.fsti
Vale.Interop.X64.arg_list Vale.Interop.Base.arg Prims.list Vale.Interop.X64.taint_arg_args_b8_mem Prims.unit Prims.l_True Prims.squash Prims.l_imp Prims.l_and FStar.List.Tot.Base.memP Prims.b2t FStar.Pervasives.Native.uu___is_Some Vale.Arch.HeapTypes_s.taint Vale.Interop.X64.taint_of_arg Vale.Interop.Types.b8 Vale.Interop.X64.taint_arg_b8 Vale.Interop.Base.args_b8 Prims.Nil FStar.Pervasives.pattern
module Vale.Interop.X64
open FStar.Mul
open Vale.Interop.Base
open Vale.Arch.HeapTypes_s
open Vale.Arch.Heap
module B = LowStar.Buffer
module BS = Vale.X64.Machine_Semantics_s
module UV = LowStar.BufferView.Up
module DV = LowStar.BufferView.Down
module HS = FStar.HyperStack
module MS = Vale.X64.Machine_s
module IA = Vale.Interop.Assumptions
module List = FStar.List.Tot

////////////////////////////////////////////////////////////////////////////////
//The calling convention w.r.t the register mapping
////////////////////////////////////////////////////////////////////////////////

let calling_conventions
  (s0 s1:BS.machine_state)
  (regs_modified: MS.reg_64 -> bool)
  (xmms_modified: MS.reg_xmm -> bool) =
  let s0 = s0 in
  let s1 = s1 in
  s1.BS.ms_ok /\
  s0.BS.ms_regs MS.reg_Rsp == s1.BS.ms_regs MS.reg_Rsp /\
  (forall (r:MS.reg). {:pattern (s0.BS.ms_regs r)}
    match r with
    | MS.Reg 0 r -> not (regs_modified r) ==> s0.BS.ms_regs (MS.Reg 0 r) == s1.BS.ms_regs (MS.Reg 0 r)
    | MS.Reg 1 r -> not (xmms_modified r) ==> s0.BS.ms_regs (MS.Reg 1 r) == s1.BS.ms_regs (MS.Reg 1 r)
  )

let reg_nat (n:nat) = i:nat{i < n}
let arity_ok n 'a = l:list 'a { List.Tot.length l <= n }

(* We limit the number of args we can pass through the interop wrappers to an arbitrary 20.
   This ensures first that the addr_map axiom is sound: Since the length of buffers is limited to 2^32, we can prove that addr_map is inhabited.
   for extra arguments + the extra slots needed.
   Note that this number can be increased if needed*)
let arg_list = l:list arg{List.Tot.length l <= 20}
let arg_list_sb = l:list arg{List.Tot.length l <= 21}

unfold
let injective f = forall x y.{:pattern f x; f y} f x == f y ==> x == y

noeq
type arg_reg_relation' (n:nat) =
  | Rel: of_reg:(MS.reg_64 -> option (reg_nat n)) ->
         of_arg:(reg_nat n -> MS.reg_64){
           // This function should be injective
           injective of_arg /\
           // rRsp is not a valid register to store paramters
           (forall (i:reg_nat n).{:pattern of_arg i} of_arg i <> MS.rRsp) /\
           // of_reg should always return Some when the register corresponds to an of_arg
           (forall (i:reg_nat n).{:pattern of_arg i}
              Some? (of_reg (of_arg i)) /\ Some?.v (of_reg (of_arg i)) = i)} ->
         arg_reg_relation' n

unfold
let arg_reg_relation (n:nat) = (v:arg_reg_relation' n{
  // of_reg is a partial inverse of of_arg
  forall (r:MS.reg_64).{:pattern v.of_reg r} Some? (v.of_reg r) ==> v.of_arg (Some?.v (v.of_reg r)) = r})

let registers = MS.reg_64 -> MS.nat64

let upd_reg (n:nat) (arg_reg:arg_reg_relation n) (regs:registers) (i:nat) (v:_) : registers =
    fun (r:MS.reg_64) ->
      match arg_reg.of_reg r with
      | Some j ->
        if i = j then v
        else regs r
      | _ -> regs r

[@__reduce__]
let arg_as_nat64 (a:arg) : GTot MS.nat64 =
  let (| tag, x |) = a in
  match tag with
  | TD_Base TUInt8 ->
     UInt8.v x
  | TD_Base TUInt16 ->
     UInt16.v x
  | TD_Base TUInt32 ->
     UInt32.v x
  | TD_Base TUInt64 ->
     UInt64.v x
  | TD_Buffer src _ _ ->
    let b:b8 = Buffer true (x <: B.buffer (base_typ_as_type src)) in
    global_addrs_map b
  | TD_ImmBuffer src _ _ -> global_addrs_map (imm_to_b8 src x)

[@__reduce__]
let update_regs (n:nat)
                (arg_reg:arg_reg_relation n)
                (x:arg)
                (i:reg_nat n)
                (regs:registers)
  : GTot registers
  = upd_reg n arg_reg regs i (arg_as_nat64 x)

[@__reduce__]
let rec register_of_args (max_arity:nat)
                         (arg_reg:arg_reg_relation max_arity)
                         (n:nat)
                         (args:arg_list{List.Tot.length args = n})
                         (regs:registers) : GTot (regs':registers{regs MS.rRsp == regs' MS.rRsp}) =
    match args with
    | [] -> regs
    | hd::tl ->
      if n > max_arity then
        // This arguments will be passed on the stack
        register_of_args max_arity arg_reg (n-1) tl regs
      else
        update_regs max_arity arg_reg hd (n - 1) (register_of_args max_arity arg_reg (n - 1) tl regs)

// Pass extra arguments on the stack. The arity_ok condition on inline wrappers ensures that
// this only happens for stdcalls
[@__reduce__]
let rec stack_of_args (max_arity:nat)
                      (n:nat)
                      (rsp:int)
                      (args:arg_list{List.Tot.length args = n})
                      (st:Map.t int Vale.Def.Words_s.nat8)
                      : GTot (Map.t int Vale.Def.Words_s.nat8) =
  match args with
  | [] -> st
  | hd::tl ->
    if n <= max_arity then st // We can pass the remaining args in registers
    else
      let ptr = ((n - max_arity) - 1) * 8 // Arguments on the stack are pushed from right to left
        + (if IA.win then 32 else 0) // The shadow space on Windows comes next
        + 8 // The return address is then pushed on the stack
        + rsp // And we then have all the extra slots required for the Vale procedure
      in
      let st1 = stack_of_args max_arity (n-1) rsp tl st in
      let v = arg_as_nat64 hd in // We will store the arg hd
      BS.update_heap64 ptr v st1

////////////////////////////////////////////////////////////////////////////////
let taint_map = b8 -> GTot taint

let upd_taint_map_b8 (tm:taint_map) (x:b8) (tnt:taint) : taint_map =
   fun (y:b8) ->
     if StrongExcludedMiddle.strong_excluded_middle ((x <: b8) == y) then
        tnt
     else tm y

[@__reduce__]
let upd_taint_map_arg (a:arg) (tm:taint_map) : GTot taint_map =
    match a with
    | (| TD_Buffer _ _ {taint=tnt}, x |) ->
      upd_taint_map_b8 tm (Buffer true x) tnt
    | (| TD_ImmBuffer src _ {taint=tnt}, x |) ->
      upd_taint_map_b8 tm (imm_to_b8 src x) tnt
    | (| TD_Base _, _ |) ->
      tm

let init_taint : taint_map = fun r -> Public

[@__reduce__]
let mk_taint (args:arg_list_sb) (tm:taint_map) : GTot taint_map =
  List.fold_right_gtot args upd_taint_map_arg init_taint

let taint_of_arg (a:arg) =
  let (| tag, x |) = a in
  match tag with
  | TD_ImmBuffer _ TUInt64 {taint=tnt}
  | TD_ImmBuffer _ TUInt128 {taint=tnt}
  | TD_Buffer _ TUInt64 {taint=tnt}
  | TD_Buffer _ TUInt128 {taint=tnt} -> Some tnt
  | _ -> None

let taint_arg_b8 (a:arg{Some? (taint_of_arg a)}) : GTot b8 =
  let (| tag, x |) = a in
  match tag with
  | TD_Buffer src _ _ -> Buffer true (x <: B.buffer (base_typ_as_type src))
  | TD_ImmBuffer src _ _ -> imm_to_b8 src x

let rec taint_arg_args_b8_mem (args:arg_list) (a:arg)
  : Lemma (List.memP a args /\ Some? (taint_of_arg a) ==>
val taint_arg_args_b8_mem (args: arg_list) (a: arg)
    : Lemma
    (List.memP a args /\ Some? (taint_of_arg a) ==> List.memP (taint_arg_b8 a) (args_b8 args))
args: Vale.Interop.X64.arg_list -> a: Vale.Interop.Base.arg
  -> FStar.Pervasives.Lemma
    (ensures
      FStar.List.Tot.Base.memP a args /\ Some? (Vale.Interop.X64.taint_of_arg a) ==>
      FStar.List.Tot.Base.memP (Vale.Interop.X64.taint_arg_b8 a) (Vale.Interop.Base.args_b8 args))