soma.cell

Invoice factoring — no advance on unverified paper, no double-selling

Greensill Capital collapsed in 2021 holding billions in "invoices" that were never verified — some for trade that hadn't happened, some financed twice through different vehicles. The two frauds are structural here: an invoice can only be SOLD from the verified state (the issued -> sold edge does not exist), and sold has no edge back to itself or to verified, so the same invoice cannot be advanced twice. The advance ledger caps the cash at 90% of face value and refuses negative writes.

A Soma program from the escrow_finance part of the verified corpus: 108 lines, cells Factoring, FactoringTests. It passes soma check with soma 3.2.4.

How it is built

The cell Factoring declares 6 signals in its face: issue_invoice(id: String, face_value: Int) -> Map, verify_delivery(id: String) -> Map, sell_invoice(id: String, advance: Int) -> Map, collect(id: String) -> Map, write_off(id: String) -> Map and advance_paid(id: String) -> Int; keeps 2 memory slots: advanced (Map<String, Int>, persistent and consistent) under the invariant advanced >= 0 and face_val (Map<String, Int>, persistent and consistent) under the invariant face_val >= 0. Its state machine invoice starts in drafted and allows 5 transitions: drafted -> issued, issued -> verified, verified -> sold, sold -> collected and sold -> defaulted. collected and defaulted are terminal. Handlers: issue_invoice (line 42), verify_delivery (line 50), sell_invoice (line 55), collect (line 65), write_off (line 72) and advance_paid (line 77).

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

Generated from soma describe on this file.

The source

invoice_factoring.cell

// ============================================================================
// INVOICE FACTORING — no advance on unverified paper, no double-selling
// ============================================================================
//
// Greensill Capital collapsed in 2021 holding billions in "invoices" that
// were never verified — some for trade that hadn't happened, some financed
// twice through different vehicles. The two frauds are structural here:
// an invoice can only be SOLD from the verified state (the issued -> sold
// edge does not exist), and sold has no edge back to itself or to verified,
// so the same invoice cannot be advanced twice. The advance ledger caps
// the cash at 90% of face value and refuses negative writes.
// ============================================================================

cell Factoring {
    face {
        signal issue_invoice(id: String, face_value: Int) -> Map
        signal verify_delivery(id: String) -> Map
        signal sell_invoice(id: String, advance: Int) -> Map
        signal collect(id: String) -> Map
        signal write_off(id: String) -> Map
        signal advance_paid(id: String) -> Int
    }

    memory {
        advanced: Map<String, Int> [persistent, consistent]
        invariant advanced >= 0
        face_val: Map<String, Int> [persistent, consistent]
        invariant face_val >= 0
    }

    // collected and defaulted are terminal. The fraud edges are ABSENT:
    // no issued -> sold (unverified paper), no sold -> sold (double-sale).
    state invoice {
        initial: drafted
        drafted -> issued
        issued -> verified
        verified -> sold
        sold -> collected
        sold -> defaulted
    }

    on issue_invoice(id: String, face_value: Int) {
        if face_value <= 0 { return map("ok", false, "reason", "bad face value") }
        transition(id, "issued")
        face_val.set(id, face_value)
        advanced.set(id, 0)
        return map("ok", true, "state", get_status(id))
    }

    on verify_delivery(id: String) {
        transition(id, "verified")    // raises unless invoice was issued
        return map("ok", true, "state", get_status(id))
    }

    on sell_invoice(id: String, advance: Int) {
        let fv = face_val.get(id) ?? 0
        if advance <= 0 || advance * 10 > fv * 9 {
            return map("ok", false, "reason", "advance must be in (0, 90% of {fv}]")
        }
        transition(id, "sold")        // raises unless verified — and only once
        advanced.set(id, advance)
        return map("ok", true, "advance", advance, "face", fv)
    }

    on collect(id: String) {
        transition(id, "collected")
        let fv = face_val.get(id) ?? 0
        let adv = advanced.get(id) ?? 0
        return map("ok", true, "rebate_to_seller", fv - adv)
    }

    on write_off(id: String) {
        transition(id, "defaulted")
        return map("ok", true, "loss", advanced.get(id) ?? 0)
    }

    on advance_paid(id: String) {
        return advanced.get(id) ?? 0
    }
}

