Guessing the certificate onto the region

The certificate is one bit per address of the region, not per register of the file: the evaluation reads its dictionary at the address whose argument blocks encode a tuple of points, and there are 2 ^ (k · nᵈ) of those, where the file has one register per block and tuple and is polynomial. So the guessing sweep is not the file-laying sweep with a different write; it is a walk over the region.

That has one consequence for its rules, and it is what this file is: the walk cannot be pointer-driven. A pointer holds a block and a tuple and can count the file's registers; it cannot count the region. So the guess is a sweep in the space-bounded program's style – one phase for the whole walk, a nondeterministic write, a step right – and its exit is a rule available at every address, so that where the guess stops is one more nondeterministic choice. Nothing has to recognize the region's end: the run a yes-instance exhibits stops at the logical top, and a run that stops earlier has left its remaining bits clear, which is a certificate like any other.

The rules are the program's own at DescriptiveComplexity.Draw.Data.regionSpec – a guess specification whose pointer never moves, so that the site's roll-over arm is the walk's every step – together with the stopping rule hasLeft_guessStop. The sweep is reachesIn_guessRegion, at the stretch's own length, and the whole phase – sweep, stop, walk home – is reachesIn_guessRegionPhase.

theorem DescriptiveComplexity.Draw.Data.hasRight_guessRegion {L : FirstOrder.Language} {dt : Data L} {A R' I PE : Type} [Fintype dt.CtlIx] [Fintype dt.SlotIx] [DecidableEq dt.SlotIx] [LinearOrder A] [LinearOrder R'] [LinearOrder (NexPh (Option dt.KIx) PE)] [FirstOrder.Language.wide.Structure (Univ A R' (NexPh (Option dt.KIx) PE) dt.KIx dt.dd)] {PR : Prog A R' (NexPh (Option dt.KIx) PE) dt.CtlIx dt.SlotIx dt.KIx dt.dd} {F : LaidFile dt A R' (NexPh (Option dt.KIx) PE) I} {m : I → Prop} {SE : Type} {ShE : SE → Type} {f₀ : dt.CtlIx → A} {ruleE : (e : SE) → ShE e → Rule A dt.CtlIx dt.SlotIx (NexPh (Option dt.KIx) PE)} {evalEntry : PE} {bot : Option dt.KIx} {β : SweepSpec A dt.CtlIx dt.SlotIx (Option dt.KIx)} {rEmb : (i : NexSite SE) → NexSh SE (Option dt.KIx) (dt.d.B.ι → Bool) ShE i → R'} (hrules : ∀ (i : NexSite SE) (ρ : NexSh SE (Option dt.KIx) (dt.d.B.ι → Bool) ShE i), PR.rules (rEmb i ρ) = dt.nexRule PR.one β (dt.regionSpec PR.zero PR.one) ruleE evalEntry bot i ρ) {st : TapeSt dt A R' (NexPh (Option dt.KIx) PE) I} (σ : dt.d.B.ι → (Univ A R' (NexPh (Option dt.KIx) PE) dt.KIx dt.dd → Prop) → Prop) {t : dt.SlotIx} (hne : ∀ (i : dt.d.B.ι), Slot.old i ≠ t) (b : Option dt.KIx) (r : Univ A R' (NexPh (Option dt.KIx) PE) dt.KIx dt.dd → Prop) : PR.HasRight (NexPh.guessP b) f₀ (PR.passTracksAt F.cell t (dt.ixBack F.toLayout PR.zero PR.one ⋯ st) m r) (NexPh.guessP b) f₀ (PR.passTracksAt F.cell t (dt.ixBack F.toLayout PR.zero PR.one ⋯ { mir := st.mir, tgt := st.tgt, sav := st.sav, val := st.val, old := σ, new := st.new, wk := st.wk, bot := st.bot, ltp := st.ltp }) m r)

The write step of the region-wide guess, at an address of the stretch: the rule whose bit vector is the certificate's there fires. It is the guess site's roll-over arm – at regionSpec the pointer never moves, so that arm's guard is always true and its destination is the phase it came from.

theorem DescriptiveComplexity.Draw.Data.reachesIn_guessRegion {L : FirstOrder.Language} {dt : Data L} {A R' I PE : Type} [Fintype dt.CtlIx] [Fintype dt.SlotIx] [DecidableEq dt.SlotIx] [LinearOrder A] [LinearOrder R'] [LinearOrder (NexPh (Option dt.KIx) PE)] [FirstOrder.Language.wide.Structure (Univ A R' (NexPh (Option dt.KIx) PE) dt.KIx dt.dd)] [Finite A] [Finite R'] [Finite (NexPh (Option dt.KIx) PE)] [Finite dt.KIx] {PR : Prog A R' (NexPh (Option dt.KIx) PE) dt.CtlIx dt.SlotIx dt.KIx dt.dd} {F : LaidFile dt A R' (NexPh (Option dt.KIx) PE) I} {m : I → Prop} {SE : Type} {ShE : SE → Type} {f₀ : dt.CtlIx → A} {ruleE : (e : SE) → ShE e → Rule A dt.CtlIx dt.SlotIx (NexPh (Option dt.KIx) PE)} {evalEntry : PE} {bot : Option dt.KIx} {β : SweepSpec A dt.CtlIx dt.SlotIx (Option dt.KIx)} {rEmb : (i : NexSite SE) → NexSh SE (Option dt.KIx) (dt.d.B.ι → Bool) ShE i → R'} (hrules : ∀ (i : NexSite SE) (ρ : NexSh SE (Option dt.KIx) (dt.d.B.ι → Bool) ShE i), PR.rules (rEmb i ρ) = dt.nexRule PR.one β (dt.regionSpec PR.zero PR.one) ruleE evalEntry bot i ρ) (hR : PR.table.Reads) (hlin : IsLinOrd WMLe) {st : TapeSt dt A R' (NexPh (Option dt.KIx) PE) I} (σ : dt.d.B.ι → (Univ A R' (NexPh (Option dt.KIx) PE) dt.KIx dt.dd → Prop) → Prop) {t : dt.SlotIx} (hne : ∀ (i : dt.d.B.ι), Slot.old i ≠ t) (b : Option dt.KIx) {s₀ s₁ : Univ A R' (NexPh (Option dt.KIx) PE) dt.KIx dt.dd → Prop} (hle : WMSetLe WMLe s₀ s₁) (hout : ∀ (i : dt.d.B.ι) (r : Univ A R' (NexPh (Option dt.KIx) PE) dt.KIx dt.dd → Prop), WMSetLt WMLe r s₀ ∨ ¬WMSetLt WMLe r s₁ → (σ i r ↔ st.old i r)) : (wideData (Univ A R' (NexPh (Option dt.KIx) PE) dt.KIx dt.dd)).ReachesIn (wideRank s₁ - wideRank s₀) { state := Sum.inr (PR.stElt (NexPh.guessP b) f₀), head := Sum.inl s₀, tape := wideTape (PR.trackTapeAt F.cell t (dt.ixBack F.toLayout PR.zero PR.one ⋯ st) m) (PR.syElt PR.blank) } { state := Sum.inr (PR.stElt (NexPh.guessP b) f₀), head := Sum.inl s₁, tape := wideTape (PR.trackTapeAt F.cell t (dt.ixBack F.toLayout PR.zero PR.one ⋯ { mir := st.mir, tgt := st.tgt, sav := st.sav, val := st.val, old := σ, new := st.new, wk := st.wk, bot := st.bot, ltp := st.ltp }) m) (PR.syElt PR.blank) }

The clocked program guesses its certificate onto the region: one nondeterministic write per address of the stretch, at the stretch's own length. The walk carries no pointer – every step is the same rule at the same phase – so it is as long as the region asks and no wider than a bit vector.

theorem DescriptiveComplexity.Draw.Data.reachesIn_guessRegionPhase {L : FirstOrder.Language} {dt : Data L} {A R' I PE : Type} [Fintype dt.CtlIx] [Fintype dt.SlotIx] [DecidableEq dt.SlotIx] [LinearOrder A] [LinearOrder R'] [LinearOrder (NexPh (Option dt.KIx) PE)] [FirstOrder.Language.wide.Structure (Univ A R' (NexPh (Option dt.KIx) PE) dt.KIx dt.dd)] [Finite A] [Finite R'] [Finite (NexPh (Option dt.KIx) PE)] [Finite dt.KIx] {PR : Prog A R' (NexPh (Option dt.KIx) PE) dt.CtlIx dt.SlotIx dt.KIx dt.dd} {F : LaidFile dt A R' (NexPh (Option dt.KIx) PE) I} {m : I → Prop} {SE : Type} {ShE : SE → Type} {f₀ : dt.CtlIx → A} {ruleE : (e : SE) → ShE e → Rule A dt.CtlIx dt.SlotIx (NexPh (Option dt.KIx) PE)} {evalEntry : PE} {bot : Option dt.KIx} {β : SweepSpec A dt.CtlIx dt.SlotIx (Option dt.KIx)} {rEmb : (i : NexSite SE) → NexSh SE (Option dt.KIx) (dt.d.B.ι → Bool) ShE i → R'} (hrules : ∀ (i : NexSite SE) (ρ : NexSh SE (Option dt.KIx) (dt.d.B.ι → Bool) ShE i), PR.rules (rEmb i ρ) = dt.nexRule PR.one β (dt.regionSpec PR.zero PR.one) ruleE evalEntry bot i ρ) (hR : PR.table.Reads) (hlin : IsLinOrd WMLe) {st : TapeSt dt A R' (NexPh (Option dt.KIx) PE) I} (σ : dt.d.B.ι → (Univ A R' (NexPh (Option dt.KIx) PE) dt.KIx dt.dd → Prop) → Prop) {t : dt.SlotIx} (hne : ∀ (i : dt.d.B.ι), Slot.old i ≠ t) (hnewk : Slot.wk ≠ t) (b : Option dt.KIx) {v s₀ s₁ : Univ A R' (NexPh (Option dt.KIx) PE) dt.KIx dt.dd → Prop} (hwkS : st.wk = fun (r : Univ A R' (NexPh (Option dt.KIx) PE) dt.KIx dt.dd → Prop) => r = v) (hle : WMSetLe WMLe s₀ s₁) (hv : WMSetLt WMLe v s₀) (hne₁ : ∃ (x : Univ A R' (NexPh (Option dt.KIx) PE) dt.KIx dt.dd), s₁ x) {rHome : HomeKit.HomeRule → R'} (hrulesH : ∀ (ρ : HomeKit.HomeRule), PR.rules (rHome ρ) = { t := t, wk := Slot.wk, ph := NexPh.homeGuessP }.rule PR.one ρ) (hout : ∀ (i : dt.d.B.ι) (r : Univ A R' (NexPh (Option dt.KIx) PE) dt.KIx dt.dd → Prop), WMSetLt WMLe r s₀ ∨ ¬WMSetLt WMLe r s₁ → (σ i r ↔ st.old i r)) : (wideData (Univ A R' (NexPh (Option dt.KIx) PE) dt.KIx dt.dd)).ReachesIn (wideRank s₁ - wideRank s₀ + (wideRank s₁ - wideRank v) + 1) { state := Sum.inr (PR.stElt (NexPh.guessP b) f₀), head := Sum.inl s₀, tape := wideTape (PR.trackTapeAt F.cell t (dt.ixBack F.toLayout PR.zero PR.one ⋯ st) m) (PR.syElt PR.blank) } { state := Sum.inr (PR.stElt NexPh.homeGuessP f₀), head := Sum.inl v, tape := wideTape (PR.trackTapeAt F.cell t (dt.ixBack F.toLayout PR.zero PR.one ⋯ { mir := st.mir, tgt := st.tgt, sav := st.sav, val := st.val, old := σ, new := st.new, wk := st.wk, bot := st.bot, ltp := st.ltp }) m) (PR.syElt PR.blank) }

The whole guessing phase of a clocked program: the sweep over the region, the stop – which may fall anywhere, and here falls at the stretch's top – and the walk home to the marker. Its cost is the stretch out and back with the one step that turns round.