val va_codegen_success_Alloc_stack : n:nat64 -> Tot va_pbool
let va_codegen_success_Alloc_stack n =
  (va_ttrue ())
val va_codegen_success_Alloc_stack : n:nat64 -> Tot va_pbool
let va_codegen_success_Alloc_stack n =
(va_ttrue ())
Vale.PPC64LE.InsStack.fst.checked
Vale.PPC64LE.StateLemmas.fsti.checked Vale.PPC64LE.State.fsti.checked Vale.PPC64LE.Stack_Sems.fst.checked Vale.PPC64LE.Stack_Sems.fst.checked Vale.PPC64LE.Stack_i.fst.checked Vale.PPC64LE.Stack_i.fst.checked Vale.PPC64LE.Semantics_s.fst.checked Vale.PPC64LE.Print_s.fst.checked Vale.PPC64LE.Memory.fsti.checked Vale.PPC64LE.Machine_s.fst.checked Vale.PPC64LE.InsVector.fsti.checked Vale.PPC64LE.InsBasic.fsti.checked Vale.PPC64LE.Decls.fst.checked Vale.PPC64LE.Decls.fst.checked prims.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked
Vale.PPC64LE.InsStack.fst
Vale.PPC64LE.Memory.nat64 Vale.PPC64LE.Decls.va_ttrue Vale.PPC64LE.Decls.va_pbool
module Vale.PPC64LE.InsStack
open Vale.PPC64LE.Machine_s
open Vale.PPC64LE.Memory
open Vale.PPC64LE.Stack_i
open Vale.PPC64LE.State
open Vale.PPC64LE.StateLemmas
open Vale.PPC64LE.Decls
open Vale.PPC64LE.InsBasic
open Vale.PPC64LE.InsVector
open Vale.PPC64LE.Stack_Sems
module S = Vale.PPC64LE.Semantics_s
module P = Vale.PPC64LE.Print_s

friend Vale.PPC64LE.Decls
friend Vale.PPC64LE.Stack_i
friend Vale.PPC64LE.Stack_Sems
#reset-options "--initial_fuel 2 --max_fuel 4 --max_ifuel 2 --z3rlimit 200"
//-- Alloc_stack

[@ "opaque_to_smt"]
let va_code_Alloc_stack n =
  (Ins (S.Alloc n))

[@ "opaque_to_smt"]
val va_codegen_success_Alloc_stack : n:nat64 -> Tot va_pbool
n: Vale.PPC64LE.Memory.nat64 -> Vale.PPC64LE.Decls.va_pbool