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.
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
$ 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