The seek kit: random access

The kit wrapping DescriptiveComplexity.Draw.Prog.reaches_fileSeekTo – the whole random-access loop: from the checkpoint with the working-cell marker and its mirror at the empty address, rounds of turnaround, file test MIRROR = TARGET, and ADVANCE, until the test passes on the target's cell.

Its seventeen rule families are the loop's nine phases' worth of the shapes the other kits established – the test trip's, the advance's – plus the two marker steps a0/put1 whose guards (wk = one ∧ rg ≠ one, ⊤) the successive hardenings of the layer made dischargeable. The target register tg appears only in the test rules' guards: the per-register question is the walked mirror digit agrees with the target digit, a comparison of two slots of one symbol.

Exit is the caller's: a rule at the passing phase ty, at the marker, guarded wk = one ∧ rg ≠ one – disjoint from every rule here.

The seek loop's shapes

inductive DescriptiveComplexity.Draw.SeekPh : Type

The phases of a seek: the loop head, the test trip's four, and the advance's four.

• chk : SeekPh

  The loop head, at the marker.

• scan : SeekPh

  Scanning up to the file top, for the test.

• t2b : SeekPh

  Bounced off the top, about to re-enter the test.

• ty : SeekPh

  Every register so far agreed (also: returning with verdict yes).

• tn : SeekPh

  Some register differed (also: returning with verdict no).

• a1 : SeekPh

  On the fresh marker cell, about to write it.

• a2 : SeekPh

  Scanning up to the file top, for the increment.

• a2b : SeekPh

  Bounced off the top, about to re-enter the increment.

• a3 : SeekPh

  Running the increment: clearing set digits.

@[instance_reducible]

instance DescriptiveComplexity.Draw.instDecidableEqSeekPh : DecidableEq SeekPh

Equations

• DescriptiveComplexity.Draw.instDecidableEqSeekPh x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance DescriptiveComplexity.Draw.instFiniteSeekPh : Finite SeekPh

inductive DescriptiveComplexity.Draw.SeekRule : Type

The rule families of a seek, one constructor each.

• turn : SeekRule

  Turn off the marker into the test's scan.

• scanT : SeekRule

  Scan right while the file-top mark is clear (test).

• bT1 : SeekRule

  At the file top: step left into the bounce phase (test).

• bT2 : SeekRule

  Bounce: step back right into the test.

• pass : SeekRule

  At a register whose mirror digit agrees with the target's: carry on.

• fail : SeekRule

  At a register where they differ: switch to the failing phase.

• walkTy : SeekRule

  Walk left over unmarked cells, and return, in the passing phase.

• stayTn : SeekRule

  Hold at registers, walk and return, in the failing phase.

• a0 : SeekRule

  At the marker with verdict no: erase it and step right.

• put1 : SeekRule

  Write the marker at the fresh cell, stepping on.

• scanA : SeekRule

  Scan right while the file-top mark is clear (increment).

• bA1 : SeekRule

  At the file top: step left into the bounce phase (increment).

• bA2 : SeekRule

  Bounce: step back right into the increment.

• clear : SeekRule

  At a register with a set mirror digit: clear it, carry on.

• set : SeekRule

  At a register with a clear mirror digit: set it, back to the head.

• walkA : SeekRule

  Walk left over unmarked cells while carrying.

• stayChk : SeekRule

  Hold at registers, walk and return, at the loop head.

@[instance_reducible]

instance DescriptiveComplexity.Draw.instDecidableEqSeekRule : DecidableEq SeekRule

Equations

• DescriptiveComplexity.Draw.instDecidableEqSeekRule x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance DescriptiveComplexity.Draw.instFiniteSeekRule : Finite SeekRule

structure DescriptiveComplexity.Draw.SeekKit (A Q W P : Type) : Type

A seek kit: the walked mirror track, the target track, the service slots, and the phases.

• t : W

  The walked mirror track.

• tg : W

  The target track the mirror is compared against.

• rg : W

  The register mark.

• rl : W

  The file-top mark.

• wk : W

  The working-cell marker slot.

• emb : SeekPh → P

  The kit's phases in the program.

def DescriptiveComplexity.Draw.SeekKit.rule {A Q W P : Type} [DecidableEq W] (κ : SeekKit A Q W P) (zero one : A) : SeekRule → Rule A Q W P

The kit's rules.

