val lemma_free_stack_same_valid128 (start:int) (finish:int) (ptr:int) (h:vale_stack) : Lemma
  (requires valid_src_stack128 ptr h /\
    (ptr >= finish \/ ptr + 16 <= start))
  (ensures valid_src_stack128 ptr (free_stack128 start finish h))
  [SMTPat (valid_src_stack128 ptr (free_stack128 start finish h))]
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)
val lemma_free_stack_same_valid128 (start:int) (finish:int) (ptr:int) (h:vale_stack) : Lemma
  (requires valid_src_stack128 ptr h /\
    (ptr >= finish \/ ptr + 16 <= start))
  (ensures valid_src_stack128 ptr (free_stack128 start finish h))
  [SMTPat (valid_src_stack128 ptr (free_stack128 start finish h))]
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)
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.Stack_i.vale_stack Vale.PPC64LE.Machine_s.nat64 Prims.b2t Prims.op_GreaterThanOrEqual FStar.Map.t Vale.PPC64LE.Machine_s.nat8 FStar.Classical.forall_intro Prims.l_and Prims.l_imp Prims.op_LessThanOrEqual Prims.op_LessThan Prims.op_Negation FStar.Set.mem Vale.Lib.Set.remove_between Prims.l_or Prims.op_Equality Prims.bool Vale.Lib.Set.remove_between_reveal FStar.Set.set FStar.Map.domain Prims.unit FStar.Pervasives.reveal_opaque Vale.Arch.MachineHeap_s.machine_heap Vale.Arch.MachineHeap_s.valid_addr128
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 ()
val lemma_free_stack_same_valid128 (start:int) (finish:int) (ptr:int) (h:vale_stack) : Lemma
  (requires valid_src_stack128 ptr h /\
    (ptr >= finish \/ ptr + 16 <= start))
  (ensures valid_src_stack128 ptr (free_stack128 start finish h))
  [SMTPat (valid_src_stack128 ptr (free_stack128 start finish h))]
start: Prims.int -> finish: Prims.int -> ptr: Prims.int -> h: Vale.PPC64LE.Stack_i.vale_stack
  -> FStar.Pervasives.Lemma
      (requires
        Vale.PPC64LE.Stack_i.valid_src_stack128 ptr h /\ (ptr >= finish \/ ptr + 16 <= start))
      (ensures
        Vale.PPC64LE.Stack_i.valid_src_stack128 ptr
          (Vale.PPC64LE.Stack_i.free_stack128 start finish h))
      [
        SMTPat (Vale.PPC64LE.Stack_i.valid_src_stack128 ptr
              (Vale.PPC64LE.Stack_i.free_stack128 start finish h))
      ]