structure DY.SubBaseAttackerKnowledge [BytesFunctor] [ExecTraceTypes] (ExecEntryT : Type) : Type

• attackerKnows : ExecTrace → ExecEntryT → Bytes → Prop

class DY.BaseAttackerKnowledge [BytesFunctor] [ExecTraceTypes] : Type

• attackerKnows : SubBaseAttackerKnowledge ExecTrace.Entry

class DY.BaseAttackerKnowledge.Has [BytesFunctor] [ExecTraceTypes] [BaseAttackerKnowledge] {ExecEntryT : Type} [ExecTraceTypes.Has ExecEntryT] (sub : SubBaseAttackerKnowledge ExecEntryT) : Prop

• pf (tr : ExecTrace) (entry : ExecEntryT) (b : Bytes) : sub.attackerKnows tr entry b → attackerKnows.attackerKnows tr (TraceEntryHas.inj entry) b

class DY.BaseAttackerKnowledge.HasStep [BytesFunctor] [ExecTraceTypes] {ExecEntryT1 : Type} {ExecEntryT2 : semiOutParam Type} [ExecTraceTypes.HasStep ExecEntryT1 ExecEntryT2] (sub1 : SubBaseAttackerKnowledge ExecEntryT1) (sub2 : semiOutParam (SubBaseAttackerKnowledge ExecEntryT2)) : Prop

• pf (tr : ExecTrace) (entry : ExecEntryT1) (b : Bytes) : sub1.attackerKnows tr entry b → sub2.attackerKnows tr (ExecTraceTypes.HasStep.inj entry) b

instance DY.instBaseAttackerKnowledgeHasItself [BytesFunctor] [ExecTraceTypes] [BaseAttackerKnowledge] : BaseAttackerKnowledge.Has BaseAttackerKnowledge.attackerKnows

instance DY.instBaseAttackerKnowledgeHasStep [BytesFunctor] [ExecTraceTypes] [BaseAttackerKnowledge] {ExecEntryT1 ExecEntryT2 : Type} [ExecTraceTypes.HasStep ExecEntryT1 ExecEntryT2] [ExecTraceTypes.Has ExecEntryT2] (sub1 : SubBaseAttackerKnowledge ExecEntryT1) (sub2 : SubBaseAttackerKnowledge ExecEntryT2) [BaseAttackerKnowledge.HasStep sub1 sub2] [BaseAttackerKnowledge.Has sub2] : BaseAttackerKnowledge.Has sub1

def DY.SubBaseAttackerKnowledge.combine [BytesFunctor] [ExecTraceTypes] {n : Nat} {Types : Fin n → Type} (subs : (id : Fin n) → SubBaseAttackerKnowledge (Types id)) : SubBaseAttackerKnowledge (ExecTraceTypes.combine Types)

Equations

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

instance DY.instBaseAttackerKnowledgeCombineHasStep [BytesFunctor] [ExecTraceTypes] {n : Nat} {Types : Fin n → Type} (subs : (id : Fin n) → SubBaseAttackerKnowledge (Types id)) (id : Fin n) : BaseAttackerKnowledge.HasStep (subs id) (SubBaseAttackerKnowledge.combine subs)

def DY.Trace.BaseAttackerKnows [BytesFunctor] [ExecTraceTypes] [BaseAttackerKnowledge] (tr : ExecTrace) (b : Bytes) : Prop

Equations

• DY.Trace.nil.BaseAttackerKnows b = False
• (trBefore.snoc entry).BaseAttackerKnows b = (DY.BaseAttackerKnowledge.attackerKnows.attackerKnows trBefore entry b ∨ trBefore.BaseAttackerKnows b)

theorem DY.Trace.BaseAttackerKnows_le [BytesFunctor] [ExecTraceTypes] [BaseAttackerKnowledge] (b : Bytes) (tr1 tr2 : ExecTrace) : tr1 ≤ tr2 → BaseAttackerKnows tr1 b → BaseAttackerKnows tr2 b

theorem DY.Trace.prove_BaseAttackerKnows [BytesFunctor] [ExecTraceTypes] [BaseAttackerKnowledge] {ExecEntryT : Type} [ExecTraceTypes.Has ExecEntryT] (sub : SubBaseAttackerKnowledge ExecEntryT) [BaseAttackerKnowledge.Has sub] (tr : ExecTrace) (entry : ExecEntryT) (b : Bytes) (time : Nat) : at? tr time = some entry → sub.attackerKnows («prefix» tr time) entry b → BaseAttackerKnows tr b