val map_to_regs (m: regmap) : reg_taint
let map_to_regs (m:regmap) : reg_taint =
  FunctionalExtensionality.on reg (sel m)
val map_to_regs (m: regmap) : reg_taint
let map_to_regs (m: regmap) : reg_taint =
FunctionalExtensionality.on reg (sel m)
Vale.X64.Leakage_Helpers.fst.checked
Vale.X64.Machine_Semantics_s.fst.checked Vale.X64.Machine_s.fst.checked Vale.X64.Leakage_s.fst.checked Vale.X64.Instruction_s.fsti.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
Vale.X64.Leakage_Helpers.fst
Vale.X64.Leakage_Helpers.regmap FStar.FunctionalExtensionality.on Vale.X64.Machine_s.reg Vale.Arch.HeapTypes_s.taint Vale.Lib.MapTree.sel Vale.X64.Leakage_s.reg_taint
module Vale.X64.Leakage_Helpers
open FStar.Mul
open Vale.X64.Machine_Semantics_s
open Vale.X64.Machine_s
open Vale.X64.Leakage_s
open Vale.X64.Instruction_s
open Vale.Lib.MapTree

let regmap = map reg taint

let reg_le (r1 r2:reg) : bool =
  let Reg f1 n1 = r1 in
  let Reg f2 n2 = r2 in
  f1 < f2 || (f1 = f2 && n1 <= n2)
val map_to_regs (m: regmap) : reg_taint
m: Vale.X64.Leakage_Helpers.regmap -> Vale.X64.Leakage_s.reg_taint