OAI/Computability/UniqueGames/Machines/MachineBinaryNameCompare.lean

GitHub source file

18 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.UniqueGamesTheorem.BinaryNameCompare.Alphabet line 23
  2. abbrev OAI.UniqueGamesTheorem.BinaryNameCompare.State line 24
  3. def OAI.UniqueGamesTheorem.BinaryNameCompare.clean line 26
  4. def OAI.UniqueGamesTheorem.BinaryNameCompare.scanStateEquiv line 28
  5. def OAI.UniqueGamesTheorem.BinaryNameCompare.compareStateEquiv line 34
  6. inductive OAI.UniqueGamesTheorem.BinaryNameCompare.Label line 40
  7. abbrev OAI.UniqueGamesTheorem.BinaryNameCompare.Label.enumList line 44
  8. theorem OAI.UniqueGamesTheorem.BinaryNameCompare.Label.enumList_getElem?_ctorIdx_eq line 46
  9. theorem OAI.UniqueGamesTheorem.BinaryNameCompare.Label.enumList_nodup line 50
  10. instance OAI.UniqueGamesTheorem.BinaryNameCompare.(instance at line 52) line 52
  11. def OAI.UniqueGamesTheorem.BinaryNameCompare.instruction line 57

    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.UniqueGamesTheorem.BinaryNameCompare.Label, OAI.UniqueGamesTheorem.BinaryNameCompare.Alphabet, OAI.UniqueGamesTheorem.BinaryNameCompare.State

  12. def OAI.UniqueGamesTheorem.BinaryNameCompare.steps line 70
  13. theorem OAI.UniqueGamesTheorem.BinaryNameCompare.steps_le line 73
  14. theorem OAI.UniqueGamesTheorem.BinaryNameCompare.joinTrace line 78
  15. theorem OAI.UniqueGamesTheorem.BinaryNameCompare.compareTrace line 84

    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.UniqueGamesTheorem.BinaryNameCompare.Label, OAI.UniqueGamesTheorem.BinaryNameCompare.Alphabet, OAI.UniqueGamesTheorem.BinaryNameCompare.State

  16. def OAI.UniqueGamesTheorem.BinaryNameCompare.compareInTime line 189

    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.UniqueGamesTheorem.BinaryNameCompare.Label, OAI.UniqueGamesTheorem.BinaryNameCompare.Alphabet, OAI.UniqueGamesTheorem.BinaryNameCompare.State

  17. def OAI.UniqueGamesTheorem.BinaryNameCompare.machine line 212

    Source documentation

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

    def machine : FinTM2 where
…
  18. theorem OAI.UniqueGamesTheorem.BinaryNameCompare.machine_finiteAlphabet line 225