Skip to content
Weltenwanderer Weltenwanderer

ADR-015: Abstract Interpretation for Guard Satisfiability

Context

Guard consistency checking (ADR-006) requires determining whether the conjunction of multiple require guards on the same state transition is satisfiable. Two solver options:

OptionCompletenessDependenciesBuild complexity
SMT (Z3 via WASM)CompleteNative/WASM binaryHigh
Abstract interpretationIncompleteNone (pure TS)Low

The expression grammar (ADR-013) is now in place, making expression AST analysis possible. The majority of guard contradictions in real domain models are structural: equality contradictions (state.status == "active" AND state.status == "inactive"), boolean negations, and simple numeric range conflicts.

Decision

Use abstract interpretation as the initial satisfiability mechanism. The abstract domain operates over guard expression structure via AST pattern matching, detecting:

  • Equality contradictions on the same field with different literal values
  • Boolean negation of the same field or expression
  • Numeric range conflicts detectable by interval arithmetic on literal bounds
  • Overlap detection across decide clauses for the same (Command, State) pair
  • Three-valued satisfiability result: satisfiable | unsatisfiable | unknown
  • FieldDomain parameter (open domains only for now — extension point for future enum types)

This covers the common cases without a solver dependency. The Galois connection framework (ADR-006) is the standard mathematical basis for abstract interpretation: the abstraction function maps concrete guard semantics to the abstract domain; the concretisation function maps abstract domain elements back to sets of satisfying valuations.

A deferred upgrade path to full SMT solving (Z3 via WASM) is recorded in packages/language/specs/validation-consistency.allium for cases that exceed the abstract domain’s precision.

Guard gap detection is explicitly out of scope. It requires enumerable value domains (enum/union types in the grammar), which do not yet exist. State-variant gap detection remains feasible because decider states are already enumerable from the grammar.

Consequences

Positive

  • No native or WASM dependencies; the checker is pure TypeScript.
  • Fast execution: AST pattern matching with no solver overhead or startup cost.
  • Covers the majority of domain-model guard contradictions encountered in practice.
  • Aligns with the Galois connection framework — abstract interpretation is its standard implementation technique.
  • Three-valued semantics (unknown) ensure soundness: when the abstract domain cannot determine satisfiability, it reports unknown rather than a false positive or negative.
  • Overlap detection provides early warning of ambiguous dispatch without requiring full disjointness proofs.
  • FieldDomain parameter provides a clean extension point for future enum types without reworking the core algorithm.

Negative

  • Incomplete: will not detect contradictions requiring arithmetic reasoning (e.g., x > 5 AND x < 3 when bounds are computed, not literal).
  • May produce false negatives — reporting “consistent” when guards are actually contradictory.
  • The upgrade to SMT will require rework of the satisfiability interface and significant test additions.
  • Overlap detection may produce false positive warnings when guards are semantically disjoint but structurally similar to the abstract domain.