Clock.lean`

19 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Superstring.BitCode.Program.counter_loop line 11

Source documentation

Execute a reserved loop counter, with a uniform bound for each body call. There is no test of an arbitrary predicate: only this counter is tested.

theorem counter_loop (b : Block (K ⊕ ℕ)) (f : Store K → Store K)
    (d N M C : ℕ)
    (hb : ∀ s z, Clean d z → (z 0).length = N → Bounded s M →
      ∃ n ≤ C, b.Exec (Sum.elim s z) (Sum.elim (f s) z) n)
    (s : Store K) (z : Store ℕ) (hz : Clean d z) (hN : (z 0).length = N)
    (hinv : ∀ i ≤ (z (d + 2)).length, Bounded (f^[i] s) M) :
    ∃ n ≤ (z (d + 2)).length * (C + 2) + 1,
      (Block.loop (.inr (d + 2)) (.seq (.pop (.inr (d + 2))) b)).Exec
        (Sum.elim s z)
        (Sum.elim (f^[(z (d + 2)).length] s) (Function.update z (d + 2) [])) n := by
…

Mentions: OAI.Superstring.BitCode.Block, OAI.Superstring.BitCode.Store, OAI.Superstring.BitCode.Program.Clean, OAI.Superstring.BitCode.Program.Bounded

def OAI.Superstring.BitCode.Program.clock line 59
Source documentation
Uniform bit clock; the polynomial work counts syntactic bounded iterations.
```
def clock (w N M : ℕ) : ℕ := 13 * w * (M + N + w + 1)
```
theorem OAI.Superstring.BitCode.Program.clock_add line 61
theorem OAI.Superstring.BitCode.Program.clock_step line 66
theorem OAI.Superstring.BitCode.Program.clock_loop line 72
theorem OAI.Superstring.BitCode.Program.compile_exec line 96
Source documentation
Complete correctness and a polynomial bit-clock for bounded-loop programs.
```
theorem compile_exec (p : Program K) (N : ℕ) (s : Store K) (M : ℕ)
    (hs : Bounded s M) (z : Store ℕ) (hz : Clean p.depth z)
    (hN : (z 0).length = N) :
    ∃ n ≤ clock (p.work N) N M,
      p.compile.Exec (Sum.elim s z) (Sum.elim (p.run N s) z) n := by
…
```
Mentions: OAI.Superstring.BitCode.Program, OAI.Superstring.BitCode.Store, OAI.Superstring.BitCode.Program.Bounded, OAI.Superstring.BitCode.Program.Clean, OAI.Superstring.BitCode.Program.clock
theorem OAI.Superstring.BitCode.single_bounded line 193
theorem OAI.Superstring.BitCode.Block.Exec.frame line 200
Source documentation
No syntax can modify a register it does not mention.
```
theorem Exec.frame {b : Block K} {s t : Store K} {n : ℕ} (h : b.Exec s t n)
    (k : K) (hk : k ∉ b.support) : t k = s k := by
…
```
Mentions: OAI.Superstring.BitCode.Block, OAI.Superstring.BitCode.Store
theorem OAI.Superstring.BitCode.Block.Exec.bounded line 217
Source documentation
The maximum stack length, unlike the total size, needs no finiteness of the ambient register type. A finite code will subsequently be restricted to its support.
```
theorem Exec.bounded {b : Block K} {s t : Store K} {n : ℕ} (h : b.Exec s t n)
    (M : ℕ) (hs : Program.Bounded s M) : Program.Bounded t (M + n) := by
…
```
Mentions: OAI.Superstring.BitCode.Block, OAI.Superstring.BitCode.Store, OAI.Superstring.BitCode.Program.Bounded
def OAI.Superstring.BitCode.Block.clearMany line 236
def OAI.Superstring.BitCode.Block.cleared line 240
theorem OAI.Superstring.BitCode.Block.clearMany_exec line 242

theorem OAI.Superstring.BitCode.Block.certificate_any line 262

Source documentation

Restrict to the finitely many registers used by the actual finite code. This proves that infinite ambient names are merely notation, not infinite memory in the delivered machine. Every restricted alphabet is Bool.

theorem certificate_any {α β : Type} (ea : α → List Bool) (eb : β → List Bool)
    (Φ : α → β) (b : Block K) (i o : K) (P : Polynomial ℕ)
    (correct : ∀ a, ∃ n ≤ P.eval (ea a).length,
      b.Exec (single i (ea a)) (single o (eb (Φ a))) n) :
    ∃ M : Turing.TM2ComputableInPolyTime ea eb Φ, ∀ k : M.tm.K, Finite (M.tm.Γ k) := by
…

Mentions: OAI.Superstring.BitCode.Block, OAI.Superstring.BitCode.single

theorem OAI.Superstring.BitCode.Block.certificate_observed line 303

Source documentation

Uniformly erase every used non-output stack. A proof of the observed output and a polynomial clock suffice; hidden garbage is neither permitted nor assumed away in the exact Mathlib final configuration.

theorem certificate_observed {α β : Type} (ea : α → List Bool) (eb : β → List Bool)
    (Φ : α → β) (b : Block K) (i o : K) (P : Polynomial ℕ)
    (correct : ∀ a, ∃ n t, n ≤ P.eval (ea a).length ∧
      b.Exec (single i (ea a)) t n ∧ t o = eb (Φ a)) :
    ∃ M : Turing.TM2ComputableInPolyTime ea eb Φ, ∀ k : M.tm.K, Finite (M.tm.Γ k) := by
…

Mentions: OAI.Superstring.BitCode.Block, OAI.Superstring.BitCode.single

theorem OAI.Superstring.BitCode.Program.certificate line 350

Source documentation

A syntactically bounded-loop program gives a polynomial-time certificate, including finite alphabets and erasure of temporary registers.

theorem certificate {α β : Type} (ea : α → List Bool) (eb : β → List Bool)
    (f : α → β) (p : Program K) (i o : K)
    (correct : ∀ a, (p.run (ea a).length (single i (ea a))) o = eb (f a)) :
    ∃ M : Turing.TM2ComputableInPolyTime ea eb f, ∀ k : M.tm.K, Finite (M.tm.Γ k) := by
…

Mentions: OAI.Superstring.BitCode.Program, OAI.Superstring.BitCode.single

theorem OAI.Superstring.BitCode.Block.update_left line 397
theorem OAI.Superstring.BitCode.Block.update_right line 404
theorem OAI.Superstring.BitCode.Block.Exec.left line 413
Source documentation
Renaming into a disjoint register bank preserves a run and frames the entire other bank, even when that other bank contains nonempty data.
```
theorem Exec.left {b : Block K} {s t : Store K} {n : ℕ} (h : b.Exec s t n)
    (r : Store L) : (b.rename Sum.inl).Exec (Sum.elim s r) (Sum.elim t r) n := by
…
```
Mentions: OAI.Superstring.BitCode.Block, OAI.Superstring.BitCode.Store, OAI.Superstring.BitCode.Block.Exec
theorem OAI.Superstring.BitCode.Block.Exec.right line 428