Plain sweeps: one step per address, a flag or a write

COMPARE and COPY are plain sweeps: one step per address of a stretch, no register visits, no rounds. This file is their two shapes.

• DescriptiveComplexity.Draw.Prog.reaches_flagSweep – the machine walks the stretch asking one question per cell, the verdict carried in the phase: the passing one exactly while every cell so far passed (DescriptiveComplexity.sweepState, whose two ends the caller reads off DescriptiveComplexity.sweepState_bot / DescriptiveComplexity.sweepStateAfter_pos / _neg). COMPARE is this with these two stage tracks agree here.
• DescriptiveComplexity.Draw.Prog.reaches_writeSweep – the machine walks the stretch rewriting each cell's background once, the background presented as a function of the frontier. COPY is this with the current stage track takes the next one's digit.

Both take their rules cell-coupled and bounded to the stretch, for the reason DrawAdv taught: a sweep whose stepping rules covered every cell could never stop. How a program's actual rules respect the bound is its own business – the intended device is a permanent end marker planted at the top of the logical interval once, at startup, since a cell of the working area is not otherwise recognizable (its tracks are stage bits like any other).

theorem DescriptiveComplexity.Draw.Prog.reaches_flagSweep {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] {PR : Prog A R P Q W K dd} {I : Type} {cell : I → Univ A R P K dd → Prop} (hR : PR.table.Reads) (hlin : IsLinOrd WMLe) {t : W} {rest : (Univ A R P K dd → Prop) → W → A} {m : I → Prop} {Test : (Univ A R P K dd → Prop) → Prop} {py pn : P} {f : Q → A} {s₀ s₁ : Univ A R P K dd → Prop} (hle : WMSetLe WMLe s₀ s₁) (hstepY : ∀ (r r' : Univ A R P K dd → Prop), WMIncr WMLe r r' → WMSetLe WMLe s₀ r → WMSetLe WMLe r' s₁ → Test r → PR.HasRight py f (PR.passTracksAt cell t rest m r) py f (PR.passTracksAt cell t rest m r)) (hstepN : ∀ (r r' : Univ A R P K dd → Prop), WMIncr WMLe r r' → WMSetLe WMLe s₀ r → WMSetLe WMLe r' s₁ → ¬Test r → PR.HasRight py f (PR.passTracksAt cell t rest m r) pn f (PR.passTracksAt cell t rest m r)) (hstepP : ∀ (r r' : Univ A R P K dd → Prop), WMIncr WMLe r r' → WMSetLe WMLe s₀ r → WMSetLe WMLe r' s₁ → PR.HasRight pn f (PR.passTracksAt cell t rest m r) pn f (PR.passTracksAt cell t rest m r)) : Relation.ReflTransGen (wideData (Univ A R P K dd)).Step { state := Sum.inr (sweepState Test (PR.stElt py f) (PR.stElt pn f) s₀), head := Sum.inl s₀, tape := wideTape (PR.trackTapeAt cell t rest m) (PR.syElt PR.blank) } { state := Sum.inr (sweepState Test (PR.stElt py f) (PR.stElt pn f) s₁), head := Sum.inl s₁, tape := wideTape (PR.trackTapeAt cell t rest m) (PR.syElt PR.blank) }

A flag sweep, the budget forgotten.

theorem DescriptiveComplexity.Draw.Prog.reaches_writeSweep {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] {PR : Prog A R P Q W K dd} {I : Type} {cell : I → Univ A R P K dd → Prop} (hR : PR.table.Reads) (hlin : IsLinOrd WMLe) {t : W} {m : I → Prop} {restAt : (Univ A R P K dd → Prop) → (Univ A R P K dd → Prop) → W → A} {p : P} {f : Q → A} {s₀ s₁ : Univ A R P K dd → Prop} (hle : WMSetLe WMLe s₀ s₁) (hframe : ∀ (s u : Univ A R P K dd → Prop), WMIncr WMLe s u → WMSetLe WMLe s₀ s → WMSetLe WMLe u s₁ → ∀ (r : Univ A R P K dd → Prop), r ≠ s → restAt u r = restAt s r) (hstep : ∀ (s u : Univ A R P K dd → Prop), WMIncr WMLe s u → WMSetLe WMLe s₀ s → WMSetLe WMLe u s₁ → PR.HasRight p f (PR.passTracksAt cell t (restAt s) m s) p f (PR.passTracksAt cell t (restAt u) m s)) : Relation.ReflTransGen (wideData (Univ A R P K dd)).Step { state := Sum.inr (PR.stElt p f), head := Sum.inl s₀, tape := wideTape (PR.trackTapeAt cell t (restAt s₀) m) (PR.syElt PR.blank) } { state := Sum.inr (PR.stElt p f), head := Sum.inl s₁, tape := wideTape (PR.trackTapeAt cell t (restAt s₁) m) (PR.syElt PR.blank) }

A writing sweep, the budget forgotten.

Installing a background

The two phases a clocked program opens with – laying its own register file out and guessing the certificate onto its working region – are one shape: sweep a stretch replacing the background wholesale, one cell per step. The frontier form DescriptiveComplexity.midTape is what makes them a sweep rather than an induction, and the new background is a parameter, so the guessing reading is the same statement at an arbitrary choice.

theorem DescriptiveComplexity.Draw.Prog.reachesIn_installSweep {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] {PR : Prog A R P Q W K dd} {I : Type} {cell : I → Univ A R P K dd → Prop} (hR : PR.table.Reads) (hlin : IsLinOrd WMLe) {t : W} {m : I → Prop} {bg₀ bg₁ : (Univ A R P K dd → Prop) → W → A} {ph : (Univ A R P K dd → Prop) → P} {fc : (Univ A R P K dd → Prop) → Q → A} {s₀ s₁ : Univ A R P K dd → Prop} (hle : WMSetLe WMLe s₀ s₁) (hstep : ∀ (s u : Univ A R P K dd → Prop), WMIncr WMLe s u → WMSetLe WMLe s₀ s → WMSetLe WMLe u s₁ → PR.HasRight (ph s) (fc s) (PR.passTracksAt cell t bg₀ m s) (ph u) (fc u) (PR.passTracksAt cell t bg₁ m s)) : (wideData (Univ A R P K dd)).ReachesIn (wideRank s₁ - wideRank s₀) { state := Sum.inr (PR.stElt (ph s₀) (fc s₀)), head := Sum.inl s₀, tape := wideTape (PR.trackTapeAt cell t (midTape bg₀ bg₁ s₀) m) (PR.syElt PR.blank) } { state := Sum.inr (PR.stElt (ph s₁) (fc s₁)), head := Sum.inl s₁, tape := wideTape (PR.trackTapeAt cell t (midTape bg₀ bg₁ s₁) m) (PR.syElt PR.blank) }

A phase installing a new background over a stretch. From the bottom of the stretch with the old background everywhere, one rule per cell rewrites that cell and moves right; the run ends at the top of the stretch with the new background below it and the old one above. The pointer walks along, so the rule at a cell may write something that depends on where the head is.

theorem DescriptiveComplexity.Draw.Prog.reachesIn_installOut {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] {PR : Prog A R P Q W K dd} {I : Type} {cell : I → Univ A R P K dd → Prop} (hR : PR.table.Reads) (hlin : IsLinOrd WMLe) {t : W} {m : I → Prop} {bg₀ bg₁ : (Univ A R P K dd → Prop) → W → A} {ph : (Univ A R P K dd → Prop) → P} {fc : (Univ A R P K dd → Prop) → Q → A} {s₀ s₁ : Univ A R P K dd → Prop} (hle : WMSetLe WMLe s₀ s₁) (hbelow : ∀ (r : Univ A R P K dd → Prop), WMSetLt WMLe r s₀ → bg₁ r = bg₀ r) (habove : ∀ (r : Univ A R P K dd → Prop), ¬WMSetLt WMLe r s₁ → bg₁ r = bg₀ r) (hstep : ∀ (s u : Univ A R P K dd → Prop), WMIncr WMLe s u → WMSetLe WMLe s₀ s → WMSetLe WMLe u s₁ → PR.HasRight (ph s) (fc s) (PR.passTracksAt cell t bg₀ m s) (ph u) (fc u) (PR.passTracksAt cell t bg₁ m s)) : (wideData (Univ A R P K dd)).ReachesIn (wideRank s₁ - wideRank s₀) { state := Sum.inr (PR.stElt (ph s₀) (fc s₀)), head := Sum.inl s₀, tape := wideTape (PR.trackTapeAt cell t bg₀ m) (PR.syElt PR.blank) } { state := Sum.inr (PR.stElt (ph s₁) (fc s₁)), head := Sum.inl s₁, tape := wideTape (PR.trackTapeAt cell t bg₁ m) (PR.syElt PR.blank) }

A phase installing a background that already agrees outside the stretch. The sweep only ever writes inside the stretch, so if the background it is installing is the one already there below the start and at or above the end, the run begins and ends at that background whole rather than at a frontier form. That is the shape every opening phase of a program takes: what it changes lies in a stretch, and what lies outside it was right to begin with.