OAI/Combinatorics/LowSpaceSubsetSum/Search/BudgetedReplay.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

Replay with a budget checked before every iteration

charge is a bound for one read, one key, one callback and the loop's bookkeeping. A failed check returns before evaluating any of these operations. In the parent join this charge is polynomial in the input scale. The callback here is the bounded dictionary emitter, not another unbounded replay.

  1. def OAI.LowSpaceSubsetSum.BudgetedReplay.runAcc line 18
  2. theorem OAI.LowSpaceSubsetSum.BudgetedReplay.insufficient line 37
  3. theorem OAI.LowSpaceSubsetSum.BudgetedReplay.runAcc_value line 43

    Source documentation

    Every completed budgeted execution is exactly the original replay.

    theorem runAcc_value (charge : ℕ) (read : σ → Option (α × σ)) (key : α → ℤ) (K : ℤ)
    (report : α → τ → τ × Bool) (fuel : ℕ) (s : σ) (a : τ) (q r budget : ℕ)
    (out : TieReplay.Result σ τ) (left : ℕ)
    (h : runAcc charge read key K report fuel s a q r budget = some (out, left)) :
    out = TieReplay.runAcc read key K report fuel s a q r ∧ left ≤ budget := by
…

    Mentions: OAI.LowSpaceSubsetSum.TieReplay.Result, OAI.LowSpaceSubsetSum.BudgetedReplay.runAcc, OAI.LowSpaceSubsetSum.TieReplay.runAcc

  4. theorem OAI.LowSpaceSubsetSum.BudgetedReplay.queries_mono line 82
  5. theorem OAI.LowSpaceSubsetSum.BudgetedReplay.runAcc_complete line 101

    Source documentation

    Enough prepaid iterations guarantee completion. The number of iterations is bounded by the original replay's query counter, not its unused fuel.

    theorem runAcc_complete (charge : ℕ) (read : σ → Option (α × σ)) (key : α → ℤ) (K : ℤ)
    (report : α → τ → τ × Bool) (fuel : ℕ) (s : σ) (a : τ) (q r budget : ℕ)
    (hbudget : charge * ((TieReplay.runAcc read key K report fuel s a q r).queries - q + 1)
      ≤ budget) :
    ∃ left, runAcc charge read key K report fuel s a q r budget =
      some (TieReplay.runAcc read key K report fuel s a q r, left) := by
…

    Mentions: OAI.LowSpaceSubsetSum.TieReplay.runAcc, OAI.LowSpaceSubsetSum.BudgetedReplay.runAcc

  6. theorem OAI.LowSpaceSubsetSum.BudgetedReplay.runAcc_work line 144

    Source documentation

    The prepaid budget covers the counted primitive work of every completed execution, including all reads and the callback's actual work.

    theorem runAcc_work (read : σ → Option (α × σ) × ℕ) (key : α → ℤ × ℕ) (K : ℤ)
    (report : α → τ → (τ × Bool) × ℕ) (R L C charge : ℕ)
    (hr : ∀ s, (read s).2 ≤ R) (hk : ∀ x, (key x).2 ≤ L)
    (hc : ∀ x a, (report x a).2 ≤ C) (hcharge : R + L + C + 8 ≤ charge)
    (fuel : ℕ) (s : σ) (a : τ) (q r budget : ℕ) (out : TieReplay.Result σ τ) (left : ℕ)
    (h : runAcc charge (fun s => (read s).1) (fun x => (key x).1) K
      (fun x a => (report x a).1) fuel s a q r budget = some (out, left)) :
    (CountedReplay.runAcc read key K report fuel s a q r).2 ≤ budget - left := by
…

    Mentions: OAI.LowSpaceSubsetSum.TieReplay.Result, OAI.LowSpaceSubsetSum.BudgetedReplay.runAcc, OAI.LowSpaceSubsetSum.CountedReplay.runAcc

  7. def OAI.LowSpaceSubsetSum.BudgetedReplay.execute line 199

    Source documentation

    The executing version retains a work counter even when the budget test aborts. The guard precedes every counted read/key/report call.

    def execute (charge : ℕ) (read : σ → Option (α × σ) × ℕ) (key : α → ℤ × ℕ) (K : ℤ)
    (report : α → τ → (τ × Bool) × ℕ) :
    ℕ → σ → τ → ℕ → ℕ → ℕ → (Option (TieReplay.Result σ τ × ℕ) × ℕ)
  | fuel, s, a, q, r, budget =>
    if charge ≤ budget then
      let left := budget - charge
