What a rule may not write

A forward run constructs the tape it walks: every lemma says the machine reaches a configuration whose tape is a named function of a named tape state, so nothing has to be said about what the rules leave alone. A backward reading is handed an arbitrary run and has to recognize the tape, and there the missing fact bites: a configuration's tape is of the form DescriptiveComplexity.Draw.Data.ixBack of some tape state only because no rule ever writes the slots the channel wrote – the register flag, the two ends, the block one-hots, the name coordinates and the padding flag.

This file states that (Rule.KeepsFile) and proves it of the shapes a rule's write can take: no write at all, an update of a slot that is not one of those, and the guess's own write. With them the outer layer's rules keep the file, which is what an opening's reading needs.

A run as a sequence

The slots the channel writes

def DescriptiveComplexity.Draw.Slot.IsFile {ι : Type} {ko ki dd0 : ℕ} : Slot ι ko ki dd0 → Prop

A slot of the register file: what the channel writes at time zero and no rule may touch – the register flag, the file's two ends, the block one-hots, the name coordinates and the padding flag. Everything else is a track: scratch the program owns.

Equations

• DescriptiveComplexity.Draw.Slot.reg.IsFile = True
• DescriptiveComplexity.Draw.Slot.regFirst.IsFile = True
• DescriptiveComplexity.Draw.Slot.regLast.IsFile = True
• (DescriptiveComplexity.Draw.Slot.blk a).IsFile = True
• (DescriptiveComplexity.Draw.Slot.name a).IsFile = True
• DescriptiveComplexity.Draw.Slot.pdd.IsFile = True
• x✝.IsFile = False

@[simp]

theorem DescriptiveComplexity.Draw.Slot.not_isFile_mir {ι : Type} {ko ki dd0 : ℕ} : ¬mir.IsFile

@[simp]

theorem DescriptiveComplexity.Draw.Slot.not_isFile_tgt {ι : Type} {ko ki dd0 : ℕ} : ¬tgt.IsFile

@[simp]

theorem DescriptiveComplexity.Draw.Slot.not_isFile_sav {ι : Type} {ko ki dd0 : ℕ} : ¬sav.IsFile

@[simp]

theorem DescriptiveComplexity.Draw.Slot.not_isFile_val {ι : Type} {ko ki dd0 : ℕ} : ¬val.IsFile

@[simp]

theorem DescriptiveComplexity.Draw.Slot.not_isFile_wk {ι : Type} {ko ki dd0 : ℕ} : ¬wk.IsFile

@[simp]

theorem DescriptiveComplexity.Draw.Slot.not_isFile_bot {ι : Type} {ko ki dd0 : ℕ} : ¬bot.IsFile

@[simp]

theorem DescriptiveComplexity.Draw.Slot.not_isFile_ltp {ι : Type} {ko ki dd0 : ℕ} : ¬ltp.IsFile

@[simp]

theorem DescriptiveComplexity.Draw.Slot.not_isFile_old {ι : Type} {ko ki dd0 : ℕ} (i : ι) : ¬(old i).IsFile

@[simp]

theorem DescriptiveComplexity.Draw.Slot.not_isFile_new {ι : Type} {ko ki dd0 : ℕ} (i : ι) : ¬(new i).IsFile

Rules that keep the file

The shapes the outer layer writes with

Reading a tape back as a tape state

structure DescriptiveComplexity.Draw.Data.TapeShape {L : FirstOrder.Language} {dt : Data L} {A R' P' I : Type} (lay : Layout dt A R' P' I) (zero one : A) (st₀ : TapeSt dt A R' P' I) (rest : (Univ A R' P' dt.KIx dt.dd → Prop) → dt.SlotIx → A) : Prop

A tape the reading recognizes: every cell carries a slot vector, the file's slots are the layout's, the four addressed tracks are clear, and every other track is a bit.

• file (r : Univ A R' P' dt.KIx dt.dd → Prop) (s : Slot dt.d.B.ι dt.ko dt.ki dt.dd0) : s.IsFile → rest r s = dt.ixBack lay zero one ⋯ st₀ r s

  The file's slots are the layout's.

• cells (r : Univ A R' P' dt.KIx dt.dd → Prop) (s : Slot dt.d.B.ι dt.ko dt.ki dt.dd0) : s = Slot.mir ∨ s = Slot.tgt ∨ s = Slot.sav ∨ s = Slot.val → rest r s = zero

  The four tracks read at a register are clear.

• bits (r : Univ A R' P' dt.KIx dt.dd → Prop) (s : Slot dt.d.B.ι dt.ko dt.ki dt.dd0) : ¬s.IsFile → rest r s = zero ∨ rest r s = one

  Every other track is a bit.

One step of the machine, seen from the tape

The reading, along a run