val va_wpProof_Vncipherlast : dst:va_operand_vec_opr -> src1:va_operand_vec_opr ->
  src2:va_operand_vec_opr -> va_s0:va_state -> va_k:(va_state -> unit -> Type0)
  -> Ghost (va_state & va_fuel & unit)
  (requires (va_t_require va_s0 /\ va_wp_Vncipherlast dst src1 src2 va_s0 va_k))
  (ensures (fun (va_sM, va_f0, va_g) -> va_t_ensure (va_code_Vncipherlast dst src1 src2)
    ([va_mod_vec_opr dst]) va_s0 va_k ((va_sM, va_f0, va_g))))
let va_wpProof_Vncipherlast dst src1 src2 va_s0 va_k =
  let (va_sM, va_f0) = va_lemma_Vncipherlast (va_code_Vncipherlast 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)
val va_wpProof_Vncipherlast : dst:va_operand_vec_opr -> src1:va_operand_vec_opr ->
  src2:va_operand_vec_opr -> va_s0:va_state -> va_k:(va_state -> unit -> Type0)
  -> Ghost (va_state & va_fuel & unit)
  (requires (va_t_require va_s0 /\ va_wp_Vncipherlast dst src1 src2 va_s0 va_k))
  (ensures (fun (va_sM, va_f0, va_g) -> va_t_ensure (va_code_Vncipherlast dst src1 src2)
    ([va_mod_vec_opr dst]) va_s0 va_k ((va_sM, va_f0, va_g))))
let va_wpProof_Vncipherlast dst src1 src2 va_s0 va_k =
let va_sM, va_f0 = va_lemma_Vncipherlast (va_code_Vncipherlast 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)
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.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_vec_opr Prims.Nil Prims._assert Vale.PPC64LE.Decls.va_state_eq Vale.PPC64LE.Decls.va_update_ok Vale.PPC64LE.Decls.va_update_operand_vec_opr Vale.PPC64LE.Decls.va_lemma_upd_update FStar.Pervasives.Native.tuple3 FStar.Pervasives.Native.tuple2 Vale.PPC64LE.Machine_s.state Vale.PPC64LE.InsVector.va_lemma_Vncipherlast Vale.PPC64LE.InsVector.va_code_Vncipherlast
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"]
let va_code_Vand dst src1 src2 =
  (Ins (S.Vand dst src1 src2))

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

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


[@"opaque_to_smt"]
let va_wpProof_Vand dst src1 src2 va_s0 va_k =
  let (va_sM, va_f0) = va_lemma_Vand (va_code_Vand 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)

//--
//-- Vslw

[@ "opaque_to_smt"]
let va_code_Vslw dst src1 src2 =
  (Ins (S.Vslw dst src1 src2))

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

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


[@"opaque_to_smt"]
let va_wpProof_Vslw dst src1 src2 va_s0 va_k =
  let (va_sM, va_f0) = va_lemma_Vslw (va_code_Vslw 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)

//--
//-- Vsrw

[@ "opaque_to_smt"]
let va_code_Vsrw dst src1 src2 =
  (Ins (S.Vsrw dst src1 src2))

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

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


[@"opaque_to_smt"]
let va_wpProof_Vsrw dst src1 src2 va_s0 va_k =
  let (va_sM, va_f0) = va_lemma_Vsrw (va_code_Vsrw 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)

//--
//-- Vsl

[@ "opaque_to_smt"]
let va_code_Vsl dst src1 src2 =
  (Ins (S.Vsl dst src1 src2))

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

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


[@"opaque_to_smt"]
let va_wpProof_Vsl dst src1 src2 va_s0 va_k =
  let (va_sM, va_f0) = va_lemma_Vsl (va_code_Vsl 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)

//--
//-- Vcmpequw

[@ "opaque_to_smt"]
let va_code_Vcmpequw dst src1 src2 =
  (Ins (S.Vcmpequw dst src1 src2))

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

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


