A round trip to the register file #
Every visit the program pays to its register file has the same itinerary: scan
up to the file's top, bounce (two steps changing phase, since the scan
cannot overshoot the maximal cell), run one pass down the file, and scan back
to the working-cell marker. Only the middle differs – a mirror increment, a
file test, a track write. DescriptiveComplexity.Draw.Prog.reaches_fileRoundTrip
is the itinerary with the middle a hypothesis: any run from the file's top
to just below its bottom, changing at most the walked track.
The seek loop, the test rounds of a random access and the gate checks are all
this composite around their respective passes; DrawAdv's ADVANCE is the same
shape inlined with its two marker steps.
theorem
DescriptiveComplexity.Draw.Prog.reachesIn_fileRoundTrip
{A R P Q W K : Type}
{dd : ℕ}
[Fintype Q]
[Fintype W]
[DecidableEq W]
[LinearOrder A]
[LinearOrder R]
[LinearOrder P]
[LinearOrder K]
[FirstOrder.Language.wide.Structure (Univ A R P K dd)]
[Finite A]
[Finite R]
[Finite P]
[Finite K]
{I : Type}
{ile : I → I → Prop}
{PR : Prog A R P Q W K dd}
(F : IxFile (Univ A R P K dd) I ile)
(hR : PR.table.Reads)
(hlin : IsLinOrd WMLe)
(hix : IsLinOrd ile)
{t rl wk : W}
(hnerl : rl ≠ t)
(hnewk : wk ≠ t)
{gtop gbot : I}
(hbot : ∀ (y : I), ile gbot y)
{rest : (Univ A R P K dd → Prop) → W → A}
{m m₂ : I → Prop}
{wkAddr : Univ A R P K dd → Prop}
(hrl : ∀ (r : Univ A R P K dd → Prop), rest r rl = bitVal PR.zero PR.one (r = F.cell gtop))
(hwkS : ∀ (r : Univ A R P K dd → Prop), rest r wk = bitVal PR.zero PR.one (r = wkAddr))
{p₁ p₂b pIn pOut : P}
{fc : Q → A}
(hscanUp : ∀ (g : W → A), g rl ≠ PR.one → PR.HasRight p₁ fc g p₁ fc g)
(hb₁ :
PR.HasLeft p₁ fc (PR.passTracksAt F.cell t rest m (F.cell gtop)) p₂b fc
(PR.passTracksAt F.cell t rest m (F.cell gtop)))
(hb₂ : ∀ (g : W → A), PR.HasRight p₂b fc g pIn fc g)
{pend : Univ A R P K dd → Prop}
(hpend : WMIncr WMLe pend (F.cell gbot))
{n : ℕ}
(hmid :
(wideData (Univ A R P K dd)).ReachesIn n
{ state := Sum.inr (PR.stElt pIn fc), head := Sum.inl (F.cell gtop),
tape := wideTape (PR.trackTapeAt F.cell t rest m) (PR.syElt PR.blank) }
{ state := Sum.inr (PR.stElt pOut fc), head := Sum.inl pend,
tape := wideTape (PR.trackTapeAt F.cell t rest m₂) (PR.syElt PR.blank) })
(hback :
∀ (r : Univ A R P K dd → Prop),
(∀ (x : I), r ≠ F.cell x) →
PR.passTracksAt F.cell t rest m₂ r wk ≠ PR.one →
PR.HasLeft pOut fc (PR.passTracksAt F.cell t rest m₂ r) pOut fc (PR.passTracksAt F.cell t rest m₂ r))
(hwkLt : WMSetLt WMLe wkAddr (F.cell gbot))
{s : Univ A R P K dd → Prop}
(hsle : WMSetLe WMLe s (F.cell gtop))
:
(wideData (Univ A R P K dd)).ReachesIn (wideRank (F.cell gtop) - wideRank s + 2 + n + (wideRank pend - wideRank wkAddr))
{ state := Sum.inr (PR.stElt p₁ fc), head := Sum.inl s,
tape := wideTape (PR.trackTapeAt F.cell t rest m) (PR.syElt PR.blank) }
{ state := Sum.inr (PR.stElt pOut fc), head := Sum.inl wkAddr,
tape := wideTape (PR.trackTapeAt F.cell t rest m₂) (PR.syElt PR.blank) }
A round trip to the register file: from anywhere at or below the file's top, scan up to it, bounce into the pass phase, run the middle – any run from the top to just below the file, changing at most the walked track – and scan back down to the working-cell marker. The marker sits strictly below the file, so the return scan's stop is unique.
Dependency graph
theorem
DescriptiveComplexity.Draw.Prog.reaches_fileRoundTrip
{A R P Q W K : Type}
{dd : ℕ}
[Fintype Q]
[Fintype W]
[DecidableEq W]
[LinearOrder A]
[LinearOrder R]
[LinearOrder P]
[LinearOrder K]
[FirstOrder.Language.wide.Structure (Univ A R P K dd)]
[Finite A]
[Finite R]
[Finite P]
[Finite K]
{I : Type}
{ile : I → I → Prop}
{PR : Prog A R P Q W K dd}
(F : IxFile (Univ A R P K dd) I ile)
(hR : PR.table.Reads)
(hlin : IsLinOrd WMLe)
(hix : IsLinOrd ile)
{t rl wk : W}
(hnerl : rl ≠ t)
(hnewk : wk ≠ t)
{gtop gbot : I}
(hbot : ∀ (y : I), ile gbot y)
{rest : (Univ A R P K dd → Prop) → W → A}
{m m₂ : I → Prop}
{wkAddr : Univ A R P K dd → Prop}
(hrl : ∀ (r : Univ A R P K dd → Prop), rest r rl = bitVal PR.zero PR.one (r = F.cell gtop))
(hwkS : ∀ (r : Univ A R P K dd → Prop), rest r wk = bitVal PR.zero PR.one (r = wkAddr))
{p₁ p₂b pIn pOut : P}
{fc : Q → A}
(hscanUp : ∀ (g : W → A), g rl ≠ PR.one → PR.HasRight p₁ fc g p₁ fc g)
(hb₁ :
PR.HasLeft p₁ fc (PR.passTracksAt F.cell t rest m (F.cell gtop)) p₂b fc
(PR.passTracksAt F.cell t rest m (F.cell gtop)))
(hb₂ : ∀ (g : W → A), PR.HasRight p₂b fc g pIn fc g)
{pend : Univ A R P K dd → Prop}
(hpend : WMIncr WMLe pend (F.cell gbot))
(hmid :
Relation.ReflTransGen (wideData (Univ A R P K dd)).Step
{ state := Sum.inr (PR.stElt pIn fc), head := Sum.inl (F.cell gtop),
tape := wideTape (PR.trackTapeAt F.cell t rest m) (PR.syElt PR.blank) }
{ state := Sum.inr (PR.stElt pOut fc), head := Sum.inl pend,
tape := wideTape (PR.trackTapeAt F.cell t rest m₂) (PR.syElt PR.blank) })
(hback :
∀ (r : Univ A R P K dd → Prop),
(∀ (x : I), r ≠ F.cell x) →
PR.passTracksAt F.cell t rest m₂ r wk ≠ PR.one →
PR.HasLeft pOut fc (PR.passTracksAt F.cell t rest m₂ r) pOut fc (PR.passTracksAt F.cell t rest m₂ r))
(hwkLt : WMSetLt WMLe wkAddr (F.cell gbot))
{s : Univ A R P K dd → Prop}
(hsle : WMSetLe WMLe s (F.cell gtop))
:
Relation.ReflTransGen (wideData (Univ A R P K dd)).Step
{ state := Sum.inr (PR.stElt p₁ fc), head := Sum.inl s,
tape := wideTape (PR.trackTapeAt F.cell t rest m) (PR.syElt PR.blank) }
{ state := Sum.inr (PR.stElt pOut fc), head := Sum.inl wkAddr,
tape := wideTape (PR.trackTapeAt F.cell t rest m₂) (PR.syElt PR.blank) }
A round trip to the register file, the budget forgotten.