OAI/Computability/UniqueGames/PCP/Body.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

One actual iteration of the alphabet-table driver. The positive unary guard, row parser, preserving head lookup, comparison, finite emission plan, three drains, and unary index increment all execute inside Driver.program.

  1. def OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Body.bodyTime line 20
  2. structure OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Body.RowStepResult line 24

    Source documentation

    An execution witness, with the exact invariant needed by the next guard.

    structure RowStepResult (input : GenericGraphTables.Table q) (e : Fin input.darts)
    (base : Tape → List Bool) (oldRelation : GenericGraphTables.RelationTable q)
    (oldFlag : Bool) where
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.GenericGraphTables.Table, OAI.UniqueGamesTheorem.Foundations.PCP.GenericGraphTables.RelationTable

  3. def OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Body.guardTapes line 34
  4. def OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Body.parsedTapes line 38
  5. def OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Body.workingTapes line 43
  6. def OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Body.emittedTapes line 47
  7. def OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Body.clearFieldsTapes line 52
  8. def OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Body.resultTapes line 56

    Source documentation

    Exact final tapes, including the lookup's retained scan suffixes.

    def resultTapes (input : GenericGraphTables.Table q) (e : Fin input.darts)
    (base : Tape → List Bool) : Tape → List Bool :=
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.GenericGraphTables.Table

  9. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Body.workingTapes_other line 61
  10. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Body.workingTapes_counter line 71
  11. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Body.workingTapes_cursor line 77
  12. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Body.workingTapes_tail line 83
  13. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Body.workingTapes_reverse line 89
  14. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Body.workingTapes_head line 95
  15. def OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Body.clearFieldsInTime line 103

    Source documentation

    The three cleanup phases are actual drains in the concrete program.

    def clearFieldsInTime (base : Tape → List Bool) (ambient : Ambient q) :
    StateTransition.EvalsToInTime (TM2.step (Driver.program q))
      ⟨some (.clearField 0), (ambient, none), base⟩
      (some ⟨some .increment, (ambient, none), clearFieldsTapes base⟩)
      ((base .tail).length + (base .reverseIndex).length + (base .head).length + 3) := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Driver.program, OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Body.clearFieldsTapes

  16. def OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Body.incrementInTime line 125
  17. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Body.emitterView_at line 140
  18. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Body.context_rowState line 150
  19. def OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Body.emitInTime line 160

    Source documentation

    Execute the actual emitted row block through the finite register equivalence.

    def emitInTime (input : GenericGraphTables.Table q) (e : Fin input.darts)
    (base : Tape → List Bool)
    (operands : ∀ i, base (rowSources i) = encodeWord (EmitRows.rowValues input e i))
    (scratchEmpty : base .scratch = []) :
    StateTransition.EvalsToInTime (TM2.step (Driver.program q))
      ⟨some (Driver.rowEntry q), CompareLoop.rowState input e, base⟩
      (some ⟨some (.clearField 0), CompareLoop.rowState input e,
        Emitter.resultTapes .reversed base (encodeWords (EmitRows.blockWords input e))⟩)
      (Enumeration.localCount q * (6 * (2 * 4104)) *
        (3 * ((LoopState.inputBits input).length + 1) + 3) + 1) := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.GenericGraphTables.Table, OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.EmitRows.rowValues, OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Driver.program, OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Driver.rowEntry, OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.CompareLoop.rowState, OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Emitter.resultTapes, OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.EmitRows.blockWords, OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Enumeration.localCount, OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.LoopState.inputBits

  20. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Body.result_ready line 198
  21. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Body.workingOperands line 209
  22. def OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Body.rowStep line 221

    Source documentation

    Execute a whole row iteration from the exact guard invariant. Every run below is obtained from the concrete code at its component labels.

    def rowStep (input : GenericGraphTables.Table q) (e : Fin input.darts)
    (base : Tape → List Bool) (ready : LoopState.Ready input e.val base)
    (oldRelation : GenericGraphTables.RelationTable q) (oldFlag : Bool) :
    RowStepResult input e base oldRelation oldFlag := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.GenericGraphTables.Table, OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.LoopState.Ready, OAI.UniqueGamesTheorem.Foundations.PCP.GenericGraphTables.RelationTable, OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Body.RowStepResult