val va_quick_Vspltw (dst src: va_operand_vec_opr) (uim: nat2)
    : (va_quickCode unit (va_code_Vspltw dst src uim))
let va_quick_Vspltw (dst:va_operand_vec_opr) (src:va_operand_vec_opr) (uim:nat2) : (va_quickCode
  unit (va_code_Vspltw dst src uim)) =
  (va_QProc (va_code_Vspltw dst src uim) ([va_mod_vec_opr dst]) (va_wp_Vspltw dst src uim)
    (va_wpProof_Vspltw dst src uim))
val va_quick_Vspltw (dst src: va_operand_vec_opr) (uim: nat2)
    : (va_quickCode unit (va_code_Vspltw dst src uim))
let va_quick_Vspltw (dst src: va_operand_vec_opr) (uim: nat2)
    : (va_quickCode unit (va_code_Vspltw dst src uim)) =
(va_QProc (va_code_Vspltw dst src uim)
    ([va_mod_vec_opr dst])
    (va_wp_Vspltw dst src uim)
    (va_wpProof_Vspltw dst src uim))
Vale.PPC64LE.InsVector.fsti.checked
Vale.SHA.PPC64LE.SHA_helpers.fsti.checked Vale.PPC64LE.State.fsti.checked Vale.PPC64LE.QuickCode.fst.checked Vale.PPC64LE.Memory.fsti.checked Vale.PPC64LE.Machine_s.fst.checked Vale.PPC64LE.InsMem.fsti.checked Vale.PPC64LE.InsBasic.fsti.checked Vale.PPC64LE.Decls.fsti.checked Vale.Math.Poly2_s.fsti.checked Vale.Math.Poly2.Bits_s.fsti.checked Vale.Def.Words_s.fsti.checked Vale.Def.Words.Two_s.fsti.checked Vale.Def.Words.Seq_s.fsti.checked Vale.Def.Words.Four_s.fsti.checked Vale.Def.Types_s.fst.checked Vale.Def.Sel.fst.checked Vale.Arch.Types.fsti.checked Vale.AES.AES_common_s.fst.checked Vale.AES.AES_BE_s.fst.checked Spec.SHA2.fsti.checked Spec.Hash.Definitions.fst.checked prims.fst.checked FStar.Seq.Base.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked
Vale.PPC64LE.InsVector.fsti
Vale.PPC64LE.Decls.va_operand_vec_opr Vale.Def.Words_s.nat2 Vale.PPC64LE.QuickCode.va_QProc Prims.unit Vale.PPC64LE.InsVector.va_code_Vspltw Prims.Cons Vale.PPC64LE.QuickCode.mod_t Vale.PPC64LE.QuickCode.va_mod_vec_opr Prims.Nil Vale.PPC64LE.InsVector.va_wp_Vspltw Vale.PPC64LE.InsVector.va_wpProof_Vspltw Vale.PPC64LE.QuickCode.va_quickCode
module Vale.PPC64LE.InsVector
open FStar.Seq
open FStar.Mul
open Vale.Def.Words_s
open Vale.Def.Words.Two_s
open Vale.Def.Words.Four_s
open Vale.Def.Types_s
open Vale.PPC64LE.Machine_s
open Vale.PPC64LE.State
open Vale.PPC64LE.Decls
open Vale.PPC64LE.QuickCode
open Vale.PPC64LE.InsBasic
open Vale.PPC64LE.InsMem
open Vale.PPC64LE.Memory
open Vale.Def.Sel
open Spec.SHA2
open Spec.Hash.Definitions
open Vale.SHA.PPC64LE.SHA_helpers
open Vale.AES.AES_BE_s
open Vale.Math.Poly2_s
open Vale.Math.Poly2.Bits_s

let buffer128_write (b:buffer128) (i:int) (v:quad32) (h:vale_heap) : Ghost vale_heap
  (requires buffer_readable h b /\ buffer_writeable b)
  (ensures fun _ -> True)
  =
  buffer_write b i v h
//-- Vmr

val va_code_Vmr : dst:va_operand_vec_opr -> src:va_operand_vec_opr -> Tot va_code

val va_codegen_success_Vmr : dst:va_operand_vec_opr -> src:va_operand_vec_opr -> Tot va_pbool

val va_lemma_Vmr : va_b0:va_code -> va_s0:va_state -> dst:va_operand_vec_opr ->
  src:va_operand_vec_opr
  -> Ghost (va_state & va_fuel)
  (requires (va_require_total va_b0 (va_code_Vmr dst src) va_s0 /\ va_is_dst_vec_opr dst va_s0 /\
    va_is_src_vec_opr src va_s0 /\ va_get_ok va_s0))
  (ensures (fun (va_sM, va_fM) -> va_ensure_total va_b0 va_s0 va_sM va_fM /\ va_get_ok va_sM /\
    va_eval_vec_opr va_sM dst == va_eval_vec_opr va_sM src /\ va_state_eq va_sM (va_update_ok va_sM
    (va_update_operand_vec_opr dst va_sM va_s0))))
[@ va_qattr]
let va_wp_Vmr (dst:va_operand_vec_opr) (src:va_operand_vec_opr) (va_s0:va_state) (va_k:(va_state ->
  unit -> Type0)) : Type0 =
  (va_is_dst_vec_opr dst va_s0 /\ va_is_src_vec_opr src va_s0 /\ va_get_ok va_s0 /\ (forall
    (va_x_dst:va_value_vec_opr) . let va_sM = va_upd_operand_vec_opr dst va_x_dst va_s0 in
    va_get_ok va_sM /\ va_eval_vec_opr va_sM dst == va_eval_vec_opr va_sM src ==> va_k va_sM (())))

val va_wpProof_Vmr : dst:va_operand_vec_opr -> src: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_Vmr dst src va_s0 va_k))
  (ensures (fun (va_sM, va_f0, va_g) -> va_t_ensure (va_code_Vmr dst src) ([va_mod_vec_opr dst])
    va_s0 va_k ((va_sM, va_f0, va_g))))
[@ "opaque_to_smt" va_qattr]
let va_quick_Vmr (dst:va_operand_vec_opr) (src:va_operand_vec_opr) : (va_quickCode unit
  (va_code_Vmr dst src)) =
  (va_QProc (va_code_Vmr dst src) ([va_mod_vec_opr dst]) (va_wp_Vmr dst src) (va_wpProof_Vmr dst
    src))
//--
//-- Mfvsrd

val va_code_Mfvsrd : dst:va_operand_reg_opr -> src:va_operand_vec_opr -> Tot va_code

val va_codegen_success_Mfvsrd : dst:va_operand_reg_opr -> src:va_operand_vec_opr -> Tot va_pbool

val va_lemma_Mfvsrd : va_b0:va_code -> va_s0:va_state -> dst:va_operand_reg_opr ->
  src:va_operand_vec_opr
  -> Ghost (va_state & va_fuel)
  (requires (va_require_total va_b0 (va_code_Mfvsrd dst src) va_s0 /\ va_is_dst_reg_opr dst va_s0
    /\ va_is_src_vec_opr src va_s0 /\ va_get_ok va_s0))
  (ensures (fun (va_sM, va_fM) -> va_ensure_total va_b0 va_s0 va_sM va_fM /\ va_get_ok va_sM /\
    va_eval_reg_opr va_sM dst == Vale.Arch.Types.hi64 (va_eval_vec_opr va_sM src) /\ va_state_eq
    va_sM (va_update_ok va_sM (va_update_operand_reg_opr dst va_sM va_s0))))
[@ va_qattr]
let va_wp_Mfvsrd (dst:va_operand_reg_opr) (src:va_operand_vec_opr) (va_s0:va_state) (va_k:(va_state
  -> unit -> Type0)) : Type0 =
  (va_is_dst_reg_opr dst va_s0 /\ va_is_src_vec_opr src va_s0 /\ va_get_ok va_s0 /\ (forall
    (va_x_dst:va_value_reg_opr) . let va_sM = va_upd_operand_reg_opr dst va_x_dst va_s0 in
    va_get_ok va_sM /\ va_eval_reg_opr va_sM dst == Vale.Arch.Types.hi64 (va_eval_vec_opr va_sM
    src) ==> va_k va_sM (())))

val va_wpProof_Mfvsrd : dst:va_operand_reg_opr -> src: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_Mfvsrd dst src va_s0 va_k))
  (ensures (fun (va_sM, va_f0, va_g) -> va_t_ensure (va_code_Mfvsrd dst src) ([va_mod_reg_opr dst])
    va_s0 va_k ((va_sM, va_f0, va_g))))
[@ "opaque_to_smt" va_qattr]
let va_quick_Mfvsrd (dst:va_operand_reg_opr) (src:va_operand_vec_opr) : (va_quickCode unit
  (va_code_Mfvsrd dst src)) =
  (va_QProc (va_code_Mfvsrd dst src) ([va_mod_reg_opr dst]) (va_wp_Mfvsrd dst src)
    (va_wpProof_Mfvsrd dst src))
//--
//-- Mfvsrld

val va_code_Mfvsrld : dst:va_operand_reg_opr -> src:va_operand_vec_opr -> Tot va_code

val va_codegen_success_Mfvsrld : dst:va_operand_reg_opr -> src:va_operand_vec_opr -> Tot va_pbool

val va_lemma_Mfvsrld : va_b0:va_code -> va_s0:va_state -> dst:va_operand_reg_opr ->
  src:va_operand_vec_opr
  -> Ghost (va_state & va_fuel)
  (requires (va_require_total va_b0 (va_code_Mfvsrld dst src) va_s0 /\ va_is_dst_reg_opr dst va_s0
    /\ va_is_src_vec_opr src va_s0 /\ va_get_ok va_s0))
  (ensures (fun (va_sM, va_fM) -> va_ensure_total va_b0 va_s0 va_sM va_fM /\ va_get_ok va_sM /\
    va_eval_reg_opr va_sM dst == Vale.Arch.Types.lo64 (va_eval_vec_opr va_sM src) /\ va_state_eq
    va_sM (va_update_ok va_sM (va_update_operand_reg_opr dst va_sM va_s0))))
[@ va_qattr]
let va_wp_Mfvsrld (dst:va_operand_reg_opr) (src:va_operand_vec_opr) (va_s0:va_state)
  (va_k:(va_state -> unit -> Type0)) : Type0 =
  (va_is_dst_reg_opr dst va_s0 /\ va_is_src_vec_opr src va_s0 /\ va_get_ok va_s0 /\ (forall
    (va_x_dst:va_value_reg_opr) . let va_sM = va_upd_operand_reg_opr dst va_x_dst va_s0 in
    va_get_ok va_sM /\ va_eval_reg_opr va_sM dst == Vale.Arch.Types.lo64 (va_eval_vec_opr va_sM
    src) ==> va_k va_sM (())))

