@[reducible, inline]

abbrev DY.BytesWellFormedT [ExecTraceTypes] [ProofTraceTypes] : Type

Equations

• DY.BytesWellFormedT = (DY.ProofTrace → Prop)

class DY.BytesWellFormed [BytesFunctor] [ExecTraceTypes] [ProofTraceTypes] : Type

• funs : Bytes.Function BytesWellFormedT

def DY.Bytes.WellFormed [BytesFunctor] [ExecTraceTypes] [ProofTraceTypes] [BytesWellFormed] (b : Bytes) : BytesWellFormedT

Equations

• b.WellFormed = DY.Bytes.rec DY.BytesWellFormed.funs b

class DY.BytesWellFormed.Has [BytesFunctor] [ExecTraceTypes] [ProofTraceTypes] [BytesWellFormed] {SubF : Type → Type} [SubBytesFunctor SubF] [BytesFunctor.Has SubF] (binv : outParam (Bytes.PartialFunction SubF BytesWellFormedT)) : Prop

• pf : Bytes.SubFunction binv funs

@[simp]

theorem DY.Bytes.WellFormed.eq [BytesFunctor] [ExecTraceTypes] [ProofTraceTypes] {SubF : Type → Type} [SubBytesFunctor SubF] [BytesFunctor.Has SubF] [BytesWellFormed] {binv : PartialFunction SubF BytesWellFormedT} [tc : BytesWellFormed.Has binv] (b : BytesView SubF) (tr : ProofTrace) : b.pack.WellFormed tr = binv b (fun (y : Bytes) (x : sizeOf y ≤ ALaCarte.FunctorSizeOf.sizeOf b) => y.WellFormed) tr

def DY.BytesWellFormedLaterT [ExecTraceTypes] [ProofTraceTypes] (bwf : BytesWellFormedT) : Prop

Equations

• DY.BytesWellFormedLaterT bwf = ∀ (tr1 tr2 : DY.ProofTrace), tr1 ≤ tr2 → bwf tr1 → bwf tr2

class DY.BytesWellFormedLater [BytesFunctor] [ExecTraceTypes] [ProofTraceTypes] [BytesWellFormed] : Prop

• proofs : Bytes.Proof1 BytesWellFormed.funs BytesWellFormedLaterT

theorem DY.Bytes.WellFormed.later [BytesFunctor] [ExecTraceTypes] [ProofTraceTypes] [BytesWellFormed] [BytesWellFormedLater] (b : Bytes) (tr1 tr2 : ProofTrace) : tr1 ≤ tr2 → b.WellFormed tr1 → b.WellFormed tr2

structure DY.Usage [BytesFunctor] : Type

• type : String
• tag : String
• data : Option Bytes

def DY.Usage.nothing [BytesFunctor] : Usage

Equations

• DY.Usage.nothing = { type := "", tag := "", data := none }

@[reducible, inline]

abbrev DY.GetUsageT [BytesFunctor] [ExecTraceTypes] [ProofTraceTypes] : Type

Equations

• DY.GetUsageT = (DY.ProofTrace → DY.Usage)

class DY.GetUsage [BytesFunctor] [ExecTraceTypes] [ProofTraceTypes] : Type

• funs : Bytes.Function GetUsageT

def DY.Bytes.usage [BytesFunctor] [ExecTraceTypes] [ProofTraceTypes] [GetUsage] (b : Bytes) : GetUsageT

Equations

• b.usage = DY.Bytes.rec DY.GetUsage.funs b

class DY.GetUsage.Has [BytesFunctor] [ExecTraceTypes] [ProofTraceTypes] [GetUsage] {SubF : Type → Type} [SubBytesFunctor SubF] [BytesFunctor.Has SubF] (binv : outParam (Bytes.PartialFunction SubF GetUsageT)) : Prop

• pf : Bytes.SubFunction binv funs

@[simp]

