val free_stack64 (start:int) (finish:int) (h:vale_stack) : GTot vale_stack
let free_stack64 start finish h = BS.free_stack' start finish h
val free_stack64 (start:int) (finish:int) (h:vale_stack) : GTot vale_stack
let free_stack64 start finish h =
BS.free_stack' start finish h
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.free_stack'
module Vale.PPC64LE.Stack_i
open FStar.Mul

module BS = Vale.PPC64LE.Semantics_s
open Vale.Arch.MachineHeap
let vale_stack = machine_stack

let valid_src_stack64 i st = BS.valid_src_stack64 i st
let load_stack64 i st = BS.eval_stack i st
val free_stack64 (start:int) (finish:int) (h:vale_stack) : GTot vale_stack
start: Prims.int -> finish: Prims.int -> h: Vale.PPC64LE.Stack_i.vale_stack
  -> Prims.GTot Vale.PPC64LE.Stack_i.vale_stack