soma.cell

Lab chain of custody — a sample whose custody broke can never be reported, by construction A forensic toxicology or pathology result is only as trustworthy as the unbroken chain of custody behind it

If a sample is left unsealed, or its identity can't be accounted for at any handoff, the result is inadmissible and clinically worthless — but the dangerous version is the lab that reports it anyway, and a treatment (or a conviction) rests on a possibly-swapped tube. Here a specimen walks collected → sealed → in_transit → received → analyzed → reported. The one terminal failure state is `compromised`: any custody break sends the sample there and it can NEVER reach `reported`. `soma verify` proves reported is unreachable from compromised, and that compromised is itself terminal — no "re-seal and pretend" path exists.

A Soma program from the medical part of the verified corpus: 125 lines, cells ChainOfCustody, CustodyTests. It passes soma check with soma 3.2.4.

How it is built

The cell ChainOfCustody declares 6 signals in its face: collect(sample: String) -> Map, handoff(sample: String, step: String) -> Map, breach(sample: String) -> Map, report(sample: String) -> Map, sample_state(sample: String) -> String and demo() -> String. Its state machine specimen starts in collected and allows 10 transitions: collected -> sealed, sealed -> in_transit, in_transit -> received, received -> analyzed, analyzed -> reported, collected -> compromised, sealed -> compromised, in_transit -> compromised, received -> compromised and analyzed -> compromised. compromised and reported are terminal. Handlers: collect (line 53), handoff (line 59), breach (line 67), report (line 75), sample_state (line 83) and demo (line 87).

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

Generated from soma describe on this file.

The source

chain_of_custody.cell

// ============================================================================
// LAB CHAIN OF CUSTODY — a sample whose custody broke can never be
// reported, by construction
// ============================================================================
//
// A forensic toxicology or pathology result is only as trustworthy as the
// unbroken chain of custody behind it. If a sample is left unsealed, or
// its identity can't be accounted for at any handoff, the result is
// inadmissible and clinically worthless — but the dangerous version is the
// lab that reports it anyway, and a treatment (or a conviction) rests on a
// possibly-swapped tube.
//
// Here a specimen walks collected → sealed → in_transit → received →
// analyzed → reported. The one terminal failure state is `compromised`:
// any custody break sends the sample there and it can NEVER reach
// `reported`. `soma verify` proves reported is unreachable from
// compromised, and that compromised is itself terminal — no "re-seal and
// pretend" path exists.
//
//   soma verify examples/corpus/medical/chain_of_custody.cell
//   soma test   examples/corpus/medical/chain_of_custody.cell
//   soma run    examples/corpus/medical/chain_of_custody.cell demo
// ============================================================================

cell ChainOfCustody {
    face {
        signal collect(sample: String) -> Map
        signal handoff(sample: String, step: String) -> Map
        signal breach(sample: String) -> Map
        signal report(sample: String) -> Map
        signal sample_state(sample: String) -> String
        signal demo() -> String
    }

    // `reportable` order: collected -> sealed -> in_transit -> received ->
    // analyzed -> reported. `compromised` is the TERMINAL trap: every
    // custody-bearing state can fall into it, none escape. verify proves
    // reported is unreachable once compromised.
    state specimen {
        initial: collected
        collected  -> sealed
        sealed     -> in_transit
        in_transit -> received
        received   -> analyzed
        analyzed   -> reported
        collected  -> compromised
        sealed     -> compromised
        in_transit -> compromised
        received   -> compromised
        analyzed   -> compromised
    }

    on collect(sample: String) {
        return map("ok", true, "state", get_status(sample))
    }

    // A legitimate handoff is the next step in the chain; the machine
    // rejects skipping a step (e.g. shipping an unsealed tube).
    on handoff(sample: String, step: String) {
        let r = try { transition(sample, step) }
        if r.error != () {
            return map("ok", false, "reason", "custody violation: {r.error}")
        }
        return map("ok", true, "state", get_status(sample))
    }

    on breach(sample: String) {
        let r = try { transition(sample, "compromised") }
        if r.error != () { return map("ok", false, "reason", "{r.error}") }
        return map("ok", true, "state", get_status(sample))
    }

    // Reporting is only reachable through an unbroken chain. A compromised
    // sample cannot transition to reported — the proof, not a policy memo.
    on report(sample: String) {
        let r = try { transition(sample, "reported") }
        if r.error != () {
            return map("ok", false, "reason", "cannot report: {r.error}")
        }
        return map("ok", true, "state", get_status(sample))
    }

    on sample_state(sample: String) {
        return get_status(sample)
    }

    on demo() {
        collect("tube-A")
        handoff("tube-A", "sealed")
        handoff("tube-A", "in_transit")
        breach("tube-A")                       // seal found broken at the dock
        let r = report("tube-A")               // REFUSED — chain is broken
        let st = sample_state("tube-A")
        print("after breach: report = {r}")
        print("final state:  {st}")
        return "demo done"
    }
}

