inductive DY.Example.MerkleTree.MerkleTreeNode (Bytes α : Type) : Type

• Empty {Bytes α : Type} : MerkleTreeNode Bytes α
• Leaf {Bytes α : Type} : α → MerkleTreeNode Bytes α
• Internal {Bytes α : Type} : Bytes → Bytes → MerkleTreeNode Bytes α

@[instance_reducible]

instance DY.Example.MerkleTree.instDecidableEqMerkleTreeNode {Bytes✝ α✝ : Type} [DecidableEq Bytes✝] [DecidableEq α✝] : DecidableEq (MerkleTreeNode Bytes✝ α✝)

Equations

• DY.Example.MerkleTree.instDecidableEqMerkleTreeNode = DY.Example.MerkleTree.instDecidableEqMerkleTreeNode.decEq

def DY.Example.MerkleTree.instDecidableEqMerkleTreeNode.decEq {Bytes✝ α✝ : Type} [DecidableEq Bytes✝] [DecidableEq α✝] (x✝ x✝¹ : MerkleTreeNode Bytes✝ α✝) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• DY.Example.MerkleTree.instDecidableEqMerkleTreeNode.decEq DY.Example.MerkleTree.MerkleTreeNode.Empty DY.Example.MerkleTree.MerkleTreeNode.Empty = isTrue ⋯
• DY.Example.MerkleTree.instDecidableEqMerkleTreeNode.decEq DY.Example.MerkleTree.MerkleTreeNode.Empty (DY.Example.MerkleTree.MerkleTreeNode.Leaf a) = isFalse ⋯
• DY.Example.MerkleTree.instDecidableEqMerkleTreeNode.decEq DY.Example.MerkleTree.MerkleTreeNode.Empty (DY.Example.MerkleTree.MerkleTreeNode.Internal a a_1) = isFalse ⋯
• DY.Example.MerkleTree.instDecidableEqMerkleTreeNode.decEq (DY.Example.MerkleTree.MerkleTreeNode.Leaf a) DY.Example.MerkleTree.MerkleTreeNode.Empty = isFalse ⋯
• DY.Example.MerkleTree.instDecidableEqMerkleTreeNode.decEq (DY.Example.MerkleTree.MerkleTreeNode.Leaf a) (DY.Example.MerkleTree.MerkleTreeNode.Internal a_1 a_2) = isFalse ⋯
• DY.Example.MerkleTree.instDecidableEqMerkleTreeNode.decEq (DY.Example.MerkleTree.MerkleTreeNode.Internal a a_1) DY.Example.MerkleTree.MerkleTreeNode.Empty = isFalse ⋯
• DY.Example.MerkleTree.instDecidableEqMerkleTreeNode.decEq (DY.Example.MerkleTree.MerkleTreeNode.Internal a a_1) (DY.Example.MerkleTree.MerkleTreeNode.Leaf a_2) = isFalse ⋯

@[irreducible]

def DY.Example.MerkleTree.merkleTreeHash {Bytes : Type} [Comparse.BytesLike Bytes] [Hash.CanHash Bytes] {α : Type} (mf : Comparse.ExtensibleMessageFormat Bytes α) (l : List α) : Bytes

Equations

• DY.Example.MerkleTree.merkleTreeHash mf l = DY.Hash.hash ((DY.Example.MerkleTree.MerkleTreeNode.mf✝ mf).serialize (DY.Example.MerkleTree.merkleTreeHashInput✝ mf l))

@[irreducible]

def DY.Example.MerkleTree.mkInclusionProof {Bytes : Type} [Comparse.BytesLike Bytes] [Hash.CanHash Bytes] {α : Type} (mf : Comparse.ExtensibleMessageFormat Bytes α) (l : List α) (i : Nat) (h_i : i < l.length) : List Bytes

Equations

• One or more equations did not get rendered due to their size.
• DY.Example.MerkleTree.mkInclusionProof mf [x] i h_i_2 = []

def DY.Example.MerkleTree.checkInclusionProof {Bytes : Type} [DecidableEq Bytes] [Comparse.BytesLike Bytes] [Hash.CanHash Bytes] {α : Type} (mf : Comparse.ExtensibleMessageFormat Bytes α) (proof : List Bytes) (leaf : α) (i : Nat) (rootHash : Bytes) (length : Nat) : Prop

Equations

• DY.Example.MerkleTree.checkInclusionProof mf proof leaf i rootHash length = (DY.Example.MerkleTree.inclusionProofToRootHash✝ mf proof leaf i length = rootHash ∧ i < length)

@[instance_reducible]

