val get_heap_val32_def (ptr: int) (mem: machine_heap) : nat32
let get_heap_val32_def (ptr:int) (mem:machine_heap) : nat32 =
  four_to_nat 8
  (Mkfour
    mem.[ptr]
    mem.[ptr + 1]
    mem.[ptr + 2]
    mem.[ptr + 3])
val get_heap_val32_def (ptr: int) (mem: machine_heap) : nat32
let get_heap_val32_def (ptr: int) (mem: machine_heap) : nat32 =
four_to_nat 8 (Mkfour mem.[ ptr ] mem.[ ptr + 1 ] mem.[ ptr + 2 ] mem.[ ptr + 3 ])
Vale.Arch.MachineHeap_s.fst.checked
Vale.Def.Words_s.fsti.checked Vale.Def.Words.Two_s.fsti.checked Vale.Def.Words.Four_s.fsti.checked Vale.Def.Types_s.fst.checked Vale.Def.Prop_s.fst.checked Vale.Def.Opaque_s.fsti.checked prims.fst.checked FStar.Set.fsti.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.Map.fsti.checked
Vale.Arch.MachineHeap_s.fst
Prims.int Vale.Arch.MachineHeap_s.machine_heap Vale.Def.Words.Four_s.four_to_nat Vale.Def.Words_s.Mkfour Vale.Def.Words_s.natN Prims.pow2 Vale.Arch.MachineHeap_s.op_String_Access Vale.Def.Types_s.nat8 Prims.op_Addition Vale.Def.Types_s.nat32
module Vale.Arch.MachineHeap_s

open FStar.Mul
open Vale.Def.Prop_s
open Vale.Def.Opaque_s
open Vale.Def.Words_s
open Vale.Def.Words.Two_s
open Vale.Def.Words.Four_s
open Vale.Def.Types_s

unfold let (.[]) = Map.sel
unfold let (.[]<-) = Map.upd

let machine_heap = Map.t int nat8

let is_machine_heap_update (mh mh':machine_heap) =
  Set.equal (Map.domain mh) (Map.domain mh') /\
  (forall (i:int).{:pattern Map.sel mh i \/ Map.sel mh' i}
    not (Map.contains mh i) ==> Map.sel mh i == Map.sel mh' i)
val get_heap_val32_def (ptr: int) (mem: machine_heap) : nat32
ptr: Prims.int -> mem: Vale.Arch.MachineHeap_s.machine_heap -> Vale.Def.Types_s.nat32