[@"opaque_to_smt"]
let va_wpProof_Vcmpequw dst src1 src2 va_s0 va_k =
  let (va_sM, va_f0) = va_lemma_Vcmpequw (va_code_Vcmpequw 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)

//--
//-- Vsldoi

[@ "opaque_to_smt"]
let va_code_Vsldoi dst src1 src2 count =
  (Ins (S.Vsldoi dst src1 src2 count))

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

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


[@"opaque_to_smt"]
let va_wpProof_Vsldoi dst src1 src2 count va_s0 va_k =
  let (va_sM, va_f0) = va_lemma_Vsldoi (va_code_Vsldoi dst src1 src2 count) va_s0 dst src1 src2
    count 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)

//--
//-- Vmrghw

[@ "opaque_to_smt"]
let va_code_Vmrghw dst src1 src2 =
  (Ins (S.Vmrghw dst src1 src2))

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

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


[@"opaque_to_smt"]
let va_wpProof_Vmrghw dst src1 src2 va_s0 va_k =
  let (va_sM, va_f0) = va_lemma_Vmrghw (va_code_Vmrghw 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)

//--
//-- Xxmrghd

[@ "opaque_to_smt"]
let va_code_Xxmrghd dst src1 src2 =
  (Ins (S.Xxmrghd dst src1 src2))

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

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


[@"opaque_to_smt"]
let va_wpProof_Xxmrghd dst src1 src2 va_s0 va_k =
  let (va_sM, va_f0) = va_lemma_Xxmrghd (va_code_Xxmrghd 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)

//--
//-- Vsel

[@ "opaque_to_smt"]
let va_code_Vsel dst src1 src2 sel =
  (Ins (S.Vsel dst src1 src2 sel))

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

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


[@"opaque_to_smt"]
let va_wpProof_Vsel dst src1 src2 sel va_s0 va_k =
  let (va_sM, va_f0) = va_lemma_Vsel (va_code_Vsel dst src1 src2 sel) va_s0 dst src1 src2 sel 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)

//--
//-- Vspltw

[@ "opaque_to_smt"]
let va_code_Vspltw dst src uim =
  (Ins (S.Vspltw dst src uim))

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

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


[@"opaque_to_smt"]
let va_wpProof_Vspltw dst src uim va_s0 va_k =
  let (va_sM, va_f0) = va_lemma_Vspltw (va_code_Vspltw dst src uim) va_s0 dst src uim 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)

//--
//-- Vspltisw

[@ "opaque_to_smt"]
let va_code_Vspltisw dst src =
  (Ins (S.Vspltisw dst src))

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

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


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

//--
//-- Vspltisb

[@ "opaque_to_smt"]
let va_code_Vspltisb dst src =
  (Ins (S.Vspltisb dst src))

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

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


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

//--
//-- Load128_buffer

[@ "opaque_to_smt"]
let va_code_Load128_buffer h dst base offset t =
  (Ins (S.Load128 dst base offset))

[@ "opaque_to_smt"]
let va_codegen_success_Load128_buffer h dst base offset t =
  (va_ttrue ())

