class DY.SubBytesFunctor (SubF : Type → Type) : Type 1

• sizeOf : ALaCarte.FunctorSizeOf SubF
• repr : ALaCarte.Representable SubF
• deq : ALaCarte.RepresentableDecidableEq SubF
• ord : ALaCarte.RepresentableOrd SubF

@[instance_reducible]

instance DY.instFunctorSizeOfOfSubBytesFunctor (SubF : Type → Type) [inst : SubBytesFunctor SubF] : ALaCarte.FunctorSizeOf SubF

Equations

• DY.instFunctorSizeOfOfSubBytesFunctor SubF = DY.SubBytesFunctor.sizeOf

@[instance_reducible]

instance DY.instRepresentable (SubF : Type → Type) [inst : SubBytesFunctor SubF] : ALaCarte.Representable SubF

Equations

• DY.instRepresentable SubF = DY.SubBytesFunctor.repr

@[instance_reducible]

instance DY.instRepresentableDecidableEq (SubF : Type → Type) [inst : SubBytesFunctor SubF] : ALaCarte.RepresentableDecidableEq SubF

Equations

• DY.instRepresentableDecidableEq SubF = DY.SubBytesFunctor.deq

@[instance_reducible]

instance DY.instRepresentableOrd (SubF : Type → Type) [inst : SubBytesFunctor SubF] : ALaCarte.RepresentableOrd SubF

Equations

• DY.instRepresentableOrd SubF = DY.SubBytesFunctor.ord

class DY.BytesFunctor : Type 1

• BytesF : Type → Type
• inst : SubBytesFunctor BytesF

@[instance_reducible]

instance DY.instSubBytesFunctorBytesF [inst : BytesFunctor] : SubBytesFunctor BytesF

Equations

• DY.instSubBytesFunctorBytesF = DY.BytesFunctor.inst

@[irreducible]

def DY.Bytes [BytesFunctor] : Type

Equations

• DY.Bytes = DY.ALaCarte.ContainerFor DY.BytesF

@[instance_reducible]

noncomputable instance DY.instSizeOfBytes [BytesFunctor] : SizeOf Bytes

Equations

• DY.instSizeOfBytes = { sizeOf := DY.instSizeOfBytes._aux_1 }

@[instance_reducible]

instance DY.instDecidableEqBytes [BytesFunctor] : DecidableEq Bytes

Equations

• DY.instDecidableEqBytes = DY.instDecidableEqBytes._aux_1

@[instance_reducible]

instance DY.instOrdBytes [BytesFunctor] : Ord Bytes

Equations

• DY.instOrdBytes = { compare := DY.instOrdBytes._aux_1 }

instance DY.instReflOrdBytes [BytesFunctor] : Std.ReflOrd Bytes

instance DY.instLawfulEqOrdBytes [BytesFunctor] : Std.LawfulEqOrd Bytes

instance DY.instOrientedOrdBytes [BytesFunctor] : Std.OrientedOrd Bytes

instance DY.instTransOrdBytes [BytesFunctor] : Std.TransOrd Bytes

@[instance_reducible]

instance DY.instLEBytes [BytesFunctor] : LE Bytes

Equations

• DY.instLEBytes = LE.ofOrd DY.Bytes

instance DY.instIsLinearOrderBytes [BytesFunctor] : Std.IsLinearOrder Bytes

class DY.BytesFunctor.HasStep (SubF1 : Type → Type) (SubF2 : semiOutParam (Type → Type)) [SubBytesFunctor SubF1] [semiOutParam (SubBytesFunctor SubF2)] extends DY.ALaCarte.SubFunctor SubF1 SubF2 : Type 1

• inj {a : Type} : SubF1 a → SubF2 a
• proj {a : Type} : SubF2 a → Option (SubF1 a)
• proj_inj {a : Type} (x : SubF1 a) : proj (inj x) = some x
• inj_proj {a : Type} (x : SubF2 a) : match proj x with | some y => inj y = x | none => True
• sizeOf_inj {a : Type} [SizeOf a] (x : SubF1 a) : FunctorSizeOf.sizeOf (inj x) = FunctorSizeOf.sizeOf x

class DY.BytesFunctor.Has [BytesFunctor] (SubF : Type → Type) [SubBytesFunctor SubF] extends DY.ALaCarte.SubFunctorTC SubF DY.BytesF : Type 1

• inj {a : Type} : SubF a → BytesF a
• proj {a : Type} : BytesF a → Option (SubF a)
• proj_inj {a : Type} (x : SubF a) : proj (inj x) = some x
• inj_proj {a : Type} (x : BytesF a) : match proj x with | some y => inj y = x | none => True
• sizeOf_inj {a : Type} [SizeOf a] (x : SubF a) : FunctorSizeOf.sizeOf (inj x) = FunctorSizeOf.sizeOf x

