v0.8.2 — accumulation folds

The dominant real-world sum patterns now translate and prove.

requires(forall(lineItems, (li) => !li.invoicedAmount || li.invoicedAmount.greaterThanOrEqualTo(0)))
ensures(output().greaterThanOrEqualTo(0))          // ✓ PROVED
return lineItems.reduce((amount, li) => {
    return amount.add(li.invoicedAmount || 0);
}, new Decimal(0));

Array.prototype.reduce — (acc, x) => acc + x.f and the Decimal variant (acc.add(x.f || 0), init new Decimal(0)), block bodies with a single return — and for-of accumulation loops (let acc = 0; for (const x of arr) acc += x.f, multiple accumulators per loop, leading if (cond) continue; guards) desugar to __sumBy fold constants with boundary axioms: len === 0 ⟹ sum === 0, and quantified element facts derive linear bounds (forall x.f >= c gives sum >= c·len).

Soundness is mode-tracked: a continue guard makes the loop a subset, so bounds clamp through zero; conditional facts (!x.f || x.f >= c) only apply to zero-guarded projections (|| 0 / ?? 0 — an unguarded nullish field is NaN poison); unknown fallbacks derive no bounds. The refusals are tested as thoroughly as the proofs.

Also: theorem --version reads package.json (0.8.1 binaries self-reported 0.8.0).

~320 core tests.