OAI/Combinatorics/ParityLifts/CompilerBounds.lean

GitHub source file

41 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ParityWL.Complexity.DataBound line 7
  2. lemma OAI.ParityWL.Complexity.DataBound.mass line 9
  3. inductive OAI.ParityWL.Complexity.BoundedExec line 13
  4. lemma OAI.ParityWL.Complexity.BoundedExec.start_bound line 20
  5. lemma OAI.ParityWL.Complexity.BoundedExec.end_bound line 23
  6. lemma OAI.ParityWL.Complexity.BoundedExec.work line 29
  7. abbrev OAI.ParityWL.Complexity.BoundedRuns line 40
  8. lemma OAI.ParityWL.Complexity.boundedHalt line 44
  9. lemma OAI.ParityWL.Complexity.boundedAtomic line 47
  10. lemma OAI.ParityWL.Complexity.BoundedExec.map line 52
  11. lemma OAI.ParityWL.Complexity.BoundedExec.andThen_right line 64
  12. lemma OAI.ParityWL.Complexity.BoundedExec.andThen line 70
  13. lemma OAI.ParityWL.Complexity.BoundedRuns.andThen line 94
  14. lemma OAI.ParityWL.Complexity.BoundedRuns.branch_true line 100
  15. lemma OAI.ParityWL.Complexity.BoundedRuns.branch_false line 110
  16. lemma OAI.ParityWL.Complexity.BoundedExec.repeat_true line 120
  17. lemma OAI.ParityWL.Complexity.BoundedExec.repeat_false line 130
  18. def OAI.ParityWL.Complexity.extendData line 154
  19. lemma OAI.ParityWL.Complexity.extendData_apply line 157
  20. lemma OAI.ParityWL.Complexity.extendData_outside line 161
  21. lemma OAI.ParityWL.Complexity.extendData_update line 165
  22. lemma OAI.ParityWL.Complexity.DataBound.extend line 177
  23. def OAI.ParityWL.Complexity.TreeOp.rename line 185
  24. lemma OAI.ParityWL.Complexity.TreeOp.rename_eval line 192
  25. def OAI.ParityWL.Complexity.TreeMachine.rename line 197
  26. lemma OAI.ParityWL.Complexity.BoundedExec.rename line 204
  27. def OAI.ParityWL.Complexity.TreeMachine.compiled line 216

    Source documentation

    A complete compiler from raw input bits, with explicit initialization and all serialization work charged.

    noncomputable def TreeMachine.compiled {Q : Type} [Fintype Q] {r : ℕ} (P : TreeMachine Q (r + 1)) : Machine :=
…

    Mentions: OAI.ParityWL.Complexity.TreeMachine, OAI.ParityWL.Complexity.Machine

  28. lemma OAI.ParityWL.Complexity.TreeRuns.compiled line 219
  29. lemma OAI.ParityWL.Complexity.BoundedRuns.compiled line 228
  30. lemma OAI.ParityWL.Complexity.DataBound.update line 242
  31. inductive OAI.ParityWL.Complexity.BCodeExec line 249
  32. lemma OAI.ParityWL.Complexity.BCodeExec.compile line 264
  33. lemma OAI.ParityWL.Complexity.BCodeExec.start_bound line 283
  34. lemma OAI.ParityWL.Complexity.BCodeExec.end_bound line 285
  35. lemma OAI.ParityWL.Complexity.BCodeExec.nil line 288
  36. lemma OAI.ParityWL.Complexity.BCodeExec.node line 293
  37. lemma OAI.ParityWL.Complexity.DataTree.size_child line 298
  38. lemma OAI.ParityWL.Complexity.BCodeExec.project line 302
  39. def OAI.ParityWL.Complexity.TreeCode.copy line 308

    Source documentation

    Copying is compiled, not a primitive constant-time operation of the tape model.

    def TreeCode.copy {r : ℕ} (dst src : Fin r) : TreeCode r :=
…

    Mentions: OAI.ParityWL.Complexity.TreeCode

  40. lemma OAI.ParityWL.Complexity.BCodeExec.copy line 311
  41. lemma OAI.ParityWL.Complexity.BCodeExec.mono line 318