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.
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
$ 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