val va_wpProof_AddLa : dst:va_operand_reg_opr -> src1:va_operand_reg_opr -> src2:simm16 ->
  va_s0:va_state -> va_k:(va_state -> unit -> Type0)
  -> Ghost (va_state & va_fuel & unit)
  (requires (va_t_require va_s0 /\ va_wp_AddLa dst src1 src2 va_s0 va_k))
  (ensures (fun (va_sM, va_f0, va_g) -> va_t_ensure (va_code_AddLa dst src1 src2) ([va_mod_reg_opr
    dst]) va_s0 va_k ((va_sM, va_f0, va_g))))
let va_wpProof_AddLa dst src1 src2 va_s0 va_k =
  let (va_sM, va_f0) = va_lemma_AddLa (va_code_AddLa dst src1 src2) va_s0 dst src1 src2 in
  va_lemma_upd_update va_sM;
  assert (va_state_eq va_sM (va_update_ok va_sM (va_update_operand_reg_opr dst va_sM va_s0)));
  va_lemma_norm_mods ([va_mod_reg_opr dst]) va_sM va_s0;
  let va_g = () in
  (va_sM, va_f0, va_g)
val va_wpProof_AddLa : dst:va_operand_reg_opr -> src1:va_operand_reg_opr -> src2:simm16 ->
  va_s0:va_state -> va_k:(va_state -> unit -> Type0)
  -> Ghost (va_state & va_fuel & unit)
  (requires (va_t_require va_s0 /\ va_wp_AddLa dst src1 src2 va_s0 va_k))
  (ensures (fun (va_sM, va_f0, va_g) -> va_t_ensure (va_code_AddLa dst src1 src2) ([va_mod_reg_opr
    dst]) va_s0 va_k ((va_sM, va_f0, va_g))))
let va_wpProof_AddLa dst src1 src2 va_s0 va_k =
let va_sM, va_f0 = va_lemma_AddLa (va_code_AddLa dst src1 src2) va_s0 dst src1 src2 in
va_lemma_upd_update va_sM;
assert (va_state_eq va_sM (va_update_ok va_sM (va_update_operand_reg_opr dst va_sM va_s0)));
va_lemma_norm_mods ([va_mod_reg_opr dst]) va_sM va_s0;
let va_g = () in
(va_sM, va_f0, va_g)
Vale.PPC64LE.InsBasic.fst.checked
Vale.PPC64LE.State.fsti.checked Vale.PPC64LE.Stack_i.fsti.checked Vale.PPC64LE.Semantics_s.fst.checked Vale.PPC64LE.Memory.fsti.checked Vale.PPC64LE.Machine_s.fst.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.InsBasic.fst
Vale.PPC64LE.Decls.va_operand_reg_opr Vale.PPC64LE.Machine_s.simm16 Vale.PPC64LE.Decls.va_state Prims.unit Vale.PPC64LE.Decls.va_fuel FStar.Pervasives.Native.Mktuple3 Vale.PPC64LE.QuickCode.va_lemma_norm_mods Prims.Cons Vale.PPC64LE.QuickCode.mod_t Vale.PPC64LE.QuickCode.va_mod_reg_opr Prims.Nil Prims._assert Vale.PPC64LE.Decls.va_state_eq Vale.PPC64LE.Decls.va_update_ok Vale.PPC64LE.Decls.va_update_operand_reg_opr Vale.PPC64LE.Decls.va_lemma_upd_update FStar.Pervasives.Native.tuple3 FStar.Pervasives.Native.tuple2 Vale.PPC64LE.Machine_s.state Vale.PPC64LE.InsBasic.va_lemma_AddLa Vale.PPC64LE.InsBasic.va_code_AddLa
module Vale.PPC64LE.InsBasic
open Vale.PPC64LE.Machine_s
open Vale.PPC64LE.State
open Vale.PPC64LE.Decls
open Vale.PPC64LE.Memory
open Vale.PPC64LE.Stack_i
friend Vale.PPC64LE.Decls
module S = Vale.PPC64LE.Semantics_s
//-- Move

[@ "opaque_to_smt"]
let va_code_Move dst src =
  (Ins (S.Move dst src))

[@ "opaque_to_smt"]
let va_codegen_success_Move dst src =
  (va_ttrue ())

