OAI/Computability/MaxCut/Machines/MachineClone100Triples.lean

GitHub source file

70 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MaxCutGames.Explicit.MachineClone100Triples.rowOutput line 15
  2. def OAI.MaxCutGames.Explicit.MachineClone100Triples.rowSteps line 21
  3. def OAI.MaxCutGames.Explicit.MachineClone100Triples.startAt line 25
  4. theorem OAI.MaxCutGames.Explicit.MachineClone100Triples.contextTapes_field line 28
  5. theorem OAI.MaxCutGames.Explicit.MachineClone100Triples.rowOutput_update line 33
  6. theorem OAI.MaxCutGames.Explicit.MachineClone100Triples.rowSteps_update line 38
  7. theorem OAI.MaxCutGames.Explicit.MachineClone100Triples.chain_inline_MachineClone100Triples line 42
  8. theorem OAI.MaxCutGames.Explicit.MachineClone100Triples.fourContexts_tapes line 46
  9. theorem OAI.MaxCutGames.Explicit.MachineClone100Triples.rowTrace line 58

    Source documentation

    Execute each of the four actual contexts in slot order.

    theorem rowTrace (triples : List (Nat × Nat × Nat)) (nonempty : triples ≠ [])
    (i : Fin triples.length) (base : Tape → List Bool)
    (scratchEmpty : base .scratch = []) (state : State triples.length) :
    (MachineComposition.advance (TM2.step (program triples nonempty)))^[rowSteps base]
      (some ⟨some (.setup (.inr (i, 0))), state, base⟩) =
      some ⟨startAt triples.length (i.val + 1), initialState _,
        Function.update base .reversed ((rowOutput (triples.get i) base).reverse ++
          base .reversed)⟩ := by
…

    Mentions: OAI.MaxCutGames.Explicit.MachineClone100Triples.rowSteps, OAI.MaxCutGames.Explicit.MachineClone100Triples.startAt, OAI.MaxCutGames.Explicit.MachineClone100Triples.rowOutput

  10. theorem OAI.MaxCutGames.Explicit.MachineClone100Triples.tailTrace_inline_MachineClone100Triples line 93
  11. theorem OAI.MaxCutGames.Explicit.MachineClone100Triples.tableTrace_raw line 133
  12. def OAI.MaxCutGames.Explicit.MachineClone100Triples.affineRecord line 144
  13. theorem OAI.MaxCutGames.Explicit.MachineClone100Triples.rowOutput_words line 147
  14. theorem OAI.MaxCutGames.Explicit.MachineClone100Triples.tableOutput_words line 155
  15. theorem OAI.MaxCutGames.Explicit.MachineClone100Triples.tableTrace line 168

    Source documentation

    The actual inner loop outputs the concrete cloned equation words.

    theorem tableTrace (triples : List (Nat × Nat × Nat)) (nonempty : triples ≠ [])
    (base : Tape → List Bool) (scratchEmpty : base .scratch = [])
    (state : State triples.length) (a b c rhs : Nat)
    (h0 : base (.field 0) = encodeWord a) (h1 : base (.field 1) = encodeWord b)
    (h2 : base (.field 2) = encodeWord c) (h3 : base (.field 3) = encodeWord rhs) :
    (MachineComposition.advance (TM2.step (program triples nonempty)))^[
      triples.length * (3 * ((a + 1) + (b + 1) + (c + 1) + (rhs + 1)) + 12)]
      (some ⟨some (.setup (.inr (⟨0, List.length_pos_iff.mpr nonempty⟩, 0))), state, base⟩) =
      some ⟨some (.cleanup 0), initialState _, Function.update base .reversed
        ((encodeWords (triples.flatMap (affineRecord a b c rhs))).reverse ++ base .reversed)⟩ := by