[@"opaque_to_smt"]
let va_lemma_Load128_buffer va_b0 va_s0 h dst base offset t b index =
  va_reveal_opaque (`%va_code_Load128_buffer) (va_code_Load128_buffer h dst base offset t);
  let (va_old_s:va_state) = va_s0 in
  va_ins_lemma (Ins (S.Load128 dst base offset)) va_s0;
  let (va_sM, va_fM) = va_eval_ins (Ins (S.Load128 dst base offset)) va_s0 in
  Vale.PPC64LE.Memory_Sems.low_lemma_load_mem128_full b index (Vale.PPC64LE.Decls.from_heap_impl
    (va_sM.ms_heap)) t h;
  (va_sM, va_fM)


[@"opaque_to_smt"]
let va_wpProof_Load128_buffer h dst base offset t b index va_s0 va_k =
  let (va_sM, va_f0) = va_lemma_Load128_buffer (va_code_Load128_buffer h dst base offset t) va_s0 h
    dst base offset t b index 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)

//--
//-- Store128_buffer

[@ "opaque_to_smt"]
let va_code_Store128_buffer h src base offset t =
  (Ins (S.Store128 src base offset))

[@ "opaque_to_smt"]
let va_codegen_success_Store128_buffer h src base offset t =
  (va_ttrue ())

[@"opaque_to_smt"]
let va_lemma_Store128_buffer va_b0 va_s0 h src base offset t b index =
  va_reveal_opaque (`%va_code_Store128_buffer) (va_code_Store128_buffer h src base offset t);
  let (va_old_s:va_state) = va_s0 in
  va_ins_lemma (Ins (S.Store128 src base offset)) va_s0;
  let (va_sM, va_fM) = va_eval_ins (Ins (S.Store128 src base offset)) va_s0 in
  Vale.PPC64LE.Memory_Sems.low_lemma_store_mem128_full b index (va_eval_vec_opr va_old_s src)
    (Vale.PPC64LE.Decls.from_heap_impl (va_old_s.ms_heap)) t h;
  (va_sM, va_fM)


[@"opaque_to_smt"]
let va_wpProof_Store128_buffer h src base offset t b index va_s0 va_k =
  let (va_sM, va_f0) = va_lemma_Store128_buffer (va_code_Store128_buffer h src base offset t) va_s0
    h src base offset t b index in
  va_lemma_upd_update va_sM;
  assert (va_state_eq va_sM (va_update_mem va_sM (va_update_ok va_sM (va_update_operand_heaplet h
    va_sM va_s0))));
  va_lemma_norm_mods ([va_Mod_mem; va_mod_heaplet h]) va_sM va_s0;
  let va_g = () in
  (va_sM, va_f0, va_g)

//--
//-- Load128_word4_buffer

[@ "opaque_to_smt"]
let va_code_Load128_word4_buffer h dst base t =
  (Ins (S.Load128Word4 dst base))

[@ "opaque_to_smt"]
let va_codegen_success_Load128_word4_buffer h dst base t =
  (va_ttrue ())

[@"opaque_to_smt"]
let va_lemma_Load128_word4_buffer va_b0 va_s0 h dst base t b index =
  va_reveal_opaque (`%va_code_Load128_word4_buffer) (va_code_Load128_word4_buffer h dst base t);
  let (va_old_s:va_state) = va_s0 in
  va_ins_lemma (Ins (S.Load128Word4 dst base)) va_s0;
  let (va_sM, va_fM) = va_eval_ins (Ins (S.Load128Word4 dst base)) va_s0 in
  Vale.PPC64LE.Memory_Sems.low_lemma_load_mem128_full b index (Vale.PPC64LE.Decls.from_heap_impl
    (va_sM.ms_heap)) t h;
  (va_sM, va_fM)


[@"opaque_to_smt"]
let va_wpProof_Load128_word4_buffer h dst base t b index va_s0 va_k =
  let (va_sM, va_f0) = va_lemma_Load128_word4_buffer (va_code_Load128_word4_buffer h dst base t)
    va_s0 h dst base t b index 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)

//--
//-- Load128_word4_buffer_index

[@ "opaque_to_smt"]
let va_code_Load128_word4_buffer_index h dst base offset t =
  (Ins (S.Load128Word4Index dst base offset))

[@ "opaque_to_smt"]
let va_codegen_success_Load128_word4_buffer_index h dst base offset t =
  (va_ttrue ())

[@"opaque_to_smt"]
let va_lemma_Load128_word4_buffer_index va_b0 va_s0 h dst base offset t b index =
  va_reveal_opaque (`%va_code_Load128_word4_buffer_index) (va_code_Load128_word4_buffer_index h dst
    base offset t);
  let (va_old_s:va_state) = va_s0 in
  va_ins_lemma (Ins (S.Load128Word4Index dst base offset)) va_s0;
  let (va_sM, va_fM) = va_eval_ins (Ins (S.Load128Word4Index dst base offset)) va_s0 in
  Vale.PPC64LE.Memory_Sems.low_lemma_load_mem128_full b index (Vale.PPC64LE.Decls.from_heap_impl
    (va_sM.ms_heap)) t h;
  (va_sM, va_fM)