theorem DY.Bytes.usage.eq [BytesFunctor] [ExecTraceTypes] [ProofTraceTypes] {SubF : Type → Type} [SubBytesFunctor SubF] [BytesFunctor.Has SubF] [GetUsage] {binv : PartialFunction SubF GetUsageT} [tc : GetUsage.Has binv] (b : BytesView SubF) (tr : ProofTrace) : b.pack.usage tr = binv b (fun (y : Bytes) (x : sizeOf y ≤ ALaCarte.FunctorSizeOf.sizeOf b) => y.usage) tr

def DY.GetUsageLaterT [BytesFunctor] [ExecTraceTypes] [ProofTraceTypes] (x : BytesWellFormedT × GetUsageT) : Prop

Equations

• DY.GetUsageLaterT (wf, usg) = ∀ (tr1 tr2 : DY.ProofTrace), tr1 ≤ tr2 → wf tr1 → usg tr1 = usg tr2

class DY.GetUsageLater [BytesFunctor] [ExecTraceTypes] [ProofTraceTypes] [BytesWellFormed] [GetUsage] : Prop

• proofs : Bytes.Proof2 BytesWellFormed.funs GetUsage.funs GetUsageLaterT

theorem DY.Bytes.usage_later [BytesFunctor] [ExecTraceTypes] [ProofTraceTypes] [BytesWellFormed] [GetUsage] [GetUsageLater] (b : Bytes) (tr1 tr2 : ProofTrace) : tr1 ≤ tr2 → b.WellFormed tr1 → b.usage tr1 = b.usage tr2

@[reducible, inline]

abbrev DY.GetLabelT [ExecTraceTypes] [ProofTraceTypes] : Type

Equations

• DY.GetLabelT = (DY.ProofTrace → DY.Label)

class DY.GetLabel [BytesFunctor] [ExecTraceTypes] [ProofTraceTypes] : Type

• funs : Bytes.Function GetLabelT

def DY.Bytes.label [BytesFunctor] [ExecTraceTypes] [ProofTraceTypes] [GetLabel] (b : Bytes) : GetLabelT

Equations

• b.label = DY.Bytes.rec DY.GetLabel.funs b

class DY.GetLabel.Has [BytesFunctor] [ExecTraceTypes] [ProofTraceTypes] [GetLabel] {SubF : Type → Type} [SubBytesFunctor SubF] [BytesFunctor.Has SubF] (binv : outParam (Bytes.PartialFunction SubF GetLabelT)) : Prop

• pf : Bytes.SubFunction binv funs

@[simp]

theorem DY.Bytes.label.eq [BytesFunctor] [ExecTraceTypes] [ProofTraceTypes] {SubF : Type → Type} [SubBytesFunctor SubF] [BytesFunctor.Has SubF] [GetLabel] {binv : PartialFunction SubF GetLabelT} [tc : GetLabel.Has binv] (b : BytesView SubF) (tr : ProofTrace) : b.pack.label tr = binv b (fun (y : Bytes) (x : sizeOf y ≤ ALaCarte.FunctorSizeOf.sizeOf b) => y.label) tr

def DY.GetLabelLaterT [ExecTraceTypes] [ProofTraceTypes] (x : BytesWellFormedT × GetLabelT) : Prop

Equations

• DY.GetLabelLaterT (wf, usg) = ∀ (tr1 tr2 : DY.ProofTrace), tr1 ≤ tr2 → wf tr1 → usg tr1 = usg tr2

class DY.GetLabelLater [BytesFunctor] [ExecTraceTypes] [ProofTraceTypes] [BytesWellFormed] [GetLabel] : Prop

• proofs : Bytes.Proof2 BytesWellFormed.funs GetLabel.funs GetLabelLaterT

theorem DY.Bytes.label_later [BytesFunctor] [ExecTraceTypes] [ProofTraceTypes] [BytesWellFormed] [GetLabel] [GetLabelLater] (b : Bytes) (tr1 tr2 : ProofTrace) : tr1 ≤ tr2 → b.WellFormed tr1 → b.label tr1 = b.label tr2

@[reducible, inline]

abbrev DY.BytesInvariantT [ExecTraceTypes] [ProofTraceTypes] : Type

Equations

• DY.BytesInvariantT = (DY.ProofTrace → Prop)

