val combine_reg_taints (regs1 regs2: reg_taint) : reg_taint
let combine_reg_taints (regs1 regs2:reg_taint) : reg_taint =
  FunctionalExtensionality.on reg (fun x -> merge_taint (regs1 x) (regs2 x))
val combine_reg_taints (regs1 regs2: reg_taint) : reg_taint
let combine_reg_taints (regs1 regs2: reg_taint) : reg_taint =
FunctionalExtensionality.on reg (fun x -> merge_taint (regs1 x) (regs2 x))
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.reg_taint FStar.FunctionalExtensionality.on Vale.X64.Machine_s.reg Vale.Arch.HeapTypes_s.taint Vale.X64.Leakage_Helpers.merge_taint
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))
val combine_reg_taints (regs1 regs2: reg_taint) : reg_taint
regs1: Vale.X64.Leakage_s.reg_taint -> regs2: Vale.X64.Leakage_s.reg_taint
  -> Vale.X64.Leakage_s.reg_taint