Postconditions

Syntax

decide(<Command>, <State>) {
  -> [<Event> { ... }]
  ensure <expression>
}

Behavior

ensure postconditions state a property that must hold after the events from a decide clause have been applied. The compiler verifies this statically — postconditions are never checked at runtime.

decide(AddItem, Active) {
  -> [ItemAdded { cartId, productId, quantity }]
  ensure items.length == old.items.length + 1
}

The old keyword references the state before the decision’s events are applied. After all events from the decide clause have been folded through evolve, the compiler checks whether the postcondition holds given the evolve definition.

Multi-event decisions

When a decide clause emits multiple events, the postcondition checks the final state after all events have been applied via left-fold:

decide(CompleteOrder, Active) {
  -> [ItemsReserved { orderId }, PaymentCharged { orderId, amount }]
  ensure status == Fulfilled
}

The compiler applies evolve(Active, ItemsReserved) and then evolve(<result>, PaymentCharged), then checks the postcondition against the resulting state.

How the compiler verifies postconditions

The compiler uses symbolic assignment tracking over evolve definitions. It builds an assignment map by walking the fold chain in emission order — each evolve clause for the (fromState, event) pair contributes its field assignments. The compiler then pattern-matches the postcondition expression against this map.

Supported patterns

Pattern	Example	Verified
Identity (field not modified)	`ensure status == old.status`	Yes — derivable when evolve does not assign the field
Constant equality	`ensure active == true`	Yes — derivable when evolve assigns the field to that literal
Boolean shorthand	`ensure active`	Yes — equivalent to `ensure active == true`
Negated boolean	`ensure not deleted`	Yes — equivalent to `ensure deleted == false`
Logical conjunction	`ensure active and confirmed`	Yes — each operand checked independently
Logical disjunction	`ensure active or pending`	Yes — derivable if either operand is derivable

Comparison operators (>, <, >=, <=) and complex expressions that cannot be reduced to the above patterns are treated as unknown — the compiler emits no error, but provides no guarantee. This is a sound over-approximation: absence of an error does not imply the postcondition holds at runtime.

Multi-event fold chain

For a decision emitting [E1, E2, E3], the compiler applies evolve clauses in order:

Locate evolve(fromState, E1) — record its field assignments, advance to toState
Locate evolve(toState, E2) — record its field assignments (later assignments shadow earlier ones for the same field), advance
Locate evolve(resultState, E3) — record its field assignments
Check the postcondition against the cumulative assignment map

A field assigned by a later event in the chain overrides the value assigned by an earlier event.

Error message format

When a postcondition is provably not derivable from the evolve definition:

Postcondition not derivable: 'active == false' cannot be verified from the evolve definition

The quoted expression is the exact postcondition text as written in the source file.