class DY.Signature'.CanSign (Bytes : Type u) : Type u

• vk (sk : Bytes) : Bytes
• sign (sk nonce msg : Bytes) : Bytes
• verify (vk msg sig : Bytes) : Bool

structure DY.Signature'.Vk.SubF (Bytes : Type) : Type

• sk : Bytes

@[instance_reducible]

instance DY.Signature'.Vk.instFunctorSizeOfSubF : ALaCarte.FunctorSizeOf SubF

Equations

• DY.Signature'.Vk.instFunctorSizeOfSubF = { sizeOf := fun {t : Type} [SizeOf t] (x : DY.Signature'.Vk.SubF t) => match x with | { sk := sk } => sizeOf sk }

@[instance_reducible]

instance DY.Signature'.Vk.instRepresentableSubF : ALaCarte.Representable SubF

Equations

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

@[instance_reducible]

instance DY.Signature'.Vk.instRepresentableDecidableEqSubF : ALaCarte.RepresentableDecidableEq SubF

Equations

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

@[instance_reducible]

instance DY.Signature'.Vk.instRepresentableOrdSubF : ALaCarte.RepresentableOrd SubF

Equations

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

@[instance_reducible]

instance DY.Signature'.Vk.instSubBytesFunctorSubF : SubBytesFunctor SubF

Equations

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

def DY.Signature'.Vk.SubF.length [BytesFunctor] : Bytes.PartialLength SubF

Equations

• x✝¹.length x✝ = 32

structure DY.Signature'.Sign.SubF (Bytes : Type) : Type

• sk : Bytes
• nonce : Bytes
• msg : Bytes

@[instance_reducible]

instance DY.Signature'.Sign.instFunctorSizeOfSubF : ALaCarte.FunctorSizeOf SubF

Equations

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

@[instance_reducible]

instance DY.Signature'.Sign.instRepresentableSubF : ALaCarte.Representable SubF

Equations

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

@[instance_reducible]

instance DY.Signature'.Sign.instRepresentableDecidableEqSubF : ALaCarte.RepresentableDecidableEq SubF

Equations

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

@[instance_reducible]

instance DY.Signature'.Sign.instRepresentableOrdSubF : ALaCarte.RepresentableOrd SubF

Equations

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

@[instance_reducible]

instance DY.Signature'.Sign.instSubBytesFunctorSubF : SubBytesFunctor SubF

Equations

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

def DY.Signature'.Sign.SubF.length [BytesFunctor] : Bytes.PartialLength SubF

Equations

• x✝¹.length x✝ = 64

def DY.Signature'.SubF.length.internal [BytesFunctor] (id✝ : Fin 2) : Bytes.PartialLength (SubF.internal id✝)

Equations

• DY.Signature'.SubF.length.internal 0 = DY.Signature'.Vk.SubF.length
• DY.Signature'.SubF.length.internal 1 = DY.Signature'.Sign.SubF.length
• DY.Signature'.SubF.length.internal ⟨n.succ.succ, isLt⟩ = ⋯.elim

@[instance_reducible]

def DY.Signature'.SubF : Type → Type

Equations

• DY.Signature'.SubF = DY.BytesFunctor.combine DY.Signature'.SubF.internal

@[instance_reducible]

def DY.Signature'.SubF.length [BytesFunctor] : Bytes.PartialLength SubF

Equations

• DY.Signature'.SubF.length = DY.Bytes.PartialLength.combine DY.Signature'.SubF.length.internal

def DY.Signature'.SubF.internal : Fin 2 → Type → Type

Equations

• DY.Signature'.SubF.internal 0 = DY.Signature'.Vk.SubF
• DY.Signature'.SubF.internal 1 = DY.Signature'.Sign.SubF
• DY.Signature'.SubF.internal ⟨n.succ.succ, isLt⟩ = ⋯.elim

@[reducible, inline]

abbrev DY.Signature'.Vk.SubF.pack [BytesFunctor] [BytesFunctor.Has SubF] (x : SubF Bytes) : Bytes

