def DY.Label.pub [ExecTraceTypes] : Label

Equations

• DY.Label.pub = { isCorrupt := fun (tr : DY.ExecTrace) => True, isCorruptLater := ⋯ }

@[simp]

theorem DY.Label.pubIsCorrupt [ExecTraceTypes] (tr : ExecTrace) : pub.isCorrupt tr

theorem DY.canFlowPubEqIsCorrupt [ExecTraceTypes] (l : Label) (tr : ExecTrace) : l.isCorrupt tr = l.canFlow Label.pub tr

theorem DY.Label.pubCanFlow [ExecTraceTypes] (l : Label) (tr : ExecTrace) : pub.canFlow l tr

def DY.Label.secret [ExecTraceTypes] : Label

Equations

• DY.Label.secret = { isCorrupt := fun (tr : DY.ExecTrace) => False, isCorruptLater := ⋯ }

@[simp]

theorem DY.Label.secretIsCorrupt [ExecTraceTypes] (tr : ExecTrace) : ¬secret.isCorrupt tr

theorem DY.Label.secret.canFlow [ExecTraceTypes] (l : Label) (tr : ExecTrace) : l.canFlow secret tr

def DY.Label.join [ExecTraceTypes] (l1 l2 : Label) : Label

Equations

• l1.join l2 = { isCorrupt := fun (tr : DY.ExecTrace) => l1.isCorrupt tr ∨ l2.isCorrupt tr, isCorruptLater := ⋯ }

@[simp]

theorem DY.Label.joinIsCorrupt [ExecTraceTypes] (l1 l2 : Label) (tr : ExecTrace) : (l1.join l2).isCorrupt tr = (l1.isCorrupt tr ∨ l2.isCorrupt tr)

def DY.Label.meet [ExecTraceTypes] (l1 l2 : Label) : Label

Equations

• l1.meet l2 = { isCorrupt := fun (tr : DY.ExecTrace) => l1.isCorrupt tr ∧ l2.isCorrupt tr, isCorruptLater := ⋯ }

@[simp]

theorem DY.Label.meetIsCorrupt [ExecTraceTypes] (l1 l2 : Label) (tr : ExecTrace) : (l1.meet l2).isCorrupt tr = (l1.isCorrupt tr ∧ l2.isCorrupt tr)

theorem DY.Label.meetEq [ExecTraceTypes] (l1 l2 l3 : Label) (tr : ExecTrace) : (l1.meet l2).canFlow l3 tr = (l1.canFlow l3 tr ∧ l2.canFlow l3 tr)

theorem DY.Label.joinEq [ExecTraceTypes] (l1 l2 l3 : Label) (tr : ExecTrace) : l1.canFlow (l2.join l3) tr = (l1.canFlow l2 tr ∧ l1.canFlow l3 tr)

theorem DY.Label.joinCanFlowLeft [ExecTraceTypes] (l1 l2 : Label) (tr : ExecTrace) : (l1.join l2).canFlow l1 tr

theorem DY.Label.joinCanFlowRight [ExecTraceTypes] (l1 l2 : Label) (tr : ExecTrace) : (l1.join l2).canFlow l2 tr

theorem DY.Label.join_pub_left [ExecTraceTypes] (l : Label) : pub.join l = pub

theorem DY.Label.join_pub_right [ExecTraceTypes] (l : Label) : l.join pub = pub

theorem DY.Label.join_commutes [ExecTraceTypes] (l1 l2 : Label) : l1.join l2 = l2.join l1