val va_quick_RotWord (dst src1 src2: va_operand_vec_opr)
    : (va_quickCode unit (va_code_RotWord dst src1 src2))
let va_quick_RotWord (dst:va_operand_vec_opr) (src1:va_operand_vec_opr) (src2:va_operand_vec_opr) :
  (va_quickCode unit (va_code_RotWord dst src1 src2)) =
  (va_QProc (va_code_RotWord dst src1 src2) ([va_mod_vec_opr dst]) (va_wp_RotWord dst src1 src2)
    (va_wpProof_RotWord dst src1 src2))
val va_quick_RotWord (dst src1 src2: va_operand_vec_opr)
    : (va_quickCode unit (va_code_RotWord dst src1 src2))
let va_quick_RotWord (dst src1 src2: va_operand_vec_opr)
    : (va_quickCode unit (va_code_RotWord dst src1 src2)) =
(va_QProc (va_code_RotWord dst src1 src2)
    ([va_mod_vec_opr dst])
    (va_wp_RotWord dst src1 src2)
    (va_wpProof_RotWord dst src1 src2))
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.PPC64LE.QuickCode.va_QProc Prims.unit Vale.PPC64LE.InsVector.va_code_RotWord Prims.Cons Vale.PPC64LE.QuickCode.mod_t Vale.PPC64LE.QuickCode.va_mod_vec_opr Prims.Nil Vale.PPC64LE.InsVector.va_wp_RotWord Vale.PPC64LE.InsVector.va_wpProof_RotWord 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
  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))
//--
//-- Vspltisw

val va_code_Vspltisw : dst:va_operand_vec_opr -> src:sim -> Tot va_code

val va_codegen_success_Vspltisw : dst:va_operand_vec_opr -> src:sim -> Tot va_pbool

