soma.cell

Monthly budget tracker with a spend cap invariant

Total spend per category must never exceed its allotted budget; an over-budget write is rejected by memory. Shows group accounting and a remaining-budget query.

A Soma program from the finance part of the verified corpus: 54 lines, cells BudgetTracker, BudgetTests. It passes soma check with soma 3.2.4.

How it is built

The cell BudgetTracker declares 3 signals in its face: spend(category: String, amount: Int) -> Map, spent(category: String) -> Int and remaining(category: String) -> Int; keeps 1 memory slot: outlays (Map<String, Int>, persistent and consistent) under the invariant outlays >= 0 && outlays <= 50000. Handlers: spent (line 19), remaining (line 25) and spend (line 29).

The file also holds 1 test cell (BudgetTests) with 8 assertions, run by soma test.

Generated from soma describe on this file.

The source

budget_tracker.cell

// Monthly budget tracker with a spend cap invariant. Total spend per
// category must never exceed its allotted budget; an over-budget write
// is rejected by memory. Shows group accounting and a remaining-budget query.

cell BudgetTracker {
    face {
        signal spend(category: String, amount: Int) -> Map
        signal spent(category: String) -> Int
        signal remaining(category: String) -> Int
        promise all_persistent
    }

    memory {
        // cents spent per category; capped so no category overspends its 50_000 cap
        outlays: Map<String, Int> [persistent, consistent]
        invariant outlays >= 0 && outlays <= 50000
    }

    on spent(category: String) {
        let s = outlays.get(category)
        if s == () { return 0 }
        return s
    }

    on remaining(category: String) {
        return 50000 - spent(category)
    }

    on spend(category: String, amount: Int) {
        let cur = spent(category)
        let r = try { outlays.set(category, cur + amount) }
        if r.error != () {
            return map("ok", false, "reason", "over budget", "remaining", remaining(category))
        }
        return map("ok", true, "spent", cur + amount, "remaining", 50000 - (cur + amount))
    }
}

cell test BudgetTests {
    rules {
        assert spend("groceries", 12000).ok == true
        assert spent("groceries") == 12000
        assert remaining("groceries") == 38000
        // a charge that blows the cap is refused
        assert spend("groceries", 40000).ok == false
        // and nothing was recorded
        assert spent("groceries") == 12000
        // hitting the cap exactly is fine
        assert spend("rent", 50000).ok == true
        assert remaining("rent") == 0
        assert_fails outlays.set("x", 60000)
    }
}

What the toolchain says

Run on a fresh copy of the program at build time; the outputs are pasted unedited.

$ soma check budget_tracker.cell
✓ All checks passed.
$ soma test budget_tracker.cell
test BudgetTests ...
  ✓ assert spend("groceries", 12000).ok == true
  ✓ assert spent("groceries") == 12000
  ✓ assert remaining("groceries") == 38000
  ✓ assert spend("groceries", 40000).ok == false
  ✓ assert spent("groceries") == 12000
  ✓ assert spend("rent", 50000).ok == true
  ✓ assert remaining("rent") == 0
  ✓ assert_fails outlays.set("x", 60000) — raised memory invariant violated on 'outlays': outlays >= 0 && outlays <= 50000 — rejected write of 60000 (key "x"); the slot is unchanged

8 tests: 8 passed, 0 failed
$ soma verify budget_tracker.cell
Verifying budget_tracker.cell...

BudgetTracker/invariants:

  ⚠ invariant outlays >= 0 && outlays <= 50000 — runtime-checked (computed values): spend → outlays because `amount` is a parameter (narrow it: `require (cur + amount) >= 0 && (cur + amount) <= 50000 else …`)

0 passed, 1 warnings, 0 failures
Temporal: 0 passed, 0 failed
VERIFY OK

Builtins used

map

Source file: /corpus/finance/budget_tracker.cell · examples/corpus/finance/budget_tracker.cell