instance DY.Example.MerkleTree.instDecidableCheckInclusionProof {Bytes : Type} [DecidableEq Bytes] [Comparse.BytesLike Bytes] [Hash.CanHash Bytes] {α : Type} (mf : Comparse.ExtensibleMessageFormat Bytes α) (proof : List Bytes) (leaf : α) (i : Nat) (rootHash : Bytes) (length : Nat) : Decidable (checkInclusionProof mf proof leaf i rootHash length)

Equations

• DY.Example.MerkleTree.instDecidableCheckInclusionProof mf proof leaf i rootHash length = DY.Example.MerkleTree.instDecidableCheckInclusionProof._aux_1✝ mf proof leaf i rootHash length

class DY.Example.MerkleTree.HasExecBytes : Type 1

• bytesFunc : BytesFunctor
• bytesFunc0 : BytesFunctor.Has Literal.SubF
• bytesFunc1 : BytesFunctor.Has Concat.SubF
• bytesFunc2 : BytesFunctor.Has Hash.SubF
• bytesFunc3 : BytesFunctor.Has Signature.SubF
• bytesFunc4 : BytesFunctor.Has Random.SubF
• bytesLen : BytesLength
• bytesLen0 : BytesLength.Has Literal.SubF.length
• bytesLen1 : BytesLength.Has Concat.SubF.length
• bytesLen2 : BytesLength.Has Hash.SubF.length
• bytesLen3 : BytesLength.Has Signature.SubF.length
• bytesLen4 : BytesLength.Has Random.SubF.length
• att : AttackerKnowledge
• att0 : AttackerKnowledge.Has Literal.attackerKnowledge
• att1 : AttackerKnowledge.Has Concat.attackerKnowledge
• att2 : AttackerKnowledge.Has Hash.attackerKnowledge
• att3 : AttackerKnowledge.Has Signature.attackerKnowledge
• att4 : AttackerKnowledge.Has Random.attackerKnowledge

structure DY.Example.MerkleTree.SignedRootHashTBS [HasExecBytes] : Type

• rootHash : Bytes
• length : Nat

structure DY.Example.MerkleTree.SignedRootHash [HasExecBytes] : Type

• tbs : SignedRootHashTBS
• sig : Bytes

structure DY.Example.MerkleTree.ElementAndInclusionProof [HasExecBytes] : Type

• element : Bytes
• i : Nat
• inclusionProof : List Bytes

structure DY.Example.MerkleTree.ServerState [HasExecBytes] : Type

• elements : List Bytes

inductive DY.Example.MerkleTree.TheEvent [HasExecBytes] : Type

• ServerAuthenticated [HasExecBytes] (server : Participant) (msg : Bytes) : TheEvent
• ClientAccept [HasExecBytes] (server : Participant) (msg : Bytes) : TheEvent

@[instance_reducible]

instance DY.Example.MerkleTree.instDecidableEqTheEvent {inst✝ : HasExecBytes} : DecidableEq TheEvent

Equations

• DY.Example.MerkleTree.instDecidableEqTheEvent = DY.Example.MerkleTree.instDecidableEqTheEvent.decEq

def DY.Example.MerkleTree.instDecidableEqTheEvent.decEq {inst✝ : HasExecBytes} (x✝ x✝¹ : TheEvent) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• DY.Example.MerkleTree.instDecidableEqTheEvent.decEq (DY.Example.MerkleTree.TheEvent.ServerAuthenticated server msg) (DY.Example.MerkleTree.TheEvent.ClientAccept server_1 msg_1) = isFalse ⋯
• DY.Example.MerkleTree.instDecidableEqTheEvent.decEq (DY.Example.MerkleTree.TheEvent.ClientAccept server msg) (DY.Example.MerkleTree.TheEvent.ServerAuthenticated server_1 msg_1) = isFalse ⋯

@[instance_reducible]

instance DY.Example.MerkleTree.SignedRootHashTBS.ps [HasExecBytes] : Comparse.ParseableSerializeableNE SignedRootHashTBS

Equations

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

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

@[instance_reducible]

instance DY.Example.MerkleTree.SignedRootHash.ps [HasExecBytes] : Comparse.ParseableSerializeableNE SignedRootHash

Equations

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

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

@[instance_reducible]

instance DY.Example.MerkleTree.ElementAndInclusionProof.ps [HasExecBytes] : Comparse.ParseableSerializeable ElementAndInclusionProof

Equations

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

theorem DY.Example.MerkleTree.ElementAndInclusionProof.IsWellFormed_eq [HasExecBytes] {τ : Sort u_1} (pre : Bytes → τ → Prop) [Comparse.BytesCompatibleTracePred pre] (x : ElementAndInclusionProof) (tr : τ) : Comparse.IsWellFormed pre x tr = (pre x.element tr ∧ ∀ (b : Bytes), b ∈ x.inclusionProof → pre b tr)

@[instance_reducible]

instance DY.Example.MerkleTree.ServerState.ps [HasExecBytes] : Comparse.ParseableSerializeable ServerState

