Documentation

DescriptiveComplexity.Problems.Wide.DrawSlots

The slots of the EXPSPACE program, and the mark of a register cell #

The first concrete piece of the program: which track slots a symbol carries, which control slots a state carries, and what the input channel writes in the cell of each element at time zero. Nothing here depends on the program's phases, so it is fixed before they are enumerated.

The track slots (DescriptiveComplexity.Draw.Slot) #

slotheld bywhat it says
regevery markthis cell is a register
regFirst, regLastthe two end marksthe ends of the file, recognizable on sight
blk bevery mark, one-hotthe argument block of the cell's tag (none off the arguments)
name jpadded marksthe cell's element's j-th coordinate – an element, not a bit
pddevery markthe cell's element is canonically padded
mir, tgt, sav, valregister cellsMIRROR, TARGET, SAV, VAL – the machine's registers
wk, botthe working areathe working-cell marker, the bottom marker
ltpthe working areathe end marker of the logical interval, planted at startup
old i, new ithe working areathe current and next stage of variable i

The name slots are the budgeted register naming: a mark cannot carry its cell's full name (|Q| + |W| ≤ dd), but the encodings only inhabit the first dd₀ < dd coordinates, and those fit. Together with pdd and the one-hot blk family they are what the navigation-by-name scans (DescriptiveComplexity.Draw.Prog.reaches_toCell) read.

The control slots (DescriptiveComplexity.Draw.Ctl) #

Loop variables (elements of the source structure, for the element loops of the atom subroutines), the fold accumulators of the inner loop, the accumulators of the element-loop sub-folds, the atom verdicts of the matrix, and a few scratch flags. All bits are stored as the two designated elements (DescriptiveComplexity.Draw.bitVal).

DescriptiveComplexity.Draw.slotMark is the mark itself, with one read-back lemma per slot kind; DescriptiveComplexity.Draw.slotMark_name is the one the counting argument of Problems/Wide/Marks.lean allows, and the one everything else was built to reach.

The track slots #

source
inductive DescriptiveComplexity.Draw.Slot (ι : Type) (ko ki dd0 : ℕ) :
Type

The track slots of the program's symbols. ι is the index type of the fixed-point variables, ko/ki the numbers of outer and inner argument blocks, dd0 the coordinate width of the encodings.

  • reg {ι : Type} {ko ki dd0 : ℕ} : Slot ι ko ki dd0

    This cell is a register.

  • regFirst {ι : Type} {ko ki dd0 : ℕ} : Slot ι ko ki dd0

    This cell is the first register of the file.

  • regLast {ι : Type} {ko ki dd0 : ℕ} : Slot ι ko ki dd0

    This cell is the last register of the file.

  • blk {ι : Type} {ko ki dd0 : ℕ} : Option (Fin ko ⊕ Fin ki) → Slot ι ko ki dd0

    One-hot: the argument block of the cell's element's tag.

  • name {ι : Type} {ko ki dd0 : ℕ} : Fin dd0 → Slot ι ko ki dd0

    The cell's element's j-th coordinate, when it is padded.

  • pdd {ι : Type} {ko ki dd0 : ℕ} : Slot ι ko ki dd0

    The cell's element is canonically padded.

  • mir {ι : Type} {ko ki dd0 : ℕ} : Slot ι ko ki dd0

    The mirror of the working cell's address.

  • tgt {ι : Type} {ko ki dd0 : ℕ} : Slot ι ko ki dd0

    The target of a random access.

  • sav {ι : Type} {ko ki dd0 : ℕ} : Slot ι ko ki dd0

    The saved mirror, across a random access.

  • val {ι : Type} {ko ki dd0 : ℕ} : Slot ι ko ki dd0

    The valuation of the quantifier prefix, enumerated by the inner loop.

  • wk {ι : Type} {ko ki dd0 : ℕ} : Slot ι ko ki dd0

    The working-cell marker.

  • bot {ι : Type} {ko ki dd0 : ℕ} : Slot ι ko ki dd0

    The bottom marker, written at the empty address at startup.

  • ltp {ι : Type} {ko ki dd0 : ℕ} : Slot ι ko ki dd0

    The end marker of the logical interval, planted at DescriptiveComplexity.Draw.logicalTop at startup: what the plain sweeps stop at.

  • old {ι : Type} {ko ki dd0 : ℕ} : ι → Slot ι ko ki dd0

    The current stage of variable i.

  • new {ι : Type} {ko ki dd0 : ℕ} : ι → Slot ι ko ki dd0

    The next stage of variable i.

