One variable's machinery at an arbitrary file

DescriptiveComplexity.Problems.Wide.DrawInstVar read at a coarse file: the gates' leg and the matrix leg of one variable's machinery, the VAL loop's thread and the capstone runs. Everything below it is already at the file, so this is the last layer before the evaluation.

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

What the gates' leg of one variable's machinery is charged: the walk-back into the sequence, the gate sequence itself, and the walk-back at the verdict checkpoint.

Equations

• dt.ixVarGatesCost A vi w wP = 1 + ((dt.ixGateCost A w wP + 2) * dt.arOf vi + 1) + 1

noncomputable def DescriptiveComplexity.Draw.Data.ixFailCtl {L : FirstOrder.Language} (dt : Data L) {A R P : Type} [Fintype dt.SlotIx] [LinearOrder A] [LinearOrder R] [LinearOrder P] [FirstOrder.Language.wide.Structure (Univ A R P dt.KIx dt.dd)] [Finite A] {PR : Prog A R P dt.CtlIx dt.SlotIx dt.KIx dt.dd} {I : Type} (F : LaidFile dt A R P I) (hhasP : F.toLayout.HasName PR.zero) [Nonempty A] [L.IsRelational] [L.Structure A] (vi : dt.VarIx) (st : TapeSt dt A R P I) {v : Univ A R P dt.KIx dt.dd → Prop} (tOf : Fin (dt.arOf vi) → dt.X.Tag) (ℓ₀ : Fin (dt.arOf vi)) (f₀ : dt.CtlIx → A) : dt.CtlIx → A

The control after a failing gate sequence: the fail store at the failing block's entry, the flag clear.

Equations

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

noncomputable def DescriptiveComplexity.Draw.Data.ixUngatedCtl {L : FirstOrder.Language} (dt : Data L) {A R P : Type} [Fintype dt.SlotIx] [LinearOrder A] [LinearOrder R] [LinearOrder P] [FirstOrder.Language.wide.Structure (Univ A R P dt.KIx dt.dd)] [Finite A] {PR : Prog A R P dt.CtlIx dt.SlotIx dt.KIx dt.dd} {I : Type} (F : LaidFile dt A R P I) (hhasP : F.toLayout.HasName PR.zero) [Nonempty A] [L.IsRelational] [L.Structure A] (vi : dt.VarIx) (st : TapeSt dt A R P I) {v : Univ A R P dt.KIx dt.dd → Prop} (tOf : Fin (dt.arOf vi) → dt.X.Tag) (f₀ : dt.CtlIx → A) : dt.CtlIx → A

The control after a completed but failing gate sequence: the whole gates' thread – every block's file test passed and every block's machinery ran – with the flag clear because some block encoded no point.

Equations

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

The whole variable machinery, run

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

What one variable's machinery is charged: the gates' leg, one round, the three sweeps of the entry and the exhaustion test, and then one round and two sweeps per VAL content the loop enumerates.

Equations

• dt.ixVarCost A vi w wP wR wK n = dt.ixVarGatesCost A vi w wP + dt.ixRoundCost A vi w wP wR wK + 3 * wP + 6 + (2 * wP + dt.ixRoundCost A vi w wP wR wK + 3) * n

noncomputable def DescriptiveComplexity.Draw.Data.ixRoundSt {L : FirstOrder.Language} (dt : Data L) {A R P I : Type} (st : TapeSt dt A R P I) (m : I → Prop) : TapeSt dt A R P I

The state of one VAL-loop round: the entry state with the round's VAL content.

Equations

• dt.ixRoundSt st m = { mir := st.mir, tgt := st.tgt, sav := st.sav, val := m, old := st.old, new := st.new, wk := st.wk, bot := st.bot, ltp := st.ltp }

noncomputable def DescriptiveComplexity.Draw.Data.ixValCarry {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)] {I : Type} (F : LaidFile dt A R P I) (m : I → Prop) : Option I

