let oneXmm (o:operand128) = IOpIm (IOpXmmOne o)
let oneXmm (o: operand128) =
IOpIm (IOpXmmOne o)
Vale.X64.Instruction_s.fsti.checked
Vale.X64.Machine_s.fst.checked Vale.Def.Words_s.fsti.checked Vale.Def.Types_s.fst.checked prims.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked
Vale.X64.Instruction_s.fsti
Vale.X64.Machine_s.operand128 Vale.X64.Instruction_s.IOpIm Vale.X64.Instruction_s.IOpXmmOne Vale.X64.Instruction_s.instr_operand
module Vale.X64.Instruction_s
open FStar.Mul
open Vale.Def.Words_s
open Vale.Def.Types_s
open Vale.X64.Machine_s

(*
An generic instruction has:
- zero or more input operands
- zero or more output operands or input/output operands
- a possible effect on the status flags
Some of the operands may be hard-coded to a particular register; other operands are flexible.
For example, the Intel 64-bit MUL instruction, which executes "(RDX:RAX) := RAX * src" has:
- one hard-coded input/output operand, the flags
  - note: the instruction can havoc the flags in addition to or instead of specifying a flags operand
- one hard-coded output operand, RDX
- one hard-coded input/output operand, RAX
- one flexible input operand (src)
*)
type instr_operand_inout = | InOut | Out
type instr_operand_explicit = // flexible operand
  | IOp64 : instr_operand_explicit
  | IOpXmm : instr_operand_explicit
type instr_operand_implicit = // hard-coded operand
  | IOp64One : o:operand64 -> instr_operand_implicit
  | IOpXmmOne : o:operand128 -> instr_operand_implicit
  | IOpFlagsCf : instr_operand_implicit
  | IOpFlagsOf : instr_operand_implicit
type instr_operand =
  | IOpEx : instr_operand_explicit -> instr_operand
  | IOpIm : instr_operand_implicit -> instr_operand
let instr_out = instr_operand_inout & instr_operand

irreducible let instr_attr = ()
unfold let normal (#a:Type) (x:a) : a = norm [zeta; iota; delta_attr [`%instr_attr]] x

let arrow (a b:Type) = a -> b
[@instr_attr] unfold let coerce (#b #a:Type) (x:a{a == b}) : b = x

[@instr_attr] unfold let inOut (o:instr_operand) = (InOut, o)
[@instr_attr] unfold let out (o:instr_operand) = (Out, o)
[@instr_attr] unfold let op64 = IOpEx IOp64
[@instr_attr] unfold let opXmm = IOpEx IOpXmm
[@instr_attr] unfold let one64 (o:operand64) = IOpIm (IOp64One o)
val oneXmm : o: Vale.X64.Machine_s.operand128 -> Vale.X64.Instruction_s.instr_operand
o: Vale.X64.Machine_s.operand128 -> Vale.X64.Instruction_s.instr_operand