val va_wpProof_Mfvsrld : dst:va_operand_reg_opr -> src: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_Mfvsrld dst src va_s0 va_k))
  (ensures (fun (va_sM, va_f0, va_g) -> va_t_ensure (va_code_Mfvsrld dst src) ([va_mod_reg_opr
    dst]) va_s0 va_k ((va_sM, va_f0, va_g))))
[@ "opaque_to_smt" va_qattr]
let va_quick_Mfvsrld (dst:va_operand_reg_opr) (src:va_operand_vec_opr) : (va_quickCode unit
  (va_code_Mfvsrld dst src)) =
  (va_QProc (va_code_Mfvsrld dst src) ([va_mod_reg_opr dst]) (va_wp_Mfvsrld dst src)
    (va_wpProof_Mfvsrld dst src))
//--
//-- Mtvsrdd

val va_code_Mtvsrdd : dst:va_operand_vec_opr -> src1:va_operand_reg_opr -> src2:va_operand_reg_opr
  -> Tot va_code

val va_codegen_success_Mtvsrdd : dst:va_operand_vec_opr -> src1:va_operand_reg_opr ->
  src2:va_operand_reg_opr -> Tot va_pbool

val va_lemma_Mtvsrdd : va_b0:va_code -> va_s0:va_state -> dst:va_operand_vec_opr ->
  src1:va_operand_reg_opr -> src2:va_operand_reg_opr
  -> Ghost (va_state & va_fuel)
  (requires (va_require_total va_b0 (va_code_Mtvsrdd dst src1 src2) va_s0 /\ va_is_dst_vec_opr dst
    va_s0 /\ va_is_src_reg_opr src1 va_s0 /\ va_is_src_reg_opr src2 va_s0 /\ va_get_ok va_s0))
  (ensures (fun (va_sM, va_fM) -> va_ensure_total va_b0 va_s0 va_sM va_fM /\ va_get_ok va_sM /\
    va_mul_nat pow2_32 (Vale.Def.Words_s.__proj__Mkfour__item__hi3 (va_eval_vec_opr va_sM dst)) +
    Vale.Def.Words_s.__proj__Mkfour__item__hi2 (va_eval_vec_opr va_sM dst) == va_eval_reg_opr va_s0
    src1 /\ va_mul_nat pow2_32 (Vale.Def.Words_s.__proj__Mkfour__item__lo1 (va_eval_vec_opr va_sM
    dst)) + Vale.Def.Words_s.__proj__Mkfour__item__lo0 (va_eval_vec_opr va_sM dst) ==
    va_eval_reg_opr va_s0 src2 /\ va_eval_vec_opr va_sM dst ==
    Vale.Def.Words.Four_s.two_two_to_four #Vale.Def.Types_s.nat32 (Vale.Def.Words_s.Mktwo
    #(Vale.Def.Words_s.two Vale.Def.Types_s.nat32) (Vale.Def.Words_s.Mktwo #Vale.Def.Types_s.nat32
    (va_eval_reg_opr va_s0 src2 `op_Modulus` pow2_32) (va_eval_reg_opr va_s0 src2 `op_Division`
    pow2_32)) (Vale.Def.Words_s.Mktwo #Vale.Def.Types_s.nat32 (va_eval_reg_opr va_s0 src1
    `op_Modulus` pow2_32) (va_eval_reg_opr va_s0 src1 `op_Division` pow2_32))) /\ va_state_eq va_sM
    (va_update_ok va_sM (va_update_operand_vec_opr dst va_sM va_s0))))
[@ va_qattr]
let va_wp_Mtvsrdd (dst:va_operand_vec_opr) (src1:va_operand_reg_opr) (src2:va_operand_reg_opr)
  (va_s0:va_state) (va_k:(va_state -> unit -> Type0)) : Type0 =
  (va_is_dst_vec_opr dst va_s0 /\ va_is_src_reg_opr src1 va_s0 /\ va_is_src_reg_opr src2 va_s0 /\
    va_get_ok va_s0 /\ (forall (va_x_dst:va_value_vec_opr) . let va_sM = va_upd_operand_vec_opr dst
    va_x_dst va_s0 in va_get_ok va_sM /\ va_mul_nat pow2_32
    (Vale.Def.Words_s.__proj__Mkfour__item__hi3 (va_eval_vec_opr va_sM dst)) +
    Vale.Def.Words_s.__proj__Mkfour__item__hi2 (va_eval_vec_opr va_sM dst) == va_eval_reg_opr va_s0
    src1 /\ va_mul_nat pow2_32 (Vale.Def.Words_s.__proj__Mkfour__item__lo1 (va_eval_vec_opr va_sM
    dst)) + Vale.Def.Words_s.__proj__Mkfour__item__lo0 (va_eval_vec_opr va_sM dst) ==
    va_eval_reg_opr va_s0 src2 /\ va_eval_vec_opr va_sM dst ==
    Vale.Def.Words.Four_s.two_two_to_four #Vale.Def.Types_s.nat32 (Vale.Def.Words_s.Mktwo
    #(Vale.Def.Words_s.two Vale.Def.Types_s.nat32) (Vale.Def.Words_s.Mktwo #Vale.Def.Types_s.nat32
    (va_eval_reg_opr va_s0 src2 `op_Modulus` pow2_32) (va_eval_reg_opr va_s0 src2 `op_Division`
    pow2_32)) (Vale.Def.Words_s.Mktwo #Vale.Def.Types_s.nat32 (va_eval_reg_opr va_s0 src1
    `op_Modulus` pow2_32) (va_eval_reg_opr va_s0 src1 `op_Division` pow2_32))) ==> va_k va_sM (())))

val va_wpProof_Mtvsrdd : dst:va_operand_vec_opr -> src1:va_operand_reg_opr ->
  src2:va_operand_reg_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_Mtvsrdd dst src1 src2 va_s0 va_k))
  (ensures (fun (va_sM, va_f0, va_g) -> va_t_ensure (va_code_Mtvsrdd dst src1 src2)
    ([va_mod_vec_opr dst]) va_s0 va_k ((va_sM, va_f0, va_g))))
[@ "opaque_to_smt" va_qattr]
let va_quick_Mtvsrdd (dst:va_operand_vec_opr) (src1:va_operand_reg_opr) (src2:va_operand_reg_opr) :
  (va_quickCode unit (va_code_Mtvsrdd dst src1 src2)) =
  (va_QProc (va_code_Mtvsrdd dst src1 src2) ([va_mod_vec_opr dst]) (va_wp_Mtvsrdd dst src1 src2)
    (va_wpProof_Mtvsrdd dst src1 src2))
//--
//-- Mtvsrws

val va_code_Mtvsrws : dst:va_operand_vec_opr -> src:va_operand_reg_opr -> Tot va_code

val va_codegen_success_Mtvsrws : dst:va_operand_vec_opr -> src:va_operand_reg_opr -> Tot va_pbool

val va_lemma_Mtvsrws : va_b0:va_code -> va_s0:va_state -> dst:va_operand_vec_opr ->
  src:va_operand_reg_opr
  -> Ghost (va_state & va_fuel)
  (requires (va_require_total va_b0 (va_code_Mtvsrws dst src) va_s0 /\ va_is_dst_vec_opr dst va_s0
    /\ va_is_src_reg_opr src va_s0 /\ va_get_ok va_s0))
  (ensures (fun (va_sM, va_fM) -> va_ensure_total va_b0 va_s0 va_sM va_fM /\ va_get_ok va_sM /\
    Vale.Def.Words_s.__proj__Mkfour__item__lo0 (va_eval_vec_opr va_sM dst) == va_eval_reg_opr va_s0
    src `op_Modulus` pow2_32 /\ Vale.Def.Words_s.__proj__Mkfour__item__lo1 (va_eval_vec_opr va_sM
    dst) == va_eval_reg_opr va_s0 src `op_Modulus` pow2_32 /\
    Vale.Def.Words_s.__proj__Mkfour__item__hi2 (va_eval_vec_opr va_sM dst) == va_eval_reg_opr va_s0
    src `op_Modulus` pow2_32 /\ Vale.Def.Words_s.__proj__Mkfour__item__hi3 (va_eval_vec_opr va_sM
    dst) == va_eval_reg_opr va_s0 src `op_Modulus` pow2_32 /\ va_state_eq va_sM (va_update_ok va_sM
    (va_update_operand_vec_opr dst va_sM va_s0))))
[@ va_qattr]
let va_wp_Mtvsrws (dst:va_operand_vec_opr) (src:va_operand_reg_opr) (va_s0:va_state)
  (va_k:(va_state -> unit -> Type0)) : Type0 =
  (va_is_dst_vec_opr dst va_s0 /\ va_is_src_reg_opr src va_s0 /\ va_get_ok va_s0 /\ (forall
    (va_x_dst:va_value_vec_opr) . let va_sM = va_upd_operand_vec_opr dst va_x_dst va_s0 in
    va_get_ok va_sM /\ Vale.Def.Words_s.__proj__Mkfour__item__lo0 (va_eval_vec_opr va_sM dst) ==
    va_eval_reg_opr va_s0 src `op_Modulus` pow2_32 /\ Vale.Def.Words_s.__proj__Mkfour__item__lo1
    (va_eval_vec_opr va_sM dst) == va_eval_reg_opr va_s0 src `op_Modulus` pow2_32 /\
    Vale.Def.Words_s.__proj__Mkfour__item__hi2 (va_eval_vec_opr va_sM dst) == va_eval_reg_opr va_s0
    src `op_Modulus` pow2_32 /\ Vale.Def.Words_s.__proj__Mkfour__item__hi3 (va_eval_vec_opr va_sM
    dst) == va_eval_reg_opr va_s0 src `op_Modulus` pow2_32 ==> va_k va_sM (())))

val va_wpProof_Mtvsrws : dst:va_operand_vec_opr -> src:va_operand_reg_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_Mtvsrws dst src va_s0 va_k))
  (ensures (fun (va_sM, va_f0, va_g) -> va_t_ensure (va_code_Mtvsrws dst src) ([va_mod_vec_opr
    dst]) va_s0 va_k ((va_sM, va_f0, va_g))))
