Guard & Constraint Checks

Guard Consistency

When a decide clause has multiple require guards, their conjunction must be satisfiable. Contradictory guards (e.g., require x > 10 and require x < 5) make the clause unreachable.

Contradictory guards on decide(AddItem, Active): guards are mutually exclusive.
Review require clauses — their conjunction can never be true

The abstract interpreter detects equality contradictions, boolean negations, and numeric range conflicts. When the abstract domain cannot determine satisfiability, no error is emitted (sound approximation).

When multiple guarded decide clauses exist for the same (Command, State) pair and their guards overlap (the intersection is satisfiable), the compiler emits a warning:

Overlapping guards on decide(Register, Initial): clauses may both match.
Add mutually exclusive guards or merge into a single clause

require false Deprecation

The require false else reject "message" pattern is a hard error. Use rejection clauses instead:

require false is deprecated. Use: -> already|forbidden|impossible "message"

Replace require false blocks with the appropriate rejection keyword. See Rejection Clauses for the three categories and their semantics.

Postcondition Derivability

Each ensure postcondition must be derivable from the corresponding evolve clause. The compiler verifies this statically using symbolic assignment tracking — postconditions are never checked at runtime.

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

The compiler builds an assignment map from the evolve definitions reached by the emitted events and pattern-matches each postcondition against it. Supported pattern categories:

• Identity: ensure field == old.field — derivable when the field is not assigned by any evolve in the chain
• Constant equality: ensure status == Active — derivable when evolve assigns the field to that exact literal
• Boolean shorthand: ensure active / ensure not deleted — shorthand for == true / == false
• Logical connectives: and/or expressions — checked operand by operand

Expressions that do not match a known pattern are treated as unknown: no error is emitted. This is a sound approximation — the absence of an error does not imply the postcondition is correct.

The old keyword refers to the state before the decide was invoked. For multi-event emissions, the compiler applies evolve clauses in emission order (left-fold), with later assignments shadowing earlier ones for the same field. The postcondition is checked against the final cumulative state.