OAI/Computability/RationalHitting/DenseRecords.lean

GitHub source file

43 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.RationalHitting.StackLanguage.codeWord line 9

    Source documentation

    Self-delimiting word records (distinct from the final output encoding).

    def codeWord : List Bool → List Bool
  | [] => [true]
  | b::w => false::b::codeWord w
  2. theorem OAI.RationalHitting.StackLanguage.codeWord_length line 13
  3. def OAI.RationalHitting.StackLanguage.pairWord line 16
  4. lemma OAI.RationalHitting.StackLanguage.pairWord_nil line 17
  5. lemma OAI.RationalHitting.StackLanguage.pairWord_cons line 18
  6. lemma OAI.RationalHitting.StackLanguage.pairWord_append line 20
  7. lemma OAI.RationalHitting.StackLanguage.codeWord_pair line 22
  8. def OAI.RationalHitting.StackLanguage.packLoop line 25
  9. lemma OAI.RationalHitting.StackLanguage.eval_packLoop line 28
  10. def OAI.RationalHitting.StackLanguage.packRecord line 54

    Source documentation

    Consume a binary word, prepending one encoded reversed record.

    def packRecord : Program (Fin 3) := .seq (.push 1 true) (packLoop 0 1)

    Mentions: OAI.RationalHitting.StackLanguage.Program, OAI.RationalHitting.StackLanguage.packLoop

  11. lemma OAI.RationalHitting.StackLanguage.eval_packRecord line 56
  12. def OAI.RationalHitting.StackLanguage.unpackBody line 70
  13. lemma OAI.RationalHitting.StackLanguage.eval_unpackLoop line 73
  14. def OAI.RationalHitting.StackLanguage.unpackRecord line 109

    Source documentation

    Remove one self-delimiting record; produce its reversed binary word.

    def unpackRecord : Program (Fin 3) := .seq (.push 2 true) (.loop 2 unpackBody)

    Mentions: OAI.RationalHitting.StackLanguage.Program, OAI.RationalHitting.StackLanguage.unpackBody

  15. lemma OAI.RationalHitting.StackLanguage.eval_unpackRecord line 111
  16. def OAI.RationalHitting.StackLanguage.codeArray line 130

    Source documentation

    Dense serialized arrays of variable-width binary records.

    def codeArray (ws : List (List Bool)) : List Bool := ws.flatMap codeWord

    Mentions: OAI.RationalHitting.StackLanguage.codeWord

  17. lemma OAI.RationalHitting.StackLanguage.codeArray_nil line 131
  18. lemma OAI.RationalHitting.StackLanguage.codeArray_cons line 132
  19. lemma OAI.RationalHitting.StackLanguage.codeArray_append line 134
  20. lemma OAI.RationalHitting.StackLanguage.codeArray_nonempty line 137
  21. def OAI.RationalHitting.StackLanguage.unpackMove line 144
  22. def OAI.RationalHitting.StackLanguage.packMove line 145
  23. def OAI.RationalHitting.StackLanguage.recordMove line 146
  24. lemma OAI.RationalHitting.StackLanguage.eval_recordMove line 149
  25. lemma OAI.RationalHitting.StackLanguage.eval_recordMove_rename line 182
  26. def OAI.RationalHitting.StackLanguage.arrayForward line 191
  27. def OAI.RationalHitting.StackLanguage.arrayBackward line 192
  28. def OAI.RationalHitting.StackLanguage.scanBody line 193
  29. def OAI.RationalHitting.StackLanguage.scan line 194
  30. def OAI.RationalHitting.StackLanguage.scanCost line 197

    Source documentation

    Number of real finite-stack macrosteps for scanning a given prefix.

    def scanCost (ws : List (List Bool)) : ℕ :=
…
  31. lemma OAI.RationalHitting.StackLanguage.eval_scan line 200
  32. lemma OAI.RationalHitting.StackLanguage.scanCost_bound line 228
  33. def OAI.RationalHitting.StackLanguage.restore line 240
  34. def OAI.RationalHitting.StackLanguage.restoreCost line 241
  35. lemma OAI.RationalHitting.StackLanguage.eval_restore line 244
  36. lemma OAI.RationalHitting.StackLanguage.restoreCost_bound line 266
  37. lemma OAI.RationalHitting.StackLanguage.codeArray_reverse_length line 273
  38. def OAI.RationalHitting.StackLanguage.peekUnpack line 277
  39. def OAI.RationalHitting.StackLanguage.peekPack line 278
  40. def OAI.RationalHitting.StackLanguage.peekRecord line 279
  41. lemma OAI.RationalHitting.StackLanguage.eval_peekRecord line 283
  42. def OAI.RationalHitting.StackLanguage.arrayRead line 314

    Source documentation

    Indexed read. Register 4 is a unary index; register 0 is a serialized array and is restored byte-for-byte. Register 5 receives the exact binary word.

    def arrayRead : Program (Fin 8) := .seq scan (.seq peekRecord restore)

    Mentions: OAI.RationalHitting.StackLanguage.Program, OAI.RationalHitting.StackLanguage.scan, OAI.RationalHitting.StackLanguage.peekRecord, OAI.RationalHitting.StackLanguage.restore

  43. theorem OAI.RationalHitting.StackLanguage.eval_arrayRead line 316