val lemma_valid_mem_addr128 (h:vale_full_heap) (ptr:int) : Lemma
  (requires valid_mem128 ptr (get_vale_heap h))
  (ensures S.valid_addr128 ptr (heap_get (coerce h)))
  [SMTPat (valid_mem128 ptr (get_vale_heap h))]
let lemma_valid_mem_addr128 h ptr =
  bytes_valid128 ptr (get_vale_heap h);
  lemma_heap_get_heap h;
  ()
val lemma_valid_mem_addr128 (h:vale_full_heap) (ptr:int) : Lemma
  (requires valid_mem128 ptr (get_vale_heap h))
  (ensures S.valid_addr128 ptr (heap_get (coerce h)))
  [SMTPat (valid_mem128 ptr (get_vale_heap h))]
let lemma_valid_mem_addr128 h ptr =
bytes_valid128 ptr (get_vale_heap h);
lemma_heap_get_heap h;
()
Vale.PPC64LE.StateLemmas.fst.checked
Vale.PPC64LE.Memory_Sems.fsti.checked Vale.PPC64LE.Memory.fsti.checked prims.fst.checked FStar.Pervasives.fsti.checked
Vale.PPC64LE.StateLemmas.fst
Vale.PPC64LE.Memory.vale_full_heap Prims.int Prims.unit Vale.PPC64LE.Memory_Sems.lemma_heap_get_heap Vale.PPC64LE.Memory_Sems.bytes_valid128 Vale.PPC64LE.Memory.get_vale_heap
module Vale.PPC64LE.StateLemmas
open Vale.PPC64LE.Memory_Sems
open Vale.PPC64LE.Memory

#reset-options "--initial_fuel 2 --max_fuel 2"

let lemma_to_eval_reg s r = ()
let lemma_to_eval_vec s v = ()
let lemma_to_eval_maddr s m = ()
let lemma_to_eval_cmp_opr s o = ()
let lemma_to_valid_maddr64 s m = ()

let lemma_valid_mem_addr64 h ptr =
  bytes_valid64 ptr (get_vale_heap h);
  lemma_heap_get_heap h;
  ()
val lemma_valid_mem_addr128 (h:vale_full_heap) (ptr:int) : Lemma
  (requires valid_mem128 ptr (get_vale_heap h))
  (ensures S.valid_addr128 ptr (heap_get (coerce h)))
  [SMTPat (valid_mem128 ptr (get_vale_heap h))]
h: Vale.PPC64LE.Memory.vale_full_heap -> ptr: Prims.int
  -> FStar.Pervasives.Lemma
      (requires Vale.PPC64LE.Memory.valid_mem128 ptr (Vale.PPC64LE.Memory.get_vale_heap h))
      (ensures
        Vale.Arch.MachineHeap_s.valid_addr128 ptr
          (Vale.Arch.Heap.heap_get (Vale.PPC64LE.Memory_Sems.coerce h)))
      [SMTPat (Vale.PPC64LE.Memory.valid_mem128 ptr (Vale.PPC64LE.Memory.get_vale_heap h))]