Instances For
    Dependency graph
    source
    @[instance_reducible]
    instance DescriptiveComplexity.Draw.instDecidableEqSlot {ι✝ : Type} {ko✝ ki✝ dd0✝ : ℕ} [DecidableEq ι✝] :
    DecidableEq (Slot ι✝ ko✝ ki✝ dd0✝)
    Equations
    Dependency graph
    source
    def DescriptiveComplexity.Draw.instDecidableEqSlot.decEq {ι✝ : Type} {ko✝ ki✝ dd0✝ : ℕ} [DecidableEq ι✝] (x✝ x✝¹ : Slot ι✝ ko✝ ki✝ dd0✝) :
    Decidable (x✝ = x✝¹)
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      Dependency graph
      source
      instance DescriptiveComplexity.Draw.Slot.instFinite {ι : Type} {ko ki dd0 : ℕ} [Finite ι] :
      Finite (Slot ι ko ki dd0)
      Dependency graph
      source
      @[instance_reducible]
      noncomputable instance DescriptiveComplexity.Draw.Slot.instFintypeOfFinite {ι : Type} {ko ki dd0 : ℕ} [Finite ι] :
      Fintype (Slot ι ko ki dd0)
      Equations
      Dependency graph

      The control slots #

      source
      inductive DescriptiveComplexity.Draw.Ctl (e na nat nf ntg : ℕ) :
      Type

      The control slots of the program's states: loop variables, the inner fold's accumulators, the sub-folds' accumulators, the atom verdicts, the leaf-read and tag-witness flags, and scratch flags.

      • lv {e na nat nf ntg : ℕ} : Fin e → Ctl e na nat nf ntg

        A loop variable of an element loop.

      • acc {e na nat nf ntg : ℕ} : Fin na → Ctl e na nat nf ntg

        An accumulator of the inner fold.

      • sac {e na nat nf ntg : ℕ} : Fin e → Ctl e na nat nf ntg

        An accumulator of an element-loop sub-fold.

      • av {e na nat nf ntg : ℕ} : Fin nat → Ctl e na nat nf ntg

        The verdict of an atom of the matrix.

      • rdf {e na nat nf ntg : ℕ} : Fin nf → Ctl e na nat nf ntg

        The verdict of a leaf read of the current element-loop round.

      • tgf {e na nat nf ntg : ℕ} : Fin ntg → Ctl e na nat nf ntg

        A tag-witness flag, one-hot over argument positions and tags.

      • flag {e na nat nf ntg : ℕ} : Fin 8 → Ctl e na nat nf ntg

        A scratch flag.

      Instances For
        Dependency graph
        source
        def DescriptiveComplexity.Draw.instDecidableEqCtl.decEq {e✝ na✝ nat✝ nf✝ ntg✝ : ℕ} (x✝ x✝¹ : Ctl e✝ na✝ nat✝ nf✝ ntg✝) :
        Decidable (x✝ = x✝¹)
        Equations
        Instances For
          Dependency graph
          source
          @[instance_reducible]
          instance DescriptiveComplexity.Draw.instDecidableEqCtl {e✝ na✝ nat✝ nf✝ ntg✝ : ℕ} :
          DecidableEq (Ctl e✝ na✝ nat✝ nf✝ ntg✝)
          Equations
          Dependency graph
          source
          instance DescriptiveComplexity.Draw.Ctl.instFinite {e na nat nf ntg : ℕ} :
          Finite (Ctl e na nat nf ntg)
          Dependency graph
          source
          @[instance_reducible]
          noncomputable instance DescriptiveComplexity.Draw.Ctl.instFintype {e na nat nf ntg : ℕ} :
          Fintype (Ctl e na nat nf ntg)
          Equations
          Dependency graph

          The mark of a register cell #

          source
          def DescriptiveComplexity.Draw.tagBlk {R P : Type} {ko ki : ℕ} :
          Tag R P (Fin ko ⊕ₗ Fin ki) → Option (Fin ko ⊕ Fin ki)

          The argument block of a tag, none off the arguments: what the one-hot blk slots of a mark record.

          Equations
          Instances For
            Dependency graph
            source
            theorem DescriptiveComplexity.Draw.tagBlk_eq_some_iff {R P : Type} {ko ki : ℕ} (τ : Tag R P (Fin ko ⊕ₗ Fin ki)) (b' : Fin ko ⊕ Fin ki) :
            tagBlk τ = some b' ↔ τ = Tag.arg (toLex b')

            The block mark decodes the tag: only an argument tag has a block, and it has its own.

            Dependency graph
            source
            noncomputable def DescriptiveComplexity.Draw.slotMark {R P ι : Type} {ko ki dd0 dd : ℕ} {A : Type} [LinearOrder R] [LinearOrder P] [LinearOrder A] (zero one : A) (hdd : dd0 ≤ dd) (x : Univ A R P (Fin ko ⊕ₗ Fin ki) dd) :
            Slot ι ko ki dd0 → A

            The mark of the cell of an element: what the input channel writes there at time zero. The name slots carry the element's first dd0 coordinates, the blk slots its tag's block one-hot, pdd whether it is canonically padded, the two end slots whether it is an extremum of the universe order; the machine's registers and the working-area tracks start clear.

            Equations
            Instances For
              Dependency graph
              source
              @[simp]
              theorem DescriptiveComplexity.Draw.slotMark_reg {R P ι : Type} {ko ki dd0 dd : ℕ} {A : Type} [LinearOrder R] [LinearOrder P] [LinearOrder A] {zero one : A} {hdd : dd0 ≤ dd} (x : Univ A R P (Fin ko ⊕ₗ Fin ki) dd) :
              slotMark zero one hdd x Slot.reg = one
              Dependency graph
              source
              @[simp]
              theorem DescriptiveComplexity.Draw.slotMark_name {R P ι : Type} {ko ki dd0 dd : ℕ} {A : Type} [LinearOrder R] [LinearOrder P] [LinearOrder A] {zero one : A} {hdd : dd0 ≤ dd} (x : Univ A R P (Fin ko ⊕ₗ Fin ki) dd) (j : Fin dd0) :
              slotMark zero one hdd x (Slot.name j) = x.2 (Fin.castLE hdd j)
              Dependency graph
              source
              def DescriptiveComplexity.Draw.IsTopNonArg {R P : Type} {ko ki dd : ℕ} {A : Type} [LinearOrder R] [LinearOrder P] [LinearOrder A] (x : Univ A R P (Fin ko ⊕ₗ Fin ki) dd) :
              Prop

              Being the greatest element that carries no argument block: the element the register channel marks below its file, so that every logical address stays clear of it and the file lies above the working area (DescriptiveComplexity.wmSetLt_wmRegSeg_of_above).

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                Dependency graph
                source
                theorem DescriptiveComplexity.Draw.IsTopNonArg.unique {R P : Type} {ko ki dd : ℕ} {A : Type} [LinearOrder R] [LinearOrder P] [LinearOrder A] {x y : Univ A R P (Fin ko ⊕ₗ Fin ki) dd} (hx : IsTopNonArg x) (hy : IsTopNonArg y) :
                x = y

                There is only one greatest element carrying no argument block: two of them bound each other.

                Dependency graph
                source
                noncomputable def DescriptiveComplexity.Draw.regSlotMark {R P ι : Type} {ko ki dd0 dd : ℕ} {A : Type} [LinearOrder R] [LinearOrder P] [LinearOrder A] (zero one : A) (hdd : dd0 ≤ dd) (x : Univ A R P (Fin ko ⊕ₗ Fin ki) dd) (s : Slot ι ko ki dd0) :
                A

                The mark of the cell of an element, at the register channel: the mark above with one slot changed. The channel writes for the argument elements and for one element below them, so the file's first register is not the least element of the universe but the greatest element carrying no argument block – and that is what the regFirst slot has to say, the walks reading the file's ends off these two slots. The regLast slot needs no change: the argument tags being the greatest, the last register is the last element.

                Equations
                Instances For
                  Dependency graph
                  source
                  @[simp]
                  theorem DescriptiveComplexity.Draw.regSlotMark_regFirst {R P ι : Type} {ko ki dd0 dd : ℕ} {A : Type} [LinearOrder R] [LinearOrder P] [LinearOrder A] {zero one : A} {hdd : dd0 ≤ dd} (x : Univ A R P (Fin ko ⊕ₗ Fin ki) dd) :
                  regSlotMark zero one hdd x Slot.regFirst = bitVal zero one (IsTopNonArg x)
                  Dependency graph
                  source
                  @[simp]
                  theorem DescriptiveComplexity.Draw.regSlotMark_reg {R P ι : Type} {ko ki dd0 dd : ℕ} {A : Type} [LinearOrder R] [LinearOrder P] [LinearOrder A] {zero one : A} {hdd : dd0 ≤ dd} (x : Univ A R P (Fin ko ⊕ₗ Fin ki) dd) :
                  regSlotMark zero one hdd x Slot.reg = one
                  Dependency graph
                  source
                  @[simp]
                  theorem DescriptiveComplexity.Draw.regSlotMark_name {R P ι : Type} {ko ki dd0 dd : ℕ} {A : Type} [LinearOrder R] [LinearOrder P] [LinearOrder A] {zero one : A} {hdd : dd0 ≤ dd} (x : Univ A R P (Fin ko ⊕ₗ Fin ki) dd) (j : Fin dd0) :
                  regSlotMark zero one hdd x (Slot.name j) = x.2 (Fin.castLE hdd j)
                  Dependency graph
                  source
                  @[simp]
                  theorem DescriptiveComplexity.Draw.regSlotMark_regLast {R P ι : Type} {ko ki dd0 dd : ℕ} {A : Type} [LinearOrder R] [LinearOrder P] [LinearOrder A] {zero one : A} {hdd : dd0 ≤ dd} (x : Univ A R P (Fin ko ⊕ₗ Fin ki) dd) :
                  regSlotMark zero one hdd x Slot.regLast = bitVal zero one (∀ (y : Univ A R P (Fin ko ⊕ₗ Fin ki) dd), tagTupleLe y x)
                  Dependency graph
                  source
                  @[simp]
                  theorem DescriptiveComplexity.Draw.regSlotMark_blk {R P ι : Type} {ko ki dd0 dd : ℕ} {A : Type} [LinearOrder R] [LinearOrder P] [LinearOrder A] {zero one : A} {hdd : dd0 ≤ dd} (x : Univ A R P (Fin ko ⊕ₗ Fin ki) dd) (b : Option (Fin ko ⊕ Fin ki)) :
                  regSlotMark zero one hdd x (Slot.blk b) = bitVal zero one (tagBlk x.1 = b)
                  Dependency graph
                  source
                  @[simp]
                  theorem DescriptiveComplexity.Draw.regSlotMark_pdd {R P ι : Type} {ko ki dd0 dd : ℕ} {A : Type} [LinearOrder R] [LinearOrder P] [LinearOrder A] {zero one : A} {hdd : dd0 ≤ dd} (x : Univ A R P (Fin ko ⊕ₗ Fin ki) dd) :
                  regSlotMark zero one hdd x Slot.pdd = bitVal zero one (∀ (j : Fin dd), dd0 ≤ ↑j → x.2 j = zero)
                  Dependency graph
                  source
                  theorem DescriptiveComplexity.Draw.tagBlk_eq_none_of_least {R P : Type} {ko ki dd : ℕ} {A : Type} [LinearOrder R] [LinearOrder P] [LinearOrder A] {x : Univ A R P (Fin ko ⊕ₗ Fin ki) dd} (hleast : ∀ (y : Univ A R P (Fin ko ⊕ₗ Fin ki) dd), tagTupleLe x y) :
                  tagBlk x.1 = none

                  The least element carries no argument block: the argument tags are the greatest ones (DescriptiveComplexity.Draw.lt_arg), so the minimum of the universe is tagged by the control, the alphabet or a phase. This is what puts every logical address strictly below the register file: the file's first cell is the segment of the least element, and no logical address contains it.

                  Dependency graph
                  source
                  theorem DescriptiveComplexity.Draw.eq_of_slotMark_name {R P : Type} {ko ki dd0 dd : ℕ} {A : Type} {zero : A} {hdd : dd0 ≤ dd} {x y : Univ A R P (Fin ko ⊕ₗ Fin ki) dd} (hblk : tagBlk x.1 = tagBlk y.1) {b : Fin ko ⊕ Fin ki} (hb : tagBlk x.1 = some b) (hnm : ∀ (j : Fin dd0), x.2 (Fin.castLE hdd j) = y.2 (Fin.castLE hdd j)) (hpx : ∀ (j : Fin dd), dd0 ≤ ↑j → x.2 j = zero) (hpy : ∀ (j : Fin dd), dd0 ≤ ↑j → y.2 j = zero) :
                  x = y

                  A mark determines its cell among the padded cells: two padded elements with the same tag block one-hots and the same name slots are equal, provided their tags are argument tags (the block determines an argument tag). This is what makes the navigation-by-name scans stop at exactly one cell.

                  Dependency graph