val readable_cons (hd: arg) (tl: list arg) (s: ME.vale_heap)
    : Lemma VSig.(readable (hd :: tl) s <==> (readable_one s hd /\ readable tl s))
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
val readable_cons (hd: arg) (tl: list arg) (s: ME.vale_heap)
    : Lemma VSig.(readable (hd :: tl) s <==> (readable_one s hd /\ readable tl s))
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
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
Vale.Interop.Base.arg Prims.list Vale.X64.Memory.vale_heap FStar.BigOps.big_and'_cons Vale.AsLowStar.ValeSig.readable_one Prims.unit Prims.l_True Prims.squash Prims.l_iff Vale.AsLowStar.ValeSig.readable Prims.Cons Prims.l_and Prims.Nil FStar.Pervasives.pattern
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)
val readable_cons (hd: arg) (tl: list arg) (s: ME.vale_heap)
    : Lemma VSig.(readable (hd :: tl) s <==> (readable_one s hd /\ readable tl s))
hd: Vale.Interop.Base.arg -> tl: Prims.list Vale.Interop.Base.arg -> s: Vale.X64.Memory.vale_heap
  -> FStar.Pervasives.Lemma
    (ensures
      Vale.AsLowStar.ValeSig.readable (hd :: tl) s <==>
      Vale.AsLowStar.ValeSig.readable_one s hd /\ Vale.AsLowStar.ValeSig.readable tl s)