soma.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.

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.

Generated from soma describe on this file.

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

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

$ 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

Builtins used

get_status, map, transition

Source file: /corpus/escrow_finance/chargeback_window.cell · examples/corpus/escrow_finance/chargeback_window.cell