The stage atoms, instantiated: the copy loops

The second semantic instantiation: the tuple loops of a stage atom's machinery, at the pack DescriptiveComplexity.Draw.Data.stageArgs. Each argument position runs one copy loop – a read at the source block's cell, the bit through the control's copy flag, a write at the TARGET block's cell – and this file proves its three invariants and its run:

• DescriptiveComplexity.Draw.Data.readLv_stageIter0/_stageIter1 – the loop element is the round's tuple, before and after the store;
• DescriptiveComplexity.Draw.Data.stageIterD_iff – the closed form of the destination track: a cell holds a bit exactly when some round already wrote it – the round's source bit – or it held one from the start and no round has touched it;
• DescriptiveComplexity.Draw.Data.stageTuple_run – the copy loop's run at the generated families, by DescriptiveComplexity.Draw.tuple_run_iter with the name guards discharged through DescriptiveComplexity.Draw.Data.nameG_iff.

The chaining of the k loops and the whole stage atom's run assemble on top, with DescriptiveComplexity.Draw.Data.stage_run.

noncomputable def DescriptiveComplexity.Draw.Data.stageXS {L : FirstOrder.Language} (dt : Data L) {A R P : Type} (zero : A) (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)) : Univ A R P dt.KIx dt.dd

The source cell of a copy round: the padded cell of the round's tuple in the position's source block.

Equations

• dt.stageXS zero vi iv ts ℓ b = dt.blkElt (dt.lvBlk vi (ts ℓ)) (DescriptiveComplexity.Draw.pad zero (ofLex b))

noncomputable def DescriptiveComplexity.Draw.Data.stageXD {L : FirstOrder.Language} (dt : Data L) {A R P : Type} (zero : A) (iv : dt.d.B.ι) (ℓ : Fin (dt.d.B.arity iv)) (b : Lex (Fin dt.dd0 → A)) : Univ A R P dt.KIx dt.dd

The destination cell of a copy round: the padded cell of the round's tuple in the TARGET block of the position.

Equations

• dt.stageXD zero iv ℓ b = dt.blkElt (Sum.inl (Fin.castLE ⋯ ℓ)) (DescriptiveComplexity.Draw.pad zero (ofLex b))

noncomputable def DescriptiveComplexity.Draw.Data.stageRestF {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)] (RF : RegFile (Univ A R P dt.KIx dt.dd)) (zero one : A) (st : TapeStD dt A R P) (m' : Univ A R P dt.KIx dt.dd → 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.

The loop element through the copy's operations

theorem DescriptiveComplexity.Draw.Data.readLv_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] (RF : RegFile (Univ A R P dt.KIx dt.dd)) [Nonempty A] {vi : dt.VarIx} {iv : dt.d.B.ι} {ts : Fin (dt.d.B.arity iv) → Fin (dt.nOf vi)} {av : Fin dt.natMax} {ℓ : Fin (dt.d.B.arity iv)} {st : TapeStD dt A R P} {vAdr mD₀ : Univ A R P dt.KIx dt.dd → Prop} {f₀ : dt.CtlIx → A} {zero one : 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.stageRestF RF zero one st) (dt.stageXS zero vi iv ts ℓ) (dt.stageXD zero iv ℓ) mD₀ f₀ b) = ofLex b

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

The built TARGET, in closed form

theorem DescriptiveComplexity.Draw.Data.stageIterD_iff {L : FirstOrder.Language} {dt : Data L} {A R P : Type} [LinearOrder A] [Finite A] {vi : dt.VarIx} {iv : dt.d.B.ι} {ts : Fin (dt.d.B.arity iv) → Fin (dt.nOf vi)} {ℓ : Fin (dt.d.B.arity iv)} {st : TapeStD dt A R P} {mD₀ : Univ A R P dt.KIx dt.dd → Prop} {zero : A} (b : Lex (Fin dt.dd0 → A)) (y : Univ A R P dt.KIx dt.dd) : tupleIterD (dt.lvSet st vi (ts ℓ)) (dt.stageXS zero vi iv ts ℓ) (dt.stageXD zero iv ℓ) mD₀ b y ↔ (∃ u < b, y = dt.stageXD zero iv ℓ u ∧ dt.lvSet st vi (ts ℓ) (dt.stageXS zero vi iv ts ℓ u)) ∨ (∀ u < b, y ≠ dt.stageXD zero iv ℓ u) ∧ mD₀ y

The built TARGET block, in closed form: a cell of the copy loop's destination holds a bit exactly when it is the destination cell of some tuple whose source bit is set – the loop having visited every tuple – or it held one from the start, off the loop's cells.

The copy loop's run

