OAI/Computability/MaxCut/Machines/MachineBinaryNameCompare.lean

GitHub source file

75 declarations, 0 contain sorry, 0 declared as axioms

Compare one framed binary name with an already extracted reversed key. The candidate stream loses precisely that name frame. The key and every other non-work stack are preserved; the three work stacks are empty again on exit. The scanner, copy loops, and head-by-head comparison all execute actual TM2 instructions. Whole words occur only in the correctness specification.

  1. abbrev OAI.MaxCutGames.BinaryNameCompare.Alphabet line 22
  2. abbrev OAI.MaxCutGames.BinaryNameCompare.State line 23
  3. def OAI.MaxCutGames.BinaryNameCompare.clean line 25
  4. def OAI.MaxCutGames.BinaryNameCompare.scanStateEquiv line 27
  5. def OAI.MaxCutGames.BinaryNameCompare.compareStateEquiv line 33
  6. inductive OAI.MaxCutGames.BinaryNameCompare.Label line 39
  7. abbrev OAI.MaxCutGames.BinaryNameCompare.Label.enumList line 43
  8. theorem OAI.MaxCutGames.BinaryNameCompare.Label.enumList_getElem?_ctorIdx_eq line 45
  9. theorem OAI.MaxCutGames.BinaryNameCompare.Label.enumList_nodup line 49
  10. instance OAI.MaxCutGames.BinaryNameCompare.(instance at line 51) line 51
  11. def OAI.MaxCutGames.BinaryNameCompare.instruction line 56

    Source documentation

    Tapes: candidate stream, preserved key, candidate payload, key copy, scratch.

    def instruction (tape : Fin 5 → K) (labels : Label → Λ)
    (equalExit differentExit malformedExit : Option Λ) :
    Label → TM2.Stmt (Alphabet (K := K)) Λ (State A)
…

    Mentions: OAI.MaxCutGames.BinaryNameCompare.Label, OAI.MaxCutGames.BinaryNameCompare.Alphabet, OAI.MaxCutGames.BinaryNameCompare.State

  12. def OAI.MaxCutGames.BinaryNameCompare.steps line 69
  13. theorem OAI.MaxCutGames.BinaryNameCompare.steps_le line 72
  14. theorem OAI.MaxCutGames.BinaryNameCompare.joinTrace_inline_MachineBinaryNameCompare line 77
  15. theorem OAI.MaxCutGames.BinaryNameCompare.compareTrace line 83

    Source documentation

    The name is actually scanned, the key actually copied, and the resulting payloads actually compared. Program premises are literal instruction equations.

    theorem compareTrace (tape : Fin 5 → K) (distinct : Function.Injective tape)
    (labels : Label → Λ) (equalExit differentExit malformedExit : Option Λ)
    (program : Λ → TM2.Stmt (Alphabet (K := K)) Λ (State A))
…

    Mentions: OAI.MaxCutGames.BinaryNameCompare.Label, OAI.MaxCutGames.BinaryNameCompare.Alphabet, OAI.MaxCutGames.BinaryNameCompare.State

  16. def OAI.MaxCutGames.BinaryNameCompare.compareInTime line 188

    Source documentation

    Linear runtime in the extracted candidate and stored key lengths.

    def compareInTime (tape : Fin 5 → K) (distinct : Function.Injective tape)
    (labels : Label → Λ) (equalExit differentExit malformedExit : Option Λ)
    (program : Λ → TM2.Stmt (Alphabet (K := K)) Λ (State A))
…

    Mentions: OAI.MaxCutGames.BinaryNameCompare.Label, OAI.MaxCutGames.BinaryNameCompare.Alphabet, OAI.MaxCutGames.BinaryNameCompare.State

  17. def OAI.MaxCutGames.BinaryNameCompare.machine line 211

    Source documentation

    Concrete finite machine; exit labels 0, 1, 2 mean equal, different, malformed.

    def machine : FinTM2 where
…
  18. theorem OAI.MaxCutGames.BinaryNameCompare.machine_finiteAlphabet line 224
  19. abbrev OAI.MaxCutGames.BinaryNameSearch.Token line 251
  20. def OAI.MaxCutGames.BinaryNameSearch.tokenBits line 253
  21. def OAI.MaxCutGames.BinaryNameSearch.stream line 256
  22. def OAI.MaxCutGames.BinaryNameSearch.payloads line 260
  23. def OAI.MaxCutGames.BinaryNameSearch.afterMatch line 262
  24. def OAI.MaxCutGames.BinaryNameSearch.steps line 266
  25. def OAI.MaxCutGames.BinaryNameSearch.payloadSize line 272
  26. theorem OAI.MaxCutGames.BinaryNameSearch.stream_nil line 274
  27. theorem OAI.MaxCutGames.BinaryNameSearch.stream_cons line 276
  28. theorem OAI.MaxCutGames.BinaryNameSearch.payloads_nil line 279
  29. theorem OAI.MaxCutGames.BinaryNameSearch.payloads_cons line 281
  30. theorem OAI.MaxCutGames.BinaryNameSearch.payloadSize_nil line 284
  31. theorem OAI.MaxCutGames.BinaryNameSearch.payloadSize_cons line 286
  32. theorem OAI.MaxCutGames.BinaryNameSearch.stream_length line 289
  33. theorem OAI.MaxCutGames.BinaryNameSearch.steps_le line 299

    Source documentation

    Work is linear in the scanned payloads plus one key-copy cost per token.

    theorem steps_le (tokens : List Token) (key : List Bool) :
    steps tokens key ≤ 2 * payloadSize tokens + (3 * key.length + 6) * tokens.length := by