Equations

• x.pack = DY.BytesView.pack x

@[reducible, inline]

abbrev DY.Signature'.Sign.SubF.pack [BytesFunctor] [BytesFunctor.Has SubF] (x : SubF Bytes) : Bytes

Equations

• x.pack = DY.BytesView.pack x

@[instance_reducible]

instance DY.Signature'.instCanSignBytes [BytesFunctor] [BytesFunctor.Has SubF] : CanSign Bytes

Equations

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

theorem DY.Signature'.verify_sign [BytesFunctor] [BytesFunctor.Has SubF] (sk nonce msg : Bytes) : verify (vk sk) msg (sign sk nonce msg) = true

def DY.Signature'.vk.attackerKnowledge [BytesFunctor] [BytesFunctor.Has SubF] : SubAttackerKnowledge SubF

Equations

• DY.Signature'.vk.attackerKnowledge = { pred := fun (p : DY.Bytes → Prop) (out : DY.Bytes) => ∃ (sk : DY.Bytes), out = DY.Signature'.vk sk ∧ p sk, pred_isScottContinuous := ⋯ }

def DY.Signature'.sign.attackerKnowledge [BytesFunctor] [BytesFunctor.Has SubF] : SubAttackerKnowledge SubF

Equations

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

@[instance_reducible]

def DY.Signature'.attackerKnowledge [BytesFunctor] [BytesFunctor.Has SubF] : SubAttackerKnowledge SubF

Equations

• DY.Signature'.attackerKnowledge = DY.SubAttackerKnowledge.combine' DY.Signature'.attackerKnowledge.internal

def DY.Signature'.attackerKnowledge.internal [BytesFunctor] [BytesFunctor.Has SubF] : Fin 2 → SubAttackerKnowledge SubF

Equations

• DY.Signature'.attackerKnowledge.internal 0 = DY.Signature'.vk.attackerKnowledge
• DY.Signature'.attackerKnowledge.internal 1 = DY.Signature'.sign.attackerKnowledge
• DY.Signature'.attackerKnowledge.internal ⟨n.succ.succ, isLt⟩ = ⋯.elim

theorem DY.Signature'.attacker_knows_vk [BytesFunctor] [BytesFunctor.Has SubF] [ExecTraceTypes] [BaseAttackerKnowledge] [AttackerKnowledge] [AttackerKnowledge.Has attackerKnowledge] (sk : Bytes) (tr : ExecTrace) : sk.AttackerKnows tr → (vk sk).AttackerKnows tr

theorem DY.Signature'.attacker_knows_sign [BytesFunctor] [BytesFunctor.Has SubF] [ExecTraceTypes] [BaseAttackerKnowledge] [AttackerKnowledge] [AttackerKnowledge.Has attackerKnowledge] (sk nonce msg : Bytes) (tr : ExecTrace) : sk.AttackerKnows tr → nonce.AttackerKnows tr → msg.AttackerKnows tr → (sign sk nonce msg).AttackerKnows tr

def DY.Signature'.Broken.vkInvert [BytesFunctor] [BytesFunctor.Has SubF] (pk : Bytes) : Err Bytes

Equations

• DY.Signature'.Broken.vkInvert pk = match pk.view? DY.Signature'.Vk.SubF with | some { sk := sk } => some sk | none => none

theorem DY.Signature'.Broken.vkInvert_vk [BytesFunctor] [BytesFunctor.Has SubF] (sk : Bytes) : vkInvert (vk sk) = some sk

theorem DY.Signature'.Broken.vk_vkInvert [BytesFunctor] [BytesFunctor.Has SubF] (pk : Bytes) : match vkInvert pk with | none => True | some sk => vk sk = pk

structure DY.Signature'.Broken.BrokenDhEvent [BytesFunctor] : Type

• brokenPk : Bytes

@[instance_reducible]

def DY.Signature'.Broken.ExecEntryT [BytesFunctor] : Type

