LayoutPrograms.lean`

10 declarations, 0 contain sorry, 0 declared as axioms

Programming over a logical layout. Case splits over fixed finite sets are fine. No computation of Layout etc occurs in code; all needed address calculations use RAM combinators.

lemma OAI.PowerSaving.RAM.as_tab line 16
theorem OAI.PowerSaving.RAM.Able.layout line 26
lemma OAI.PowerSaving.RAM.Small.loc line 55
theorem OAI.PowerSaving.RAM.Can.layout line 66
theorem OAI.PowerSaving.RAM.Can.fetch line 76

theorem OAI.PowerSaving.RAM.Can.eqbit line 85

Source documentation

Equality test via comparison operations.

theorem eqbit {n q : ι → ℕ} (h : Can m B s w x n W) (k : Can m B s w x q W) :
    Can m B s w x (fun i => if n i = q i then 0 else 1) W := by
…

Mentions: OAI.PowerSaving.RAM.Can

def OAI.PowerSaving.RAM.Can.blankProg line 100

theorem OAI.PowerSaving.RAM.Can.cases_code line 107

Source documentation

split according to a fixed finite value on which code is allowed to depend.

theorem cases_code [DecidableEq μ] [Fintype μ] {y : ι → T t} {q : ι→μ}
    (D : Layout μ) (h : Can m B s w x (fun i => D.loc (q i)) W)
    (g : ∀ f : μ, Can m (fun i : {i // q i=f} => B i.1) s t
      (fun i => x i.1) (fun i => y i.1) (fun i => W i.1)) :
    Can m B s t x y W := by
…

Mentions: OAI.PowerSaving.Layout, OAI.PowerSaving.RAM.Can

theorem OAI.PowerSaving.RAM.Can.sum_wconst line 142

Source documentation

An arbitrary RAM word sum over a fixed finite set.

theorem sum_wconst [Fintype μ] {v : μ → ι → ℕ}
    (h : ∀ i : μ, Can m B s w x (v i) W)
    (g : ∀ i : μ, Small B (v i)) :
    Can m B s w x (fun j => ∑ i, v i j) W := by
…

Mentions: OAI.PowerSaving.RAM.Can, OAI.PowerSaving.RAM.Small

theorem OAI.PowerSaving.RAM.Can.sum_cconst line 158