structure DY.Network.ExecEntryT [BytesFunctor] : Type

• msg : Bytes

def DY.Network.baseAttackerKnowledge [BytesFunctor] [ExecTraceTypes] : SubBaseAttackerKnowledge ExecEntryT

Equations

• DY.Network.baseAttackerKnowledge = { attackerKnows := fun (x : DY.ExecTrace) (entry : DY.Network.ExecEntryT) (msg : DY.Bytes) => msg = entry.msg }

def DY.Network.sendMessage [BytesFunctor] [ExecTraceTypes] [ExecTraceTypes.Has ExecEntryT] (msg : Bytes) : Traceful Nat

Equations

• DY.Network.sendMessage msg = DY.appendEntry { msg := msg }

def DY.Network.receiveMessage [BytesFunctor] [ExecTraceTypes] [ExecTraceTypes.Has ExecEntryT] (handle : Nat) : Traceful Bytes

Equations

• DY.Network.receiveMessage handle = do let msg ← DY.getEntry handle pure msg.msg

def DY.Trace.MessageSentAt [BytesFunctor] [ExecTraceTypes] [ExecTraceTypes.Has Network.ExecEntryT] (tr : ExecTrace) (b : Bytes) (i : Nat) : Prop

Equations

• DY.Trace.MessageSentAt tr b i = (DY.Trace.at? tr i = some { msg := b })

def DY.Trace.MessageSent [BytesFunctor] [ExecTraceTypes] [ExecTraceTypes.Has Network.ExecEntryT] (tr : ExecTrace) (b : Bytes) : Prop

Equations

• DY.Trace.MessageSent tr b = ∃ (i : Nat), DY.Trace.MessageSentAt tr b i

def DY.Trace.getMessageSentAt [BytesFunctor] [ExecTraceTypes] [ExecTraceTypes.Has Network.ExecEntryT] (i : Nat) (tr : ExecTrace) : Option Bytes

Equations

• DY.Trace.getMessageSentAt i tr = match DY.Trace.at? tr i with | none => none | some entry => some entry.msg

theorem DY.Trace.MessageSentAt_eq_getMessageSentAt [BytesFunctor] [ExecTraceTypes] [ExecTraceTypes.Has Network.ExecEntryT] (msg : Bytes) (i : Nat) (tr : ExecTrace) : MessageSentAt tr msg i = (getMessageSentAt i tr = some msg)

theorem DY.Trace.MessageSentAt_implies_AttackerKnows [BytesFunctor] [ExecTraceTypes] [ExecTraceTypes.Has Network.ExecEntryT] [BaseAttackerKnowledge] [AttackerKnowledge] [BaseAttackerKnowledge.Has Network.baseAttackerKnowledge] (tr : ExecTrace) (b : Bytes) (i : Nat) : MessageSentAt tr b i → b.AttackerKnows tr

@[reducible, inline]

abbrev DY.Network.ProofEntryT [BytesFunctor] : Type

Equations

• DY.Network.ProofEntryT = DY.Network.ExecEntryT

@[instance_reducible]

instance DY.Network.instErasableProofEntryExecEntryTProofEntryT [BytesFunctor] : ErasableProofEntry ExecEntryT ProofEntryT

Equations

• DY.Network.instErasableProofEntryExecEntryTProofEntryT = DY.ErasableProofEntry.default DY.Network.ExecEntryT

@[instance_reducible]

instance DY.Network.instExecEntryAssociatedWithProofEntryExecEntryTProofEntryT [BytesFunctor] : ExecEntryAssociatedWithProofEntry ExecEntryT ProofEntryT

Equations

• DY.Network.instExecEntryAssociatedWithProofEntryExecEntryTProofEntryT = { }

@[instance_reducible]

instance DY.Network.instSubTraceInvariantExecEntryTProofEntryTOfBytesInvariants [BytesFunctor] [ExecTraceTypes] [ProofTraceTypes] [BytesInvariants] : SubTraceInvariant ProofEntryT

Equations

• DY.Network.instSubTraceInvariantExecEntryTProofEntryTOfBytesInvariants = { invariant := fun (tr : DY.ProofTrace) (entry : DY.Network.ProofEntryT) => entry.msg.Publishable tr }

instance DY.Network.baseAttackerKnowledgeTheorem [BytesFunctor] [ExecTraceTypes] [ProofTraceTypes] [TraceInvariant] [BytesInvariants] [ExecTraceTypes.Has ExecEntryT] [ProofTraceTypes.Has ProofEntryT] [TraceInvariant.Has ProofEntryT] : SubBaseAttackerKnowledgeTheorem ProofEntryT baseAttackerKnowledge

instance DY.Network.sendMessage.spec [BytesFunctor] [ExecTraceTypes] [ProofTraceTypes] [TraceInvariant] [BytesInvariants] [BytesInvariantsProofs] [ExecTraceTypes.Has ExecEntryT] [ProofTraceTypes.Has ProofEntryT] [TraceInvariant.Has ProofEntryT] (msg : Bytes) : HoareTriple (sendMessage msg) (fun (tr : ProofTrace) => msg.Publishable tr) fun (x : Nat) (x_1 : ProofTrace) => True

instance DY.Network.receiveMessage.spec [BytesFunctor] [ExecTraceTypes] [ProofTraceTypes] [TraceInvariant] [BytesInvariants] [BytesInvariantsProofs] [ExecTraceTypes.Has ExecEntryT] [ProofTraceTypes.Has ProofEntryT] [TraceInvariant.Has ProofEntryT] (handle : Nat) : HoareTriple (receiveMessage handle) (fun (x : ProofTrace) => True) fun (msg : Bytes) (tr : ProofTrace) => msg.Publishable tr

@[reducible, inline]

abbrev DY.Network.reachability [BytesFunctor] [ExecTraceTypes] [ExecTraceTypes.Has ExecEntryT] [BaseAttackerKnowledge] [AttackerKnowledge] : ReachabilityConfig

Equations

• DY.Network.reachability = { Input := DY.Bytes, PreCond := fun (b : DY.Bytes) (tr : DY.ExecTrace) => b.AttackerKnows tr, step := fun (b : DY.Bytes) => ⟨Nat, DY.Network.sendMessage b⟩ }

theorem DY.Network.receiveMessage.preservesReachability [BytesFunctor] [ExecTraceTypes] [ExecTraceTypes.Has ExecEntryT] [BaseAttackerKnowledge] [AttackerKnowledge] [BaseAttackerKnowledge.Has baseAttackerKnowledge] (config : ReachabilityConfig) (msgHandle : Nat) : Traceful.PreservesReachability config (receiveMessage msgHandle) (fun (x : ExecTrace) => True) fun (msg : Bytes) (tr : ExecTrace) => msg.AttackerKnows tr

instance DY.Network.instReachableImpliesInvariantReachability [BytesFunctor] [ExecTraceTypes] [ExecTraceTypes.Has ExecEntryT] [BaseAttackerKnowledge] [AttackerKnowledge] [ProofTraceTypes] [TraceInvariant] [BytesInvariants] [BytesInvariantsProofs] [ProofTraceTypes.Has ProofEntryT] [TraceInvariant.Has ProofEntryT] [BaseAttackerKnowledgeTheorem] [AttackerKnowledgeTheorem] : ReachableImpliesInvariant reachability