val eval_Shl64 (dst amt: nat64) : option nat64
let eval_Shl64 (dst amt:nat64) : option nat64 =
  if amt < 64 then Some (Vale.Def.Types_s.ishl dst amt) else None
val eval_Shl64 (dst amt: nat64) : option nat64
let eval_Shl64 (dst amt: nat64) : option nat64 =
if amt < 64 then Some (Vale.Def.Types_s.ishl dst amt) 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
Vale.X64.Machine_s.nat64 Prims.op_LessThan FStar.Pervasives.Native.Some Vale.Def.Types_s.ishl Vale.Def.Words_s.pow2_64 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
val eval_Shl64 (dst amt: nat64) : option nat64
dst: Vale.X64.Machine_s.nat64 -> amt: Vale.X64.Machine_s.nat64
  -> FStar.Pervasives.Native.option Vale.X64.Machine_s.nat64