val combine_leakage_taints (ts1 ts2: leakage_taints) : leakage_taints
let combine_leakage_taints (ts1:leakage_taints) (ts2:leakage_taints) : leakage_taints =
  let LeakageTaints rs1 fs1 c1 o1 = ts1 in
  let LeakageTaints rs2 fs2 c2 o2 = ts2 in
  let rs = combine_reg_taints rs1 rs2 in
  LeakageTaints
    rs
    (merge_taint fs1 fs2)
    (merge_taint c1 c2)
    (merge_taint o1 o2)
val combine_leakage_taints (ts1 ts2: leakage_taints) : leakage_taints
let combine_leakage_taints (ts1 ts2: leakage_taints) : leakage_taints =
let LeakageTaints rs1 fs1 c1 o1 = ts1 in
let LeakageTaints rs2 fs2 c2 o2 = ts2 in
let rs = combine_reg_taints rs1 rs2 in
LeakageTaints rs (merge_taint fs1 fs2) (merge_taint c1 c2) (merge_taint o1 o2)
Vale.X64.Leakage.fst.checked
Vale.X64.Machine_Semantics_s.fst.checked Vale.X64.Machine_s.fst.checked Vale.X64.Leakage_s.fst.checked Vale.X64.Leakage_Ins.fsti.checked Vale.X64.Leakage_Helpers.fst.checked Vale.Lib.MapTree.fsti.checked prims.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.FunctionalExtensionality.fsti.checked FStar.Classical.fsti.checked
Vale.X64.Leakage.fst
Vale.X64.Leakage_s.leakage_taints Vale.X64.Leakage_s.reg_taint Vale.Arch.HeapTypes_s.taint Vale.X64.Leakage_s.LeakageTaints Vale.X64.Leakage_Helpers.merge_taint Vale.X64.Leakage.combine_reg_taints
module Vale.X64.Leakage
open FStar.Mul
open Vale.X64.Machine_s
module S = Vale.X64.Machine_Semantics_s
open Vale.X64.Leakage_s
open Vale.X64.Leakage_Helpers
open Vale.X64.Leakage_Ins

unfold let machine_eval_ocmp = S.machine_eval_ocmp
unfold let machine_eval_code = S.machine_eval_code
unfold let machine_eval_codes = S.machine_eval_codes
unfold let machine_eval_while = S.machine_eval_while

#reset-options "--initial_ifuel 0 --max_ifuel 1 --initial_fuel 1 --max_fuel 1"

let normalize_taints (ts:analysis_taints) : analysis_taints =
  let AnalysisTaints lts rts = ts in
  AnalysisTaints lts (regs_to_map (map_to_regs rts))

let combine_reg_taints (regs1 regs2:reg_taint) : reg_taint =
  FunctionalExtensionality.on reg (fun x -> merge_taint (regs1 x) (regs2 x))

let rec eq_regs_file (regs1 regs2:reg_taint) (rf:reg_file_id) (k:nat{k <= n_regs rf}) : bool =
  if k = 0 then true
  else regs1 (Reg rf (k - 1)) = regs2 (Reg rf (k - 1)) && eq_regs_file regs1 regs2 rf (k - 1)

let rec eq_regs (regs1 regs2:reg_taint) (k:nat{k <= n_reg_files}) : bool =
  if k = 0 then true
  else eq_regs_file regs1 regs2 (k - 1) (n_regs (k - 1)) && eq_regs regs1 regs2 (k - 1)

let rec lemma_eq_regs_file (regs1 regs2:reg_taint) (rf:reg_file_id) (k:nat{k <= n_regs rf}) : Lemma
  (ensures eq_regs_file regs1 regs2 rf k <==>
    (forall (i:nat).{:pattern (Reg rf i)} i < k ==> regs1 (Reg rf i) == regs2 (Reg rf i)))
  =
  if k > 0 then lemma_eq_regs_file regs1 regs2 rf (k - 1)

