Documentation

DescriptiveComplexity.Problems.Wide.DrawInstMat

The matrix's stages: the atom runs in the sequencer's shape #

The sequencer (DescriptiveComplexity.Draw.seq_run) drives its stages through one uniform interface: entry one cell to the marker's right, one fixed walked track, exit at the next checkpoint. This file wraps the four instantiated atom runs into that shape:

The element loop's walk-back #

source
theorem DescriptiveComplexity.Draw.elem_back {A R P Q W K : Type} {dd : ℕ} [Fintype Q] [Fintype W] [DecidableEq W] [LinearOrder A] [LinearOrder R] [LinearOrder P] [LinearOrder K] [FirstOrder.Language.wide.Structure (Univ A R P K dd)] [Finite A] [Finite R] [Finite P] [Finite K] {PR : Prog A R P Q W K dd} {nr : ℕ} {I : Type} {ile : I → I → Prop} (RF : IxFile (Univ A R P K dd) I ile) {wk rg : W} {emb : ElemPh nr → P} {rdTrack : Fin nr → W} {MatchOf : Fin nr → (Q → A) → (W → A) → Prop} {setFlag : Fin nr → Bool → (Q → A) → (W → A) → Q → A} {initEl advEl exitSt : (Q → A) → (W → A) → Q → A} {IsMaxEl : (Q → A) → Prop} {exitPh : P} {rEmb : (i : ElemSite nr) → ElemSh nr i → R} (hlin : IsLinOrd WMLe) {v v' : Univ A R P K dd → Prop} (hvi : WMIncr WMLe v v') {rest : (Univ A R P K dd → Prop) → W → A} (hwkS : ∀ (r : Univ A R P K dd → Prop), rest r wk = bitVal PR.zero PR.one (r = v)) {t₀ : W} {m₀ : I → Prop} (hwkt₀ : wk ≠ t₀) (hR : PR.table.Reads) (hrules : ∀ (i : ElemSite nr) (ρ : ElemSh nr i), PR.rules (rEmb i ρ) = elemRule PR.one wk rg emb rdTrack MatchOf setFlag initEl advEl exitSt IsMaxEl exitPh i ρ) {f : Q → A} :
(wideData (Univ A R P K dd)).Step { state := Sum.inr (PR.stElt (emb ElemPh.e0) f), head := Sum.inl v', tape := wideTape (PR.trackTapeAt RF.cell t₀ rest m₀) (PR.syElt PR.blank) } { state := Sum.inr (PR.stElt (emb ElemPh.e0) f), head := Sum.inl v, tape := wideTape (PR.trackTapeAt RF.cell t₀ rest m₀) (PR.syElt PR.blank) }

The one leftward step a caller's rightward dispatch into an element loop owes: at its entry checkpoint, the walk back down to the marker.

Dependency graph

The boundary discipline #

source
theorem DescriptiveComplexity.Draw.Data.stageEndSt_eq {L : FirstOrder.Language} {dt : Data L} {A R P : Type} {st : TapeStD dt A R P} {v : Univ A R P dt.KIx dt.dd → Prop} (hs : st.sav = v) (ht : st.tgt = v) :
stageEndSt st v = st

A stage atom entered at the boundary leaves the state unchanged: with SAV and TARGET already at the home address, the restore restores what was there.

Dependency graph
source
theorem DescriptiveComplexity.Draw.Data.trackTape_val_eq_mir {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)] {PR : Prog A R P dt.CtlIx dt.SlotIx dt.KIx dt.dd} (RF : RegFile (Univ A R P dt.KIx dt.dd)) (st : TapeStD dt A R P) :
PR.trackTapeAt RF.cell Slot.val (dt.back RF.cell PR.zero PR.one ⋯ st) st.val = PR.trackTapeAt RF.cell Slot.mir (dt.back RF.cell PR.zero PR.one ⋯ st) st.mir

The val-walked and the mir-walked presentations of one state coincide: both are the naked background.

Dependency graph

The comparison atom, in the sequencer's shape #

The expansion atom, in the sequencer's shape #

The stage atom, in the sequencer's shape #

One gate block, in the sequencer's shape #

source
theorem DescriptiveComplexity.Draw.Data.gateBlock_hStage_pos {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)) [Nonempty A] [L.IsRelational] [L.Structure A] (b : Fin dt.ko ⊕ Fin dt.ki) (hc : Fintype.card dt.X.Tag ≤ dt.ntgDim) (hn : ∀ (t' : dt.X.Tag), (dt.domPk t').n ≤ dt.eDim) (hrd : ∀ (t' : dt.X.Tag), dt.domNr t' ≤ dt.nfDim) {emb : dt.GateBlockPh → P} (wellG : (dt.SlotIx → A) → Prop) (setFail : (dt.CtlIx → A) → (dt.SlotIx → A) → dt.CtlIx → A) {failPh exitPh : P} {rEmb : (i : dt.GateBlockSite) → dt.GateBlockSh i → R} [Finite dt.KIx] (hrules : ∀ (i : dt.GateBlockSite) (ρ : dt.GateBlockSh i), PR.rules (rEmb i ρ) = dt.gateBlockRule PR.one emb (dt.gateArgs PR.zero PR.one b hc hn hrd) wellG setFail failPh exitPh i ρ) (hR : PR.table.Reads) (hlin : IsLinOrd WMLe) (hord : ∀ (x y : Univ A R P dt.KIx dt.dd), WMLe x y ↔ tagTupleLe x y) {gtop gbot : Univ A R P dt.KIx dt.dd} (htop : ∀ (y : Univ A R P dt.KIx dt.dd), WMLe y gtop) (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') {st : TapeStD dt A R P} (hwkSt : st.wk = fun (r : Univ A R P dt.KIx dt.dd → Prop) => r = v) (Test : Univ A R P dt.KIx dt.dd → Prop) (hcompat : ∀ (u : Univ A R P dt.KIx dt.dd), wellG (PR.passTracksAt RF.cell Slot.mir (dt.back RF.cell PR.zero PR.one ⋯ st) st.mir (RF.cell u)) ↔ Test u) (t : dt.X.Tag) (htag : dt.dspTagOf PR.zero PR.one (wmBlk st.mir (Tag.arg (toLex b))) = t) (hTest : ∀ (u : Univ A R P dt.KIx dt.dd), Test u) (f : dt.CtlIx → A) :
Relation.ReflTransGen (wideData (Univ A R P dt.KIx dt.dd)).Step { state := Sum.inr (PR.stElt (emb (Sum.inl TestPh.up)) f), head := Sum.inl v', tape := wideTape (PR.trackTapeAt RF.cell Slot.val (dt.back RF.cell PR.zero PR.one ⋯ st) st.val) (PR.syElt PR.blank) } { state := Sum.inr (PR.stElt exitPh ((dt.gateArgs PR.zero PR.one b hc hn hrd).exitSt t (dt.gateFam RF PR.zero PR.one b st t hc hn hrd v (dt.gateTagFam RF PR.zero PR.one b st hc hn hrd v f (Fin.last (Fintype.card dt.X.Tag))) (toLex topTup) (Fin.last (dt.domNr t))) (dt.back RF.cell PR.zero PR.one ⋯ st v))), head := Sum.inl v', tape := wideTape (PR.trackTapeAt RF.cell Slot.val (dt.back RF.cell PR.zero PR.one ⋯ st) st.val) (PR.syElt PR.blank) }

A passing gate block, entered by a dispatch: every register is well-shaped, so the file test passes, the domain evaluation runs on the block's decoded tag, and the block exits to the next checkpoint.

Dependency graph