let get_heap_val64_reveal = opaque_revealer (`%get_heap_val64) get_heap_val64 get_heap_val64_def
let get_heap_val64_reveal =
opaque_revealer (`%get_heap_val64) get_heap_val64 get_heap_val64_def
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
Vale.Def.Opaque_s.opaque_revealer Prims.int Vale.Arch.MachineHeap_s.machine_heap Vale.Def.Types_s.nat64 Vale.Arch.MachineHeap_s.get_heap_val64 Vale.Arch.MachineHeap_s.get_heap_val64_def
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)

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])
[@"opaque_to_smt"] let get_heap_val32 = opaque_make get_heap_val32_def
irreducible let get_heap_val32_reveal = opaque_revealer (`%get_heap_val32) get_heap_val32 get_heap_val32_def

let get_heap_val64_def (ptr:int) (mem:machine_heap) : nat64 =
  two_to_nat 32
  (Mktwo
    (four_to_nat 8 (Mkfour mem.[ptr] mem.[ptr + 1] mem.[ptr + 2] mem.[ptr + 3]))
    (four_to_nat 8 (Mkfour mem.[ptr + 4] mem.[ptr + 5] mem.[ptr + 6] mem.[ptr + 7]))
  )
val get_heap_val64_reveal : _: Prims.unit
  -> FStar.Pervasives.Lemma
    (ensures Vale.Arch.MachineHeap_s.get_heap_val64 == Vale.Arch.MachineHeap_s.get_heap_val64_def)
_: Prims.unit
  -> FStar.Pervasives.Lemma
    (ensures Vale.Arch.MachineHeap_s.get_heap_val64 == Vale.Arch.MachineHeap_s.get_heap_val64_def)