module: Inventory

goal: "Deterministic item add/remove with rollback"

invariants:

  - "quantity >= 0"

  - "events are idempotent by id"

api:

  interfaces:

    - name: IInventoryService

      methods:

        - name: tryAdd

          in: { itemId: string, qty: int, traceId: string }

          out: { ok: bool, reason: string? }

          effects: [Emits(ItemAdded)]

        - name: tryRemove

          in: { itemId: string, qty: int, traceId: string }

          out: { ok: bool, reason: string? }

          effects: [Emits(ItemRemoved)]

events:

  - name: ItemAdded

    data: { itemId: string, qty: int, timestamp: long }

  - name: ItemRemoved

    data: { itemId: string, qty: int, timestamp: long }

constraints:

  perf: { mainThreadBudgetMs: 0.2 }

  memory: { allocBytesPerCall: 0 }

tests:

  - "Property: add then remove returns to initial state"

  - "Fuzz: random ops preserve quantity >= 0"