OAI/Computability/MaxCut/Machines/Body.lean

GitHub source file

60 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.MaxCutGames.Foundations.PCP.AlphabetTable.Body.bodyTime line 20
  2. structure OAI.MaxCutGames.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.MaxCutGames.Foundations.PCP.GenericGraphTables.Table, OAI.MaxCutGames.Foundations.PCP.GenericGraphTables.RelationTable

  3. def OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Body.guardTapes line 34
  4. def OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Body.parsedTapes line 38
  5. def OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Body.workingTapes line 43
  6. def OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Body.emittedTapes line 47
  7. def OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Body.clearFieldsTapes line 52
  8. def OAI.MaxCutGames.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.MaxCutGames.Foundations.PCP.GenericGraphTables.Table

  9. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Body.workingTapes_other_inline_Body line 61
  10. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Body.workingTapes_counter_inline_Body line 71
  11. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Body.workingTapes_cursor_inline_Body line 77
  12. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Body.workingTapes_tail_inline_Body line 83
  13. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Body.workingTapes_reverse_inline_Body line 89
  14. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Body.workingTapes_head_inline_Body line 95
  15. def OAI.MaxCutGames.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.MaxCutGames.Foundations.PCP.AlphabetTable.Driver.program, OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Body.clearFieldsTapes

  16. def OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Body.incrementInTime line 125
  17. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Body.emitterView_at_inline_Body line 140
  18. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Body.context_rowState_inline_Body line 150
  19. def OAI.MaxCutGames.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.MaxCutGames.Foundations.PCP.GenericGraphTables.Table, OAI.MaxCutGames.Foundations.PCP.AlphabetTable.EmitRows.rowValues, OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Driver.program, OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Driver.rowEntry, OAI.MaxCutGames.Foundations.PCP.AlphabetTable.CompareLoop.rowState, OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Emitter.resultTapes, OAI.MaxCutGames.Foundations.PCP.AlphabetTable.EmitRows.blockWords, OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Enumeration.localCount, OAI.MaxCutGames.Foundations.PCP.AlphabetTable.LoopState.inputBits

  20. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Body.result_ready_inline_Body line 198
  21. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Body.workingOperands_inline_Body line 209
  22. def OAI.MaxCutGames.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.MaxCutGames.Foundations.PCP.GenericGraphTables.Table, OAI.MaxCutGames.Foundations.PCP.AlphabetTable.LoopState.Ready, OAI.MaxCutGames.Foundations.PCP.GenericGraphTables.RelationTable, OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Body.RowStepResult

  23. def OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Initialization.inputTapes line 351
  24. def OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Initialization.rowsBits line 355
  25. def OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Initialization.headerBits line 358
  26. def OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Initialization.setupTapes line 362
  27. def OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Initialization.loopTapes line 371

    Source documentation

    Complete initial loop state. Every auxiliary tape not listed here is empty.

    def loopTapes (input : GenericGraphTables.Table q) : Tape → List Bool
  | .original => GenericGraphTables.tableBits input
  | .cursor => rowsBits input
  | .vertices => encodeWord input.vertices
  | .darts | .counter => encodeWord input.darts
  | .edge => encodeWord 0
  | .reversed => (headerBits input).reverse
  | _ => []

    Mentions: OAI.MaxCutGames.Foundations.PCP.GenericGraphTables.Table, OAI.MaxCutGames.Foundations.PCP.GenericGraphTables.tableBits, OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Initialization.rowsBits, OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Initialization.headerBits

  28. def OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Initialization.loopStart line 380
  29. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Initialization.setupResult_eq line 384
  30. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Initialization.headerResult_eq line 390
  31. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Initialization.machineInitial_eq line 395
  32. def OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Initialization.setupInTime line 406

    Source documentation

    The driver executes its actual setup statements from its actual input configuration.

    def setupInTime (input : GenericGraphTables.Table q) :
    StateTransition.EvalsToInTime (TM2.step (Driver.program q))
      (initList (Driver.machine q) (GenericGraphTables.tableBits input))
      (some ⟨some (Driver.headerEntry q), initial q, setupTapes input⟩)
      (6 * (GenericGraphTables.tableBits input).length + 11) := by
