DY.EquationalTheory.Concat

source

class DY.Concat.CanConcat (Bytes : Type u) :

Type u

concat : Bytes → Bytes → Bytes
split : Bytes → Nat → Option (Bytes × Bytes)

Instances

source

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

Type

lhs : Bytes
rhs : Bytes

Instances For

source

@[instance_reducible]

instance DY.Concat.Concat.instFunctorSizeOfSubF :

ALaCarte.FunctorSizeOf SubF

Equations

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

source

@[instance_reducible]

instance DY.Concat.Concat.instRepresentableSubF :

ALaCarte.Representable SubF

Equations

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

source

@[instance_reducible]

instance DY.Concat.Concat.instRepresentableDecidableEqSubF :

ALaCarte.RepresentableDecidableEq SubF

Equations

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

source

@[instance_reducible]

instance DY.Concat.Concat.instRepresentableOrdSubF :

ALaCarte.RepresentableOrd SubF

Equations

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

source

@[instance_reducible]

instance DY.Concat.Concat.instSubBytesFunctorSubF :

SubBytesFunctor SubF

Equations

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

source

def DY.Concat.Concat.SubF.length [BytesFunctor] :

Bytes.PartialLength SubF

Equations

{ lhs := lhs, rhs := rhs }.length rec_2 = rec_2 lhs ⋯ + rec_2 rhs ⋯

Instances For

source

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

Bytes.PartialLength (SubF.internal id✝)

Equations

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

Instances For

source

def DY.Concat.SubF.internal :

Fin 1 → Type → Type

Equations

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

Instances For

source

@[instance_reducible]

def DY.Concat.SubF :

Type → Type

Equations

DY.Concat.SubF = DY.BytesFunctor.combine DY.Concat.SubF.internal

Instances For

source

@[instance_reducible]

def DY.Concat.SubF.length [BytesFunctor] :

Bytes.PartialLength SubF

Equations

DY.Concat.SubF.length = DY.Bytes.PartialLength.combine DY.Concat.SubF.length.internal

Instances For

source

@[reducible, inline]

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

Bytes

Equations

x.pack = DY.BytesView.pack x

Instances For

source

@[instance_reducible]

instance DY.Concat.instCanConcatBytes [BytesFunctor] [BytesFunctor.Has SubF] [BytesLength] :

CanConcat Bytes

Equations

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

source

theorem DY.Concat.split_concat [BytesFunctor] [BytesFunctor.Has SubF] [BytesLength] (lhs rhs : Bytes) :

split (concat lhs rhs) lhs.length = some (lhs, rhs)

source

theorem DY.Concat.concat_split [BytesFunctor] [BytesFunctor.Has SubF] [BytesLength] (buf : Bytes) (i : Nat) (lhs rhs : Bytes) :

split buf i = some (lhs, rhs) → concat lhs rhs = buf

source

@[simp]

theorem DY.Concat.length_concat [BytesFunctor] [BytesFunctor.Has SubF] [BytesLength] [BytesLength.Has SubF.length] (lhs rhs : Bytes) :

(concat lhs rhs).length = lhs.length + rhs.length

source

@[simp]

theorem DY.Concat.length_split [BytesFunctor] [BytesFunctor.Has SubF] [BytesLength] [BytesLength.Has SubF.length] (buf : Bytes) (i : Nat) (lhs rhs : Bytes) :

split buf i = some (lhs, rhs) → lhs.length = i ∧ i + rhs.length = buf.length

source

def DY.Concat.concat.attackerKnowledge [BytesFunctor] [BytesFunctor.Has SubF] [BytesLength] :

SubAttackerKnowledge SubF

Equations

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

Instances For

source

def DY.Concat.splitLeft.attackerKnowledge [BytesFunctor] [BytesFunctor.Has SubF] [BytesLength] :

SubAttackerKnowledge SubF

Equations

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

Instances For

source

def DY.Concat.splitRight.attackerKnowledge [BytesFunctor] [BytesFunctor.Has SubF] [BytesLength] :

SubAttackerKnowledge SubF

Equations

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

Instances For

source

@[instance_reducible]

def DY.Concat.attackerKnowledge [BytesFunctor] [BytesFunctor.Has SubF] [BytesLength] :

SubAttackerKnowledge SubF

Equations

DY.Concat.attackerKnowledge = DY.SubAttackerKnowledge.combine' DY.Concat.attackerKnowledge.internal

Instances For

source

theorem DY.Concat.attacker_knows_concat [BytesFunctor] [BytesFunctor.Has SubF] [BytesLength] [ExecTraceTypes] [BaseAttackerKnowledge] [AttackerKnowledge] [AttackerKnowledge.Has attackerKnowledge] (lhs rhs : Bytes) (tr : ExecTrace) :

lhs.AttackerKnows tr → rhs.AttackerKnows tr → (concat lhs rhs).AttackerKnows tr

source

theorem DY.Concat.attacker_knows_split [BytesFunctor] [BytesFunctor.Has SubF] [BytesLength] [ExecTraceTypes] [BaseAttackerKnowledge] [AttackerKnowledge] [AttackerKnowledge.Has attackerKnowledge] (buf : Bytes) (i : Nat) (tr : ExecTrace) :

buf.AttackerKnows tr → match split buf i with | none => True | some (lhs, rhs) => lhs.AttackerKnows tr ∧ rhs.AttackerKnows tr

