val init_rsp (h:vale_stack) : (n:nat64{n >= 4096})
let init_rsp h = h.BS.initial_rsp
val init_rsp (h:vale_stack) : (n:nat64{n >= 4096})
let init_rsp h =
h.BS.initial_rsp
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
Vale.X64.Stack_i.vale_stack Vale.X64.Machine_Semantics_s.__proj__Machine_stack__item__initial_rsp Vale.X64.Memory.nat64 Prims.b2t Prims.op_GreaterThanOrEqual
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
val init_rsp (h:vale_stack) : (n:nat64{n >= 4096})
h: Vale.X64.Stack_i.vale_stack -> n: Vale.X64.Memory.nat64{n >= 4096}