[@"opaque_to_smt"]
let va_wpProof_Load128_word4_buffer_index h dst base offset t b index va_s0 va_k =
  let (va_sM, va_f0) = va_lemma_Load128_word4_buffer_index (va_code_Load128_word4_buffer_index h
    dst base offset t) va_s0 h dst base offset t b index 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)

//--
//-- Store128_word4_buffer

[@ "opaque_to_smt"]
let va_code_Store128_word4_buffer h src base t =
  (Ins (S.Store128Word4 src base))

[@ "opaque_to_smt"]
let va_codegen_success_Store128_word4_buffer h src base t =
  (va_ttrue ())

[@"opaque_to_smt"]
let va_lemma_Store128_word4_buffer va_b0 va_s0 h src base t b index =
  va_reveal_opaque (`%va_code_Store128_word4_buffer) (va_code_Store128_word4_buffer h src base t);
  let (va_old_s:va_state) = va_s0 in
  va_ins_lemma (Ins (S.Store128Word4 src base)) va_s0;
  let (va_sM, va_fM) = va_eval_ins (Ins (S.Store128Word4 src base)) va_s0 in
  Vale.PPC64LE.Memory_Sems.low_lemma_store_mem128_full b index (Vale.Def.Words_s.Mkfour
    #Vale.Def.Types_s.nat32 (Vale.Def.Words_s.__proj__Mkfour__item__hi3 (va_eval_vec_opr va_old_s
    src)) (Vale.Def.Words_s.__proj__Mkfour__item__hi2 (va_eval_vec_opr va_old_s src))
    (Vale.Def.Words_s.__proj__Mkfour__item__lo1 (va_eval_vec_opr va_old_s src))
    (Vale.Def.Words_s.__proj__Mkfour__item__lo0 (va_eval_vec_opr va_old_s src)))
    (Vale.PPC64LE.Decls.from_heap_impl (va_old_s.ms_heap)) t h;
  (va_sM, va_fM)


[@"opaque_to_smt"]
let va_wpProof_Store128_word4_buffer h src base t b index va_s0 va_k =
  let (va_sM, va_f0) = va_lemma_Store128_word4_buffer (va_code_Store128_word4_buffer h src base t)
    va_s0 h src base t b index in
  va_lemma_upd_update va_sM;
  assert (va_state_eq va_sM (va_update_mem va_sM (va_update_ok va_sM (va_update_operand_heaplet h
    va_sM va_s0))));
  va_lemma_norm_mods ([va_Mod_mem; va_mod_heaplet h]) va_sM va_s0;
  let va_g = () in
  (va_sM, va_f0, va_g)

//--
//-- Store128_word4_buffer_index

[@ "opaque_to_smt"]
let va_code_Store128_word4_buffer_index h src base offset t =
  (Ins (S.Store128Word4Index src base offset))

[@ "opaque_to_smt"]
let va_codegen_success_Store128_word4_buffer_index h src base offset t =
  (va_ttrue ())

[@"opaque_to_smt"]
let va_lemma_Store128_word4_buffer_index va_b0 va_s0 h src base offset t b index =
  va_reveal_opaque (`%va_code_Store128_word4_buffer_index) (va_code_Store128_word4_buffer_index h
    src base offset t);
  let (va_old_s:va_state) = va_s0 in
  va_ins_lemma (Ins (S.Store128Word4Index src base offset)) va_s0;
  let (va_sM, va_fM) = va_eval_ins (Ins (S.Store128Word4Index src base offset)) va_s0 in
  Vale.PPC64LE.Memory_Sems.low_lemma_store_mem128_full b index (Vale.Def.Words_s.Mkfour
    #Vale.Def.Types_s.nat32 (Vale.Def.Words_s.__proj__Mkfour__item__hi3 (va_eval_vec_opr va_old_s
    src)) (Vale.Def.Words_s.__proj__Mkfour__item__hi2 (va_eval_vec_opr va_old_s src))
    (Vale.Def.Words_s.__proj__Mkfour__item__lo1 (va_eval_vec_opr va_old_s src))
    (Vale.Def.Words_s.__proj__Mkfour__item__lo0 (va_eval_vec_opr va_old_s src)))
    (Vale.PPC64LE.Decls.from_heap_impl (va_old_s.ms_heap)) t h;
  (va_sM, va_fM)


