let vale_stack = Vale.PPC64LE.Stack_i.vale_stack
let vale_stack =
Vale.PPC64LE.Stack_i.vale_stack
Vale.PPC64LE.InsBasic.fsti.checked
Vale.PPC64LE.State.fsti.checked Vale.PPC64LE.Stack_i.fsti.checked Vale.PPC64LE.QuickCode.fst.checked Vale.PPC64LE.Memory.fsti.checked Vale.PPC64LE.Machine_s.fst.checked Vale.PPC64LE.Decls.fsti.checked Vale.Arch.Types.fsti.checked prims.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked
Vale.PPC64LE.InsBasic.fsti
Vale.PPC64LE.Stack_i.vale_stack
module Vale.PPC64LE.InsBasic
open FStar.Mul
open Vale.Arch.Types
open Vale.PPC64LE.Machine_s
open Vale.PPC64LE.State
open Vale.PPC64LE.Decls
open Vale.PPC64LE.QuickCode
val vale_stack : Type0
Type0