val va_quick_Mfvsrd (dst: va_operand_reg_opr) (src: va_operand_vec_opr)
    : (va_quickCode unit (va_code_Mfvsrd dst src))
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))
val va_quick_Mfvsrd (dst: va_operand_reg_opr) (src: va_operand_vec_opr)
    : (va_quickCode unit (va_code_Mfvsrd dst src))
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))
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_reg_opr Vale.PPC64LE.Decls.va_operand_vec_opr Vale.PPC64LE.QuickCode.va_QProc Prims.unit Vale.PPC64LE.InsVector.va_code_Mfvsrd Prims.Cons Vale.PPC64LE.QuickCode.mod_t Vale.PPC64LE.QuickCode.va_mod_reg_opr Prims.Nil Vale.PPC64LE.InsVector.va_wp_Mfvsrd Vale.PPC64LE.InsVector.va_wpProof_Mfvsrd 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
val va_quick_Mfvsrd (dst: va_operand_reg_opr) (src: va_operand_vec_opr)
    : (va_quickCode unit (va_code_Mfvsrd dst src))
dst: Vale.PPC64LE.Decls.va_operand_reg_opr -> src: Vale.PPC64LE.Decls.va_operand_vec_opr
  -> Vale.PPC64LE.QuickCode.va_quickCode Prims.unit (Vale.PPC64LE.InsVector.va_code_Mfvsrd dst src)