FX converter with a rate table in memory and a non-negative rate invariant
Cross rates are derived via a USD base. Demonstrates a Map<String,Float> slot, an invariant on stored values, and triangular cross-rate arithmetic.
A Soma program from the finance part of the verified corpus: 60 lines, cells FxConverter, FxTests. It passes soma check with soma 3.2.4.
How it is built
The cell FxConverter declares 3 signals in its face: set_rate(ccy: String, per_usd: Float) -> Map, to_usd(ccy: String, amount: Float) -> Float and convert(from_ccy: String, to_ccy: String, amount: Float) -> Float; keeps 1 memory slot: rates (Map<String, Float>, persistent and consistent) under the invariant rates >= 0.0. Handlers: set_rate (line 20), to_usd (line 28) and convert (line 36).
The file also holds 1 test cell (FxTests) with 7 assertions, run by soma test.
The source
currency_converter.cell
// FX converter with a rate table in memory and a non-negative rate
// invariant. Cross rates are derived via a USD base. Demonstrates a
// Map<String,Float> slot, an invariant on stored values, and triangular
// cross-rate arithmetic.
cell FxConverter {
face {
signal set_rate(ccy: String, per_usd: Float) -> Map
signal to_usd(ccy: String, amount: Float) -> Float
signal convert(from_ccy: String, to_ccy: String, amount: Float) -> Float
promise all_persistent
}
memory {
// units of CCY per 1 USD; must be strictly sensible (non-negative)
rates: Map<String, Float> [persistent, consistent]
invariant rates >= 0.0
}
on set_rate(ccy: String, per_usd: Float) {
let r = try { rates.set(ccy, per_usd) }
if r.error != () {
return map("ok", false, "reason", "{r.error}")
}
return map("ok", true, "ccy", ccy, "per_usd", per_usd)
}
on to_usd(ccy: String, amount: Float) {
if ccy == "USD" { return amount }
let rate = rates.get(ccy)
if rate == () { return 0.0 }
return amount / rate
}
// cross rate via USD: from -> USD -> to
on convert(from_ccy: String, to_ccy: String, amount: Float) {
let usd = to_usd(from_ccy, amount)
if to_ccy == "USD" { return usd }
let rate = rates.get(to_ccy)
if rate == () { return 0.0 }
return usd * rate
}
}
cell test FxTests {
rules {
assert set_rate("EUR", 0.92).ok == true
assert set_rate("JPY", 156.0).ok == true
// 100 EUR -> USD = 100/0.92 ≈ 108.70
assert abs(to_usd("EUR", 100.0) - 108.695652) < 0.001
// 100 EUR -> JPY via USD
assert abs(convert("EUR", "JPY", 100.0) - (100.0 / 0.92 * 156.0)) < 0.001
// USD passthrough
assert abs(to_usd("USD", 50.0) - 50.0) < 0.0001
// a negative rate is rejected by the invariant
assert set_rate("BAD", -1.0).ok == false
assert_fails rates.set("X", -0.5)
}
}What the toolchain says
$ soma check currency_converter.cell
✓ All checks passed.$ soma test currency_converter.cell
test FxTests ...
✓ assert set_rate("EUR", 0.92).ok == true
✓ assert set_rate("JPY", 156.0).ok == true
✓ assert abs(to_usd("EUR", 100.0) - 108.695652) < 0.001
✓ assert abs(convert("EUR", "JPY", 100.0) - (100.0 / 0.92 * 156.0)) < 0.001
✓ assert abs(to_usd("USD", 50.0) - 50.0) < 0.0001
✓ assert set_rate("BAD", -1.0).ok == false
✓ assert_fails rates.set("X", -0.5) — raised memory invariant violated on 'rates': rates >= 0.0 — rejected write of -0.5 (key "X"); the slot is unchanged
7 tests: 7 passed, 0 failed$ soma verify currency_converter.cell
Verifying currency_converter.cell...
FxConverter/invariants:
⚠ invariant rates >= 0.0 — runtime-checked (computed values): set_rate → rates because `per_usd` is a parameter (narrow it: `require per_usd >= 0.0 else …`)
0 passed, 1 warnings, 0 failures
Temporal: 0 passed, 0 failed
VERIFY OK