…

    Mentions: OAI.MaxCutGames.BinaryNameSearch.Token, OAI.MaxCutGames.BinaryNameSearch.steps, OAI.MaxCutGames.BinaryNameSearch.payloadSize

  34. theorem OAI.MaxCutGames.BinaryNameSearch.steps_le_stream line 309

    Source documentation

    This bound uses lengths of actual encoded words, not decoded name values.

    theorem steps_le_stream (tokens : List Token) (key : List Bool) :
    steps tokens key ≤ (3 * key.length + 7) * (stream tokens).length := by
…

    Mentions: OAI.MaxCutGames.BinaryNameSearch.Token, OAI.MaxCutGames.BinaryNameSearch.steps, OAI.MaxCutGames.BinaryNameSearch.stream

  35. abbrev OAI.MaxCutGames.BinaryNameSearch.Alphabet line 319
  36. abbrev OAI.MaxCutGames.BinaryNameSearch.State line 320
  37. abbrev OAI.MaxCutGames.BinaryNameSearch.clean line 322
  38. inductive OAI.MaxCutGames.BinaryNameSearch.Label line 324
  39. def OAI.MaxCutGames.BinaryNameSearch.compareTapes line 330
  40. theorem OAI.MaxCutGames.BinaryNameSearch.compareTapes_injective line 333
  41. def OAI.MaxCutGames.BinaryNameSearch.exitAt line 339
  42. def OAI.MaxCutGames.BinaryNameSearch.finish line 344
  43. def OAI.MaxCutGames.BinaryNameSearch.instruction line 347
  44. theorem OAI.MaxCutGames.BinaryNameSearch.stepAux_finish line 358
  45. theorem OAI.MaxCutGames.BinaryNameSearch.update_source_inline_MachineBinaryNameSearch line 362
  46. theorem OAI.MaxCutGames.BinaryNameSearch.update_counter_inline_MachineBinaryNameSearch line 373
  47. theorem OAI.MaxCutGames.BinaryNameSearch.joinTrace_inline_MachineBinaryNameSearch line 379
  48. theorem OAI.MaxCutGames.BinaryNameSearch.signStep line 392
  49. theorem OAI.MaxCutGames.BinaryNameSearch.emptyStep line 403
  50. theorem OAI.MaxCutGames.BinaryNameSearch.incrementStep line 414
  51. theorem OAI.MaxCutGames.BinaryNameSearch.tokenTrace line 425

    Source documentation

    One sign is consumed, then the actual shared scan/copy/compare routine runs.

    theorem tokenTrace (token : Token) (key suffix counter : List Bool)
    (canonical : BinaryNameMachine.canonical token.2 = true)
    (keyWord : base (tape 1) = key.reverse)
    (candidateEmpty : base (tape 2) = []) (copyEmpty : base (tape 3) = [])
    (scratchEmpty : base (tape 4) = []) :
    (advance (TM2.step program))^[1 + BinaryNameCompare.steps token.2.length key.length]
      (some ⟨some (labels .sign), clean ambient,
        tapesAt (tape 0) (tape 5) base (tokenBits token ++ suffix) counter⟩) =
      some ⟨if token.2 = key then foundExit else some (labels .increment), clean ambient,
        tapesAt (tape 0) (tape 5) base suffix counter⟩ := by
…

    Mentions: OAI.MaxCutGames.BinaryNameSearch.Token, OAI.MaxCutGames.BinaryNameMachine.canonical, OAI.MaxCutGames.BinaryNameCompare.steps, OAI.MaxCutGames.BinaryNameSearch.clean, OAI.MaxCutGames.BinaryNameSearch.tokenBits

  52. theorem OAI.MaxCutGames.BinaryNameSearch.searchTrace line 473

    Source documentation

    Successful search returns exactly the first occurrence index. All labels are literal instruction equations, so this theorem supplies its own body runs.

    theorem searchTrace (tokens : List Token) (key suffix counter : List Bool)
    (canonical : ∀ token ∈ tokens, BinaryNameMachine.canonical token.2 = true)
    (present : key ∈ payloads tokens)
    (keyWord : base (tape 1) = key.reverse)
    (candidateEmpty : base (tape 2) = []) (copyEmpty : base (tape 3) = [])
    (scratchEmpty : base (tape 4) = []) :
    (advance (TM2.step program))^[steps tokens key]
      (some ⟨some (labels .sign), clean ambient,
        tapesAt (tape 0) (tape 5) base (stream tokens ++ suffix) counter⟩) =
      some ⟨foundExit, clean ambient,
        tapesAt (tape 0) (tape 5) base (stream (afterMatch tokens key) ++ suffix)
          (List.replicate ((payloads tokens).idxOf key) true ++ counter)⟩ := by
