def DY.Example.SignedDH.attackerKnowledge.internal (id✝ : Fin 6) : SubAttackerKnowledge (SubF.internal id✝)

Equations

• DY.Example.SignedDH.attackerKnowledge.internal 0 = DY.Random.attackerKnowledge
• DY.Example.SignedDH.attackerKnowledge.internal 1 = DY.Literal.attackerKnowledge
• DY.Example.SignedDH.attackerKnowledge.internal 2 = DY.Concat.attackerKnowledge
• DY.Example.SignedDH.attackerKnowledge.internal 3 = DY.Hash.attackerKnowledge
• DY.Example.SignedDH.attackerKnowledge.internal 4 = DY.Signature.attackerKnowledge
• DY.Example.SignedDH.attackerKnowledge.internal 5 = DY.DiffieHellman.attackerKnowledge
• DY.Example.SignedDH.attackerKnowledge.internal ⟨n.succ.succ.succ.succ.succ.succ, isLt⟩ = ⋯.elim

@[instance_reducible]

def DY.Example.SignedDH.attackerKnowledge : SubAttackerKnowledge SubF

Equations

• DY.Example.SignedDH.attackerKnowledge = DY.SubAttackerKnowledge.combine DY.Example.SignedDH.attackerKnowledge.internal

@[instance_reducible]

def DY.Example.SignedDH.SubF : Type → Type

Equations

• DY.Example.SignedDH.SubF = DY.BytesFunctor.combine DY.Example.SignedDH.SubF.internal

@[instance_reducible]

instance DY.Example.SignedDH.instBytesFunctor_examples : BytesFunctor

Equations

• DY.Example.SignedDH.instBytesFunctor_examples = { BytesF := DY.Example.SignedDH.SubF, inst := DY.Example.SignedDH.wfInst✝ }

def DY.Example.SignedDH.SubF.length.internal (id✝ : Fin 6) : Bytes.PartialLength (SubF.internal id✝)

Equations

• DY.Example.SignedDH.SubF.length.internal 0 = DY.Random.SubF.length
• DY.Example.SignedDH.SubF.length.internal 1 = DY.Literal.SubF.length
• DY.Example.SignedDH.SubF.length.internal 2 = DY.Concat.SubF.length
• DY.Example.SignedDH.SubF.length.internal 3 = DY.Hash.SubF.length
• DY.Example.SignedDH.SubF.length.internal 4 = DY.Signature.SubF.length
• DY.Example.SignedDH.SubF.length.internal 5 = DY.DiffieHellman.SubF.length
• DY.Example.SignedDH.SubF.length.internal ⟨n.succ.succ.succ.succ.succ.succ, isLt⟩ = ⋯.elim

@[instance_reducible]

instance DY.Example.SignedDH.instBytesLength_examples : BytesLength

Equations

• DY.Example.SignedDH.instBytesLength_examples = { funs := DY.Example.SignedDH.SubF.length }

def DY.Example.SignedDH.SubF.internal : Fin 6 → Type → Type

Equations

• DY.Example.SignedDH.SubF.internal 0 = DY.Random.SubF
• DY.Example.SignedDH.SubF.internal 1 = DY.Literal.SubF
• DY.Example.SignedDH.SubF.internal 2 = DY.Concat.SubF
• DY.Example.SignedDH.SubF.internal 3 = DY.Hash.SubF
• DY.Example.SignedDH.SubF.internal 4 = DY.Signature.SubF
• DY.Example.SignedDH.SubF.internal 5 = DY.DiffieHellman.SubF
• DY.Example.SignedDH.SubF.internal ⟨n.succ.succ.succ.succ.succ.succ, isLt⟩ = ⋯.elim

@[instance_reducible]

def DY.Example.SignedDH.SubF.length : Bytes.PartialLength SubF

Equations

• DY.Example.SignedDH.SubF.length = DY.Bytes.PartialLength.combine DY.Example.SignedDH.SubF.length.internal

@[instance_reducible]

instance DY.Example.SignedDH.instAttackerKnowledge_examples : AttackerKnowledge

Equations

• DY.Example.SignedDH.instAttackerKnowledge_examples = { attackerKnowledge := DY.Example.SignedDH.attackerKnowledge }

instance DY.Example.SignedDH.instHasSubFAttackerKnowledge : AttackerKnowledge.Has attackerKnowledge

instance DY.Example.SignedDH.instHasSubFLength : BytesLength.Has SubF.length

@[instance_reducible]

instance DY.Example.SignedDH.instHasSubF : BytesFunctor.Has SubF

Equations

• DY.Example.SignedDH.instHasSubF = { toSubFunctorTC := DY.ALaCarte.instSubFunctorTC DY.Example.SignedDH.SubF }

@[instance_reducible]

instance DY.Example.SignedDH.instHasExecBytes : HasExecBytes