[@ "opaque_to_smt" va_qattr]
let va_quick_Mtvsrws (dst:va_operand_vec_opr) (src:va_operand_reg_opr) : (va_quickCode unit
  (va_code_Mtvsrws dst src)) =
  (va_QProc (va_code_Mtvsrws dst src) ([va_mod_vec_opr dst]) (va_wp_Mtvsrws dst src)
    (va_wpProof_Mtvsrws dst src))
//--
//-- Vadduwm

val va_code_Vadduwm : dst:va_operand_vec_opr -> src1:va_operand_vec_opr -> src2:va_operand_vec_opr
  -> Tot va_code

val va_codegen_success_Vadduwm : dst:va_operand_vec_opr -> src1:va_operand_vec_opr ->
  src2:va_operand_vec_opr -> Tot va_pbool

val va_lemma_Vadduwm : va_b0:va_code -> va_s0:va_state -> dst:va_operand_vec_opr ->
  src1:va_operand_vec_opr -> src2:va_operand_vec_opr
  -> Ghost (va_state & va_fuel)
  (requires (va_require_total va_b0 (va_code_Vadduwm dst src1 src2) va_s0 /\ va_is_dst_vec_opr dst
    va_s0 /\ va_is_src_vec_opr src1 va_s0 /\ va_is_src_vec_opr src2 va_s0 /\ va_get_ok va_s0))
  (ensures (fun (va_sM, va_fM) -> va_ensure_total va_b0 va_s0 va_sM va_fM /\ va_get_ok va_sM /\
    va_eval_vec_opr va_sM dst == Vale.Arch.Types.add_wrap_quad32 (va_eval_vec_opr va_s0 src1)
    (va_eval_vec_opr va_s0 src2) /\ va_state_eq va_sM (va_update_ok va_sM
    (va_update_operand_vec_opr dst va_sM va_s0))))
[@ va_qattr]
let va_wp_Vadduwm (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)) : Type0 =
  (va_is_dst_vec_opr dst va_s0 /\ va_is_src_vec_opr src1 va_s0 /\ va_is_src_vec_opr src2 va_s0 /\
    va_get_ok va_s0 /\ (forall (va_x_dst:va_value_vec_opr) . let va_sM = va_upd_operand_vec_opr dst
    va_x_dst va_s0 in va_get_ok va_sM /\ va_eval_vec_opr va_sM dst ==
    Vale.Arch.Types.add_wrap_quad32 (va_eval_vec_opr va_s0 src1) (va_eval_vec_opr va_s0 src2) ==>
    va_k va_sM (())))

val va_wpProof_Vadduwm : 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_Vadduwm dst src1 src2 va_s0 va_k))
  (ensures (fun (va_sM, va_f0, va_g) -> va_t_ensure (va_code_Vadduwm dst src1 src2)
    ([va_mod_vec_opr dst]) va_s0 va_k ((va_sM, va_f0, va_g))))
[@ "opaque_to_smt" va_qattr]
let va_quick_Vadduwm (dst:va_operand_vec_opr) (src1:va_operand_vec_opr) (src2:va_operand_vec_opr) :
  (va_quickCode unit (va_code_Vadduwm dst src1 src2)) =
  (va_QProc (va_code_Vadduwm dst src1 src2) ([va_mod_vec_opr dst]) (va_wp_Vadduwm dst src1 src2)
    (va_wpProof_Vadduwm dst src1 src2))
//--
//-- Vxor

val va_code_Vxor : dst:va_operand_vec_opr -> src1:va_operand_vec_opr -> src2:va_operand_vec_opr ->
  Tot va_code

val va_codegen_success_Vxor : dst:va_operand_vec_opr -> src1:va_operand_vec_opr ->
  src2:va_operand_vec_opr -> Tot va_pbool

val va_lemma_Vxor : va_b0:va_code -> va_s0:va_state -> dst:va_operand_vec_opr ->
  src1:va_operand_vec_opr -> src2:va_operand_vec_opr
  -> Ghost (va_state & va_fuel)
  (requires (va_require_total va_b0 (va_code_Vxor dst src1 src2) va_s0 /\ va_is_dst_vec_opr dst
    va_s0 /\ va_is_src_vec_opr src1 va_s0 /\ va_is_src_vec_opr src2 va_s0 /\ va_get_ok va_s0))
  (ensures (fun (va_sM, va_fM) -> va_ensure_total va_b0 va_s0 va_sM va_fM /\ va_get_ok va_sM /\
    va_eval_vec_opr va_sM dst == Vale.Def.Types_s.quad32_xor (va_eval_vec_opr va_s0 src1)
    (va_eval_vec_opr va_s0 src2) /\ va_state_eq va_sM (va_update_ok va_sM
    (va_update_operand_vec_opr dst va_sM va_s0))))
[@ va_qattr]
let va_wp_Vxor (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)) : Type0 =
  (va_is_dst_vec_opr dst va_s0 /\ va_is_src_vec_opr src1 va_s0 /\ va_is_src_vec_opr src2 va_s0 /\
    va_get_ok va_s0 /\ (forall (va_x_dst:va_value_vec_opr) . let va_sM = va_upd_operand_vec_opr dst
    va_x_dst va_s0 in va_get_ok va_sM /\ va_eval_vec_opr va_sM dst == Vale.Def.Types_s.quad32_xor
    (va_eval_vec_opr va_s0 src1) (va_eval_vec_opr va_s0 src2) ==> va_k va_sM (())))

val va_wpProof_Vxor : 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_Vxor dst src1 src2 va_s0 va_k))
  (ensures (fun (va_sM, va_f0, va_g) -> va_t_ensure (va_code_Vxor dst src1 src2) ([va_mod_vec_opr
    dst]) va_s0 va_k ((va_sM, va_f0, va_g))))
[@ "opaque_to_smt" va_qattr]
let va_quick_Vxor (dst:va_operand_vec_opr) (src1:va_operand_vec_opr) (src2:va_operand_vec_opr) :
  (va_quickCode unit (va_code_Vxor dst src1 src2)) =
  (va_QProc (va_code_Vxor dst src1 src2) ([va_mod_vec_opr dst]) (va_wp_Vxor dst src1 src2)
    (va_wpProof_Vxor dst src1 src2))
//--
//-- Vand

val va_code_Vand : dst:va_operand_vec_opr -> src1:va_operand_vec_opr -> src2:va_operand_vec_opr ->
  Tot va_code

val va_codegen_success_Vand : dst:va_operand_vec_opr -> src1:va_operand_vec_opr ->
  src2:va_operand_vec_opr -> Tot va_pbool

val va_lemma_Vand : va_b0:va_code -> va_s0:va_state -> dst:va_operand_vec_opr ->
  src1:va_operand_vec_opr -> src2:va_operand_vec_opr
  -> Ghost (va_state & va_fuel)
  (requires (va_require_total va_b0 (va_code_Vand dst src1 src2) va_s0 /\ va_is_dst_vec_opr dst
    va_s0 /\ va_is_src_vec_opr src1 va_s0 /\ va_is_src_vec_opr src2 va_s0 /\ va_get_ok va_s0))
  (ensures (fun (va_sM, va_fM) -> va_ensure_total va_b0 va_s0 va_sM va_fM /\ va_get_ok va_sM /\
    va_eval_vec_opr va_sM dst == Vale.Def.Words.Four_s.four_map2 #nat32 #Vale.Def.Types_s.nat32
    (fun (di:nat32) (si:nat32) -> Vale.Arch.Types.iand32 di si) (va_eval_vec_opr va_s0 src1)
    (va_eval_vec_opr va_s0 src2) /\ va_state_eq va_sM (va_update_ok va_sM
    (va_update_operand_vec_opr dst va_sM va_s0))))
[@ va_qattr]
let va_wp_Vand (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)) : Type0 =
  (va_is_dst_vec_opr dst va_s0 /\ va_is_src_vec_opr src1 va_s0 /\ va_is_src_vec_opr src2 va_s0 /\
    va_get_ok va_s0 /\ (forall (va_x_dst:va_value_vec_opr) . let va_sM = va_upd_operand_vec_opr dst
    va_x_dst va_s0 in va_get_ok va_sM /\ va_eval_vec_opr va_sM dst ==
    Vale.Def.Words.Four_s.four_map2 #nat32 #Vale.Def.Types_s.nat32 (fun (di:nat32) (si:nat32) ->
    Vale.Arch.Types.iand32 di si) (va_eval_vec_opr va_s0 src1) (va_eval_vec_opr va_s0 src2) ==>
    va_k va_sM (())))

val va_wpProof_Vand : 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_Vand dst src1 src2 va_s0 va_k))
  (ensures (fun (va_sM, va_f0, va_g) -> va_t_ensure (va_code_Vand dst src1 src2) ([va_mod_vec_opr
    dst]) va_s0 va_k ((va_sM, va_f0, va_g))))
[@ "opaque_to_smt" va_qattr]
let va_quick_Vand (dst:va_operand_vec_opr) (src1:va_operand_vec_opr) (src2:va_operand_vec_opr) :
  (va_quickCode unit (va_code_Vand dst src1 src2)) =
  (va_QProc (va_code_Vand dst src1 src2) ([va_mod_vec_opr dst]) (va_wp_Vand dst src1 src2)
    (va_wpProof_Vand dst src1 src2))
//--
//-- Vslw

val va_code_Vslw : dst:va_operand_vec_opr -> src1:va_operand_vec_opr -> src2:va_operand_vec_opr ->
  Tot va_code

val va_codegen_success_Vslw : dst:va_operand_vec_opr -> src1:va_operand_vec_opr ->
  src2:va_operand_vec_opr -> Tot va_pbool