Equations

• DY.Signature'.Broken.ExecEntryT = DY.ExecTraceTypes.combine DY.Signature'.Broken.ExecEntryT.internal

def DY.Signature'.Broken.baseAttackerKnowledge.internal [BytesFunctor] [ExecTraceTypes] (id✝ : Fin 1) : SubBaseAttackerKnowledge (ExecEntryT.internal id✝)

Equations

• DY.Signature'.Broken.baseAttackerKnowledge.internal 0 = DY.ProtocolEvent.baseAttackerKnowledge DY.Signature'.Broken.BrokenDhEvent
• DY.Signature'.Broken.baseAttackerKnowledge.internal ⟨n.succ, isLt⟩ = ⋯.elim

def DY.Signature'.Broken.ExecEntryT.internal [BytesFunctor] : Fin 1 → Type

Equations

• DY.Signature'.Broken.ExecEntryT.internal 0 = DY.ProtocolEvent.ExecEntryT DY.Signature'.Broken.BrokenDhEvent
• DY.Signature'.Broken.ExecEntryT.internal ⟨n.succ, isLt⟩ = ⋯.elim

@[instance_reducible]

def DY.Signature'.Broken.baseAttackerKnowledge [BytesFunctor] [ExecTraceTypes] : SubBaseAttackerKnowledge ExecEntryT

Equations

• DY.Signature'.Broken.baseAttackerKnowledge = DY.SubBaseAttackerKnowledge.combine DY.Signature'.Broken.baseAttackerKnowledge.internal

def DY.Signature'.Broken.ThisVkHasBeenBroken [BytesFunctor] [ExecTraceTypes] [ExecTraceTypes.Has ExecEntryT] (brokenPk : Bytes) (tr : ExecTrace) : Prop

Equations

• DY.Signature'.Broken.ThisVkHasBeenBroken brokenPk tr = DY.Trace.EventLogged { brokenPk := brokenPk } tr

def DY.Signature'.Broken.OneVkHasBeenBroken [BytesFunctor] [ExecTraceTypes] [ExecTraceTypes.Has ExecEntryT] (tr : ExecTrace) : Prop

Equations

• DY.Signature'.Broken.OneVkHasBeenBroken tr = ∃ (brokenPk : DY.Bytes), DY.Signature'.Broken.ThisVkHasBeenBroken brokenPk tr

def DY.Signature'.Broken.label [BytesFunctor] [ExecTraceTypes] [ExecTraceTypes.Has ExecEntryT] (brokenPk : Bytes) : Label

Equations

• DY.Signature'.Broken.label brokenPk = { isCorrupt := fun (tr : DY.ExecTrace) => DY.Signature'.Broken.ThisVkHasBeenBroken brokenPk tr, isCorruptLater := ⋯ }

def DY.Signature'.Broken.breakVk [BytesFunctor] [ExecTraceTypes] [ExecTraceTypes.Has ExecEntryT] [BytesFunctor.Has SubF] [ExecTraceTypes.Has Network.ExecEntryT] (msgHandle : Nat) : Traceful Nat

Equations

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

def DY.Signature'.Broken.breakVk.reachability [BytesFunctor] [ExecTraceTypes] [ExecTraceTypes.Has ExecEntryT] [BytesFunctor.Has SubF] [ExecTraceTypes.Has Network.ExecEntryT] : ReachabilityConfig

Equations

• DY.Signature'.Broken.breakVk.reachability = DY.ReachabilityConfig.make fun (handle : Nat) => DY.Signature'.Broken.breakVk handle

def DY.Signature'.Vk.invariants [ExecTraceTypes] [ProofTraceTypes] [BytesFunctor] [BytesFunctor.Has Signature'.SubF] [ExecTraceTypes.Has Broken.ExecEntryT] : Bytes.PartialInvariants SubF

Equations

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

