- name: reservation-checks-locked-stock
  where: "inventory.h"
  ensure: >-
    reserve must reject quantity greater than available while holding the mutex, before decrementing stock.