ProgramBounds.lean`

28 declarations, 0 contain sorry, 0 declared as axioms

Compositional proofs of operation/word bounds.

structure OAI.PowerSaving.RAM.Bank line 13
Source documentation
Parameters for one uniform open code guarantee. When doing recursion proofs the index i can range over arbitrary environments including call bounds.
```
structure Bank (r : Port) (ι : Type U) where
…
```
Mentions: OAI.PowerSaving.RAM.Port
def OAI.PowerSaving.RAM.Bank.cap line 20
theorem OAI.PowerSaving.RAM.Bank.cm line 23
def OAI.PowerSaving.RAM.Bank.closed line 26
def OAI.PowerSaving.RAM.Bank.comap line 28
def OAI.PowerSaving.RAM.Able line 33
Source documentation
The charge Z is additive work allowed (used in body proofs for calls). Unlike the budget W it does not get an implicit constant multiplier.
```
def Able {r} {ι : Type U} (m : Bool) (b : Bank r ι) (s t)
    (x : ι → T s) (y : ι → T t) (W Z : ι → ℕ) : Prop :=
…
```
Mentions: OAI.PowerSaving.RAM.Bank

abbrev OAI.PowerSaving.RAM.Can line 39

Source documentation

Ordinary closed computation guarantee.

abbrev Can {ι : Type U} (m : Bool) (B : ι → ℕ) (s t)
    (x : ι → T s) (y : ι → T t) (W : ι → ℕ) : Prop :=
…

theorem OAI.PowerSaving.RAM.Able.reindex line 49
theorem OAI.PowerSaving.RAM.Able.cong line 55
theorem OAI.PowerSaving.RAM.Able.weaken line 59
theorem OAI.PowerSaving.RAM.Able.mono line 66

theorem OAI.PowerSaving.RAM.Able.rebank line 71

Source documentation

Change word budget.

theorem rebank {b' : Bank r ι} (h : Able m b s t x y W Z)
    (hB : Small b'.B b.B) (hH : ∀ i, b.ext i ≤ b'.ext i) (hU : b.use = b'.use) :
    Able m b' s t x y W Z := by
…

Mentions: OAI.PowerSaving.RAM.Bank, OAI.PowerSaving.RAM.Able, OAI.PowerSaving.RAM.Small

theorem OAI.PowerSaving.RAM.Able.combine_time line 80
theorem OAI.PowerSaving.RAM.Able.comp line 85
theorem OAI.PowerSaving.RAM.Able.comp_keep line 95
theorem OAI.PowerSaving.RAM.Able.fork line 99
theorem OAI.PowerSaving.RAM.Able.fork_keep line 110
theorem OAI.PowerSaving.RAM.Able.use_call line 114
theorem OAI.PowerSaving.RAM.Able.of_can line 122
Source documentation
Bring in a closed program; charges its work normally.
```
theorem of_can (h : Can m b.B s t x y W) :
    Able m b s t x y W (fun _ => 0) := by
…
```
Mentions: OAI.PowerSaving.RAM.Can, OAI.PowerSaving.RAM.Able
theorem OAI.PowerSaving.RAM.Able.atom_small line 134
Source documentation
One primitive, with whatever polynomial word bound its result takes.
```
theorem atom_small (f : Atom m s t) {P : ι → ℕ} (hP : Small b.B P)
    (h : ∀ i, (f.run (x i)).OK (y i) 1 (P i)) :
    Able m b s t x y W Z := by
…
```
Mentions: OAI.PowerSaving.RAM.Atom, OAI.PowerSaving.RAM.Small, OAI.PowerSaving.RAM.Able
theorem OAI.PowerSaving.RAM.Able.atom_one line 142
theorem OAI.PowerSaving.RAM.Able.id line 146
theorem OAI.PowerSaving.RAM.Able.first line 149
theorem OAI.PowerSaving.RAM.Able.second line 152
theorem OAI.PowerSaving.RAM.Able.fst line 155
theorem OAI.PowerSaving.RAM.Able.snd line 159

theorem OAI.PowerSaving.RAM.Able.save line 164

Source documentation

let-bind an expression, retaining environment.

theorem save (h : Able m b s t x y W Z)
    (g : Able m b (p s t) u (fun i => (x i,y i)) z W' Z') :
    Able m b s u x z (fun i => W i + W' i) (fun i => Z i + Z' i) := by
…

Mentions: OAI.PowerSaving.RAM.Able

theorem OAI.PowerSaving.RAM.Able.save_keep line 170