val stack_args'
      (max_arity n: nat)
      (args: list arg {List.Tot.length args = n})
      (rsp: int)
      (stack: Map.t int Vale.Def.Words_s.nat8)
    : prop
let rec stack_args' (max_arity:nat)
                    (n:nat)
                    (args:list arg{List.Tot.length args = n})
                    (rsp:int)
                    (stack:Map.t int Vale.Def.Words_s.nat8)
                    : prop =
    match args with
    | [] -> True
    | hd::tl ->
        stack_args' max_arity (n-1) tl rsp stack /\
        (if n <= max_arity then True // This arg is passed in registers
         else
           let ptr = ((n - max_arity) - 1) * 8
             + (if IA.win then 32 else 0)
             + 8
             + rsp
           in
           BS.valid_addr64 ptr stack /\
           BS.get_heap_val64 ptr stack == IX64.arg_as_nat64 hd)
val stack_args'
      (max_arity n: nat)
      (args: list arg {List.Tot.length args = n})
      (rsp: int)
      (stack: Map.t int Vale.Def.Words_s.nat8)
    : prop
let rec stack_args'
      (max_arity n: nat)
      (args: list arg {List.Tot.length args = n})
      (rsp: int)
      (stack: Map.t int Vale.Def.Words_s.nat8)
    : prop =
match args with
| [] -> True
| hd :: tl ->
  stack_args' max_arity (n - 1) tl rsp stack /\
  (if n <= max_arity
    then True
    else
      let ptr = ((n - max_arity) - 1) * 8 + (if IA.win then 32 else 0) + 8 + rsp in
      BS.valid_addr64 ptr stack /\ BS.get_heap_val64 ptr stack == IX64.arg_as_nat64 hd)
Vale.AsLowStar.Wrapper.fst.checked
Vale.X64.StateLemmas.fsti.checked Vale.X64.State.fsti.checked Vale.X64.Stack_i.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.Lemmas.fsti.checked Vale.X64.Decls.fsti.checked Vale.Interop.X64.fsti.checked Vale.Interop.Base.fst.checked Vale.Interop.Assumptions.fst.checked Vale.Interop.fsti.checked Vale.Def.Words_s.fsti.checked Vale.AsLowStar.ValeSig.fst.checked Vale.AsLowStar.MemoryHelpers.fsti.checked Vale.AsLowStar.LowStarSig.fst.checked Vale.Arch.MachineHeap.fsti.checked Vale.Arch.HeapImpl.fsti.checked prims.fst.checked LowStar.BufferView.Up.fsti.checked LowStar.BufferView.Down.fsti.checked LowStar.Buffer.fst.checked FStar.UInt64.fsti.checked FStar.Set.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.Math.Lemmas.fst.checked FStar.Map.fsti.checked FStar.List.Tot.fst.checked FStar.List.fst.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.fst.checked FStar.FunctionalExtensionality.fsti.checked FStar.Classical.fsti.checked FStar.Calc.fsti.checked FStar.BigOps.fsti.checked
Vale.AsLowStar.Wrapper.fst
Prims.nat Prims.list Vale.Interop.Base.arg Prims.b2t Prims.op_Equality FStar.List.Tot.Base.length Prims.int FStar.Map.t Vale.Def.Words_s.nat8 Prims.l_True Prims.l_and Vale.AsLowStar.Wrapper.stack_args' Prims.op_Subtraction Prims.op_LessThanOrEqual Prims.bool Vale.Arch.MachineHeap_s.valid_addr64 Prims.eq2 Vale.Def.Types_s.nat64 Vale.Arch.MachineHeap_s.get_heap_val64 Vale.Interop.X64.arg_as_nat64 Prims.op_Addition FStar.Mul.op_Star Vale.Interop.Assumptions.win Prims.logical Prims.prop
module Vale.AsLowStar.Wrapper
open Vale.Arch.HeapImpl
open Vale.X64.MemoryAdapters
open Vale.Interop.Base
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 ME = Vale.X64.Memory
module SI = Vale.X64.Stack_i
module MS = Vale.X64.Machine_s
module IA = Vale.Interop.Assumptions
module I = Vale.Interop
module V = Vale.X64.Decls
module VS = Vale.X64.State
module IX64 = Vale.Interop.X64
module VSig = Vale.AsLowStar.ValeSig
module LSig = Vale.AsLowStar.LowStarSig
module SL = Vale.X64.StateLemmas
module VL = Vale.X64.Lemmas
module ST = FStar.HyperStack.ST
open FStar.Mul
open FStar.Calc

