val lemma_compose_free_stack64 (start:int) (inter:int) (finish:int) (h:vale_stack) : Lemma
  (requires start <= inter /\ inter <= finish)
  (ensures free_stack64 inter finish (free_stack64 start inter h) == free_stack64 start finish h)
  [SMTPat (free_stack64 inter finish (free_stack64 start inter h))]
let lemma_compose_free_stack64 start inter finish h =
  let BS.Machine_stack _ mem = h in
  let domain = Map.domain mem in
  let map_restr = Map.restrict (Vale.Lib.Set.remove_between domain start inter) mem in
  let restrict = Map.domain map_restr in
  let BS.Machine_stack _ mem1 = free_stack64 inter finish (free_stack64 start inter h) in
  let BS.Machine_stack _ mem2 = free_stack64 start finish h in
  let aux (i:int) : Lemma (Map.contains mem1 i = Map.contains mem2 i /\ Map.sel mem1 i = Map.sel mem2 i)
    = Vale.Lib.Set.remove_between_reveal domain start inter i;
      Vale.Lib.Set.remove_between_reveal restrict inter finish i;
      Vale.Lib.Set.remove_between_reveal domain start finish i;
      Vale.Lib.Set.lemma_sel_restrict (Vale.Lib.Set.remove_between domain start inter) mem i;
      Vale.Lib.Set.lemma_sel_restrict (Vale.Lib.Set.remove_between restrict inter finish) map_restr i;
      Vale.Lib.Set.lemma_sel_restrict (Vale.Lib.Set.remove_between domain start finish) mem i
  in Classical.forall_intro aux;
  assert (Map.equal mem1 mem2)
val lemma_compose_free_stack64 (start:int) (inter:int) (finish:int) (h:vale_stack) : Lemma
  (requires start <= inter /\ inter <= finish)
  (ensures free_stack64 inter finish (free_stack64 start inter h) == free_stack64 start finish h)
  [SMTPat (free_stack64 inter finish (free_stack64 start inter h))]
let lemma_compose_free_stack64 start inter finish h =
let BS.Machine_stack _ mem = h in
let domain = Map.domain mem in
let map_restr = Map.restrict (Vale.Lib.Set.remove_between domain start inter) mem in
let restrict = Map.domain map_restr in
let BS.Machine_stack _ mem1 = free_stack64 inter finish (free_stack64 start inter h) in
let BS.Machine_stack _ mem2 = free_stack64 start finish h in
let aux (i: int)
    : Lemma (Map.contains mem1 i = Map.contains mem2 i /\ Map.sel mem1 i = Map.sel mem2 i) =
  Vale.Lib.Set.remove_between_reveal domain start inter i;
  Vale.Lib.Set.remove_between_reveal restrict inter finish i;
  Vale.Lib.Set.remove_between_reveal domain start finish i;
  Vale.Lib.Set.lemma_sel_restrict (Vale.Lib.Set.remove_between domain start inter) mem i;
  Vale.Lib.Set.lemma_sel_restrict (Vale.Lib.Set.remove_between restrict inter finish) map_restr i;
  Vale.Lib.Set.lemma_sel_restrict (Vale.Lib.Set.remove_between domain start finish) mem i
in
Classical.forall_intro aux;
assert (Map.equal mem1 mem2)
Vale.X64.Stack_i.fst.checked
Vale.X64.Machine_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.X64.Stack_i.fst
Prims.int Vale.X64.Stack_i.vale_stack Vale.Def.Types_s.nat64 Prims.b2t Prims.op_GreaterThanOrEqual FStar.Map.t Vale.Def.Types_s.nat8 Prims._assert FStar.Map.equal Prims.unit FStar.Classical.forall_intro Prims.l_and Prims.op_Equality Prims.bool FStar.Map.contains FStar.Map.sel Prims.l_True Prims.squash Vale.Def.Words_s.nat8 Prims.Nil FStar.Pervasives.pattern Vale.Lib.Set.lemma_sel_restrict Vale.Lib.Set.remove_between Vale.Lib.Set.remove_between_reveal Vale.X64.Stack_i.free_stack64 FStar.Set.set FStar.Map.domain FStar.Map.restrict
module Vale.X64.Stack_i
open FStar.Mul

module BS = Vale.X64.Machine_Semantics_s
open Vale.Arch.MachineHeap
let vale_stack = BS.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 init_rsp h = h.BS.initial_rsp

(* 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 BS.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 ()
#pop-options

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

let lemma_frame_store_load_stack64 ptr v h i =
  let BS.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 BS.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 ()
val lemma_compose_free_stack64 (start:int) (inter:int) (finish:int) (h:vale_stack) : Lemma
  (requires start <= inter /\ inter <= finish)
  (ensures free_stack64 inter finish (free_stack64 start inter h) == free_stack64 start finish h)
  [SMTPat (free_stack64 inter finish (free_stack64 start inter h))]
start: Prims.int -> inter: Prims.int -> finish: Prims.int -> h: Vale.X64.Stack_i.vale_stack
  -> FStar.Pervasives.Lemma (requires start <= inter /\ inter <= finish)
      (ensures
        Vale.X64.Stack_i.free_stack64 inter finish (Vale.X64.Stack_i.free_stack64 start inter h) ==
        Vale.X64.Stack_i.free_stack64 start finish h)
      [
        SMTPat (Vale.X64.Stack_i.free_stack64 inter
              finish
              (Vale.X64.Stack_i.free_stack64 start inter h))
      ]