OAI/Computability/WLIdentification/BoundedWords.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

  1. inductive OAI.WLIdentification.BoundedWords.Program line 12

    Source documentation

    Word-register programs with bounded, captured-count loops. No unbounded natural register, whole-input transition or host-language oracle is available.

    inductive Program (K : Type) where
…
  2. def OAI.WLIdentification.BoundedWords.Program.eval line 25
  3. def OAI.WLIdentification.BoundedWords.Program.Size line 38
  4. def OAI.WLIdentification.BoundedWords.Program.Fits line 42

    Source documentation

    An explicit bound on all data consumed by an execution. Proving this invariant for an algorithm, rather than assuming its runtime, yields a cost.

    def Fits : Program K → (K → Word) → ℕ → Prop
  | .skip, S, B | .clear _, S, B | .push _ _, S, B | .pop _, S, B | .copy _ _, S, B => Size S B
  | .seq p q, S, B => p.Fits S B ∧ q.Fits (p.eval S) B
  | .cases k nil zero one, S, B => Size S B ∧ match (S k).getLast? with
      | none => nil.Fits S B
      | some false => zero.Fits S B
      | some true => one.Fits S B
  | .repeat k p, S, B => Size S B ∧ ∀ i < (S k).length, p.Fits (p.eval^[i] S) B

    Mentions: OAI.WLIdentification.BoundedWords.Program, OAI.WLIdentification.Word, OAI.WLIdentification.BoundedWords.Program.Size

  5. abbrev OAI.WLIdentification.BoundedWords.Program.Work line 51
  6. instance OAI.WLIdentification.BoundedWords.Program.workFintype line 58
  7. instance OAI.WLIdentification.BoundedWords.Program.workDecidableEq line 60
  8. def OAI.WLIdentification.BoundedWords.Program.cost line 68
  9. def OAI.WLIdentification.BoundedWords.Program.compile line 77
  10. theorem OAI.WLIdentification.BoundedWords.Program.cost_polynomial line 97

    Source documentation

    Every syntactic cost is polynomial in the maintained word bound; its constants depend on finite code, not the input or loop counts.

    theorem cost_polynomial (p : Program K) : ∃ C d : ℕ, ∀ B, p.cost B ≤ C * (B + 1)^d := by
…

    Mentions: OAI.WLIdentification.BoundedWords.Program

  11. theorem OAI.WLIdentification.BoundedWords.Program.elim_empty line 148
  12. theorem OAI.WLIdentification.BoundedWords.Program.update_inl line 152
  13. def OAI.WLIdentification.BoundedWords.Program.Correct line 159
  14. theorem OAI.WLIdentification.BoundedWords.Program.correct_skip line 163
  15. theorem OAI.WLIdentification.BoundedWords.Program.correct_clear line 167
  16. theorem OAI.WLIdentification.BoundedWords.Program.correct_push line 173
  17. theorem OAI.WLIdentification.BoundedWords.Program.correct_pop line 180
  18. theorem OAI.WLIdentification.BoundedWords.Program.correct_copy line 187
  19. theorem OAI.WLIdentification.BoundedWords.Program.correct_seq line 205
  20. theorem OAI.WLIdentification.BoundedWords.Program.correct_cases line 213
  21. def OAI.WLIdentification.BoundedWords.Program.counterData line 284
  22. def OAI.WLIdentification.BoundedWords.Program.loopState line 286
  23. theorem OAI.WLIdentification.BoundedWords.Program.loopState_var line 290
  24. theorem OAI.WLIdentification.BoundedWords.Program.loopState_counter line 293
  25. theorem OAI.WLIdentification.BoundedWords.Program.loopState_temp line 296
  26. theorem OAI.WLIdentification.BoundedWords.Program.loopState_empty line 300
  27. theorem OAI.WLIdentification.BoundedWords.Program.update_counter line 309
  28. theorem OAI.WLIdentification.BoundedWords.Program.drain_repeat line 320

    Source documentation

    The captured counter is consumed one bit per loop, independently of all public registers modified by the body.

    theorem drain_repeat {p : Program K} (hp : Correct p) (B : ℕ) (S : K → Word) (w : Word)
    (hfit : ∀ i < w.length, p.Fits (p.eval^[i] S) B) (s : Option Bool) :
    ∃ n ≤ (p.cost B + 2) * w.length + 2,
      Exec (drain (.inr (.inr false)) (p.compile.rename embedLeft)) s (loopState S w) none
        (loopState (p.eval^[w.length] S) []) n := by
…

    Mentions: OAI.WLIdentification.BoundedWords.Program, OAI.WLIdentification.BoundedWords.Program.Correct, OAI.WLIdentification.Word, OAI.WLIdentification.BoundedWords.Program.loopState

  29. theorem OAI.WLIdentification.BoundedWords.Program.correct_repeat line 359
  30. theorem OAI.WLIdentification.BoundedWords.Program.correct line 379

    Source documentation

    Fully uniform compilation, with all work stacks again empty at the boundary.

    theorem correct (p : Program K) : p.Correct := by
…

    Mentions: OAI.WLIdentification.BoundedWords.Program