Formalizing the Omega Test in Dafny

1 Introduction

• The work formalizes the Omega Test’s main projections in Dafny for systems of linear inequalities.The implementation represents rational coefficients, linear expressions, and constraint systems, together with their semantic interpretations.Source: §1 · p. 1
• The Real Shadow over-approximates solutions to establish unsatisfiability, while the Dark Shadow under-approximates them to establish satisfiability and lift solutions.Grey Shadow branches address boundary cases after the Dark Shadow fails, using additional equality constraints.Source: §1 · p. 1
• The central contribution is a Dafny verification structure using explicit contracts, invariants, and ghost predicates to connect executable code with the Omega Test’s mathematical meaning.The paper studies an elimination-based procedure rather than competing with existing solvers on performance or generality.Source: §1 · p. 1

2 Related Work

• Rocq’s omega tactic implemented only part of Pugh’s Omega Test, omitting the final Grey Shadow steps, and was later deprecated in favor of lia.The cited account describes lia as a complete procedure for Presburger arithmetic.Source: §2 · p. 2
• Lean’s omega tactic follows Pugh’s Omega algorithm but lacks the Dark and Grey Shadows and is not a complete decision procedure.Source: §2 · p. 2
• Isabelle/HOL’s presburger methods use periodicity and divisibility properties to eliminate integer variables rather than Omega Test shadow projections.Source: §2 · p. 2
• This implementation targets the Omega Test’s elimination steps in Dafny and verifies their semantic correctness, rather than providing a general Presburger-arithmetic solver.Source: §2 · p. 2

3 The Omega Test

• The Real Shadow over-approximates solutions, the Dark Shadow under-approximates them, and Grey Shadow explores boundary cases when only the Real Shadow finds a solution.An empty Real projection establishes unsatisfiability; a solution in the Dark projection establishes satisfiability.Source: §3 · p. 2
• For bounds L ≤ ax and bx ≤ U, the Real Shadow requires bL ≤ aU, while the Dark Shadow requires aU − bL > ab − a − b to guarantee an integer x.The Grey Shadow explores equations ax = L + i for 0 ≤ i < ab − a − b.Source: §3 · p. 2
• The implementation constructs the Dark Shadow before the Real Shadow to facilitate the proof for the recursive Dark Shadow call.Figure 1 summarizes the three shadows’ interaction and recursive calls.Source: §3 · pp. 2–3, Figure 1 · p. 3
• The recursive method processes a system containing inequalities, equalities, and divisibility constraints, updating the elimination order when divisibility or Grey branches alter the variable being processed.A divisibility case splits into finitely many residues by writing x = mq + r, with 0 ≤ r < m.Source: §3 · pp. 3–4
• In the example, eliminating x for the Dark Shadow produces 0 ≤ −2, so the resulting projection is unsatisfiable.The example first normalizes the inequalities, then pairs lower and upper bounds; inequalities without x are stored unchanged.Source: §3 · p. 4
• The Real Shadow produces 0 ≤ 0 and is satisfiable, so the algorithm proceeds to Grey Shadow branches.After eliminating x and then y, the Real projection is true while the Dark projection is false.Source: §3 · p. 4
• A Grey branch checks an equality such as 3x = 3y + 3; simplifying it to x = y + 1 permits substitution and finds a satisfying valuation.The example returns True with x = 1 and y = 0; when the coefficient of x is not 1, the algorithm instead derives divisibility constraints.Source: §3 · p. 5

4 Formal Representation

• Dafny specifications, loop invariants, ghost predicates, and lemmas generate proof obligations for the representations and transformations, whose satisfiability properties are proved to be preserved.The development also specifies termination for loops and recursive methods.Source: §4 · p. 5
• Because Dafny’s real type is non-executable, rational values use a custom representation with an integer numerator, positive denominator, and real-valued specification field.The validRational predicate connects the concrete fields to the mathematical fraction and is maintained by operations such as multiplication.Source: §4 · p. 5
• Terms pair variable names with rational coefficients, linear expressions combine term sequences with a constant, and inequalities are evaluated by testing whether the left-minus-right difference is non-positive.Sequences allow executable traversal and incremental construction during normalization and elimination.Source: §4 · p. 6
• The main recursive ConstraintSystem contains inequalities, equalities, and divisibility constraints, while specialized types represent partitioned inequalities and Dark Shadow source pairs and traces.Grey Shadow processing may introduce equalities and derive divisibility conditions.Source: §4 · pp. 6–7
• Equivalence is defined by matching evaluations or truth values under every valuation, rather than by structural equality of representations.This definition supports transformations such as normalization, term reordering, grouping, and duplicate removal without changing mathematical meaning.Source: §4 · p. 7

