OAI/Combinatorics/ParityLifts/Compiler.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. inductive OAI.ParityWL.Complexity.TreeCode line 10

    Source documentation

    Finite structured imperative code. Loops are data-dependent, not bounded by an external oracle. The cost counts the serialized registers traversed by the stack compiler.

    inductive TreeCode (r : ℕ) where
…
  2. def OAI.ParityWL.Complexity.TreeCode.compile line 17
  3. inductive OAI.ParityWL.Complexity.CodeExec line 25
  4. lemma OAI.ParityWL.Complexity.CodeExec.compile line 40
  5. lemma OAI.ParityWL.Complexity.CodeExec.stack_run line 61

    Source documentation

    One code derivation yields a multitape computation, after input register initialization. No complexity-class closure theorem is assumed.

    lemma CodeExec.stack_run {r : ℕ} {p : TreeCode r} {d e : Fin r → DataTree} {n : ℕ}
    (h : CodeExec p d n e) : ∃ m, m ≤ 51 * n ∧
      Runs p.compile.program.lower.lower (dataWords d) m (dataWords e) true := by
…

    Mentions: OAI.ParityWL.Complexity.TreeCode, OAI.ParityWL.Complexity.DataTree, OAI.ParityWL.Complexity.CodeExec, OAI.ParityWL.Complexity.Runs, OAI.ParityWL.Complexity.dataWords

  6. lemma OAI.ParityWL.Complexity.Runs.repeat_true line 71
  7. lemma OAI.ParityWL.Complexity.Runs.repeat_false line 76
  8. def OAI.ParityWL.Complexity.pushWord line 83
  9. lemma OAI.ParityWL.Complexity.pushWord_run line 87
  10. def OAI.ParityWL.Complexity.bitChunk line 101
  11. def OAI.ParityWL.Complexity.DataTree.ofBits line 103
  12. lemma OAI.ParityWL.Complexity.ofBits_code line 107
  13. def OAI.ParityWL.Complexity.expandBit line 113
  14. def OAI.ParityWL.Complexity.expandBitsBody line 116
  15. def OAI.ParityWL.Complexity.expandBits line 121
  16. lemma OAI.ParityWL.Complexity.expandBit_run line 123
  17. lemma OAI.ParityWL.Complexity.expandBits_run line 133
  18. def OAI.ParityWL.Complexity.readBits line 183
  19. lemma OAI.ParityWL.Complexity.bitChunk_length line 186
  20. lemma OAI.ParityWL.Complexity.flatMap_bitChunk_length line 188
  21. lemma OAI.ParityWL.Complexity.readBits_run line 195
  22. def OAI.ParityWL.Complexity.inputData line 219
  23. def OAI.ParityWL.Complexity.inputStacks line 222
  24. def OAI.ParityWL.Complexity.fillData line 225
  25. def OAI.ParityWL.Complexity.initializeData line 229
  26. lemma OAI.ParityWL.Complexity.initializeData_run line 232