val va_code_Vand : dst:va_operand_vec_opr -> src1:va_operand_vec_opr -> src2:va_operand_vec_opr ->
  Tot va_code
let va_code_Vand dst src1 src2 =
  (Ins (S.Vand dst src1 src2))
val va_code_Vand : dst:va_operand_vec_opr -> src1:va_operand_vec_opr -> src2:va_operand_vec_opr ->
  Tot va_code
let va_code_Vand dst src1 src2 =
(Ins (S.Vand dst src1 src2))
Vale.PPC64LE.InsVector.fst.checked
Vale.SHA.PPC64LE.SHA_helpers.fsti.checked Vale.PPC64LE.State.fsti.checked Vale.PPC64LE.Semantics_s.fst.checked Vale.PPC64LE.Memory_Sems.fsti.checked Vale.PPC64LE.Machine_s.fst.checked Vale.PPC64LE.Decls.fst.checked Vale.PPC64LE.Decls.fst.checked Vale.Def.Words_s.fsti.checked Vale.Def.Types_s.fst.checked Vale.Arch.Types.fsti.checked Spec.SHA2.fsti.checked Spec.Hash.Definitions.fst.checked prims.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked
Vale.PPC64LE.InsVector.fst
Vale.PPC64LE.Decls.va_operand_vec_opr Vale.PPC64LE.Machine_s.Ins Vale.PPC64LE.Decls.ins Vale.PPC64LE.Decls.ocmp Vale.PPC64LE.Semantics_s.Vand Vale.PPC64LE.Decls.va_code
module Vale.PPC64LE.InsVector
open Vale.Def.Types_s
open Vale.PPC64LE.Machine_s
open Vale.PPC64LE.State
open Vale.PPC64LE.Decls
open Spec.Hash.Definitions
open Spec.SHA2
friend Vale.PPC64LE.Decls
module S = Vale.PPC64LE.Semantics_s
#reset-options "--initial_fuel 2 --max_fuel 4 --max_ifuel 2 --z3rlimit 50"
//-- Vmr

[@ "opaque_to_smt"]
let va_code_Vmr dst src =
  (Ins (S.Vmr dst src))

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

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


[@"opaque_to_smt"]
let va_wpProof_Vmr dst src va_s0 va_k =
  let (va_sM, va_f0) = va_lemma_Vmr (va_code_Vmr 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_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)

//--
//-- Mfvsrd

[@ "opaque_to_smt"]
let va_code_Mfvsrd dst src =
  (Ins (S.Mfvsrd dst src))

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

[@"opaque_to_smt"]
let va_lemma_Mfvsrd va_b0 va_s0 dst src =
  va_reveal_opaque (`%va_code_Mfvsrd) (va_code_Mfvsrd dst src);
  let (va_old_s:va_state) = va_s0 in
  va_ins_lemma (Ins (S.Mfvsrd dst src)) va_s0;
  let (va_sM, va_fM) = va_eval_ins (Ins (S.Mfvsrd dst src)) va_s0 in
  Vale.Arch.Types.hi64_reveal ();
  (va_sM, va_fM)


[@"opaque_to_smt"]
let va_wpProof_Mfvsrd dst src va_s0 va_k =
  let (va_sM, va_f0) = va_lemma_Mfvsrd (va_code_Mfvsrd 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)

//--
//-- Mfvsrld

[@ "opaque_to_smt"]
let va_code_Mfvsrld dst src =
  (Ins (S.Mfvsrld dst src))

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

[@"opaque_to_smt"]
let va_lemma_Mfvsrld va_b0 va_s0 dst src =
  va_reveal_opaque (`%va_code_Mfvsrld) (va_code_Mfvsrld dst src);
  let (va_old_s:va_state) = va_s0 in
  va_ins_lemma (Ins (S.Mfvsrld dst src)) va_s0;
  let (va_sM, va_fM) = va_eval_ins (Ins (S.Mfvsrld dst src)) va_s0 in
  Vale.Arch.Types.lo64_reveal ();
  (va_sM, va_fM)


