soma.cell

Load shedding — the transformer's nameplate is a wall, hospitals shed last

When demand outruns supply, somebody's lights go off — the only question is whose, and whether the choice is made by a priority plan or by a melting transformer. In February 2021, winter storm Uri forced ERCOT to shed 20,000 MW; where rotation plans failed, circuits feeding hospitals and water plants went dark alongside empty offices, and people died of cold. The two properties a shedding controller must keep: 1. The transformer NEVER carries more than nameplate. Here that is a memory invariant — connecting a feeder that would overload the bank is rejected at the write, not by an if-statement upstream. 2. Shedding follows priority: interruptible contracts (3) drop before commercial (2); critical loads (1 — hospitals, water) are never auto-shed. The shed handler structurally cannot pick a priority-1 feeder.

A Soma program from the energy part of the verified corpus: 112 lines, cells Shedder, ShedTests. It passes soma check with soma 3.2.4.

How it is built

The cell Shedder declares 3 signals in its face: connect_feeder(xf: String, feeder: String, mw: Int, priority: Int) -> Map, shed_next(xf: String) -> Map and bank_load(xf: String) -> Int; keeps 3 memory slots: bank_mw (Map<String, Int>, persistent and consistent) under the invariant bank_mw >= 0 && bank_mw <= 100, feeder_mw (Map<String, Int>, persistent and consistent) under the invariant feeder_mw >= 0 and feeder_pri (Map<String, Int>, persistent and consistent) under the invariant feeder_pri >= 1 && feeder_pri <= 3. Handlers: bank_load (line 42), connect_feeder (line 44) and shed_next (line 57).

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

Generated from soma describe on this file.

The source

load_shedding.cell

// ============================================================================
// LOAD SHEDDING — the transformer's nameplate is a wall, hospitals shed last
// ============================================================================
//
// When demand outruns supply, somebody's lights go off — the only question
// is whose, and whether the choice is made by a priority plan or by a
// melting transformer. In February 2021, winter storm Uri forced ERCOT to
// shed 20,000 MW; where rotation plans failed, circuits feeding hospitals
// and water plants went dark alongside empty offices, and people died of
// cold. The two properties a shedding controller must keep:
//
//   1. The transformer NEVER carries more than nameplate. Here that is a
//      memory invariant — connecting a feeder that would overload the bank
//      is rejected at the write, not by an if-statement upstream.
//   2. Shedding follows priority: interruptible contracts (3) drop before
//      commercial (2); critical loads (1 — hospitals, water) are never
//      auto-shed. The shed handler structurally cannot pick a priority-1
//      feeder.
// ============================================================================

cell Shedder {
    face {
        signal connect_feeder(xf: String, feeder: String, mw: Int, priority: Int) -> Map
        signal shed_next(xf: String) -> Map
        signal bank_load(xf: String) -> Int
    }

    memory {
        // total MW on each transformer bank — nameplate 100 MVA
        bank_mw: Map<String, Int> [persistent, consistent]
        invariant bank_mw >= 0 && bank_mw <= 100

        // "<xf>/<feeder>" -> MW carried
        feeder_mw: Map<String, Int> [persistent, consistent]
        invariant feeder_mw >= 0

        // "<xf>/<feeder>" -> 1 critical, 2 commercial, 3 interruptible
        feeder_pri: Map<String, Int> [persistent, consistent]
        invariant feeder_pri >= 1 && feeder_pri <= 3
    }

    on bank_load(xf: String) { return bank_mw.get(xf) ?? 0 }

    on connect_feeder(xf: String, feeder: String, mw: Int, priority: Int) {
        if mw <= 0 { return map("ok", false, "reason", "feeder load must be positive") }
        let p = try { feeder_pri.set("{xf}/{feeder}", priority) }
        if p.error != () { return map("ok", false, "reason", "priority must be 1..3") }
        let w = try { bank_mw.set(xf, bank_load(xf) + mw) }
        if w.error != () {
            feeder_pri.delete("{xf}/{feeder}")
            return map("ok", false, "reason", "nameplate wall: {w.error}")
        }
        feeder_mw.set("{xf}/{feeder}", mw)
        return map("ok", true, "bank_load", bank_load(xf))
    }

    on shed_next(xf: String) {
        // pick the LOWEST-priority connected feeder (highest number).
        // Priority 1 is structurally unpickable: the filter requires >= 2.
        let pick = ""
        let pick_pri = 1
        for k in feeder_mw.keys() {
            if starts_with(k, "{xf}/") {
                let pri = feeder_pri.get(k) ?? 1
                if pri > pick_pri { pick = k  pick_pri = pri }
            }
        }
        if pick == "" {
            return map("ok", false, "reason",
                "only critical load remains on {xf} — automatic shedding stops")
        }
        let mw = feeder_mw.get(pick) ?? 0
        bank_mw.set(xf, bank_load(xf) - mw)
        feeder_mw.delete(pick)
        feeder_pri.delete(pick)
        return map("ok", true, "shed", pick, "mw", mw, "bank_load", bank_load(xf))
    }
}

