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.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.