let registers = MS.reg_64 -> MS.nat64
let registers =
MS.reg_64 -> MS.nat64
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.X64.Machine_s.reg_64 Vale.X64.Machine_s.nat64
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})
val registers : Type0
Type0