RAM.lean`

33 declarations, 0 contain sorry, 0 declared as axioms

Exact scalar and index RAM used for the algorithm

Finite, first-order, expression/program syntax. Arrays below are random-access arrays of registers (an array-valued register holds its address). An expression building an array uses a fresh array; sow builds by a loop of writes instead of a loop supplying consecutive entries. Programs have their usual sequential stack evaluation. Evaluation here records work (including stack, index and array work), the high water mark on produced/logically looped-over integer values (addresses within arrays are integers too), the value, and the side condition required along the executed path (in particular no division by zero). The charged units of work are constant time; as usual constant rescalings between ways to charge a fixed number of scalar or address operations are immaterial.

Enough address bits must be provided BOTH for the integer high water mark (and inputs), AND for the work bound together with input size, as will be required in the theorem. Indeed we use the particularly simple RAM convention where temporaries aren't reused: one work unit can leave at most a constant number of cells (stack, pairs or array cells); whenever many array entries are made their number is charged. So a constant number of words of those sizes also suffices for arena addresses. Nothing charges constant work for changing an already published array to a different array as a whole. Register and stack layouts, and the convention whether registers hold pairs or addresses of pairs, only have constant factors (the program is fixed).

Scalar and data field registers are separated. Tests and loop/request sizes are on nonnegative integer registers. There is no instruction for an arbitrary complex constant. A supplied specified root will be an input. Divisions are on prepared scalars; valid runs require every such denominator nonzero; the side condition is not a test performed by the algorithm. The Bool mode on the syntax allows or prohibits general products (two-input convolution versus the transform); even when allowed we use separate register kinds before and after the bilinear products.

Definitions are mathematical operation-count semantics, not a model of running Lean code. E.g. a function on Fin n represents the n cells of a random-access array, not a function closure at runtime.

structure OAI.PowerSaving.Tape line 47
Source documentation
Register arrays.
Also declared: ComparatorChallenges/UniformFourier.lean:51 (same declaration text).
```
structure Tape (α : Type u) where
…
```
def OAI.PowerSaving.Tape.empty line 53
Also declared: ComparatorChallenges/UniformFourier.lean:57 (same declaration text).
def OAI.PowerSaving.Tape.tab line 56
Source documentation
Materialized array.
Also declared: ComparatorChallenges/UniformFourier.lean:60 (same declaration text).
```
def tab (n : ℕ) (f : ℕ → α) : Tape α := ⟨n, fun i => f i.val⟩
```
Mentions: OAI.PowerSaving.Tape
def OAI.PowerSaving.Tape.look line 59
Source documentation
Read with fixed out of bounds default.
Also declared: ComparatorChallenges/UniformFourier.lean:63 (same declaration text).
```
def look (v : Tape α) (i : ℕ) (z : α) : α :=
…
```
Mentions: OAI.PowerSaving.Tape
theorem OAI.PowerSaving.Tape.look_of_lt line 62
Also declared: ComparatorChallenges/UniformFourier.lean:66 (same declaration text).
theorem OAI.PowerSaving.Tape.look_of_le line 65
Also declared: ComparatorChallenges/UniformFourier.lean:69 (same declaration text).
def OAI.PowerSaving.Tape.set line 70
Source documentation
Semantics of a write into fresh storage; out-of-range writes are ignored. Only used during construction, never a whole-tape functional update instruction.
Also declared: ComparatorChallenges/UniformFourier.lean:74 (same declaration text).
```
def set (v : Tape α) (i : ℕ) (x : α) : Tape α :=
…
```
Mentions: OAI.PowerSaving.Tape
def OAI.PowerSaving.Tape.sow line 73
Also declared: ComparatorChallenges/UniformFourier.lean:77 (same declaration text).
def OAI.PowerSaving.Tape.map line 80
Also declared: ComparatorChallenges/UniformFourier.lean:84 (same declaration text).
inductive OAI.PowerSaving.RAM.Paint line 86
Also declared: ComparatorChallenges/UniformFourier.lean:90 (same declaration text).
inductive OAI.PowerSaving.RAM.Ty line 92
Also declared: ComparatorChallenges/UniformFourier.lean:96 (same declaration text).
abbrev OAI.PowerSaving.RAM.sc line 100
Also declared: ComparatorChallenges/UniformFourier.lean:104 (same declaration text).
def OAI.PowerSaving.RAM.Ty.T line 102
Also declared: ComparatorChallenges/UniformFourier.lean:106 (same declaration text).
def OAI.PowerSaving.RAM.Ty.blank line 108
Also declared: ComparatorChallenges/UniformFourier.lean:112 (same declaration text).
structure OAI.PowerSaving.RAM.Bill line 117
Source documentation
One basic work unit below pays for O(1) primitive RAM operations; includes loop and stack overhead. peak tracks produced/needed integer quantities beyond inputs (total allocation for stack and array bases is covered separately by work).
Also declared: ComparatorChallenges/UniformFourier.lean:121 (same declaration text).
```
structure Bill (α : Type u) where
…
```
def OAI.PowerSaving.RAM.Bill.pay line 126
Source documentation
Charge some work and optionally a new word bound.
Also declared: ComparatorChallenges/UniformFourier.lean:130 (same declaration text).
```
def pay (b : Bill α) (n : ℕ) (m : ℕ) : Bill α :=
…
```
Mentions: OAI.PowerSaving.RAM.Bill
def OAI.PowerSaving.RAM.Bill.pass line 130
Source documentation
Both computations are evaluated.
Also declared: ComparatorChallenges/UniformFourier.lean:134 (same declaration text).
```
def pass (b : Bill α) (f : α → Bill β) : Bill β :=
…
```
Mentions: OAI.PowerSaving.RAM.Bill
def OAI.PowerSaving.RAM.Bill.one line 134
Also declared: ComparatorChallenges/UniformFourier.lean:138 (same declaration text).
def OAI.PowerSaving.RAM.Bill.word line 135
Also declared: ComparatorChallenges/UniformFourier.lean:139 (same declaration text).
def OAI.PowerSaving.RAM.Bill.steps line 138
Source documentation
Execute f 0 through f (n-1), iterating an accumulator.
Also declared: ComparatorChallenges/UniformFourier.lean:142 (same declaration text).
```
def steps (init : α) (f : ℕ → α → Bill α) : ℕ → Bill α
  | 0 => Bill.one init
  | i+1 => ((steps init f i).pass (f i)).pay 1 (i+1)

