val va_code_SHA256_rnds2 : dst:va_operand_xmm -> src:va_operand_xmm -> Tot va_code
let va_code_SHA256_rnds2 dst src =
  (mk_ins (make_instr (I.ins_SHA256_rnds2) (OReg dst) (OReg src)))
val va_code_SHA256_rnds2 : dst:va_operand_xmm -> src:va_operand_xmm -> Tot va_code
let va_code_SHA256_rnds2 dst src =
(mk_ins (make_instr (I.ins_SHA256_rnds2) (OReg dst) (OReg src)))
Vale.X64.InsSha.fst.checked
Vale.X64.Taint_Semantics.fst.checked Vale.X64.StateLemmas.fsti.checked Vale.X64.State.fsti.checked Vale.X64.Print_s.fst.checked Vale.X64.Machine_Semantics_s.fst.checked Vale.X64.Machine_s.fst.checked Vale.X64.Instructions_s.fsti.checked Vale.X64.InsLemmas.fsti.checked Vale.X64.Decls.fst.checked Vale.X64.Decls.fst.checked Vale.X64.CryptoInstructions_s.fsti.checked Vale.X64.CPU_Features_s.fst.checked Vale.Def.Types_s.fst.checked Spec.SHA2.fsti.checked Spec.Hash.Definitions.fst.checked prims.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked
Vale.X64.InsSha.fst
Vale.X64.Decls.va_operand_xmm Vale.X64.Taint_Semantics.mk_ins Vale.X64.InsLemmas.make_instr Prims.Cons Vale.X64.Instruction_s.instr_out Vale.X64.Instruction_s.inOut Vale.X64.Instruction_s.opXmm Prims.Nil Vale.X64.Instruction_s.instr_operand Vale.X64.Instruction_s.oneXmm Vale.X64.Machine_s.OReg Vale.X64.Machine_s.quad32 Vale.X64.Machine_s.reg_xmm Vale.X64.Instruction_s.PreserveFlags Vale.X64.Instructions_s.ins_SHA256_rnds2 Vale.X64.Decls.va_code
module Vale.X64.InsSha
open Vale.Def.Types_s
open Vale.X64.Machine_s
open Vale.X64
open Vale.X64.State
open Vale.X64.StateLemmas
open Vale.X64.InsLemmas
open Vale.X64.Taint_Semantics
open Vale.X64.Decls
open Vale.X64.CryptoInstructions_s
open Spec.Hash.Definitions
open Spec.SHA2
open Vale.X64.CPU_Features_s
module I = Vale.X64.Instructions_s
module S = Vale.X64.Machine_Semantics_s
module P = Vale.X64.Print_s

friend Vale.X64.Decls
#reset-options "--initial_fuel 4 --max_fuel 4 --max_ifuel 2 --z3rlimit 20"
//-- SHA256_rnds2

[@ "opaque_to_smt"]
val va_code_SHA256_rnds2 : dst:va_operand_xmm -> src:va_operand_xmm -> Tot va_code
dst: Vale.X64.Decls.va_operand_xmm -> src: Vale.X64.Decls.va_operand_xmm -> Vale.X64.Decls.va_code