soma.cell

Rack slot capacity — the pallet that brings down the aisle

Warehouse racking collapses kill. When a beam rated for 1,000 kg takes a 1,400 kg pallet, it doesn't fail politely — it buckles, sheds its load into the next bay, and entire aisles domino (the 2018 collapse at an English cold store buried a worker under hundreds of pallets; SEMA logs dozens of such collapses a year). The root cause is almost always the same: the WMS happily recorded a put-away the steel could not hold. Here the beam rating is a memory invariant. The put-away that would overload bay steel is not logged-and-regretted; the write itself is REFUSED, so the WMS record can never describe an overloaded beam.

A Soma program from the logistics part of the verified corpus: 85 lines, cells RackBay, BeamRatingIsLaw. It passes soma check with soma 3.2.4.

How it is built

The cell RackBay declares 4 signals in its face: put_away(bay: String, pallet_kg: Int) -> Map, pick_out(bay: String, pallet_kg: Int) -> Map, bay_load(bay: String) -> Int and headroom(bay: String) -> Int; keeps 1 memory slot: beam_kg (Map<String, Int>, persistent and consistent) under the invariant beam_kg >= 0 && beam_kg <= 1000. Handlers: put_away (line 31), pick_out (line 43), bay_load (line 54) and headroom (line 56).

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

Generated from soma describe on this file.

The source

rack_slot_capacity.cell

// ============================================================================
// RACK SLOT CAPACITY — the pallet that brings down the aisle
// ============================================================================
//
// Warehouse racking collapses kill. When a beam rated for 1,000 kg takes
// a 1,400 kg pallet, it doesn't fail politely — it buckles, sheds its
// load into the next bay, and entire aisles domino (the 2018 collapse at
// an English cold store buried a worker under hundreds of pallets; SEMA
// logs dozens of such collapses a year). The root cause is almost always
// the same: the WMS happily recorded a put-away the steel could not hold.
//
// Here the beam rating is a memory invariant. The put-away that would
// overload bay steel is not logged-and-regretted; the write itself is
// REFUSED, so the WMS record can never describe an overloaded beam.
// ============================================================================

cell RackBay {
    face {
        signal put_away(bay: String, pallet_kg: Int) -> Map
        signal pick_out(bay: String, pallet_kg: Int) -> Map
        signal bay_load(bay: String) -> Int
        signal headroom(bay: String) -> Int
    }

    memory {
        // kg currently resting on the bay's beam pair, rated 1,000 kg
        beam_kg: Map<String, Int> [persistent, consistent]
        invariant beam_kg >= 0 && beam_kg <= 1000
    }

    on put_away(bay: String, pallet_kg: Int) {
        if pallet_kg <= 0 { return map("ok", false, "reason", "pallet weight must be positive") }
        let current = bay_load(bay)
        let w = try { beam_kg.set(bay, current + pallet_kg) }
        if w.error != () {
            let free = 1000 - current
            return map("ok", false,
                "reason", "REFUSED: bay {bay} holds {current} kg, only {free} kg of beam rating left")
        }
        return map("ok", true, "bay", bay, "beam_kg", current + pallet_kg)
    }

    on pick_out(bay: String, pallet_kg: Int) {
        if pallet_kg <= 0 { return map("ok", false, "reason", "pick weight must be positive") }
        let current = bay_load(bay)
        // picking more than is there would record negative load — refused
        let w = try { beam_kg.set(bay, current - pallet_kg) }
        if w.error != () {
            return map("ok", false, "reason", "bay {bay} only holds {current} kg")
        }
        return map("ok", true, "bay", bay, "beam_kg", current - pallet_kg)
    }

    on bay_load(bay: String) { return beam_kg.get(bay) ?? 0 }

    on headroom(bay: String) { return 1000 - bay_load(bay) }
}

cell test BeamRatingIsLaw {
    rules {
        // two pallets fit under the rating
        assert put_away("A-03-2", 400).ok == true
        assert put_away("A-03-2", 550).ok == true
        assert bay_load("A-03-2") == 950
        assert headroom("A-03-2") == 50

        // THE COLLAPSE PALLET: 400 kg onto a beam with 50 kg of headroom.
        // The write is refused — the record never shows overloaded steel.
        assert put_away("A-03-2", 400).ok == false
        assert bay_load("A-03-2") == 950
        assert_fails beam_kg.set("A-03-2", 1350)

        // boundary: exactly the rating is legal
        assert put_away("A-03-2", 50).ok == true
        assert bay_load("A-03-2") == 1000
        assert put_away("A-03-2", 1).ok == false

        // picks free headroom again; over-picking is refused too
        assert pick_out("A-03-2", 550).ok == true
        assert bay_load("A-03-2") == 450
        assert pick_out("A-03-2", 500).ok == false
        assert_fails beam_kg.set("A-03-2", -50)
    }
}

What the toolchain says

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

$ soma check rack_slot_capacity.cell
✓ All checks passed.
$ soma test rack_slot_capacity.cell
test BeamRatingIsLaw ...
  ✓ assert put_away("A-03-2", 400).ok == true
  ✓ assert put_away("A-03-2", 550).ok == true
  ✓ assert bay_load("A-03-2") == 950
  ✓ assert headroom("A-03-2") == 50
  ✓ assert put_away("A-03-2", 400).ok == false
  ✓ assert bay_load("A-03-2") == 950
  ✓ assert_fails beam_kg.set("A-03-2", 1350) — raised memory invariant violated on 'beam_kg': beam_kg >= 0 && beam_kg <= 1000 — rejected write of 1350 (key "A-03-2"); the slot is unchanged
  ✓ assert put_away("A-03-2", 50).ok == true
  ✓ assert bay_load("A-03-2") == 1000
  ✓ assert put_away("A-03-2", 1).ok == false
  ✓ assert pick_out("A-03-2", 550).ok == true
  ✓ assert bay_load("A-03-2") == 450
  ✓ assert pick_out("A-03-2", 500).ok == false
  ✓ assert_fails beam_kg.set("A-03-2", -50) — raised memory invariant violated on 'beam_kg': beam_kg >= 0 && beam_kg <= 1000 — rejected write of -50 (key "A-03-2"); the slot is unchanged

14 tests: 14 passed, 0 failed
$ soma verify rack_slot_capacity.cell
Verifying rack_slot_capacity.cell...

RackBay/invariants:

  ✓ invariant beam_kg <= 1000 — writer 'pick_out' proven by induction (writes current - pallet_kg)
  ✓ invariant beam_kg >= 0 — writer 'put_away' proven by induction (writes current + pallet_kg)
  ⚠ invariant beam_kg >= 0 && beam_kg <= 1000 — runtime-checked (computed values): pick_out → beam_kg [beam_kg >= 0] because `current - pallet_kg` is only known to lie in (-∞, 999] — narrow it: `require (current - pallet_kg) >= 0 else …`, put_away → beam_kg [beam_kg <= 1000] because `current + pallet_kg` is only known to lie in [1, ∞) — narrow it: `require (current + pallet_kg) <= 1000 else …`

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

Builtins used

map

Source file: /corpus/logistics/rack_slot_capacity.cell · examples/corpus/logistics/rack_slot_capacity.cell