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

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

[@ "opaque_to_smt"]
val va_codegen_success_Vmr : dst:va_operand_vec_opr -> src:va_operand_vec_opr -> Tot va_pbool
dst: Vale.PPC64LE.Decls.va_operand_vec_opr -> src: Vale.PPC64LE.Decls.va_operand_vec_opr
  -> Vale.PPC64LE.Decls.va_pbool