val va_wpProof_MemLoad64 : h:va_operand_heaplet -> dst:va_operand_reg_opr ->
  base:va_operand_reg_opr -> offset:int -> t:taint -> b:buffer64 -> index:int -> va_s0:va_state ->
  va_k:(va_state -> unit -> Type0)
  -> Ghost (va_state & va_fuel & unit)
  (requires (va_t_require va_s0 /\ va_wp_MemLoad64 h dst base offset t b index va_s0 va_k))
  (ensures (fun (va_sM, va_f0, va_g) -> va_t_ensure (va_code_MemLoad64 h dst base offset t)
    ([va_mod_reg_opr dst]) va_s0 va_k ((va_sM, va_f0, va_g))))
let va_wpProof_MemLoad64 h dst base offset t b index va_s0 va_k =
  let (va_sM, va_f0) = va_lemma_MemLoad64 (va_code_MemLoad64 h dst base offset t) va_s0 h dst base
    offset t b index in
  va_lemma_upd_update va_sM;
  assert (va_state_eq va_sM (va_update_ok va_sM (va_update_operand_reg_opr dst va_sM va_s0)));
  va_lemma_norm_mods ([va_mod_reg_opr dst]) va_sM va_s0;
  let va_g = () in
  (va_sM, va_f0, va_g)
val va_wpProof_MemLoad64 : h:va_operand_heaplet -> dst:va_operand_reg_opr ->
  base:va_operand_reg_opr -> offset:int -> t:taint -> b:buffer64 -> index:int -> va_s0:va_state ->
  va_k:(va_state -> unit -> Type0)
  -> Ghost (va_state & va_fuel & unit)
  (requires (va_t_require va_s0 /\ va_wp_MemLoad64 h dst base offset t b index va_s0 va_k))
  (ensures (fun (va_sM, va_f0, va_g) -> va_t_ensure (va_code_MemLoad64 h dst base offset t)
    ([va_mod_reg_opr dst]) va_s0 va_k ((va_sM, va_f0, va_g))))
let va_wpProof_MemLoad64 h dst base offset t b index va_s0 va_k =
let va_sM, va_f0 =
  va_lemma_MemLoad64 (va_code_MemLoad64 h dst base offset t) va_s0 h dst base offset t b index
in
va_lemma_upd_update va_sM;
assert (va_state_eq va_sM (va_update_ok va_sM (va_update_operand_reg_opr dst va_sM va_s0)));
va_lemma_norm_mods ([va_mod_reg_opr dst]) va_sM va_s0;
let va_g = () in
(va_sM, va_f0, va_g)
Vale.PPC64LE.InsMem.fst.checked
Vale.PPC64LE.StateLemmas.fsti.checked Vale.PPC64LE.State.fsti.checked Vale.PPC64LE.Semantics_s.fst.checked Vale.PPC64LE.Memory_Sems.fsti.checked Vale.PPC64LE.Machine_s.fst.checked Vale.PPC64LE.InsBasic.fsti.checked Vale.PPC64LE.Decls.fst.checked Vale.PPC64LE.Decls.fst.checked Vale.Lib.Seqs.fsti.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.PPC64LE.InsMem.fst
Vale.PPC64LE.Decls.va_operand_heaplet Vale.PPC64LE.Decls.va_operand_reg_opr Prims.int Vale.Arch.HeapTypes_s.taint Vale.PPC64LE.Memory.buffer64 Vale.PPC64LE.Decls.va_state Prims.unit Vale.PPC64LE.Decls.va_fuel FStar.Pervasives.Native.Mktuple3 Vale.PPC64LE.QuickCode.va_lemma_norm_mods Prims.Cons Vale.PPC64LE.QuickCode.mod_t Vale.PPC64LE.QuickCode.va_mod_reg_opr Prims.Nil Prims._assert Vale.PPC64LE.Decls.va_state_eq Vale.PPC64LE.Decls.va_update_ok Vale.PPC64LE.Decls.va_update_operand_reg_opr Vale.PPC64LE.Decls.va_lemma_upd_update FStar.Pervasives.Native.tuple3 FStar.Pervasives.Native.tuple2 Vale.PPC64LE.Machine_s.state Vale.PPC64LE.InsMem.va_lemma_MemLoad64 Vale.PPC64LE.InsMem.va_code_MemLoad64
module Vale.PPC64LE.InsMem
open Vale.PPC64LE.Machine_s
open Vale.PPC64LE.State
open Vale.PPC64LE.StateLemmas
open Vale.PPC64LE.Decls
open Vale.PPC64LE.InsBasic
open Vale.Arch.Heap
open Vale.Arch.HeapImpl
module S = Vale.PPC64LE.Semantics_s

friend Vale.PPC64LE.Decls
#reset-options "--initial_fuel 2 --max_fuel 2 --max_ifuel 2 --z3rlimit 20"
let create_heaplets_this (buffers:list buffer_info) (s:state) : GTot state =
  {s with ms_heap = Vale.PPC64LE.Memory_Sems.create_heaplets buffers s.ms_heap}

let destroy_heaplets_this (s:state) : Ghost state
  (requires state_inv s)
  (ensures fun _ -> True)
  =
  {s with ms_heap = Vale.PPC64LE.Memory_Sems.destroy_heaplets s.ms_heap}
