The matrix's stages at an arbitrary file #
DescriptiveComplexity.Problems.Wide.DrawInstMat read at a coarse file: the
four atom runs – comparison, expansion, stage and gate block – wrapped into the
one shape the sequencer drives them through, entry one cell to the marker's
right at the Slot.val-walked presentation and exit at the next checkpoint.
Each wrapper is the clocked run of its atom with the walk-back the dispatch
owes, so each carries its atom's budget plus one step.
theorem
DescriptiveComplexity.Draw.Data.trackTape_val_eq_ixMir
{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)]
{PR : Prog A R P dt.CtlIx dt.SlotIx dt.KIx dt.dd}
{I : Type}
(F : LaidFile dt A R P I)
(st : TapeSt dt A R P I)
:
The val-walked and the mir-walked presentations of one state
coincide: both are the naked background.
Dependency graph
The comparison atom, in the sequencer's shape #
theorem
DescriptiveComplexity.Draw.Data.ixCmp_hStage
{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]
[Finite R]
[Finite P]
{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)
(hsepP : F.toLayout.NameSep PR.zero ⋯)
(hix : IsLinOrd F.le)
[Nonempty A]
(vi : dt.VarIx)
(av : Fin dt.natMax)
(hnf : 2 ≤ dt.nfDim)
(isEq : Bool)
(j₁ j₂ : Fin (dt.nOf vi))
{emb : ElemPh 2 → P}
{exitPh : P}
{rEmb : (i : ElemSite 2) → ElemSh 2 i → R}
[Finite dt.KIx]
(hrules :
∀ (i : ElemSite 2) (ρ : ElemSh 2 i),
PR.rules (rEmb i ρ) = elemRule PR.one Slot.wk Slot.reg emb (dt.cmpArgs PR.zero PR.one vi av hnf isEq j₁ j₂).rdTrack
(dt.cmpArgs PR.zero PR.one vi av hnf isEq j₁ j₂).MatchOf
(dt.cmpArgs PR.zero PR.one vi av hnf isEq j₁ j₂).setFlag (dt.cmpArgs PR.zero PR.one vi av hnf isEq j₁ j₂).initEl
(dt.cmpArgs PR.zero PR.one vi av hnf isEq j₁ j₂).advEl (dt.cmpArgs PR.zero PR.one vi av hnf isEq j₁ j₂).exitSt
(dt.cmpArgs PR.zero PR.one vi av hnf isEq j₁ j₂).IsMaxEl exitPh i ρ)
(hR : PR.table.Reads)
(hlin : IsLinOrd WMLe)
{gbot : I}
(hbot : ∀ (y : I), F.le gbot y)
{v v' : Univ A R P dt.KIx dt.dd → Prop}
(hv : WMSetLt WMLe v (F.cell gbot))
(hvi : WMIncr WMLe v v')
{st : TapeSt dt A R P I}
(hwkSt : st.wk = fun (r : Univ A R P dt.KIx dt.dd → Prop) => r = v)
(f : dt.CtlIx → A)
(w : ℕ)
(hcost :
∀ (b : Lex (Fin dt.dd0 → A)) (k : Fin 2),
2 * (wideRank (F.cell (cmpCell F PR.zero hhasP vi j₁ j₂ b k)) - wideRank v) + 2 ≤ w)
:
(wideData (Univ A R P dt.KIx dt.dd)).ReachesIn (1 + ((2 + (w + 2) * 2) * (Nat.card (Lex (Fin dt.dd0 → A)) + 1) + 1))
{ state := Sum.inr (PR.stElt (emb ElemPh.e0) f), head := Sum.inl v',
tape :=
wideTape (PR.trackTapeAt F.cell Slot.val (dt.ixBack F.toLayout PR.zero PR.one ⋯ st) st.val) (PR.syElt PR.blank) }
{ state :=
Sum.inr
(PR.stElt exitPh
((dt.cmpArgs PR.zero PR.one vi av hnf isEq j₁ j₂).exitSt
(cmpFam F PR.zero PR.one hhasP vi av hnf isEq j₁ j₂ st v f (toLex topTup) (Fin.last 2))
(dt.ixBack F.toLayout PR.zero PR.one ⋯ st v))),
head := Sum.inl v',
tape :=
wideTape (PR.trackTapeAt F.cell Slot.val (dt.ixBack F.toLayout PR.zero PR.one ⋯ st) st.val) (PR.syElt PR.blank) }
The comparison atom, entered by a dispatch: from its entry
checkpoint one cell to the marker's right, at the Slot.val-walked
presentation, to the exit phase back at the same cell.
Dependency graph
The expansion atom, in the sequencer's shape #
theorem
DescriptiveComplexity.Draw.Data.ixExp_hStage
{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]
[Finite R]
[Finite P]
{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)
(hsepP : F.toLayout.NameSep PR.zero ⋯)
(hix : IsLinOrd F.le)
{elt : I → Univ A R P dt.KIx dt.dd}
(hinj : Function.Injective elt)
(helt :
∀ (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)
{k : ℕ}
(ts : Fin k → Fin (dt.nOf vi))
(e : dt.X.E.Relations k)
(av : Fin dt.natMax)
(hk : k * Fintype.card dt.X.Tag ≤ dt.ntgDim)
(hn : ∀ (τ' : Fin k → dt.X.Tag), (dt.relPk e τ').n ≤ dt.eDim)
(hrd : ∀ (τ' : Fin k → dt.X.Tag), dt.relNr e τ' ≤ dt.nfDim)
{emb : TagPh (k * Fintype.card dt.X.Tag) (Fin k → dt.X.Tag) (dt.relNr e) → P}
{exitPh : P}
{rEmb :
(i : TagSite (k * Fintype.card dt.X.Tag) (Fin k → dt.X.Tag) (dt.relNr e)) →
TagSh (k * Fintype.card dt.X.Tag) (Fin k → dt.X.Tag) (dt.relNr e) i → R}
[Finite dt.KIx]
(hrules :
∀ (i : TagSite (k * Fintype.card dt.X.Tag) (Fin k → dt.X.Tag) (dt.relNr e))
(ρ : TagSh (k * Fintype.card dt.X.Tag) (Fin k → dt.X.Tag) (dt.relNr e) i),
PR.rules (rEmb i ρ) = tagRule PR.one Slot.wk Slot.reg emb (dt.expArgs PR.zero PR.one vi ts e av hk hn hrd).rdTrackT
(dt.expArgs PR.zero PR.one vi ts e av hk hn hrd).MatchT
(dt.expArgs PR.zero PR.one vi ts e av hk hn hrd).setTagFlag
(dt.expArgs PR.zero PR.one vi ts e av hk hn hrd).TagsAre
(dt.expArgs PR.zero PR.one vi ts e av hk hn hrd).rdTrackE
(dt.expArgs PR.zero PR.one vi ts e av hk hn hrd).MatchE
(dt.expArgs PR.zero PR.one vi ts e av hk hn hrd).setFlagE
(dt.expArgs PR.zero PR.one vi ts e av hk hn hrd).initEl (dt.expArgs PR.zero PR.one vi ts e av hk hn hrd).advEl
(dt.expArgs PR.zero PR.one vi ts e av hk hn hrd).exitSt (dt.expArgs PR.zero PR.one vi ts e av hk hn hrd).IsMaxEl
exitPh i ρ)
(hR : PR.table.Reads)
(hlin : IsLinOrd WMLe)
{gbot : I}
(hbot : ∀ (y : I), F.le gbot y)
{v v' : Univ A R P dt.KIx dt.dd → Prop}
(hv : WMSetLt WMLe v (F.cell gbot))
(hvi : WMIncr WMLe v v')
{st : TapeSt dt A R P I}
(hwkSt : st.wk = fun (r : Univ A R P dt.KIx dt.dd → Prop) => r = v)
(pts : Fin k → dt.X.Map A)
(hENC :
∀ (ℓ : Fin k),
wmBlk (ixAddr elt (dt.lvSet st vi (ts ℓ))) (Tag.arg (toLex (dt.lvBlk vi (ts ℓ)))) = encMap dt.ly PR.zero PR.one (pts ℓ))
(f : dt.CtlIx → A)
(w : ℕ)
(hcostT :
∀ (i : Fin (k * Fintype.card dt.X.Tag)),
2 * (wideRank (F.cell (dt.ixExpTagCell F hhasP PR.one vi ts i)) - wideRank v) + 2 ≤ w)
(hcostE :
∀ (a : Lex (Fin dt.eDim → A)) (r : Fin (dt.relNr e fun (ℓ : Fin k) => (↑(pts ℓ)).1)),
2 * (wideRank (F.cell (dt.ixExpECell F hhasP PR.one vi ts e (fun (ℓ : Fin k) => (↑(pts ℓ)).1) ⋯ a r)) - wideRank v) + 2 ≤ w)
:
(wideData (Univ A R P dt.KIx dt.dd)).ReachesIn
(1 + ((w + 2) * (k * Fintype.card dt.X.Tag) + 2 + ((2 + (w + 2) * dt.relNr e fun (ℓ : Fin k) => (↑(pts ℓ)).1) * (Nat.card (Lex (Fin dt.eDim → A)) + 1) + 1)))
{ state := Sum.inr (PR.stElt (tagFirstRd emb) f), head := Sum.inl v',
tape :=
wideTape (PR.trackTapeAt F.cell Slot.val (dt.ixBack F.toLayout PR.zero PR.one ⋯ st) st.val) (PR.syElt PR.blank) }
{ state :=
Sum.inr
(PR.stElt exitPh
((dt.expArgs PR.zero PR.one vi ts e av hk hn hrd).exitSt (fun (ℓ : Fin k) => (↑(pts ℓ)).1)
(dt.ixExpFam F hhasP PR.one vi ts e av st (fun (ℓ : Fin k) => (↑(pts ℓ)).1) hk hn hrd v
(dt.ixExpTagFam F hhasP PR.one vi ts e av st hk hn hrd v f (Fin.last (k * Fintype.card dt.X.Tag)))
(toLex topTup) (Fin.last (dt.relNr e fun (ℓ : Fin k) => (↑(pts ℓ)).1)))
(dt.ixBack F.toLayout PR.zero PR.one ⋯ st v))),
head := Sum.inl v',
tape :=
wideTape (PR.trackTapeAt F.cell Slot.val (dt.ixBack F.toLayout PR.zero PR.one ⋯ st) st.val) (PR.syElt PR.blank) }
The expansion atom, entered by a dispatch: from its first phase one
cell to the marker's right, at the Slot.val-walked presentation, to the
exit phase back at the same cell.
Dependency graph
The stage atom, in the sequencer's shape #
theorem
DescriptiveComplexity.Draw.Data.ixStageEndSt_eq
{L : FirstOrder.Language}
{dt : Data L}
{A R P I : Type}
{st : TapeSt dt A R P I}
{elt : I → Univ A R P dt.KIx dt.dd}
{v : Univ A R P dt.KIx dt.dd → Prop}
(hs : st.sav = ixMark elt v)
(ht : st.tgt = ixMark elt v)
:
A stage atom entered at the boundary leaves the state unchanged, at an arbitrary file: with SAV and TARGET already the marks of the home address, the restore restores what was there.
Dependency graph
theorem
DescriptiveComplexity.Draw.Data.ixStage_hStage_thread
{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]
[Finite R]
[Finite P]
{PR : Prog A R P dt.CtlIx dt.SlotIx dt.KIx dt.dd}
{I : Type}
[Finite I]
(F : LaidFile dt A R P I)
(hhasP : F.toLayout.HasName PR.zero)
(hsepP : F.toLayout.NameSep PR.zero ⋯)
(hix : IsLinOrd F.le)
{elt : I → Univ A R P dt.KIx dt.dd}
(hinj : Function.Injective elt)
(helt :
∀ (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]
{e₀ : Univ A R P dt.KIx dt.dd}
(he₀ : ∀ (y : Univ A R P dt.KIx dt.dd), WMLe e₀ y)
(vi : dt.VarIx)
(iv : dt.d.B.ι)
(ts : Fin (dt.d.B.arity iv) → Fin (dt.nOf vi))
(av : Fin dt.natMax)
{emb : StagePh (dt.d.B.arity iv) → P}
{exitPh : P}
{rEmb : (i : StageSite (dt.d.B.arity iv)) → StageSh (dt.d.B.arity iv) i → R}
[Finite dt.KIx]
(hrules :
∀ (i : StageSite (dt.d.B.arity iv)) (ρ : StageSh (dt.d.B.arity iv) i),
PR.rules (rEmb i ρ) = dt.stageRule PR.zero PR.one emb (dt.stageArgs PR.zero PR.one vi iv ts av).srcTrack
(dt.stageArgs PR.zero PR.one vi iv ts av).srcBlk (dt.stageArgs PR.zero PR.one vi iv ts av).dstBlk
(dt.stageArgs PR.zero PR.one vi iv ts av).coord (dt.stageArgs PR.zero PR.one vi iv ts av).bitFlag
(dt.stageArgs PR.zero PR.one vi iv ts av).setBit (dt.stageArgs PR.zero PR.one vi iv ts av).initLv
(dt.stageArgs PR.zero PR.one vi iv ts av).advLv (dt.stageArgs PR.zero PR.one vi iv ts av).IsMaxLv
(dt.stageArgs PR.zero PR.one vi iv ts av).oldSlot (dt.stageArgs PR.zero PR.one vi iv ts av).setAv exitPh i ρ)
(hR : PR.table.Reads)
(hlin : IsLinOrd WMLe)
(hord : ∀ (x y : Univ A R P dt.KIx dt.dd), WMLe x y ↔ tagTupleLe x y)
{gtop gbot : I}
(htop : ∀ (y : I), F.le y gtop)
(hbot : ∀ (y : I), F.le gbot y)
(hwork :
∀ {r : Univ A R P dt.KIx dt.dd → Prop},
(∀ (x : Univ A R P dt.KIx dt.dd), r x → ∃ (i : dt.KIx), x.1 = Tag.arg i) → ∀ (u : I), WMSetLt WMLe r (F.cell u))
{v v' : Univ A R P dt.KIx dt.dd → Prop}
(hv : WMSetLt WMLe v (F.cell gbot))
(hvi : WMIncr WMLe v v')
{st : TapeSt dt A R P I}
(hwkSt : st.wk = fun (r : Univ A R P dt.KIx dt.dd → Prop) => r = v)
(hmirSt : st.mir = ixMark elt v)
(hbotSt : st.bot = fun (r : Univ A R P dt.KIx dt.dd → Prop) => r = fun (x : Univ A R P dt.KIx dt.dd) => False)
{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 P dt.KIx dt.dd), Use u → WMLt WMLe (elt u) x → ∃ (u' : I), Use u' ∧ elt u' = x)
(hvh : IxHolds elt Use v)
(hxdUse : ∀ (ℓ : Fin (dt.d.B.arity iv)) (bb : Lex (Fin dt.dd0 → A)), Use (dt.ixStageXD F hhasP ℓ bb))
(b : Bool)
(w wG wP wR wK : ℕ)
(hcost :
∀ (ℓ : Fin (dt.d.B.arity iv)) (a : Lex (Fin dt.dd0 → A)),
2 * (wideRank (F.cell (dt.ixStageXS F hhasP vi ts ℓ a)) - wideRank v) + 2 ≤ w ∧ 2 * (wideRank (F.cell (dt.ixStageXD F hhasP ℓ a)) - wideRank v) + 2 ≤ w)
(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 P dt.KIx dt.dd → Prop), WMSetLt WMLe s (F.cell gbot) → wideRank s + 4 ≤ wR)
(hwK :
∀ (T : Univ A R P 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)
(hb :
st.old iv
(ixAddr elt
(dt.ixStageTgt F hhasP vi ts
{ mir := st.mir, tgt := st.tgt, sav := ixMark elt v, val := st.val, old := st.old, new := st.new, wk := st.wk,
bot := st.bot, ltp := st.ltp }
(dt.d.B.arity iv))) ↔ b = true)
(f : dt.CtlIx → A)
:
(wideData (Univ A R P dt.KIx dt.dd)).ReachesIn
(5 * wP + 2 * wR + 2 * wK + ((2 * w + 8) * (Nat.card (Lex (Fin dt.dd0 → A)) + 1) + 1 + 1) * dt.d.B.arity iv + 13)
{ state := Sum.inr (PR.stElt (emb (StagePh.savP TrackPh.up)) f), head := Sum.inl v',
tape :=
wideTape (PR.trackTapeAt F.cell Slot.val (dt.ixBack F.toLayout PR.zero PR.one ⋯ st) st.val) (PR.syElt PR.blank) }
{ state :=
Sum.inr
(PR.stElt exitPh
((dt.stageArgs PR.zero PR.one vi iv ts av).setAv b
(dt.ixStageFAt F hhasP PR.one vi ts av st elt v f (dt.d.B.arity iv))
(dt.ixBack F.toLayout PR.zero PR.one ⋯
(dt.ixStageAtSt st elt v
(ixAddr elt
(dt.ixStageTgt F hhasP vi ts
{ mir := st.mir, tgt := st.tgt, sav := ixMark elt v, val := st.val, old := st.old, new := st.new,
wk := st.wk, bot := st.bot, ltp := st.ltp }
(dt.d.B.arity iv))))
(ixAddr elt
(dt.ixStageTgt F hhasP vi ts
{ mir := st.mir, tgt := st.tgt, sav := ixMark elt v, val := st.val, old := st.old, new := st.new,
wk := st.wk, bot := st.bot, ltp := st.ltp }
(dt.d.B.arity iv)))))),
head := Sum.inl v',
tape :=
wideTape
(PR.trackTapeAt F.cell Slot.val (dt.ixBack F.toLayout PR.zero PR.one ⋯ (dt.ixStageEndSt st elt v))
(dt.ixStageEndSt st elt v).val)
(PR.syElt PR.blank) }
The stage atom, threaded: the same run as
DescriptiveComplexity.Draw.Data.ixStage_hStage with no boundary
discipline assumed – the random access writes the home address into SAV and
TARGET whatever they held, so its exit state is the normalized
DescriptiveComplexity.Draw.Data.ixStageEndSt.
Dependency graph
theorem
DescriptiveComplexity.Draw.Data.ixStage_hStage
{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]
[Finite R]
[Finite P]
{PR : Prog A R P dt.CtlIx dt.SlotIx dt.KIx dt.dd}
{I : Type}
[Finite I]
(F : LaidFile dt A R P I)
(hhasP : F.toLayout.HasName PR.zero)
(hsepP : F.toLayout.NameSep PR.zero ⋯)
(hix : IsLinOrd F.le)
{elt : I → Univ A R P dt.KIx dt.dd}
(hinj : Function.Injective elt)
(helt :
∀ (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]
{e₀ : Univ A R P dt.KIx dt.dd}
(he₀ : ∀ (y : Univ A R P dt.KIx dt.dd), WMLe e₀ y)
(vi : dt.VarIx)
(iv : dt.d.B.ι)
(ts : Fin (dt.d.B.arity iv) → Fin (dt.nOf vi))
(av : Fin dt.natMax)
{emb : StagePh (dt.d.B.arity iv) → P}
{exitPh : P}
{rEmb : (i : StageSite (dt.d.B.arity iv)) → StageSh (dt.d.B.arity iv) i → R}
[Finite dt.KIx]
(hrules :
∀ (i : StageSite (dt.d.B.arity iv)) (ρ : StageSh (dt.d.B.arity iv) i),
PR.rules (rEmb i ρ) = dt.stageRule PR.zero PR.one emb (dt.stageArgs PR.zero PR.one vi iv ts av).srcTrack
(dt.stageArgs PR.zero PR.one vi iv ts av).srcBlk (dt.stageArgs PR.zero PR.one vi iv ts av).dstBlk
(dt.stageArgs PR.zero PR.one vi iv ts av).coord (dt.stageArgs PR.zero PR.one vi iv ts av).bitFlag
(dt.stageArgs PR.zero PR.one vi iv ts av).setBit (dt.stageArgs PR.zero PR.one vi iv ts av).initLv
(dt.stageArgs PR.zero PR.one vi iv ts av).advLv (dt.stageArgs PR.zero PR.one vi iv ts av).IsMaxLv
(dt.stageArgs PR.zero PR.one vi iv ts av).oldSlot (dt.stageArgs PR.zero PR.one vi iv ts av).setAv exitPh i ρ)
(hR : PR.table.Reads)
(hlin : IsLinOrd WMLe)
(hord : ∀ (x y : Univ A R P dt.KIx dt.dd), WMLe x y ↔ tagTupleLe x y)
{gtop gbot : I}
(htop : ∀ (y : I), F.le y gtop)
(hbot : ∀ (y : I), F.le gbot y)
(hwork :
∀ {r : Univ A R P dt.KIx dt.dd → Prop},
(∀ (x : Univ A R P dt.KIx dt.dd), r x → ∃ (i : dt.KIx), x.1 = Tag.arg i) → ∀ (u : I), WMSetLt WMLe r (F.cell u))
{v v' : Univ A R P dt.KIx dt.dd → Prop}
(hv : WMSetLt WMLe v (F.cell gbot))
(hvi : WMIncr WMLe v v')
{st : TapeSt dt A R P I}
(hwkSt : st.wk = fun (r : Univ A R P dt.KIx dt.dd → Prop) => r = v)
(hmirSt : st.mir = ixMark elt v)
(hbotSt : st.bot = fun (r : Univ A R P dt.KIx dt.dd → Prop) => r = fun (x : Univ A R P dt.KIx dt.dd) => False)
(hsav : st.sav = ixMark elt v)
(htgt : st.tgt = ixMark elt 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 P dt.KIx dt.dd), Use u → WMLt WMLe (elt u) x → ∃ (u' : I), Use u' ∧ elt u' = x)
(hvh : IxHolds elt Use v)
(hxdUse : ∀ (ℓ : Fin (dt.d.B.arity iv)) (bb : Lex (Fin dt.dd0 → A)), Use (dt.ixStageXD F hhasP ℓ bb))
(b : Bool)
(w wG wP wR wK : ℕ)
(hcost :
∀ (ℓ : Fin (dt.d.B.arity iv)) (a : Lex (Fin dt.dd0 → A)),
2 * (wideRank (F.cell (dt.ixStageXS F hhasP vi ts ℓ a)) - wideRank v) + 2 ≤ w ∧ 2 * (wideRank (F.cell (dt.ixStageXD F hhasP ℓ a)) - wideRank v) + 2 ≤ w)
(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 P dt.KIx dt.dd → Prop), WMSetLt WMLe s (F.cell gbot) → wideRank s + 4 ≤ wR)
(hwK :
∀ (T : Univ A R P 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)
(hb :
st.old iv
(ixAddr elt
(dt.ixStageTgt F hhasP vi ts
{ mir := st.mir, tgt := st.tgt, sav := ixMark elt v, val := st.val, old := st.old, new := st.new, wk := st.wk,
bot := st.bot, ltp := st.ltp }
(dt.d.B.arity iv))) ↔ b = true)
(f : dt.CtlIx → A)
:
(wideData (Univ A R P dt.KIx dt.dd)).ReachesIn
(5 * wP + 2 * wR + 2 * wK + ((2 * w + 8) * (Nat.card (Lex (Fin dt.dd0 → A)) + 1) + 1 + 1) * dt.d.B.arity iv + 13)
{ state := Sum.inr (PR.stElt (emb (StagePh.savP TrackPh.up)) f), head := Sum.inl v',
tape :=
wideTape (PR.trackTapeAt F.cell Slot.val (dt.ixBack F.toLayout PR.zero PR.one ⋯ st) st.val) (PR.syElt PR.blank) }
{ state :=
Sum.inr
(PR.stElt exitPh
((dt.stageArgs PR.zero PR.one vi iv ts av).setAv b
(dt.ixStageFAt F hhasP PR.one vi ts av st elt v f (dt.d.B.arity iv))
(dt.ixBack F.toLayout PR.zero PR.one ⋯
(dt.ixStageAtSt st elt v
(ixAddr elt
(dt.ixStageTgt F hhasP vi ts
{ mir := st.mir, tgt := st.tgt, sav := ixMark elt v, val := st.val, old := st.old, new := st.new,
wk := st.wk, bot := st.bot, ltp := st.ltp }
(dt.d.B.arity iv))))
(ixAddr elt
(dt.ixStageTgt F hhasP vi ts
{ mir := st.mir, tgt := st.tgt, sav := ixMark elt v, val := st.val, old := st.old, new := st.new,
wk := st.wk, bot := st.bot, ltp := st.ltp }
(dt.d.B.arity iv)))))),
head := Sum.inl v',
tape :=
wideTape (PR.trackTapeAt F.cell Slot.val (dt.ixBack F.toLayout PR.zero PR.one ⋯ st) st.val) (PR.syElt PR.blank) }
The stage atom, entered by a dispatch: at the boundary discipline – SAV and TARGET at the home address – the random access runs and restores the state, so the sequencer's background is untouched.
Dependency graph
One gate block, in the sequencer's shape #
theorem
DescriptiveComplexity.Draw.Data.ixGateBlock_hStage_pos
{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]
[Finite R]
[Finite P]
{PR : Prog A R P dt.CtlIx dt.SlotIx dt.KIx dt.dd}
{I : Type}
[Finite I]
(F : LaidFile dt A R P I)
(hhasP : F.toLayout.HasName PR.zero)
(hsepP : F.toLayout.NameSep PR.zero ⋯)
(hix : IsLinOrd F.le)
{elt : I → Univ A R P dt.KIx dt.dd}
(hinj : Function.Injective elt)
(helt :
∀ (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]
(b : Fin dt.ko ⊕ Fin dt.ki)
(hc : Fintype.card dt.X.Tag ≤ dt.ntgDim)
(hn : ∀ (t' : dt.X.Tag), (dt.domPk t').n ≤ dt.eDim)
(hrd : ∀ (t' : dt.X.Tag), dt.domNr t' ≤ dt.nfDim)
{emb : dt.GateBlockPh → P}
(wellG : (dt.SlotIx → A) → Prop)
(setFail : (dt.CtlIx → A) → (dt.SlotIx → A) → dt.CtlIx → A)
{failPh exitPh : P}
{rEmb : (i : dt.GateBlockSite) → dt.GateBlockSh i → R}
[Finite dt.KIx]
(hrules :
∀ (i : dt.GateBlockSite) (ρ : dt.GateBlockSh i),
PR.rules (rEmb i ρ) = dt.gateBlockRule PR.one emb (dt.gateArgs PR.zero PR.one b hc hn hrd) wellG setFail failPh exitPh 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)
{v v' : Univ A R P dt.KIx dt.dd → Prop}
(hv : WMSetLt WMLe v (F.cell gbot))
(hvi : WMIncr WMLe v v')
{st : TapeSt dt A R P I}
(hwkSt : st.wk = fun (r : Univ A R P dt.KIx dt.dd → Prop) => r = v)
(Test : I → Prop)
{wG : ℕ}
(hgap : ∀ (u u' : I), IxSucc F.le u u' → wideRank (F.cell u') - wideRank (F.cell u) ≤ wG)
(hcompat :
∀ (u : I),
wellG (PR.passTracksAt F.cell Slot.mir (dt.ixBack F.toLayout PR.zero PR.one ⋯ st) st.mir (F.cell u)) ↔ Test u)
(t : dt.X.Tag)
(htag : dt.dspTagOf PR.zero PR.one (wmBlk (ixAddr elt st.mir) (Tag.arg (toLex b))) = t)
(hTest : ∀ (u : I), Test u)
(f : dt.CtlIx → A)
(w : ℕ)
(hcostT :
∀ (c : Fin (Fintype.card dt.X.Tag)),
2 * (wideRank (F.cell (dt.ixGateTagCell F hhasP PR.one b c)) - wideRank v) + 2 ≤ w)
(hcostE :
∀ (a : Lex (Fin dt.eDim → A)) (r : Fin (dt.domNr t)),
2 * (wideRank (F.cell (dt.ixGateECell F hhasP PR.one b t ⋯ a r)) - wideRank v) + 2 ≤ w)
:
(wideData (Univ A R P dt.KIx dt.dd)).ReachesIn
(wideRank (F.cell gtop) + 2 + ((ixRank F.le gtop - ixRank F.le gbot) * wG + 1) + wideRank (F.cell gbot) + (1 + (1 + ((w + 2) * Fintype.card dt.X.Tag + 2 + ((2 + (w + 2) * dt.domNr t) * (Nat.card (Lex (Fin dt.eDim → A)) + 1) + 1)))))
{ state := Sum.inr (PR.stElt (emb (Sum.inl TestPh.up)) f), head := Sum.inl v',
tape :=
wideTape (PR.trackTapeAt F.cell Slot.val (dt.ixBack F.toLayout PR.zero PR.one ⋯ st) st.val) (PR.syElt PR.blank) }
{ state :=
Sum.inr
(PR.stElt exitPh
((dt.gateArgs PR.zero PR.one b hc hn hrd).exitSt t
(dt.ixGateFam F hhasP PR.one b st t hc hn hrd v
(dt.ixGateTagFam F hhasP PR.one b st hc hn hrd v f (Fin.last (Fintype.card dt.X.Tag))) (toLex topTup)
(Fin.last (dt.domNr t)))
(dt.ixBack F.toLayout PR.zero PR.one ⋯ st v))),
head := Sum.inl v',
tape :=
wideTape (PR.trackTapeAt F.cell Slot.val (dt.ixBack F.toLayout PR.zero PR.one ⋯ st) st.val) (PR.syElt PR.blank) }
A passing gate block, entered by a dispatch: every register is well-shaped, so the file test passes, the domain evaluation runs on the block's decoded tag, and the block exits to the next checkpoint.
Dependency graph
theorem
DescriptiveComplexity.Draw.Data.ixGateBlock_hStage_neg
{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]
[Finite R]
[Finite P]
{PR : Prog A R P dt.CtlIx dt.SlotIx dt.KIx dt.dd}
{I : Type}
[Finite I]
(F : LaidFile dt A R P I)
(hix : IsLinOrd F.le)
[Nonempty A]
[L.IsRelational]
[L.Structure A]
(b : Fin dt.ko ⊕ Fin dt.ki)
(hc : Fintype.card dt.X.Tag ≤ dt.ntgDim)
(hn : ∀ (t' : dt.X.Tag), (dt.domPk t').n ≤ dt.eDim)
(hrd : ∀ (t' : dt.X.Tag), dt.domNr t' ≤ dt.nfDim)
{emb : dt.GateBlockPh → P}
(wellG : (dt.SlotIx → A) → Prop)
(setFail : (dt.CtlIx → A) → (dt.SlotIx → A) → dt.CtlIx → A)
{failPh exitPh : P}
{rEmb : (i : dt.GateBlockSite) → dt.GateBlockSh i → R}
[Finite dt.KIx]
(hrules :
∀ (i : dt.GateBlockSite) (ρ : dt.GateBlockSh i),
PR.rules (rEmb i ρ) = dt.gateBlockRule PR.one emb (dt.gateArgs PR.zero PR.one b hc hn hrd) wellG setFail failPh exitPh 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)
{v v' : Univ A R P dt.KIx dt.dd → Prop}
(hv : WMSetLt WMLe v (F.cell gbot))
(hvi : WMIncr WMLe v v')
{st : TapeSt dt A R P I}
(hwkSt : st.wk = fun (r : Univ A R P dt.KIx dt.dd → Prop) => r = v)
(Test : I → Prop)
{wG : ℕ}
(hgap : ∀ (u u' : I), IxSucc F.le u u' → wideRank (F.cell u') - wideRank (F.cell u) ≤ wG)
(hcompat :
∀ (u : I),
wellG (PR.passTracksAt F.cell Slot.mir (dt.ixBack F.toLayout PR.zero PR.one ⋯ st) st.mir (F.cell u)) ↔ Test u)
{u : I}
(hTest : ¬Test u)
(f : dt.CtlIx → A)
:
(wideData (Univ A R P dt.KIx dt.dd)).ReachesIn
(wideRank (F.cell gtop) + 2 + ((ixRank F.le gtop - ixRank F.le gbot) * wG + 1) + wideRank (F.cell gbot) + 1)
{ state := Sum.inr (PR.stElt (emb (Sum.inl TestPh.up)) f), head := Sum.inl v',
tape :=
wideTape (PR.trackTapeAt F.cell Slot.val (dt.ixBack F.toLayout PR.zero PR.one ⋯ st) st.val) (PR.syElt PR.blank) }
{ state := Sum.inr (PR.stElt failPh (setFail f (dt.ixBack F.toLayout PR.zero PR.one ⋯ st v))), head := Sum.inl v',
tape :=
wideTape (PR.trackTapeAt F.cell Slot.val (dt.ixBack F.toLayout PR.zero PR.one ⋯ st) st.val) (PR.syElt PR.blank) }
A failing gate block: some register is not well-shaped, so the file test fails and the block leaves the whole gate sequence through the failing exit, the fail store applied at the marker's symbol.