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