…

    Mentions: OAI.MaxCutGames.Foundations.PCP.GenericGraphTables.Table, OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Driver.program, OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Driver.machine, OAI.MaxCutGames.Foundations.PCP.GenericGraphTables.tableBits, OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Driver.headerEntry, OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Initialization.setupTapes

  33. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Initialization.headerView_at_inline_Initialization line 425
  34. def OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Initialization.headerInTime line 437

    Source documentation

    No header execution is assumed: the checked template is instantiated at the concrete driver labels and transported through the finite state layout.

    def headerInTime (input : GenericGraphTables.Table q) :
    StateTransition.EvalsToInTime (TM2.step (Driver.program q))
      ⟨some (Driver.headerEntry q), initial q, setupTapes input⟩
      (some (loopStart input))
      (7 * (3 * ((GenericGraphTables.tableBits input).length + 1) + 3) + 1) := by
…

    Mentions: OAI.MaxCutGames.Foundations.PCP.GenericGraphTables.Table, OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Driver.program, OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Driver.headerEntry, OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Initialization.setupTapes, OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Initialization.loopStart, OAI.MaxCutGames.Foundations.PCP.GenericGraphTables.tableBits

  35. def OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Initialization.time line 475
  36. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Initialization.time_eq line 477
  37. def OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Initialization.initializeInTime line 483

    Source documentation

    Actual initialization of the complete finite driver, ending at its first guard with the exact input, counter, cursor, index, and reversed headers.

    def initializeInTime (input : GenericGraphTables.Table q) :
    StateTransition.EvalsToInTime (TM2.step (Driver.program q))
      (initList (Driver.machine q) (GenericGraphTables.tableBits input))
      (some (loopStart input)) (time (GenericGraphTables.tableBits input).length) := by
…

    Mentions: OAI.MaxCutGames.Foundations.PCP.GenericGraphTables.Table, OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Driver.program, OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Driver.machine, OAI.MaxCutGames.Foundations.PCP.GenericGraphTables.tableBits, OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Initialization.loopStart, OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Initialization.time

  38. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.LoopInitialization.initialization_ready line 509

    Source documentation

    The actual initial loop tapes contain the complete unread input rows and exactly the two output headers in reverse order on the accumulation tape.

    theorem initialization_ready {q : Nat} (input : GenericGraphTables.Table q) :
    Ready input 0 (Initialization.loopTapes input) where
…

    Mentions: OAI.MaxCutGames.Foundations.PCP.GenericGraphTables.Table, OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Initialization.loopTapes

  39. def OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Loop.zeroGuardInTime line 545

    Source documentation

    The zero guard preserves all tapes, resets its temporary register, and enters the actual driver's output-reversal phase in one transition.

    def zeroGuardInTime (input : GenericGraphTables.Table q) (base : Tape → List Bool)
    (ready : LoopState.Ready input input.darts base)
    (relation : GenericGraphTables.RelationTable q) (flag : Bool) :
    StateTransition.EvalsToInTime (TM2.step (Driver.program q))
      ⟨some .guard, normal relation flag, base⟩
      (some ⟨some .reverseOutput, normal relation flag, base⟩) 1 := by
…

    Mentions: OAI.MaxCutGames.Foundations.PCP.GenericGraphTables.Table, OAI.MaxCutGames.Foundations.PCP.AlphabetTable.LoopState.Ready, OAI.MaxCutGames.Foundations.PCP.GenericGraphTables.RelationTable, OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Driver.program

  40. structure OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Loop.LoopResult line 560

    Source documentation

    Concrete final configuration and full remaining-loop execution.

    structure LoopResult (input : GenericGraphTables.Table q) (e remaining : Nat)
    (base : Tape → List Bool) (oldRelation : GenericGraphTables.RelationTable q)
    (oldFlag : Bool) where
