val va_codegen_success_Store_stack64 : src:va_operand_reg_opr -> offset:int -> Tot va_pbool
let va_codegen_success_Store_stack64 src offset =
  (va_ttrue ())
val va_codegen_success_Store_stack64 : src:va_operand_reg_opr -> offset:int -> Tot va_pbool
let va_codegen_success_Store_stack64 src offset =
(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.Decls.va_operand_reg_opr Prims.int 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"]
let va_codegen_success_Alloc_stack n =
  (va_ttrue ())

[@"opaque_to_smt"]
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)


[@"opaque_to_smt"]
let va_wpProof_Alloc_stack n va_s0 va_k =
  let (va_sM, va_f0) = va_lemma_Alloc_stack (va_code_Alloc_stack n) va_s0 n in
  va_lemma_upd_update va_sM;
  assert (va_state_eq va_sM (va_update_reg 1 va_sM (va_update_ok va_sM va_s0)));
  va_lemma_norm_mods ([va_Mod_reg 1]) va_sM va_s0;
  let va_g = () in
  (va_sM, va_f0, va_g)

//--
//-- Dealloc_stack

[@ "opaque_to_smt"]
let va_code_Dealloc_stack n =
  (Ins (S.Dealloc n))

[@ "opaque_to_smt"]
let va_codegen_success_Dealloc_stack n =
  (va_ttrue ())

[@"opaque_to_smt"]
let va_lemma_Dealloc_stack va_b0 va_s0 n =
  va_reveal_opaque (`%va_code_Dealloc_stack) (va_code_Dealloc_stack n);
  let (va_old_s:va_state) = va_s0 in
  va_ins_lemma (Ins (S.Dealloc n)) va_s0;
  let (va_sM, va_fM) = va_eval_ins (Ins (S.Dealloc n)) va_s0 in
  (va_sM, va_fM)


[@"opaque_to_smt"]
let va_wpProof_Dealloc_stack n va_s0 va_k =
  let (va_sM, va_f0) = va_lemma_Dealloc_stack (va_code_Dealloc_stack n) va_s0 n in
  va_lemma_upd_update va_sM;
  assert (va_state_eq va_sM (va_update_stack va_sM (va_update_reg 1 va_sM (va_update_ok va_sM
    va_s0))));
  va_lemma_norm_mods ([va_Mod_stack; va_Mod_reg 1]) va_sM va_s0;
  let va_g = () in
  (va_sM, va_f0, va_g)

//--
//-- Store_stack128

[@ "opaque_to_smt"]
let va_code_Store_stack128 src offset =
  (Ins (S.StoreStack128 src Secret offset))

[@ "opaque_to_smt"]
let va_codegen_success_Store_stack128 src offset =
  (va_ttrue ())

[@"opaque_to_smt"]
let va_lemma_Store_stack128 va_b0 va_s0 src offset =
  va_reveal_opaque (`%va_code_Store_stack128) (va_code_Store_stack128 src offset);
  let (va_old_s:va_state) = va_s0 in
  va_ins_lemma (Ins (S.StoreStack128 src Secret offset)) va_s0;
  let (va_sM, va_fM) = va_eval_ins (Ins (S.StoreStack128 src Secret offset)) va_s0 in
  (va_sM, va_fM)


[@"opaque_to_smt"]
let va_wpProof_Store_stack128 src offset va_s0 va_k =
  let (va_sM, va_f0) = va_lemma_Store_stack128 (va_code_Store_stack128 src offset) va_s0 src offset
    in
  va_lemma_upd_update va_sM;
  assert (va_state_eq va_sM (va_update_stackTaint va_sM (va_update_stack va_sM (va_update_ok va_sM
    va_s0))));
  va_lemma_norm_mods ([va_Mod_stackTaint; va_Mod_stack]) va_sM va_s0;
  let va_g = () in
  (va_sM, va_f0, va_g)

//--
//-- Load_stack128

[@ "opaque_to_smt"]
let va_code_Load_stack128 dst offset =
  (Ins (S.LoadStack128 dst Secret offset))

[@ "opaque_to_smt"]
let va_codegen_success_Load_stack128 dst offset =
  (va_ttrue ())

[@"opaque_to_smt"]
let va_lemma_Load_stack128 va_b0 va_s0 dst offset =
  va_reveal_opaque (`%va_code_Load_stack128) (va_code_Load_stack128 dst offset);
  let (va_old_s:va_state) = va_s0 in
  va_ins_lemma (Ins (S.LoadStack128 dst Secret offset)) va_s0;
  let (va_sM, va_fM) = va_eval_ins (Ins (S.LoadStack128 dst Secret offset)) va_s0 in
  Vale.PPC64LE.Stack_i.lemma_valid_taint_stack128 (va_get_reg 1 va_old_s + offset) Secret
    (va_get_stackTaint va_old_s);
  (va_sM, va_fM)


[@"opaque_to_smt"]
let va_wpProof_Load_stack128 dst offset va_s0 va_k =
  let (va_sM, va_f0) = va_lemma_Load_stack128 (va_code_Load_stack128 dst offset) va_s0 dst offset in
  va_lemma_upd_update va_sM;
  assert (va_state_eq va_sM (va_update_ok va_sM (va_update_operand_vec_opr dst va_sM va_s0)));
  va_lemma_norm_mods ([va_mod_vec_opr dst]) va_sM va_s0;
  let va_g = () in
  (va_sM, va_f0, va_g)

//--
//-- Store_stack64

[@ "opaque_to_smt"]
let va_code_Store_stack64 src offset =
  (Ins (S.StoreStack64 src Secret offset))

[@ "opaque_to_smt"]
val va_codegen_success_Store_stack64 : src:va_operand_reg_opr -> offset:int -> Tot va_pbool
src: Vale.PPC64LE.Decls.va_operand_reg_opr -> offset: Prims.int -> Vale.PPC64LE.Decls.va_pbool