//-- CreateHeaplets

[@ "opaque_to_smt"]
let va_code_CreateHeaplets () =
  (Ins (S.Ghost ()))

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

[@"opaque_to_smt"]
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 (Ins (S.Ghost ())) va_s0;
  let (va_sM, va_fM) = va_eval_ins (Ins (S.Ghost ())) 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.PPC64LE.Memory_Sems.lemma_create_heaplets buffers (Vale.PPC64LE.Decls.from_heap_impl
    (va_old_s.ms_heap));
  Vale.PPC64LE.State.use_machine_state_equal ();
  (va_sM, va_fM)


[@"opaque_to_smt"]
let va_wpProof_CreateHeaplets buffers va_s0 va_k =
  let (va_sM, va_f0) = va_lemma_CreateHeaplets (va_code_CreateHeaplets ()) va_s0 buffers in
  va_lemma_upd_update va_sM;
  assert (va_state_eq va_sM (va_update_mem_layout va_sM (va_update_ok va_sM va_s0)));
  va_lemma_norm_mods ([va_Mod_mem_layout]) va_sM va_s0;
  let va_g = () in
  (va_sM, va_f0, va_g)

//--
//-- DestroyHeaplets

[@ "opaque_to_smt"]
let va_code_DestroyHeaplets () =
  (Ins (S.Ghost ()))

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

[@"opaque_to_smt"]
let va_lemma_DestroyHeaplets va_b0 va_s0 =
  va_reveal_opaque (`%va_code_DestroyHeaplets) (va_code_DestroyHeaplets ());
  let (va_old_s:va_state) = va_s0 in
  va_ins_lemma (Ins (S.Ghost ())) va_s0;
  let (va_sM, va_fM) = va_eval_ins (Ins (S.Ghost ())) va_s0 in
  let va_sM = destroy_heaplets_this va_sM in
  Vale.PPC64LE.Memory_Sems.lemma_destroy_heaplets (Vale.PPC64LE.Decls.from_heap_impl
    (va_old_s.ms_heap));
  Vale.PPC64LE.State.use_machine_state_equal ();
  (va_sM, va_fM)


[@"opaque_to_smt"]
let va_wpProof_DestroyHeaplets va_s0 va_k =
  let (va_sM, va_f0) = va_lemma_DestroyHeaplets (va_code_DestroyHeaplets ()) va_s0 in
  va_lemma_upd_update va_sM;
  assert (va_state_eq va_sM (va_update_mem_layout va_sM (va_update_ok va_sM va_s0)));
  va_lemma_norm_mods ([va_Mod_mem_layout]) va_sM va_s0;
  let va_g = () in
  (va_sM, va_f0, va_g)

//--
//-- MemLoad64

[@ "opaque_to_smt"]
let va_code_MemLoad64 h dst base offset t =
  (Ins (S.Load64 dst base offset))

[@ "opaque_to_smt"]
let va_codegen_success_MemLoad64 h dst base offset t =
  (va_ttrue ())

[@"opaque_to_smt"]
let va_lemma_MemLoad64 va_b0 va_s0 h dst base offset t b index =
  va_reveal_opaque (`%va_code_MemLoad64) (va_code_MemLoad64 h dst base offset t);
  let (va_old_s:va_state) = va_s0 in
  va_ins_lemma (Ins (S.Load64 dst base offset)) va_s0;
  let (va_sM, va_fM) = va_eval_ins (Ins (S.Load64 dst base offset)) va_s0 in
  Vale.PPC64LE.Memory_Sems.low_lemma_load_mem64_full b index (Vale.PPC64LE.Decls.from_heap_impl
    (va_sM.ms_heap)) t h;
  (va_sM, va_fM)
val va_wpProof_MemLoad64 : h:va_operand_heaplet -> dst:va_operand_reg_opr ->
  base:va_operand_reg_opr -> offset:int -> t:taint -> b:buffer64 -> index:int -> va_s0:va_state ->
  va_k:(va_state -> unit -> Type0)
  -> Ghost (va_state & va_fuel & unit)
  (requires (va_t_require va_s0 /\ va_wp_MemLoad64 h dst base offset t b index va_s0 va_k))
  (ensures (fun (va_sM, va_f0, va_g) -> va_t_ensure (va_code_MemLoad64 h dst base offset t)
    ([va_mod_reg_opr dst]) va_s0 va_k ((va_sM, va_f0, va_g))))

    h: Vale.PPC64LE.Decls.va_operand_heaplet ->
    dst: Vale.PPC64LE.Decls.va_operand_reg_opr ->
    base: Vale.PPC64LE.Decls.va_operand_reg_opr ->
    offset: Prims.int ->
    t: Vale.Arch.HeapTypes_s.taint ->
    b: Vale.PPC64LE.Memory.buffer64 ->
    index: Prims.int ->
    va_s0: Vale.PPC64LE.Decls.va_state ->
    va_k: (_: Vale.PPC64LE.Decls.va_state -> _: Prims.unit -> Type0)
  -> Prims.Ghost ((Vale.PPC64LE.Decls.va_state * Vale.PPC64LE.Decls.va_fuel) * Prims.unit)