Equations

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

@[instance_reducible]

instance DY.Example.SignedDH.instBaseAttackerKnowledge_examples : BaseAttackerKnowledge

Equations

• DY.Example.SignedDH.instBaseAttackerKnowledge_examples = { attackerKnows := DY.Example.SignedDH.baseAttackerKnowledge }

@[instance_reducible]

instance DY.Example.SignedDH.instExecTraceTypes_examples : ExecTraceTypes

Equations

• DY.Example.SignedDH.instExecTraceTypes_examples = { ExecT := DY.Example.SignedDH.ExecEntryT }

def DY.Example.SignedDH.ExecEntryT.internal : Fin 7 → Type

Equations

• DY.Example.SignedDH.ExecEntryT.internal 0 = DY.Network.ExecEntryT
• DY.Example.SignedDH.ExecEntryT.internal 1 = DY.Random.ExecEntryT
• DY.Example.SignedDH.ExecEntryT.internal 2 = DY.ProtocolEvent.ExecEntryT DY.Example.SignedDH.SignedDHEvent
• DY.Example.SignedDH.ExecEntryT.internal 3 = DY.PersistentLocalState.CompromisableState.ExecEntryT DY.Example.SignedDH.ClientInitiateState
• DY.Example.SignedDH.ExecEntryT.internal 4 = DY.PersistentLocalState.CompromisableState.ExecEntryT DY.Example.SignedDH.ClientFinishState
• DY.Example.SignedDH.ExecEntryT.internal 5 = DY.PersistentLocalState.CompromisableState.ExecEntryT DY.Example.SignedDH.ServerFinishState
• DY.Example.SignedDH.ExecEntryT.internal 6 = DY.LongTermKeys.ExecEntryT "SignedDH PKI"
• DY.Example.SignedDH.ExecEntryT.internal ⟨n.succ.succ.succ.succ.succ.succ.succ, isLt⟩ = ⋯.elim

@[instance_reducible]

def DY.Example.SignedDH.baseAttackerKnowledge : SubBaseAttackerKnowledge ExecEntryT

Equations

• DY.Example.SignedDH.baseAttackerKnowledge = DY.SubBaseAttackerKnowledge.combine DY.Example.SignedDH.baseAttackerKnowledge.internal

def DY.Example.SignedDH.baseAttackerKnowledge.internal (id✝ : Fin 7) : SubBaseAttackerKnowledge (ExecEntryT.internal id✝)

Equations

• DY.Example.SignedDH.baseAttackerKnowledge.internal 0 = DY.Network.baseAttackerKnowledge
• DY.Example.SignedDH.baseAttackerKnowledge.internal 1 = DY.Random.baseAttackerKnowledge
• DY.Example.SignedDH.baseAttackerKnowledge.internal 2 = DY.ProtocolEvent.baseAttackerKnowledge DY.Example.SignedDH.SignedDHEvent
• DY.Example.SignedDH.baseAttackerKnowledge.internal 3 = DY.PersistentLocalState.CompromisableState.baseAttackerKnowledge DY.Example.SignedDH.ClientInitiateState
• DY.Example.SignedDH.baseAttackerKnowledge.internal 4 = DY.PersistentLocalState.CompromisableState.baseAttackerKnowledge DY.Example.SignedDH.ClientFinishState
• DY.Example.SignedDH.baseAttackerKnowledge.internal 5 = DY.PersistentLocalState.CompromisableState.baseAttackerKnowledge DY.Example.SignedDH.ServerFinishState
• DY.Example.SignedDH.baseAttackerKnowledge.internal 6 = DY.LongTermKeys.baseAttackerKnowledge "SignedDH PKI"
• DY.Example.SignedDH.baseAttackerKnowledge.internal ⟨n.succ.succ.succ.succ.succ.succ.succ, isLt⟩ = ⋯.elim

@[instance_reducible]

instance DY.Example.SignedDH.instHasExecEntryT : ExecTraceTypes.Has ExecEntryT

Equations

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

@[instance_reducible]

def DY.Example.SignedDH.ExecEntryT : Type

Equations

• DY.Example.SignedDH.ExecEntryT = DY.ExecTraceTypes.combine DY.Example.SignedDH.ExecEntryT.internal

instance DY.Example.SignedDH.instHasExecEntryTBaseAttackerKnowledge : BaseAttackerKnowledge.Has baseAttackerKnowledge

@[instance_reducible]

instance DY.Example.SignedDH.instHasExecTrace : HasExecTrace

Equations

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

@[instance_reducible]

def DY.Example.SignedDH.ProofEntryT : Type

Equations

• DY.Example.SignedDH.ProofEntryT = DY.ProofTraceTypes.combine DY.Example.SignedDH.ProofEntryT.internal

@[instance_reducible]

