structure DY.ProtocolEvent.ExecEntryT (EventT : Type) : Type

• ev : EventT

def DY.ProtocolEvent.baseAttackerKnowledge [BytesFunctor] [ExecTraceTypes] (EventT : Type) : SubBaseAttackerKnowledge (ExecEntryT EventT)

Equations

• DY.ProtocolEvent.baseAttackerKnowledge EventT = { attackerKnows := fun (x : DY.ExecTrace) (x_1 : DY.ProtocolEvent.ExecEntryT EventT) (x_2 : DY.Bytes) => False }

@[reducible, inline]

abbrev DY.ProtocolEvent.ProofEntryT (EventT : Type) : Type

Equations

• DY.ProtocolEvent.ProofEntryT EventT = DY.ProtocolEvent.ExecEntryT EventT

@[instance_reducible]

instance DY.ProtocolEvent.instErasableProofEntryExecEntryTProofEntryT (EventT : Type) : ErasableProofEntry (ExecEntryT EventT) (ProofEntryT EventT)

Equations

• DY.ProtocolEvent.instErasableProofEntryExecEntryTProofEntryT EventT = DY.ErasableProofEntry.default (DY.ProtocolEvent.ExecEntryT EventT)

@[instance_reducible]

instance DY.ProtocolEvent.instExecEntryAssociatedWithProofEntryExecEntryTProofEntryT (EventT : Type) : ExecEntryAssociatedWithProofEntry (ExecEntryT EventT) (ProofEntryT EventT)

Equations

• DY.ProtocolEvent.instExecEntryAssociatedWithProofEntryExecEntryTProofEntryT EventT = { }

class DY.ProtocolEvent.EventInv [ExecTraceTypes] [ProofTraceTypes] (EventT : Type) : Type

• invariant : ProofTrace → EventT → Prop

@[instance_reducible]

instance DY.ProtocolEvent.instSubTraceInvariantExecEntryTProofEntryTOfEventInv [ExecTraceTypes] [ProofTraceTypes] (EventT : Type) [EventInv EventT] : SubTraceInvariant (ProofEntryT EventT)

Equations

• One or more equations did not get rendered due to their size.

instance DY.ProtocolEvent.baseAttackerKnowledgeTheorem [ExecTraceTypes] [ProofTraceTypes] [TraceInvariant] [BytesFunctor] [BytesInvariants] (EventT : Type) [ExecTraceTypes.Has (ExecEntryT EventT)] [ProofTraceTypes.Has (ProofEntryT EventT)] [EventInv EventT] [TraceInvariant.Has (ProofEntryT EventT)] : SubBaseAttackerKnowledgeTheorem (ProofEntryT EventT) (baseAttackerKnowledge EventT)

def DY.Trace.EventLoggedAt {EventT : Type} [ExecTraceTypes] [ExecTraceTypes.Has (ProtocolEvent.ExecEntryT EventT)] (ev : EventT) (time : Nat) (tr : ExecTrace) : Prop

Equations

• DY.Trace.EventLoggedAt ev time tr = (DY.Trace.at? tr time = some { ev := ev })

theorem DY.Trace.EventLoggedAt_implies_i_le_length {EventT : Type} [ExecTraceTypes] [ExecTraceTypes.Has (ProtocolEvent.ExecEntryT EventT)] (ev : EventT) (i : Nat) (tr : ExecTrace) : EventLoggedAt ev i tr → i < length tr

def DY.Trace.getEventAt (EventT : Type) [ExecTraceTypes] [ExecTraceTypes.Has (ProtocolEvent.ExecEntryT EventT)] (i : Nat) (tr : ExecTrace) : Option EventT

Equations

• DY.Trace.getEventAt EventT i tr = match DY.Trace.at? tr i with | none => none | some entry => some entry.ev

theorem DY.Trace.EventLoggedAt_eq_getEventAt {EventT : Type} [ExecTraceTypes] [ExecTraceTypes.Has (ProtocolEvent.ExecEntryT EventT)] (ev : EventT) (i : Nat) (tr : ExecTrace) : EventLoggedAt ev i tr = (getEventAt EventT i tr = some ev)