The carry of a VAL round at a coarse file: the greatest register the mark is clear at, every register above it set – what the increment's landing phase names. A file need not have one (an empty file has none), so this is an Option; at the elementwise file it is always some.

Equations

• dt.ixValCarry F m = if h : ∃ (u : I), ¬m u ∧ ∀ (w : I), DescriptiveComplexity.WMLt F.le u w → m w then some h.choose else none

noncomputable def DescriptiveComplexity.Draw.Data.ixCarryBlk {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)] {I : Type} (F : LaidFile dt A R P I) (m : I → Prop) : Option dt.KIx

The block the carry lies in: what a round's store is indexed by.

Equations

• dt.ixCarryBlk F m = (dt.ixValCarry F m).bind F.blk

noncomputable def DescriptiveComplexity.Draw.Data.ixRoundFX {L : FirstOrder.Language} {dt : Data L} {A R P : Type} [Fintype dt.SlotIx] [LinearOrder A] [LinearOrder R] [LinearOrder P] [FirstOrder.Language.wide.Structure (Univ A R P dt.KIx dt.dd)] [Finite A] {PR : Prog A R P dt.CtlIx dt.SlotIx dt.KIx dt.dd} {I : Type} (F : LaidFile dt A R P I) {elt : I → Univ A R P dt.KIx dt.dd} (hinj : Function.Injective elt) (hhasP : F.toLayout.HasName PR.zero) (heltP : ∀ (b : Fin dt.ko ⊕ Fin dt.ki) (c : Fin dt.dd0 → A), elt (F.toLayout.reg hhasP b c) = dt.blkElt b (pad PR.zero c)) [Nonempty A] [L.IsRelational] [L.Structure A] (vi : dt.VarIx) (st : TapeSt dt A R P I) (v : Univ A R P dt.KIx dt.dd → Prop) {ιV : Type} (mV : ιV → I → Prop) (semOf : (a : ιV) → (∀ (ℓ : Fin (dt.nIn vi)), dt.ixIGPassP F PR.zero PR.one vi (dt.ixRoundSt st (mV a)) ℓ) → (b : Fin (dt.natOf vi)) → dt.IxKindSem PR.zero PR.one vi (dt.ixRoundSt st (mV a)) elt (dt.kindOf vi b)) (q : dt.CtlIx → A) (a : ιV) : dt.CtlIx → A

The exit control of one VAL round, at an entry control: the inner gates' thread over the round's register, then – at a passing round only, both flags set – the matrix thread on its output.

Equations

• DescriptiveComplexity.Draw.Data.ixRoundFX F hinj hhasP heltP vi st v mV semOf q a = dt.ixRoundCtl F hinj hhasP heltP ⋯ vi (dt.ixRoundSt st (mV a)) v (semOf a) q

noncomputable def DescriptiveComplexity.Draw.Data.ixVarFM {L : FirstOrder.Language} {dt : Data L} {A R P : Type} [Fintype dt.SlotIx] [LinearOrder A] [LinearOrder R] [LinearOrder P] [FirstOrder.Language.wide.Structure (Univ A R P dt.KIx dt.dd)] [Finite A] {PR : Prog A R P dt.CtlIx dt.SlotIx dt.KIx dt.dd} {I : Type} (F : LaidFile dt A R P I) {elt : I → Univ A R P dt.KIx dt.dd} (hinj : Function.Injective elt) (hhasP : F.toLayout.HasName PR.zero) (heltP : ∀ (b : Fin dt.ko ⊕ Fin dt.ki) (c : Fin dt.dd0 → A), elt (F.toLayout.reg hhasP b c) = dt.blkElt b (pad PR.zero c)) [Nonempty A] [L.IsRelational] [L.Structure A] (vi : dt.VarIx) (st : TapeSt dt A R P I) (v : Univ A R P dt.KIx dt.dd → Prop) {ιV : Type} [LinearOrder ιV] (mV : ιV → I → Prop) (semOf : (a : ιV) → (∀ (ℓ : Fin (dt.nIn vi)), dt.ixIGPassP F PR.zero PR.one vi (dt.ixRoundSt st (mV a)) ℓ) → (b : Fin (dt.natOf vi)) → dt.IxKindSem PR.zero PR.one vi (dt.ixRoundSt st (mV a)) elt (dt.kindOf vi b)) (fG : dt.CtlIx → A) : ιV → dt.CtlIx → A