theorem DY.Signature'.Vk.invariantsProofs [ExecTraceTypes] [ProofTraceTypes] [BytesFunctor] [BytesFunctor.Has Signature'.SubF] [ExecTraceTypes.Has Broken.ExecEntryT] [BytesInvariants] : Bytes.PartialInvariantsProofs invariants

@[simp]

theorem DY.Signature'.vk.WellFormed [ExecTraceTypes] [ProofTraceTypes] [BytesFunctor] [BytesFunctor.Has SubF] [ExecTraceTypes.Has Broken.ExecEntryT] [BytesInvariants] [BytesInvariants.Has Vk.invariants] (inp : Bytes) (tr : ProofTrace) : (vk inp).WellFormed tr = inp.WellFormed tr

@[simp]

theorem DY.Signature'.vk.label [ExecTraceTypes] [ProofTraceTypes] [BytesFunctor] [BytesFunctor.Has SubF] [ExecTraceTypes.Has Broken.ExecEntryT] [BytesInvariants] [BytesInvariants.Has Vk.invariants] (inp : Bytes) (tr : ProofTrace) : (vk inp).label tr = Label.pub

@[simp]

theorem DY.Signature'.vk.Invariant [ExecTraceTypes] [ProofTraceTypes] [BytesFunctor] [BytesFunctor.Has SubF] [ExecTraceTypes.Has Broken.ExecEntryT] [BytesInvariants] [BytesInvariants.Has Vk.invariants] (sk : Bytes) (tr : ProofTrace) : sk.Invariant tr → (sk.label tr).canFlow (Broken.label (vk sk)) (Trace.erase tr) → (vk sk).Invariant tr

class DY.Signature'.SignPred [ExecTraceTypes] [ProofTraceTypes] [BytesFunctor] : Type

• pred [BytesWellFormed] [GetUsage] [GetLabel] : Usage → Bytes → Bytes → ProofTrace → Prop

class DY.Signature'.SignPredProof [ExecTraceTypes] [ProofTraceTypes] [BytesFunctor] [BytesInvariants] [SignPred] : Prop

• pred_later [BytesWellFormedLater] [GetUsageLater] [GetLabelLater] (skUsg : Usage) (vk msg : Bytes) (tr1 tr2 : ProofTrace) : vk.WellFormed tr1 → msg.WellFormed tr1 → tr1 ≤ tr2 → SignPred.pred skUsg vk msg tr1 → SignPred.pred skUsg vk msg tr2

theorem DY.Signature'.SignPredProof.pred_later_fast [ExecTraceTypes] [ProofTraceTypes] [BytesFunctor] [BytesInvariants] [SignPred] [SignPredProof] [BytesInvariantsProofs] (skUsg : Usage) (vk msg : Bytes) (tr1 tr2 : ProofTrace) : vk.Invariant tr1 → msg.Invariant tr1 → tr1 ≤ tr2 → SignPred.pred skUsg vk msg tr1 → SignPred.pred skUsg vk msg tr2

def DY.Signature'.Sign.invariants [ExecTraceTypes] [ProofTraceTypes] [BytesFunctor] [BytesFunctor.Has Signature'.SubF] [SignPred] : Bytes.PartialInvariants SubF

Equations

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

theorem DY.Signature'.Sign.invariantsProofs [ExecTraceTypes] [ProofTraceTypes] [BytesFunctor] [BytesFunctor.Has Signature'.SubF] [ExecTraceTypes.Has Broken.ExecEntryT] [BytesInvariants] [BytesInvariants.Has Vk.invariants] [SignPred] [SignPredProof] : Bytes.PartialInvariantsProofs invariants

theorem DY.Signature'.invariantsProofs [BytesFunctor] [ExecTraceTypes] [ProofTraceTypes] [BytesInvariants] [BytesFunctor.Has SubF] [SignPred] [ExecTraceTypes.Has Broken.ExecEntryT] [BytesInvariants.Has Vk.invariants] [SignPredProof] : Bytes.PartialInvariantsProofs invariants