/-- Build Tape len by count writes (initialized with a blank z). -/
```
Mentions: OAI.PowerSaving.RAM.Bill, OAI.PowerSaving.RAM.Bill.one, OAI.PowerSaving.RAM.Bill.pass, OAI.PowerSaving.RAM.Bill.pay, OAI.PowerSaving.Tape
def OAI.PowerSaving.RAM.Bill.sow line 143
Source documentation
Build Tape len by count writes (initialized with a blank z).
Also declared: ComparatorChallenges/UniformFourier.lean:147 (same declaration text).
```
def sow (len count : ℕ) (z : α) (f : ℕ → Bill (ℕ × α)) : Bill (Tape α) :=
…
```
Mentions: OAI.PowerSaving.RAM.Bill, OAI.PowerSaving.Tape
def OAI.PowerSaving.RAM.Bill.tab line 148
Source documentation
Build Tape len. As for sow we can first allocate then perform writes.
Also declared: ComparatorChallenges/UniformFourier.lean:152 (same declaration text).
```
def tab (len : ℕ) (z : α) (f : ℕ → Bill α) : Bill (Tape α) :=
…
```
Mentions: OAI.PowerSaving.RAM.Bill, OAI.PowerSaving.Tape
inductive OAI.PowerSaving.RAM.NOp line 153
Also declared: ComparatorChallenges/UniformFourier.lean:157 (same declaration text).
inductive OAI.PowerSaving.RAM.Atom line 156
Also declared: ComparatorChallenges/UniformFourier.lean:160 (same declaration text).
def OAI.PowerSaving.RAM.NOp.run line 173
Also declared: ComparatorChallenges/UniformFourier.lean:177 (same declaration text).
def OAI.PowerSaving.RAM.Atom.run line 181
Also declared: ComparatorChallenges/UniformFourier.lean:185 (same declaration text).
abbrev OAI.PowerSaving.RAM.Port line 197
Also declared: ComparatorChallenges/UniformFourier.lean:201 (same declaration text).

inductive OAI.PowerSaving.RAM.Code line 202

Source documentation

call is internal for bounded recursion; a program has Port = none. loop, tab and sow retain the input to access parameters in the body. descend sets up bounded recursion, reading fuel and initial argument.

Also declared: ComparatorChallenges/UniformFourier.lean:206 (same declaration text).

inductive Code (allow : Bool) : Port → Ty → Ty → Type
  | atom {r s t} (op : Atom allow s t) : Code allow r s t
  | comp {r s t u} (f : Code allow r s t) (g : Code allow r t u) : Code allow r s u
  | fork {r s t u} (f : Code allow r s t) (g : Code allow r s u) : Code allow r s (p t u)
  | ifz {r s t} (q : Code allow r s w) (f g : Code allow r s t) : Code allow r s t
  | loop {r s t} (n : Code allow r s w) (init : Code allow r s t)
      (body : Code allow r (p s (p w t)) t) : Code allow r s t
  | tab {r s t} (n : Code allow r s w)
      (body : Code allow r (p s w) t) : Code allow r s (a t)
  | sow {r s t} (n count : Code allow r s w)
      (body : Code allow r (p s w) (p w t)) : Code allow r s (a t)
  | importClosed {r s t} (f : Code allow none s t) : Code allow r s t
…

Mentions: OAI.PowerSaving.RAM.Port, OAI.PowerSaving.RAM.Ty, OAI.PowerSaving.RAM.Atom

def OAI.PowerSaving.RAM.Handler line 218
Also declared: ComparatorChallenges/UniformFourier.lean:222 (same declaration text).
def OAI.PowerSaving.RAM.depthRun line 222
Also declared: ComparatorChallenges/UniformFourier.lean:226 (same declaration text).
def OAI.PowerSaving.RAM.Code.run line 227
Also declared: ComparatorChallenges/UniformFourier.lean:231 (same declaration text).
abbrev OAI.PowerSaving.RAM.Prog line 247
Also declared: ComparatorChallenges/UniformFourier.lean:251 (same declaration text).
abbrev OAI.PowerSaving.RAM.run line 249
Also declared: ComparatorChallenges/UniformFourier.lean:253 (same declaration text).