val free_stack_same_load128 (start:int) (finish:int) (ptr:int) (h:S.machine_stack) : Lemma
  (requires S.valid_src_stack128 ptr h /\
    (ptr >= finish \/ ptr + 16 <= start))
  (ensures S.eval_stack128 ptr h == S.eval_stack128 ptr (S.free_stack' start finish h))
  [SMTPat (S.eval_stack128 ptr (S.free_stack' start finish h))]
let free_stack_same_load128 start finish ptr h =
  reveal_opaque (`%S.valid_addr128) S.valid_addr128;
  let S.Machine_stack _ mem = h in
  let S.Machine_stack _ mem' = S.free_stack' start finish h in
  Classical.forall_intro (Vale.Lib.Set.remove_between_reveal (Map.domain mem) start finish);
  S.get_heap_val128_reveal ();
  S.get_heap_val32_reveal ()
val free_stack_same_load128 (start:int) (finish:int) (ptr:int) (h:S.machine_stack) : Lemma
  (requires S.valid_src_stack128 ptr h /\
    (ptr >= finish \/ ptr + 16 <= start))
  (ensures S.eval_stack128 ptr h == S.eval_stack128 ptr (S.free_stack' start finish h))
  [SMTPat (S.eval_stack128 ptr (S.free_stack' start finish h))]
let free_stack_same_load128 start finish ptr h =
reveal_opaque (`%S.valid_addr128) S.valid_addr128;
let S.Machine_stack _ mem = h in
let S.Machine_stack _ mem' = S.free_stack' start finish h in
Classical.forall_intro (Vale.Lib.Set.remove_between_reveal (Map.domain mem) start finish);
S.get_heap_val128_reveal ();
S.get_heap_val32_reveal ()
Vale.X64.Stack_Sems.fst.checked
Vale.X64.Stack_i.fst.checked Vale.Lib.Set.fsti.checked prims.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.Map.fsti.checked FStar.Classical.fsti.checked
Vale.X64.Stack_Sems.fst
Prims.int Vale.X64.Machine_Semantics_s.machine_stack Vale.Def.Types_s.nat64 Prims.b2t Prims.op_GreaterThanOrEqual FStar.Map.t Vale.Def.Types_s.nat8 Vale.Arch.MachineHeap_s.get_heap_val32_reveal Prims.unit Vale.Arch.MachineHeap_s.get_heap_val128_reveal 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 FStar.Map.domain Prims.l_or Prims.op_Equality Prims.bool Vale.Lib.Set.remove_between_reveal Vale.X64.Machine_Semantics_s.free_stack' FStar.Pervasives.reveal_opaque Vale.Arch.MachineHeap_s.machine_heap Vale.Arch.MachineHeap_s.valid_addr128
module Vale.X64.Stack_Sems
open FStar.Mul

friend Vale.X64.Stack_i

let stack_to_s s = s
let stack_from_s s = s

let lemma_stack_from_to s = ()
let lemma_stack_to_from s = ()

let equiv_valid_src_stack64 ptr h = ()

let equiv_load_stack64 ptr h = ()

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

let equiv_store_stack64 ptr v h = ()

let store64_same_init_rsp ptr v h = ()

let equiv_init_rsp h = ()

let equiv_free_stack start finish h = ()

let equiv_valid_src_stack128 ptr h = ()

let equiv_load_stack128 ptr h = ()
val free_stack_same_load128 (start:int) (finish:int) (ptr:int) (h:S.machine_stack) : Lemma
  (requires S.valid_src_stack128 ptr h /\
    (ptr >= finish \/ ptr + 16 <= start))
  (ensures S.eval_stack128 ptr h == S.eval_stack128 ptr (S.free_stack' start finish h))
  [SMTPat (S.eval_stack128 ptr (S.free_stack' start finish h))]

    start: Prims.int ->
    finish: Prims.int ->
    ptr: Prims.int ->
    h: Vale.X64.Machine_Semantics_s.machine_stack
  -> FStar.Pervasives.Lemma
      (requires
        Vale.X64.Machine_Semantics_s.valid_src_stack128 ptr h /\
        (ptr >= finish \/ ptr + 16 <= start))
      (ensures
        Vale.X64.Machine_Semantics_s.eval_stack128 ptr h ==
        Vale.X64.Machine_Semantics_s.eval_stack128 ptr
          (Vale.X64.Machine_Semantics_s.free_stack' start finish h))
      [
        SMTPat (Vale.X64.Machine_Semantics_s.eval_stack128 ptr
              (Vale.X64.Machine_Semantics_s.free_stack' start finish h))
      ]