vaelii.impl.budget — com.vaelii/vaelii 0.24.0

Resource-bounded / anytime realization of an answer stream.

The engine's query paths are lazy — ask, query, and the level stack all yield one solution at a time, paying per result consumed. Resource-bounding is therefore the consumer-side discipline of realizing that stream under a bound and reporting whether it ran dry or was cut short — and resumption falls out of laziness for free, because the unrealized tail is the continuation.

A budget is a map of optional bounds (any subset; nil / {} means unbounded):

:max-ms wall-clock milliseconds — a soft deadline, checked between yielded results (between DFS steps and node expansions in prove-within), and inside one only by a walk that reads *deadline* (the argument-preservation prover's claim walk); every other single pull or step runs to its end :max-results stop after this many solutions :max-cost a qualitative prover-cost ceiling — a tier keyword (see vaelii.impl.provers/cost-tiers). Honored by ask-within, which drops provers above the tier before the stream is built; ignored here, since it selects which work runs, not how much of a stream to realize. :max-depth transformation (rule-expansion) depth — honored by prove-within :max-term-growth how many levels of compound nesting a subgoal may add over what its own derivation path has already met (res/default-max-term-growth, 8) — the DFS prover's other termination guard, honored by prove-within through prove-bounds

A key outside those five is refused (:unknown-option, check-budget!): every bound is optional, so a misspelt one is not missing — the run is simply unbounded, in silence.

A partial result — the anytime contract returned by collect / from-batch / resume:

:results the solutions realized in this step (a vector) :status :complete the source ran dry — the answer is exhaustive :timeout :max-ms elapsed with work remaining :capped :max-results reached with work remaining :count (count :results) :elapsed-ms wall-clock spent in this step :resume nil when :complete; otherwise a 1-arg fn (budget -> partial result) that continues exactly where this step stopped

:results are per-step, not cumulative: concatenate across steps for the whole answer. The resume continuation captures an in-memory lazy tail (or, for prove-within, the DFS goal stack), so resumption is in-process only — it does not survive a restart, and holding one pins its captured state in the heap (see the single-writer contract in docs/storage.md).

*deadline* clj

The now instant a walk inside one step of a bounded read stops at: bound by collect around its pulls when the caller hands it a restart, by the two backward chainers around a leaf (interruptible), and by metered to its meter's deadline; nil otherwise. A walk reads it through check-deadline!.

ask-budget-keys clj

Every bound ask-within reads: the wall clock, the result cap, and the qualitative prover-cost ceiling. Not :max-depth / :max-term-growth, which bound rule expansion ask does not do — the same split vaelii.core/ask-opt-keys makes for ask.

budget-keys clj

Every bound a budget may carry — the union of what ask-within and prove-within each read. resume continues either, so it holds a partial to this union rather than to one entry point's half; check-budget! defaults to it, and the two entry points pass their own narrower roster instead. Public for the reason vaelii.core/assert-opt-keys is: it is the answer to "is this a real bound?".

check-budget! clj

(check-budget! budget)

(check-budget! budget opt-keys subject)

Refuse a budget key nothing reads, a value outside a bound's domain, and a non-nil non-map budget (:unknown-option all three). A budget is a map of optional bounds, so a misspelt key is not missing — the run is simply unbounded: {:max-mss 100} realizes the whole stream, which on an infinite source never returns, and is in any case the opposite of what was asked. And a bound holding a value it cannot mean — a string :max-ms, a zero :max-results — reaches arithmetic and throws bare, where every sibling refusal is typed; check-values! catches it here (opts/bound-domains). (A :max-cost value outside the tiers is checked separately, :unknown-option at vaelii.impl.provers/cost-capped-provers, which ask-capped reads the registry through — it is not a numeric bound, so it has no row in bound-domains.)

opt-keys defaults to the union budget-keys — what resume, collect and the two drivers hold a budget to, since a resume continues either entry point. ask-within and prove-within pass their own narrower roster and subject, so a caller who names :max-depth at ask-within is told it is not a bound ask reads.

check-deadline! clj

(check-deadline! dl)

Throw the signal collect catches when the instant dl has passed. A nil dl never throws.

checked-call clj

(checked-call f)

(f) between two spend! checkpoints, so a deadline passed inside an opaque callback stops the read as soon as it returns. Outside metered it is (f).

checked-seq clj

(checked-seq xs)

xs with a spend! before and after each pull, or xs itself outside metered. A chunked source realizes its whole chunk in one pull, and the meter observes that only after the pull returns.

collect clj

(collect xs budget)

(collect xs budget restart)

Realize the lazy seq xs under budget, returning the partial-result contract.

Both bounds are checked before pulling the next element, so :max-results n pulls the source n times and a passed deadline stops without over-reading; the element under the cursor is never lost — it stays the head of the captured tail, so resume re-pulls it. A nil / {} budget realizes the whole seq (:complete).

restart, a 0-arg fn building xs afresh, lets a walk inside one pull stop at the deadline too: the pulls run with *deadline* bound, and a pull a walk interrupts (check-deadline!) answers :timeout. An interrupted lazy seq cannot be re-pulled (a LazySeq whose nested realization threw reads as empty afterwards), so the continuation rebuilds the stream with restart, drops the answers already returned, and runs its first pull without the deadline. Each resume therefore gets past the interrupted walk, and a resume loop under a fixed budget terminates.

rest, not next: next realizes one element ahead to decide whether a tail exists, so a cap of n would pull n+1 from the source. rest defers that, and the cap check sits above the empty? that would force it — so an unbounded source is bounded without reading past the cap.

How many elements that realizes is the source's business, not this loop's. n pulls realize exactly n elements of an unchunked seq, which is what every seq the engine hands here is — a lazy-seq/cons chain out of the solvers and the index, pinned by laziness_test/a-capped-ask-pays-for-the-cap-and-not-for-a-chunk. A chunked source — anything built by map/filter over a vector or a range — realizes its whole 32-element chunk on the first pull whatever the cap says, and no cap check above it can prevent that. So the promise a caller may rely on is the one about the source: n pulls, and the tail resumable from where they stopped.

deadline clj

(deadline budget)

Absolute now instant :max-ms from now, or nil when unbounded.

exhausted clj

(exhausted e)

The bound that e reports running out, :max-work or :max-ms, when e is spend!'s signal or check-deadline!'s; else nil.

found clj

(found m)

The findings record! added to meter m, as {k [x …]} in arrival order.

from-batch clj

(from-batch results status start-nanos resume-fn)

Assemble the partial-result contract from a completed step. resume-fn is a 1-arg (budget -> partial result) continuation; it is dropped when status is :complete (nothing remains to continue). Both engines — the lazy collect and the eager prove-within — build their answer through here, so the two return the identical shape.

interruptible clj

(interruptible dl f)

(f) with *deadline* bound to dl (nil: no deadline, whatever an enclosing frame bound), or ::interrupted when a walk inside it threw check-deadline!'s signal. f must be eager: a lazy seq handed back realizes after the binding has popped, and outside the catch.

meter clj

(meter opts)

A new work meter for the bounds opts reads (:max-work, :max-ms), started now.

metered clj

(metered m f)

(f) with *meter* bound to the meter m and *deadline* to its deadline, so a walk that reads *deadline* stops at it too. A bound running out throws spend!'s or check-deadline!'s signal out of f; exhausted reads either.

ms-since clj

(ms-since start-nanos)

Milliseconds elapsed since a now instant, as a double.

now clj

(now)

The System/nanoTime instant every deadline in this namespace is set and checked against. A test hooks it to move a deadline past without sleeping.

prove-bounds clj

(prove-bounds budget)

A budget as the DFS prover's bounds map (res/prove-from) — the deadline the wall-clock bound resolves to, plus the caps it reads under their own names.

One translation, and it lives beside budget-keys on purpose: the roster and the map that honours it are two halves of one claim, and a bound rostered there but not built here is accepted and then ignored — precisely what check-budget! refuses a misspelt key to prevent. :max-cost is absent because it bounds ask's prover tiers rather than a search, and the node-engine arm of prove-within takes the budget itself rather than this map.

A bound the caller did not name reads nil, which prove-from takes as unbounded — except :max-term-growth, whose absence is res/default-max-term-growth rather than no ceiling, since it is a termination guard and not a budget the caller may drop.

prove-budget-keys clj

Every bound prove-within reads: the wall clock, the result cap, and the two guards on rule expansion. Not :max-cost, an ask concept prove ignores — the same split vaelii.core/prove-opt-keys makes for prove.

record! clj

(record! k x)

Add x to the running meter's findings under k, which found reads however the read stopped. Returns x.

resume clj

(resume partial budget)

Continue a :timeout / :capped partial result under a fresh budget. A :complete result has no continuation, so resume returns it unchanged — making a while (:resume …) (recur (resume …)) loop terminate cleanly.

snapshot clj

(snapshot m)

The work meter m charged and the milliseconds since it started.

spend! clj

(spend!)

Charge one work unit to the running meter. Throws before the unit when the meter's deadline has passed or its :max-work units are spent. A no-op outside metered.