The tuple loop: copying a block bit by bit

The stage atoms of the EXPSPACE program build their TARGET register by copying a block of VAL or MIRROR into a block of TARGET, one bit per named cell: a loop over the tuples the control enumerates in its loop-variable slots, each round a read trip at the source cell, a write trip at the destination cell, and an advance-or-exit dispatch.

This is the first client of the chain combinator (DescriptiveComplexity.Problems.Wide.DrawChain): three checkpoints around two stages – a DescriptiveComplexity.Draw.ReadKit whose verdict exits store the bit into the control, and a DescriptiveComplexity.Draw.WriteKit whose written bit reads it back – with the loop's back edge a plain descriptor (the combinator's dispatches may target any phase). The loop-variable updates (initLv, advLv) and the exhaustion guard (IsMaxLv) stay parameters: their content – the lexicographic enumeration, tied to DescriptiveComplexity.Draw.reflTransGen_of_tupLoop – is fixed with the runs.

The shapes

@[reducible, inline]

abbrev DescriptiveComplexity.Draw.TuplePS : Type

The stage phases of a tuple loop: the read trip's and the write trip's.

Equations

• DescriptiveComplexity.Draw.TuplePS = (DescriptiveComplexity.Draw.ReadPh ⊕ DescriptiveComplexity.Draw.WritePh)

@[reducible, inline]

abbrev DescriptiveComplexity.Draw.TupleSS : Type

The stage sites: false the read trip, true the write trip.

Equations

• DescriptiveComplexity.Draw.TupleSS = Bool

def DescriptiveComplexity.Draw.TupleSh : TupleSS → Type

The stage shapes: each kit's rules with its verdict exits.

Equations

• DescriptiveComplexity.Draw.TupleSh false = (DescriptiveComplexity.Draw.ReadRule ⊕ Bool)
• DescriptiveComplexity.Draw.TupleSh true = (DescriptiveComplexity.Draw.WriteRule ⊕ Unit)

def DescriptiveComplexity.Draw.tupleOwn : ChainPh 3 TuplePS → ChainSite 3 TupleSS

The owner of each phase of a tuple loop.

Equations

• DescriptiveComplexity.Draw.tupleOwn (DescriptiveComplexity.Draw.ChainPh.chk k) = DescriptiveComplexity.Draw.ChainSite.chk k
• DescriptiveComplexity.Draw.tupleOwn (DescriptiveComplexity.Draw.ChainPh.sub (Sum.inl val)) = DescriptiveComplexity.Draw.ChainSite.sub false
• DescriptiveComplexity.Draw.tupleOwn (DescriptiveComplexity.Draw.ChainPh.sub (Sum.inr val)) = DescriptiveComplexity.Draw.ChainSite.sub true

noncomputable def DescriptiveComplexity.Draw.tupleStageRule {A Q W P : Type} [DecidableEq W] (zero one : A) (wk rg : W) (emb : ChainPh 3 TuplePS → P) (tSrc tDst : W) (MatchS MatchD : (Q → A) → (W → A) → Prop) (bitFlag : (Q → A) → Prop) (setBit : Bool → (Q → A) → (W → A) → Q → A) (s : TupleSS) : TupleSh s → Rule A Q W P

The stage rules: the read kit with its bit-storing verdict exits, the write kit with its return exit.

Equations

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

def DescriptiveComplexity.Draw.tupleDsp {A Q W P : Type} (one : A) (wk rg : W) (emb : ChainPh 3 TuplePS → P) (initLv advLv : (Q → A) → (W → A) → Q → A) (IsMaxLv : (Q → A) → Prop) (exitPh : P) : Fin 3 → Bool → PreRule A Q W P

The dispatch descriptors: begin the first round (initializing the loop variables), hand the stored bit to the write trip, and advance or leave.

Equations

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