class DY.BytesInvariant [BytesFunctor] [ExecTraceTypes] [ProofTraceTypes] : Type

• funs : Bytes.Function BytesInvariantT

def DY.Bytes.Invariant [BytesFunctor] [ExecTraceTypes] [ProofTraceTypes] [BytesInvariant] (b : Bytes) (tr : ProofTrace) : Prop

Equations

• b.Invariant tr = DY.Bytes.rec DY.BytesInvariant.funs b tr

class DY.BytesInvariant.Has [BytesFunctor] [ExecTraceTypes] [ProofTraceTypes] [BytesInvariant] {SubF : Type → Type} [SubBytesFunctor SubF] [BytesFunctor.Has SubF] (binv : outParam (Bytes.PartialFunction SubF BytesInvariantT)) : Prop

• pf : Bytes.SubFunction binv funs

@[simp]

theorem DY.Bytes.Invariant.eq [BytesFunctor] [ExecTraceTypes] [ProofTraceTypes] {SubF : Type → Type} [SubBytesFunctor SubF] [BytesFunctor.Has SubF] [BytesInvariant] {binv : PartialFunction SubF BytesInvariantT} [tc : BytesInvariant.Has binv] (b : BytesView SubF) (tr : ProofTrace) : b.pack.Invariant tr = binv b (fun (y : Bytes) (x : sizeOf y ≤ ALaCarte.FunctorSizeOf.sizeOf b) => y.Invariant) tr

def DY.BytesInvariantImpliesBytesWellFormedT [ExecTraceTypes] [ProofTraceTypes] (x : BytesInvariantT × BytesWellFormedT) : Prop

Equations

• DY.BytesInvariantImpliesBytesWellFormedT (binv, bwf) = ∀ (tr : DY.ProofTrace), binv tr → bwf tr

class DY.BytesInvariantImpliesBytesWellFormed [BytesFunctor] [ExecTraceTypes] [ProofTraceTypes] [BytesWellFormed] [BytesInvariant] : Prop

• proofs : Bytes.Proof2 BytesInvariant.funs BytesWellFormed.funs BytesInvariantImpliesBytesWellFormedT

theorem DY.Bytes.Invariant_implies_WellFormed [BytesFunctor] [ExecTraceTypes] [ProofTraceTypes] [BytesWellFormed] [BytesInvariant] [BytesInvariantImpliesBytesWellFormed] (b : Bytes) (tr : ProofTrace) : b.Invariant tr → b.WellFormed tr

def DY.BytesInvariantLaterT [ExecTraceTypes] [ProofTraceTypes] (binv : BytesInvariantT) : Prop

Equations

• DY.BytesInvariantLaterT binv = ∀ (tr1 tr2 : DY.ProofTrace), tr1 ≤ tr2 → binv tr1 → binv tr2

class DY.BytesInvariantLater [BytesFunctor] [ExecTraceTypes] [ProofTraceTypes] [BytesInvariant] : Prop

• proofs : Bytes.Proof1 BytesInvariant.funs BytesInvariantLaterT

theorem DY.Bytes.Invariant.later [BytesFunctor] [ExecTraceTypes] [ProofTraceTypes] [BytesInvariant] [BytesInvariantLater] (b : Bytes) (tr1 tr2 : ProofTrace) : tr1 ≤ tr2 → b.Invariant tr1 → b.Invariant tr2

structure DY.Bytes.PartialInvariants [BytesFunctor] [ExecTraceTypes] [ProofTraceTypes] (SubF : Type → Type) [SubBytesFunctor SubF] : Type

To reduce the boilerplate required to combine all (sub-)invariants, we bundle them into this structure, so that instead of having to combine each function separately, we can simply combine this bundle of functions. However, such a bundling prevents e.g. the definition of invariant to assume that well_formed is constructed in some particular way (e.g. that it contains some Pk invariants). Later on we will define properties on these (sub-)invariants: we do not bundle them here because in these proofs we want to be able to assume a particular implementation of well_formed.

