This record groups the data and proof fields needed for “cache”. A proposition-valued field is a requirement until a constructor supplies it.
structure Cache (k : ℕ) where
source : Vector ℝ (2*k+1+1)
shared : StoredHermiteSharedTables.Tables (2*k+1)
tail : StoredHermiteGeometry.TailLevel
children : Vector StoredHermiteChildGeometry.Child 2
grid : ℝ
/-- Register-local results of the charged input reads. -/
commit-pinned source · Verso Blueprint panel
This record groups the data and proof fields needed for “loaded”. A proposition-valued field is a requirement until a constructor supplies it. Register-local results of the charged input reads.
structure Loaded (k : ℕ) where
source : Vector ℝ (2*k+1+1)
shared : StoredMatrix (2*k+1+1) (2*k+1+1)
lower : ℝ
upper : ℝ
width : ℝ
factor : ℝ
grid : ℝ
leftFull : Bool
leftPartial : Bool
middleFull : Bool
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “view”.
def view {k : ℕ} (cache : Cache k) (bit : Fin 2) : Loaded k :=
let b := decide (bit = 1)
let child := cache.children[bit.val]
⟨cache.source, if b then cache.shared.trueTable else cache.shared.falseTable,
child.lower, child.upper, cache.tail.width, cache.tail.factor, cache.grid,
child.leftFull, child.leftPartial, child.middleFull, child.middlePartial, b⟩
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “load”.
def load {k : ℕ} (cache : Cache k) (bit : Fin 2) : Run (Loaded k) := do
let b ← charge .compare (decide (bit = 1))
let children ← charge .read cache.children
let child ← read children bit
let lower ← charge .read child.lower
let upper ← charge .read child.upper
let lf ← charge .read child.leftFull
let lp ← charge .read child.leftPartial
let mf ← charge .read child.middleFull
let mp ← charge .read child.middlePartial
let source ← charge .read cache.source
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “load value”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem load_value {k : ℕ} (cache : Cache k) (bit : Fin 2) :
(load cache bit).value = view cache bit := rfl
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “load cost”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem load_cost {k : ℕ} (cache : Cache k) (bit : Fin 2) (op : Op) :
(load cache bit).cost op = 15 * tick .read op + 2 * tick .compare op := by
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “select tails”. Four Boolean selections, including the n=0 first-stage right selector.
def selectTails (first bit : Bool) (factor : ℝ) : Run (ℝ × ℝ) := do
let left ← charge .compare (if bit then 1 else factor)
let rightFree ← charge .compare (if bit then factor else 1)
let rightFirst ← charge .compare (if bit then 1 else 0)
let right ← charge .compare (if first then rightFirst else rightFree)
pure (left, right)
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “select tails value”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem selectTails_value (first bit : Bool) (factor : ℝ) :
(selectTails first bit factor).value =
(if bit then 1 else factor,
if first then (if bit then 1 else 0) else (if bit then factor else 1)) := rfl
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “select tails cost”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem selectTails_cost (first bit : Bool) (factor : ℝ) (op : Op) :
(selectTails first bit factor).cost op = 4 * tick .compare op := by
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “from loaded”. Actual scalar suppliers followed by seven output payload writes.
noncomputable def fromLoaded {k : ℕ} (t : ℕ) (x : Loaded k) : SourceRun (Fields k) :=
let first := charge .compare (decide (t = 0))
let tails := selectTails first.value x.bit x.factor
let left := StoredHermiteGeometry.leftInjection x.leftFull x.lower x.width x.grid
let middle := StoredHermiteSharedTables.injectionRow x.source x.lower x.upper x.middleFull
let output : Fields k := ⟨x.leftPartial, left.run.value, tails.value.1,
x.middlePartial, middle.value, x.shared, tails.value.2⟩
⟨⟨output, first.cost + tails.cost + left.run.cost + middle.cost + 7 • tick .write⟩,
left.exponentialCalls⟩
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “fields view”.
noncomputable def fieldsView {k : ℕ} (t : ℕ) (x : Loaded k) : Fields k :=
⟨x.leftPartial,
(StoredHermiteGeometry.leftInjection x.leftFull x.lower x.width x.grid).run.value,
if x.bit then 1 else x.factor,
x.middlePartial,
(StoredHermiteSharedTables.injectionRow x.source x.lower x.upper x.middleFull).value,
x.shared,
if t = 0 then (if x.bit then 1 else 0) else (if x.bit then x.factor else 1)⟩
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “from loaded value”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem fromLoaded_value {k : ℕ} (t : ℕ) (x : Loaded k) :
(fromLoaded t x).run.value = fieldsView t x := by
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “add cost”.
def addCost (cost : Cost) (x : SourceRun α) : SourceRun α :=
⟨StoredHermiteSharedTables.withCost cost x.run, x.exponentialCalls⟩
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “add cost value”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem addCost_value (cost : Cost) (x : SourceRun α) :
(addCost cost x).run.value = x.run.value := rfl
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “add cost cost”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem addCost_cost (cost : Cost) (x : SourceRun α) (op : Op) :
(addCost cost x).run.cost op = cost op + x.run.cost op := rfl
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “one”.
noncomputable def one {k : ℕ} (cache : Cache k) (t : ℕ) (bit : Fin 2) :
SourceRun (Fields k) :=
let loaded := load cache bit
addCost loaded.cost (fromLoaded t loaded.value)
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “one value”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem one_value {k : ℕ} (cache : Cache k) (t : ℕ) (bit : Fin 2) :
(one cache t bit).run.value = fieldsView t (view cache bit) := by
commit-pinned source · Verso Blueprint panel
This record groups the data and proof fields needed for “cache correct”. A proposition-valued field is a requirement until a constructor supplies it. Cache conditions, not a SourceCorrect assumption.
structure CacheCorrect {k : ℕ} (n t : ℕ) (L : ℝ) (cache : Cache k) : Prop where
source : ∀ i : Fin (2*k+1+1),
cache.source[i.val] = HermiteBernstein.sourceBernsteinCoefficient k i.val
sharedFalse : denote cache.shared.falseTable = sharedCore (2*k+1) false
sharedTrue : denote cache.shared.trueTable = sharedCore (2*k+1) true
grid : cache.grid = gridStep n L
width : cache.tail.width = gridStep n L * (2 : ℝ)^(n-t)
factor : cache.tail.factor = Real.exp (-gridStep n L * (2 : ℝ)^(n-t))
children : ∀ bit : Fin 2,
StoredHermiteChildGeometry.Refines cache.children[bit.val] (cutIndex n L) n (n-t)
(-Real.pi * L) (gridStep n L) (decide (bit = 1))
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “one source”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem one_source {k n : ℕ} (cache : Cache k) (t : Fin (n+1)) (L : ℝ)
(h : CacheCorrect n t.val L cache) (bit : Fin 2) :
SourceCorrect k n t.val L bit (one cache t.val bit).run.value := by
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “collect source”. Source runs are first physically cached, then their outputs projected.
def collectSource {m : ℕ} (f : Fin m → SourceRun α) : SourceRun (Vector α m) :=
let entries : Vector (SourceRun α) m := Vector.ofFn f
let projected := collect fun i => do
let entry ← read entries i
pure entry.run.value
⟨⟨projected.value,
(fun op => ∑ i : Fin m, entries[i.val].run.cost op) + m • tick .write + projected.cost⟩,
∑ i : Fin m, entries[i.val].exponentialCalls⟩
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “collect source value”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem collectSource_value {m : ℕ} (f : Fin m → SourceRun α) (i : Fin m) :
(collectSource f).run.value[i.val] = (f i).run.value := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “collect source cost”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem collectSource_cost {m : ℕ} (f : Fin m → SourceRun α) (op : Op) :
(collectSource f).run.cost op = (∑ i : Fin m, (f i).run.cost op) +
m * (3 * tick .read op + 3 * tick .write op) := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “collect source exponential calls”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem collectSource_exponentialCalls {m : ℕ} (f : Fin m → SourceRun α) :
(collectSource f).exponentialCalls = ∑ i : Fin m, (f i).exponentialCalls := by
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “two”.
noncomputable def two {k : ℕ} (cache : Cache k) (t : ℕ) :
SourceRun (Vector (Fields k) 2) := collectSource (one cache t)
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “two value”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem two_value {k : ℕ} (cache : Cache k) (t : ℕ) (bit : Fin 2) :
(two cache t).run.value[bit.val] = (one cache t bit).run.value :=
collectSource_value _ bit
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “two source”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem two_source {k n : ℕ} (cache : Cache k) (t : Fin (n+1)) (L : ℝ)
(h : CacheCorrect n t.val L cache) (bit : Fin 2) :
SourceCorrect k n t.val L bit (two cache t.val).run.value[bit.val] := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “one exponential calls”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem one_exponentialCalls {k : ℕ} (cache : Cache k) (t : ℕ) (bit : Fin 2) :
(one cache t bit).exponentialCalls = if cache.children[bit.val].leftFull then 1 else 0 := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “one exponential calls le”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem one_exponentialCalls_le {k : ℕ} (cache : Cache k) (t : ℕ) (bit : Fin 2) :
(one cache t bit).exponentialCalls ≤ 1 := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “two exponential calls le”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem two_exponentialCalls_le {k : ℕ} (cache : Cache k) (t : ℕ) :
(two cache t).exponentialCalls ≤ 2 := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “from loaded cost le”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem fromLoaded_cost_le {k : ℕ} (t : ℕ) (x : Loaded k) (op : Op) :
(fromLoaded t x).run.cost op ≤ 2 * StoredBernstein.edgeBudget (2*k+1) op +
7 * tick .field op + 7 * tick .compare op + 7 * tick .write op := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “one cost le”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem one_cost_le {k : ℕ} (cache : Cache k) (t : ℕ) (bit : Fin 2) (op : Op) :
(one cache t bit).run.cost op ≤ 2 * StoredBernstein.edgeBudget (2*k+1) op +
7 * tick .field op + 9 * tick .compare op + 15 * tick .read op +
7 * tick .write op := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “one total cost le”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem one_total_cost_le {k : ℕ} (cache : Cache k) (t : ℕ) (bit : Fin 2) :
StoredRectangularGivens.total (one cache t bit).run.cost ≤
20*(2*k+1)^3 + 42*(2*k+1)^2 + 32*(2*k+1) + 48 := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “two cost le”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem two_cost_le {k : ℕ} (cache : Cache k) (t : ℕ) (op : Op) :
(two cache t).run.cost op ≤ 4 * StoredBernstein.edgeBudget (2*k+1) op +
14 * tick .field op + 18 * tick .compare op + 36 * tick .read op +
20 * tick .write op := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “two total cost le”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem two_total_cost_le {k : ℕ} (cache : Cache k) (t : ℕ) :
StoredRectangularGivens.total (two cache t).run.cost ≤
40*(2*k+1)^3 + 84*(2*k+1)^2 + 64*(2*k+1) + 108 := by
commit-pinned source · Verso Blueprint panel