cell test CustodyTests {
    rules {
        // an unbroken chain reaches reported
        assert collect("s1").ok == true
        assert handoff("s1", "sealed").ok == true
        assert handoff("s1", "in_transit").ok == true
        assert handoff("s1", "received").ok == true
        assert handoff("s1", "analyzed").ok == true
        assert report("s1").ok == true
        assert sample_state("s1") == "reported"

        // you cannot skip sealing — shipping a raw tube is rejected
        assert collect("s2").ok == true
        assert_fails transition("s2", "in_transit")

        // a breach is terminal and blocks reporting forever
        assert collect("s3").ok == true
        assert handoff("s3", "sealed").ok == true
        assert breach("s3").ok == true
        assert sample_state("s3") == "compromised"
        assert_fails transition("s3", "reported")
        assert_fails transition("s3", "sealed")
        assert report("s3").ok == false
    }
}

What the toolchain says

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

$ soma check chain_of_custody.cell
✓ All checks passed.
$ soma test chain_of_custody.cell
test CustodyTests ...
  ✓ assert collect("s1").ok == true
  ✓ assert handoff("s1", "sealed").ok == true
  ✓ assert handoff("s1", "in_transit").ok == true
  ✓ assert handoff("s1", "received").ok == true
  ✓ assert handoff("s1", "analyzed").ok == true
  ✓ assert report("s1").ok == true
  ✓ assert sample_state("s1") == "reported"
  ✓ assert collect("s2").ok == true
  ✓ assert_fails transition("s2", "in_transit") — raised invalid transition: collected → in_transit. Current state: 'collected'. Valid targets: [sealed, compromised]
  ✓ assert collect("s3").ok == true
  ✓ assert handoff("s3", "sealed").ok == true
  ✓ assert breach("s3").ok == true
  ✓ assert sample_state("s3") == "compromised"
  ✓ assert_fails transition("s3", "reported") — raised invalid transition: compromised → reported. Current state: 'compromised'. Valid targets: []
  ✓ assert_fails transition("s3", "sealed") — raised invalid transition: compromised → sealed. Current state: 'compromised'. Valid targets: []
  ✓ assert report("s3").ok == false

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

State machine 'specimen': 7 states, initial 'collected'
  States: [analyzed, collected, compromised, in_transit, received, reported, sealed]

  ✓ 7 states, 10 transitions
  ✓ all states reachable from 'collected'
  ✓ terminal states: [reported, compromised]
  ✓ no deadlocks
  ✓ liveness: every state can eventually reach a terminal state
  ⚠ dynamic transition targets: handler `handoff` 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 `handoff` 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 `handoff` ⟶ <dynamic>
  ✓ refinement (partial — dynamic targets fall back to runtime check): handler `breach` ⟶ {compromised}
  ✓ refinement (partial — dynamic targets fall back to runtime check): handler `report` ⟶ {reported}
  · transition sources: `breach`, `report` 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)

9 passed, 2 warnings, 0 failures

  Temporal properties for 'specimen':
  ✓ deadlock_free — no deadlocks in any reachable state
Temporal: 1 passed, 0 failed
VERIFY OK
$ soma run chain_of_custody.cell demo
after breach: report = {"ok": false, "reason": "cannot report: invalid transition: compromised → reported. Current state: 'compromised'. Valid targets: []"}
final state:  compromised
demo done

Builtins used

get_status, map, print, transition

Source file: /corpus/medical/chain_of_custody.cell · examples/corpus/medical/chain_of_custody.cell