val instr_operands_t (outs: list instr_out) (args: list instr_operand) : Type0
let rec instr_operands_t (outs:list instr_out) (args:list instr_operand) : Type0 =
  match outs with
  | [] -> instr_operands_t_args args
  | (_, IOpEx i)::outs -> instr_operand_t i & instr_operands_t outs args
  | (_, IOpIm _)::outs -> instr_operands_t outs args
val instr_operands_t (outs: list instr_out) (args: list instr_operand) : Type0
let rec instr_operands_t (outs: list instr_out) (args: list instr_operand) : Type0 =
match outs with
| [] -> instr_operands_t_args args
| (_, IOpEx i) :: outs -> instr_operand_t i & instr_operands_t outs args
| (_, IOpIm _) :: outs -> instr_operands_t outs args
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
Prims.list Vale.X64.Instruction_s.instr_out Vale.X64.Instruction_s.instr_operand Vale.X64.Instruction_s.instr_operands_t_args Vale.X64.Instruction_s.instr_operand_inout Vale.X64.Instruction_s.instr_operand_explicit FStar.Pervasives.Native.tuple2 Vale.X64.Instruction_s.instr_operand_t Vale.X64.Instruction_s.instr_operands_t Vale.X64.Instruction_s.instr_operand_implicit
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)
[@instr_attr] unfold let one64Reg (r:reg_64) = IOpIm (IOp64One (OReg r))
[@instr_attr] unfold let oneXmm (o:operand128) = IOpIm (IOpXmmOne o)
[@instr_attr] unfold let opFlagsCf = IOpIm IOpFlagsCf
[@instr_attr] unfold let opFlagsOf = IOpIm IOpFlagsOf

[@instr_attr]
let instr_val_t (o:instr_operand) : Type0 =
  match o with
  | IOpEx IOp64 | IOpIm (IOp64One _) -> nat64
  | IOpEx IOpXmm | IOpIm (IOpXmmOne _) -> quad32
  | IOpIm IOpFlagsCf -> bool
  | IOpIm IOpFlagsOf -> bool

[@instr_attr]
let rec instr_ret_t (outs:list instr_out) : Type0 =
  match outs with
  | [] -> unit
  | [(_, o)] -> instr_val_t o
  | (_, o)::outs -> instr_val_t o & instr_ret_t outs

[@instr_attr]
let rec instr_args_t (outs:list instr_out) (args:list instr_operand) : Type0 =
  match args with
  | [] -> option (instr_ret_t outs)
  | i::args -> arrow (instr_val_t i) (instr_args_t outs args)

[@instr_attr]
let rec instr_inouts_t (outs inouts:list instr_out) (args:list instr_operand) : Type0 =
  match inouts with
  | [] -> instr_args_t outs args
  | (Out, _)::inouts -> instr_inouts_t outs inouts args
  | (InOut, i)::inouts -> arrow (instr_val_t i) (instr_inouts_t outs inouts args)

(*
An instr evaluator is a function of type:
  in_outs1 ... ->  in_outsi -> args1 -> ...> argsj -> (outs1 & (... & outsk) ...)
where in_outs = [(b, o) in outs | b = InOut]
*)
[@instr_attr]
let instr_eval_t (outs:list instr_out) (args:list instr_operand) : Type0 =
  instr_inouts_t outs outs args

[@instr_attr]
let instr_operand_t (arg:instr_operand_explicit) : Type0 =
  match arg with
  | IOp64 -> operand64
  | IOpXmm -> operand128

[@instr_attr]
let rec instr_operands_t_args (args:list instr_operand) : Type0 =
  match args with
  | [] -> unit
  | (IOpEx i)::args -> instr_operand_t i & instr_operands_t_args args
  | (IOpIm _)::args -> instr_operands_t_args args

[@instr_attr]
val instr_operands_t (outs: list instr_out) (args: list instr_operand) : Type0

    outs: Prims.list Vale.X64.Instruction_s.instr_out ->
    args: Prims.list Vale.X64.Instruction_s.instr_operand
  -> Type0