soma.cell

Customs clearance — no release without an examination verdict

The 2019 Philadelphia seizure of 17.5 tonnes of cocaine aboard the MSC Gayane worked because the containers were HELD at the port until CBP finished examining them. The failure mode customs agencies fear is the opposite: a "port runner" — cargo that leaves the terminal while its entry is still under review, or after a seizure order. Once goods are on a truck, the border has already failed. This lifecycle makes the run impossible in the record system: `released` is reachable ONLY from `cleared`, an exam hold must return a verdict before anything moves, and `seized` is TERMINAL — a seizure order can never be walked back to circulation. soma verify proves all three.

A Soma program from the logistics part of the verified corpus: 112 lines, cells Customs, NoPortRunners. It passes soma check with soma 3.2.4.

How it is built

The cell Customs declares 6 signals in its face: file_entry(entry: String, duty_cents: Int) -> Map, flag_for_exam(entry: String) -> Map, exam_verdict(entry: String, verdict: String) -> Map, clear_entry(entry: String) -> Map, release_cargo(entry: String) -> Map and entry_status(entry: String) -> String; keeps 1 memory slot: duty (Map<String, Int>, persistent and consistent) under the invariant duty >= 0. Its state machine entry_flow starts in filed and allows 6 transitions: filed -> under_review, under_review -> cleared, under_review -> exam_hold, exam_hold -> cleared, exam_hold -> seized and cleared -> released. released and seized are terminal. Handlers: file_entry (line 45), flag_for_exam (line 53), exam_verdict (line 59), clear_entry (line 68), release_cargo (line 74) and entry_status (line 80).

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

Generated from soma describe on this file.

The source

customs_clearance.cell

// ============================================================================
// CUSTOMS CLEARANCE — no release without an examination verdict
// ============================================================================
//
// The 2019 Philadelphia seizure of 17.5 tonnes of cocaine aboard the MSC
// Gayane worked because the containers were HELD at the port until CBP
// finished examining them. The failure mode customs agencies fear is the
// opposite: a "port runner" — cargo that leaves the terminal while its
// entry is still under review, or after a seizure order. Once goods are
// on a truck, the border has already failed.
//
// This lifecycle makes the run impossible in the record system: `released`
// is reachable ONLY from `cleared`, an exam hold must return a verdict
// before anything moves, and `seized` is TERMINAL — a seizure order can
// never be walked back to circulation. soma verify proves all three.
// ============================================================================

cell Customs {
    face {
        signal file_entry(entry: String, duty_cents: Int) -> Map
        signal flag_for_exam(entry: String) -> Map
        signal exam_verdict(entry: String, verdict: String) -> Map
        signal clear_entry(entry: String) -> Map
        signal release_cargo(entry: String) -> Map
        signal entry_status(entry: String) -> String
    }

    memory {
        // assessed duty per entry, in cents — never negative
        duty: Map<String, Int> [persistent, consistent]
        invariant duty >= 0
    }

    // released and seized are terminal: gone is gone, seized is seized.
    state entry_flow {
        initial: filed
        filed        -> under_review
        under_review -> cleared
        under_review -> exam_hold
        exam_hold    -> cleared
        exam_hold    -> seized
        cleared      -> released
    }

    on file_entry(entry: String, duty_cents: Int) {
        let w = try { duty.set(entry, duty_cents) }
        if w.error != () { return map("ok", false, "reason", "duty cannot be negative") }
        let r = try { transition(entry, "under_review") }
        if r.error != () { return map("ok", false, "reason", "{r.error}") }
        return map("ok", true, "entry", entry, "duty_cents", duty_cents)
    }

    on flag_for_exam(entry: String) {
        let r = try { transition(entry, "exam_hold") }
        if r.error != () { return map("ok", false, "reason", "{r.error}") }
        return map("ok", true, "state", "exam_hold")
    }

    on exam_verdict(entry: String, verdict: String) {
        if verdict != "cleared" && verdict != "seized" {
            return map("ok", false, "reason", "verdict must be cleared or seized")
        }
        let r = try { transition(entry, verdict) }
        if r.error != () { return map("ok", false, "reason", "{r.error}") }
        return map("ok", true, "state", verdict)
    }

    on clear_entry(entry: String) {
        let r = try { transition(entry, "cleared") }
        if r.error != () { return map("ok", false, "reason", "{r.error}") }
        return map("ok", true, "state", "cleared")
    }

    on release_cargo(entry: String) {
        let r = try { transition(entry, "released") }
        if r.error != () { return map("ok", false, "reason", "not cleared: {r.error}") }
        return map("ok", true, "state", "released")
    }

    on entry_status(entry: String) { return get_status(entry) }
}

