BudgetedJoinOne.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Prepaid buffered replay and suffix restoration

The fixed overhead and snapshot allowance are reserved before their operations. The suffix receives only the allowance left by the completed buffer replay. No branch tests the cost of an operation after executing it.

def OAI.LowSpaceSubsetSum.BudgetedJoinOne.execute line 19
theorem OAI.LowSpaceSubsetSum.BudgetedJoinOne.execute_value line 45

theorem OAI.LowSpaceSubsetSum.BudgetedJoinOne.execute_work line 99

Source documentation

Every outcome, including either failed guard, stays within the allowance plus its final failed comparison.

theorem execute_work (read : σ → Option (α × σ) × ℕ) (key : α → ℤ × ℕ) (K : ℤ)
    (report : α → τ → (τ × Bool) × ℕ) (clone : σ → σ × ℕ)
    (R L C charge copyCharge : ℕ) (hr : ∀ s, (read s).2 ≤ R)
    (hk : ∀ x, (key x).2 ≤ L) (hc : ∀ x a, (report x a).2 ≤ C)
    (hcharge : max R 4 + L + C + 8 ≤ charge) (hcopy : ∀ s, (clone s).2 ≤ copyCharge)
    (buffer : Array α) (saved : σ) (long : Bool) (fuel : ℕ) (a : τ) (budget : ℕ) :
    (execute charge copyCharge read key K report clone buffer saved long fuel a budget).2 ≤
      budget + 1 := by
…

Mentions: OAI.LowSpaceSubsetSum.BudgetedJoinOne.execute

theorem OAI.LowSpaceSubsetSum.BudgetedJoinOne.execute_spent line 144

Source documentation

Successful nested calls leave the claimed allowance unspent.

theorem execute_spent (read : σ → Option (α × σ) × ℕ) (key : α → ℤ × ℕ) (K : ℤ)
    (report : α → τ → (τ × Bool) × ℕ) (clone : σ → σ × ℕ)
    (R L C charge copyCharge : ℕ) (hr : ∀ s, (read s).2 ≤ R)
    (hk : ∀ x, (key x).2 ≤ L) (hc : ∀ x a, (report x a).2 ≤ C)
    (hcharge : max R 4 + L + C + 8 ≤ charge) (hcopy : ∀ s, (clone s).2 ≤ copyCharge)
    (buffer : Array α) (saved : σ) (long : Bool) (fuel : ℕ) (a : τ) (budget : ℕ)
    (out : TieReplay.Result σ τ) (remaining : ℕ)
    (h : (execute charge copyCharge read key K report clone buffer saved long fuel a budget).1 =
      some (out, remaining)) :
    (execute charge copyCharge read key K report clone buffer saved long fuel a budget).2 ≤
      budget - remaining := by
…

Mentions: OAI.LowSpaceSubsetSum.TieReplay.Result, OAI.LowSpaceSubsetSum.BudgetedJoinOne.execute

theorem OAI.LowSpaceSubsetSum.BudgetedJoinOne.execute_complete line 209

Source documentation

Completion is governed by performed queries and actual restores, not by multiplying the two advertised stream fuel bounds.

theorem execute_complete (charge copyCharge : ℕ) (read : σ → Option (α × σ) × ℕ)
    (key : α → ℤ × ℕ) (K : ℤ) (report : α → τ → (τ × Bool) × ℕ)
    (clone : σ → σ × ℕ) (buffer : Array α) (saved : σ) (long : Bool)
    (fuel : ℕ) (a : τ) (budget : ℕ)
    (hbudget : charge * ((CountedJoinOne.run read key K report clone buffer saved long fuel a).1.queries + 2) +
      (if long then copyCharge else 0) + 6 ≤ budget) :
    ∃ remaining, (execute charge copyCharge read key K report clone buffer saved long fuel a budget).1 =
      some ((CountedJoinOne.run read key K report clone buffer saved long fuel a).1, remaining) := by
…

Mentions: OAI.LowSpaceSubsetSum.CountedJoinOne.run, OAI.LowSpaceSubsetSum.BudgetedJoinOne.execute

theorem OAI.LowSpaceSubsetSum.BudgetedJoinOne.execute_remaining line 272

Source documentation

At most one charge per query, two terminal charges, and one snapshot allowance are discarded by a completed inner replay.

theorem execute_remaining (charge copyCharge : ℕ) (read : σ → Option (α × σ) × ℕ)
    (key : α → ℤ × ℕ) (K : ℤ) (report : α → τ → (τ × Bool) × ℕ)
    (clone : σ → σ × ℕ) (buffer : Array α) (saved : σ) (long : Bool)
    (fuel : ℕ) (a : τ) (budget : ℕ) (out : TieReplay.Result σ τ) (remaining : ℕ)
    (h : (execute charge copyCharge read key K report clone buffer saved long fuel a budget).1 =
      some (out, remaining)) :
    budget ≤ remaining + charge * (out.queries + 2) + (if long then copyCharge else 0) + 6 := by
…

Mentions: OAI.LowSpaceSubsetSum.TieReplay.Result, OAI.LowSpaceSubsetSum.BudgetedJoinOne.execute