The VAL loop's entry-control thread: the fold's start at the cleared register, each round the matrix pass folded and stored at the carry's block.

Equations

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

The fold invariant of the VAL loop

The leaf, discharged

The threaded twins of the VAL loop's two threads

A round's exit state is its entry state unless the round's matrix ran a stage atom, which normalizes SAV and TARGET (DescriptiveComplexity.Draw.Data.ixRoundEndSt). Whether it ran at all is the gates' verdict, read off the control entering the round – so the two have to be iterated together, one pair per round, exactly as the spine's nodes are one scale up.

What is threaded is not the state but the two scratch registers (DescriptiveComplexity.Draw.Data.ixRoundEndSt_eq): every other register is the machinery's entry state's, definitionally. That is what keeps the semantic packs available – a pack reads the tape state through the levels' register sets, i.e., through the mirror and VAL alone, so one family indexed by the two registers serves every round, and it can actually be built, which a family over arbitrary states could not be.

@[reducible, inline]

abbrev DescriptiveComplexity.Draw.Data.IxScratch {L : FirstOrder.Language} (_dt : Data L) (_A _R _P I : Type) : Type

The two registers one round of the VAL loop can change.

Equations

• _dt.IxScratch _A _R _P I = ((I → Prop) × (I → Prop))

noncomputable def DescriptiveComplexity.Draw.Data.ixVarRdSt {L : FirstOrder.Language} {dt : Data L} {A R P I : Type} (st : TapeSt dt A R P I) (p : dt.IxScratch A R P I) (m : I → Prop) : TapeSt dt A R P I

The state a round is entered in: the machinery's entry state with the round's two scratch registers and the register it enumerates.

Equations

• DescriptiveComplexity.Draw.Data.ixVarRdSt st p m = { mir := st.mir, tgt := p.2, sav := p.1, val := m, old := st.old, new := st.new, wk := st.wk, bot := st.bot, ltp := st.ltp }

noncomputable def DescriptiveComplexity.Draw.Data.ixVarPairT {L : FirstOrder.Language} {dt : Data L} {A R P : Type} [Fintype dt.SlotIx] [LinearOrder A] [LinearOrder R] [LinearOrder P] [FirstOrder.Language.wide.Structure (Univ A R P dt.KIx dt.dd)] [Finite A] {PR : Prog A R P dt.CtlIx dt.SlotIx dt.KIx dt.dd} {I : Type} (F : LaidFile dt A R P I) {elt : I → Univ A R P dt.KIx dt.dd} (hinj : Function.Injective elt) (hhasP : F.toLayout.HasName PR.zero) (heltP : ∀ (b : Fin dt.ko ⊕ Fin dt.ki) (c : Fin dt.dd0 → A), elt (F.toLayout.reg hhasP b c) = dt.blkElt b (pad PR.zero c)) [Nonempty A] [L.IsRelational] [L.Structure A] (vi : dt.VarIx) (st : TapeSt dt A R P I) (v : Univ A R P dt.KIx dt.dd → Prop) {ιV : Type} [LinearOrder ιV] (mV : ιV → I → Prop) (semT : (p : dt.IxScratch A R P I) → (a : ιV) → (∀ (ℓ : Fin (dt.nIn vi)), dt.ixIGPassP F PR.zero PR.one vi (ixVarRdSt st p (mV a)) ℓ) → (b : Fin (dt.natOf vi)) → dt.IxKindSem PR.zero PR.one vi (dt.ixMatSt vi (ixVarRdSt st p (mV a)) v ↑b) elt (dt.kindOf vi b)) (fG : dt.CtlIx → A) : ιV → dt.IxScratch A R P I × (dt.CtlIx → A)

