@[instance_reducible]

instance DY.Comparse.instBytesLikeBytes [BytesFunctor] [BytesLength] [BytesFunctor.Has Literal.SubF] [BytesLength.Has Literal.SubF.length] [BytesFunctor.Has Concat.SubF] [BytesLength.Has Concat.SubF.length] : Comparse.BytesLike Bytes

Equations

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

class DY.Comparse.ParseableSerializeable [BytesFunctor] [BytesLength] [BytesFunctor.Has Literal.SubF] [BytesLength.Has Literal.SubF.length] [BytesFunctor.Has Concat.SubF] [BytesLength.Has Concat.SubF.length] (a : Type) : Type

• mf : Comparse.ExtensibleMessageFormat Bytes a
• mf_na : mf.IsNonAmbiguous
• mf_ur : mf.HasUniqueRepresentation

class DY.Comparse.ParseableSerializeableNE [BytesFunctor] [BytesLength] [BytesFunctor.Has Literal.SubF] [BytesLength.Has Literal.SubF.length] [BytesFunctor.Has Concat.SubF] [BytesLength.Has Concat.SubF.length] (a : Type) : Type

• mf : Comparse.NonExtensibleMessageFormat Bytes a
• mf_na : mf.IsNonAmbiguous
• mf_ur : mf.HasUniqueRepresentation

@[instance_reducible]

instance DY.Comparse.instParseableSerializeableOfParseableSerializeableNE [BytesFunctor] [BytesLength] [BytesFunctor.Has Literal.SubF] [BytesLength.Has Literal.SubF.length] [BytesFunctor.Has Concat.SubF] [BytesLength.Has Concat.SubF.length] (a : Type) [inst : ParseableSerializeableNE a] : ParseableSerializeable a

Equations

• DY.Comparse.instParseableSerializeableOfParseableSerializeableNE a = { mf := DY.Comparse.ParseableSerializeableNE.mf.toExtensible, mf_na := ⋯, mf_ur := ⋯ }

def DY.Comparse.parse [BytesFunctor] [BytesLength] [BytesFunctor.Has Literal.SubF] [BytesLength.Has Literal.SubF.length] [BytesFunctor.Has Concat.SubF] [BytesLength.Has Concat.SubF.length] {a : Type} [ParseableSerializeable a] (buf : Bytes) : Err a

Equations

• DY.Comparse.parse buf = DY.Comparse.ParseableSerializeable.mf.parse buf

def DY.Comparse.serialize [BytesFunctor] [BytesLength] [BytesFunctor.Has Literal.SubF] [BytesLength.Has Literal.SubF.length] [BytesFunctor.Has Concat.SubF] [BytesLength.Has Concat.SubF.length] {a : Type} [ParseableSerializeable a] (x : a) : Bytes

Equations

• DY.Comparse.serialize x = DY.Comparse.ParseableSerializeable.mf.serialize x

@[simp]

theorem DY.Comparse.parse_serialize_inv [BytesFunctor] [BytesLength] [BytesFunctor.Has Literal.SubF] [BytesLength.Has Literal.SubF.length] [BytesFunctor.Has Concat.SubF] [BytesLength.Has Concat.SubF.length] {a : Type} [ParseableSerializeable a] (x : a) : parse (serialize x) = some x

theorem DY.Comparse.serialize_injective [BytesFunctor] [BytesLength] [BytesFunctor.Has Literal.SubF] [BytesLength.Has Literal.SubF.length] [BytesFunctor.Has Concat.SubF] [BytesLength.Has Concat.SubF.length] {a : Type} [ParseableSerializeable a] : Function.Injective serialize

@[reducible, inline]

abbrev DY.Comparse.ParseableSerializeable.make [BytesFunctor] [BytesLength] [BytesFunctor.Has Literal.SubF] [BytesLength.Has Literal.SubF.length] [BytesFunctor.Has Concat.SubF] [BytesLength.Has Concat.SubF.length] {a : Type} (mf : Comparse.ExtensibleMessageFormat Bytes a) [mf.IsNonAmbiguous] [mf.HasUniqueRepresentation] : ParseableSerializeable a

Equations

• DY.Comparse.ParseableSerializeable.make mf = { mf := mf, mf_na := inst✝¹, mf_ur := inst✝ }

@[reducible, inline]

abbrev DY.Comparse.ParseableSerializeableNE.make [BytesFunctor] [BytesLength] [BytesFunctor.Has Literal.SubF] [BytesLength.Has Literal.SubF.length] [BytesFunctor.Has Concat.SubF] [BytesLength.Has Concat.SubF.length] {a : Type} (mf : Comparse.NonExtensibleMessageFormat Bytes a) [mf.IsNonAmbiguous] [mf.HasUniqueRepresentation] : ParseableSerializeableNE a

