The address a stage atom builds, at an arbitrary file

The random access of a stage atom copies each argument position's source block into the TARGET register and then seeks to the address TARGET spells. At the elementwise file that address is the register set, and the copy's two cells are elements of the universe (DescriptiveComplexity.Draw.Data.stageXS/stageXD). At a coarser file they are registers, named by a block and a tuple (DescriptiveComplexity.Draw.Layout.reg), what the copy builds is a mark, and the address is DescriptiveComplexity.ixAddr of it.

This file is that reading, from the data up to the run: the two named registers, the mark the loops build (ixStageTgt) with its closed form, the facts that place the address it stands for in the logical interval, the copy loop's run (ixStageTuple_reachesIn), the loops chained (ixStageChain_reachesIn) and the whole random access (ixStageAtom_reachesIn), each on the clock a NEXPTIME machine is held to. The hypothesis that carries everything across is one coherence condition on the file – the element a register holds the bit of is the element its name spells:

elt (F.toLayout.reg hhas b c) = dt.blkElt b (padTup zero c)

With it the address ixAddr elt (ixStageTgt …) has the same blocks as the elementwise one, so the semantics of the atom – the dictionary, trackOf, the logical interval – says of a clocked program's run exactly what it says of a space-bounded one.

The two registers a copy round names

noncomputable def DescriptiveComplexity.Draw.Data.ixStageXS {L : FirstOrder.Language} (dt : Data L) {A R P : Type} [LinearOrder A] [LinearOrder R] [LinearOrder P] [FirstOrder.Language.wide.Structure (Univ A R P dt.KIx dt.dd)] {I : Type} (F : LaidFile dt A R P I) {zero : A} (hhas : F.toLayout.HasName zero) (vi : dt.VarIx) {iv : dt.d.B.ι} (ts : Fin (dt.d.B.arity iv) → Fin (dt.nOf vi)) (ℓ : Fin (dt.d.B.arity iv)) (b : Lex (Fin dt.dd0 → A)) : I

The source register of a copy round: the register named by the round's tuple in the position's source block.

Equations

• dt.ixStageXS F hhas vi ts ℓ b = F.toLayout.reg hhas (dt.lvBlk vi (ts ℓ)) (ofLex b)

noncomputable def DescriptiveComplexity.Draw.Data.ixStageXD {L : FirstOrder.Language} (dt : Data L) {A R P : Type} [LinearOrder A] [LinearOrder R] [LinearOrder P] [FirstOrder.Language.wide.Structure (Univ A R P dt.KIx dt.dd)] {I : Type} (F : LaidFile dt A R P I) {zero : A} (hhas : F.toLayout.HasName zero) {iv : dt.d.B.ι} (ℓ : Fin (dt.d.B.arity iv)) (b : Lex (Fin dt.dd0 → A)) : I

The destination register of a copy round: the register named by the round's tuple in the TARGET block of the position.

Equations

• dt.ixStageXD F hhas ℓ b = F.toLayout.reg hhas (Sum.inl (Fin.castLE ⋯ ℓ)) (ofLex b)

theorem DescriptiveComplexity.Draw.Data.ixStageXD_injective {L : FirstOrder.Language} (dt : Data L) {A R P : Type} [LinearOrder A] [LinearOrder R] [LinearOrder P] [FirstOrder.Language.wide.Structure (Univ A R P dt.KIx dt.dd)] {I : Type} (F : LaidFile dt A R P I) {zero : A} (hhas : F.toLayout.HasName zero) {iv : dt.d.B.ι} {ℓ : Fin (dt.d.B.arity iv)} {b b' : Lex (Fin dt.dd0 → A)} (h : dt.ixStageXD F hhas ℓ b = dt.ixStageXD F hhas ℓ b') : b = b'

Distinct tuples name distinct registers: a register carries its own name, and the name determines the tuple.

theorem DescriptiveComplexity.Draw.Data.ixStageXD_pos_eq {L : FirstOrder.Language} (dt : Data L) {A R P : Type} [LinearOrder A] [LinearOrder R] [LinearOrder P] [FirstOrder.Language.wide.Structure (Univ A R P dt.KIx dt.dd)] {I : Type} (F : LaidFile dt A R P I) {zero : A} (hhas : F.toLayout.HasName zero) {iv : dt.d.B.ι} {ℓ ℓ' : Fin (dt.d.B.arity iv)} {b b' : Lex (Fin dt.dd0 → A)} (h : dt.ixStageXD F hhas ℓ b = dt.ixStageXD F hhas ℓ' b') : ℓ = ℓ'

Distinct positions write distinct blocks: a register carries its block, and the block names the position that wrote it.

The mark the copy loops build

