BudgetedFill.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Prepaid construction of a tie buffer

The budget guard precedes the reader, key evaluator and record copy. It can therefore interrupt a long tie before materializing the entire requested buffer. The reference fill appears only in correctness and completion proofs.

def OAI.LowSpaceSubsetSum.BudgetedFill.execute line 17
theorem OAI.LowSpaceSubsetSum.BudgetedFill.insufficient line 37
theorem OAI.LowSpaceSubsetSum.BudgetedFill.execute_value line 43
theorem OAI.LowSpaceSubsetSum.BudgetedFill.queries_mono line 79
theorem OAI.LowSpaceSubsetSum.BudgetedFill.execute_complete line 96
theorem OAI.LowSpaceSubsetSum.BudgetedFill.execute_work line 138

theorem OAI.LowSpaceSubsetSum.BudgetedFill.execute_spent line 168

Source documentation

A successful fill charges its work against the budget it actually spent, so the remaining allowance can be passed to the next join stage.

theorem execute_spent (read : σ → Option (α × σ) × ℕ)
    (key : α → ℤ × ℕ) (cells : α → ℕ) (K : ℤ) (R L S charge : ℕ)
    (hr : ∀ s, (read s).2 ≤ R) (hk : ∀ x, (key x).2 ≤ L)
    (hs : ∀ x, cells x ≤ S) (hcharge : R + L + S + 8 ≤ charge)
    (fuel : ℕ) (s : σ) (buf : Array α) (q budget : ℕ)
    (out : TieBuffer.Result α σ) (left : ℕ)
    (h : (execute charge read key cells K fuel s buf q budget).1 = some (out, left)) :
    (execute charge read key cells K fuel s buf q budget).2 ≤ budget - left := by
…

Mentions: OAI.LowSpaceSubsetSum.TieBuffer.Result, OAI.LowSpaceSubsetSum.BudgetedFill.execute

theorem OAI.LowSpaceSubsetSum.BudgetedFill.execute_remaining line 213

Source documentation

The discarded fill allowance is bounded by its performed queries.

theorem execute_remaining (charge : ℕ) (read : σ → Option (α × σ) × ℕ)
    (key : α → ℤ × ℕ) (cells : α → ℕ) (K : ℤ)
    (fuel : ℕ) (s : σ) (buf : Array α) (q budget : ℕ)
    (out : TieBuffer.Result α σ) (left : ℕ)
    (h : (execute charge read key cells K fuel s buf q budget).1 = some (out, left)) :
    budget ≤ left + charge * (out.queries - q + 1) := by
…

Mentions: OAI.LowSpaceSubsetSum.TieBuffer.Result, OAI.LowSpaceSubsetSum.BudgetedFill.execute