val va_lemma_Vslw : va_b0:va_code -> va_s0:va_state -> dst:va_operand_vec_opr ->
  src1:va_operand_vec_opr -> src2:va_operand_vec_opr
  -> Ghost (va_state & va_fuel)
  (requires (va_require_total va_b0 (va_code_Vslw dst src1 src2) va_s0 /\ va_is_dst_vec_opr dst
    va_s0 /\ va_is_src_vec_opr src1 va_s0 /\ va_is_src_vec_opr src2 va_s0 /\ va_get_ok va_s0))
  (ensures (fun (va_sM, va_fM) -> va_ensure_total va_b0 va_s0 va_sM va_fM /\ va_get_ok va_sM /\
    va_eval_vec_opr va_sM dst == Vale.Def.Words_s.Mkfour #Vale.Def.Types_s.nat32
    (Vale.Arch.Types.ishl32 (Vale.Def.Words_s.__proj__Mkfour__item__lo0 (va_eval_vec_opr va_s0
    src1)) (Vale.Def.Words_s.__proj__Mkfour__item__lo0 (va_eval_vec_opr va_s0 src2) `op_Modulus`
    32)) (Vale.Arch.Types.ishl32 (Vale.Def.Words_s.__proj__Mkfour__item__lo1 (va_eval_vec_opr va_s0
    src1)) (Vale.Def.Words_s.__proj__Mkfour__item__lo1 (va_eval_vec_opr va_s0 src2) `op_Modulus`
    32)) (Vale.Arch.Types.ishl32 (Vale.Def.Words_s.__proj__Mkfour__item__hi2 (va_eval_vec_opr va_s0
    src1)) (Vale.Def.Words_s.__proj__Mkfour__item__hi2 (va_eval_vec_opr va_s0 src2) `op_Modulus`
    32)) (Vale.Arch.Types.ishl32 (Vale.Def.Words_s.__proj__Mkfour__item__hi3 (va_eval_vec_opr va_s0
    src1)) (Vale.Def.Words_s.__proj__Mkfour__item__hi3 (va_eval_vec_opr va_s0 src2) `op_Modulus`
    32)) /\ va_state_eq va_sM (va_update_ok va_sM (va_update_operand_vec_opr dst va_sM va_s0))))
[@ va_qattr]
let va_wp_Vslw (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)) : Type0 =
  (va_is_dst_vec_opr dst va_s0 /\ va_is_src_vec_opr src1 va_s0 /\ va_is_src_vec_opr src2 va_s0 /\
    va_get_ok va_s0 /\ (forall (va_x_dst:va_value_vec_opr) . let va_sM = va_upd_operand_vec_opr dst
    va_x_dst va_s0 in va_get_ok va_sM /\ va_eval_vec_opr va_sM dst == Vale.Def.Words_s.Mkfour
    #Vale.Def.Types_s.nat32 (Vale.Arch.Types.ishl32 (Vale.Def.Words_s.__proj__Mkfour__item__lo0
    (va_eval_vec_opr va_s0 src1)) (Vale.Def.Words_s.__proj__Mkfour__item__lo0 (va_eval_vec_opr
    va_s0 src2) `op_Modulus` 32)) (Vale.Arch.Types.ishl32
    (Vale.Def.Words_s.__proj__Mkfour__item__lo1 (va_eval_vec_opr va_s0 src1))
    (Vale.Def.Words_s.__proj__Mkfour__item__lo1 (va_eval_vec_opr va_s0 src2) `op_Modulus` 32))
    (Vale.Arch.Types.ishl32 (Vale.Def.Words_s.__proj__Mkfour__item__hi2 (va_eval_vec_opr va_s0
    src1)) (Vale.Def.Words_s.__proj__Mkfour__item__hi2 (va_eval_vec_opr va_s0 src2) `op_Modulus`
    32)) (Vale.Arch.Types.ishl32 (Vale.Def.Words_s.__proj__Mkfour__item__hi3 (va_eval_vec_opr va_s0
    src1)) (Vale.Def.Words_s.__proj__Mkfour__item__hi3 (va_eval_vec_opr va_s0 src2) `op_Modulus`
    32)) ==> va_k va_sM (())))

val va_wpProof_Vslw : 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_Vslw dst src1 src2 va_s0 va_k))
  (ensures (fun (va_sM, va_f0, va_g) -> va_t_ensure (va_code_Vslw dst src1 src2) ([va_mod_vec_opr
    dst]) va_s0 va_k ((va_sM, va_f0, va_g))))
[@ "opaque_to_smt" va_qattr]
let va_quick_Vslw (dst:va_operand_vec_opr) (src1:va_operand_vec_opr) (src2:va_operand_vec_opr) :
  (va_quickCode unit (va_code_Vslw dst src1 src2)) =
  (va_QProc (va_code_Vslw dst src1 src2) ([va_mod_vec_opr dst]) (va_wp_Vslw dst src1 src2)
    (va_wpProof_Vslw dst src1 src2))
//--
//-- Vsrw

val va_code_Vsrw : dst:va_operand_vec_opr -> src1:va_operand_vec_opr -> src2:va_operand_vec_opr ->
  Tot va_code

val va_codegen_success_Vsrw : dst:va_operand_vec_opr -> src1:va_operand_vec_opr ->
  src2:va_operand_vec_opr -> Tot va_pbool

val va_lemma_Vsrw : va_b0:va_code -> va_s0:va_state -> dst:va_operand_vec_opr ->
  src1:va_operand_vec_opr -> src2:va_operand_vec_opr
  -> Ghost (va_state & va_fuel)
  (requires (va_require_total va_b0 (va_code_Vsrw dst src1 src2) va_s0 /\ va_is_dst_vec_opr dst
    va_s0 /\ va_is_src_vec_opr src1 va_s0 /\ va_is_src_vec_opr src2 va_s0 /\ va_get_ok va_s0))
  (ensures (fun (va_sM, va_fM) -> va_ensure_total va_b0 va_s0 va_sM va_fM /\ va_get_ok va_sM /\
    va_eval_vec_opr va_sM dst == Vale.Def.Words_s.Mkfour #Vale.Def.Types_s.nat32
    (Vale.Arch.Types.ishr32 (Vale.Def.Words_s.__proj__Mkfour__item__lo0 (va_eval_vec_opr va_s0
    src1)) (Vale.Def.Words_s.__proj__Mkfour__item__lo0 (va_eval_vec_opr va_s0 src2) `op_Modulus`
    32)) (Vale.Arch.Types.ishr32 (Vale.Def.Words_s.__proj__Mkfour__item__lo1 (va_eval_vec_opr va_s0
    src1)) (Vale.Def.Words_s.__proj__Mkfour__item__lo1 (va_eval_vec_opr va_s0 src2) `op_Modulus`
    32)) (Vale.Arch.Types.ishr32 (Vale.Def.Words_s.__proj__Mkfour__item__hi2 (va_eval_vec_opr va_s0
    src1)) (Vale.Def.Words_s.__proj__Mkfour__item__hi2 (va_eval_vec_opr va_s0 src2) `op_Modulus`
    32)) (Vale.Arch.Types.ishr32 (Vale.Def.Words_s.__proj__Mkfour__item__hi3 (va_eval_vec_opr va_s0
    src1)) (Vale.Def.Words_s.__proj__Mkfour__item__hi3 (va_eval_vec_opr va_s0 src2) `op_Modulus`
    32)) /\ va_state_eq va_sM (va_update_ok va_sM (va_update_operand_vec_opr dst va_sM va_s0))))
[@ va_qattr]
let va_wp_Vsrw (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)) : Type0 =
  (va_is_dst_vec_opr dst va_s0 /\ va_is_src_vec_opr src1 va_s0 /\ va_is_src_vec_opr src2 va_s0 /\
    va_get_ok va_s0 /\ (forall (va_x_dst:va_value_vec_opr) . let va_sM = va_upd_operand_vec_opr dst
    va_x_dst va_s0 in va_get_ok va_sM /\ va_eval_vec_opr va_sM dst == Vale.Def.Words_s.Mkfour
    #Vale.Def.Types_s.nat32 (Vale.Arch.Types.ishr32 (Vale.Def.Words_s.__proj__Mkfour__item__lo0
    (va_eval_vec_opr va_s0 src1)) (Vale.Def.Words_s.__proj__Mkfour__item__lo0 (va_eval_vec_opr
    va_s0 src2) `op_Modulus` 32)) (Vale.Arch.Types.ishr32
    (Vale.Def.Words_s.__proj__Mkfour__item__lo1 (va_eval_vec_opr va_s0 src1))
    (Vale.Def.Words_s.__proj__Mkfour__item__lo1 (va_eval_vec_opr va_s0 src2) `op_Modulus` 32))
    (Vale.Arch.Types.ishr32 (Vale.Def.Words_s.__proj__Mkfour__item__hi2 (va_eval_vec_opr va_s0
    src1)) (Vale.Def.Words_s.__proj__Mkfour__item__hi2 (va_eval_vec_opr va_s0 src2) `op_Modulus`
    32)) (Vale.Arch.Types.ishr32 (Vale.Def.Words_s.__proj__Mkfour__item__hi3 (va_eval_vec_opr va_s0
    src1)) (Vale.Def.Words_s.__proj__Mkfour__item__hi3 (va_eval_vec_opr va_s0 src2) `op_Modulus`
    32)) ==> va_k va_sM (())))

val va_wpProof_Vsrw : 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_Vsrw dst src1 src2 va_s0 va_k))
  (ensures (fun (va_sM, va_f0, va_g) -> va_t_ensure (va_code_Vsrw dst src1 src2) ([va_mod_vec_opr
    dst]) va_s0 va_k ((va_sM, va_f0, va_g))))
[@ "opaque_to_smt" va_qattr]
let va_quick_Vsrw (dst:va_operand_vec_opr) (src1:va_operand_vec_opr) (src2:va_operand_vec_opr) :
  (va_quickCode unit (va_code_Vsrw dst src1 src2)) =
  (va_QProc (va_code_Vsrw dst src1 src2) ([va_mod_vec_opr dst]) (va_wp_Vsrw dst src1 src2)
    (va_wpProof_Vsrw dst src1 src2))
//--
//-- Vsl

val va_code_Vsl : dst:va_operand_vec_opr -> src1:va_operand_vec_opr -> src2:va_operand_vec_opr ->
  Tot va_code

val va_codegen_success_Vsl : dst:va_operand_vec_opr -> src1:va_operand_vec_opr ->
  src2:va_operand_vec_opr -> Tot va_pbool