Equations

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

theorem DY.Example.MerkleTree.ServerState.IsWellFormed_eq [HasExecBytes] {τ : Sort u_1} (pre : Bytes → τ → Prop) [Comparse.BytesCompatibleTracePred pre] (x : ServerState) (tr : τ) : Comparse.IsWellFormed pre x tr = ∀ (element : Bytes), element ∈ x.elements → pre element tr

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

• bytesFunc : BytesFunctor
• bytesFunc0 : BytesFunctor.Has Literal.SubF
• bytesFunc1 : BytesFunctor.Has Concat.SubF
• bytesFunc2 : BytesFunctor.Has Hash.SubF
• bytesFunc3 : BytesFunctor.Has Signature.SubF
• bytesFunc4 : BytesFunctor.Has Random.SubF
• bytesLen : BytesLength
• bytesLen0 : BytesLength.Has Literal.SubF.length
• bytesLen1 : BytesLength.Has Concat.SubF.length
• bytesLen2 : BytesLength.Has Hash.SubF.length
• bytesLen3 : BytesLength.Has Signature.SubF.length
• bytesLen4 : BytesLength.Has Random.SubF.length
• att : AttackerKnowledge
• att0 : AttackerKnowledge.Has Literal.attackerKnowledge
• att1 : AttackerKnowledge.Has Concat.attackerKnowledge
• att2 : AttackerKnowledge.Has Hash.attackerKnowledge
• att3 : AttackerKnowledge.Has Signature.attackerKnowledge
• att4 : AttackerKnowledge.Has Random.attackerKnowledge
• traceExec : ExecTraceTypes
• traceExec0 : ExecTraceTypes.Has Network.ExecEntryT
• traceExec1 : ExecTraceTypes.Has Random.ExecEntryT
• traceExec2 : ExecTraceTypes.Has (ProtocolEvent.ExecEntryT TheEvent)
• traceExec3 : ExecTraceTypes.Has (LongTermKeys.ExecEntryT "MerkleTree PKI")
• traceExec4 : ExecTraceTypes.Has (PersistentLocalState.CompromisableState.ExecEntryT ServerState)
• attBase : BaseAttackerKnowledge

@[instance_reducible]

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

Equations

• DY.Example.MerkleTree.instExecConfigVkBytes_examples = { }

def DY.Example.MerkleTree.Server.authenticate [HasExecTrace] (server : Participant) (msgHandles : List Nat) (skHandle : Nat) : Traceful (Nat × Nat)

Equations

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

def DY.Example.MerkleTree.Server.proveInclusion [HasExecTrace] (server : Participant) (i stHandle : Nat) : Traceful Nat

Equations

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

def DY.Example.MerkleTree.Client.checkInclusion [HasExecTrace] (server : Participant) (msgSigHandle msgInclHandle pkHandle : Nat) : Traceful Unit

Equations

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

def DY.Example.MerkleTree.ServerState.compromise [HasExecTrace] (stHandle : Nat) : Traceful Nat

Equations

• DY.Example.MerkleTree.ServerState.compromise stHandle = DY.PersistentLocalState.compromise DY.Example.MerkleTree.ServerState stHandle

def DY.Example.MerkleTree.Server.authenticate.reachability [HasExecTrace] : ReachabilityConfig

Equations

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

def DY.Example.MerkleTree.Server.proveInclusion.reachability [HasExecTrace] : ReachabilityConfig

Equations

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

def DY.Example.MerkleTree.Client.checkInclusion.reachability [HasExecTrace] : ReachabilityConfig

Equations

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

def DY.Example.MerkleTree.ServerState.compromise.reachability [HasExecTrace] : ReachabilityConfig

Equations

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

@[instance_reducible]

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

Equations

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

def DY.Example.MerkleTree.reachability.internal [HasExecTrace] : Fin 6 → ReachabilityConfig

Equations

• DY.Example.MerkleTree.reachability.internal 0 = DY.Network.reachability
• DY.Example.MerkleTree.reachability.internal 1 = DY.LongTermKeys.reachability "MerkleTree PKI"
• DY.Example.MerkleTree.reachability.internal 2 = DY.Example.MerkleTree.Server.authenticate.reachability
• DY.Example.MerkleTree.reachability.internal 3 = DY.Example.MerkleTree.Server.proveInclusion.reachability
• DY.Example.MerkleTree.reachability.internal 4 = DY.Example.MerkleTree.Client.checkInclusion.reachability
• DY.Example.MerkleTree.reachability.internal 5 = DY.Example.MerkleTree.ServerState.compromise.reachability
• DY.Example.MerkleTree.reachability.internal ⟨n.succ.succ.succ.succ.succ.succ, isLt⟩ = ⋯.elim