AlphaProof Code: Verifying Signal’s Security at the Machine-Code Level

Paper › Symbolic/Specifications/Model/EquationalTheory › Representable.leanTier 2 · definitions

Representable.lean🔗

Tier 2 · definitions used by the symbolic proof 13 headline theorems depend on it 177 of 211 lines trusted source ↗

trust banner in the header: none; the closure computes B2 for the symbolic proof

Read the definitions shown. Only the declarations that the headline statements use are shown, with the namespace, section, open and variable commands needed to read them. The collapsed runs are theorems, which Lean checks, and definitions that no headline statement uses.

Declarations on this page (9)

Single-Constructor SubBytesFunctor Builders

Arity-indexed builders for single-constructor ALaCarte term functors (SubF) and their FunctorSizeOf, Representable, RepresentableDecidableEq, and RepresentableOrd instances.

namespace DY

abbrev ALaCarte.FunctorSizeOf.unaryL25–27 ↗#

public abbrev ALaCarte.FunctorSizeOf.unary {F : Type → Type} (f0 : {a : Type} → F a → a) : ALaCarte.FunctorSizeOf F where sizeOf x := SizeOf.sizeOf (f0 x)

abbrev ALaCarte.FunctorSizeOf.binaryL29–31 ↗#

public abbrev ALaCarte.FunctorSizeOf.binary {F : Type → Type} (f0 f1 : {a : Type} → F a → a) : ALaCarte.FunctorSizeOf F where sizeOf x := SizeOf.sizeOf (f0 x) + SizeOf.sizeOf (f1 x)

abbrev ALaCarte.FunctorSizeOf.ternaryL33–35 ↗#

public abbrev ALaCarte.FunctorSizeOf.ternary {F : Type → Type} (f0 f1 f2 : {a : Type} → F a → a) : ALaCarte.FunctorSizeOf F where sizeOf x := SizeOf.sizeOf (f0 x) + SizeOf.sizeOf (f1 x) + SizeOf.sizeOf (f2 x)

def SubBytesFunctor.ofDataExplicitL37–77 ↗#

Builds a SubBytesFunctor for a single-constructor functor F with non-recursive metadata D and n recursive children.

@[expose, instance_reducible] public def SubBytesFunctor.ofDataExplicit {F : Type → Type} [sz : ALaCarte.FunctorSizeOf F] (D : Type) (deqD : DecidableEq D) (ordD : Ord D) (lawfulD : @Std.LawfulEqOrd D ordD) (transD : @Std.TransOrd D ordD) (n : Nat) (toData : {a : Type} → F a → D) (toChildren : {a : Type} → F a → Vector a n) (ofDataChildren : {a : Type} → D → Vector a n → F a) (from_to : {a : Type} → (x : F a) → ofDataChildren (toData x) (toChildren x) = x) (toData_of : {a : Type} → (d : D) → (as : Vector a n) → toData (ofDataChildren d as) = d) (toChildren_of : {a : Type} → (d : D) → (as : Vector a n) → toChildren (ofDataChildren d as) = as) (sizeOf_eq : {a : Type} → [SizeOf a] → (x : F a) → ALaCarte.FunctorSizeOf.sizeOf x = ((toChildren x).map SizeOf.sizeOf).sum) : SubBytesFunctor F := letI repr : ALaCarte.Representable F := { CtorId := Unit ctors := fun () => { Data := D, nRec := n } toRepr := fun x => { id := (), data := toData x, as := toChildren x } fromRepr := fun r => ofDataChildren r.data r.as from_to := from_to to_from := fun ⟨(), d, as⟩ => F:Type → Typesz:ALaCarte.FunctorSizeOf FD:TypedeqD:DecidableEq DordD:Ord DlawfulD:Std.LawfulEqOrd DtransD:Std.TransOrd Dn:NattoData:{a : Type} → F a → DtoChildren:{a : Type} → F a → Vector a nofDataChildren:{a : Type} → D → Vector a n → F afrom_to:∀ {a : Type} (x : F a), ofDataChildren (toData x) (toChildren x) = xtoData_of:∀ {a : Type} (d : D) (as : Vector a n), toData (ofDataChildren d as) = dtoChildren_of:∀ {a : Type} (d : D) (as : Vector a n), toChildren (ofDataChildren d as) = assizeOf_eq:∀ {a : Type} [inst : SizeOf a] (x : F a), ALaCarte.FunctorSizeOf.sizeOf x = (Vector.map SizeOf.sizeOf (toChildren x)).suma✝:Typex✝:ALaCarte.FunctorRepr (fun x => { Data := D, nRec := n }) a✝d:{ Data := D, nRec := n }.Dataas:Vector a✝ { Data := D, nRec := n }.nRec⊢ { id := (), data := toData (ofDataChildren { id := (), data := d, as := as }.data { id := (), data := d, as := as }.as), as := toChildren (ofDataChildren { id := (), data := d, as := as }.data { id := (), data := d, as := as }.as) } = { id := (), data := d, as := as } F:Type → Typesz:ALaCarte.FunctorSizeOf FD:TypedeqD:DecidableEq DordD:Ord DlawfulD:Std.LawfulEqOrd DtransD:Std.TransOrd Dn:NattoData:{a : Type} → F a → DtoChildren:{a : Type} → F a → Vector a nofDataChildren:{a : Type} → D → Vector a n → F afrom_to:∀ {a : Type} (x : F a), ofDataChildren (toData x) (toChildren x) = xtoData_of:∀ {a : Type} (d : D) (as : Vector a n), toData (ofDataChildren d as) = dtoChildren_of:∀ {a : Type} (d : D) (as : Vector a n), toChildren (ofDataChildren d as) = assizeOf_eq:∀ {a : Type} [inst : SizeOf a] (x : F a), ALaCarte.FunctorSizeOf.sizeOf x = (Vector.map SizeOf.sizeOf (toChildren x)).suma✝:Typex✝:ALaCarte.FunctorRepr (fun x => { Data := D, nRec := n }) a✝d:{ Data := D, nRec := n }.Dataas:Vector a✝ { Data := D, nRec := n }.nRec⊢ toData (ofDataChildren d as) = d ∧ toChildren (ofDataChildren d as) = as All goals completed! 🐙 sizeOf_eq := sizeOf_eq } letI deq : ALaCarte.RepresentableDecidableEq F := { ctorid_deq := (inferInstance : DecidableEq Unit) ctor_data_deq := fun () => deqD } letI ord : ALaCarte.RepresentableOrd F := { ctoridOrd := (inferInstance : Ord Unit) ctoridOrd_lawfulEq := (inferInstance : Std.LawfulEqOrd Unit) ctoridOrd_trans := (inferInstance : Std.TransOrd Unit) ctorDataOrd := fun () => ordD ctorDataOrd_lawfulEq := fun () => lawfulD ctorDataOrd_trans := fun () => transD } {}

