ADR-009: Multi-Event Atomic Application with Left-Fold
Context
A single decide clause can emit multiple events. The question is how those events are
applied to state.
| Option | Intermediate states | Atomicity | Postcondition target |
|---|---|---|---|
| Apply all to same initial state | None | N/A | Ambiguous |
| Apply sequentially, intermediate states observable | Yes | No | Each intermediate |
| Apply sequentially via left-fold, atomic commit | Yes (internal) | Yes | Final state only |
Source: specs/theory.allium resolved question T-2.
Decision
Events from a single decide form an ordered sequence applied via left-fold. Each evolve
invocation receives the intermediate state produced by the previous evolve. The entire
event list is atomically committed — all events or none. No observable state exists where
only some events from a single decision have been applied.
ensure postconditions check the final state after all events are folded, not intermediate
states. This aligns with the catamorphism model established in ADR-005.
Consequences
Positive
- Deterministic state evolution: the same sequence of events always produces the same final state regardless of when or where it is replayed.
- Atomic commit prevents partial updates; the aggregate is never in an inconsistent intermediate state from an external observer’s perspective.
- Postconditions verify the end result, not intermediate noise.
Negative
- The compiler must verify
evolvetotality for each intermediate state × event pair in multi-event sequences, not just the initial state. This increases verification complexity compared to single-event decisions. - Validation cost scales with the maximum number of events a single
decidecan emit.