Counter API: a persistent integer counter exposed over HTTP
One fat `on request` routes GET/POST. State lives in a [persistent] slot. curl -X POST localhost:8080/inc ; curl localhost:8080/value
A Soma program from the web part of the verified corpus: 68 lines, cells CounterApi, CounterApiTest. It passes soma check with soma 3.2.4.
How it is built
The cell CounterApi declares 5 signals in its face: request(method: String, path: String, body: String) -> String, value() -> Int, inc() -> Int, dec() -> Int and reset() -> Int; keeps 1 memory slot: store (Map<String, Int>, persistent and consistent). Handlers: value (line 26), inc (line 28), dec (line 34), reset (line 40) and request (line 45). Private helpers: _n.
The file also holds 1 test cell (CounterApiTest) with 6 assertions, run by soma test.
The source
soma.toml
[package]
name = "web-corpus"
version = "0.1.0"
entry = "todo_state.cell"
[verify]
cells = ["TodoService"]
deadlock_free = true
eventually = ["Done", "Cancelled"]counter_api.cell
// Counter API: a persistent integer counter exposed over HTTP.
// One fat `on request` routes GET/POST. State lives in a [persistent] slot.
// soma serve counter_api.cell
// curl -X POST localhost:8080/inc ; curl localhost:8080/value
cell CounterApi {
face {
signal request(method: String, path: String, body: String) -> String
signal value() -> Int
signal inc() -> Int
signal dec() -> Int
signal reset() -> Int
promise all_persistent
}
memory {
store: Map<String, Int> [persistent, consistent]
}
on _n() {
let v = store.get("count")
if v == () { return 0 }
return v
}
on value() { return _n() }
on inc() {
let v = _n() + 1
store.set("count", v)
return v
}
on dec() {
let v = _n() - 1
store.set("count", v)
return v
}
on reset() {
store.set("count", 0)
return 0
}
on request(method: String, path: String, body: String) {
let req = map("method", method, "path", path)
match req {
{method: "GET", path: "/value"} -> to_string(value())
{method: "POST", path: "/inc"} -> to_string(inc())
{method: "POST", path: "/dec"} -> to_string(dec())
{method: "POST", path: "/reset"} -> to_string(reset())
{method: "GET", path: "/"} -> html("<h1>Counter</h1><p>POST /inc /dec /reset, GET /value</p>")
_ -> response(404, "not found")
}
}
}
cell test CounterApiTest {
rules {
assert reset() == 0
assert inc() == 1
assert inc() == 2
assert dec() == 1
assert value() == 1
assert reset() == 0
}
}What the toolchain says
$ soma check counter_api.cell
✓ All checks passed.$ soma test counter_api.cell
test CounterApiTest ...
✓ assert reset() == 0
✓ assert inc() == 1
✓ assert inc() == 2
✓ assert dec() == 1
✓ assert value() == 1
✓ assert reset() == 0
6 tests: 6 passed, 0 failed$ soma verify counter_api.cell
Verifying counter_api.cell...
No state machine in this program: nothing to prove beyond `soma check` (invariants and lifecycles are what verify proves).
note: the soma.toml beside this file declares [verify] properties; none applies here (no state machine)
VERIFY OK (vacuous — no state machine)