val make_instr_outs
      (outs: list instr_out)
      (args: list instr_operand)
      (k: arrow (instr_operands_t outs args) S.ins)
    : make_instr_t outs args
let rec make_instr_outs
    (outs:list instr_out) (args:list instr_operand) (k:arrow (instr_operands_t outs args) S.ins)
  : make_instr_t outs args =
  match outs with
  | [] -> make_instr_args args k
  | (b, IOpEx i)::outs -> fun (o:instr_operand_t i) ->
      let k = coerce #(arrow (instr_operand_t i & instr_operands_t outs args) S.ins) k in // REVIEW: workaround for F* -> OCaml bug
      let k (oprs:instr_operands_t outs args) = k (o, oprs) in
      make_instr_outs outs args k
  | (_, IOpIm i)::outs -> coerce (make_instr_outs outs args (coerce #(arrow (instr_operands_t outs args) S.ins) k))
val make_instr_outs
      (outs: list instr_out)
      (args: list instr_operand)
      (k: arrow (instr_operands_t outs args) S.ins)
    : make_instr_t outs args
let rec make_instr_outs
      (outs: list instr_out)
      (args: list instr_operand)
      (k: arrow (instr_operands_t outs args) S.ins)
    : make_instr_t outs args =
match outs with
| [] -> make_instr_args args k
| (b, IOpEx i) :: outs ->
  fun (o: instr_operand_t i) ->
    let k = coerce #(arrow (instr_operand_t i & instr_operands_t outs args) S.ins) k in
    let k (oprs: instr_operands_t outs args) = k (o, oprs) in
    make_instr_outs outs args k
| (_, IOpIm i) :: outs ->
  coerce (make_instr_outs outs args (coerce #(arrow (instr_operands_t outs args) S.ins) k))
Vale.X64.InsLemmas.fsti.checked
Vale.X64.StateLemmas.fsti.checked Vale.X64.State.fsti.checked Vale.X64.Memory.fsti.checked Vale.X64.Machine_Semantics_s.fst.checked Vale.X64.Machine_s.fst.checked Vale.X64.Instruction_s.fsti.checked Vale.X64.Decls.fsti.checked Vale.X64.Bytes_Code_s.fst.checked Vale.Arch.HeapImpl.fsti.checked prims.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked
Vale.X64.InsLemmas.fsti
Prims.list Vale.X64.Instruction_s.instr_out Vale.X64.Instruction_s.instr_operand Vale.X64.Instruction_s.arrow Vale.X64.Instruction_s.instr_operands_t Vale.X64.Machine_Semantics_s.ins Vale.X64.InsLemmas.make_instr_args Vale.X64.Instruction_s.instr_operand_inout Vale.X64.Instruction_s.instr_operand_explicit Vale.X64.Instruction_s.instr_operand_t Vale.X64.InsLemmas.make_instr_outs FStar.Pervasives.Native.Mktuple2 FStar.Pervasives.Native.tuple2 Vale.X64.StateLemmas.coerce Vale.X64.InsLemmas.make_instr_t Vale.X64.Instruction_s.instr_operand_implicit
module Vale.X64.InsLemmas

open FStar.Mul
open Vale.Arch.HeapImpl
open Vale.X64.Machine_s
open Vale.X64.Instruction_s
open Vale.X64.State
open Vale.X64.StateLemmas
open Vale.X64.Decls
open Vale.X64.Memory
module BC = Vale.X64.Bytes_Code_s
module S = Vale.X64.Machine_Semantics_s
let has_taint128 (o:operand128) (t:taint) : bool =
  match o with
  | OMem (_, t') | OStack (_, t') -> t = t'
  | _ -> true

val lemma_valid_src_operand64_and_taint (o:operand64) (s:vale_state) : Lemma
  (requires valid_operand o s)
  (ensures S.valid_src_operand64_and_taint o (state_to_S s))
  [SMTPat (S.valid_src_operand64_and_taint o (state_to_S s))]

val lemma_valid_src_operand128_and_taint (o:operand128) (s:vale_state) : Lemma
  (requires valid_operand128 o s)
  (ensures S.valid_src_operand128_and_taint o (state_to_S s))
  [SMTPat (S.valid_src_operand128_and_taint o (state_to_S s))]

[@instr_attr]
let rec make_instr_t_args (args:list instr_operand) : Type0 =
  match normal args with
  | [] -> S.ins
  | (IOpEx i)::args -> arrow (instr_operand_t i) (make_instr_t_args args)
  | (IOpIm _)::args -> make_instr_t_args args

[@instr_attr]
let rec make_instr_t (outs:list instr_out) (args:list instr_operand) : Type0 =
  match normal outs with
  | [] -> make_instr_t_args args
  | (_, IOpEx i)::outs -> arrow (instr_operand_t i) (make_instr_t outs args)
  | (_, IOpIm _)::outs -> make_instr_t outs args

[@instr_attr]
let rec make_instr_args
    (args:list instr_operand) (k:arrow (instr_operands_t_args args) S.ins)
  : make_instr_t_args args =
  match args with
  | [] -> k ()
  | (IOpEx i)::args -> fun (o:instr_operand_t i) ->
      let k = coerce #(arrow (instr_operand_t i & instr_operands_t_args args) S.ins) k in // REVIEW: workaround for F* -> OCaml bug
      let k (oprs:instr_operands_t_args args) : S.ins = k (o, oprs) in
      make_instr_args args k
  | (IOpIm i)::args -> coerce (make_instr_args args (coerce #(arrow (instr_operands_t_args args) S.ins) k))

[@instr_attr]
let rec make_instr_outs
    (outs:list instr_out) (args:list instr_operand) (k:arrow (instr_operands_t outs args) S.ins)
val make_instr_outs
      (outs: list instr_out)
      (args: list instr_operand)
      (k: arrow (instr_operands_t outs args) S.ins)
    : make_instr_t outs args

    outs: Prims.list Vale.X64.Instruction_s.instr_out ->
    args: Prims.list Vale.X64.Instruction_s.instr_operand ->
    k:
      Vale.X64.Instruction_s.arrow (Vale.X64.Instruction_s.instr_operands_t outs args)
        Vale.X64.Machine_Semantics_s.ins
  -> Vale.X64.InsLemmas.make_instr_t outs args