val update_heap32_get_heap32 (ptr:int) (mem:machine_heap) : Lemma
  (requires
    Map.contains mem ptr /\
    Map.contains mem (ptr + 1) /\
    Map.contains mem (ptr + 2) /\
    Map.contains mem (ptr + 3))
  (ensures (update_heap32 ptr (get_heap_val32 ptr mem) mem == mem))
val update_heap32_get_heap32 (ptr:int) (mem:machine_heap) : Lemma
  (requires
    Map.contains mem ptr /\
    Map.contains mem (ptr + 1) /\
    Map.contains mem (ptr + 2) /\
    Map.contains mem (ptr + 3))
  (ensures (update_heap32 ptr (get_heap_val32 ptr mem) mem == mem))
let update_heap32_get_heap32 ptr mem =
  get_heap_val32_reveal ();
  update_heap32_reveal ();
  assert (Map.equal mem (update_heap32 ptr (get_heap_val32 ptr mem) mem))
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))

let same_mem_get_heap_val32 ptr mem1 mem2 =
  get_heap_val32_reveal ();
  four_to_nat_8_injective ()

let frame_update_heap32 ptr v mem =
  get_heap_val32_reveal ();
  update_heap32_reveal ()

let same_domain_update32 ptr v mem =
  get_heap_val32_reveal ();
  update_heap32_reveal ();
  assert (Set.equal (Map.domain mem) (Map.domain (update_heap32 ptr v mem)))
/
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 -> mem: Vale.Arch.MachineHeap_s.machine_heap
  -> FStar.Pervasives.Lemma
      (requires
        FStar.Map.contains mem ptr /\ FStar.Map.contains mem (ptr + 1) /\
        FStar.Map.contains mem (ptr + 2) /\ FStar.Map.contains mem (ptr + 3))
      (ensures
        Vale.Arch.MachineHeap_s.update_heap32 ptr
          (Vale.Arch.MachineHeap_s.get_heap_val32 ptr mem)
          mem ==
        mem)
Prims.int Vale.Arch.MachineHeap_s.machine_heap Prims._assert FStar.Map.equal Vale.Def.Types_s.nat8 Vale.Arch.MachineHeap_s.update_heap32 Vale.Arch.MachineHeap_s.get_heap_val32 Prims.unit Vale.Arch.MachineHeap_s.update_heap32_reveal Vale.Arch.MachineHeap_s.get_heap_val32_reveal
let update_heap32_get_heap32 ptr mem =
  
get_heap_val32_reveal ();
update_heap32_reveal ();
assert (Map.equal mem (update_heap32 ptr (get_heap_val32 ptr mem) mem))