Equations

• DY.Comparse.ParseableSerializeableNE.make mf = { mf := mf, mf_na := inst✝¹, mf_ur := inst✝ }

def DY.Comparse.FormatRel [BytesFunctor] [BytesLength] [BytesFunctor.Has Literal.SubF] [BytesLength.Has Literal.SubF.length] [BytesFunctor.Has Concat.SubF] [BytesLength.Has Concat.SubF.length] {a : Type} [ParseableSerializeable a] (buf : Bytes) (x : a) : Prop

Equations

• DY.Comparse.FormatRel buf x = (buf = DY.Comparse.serialize x)

instance DY.Comparse.instHoareTripleErrParseTrueFormatRel [BytesFunctor] [BytesLength] [BytesFunctor.Has Literal.SubF] [BytesLength.Has Literal.SubF.length] [BytesFunctor.Has Concat.SubF] [BytesLength.Has Concat.SubF.length] {a : Type} {buf : Bytes} [ExecTraceTypes] [ProofTraceTypes] [TraceInvariant] [ParseableSerializeable a] : HoareTriple (parse buf) (fun (x : ProofTrace) => True) fun (res : a) (x : ProofTrace) => FormatRel buf res

theorem DY.Comparse.serialize_FormatRel [BytesFunctor] [BytesLength] [BytesFunctor.Has Literal.SubF] [BytesLength.Has Literal.SubF.length] [BytesFunctor.Has Concat.SubF] [BytesLength.Has Concat.SubF.length] {a : Type} [ParseableSerializeable a] (x : a) : FormatRel (serialize x) x

theorem DY.Comparse.parse_FormatRel [BytesFunctor] [BytesLength] [BytesFunctor.Has Literal.SubF] [BytesLength.Has Literal.SubF.length] [BytesFunctor.Has Concat.SubF] [BytesLength.Has Concat.SubF.length] {a : Type} [ParseableSerializeable a] (b : Bytes) : match parse b with | none => True | some x => FormatRel b x

class DY.Comparse.BytesCompatibleTracePred [BytesFunctor] [BytesLength] [BytesFunctor.Has Literal.SubF] [BytesLength.Has Literal.SubF.length] [BytesFunctor.Has Concat.SubF] [BytesLength.Has Concat.SubF.length] {τ : Sort u_1} (pre : Bytes → τ → Prop) : Prop

• pf (tr : τ) : Comparse.BytesCompatiblePred fun (x : Bytes) => pre x tr

instance DY.Comparse.instBytesCompatiblePredBytesOfBytesCompatibleTracePred [BytesFunctor] [BytesLength] [BytesFunctor.Has Literal.SubF] [BytesLength.Has Literal.SubF.length] [BytesFunctor.Has Concat.SubF] [BytesLength.Has Concat.SubF.length] {τ : Sort u_1} (pre : Bytes → τ → Prop) [inst : BytesCompatibleTracePred pre] (tr : τ) : Comparse.BytesCompatiblePred fun (x : Bytes) => pre x tr

instance DY.Comparse.instBytesCompatibleTracePredExecTraceAttackerKnowsOfSubFAttackerKnowledgeOfHasSubFAttackerKnowledge [BytesFunctor] [BytesLength] [BytesFunctor.Has Literal.SubF] [BytesLength.Has Literal.SubF.length] [BytesFunctor.Has Concat.SubF] [BytesLength.Has Concat.SubF.length] [ExecTraceTypes] [BaseAttackerKnowledge] [AttackerKnowledge] [AttackerKnowledge.Has Literal.attackerKnowledge] [AttackerKnowledge.Has Concat.attackerKnowledge] : BytesCompatibleTracePred Bytes.AttackerKnows

def DY.Comparse.IsWellFormed [BytesFunctor] [BytesLength] [BytesFunctor.Has Literal.SubF] [BytesLength.Has Literal.SubF.length] [BytesFunctor.Has Concat.SubF] [BytesLength.Has Concat.SubF.length] {a : Type} {τ : Sort u_1} [ParseableSerializeable a] (pre : Bytes → τ → Prop) (x : a) (tr : τ) : Prop

Equations

• DY.Comparse.IsWellFormed pre x tr = DY.Comparse.ParseableSerializeable.mf.wf (fun (x : DY.Bytes) => pre x tr) x

theorem DY.Comparse.IsWellFormed_FormatRel [BytesFunctor] [BytesLength] [BytesFunctor.Has Literal.SubF] [BytesLength.Has Literal.SubF.length] [BytesFunctor.Has Concat.SubF] [BytesLength.Has Concat.SubF.length] {a : Type} {τ : Sort u_1} [ParseableSerializeable a] (pre : Bytes → τ → Prop) (buf : Bytes) (x : a) (tr : τ) : FormatRel buf x → pre buf tr = IsWellFormed pre x tr

