soma.cell

Prescription interaction lockout — a lethal drug combination is refused

at the point of order, not flagged for later Serotonin syndrome (an MAOI plus an SSRI), fatal bleeds (warfarin plus an NSAID), torsade from stacked QT-prolongers — co-prescribing certain drugs can kill. Every CPOE system has an interaction checker; the recurring tragedy is alert fatigue, where the warning is one more dismissible pop-up and the order goes through anyway. Here the active medication list is the source of truth, and `prescribe` REFUSES to add a drug that interacts with anything already on the list — there is no "override" path in the data model, so the dangerous pair never coexists. A bounded count invariant also caps polypharmacy, the independent risk multiplier behind most interaction harm.

A Soma program from the medical part of the verified corpus: 142 lines, cells Pharmacy, PharmacyTests. It passes soma check with soma 3.2.4.

How it is built

The cell Pharmacy declares 5 signals in its face: prescribe(patient: String, drug: String) -> Map, discontinue(patient: String, drug: String) -> Map, interacts(a: String, b: String) -> Bool, active_count(patient: String) -> Int and demo() -> String; keeps 2 memory slots: drug_count (Map<String, Int>, persistent and consistent) under the invariant drug_count >= 0 && drug_count <= 12 and active (Map<String, String>, persistent). Handlers: interacts (line 45), list_for (line 60), prescribe (line 68), discontinue (line 86), active_count (line 98) and demo (line 102).

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

Generated from soma describe on this file.

The source

prescription_lockout.cell

// ============================================================================
// PRESCRIPTION INTERACTION LOCKOUT — a lethal drug combination is refused
// at the point of order, not flagged for later
// ============================================================================
//
// Serotonin syndrome (an MAOI plus an SSRI), fatal bleeds (warfarin plus
// an NSAID), torsade from stacked QT-prolongers — co-prescribing certain
// drugs can kill. Every CPOE system has an interaction checker; the
// recurring tragedy is alert fatigue, where the warning is one more
// dismissible pop-up and the order goes through anyway.
//
// Here the active medication list is the source of truth, and `prescribe`
// REFUSES to add a drug that interacts with anything already on the list —
// there is no "override" path in the data model, so the dangerous pair
// never coexists. A bounded count invariant also caps polypharmacy, the
// independent risk multiplier behind most interaction harm.
//
//   soma check examples/corpus/medical/prescription_lockout.cell
//   soma test  examples/corpus/medical/prescription_lockout.cell
//   soma run   examples/corpus/medical/prescription_lockout.cell demo
// ============================================================================

cell Pharmacy {
    face {
        signal prescribe(patient: String, drug: String) -> Map
        signal discontinue(patient: String, drug: String) -> Map
        signal interacts(a: String, b: String) -> Bool
        signal active_count(patient: String) -> Int
        signal demo() -> String
    }

    memory {
        // Number of active drugs per patient. Polypharmacy is itself a
        // hazard; the cap is a hard wall on how many concurrent orders
        // exist, independent of the pairwise checker.
        drug_count: Map<String, Int> [persistent, consistent]
        invariant drug_count >= 0 && drug_count <= 12

        // Active medication list per patient, stored as a joined string.
        active: Map<String, String> [persistent]
    }

    // The contraindication table — known dangerous pairs. Symmetric by
    // construction (we check both orderings at the call site).
    on interacts(a: String, b: String) {
        let bad = map(
            "warfarin",   list("aspirin", "ibuprofen", "naproxen"),
            "phenelzine", list("fluoxetine", "sertraline", "tramadol"),
            "fluoxetine", list("phenelzine", "tramadol"),
            "simvastatin", list("clarithromycin", "itraconazole"),
            "sildenafil", list("nitroglycerin")
        )
        let fwd = bad[a] ?? list()
        let rev = bad[b] ?? list()
        let hit_fwd = any(fwd, x => x == b)
        let hit_rev = any(rev, x => x == a)
        return hit_fwd || hit_rev
    }

    on list_for(patient: String) {
        let s = active.get(patient) ?? ""
        if s == "" { return list() }
        return split(s, ",")
    }

    // Add a drug ONLY if it interacts with nothing currently active. The
    // refusal is the lockout — no parameter, no flag, lets it through.
    on prescribe(patient: String, drug: String) {
        let current = list_for(patient)
        for d in current {
            if interacts(d, drug) {
                return map("ok", false, "reason",
                    "INTERACTION: {drug} with active {d} — order blocked")
            }
        }
        let n = drug_count.get(patient) ?? 0
        let w = try { drug_count.set(patient, n + 1) }
        if w.error != () {
            return map("ok", false, "reason", "polypharmacy cap: {w.error}")
        }
        let joined = join(push(current, drug), ",")
        active.set(patient, joined)
        return map("ok", true, "drug", drug, "active", n + 1)
    }

    on discontinue(patient: String, drug: String) {
        let current = list_for(patient)
        let kept = filter(current, d => d != drug)
        if len(kept) == len(current) {
            return map("ok", false, "reason", "{drug} not on the list")
        }
        active.set(patient, join(kept, ","))
        let n = drug_count.get(patient) ?? 0
        drug_count.set(patient, n - 1)
        return map("ok", true, "remaining", len(kept))
    }

    on active_count(patient: String) {
        return drug_count.get(patient) ?? 0
    }

    on demo() {
        prescribe("pt-1", "warfarin")
        let danger = prescribe("pt-1", "ibuprofen")   // bleed risk — REFUSED
        prescribe("pt-1", "metoprolol")               // unrelated — fine
        discontinue("pt-1", "warfarin")
        let now_ok = prescribe("pt-1", "ibuprofen")   // safe once warfarin gone
        let n = active_count("pt-1")
        print("ibuprofen w/ warfarin: {danger}")
        print("ibuprofen after stop:  {now_ok}")
        print("active drugs:          {n}")
        return "demo done"
    }
}

