let publicStackValuesAreSame (s1:machine_state) (s2:machine_state) =
  let Machine_stack _ stack1 = s1.ms_stack in
  let Machine_stack _ stack2 = s2.ms_stack in
  forall x.{:pattern s1.ms_stackTaint.[x] \/ s2.ms_stackTaint.[x] \/ stack1.[x] \/ stack2.[x]}
    publicStackValueIsSame stack1 stack2 s1.ms_stackTaint s2.ms_stackTaint x
let publicStackValuesAreSame (s1 s2: machine_state) =
let Machine_stack _ stack1 = s1.ms_stack in
let Machine_stack _ stack2 = s2.ms_stack in
forall x. {:pattern s1.ms_stackTaint.[ x ]\/s2.ms_stackTaint.[ x ]\/stack1.[ x ]\/stack2.[ x ]}
  publicStackValueIsSame stack1 stack2 s1.ms_stackTaint s2.ms_stackTaint 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 Vale.Def.Types_s.nat64 Prims.b2t Prims.op_GreaterThanOrEqual FStar.Map.t Prims.int Vale.Def.Types_s.nat8 Prims.l_Forall Vale.X64.Leakage_s.publicStackValueIsSame Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_stackTaint Vale.X64.Machine_Semantics_s.op_String_Access Vale.Arch.HeapTypes_s.taint Prims.logical Vale.X64.Machine_Semantics_s.machine_stack Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_stack
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]

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 publicStackValueIsSame
  (stack1 stack2:machine_heap)
  (stackTaint1 stackTaint2:Map.t int taint)
  (x:int)
  = (Public? (stackTaint1.[x]) || Public? (stackTaint2.[x])) ==>
     stack1.[x] == stack2.[x]
val publicStackValuesAreSame : 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