The VAL loop's thread: the two scratch registers beside the control, the fold's start at the cleared register, and at each cover the round's exit – the store taken against the background the round ends in.

Equations

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

noncomputable def DescriptiveComplexity.Draw.Data.ixVarSTT {L : FirstOrder.Language} {dt : Data L} {A R P : Type} [Fintype dt.SlotIx] [LinearOrder A] [LinearOrder R] [LinearOrder P] [FirstOrder.Language.wide.Structure (Univ A R P dt.KIx dt.dd)] [Finite A] {PR : Prog A R P dt.CtlIx dt.SlotIx dt.KIx dt.dd} {I : Type} (F : LaidFile dt A R P I) {elt : I → Univ A R P dt.KIx dt.dd} (hinj : Function.Injective elt) (hhasP : F.toLayout.HasName PR.zero) (heltP : ∀ (b : Fin dt.ko ⊕ Fin dt.ki) (c : Fin dt.dd0 → A), elt (F.toLayout.reg hhasP b c) = dt.blkElt b (pad PR.zero c)) [Nonempty A] [L.IsRelational] [L.Structure A] (vi : dt.VarIx) (st : TapeSt dt A R P I) (v : Univ A R P dt.KIx dt.dd → Prop) {ιV : Type} [LinearOrder ιV] (mV : ιV → I → Prop) (semT : (p : dt.IxScratch A R P I) → (a : ιV) → (∀ (ℓ : Fin (dt.nIn vi)), dt.ixIGPassP F PR.zero PR.one vi (ixVarRdSt st p (mV a)) ℓ) → (b : Fin (dt.natOf vi)) → dt.IxKindSem PR.zero PR.one vi (dt.ixMatSt vi (ixVarRdSt st p (mV a)) v ↑b) elt (dt.kindOf vi b)) (fG : dt.CtlIx → A) (a : ιV) : dt.IxScratch A R P I

The scratch family of the VAL loop.

Equations

• DescriptiveComplexity.Draw.Data.ixVarSTT F hinj hhasP heltP vi st v mV semT fG a = (DescriptiveComplexity.Draw.Data.ixVarPairT F hinj hhasP heltP vi st v mV semT fG a).1

noncomputable def DescriptiveComplexity.Draw.Data.ixVarStT {L : FirstOrder.Language} {dt : Data L} {A R P : Type} [Fintype dt.SlotIx] [LinearOrder A] [LinearOrder R] [LinearOrder P] [FirstOrder.Language.wide.Structure (Univ A R P dt.KIx dt.dd)] [Finite A] {PR : Prog A R P dt.CtlIx dt.SlotIx dt.KIx dt.dd} {I : Type} (F : LaidFile dt A R P I) {elt : I → Univ A R P dt.KIx dt.dd} (hinj : Function.Injective elt) (hhasP : F.toLayout.HasName PR.zero) (heltP : ∀ (b : Fin dt.ko ⊕ Fin dt.ki) (c : Fin dt.dd0 → A), elt (F.toLayout.reg hhasP b c) = dt.blkElt b (pad PR.zero c)) [Nonempty A] [L.IsRelational] [L.Structure A] (vi : dt.VarIx) (st : TapeSt dt A R P I) (v : Univ A R P dt.KIx dt.dd → Prop) {ιV : Type} [LinearOrder ιV] (mV : ιV → I → Prop) (semT : (p : dt.IxScratch A R P I) → (a : ιV) → (∀ (ℓ : Fin (dt.nIn vi)), dt.ixIGPassP F PR.zero PR.one vi (ixVarRdSt st p (mV a)) ℓ) → (b : Fin (dt.natOf vi)) → dt.IxKindSem PR.zero PR.one vi (dt.ixMatSt vi (ixVarRdSt st p (mV a)) v ↑b) elt (dt.kindOf vi b)) (fG : dt.CtlIx → A) (a : ιV) : TapeSt dt A R P I