def SubBytesFunctor.unaryL79–97 ↗#

@[expose, instance_reducible] public def SubBytesFunctor.unary {F : Type → Type} [sz : ALaCarte.FunctorSizeOf F] (f0 : {a : Type} → F a → a) (mk : {a : Type} → a → F a) (eta : {a : Type} → (x : F a) → mk (f0 x) = x := by intros; rfl) (f0_mk : {a : Type} → (x0 : a) → f0 (mk x0) = x0 := by intros; rfl) (hsz : {a : Type} → [SizeOf a] → (x : F a) → ALaCarte.FunctorSizeOf.sizeOf x = SizeOf.sizeOf (f0 x) := by intros; rfl) : SubBytesFunctor F := SubBytesFunctor.ofDataExplicit Unit inferInstance inferInstance inferInstance inferInstance 1 (fun _ => ()) (fun x => #v[f0 x]) (fun () as => mk as[0]) (fun x => eta x) (fun () _ => rfl) (fun () as => F:Type → Typesz:ALaCarte.FunctorSizeOf Ff0:{a : Type} → F a → amk:{a : Type} → a → F aeta:∀ {a : Type} (x : F a), mk (f0 x) = xf0_mk:∀ {a : Type} (x0 : a), f0 (mk x0) = x0hsz:∀ {a : Type} [inst : SizeOf a] (x : F a), ALaCarte.FunctorSizeOf.sizeOf x = SizeOf.sizeOf (f0 x)a✝:Typex✝:Unitas:Vector a✝ 1⊢ #v[f0 (mk as[0])] = as F:Type → Typesz:ALaCarte.FunctorSizeOf Ff0:{a : Type} → F a → amk:{a : Type} → a → F aeta:∀ {a : Type} (x : F a), mk (f0 x) = xf0_mk:∀ {a : Type} (x0 : a), f0 (mk x0) = x0hsz:∀ {a : Type} [inst : SizeOf a] (x : F a), ALaCarte.FunctorSizeOf.sizeOf x = SizeOf.sizeOf (f0 x)a✝:Typex✝:Unitl:List a✝hl:{ toList := l }.size = 1⊢ #v[f0 (mk (Vector.mk { toList := l } hl)[0])] = Vector.mk { toList := l } hl match l, hl with F:Type → Typesz:ALaCarte.FunctorSizeOf Ff0:{a : Type} → F a → amk:{a : Type} → a → F aeta:∀ {a : Type} (x : F a), mk (f0 x) = xf0_mk:∀ {a : Type} (x0 : a), f0 (mk x0) = x0hsz:∀ {a : Type} [inst : SizeOf a] (x : F a), ALaCarte.FunctorSizeOf.sizeOf x = SizeOf.sizeOf (f0 x)a✝:Typex✝¹:Unitl:List a✝hl:{ toList := l }.size = 1x0:a✝x✝:{ toList := [x0] }.size = 1⊢ #v[f0 (mk (Vector.mk { toList := [x0] } x✝)[0])] = Vector.mk { toList := [x0] } x✝ All goals completed! 🐙) (fun x => F:Type → Typesz:ALaCarte.FunctorSizeOf Ff0:{a : Type} → F a → amk:{a : Type} → a → F aeta:∀ {a : Type} (x : F a), mk (f0 x) = xf0_mk:∀ {a : Type} (x0 : a), f0 (mk x0) = x0hsz:∀ {a : Type} [inst : SizeOf a] (x : F a), ALaCarte.FunctorSizeOf.sizeOf x = SizeOf.sizeOf (f0 x)a✝:Typeinst✝:SizeOf a✝x:F a✝⊢ ALaCarte.FunctorSizeOf.sizeOf x = (Vector.map SizeOf.sizeOf #v[f0 x]).sum F:Type → Typesz:ALaCarte.FunctorSizeOf Ff0:{a : Type} → F a → amk:{a : Type} → a → F aeta:∀ {a : Type} (x : F a), mk (f0 x) = xf0_mk:∀ {a : Type} (x0 : a), f0 (mk x0) = x0hsz:∀ {a : Type} [inst : SizeOf a] (x : F a), ALaCarte.FunctorSizeOf.sizeOf x = SizeOf.sizeOf (f0 x)a✝:Typeinst✝:SizeOf a✝x:F a✝⊢ SizeOf.sizeOf (f0 x) = (Vector.map SizeOf.sizeOf #v[f0 x]).sum; All goals completed! 🐙)

def SubBytesFunctor.binaryL99–119 ↗#

@[expose, instance_reducible] public def SubBytesFunctor.binary {F : Type → Type} [sz : ALaCarte.FunctorSizeOf F] (f0 f1 : {a : Type} → F a → a) (mk : {a : Type} → a → a → F a) (eta : {a : Type} → (x : F a) → mk (f0 x) (f1 x) = x := by intros; rfl) (f0_mk : {a : Type} → (x0 x1 : a) → f0 (mk x0 x1) = x0 := by intros; rfl) (f1_mk : {a : Type} → (x0 x1 : a) → f1 (mk x0 x1) = x1 := by intros; rfl) (hsz : {a : Type} → [SizeOf a] → (x : F a) → ALaCarte.FunctorSizeOf.sizeOf x = SizeOf.sizeOf (f0 x) + SizeOf.sizeOf (f1 x) := by intros; rfl) : SubBytesFunctor F := SubBytesFunctor.ofDataExplicit Unit inferInstance inferInstance inferInstance inferInstance 2 (fun _ => ()) (fun x => #v[f0 x, f1 x]) (fun () as => mk as[0] as[1]) (fun x => eta x) (fun () _ => rfl) (fun () as => F:Type → Typesz:ALaCarte.FunctorSizeOf Ff0:{a : Type} → F a → af1:{a : Type} → F a → amk:{a : Type} → a → a → F aeta:∀ {a : Type} (x : F a), mk (f0 x) (f1 x) = xf0_mk:∀ {a : Type} (x0 x1 : a), f0 (mk x0 x1) = x0f1_mk:∀ {a : Type} (x0 x1 : a), f1 (mk x0 x1) = x1hsz:∀ {a : Type} [inst : SizeOf a] (x : F a), ALaCarte.FunctorSizeOf.sizeOf x = SizeOf.sizeOf (f0 x) + SizeOf.sizeOf (f1 x)a✝:Typex✝:Unitas:Vector a✝ 2⊢ #v[f0 (mk as[0] as[1]), f1 (mk as[0] as[1])] = as F:Type → Typesz:ALaCarte.FunctorSizeOf Ff0:{a : Type} → F a → af1:{a : Type} → F a → amk:{a : Type} → a → a → F aeta:∀ {a : Type} (x : F a), mk (f0 x) (f1 x) = xf0_mk:∀ {a : Type} (x0 x1 : a), f0 (mk x0 x1) = x0f1_mk:∀ {a : Type} (x0 x1 : a), f1 (mk x0 x1) = x1hsz:∀ {a : Type} [inst : SizeOf a] (x : F a), ALaCarte.FunctorSizeOf.sizeOf x = SizeOf.sizeOf (f0 x) + SizeOf.sizeOf (f1 x)a✝:Typex✝:Unitl:List a✝hl:{ toList := l }.size = 2⊢ #v[f0 (mk (Vector.mk { toList := l } hl)[0] (Vector.mk { toList := l } hl)[1]), f1 (mk (Vector.mk { toList := l } hl)[0] (Vector.mk { toList := l } hl)[1])] = Vector.mk { toList := l } hl match l, hl with F:Type → Typesz:ALaCarte.FunctorSizeOf Ff0:{a : Type} → F a → af1:{a : Type} → F a → amk:{a : Type} → a → a → F aeta:∀ {a : Type} (x : F a), mk (f0 x) (f1 x) = xf0_mk:∀ {a : Type} (x0 x1 : a), f0 (mk x0 x1) = x0f1_mk:∀ {a : Type} (x0 x1 : a), f1 (mk x0 x1) = x1hsz:∀ {a : Type} [inst : SizeOf a] (x : F a), ALaCarte.FunctorSizeOf.sizeOf x = SizeOf.sizeOf (f0 x) + SizeOf.sizeOf (f1 x)a✝:Typex✝¹:Unitl:List a✝hl:{ toList := l }.size = 2x0:a✝x1:a✝x✝:{ toList := [x0, x1] }.size = 2⊢ #v[f0 (mk (Vector.mk { toList := [x0, x1] } x✝)[0] (Vector.mk { toList := [x0, x1] } x✝)[1]), f1 (mk (Vector.mk { toList := [x0, x1] } x✝)[0] (Vector.mk { toList := [x0, x1] } x✝)[1])] = Vector.mk { toList := [x0, x1] } x✝ All goals completed! 🐙) (fun x => F:Type → Typesz:ALaCarte.FunctorSizeOf Ff0:{a : Type} → F a → af1:{a : Type} → F a → amk:{a : Type} → a → a → F aeta:∀ {a : Type} (x : F a), mk (f0 x) (f1 x) = xf0_mk:∀ {a : Type} (x0 x1 : a), f0 (mk x0 x1) = x0f1_mk:∀ {a : Type} (x0 x1 : a), f1 (mk x0 x1) = x1hsz:∀ {a : Type} [inst : SizeOf a] (x : F a), ALaCarte.FunctorSizeOf.sizeOf x = SizeOf.sizeOf (f0 x) + SizeOf.sizeOf (f1 x)a✝:Typeinst✝:SizeOf a✝x:F a✝⊢ ALaCarte.FunctorSizeOf.sizeOf x = (Vector.map SizeOf.sizeOf #v[f0 x, f1 x]).sum F:Type → Typesz:ALaCarte.FunctorSizeOf Ff0:{a : Type} → F a → af1:{a : Type} → F a → amk:{a : Type} → a → a → F aeta:∀ {a : Type} (x : F a), mk (f0 x) (f1 x) = xf0_mk:∀ {a : Type} (x0 x1 : a), f0 (mk x0 x1) = x0f1_mk:∀ {a : Type} (x0 x1 : a), f1 (mk x0 x1) = x1hsz:∀ {a : Type} [inst : SizeOf a] (x : F a), ALaCarte.FunctorSizeOf.sizeOf x = SizeOf.sizeOf (f0 x) + SizeOf.sizeOf (f1 x)a✝:Typeinst✝:SizeOf a✝x:F a✝⊢ SizeOf.sizeOf (f0 x) + SizeOf.sizeOf (f1 x) = (Vector.map SizeOf.sizeOf #v[f0 x, f1 x]).sum; All goals completed! 🐙)

def SubBytesFunctor.ternaryL121–142 ↗#

@[expose, instance_reducible] public def SubBytesFunctor.ternary {F : Type → Type} [sz : ALaCarte.FunctorSizeOf F] (f0 f1 f2 : {a : Type} → F a → a) (mk : {a : Type} → a → a → a → F a) (eta : {a : Type} → (x : F a) → mk (f0 x) (f1 x) (f2 x) = x := by intros; rfl) (f0_mk : {a : Type} → (x0 x1 x2 : a) → f0 (mk x0 x1 x2) = x0 := by intros; rfl) (f1_mk : {a : Type} → (x0 x1 x2 : a) → f1 (mk x0 x1 x2) = x1 := by intros; rfl) (f2_mk : {a : Type} → (x0 x1 x2 : a) → f2 (mk x0 x1 x2) = x2 := by intros; rfl) (hsz : {a : Type} → [SizeOf a] → (x : F a) → ALaCarte.FunctorSizeOf.sizeOf x = SizeOf.sizeOf (f0 x) + SizeOf.sizeOf (f1 x) + SizeOf.sizeOf (f2 x) := by intros; rfl) : SubBytesFunctor F := SubBytesFunctor.ofDataExplicit Unit inferInstance inferInstance inferInstance inferInstance 3 (fun _ => ()) (fun x => #v[f0 x, f1 x, f2 x]) (fun () as => mk as[0] as[1] as[2]) (fun x => eta x) (fun () _ => rfl) (fun () as => F:Type → Typesz:ALaCarte.FunctorSizeOf Ff0:{a : Type} → F a → af1:{a : Type} → F a → af2:{a : Type} → F a → amk:{a : Type} → a → a → a → F aeta:∀ {a : Type} (x : F a), mk (f0 x) (f1 x) (f2 x) = xf0_mk:∀ {a : Type} (x0 x1 x2 : a), f0 (mk x0 x1 x2) = x0f1_mk:∀ {a : Type} (x0 x1 x2 : a), f1 (mk x0 x1 x2) = x1f2_mk:∀ {a : Type} (x0 x1 x2 : a), f2 (mk x0 x1 x2) = x2hsz:∀ {a : Type} [inst : SizeOf a] (x : F a), ALaCarte.FunctorSizeOf.sizeOf x = SizeOf.sizeOf (f0 x) + SizeOf.sizeOf (f1 x) + SizeOf.sizeOf (f2 x)a✝:Typex✝:Unitas:Vector a✝ 3⊢ #v[f0 (mk as[0] as[1] as[2]), f1 (mk as[0] as[1] as[2]), f2 (mk as[0] as[1] as[2])] = as F:Type → Typesz:ALaCarte.FunctorSizeOf Ff0:{a : Type} → F a → af1:{a : Type} → F a → af2:{a : Type} → F a → amk:{a : Type} → a → a → a → F aeta:∀ {a : Type} (x : F a), mk (f0 x) (f1 x) (f2 x) = xf0_mk:∀ {a : Type} (x0 x1 x2 : a), f0 (mk x0 x1 x2) = x0f1_mk:∀ {a : Type} (x0 x1 x2 : a), f1 (mk x0 x1 x2) = x1f2_mk:∀ {a : Type} (x0 x1 x2 : a), f2 (mk x0 x1 x2) = x2hsz:∀ {a : Type} [inst : SizeOf a] (x : F a), ALaCarte.FunctorSizeOf.sizeOf x = SizeOf.sizeOf (f0 x) + SizeOf.sizeOf (f1 x) + SizeOf.sizeOf (f2 x)a✝:Typex✝:Unitl:List a✝hl:{ toList := l }.size = 3⊢ #v[f0 (mk (Vector.mk { toList := l } hl)[0] (Vector.mk { toList := l } hl)[1] (Vector.mk { toList := l } hl)[2]), f1 (mk (Vector.mk { toList := l } hl)[0] (Vector.mk { toList := l } hl)[1] (Vector.mk { toList := l } hl)[2]), f2 (mk (Vector.mk { toList := l } hl)[0] (Vector.mk { toList := l } hl)[1] (Vector.mk { toList := l } hl)[2])] = Vector.mk { toList := l } hl match l, hl with F:Type → Typesz:ALaCarte.FunctorSizeOf Ff0:{a : Type} → F a → af1:{a : Type} → F a → af2:{a : Type} → F a → amk:{a : Type} → a → a → a → F aeta:∀ {a : Type} (x : F a), mk (f0 x) (f1 x) (f2 x) = xf0_mk:∀ {a : Type} (x0 x1 x2 : a), f0 (mk x0 x1 x2) = x0f1_mk:∀ {a : Type} (x0 x1 x2 : a), f1 (mk x0 x1 x2) = x1f2_mk:∀ {a : Type} (x0 x1 x2 : a), f2 (mk x0 x1 x2) = x2hsz:∀ {a : Type} [inst : SizeOf a] (x : F a), ALaCarte.FunctorSizeOf.sizeOf x = SizeOf.sizeOf (f0 x) + SizeOf.sizeOf (f1 x) + SizeOf.sizeOf (f2 x)a✝:Typex✝¹:Unitl:List a✝hl:{ toList := l }.size = 3x0:a✝x1:a✝x2:a✝x✝:{ toList := [x0, x1, x2] }.size = 3⊢ #v[f0 (mk (Vector.mk { toList := [x0, x1, x2] } x✝)[0] (Vector.mk { toList := [x0, x1, x2] } x✝)[1] (Vector.mk { toList := [x0, x1, x2] } x✝)[2]), f1 (mk (Vector.mk { toList := [x0, x1, x2] } x✝)[0] (Vector.mk { toList := [x0, x1, x2] } x✝)[1] (Vector.mk { toList := [x0, x1, x2] } x✝)[2]), f2 (mk (Vector.mk { toList := [x0, x1, x2] } x✝)[0] (Vector.mk { toList := [x0, x1, x2] } x✝)[1] (Vector.mk { toList := [x0, x1, x2] } x✝)[2])] = Vector.mk { toList := [x0, x1, x2] } x✝ All goals completed! 🐙) (fun x => F:Type → Typesz:ALaCarte.FunctorSizeOf Ff0:{a : Type} → F a → af1:{a : Type} → F a → af2:{a : Type} → F a → amk:{a : Type} → a → a → a → F aeta:∀ {a : Type} (x : F a), mk (f0 x) (f1 x) (f2 x) = xf0_mk:∀ {a : Type} (x0 x1 x2 : a), f0 (mk x0 x1 x2) = x0f1_mk:∀ {a : Type} (x0 x1 x2 : a), f1 (mk x0 x1 x2) = x1f2_mk:∀ {a : Type} (x0 x1 x2 : a), f2 (mk x0 x1 x2) = x2hsz:∀ {a : Type} [inst : SizeOf a] (x : F a), ALaCarte.FunctorSizeOf.sizeOf x = SizeOf.sizeOf (f0 x) + SizeOf.sizeOf (f1 x) + SizeOf.sizeOf (f2 x)a✝:Typeinst✝:SizeOf a✝x:F a✝⊢ ALaCarte.FunctorSizeOf.sizeOf x = (Vector.map SizeOf.sizeOf #v[f0 x, f1 x, f2 x]).sum F:Type → Typesz:ALaCarte.FunctorSizeOf Ff0:{a : Type} → F a → af1:{a : Type} → F a → af2:{a : Type} → F a → amk:{a : Type} → a → a → a → F aeta:∀ {a : Type} (x : F a), mk (f0 x) (f1 x) (f2 x) = xf0_mk:∀ {a : Type} (x0 x1 x2 : a), f0 (mk x0 x1 x2) = x0f1_mk:∀ {a : Type} (x0 x1 x2 : a), f1 (mk x0 x1 x2) = x1f2_mk:∀ {a : Type} (x0 x1 x2 : a), f2 (mk x0 x1 x2) = x2hsz:∀ {a : Type} [inst : SizeOf a] (x : F a), ALaCarte.FunctorSizeOf.sizeOf x = SizeOf.sizeOf (f0 x) + SizeOf.sizeOf (f1 x) + SizeOf.sizeOf (f2 x)a✝:Typeinst✝:SizeOf a✝x:F a✝⊢ SizeOf.sizeOf (f0 x) + SizeOf.sizeOf (f1 x) + SizeOf.sizeOf (f2 x) = (Vector.map SizeOf.sizeOf #v[f0 x, f1 x, f2 x]).sum; All goals completed! 🐙)

def SubBytesFunctor.unaryDataL144–165 ↗#

Builds a SubBytesFunctor for a 1-child functor F carrying non-recursive metadata D.

@[expose, instance_reducible] public def SubBytesFunctor.unaryData {F : Type → Type} [sz : ALaCarte.FunctorSizeOf F] (D : Type) [DecidableEq D] [Ord D] [Std.LawfulEqOrd D] [Std.TransOrd D] (toData : {a : Type} → F a → D) (f0 : {a : Type} → F a → a) (mk : {a : Type} → D → a → F a) (eta : {a : Type} → (x : F a) → mk (toData x) (f0 x) = x) (toData_mk : {a : Type} → (d : D) → (x0 : a) → toData (mk d x0) = d) (f0_mk : {a : Type} → (d : D) → (x0 : a) → f0 (mk d x0) = x0 := by intros; rfl) (hsz : {a : Type} → [SizeOf a] → (x : F a) → ALaCarte.FunctorSizeOf.sizeOf x = SizeOf.sizeOf (f0 x) := by intros; rfl) : SubBytesFunctor F := SubBytesFunctor.ofDataExplicit D inferInstance inferInstance inferInstance inferInstance 1 toData (fun x => #v[f0 x]) (fun d as => mk d as[0]) eta (fun d as => toData_mk d as[0]) (fun d as => F:Type → Typesz:ALaCarte.FunctorSizeOf FD:Typeinst✝³:DecidableEq Dinst✝²:Ord Dinst✝¹:Std.LawfulEqOrd Dinst✝:Std.TransOrd DtoData:{a : Type} → F a → Df0:{a : Type} → F a → amk:{a : Type} → D → a → F aeta:∀ {a : Type} (x : F a), mk (toData x) (f0 x) = xtoData_mk:∀ {a : Type} (d : D) (x0 : a), toData (mk d x0) = df0_mk:∀ {a : Type} (d : D) (x0 : a), f0 (mk d x0) = x0hsz:∀ {a : Type} [inst : SizeOf a] (x : F a), ALaCarte.FunctorSizeOf.sizeOf x = SizeOf.sizeOf (f0 x)a✝:Typed:Das:Vector a✝ 1⊢ #v[f0 (mk d as[0])] = as F:Type → Typesz:ALaCarte.FunctorSizeOf FD:Typeinst✝³:DecidableEq Dinst✝²:Ord Dinst✝¹:Std.LawfulEqOrd Dinst✝:Std.TransOrd DtoData:{a : Type} → F a → Df0:{a : Type} → F a → amk:{a : Type} → D → a → F aeta:∀ {a : Type} (x : F a), mk (toData x) (f0 x) = xtoData_mk:∀ {a : Type} (d : D) (x0 : a), toData (mk d x0) = df0_mk:∀ {a : Type} (d : D) (x0 : a), f0 (mk d x0) = x0hsz:∀ {a : Type} [inst : SizeOf a] (x : F a), ALaCarte.FunctorSizeOf.sizeOf x = SizeOf.sizeOf (f0 x)a✝:Typed:Dl:List a✝hl:{ toList := l }.size = 1⊢ #v[f0 (mk d (Vector.mk { toList := l } hl)[0])] = Vector.mk { toList := l } hl match l, hl with F:Type → Typesz:ALaCarte.FunctorSizeOf FD:Typeinst✝³:DecidableEq Dinst✝²:Ord Dinst✝¹:Std.LawfulEqOrd Dinst✝:Std.TransOrd DtoData:{a : Type} → F a → Df0:{a : Type} → F a → amk:{a : Type} → D → a → F aeta:∀ {a : Type} (x : F a), mk (toData x) (f0 x) = xtoData_mk:∀ {a : Type} (d : D) (x0 : a), toData (mk d x0) = df0_mk:∀ {a : Type} (d : D) (x0 : a), f0 (mk d x0) = x0hsz:∀ {a : Type} [inst : SizeOf a] (x : F a), ALaCarte.FunctorSizeOf.sizeOf x = SizeOf.sizeOf (f0 x)a✝:Typed:Dl:List a✝hl:{ toList := l }.size = 1x0:a✝x✝:{ toList := [x0] }.size = 1⊢ #v[f0 (mk d (Vector.mk { toList := [x0] } x✝)[0])] = Vector.mk { toList := [x0] } x✝ All goals completed! 🐙) (fun x => F:Type → Typesz:ALaCarte.FunctorSizeOf FD:Typeinst✝⁴:DecidableEq Dinst✝³:Ord Dinst✝²:Std.LawfulEqOrd Dinst✝¹:Std.TransOrd DtoData:{a : Type} → F a → Df0:{a : Type} → F a → amk:{a : Type} → D → a → F aeta:∀ {a : Type} (x : F a), mk (toData x) (f0 x) = xtoData_mk:∀ {a : Type} (d : D) (x0 : a), toData (mk d x0) = df0_mk:∀ {a : Type} (d : D) (x0 : a), f0 (mk d x0) = x0hsz:∀ {a : Type} [inst : SizeOf a] (x : F a), ALaCarte.FunctorSizeOf.sizeOf x = SizeOf.sizeOf (f0 x)a✝:Typeinst✝:SizeOf a✝x:F a✝⊢ ALaCarte.FunctorSizeOf.sizeOf x = (Vector.map SizeOf.sizeOf #v[f0 x]).sum F:Type → Typesz:ALaCarte.FunctorSizeOf FD:Typeinst✝⁴:DecidableEq Dinst✝³:Ord Dinst✝²:Std.LawfulEqOrd Dinst✝¹:Std.TransOrd DtoData:{a : Type} → F a → Df0:{a : Type} → F a → amk:{a : Type} → D → a → F aeta:∀ {a : Type} (x : F a), mk (toData x) (f0 x) = xtoData_mk:∀ {a : Type} (d : D) (x0 : a), toData (mk d x0) = df0_mk:∀ {a : Type} (d : D) (x0 : a), f0 (mk d x0) = x0hsz:∀ {a : Type} [inst : SizeOf a] (x : F a), ALaCarte.FunctorSizeOf.sizeOf x = SizeOf.sizeOf (f0 x)a✝:Typeinst✝:SizeOf a✝x:F a✝⊢ SizeOf.sizeOf (f0 x) = (Vector.map SizeOf.sizeOf #v[f0 x]).sum; All goals completed! 🐙)

def SubBytesFunctor.ternaryByCodeL167–212 ↗#

Builds a SubBytesFunctor for a 3-child functor F whose non-recursive metadata D inherits its Ord laws along an injective encoding code : D → C.

@[expose, instance_reducible] public def SubBytesFunctor.ternaryByCode {F : Type → Type} [sz : ALaCarte.FunctorSizeOf F] {D C : Type} [DecidableEq D] [Ord C] [Std.LawfulEqOrd C] [Std.TransOrd C] (code : D → C) (code_inj : ∀ {x y : D}, code x = code y → x = y) (toData : {a : Type} → F a → D) (f0 f1 f2 : {a : Type} → F a → a) (mk : {a : Type} → D → a → a → a → F a) (eta : {a : Type} → (x : F a) → mk (toData x) (f0 x) (f1 x) (f2 x) = x := by intros; rfl) (toData_mk : {a : Type} → (d : D) → (x0 x1 x2 : a) → toData (mk d x0 x1 x2) = d := by intros; rfl) (f0_mk : {a : Type} → (d : D) → (x0 x1 x2 : a) → f0 (mk d x0 x1 x2) = x0 := by intros; rfl) (f1_mk : {a : Type} → (d : D) → (x0 x1 x2 : a) → f1 (mk d x0 x1 x2) = x1 := by intros; rfl) (f2_mk : {a : Type} → (d : D) → (x0 x1 x2 : a) → f2 (mk d x0 x1 x2) = x2 := by intros; rfl) (hsz : {a : Type} → [SizeOf a] → (x : F a) → ALaCarte.FunctorSizeOf.sizeOf x = SizeOf.sizeOf (f0 x) + SizeOf.sizeOf (f1 x) + SizeOf.sizeOf (f2 x) := by intros; rfl) : SubBytesFunctor F := letI ordD : Ord D := { compare x y := Ord.compare (code x) (code y) } letI reflD : Std.ReflOrd D := { compare_self := fun {x} => Std.ReflOrd.compare_self (a := code x) } letI lawfulD : Std.LawfulEqOrd D := { eq_of_compare := fun h => code_inj (Std.LawfulEqOrd.eq_of_compare h) } letI orientD : Std.OrientedOrd D := { eq_swap := fun {x y} => Std.OrientedOrd.eq_swap (a := code x) (b := code y) } letI transD : Std.TransOrd D := { isLE_trans := fun h1 h2 => Std.TransOrd.isLE_trans (a := code _) (b := code _) (c := code _) h1 h2 } SubBytesFunctor.ofDataExplicit D inferInstance ordD lawfulD transD 3 toData (fun x => #v[f0 x, f1 x, f2 x]) (fun d as => mk d as[0] as[1] as[2]) eta (fun d as => toData_mk d as[0] as[1] as[2]) (fun d as => F:Type → Typesz:ALaCarte.FunctorSizeOf FD:TypeC:Typeinst✝³:DecidableEq Dinst✝²:Ord Cinst✝¹:Std.LawfulEqOrd Cinst✝:Std.TransOrd Ccode:D → Ccode_inj:∀ {x y : D}, code x = code y → x = ytoData:{a : Type} → F a → Df0:{a : Type} → F a → af1:{a : Type} → F a → af2:{a : Type} → F a → amk:{a : Type} → D → a → a → a → F aeta:∀ {a : Type} (x : F a), mk (toData x) (f0 x) (f1 x) (f2 x) = xtoData_mk:∀ {a : Type} (d : D) (x0 x1 x2 : a), toData (mk d x0 x1 x2) = df0_mk:∀ {a : Type} (d : D) (x0 x1 x2 : a), f0 (mk d x0 x1 x2) = x0f1_mk:∀ {a : Type} (d : D) (x0 x1 x2 : a), f1 (mk d x0 x1 x2) = x1f2_mk:∀ {a : Type} (d : D) (x0 x1 x2 : a), f2 (mk d x0 x1 x2) = x2hsz:∀ {a : Type} [inst : SizeOf a] (x : F a), ALaCarte.FunctorSizeOf.sizeOf x = SizeOf.sizeOf (f0 x) + SizeOf.sizeOf (f1 x) + SizeOf.sizeOf (f2 x)ordD:Ord D := { compare := fun x y => compare (code x) (code y) }reflD:Std.ReflOrd D := ···lawfulD:Std.LawfulEqOrd D := ···orientD:Std.OrientedOrd D := ···transD:Std.TransOrd D := ···a✝:Typed:Das:Vector a✝ 3⊢ #v[f0 (mk d as[0] as[1] as[2]), f1 (mk d as[0] as[1] as[2]), f2 (mk d as[0] as[1] as[2])] = as F:Type → Typesz:ALaCarte.FunctorSizeOf FD:TypeC:Typeinst✝³:DecidableEq Dinst✝²:Ord Cinst✝¹:Std.LawfulEqOrd Cinst✝:Std.TransOrd Ccode:D → Ccode_inj:∀ {x y : D}, code x = code y → x = ytoData:{a : Type} → F a → Df0:{a : Type} → F a → af1:{a : Type} → F a → af2:{a : Type} → F a → amk:{a : Type} → D → a → a → a → F aeta:∀ {a : Type} (x : F a), mk (toData x) (f0 x) (f1 x) (f2 x) = xtoData_mk:∀ {a : Type} (d : D) (x0 x1 x2 : a), toData (mk d x0 x1 x2) = df0_mk:∀ {a : Type} (d : D) (x0 x1 x2 : a), f0 (mk d x0 x1 x2) = x0f1_mk:∀ {a : Type} (d : D) (x0 x1 x2 : a), f1 (mk d x0 x1 x2) = x1f2_mk:∀ {a : Type} (d : D) (x0 x1 x2 : a), f2 (mk d x0 x1 x2) = x2hsz:∀ {a : Type} [inst : SizeOf a] (x : F a), ALaCarte.FunctorSizeOf.sizeOf x = SizeOf.sizeOf (f0 x) + SizeOf.sizeOf (f1 x) + SizeOf.sizeOf (f2 x)ordD:Ord D := { compare := fun x y => compare (code x) (code y) }reflD:Std.ReflOrd D := ···lawfulD:Std.LawfulEqOrd D := ···orientD:Std.OrientedOrd D := ···transD:Std.TransOrd D := ···a✝:Typed:Dl:List a✝hl:{ toList := l }.size = 3⊢ #v[f0 (mk d (Vector.mk { toList := l } hl)[0] (Vector.mk { toList := l } hl)[1] (Vector.mk { toList := l } hl)[2]), f1 (mk d (Vector.mk { toList := l } hl)[0] (Vector.mk { toList := l } hl)[1] (Vector.mk { toList := l } hl)[2]), f2 (mk d (Vector.mk { toList := l } hl)[0] (Vector.mk { toList := l } hl)[1] (Vector.mk { toList := l } hl)[2])] = Vector.mk { toList := l } hl match l, hl with F:Type → Typesz:ALaCarte.FunctorSizeOf FD:TypeC:Typeinst✝³:DecidableEq Dinst✝²:Ord Cinst✝¹:Std.LawfulEqOrd Cinst✝:Std.TransOrd Ccode:D → Ccode_inj:∀ {x y : D}, code x = code y → x = ytoData:{a : Type} → F a → Df0:{a : Type} → F a → af1:{a : Type} → F a → af2:{a : Type} → F a → amk:{a : Type} → D → a → a → a → F aeta:∀ {a : Type} (x : F a), mk (toData x) (f0 x) (f1 x) (f2 x) = xtoData_mk:∀ {a : Type} (d : D) (x0 x1 x2 : a), toData (mk d x0 x1 x2) = df0_mk:∀ {a : Type} (d : D) (x0 x1 x2 : a), f0 (mk d x0 x1 x2) = x0f1_mk:∀ {a : Type} (d : D) (x0 x1 x2 : a), f1 (mk d x0 x1 x2) = x1f2_mk:∀ {a : Type} (d : D) (x0 x1 x2 : a), f2 (mk d x0 x1 x2) = x2hsz:∀ {a : Type} [inst : SizeOf a] (x : F a), ALaCarte.FunctorSizeOf.sizeOf x = SizeOf.sizeOf (f0 x) + SizeOf.sizeOf (f1 x) + SizeOf.sizeOf (f2 x)ordD:Ord D := { compare := fun x y => compare (code x) (code y) }reflD:Std.ReflOrd D := ···lawfulD:Std.LawfulEqOrd D := ···orientD:Std.OrientedOrd D := ···transD:Std.TransOrd D := ···a✝:Typed:Dl:List a✝hl:{ toList := l }.size = 3x0:a✝x1:a✝x2:a✝x✝:{ toList := [x0, x1, x2] }.size = 3⊢ #v[f0 (mk d (Vector.mk { toList := [x0, x1, x2] } x✝)[0] (Vector.mk { toList := [x0, x1, x2] } x✝)[1] (Vector.mk { toList := [x0, x1, x2] } x✝)[2]), f1 (mk d (Vector.mk { toList := [x0, x1, x2] } x✝)[0] (Vector.mk { toList := [x0, x1, x2] } x✝)[1] (Vector.mk { toList := [x0, x1, x2] } x✝)[2]), f2 (mk d (Vector.mk { toList := [x0, x1, x2] } x✝)[0] (Vector.mk { toList := [x0, x1, x2] } x✝)[1] (Vector.mk { toList := [x0, x1, x2] } x✝)[2])] = Vector.mk { toList := [x0, x1, x2] } x✝ All goals completed! 🐙) (fun x => F:Type → Typesz:ALaCarte.FunctorSizeOf FD:TypeC:Typeinst✝⁴:DecidableEq Dinst✝³:Ord Cinst✝²:Std.LawfulEqOrd Cinst✝¹:Std.TransOrd Ccode:D → Ccode_inj:∀ {x y : D}, code x = code y → x = ytoData:{a : Type} → F a → Df0:{a : Type} → F a → af1:{a : Type} → F a → af2:{a : Type} → F a → amk:{a : Type} → D → a → a → a → F aeta:∀ {a : Type} (x : F a), mk (toData x) (f0 x) (f1 x) (f2 x) = xtoData_mk:∀ {a : Type} (d : D) (x0 x1 x2 : a), toData (mk d x0 x1 x2) = df0_mk:∀ {a : Type} (d : D) (x0 x1 x2 : a), f0 (mk d x0 x1 x2) = x0f1_mk:∀ {a : Type} (d : D) (x0 x1 x2 : a), f1 (mk d x0 x1 x2) = x1f2_mk:∀ {a : Type} (d : D) (x0 x1 x2 : a), f2 (mk d x0 x1 x2) = x2hsz:∀ {a : Type} [inst : SizeOf a] (x : F a), ALaCarte.FunctorSizeOf.sizeOf x = SizeOf.sizeOf (f0 x) + SizeOf.sizeOf (f1 x) + SizeOf.sizeOf (f2 x)ordD:Ord D := { compare := fun x y => compare (code x) (code y) }reflD:Std.ReflOrd D := ···lawfulD:Std.LawfulEqOrd D := ···orientD:Std.OrientedOrd D := ···transD:Std.TransOrd D := ···a✝:Typeinst✝:SizeOf a✝x:F a✝⊢ ALaCarte.FunctorSizeOf.sizeOf x = (Vector.map SizeOf.sizeOf #v[f0 x, f1 x, f2 x]).sum F:Type → Typesz:ALaCarte.FunctorSizeOf FD:TypeC:Typeinst✝⁴:DecidableEq Dinst✝³:Ord Cinst✝²:Std.LawfulEqOrd Cinst✝¹:Std.TransOrd Ccode:D → Ccode_inj:∀ {x y : D}, code x = code y → x = ytoData:{a : Type} → F a → Df0:{a : Type} → F a → af1:{a : Type} → F a → af2:{a : Type} → F a → amk:{a : Type} → D → a → a → a → F aeta:∀ {a : Type} (x : F a), mk (toData x) (f0 x) (f1 x) (f2 x) = xtoData_mk:∀ {a : Type} (d : D) (x0 x1 x2 : a), toData (mk d x0 x1 x2) = df0_mk:∀ {a : Type} (d : D) (x0 x1 x2 : a), f0 (mk d x0 x1 x2) = x0f1_mk:∀ {a : Type} (d : D) (x0 x1 x2 : a), f1 (mk d x0 x1 x2) = x1f2_mk:∀ {a : Type} (d : D) (x0 x1 x2 : a), f2 (mk d x0 x1 x2) = x2hsz:∀ {a : Type} [inst : SizeOf a] (x : F a), ALaCarte.FunctorSizeOf.sizeOf x = SizeOf.sizeOf (f0 x) + SizeOf.sizeOf (f1 x) + SizeOf.sizeOf (f2 x)ordD:Ord D := { compare := fun x y => compare (code x) (code y) }reflD:Std.ReflOrd D := ···lawfulD:Std.LawfulEqOrd D := ···orientD:Std.OrientedOrd D := ···transD:Std.TransOrd D := ···a✝:Typeinst✝:SizeOf a✝x:F a✝⊢ SizeOf.sizeOf (f0 x) + SizeOf.sizeOf (f1 x) + SizeOf.sizeOf (f2 x) = (Vector.map SizeOf.sizeOf #v[f0 x, f1 x, f2 x]).sum; All goals completed! 🐙)
end DY