let regmap = map reg taint
let regmap =
map reg taint
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.Lib.MapTree.map Vale.X64.Machine_s.reg Vale.Arch.HeapTypes_s.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
val regmap : Type0
Type0