cell test NoPortRunners {
    rules {
        // THE PORT RUN: release straight from review. No such edge.
        assert file_entry("E-100", 250000).ok == true
        assert release_cargo("E-100").ok == false
        assert_fails transition("E-100", "released")

        // a clean entry clears, then releases
        assert clear_entry("E-100").ok == true
        assert release_cargo("E-100").ok == true
        assert entry_status("E-100") == "released"

        // the Gayane: flagged, examined, SEIZED — terminal forever
        assert file_entry("E-666", 90000).ok == true
        assert flag_for_exam("E-666").ok == true
        assert exam_verdict("E-666", "seized").ok == true
        assert_fails transition("E-666", "cleared")
        assert_fails transition("E-666", "released")
        assert entry_status("E-666") == "seized"

        // an exam hold cannot be released without a verdict
        assert file_entry("E-7", 100).ok == true
        assert flag_for_exam("E-7").ok == true
        assert_fails transition("E-7", "released")

        // negative duty assessments are refused by the memory
        assert_fails duty.set("E-7", -500)
    }
}

What the toolchain says

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

$ soma check customs_clearance.cell
✓ All checks passed.
$ soma test customs_clearance.cell
test NoPortRunners ...
  ✓ assert file_entry("E-100", 250000).ok == true
  ✓ assert release_cargo("E-100").ok == false
  ✓ assert_fails transition("E-100", "released") — raised invalid transition: under_review → released. Current state: 'under_review'. Valid targets: [cleared, exam_hold]
  ✓ assert clear_entry("E-100").ok == true
  ✓ assert release_cargo("E-100").ok == true
  ✓ assert entry_status("E-100") == "released"
  ✓ assert file_entry("E-666", 90000).ok == true
  ✓ assert flag_for_exam("E-666").ok == true
  ✓ assert exam_verdict("E-666", "seized").ok == true
  ✓ assert_fails transition("E-666", "cleared") — raised invalid transition: seized → cleared. Current state: 'seized'. Valid targets: []
  ✓ assert_fails transition("E-666", "released") — raised invalid transition: seized → released. Current state: 'seized'. Valid targets: []
  ✓ assert entry_status("E-666") == "seized"
  ✓ assert file_entry("E-7", 100).ok == true
  ✓ assert flag_for_exam("E-7").ok == true
  ✓ assert_fails transition("E-7", "released") — raised invalid transition: exam_hold → released. Current state: 'exam_hold'. Valid targets: [cleared, seized]
  ✓ assert_fails duty.set("E-7", -500) — raised memory invariant violated on 'duty': duty >= 0 — rejected write of -500 (key "E-7"); the slot is unchanged

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

State machine 'entry_flow': 6 states, initial 'filed'
  States: [cleared, exam_hold, filed, released, seized, under_review]

  ✓ 6 states, 6 transitions
  ✓ all states reachable from 'filed'
  ✓ terminal states: [seized, released]
  ✓ no deadlocks
  ✓ liveness: every state can eventually reach a terminal state
  ⚠ dynamic transition targets: handler `exam_verdict` uses a dynamic (computed) transition target — the state these handlers move to is computed at run time (from input or an LLM answer), so the machine's safety is checked at run time for them, not proven
  ✓ termination: all 6 handlers structurally terminate
  ⚠ refinement (partial — dynamic targets fall back to runtime check): handler `exam_verdict` calls transition() with a computed target — which edge it takes is checked at run time (invalid_transition), not proven; write the target as a literal state to have it verified
  ✓ refinement (partial — dynamic targets fall back to runtime check): handler `file_entry` ⟶ {under_review}
  ✓ refinement (partial — dynamic targets fall back to runtime check): handler `flag_for_exam` ⟶ {exam_hold}
  ✓ refinement (partial — dynamic targets fall back to runtime check): handler `exam_verdict` ⟶ <dynamic>
  ✓ refinement (partial — dynamic targets fall back to runtime check): handler `clear_entry` ⟶ {cleared}
  ✓ refinement (partial — dynamic targets fall back to runtime check): handler `release_cargo` ⟶ {released}
  · transition sources: `file_entry`, `flag_for_exam`, `clear_entry`, `release_cargo` 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)

Customs/invariants:

  ⚠ invariant duty >= 0 — runtime-checked (computed values): file_entry → duty because `duty_cents` is a parameter (narrow it: `require duty_cents >= 0 else …`)

11 passed, 3 warnings, 0 failures

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

Builtins used

get_status, map, transition

Source file: /corpus/logistics/customs_clearance.cell · examples/corpus/logistics/customs_clearance.cell