Documentation

DY.Bytes.Basic

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

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

Instances

@[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 :

BytesF : Type → Type
inst : SubBytesFunctor BytesF

Instances

@[instance_reducible]

instance DY.instSubBytesFunctorBytesF [inst : BytesFunctor] :

SubBytesFunctor BytesF

Equations

DY.instSubBytesFunctorBytesF = DY.BytesFunctor.inst

@[irreducible]

def DY.Bytes [BytesFunctor] :

Equations

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

Instances For

@[instance_reducible]

noncomputable instance DY.instSizeOfBytes [BytesFunctor] :

Equations

DY.instSizeOfBytes = { sizeOf := fun (m : Subtype DY.ALaCarte.BareContainer.wf) => m._sizeOf_1 }

@[instance_reducible]

instance DY.instDecidableEqBytes [BytesFunctor] :

DecidableEq Bytes

Equations

DY.instDecidableEqBytes a b = DY.ALaCarte.instDecidableEqContainerForOfRepresentableDecidableEq DY.BytesF a b

@[instance_reducible]

instance DY.instOrdBytes [BytesFunctor] :

Equations

DY.instOrdBytes = { compare := DY.ALaCarte.Container.compare }

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] :

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 :

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

Instances

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

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

Instances

@[instance_reducible]

instance DY.BytesFunctor.instHasBytesF [BytesFunctor] :

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 {a : Type} (SubFs : a → Type → Type) :

Equations

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

Instances For

@[instance_reducible]

instance DY.instSubBytesFunctorCombineOfDecidableEqOfLawfulEqOrdOfTransOrd {a : Type} [DecidableEq a] [Ord a] [Std.LawfulEqOrd a] [Std.TransOrd a] (SubFs : a → Type → Type) [(id : a) → 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 {a : Type} [DecidableEq a] [Ord a] [Std.LawfulEqOrd a] [Std.TransOrd a] (SubFs : a → Type → Type) [(id : a) → SubBytesFunctor (SubFs id)] (id : a) :

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) :

Equations

DY.BytesView SubF = SubF DY.Bytes

Instances For

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

Instances For

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

Equations

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

Instances For

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

def DY.Bytes.PartialFunction [BytesFunctor] (SubF : Type → Type) [SubBytesFunctor SubF] (a : 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)

Instances For

@[reducible, inline]

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

Equations

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

Instances For

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

Instances For

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)) extends DY.ALaCarte.SubPartialFun partialFun1 partialFun2 :

pf (x : SubF1 (ContainerFor BytesF)) (rec : (y : ContainerFor BytesF) → sizeOf y ≤ FunctorSizeOf.sizeOf x → a) : partialFun1 x rec = partialFun2 (SubFunctor.inj x) fun (y : ContainerFor BytesF) (h : sizeOf y ≤ FunctorSizeOf.sizeOf (SubFunctor.inj x)) => rec y ⋯

Instances

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

pf (x : SubF (ContainerFor BytesF)) (rec : (y : ContainerFor BytesF) → sizeOf y ≤ FunctorSizeOf.sizeOf x → a) : partialFun x rec = totalFun (SubFunctorTC.inj x) fun (y : ContainerFor BytesF) (h : sizeOf y ≤ FunctorSizeOf.sizeOf (SubFunctorTC.inj x)) => rec y ⋯

Instances

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] {t : Type} [DecidableEq t] [Ord t] [Std.LawfulEqOrd t] [Std.TransOrd t] {SubFs : t → Type → Type} [(id : t) → SubBytesFunctor (SubFs id)] {a : Type} (funs : (id : t) → PartialFunction (SubFs id) a) :

PartialFunction (BytesFunctor.combine SubFs) a

Equations

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

Instances For

instance DY.instSubFunctionStepCombineCombine [BytesFunctor] {t : Type} [DecidableEq t] [Ord t] [Std.LawfulEqOrd t] [Std.TransOrd t] {SubFs : t → Type → Type} [(id : t) → SubBytesFunctor (SubFs id)] {a : Type} (funs : (id : t) → Bytes.PartialFunction (SubFs id) a) (id : t) :

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) :

Equations

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

Instances For

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

Equations

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

Instances For

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] {t : Type} [DecidableEq t] [Ord t] [Std.LawfulEqOrd t] [Std.TransOrd t] {SubFs : t → Type → Type} [(id : t) → SubBytesFunctor (SubFs id)] {a : Type} {funs : (id : t) → PartialFunction (SubFs id) a} {rec : Bytes → a} {p : a → Prop} (pfs : ∀ (id : t), 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) :

Equations

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

Instances For

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

Equations

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

Instances For

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] {t : Type} [DecidableEq t] [Ord t] [Std.LawfulEqOrd t] [Std.TransOrd t] {SubFs : t → Type → Type} [(id : t) → SubBytesFunctor (SubFs id)] {a b : Type} {funs1 : (id : t) → PartialFunction (SubFs id) a} {funs2 : (id : t) → PartialFunction (SubFs id) b} {rec1 : Bytes → a} {rec2 : Bytes → b} {p : a × b → Prop} (pfs : ∀ (id : t), PartialProof2 (funs1 id) (funs2 id) rec1 rec2 p) :

PartialProof2 (PartialFunction.combine funs1) (PartialFunction.combine funs2) rec1 rec2 p

class DY.BytesLength [BytesFunctor] :

funs : Bytes.Function Nat

Instances

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

Equations

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

Instances For

@[reducible, inline]

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

Equations

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

Instances For

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 :

pf (x : SubF1 (ContainerFor BytesF)) (rec : (y : ContainerFor BytesF) → sizeOf y ≤ FunctorSizeOf.sizeOf x → Nat) : partialLength1 x rec = partialLength2 (SubFunctor.inj x) fun (y : ContainerFor BytesF) (h : sizeOf y ≤ FunctorSizeOf.sizeOf (SubFunctor.inj x)) => rec y ⋯

Instances

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 :

pf (x : SubF (ContainerFor BytesF)) (rec : (y : ContainerFor BytesF) → sizeOf y ≤ FunctorSizeOf.sizeOf x → Nat) : binv x rec = BytesLength.funs (SubFunctorTC.inj x) fun (y : ContainerFor BytesF) (h : sizeOf y ≤ FunctorSizeOf.sizeOf (SubFunctorTC.inj x)) => rec y ⋯

Instances

@[reducible, inline]

abbrev DY.Bytes.PartialLength.combine [BytesFunctor] {t : Type} [DecidableEq t] [Ord t] [Std.LawfulEqOrd t] [Std.TransOrd t] {SubFs : t → Type → Type} [(id : t) → SubBytesFunctor (SubFs id)] (lens : (id : t) → PartialLength (SubFs id)) :

PartialLength (BytesFunctor.combine SubFs)

Equations

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

Instances For

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

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] {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.PartialLength (SubFs id)) (id : t) :

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} [tc : BytesLength.Has subLength] (b : BytesView SubF) :

b.pack.length = subLength b fun (y : Bytes) (x : sizeOf y ≤ ALaCarte.FunctorSizeOf.sizeOf b) => y.length