val va_lemma_CreateHeaplets : va_b0:va_code -> va_s0:va_state -> buffers:(list buffer_info)
  -> Ghost (va_state & va_fuel)
  (requires (va_require_total va_b0 (va_code_CreateHeaplets ()) va_s0 /\ va_get_ok va_s0 /\ (let
    (bs:(FStar.Seq.Base.seq buffer_info)) = Vale.Lib.Seqs.list_to_seq #buffer_info buffers in
    Vale.X64.Memory.is_initial_heap (va_get_mem_layout va_s0) (va_get_mem va_s0) /\ (norm_list
    (Vale.Lib.Seqs.list_to_seq_post #buffer_info buffers bs 0) ==>
    Vale.X64.Memory.init_heaplets_req (va_get_mem va_s0) bs))))
  (ensures (fun (va_sM, va_fM) -> va_ensure_total va_b0 va_s0 va_sM va_fM /\ va_get_ok va_sM /\
    (let (bs:(FStar.Seq.Base.seq buffer_info)) = Vale.Lib.Seqs.list_to_seq #buffer_info buffers in
    norm_list (Vale.Lib.Seqs.list_to_seq_post #buffer_info buffers bs 0) /\
    Vale.X64.Memory.layout_modifies_loc ((va_get_mem_layout va_sM).vl_inner) == norm_loc
    (Vale.X64.Memory.loc_mutable_buffers buffers) /\ Vale.X64.Memory.layout_old_heap
    ((va_get_mem_layout va_sM).vl_inner) == va_get_mem va_s0 /\ Vale.X64.Memory.layout_buffers
    ((va_get_mem_layout va_sM).vl_inner) == bs /\ Vale.X64.Memory.layout_heaplets_initialized
    ((va_get_mem_layout va_sM).vl_inner) /\ (va_get_mem_layout va_sM).vl_taint ==
    (va_get_mem_layout va_s0).vl_taint /\ create_post (va_get_mem_layout va_sM) bs /\
    heaplet_id_is_none (va_get_mem va_sM) /\ (forall (h:heaplet_id) .
    {:pattern(trigger_create_heaplet h)}trigger_create_heaplet h ==> heaplet_id_is_some
    (Vale.X64.Decls.va_get_mem_heaplet h va_sM) h /\ Vale.X64.Memory.heaps_match bs
    ((va_get_mem_layout va_sM).vl_taint) (va_get_mem va_sM) (Vale.X64.Decls.va_get_mem_heaplet h
    va_sM) h) /\ (forall (i:nat) . {:pattern(Seq.index bs i)}i < FStar.Seq.Base.length #buffer_info
    bs ==> Vale.X64.Memory.buffer_info_has_id bs i ((FStar.Seq.Base.index
    #Vale.Arch.HeapImpl.buffer_info bs i).bi_heaplet))) /\ va_state_eq va_sM (va_update_mem_layout
    va_sM (va_update_ok va_sM va_s0))))
let va_lemma_CreateHeaplets va_b0 va_s0 buffers =
  va_reveal_opaque (`%va_code_CreateHeaplets) (va_code_CreateHeaplets ());
  let (va_old_s:va_state) = va_s0 in
  va_ins_lemma (mk_ins (make_instr_annotate (I.ins_Ghost) (S.AnnotateGhost ()))) va_s0;
  let (va_sM, va_fM) = va_eval_ins (mk_ins (make_instr_annotate (I.ins_Ghost) (S.AnnotateGhost
    ()))) va_s0 in
  let (bs:(FStar.Seq.Base.seq buffer_info)) = Vale.Lib.Seqs.list_to_seq #buffer_info buffers in
  Vale.Lib.Seqs.lemma_list_to_seq #buffer_info buffers;
  let va_sM = create_heaplets_this buffers va_sM in
  Vale.X64.Memory_Sems.lemma_create_heaplets buffers (va_old_s.vs_heap);
  Vale.X64.StateLemmas.use_machine_state_equal ();
  (va_sM, va_fM)
val va_lemma_CreateHeaplets : va_b0:va_code -> va_s0:va_state -> buffers:(list buffer_info)
  -> Ghost (va_state & va_fuel)
  (requires (va_require_total va_b0 (va_code_CreateHeaplets ()) va_s0 /\ va_get_ok va_s0 /\ (let
    (bs:(FStar.Seq.Base.seq buffer_info)) = Vale.Lib.Seqs.list_to_seq #buffer_info buffers in
    Vale.X64.Memory.is_initial_heap (va_get_mem_layout va_s0) (va_get_mem va_s0) /\ (norm_list
    (Vale.Lib.Seqs.list_to_seq_post #buffer_info buffers bs 0) ==>
    Vale.X64.Memory.init_heaplets_req (va_get_mem va_s0) bs))))
  (ensures (fun (va_sM, va_fM) -> va_ensure_total va_b0 va_s0 va_sM va_fM /\ va_get_ok va_sM /\
    (let (bs:(FStar.Seq.Base.seq buffer_info)) = Vale.Lib.Seqs.list_to_seq #buffer_info buffers in
    norm_list (Vale.Lib.Seqs.list_to_seq_post #buffer_info buffers bs 0) /\
    Vale.X64.Memory.layout_modifies_loc ((va_get_mem_layout va_sM).vl_inner) == norm_loc
    (Vale.X64.Memory.loc_mutable_buffers buffers) /\ Vale.X64.Memory.layout_old_heap
    ((va_get_mem_layout va_sM).vl_inner) == va_get_mem va_s0 /\ Vale.X64.Memory.layout_buffers
    ((va_get_mem_layout va_sM).vl_inner) == bs /\ Vale.X64.Memory.layout_heaplets_initialized
    ((va_get_mem_layout va_sM).vl_inner) /\ (va_get_mem_layout va_sM).vl_taint ==
    (va_get_mem_layout va_s0).vl_taint /\ create_post (va_get_mem_layout va_sM) bs /\
    heaplet_id_is_none (va_get_mem va_sM) /\ (forall (h:heaplet_id) .
    {:pattern(trigger_create_heaplet h)}trigger_create_heaplet h ==> heaplet_id_is_some
    (Vale.X64.Decls.va_get_mem_heaplet h va_sM) h /\ Vale.X64.Memory.heaps_match bs
    ((va_get_mem_layout va_sM).vl_taint) (va_get_mem va_sM) (Vale.X64.Decls.va_get_mem_heaplet h
    va_sM) h) /\ (forall (i:nat) . {:pattern(Seq.index bs i)}i < FStar.Seq.Base.length #buffer_info
    bs ==> Vale.X64.Memory.buffer_info_has_id bs i ((FStar.Seq.Base.index
    #Vale.Arch.HeapImpl.buffer_info bs i).bi_heaplet))) /\ va_state_eq va_sM (va_update_mem_layout
    va_sM (va_update_ok va_sM va_s0))))
let va_lemma_CreateHeaplets va_b0 va_s0 buffers =
va_reveal_opaque (`%va_code_CreateHeaplets) (va_code_CreateHeaplets ());
let va_old_s:va_state = va_s0 in
va_ins_lemma (mk_ins (make_instr_annotate (I.ins_Ghost) (S.AnnotateGhost ()))) va_s0;
let va_sM, va_fM =
  va_eval_ins (mk_ins (make_instr_annotate (I.ins_Ghost) (S.AnnotateGhost ()))) va_s0
in
let bs:(FStar.Seq.Base.seq buffer_info) = Vale.Lib.Seqs.list_to_seq #buffer_info buffers in
Vale.Lib.Seqs.lemma_list_to_seq #buffer_info buffers;
let va_sM = create_heaplets_this buffers va_sM in
Vale.X64.Memory_Sems.lemma_create_heaplets buffers (va_old_s.vs_heap);
Vale.X64.StateLemmas.use_machine_state_equal ();
(va_sM, va_fM)
Vale.X64.InsMem.fst.checked
Vale.X64.Taint_Semantics.fst.checked Vale.X64.StateLemmas.fsti.checked Vale.X64.Print_s.fst.checked Vale.X64.Memory_Sems.fsti.checked Vale.X64.Machine_Semantics_s.fst.checked Vale.X64.Instructions_s.fsti.checked Vale.X64.InsLemmas.fsti.checked Vale.X64.Decls.fst.checked Vale.Lib.Seqs.fsti.checked Vale.Def.Types_s.fst.checked Vale.Arch.HeapImpl.fsti.checked Vale.Arch.Heap.fsti.checked prims.fst.checked FStar.Seq.Base.fsti.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked
Vale.X64.InsMem.fst
Vale.X64.Decls.va_code Vale.X64.Decls.va_state Prims.list Vale.Arch.HeapImpl.buffer_info Vale.X64.State.vale_state Vale.X64.Lemmas.fuel FStar.Pervasives.Native.Mktuple2 Vale.X64.Decls.va_fuel Prims.unit Vale.X64.StateLemmas.use_machine_state_equal Vale.X64.Memory_Sems.lemma_create_heaplets Vale.X64.State.__proj__Mkvale_state__item__vs_heap Vale.X64.InsMem.create_heaplets_this Vale.Lib.Seqs.lemma_list_to_seq FStar.Seq.Base.seq Vale.Lib.Seqs.list_to_seq FStar.Pervasives.Native.tuple2 Prims.nat Vale.X64.Decls.va_eval_ins Vale.X64.Taint_Semantics.mk_ins Vale.X64.InsLemmas.make_instr_annotate Prims.Nil Vale.X64.Instruction_s.instr_out Vale.X64.Instruction_s.instr_operand Vale.X64.Instruction_s.PreserveFlags Vale.X64.Instructions_s.ins_Ghost Vale.X64.Machine_Semantics_s.AnnotateGhost Vale.X64.Instruction_s.InstrTypeRecord Vale.X64.Decls.va_ins_lemma Vale.X64.Decls.va_reveal_opaque Vale.X64.InsMem.va_code_CreateHeaplets
module Vale.X64.InsMem
open Vale.X64
open Vale.X64.StateLemmas
open Vale.X64.InsLemmas
open Vale.Arch.Heap
open Vale.Arch.HeapImpl
module I = Vale.X64.Instructions_s
module S = Vale.X64.Machine_Semantics_s
module P = Vale.X64.Print_s
open Vale.X64.Taint_Semantics

friend Vale.X64.Decls
#reset-options "--initial_fuel 2 --max_fuel 2 --max_ifuel 2 --z3rlimit 20"
//-- Mem64_in
//--
//-- Mem64_lemma

[@ "opaque_to_smt"]
let va_code_Mem64_lemma () =
  (va_Block (va_CNil ()))

[@ "opaque_to_smt"]
let va_codegen_success_Mem64_lemma () =
  (va_ttrue ())

[@"opaque_to_smt"]
let va_lemma_Mem64_lemma va_b0 va_s0 h base offset b index t =
  va_reveal_opaque (`%va_code_Mem64_lemma) (va_code_Mem64_lemma ());
  let (va_old_s:va_state) = va_s0 in
  let (va_b1:va_codes) = va_get_block va_b0 in
  let heap_h = va_get_mem_heaplet h va_s0 in
  lemma_opr_Mem64 h va_s0 base offset b index t;
  let (va_sM, va_fM) = va_lemma_empty_total va_s0 va_b1 in
  (va_sM, va_fM)


[@"opaque_to_smt"]
let va_wpProof_Mem64_lemma h base offset b index t va_s0 va_k =
  let (va_sM, va_f0) = va_lemma_Mem64_lemma (va_code_Mem64_lemma ()) va_s0 h base offset b index t
    in
  va_lemma_upd_update va_sM;
  assert (va_state_eq va_sM (va_update_ok va_sM va_s0));
  va_lemma_norm_mods ([]) va_sM va_s0;
  let va_g = () in
  (va_sM, va_f0, va_g)

//--
let create_heaplets_this (buffers:list buffer_info) (s:vale_state) : GTot vale_state =
  {s with vs_heap = Vale.X64.Memory_Sems.create_heaplets buffers s.vs_heap}

let destroy_heaplets_this (s:vale_state) : Ghost vale_state
  (requires state_inv s)
  (ensures fun _ -> True)
  =
  {s with vs_heap = Vale.X64.Memory_Sems.destroy_heaplets s.vs_heap}
//-- Vale.X64.StateLemmas.use_machine_state_equal
//--
//-- CreateHeaplets

[@ "opaque_to_smt"]
let va_code_CreateHeaplets () =
  (mk_ins (make_instr_annotate (I.ins_Ghost) (S.AnnotateGhost ())))

[@ "opaque_to_smt"]
let va_codegen_success_CreateHeaplets () =
  (va_ttrue ())

[@"opaque_to_smt"]
val va_lemma_CreateHeaplets : va_b0:va_code -> va_s0:va_state -> buffers:(list buffer_info)
  -> Ghost (va_state & va_fuel)
  (requires (va_require_total va_b0 (va_code_CreateHeaplets ()) va_s0 /\ va_get_ok va_s0 /\ (let
    (bs:(FStar.Seq.Base.seq buffer_info)) = Vale.Lib.Seqs.list_to_seq #buffer_info buffers in
    Vale.X64.Memory.is_initial_heap (va_get_mem_layout va_s0) (va_get_mem va_s0) /\ (norm_list
    (Vale.Lib.Seqs.list_to_seq_post #buffer_info buffers bs 0) ==>
    Vale.X64.Memory.init_heaplets_req (va_get_mem va_s0) bs))))
  (ensures (fun (va_sM, va_fM) -> va_ensure_total va_b0 va_s0 va_sM va_fM /\ va_get_ok va_sM /\
    (let (bs:(FStar.Seq.Base.seq buffer_info)) = Vale.Lib.Seqs.list_to_seq #buffer_info buffers in
    norm_list (Vale.Lib.Seqs.list_to_seq_post #buffer_info buffers bs 0) /\
    Vale.X64.Memory.layout_modifies_loc ((va_get_mem_layout va_sM).vl_inner) == norm_loc
    (Vale.X64.Memory.loc_mutable_buffers buffers) /\ Vale.X64.Memory.layout_old_heap
    ((va_get_mem_layout va_sM).vl_inner) == va_get_mem va_s0 /\ Vale.X64.Memory.layout_buffers
    ((va_get_mem_layout va_sM).vl_inner) == bs /\ Vale.X64.Memory.layout_heaplets_initialized
    ((va_get_mem_layout va_sM).vl_inner) /\ (va_get_mem_layout va_sM).vl_taint ==
    (va_get_mem_layout va_s0).vl_taint /\ create_post (va_get_mem_layout va_sM) bs /\
    heaplet_id_is_none (va_get_mem va_sM) /\ (forall (h:heaplet_id) .
    {:pattern(trigger_create_heaplet h)}trigger_create_heaplet h ==> heaplet_id_is_some
    (Vale.X64.Decls.va_get_mem_heaplet h va_sM) h /\ Vale.X64.Memory.heaps_match bs
    ((va_get_mem_layout va_sM).vl_taint) (va_get_mem va_sM) (Vale.X64.Decls.va_get_mem_heaplet h
    va_sM) h) /\ (forall (i:nat) . {:pattern(Seq.index bs i)}i < FStar.Seq.Base.length #buffer_info
    bs ==> Vale.X64.Memory.buffer_info_has_id bs i ((FStar.Seq.Base.index
    #Vale.Arch.HeapImpl.buffer_info bs i).bi_heaplet))) /\ va_state_eq va_sM (va_update_mem_layout
    va_sM (va_update_ok va_sM va_s0))))

    va_b0: Vale.X64.Decls.va_code ->
    va_s0: Vale.X64.Decls.va_state ->
    buffers: Prims.list Vale.Arch.HeapImpl.buffer_info
  -> Prims.Ghost (Vale.X64.Decls.va_state * Vale.X64.Decls.va_fuel)