Chargeback window — disputes die at day 120, reversals happen exactly once
Card networks give cardholders ~120 days to dispute a charge. Two ways processors lose money here: accepting a dispute after the window (the merchant's funds were already swept as final), and reversing the same charge twice when a manual agent and an automated rule both fire. Both are structural below: `finalized` is terminal so a late dispute has no edge to take, and `reversed`/`upheld` are terminal so a second reversal raises. The merchant ledger refuses negative balances.
A Soma program from the escrow_finance part of the verified corpus: 109 lines, cells Chargeback, ChargebackTests. It passes soma check with soma 3.2.4.
How it is built
The cell Chargeback declares 5 signals in its face: capture(id: String, amount: Int) -> Map, close_window(id: String, day: Int) -> Map, open_dispute(id: String, day: Int) -> Map, resolve(id: String, outcome: String) -> Map and merchant_balance() -> Int; keeps 2 memory slots: merchant (Map<String, Int>, persistent and consistent) under the invariant merchant >= 0 and amounts (Map<String, Int>, persistent and consistent) under the invariant amounts >= 0. Its state machine charge starts in authorized and allows 5 transitions: authorized -> settled, settled -> finalized, settled -> disputed, disputed -> reversed and disputed -> upheld. finalized, reversed and upheld are terminal. Handlers: capture (line 41), close_window (line 50), open_dispute (line 58), resolve (line 66) and merchant_balance (line 77).
The file also holds 1 test cell (ChargebackTests) with 17 assertions, run by soma test.
The source
chargeback_window.cell
// ============================================================================
// CHARGEBACK WINDOW — disputes die at day 120, reversals happen exactly once
// ============================================================================
//
// Card networks give cardholders ~120 days to dispute a charge. Two ways
// processors lose money here: accepting a dispute after the window (the
// merchant's funds were already swept as final), and reversing the same
// charge twice when a manual agent and an automated rule both fire. Both
// are structural below: `finalized` is terminal so a late dispute has no
// edge to take, and `reversed`/`upheld` are terminal so a second reversal
// raises. The merchant ledger refuses negative balances.
// ============================================================================
cell Chargeback {
face {
signal capture(id: String, amount: Int) -> Map
signal close_window(id: String, day: Int) -> Map
signal open_dispute(id: String, day: Int) -> Map
signal resolve(id: String, outcome: String) -> Map
signal merchant_balance() -> Int
}
memory {
merchant: Map<String, Int> [persistent, consistent]
invariant merchant >= 0
amounts: Map<String, Int> [persistent, consistent]
invariant amounts >= 0
}
// finalized, reversed, upheld: all terminal. A finalized charge can
// never become disputed; a reversed charge can never reverse again.
state charge {
initial: authorized
authorized -> settled
settled -> finalized
settled -> disputed
disputed -> reversed
disputed -> upheld
}
on capture(id: String, amount: Int) {
if amount <= 0 { return map("ok", false, "reason", "bad amount") }
if merchant.get("acct") == () { merchant.set("acct", 0) }
transition(id, "settled")
amounts.set(id, amount)
merchant.set("acct", (merchant.get("acct") ?? 0) + amount)
return map("ok", true, "state", get_status(id))
}
on close_window(id: String, day: Int) {
if day <= 120 {
return map("ok", false, "reason", "window still open until day 120")
}
transition(id, "finalized")
return map("ok", true, "state", get_status(id))
}
on open_dispute(id: String, day: Int) {
if day > 120 {
return map("ok", false, "reason", "day {day} is past the 120-day window")
}
transition(id, "disputed") // raises if charge already finalized
return map("ok", true, "state", get_status(id))
}
on resolve(id: String, outcome: String) {
if outcome == "merchant_wins" {
transition(id, "upheld")
return map("ok", true, "state", "upheld")
}
transition(id, "reversed") // money goes back exactly once
let amt = amounts.get(id) ?? 0
merchant.set("acct", (merchant.get("acct") ?? 0) - amt)
return map("ok", true, "state", "reversed", "clawed_back", amt)
}
on merchant_balance() {
return merchant.get("acct") ?? 0
}
}
cell test ChargebackTests {
rules {
assert capture("c1", 300).ok == true
assert capture("c2", 200).ok == true
assert merchant_balance() == 500
// in-window dispute on c1, cardholder wins: money moves back ONCE
assert open_dispute("c1", 45).ok == true
assert resolve("c1", "cardholder_wins").clawed_back == 300
assert merchant_balance() == 200
// THE DOUBLE REVERSAL: terminal state, second clawback has no edge
assert_fails transition("c1", "reversed")
assert_fails transition("c1", "disputed")
// c2 survives the window and is finalized
assert close_window("c2", 100).ok == false
assert close_window("c2", 121).ok == true
// THE LATE DISPUTE: day 130 — refused by guard AND by the machine
assert open_dispute("c2", 130).ok == false
assert_fails transition("c2", "disputed")
// the merchant account cannot be driven below zero
assert_fails merchant.set("acct", -1)
// merchant-wins path is just as final
assert capture("c3", 50).ok == true
assert open_dispute("c3", 10).ok == true
assert resolve("c3", "merchant_wins").ok == true
assert_fails transition("c3", "reversed")
}
}What the toolchain says
$ soma check chargeback_window.cell
✓ All checks passed.$ soma test chargeback_window.cell
test ChargebackTests ...
✓ assert capture("c1", 300).ok == true
✓ assert capture("c2", 200).ok == true
✓ assert merchant_balance() == 500
✓ assert open_dispute("c1", 45).ok == true
✓ assert resolve("c1", "cardholder_wins").clawed_back == 300
✓ assert merchant_balance() == 200
✓ assert_fails transition("c1", "reversed") — raised invalid transition: reversed → reversed. Current state: 'reversed'. Valid targets: []
✓ assert_fails transition("c1", "disputed") — raised invalid transition: reversed → disputed. Current state: 'reversed'. Valid targets: []
✓ assert close_window("c2", 100).ok == false
✓ assert close_window("c2", 121).ok == true
✓ assert open_dispute("c2", 130).ok == false
✓ assert_fails transition("c2", "disputed") — raised invalid transition: finalized → disputed. Current state: 'finalized'. Valid targets: []
✓ assert_fails merchant.set("acct", -1) — raised memory invariant violated on 'merchant': merchant >= 0 — rejected write of -1 (key "acct"); the slot is unchanged
✓ assert capture("c3", 50).ok == true
✓ assert open_dispute("c3", 10).ok == true
✓ assert resolve("c3", "merchant_wins").ok == true
✓ assert_fails transition("c3", "reversed") — raised invalid transition: upheld → reversed. Current state: 'upheld'. Valid targets: []
17 tests: 17 passed, 0 failed$ soma verify chargeback_window.cell
Verifying chargeback_window.cell...
State machine 'charge': 6 states, initial 'authorized'
States: [authorized, disputed, finalized, reversed, settled, upheld]
✓ 6 states, 5 transitions
✓ all states reachable from 'authorized'
✓ terminal states: [finalized, reversed, upheld]
✓ no deadlocks
✓ liveness: every state can eventually reach a terminal state
✓ think-isolated: CTL safety properties hold regardless of LLM output (4 handlers, 5 literal transitions, 0 dynamic)
✓ termination: all 5 handlers structurally terminate
✓ refinement: handler `capture` ⟶ {settled}
✓ refinement: handler `close_window` ⟶ {finalized}
✓ refinement: handler `open_dispute` ⟶ {disputed}
✓ refinement: handler `resolve` ⟶ {upheld [if outcome == "merchant_wins"], reversed}
· transition sources: `capture`, `close_window`, `open_dispute`, `resolve` call transition(id, target) without declaring the source — the runtime refuses a move the graph forbids, but the proof does not see where the handler starts; `transition(id, from, to)` names the edge (checked by `soma check`, refused at run time from any other state)
Chargeback/invariants:
✓ invariant merchant >= 0 — writer 'capture' proven (writes 0)
✓ invariant merchant >= 0 — writer 'capture' proven by induction (writes (merchant.get("acct") ?? 0) + amount)
⚠ invariant merchant >= 0 — runtime-checked (computed values): resolve → merchant because `merchant` has no known range
✓ invariant amounts >= 0 — writer 'capture' proven by induction (writes amount)
14 passed, 1 warnings, 0 failures
Temporal properties for 'charge':
✓ deadlock_free — no deadlocks in any reachable state
Temporal: 1 passed, 0 failed
VERIFY OK