theorem DY.Comparse.IsWellFormed_FormatRel_WellFormed [BytesFunctor] [BytesLength] [BytesFunctor.Has Literal.SubF] [BytesLength.Has Literal.SubF.length] [BytesFunctor.Has Concat.SubF] [BytesLength.Has Concat.SubF.length] {a : Type} [ExecTraceTypes] [ProofTraceTypes] [BytesWellFormed] [ParseableSerializeable a] (buf : Bytes) (x : a) (tr : ProofTrace) : FormatRel buf x → buf.WellFormed tr = IsWellFormed Bytes.WellFormed x tr

@[simp]

theorem DY.Comparse.WellFormed_serialize [BytesFunctor] [BytesLength] [BytesFunctor.Has Literal.SubF] [BytesLength.Has Literal.SubF.length] [BytesFunctor.Has Concat.SubF] [BytesLength.Has Concat.SubF.length] {a : Type} [ExecTraceTypes] [ProofTraceTypes] [BytesWellFormed] [ParseableSerializeable a] (x : a) (tr : ProofTrace) : (serialize x).WellFormed tr = IsWellFormed Bytes.WellFormed x tr

theorem DY.Comparse.IsWellFormed_FormatRel_Invariant [BytesFunctor] [BytesLength] [BytesFunctor.Has Literal.SubF] [BytesLength.Has Literal.SubF.length] [BytesFunctor.Has Concat.SubF] [BytesLength.Has Concat.SubF.length] {a : Type} [ExecTraceTypes] [ProofTraceTypes] [BytesInvariant] [ParseableSerializeable a] (buf : Bytes) (x : a) (tr : ProofTrace) : FormatRel buf x → buf.Invariant tr = IsWellFormed Bytes.Invariant x tr

@[simp]

theorem DY.Comparse.Invariant_serialize [BytesFunctor] [BytesLength] [BytesFunctor.Has Literal.SubF] [BytesLength.Has Literal.SubF.length] [BytesFunctor.Has Concat.SubF] [BytesLength.Has Concat.SubF.length] {a : Type} [ExecTraceTypes] [ProofTraceTypes] [BytesInvariants] [ParseableSerializeable a] (x : a) (tr : ProofTrace) : (serialize x).Invariant tr = IsWellFormed Bytes.Invariant x tr

theorem DY.Comparse.IsWellFormed_FormatRel_Publishable [BytesFunctor] [BytesLength] [BytesFunctor.Has Literal.SubF] [BytesLength.Has Literal.SubF.length] [BytesFunctor.Has Concat.SubF] [BytesLength.Has Concat.SubF.length] {a : Type} [ExecTraceTypes] [ProofTraceTypes] [BytesInvariants] [ParseableSerializeable a] (buf : Bytes) (x : a) (tr : ProofTrace) : FormatRel buf x → buf.Publishable tr = IsWellFormed Bytes.Publishable x tr

@[simp]

theorem DY.Comparse.Publishable_serialize [BytesFunctor] [BytesLength] [BytesFunctor.Has Literal.SubF] [BytesLength.Has Literal.SubF.length] [BytesFunctor.Has Concat.SubF] [BytesLength.Has Concat.SubF.length] {a : Type} [ExecTraceTypes] [ProofTraceTypes] [BytesInvariants] [ParseableSerializeable a] (x : a) (tr : ProofTrace) : (serialize x).Publishable tr = IsWellFormed Bytes.Publishable x tr

theorem DY.Comparse.IsWellFormed_FormatRel_AttackerKnows [BytesFunctor] [BytesLength] [BytesFunctor.Has Literal.SubF] [BytesLength.Has Literal.SubF.length] [BytesFunctor.Has Concat.SubF] [BytesLength.Has Concat.SubF.length] {a : Type} [ExecTraceTypes] [BaseAttackerKnowledge] [AttackerKnowledge] [ParseableSerializeable a] (buf : Bytes) (x : a) (tr : ExecTrace) : FormatRel buf x → buf.AttackerKnows tr = IsWellFormed Bytes.AttackerKnows x tr

@[simp]

theorem DY.Comparse.AttackerKnows_serialize [BytesFunctor] [BytesLength] [BytesFunctor.Has Literal.SubF] [BytesLength.Has Literal.SubF.length] [BytesFunctor.Has Concat.SubF] [BytesLength.Has Concat.SubF.length] {a : Type} [ExecTraceTypes] [BaseAttackerKnowledge] [AttackerKnowledge] [ParseableSerializeable a] (x : a) (tr : ExecTrace) : (serialize x).AttackerKnows tr = IsWellFormed Bytes.AttackerKnows x tr