let publicFlagValuesAreSame (ts:leakage_taints) (s1:machine_state) (s2:machine_state) =
  ts.flagsTaint = Public ==> (s1.ms_flags == s2.ms_flags)
let publicFlagValuesAreSame (ts: leakage_taints) (s1 s2: machine_state) =
ts.flagsTaint = Public ==> (s1.ms_flags == s2.ms_flags)
Vale.X64.Leakage_s.fst.checked
Vale.X64.Machine_Semantics_s.fst.checked Vale.X64.Machine_s.fst.checked Vale.Arch.HeapTypes_s.fst.checked Vale.Arch.Heap.fsti.checked prims.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.Map.fsti.checked FStar.FunctionalExtensionality.fsti.checked
Vale.X64.Leakage_s.fst
Vale.X64.Leakage_s.leakage_taints Vale.X64.Machine_Semantics_s.machine_state Prims.l_imp Prims.b2t Prims.op_Equality Vale.Arch.HeapTypes_s.taint Vale.X64.Leakage_s.__proj__LeakageTaints__item__flagsTaint Vale.Arch.HeapTypes_s.Public Prims.eq2 Vale.X64.Machine_Semantics_s.flags_t Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_flags Prims.logical
module Vale.X64.Leakage_s

open FStar.Mul
open Vale.Arch.HeapTypes_s
open Vale.Arch.Heap
open Vale.X64.Machine_s
open Vale.X64.Machine_Semantics_s
module F = FStar.FunctionalExtensionality

type reg_taint = F.restricted_t reg (fun _ -> taint)

noeq type leakage_taints =
  | LeakageTaints: regTaint: reg_taint -> flagsTaint: taint -> cfFlagsTaint: taint -> ofFlagsTaint: taint ->
      leakage_taints
val publicFlagValuesAreSame : ts: Vale.X64.Leakage_s.leakage_taints ->
    s1: Vale.X64.Machine_Semantics_s.machine_state ->
    s2: Vale.X64.Machine_Semantics_s.machine_state
  -> Prims.logical

    ts: Vale.X64.Leakage_s.leakage_taints ->
    s1: Vale.X64.Machine_Semantics_s.machine_state ->
    s2: Vale.X64.Machine_Semantics_s.machine_state
  -> Prims.logical