class DY.LongTermKeys.ExecConfig [BytesFunctor] (name : String) (skToPk : outParam (Bytes → Bytes)) : Type

structure DY.LongTermKeys.SecretKeyState [BytesFunctor] (name : String) : Type

• sk : Bytes

theorem DY.LongTermKeys.SecretKeyState.IsWellFormed_eq {τ : Sort u_1} {name : String} [BytesFunctor] [BytesLength] [BytesFunctor.Has Literal.SubF] [BytesLength.Has Literal.SubF.length] [BytesFunctor.Has Concat.SubF] [BytesLength.Has Concat.SubF.length] (pre : Bytes → τ → Prop) [Comparse.BytesCompatibleTracePred pre] (x : SecretKeyState name) (tr : τ) : Comparse.IsWellFormed pre x tr = pre x.sk tr

structure DY.LongTermKeys.PublicKeyState [BytesFunctor] (name : String) : Type

• p : Participant
• pk : Bytes

theorem DY.LongTermKeys.PublicKeyState.IsWellFormed_eq {τ : Sort u_1} {name : String} [BytesFunctor] [BytesLength] [BytesFunctor.Has Literal.SubF] [BytesLength.Has Literal.SubF.length] [BytesFunctor.Has Concat.SubF] [BytesLength.Has Concat.SubF.length] (pre : Bytes → τ → Prop) [Comparse.BytesCompatibleTracePred pre] (x : PublicKeyState name) (tr : τ) : Comparse.IsWellFormed pre x tr = pre x.pk tr

def DY.LongTermKeys.ExecEntryT.internal [BytesFunctor] (name : String) : Fin 2 → Type

Equations

• DY.LongTermKeys.ExecEntryT.internal name 0 = DY.PersistentLocalState.CompromisableState.ExecEntryT (DY.LongTermKeys.SecretKeyState name)
• DY.LongTermKeys.ExecEntryT.internal name 1 = DY.PersistentGlobalState.CompromisableState.ExecEntryT (DY.LongTermKeys.PublicKeyState name)
• DY.LongTermKeys.ExecEntryT.internal name ⟨n.succ.succ, isLt⟩ = ⋯.elim

def DY.LongTermKeys.baseAttackerKnowledge.internal [BytesFunctor] [ExecTraceTypes] [BytesFunctor] (name : String) (id✝ : Fin 2) : SubBaseAttackerKnowledge (ExecEntryT.internal name id✝)

Equations

• DY.LongTermKeys.baseAttackerKnowledge.internal name 0 = DY.PersistentLocalState.CompromisableState.baseAttackerKnowledge (DY.LongTermKeys.SecretKeyState name)
• DY.LongTermKeys.baseAttackerKnowledge.internal name 1 = DY.PersistentGlobalState.CompromisableState.baseAttackerKnowledge (DY.LongTermKeys.PublicKeyState name)
• DY.LongTermKeys.baseAttackerKnowledge.internal name ⟨n.succ.succ, isLt⟩ = ⋯.elim

@[instance_reducible]

def DY.LongTermKeys.ExecEntryT [BytesFunctor] (name : String) : Type

Equations

• DY.LongTermKeys.ExecEntryT name = DY.ExecTraceTypes.combine (DY.LongTermKeys.ExecEntryT.internal name)

@[instance_reducible]

def DY.LongTermKeys.baseAttackerKnowledge [BytesFunctor] [ExecTraceTypes] [BytesFunctor] (name : String) : SubBaseAttackerKnowledge (ExecEntryT name)

Equations

• DY.LongTermKeys.baseAttackerKnowledge name = DY.SubBaseAttackerKnowledge.combine (DY.LongTermKeys.baseAttackerKnowledge.internal name)

def DY.LongTermKeys.generateKeyPair [BytesFunctor] (name : String) {skToPk : Bytes → Bytes} [ExecConfig name skToPk] [ExecTraceTypes] [BytesFunctor.Has Random.SubF] [ExecTraceTypes.Has Random.ExecEntryT] [ExecTraceTypes.Has Network.ExecEntryT] [ExecTraceTypes.Has (ExecEntryT name)] (p : Participant) : Traceful (Nat × Nat × Nat)

