OAI/Computability/UniqueGames/Machines/MachineBinaryParsingLemmas.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

Soundness of the ordinary-binary parser and its concrete name-scanning machine. Every successful parse consumes exactly a canonical encoding and leaves its stated suffix. Thus malformed or noncanonical bitstrings cannot name an extra formula. The finite scanner's final-digit test is proved equivalent to the codec's arithmetic canonicality test.

  1. theorem OAI.UniqueGamesTheorem.BinaryParsing.frame_eq line 21
  2. theorem OAI.UniqueGamesTheorem.BinaryParsing.canonical_cons_cons line 26
  3. theorem OAI.UniqueGamesTheorem.BinaryParsing.canonical_iff line 31

    Source documentation

    A payload has no redundant high zero precisely when its last digit is one, with the empty payload representing zero.

    theorem canonical_iff (bits : List Bool) :
    BinaryNameMachine.canonical bits = true ↔ (bitsValue bits).bits = bits := by
…

    Mentions: OAI.UniqueGamesTheorem.BinaryNameMachine.canonical

  4. theorem OAI.UniqueGamesTheorem.BinaryParsing.canonical_nat_bits line 56
  5. theorem OAI.UniqueGamesTheorem.BinaryParsing.parseFrame_sound line 61
  6. theorem OAI.UniqueGamesTheorem.BinaryParsing.parseName_sound line 85
  7. theorem OAI.UniqueGamesTheorem.BinaryParsing.parseLiteral_sound line 101
  8. theorem OAI.UniqueGamesTheorem.BinaryParsing.parseClause_sound line 116
  9. theorem OAI.UniqueGamesTheorem.BinaryParsing.parseClauses_sound line 140
  10. theorem OAI.UniqueGamesTheorem.BinaryParsing.decodeFormula_sound line 168
  11. theorem OAI.UniqueGamesTheorem.BinaryParsing.decodeFormula_eq_some_iff line 182
  12. theorem OAI.UniqueGamesTheorem.BinaryParsing.scanSpec_nameBits line 188

    Source documentation

    Exact agreement of the finite-state name scanner with a canonical encoded name, including the untouched suffix and the actual binary payload stack.

    theorem scanSpec_nameBits (name : Nat) (suffix output : List Bool) :
    BinaryNameMachine.scanSpec (nameBits name ++ suffix) output none =
      ⟨true, suffix, name.bits.reverse ++ output⟩ := by
…

    Mentions: OAI.UniqueGamesTheorem.BinaryNameMachine.scanSpec

  13. def OAI.UniqueGamesTheorem.BinaryLanguage.rejectBinary line 215
  14. theorem OAI.UniqueGamesTheorem.BinaryLanguage.rejectBinary_unsatisfiable line 219
  15. def OAI.UniqueGamesTheorem.BinaryLanguage.rejectFormula line 228
  16. theorem OAI.UniqueGamesTheorem.BinaryLanguage.reject_unsatisfiable line 230
  17. def OAI.UniqueGamesTheorem.BinaryLanguage.totalParsed line 234
  18. def OAI.UniqueGamesTheorem.BinaryLanguage.totalRename line 237
  19. theorem OAI.UniqueGamesTheorem.BinaryLanguage.totalParsed_satisfiable_iff line 240
  20. theorem OAI.UniqueGamesTheorem.BinaryLanguage.totalRename_satisfiable_iff line 246
  21. theorem OAI.UniqueGamesTheorem.BinaryLanguage.totalRename_encoded line 251
  22. theorem OAI.UniqueGamesTheorem.BinaryLanguage.language_encoded line 255
  23. theorem OAI.UniqueGamesTheorem.BinaryLanguage.reject_bits_length line 259
  24. theorem OAI.UniqueGamesTheorem.BinaryLanguage.totalRename_output_length line 261