val va_lemma_Vsl : va_b0:va_code -> va_s0:va_state -> dst:va_operand_vec_opr ->
  src1:va_operand_vec_opr -> src2:va_operand_vec_opr
  -> Ghost (va_state & va_fuel)
  (requires (va_require_total va_b0 (va_code_Vsl dst src1 src2) va_s0 /\ va_is_dst_vec_opr dst
    va_s0 /\ va_is_src_vec_opr src1 va_s0 /\ va_is_src_vec_opr src2 va_s0 /\ va_get_ok va_s0 /\
    (let sh = FStar.Seq.Base.index #nat8 (Vale.Def.Types_s.nat32_to_be_bytes
    (Vale.Def.Words_s.__proj__Mkfour__item__lo0 (va_eval_vec_opr va_s0 src2))) 3 `op_Modulus` 8 in
    let chk = fun (v:nat32) (sh:nat8) -> let bytes = Vale.Def.Types_s.nat32_to_be_bytes v in l_and
    (l_and (l_and (sh = FStar.Seq.Base.index #nat8 bytes 3 `op_Modulus` 8) (sh =
    FStar.Seq.Base.index #nat8 bytes 2 `op_Modulus` 8)) (sh = FStar.Seq.Base.index #nat8 bytes 1
    `op_Modulus` 8)) (sh = FStar.Seq.Base.index #nat8 bytes 0 `op_Modulus` 8) in l_and (l_and
    (l_and (chk (Vale.Def.Words_s.__proj__Mkfour__item__lo0 (va_eval_vec_opr va_s0 src2)) sh) (chk
    (Vale.Def.Words_s.__proj__Mkfour__item__lo1 (va_eval_vec_opr va_s0 src2)) sh)) (chk
    (Vale.Def.Words_s.__proj__Mkfour__item__hi2 (va_eval_vec_opr va_s0 src2)) sh)) (chk
    (Vale.Def.Words_s.__proj__Mkfour__item__hi3 (va_eval_vec_opr va_s0 src2)) sh))))
  (ensures (fun (va_sM, va_fM) -> va_ensure_total va_b0 va_s0 va_sM va_fM /\ va_get_ok va_sM /\
    (let sh = FStar.Seq.Base.index #nat8 (Vale.Def.Types_s.nat32_to_be_bytes
    (Vale.Def.Words_s.__proj__Mkfour__item__lo0 (va_eval_vec_opr va_s0 src2))) 3 `op_Modulus` 8 in
    let l = Vale.Def.Words.Four_s.four_map #nat32 #Vale.Def.Words_s.nat32 (fun (i:nat32) ->
    Vale.Arch.Types.ishl32 i sh) (va_eval_vec_opr va_s0 src1) in let r =
    Vale.Def.Words.Four_s.four_map #nat32 #Vale.Def.Words_s.nat32 (fun (i:nat32) ->
    Vale.Arch.Types.ishr32 i (32 - sh)) (va_eval_vec_opr va_s0 src1) in va_eval_vec_opr va_sM dst
    == Vale.Def.Types_s.quad32_xor l (Vale.Def.Words_s.Mkfour #Vale.Def.Types_s.nat32 0
    (Vale.Def.Words_s.__proj__Mkfour__item__lo0 r) (Vale.Def.Words_s.__proj__Mkfour__item__lo1 r)
    (Vale.Def.Words_s.__proj__Mkfour__item__hi2 r))) /\ va_state_eq va_sM (va_update_ok va_sM
    (va_update_operand_vec_opr dst va_sM va_s0))))
[@ va_qattr]
let va_wp_Vsl (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)) : Type0 =
  (va_is_dst_vec_opr dst va_s0 /\ va_is_src_vec_opr src1 va_s0 /\ va_is_src_vec_opr src2 va_s0 /\
    va_get_ok va_s0 /\ (let sh = FStar.Seq.Base.index #nat8 (Vale.Def.Types_s.nat32_to_be_bytes
    (Vale.Def.Words_s.__proj__Mkfour__item__lo0 (va_eval_vec_opr va_s0 src2))) 3 `op_Modulus` 8 in
    let chk = fun (v:nat32) (sh:nat8) -> let bytes = Vale.Def.Types_s.nat32_to_be_bytes v in l_and
    (l_and (l_and (sh = FStar.Seq.Base.index #nat8 bytes 3 `op_Modulus` 8) (sh =
    FStar.Seq.Base.index #nat8 bytes 2 `op_Modulus` 8)) (sh = FStar.Seq.Base.index #nat8 bytes 1
    `op_Modulus` 8)) (sh = FStar.Seq.Base.index #nat8 bytes 0 `op_Modulus` 8) in l_and (l_and
    (l_and (chk (Vale.Def.Words_s.__proj__Mkfour__item__lo0 (va_eval_vec_opr va_s0 src2)) sh) (chk
    (Vale.Def.Words_s.__proj__Mkfour__item__lo1 (va_eval_vec_opr va_s0 src2)) sh)) (chk
    (Vale.Def.Words_s.__proj__Mkfour__item__hi2 (va_eval_vec_opr va_s0 src2)) sh)) (chk
    (Vale.Def.Words_s.__proj__Mkfour__item__hi3 (va_eval_vec_opr va_s0 src2)) sh)) /\ (forall
    (va_x_dst:va_value_vec_opr) . let va_sM = va_upd_operand_vec_opr dst va_x_dst va_s0 in
    va_get_ok va_sM /\ (let sh = FStar.Seq.Base.index #nat8 (Vale.Def.Types_s.nat32_to_be_bytes
    (Vale.Def.Words_s.__proj__Mkfour__item__lo0 (va_eval_vec_opr va_s0 src2))) 3 `op_Modulus` 8 in
    let l = Vale.Def.Words.Four_s.four_map #nat32 #Vale.Def.Words_s.nat32 (fun (i:nat32) ->
    Vale.Arch.Types.ishl32 i sh) (va_eval_vec_opr va_s0 src1) in let r =
    Vale.Def.Words.Four_s.four_map #nat32 #Vale.Def.Words_s.nat32 (fun (i:nat32) ->
    Vale.Arch.Types.ishr32 i (32 - sh)) (va_eval_vec_opr va_s0 src1) in va_eval_vec_opr va_sM dst
    == Vale.Def.Types_s.quad32_xor l (Vale.Def.Words_s.Mkfour #Vale.Def.Types_s.nat32 0
    (Vale.Def.Words_s.__proj__Mkfour__item__lo0 r) (Vale.Def.Words_s.__proj__Mkfour__item__lo1 r)
    (Vale.Def.Words_s.__proj__Mkfour__item__hi2 r))) ==> va_k va_sM (())))

val va_wpProof_Vsl : 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_Vsl dst src1 src2 va_s0 va_k))
  (ensures (fun (va_sM, va_f0, va_g) -> va_t_ensure (va_code_Vsl dst src1 src2) ([va_mod_vec_opr
    dst]) va_s0 va_k ((va_sM, va_f0, va_g))))
[@ "opaque_to_smt" va_qattr]
let va_quick_Vsl (dst:va_operand_vec_opr) (src1:va_operand_vec_opr) (src2:va_operand_vec_opr) :
  (va_quickCode unit (va_code_Vsl dst src1 src2)) =
  (va_QProc (va_code_Vsl dst src1 src2) ([va_mod_vec_opr dst]) (va_wp_Vsl dst src1 src2)
    (va_wpProof_Vsl dst src1 src2))
//--
//-- Vcmpequw

val va_code_Vcmpequw : dst:va_operand_vec_opr -> src1:va_operand_vec_opr -> src2:va_operand_vec_opr
  -> Tot va_code

val va_codegen_success_Vcmpequw : dst:va_operand_vec_opr -> src1:va_operand_vec_opr ->
  src2:va_operand_vec_opr -> Tot va_pbool

val va_lemma_Vcmpequw : va_b0:va_code -> va_s0:va_state -> dst:va_operand_vec_opr ->
  src1:va_operand_vec_opr -> src2:va_operand_vec_opr
  -> Ghost (va_state & va_fuel)
  (requires (va_require_total va_b0 (va_code_Vcmpequw dst src1 src2) va_s0 /\ va_is_dst_vec_opr dst
    va_s0 /\ va_is_src_vec_opr src1 va_s0 /\ va_is_src_vec_opr src2 va_s0 /\ va_get_ok va_s0))
  (ensures (fun (va_sM, va_fM) -> va_ensure_total va_b0 va_s0 va_sM va_fM /\ va_get_ok va_sM /\
    va_eval_vec_opr va_sM dst == Vale.Def.Words_s.Mkfour #Vale.Def.Types_s.nat32 (if
    (Vale.Def.Words_s.__proj__Mkfour__item__lo0 (va_eval_vec_opr va_s0 src1) =
    Vale.Def.Words_s.__proj__Mkfour__item__lo0 (va_eval_vec_opr va_s0 src2)) then 4294967295 else
    0) (if (Vale.Def.Words_s.__proj__Mkfour__item__lo1 (va_eval_vec_opr va_s0 src1) =
    Vale.Def.Words_s.__proj__Mkfour__item__lo1 (va_eval_vec_opr va_s0 src2)) then 4294967295 else
    0) (if (Vale.Def.Words_s.__proj__Mkfour__item__hi2 (va_eval_vec_opr va_s0 src1) =
    Vale.Def.Words_s.__proj__Mkfour__item__hi2 (va_eval_vec_opr va_s0 src2)) then 4294967295 else
    0) (if (Vale.Def.Words_s.__proj__Mkfour__item__hi3 (va_eval_vec_opr va_s0 src1) =
    Vale.Def.Words_s.__proj__Mkfour__item__hi3 (va_eval_vec_opr va_s0 src2)) then 4294967295 else
    0) /\ va_state_eq va_sM (va_update_ok va_sM (va_update_operand_vec_opr dst va_sM va_s0))))
[@ va_qattr]
let va_wp_Vcmpequw (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)) : Type0 =
  (va_is_dst_vec_opr dst va_s0 /\ va_is_src_vec_opr src1 va_s0 /\ va_is_src_vec_opr src2 va_s0 /\
    va_get_ok va_s0 /\ (forall (va_x_dst:va_value_vec_opr) . let va_sM = va_upd_operand_vec_opr dst
    va_x_dst va_s0 in va_get_ok va_sM /\ va_eval_vec_opr va_sM dst == Vale.Def.Words_s.Mkfour
    #Vale.Def.Types_s.nat32 (va_if (Vale.Def.Words_s.__proj__Mkfour__item__lo0 (va_eval_vec_opr
    va_s0 src1) = Vale.Def.Words_s.__proj__Mkfour__item__lo0 (va_eval_vec_opr va_s0 src2)) (fun _
    -> 4294967295) (fun _ -> 0)) (va_if (Vale.Def.Words_s.__proj__Mkfour__item__lo1
    (va_eval_vec_opr va_s0 src1) = Vale.Def.Words_s.__proj__Mkfour__item__lo1 (va_eval_vec_opr
    va_s0 src2)) (fun _ -> 4294967295) (fun _ -> 0)) (va_if
    (Vale.Def.Words_s.__proj__Mkfour__item__hi2 (va_eval_vec_opr va_s0 src1) =
    Vale.Def.Words_s.__proj__Mkfour__item__hi2 (va_eval_vec_opr va_s0 src2)) (fun _ -> 4294967295)
    (fun _ -> 0)) (va_if (Vale.Def.Words_s.__proj__Mkfour__item__hi3 (va_eval_vec_opr va_s0 src1) =
    Vale.Def.Words_s.__proj__Mkfour__item__hi3 (va_eval_vec_opr va_s0 src2)) (fun _ -> 4294967295)
    (fun _ -> 0)) ==> va_k va_sM (())))

