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

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))

let frame_update_heap128 ptr v mem =
  update_heap128_reveal ();
  let mem1 = update_heap32 ptr v.lo0 mem in
  frame_update_heap32 ptr v.lo0 mem;
  let mem2 = update_heap32 (ptr+4) v.lo1 mem1 in
  frame_update_heap32 (ptr+4) v.lo1 mem1;
  let mem3 = update_heap32 (ptr+8) v.hi2 mem2 in
  frame_update_heap32 (ptr+8) v.hi2 mem2;
  let mem4 = update_heap32 (ptr+12) v.hi3 mem3 in
  frame_update_heap32 (ptr+12) v.hi3 mem3

let correct_update_get32 (ptr:int) (v:nat32) (mem:machine_heap) : Lemma
  (get_heap_val32 ptr (update_heap32 ptr v mem) == v) =
  get_heap_val32_reveal ();
  update_heap32_reveal ()

#reset-options "--z3rlimit 30 --using_facts_from 'Prims Vale.Def.Opaque_s Vale.Arch.MachineHeap_s Vale.Def.Words_s Vale.Def.Types_s'"

let correct_update_get128 ptr v mem =
  update_heap128_reveal ();
  get_heap_val32_reveal ();
  update_heap32_reveal ();
  get_heap_val128_reveal ();
  let mem1 = update_heap32 ptr v.lo0 mem in
  frame_update_heap32 ptr v.lo0 mem;
  correct_update_get32 ptr v.lo0 mem;
  let mem2 = update_heap32 (ptr+4) v.lo1 mem1 in
  frame_update_heap32 (ptr+4) v.lo1 mem1;
  correct_update_get32 (ptr+4) v.lo1 mem1;
  let mem3 = update_heap32 (ptr+8) v.hi2 mem2 in
  frame_update_heap32 (ptr+8) v.hi2 mem2;
  correct_update_get32 (ptr+8) v.hi2 mem2;
  let mem4 = update_heap32 (ptr+12) v.hi3 mem3 in
  frame_update_heap32 (ptr+12) v.hi3 mem3;
  correct_update_get32 (ptr+12) v.hi3 mem3

#reset-options "--z3rlimit 10 --max_fuel 2 --initial_fuel 2 --max_ifuel 1 --initial_ifuel 1"

let same_domain_update128 ptr v mem =
  let mem1 = update_heap32 ptr v.lo0 mem in
  let mem2 = update_heap32 (ptr + 4) v.lo1 mem1 in
  let mem3 = update_heap32 (ptr + 8) v.hi2 mem2 in
  reveal_opaque (`%valid_addr128) valid_addr128;
  update_heap128_reveal ();
  same_domain_update32 ptr v.lo0 mem;
  same_domain_update32 (ptr+4) v.lo1 mem1;
  same_domain_update32 (ptr+8) v.hi2 mem2;
  same_domain_update32 (ptr+12) v.hi3 mem3;
  let memf = update_heap128 ptr v mem in
  assert (Set.equal (Map.domain mem) (Map.domain memf))
/
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_val128 ptr mem1 ==
        Vale.Arch.MachineHeap_s.get_heap_val128 ptr mem2)
      (ensures
        forall (i: Prims.int). {:pattern mem1.[ i ]\/mem2.[ i ]}
          i >= ptr /\ i < ptr + 16 ==> mem1.[ i ] == mem2.[ i ])
Prims.int Vale.Arch.MachineHeap_s.machine_heap Vale.Arch.MachineHeap.same_mem_get_heap_val32 Prims.op_Addition Prims.unit Vale.Arch.MachineHeap_s.get_heap_val128_reveal
let same_mem_get_heap_val128 ptr mem1 mem2 =
  
get_heap_val128_reveal ();
same_mem_get_heap_val32 ptr mem1 mem2;
same_mem_get_heap_val32 (ptr + 4) mem1 mem2;
same_mem_get_heap_val32 (ptr + 8) mem1 mem2;
same_mem_get_heap_val32 (ptr + 12) mem1 mem2