The clocked evaluation's spine

The space-bounded spine (DescriptiveComplexity.Draw.Data.evalRule) ends its last checkpoint in one of two outer phases – the sweep's advance, or the post-sweep reset – because it runs inside an iteration. A clocked program has neither: its evaluation runs once, and its last checkpoint leaves into whatever phase the caller names. So the spine's rules are not the space-bounded ones at another embedding; they are two rules per checkpoint instead of three, at the clocked program's own phases (DescriptiveComplexity.Draw.NexPh).

Everything else is shared: the sites are DescriptiveComplexity.Draw.EvalSite, the machineries' rules are the parameter, and the ownership and separation proofs are the same case analysis with the dead third rule gone.

The run is nexEval_reachesIn, and it is the space-bounded spine's count with the same shape: one machinery's width plus its dispatch and its walk back, once per variable.

The file also assembles the program: the spine's rules at the shared machineries – a clocked program's tower above the atom is the space-bounded one, PMF, SMF, SEF and varRuleF and all – with nexEvalHosrcF/nexEvalSepF, and nexProg – the outer layer's rules at the two sweep specifications with the evaluation's as their parameter. That last is built directly rather than through DescriptiveComplexity.Draw.Assembly, because a clocked program is not deterministic: its guess site fires three rules on the same data, which is the one piece of nondeterminism it has, and what does hold there is DescriptiveComplexity.Draw.Data.nexSep_postGuess.

inductive DescriptiveComplexity.Draw.NexEvalChkRule : Type

The rules of a clocked checkpoint: the walk back to the marker, and the one dispatch – into the variable's machinery below the last checkpoint, out of the evaluation at it.

• stay : NexEvalChkRule

  Walk left back to the marker.

• dsp : NexEvalChkRule

  Dispatch: into the machinery, or out of the evaluation.

@[instance_reducible]

instance DescriptiveComplexity.Draw.instDecidableEqNexEvalChkRule : DecidableEq NexEvalChkRule

Equations

• DescriptiveComplexity.Draw.instDecidableEqNexEvalChkRule x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance DescriptiveComplexity.Draw.instFiniteNexEvalChkRule : Finite NexEvalChkRule

def DescriptiveComplexity.Draw.NexEvalSh (nv : ℕ) (SM : Type) (ShM : SM → Type) : EvalSite nv SM → Type

The rule shape of each clocked evaluation site.

Equations

• DescriptiveComplexity.Draw.NexEvalSh nv SM ShM (DescriptiveComplexity.Draw.EvalSite.chk a) = DescriptiveComplexity.Draw.NexEvalChkRule
• DescriptiveComplexity.Draw.NexEvalSh nv SM ShM (DescriptiveComplexity.Draw.EvalSite.sub s) = ShM s

noncomputable def DescriptiveComplexity.Draw.Data.nexEvalRule {L : FirstOrder.Language} (dt : Data L) {A Q PM SM B : Type} {nv : ℕ} (one : A) {ShM : SM → Type} (ruleM : (s : SM) → ShM s → Rule A Q dt.SlotIx (NexPh B (EvalPh nv PM))) (subEntry : Fin nv → PM) (exitPh : NexPh B (EvalPh nv PM)) (i : EvalSite nv SM) : NexEvalSh nv SM ShM i → Rule A Q dt.SlotIx (NexPh B (EvalPh nv PM))

The rules of a clocked evaluation's spine: per checkpoint the walk back and the dispatch; the sub-machineries' rules are the parameter, and the exit at the last checkpoint is the caller's phase.

Equations

• One or more equations did not get rendered due to their size.
• dt.nexEvalRule one ruleM subEntry exitPh (DescriptiveComplexity.Draw.EvalSite.sub s) ρ = ruleM s ρ