val va_wpProof_Vcmpequw : 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_Vcmpequw dst src1 src2 va_s0 va_k))
  (ensures (fun (va_sM, va_f0, va_g) -> va_t_ensure (va_code_Vcmpequw dst src1 src2)
    ([va_mod_vec_opr dst]) va_s0 va_k ((va_sM, va_f0, va_g))))
[@ "opaque_to_smt" va_qattr]
let va_quick_Vcmpequw (dst:va_operand_vec_opr) (src1:va_operand_vec_opr) (src2:va_operand_vec_opr)
  : (va_quickCode unit (va_code_Vcmpequw dst src1 src2)) =
  (va_QProc (va_code_Vcmpequw dst src1 src2) ([va_mod_vec_opr dst]) (va_wp_Vcmpequw dst src1 src2)
    (va_wpProof_Vcmpequw dst src1 src2))
//--
//-- Vsldoi

val va_code_Vsldoi : dst:va_operand_vec_opr -> src1:va_operand_vec_opr -> src2:va_operand_vec_opr
  -> count:quad32bytes -> Tot va_code

val va_codegen_success_Vsldoi : dst:va_operand_vec_opr -> src1:va_operand_vec_opr ->
  src2:va_operand_vec_opr -> count:quad32bytes -> Tot va_pbool

val va_lemma_Vsldoi : va_b0:va_code -> va_s0:va_state -> dst:va_operand_vec_opr ->
  src1:va_operand_vec_opr -> src2:va_operand_vec_opr -> count:quad32bytes
  -> Ghost (va_state & va_fuel)
  (requires (va_require_total va_b0 (va_code_Vsldoi dst src1 src2 count) va_s0 /\ va_is_dst_vec_opr
    dst va_s0 /\ va_is_src_vec_opr src1 va_s0 /\ va_is_src_vec_opr src2 va_s0 /\ va_get_ok va_s0 /\
    (count == 4 \/ count == 8 \/ count == 12)))
  (ensures (fun (va_sM, va_fM) -> va_ensure_total va_b0 va_s0 va_sM va_fM /\ va_get_ok va_sM /\
    (count == 4 ==> va_eval_vec_opr va_sM dst == Vale.Def.Words_s.Mkfour #Vale.Def.Types_s.nat32
    (Vale.Def.Words_s.__proj__Mkfour__item__hi3 (va_eval_vec_opr va_s0 src2))
    (Vale.Def.Words_s.__proj__Mkfour__item__lo0 (va_eval_vec_opr va_s0 src1))
    (Vale.Def.Words_s.__proj__Mkfour__item__lo1 (va_eval_vec_opr va_s0 src1))
    (Vale.Def.Words_s.__proj__Mkfour__item__hi2 (va_eval_vec_opr va_s0 src1))) /\ (count == 8 ==>
    va_eval_vec_opr va_sM dst == Vale.Def.Words_s.Mkfour #Vale.Def.Types_s.nat32
    (Vale.Def.Words_s.__proj__Mkfour__item__hi2 (va_eval_vec_opr va_s0 src2))
    (Vale.Def.Words_s.__proj__Mkfour__item__hi3 (va_eval_vec_opr va_s0 src2))
    (Vale.Def.Words_s.__proj__Mkfour__item__lo0 (va_eval_vec_opr va_s0 src1))
    (Vale.Def.Words_s.__proj__Mkfour__item__lo1 (va_eval_vec_opr va_s0 src1))) /\ (count == 12 ==>
    va_eval_vec_opr va_sM dst == Vale.Def.Words_s.Mkfour #Vale.Def.Types_s.nat32
    (Vale.Def.Words_s.__proj__Mkfour__item__lo1 (va_eval_vec_opr va_s0 src2))
    (Vale.Def.Words_s.__proj__Mkfour__item__hi2 (va_eval_vec_opr va_s0 src2))
    (Vale.Def.Words_s.__proj__Mkfour__item__hi3 (va_eval_vec_opr va_s0 src2))
    (Vale.Def.Words_s.__proj__Mkfour__item__lo0 (va_eval_vec_opr va_s0 src1))) /\ va_state_eq va_sM
    (va_update_ok va_sM (va_update_operand_vec_opr dst va_sM va_s0))))
[@ va_qattr]
let va_wp_Vsldoi (dst:va_operand_vec_opr) (src1:va_operand_vec_opr) (src2:va_operand_vec_opr)
  (count:quad32bytes) (va_s0:va_state) (va_k:(va_state -> unit -> Type0)) : Type0 =
  (va_is_dst_vec_opr dst va_s0 /\ va_is_src_vec_opr src1 va_s0 /\ va_is_src_vec_opr src2 va_s0 /\
    va_get_ok va_s0 /\ (count == 4 \/ count == 8 \/ count == 12) /\ (forall
    (va_x_dst:va_value_vec_opr) . let va_sM = va_upd_operand_vec_opr dst va_x_dst va_s0 in
    va_get_ok va_sM /\ (count == 4 ==> va_eval_vec_opr va_sM dst == Vale.Def.Words_s.Mkfour
    #Vale.Def.Types_s.nat32 (Vale.Def.Words_s.__proj__Mkfour__item__hi3 (va_eval_vec_opr va_s0
    src2)) (Vale.Def.Words_s.__proj__Mkfour__item__lo0 (va_eval_vec_opr va_s0 src1))
    (Vale.Def.Words_s.__proj__Mkfour__item__lo1 (va_eval_vec_opr va_s0 src1))
    (Vale.Def.Words_s.__proj__Mkfour__item__hi2 (va_eval_vec_opr va_s0 src1))) /\ (count == 8 ==>
    va_eval_vec_opr va_sM dst == Vale.Def.Words_s.Mkfour #Vale.Def.Types_s.nat32
    (Vale.Def.Words_s.__proj__Mkfour__item__hi2 (va_eval_vec_opr va_s0 src2))
    (Vale.Def.Words_s.__proj__Mkfour__item__hi3 (va_eval_vec_opr va_s0 src2))
    (Vale.Def.Words_s.__proj__Mkfour__item__lo0 (va_eval_vec_opr va_s0 src1))
    (Vale.Def.Words_s.__proj__Mkfour__item__lo1 (va_eval_vec_opr va_s0 src1))) /\ (count == 12 ==>
    va_eval_vec_opr va_sM dst == Vale.Def.Words_s.Mkfour #Vale.Def.Types_s.nat32
    (Vale.Def.Words_s.__proj__Mkfour__item__lo1 (va_eval_vec_opr va_s0 src2))
    (Vale.Def.Words_s.__proj__Mkfour__item__hi2 (va_eval_vec_opr va_s0 src2))
    (Vale.Def.Words_s.__proj__Mkfour__item__hi3 (va_eval_vec_opr va_s0 src2))
    (Vale.Def.Words_s.__proj__Mkfour__item__lo0 (va_eval_vec_opr va_s0 src1))) ==> va_k va_sM (())))

val va_wpProof_Vsldoi : dst:va_operand_vec_opr -> src1:va_operand_vec_opr ->
  src2:va_operand_vec_opr -> count:quad32bytes -> va_s0:va_state -> va_k:(va_state -> unit -> Type0)
  -> Ghost (va_state & va_fuel & unit)
  (requires (va_t_require va_s0 /\ va_wp_Vsldoi dst src1 src2 count va_s0 va_k))
  (ensures (fun (va_sM, va_f0, va_g) -> va_t_ensure (va_code_Vsldoi dst src1 src2 count)
    ([va_mod_vec_opr dst]) va_s0 va_k ((va_sM, va_f0, va_g))))
[@ "opaque_to_smt" va_qattr]
let va_quick_Vsldoi (dst:va_operand_vec_opr) (src1:va_operand_vec_opr) (src2:va_operand_vec_opr)
  (count:quad32bytes) : (va_quickCode unit (va_code_Vsldoi dst src1 src2 count)) =
  (va_QProc (va_code_Vsldoi dst src1 src2 count) ([va_mod_vec_opr dst]) (va_wp_Vsldoi dst src1 src2
    count) (va_wpProof_Vsldoi dst src1 src2 count))
//--
//-- Vmrghw

val va_code_Vmrghw : dst:va_operand_vec_opr -> src1:va_operand_vec_opr -> src2:va_operand_vec_opr
  -> Tot va_code

val va_codegen_success_Vmrghw : dst:va_operand_vec_opr -> src1:va_operand_vec_opr ->
  src2:va_operand_vec_opr -> Tot va_pbool

val va_lemma_Vmrghw : va_b0:va_code -> va_s0:va_state -> dst:va_operand_vec_opr ->
  src1:va_operand_vec_opr -> src2:va_operand_vec_opr
  -> Ghost (va_state & va_fuel)
  (requires (va_require_total va_b0 (va_code_Vmrghw dst src1 src2) va_s0 /\ va_is_dst_vec_opr dst
    va_s0 /\ va_is_src_vec_opr src1 va_s0 /\ va_is_src_vec_opr src2 va_s0 /\ va_get_ok va_s0))
  (ensures (fun (va_sM, va_fM) -> va_ensure_total va_b0 va_s0 va_sM va_fM /\ va_get_ok va_sM /\
    va_eval_vec_opr va_sM dst == Vale.Def.Words_s.Mkfour #Vale.Def.Types_s.nat32
    (Vale.Def.Words_s.__proj__Mkfour__item__lo1 (va_eval_vec_opr va_s0 src2))
    (Vale.Def.Words_s.__proj__Mkfour__item__lo1 (va_eval_vec_opr va_s0 src1))
    (Vale.Def.Words_s.__proj__Mkfour__item__hi3 (va_eval_vec_opr va_s0 src2))
    (Vale.Def.Words_s.__proj__Mkfour__item__hi3 (va_eval_vec_opr va_s0 src1)) /\ va_state_eq va_sM
    (va_update_ok va_sM (va_update_operand_vec_opr dst va_sM va_s0))))
