Order completion rollup: all-cancelled and partially-failed orders both report 'completed' — intended?

Start with allFulfillmentsFailed() and the completion rollup in run(), then replay the testsuite scenarios using traces/s8_all_unavailable_amend_completes_empty.ndjson and traces/s7_partial_shipment_failure.ndjson. Confirm the intended status semantics with maintainers; done means an agreed behavior is covered by the relevant workflow checks or documented on allFulfillmentsFailed().

Summary

While running a formal-verification exercise over this reference app's workflows (details below, and previously referenced in #121), the model checker surfaced two reachable end states of the Order workflow that a reader of the order status alone would probably not expect. Both follow from the same line of logic, both are easy to reproduce, and both may well be intentional demo simplifications — filing this as a question about intent rather than a bug report.

The root is allFulfillmentsFailed() combined with the completion rollup in run():

status := OrderStatusCompleted
if wf.allFulfillmentsFailed() {   // failures >= 1 && failures == len(fulfillments)
    status = OrderStatusFailed
}

Only FulfillmentStatusFailed counts toward failure — cancelled does not — so:

Observation 1 — an order can complete with nothing fulfilled and nothing charged

Shortest path (two customer-visible steps):

1. Customer places an order in which every item is unavailable → status customerActionRequired, all fulfillments unavailable.
2. Customer sends the amend action (as the flow invites) → cancelUnavailableFulfillments() cancels all of them → each fulfillment's process() returns immediately → zero failures → final status completed, fulfillments all cancelled.

No charge was made, nothing shipped, and the order reports success. A Charge activity is never invoked on this path.

Observation 2 — partial failure reports as plain completed

With two fulfillments: one charge is declined (fulfillment → failed), the other fulfillment ships and delivers (→ completed). Since not all fulfillments failed, the order's final status is completed, with no partial marker at the status level. A caller reading only OrderStatus.Status (e.g. the orders list in the web UI) cannot distinguish this from full success; the per-fulfillment detail is present but requires drilling into the fulfillments array.

Questions for maintainers

1. Are these the intended semantics for the demo? (Entirely plausible — a partial-success status adds UI and API surface a teaching app may not want.)
2. If a change would be welcome, two minimal options, happy to PR either:
   • count cancelled fulfillments toward the "nothing succeeded" check, so the all-cancelled case ends cancelled/failed rather than completed; and/or
   • introduce a partiallyCompleted-style status (or a boolean on OrderStatus) when fulfillment outcomes are mixed.
3. If the current behavior is intended, would you take a short doc comment on allFulfillmentsFailed() noting that cancelled ≠ failed and that mixed outcomes report completed? That would make the intent legible to people using this app as a reference, which is presumably its job.

How this was found / how to reproduce

The workflows were driven unmodified through the SDK's testsuite (no server) to capture execution traces; several independently LLM-derived specs were replayed against those traces to establish faithfulness; then an exhaustive model check ran against intent invariants such as "completed implies some fulfillment completed." Both observations come with machine-found shortest counterexamples and captured trace witnesses:

• write-up + traces + counterexamples: https://github.com/jdubray/polygraph/tree/main/examples/polygraph-oms-go
• trace witnesses: traces/s8_all_unavailable_amend_completes_empty.ndjson (Observation 1), traces/s7_partial_shipment_failure.ndjson (Observation 2)

Reproducing Observation 1 by hand in the running app: add only out-of-stock items to an order, then choose "amend" when prompted — the order lands on completed.

Related: #121 (carrier-status validation on the Shipment workflow, from the same exercise).