val normalize_taints (ts: analysis_taints) : analysis_taints
let normalize_taints (ts:analysis_taints) : analysis_taints =
  let AnalysisTaints lts rts = ts in
  AnalysisTaints lts (regs_to_map (map_to_regs rts))
val normalize_taints (ts: analysis_taints) : analysis_taints
let normalize_taints (ts: analysis_taints) : analysis_taints =
let AnalysisTaints lts rts = ts in
AnalysisTaints lts (regs_to_map (map_to_regs rts))
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_Helpers.analysis_taints Vale.X64.Leakage_s.leakage_taints Vale.X64.Leakage_Helpers.regmap Vale.X64.Leakage_Helpers.is_map_of Vale.X64.Leakage_s.__proj__LeakageTaints__item__regTaint Vale.X64.Leakage_Helpers.AnalysisTaints Vale.X64.Leakage_Helpers.regs_to_map Vale.X64.Leakage_Helpers.map_to_regs
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"
val normalize_taints (ts: analysis_taints) : analysis_taints
ts: Vale.X64.Leakage_Helpers.analysis_taints -> Vale.X64.Leakage_Helpers.analysis_taints