let publicMemValuesAreSame (s1:machine_state) (s2:machine_state) =
  forall x.{:pattern (heap_taint s1.ms_heap).[x] \/ (heap_taint s2.ms_heap).[x] \/ (heap_get s1.ms_heap).[x] \/ (heap_get s2.ms_heap).[x]}
    publicMemValueIsSame (heap_get s1.ms_heap) (heap_get s2.ms_heap) (heap_taint s1.ms_heap) (heap_taint s2.ms_heap) x
let publicMemValuesAreSame (s1 s2: machine_state) =
forall x.
  {:pattern

    (heap_taint s1.ms_heap).[ x ]\/(heap_taint s2.ms_heap).[ x ]\/(heap_get s1.ms_heap).[ x ]\/(heap_get
        s2.ms_heap).[ x ]}
  publicMemValueIsSame (heap_get s1.ms_heap)
    (heap_get s2.ms_heap)
    (heap_taint s1.ms_heap)
    (heap_taint s2.ms_heap)
    x
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.Machine_Semantics_s.machine_state Prims.l_Forall Prims.int Vale.X64.Leakage_s.publicMemValueIsSame Vale.Arch.Heap.heap_get Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_heap Vale.Arch.Heap.heap_taint Vale.X64.Machine_Semantics_s.op_String_Access Vale.Def.Types_s.nat8 Vale.Arch.HeapTypes_s.taint 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

let publicFlagValuesAreSame (ts:leakage_taints) (s1:machine_state) (s2:machine_state) =
  ts.flagsTaint = Public ==> (s1.ms_flags == s2.ms_flags)

let publicCfFlagValuesAreSame (ts:leakage_taints) (s1:machine_state) (s2:machine_state) =
  Public? ts.cfFlagsTaint ==> (cf s1.ms_flags = cf s2.ms_flags)

let publicOfFlagValuesAreSame (ts:leakage_taints) (s1:machine_state) (s2:machine_state) =
  Public? ts.ofFlagsTaint ==> (overflow s1.ms_flags = overflow s2.ms_flags)

let publicRegisterValuesAreSame (ts:leakage_taints) (s1:machine_state) (s2:machine_state) =
  forall r.{:pattern ts.regTaint r \/ s1.ms_regs r \/ s2.ms_regs r}
    ts.regTaint r = Public ==>
    (s1.ms_regs r = s2.ms_regs r)

let publicMemValueIsSame
  (mem1 mem2:machine_heap)
  (memTaint1 memTaint2:Map.t int taint)
  (x:int) =
  (Public? (memTaint1.[x]) || Public? (memTaint2.[x])) ==>
     mem1.[x] == mem2.[x]
val publicMemValuesAreSame : s1: Vale.X64.Machine_Semantics_s.machine_state -> s2: Vale.X64.Machine_Semantics_s.machine_state
  -> Prims.logical
s1: Vale.X64.Machine_Semantics_s.machine_state -> s2: Vale.X64.Machine_Semantics_s.machine_state
  -> Prims.logical