val eval_Cmovc64 (dst src: nat64) (carry: bool) : option nat64
let eval_Cmovc64 (dst src:nat64) (carry:bool) : option nat64 = Some (if carry then src else dst)
val eval_Cmovc64 (dst src: nat64) (carry: bool) : option nat64
let eval_Cmovc64 (dst src: nat64) (carry: bool) : option nat64 =
Some (if carry then src else dst)
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.bool FStar.Pervasives.Native.Some 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
val eval_Cmovc64 (dst src: nat64) (carry: bool) : option nat64
dst: Vale.X64.Machine_s.nat64 -> src: Vale.X64.Machine_s.nat64 -> carry: Prims.bool
  -> FStar.Pervasives.Native.option Vale.X64.Machine_s.nat64