The stage atom's run #

The run theorem of DescriptiveComplexity.Draw.Data.stageRule – the random access. The tuple loops stay abstract (one hypothesis for the whole chain, discharged by DescriptiveComplexity.Draw.tuple_run at instantiation); this file contributes the itinerary around them: save the mirror, clear the target, run the loops, reset, clear the mirror, seek the target, read the stage bit under the head, restore the target, and come home the same way.

The statement is in the DescriptiveComplexity.Draw.TapeSt idiom: the machine's mutable state is a record, each leg one update, and every slot equation a kit asks for is definitional in DescriptiveComplexity.Draw.Data.ixBack; the handoff between legs walking different tracks is DescriptiveComplexity.Draw.Data.trackTape_back_gen.

The file is a parameter. A clocked program has no register per element, so the run is stated at an arbitrary DescriptiveComplexity.Draw.LaidFile with the address correspondence of DescriptiveComplexity.Problems.Wide.IxAddr: what the mirror, the save and the target hold are the marks of their addresses (DescriptiveComplexity.ixMark), and the seek's verdict is again an equality of addresses because the correspondence carries the order. The elementwise file is that at the identity (DescriptiveComplexity.Draw.Data.diagLaid), which is what stageAtSt, stageEndSt and trackTape_back_gen_diag are.

source

noncomputable def DescriptiveComplexity.Draw.Data.ixStageAtSt {L : FirstOrder.Language} (dt : Data L) {A R P I : Type} (st : TapeSt dt A R P I) (elt : I → Univ A R P dt.KIx dt.dd) (v mT : Univ A R P dt.KIx dt.dd → Prop) :

TapeSt dt A R P I

The state at the far end of the random access: marker and mirror on the target, the mirror's address saved, the target built.

Equations

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

Instances For

Dependency graph

source

noncomputable def DescriptiveComplexity.Draw.Data.ixStageEndSt {L : FirstOrder.Language} (dt : Data L) {A R P I : Type} (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) :

TapeSt dt A R P I

The state the random access returns in: the target and the save both holding the home address, everything else as at entry.

Equations

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

Instances For

Dependency graph

source

theorem DescriptiveComplexity.Draw.Data.trackTape_back_gen {L : FirstOrder.Language} (dt : Data L) {A R P Q : Type} [Fintype Q] [Fintype dt.SlotIx] [LinearOrder A] [LinearOrder R] [LinearOrder P] [FirstOrder.Language.wide.Structure (Univ A R P dt.KIx dt.dd)] {PR : Prog A R P Q dt.SlotIx dt.KIx dt.dd} {I : Type} (F : LaidFile dt A R P I) {stA stB : TapeSt dt A R P I} {t : dt.SlotIx} {m : I → Prop} (hagree : ∀ (r : Univ A R P dt.KIx dt.dd → Prop) (s : dt.SlotIx), s ≠ t → dt.ixBack F.toLayout PR.zero PR.one ⋯ stA r s = dt.ixBack F.toLayout PR.zero PR.one ⋯ stB r s) (ht : ∀ (r : Univ A R P dt.KIx dt.dd → Prop), dt.ixBack F.toLayout PR.zero PR.one ⋯ stB r t = bitVal PR.zero PR.one (bitAtOf F.cell m r)) :

PR.trackTapeAt F.cell t (dt.ixBack F.toLayout PR.zero PR.one ⋯ stA) m = fun (r : Univ A R P dt.KIx dt.dd → Prop) => PR.syElt (dt.ixBack F.toLayout PR.zero PR.one ⋯ stB r)

A leg's after-tape, read against the state it produced: the walked track moves into the new state's background, whose other slots agree with the old one's. The generic sibling of the concrete DescriptiveComplexity.Draw.Data.trackTape_back.

Dependency graph

source

