The clocked spine at an arbitrary file #
DescriptiveComplexity.Problems.Wide.DrawIxEval's legs folded by the clocked
program's spine (nexEvalRuleF, two rules per checkpoint instead of three, its
phases wrapped in NexPh). The legs are the same theorems the space-bounded
spine folds – they are generic in the wrapper – so what this file adds is one
run: the branched evaluation of the whole spine, on a clock.
theorem
DescriptiveComplexity.Draw.Data.nexIxSpineB_reachesIn
{L : FirstOrder.Language}
(dt : Data L)
{A R B : Type}
[Fintype dt.SlotIx]
[LinearOrder A]
[LinearOrder R]
[LinearOrder (NexPh B (EvalPh dt.nv dt.PMF))]
[FirstOrder.Language.wide.Structure (Univ A R (NexPh B (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)]
[Finite A]
[Finite R]
[Finite (NexPh B (EvalPh dt.nv dt.PMF))]
{PR : Prog A R (NexPh B (EvalPh dt.nv dt.PMF)) dt.CtlIx dt.SlotIx dt.KIx dt.dd}
{I : Type}
[Finite I]
(F : LaidFile dt A R (NexPh B (EvalPh dt.nv dt.PMF)) I)
{elt : I → Univ A R (NexPh B (EvalPh dt.nv dt.PMF)) 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))
(hsepP : F.toLayout.NameSep PR.zero ⋯)
(hix : IsLinOrd F.le)
{e₀ : Univ A R (NexPh B (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd}
(he₀ : ∀ (y : Univ A R (NexPh B (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd), WMLe e₀ y)
(hord : ∀ (x y : Univ A R (NexPh B (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd), WMLe x y ↔ tagTupleLe x y)
[Nonempty A]
[L.IsRelational]
[L.Structure A]
[Finite dt.KIx]
{v v' : Univ A R (NexPh B (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop}
{rEmb : (i : dt.SEF) → dt.NexSESh i → R}
(hrules :
∀ (i : dt.SEF) (ρ : dt.NexSESh i),
PR.rules (rEmb i ρ) = dt.nexEvalRuleF PR.zero PR.one (fun (w : dt.VarIx) => dt.varArgsOf PR.zero PR.one w) i ρ)
(hR : PR.table.Reads)
(hlin : IsLinOrd WMLe)
{gtop gbot : I}
(htop : ∀ (y : I), F.le y gtop)
(hbot : ∀ (y : I), F.le gbot y)
(hwork :
∀ {r : Univ A R (NexPh B (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop},
(∀ (x : Univ A R (NexPh B (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd), r x → ∃ (i : dt.KIx), x.1 = Tag.arg i) →
∀ (u : I), WMSetLt WMLe r (F.cell u))
(hv : WMSetLt WMLe v (F.cell gbot))
(hvi : WMIncr WMLe v v')
{Use : I → Prop}
(hmono : ∀ (u u' : I), WMLt F.le u u' ↔ WMLt WMLe (elt u) (elt u'))
(hup :
∀ (u : I) (x : Univ A R (NexPh B (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd),
Use u → WMLt WMLe (elt u) x → ∃ (u' : I), Use u' ∧ elt u' = x)
(hvh : IxHolds elt Use v)
(hxdUse : ∀ {iv : dt.d.B.ι} (ℓ : Fin (dt.d.B.arity iv)) (b : Lex (Fin dt.dd0 → A)), Use (dt.ixStageXD F hhasP ℓ b))
(w wG wP wR wK : ℕ)
(hgap : ∀ (u u' : I), IxSucc F.le u u' → wideRank (F.cell u') - wideRank (F.cell u) ≤ wG)
(hwP : wideRank (F.cell gtop) + 2 + ((ixRank F.le gtop - ixRank F.le gbot) * wG + 1) + wideRank (F.cell gbot) ≤ wP)
(hwR :
∀ (s : Univ A R (NexPh B (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop),
WMSetLt WMLe s (F.cell gbot) → wideRank s + 4 ≤ wR)
(hwK :
∀ (T : Univ A R (NexPh B (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop),
WMSetLt WMLe T (F.cell gbot) →
wideRank T * (1 + (wideRank (F.cell gtop) + 3 + (ixRank F.le gtop - ixRank F.le gbot) * wG + wideRank (F.cell gbot)) + (wideRank (F.cell gtop) + ((ixRank F.le gtop - ixRank F.le gbot) * wG + 1) + wideRank (F.cell gbot) + 4)) + 1 + (wideRank (F.cell gtop) + 3 + (ixRank F.le gtop - ixRank F.le gbot) * wG + wideRank (F.cell gbot)) ≤ wK)
(hcostR :
∀ (b : Fin dt.ko ⊕ Fin dt.ki) (c : Fin dt.dd0 → A),
2 * (wideRank (F.cell (F.toLayout.reg hhasP b c)) - wideRank v) + 2 ≤ w)
{ιV : Type}
[LinearOrder ιV]
[Finite ιV]
{a₀ aT : ιV}
(hbotV : ∀ (a : ιV), a₀ ≤ a)
(htopV : ∀ (a : ιV), a ≤ aT)
(mV : ιV → I → Prop)
(hmV0 : mV a₀ = fun (x : I) => False)
(hIncr : ∀ (a a' : ιV), a < a' → (∀ (b : ιV), ¬(a < b ∧ b < a')) → WMIncr F.le (mV a) (mV a'))
(hTestT : ∀ (u : I), dt.InnerFull F.blk (mV aT) u)
(hTestF : ∀ a < aT, ∃ (u : I), ¬dt.InnerFull F.blk (mV a) u)
(stOf : Fin (dt.nv + 1) → TapeSt dt A R (NexPh B (EvalPh dt.nv dt.PMF)) I)
(fsOf : Fin (dt.nv + 1) → dt.CtlIx → A)
(hwkOf :
∀ (k : Fin (dt.nv + 1)),
(stOf k).wk = fun (r : Univ A R (NexPh B (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) => r = v)
(hmirOf : ∀ (j : Fin dt.nv), (stOf j.castSucc).mir = ixMark elt v)
(hbotOf :
∀ (j : Fin dt.nv),
(stOf j.castSucc).bot = fun (r : Univ A R (NexPh B (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) =>
r = fun (x : Univ A R (NexPh B (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd) => False)
(semTJ :
(j : Fin dt.nv) →
dt.ixGatedAt F j (stOf j.castSucc) →
(p : dt.IxScratch A R (NexPh B (EvalPh dt.nv dt.PMF)) I) →
(a : ιV) →
(∀ (ℓ : Fin (dt.nIn (dt.varAt j))),
dt.ixIGPassP F PR.zero PR.one (dt.varAt j) (ixVarRdSt (stOf j.castSucc) p (mV a)) ℓ) →
(b : Fin (dt.natOf (dt.varAt j))) →
dt.IxKindSem PR.zero PR.one (dt.varAt j)
(dt.ixMatSt (dt.varAt j) (ixVarRdSt (stOf j.castSucc) p (mV a)) v ↑b) elt (dt.kindOf (dt.varAt j) b))
(hst :
∀ (j : Fin dt.nv), stOf j.succ = dt.ixLegStB F hinj hhasP heltP mV j (stOf j.castSucc) (semTJ j) (fsOf j.castSucc))
(hfs :
∀ (j : Fin dt.nv), fsOf j.succ = dt.ixLegCtlB F hinj hhasP heltP mV j (stOf j.castSucc) (semTJ j) (fsOf j.castSucc))
:
(wideData (Univ A R (NexPh B (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)).ReachesIn
((dt.ixLegCost A w wP wR wK (Nat.card ιV) + 2) * dt.nv)
{ state := Sum.inr (PR.stElt (NexPh.evalP (EvalPh.chk 0)) (fsOf 0)), head := Sum.inl v,
tape :=
wideTape (PR.trackTapeAt F.cell Slot.val (dt.ixBack F.toLayout PR.zero PR.one ⋯ (stOf 0)) (stOf 0).val)
(PR.syElt PR.blank) }
{ state := Sum.inr (PR.stElt (NexPh.evalP (EvalPh.chk (Fin.last dt.nv))) (fsOf (Fin.last dt.nv))), head := Sum.inl v,
tape :=
wideTape
(PR.trackTapeAt F.cell Slot.val (dt.ixBack F.toLayout PR.zero PR.one ⋯ (stOf (Fin.last dt.nv)))
(stOf (Fin.last dt.nv)).val)
(PR.syElt PR.blank) }
The clocked evaluation's spine at an arbitrary address: the threaded spine, with the gates no longer assumed to pass. Each position takes whichever of the three legs its own gates call for, and what the caller owes is only the marker, the mirror and the bottom mark – all of which the advance sets and every leg leaves alone. This is the form a sweep can use, since it visits junk addresses and gated ones alike.
Dependency graph
theorem
DescriptiveComplexity.Draw.Data.nexIxEvalB_reachesIn
{L : FirstOrder.Language}
(dt : Data L)
{A R B : Type}
[Fintype dt.SlotIx]
[LinearOrder A]
[LinearOrder R]
[LinearOrder (NexPh B (EvalPh dt.nv dt.PMF))]
[FirstOrder.Language.wide.Structure (Univ A R (NexPh B (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)]
[Finite A]
[Finite R]
[Finite (NexPh B (EvalPh dt.nv dt.PMF))]
{PR : Prog A R (NexPh B (EvalPh dt.nv dt.PMF)) dt.CtlIx dt.SlotIx dt.KIx dt.dd}
{I : Type}
[Finite I]
(F : LaidFile dt A R (NexPh B (EvalPh dt.nv dt.PMF)) I)
{elt : I → Univ A R (NexPh B (EvalPh dt.nv dt.PMF)) 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))
(hsepP : F.toLayout.NameSep PR.zero ⋯)
(hix : IsLinOrd F.le)
{e₀ : Univ A R (NexPh B (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd}
(he₀ : ∀ (y : Univ A R (NexPh B (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd), WMLe e₀ y)
(hord : ∀ (x y : Univ A R (NexPh B (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd), WMLe x y ↔ tagTupleLe x y)
[Nonempty A]
[L.IsRelational]
[L.Structure A]
[Finite dt.KIx]
{v v' : Univ A R (NexPh B (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop}
{rEmb : (i : dt.SEF) → dt.NexSESh i → R}
(hrules :
∀ (i : dt.SEF) (ρ : dt.NexSESh i),
PR.rules (rEmb i ρ) = dt.nexEvalRuleF PR.zero PR.one (fun (w : dt.VarIx) => dt.varArgsOf PR.zero PR.one w) i ρ)
(hR : PR.table.Reads)
(hlin : IsLinOrd WMLe)
{gtop gbot : I}
(htop : ∀ (y : I), F.le y gtop)
(hbot : ∀ (y : I), F.le gbot y)
(hwork :
∀ {r : Univ A R (NexPh B (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop},
(∀ (x : Univ A R (NexPh B (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd), r x → ∃ (i : dt.KIx), x.1 = Tag.arg i) →
∀ (u : I), WMSetLt WMLe r (F.cell u))
(hv : WMSetLt WMLe v (F.cell gbot))
(hvi : WMIncr WMLe v v')
{Use : I → Prop}
(hmono : ∀ (u u' : I), WMLt F.le u u' ↔ WMLt WMLe (elt u) (elt u'))
(hup :
∀ (u : I) (x : Univ A R (NexPh B (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd),
Use u → WMLt WMLe (elt u) x → ∃ (u' : I), Use u' ∧ elt u' = x)
(hvh : IxHolds elt Use v)
(hxdUse : ∀ {iv : dt.d.B.ι} (ℓ : Fin (dt.d.B.arity iv)) (b : Lex (Fin dt.dd0 → A)), Use (dt.ixStageXD F hhasP ℓ b))
(w wG wP wR wK : ℕ)
(hgap : ∀ (u u' : I), IxSucc F.le u u' → wideRank (F.cell u') - wideRank (F.cell u) ≤ wG)
(hwP : wideRank (F.cell gtop) + 2 + ((ixRank F.le gtop - ixRank F.le gbot) * wG + 1) + wideRank (F.cell gbot) ≤ wP)
(hwR :
∀ (s : Univ A R (NexPh B (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop),
WMSetLt WMLe s (F.cell gbot) → wideRank s + 4 ≤ wR)
(hwK :
∀ (T : Univ A R (NexPh B (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop),
WMSetLt WMLe T (F.cell gbot) →
wideRank T * (1 + (wideRank (F.cell gtop) + 3 + (ixRank F.le gtop - ixRank F.le gbot) * wG + wideRank (F.cell gbot)) + (wideRank (F.cell gtop) + ((ixRank F.le gtop - ixRank F.le gbot) * wG + 1) + wideRank (F.cell gbot) + 4)) + 1 + (wideRank (F.cell gtop) + 3 + (ixRank F.le gtop - ixRank F.le gbot) * wG + wideRank (F.cell gbot)) ≤ wK)
(hcostR :
∀ (b : Fin dt.ko ⊕ Fin dt.ki) (c : Fin dt.dd0 → A),
2 * (wideRank (F.cell (F.toLayout.reg hhasP b c)) - wideRank v) + 2 ≤ w)
{ιV : Type}
[LinearOrder ιV]
[Finite ιV]
{a₀ aT : ιV}
(hbotV : ∀ (a : ιV), a₀ ≤ a)
(htopV : ∀ (a : ιV), a ≤ aT)
(mV : ιV → I → Prop)
(hmV0 : mV a₀ = fun (x : I) => False)
(hIncr : ∀ (a a' : ιV), a < a' → (∀ (b : ιV), ¬(a < b ∧ b < a')) → WMIncr F.le (mV a) (mV a'))
(hTestT : ∀ (u : I), dt.InnerFull F.blk (mV aT) u)
(hTestF : ∀ a < aT, ∃ (u : I), ¬dt.InnerFull F.blk (mV a) u)
(stOf : Fin (dt.nv + 1) → TapeSt dt A R (NexPh B (EvalPh dt.nv dt.PMF)) I)
(fsOf : Fin (dt.nv + 1) → dt.CtlIx → A)
(hwkOf :
∀ (k : Fin (dt.nv + 1)),
(stOf k).wk = fun (r : Univ A R (NexPh B (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) => r = v)
(hmirOf : ∀ (j : Fin dt.nv), (stOf j.castSucc).mir = ixMark elt v)
(hbotOf :
∀ (j : Fin dt.nv),
(stOf j.castSucc).bot = fun (r : Univ A R (NexPh B (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) =>
r = fun (x : Univ A R (NexPh B (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd) => False)
(semTJ :
(j : Fin dt.nv) →
dt.ixGatedAt F j (stOf j.castSucc) →
(p : dt.IxScratch A R (NexPh B (EvalPh dt.nv dt.PMF)) I) →
(a : ιV) →
(∀ (ℓ : Fin (dt.nIn (dt.varAt j))),
dt.ixIGPassP F PR.zero PR.one (dt.varAt j) (ixVarRdSt (stOf j.castSucc) p (mV a)) ℓ) →
(b : Fin (dt.natOf (dt.varAt j))) →
dt.IxKindSem PR.zero PR.one (dt.varAt j)
(dt.ixMatSt (dt.varAt j) (ixVarRdSt (stOf j.castSucc) p (mV a)) v ↑b) elt (dt.kindOf (dt.varAt j) b))
(hst :
∀ (j : Fin dt.nv), stOf j.succ = dt.ixLegStB F hinj hhasP heltP mV j (stOf j.castSucc) (semTJ j) (fsOf j.castSucc))
(hfs :
∀ (j : Fin dt.nv), fsOf j.succ = dt.ixLegCtlB F hinj hhasP heltP mV j (stOf j.castSucc) (semTJ j) (fsOf j.castSucc))
:
(wideData (Univ A R (NexPh B (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)).ReachesIn
(1 + (dt.ixLegCost A w wP wR wK (Nat.card ιV) + 2) * dt.nv + 1)
{ state := Sum.inr (PR.stElt (NexPh.evalP (EvalPh.chk 0)) (fsOf 0)), head := Sum.inl v',
tape :=
wideTape (PR.trackTapeAt F.cell Slot.val (dt.ixBack F.toLayout PR.zero PR.one ⋯ (stOf 0)) (stOf 0).val)
(PR.syElt PR.blank) }
{ state := Sum.inr (PR.stElt (NexPh.evalP (EvalPh.sub dt.smEntryOut)) (fsOf (Fin.last dt.nv))), head := Sum.inl v',
tape :=
wideTape
(PR.trackTapeAt F.cell Slot.val (dt.ixBack F.toLayout PR.zero PR.one ⋯ (stOf (Fin.last dt.nv)))
(stOf (Fin.last dt.nv)).val)
(PR.syElt PR.blank) }
The clocked evaluation, entered and left: the walk-back the opening's
dispatch owes, the branched spine over the positions, and the dispatch into the
output's machinery, whose own exit is the accepting phase (the verdict bit
the accepting predicate reads is that machinery's, so the run has to reach
it). This is the middle leg of
DescriptiveComplexity.Draw.Data.nexProg_wideAccept_of_legs, at an arbitrary
file and on a clock.
Dependency graph
theorem
DescriptiveComplexity.Draw.Data.nexIxEvalOutB_reachesIn
{L : FirstOrder.Language}
(dt : Data L)
{A R B : Type}
[Fintype dt.SlotIx]
[LinearOrder A]
[LinearOrder R]
[LinearOrder (NexPh B (EvalPh dt.nv dt.PMF))]
[FirstOrder.Language.wide.Structure (Univ A R (NexPh B (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)]
[Finite A]
[Finite R]
[Finite (NexPh B (EvalPh dt.nv dt.PMF))]
{PR : Prog A R (NexPh B (EvalPh dt.nv dt.PMF)) dt.CtlIx dt.SlotIx dt.KIx dt.dd}
{I : Type}
[Finite I]
(F : LaidFile dt A R (NexPh B (EvalPh dt.nv dt.PMF)) I)
{elt : I → Univ A R (NexPh B (EvalPh dt.nv dt.PMF)) 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))
(hsepP : F.toLayout.NameSep PR.zero ⋯)
(hix : IsLinOrd F.le)
{e₀ : Univ A R (NexPh B (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd}
(he₀ : ∀ (y : Univ A R (NexPh B (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd), WMLe e₀ y)
(hord : ∀ (x y : Univ A R (NexPh B (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd), WMLe x y ↔ tagTupleLe x y)
[Nonempty A]
[L.IsRelational]
[L.Structure A]
[Finite dt.KIx]
{v v' : Univ A R (NexPh B (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop}
{rEmb : (i : dt.SEF) → dt.NexSESh i → R}
(hrules :
∀ (i : dt.SEF) (ρ : dt.NexSESh i),
PR.rules (rEmb i ρ) = dt.nexEvalRuleF PR.zero PR.one (fun (w : dt.VarIx) => dt.varArgsOf PR.zero PR.one w) i ρ)
(hR : PR.table.Reads)
(hlin : IsLinOrd WMLe)
{gtop gbot : I}
(htop : ∀ (y : I), F.le y gtop)
(hbot : ∀ (y : I), F.le gbot y)
(hwork :
∀ {r : Univ A R (NexPh B (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop},
(∀ (x : Univ A R (NexPh B (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd), r x → ∃ (i : dt.KIx), x.1 = Tag.arg i) →
∀ (u : I), WMSetLt WMLe r (F.cell u))
(hv : WMSetLt WMLe v (F.cell gbot))
(hvi : WMIncr WMLe v v')
{Use : I → Prop}
(hmono : ∀ (u u' : I), WMLt F.le u u' ↔ WMLt WMLe (elt u) (elt u'))
(hup :
∀ (u : I) (x : Univ A R (NexPh B (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd),
Use u → WMLt WMLe (elt u) x → ∃ (u' : I), Use u' ∧ elt u' = x)
(hvh : IxHolds elt Use v)
(hxdUse : ∀ {iv : dt.d.B.ι} (ℓ : Fin (dt.d.B.arity iv)) (b : Lex (Fin dt.dd0 → A)), Use (dt.ixStageXD F hhasP ℓ b))
(w wG wP wR wK : ℕ)
(hgap : ∀ (u u' : I), IxSucc F.le u u' → wideRank (F.cell u') - wideRank (F.cell u) ≤ wG)
(hwP : wideRank (F.cell gtop) + 2 + ((ixRank F.le gtop - ixRank F.le gbot) * wG + 1) + wideRank (F.cell gbot) ≤ wP)
(hwR :
∀ (s : Univ A R (NexPh B (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop),
WMSetLt WMLe s (F.cell gbot) → wideRank s + 4 ≤ wR)
(hwK :
∀ (T : Univ A R (NexPh B (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop),
WMSetLt WMLe T (F.cell gbot) →
wideRank T * (1 + (wideRank (F.cell gtop) + 3 + (ixRank F.le gtop - ixRank F.le gbot) * wG + wideRank (F.cell gbot)) + (wideRank (F.cell gtop) + ((ixRank F.le gtop - ixRank F.le gbot) * wG + 1) + wideRank (F.cell gbot) + 4)) + 1 + (wideRank (F.cell gtop) + 3 + (ixRank F.le gtop - ixRank F.le gbot) * wG + wideRank (F.cell gbot)) ≤ wK)
(hcostR :
∀ (b : Fin dt.ko ⊕ Fin dt.ki) (c : Fin dt.dd0 → A),
2 * (wideRank (F.cell (F.toLayout.reg hhasP b c)) - wideRank v) + 2 ≤ w)
{ιV : Type}
[LinearOrder ιV]
[Finite ιV]
{a₀ aT : ιV}
(hbotV : ∀ (a : ιV), a₀ ≤ a)
(htopV : ∀ (a : ιV), a ≤ aT)
(mV : ιV → I → Prop)
(hmV0 : mV a₀ = fun (x : I) => False)
(hIncr : ∀ (a a' : ιV), a < a' → (∀ (b : ιV), ¬(a < b ∧ b < a')) → WMIncr F.le (mV a) (mV a'))
(hTestT : ∀ (u : I), dt.InnerFull F.blk (mV aT) u)
(hTestF : ∀ a < aT, ∃ (u : I), ¬dt.InnerFull F.blk (mV a) u)
(stOf : Fin (dt.nv + 1) → TapeSt dt A R (NexPh B (EvalPh dt.nv dt.PMF)) I)
(fsOf : Fin (dt.nv + 1) → dt.CtlIx → A)
(hwkOf :
∀ (k : Fin (dt.nv + 1)),
(stOf k).wk = fun (r : Univ A R (NexPh B (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) => r = v)
(hmirOf : ∀ (j : Fin dt.nv), (stOf j.castSucc).mir = ixMark elt v)
(hbotOf :
∀ (j : Fin dt.nv),
(stOf j.castSucc).bot = fun (r : Univ A R (NexPh B (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) =>
r = fun (x : Univ A R (NexPh B (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd) => False)
(semTJ :
(j : Fin dt.nv) →
dt.ixGatedAt F j (stOf j.castSucc) →
(p : dt.IxScratch A R (NexPh B (EvalPh dt.nv dt.PMF)) I) →
(a : ιV) →
(∀ (ℓ : Fin (dt.nIn (dt.varAt j))),
dt.ixIGPassP F PR.zero PR.one (dt.varAt j) (ixVarRdSt (stOf j.castSucc) p (mV a)) ℓ) →
(b : Fin (dt.natOf (dt.varAt j))) →
dt.IxKindSem PR.zero PR.one (dt.varAt j)
(dt.ixMatSt (dt.varAt j) (ixVarRdSt (stOf j.castSucc) p (mV a)) v ↑b) elt (dt.kindOf (dt.varAt j) b))
(hst :
∀ (j : Fin dt.nv), stOf j.succ = dt.ixLegStB F hinj hhasP heltP mV j (stOf j.castSucc) (semTJ j) (fsOf j.castSucc))
(hfs :
∀ (j : Fin dt.nv), fsOf j.succ = dt.ixLegCtlB F hinj hhasP heltP mV j (stOf j.castSucc) (semTJ j) (fsOf j.castSucc))
{rEmbO : (i : dt.VarSiteF none) → dt.VarShF none i → R}
(hrulesOut :
∀ (i : dt.VarSiteF none) (ρ : dt.VarShF none i),
PR.rules (rEmbO i ρ) = dt.varRuleF PR.zero PR.one none (dt.varArgsOf PR.zero PR.one none)
(fun (p : dt.VarPhF none) => NexPh.evalP (EvalPh.sub (Sum.inr p))) NexPh.acceptP i ρ)
(TestOf : Fin (dt.arOf none) → I → Prop)
(hcompatOf :
∀ (ℓ : Fin (dt.arOf none)) (u : I),
dt.wellShapedG PR.zero PR.one (Sum.inl (Fin.castLE ⋯ ℓ))
(PR.passTracksAt F.cell Slot.mir (dt.ixBack F.toLayout PR.zero PR.one ⋯ (stOf (Fin.last dt.nv)))
(stOf (Fin.last dt.nv)).mir (F.cell u)) ↔ TestOf ℓ u)
(tOf : Fin (dt.arOf none) → dt.X.Tag)
(hwitOf :
∀ (ℓ : Fin (dt.arOf none)) (t' : dt.X.Tag),
wmBlk (ixAddr elt (stOf (Fin.last dt.nv)).mir) (Tag.arg (toLex (Sum.inl (Fin.castLE ⋯ ℓ))))
(encTagTup dt.ly PR.zero PR.one t') ↔ t' = tOf ℓ)
(hmirL : (stOf (Fin.last dt.nv)).mir = ixMark elt v)
(hbotL :
(stOf (Fin.last dt.nv)).bot = fun (r : Univ A R (NexPh B (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) =>
r = fun (x : Univ A R (NexPh B (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd) => False)
(hsavL : (stOf (Fin.last dt.nv)).sav = ixMark elt v)
(htgtL : (stOf (Fin.last dt.nv)).tgt = ixMark elt v)
(semOf :
(a : ιV) →
(∀ (ℓ : Fin (dt.nIn none)), dt.ixIGPassP F PR.zero PR.one none (dt.ixRoundSt (stOf (Fin.last dt.nv)) (mV a)) ℓ) →
(b : Fin (dt.natOf none)) →
dt.IxKindSem PR.zero PR.one none (dt.ixRoundSt (stOf (Fin.last dt.nv)) (mV a)) elt (dt.kindOf none b))
(hDom :
∀ (ℓ : Fin (dt.arOf none)),
ExpExpansion.DomHolds
(tOf ℓ, decRho dt.ly PR.zero PR.one
(wmBlk (ixAddr elt (stOf (Fin.last dt.nv)).mir) (Tag.arg (toLex (Sum.inl (Fin.castLE ⋯ ℓ)))))))
(hTestOf : ∀ (ℓ : Fin (dt.arOf none)) (u : I), TestOf ℓ u)
(hacc :
(dt.varArgsOf PR.zero PR.one none).accBit
(dt.ixOutCtl F hinj hhasP heltP mV (stOf (Fin.last dt.nv)) tOf semOf (fsOf (Fin.last dt.nv))))
:
(wideData (Univ A R (NexPh B (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)).ReachesIn
(1 + (dt.ixLegCost A w wP wR wK (Nat.card ιV) + 2) * dt.nv + 1 + dt.ixOutLegCost A w wP wR wK (Nat.card ιV))
{ state := Sum.inr (PR.stElt (NexPh.evalP (EvalPh.chk 0)) (fsOf 0)), head := Sum.inl v',
tape :=
wideTape (PR.trackTapeAt F.cell Slot.val (dt.ixBack F.toLayout PR.zero PR.one ⋯ (stOf 0)) (stOf 0).val)
(PR.syElt PR.blank) }
{ state :=
Sum.inr
(PR.stElt NexPh.acceptP
(dt.ixOutCtl F hinj hhasP heltP mV (stOf (Fin.last dt.nv)) tOf semOf (fsOf (Fin.last dt.nv)))),
head := Sum.inl v',
tape :=
wideTape
(PR.trackTapeAt F.cell Slot.val
(dt.ixBack F.toLayout PR.zero PR.one ⋯ (dt.ixRoundSt (stOf (Fin.last dt.nv)) (mV aT))) (mV aT))
(PR.syElt PR.blank) }
The clocked evaluation, all the way to the accepting phase: the run above, and then the output's machinery – the one whose verdict bit the accepting predicate reads. What it asks for is what the output leg asks: the shape of the argument blocks at the state the spine leaves, the tags they name, the packs, and the verdict itself.
Dependency graph
theorem
DescriptiveComplexity.Draw.Data.nexIxEvalOutB_any_reachesIn
{L : FirstOrder.Language}
(dt : Data L)
{A R B : Type}
[Fintype dt.SlotIx]
[LinearOrder A]
[LinearOrder R]
[LinearOrder (NexPh B (EvalPh dt.nv dt.PMF))]
[FirstOrder.Language.wide.Structure (Univ A R (NexPh B (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)]
[Finite A]
[Finite R]
[Finite (NexPh B (EvalPh dt.nv dt.PMF))]
{PR : Prog A R (NexPh B (EvalPh dt.nv dt.PMF)) dt.CtlIx dt.SlotIx dt.KIx dt.dd}
{I : Type}
[Finite I]
(F : LaidFile dt A R (NexPh B (EvalPh dt.nv dt.PMF)) I)
{elt : I → Univ A R (NexPh B (EvalPh dt.nv dt.PMF)) 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))
(hsepP : F.toLayout.NameSep PR.zero ⋯)
(hix : IsLinOrd F.le)
{e₀ : Univ A R (NexPh B (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd}
(he₀ : ∀ (y : Univ A R (NexPh B (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd), WMLe e₀ y)
(hord : ∀ (x y : Univ A R (NexPh B (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd), WMLe x y ↔ tagTupleLe x y)
[Nonempty A]
[L.IsRelational]
[L.Structure A]
[Finite dt.KIx]
{v v' : Univ A R (NexPh B (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop}
{rEmb : (i : dt.SEF) → dt.NexSESh i → R}
(hrules :
∀ (i : dt.SEF) (ρ : dt.NexSESh i),
PR.rules (rEmb i ρ) = dt.nexEvalRuleF PR.zero PR.one (fun (w : dt.VarIx) => dt.varArgsOf PR.zero PR.one w) i ρ)
(hR : PR.table.Reads)
(hlin : IsLinOrd WMLe)
{gtop gbot : I}
(htop : ∀ (y : I), F.le y gtop)
(hbot : ∀ (y : I), F.le gbot y)
(hwork :
∀ {r : Univ A R (NexPh B (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop},
(∀ (x : Univ A R (NexPh B (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd), r x → ∃ (i : dt.KIx), x.1 = Tag.arg i) →
∀ (u : I), WMSetLt WMLe r (F.cell u))
(hv : WMSetLt WMLe v (F.cell gbot))
(hvi : WMIncr WMLe v v')
{Use : I → Prop}
(hmono : ∀ (u u' : I), WMLt F.le u u' ↔ WMLt WMLe (elt u) (elt u'))
(hup :
∀ (u : I) (x : Univ A R (NexPh B (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd),
Use u → WMLt WMLe (elt u) x → ∃ (u' : I), Use u' ∧ elt u' = x)
(hvh : IxHolds elt Use v)
(hxdUse : ∀ {iv : dt.d.B.ι} (ℓ : Fin (dt.d.B.arity iv)) (b : Lex (Fin dt.dd0 → A)), Use (dt.ixStageXD F hhasP ℓ b))
(w wG wP wR wK : ℕ)
(hgap : ∀ (u u' : I), IxSucc F.le u u' → wideRank (F.cell u') - wideRank (F.cell u) ≤ wG)
(hwP : wideRank (F.cell gtop) + 2 + ((ixRank F.le gtop - ixRank F.le gbot) * wG + 1) + wideRank (F.cell gbot) ≤ wP)
(hwR :
∀ (s : Univ A R (NexPh B (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop),
WMSetLt WMLe s (F.cell gbot) → wideRank s + 4 ≤ wR)
(hwK :
∀ (T : Univ A R (NexPh B (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop),
WMSetLt WMLe T (F.cell gbot) →
wideRank T * (1 + (wideRank (F.cell gtop) + 3 + (ixRank F.le gtop - ixRank F.le gbot) * wG + wideRank (F.cell gbot)) + (wideRank (F.cell gtop) + ((ixRank F.le gtop - ixRank F.le gbot) * wG + 1) + wideRank (F.cell gbot) + 4)) + 1 + (wideRank (F.cell gtop) + 3 + (ixRank F.le gtop - ixRank F.le gbot) * wG + wideRank (F.cell gbot)) ≤ wK)
(hcostR :
∀ (b : Fin dt.ko ⊕ Fin dt.ki) (c : Fin dt.dd0 → A),
2 * (wideRank (F.cell (F.toLayout.reg hhasP b c)) - wideRank v) + 2 ≤ w)
{ιV : Type}
[LinearOrder ιV]
[Finite ιV]
{a₀ aT : ιV}
(hbotV : ∀ (a : ιV), a₀ ≤ a)
(htopV : ∀ (a : ιV), a ≤ aT)
(mV : ιV → I → Prop)
(hmV0 : mV a₀ = fun (x : I) => False)
(hIncr : ∀ (a a' : ιV), a < a' → (∀ (b : ιV), ¬(a < b ∧ b < a')) → WMIncr F.le (mV a) (mV a'))
(hTestT : ∀ (u : I), dt.InnerFull F.blk (mV aT) u)
(hTestF : ∀ a < aT, ∃ (u : I), ¬dt.InnerFull F.blk (mV a) u)
(stOf : Fin (dt.nv + 1) → TapeSt dt A R (NexPh B (EvalPh dt.nv dt.PMF)) I)
(fsOf : Fin (dt.nv + 1) → dt.CtlIx → A)
(hwkOf :
∀ (k : Fin (dt.nv + 1)),
(stOf k).wk = fun (r : Univ A R (NexPh B (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) => r = v)
(hmirOf : ∀ (j : Fin dt.nv), (stOf j.castSucc).mir = ixMark elt v)
(hbotOf :
∀ (j : Fin dt.nv),
(stOf j.castSucc).bot = fun (r : Univ A R (NexPh B (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) =>
r = fun (x : Univ A R (NexPh B (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd) => False)
(semTJ :
(j : Fin dt.nv) →
dt.ixGatedAt F j (stOf j.castSucc) →
(p : dt.IxScratch A R (NexPh B (EvalPh dt.nv dt.PMF)) I) →
(a : ιV) →
(∀ (ℓ : Fin (dt.nIn (dt.varAt j))),
dt.ixIGPassP F PR.zero PR.one (dt.varAt j) (ixVarRdSt (stOf j.castSucc) p (mV a)) ℓ) →
(b : Fin (dt.natOf (dt.varAt j))) →
dt.IxKindSem PR.zero PR.one (dt.varAt j)
(dt.ixMatSt (dt.varAt j) (ixVarRdSt (stOf j.castSucc) p (mV a)) v ↑b) elt (dt.kindOf (dt.varAt j) b))
(hst :
∀ (j : Fin dt.nv), stOf j.succ = dt.ixLegStB F hinj hhasP heltP mV j (stOf j.castSucc) (semTJ j) (fsOf j.castSucc))
(hfs :
∀ (j : Fin dt.nv), fsOf j.succ = dt.ixLegCtlB F hinj hhasP heltP mV j (stOf j.castSucc) (semTJ j) (fsOf j.castSucc))
{rEmbO : (i : dt.VarSiteF none) → dt.VarShF none i → R}
(hrulesOut :
∀ (i : dt.VarSiteF none) (ρ : dt.VarShF none i),
PR.rules (rEmbO i ρ) = dt.varRuleF PR.zero PR.one none (dt.varArgsOf PR.zero PR.one none)
(fun (p : dt.VarPhF none) => NexPh.evalP (EvalPh.sub (Sum.inr p))) NexPh.acceptP i ρ)
(TestOf : Fin (dt.arOf none) → I → Prop)
(hcompatOf :
∀ (ℓ : Fin (dt.arOf none)) (u : I),
dt.wellShapedG PR.zero PR.one (Sum.inl (Fin.castLE ⋯ ℓ))
(PR.passTracksAt F.cell Slot.mir (dt.ixBack F.toLayout PR.zero PR.one ⋯ (stOf (Fin.last dt.nv)))
(stOf (Fin.last dt.nv)).mir (F.cell u)) ↔ TestOf ℓ u)
(tOf : Fin (dt.arOf none) → dt.X.Tag)
(hwitOf :
∀ (ℓ : Fin (dt.arOf none)) (t' : dt.X.Tag),
wmBlk (ixAddr elt (stOf (Fin.last dt.nv)).mir) (Tag.arg (toLex (Sum.inl (Fin.castLE ⋯ ℓ))))
(encTagTup dt.ly PR.zero PR.one t') ↔ t' = tOf ℓ)
(hmirL : (stOf (Fin.last dt.nv)).mir = ixMark elt v)
(hbotL :
(stOf (Fin.last dt.nv)).bot = fun (r : Univ A R (NexPh B (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) =>
r = fun (x : Univ A R (NexPh B (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd) => False)
(hsavL : (stOf (Fin.last dt.nv)).sav = ixMark elt v)
(htgtL : (stOf (Fin.last dt.nv)).tgt = ixMark elt v)
(semOf :
(a : ιV) →
(∀ (ℓ : Fin (dt.nIn none)), dt.ixIGPassP F PR.zero PR.one none (dt.ixRoundSt (stOf (Fin.last dt.nv)) (mV a)) ℓ) →
(b : Fin (dt.natOf none)) →
dt.IxKindSem PR.zero PR.one none (dt.ixRoundSt (stOf (Fin.last dt.nv)) (mV a)) elt (dt.kindOf none b))
(hDom :
∀ (ℓ : Fin (dt.arOf none)),
ExpExpansion.DomHolds
(tOf ℓ, decRho dt.ly PR.zero PR.one
(wmBlk (ixAddr elt (stOf (Fin.last dt.nv)).mir) (Tag.arg (toLex (Sum.inl (Fin.castLE ⋯ ℓ)))))))
(hTestOf : ∀ (ℓ : Fin (dt.arOf none)) (u : I), TestOf ℓ u)
:
(wideData (Univ A R (NexPh B (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)).ReachesIn
(1 + (dt.ixLegCost A w wP wR wK (Nat.card ιV) + 2) * dt.nv + 1 + dt.ixOutLegCost A w wP wR wK (Nat.card ιV))
{ state := Sum.inr (PR.stElt (NexPh.evalP (EvalPh.chk 0)) (fsOf 0)), head := Sum.inl v',
tape :=
wideTape (PR.trackTapeAt F.cell Slot.val (dt.ixBack F.toLayout PR.zero PR.one ⋯ (stOf 0)) (stOf 0).val)
(PR.syElt PR.blank) }
{ state :=
Sum.inr
(PR.stElt NexPh.acceptP
(dt.ixOutCtl F hinj hhasP heltP mV (stOf (Fin.last dt.nv)) tOf semOf (fsOf (Fin.last dt.nv)))),
head := Sum.inl v',
tape :=
wideTape
(PR.trackTapeAt F.cell Slot.val
(fun (r : Univ A R (NexPh B (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) =>
if r = v then
Function.update (dt.ixBack F.toLayout PR.zero PR.one ⋯ (dt.ixRoundSt (stOf (Fin.last dt.nv)) (mV aT)) v)
(dt.varArgsOf PR.zero PR.one none).newSlot
(bitVal PR.zero PR.one
((dt.varArgsOf PR.zero PR.one none).accBit
(dt.ixOutCtl F hinj hhasP heltP mV (stOf (Fin.last dt.nv)) tOf semOf (fsOf (Fin.last dt.nv)))))
else dt.ixBack F.toLayout PR.zero PR.one ⋯ (dt.ixRoundSt (stOf (Fin.last dt.nv)) (mV aT)) r)
(mV aT))
(PR.syElt PR.blank) }
The clocked evaluation, entered and left, whatever the verdict:
nexIxEvalOutB_reachesIn with the verdict not assumed – the run is the same and
what changes is the bit the exit writes at the marker (ixOutLeg_run_any). This
is the shape a backward reading uses.