val same_mem_get_heap_val32 (ptr:int) (mem1 mem2:machine_heap) : Lemma
  (requires get_heap_val32 ptr mem1 == get_heap_val32 ptr mem2)
  (ensures forall i.{:pattern mem1.[i] \/ mem2.[i]} i >= ptr /\ i < ptr + 4 ==> mem1.[i] == mem2.[i])
val same_mem_get_heap_val32 (ptr:int) (mem1 mem2:machine_heap) : Lemma
  (requires get_heap_val32 ptr mem1 == get_heap_val32 ptr mem2)
  (ensures forall i.{:pattern mem1.[i] \/ mem2.[i]} i >= ptr /\ i < ptr + 4 ==> mem1.[i] == mem2.[i])
let same_mem_get_heap_val32 ptr mem1 mem2 =
  get_heap_val32_reveal ();
  four_to_nat_8_injective ()
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 ()

let frame_update_heap64 ptr v mem =
  get_heap_val64_reveal ();
  update_heap64_reveal ()

let correct_update_get64 ptr v mem =
  get_heap_val64_reveal ();
  update_heap64_reveal ()

let same_domain_update64 ptr v mem =
  reveal_opaque (`%valid_addr64) valid_addr64;
  update_heap64_reveal ();
  let mem2 = update_heap64 ptr v mem in
  assert (Set.equal (Map.domain mem) (Map.domain mem2))
/
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 ->
    mem1: Vale.Arch.MachineHeap_s.machine_heap ->
    mem2: Vale.Arch.MachineHeap_s.machine_heap
  -> FStar.Pervasives.Lemma
      (requires
        Vale.Arch.MachineHeap_s.get_heap_val32 ptr mem1 ==
        Vale.Arch.MachineHeap_s.get_heap_val32 ptr mem2)
      (ensures
        forall (i: Prims.int). {:pattern mem1.[ i ]\/mem2.[ i ]}
          i >= ptr /\ i < ptr + 4 ==> mem1.[ i ] == mem2.[ i ])
Prims.int Vale.Arch.MachineHeap_s.machine_heap Vale.Def.Words.Seq.four_to_nat_8_injective Prims.unit Vale.Arch.MachineHeap_s.get_heap_val32_reveal
let same_mem_get_heap_val32 ptr mem1 mem2 =
  
get_heap_val32_reveal ();
four_to_nat_8_injective ()