OAI/Computability/UniqueGames/Machines/MachineSubroutineLemmas.lean

GitHub source file

105 declarations, 0 contain sorry, 0 declared as axioms

Concrete finite-alphabet serialization primitives. A natural word n is n one-bits followed by a zero delimiter. These are size and decoding theorems, not running-time certificates. In particular, output length is never called runtime.

  1. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineSubroutine.label line 15
  2. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineSubroutine.configuration line 19
  3. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineSubroutine.statement line 22
  4. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineSubroutine.stepAux_simulation line 36
  5. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineSubroutine.step_simulation line 57
  6. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineSubroutine.trace line 73
  7. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineSubroutine.execution line 83
  8. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineStateFrame.frameStatement line 106

    Source documentation

    Same code and stacks, with an untouched caller-register component.

    def frameStatement : TM2.Stmt Γ Λ σ → TM2.Stmt Γ Λ (σ × τ)
  | .push k f next => .push k (fun state => f state.1) (frameStatement next)
  | .peek k f next => .peek k (fun state bit => (f state.1 bit, state.2))
      (frameStatement next)
  | .pop k f next => .pop k (fun state bit => (f state.1 bit, state.2))
      (frameStatement next)
  | .load f next => .load (fun state => (f state.1, state.2)) (frameStatement next)
  | .branch f yes no => .branch (fun state => f state.1)
      (frameStatement yes) (frameStatement no)
  | .goto f => .goto (fun state => f state.1)
  | .halt => .halt
  9. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineStateFrame.frameConfiguration line 118
  10. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineStateFrame.frameProgram line 121
  11. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineStateFrame.frameConfiguration_state line 124
  12. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineStateFrame.frameConfiguration_metadata line 127
  13. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineStateFrame.frameConfiguration_tapes line 130
  14. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineStateFrame.frameStatement_pushBound line 133
  15. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineStateFrame.statement line 138

    Source documentation

    Optional continuation and labels use the existing subroutine semantics.

    def statement (labels : Λ → Λ') (exit : Option Λ') (q : TM2.Stmt Γ Λ σ) :
    TM2.Stmt Γ Λ' (σ × τ) :=
