val lemma_eq_regs_file (regs1 regs2: reg_taint) (rf: reg_file_id) (k: nat{k <= n_regs rf})
    : Lemma
    (ensures
      eq_regs_file regs1 regs2 rf k <==>
      (forall (i: nat). {:pattern (Reg rf i)} i < k ==> regs1 (Reg rf i) == regs2 (Reg rf i)))
let rec lemma_eq_regs_file (regs1 regs2:reg_taint) (rf:reg_file_id) (k:nat{k <= n_regs rf}) : Lemma
  (ensures eq_regs_file regs1 regs2 rf k <==>
    (forall (i:nat).{:pattern (Reg rf i)} i < k ==> regs1 (Reg rf i) == regs2 (Reg rf i)))
  =
  if k > 0 then lemma_eq_regs_file regs1 regs2 rf (k - 1)
val lemma_eq_regs_file (regs1 regs2: reg_taint) (rf: reg_file_id) (k: nat{k <= n_regs rf})
    : Lemma
    (ensures
      eq_regs_file regs1 regs2 rf k <==>
      (forall (i: nat). {:pattern (Reg rf i)} i < k ==> regs1 (Reg rf i) == regs2 (Reg rf i)))
let rec lemma_eq_regs_file (regs1 regs2: reg_taint) (rf: reg_file_id) (k: nat{k <= n_regs rf})
    : Lemma
    (ensures
      eq_regs_file regs1 regs2 rf k <==>
      (forall (i: nat). {:pattern (Reg rf i)} i < k ==> regs1 (Reg rf i) == regs2 (Reg rf i))) =
if k > 0 then lemma_eq_regs_file regs1 regs2 rf (k - 1)
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 Vale.X64.Machine_s.reg_file_id Prims.nat Prims.b2t Prims.op_LessThanOrEqual Vale.X64.Machine_s.n_regs Prims.op_GreaterThan Vale.X64.Leakage.lemma_eq_regs_file Prims.op_Subtraction Prims.bool Prims.unit Prims.l_True Prims.squash Prims.l_iff Vale.X64.Leakage.eq_regs_file Prims.l_Forall Prims.l_imp Prims.op_LessThan Prims.eq2 Vale.Arch.HeapTypes_s.taint Vale.X64.Machine_s.Reg Prims.Nil FStar.Pervasives.pattern
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))

let combine_reg_taints (regs1 regs2:reg_taint) : reg_taint =
  FunctionalExtensionality.on reg (fun x -> merge_taint (regs1 x) (regs2 x))

let rec eq_regs_file (regs1 regs2:reg_taint) (rf:reg_file_id) (k:nat{k <= n_regs rf}) : bool =
  if k = 0 then true
  else regs1 (Reg rf (k - 1)) = regs2 (Reg rf (k - 1)) && eq_regs_file regs1 regs2 rf (k - 1)

let rec eq_regs (regs1 regs2:reg_taint) (k:nat{k <= n_reg_files}) : bool =
  if k = 0 then true
  else eq_regs_file regs1 regs2 (k - 1) (n_regs (k - 1)) && eq_regs regs1 regs2 (k - 1)

let rec lemma_eq_regs_file (regs1 regs2:reg_taint) (rf:reg_file_id) (k:nat{k <= n_regs rf}) : Lemma
  (ensures eq_regs_file regs1 regs2 rf k <==>
    (forall (i:nat).{:pattern (Reg rf i)} i < k ==> regs1 (Reg rf i) == regs2 (Reg rf i)))
val lemma_eq_regs_file (regs1 regs2: reg_taint) (rf: reg_file_id) (k: nat{k <= n_regs rf})
    : Lemma
    (ensures
      eq_regs_file regs1 regs2 rf k <==>
      (forall (i: nat). {:pattern (Reg rf i)} i < k ==> regs1 (Reg rf i) == regs2 (Reg rf i)))

    regs1: Vale.X64.Leakage_s.reg_taint ->
    regs2: Vale.X64.Leakage_s.reg_taint ->
    rf: Vale.X64.Machine_s.reg_file_id ->
    k: Prims.nat{k <= Vale.X64.Machine_s.n_regs rf}
  -> FStar.Pervasives.Lemma
    (ensures
      Vale.X64.Leakage.eq_regs_file regs1 regs2 rf k <==>
      (forall (i: Prims.nat). {:pattern Vale.X64.Machine_s.Reg rf i}
          i < k ==> regs1 (Vale.X64.Machine_s.Reg rf i) == regs2 (Vale.X64.Machine_s.Reg rf i)))