class DY.Example.Ratchet.HasExecBytes : Type 1

• bytesFunc : BytesFunctor
• bytesFunc0 : BytesFunctor.Has Random.SubF
• bytesFunc1 : BytesFunctor.Has Literal.SubF
• bytesFunc2 : BytesFunctor.Has Concat.SubF
• bytesFunc3 : BytesFunctor.Has Hash.SubF
• bytesFunc4 : BytesFunctor.Has Signature.SubF
• bytesFunc5 : BytesFunctor.Has DiffieHellman.SubF
• bytesFunc6 : BytesFunctor.Has KdfExtract.SubF
• bytesFunc7 : BytesFunctor.Has KdfExpand.SubF
• bytesLen : BytesLength
• bytesLen0 : BytesLength.Has Random.SubF.length
• bytesLen1 : BytesLength.Has Literal.SubF.length
• bytesLen2 : BytesLength.Has Concat.SubF.length
• bytesLen3 : BytesLength.Has Hash.SubF.length
• bytesLen4 : BytesLength.Has Signature.SubF.length
• bytesLen5 : BytesLength.Has DiffieHellman.SubF.length
• bytesLen6 : BytesLength.Has KdfExtract.SubF.length
• bytesLen7 : BytesLength.Has KdfExpand.SubF.length
• att : AttackerKnowledge
• att0 : AttackerKnowledge.Has Random.attackerKnowledge
• att1 : AttackerKnowledge.Has Literal.attackerKnowledge
• att2 : AttackerKnowledge.Has Concat.attackerKnowledge
• att3 : AttackerKnowledge.Has Hash.attackerKnowledge
• att4 : AttackerKnowledge.Has Signature.attackerKnowledge
• att5 : AttackerKnowledge.Has DiffieHellman.attackerKnowledge
• att6 : AttackerKnowledge.Has KdfExtract.attackerKnowledge
• att7 : AttackerKnowledge.Has KdfExpand.attackerKnowledge

structure DY.Example.Ratchet.Message [HasExecBytes] : Type

• dhPk : Bytes
• sig : Bytes

structure DY.Example.Ratchet.TranscriptElement [HasExecBytes] : Type

• recipient : Participant
• dhPk : Bytes

def DY.Example.Ratchet.instDecidableEqTranscriptElement.decEq {inst✝ : HasExecBytes} (x✝ x✝¹ : TranscriptElement) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance DY.Example.Ratchet.instDecidableEqTranscriptElement {inst✝ : HasExecBytes} : DecidableEq TranscriptElement

Equations

• DY.Example.Ratchet.instDecidableEqTranscriptElement = DY.Example.Ratchet.instDecidableEqTranscriptElement.decEq

@[reducible, inline]

abbrev DY.Example.Ratchet.Transcript [HasExecBytes] : Type

Equations

• DY.Example.Ratchet.Transcript = List DY.Example.Ratchet.TranscriptElement

structure DY.Example.Ratchet.TranscriptHashInput [HasExecBytes] : Type

• elem : TranscriptElement
• previousTranscriptHash : Bytes

structure DY.Example.Ratchet.SigInput [HasExecBytes] : Type

• transcriptHash : Bytes

structure DY.Example.Ratchet.StateMyTurn [HasExecBytes] : Type

• transcript : Transcript
• recipient : Participant
• transcriptHash : Bytes
• otherDhPk : Bytes
• k : Bytes

structure DY.Example.Ratchet.StateOtherTurn [HasExecBytes] : Type

• transcript : Transcript
• recipient : Participant
• transcriptHash : Bytes
• myDhSk : Bytes
• k : Bytes

inductive DY.Example.Ratchet.RatchetEvent [HasExecBytes] : Type

• SendUpdate [HasExecBytes] (me other : Participant) (transcript : Transcript) (k : Bytes) : RatchetEvent
• ReceiveUpdate [HasExecBytes] (me other : Participant) (transcript : Transcript) (k : Bytes) : RatchetEvent

def DY.Example.Ratchet.instDecidableEqRatchetEvent.decEq {inst✝ : HasExecBytes} (x✝ x✝¹ : RatchetEvent) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance DY.Example.Ratchet.instDecidableEqRatchetEvent {inst✝ : HasExecBytes} : DecidableEq RatchetEvent

Equations

• DY.Example.Ratchet.instDecidableEqRatchetEvent = DY.Example.Ratchet.instDecidableEqRatchetEvent.decEq

@[instance_reducible]

instance DY.Example.Ratchet.instParseableSerializeableMessage [HasExecBytes] : Comparse.ParseableSerializeable Message

Equations

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

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

@[instance_reducible]

instance DY.Example.Ratchet.TranscriptElement.ps [HasExecBytes] : Comparse.ParseableSerializeableNE TranscriptElement

Equations

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

instance DY.Example.Ratchet.instParseConsumesBytesTranscriptElementMf [HasExecBytes] : Comparse.ParseableSerializeableNE.mf.ParseConsumes

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

