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.

The discharge