class DY.Example.ACME.HasExecBytes : Type 1

• bytesFunc : BytesFunctor
• bytesFunc0 : BytesFunctor.Has Random.SubF
• bytesFunc1 : BytesFunctor.Has Literal.SubF
• bytesFunc2 : BytesFunctor.Has Concat.SubF
• canSign : Signature.CanSign Bytes
• bytesLen : BytesLength
• bytesLen0 : BytesLength.Has Random.SubF.length
• bytesLen1 : BytesLength.Has Literal.SubF.length
• bytesLen2 : BytesLength.Has Concat.SubF.length
• att : AttackerKnowledge
• att0 : AttackerKnowledge.Has Random.attackerKnowledge
• att1 : AttackerKnowledge.Has Literal.attackerKnowledge
• att2 : AttackerKnowledge.Has Concat.attackerKnowledge

structure DY.Example.ACME.LetsEncryptMessage [HasExecBytes] : Type

• token : Bytes
• sig : Bytes

structure DY.Example.ACME.OwnerMessage [HasExecBytes] : Type

• address : String
• oPk : Bytes

structure DY.Example.ACME.OwnerKeyState [HasExecBytes] : Type

• oSk : Bytes

structure DY.Example.ACME.OwnerAddressState [HasExecBytes] : Type

• address : String
• oSk : Bytes

structure DY.Example.ACME.LetsEncryptPendingChallengeState [HasExecBytes] : Type

• address : String
• token : Bytes

structure DY.Example.ACME.DNSEntry [HasExecBytes] : Type

• address : String
• sig : Bytes

inductive DY.Example.ACME.ACMEEvent [HasExecBytes] : Type

• OwnerRegisterAddress [HasExecBytes] (address : String) (oPk : Bytes) : ACMEEvent
• LetsEncryptAcceptAddress [HasExecBytes] (address : String) (oPk : Bytes) : ACMEEvent

@[instance_reducible]

instance DY.Example.ACME.instDecidableEqACMEEvent {inst✝ : HasExecBytes} : DecidableEq ACMEEvent

Equations

• DY.Example.ACME.instDecidableEqACMEEvent = DY.Example.ACME.instDecidableEqACMEEvent.decEq

def DY.Example.ACME.instDecidableEqACMEEvent.decEq {inst✝ : HasExecBytes} (x✝ x✝¹ : ACMEEvent) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• DY.Example.ACME.instDecidableEqACMEEvent.decEq (DY.Example.ACME.ACMEEvent.OwnerRegisterAddress address oPk) (DY.Example.ACME.ACMEEvent.LetsEncryptAcceptAddress address_1 oPk_1) = isFalse ⋯
• DY.Example.ACME.instDecidableEqACMEEvent.decEq (DY.Example.ACME.ACMEEvent.LetsEncryptAcceptAddress address oPk) (DY.Example.ACME.ACMEEvent.OwnerRegisterAddress address_1 oPk_1) = isFalse ⋯

@[instance_reducible]

instance DY.Example.ACME.instParseableSerializeableLetsEncryptMessage [HasExecBytes] : Comparse.ParseableSerializeable LetsEncryptMessage

Equations

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

theorem DY.Example.ACME.LetsEncryptMessage.IsWellFormed_eq [HasExecBytes] {τ : Sort u_1} (pre : Bytes → τ → Prop) [Comparse.BytesCompatibleTracePred pre] (x : LetsEncryptMessage) (tr : τ) : Comparse.IsWellFormed pre x tr = (pre x.token tr ∧ pre x.sig tr)

@[instance_reducible]

instance DY.Example.ACME.instParseableSerializeableOwnerMessage [HasExecBytes] : Comparse.ParseableSerializeable OwnerMessage

Equations

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

theorem DY.Example.ACME.OwnerMessage.IsWellFormed_eq [HasExecBytes] {τ : Sort u_1} (pre : Bytes → τ → Prop) [Comparse.BytesCompatibleTracePred pre] (x : OwnerMessage) (tr : τ) : Comparse.IsWellFormed pre x tr = pre x.oPk tr

@[instance_reducible]

instance DY.Example.ACME.instParseableSerializeableOwnerKeyState [HasExecBytes] : Comparse.ParseableSerializeable OwnerKeyState

Equations

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

theorem DY.Example.ACME.OwnerKeyState.IsWellFormed_eq [HasExecBytes] {τ : Sort u_1} (pre : Bytes → τ → Prop) [Comparse.BytesCompatibleTracePred pre] (x : OwnerKeyState) (tr : τ) : Comparse.IsWellFormed pre x tr = pre x.oSk tr

@[instance_reducible]

instance DY.Example.ACME.instParseableSerializeableNEOwnerAddressState [HasExecBytes] : Comparse.ParseableSerializeableNE OwnerAddressState