[@"opaque_to_smt"]
let va_lemma_Move va_b0 va_s0 dst src =
  va_reveal_opaque (`%va_code_Move) (va_code_Move dst src);
  let (va_old_s:va_state) = va_s0 in
  va_ins_lemma (Ins (S.Move dst src)) va_s0;
  let (va_sM, va_fM) = va_eval_ins (Ins (S.Move dst src)) va_s0 in
  (va_sM, va_fM)


[@"opaque_to_smt"]
let va_wpProof_Move dst src va_s0 va_k =
  let (va_sM, va_f0) = va_lemma_Move (va_code_Move dst src) va_s0 dst src in
  va_lemma_upd_update va_sM;
  assert (va_state_eq va_sM (va_update_ok va_sM (va_update_operand_reg_opr dst va_sM va_s0)));
  va_lemma_norm_mods ([va_mod_reg_opr dst]) va_sM va_s0;
  let va_g = () in
  (va_sM, va_f0, va_g)

//--
//-- LoadImm64

[@ "opaque_to_smt"]
let va_code_LoadImm64 dst src =
  (Ins (S.LoadImm64 dst src))

[@ "opaque_to_smt"]
let va_codegen_success_LoadImm64 dst src =
  (va_ttrue ())

[@"opaque_to_smt"]
let va_lemma_LoadImm64 va_b0 va_s0 dst src =
  va_reveal_opaque (`%va_code_LoadImm64) (va_code_LoadImm64 dst src);
  let (va_old_s:va_state) = va_s0 in
  va_ins_lemma (Ins (S.LoadImm64 dst src)) va_s0;
  let (va_sM, va_fM) = va_eval_ins (Ins (S.LoadImm64 dst src)) va_s0 in
  (va_sM, va_fM)


[@"opaque_to_smt"]
let va_wpProof_LoadImm64 dst src va_s0 va_k =
  let (va_sM, va_f0) = va_lemma_LoadImm64 (va_code_LoadImm64 dst src) va_s0 dst src in
  va_lemma_upd_update va_sM;
  assert (va_state_eq va_sM (va_update_ok va_sM (va_update_operand_reg_opr dst va_sM va_s0)));
  va_lemma_norm_mods ([va_mod_reg_opr dst]) va_sM va_s0;
  let va_g = () in
  (va_sM, va_f0, va_g)

//--
//-- LoadImmShl64

[@ "opaque_to_smt"]
let va_code_LoadImmShl64 dst src =
  (Ins (S.LoadImmShl64 dst src))

[@ "opaque_to_smt"]
let va_codegen_success_LoadImmShl64 dst src =
  (va_ttrue ())

[@"opaque_to_smt"]
let va_lemma_LoadImmShl64 va_b0 va_s0 dst src =
  va_reveal_opaque (`%va_code_LoadImmShl64) (va_code_LoadImmShl64 dst src);
  let (va_old_s:va_state) = va_s0 in
  va_ins_lemma (Ins (S.LoadImmShl64 dst src)) va_s0;
  let (va_sM, va_fM) = va_eval_ins (Ins (S.LoadImmShl64 dst src)) va_s0 in
  (va_sM, va_fM)


[@"opaque_to_smt"]
let va_wpProof_LoadImmShl64 dst src va_s0 va_k =
  let (va_sM, va_f0) = va_lemma_LoadImmShl64 (va_code_LoadImmShl64 dst src) va_s0 dst src in
  va_lemma_upd_update va_sM;
  assert (va_state_eq va_sM (va_update_ok va_sM (va_update_operand_reg_opr dst va_sM va_s0)));
  va_lemma_norm_mods ([va_mod_reg_opr dst]) va_sM va_s0;
  let va_g = () in
  (va_sM, va_f0, va_g)

//--
//-- AddLa

[@ "opaque_to_smt"]
let va_code_AddLa dst src1 src2 =
  (Ins (S.AddLa dst src1 src2))

[@ "opaque_to_smt"]
let va_codegen_success_AddLa dst src1 src2 =
  (va_ttrue ())

[@"opaque_to_smt"]
let va_lemma_AddLa va_b0 va_s0 dst src1 src2 =
  va_reveal_opaque (`%va_code_AddLa) (va_code_AddLa dst src1 src2);
  let (va_old_s:va_state) = va_s0 in
  va_ins_lemma (Ins (S.AddLa dst src1 src2)) va_s0;
  let (va_sM, va_fM) = va_eval_ins (Ins (S.AddLa dst src1 src2)) va_s0 in
  (va_sM, va_fM)
val va_wpProof_AddLa : dst:va_operand_reg_opr -> src1:va_operand_reg_opr -> src2:simm16 ->
  va_s0:va_state -> va_k:(va_state -> unit -> Type0)
  -> Ghost (va_state & va_fuel & unit)
  (requires (va_t_require va_s0 /\ va_wp_AddLa dst src1 src2 va_s0 va_k))
  (ensures (fun (va_sM, va_f0, va_g) -> va_t_ensure (va_code_AddLa dst src1 src2) ([va_mod_reg_opr
    dst]) va_s0 va_k ((va_sM, va_f0, va_g))))

    dst: Vale.PPC64LE.Decls.va_operand_reg_opr ->
    src1: Vale.PPC64LE.Decls.va_operand_reg_opr ->
    src2: Vale.PPC64LE.Machine_s.simm16 ->
    va_s0: Vale.PPC64LE.Decls.va_state ->
    va_k: (_: Vale.PPC64LE.Decls.va_state -> _: Prims.unit -> Type0)
  -> Prims.Ghost ((Vale.PPC64LE.Decls.va_state * Vale.PPC64LE.Decls.va_fuel) * Prims.unit)