…

    Mentions: OAI.MaxCutGames.Explicit.MachineClone100Triples.affineRecord

  16. theorem OAI.MaxCutGames.Explicit.MachineClone100Triples.tableTapes_other line 182
  17. structure OAI.MaxCutGames.Explicit.MachineClone100Loop.Record line 199
  18. def OAI.MaxCutGames.Explicit.MachineClone100Loop.recordWords line 205
  19. def OAI.MaxCutGames.Explicit.MachineClone100Loop.recordBits line 206
  20. def OAI.MaxCutGames.Explicit.MachineClone100Loop.recordsBits line 207
  21. def OAI.MaxCutGames.Explicit.MachineClone100Loop.clonedRecordBits line 209
  22. def OAI.MaxCutGames.Explicit.MachineClone100Loop.clonedRecordsBits line 212
  23. def OAI.MaxCutGames.Explicit.MachineClone100Loop.recordFields line 215
  24. def OAI.MaxCutGames.Explicit.MachineClone100Loop.tapes line 220

    Source documentation

    The frame records all tapes, including untouched header and output tapes. At every loop guard the four fields are empty and scratch is empty.

    def tapes (base : Tape → List Bool) (input counter accumulator : List Bool)
    (fields : Fin 4 → List Bool) : Tape → List Bool
  | .input => input
  | .header => base .header
  | .counter => counter
  | .field j => fields j
  | .scratch => []
  | .reversed => accumulator
  | .output => base .output
  25. theorem OAI.MaxCutGames.Explicit.MachineClone100Loop.update_reversed line 230
  26. theorem OAI.MaxCutGames.Explicit.MachineClone100Loop.counterTapes_eq line 237
  27. theorem OAI.MaxCutGames.Explicit.MachineClone100Loop.fourTapes_eq line 245
  28. theorem OAI.MaxCutGames.Explicit.MachineClone100Loop.clearFields_eq line 260
  29. theorem OAI.MaxCutGames.Explicit.MachineClone100Loop.cleanupSteps_eq line 267
  30. theorem OAI.MaxCutGames.Explicit.MachineClone100Loop.recordBits_length line 274
  31. def OAI.MaxCutGames.Explicit.MachineClone100Loop.bodyCost line 279
  32. theorem OAI.MaxCutGames.Explicit.MachineClone100Loop.bodyCost_eq_inline_MachineClone100Loop line 282
  33. def OAI.MaxCutGames.Explicit.MachineClone100Loop.bodyInTime line 289
  34. def OAI.MaxCutGames.Explicit.MachineClone100Loop.loopCost line 338
  35. theorem OAI.MaxCutGames.Explicit.MachineClone100Loop.loopCost_eq line 342
  36. def OAI.MaxCutGames.Explicit.MachineClone100Loop.loopInTime line 355

    Source documentation

    The complete record loop consumes exactly the specified occurrence list. The final zero guard retains the counter delimiter for the final cleanup stage. Arbitrary suffixes and already emitted prefixes are preserved explicitly.

    def loopInTime (triples : List (Nat × Nat × Nat)) (nonempty : triples ≠ [])
    (base : Tape → List Bool) (suffix : List Bool) (rs : List Record) (acc : List Bool) :
    StateTransition.EvalsToInTime (TM2.step (program triples nonempty))
      ⟨some .guard, initialState _,
        tapes base (recordsBits rs ++ suffix) (encodeWord rs.length) acc (fun _ => [])⟩
      (some ⟨some .finalCounter, initialState _,
        tapes base suffix (encodeWord 0) ((clonedRecordsBits triples rs).reverse ++ acc)
          (fun _ => [])⟩)
      (loopCost triples.length rs) := by
…

    Mentions: OAI.MaxCutGames.Explicit.MachineClone100Loop.Record, OAI.MaxCutGames.Explicit.MachineClone100Loop.tapes, OAI.MaxCutGames.Explicit.MachineClone100Loop.recordsBits, OAI.MaxCutGames.Explicit.MachineClone100Loop.clonedRecordsBits, OAI.MaxCutGames.Explicit.MachineClone100Loop.loopCost

  37. def OAI.MaxCutGames.Explicit.MachineClone100Loop.loopInTime_linear line 390

    Source documentation

    A linear bound derived from the actual composed execution.

    def loopInTime_linear (triples : List (Nat × Nat × Nat)) (nonempty : triples ≠ [])
    (base : Tape → List Bool) (suffix : List Bool) (rs : List Record) (acc : List Bool) :
    StateTransition.EvalsToInTime (TM2.step (program triples nonempty))
      ⟨some .guard, initialState _,
        tapes base (recordsBits rs ++ suffix) (encodeWord rs.length) acc (fun _ => [])⟩
      (some ⟨some .finalCounter, initialState _,
        tapes base suffix (encodeWord 0) ((clonedRecordsBits triples rs).reverse ++ acc)
          (fun _ => [])⟩)
      ((2 + 3 * triples.length) * (recordsBits rs).length +
        (9 + 12 * triples.length) * rs.length + 1) := by
