Bank accounts as Account records kept in a persistent Map slot, with deposit/withdraw that read, mutate, and write the record back
Shows the read-modify-write round-trip pattern and a negative (overdraft) path.
A Soma program from the records part of the verified corpus: 57 lines, cells Bank, BankTest. It passes soma check with soma 3.2.4.
How it is built
The cell Bank declares 4 signals in its face: open(owner: String, initial: Int) -> String, balance(id: String) -> Int, deposit(id: String, amount: Int) -> Int and withdraw(id: String, amount: Int) -> Map; keeps 1 memory slot: accounts (Map<String, Map>, persistent and consistent). Handlers: open (line 17), balance (line 23), deposit (line 29) and withdraw (line 37).
The file also holds 1 test cell (BankTest) with 6 assertions, run by soma test.
The source
bank.cell
// Bank accounts as Account records kept in a persistent Map slot, with
// deposit/withdraw that read, mutate, and write the record back. Shows
// the read-modify-write round-trip pattern and a negative (overdraft) path.
cell Bank {
face {
signal open(owner: String, initial: Int) -> String
signal balance(id: String) -> Int
signal deposit(id: String, amount: Int) -> Int
signal withdraw(id: String, amount: Int) -> Map
}
memory {
accounts: Map<String, Map> [persistent, consistent]
}
on open(owner: String, initial: Int) {
let id = "acct-{owner}"
accounts.set(id, Account { id: id, owner: owner, balance: initial })
return id
}
on balance(id: String) {
let a = accounts.get(id)
if a == () { return -1 }
return a.balance
}
on deposit(id: String, amount: Int) {
let a = accounts.get(id)
if a == () { return -1 }
a.balance = a.balance + amount // mutate the loaded record
accounts.set(id, a) // write it back
return a.balance
}
on withdraw(id: String, amount: Int) {
let a = accounts.get(id)
if a == () { return map("error", "no account") }
if a.balance < amount { return map("error", "overdraft") }
a.balance = a.balance - amount
accounts.set(id, a)
return map("id", id, "balance", a.balance)
}
}
cell test BankTest {
rules {
assert open("Ada", 100) == "acct-Ada"
assert balance("acct-Ada") == 100
assert deposit("acct-Ada", 50) == 150
assert withdraw("acct-Ada", 30).balance == 120
assert withdraw("acct-Ada", 9999).error == "overdraft"
assert balance("acct-Ghost") == -1
}
}What the toolchain says
$ soma check bank.cell
✓ All checks passed.$ soma test bank.cell
test BankTest ...
✓ assert open("Ada", 100) == "acct-Ada"
✓ assert balance("acct-Ada") == 100
✓ assert deposit("acct-Ada", 50) == 150
✓ assert withdraw("acct-Ada", 30).balance == 120
✓ assert withdraw("acct-Ada", 9999).error == "overdraft"
✓ assert balance("acct-Ghost") == -1
6 tests: 6 passed, 0 failed$ soma verify bank.cell
Verifying bank.cell...
No state machine in this program: nothing to prove beyond `soma check` (invariants and lifecycles are what verify proves).
VERIFY OK (vacuous — no state machine)