cell test FactoringTests {
    rules {
        assert issue_invoice("inv1", 10000).ok == true
        // GREENSILL MOVE 1: advance cash on unverified paper — edge absent
        assert_fails transition("inv1", "sold")
        assert verify_delivery("inv1").ok == true
        // advance capped at 90% of face
        assert sell_invoice("inv1", 9500).ok == false
        assert sell_invoice("inv1", 9000).ok == true
        assert advance_paid("inv1") == 9000
        // GREENSILL MOVE 2: sell the same invoice again — no sold -> sold
        assert_fails transition("inv1", "sold")
        assert_fails transition("inv1", "verified")
        // the ledger refuses a negative advance outright
        assert_fails advanced.set("inv1", -1)
        // collection is terminal; a collected invoice cannot default too
        assert collect("inv1").rebate_to_seller == 1000
        assert_fails transition("inv1", "defaulted")
        // default path on a second invoice, equally final
        assert issue_invoice("inv2", 5000).ok == true
        assert verify_delivery("inv2").ok == true
        assert sell_invoice("inv2", 4000).ok == true
        assert write_off("inv2").loss == 4000
        assert_fails transition("inv2", "collected")
    }
}

What the toolchain says

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

$ soma check invoice_factoring.cell
✓ All checks passed.
$ soma test invoice_factoring.cell
test FactoringTests ...
  ✓ assert issue_invoice("inv1", 10000).ok == true
  ✓ assert_fails transition("inv1", "sold") — raised invalid transition: issued → sold. Current state: 'issued'. Valid targets: [verified]
  ✓ assert verify_delivery("inv1").ok == true
  ✓ assert sell_invoice("inv1", 9500).ok == false
  ✓ assert sell_invoice("inv1", 9000).ok == true
  ✓ assert advance_paid("inv1") == 9000
  ✓ assert_fails transition("inv1", "sold") — raised invalid transition: sold → sold. Current state: 'sold'. Valid targets: [collected, defaulted]
  ✓ assert_fails transition("inv1", "verified") — raised invalid transition: sold → verified. Current state: 'sold'. Valid targets: [collected, defaulted]
  ✓ assert_fails advanced.set("inv1", -1) — raised memory invariant violated on 'advanced': advanced >= 0 — rejected write of -1 (key "inv1"); the slot is unchanged
  ✓ assert collect("inv1").rebate_to_seller == 1000
  ✓ assert_fails transition("inv1", "defaulted") — raised invalid transition: collected → defaulted. Current state: 'collected'. Valid targets: []
  ✓ assert issue_invoice("inv2", 5000).ok == true
  ✓ assert verify_delivery("inv2").ok == true
  ✓ assert sell_invoice("inv2", 4000).ok == true
  ✓ assert write_off("inv2").loss == 4000
  ✓ assert_fails transition("inv2", "collected") — raised invalid transition: defaulted → collected. Current state: 'defaulted'. Valid targets: []

16 tests: 16 passed, 0 failed
$ soma verify invoice_factoring.cell
Verifying invoice_factoring.cell...

State machine 'invoice': 6 states, initial 'drafted'
  States: [collected, defaulted, drafted, issued, sold, verified]

  ✓ 6 states, 5 transitions
  ✓ all states reachable from 'drafted'
  ✓ terminal states: [collected, defaulted]
  ✓ no deadlocks
  ✓ liveness: every state can eventually reach a terminal state
  ✓ think-isolated: CTL safety properties hold regardless of LLM output (5 handlers, 5 literal transitions, 0 dynamic)
  ✓ termination: all 6 handlers structurally terminate
  ✓ refinement: handler `issue_invoice` ⟶ {issued}
  ✓ refinement: handler `verify_delivery` ⟶ {verified}
  ✓ refinement: handler `sell_invoice` ⟶ {sold}
  ✓ refinement: handler `collect` ⟶ {collected}
  ✓ refinement: handler `write_off` ⟶ {defaulted}
  · transition sources: `issue_invoice`, `verify_delivery`, `sell_invoice`, `collect`, `write_off` 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)

Factoring/invariants:

  ✓ invariant advanced >= 0 — writer 'issue_invoice' proven (writes 0)
  ✓ invariant advanced >= 0 — writer 'sell_invoice' proven by induction (writes advance)
  ✓ invariant face_val >= 0 — writer 'issue_invoice' proven by induction (writes face_value)

15 passed, 0 warnings, 0 failures

  Temporal properties for 'invoice':
  ✓ 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/invoice_factoring.cell · examples/corpus/escrow_finance/invoice_factoring.cell