[@"opaque_to_smt"]
let va_wpProof_Store128_word4_buffer_index h src base offset t b index va_s0 va_k =
  let (va_sM, va_f0) = va_lemma_Store128_word4_buffer_index (va_code_Store128_word4_buffer_index h
    src base offset t) va_s0 h src base offset t b index in
  va_lemma_upd_update va_sM;
  assert (va_state_eq va_sM (va_update_mem va_sM (va_update_ok va_sM (va_update_operand_heaplet h
    va_sM va_s0))));
  va_lemma_norm_mods ([va_Mod_mem; va_mod_heaplet h]) va_sM va_s0;
  let va_g = () in
  (va_sM, va_f0, va_g)

//--
//-- Load128_byte16_buffer

[@ "opaque_to_smt"]
let va_code_Load128_byte16_buffer h dst base t =
  (Ins (S.Load128Byte16 dst base))

[@ "opaque_to_smt"]
let va_codegen_success_Load128_byte16_buffer h dst base t =
  (va_ttrue ())

[@"opaque_to_smt"]
let va_lemma_Load128_byte16_buffer va_b0 va_s0 h dst base t b index =
  va_reveal_opaque (`%va_code_Load128_byte16_buffer) (va_code_Load128_byte16_buffer h dst base t);
  let (va_old_s:va_state) = va_s0 in
  va_ins_lemma (Ins (S.Load128Byte16 dst base)) va_s0;
  let (va_sM, va_fM) = va_eval_ins (Ins (S.Load128Byte16 dst base)) va_s0 in
  Vale.PPC64LE.Memory_Sems.low_lemma_load_mem128_full b index (Vale.PPC64LE.Decls.from_heap_impl
    (va_sM.ms_heap)) t h;
  (va_sM, va_fM)


[@"opaque_to_smt"]
let va_wpProof_Load128_byte16_buffer h dst base t b index va_s0 va_k =
  let (va_sM, va_f0) = va_lemma_Load128_byte16_buffer (va_code_Load128_byte16_buffer h dst base t)
    va_s0 h dst base t b index 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)

//--
//-- Load128_byte16_buffer_index

[@ "opaque_to_smt"]
let va_code_Load128_byte16_buffer_index h dst base offset t =
  (Ins (S.Load128Byte16Index dst base offset))

[@ "opaque_to_smt"]
let va_codegen_success_Load128_byte16_buffer_index h dst base offset t =
  (va_ttrue ())

[@"opaque_to_smt"]
let va_lemma_Load128_byte16_buffer_index va_b0 va_s0 h dst base offset t b index =
  va_reveal_opaque (`%va_code_Load128_byte16_buffer_index) (va_code_Load128_byte16_buffer_index h
    dst base offset t);
  let (va_old_s:va_state) = va_s0 in
  va_ins_lemma (Ins (S.Load128Byte16Index dst base offset)) va_s0;
  let (va_sM, va_fM) = va_eval_ins (Ins (S.Load128Byte16Index dst base offset)) va_s0 in
  Vale.PPC64LE.Memory_Sems.low_lemma_load_mem128_full b index (Vale.PPC64LE.Decls.from_heap_impl
    (va_sM.ms_heap)) t h;
  (va_sM, va_fM)


[@"opaque_to_smt"]
let va_wpProof_Load128_byte16_buffer_index h dst base offset t b index va_s0 va_k =
  let (va_sM, va_f0) = va_lemma_Load128_byte16_buffer_index (va_code_Load128_byte16_buffer_index h
    dst base offset t) va_s0 h dst base offset t b index 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)

//--
//-- Store128_byte16_buffer

[@ "opaque_to_smt"]
let va_code_Store128_byte16_buffer h src base t =
  (Ins (S.Store128Byte16 src base))

[@ "opaque_to_smt"]
let va_codegen_success_Store128_byte16_buffer h src base t =
  (va_ttrue ())

[@"opaque_to_smt"]
let va_lemma_Store128_byte16_buffer va_b0 va_s0 h src base t b index =
  va_reveal_opaque (`%va_code_Store128_byte16_buffer) (va_code_Store128_byte16_buffer h src base t);
  let (va_old_s:va_state) = va_s0 in
  va_ins_lemma (Ins (S.Store128Byte16 src base)) va_s0;
  let (va_sM, va_fM) = va_eval_ins (Ins (S.Store128Byte16 src base)) va_s0 in
  Vale.PPC64LE.Memory_Sems.low_lemma_store_mem128_full b index
    (Vale.Def.Types_s.reverse_bytes_quad32 (va_eval_vec_opr va_old_s src))
    (Vale.PPC64LE.Decls.from_heap_impl (va_old_s.ms_heap)) t h;
  (va_sM, va_fM)


[@"opaque_to_smt"]
let va_wpProof_Store128_byte16_buffer h src base t b index va_s0 va_k =
  let (va_sM, va_f0) = va_lemma_Store128_byte16_buffer (va_code_Store128_byte16_buffer h src base
    t) va_s0 h src base t b index in
  va_lemma_upd_update va_sM;
  assert (va_state_eq va_sM (va_update_mem va_sM (va_update_ok va_sM (va_update_operand_heaplet h
    va_sM va_s0))));
  va_lemma_norm_mods ([va_Mod_mem; va_mod_heaplet h]) va_sM va_s0;
  let va_g = () in
  (va_sM, va_f0, va_g)

//--
//-- Store128_byte16_buffer_index

[@ "opaque_to_smt"]
let va_code_Store128_byte16_buffer_index h src base offset t =
  (Ins (S.Store128Byte16Index src base offset))

[@ "opaque_to_smt"]
let va_codegen_success_Store128_byte16_buffer_index h src base offset t =
  (va_ttrue ())

[@"opaque_to_smt"]
let va_lemma_Store128_byte16_buffer_index va_b0 va_s0 h src base offset t b index =
  va_reveal_opaque (`%va_code_Store128_byte16_buffer_index) (va_code_Store128_byte16_buffer_index h
    src base offset t);
  let (va_old_s:va_state) = va_s0 in
  va_ins_lemma (Ins (S.Store128Byte16Index src base offset)) va_s0;
  let (va_sM, va_fM) = va_eval_ins (Ins (S.Store128Byte16Index src base offset)) va_s0 in
  Vale.PPC64LE.Memory_Sems.low_lemma_store_mem128_full b index
    (Vale.Def.Types_s.reverse_bytes_quad32 (va_eval_vec_opr va_old_s src))
    (Vale.PPC64LE.Decls.from_heap_impl (va_old_s.ms_heap)) t h;
  (va_sM, va_fM)


[@"opaque_to_smt"]
let va_wpProof_Store128_byte16_buffer_index h src base offset t b index va_s0 va_k =
  let (va_sM, va_f0) = va_lemma_Store128_byte16_buffer_index (va_code_Store128_byte16_buffer_index
    h src base offset t) va_s0 h src base offset t b index in
  va_lemma_upd_update va_sM;
  assert (va_state_eq va_sM (va_update_mem va_sM (va_update_ok va_sM (va_update_operand_heaplet h
    va_sM va_s0))));
  va_lemma_norm_mods ([va_Mod_mem; va_mod_heaplet h]) va_sM va_s0;
  let va_g = () in
  (va_sM, va_f0, va_g)

//--
//-- SHA256_sigma0

