val lemma_instr_write_outputs_ok
      (outs: list instr_out)
      (args: list instr_operand)
      (vs: instr_ret_t outs)
      (oprs: instr_operands_t outs args)
      (s_orig s: S.machine_state)
    : Lemma (requires (S.instr_write_outputs outs args vs oprs s_orig s).S.ms_ok)
      (ensures s.S.ms_ok)
let rec lemma_instr_write_outputs_ok
    (outs:list instr_out) (args:list instr_operand)
    (vs:instr_ret_t outs) (oprs:instr_operands_t outs args) (s_orig s:S.machine_state)
  : Lemma
    (requires (S.instr_write_outputs outs args vs oprs s_orig s).S.ms_ok)
    (ensures s.S.ms_ok)
  =
  match outs with
  | [] -> ()
  | (_, i)::outs ->
    (
      let ((v:instr_val_t i), (vs:instr_ret_t outs)) =
        match outs with
        | [] -> (vs, ())
        | _::_ -> let vs = coerce vs in (fst vs, snd vs)
        in
      match i with
      | IOpEx i ->
          let oprs:instr_operand_t i & instr_operands_t outs args = coerce oprs in
          let s' = S.instr_write_output_explicit i v (fst oprs) s_orig s in
          lemma_instr_write_outputs_ok outs args vs (snd oprs) s_orig s'
      | IOpIm i ->
          let s' = S.instr_write_output_implicit i v s_orig s in
          lemma_instr_write_outputs_ok outs args vs (coerce oprs) s_orig s'
    )
val lemma_instr_write_outputs_ok
      (outs: list instr_out)
      (args: list instr_operand)
      (vs: instr_ret_t outs)
      (oprs: instr_operands_t outs args)
      (s_orig s: S.machine_state)
    : Lemma (requires (S.instr_write_outputs outs args vs oprs s_orig s).S.ms_ok)
      (ensures s.S.ms_ok)
let rec lemma_instr_write_outputs_ok
      (outs: list instr_out)
      (args: list instr_operand)
      (vs: instr_ret_t outs)
      (oprs: instr_operands_t outs args)
      (s_orig s: S.machine_state)
    : Lemma (requires (S.instr_write_outputs outs args vs oprs s_orig s).S.ms_ok)
      (ensures s.S.ms_ok) =
match outs with
| [] -> ()
| (_, i) :: outs ->
  (let (v: instr_val_t i), (vs: instr_ret_t outs) =
      match outs with
      | [] -> (vs, ())
      | _ :: _ ->
        let vs = coerce vs in
        (fst vs, snd vs)
    in
    match i with
    | IOpEx i ->
      let oprs:instr_operand_t i & instr_operands_t outs args = coerce oprs in
      let s' = S.instr_write_output_explicit i v (fst oprs) s_orig s in
      lemma_instr_write_outputs_ok outs args vs (snd oprs) s_orig s'
    | IOpIm i ->
      let s' = S.instr_write_output_implicit i v s_orig s in
      lemma_instr_write_outputs_ok outs args vs (coerce oprs) s_orig s')
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_ret_t Vale.X64.Instruction_s.instr_operands_t Vale.X64.Machine_Semantics_s.machine_state Vale.X64.Instruction_s.instr_operand_inout Vale.X64.Instruction_s.instr_val_t Vale.X64.Instruction_s.instr_operand_explicit Vale.X64.Leakage_Ins.lemma_instr_write_outputs_ok FStar.Pervasives.Native.snd Vale.X64.Instruction_s.instr_operand_t Vale.X64.Machine_Semantics_s.instr_write_output_explicit FStar.Pervasives.Native.fst FStar.Pervasives.Native.tuple2 Vale.X64.Instruction_s.coerce Vale.X64.Instruction_s.instr_operand_implicit Vale.X64.Machine_Semantics_s.instr_write_output_implicit Prims.unit FStar.Pervasives.Native.Mktuple2 Prims.b2t Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_ok Vale.X64.Machine_Semantics_s.instr_write_outputs Prims.squash Prims.Nil FStar.Pervasives.pattern
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))
  =
  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''

#restart-solver
#reset-options "--z3rlimit 300"
let rec lemma_args_taint
    (outs:list instr_out) (args:list instr_operand)
    (f:instr_args_t outs args) (oprs:instr_operands_t_args args)
    (ts:analysis_taints) (s1 s2:S.machine_state)
  : Lemma
    (requires
      constTimeInvariant ts.lts s1 s2 /\
      Some? (S.instr_apply_eval_args outs args f oprs s1) /\
      Some? (S.instr_apply_eval_args outs args f oprs s2) /\
      check_if_consumes_fixed_time_args args oprs ts /\
      args_taint args oprs ts == Public)
    (ensures
      S.instr_apply_eval_args outs args f oprs s1 ==
      S.instr_apply_eval_args outs args f oprs s2)
  =
  allow_inversion maddr;
  allow_inversion tmaddr;
  allow_inversion operand64;
  allow_inversion operand128;
  match args with
  | [] -> ()
  | i::args ->
    let (v1, v2, oprs) : option (instr_val_t i) & option (instr_val_t i) & instr_operands_t_args args =
      match i with
      | IOpEx i ->
        let (o, (oprs:instr_operands_t_args args)) = coerce oprs in
        (
          S.instr_eval_operand_explicit i o s1,
          S.instr_eval_operand_explicit i o s2,
          oprs)
      | IOpIm i ->
        let oprs = coerce oprs in (
          S.instr_eval_operand_implicit i s1,
          S.instr_eval_operand_implicit i s2,
          oprs)
      in
    let f:arrow (instr_val_t i) (instr_args_t outs args) = coerce f in
    S.get_heap_val32_reveal ();
    S.get_heap_val64_reveal ();
    S.get_heap_val128_reveal ();
    assert (v1 == v2);
    let Some v = v1 in
    lemma_args_taint outs args (f v) oprs ts s1 s2

