OAI/Computability/MaxCut/Machines/RawInitialMachineModel.lean

GitHub source file

85 declarations, 0 contain sorry, 0 declared as axioms

Actual execution of the raw initial graph machine from its standard input configuration to the first clause-loop guard. The unread clause bits are preserved verbatim, and all tape contents at the boundary are explicit.

  1. inductive OAI.MaxCutGames.Foundations.PCP.RawInitialMachineModel.Tape line 11
  2. abbrev OAI.MaxCutGames.Foundations.PCP.RawInitialMachineModel.Signs line 16
  3. abbrev OAI.MaxCutGames.Foundations.PCP.RawInitialMachineModel.State line 17
  4. abbrev OAI.MaxCutGames.Foundations.PCP.RawInitialMachineModel.Alphabet line 18
  5. inductive OAI.MaxCutGames.Foundations.PCP.RawInitialMachineModel.CopyPhase line 20
  6. inductive OAI.MaxCutGames.Foundations.PCP.RawInitialMachineModel.Label line 28
  7. def OAI.MaxCutGames.Foundations.PCP.RawInitialMachineModel.initialState line 42
  8. def OAI.MaxCutGames.Foundations.PCP.RawInitialMachineModel.stateKeys line 44
  9. theorem OAI.MaxCutGames.Foundations.PCP.RawInitialMachineModel.stateKeys_complete line 49
  10. def OAI.MaxCutGames.Foundations.PCP.RawInitialMachineModel.nameField line 55
  11. def OAI.MaxCutGames.Foundations.PCP.RawInitialMachineModel.copySource line 57
  12. def OAI.MaxCutGames.Foundations.PCP.RawInitialMachineModel.copyScale line 62
  13. def OAI.MaxCutGames.Foundations.PCP.RawInitialMachineModel.copyNext line 66
  14. def OAI.MaxCutGames.Foundations.PCP.RawInitialMachineModel.relationNext line 75
  15. def OAI.MaxCutGames.Foundations.PCP.RawInitialMachineModel.finalTape line 81
  16. def OAI.MaxCutGames.Foundations.PCP.RawInitialMachineModel.drain line 84
  17. def OAI.MaxCutGames.Foundations.PCP.RawInitialMachineModel.headerTape line 87
  18. def OAI.MaxCutGames.Foundations.PCP.RawInitialMachineModel.relationOutput line 89
  19. def OAI.MaxCutGames.Foundations.PCP.RawInitialMachineModel.program line 93
  20. def OAI.MaxCutGames.Foundations.PCP.RawInitialMachineModel.machine line 143
  21. def OAI.MaxCutGames.Foundations.PCP.RawInitialMachineStart.inputTapes line 166
  22. def OAI.MaxCutGames.Foundations.PCP.RawInitialMachineStart.firstTapes_inline_RawInitialMachineStart line 170
  23. def OAI.MaxCutGames.Foundations.PCP.RawInitialMachineStart.counterTapes line 175
  24. def OAI.MaxCutGames.Foundations.PCP.RawInitialMachineStart.headerTapes_inline_RawInitialMachineStart line 181
  25. def OAI.MaxCutGames.Foundations.PCP.RawInitialMachineStart.startTapes line 189

    Source documentation

    Complete machine frame at the first clause-loop guard.

    def startTapes (n m : ℕ) (clauseBits : List Bool) : Tape → List Bool
  | .input => clauseBits
  | .«variables» => encodeWord n
  | .counter => encodeWord m
  | .index => [false]
  | .reversed => (encodeWords [n + m + 1, 6 * m + 1]).reverse
  | _ => []
  26. theorem OAI.MaxCutGames.Foundations.PCP.RawInitialMachineStart.initList_eq line 197
  27. theorem OAI.MaxCutGames.Foundations.PCP.RawInitialMachineStart.trace_trans_inline_RawInitialMachineStart line 206
  28. theorem OAI.MaxCutGames.Foundations.PCP.RawInitialMachineStart.readCountersTrace line 211

    Source documentation

    The two actual header-field readers reach the prepared counter boundary.

    theorem readCountersTrace (n m : ℕ) (clauseBits : List Bool) :
    (MachineComposition.advance (TM2.step program))^[n + m + 4]
      (some (initList machine (encodeWords [n, m] ++ clauseBits))) =
      some ⟨some .scanN, initialState, counterTapes n m clauseBits⟩ := by