cell test ShedTests {
    rules {
        // build the bank: hospital, mall, interruptible smelter contract
        assert connect_feeder("t1", "hospital", 40, 1).ok == true
        assert connect_feeder("t1", "mall", 30, 2).ok == true
        assert connect_feeder("t1", "smelter", 25, 3).ok == true
        assert bank_load("t1") == 95

        // one more feeder would overload the bank — refused at the write
        assert connect_feeder("t1", "suburb", 10, 2).ok == false
        assert bank_load("t1") == 95

        // THE WALL itself: no handler, no overload
        assert_fails bank_mw.set("t1", 150)
        assert_fails bank_mw.set("t1", -5)

        // emergency: shed in priority order — interruptible first
        assert shed_next("t1").shed == "t1/smelter"
        assert bank_load("t1") == 70
        // commercial second
        assert shed_next("t1").shed == "t1/mall"
        assert bank_load("t1") == 40

        // the hospital is never auto-shed: the picker cannot choose pri 1
        assert shed_next("t1").ok == false
        assert bank_load("t1") == 40

        // garbage priorities are rejected by the memory
        assert_fails feeder_pri.set("t1/x", 0)
        assert_fails feeder_pri.set("t1/x", 9)
    }
}

What the toolchain says

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

$ soma check load_shedding.cell
✓ All checks passed.
$ soma test load_shedding.cell
test ShedTests ...
  ✓ assert connect_feeder("t1", "hospital", 40, 1).ok == true
  ✓ assert connect_feeder("t1", "mall", 30, 2).ok == true
  ✓ assert connect_feeder("t1", "smelter", 25, 3).ok == true
  ✓ assert bank_load("t1") == 95
  ✓ assert connect_feeder("t1", "suburb", 10, 2).ok == false
  ✓ assert bank_load("t1") == 95
  ✓ assert_fails bank_mw.set("t1", 150) — raised memory invariant violated on 'bank_mw': bank_mw >= 0 && bank_mw <= 100 — rejected write of 150 (key "t1"); the slot is unchanged
  ✓ assert_fails bank_mw.set("t1", -5) — raised memory invariant violated on 'bank_mw': bank_mw >= 0 && bank_mw <= 100 — rejected write of -5 (key "t1"); the slot is unchanged
  ✓ assert shed_next("t1").shed == "t1/smelter"
  ✓ assert bank_load("t1") == 70
  ✓ assert shed_next("t1").shed == "t1/mall"
  ✓ assert bank_load("t1") == 40
  ✓ assert shed_next("t1").ok == false
  ✓ assert bank_load("t1") == 40
  ✓ assert_fails feeder_pri.set("t1/x", 0) — raised memory invariant violated on 'feeder_pri': feeder_pri >= 1 && feeder_pri <= 3 — rejected write of 0 (key "t1/x"); the slot is unchanged
  ✓ assert_fails feeder_pri.set("t1/x", 9) — raised memory invariant violated on 'feeder_pri': feeder_pri >= 1 && feeder_pri <= 3 — rejected write of 9 (key "t1/x"); the slot is unchanged

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

Shedder/invariants:

  ✓ invariant bank_mw >= 0 — writer 'connect_feeder' proven by induction (writes bank_load(xf) + mw)
  ✓ invariant bank_mw <= 100 — writer 'shed_next' proven by induction (writes bank_load(xf) - mw)
  ⚠ invariant bank_mw >= 0 && bank_mw <= 100 — runtime-checked (computed values): connect_feeder → bank_mw [bank_mw <= 100] because `bank_load(xf) + mw` is only known to lie in [1, ∞) — narrow it: `require (bank_load(xf) + mw) <= 100 else …`, shed_next → bank_mw [bank_mw >= 0] because `bank_load(xf) - mw` is only known to lie in (-∞, 100] — narrow it: `require (bank_load(xf) - mw) >= 0 else …`
  ✓ invariant feeder_mw >= 0 — writer 'connect_feeder' proven by induction (writes mw)
  ✓ invariant feeder_mw >= 0 — writer 'shed_next' only deletes from 'feeder_mw' (a value invariant cannot break on a delete)
  ✓ invariant feeder_pri >= 1 && feeder_pri <= 3 — writer 'shed_next' only deletes from 'feeder_pri' (a value invariant cannot break on a delete)
  ⚠ invariant feeder_pri >= 1 && feeder_pri <= 3 — runtime-checked (computed values): connect_feeder → feeder_pri because `priority` is a parameter (narrow it: `require priority >= 1 && priority <= 3 else …`)

5 passed, 2 warnings, 0 failures
Temporal: 0 passed, 0 failed
VERIFY OK

Builtins used

map, starts_with

Source file: /corpus/energy/load_shedding.cell · examples/corpus/energy/load_shedding.cell