Equations

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

def DY.LongTermKeys.getPublicKey [BytesFunctor] (name : String) [ExecTraceTypes] [ExecTraceTypes.Has (ExecEntryT name)] (p : Participant) (pkHandle : Nat) : Traceful Bytes

Equations

• DY.LongTermKeys.getPublicKey name p pkHandle = do let st ← DY.PersistentGlobalState.getGlobalState pkHandle guard (st.p = p) pure st.pk

def DY.LongTermKeys.getPrivateKey [BytesFunctor] (name : String) [ExecTraceTypes] [ExecTraceTypes.Has (ExecEntryT name)] (p : Participant) (skHandle : Nat) : Traceful Bytes

Equations

• DY.LongTermKeys.getPrivateKey name p skHandle = do let st ← DY.PersistentLocalState.getLocalState p skHandle pure st.sk

def DY.LongTermKeys.compromisePrivateKey [BytesFunctor] (name : String) [ExecTraceTypes] [ExecTraceTypes.Has (ExecEntryT name)] [BytesLength] [BytesFunctor.Has Literal.SubF] [BytesLength.Has Literal.SubF.length] [BytesFunctor.Has Concat.SubF] [BytesLength.Has Concat.SubF.length] [ExecTraceTypes.Has Network.ExecEntryT] (skHandle : Nat) : Traceful Nat

Equations

• DY.LongTermKeys.compromisePrivateKey name skHandle = DY.PersistentLocalState.compromise (DY.LongTermKeys.SecretKeyState name) skHandle

def DY.LongTermKeys.LongTermKeyCompromised [BytesFunctor] (name : String) {skToPk : Bytes → Bytes} [ExecConfig name skToPk] [ExecTraceTypes] [ExecTraceTypes.Has (ExecEntryT name)] (participant : Participant) (pk : Bytes) (tr : ExecTrace) : Prop

Equations

• DY.LongTermKeys.LongTermKeyCompromised name participant pk tr = ∃ (sk : DY.Bytes), pk = skToPk sk ∧ DY.PersistentLocalState.LocalStateCompromised participant { sk := sk } tr

theorem DY.LongTermKeys.LongTermKeyCompromised_le [BytesFunctor] (name : String) {skToPk : Bytes → Bytes} [ExecConfig name skToPk] [ExecTraceTypes] [ExecTraceTypes.Has (ExecEntryT name)] (participant : Participant) (pk : Bytes) (tr1 tr2 : ExecTrace) : tr1 ≤ tr2 → LongTermKeyCompromised name participant pk tr1 → LongTermKeyCompromised name participant pk tr2

def DY.LongTermKeys.label [BytesFunctor] (name : String) {skToPk : Bytes → Bytes} [ExecConfig name skToPk] [ExecTraceTypes] [ExecTraceTypes.Has (ExecEntryT name)] (participant : Participant) (pk : Bytes) : Label

Equations

• DY.LongTermKeys.label name participant pk = { isCorrupt := DY.LongTermKeys.LongTermKeyCompromised name participant pk, isCorruptLater := ⋯ }

class DY.LongTermKeys.ProofConfig [BytesFunctor] [ExecTraceTypes] [ProofTraceTypes] [BytesInvariants] (name : String) {skToPk : outParam (Bytes → Bytes)} (usage : outParam (Participant → Usage)) (lab : outParam (Participant → Bytes → Label)) [ExecConfig name skToPk] [ExecTraceTypes.Has (ExecEntryT name)] : Type

• IsLongTermPublicKey : Participant → Bytes → ProofTrace → Prop
• label_canFlow (p : Participant) (b : Bytes) (tr : ExecTrace) : (lab p b).canFlow (label name p b) tr
• IsLongTermPublicKey_le (p : Participant) (b : Bytes) (tr1 tr2 : ProofTrace) : tr1 ≤ tr2 → IsLongTermPublicKey name p b tr1 → IsLongTermPublicKey name p b tr2
• IsLongTermPublicKey_implied (p : Participant) (b : Bytes) (tr : ProofTrace) : b.Invariant tr → b.label tr = lab p (skToPk b) → b.HasUsage (usage p) tr → IsLongTermPublicKey name p (skToPk b) tr
• IsLongTermPublicKey_implies (p : Participant) (b : Bytes) (tr : ProofTrace) : IsLongTermPublicKey name p b tr → b.Publishable tr