…

    Mentions: OAI.MaxCutGames.Explicit.MachineClone100Loop.Record, OAI.MaxCutGames.Explicit.MachineClone100Loop.tapes, OAI.MaxCutGames.Explicit.MachineClone100Loop.recordsBits, OAI.MaxCutGames.Explicit.MachineClone100Loop.clonedRecordsBits

  38. def OAI.MaxCutGames.Explicit.MachineClone100Loop.recordOfEquation line 402
  39. theorem OAI.MaxCutGames.Explicit.MachineClone100Loop.recordsBits_equations line 405
  40. theorem OAI.MaxCutGames.Explicit.MachineClone100Loop.clonedRecordsBits_equations_table line 415
  41. def OAI.MaxCutGames.Explicit.MachineClone100Loop.sourceLoopInTime_table line 426
  42. def OAI.MaxCutGames.Explicit.MachineClone100Finish.finishTapes line 452
  43. theorem OAI.MaxCutGames.Explicit.MachineClone100Finish.finishTapes_counter line 456
  44. theorem OAI.MaxCutGames.Explicit.MachineClone100Finish.finishTapes_reversed line 459
  45. theorem OAI.MaxCutGames.Explicit.MachineClone100Finish.finishTapes_output line 462
  46. theorem OAI.MaxCutGames.Explicit.MachineClone100Finish.finishTapes_other line 466
  47. theorem OAI.MaxCutGames.Explicit.MachineClone100Finish.counterStep line 471
  48. theorem OAI.MaxCutGames.Explicit.MachineClone100Finish.finishTrace line 478
  49. def OAI.MaxCutGames.Explicit.MachineClone100Finish.finishInTime line 502
  50. theorem OAI.MaxCutGames.Explicit.MachineClone100Finish.finish_eq_haltList line 511
  51. def OAI.MaxCutGames.Explicit.MachineClone100Run.tm line 536
  52. def OAI.MaxCutGames.Explicit.MachineClone100Run.emptyTapes line 539
  53. def OAI.MaxCutGames.Explicit.MachineClone100Run.sourceBody line 541
  54. def OAI.MaxCutGames.Explicit.MachineClone100Run.outputHeaders line 544
  55. def OAI.MaxCutGames.Explicit.MachineClone100Run.outputBody line 548
  56. def OAI.MaxCutGames.Explicit.MachineClone100Run.outputBits line 553
  57. def OAI.MaxCutGames.Explicit.MachineClone100Run.inputTapes line 557
  58. def OAI.MaxCutGames.Explicit.MachineClone100Run.guardTapes line 560
  59. def OAI.MaxCutGames.Explicit.MachineClone100Run.afterLoopTapes line 565
  60. theorem OAI.MaxCutGames.Explicit.MachineClone100Run.inputBits_eq line 570
  61. theorem OAI.MaxCutGames.Explicit.MachineClone100Run.initList_eq line 575
  62. theorem OAI.MaxCutGames.Explicit.MachineClone100Run.headers_result_eq line 588
  63. theorem OAI.MaxCutGames.Explicit.MachineClone100Run.afterLoop_reversed line 595
  64. theorem OAI.MaxCutGames.Explicit.MachineClone100Run.afterLoop_length line 600
  65. theorem OAI.MaxCutGames.Explicit.MachineClone100Run.finish_eq line 606
  66. def OAI.MaxCutGames.Explicit.MachineClone100Run.runInTime line 620

    Source documentation

    Actual execution from the existing input codec to the complete literal halt configuration, with the sum of the three proved phase budgets.

    def runInTime (triples : List (Nat × Nat × Nat)) (nonempty : triples ≠ [])
    (input : SourceEncoding.Input) :
    TM2OutputsInTime (tm triples nonempty) (SourceEncoding.inputBits input)
      (some (outputBits triples input))
      (((outputBits triples input).length + 2) +
        (((2 + 3 * triples.length) * (sourceBody input).length +
            (9 + 12 * triples.length) * input.equations.length + 1) +
          (5 * input.«variables» + 4 * input.equations.length + 18))) := by
…

    Mentions: OAI.MaxCutGames.Explicit.MachineClone100Run.tm, OAI.MaxCutGames.Explicit.MachineClone100Run.outputBits, OAI.MaxCutGames.Explicit.MachineClone100Run.sourceBody

  67. def OAI.MaxCutGames.Explicit.MachineClone100Certified.timePolynomial line 667
  68. theorem OAI.MaxCutGames.Explicit.MachineClone100Certified.timePolynomial_eval line 671
  69. theorem OAI.MaxCutGames.Explicit.MachineClone100Certified.numericalBudget_inline_MachineClone100Certified line 677
  70. def OAI.MaxCutGames.Explicit.MachineClone100Certified.certifiedFunction line 691