class DY.KdfExpand.CanKdfExpand (Bytes : Type u) : Type u

• kdfExpand (prk info : Bytes) (len : Nat) : Bytes

structure DY.KdfExpand.KdfExpand.SubF (Bytes : Type) : Type

• prk : Bytes
• info : Bytes
• len : Nat

@[instance_reducible]

instance DY.KdfExpand.KdfExpand.instFunctorSizeOfSubF : ALaCarte.FunctorSizeOf SubF

Equations

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

@[instance_reducible]

instance DY.KdfExpand.KdfExpand.instRepresentableSubF : ALaCarte.Representable SubF

Equations

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

@[instance_reducible]

instance DY.KdfExpand.KdfExpand.instRepresentableDecidableEqSubF : ALaCarte.RepresentableDecidableEq SubF

Equations

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

@[instance_reducible]

instance DY.KdfExpand.KdfExpand.instRepresentableOrdSubF : ALaCarte.RepresentableOrd SubF

Equations

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

@[instance_reducible]

instance DY.KdfExpand.KdfExpand.instSubBytesFunctorSubF : SubBytesFunctor SubF

Equations

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

def DY.KdfExpand.KdfExpand.SubF.length [BytesFunctor] : Bytes.PartialLength SubF

Equations

• { prk := prk, info := info, len := len }.length x_2 = len

@[instance_reducible]

def DY.KdfExpand.SubF.length [BytesFunctor] : Bytes.PartialLength SubF

Equations

• DY.KdfExpand.SubF.length = DY.Bytes.PartialLength.combine DY.KdfExpand.SubF.length.internal

@[instance_reducible]

def DY.KdfExpand.SubF : Type → Type

Equations

• DY.KdfExpand.SubF = DY.BytesFunctor.combine DY.KdfExpand.SubF.internal

def DY.KdfExpand.SubF.length.internal [BytesFunctor] (id✝ : Fin 1) : Bytes.PartialLength (SubF.internal id✝)

Equations

• DY.KdfExpand.SubF.length.internal 0 = DY.KdfExpand.KdfExpand.SubF.length
• DY.KdfExpand.SubF.length.internal ⟨n.succ, isLt⟩ = ⋯.elim

def DY.KdfExpand.SubF.internal : Fin 1 → Type → Type

Equations

• DY.KdfExpand.SubF.internal 0 = DY.KdfExpand.KdfExpand.SubF
• DY.KdfExpand.SubF.internal ⟨n.succ, isLt⟩ = ⋯.elim

@[reducible, inline]

abbrev DY.KdfExpand.KdfExpand.SubF.pack [BytesFunctor] [BytesFunctor.Has SubF] (x : SubF Bytes) : Bytes

Equations

• x.pack = DY.BytesView.pack x

@[instance_reducible]

instance DY.KdfExpand.instCanKdfExpandBytes [BytesFunctor] [BytesFunctor.Has SubF] : CanKdfExpand Bytes

Equations

• DY.KdfExpand.instCanKdfExpandBytes = { kdfExpand := fun (prk info : DY.Bytes) (len : Nat) => { prk := prk, info := info, len := len }.pack }

def DY.KdfExpand.kdfExpand.attackerKnowledge [BytesFunctor] [BytesFunctor.Has SubF] : SubAttackerKnowledge SubF

Equations

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

@[instance_reducible]

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

Equations

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

def DY.KdfExpand.attackerKnowledge.internal [BytesFunctor] [BytesFunctor.Has SubF] : Fin 1 → SubAttackerKnowledge SubF

Equations

• DY.KdfExpand.attackerKnowledge.internal 0 = DY.KdfExpand.kdfExpand.attackerKnowledge
• DY.KdfExpand.attackerKnowledge.internal ⟨n.succ, isLt⟩ = ⋯.elim

theorem DY.KdfExpand.attacker_knows_kdfExpand [BytesFunctor] [BytesFunctor.Has SubF] [ExecTraceTypes] [BaseAttackerKnowledge] [AttackerKnowledge] [AttackerKnowledge.Has attackerKnowledge] (prk info : Bytes) (len : Nat) (tr : ExecTrace) : prk.AttackerKnows tr → info.AttackerKnows tr → (kdfExpand prk info len).AttackerKnows tr

class DY.KdfExpand.KdfExpandInvariant [ExecTraceTypes] [BytesFunctor] : Type

• usage (prkUsage : Usage) (info : Bytes) : Usage
• label (prkUsage : Usage) (prkLabel : Label) (info : Bytes) : Label
• label_sound (prkUsage : Usage) (prkLabel : Label) (info : Bytes) (tr : ExecTrace) : (label prkUsage prkLabel info).canFlow prkLabel tr

def DY.KdfExpand.KdfExpand.invariants [ExecTraceTypes] [ProofTraceTypes] [BytesFunctor] [KdfExpandInvariant] : Bytes.PartialInvariants SubF

Equations

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

theorem DY.KdfExpand.KdfExpand.invariantsProofs [ExecTraceTypes] [ProofTraceTypes] [BytesFunctor] [BytesInvariants] [KdfExpandInvariant] : Bytes.PartialInvariantsProofs invariants

