class DY.SubBaseAttackerKnowledgeTheorem [ExecTraceTypes] [ProofTraceTypes] [TraceInvariant] [BytesFunctor] [BytesInvariants] {ExecEntryT : Type} (ProofEntryT : Type) [ErasableProofEntry ExecEntryT ProofEntryT] [SubTraceInvariant ProofEntryT] [ExecTraceTypes.Has ExecEntryT] [ProofTraceTypes.Has ProofEntryT] [TraceInvariant.Has ProofEntryT] (att : SubBaseAttackerKnowledge ExecEntryT) : Prop

• pf (trBefore : ProofTrace) (entry : ProofEntryT) (b : Bytes) : SubTraceInvariant.invariant trBefore entry → att.attackerKnows (Trace.erase trBefore) (ErasableProofEntry.erase entry) b → b.Publishable trBefore

class DY.BaseAttackerKnowledgeTheorem [ExecTraceTypes] [ProofTraceTypes] [TraceInvariant] [BytesFunctor] [BytesInvariants] [BaseAttackerKnowledge] : Prop

• pf : SubBaseAttackerKnowledgeTheorem ProofTrace.Entry BaseAttackerKnowledge.attackerKnows

instance DY.instSubBaseAttackerKnowledgeTheoremCombine [ExecTraceTypes] [ProofTraceTypes] [TraceInvariant] [BytesFunctor] [BytesInvariants] {n : Nat} {ExecTypes ProofTypes : Fin n → Type} [(id : Fin n) → ErasableProofEntry (ExecTypes id) (ProofTypes id)] [(id : Fin n) → SubTraceInvariant (ProofTypes id)] [ExecTraceTypes.Has (ExecTraceTypes.combine ExecTypes)] [ProofTraceTypes.Has (ProofTraceTypes.combine ProofTypes)] [TraceInvariant.Has (ProofTraceTypes.combine ProofTypes)] (atts : (id : Fin n) → SubBaseAttackerKnowledge (ExecTypes id)) [attThms : ∀ (id : Fin n), SubBaseAttackerKnowledgeTheorem (ProofTypes id) (atts id)] : SubBaseAttackerKnowledgeTheorem (ProofTraceTypes.combine ProofTypes) (SubBaseAttackerKnowledge.combine atts)

theorem DY.Trace.BaseAttackerKnows_implies_Publishable [ExecTraceTypes] [ProofTraceTypes] [TraceInvariant] [BytesFunctor] [BytesInvariants] [BytesInvariantsProofs] [BaseAttackerKnowledge] [BaseAttackerKnowledgeTheorem] (tr : ProofTrace) (b : Bytes) : Invariant tr → BaseAttackerKnows (erase tr) b → b.Publishable tr