• well_formed : PartialFunction SubF BytesWellFormedT
• usage : PartialFunction SubF GetUsageT
• label [GetUsage] : PartialFunction SubF GetLabelT
• invariant [BytesWellFormed] [GetUsage] [GetLabel] : PartialFunction SubF BytesInvariantT

class DY.BytesInvariants [BytesFunctor] [ExecTraceTypes] [ProofTraceTypes] : Type

• invs : Bytes.PartialInvariants BytesF

@[instance_reducible]

instance DY.instBytesWellFormedOfBytesInvariants [BytesFunctor] [ExecTraceTypes] [ProofTraceTypes] [BytesInvariants] : BytesWellFormed

Equations

• DY.instBytesWellFormedOfBytesInvariants = { funs := DY.BytesInvariants.invs.well_formed }

@[instance_reducible]

instance DY.instGetUsageOfBytesInvariants [BytesFunctor] [ExecTraceTypes] [ProofTraceTypes] [BytesInvariants] : GetUsage

Equations

• DY.instGetUsageOfBytesInvariants = { funs := DY.BytesInvariants.invs.usage }

@[instance_reducible]

instance DY.instGetLabelOfBytesInvariants [BytesFunctor] [ExecTraceTypes] [ProofTraceTypes] [BytesInvariants] : GetLabel

Equations

• DY.instGetLabelOfBytesInvariants = { funs := DY.BytesInvariants.invs.label }

@[instance_reducible]

instance DY.instBytesInvariantOfBytesInvariants [BytesFunctor] [ExecTraceTypes] [ProofTraceTypes] [BytesInvariants] : BytesInvariant

Equations

• DY.instBytesInvariantOfBytesInvariants = { funs := DY.BytesInvariants.invs.invariant }

structure DY.Bytes.PartialInvariantsProofs [BytesFunctor] [ExecTraceTypes] [ProofTraceTypes] [BytesInvariants] {SubF : Type → Type} [SubBytesFunctor SubF] (invs : PartialInvariants SubF) : Prop

• well_formed_later : PartialProof1 invs.well_formed WellFormed BytesWellFormedLaterT
• usage_later : PartialProof2 invs.well_formed invs.usage WellFormed usage GetUsageLaterT
• label_later [GetUsageLater] : PartialProof2 invs.well_formed invs.label WellFormed label GetLabelLaterT
• invariant_implies_wellformed : PartialProof2 invs.invariant invs.well_formed Invariant WellFormed BytesInvariantImpliesBytesWellFormedT
• invariant_later [BytesWellFormedLater] [GetUsageLater] [GetLabelLater] [BytesInvariantImpliesBytesWellFormed] : PartialProof1 invs.invariant Invariant BytesInvariantLaterT

class DY.BytesInvariantsProofs [BytesFunctor] [ExecTraceTypes] [ProofTraceTypes] [BytesInvariants] : Prop

• pfs : Bytes.PartialInvariantsProofs BytesInvariants.invs

instance DY.instBytesWellFormedLaterOfBytesInvariantsProofs [BytesFunctor] [ExecTraceTypes] [ProofTraceTypes] [BytesInvariants] [BytesInvariantsProofs] : BytesWellFormedLater

instance DY.instGetUsageLaterOfBytesInvariantsProofs [BytesFunctor] [ExecTraceTypes] [ProofTraceTypes] [BytesInvariants] [BytesInvariantsProofs] : GetUsageLater

instance DY.instGetLabelLaterOfBytesInvariantsProofs [BytesFunctor] [ExecTraceTypes] [ProofTraceTypes] [BytesInvariants] [BytesInvariantsProofs] : GetLabelLater

instance DY.instBytesInvariantImpliesBytesWellFormedOfBytesInvariantsProofs [BytesFunctor] [ExecTraceTypes] [ProofTraceTypes] [BytesInvariants] [BytesInvariantsProofs] : BytesInvariantImpliesBytesWellFormed

instance DY.instBytesInvariantLaterOfBytesInvariantsProofs [BytesFunctor] [ExecTraceTypes] [ProofTraceTypes] [BytesInvariants] [BytesInvariantsProofs] : BytesInvariantLater