[@"opaque_to_smt"]
let va_wpProof_Mfvsrld dst src va_s0 va_k =
  let (va_sM, va_f0) = va_lemma_Mfvsrld (va_code_Mfvsrld 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)

//--
//-- Mtvsrdd

[@ "opaque_to_smt"]
let va_code_Mtvsrdd dst src1 src2 =
  (Ins (S.Mtvsrdd dst src1 src2))

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

[@"opaque_to_smt"]
let va_lemma_Mtvsrdd va_b0 va_s0 dst src1 src2 =
  va_reveal_opaque (`%va_code_Mtvsrdd) (va_code_Mtvsrdd dst src1 src2);
  let (va_old_s:va_state) = va_s0 in
  va_ins_lemma (Ins (S.Mtvsrdd dst src1 src2)) va_s0;
  let (va_sM, va_fM) = va_eval_ins (Ins (S.Mtvsrdd dst src1 src2)) va_s0 in
  (va_sM, va_fM)


[@"opaque_to_smt"]
let va_wpProof_Mtvsrdd dst src1 src2 va_s0 va_k =
  let (va_sM, va_f0) = va_lemma_Mtvsrdd (va_code_Mtvsrdd 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_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)

//--
//-- Mtvsrws

[@ "opaque_to_smt"]
let va_code_Mtvsrws dst src =
  (Ins (S.Mtvsrws dst src))

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

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


[@"opaque_to_smt"]
let va_wpProof_Mtvsrws dst src va_s0 va_k =
  let (va_sM, va_f0) = va_lemma_Mtvsrws (va_code_Mtvsrws 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_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)

//--
//-- Vadduwm

[@ "opaque_to_smt"]
let va_code_Vadduwm dst src1 src2 =
  (Ins (S.Vadduwm dst src1 src2))

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

[@"opaque_to_smt"]
let va_lemma_Vadduwm va_b0 va_s0 dst src1 src2 =
  va_reveal_opaque (`%va_code_Vadduwm) (va_code_Vadduwm dst src1 src2);
  let (va_old_s:va_state) = va_s0 in
  va_ins_lemma (Ins (S.Vadduwm dst src1 src2)) va_s0;
  let (va_sM, va_fM) = va_eval_ins (Ins (S.Vadduwm dst src1 src2)) va_s0 in
  (va_sM, va_fM)


[@"opaque_to_smt"]
let va_wpProof_Vadduwm dst src1 src2 va_s0 va_k =
  let (va_sM, va_f0) = va_lemma_Vadduwm (va_code_Vadduwm 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_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)

//--
//-- Vxor

[@ "opaque_to_smt"]
let va_code_Vxor dst src1 src2 =
  (Ins (S.Vxor dst src1 src2))

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

[@"opaque_to_smt"]
let va_lemma_Vxor va_b0 va_s0 dst src1 src2 =
  va_reveal_opaque (`%va_code_Vxor) (va_code_Vxor dst src1 src2);
  let (va_old_s:va_state) = va_s0 in
  va_ins_lemma (Ins (S.Vxor dst src1 src2)) va_s0;
  let (va_sM, va_fM) = va_eval_ins (Ins (S.Vxor dst src1 src2)) va_s0 in
  (va_sM, va_fM)


[@"opaque_to_smt"]
let va_wpProof_Vxor dst src1 src2 va_s0 va_k =
  let (va_sM, va_f0) = va_lemma_Vxor (va_code_Vxor 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_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)

//--
//-- Vand

[@ "opaque_to_smt"]
val va_code_Vand : dst:va_operand_vec_opr -> src1:va_operand_vec_opr -> src2:va_operand_vec_opr ->
  Tot va_code

    dst: Vale.PPC64LE.Decls.va_operand_vec_opr ->
    src1: Vale.PPC64LE.Decls.va_operand_vec_opr ->
    src2: Vale.PPC64LE.Decls.va_operand_vec_opr
  -> Vale.PPC64LE.Decls.va_code