OAI/Computability/MaxCut/Machines/MachineCloudSelect.lean

GitHub source file

64 declarations, 0 contain sorry, 0 declared as axioms

Actual inverse cloud numbering. The input table and query are copied preservingly. A unary working rank decreases only on equal stored tail fields; a separate unary row position increases on every skipped row. Only finite phase flags and symbol registers occur in the control state.

  1. abbrev OAI.MaxCutGames.Foundations.Complexity.MachineCloudSelect.BaseTape line 16
  2. abbrev OAI.MaxCutGames.Foundations.Complexity.MachineCloudSelect.BaseAlphabet line 17
  3. abbrev OAI.MaxCutGames.Foundations.Complexity.MachineCloudSelect.BaseState line 18
  4. inductive OAI.MaxCutGames.Foundations.Complexity.MachineCloudSelect.BaseLabel line 20
  5. def OAI.MaxCutGames.Foundations.Complexity.MachineCloudSelect.skipLabel line 26
  6. def OAI.MaxCutGames.Foundations.Complexity.MachineCloudSelect.baseProgram line 31
  7. theorem OAI.MaxCutGames.Foundations.Complexity.MachineCloudSelect.baseProgram_skip line 51
  8. inductive OAI.MaxCutGames.Foundations.Complexity.MachineCloudSelect.Phase line 56
  9. abbrev OAI.MaxCutGames.Foundations.Complexity.MachineCloudSelect.Phase.enumList line 59
  10. theorem OAI.MaxCutGames.Foundations.Complexity.MachineCloudSelect.Phase.enumList_getElem?_ctorIdx_eq line 61
  11. theorem OAI.MaxCutGames.Foundations.Complexity.MachineCloudSelect.Phase.enumList_nodup line 65
  12. instance OAI.MaxCutGames.Foundations.Complexity.MachineCloudSelect.(instance at line 67) line 67
  13. inductive OAI.MaxCutGames.Foundations.Complexity.MachineCloudSelect.Control line 71
  14. abbrev OAI.MaxCutGames.Foundations.Complexity.MachineCloudSelect.Control.enumList line 74
  15. theorem OAI.MaxCutGames.Foundations.Complexity.MachineCloudSelect.Control.enumList_getElem?_ctorIdx_eq line 76
  16. theorem OAI.MaxCutGames.Foundations.Complexity.MachineCloudSelect.Control.enumList_nodup line 80
  17. instance OAI.MaxCutGames.Foundations.Complexity.MachineCloudSelect.(instance at line 82) line 82
  18. abbrev OAI.MaxCutGames.Foundations.Complexity.MachineCloudSelect.Tape line 86
  19. abbrev OAI.MaxCutGames.Foundations.Complexity.MachineCloudSelect.Alphabet line 87
  20. abbrev OAI.MaxCutGames.Foundations.Complexity.MachineCloudSelect.Label line 88
  21. abbrev OAI.MaxCutGames.Foundations.Complexity.MachineCloudSelect.State line 89
  22. def OAI.MaxCutGames.Foundations.Complexity.MachineCloudSelect.go line 91
  23. def OAI.MaxCutGames.Foundations.Complexity.MachineCloudSelect.dispatcher line 96

    Source documentation

    Pop the one-bit match result. Only a match pops the remaining local rank. Every completed skipped row separately pushes the global position.

    def dispatcher : TM2.Stmt Alphabet Label (State σ) :=
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineCloudSelect.Alphabet, OAI.MaxCutGames.Foundations.Complexity.MachineCloudSelect.Label, OAI.MaxCutGames.Foundations.Complexity.MachineCloudSelect.State

  24. def OAI.MaxCutGames.Foundations.Complexity.MachineCloudSelect.extra line 109
  25. def OAI.MaxCutGames.Foundations.Complexity.MachineCloudSelect.program line 113
  26. def OAI.MaxCutGames.Foundations.Complexity.MachineCloudSelect.memory line 116
  27. theorem OAI.MaxCutGames.Foundations.Complexity.MachineCloudSelect.memory_inl line 121
  28. theorem OAI.MaxCutGames.Foundations.Complexity.MachineCloudSelect.memory_position line 123
  29. theorem OAI.MaxCutGames.Foundations.Complexity.MachineCloudSelect.update_memory_hit line 126
  30. theorem OAI.MaxCutGames.Foundations.Complexity.MachineCloudSelect.update_memory_rank line 132
  31. theorem OAI.MaxCutGames.Foundations.Complexity.MachineCloudSelect.update_memory_position line 138
  32. def OAI.MaxCutGames.Foundations.Complexity.MachineCloudSelect.cfg line 145
  33. theorem OAI.MaxCutGames.Foundations.Complexity.MachineCloudSelect.liftTrace line 150
  34. theorem OAI.MaxCutGames.Foundations.Complexity.MachineCloudSelect.compareTrace line 163
  35. theorem OAI.MaxCutGames.Foundations.Complexity.MachineCloudSelect.dispatch_miss line 186
  36. theorem OAI.MaxCutGames.Foundations.Complexity.MachineCloudSelect.dispatch_hit_succ line 193
  37. theorem OAI.MaxCutGames.Foundations.Complexity.MachineCloudSelect.dispatch_hit_zero line 202
  38. theorem OAI.MaxCutGames.Foundations.Complexity.MachineCloudSelect.advanceStep line 210
  39. theorem OAI.MaxCutGames.Foundations.Complexity.MachineCloudSelect.finishStep line 219
  40. theorem OAI.MaxCutGames.Foundations.Complexity.MachineCloudSelect.initializeStep line 225
  41. theorem OAI.MaxCutGames.Foundations.Complexity.MachineCloudSelect.skipTrace line 233

    Source documentation

    The rest of a row is skipped field by field by the actual fixed program.

    theorem skipTrace (fields : List Nat) (hwidth : fields.length = 4097)
    (original suffix target rank position : List Bool) (ambient : σ) :
    (advance (TM2.step program))^[(encodeWords fields).length + 1]
      (some (cfg (some (.inl (skipLabel 0))) .advancing original
        (encodeWords fields ++ suffix) target [] rank position ambient none)) =
      some (cfg (some (.inr .dispatch)) .advancing
        original suffix target [] rank position ambient none) := by
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineCloudSelect.program, OAI.MaxCutGames.Foundations.Complexity.encodeWords, OAI.MaxCutGames.Foundations.Complexity.MachineCloudSelect.cfg, OAI.MaxCutGames.Foundations.Complexity.MachineCloudSelect.skipLabel

  42. theorem OAI.MaxCutGames.Foundations.Complexity.MachineCloudSelect.rowSkipTrace line 259

    Source documentation

    One nonselected row, with enough remaining rank to pass this row when it matches. Its global position is incremented on the output tape.

    theorem rowSkipTrace (r : Row) (hwidth : r.2.length = 4097) (v rank position : Nat)
    (original suffix targetSuffix rankSuffix outputSuffix : List Bool)
    (ambient : σ) (register : Option Bool) :
    (advance (TM2.step program))^[rowTime v r + 3]
      (some (cfg (some (.inl .field)) .checking original
        (encodeWords (rowWords r) ++ suffix) (encodeWord v ++ targetSuffix) []
        (encodeWord (rank + if r.1 = v then 1 else 0) ++ rankSuffix)
        (encodeWord position ++ outputSuffix) ambient register)) =
      some (cfg (some (.inl .field)) .checking original suffix
        (encodeWord v ++ targetSuffix) [] (encodeWord rank ++ rankSuffix)
        (encodeWord (position + 1) ++ outputSuffix) ambient none) := by
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineCloudSelect.program, OAI.MaxCutGames.Foundations.Complexity.MachineCloudSelect.cfg, OAI.MaxCutGames.Foundations.Complexity.encodeWords, OAI.MaxCutGames.Foundations.Complexity.encodeWord

  43. def OAI.MaxCutGames.Foundations.Complexity.MachineCloudSelect.prefixTime line 303
  44. theorem OAI.MaxCutGames.Foundations.Complexity.MachineCloudSelect.prefixTrace line 309

    Source documentation

    A preceding consumes precisely its number of matching tails from unary rank, while physically counting every original row on the position tape.

    theorem prefixTrace (rs : List Row) (hwidth : ∀ r ∈ rs, r.2.length = 4097)
    (v rank position : Nat) (original suffix targetSuffix rankSuffix outputSuffix : List Bool)
    (ambient : σ) (register : Option Bool) :
    (advance (TM2.step program))^[prefixTime v rs]
      (some (cfg (some (.inl .field)) .checking original
        (encodeWords (rs.flatMap rowWords) ++ suffix) (encodeWord v ++ targetSuffix) []
        (encodeWord (rowsHits v rs + rank) ++ rankSuffix)
        (encodeWord position ++ outputSuffix) ambient register)) =
      some (cfg (some (.inl .field)) .checking original suffix
        (encodeWord v ++ targetSuffix) [] (encodeWord rank ++ rankSuffix)
        (encodeWord (position + rs.length) ++ outputSuffix) ambient
        (if rs = [] then register else none)) := by
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineCloudSelect.program, OAI.MaxCutGames.Foundations.Complexity.MachineCloudSelect.prefixTime, OAI.MaxCutGames.Foundations.Complexity.MachineCloudSelect.cfg, OAI.MaxCutGames.Foundations.Complexity.encodeWords, OAI.MaxCutGames.Foundations.Complexity.encodeWord

  45. theorem OAI.MaxCutGames.Foundations.Complexity.MachineCloudSelect.cleanupTrace line 339

    Source documentation

    Both copied workspaces are physically drained after finding the row; the original table, complete query, and position output are retained.

    theorem cleanupTrace (original work target rank position : List Bool) (ambient : σ) :
    (advance (TM2.step program))^[work.length + rank.length + 4]
      (some (cfg (some (.inl .clearWork)) .finishing
        original work target [] rank position ambient none)) =
      some (cfg none .checking original [] target [] [] position ambient none) := by
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineCloudSelect.program, OAI.MaxCutGames.Foundations.Complexity.MachineCloudSelect.cfg

  46. theorem OAI.MaxCutGames.Foundations.Complexity.MachineCloudSelect.selectedTrace line 373
  47. abbrev OAI.MaxCutGames.Foundations.Complexity.MachineCloudSelect.queryWord line 390
  48. def OAI.MaxCutGames.Foundations.Complexity.MachineCloudSelect.prepareSteps line 392
  49. theorem OAI.MaxCutGames.Foundations.Complexity.MachineCloudSelect.prepareTrace line 398

    Source documentation

    Preserve the complete query and table while making the two working copies; extract the rank and skip the two actual table header fields.

    theorem prepareTrace (n m v rank : Nat) (rs : List Row)
    (querySuffix position : List Bool) (ambient : σ) (register : Option Bool) :
    (advance (TM2.step program))^[prepareSteps n m v rank rs querySuffix]
      (some (cfg (some (.inl .queryFirst)) .checking (MachineCloudCount.inputWord n m rs)
        [] (queryWord v rank querySuffix) [] [] position ambient register)) =
      some (cfg (some (.inl .field)) .checking (MachineCloudCount.inputWord n m rs)
        (encodeWords (rs.flatMap rowWords)) (queryWord v rank querySuffix) []
        (encodeWord rank ++ querySuffix) position ambient none) := by
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineCloudSelect.program, OAI.MaxCutGames.Foundations.Complexity.MachineCloudSelect.prepareSteps, OAI.MaxCutGames.Foundations.Complexity.MachineCloudSelect.cfg, OAI.MaxCutGames.Foundations.Complexity.MachineCloudCount.inputWord, OAI.MaxCutGames.Foundations.Complexity.MachineCloudSelect.queryWord, OAI.MaxCutGames.Foundations.Complexity.encodeWords, OAI.MaxCutGames.Foundations.Complexity.encodeWord

  50. theorem OAI.MaxCutGames.Foundations.Complexity.MachineCloudSelect.prefixSelectedTrace line 459

    Source documentation

    A selected matching field is reached after precisely the matching count of its actual preceding rows has been consumed from the copied query.

    theorem prefixSelectedTrace (preceding : List Row)
    (hwidth : ∀ r ∈ preceding, r.2.length = 4097) (v position : Nat)
    (original work targetSuffix rankSuffix outputSuffix : List Bool)
    (ambient : σ) (register : Option Bool) :
    (advance (TM2.step program))^[prefixTime v preceding + 2 * v + work.length + rankSuffix.length + 8]
      (some (cfg (some (.inl .field)) .checking original
        (encodeWords (preceding.flatMap rowWords) ++ (encodeWord v ++ work))
        (encodeWord v ++ targetSuffix) [] (encodeWord (rowsHits v preceding) ++ rankSuffix)
        (encodeWord position ++ outputSuffix) ambient register)) =
      some (cfg none .checking original [] (encodeWord v ++ targetSuffix) [] []
        (encodeWord (position + preceding.length) ++ outputSuffix) ambient none) := by
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineCloudSelect.program, OAI.MaxCutGames.Foundations.Complexity.MachineCloudSelect.prefixTime, OAI.MaxCutGames.Foundations.Complexity.MachineCloudSelect.cfg, OAI.MaxCutGames.Foundations.Complexity.encodeWords, OAI.MaxCutGames.Foundations.Complexity.encodeWord

  51. def OAI.MaxCutGames.Foundations.Complexity.MachineCloudSelect.totalSteps line 481
  52. theorem OAI.MaxCutGames.Foundations.Complexity.MachineCloudSelect.fullTrace line 488

    Source documentation

    Complete execution for the actual encoded preceding decomposition. The decomposition is semantic data; every machine phase is proved above.

    theorem fullTrace (n m v rank : Nat) (rs preceding : List Row) (work : List Bool)
    (hwidth : ∀ r ∈ preceding, r.2.length = 4097)
    (hword : encodeWords (rs.flatMap rowWords) =
      encodeWords (preceding.flatMap rowWords) ++ (encodeWord v ++ work))
    (hrank : rank = rowsHits v preceding) (querySuffix outputSuffix : List Bool)
    (ambient : σ) (register : Option Bool) :
    (advance (TM2.step program))^[totalSteps n m v rank rs preceding work querySuffix]
      (some (cfg (some (.inr .initialize)) .checking (MachineCloudCount.inputWord n m rs)
        [] (queryWord v rank querySuffix) [] [] outputSuffix ambient register)) =
      some (cfg none .checking (MachineCloudCount.inputWord n m rs) []
        (queryWord v rank querySuffix) [] [] (encodeWord preceding.length ++ outputSuffix) ambient none) := by
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.encodeWords, OAI.MaxCutGames.Foundations.Complexity.encodeWord, OAI.MaxCutGames.Foundations.Complexity.MachineCloudSelect.program, OAI.MaxCutGames.Foundations.Complexity.MachineCloudSelect.totalSteps, OAI.MaxCutGames.Foundations.Complexity.MachineCloudSelect.cfg, OAI.MaxCutGames.Foundations.Complexity.MachineCloudCount.inputWord, OAI.MaxCutGames.Foundations.Complexity.MachineCloudSelect.queryWord

  53. theorem OAI.MaxCutGames.Foundations.Complexity.MachineCloudSelect.prefixTime_le line 512
  54. theorem OAI.MaxCutGames.Foundations.Complexity.MachineCloudSelect.totalSteps_le line 524
  55. def OAI.MaxCutGames.Foundations.Complexity.MachineCloudSelect.remainder line 543

    Source documentation

    Bytes remaining after the selected row's actual tail field.

    def remainder (t : GraphTables.Table) (e : Fin t.darts) : List Bool :=