@[instance_reducible]

def DY.KdfExpand.invariants [BytesFunctor] [ExecTraceTypes] [ProofTraceTypes] [KdfExpandInvariant] : Bytes.PartialInvariants SubF

Equations

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

theorem DY.KdfExpand.invariantsProofs.internal [BytesFunctor] [ExecTraceTypes] [ProofTraceTypes] [BytesInvariants] [KdfExpandInvariant] (id✝ : Fin 1) : Bytes.PartialInvariantsProofs (invariants.internal id✝)

def DY.KdfExpand.invariants.internal [BytesFunctor] [ExecTraceTypes] [ProofTraceTypes] [KdfExpandInvariant] (id✝ : Fin 1) : Bytes.PartialInvariants (SubF.internal id✝)

Equations

• DY.KdfExpand.invariants.internal 0 = DY.KdfExpand.KdfExpand.invariants
• DY.KdfExpand.invariants.internal ⟨n.succ, isLt⟩ = ⋯.elim

theorem DY.KdfExpand.invariantsProofs [BytesFunctor] [ExecTraceTypes] [ProofTraceTypes] [BytesInvariants] [KdfExpandInvariant] : Bytes.PartialInvariantsProofs invariants

@[simp]

theorem DY.KdfExpand.kdfExpand.WellFormed [ExecTraceTypes] [ProofTraceTypes] [BytesFunctor] [BytesFunctor.Has SubF] [KdfExpandInvariant] [BytesWellFormed] [BytesWellFormed.Has KdfExpand.invariants.well_formed] (prk info : Bytes) (len : Nat) (tr : ProofTrace) : (kdfExpand prk info len).WellFormed tr = (prk.WellFormed tr ∧ info.WellFormed tr)

@[simp]

theorem DY.KdfExpand.kdfExpand.HasUsage [ExecTraceTypes] [ProofTraceTypes] [BytesFunctor] [BytesFunctor.Has SubF] [KdfExpandInvariant] [BytesInvariants] [BytesInvariants.Has invariants] (prk info : Bytes) (len : Nat) (prkUsage : Usage) (tr : ProofTrace) : prk.HasUsage prkUsage tr → (kdfExpand prk info len).HasUsage (KdfExpandInvariant.usage prkUsage info) tr

@[simp]

theorem DY.KdfExpand.kdfExpand.label [ExecTraceTypes] [ProofTraceTypes] [BytesFunctor] [BytesFunctor.Has SubF] [KdfExpandInvariant] [BytesInvariants] [BytesInvariants.Has invariants] (prk info : Bytes) (len : Nat) (prkUsage : Usage) (tr : ProofTrace) : prk.HasUsage prkUsage tr → ((kdfExpand prk info len).label tr).equivalent (KdfExpandInvariant.label prkUsage (prk.label tr) info) (Trace.erase tr)

@[simp]

theorem DY.KdfExpand.kdfExpand.Invariant [ExecTraceTypes] [ProofTraceTypes] [BytesFunctor] [BytesFunctor.Has SubF] [KdfExpandInvariant] [BytesInvariants] [BytesInvariants.Has invariants] (prk info : Bytes) (len : Nat) (tr : ProofTrace) : (kdfExpand prk info len).Invariant tr = (prk.Invariant tr ∧ info.Invariant tr)

@[instance_reducible]

instance DY.KdfExpand.instHasGhostArgumentTypeBytesKdfExpandUsage [BytesFunctor] [BytesFunctor.Has SubF] (prk info : Bytes) (len : Nat) : HasGhostArgumentType (kdfExpand prk info len) Usage

Equations

• DY.KdfExpand.instHasGhostArgumentTypeBytesKdfExpandUsage prk info len = { dummy := () }

instance DY.KdfExpand.instHoareTriplePureGhostBytesUsageKdfExpandAndInvariantHasUsagePublishableEquivalentLabelLabelEraseUsage [BytesFunctor] [BytesFunctor.Has SubF] [ExecTraceTypes] [ProofTraceTypes] [KdfExpandInvariant] [BytesInvariants] [BytesInvariants.Has invariants] (prk info : Bytes) (len : Nat) (prkUsage : Usage) : HoareTriplePureGhost (kdfExpand prk info len) prkUsage (fun (tr : ProofTrace) => prk.Invariant tr ∧ prk.HasUsage prkUsage tr ∧ info.Publishable tr) fun (res : Bytes) (tr : ProofTrace) => res.Invariant tr ∧ (res.label tr).equivalent (KdfExpandInvariant.label prkUsage (prk.label tr) info) (Trace.erase tr) ∧ res.HasUsage (KdfExpandInvariant.usage prkUsage info) tr

instance DY.KdfExpand.instSubAttackerKnowledgeTheoremSubFAttackerKnowledge [ExecTraceTypes] [ProofTraceTypes] [TraceInvariant] [BytesFunctor] [BytesInvariants] [BytesFunctor.Has SubF] [KdfExpandInvariant] [BytesInvariants.Has invariants] : SubAttackerKnowledgeTheorem kdfExpand.attackerKnowledge