[@ "opaque_to_smt"]
let va_code_SHA256_sigma0 dst src =
  (Ins (S.Vshasigmaw0 dst src))

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

[@"opaque_to_smt"]
let va_lemma_SHA256_sigma0 va_b0 va_s0 dst src t block =
  va_reveal_opaque (`%va_code_SHA256_sigma0) (va_code_SHA256_sigma0 dst src);
  let (va_old_s:va_state) = va_s0 in
  va_ins_lemma (Ins (S.Vshasigmaw0 dst src)) va_s0;
  let (va_sM, va_fM) = va_eval_ins (Ins (S.Vshasigmaw0 dst src)) va_s0 in
  lemma_sha256_sigma0 (va_eval_vec_opr va_old_s src) t block;
  (va_sM, va_fM)


[@"opaque_to_smt"]
let va_wpProof_SHA256_sigma0 dst src t block va_s0 va_k =
  let (va_sM, va_f0) = va_lemma_SHA256_sigma0 (va_code_SHA256_sigma0 dst src) va_s0 dst src t block
    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)

//--
//-- SHA256_sigma1

[@ "opaque_to_smt"]
let va_code_SHA256_sigma1 dst src =
  (Ins (S.Vshasigmaw1 dst src))

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

[@"opaque_to_smt"]
let va_lemma_SHA256_sigma1 va_b0 va_s0 dst src t block =
  va_reveal_opaque (`%va_code_SHA256_sigma1) (va_code_SHA256_sigma1 dst src);
  let (va_old_s:va_state) = va_s0 in
  va_ins_lemma (Ins (S.Vshasigmaw1 dst src)) va_s0;
  let (va_sM, va_fM) = va_eval_ins (Ins (S.Vshasigmaw1 dst src)) va_s0 in
  lemma_sha256_sigma1 (va_eval_vec_opr va_old_s src) t block;
  (va_sM, va_fM)


[@"opaque_to_smt"]
let va_wpProof_SHA256_sigma1 dst src t block va_s0 va_k =
  let (va_sM, va_f0) = va_lemma_SHA256_sigma1 (va_code_SHA256_sigma1 dst src) va_s0 dst src t block
    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)

//--
//-- SHA256_Sigma0

[@ "opaque_to_smt"]
let va_code_SHA256_Sigma0 dst src =
  (Ins (S.Vshasigmaw2 dst src))

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

[@"opaque_to_smt"]
let va_lemma_SHA256_Sigma0 va_b0 va_s0 dst src t block hash_orig =
  va_reveal_opaque (`%va_code_SHA256_Sigma0) (va_code_SHA256_Sigma0 dst src);
  let (va_old_s:va_state) = va_s0 in
  va_ins_lemma (Ins (S.Vshasigmaw2 dst src)) va_s0;
  let (va_sM, va_fM) = va_eval_ins (Ins (S.Vshasigmaw2 dst src)) va_s0 in
  Vale.SHA.PPC64LE.SHA_helpers.lemma_sha256_sigma2 (va_eval_vec_opr va_old_s src) t block hash_orig;
  (va_sM, va_fM)


[@"opaque_to_smt"]
let va_wpProof_SHA256_Sigma0 dst src t block hash_orig va_s0 va_k =
  let (va_sM, va_f0) = va_lemma_SHA256_Sigma0 (va_code_SHA256_Sigma0 dst src) va_s0 dst src t block
    hash_orig 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)

//--
//-- SHA256_Sigma1

[@ "opaque_to_smt"]
let va_code_SHA256_Sigma1 dst src =
  (Ins (S.Vshasigmaw3 dst src))

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

[@"opaque_to_smt"]
let va_lemma_SHA256_Sigma1 va_b0 va_s0 dst src t block hash_orig =
  va_reveal_opaque (`%va_code_SHA256_Sigma1) (va_code_SHA256_Sigma1 dst src);
  let (va_old_s:va_state) = va_s0 in
  va_ins_lemma (Ins (S.Vshasigmaw3 dst src)) va_s0;
  let (va_sM, va_fM) = va_eval_ins (Ins (S.Vshasigmaw3 dst src)) va_s0 in
  Vale.SHA.PPC64LE.SHA_helpers.lemma_sha256_sigma3 (va_eval_vec_opr va_old_s src) t block hash_orig;
  (va_sM, va_fM)