Equations

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

theorem DescriptiveComplexity.Draw.SeekKit.dstPh_emb {A Q W P : Type} [DecidableEq W] (κ : SeekKit A Q W P) (zero one : A) (ρ : SeekRule) : ∃ (p : SeekPh), (κ.rule zero one ρ).dstPh = κ.emb p

A seek stays inside its own phases: every rule of the kit lands in one of the phases the kit was given.

theorem DescriptiveComplexity.Draw.SeekKit.sep {A Q W P : Type} [DecidableEq W] (κ : SeekKit A Q W P) (zero one : A) (hzo : zero ≠ one) (hemb : Function.Injective κ.emb) (ρ ρ' : SeekRule) (f : Q → A) (g : W → A) : (κ.rule zero one ρ).guard f g → (κ.rule zero one ρ').guard f g → (κ.rule zero one ρ).srcPh = (κ.rule zero one ρ').srcPh → ρ = ρ'

In-shape separation.

theorem DescriptiveComplexity.Draw.SeekKit.exit_disjoint {A Q W P : Type} [DecidableEq W] (κ : SeekKit A Q W P) (zero one : A) (hemb : Function.Injective κ.emb) (ρ : SeekRule) (f : Q → A) (g : W → A) : (κ.rule zero one ρ).guard f g → g κ.wk = one → g κ.rg ≠ one → (κ.rule zero one ρ).srcPh = κ.emb SeekPh.ty → False

Exit disjointness at the kit's passing verdict phase, where the caller's exit rule reads the sought cell.

The discharge

theorem DescriptiveComplexity.Draw.SeekKit.reachesIn {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} {κ : SeekKit A Q W P} {rEmb : SeekRule → R} (hrules : ∀ (ρ : SeekRule), PR.rules (rEmb ρ) = κ.rule PR.zero PR.one ρ) {I : Type} [Finite I] {ile : I → I → Prop} (F : IxFile (Univ A R P K dd) I ile) (hR : PR.table.Reads) (hlin : IsLinOrd WMLe) (hix : IsLinOrd ile) {elt : I → Univ A R P K dd} {Use : I → Prop} (hinj : Function.Injective elt) (hmono : ∀ (u u' : I), WMLt ile u u' ↔ WMLt WMLe (elt u) (elt u')) (hup : ∀ (u : I) (x : Univ A R P K dd), Use u → WMLt WMLe (elt u) x → ∃ (u' : I), Use u' ∧ elt u' = x) (hnerg : κ.t ≠ κ.rg) (hnerl : κ.rl ≠ κ.t) (hnewk : κ.wk ≠ κ.t) (hnetg : κ.tg ≠ κ.t) {gtop gbot : I} (htop : ∀ (y : I), ile y gtop) (hbot : ∀ (y : I), ile gbot y) {T : Univ A R P K dd → Prop} (hTh : IxHolds elt Use T) (hT : WMSetLt WMLe T (F.cell gbot)) {bg : (Univ A R P K dd → Prop) → (Univ A R P K dd → Prop) → W → A} {bgN : (Univ A R P K dd → Prop) → W → A} (hbgwk : ∀ (v r : Univ A R P K dd → Prop), bg v r κ.wk = bitVal PR.zero PR.one (r = v)) (hbgNwk : ∀ (r : Univ A R P K dd → Prop), bgN r κ.wk = PR.zero) (hbgNoth : ∀ (v r : Univ A R P K dd → Prop) (s : W), s ≠ κ.wk → bgN r s = bg v r s) (hbgrg : ∀ (v r : Univ A R P K dd → Prop), bg v r κ.rg = bitVal PR.zero PR.one (∃ (u : I), r = F.cell u)) (hbgrl : ∀ (v r : Univ A R P K dd → Prop), bg v r κ.rl = bitVal PR.zero PR.one (r = F.cell gtop)) (hbgtg : ∀ (v : Univ A R P K dd → Prop) (u : I), bg v (F.cell u) κ.tg = bitVal PR.zero PR.one (ixMark elt T u)) {fc : Q → A} {w : ℕ} (hgap : ∀ (u u' : I), IxSucc ile u u' → wideRank (F.cell u') - wideRank (F.cell u) ≤ w) : (wideData (Univ A R P K dd)).ReachesIn (wideRank T * (1 + (wideRank (F.cell gtop) + 3 + (ixRank ile gtop - ixRank ile gbot) * w + wideRank (F.cell gbot)) + (wideRank (F.cell gtop) + ((ixRank ile gtop - ixRank ile gbot) * w + 1) + wideRank (F.cell gbot) + 4)) + 1 + (wideRank (F.cell gtop) + 3 + (ixRank ile gtop - ixRank ile gbot) * w + wideRank (F.cell gbot))) { state := Sum.inr (PR.stElt (κ.emb SeekPh.chk) fc), head := Sum.inl fun (x : Univ A R P K dd) => False, tape := wideTape (PR.trackTapeAt F.cell κ.t (bg fun (x : Univ A R P K dd) => False) fun (x : I) => False) (PR.syElt PR.blank) } { state := Sum.inr (PR.stElt (κ.emb SeekPh.ty) fc), head := Sum.inl T, tape := wideTape (PR.trackTapeAt F.cell κ.t (bg T) (ixMark elt T)) (PR.syElt PR.blank) }

The kit seeks the working cell to the target: from the loop head with the marker and mirror at the empty address, to the passing verdict phase on the target's cell.

theorem DescriptiveComplexity.Draw.SeekKit.reaches {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} {κ : SeekKit A Q W P} {rEmb : SeekRule → R} (hrules : ∀ (ρ : SeekRule), PR.rules (rEmb ρ) = κ.rule PR.zero PR.one ρ) {I : Type} [Finite I] {ile : I → I → Prop} (F : IxFile (Univ A R P K dd) I ile) (hR : PR.table.Reads) (hlin : IsLinOrd WMLe) (hix : IsLinOrd ile) {elt : I → Univ A R P K dd} {Use : I → Prop} (hinj : Function.Injective elt) (hmono : ∀ (u u' : I), WMLt ile u u' ↔ WMLt WMLe (elt u) (elt u')) (hup : ∀ (u : I) (x : Univ A R P K dd), Use u → WMLt WMLe (elt u) x → ∃ (u' : I), Use u' ∧ elt u' = x) (hnerg : κ.t ≠ κ.rg) (hnerl : κ.rl ≠ κ.t) (hnewk : κ.wk ≠ κ.t) (hnetg : κ.tg ≠ κ.t) {gtop gbot : I} (htop : ∀ (y : I), ile y gtop) (hbot : ∀ (y : I), ile gbot y) {T : Univ A R P K dd → Prop} (hTh : IxHolds elt Use T) (hT : WMSetLt WMLe T (F.cell gbot)) {bg : (Univ A R P K dd → Prop) → (Univ A R P K dd → Prop) → W → A} {bgN : (Univ A R P K dd → Prop) → W → A} (hbgwk : ∀ (v r : Univ A R P K dd → Prop), bg v r κ.wk = bitVal PR.zero PR.one (r = v)) (hbgNwk : ∀ (r : Univ A R P K dd → Prop), bgN r κ.wk = PR.zero) (hbgNoth : ∀ (v r : Univ A R P K dd → Prop) (s : W), s ≠ κ.wk → bgN r s = bg v r s) (hbgrg : ∀ (v r : Univ A R P K dd → Prop), bg v r κ.rg = bitVal PR.zero PR.one (∃ (u : I), r = F.cell u)) (hbgrl : ∀ (v r : Univ A R P K dd → Prop), bg v r κ.rl = bitVal PR.zero PR.one (r = F.cell gtop)) (hbgtg : ∀ (v : Univ A R P K dd → Prop) (u : I), bg v (F.cell u) κ.tg = bitVal PR.zero PR.one (ixMark elt T u)) {fc : Q → A} : Relation.ReflTransGen (wideData (Univ A R P K dd)).Step { state := Sum.inr (PR.stElt (κ.emb SeekPh.chk) fc), head := Sum.inl fun (x : Univ A R P K dd) => False, tape := wideTape (PR.trackTapeAt F.cell κ.t (bg fun (x : Univ A R P K dd) => False) fun (x : I) => False) (PR.syElt PR.blank) } { state := Sum.inr (PR.stElt (κ.emb SeekPh.ty) fc), head := Sum.inl T, tape := wideTape (PR.trackTapeAt F.cell κ.t (bg T) (ixMark elt T)) (PR.syElt PR.blank) }

The kit seeks the working cell to the target, the budget forgotten.