…

    Mentions: OAI.LowSpaceSubsetSum.TieReplay.Result

  8. theorem OAI.LowSpaceSubsetSum.BudgetedReplay.execute_value line 225
  9. theorem OAI.LowSpaceSubsetSum.BudgetedReplay.execute_work line 251

    Source documentation

    This includes exhausted-budget executions. One final failed comparison can add one operation after the prepaid budget has been consumed.

    theorem execute_work (read : σ → Option (α × σ) × ℕ) (key : α → ℤ × ℕ) (K : ℤ)
    (report : α → τ → (τ × Bool) × ℕ) (R L C charge : ℕ)
    (hr : ∀ s, (read s).2 ≤ R) (hk : ∀ x, (key x).2 ≤ L)
    (hc : ∀ x a, (report x a).2 ≤ C) (hcharge : R + L + C + 8 ≤ charge)
    (fuel : ℕ) (s : σ) (a : τ) (q r budget : ℕ) :
    (execute charge read key K report fuel s a q r budget).2 ≤ budget + 1 := by
…

    Mentions: OAI.LowSpaceSubsetSum.BudgetedReplay.execute

  10. theorem OAI.LowSpaceSubsetSum.BudgetedReplay.execute_work_eq line 283

    Source documentation

    A completed execution performs precisely the reference operations. This equality permits nested callers to retain the unspent budget.

    theorem execute_work_eq (charge : ℕ) (read : σ → Option (α × σ) × ℕ)
    (key : α → ℤ × ℕ) (K : ℤ) (report : α → τ → (τ × Bool) × ℕ)
    (fuel : ℕ) (s : σ) (a : τ) (q r budget : ℕ)
    (out : TieReplay.Result σ τ) (left : ℕ)
    (h : (execute charge read key K report fuel s a q r budget).1 = some (out, left)) :
    (execute charge read key K report fuel s a q r budget).2 =
      (CountedReplay.runAcc read key K report fuel s a q r).2 := by
…

    Mentions: OAI.LowSpaceSubsetSum.TieReplay.Result, OAI.LowSpaceSubsetSum.BudgetedReplay.execute, OAI.LowSpaceSubsetSum.CountedReplay.runAcc

  11. theorem OAI.LowSpaceSubsetSum.BudgetedReplay.execute_spent line 316
  12. theorem OAI.LowSpaceSubsetSum.BudgetedReplay.runAcc_remaining line 330

    Source documentation

    The discarded allowance is bounded by the performed queries plus one terminal check, which supports completion proofs for sequential stages.

    theorem runAcc_remaining (charge : ℕ) (read : σ → Option (α × σ))
    (key : α → ℤ) (K : ℤ) (report : α → τ → τ × Bool)
    (fuel : ℕ) (s : σ) (a : τ) (q r budget : ℕ)
    (out : TieReplay.Result σ τ) (left : ℕ)
    (h : runAcc charge read key K report fuel s a q r budget = some (out, left)) :
    budget ≤ left + charge * (out.queries - q + 1) := by
…

    Mentions: OAI.LowSpaceSubsetSum.TieReplay.Result, OAI.LowSpaceSubsetSum.BudgetedReplay.runAcc

  13. theorem OAI.LowSpaceSubsetSum.BudgetedReplay.execute_remaining line 386
  14. theorem OAI.LowSpaceSubsetSum.BudgetedReplay.execute_result line 398

    Source documentation

    The counted reference value of a completed execution.

    theorem execute_result (charge : ℕ) (read : σ → Option (α × σ) × ℕ)
    (key : α → ℤ × ℕ) (K : ℤ) (report : α → τ → (τ × Bool) × ℕ)
    (fuel : ℕ) (s : σ) (a : τ) (q r budget : ℕ)
    (out : TieReplay.Result σ τ) (left : ℕ)
    (h : (execute charge read key K report fuel s a q r budget).1 = some (out, left)) :
    out = (CountedReplay.runAcc read key K report fuel s a q r).1 ∧ left ≤ budget := by
…

    Mentions: OAI.LowSpaceSubsetSum.TieReplay.Result, OAI.LowSpaceSubsetSum.BudgetedReplay.execute, OAI.LowSpaceSubsetSum.CountedReplay.runAcc

  15. theorem OAI.LowSpaceSubsetSum.BudgetedReplay.execute_complete line 409