BudgetedOuterCompletion.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Sufficient prepaid allowance for nested outer replay

The analysis charges the actual callback at each consumed occurrence. Unused advertised fuel is absent from the allowance. allowance is proof-only.

def OAI.LowSpaceSubsetSum.BudgetedOuterReplay.allowance line 16
theorem OAI.LowSpaceSubsetSum.BudgetedOuterReplay.execute_complete line 27

theorem OAI.LowSpaceSubsetSum.BudgetedOuterReplay.allowance_le_potential line 88

Source documentation

Callback charges telescope through the actual callback state.

theorem allowance_le_potential (read : σ → Option (α × σ)) (key : α → ℤ) (K : ℤ)
    (report : α → τ → τ × Bool) (bill : α → τ → ℕ) (potential : τ → ℕ)
    (charge extra : ℕ)
    (hbill : ∀ x a, bill x a + potential a ≤ potential (report x a).1 + extra)
    (fuel : ℕ) (s : σ) (a : τ) (q r : ℕ) :
    allowance charge read key K report bill fuel s a + potential a + (charge + extra) * q ≤
      (charge + extra) * (TieReplay.runAcc read key K report fuel s a q r).queries +
        potential (TieReplay.runAcc read key K report fuel s a q r).state + charge := by
…

Mentions: OAI.LowSpaceSubsetSum.BudgetedOuterReplay.allowance, OAI.LowSpaceSubsetSum.TieReplay.runAcc