class DY.BytesInvariants.HasStep [BytesFunctor] [ExecTraceTypes] [ProofTraceTypes] [BytesInvariants] {SubF1 SubF2 : Type → Type} [SubBytesFunctor SubF1] [SubBytesFunctor SubF2] [BytesFunctor.HasStep SubF1 SubF2] (partialInvs1 : outParam (Bytes.PartialInvariants SubF1)) (partialInvs2 : Bytes.PartialInvariants SubF2) : Prop

• well_formed_sub : Bytes.SubFunctionStep partialInvs1.well_formed partialInvs2.well_formed
• usage_sub : Bytes.SubFunctionStep partialInvs1.usage partialInvs2.usage
• label_sub : Bytes.SubFunctionStep partialInvs1.label partialInvs2.label
• invariant_sub : Bytes.SubFunctionStep partialInvs1.invariant partialInvs2.invariant

class DY.BytesInvariants.Has [BytesFunctor] [ExecTraceTypes] [ProofTraceTypes] [BytesInvariants] {SubF : Type → Type} [SubBytesFunctor SubF] [BytesFunctor.Has SubF] (partialInvs : outParam (Bytes.PartialInvariants SubF)) : Prop

• well_formed_sub : Bytes.SubFunction partialInvs.well_formed BytesWellFormed.funs
• usage_sub : Bytes.SubFunction partialInvs.usage GetUsage.funs
• label_sub : Bytes.SubFunction partialInvs.label GetLabel.funs
• invariant_sub : Bytes.SubFunction partialInvs.invariant BytesInvariant.funs

def DY.Bytes.PartialInvariants.combine [BytesFunctor] [ExecTraceTypes] [ProofTraceTypes] {t : Type} [DecidableEq t] [Ord t] [Std.LawfulEqOrd t] [Std.TransOrd t] {SubFs : t → Type → Type} [(id : t) → SubBytesFunctor (SubFs id)] (invs : (id : t) → PartialInvariants (SubFs id)) : PartialInvariants (BytesFunctor.combine SubFs)

Equations

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

theorem DY.Bytes.PartialInvariantsProofs.combine [BytesFunctor] [ExecTraceTypes] [ProofTraceTypes] [BytesInvariants] {t : Type} [DecidableEq t] [Ord t] [Std.LawfulEqOrd t] [Std.TransOrd t] {SubFs : t → Type → Type} [(id : t) → SubBytesFunctor (SubFs id)] {invs : (id : t) → PartialInvariants (SubFs id)} (pfs : ∀ (id : t), PartialInvariantsProofs (invs id)) : PartialInvariantsProofs (PartialInvariants.combine invs)

instance DY.BytesInvariants.instHasBytesFInvs [BytesFunctor] [ExecTraceTypes] [ProofTraceTypes] [BytesInvariants] : Has invs

instance DY.BytesInvariants.instHasOfHasStep [BytesFunctor] [ExecTraceTypes] [ProofTraceTypes] [BytesInvariants] {SubF1 SubF2 : Type → Type} [SubBytesFunctor SubF1] [SubBytesFunctor SubF2] [BytesFunctor.HasStep SubF1 SubF2] [BytesFunctor.Has SubF2] (partialInvs1 : Bytes.PartialInvariants SubF1) (partialInvs2 : Bytes.PartialInvariants SubF2) [inst1 : HasStep partialInvs1 partialInvs2] [inst2 : Has partialInvs2] : Has partialInvs1

instance DY.BytesInvariants.instHasStepCombineCombine [BytesFunctor] [ExecTraceTypes] [ProofTraceTypes] [BytesInvariants] {t : Type} [DecidableEq t] [Ord t] [Std.LawfulEqOrd t] [Std.TransOrd t] (SubFs : t → Type → Type) [(id : t) → SubBytesFunctor (SubFs id)] (invs : (id : t) → Bytes.PartialInvariants (SubFs id)) (id : t) : HasStep (invs id) (Bytes.PartialInvariants.combine invs)