def DY.Signature'.invariants.internal [BytesFunctor] [ExecTraceTypes] [ProofTraceTypes] [BytesFunctor.Has SubF] [SignPred] [ExecTraceTypes.Has Broken.ExecEntryT] (id✝ : Fin 2) : Bytes.PartialInvariants (SubF.internal id✝)

Equations

• DY.Signature'.invariants.internal 0 = DY.Signature'.Vk.invariants
• DY.Signature'.invariants.internal 1 = DY.Signature'.Sign.invariants
• DY.Signature'.invariants.internal ⟨n.succ.succ, isLt⟩ = ⋯.elim

theorem DY.Signature'.invariantsProofs.internal [BytesFunctor] [ExecTraceTypes] [ProofTraceTypes] [BytesInvariants] [BytesFunctor.Has SubF] [SignPred] [ExecTraceTypes.Has Broken.ExecEntryT] [BytesInvariants.Has Vk.invariants] [SignPredProof] (id✝ : Fin 2) : Bytes.PartialInvariantsProofs (invariants.internal id✝)

@[instance_reducible]

def DY.Signature'.invariants [BytesFunctor] [ExecTraceTypes] [ProofTraceTypes] [BytesFunctor.Has SubF] [SignPred] [ExecTraceTypes.Has Broken.ExecEntryT] : Bytes.PartialInvariants SubF

Equations

• DY.Signature'.invariants = DY.Bytes.PartialInvariants.combine DY.Signature'.invariants.internal

def DY.Bytes.SignkeyHasUsage' [BytesFunctor] [BytesFunctor.Has Signature'.SubF] [ExecTraceTypes] [ProofTraceTypes] [BytesInvariants] (vk : Bytes) (skUsg : Usage) (tr : ProofTrace) : Prop

Equations

• vk.SignkeyHasUsage' skUsg tr = DY.Bytes.XXXHasUsage DY.Signature'.extractSignkey✝ vk skUsg tr

theorem DY.Bytes.SignkeyHasUsage'_vk [BytesFunctor] [BytesFunctor.Has Signature'.SubF] [ExecTraceTypes] [ProofTraceTypes] [BytesInvariants] (sk : Bytes) (skUsg : Usage) (tr : ProofTrace) : (Signature'.vk sk).SignkeyHasUsage' skUsg tr = sk.HasUsage skUsg tr

theorem DY.Bytes.SignkeyHasUsage'_later [BytesFunctor] [BytesFunctor.Has Signature'.SubF] [ExecTraceTypes] [ProofTraceTypes] [BytesInvariants] [BytesInvariantsProofs] [ExecTraceTypes.Has Signature'.Broken.ExecEntryT] [Signature'.SignPred] [BytesInvariants.Has Signature'.invariants] (b : Bytes) (usg : Usage) (tr1 tr2 : ProofTrace) : b.WellFormed tr1 → tr1 ≤ tr2 → b.SignkeyHasUsage' usg tr1 → b.SignkeyHasUsage' usg tr2

theorem DY.Bytes.SignkeyHasUsage'_later_fast [BytesFunctor] [BytesFunctor.Has Signature'.SubF] [ExecTraceTypes] [ProofTraceTypes] [BytesInvariants] [BytesInvariantsProofs] [ExecTraceTypes.Has Signature'.Broken.ExecEntryT] [Signature'.SignPred] [BytesInvariants.Has Signature'.invariants] (b : Bytes) (usg : Usage) (tr1 tr2 : ProofTrace) : b.Invariant tr1 → tr1 ≤ tr2 → b.SignkeyHasUsage' usg tr1 → b.SignkeyHasUsage' usg tr2

noncomputable def DY.Bytes.signkeyLabel' [BytesFunctor] [BytesFunctor.Has Signature'.SubF] [ExecTraceTypes] [ProofTraceTypes] [BytesInvariants] (vk : Bytes) (tr : ProofTrace) : Label

Equations

