val frame_update_heap64 (ptr:int) (v:nat64) (mem:machine_heap) : Lemma (
  let new_mem = update_heap64 ptr v mem in
  forall j.{:pattern mem.[j] \/ new_mem.[j]} j < ptr \/ j >= ptr + 8 ==>
    mem.[j] == new_mem.[j])
val frame_update_heap64 (ptr:int) (v:nat64) (mem:machine_heap) : Lemma (
  let new_mem = update_heap64 ptr v mem in
  forall j.{:pattern mem.[j] \/ new_mem.[j]} j < ptr \/ j >= ptr + 8 ==>
    mem.[j] == new_mem.[j])
let frame_update_heap64 ptr v mem =
  get_heap_val64_reveal ();
  update_heap64_reveal ()
module Vale.Arch.MachineHeap
open FStar.Mul
open Vale.Def.Opaque_s
open Vale.Def.Words_s
open Vale.Def.Words.Two_s
open Vale.Def.Words.Two
open Vale.Def.Words.Four_s
open Vale.Def.Words.Seq_s
open Vale.Def.Words.Seq
open Vale.Def.Types_s
open Vale.Arch.Types

let same_mem_get_heap_val64 ptr mem1 mem2 =
  get_heap_val64_reveal ();
  four_to_nat_8_injective ();
  two_to_nat_32_injective ()
/
Vale.Def.Words_s.fsti.checked Vale.Def.Words.Two_s.fsti.checked Vale.Def.Words.Two.fsti.checked Vale.Def.Words.Seq_s.fsti.checked Vale.Def.Words.Seq.fsti.checked Vale.Def.Words.Four_s.fsti.checked Vale.Def.Types_s.fst.checked Vale.Def.Opaque_s.fsti.checked Vale.Arch.Types.fsti.checked prims.fst.checked FStar.Set.fsti.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.Map.fsti.checked
Vale.Arch.MachineHeap.fst
ptr: Prims.int -> v: Vale.Def.Types_s.nat64 -> mem: Vale.Arch.MachineHeap_s.machine_heap
  -> FStar.Pervasives.Lemma
    (ensures
      (let new_mem = Vale.Arch.MachineHeap_s.update_heap64 ptr v mem in
        forall (j: Prims.int). {:pattern mem.[ j ]\/new_mem.[ j ]}
          j < ptr \/ j >= ptr + 8 ==> mem.[ j ] == new_mem.[ j ]))
Prims.int Vale.Def.Types_s.nat64 Vale.Arch.MachineHeap_s.machine_heap Vale.Arch.MachineHeap_s.update_heap64_reveal Prims.unit Vale.Arch.MachineHeap_s.get_heap_val64_reveal
let frame_update_heap64 ptr v mem =
  
get_heap_val64_reveal ();
update_heap64_reveal ()