@[instance_reducible]

instance DY.Example.ACME.WithDEO.instBytesFunctor_examples : BytesFunctor

Equations

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

@[instance_reducible]

instance DY.Example.ACME.WithDEO.instHasSubF : BytesFunctor.Has SubF

Equations

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

@[instance_reducible]

def DY.Example.ACME.WithDEO.SubF : Type → Type

Equations

• DY.Example.ACME.WithDEO.SubF = DY.BytesFunctor.combine DY.Example.ACME.WithDEO.SubF.internal

@[instance_reducible]

instance DY.Example.ACME.WithDEO.instBytesLength_examples : BytesLength

Equations

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

@[instance_reducible]

def DY.Example.ACME.WithDEO.SubF.length : Bytes.PartialLength SubF

Equations

• DY.Example.ACME.WithDEO.SubF.length = DY.Bytes.PartialLength.combine DY.Example.ACME.WithDEO.SubF.length.internal

@[instance_reducible]

def DY.Example.ACME.WithDEO.attackerKnowledge : SubAttackerKnowledge SubF

Equations

• DY.Example.ACME.WithDEO.attackerKnowledge = DY.SubAttackerKnowledge.combine DY.Example.ACME.WithDEO.attackerKnowledge.internal

instance DY.Example.ACME.WithDEO.instHasSubFAttackerKnowledge : AttackerKnowledge.Has attackerKnowledge

instance DY.Example.ACME.WithDEO.instHasSubFLength : BytesLength.Has SubF.length

@[instance_reducible]

instance DY.Example.ACME.WithDEO.instAttackerKnowledge_examples : AttackerKnowledge

Equations

• DY.Example.ACME.WithDEO.instAttackerKnowledge_examples = { attackerKnowledge := DY.Example.ACME.WithDEO.attackerKnowledge }

def DY.Example.ACME.WithDEO.attackerKnowledge.internal (id✝ : Fin 4) : SubAttackerKnowledge (SubF.internal id✝)

Equations

• DY.Example.ACME.WithDEO.attackerKnowledge.internal 0 = DY.Random.attackerKnowledge
• DY.Example.ACME.WithDEO.attackerKnowledge.internal 1 = DY.Literal.attackerKnowledge
• DY.Example.ACME.WithDEO.attackerKnowledge.internal 2 = DY.Concat.attackerKnowledge
• DY.Example.ACME.WithDEO.attackerKnowledge.internal 3 = DY.Example.ACME.WithDEO.SignDEO.attackerKnowledge
• DY.Example.ACME.WithDEO.attackerKnowledge.internal ⟨n.succ.succ.succ.succ, isLt⟩ = ⋯.elim

def DY.Example.ACME.WithDEO.SubF.length.internal (id✝ : Fin 4) : Bytes.PartialLength (SubF.internal id✝)

Equations

• DY.Example.ACME.WithDEO.SubF.length.internal 0 = DY.Random.SubF.length
• DY.Example.ACME.WithDEO.SubF.length.internal 1 = DY.Literal.SubF.length
• DY.Example.ACME.WithDEO.SubF.length.internal 2 = DY.Concat.SubF.length
• DY.Example.ACME.WithDEO.SubF.length.internal 3 = DY.Example.ACME.WithDEO.SignDEO.SubF.length
• DY.Example.ACME.WithDEO.SubF.length.internal ⟨n.succ.succ.succ.succ, isLt⟩ = ⋯.elim

def DY.Example.ACME.WithDEO.SubF.internal : Fin 4 → Type → Type

Equations

• DY.Example.ACME.WithDEO.SubF.internal 0 = DY.Random.SubF
• DY.Example.ACME.WithDEO.SubF.internal 1 = DY.Literal.SubF
• DY.Example.ACME.WithDEO.SubF.internal 2 = DY.Concat.SubF
• DY.Example.ACME.WithDEO.SubF.internal 3 = DY.Example.ACME.WithDEO.SignDEO.SubF
• DY.Example.ACME.WithDEO.SubF.internal ⟨n.succ.succ.succ.succ, isLt⟩ = ⋯.elim

@[instance_reducible]

instance DY.Example.ACME.WithDEO.instHasExecBytes : HasExecBytes

Equations

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

@[instance_reducible]

def DY.Example.ACME.WithDEO.baseAttackerKnowledge : SubBaseAttackerKnowledge ExecEntryT

Equations

• DY.Example.ACME.WithDEO.baseAttackerKnowledge = DY.SubBaseAttackerKnowledge.combine DY.Example.ACME.WithDEO.baseAttackerKnowledge.internal

def DY.Example.ACME.WithDEO.ExecEntryT.internal : Fin 8 → Type

Equations

