structure DY.Example.ACME.WithDEO.SignDEO.DEO.SubF (Bytes : Type) : Type

• msg : Bytes
• sig : Bytes

@[instance_reducible]

instance DY.Example.ACME.WithDEO.SignDEO.DEO.instFunctorSizeOfSubF : ALaCarte.FunctorSizeOf SubF

Equations

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

@[instance_reducible]

instance DY.Example.ACME.WithDEO.SignDEO.DEO.instRepresentableSubF : ALaCarte.Representable SubF

Equations

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

@[instance_reducible]

instance DY.Example.ACME.WithDEO.SignDEO.DEO.instRepresentableDecidableEqSubF : ALaCarte.RepresentableDecidableEq SubF

Equations

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

@[instance_reducible]

instance DY.Example.ACME.WithDEO.SignDEO.DEO.instRepresentableOrdSubF : ALaCarte.RepresentableOrd SubF

Equations

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

@[instance_reducible]

instance DY.Example.ACME.WithDEO.SignDEO.DEO.instSubBytesFunctorSubF : SubBytesFunctor SubF

Equations

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

def DY.Example.ACME.WithDEO.SignDEO.DEO.SubF.length [BytesFunctor] : Bytes.PartialLength SubF

Equations

• x✝¹.length x✝ = 32

@[instance_reducible]

def DY.Example.ACME.WithDEO.SignDEO.SubF.length [BytesFunctor] : Bytes.PartialLength SubF

Equations

• DY.Example.ACME.WithDEO.SignDEO.SubF.length = DY.Bytes.PartialLength.combine DY.Example.ACME.WithDEO.SignDEO.SubF.length.internal

@[instance_reducible]

def DY.Example.ACME.WithDEO.SignDEO.SubF : Type → Type

Equations

• DY.Example.ACME.WithDEO.SignDEO.SubF = DY.BytesFunctor.combine DY.Example.ACME.WithDEO.SignDEO.SubF.internal

def DY.Example.ACME.WithDEO.SignDEO.SubF.internal : Fin 3 → Type → Type

Equations

• DY.Example.ACME.WithDEO.SignDEO.SubF.internal 0 = DY.Signature.Vk.SubF
• DY.Example.ACME.WithDEO.SignDEO.SubF.internal 1 = DY.Signature.Sign.SubF
• DY.Example.ACME.WithDEO.SignDEO.SubF.internal 2 = DY.Example.ACME.WithDEO.SignDEO.DEO.SubF
• DY.Example.ACME.WithDEO.SignDEO.SubF.internal ⟨n.succ.succ.succ, isLt⟩ = ⋯.elim

def DY.Example.ACME.WithDEO.SignDEO.SubF.length.internal [BytesFunctor] (id✝ : Fin 3) : Bytes.PartialLength (SubF.internal id✝)

Equations

• DY.Example.ACME.WithDEO.SignDEO.SubF.length.internal 0 = DY.Signature.Vk.SubF.length
• DY.Example.ACME.WithDEO.SignDEO.SubF.length.internal 1 = DY.Signature.Sign.SubF.length
• DY.Example.ACME.WithDEO.SignDEO.SubF.length.internal 2 = DY.Example.ACME.WithDEO.SignDEO.DEO.SubF.length
• DY.Example.ACME.WithDEO.SignDEO.SubF.length.internal ⟨n.succ.succ.succ, isLt⟩ = ⋯.elim

@[reducible, inline]

abbrev DY.Example.ACME.WithDEO.SignDEO.DEO.SubF.pack [BytesFunctor] [BytesFunctor.Has SubF] (x : SubF Bytes) : Bytes

Equations

• x.pack = DY.BytesView.pack x

@[instance_reducible]

instance DY.Example.ACME.WithDEO.SignDEO.instCanSignBytes_examples [BytesFunctor] [BytesFunctor.Has SubF] : Signature.CanSign Bytes

Equations

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

def DY.Example.ACME.WithDEO.SignDEO.deogen [BytesFunctor] [BytesFunctor.Has SubF] (msg sig : Bytes) : Bytes

Equations

• DY.Example.ACME.WithDEO.SignDEO.deogen msg sig = { msg := msg, sig := sig }.pack

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

theorem DY.Example.ACME.WithDEO.SignDEO.verify_deo [BytesFunctor] [BytesFunctor.Has SubF] (sk nonce msg1 msg2 : Bytes) : Signature.verify (Signature.vk (deogen msg2 (Signature.sign sk nonce msg1))) msg2 (Signature.sign sk nonce msg1) = true

def DY.Example.ACME.WithDEO.SignDEO.vk.attackerKnowledge [BytesFunctor] [BytesFunctor.Has SubF] : SubAttackerKnowledge SubF

Equations

• DY.Example.ACME.WithDEO.SignDEO.vk.attackerKnowledge = { pred := fun (p : DY.Bytes → Prop) (out : DY.Bytes) => ∃ (sk : DY.Bytes), out = DY.Signature.vk sk ∧ p sk, pred_isMonotonic := ⋯ }

def DY.Example.ACME.WithDEO.SignDEO.sign.attackerKnowledge [BytesFunctor] [BytesFunctor.Has SubF] : SubAttackerKnowledge SubF

Equations

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

def DY.Example.ACME.WithDEO.SignDEO.deogen.attackerKnowledge [BytesFunctor] [BytesFunctor.Has SubF] : SubAttackerKnowledge SubF

Equations

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

def DY.Example.ACME.WithDEO.SignDEO.attackerKnowledge.internal [BytesFunctor] [BytesFunctor.Has SubF] : Fin 3 → SubAttackerKnowledge SubF

Equations

• DY.Example.ACME.WithDEO.SignDEO.attackerKnowledge.internal 0 = DY.Example.ACME.WithDEO.SignDEO.vk.attackerKnowledge
• DY.Example.ACME.WithDEO.SignDEO.attackerKnowledge.internal 1 = DY.Example.ACME.WithDEO.SignDEO.sign.attackerKnowledge
• DY.Example.ACME.WithDEO.SignDEO.attackerKnowledge.internal 2 = DY.Example.ACME.WithDEO.SignDEO.deogen.attackerKnowledge
• DY.Example.ACME.WithDEO.SignDEO.attackerKnowledge.internal ⟨n.succ.succ.succ, isLt⟩ = ⋯.elim

@[instance_reducible]

def DY.Example.ACME.WithDEO.SignDEO.attackerKnowledge [BytesFunctor] [BytesFunctor.Has SubF] : SubAttackerKnowledge SubF

Equations

• DY.Example.ACME.WithDEO.SignDEO.attackerKnowledge = DY.SubAttackerKnowledge.combine' DY.Example.ACME.WithDEO.SignDEO.attackerKnowledge.internal

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

theorem DY.Example.ACME.WithDEO.SignDEO.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 → (Signature.sign sk nonce msg).AttackerKnows tr

theorem DY.Example.ACME.WithDEO.SignDEO.attacker_knows_deogen [BytesFunctor] [BytesFunctor.Has SubF] [ExecTraceTypes] [BaseAttackerKnowledge] [AttackerKnowledge] [AttackerKnowledge.Has attackerKnowledge] (msg sig : Bytes) (tr : ExecTrace) : msg.AttackerKnows tr → sig.AttackerKnows tr → (deogen msg sig).AttackerKnows tr