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.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

@[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.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

@[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.

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

@[instance_reducible]

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

Equations

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

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.Vk.invariants [ExecTraceTypes] [ProofTraceTypes] [BytesFunctor] : Bytes.PartialInvariants SubF

Equations

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

theorem DY.Signature.Vk.invariantsProofs [ExecTraceTypes] [ProofTraceTypes] [BytesFunctor] [BytesInvariants] : Bytes.PartialInvariantsProofs invariants

@[simp]

theorem DY.Signature.vk.WellFormed [ExecTraceTypes] [ProofTraceTypes] [BytesFunctor] [BytesFunctor.Has SubF] [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] [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] [BytesInvariants] [BytesInvariants.Has Vk.invariants] (inp : Bytes) (tr : ProofTrace) : inp.Invariant tr → (vk inp).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] [BytesInvariants] [BytesInvariants.Has Vk.invariants] [SignPred] [SignPredProof] : Bytes.PartialInvariantsProofs invariants

def DY.Signature.invariants.internal [BytesFunctor] [ExecTraceTypes] [ProofTraceTypes] [BytesFunctor.Has SubF] [SignPred] (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 [BytesFunctor] [ExecTraceTypes] [ProofTraceTypes] [BytesInvariants] [BytesFunctor.Has SubF] [SignPred] [BytesInvariants.Has Vk.invariants] [SignPredProof] : Bytes.PartialInvariantsProofs invariants

@[instance_reducible]

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

Equations

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

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

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] [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] [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] [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] [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] [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] [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] [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] [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] [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 := () }

def DY.Signature.signMetaprog : GhostParameterFinder

Equations

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

@[instance_reducible]

instance DY.Signature.instHasGhostMetaprogramBytesSignSignMetaprog [BytesFunctor] [BytesFunctor.Has SubF] (sk nonce msg : Bytes) : HasGhostMetaprogram (sign sk nonce msg) signMetaprog

Equations

• DY.Signature.instHasGhostMetaprogramBytesSignSignMetaprog 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 := () }

def DY.Signature.verifyMetaprog : GhostParameterFinder

Equations

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

@[instance_reducible]

instance DY.Signature.instHasGhostMetaprogramBoolVerifyBytesVerifyMetaprog [BytesFunctor] [BytesFunctor.Has SubF] (vkey msg sig : Bytes) : HasGhostMetaprogram (verify vkey msg sig) verifyMetaprog

Equations

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

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

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