def DY.Example.SignedDHKEM.SubF.length.internal (id✝ : Fin 7) : Bytes.PartialLength (SubF.internal id✝)

Equations

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

@[instance_reducible]

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

Equations

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

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

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

@[instance_reducible]

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

Equations

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

@[instance_reducible]

instance DY.Example.SignedDHKEM.instBytesFunctor_examples : BytesFunctor

Equations

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

def DY.Example.SignedDHKEM.attackerKnowledge.internal (id✝ : Fin 7) : SubAttackerKnowledge (SubF.internal id✝)

Equations

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

def DY.Example.SignedDHKEM.SubF.internal : Fin 7 → Type → Type

Equations

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

@[instance_reducible]

instance DY.Example.SignedDHKEM.instAttackerKnowledge_examples : AttackerKnowledge

Equations

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

@[instance_reducible]

def DY.Example.SignedDHKEM.attackerKnowledge : SubAttackerKnowledge SubF

Equations

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

@[instance_reducible]

instance DY.Example.SignedDHKEM.instBytesLength_examples : BytesLength

Equations

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

@[instance_reducible]

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

Equations

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

@[instance_reducible]

instance DY.Example.SignedDHKEM.instHasExecBytes : HasExecBytes

Equations

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

def DY.Example.SignedDHKEM.ExecEntryT.internal : Fin 11 → Type

Equations

• DY.Example.SignedDHKEM.ExecEntryT.internal 0 = DY.Network.ExecEntryT
• DY.Example.SignedDHKEM.ExecEntryT.internal 1 = DY.Random.ExecEntryT
• DY.Example.SignedDHKEM.ExecEntryT.internal 2 = DY.ProtocolEvent.ExecEntryT DY.Example.SignedDHKEM.SignedDHKEMEvent
• DY.Example.SignedDHKEM.ExecEntryT.internal 3 = DY.PersistentLocalState.CompromisableState.ExecEntryT DY.Example.SignedDHKEM.ClientInitiateDHState
• DY.Example.SignedDHKEM.ExecEntryT.internal 4 = DY.PersistentLocalState.CompromisableState.ExecEntryT DY.Example.SignedDHKEM.ClientInitiateKEMState
• DY.Example.SignedDHKEM.ExecEntryT.internal 5 = DY.PersistentLocalState.CompromisableState.ExecEntryT DY.Example.SignedDHKEM.ClientFinishState
• DY.Example.SignedDHKEM.ExecEntryT.internal 6 = DY.PersistentLocalState.CompromisableState.ExecEntryT DY.Example.SignedDHKEM.ServerFinishState
• DY.Example.SignedDHKEM.ExecEntryT.internal 7 = DY.LongTermKeys.ExecEntryT "SignedDHKEM PKI"
• DY.Example.SignedDHKEM.ExecEntryT.internal 8 = DY.KEM.Broken.ExecEntryT
• DY.Example.SignedDHKEM.ExecEntryT.internal 9 = DY.DiffieHellman'.Broken.ExecEntryT
• DY.Example.SignedDHKEM.ExecEntryT.internal 10 = DY.Signature'.Broken.ExecEntryT
• DY.Example.SignedDHKEM.ExecEntryT.internal ⟨n.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ, isLt⟩ = ⋯.elim

@[instance_reducible]

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

Equations

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

def DY.Example.SignedDHKEM.baseAttackerKnowledge.internal (id✝ : Fin 11) : SubBaseAttackerKnowledge (ExecEntryT.internal id✝)

Equations

• DY.Example.SignedDHKEM.baseAttackerKnowledge.internal 0 = DY.Network.baseAttackerKnowledge
• DY.Example.SignedDHKEM.baseAttackerKnowledge.internal 1 = DY.Random.baseAttackerKnowledge
• DY.Example.SignedDHKEM.baseAttackerKnowledge.internal 2 = DY.ProtocolEvent.baseAttackerKnowledge DY.Example.SignedDHKEM.SignedDHKEMEvent
• DY.Example.SignedDHKEM.baseAttackerKnowledge.internal 3 = DY.PersistentLocalState.CompromisableState.baseAttackerKnowledge DY.Example.SignedDHKEM.ClientInitiateDHState
• DY.Example.SignedDHKEM.baseAttackerKnowledge.internal 4 = DY.PersistentLocalState.CompromisableState.baseAttackerKnowledge DY.Example.SignedDHKEM.ClientInitiateKEMState
• DY.Example.SignedDHKEM.baseAttackerKnowledge.internal 5 = DY.PersistentLocalState.CompromisableState.baseAttackerKnowledge DY.Example.SignedDHKEM.ClientFinishState
• DY.Example.SignedDHKEM.baseAttackerKnowledge.internal 6 = DY.PersistentLocalState.CompromisableState.baseAttackerKnowledge DY.Example.SignedDHKEM.ServerFinishState
• DY.Example.SignedDHKEM.baseAttackerKnowledge.internal 7 = DY.LongTermKeys.baseAttackerKnowledge "SignedDHKEM PKI"
• DY.Example.SignedDHKEM.baseAttackerKnowledge.internal 8 = DY.KEM.Broken.baseAttackerKnowledge
• DY.Example.SignedDHKEM.baseAttackerKnowledge.internal 9 = DY.DiffieHellman'.Broken.baseAttackerKnowledge
• DY.Example.SignedDHKEM.baseAttackerKnowledge.internal 10 = DY.Signature'.Broken.baseAttackerKnowledge
• DY.Example.SignedDHKEM.baseAttackerKnowledge.internal ⟨n.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ, isLt⟩ = ⋯.elim