instance DY.BytesInvariants.instHasWell_formedOfHas [BytesFunctor] [ExecTraceTypes] [ProofTraceTypes] [BytesInvariants] {SubF : Type → Type} [SubBytesFunctor SubF] [BytesFunctor.Has SubF] (invs : Bytes.PartialInvariants SubF) [tc : Has invs] : BytesWellFormed.Has invs.well_formed

instance DY.BytesInvariants.instHasUsageOfHas [BytesFunctor] [ExecTraceTypes] [ProofTraceTypes] [BytesInvariants] {SubF : Type → Type} [SubBytesFunctor SubF] [BytesFunctor.Has SubF] (invs : Bytes.PartialInvariants SubF) [tc : Has invs] : GetUsage.Has invs.usage

instance DY.BytesInvariants.instHasLabelOfHas [BytesFunctor] [ExecTraceTypes] [ProofTraceTypes] [BytesInvariants] {SubF : Type → Type} [SubBytesFunctor SubF] [BytesFunctor.Has SubF] (invs : Bytes.PartialInvariants SubF) [tc : Has invs] : GetLabel.Has invs.label

instance DY.BytesInvariants.instHasInvariantOfHas [BytesFunctor] [ExecTraceTypes] [ProofTraceTypes] [BytesInvariants] {SubF : Type → Type} [SubBytesFunctor SubF] [BytesFunctor.Has SubF] (invs : Bytes.PartialInvariants SubF) [tc : Has invs] : BytesInvariant.Has invs.invariant

def DY.Bytes.Publishable [BytesFunctor] [ExecTraceTypes] [ProofTraceTypes] [BytesInvariants] (b : Bytes) (tr : ProofTrace) : Prop

Equations

• b.Publishable tr = (b.Invariant tr ∧ (b.label tr).canFlow DY.Label.pub (DY.Trace.erase tr))

def DY.Bytes.KnowableBy [BytesFunctor] [ExecTraceTypes] [ProofTraceTypes] [BytesInvariants] (l : Label) (b : Bytes) (tr : ProofTrace) : Prop

Equations

• DY.Bytes.KnowableBy l b tr = (b.Invariant tr ∧ (b.label tr).canFlow l (DY.Trace.erase tr))

def DY.Bytes.HasUsage [BytesFunctor] [ExecTraceTypes] [ProofTraceTypes] [GetUsage] [GetLabel] (b : Bytes) (usg : Usage) (tr : ProofTrace) : Prop

Equations

• b.HasUsage usg tr = (b.usage tr = usg ∨ (b.label tr).canFlow DY.Label.pub (DY.Trace.erase tr))

theorem DY.Bytes.HasUsage_later [BytesFunctor] [ExecTraceTypes] [ProofTraceTypes] [BytesWellFormed] [GetUsage] [GetUsageLater] [GetLabel] [GetLabelLater] (b : Bytes) (usg : Usage) (tr1 tr2 : ProofTrace) : b.WellFormed tr1 → tr1 ≤ tr2 → b.HasUsage usg tr1 → b.HasUsage usg tr2

theorem DY.Bytes.HasUsage_inj [BytesFunctor] [ExecTraceTypes] [ProofTraceTypes] [BytesWellFormed] [GetUsage] [GetLabel] (b : Bytes) (usg1 usg2 : Usage) (tr : ProofTrace) : b.HasUsage usg1 tr → b.HasUsage usg2 tr → usg1 = usg2 ∨ (b.label tr).canFlow Label.pub (Trace.erase tr)

theorem DY.Bytes.HasUsage_public [BytesFunctor] [ExecTraceTypes] [ProofTraceTypes] [BytesWellFormed] [GetUsage] [GetLabel] (b : Bytes) (usg : Usage) (tr : ProofTrace) : (b.label tr).canFlow Label.pub (Trace.erase tr) → b.HasUsage usg tr

def DY.Bytes.xxxLabel [BytesFunctor] [ExecTraceTypes] [ProofTraceTypes] [GetLabel] (extract : Bytes → Option Bytes) (b : Bytes) (tr : ProofTrace) : Label

Equations