@[instance_reducible]

instance DY.BytesFunctor.instHasBytesF [BytesFunctor] : Has BytesF

Equations

• DY.BytesFunctor.instHasBytesF = { toSubFunctorTC := DY.ALaCarte.instSubFunctorTC DY.BytesF }

@[instance_reducible]

instance DY.BytesFunctor.instHasOfHasStep [BytesFunctor] (SubF1 SubF2 : Type → Type) [SubBytesFunctor SubF1] [SubBytesFunctor SubF2] [HasStep SubF1 SubF2] [Has SubF2] : Has SubF1

Equations

• DY.BytesFunctor.instHasOfHasStep SubF1 SubF2 = { toSubFunctorTC := DY.ALaCarte.instSubFunctorTCOfSubFunctor }

@[reducible, inline]

abbrev DY.BytesFunctor.combine {n : Nat} (SubFs : Fin n → Type → Type) : Type → Type

Equations

• DY.BytesFunctor.combine SubFs = DY.ALaCarte.FunctorUnion SubFs

@[instance_reducible]

instance DY.instSubBytesFunctorCombine {n : Nat} (SubFs : Fin n → Type → Type) [(id : Fin n) → SubBytesFunctor (SubFs id)] : SubBytesFunctor (BytesFunctor.combine SubFs)

Equations

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

@[instance_reducible]

instance DY.instHasStepCombine {n : Nat} (SubFs : Fin n → Type → Type) [(id : Fin n) → SubBytesFunctor (SubFs id)] (id : Fin n) : BytesFunctor.HasStep (SubFs id) (BytesFunctor.combine SubFs)

Equations

• DY.instHasStepCombine SubFs id = { toSubFunctor := DY.ALaCarte.instSubFunctorFunctorUnionOfDecidableEq SubFs id }

@[reducible, inline]

abbrev DY.BytesView [BytesFunctor] (SubF : Type → Type) : Type

Equations

• DY.BytesView SubF = SubF DY.Bytes

def DY.Bytes.view? [BytesFunctor] (b : Bytes) (SubF : Type → Type) [SubBytesFunctor SubF] [BytesFunctor.Has SubF] : Option (BytesView SubF)

Equations

• b.view? SubF = DY.ALaCarte.Container.view SubF b

def DY.BytesView.pack [BytesFunctor] {SubF : Type → Type} [SubBytesFunctor SubF] [BytesFunctor.Has SubF] (b : BytesView SubF) : Bytes

Equations

• b.pack = DY.ALaCarte.Container.pack SubF b

theorem DY.Bytes.pack_view? [BytesFunctor] (SubF : Type → Type) [SubBytesFunctor SubF] [BytesFunctor.Has SubF] (b : Bytes) : match b.view? SubF with | some bview => bview.pack = b | none => True

theorem DY.BytesView.view_pack [BytesFunctor] {SubF : Type → Type} [SubBytesFunctor SubF] [BytesFunctor.Has SubF] (b : BytesView SubF) : b.pack.view? SubF = some b

theorem DY.Bytes.sizeOf_view [BytesFunctor] (SubF : Type → Type) [SubBytesFunctor SubF] [BytesFunctor.Has SubF] (b : Bytes) : match b.view? SubF with | some bview => ALaCarte.FunctorSizeOf.sizeOf bview ≤ sizeOf b | none => True

@[reducible, inline]

abbrev DY.Bytes.PartialFunction [BytesFunctor] (SubF : Type → Type) [SubBytesFunctor SubF] (a : Type) : Type

Equations

• DY.Bytes.PartialFunction SubF a = ((x : SubF DY.Bytes) → ((y : DY.Bytes) → autoParam (sizeOf y ≤ DY.ALaCarte.FunctorSizeOf.sizeOf x) DY.Bytes.PartialFunction._auto_1 → a) → a)

@[reducible, inline]

abbrev DY.Bytes.Function [BytesFunctor] (a : Type) : Type

Equations

• DY.Bytes.Function a = DY.Bytes.PartialFunction DY.BytesF a

def DY.Bytes.rec [BytesFunctor] {a : Type} (f : Function a) (x : Bytes) : a

Equations

• DY.Bytes.rec f x = DY.ALaCarte.Container.rec f x