theorem DY.LongTermKeys.IsLongTermPublicKey_implies_Invariant [BytesFunctor] [ExecTraceTypes] [ProofTraceTypes] [BytesInvariants] (name : String) {skToPk : Bytes → Bytes} (usage : Participant → Usage) (lab : Participant → Bytes → Label) [ExecTraceTypes.Has (ExecEntryT name)] [ExecConfig name skToPk] [ProofConfig name usage lab] (p : Participant) (b : Bytes) (tr : ProofTrace) : IsLongTermPublicKey name p b tr → b.Invariant tr

def DY.LongTermKeys.IsLongTermSecretKey [BytesFunctor] [ExecTraceTypes] [ProofTraceTypes] [BytesInvariants] (name : String) {skToPk : Bytes → Bytes} {usage : Participant → Usage} {lab : Participant → Bytes → Label} [ExecTraceTypes.Has (ExecEntryT name)] [ExecConfig name skToPk] [ProofConfig name usage lab] (p : Participant) (b : Bytes) (tr : ProofTrace) : Prop

Equations

• DY.LongTermKeys.IsLongTermSecretKey name p b tr = (b.Invariant tr ∧ b.label tr = lab p (skToPk b) ∧ b.HasUsage (usage p) tr)

theorem DY.LongTermKeys.IsLongTermSecretKey_later [BytesFunctor] [ExecTraceTypes] [ProofTraceTypes] [BytesInvariants] [BytesInvariantsProofs] (name : String) {skToPk : Bytes → Bytes} {usage : Participant → Usage} {lab : Participant → Bytes → Label} [ExecTraceTypes.Has (ExecEntryT name)] [ExecConfig name skToPk] [ProofConfig name usage lab] (p : Participant) (b : Bytes) (tr1 tr2 : ProofTrace) : tr1 ≤ tr2 → IsLongTermSecretKey name p b tr1 → IsLongTermSecretKey name p b tr2

@[instance_reducible]

instance DY.LongTermKeys.instCompromisableLocalStateInvSecretKeyState [BytesFunctor] [BytesLength] [ExecTraceTypes] [ProofTraceTypes] [BytesInvariants] [BytesInvariantsProofs] [BytesFunctor.Has Literal.SubF] [BytesLength.Has Literal.SubF.length] [BytesFunctor.Has Concat.SubF] [BytesLength.Has Concat.SubF.length] [BytesInvariants.Has Literal.invariants] [BytesInvariants.Has Concat.invariants] (name : String) [ExecTraceTypes.Has (ExecEntryT name)] {skToPk : Bytes → Bytes} {usage : Participant → Usage} {lab : Participant → Bytes → Label} [ExecConfig name skToPk] [ProofConfig name usage lab] : PersistentLocalState.CompromisableLocalStateInv (SecretKeyState name)

Equations

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

@[instance_reducible]

instance DY.LongTermKeys.instCompromisableGlobalStateInvPublicKeyState [BytesFunctor] [BytesLength] [ExecTraceTypes] [ProofTraceTypes] [BytesInvariants] [BytesFunctor.Has Literal.SubF] [BytesLength.Has Literal.SubF.length] [BytesFunctor.Has Concat.SubF] [BytesLength.Has Concat.SubF.length] [BytesInvariants.Has Literal.invariants] [BytesInvariants.Has Concat.invariants] (name : String) [ExecTraceTypes.Has (ExecEntryT name)] {skToPk : Bytes → Bytes} {usage : Participant → Usage} {lab : Participant → Bytes → Label} [ExecConfig name skToPk] [ProofConfig name usage lab] : PersistentGlobalState.CompromisableGlobalStateInv (PublicKeyState name)

Equations

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

@[instance_reducible]