• DY.Example.ACME.WithDEO.ExecEntryT.internal 0 = DY.Network.ExecEntryT
• DY.Example.ACME.WithDEO.ExecEntryT.internal 1 = DY.Random.ExecEntryT
• DY.Example.ACME.WithDEO.ExecEntryT.internal 2 = DY.ProtocolEvent.ExecEntryT DY.Example.ACME.ACMEEvent
• DY.Example.ACME.WithDEO.ExecEntryT.internal 3 = DY.PersistentLocalState.CompromisableState.ExecEntryT DY.Example.ACME.OwnerKeyState
• DY.Example.ACME.WithDEO.ExecEntryT.internal 4 = DY.PersistentLocalState.CompromisableState.ExecEntryT DY.Example.ACME.OwnerAddressState
• DY.Example.ACME.WithDEO.ExecEntryT.internal 5 = DY.PersistentLocalState.CompromisableState.ExecEntryT DY.Example.ACME.LetsEncryptPendingChallengeState
• DY.Example.ACME.WithDEO.ExecEntryT.internal 6 = DY.PersistentGlobalState.CompromisableState.ExecEntryT DY.Example.ACME.DNSEntry
• DY.Example.ACME.WithDEO.ExecEntryT.internal 7 = DY.LongTermKeys.ExecEntryT "ACME PKI"
• DY.Example.ACME.WithDEO.ExecEntryT.internal ⟨n.succ.succ.succ.succ.succ.succ.succ.succ, isLt⟩ = ⋯.elim

@[instance_reducible]

def DY.Example.ACME.WithDEO.ExecEntryT : Type

Equations

• DY.Example.ACME.WithDEO.ExecEntryT = DY.ExecTraceTypes.combine DY.Example.ACME.WithDEO.ExecEntryT.internal

@[instance_reducible]

instance DY.Example.ACME.WithDEO.instExecTraceTypes_examples : ExecTraceTypes

Equations

• DY.Example.ACME.WithDEO.instExecTraceTypes_examples = { ExecT := DY.Example.ACME.WithDEO.ExecEntryT }

def DY.Example.ACME.WithDEO.baseAttackerKnowledge.internal (id✝ : Fin 8) : SubBaseAttackerKnowledge (ExecEntryT.internal id✝)

Equations

• DY.Example.ACME.WithDEO.baseAttackerKnowledge.internal 0 = DY.Network.baseAttackerKnowledge
• DY.Example.ACME.WithDEO.baseAttackerKnowledge.internal 1 = DY.Random.baseAttackerKnowledge
• DY.Example.ACME.WithDEO.baseAttackerKnowledge.internal 2 = DY.ProtocolEvent.baseAttackerKnowledge DY.Example.ACME.ACMEEvent
• DY.Example.ACME.WithDEO.baseAttackerKnowledge.internal 3 = DY.PersistentLocalState.CompromisableState.baseAttackerKnowledge DY.Example.ACME.OwnerKeyState
• DY.Example.ACME.WithDEO.baseAttackerKnowledge.internal 4 = DY.PersistentLocalState.CompromisableState.baseAttackerKnowledge DY.Example.ACME.OwnerAddressState
• DY.Example.ACME.WithDEO.baseAttackerKnowledge.internal 5 = DY.PersistentLocalState.CompromisableState.baseAttackerKnowledge DY.Example.ACME.LetsEncryptPendingChallengeState
• DY.Example.ACME.WithDEO.baseAttackerKnowledge.internal 6 = DY.PersistentGlobalState.CompromisableState.baseAttackerKnowledge DY.Example.ACME.DNSEntry
• DY.Example.ACME.WithDEO.baseAttackerKnowledge.internal 7 = DY.LongTermKeys.baseAttackerKnowledge "ACME PKI"
• DY.Example.ACME.WithDEO.baseAttackerKnowledge.internal ⟨n.succ.succ.succ.succ.succ.succ.succ.succ, isLt⟩ = ⋯.elim

@[instance_reducible]

instance DY.Example.ACME.WithDEO.instBaseAttackerKnowledge_examples : BaseAttackerKnowledge

Equations

• DY.Example.ACME.WithDEO.instBaseAttackerKnowledge_examples = { attackerKnows := DY.Example.ACME.WithDEO.baseAttackerKnowledge }

@[instance_reducible]

instance DY.Example.ACME.WithDEO.instHasExecEntryT : ExecTraceTypes.Has ExecEntryT

Equations

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

instance DY.Example.ACME.WithDEO.instHasExecEntryTBaseAttackerKnowledge : BaseAttackerKnowledge.Has baseAttackerKnowledge

@[instance_reducible]

instance DY.Example.ACME.WithDEO.instHasExecTrace : HasExecTrace

Equations

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