val reg_le (r1 r2: reg) : bool
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 reg_le (r1 r2: reg) : bool
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)
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.Machine_s.reg Vale.X64.Machine_s.reg_file_id Vale.X64.Machine_s.reg_id Prims.op_BarBar Prims.op_LessThan Prims.op_AmpAmp Prims.op_Equality Prims.op_LessThanOrEqual Prims.bool
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
val reg_le (r1 r2: reg) : bool
r1: Vale.X64.Machine_s.reg -> r2: Vale.X64.Machine_s.reg -> Prims.bool