cell test PharmacyTests {
    rules {
        // the table is symmetric
        assert interacts("warfarin", "aspirin") == true
        assert interacts("aspirin", "warfarin") == true
        assert interacts("phenelzine", "sertraline") == true
        assert interacts("metoprolol", "aspirin") == false

        // first order is always fine; the interacting second is REFUSED
        assert prescribe("p", "warfarin").ok == true
        assert prescribe("p", "ibuprofen").ok == false   // lockout
        assert active_count("p") == 1                    // ibuprofen never added

        // a non-interacting drug goes on
        assert prescribe("p", "lisinopril").ok == true
        assert active_count("p") == 2

        // discontinue clears the conflict, then the order succeeds
        assert discontinue("p", "warfarin").ok == true
        assert prescribe("p", "ibuprofen").ok == true

        // the polypharmacy count can never go out of bounds
        assert_fails drug_count.set("p", -1)
        assert_fails drug_count.set("p", 13)
    }
}

What the toolchain says

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

$ soma check prescription_lockout.cell
✓ All checks passed.
$ soma test prescription_lockout.cell
test PharmacyTests ...
  ✓ assert interacts("warfarin", "aspirin") == true
  ✓ assert interacts("aspirin", "warfarin") == true
  ✓ assert interacts("phenelzine", "sertraline") == true
  ✓ assert interacts("metoprolol", "aspirin") == false
  ✓ assert prescribe("p", "warfarin").ok == true
  ✓ assert prescribe("p", "ibuprofen").ok == false
  ✓ assert active_count("p") == 1
  ✓ assert prescribe("p", "lisinopril").ok == true
  ✓ assert active_count("p") == 2
  ✓ assert discontinue("p", "warfarin").ok == true
  ✓ assert prescribe("p", "ibuprofen").ok == true
  ✓ assert_fails drug_count.set("p", -1) — raised memory invariant violated on 'drug_count': drug_count >= 0 && drug_count <= 12 — rejected write of -1 (key "p"); the slot is unchanged
  ✓ assert_fails drug_count.set("p", 13) — raised memory invariant violated on 'drug_count': drug_count >= 0 && drug_count <= 12 — rejected write of 13 (key "p"); the slot is unchanged

13 tests: 13 passed, 0 failed
$ soma verify prescription_lockout.cell
Verifying prescription_lockout.cell...

Pharmacy/invariants:

  ✓ invariant drug_count <= 12 — writer 'discontinue' proven by induction (writes n - 1)
  ✓ invariant drug_count >= 0 — writer 'prescribe' proven by induction (writes n + 1)
  ⚠ invariant drug_count >= 0 && drug_count <= 12 — runtime-checked (computed values): discontinue → drug_count [drug_count >= 0] because `n - 1` is only known to lie in [-1, 11] — narrow it: `require (n - 1) >= 0 else …`, prescribe → drug_count [drug_count <= 12] because `n + 1` is only known to lie in [1, 13] — narrow it: `require (n + 1) <= 12 else …`

2 passed, 1 warnings, 0 failures
Temporal: 0 passed, 0 failed
VERIFY OK
$ soma run prescription_lockout.cell demo
ibuprofen w/ warfarin: {"ok": false, "reason": "INTERACTION: ibuprofen with active warfarin — order blocked"}
ibuprofen after stop:  {"ok": true, "drug": "ibuprofen", "active": 2}
active drugs:          2
demo done

Builtins used

any, filter, join, len, list, map, print, push, split

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