soma.cell

Two-hand press control — anti-tie-down, anti-repeat, structural

Mechanical power presses amputated thousands of hands a year before OSHA 1910.217. The classic defeat: tape one palm button down, feed the die with the free hand. Here the machine has NO path from `one_held` to `armed` — concurrent actuation (both buttons inside the 500 ms window) is the ONLY arming edge, so a tied-down button is a dead end that must be fully released. Anti-repeat is the same trick: `stroking` exits only to `released`, so holding both buttons cannot recycle the ram. The stroke ledger refuses a ram position outside the die set.

A Soma program from the safety_interlocks part of the verified corpus: 78 lines, cells PressControl, PressTests. It passes soma check with soma 3.2.4.

How it is built

The cell PressControl declares 5 signals in its face: press_both(id: String) -> String, press_one(id: String) -> String, let_go(id: String) -> String, cycle_ram(id: String) -> Map and ram_home(id: String) -> String; keeps 1 memory slot: ram_mm (Map<String, Int>, persistent and consistent) under the invariant ram_mm >= 0 && ram_mm <= 180. Its state machine actuators starts in released and allows 6 transitions: released -> armed, released -> one_held, one_held -> released, armed -> released, armed -> stroking and stroking -> released. Handlers: press_both (line 36), press_one (line 37), let_go (line 38), cycle_ram (line 40) and ram_home (line 49).

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

Generated from soma describe on this file.

The source

two_hand_press.cell

// TWO-HAND PRESS CONTROL — anti-tie-down, anti-repeat, structural.
// Mechanical power presses amputated thousands of hands a year before
// OSHA 1910.217. The classic defeat: tape one palm button down, feed the
// die with the free hand. Here the machine has NO path from `one_held`
// to `armed` — concurrent actuation (both buttons inside the 500 ms
// window) is the ONLY arming edge, so a tied-down button is a dead end
// that must be fully released. Anti-repeat is the same trick: `stroking`
// exits only to `released`, so holding both buttons cannot recycle the
// ram. The stroke ledger refuses a ram position outside the die set.

cell PressControl {
    face {
        signal press_both(id: String) -> String      // within the sync window
        signal press_one(id: String) -> String       // single / tied-down actuator
        signal let_go(id: String) -> String
        signal cycle_ram(id: String) -> Map
        signal ram_home(id: String) -> String
    }

    memory {
        // ram travel in mm; 0 = top dead center, 180 = full stroke
        ram_mm: Map<String, Int> [persistent, consistent]
        invariant ram_mm >= 0 && ram_mm <= 180
    }

    state actuators {
        initial: released
        released -> armed       // BOTH buttons within 500 ms — the only way
        released -> one_held    // a lone (possibly taped) button
        one_held -> released    // full release; never one_held -> armed
        armed -> released       // a hand came off before the stroke
        armed -> stroking
        stroking -> released    // anti-repeat: full release before re-arm
    }

    on press_both(id: String) { transition(id, "armed")  return get_status(id) }
    on press_one(id: String)  { transition(id, "one_held")  return get_status(id) }
    on let_go(id: String)     { transition(id, "released")  return get_status(id) }

    on cycle_ram(id: String) {
        let r = try { transition(id, "stroking") }
        if r.error != () {
            return map("ok", false, "reason", "stroke refused: hands not proven clear")
        }
        ram_mm.set(id, 180)
        return map("ok", true, "state", get_status(id), "ram_mm", ram_mm.get(id))
    }

    on ram_home(id: String) {
        transition(id, "released")
        ram_mm.set(id, 0)
        return get_status(id)
    }
}

cell test PressTests {
    rules {
        // tie-down: one button held forever NEVER arms the press
        assert press_one("p1") == "one_held"
        assert_fails transition("p1", "armed")
        assert_fails transition("p1", "stroking")
        assert cycle_ram("p1").ok == false
        assert let_go("p1") == "released"

        // the legitimate cycle: both buttons, stroke, full release
        assert press_both("p1") == "armed"
        assert cycle_ram("p1").ok == true
        assert ram_home("p1") == "released"

        // anti-repeat: a finished stroke cannot re-stroke without re-arm
        assert_fails transition("p1", "stroking")

        // the ram ledger refuses travel outside the die set
        assert_fails ram_mm.set("p1", 181)
        assert_fails ram_mm.set("p1", -5)
    }
}

What the toolchain says

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

$ soma check two_hand_press.cell
✓ All checks passed.
$ soma test two_hand_press.cell
test PressTests ...
  ✓ assert press_one("p1") == "one_held"
  ✓ assert_fails transition("p1", "armed") — raised invalid transition: one_held → armed. Current state: 'one_held'. Valid targets: [released]
  ✓ assert_fails transition("p1", "stroking") — raised invalid transition: one_held → stroking. Current state: 'one_held'. Valid targets: [released]
  ✓ assert cycle_ram("p1").ok == false
  ✓ assert let_go("p1") == "released"
  ✓ assert press_both("p1") == "armed"
  ✓ assert cycle_ram("p1").ok == true
  ✓ assert ram_home("p1") == "released"
  ✓ assert_fails transition("p1", "stroking") — raised invalid transition: released → stroking. Current state: 'released'. Valid targets: [armed, one_held]
  ✓ assert_fails ram_mm.set("p1", 181) — raised memory invariant violated on 'ram_mm': ram_mm >= 0 && ram_mm <= 180 — rejected write of 181 (key "p1"); the slot is unchanged
  ✓ assert_fails ram_mm.set("p1", -5) — raised memory invariant violated on 'ram_mm': ram_mm >= 0 && ram_mm <= 180 — rejected write of -5 (key "p1"); the slot is unchanged

11 tests: 11 passed, 0 failed
$ soma verify two_hand_press.cell
Verifying two_hand_press.cell...

State machine 'actuators': 4 states, initial 'released'
  States: [armed, one_held, released, stroking]

  ✓ 4 states, 6 transitions
  ✓ all states reachable from 'released'
  ✓ reactive machine: no terminal state, and every reachable state can return to 'released'
  ✓ no deadlocks
  ✓ liveness: every reachable state can return to 'released' (reactive machine)
  ✓ think-isolated: CTL safety properties hold regardless of LLM output (5 handlers, 5 literal transitions, 0 dynamic)
  ✓ termination: all 5 handlers structurally terminate
  ✓ refinement: handler `press_both` ⟶ {armed}
  ✓ refinement: handler `press_one` ⟶ {one_held}
  ✓ refinement: handler `let_go` ⟶ {released}
  ✓ refinement: handler `cycle_ram` ⟶ {stroking}
  ✓ refinement: handler `ram_home` ⟶ {released}
  · transition sources: `press_both`, `press_one`, `let_go`, `cycle_ram`, `ram_home` 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)

PressControl/invariants:

  ✓ invariant ram_mm >= 0 && ram_mm <= 180 — writer 'cycle_ram' proven (writes 180)
  ✓ invariant ram_mm >= 0 && ram_mm <= 180 — writer 'ram_home' proven (writes 0)

14 passed, 0 warnings, 0 failures

  Temporal properties for 'actuators':
  ✓ deadlock_free — no deadlocks in any reachable state
Temporal: 1 passed, 0 failed
VERIFY OK

Builtins used

get_status, map, transition

Source file: /corpus/safety_interlocks/two_hand_press.cell · examples/corpus/safety_interlocks/two_hand_press.cell