noncomputable def DescriptiveComplexity.Draw.Data.ixStageTgt {L : FirstOrder.Language} (dt : Data L) {A R P : Type} [LinearOrder A] [LinearOrder R] [LinearOrder P] [FirstOrder.Language.wide.Structure (Univ A R P dt.KIx dt.dd)] [Finite A] [Nonempty A] {I : Type} (F : LaidFile dt A R P I) {zero : A} (hhas : F.toLayout.HasName zero) (vi : dt.VarIx) {iv : dt.d.B.ι} (ts : Fin (dt.d.B.arity iv) → Fin (dt.nOf vi)) (st : TapeSt dt A R P I) : ℕ → I → Prop

The TARGET after the first n copy loops: each position's loop writes its source bits at its destination registers over what the earlier positions built.

Equations

• One or more equations did not get rendered due to their size.
• dt.ixStageTgt F hhas vi ts st 0 = fun (x : I) => False

theorem DescriptiveComplexity.Draw.Data.ixStageTgt_iff {L : FirstOrder.Language} (dt : Data L) {A R P : Type} [LinearOrder A] [LinearOrder R] [LinearOrder P] [FirstOrder.Language.wide.Structure (Univ A R P dt.KIx dt.dd)] [Finite A] [Nonempty A] {I : Type} (F : LaidFile dt A R P I) {zero : A} (hhas : F.toLayout.HasName zero) (vi : dt.VarIx) {iv : dt.d.B.ι} (ts : Fin (dt.d.B.arity iv) → Fin (dt.nOf vi)) (st : TapeSt dt A R P I) (n : ℕ) (y : I) : dt.ixStageTgt F hhas vi ts st n y ↔ ∃ (ℓ : Fin (dt.d.B.arity iv)) (b : Lex (Fin dt.dd0 → A)), ↑ℓ < n ∧ y = dt.ixStageXD F hhas ℓ b ∧ dt.lvSet st vi (ts ℓ) (dt.ixStageXS F hhas vi ts ℓ b)

The composed TARGET, in closed form: a register holds a bit exactly when some position below n copied it there – the source block's bit at the same tuple. Distinct positions write distinct blocks, so the loops never collide and the disjunction is honest.

The copy loop at an arbitrary file

The loop's background, its generated controls and its run, all as the elementwise instantiation has them – the only difference being that the two cells it names are registers and the marks are the index's.