def DY.LongTermKeys.ProofEntryT [BytesFunctor] (name : String) : Type

Equations

• DY.LongTermKeys.ProofEntryT name = DY.ProofTraceTypes.combine (DY.LongTermKeys.ProofEntryT.internal name)

def DY.LongTermKeys.ProofEntryT.internal [BytesFunctor] (name : String) : Fin 2 → Type

Equations

• DY.LongTermKeys.ProofEntryT.internal name 0 = DY.PersistentLocalState.CompromisableState.ProofEntryT (DY.LongTermKeys.SecretKeyState name)
• DY.LongTermKeys.ProofEntryT.internal name 1 = DY.PersistentGlobalState.CompromisableState.ProofEntryT (DY.LongTermKeys.PublicKeyState name)
• DY.LongTermKeys.ProofEntryT.internal name ⟨n.succ.succ, isLt⟩ = ⋯.elim

instance DY.LongTermKeys.generateKeyPair.proof [BytesFunctor] [ExecTraceTypes] [ProofTraceTypes] [TraceInvariant] [BytesInvariants] [BytesInvariantsProofs] [BytesLength] [BytesFunctor.Has Literal.SubF] [BytesLength.Has Literal.SubF.length] [BytesFunctor.Has Concat.SubF] [BytesLength.Has Concat.SubF.length] [BytesInvariants.Has Literal.invariants] [BytesInvariants.Has Concat.invariants] (name : String) {skToPk : Bytes → Bytes} {usage : Participant → Usage} {lab : Participant → Bytes → Label} [BytesFunctor.Has Random.SubF] [ExecTraceTypes.Has Random.ExecEntryT] [ProofTraceTypes.Has Random.ProofEntryT] [ExecTraceTypes.Has Network.ExecEntryT] [ProofTraceTypes.Has Network.ProofEntryT] [ExecTraceTypes.Has (ExecEntryT name)] [ProofTraceTypes.Has (ProofEntryT name)] [BytesInvariants.Has Random.invariants] [ExecConfig name skToPk] [ProofConfig name usage lab] [TraceInvariant.Has Random.ProofEntryT] [TraceInvariant.Has Network.ProofEntryT] [TraceInvariant.Has (ProofEntryT name)] (p : Participant) : HoareTriple (generateKeyPair name p) (fun (x : ProofTrace) => True) fun (x : Nat × Nat × Nat) (x_1 : ProofTrace) => True

instance DY.LongTermKeys.getPublicKey.proof [BytesFunctor] [ExecTraceTypes] [ProofTraceTypes] [TraceInvariant] [BytesInvariants] [BytesInvariantsProofs] [BytesLength] [BytesFunctor.Has Literal.SubF] [BytesLength.Has Literal.SubF.length] [BytesFunctor.Has Concat.SubF] [BytesLength.Has Concat.SubF.length] [BytesInvariants.Has Literal.invariants] [BytesInvariants.Has Concat.invariants] (name : String) {skToPk : Bytes → Bytes} {usage : Participant → Usage} {lab : Participant → Bytes → Label} [BytesFunctor.Has Random.SubF] [ExecTraceTypes.Has (ExecEntryT name)] [ProofTraceTypes.Has (ProofEntryT name)] [ExecConfig name skToPk] [ProofConfig name usage lab] [TraceInvariant.Has (ProofEntryT name)] (p : Participant) (pkHandle : Nat) : HoareTriple (getPublicKey name p pkHandle) (fun (x : ProofTrace) => True) fun (res : Bytes) (tr : ProofTrace) => IsLongTermPublicKey name p res tr

