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

Equations

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

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

@[instance_reducible]

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

Equations

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

@[instance_reducible]

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

Equations

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

@[instance_reducible]

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

Equations

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

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

@[instance_reducible]

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

Equations

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

@[instance_reducible]

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

Equations

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

@[instance_reducible]

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

Equations

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

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

Equations

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

@[instance_reducible]

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

Equations

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

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

Equations

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

@[instance_reducible]

instance DY.Example.ACME.WithoutDEO.instHasExecBytesWithoutDEO : HasExecBytesWithoutDEO

Equations

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

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

Equations

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

@[instance_reducible]

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

Equations

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

@[instance_reducible]

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

Equations

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

@[instance_reducible]

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

Equations

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

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

@[instance_reducible]

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

Equations

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

@[instance_reducible]

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

Equations

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

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

Equations

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

@[instance_reducible]

instance DY.Example.ACME.WithoutDEO.instHasExecTraceWithoutDEO : HasExecTraceWithoutDEO

Equations

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

def DY.Example.ACME.WithoutDEO.ProofEntryT.internal : Fin 8 → Type

Equations

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

@[instance_reducible]

instance DY.Example.ACME.WithoutDEO.instProofTraceTypes_examples : ProofTraceTypes

Equations

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

@[instance_reducible]

instance DY.Example.ACME.WithoutDEO.instHasExecEntryTProofEntryT : ProofTraceTypes.Has ProofEntryT

Equations

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

@[instance_reducible]

def DY.Example.ACME.WithoutDEO.ProofEntryT : Type

Equations

• DY.Example.ACME.WithoutDEO.ProofEntryT = DY.ProofTraceTypes.combine DY.Example.ACME.WithoutDEO.ProofEntryT.internal

@[instance_reducible]

instance DY.Example.ACME.WithoutDEO.instHasProofTrace : HasProofTrace

Equations

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

instance DY.Example.ACME.WithoutDEO.instBytesInvariantsProofs_examples : BytesInvariantsProofs

def DY.Example.ACME.WithoutDEO.invariants.internal (id✝ : Fin 4) : Bytes.PartialInvariants (SubF.internal id✝)

Equations

• DY.Example.ACME.WithoutDEO.invariants.internal 0 = DY.Random.invariants
• DY.Example.ACME.WithoutDEO.invariants.internal 1 = DY.Literal.invariants
• DY.Example.ACME.WithoutDEO.invariants.internal 2 = DY.Concat.invariants
• DY.Example.ACME.WithoutDEO.invariants.internal 3 = DY.Signature.invariants
• DY.Example.ACME.WithoutDEO.invariants.internal ⟨n.succ.succ.succ.succ, isLt⟩ = ⋯.elim

@[instance_reducible]

instance DY.Example.ACME.WithoutDEO.instBytesInvariants_examples : BytesInvariants

Equations

• DY.Example.ACME.WithoutDEO.instBytesInvariants_examples = { invs := DY.Example.ACME.WithoutDEO.invariants }

theorem DY.Example.ACME.WithoutDEO.invariantsProofs.internal (id✝ : Fin 4) : Bytes.PartialInvariantsProofs (invariants.internal id✝)

theorem DY.Example.ACME.WithoutDEO.invariantsProofs : Bytes.PartialInvariantsProofs invariants

@[instance_reducible]

def DY.Example.ACME.WithoutDEO.invariants : Bytes.PartialInvariants SubF

Equations

• DY.Example.ACME.WithoutDEO.invariants = DY.Bytes.PartialInvariants.combine DY.Example.ACME.WithoutDEO.invariants.internal

instance DY.Example.ACME.WithoutDEO.instHasSubFInvariants : BytesInvariants.Has invariants

@[instance_reducible]

instance DY.Example.ACME.WithoutDEO.instHasBytesInvariants : HasBytesInvariants

Equations

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

instance DY.Example.ACME.WithoutDEO.instHasExecEntryTProofEntryT_1 : TraceInvariant.Has ProofEntryT

@[instance_reducible]

instance DY.Example.ACME.WithoutDEO.instTraceInvariant_examples : TraceInvariant

Equations

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

instance DY.Example.ACME.WithoutDEO.instBaseAttackerKnowledgeTheorem_examples : BaseAttackerKnowledgeTheorem

@[instance_reducible]

instance DY.Example.ACME.WithoutDEO.instSubTraceInvariantExecEntryTProofEntryT : SubTraceInvariant ProofEntryT

Equations

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

instance DY.Example.ACME.WithoutDEO.instAttackerKnowledgeTheorem_examples : AttackerKnowledgeTheorem

@[instance_reducible]

instance DY.Example.ACME.WithoutDEO.instHasTraceInvariant : HasTraceInvariant

Equations

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