The stage atom's machinery: a random access

The largest atom subroutine of the EXPSPACE program: to evaluate a stage atom R i' (w̄), the machine saves its mirror, builds the target address – one tuple loop per argument position, copying the source block of VAL or MIRROR into the target's block by named bits – resets to the bottom and seeks the target, reads the stage bit under the head, and comes back: restore the target from the save, reset, seek home.

The sites: two DescriptiveComplexity.Draw.CopyKit trips (save and restore), a DescriptiveComplexity.Draw.ClearKit trip (the target's blocks not written by any loop), the per-argument DescriptiveComplexity.Draw.tupleRule loops chained head to tail, two DescriptiveComplexity.Draw.ResetKit+ClearKit pairs with their erasing entry checkpoints, and two DescriptiveComplexity.Draw.SeekKit instances – the first's verdict exits are the read under the head, branching on the stage track's digit at the sought cell and storing it into the control.

As everywhere in the assembly, the semantic parameters – the loop-variable updates, the stored-bit updates, the verdict store – are dstSt/guard parameters; the shapes and their separation are what this file fixes.

The shapes

inductive DescriptiveComplexity.Draw.StagePh (k : ℕ) : Type

The phases of a stage atom's machinery.

• savP {k : ℕ} : TrackPh → StagePh k

  Saving the mirror.

• clrP {k : ℕ} : TrackPh → StagePh k

  Clearing the target.

• tupP {k : ℕ} : Fin k → ChainPh 3 TuplePS → StagePh k

  The ℓ-th argument's tuple loop.

• cR1 {k : ℕ} : StagePh k

  The checkpoint entering the first reset.

• rst1P {k : ℕ} : ResetPh → StagePh k

  The first reset.

• cm1P {k : ℕ} : TrackPh → StagePh k

  Clearing the mirror before the seek out.

• skP {k : ℕ} : SeekPh → StagePh k

  The seek to the target.

• resP {k : ℕ} : TrackPh → StagePh k

  Restoring the target from the save.

• cR2 {k : ℕ} : StagePh k

  The checkpoint entering the second reset.

• rst2P {k : ℕ} : ResetPh → StagePh k

  The second reset.

• cm2P {k : ℕ} : TrackPh → StagePh k

  Clearing the mirror before the seek home.

• sk2P {k : ℕ} : SeekPh → StagePh k

  The seek home.

inductive DescriptiveComplexity.Draw.StageSite (k : ℕ) : Type

The sites of a stage atom's machinery.

• sav {k : ℕ} : StageSite k

  The mirror save.

• clr {k : ℕ} : StageSite k

  The target clear.

• tup {k : ℕ} : Fin k → ChainSite 3 TupleSS → StageSite k

  An argument's tuple loop.

• cR1 {k : ℕ} : StageSite k

  The first reset's entry checkpoint.

• rst1 {k : ℕ} : StageSite k

  The first reset.

• cm1 {k : ℕ} : StageSite k

  The first mirror clear.

• sk {k : ℕ} : StageSite k

  The seek to the target.

• res {k : ℕ} : StageSite k

  The target restore.

• cR2 {k : ℕ} : StageSite k

  The second reset's entry checkpoint.

• rst2 {k : ℕ} : StageSite k

  The second reset.

• cm2 {k : ℕ} : StageSite k

  The second mirror clear.

• sk2 {k : ℕ} : StageSite k

  The seek home.

def DescriptiveComplexity.Draw.StageSh (k : ℕ) : StageSite k → Type

The rule shape of each site.

Equations

• DescriptiveComplexity.Draw.StageSh k DescriptiveComplexity.Draw.StageSite.sav = (DescriptiveComplexity.Draw.TrackRule ⊕ Unit)
• DescriptiveComplexity.Draw.StageSh k DescriptiveComplexity.Draw.StageSite.clr = (DescriptiveComplexity.Draw.TrackRule ⊕ Unit)
• DescriptiveComplexity.Draw.StageSh k (DescriptiveComplexity.Draw.StageSite.tup a c) = DescriptiveComplexity.Draw.ChainSh 3 DescriptiveComplexity.Draw.TupleSS DescriptiveComplexity.Draw.TupleSh c
• DescriptiveComplexity.Draw.StageSh k DescriptiveComplexity.Draw.StageSite.cR1 = DescriptiveComplexity.Draw.EvalChkRule
• DescriptiveComplexity.Draw.StageSh k DescriptiveComplexity.Draw.StageSite.rst1 = (DescriptiveComplexity.Draw.ResetRule ⊕ Unit)
• DescriptiveComplexity.Draw.StageSh k DescriptiveComplexity.Draw.StageSite.cm1 = (DescriptiveComplexity.Draw.TrackRule ⊕ Unit)
• DescriptiveComplexity.Draw.StageSh k DescriptiveComplexity.Draw.StageSite.sk = (DescriptiveComplexity.Draw.SeekRule ⊕ Bool)
• DescriptiveComplexity.Draw.StageSh k DescriptiveComplexity.Draw.StageSite.res = (DescriptiveComplexity.Draw.TrackRule ⊕ Unit)
• DescriptiveComplexity.Draw.StageSh k DescriptiveComplexity.Draw.StageSite.cR2 = DescriptiveComplexity.Draw.EvalChkRule
• DescriptiveComplexity.Draw.StageSh k DescriptiveComplexity.Draw.StageSite.rst2 = (DescriptiveComplexity.Draw.ResetRule ⊕ Unit)
• DescriptiveComplexity.Draw.StageSh k DescriptiveComplexity.Draw.StageSite.cm2 = (DescriptiveComplexity.Draw.TrackRule ⊕ Unit)
• DescriptiveComplexity.Draw.StageSh k DescriptiveComplexity.Draw.StageSite.sk2 = (DescriptiveComplexity.Draw.SeekRule ⊕ Unit)

def DescriptiveComplexity.Draw.stageOwn {k : ℕ} : StagePh k → StageSite k

The owner of each phase of a stage atom's machinery.

Equations

• DescriptiveComplexity.Draw.stageOwn (DescriptiveComplexity.Draw.StagePh.savP a) = DescriptiveComplexity.Draw.StageSite.sav
• DescriptiveComplexity.Draw.stageOwn (DescriptiveComplexity.Draw.StagePh.clrP a) = DescriptiveComplexity.Draw.StageSite.clr
• DescriptiveComplexity.Draw.stageOwn (DescriptiveComplexity.Draw.StagePh.tupP ℓ c) = DescriptiveComplexity.Draw.StageSite.tup ℓ (DescriptiveComplexity.Draw.tupleOwn c)
• DescriptiveComplexity.Draw.stageOwn DescriptiveComplexity.Draw.StagePh.cR1 = DescriptiveComplexity.Draw.StageSite.cR1
• DescriptiveComplexity.Draw.stageOwn (DescriptiveComplexity.Draw.StagePh.rst1P a) = DescriptiveComplexity.Draw.StageSite.rst1
• DescriptiveComplexity.Draw.stageOwn (DescriptiveComplexity.Draw.StagePh.cm1P a) = DescriptiveComplexity.Draw.StageSite.cm1
• DescriptiveComplexity.Draw.stageOwn (DescriptiveComplexity.Draw.StagePh.skP a) = DescriptiveComplexity.Draw.StageSite.sk
• DescriptiveComplexity.Draw.stageOwn (DescriptiveComplexity.Draw.StagePh.resP a) = DescriptiveComplexity.Draw.StageSite.res
• DescriptiveComplexity.Draw.stageOwn DescriptiveComplexity.Draw.StagePh.cR2 = DescriptiveComplexity.Draw.StageSite.cR2
• DescriptiveComplexity.Draw.stageOwn (DescriptiveComplexity.Draw.StagePh.rst2P a) = DescriptiveComplexity.Draw.StageSite.rst2
• DescriptiveComplexity.Draw.stageOwn (DescriptiveComplexity.Draw.StagePh.cm2P a) = DescriptiveComplexity.Draw.StageSite.cm2
• DescriptiveComplexity.Draw.stageOwn (DescriptiveComplexity.Draw.StagePh.sk2P a) = DescriptiveComplexity.Draw.StageSite.sk2

def DescriptiveComplexity.Draw.Data.stageFirstTup {P : Type} {k : ℕ} (emb : StagePh k → P) : P

The phase entering the loops, or the first reset checkpoint when there is no argument.

Equations

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

def DescriptiveComplexity.Draw.Data.stageNextTup {P : Type} {k : ℕ} (emb : StagePh k → P) (ℓ : Fin k) : P

The phase after the ℓ-th loop.

Equations

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

noncomputable def DescriptiveComplexity.Draw.Data.stageRule {L : FirstOrder.Language} (dt : Data L) {A Q P : Type} {k : ℕ} (zero one : A) (emb : StagePh k → P) (srcTrack : Fin k → dt.SlotIx) (srcBlk dstBlk : Fin k → Fin dt.ko ⊕ Fin dt.ki) (coord : Fin dt.dd0 → Q) (bitFlag : (Q → A) → Prop) (setBit : Bool → (Q → A) → (dt.SlotIx → A) → Q → A) (initLv advLv : (Q → A) → (dt.SlotIx → A) → Q → A) (IsMaxLv : (Q → A) → Prop) (oldSlot : dt.SlotIx) (setAv : Bool → (Q → A) → (dt.SlotIx → A) → Q → A) (exitPh : P) (i : StageSite k) : StageSh k i → Rule A Q dt.SlotIx P

The rules of a stage atom's machinery.

Equations

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

theorem DescriptiveComplexity.Draw.Data.stageRule_dstIn {L : FirstOrder.Language} (dt : Data L) {A Q P : Type} {k : ℕ} (zero one : A) {emb : StagePh k → P} (srcTrack : Fin k → dt.SlotIx) (srcBlk dstBlk : Fin k → Fin dt.ko ⊕ Fin dt.ki) (coord : Fin dt.dd0 → Q) (bitFlag : (Q → A) → Prop) (setBit : Bool → (Q → A) → (dt.SlotIx → A) → Q → A) (initLv advLv : (Q → A) → (dt.SlotIx → A) → Q → A) (IsMaxLv : (Q → A) → Prop) (oldSlot : dt.SlotIx) (setAv : Bool → (Q → A) → (dt.SlotIx → A) → Q → A) (exitPh : P) {S : P → Prop} (hemb : ∀ (p : StagePh k), S (emb p)) (hexit : S exitPh) (i : StageSite k) (ρ : StageSh k i) : S (dt.stageRule zero one emb srcTrack srcBlk dstBlk coord bitFlag setBit initLv advLv IsMaxLv oldSlot setAv exitPh i ρ).dstPh

A property of a stage atom's phases and its exit holds of every phase it can move to: the save, the clear, the tuple loops, the two resets, the two mirror clears and the two seeks all stay inside the machinery's own phases, and only the last seek's verdict leaves. This is what a determinism-after-the-guess argument asks of the random access (DescriptiveComplexity.Draw.Data.nexProg_uniqueFrom).

theorem DescriptiveComplexity.Draw.Data.stageHosrc {L : FirstOrder.Language} (dt : Data L) {A Q P : Type} {k : ℕ} (zero one : A) {emb : StagePh k → P} (srcTrack : Fin k → dt.SlotIx) (srcBlk dstBlk : Fin k → Fin dt.ko ⊕ Fin dt.ki) (coord : Fin dt.dd0 → Q) (bitFlag : (Q → A) → Prop) (setBit : Bool → (Q → A) → (dt.SlotIx → A) → Q → A) (initLv advLv : (Q → A) → (dt.SlotIx → A) → Q → A) (IsMaxLv : (Q → A) → Prop) (oldSlot : dt.SlotIx) (setAv : Bool → (Q → A) → (dt.SlotIx → A) → Q → A) (exitPh : P) (i : StageSite k) (ρ : StageSh k i) : ∃ (p : StagePh k), (dt.stageRule zero one emb srcTrack srcBlk dstBlk coord bitFlag setBit initLv advLv IsMaxLv oldSlot setAv exitPh i ρ).srcPh = emb p ∧ stageOwn p = i

Every rule of a stage atom's machinery fires from a phase its site owns; the tuple loops' obligation is their own.

theorem DescriptiveComplexity.Draw.Data.stageSep {L : FirstOrder.Language} (dt : Data L) {A Q P : Type} {k : ℕ} (zero one : A) {emb : StagePh k → P} (srcTrack : Fin k → dt.SlotIx) (srcBlk dstBlk : Fin k → Fin dt.ko ⊕ Fin dt.ki) (coord : Fin dt.dd0 → Q) (bitFlag : (Q → A) → Prop) (setBit : Bool → (Q → A) → (dt.SlotIx → A) → Q → A) (initLv advLv : (Q → A) → (dt.SlotIx → A) → Q → A) (IsMaxLv : (Q → A) → Prop) (oldSlot : dt.SlotIx) (setAv : Bool → (Q → A) → (dt.SlotIx → A) → Q → A) (exitPh : P) (hzo : zero ≠ one) (hemb : Function.Injective emb) (i : StageSite k) (ρ ρ' : StageSh k i) (f : Q → A) (g : dt.SlotIx → A) : (dt.stageRule zero one emb srcTrack srcBlk dstBlk coord bitFlag setBit initLv advLv IsMaxLv oldSlot setAv exitPh i ρ).guard f g → (dt.stageRule zero one emb srcTrack srcBlk dstBlk coord bitFlag setBit initLv advLv IsMaxLv oldSlot setAv exitPh i ρ').guard f g → (dt.stageRule zero one emb srcTrack srcBlk dstBlk coord bitFlag setBit initLv advLv IsMaxLv oldSlot setAv exitPh i ρ).srcPh = (dt.stageRule zero one emb srcTrack srcBlk dstBlk coord bitFlag setBit initLv advLv IsMaxLv oldSlot setAv exitPh i ρ').srcPh → ρ = ρ'

A stage atom's machinery separates in-shape.