#restart-solver
let rec lemma_inouts_taint
    (outs inouts:list instr_out) (args:list instr_operand)
    (f:instr_inouts_t outs inouts args) (oprs:instr_operands_t inouts args)
    (ts:analysis_taints) (s1 s2:S.machine_state)
  : Lemma
    (requires
      constTimeInvariant ts.lts s1 s2 /\
      Some? (S.instr_apply_eval_inouts outs inouts args f oprs s1) /\
      Some? (S.instr_apply_eval_inouts outs inouts args f oprs s2) /\
      check_if_consumes_fixed_time_outs inouts args oprs ts Public /\
      inouts_taint inouts args oprs ts == Public)
    (ensures
      S.instr_apply_eval_inouts outs inouts args f oprs s1 ==
      S.instr_apply_eval_inouts outs inouts args f oprs s2)
  =
  allow_inversion maddr;
  allow_inversion tmaddr;
  allow_inversion operand64;
  allow_inversion operand128;
  match inouts with
  | [] -> lemma_args_taint outs args f oprs ts s1 s2
  | (Out, i)::inouts ->
    let oprs =
      match i with
      | IOpEx i -> snd #(instr_operand_t i) (coerce oprs)
      | IOpIm i -> coerce oprs
      in
    lemma_inouts_taint outs inouts args (coerce f) oprs ts s1 s2
  | (InOut, i)::inouts ->
    let (v1, v2, oprs) : option (instr_val_t i) & option (instr_val_t i) & instr_operands_t inouts args =
      match i with
      | IOpEx i ->
        let (o, (oprs:instr_operands_t inouts args)) = coerce oprs in
        let oprs = coerce oprs in (
          S.instr_eval_operand_explicit i o s1,
          S.instr_eval_operand_explicit i o s2,
          oprs)
      | IOpIm i ->
        let oprs = coerce oprs in (
          S.instr_eval_operand_implicit i s1,
          S.instr_eval_operand_implicit i s2,
          oprs)
      in
    let f:arrow (instr_val_t i) (instr_inouts_t outs inouts args) = coerce f in
    S.get_heap_val32_reveal ();
    S.get_heap_val64_reveal ();
    S.get_heap_val128_reveal ();
    assert (v1 == v2);
    let Some v = v1 in
    lemma_inouts_taint outs inouts args (f v) oprs ts s1 s2

let instr_set_taint_explicit
    (i:instr_operand_explicit) (o:instr_operand_t i) (ts:analysis_taints) (t:taint)
  : analysis_taints =
  match i with
  | IOp64 -> set_taint 0 (o <: operand64) ts t
  | IOpXmm -> set_taint 1 (o <: operand128) ts t

[@instr_attr]
let instr_set_taint_implicit (i:instr_operand_implicit) (ts:analysis_taints) (t:taint) : analysis_taints =
  match i with
  | IOp64One o -> set_taint 0 o ts t
  | IOpXmmOne o -> set_taint 1 o ts t
  | IOpFlagsCf -> set_taint_cf_and_flags ts t
  | IOpFlagsOf -> set_taint_of_and_flags ts t

let rec instr_set_taints
    (outs:list instr_out) (args:list instr_operand)
    (oprs:instr_operands_t outs args) (ts:analysis_taints) (t:taint)
  : analysis_taints =
  match outs with
  | [] -> ts
  | (_, i)::outs ->
    (
      match i with
      | IOpEx i ->
        let oprs:instr_operand_t i & instr_operands_t outs args = coerce oprs in
        instr_set_taints outs args (snd oprs) (instr_set_taint_explicit i (fst oprs) ts t) t
      | IOpIm i -> instr_set_taints outs args (coerce oprs) (instr_set_taint_implicit i ts t) t
    )

let rec lemma_instr_write_outputs_ok
    (outs:list instr_out) (args:list instr_operand)
    (vs:instr_ret_t outs) (oprs:instr_operands_t outs args) (s_orig s:S.machine_state)
  : Lemma
    (requires (S.instr_write_outputs outs args vs oprs s_orig s).S.ms_ok)
    (ensures s.S.ms_ok)
val lemma_instr_write_outputs_ok
      (outs: list instr_out)
      (args: list instr_operand)
      (vs: instr_ret_t outs)
      (oprs: instr_operands_t outs args)
      (s_orig s: S.machine_state)
    : Lemma (requires (S.instr_write_outputs outs args vs oprs s_orig s).S.ms_ok)
      (ensures s.S.ms_ok)

    outs: Prims.list Vale.X64.Instruction_s.instr_out ->
    args: Prims.list Vale.X64.Instruction_s.instr_operand ->
    vs: Vale.X64.Instruction_s.instr_ret_t outs ->
    oprs: Vale.X64.Instruction_s.instr_operands_t outs args ->
    s_orig: Vale.X64.Machine_Semantics_s.machine_state ->
    s: Vale.X64.Machine_Semantics_s.machine_state
  -> FStar.Pervasives.Lemma
      (requires
        Mkmachine_state?.ms_ok (Vale.X64.Machine_Semantics_s.instr_write_outputs outs
              args
              vs
              oprs
              s_orig
              s)) (ensures Mkmachine_state?.ms_ok s)