Documentation

DescriptiveComplexity.Problems.Wide.DrawVar

One variable's machinery: gates, the VAL loop, the stage write #

The spine of the per-variable evaluation (DescriptiveComplexity.Problems.Wide.DrawEval dispatches into it, once per variable position): the gates decide whether the working address's outer blocks encode points – their machinery is abstract here, their verdict a control flag – the junk path writes False into the stage track directly, and the valid path runs the VAL loop: clear the VAL register, evaluate the matrix at the empty valuation, then rounds of exhaustion test, increment and matrix until VAL is exhausted, the accumulator folds riding in the dispatching rules' dstSt (separation never reads dstSt, so the folds are parameters here – initSt at the empty valuation, storeCarry at each increment's block-indexed landing, postFold after each matrix pass – and their content is fixed with the runs, not with the shapes).

Everything is generic over the program's phase type: the spine's phases embed by a parameter, the gates' and the matrix's machineries come with their own rules, and the exit – writing the variable's next-stage bit at the marker off the verdict accumulator – targets a parameter phase. One copy of this file's shapes per variable position is instantiated at assembly.

The shapes #

source
inductive DescriptiveComplexity.Draw.VarPh (B PG PX : Type) :
Type

The phases of one variable's machinery: the four checkpoints, the kit copies, and the two abstract blocks. B is the carry-block index of the VAL increment.

  • vchk0 {B PG PX : Type} : VarPh B PG PX

    The entry checkpoint: walk to the marker, begin the gates.

  • gatesP {B PG PX : Type} : PG → VarPh B PG PX

    A phase of the gates' machinery.

  • vchk1 {B PG PX : Type} : VarPh B PG PX

    After the gates: dispatch on their verdict flag.

  • clearValP {B PG PX : Type} : TrackPh → VarPh B PG PX

    Clearing the VAL register.

  • matrixP {B PG PX : Type} : PX → VarPh B PG PX

    A phase of the matrix's machinery.

  • mchk1 {B PG PX : Type} : VarPh B PG PX

    After a matrix pass: fold and begin the exhaustion test.

  • valTestP {B PG PX : Type} : TestPh → VarPh B PG PX

    The exhaustion test on VAL.

  • valIncrP {B PG PX : Type} : IncrPh B → VarPh B PG PX

    The increment of VAL, landing per carry block.

  • vchk2 {B PG PX : Type} : VarPh B PG PX

    Converged: write the stage bit and leave.

Instances For
    Dependency graph
    source
    inductive DescriptiveComplexity.Draw.VarSite (SG SX : Type) :
    Type

    The sites of one variable's machinery.

    • vchk0 {SG SX : Type} : VarSite SG SX

      The entry checkpoint.

    • gates {SG SX : Type} : SG → VarSite SG SX

      A gates site.

    • vchk1 {SG SX : Type} : VarSite SG SX

      The verdict checkpoint.

    • clearVal {SG SX : Type} : VarSite SG SX

      The VAL clear.

    • matrix {SG SX : Type} : SX → VarSite SG SX

      A matrix site.

    • mchk1 {SG SX : Type} : VarSite SG SX

      The post-matrix checkpoint.

    • valTest {SG SX : Type} : VarSite SG SX

      The exhaustion test.

    • valIncr {SG SX : Type} : VarSite SG SX

      The VAL increment.

    • vchk2 {SG SX : Type} : VarSite SG SX

      The exit checkpoint.

    Instances For
      Dependency graph
      source
      def DescriptiveComplexity.Draw.VarSh (SG SX : Type) (ShG : SG → Type) (ShX : SX → Type) (B : Type) :
      VarSite SG SX → Type

      The rule shape of each site: kit rules summed with exits, the checkpoints' the three-rule gadget of the spine layer.

      Equations
      Instances For
        Dependency graph
        source
        def DescriptiveComplexity.Draw.varOwn {B PG PX SG SX : Type} (ownG : PG → SG) (ownX : PX → SX) :
        VarPh B PG PX → VarSite SG SX

        The owner of each phase of one variable's machinery, over the gates' and the matrix's owners.

        Equations
        Instances For
          Dependency graph
          source
          @[reducible, inline]
          abbrev DescriptiveComplexity.Draw.Data.CarryB {L : FirstOrder.Language} (dt : Data L) :
          Type

          The carry-block index of the VAL increment.

          Equations
          Instances For
            Dependency graph
            source
            noncomputable def DescriptiveComplexity.Draw.Data.varRule {L : FirstOrder.Language} (dt : Data L) {A Q P PG PX SG SX : Type} (zero one : A) {ShG : SG → Type} {ShX : SX → Type} (emb : VarPh dt.CarryB PG PX → P) (ruleG : (s : SG) → ShG s → Rule A Q dt.SlotIx P) (ruleX : (s : SX) → ShX s → Rule A Q dt.SlotIx P) (pgEntry pxEntry exitPh : P) (newSlot : dt.SlotIx) (gateFlag : Q) (accBit : (Q → A) → Prop) (enterSt initSt postFold : (Q → A) → (dt.SlotIx → A) → Q → A) (storeCarry : dt.CarryB → (Q → A) → (dt.SlotIx → A) → Q → A) (i : VarSite SG SX) :
            VarSh SG SX ShG ShX dt.CarryB i → Rule A Q dt.SlotIx P

            The rules of one variable's machinery. Parameters: the phase embedding, the two abstract machineries with their entry phases, the exit phase, the variable's stage slot, the gates' verdict flag, the verdict accumulator, and the three fold updates.

            Equations
            Instances For
              Dependency graph
              source
              theorem DescriptiveComplexity.Draw.Data.varRule_dstIn {L : FirstOrder.Language} (dt : Data L) {A Q P PG PX SG SX : Type} (zero one : A) {ShG : SG → Type} {ShX : SX → Type} {emb : VarPh dt.CarryB PG PX → P} {ruleG : (s : SG) → ShG s → Rule A Q dt.SlotIx P} {ruleX : (s : SX) → ShX s → Rule A Q dt.SlotIx P} (pgEntry pxEntry exitPh : P) (newSlot : dt.SlotIx) (gateFlag : Q) (accBit : (Q → A) → Prop) (enterSt initSt postFold : (Q → A) → (dt.SlotIx → A) → Q → A) (storeCarry : dt.CarryB → (Q → A) → (dt.SlotIx → A) → Q → A) {S : P → Prop} (hemb : ∀ (p : VarPh dt.CarryB PG PX), S (emb p)) (hexit : S exitPh) (hG : ∀ (s : SG) (ρ : ShG s), S (ruleG s ρ).dstPh) (hX : ∀ (s : SX) (ρ : ShX s), S (ruleX s ρ).dstPh) (hpg : S pgEntry) (hpx : S pxEntry) (i : VarSite SG SX) (ρ : VarSh SG SX ShG ShX dt.CarryB i) :
              S (dt.varRule zero one emb ruleG ruleX pgEntry pxEntry exitPh newSlot gateFlag accBit enterSt initSt postFold storeCarry i ρ).dstPh

              A property of a variable machinery's phases and its exit holds of every phase it can move to, given it holds of the gates' and the matrix's.

              Dependency graph
              source
              theorem DescriptiveComplexity.Draw.Data.varHosrc {L : FirstOrder.Language} (dt : Data L) {A Q P PG PX SG SX : Type} (zero one : A) {ShG : SG → Type} {ShX : SX → Type} {emb : VarPh dt.CarryB PG PX → P} {ruleG : (s : SG) → ShG s → Rule A Q dt.SlotIx P} {ruleX : (s : SX) → ShX s → Rule A Q dt.SlotIx P} (pgEntry pxEntry exitPh : P) (newSlot : dt.SlotIx) (gateFlag : Q) (accBit : (Q → A) → Prop) (enterSt initSt postFold : (Q → A) → (dt.SlotIx → A) → Q → A) (storeCarry : dt.CarryB → (Q → A) → (dt.SlotIx → A) → Q → A) {ownG : PG → SG} {ownX : PX → SX} (hosrcG : ∀ (s : SG) (ρ : ShG s), ∃ (p : PG), (ruleG s ρ).srcPh = emb (VarPh.gatesP p) ∧ ownG p = s) (hosrcX : ∀ (s : SX) (ρ : ShX s), ∃ (p : PX), (ruleX s ρ).srcPh = emb (VarPh.matrixP p) ∧ ownX p = s) (i : VarSite SG SX) (ρ : VarSh SG SX ShG ShX dt.CarryB i) :
              ∃ (p : VarPh dt.CarryB PG PX), (dt.varRule zero one emb ruleG ruleX pgEntry pxEntry exitPh newSlot gateFlag accBit enterSt initSt postFold storeCarry i ρ).srcPh = emb p ∧ varOwn ownG ownX p = i

              Every rule of one variable's machinery fires from a phase its site owns; the two abstract machineries' obligations are parameters.

              Dependency graph
              source
              theorem DescriptiveComplexity.Draw.Data.varSep {L : FirstOrder.Language} (dt : Data L) {A Q P PG PX SG SX : Type} (zero one : A) {ShG : SG → Type} {ShX : SX → Type} (hzo : zero ≠ one) {emb : VarPh dt.CarryB PG PX → P} (hemb : Function.Injective emb) {ruleG : (s : SG) → ShG s → Rule A Q dt.SlotIx P} {ruleX : (s : SX) → ShX s → Rule A Q dt.SlotIx P} {pgEntry pxEntry exitPh : P} {newSlot : dt.SlotIx} {gateFlag : Q} {accBit : (Q → A) → Prop} {enterSt initSt postFold : (Q → A) → (dt.SlotIx → A) → Q → A} {storeCarry : dt.CarryB → (Q → A) → (dt.SlotIx → A) → Q → A} (hsepG : ∀ (s : SG) (ρ ρ' : ShG s) (f : Q → A) (g : dt.SlotIx → A), (ruleG s ρ).guard f g → (ruleG s ρ').guard f g → (ruleG s ρ).srcPh = (ruleG s ρ').srcPh → ρ = ρ') (hsepX : ∀ (s : SX) (ρ ρ' : ShX s) (f : Q → A) (g : dt.SlotIx → A), (ruleX s ρ).guard f g → (ruleX s ρ').guard f g → (ruleX s ρ).srcPh = (ruleX s ρ').srcPh → ρ = ρ') (i : VarSite SG SX) (ρ ρ' : VarSh SG SX ShG ShX dt.CarryB i) (f : Q → A) (g : dt.SlotIx → A) :
              (dt.varRule zero one emb ruleG ruleX pgEntry pxEntry exitPh newSlot gateFlag accBit enterSt initSt postFold storeCarry i ρ).guard f g → (dt.varRule zero one emb ruleG ruleX pgEntry pxEntry exitPh newSlot gateFlag accBit enterSt initSt postFold storeCarry i ρ').guard f g → (dt.varRule zero one emb ruleG ruleX pgEntry pxEntry exitPh newSlot gateFlag accBit enterSt initSt postFold storeCarry i ρ).srcPh = (dt.varRule zero one emb ruleG ruleX pgEntry pxEntry exitPh newSlot gateFlag accBit enterSt initSt postFold storeCarry i ρ').srcPh → ρ = ρ'

              One variable's machinery separates in-shape: the checkpoints by their guards, the kits by their sep and exit_disjoint, the exit pairs by the phases the embedding keeps apart; the two abstract machineries by their parameters.

              Dependency graph