The tape family of the VAL loop – the state each round is entered in.

Equations

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

noncomputable def DescriptiveComplexity.Draw.Data.ixVarFMT {L : FirstOrder.Language} {dt : Data L} {A R P : Type} [Fintype dt.SlotIx] [LinearOrder A] [LinearOrder R] [LinearOrder P] [FirstOrder.Language.wide.Structure (Univ A R P dt.KIx dt.dd)] [Finite A] {PR : Prog A R P dt.CtlIx dt.SlotIx dt.KIx dt.dd} {I : Type} (F : LaidFile dt A R P I) {elt : I → Univ A R P dt.KIx dt.dd} (hinj : Function.Injective elt) (hhasP : F.toLayout.HasName PR.zero) (heltP : ∀ (b : Fin dt.ko ⊕ Fin dt.ki) (c : Fin dt.dd0 → A), elt (F.toLayout.reg hhasP b c) = dt.blkElt b (pad PR.zero c)) [Nonempty A] [L.IsRelational] [L.Structure A] (vi : dt.VarIx) (st : TapeSt dt A R P I) (v : Univ A R P dt.KIx dt.dd → Prop) {ιV : Type} [LinearOrder ιV] (mV : ιV → I → Prop) (semT : (p : dt.IxScratch A R P I) → (a : ιV) → (∀ (ℓ : Fin (dt.nIn vi)), dt.ixIGPassP F PR.zero PR.one vi (ixVarRdSt st p (mV a)) ℓ) → (b : Fin (dt.natOf vi)) → dt.IxKindSem PR.zero PR.one vi (dt.ixMatSt vi (ixVarRdSt st p (mV a)) v ↑b) elt (dt.kindOf vi b)) (fG : dt.CtlIx → A) (a : ιV) : dt.CtlIx → A

The control family of the VAL loop, threaded – the twin of DescriptiveComplexity.Draw.Data.ixVarFM.

Equations

• DescriptiveComplexity.Draw.Data.ixVarFMT F hinj hhasP heltP vi st v mV semT fG a = (DescriptiveComplexity.Draw.Data.ixVarPairT F hinj hhasP heltP vi st v mV semT fG a).2

noncomputable def DescriptiveComplexity.Draw.Data.ixVarStE {L : FirstOrder.Language} {dt : Data L} {A R P : Type} [Fintype dt.SlotIx] [LinearOrder A] [LinearOrder R] [LinearOrder P] [FirstOrder.Language.wide.Structure (Univ A R P dt.KIx dt.dd)] [Finite A] {PR : Prog A R P dt.CtlIx dt.SlotIx dt.KIx dt.dd} {I : Type} (F : LaidFile dt A R P I) {elt : I → Univ A R P dt.KIx dt.dd} (hinj : Function.Injective elt) (hhasP : F.toLayout.HasName PR.zero) (heltP : ∀ (b : Fin dt.ko ⊕ Fin dt.ki) (c : Fin dt.dd0 → A), elt (F.toLayout.reg hhasP b c) = dt.blkElt b (pad PR.zero c)) [Nonempty A] [L.IsRelational] [L.Structure A] (vi : dt.VarIx) (st : TapeSt dt A R P I) (v : Univ A R P dt.KIx dt.dd → Prop) {ιV : Type} [LinearOrder ιV] (mV : ιV → I → Prop) (semT : (p : dt.IxScratch A R P I) → (a : ιV) → (∀ (ℓ : Fin (dt.nIn vi)), dt.ixIGPassP F PR.zero PR.one vi (ixVarRdSt st p (mV a)) ℓ) → (b : Fin (dt.natOf vi)) → dt.IxKindSem PR.zero PR.one vi (dt.ixMatSt vi (ixVarRdSt st p (mV a)) v ↑b) elt (dt.kindOf vi b)) (fG : dt.CtlIx → A) (a : ιV) : TapeSt dt A R P I