theorem DY.Trace.EventLoggedAt_le {EventT : Type} [ExecTraceTypes] [ExecTraceTypes.Has (ProtocolEvent.ExecEntryT EventT)] (ev : EventT) (time : Nat) (tr1 tr2 : ExecTrace) : tr1 ≤ tr2 → EventLoggedAt ev time tr1 → EventLoggedAt ev time tr2

theorem DY.Trace.EventLoggedAt_le' {EventT : Type} [ExecTraceTypes] [ExecTraceTypes.Has (ProtocolEvent.ExecEntryT EventT)] (ev : EventT) (time : Nat) (tr1 tr2 : ExecTrace) : time < length tr1 → tr1 ≤ tr2 → EventLoggedAt ev time tr2 → EventLoggedAt ev time tr1

def DY.Trace.EventLogged {EventT : Type} [ExecTraceTypes] [ExecTraceTypes.Has (ProtocolEvent.ExecEntryT EventT)] (ev : EventT) (tr : ExecTrace) : Prop

Equations

• DY.Trace.EventLogged ev tr = ∃ (i : Nat), DY.Trace.EventLoggedAt ev i tr

theorem DY.Trace.EventLogged_le {EventT : Type} [ExecTraceTypes] [ExecTraceTypes.Has (ProtocolEvent.ExecEntryT EventT)] (ev : EventT) (tr1 tr2 : ExecTrace) : tr1 ≤ tr2 → EventLogged ev tr1 → EventLogged ev tr2

theorem DY.Trace.EventLoggedAt_imp_EventInv {EventT : Type} [ExecTraceTypes] [ProofTraceTypes] [TraceInvariant] [ProtocolEvent.EventInv EventT] [ExecTraceTypes.Has (ProtocolEvent.ExecEntryT EventT)] [ProofTraceTypes.Has (ProtocolEvent.ProofEntryT EventT)] [TraceInvariant.Has (ProtocolEvent.ProofEntryT EventT)] (ev : EventT) (i : Nat) (tr : ProofTrace) : Invariant tr → EventLoggedAt ev i (erase tr) → ProtocolEvent.EventInv.invariant («prefix» tr i) ev

theorem DY.Trace.EventLogged_imp_EventInv {EventT : Type} [ExecTraceTypes] [ProofTraceTypes] [TraceInvariant] [ProtocolEvent.EventInv EventT] [ExecTraceTypes.Has (ProtocolEvent.ExecEntryT EventT)] [ProofTraceTypes.Has (ProtocolEvent.ProofEntryT EventT)] [TraceInvariant.Has (ProtocolEvent.ProofEntryT EventT)] (ev : EventT) (tr : ProofTrace) : Invariant tr → EventLogged ev (erase tr) → ∃ (i : Nat), ProtocolEvent.EventInv.invariant («prefix» tr i) ev

def DY.ProtocolEvent.logEvent {EventT : Type} [ExecTraceTypes] [ExecTraceTypes.Has (ExecEntryT EventT)] (ev : EventT) : Traceful Unit

Equations

• DY.ProtocolEvent.logEvent ev = do let _ ← DY.appendEntry { ev := ev } pure ()

instance DY.ProtocolEvent.logEvent.proof {EventT : Type} [ExecTraceTypes] [ProofTraceTypes] [TraceInvariant] [EventInv EventT] [ExecTraceTypes.Has (ExecEntryT EventT)] [ProofTraceTypes.Has (ProofEntryT EventT)] [TraceInvariant.Has (ProofEntryT EventT)] (ev : EventT) : HoareTriple (logEvent ev) (fun (tr : ProofTrace) => EventInv.invariant tr ev) fun (x : Unit) (tr : ProofTrace) => Trace.EventLogged ev (Trace.erase tr)

def DY.ProtocolEvent.label {EventT : Type} [ExecTraceTypes] [ExecTraceTypes.Has (ExecEntryT EventT)] (ev : EventT) : Label

Equations

• DY.ProtocolEvent.label ev = { isCorrupt := fun (tr : DY.ExecTrace) => DY.Trace.EventLogged ev tr, isCorruptLater := ⋯ }

theorem DY.ProtocolEvent.label_isCorrupt {EventT : Type} [ExecTraceTypes] [ExecTraceTypes.Has (ExecEntryT EventT)] (ev : EventT) (tr : ExecTrace) : (label ev).isCorrupt tr = Trace.EventLogged ev tr