theorem DescriptiveComplexity.Draw.Data.stage_run {L : FirstOrder.Language} (dt : Data L) {A R P Q : Type} {k : ℕ} [Fintype Q] [Fintype dt.SlotIx] [LinearOrder A] [LinearOrder R] [LinearOrder P] [FirstOrder.Language.wide.Structure (Univ A R P dt.KIx dt.dd)] [Finite A] [Finite R] [Finite P] {PR : Prog A R P Q dt.SlotIx dt.KIx dt.dd} {I : Type} [Finite I] (F : LaidFile dt A R P I) {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) {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} {rEmb : (i : StageSite k) → StageSh k i → R} (hrules : ∀ (i : StageSite k) (ρ : StageSh k i), PR.rules (rEmb i ρ) = dt.stageRule PR.zero PR.one emb srcTrack srcBlk dstBlk coord bitFlag setBit initLv advLv IsMaxLv oldSlot setAv exitPh i ρ) (hR : PR.table.Reads) (hlin : IsLinOrd WMLe) (hix : IsLinOrd F.le) {gtop gbot : I} (htop : ∀ (y : I), F.le y gtop) (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') {st : TapeSt dt A R P I} (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) {mT : Univ A R P dt.KIx dt.dd → Prop} (hTh : IxHolds elt Use mT) (hvh : IxHolds elt Use v) (hT : WMSetLt WMLe mT (F.cell gbot)) {T' : Univ A R P dt.KIx dt.dd → Prop} (hTi : WMIncr WMLe mT T') {f₀ fL : Q → A} (hLoops : Relation.ReflTransGen (wideData (Univ A R P dt.KIx dt.dd)).Step { state := Sum.inr (PR.stElt (stageFirstTup emb) (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) fL), head := Sum.inl v', tape := wideTape (PR.trackTapeAt F.cell Slot.mir (dt.ixBack F.toLayout PR.zero PR.one ⋯ { mir := st.mir, tgt := ixMark elt mT, 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) }) {b : Bool} (hbT : dt.ixBack F.toLayout PR.zero PR.one ⋯ (dt.ixStageAtSt st elt v mT) mT oldSlot = PR.one ↔ b = true) (holdmir : oldSlot ≠ Slot.mir) :

Relation.ReflTransGen (wideData (Univ A R P dt.KIx dt.dd)).Step { 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 (setAv b fL (dt.ixBack F.toLayout PR.zero PR.one ⋯ (dt.ixStageAtSt st elt v mT) mT))), 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, the budget forgotten: what a space-bounded caller reads. The width of a trip is then the largest of the finitely many the atom takes.

Dependency graph

The chain of the copy loops #

The k tuple loops run head to tail – position ℓ's exit is DescriptiveComplexity.Draw.Data.stageNextTup emb ℓ – so their chain is one induction over the positions, each round an abstract per-position run (discharged by the copy loop's instantiation) between the walk-backs this file's rules provide.

source

theorem DescriptiveComplexity.Draw.Data.stage_loops_run {L : FirstOrder.Language} (dt : Data L) {A R P Q : Type} {k : ℕ} [Fintype Q] [Fintype dt.SlotIx] [LinearOrder A] [LinearOrder R] [LinearOrder P] [FirstOrder.Language.wide.Structure (Univ A R P dt.KIx dt.dd)] [Finite A] [Finite R] [Finite P] {PR : Prog A R P Q dt.SlotIx dt.KIx dt.dd} {I : Type} (F : LaidFile dt A R P I) {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} {rEmb : (i : StageSite k) → StageSh k i → R} (hrules : ∀ (i : StageSite k) (ρ : StageSh k i), PR.rules (rEmb i ρ) = dt.stageRule PR.zero PR.one emb srcTrack srcBlk dstBlk coord bitFlag setBit initLv advLv IsMaxLv oldSlot setAv exitPh i ρ) (hR : PR.table.Reads) (hlin : IsLinOrd WMLe) {v v' : Univ A R P dt.KIx dt.dd → Prop} (hvi : WMIncr WMLe v v') (trkOf : Fin (k + 1) → dt.SlotIx) (restOf : Fin (k + 1) → (Univ A R P dt.KIx dt.dd → Prop) → dt.SlotIx → A) (mOf : Fin (k + 1) → I → Prop) (hwkOf : ∀ (ℓ : Fin (k + 1)) (r : Univ A R P dt.KIx dt.dd → Prop), restOf ℓ r Slot.wk = bitVal PR.zero PR.one (r = v)) (hwkTrk : ∀ (ℓ : Fin (k + 1)), Slot.wk ≠ trkOf ℓ) (fAt : Fin (k + 1) → Q → A) (hLoop : ∀ (ℓ : Fin k), Relation.ReflTransGen (wideData (Univ A R P dt.KIx dt.dd)).Step { state := Sum.inr (PR.stElt (emb (StagePh.tupP ℓ (ChainPh.chk ⟨0, _proof_88✝⟩))) (fAt ℓ.castSucc)), head := Sum.inl v, tape := wideTape (PR.trackTapeAt F.cell (trkOf ℓ.castSucc) (restOf ℓ.castSucc) (mOf ℓ.castSucc)) (PR.syElt PR.blank) } { state := Sum.inr (PR.stElt (stageNextTup emb ℓ) (fAt ℓ.succ)), head := Sum.inl v', tape := wideTape (PR.trackTapeAt F.cell (trkOf ℓ.succ) (restOf ℓ.succ) (mOf ℓ.succ)) (PR.syElt PR.blank) }) :

Relation.ReflTransGen (wideData (Univ A R P dt.KIx dt.dd)).Step { state := Sum.inr (PR.stElt (stageFirstTup emb) (fAt 0)), head := Sum.inl v', tape := wideTape (PR.trackTapeAt F.cell (trkOf 0) (restOf 0) (mOf 0)) (PR.syElt PR.blank) } { state := Sum.inr (PR.stElt (emb StagePh.cR1) (fAt (Fin.last k))), head := Sum.inl v', tape := wideTape (PR.trackTapeAt F.cell (trkOf (Fin.last k)) (restOf (Fin.last k)) (mOf (Fin.last k))) (PR.syElt PR.blank) }

The copy loops, chained, the budget forgotten: from the phase entering the first loop – one cell to the marker's right, as every dispatch leaves it – to the first reset's checkpoint, each position's run handed to the next by its own walk-back.

Dependency graph

The elementwise instantiation #

The space-bounded program's file is the input channel's ruler, one register per element: the runs above are that file at the identity embedding, and these are the statements their callers had before the file became a parameter.

source