instance DY.LongTermKeys.getPrivateKey.proof [BytesFunctor] [ExecTraceTypes] [ProofTraceTypes] [TraceInvariant] [BytesInvariants] [BytesInvariantsProofs] [BytesLength] [BytesFunctor.Has Literal.SubF] [BytesLength.Has Literal.SubF.length] [BytesFunctor.Has Concat.SubF] [BytesLength.Has Concat.SubF.length] [BytesInvariants.Has Literal.invariants] [BytesInvariants.Has Concat.invariants] (name : String) {skToPk : Bytes → Bytes} {usage : Participant → Usage} {lab : Participant → Bytes → Label} [BytesFunctor.Has Random.SubF] [ExecTraceTypes.Has (ExecEntryT name)] [ProofTraceTypes.Has (ProofEntryT name)] [ExecConfig name skToPk] [ProofConfig name usage lab] [TraceInvariant.Has (ProofEntryT name)] (p : Participant) (skHandle : Nat) : HoareTriple (getPrivateKey name p skHandle) (fun (x : ProofTrace) => True) fun (res : Bytes) (tr : ProofTrace) => IsLongTermSecretKey name p res tr

instance DY.LongTermKeys.compromisePrivateKey.proof [BytesFunctor] [ExecTraceTypes] [ProofTraceTypes] [TraceInvariant] [BytesInvariants] [BytesInvariantsProofs] [BytesLength] [BytesFunctor.Has Literal.SubF] [BytesLength.Has Literal.SubF.length] [BytesFunctor.Has Concat.SubF] [BytesLength.Has Concat.SubF.length] [BytesInvariants.Has Literal.invariants] [BytesInvariants.Has Concat.invariants] (name : String) {skToPk : Bytes → Bytes} {usage : Participant → Usage} {lab : Participant → Bytes → Label} [BytesFunctor.Has Random.SubF] [ExecTraceTypes.Has (ExecEntryT name)] [ProofTraceTypes.Has (ProofEntryT name)] [ExecConfig name skToPk] [ProofConfig name usage lab] [TraceInvariant.Has (ProofEntryT name)] [ExecTraceTypes.Has Network.ExecEntryT] [ProofTraceTypes.Has Network.ProofEntryT] [TraceInvariant.Has Network.ProofEntryT] (skHandle : Nat) : HoareTriple (compromisePrivateKey name skHandle) (fun (x : ProofTrace) => True) fun (x : Nat) (x_1 : ProofTrace) => True

def DY.LongTermKeys.generateKeyPair.reachability [BytesFunctor] (name : String) {skToPk : Bytes → Bytes} [ExecConfig name skToPk] [ExecTraceTypes] [BytesFunctor.Has Random.SubF] [ExecTraceTypes.Has Random.ExecEntryT] [ExecTraceTypes.Has Network.ExecEntryT] [ExecTraceTypes.Has (ExecEntryT name)] : ReachabilityConfig

Equations

• DY.LongTermKeys.generateKeyPair.reachability name = DY.ReachabilityConfig.make fun (p : DY.Participant) => DY.LongTermKeys.generateKeyPair name p

def DY.LongTermKeys.compromisePrivateKey.reachability [BytesFunctor] (name : String) [ExecTraceTypes] [ExecTraceTypes.Has Network.ExecEntryT] [ExecTraceTypes.Has (ExecEntryT name)] [BytesLength] [BytesFunctor.Has Literal.SubF] [BytesLength.Has Literal.SubF.length] [BytesFunctor.Has Concat.SubF] [BytesLength.Has Concat.SubF.length] : ReachabilityConfig

Equations

• DY.LongTermKeys.compromisePrivateKey.reachability name = DY.ReachabilityConfig.make fun (skHandle : Nat) => DY.LongTermKeys.compromisePrivateKey name skHandle

def DY.LongTermKeys.reachability.internal [BytesFunctor] (name : String) {skToPk : Bytes → Bytes} [ExecConfig name skToPk] [ExecTraceTypes] [BytesFunctor.Has Random.SubF] [ExecTraceTypes.Has Random.ExecEntryT] [ExecTraceTypes.Has Network.ExecEntryT] [ExecTraceTypes.Has (ExecEntryT name)] [BytesLength] [BytesFunctor.Has Literal.SubF] [BytesLength.Has Literal.SubF.length] [BytesFunctor.Has Concat.SubF] [BytesLength.Has Concat.SubF.length] : Fin 2 → ReachabilityConfig

Equations

• DY.LongTermKeys.reachability.internal name 0 = DY.LongTermKeys.generateKeyPair.reachability name
• DY.LongTermKeys.reachability.internal name 1 = DY.LongTermKeys.compromisePrivateKey.reachability name

