val va_lemma_Alloc_stack : va_b0:va_code -> va_s0:va_state -> n:nat64
  -> Ghost (va_state & va_fuel)
  (requires (va_require_total va_b0 (va_code_Alloc_stack n) va_s0 /\ va_get_ok va_s0 /\ n
    `op_Modulus` 16 == 0 /\ va_get_reg 1 va_s0 <= Vale.PPC64LE.Stack_i.init_r1 (va_get_stack va_s0)
    /\ Vale.PPC64LE.Stack_i.init_r1 (va_get_stack va_s0) - 65536 <= va_get_reg 1 va_s0 - n))
  (ensures (fun (va_sM, va_fM) -> va_ensure_total va_b0 va_s0 va_sM va_fM /\ va_get_ok va_sM /\
    va_get_reg 1 va_sM == va_get_reg 1 va_s0 - n /\ va_state_eq va_sM (va_update_reg 1 va_sM
    (va_update_ok va_sM va_s0))))
let va_lemma_Alloc_stack va_b0 va_s0 n =
  va_reveal_opaque (`%va_code_Alloc_stack) (va_code_Alloc_stack n);
  let (va_old_s:va_state) = va_s0 in
  va_ins_lemma (Ins (S.Alloc n)) va_s0;
  let (va_sM, va_fM) = va_eval_ins (Ins (S.Alloc n)) va_s0 in
  (va_sM, va_fM)
val va_lemma_Alloc_stack : va_b0:va_code -> va_s0:va_state -> n:nat64
  -> Ghost (va_state & va_fuel)
  (requires (va_require_total va_b0 (va_code_Alloc_stack n) va_s0 /\ va_get_ok va_s0 /\ n
    `op_Modulus` 16 == 0 /\ va_get_reg 1 va_s0 <= Vale.PPC64LE.Stack_i.init_r1 (va_get_stack va_s0)
    /\ Vale.PPC64LE.Stack_i.init_r1 (va_get_stack va_s0) - 65536 <= va_get_reg 1 va_s0 - n))
  (ensures (fun (va_sM, va_fM) -> va_ensure_total va_b0 va_s0 va_sM va_fM /\ va_get_ok va_sM /\
    va_get_reg 1 va_sM == va_get_reg 1 va_s0 - n /\ va_state_eq va_sM (va_update_reg 1 va_sM
    (va_update_ok va_sM va_s0))))
let va_lemma_Alloc_stack va_b0 va_s0 n =
va_reveal_opaque (`%va_code_Alloc_stack) (va_code_Alloc_stack n);
let va_old_s:va_state = va_s0 in
va_ins_lemma (Ins (S.Alloc n)) va_s0;
let va_sM, va_fM = va_eval_ins (Ins (S.Alloc n)) va_s0 in
(va_sM, va_fM)
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.Decls.va_code Vale.PPC64LE.Decls.va_state Vale.PPC64LE.Memory.nat64 Vale.PPC64LE.State.state Vale.PPC64LE.Lemmas.fuel FStar.Pervasives.Native.Mktuple2 Vale.PPC64LE.Decls.va_fuel FStar.Pervasives.Native.tuple2 Vale.PPC64LE.Machine_s.state Prims.nat Vale.PPC64LE.Decls.va_eval_ins Vale.PPC64LE.Machine_s.Ins Vale.PPC64LE.Semantics_s.ins Vale.PPC64LE.Semantics_s.ocmp Vale.PPC64LE.Semantics_s.Alloc Prims.unit Vale.PPC64LE.Decls.va_ins_lemma Vale.PPC64LE.Decls.ins Vale.PPC64LE.Decls.ocmp Vale.PPC64LE.Decls.va_reveal_opaque Vale.PPC64LE.InsStack.va_code_Alloc_stack
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"]
let va_codegen_success_Alloc_stack n =
  (va_ttrue ())

[@"opaque_to_smt"]
val va_lemma_Alloc_stack : va_b0:va_code -> va_s0:va_state -> n:nat64
  -> Ghost (va_state & va_fuel)
  (requires (va_require_total va_b0 (va_code_Alloc_stack n) va_s0 /\ va_get_ok va_s0 /\ n
    `op_Modulus` 16 == 0 /\ va_get_reg 1 va_s0 <= Vale.PPC64LE.Stack_i.init_r1 (va_get_stack va_s0)
    /\ Vale.PPC64LE.Stack_i.init_r1 (va_get_stack va_s0) - 65536 <= va_get_reg 1 va_s0 - n))
  (ensures (fun (va_sM, va_fM) -> va_ensure_total va_b0 va_s0 va_sM va_fM /\ va_get_ok va_sM /\
    va_get_reg 1 va_sM == va_get_reg 1 va_s0 - n /\ va_state_eq va_sM (va_update_reg 1 va_sM
    (va_update_ok va_sM va_s0))))

    va_b0: Vale.PPC64LE.Decls.va_code ->
    va_s0: Vale.PPC64LE.Decls.va_state ->
    n: Vale.PPC64LE.Memory.nat64
  -> Prims.Ghost (Vale.PPC64LE.Decls.va_state * Vale.PPC64LE.Decls.va_fuel)