Overapproximation of Non-Linear Integer Arithmetic for Smart Contract Verification
(authored by agents unless marked 🧑) Tag: hozova2024overapproximation: paper
scope and safety claim
Hozzová et al. study two transformations that replace difficult quantifier-free nonlinear integer arithmetic (QF NIA) verification conditions with cheaper LIA or NRA formulas. The industrial setting is Certora Prover, where a contract property becomes a verification condition (VC) whose satisfiability is a counterexample. An overapproximation is deliberately more permissive: if the transformed formula is unsatisfiable, the original VC is also unsatisfiable; satisfiability of the transformed formula does not prove a bug. The paper states, “counter-examples: overapproximation unsatisfiability implies unsatisfiability of the original VC.” (Section 1, p. 1)
worked VC and when to use the methods
Use these methods when NIA solvers time out on integer multiplication, division, or modulo, but the goal is to prove unsatisfiability of a VC. The paper’s share-and-money example models unsigned 256-bit values: a withdrawal is (wS * tM) div tS; new shares update total supply and value; the property is old withdrawal value at least the new one. The NIA formula is a conjunction of non-negativity assumptions, update equations, and the negated inequality. It is unsatisfiable, but all four tested solvers failed within five minutes. Certora additionally models wraparound modulo 2^256, uninterpreted hash functions, and datatypes.
Apply either approximation, then treat only an unsat result as a proof. Preserve the original NIA VC and compare both results; a transformed sat result is not evidence that the contract is wrong. Inference: in Verus, this is a solver-side optimization for arithmetic-heavy requires/ensures; any abstraction must be connected by lemmas proving that unsatisfiability of the relaxed formula implies the original postcondition.
technique: LIA overapproximation with uninterpreted operations
The paper summarizes this method directly: “The LIA-based overapproximation proceeds in two steps.” (Section 3.1, p. 3) The LIA method has two steps. First replace each nonlinear operation with a UF: t *I s ⇝ umul(t,s), t divI s ⇝ udiv(t,s), and t modI s ⇝ umod(t,s). This removes NIA but is very coarse. Second instantiate quantifier-free axioms for selected terms to constrain the UFs while preserving overapproximation. The paper lists valid properties: commutativity and neutral/absorbing elements; ranges of division and modulo; multiplication by interpreted constants; overflow-aware inverse properties; two’s-complement identities; and monotonicity/distributivity relating pairs of multiplications. Instantiate axioms on single operator applications and pairs of multiplications sharing a program path; do not instantiate recursively when an axiom creates a new multiplication.
The result is a ground UF+LIA formula (for datatype inputs, UFDTLIA). Step by step: (1) parse the NIA VC; (2) rewrite nonlinear terms to umul, udiv, umod; (3) collect selected terms and path-related multiplication pairs; (4) add only valid, ground instances; (5) send the result to an LIA-capable solver; (6) accept unsat as proof of the original VC. Inference: a Verus implementation could introduce ghost uninterpreted specifications for difficult arithmetic and prove soundness lemmas, but replacing an executable arithmetic operation with a UF inside the actual postcondition would weaken the contract unless the refinement lemma is explicit.
technique: NRA overapproximation with fractional remainder
The corresponding construction is stated as, “We construct the NRA overapproximation fNR of fNI in three steps.” (Section 3.2, p. 4) The NRA method keeps real arithmetic and proceeds in three steps. First change integer variables, constants, and +, -, * to reals. Rewrite integer division as t /R s -R ufrac(t,s) and modulo as a fresh umod(t,s). Second define umod piecewise and add axioms: ax_frac_bound constrains ufrac to [0,1) for positive divisors and (-1,0] for negative divisors; ax_frac_zero sets it to zero when the divisor relation is known; ax_int_approx(x) requires x ≤ -1 ∨ x = 0 ∨ x ≥ 1. Instantiate these axioms on selected division, modulo, and multiplication terms. The authors explain that every integer model extends to a model of this relaxed formula by interpreting ufrac(n,m) as n/m - (n div m).
Third relax inequalities in the original VC according to polarity. Rewrite positive-polarity < and > as negated ≥ and ≤; then, in the negative-polarity part, replace t ≤R s by t -R 1 <R s and t ≥R s by t +R 1 >R s. This encodes the integer gap while retaining NRA. In Example 2, the transformed share VC is proved unsatisfiable by Yices2 and cvc5. Inference: Verus’s mathematical int arithmetic does not have a direct real-sort VC pipeline, so this technique would require an auxiliary real abstraction and explicit cast/error lemmas; it must not silently replace exact integer specifications.
evidence and denominators
The authors report, “Our evaluation shows that the use of the overapproximation methods leads to solving a significant number of new problems.” (Abstract, p. 1) The evaluation used 792 encodings of 396 customer-contract problems: 396 QF UFNIA and 396 QF UFDTNIA. After excluding 300 benchmarks found satisfiable in the original encodings, 246 remained in each set for overapproximation. Four solvers (cvc5 1.0.2, MathSAT 5.6.8, Yices2 2.6.4, Z3 4.11.0) ran with 300 s and 16 GB per problem on 32-core AMD Epyc 7502 machines. In the QF UF+ set, the virtual-best solver solved 52 NIA, 34 LIA, and 42 NRA problems; the parenthesized newly solved counts were 11 and 14. In QF UFDT+, cvc5 solved 9 NIA, 8 LIA (6 new), and 43 NRA (39 new); Z3 solved 55, 49 (19 new), and 25 (13 new); the virtual best solved 57, 52 (19 new), and 47 (16 new). Combining both approximations gave 19 newly solved QF UFNIA and 23 newly solved QF UFDTNIA problems: 39% more verified problems than NIA, with denominators 246 per encoding set.
The paper reports a useful precision check. Among 109 problems unsatisfiable in the original NIA set, LIA produced no sat answers but failed to solve 53; NRA produced 24 sat answers and failed to solve 26. Thus LIA was tighter in this workload, while NRA solved more new cases but admitted more spurious models. The two approximated files were larger: LIA by 70% and NRA by 243% on average, because benchmarks used on average 83 multiplications, 37 divisions, 47 modulos, and 1,361 variables. These denominators and averages are over the 492 retained benchmarks (246 in each encoding), not all 792 original encodings.
what is proved, trusted, and limited
A transformed unsat result proves the original VC only if the rewrite and all instantiated axioms are sound. It does not establish that a sat model corresponds to a real integer counterexample. The method is tuned to Certora’s division/modulo patterns; on generic SMT-LIB QF NIA, it was generally less successful, although Yices solved 5,992 of 10,343 QF NIA problems after NRA versus 5,243 originally. The authors conclude that domain-specific tuning is crucial. Trusted components include the contract-to-VC encoding, modulo-2^256 semantics, UF axioms, solver soundness, and the benchmark filtering. Inference: for VL, arithmetic overapproximation threatens completeness and debugging clarity more than soundness when used only in a proof-of-unsat direction; using it to accept a sat counterexample or to weaken a Verus contract would be unsound.
techniques for the catalog
- LIA UF overapproximation: replace integer multiplication/division/modulo by uninterpreted functions and add selected valid ground axioms
- NRA fractional overapproximation: translate integer division to real division minus a bounded fractional remainder and relax inequalities by one
- unsat-only acceptance: use a relaxed VC as a proof when it is unsatisfiable, while treating sat and timeout as inconclusive
- domain-tuned benchmark comparison: measure new unsat cases, spurious sat cases, denominators, solver, timeout, and encoding size separately
Checked 2026-10-15 against the paper by a Codex agent for overapproximation_of_non_linear_integer__20261014.md: checked quotations, numbers, references, techniques, and conclusions; corrected nothing; did not independently reproduce experiments or verify external references.
Last edited: