val eval_Psrldq (amt: int) (dst: quad32) : option quad32
let eval_Psrldq (amt:int) (dst:quad32) : option quad32 = check_sse2 (
  if 0 <= amt && amt < 16 then
    let src_bytes = le_quad32_to_bytes dst in
    let zero_pad = Seq.create amt 0 in
    let remaining_bytes = slice src_bytes amt (length src_bytes) in
    Some (le_bytes_to_quad32 (append zero_pad remaining_bytes))
  else None)
val eval_Psrldq (amt: int) (dst: quad32) : option quad32
let eval_Psrldq (amt: int) (dst: quad32) : option quad32 =
check_sse2 (if 0 <= amt && amt < 16
    then
      let src_bytes = le_quad32_to_bytes dst in
      let zero_pad = Seq.create amt 0 in
      let remaining_bytes = slice src_bytes amt (length src_bytes) in
      Some (le_bytes_to_quad32 (append zero_pad remaining_bytes))
    else None)
Vale.X64.Instructions_s.fsti.checked
Vale.X64.Machine_s.fst.checked Vale.X64.Instruction_s.fsti.checked Vale.X64.CryptoInstructions_s.fsti.checked Vale.X64.CPU_Features_s.fst.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.Four_s.fsti.checked Vale.Def.Types_s.fst.checked Vale.AES.AES_s.fst.checked prims.fst.checked FStar.UInt.fsti.checked FStar.Seq.Base.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked
Vale.X64.Instructions_s.fsti
Prims.int Vale.X64.Machine_s.quad32 Vale.X64.Instructions_s.check_sse2 Prims.op_AmpAmp Prims.op_LessThanOrEqual Prims.op_LessThan FStar.Pervasives.Native.Some Vale.Def.Types_s.le_bytes_to_quad32 FStar.Seq.Base.append Vale.Def.Types_s.nat8 FStar.Seq.Base.seq Vale.Def.Words_s.nat8 FStar.Seq.Base.slice FStar.Seq.Base.length FStar.Seq.Base.create Vale.Def.Types_s.le_quad32_to_bytes Prims.bool FStar.Pervasives.Native.None FStar.Pervasives.Native.option
module Vale.X64.Instructions_s
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.X64.Machine_s
open Vale.X64.Instruction_s
open Vale.X64.CPU_Features_s
open Vale.X64.CryptoInstructions_s
open FStar.Seq.Base

let eval_Mov64 (src:nat64) : option nat64 = Some src
val ins_Mov64 : instr_dep [out op64] [op64] PreserveFlags eval_Mov64

let eval_MovBe64 (src:nat64) : option nat64 = if movbe_enabled then Some (reverse_bytes_nat64 src) else None
val ins_MovBe64 : instr_dep [out op64] [op64] PreserveFlags eval_MovBe64

let eval_Bswap64 (dst:nat64) : option nat64 = Some (reverse_bytes_nat64 dst)
val ins_Bswap64 : instr_dep [inOut op64] [] PreserveFlags eval_Bswap64

let eval_Cmovc64 (dst src:nat64) (carry:bool) : option nat64 = Some (if carry then src else dst)
val ins_Cmovc64 : instr_dep [inOut op64] [op64; opFlagsCf] PreserveFlags eval_Cmovc64

let eval_Add64 (dst src:nat64) : option (bool & nat64) =
  let sum = dst + src in Some (sum >= pow2_64, sum % pow2_64)
val ins_Add64 : instr_dep [out opFlagsCf; inOut op64] [op64] HavocFlags eval_Add64

let eval_AddLea64 (src1 src2:nat64) : option nat64 = Some ((src1 + src2) % pow2_64)
val ins_AddLea64 :instr_dep [out op64] [op64; op64] PreserveFlags eval_AddLea64

let eval_AddCarry64 (old_carry:bool) (dst src:nat64) : option (bool & nat64) =
  let sum = dst + src + (if old_carry then 1 else 0) in
  Some (sum >= pow2_64, sum % pow2_64)
val ins_AddCarry64 : instr_dep [inOut opFlagsCf; inOut op64] [op64] HavocFlags eval_AddCarry64

let eval_Adcx64_Adox64 (old_flag:bool) (dst src:nat64) : option (bool & nat64) =
  let sum = dst + src + (if old_flag then 1 else 0) in
  if adx_enabled then Some (sum >= pow2_64, sum % pow2_64) else None
val ins_Adcx64 : instr_dep [inOut opFlagsCf; inOut op64] [op64] PreserveFlags eval_Adcx64_Adox64
val ins_Adox64 : instr_dep [inOut opFlagsOf; inOut op64] [op64] PreserveFlags eval_Adcx64_Adox64

let eval_Sub64 (dst src:nat64) : option (bool & nat64) =
  let diff = dst - src in Some (diff < 0, diff % pow2_64)
val ins_Sub64 : instr_dep [out opFlagsCf; inOut op64] [op64] HavocFlags eval_Sub64

let eval_Sbb64 (old_carry:bool) (dst src:nat64) : option (bool & nat64) =
  let diff = dst - (src + (if old_carry then 1 else 0)) in
  Some (diff < 0, diff % pow2_64) // We specify cf, but underspecify everything else (via HavocFlags)
val ins_Sbb64 : instr_dep [inOut opFlagsCf; inOut op64] [op64] HavocFlags eval_Sbb64