instance DY.Example.SignedDH.instProofTraceTypes_examples : ProofTraceTypes

Equations

• DY.Example.SignedDH.instProofTraceTypes_examples = { ProofT := DY.Example.SignedDH.ProofEntryT, tc := DY.Example.SignedDH.wfInst✝ }

@[instance_reducible]

instance DY.Example.SignedDH.instHasExecEntryTProofEntryT : ProofTraceTypes.Has ProofEntryT

Equations

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

def DY.Example.SignedDH.ProofEntryT.internal : Fin 7 → Type

Equations

• DY.Example.SignedDH.ProofEntryT.internal 0 = DY.Network.ProofEntryT
• DY.Example.SignedDH.ProofEntryT.internal 1 = DY.Random.ProofEntryT
• DY.Example.SignedDH.ProofEntryT.internal 2 = DY.ProtocolEvent.ProofEntryT DY.Example.SignedDH.SignedDHEvent
• DY.Example.SignedDH.ProofEntryT.internal 3 = DY.PersistentLocalState.CompromisableState.ProofEntryT DY.Example.SignedDH.ClientInitiateState
• DY.Example.SignedDH.ProofEntryT.internal 4 = DY.PersistentLocalState.CompromisableState.ProofEntryT DY.Example.SignedDH.ClientFinishState
• DY.Example.SignedDH.ProofEntryT.internal 5 = DY.PersistentLocalState.CompromisableState.ProofEntryT DY.Example.SignedDH.ServerFinishState
• DY.Example.SignedDH.ProofEntryT.internal 6 = DY.LongTermKeys.ProofEntryT "SignedDH PKI"
• DY.Example.SignedDH.ProofEntryT.internal ⟨n.succ.succ.succ.succ.succ.succ.succ, isLt⟩ = ⋯.elim

@[instance_reducible]

instance DY.Example.SignedDH.instHasProofTrace : HasProofTrace

Equations

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

instance DY.Example.SignedDH.instBytesInvariantsProofs_examples : BytesInvariantsProofs

theorem DY.Example.SignedDH.invariantsProofs : Bytes.PartialInvariantsProofs invariants

def DY.Example.SignedDH.invariants.internal (id✝ : Fin 6) : Bytes.PartialInvariants (SubF.internal id✝)

Equations

• DY.Example.SignedDH.invariants.internal 0 = DY.Random.invariants
• DY.Example.SignedDH.invariants.internal 1 = DY.Literal.invariants
• DY.Example.SignedDH.invariants.internal 2 = DY.Concat.invariants
• DY.Example.SignedDH.invariants.internal 3 = DY.Hash.invariants
• DY.Example.SignedDH.invariants.internal 4 = DY.Signature.invariants
• DY.Example.SignedDH.invariants.internal 5 = DY.DiffieHellman.invariants
• DY.Example.SignedDH.invariants.internal ⟨n.succ.succ.succ.succ.succ.succ, isLt⟩ = ⋯.elim

theorem DY.Example.SignedDH.invariantsProofs.internal (id✝ : Fin 6) : Bytes.PartialInvariantsProofs (invariants.internal id✝)

@[instance_reducible]

def DY.Example.SignedDH.invariants : Bytes.PartialInvariants SubF

Equations

• DY.Example.SignedDH.invariants = DY.Bytes.PartialInvariants.combine DY.Example.SignedDH.invariants.internal

instance DY.Example.SignedDH.instHasSubFInvariants : BytesInvariants.Has invariants

@[instance_reducible]

instance DY.Example.SignedDH.instBytesInvariants_examples : BytesInvariants

Equations

• DY.Example.SignedDH.instBytesInvariants_examples = { invs := DY.Example.SignedDH.invariants }

@[instance_reducible]

instance DY.Example.SignedDH.instHasBytesInvariants : HasBytesInvariants

Equations

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

instance DY.Example.SignedDH.instHasExecEntryTProofEntryT_1 : TraceInvariant.Has ProofEntryT

@[instance_reducible]

instance DY.Example.SignedDH.instTraceInvariant_examples : TraceInvariant

Equations

• DY.Example.SignedDH.instTraceInvariant_examples = { tc_inv := { invariant := DY.Example.SignedDH.instTraceInvariant_examples._aux_1 } }

instance DY.Example.SignedDH.instBaseAttackerKnowledgeTheorem_examples : BaseAttackerKnowledgeTheorem

@[instance_reducible]

instance DY.Example.SignedDH.instSubTraceInvariantExecEntryTProofEntryT : SubTraceInvariant ProofEntryT

Equations

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

instance DY.Example.SignedDH.instAttackerKnowledgeTheorem_examples : AttackerKnowledgeTheorem

@[instance_reducible]

instance DY.Example.SignedDH.instHasTraceInvariant : HasTraceInvariant

Equations

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