[@ va_qattr]
let va_wp_Vmrghw (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)) : Type0 =
  (va_is_dst_vec_opr dst va_s0 /\ va_is_src_vec_opr src1 va_s0 /\ va_is_src_vec_opr src2 va_s0 /\
    va_get_ok va_s0 /\ (forall (va_x_dst:va_value_vec_opr) . let va_sM = va_upd_operand_vec_opr dst
    va_x_dst va_s0 in va_get_ok va_sM /\ va_eval_vec_opr va_sM dst == Vale.Def.Words_s.Mkfour
    #Vale.Def.Types_s.nat32 (Vale.Def.Words_s.__proj__Mkfour__item__lo1 (va_eval_vec_opr va_s0
    src2)) (Vale.Def.Words_s.__proj__Mkfour__item__lo1 (va_eval_vec_opr va_s0 src1))
    (Vale.Def.Words_s.__proj__Mkfour__item__hi3 (va_eval_vec_opr va_s0 src2))
    (Vale.Def.Words_s.__proj__Mkfour__item__hi3 (va_eval_vec_opr va_s0 src1)) ==> va_k va_sM (())))

val va_wpProof_Vmrghw : 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_Vmrghw dst src1 src2 va_s0 va_k))
  (ensures (fun (va_sM, va_f0, va_g) -> va_t_ensure (va_code_Vmrghw dst src1 src2) ([va_mod_vec_opr
    dst]) va_s0 va_k ((va_sM, va_f0, va_g))))
[@ "opaque_to_smt" va_qattr]
let va_quick_Vmrghw (dst:va_operand_vec_opr) (src1:va_operand_vec_opr) (src2:va_operand_vec_opr) :
  (va_quickCode unit (va_code_Vmrghw dst src1 src2)) =
  (va_QProc (va_code_Vmrghw dst src1 src2) ([va_mod_vec_opr dst]) (va_wp_Vmrghw dst src1 src2)
    (va_wpProof_Vmrghw dst src1 src2))
//--
//-- Xxmrghd

val va_code_Xxmrghd : dst:va_operand_vec_opr -> src1:va_operand_vec_opr -> src2:va_operand_vec_opr
  -> Tot va_code

val va_codegen_success_Xxmrghd : dst:va_operand_vec_opr -> src1:va_operand_vec_opr ->
  src2:va_operand_vec_opr -> Tot va_pbool

val va_lemma_Xxmrghd : va_b0:va_code -> va_s0:va_state -> dst:va_operand_vec_opr ->
  src1:va_operand_vec_opr -> src2:va_operand_vec_opr
  -> Ghost (va_state & va_fuel)
  (requires (va_require_total va_b0 (va_code_Xxmrghd dst src1 src2) va_s0 /\ va_is_dst_vec_opr dst
    va_s0 /\ va_is_src_vec_opr src1 va_s0 /\ va_is_src_vec_opr src2 va_s0 /\ va_get_ok va_s0))
  (ensures (fun (va_sM, va_fM) -> va_ensure_total va_b0 va_s0 va_sM va_fM /\ va_get_ok va_sM /\
    va_eval_vec_opr va_sM dst == Vale.Def.Words_s.Mkfour #Vale.Def.Types_s.nat32
    (Vale.Def.Words_s.__proj__Mkfour__item__hi2 (va_eval_vec_opr va_s0 src2))
    (Vale.Def.Words_s.__proj__Mkfour__item__hi3 (va_eval_vec_opr va_s0 src2))
    (Vale.Def.Words_s.__proj__Mkfour__item__hi2 (va_eval_vec_opr va_s0 src1))
    (Vale.Def.Words_s.__proj__Mkfour__item__hi3 (va_eval_vec_opr va_s0 src1)) /\ va_state_eq va_sM
    (va_update_ok va_sM (va_update_operand_vec_opr dst va_sM va_s0))))
[@ va_qattr]
let va_wp_Xxmrghd (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)) : Type0 =
  (va_is_dst_vec_opr dst va_s0 /\ va_is_src_vec_opr src1 va_s0 /\ va_is_src_vec_opr src2 va_s0 /\
    va_get_ok va_s0 /\ (forall (va_x_dst:va_value_vec_opr) . let va_sM = va_upd_operand_vec_opr dst
    va_x_dst va_s0 in va_get_ok va_sM /\ va_eval_vec_opr va_sM dst == Vale.Def.Words_s.Mkfour
    #Vale.Def.Types_s.nat32 (Vale.Def.Words_s.__proj__Mkfour__item__hi2 (va_eval_vec_opr va_s0
    src2)) (Vale.Def.Words_s.__proj__Mkfour__item__hi3 (va_eval_vec_opr va_s0 src2))
    (Vale.Def.Words_s.__proj__Mkfour__item__hi2 (va_eval_vec_opr va_s0 src1))
    (Vale.Def.Words_s.__proj__Mkfour__item__hi3 (va_eval_vec_opr va_s0 src1)) ==> va_k va_sM (())))

val va_wpProof_Xxmrghd : 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_Xxmrghd dst src1 src2 va_s0 va_k))
  (ensures (fun (va_sM, va_f0, va_g) -> va_t_ensure (va_code_Xxmrghd dst src1 src2)
    ([va_mod_vec_opr dst]) va_s0 va_k ((va_sM, va_f0, va_g))))
[@ "opaque_to_smt" va_qattr]
let va_quick_Xxmrghd (dst:va_operand_vec_opr) (src1:va_operand_vec_opr) (src2:va_operand_vec_opr) :
  (va_quickCode unit (va_code_Xxmrghd dst src1 src2)) =
  (va_QProc (va_code_Xxmrghd dst src1 src2) ([va_mod_vec_opr dst]) (va_wp_Xxmrghd dst src1 src2)
    (va_wpProof_Xxmrghd dst src1 src2))
//--
//-- Vsel

val va_code_Vsel : dst:va_operand_vec_opr -> src1:va_operand_vec_opr -> src2:va_operand_vec_opr ->
  sel:va_operand_vec_opr -> Tot va_code

val va_codegen_success_Vsel : dst:va_operand_vec_opr -> src1:va_operand_vec_opr ->
  src2:va_operand_vec_opr -> sel:va_operand_vec_opr -> Tot va_pbool

val va_lemma_Vsel : va_b0:va_code -> va_s0:va_state -> dst:va_operand_vec_opr ->
  src1:va_operand_vec_opr -> src2:va_operand_vec_opr -> sel:va_operand_vec_opr
  -> Ghost (va_state & va_fuel)
  (requires (va_require_total va_b0 (va_code_Vsel dst src1 src2 sel) va_s0 /\ va_is_dst_vec_opr dst
    va_s0 /\ va_is_src_vec_opr src1 va_s0 /\ va_is_src_vec_opr src2 va_s0 /\ va_is_src_vec_opr sel
    va_s0 /\ va_get_ok va_s0))
  (ensures (fun (va_sM, va_fM) -> va_ensure_total va_b0 va_s0 va_sM va_fM /\ va_get_ok va_sM /\
    Vale.Def.Words_s.__proj__Mkfour__item__lo0 (va_eval_vec_opr va_sM dst) == Vale.Def.Sel.isel32
    (Vale.Def.Words_s.__proj__Mkfour__item__lo0 (va_eval_vec_opr va_s0 src2))
    (Vale.Def.Words_s.__proj__Mkfour__item__lo0 (va_eval_vec_opr va_s0 src1))
    (Vale.Def.Words_s.__proj__Mkfour__item__lo0 (va_eval_vec_opr va_s0 sel)) /\
    Vale.Def.Words_s.__proj__Mkfour__item__lo1 (va_eval_vec_opr va_sM dst) == Vale.Def.Sel.isel32
    (Vale.Def.Words_s.__proj__Mkfour__item__lo1 (va_eval_vec_opr va_s0 src2))
    (Vale.Def.Words_s.__proj__Mkfour__item__lo1 (va_eval_vec_opr va_s0 src1))
    (Vale.Def.Words_s.__proj__Mkfour__item__lo1 (va_eval_vec_opr va_s0 sel)) /\
    Vale.Def.Words_s.__proj__Mkfour__item__hi2 (va_eval_vec_opr va_sM dst) == Vale.Def.Sel.isel32
    (Vale.Def.Words_s.__proj__Mkfour__item__hi2 (va_eval_vec_opr va_s0 src2))
    (Vale.Def.Words_s.__proj__Mkfour__item__hi2 (va_eval_vec_opr va_s0 src1))
    (Vale.Def.Words_s.__proj__Mkfour__item__hi2 (va_eval_vec_opr va_s0 sel)) /\
    Vale.Def.Words_s.__proj__Mkfour__item__hi3 (va_eval_vec_opr va_sM dst) == Vale.Def.Sel.isel32
    (Vale.Def.Words_s.__proj__Mkfour__item__hi3 (va_eval_vec_opr va_s0 src2))
    (Vale.Def.Words_s.__proj__Mkfour__item__hi3 (va_eval_vec_opr va_s0 src1))
    (Vale.Def.Words_s.__proj__Mkfour__item__hi3 (va_eval_vec_opr va_s0 sel)) /\ va_state_eq va_sM
    (va_update_ok va_sM (va_update_operand_vec_opr dst va_sM va_s0))))
[@ va_qattr]
let va_wp_Vsel (dst:va_operand_vec_opr) (src1:va_operand_vec_opr) (src2:va_operand_vec_opr)
  (sel:va_operand_vec_opr) (va_s0:va_state) (va_k:(va_state -> unit -> Type0)) : Type0 =
  (va_is_dst_vec_opr dst va_s0 /\ va_is_src_vec_opr src1 va_s0 /\ va_is_src_vec_opr src2 va_s0 /\
    va_is_src_vec_opr sel va_s0 /\ va_get_ok va_s0 /\ (forall (va_x_dst:va_value_vec_opr) . let
    va_sM = va_upd_operand_vec_opr dst va_x_dst va_s0 in va_get_ok va_sM /\
    Vale.Def.Words_s.__proj__Mkfour__item__lo0 (va_eval_vec_opr va_sM dst) == Vale.Def.Sel.isel32
    (Vale.Def.Words_s.__proj__Mkfour__item__lo0 (va_eval_vec_opr va_s0 src2))
    (Vale.Def.Words_s.__proj__Mkfour__item__lo0 (va_eval_vec_opr va_s0 src1))
    (Vale.Def.Words_s.__proj__Mkfour__item__lo0 (va_eval_vec_opr va_s0 sel)) /\
    Vale.Def.Words_s.__proj__Mkfour__item__lo1 (va_eval_vec_opr va_sM dst) == Vale.Def.Sel.isel32
    (Vale.Def.Words_s.__proj__Mkfour__item__lo1 (va_eval_vec_opr va_s0 src2))
    (Vale.Def.Words_s.__proj__Mkfour__item__lo1 (va_eval_vec_opr va_s0 src1))
    (Vale.Def.Words_s.__proj__Mkfour__item__lo1 (va_eval_vec_opr va_s0 sel)) /\
    Vale.Def.Words_s.__proj__Mkfour__item__hi2 (va_eval_vec_opr va_sM dst) == Vale.Def.Sel.isel32
    (Vale.Def.Words_s.__proj__Mkfour__item__hi2 (va_eval_vec_opr va_s0 src2))
    (Vale.Def.Words_s.__proj__Mkfour__item__hi2 (va_eval_vec_opr va_s0 src1))
    (Vale.Def.Words_s.__proj__Mkfour__item__hi2 (va_eval_vec_opr va_s0 sel)) /\
    Vale.Def.Words_s.__proj__Mkfour__item__hi3 (va_eval_vec_opr va_sM dst) == Vale.Def.Sel.isel32
    (Vale.Def.Words_s.__proj__Mkfour__item__hi3 (va_eval_vec_opr va_s0 src2))
    (Vale.Def.Words_s.__proj__Mkfour__item__hi3 (va_eval_vec_opr va_s0 src1))
    (Vale.Def.Words_s.__proj__Mkfour__item__hi3 (va_eval_vec_opr va_s0 sel)) ==> va_k va_sM (())))

