val lemma_store_new_valid64 (ptr:int) (v:nat64) (h:vale_stack) : Lemma
  (valid_src_stack64 ptr (store_stack64 ptr v h))
  [SMTPat (valid_src_stack64 ptr (store_stack64 ptr v h))]
let lemma_store_new_valid64 ptr v h =
  reveal_opaque (`%BS.valid_addr64) BS.valid_addr64;
  BS.update_heap64_reveal ()
val lemma_store_new_valid64 (ptr:int) (v:nat64) (h:vale_stack) : Lemma
  (valid_src_stack64 ptr (store_stack64 ptr v h))
  [SMTPat (valid_src_stack64 ptr (store_stack64 ptr v h))]
let lemma_store_new_valid64 ptr v h =
reveal_opaque (`%BS.valid_addr64) BS.valid_addr64;
BS.update_heap64_reveal ()
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.Memory.nat64 Vale.X64.Stack_i.vale_stack Vale.Arch.MachineHeap_s.update_heap64_reveal Prims.unit FStar.Pervasives.reveal_opaque Vale.Arch.MachineHeap_s.machine_heap Prims.bool Vale.Arch.MachineHeap_s.valid_addr64
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)
val lemma_store_new_valid64 (ptr:int) (v:nat64) (h:vale_stack) : Lemma
  (valid_src_stack64 ptr (store_stack64 ptr v h))
  [SMTPat (valid_src_stack64 ptr (store_stack64 ptr v h))]
ptr: Prims.int -> v: Vale.X64.Memory.nat64 -> h: Vale.X64.Stack_i.vale_stack
  -> FStar.Pervasives.Lemma
      (ensures Vale.X64.Stack_i.valid_src_stack64 ptr (Vale.X64.Stack_i.store_stack64 ptr v h))
      [SMTPat (Vale.X64.Stack_i.valid_src_stack64 ptr (Vale.X64.Stack_i.store_stack64 ptr v h))]