noncomputable def DescriptiveComplexity.Draw.Data.ixStageRestF {L : FirstOrder.Language} (dt : Data L) {A R P : Type} [LinearOrder A] [LinearOrder R] [LinearOrder P] [FirstOrder.Language.wide.Structure (Univ A R P dt.KIx dt.dd)] {I : Type} (F : LaidFile dt A R P I) (zero one : A) (st : TapeSt dt A R P I) (m' : I → Prop) : (Univ A R P dt.KIx dt.dd → Prop) → dt.SlotIx → A

The background of a copy loop, as a function of the destination content: the state with the TARGET register at the given track.

Equations

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

theorem DescriptiveComplexity.Draw.Data.ixStageRestF_off {L : FirstOrder.Language} (dt : Data L) {A R P : Type} [LinearOrder A] [LinearOrder R] [LinearOrder P] [FirstOrder.Language.wide.Structure (Univ A R P dt.KIx dt.dd)] {I : Type} (F : LaidFile dt A R P I) (zero one : A) (st : TapeSt dt A R P I) (m₁ m₂ : I → Prop) (r : Univ A R P dt.KIx dt.dd → Prop) (s : dt.SlotIx) (hs : s ≠ Slot.tgt) : dt.ixStageRestF F zero one st m₁ r s = dt.ixStageRestF F zero one st m₂ r s

The destination-dependent background moves only at the TARGET slot.

theorem DescriptiveComplexity.Draw.Data.ixReadLv_stageIter0 {L : FirstOrder.Language} (dt : Data L) {A R P : Type} [LinearOrder A] [LinearOrder R] [LinearOrder P] [FirstOrder.Language.wide.Structure (Univ A R P dt.KIx dt.dd)] [Finite A] [Nonempty A] {I : Type} (F : LaidFile dt A R P I) {zero : A} (hhas : F.toLayout.HasName zero) (vi : dt.VarIx) {iv : dt.d.B.ι} (ts : Fin (dt.d.B.arity iv) → Fin (dt.nOf vi)) (one : A) (av : Fin dt.natMax) (ℓ : Fin (dt.d.B.arity iv)) (st : TapeSt dt A R P I) {vAdr : Univ A R P dt.KIx dt.dd → Prop} {mD₀ : I → Prop} {f₀ : dt.CtlIx → A} (b : Lex (Fin dt.dd0 → A)) : dt.readLv (tupleIter0 (dt.stageArgs zero one vi iv ts av).setBit (dt.stageArgs zero one vi iv ts av).initLv (dt.stageArgs zero one vi iv ts av).advLv (dt.lvSet st vi (ts ℓ)) vAdr (dt.ixStageRestF F zero one st) (dt.ixStageXS F hhas vi ts ℓ) (dt.ixStageXD F hhas ℓ) mD₀ f₀ b) = ofLex b

The copy loop's generated round tuples: the pre-store control's loop element is the round's tuple.

theorem DescriptiveComplexity.Draw.Data.ixReadLv_stageIter1 {L : FirstOrder.Language} (dt : Data L) {A R P : Type} [LinearOrder A] [LinearOrder R] [LinearOrder P] [FirstOrder.Language.wide.Structure (Univ A R P dt.KIx dt.dd)] [Finite A] [Nonempty A] {I : Type} (F : LaidFile dt A R P I) {zero : A} (hhas : F.toLayout.HasName zero) (vi : dt.VarIx) {iv : dt.d.B.ι} (ts : Fin (dt.d.B.arity iv) → Fin (dt.nOf vi)) (one : A) (av : Fin dt.natMax) (ℓ : Fin (dt.d.B.arity iv)) (st : TapeSt dt A R P I) {vAdr : Univ A R P dt.KIx dt.dd → Prop} {mD₀ : I → Prop} {f₀ : dt.CtlIx → A} (b : Lex (Fin dt.dd0 → A)) : dt.readLv (tupleIter1 (dt.stageArgs zero one vi iv ts av).setBit (dt.stageArgs zero one vi iv ts av).initLv (dt.stageArgs zero one vi iv ts av).advLv (dt.lvSet st vi (ts ℓ)) vAdr (dt.ixStageRestF F zero one st) (dt.ixStageXS F hhas vi ts ℓ) (dt.ixStageXD F hhas ℓ) mD₀ f₀ b) = ofLex b

The post-store control's loop element is still the round's tuple.

theorem DescriptiveComplexity.Draw.Data.ixStageTuple_reachesIn {L : FirstOrder.Language} (dt : Data L) {A R P : Type} [LinearOrder A] [LinearOrder R] [LinearOrder P] [FirstOrder.Language.wide.Structure (Univ A R P dt.KIx dt.dd)] [Finite A] [Finite R] [Finite P] [Nonempty A] {I : Type} (F : LaidFile dt A R P I) (vi : dt.VarIx) {iv : dt.d.B.ι} (ts : Fin (dt.d.B.arity iv) → Fin (dt.nOf vi)) [Fintype dt.SlotIx] [Finite dt.KIx] {PR : Prog A R P dt.CtlIx dt.SlotIx dt.KIx dt.dd} (av : Fin dt.natMax) (ℓ : Fin (dt.d.B.arity iv)) (st : TapeSt dt A R P I) (hix : IsLinOrd F.le) {mD₀ : I → Prop} {f₀ : dt.CtlIx → A} {emb : ChainPh 3 TuplePS → P} {exitPh : P} {rEmb : (i : ChainSite 3 TupleSS) → ChainSh 3 TupleSS TupleSh i → R} (hhasP : F.toLayout.HasName PR.zero) (hsepP : F.toLayout.NameSep PR.zero ⋯) (hrules : ∀ (i : ChainSite 3 TupleSS) (ρ : ChainSh 3 TupleSS TupleSh i), PR.rules (rEmb i ρ) = tupleRule PR.zero PR.one Slot.wk Slot.reg emb ((dt.stageArgs PR.zero PR.one vi iv ts av).srcTrack ℓ) Slot.tgt (dt.nameG PR.one ((dt.stageArgs PR.zero PR.one vi iv ts av).srcBlk ℓ) dt.lvC) (dt.nameG PR.one ((dt.stageArgs PR.zero PR.one vi iv ts av).dstBlk ℓ) dt.lvC) (dt.stageArgs PR.zero PR.one vi iv ts av).bitFlag (dt.stageArgs PR.zero PR.one vi iv ts av).setBit (dt.stageArgs PR.zero PR.one vi iv ts av).initLv (dt.stageArgs PR.zero PR.one vi iv ts av).advLv (dt.stageArgs PR.zero PR.one vi iv ts av).IsMaxLv exitPh i ρ) (hR : PR.table.Reads) (hlin : IsLinOrd WMLe) {gbot : I} (hbot : ∀ (y : I), F.le gbot y) {v v' : Univ A R P dt.KIx dt.dd → Prop} (hv : WMSetLt WMLe v (F.cell gbot)) (hvi : WMIncr WMLe v v') (hwkSt : st.wk = fun (r : Univ A R P dt.KIx dt.dd → Prop) => r = v) (w : ℕ) (hcost : ∀ (a : Lex (Fin dt.dd0 → A)), 2 * (wideRank (F.cell (dt.ixStageXS F hhasP vi ts ℓ a)) - wideRank v) + 2 ≤ w ∧ 2 * (wideRank (F.cell (dt.ixStageXD F hhasP ℓ a)) - wideRank v) + 2 ≤ w) : (wideData (Univ A R P dt.KIx dt.dd)).ReachesIn ((2 * w + 8) * (Nat.card (Lex (Fin dt.dd0 → A)) + 1) + 1) { state := Sum.inr (PR.stElt (emb (ChainPh.chk ⟨0, ⋯⟩)) f₀), head := Sum.inl v, tape := wideTape (PR.trackTapeAt F.cell ((dt.stageArgs PR.zero PR.one vi iv ts av).srcTrack ℓ) (dt.ixStageRestF F PR.zero PR.one st (tupleIterD (dt.lvSet st vi (ts ℓ)) (dt.ixStageXS F hhasP vi ts ℓ) (dt.ixStageXD F hhasP ℓ) mD₀ (toLex botTup))) (dt.lvSet st vi (ts ℓ))) (PR.syElt PR.blank) } { state := Sum.inr (PR.stElt exitPh (tupleIter1 (dt.stageArgs PR.zero PR.one vi iv ts av).setBit (dt.stageArgs PR.zero PR.one vi iv ts av).initLv (dt.stageArgs PR.zero PR.one vi iv ts av).advLv (dt.lvSet st vi (ts ℓ)) v (dt.ixStageRestF F PR.zero PR.one st) (dt.ixStageXS F hhasP vi ts ℓ) (dt.ixStageXD F hhasP ℓ) mD₀ f₀ (toLex topTup))), head := Sum.inl v', tape := wideTape (PR.trackTapeAt F.cell Slot.tgt (dt.ixStageRestF F PR.zero PR.one st (tupleIterD (dt.lvSet st vi (ts ℓ)) (dt.ixStageXS F hhasP vi ts ℓ) (dt.ixStageXD F hhasP ℓ) mD₀ (toLex topTup))) (tuplePost (dt.lvSet st vi (ts ℓ)) (tupleIterD (dt.lvSet st vi (ts ℓ)) (dt.ixStageXS F hhasP vi ts ℓ) (dt.ixStageXD F hhasP ℓ) mD₀) (dt.ixStageXS F hhasP vi ts ℓ) (dt.ixStageXD F hhasP ℓ) (toLex topTup))) (PR.syElt PR.blank) }

One copy loop's run, on a clock: from its entry checkpoint at the marker to the exit phase one cell to its right, the TARGET block of the position holding the source block's bits at every tuple's cell, a round's width paid once per tuple.

noncomputable def DescriptiveComplexity.Draw.Data.ixStageFAt {L : FirstOrder.Language} (dt : Data L) {A R P : Type} [LinearOrder A] [LinearOrder R] [LinearOrder P] [FirstOrder.Language.wide.Structure (Univ A R P dt.KIx dt.dd)] [Finite A] [Nonempty A] {I : Type} (F : LaidFile dt A R P I) {zero : A} (hhas : F.toLayout.HasName zero) (one : A) (vi : dt.VarIx) {iv : dt.d.B.ι} (ts : Fin (dt.d.B.arity iv) → Fin (dt.nOf vi)) (av : Fin dt.natMax) (st : TapeSt dt A R P I) (elt : I → Univ A R P dt.KIx dt.dd) (v : Univ A R P dt.KIx dt.dd → Prop) (f₀ : dt.CtlIx → A) : ℕ → dt.CtlIx → A

The control after the first n copy loops.

Equations

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

theorem DescriptiveComplexity.Draw.Data.ixStageChain_reachesIn {L : FirstOrder.Language} (dt : Data L) {A R P : Type} [LinearOrder A] [LinearOrder R] [LinearOrder P] [FirstOrder.Language.wide.Structure (Univ A R P dt.KIx dt.dd)] [Finite A] [Finite R] [Finite P] [Nonempty A] {I : Type} (F : LaidFile dt A R P I) (vi : dt.VarIx) {iv : dt.d.B.ι} (ts : Fin (dt.d.B.arity iv) → Fin (dt.nOf vi)) [Fintype dt.SlotIx] {PR : Prog A R P dt.CtlIx dt.SlotIx dt.KIx dt.dd} (hix : IsLinOrd F.le) (hhasP : F.toLayout.HasName PR.zero) (hsepP : F.toLayout.NameSep PR.zero ⋯) {elt : I → Univ A R P dt.KIx dt.dd} (av : Fin dt.natMax) (st : TapeSt dt A R P I) {v : Univ A R P dt.KIx dt.dd → Prop} {emb : StagePh (dt.d.B.arity iv) → P} {exitPh : P} {rEmb : (i : StageSite (dt.d.B.arity iv)) → StageSh (dt.d.B.arity iv) i → R} [Finite dt.KIx] (hrules : ∀ (i : StageSite (dt.d.B.arity iv)) (ρ : StageSh (dt.d.B.arity iv) i), PR.rules (rEmb i ρ) = dt.stageRule PR.zero PR.one emb (dt.stageArgs PR.zero PR.one vi iv ts av).srcTrack (dt.stageArgs PR.zero PR.one vi iv ts av).srcBlk (dt.stageArgs PR.zero PR.one vi iv ts av).dstBlk (dt.stageArgs PR.zero PR.one vi iv ts av).coord (dt.stageArgs PR.zero PR.one vi iv ts av).bitFlag (dt.stageArgs PR.zero PR.one vi iv ts av).setBit (dt.stageArgs PR.zero PR.one vi iv ts av).initLv (dt.stageArgs PR.zero PR.one vi iv ts av).advLv (dt.stageArgs PR.zero PR.one vi iv ts av).IsMaxLv (dt.stageArgs PR.zero PR.one vi iv ts av).oldSlot (dt.stageArgs PR.zero PR.one vi iv ts av).setAv exitPh i ρ) (hR : PR.table.Reads) (hlin : IsLinOrd WMLe) {gbot : I} (hbot : ∀ (y : I), F.le gbot y) {v' : Univ A R P dt.KIx dt.dd → Prop} (hv : WMSetLt WMLe v (F.cell gbot)) (hvi : WMIncr WMLe v v') (hwkSt : st.wk = fun (r : Univ A R P dt.KIx dt.dd → Prop) => r = v) (hmirSt : st.mir = ixMark elt v) (f₀ : dt.CtlIx → A) (w : ℕ) (hcost : ∀ (ℓ : Fin (dt.d.B.arity iv)) (a : Lex (Fin dt.dd0 → A)), 2 * (wideRank (F.cell (dt.ixStageXS F hhasP vi ts ℓ a)) - wideRank v) + 2 ≤ w ∧ 2 * (wideRank (F.cell (dt.ixStageXD F hhasP ℓ a)) - wideRank v) + 2 ≤ w) : (wideData (Univ A R P dt.KIx dt.dd)).ReachesIn (((2 * w + 8) * (Nat.card (Lex (Fin dt.dd0 → A)) + 1) + 1 + 1) * dt.d.B.arity iv) { state := Sum.inr (PR.stElt (stageFirstTup emb) ((dt.stageArgs PR.zero PR.one vi iv ts av).initLv f₀ (dt.ixBack F.toLayout PR.zero PR.one ⋯ { mir := st.mir, tgt := fun (x : I) => False, sav := ixMark elt v, val := st.val, old := st.old, new := st.new, wk := st.wk, bot := st.bot, ltp := st.ltp } v))), head := Sum.inl v', tape := wideTape (PR.trackTapeAt F.cell Slot.mir (dt.ixBack F.toLayout PR.zero PR.one ⋯ { mir := st.mir, tgt := fun (x : I) => False, sav := ixMark elt v, val := st.val, old := st.old, new := st.new, wk := st.wk, bot := st.bot, ltp := st.ltp }) (ixMark elt v)) (PR.syElt PR.blank) } { state := Sum.inr (PR.stElt (emb StagePh.cR1) (dt.ixStageFAt F hhasP PR.one vi ts av st elt v f₀ (dt.d.B.arity iv))), head := Sum.inl v', tape := wideTape (PR.trackTapeAt F.cell Slot.mir (dt.ixBack F.toLayout PR.zero PR.one ⋯ { mir := st.mir, tgt := dt.ixStageTgt F hhasP vi ts { mir := st.mir, tgt := st.tgt, sav := ixMark elt v, val := st.val, old := st.old, new := st.new, wk := st.wk, bot := st.bot, ltp := st.ltp } (dt.d.B.arity iv), sav := ixMark elt v, val := st.val, old := st.old, new := st.new, wk := st.wk, bot := st.bot, ltp := st.ltp }) (ixMark elt v)) (PR.syElt PR.blank) }

The copy loops of a stage atom, chained and instantiated, on a clock: from the phase entering the first loop to the first reset's checkpoint, the TARGET holding the composed content of every position – exactly the hLoopsIn leg of DescriptiveComplexity.Draw.Data.stage_reachesIn, at one loop and one walk-back per position.

Where the address sits

theorem DescriptiveComplexity.Draw.Data.ixStageTgt_arg {L : FirstOrder.Language} (dt : Data L) {A R P : Type} [LinearOrder A] [LinearOrder R] [LinearOrder P] [FirstOrder.Language.wide.Structure (Univ A R P dt.KIx dt.dd)] [Finite A] [Nonempty A] {I : Type} (F : LaidFile dt A R P I) {zero : A} (hhas : F.toLayout.HasName zero) (vi : dt.VarIx) {iv : dt.d.B.ι} (ts : Fin (dt.d.B.arity iv) → Fin (dt.nOf vi)) {elt : I → Univ A R P dt.KIx dt.dd} (helt : ∀ (b : Fin dt.ko ⊕ Fin dt.ki) (c : Fin dt.dd0 → A), elt (F.toLayout.reg hhas b c) = dt.blkElt b (pad zero c)) (st : TapeSt dt A R P I) (n : ℕ) {u : I} (hy : dt.ixStageTgt F hhas vi ts st n u) : ∃ (i : dt.KIx), (elt u).1 = Tag.arg i

The target of a random access is an address of argument cells alone: every register it holds was written by a copy round, at that round's destination – in an argument block – over the empty mark.

theorem DescriptiveComplexity.Draw.Data.ixStageTgt_isPad {L : FirstOrder.Language} (dt : Data L) {A R P : Type} [LinearOrder A] [LinearOrder R] [LinearOrder P] [FirstOrder.Language.wide.Structure (Univ A R P dt.KIx dt.dd)] [Finite A] [Nonempty A] {I : Type} (F : LaidFile dt A R P I) {zero : A} (hhas : F.toLayout.HasName zero) (vi : dt.VarIx) {iv : dt.d.B.ι} (ts : Fin (dt.d.B.arity iv) → Fin (dt.nOf vi)) {elt : I → Univ A R P dt.KIx dt.dd} (helt : ∀ (b : Fin dt.ko ⊕ Fin dt.ki) (c : Fin dt.dd0 → A), elt (F.toLayout.reg hhas b c) = dt.blkElt b (pad zero c)) (st : TapeSt dt A R P I) (n : ℕ) {u : I} (hy : dt.ixStageTgt F hhas vi ts st n u) : IsPad dt.dd0 zero (elt u).2

The target of a random access is padded: every register it holds is a destination register, and those carry the round's tuple in the name slots and zero beyond them.

theorem DescriptiveComplexity.Draw.Data.wmSetLt_ixStageTgt_logicalTop {L : FirstOrder.Language} (dt : Data L) {A R P : Type} [LinearOrder A] [LinearOrder R] [LinearOrder P] [FirstOrder.Language.wide.Structure (Univ A R P dt.KIx dt.dd)] [Finite A] [Finite R] [Finite P] [Nonempty A] {I : Type} (F : LaidFile dt A R P I) {zero : A} (hhas : F.toLayout.HasName zero) (vi : dt.VarIx) {iv : dt.d.B.ι} (ts : Fin (dt.d.B.arity iv) → Fin (dt.nOf vi)) {elt : I → Univ A R P dt.KIx dt.dd} (helt : ∀ (b : Fin dt.ko ⊕ Fin dt.ki) (c : Fin dt.dd0 → A), elt (F.toLayout.reg hhas b c) = dt.blkElt b (pad zero c)) {one : A} (hne : zero ≠ one) (hV : IsLinOrd tupLeLex) (hd : dt.dd0 < dt.dd) (i : dt.KIx) (st : TapeSt dt A R P I) (n : ℕ) : WMSetLt (lexRel (fun (x1 x2 : Tag R P dt.KIx) => x1 ≤ x2) tupLeLex) (ixAddr elt (dt.ixStageTgt F hhas vi ts st n)) logicalTop

The address a stage atom reads lies in the logical interval: it is built from padded destination registers in argument blocks alone, which is wmSetLt_logicalTop_of_isPad's hypothesis.

The stage atom's run at an arbitrary file

The random access, end to end: the save, the clear, the copy loops of ixStageChain_reachesIn, the reset–clear–seek out to the address the marks stand for, the read under the head, the restore and the seek home. Everything below it is DescriptiveComplexity.Draw.Data.stage_run, which takes the file as a parameter; what this adds is the instantiation – the built target, and the two facts that put it in the working area.

theorem DescriptiveComplexity.Draw.Data.ixStageAtom_reachesIn {L : FirstOrder.Language} (dt : Data L) {A R P : Type} [LinearOrder A] [LinearOrder R] [LinearOrder P] [FirstOrder.Language.wide.Structure (Univ A R P dt.KIx dt.dd)] [Finite A] [Finite R] [Finite P] [Nonempty A] {I : Type} (F : LaidFile dt A R P I) (vi : dt.VarIx) {iv : dt.d.B.ι} (ts : Fin (dt.d.B.arity iv) → Fin (dt.nOf vi)) [Fintype dt.SlotIx] [Finite dt.KIx] [Finite I] {PR : Prog A R P dt.CtlIx dt.SlotIx dt.KIx dt.dd} (av : Fin dt.natMax) (st : TapeSt dt A R P I) (hix : IsLinOrd F.le) (hhasP : F.toLayout.HasName PR.zero) (hsepP : F.toLayout.NameSep PR.zero ⋯) {elt : I → Univ A R P dt.KIx dt.dd} {Use : I → Prop} (hinj : Function.Injective elt) (hmono : ∀ (u u' : I), WMLt F.le u u' ↔ WMLt WMLe (elt u) (elt u')) (hup : ∀ (u : I) (x : Univ A R P dt.KIx dt.dd), Use u → WMLt WMLe (elt u) x → ∃ (u' : I), Use u' ∧ elt u' = x) (heltP : ∀ (b : Fin dt.ko ⊕ Fin dt.ki) (c : Fin dt.dd0 → A), elt (F.toLayout.reg hhasP b c) = dt.blkElt b (pad PR.zero c)) {emb : StagePh (dt.d.B.arity iv) → P} {exitPh : P} {rEmb : (i : StageSite (dt.d.B.arity iv)) → StageSh (dt.d.B.arity iv) i → R} (hrules : ∀ (i : StageSite (dt.d.B.arity iv)) (ρ : StageSh (dt.d.B.arity iv) i), PR.rules (rEmb i ρ) = dt.stageRule PR.zero PR.one emb (dt.stageArgs PR.zero PR.one vi iv ts av).srcTrack (dt.stageArgs PR.zero PR.one vi iv ts av).srcBlk (dt.stageArgs PR.zero PR.one vi iv ts av).dstBlk (dt.stageArgs PR.zero PR.one vi iv ts av).coord (dt.stageArgs PR.zero PR.one vi iv ts av).bitFlag (dt.stageArgs PR.zero PR.one vi iv ts av).setBit (dt.stageArgs PR.zero PR.one vi iv ts av).initLv (dt.stageArgs PR.zero PR.one vi iv ts av).advLv (dt.stageArgs PR.zero PR.one vi iv ts av).IsMaxLv (dt.stageArgs PR.zero PR.one vi iv ts av).oldSlot (dt.stageArgs PR.zero PR.one vi iv ts av).setAv exitPh i ρ) (hR : PR.table.Reads) (hlin : IsLinOrd WMLe) {gtop gbot : I} (htop : ∀ (y : I), F.le y gtop) (hbot : ∀ (y : I), F.le gbot y) {e₀ : Univ A R P dt.KIx dt.dd} (he₀ : ∀ (y : Univ A R P dt.KIx dt.dd), WMLe e₀ y) (hord : ∀ (x y : Univ A R P dt.KIx dt.dd), WMLe x y ↔ tagTupleLe x y) (hwork : ∀ {r : Univ A R P dt.KIx dt.dd → Prop}, (∀ (x : Univ A R P dt.KIx dt.dd), r x → ∃ (i : dt.KIx), x.1 = Tag.arg i) → ∀ (u : I), WMSetLt WMLe r (F.cell u)) {v v' : Univ A R P dt.KIx dt.dd → Prop} (hv : WMSetLt WMLe v (F.cell gbot)) (hvi : WMIncr WMLe v v') (hwkSt : st.wk = fun (r : Univ A R P dt.KIx dt.dd → Prop) => r = v) (hmirSt : st.mir = ixMark elt v) (hbotSt : st.bot = fun (r : Univ A R P dt.KIx dt.dd → Prop) => r = fun (x : Univ A R P dt.KIx dt.dd) => False) (hvh : IxHolds elt Use v) (hxdUse : ∀ (ℓ : Fin (dt.d.B.arity iv)) (b : Lex (Fin dt.dd0 → A)), Use (dt.ixStageXD F hhasP ℓ b)) (f₀ : dt.CtlIx → A) (b : Bool) (w wG wP wR wK : ℕ) (hcost : ∀ (ℓ : Fin (dt.d.B.arity iv)) (a : Lex (Fin dt.dd0 → A)), 2 * (wideRank (F.cell (dt.ixStageXS F hhasP vi ts ℓ a)) - wideRank v) + 2 ≤ w ∧ 2 * (wideRank (F.cell (dt.ixStageXD F hhasP ℓ a)) - wideRank v) + 2 ≤ w) (hgap : ∀ (u u' : I), IxSucc F.le u u' → wideRank (F.cell u') - wideRank (F.cell u) ≤ wG) (hwP : wideRank (F.cell gtop) + 2 + ((ixRank F.le gtop - ixRank F.le gbot) * wG + 1) + wideRank (F.cell gbot) ≤ wP) (hwR : ∀ (s : Univ A R P dt.KIx dt.dd → Prop), WMSetLt WMLe s (F.cell gbot) → wideRank s + 4 ≤ wR) (hwK : ∀ (T : Univ A R P dt.KIx dt.dd → Prop), WMSetLt WMLe T (F.cell gbot) → wideRank T * (1 + (wideRank (F.cell gtop) + 3 + (ixRank F.le gtop - ixRank F.le gbot) * wG + wideRank (F.cell gbot)) + (wideRank (F.cell gtop) + ((ixRank F.le gtop - ixRank F.le gbot) * wG + 1) + wideRank (F.cell gbot) + 4)) + 1 + (wideRank (F.cell gtop) + 3 + (ixRank F.le gtop - ixRank F.le gbot) * wG + wideRank (F.cell gbot)) ≤ wK) (hb : st.old iv (ixAddr elt (dt.ixStageTgt F hhasP vi ts { mir := st.mir, tgt := st.tgt, sav := ixMark elt v, val := st.val, old := st.old, new := st.new, wk := st.wk, bot := st.bot, ltp := st.ltp } (dt.d.B.arity iv))) ↔ b = true) : (wideData (Univ A R P dt.KIx dt.dd)).ReachesIn (5 * wP + 2 * wR + 2 * wK + ((2 * w + 8) * (Nat.card (Lex (Fin dt.dd0 → A)) + 1) + 1 + 1) * dt.d.B.arity iv + 13) { state := Sum.inr (PR.stElt (emb (StagePh.savP TrackPh.up)) f₀), head := Sum.inl v', tape := wideTape (PR.trackTapeAt F.cell Slot.mir (dt.ixBack F.toLayout PR.zero PR.one ⋯ st) st.mir) (PR.syElt PR.blank) } { state := Sum.inr (PR.stElt exitPh ((dt.stageArgs PR.zero PR.one vi iv ts av).setAv b (dt.ixStageFAt F hhasP PR.one vi ts av st elt v f₀ (dt.d.B.arity iv)) (dt.ixBack F.toLayout PR.zero PR.one ⋯ (dt.ixStageAtSt st elt v (ixAddr elt (dt.ixStageTgt F hhasP vi ts { mir := st.mir, tgt := st.tgt, sav := ixMark elt v, val := st.val, old := st.old, new := st.new, wk := st.wk, bot := st.bot, ltp := st.ltp } (dt.d.B.arity iv)))) (ixAddr elt (dt.ixStageTgt F hhasP vi ts { mir := st.mir, tgt := st.tgt, sav := ixMark elt v, val := st.val, old := st.old, new := st.new, wk := st.wk, bot := st.bot, ltp := st.ltp } (dt.d.B.arity iv)))))), head := Sum.inl v', tape := wideTape (PR.trackTapeAt F.cell Slot.mir (dt.ixBack F.toLayout PR.zero PR.one ⋯ (dt.ixStageEndSt st elt v)) (dt.ixStageEndSt st elt v).mir) (PR.syElt PR.blank) }

The stage atom's run at an arbitrary file, on a clock: from its entry phase to the exit phase, the verdict – the old track's bit at the address the built TARGET stands for – stored in the atom's control slot, the marker, mirror and save restored at the home address. The cost is the atom's nine trips and thirteen dispatches over the copy loops' own.

The address the marks stand for, block by block

The one place the file's naming and the encoding have to agree, and the reason they can: with the coherence hypothesis, the address a clocked program's TARGET spells has the same blocks as the address a space-bounded one builds, so every statement of the semantics about that address – the dictionary, trackOf, the logical interval – holds of the clocked run with no restatement.

Blindness to the two scratch registers

theorem DescriptiveComplexity.Draw.Data.ixStageTgt_congr_scratch {L : FirstOrder.Language} (dt : Data L) {A R P : Type} [LinearOrder A] [LinearOrder R] [LinearOrder P] [FirstOrder.Language.wide.Structure (Univ A R P dt.KIx dt.dd)] [Finite A] [Nonempty A] {I : Type} (F : LaidFile dt A R P I) {zero : A} (hhas : F.toLayout.HasName zero) (vi : dt.VarIx) {iv : dt.d.B.ι} (ts : Fin (dt.d.B.arity iv) → Fin (dt.nOf vi)) {elt : I → Univ A R P dt.KIx dt.dd} {st : TapeSt dt A R P I} {v : Univ A R P dt.KIx dt.dd → Prop} {st' : TapeSt dt A R P I} (h : dt.ScratchEq st st') (n : ℕ) : dt.ixStageTgt F hhas vi ts { mir := st.mir, tgt := st.tgt, sav := ixMark elt v, val := st.val, old := st.old, new := st.new, wk := st.wk, bot := st.bot, ltp := st.ltp } n = dt.ixStageTgt F hhas vi ts { mir := st'.mir, tgt := st'.tgt, sav := ixMark elt v, val := st'.val, old := st'.old, new := st'.new, wk := st'.wk, bot := st'.bot, ltp := st'.ltp } n

The TARGET a random access builds is blind to the two scratch registers, at an arbitrary file: every copy round reads a level's register set, and the loop pins SAV at the home address itself.

theorem DescriptiveComplexity.Draw.Data.ixStageFAt_congr_scratch {L : FirstOrder.Language} (dt : Data L) {A R P : Type} [LinearOrder A] [LinearOrder R] [LinearOrder P] [FirstOrder.Language.wide.Structure (Univ A R P dt.KIx dt.dd)] [Finite A] [Nonempty A] {I : Type} (F : LaidFile dt A R P I) {zero : A} (hhas : F.toLayout.HasName zero) (vi : dt.VarIx) {iv : dt.d.B.ι} (ts : Fin (dt.d.B.arity iv) → Fin (dt.nOf vi)) (one : A) (av : Fin dt.natMax) {elt : I → Univ A R P dt.KIx dt.dd} {st : TapeSt dt A R P I} {v : Univ A R P dt.KIx dt.dd → Prop} {st' : TapeSt dt A R P I} (h : dt.ScratchEq st st') (hreg : ¬∃ (u : I), v = F.cell u) (f₀ : dt.CtlIx → A) (n : ℕ) : dt.ixStageFAt F hhas one vi ts av st elt v f₀ n = dt.ixStageFAt F hhas one vi ts av st' elt v f₀ n

The control of the copy loops is blind to them too, at an arbitrary file: the destination-dependent background overwrites TARGET, and the loop reads it at the home cell alone.