…

    Mentions: OAI.MaxCutGames.Foundations.PCP.RawInitialMachineStart.counterTapes

  29. theorem OAI.MaxCutGames.Foundations.PCP.RawInitialMachineStart.headersTrace line 245

    Source documentation

    Instantiation of the checked arithmetic phase in the actual global program.

    theorem headersTrace (n m : ℕ) (clauseBits : List Bool) :
    (MachineComposition.advance (TM2.step program))^[2 * n + 4 * m + 8]
      (some ⟨some .scanN, initialState, counterTapes n m clauseBits⟩) =
      some ⟨some .initializeIndex, initialState, headerTapes_inline_RawInitialMachineStart n m clauseBits⟩ := by
…

    Mentions: OAI.MaxCutGames.Foundations.PCP.RawInitialMachineStart.counterTapes, OAI.MaxCutGames.Foundations.PCP.RawInitialMachineStart.headerTapes_inline_RawInitialMachineStart

  30. theorem OAI.MaxCutGames.Foundations.PCP.RawInitialMachineStart.initializeIndexTrace line 264
  31. theorem OAI.MaxCutGames.Foundations.PCP.RawInitialMachineStart.startTrace line 277

    Source documentation

    Exact startup trace for arbitrary encoded clause-tail data.

    theorem startTrace (n m : ℕ) (clauseBits : List Bool) :
    (MachineComposition.advance (TM2.step program))^[3 * n + 5 * m + 13]
      (some (initList machine (encodeWords [n, m] ++ clauseBits))) =
      some ⟨some .guard, initialState, startTapes n m clauseBits⟩ := by
…

    Mentions: OAI.MaxCutGames.Foundations.PCP.RawInitialMachineStart.startTapes

  32. theorem OAI.MaxCutGames.Foundations.PCP.RawInitialMachineStart.formulaStartTrace line 288

    Source documentation

    Startup from the actual serialized CNF, with its untouched clause tail.

    theorem formulaStartTrace (F : Target.Formula) :
    (MachineComposition.advance (TM2.step program))^[
        3 * F.«variables» + 5 * F.clauses.length + 13]
      (some (initList machine (formulaBits F))) =
      some ⟨some .guard, initialState,
        startTapes F.«variables» F.clauses.length
          (encodeWords (F.clauses.flatMap clauseWords))⟩ := by