noncomputable def DescriptiveComplexity.Draw.tupleRule {A Q W P : Type} [DecidableEq W] (zero one : A) (wk rg : W) (emb : ChainPh 3 TuplePS → P) (tSrc tDst : W) (MatchS MatchD : (Q → A) → (W → A) → Prop) (bitFlag : (Q → A) → Prop) (setBit : Bool → (Q → A) → (W → A) → Q → A) (initLv advLv : (Q → A) → (W → A) → Q → A) (IsMaxLv : (Q → A) → Prop) (exitPh : P) (i : ChainSite 3 TupleSS) : ChainSh 3 TupleSS TupleSh i → Rule A Q W P

The rules of a tuple loop, assembled by the chain combinator.

Equations

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

theorem DescriptiveComplexity.Draw.tupleHosrc {A Q W P : Type} [DecidableEq W] (zero one : A) (wk rg : W) {emb : ChainPh 3 TuplePS → P} (tSrc tDst : W) (MatchS MatchD : (Q → A) → (W → A) → Prop) (bitFlag : (Q → A) → Prop) (setBit : Bool → (Q → A) → (W → A) → Q → A) (initLv advLv : (Q → A) → (W → A) → Q → A) (IsMaxLv : (Q → A) → Prop) (exitPh : P) (i : ChainSite 3 TupleSS) (ρ : ChainSh 3 TupleSS TupleSh i) : ∃ (p : ChainPh 3 TuplePS), (tupleRule zero one wk rg emb tSrc tDst MatchS MatchD bitFlag setBit initLv advLv IsMaxLv exitPh i ρ).srcPh = emb p ∧ tupleOwn p = i

Every rule of a tuple loop fires from a phase its site owns.

theorem DescriptiveComplexity.Draw.tupleRule_dstIn {A Q W P : Type} [DecidableEq W] (zero one : A) (wk rg : W) {emb : ChainPh 3 TuplePS → P} (tSrc tDst : W) (MatchS MatchD : (Q → A) → (W → A) → Prop) (bitFlag : (Q → A) → Prop) (setBit : Bool → (Q → A) → (W → A) → Q → A) (initLv advLv : (Q → A) → (W → A) → Q → A) (IsMaxLv : (Q → A) → Prop) (exitPh : P) {S : P → Prop} (hemb : ∀ (p : ChainPh 3 TuplePS), S (emb p)) (hexit : S exitPh) (i : ChainSite 3 TupleSS) (ρ : ChainSh 3 TupleSS TupleSh i) : S (tupleRule zero one wk rg emb tSrc tDst MatchS MatchD bitFlag setBit initLv advLv IsMaxLv exitPh i ρ).dstPh

A property of a tuple loop's phases and its exit holds of every phase it can move to: the two trips stay inside their own, the checkpoints stay where they are, and only the last dispatch leaves.

theorem DescriptiveComplexity.Draw.tupleSep {A Q W P : Type} [DecidableEq W] (zero one : A) (wk rg : W) {emb : ChainPh 3 TuplePS → P} (tSrc tDst : W) (MatchS MatchD : (Q → A) → (W → A) → Prop) (bitFlag : (Q → A) → Prop) (setBit : Bool → (Q → A) → (W → A) → Q → A) (initLv advLv : (Q → A) → (W → A) → Q → A) (IsMaxLv : (Q → A) → Prop) (exitPh : P) (hemb : Function.Injective emb) (i : ChainSite 3 TupleSS) (ρ ρ' : ChainSh 3 TupleSS TupleSh i) (f : Q → A) (g : W → A) : (tupleRule zero one wk rg emb tSrc tDst MatchS MatchD bitFlag setBit initLv advLv IsMaxLv exitPh i ρ).guard f g → (tupleRule zero one wk rg emb tSrc tDst MatchS MatchD bitFlag setBit initLv advLv IsMaxLv exitPh i ρ').guard f g → (tupleRule zero one wk rg emb tSrc tDst MatchS MatchD bitFlag setBit initLv advLv IsMaxLv exitPh i ρ).srcPh = (tupleRule zero one wk rg emb tSrc tDst MatchS MatchD bitFlag setBit initLv advLv IsMaxLv exitPh i ρ').srcPh → ρ = ρ'

A tuple loop separates in-shape.