val va_wpProof_Vsel : dst:va_operand_vec_opr -> src1:va_operand_vec_opr -> src2:va_operand_vec_opr
  -> sel: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_Vsel dst src1 src2 sel va_s0 va_k))
  (ensures (fun (va_sM, va_f0, va_g) -> va_t_ensure (va_code_Vsel dst src1 src2 sel)
    ([va_mod_vec_opr dst]) va_s0 va_k ((va_sM, va_f0, va_g))))
[@ "opaque_to_smt" va_qattr]
let va_quick_Vsel (dst:va_operand_vec_opr) (src1:va_operand_vec_opr) (src2:va_operand_vec_opr)
  (sel:va_operand_vec_opr) : (va_quickCode unit (va_code_Vsel dst src1 src2 sel)) =
  (va_QProc (va_code_Vsel dst src1 src2 sel) ([va_mod_vec_opr dst]) (va_wp_Vsel dst src1 src2 sel)
    (va_wpProof_Vsel dst src1 src2 sel))
//--
//-- Vspltw

val va_code_Vspltw : dst:va_operand_vec_opr -> src:va_operand_vec_opr -> uim:nat2 -> Tot va_code

val va_codegen_success_Vspltw : dst:va_operand_vec_opr -> src:va_operand_vec_opr -> uim:nat2 -> Tot
  va_pbool

val va_lemma_Vspltw : va_b0:va_code -> va_s0:va_state -> dst:va_operand_vec_opr ->
  src:va_operand_vec_opr -> uim:nat2
  -> Ghost (va_state & va_fuel)
  (requires (va_require_total va_b0 (va_code_Vspltw dst src uim) va_s0 /\ va_is_dst_vec_opr dst
    va_s0 /\ va_is_src_vec_opr src va_s0 /\ va_get_ok va_s0))
  (ensures (fun (va_sM, va_fM) -> va_ensure_total va_b0 va_s0 va_sM va_fM /\ va_get_ok va_sM /\
    (uim == 0 ==> va_eval_vec_opr va_sM dst == Vale.Def.Words_s.Mkfour #Vale.Def.Types_s.nat32
    (Vale.Def.Words_s.__proj__Mkfour__item__hi3 (va_eval_vec_opr va_s0 src))
    (Vale.Def.Words_s.__proj__Mkfour__item__hi3 (va_eval_vec_opr va_s0 src))
    (Vale.Def.Words_s.__proj__Mkfour__item__hi3 (va_eval_vec_opr va_s0 src))
    (Vale.Def.Words_s.__proj__Mkfour__item__hi3 (va_eval_vec_opr va_s0 src))) /\ (uim == 1 ==>
    va_eval_vec_opr va_sM dst == Vale.Def.Words_s.Mkfour #Vale.Def.Types_s.nat32
    (Vale.Def.Words_s.__proj__Mkfour__item__hi2 (va_eval_vec_opr va_s0 src))
    (Vale.Def.Words_s.__proj__Mkfour__item__hi2 (va_eval_vec_opr va_s0 src))
    (Vale.Def.Words_s.__proj__Mkfour__item__hi2 (va_eval_vec_opr va_s0 src))
    (Vale.Def.Words_s.__proj__Mkfour__item__hi2 (va_eval_vec_opr va_s0 src))) /\ (uim == 2 ==>
    va_eval_vec_opr va_sM dst == Vale.Def.Words_s.Mkfour #Vale.Def.Types_s.nat32
    (Vale.Def.Words_s.__proj__Mkfour__item__lo1 (va_eval_vec_opr va_s0 src))
    (Vale.Def.Words_s.__proj__Mkfour__item__lo1 (va_eval_vec_opr va_s0 src))
    (Vale.Def.Words_s.__proj__Mkfour__item__lo1 (va_eval_vec_opr va_s0 src))
    (Vale.Def.Words_s.__proj__Mkfour__item__lo1 (va_eval_vec_opr va_s0 src))) /\ (uim == 3 ==>
    va_eval_vec_opr va_sM dst == Vale.Def.Words_s.Mkfour #Vale.Def.Types_s.nat32
    (Vale.Def.Words_s.__proj__Mkfour__item__lo0 (va_eval_vec_opr va_s0 src))
    (Vale.Def.Words_s.__proj__Mkfour__item__lo0 (va_eval_vec_opr va_s0 src))
    (Vale.Def.Words_s.__proj__Mkfour__item__lo0 (va_eval_vec_opr va_s0 src))
    (Vale.Def.Words_s.__proj__Mkfour__item__lo0 (va_eval_vec_opr va_s0 src))) /\ va_state_eq va_sM
    (va_update_ok va_sM (va_update_operand_vec_opr dst va_sM va_s0))))
[@ va_qattr]
let va_wp_Vspltw (dst:va_operand_vec_opr) (src:va_operand_vec_opr) (uim:nat2) (va_s0:va_state)
  (va_k:(va_state -> unit -> Type0)) : Type0 =
  (va_is_dst_vec_opr dst va_s0 /\ va_is_src_vec_opr src va_s0 /\ va_get_ok va_s0 /\ (forall
    (va_x_dst:va_value_vec_opr) . let va_sM = va_upd_operand_vec_opr dst va_x_dst va_s0 in
    va_get_ok va_sM /\ (uim == 0 ==> va_eval_vec_opr va_sM dst == Vale.Def.Words_s.Mkfour
    #Vale.Def.Types_s.nat32 (Vale.Def.Words_s.__proj__Mkfour__item__hi3 (va_eval_vec_opr va_s0
    src)) (Vale.Def.Words_s.__proj__Mkfour__item__hi3 (va_eval_vec_opr va_s0 src))
    (Vale.Def.Words_s.__proj__Mkfour__item__hi3 (va_eval_vec_opr va_s0 src))
    (Vale.Def.Words_s.__proj__Mkfour__item__hi3 (va_eval_vec_opr va_s0 src))) /\ (uim == 1 ==>
    va_eval_vec_opr va_sM dst == Vale.Def.Words_s.Mkfour #Vale.Def.Types_s.nat32
    (Vale.Def.Words_s.__proj__Mkfour__item__hi2 (va_eval_vec_opr va_s0 src))
    (Vale.Def.Words_s.__proj__Mkfour__item__hi2 (va_eval_vec_opr va_s0 src))
    (Vale.Def.Words_s.__proj__Mkfour__item__hi2 (va_eval_vec_opr va_s0 src))
    (Vale.Def.Words_s.__proj__Mkfour__item__hi2 (va_eval_vec_opr va_s0 src))) /\ (uim == 2 ==>
    va_eval_vec_opr va_sM dst == Vale.Def.Words_s.Mkfour #Vale.Def.Types_s.nat32
    (Vale.Def.Words_s.__proj__Mkfour__item__lo1 (va_eval_vec_opr va_s0 src))
    (Vale.Def.Words_s.__proj__Mkfour__item__lo1 (va_eval_vec_opr va_s0 src))
    (Vale.Def.Words_s.__proj__Mkfour__item__lo1 (va_eval_vec_opr va_s0 src))
    (Vale.Def.Words_s.__proj__Mkfour__item__lo1 (va_eval_vec_opr va_s0 src))) /\ (uim == 3 ==>
    va_eval_vec_opr va_sM dst == Vale.Def.Words_s.Mkfour #Vale.Def.Types_s.nat32
    (Vale.Def.Words_s.__proj__Mkfour__item__lo0 (va_eval_vec_opr va_s0 src))
    (Vale.Def.Words_s.__proj__Mkfour__item__lo0 (va_eval_vec_opr va_s0 src))
    (Vale.Def.Words_s.__proj__Mkfour__item__lo0 (va_eval_vec_opr va_s0 src))
    (Vale.Def.Words_s.__proj__Mkfour__item__lo0 (va_eval_vec_opr va_s0 src))) ==> va_k va_sM (())))

val va_wpProof_Vspltw : dst:va_operand_vec_opr -> src:va_operand_vec_opr -> uim:nat2 ->
  va_s0:va_state -> va_k:(va_state -> unit -> Type0)
  -> Ghost (va_state & va_fuel & unit)
  (requires (va_t_require va_s0 /\ va_wp_Vspltw dst src uim va_s0 va_k))
  (ensures (fun (va_sM, va_f0, va_g) -> va_t_ensure (va_code_Vspltw dst src uim) ([va_mod_vec_opr
    dst]) va_s0 va_k ((va_sM, va_f0, va_g))))
[@ "opaque_to_smt" va_qattr]
let va_quick_Vspltw (dst:va_operand_vec_opr) (src:va_operand_vec_opr) (uim:nat2) : (va_quickCode
val va_quick_Vspltw (dst src: va_operand_vec_opr) (uim: nat2)
    : (va_quickCode unit (va_code_Vspltw dst src uim))

    dst: Vale.PPC64LE.Decls.va_operand_vec_opr ->
    src: Vale.PPC64LE.Decls.va_operand_vec_opr ->
    uim: Vale.Def.Words_s.nat2
  -> Vale.PPC64LE.QuickCode.va_quickCode Prims.unit
      (Vale.PPC64LE.InsVector.va_code_Vspltw dst src uim)