let eval_Mul64 (rax src:nat64) : option (nat64 & nat64) =
  Some (FStar.UInt.mul_div #64 rax src, FStar.UInt.mul_mod #64 rax src)
val ins_Mul64 : instr_dep [out (one64Reg rRdx); inOut (one64Reg rRax)] [op64] HavocFlags eval_Mul64

let eval_Mulx64 (rdx src:nat64) : option (nat64 & nat64) =
  let hi = FStar.UInt.mul_div #64 rdx src in
  let lo = FStar.UInt.mul_mod #64 rdx src in
  if bmi2_enabled then Some (hi, lo) else None
val ins_Mulx64 : instr_dep [out op64; out op64] [one64Reg rRdx; op64] PreserveFlags eval_Mulx64

let eval_IMul64 (dst src:nat64) : option nat64 =
  Some (FStar.UInt.mul_mod #64 dst src)
val ins_IMul64 : instr_dep [inOut op64] [op64] HavocFlags eval_IMul64

let eval_And64 (dst src:nat64) : option nat64 = Some (iand dst src)
val ins_And64 : instr_dep [inOut op64] [op64] HavocFlags eval_And64

let eval_Xor64 (dst src:nat64) : option (nat64 & (bool & bool)) =
  Some (Vale.Def.Types_s.ixor dst src, (false, false))
val ins_Xor64 : instr_dep [inOut op64; out opFlagsCf; out opFlagsOf] [op64] HavocFlags eval_Xor64

let eval_Shr64 (dst amt:nat64) : option nat64 =
  if amt < 64 then Some (Vale.Def.Types_s.ishr dst amt) else None
val ins_Shr64 : instr_dep [inOut op64] [op64] HavocFlags eval_Shr64

let eval_Shl64 (dst amt:nat64) : option nat64 =
  if amt < 64 then Some (Vale.Def.Types_s.ishl dst amt) else None
val ins_Shl64 : instr_dep [inOut op64] [op64] HavocFlags eval_Shl64

let eval_Cpuid (rax rcx:nat64) : option (nat64 & (nat64 & (nat64 & nat64))) =
  Some (cpuid rRax rax rcx, (cpuid rRbx rax rcx, (cpuid rRcx rax rcx, cpuid rRdx rax rcx)))
val ins_Cpuid :
  instr_dep
    [inOut (one64Reg rRax); out (one64Reg rRbx); inOut (one64Reg rRcx); out (one64Reg rRdx)]
    [] PreserveFlags eval_Cpuid

// The XGETBV instruction requires that OSXSAVE (in CPUID) is enabled.
// We underspecify XGETBV here to only support fetching XCR0, which
// is supported on any processor supporting the XGETBV instruction
let eval_Xgetbv (rcx:nat64) : option (nat64 & nat64) =
  if osxsave_enabled && rcx = 0 then Some (xgetbv rRax rcx, xgetbv rRdx rcx) else None
val ins_Xgetbv :
  instr_dep
    [out (one64Reg rRax); out (one64Reg rRdx)]
    [one64Reg rRcx] PreserveFlags eval_Xgetbv

let check_avx (#a:Type0) (x:option a) : option a =
  if avx_enabled then x else None

let check_sse2 (#a:Type0) (x:option a) : option a =
  if sse2_enabled then x else None

let check_ssse3 (#a:Type0) (x:option a) : option a =
  if ssse3_enabled then x else None

let check_sse4_1 (#a:Type0) (x:option a) : option a =
  if sse4_1_enabled then x else None

let eval_Movdqu (src:quad32) : option quad32 = check_sse2 (Some src)
val ins_Movdqu : instr_dep [out opXmm] [opXmm] PreserveFlags eval_Movdqu

let eval_Pxor (dst src:quad32) : option quad32 = check_sse2 (Some (quad32_xor dst src))
val ins_Pxor : instr_dep [inOut opXmm] [opXmm] PreserveFlags eval_Pxor

let eval_VPxor (src1 src2:quad32) : option quad32 = check_avx (Some (quad32_xor src1 src2))
val ins_VPxor : instr_dep [out opXmm] [opXmm; opXmm] PreserveFlags eval_VPxor

let eval_Pand (dst src:quad32) : option quad32 = check_sse2 (Some (four_map2 (fun di si -> iand di si) dst src))
val ins_Pand : instr_dep [inOut opXmm] [opXmm] PreserveFlags eval_Pand

let eval_Paddd_raw (src1 src2:quad32) : option quad32 =
  Some (Mkfour
    ((src1.lo0 + src2.lo0) % pow2_32)
    ((src1.lo1 + src2.lo1) % pow2_32)
    ((src1.hi2 + src2.hi2) % pow2_32)
    ((src1.hi3 + src2.hi3) % pow2_32))

let eval_Paddd (src1 src2:quad32) : option quad32 = check_sse2 (eval_Paddd_raw src1 src2)
val ins_Paddd : instr_dep [inOut opXmm] [opXmm] PreserveFlags eval_Paddd

let eval_VPaddd (src1 src2:quad32) : option quad32 = check_avx (eval_Paddd_raw src1 src2)
val ins_VPaddd : instr_dep [out opXmm] [opXmm; opXmm] PreserveFlags eval_VPaddd

let eval_Pslld (amt:int) (dst:quad32) : option quad32 =
  check_sse2 (if 0 <= amt && amt < 32 then Some (four_map (fun i -> ishl i amt) dst) else None)
val ins_Pslld (amt:int) : instr_dep [inOut opXmm] [] PreserveFlags (eval_Pslld amt)

let eval_Psrld (amt:int) (dst:quad32) : option quad32 =
  check_sse2 (if 0 <= amt && amt < 32 then Some (four_map (fun i -> ishr i amt) dst) else None)
val ins_Psrld (amt:int) : instr_dep [inOut opXmm] [] PreserveFlags (eval_Psrld amt)
val eval_Psrldq (amt: int) (dst: quad32) : option quad32
amt: Prims.int -> dst: Vale.X64.Machine_s.quad32
  -> FStar.Pervasives.Native.option Vale.X64.Machine_s.quad32