What the clocked program's file-laying sweep writes

DescriptiveComplexity.Draw.SweepSpec leaves the write to the caller, because what a cell of the file holds is a fact about the layout and not about the shape of the loop. This file is that fact at the layout a clocked program uses (DescriptiveComplexity.Draw.Data.blkLaid): the sweep writes, at the register the pointer names, the mark of that register – it is a register, whether it is the first or the last of the file, its block one-hot, its coordinates, and that it is canonically padded – and the blank in every track.

The one theorem is that this is the background the file's run installs (DescriptiveComplexity.Draw.Data.buildWr_eq_ixBack): slot by slot, the mark the pointer can compute agrees with DescriptiveComplexity.Draw.Data.ixBack at the register's cell, given that the state's own tracks are clear – which they are, the file being laid before anything is written to it.

What makes the agreement possible at all is that a register's contents depend on its block and its named tuple and on nothing else, which is the point the whole index parameter was introduced for: the pointer holds exactly those, the block in the phase and the tuple in the control.

The pointer's advance is here too: DescriptiveComplexity.Draw.Data.ptrNext writes the next register's tuple into the control's coordinate slots and leaves every other slot alone, and DescriptiveComplexity.Draw.Data.buildSpec is the whole DescriptiveComplexity.Draw.SweepSpec the file-laying phase runs at. The guessing phase's write is here as well (DescriptiveComplexity.Draw.Data.guessWr): the cell it read with the stage tracks holding the guessed value, and nothing else touched.

def DescriptiveComplexity.Draw.Data.ptrTup {L : FirstOrder.Language} (dt : Data L) {A : Type} (coord : Fin dt.dd → dt.CtlIx) (f : dt.CtlIx → A) : Fin dt.dd → A

The tuple the pointer holds: the control's coordinates, at the slots the caller reserved for them.

Equations

• dt.ptrTup coord f j = f (coord j)

noncomputable def DescriptiveComplexity.Draw.Data.buildWr {L : FirstOrder.Language} (dt : Data L) {A : Type} [LinearOrder A] [Finite A] [Nonempty A] [Finite dt.KIx] (zero one : A) (coord : Fin dt.dd → dt.CtlIx) (b : Option dt.KIx) (f : dt.CtlIx → A) : dt.SlotIx → A

What the file-laying sweep writes: the mark of the register the pointer names, and the blank in every track. Every one of these is read off the block the phase carries and the coordinates the control holds, which is what makes it a legal DescriptiveComplexity.Draw.SweepSpec.wr.

Equations

• dt.buildWr zero one coord b f DescriptiveComplexity.Draw.Slot.reg = one
• dt.buildWr zero one coord b f DescriptiveComplexity.Draw.Slot.regFirst = DescriptiveComplexity.Draw.bitVal zero one ((b, dt.ptrTup coord f) = DescriptiveComplexity.blkBot A dt.KIx dt.dd)
• dt.buildWr zero one coord b f DescriptiveComplexity.Draw.Slot.regLast = DescriptiveComplexity.Draw.bitVal zero one ((b, dt.ptrTup coord f) = DescriptiveComplexity.blkTop A dt.KIx dt.dd)
• dt.buildWr zero one coord b f (DescriptiveComplexity.Draw.Slot.blk c) = DescriptiveComplexity.Draw.bitVal zero one (b = c)
• dt.buildWr zero one coord b f (DescriptiveComplexity.Draw.Slot.name j) = f (coord (Fin.castLE ⋯ j))
• dt.buildWr zero one coord b f DescriptiveComplexity.Draw.Slot.pdd = DescriptiveComplexity.Draw.bitVal zero one (∀ (j : Fin dt.dd), dt.dd0 ≤ ↑j → f (coord j) = zero)
• dt.buildWr zero one coord b f DescriptiveComplexity.Draw.Slot.mir = zero
• dt.buildWr zero one coord b f DescriptiveComplexity.Draw.Slot.tgt = zero
• dt.buildWr zero one coord b f DescriptiveComplexity.Draw.Slot.sav = zero
• dt.buildWr zero one coord b f DescriptiveComplexity.Draw.Slot.val = zero
• dt.buildWr zero one coord b f DescriptiveComplexity.Draw.Slot.wk = zero
• dt.buildWr zero one coord b f DescriptiveComplexity.Draw.Slot.bot = zero
• dt.buildWr zero one coord b f DescriptiveComplexity.Draw.Slot.ltp = zero
• dt.buildWr zero one coord b f (DescriptiveComplexity.Draw.Slot.old a) = zero
• dt.buildWr zero one coord b f (DescriptiveComplexity.Draw.Slot.new a) = zero