• DY.Bytes.xxxLabel extract b tr = match extract b with | some sk => sk.label tr | none => DY.Label.pub

def DY.Bytes.XXXHasUsage [BytesFunctor] [ExecTraceTypes] [ProofTraceTypes] [GetUsage] [GetLabel] (extract : Bytes → Option Bytes) (b : Bytes) (usg : Usage) (tr : ProofTrace) : Prop

Equations

• DY.Bytes.XXXHasUsage extract b usg tr = match extract b with | some sk => sk.HasUsage usg tr | none => True

def DY.ExtractPreservesWellFormed [BytesFunctor] [ExecTraceTypes] [ProofTraceTypes] [BytesWellFormed] (extract : Bytes → Option Bytes) : Prop

Equations

• DY.ExtractPreservesWellFormed extract = ∀ (b : DY.Bytes) (tr : DY.ProofTrace), b.WellFormed tr → match extract b with | some b' => b'.WellFormed tr | none => True

theorem DY.Bytes.xxxLabel_later [BytesFunctor] [ExecTraceTypes] [ProofTraceTypes] [BytesWellFormed] [GetLabel] [GetLabelLater] (extract : Bytes → Option Bytes) (h_extract : ExtractPreservesWellFormed extract) (b : Bytes) (tr1 tr2 : ProofTrace) : b.WellFormed tr1 → tr1 ≤ tr2 → xxxLabel extract b tr1 = xxxLabel extract b tr2

theorem DY.Bytes.XXXHasUsage_later [BytesFunctor] [ExecTraceTypes] [ProofTraceTypes] [BytesWellFormed] [GetUsage] [GetUsageLater] [GetLabel] [GetLabelLater] (extract : Bytes → Option Bytes) (h_extract : ExtractPreservesWellFormed extract) (b : Bytes) (usg : Usage) (tr1 tr2 : ProofTrace) : b.WellFormed tr1 → tr1 ≤ tr2 → XXXHasUsage extract b usg tr1 → XXXHasUsage extract b usg tr2

theorem DY.Bytes.usage_later_fast [BytesFunctor] [ExecTraceTypes] [ProofTraceTypes] [BytesInvariants] [BytesInvariantsProofs] (b : Bytes) (tr1 tr2 : ProofTrace) : tr1 ≤ tr2 → b.Invariant tr1 → b.usage tr1 = b.usage tr2

theorem DY.Bytes.label_later_fast [BytesFunctor] [ExecTraceTypes] [ProofTraceTypes] [BytesInvariants] [BytesInvariantsProofs] (b : Bytes) (tr1 tr2 : ProofTrace) : tr1 ≤ tr2 → b.Invariant tr1 → b.label tr1 = b.label tr2

theorem DY.Bytes.Invariant.later_fast [BytesFunctor] [ExecTraceTypes] [ProofTraceTypes] [BytesInvariants] [BytesInvariantsProofs] (b : Bytes) (tr1 tr2 : ProofTrace) : tr1 ≤ tr2 → b.Invariant tr1 → b.Invariant tr2

theorem DY.Bytes.Publishable_later_fast [BytesFunctor] [ExecTraceTypes] [ProofTraceTypes] [BytesInvariants] [BytesInvariantsProofs] (b : Bytes) (tr1 tr2 : ProofTrace) : tr1 ≤ tr2 → b.Publishable tr1 → b.Publishable tr2

theorem DY.Bytes.Publishable_imp_Invariant_fast [BytesFunctor] [ExecTraceTypes] [ProofTraceTypes] [BytesInvariants] [BytesInvariantsProofs] (b : Bytes) (tr : ProofTrace) : b.Publishable tr → b.Invariant tr

theorem DY.Bytes.HasUsage_later_fast [BytesFunctor] [ExecTraceTypes] [ProofTraceTypes] [BytesInvariants] [BytesInvariantsProofs] (b : Bytes) (usg : Usage) (tr1 tr2 : ProofTrace) : b.Invariant tr1 → tr1 ≤ tr2 → b.HasUsage usg tr1 → b.HasUsage usg tr2