Lesson 3 — A rule next to the data, proven

A lesson of the course on the Soma programming language. Every output on this page was printed by soma 3.2.4: the build writes each file to an empty folder and runs each command.

A quota of 100 units per user. The rule is one line in memory. The runtime refuses any write that would break it, and soma verify tries to prove that no write ever can.

quota.cell

cell Quota {
    memory {
        used: Map<String, Int> [persistent]
        invariant used >= 0 && used <= 100
    }
    on consume(user: String, n: Int) {
        require n > 0 else BadAmount
        let before = used.get(user) ?? 0
        require before + n <= 100 else QuotaExceeded
        used.set(user, before + n)
        return 100 - (before + n)
    }
}

$ soma verify quota.cell
Verifying quota.cell...

Quota/invariants:

  ✓ invariant used >= 0 && used <= 100 — writer 'consume' proven by induction (writes before + n)

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

$ soma run quota.cell consume ana 60
40

$ soma run quota.cell consume ana 60
error: require failed: QuotaExceeded: constraint violated
  --> quota.cell:9:9
  |
9 |         require before + n <= 100 else QuotaExceeded
  |         ^

$ soma run quota.cell consume ana 40
0

✓ means proven for every input, not just tested. Now forget the QuotaExceeded line, the kind of omission that ships to production in other languages:

quota.cell

cell Quota {
    memory {
        used: Map<String, Int> [persistent]
        invariant used >= 0 && used <= 100
    }
    on consume(user: String, n: Int) {
        require n > 0 else BadAmount
        let before = used.get(user) ?? 0
        used.set(user, before + n)
        return 100 - (before + n)
    }
}

$ soma verify quota.cell
Verifying quota.cell...

Quota/invariants:

  ✓ invariant used >= 0 — writer 'consume' proven by induction (writes before + n)
  ⚠ invariant used >= 0 && used <= 100 — runtime-checked (computed values): consume → used [used <= 100] because `before + n` is only known to lie in [1, ∞) — narrow it: `require (before + n) <= 100 else …`

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

$ soma run --fresh quota.cell consume ana 60
fresh: removed .soma_data
40

$ soma run quota.cell consume ana 60
error: memory invariant violated on 'used': used >= 0 && used <= 100 — rejected write of 120 (key "ana"); the slot is unchanged
  --> quota.cell:9:9
  |
9 |         used.set(user, before + n)
  |         ^

The bound is no longer proven. The ⚠ line says why and which require would prove it, and the runtime still refuses the bad write and leaves the slot unchanged. soma verify --strict turns every ⚠ into a failure: use it in CI.