soma.cell

Procurement — sealed bids stay sealed, and the unsealing ends the auction

Classic bid-rigging (a DOJ antitrust staple): a procurement officer leaks the standing low bid to a favored vendor, who then "submits" a bid one dollar under it — possible because the system can read bids before close and accept bids after. Both capabilities are removed here, structurally: bid amounts are unreadable until the tender leaves `accepting`, the unsealing transition is the same event that closes submissions forever, and one bid per vendor is a memory invariant — there is no "revised bid" after a peek. `awarded` is terminal: the contract cannot be quietly re-tendered for a do-over.

A Soma program from the civic part of the verified corpus: 112 lines, cells SealedTender, TenderTests. It passes soma check with soma 3.2.4.

How it is built

The cell SealedTender declares 5 signals in its face: submit_bid(vendor: String, amount: Int) -> Map, peek_bids() -> Map, unseal() -> Map, award_contract() -> Map and phase() -> String; keeps 2 memory slots: bid_count (Map<String, Int>, persistent and consistent) under the invariant bid_count >= 0 && bid_count <= 1 and sealed (Map<String, Int>, persistent and consistent) under the invariant sealed >= 1. Its state machine tender starts in accepting and allows 2 transitions: accepting -> unsealed and unsealed -> awarded. awarded is terminal. Handlers: phase (line 42), submit_bid (line 44), peek_bids (line 61), unseal (line 71) and award_contract (line 77).

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

Generated from soma describe on this file.

The source

procurement.cell

// ============================================================================
// PROCUREMENT — sealed bids stay sealed, and the unsealing ends the auction
// ============================================================================
// Classic bid-rigging (a DOJ antitrust staple): a procurement officer leaks
// the standing low bid to a favored vendor, who then "submits" a bid one
// dollar under it — possible because the system can read bids before close
// and accept bids after. Both capabilities are removed here, structurally:
// bid amounts are unreadable until the tender leaves `accepting`, the
// unsealing transition is the same event that closes submissions forever,
// and one bid per vendor is a memory invariant — there is no "revised bid"
// after a peek. `awarded` is terminal: the contract cannot be quietly
// re-tendered for a do-over.
// ============================================================================

cell SealedTender {
    face {
        signal submit_bid(vendor: String, amount: Int) -> Map
        signal peek_bids() -> Map
        signal unseal() -> Map
        signal award_contract() -> Map
        signal phase() -> String
    }

    memory {
        // vendor -> bids submitted. A second (revised) bid is unrepresentable.
        bid_count: Map<String, Int> [persistent, consistent]
        invariant bid_count >= 0 && bid_count <= 1

        // amounts must be positive — a $0 placeholder bid is refused.
        sealed: Map<String, Int> [persistent, consistent]
        invariant sealed >= 1
    }

    // One arrow forward only: unsealing closes submissions, awarding
    // closes the tender. No state re-opens the box.
    state tender {
        initial: accepting
        accepting -> unsealed
        unsealed -> awarded
    }

    on phase() { return get_status("tender") }

    on submit_bid(vendor: String, amount: Int) {
        if phase() != "accepting" {
            return map("ok", false, "reason", "tender is {phase()}")
        }
        let prior = bid_count.get(vendor) ?? 0
        let c = try { bid_count.set(vendor, prior + 1) }
        if c.error != () {
            return map("ok", false, "reason", "{vendor} already bid — no revisions")
        }
        let w = try { sealed.set(vendor, amount) }
        if w.error != () {
            return map("ok", false, "reason", "bid must be at least 1")
        }
        return map("ok", true, "vendor", vendor)
    }

    // The leak, refused: while accepting, amounts are not readable.
    on peek_bids() {
        if phase() == "accepting" {
            return map("ok", false, "reason", "bids are sealed until opening")
        }
        let names = sealed.keys()
        let out = map()
        for v in names { out[v] = sealed.get(v) ?? 0 }
        return map("ok", true, "bids", out)
    }

    on unseal() {
        let r = try { transition("tender", "unsealed") }
        if r.error != () { return map("ok", false, "reason", "{r.error}") }
        return map("ok", true, "bidders", len(sealed.keys()))
    }

    on award_contract() {
        let r = try { transition("tender", "awarded") }
        if r.error != () { return map("ok", false, "reason", "{r.error}") }
        let names = sealed.keys()
        let best = ""
        let low = 0
        for v in names {
            let amt = sealed.get(v) ?? 0
            if best == "" || amt < low {
                best = v
                low = amt
            }
        }
        return map("ok", true, "winner", best, "amount", low)
    }
}

