The matrix's sequencer at an arbitrary file

DescriptiveComplexity.Problems.Wide.DrawInstSeq read at a coarse file: the uniform stage discharge (ixKind_hStage), the control the sequencer folds (ixKindExitCtl, ixMatFs), the matrix's run and the gates' run, all at the registers of an arbitrary file rather than the elements of the universe.

The runs here are Relation.ReflTransGen: the atoms below them carry their budgets, and the counting of the layers above the matrix is one pass, to be made once the conversion reaches the evaluation.

noncomputable def DescriptiveComplexity.Draw.Data.IxKindSem {L : FirstOrder.Language} (dt : Data L) {A R P : Type} [LinearOrder A] {I : Type} [L.Structure A] (zero one : A) (vi : dt.VarIx) (st : TapeSt dt A R P I) (elt : I → Univ A R P dt.KIx dt.dd) : MatAtom dt.X dt.d.B (dt.nOf vi) → Type

The semantic data of one atom's run: an expansion atom needs the points its levels' registers encode; the other kinds need nothing.

Equations

• One or more equations did not get rendered due to their size.
• dt.IxKindSem zero one vi st elt (DescriptiveComplexity.Draw.MatAtom.eq a a_1) = PUnit.{1}
• dt.IxKindSem zero one vi st elt (DescriptiveComplexity.Draw.MatAtom.ord a a_1) = PUnit.{1}
• dt.IxKindSem zero one vi st elt (DescriptiveComplexity.Draw.MatAtom.stage i a) = PUnit.{1}

noncomputable def DescriptiveComplexity.Draw.Data.ixKindSemCast {L : FirstOrder.Language} (dt : Data L) {A R P : Type} [LinearOrder A] {I : Type} {elt : I → Univ A R P dt.KIx dt.dd} [L.Structure A] (zero one : A) (vi : dt.VarIx) {st st' : TapeSt dt A R P I} (hmir : st.mir = st'.mir) (hval : st.val = st'.val) (κ : MatAtom dt.X dt.d.B (dt.nOf vi)) (s : dt.IxKindSem zero one vi st elt κ) : dt.IxKindSem zero one vi st' elt κ

A semantic pack transports along the registers it reads. DescriptiveComplexity.Draw.Data.KindSem sees the tape state only through the levels' register sets, so a pack at one state is a pack at every state with the same mirror and VAL. This is what lets one pack – built at an address's entry state – serve every position of the spine and every round of the VAL loop, whose states differ from it in the tracks they have written and in the two scratch registers.

Equations

• dt.ixKindSemCast zero one vi hmir hval (DescriptiveComplexity.Draw.MatAtom.eq a a_1) s_2 = s_2
• dt.ixKindSemCast zero one vi hmir hval (DescriptiveComplexity.Draw.MatAtom.ord a a_1) s_2 = s_2
• dt.ixKindSemCast zero one vi hmir hval (DescriptiveComplexity.Draw.MatAtom.stage i a) s_2 = s_2
• dt.ixKindSemCast zero one vi hmir hval (DescriptiveComplexity.Draw.MatAtom.exp a ts) s_2 = ⟨↑s_2, ⋯⟩

noncomputable def DescriptiveComplexity.Draw.Data.ixKindExitCtl {L : FirstOrder.Language} (dt : Data L) {A R P : Type} [LinearOrder A] [LinearOrder R] [LinearOrder P] [FirstOrder.Language.wide.Structure (Univ A R P dt.KIx dt.dd)] [Finite A] {I : Type} (F : LaidFile dt A R P I) {elt : I → Univ A R P dt.KIx dt.dd} [Nonempty A] [L.IsRelational] [L.Structure A] (zero one : A) (hhas : F.toLayout.HasName zero) (vi : dt.VarIx) (av : Fin dt.natMax) (st : TapeSt dt A R P I) (v : Univ A R P dt.KIx dt.dd → Prop) (κ : MatAtom dt.X dt.d.B (dt.nOf vi)) : dt.IxKindSem zero one vi st elt κ → dt.kindArgs κ * Fintype.card dt.X.Tag ≤ dt.ntgDim → dt.kindDepth κ ≤ dt.eDim → dt.kindReads κ ≤ dt.nfDim → (dt.CtlIx → A) → dt.CtlIx → A

The control one atom's machinery leaves behind, by kind: the fold's exit at the comparison's or the expansion atom's family, the verdict store at the stage atom's read bit.

Equations

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

noncomputable def DescriptiveComplexity.Draw.Data.ixKindEndSt {L : FirstOrder.Language} (dt : Data L) {A R P I : Type} {elt : I → Univ A R P dt.KIx dt.dd} (vi : dt.VarIx) (v : Univ A R P dt.KIx dt.dd → Prop) (κ : MatAtom dt.X dt.d.B (dt.nOf vi)) (st : TapeSt dt A R P I) : TapeSt dt A R P I

The state an atom leaves: a stage atom normalizes SAV and TARGET to the home address (its random access writes them whatever they held), every other kind leaves the state alone.

Equations

• dt.ixKindEndSt vi v (DescriptiveComplexity.Draw.MatAtom.stage i a) st = dt.ixStageEndSt st elt v
• dt.ixKindEndSt vi v κ st = st

noncomputable def DescriptiveComplexity.Draw.Data.ixKindCost {L : FirstOrder.Language} (dt : Data L) (A : Type) (vi : dt.VarIx) (w wP wR wK : ℕ) : MatAtom dt.X dt.d.B (dt.nOf vi) → ℕ

What one atom's machinery is charged, by kind. A comparison walks its two coordinate loops once per tuple, an expansion its tag flags and then its leaf reads once per point of the evaluation order, both at the width w a walk to a named register costs; a stage atom pays its nine trips and thirteen dispatches over one copy loop per argument, at the widths the caller supplies. The bound is uniform in the atom's data – the expansion's are bounded by ntgDim and nfDim – which is what makes the sequencer's fold a single width.

Equations

• dt.ixKindCost A vi w wP wR wK (DescriptiveComplexity.Draw.MatAtom.eq a a_1) = 1 + ((2 + (w + 2) * 2) * (Nat.card (Lex (Fin dt.dd0 → A)) + 1) + 1)
• dt.ixKindCost A vi w wP wR wK (DescriptiveComplexity.Draw.MatAtom.ord a a_1) = 1 + ((2 + (w + 2) * 2) * (Nat.card (Lex (Fin dt.dd0 → A)) + 1) + 1)
• dt.ixKindCost A vi w wP wR wK (DescriptiveComplexity.Draw.MatAtom.exp a a_1) = 1 + ((w + 2) * dt.ntgDim + 2 + ((2 + (w + 2) * dt.nfDim) * (Nat.card (Lex (Fin dt.eDim → A)) + 1) + 1))
• dt.ixKindCost A vi w wP wR wK (DescriptiveComplexity.Draw.MatAtom.stage iv a) = 5 * wP + 2 * wR + 2 * wK + ((2 * w + 8) * (Nat.card (Lex (Fin dt.dd0 → A)) + 1) + 1 + 1) * dt.d.B.arity iv + 13

The matrix, assembled

noncomputable def DescriptiveComplexity.Draw.Data.ixMatCost {L : FirstOrder.Language} (dt : Data L) (A : Type) (vi : dt.VarIx) (w wP wR wK : ℕ) : ℕ

What the matrix charges one atom: the largest of its atoms' costs. A clocked caller that has no reason to prefer a coarser width takes this one, and the fold's (w + 2) * natOf vi + 1 is then a closed expression in the file's widths.

Equations

• dt.ixMatCost A vi w wP wR wK = Finset.univ.sup fun (a : Fin (dt.natOf vi)) => dt.ixKindCost A vi w wP wR wK (dt.kindOf vi a)

noncomputable def DescriptiveComplexity.Draw.Data.ixMatFs {L : FirstOrder.Language} (dt : Data L) {A R P : Type} [LinearOrder A] [LinearOrder R] [LinearOrder P] [FirstOrder.Language.wide.Structure (Univ A R P dt.KIx dt.dd)] [Finite A] {I : Type} (F : LaidFile dt A R P I) {elt : I → Univ A R P dt.KIx dt.dd} [Nonempty A] [L.IsRelational] [L.Structure A] (zero one : A) (hhas : F.toLayout.HasName zero) (vi : dt.VarIx) (st : TapeSt dt A R P I) (v : Univ A R P dt.KIx dt.dd → Prop) (enterSt : Fin (dt.natOf vi) → (dt.CtlIx → A) → (dt.SlotIx → A) → dt.CtlIx → A) (sem : (a : Fin (dt.natOf vi)) → dt.IxKindSem zero one vi st elt (dt.kindOf vi a)) (f₀ : dt.CtlIx → A) : ℕ → dt.CtlIx → A

The control thread across the matrix's atoms: each atom's machinery entered through the dispatch's enterSt, its exit control the next atom's input.

Equations

• One or more equations did not get rendered due to their size.
• dt.ixMatFs F zero one hhas vi st v enterSt sem f₀ 0 = f₀

The threaded states of the matrix

noncomputable def DescriptiveComplexity.Draw.Data.ixMatSt {L : FirstOrder.Language} (dt : Data L) {A R P I : Type} {elt : I → Univ A R P dt.KIx dt.dd} (vi : dt.VarIx) (st : TapeSt dt A R P I) (v : Univ A R P dt.KIx dt.dd → Prop) : ℕ → TapeSt dt A R P I

The state after the matrix's first n atoms: each stage atom normalizes SAV and TARGET, the other kinds change nothing.

Equations

• dt.ixMatSt vi st v 0 = st
• dt.ixMatSt vi st v n.succ = if h : n < dt.natOf vi then dt.ixKindEndSt vi v (dt.kindOf vi ⟨n, h⟩) (dt.ixMatSt vi st v n) else dt.ixMatSt vi st v n

theorem DescriptiveComplexity.Draw.Data.ixMatSt_fields {L : FirstOrder.Language} {dt : Data L} {A R P I : Type} {elt : I → Univ A R P dt.KIx dt.dd} {vi : dt.VarIx} {st : TapeSt dt A R P I} {v : Univ A R P dt.KIx dt.dd → Prop} (n : ℕ) : (dt.ixMatSt vi st v n).wk = st.wk ∧ (dt.ixMatSt vi st v n).mir = st.mir ∧ (dt.ixMatSt vi st v n).bot = st.bot ∧ (dt.ixMatSt vi st v n).val = st.val ∧ (dt.ixMatSt vi st v n).old = st.old

The threaded states differ from the entry state in SAV and TARGET alone – so every hypothesis the atoms need at them is the entry state's.

theorem DescriptiveComplexity.Draw.Data.ixMatSt_fields' {L : FirstOrder.Language} {dt : Data L} {A R P I : Type} {elt : I → Univ A R P dt.KIx dt.dd} {vi : dt.VarIx} {st : TapeSt dt A R P I} {v : Univ A R P dt.KIx dt.dd → Prop} (n : ℕ) : (dt.ixMatSt vi st v n).new = st.new ∧ (dt.ixMatSt vi st v n).ltp = st.ltp

The same two, along the matrix's whole chain of atoms.

noncomputable def DescriptiveComplexity.Draw.Data.ixMkKindSem {L : FirstOrder.Language} (dt : Data L) {A R P : Type} [LinearOrder A] {I : Type} [L.Structure A] (zero one : A) (vi : dt.VarIx) (st : TapeSt dt A R P I) {elt : I → Univ A R P dt.KIx dt.dd} (w : Fin (dt.nOf vi) → dt.X.Map A) (hENC : ∀ (j : Fin (dt.nOf vi)), wmBlk (ixAddr elt (dt.lvSet st vi j)) (Tag.arg (toLex (dt.lvBlk vi j))) = encMap dt.ly zero one (w j)) (κ : MatAtom dt.X dt.d.B (dt.nOf vi)) : dt.IxKindSem zero one vi st elt κ

The semantic data of every atom, from one encoded valuation: the expansion atoms' points are the valuation's, everything else needs nothing.

Equations

• dt.ixMkKindSem zero one vi st w hENC (DescriptiveComplexity.Draw.MatAtom.eq a a_1) = PUnit.unit
• dt.ixMkKindSem zero one vi st w hENC (DescriptiveComplexity.Draw.MatAtom.ord a a_1) = PUnit.unit
• dt.ixMkKindSem zero one vi st w hENC (DescriptiveComplexity.Draw.MatAtom.stage i a) = PUnit.unit
• dt.ixMkKindSem zero one vi st w hENC (DescriptiveComplexity.Draw.MatAtom.exp a ts) = ⟨fun (ℓ : Fin k) => w (ts ℓ), ⋯⟩

noncomputable def DescriptiveComplexity.Draw.Data.ixMatFsT {L : FirstOrder.Language} (dt : Data L) {A R P : Type} [LinearOrder A] [LinearOrder R] [LinearOrder P] [FirstOrder.Language.wide.Structure (Univ A R P dt.KIx dt.dd)] [Finite A] {I : Type} (F : LaidFile dt A R P I) {elt : I → Univ A R P dt.KIx dt.dd} [Nonempty A] [L.IsRelational] [L.Structure A] (zero one : A) (hhas : F.toLayout.HasName zero) (vi : dt.VarIx) (st : TapeSt dt A R P I) (v : Univ A R P dt.KIx dt.dd → Prop) (enterSt : Fin (dt.natOf vi) → (dt.CtlIx → A) → (dt.SlotIx → A) → dt.CtlIx → A) (sem : (a : Fin (dt.natOf vi)) → dt.IxKindSem zero one vi (dt.ixMatSt vi st v ↑a) elt (dt.kindOf vi a)) (f₀ : dt.CtlIx → A) : ℕ → dt.CtlIx → A

The control thread across the matrix's atoms, threaded: as DescriptiveComplexity.Draw.Data.matFs, with each atom's exit control computed at the state that atom actually runs at.

Equations

• One or more equations did not get rendered due to their size.
• dt.ixMatFsT F zero one hhas vi st v enterSt sem f₀ 0 = f₀

theorem DescriptiveComplexity.Draw.Data.ixScratchEq_matSt {L : FirstOrder.Language} {dt : Data L} {A R P I : Type} {elt : I → Univ A R P dt.KIx dt.dd} {vi : dt.VarIx} {st : TapeSt dt A R P I} {v : Univ A R P dt.KIx dt.dd → Prop} (n : ℕ) : dt.ScratchEq (dt.ixMatSt vi st v n) st

A threaded state of the matrix is the entry state up to the two scratch registers – matSt_eq in the form the congruences take.

The gates, assembled

noncomputable def DescriptiveComplexity.Draw.Data.ixGateCost {L : FirstOrder.Language} (dt : Data L) (A : Type) (w wP : ℕ) : ℕ

What one gate block's machinery is charged: the file test's sweep of the registers, the passing dispatch, the walk back and the tag flags, then the domain evaluation's leaf reads once per point of the evaluation order. Uniform in the block – the tag count and the read count are bounded by ntgDim and nfDim – so the gate sequence's fold is a single width.

Equations

• dt.ixGateCost A w wP = wP + (1 + (1 + ((w + 2) * dt.ntgDim + 2 + ((2 + (w + 2) * dt.nfDim) * (Nat.card (Lex (Fin dt.eDim → A)) + 1) + 1))))

noncomputable def DescriptiveComplexity.Draw.Data.ixGatesFs {L : FirstOrder.Language} (dt : Data L) {A R P : Type} [LinearOrder A] [LinearOrder R] [LinearOrder P] [FirstOrder.Language.wide.Structure (Univ A R P dt.KIx dt.dd)] [Finite A] {I : Type} (F : LaidFile dt A R P I) [Nonempty A] [L.IsRelational] [L.Structure A] (zero one : A) (hhas : F.toLayout.HasName zero) (vi : dt.VarIx) (st : TapeSt dt A R P I) (v : Univ A R P dt.KIx dt.dd → Prop) (bOf : Fin (dt.arOf vi) → Fin dt.ko ⊕ Fin dt.ki) (hc : Fintype.card dt.X.Tag ≤ dt.ntgDim) (hnG : ∀ (t' : dt.X.Tag), (dt.domPk t').n ≤ dt.eDim) (hrdG : ∀ (t' : dt.X.Tag), dt.domNr t' ≤ dt.nfDim) (tOf : Fin (dt.arOf vi) → dt.X.Tag) (enterSt : Fin (dt.arOf vi) → (dt.CtlIx → A) → (dt.SlotIx → A) → dt.CtlIx → A) (f₀ : dt.CtlIx → A) : ℕ → dt.CtlIx → A

The control thread across the gates' blocks (the all-pass path): each block's machinery entered through the dispatch's enterSt, its conjoining exit the next block's input.

Equations

• One or more equations did not get rendered due to their size.
• dt.ixGatesFs F zero one hhas vi st v bOf hc hnG hrdG tOf enterSt f₀ 0 = f₀