…

    Mentions: OAI.MaxCutGames.BinaryNameSearch.Token, OAI.MaxCutGames.BinaryNameMachine.canonical, OAI.MaxCutGames.BinaryNameSearch.payloads, OAI.MaxCutGames.BinaryNameSearch.steps, OAI.MaxCutGames.BinaryNameSearch.clean, OAI.MaxCutGames.BinaryNameSearch.stream, OAI.MaxCutGames.BinaryNameSearch.afterMatch

  53. def OAI.MaxCutGames.BinaryNameSearch.searchInTime line 525

    Source documentation

    Explicit polynomial bound for the actual successful run.

    def searchInTime (tokens : List Token) (key suffix counter : List Bool)
    (canonical : ∀ token ∈ tokens, BinaryNameMachine.canonical token.2 = true)
    (present : key ∈ payloads tokens)
    (keyWord : base (tape 1) = key.reverse)
    (candidateEmpty : base (tape 2) = []) (copyEmpty : base (tape 3) = [])
    (scratchEmpty : base (tape 4) = []) :
    StateTransition.EvalsToInTime (TM2.step program)
      ⟨some (labels .sign), clean ambient,
        tapesAt (tape 0) (tape 5) base (stream tokens ++ suffix) counter⟩
      (some ⟨foundExit, clean ambient,
        tapesAt (tape 0) (tape 5) base (stream (afterMatch tokens key) ++ suffix)
          (List.replicate ((payloads tokens).idxOf key) true ++ counter)⟩)
…

    Mentions: OAI.MaxCutGames.BinaryNameSearch.Token, OAI.MaxCutGames.BinaryNameMachine.canonical, OAI.MaxCutGames.BinaryNameSearch.payloads, OAI.MaxCutGames.BinaryNameSearch.clean, OAI.MaxCutGames.BinaryNameSearch.stream, OAI.MaxCutGames.BinaryNameSearch.afterMatch

  54. def OAI.MaxCutGames.BinaryNameSearch.machine line 547

    Source documentation

    Concrete finite-control instantiation; the counter is its designated output.

    def machine : FinTM2 where
…
  55. theorem OAI.MaxCutGames.BinaryNameSearch.machine_finiteAlphabet line 560
  56. abbrev OAI.MaxCutGames.BinaryLiteralMachine.Alphabet line 575
  57. abbrev OAI.MaxCutGames.BinaryLiteralMachine.State line 576
  58. abbrev OAI.MaxCutGames.BinaryLiteralMachine.clean line 577
  59. inductive OAI.MaxCutGames.BinaryLiteralMachine.Label line 580
  60. def OAI.MaxCutGames.BinaryLiteralMachine.searchTapes line 588

    Source documentation

    Cursor, permanent stream, key, search stream, candidate, key-copy, copy scratch, index counter, reversed output.

    def searchTapes (tape : Fin 9 → K) : Fin 6 → K
  | 0 => tape 3
  | 1 => tape 2
  | 2 => tape 4
  | 3 => tape 5
  | 4 => tape 6
  | 5 => tape 7

omit [DecidableEq K] in
  61. theorem OAI.MaxCutGames.BinaryLiteralMachine.searchTapes_injective line 597
  62. def OAI.MaxCutGames.BinaryLiteralMachine.finish line 603
  63. def OAI.MaxCutGames.BinaryLiteralMachine.readSign line 609
  64. def OAI.MaxCutGames.BinaryLiteralMachine.emitSign line 617
  65. def OAI.MaxCutGames.BinaryLiteralMachine.instruction line 623
  66. def OAI.MaxCutGames.BinaryLiteralMachine.signWord line 643
  67. def OAI.MaxCutGames.BinaryLiteralMachine.index line 645
  68. def OAI.MaxCutGames.BinaryLiteralMachine.outputWord line 648
  69. def OAI.MaxCutGames.BinaryLiteralMachine.steps line 651
  70. theorem OAI.MaxCutGames.BinaryLiteralMachine.afterMatch_length_le line 657
  71. theorem OAI.MaxCutGames.BinaryLiteralMachine.steps_le line 666
  72. theorem OAI.MaxCutGames.BinaryLiteralMachine.stepAux_finish line 682
  73. theorem OAI.MaxCutGames.BinaryLiteralMachine.joinTrace_inline_MachineBinaryLiteralMachine line 686
  74. theorem OAI.MaxCutGames.BinaryLiteralMachine.literalTrace line 690
  75. def OAI.MaxCutGames.BinaryLiteralMachine.literalInTime line 861

    Source documentation

    Polynomial resource bound attached to the proved literal execution.

    def literalInTime (tape : Fin 9 → K) (distinct : Function.Injective tape)
    (labels : Label → Λ) (exit malformed : Option Λ)
    (program : Λ → TM2.Stmt (Alphabet (K := K)) Λ (State A))
…

    Mentions: OAI.MaxCutGames.BinaryLiteralMachine.Label, OAI.MaxCutGames.BinaryLiteralMachine.Alphabet, OAI.MaxCutGames.BinaryLiteralMachine.State