ADR-006: Guard Analysis via Galois Connection

Context

Guard consistency checking — detecting contradictory or incomplete require clauses — needs a formal framework. Guards are predicates over state; we need to reason about their satisfiability and completeness.

Options evaluated:

Option	Soundness	Completeness	Complexity
Direct semantic analysis	Manual	Fragile	High
SAT/SMT solver	Yes	Yes	External dependency
Abstract interpretation (Galois connection)	Yes	Approximate	Moderate

Source: specs/theory.allium — “Galois Connection (guard analysis)” section (Th-2).

Decision

Model guard consistency as a Galois connection (α, γ) between:

• Concrete domain: P(State) — powerset of runtime state values
• Abstract domain: Predicates — guard expressions

Where α: P(State) → Predicates (abstraction) and γ: Predicates → P(State) (concretization). Soundness condition: α(S) ⊑ P ⟺ S ⊆ γ(P).

Two consistency checks follow directly from the framework:

• Guard overlap: γ(guard₁) ∩ γ(guard₂) ≠ ∅ implies ambiguity (two guards can match the same state simultaneously).
• Guard gap: ⋃ γ(guardᵢ) ⊊ State implies incompleteness (some states match no guard).

The initial implementation uses abstract interpretation rather than full concretization. Precision depends on the abstract domain chosen; this is tunable over time.

Consequences

Positive

• Sound by construction: if the abstract analysis says guards are consistent, they are.
• Provides both overlap detection (ambiguity) and gap detection (incompleteness) from the same framework.
• Extends naturally to more precise abstract domains without changing the architecture.

Negative

• Initial implementation approximates — may produce false positives (spurious warnings).
• Complex theoretical foundation; contributors must understand abstract interpretation.
• Full concretization (SMT-backed) is deferred; precision is bounded by the abstract domain.