…

    Mentions: OAI.MaxCutGames.Foundations.Target.Formula, OAI.MaxCutGames.Foundations.PCP.RawInitialMachineStart.startTapes

  33. def OAI.MaxCutGames.Foundations.PCP.RawInitialMachineStart.startInTime line 298
  34. def OAI.MaxCutGames.Foundations.PCP.RawInitialMachineStart.formulaStartInTime line 307
  35. def OAI.MaxCutGames.Foundations.PCP.RawInitialMachineLoopData.clauseInput line 326
  36. theorem OAI.MaxCutGames.Foundations.PCP.RawInitialMachineLoopData.clauseInput_nil line 329
  37. theorem OAI.MaxCutGames.Foundations.PCP.RawInitialMachineLoopData.clauseInput_cons line 331
  38. def OAI.MaxCutGames.Foundations.PCP.RawInitialMachineLoopData.clauseOutput line 335
  39. theorem OAI.MaxCutGames.Foundations.PCP.RawInitialMachineLoopData.mapIdx_ofFn_inline_RawInitialMachineLoopData line 339
  40. theorem OAI.MaxCutGames.Foundations.PCP.RawInitialMachineLoopData.clauseOutput_nil line 345
  41. theorem OAI.MaxCutGames.Foundations.PCP.RawInitialMachineLoopData.clauseOutput_cons line 347
  42. theorem OAI.MaxCutGames.Foundations.PCP.RawInitialMachineLoopData.clauseOutput_numbered line 354
  43. theorem OAI.MaxCutGames.Foundations.PCP.RawInitialMachineLoopData.tableWords_decomposition line 364
  44. def OAI.MaxCutGames.Foundations.PCP.RawInitialMachineLoopData.loopTapes line 371
  45. theorem OAI.MaxCutGames.Foundations.PCP.RawInitialMachineLoopData.startTapes_eq line 379
  46. theorem OAI.MaxCutGames.Foundations.PCP.RawInitialMachineLoopData.decrement_counter line 385
  47. theorem OAI.MaxCutGames.Foundations.PCP.RawInitialMachineLoopData.increment_index line 391
  48. theorem OAI.MaxCutGames.Foundations.PCP.RawInitialMachinePhases.copySource_ne_scratch line 405
  49. theorem OAI.MaxCutGames.Foundations.PCP.RawInitialMachinePhases.copySource_ne_reversed line 408
  50. def OAI.MaxCutGames.Foundations.PCP.RawInitialMachinePhases.copyInTime line 411
  51. def OAI.MaxCutGames.Foundations.PCP.RawInitialMachinePhases.relationInTime line 426
  52. theorem OAI.MaxCutGames.Foundations.PCP.RawInitialMachinePhases.bitWord_head_inline_RawInitialMachinePhases line 439
  53. theorem OAI.MaxCutGames.Foundations.PCP.RawInitialMachinePhases.loadSigns_step line 443
  54. def OAI.MaxCutGames.Foundations.PCP.RawInitialMachinePhases.loadSignsInTime line 452
  55. def OAI.MaxCutGames.Foundations.PCP.RawInitialMachinePhases.cleanupFieldInTime line 463
  56. def OAI.MaxCutGames.Foundations.PCP.RawInitialMachinePhases.cleanupFinalInTime line 471
  57. def OAI.MaxCutGames.Foundations.PCP.RawInitialMachineReadClause.fieldValue line 492

    Source documentation

    The six actual serialized fields, in name/sign/name/sign/name/sign order.

    def fieldValue {n : ℕ} (c : Target.Clause n) (j : Fin 6) : ℕ :=
…

    Mentions: OAI.MaxCutGames.Foundations.Target.Clause

  58. def OAI.MaxCutGames.Foundations.PCP.RawInitialMachineReadClause.recordTapes line 498

    Source documentation

    Full caller frame after the clause fields have been consumed.

    def recordTapes {n : ℕ} (base : Tape → List Bool) (c : Target.Clause n)
    (suffix : List Bool) : Tape → List Bool
  | .input => suffix
  | .field j => encodeWord (fieldValue c j)
  | k => base k

    Mentions: OAI.MaxCutGames.Foundations.Target.Clause, OAI.MaxCutGames.Foundations.PCP.RawInitialMachineReadClause.fieldValue

  59. theorem OAI.MaxCutGames.Foundations.PCP.RawInitialMachineReadClause.recordTapes_input line 504
  60. theorem OAI.MaxCutGames.Foundations.PCP.RawInitialMachineReadClause.recordTapes_field line 508
  61. theorem OAI.MaxCutGames.Foundations.PCP.RawInitialMachineReadClause.recordTapes_other line 512
  62. theorem OAI.MaxCutGames.Foundations.PCP.RawInitialMachineReadClause.recordTapes_name line 520
  63. theorem OAI.MaxCutGames.Foundations.PCP.RawInitialMachineReadClause.trace_trans_inline_RawInitialMachineReadClause line 526
  64. theorem OAI.MaxCutGames.Foundations.PCP.RawInitialMachineReadClause.fieldsTrace line 531

    Source documentation

    Six actual field routines, stopping directly at the global sign loader.

    theorem fieldsTrace {n : ℕ} (base : Tape → List Bool) (c : Target.Clause n)
    (suffix : List Bool)
    (hinput : base .input = encodeWords (Complexity.clauseWords c) ++ suffix)
    (hempty : ∀ j, base (.field j) = []) (state : State) :
    (MachineComposition.advance (TM2.step program))^[
        (encodeWords (Complexity.clauseWords c)).length + 6]
      (some ⟨some (.fieldStart 0), state, base⟩) =
      some ⟨some .loadSigns, (state.1, none), recordTapes base c suffix⟩ := by