val va_lemma_Vspltisw : va_b0:va_code -> va_s0:va_state -> dst:va_operand_vec_opr -> src:sim
  -> Ghost (va_state & va_fuel)
  (requires (va_require_total va_b0 (va_code_Vspltisw dst src) va_s0 /\ va_is_dst_vec_opr dst 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 /\
    (let src_nat32 = Vale.PPC64LE.Machine_s.int_to_nat32 src in va_eval_vec_opr va_sM dst ==
    Vale.Def.Words_s.Mkfour #Vale.Def.Types_s.nat32 src_nat32 src_nat32 src_nat32 src_nat32) /\
    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_Vspltisw (dst:va_operand_vec_opr) (src:sim) (va_s0:va_state) (va_k:(va_state -> unit ->
  Type0)) : Type0 =
  (va_is_dst_vec_opr dst 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 /\ (let src_nat32 =
    Vale.PPC64LE.Machine_s.int_to_nat32 src in va_eval_vec_opr va_sM dst == Vale.Def.Words_s.Mkfour
    #Vale.Def.Types_s.nat32 src_nat32 src_nat32 src_nat32 src_nat32) ==> va_k va_sM (())))

val va_wpProof_Vspltisw : dst:va_operand_vec_opr -> src:sim -> va_s0:va_state -> va_k:(va_state ->
  unit -> Type0)
  -> Ghost (va_state & va_fuel & unit)
  (requires (va_t_require va_s0 /\ va_wp_Vspltisw dst src va_s0 va_k))
  (ensures (fun (va_sM, va_f0, va_g) -> va_t_ensure (va_code_Vspltisw 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_Vspltisw (dst:va_operand_vec_opr) (src:sim) : (va_quickCode unit (va_code_Vspltisw dst
  src)) =
  (va_QProc (va_code_Vspltisw dst src) ([va_mod_vec_opr dst]) (va_wp_Vspltisw dst src)
    (va_wpProof_Vspltisw dst src))
//--
//-- Vspltisb

val va_code_Vspltisb : dst:va_operand_vec_opr -> src:sim -> Tot va_code

val va_codegen_success_Vspltisb : dst:va_operand_vec_opr -> src:sim -> Tot va_pbool

val va_lemma_Vspltisb : va_b0:va_code -> va_s0:va_state -> dst:va_operand_vec_opr -> src:sim
  -> Ghost (va_state & va_fuel)
  (requires (va_require_total va_b0 (va_code_Vspltisb dst src) va_s0 /\ va_is_dst_vec_opr dst 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 /\
    (let src_nat8 = Vale.PPC64LE.Machine_s.int_to_nat8 src in let src_nat32 =
    Vale.Def.Types_s.be_bytes_to_nat32 (Vale.Def.Words.Seq_s.four_to_seq_BE #Vale.Def.Types_s.nat8
    (Vale.Def.Words_s.Mkfour #Vale.Def.Types_s.nat8 src_nat8 src_nat8 src_nat8 src_nat8)) in
    va_eval_vec_opr va_sM dst == Vale.Def.Words_s.Mkfour #Vale.Def.Types_s.nat32 src_nat32
    src_nat32 src_nat32 src_nat32) /\ 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_Vspltisb (dst:va_operand_vec_opr) (src:sim) (va_s0:va_state) (va_k:(va_state -> unit ->
  Type0)) : Type0 =
  (va_is_dst_vec_opr dst 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 /\ (let src_nat8 =
    Vale.PPC64LE.Machine_s.int_to_nat8 src in let src_nat32 = Vale.Def.Types_s.be_bytes_to_nat32
    (Vale.Def.Words.Seq_s.four_to_seq_BE #Vale.Def.Types_s.nat8 (Vale.Def.Words_s.Mkfour
    #Vale.Def.Types_s.nat8 src_nat8 src_nat8 src_nat8 src_nat8)) in va_eval_vec_opr va_sM dst ==
    Vale.Def.Words_s.Mkfour #Vale.Def.Types_s.nat32 src_nat32 src_nat32 src_nat32 src_nat32) ==>
    va_k va_sM (())))

val va_wpProof_Vspltisb : dst:va_operand_vec_opr -> src:sim -> va_s0:va_state -> va_k:(va_state ->
  unit -> Type0)
  -> Ghost (va_state & va_fuel & unit)
  (requires (va_t_require va_s0 /\ va_wp_Vspltisb dst src va_s0 va_k))
  (ensures (fun (va_sM, va_f0, va_g) -> va_t_ensure (va_code_Vspltisb 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_Vspltisb (dst:va_operand_vec_opr) (src:sim) : (va_quickCode unit (va_code_Vspltisb dst
  src)) =
  (va_QProc (va_code_Vspltisb dst src) ([va_mod_vec_opr dst]) (va_wp_Vspltisb dst src)
    (va_wpProof_Vspltisb dst src))
//--
//-- Load128_buffer

val va_code_Load128_buffer : h:va_operand_heaplet -> dst:va_operand_vec_opr ->
  base:va_operand_reg_opr -> offset:va_operand_reg_opr -> t:taint -> Tot va_code

val va_codegen_success_Load128_buffer : h:va_operand_heaplet -> dst:va_operand_vec_opr ->
  base:va_operand_reg_opr -> offset:va_operand_reg_opr -> t:taint -> Tot va_pbool

val va_lemma_Load128_buffer : va_b0:va_code -> va_s0:va_state -> h:va_operand_heaplet ->
  dst:va_operand_vec_opr -> base:va_operand_reg_opr -> offset:va_operand_reg_opr -> t:taint ->
  b:buffer128 -> index:int
  -> Ghost (va_state & va_fuel)
  (requires (va_require_total va_b0 (va_code_Load128_buffer h dst base offset t) va_s0 /\
    va_is_src_heaplet h va_s0 /\ va_is_dst_vec_opr dst va_s0 /\ va_is_src_reg_opr base va_s0 /\
    va_is_src_reg_opr offset va_s0 /\ va_get_ok va_s0 /\ Vale.PPC64LE.Decls.valid_src_addr
    #Vale.PPC64LE.Memory.vuint128 (va_eval_heaplet va_s0 h) b index /\
    Vale.PPC64LE.Memory.valid_layout_buffer #Vale.PPC64LE.Memory.vuint128 b (va_get_mem_layout
    va_s0) (va_eval_heaplet va_s0 h) false /\ Vale.PPC64LE.Memory.valid_taint_buf128 b
    (va_eval_heaplet va_s0 h) ((va_get_mem_layout va_s0).vl_taint) t /\ va_eval_reg_opr va_s0 base
    + va_eval_reg_opr va_s0 offset == Vale.PPC64LE.Memory.buffer_addr #Vale.PPC64LE.Memory.vuint128
    b (va_eval_heaplet va_s0 h) + 16 `op_Multiply` index))
  (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.PPC64LE.Decls.buffer128_read b index (va_eval_heaplet va_sM
    h) /\ 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_Load128_buffer (h:va_operand_heaplet) (dst:va_operand_vec_opr) (base:va_operand_reg_opr)
  (offset:va_operand_reg_opr) (t:taint) (b:buffer128) (index:int) (va_s0:va_state) (va_k:(va_state
  -> unit -> Type0)) : Type0 =
  (va_is_src_heaplet h va_s0 /\ va_is_dst_vec_opr dst va_s0 /\ va_is_src_reg_opr base va_s0 /\
    va_is_src_reg_opr offset va_s0 /\ va_get_ok va_s0 /\ Vale.PPC64LE.Decls.valid_src_addr
    #Vale.PPC64LE.Memory.vuint128 (va_eval_heaplet va_s0 h) b index /\
    Vale.PPC64LE.Memory.valid_layout_buffer #Vale.PPC64LE.Memory.vuint128 b (va_get_mem_layout
    va_s0) (va_eval_heaplet va_s0 h) false /\ Vale.PPC64LE.Memory.valid_taint_buf128 b
    (va_eval_heaplet va_s0 h) ((va_get_mem_layout va_s0).vl_taint) t /\ va_eval_reg_opr va_s0 base
    + va_eval_reg_opr va_s0 offset == Vale.PPC64LE.Memory.buffer_addr #Vale.PPC64LE.Memory.vuint128
    b (va_eval_heaplet va_s0 h) + 16 `op_Multiply` index /\ (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.PPC64LE.Decls.buffer128_read b index (va_eval_heaplet va_sM h) ==> va_k va_sM
    (())))

val va_wpProof_Load128_buffer : h:va_operand_heaplet -> dst:va_operand_vec_opr ->
  base:va_operand_reg_opr -> offset:va_operand_reg_opr -> t:taint -> b:buffer128 -> index:int ->
  va_s0:va_state -> va_k:(va_state -> unit -> Type0)
  -> Ghost (va_state & va_fuel & unit)
  (requires (va_t_require va_s0 /\ va_wp_Load128_buffer h dst base offset t b index va_s0 va_k))
  (ensures (fun (va_sM, va_f0, va_g) -> va_t_ensure (va_code_Load128_buffer h dst base offset t)
    ([va_mod_vec_opr dst]) va_s0 va_k ((va_sM, va_f0, va_g))))
[@ "opaque_to_smt" va_qattr]
let va_quick_Load128_buffer (h:va_operand_heaplet) (dst:va_operand_vec_opr)
  (base:va_operand_reg_opr) (offset:va_operand_reg_opr) (t:taint) (b:buffer128) (index:int) :
  (va_quickCode unit (va_code_Load128_buffer h dst base offset t)) =
  (va_QProc (va_code_Load128_buffer h dst base offset t) ([va_mod_vec_opr dst])
    (va_wp_Load128_buffer h dst base offset t b index) (va_wpProof_Load128_buffer h dst base offset
    t b index))
//--
//-- Store128_buffer

val va_code_Store128_buffer : h:va_operand_heaplet -> src:va_operand_vec_opr ->
  base:va_operand_reg_opr -> offset:va_operand_reg_opr -> t:taint -> Tot va_code

val va_codegen_success_Store128_buffer : h:va_operand_heaplet -> src:va_operand_vec_opr ->
  base:va_operand_reg_opr -> offset:va_operand_reg_opr -> t:taint -> Tot va_pbool

val va_lemma_Store128_buffer : va_b0:va_code -> va_s0:va_state -> h:va_operand_heaplet ->
  src:va_operand_vec_opr -> base:va_operand_reg_opr -> offset:va_operand_reg_opr -> t:taint ->
  b:buffer128 -> index:int
  -> Ghost (va_state & va_fuel)
  (requires (va_require_total va_b0 (va_code_Store128_buffer h src base offset t) va_s0 /\
    va_is_dst_heaplet h va_s0 /\ va_is_src_vec_opr src va_s0 /\ va_is_src_reg_opr base va_s0 /\
    va_is_src_reg_opr offset va_s0 /\ va_get_ok va_s0 /\ Vale.PPC64LE.Decls.valid_dst_addr
    #Vale.PPC64LE.Memory.vuint128 (va_eval_heaplet va_s0 h) b index /\
    Vale.PPC64LE.Memory.valid_layout_buffer #Vale.PPC64LE.Memory.vuint128 b (va_get_mem_layout
    va_s0) (va_eval_heaplet va_s0 h) true /\ Vale.PPC64LE.Memory.valid_taint_buf128 b
    (va_eval_heaplet va_s0 h) ((va_get_mem_layout va_s0).vl_taint) t /\ va_eval_reg_opr va_s0 base
    + va_eval_reg_opr va_s0 offset == Vale.PPC64LE.Memory.buffer_addr #Vale.PPC64LE.Memory.vuint128
    b (va_eval_heaplet va_s0 h) + 16 `op_Multiply` index))
  (ensures (fun (va_sM, va_fM) -> va_ensure_total va_b0 va_s0 va_sM va_fM /\ va_get_ok va_sM /\
    va_eval_heaplet va_sM h == buffer128_write b index (va_eval_vec_opr va_s0 src) (va_eval_heaplet
    va_s0 h) /\ 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_qattr]
let va_wp_Store128_buffer (h:va_operand_heaplet) (src:va_operand_vec_opr) (base:va_operand_reg_opr)
  (offset:va_operand_reg_opr) (t:taint) (b:buffer128) (index:int) (va_s0:va_state) (va_k:(va_state
  -> unit -> Type0)) : Type0 =
  (va_is_dst_heaplet h va_s0 /\ va_is_src_vec_opr src va_s0 /\ va_is_src_reg_opr base va_s0 /\
    va_is_src_reg_opr offset va_s0 /\ va_get_ok va_s0 /\ Vale.PPC64LE.Decls.valid_dst_addr
    #Vale.PPC64LE.Memory.vuint128 (va_eval_heaplet va_s0 h) b index /\
    Vale.PPC64LE.Memory.valid_layout_buffer #Vale.PPC64LE.Memory.vuint128 b (va_get_mem_layout
    va_s0) (va_eval_heaplet va_s0 h) true /\ Vale.PPC64LE.Memory.valid_taint_buf128 b
    (va_eval_heaplet va_s0 h) ((va_get_mem_layout va_s0).vl_taint) t /\ va_eval_reg_opr va_s0 base
    + va_eval_reg_opr va_s0 offset == Vale.PPC64LE.Memory.buffer_addr #Vale.PPC64LE.Memory.vuint128
    b (va_eval_heaplet va_s0 h) + 16 `op_Multiply` index /\ (forall (va_x_h:va_value_heaplet)
    (va_x_mem:vale_heap) . let va_sM = va_upd_mem va_x_mem (va_upd_operand_heaplet h va_x_h va_s0)
    in va_get_ok va_sM /\ va_eval_heaplet va_sM h == buffer128_write b index (va_eval_vec_opr va_s0
    src) (va_eval_heaplet va_s0 h) ==> va_k va_sM (())))

val va_wpProof_Store128_buffer : h:va_operand_heaplet -> src:va_operand_vec_opr ->
  base:va_operand_reg_opr -> offset:va_operand_reg_opr -> t:taint -> b:buffer128 -> index:int ->
  va_s0:va_state -> va_k:(va_state -> unit -> Type0)
  -> Ghost (va_state & va_fuel & unit)
  (requires (va_t_require va_s0 /\ va_wp_Store128_buffer h src base offset t b index va_s0 va_k))
  (ensures (fun (va_sM, va_f0, va_g) -> va_t_ensure (va_code_Store128_buffer h src base offset t)
    ([va_Mod_mem; va_mod_heaplet h]) va_s0 va_k ((va_sM, va_f0, va_g))))
[@ "opaque_to_smt" va_qattr]
let va_quick_Store128_buffer (h:va_operand_heaplet) (src:va_operand_vec_opr)
  (base:va_operand_reg_opr) (offset:va_operand_reg_opr) (t:taint) (b:buffer128) (index:int) :
  (va_quickCode unit (va_code_Store128_buffer h src base offset t)) =
  (va_QProc (va_code_Store128_buffer h src base offset t) ([va_Mod_mem; va_mod_heaplet h])
    (va_wp_Store128_buffer h src base offset t b index) (va_wpProof_Store128_buffer h src base
    offset t b index))
//--
//-- Load128_word4_buffer

val va_code_Load128_word4_buffer : h:va_operand_heaplet -> dst:va_operand_vec_opr ->
  base:va_operand_reg_opr -> t:taint -> Tot va_code

val va_codegen_success_Load128_word4_buffer : h:va_operand_heaplet -> dst:va_operand_vec_opr ->
  base:va_operand_reg_opr -> t:taint -> Tot va_pbool

val va_lemma_Load128_word4_buffer : va_b0:va_code -> va_s0:va_state -> h:va_operand_heaplet ->
  dst:va_operand_vec_opr -> base:va_operand_reg_opr -> t:taint -> b:buffer128 -> index:int
  -> Ghost (va_state & va_fuel)
  (requires (va_require_total va_b0 (va_code_Load128_word4_buffer h dst base t) va_s0 /\
    va_is_src_heaplet h va_s0 /\ va_is_dst_vec_opr dst va_s0 /\ va_is_src_reg_opr base va_s0 /\
    va_get_ok va_s0 /\ Vale.PPC64LE.Decls.valid_src_addr #Vale.PPC64LE.Memory.vuint128
    (va_eval_heaplet va_s0 h) b index /\ Vale.PPC64LE.Memory.valid_layout_buffer
    #Vale.PPC64LE.Memory.vuint128 b (va_get_mem_layout va_s0) (va_eval_heaplet va_s0 h) false /\
    Vale.PPC64LE.Memory.valid_taint_buf128 b (va_eval_heaplet va_s0 h) ((va_get_mem_layout
    va_s0).vl_taint) t /\ va_eval_reg_opr va_s0 base == Vale.PPC64LE.Memory.buffer_addr
    #Vale.PPC64LE.Memory.vuint128 b (va_eval_heaplet va_s0 h) + 16 `op_Multiply` index))
  (ensures (fun (va_sM, va_fM) -> va_ensure_total va_b0 va_s0 va_sM va_fM /\ va_get_ok va_sM /\
    (let buf = Vale.PPC64LE.Decls.buffer128_read b index (va_eval_heaplet va_sM h) in l_and (l_and
    (l_and (Vale.Def.Words_s.__proj__Mkfour__item__lo0 (va_eval_vec_opr va_sM dst) ==
    Vale.Def.Words_s.__proj__Mkfour__item__hi3 buf) (Vale.Def.Words_s.__proj__Mkfour__item__lo1
    (va_eval_vec_opr va_sM dst) == Vale.Def.Words_s.__proj__Mkfour__item__hi2 buf))
    (Vale.Def.Words_s.__proj__Mkfour__item__hi2 (va_eval_vec_opr va_sM dst) ==
    Vale.Def.Words_s.__proj__Mkfour__item__lo1 buf)) (Vale.Def.Words_s.__proj__Mkfour__item__hi3
    (va_eval_vec_opr va_sM dst) == Vale.Def.Words_s.__proj__Mkfour__item__lo0 buf)) /\ 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_Load128_word4_buffer (h:va_operand_heaplet) (dst:va_operand_vec_opr)
  (base:va_operand_reg_opr) (t:taint) (b:buffer128) (index:int) (va_s0:va_state) (va_k:(va_state ->
  unit -> Type0)) : Type0 =
  (va_is_src_heaplet h va_s0 /\ va_is_dst_vec_opr dst va_s0 /\ va_is_src_reg_opr base va_s0 /\
    va_get_ok va_s0 /\ Vale.PPC64LE.Decls.valid_src_addr #Vale.PPC64LE.Memory.vuint128
    (va_eval_heaplet va_s0 h) b index /\ Vale.PPC64LE.Memory.valid_layout_buffer
    #Vale.PPC64LE.Memory.vuint128 b (va_get_mem_layout va_s0) (va_eval_heaplet va_s0 h) false /\
    Vale.PPC64LE.Memory.valid_taint_buf128 b (va_eval_heaplet va_s0 h) ((va_get_mem_layout
    va_s0).vl_taint) t /\ va_eval_reg_opr va_s0 base == Vale.PPC64LE.Memory.buffer_addr
    #Vale.PPC64LE.Memory.vuint128 b (va_eval_heaplet va_s0 h) + 16 `op_Multiply` index /\ (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 buf = Vale.PPC64LE.Decls.buffer128_read b index (va_eval_heaplet va_sM
    h) in l_and (l_and (l_and (Vale.Def.Words_s.__proj__Mkfour__item__lo0 (va_eval_vec_opr va_sM
    dst) == Vale.Def.Words_s.__proj__Mkfour__item__hi3 buf)
    (Vale.Def.Words_s.__proj__Mkfour__item__lo1 (va_eval_vec_opr va_sM dst) ==
    Vale.Def.Words_s.__proj__Mkfour__item__hi2 buf)) (Vale.Def.Words_s.__proj__Mkfour__item__hi2
    (va_eval_vec_opr va_sM dst) == Vale.Def.Words_s.__proj__Mkfour__item__lo1 buf))
    (Vale.Def.Words_s.__proj__Mkfour__item__hi3 (va_eval_vec_opr va_sM dst) ==
    Vale.Def.Words_s.__proj__Mkfour__item__lo0 buf)) ==> va_k va_sM (())))

val va_wpProof_Load128_word4_buffer : h:va_operand_heaplet -> dst:va_operand_vec_opr ->
  base:va_operand_reg_opr -> t:taint -> b:buffer128 -> index:int -> va_s0:va_state ->
  va_k:(va_state -> unit -> Type0)
  -> Ghost (va_state & va_fuel & unit)
  (requires (va_t_require va_s0 /\ va_wp_Load128_word4_buffer h dst base t b index va_s0 va_k))
  (ensures (fun (va_sM, va_f0, va_g) -> va_t_ensure (va_code_Load128_word4_buffer h dst base t)
    ([va_mod_vec_opr dst]) va_s0 va_k ((va_sM, va_f0, va_g))))
[@ "opaque_to_smt" va_qattr]
let va_quick_Load128_word4_buffer (h:va_operand_heaplet) (dst:va_operand_vec_opr)
  (base:va_operand_reg_opr) (t:taint) (b:buffer128) (index:int) : (va_quickCode unit
  (va_code_Load128_word4_buffer h dst base t)) =
  (va_QProc (va_code_Load128_word4_buffer h dst base t) ([va_mod_vec_opr dst])
    (va_wp_Load128_word4_buffer h dst base t b index) (va_wpProof_Load128_word4_buffer h dst base t
    b index))
//--
//-- Load128_word4_buffer_index

val va_code_Load128_word4_buffer_index : h:va_operand_heaplet -> dst:va_operand_vec_opr ->
  base:va_operand_reg_opr -> offset:va_operand_reg_opr -> t:taint -> Tot va_code

val va_codegen_success_Load128_word4_buffer_index : h:va_operand_heaplet -> dst:va_operand_vec_opr
  -> base:va_operand_reg_opr -> offset:va_operand_reg_opr -> t:taint -> Tot va_pbool

val va_lemma_Load128_word4_buffer_index : va_b0:va_code -> va_s0:va_state -> h:va_operand_heaplet
  -> dst:va_operand_vec_opr -> base:va_operand_reg_opr -> offset:va_operand_reg_opr -> t:taint ->
  b:buffer128 -> index:int
  -> Ghost (va_state & va_fuel)
  (requires (va_require_total va_b0 (va_code_Load128_word4_buffer_index h dst base offset t) va_s0
    /\ va_is_src_heaplet h va_s0 /\ va_is_dst_vec_opr dst va_s0 /\ va_is_src_reg_opr base va_s0 /\
    va_is_src_reg_opr offset va_s0 /\ va_get_ok va_s0 /\ offset =!= 0 /\
    Vale.PPC64LE.Decls.valid_src_addr #Vale.PPC64LE.Memory.vuint128 (va_eval_heaplet va_s0 h) b
    index /\ Vale.PPC64LE.Memory.valid_layout_buffer #Vale.PPC64LE.Memory.vuint128 b
    (va_get_mem_layout va_s0) (va_eval_heaplet va_s0 h) false /\
    Vale.PPC64LE.Memory.valid_taint_buf128 b (va_eval_heaplet va_s0 h) ((va_get_mem_layout
    va_s0).vl_taint) t /\ va_eval_reg_opr va_s0 base + va_eval_reg_opr va_s0 offset ==
    Vale.PPC64LE.Memory.buffer_addr #Vale.PPC64LE.Memory.vuint128 b (va_eval_heaplet va_s0 h) + 16
    `op_Multiply` index))
  (ensures (fun (va_sM, va_fM) -> va_ensure_total va_b0 va_s0 va_sM va_fM /\ va_get_ok va_sM /\
    (let buf = Vale.PPC64LE.Decls.buffer128_read b index (va_eval_heaplet va_sM h) in l_and (l_and
    (l_and (Vale.Def.Words_s.__proj__Mkfour__item__lo0 (va_eval_vec_opr va_sM dst) ==
    Vale.Def.Words_s.__proj__Mkfour__item__hi3 buf) (Vale.Def.Words_s.__proj__Mkfour__item__lo1
    (va_eval_vec_opr va_sM dst) == Vale.Def.Words_s.__proj__Mkfour__item__hi2 buf))
    (Vale.Def.Words_s.__proj__Mkfour__item__hi2 (va_eval_vec_opr va_sM dst) ==
    Vale.Def.Words_s.__proj__Mkfour__item__lo1 buf)) (Vale.Def.Words_s.__proj__Mkfour__item__hi3
    (va_eval_vec_opr va_sM dst) == Vale.Def.Words_s.__proj__Mkfour__item__lo0 buf)) /\ 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_Load128_word4_buffer_index (h:va_operand_heaplet) (dst:va_operand_vec_opr)
  (base:va_operand_reg_opr) (offset:va_operand_reg_opr) (t:taint) (b:buffer128) (index:int)
  (va_s0:va_state) (va_k:(va_state -> unit -> Type0)) : Type0 =
  (va_is_src_heaplet h va_s0 /\ va_is_dst_vec_opr dst va_s0 /\ va_is_src_reg_opr base va_s0 /\
    va_is_src_reg_opr offset va_s0 /\ va_get_ok va_s0 /\ offset =!= 0 /\
    Vale.PPC64LE.Decls.valid_src_addr #Vale.PPC64LE.Memory.vuint128 (va_eval_heaplet va_s0 h) b
    index /\ Vale.PPC64LE.Memory.valid_layout_buffer #Vale.PPC64LE.Memory.vuint128 b
    (va_get_mem_layout va_s0) (va_eval_heaplet va_s0 h) false /\
    Vale.PPC64LE.Memory.valid_taint_buf128 b (va_eval_heaplet va_s0 h) ((va_get_mem_layout
    va_s0).vl_taint) t /\ va_eval_reg_opr va_s0 base + va_eval_reg_opr va_s0 offset ==
    Vale.PPC64LE.Memory.buffer_addr #Vale.PPC64LE.Memory.vuint128 b (va_eval_heaplet va_s0 h) + 16
    `op_Multiply` index /\ (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 buf = Vale.PPC64LE.Decls.buffer128_read b index
    (va_eval_heaplet va_sM h) in l_and (l_and (l_and (Vale.Def.Words_s.__proj__Mkfour__item__lo0
    (va_eval_vec_opr va_sM dst) == Vale.Def.Words_s.__proj__Mkfour__item__hi3 buf)
    (Vale.Def.Words_s.__proj__Mkfour__item__lo1 (va_eval_vec_opr va_sM dst) ==
    Vale.Def.Words_s.__proj__Mkfour__item__hi2 buf)) (Vale.Def.Words_s.__proj__Mkfour__item__hi2
    (va_eval_vec_opr va_sM dst) == Vale.Def.Words_s.__proj__Mkfour__item__lo1 buf))
    (Vale.Def.Words_s.__proj__Mkfour__item__hi3 (va_eval_vec_opr va_sM dst) ==
    Vale.Def.Words_s.__proj__Mkfour__item__lo0 buf)) ==> va_k va_sM (())))

val va_wpProof_Load128_word4_buffer_index : h:va_operand_heaplet -> dst:va_operand_vec_opr ->
  base:va_operand_reg_opr -> offset:va_operand_reg_opr -> t:taint -> b:buffer128 -> index:int ->
  va_s0:va_state -> va_k:(va_state -> unit -> Type0)
  -> Ghost (va_state & va_fuel & unit)
  (requires (va_t_require va_s0 /\ va_wp_Load128_word4_buffer_index h dst base offset t b index
    va_s0 va_k))
  (ensures (fun (va_sM, va_f0, va_g) -> va_t_ensure (va_code_Load128_word4_buffer_index h dst base
    offset t) ([va_mod_vec_opr dst]) va_s0 va_k ((va_sM, va_f0, va_g))))
[@ "opaque_to_smt" va_qattr]
let va_quick_Load128_word4_buffer_index (h:va_operand_heaplet) (dst:va_operand_vec_opr)
  (base:va_operand_reg_opr) (offset:va_operand_reg_opr) (t:taint) (b:buffer128) (index:int) :
  (va_quickCode unit (va_code_Load128_word4_buffer_index h dst base offset t)) =
  (va_QProc (va_code_Load128_word4_buffer_index h dst base offset t) ([va_mod_vec_opr dst])
    (va_wp_Load128_word4_buffer_index h dst base offset t b index)
    (va_wpProof_Load128_word4_buffer_index h dst base offset t b index))
//--
//-- Store128_word4_buffer

val va_code_Store128_word4_buffer : h:va_operand_heaplet -> src:va_operand_vec_opr ->
  base:va_operand_reg_opr -> t:taint -> Tot va_code

val va_codegen_success_Store128_word4_buffer : h:va_operand_heaplet -> src:va_operand_vec_opr ->
  base:va_operand_reg_opr -> t:taint -> Tot va_pbool

val va_lemma_Store128_word4_buffer : va_b0:va_code -> va_s0:va_state -> h:va_operand_heaplet ->
  src:va_operand_vec_opr -> base:va_operand_reg_opr -> t:taint -> b:buffer128 -> index:int
  -> Ghost (va_state & va_fuel)
  (requires (va_require_total va_b0 (va_code_Store128_word4_buffer h src base t) va_s0 /\
    va_is_dst_heaplet h va_s0 /\ va_is_src_vec_opr src va_s0 /\ va_is_src_reg_opr base va_s0 /\
    va_get_ok va_s0 /\ Vale.PPC64LE.Decls.valid_dst_addr #Vale.PPC64LE.Memory.vuint128
    (va_eval_heaplet va_s0 h) b index /\ Vale.PPC64LE.Memory.valid_layout_buffer
    #Vale.PPC64LE.Memory.vuint128 b (va_get_mem_layout va_s0) (va_eval_heaplet va_s0 h) true /\
    Vale.PPC64LE.Memory.valid_taint_buf128 b (va_eval_heaplet va_s0 h) ((va_get_mem_layout
    va_s0).vl_taint) t /\ va_eval_reg_opr va_s0 base == Vale.PPC64LE.Memory.buffer_addr
    #Vale.PPC64LE.Memory.vuint128 b (va_eval_heaplet va_s0 h) + 16 `op_Multiply` index))
  (ensures (fun (va_sM, va_fM) -> va_ensure_total va_b0 va_s0 va_sM va_fM /\ va_get_ok va_sM /\
    va_eval_heaplet va_sM h == buffer128_write 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_s0
    src)) (Vale.Def.Words_s.__proj__Mkfour__item__hi2 (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__lo0 (va_eval_vec_opr va_s0 src))) (va_eval_heaplet
    va_s0 h) /\ 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_qattr]
let va_wp_Store128_word4_buffer (h:va_operand_heaplet) (src:va_operand_vec_opr)
  (base:va_operand_reg_opr) (t:taint) (b:buffer128) (index:int) (va_s0:va_state) (va_k:(va_state ->
  unit -> Type0)) : Type0 =
  (va_is_dst_heaplet h va_s0 /\ va_is_src_vec_opr src va_s0 /\ va_is_src_reg_opr base va_s0 /\
    va_get_ok va_s0 /\ Vale.PPC64LE.Decls.valid_dst_addr #Vale.PPC64LE.Memory.vuint128
    (va_eval_heaplet va_s0 h) b index /\ Vale.PPC64LE.Memory.valid_layout_buffer
    #Vale.PPC64LE.Memory.vuint128 b (va_get_mem_layout va_s0) (va_eval_heaplet va_s0 h) true /\
    Vale.PPC64LE.Memory.valid_taint_buf128 b (va_eval_heaplet va_s0 h) ((va_get_mem_layout
    va_s0).vl_taint) t /\ va_eval_reg_opr va_s0 base == Vale.PPC64LE.Memory.buffer_addr
    #Vale.PPC64LE.Memory.vuint128 b (va_eval_heaplet va_s0 h) + 16 `op_Multiply` index /\ (forall
    (va_x_h:va_value_heaplet) (va_x_mem:vale_heap) . let va_sM = va_upd_mem va_x_mem
    (va_upd_operand_heaplet h va_x_h va_s0) in va_get_ok va_sM /\ va_eval_heaplet va_sM h ==
    buffer128_write 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_s0 src))
    (Vale.Def.Words_s.__proj__Mkfour__item__hi2 (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__lo0 (va_eval_vec_opr va_s0 src))) (va_eval_heaplet
    va_s0 h) ==> va_k va_sM (())))

val va_wpProof_Store128_word4_buffer : h:va_operand_heaplet -> src:va_operand_vec_opr ->
  base:va_operand_reg_opr -> t:taint -> b:buffer128 -> index:int -> va_s0:va_state ->
  va_k:(va_state -> unit -> Type0)
  -> Ghost (va_state & va_fuel & unit)
  (requires (va_t_require va_s0 /\ va_wp_Store128_word4_buffer h src base t b index va_s0 va_k))
  (ensures (fun (va_sM, va_f0, va_g) -> va_t_ensure (va_code_Store128_word4_buffer h src base t)
    ([va_Mod_mem; va_mod_heaplet h]) va_s0 va_k ((va_sM, va_f0, va_g))))
[@ "opaque_to_smt" va_qattr]
let va_quick_Store128_word4_buffer (h:va_operand_heaplet) (src:va_operand_vec_opr)
  (base:va_operand_reg_opr) (t:taint) (b:buffer128) (index:int) : (va_quickCode unit
  (va_code_Store128_word4_buffer h src base t)) =
  (va_QProc (va_code_Store128_word4_buffer h src base t) ([va_Mod_mem; va_mod_heaplet h])
    (va_wp_Store128_word4_buffer h src base t b index) (va_wpProof_Store128_word4_buffer h src base
    t b index))
//--
//-- Store128_word4_buffer_index

val va_code_Store128_word4_buffer_index : h:va_operand_heaplet -> src:va_operand_vec_opr ->
  base:va_operand_reg_opr -> offset:va_operand_reg_opr -> t:taint -> Tot va_code

val va_codegen_success_Store128_word4_buffer_index : h:va_operand_heaplet -> src:va_operand_vec_opr
  -> base:va_operand_reg_opr -> offset:va_operand_reg_opr -> t:taint -> Tot va_pbool

val va_lemma_Store128_word4_buffer_index : va_b0:va_code -> va_s0:va_state -> h:va_operand_heaplet
  -> src:va_operand_vec_opr -> base:va_operand_reg_opr -> offset:va_operand_reg_opr -> t:taint ->
  b:buffer128 -> index:int
  -> Ghost (va_state & va_fuel)
  (requires (va_require_total va_b0 (va_code_Store128_word4_buffer_index h src base offset t) va_s0
    /\ va_is_dst_heaplet h va_s0 /\ va_is_src_vec_opr src va_s0 /\ va_is_src_reg_opr base va_s0 /\
    va_is_src_reg_opr offset va_s0 /\ va_get_ok va_s0 /\ offset =!= 0 /\
    Vale.PPC64LE.Decls.valid_dst_addr #Vale.PPC64LE.Memory.vuint128 (va_eval_heaplet va_s0 h) b
    index /\ Vale.PPC64LE.Memory.valid_layout_buffer #Vale.PPC64LE.Memory.vuint128 b
    (va_get_mem_layout va_s0) (va_eval_heaplet va_s0 h) true /\
    Vale.PPC64LE.Memory.valid_taint_buf128 b (va_eval_heaplet va_s0 h) ((va_get_mem_layout
    va_s0).vl_taint) t /\ va_eval_reg_opr va_s0 base + va_eval_reg_opr va_s0 offset ==
    Vale.PPC64LE.Memory.buffer_addr #Vale.PPC64LE.Memory.vuint128 b (va_eval_heaplet va_s0 h) + 16
    `op_Multiply` index))
  (ensures (fun (va_sM, va_fM) -> va_ensure_total va_b0 va_s0 va_sM va_fM /\ va_get_ok va_sM /\
    va_eval_heaplet va_sM h == buffer128_write 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_s0
    src)) (Vale.Def.Words_s.__proj__Mkfour__item__hi2 (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__lo0 (va_eval_vec_opr va_s0 src))) (va_eval_heaplet
    va_s0 h) /\ 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_qattr]
let va_wp_Store128_word4_buffer_index (h:va_operand_heaplet) (src:va_operand_vec_opr)
  (base:va_operand_reg_opr) (offset:va_operand_reg_opr) (t:taint) (b:buffer128) (index:int)
  (va_s0:va_state) (va_k:(va_state -> unit -> Type0)) : Type0 =
  (va_is_dst_heaplet h va_s0 /\ va_is_src_vec_opr src va_s0 /\ va_is_src_reg_opr base va_s0 /\
    va_is_src_reg_opr offset va_s0 /\ va_get_ok va_s0 /\ offset =!= 0 /\
    Vale.PPC64LE.Decls.valid_dst_addr #Vale.PPC64LE.Memory.vuint128 (va_eval_heaplet va_s0 h) b
    index /\ Vale.PPC64LE.Memory.valid_layout_buffer #Vale.PPC64LE.Memory.vuint128 b
    (va_get_mem_layout va_s0) (va_eval_heaplet va_s0 h) true /\
    Vale.PPC64LE.Memory.valid_taint_buf128 b (va_eval_heaplet va_s0 h) ((va_get_mem_layout
    va_s0).vl_taint) t /\ va_eval_reg_opr va_s0 base + va_eval_reg_opr va_s0 offset ==
    Vale.PPC64LE.Memory.buffer_addr #Vale.PPC64LE.Memory.vuint128 b (va_eval_heaplet va_s0 h) + 16
    `op_Multiply` index /\ (forall (va_x_h:va_value_heaplet) (va_x_mem:vale_heap) . let va_sM =
    va_upd_mem va_x_mem (va_upd_operand_heaplet h va_x_h va_s0) in va_get_ok va_sM /\
    va_eval_heaplet va_sM h == buffer128_write 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_s0
    src)) (Vale.Def.Words_s.__proj__Mkfour__item__hi2 (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__lo0 (va_eval_vec_opr va_s0 src))) (va_eval_heaplet
    va_s0 h) ==> va_k va_sM (())))

val va_wpProof_Store128_word4_buffer_index : h:va_operand_heaplet -> src:va_operand_vec_opr ->
  base:va_operand_reg_opr -> offset:va_operand_reg_opr -> t:taint -> b:buffer128 -> index:int ->
  va_s0:va_state -> va_k:(va_state -> unit -> Type0)
  -> Ghost (va_state & va_fuel & unit)
  (requires (va_t_require va_s0 /\ va_wp_Store128_word4_buffer_index h src base offset t b index
    va_s0 va_k))
  (ensures (fun (va_sM, va_f0, va_g) -> va_t_ensure (va_code_Store128_word4_buffer_index h src base
    offset t) ([va_Mod_mem; va_mod_heaplet h]) va_s0 va_k ((va_sM, va_f0, va_g))))
[@ "opaque_to_smt" va_qattr]
let va_quick_Store128_word4_buffer_index (h:va_operand_heaplet) (src:va_operand_vec_opr)
  (base:va_operand_reg_opr) (offset:va_operand_reg_opr) (t:taint) (b:buffer128) (index:int) :
  (va_quickCode unit (va_code_Store128_word4_buffer_index h src base offset t)) =
  (va_QProc (va_code_Store128_word4_buffer_index h src base offset t) ([va_Mod_mem; va_mod_heaplet
    h]) (va_wp_Store128_word4_buffer_index h src base offset t b index)
    (va_wpProof_Store128_word4_buffer_index h src base offset t b index))
//--
//-- Load128_byte16_buffer

val va_code_Load128_byte16_buffer : h:va_operand_heaplet -> dst:va_operand_vec_opr ->
  base:va_operand_reg_opr -> t:taint -> Tot va_code

val va_codegen_success_Load128_byte16_buffer : h:va_operand_heaplet -> dst:va_operand_vec_opr ->
  base:va_operand_reg_opr -> t:taint -> Tot va_pbool

val va_lemma_Load128_byte16_buffer : va_b0:va_code -> va_s0:va_state -> h:va_operand_heaplet ->
  dst:va_operand_vec_opr -> base:va_operand_reg_opr -> t:taint -> b:buffer128 -> index:int
  -> Ghost (va_state & va_fuel)
  (requires (va_require_total va_b0 (va_code_Load128_byte16_buffer h dst base t) va_s0 /\
    va_is_src_heaplet h va_s0 /\ va_is_dst_vec_opr dst va_s0 /\ va_is_src_reg_opr base va_s0 /\
    va_get_ok va_s0 /\ Vale.PPC64LE.Decls.valid_src_addr #Vale.PPC64LE.Memory.vuint128
    (va_eval_heaplet va_s0 h) b index /\ Vale.PPC64LE.Memory.valid_layout_buffer
    #Vale.PPC64LE.Memory.vuint128 b (va_get_mem_layout va_s0) (va_eval_heaplet va_s0 h) false /\
    Vale.PPC64LE.Memory.valid_taint_buf128 b (va_eval_heaplet va_s0 h) ((va_get_mem_layout
    va_s0).vl_taint) t /\ va_eval_reg_opr va_s0 base == Vale.PPC64LE.Memory.buffer_addr
    #Vale.PPC64LE.Memory.vuint128 b (va_eval_heaplet va_s0 h) + 16 `op_Multiply` index))
  (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.reverse_bytes_quad32
    (Vale.PPC64LE.Decls.buffer128_read b index (va_eval_heaplet va_sM h)) /\ 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_Load128_byte16_buffer (h:va_operand_heaplet) (dst:va_operand_vec_opr)
  (base:va_operand_reg_opr) (t:taint) (b:buffer128) (index:int) (va_s0:va_state) (va_k:(va_state ->
  unit -> Type0)) : Type0 =
  (va_is_src_heaplet h va_s0 /\ va_is_dst_vec_opr dst va_s0 /\ va_is_src_reg_opr base va_s0 /\
    va_get_ok va_s0 /\ Vale.PPC64LE.Decls.valid_src_addr #Vale.PPC64LE.Memory.vuint128
    (va_eval_heaplet va_s0 h) b index /\ Vale.PPC64LE.Memory.valid_layout_buffer
    #Vale.PPC64LE.Memory.vuint128 b (va_get_mem_layout va_s0) (va_eval_heaplet va_s0 h) false /\
    Vale.PPC64LE.Memory.valid_taint_buf128 b (va_eval_heaplet va_s0 h) ((va_get_mem_layout
    va_s0).vl_taint) t /\ va_eval_reg_opr va_s0 base == Vale.PPC64LE.Memory.buffer_addr
    #Vale.PPC64LE.Memory.vuint128 b (va_eval_heaplet va_s0 h) + 16 `op_Multiply` index /\ (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.reverse_bytes_quad32
    (Vale.PPC64LE.Decls.buffer128_read b index (va_eval_heaplet va_sM h)) ==> va_k va_sM (())))

val va_wpProof_Load128_byte16_buffer : h:va_operand_heaplet -> dst:va_operand_vec_opr ->
  base:va_operand_reg_opr -> t:taint -> b:buffer128 -> index:int -> va_s0:va_state ->
  va_k:(va_state -> unit -> Type0)
  -> Ghost (va_state & va_fuel & unit)
  (requires (va_t_require va_s0 /\ va_wp_Load128_byte16_buffer h dst base t b index va_s0 va_k))
  (ensures (fun (va_sM, va_f0, va_g) -> va_t_ensure (va_code_Load128_byte16_buffer h dst base t)
    ([va_mod_vec_opr dst]) va_s0 va_k ((va_sM, va_f0, va_g))))
[@ "opaque_to_smt" va_qattr]
let va_quick_Load128_byte16_buffer (h:va_operand_heaplet) (dst:va_operand_vec_opr)
  (base:va_operand_reg_opr) (t:taint) (b:buffer128) (index:int) : (va_quickCode unit
  (va_code_Load128_byte16_buffer h dst base t)) =
  (va_QProc (va_code_Load128_byte16_buffer h dst base t) ([va_mod_vec_opr dst])
    (va_wp_Load128_byte16_buffer h dst base t b index) (va_wpProof_Load128_byte16_buffer h dst base
    t b index))
//--
//-- Load128_byte16_buffer_index

val va_code_Load128_byte16_buffer_index : h:va_operand_heaplet -> dst:va_operand_vec_opr ->
  base:va_operand_reg_opr -> offset:va_operand_reg_opr -> t:taint -> Tot va_code

val va_codegen_success_Load128_byte16_buffer_index : h:va_operand_heaplet -> dst:va_operand_vec_opr
  -> base:va_operand_reg_opr -> offset:va_operand_reg_opr -> t:taint -> Tot va_pbool

val va_lemma_Load128_byte16_buffer_index : va_b0:va_code -> va_s0:va_state -> h:va_operand_heaplet
  -> dst:va_operand_vec_opr -> base:va_operand_reg_opr -> offset:va_operand_reg_opr -> t:taint ->
  b:buffer128 -> index:int
  -> Ghost (va_state & va_fuel)
  (requires (va_require_total va_b0 (va_code_Load128_byte16_buffer_index h dst base offset t) va_s0
    /\ va_is_src_heaplet h va_s0 /\ va_is_dst_vec_opr dst va_s0 /\ va_is_src_reg_opr base va_s0 /\
    va_is_src_reg_opr offset va_s0 /\ va_get_ok va_s0 /\ offset =!= 0 /\
    Vale.PPC64LE.Decls.valid_src_addr #Vale.PPC64LE.Memory.vuint128 (va_eval_heaplet va_s0 h) b
    index /\ Vale.PPC64LE.Memory.valid_layout_buffer #Vale.PPC64LE.Memory.vuint128 b
    (va_get_mem_layout va_s0) (va_eval_heaplet va_s0 h) false /\
    Vale.PPC64LE.Memory.valid_taint_buf128 b (va_eval_heaplet va_s0 h) ((va_get_mem_layout
    va_s0).vl_taint) t /\ va_eval_reg_opr va_s0 base + va_eval_reg_opr va_s0 offset ==
    Vale.PPC64LE.Memory.buffer_addr #Vale.PPC64LE.Memory.vuint128 b (va_eval_heaplet va_s0 h) + 16
    `op_Multiply` index))
  (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.reverse_bytes_quad32
    (Vale.PPC64LE.Decls.buffer128_read b index (va_eval_heaplet va_sM h)) /\ 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_Load128_byte16_buffer_index (h:va_operand_heaplet) (dst:va_operand_vec_opr)
  (base:va_operand_reg_opr) (offset:va_operand_reg_opr) (t:taint) (b:buffer128) (index:int)
  (va_s0:va_state) (va_k:(va_state -> unit -> Type0)) : Type0 =
  (va_is_src_heaplet h va_s0 /\ va_is_dst_vec_opr dst va_s0 /\ va_is_src_reg_opr base va_s0 /\
    va_is_src_reg_opr offset va_s0 /\ va_get_ok va_s0 /\ offset =!= 0 /\
    Vale.PPC64LE.Decls.valid_src_addr #Vale.PPC64LE.Memory.vuint128 (va_eval_heaplet va_s0 h) b
    index /\ Vale.PPC64LE.Memory.valid_layout_buffer #Vale.PPC64LE.Memory.vuint128 b
    (va_get_mem_layout va_s0) (va_eval_heaplet va_s0 h) false /\
    Vale.PPC64LE.Memory.valid_taint_buf128 b (va_eval_heaplet va_s0 h) ((va_get_mem_layout
    va_s0).vl_taint) t /\ va_eval_reg_opr va_s0 base + va_eval_reg_opr va_s0 offset ==
    Vale.PPC64LE.Memory.buffer_addr #Vale.PPC64LE.Memory.vuint128 b (va_eval_heaplet va_s0 h) + 16
    `op_Multiply` index /\ (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.reverse_bytes_quad32 (Vale.PPC64LE.Decls.buffer128_read b index
    (va_eval_heaplet va_sM h)) ==> va_k va_sM (())))

val va_wpProof_Load128_byte16_buffer_index : h:va_operand_heaplet -> dst:va_operand_vec_opr ->
  base:va_operand_reg_opr -> offset:va_operand_reg_opr -> t:taint -> b:buffer128 -> index:int ->
  va_s0:va_state -> va_k:(va_state -> unit -> Type0)
  -> Ghost (va_state & va_fuel & unit)
  (requires (va_t_require va_s0 /\ va_wp_Load128_byte16_buffer_index h dst base offset t b index
    va_s0 va_k))
  (ensures (fun (va_sM, va_f0, va_g) -> va_t_ensure (va_code_Load128_byte16_buffer_index h dst base
    offset t) ([va_mod_vec_opr dst]) va_s0 va_k ((va_sM, va_f0, va_g))))
[@ "opaque_to_smt" va_qattr]
let va_quick_Load128_byte16_buffer_index (h:va_operand_heaplet) (dst:va_operand_vec_opr)
  (base:va_operand_reg_opr) (offset:va_operand_reg_opr) (t:taint) (b:buffer128) (index:int) :
  (va_quickCode unit (va_code_Load128_byte16_buffer_index h dst base offset t)) =
  (va_QProc (va_code_Load128_byte16_buffer_index h dst base offset t) ([va_mod_vec_opr dst])
    (va_wp_Load128_byte16_buffer_index h dst base offset t b index)
    (va_wpProof_Load128_byte16_buffer_index h dst base offset t b index))
//--
//-- Store128_byte16_buffer

val va_code_Store128_byte16_buffer : h:va_operand_heaplet -> src:va_operand_vec_opr ->
  base:va_operand_reg_opr -> t:taint -> Tot va_code

val va_codegen_success_Store128_byte16_buffer : h:va_operand_heaplet -> src:va_operand_vec_opr ->
  base:va_operand_reg_opr -> t:taint -> Tot va_pbool

val va_lemma_Store128_byte16_buffer : va_b0:va_code -> va_s0:va_state -> h:va_operand_heaplet ->
  src:va_operand_vec_opr -> base:va_operand_reg_opr -> t:taint -> b:buffer128 -> index:int
  -> Ghost (va_state & va_fuel)
  (requires (va_require_total va_b0 (va_code_Store128_byte16_buffer h src base t) va_s0 /\
    va_is_dst_heaplet h va_s0 /\ va_is_src_vec_opr src va_s0 /\ va_is_src_reg_opr base va_s0 /\
    va_get_ok va_s0 /\ Vale.PPC64LE.Decls.valid_dst_addr #Vale.PPC64LE.Memory.vuint128
    (va_eval_heaplet va_s0 h) b index /\ Vale.PPC64LE.Memory.valid_layout_buffer
    #Vale.PPC64LE.Memory.vuint128 b (va_get_mem_layout va_s0) (va_eval_heaplet va_s0 h) true /\
    Vale.PPC64LE.Memory.valid_taint_buf128 b (va_eval_heaplet va_s0 h) ((va_get_mem_layout
    va_s0).vl_taint) t /\ va_eval_reg_opr va_s0 base == Vale.PPC64LE.Memory.buffer_addr
    #Vale.PPC64LE.Memory.vuint128 b (va_eval_heaplet va_s0 h) + 16 `op_Multiply` index))
  (ensures (fun (va_sM, va_fM) -> va_ensure_total va_b0 va_s0 va_sM va_fM /\ va_get_ok va_sM /\
    va_eval_heaplet va_sM h == buffer128_write b index (Vale.Def.Types_s.reverse_bytes_quad32
    (va_eval_vec_opr va_s0 src)) (va_eval_heaplet va_s0 h) /\ 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_qattr]
let va_wp_Store128_byte16_buffer (h:va_operand_heaplet) (src:va_operand_vec_opr)
  (base:va_operand_reg_opr) (t:taint) (b:buffer128) (index:int) (va_s0:va_state) (va_k:(va_state ->
  unit -> Type0)) : Type0 =
  (va_is_dst_heaplet h va_s0 /\ va_is_src_vec_opr src va_s0 /\ va_is_src_reg_opr base va_s0 /\
    va_get_ok va_s0 /\ Vale.PPC64LE.Decls.valid_dst_addr #Vale.PPC64LE.Memory.vuint128
    (va_eval_heaplet va_s0 h) b index /\ Vale.PPC64LE.Memory.valid_layout_buffer
    #Vale.PPC64LE.Memory.vuint128 b (va_get_mem_layout va_s0) (va_eval_heaplet va_s0 h) true /\
    Vale.PPC64LE.Memory.valid_taint_buf128 b (va_eval_heaplet va_s0 h) ((va_get_mem_layout
    va_s0).vl_taint) t /\ va_eval_reg_opr va_s0 base == Vale.PPC64LE.Memory.buffer_addr
    #Vale.PPC64LE.Memory.vuint128 b (va_eval_heaplet va_s0 h) + 16 `op_Multiply` index /\ (forall
    (va_x_h:va_value_heaplet) (va_x_mem:vale_heap) . let va_sM = va_upd_mem va_x_mem
    (va_upd_operand_heaplet h va_x_h va_s0) in va_get_ok va_sM /\ va_eval_heaplet va_sM h ==
    buffer128_write b index (Vale.Def.Types_s.reverse_bytes_quad32 (va_eval_vec_opr va_s0 src))
    (va_eval_heaplet va_s0 h) ==> va_k va_sM (())))

val va_wpProof_Store128_byte16_buffer : h:va_operand_heaplet -> src:va_operand_vec_opr ->
  base:va_operand_reg_opr -> t:taint -> b:buffer128 -> index:int -> va_s0:va_state ->
  va_k:(va_state -> unit -> Type0)
  -> Ghost (va_state & va_fuel & unit)
  (requires (va_t_require va_s0 /\ va_wp_Store128_byte16_buffer h src base t b index va_s0 va_k))
  (ensures (fun (va_sM, va_f0, va_g) -> va_t_ensure (va_code_Store128_byte16_buffer h src base t)
    ([va_Mod_mem; va_mod_heaplet h]) va_s0 va_k ((va_sM, va_f0, va_g))))
[@ "opaque_to_smt" va_qattr]
let va_quick_Store128_byte16_buffer (h:va_operand_heaplet) (src:va_operand_vec_opr)
  (base:va_operand_reg_opr) (t:taint) (b:buffer128) (index:int) : (va_quickCode unit
  (va_code_Store128_byte16_buffer h src base t)) =
  (va_QProc (va_code_Store128_byte16_buffer h src base t) ([va_Mod_mem; va_mod_heaplet h])
    (va_wp_Store128_byte16_buffer h src base t b index) (va_wpProof_Store128_byte16_buffer h src
    base t b index))
//--
//-- Store128_byte16_buffer_index

val va_code_Store128_byte16_buffer_index : h:va_operand_heaplet -> src:va_operand_vec_opr ->
  base:va_operand_reg_opr -> offset:va_operand_reg_opr -> t:taint -> Tot va_code

val va_codegen_success_Store128_byte16_buffer_index : h:va_operand_heaplet ->
  src:va_operand_vec_opr -> base:va_operand_reg_opr -> offset:va_operand_reg_opr -> t:taint -> Tot
  va_pbool

val va_lemma_Store128_byte16_buffer_index : va_b0:va_code -> va_s0:va_state -> h:va_operand_heaplet
  -> src:va_operand_vec_opr -> base:va_operand_reg_opr -> offset:va_operand_reg_opr -> t:taint ->
  b:buffer128 -> index:int
  -> Ghost (va_state & va_fuel)
  (requires (va_require_total va_b0 (va_code_Store128_byte16_buffer_index h src base offset t)
    va_s0 /\ va_is_dst_heaplet h va_s0 /\ va_is_src_vec_opr src va_s0 /\ va_is_src_reg_opr base
    va_s0 /\ va_is_src_reg_opr offset va_s0 /\ va_get_ok va_s0 /\ offset =!= 0 /\
    Vale.PPC64LE.Decls.valid_dst_addr #Vale.PPC64LE.Memory.vuint128 (va_eval_heaplet va_s0 h) b
    index /\ Vale.PPC64LE.Memory.valid_layout_buffer #Vale.PPC64LE.Memory.vuint128 b
    (va_get_mem_layout va_s0) (va_eval_heaplet va_s0 h) true /\
    Vale.PPC64LE.Memory.valid_taint_buf128 b (va_eval_heaplet va_s0 h) ((va_get_mem_layout
    va_s0).vl_taint) t /\ va_eval_reg_opr va_s0 base + va_eval_reg_opr va_s0 offset ==
    Vale.PPC64LE.Memory.buffer_addr #Vale.PPC64LE.Memory.vuint128 b (va_eval_heaplet va_s0 h) + 16
    `op_Multiply` index))
  (ensures (fun (va_sM, va_fM) -> va_ensure_total va_b0 va_s0 va_sM va_fM /\ va_get_ok va_sM /\
    va_eval_heaplet va_sM h == buffer128_write b index (Vale.Def.Types_s.reverse_bytes_quad32
    (va_eval_vec_opr va_s0 src)) (va_eval_heaplet va_s0 h) /\ 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_qattr]
let va_wp_Store128_byte16_buffer_index (h:va_operand_heaplet) (src:va_operand_vec_opr)
  (base:va_operand_reg_opr) (offset:va_operand_reg_opr) (t:taint) (b:buffer128) (index:int)
  (va_s0:va_state) (va_k:(va_state -> unit -> Type0)) : Type0 =
  (va_is_dst_heaplet h va_s0 /\ va_is_src_vec_opr src va_s0 /\ va_is_src_reg_opr base va_s0 /\
    va_is_src_reg_opr offset va_s0 /\ va_get_ok va_s0 /\ offset =!= 0 /\
    Vale.PPC64LE.Decls.valid_dst_addr #Vale.PPC64LE.Memory.vuint128 (va_eval_heaplet va_s0 h) b
    index /\ Vale.PPC64LE.Memory.valid_layout_buffer #Vale.PPC64LE.Memory.vuint128 b
    (va_get_mem_layout va_s0) (va_eval_heaplet va_s0 h) true /\
    Vale.PPC64LE.Memory.valid_taint_buf128 b (va_eval_heaplet va_s0 h) ((va_get_mem_layout
    va_s0).vl_taint) t /\ va_eval_reg_opr va_s0 base + va_eval_reg_opr va_s0 offset ==
    Vale.PPC64LE.Memory.buffer_addr #Vale.PPC64LE.Memory.vuint128 b (va_eval_heaplet va_s0 h) + 16
    `op_Multiply` index /\ (forall (va_x_h:va_value_heaplet) (va_x_mem:vale_heap) . let va_sM =
    va_upd_mem va_x_mem (va_upd_operand_heaplet h va_x_h va_s0) in va_get_ok va_sM /\
    va_eval_heaplet va_sM h == buffer128_write b index (Vale.Def.Types_s.reverse_bytes_quad32
    (va_eval_vec_opr va_s0 src)) (va_eval_heaplet va_s0 h) ==> va_k va_sM (())))

val va_wpProof_Store128_byte16_buffer_index : h:va_operand_heaplet -> src:va_operand_vec_opr ->
  base:va_operand_reg_opr -> offset:va_operand_reg_opr -> t:taint -> b:buffer128 -> index:int ->
  va_s0:va_state -> va_k:(va_state -> unit -> Type0)
  -> Ghost (va_state & va_fuel & unit)
  (requires (va_t_require va_s0 /\ va_wp_Store128_byte16_buffer_index h src base offset t b index
    va_s0 va_k))
  (ensures (fun (va_sM, va_f0, va_g) -> va_t_ensure (va_code_Store128_byte16_buffer_index h src
    base offset t) ([va_Mod_mem; va_mod_heaplet h]) va_s0 va_k ((va_sM, va_f0, va_g))))
[@ "opaque_to_smt" va_qattr]
let va_quick_Store128_byte16_buffer_index (h:va_operand_heaplet) (src:va_operand_vec_opr)
  (base:va_operand_reg_opr) (offset:va_operand_reg_opr) (t:taint) (b:buffer128) (index:int) :
  (va_quickCode unit (va_code_Store128_byte16_buffer_index h src base offset t)) =
  (va_QProc (va_code_Store128_byte16_buffer_index h src base offset t) ([va_Mod_mem; va_mod_heaplet
    h]) (va_wp_Store128_byte16_buffer_index h src base offset t b index)
    (va_wpProof_Store128_byte16_buffer_index h src base offset t b index))
//--
//-- SHA256_sigma0

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

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

val va_lemma_SHA256_sigma0 : va_b0:va_code -> va_s0:va_state -> dst:va_operand_vec_opr ->
  src:va_operand_vec_opr -> t:counter -> block:block_w
  -> Ghost (va_state & va_fuel)
  (requires (va_require_total va_b0 (va_code_SHA256_sigma0 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 /\ ((16 <= t && t < size_k_w_256)) /\
    (va_eval_vec_opr va_s0 src).hi3 == ws_opaque block (t - 15)))
  (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).hi3 == sigma_0_0_partial t block /\ 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_SHA256_sigma0 (dst:va_operand_vec_opr) (src:va_operand_vec_opr) (t:counter)
  (block:block_w) (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 /\ ((16 <= t && t
    < size_k_w_256)) /\ (va_eval_vec_opr va_s0 src).hi3 == ws_opaque block (t - 15) /\ (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).hi3 == sigma_0_0_partial t block ==> va_k va_sM
    (())))

val va_wpProof_SHA256_sigma0 : dst:va_operand_vec_opr -> src:va_operand_vec_opr -> t:counter ->
  block:block_w -> va_s0:va_state -> va_k:(va_state -> unit -> Type0)
  -> Ghost (va_state & va_fuel & unit)
  (requires (va_t_require va_s0 /\ va_wp_SHA256_sigma0 dst src t block va_s0 va_k))
  (ensures (fun (va_sM, va_f0, va_g) -> va_t_ensure (va_code_SHA256_sigma0 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_SHA256_sigma0 (dst:va_operand_vec_opr) (src:va_operand_vec_opr) (t:counter)
  (block:block_w) : (va_quickCode unit (va_code_SHA256_sigma0 dst src)) =
  (va_QProc (va_code_SHA256_sigma0 dst src) ([va_mod_vec_opr dst]) (va_wp_SHA256_sigma0 dst src t
    block) (va_wpProof_SHA256_sigma0 dst src t block))
//--
//-- SHA256_sigma1

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

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

val va_lemma_SHA256_sigma1 : va_b0:va_code -> va_s0:va_state -> dst:va_operand_vec_opr ->
  src:va_operand_vec_opr -> t:counter -> block:block_w
  -> Ghost (va_state & va_fuel)
  (requires (va_require_total va_b0 (va_code_SHA256_sigma1 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 /\ ((16 <= t && t < size_k_w_256)) /\
    (va_eval_vec_opr va_s0 src).hi3 == ws_opaque block (t - 2)))
  (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).hi3 == sigma_0_1_partial t block /\ 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_SHA256_sigma1 (dst:va_operand_vec_opr) (src:va_operand_vec_opr) (t:counter)
  (block:block_w) (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 /\ ((16 <= t && t
    < size_k_w_256)) /\ (va_eval_vec_opr va_s0 src).hi3 == ws_opaque block (t - 2) /\ (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).hi3 == sigma_0_1_partial t block ==> va_k va_sM
    (())))

val va_wpProof_SHA256_sigma1 : dst:va_operand_vec_opr -> src:va_operand_vec_opr -> t:counter ->
  block:block_w -> va_s0:va_state -> va_k:(va_state -> unit -> Type0)
  -> Ghost (va_state & va_fuel & unit)
  (requires (va_t_require va_s0 /\ va_wp_SHA256_sigma1 dst src t block va_s0 va_k))
  (ensures (fun (va_sM, va_f0, va_g) -> va_t_ensure (va_code_SHA256_sigma1 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_SHA256_sigma1 (dst:va_operand_vec_opr) (src:va_operand_vec_opr) (t:counter)
  (block:block_w) : (va_quickCode unit (va_code_SHA256_sigma1 dst src)) =
  (va_QProc (va_code_SHA256_sigma1 dst src) ([va_mod_vec_opr dst]) (va_wp_SHA256_sigma1 dst src t
    block) (va_wpProof_SHA256_sigma1 dst src t block))
//--
//-- SHA256_Sigma0

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

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

val va_lemma_SHA256_Sigma0 : va_b0:va_code -> va_s0:va_state -> dst:va_operand_vec_opr ->
  src:va_operand_vec_opr -> t:counter -> block:block_w -> hash_orig:hash256
  -> Ghost (va_state & va_fuel)
  (requires (va_require_total va_b0 (va_code_SHA256_Sigma0 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 /\ t < size_k_w_256 /\
    Vale.Def.Words_s.__proj__Mkfour__item__hi3 (va_eval_vec_opr va_s0 src) ==
    Vale.SHA.PPC64LE.SHA_helpers.word_to_nat32 (FStar.Seq.Base.index
    #Vale.SHA.PPC64LE.SHA_helpers.word (Vale.SHA.PPC64LE.SHA_helpers.repeat_range_vale t block
    hash_orig) 0)))
  (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__hi3 (va_eval_vec_opr va_sM dst) ==
    Vale.SHA.PPC64LE.SHA_helpers.sigma_1_0_partial t block hash_orig /\ 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_SHA256_Sigma0 (dst:va_operand_vec_opr) (src:va_operand_vec_opr) (t:counter)
  (block:block_w) (hash_orig:hash256) (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 /\ t <
    size_k_w_256 /\ Vale.Def.Words_s.__proj__Mkfour__item__hi3 (va_eval_vec_opr va_s0 src) ==
    Vale.SHA.PPC64LE.SHA_helpers.word_to_nat32 (FStar.Seq.Base.index
    #Vale.SHA.PPC64LE.SHA_helpers.word (Vale.SHA.PPC64LE.SHA_helpers.repeat_range_vale t block
    hash_orig) 0) /\ (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__hi3
    (va_eval_vec_opr va_sM dst) == Vale.SHA.PPC64LE.SHA_helpers.sigma_1_0_partial t block hash_orig
    ==> va_k va_sM (())))

val va_wpProof_SHA256_Sigma0 : dst:va_operand_vec_opr -> src:va_operand_vec_opr -> t:counter ->
  block:block_w -> hash_orig:hash256 -> va_s0:va_state -> va_k:(va_state -> unit -> Type0)
  -> Ghost (va_state & va_fuel & unit)
  (requires (va_t_require va_s0 /\ va_wp_SHA256_Sigma0 dst src t block hash_orig va_s0 va_k))
  (ensures (fun (va_sM, va_f0, va_g) -> va_t_ensure (va_code_SHA256_Sigma0 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_SHA256_Sigma0 (dst:va_operand_vec_opr) (src:va_operand_vec_opr) (t:counter)
  (block:block_w) (hash_orig:hash256) : (va_quickCode unit (va_code_SHA256_Sigma0 dst src)) =
  (va_QProc (va_code_SHA256_Sigma0 dst src) ([va_mod_vec_opr dst]) (va_wp_SHA256_Sigma0 dst src t
    block hash_orig) (va_wpProof_SHA256_Sigma0 dst src t block hash_orig))
//--
//-- SHA256_Sigma1

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

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

val va_lemma_SHA256_Sigma1 : va_b0:va_code -> va_s0:va_state -> dst:va_operand_vec_opr ->
  src:va_operand_vec_opr -> t:counter -> block:block_w -> hash_orig:hash256
  -> Ghost (va_state & va_fuel)
  (requires (va_require_total va_b0 (va_code_SHA256_Sigma1 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 /\ t < size_k_w_256 /\
    Vale.Def.Words_s.__proj__Mkfour__item__hi3 (va_eval_vec_opr va_s0 src) ==
    Vale.SHA.PPC64LE.SHA_helpers.word_to_nat32 (FStar.Seq.Base.index
    #Vale.SHA.PPC64LE.SHA_helpers.word (Vale.SHA.PPC64LE.SHA_helpers.repeat_range_vale t block
    hash_orig) 4)))
  (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__hi3 (va_eval_vec_opr va_sM dst) ==
    Vale.SHA.PPC64LE.SHA_helpers.sigma_1_1_partial t block hash_orig /\ 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_SHA256_Sigma1 (dst:va_operand_vec_opr) (src:va_operand_vec_opr) (t:counter)
  (block:block_w) (hash_orig:hash256) (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 /\ t <
    size_k_w_256 /\ Vale.Def.Words_s.__proj__Mkfour__item__hi3 (va_eval_vec_opr va_s0 src) ==
    Vale.SHA.PPC64LE.SHA_helpers.word_to_nat32 (FStar.Seq.Base.index
    #Vale.SHA.PPC64LE.SHA_helpers.word (Vale.SHA.PPC64LE.SHA_helpers.repeat_range_vale t block
    hash_orig) 4) /\ (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__hi3
    (va_eval_vec_opr va_sM dst) == Vale.SHA.PPC64LE.SHA_helpers.sigma_1_1_partial t block hash_orig
    ==> va_k va_sM (())))

val va_wpProof_SHA256_Sigma1 : dst:va_operand_vec_opr -> src:va_operand_vec_opr -> t:counter ->
  block:block_w -> hash_orig:hash256 -> va_s0:va_state -> va_k:(va_state -> unit -> Type0)
  -> Ghost (va_state & va_fuel & unit)
  (requires (va_t_require va_s0 /\ va_wp_SHA256_Sigma1 dst src t block hash_orig va_s0 va_k))
  (ensures (fun (va_sM, va_f0, va_g) -> va_t_ensure (va_code_SHA256_Sigma1 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_SHA256_Sigma1 (dst:va_operand_vec_opr) (src:va_operand_vec_opr) (t:counter)
  (block:block_w) (hash_orig:hash256) : (va_quickCode unit (va_code_SHA256_Sigma1 dst src)) =
  (va_QProc (va_code_SHA256_Sigma1 dst src) ([va_mod_vec_opr dst]) (va_wp_SHA256_Sigma1 dst src t
    block hash_orig) (va_wpProof_SHA256_Sigma1 dst src t block hash_orig))
//--
//-- Vsbox

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

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

val va_lemma_Vsbox : 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_Vsbox 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 == Vale.Def.Words_s.Mkfour #Vale.Def.Types_s.nat32
    (Vale.AES.AES_common_s.sub_word (Vale.Def.Words_s.__proj__Mkfour__item__lo0 (va_eval_vec_opr
    va_s0 src))) (Vale.AES.AES_common_s.sub_word (Vale.Def.Words_s.__proj__Mkfour__item__lo1
    (va_eval_vec_opr va_s0 src))) (Vale.AES.AES_common_s.sub_word
    (Vale.Def.Words_s.__proj__Mkfour__item__hi2 (va_eval_vec_opr va_s0 src)))
    (Vale.AES.AES_common_s.sub_word (Vale.Def.Words_s.__proj__Mkfour__item__hi3 (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_Vsbox (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 == Vale.Def.Words_s.Mkfour #Vale.Def.Types_s.nat32
    (Vale.AES.AES_common_s.sub_word (Vale.Def.Words_s.__proj__Mkfour__item__lo0 (va_eval_vec_opr
    va_s0 src))) (Vale.AES.AES_common_s.sub_word (Vale.Def.Words_s.__proj__Mkfour__item__lo1
    (va_eval_vec_opr va_s0 src))) (Vale.AES.AES_common_s.sub_word
    (Vale.Def.Words_s.__proj__Mkfour__item__hi2 (va_eval_vec_opr va_s0 src)))
    (Vale.AES.AES_common_s.sub_word (Vale.Def.Words_s.__proj__Mkfour__item__hi3 (va_eval_vec_opr
    va_s0 src))) ==> va_k va_sM (())))

val va_wpProof_Vsbox : 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_Vsbox dst src va_s0 va_k))
  (ensures (fun (va_sM, va_f0, va_g) -> va_t_ensure (va_code_Vsbox 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_Vsbox (dst:va_operand_vec_opr) (src:va_operand_vec_opr) : (va_quickCode unit
  (va_code_Vsbox dst src)) =
  (va_QProc (va_code_Vsbox dst src) ([va_mod_vec_opr dst]) (va_wp_Vsbox dst src) (va_wpProof_Vsbox
    dst src))
//--
//-- RotWord

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

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

val va_lemma_RotWord : 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_RotWord 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 /\
    (Vale.Def.Words_s.__proj__Mkfour__item__lo0 (va_eval_vec_opr va_s0 src2) == 8 /\
    Vale.Def.Words_s.__proj__Mkfour__item__lo1 (va_eval_vec_opr va_s0 src2) == 8 /\
    Vale.Def.Words_s.__proj__Mkfour__item__hi2 (va_eval_vec_opr va_s0 src2) == 8 /\
    Vale.Def.Words_s.__proj__Mkfour__item__hi3 (va_eval_vec_opr va_s0 src2) == 8)))
  (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.AES.AES_BE_s.rot_word (Vale.Def.Words_s.__proj__Mkfour__item__lo0 (va_eval_vec_opr va_s0
    src1))) (Vale.AES.AES_BE_s.rot_word (Vale.Def.Words_s.__proj__Mkfour__item__lo1
    (va_eval_vec_opr va_s0 src1))) (Vale.AES.AES_BE_s.rot_word
    (Vale.Def.Words_s.__proj__Mkfour__item__hi2 (va_eval_vec_opr va_s0 src1)))
    (Vale.AES.AES_BE_s.rot_word (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_RotWord (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 /\ (Vale.Def.Words_s.__proj__Mkfour__item__lo0 (va_eval_vec_opr va_s0 src2) ==
    8 /\ Vale.Def.Words_s.__proj__Mkfour__item__lo1 (va_eval_vec_opr va_s0 src2) == 8 /\
    Vale.Def.Words_s.__proj__Mkfour__item__hi2 (va_eval_vec_opr va_s0 src2) == 8 /\
    Vale.Def.Words_s.__proj__Mkfour__item__hi3 (va_eval_vec_opr va_s0 src2) == 8) /\ (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.AES.AES_BE_s.rot_word (Vale.Def.Words_s.__proj__Mkfour__item__lo0 (va_eval_vec_opr va_s0
    src1))) (Vale.AES.AES_BE_s.rot_word (Vale.Def.Words_s.__proj__Mkfour__item__lo1
    (va_eval_vec_opr va_s0 src1))) (Vale.AES.AES_BE_s.rot_word
    (Vale.Def.Words_s.__proj__Mkfour__item__hi2 (va_eval_vec_opr va_s0 src1)))
    (Vale.AES.AES_BE_s.rot_word (Vale.Def.Words_s.__proj__Mkfour__item__hi3 (va_eval_vec_opr va_s0
    src1))) ==> va_k va_sM (())))

val va_wpProof_RotWord : 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_RotWord dst src1 src2 va_s0 va_k))
  (ensures (fun (va_sM, va_f0, va_g) -> va_t_ensure (va_code_RotWord 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_RotWord (dst:va_operand_vec_opr) (src1:va_operand_vec_opr) (src2:va_operand_vec_opr) :
val va_quick_RotWord (dst src1 src2: va_operand_vec_opr)
    : (va_quickCode unit (va_code_RotWord dst src1 src2))

    dst: Vale.PPC64LE.Decls.va_operand_vec_opr ->
    src1: Vale.PPC64LE.Decls.va_operand_vec_opr ->
    src2: Vale.PPC64LE.Decls.va_operand_vec_opr
  -> Vale.PPC64LE.QuickCode.va_quickCode Prims.unit
      (Vale.PPC64LE.InsVector.va_code_RotWord dst src1 src2)