//let lemma_create_initial_vale_state_core
//    (#max_arity:nat)
//    (#reg_arg:IX64.arg_reg_relation max_arity)
//    (args:IX64.arg_list)
//    (h0:HS.mem{mem_roots_p h0 args})
//  : Lemma
//      (ensures (
//        let s = LSig.create_initial_vale_state #max_arity #reg_arg args h0 in
//        hs_of_mem (as_mem s.VS.vs_heap.vf_heap) == h0
//      ))
//  = ()

#reset-options "--initial_ifuel 2 --max_ifuel 2"
let rec core_create_lemma_disjointness
    (args:list arg{disjoint_or_eq args})
  : Lemma
    (ensures VSig.disjoint_or_eq args)
  = match args with
    | [] -> ()
    | hd::tl ->
      disjoint_or_eq_cons hd tl;
      BigOps.pairwise_and'_cons VSig.disjoint_or_eq_1 hd tl;
      core_create_lemma_disjointness tl;
      assert (VSig.disjoint_or_eq tl);
      let rec aux (n:list arg)
        : Lemma (requires (BigOps.big_and' (disjoint_or_eq_1 hd) n))
                (ensures (BigOps.big_and' (VSig.disjoint_or_eq_1 hd) n)) =
        match n with
        | [] -> ()
        | n::ns ->
          BigOps.big_and'_cons (disjoint_or_eq_1 hd) n ns;
          BigOps.big_and'_cons (VSig.disjoint_or_eq_1 hd) n ns;
          aux ns
      in
      aux tl
#reset-options

#push-options "--z3rlimit 40 --fuel 1 --ifuel 2"
let rec args_b8_lemma (args:list arg) (x:arg)
  : Lemma
      (List.memP x args ==>
        (match x with
         | (| TD_Buffer src bt _, x |) -> List.memP (mut_to_b8 src x) (args_b8 args)
         | (| TD_ImmBuffer src bt _, x |) -> List.memP (imm_to_b8 src x) (args_b8 args)
         | _ -> True))
  = match args with
    | [] -> ()
    | a::q ->
      assert (List.memP x q ==> List.memP x args);
      args_b8_lemma q x
#pop-options

let readable_cons (hd:arg) (tl:list arg) (s:ME.vale_heap)
  : Lemma VSig.(readable (hd::tl) s <==> (readable_one s hd /\ readable tl s))
  = BigOps.big_and'_cons VSig.(readable_one s) hd tl

let arg_is_registered_root (h:ME.vale_heap) (a:arg) =
  match a with
  | (| TD_Buffer src bt _, x |) ->
    List.memP (mut_to_b8 src x) (ptrs_of_mem (as_mem h))
  | (| TD_ImmBuffer src bt _, x |) ->
    List.memP (imm_to_b8 src x) (ptrs_of_mem (as_mem h))
  | _ -> true

#set-options "--z3rlimit 20"

let core_create_lemma_readable
    (#max_arity:nat)
    (#arg_reg:IX64.arg_reg_relation max_arity)
    (args:IX64.arg_list)
    (h0:HS.mem{mem_roots_p h0 args})
  : Lemma
      (ensures
        (let va_s = LSig.create_initial_vale_state #max_arity #arg_reg args h0 in
         VSig.readable args (ME.get_vale_heap va_s.VS.vs_heap)))
  =
    let readable_registered_one (a:arg) (h:ME.vale_heap)
      : Lemma VSig.(arg_is_registered_root h a <==> readable_one h a)
      = match a with
        | (| TD_Buffer src bt _, x |) ->
          Vale.AsLowStar.MemoryHelpers.reveal_readable #src #bt x h;
          Vale.AsLowStar.MemoryHelpers.buffer_writeable_reveal src bt x
        | (| TD_ImmBuffer src bt ig, x |) ->
          Vale.AsLowStar.MemoryHelpers.reveal_imm_readable #src #bt x h;
          assert_norm (ME.buffer_readable h (as_vale_immbuffer #src #bt x) <==>
                       VSig.readable_one h (| TD_ImmBuffer src bt ig, x |))
        | (| TD_Base _, _ |) -> ()
    in
    let rec readable_registered_all
        (args:list arg)
        (h:ME.vale_heap {forall x. List.memP x args ==> arg_is_registered_root h x})
      : Lemma VSig.(readable args h)
      = match args with
        | [] -> ()
        | hd::tl ->
          readable_cons hd tl h;
          readable_registered_one hd h;
          readable_registered_all tl h
     in
     let readable_mk_mem
         (args:list arg)
         (h:mem_roots args)
       : Lemma
           (let mem = mk_mem args h in
            VSig.readable args (create_initial_vale_heap mem))
       = let mem = mk_mem args h in
         FStar.Classical.forall_intro (FStar.Classical.move_requires (args_b8_lemma args));
         readable_registered_all args (create_initial_vale_heap mem)
     in
     readable_mk_mem args h0

let readable_live_one (h:ME.vale_heap) (a:arg)
  : Lemma (VSig.readable_one h a ==>
           live_arg (hs_of_mem (as_mem h)) a)
  = match a with
    | (| TD_Buffer src bt _, x |) ->
      Vale.AsLowStar.MemoryHelpers.readable_live #src #bt x h
    | (| TD_ImmBuffer src bt ig, x |) ->
      Vale.AsLowStar.MemoryHelpers.readable_imm_live #src #bt x h;
      assert_norm (ME.buffer_readable h (as_vale_immbuffer #src #bt x) <==>
                   VSig.readable_one h (| TD_ImmBuffer src bt ig, x |))
    | (| TD_Base _, _ |) -> ()

let rec readable_all_live (h:ME.vale_heap) (args:list arg)
  : Lemma (VSig.readable args h ==>
           all_live (hs_of_mem (as_mem h)) args)
  = match args with
    | [] -> ()
    | hd::tl ->
      readable_cons hd tl h;
      all_live_cons hd tl (hs_of_mem (as_mem h));
      readable_live_one h hd;
      readable_all_live h tl

let core_create_lemma_mem_correspondance
    (#max_arity:nat)
    (#arg_reg:IX64.arg_reg_relation max_arity)
    (args:IX64.arg_list)
    (h0:HS.mem{mem_roots_p h0 args})
  : Lemma
      (ensures
        (let va_s = LSig.create_initial_vale_state #max_arity #arg_reg args h0 in
         LSig.mem_correspondence args h0 va_s))
  =
    let va_s = LSig.create_initial_vale_state #max_arity #arg_reg args h0 in
    let rec aux (accu:list arg) : Lemma
      (requires (forall x. List.memP x accu ==> (live_arg h0 x)))
      (ensures LSig.mem_correspondence accu h0 va_s) =
    match accu with
    | [] -> ()
    | hd::tl -> aux tl;
      match hd with
      | (| TD_Buffer src bt _, x |) ->
        Vale.AsLowStar.MemoryHelpers.buffer_as_seq_reveal src bt x args h0;
        let db = get_downview x in
        DV.length_eq db;
        let ub = UV.mk_buffer db (LSig.view_of_base_typ bt) in
        assert (Seq.equal (UV.as_seq h0 ub) (UV.as_seq h0 ub))
      | (| TD_ImmBuffer src bt _, x |) ->
        Vale.AsLowStar.MemoryHelpers.immbuffer_as_seq_reveal src bt x args h0;
        let db = get_downview x in
        DV.length_eq db;
        let ub = UV.mk_buffer db (LSig.view_of_base_typ bt) in
        assert (Seq.equal (UV.as_seq h0 ub) (UV.as_seq h0 ub))
      | (| TD_Base _, _ |) -> ()
    in
    BigOps.big_and'_forall (live_arg h0) args;
    aux args

let rec register_args'
    (max_arity:nat)
    (arg_reg:IX64.arg_reg_relation max_arity)
    (n:nat)
    (args:list arg{List.length args = n})
    (regs:IX64.registers)
  : prop
  = match args with
    | [] -> True
    | hd::tl ->
      register_args' max_arity arg_reg (n - 1) tl regs /\
      (if n > max_arity then True
       else regs (arg_reg.IX64.of_arg (n - 1)) == IX64.arg_as_nat64 hd)

let rec lemma_register_args'_aux
    (max_arity:nat)
    (arg_reg:IX64.arg_reg_relation max_arity)
    (n:nat)
    (args:list arg{List.length args = n})
    (regs1 regs2:IX64.registers)
  : Lemma
      (requires
        register_args' max_arity arg_reg n args regs1 /\
        (forall r. (forall (i:IX64.reg_nat max_arity{i >= n}). r <> (arg_reg.IX64.of_arg i)) /\
              r <> MS.rRsp ==>
              regs1 r == regs2 r))
      (ensures register_args' max_arity arg_reg n args regs2)
  = match args with
    | [] -> ()
    | hd::tl ->
      lemma_register_args'_aux max_arity arg_reg (n-1) tl regs1 regs2

let rec lemma_register_args'
    (max_arity:nat)
    (arg_reg:IX64.arg_reg_relation max_arity)
    (args:IX64.arg_list)
    (regs:IX64.registers)
  : Lemma
     (ensures
       (let final_regs = IX64.register_of_args max_arity arg_reg (List.length args) args regs in
        register_args' max_arity arg_reg (List.length args) args final_regs))
  = let final_regs = IX64.register_of_args max_arity arg_reg (List.length args) args regs in
    match args with
    | [] -> ()
    | hd::tl ->
      let n = List.length args in
      let regs' = (IX64.register_of_args max_arity arg_reg (n-1) tl regs) in
      lemma_register_args' max_arity arg_reg tl regs;
      lemma_register_args'_aux max_arity arg_reg (n-1) tl regs' final_regs

let core_create_lemma_register_args
    (#max_arity:nat)
    (#arg_reg:IX64.arg_reg_relation max_arity)
    (args:IX64.arg_list)
    (h0:HS.mem{mem_roots_p h0 args})
  : Lemma
      (ensures (let va_s = LSig.create_initial_vale_state #max_arity #arg_reg args h0 in
                LSig.register_args max_arity arg_reg (List.length args) args va_s))
  =
    let va_s = LSig.create_initial_vale_state #max_arity #arg_reg args h0 in
    let regs' = IX64.register_of_args max_arity arg_reg (List.Tot.length args) args IA.init_regs in
    lemma_register_args' max_arity arg_reg args IA.init_regs;
    let open MS in
    let regs = FunctionalExtensionality.on reg_64 regs' in
    lemma_register_args'_aux max_arity arg_reg (List.length args) args regs' regs;
    assert (register_args' max_arity arg_reg (List.length args) args regs);
    let rec aux
        (args:IX64.arg_list)
        (s:VS.vale_state)
        (args':list arg)
        (h0:HS.mem{mem_roots_p h0 args'})
     : Lemma
         (requires
            (forall r. VS.eval_reg_64 r s == regs r) /\
            register_args' max_arity arg_reg (List.length args) args regs /\
            s.VS.vs_heap.vf_heap == create_initial_vale_heap (mk_mem args' h0))
         (ensures LSig.register_args max_arity arg_reg (List.length args) args s)
         (decreases args)
    = let n = List.length args in
      match args with
      | [] -> ()
      | hd::tl -> aux tl s args' h0;
        let (| tag, x |) = hd in
        match tag with
        | TD_Buffer src bt _ -> Vale.AsLowStar.MemoryHelpers.buffer_addr_reveal src bt x args' h0
        | TD_ImmBuffer src bt _ -> Vale.AsLowStar.MemoryHelpers.immbuffer_addr_reveal src bt x args' h0
        | TD_Base _ -> ()
      in
      aux args va_s args h0

let core_create_lemma_state
    (#max_arity:nat)
    (#arg_reg:IX64.arg_reg_relation max_arity)
    (args:IX64.arg_list)
    (h0:HS.mem{mem_roots_p h0 args})
  : Lemma
      (ensures
        (let va_s = LSig.create_initial_vale_state #max_arity #arg_reg args h0 in
         fst (IX64.create_initial_trusted_state max_arity arg_reg args h0) == SL.state_to_S va_s))
  = let va_s = LSig.create_initial_vale_state #max_arity #arg_reg args h0 in
    let tr_s = fst (IX64.create_initial_trusted_state max_arity arg_reg args h0) in
    let sl_s = SL.state_to_S va_s in
    assert (tr_s.BS.ms_stackTaint == va_s.VS.vs_stackTaint);
    //SL.lemma_to_ok va_s;
    let aux_flag (f:MS.flag) : Lemma (tr_s.BS.ms_flags f == sl_s.BS.ms_flags f)
      = ()//SL.lemma_to_flags va_s f
    in
    Classical.forall_intro aux_flag;
    assert (FunctionalExtensionality.feq tr_s.BS.ms_flags sl_s.BS.ms_flags);
    //SL.lemma_to_mem va_s;
    //SL.lemma_to_stack va_s;
    let aux_reg (r:MS.reg) : Lemma (tr_s.BS.ms_regs r == sl_s.BS.ms_regs r)
      = ()//SL.lemma_to_reg va_s r
    in
    Classical.forall_intro aux_reg;
    assert (FunctionalExtensionality.feq tr_s.BS.ms_regs sl_s.BS.ms_regs);
//    Vale.AsLowStar.MemoryHelpers.get_heap_mk_mem_reveal args h0;
    Vale.AsLowStar.MemoryHelpers.mk_stack_reveal tr_s.BS.ms_stack

let rec stack_args' (max_arity:nat)
                    (n:nat)
                    (args:list arg{List.Tot.length args = n})
                    (rsp:int)
                    (stack:Map.t int Vale.Def.Words_s.nat8)
val stack_args'
      (max_arity n: nat)
      (args: list arg {List.Tot.length args = n})
      (rsp: int)
      (stack: Map.t int Vale.Def.Words_s.nat8)
    : prop

    max_arity: Prims.nat ->
    n: Prims.nat ->
    args: Prims.list Vale.Interop.Base.arg {FStar.List.Tot.Base.length args = n} ->
    rsp: Prims.int ->
    stack: FStar.Map.t Prims.int Vale.Def.Words_s.nat8
  -> Prims.prop