let rec lemma_eq_regs (regs1 regs2:reg_taint) (k:nat{k <= n_reg_files}) : Lemma
  (ensures
    eq_regs regs1 regs2 k <==>
    (forall (i j:nat).{:pattern (Reg i j)} i < k /\ j < n_regs i ==>
      regs1 (Reg i j) == regs2 (Reg i j)))
  =
  if k > 0 then (
    lemma_eq_regs_file regs1 regs2 (k - 1) (n_regs (k - 1));
    lemma_eq_regs regs1 regs2 (k - 1)
  )

let eq_registers (regs1 regs2:reg_taint) : (b:bool{b <==> regs1 == regs2}) =
  lemma_eq_regs regs1 regs2 n_reg_files;
  let b = eq_regs regs1 regs2 n_reg_files in
  if b then (
    assert (FStar.FunctionalExtensionality.feq regs1 regs2)
  );
  b

let eq_leakage_taints (ts1 ts2:leakage_taints) : (b:bool{b <==> ts1 == ts2}) =
  eq_registers ts1.regTaint ts2.regTaint &&
  ts1.flagsTaint = ts2.flagsTaint &&
  ts1.cfFlagsTaint = ts2.cfFlagsTaint &&
  ts1.ofFlagsTaint = ts2.ofFlagsTaint

let taintstate_monotone_regs (ts ts':reg_taint) =
  (forall (r:reg).{:pattern (ts' r) \/ (ts r)}
    Public? (ts' r) ==> Public? (ts r))

let taintstate_monotone (ts ts':analysis_taints) =
  let ts = ts.lts in
  let ts' = ts'.lts in
  taintstate_monotone_regs ts.regTaint ts'.regTaint /\
  (Public? (ts'.flagsTaint) ==> Public? (ts.flagsTaint)) /\
  (Public? (ts'.cfFlagsTaint) ==> Public? (ts.cfFlagsTaint)) /\
  (Public? (ts'.ofFlagsTaint) ==> Public? (ts.ofFlagsTaint))

let taintstate_monotone_trans (ts1:analysis_taints) (ts2:analysis_taints) (ts3:analysis_taints)
  : Lemma (taintstate_monotone ts1 ts2 /\ taintstate_monotone ts2 ts3 ==> taintstate_monotone ts1 ts3) = ()

let isConstant_monotone (ts1:analysis_taints) (ts2:analysis_taints) (code:S.code) (fuel:nat) (s1:S.machine_state) (s2:S.machine_state)
  : Lemma (isConstantTimeGivenStates code fuel ts2.lts s1 s2 /\ taintstate_monotone ts1 ts2 ==> isConstantTimeGivenStates code fuel ts1.lts s1 s2)
  = ()

let isExplicit_monotone (ts:analysis_taints) (ts1:analysis_taints) (ts2:analysis_taints) (code:S.code)
  (fuel:nat) (s1:S.machine_state) (s2:S.machine_state)
  : Lemma (isExplicitLeakageFreeGivenStates code fuel ts.lts ts1.lts s1 s2 /\ taintstate_monotone ts1 ts2 ==> isExplicitLeakageFreeGivenStates code fuel ts.lts ts2.lts s1 s2)
  = ()

let isExplicit_monotone2 (ts:analysis_taints) (ts1:analysis_taints) (ts2:analysis_taints)
  (code:S.code) (fuel:nat) (s1:S.machine_state) (s2:S.machine_state)
  : Lemma (isExplicitLeakageFreeGivenStates code fuel ts2.lts ts.lts s1 s2 /\ taintstate_monotone ts1 ts2 ==> isExplicitLeakageFreeGivenStates code fuel ts1.lts ts.lts s1 s2)
  = ()
val combine_leakage_taints (ts1 ts2: leakage_taints) : leakage_taints
ts1: Vale.X64.Leakage_s.leakage_taints -> ts2: Vale.X64.Leakage_s.leakage_taints
  -> Vale.X64.Leakage_s.leakage_taints