val va_codegen_success_CreateHeaplets : va_dummy:unit -> Tot va_pbool
let va_codegen_success_CreateHeaplets () =
  (va_ttrue ())
val va_codegen_success_CreateHeaplets : va_dummy:unit -> Tot va_pbool
let va_codegen_success_CreateHeaplets () =
(va_ttrue ())
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
Prims.unit Vale.PPC64LE.Decls.va_ttrue Vale.PPC64LE.Decls.va_pbool
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"]
val va_codegen_success_CreateHeaplets : va_dummy:unit -> Tot va_pbool
va_dummy: Prims.unit -> Vale.PPC64LE.Decls.va_pbool