@[instance_reducible]

def DY.Example.SignedDHKEM.baseAttackerKnowledge : SubBaseAttackerKnowledge ExecEntryT

Equations

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

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

@[instance_reducible]

def DY.Example.SignedDHKEM.ExecEntryT : Type

Equations

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

@[instance_reducible]

instance DY.Example.SignedDHKEM.instExecTraceTypes_examples : ExecTraceTypes

Equations

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

@[instance_reducible]

instance DY.Example.SignedDHKEM.instBaseAttackerKnowledge_examples : BaseAttackerKnowledge

Equations

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

@[instance_reducible]

instance DY.Example.SignedDHKEM.instHasExecTrace : HasExecTrace

Equations

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

@[instance_reducible]

instance DY.Example.SignedDHKEM.instProofTraceTypes_examples : ProofTraceTypes

Equations

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

@[instance_reducible]

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

Equations

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

def DY.Example.SignedDHKEM.ProofEntryT.internal : Fin 11 → Type

Equations

• DY.Example.SignedDHKEM.ProofEntryT.internal 0 = DY.Network.ProofEntryT
• DY.Example.SignedDHKEM.ProofEntryT.internal 1 = DY.Random.ProofEntryT
• DY.Example.SignedDHKEM.ProofEntryT.internal 2 = DY.ProtocolEvent.ProofEntryT DY.Example.SignedDHKEM.SignedDHKEMEvent
• DY.Example.SignedDHKEM.ProofEntryT.internal 3 = DY.PersistentLocalState.CompromisableState.ProofEntryT DY.Example.SignedDHKEM.ClientInitiateDHState
• DY.Example.SignedDHKEM.ProofEntryT.internal 4 = DY.PersistentLocalState.CompromisableState.ProofEntryT DY.Example.SignedDHKEM.ClientInitiateKEMState
• DY.Example.SignedDHKEM.ProofEntryT.internal 5 = DY.PersistentLocalState.CompromisableState.ProofEntryT DY.Example.SignedDHKEM.ClientFinishState
• DY.Example.SignedDHKEM.ProofEntryT.internal 6 = DY.PersistentLocalState.CompromisableState.ProofEntryT DY.Example.SignedDHKEM.ServerFinishState
• DY.Example.SignedDHKEM.ProofEntryT.internal 7 = DY.LongTermKeys.ProofEntryT "SignedDHKEM PKI"
• DY.Example.SignedDHKEM.ProofEntryT.internal 8 = DY.KEM.Broken.ProofEntryT
• DY.Example.SignedDHKEM.ProofEntryT.internal 9 = DY.DiffieHellman'.Broken.ProofEntryT
• DY.Example.SignedDHKEM.ProofEntryT.internal 10 = DY.Signature'.Broken.ProofEntryT
• DY.Example.SignedDHKEM.ProofEntryT.internal ⟨n.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ, isLt⟩ = ⋯.elim

@[instance_reducible]

def DY.Example.SignedDHKEM.ProofEntryT : Type

Equations

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

@[instance_reducible]

instance DY.Example.SignedDHKEM.instHasProofTrace : HasProofTrace

Equations

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

@[instance_reducible]

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

Equations

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

theorem DY.Example.SignedDHKEM.invariantsProofs.internal (id✝ : Fin 7) : Bytes.PartialInvariantsProofs (invariants.internal id✝)

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

def DY.Example.SignedDHKEM.invariants.internal (id✝ : Fin 7) : Bytes.PartialInvariants (SubF.internal id✝)

Equations

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

instance DY.Example.SignedDHKEM.instBytesInvariantsProofs_examples : BytesInvariantsProofs

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

@[instance_reducible]

instance DY.Example.SignedDHKEM.instBytesInvariants_examples : BytesInvariants

Equations

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

@[instance_reducible]

instance DY.Example.SignedDHKEM.instHasBytesInvariants : HasBytesInvariants

Equations

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

@[instance_reducible]

instance DY.Example.SignedDHKEM.instTraceInvariant_examples : TraceInvariant

Equations

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

instance DY.Example.SignedDHKEM.instBaseAttackerKnowledgeTheorem_examples : BaseAttackerKnowledgeTheorem

@[instance_reducible]

instance DY.Example.SignedDHKEM.instSubTraceInvariantExecEntryTProofEntryT : SubTraceInvariant ProofEntryT

Equations

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

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

instance DY.Example.SignedDHKEM.instAttackerKnowledgeTheorem_examples : AttackerKnowledgeTheorem

@[instance_reducible]

instance DY.Example.SignedDHKEM.instHasTraceInvariant : HasTraceInvariant

Equations

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