The state one round ends in – the next round's entry state at a cover, and the loop's exit state at the top.

Equations

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

noncomputable def DescriptiveComplexity.Draw.Data.ixVarFXT {L : FirstOrder.Language} {dt : Data L} {A R P : Type} [Fintype dt.SlotIx] [LinearOrder A] [LinearOrder R] [LinearOrder P] [FirstOrder.Language.wide.Structure (Univ A R P dt.KIx dt.dd)] [Finite A] {PR : Prog A R P dt.CtlIx dt.SlotIx dt.KIx dt.dd} {I : Type} (F : LaidFile dt A R P I) {elt : I → Univ A R P dt.KIx dt.dd} (hinj : Function.Injective elt) (hhasP : F.toLayout.HasName PR.zero) (heltP : ∀ (b : Fin dt.ko ⊕ Fin dt.ki) (c : Fin dt.dd0 → A), elt (F.toLayout.reg hhasP b c) = dt.blkElt b (pad PR.zero c)) [Nonempty A] [L.IsRelational] [L.Structure A] (vi : dt.VarIx) (st : TapeSt dt A R P I) (v : Univ A R P dt.KIx dt.dd → Prop) {ιV : Type} [LinearOrder ιV] (mV : ιV → I → Prop) (semT : (p : dt.IxScratch A R P I) → (a : ιV) → (∀ (ℓ : Fin (dt.nIn vi)), dt.ixIGPassP F PR.zero PR.one vi (ixVarRdSt st p (mV a)) ℓ) → (b : Fin (dt.natOf vi)) → dt.IxKindSem PR.zero PR.one vi (dt.ixMatSt vi (ixVarRdSt st p (mV a)) v ↑b) elt (dt.kindOf vi b)) (fG : dt.CtlIx → A) (a : ιV) : dt.CtlIx → A

The exit control of one VAL round, threaded – the twin of DescriptiveComplexity.Draw.Data.ixRoundFX, at the state the round's atoms actually run at.

Equations

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

The threaded loop is the unthreaded one

The VAL loop's rounds run at states that differ from the machinery's entry state in SAV and TARGET alone, and every control they compute is blind to that difference (DescriptiveComplexity.Draw.Data.ixRoundCtlT_eq_ixRoundCtl, DescriptiveComplexity.Draw.Data.ixRoundCtl_congr_scratch). What the threading can change is the semantic pack, since a family indexed by the scratch registers may pick different points at different registers; so the bridge is stated at a pack that is one unthreaded pack transported (ixSemCastT), which is what a reduction supplies (DescriptiveComplexity.Draw.Data.gatedSem, whose points are the address's blocks and nothing else).

noncomputable def DescriptiveComplexity.Draw.Data.ixVarFG {L : FirstOrder.Language} {dt : Data L} {A R P : Type} [Fintype dt.SlotIx] [LinearOrder A] [LinearOrder R] [LinearOrder P] [FirstOrder.Language.wide.Structure (Univ A R P dt.KIx dt.dd)] [Finite A] {PR : Prog A R P dt.CtlIx dt.SlotIx dt.KIx dt.dd} {I : Type} (F : LaidFile dt A R P I) (hhasP : F.toLayout.HasName PR.zero) [Nonempty A] [L.IsRelational] [L.Structure A] (vi : dt.VarIx) (st : TapeSt dt A R P I) (v : Univ A R P dt.KIx dt.dd → Prop) (tOf : Fin (dt.arOf vi) → dt.X.Tag) (f₀ : dt.CtlIx → A) : dt.CtlIx → A

The control the gates leave, at the reduction's own budgets – what both forms of the machinery's run start their VAL loop from.

Equations

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