def DY.LongTermKeys.reachability [BytesFunctor] (name : String) {skToPk : Bytes → Bytes} [ExecConfig name skToPk] [ExecTraceTypes] [BytesFunctor.Has Random.SubF] [ExecTraceTypes.Has Random.ExecEntryT] [ExecTraceTypes.Has Network.ExecEntryT] [ExecTraceTypes.Has (ExecEntryT name)] [BytesLength] [BytesFunctor.Has Literal.SubF] [BytesLength.Has Literal.SubF.length] [BytesFunctor.Has Concat.SubF] [BytesLength.Has Concat.SubF.length] : ReachabilityConfig

Equations

• DY.LongTermKeys.reachability name = DY.ReachabilityConfig.combine (DY.LongTermKeys.reachability.internal name)

@[instance_reducible]

instance DY.LongTermKeys.instHasStepReachabilityReachability [BytesFunctor] (name : String) {skToPk : Bytes → Bytes} [ExecConfig name skToPk] [ExecTraceTypes] [BytesFunctor.Has Random.SubF] [ExecTraceTypes.Has Random.ExecEntryT] [ExecTraceTypes.Has Network.ExecEntryT] [ExecTraceTypes.Has (ExecEntryT name)] [BytesLength] [BytesFunctor.Has Literal.SubF] [BytesLength.Has Literal.SubF.length] [BytesFunctor.Has Concat.SubF] [BytesLength.Has Concat.SubF.length] : (generateKeyPair.reachability name).HasStep (reachability name)

Equations

• DY.LongTermKeys.instHasStepReachabilityReachability name = { inj := DY.LongTermKeys.instHasStepReachabilityReachability._aux_1 name, pf_pre := ⋯, pf_step := ⋯ }

@[instance_reducible]

instance DY.LongTermKeys.instHasStepReachabilityReachability_1 [BytesFunctor] (name : String) {skToPk : Bytes → Bytes} [ExecConfig name skToPk] [ExecTraceTypes] [BytesFunctor.Has Random.SubF] [ExecTraceTypes.Has Random.ExecEntryT] [ExecTraceTypes.Has Network.ExecEntryT] [ExecTraceTypes.Has (ExecEntryT name)] [BytesLength] [BytesFunctor.Has Literal.SubF] [BytesLength.Has Literal.SubF.length] [BytesFunctor.Has Concat.SubF] [BytesLength.Has Concat.SubF.length] : (compromisePrivateKey.reachability name).HasStep (reachability name)

Equations

• DY.LongTermKeys.instHasStepReachabilityReachability_1 name = { inj := DY.LongTermKeys.instHasStepReachabilityReachability_1._aux_1 name, pf_pre := ⋯, pf_step := ⋯ }

instance DY.LongTermKeys.instReachableImpliesInvariantReachability [BytesFunctor] (name : String) {skToPk : Bytes → Bytes} [ExecConfig name skToPk] [ExecTraceTypes] [BytesFunctor.Has Random.SubF] [ExecTraceTypes.Has Random.ExecEntryT] [ExecTraceTypes.Has Network.ExecEntryT] [ExecTraceTypes.Has (ExecEntryT name)] [ProofTraceTypes] [TraceInvariant] [BytesInvariants] [BytesInvariantsProofs] [BytesLength] [BytesFunctor.Has Literal.SubF] [BytesLength.Has Literal.SubF.length] [BytesFunctor.Has Concat.SubF] [BytesLength.Has Concat.SubF.length] [BytesInvariants.Has Literal.invariants] [BytesInvariants.Has Concat.invariants] {usage : Participant → Usage} {lab : Participant → Bytes → Label} [ProofTraceTypes.Has Random.ProofEntryT] [ProofTraceTypes.Has Network.ProofEntryT] [ProofTraceTypes.Has (ProofEntryT name)] [BytesInvariants.Has Random.invariants] [ProofConfig name usage lab] [TraceInvariant.Has Random.ProofEntryT] [TraceInvariant.Has Network.ProofEntryT] [TraceInvariant.Has (ProofEntryT name)] : ReachableImpliesInvariant (generateKeyPair.reachability name)