class DY.Bytes.SubFunctionStep [BytesFunctor] {SubF1 SubF2 : Type → Type} {a : Type} [SubBytesFunctor SubF1] [SubBytesFunctor SubF2] [BytesFunctor.HasStep SubF1 SubF2] (partialFun1 : PartialFunction SubF1 a) (partialFun2 : semiOutParam (PartialFunction SubF2 a)) : Prop

• toALaCarte : ALaCarte.SubPartialFun partialFun1 partialFun2

class DY.Bytes.SubFunction [BytesFunctor] {SubF : Type → Type} [SubBytesFunctor SubF] [BytesFunctor.Has SubF] {a : Type} (partialFun : PartialFunction SubF a) (totalFun : Function a) : Prop

• toALaCarte : ALaCarte.SubPartialFunTC partialFun totalFun

instance DY.instSubFunctionBytesF [BytesFunctor] {a : Type} (totalFun : Bytes.Function a) : Bytes.SubFunction totalFun totalFun

instance DY.instSubFunctionOfSubFunctionStep [BytesFunctor] {SubF1 SubF2 : Type → Type} [SubBytesFunctor SubF1] [SubBytesFunctor SubF2] [BytesFunctor.HasStep SubF1 SubF2] [BytesFunctor.Has SubF2] {a : Type} (partialFun1 : Bytes.PartialFunction SubF1 a) (partialFun2 : Bytes.PartialFunction SubF2 a) (totalFun : Bytes.Function a) [Bytes.SubFunctionStep partialFun1 partialFun2] [Bytes.SubFunction partialFun2 totalFun] : Bytes.SubFunction partialFun1 totalFun

def DY.Bytes.PartialFunction.combine [BytesFunctor] {n : Nat} {SubFs : Fin n → Type → Type} [(id : Fin n) → SubBytesFunctor (SubFs id)] {a : Type} (funs : (id : Fin n) → PartialFunction (SubFs id) a) : PartialFunction (BytesFunctor.combine SubFs) a

Equations

• DY.Bytes.PartialFunction.combine funs = DY.ALaCarte.Container.PartialFun.combine funs

instance DY.instSubFunctionStepCombineCombine [BytesFunctor] {n : Nat} {SubFs : Fin n → Type → Type} [(id : Fin n) → SubBytesFunctor (SubFs id)] {a : Type} (funs : (id : Fin n) → Bytes.PartialFunction (SubFs id) a) (id : Fin n) : Bytes.SubFunctionStep (funs id) (Bytes.PartialFunction.combine funs)

theorem DY.Bytes.rec_eq [BytesFunctor] {SubF : Type → Type} [SubBytesFunctor SubF] [BytesFunctor.Has SubF] {a : Type} (partialFun : PartialFunction SubF a) (totalFun : Function a) [SubFunction partialFun totalFun] (x : BytesView SubF) : rec totalFun x.pack = partialFun x fun (y : Bytes) (x : sizeOf y ≤ ALaCarte.FunctorSizeOf.sizeOf x) => rec totalFun y

def DY.Bytes.PartialProof1 [BytesFunctor] {SubF : Type → Type} [SubBytesFunctor SubF] {a : Type} (fn : PartialFunction SubF a) (rec : Bytes → a) (p : a → Prop) : Prop

Equations

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

def DY.Bytes.Proof1 [BytesFunctor] {a : Type} (fn : Function a) (p : a → Prop) : Prop

Equations

• DY.Bytes.Proof1 fn p = DY.Bytes.PartialProof1 fn (DY.Bytes.rec fn) p

theorem DY.Bytes.Proof1.prove [BytesFunctor] {a : Type} {fn : Function a} {p : a → Prop} (pf : Proof1 fn p) (x : Bytes) : p (rec fn x)

theorem DY.Bytes.PartialProof1.combine [BytesFunctor] {n : Nat} {SubFs : Fin n → Type → Type} [(id : Fin n) → SubBytesFunctor (SubFs id)] {a : Type} {funs : (id : Fin n) → PartialFunction (SubFs id) a} {rec : Bytes → a} {p : a → Prop} (pfs : ∀ (id : Fin n), PartialProof1 (funs id) rec p) : PartialProof1 (PartialFunction.combine funs) rec p

def DY.Bytes.PartialProof2 [BytesFunctor] {SubF : Type → Type} [SubBytesFunctor SubF] {a b : Type} (fn1 : PartialFunction SubF a) (fn2 : PartialFunction SubF b) (rec1 : Bytes → a) (rec2 : Bytes → b) (p : a × b → Prop) : Prop

Equations

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

def DY.Bytes.Proof2 [BytesFunctor] {a b : Type} (fn1 : Function a) (fn2 : Function b) (p : a × b → Prop) : Prop