@[instance_reducible]

instance DY.Example.Ratchet.instParseableSerializeableTranscriptHashInput [HasExecBytes] : Comparse.ParseableSerializeable TranscriptHashInput

Equations

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

theorem DY.Example.Ratchet.TranscriptHashInput.IsWellFormed_eq [HasExecBytes] {τ : Sort u_1} (pre : Bytes → τ → Prop) [Comparse.BytesCompatibleTracePred pre] (x : TranscriptHashInput) (tr : τ) : Comparse.IsWellFormed pre x tr = (Comparse.IsWellFormed pre x.elem tr ∧ pre x.previousTranscriptHash tr)

@[instance_reducible]

instance DY.Example.Ratchet.instParseableSerializeableSigInput [HasExecBytes] : Comparse.ParseableSerializeable SigInput

Equations

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

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

@[instance_reducible]

instance DY.Example.Ratchet.instParseableSerializeableStateMyTurn [HasExecBytes] : Comparse.ParseableSerializeable StateMyTurn

Equations

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

theorem DY.Example.Ratchet.StateMyTurn.IsWellFormed_eq [HasExecBytes] {τ : Sort u_1} (pre : Bytes → τ → Prop) [Comparse.BytesCompatibleTracePred pre] (x : StateMyTurn) (tr : τ) : Comparse.IsWellFormed pre x tr = ((∀ (elem : TranscriptElement), elem ∈ x.transcript → Comparse.IsWellFormed pre elem tr) ∧ pre x.transcriptHash tr ∧ pre x.otherDhPk tr ∧ pre x.k tr)

@[instance_reducible]

instance DY.Example.Ratchet.instParseableSerializeableStateOtherTurn [HasExecBytes] : Comparse.ParseableSerializeable StateOtherTurn

Equations

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

theorem DY.Example.Ratchet.StateOtherTurn.IsWellFormed_eq [HasExecBytes] {τ : Sort u_1} (pre : Bytes → τ → Prop) [Comparse.BytesCompatibleTracePred pre] (x : StateOtherTurn) (tr : τ) : Comparse.IsWellFormed pre x tr = ((∀ (elem : TranscriptElement), elem ∈ x.transcript → Comparse.IsWellFormed pre elem tr) ∧ pre x.transcriptHash tr ∧ pre x.myDhSk tr ∧ pre x.k tr)

class DY.Example.Ratchet.HasExecTrace extends DY.Example.Ratchet.HasExecBytes : Type 1

• bytesFunc : BytesFunctor
• bytesFunc0 : BytesFunctor.Has Random.SubF
• bytesFunc1 : BytesFunctor.Has Literal.SubF
• bytesFunc2 : BytesFunctor.Has Concat.SubF
• bytesFunc3 : BytesFunctor.Has Hash.SubF
• bytesFunc4 : BytesFunctor.Has Signature.SubF
• bytesFunc5 : BytesFunctor.Has DiffieHellman.SubF
• bytesFunc6 : BytesFunctor.Has KdfExtract.SubF
• bytesFunc7 : BytesFunctor.Has KdfExpand.SubF
• bytesLen : BytesLength
• bytesLen0 : BytesLength.Has Random.SubF.length
• bytesLen1 : BytesLength.Has Literal.SubF.length
• bytesLen2 : BytesLength.Has Concat.SubF.length
• bytesLen3 : BytesLength.Has Hash.SubF.length
• bytesLen4 : BytesLength.Has Signature.SubF.length
• bytesLen5 : BytesLength.Has DiffieHellman.SubF.length
• bytesLen6 : BytesLength.Has KdfExtract.SubF.length
• bytesLen7 : BytesLength.Has KdfExpand.SubF.length
• att : AttackerKnowledge
• att0 : AttackerKnowledge.Has Random.attackerKnowledge
• att1 : AttackerKnowledge.Has Literal.attackerKnowledge
• att2 : AttackerKnowledge.Has Concat.attackerKnowledge
• att3 : AttackerKnowledge.Has Hash.attackerKnowledge
• att4 : AttackerKnowledge.Has Signature.attackerKnowledge
• att5 : AttackerKnowledge.Has DiffieHellman.attackerKnowledge
• att6 : AttackerKnowledge.Has KdfExtract.attackerKnowledge
• att7 : AttackerKnowledge.Has KdfExpand.attackerKnowledge
• traceExec : ExecTraceTypes
• traceExec0 : ExecTraceTypes.Has Network.ExecEntryT
• traceExec1 : ExecTraceTypes.Has Random.ExecEntryT
• traceExec2 : ExecTraceTypes.Has (ProtocolEvent.ExecEntryT RatchetEvent)
• traceExec3 : ExecTraceTypes.Has (PersistentLocalState.CompromisableState.ExecEntryT StateMyTurn)
• traceExec4 : ExecTraceTypes.Has (PersistentLocalState.CompromisableState.ExecEntryT StateOtherTurn)
• traceExec5 : ExecTraceTypes.Has (LongTermKeys.ExecEntryT "Ratchet PKI")
• attBase : BaseAttackerKnowledge