• vk.signkeyLabel' tr = DY.Bytes.xxxLabel DY.Signature'.extractSignkey✝ vk tr

theorem DY.Bytes.signkeyLabel'_vk [BytesFunctor] [BytesFunctor.Has Signature'.SubF] [ExecTraceTypes] [ProofTraceTypes] [BytesInvariants] [ExecTraceTypes.Has Signature'.Broken.ExecEntryT] [Signature'.SignPred] [BytesInvariants.Has Signature'.invariants] (sk : Bytes) (tr : ProofTrace) : (Signature'.vk sk).signkeyLabel' tr = sk.label tr

theorem DY.Bytes.signkeyLabel'_later [BytesFunctor] [BytesFunctor.Has Signature'.SubF] [ExecTraceTypes] [ProofTraceTypes] [BytesInvariants] [BytesInvariantsProofs] [ExecTraceTypes.Has Signature'.Broken.ExecEntryT] [Signature'.SignPred] [BytesInvariants.Has Signature'.invariants] (b : Bytes) (tr1 tr2 : ProofTrace) : b.WellFormed tr1 → tr1 ≤ tr2 → b.signkeyLabel' tr1 = b.signkeyLabel' tr2

theorem DY.Bytes.signkeyLabel'_later_fast [BytesFunctor] [BytesFunctor.Has Signature'.SubF] [ExecTraceTypes] [ProofTraceTypes] [BytesInvariants] [BytesInvariantsProofs] [ExecTraceTypes.Has Signature'.Broken.ExecEntryT] [Signature'.SignPred] [BytesInvariants.Has Signature'.invariants] (b : Bytes) (tr1 tr2 : ProofTrace) : b.Invariant tr1 → tr1 ≤ tr2 → b.signkeyLabel' tr1 = b.signkeyLabel' tr2

@[simp]

theorem DY.Signature'.sign.WellFormed [ExecTraceTypes] [ProofTraceTypes] [BytesFunctor] [BytesFunctor.Has SubF] [ExecTraceTypes.Has Broken.ExecEntryT] [SignPred] [BytesInvariants] [BytesInvariants.Has invariants] (sk nonce msg : Bytes) (tr : ProofTrace) : (sign sk nonce msg).WellFormed tr = (sk.WellFormed tr ∧ nonce.WellFormed tr ∧ msg.WellFormed tr)

@[simp]

theorem DY.Signature'.sign.label [ExecTraceTypes] [ProofTraceTypes] [BytesFunctor] [BytesFunctor.Has SubF] [ExecTraceTypes.Has Broken.ExecEntryT] [SignPred] [BytesInvariants] [BytesInvariants.Has invariants] (sk nonce msg : Bytes) (tr : ProofTrace) : (sign sk nonce msg).label tr = msg.label tr

@[simp]

theorem DY.Signature'.sign.Invariant [ExecTraceTypes] [ProofTraceTypes] [BytesFunctor] [BytesFunctor.Has SubF] [ExecTraceTypes.Has Broken.ExecEntryT] [SignPred] [BytesInvariants] [BytesInvariants.Has invariants] (sk nonce msg : Bytes) (sk_usg : Usage) (tr : ProofTrace) : sk.Invariant tr ∧ nonce.Invariant tr ∧ msg.Invariant tr ∧ sk.HasUsage sk_usg tr ∧ (sk.label tr).canFlow (nonce.label tr) (Trace.erase tr) ∧ (sk_usg.type = "SigKey" ∧ SignPred.pred sk_usg (vk sk) msg tr ∨ (sk.label tr).canFlow Label.pub (Trace.erase tr)) → (sign sk nonce msg).Invariant tr

@[simp]

theorem DY.Signature'.verify.Invariant [ExecTraceTypes] [ProofTraceTypes] [BytesFunctor] [BytesFunctor.Has SubF] [ExecTraceTypes.Has Broken.ExecEntryT] [SignPred] [BytesInvariants] [BytesInvariants.Has invariants] (vk msg sig : Bytes) (skUsg : Usage) (tr : ProofTrace) : vk.Invariant tr → msg.Invariant tr → sig.Invariant tr → vk.SignkeyHasUsage' skUsg tr → verify vk msg sig = true → (skUsg.type = "SigKey" → SignPred.pred skUsg vk msg tr) ∨ (vk.signkeyLabel' tr).canFlow Label.pub (Trace.erase tr)

@[instance_reducible]

instance DY.Signature'.instHasGhostArgumentTypeBytesSignUsage [BytesFunctor] [BytesFunctor.Has SubF] (sk nonce msg : Bytes) : HasGhostArgumentType (sign sk nonce msg) Usage

Equations

• DY.Signature'.instHasGhostArgumentTypeBytesSignUsage sk nonce msg = { dummy := () }

@[instance_reducible]

instance DY.Signature'.instHasGhostArgumentTypeBoolVerifyBytesUsage [BytesFunctor] [BytesFunctor.Has SubF] (vkey msg sig : Bytes) : HasGhostArgumentType (verify vkey msg sig) Usage

Equations

• DY.Signature'.instHasGhostArgumentTypeBoolVerifyBytesUsage vkey msg sig = { dummy := () }

instance DY.Signature'.instSubAttackerKnowledgeTheoremSubFAttackerKnowledge [ExecTraceTypes] [ProofTraceTypes] [TraceInvariant] [BytesFunctor] [BytesInvariants] [BytesFunctor.Has SubF] [ExecTraceTypes.Has Broken.ExecEntryT] [SignPred] [BytesInvariants.Has invariants] : SubAttackerKnowledgeTheorem vk.attackerKnowledge

instance DY.Signature'.instSubAttackerKnowledgeTheoremSubFAttackerKnowledge_1 [ExecTraceTypes] [ProofTraceTypes] [TraceInvariant] [BytesFunctor] [BytesInvariants] [BytesFunctor.Has SubF] [ExecTraceTypes.Has Broken.ExecEntryT] [SignPred] [BytesInvariants.Has invariants] : SubAttackerKnowledgeTheorem sign.attackerKnowledge

@[instance_reducible]

instance DY.Signature'.Broken.instEventInvBrokenDhEvent [BytesFunctor] [ExecTraceTypes] [ProofTraceTypes] : ProtocolEvent.EventInv BrokenDhEvent

Equations

• DY.Signature'.Broken.instEventInvBrokenDhEvent = { invariant := fun (x : DY.ProofTrace) (x_1 : DY.Signature'.Broken.BrokenDhEvent) => True }