Equations

• DY.Bytes.Proof2 fn1 fn2 p = DY.Bytes.PartialProof2 fn1 fn2 (DY.Bytes.rec fn1) (DY.Bytes.rec fn2) p

theorem DY.Bytes.Proof2.prove [BytesFunctor] {a b : Type} {fn1 : Function a} {fn2 : Function b} {p : a × b → Prop} (pf : Proof2 fn1 fn2 p) (x : Bytes) : p (rec fn1 x, rec fn2 x)

theorem DY.Bytes.PartialProof2.combine [BytesFunctor] {n : Nat} {SubFs : Fin n → Type → Type} [(id : Fin n) → SubBytesFunctor (SubFs id)] {a b : Type} {funs1 : (id : Fin n) → PartialFunction (SubFs id) a} {funs2 : (id : Fin n) → PartialFunction (SubFs id) b} {rec1 : Bytes → a} {rec2 : Bytes → b} {p : a × b → Prop} (pfs : ∀ (id : Fin n), PartialProof2 (funs1 id) (funs2 id) rec1 rec2 p) : PartialProof2 (PartialFunction.combine funs1) (PartialFunction.combine funs2) rec1 rec2 p

class DY.BytesLength [BytesFunctor] : Type

• funs : Bytes.Function Nat

def DY.Bytes.length [BytesFunctor] [BytesLength] (b : Bytes) : Nat

Equations

• b.length = DY.Bytes.rec DY.BytesLength.funs b

@[reducible, inline]

abbrev DY.Bytes.PartialLength [BytesFunctor] (SubF : Type → Type) [SubBytesFunctor SubF] : Type

Equations

• DY.Bytes.PartialLength SubF = DY.Bytes.PartialFunction SubF Nat

class DY.BytesLength.HasStep [BytesFunctor] {SubF1 SubF2 : Type → Type} [SubBytesFunctor SubF1] [SubBytesFunctor SubF2] [BytesFunctor.HasStep SubF1 SubF2] (partialLength1 : outParam (Bytes.PartialLength SubF1)) (partialLength2 : Bytes.PartialLength SubF2) extends DY.Bytes.SubFunctionStep partialLength1 partialLength2 : Prop

• toALaCarte : ALaCarte.SubPartialFun partialLength1 partialLength2

class DY.BytesLength.Has [BytesFunctor] [BytesLength] {SubF : Type → Type} [SubBytesFunctor SubF] [BytesFunctor.Has SubF] (binv : outParam (Bytes.PartialLength SubF)) extends DY.Bytes.SubFunction binv DY.BytesLength.funs : Prop

• toALaCarte : ALaCarte.SubPartialFunTC binv BytesLength.funs

@[reducible, inline]

abbrev DY.Bytes.PartialLength.combine [BytesFunctor] {n : Nat} {SubFs : Fin n → Type → Type} [(id : Fin n) → SubBytesFunctor (SubFs id)] (lens : (id : Fin n) → PartialLength (SubFs id)) : PartialLength (BytesFunctor.combine SubFs)

Equations

• DY.Bytes.PartialLength.combine lens = DY.Bytes.PartialFunction.combine lens

instance DY.BytesLength.instHasBytesFFuns [BytesFunctor] [BytesLength] : Has funs

instance DY.BytesLength.instHasOfHasStep [BytesFunctor] [BytesLength] {SubF1 SubF2 : Type → Type} [SubBytesFunctor SubF1] [SubBytesFunctor SubF2] [BytesFunctor.HasStep SubF1 SubF2] [BytesFunctor.Has SubF2] (partialLen1 : Bytes.PartialLength SubF1) (partialLen2 : Bytes.PartialLength SubF2) [inst1 : HasStep partialLen1 partialLen2] [inst2 : Has partialLen2] : Has partialLen1

instance DY.BytesLength.instHasStepCombineCombine [BytesFunctor] {n : Nat} (SubFs : Fin n → Type → Type) [(id : Fin n) → SubBytesFunctor (SubFs id)] (invs : (id : Fin n) → Bytes.PartialLength (SubFs id)) (id : Fin n) : HasStep (invs id) (Bytes.PartialLength.combine invs)

@[simp]

theorem DY.Bytes.length.eq [BytesFunctor] {SubF : Type → Type} [SubBytesFunctor SubF] [BytesFunctor.Has SubF] [BytesLength] {subLength : PartialLength SubF} [BytesLength.Has subLength] (b : BytesView SubF) : b.pack.length = subLength b fun (y : Bytes) (x : sizeOf y ≤ ALaCarte.FunctorSizeOf.sizeOf b) => y.length