OAI/Combinatorics/LowSpaceSubsetSum/Streams/TieReplay.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

Bounded replay of one tie suffix

The reporter can stop after any matching occurrence. The replay retains only its cursor, callback state, counters, and fixed key. Its recursion is tail recursion. All attempted reports are bounded by the complete suffix length, even if the callback or fuel stops execution early.

  1. structure OAI.LowSpaceSubsetSum.TieReplay.Result line 21
  2. def OAI.LowSpaceSubsetSum.TieReplay.runAcc line 29
  3. def OAI.LowSpaceSubsetSum.TieReplay.run line 40
  4. theorem OAI.LowSpaceSubsetSum.TieReplay.runAcc_bounds line 44
  5. theorem OAI.LowSpaceSubsetSum.TieReplay.run_queries_le line 77
  6. theorem OAI.LowSpaceSubsetSum.TieReplay.run_reports_le_potential line 82
  7. theorem OAI.LowSpaceSubsetSum.TieReplay.runAcc_queries_le_potential line 92

    Source documentation

    The one final lookahead is the only read not charged to a reportable occurrence, even when the fuel is much larger than the tie group.

    theorem runAcc_queries_le_potential (read : σ → Option (α × σ)) (key : α → ℤ) (K : ℤ)
    (report : α → τ → τ × Bool) (view : σ → List α) (hread : RowMerge.IsReader read view)
    (fuel : ℕ) (s : σ) (a : τ) (q r : ℕ) :
    (runAcc read key K report fuel s a q r).queries ≤
      q + min fuel ((TieBuffer.groupView key K view s).length + 1) := by
…

    Mentions: OAI.LowSpaceSubsetSum.RowMerge.IsReader, OAI.LowSpaceSubsetSum.TieReplay.runAcc, OAI.LowSpaceSubsetSum.TieBuffer.groupView

  8. theorem OAI.LowSpaceSubsetSum.TieReplay.run_queries_le_potential line 122
  9. theorem OAI.LowSpaceSubsetSum.TieReplay.runAcc_halted_false line 130
  10. theorem OAI.LowSpaceSubsetSum.TieReplay.run_halted_false line 146
  11. theorem OAI.LowSpaceSubsetSum.TieReplay.runAcc_preserves line 154

    Source documentation

    A callback invariant can depend on the exact number of reports. This also applies to executions stopped by the callback or by the fuel.

    theorem runAcc_preserves (read : σ → Option (α × σ)) (key : α → ℤ) (K : ℤ)
    (report : α → τ → τ × Bool) (P : τ → ℕ → Prop)
    (hstep : ∀ x a r, P a r → P (report x a).1 (r + 1))
    (fuel : ℕ) (s : σ) (a : τ) (q r : ℕ) (ha : P a r) :
    P (runAcc read key K report fuel s a q r).state
      (runAcc read key K report fuel s a q r).reports := by
…

    Mentions: OAI.LowSpaceSubsetSum.TieReplay.runAcc

  12. theorem OAI.LowSpaceSubsetSum.TieReplay.run_preserves line 174
  13. theorem OAI.LowSpaceSubsetSum.TieReplay.runAcc_nonhalting_spec line 183

    Source documentation

    If reporting continues, replay processes exactly the requested prefix of the tie suffix and leaves every following occurrence untouched.

    theorem runAcc_nonhalting_spec (read : σ → Option (α × σ)) (key : α → ℤ) (K : ℤ)
    (report : α → τ → τ × Bool) (hreport : ∀ x a, (report x a).2 = false)
    (view : σ → List α) (hread : RowMerge.IsReader read view)
    (fuel : ℕ) (s : σ) (a : τ) (q r : ℕ) :
    (runAcc read key K report fuel s a q r).state =
      ((TieBuffer.groupView key K view s).take fuel).foldl (fun a x => (report x a).1) a ∧
    (runAcc read key K report fuel s a q r).reports =
      r + min fuel (TieBuffer.groupView key K view s).length ∧
    TieBuffer.groupView key K view (runAcc read key K report fuel s a q r).cursor =
      (TieBuffer.groupView key K view s).drop fuel ∧
    view s = (TieBuffer.groupView key K view s).take fuel ++
      view (runAcc read key K report fuel s a q r).cursor := by
…

    Mentions: OAI.LowSpaceSubsetSum.RowMerge.IsReader, OAI.LowSpaceSubsetSum.TieReplay.runAcc, OAI.LowSpaceSubsetSum.TieBuffer.groupView

  14. theorem OAI.LowSpaceSubsetSum.TieReplay.run_state_complete line 226