Equations

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

theorem DY.Example.ACME.OwnerAddressState.IsWellFormed_eq [HasExecBytes] {τ : Sort u_1} (pre : Bytes → τ → Prop) [Comparse.BytesCompatibleTracePred pre] (x : OwnerAddressState) (tr : τ) : Comparse.IsWellFormed pre x tr = pre x.oSk tr

@[instance_reducible]

instance DY.Example.ACME.instParseableSerializeableNELetsEncryptPendingChallengeState [HasExecBytes] : Comparse.ParseableSerializeableNE LetsEncryptPendingChallengeState

Equations

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

theorem DY.Example.ACME.LetsEncryptPendingChallengeState.IsWellFormed_eq [HasExecBytes] {τ : Sort u_1} (pre : Bytes → τ → Prop) [Comparse.BytesCompatibleTracePred pre] (x : LetsEncryptPendingChallengeState) (tr : τ) : Comparse.IsWellFormed pre x tr = pre x.token tr

@[instance_reducible]

instance DY.Example.ACME.instParseableSerializeableDNSEntry [HasExecBytes] : Comparse.ParseableSerializeable DNSEntry

Equations

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

theorem DY.Example.ACME.DNSEntry.IsWellFormed_eq [HasExecBytes] {τ : Sort u_1} (pre : Bytes → τ → Prop) [Comparse.BytesCompatibleTracePred pre] (x : DNSEntry) (tr : τ) : Comparse.IsWellFormed pre x tr = pre x.sig tr

class DY.Example.ACME.HasExecTraceextends DY.Example.ACME.HasExecBytes : Type 1

• bytesFunc : BytesFunctor
• bytesFunc0 : BytesFunctor.Has Random.SubF
• bytesFunc1 : BytesFunctor.Has Literal.SubF
• bytesFunc2 : BytesFunctor.Has Concat.SubF
• canSign : Signature.CanSign Bytes
• bytesLen : BytesLength
• bytesLen0 : BytesLength.Has Random.SubF.length
• bytesLen1 : BytesLength.Has Literal.SubF.length
• bytesLen2 : BytesLength.Has Concat.SubF.length
• att : AttackerKnowledge
• att0 : AttackerKnowledge.Has Random.attackerKnowledge
• att1 : AttackerKnowledge.Has Literal.attackerKnowledge
• att2 : AttackerKnowledge.Has Concat.attackerKnowledge
• traceExec : ExecTraceTypes
• traceExec0 : ExecTraceTypes.Has Network.ExecEntryT
• traceExec1 : ExecTraceTypes.Has Random.ExecEntryT
• traceExec2 : ExecTraceTypes.Has (ProtocolEvent.ExecEntryT ACMEEvent)
• traceExec3 : ExecTraceTypes.Has (PersistentLocalState.CompromisableState.ExecEntryT OwnerKeyState)
• traceExec4 : ExecTraceTypes.Has (PersistentLocalState.CompromisableState.ExecEntryT OwnerAddressState)
• traceExec5 : ExecTraceTypes.Has (PersistentLocalState.CompromisableState.ExecEntryT LetsEncryptPendingChallengeState)
• traceExec6 : ExecTraceTypes.Has (PersistentGlobalState.CompromisableState.ExecEntryT DNSEntry)
• traceExec7 : ExecTraceTypes.Has (LongTermKeys.ExecEntryT "ACME PKI")
• attBase : BaseAttackerKnowledge

@[instance_reducible]

instance DY.Example.ACME.instExecConfigVkBytes_examples [HasExecTrace] : LongTermKeys.ExecConfig "ACME PKI" Signature.vk

Equations

• DY.Example.ACME.instExecConfigVkBytes_examples = { }

def DY.Example.ACME.Owner.generateKeyPair [HasExecTrace] (owner : Participant) : Traceful (Nat × Nat)

Equations

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

def DY.Example.ACME.Owner.claimAddress [HasExecTrace] (owner : Participant) (address : String) (oSkHandle : Nat) : Traceful Nat

Equations

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

def DY.Example.ACME.LetsEncrypt.initiate [HasExecTrace] (server : Participant) (address : String) (skHandle : Nat) : Traceful (Nat × Nat)

Equations

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

def DY.Example.ACME.Owner.respond [HasExecTrace] (owner server : Participant) (msgHandle lePkHandle stHandle : Nat) : Traceful (Nat × Nat)

Equations

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

def DY.Example.ACME.LetsEncrypt.finish [HasExecTrace] (server : Participant) (msgHandle pendingStHandle dnsEntryHandle : Nat) : Traceful Unit

Equations

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

def DY.Example.ACME.OwnerKeyState.compromise [HasExecTrace] (stHandle : Nat) : Traceful Nat

Equations