cell test TenderTests {
    rules {
        assert submit_bid("acme", 100).ok == true
        assert submit_bid("rival", 90).ok == true
        assert peek_bids().ok == false                    // sealed means sealed
        assert submit_bid("acme", 89).ok == false         // no revised bid
        assert_fails bid_count.set("acme", 2)             // unrepresentable
        assert_fails sealed.set("ghost", 0)               // no placeholder bids
        assert award_contract().ok == false               // can't award sealed bids
        assert unseal().ok == true
        assert submit_bid("late", 1).ok == false          // unsealing closed the door
        assert peek_bids().ok == true
        assert award_contract().winner == "rival"
        assert phase() == "awarded"
        assert_fails transition("tender", "accepting")    // no re-tender
        assert_fails transition("tender", "unsealed")
    }
}

What the toolchain says

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

$ soma check procurement.cell
✓ All checks passed.
$ soma test procurement.cell
test TenderTests ...
  ✓ assert submit_bid("acme", 100).ok == true
  ✓ assert submit_bid("rival", 90).ok == true
  ✓ assert peek_bids().ok == false
  ✓ assert submit_bid("acme", 89).ok == false
  ✓ assert_fails bid_count.set("acme", 2) — raised memory invariant violated on 'bid_count': bid_count >= 0 && bid_count <= 1 — rejected write of 2 (key "acme"); the slot is unchanged
  ✓ assert_fails sealed.set("ghost", 0) — raised memory invariant violated on 'sealed': sealed >= 1 — rejected write of 0 (key "ghost"); the slot is unchanged
  ✓ assert award_contract().ok == false
  ✓ assert unseal().ok == true
  ✓ assert submit_bid("late", 1).ok == false
  ✓ assert peek_bids().ok == true
  ✓ assert award_contract().winner == "rival"
  ✓ assert phase() == "awarded"
  ✓ assert_fails transition("tender", "accepting") — raised invalid transition: awarded → accepting. Current state: 'awarded'. Valid targets: []
  ✓ assert_fails transition("tender", "unsealed") — raised invalid transition: awarded → unsealed. Current state: 'awarded'. Valid targets: []

14 tests: 14 passed, 0 failed
$ soma verify procurement.cell
Verifying procurement.cell...

State machine 'tender': 3 states, initial 'accepting'
  States: [accepting, awarded, unsealed]

  ✓ 3 states, 2 transitions
  ✓ all states reachable from 'accepting'
  ✓ terminal states: [awarded]
  ✓ no deadlocks
  ✓ liveness: every state can eventually reach a terminal state
  ✓ think-isolated: CTL safety properties hold regardless of LLM output (2 handlers, 2 literal transitions, 0 dynamic)
  ✓ termination: all 5 handlers structurally terminate
  ✓ refinement: handler `unseal` ⟶ {unsealed}
  ✓ refinement: handler `award_contract` ⟶ {awarded}
  · transition sources: `unseal`, `award_contract` 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)

SealedTender/invariants:

  ✓ invariant bid_count >= 0 — writer 'submit_bid' proven by induction (writes prior + 1)
  ⚠ invariant bid_count >= 0 && bid_count <= 1 — runtime-checked (computed values): submit_bid → bid_count [bid_count <= 1] because `prior + 1` is only known to lie in [1, 2] — narrow it: `require (prior + 1) <= 1 else …`
  ⚠ invariant sealed >= 1 — runtime-checked (computed values): submit_bid → sealed because `amount` is a parameter (narrow it: `require amount >= 1 else …`)

10 passed, 2 warnings, 0 failures

  Temporal properties for 'tender':
  ✓ deadlock_free — no deadlocks in any reachable state
Temporal: 1 passed, 0 failed
VERIFY OK

Builtins used

get_status, len, map, transition

Source file: /corpus/civic/procurement.cell · examples/corpus/civic/procurement.cell