source

def DY.Concat.Concat.invariants [ExecTraceTypes] [ProofTraceTypes] [BytesFunctor] :

Bytes.PartialInvariants SubF

Equations

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

Instances For

source

theorem DY.Concat.Concat.invariantsProofs [ExecTraceTypes] [ProofTraceTypes] [BytesFunctor] [BytesInvariants] :

Bytes.PartialInvariantsProofs invariants

source

theorem DY.Concat.invariantsProofs.internal [BytesFunctor] [ExecTraceTypes] [ProofTraceTypes] [BytesInvariants] (id✝ : Fin 1) :

Bytes.PartialInvariantsProofs (invariants.internal id✝)

source

@[instance_reducible]

def DY.Concat.invariants [BytesFunctor] [ExecTraceTypes] [ProofTraceTypes] :

Bytes.PartialInvariants SubF

Equations

DY.Concat.invariants = DY.Bytes.PartialInvariants.combine DY.Concat.invariants.internal

Instances For

source

def DY.Concat.invariants.internal [BytesFunctor] [ExecTraceTypes] [ProofTraceTypes] (id✝ : Fin 1) :

Bytes.PartialInvariants (SubF.internal id✝)

Equations

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

Instances For

source

theorem DY.Concat.invariantsProofs [BytesFunctor] [ExecTraceTypes] [ProofTraceTypes] [BytesInvariants] :

Bytes.PartialInvariantsProofs invariants

source

@[simp]

theorem DY.Concat.concat.WellFormed [ExecTraceTypes] [ProofTraceTypes] [BytesFunctor] [BytesFunctor.Has SubF] [BytesLength] [BytesWellFormed] [BytesWellFormed.Has Concat.invariants.well_formed] (lhs rhs : Bytes) (tr : ProofTrace) :

(concat lhs rhs).WellFormed tr = (lhs.WellFormed tr ∧ rhs.WellFormed tr)

source

@[simp]

theorem DY.Concat.concat.label [ExecTraceTypes] [ProofTraceTypes] [BytesFunctor] [BytesFunctor.Has SubF] [BytesLength] [BytesInvariants] [BytesInvariants.Has invariants] (lhs rhs : Bytes) (tr : ProofTrace) :

(concat lhs rhs).label tr = (lhs.label tr).meet (rhs.label tr)

source

@[simp]

theorem DY.Concat.concat.Invariant [ExecTraceTypes] [ProofTraceTypes] [BytesFunctor] [BytesFunctor.Has SubF] [BytesLength] [BytesInvariants] [BytesInvariants.Has invariants] (lhs rhs : Bytes) (tr : ProofTrace) :

(concat lhs rhs).Invariant tr = (lhs.Invariant tr ∧ rhs.Invariant tr)

source

@[simp]

theorem DY.Concat.split.WellFormed [ExecTraceTypes] [ProofTraceTypes] [BytesFunctor] [BytesFunctor.Has SubF] [BytesLength] [BytesWellFormed] [BytesWellFormed.Has Concat.invariants.well_formed] (buf : Bytes) (i : Nat) (tr : ProofTrace) :

match split buf i with | none => True | some (lhs, rhs) => buf.WellFormed tr = (lhs.WellFormed tr ∧ rhs.WellFormed tr)

source

@[simp]

theorem DY.Concat.split.label [ExecTraceTypes] [ProofTraceTypes] [BytesFunctor] [BytesFunctor.Has SubF] [BytesLength] [BytesInvariants] [BytesInvariants.Has invariants] (buf : Bytes) (i : Nat) (tr : ProofTrace) :

match split buf i with | none => True | some (lhs, rhs) => buf.label tr = (lhs.label tr).meet (rhs.label tr)

source

@[simp]

theorem DY.Concat.split.Invariant [ExecTraceTypes] [ProofTraceTypes] [BytesFunctor] [BytesFunctor.Has SubF] [BytesLength] [BytesInvariants] [BytesInvariants.Has invariants] (buf : Bytes) (i : Nat) (tr : ProofTrace) :

buf.Invariant tr → match split buf i with | none => True | some (lhs, rhs) => lhs.Invariant tr ∧ rhs.Invariant tr

source

instance DY.Concat.instSubAttackerKnowledgeTheoremSubFAttackerKnowledge [ExecTraceTypes] [ProofTraceTypes] [TraceInvariant] [BytesFunctor] [BytesInvariants] [BytesFunctor.Has SubF] [BytesLength] [BytesInvariants.Has invariants] :

SubAttackerKnowledgeTheorem concat.attackerKnowledge

source

instance DY.Concat.instSubAttackerKnowledgeTheoremSubFAttackerKnowledge_1 [ExecTraceTypes] [ProofTraceTypes] [TraceInvariant] [BytesFunctor] [BytesInvariants] [BytesFunctor.Has SubF] [BytesLength] [BytesInvariants.Has invariants] :

SubAttackerKnowledgeTheorem splitLeft.attackerKnowledge

source

instance DY.Concat.instSubAttackerKnowledgeTheoremSubFAttackerKnowledge_2 [ExecTraceTypes] [ProofTraceTypes] [TraceInvariant] [BytesFunctor] [BytesInvariants] [BytesFunctor.Has SubF] [BytesLength] [BytesInvariants.Has invariants] :

SubAttackerKnowledgeTheorem splitRight.attackerKnowledge