CountedStreamJoin.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Costed execution of the stopped sorted-stream join

Every read, key evaluation, callback and snapshot invokes its supplied counted implementation. The resulting work follows the exact stopped query/report/copy ledger. The unused control fuel is never traversed.

def OAI.LowSpaceSubsetSum.CountedStreamJoin.potential line 18
def OAI.LowSpaceSubsetSum.CountedStreamJoin.step line 21
theorem OAI.LowSpaceSubsetSum.CountedStreamJoin.step_value line 49
theorem OAI.LowSpaceSubsetSum.CountedStreamJoin.step_work_potential line 72
def OAI.LowSpaceSubsetSum.CountedStreamJoin.runAcc line 135
theorem OAI.LowSpaceSubsetSum.CountedStreamJoin.runAcc_value line 146
theorem OAI.LowSpaceSubsetSum.CountedStreamJoin.runAcc_work line 162

theorem OAI.LowSpaceSubsetSum.CountedStreamJoin.run_work_queries line 191

Source documentation

After initialization, control iterations can themselves be charged to queries, giving a bound using only the original join ledger.

theorem run_work_queries
    (read₁ : σ₁ → Option (α × σ₁) × ℕ) (key₁ : α → ℤ × ℕ)
    (read₂ : σ₂ → Option (β × σ₂) × ℕ) (key₂ : β → ℤ × ℕ) (cells : β → ℕ)
    (report : α → β → τ → (τ × Bool) × ℕ) (clone : σ₂ → σ₂ × ℕ)
    (hclone : ∀ s, (clone s).1 = s) (R₁ R₂ L₁ L₂ S C D : ℕ)
    (hr₁ : ∀ s, (read₁ s).2 ≤ R₁) (hr₂ : ∀ s, (read₂ s).2 ≤ R₂)
    (hk₁ : ∀ x, (key₁ x).2 ≤ L₁) (hk₂ : ∀ y, (key₂ y).2 ≤ L₂)
    (hs : ∀ y, cells y ≤ S) (hc : ∀ x y a, (report x y a).2 ≤ C)
    (hcopy : ∀ s, (clone s).2 ≤ D)
    (B fuel₁ fuel₂ fuel : ℕ) (s₁ : σ₁) (s₂ : σ₂) (a : τ) :
    (runAcc read₁ key₁ read₂ key₂ cells report clone B fuel₁ fuel₂ fuel
      (StreamJoin.start s₁ s₂ a)).2 ≤
…

Mentions: OAI.LowSpaceSubsetSum.CountedStreamJoin.runAcc, OAI.LowSpaceSubsetSum.StreamJoin.start