…

    Mentions: OAI.MaxCutGames.Foundations.Target.Clause, OAI.MaxCutGames.Foundations.Complexity.clauseWords, OAI.MaxCutGames.Foundations.PCP.RawInitialMachineReadClause.recordTapes

  65. theorem OAI.MaxCutGames.Foundations.PCP.RawInitialMachineReadClause.readClauseTrace line 627
  66. def OAI.MaxCutGames.Foundations.PCP.RawInitialMachineReadClause.readClauseInTime line 647
  67. abbrev OAI.MaxCutGames.Foundations.PCP.RawInitialMachineRows.advance_inline_RawInitialMachineRows line 671
  68. def OAI.MaxCutGames.Foundations.PCP.RawInitialMachineRows.outputTapes line 673
  69. theorem OAI.MaxCutGames.Foundations.PCP.RawInitialMachineRows.outputTapes_reversed line 676
  70. theorem OAI.MaxCutGames.Foundations.PCP.RawInitialMachineRows.outputTapes_other line 679
  71. theorem OAI.MaxCutGames.Foundations.PCP.RawInitialMachineRows.outputTapes_twice line 683
  72. theorem OAI.MaxCutGames.Foundations.PCP.RawInitialMachineRows.trace_trans_inline_RawInitialMachineRows line 690
  73. theorem OAI.MaxCutGames.Foundations.PCP.RawInitialMachineRows.copyTrace_inline_RawInitialMachineRows line 694
  74. theorem OAI.MaxCutGames.Foundations.PCP.RawInitialMachineRows.closeTailTrace_inline_RawInitialMachineRows line 702
  75. theorem OAI.MaxCutGames.Foundations.PCP.RawInitialMachineRows.closeReverseTrace_inline_RawInitialMachineRows line 710
  76. theorem OAI.MaxCutGames.Foundations.PCP.RawInitialMachineRows.reverse_encodeWord_add_inline_RawInitialMachineRows line 720
  77. def OAI.MaxCutGames.Foundations.PCP.RawInitialMachineRows.rowEndBits line 726
  78. theorem OAI.MaxCutGames.Foundations.PCP.RawInitialMachineRows.rowEndTrace_inline_RawInitialMachineRows line 730
  79. theorem OAI.MaxCutGames.Foundations.PCP.RawInitialMachineRows.rowEndBits_append_inline_RawInitialMachineRows line 762
  80. theorem OAI.MaxCutGames.Foundations.PCP.RawInitialMachineRows.falseRowTrace line 771
  81. theorem OAI.MaxCutGames.Foundations.PCP.RawInitialMachineRows.trueRowTrace line 809
  82. def OAI.MaxCutGames.Foundations.PCP.RawInitialMachineRows.pairWords line 838
  83. theorem OAI.MaxCutGames.Foundations.PCP.RawInitialMachineRows.pairTrace line 843
  84. theorem OAI.MaxCutGames.Foundations.PCP.RawInitialMachineRows.rowsTrace line 871

    Source documentation

    Exact execution of all six incidence rows. Relation tables stay symbolic; no entry is discarded and every non-output tape is preserved.

    theorem rowsTrace (base : Tape → List Bool) (n i : ℕ)
    (names : RawInitialRows.Names) (signs : Signs)
    (hvariables : base .«variables» = encodeWord n) (hindex : base .index = encodeWord i)
    (hname0 : base (.field 0) = encodeWord names.1)
    (hname2 : base (.field 2) = encodeWord names.2.1)
    (hname4 : base (.field 4) = encodeWord names.2.2)
    (hscratch : base .scratch = []) :
    advance_inline_RawInitialMachineRows^[6 * n + 18 * i + 2 * (names.1 + names.2.1 + names.2.2) + 48]
      (some ⟨some (.scan (.tailVariables 0)), (signs, none), base⟩) =
      some ⟨some (.cleanupField 0), (signs, none),
        outputTapes base (encodeWords (RawInitialRows.clauseWords n i names signs)).reverse⟩ := by
…

    Mentions: OAI.MaxCutGames.Foundations.PCP.RawInitialRows.Names, OAI.MaxCutGames.Foundations.PCP.RawInitialMachineRows.advance_inline_RawInitialMachineRows, OAI.MaxCutGames.Foundations.PCP.RawInitialMachineRows.outputTapes, OAI.MaxCutGames.Foundations.PCP.RawInitialRows.clauseWords

  85. def OAI.MaxCutGames.Foundations.PCP.RawInitialMachineRows.rowsInTime line 918