val 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 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
val 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 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
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 Vale.Interop.X64.arg_reg_relation Vale.Interop.X64.arg_list FStar.Monotonic.HyperStack.mem Vale.Interop.Base.mem_roots_p Prims.list Vale.Interop.Base.arg Vale.Interop.Base.mem_roots Prims.unit Prims.l_True Prims.squash Vale.AsLowStar.ValeSig.readable Vale.X64.MemoryAdapters.create_initial_vale_heap Vale.Interop.Base.mk_mem Prims.Nil FStar.Pervasives.pattern FStar.Classical.forall_intro Prims.l_imp FStar.List.Tot.Base.memP Vale.Arch.HeapTypes_s.base_typ Vale.Interop.Base.buffer_qualifiers Vale.Interop.Base.td_as_type Vale.Interop.Base.TD_Buffer Vale.Interop.Types.b8 Vale.Interop.Base.mut_to_b8 Vale.Interop.Base.args_b8 Vale.Interop.Base.TD_ImmBuffer Vale.Interop.Base.imm_to_b8 Prims.dtuple2 Vale.Interop.Base.td Prims.logical FStar.Classical.move_requires Vale.AsLowStar.Wrapper.args_b8_lemma Vale.Interop.Heap_s.interop_heap Vale.X64.Memory.vale_heap Prims.l_Forall Vale.AsLowStar.Wrapper.arg_is_registered_root Vale.AsLowStar.Wrapper.readable_cons Vale.Arch.HeapImpl.vale_heap Prims.l_iff Vale.AsLowStar.ValeSig.readable_one Vale.AsLowStar.MemoryHelpers.buffer_writeable_reveal Vale.AsLowStar.MemoryHelpers.reveal_readable FStar.Pervasives.assert_norm Vale.X64.Memory.buffer_readable Vale.X64.MemoryAdapters.as_vale_immbuffer Prims.Mkdtuple2 Vale.AsLowStar.MemoryHelpers.reveal_imm_readable Vale.Interop.Base.valid_base_type Vale.Interop.Base.TD_Base Vale.X64.Memory.get_vale_heap Vale.X64.State.__proj__Mkvale_state__item__vs_heap Vale.X64.Decls.vale_state_with_inv Vale.AsLowStar.LowStarSig.create_initial_vale_state
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
val 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)))

    args: Vale.Interop.X64.arg_list ->
    h0: FStar.Monotonic.HyperStack.mem{Vale.Interop.Base.mem_roots_p h0 args}
  -> FStar.Pervasives.Lemma
    (ensures
      (let va_s = Vale.AsLowStar.LowStarSig.create_initial_vale_state args h0 in
        Vale.AsLowStar.ValeSig.readable args
          (Vale.X64.Memory.get_vale_heap (Mkvale_state?.vs_heap va_s))))