soma.cell

Reefer setpoint — the typo that thaws forty tonnes of tuna

Refrigerated containers are programmed by hand at the terminal: a tech keys the setpoint from the booking sheet. The classic, expensive typo is sign and unit confusion — +18 instead of -18 (cargo claims files are full of them), or a Fahrenheit value keyed into a Celsius controller. Frozen tuna, ice cream, plasma: one transposed character and the claim runs to hundreds of thousands of dollars, discovered three weeks later at the destination port. This controller's setpoint memory carries the frozen-cargo envelope as an invariant: nothing outside [-30, -10] C can ever BE the setpoint. The +18 typo isn't caught by a validator someone forgot to call on one code path — the memory itself refuses, and the reefer keeps its last safe value. Power state is a verified machine: you cannot program a unit that isn't on, and a tripped unit must be inspected before reuse.

A Soma program from the logistics part of the verified corpus: 111 lines, cells ReeferController, FrozenEnvelope. It passes soma check with soma 3.2.4.

How it is built

The cell ReeferController declares 6 signals in its face: power_on(unit: String) -> Map, program_setpoint(unit: String, celsius: Int) -> Map, trip_alarm(unit: String) -> Map, inspect_unit(unit: String) -> Map, setpoint_of(unit: String) -> Int and unit_state(unit: String) -> String; keeps 1 memory slot: setpoint_c (Map<String, Int>, persistent and consistent) under the invariant setpoint_c >= -30 && setpoint_c <= -10. Its state machine reefer starts in unpowered and allows 5 transitions: unpowered -> running, running -> unpowered, running -> tripped, tripped -> under_inspection and under_inspection -> unpowered. Handlers: power_on (line 46), program_setpoint (line 52), trip_alarm (line 65), inspect_unit (line 71), setpoint_of (line 78) and unit_state (line 79).

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

Generated from soma describe on this file.

The source

reefer_setpoint.cell

// ============================================================================
// REEFER SETPOINT — the typo that thaws forty tonnes of tuna
// ============================================================================
//
// Refrigerated containers are programmed by hand at the terminal: a tech
// keys the setpoint from the booking sheet. The classic, expensive typo
// is sign and unit confusion — +18 instead of -18 (cargo claims files are
// full of them), or a Fahrenheit value keyed into a Celsius controller.
// Frozen tuna, ice cream, plasma: one transposed character and the claim
// runs to hundreds of thousands of dollars, discovered three weeks later
// at the destination port.
//
// This controller's setpoint memory carries the frozen-cargo envelope as
// an invariant: nothing outside [-30, -10] C can ever BE the setpoint.
// The +18 typo isn't caught by a validator someone forgot to call on one
// code path — the memory itself refuses, and the reefer keeps its last
// safe value. Power state is a verified machine: you cannot program a
// unit that isn't on, and a tripped unit must be inspected before reuse.
// ============================================================================

cell ReeferController {
    face {
        signal power_on(unit: String) -> Map
        signal program_setpoint(unit: String, celsius: Int) -> Map
        signal trip_alarm(unit: String) -> Map
        signal inspect_unit(unit: String) -> Map
        signal setpoint_of(unit: String) -> Int
        signal unit_state(unit: String) -> String
    }

    memory {
        // frozen-cargo envelope, deg C. The +18 typo cannot exist here.
        setpoint_c: Map<String, Int> [persistent, consistent]
        invariant setpoint_c >= -30 && setpoint_c <= -10
    }

    state reefer {
        initial: unpowered
        unpowered  -> running
        running    -> unpowered
        running    -> tripped
        tripped    -> under_inspection
        under_inspection -> unpowered
    }

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

    on program_setpoint(unit: String, celsius: Int) {
        if get_status(unit) != "running" {
            let s = get_status(unit)
            return map("ok", false, "reason", "unit {unit} is {s} — cannot program")
        }
        let w = try { setpoint_c.set(unit, celsius) }
        if w.error != () {
            return map("ok", false,
                "reason", "REFUSED: {celsius} C is outside the frozen envelope [-30, -10]")
        }
        return map("ok", true, "unit", unit, "setpoint_c", celsius)
    }

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

    on inspect_unit(unit: String) {
        let r = try { transition(unit, "under_inspection") }
        if r.error != () { return map("ok", false, "reason", "{r.error}") }
        transition(unit, "unpowered")
        return map("ok", true, "unit", unit, "state", "unpowered")
    }

    on setpoint_of(unit: String) { return setpoint_c.get(unit) ?? -18 }
    on unit_state(unit: String) { return get_status(unit) }
}

