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)

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

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.

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.

Where the address sits

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