val check_if_consumes_fixed_time_outs
      (outs: list instr_out)
      (args: list instr_operand)
      (oprs: instr_operands_t outs args)
      (ts: analysis_taints)
      (t_out: taint)
    : Pure bool
      (requires True)
      (ensures
        fun b ->
          b ==>
          (forall (s1: S.machine_state) (s2: S.machine_state).
              {:pattern (constTimeInvariant ts.lts s1 s2)}
              constTimeInvariant ts.lts s1 s2 ==>
              obs_inouts outs args oprs s1 == obs_inouts outs args oprs s2))
let rec check_if_consumes_fixed_time_outs
    (outs:list instr_out) (args:list instr_operand) (oprs:instr_operands_t outs args)
    (ts:analysis_taints) (t_out:taint)
  : Pure bool
    (requires True)
    (ensures fun b -> b ==> (forall (s1 s2:S.machine_state).{:pattern (constTimeInvariant ts.lts s1 s2)}
      constTimeInvariant ts.lts s1 s2 ==> obs_inouts outs args oprs s1 == obs_inouts outs args oprs s2))
  =
  allow_inversion maddr;
  allow_inversion tmaddr;
  allow_inversion operand64;
  allow_inversion operand128;
  match outs with
  | [] -> check_if_consumes_fixed_time_args args oprs ts
  | (_, IOpEx i)::outs ->
    let ((o:instr_operand_t i), (oprs:instr_operands_t outs args)) = coerce oprs in
    let b' = check_if_consumes_fixed_time_outs_explicit i o ts t_out in
    let b'' = check_if_consumes_fixed_time_outs outs args oprs ts t_out in
    b' && b''
  | (_, IOpIm i)::outs ->
    let b' = check_if_consumes_fixed_time_outs_implicit i ts t_out in
    let b'' = check_if_consumes_fixed_time_outs outs args (coerce oprs) ts t_out in
    b' && b''
val check_if_consumes_fixed_time_outs
      (outs: list instr_out)
      (args: list instr_operand)
      (oprs: instr_operands_t outs args)
      (ts: analysis_taints)
      (t_out: taint)
    : Pure bool
      (requires True)
      (ensures
        fun b ->
          b ==>
          (forall (s1: S.machine_state) (s2: S.machine_state).
              {:pattern (constTimeInvariant ts.lts s1 s2)}
              constTimeInvariant ts.lts s1 s2 ==>
              obs_inouts outs args oprs s1 == obs_inouts outs args oprs s2))
let rec check_if_consumes_fixed_time_outs
      (outs: list instr_out)
      (args: list instr_operand)
      (oprs: instr_operands_t outs args)
      (ts: analysis_taints)
      (t_out: taint)
    : Pure bool
      (requires True)
      (ensures
        fun b ->
          b ==>
          (forall (s1: S.machine_state) (s2: S.machine_state).
              {:pattern (constTimeInvariant ts.lts s1 s2)}
              constTimeInvariant ts.lts s1 s2 ==>
              obs_inouts outs args oprs s1 == obs_inouts outs args oprs s2)) =
allow_inversion maddr;
allow_inversion tmaddr;
allow_inversion operand64;
allow_inversion operand128;
match outs with
| [] -> check_if_consumes_fixed_time_args args oprs ts
| (_, IOpEx i) :: outs ->
  let (o: instr_operand_t i), (oprs: instr_operands_t outs args) = coerce oprs in
  let b' = check_if_consumes_fixed_time_outs_explicit i o ts t_out in
  let b'' = check_if_consumes_fixed_time_outs outs args oprs ts t_out in
  b' && b''
| (_, IOpIm i) :: outs ->
  let b' = check_if_consumes_fixed_time_outs_implicit i ts t_out in
  let b'' = check_if_consumes_fixed_time_outs outs args (coerce oprs) ts t_out in
  b' && b''
Vale.X64.Leakage_Ins.fst.checked
Vale.X64.Machine_Semantics_s.fst.checked Vale.X64.Machine_s.fst.checked Vale.X64.Leakage_s.fst.checked Vale.X64.Leakage_Helpers.fst.checked Vale.X64.Instruction_s.fsti.checked Vale.X64.Bytes_Code_s.fst.checked Vale.Lib.Set.fsti.checked Vale.Lib.MapTree.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.Arch.Types.fsti.checked Vale.Arch.MachineHeap_s.fst.checked Vale.Arch.Heap.fsti.checked prims.fst.checked FStar.Set.fsti.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.Map.fsti.checked FStar.Classical.fsti.checked
Vale.X64.Leakage_Ins.fst
Prims.list Vale.X64.Instruction_s.instr_out Vale.X64.Instruction_s.instr_operand Vale.X64.Instruction_s.instr_operands_t Vale.X64.Leakage_Helpers.analysis_taints Vale.Arch.HeapTypes_s.taint Vale.X64.Leakage_Ins.check_if_consumes_fixed_time_args Vale.X64.Instruction_s.instr_operand_inout Vale.X64.Instruction_s.instr_operand_explicit Vale.X64.Instruction_s.instr_operand_t Prims.op_AmpAmp Prims.bool Vale.X64.Leakage_Ins.check_if_consumes_fixed_time_outs Vale.X64.Leakage_Ins.check_if_consumes_fixed_time_outs_explicit FStar.Pervasives.Native.tuple2 Vale.X64.Instruction_s.coerce Vale.X64.Instruction_s.instr_operand_implicit Vale.X64.Leakage_Ins.check_if_consumes_fixed_time_outs_implicit Prims.unit FStar.Pervasives.allow_inversion Vale.X64.Machine_s.operand128 Vale.X64.Machine_s.operand64 Vale.X64.Machine_s.tmaddr Vale.X64.Machine_s.maddr Prims.l_True Prims.l_imp Prims.b2t Prims.l_Forall Vale.X64.Machine_Semantics_s.machine_state Vale.X64.Leakage_s.constTimeInvariant Vale.X64.Leakage_Helpers.__proj__AnalysisTaints__item__lts Prims.eq2 Vale.X64.Machine_s.observation Vale.X64.Leakage_Ins.obs_inouts
module Vale.X64.Leakage_Ins
open FStar.Mul
open Vale.Arch.MachineHeap_s
open Vale.Arch.Heap
open Vale.X64.Machine_s
open Vale.X64.Instruction_s
module BC = Vale.X64.Bytes_Code_s
module S = Vale.X64.Machine_Semantics_s
open Vale.X64.Leakage_s
open Vale.X64.Leakage_Helpers