5 Verified Elimination

• Equalities with unit coefficients are substituted directly; non-unit coefficients undergo a GCD compatibility check and may yield divisibility constraints.Incompatible equalities prove unsatisfiability; compatible ones are rewritten to remove the current variable.Source: §5 · pp. 7–8
• For each variable, the Real Shadow combines every lower and upper bound and retains inequalities independent of that variable.The resulting projection is an over-approximation: its unsatisfiability proves the original system unsatisfiable, but its satisfiability does not prove the converse.Source: §5 · pp. 8–9
• Normalization combines repeated-variable coefficients, removes zero terms, and produces an equivalent inequality with one constant on the right.The normalizing method also specifies validity, variable preservation, and semantic equivalence.Source: §5 · p. 8
• The Dark Shadow adds a sufficient integer-feasibility condition, requiring integer-valued bounds and coefficients for its proof.Its projected inequalities are supported by a trace that records source bounds and their generated constraints.Source: §5 · p. 10
• Dark-trace specifications ensure every lower–upper bound pair has a corresponding recorded constraint and that the trace contains exactly the generated pairs.Loop invariants and indexed witnesses support the completeness properties used in verification.Source: §5 · pp. 10–11
• When the Dark Shadow is unsatisfiable but the Real Shadow is satisfiable, Grey Shadow branches test finitely many offsets from lower bounds.Branches add equalities, simplify them by GCD, and use substitution or divisibility constraints; a satisfying branch implies the original system is satisfiable.Source: §5 · pp. 11–12
• Divisibility constraints are eliminated by splitting into residue cases modulo the product of their divisors and replacing the variable with a quotient expression.For example, 3 | 2x + y yields the cases x = 3q, x = 3q + 1, and x = 3q + 2.Source: §5 · p. 12
• The method’s postconditions guarantee that a satisfiable result has a satisfying valuation and an unsatisfiable result has none.The final contract states both directions for the original system.Source: §5 · p. 12

6 Termination of the recursive method

• A Grey Shadow equality can recur indefinitely if represented again as inequalities while the same variable remains in the system.The example produces an ever-growing sequence of repeated constraints.Source: §6 · pp. 12–13
• Recording the equality as a divisibility condition allows finitely many residue cases instead of repeatedly adding the same Grey Shadow equality.The residue loop checks only 0 through m − 1, where m is the product of the divisors.Source: §6 · p. 13
• To the authors’ knowledge, this is the first formalized verified termination argument for the Omega Test, based on a lexicographic measure.The measure tracks elimination-order length, divisibility involvement, equality count, and current-variable side constraints.Source: §6 · p. 13
• The measure decreases when variables are eliminated, when residue splitting removes the head variable from divisibility constraints, and when equalities or side constraints are simplified.The divisibility component can decrease even when the elimination-order length stays unchanged.Source: §6 · p. 13

• Verification-friendly representations make the implementation proof-oriented rather than performance-oriented, with overhead from repeated traversals, copying, normalization, and reconstruction.Source: §7 · p. 13
• 49 minutes and 22 seconds on the reported machine are required to verify the full development, reflecting obligations across shadow, equality, and divisibility cases plus auxiliary lemmas and invariants.Source: §7 · p. 14
• The current elimination order simply finds variables one by one; future work could verify heuristics because order can change the number of generated inequalities or Grey branches.Source: §7 · p. 14
• The implementation mainly decides satisfiability rather than returning valuations, although some Dark Shadow proofs retain information for lifting projected solutions.Source: §7 · p. 14