…

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

  41. def OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Loop.runRemaining line 572
  42. def OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Loop.prefixTime line 606

    Source documentation

    A quadratic prefix allowance because the number of original rows is at most the length of their fully encoded input table.

    def prefixTime (q N : Nat) : Nat :=
…
  43. structure OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Loop.PrefixResult line 623

    Source documentation

    Actual initialization followed by every row, ending just before reversal.

    structure PrefixResult (input : GenericGraphTables.Table q) where
…

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

  44. def OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Loop.runPrefix line 635

    Source documentation

    No initialization or row trace is assumed: both are instantiated at this actual finite driver and this input, then composed.

    def runPrefix (input : GenericGraphTables.Table q) : PrefixResult input := by
…

    Mentions: OAI.MaxCutGames.Foundations.PCP.GenericGraphTables.Table, OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Loop.PrefixResult

  45. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Loop.PrefixResult.reversed line 658
  46. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Loop.PrefixResult.output line 662
  47. def OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Finish.afterReversal line 678
  48. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Finish.afterReversal_output line 681
  49. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Finish.afterReversal_reversed line 685
  50. def OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Finish.finishBudget line 689
  51. def OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Finish.reverseInTime line 693

    Source documentation

    The actual driver's reversal loop enters its first cleanup label.

    def reverseInTime (q : Nat) (base : Tape → List Bool) (word : List Bool)
    (state : State q) (hreversed : base .reversed = word.reverse)
    (houtput : base .output = []) :
    StateTransition.EvalsToInTime (Driver.machine q).step
      ⟨some .reverseOutput, state, base⟩
      (some ⟨some (.cleanup 0), (state.1, none), afterReversal base word⟩)
      (word.length + 1) := by
…

    Mentions: OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Driver.machine, OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Finish.afterReversal

  52. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Finish.cleared_eq_haltList line 707
  53. def OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Finish.cleanupInTime line 716

    Source documentation

    All remaining driver stacks are actually popped, and the exact initial finite state is restored before the halting configuration is reached.

    def cleanupInTime (q : Nat) (base : Tape → List Bool) (state : State q) :
    StateTransition.EvalsToInTime (Driver.machine q).step
      ⟨some (.cleanup 0), state, base⟩
      (some (haltList (Driver.machine q) (base .output)))
      ((∑ i : Fin 15, (base (cleanupPorts i)).length) + 16) := by
…

    Mentions: OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Driver.machine

  54. def OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Finish.finishInTime line 732
  55. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Finish.afterReversal_selected_length_le line 753
  56. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Finish.stackLength_after_prefix line 761

    Source documentation

    Every stack bound here is derived from the actual preceding driver trace.

    theorem stackLength_after_prefix (q : Nat) (input : List Bool)
    (base : Tape → List Bool) (state : State q) (budget : Nat)
    (prefixRun : StateTransition.EvalsToInTime (Driver.machine q).step
      (initList (Driver.machine q) input) (some ⟨some .reverseOutput, state, base⟩) budget)
    (k : Tape) :
    (base k).length ≤ input.length + budget * Runtime.programPushBound (Driver.machine q) := by
…

    Mentions: OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Driver.machine

  57. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Finish.finishBudget_le_of_prefix line 773
  58. def OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Finish.completedPolynomial line 797

    Source documentation

    A polynomial time allowance for the whole prefixRun followed by actual reversal and cleanup. The fixed push bound belongs to the concrete driver.

    noncomputable def completedPolynomial (q : Nat) (prefixTime : Polynomial Nat) : Polynomial Nat :=
…
  59. def OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Finish.finishAfterPrefix line 802
  60. def OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Finish.finishAfterPolynomialPrefix line 818