…
  16. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineStateFrame.configuration line 142
  17. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineStateFrame.configuration_state line 146
  18. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineStateFrame.configuration_metadata line 150
  19. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineStateFrame.configuration_tapes line 154
  20. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineStateFrame.statement_pushBound line 158
  21. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineStateFrame.frame_stepAux line 168
  22. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineStateFrame.frame_step line 190

    Source documentation

    This identity also covers the final halted configuration.

    theorem frame_step (source : Λ → TM2.Stmt Γ Λ σ) (ambient : τ)
    (c : TM2.Cfg Γ Λ σ) :
    TM2.step (frameProgram source) (frameConfiguration ambient c) =
      (TM2.step source c).map (frameConfiguration ambient) := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineStateFrame.frameProgram, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineStateFrame.frameConfiguration

  23. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineStateFrame.frame_advance line 202
  24. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineStateFrame.frame_iterate line 211
  25. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineStateFrame.frameExecution line 224

    Source documentation

    Actual execution with the same step count, budget, and tapes.

    def frameExecution (source : Λ → TM2.Stmt Γ Λ σ) (ambient : τ)
    {start : TM2.Cfg Γ Λ σ} {finish : Option (TM2.Cfg Γ Λ σ)} {budget : ℕ}
    (run : StateTransition.EvalsToInTime (TM2.step source) start finish budget) :
    StateTransition.EvalsToInTime (TM2.step (frameProgram source))
      (frameConfiguration ambient start) (finish.map (frameConfiguration ambient)) budget where
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineStateFrame.frameProgram, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineStateFrame.frameConfiguration

  26. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineStateFrame.frameExecution_steps line 238
  27. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineStateFrame.stepAux_simulation line 243
  28. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineStateFrame.step_simulation line 250
  29. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineStateFrame.trace line 263
  30. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineStateFrame.execution line 274
  31. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineStateFrame.execution_steps line 284
  32. def OAI.UniqueGamesTheorem.Foundations.Complexity.decodeWordsAux line 305
  33. def OAI.UniqueGamesTheorem.Foundations.Complexity.decodeWords line 311
  34. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.decodeWordsAux_word line 313
  35. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.decodeWords_encodeWords line 323
  36. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.encodeWords_injective line 331
  37. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.encodeWord_length line 336
  38. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.encodeWords_append line 339
  39. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.encodeWords_length line 345
  40. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.encodeWords_length_le line 351
  41. def OAI.UniqueGamesTheorem.Foundations.Complexity.literalWords line 365
  42. def OAI.UniqueGamesTheorem.Foundations.Complexity.clauseWords line 368
  43. def OAI.UniqueGamesTheorem.Foundations.Complexity.formulaWords line 371
  44. def OAI.UniqueGamesTheorem.Foundations.Complexity.formulaBits line 374
  45. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.literalWords_length line 376
  46. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.clauseWords_length line 379
  47. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.clausesWords_length line 382
  48. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.formulaWords_length line 391
  49. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.literalBits_length_le line 396
  50. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.clauseBits_length_le line 401
  51. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.clausesBits_length_le line 409
  52. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.formulaBits_length_le line 419
  53. def OAI.UniqueGamesTheorem.Foundations.Complexity.parseLiteral line 441
  54. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.parseLiteral_encoded line 450
  55. def OAI.UniqueGamesTheorem.Foundations.Complexity.parseClause line 456
  56. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.clause_three_entries line 462
  57. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.parseClause_encoded line 469
  58. def OAI.UniqueGamesTheorem.Foundations.Complexity.parseClauses line 474
  59. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.parseClauses_encoded line 481
  60. def OAI.UniqueGamesTheorem.Foundations.Complexity.decodeFormulaWords line 488
  61. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.decodeFormulaWords_encoded line 494
  62. def OAI.UniqueGamesTheorem.Foundations.Complexity.decodeFormulaBits line 502
  63. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.decodeFormulaBits_encoded line 505
  64. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.formulaBits_injective line 509
  65. def OAI.UniqueGamesTheorem.Foundations.Complexity.parseLabel line 528
  66. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.parseLabel_value line 531
  67. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.parseLabels_values line 534
  68. def OAI.UniqueGamesTheorem.Foundations.Complexity.parseImages line 540
  69. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.parseImages_values line 546
  70. def OAI.UniqueGamesTheorem.Foundations.Complexity.findPreimage line 553
  71. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.findPreimage_permutation line 556
  72. def OAI.UniqueGamesTheorem.Foundations.Complexity.searchedInverse line 575
  73. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.searchedInverse_permutation line 578
  74. def OAI.UniqueGamesTheorem.Foundations.Complexity.parsePermutation line 584
  75. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.parsePermutation_encoded line 593
  76. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.tableWords_length line 600
  77. def OAI.UniqueGamesTheorem.Foundations.Complexity.parseConstraint line 603
  78. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.parseConstraint_encoded line 612
  79. def OAI.UniqueGamesTheorem.Foundations.Complexity.parseConstraints line 621
  80. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.parseConstraints_encoded line 629
  81. def OAI.UniqueGamesTheorem.Foundations.Complexity.decodeGameWords line 638
  82. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.decodeGameWords_encoded line 648
  83. def OAI.UniqueGamesTheorem.Foundations.Complexity.decodeGameBits line 656
  84. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.decodeGameBits_encoded line 659
  85. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.gameBits_injective line 663
  86. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.constraintWords_length line 668
  87. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.constraintsWords_length line 671
  88. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.gameWords_length line 680
  89. def OAI.UniqueGamesTheorem.Explicit.MachineSingleOrbitCodec.doubleConstraint line 699
  90. def OAI.UniqueGamesTheorem.Explicit.MachineSingleOrbitCodec.doubleInstance line 704
  91. def OAI.UniqueGamesTheorem.Explicit.MachineSingleOrbitCodec.rowBits line 709
  92. def OAI.UniqueGamesTheorem.Explicit.MachineSingleOrbitCodec.doubledRowBits line 712
  93. def OAI.UniqueGamesTheorem.Explicit.MachineSingleOrbitCodec.rowsBits line 715
  94. def OAI.UniqueGamesTheorem.Explicit.MachineSingleOrbitCodec.doubledRowsBits line 718
  95. theorem OAI.UniqueGamesTheorem.Explicit.MachineSingleOrbitCodec.rowBits_eq line 721
  96. theorem OAI.UniqueGamesTheorem.Explicit.MachineSingleOrbitCodec.doubledRowBits_eq line 726
  97. theorem OAI.UniqueGamesTheorem.Explicit.MachineSingleOrbitCodec.rowsBits_nil line 731
  98. theorem OAI.UniqueGamesTheorem.Explicit.MachineSingleOrbitCodec.doubledRowsBits_nil line 732
  99. theorem OAI.UniqueGamesTheorem.Explicit.MachineSingleOrbitCodec.rowsBits_cons line 735
  100. theorem OAI.UniqueGamesTheorem.Explicit.MachineSingleOrbitCodec.doubledRowsBits_cons line 739
  101. theorem OAI.UniqueGamesTheorem.Explicit.MachineSingleOrbitCodec.gameBits_eq line 744
  102. theorem OAI.UniqueGamesTheorem.Explicit.MachineSingleOrbitCodec.doubled_gameBits_eq line 749
  103. theorem OAI.UniqueGamesTheorem.Explicit.MachineSingleOrbitCodec.input_length_eq line 755
  104. theorem OAI.UniqueGamesTheorem.Explicit.MachineSingleOrbitCodec.vertices_le_input_length line 763
  105. theorem OAI.UniqueGamesTheorem.Explicit.MachineSingleOrbitCodec.rows_le_input_length line 768