val lemma_frame_store_load_stack128 (ptr:int) (v:quad32) (h:vale_stack) (i:int) : Lemma
  (requires valid_src_stack128 i h /\
    (i >= ptr + 16 \/ i + 16 <= ptr))
  (ensures (load_stack128 i (store_stack128 ptr v h) == load_stack128 i h))
  [SMTPat (load_stack128 i (store_stack128 ptr v h))]
let lemma_frame_store_load_stack128 ptr v h i =
  let Machine_stack _ mem = h in
  frame_update_heap128 ptr v mem;
  BS.get_heap_val32_reveal ();
  BS.get_heap_val128_reveal ()
val lemma_frame_store_load_stack128 (ptr:int) (v:quad32) (h:vale_stack) (i:int) : Lemma
  (requires valid_src_stack128 i h /\
    (i >= ptr + 16 \/ i + 16 <= ptr))
  (ensures (load_stack128 i (store_stack128 ptr v h) == load_stack128 i h))
  [SMTPat (load_stack128 i (store_stack128 ptr v h))]
let lemma_frame_store_load_stack128 ptr v h i =
let Machine_stack _ mem = h in
frame_update_heap128 ptr v mem;
BS.get_heap_val32_reveal ();
BS.get_heap_val128_reveal ()
Vale.PPC64LE.Stack_i.fst.checked
Vale.PPC64LE.Semantics_s.fst.checked Vale.Lib.Set.fsti.checked Vale.Arch.MachineHeap.fsti.checked prims.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.Map.fsti.checked FStar.Classical.fsti.checked
Vale.PPC64LE.Stack_i.fst
Prims.int Vale.PPC64LE.Memory.quad32 Vale.PPC64LE.Stack_i.vale_stack Vale.PPC64LE.Machine_s.nat64 Prims.b2t Prims.op_GreaterThanOrEqual FStar.Map.t Vale.PPC64LE.Machine_s.nat8 Vale.Arch.MachineHeap_s.get_heap_val128_reveal Prims.unit Vale.Arch.MachineHeap_s.get_heap_val32_reveal Vale.Arch.MachineHeap.frame_update_heap128
module Vale.PPC64LE.Stack_i
open FStar.Mul

module BS = Vale.PPC64LE.Semantics_s
open Vale.Arch.MachineHeap
let vale_stack = machine_stack

let valid_src_stack64 i st = BS.valid_src_stack64 i st
let load_stack64 i st = BS.eval_stack i st
let store_stack64 i v h = BS.update_stack64' i v h
let free_stack64 start finish h = BS.free_stack' start finish h

let valid_src_stack128 i st = BS.valid_src_stack128 i st
let load_stack128 i st = BS.eval_stack128 i st
let store_stack128 i v h = BS.update_stack128' i v h
let free_stack128 start finish h = BS.free_stack' start finish h

let init_r1 h = h.initial_r1

(* Lemmas *)
#push-options "--z3rlimit 40"
let lemma_store_stack_same_valid64 ptr v h i =
  reveal_opaque (`%BS.valid_addr64) BS.valid_addr64;
  BS.update_heap64_reveal ()

let lemma_free_stack_same_valid64 start finish ptr h =
  reveal_opaque (`%BS.valid_addr64) BS.valid_addr64;
  let Machine_stack _ mem = h in
  let domain = Map.domain mem in
  Classical.forall_intro (Vale.Lib.Set.remove_between_reveal domain start finish)

let lemma_store_stack_same_valid128 ptr v h i =
  reveal_opaque (`%BS.valid_addr128) BS.valid_addr128;
  BS.update_heap32_reveal ();
  BS.update_heap128_reveal ()

let lemma_free_stack_same_valid128 start finish ptr h =
  reveal_opaque (`%BS.valid_addr128) BS.valid_addr128;
  let Machine_stack _ mem = h in
  let domain = Map.domain mem in
  Classical.forall_intro (Vale.Lib.Set.remove_between_reveal domain start finish)

let lemma_store_new_valid64 ptr v h =
  reveal_opaque (`%BS.valid_addr64) BS.valid_addr64;
  BS.update_heap64_reveal ()

let lemma_store_new_valid128 ptr v h =
  reveal_opaque (`%BS.valid_addr128) BS.valid_addr128;
  BS.update_heap32_reveal ();
  BS.update_heap128_reveal ()
#pop-options

let lemma_correct_store_load_stack64 ptr v h =
  let Machine_stack _ mem = h in
  correct_update_get64 ptr v mem

let lemma_frame_store_load_stack64 ptr v h i =
  let Machine_stack _ mem = h in
  frame_update_heap64 ptr v mem;
  BS.get_heap_val64_reveal ()

let lemma_free_stack_same_load64 start finish ptr h =
  reveal_opaque (`%BS.valid_addr64) BS.valid_addr64;
  let Machine_stack _ mem = h in
  let domain = Map.domain mem in
  Classical.forall_intro (Vale.Lib.Set.remove_between_reveal domain start finish);
  BS.get_heap_val64_reveal ()

let lemma_correct_store_load_stack128 ptr v h =
  let Machine_stack _ mem = h in
  correct_update_get128 ptr v mem
val lemma_frame_store_load_stack128 (ptr:int) (v:quad32) (h:vale_stack) (i:int) : Lemma
  (requires valid_src_stack128 i h /\
    (i >= ptr + 16 \/ i + 16 <= ptr))
  (ensures (load_stack128 i (store_stack128 ptr v h) == load_stack128 i h))
  [SMTPat (load_stack128 i (store_stack128 ptr v h))]

    ptr: Prims.int ->
    v: Vale.PPC64LE.Memory.quad32 ->
    h: Vale.PPC64LE.Stack_i.vale_stack ->
    i: Prims.int
  -> FStar.Pervasives.Lemma
      (requires Vale.PPC64LE.Stack_i.valid_src_stack128 i h /\ (i >= ptr + 16 \/ i + 16 <= ptr))
      (ensures
        Vale.PPC64LE.Stack_i.load_stack128 i (Vale.PPC64LE.Stack_i.store_stack128 ptr v h) ==
        Vale.PPC64LE.Stack_i.load_stack128 i h)
      [SMTPat (Vale.PPC64LE.Stack_i.load_stack128 i (Vale.PPC64LE.Stack_i.store_stack128 ptr v h))]