val lemma_load_buffer_read128 (h:vale_heap) (b:buffer128) (i:int) : Lemma
  (requires valid_buffer_read h b i)
  (ensures buffer_read b i h == load_mem128 (buffer_addr b h + 16 * i) h)
  [SMTPat (buffer_read b i h)]
let lemma_load_buffer_read128 h b i =
  lemma_load_mem128 b i h
val lemma_load_buffer_read128 (h:vale_heap) (b:buffer128) (i:int) : Lemma
  (requires valid_buffer_read h b i)
  (ensures buffer_read b i h == load_mem128 (buffer_addr b h + 16 * i) h)
  [SMTPat (buffer_read b i h)]
let lemma_load_buffer_read128 h b i =
lemma_load_mem128 b i 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_heap Vale.PPC64LE.Memory.buffer128 Prims.int Vale.PPC64LE.Memory.lemma_load_mem128 Prims.unit
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;
  ()

let lemma_valid_mem_addr128 h ptr =
  bytes_valid128 ptr (get_vale_heap h);
  lemma_heap_get_heap h;
  ()

let lemma_load_mem_get64 h ptr =
  equiv_load_mem64 ptr (get_vale_heap h);
  lemma_heap_get_heap h;
  ()

let lemma_load_mem_get128 h ptr =
  equiv_load_mem128 ptr (get_vale_heap h);
  lemma_heap_get_heap h;
  ()

let lemma_load_buffer_read64 h b i =
  lemma_load_mem64 b i h
val lemma_load_buffer_read128 (h:vale_heap) (b:buffer128) (i:int) : Lemma
  (requires valid_buffer_read h b i)
  (ensures buffer_read b i h == load_mem128 (buffer_addr b h + 16 * i) h)
  [SMTPat (buffer_read b i h)]
h: Vale.PPC64LE.Memory.vale_heap -> b: Vale.PPC64LE.Memory.buffer128 -> i: Prims.int
  -> FStar.Pervasives.Lemma (requires Vale.PPC64LE.Memory.valid_buffer_read h b i)
      (ensures
        Vale.PPC64LE.Memory.buffer_read b i h ==
        Vale.PPC64LE.Memory.load_mem128 (Vale.PPC64LE.Memory.buffer_addr b h + 16 * i) h)
      [SMTPat (Vale.PPC64LE.Memory.buffer_read b i h)]