instance DY.LongTermKeys.instReachableImpliesInvariantReachability_1 [BytesFunctor] (name : String) {skToPk : Bytes → Bytes} [ExecConfig name skToPk] [ExecTraceTypes] [BytesFunctor.Has Random.SubF] [ExecTraceTypes.Has Network.ExecEntryT] [ExecTraceTypes.Has (ExecEntryT name)] [ProofTraceTypes] [TraceInvariant] [BytesInvariants] [BytesInvariantsProofs] [BytesLength] [BytesFunctor.Has Literal.SubF] [BytesLength.Has Literal.SubF.length] [BytesFunctor.Has Concat.SubF] [BytesLength.Has Concat.SubF.length] [BytesInvariants.Has Literal.invariants] [BytesInvariants.Has Concat.invariants] {usage : Participant → Usage} {lab : Participant → Bytes → Label} [ProofTraceTypes.Has Network.ProofEntryT] [ProofTraceTypes.Has (ProofEntryT name)] [ProofConfig name usage lab] [TraceInvariant.Has Network.ProofEntryT] [TraceInvariant.Has (ProofEntryT name)] : ReachableImpliesInvariant (compromisePrivateKey.reachability name)

instance DY.LongTermKeys.instReachableImpliesInvariantInternal [BytesFunctor] (name : String) {skToPk : Bytes → Bytes} [ExecConfig name skToPk] [ExecTraceTypes] [BytesFunctor.Has Random.SubF] [ExecTraceTypes.Has Random.ExecEntryT] [ExecTraceTypes.Has Network.ExecEntryT] [ExecTraceTypes.Has (ExecEntryT name)] [ProofTraceTypes] [TraceInvariant] [BytesInvariants] [BytesInvariantsProofs] [BytesLength] [BytesFunctor.Has Literal.SubF] [BytesLength.Has Literal.SubF.length] [BytesFunctor.Has Concat.SubF] [BytesLength.Has Concat.SubF.length] [BytesInvariants.Has Literal.invariants] [BytesInvariants.Has Concat.invariants] {usage : Participant → Usage} {lab : Participant → Bytes → Label} [ProofTraceTypes.Has Random.ProofEntryT] [ProofTraceTypes.Has Network.ProofEntryT] [ProofTraceTypes.Has (ProofEntryT name)] [BytesInvariants.Has Random.invariants] [ProofConfig name usage lab] [TraceInvariant.Has Random.ProofEntryT] [TraceInvariant.Has Network.ProofEntryT] [TraceInvariant.Has (ProofEntryT name)] (id : Fin 2) : ReachableImpliesInvariant (reachability.internal name id)

instance DY.LongTermKeys.instReachableImpliesInvariantReachability_2 [BytesFunctor] (name : String) {skToPk : Bytes → Bytes} [ExecConfig name skToPk] [ExecTraceTypes] [BytesFunctor.Has Random.SubF] [ExecTraceTypes.Has Random.ExecEntryT] [ExecTraceTypes.Has Network.ExecEntryT] [ExecTraceTypes.Has (ExecEntryT name)] [ProofTraceTypes] [TraceInvariant] [BytesInvariants] [BytesInvariantsProofs] [BytesLength] [BytesFunctor.Has Literal.SubF] [BytesLength.Has Literal.SubF.length] [BytesFunctor.Has Concat.SubF] [BytesLength.Has Concat.SubF.length] [BytesInvariants.Has Literal.invariants] [BytesInvariants.Has Concat.invariants] {usage : Participant → Usage} {lab : Participant → Bytes → Label} [ProofTraceTypes.Has Random.ProofEntryT] [ProofTraceTypes.Has Network.ProofEntryT] [ProofTraceTypes.Has (ProofEntryT name)] [BytesInvariants.Has Random.invariants] [ProofConfig name usage lab] [TraceInvariant.Has Random.ProofEntryT] [TraceInvariant.Has Network.ProofEntryT] [TraceInvariant.Has (ProofEntryT name)] : ReachableImpliesInvariant (reachability name)