val operand_taint (rf: reg_file_id) (o: operand_rf rf) (ts: analysis_taints) : taint
let operand_taint (rf:reg_file_id) (o:operand_rf rf) (ts:analysis_taints) : taint =
  match o with
  | OConst _ -> Public
  | OReg r -> sel ts.rts (Reg rf r)
  | OMem (_, t) | OStack (_, t) -> t
val operand_taint (rf: reg_file_id) (o: operand_rf rf) (ts: analysis_taints) : taint
let operand_taint (rf: reg_file_id) (o: operand_rf rf) (ts: analysis_taints) : taint =
match o with
| OConst _ -> Public
| OReg r -> sel ts.rts (Reg rf r)
| OMem (_, t) | OStack (_, t) -> t
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_file_id Vale.X64.Machine_s.operand_rf Vale.X64.Leakage_Helpers.analysis_taints Vale.X64.Machine_s.t_reg_file Vale.Arch.HeapTypes_s.Public Vale.X64.Machine_s.reg_id Vale.Lib.MapTree.sel Vale.X64.Machine_s.reg Vale.Arch.HeapTypes_s.taint Vale.X64.Leakage_Helpers.__proj__AnalysisTaints__item__rts Vale.X64.Machine_s.Reg Vale.X64.Machine_s.maddr
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)

let map_to_regs (m:regmap) : reg_taint =
  FunctionalExtensionality.on reg (sel m)

let is_map_of (m:regmap) (rs:reg_taint) =
  FStar.FunctionalExtensionality.feq (map_to_regs m) rs

let rec regs_to_map_rec (rs:reg_taint) (f n:nat) : Pure regmap
  (requires (f == n_reg_files /\ n == 0) \/ (f < n_reg_files /\ n <= n_regs f))
  (ensures (fun m -> forall (r:reg).{:pattern sel m r}
    r.rf < f \/ (r.rf == f /\ r.r < n) ==> sel m r == rs r))
  (decreases %[f; n])
  =
  if n = 0 then
    if f = 0 then const reg taint reg_le Secret
    else regs_to_map_rec rs (f - 1) (n_regs (f - 1))
  else
    let m = regs_to_map_rec rs f (n - 1) in
    let r = Reg f (n - 1) in
    upd m r (rs r)

let regs_to_map (rs:reg_taint) : (m:regmap{is_map_of m rs}) =
  regs_to_map_rec rs n_reg_files 0

noeq type analysis_taints =
  | AnalysisTaints: lts:leakage_taints -> rts:regmap{is_map_of rts lts.regTaint} -> analysis_taints

let merge_taint (t1:taint) (t2:taint) :taint =
  if Secret? t1 || Secret? t2 then Secret
  else Public

// Also pass the taint of the instruction
val operand_taint (rf: reg_file_id) (o: operand_rf rf) (ts: analysis_taints) : taint

    rf: Vale.X64.Machine_s.reg_file_id ->
    o: Vale.X64.Machine_s.operand_rf rf ->
    ts: Vale.X64.Leakage_Helpers.analysis_taints
  -> Vale.Arch.HeapTypes_s.taint