cell test FrozenEnvelope {
    rules {
        // programmed correctly for frozen tuna
        assert power_on("RF-201").ok == true
        assert program_setpoint("RF-201", -18).ok == true
        assert setpoint_of("RF-201") == -18

        // THE TYPO: +18. The memory refuses; last safe value survives.
        assert program_setpoint("RF-201", 18).ok == false
        assert setpoint_of("RF-201") == -18
        assert_fails setpoint_c.set("RF-201", 18)
        assert_fails setpoint_c.set("RF-201", -45)

        // boundary values of the envelope are legal
        assert program_setpoint("RF-201", -30).ok == true
        assert program_setpoint("RF-201", -10).ok == true
        assert program_setpoint("RF-201", -9).ok == false

        // you cannot program a unit that is not running
        assert program_setpoint("RF-999", -18).ok == false

        // a tripped unit must pass inspection before it runs again
        assert trip_alarm("RF-201").ok == true
        assert program_setpoint("RF-201", -20).ok == false
        assert_fails transition("RF-201", "running")
        assert inspect_unit("RF-201").ok == true
        assert power_on("RF-201").ok == true
    }
}

What the toolchain says

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

$ soma check reefer_setpoint.cell
✓ All checks passed.
$ soma test reefer_setpoint.cell
test FrozenEnvelope ...
  ✓ assert power_on("RF-201").ok == true
  ✓ assert program_setpoint("RF-201", -18).ok == true
  ✓ assert setpoint_of("RF-201") == -18
  ✓ assert program_setpoint("RF-201", 18).ok == false
  ✓ assert setpoint_of("RF-201") == -18
  ✓ assert_fails setpoint_c.set("RF-201", 18) — raised memory invariant violated on 'setpoint_c': setpoint_c >= -30 && setpoint_c <= -10 — rejected write of 18 (key "RF-201"); the slot is unchanged
  ✓ assert_fails setpoint_c.set("RF-201", -45) — raised memory invariant violated on 'setpoint_c': setpoint_c >= -30 && setpoint_c <= -10 — rejected write of -45 (key "RF-201"); the slot is unchanged
  ✓ assert program_setpoint("RF-201", -30).ok == true
  ✓ assert program_setpoint("RF-201", -10).ok == true
  ✓ assert program_setpoint("RF-201", -9).ok == false
  ✓ assert program_setpoint("RF-999", -18).ok == false
  ✓ assert trip_alarm("RF-201").ok == true
  ✓ assert program_setpoint("RF-201", -20).ok == false
  ✓ assert_fails transition("RF-201", "running") — raised invalid transition: tripped → running. Current state: 'tripped'. Valid targets: [under_inspection]
  ✓ assert inspect_unit("RF-201").ok == true
  ✓ assert power_on("RF-201").ok == true

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

State machine 'reefer': 4 states, initial 'unpowered'
  States: [running, tripped, under_inspection, unpowered]

  ✓ 4 states, 5 transitions
  ✓ all states reachable from 'unpowered'
  ✓ reactive machine: no terminal state, and every reachable state can return to 'unpowered'
  ✓ no deadlocks
  ✓ liveness: every reachable state can return to 'unpowered' (reactive machine)
  ✓ think-isolated: CTL safety properties hold regardless of LLM output (3 handlers, 4 literal transitions, 0 dynamic)
  ✓ termination: all 6 handlers structurally terminate
  ✓ refinement: handler `power_on` ⟶ {running}
  ✓ refinement: handler `trip_alarm` ⟶ {tripped}
  ✓ refinement: handler `inspect_unit` ⟶ {under_inspection, unpowered}
  · transition sources: `power_on`, `trip_alarm`, `inspect_unit` 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)

ReeferController/invariants:

  ⚠ invariant setpoint_c >= -30 && setpoint_c <= -10 — runtime-checked (computed values): program_setpoint → setpoint_c because `celsius` is a parameter (narrow it: `require celsius >= -30 && celsius <= -10 else …`)

10 passed, 1 warnings, 0 failures

  Temporal properties for 'reefer':
  ✓ 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/reefer_setpoint.cell · examples/corpus/logistics/reefer_setpoint.cell