E0100: cost_unprovable

E0100 cost_unprovable — a declared cost bound that cannot be proven.

A compile-time error of soma check, the checker of the Soma programming language (soma explain E0100).

The rule

A cost { tokens: N } declaration is a promise that soma check must prove: every think() needs a literal max_tokens, and every loop around a think() needs a known number of iterations. A loop over a list of unknown length makes the bound unprovable, and a declared bound that cannot be proven is an error (E0100), not a note. Annotate the loop with for [loop_bound(50)] t in tickets (more iterations raise kind loop_bound at run time), or remove the cost declaration; here 50 × 100 reply tokens fits the declared 5000.

A program that triggers it

cell Summarizer {
    face {
        signal summarize(tickets: List<String>) -> List<String>
    }
    cost { tokens: 5000 }
    on summarize(tickets: List<String>) {
        let out = []
        for t in tickets {
            out.push(think("Summarize this support ticket in one line: {t}", map("max_tokens", 100)))
        }
        return out
    }
}

What soma check prints:

$ soma check wrong.cell
error: cost: 'tokens' bound is advisory — 1 unbounded think()/loop site(s): [summarize::for-loop over a collection of unknown size (write `for [loop_bound(N)] x in xs`)] — give every think() a literal max_tokens and every loop around it a literal bound, or remove the cost declaration
  = code: E0100
✗ 1 error(s), 0 warning(s).

The fix field of soma check --json: 1 unbounded think()/loop site(s): [summarize::for-loop over a collection of unknown size (write `for [loop_bound(N)] x in xs`)]

The fix

On line 8, for t in tickets { becomes for [loop_bound(50)] t in tickets {.

--- wrong.cell
+++ right.cell
@@ -6,5 +6,5 @@
     on summarize(tickets: List<String>) {
         let out = []
-        for t in tickets {
+        for [loop_bound(50)] t in tickets {
             out.push(think("Summarize this support ticket in one line: {t}", map("max_tokens", 100)))
         }

With the fix, soma check accepts the program:

$ soma check right.cell
✓ cost: 'tokens' bound proven — peak 5000 reply tokens (the max_tokens caps) ≤ declared 5000 (prompts are not counted: cap them with set_budget)
✓ All checks passed (1 note above).