[@"opaque_to_smt"]
let va_wpProof_SHA256_Sigma1 dst src t block hash_orig va_s0 va_k =
  let (va_sM, va_f0) = va_lemma_SHA256_Sigma1 (va_code_SHA256_Sigma1 dst src) va_s0 dst src t block
    hash_orig 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)

//--
//-- Vsbox

[@ "opaque_to_smt"]
let va_code_Vsbox dst src =
  (Ins (S.Vsbox dst src))

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

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


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

//--
//-- RotWord

[@ "opaque_to_smt"]
let va_code_RotWord dst src1 src2 =
  (Ins (S.RotWord dst src1 src2))

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

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


[@"opaque_to_smt"]
let va_wpProof_RotWord dst src1 src2 va_s0 va_k =
  let (va_sM, va_f0) = va_lemma_RotWord (va_code_RotWord 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)

//--
//-- Vcipher

[@ "opaque_to_smt"]
let va_code_Vcipher dst src1 src2 =
  (Ins (S.Vcipher dst src1 src2))

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

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


[@"opaque_to_smt"]
let va_wpProof_Vcipher dst src1 src2 va_s0 va_k =
  let (va_sM, va_f0) = va_lemma_Vcipher (va_code_Vcipher 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)

//--
//-- Vcipherlast

[@ "opaque_to_smt"]
let va_code_Vcipherlast dst src1 src2 =
  (Ins (S.Vcipherlast dst src1 src2))

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

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


[@"opaque_to_smt"]
let va_wpProof_Vcipherlast dst src1 src2 va_s0 va_k =
  let (va_sM, va_f0) = va_lemma_Vcipherlast (va_code_Vcipherlast 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)

//--
//-- Vncipher

[@ "opaque_to_smt"]
let va_code_Vncipher dst src1 src2 =
  (Ins (S.Vncipher dst src1 src2))

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

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


[@"opaque_to_smt"]
let va_wpProof_Vncipher dst src1 src2 va_s0 va_k =
  let (va_sM, va_f0) = va_lemma_Vncipher (va_code_Vncipher 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)

//--
//-- Vncipherlast

[@ "opaque_to_smt"]
let va_code_Vncipherlast dst src1 src2 =
  (Ins (S.Vncipherlast dst src1 src2))

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

[@"opaque_to_smt"]
let va_lemma_Vncipherlast va_b0 va_s0 dst src1 src2 =
  va_reveal_opaque (`%va_code_Vncipherlast) (va_code_Vncipherlast dst src1 src2);
  let (va_old_s:va_state) = va_s0 in
  va_ins_lemma (Ins (S.Vncipherlast dst src1 src2)) va_s0;
  let (va_sM, va_fM) = va_eval_ins (Ins (S.Vncipherlast dst src1 src2)) va_s0 in
  (va_sM, va_fM)
val va_wpProof_Vncipherlast : dst:va_operand_vec_opr -> src1:va_operand_vec_opr ->
  src2:va_operand_vec_opr -> va_s0:va_state -> va_k:(va_state -> unit -> Type0)
  -> Ghost (va_state & va_fuel & unit)
  (requires (va_t_require va_s0 /\ va_wp_Vncipherlast dst src1 src2 va_s0 va_k))
  (ensures (fun (va_sM, va_f0, va_g) -> va_t_ensure (va_code_Vncipherlast dst src1 src2)
    ([va_mod_vec_opr dst]) va_s0 va_k ((va_sM, va_f0, va_g))))

    dst: Vale.PPC64LE.Decls.va_operand_vec_opr ->
    src1: Vale.PPC64LE.Decls.va_operand_vec_opr ->
    src2: Vale.PPC64LE.Decls.va_operand_vec_opr ->
    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)