• DY.Example.ACME.OwnerKeyState.compromise stHandle = DY.PersistentLocalState.compromise DY.Example.ACME.OwnerKeyState stHandle

def DY.Example.ACME.OwnerAddressState.compromise [HasExecTrace] (stHandle : Nat) : Traceful Nat

Equations

• DY.Example.ACME.OwnerAddressState.compromise stHandle = DY.PersistentLocalState.compromise DY.Example.ACME.OwnerAddressState stHandle

def DY.Example.ACME.LetsEncryptPendingChallengeState.compromise [HasExecTrace] (stHandle : Nat) : Traceful Nat

Equations

• DY.Example.ACME.LetsEncryptPendingChallengeState.compromise stHandle = DY.PersistentLocalState.compromise DY.Example.ACME.LetsEncryptPendingChallengeState stHandle

def DY.Example.ACME.DNSEntry.compromise [HasExecTrace] (stHandle : Nat) : Traceful Nat

Equations

• DY.Example.ACME.DNSEntry.compromise stHandle = DY.PersistentGlobalState.compromise DY.Example.ACME.DNSEntry stHandle

def DY.Example.ACME.Owner.generateKeyPair.reachability [HasExecTrace] : ReachabilityConfig

Equations

• DY.Example.ACME.Owner.generateKeyPair.reachability = DY.ReachabilityConfig.make fun (owner : DY.Participant) => DY.Example.ACME.Owner.generateKeyPair owner

def DY.Example.ACME.Owner.claimAddress.reachability [HasExecTrace] : ReachabilityConfig

Equations

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

def DY.Example.ACME.LetsEncrypt.initiate.reachability [HasExecTrace] : ReachabilityConfig

Equations

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

def DY.Example.ACME.Owner.respond.reachability [HasExecTrace] : ReachabilityConfig

Equations

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

def DY.Example.ACME.LetsEncrypt.finish.reachability [HasExecTrace] : ReachabilityConfig

Equations

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

def DY.Example.ACME.OwnerKeyState.compromise.reachability [HasExecTrace] : ReachabilityConfig

Equations

• DY.Example.ACME.OwnerKeyState.compromise.reachability = DY.ReachabilityConfig.make fun (stHandle : Nat) => DY.Example.ACME.OwnerKeyState.compromise stHandle

def DY.Example.ACME.OwnerAddressState.compromise.reachability [HasExecTrace] : ReachabilityConfig

Equations

• DY.Example.ACME.OwnerAddressState.compromise.reachability = DY.ReachabilityConfig.make fun (stHandle : Nat) => DY.Example.ACME.OwnerAddressState.compromise stHandle

def DY.Example.ACME.LetsEncryptPendingChallengeState.compromise.reachability [HasExecTrace] : ReachabilityConfig

Equations

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

def DY.Example.ACME.DNSEntry.compromise.reachability [HasExecTrace] : ReachabilityConfig

Equations

• DY.Example.ACME.DNSEntry.compromise.reachability = DY.ReachabilityConfig.make fun (stHandle : Nat) => DY.Example.ACME.DNSEntry.compromise stHandle

def DY.Example.ACME.reachability.internal [HasExecTrace] : Fin 11 → ReachabilityConfig

Equations

• DY.Example.ACME.reachability.internal 0 = DY.Network.reachability
• DY.Example.ACME.reachability.internal 1 = DY.LongTermKeys.reachability "ACME PKI"
• DY.Example.ACME.reachability.internal 2 = DY.Example.ACME.Owner.generateKeyPair.reachability
• DY.Example.ACME.reachability.internal 3 = DY.Example.ACME.Owner.claimAddress.reachability
• DY.Example.ACME.reachability.internal 4 = DY.Example.ACME.LetsEncrypt.initiate.reachability
• DY.Example.ACME.reachability.internal 5 = DY.Example.ACME.Owner.respond.reachability
• DY.Example.ACME.reachability.internal 6 = DY.Example.ACME.LetsEncrypt.finish.reachability
• DY.Example.ACME.reachability.internal 7 = DY.Example.ACME.OwnerKeyState.compromise.reachability
• DY.Example.ACME.reachability.internal 8 = DY.Example.ACME.OwnerAddressState.compromise.reachability
• DY.Example.ACME.reachability.internal 9 = DY.Example.ACME.LetsEncryptPendingChallengeState.compromise.reachability
• DY.Example.ACME.reachability.internal 10 = DY.Example.ACME.DNSEntry.compromise.reachability
• DY.Example.ACME.reachability.internal ⟨n.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ, isLt⟩ = ⋯.elim

@[instance_reducible]

def DY.Example.ACME.reachability [HasExecTrace] : ReachabilityConfig

Equations

• DY.Example.ACME.reachability = DY.ReachabilityConfig.combine DY.Example.ACME.reachability.internal