val load_stack64 (ptr:int) (h:vale_stack) : GTot nat64
let load_stack64 i st = BS.eval_stack i st
val load_stack64 (ptr:int) (h:vale_stack) : GTot nat64
let load_stack64 i st =
BS.eval_stack i st
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.Semantics_s.eval_stack Vale.PPC64LE.Memory.nat64
module Vale.PPC64LE.Stack_i
open FStar.Mul

module BS = Vale.PPC64LE.Semantics_s
open Vale.Arch.MachineHeap
let vale_stack = machine_stack
val load_stack64 (ptr:int) (h:vale_stack) : GTot nat64
ptr: Prims.int -> h: Vale.PPC64LE.Stack_i.vale_stack -> Prims.GTot Vale.PPC64LE.Memory.nat64