soma.cell

Position-limit risk gate. Each symbol's net position must stay within

[-MAX, +MAX]. The memory invariant enforces it on every write, so an order that would breach the limit is refused and the book is unchanged.

A Soma program from the finance part of the verified corpus: 59 lines, cells PositionBook, PositionTests. It passes soma check with soma 3.2.4.

How it is built

The cell PositionBook declares 3 signals in its face: buy(symbol: String, qty: Int) -> Map, sell(symbol: String, qty: Int) -> Map and position(symbol: String) -> Int; keeps 1 memory slot: positions (Map<String, Int>, persistent and consistent) under the invariant positions >= -100 && positions <= 100. Handlers: position (line 19), buy (line 25) and sell (line 34).

The file also holds 1 test cell (PositionTests) with 7 assertions, run by soma test.

Generated from soma describe on this file.

The source

position_limit.cell

// Position-limit risk gate. Each symbol's net position must stay within
// [-MAX, +MAX]. The memory invariant enforces it on every write, so an
// order that would breach the limit is refused and the book is unchanged.

cell PositionBook {
    face {
        signal buy(symbol: String, qty: Int) -> Map
        signal sell(symbol: String, qty: Int) -> Map
        signal position(symbol: String) -> Int
        promise all_persistent
    }

    memory {
        positions: Map<String, Int> [persistent, consistent]
        // net position per symbol bounded to +/- 100 lots
        invariant positions >= -100 && positions <= 100
    }

    on position(symbol: String) {
        let p = positions.get(symbol)
        if p == () { return 0 }
        return p
    }

    on buy(symbol: String, qty: Int) {
        let cur = position(symbol)
        let r = try { positions.set(symbol, cur + qty) }
        if r.error != () {
            return map("filled", false, "reason", "long limit", "position", cur)
        }
        return map("filled", true, "position", cur + qty)
    }

    on sell(symbol: String, qty: Int) {
        let cur = position(symbol)
        let r = try { positions.set(symbol, cur - qty) }
        if r.error != () {
            return map("filled", false, "reason", "short limit", "position", cur)
        }
        return map("filled", true, "position", cur - qty)
    }
}

cell test PositionTests {
    rules {
        assert buy("ES", 60).filled == true
        assert position("ES") == 60
        // adding 60 more would hit 120 > 100 → refused
        assert buy("ES", 60).filled == false
        assert position("ES") == 60
        // can still trade within bounds
        assert buy("ES", 40).position == 100
        // shorting past -100 is refused too
        assert sell("NQ", 200).filled == false
        // direct breach is a runtime error
        assert_fails positions.set("X", 500)
    }
}

What the toolchain says

Run on a fresh copy of the program at build time; the outputs are pasted unedited.

$ soma check position_limit.cell
✓ All checks passed.
$ soma test position_limit.cell
test PositionTests ...
  ✓ assert buy("ES", 60).filled == true
  ✓ assert position("ES") == 60
  ✓ assert buy("ES", 60).filled == false
  ✓ assert position("ES") == 60
  ✓ assert buy("ES", 40).position == 100
  ✓ assert sell("NQ", 200).filled == false
  ✓ assert_fails positions.set("X", 500) — raised memory invariant violated on 'positions': positions >= -100 && positions <= 100 — rejected write of 500 (key "X"); the slot is unchanged

7 tests: 7 passed, 0 failed
$ soma verify position_limit.cell
Verifying position_limit.cell...

PositionBook/invariants:

  ⚠ invariant positions >= -100 && positions <= 100 — runtime-checked (computed values): buy → positions because `qty` is a parameter (narrow it: `require (cur + qty) >= -100 && (cur + qty) <= 100 else …`), sell → positions because `qty` is a parameter (narrow it: `require (cur - qty) >= -100 && (cur - qty) <= 100 else …`)

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

Builtins used

map

Source file: /corpus/finance/position_limit.cell · examples/corpus/finance/position_limit.cell