def DY.Signature'.Broken.ProofEntryT.internal [BytesFunctor] : Fin 1 → Type

Equations

• DY.Signature'.Broken.ProofEntryT.internal 0 = DY.ProtocolEvent.ProofEntryT DY.Signature'.Broken.BrokenDhEvent
• DY.Signature'.Broken.ProofEntryT.internal ⟨n.succ, isLt⟩ = ⋯.elim

@[instance_reducible]

def DY.Signature'.Broken.ProofEntryT [BytesFunctor] : Type

Equations

• DY.Signature'.Broken.ProofEntryT = DY.ProofTraceTypes.combine DY.Signature'.Broken.ProofEntryT.internal

instance DY.Signature'.Broken.instReachableImpliesInvariantReachability [BytesFunctor] [ExecTraceTypes] [ProofTraceTypes] [TraceInvariant] [BytesInvariants] [BytesFunctor.Has SubF] [ExecTraceTypes.Has ExecEntryT] [SignPred] [BytesInvariants.Has invariants] [BytesInvariantsProofs] [ExecTraceTypes.Has Network.ExecEntryT] [ProofTraceTypes.Has ProofEntryT] [ProofTraceTypes.Has Network.ProofEntryT] [TraceInvariant.Has Network.ProofEntryT] [TraceInvariant.Has ProofEntryT] : ReachableImpliesInvariant breakVk.reachability