theorem DescriptiveComplexity.Draw.Data.nexEvalHosrc {L : FirstOrder.Language} (dt : Data L) {A Q PM SM B : Type} {nv : ℕ} (one : A) {ShM : SM → Type} {ruleM : (s : SM) → ShM s → Rule A Q dt.SlotIx (NexPh B (EvalPh nv PM))} {subEntry : Fin nv → PM} {ownM : PM → SM} {exitPh : NexPh B (EvalPh nv PM)} (hosrcM : ∀ (s : SM) (ρ : ShM s), ∃ (p : PM), (ruleM s ρ).srcPh = NexPh.evalP (EvalPh.sub p) ∧ ownM p = s) (e : EvalSite nv SM) (ρ : NexEvalSh nv SM ShM e) : ∃ (p : EvalPh nv PM), (dt.nexEvalRule one ruleM subEntry exitPh e ρ).srcPh = NexPh.evalP p ∧ evalOwn ownM p = e

Every clocked spine rule fires from a phase its site owns; the sub-machineries' obligation is the parameter.

theorem DescriptiveComplexity.Draw.Data.nexEvalSep {L : FirstOrder.Language} (dt : Data L) {A Q PM SM B : Type} {nv : ℕ} (one : A) {ShM : SM → Type} {ruleM : (s : SM) → ShM s → Rule A Q dt.SlotIx (NexPh B (EvalPh nv PM))} {subEntry : Fin nv → PM} {exitPh : NexPh B (EvalPh nv PM)} (hsepM : ∀ (s : SM) (ρ ρ' : ShM s) (f : Q → A) (g : dt.SlotIx → A), (ruleM s ρ).guard f g → (ruleM s ρ').guard f g → (ruleM s ρ).srcPh = (ruleM s ρ').srcPh → ρ = ρ') (e : EvalSite nv SM) (ρ ρ' : NexEvalSh nv SM ShM e) (f : Q → A) (g : dt.SlotIx → A) : (dt.nexEvalRule one ruleM subEntry exitPh e ρ).guard f g → (dt.nexEvalRule one ruleM subEntry exitPh e ρ').guard f g → (dt.nexEvalRule one ruleM subEntry exitPh e ρ).srcPh = (dt.nexEvalRule one ruleM subEntry exitPh e ρ').srcPh → ρ = ρ'

The clocked spine separates in-shape: per checkpoint, the walk's guard is disjoint from the dispatch's, and there is no third rule to tell apart.

theorem DescriptiveComplexity.Draw.Data.nexEvalRule_dstIn {L : FirstOrder.Language} (dt : Data L) {A Q PM SM B : Type} {nv : ℕ} (one : A) {ShM : SM → Type} {ruleM : (s : SM) → ShM s → Rule A Q dt.SlotIx (NexPh B (EvalPh nv PM))} {subEntry : Fin nv → PM} {exitPh : NexPh B (EvalPh nv PM)} {S : NexPh B (EvalPh nv PM) → Prop} (hemb : ∀ (p : EvalPh nv PM), S (NexPh.evalP p)) (hexit : S exitPh) (hM : ∀ (s : SM) (ρ : ShM s), S (ruleM s ρ).dstPh) (e : EvalSite nv SM) (ρ : NexEvalSh nv SM ShM e) : S (dt.nexEvalRule one ruleM subEntry exitPh e ρ).dstPh

A property of the spine's phases and its exit holds of every phase it can move to, given it holds of every phase a machinery can move to.

The spine at the clocked machineries

The types of the spine, and its rules at the clocked variable machineries: what DescriptiveComplexity.Draw.Data.nexRule takes as its evaluation parameter. The phases are EvalPh over the machineries', as in the space-bounded program; only the machineries are the clocked ones and the exit is the accepting phase.

noncomputable def DescriptiveComplexity.Draw.Data.NexSESh {L : FirstOrder.Language} (dt : Data L) : dt.SEF → Type

The rule shape of the clocked evaluation's sites: the spine's own, two rules per checkpoint, over the machinery sites of the shared tower.

Equations

• dt.NexSESh = DescriptiveComplexity.Draw.NexEvalSh dt.nv dt.SMF dt.SMSh

noncomputable def DescriptiveComplexity.Draw.Data.nexSmRule {L : FirstOrder.Language} (dt : Data L) {A Q B : Type} (zero one : A) (args : (v : dt.VarIx) → dt.VarArgs v) (s : dt.SMF) : dt.SMSh s → Rule A Q dt.SlotIx (NexPh B (EvalPh dt.nv dt.PMF))

The rules of the clocked evaluation's machineries: one copy of the clocked variable machinery per spine position – its exit the next checkpoint – and the output's, whose exit is the accepting phase.

Equations

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

noncomputable def DescriptiveComplexity.Draw.Data.nexEvalRuleF {L : FirstOrder.Language} (dt : Data L) {A Q B : Type} (zero one : A) (args : (v : dt.VarIx) → dt.VarArgs v) (e : dt.SEF) : dt.NexSESh e → Rule A Q dt.SlotIx (NexPh B (EvalPh dt.nv dt.PMF))

The rules of the clocked evaluation: the spine over the machineries, leaving at the last checkpoint into the output's machinery, whose own exit is the accepting phase. The accepting predicate reads that machinery's verdict bit, so the evaluation has to run it: a last checkpoint that went straight to acceptP would leave the bit unwritten.

Equations

• dt.nexEvalRuleF zero one args = dt.nexEvalRule one (dt.nexSmRule zero one args) dt.smEntry (DescriptiveComplexity.Draw.NexPh.evalP (DescriptiveComplexity.Draw.EvalPh.sub dt.smEntryOut))

theorem DescriptiveComplexity.Draw.Data.nexSmHosrc {L : FirstOrder.Language} {dt : Data L} {A Q B : Type} {zero one : A} (args : (v : dt.VarIx) → dt.VarArgs v) (s : dt.SMF) (ρ : dt.SMSh s) : ∃ (p : dt.PMF), (dt.nexSmRule zero one args s ρ).srcPh = NexPh.evalP (EvalPh.sub p) ∧ dt.smOwn p = s

Every rule of the clocked evaluation's machineries fires from a phase its site owns.

theorem DescriptiveComplexity.Draw.Data.nexSmSep {L : FirstOrder.Language} {dt : Data L} {A Q B : Type} {zero one : A} (hzo : zero ≠ one) (args : (v : dt.VarIx) → dt.VarArgs v) (s : dt.SMF) (ρ ρ' : dt.SMSh s) (f : Q → A) (g : dt.SlotIx → A) : (dt.nexSmRule zero one args s ρ).guard f g → (dt.nexSmRule zero one args s ρ').guard f g → (dt.nexSmRule zero one args s ρ).srcPh = (dt.nexSmRule zero one args s ρ').srcPh → ρ = ρ'

The clocked evaluation's machineries separate in-shape.

theorem DescriptiveComplexity.Draw.Data.nexEvalHosrcF {L : FirstOrder.Language} {dt : Data L} {A Q B : Type} {zero one : A} (args : (v : dt.VarIx) → dt.VarArgs v) (e : dt.SEF) (ρ : dt.NexSESh e) : ∃ (p : EvalPh dt.nv dt.PMF), (dt.nexEvalRuleF zero one args e ρ).srcPh = NexPh.evalP p ∧ dt.seOwn p = e

Every rule of the clocked evaluation fires from a phase its site owns.

theorem DescriptiveComplexity.Draw.Data.nexEvalSepF {L : FirstOrder.Language} {dt : Data L} {A Q B : Type} {zero one : A} (hzo : zero ≠ one) (args : (v : dt.VarIx) → dt.VarArgs v) (e : dt.SEF) (ρ ρ' : dt.NexSESh e) (f : Q → A) (g : dt.SlotIx → A) : (dt.nexEvalRuleF zero one args e ρ).guard f g → (dt.nexEvalRuleF zero one args e ρ').guard f g → (dt.nexEvalRuleF zero one args e ρ).srcPh = (dt.nexEvalRuleF zero one args e ρ').srcPh → ρ = ρ'

The clocked evaluation separates in-shape.

theorem DescriptiveComplexity.Draw.Data.nexSmRule_dstIn {L : FirstOrder.Language} {dt : Data L} {A B : Type} {zero one : A} {S : NexPh B (EvalPh dt.nv dt.PMF) → Prop} (args : (v : dt.VarIx) → dt.VarArgs v) (hemb : ∀ (p : EvalPh dt.nv dt.PMF), S (NexPh.evalP p)) (hacc : S NexPh.acceptP) (s : dt.SMF) (ρ : dt.SMSh s) : S (dt.nexSmRule zero one args s ρ).dstPh

A property of the evaluation's phases and its accepting phase holds of every phase a machinery can move to.

theorem DescriptiveComplexity.Draw.Data.nexEvalRuleF_postGuess {L : FirstOrder.Language} {dt : Data L} {A B : Type} {zero one : A} (args : (v : dt.VarIx) → dt.VarArgs v) (e : dt.SEF) (ρ : dt.NexSESh e) : (dt.nexEvalRuleF zero one args e ρ).dstPh.PostGuess

The clocked evaluation never leaves the post-guess phases: every phase its rules can move to is the evaluation's own or the accepting one, and NexPh.PostGuess holds of both. This is the one fact DescriptiveComplexity.Draw.Data.nexProg_uniqueFrom takes from the evaluation, and the tower discharges it layer by layer down to the trips.

The clocked program

The rule set assembled: the outer layer's rules at the two sweep specifications, with the evaluation's as their parameter. Unlike the space-bounded program this is not an DescriptiveComplexity.Draw.Assembly – the guess site fires three rules on the same data, which is the program's one piece of nondeterminism – so the record is built directly and the separation that does hold is DescriptiveComplexity.Draw.Data.nexSep_postGuess.

@[reducible, inline]

noncomputable abbrev DescriptiveComplexity.Draw.Data.NexRIx {L : FirstOrder.Language} (dt : Data L) {G : Type} : Type

The rule names of the clocked program: a site of its outer layer, or of its evaluation, and one of that site's rules.

Equations

• dt.NexRIx = ((i : DescriptiveComplexity.Draw.NexSite dt.SEF) × DescriptiveComplexity.Draw.NexSh dt.SEF (Option dt.KIx) G dt.NexSESh i)

noncomputable def DescriptiveComplexity.Draw.Data.nexProg {L : FirstOrder.Language} (dt : Data L) {A G : Type} [Fintype dt.CtlIx] [Fintype dt.SlotIx] [DecidableEq dt.SlotIx] [LinearOrder A] [Finite A] [Finite dt.KIx] [Nonempty A] (zero one : A) (hzo : zero ≠ one) (hpl : Fintype.card (dt.CtlIx ⊕ dt.SlotIx) ≤ dt.dd) (coord : Fin dt.dd → dt.CtlIx) (β : SweepSpec A dt.CtlIx dt.SlotIx (Option dt.KIx)) (γ : GuessSpec A dt.CtlIx dt.SlotIx (Option dt.KIx) G) (args : (v : dt.VarIx) → dt.VarArgs v) (bot : Option dt.KIx) : Prog A dt.NexRIx (NexPh (Option dt.KIx) (EvalPh dt.nv dt.PMF)) dt.CtlIx dt.SlotIx dt.KIx dt.dd

The clocked program: the outer layer's rules – the opening step, the build sweep, the walk home, the guess sweep, the walk home – with the clocked evaluation's as their parameter, and the reduction's constants. The accepting phase is the outer layer's, and its verdict is read from the control exactly as the space-bounded program's is.

Equations

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

theorem DescriptiveComplexity.Draw.Data.nexProg_rules {L : FirstOrder.Language} {dt : Data L} {A G : Type} [Fintype dt.CtlIx] [Fintype dt.SlotIx] [DecidableEq dt.SlotIx] [LinearOrder A] [Finite A] [Finite dt.KIx] [Nonempty A] {zero one : A} (hzo : zero ≠ one) (hpl : Fintype.card (dt.CtlIx ⊕ dt.SlotIx) ≤ dt.dd) {coord : Fin dt.dd → dt.CtlIx} {β : SweepSpec A dt.CtlIx dt.SlotIx (Option dt.KIx)} {γ : GuessSpec A dt.CtlIx dt.SlotIx (Option dt.KIx) G} {args : (v : dt.VarIx) → dt.VarArgs v} {bot : Option dt.KIx} (i : NexSite dt.SEF) (ρ : NexSh dt.SEF (Option dt.KIx) G dt.NexSESh i) : (dt.nexProg zero one hzo hpl coord β γ args bot).rules ⟨i, ρ⟩ = dt.nexRule one β γ (dt.nexEvalRuleF zero one args) (EvalPh.chk 0) bot i ρ

The clocked program's rules, at a rule name: what every run lemma's rule hypothesis is discharged by.

theorem DescriptiveComplexity.Draw.Data.nexEval_reachesIn {L : FirstOrder.Language} {dt : Data L} {A R Q PM SM B : Type} {nv : ℕ} [Fintype Q] [Fintype dt.SlotIx] [LinearOrder A] [LinearOrder R] [LinearOrder (NexPh B (EvalPh nv PM))] [FirstOrder.Language.wide.Structure (Univ A R (NexPh B (EvalPh nv PM)) dt.KIx dt.dd)] [Finite A] [Finite R] [Finite (NexPh B (EvalPh nv PM))] {ShM : SM → Type} {PR : Prog A R (NexPh B (EvalPh nv PM)) Q dt.SlotIx dt.KIx dt.dd} {I : Type} {ile : I → I → Prop} (RF : IxFile (Univ A R (NexPh B (EvalPh nv PM)) dt.KIx dt.dd) I ile) {ruleM : (s : SM) → ShM s → Rule A Q dt.SlotIx (NexPh B (EvalPh nv PM))} {subEntry : Fin nv → PM} {exitPh : NexPh B (EvalPh nv PM)} {rEmb : (i : EvalSite nv SM) → NexEvalSh nv SM ShM i → R} (hrules : ∀ (i : EvalSite nv SM) (ρ : NexEvalSh nv SM ShM i), PR.rules (rEmb i ρ) = dt.nexEvalRule PR.one ruleM subEntry exitPh i ρ) (hR : PR.table.Reads) (hlin : IsLinOrd WMLe) (hix : IsLinOrd ile) {gbot : I} (hbot : ∀ (y : I), ile gbot y) {v v' : Univ A R (NexPh B (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 (NexPh B (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 (NexPh B (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 (NexPh B (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) (w : ℕ) (hVar : ∀ (k : Fin nv), (wideData (Univ A R (NexPh B (EvalPh nv PM)) dt.KIx dt.dd)).ReachesIn w { state := Sum.inr (PR.stElt (NexPh.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 (NexPh.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) }) : (wideData (Univ A R (NexPh B (EvalPh nv PM)) dt.KIx dt.dd)).ReachesIn ((w + 2) * nv) { state := Sum.inr (PR.stElt (NexPh.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 (NexPh.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, on a clock: from the checkpoint before the first variable at the marker to the checkpoint after the last, one machinery run per position, each with its dispatch and its walk back.

theorem DescriptiveComplexity.Draw.Data.step_nexEvalBack {L : FirstOrder.Language} {dt : Data L} {A R Q PM SM B : Type} {nv : ℕ} [Fintype Q] [Fintype dt.SlotIx] [LinearOrder A] [LinearOrder R] [LinearOrder (NexPh B (EvalPh nv PM))] [FirstOrder.Language.wide.Structure (Univ A R (NexPh B (EvalPh nv PM)) dt.KIx dt.dd)] [Finite A] [Finite R] [Finite (NexPh B (EvalPh nv PM))] {ShM : SM → Type} {PR : Prog A R (NexPh B (EvalPh nv PM)) Q dt.SlotIx dt.KIx dt.dd} {I : Type} {ile : I → I → Prop} (RF : IxFile (Univ A R (NexPh B (EvalPh nv PM)) dt.KIx dt.dd) I ile) {ruleM : (s : SM) → ShM s → Rule A Q dt.SlotIx (NexPh B (EvalPh nv PM))} {subEntry : Fin nv → PM} {exitPh : NexPh B (EvalPh nv PM)} {rEmb : (i : EvalSite nv SM) → NexEvalSh nv SM ShM i → R} (hrules : ∀ (i : EvalSite nv SM) (ρ : NexEvalSh nv SM ShM i), PR.rules (rEmb i ρ) = dt.nexEvalRule PR.one ruleM subEntry exitPh i ρ) (hR : PR.table.Reads) (hlin : IsLinOrd WMLe) {v v' : Univ A R (NexPh B (EvalPh nv PM)) dt.KIx dt.dd → Prop} (hvi : WMIncr WMLe v v') {rest : (Univ A R (NexPh B (EvalPh nv PM)) dt.KIx dt.dd → Prop) → dt.SlotIx → A} {m : I → Prop} {f : Q → A} (k : Fin (nv + 1)) (hwk : ∀ (r : Univ A R (NexPh B (EvalPh nv PM)) dt.KIx dt.dd → Prop), rest r Slot.wk = bitVal PR.zero PR.one (r = v)) : (wideData (Univ A R (NexPh B (EvalPh nv PM)) dt.KIx dt.dd)).Step { state := Sum.inr (PR.stElt (NexPh.evalP (EvalPh.chk k)) f), head := Sum.inl v', tape := wideTape (PR.trackTapeAt RF.cell Slot.val rest m) (PR.syElt PR.blank) } { state := Sum.inr (PR.stElt (NexPh.evalP (EvalPh.chk k)) f), head := Sum.inl v, tape := wideTape (PR.trackTapeAt RF.cell Slot.val rest m) (PR.syElt PR.blank) }

The evaluation's entry walk-back: whatever dispatches into the spine leaves the head one cell to the right of the marker, and a checkpoint's stay rule walks it back. This is the step between the opening and DescriptiveComplexity.Draw.Data.nexEval_reachesIn.

theorem DescriptiveComplexity.Draw.Data.step_nexEvalExit {L : FirstOrder.Language} {dt : Data L} {A R Q PM SM B : Type} {nv : ℕ} [Fintype Q] [Fintype dt.SlotIx] [LinearOrder A] [LinearOrder R] [LinearOrder (NexPh B (EvalPh nv PM))] [FirstOrder.Language.wide.Structure (Univ A R (NexPh B (EvalPh nv PM)) dt.KIx dt.dd)] [Finite A] [Finite R] [Finite (NexPh B (EvalPh nv PM))] {ShM : SM → Type} {PR : Prog A R (NexPh B (EvalPh nv PM)) Q dt.SlotIx dt.KIx dt.dd} {I : Type} {ile : I → I → Prop} (RF : IxFile (Univ A R (NexPh B (EvalPh nv PM)) dt.KIx dt.dd) I ile) {ruleM : (s : SM) → ShM s → Rule A Q dt.SlotIx (NexPh B (EvalPh nv PM))} {subEntry : Fin nv → PM} {exitPh : NexPh B (EvalPh nv PM)} {rEmb : (i : EvalSite nv SM) → NexEvalSh nv SM ShM i → R} (hrules : ∀ (i : EvalSite nv SM) (ρ : NexEvalSh nv SM ShM i), PR.rules (rEmb i ρ) = dt.nexEvalRule PR.one ruleM subEntry exitPh i ρ) (hR : PR.table.Reads) (hlin : IsLinOrd WMLe) {v v' : Univ A R (NexPh B (EvalPh nv PM)) dt.KIx dt.dd → Prop} (hvi : WMIncr WMLe v v') {rest : (Univ A R (NexPh B (EvalPh nv PM)) dt.KIx dt.dd → Prop) → dt.SlotIx → A} {m : I → Prop} {f : Q → A} (hex : dt.exitG PR.one (PR.passTracksAt RF.cell Slot.val rest m v)) : (wideData (Univ A R (NexPh B (EvalPh nv PM)) dt.KIx dt.dd)).Step { state := Sum.inr (PR.stElt (NexPh.evalP (EvalPh.chk (Fin.last nv))) f), head := Sum.inl v, tape := wideTape (PR.trackTapeAt RF.cell Slot.val rest m) (PR.syElt PR.blank) } { state := Sum.inr (PR.stElt exitPh f), head := Sum.inl v', tape := wideTape (PR.trackTapeAt RF.cell Slot.val rest m) (PR.syElt PR.blank) }

The evaluation's exit: at the last checkpoint the spine leaves into the phase the caller named, one cell to the right of the marker. This is the step between nexEval_reachesIn and the accepting phase.