unfold let (.[]) = Map.sel
unfold let (.[]<-) = Map.upd

unfold let obs_args = S.obs_args
unfold let obs_inouts = S.obs_inouts
unfold let machine_eval_code = S.machine_eval_code

let reveal_machine_eval_code_ins (i:S.ins) (s:S.machine_state) : Lemma
  (requires True)
  (ensures S.machine_eval_code_ins i s == S.machine_eval_code_ins_def i s)
  [SMTPat (S.machine_eval_code_ins i s)]
  =
  reveal_opaque (`%S.machine_eval_code_ins) S.machine_eval_code_ins

let rec check_if_consumes_fixed_time_args
    (args:list instr_operand) (oprs:instr_operands_t_args args) (ts:analysis_taints)
  : Pure bool
    (requires True)
    (ensures fun b -> b ==> (forall (s1 s2:S.machine_state).{:pattern (constTimeInvariant ts.lts s1 s2)}
      constTimeInvariant ts.lts s1 s2 ==> obs_args args oprs s1 == obs_args args oprs s2))
  =
  allow_inversion maddr;
  allow_inversion tmaddr;
  match args with
  | [] -> true
  | (IOpEx i)::args ->
    let ((o:instr_operand_t i), (oprs:instr_operands_t_args args)) = coerce oprs in
    let b' =
      match i with
      | IOp64 -> operand_does_not_use_secrets #nat64 #reg_64 o ts
      | IOpXmm -> operand_does_not_use_secrets #quad32 #reg_xmm o ts
      in
    let b'' = check_if_consumes_fixed_time_args args oprs ts in
    b' && b''
  | (IOpIm i)::args ->
    let b' =
      match i with
      | IOp64One o -> operand_does_not_use_secrets o ts
      | IOpXmmOne o -> operand_does_not_use_secrets o ts
      | IOpFlagsCf -> true
      | IOpFlagsOf -> true
      in
    let b'' = check_if_consumes_fixed_time_args args (coerce oprs) ts in
    b' && b''

let check_if_consumes_fixed_time_outs_explicit
    (i:instr_operand_explicit) (o:instr_operand_t i)
    (ts:analysis_taints) (t_out:taint)
  : bool
  =
  match i with
  | IOp64 -> operand_does_not_use_secrets #nat64 #reg_64 o ts && operand_taint_allowed #nat64 #reg_64 o t_out
  | IOpXmm -> operand_does_not_use_secrets #quad32 #reg_xmm o ts && operand_taint_allowed #quad32 #reg_xmm o t_out

let check_if_consumes_fixed_time_outs_implicit
    (i:instr_operand_implicit) (ts:analysis_taints) (t_out:taint)
  : bool
  =
  match i with
  | IOp64One o -> operand_does_not_use_secrets o ts && operand_taint_allowed o t_out
  | IOpXmmOne o -> operand_does_not_use_secrets o ts && operand_taint_allowed o t_out
  | IOpFlagsCf -> true
  | IOpFlagsOf -> true

let rec check_if_consumes_fixed_time_outs
    (outs:list instr_out) (args:list instr_operand) (oprs:instr_operands_t outs args)
    (ts:analysis_taints) (t_out:taint)
  : Pure bool
    (requires True)
    (ensures fun b -> b ==> (forall (s1 s2:S.machine_state).{:pattern (constTimeInvariant ts.lts s1 s2)}
      constTimeInvariant ts.lts s1 s2 ==> obs_inouts outs args oprs s1 == obs_inouts outs args oprs s2))
val check_if_consumes_fixed_time_outs
      (outs: list instr_out)
      (args: list instr_operand)
      (oprs: instr_operands_t outs args)
      (ts: analysis_taints)
      (t_out: taint)
    : Pure bool
      (requires True)
      (ensures
        fun b ->
          b ==>
          (forall (s1: S.machine_state) (s2: S.machine_state).
              {:pattern (constTimeInvariant ts.lts s1 s2)}
              constTimeInvariant ts.lts s1 s2 ==>
              obs_inouts outs args oprs s1 == obs_inouts outs args oprs s2))

    outs: Prims.list Vale.X64.Instruction_s.instr_out ->
    args: Prims.list Vale.X64.Instruction_s.instr_operand ->
    oprs: Vale.X64.Instruction_s.instr_operands_t outs args ->
    ts: Vale.X64.Leakage_Helpers.analysis_taints ->
    t_out: Vale.Arch.HeapTypes_s.taint
  -> Prims.Pure Prims.bool