One variable's machinery: the run #
The run theorem of DescriptiveComplexity.Draw.Data.varRule – the spine of
the per-variable evaluation. The two abstract machineries stay abstract: the
gates' run and the matrix's runs enter as hypotheses, one per VAL-loop
round, and this file contributes exactly the spine – the entry dispatch, the
VAL clear (DescriptiveComplexity.Draw.ClearKit), the rounds of matrix pass,
exhaustion test (DescriptiveComplexity.Draw.TestKit) and block-indexed
increment (DescriptiveComplexity.Draw.IncrKit) with the fold updates riding
in the dispatches, and the arrival at the exit checkpoint once VAL is
exhausted.
The background conditions every kit reads are bundled once
(DescriptiveComplexity.Draw.Data.VarBg); the VAL register's contents over
the rounds are an abstract family mV over an abstract enumeration, exactly
as in the element loop's run.
What indexes the file is a parameter (DescriptiveComplexity.Draw.LaidFile),
because everything the loop carries is a set of registers – the VAL register's
contents, a level's block value, the exhaustion pattern – and never an address of
the working area. So a clocked program, whose file has far fewer registers than
the universe has elements, runs this loop unchanged.
The run comes with its cost (var_reachesIn): the gates' width, the VAL
clear, one matrix pass, and then per round the test, the increment, the pass and
three dispatches – the loop's own count once per element of the enumeration.
var_run and var_run_fail are the same runs with the budget forgotten: the
widths are read off the caller's own runs
(DescriptiveComplexity.TMData.exists_reachesIn_of_reflTransGen) and the
sweeps' off wideRank_lt_card, so a space-bounded caller counts nothing.
def
DescriptiveComplexity.Draw.Data.VarBg
{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}
(RF : LaidFile dt A R P I)
(zero one : A)
(v : Univ A R P dt.KIx dt.dd → Prop)
(gtop : I)
(rest : (Univ A R P dt.KIx dt.dd → Prop) → dt.SlotIx → A)
(mval : I → Prop)
:
The background conditions of the VAL loop's kits, bundled: the
working-cell marker sits at v, the register file's marks are in place, and
the VAL slot backs the given track.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Dependency graph
def
DescriptiveComplexity.Draw.Data.InnerFull
{L : FirstOrder.Language}
(dt : Data L)
{I : Type}
(blkOf : I → Option dt.KIx)
(mv : I → Prop)
(u : I)
:
The exhaustion condition of a VAL-loop round: the register's bit at an element is set exactly when the element lies in an inner block – the “VAL = Kin-top” pattern the exhaustion test decides.
Instances For
Dependency graph
theorem
DescriptiveComplexity.Draw.Data.var_reachesIn_gates
{L : FirstOrder.Language}
(dt : Data L)
{A R P Q PG PX SG SX : Type}
[Fintype Q]
[Fintype dt.SlotIx]
[LinearOrder A]
[LinearOrder R]
[LinearOrder P]
[FirstOrder.Language.wide.Structure (Univ A R P dt.KIx dt.dd)]
[Finite A]
[Finite R]
[Finite P]
{ShG : SG → Type}
{ShX : SX → Type}
{PR : Prog A R P Q dt.SlotIx dt.KIx dt.dd}
{I : Type}
(RF : LaidFile dt A R P I)
{emb : VarPh dt.CarryB PG PX → P}
{ruleG : (s : SG) → ShG s → Rule A Q dt.SlotIx P}
{ruleX : (s : SX) → ShX s → Rule A Q dt.SlotIx P}
{pgEntry pxEntry exitPh : P}
{newSlot : dt.SlotIx}
{gateFlag : Q}
{accBit : (Q → A) → Prop}
{enterSt initSt postFold : (Q → A) → (dt.SlotIx → A) → Q → A}
{storeCarry : dt.CarryB → (Q → A) → (dt.SlotIx → A) → Q → A}
{rEmb : (i : VarSite SG SX) → VarSh SG SX ShG ShX dt.CarryB i → R}
(hrules :
∀ (i : VarSite SG SX) (ρ : VarSh SG SX ShG ShX dt.CarryB i),
PR.rules (rEmb i ρ) = dt.varRule PR.zero PR.one emb ruleG ruleX pgEntry pxEntry exitPh newSlot gateFlag accBit enterSt initSt postFold
storeCarry i ρ)
(hR : PR.table.Reads)
(hlin : IsLinOrd WMLe)
(hix : IsLinOrd RF.le)
{gtop gbot : I}
(hbot : ∀ (y : I), RF.le gbot y)
{v v' : Univ A R P dt.KIx dt.dd → Prop}
(hv : WMSetLt WMLe v (RF.cell gbot))
(hvi : WMIncr WMLe v v')
{rest : (Univ A R P dt.KIx dt.dd → Prop) → dt.SlotIx → A}
{mval : I → Prop}
(hbg : dt.VarBg RF PR.zero PR.one v gtop rest mval)
{f₀ fG : Q → A}
(wG : ℕ)
(hGates :
(wideData (Univ A R P dt.KIx dt.dd)).ReachesIn wG
{ state := Sum.inr (PR.stElt pgEntry (enterSt f₀ (rest v))), head := Sum.inl v',
tape := wideTape (PR.trackTapeAt RF.cell Slot.val rest mval) (PR.syElt PR.blank) }
{ state := Sum.inr (PR.stElt (emb VarPh.vchk1) fG), head := Sum.inl v,
tape := wideTape (PR.trackTapeAt RF.cell Slot.val rest mval) (PR.syElt PR.blank) })
:
(wideData (Univ A R P dt.KIx dt.dd)).ReachesIn (1 + wG)
{ state := Sum.inr (PR.stElt (emb VarPh.vchk0) f₀), head := Sum.inl v,
tape := wideTape (PR.trackTapeAt RF.cell Slot.val rest mval) (PR.syElt PR.blank) }
{ state := Sum.inr (PR.stElt (emb VarPh.vchk1) fG), head := Sum.inl v,
tape := wideTape (PR.trackTapeAt RF.cell Slot.val rest mval) (PR.syElt PR.blank) }
The machinery, entered: from the entry checkpoint at the marker, through the gates, to the verdict checkpoint.
Dependency graph
theorem
DescriptiveComplexity.Draw.Data.var_reachesIn
{L : FirstOrder.Language}
(dt : Data L)
{A R P Q PG PX SG SX : Type}
[Fintype Q]
[Fintype dt.SlotIx]
[LinearOrder A]
[LinearOrder R]
[LinearOrder P]
[FirstOrder.Language.wide.Structure (Univ A R P dt.KIx dt.dd)]
[Finite A]
[Finite R]
[Finite P]
{ShG : SG → Type}
{ShX : SX → Type}
{PR : Prog A R P Q dt.SlotIx dt.KIx dt.dd}
{I : Type}
[Finite I]
(RF : LaidFile dt A R P I)
{emb : VarPh dt.CarryB PG PX → P}
{ruleG : (s : SG) → ShG s → Rule A Q dt.SlotIx P}
{ruleX : (s : SX) → ShX s → Rule A Q dt.SlotIx P}
{pgEntry pxEntry exitPh : P}
{newSlot : dt.SlotIx}
{gateFlag : Q}
{accBit : (Q → A) → Prop}
{enterSt initSt postFold : (Q → A) → (dt.SlotIx → A) → Q → A}
{storeCarry : dt.CarryB → (Q → A) → (dt.SlotIx → A) → Q → A}
{rEmb : (i : VarSite SG SX) → VarSh SG SX ShG ShX dt.CarryB i → R}
(hrules :
∀ (i : VarSite SG SX) (ρ : VarSh SG SX ShG ShX dt.CarryB i),
PR.rules (rEmb i ρ) = dt.varRule PR.zero PR.one emb ruleG ruleX pgEntry pxEntry exitPh newSlot gateFlag accBit enterSt initSt postFold
storeCarry i ρ)
(hR : PR.table.Reads)
(hlin : IsLinOrd WMLe)
(hix : IsLinOrd RF.le)
{gtop gbot : I}
(htop : ∀ (y : I), RF.le y gtop)
(hbot : ∀ (y : I), RF.le gbot y)
{v v' : Univ A R P dt.KIx dt.dd → Prop}
(hv : WMSetLt WMLe v (RF.cell gbot))
(hvi : WMIncr WMLe v v')
{rest : (Univ A R P dt.KIx dt.dd → Prop) → dt.SlotIx → A}
{mval : I → Prop}
(hbg : dt.VarBg RF PR.zero PR.one v gtop rest mval)
{f₀ fG : Q → A}
(wG wM wS w : ℕ)
(hgap : ∀ (u u' : I), IxSucc RF.le u u' → wideRank (RF.cell u') - wideRank (RF.cell u) ≤ w)
(hGates :
(wideData (Univ A R P dt.KIx dt.dd)).ReachesIn wG
{ state := Sum.inr (PR.stElt pgEntry (enterSt f₀ (rest v))), head := Sum.inl v',
tape := wideTape (PR.trackTapeAt RF.cell Slot.val rest mval) (PR.syElt PR.blank) }
{ state := Sum.inr (PR.stElt (emb VarPh.vchk1) fG), head := Sum.inl v,
tape := wideTape (PR.trackTapeAt RF.cell Slot.val rest mval) (PR.syElt PR.blank) })
(hflag : fG gateFlag = PR.one)
{restC : (Univ A R P dt.KIx dt.dd → Prop) → dt.SlotIx → A}
(hbgC : dt.VarBg RF PR.zero PR.one v gtop restC fun (x : I) => False)
(hCoff :
∀ (r : Univ A R P dt.KIx dt.dd → Prop) (s : Slot dt.d.B.ι dt.ko dt.ki dt.dd0), s ≠ Slot.val → restC r s = rest r s)
{ι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)
{restM restO : ιV → (Univ A R P dt.KIx dt.dd → Prop) → dt.SlotIx → A}
(hbgO : ∀ (a : ιV), dt.VarBg RF PR.zero PR.one v gtop (restO a) (mV a))
(hM0 : restM a₀ = restC)
{fM fX : ιV → Q → A}
(hfM0 : fM a₀ = initSt fG (restC v))
(hMatrix :
∀ (a : ιV),
(wideData (Univ A R P dt.KIx dt.dd)).ReachesIn wM
{ state := Sum.inr (PR.stElt pxEntry (fM a)), head := Sum.inl v',
tape := wideTape (PR.trackTapeAt RF.cell Slot.val (restM a) (mV a)) (PR.syElt PR.blank) }
{ state := Sum.inr (PR.stElt (emb VarPh.mchk1) (fX a)), head := Sum.inl v,
tape := wideTape (PR.trackTapeAt RF.cell Slot.val (restO a) (mV a)) (PR.syElt PR.blank) })
(hIncr : ∀ (a a' : ιV), a < a' → (∀ (b : ιV), ¬(a < b ∧ b < a')) → WMIncr RF.le (mV a) (mV a'))
(hOMagree :
∀ (a a' : ιV),
a < a' →
(∀ (b : ιV), ¬(a < b ∧ b < a')) →
∀ (r : Univ A R P dt.KIx dt.dd → Prop) (s : Slot dt.d.B.ι dt.ko dt.ki dt.dd0),
s ≠ Slot.val → restM a' r s = restO a r s)
(hStore :
∀ (a a' : ιV),
a < a' →
(∀ (b : ιV), ¬(a < b ∧ b < a')) →
∀ (u₀ : I),
¬mV a u₀ →
(∀ (w : I), WMLt RF.le u₀ w → mV a w) →
storeCarry (RF.blk u₀) (postFold (fX a) (restO a v)) (restO a v) = fM a')
(hTestT : ∀ (u : I), dt.InnerFull RF.blk (mV aT) u)
(hTestF : ∀ a < aT, ∃ (u : I), ¬dt.InnerFull RF.blk (mV a) u)
(hS : wideRank (RF.cell gtop) + 2 + ((ixRank RF.le gtop - ixRank RF.le gbot) * w + 1) + wideRank (RF.cell gbot) ≤ wS)
:
(wideData (Univ A R P dt.KIx dt.dd)).ReachesIn (wG + wM + 3 * wS + 6 + (2 * wS + wM + 3) * Nat.card ιV)
{ state := Sum.inr (PR.stElt (emb VarPh.vchk0) f₀), head := Sum.inl v,
tape := wideTape (PR.trackTapeAt RF.cell Slot.val rest mval) (PR.syElt PR.blank) }
{ state := Sum.inr (PR.stElt (emb VarPh.vchk2) (postFold (fX aT) (restO aT v))), head := Sum.inl v,
tape := wideTape (PR.trackTapeAt RF.cell Slot.val (restO aT) (mV aT)) (PR.syElt PR.blank) }
One variable's machinery runs: from the entry checkpoint at the marker, through the gates, the VAL clear and the rounds of matrix pass, test and increment, to the exit checkpoint – VAL exhausted, the verdict spelled by the accumulators the dispatches folded.
Dependency graph
The two boundary steps a caller owes #
A spine dispatches into the machinery at the successor of the marker, and
receives the exit at the successor again: the walk back into the entry
checkpoint, and the written exit step out of vchk2.
theorem
DescriptiveComplexity.Draw.Data.step_var_back
{L : FirstOrder.Language}
(dt : Data L)
{A R P Q PG PX SG SX : Type}
[Fintype Q]
[Fintype dt.SlotIx]
[LinearOrder A]
[LinearOrder R]
[LinearOrder P]
[FirstOrder.Language.wide.Structure (Univ A R P dt.KIx dt.dd)]
[Finite A]
[Finite R]
[Finite P]
{ShG : SG → Type}
{ShX : SX → Type}
{PR : Prog A R P Q dt.SlotIx dt.KIx dt.dd}
{I : Type}
(RF : LaidFile dt A R P I)
{emb : VarPh dt.CarryB PG PX → P}
{ruleG : (s : SG) → ShG s → Rule A Q dt.SlotIx P}
{ruleX : (s : SX) → ShX s → Rule A Q dt.SlotIx P}
{pgEntry pxEntry exitPh : P}
{newSlot : dt.SlotIx}
{gateFlag : Q}
{accBit : (Q → A) → Prop}
{enterSt initSt postFold : (Q → A) → (dt.SlotIx → A) → Q → A}
{storeCarry : dt.CarryB → (Q → A) → (dt.SlotIx → A) → Q → A}
{rEmb : (i : VarSite SG SX) → VarSh SG SX ShG ShX dt.CarryB i → R}
(hrules :
∀ (i : VarSite SG SX) (ρ : VarSh SG SX ShG ShX dt.CarryB i),
PR.rules (rEmb i ρ) = dt.varRule PR.zero PR.one emb ruleG ruleX pgEntry pxEntry exitPh newSlot gateFlag accBit enterSt initSt postFold
storeCarry i ρ)
(hR : PR.table.Reads)
(hlin : IsLinOrd WMLe)
{v v' : Univ A R P dt.KIx dt.dd → Prop}
(hvi : WMIncr WMLe v v')
{rest : (Univ A R P dt.KIx dt.dd → Prop) → dt.SlotIx → A}
{mval : I → Prop}
{f : Q → A}
(hwk : rest v' Slot.wk = bitVal PR.zero PR.one (v' = v))
:
(wideData (Univ A R P dt.KIx dt.dd)).Step
{ state := Sum.inr (PR.stElt (emb VarPh.vchk0) f), head := Sum.inl v',
tape := wideTape (PR.trackTapeAt RF.cell Slot.val rest mval) (PR.syElt PR.blank) }
{ state := Sum.inr (PR.stElt (emb VarPh.vchk0) f), head := Sum.inl v,
tape := wideTape (PR.trackTapeAt RF.cell Slot.val rest mval) (PR.syElt PR.blank) }
The walk back into the entry checkpoint: arriving from a caller's dispatch one cell right of the marker, the checkpoint steps back to it.
Dependency graph
theorem
DescriptiveComplexity.Draw.Data.step_var_exit
{L : FirstOrder.Language}
(dt : Data L)
{A R P Q PG PX SG SX : Type}
[Fintype Q]
[Fintype dt.SlotIx]
[LinearOrder A]
[LinearOrder R]
[LinearOrder P]
[FirstOrder.Language.wide.Structure (Univ A R P dt.KIx dt.dd)]
[Finite A]
[Finite R]
[Finite P]
{ShG : SG → Type}
{ShX : SX → Type}
{PR : Prog A R P Q dt.SlotIx dt.KIx dt.dd}
{I : Type}
(RF : LaidFile dt A R P I)
{emb : VarPh dt.CarryB PG PX → P}
{ruleG : (s : SG) → ShG s → Rule A Q dt.SlotIx P}
{ruleX : (s : SX) → ShX s → Rule A Q dt.SlotIx P}
{pgEntry pxEntry exitPh : P}
{newSlot : dt.SlotIx}
{gateFlag : Q}
{accBit : (Q → A) → Prop}
{enterSt initSt postFold : (Q → A) → (dt.SlotIx → A) → Q → A}
{storeCarry : dt.CarryB → (Q → A) → (dt.SlotIx → A) → Q → A}
{rEmb : (i : VarSite SG SX) → VarSh SG SX ShG ShX dt.CarryB i → R}
(hrules :
∀ (i : VarSite SG SX) (ρ : VarSh SG SX ShG ShX dt.CarryB i),
PR.rules (rEmb i ρ) = dt.varRule PR.zero PR.one emb ruleG ruleX pgEntry pxEntry exitPh newSlot gateFlag accBit enterSt initSt postFold
storeCarry i ρ)
(hR : PR.table.Reads)
(hlin : IsLinOrd WMLe)
(hix : IsLinOrd RF.le)
{gtop gbot : I}
(hbot : ∀ (y : I), RF.le gbot y)
{v v' : Univ A R P dt.KIx dt.dd → Prop}
(hv : WMSetLt WMLe v (RF.cell gbot))
(hvi : WMIncr WMLe v v')
{rest rest' : (Univ A R P dt.KIx dt.dd → Prop) → dt.SlotIx → A}
{mval : I → Prop}
{f : Q → A}
(hbgV : dt.VarBg RF PR.zero PR.one v gtop rest mval)
(hns : newSlot ≠ Slot.val)
(hoff : ∀ (r : Univ A R P dt.KIx dt.dd → Prop), r ≠ v → rest' r = rest r)
(hupd : rest' v = Function.update (rest v) newSlot (bitVal PR.zero PR.one (accBit f)))
:
(wideData (Univ A R P dt.KIx dt.dd)).Step
{ state := Sum.inr (PR.stElt (emb VarPh.vchk2) f), head := Sum.inl v,
tape := wideTape (PR.trackTapeAt RF.cell Slot.val rest mval) (PR.syElt PR.blank) }
{ state := Sum.inr (PR.stElt exitPh f), head := Sum.inl v',
tape := wideTape (PR.trackTapeAt RF.cell Slot.val rest' mval) (PR.syElt PR.blank) }
The written exit step: at the marker, the exit checkpoint writes the variable's verdict into its stage slot and leaves right into the exit phase, the control untouched.
Dependency graph
theorem
DescriptiveComplexity.Draw.Data.step_var_failExit
{L : FirstOrder.Language}
(dt : Data L)
{A R P Q PG PX SG SX : Type}
[Fintype Q]
[Fintype dt.SlotIx]
[LinearOrder A]
[LinearOrder R]
[LinearOrder P]
[FirstOrder.Language.wide.Structure (Univ A R P dt.KIx dt.dd)]
[Finite A]
[Finite R]
[Finite P]
{ShG : SG → Type}
{ShX : SX → Type}
{PR : Prog A R P Q dt.SlotIx dt.KIx dt.dd}
{I : Type}
(RF : LaidFile dt A R P I)
{emb : VarPh dt.CarryB PG PX → P}
{ruleG : (s : SG) → ShG s → Rule A Q dt.SlotIx P}
{ruleX : (s : SX) → ShX s → Rule A Q dt.SlotIx P}
{pgEntry pxEntry exitPh : P}
{newSlot : dt.SlotIx}
{gateFlag : Q}
{accBit : (Q → A) → Prop}
{enterSt initSt postFold : (Q → A) → (dt.SlotIx → A) → Q → A}
{storeCarry : dt.CarryB → (Q → A) → (dt.SlotIx → A) → Q → A}
{rEmb : (i : VarSite SG SX) → VarSh SG SX ShG ShX dt.CarryB i → R}
(hrules :
∀ (i : VarSite SG SX) (ρ : VarSh SG SX ShG ShX dt.CarryB i),
PR.rules (rEmb i ρ) = dt.varRule PR.zero PR.one emb ruleG ruleX pgEntry pxEntry exitPh newSlot gateFlag accBit enterSt initSt postFold
storeCarry i ρ)
(hR : PR.table.Reads)
(hlin : IsLinOrd WMLe)
(hix : IsLinOrd RF.le)
{gtop gbot : I}
(hbot : ∀ (y : I), RF.le gbot y)
{v v' : Univ A R P dt.KIx dt.dd → Prop}
(hv : WMSetLt WMLe v (RF.cell gbot))
(hvi : WMIncr WMLe v v')
{rest rest' : (Univ A R P dt.KIx dt.dd → Prop) → dt.SlotIx → A}
{mval : I → Prop}
{f : Q → A}
(hbgV : dt.VarBg RF PR.zero PR.one v gtop rest mval)
(hflagF : f gateFlag ≠ PR.one)
(hns : newSlot ≠ Slot.val)
(hoff : ∀ (r : Univ A R P dt.KIx dt.dd → Prop), r ≠ v → rest' r = rest r)
(hupd : rest' v = Function.update (rest v) newSlot PR.zero)
:
(wideData (Univ A R P dt.KIx dt.dd)).Step
{ state := Sum.inr (PR.stElt (emb VarPh.vchk1) f), head := Sum.inl v,
tape := wideTape (PR.trackTapeAt RF.cell Slot.val rest mval) (PR.syElt PR.blank) }
{ state := Sum.inr (PR.stElt exitPh f), head := Sum.inl v',
tape := wideTape (PR.trackTapeAt RF.cell Slot.val rest' mval) (PR.syElt PR.blank) }
The failing exit step: at the marker with the gates' verdict flag clear, the verdict checkpoint erases the variable's stage slot and leaves right into the exit phase, skipping the whole VAL loop.
Dependency graph
theorem
DescriptiveComplexity.Draw.Data.var_reachesIn_fail
{L : FirstOrder.Language}
(dt : Data L)
{A R P Q PG PX SG SX : Type}
[Fintype Q]
[Fintype dt.SlotIx]
[LinearOrder A]
[LinearOrder R]
[LinearOrder P]
[FirstOrder.Language.wide.Structure (Univ A R P dt.KIx dt.dd)]
[Finite A]
[Finite R]
[Finite P]
{ShG : SG → Type}
{ShX : SX → Type}
{PR : Prog A R P Q dt.SlotIx dt.KIx dt.dd}
{I : Type}
(RF : LaidFile dt A R P I)
{emb : VarPh dt.CarryB PG PX → P}
{ruleG : (s : SG) → ShG s → Rule A Q dt.SlotIx P}
{ruleX : (s : SX) → ShX s → Rule A Q dt.SlotIx P}
{pgEntry pxEntry exitPh : P}
{newSlot : dt.SlotIx}
{gateFlag : Q}
{accBit : (Q → A) → Prop}
{enterSt initSt postFold : (Q → A) → (dt.SlotIx → A) → Q → A}
{storeCarry : dt.CarryB → (Q → A) → (dt.SlotIx → A) → Q → A}
{rEmb : (i : VarSite SG SX) → VarSh SG SX ShG ShX dt.CarryB i → R}
(hrules :
∀ (i : VarSite SG SX) (ρ : VarSh SG SX ShG ShX dt.CarryB i),
PR.rules (rEmb i ρ) = dt.varRule PR.zero PR.one emb ruleG ruleX pgEntry pxEntry exitPh newSlot gateFlag accBit enterSt initSt postFold
storeCarry i ρ)
(hR : PR.table.Reads)
(hlin : IsLinOrd WMLe)
(hix : IsLinOrd RF.le)
{gtop gbot : I}
(hbot : ∀ (y : I), RF.le gbot y)
{v v' : Univ A R P dt.KIx dt.dd → Prop}
(hv : WMSetLt WMLe v (RF.cell gbot))
(hvi : WMIncr WMLe v v')
{rest : (Univ A R P dt.KIx dt.dd → Prop) → dt.SlotIx → A}
{mval : I → Prop}
(hbg : dt.VarBg RF PR.zero PR.one v gtop rest mval)
{f₀ fG : Q → A}
(wG : ℕ)
(hGates :
(wideData (Univ A R P dt.KIx dt.dd)).ReachesIn wG
{ state := Sum.inr (PR.stElt pgEntry (enterSt f₀ (rest v))), head := Sum.inl v',
tape := wideTape (PR.trackTapeAt RF.cell Slot.val rest mval) (PR.syElt PR.blank) }
{ state := Sum.inr (PR.stElt (emb VarPh.vchk1) fG), head := Sum.inl v,
tape := wideTape (PR.trackTapeAt RF.cell Slot.val rest mval) (PR.syElt PR.blank) })
(hflagF : fG gateFlag ≠ PR.one)
(hns : newSlot ≠ Slot.val)
{rest' : (Univ A R P dt.KIx dt.dd → Prop) → dt.SlotIx → A}
(hoff : ∀ (r : Univ A R P dt.KIx dt.dd → Prop), r ≠ v → rest' r = rest r)
(hupd : rest' v = Function.update (rest v) newSlot PR.zero)
:
(wideData (Univ A R P dt.KIx dt.dd)).ReachesIn (1 + wG + 1)
{ state := Sum.inr (PR.stElt (emb VarPh.vchk0) f₀), head := Sum.inl v,
tape := wideTape (PR.trackTapeAt RF.cell Slot.val rest mval) (PR.syElt PR.blank) }
{ state := Sum.inr (PR.stElt exitPh fG), head := Sum.inl v',
tape := wideTape (PR.trackTapeAt RF.cell Slot.val rest' mval) (PR.syElt PR.blank) }
The machinery on a failing address: through the gates to the verdict checkpoint, whose clear flag routes straight to the exit – the stage slot erased, the VAL loop never entered.
Dependency graph
The runs with their budgets forgotten #
What a space-bounded caller reads. The widths are recovered from the runs it
supplies (DescriptiveComplexity.TMData.exists_reachesIn_of_reflTransGen), the
sweeps' from wideRank_lt_card, so nothing has to have been counted.
theorem
DescriptiveComplexity.Draw.Data.var_run_fail
{L : FirstOrder.Language}
(dt : Data L)
{A R P Q PG PX SG SX : Type}
[Fintype Q]
[Fintype dt.SlotIx]
[LinearOrder A]
[LinearOrder R]
[LinearOrder P]
[FirstOrder.Language.wide.Structure (Univ A R P dt.KIx dt.dd)]
[Finite A]
[Finite R]
[Finite P]
{ShG : SG → Type}
{ShX : SX → Type}
{PR : Prog A R P Q dt.SlotIx dt.KIx dt.dd}
{I : Type}
(RF : LaidFile dt A R P I)
{emb : VarPh dt.CarryB PG PX → P}
{ruleG : (s : SG) → ShG s → Rule A Q dt.SlotIx P}
{ruleX : (s : SX) → ShX s → Rule A Q dt.SlotIx P}
{pgEntry pxEntry exitPh : P}
{newSlot : dt.SlotIx}
{gateFlag : Q}
{accBit : (Q → A) → Prop}
{enterSt initSt postFold : (Q → A) → (dt.SlotIx → A) → Q → A}
{storeCarry : dt.CarryB → (Q → A) → (dt.SlotIx → A) → Q → A}
{rEmb : (i : VarSite SG SX) → VarSh SG SX ShG ShX dt.CarryB i → R}
(hrules :
∀ (i : VarSite SG SX) (ρ : VarSh SG SX ShG ShX dt.CarryB i),
PR.rules (rEmb i ρ) = dt.varRule PR.zero PR.one emb ruleG ruleX pgEntry pxEntry exitPh newSlot gateFlag accBit enterSt initSt postFold
storeCarry i ρ)
(hR : PR.table.Reads)
(hlin : IsLinOrd WMLe)
(hix : IsLinOrd RF.le)
{gtop gbot : I}
(hbot : ∀ (y : I), RF.le gbot y)
{v v' : Univ A R P dt.KIx dt.dd → Prop}
(hv : WMSetLt WMLe v (RF.cell gbot))
(hvi : WMIncr WMLe v v')
{rest : (Univ A R P dt.KIx dt.dd → Prop) → dt.SlotIx → A}
{mval : I → Prop}
(hbg : dt.VarBg RF PR.zero PR.one v gtop rest mval)
{f₀ fG : Q → A}
(hGatesR :
Relation.ReflTransGen (wideData (Univ A R P dt.KIx dt.dd)).Step
{ state := Sum.inr (PR.stElt pgEntry (enterSt f₀ (rest v))), head := Sum.inl v',
tape := wideTape (PR.trackTapeAt RF.cell Slot.val rest mval) (PR.syElt PR.blank) }
{ state := Sum.inr (PR.stElt (emb VarPh.vchk1) fG), head := Sum.inl v,
tape := wideTape (PR.trackTapeAt RF.cell Slot.val rest mval) (PR.syElt PR.blank) })
(hflagF : fG gateFlag ≠ PR.one)
(hns : newSlot ≠ Slot.val)
{rest' : (Univ A R P dt.KIx dt.dd → Prop) → dt.SlotIx → A}
(hoff : ∀ (r : Univ A R P dt.KIx dt.dd → Prop), r ≠ v → rest' r = rest r)
(hupd : rest' v = Function.update (rest v) newSlot PR.zero)
:
Relation.ReflTransGen (wideData (Univ A R P dt.KIx dt.dd)).Step
{ state := Sum.inr (PR.stElt (emb VarPh.vchk0) f₀), head := Sum.inl v,
tape := wideTape (PR.trackTapeAt RF.cell Slot.val rest mval) (PR.syElt PR.blank) }
{ state := Sum.inr (PR.stElt exitPh fG), head := Sum.inl v',
tape := wideTape (PR.trackTapeAt RF.cell Slot.val rest' mval) (PR.syElt PR.blank) }
The machinery on a failing address, the budget forgotten.
Dependency graph
theorem
DescriptiveComplexity.Draw.Data.var_run
{L : FirstOrder.Language}
(dt : Data L)
{A R P Q PG PX SG SX : Type}
[Fintype Q]
[Fintype dt.SlotIx]
[LinearOrder A]
[LinearOrder R]
[LinearOrder P]
[FirstOrder.Language.wide.Structure (Univ A R P dt.KIx dt.dd)]
[Finite A]
[Finite R]
[Finite P]
{ShG : SG → Type}
{ShX : SX → Type}
{PR : Prog A R P Q dt.SlotIx dt.KIx dt.dd}
{I : Type}
[Finite I]
(RF : LaidFile dt A R P I)
{emb : VarPh dt.CarryB PG PX → P}
{ruleG : (s : SG) → ShG s → Rule A Q dt.SlotIx P}
{ruleX : (s : SX) → ShX s → Rule A Q dt.SlotIx P}
{pgEntry pxEntry exitPh : P}
{newSlot : dt.SlotIx}
{gateFlag : Q}
{accBit : (Q → A) → Prop}
{enterSt initSt postFold : (Q → A) → (dt.SlotIx → A) → Q → A}
{storeCarry : dt.CarryB → (Q → A) → (dt.SlotIx → A) → Q → A}
{rEmb : (i : VarSite SG SX) → VarSh SG SX ShG ShX dt.CarryB i → R}
(hrules :
∀ (i : VarSite SG SX) (ρ : VarSh SG SX ShG ShX dt.CarryB i),
PR.rules (rEmb i ρ) = dt.varRule PR.zero PR.one emb ruleG ruleX pgEntry pxEntry exitPh newSlot gateFlag accBit enterSt initSt postFold
storeCarry i ρ)
(hR : PR.table.Reads)
(hlin : IsLinOrd WMLe)
(hix : IsLinOrd RF.le)
{gtop gbot : I}
(htop : ∀ (y : I), RF.le y gtop)
(hbot : ∀ (y : I), RF.le gbot y)
{v v' : Univ A R P dt.KIx dt.dd → Prop}
(hv : WMSetLt WMLe v (RF.cell gbot))
(hvi : WMIncr WMLe v v')
{rest : (Univ A R P dt.KIx dt.dd → Prop) → dt.SlotIx → A}
{mval : I → Prop}
(hbg : dt.VarBg RF PR.zero PR.one v gtop rest mval)
{f₀ fG : Q → A}
(hflag : fG gateFlag = PR.one)
{restC : (Univ A R P dt.KIx dt.dd → Prop) → dt.SlotIx → A}
(hbgC : dt.VarBg RF PR.zero PR.one v gtop restC fun (x : I) => False)
(hCoff :
∀ (r : Univ A R P dt.KIx dt.dd → Prop) (s : Slot dt.d.B.ι dt.ko dt.ki dt.dd0), s ≠ Slot.val → restC r s = rest r s)
{ι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)
{restM restO : ιV → (Univ A R P dt.KIx dt.dd → Prop) → dt.SlotIx → A}
(hbgO : ∀ (a : ιV), dt.VarBg RF PR.zero PR.one v gtop (restO a) (mV a))
(hM0 : restM a₀ = restC)
{fM fX : ιV → Q → A}
(hfM0 : fM a₀ = initSt fG (restC v))
(hIncr : ∀ (a a' : ιV), a < a' → (∀ (b : ιV), ¬(a < b ∧ b < a')) → WMIncr RF.le (mV a) (mV a'))
(hOMagree :
∀ (a a' : ιV),
a < a' →
(∀ (b : ιV), ¬(a < b ∧ b < a')) →
∀ (r : Univ A R P dt.KIx dt.dd → Prop) (s : Slot dt.d.B.ι dt.ko dt.ki dt.dd0),
s ≠ Slot.val → restM a' r s = restO a r s)
(hStore :
∀ (a a' : ιV),
a < a' →
(∀ (b : ιV), ¬(a < b ∧ b < a')) →
∀ (u₀ : I),
¬mV a u₀ →
(∀ (w : I), WMLt RF.le u₀ w → mV a w) →
storeCarry (RF.blk u₀) (postFold (fX a) (restO a v)) (restO a v) = fM a')
(hTestT : ∀ (u : I), dt.InnerFull RF.blk (mV aT) u)
(hTestF : ∀ a < aT, ∃ (u : I), ¬dt.InnerFull RF.blk (mV a) u)
(hGatesR :
Relation.ReflTransGen (wideData (Univ A R P dt.KIx dt.dd)).Step
{ state := Sum.inr (PR.stElt pgEntry (enterSt f₀ (rest v))), head := Sum.inl v',
tape := wideTape (PR.trackTapeAt RF.cell Slot.val rest mval) (PR.syElt PR.blank) }
{ state := Sum.inr (PR.stElt (emb VarPh.vchk1) fG), head := Sum.inl v,
tape := wideTape (PR.trackTapeAt RF.cell Slot.val rest mval) (PR.syElt PR.blank) })
(hMatrixR :
∀ (a : ιV),
Relation.ReflTransGen (wideData (Univ A R P dt.KIx dt.dd)).Step
{ state := Sum.inr (PR.stElt pxEntry (fM a)), head := Sum.inl v',
tape := wideTape (PR.trackTapeAt RF.cell Slot.val (restM a) (mV a)) (PR.syElt PR.blank) }
{ state := Sum.inr (PR.stElt (emb VarPh.mchk1) (fX a)), head := Sum.inl v,
tape := wideTape (PR.trackTapeAt RF.cell Slot.val (restO a) (mV a)) (PR.syElt PR.blank) })
:
Relation.ReflTransGen (wideData (Univ A R P dt.KIx dt.dd)).Step
{ state := Sum.inr (PR.stElt (emb VarPh.vchk0) f₀), head := Sum.inl v,
tape := wideTape (PR.trackTapeAt RF.cell Slot.val rest mval) (PR.syElt PR.blank) }
{ state := Sum.inr (PR.stElt (emb VarPh.vchk2) (postFold (fX aT) (restO aT v))), head := Sum.inl v,
tape := wideTape (PR.trackTapeAt RF.cell Slot.val (restO aT) (mV aT)) (PR.syElt PR.blank) }
One variable's machinery runs, the budget forgotten: what a space-bounded caller reads.