def DY.Example.Ratchet.initialTranscriptHash [HasExecTrace] : Bytes

Equations

• DY.Example.Ratchet.initialTranscriptHash = Comparse.BytesLike.empty

def DY.Example.Ratchet.computeTranscriptHash [HasExecTrace] (previousTranscriptHash : Bytes) (elem : TranscriptElement) : Bytes

Equations

• DY.Example.Ratchet.computeTranscriptHash previousTranscriptHash elem = DY.Hash.hash (DY.Comparse.serialize { elem := elem, previousTranscriptHash := previousTranscriptHash })

def DY.Example.Ratchet.firstKey [HasExecTrace] : Bytes

Equations

• DY.Example.Ratchet.firstKey = DY.Literal.literalToBytes "00000000000000000000000000000000".toByteArray

@[instance_reducible]

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

Equations

• DY.Example.Ratchet.instExecConfigVkBytes_examples = { }

def DY.Example.Ratchet.initiate [HasExecTrace] (me other : Participant) (mySigKeyHandle : Nat) : Traceful (Nat × Nat)

Equations

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

def DY.Example.Ratchet.processInitiate [HasExecTrace] (me other : Participant) (otherVerifKeyHandle msgHandle : Nat) : Traceful Nat

Equations

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

def DY.Example.Ratchet.sendUpdate [HasExecTrace] (me : Participant) (mySigKeyHandle stHandle : Nat) : Traceful (Nat × Nat)

Equations

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

def DY.Example.Ratchet.processUpdate [HasExecTrace] (me : Participant) (otherVerifKeyHandle stHandle msgHandle : Nat) : Traceful Nat

Equations

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

def DY.Example.Ratchet.StateMyTurn.compromise [HasExecTrace] (stHandle : Nat) : Traceful Nat

Equations

• DY.Example.Ratchet.StateMyTurn.compromise stHandle = DY.PersistentLocalState.compromise DY.Example.Ratchet.StateMyTurn stHandle

def DY.Example.Ratchet.StateOtherTurn.compromise [HasExecTrace] (stHandle : Nat) : Traceful Nat

Equations

• DY.Example.Ratchet.StateOtherTurn.compromise stHandle = DY.PersistentLocalState.compromise DY.Example.Ratchet.StateOtherTurn stHandle

def DY.Example.Ratchet.StateCompromised [HasExecTrace] (me : Participant) (transcript : Transcript) (tr : ExecTrace) : Prop

Equations

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

theorem DY.Example.Ratchet.StateCompromised_le [HasExecTrace] (me : Participant) (transcript : Transcript) (tr1 tr2 : ExecTrace) : tr1 ≤ tr2 → StateCompromised me transcript tr1 → StateCompromised me transcript tr2

def DY.Example.Ratchet.initiate.reachability [HasExecTrace] : ReachabilityConfig

Equations

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

def DY.Example.Ratchet.processInitiate.reachability [HasExecTrace] : ReachabilityConfig

Equations

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

def DY.Example.Ratchet.sendUpdate.reachability [HasExecTrace] : ReachabilityConfig

Equations

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

def DY.Example.Ratchet.processUpdate.reachability [HasExecTrace] : ReachabilityConfig

Equations

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

def DY.Example.Ratchet.StateMyTurn.compromise.reachability [HasExecTrace] : ReachabilityConfig

Equations

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

def DY.Example.Ratchet.StateOtherTurn.compromise.reachability [HasExecTrace] : ReachabilityConfig

Equations

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

def DY.Example.Ratchet.reachability.internal [HasExecTrace] : Fin 8 → ReachabilityConfig

Equations

• DY.Example.Ratchet.reachability.internal 0 = DY.Network.reachability
• DY.Example.Ratchet.reachability.internal 1 = DY.LongTermKeys.reachability "Ratchet PKI"
• DY.Example.Ratchet.reachability.internal 2 = DY.Example.Ratchet.initiate.reachability
• DY.Example.Ratchet.reachability.internal 3 = DY.Example.Ratchet.processInitiate.reachability
• DY.Example.Ratchet.reachability.internal 4 = DY.Example.Ratchet.sendUpdate.reachability
• DY.Example.Ratchet.reachability.internal 5 = DY.Example.Ratchet.processUpdate.reachability
• DY.Example.Ratchet.reachability.internal 6 = DY.Example.Ratchet.StateMyTurn.compromise.reachability
• DY.Example.Ratchet.reachability.internal 7 = DY.Example.Ratchet.StateOtherTurn.compromise.reachability
• DY.Example.Ratchet.reachability.internal ⟨n.succ.succ.succ.succ.succ.succ.succ.succ, isLt⟩ = ⋯.elim

@[instance_reducible]

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

Equations

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