theorem DescriptiveComplexity.Draw.Data.buildWr_eq_ixBack {L : FirstOrder.Language} {dt : Data L} {A R' P' : Type} [LinearOrder A] [LinearOrder R'] [LinearOrder P'] [Finite A] [Nonempty A] [Finite dt.KIx] [FirstOrder.Language.wide.Structure (Univ A R' P' dt.KIx dt.dd)] [Finite (Univ A R' P' dt.KIx dt.dd)] {zero one : A} (coord : Fin dt.dd → dt.CtlIx) (hdd : dt.dd0 ≤ dt.dd) (h : IsLinOrd WMLe) {base : ℕ} (hpos : 0 < base) (hbase : base + Nat.card (Wide.BlkIx dt.KIx A dt.dd) ≤ Nat.card { p : WPoint (Univ A R' P' dt.KIx dt.dd) // (wideData (Univ A R' P' dt.KIx dt.dd)).Posn p }) {st : TapeSt dt A R' P' (Wide.BlkIx dt.KIx A dt.dd)} (hmir : ∀ (u : Wide.BlkIx dt.KIx A dt.dd), ¬st.mir u) (htgt : ∀ (u : Wide.BlkIx dt.KIx A dt.dd), ¬st.tgt u) (hsav : ∀ (u : Wide.BlkIx dt.KIx A dt.dd), ¬st.sav u) (hval : ∀ (u : Wide.BlkIx dt.KIx A dt.dd), ¬st.val u) (hwk : ∀ (v : Wide.BlkIx dt.KIx A dt.dd), ¬st.wk ((dt.blkLaid h hpos hbase).cell v)) (hbot : ∀ (v : Wide.BlkIx dt.KIx A dt.dd), ¬st.bot ((dt.blkLaid h hpos hbase).cell v)) (hltp : ∀ (v : Wide.BlkIx dt.KIx A dt.dd), ¬st.ltp ((dt.blkLaid h hpos hbase).cell v)) (hold : ∀ (i : dt.d.B.ι) (v : Wide.BlkIx dt.KIx A dt.dd), ¬st.old i ((dt.blkLaid h hpos hbase).cell v)) (hnew : ∀ (i : dt.d.B.ι) (v : Wide.BlkIx dt.KIx A dt.dd), ¬st.new i ((dt.blkLaid h hpos hbase).cell v)) (b : Option dt.KIx) (f : dt.CtlIx → A) : dt.buildWr zero one coord b f = dt.ixBack (dt.blkLaid h hpos hbase).toLayout zero one hdd st ((dt.blkLaid h hpos hbase).cell (b, dt.ptrTup coord f))

The sweep's write is the file's background, at the register the pointer names: every mark is a fact about the register's block and named tuple, and every track is clear at the registers – the file is laid before anything is written to it, and what the marker does below them is no business of a register's mark.

The pointer's advance, and the specification it makes

noncomputable def DescriptiveComplexity.Draw.Data.ptrNext {L : FirstOrder.Language} (dt : Data L) {A : Type} [LinearOrder A] [Finite A] [Finite dt.KIx] (coord : Fin dt.dd → dt.CtlIx) (b : Option dt.KIx) (f : dt.CtlIx → A) : dt.CtlIx → A

The pointer's advance: the control with its coordinate slots holding the next register's tuple, every other slot left alone.

Equations

• dt.ptrNext coord b f q = if h : ∃ (j : Fin dt.dd), coord j = q then (DescriptiveComplexity.blkNext A dt.KIx dt.dd (b, dt.ptrTup coord f)).2 h.choose else f q

noncomputable def DescriptiveComplexity.Draw.Data.ctlOf {L : FirstOrder.Language} (dt : Data L) {A : Type} (coord : Fin dt.dd → dt.CtlIx) (f₀ : dt.CtlIx → A) (t : Fin dt.dd → A) : dt.CtlIx → A

The control holding a register's tuple: the given control with its coordinate slots carrying the tuple, and every other slot as it was. This is what the pointer is, and the sweep's advance moves it from one register's to the next's.

Equations

• dt.ctlOf coord f₀ t q = if h : ∃ (j : Fin dt.dd), coord j = q then t h.choose else f₀ q

theorem DescriptiveComplexity.Draw.Data.ptrTup_ctlOf {L : FirstOrder.Language} {dt : Data L} {A : Type} {coord : Fin dt.dd → dt.CtlIx} (hcoord : Function.Injective coord) (f₀ : dt.CtlIx → A) (t : Fin dt.dd → A) : dt.ptrTup coord (dt.ctlOf coord f₀ t) = t

The pointer reads back the tuple it was set to.

theorem DescriptiveComplexity.Draw.Data.ctlOf_ctlOf {L : FirstOrder.Language} {dt : Data L} {A : Type} (coord : Fin dt.dd → dt.CtlIx) (f₀ : dt.CtlIx → A) (t t' : Fin dt.dd → A) : dt.ctlOf coord (dt.ctlOf coord f₀ t') t = dt.ctlOf coord f₀ t

Setting the pointer forgets the pointer that was there: the coordinate slots are overwritten and every other slot rides along, so the exit's reset of the pointer to the file's first register lands exactly where the next sweep starts.

theorem DescriptiveComplexity.Draw.Data.ptrNext_ctlOf {L : FirstOrder.Language} {dt : Data L} {A : Type} [LinearOrder A] [Finite A] [Finite dt.KIx] {coord : Fin dt.dd → dt.CtlIx} (hcoord : Function.Injective coord) (f₀ : dt.CtlIx → A) (b : Option dt.KIx) (t : Fin dt.dd → A) : dt.ptrNext coord b (dt.ctlOf coord f₀ t) = dt.ctlOf coord f₀ (blkNext A dt.KIx dt.dd (b, t)).2

The advance carries the pointer from one register to the next: at a control holding a register's tuple, the advance holds the next register's.

noncomputable def DescriptiveComplexity.Draw.Data.nullSpec {L : FirstOrder.Language} (dt : Data L) {A : Type} (B : Type) : SweepSpec A dt.CtlIx dt.SlotIx B

The sweep that does nothing: it writes nothing, moves no pointer and is over at once. A program that is handed its file – the register channel of DescriptiveComplexity.WideRegAccept hands one over – has nothing to lay, and this is what it puts where a file-laying program puts DescriptiveComplexity.Draw.Data.buildSpec: the site's rules still exist, and the one that fires is the one whose guard is «rolled over and done», so the phase costs a single step.

Being trivial it is definable at once (uSweepSpecDef_nullSpec), and it needs no coordinate map – which is the point, a pointer wide enough to name a register being what no wide machine's control can hold (DescriptiveComplexity.Problems.Wide.Limits).

Equations

• One or more equations did not get rendered due to their size.

noncomputable def DescriptiveComplexity.Draw.Data.buildSpec {L : FirstOrder.Language} (dt : Data L) {A : Type} [LinearOrder A] [Finite A] [Nonempty A] [Finite dt.KIx] (zero one : A) (coord : Fin dt.dd → dt.CtlIx) : SweepSpec A dt.CtlIx dt.SlotIx (Option dt.KIx)

The file-laying sweep, specified: write the register's mark, advance the pointer, roll over at the last tuple of a block and stop at the last register of the file.

Equations

• One or more equations did not get rendered due to their size.

theorem DescriptiveComplexity.Draw.Data.blkNext_fst_of_roll {L : FirstOrder.Language} {dt : Data L} {A : Type} [LinearOrder A] [Finite A] [Nonempty A] [Finite dt.KIx] (zero one : A) (coord : Fin dt.dd → dt.CtlIx) {b : Option dt.KIx} {f : dt.CtlIx → A} (hroll : (dt.buildSpec zero one coord).Roll b f) : (blkNext A dt.KIx dt.dd (b, dt.ptrTup coord f)).1 = (dt.buildSpec zero one coord).nx b

A roll-over lands in the next block's first register, which is what DescriptiveComplexity.Draw.SweepSpec.nx being a function of the block alone buys: at the last tuple the advance's block is blkNextB of the current one.

What the guessing sweep writes

The guessing phase runs the same sweep over the same stretch with the background on both sides (DescriptiveComplexity.Draw.Prog.reachesIn_guessTracks): what changes at a cell is the stage tracks and nothing else, so the write is the cell it read with those tracks set to the guessed value, and the value is a shape – one rule per assignment of the tracks – which is the program's only nondeterminism.

noncomputable def DescriptiveComplexity.Draw.Data.guessWr {L : FirstOrder.Language} (dt : Data L) {A : Type} (zero one : A) (x : dt.d.B.ι → Bool) (g : dt.SlotIx → A) : dt.SlotIx → A

What the guessing sweep writes: the cell it read, with the stage tracks holding the guessed value.

Equations

• dt.guessWr zero one x g (DescriptiveComplexity.Draw.Slot.old i) = DescriptiveComplexity.Draw.bitVal zero one (x i = true)
• dt.guessWr zero one x g DescriptiveComplexity.Draw.Slot.reg = g DescriptiveComplexity.Draw.Slot.reg
• dt.guessWr zero one x g DescriptiveComplexity.Draw.Slot.regFirst = g DescriptiveComplexity.Draw.Slot.regFirst
• dt.guessWr zero one x g DescriptiveComplexity.Draw.Slot.regLast = g DescriptiveComplexity.Draw.Slot.regLast
• dt.guessWr zero one x g (DescriptiveComplexity.Draw.Slot.blk c) = g (DescriptiveComplexity.Draw.Slot.blk c)
• dt.guessWr zero one x g (DescriptiveComplexity.Draw.Slot.name j) = g (DescriptiveComplexity.Draw.Slot.name j)
• dt.guessWr zero one x g DescriptiveComplexity.Draw.Slot.pdd = g DescriptiveComplexity.Draw.Slot.pdd
• dt.guessWr zero one x g DescriptiveComplexity.Draw.Slot.mir = g DescriptiveComplexity.Draw.Slot.mir
• dt.guessWr zero one x g DescriptiveComplexity.Draw.Slot.tgt = g DescriptiveComplexity.Draw.Slot.tgt
• dt.guessWr zero one x g DescriptiveComplexity.Draw.Slot.sav = g DescriptiveComplexity.Draw.Slot.sav
• dt.guessWr zero one x g DescriptiveComplexity.Draw.Slot.val = g DescriptiveComplexity.Draw.Slot.val
• dt.guessWr zero one x g DescriptiveComplexity.Draw.Slot.wk = g DescriptiveComplexity.Draw.Slot.wk
• dt.guessWr zero one x g DescriptiveComplexity.Draw.Slot.bot = g DescriptiveComplexity.Draw.Slot.bot
• dt.guessWr zero one x g DescriptiveComplexity.Draw.Slot.ltp = g DescriptiveComplexity.Draw.Slot.ltp
• dt.guessWr zero one x g (DescriptiveComplexity.Draw.Slot.new i) = g (DescriptiveComplexity.Draw.Slot.new i)

theorem DescriptiveComplexity.Draw.Data.guessWr_eq_passTracks {L : FirstOrder.Language} {dt : Data L} {A R' P' Q : Type} [Fintype Q] [Fintype dt.SlotIx] [DecidableEq dt.SlotIx] {PR : Prog A R' P' Q dt.SlotIx dt.KIx dt.dd} {I : Type} {zero one : A} {hdd : dt.dd0 ≤ dt.dd} {lay : Layout dt A R' P' I} {st : TapeSt dt A R' P' I} (σ : dt.d.B.ι → (Univ A R' P' dt.KIx dt.dd → Prop) → Prop) {t : dt.SlotIx} (hne : ∀ (i : dt.d.B.ι), Slot.old i ≠ t) {m : I → Prop} {r : Univ A R' P' dt.KIx dt.dd → Prop} (x : dt.d.B.ι → Bool) (hx : ∀ (i : dt.d.B.ι), σ i r ↔ x i = true) : dt.guessWr zero one x (PR.passTracksAt lay.cell t (dt.ixBack lay zero one hdd st) m r) = PR.passTracksAt lay.cell t (dt.ixBack lay zero one hdd { 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 guess's write installs the guessed tracks: at the cell under the head, the background of the state with its stage tracks replaced – which is what the guessing run asks of the rule, and all it asks.

noncomputable def DescriptiveComplexity.Draw.Data.guessSpec {L : FirstOrder.Language} (dt : Data L) {A : Type} [LinearOrder A] [Finite A] [Nonempty A] [Finite dt.KIx] (zero one : A) (coord : Fin dt.dd → dt.CtlIx) : GuessSpec A dt.CtlIx dt.SlotIx (Option dt.KIx) (dt.d.B.ι → Bool)

The guessing sweep, specified: write the guessed stage tracks, advance the pointer, roll over and stop exactly where the file-laying sweep does – it is the same walk over the same registers, and only the write differs.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def DescriptiveComplexity.Draw.Data.regionSpec {L : FirstOrder.Language} (dt : Data L) {A : Type} (zero one : A) : GuessSpec A dt.CtlIx dt.SlotIx (Option dt.KIx) (dt.d.B.ι → Bool)

The region-wide guess, specified: the same write as the file's, and a pointer that never moves – a control holding dd₀ coordinates cannot count the region, so the walk carries no pointer at all. Every step is a roll-over that stays in its own block phase, which is the one arm of the guess site whose guard is then always true; the walk's end is the site's own stopping rule and not a test on the control.

Equations

• One or more equations did not get rendered due to their size.