class DY.Literal.CanMkLiteral (Bytes : Type u) : Type u

• literalToBytes : ByteArray → Bytes
• bytesToLiteral : Bytes → Option ByteArray

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

• lit : ByteArray

@[instance_reducible]

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

Equations

• DY.Literal.Literal.instFunctorSizeOfSubF = { sizeOf := fun {t : Type} [SizeOf t] (x : DY.Literal.Literal.SubF t) => match x with | { lit := lit } => 0 }

@[instance_reducible]

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

Equations

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

@[instance_reducible]

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

Equations

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

@[instance_reducible]

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

Equations

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

@[instance_reducible]

instance DY.Literal.Literal.instSubBytesFunctorSubF : SubBytesFunctor SubF

Equations

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

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

Equations

• { lit := lit }.length x_2 = lit.size

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

Equations

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

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

Equations

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

@[instance_reducible]

def DY.Literal.SubF : Type → Type

Equations

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

@[instance_reducible]

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

Equations

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

@[reducible, inline]

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

Equations

• x.pack = DY.BytesView.pack x

theorem DY.Literal.bytesToLiteral_literalToBytes [BytesFunctor] [BytesFunctor.Has SubF] (lit : ByteArray) : bytesToLiteral (literalToBytes lit) = some lit

theorem DY.Literal.literalToBytes_bytesToLiteral [BytesFunctor] [BytesFunctor.Has SubF] (buf : Bytes) : match bytesToLiteral buf with | none => True | some lit => buf = literalToBytes lit

@[simp]

theorem DY.Literal.length_literalToBytes [BytesFunctor] [BytesLength] [BytesFunctor.Has SubF] [BytesLength.Has SubF.length] (buf : ByteArray) : (literalToBytes buf).length = buf.size

def DY.Literal.literalToBytes.attackerKnowledge [BytesFunctor] [BytesFunctor.Has SubF] : SubAttackerKnowledge SubF

Equations

• DY.Literal.literalToBytes.attackerKnowledge = { pred := fun (p : DY.Bytes → Prop) (out : DY.Bytes) => ∃ (lit : ByteArray), out = DY.Literal.literalToBytes lit, pred_isScottContinuous := ⋯ }

@[instance_reducible]

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

Equations

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

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

Equations

• DY.Literal.attackerKnowledge.internal 0 = DY.Literal.literalToBytes.attackerKnowledge
• DY.Literal.attackerKnowledge.internal ⟨n.succ, isLt⟩ = ⋯.elim

theorem DY.Literal.attacker_knows_literalToBytes [BytesFunctor] [BytesFunctor.Has SubF] [ExecTraceTypes] [BaseAttackerKnowledge] [AttackerKnowledge] [AttackerKnowledge.Has attackerKnowledge] (lit : ByteArray) (tr : ExecTrace) : (literalToBytes lit).AttackerKnows tr

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

Equations

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

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

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

Equations

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

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

@[instance_reducible]

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

Equations

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

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

@[simp]

theorem DY.Literal.literalToBytes.WellFormed [ExecTraceTypes] [ProofTraceTypes] [BytesFunctor] [BytesFunctor.Has SubF] [BytesWellFormed] [BytesWellFormed.Has Literal.invariants.well_formed] (lit : ByteArray) (tr : ProofTrace) : (literalToBytes lit).WellFormed tr

@[simp]

theorem DY.Literal.literalToBytes.label [ExecTraceTypes] [ProofTraceTypes] [BytesFunctor] [BytesFunctor.Has SubF] [BytesInvariants] [BytesInvariants.Has invariants] (lit : ByteArray) (tr : ProofTrace) : (literalToBytes lit).label tr = Label.pub

@[simp]

theorem DY.Literal.literalToBytes.Invariant [ExecTraceTypes] [ProofTraceTypes] [BytesFunctor] [BytesFunctor.Has SubF] [BytesInvariants] [BytesInvariants.Has invariants] (lit : ByteArray) (tr : ProofTrace) : (literalToBytes lit).Invariant tr

instance DY.Literal.instSubAttackerKnowledgeTheoremSubFAttackerKnowledge [ExecTraceTypes] [ProofTraceTypes] [TraceInvariant] [BytesFunctor] [BytesInvariants] [BytesFunctor.Has SubF] [BytesInvariants.Has invariants] : SubAttackerKnowledgeTheorem literalToBytes.attackerKnowledge