…
  56. theorem OAI.MaxCutGames.Foundations.Complexity.MachineCloudSelect.tableRows_getElem line 547
  57. theorem OAI.MaxCutGames.Foundations.Complexity.MachineCloudSelect.tableWord_split line 559

    Source documentation

    Canonical dart indexing yields the literal byte decomposition consumed by the actual preceding scan and final matching-field test.

    theorem tableWord_split (t : GraphTables.Table) (v : Fin t.vertices) (e : Fin t.darts)
    (owner : t.rows[e].tail = v) :
    encodeWords ((tableRows t).flatMap rowWords) =
      encodeWords (((tableRows t).take e.val).flatMap rowWords) ++
        (encodeWord v.val ++ remainder t e) := by
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.encodeWords, OAI.MaxCutGames.Foundations.Complexity.encodeWord, OAI.MaxCutGames.Foundations.Complexity.MachineCloudSelect.remainder

  58. def OAI.MaxCutGames.Foundations.Complexity.MachineCloudSelect.cloudSelectSteps line 572
  59. theorem OAI.MaxCutGames.Foundations.Complexity.MachineCloudSelect.cloudSelectTrace line 578
  60. theorem OAI.MaxCutGames.Foundations.Complexity.MachineCloudSelect.cloudSelectSteps_le line 602
  61. def OAI.MaxCutGames.Foundations.Complexity.MachineCloudSelect.timePolynomial line 612
  62. def OAI.MaxCutGames.Foundations.Complexity.MachineCloudSelect.cloudSelectInTime line 615
  63. def OAI.MaxCutGames.Foundations.Complexity.MachineCloudSelect.machine line 631
  64. def OAI.MaxCutGames.Foundations.Complexity.MachineCloudSelect.machineInTime line 644

    Source documentation

    A concrete finite-machine certificate, with neither a runtime nor a selection oracle among its hypotheses.

    def machineInTime (t : GraphTables.Table) (v : Fin t.vertices)
    (i : Fin (PreprocessingCloudIndex.cloudSize t v)) (querySuffix outputSuffix : List Bool)
    (register : Option Bool) :
    StateTransition.EvalsToInTime machine.step
      (cfg (some (.inr .initialize)) .checking (GraphTables.tableBits t)
        [] (queryWord v.val i.val querySuffix) [] [] outputSuffix () register)
      (some (cfg none .checking (GraphTables.tableBits t) [] (queryWord v.val i.val querySuffix)
        [] [] (encodeWord (PreprocessingCloudIndex.cloudSelect t v i).val.val ++ outputSuffix)
        () none))
      (timePolynomial.eval ((GraphTables.tableBits t).length + (queryWord v.val i.val querySuffix).length)) where
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineCloudSelect.cfg, OAI.MaxCutGames.Foundations.Complexity.MachineCloudSelect.queryWord, OAI.MaxCutGames.Foundations.Complexity.encodeWord