The evaluation spine's run

The run theorem of DescriptiveComplexity.Draw.Data.evalRule: from the checkpoint before the first variable to the checkpoint after the last, one abstract sub-machinery run per position – the spine contributes only its dispatches and walk-backs, so it needs to know nothing about a machinery's internals beyond its entry phase, its control transform and its tape transform.

The run comes with its cost (eval_reachesIn): one machinery's width plus its dispatch and its walk back, once per variable. eval_run is it with the budget forgotten.

The two boundary steps at the last checkpoint – erase the marker rightwards into the sweep's advance, or into the post-sweep reset at the ltp cell – are separate single-step lemmas, consumed by the outer composition.

theorem DescriptiveComplexity.Draw.Data.eval_run {L : FirstOrder.Language} (dt : Data L) {A R Q PM SM : Type} {nv : ℕ} [Fintype Q] [Fintype dt.SlotIx] [LinearOrder A] [LinearOrder R] [LinearOrder (OuterPh (EvalPh nv PM))] [FirstOrder.Language.wide.Structure (Univ A R (OuterPh (EvalPh nv PM)) dt.KIx dt.dd)] [Finite A] [Finite R] [Finite (OuterPh (EvalPh nv PM))] {ShM : SM → Type} {PR : Prog A R (OuterPh (EvalPh nv PM)) Q dt.SlotIx dt.KIx dt.dd} {I : Type} {ile : I → I → Prop} (RF : IxFile (Univ A R (OuterPh (EvalPh nv PM)) dt.KIx dt.dd) I ile) {ruleM : (s : SM) → ShM s → Rule A Q dt.SlotIx (OuterPh (EvalPh nv PM))} {subEntry : Fin nv → PM} {rEmb : (i : EvalSite nv SM) → EvalSh nv SM ShM i → R} (hrules : ∀ (i : EvalSite nv SM) (ρ : EvalSh nv SM ShM i), PR.rules (rEmb i ρ) = dt.evalRule PR.zero PR.one ruleM subEntry i ρ) (hR : PR.table.Reads) (hlin : IsLinOrd WMLe) (hix : IsLinOrd ile) {gbot : I} (hbot : ∀ (y : I), ile gbot y) {v v' : Univ A R (OuterPh (EvalPh nv PM)) dt.KIx dt.dd → Prop} (hv : WMSetLt WMLe v (RF.cell gbot)) (hvi : WMIncr WMLe v v') {restOf : Fin (nv + 1) → (Univ A R (OuterPh (EvalPh nv PM)) dt.KIx dt.dd → Prop) → dt.SlotIx → A} {mvOf : Fin (nv + 1) → I → Prop} (hwkOf : ∀ (k : Fin (nv + 1)) (r : Univ A R (OuterPh (EvalPh nv PM)) dt.KIx dt.dd → Prop), restOf k r Slot.wk = bitVal PR.zero PR.one (r = v)) (hrgOf : ∀ (k : Fin (nv + 1)) (r : Univ A R (OuterPh (EvalPh nv PM)) dt.KIx dt.dd → Prop), restOf k r Slot.reg = bitVal PR.zero PR.one (∃ (u : I), r = RF.cell u)) (fs : Fin (nv + 1) → Q → A) (hVarR : ∀ (k : Fin nv), Relation.ReflTransGen (wideData (Univ A R (OuterPh (EvalPh nv PM)) dt.KIx dt.dd)).Step { state := Sum.inr (PR.stElt (OuterPh.evalP (EvalPh.sub (subEntry k))) (fs k.castSucc)), head := Sum.inl v', tape := wideTape (PR.trackTapeAt RF.cell Slot.val (restOf k.castSucc) (mvOf k.castSucc)) (PR.syElt PR.blank) } { state := Sum.inr (PR.stElt (OuterPh.evalP (EvalPh.chk k.succ)) (fs k.succ)), head := Sum.inl v', tape := wideTape (PR.trackTapeAt RF.cell Slot.val (restOf k.succ) (mvOf k.succ)) (PR.syElt PR.blank) }) : Relation.ReflTransGen (wideData (Univ A R (OuterPh (EvalPh nv PM)) dt.KIx dt.dd)).Step { state := Sum.inr (PR.stElt (OuterPh.evalP (EvalPh.chk 0)) (fs 0)), head := Sum.inl v, tape := wideTape (PR.trackTapeAt RF.cell Slot.val (restOf 0) (mvOf 0)) (PR.syElt PR.blank) } { state := Sum.inr (PR.stElt (OuterPh.evalP (EvalPh.chk (Fin.last nv))) (fs (Fin.last nv))), head := Sum.inl v, tape := wideTape (PR.trackTapeAt RF.cell Slot.val (restOf (Fin.last nv)) (mvOf (Fin.last nv))) (PR.syElt PR.blank) }

The spine's run, the budget forgotten: what a space-bounded caller reads, its machineries' runs carrying no count.