OAI/Computability/UniqueGames/Machines/MachineRepeat.lean

GitHub source file

51 declarations, 0 contain sorry, 0 declared as axioms

A fixed finite TM2 interpreter for a unary number of runs of a fixed certified machine. The counter is data on a separate tape. Every body run is lifted from an actual TM2OutputsInTime witness, and all transfers are executed by the checked finite transfer loops.

  1. inductive OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRepeat.ExtraTape line 15
  2. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRepeat.ExtraTape.enumList line 19
  3. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRepeat.ExtraTape.enumList_getElem?_ctorIdx_eq line 21
  4. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRepeat.ExtraTape.enumList_nodup line 25
  5. instance OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRepeat.(instance at line 27) line 27
  6. inductive OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRepeat.Phase line 30
  7. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRepeat.Phase.enumList line 34
  8. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRepeat.Phase.enumList_getElem?_ctorIdx_eq line 37
  9. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRepeat.Phase.enumList_nodup line 41
  10. instance OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRepeat.(instance at line 43) line 43
  11. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRepeat.Tape line 47
  12. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRepeat.Symbols line 48
  13. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRepeat.Label line 49
  14. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRepeat.State line 50
  15. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRepeat.extraTapes line 52
  16. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRepeat.auxProgram line 58
  17. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRepeat.program line 79
  18. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRepeat.machine line 83
  19. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRepeat.inputTapes line 101
  20. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRepeat.inputTapes_input line 104
  21. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRepeat.inputTapes_counter line 108
  22. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRepeat.inputConfig line 111
  23. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRepeat.embedded line 115
  24. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRepeat.temporaryTapes line 120
  25. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRepeat.temporaryConfig line 123
  26. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRepeat.inputTapes_update_input line 127
  27. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRepeat.inputTapes_update_counter line 139
  28. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRepeat.oneStep line 148
  29. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRepeat.parseStep_true line 156
  30. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRepeat.parseStep_false line 165
  31. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRepeat.parseTrace line 174
  32. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRepeat.guardStep_some line 200
  33. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRepeat.guardStep_none line 209
  34. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRepeat.bodyExecution line 217

    Source documentation

    Lift the actual certified body run while preserving the remaining counter.

    def bodyExecution (counter : List (M.Γ M.k₀))
    (word : List (M.Γ M.k₀)) (result : List (M.Γ M.k₁)) (budget : Nat)
    (run : TM2OutputsInTime M word (some result) budget) :
    StateTransition.EvalsToInTime (machine M input output).step
      (embedded M counter (initList M word))
      (some (embedded M counter (haltList M result))) budget :=
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRepeat.machine, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRepeat.embedded

  35. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRepeat.bodyToTemp_tapes line 227
  36. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRepeat.tempToBody_tapes line 243
  37. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRepeat.finalToTemp_tapes line 255
  38. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRepeat.tempToOutput_tapes line 267
  39. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRepeat.bodyToTemp line 278
  40. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRepeat.tempToBody line 294
  41. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRepeat.finalToTemp line 309
  42. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRepeat.tempToOutput line 321
  43. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRepeat.bodyReturn line 335

    Source documentation

    Transfer the literal body output back to the input, preserving its order.

    def bodyReturn (result : List (M.Γ M.k₁)) (counter : List (M.Γ M.k₀)) :
    StateTransition.EvalsToInTime (machine M input output).step
      (embedded M counter (haltList M result))
      (some (inputConfig M .guard (result.map (fun b => input.symm (output b))) counter))
      (2*(result.length+1)) := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRepeat.machine, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRepeat.embedded, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRepeat.inputConfig

  44. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRepeat.finish line 348

    Source documentation

    Zero remaining iterations still run the actual final transfers and halt with every tape other than the designated output empty.

    def finish (word : List (M.Γ M.k₀)) :
    StateTransition.EvalsToInTime (machine M input output).step
      (inputConfig M .guard word []) (some (haltList (machine M input output) word))
      (2*word.length+3) := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRepeat.machine, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRepeat.inputConfig

  45. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRepeat.loopBudget line 362

    Source documentation

    Running time after the parser: actual body budgets, two transfers per body result, one guard per iteration, and the final transfer and empty guard.

    def loopBudget : Nat → (Nat → List Bool) → (Nat → Nat) → Nat
  | 0, words, _ => 2*(words 0).length+3
  | count+1, words, budgets => budgets 0 + 2*(words 1).length+3 +
      loopBudget count (fun i => words (i+1)) (fun i => budgets (i+1))
  46. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRepeat.loopExecution line 367
  47. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRepeat.inputConfig_init line 405
  48. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRepeat.executeSequence line 417
  49. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRepeat.loopBudget_eq_sum line 444

    Source documentation

    Explicit sum form of the actual repeat budget.

    theorem loopBudget_eq_sum (count : Nat) (words : Nat → List Bool) (budgets : Nat → Nat) :
    loopBudget count words budgets =
      (∑ i ∈ Finset.range count, (budgets i + 2*(words (i+1)).length+3)) +
      2*(words count).length+3 := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRepeat.loopBudget

  50. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRepeat.executeSequenceSum line 456

    Source documentation

    The sum of supplied body budgets and explicit linear transfer overheads.

    def executeSequenceSum (count : Nat) (words : Nat → List Bool) (budgets : Nat → Nat)
    (runs : ∀ i, i < count → TM2OutputsInTime M ((words i).map input.symm)
      (some ((words (i+1)).map output.symm)) (budgets i)) :
    TM2OutputsInTime (machine M input output)
      ((encodeWord count ++ words 0).map input.symm)
      (some ((words count).map input.symm))
      (count+1 + ((∑ i ∈ Finset.range count, (budgets i+2*(words (i+1)).length+3)) +
        2*(words count).length+3)) := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRepeat.machine, OAI.UniqueGamesTheorem.Foundations.Complexity.encodeWord

  51. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRepeat.loopBudget_le line 470

    Source documentation

    A uniform bound along the executed sequence is enough to bound the actual repeat runtime. No polynomial growth of an arbitrary iteration is asserted.

    theorem loopBudget_le (count : Nat) (words : Nat → List Bool) (budgets : Nat → Nat)
    (bodyBound lengthBound : Nat)
    (hb : ∀i, i<count → budgets i ≤ bodyBound)
    (hl : ∀i, i≤count → (words i).length ≤ lengthBound) :
    loopBudget count words budgets ≤ count*(bodyBound+2*lengthBound+3)+2*lengthBound+3 := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRepeat.loopBudget