OAI/Computability/UniqueGames/Machines/MachineBinaryTotalInputMachine.lean

GitHub source file

37 declarations, 0 contain sorry, 0 declared as axioms

Total raw-input preprocessing for the ordinary binary formula codec. The machine copies each input bit onto a reverse stack while running the finite validator. Accepted words are restored verbatim; rejected words are drained and replaced by the fixed contradictory formula. All three stack alphabets and all control/register types are finite.

  1. inductive OAI.UniqueGamesTheorem.BinaryTotalInputMachine.Label line 26
  2. abbrev OAI.UniqueGamesTheorem.BinaryTotalInputMachine.Label.enumList line 33
  3. theorem OAI.UniqueGamesTheorem.BinaryTotalInputMachine.Label.enumList_getElem?_ctorIdx_eq line 35
  4. theorem OAI.UniqueGamesTheorem.BinaryTotalInputMachine.Label.enumList_nodup line 39
  5. instance OAI.UniqueGamesTheorem.BinaryTotalInputMachine.(instance at line 41) line 41
  6. abbrev OAI.UniqueGamesTheorem.BinaryTotalInputMachine.Alphabet line 45
  7. abbrev OAI.UniqueGamesTheorem.BinaryTotalInputMachine.State line 46
  8. def OAI.UniqueGamesTheorem.BinaryTotalInputMachine.rejectedWord line 48
  9. def OAI.UniqueGamesTheorem.BinaryTotalInputMachine.instruction line 52

    Source documentation

    Stack zero is the input, one the output, and two the reversed input. Branches inspect only the finite validator state and the popped symbol.

    def instruction : Label → TM2.Stmt Alphabet Label State
  | .scan =>
      .pop 0 (fun state head => (state.1, head))
        (.branch (fun state => state.2.isSome)
          (.push 2 (fun state => state.2.getD false)
            (.load (fun state => (nextMode state.1 (state.2.getD false), none))
              (.goto fun _ => .scan)))
          (.branch (fun state => decide (state.1 = .done))
            (.load (fun _ => (.clause, none)) (.goto fun _ => .restore))
            (.load (fun _ => (.clause, none)) (.goto fun _ => .drain))))
  | .restore => loopAt 2 1 id false .restore none
  | .drain => MachineDrain.drain 2 .drain (some .rejectOutput)
…

    Mentions: OAI.UniqueGamesTheorem.BinaryTotalInputMachine.Label, OAI.UniqueGamesTheorem.BinaryTotalInputMachine.Alphabet, OAI.UniqueGamesTheorem.BinaryTotalInputMachine.State

  10. abbrev OAI.UniqueGamesTheorem.BinaryTotalInputMachine.machine line 66
  11. def OAI.UniqueGamesTheorem.BinaryTotalInputMachine.tapes line 77
  12. def OAI.UniqueGamesTheorem.BinaryTotalInputMachine.cfg line 82
  13. theorem OAI.UniqueGamesTheorem.BinaryTotalInputMachine.tapes_input line 86
  14. theorem OAI.UniqueGamesTheorem.BinaryTotalInputMachine.tapes_output line 89
  15. theorem OAI.UniqueGamesTheorem.BinaryTotalInputMachine.tapes_saved line 92
  16. theorem OAI.UniqueGamesTheorem.BinaryTotalInputMachine.update_input line 95
  17. theorem OAI.UniqueGamesTheorem.BinaryTotalInputMachine.update_output line 101
  18. theorem OAI.UniqueGamesTheorem.BinaryTotalInputMachine.update_saved line 107
  19. def OAI.UniqueGamesTheorem.BinaryTotalInputMachine.afterScan line 113
  20. theorem OAI.UniqueGamesTheorem.BinaryTotalInputMachine.step_scan_empty line 115
  21. theorem OAI.UniqueGamesTheorem.BinaryTotalInputMachine.step_scan_cons line 122
  22. theorem OAI.UniqueGamesTheorem.BinaryTotalInputMachine.scanTrace line 132

    Source documentation

    The finite DFA reads every bit, including all bits in its rejection sink. The trace also records the physical reversed copy needed by the second phase.

    theorem scanTrace (input output saved : List Bool) (mode : Mode) (register : Option Bool) :
    (advance machine.step)^[input.length + 1]
      (some (cfg (some .scan) input output saved mode register)) =
      some (cfg (some (afterScan (run mode input))) [] output (input.reverse ++ saved)) := by
…

    Mentions: OAI.UniqueGamesTheorem.BinaryTotalInputMachine.cfg, OAI.UniqueGamesTheorem.BinaryTotalInputMachine.afterScan

  23. theorem OAI.UniqueGamesTheorem.BinaryTotalInputMachine.restoreTrace line 148
  24. theorem OAI.UniqueGamesTheorem.BinaryTotalInputMachine.drainTrace line 160
  25. theorem OAI.UniqueGamesTheorem.BinaryTotalInputMachine.step_rejectOutput line 171
  26. theorem OAI.UniqueGamesTheorem.BinaryTotalInputMachine.joinTrace line 181
  27. theorem OAI.UniqueGamesTheorem.BinaryTotalInputMachine.acceptedTrace line 185
  28. theorem OAI.UniqueGamesTheorem.BinaryTotalInputMachine.rejectedTrace line 196
  29. theorem OAI.UniqueGamesTheorem.BinaryTotalInputMachine.initList_eq line 211
  30. theorem OAI.UniqueGamesTheorem.BinaryTotalInputMachine.haltList_eq line 218
  31. def OAI.UniqueGamesTheorem.BinaryTotalInputMachine.steps line 225
  32. theorem OAI.UniqueGamesTheorem.BinaryTotalInputMachine.steps_le line 228
  33. theorem OAI.UniqueGamesTheorem.BinaryTotalInputMachine.totalTrace line 233

    Source documentation

    Full correspondence on every raw word, with no validity premise.

    theorem totalTrace (input : List Bool) :
    (advance machine.step)^[steps input] (some (initList machine input)) =
      some (haltList machine (BinaryEncoding.formulaBits (BinaryLanguage.totalParsed input))) := by
…

    Mentions: OAI.UniqueGamesTheorem.BinaryTotalInputMachine.steps, OAI.UniqueGamesTheorem.BinaryTotalInputMachine.machine, OAI.UniqueGamesTheorem.BinaryEncoding.formulaBits, OAI.UniqueGamesTheorem.BinaryLanguage.totalParsed

  34. def OAI.UniqueGamesTheorem.BinaryTotalInputMachine.outputsInTime line 255
  35. def OAI.UniqueGamesTheorem.BinaryTotalInputMachine.computableInPolyTime line 265

    Source documentation

    The certificate contains the displayed total machine and its linear trace; it assumes no execution, parser-cost, or malformed-input premise.

    noncomputable def computableInPolyTime :
    TM2ComputableInPolyTime (id : List Bool → List Bool) BinaryEncoding.formulaBits
      BinaryLanguage.totalParsed where
…

    Mentions: OAI.UniqueGamesTheorem.BinaryEncoding.formulaBits, OAI.UniqueGamesTheorem.BinaryLanguage.totalParsed

  36. theorem OAI.UniqueGamesTheorem.BinaryTotalInputMachine.machine_finiteAlphabet line 279
  37. theorem OAI.UniqueGamesTheorem.BinaryTotalInputMachine.computation_finiteAlphabet line 283