theorem DescriptiveComplexity.Draw.Data.stageTuple_run {L : FirstOrder.Language} {dt : Data L} {A R P : Type} [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 dt.CtlIx dt.SlotIx dt.KIx dt.dd} (RF : RegFile (Univ A R P dt.KIx dt.dd)) (hord : ∀ (x y : Univ A R P dt.KIx dt.dd), WMLe x y ↔ tagTupleLe x y) [Nonempty A] {vi : dt.VarIx} {iv : dt.d.B.ι} {ts : Fin (dt.d.B.arity iv) → Fin (dt.nOf vi)} {av : Fin dt.natMax} {ℓ : Fin (dt.d.B.arity iv)} {st : TapeStD dt A R P} {emb : ChainPh 3 TuplePS → P} {exitPh : P} {rEmb : (i : ChainSite 3 TupleSS) → ChainSh 3 TupleSS TupleSh i → R} [Finite dt.KIx] (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 : Univ A R P dt.KIx dt.dd} (hbot : ∀ (y : Univ A R P dt.KIx dt.dd), WMLe gbot y) {v v' : Univ A R P dt.KIx dt.dd → Prop} (hv : WMSetLt WMLe v (RF.cell gbot)) (hvi : WMIncr WMLe v v') (hwkSt : st.wk = fun (r : Univ A R P dt.KIx dt.dd → Prop) => r = v) (mD₀ : Univ A R P dt.KIx dt.dd → Prop) (f₀ : dt.CtlIx → A) : Relation.ReflTransGen (wideData (Univ A R P dt.KIx dt.dd)).Step { state := Sum.inr (PR.stElt (emb (ChainPh.chk ⟨0, stageTuple_run._proof_2⟩)) f₀), head := Sum.inl v, tape := wideTape (PR.trackTapeAt RF.cell ((dt.stageArgs PR.zero PR.one vi iv ts av).srcTrack ℓ) (dt.stageRestF RF PR.zero PR.one st (tupleIterD (dt.lvSet st vi (ts ℓ)) (dt.stageXS PR.zero vi iv ts ℓ) (dt.stageXD PR.zero iv ℓ) 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.stageRestF RF PR.zero PR.one st) (dt.stageXS PR.zero vi iv ts ℓ) (dt.stageXD PR.zero iv ℓ) mD₀ f₀ (toLex topTup))), head := Sum.inl v', tape := wideTape (PR.trackTapeAt RF.cell Slot.tgt (dt.stageRestF RF PR.zero PR.one st (tupleIterD (dt.lvSet st vi (ts ℓ)) (dt.stageXS PR.zero vi iv ts ℓ) (dt.stageXD PR.zero iv ℓ) mD₀ (toLex topTup))) (tuplePost (dt.lvSet st vi (ts ℓ)) (tupleIterD (dt.lvSet st vi (ts ℓ)) (dt.stageXS PR.zero vi iv ts ℓ) (dt.stageXD PR.zero iv ℓ) mD₀) (dt.stageXS PR.zero vi iv ts ℓ) (dt.stageXD PR.zero iv ℓ) (toLex topTup))) (PR.syElt PR.blank) }

One copy loop's run: 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.

The copy loops, chained: the TARGET built position by position

Position ℓ's loop copies its source block over what the earlier positions built. The composed content and the control each thread through by one recursion, DescriptiveComplexity.Draw.Data.stage_loops_run chains the runs – every handover a backed-track equality – and DescriptiveComplexity.Draw.Data.stage_run closes the whole random access over the chain.

noncomputable def DescriptiveComplexity.Draw.Data.stageTgtD {L : FirstOrder.Language} (dt : Data L) {A R P : Type} [LinearOrder A] [Finite A] [Nonempty A] (zero : A) (vi : dt.VarIx) (iv : dt.d.B.ι) (ts : Fin (dt.d.B.arity iv) → Fin (dt.nOf vi)) (st : TapeStD dt A R P) (v : Univ A R P dt.KIx dt.dd → Prop) : ℕ → Univ A R P dt.KIx dt.dd → Prop

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

Equations

• One or more equations did not get rendered due to their size.
• dt.stageTgtD zero vi iv ts st v 0 = fun (x : DescriptiveComplexity.Draw.Univ A R P dt.KIx dt.dd) => False

theorem DescriptiveComplexity.Draw.Data.wmSetLt_stageTgtD_logicalTop {L : FirstOrder.Language} {dt : Data L} {A R P : Type} [LinearOrder A] [LinearOrder R] [LinearOrder P] [Finite A] [Finite R] [Finite P] [Nonempty A] {zero one : A} {vi : dt.VarIx} {iv : dt.d.B.ι} {ts : Fin (dt.d.B.arity iv) → Fin (dt.nOf vi)} {st : TapeStD dt A R P} {v : Univ A R P dt.KIx dt.dd → Prop} (hne : zero ≠ one) (hV : IsLinOrd tupLeLex) (hd : dt.dd0 < dt.dd) (i : dt.KIx) (n : ℕ) : WMSetLt (lexRel (fun (x1 x2 : Tag R P dt.KIx) => x1 ≤ x2) tupLeLex) (dt.stageTgtD zero vi iv ts st v n) logicalTop

The address a stage atom reads lies in the logical interval: it is built from padded destination cells in argument blocks alone (stageTgtD_arg, stageTgtD_isPad), which is exactly wmSetLt_logicalTop_of_isPad. This is the hbelow the dictionary invariant of DescriptiveComplexity.Draw.Data.stageSt_old is owed: the invariant is an equivalence over the interval and nowhere else, so an address that is read has to be shown to lie there.

noncomputable def DescriptiveComplexity.Draw.Data.stageFAt {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] (RF : RegFile (Univ A R P dt.KIx dt.dd)) [Nonempty A] (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 : TapeStD dt A R P) (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.