# Equational Bit-Vector Solving via Strong Gröbner Bases

Jiaxin Song Email<EMAIL_ADDRESS>Shanghai Jiao Tong University, China Hong
Kong University of Science and Technology, China  Hongfei Fu Email:
<EMAIL_ADDRESS>is the corresponding author. Shanghai Jiao Tong
University, China Charles Zhang Email<EMAIL_ADDRESS>Hong Kong
University of Science and Technology, China

###### Abstract

Bit-vectors, which are integers in a finite number of bits, are ubiquitous in
software and hardware systems. In this work, we consider the satisfiability
modulo theories (SMT) of bit-vectors. Unlike normal integers, the arithmetics
of bit-vectors are modular upon integer overflow. Therefore, the SMT solving
of bit-vectors needs to resolve the underlying modular arithmetics. In the
literature, two prominent approaches for SMT solving are bit-blasting (that
transforms the SMT problem into boolean satisfiability) and integer solving
(that transforms the SMT problem into integer properties). Both approaches
ignore the algebraic properties of the modular arithmetics and hence could not
utilize these properties to improve the efficiency of SMT solving.

In this work, we consider the equational theory of bit-vectors and capture the
algebraic properties behind them via strong Gröbner bases. First, we apply
strong Gröbner bases to the quantifier-free equational theory of bit-vectors
and propose a novel algorithmic improvement in the key computation of
multiplicative inverse modulo a power of two. Second, we resolve the important
case of invariant generation in quantified equational bit-vector properties
via strong Gröbner bases and linear congruence solving. Experimental results
over an extensive range of benchmarks show that our approach outperforms
existing methods in both time efficiency and memory consumption.

##  1 Introduction

In software and hardware systems, integers are often represented by a finite
number of bits, resulting in _bit-vectors_ (or _machine integers_) that take
values from a bounded range. Unlike normal integer arithmetics, the integer
overflow in bit-vectors is often handled via modular arithmetics. This causes
a significant problem in verifying program correctness with bit-vectors. For
example, the conditional branch

if (x > 0 && y > 0) assert(x + y > 0);

is unsafe since the value of x + y may overflow, and simply treating the
variables x and y as unbounded integers would produce incorrect results. Thus,
integer overflow imposes a challenge to verify the correctness of bit-vector
programs.

As bit-vectors are rudimentary, the correctness of software and hardware
systems heavily relies on the correctness of bit-vector operations. Hence,
verification of bit-vector properties has received significant attention in
the literatures [52, 28, 23, 15]. An important subject in the verification of
bit-vectors is their satisfiability modulo theories (SMT) [8, 35] that aim to
solve the satisfiability of formulas over bit-vectors. In the SMT of bit-
vector theory, the formulas of concern usually include standard operations
such as addition, multiplication, bitwise-or/and, division, signed/unsigned
comparison, etc.

By distinguishing whether the overflow of bit-vectors is discarded immediately
or recorded by extra bits, bit-vectors can be of either _fixed_ or _flexible_
size. Fixed-size bit-vectors (see [6] and [35, Chapter 6]) completely throw
away the overflow bit, and hence the arithmetics are exactly the modular
arithmetics. Flexible-size bit-vectors [24, 54, 31] record the overflow by
specialized bits, and hence achieve varying size for a bit-vector.

In the literature, there are two prominent approaches to solving the SMT of
bit-vectors. The first approach is often called _bit-blasting_ [35, Chapter 6]
that transforms a bit-vector equivalently into the collection of bits in the
bit-vector and solves the SMT via boolean satisfiability. Bit-blasting has the
drawback that it completely breaks the algebraic structure behind bit-vector
arithmetics and hence cannot utilize the algebraic properties to improve SMT
solving. To resolve this drawback, the second approach [28, 32, 25] transforms
bit-vector arithmetics into integer arithmetics and solves the original
formula via integer SMT solving such as linear and polynomial integer
arithmetics. Its main obstacle is SMT solving of the polynomial theory of
integers which is highly difficult to handle.

To fully capture the algebraic structure of bit-vectors, Gröbner bases have
been applied to handle the equational theory of bit-vectors. Note that the
classical Gröbner basis [1, Chapter 1] is limited to polynomials with
coefficients from a field and cannot be applied to polynomials with
coefficients from the ring $\mathbb{Z}_{2^{d}}$ ($d>1$) of bit-vectors, since
the ring $\mathbb{Z}_{2^{d}}$ is a field only when $d=1$. To circumvent this
issue, several approaches [33, 12, 48] have considered extensions of Gröbner
bases. The work [33] considers Gröbner bases with coefficients from a
principal ideal domain (in particular, the set of integers) [1, Chapter 4].
The work [12] establishes the general theory of Gröbner bases over polynomials
with coefficients from a commutative Noetherian ring. The work [48] further
improves the computation of Gröbner bases in [12] by a heuristics. These
approaches are either too narrow (e.g., only considering principal ideal
domains) or too wide (that consider general commutative Noetherian rings),
resulting in excessive computations in Gröbner bases for bit-vectors.

In this work, we consider the SMT of fixed-size bit-vectors. We focus on the
SMT solving of the theory of polynomial equations over bit-vectors, which is
the basic class of SMT that considers polynomial (in)equations with modular
addition and multiplication, and finds applications in verification of
arithmetic circuits [33, 51]. This work aims to develop novel SMT-solving
algorithms that leverage the algebraic structure from the ring of bit-vectors
to improve the efficiency of SMT solving. Our detailed contributions are as
follows:

  * •

First, we propose a novel approach to solve the quantifier-free polynomial
equational theory of bit-vectors via strong Gröbner bases [39]. Strong Gröbner
bases extend Gröbner bases to polynomials with coefficients from a principal
ideal ring (PIR) and, therefore well fits bit-vectors. A key contribution here
is a theorem that establishes the connection between the existence of a
constant polynomial in an ideal and in a strong Gröbner basis for the ideal.

  * •

Second, we propose an algorithmic improvement for the key calculation of
multiplicative inverse modulo a power of two in the computation of strong
Gröbner bases. As multiplicative inverse is a main factor in computing strong
Gröbner bases, the improvement substantially speeds up SMT solving.

  * •

Third, we propose an invariant generation method for bit-vectors. Note that
invariant generation can be encoded as a special class of constraint Horn
clauses (CHC) and is an important case of quantified SMT solving [53]. We show
that the generation of polynomial equational invariants can be solved by
strong Gröbner bases and linear congruence solving.

We implement our approach in the cvc5 SMT solver [5]. Experimental results
over a wide range of benchmarks show that our approach substantially
outperforms existing approaches in both the number of solved instances, time
efficiency, and memory consumption. Especially, for quantifier-free SMT, our
method can solve $40\%$ more unsatisfiable instances compared to state-of-the-
art approaches. For polynomial invariant generation, our method achieves a
$20$X speedup and a $6$X reduction in memory usage.

##  2 Preliminaries

In this section, we present basic concepts in rings, polynomials, strong
Gröbner bases, and bit-vectors. We refer to standard textbooks (e.g., [4]) for
a detailed treatment of rings and polynomials.

###  2.1 Rings, Polynomials and the Ring of Bit-Vectors

Generally, a _ring_ is a non-empty set $R$ equipped with two binary operations
$+,\cdot:R\times R\rightarrow R$ (where $+$ is the abstract addition and
$\cdot$ is the abstract multiplication) and two constants $0$ and $1$, such
that (i) the addition $+$ is commutative and associative, (ii) the
multiplication $\cdot$ is associative and distributive over the addition,
(iii) the element $0$ is the identity element for the addition, and (iv) the
element $1$ is the identity element for the multiplication. Formally, a _ring_
is an algebraic structure $(R,+,\cdot,0,1)$ such that $R$ is a non-empty set,
$+,\cdot$ are functions from $R\times R$ into $R$, $0,1\in R$ are constants in
$R$, and the following properties hold for all $a,b,c\in R$:

  * •

$a+b=b+a$, $(a+b)+c=a+(b+c)$ and $(a\cdot b)\cdot c=a\cdot(b\cdot c)$;

  * •

$a\cdot(b+c)=(a\cdot b)+(a\cdot c)$ and $(b+c)\cdot a=(b\cdot a)+(c\cdot a)$;

  * •

$a+0=a$ and $a\cdot 1=1\cdot a=a$.

  * •

there is a unique element $d\in R$ (usually denoted by $-a$) such that
$a+d=0$.

A ring $(R,+,\cdot,0,1)$ is a _field_ if the multiplication is commutative and
for every $a\in R$, there exists $b\in R$ (called the _multiplicative inverse_
of $a$) such that $a\cdot b=b\cdot a=1$. The ring $(R,+,\cdot,0,1)$ is
_communicative_ if $a\cdot b=b\cdot a$ for all $a,b\in R$. In the following,
we always consider commutative rings when referring to a ring and only write
$R$ instead of $(R,+,\cdot,0,1)$ for the sake of brevity. A subset of $R$ is
called a _subring_ of $R$ if it contains $1$ and is closed under the ring
operations induced from $R$.

A typical example of a finite ring is the ring $\mathbb{Z}_{m}$ ($m$ is a
positive integer) of modular addition and multiplication w.r.t the modulus
$m$. In this work, we pay special attention to the ring $\mathbb{Z}_{p^{k}}$
where $p$ is prime and $k$ is a positive integer. Notice that when $k>1$,
$\mathbb{Z}_{p^{k}}$ is not a field as multiplicative inverse may not exist.
When $p=2$, $\mathbb{Z}_{2^{k}}$ is exactly the ring of bit-vectors with size
$k$. In the ring $\mathbb{Z}_{2^{k}}$, for any element
$a\in\mathbb{Z}_{2^{k}}\setminus\\{0\\}$, we define $\nu_{2}(a)$ to be the
maximum power of two that divides $a$, i.e., $a=2^{\nu_{2}(a)}\cdot b$ and
$2{\not|}\,b$ for some integer $b$.

A polynomial with coefficients from a ring is a finite summation of terms for
which a term is a product between an element in the ring (as the coefficient)
and the variables in the polynomial. Formally, let $R$ be a ring,
$x_{1},\ldots,x_{n}$ be $n$ variables and $\bm{x}:=\left\langle
x_{1},\ldots,x_{n}\right\rangle$. A _monomial_ is a product of the form
$\bm{x}^{\bm{\alpha}}:=x_{1}^{\alpha_{1}}\cdot\ldots\cdot x_{n}^{\alpha_{n}}$,
where
$\bm{\alpha}=\left\langle\alpha_{1},\ldots,\alpha_{n}\right\rangle\in\mathbb{N}^{n}$
is a vector of natural numbers for which each $\alpha_{i}$ specifies the
exponent of the variable $x_{i}$. We define
$\left|\bm{\alpha}\right|:=\alpha_{1}+\ldots+\alpha_{n}$ as the _degree_ of
the monomial $\bm{x}^{\bm{\alpha}}$. A _term_ $t$ is a product
$t=c\cdot\bm{x}^{\bm{\alpha}}$ where $c$ is an element in $R$ (as the
coefficient of the term) and $\bm{x}^{\bm{\alpha}}$ is a monomial. When
${\bm{\alpha}}$ is the zero vector, i.e., $\left\langle
0,\dots,0\right\rangle$, then the term $c\cdot\bm{x}^{\bm{\alpha}}$ is treated
as the constant element $c$. A _polynomial_ $f$ is a finite sum of terms,
i.e., $f=\sum_{i=1}^{\ell}t_{i}$, where each $t_{i}$ is a term. The _degree_
of a polynomial $f=\sum_{i=1}^{\ell}t_{i}$ with each term
$t_{i}=c_{i}\cdot\bm{x}^{{\bm{\alpha}}_{i}}$, denoted by
$\mathrm{deg}\left(f\right)$, is defined as $\max_{1\leq
i\leq\ell}\left|{\bm{\alpha}}_{i}\right|$. The set of all polynomials with
variables $x_{1},\ldots,x_{n}$ and coefficients from a ring $R$ is denoted by
$R[\bm{x}]$ (or $R[x_{1},\ldots,x_{n}]$). Moreover, we denote the set of
monomials and terms with variables $x_{1},\ldots,x_{n}$ and coefficients from
a ring $R$ by $M_{R}[\bm{x}]$ and $T_{R}[\bm{x}]$, respectively. It is
straightforward to verify that the polynomials in $R[\bm{x}]$ with the
intuitive addition and multiplication operations form a ring. See [27,
Definition 1.1.3] for details.

Given a polynomial $f\in R[\bm{x}]$, the polynomial evaluation $f(\bm{v})$ at
a vector $\bm{v}=\left\langle v_{1},\dots,v_{n}\right\rangle\in R^{n}$ is
defined as the value calculated by substituting each $x_{i}$ with $v_{i}$ in
the polynomial $f$. For a subset $F\subseteq R[\bm{x}]$, we define the
_variety_ of $F$, denoted by $\mathcal{V}(F)$, as the set of common roots of
polynomials in $F$. Formally, $\mathcal{V}(F):=\\{\bm{v}\in R^{n}\mid
f(\bm{v})=0\mbox{ for all }f\in F\\}$.

Let $d$ be a positive integer. An unsigned _bit-vector_ of size $d$ is a
vector of $d$ bits and represents an integer in $[0,2^{d}-1]$. The arithmetics
of unsigned bit-vectors of size $d$ follow the modular addition and
multiplication of the ring $\mathbb{Z}_{2^{d}}$. In this work, we call
$\mathbb{Z}_{2^{d}}$ the ring of bit-vectors of size $d$ and focus on
polynomials in $\mathbb{Z}_{2^{d}}[\bm{x}]$ where $x_{1},\dots,x_{n}$ are
variables that take integer values from $[0,2^{d}-1]$.

###  2.2 Strong Gröbner Bases

Strong Gröbner bases [39] are an extension of classical Gröbner bases [1] that
deal with the membership of ideals generated by a set of polynomials over a
principal ideal ring. To present strong Gröbner bases, we recall ideals as
follows.

Ideals. An _ideal_ $I$ of a ring $R$ is a subset $I\subseteq R$ such that (i)
the algebraic structure $(I,+)$ forms a group (i.e., $I$ is closed under the
addition and the additive inverse), and (ii) for all $a\in I$ and $r\in R$, we
have that $ra\in I$. For a finite subset $S=\\{a_{1},\ldots,a_{n}\\}$ of the
ring $R$, we define the set $\left\langle S\right\rangle:=\left\\{r_{1}\cdot
a_{1}+\ldots+r_{m}\cdot a_{m}\ :\ r_{i}\in R\right\\}$ as the ideal
_generated_ by $S$. Conversely, $S$ is called a _generating set_ of the ideal
$\left\langle S\right\rangle$. When $S$ is a subset of a subring $R^{\prime}$
of $R$, and $r_{i}$ comes from $R$, we especially denote the above set by
$\left\langle S:R^{\prime}\right\rangle_{R}$. We abbreviate $\left\langle
S:R^{\prime}\right\rangle_{R}$ as $\left\langle S\right\rangle_{R}$. By the
definition of variety, it can be verified that
$\mathcal{V}(S)=\mathcal{V}(\left\langle S\right\rangle)$ when $S\subseteq
R[\bm{x}]$. An ideal $I\subseteq R$ is _principal_ if $I=\left\langle
a\right\rangle$ for some $a\in R$. A fundamental problem is the ideal
membership that asks to check whether an element $b\in R$ belongs to the ideal
$\left\langle S\right\rangle$ generated by a finite set $S\subseteq R$.

Below we fix a ring $R$ and $n$ variables $x_{1},\ldots,x_{n}$. The key
ingredient in strong Gröbner bases is a polynomial reduction operation called
_strong reduction_. To present strong reduction, we first introduce monomial
orderings as follows.

_Monomial orderings_. A _monomial ordering_ $\prec$ over $M_{R}[\bm{x}]$ is a
total ordering over $M_{R}[\bm{x}]$. In this work, we consider _well-ordered_
monomial ordering, which means $\bm{x}^{\textbf{0}}\prec\bm{x}^{\bm{\alpha}}$
for any $\bm{\alpha}\neq 0$ and for any monomials $p,q,r$, if $p\prec q$, then
$p\cdot r\prec q\cdot r$. For example, the _lexicographical ordering_ (lex)
orders the monomials lexicographically by
$\left\langle\alpha_{1},\ldots,\alpha_{n}\right\rangle$. The _graded-reverse
lexicographical ordering_ (grevlex) is defined as the lexicographical ordering
over the tuple
$\left\langle\alpha_{1}+\ldots+\alpha_{n},\alpha_{1},\ldots,\alpha_{n}\right\rangle$.

Given a polynomial $f\in R[\bm{x}]$ and a well-ordered monomial ordering
$\prec$, the _leading monomial_ of $f$ is the maximum monomial among all the
monomials in the finite sum of terms of the polynomial $f$ under the ordering
$\prec$. We denote the leading monomial of a polynomial $f$ by
$\textsf{lm}(f)$. For example, if $x_{2}\prec x_{1}$ and
$f=x_{1}x_{2}-2x_{1}^{2}x_{2}$, the leading monomial of $f$ under grevlex
(i.e., $\textsf{lm}(f)$) is $x_{1}^{2}x_{2}$. Additionally, the _leading term_
$\textsf{lt}(f)$ and resp. _leading coefficient_ $\textsf{lc}(f)$ of a
polynomial $f$ are defined as the term containing the leading monomial and
resp. the coefficient of the leading term. Hence,
$\textsf{lt}(f)=-2x_{1}^{2}x_{2}$ and $\textsf{lc}(f)=-2$.

_Strong Gröbner bases_. Strong Gröbner bases provide a way to check the
membership of an ideal of a polynomial ring whose coefficients are from a
principal ideal ring. Here we first show the definition of these rings.

######  Definition 1 (Principal Ideal Ring [27]).

A _principal ideal ring_ (PIR) is a ring $R$ such that every ideal $I\subseteq
R$ is principal.

Especially, for any prime number $p$, the ring $\mathbb{Z}_{p^{k}}$ is a PIR.
Then, we present the strong reduction used in strong Gröbner bases as follows.

######  Definition 2 (Strong Reduction).

Let $G\neq\emptyset$ be a finite subset of $R[\bm{x}]\setminus\\{0\\}$ and
$f,h\in R[\bm{x}]\setminus\\{0\\}$. Then we say that $f$ _strongly reduces_ to
$h$ with respect to $G$, denoted by $f\twoheadrightarrow_{G}h$, if there
exists $t\in T_{R}[\bm{x}],g\in G$ such that $h=f-t\cdot g$ and
$\textsf{lt}(f)=t\cdot\textsf{lt}(g)$. Denote the transitive closure of
relation $\twoheadrightarrow_{G}$ by $\twoheadrightarrow_{G}^{*}$.

Note that when there exists $h$ such that $f\twoheadrightarrow_{G}h$, we say
$f$ is _strongly reducible with respect to $G$_. Otherwise, we say $f$ is
_irreducible with respect to $G$_. Now, we present the definition of strong
Gröbner bases, which work for PIRs.

######  Definition 3 (Strong Gröbner Basis [39]).

A _strong Gröbner basis_ for an ideal $I\subseteq R[\bm{x}]$ is a finite
subset $G\subseteq I$ such that for any polynomial $f\in R[\bm{x}]$, $f\in I$
if and only if $f\twoheadrightarrow_{G}^{*}0$.

While strong Gröbner bases do not always exist for general rings, they exist
for PIR. When $R$ is a PIR, Norton et al. [39] propose a constructive
algorithm for computing them in finite time, which can be summarized as
follows.

######  Theorem 4.

When $R$ is a PIR and $F\subseteq R[\bm{x}]$ is finite, Algorithm 6.4 of [39]
always returns a strong Gröbner basis of $\left\langle F\right\rangle$ in
finite time.

##  3 Quantifier-Free Equational Bit-Vector Theory

In this section, we introduce a novel approach for solving SMT formulas in the
quantifier-free equational bit-vector theory. This section is organized as
follows. First, we present the overall framework for SMT solving via strong
Gröbner bases. Second, we propose a key algorithmic improvement in the
computation for strong Gröbner bases, namely the calculation of the
multiplicative inverse in the ring $\mathbb{Z}_{2^{d}}$ of bit-vectors of size
$d$.

Below we fix the size $d$ for bit-vectors and $n$ variables
$x_{1},\ldots,x_{n}$ where each variable takes values from the ring
$\mathbb{Z}_{2^{d}}$. Let $V=\\{x_{1},\ldots,x_{n}\\}$. Formulas in the
quantifier-free equational bit-vector theory are given by the following
grammar:

$\phi::=f=g\,\mid\,f\neq g\,\mid
f=ite(\phi,g,h)\,\mid\,\phi\vee\phi\,\mid\,\phi\wedge\phi\,\mid\neg\phi$

where $f,g,h\in\mathbb{Z}_{2^{d}}[\bm{x}]$. Informally, the quantifier-free
equational bit-vector theory covers boolean combinations of (in)equations
between polynomials in $\mathbb{Z}_{2^{d}}[\bm{x}]$.

Note that in our grammar there is no distinction between signed and unsigned
bit-vectors since we only consider equalities (i.e., $f=g$) and strict
inequalities (i.e., $f\neq g$) and there are no bit-wise operations (like bit-
or, bit-and, etc).

###  3.1 SMT Solving with Strong Gröbner Bases

Our approach is built upon the framework of DPLL(T) [35, Chapter 11] with
conflict-driven clause learning (CDCL) [9, Chapter 4], which is a technique
widely adopted in modern SMT solvers. The general workflow of DPLL(T) is as
follows. DPLL(T) regards each atomic predicate in the SMT formula $\phi$ as a
propositional variable so that the original SMT formula is transformed into a
propositional formula and partially assigns truth values to these
propositional variables in a back-tracking procedure while checking whether
conflict arises. When a conflict is detected, DPLL(T) tries to learn a new
clause through CDCL to guide the subsequent SMT solving.

A central component of a DPLL(T) solver is the satisfiability checking of a
conjunction of atomic predicates and their negations. In the DPLL(T) solving
of our quantifier-free equational bit-vector theory, the atomic predicates are
equational predicates of the forms $f=g$ (with their negations $f\neq g$).
Therefore, the aforementioned central component corresponds to the
satisfiability checking of a system of polynomial (in)equations modulo $2^{d}$
for bit-vectors.

We solve the satisfiability of a system of polynomial (in)equations modulo
$2^{d}$ via strong Gröbner bases. The detailed algorithmic steps are as
follows. Below we fix an input finite conjunction $\Phi=\bigwedge_{i}\phi_{i}$
where each $\phi_{i}$ is either an equation $f=g$ or an inequality $f\neq g$
where $f,g\in\mathbb{Z}_{2^{d}}[\bm{x}]$.

$\blacktriangleright$ Step A1: Pre-processing. Our algorithm first operates a
pre-processing that transforms each (in)equation $\phi_{i}$ in the conjunction
$\Phi$ into an equivalent equation of the form $h=0$ for some polynomial $h$
in $\mathbb{Z}_{2^{d}}[\bm{x}]$. If $\phi_{i}$ is an equation $f_{i}=g_{i}$,
then we simply set $h_{i}=f_{i}-g_{i}$. Otherwise, if $\phi_{i}$ is an
inequation $f_{i}\neq g_{i}$, let $h_{i}=z_{i}(f_{i}-g_{i})-2^{d-1}$ where
$z_{i}$ is a fresh variable.

The idea behind introducing the fresh variable $z_{i}$ to handle inequations
is that in the ring $\mathbb{Z}_{2^{d}}$, we have $a\not\equiv 0\mod 2^{d}$ if
and only if $a\cdot b\equiv 2^{d-1}\mod 2^{d}$ for some
$b\in\mathbb{Z}_{2^{d}}$. We then denote the collection of all the $h_{i}$ by
$H$. The following propositions demonstrate the correctness of the pre-
processing. The proofs of Proposition 5 and Proposition 6 are deferred to
Appendix A.1 and Appendix A.2.

######  Proposition 5.

Given $a\in\mathbb{Z}_{2^{d}}\setminus\\{0\\}$ with $\nu_{2}(a)=\alpha$, then
there exists an integer $b\in\mathbb{Z}_{2^{d}}$ such that $ab=2^{\alpha}$.
Especially, if $\alpha=0$, $b$ is unique.

######  Proposition 6.

$\Phi$ is satisfiable if and only if $\mathcal{V}(H)$ is non-empty.

After the preprocessing, our algorithm constructs a finite set of polynomials
$H$. According to the above proposition, to check whether $\Phi$ is
satisfiable, it suffices to examine the emptiness of $\mathcal{V}(H)$. We
present this in the next step.

$\blacktriangleright$ Step A2: Emptiness checking of $\mathcal{V}(H)$. In the
previous step, we have reduced the satisfiability of the original SMT formula
$\Phi$ into the existence of a common root of the polynomials in $H$ modulo
$2^{d}$. Our strategy is first to try witnessing the emptiness of
$\mathcal{V}(H)$ via strong Gröbner bases for the ideal $\left\langle
H\right\rangle$, and then resort to the root-finding of polynomials if the
witnessing fails. The witnessing through strong Gröbner bases has the
potential to determine the unsatisfiability of $\Phi$ quickly and, therefore,
can speed up the overall SMT solving.

By the definition of ideals, one has that $\mathcal{V}(H)$ is empty if there
is some nonzero element $c\in\mathbb{Z}_{2^{d}}$ in $\left\langle
H\right\rangle$. This is given by the following proposition.

######  Proposition 7.

If there exists a nonzero $c\in\mathbb{Z}_{2^{d}}$ in $\left\langle
H\right\rangle$, then $\mathcal{V}(H)=\emptyset$.

The above proposition suggests that to witness the emptiness of
$\mathcal{V}(H)$, it suffices to find a nonzero constant
$c\in\mathbb{Z}_{2^{d}}$ in the ideal $\left\langle H\right\rangle$. The
following theorem establishes a connection between the existence of such
constant in the ideal $\left\langle H\right\rangle$ and the strong Gröbner
basis for the ideal.

######  Theorem 8.

There exists a constant nonzero polynomial $f\in\mathbb{Z}_{2^{d}}$ in
$\left\langle H\right\rangle$ if and only if for any strong Gröbner basis $G$
for the ideal $\left\langle H\right\rangle$, $G$ contains some nonzero
constant $g\in\mathbb{Z}_{2^{d}}$.

###### Proof.

According to the definition of the strong Gröbner bases, for any polynomial
$f$, $f\in\left\langle H\right\rangle$ if and only if
$f\twoheadrightarrow_{G}^{*}0$. It implies there exists a polynomial $g\in G$,
a monomial $m\in M_{R}[\bm{x}]$ and a coefficient $c\in\mathbb{Z}_{2^{n}}$
such that $\textsf{lt}(f)=cm\cdot\textsf{lt}(g)$. If $\deg(f)=0$, then
$\textsf{lt}(f)$ is $f$ itself. In addition, since
$\bm{x}^{\textbf{0}}=\textsf{lm}(f)=m\cdot\textsf{lm}(g)$, we have
$m=\textsf{lm}(g)=\bm{x}^{\textbf{0}}$. Thus, according to the property of
well-ordered ordering, $g$ is also a constant polynomial. Since $f\neq 0$, $g$
is also a nonzero constant polynomial. Conversely, if there is a nonzero
constant within $G$, it certainly implies that there exists a nonzero constant
in $\left\langle H\right\rangle$. ∎

By Theorem 8, we reduce the witness of a nonzero constant polynomial in the
ideal to that in a strong Gröbner basis. Thus, our algorithm computes a strong
Gröbner basis for the ideal $\left\langle H\right\rangle$ to witness the
emptiness of $\mathcal{V}(H)$ and the unsatisfiability of the original
conjunction $\Phi$. If the witnessing fails, our algorithm resorts to existing
computer algebra methods to check the emptiness of $\mathcal{V}(H)$.

In Algorithm 1, we implement the original algorithm in [39] to compute a
strong Gröbner basis $GB(H)$ of the ideal $\left\langle H\right\rangle$. The
basic idea is to iteratively construct new polynomials from existing ones $f$
derived from $H$ and add them to the candidate bases $G$ until convergence.
Before describing this algorithm, we first introduce two key concepts used to
construct new polynomials, namely _S-polynomials_ and _A-polynomials_ , which
are defined as follows. Both provide approaches to constructing new
polynomials from original polynomials of $G$.

######  Definition 9 (S-polynomials [39]).

Given two distinct polynomials $f_{1},f_{2}\in R[\bm{x}]\setminus\\{0\\}$, a
polynomial in form of $c_{1}m_{1}f_{1}-c_{2}m_{2}f_{2}$ where $c_{1},c_{2}\in
R$ is called a _S-polynomial_ , if
$c_{1}\textsf{lc}(f_{1})=c_{2}\textsf{lc}(f_{2})$ is a least common multiple
of $\textsf{lc}(f_{1})$ and $\textsf{lc}(f_{2})$, and
$m_{i}=\mathrm{lcm}(\textsf{lm}(f_{1}),\textsf{lm}(f_{2}))/\textsf{lm}(f_{i})\in
M_{R}[\bm{x}]$, where $\mathrm{lcm}(\textsf{lm}(f_{1}),\textsf{lm}(f_{2}))$ is
the least multiple of $\textsf{lm}(f_{1})$ and $\textsf{lm}(f_{2})$. We denote
the set of S-polynomials of $f_{1}$ and $f_{2}$ by
$\mathrm{Spoly}(f_{1},f_{2})$.

######  Definition 10 (A-polynomials [39]).

Given $f\in R[\bm{x}]\setminus\\{0\\}$, an _A-polynomial_ of $f$ is any
polynomial in form of $a\cdot f$, where $\left\langle
a\right\rangle_{R}=\mathrm{Ann}(\textsf{lc}(f))$ and
$\mathrm{Ann}(x):=\\{a:ax=0\\}$. We denote the set of A-polynomials of $f$ by
$\mathrm{Apoly}(f)$.

Besides, a new polynomial can also be generated by iteratively reducing $f$
with respect to the polynomials in $G$ until a remainder $h$ is obtained,
which is irreducible. The remainder $h$ is defined as the _normal form of $f$
with respect to $G$_ and denoted by $\mathrm{NF}(f\ |\ G)$. It can be verified
that $f\twoheadrightarrow_{G}^{*}\mathrm{NF}(f\ |\ G)$, and if $G$ is a
Gröbner basis of $\left\langle H\right\rangle$, $f\in\left\langle
H\right\rangle$ if and only $\mathrm{NF}(f\ |\ G)=0$.

Algorithm 1 Finding a strong Gröbner basis of $\left\langle H\right\rangle$

1:$G\leftarrow H$ and $C\leftarrow H$

2:$P\leftarrow\\{(f_{1},f_{2})\ :\ f_{1}\neq f_{2}\in H\\}$

3:while $P\neq\varnothing$ or $C\neq\varnothing$ do

4: $h\leftarrow 0$

5: if $C\neq\varnothing$ then

6: Pop a polynomial $f_{1}$ from $C$

7: $h\leftarrow\textsf{apoly}\left(f_{1}\right)$

8: else

9: Pop a pair $(f_{1},f_{2})$ from $P$

10: $h\leftarrow\textsf{spoly}\left(f_{1},f_{2}\right)$

11: Compute $g\leftarrow\mathrm{NF}(h\ |\ G)$

12: if $g\neq 0$ then

13: $P\leftarrow P\cup\\{(g,f):f\in G\\}$

14: $C\leftarrow C\cup\\{g\\},G\leftarrow G\cup\\{g\\}$ return $G$

1:$f,G$

2:$\mathrm{NF}(f\ |\ G)$

3:function $\mathrm{NF}(f\ |\ G)$

4: while there exists a $g\in G$ and a term $t=c_{t}\cdot m_{t}$ of $f$, s.t.,
$\nu_{2}(\textsf{lc}(g))\leq\nu_{2}(c_{t})$ and $\textsf{lm}(g)\ |\ m_{t}$ do

5: $f\leftarrow f-\frac{t}{\textsf{lt}(g)}\cdot g$ return $f$

Below, we are ready to give a brief description of Algorithm 1. Given a set of
polynomials $H$ as input, it initializes the candidate polynomials as $G=H$.
Meanwhile, it sets $C=H$ as the set of polynomials required to compute their
A-polynomials and $P$ as the set of pairs required to compute S-polynomials.
When the set $C$ is non-empty, it pops a polynomial $f\in C$ and computes one
of its A-polynomials $h$ (Line 7). If its normal form $g=\mathrm{NF}(h\ |\
G)\neq 0$, it appends $g$ into $G$ of candidate Gröbner basis. Besides, it
updates $P$ and $C$ through building new pairs $\\{(g,f):g\in G\\}$ and
appending $g$ to $C$ (Line 13,14). When $C$ is empty, it pops a pair
$(f_{1},f_{2})$ from $P$ and computes its S-polynomial $h$ (Line 10). When the
normal form of $h$ is non-zero, we do the same operation as above. In
particular, we instantiate the A-polynomial and S-polynomial selected on Line
7 and Line 10 by $\textsf{apoly}\left(f_{1}\right)$ and
$\textsf{spoly}\left(f_{1},f_{2}\right)$, whose definitions are as follows.

$\displaystyle\textsf{apoly}(f_{1}):=2^{d-k_{1}}\cdot f_{1},$
$\displaystyle\textsf{spoly}(f_{1},f_{2}):=2^{d-k_{1}}\cdot
s_{2}\cdot\bm{x}^{\bm{\alpha}-\bm{\alpha_{1}}}\cdot f_{1}-2^{d-k_{2}}\cdot
s_{1}\cdot\bm{x}^{\bm{\alpha}-\bm{\alpha_{2}}}\cdot f_{2},$

where
$\bm{x}^{\alpha_{i}}=\textsf{lm}(f_{i}),\bm{x}^{\alpha}=\mathrm{lcm}(\bm{x}^{\bm{\alpha_{1}}},\bm{x}^{\bm{\alpha_{2}}}),k_{i}=\nu_{2}(\textsf{lc}(f_{i}))$
and $\textsf{lc}(f_{i})=2^{k_{i}}\cdot s_{i}$. The correctness of Algorithm 1
is given in Theorem 11, with proof in Appendix A.3.

Algorithm 2 Finding common roots of a Gröbner basis.

1:function $FindZeros(H,\mathcal{M})$

2: $G\leftarrow GB(H)$

3: if there exists some constant in $G$ then return $\perp$

4: if $\left|\mathcal{M}\right|=n$ then return $\mathcal{M}$

5: if there exists an univariate polynomial $p\in\mathbb{Z}_{2^{n}}[x]$ then

6: if $Zeros(p)=\emptyset$ then return $\perp$

7: for $z\in Zeros(p)$ do $\triangleright$Traverse zeros of a univariate
polynomial

8: $r\leftarrow FindZeros(G\cup\\{x-z\\},\mathcal{M}\cup\\{x\mapsto z\\})$

9: if $r\neq\perp$ then return $r$

10: else if there exists a polynomial $p$ can be decomposed as $p=f\cdot g$
then

11: for $i=0,\ldots,d-1$ do $\triangleright$Factorize $p$ over $\mathbb{Z}$

12: $r\leftarrow FindZeros(G\cup\\{2^{i}\cdot f,2^{d-i}\cdot
g\\}\setminus\\{p\\},\mathcal{M})$

13: if $r\neq\perp$ then return $r$

14: else

15: Arbitrarily select a variable $x\notin\mathcal{M}$
$\triangleright$Exhaustive search

16: for $z=0,\ldots,2^{d}-1$ do

17: $r\leftarrow FindZeros(G\cup\\{x-z\\},\mathcal{M}\cup\\{x\mapsto z\\})$

18: if $r\neq\perp$ then return $r$

19: return $\perp$

######  Theorem 11.

For any finite set $H\subseteq\mathbb{Z}_{2^{d}}[x_{1},\ldots,x_{n}]$,
Algorithm 1 always returns a strong Gröbner basis of $\left\langle
H\right\rangle$ in finite time.

$\blacktriangleright$ Step A3: Guarantee on completeness. As previously
discussed, we have presented a sound procedure for determining whether
$\mathcal{V}(H)$ is empty. However, there may be cases where $\mathcal{V}(H)$
is empty despite passing the aforementioned check. To address this issue, we
have developed a complete procedure that utilizes a backtracking strategy to
identify solutions.

Similar to the complete decision procedure of [40], we maintain two data
structures: $G$, a Gröbner basis and
$\mathcal{M}:V\rightarrow\mathbb{Z}_{2^{n}}$, a (partial) map from variables
to elements of ring $\mathbb{Z}_{2^{n}}$. Algorithm 2 presents the _FindZeros_
procedure for finding solutions. $G$ is first initialised to $GB(H)$ and
$\mathcal{M}$ is initialised to an empty map.

We say a polynomial $p$ is _unvariate_ if $p$ only contains one variable not
assigned a value in $\mathcal{M}$. If $G$ contains a univariate polynomial $p$
with only one variable $x$ that is not assigned a value, we compute the zeros
of $p$ over $\mathbb{Z}_{2^{n}}$ (denoted by $Zeros(p)$). Then, we traverse
each root $z\in Zeros(p)$ and iteratively assign $x$ as $z$. For each
assignment, we recursively check whether the updated Gröbner basis has a
solution. If each polynomial has more than two variables not assigned, we
attempt to decompose a polynomial $p\in G$ into $p=f\cdot g$ through
factorization over $\mathbb{Z}$. Since $p=0\ (\mathrm{mod}\ 2^{d})$ is
equivalent to $f=0\ (\mathrm{mod}\ 2^{d-i})$ and $g=0\ (\mathrm{mod}\ 2^{i})$
for some $0\leq i\leq d$, we enumerate $i$ and recursively search for
solutions by appending $f\cdot 2^{i}$ and $g\cdot 2^{d-i}$ into the Gröbner
basis. When neither of the two conditions mentioned above are met, we then
perform an exhaustive search until a solution is found. The soundness of the
complete decision procedure is given by Theorem 12, whose proof is deferred to
Appendix A.4.

######  Theorem 12.

Algorithm 2 always terminates and returns an element of $\mathcal{V}(H)$ if
$\mathcal{V}(H)\neq\emptyset$. Otherwise, it returns $\perp$.

###  3.2 Algorithmic Improvement for Multiplicative Inverse

In the computation of a strong Gröbner basis, a key bottleneck is the division
operation (Line 5 of NF in Algorithm 1). Given two integers
$a,b\in\mathbb{Z}_{2^{n}}$, let $a=2^{\nu_{2}(a)}\cdot s_{a}$ and
$b=2^{\nu_{2}(b)}\cdot s_{b}$, where $s_{a},s_{b}$ are both odd integers.
According to Proposition 5, there exists an unique integer $t$ such that
$t\cdot s_{b}=1\ (\mathrm{mod}\ 2^{d})$. We denote $t$ by $s_{b}^{-1}$ and
implement the division operation as
$\frac{a}{b}=2^{\nu_{2}(a)-\nu_{2}(b)}\cdot s_{a}\cdot s_{b}^{-1}$.

There are various ways to calculate the inverse of an odd integer $a$ in
$\mathbb{Z}_{2^{d}}$. A simple method is via the classical extended Euclidean
algorithm [50, Chapter 2] that finds integer coefficients $k_{1},k_{2}$ such
that $k_{1}\cdot a+k_{2}\cdot{2^{d}}=1$. The extended Euclidean algorithm
requires $O(d)$ arithmetic operations. A significant improvement is via
Hensel’s lifting [34] that requires only $O(\log d)$ arithmetic operations.
Let $a=2^{s}\cdot a^{\prime}+1$, where $a^{\prime}$ is an odd integer.
Prominent implementations of Hensel’s lifting include Arazi and Qi’s algorithm
[3] (that requires $13\lfloor\log d\rfloor+1$ arithmetic operations) and
Dumma’s algorithm [22] (that requires $5\lfloor\log(\frac{d}{s})\rfloor+2$
arithmetic operations). They adopt constructive methods through recursive
formulas. In particular, Dumma’s algorithm calculates the inverse of $a$
through iteratively calculating $(2-a)\prod_{i=1}^{n-1}(1+(a-1)^{2^{i}})$.

A limitation of methods using Hensel’s lifting is constructing the inverse
from scratch, even if $a$ is small. For example, when $a=3$, Dumma’s algorithm
will iteratively calculate $-\prod_{i=1}^{n-1}(1+2^{2^{i}})$ while $3^{-1}$
could be simply given by $\frac{2^{d+1}+1}{3}$. The cost of construction will
be non-negligible when $2^{d}$ is extremely large.

Algorithm 3 Finding the multiplicative inverse of $a$ over
$\mathbb{Z}_{2^{d}}$ when $a$ is small.

1:$r\leftarrow 2^{d}\mod a$

2:Implement $f\leftarrow\frac{2^{d}-r}{a}$ by $f\leftarrow(\frac{1}{a})\gg d$

3:Apply extended Euclidean algorithm to find $k_{1},k_{2}$, such that
$k_{1}\cdot r+k_{2}\cdot a=-1$

4:return $(k_{1}\cdot f-k_{2})\mod 2^{d}$

To improve this, our observation is that the arithmetic operations over
$\mathbb{Z}_{a}$ will be cheaper when $a$ is small compared to $2^{d}$. Since
finding the multiplicative inverse of $a$ is equivalent to finding $k$ such
that $\frac{k\cdot 2^{d}+1}{a}$ is an integer, it could be achieved by finding
the inverse of $2^{d}$ over $\mathbb{Z}_{a}$.

Based on this insight, we adopt Algorithm 3 to find the inverse of $a$ when
$a$ is small. Its detailed description is deferred to Appendix A.5. Here we
present a high-level description. First, it computes the remainder of $2^{d}$
modulo $a$, which can be implemented by the modular exponentiation algorithm
[46]. Then, we use Newton’s method and a shifting operation to calculate the
result of $a$ dividing $2^{d}-r$. Next, we invoke the extended Euclidean
algorithm to find integer $k_{1},k_{2}$ such that $k_{1}\cdot r+k_{2}\cdot
a=-1$. Finally, we return $k_{1}\cdot f-k_{2}$ as the inverse of $a$, whose
correctness is given by

$a\cdot(k_{1}\cdot f-k_{2})=k_{1}\left(2^{d}-r\right)-k_{2}\cdot a\equiv 1\
(\mathrm{mod}\ 2^{d})\,.$

It can observed that most arithmetic operations (Line 1 and 3) in Algorithm 3
are over $\mathbb{Z}_{a}$. Hence, when $a$ is small compared to $2^{d}$, the
number of binary operations over $\mathbb{Z}_{a}$ will also be small compared
to that over $\mathbb{Z}_{2^{d}}$. Assume the classical multiplication costs
$\mathcal{O}(2d^{2})$ binary operations. A division operation $\frac{b}{a}$
could be implemented by pre-computing $\frac{1}{a}$ and then performing one
multiplication $b\cdot(\frac{1}{a})$ as [26]. Formally, we provide the
following lemma, which estimates the number of arithmetic and binary
operations. Notably, our method outperforms those of [3, 22] when $a$ is much
smaller than $2^{d}$. Its proof is deferred to Appendix A.5.

######  Theorem 13.

Algorithm 3 requires $\mathcal{O}\left(2\log d+8\log a\right)$ arithmetic
operations and $\mathcal{O}(2d^{2}+4d+8a^{2}\cdot\log a+4a\cdot\log a)$ binary
operations.

##  4 Loop Invariant Generation

In this section, we introduce a novel approach for generating polynomial
equational invariants over bit-vectors. Invariant generation aims at solving
predicates that over-approximate the set of reachable program states and can
be viewed as an important case of quantified SMT solving [53]. We solve the
invariant by parametrically reducing a polynomial invariant template with
unknown coefficients with respect to the strong Gröbner basis of transitions.
Below we first present the invariant generation problem and the connection
with SMT. Then we present the details of our approach.

###  4.1 Inductive Loop Invariants

We consider polynomial while loops in which addition and multiplication are
considered modulo $2^{d}$ where $d$ is the size of a bit-vector. Fix a finite
set $V=\\{x_{1},\dots,x_{n}\\}$ of program variables and let
$V=\\{x^{\prime}\mid x\in V\\}$ be the set of primed variables of $V$. A
program variable $x$ in $V$ is used to represent the current value of the
variable, while its primed counterpart $x^{\prime}\in V^{\prime}$ is to
represent the next value of the variable $x$ after the current loop iteration.
An _equational polynomial assertion_ is a conjunction of polynomial equations
over variables in $V,V^{\prime}$, i.e., a formula of the form
$\bigwedge_{i}p_{i}(x_{1},x_{1}^{\prime},\dots,x_{n},x^{\prime}_{n})=0$ where
each $p_{i}$ is a polynomial with variables from $V,V^{\prime}$. More
generally, a _polynomial assertion_ includes polynomial inequalities, i.e.,
$\bigwedge_{i}p_{i}(x_{1},x_{1}^{\prime},\dots,x_{n},x^{\prime}_{n})\Join
q_{i}(x_{1},x_{1}^{\prime},\dots,x_{n},x^{\prime}_{n})$, where
$\Join\in\\{=,\neq,\leq,\geq,>,<\\}$ and $p_{i},q_{i}$ are polynomials with
variables from $V,V^{\prime}$.

We say that a polynomial assertion is in $V$ if it only involves variables
from $V$ and in $V,V^{\prime}$ generally. A polynomial while loop takes the
form

$\textbf{assume}\
\theta(V);\,\textbf{while}\,(c(V))\,\\{\rho(V,V^{\prime});\\};\textbf{assert}(\kappa(V))$
(1)

where (a) $\theta(V)$ is a polynomial assertion in $V$ and specifies the
initial condition (or precondition) for program inputs, (b) $c(V)$ is a
polynomial assertion in $V$ and acts as the loop condition, (c)
$\rho(V,V^{\prime})$ is an equational polynomial assertion in $V,V^{\prime}$
that specifies the relationship between the current values of $V$ and the next
values of $V^{\prime}$, and (d) $\kappa(V)$ is a polynomial assertion in $V$
that acts as the postcondition at the termination of the loop.

A _program state_ is a function $\bm{v}:V\rightarrow\mathbb{Z}_{2^{d}}$ that
specifies the current value $\bm{v}(x)$ for every variable $x\in V$, while a
_primed state_ is a function
$\bm{v}^{\prime}:V^{\prime}\rightarrow\mathbb{Z}_{2^{d}}$ that specifies the
next value $\bm{v}^{\prime}(x^{\prime})$ of each variable $x$ after one loop
iteration. Given a program state $\bm{v}$ and a polynomial assertion $\phi$ in
$V$, we write $\bm{v}\models\phi$ if $\phi$ is true when each variable $x\in
V$ is instantiated by its current value $\bm{v}(x)$ in $\phi$. Moreover, given
a program state $\bm{v}$, a primed state $\bm{v}^{\prime}$ and a polynomial
assertion $\phi$ in $V,V^{\prime}$, we write
$\bm{v},\bm{v}^{\prime}\models\phi$ if $\phi$ is true when instantiating each
variable $x\in V$ with the value $\bm{v}(x)$ and each variable $x^{\prime}\in
V$ with the value $\bm{v}^{\prime}(x^{\prime})$ in $\phi$.

The semantics of a polynomial while loop in the form of (1) is given by its
(finite) executions. A (finite) _execution_ of the loop is a finite sequence
$\bm{v}_{0},\bm{v}_{1},\dots,\bm{v}_{n}$ of program states such that
$\bm{v}_{0}\models\theta(V)$ and for every $0\leq k<n$ we have
$\bm{v}_{k},\bm{v}^{\prime}_{k+1}\models\rho(V,V^{\prime})$, where the primed
state $\bm{v}^{\prime}_{k+1}$ is defined by
$\bm{v}^{\prime}_{k+1}(x^{\prime}):=\bm{v}_{k+1}(x)$ for each $x\in V$. A
program state $\bm{v}$ is _reachable_ if it appears in some execution of the
loop. We consider polynomial invariants, which are equational polynomial
assertions $\phi$ in $V$ such that for all reachable program states $\bm{v}$,
we have $\bm{v}\models\phi$.

In this work, we consider inductive polynomial invariants that are inductive
invariants in the form of polynomial equations. An _inductive polynomial
invariant_ for a polynomial while loop in the form of (1) is an equational
polynomial assertion $\phi$ in $V$ that satisfies the initiation and
consecution conditions as follows:

  * •

(Initiation) for any program state $\bm{v}$, $\bm{v}\models\theta(V)$ implies
$\bm{v}\models\phi$.

  * •

(Consecution) for any program state $\bm{v}$ and primed state
$\bm{v}^{\prime}$, we have that

$\left[(\bm{v}\models
c(V)\wedge\phi)\wedge(\bm{v},\bm{v}^{\prime}\models\rho(V,V^{\prime}))\right]\Rightarrow\bm{v}^{\prime}\models\phi[x^{\prime}_{1}/x_{1},\dots,x^{\prime}_{n}/x_{n}].$

By a straightforward induction on the length of an execution, one easily
observes that every inductive polynomial invariant is an invariant that over-
approximates the set of reachable program states of a polynomial while loop.
An inductive polynomial invariant $\phi$ _verifies_ the post condition
$\kappa(V)$ if for all program states $\bm{v}\models\phi$, we have that
$\bm{v}\models\kappa(V)$. Moreover, the invariant $\phi$ _refutes_ the post
condition if $\phi\wedge\kappa(V)$ is unsatisfiable.

We consider the automated synthesis of inductive polynomial invariants: given
an input polynomial while loop in the form of (1), generate an inductive
polynomial invariant for the loop that suffices to verify the postcondition of
the loop. The problem is a special case of SMT solving in the CHC (constraint
Horn clauses) form [10]. The corresponding CHC constraints are as follows:

Initiation: $\displaystyle\,\theta(V)\Rightarrow\phi$ Consecution:
$\displaystyle\,\left[(c(V)\wedge\phi)\wedge\rho(V,V^{\prime})\right]\Rightarrow\phi[x^{\prime}_{1}/x_{1},\dots,x^{\prime}_{n}/x_{n}]$
Verification: $\displaystyle\,(\phi\wedge\neg
c(V))\Rightarrow\kappa(V)\enskip\enskip\textbf{Refutation:}\,(\phi\wedge\neg
c(V))\Rightarrow\neg\kappa(V)$ (2)

where the task is to solve a formula $\phi$ that fulfills the constraints
above, for which we use the verification condition to verify the postcondition
and the refutation condition to refute the postcondition. One directly
observes that any solution of $\phi$ w.r.t the CHC constraints is an inductive
polynomial invariant for the loop.

######  Example 1.

Consider the following program, where $x,y$ are two $32$-bit unsigned integers
and initialized as $1$ and $9$, respectively, and incremented by $1$ in each
iteration. We want to verify that $y-x<10$ when the loop program terminates.
According to the definition of polynomial inductive loop invariant, the value
of $y-x$ is fixed during the loop. Since its value is initialized as $8$,
$y-x=8\ (\mathrm{mod}\ 2^{32})$ is a polynomial loop invariant. Further, since
$(y=0)\wedge(y-x=8\ (\mathrm{mod}\ 2^{32}))$ implies $y-x<10$, the
postcondition is satisfied.

    x = 1, y = 9;
    while (y != 0) {
        x = x + 1;
        y = y + 1;
    }
    @assert(y - x < 10);

$\xrightarrow{\begin{subarray}{c}\text{Embed into}\\\ \text{quantified
formulas}\end{subarray}}$ $\displaystyle\textbf{assert}(\forall x,y.(x=1\wedge
y=9)\rightarrow inv(x,y))$ $\displaystyle\textbf{assert}(\forall
x,y,x^{\prime},y^{\prime}.(y\neq 0\wedge inv(x,y))\rightarrow$
$\displaystyle\qquad(x^{\prime}=x+1)\wedge(y^{\prime}=y+1)\wedge
inv(x^{\prime},y^{\prime}))$ $\displaystyle\textbf{assert}(\forall
x,y.(inv(x,y)\wedge(y=0))\rightarrow(y-x<10))$

###  4.2 Polynomial Invariants Generation over Bit-Vectors

Below we present our approach for synthesizing polynomial equational loop
invariants over bit-vectors. The high-level idea is first to have a polynomial
template with unknown coefficients as parameters, then to establish linear
congruence equations for these unknown coefficients via strong Gröbner bases,
and finally to solve the linear congruence equations to get polynomial
invariants.

Let $P$ be an input polynomial while loop in the form of (1) and $d$ be the
size of bit-vectors. Let $k$ be an extra algorithmic input that specifies the
maximum degree of the target polynomial invariant and $M^{(k)}[V]$ be the set
of all monomials in $V$ with degree $\leq k$. Our approach is divided into
three steps as follows.

$\blacktriangleright$ Step B1: Polynomial templates. Our approach first sets
up a polynomial template $\eta=0$ for the desired invariant, where $\eta$ is
the polynomial $\textstyle\eta=\sum_{q\in{M^{(k)}}[V]}\lambda_{q}\cdot q$ with
the unknown coefficients $\lambda_{q}$ for every monomial $q\in M^{(k)}[V]$.
In particular, the coefficient of $q=\bm{x}^{\bm{0}}$ is also denoted as
$\xi$. For example, when $V=\\{x,y\\}$, and $k=2$, template $\eta$ contains
monomials with degree $\leq 2$, i.e., $\eta=\lambda_{1}\cdot
x^{2}+\lambda_{2}\cdot xy+\lambda_{3}\cdot y^{2}+\lambda_{4}\cdot
x+\lambda_{5}\cdot y+\xi$. Denote $\bm{\lambda}$ as the vector of all these
coefficients. Note that the template enumerates all monomials with degrees no
more than $k$. We denote
$\eta^{\prime}:=\eta[x^{\prime}_{1}/x_{1},\dots,x^{\prime}_{n}/x_{n}]$. We
obtain the following constraints, which specify that the template is an
invariant:

Initiation: $\displaystyle\,\theta(V)\Rightarrow\left(\eta=0\right)$
Consecution:
$\displaystyle\,\left[c(V)\wedge(\eta=0)\wedge\rho(V,V^{\prime})\right]\Rightarrow(\eta^{\prime}=0)$
(3)

$\blacktriangleright$ Step B2: Reduction of strong Gröbner bases. Then, our
approach derives a system of linear congruence equations for the unknown
coefficients in the template with respect to the constraints in (4.2). To
derive a sound and complete characterization for the unknown coefficients is
intractable as it requires multivariate nonlinear reasoning of integers with
modular arithmetics. Henceforth, we resort to incomplete sound conditions. We
derive sound conditions from the proposition below, whose correctness follows
directly from the definition of ideals.

######  Proposition 14.

Let $F_{\rho}$ be the set of left-hand-side polynomials of assertion
$\rho(V,V^{\prime})$. The consecution condition
$\left[c(V)\wedge(\eta=0)\wedge\rho(V,V^{\prime})\right]\Rightarrow(\eta^{\prime}=0)$
holds if $\eta^{\prime}-\mu\cdot\eta\in\left\langle F_{\rho}\right\rangle$ for
some constant $\mu\in\mathbb{Z}_{2^{d}}$.

Proposition 14 provides the sound condition
$\exists\mu\in\mathbb{Z}_{2^{d}}.(\eta^{\prime}-\mu\cdot\eta\in\left\langle
F_{\rho}\right\rangle)$ for the consecution condition in (4.2). We employ
several heuristics to further simplify the condition. The first heuristics is
to enumerate small values of $\mu$ (e.g., $\mu\in\\{-1,0,1\\}$) that reflect
common patterns in invariant generation. For example, the case $\mu=0$
corresponds to _local_ invariants, and $\mu=1$ corresponds to _incremental_
invariants (see [44, 45] for details). Then, the condition is soundly reduced
to checking $\eta^{\prime}-\mu\cdot\eta\in\left\langle F_{\rho}\right\rangle$
for specific values of $\mu$.

To check whether $\eta^{\prime}-\mu\cdot\eta\in\left\langle
F_{\rho}\right\rangle$ or not, a direct method is to reduce the polynomial
$\eta^{\prime}-\mu\cdot\eta$ with respect to the strong Gröbner basis of the
ideal $\left\langle F_{\rho}\right\rangle$. However, this would cause the
combinatorial explosion as one needs to maintain the information of the
unknown coefficients from the template in the reduction of strong Gröbner
bases, which is already the case in the simpler situation of real numbers
(that constitute a field and do not involve modular arithmetics) [44].
Therefore, we consider heuristics via a normal-form reduction as follows.

Parametric Normal Form. Below we define an operation $\mathrm{PNF}$ of
parametric normal form for reducing a polynomial $f$ whose coefficients are
polynomials in the unknown coefficients of our template against a finite
subset of $\mathbb{Z}_{2^{d}}[V]$.

######  Definition 15 (Parametric Normal Form).

Let $\mathcal{L}=\mathbb{Z}_{2^{d}}[\bm{\lambda}]$,
$\mathcal{F}=\mathcal{L}[V]$ and $\mathcal{G}$ be the set of finite subsets of
$\mathbb{Z}_{2^{d}}[V]$. A map
$\mathrm{PNF}:\mathcal{F}\times\mathcal{G}\rightarrow\mathcal{F},(f,G)\mapsto\mathrm{PNF}(f\
|\ G)$ is called a _parametric normal form_ if for any $f\in\mathcal{F}$ and
$G\in\mathcal{G}$,

  1. 1.

$\mathrm{PNF}(0\ |\ G)=0$,

  2. 2.

$\mathrm{PNF}(f\ |\ G)\neq 0$ implies $\textsf{lt}(\mathrm{PNF}(f\ |\
G))\notin\left\langle\\{\textsf{lt}(g)\\}\right\rangle_{\mathcal{L}[V]}$ for
any $g\in G$, and

  3. 3.

$r:=f-\mathrm{PNF}(f\ |\ G)$ belongs to $\left\langle
G\right\rangle_{\mathcal{L}[V]}$.

In Algorithm 4 (deferred to Appendix B.1), we show an instance of parametric
normal form and its calculation. Similar to Algorithm 1, at each time we
attempt to find polynomial $g\in G$ satisfying its leading monomial divides
the monomial of a term $t=c_{t}\cdot m_{t}$ of $f$. A difference is that
$c_{t}$ is no longer a constant and includes unknown parameters of
$\bm{\lambda}$. We consider the coefficients of these parameters. Let
$\bar{\nu}_{2}(c_{t})$ be the minimum exponent of two of the coefficients. For
example, if $c_{t}=2\lambda_{1}+4\lambda_{2}$, then
$\bar{\nu}_{2}(c_{t})=\min(\nu_{2}(2),\nu_{2}(4))=1$. Hence, if
$\bar{\nu}_{2}(c_{t})\geq\nu_{2}(\textsf{lc}(g))$, we scale $g$ and update $f$
by eliminating term $t$. The formal description of the normal form calculation
and its soundness are deferred to Appendix B.1. Below we apply the parametric
normal form to check $\eta^{\prime}-\mu\cdot\eta\in\left\langle
F_{\rho}\right\rangle$ with specific values of $\mu$ in the next proposition,
whose proof is deferred to Appendix B.2.

######  Proposition 16.

For all $\mu\in\mathbb{Z}_{2^{d}}$ and concrete values
$\overline{\bm{\lambda}}$ substituted for $\bm{\lambda}$, if
$\mathrm{PNF}(\eta^{\prime}-\mu\cdot\eta\ |\ GB(F_{\rho}))=0$, then
$\mathrm{NF}(\eta^{\prime}-\mu\cdot\eta\ |\ GB(F_{\rho}))=0$.

######  Example 2.

Let $V=\\{x,y\\}$ and
$\rho(V,V^{\prime})=(x^{\prime}=x+1)\wedge(y^{\prime}=y+x)$ and the degree
$k=2$. Hence, the strong Gröbner basis of $F_{\rho}$ is
$G=\\{x^{\prime}-x-1,y^{\prime}-y-x\\}$. When $\mu$ is set as $1$, the
parametric normal form of $\eta^{\prime}-\mu\cdot\eta$ is shown in the left
part below. According to Proposition 16, to make
$\eta^{\prime}-\mu\cdot\eta\in\left\langle F_{\rho}\right\rangle$, it suffices
to solve the system of linear congruences shown in the right part. $\square$

$\displaystyle\eta\
=\lambda_{1}x^{2}+\lambda_{2}xy+\lambda_{3}y^{2}+\lambda_{4}x+\lambda_{5}y+\xi,$
$\displaystyle\mathrm{PNF}(\eta^{\prime}-\mu\cdot\eta\ |\ G)$
$\displaystyle\quad=(\lambda_{2}+\lambda_{3})\cdot x^{2}+2\lambda_{3}\cdot
xy+$ $\displaystyle\quad\ \ \ (2\lambda_{1}+\lambda_{2}+\lambda_{5})\cdot
x+\lambda_{2}\cdot y+(\lambda_{1}+\lambda_{4})$

$\Rightarrow\quad\left\\{\begin{aligned} &\lambda_{2}+\lambda_{3}=0\\\
&2\lambda_{3}=0\\\ &2\lambda_{1}+\lambda_{2}+\lambda_{5}=0\\\
&\lambda_{2}=0\\\ &\lambda_{1}+\lambda_{4}=0\end{aligned}\right.$

$\blacktriangleright$ Step B3. Finding values of parameters. It can be
verified that each coefficient of the returned value of Algorithm 4 is a
linear polynomial of variables of $\\{\lambda_{q}\\}_{q\in M^{(k)}[V]}$. Thus,
the normal form computation results in a system of linear congruences modulo
$2^{d}$ over $\\{\lambda_{q}\\}_{q\in M^{(k)}[V]}$, for which a succinct
representation of the set of solutions can be computed efficiently [37]. Each
solution corresponds to a synthesized polynomial invariant. However, to verify
or refute the postcondition, one may need to enumerate the solutions that can
be exponentially many. To avoid the explicit enumeration, we take the strategy
of first finding a specific solution $\bm{\lambda_{0}}$ to the system of
congruences and then solving the congruences over the real number space
$\mathbb{R}$. Let $\mathrm{Null}(\mathbf{A})$ be the nullspace of the
coefficient matrix $\mathbf{A}$ over $\mathbb{R}$. Then, we shift the
nullspace through $\mathrm{Null}(\mathbf{A})+\bm{\lambda_{0}}$ and use them to
synthesize invariants. A detailed description can be found in Appendix B.3.

In this work, we allow the initial condition to have inequalities.
Inequalities cause the problem that the value of the unknown coefficient $\xi$
may not be determined when $\mu=1$. This is because $\xi$ is eliminated in
$\eta^{\prime}-\mu\cdot\eta$, and we may not be able to determine the value of
$\xi$ using the initial condition. To tackle the inequalities, we add a fresh
variable $x_{0}$ for each program variable $x\in V$. Meanwhile, we replace
every variable $x$ by $x_{0}$ in the $\theta(V)$. Then $\xi$ can be expressed
by a polynomial expression in the variables of $\\{x_{0}:x\in V\\}$. For
example, consider Example 1 but we relax the initial condition to
$\theta(V)=(0<x<10)\wedge(0<y<10)$. We observe that it is impossible to give a
concrete value of $\xi$ such that $x-y+\xi=0$ is always guaranteed during the
loop since we do not know their initial values. We introduce two fresh
variables $x_{0},y_{0}$, for the initial values of $x$ and $y$, respectively.
Then we express $\xi$ by $x_{0}-y_{0}$ and add constraints on $x_{0}$ and
$y_{0}$ based on the initial condition, i.e., $0<x_{0},y_{0}<10$.

$\blacktriangleright$ Step B4. Verifying pre- and postconditions. Finally,
with the solved invariant from the previous step, we translate the original
CHC constraints into simpler forms that can be efficiently verified by
existing SMT solvers. We utilize SMT solvers to verify that the initialization
constraint and the verification (or refutation) constraint hold. We provide a
formal description of our transition procedure in Appendix B.4. The overall
soundness is stated in the following theorem.

######  Theorem 17 (Soundness).

If our algorithm outputs satisfiable (or resp. unsatisfiable) results, then
the postcondition in the input is correct (or resp. refuted).

##  5 Implementation and Experimental Results

In this section, we present the experimental evaluation of our SMT-solving
approach. We first describe the detailed implementation of our approach, then
the evaluation of our approach in quantifier-free bit-vector solving, and
finally, polynomial invariant generation. All the experiments are conducted on
a Linux machine with a 16-core Intel 6226R @2.90GHz CPU.

###  5.1 Implementation

Quantifier-free equational bit-vector theory. We implement the computation of
strong Gröbner bases with our improvement for calculating multiplicative
inverse in the SMT solver cvc5 [5]. We use two computer algebra systems,
namely CoCoA-5 [17] and Maple [36]. In detail, we first parse the input
formula in cvc5 format to a polynomial in CoCoA-5, then implement the
computation for strong Gröbner bases (Algorithm 1) in CoCoA-5 to check the
emptiness (Step A2), and finally resort to our complete decision procedure
(Step A3) to find a solution where we use Maple to find the roots of a
univariate polynomial in $\mathbb{Z}_{2^{n}}$.

Polynomial invariant generation. We implement our approach in Python 3.8.10.
Our implementation accepts inputs in the SMT-lib CHC format (4.1) that include
the initial, consecution, and postconditions, generates polynomial invariants
by the algorithm given in Section 4.2 with $\mu$ set as $-1,0,1$, and uses z3
to check whether the postcondition is verified or refuted and whether the
initial condition implies the loop invariant. In the implementation, we invoke
the Python package Diophantine for finding solutions of systems of linear
congruences and Sympy for finding the nullspace of a matrix.

###  5.2 Quantifier-Free Equational Bit-Vector Theory

Table 1: Number of solved and unknown instances of all approaches. Solvers | sat | unsat | unknown | timeout (10 sec) | memout (1 gb) | Solved
---|---|---|---|---|---|---
Bitwuzla | 674 | 354 | 281 | 4 | 1153 | 1028
z3 | 499 | 436 | 281 | 1117 | 133 | 935
cvc5 | 418 | 223 | 281 | 101 | 1443 | 641
MathSAT | 583 | 376 | 0 | 143 | 1364 | 959
cvc5-sgb | 631 | 620 | 0 | 1112 | 103 | 1252
In total |  |  |  |  |  | 2466

(a) Comparison of Time Efficiency

(b) Comparison of Memory Usage

Benchmark setting. We consider the extensive benchmark set in [40] as the
baseline. The benchmarks in [40] are randomly generated quantifier-free
formulas in a finite field $\mathbb{F}_{p}$ modulo a prime number $p$ . We
adapt these benchmarks to QF_BV (quantified-free, bit-vector) formulas as
follows. First, if a variable (or constant) belongs to a finite field
$\mathbb{F}_{p}$ satisfying $2^{d-1}<p<2^{d}$, we then adapt it to a bit-
vector variable with size $d$. Second, the arithmetic operations over
$\mathbb{F}_{p}$ are directly adapted to modular arithmetics over bit-vectors.
The adapted benchmark set includes $2466$ benchmarks in SMT-LIB format and
involves polynomial (in)equations of bit-vectors.

Performance analysis. We compare our methods with four state-of-art bit-vector
solvers (Bitwuzla [38], z3 [20], cvc5 [5] and MathSAT [16]). Bitwuzla uses
bit-blasting, MathSAT uses integer solving, and z3, cvc5 are prominent
comprehensive SMT solvers. We set a time-out limit of $10$ seconds and a
memory-out limit of $1$GB physical memory. Table 1 lists the number of solved
instances of different solvers, where cvc5-sgb is our approach ($\S$3). Our
approach outperforms others in the number of solved instances (approx. $20\%$
more), especially in verifying unsatisfiable instances (approx. $40\%$ more)
due to the use of strong Gröbner bases. It is worth noting that all the
unsatisfiable instances are found by strong Gröbner bases without invoking
Maple. Fig. 1(a) further shows the total time consumption on the solved
instances of all approaches. We observe that our approach has the lowest time
consumption. Moreover, Fig. 1(b) depicts the average memory usage of the
solved instances with different bit-vector sizes ($32,64,256$) by each
approach. Our approach consumes the lowest amount of memory, while the memory
consumption of others increases significantly as the size grows.

###  5.3 Polynomial Invariant Generation

Benchmark setting. We collect invariant generation tasks from three benchmark
sets: 2016.Sygus-Comp [2], 2018.SV-Comp [7] and 2018.CHI-InvGame [11]. We
classify the benchmarks into _lin_ ones that require only linear invariants
and _poly_ ones that require polynomial invariants with degree more than one.
There are in total $39$ linear benchmarks and $19$ poly benchmarks.

Table 2: Performance of Eldarica and our approach on three datasets, where “$\\#$" is the number of benchmarks and the last line shows the averaged performance.  Dataset | Linear | Polynomial
---|---|---
$\\#$ | Time (s) | Mem (mb) | # | Time (s) | Mem (mb)
Eldarica | Our | Eldarica | Our | Eldarica | Our | Eldarica | Our
2016.Sygus-Comp [2] | 23 | 15.0 | 1.3 | 234.1 | 71.6 | 6 | $>70.5$ | 5.5 | $>460.1$ | 71.0
2018.SV-Comp [7] | 16 | 15.0 | 0.9 | 248.0 | 67.6 | 1 | $5.1$ | 0.5 | $179.7$ | 70.6
2018.CHI-InvGame [11] | 0 | - | - | - | - | 12 | $>173.5$ | 7.4 | $>490.3$ | 72.5
Average | 39 | 15.0 | 1.1 | 239.8 | 70.0 | 19 | $>132.1$ | 6.4 | $>464.4$ | 71.9

Performance Analysis. We compare our approach with Eldarica [30], a state-of-
art Horn clause solver that has the best performance in the experimental
evaluation in [53]. We set the time limit to $200$ seconds and the memory
limit to $1$GB. Our approach solves all the benchmarks, while Eldarica times
out over $11$ poly benchmarks. Table 2 shows the average time and memory
consumption over the benchmarks. From the table, we can observe our approach
has substantially better time efficiency and memory consumption, especially
over poly benchmarks. For the polynomial benchmark, our approach has achieved
an average speedup of more than $20$X in terms of time and an average
reduction of more than $7$X in terms of memory. Due to the space constraints,
the detailed performance between Eldarica and our approach over these
benchmarks is relegated to Table 3 and Table 4 in Appendix C, where “$>200$"
indicates that Eldarica times out on the benchmark. It is also worth noting
that for most of these benchmarks, z3 times out, and cvc5 quickly outputs
“unknown”.

##  6 Related Works

Bit-blasting approaches ([35, Chapter 6], [31]) decompose a bit-vector into
the bits constituting it and solve the SMT problem by boolean satisfiability
over these bits. Bit-blasting ignores the algebraic structure behind modular
addition and multiplication and hence cannot utilize them to speed up SMT
solving. Compared with bit blasting, our approach leverages strong Gröbner
base to speed up the SMT solving of equational bit-vector theory.

Integer-solving approaches [28, 32, 25] reduce bit-vector problems to the SMT
solving of integer properties. Although bit-vectors can be viewed as a special
case of integers, nonlinear integer theory is notoriously difficult to solve.
Compared with these approaches, our approach solves the polynomial theory of
bit-vectors via strong Gröbner bases, which are more suitable to characterize
algebraic properties of bit-vectors than general nonlinear integer theory.

The application of Gröbner bases to the equational theory of bit-vectors has
been considered in previous works such as [33, 12, 42]. The Gröbner bases used
in these approaches are either restrictive (such as [33] that uses Gröbner
bases over principal ideal domains) or too general (such as [12, 42] that uses
Gröbner bases over general commutative Noetherian rings). This results in
excessive computation to derive a Gröbner basis. Compared with these results,
our approach uses the strong Gröbner bases that lie between principal ideal
domains and commutative Noetherian rings and avoids the excessive computation
by the succinct strong reduction in computing a strong Gröbner basis. Some
recent work [51, 48] adopts the methods of [12] to compute a Gröbner basis
without the need for solving an integer programming problem each time.
However, we have observed the Gröbner bases used in [51] are equivalent to
strong Gröbner bases presented in [39] while that in [48] is actually a
slightly improved version of the strong Gröbner bases.

It is also worth noting that the work [33] applies Gröbner bases to the
special case of acyclic circuits, the work [12] focuses on the special case of
boolean fields, and the work [48] uses Gröbner bases for bit-sequence
propagation, which solves the SMT problem by alternative methods. In contrast,
our approach completely uses strong Gröbner bases to SMT solving and tackles
invariant generation.

Abstract interpretation [47, 37, 23, 18] has also been considered to generate
polynomial equational invariants over bit-vectors. These approaches rely on
well-established abstract domains and, hence, are orthogonal to our approach.

Gröbner bases have also been applied to finite fields [40] and real numbers
[44, 14, 43]. The work [40] utilizes Gröbner bases to determine the
satisfiability of polynomial (in)equations where coefficients come from a
finite field $\mathbb{F}_{p}$, while the work [43, 44, 14] explores the
generation of real polynomial loop invariants via Gröbner bases. Compared with
these results, our approach is orthogonal as we consider polynomials over
finite rings and use strong Gröbner bases.

##  7 Conclusion and Future Work

We have proposed a novel approach for SMT solving of equational bit-vector
theory via strong Gröbner bases, including the quantifier-free case and the
quantified case of invariant generation. One future work is to optimize our
approach using methods in e.g. [49]. Another direction is to extend our
methods to more bit-vector arithmetics, such as bitwise operations and
inequalities by, e.g., the Rabinowitsch trick [19, Chapter 4.2, Proposition
8],[29]. It is also interesting to incorporate our approach with program
synthesis techniques such as [41].

## References

  * [1] Adams, W.W., Loustaunau, P.: An Introduction to Gröbner Bases. American Mathematical Society (1994). https://doi.org/10.1090/gsm/003
  * [2] Alur, R., Fisman, D., Singh, R., Solar-Lezama, A.: Sygus-COMP 2016: Results and analysis. arXiv preprint arXiv:1611.07627 (2016)
  * [3] Arazi, O., Qi, H.: On calculating multiplicative inverses modulo $2^{m}$. IEEE Transactions on Computers 57(10), 1435–1438 (2008)
  * [4] Artin, M.: Algebra. Prentice Hall (1991)
  * [5] Barbosa, H., Barrett, C., Brain, M., Kremer, G., Lachnitt, H., Mann, M., Mohamed, A., Mohamed, M., Niemetz, A., Nötzli, A., et al.: CVC5: A versatile and industrial-strength SMT solver. In: International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). pp. 415–442. Springer (2022)
  * [6] Barrett, C., Fontaine, P., Tinelli, C.: The SMT-LIB standard (version 2.6). Tech. rep., The University of Iowa (2021)
  * [7] Beyer, D.: Software verification with validation of results: (report on SV-COMP 2017). In: International conference on tools and algorithms for the construction and analysis of systems. pp. 331–349. Springer (2017)
  * [8] Beyer, D., Dangl, M., Wendler, P.: A unifying view on SMT-based software verification. J. Autom. Reason. 60(3), 299–335 (2018). https://doi.org/10.1007/S10817-017-9432-6
  * [9] Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.): Handbook of Satisfiability - Second Edition, Frontiers in Artificial Intelligence and Applications, vol. 336. IOS Press (2021). https://doi.org/10.3233/FAIA336
  * [10] Bjørner, N.S., McMillan, K.L., Rybalchenko, A.: On solving universally quantified horn clauses. In: Logozzo, F., Fähndrich, M. (eds.) Static Analysis - 20th International Symposium, SAS 2013, Seattle, WA, USA, June 20-22, 2013. Proceedings. Lecture Notes in Computer Science, vol. 7935, pp. 105–125. Springer (2013). https://doi.org/10.1007/978-3-642-38856-9_8, https://doi.org/10.1007/978-3-642-38856-9_8
  * [11] Bounov, D., DeRossi, A., Menarini, M., Griswold, W.G., Lerner, S.: Inferring loop invariants through gamification. In: Proceedings of the 2018 CHI Conference on Human Factors in Computing Systems. p. 1–13. CHI ’18, ACM, New York, NY, USA (2018). https://doi.org/10.1145/3173574.3173805
  * [12] Brickenstein, M., Dreyer, A., Greuel, G.M., Wedler, M., Wienand, O.: New developments in the theory of Gröbner bases and applications to formal verification. Journal of Pure and Applied Algebra 213(8), 1612–1635 (2008). https://doi.org/10.1016/J.JPAA.2008.11.043
  * [13] Butson, A., Stewart, B.: Systems of linear congruences. Canadian Journal of Mathematics 7, 358–368 (1955)
  * [14] Cachera, D., Jensen, T., Jobin, A., Kirchner, F.: Inference of polynomial invariants for imperative programs: A farewell to gröbner bases. Science of Computer Programming 93, 89–109 (2014)
  * [15] Chen, H., David, C., Kroening, D., Schrammel, P., Wachter, B.: Bit-precise procedure-modular termination analysis. ACM Trans. Program. Lang. Syst. 40(1), 1:1–1:38 (2018). https://doi.org/10.1145/3121136
  * [16] Cimatti, A., Griggio, A., Schaafsma, B., Sebastiani, R.: The MathSAT5 SMT Solver. In: Piterman, N., Smolka, S. (eds.) Proceedings of TACAS. LNCS, vol. 7795. Springer (2013)
  * [17] CoCoATeam: CoCoA: a system for doi ng Computations in Commutative Algebra. Available at http://cocoa.dima.unige.it
  * [18] Cousot, P., Cousot, R.: Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Graham, R.M., Harrison, M.A., Sethi, R. (eds.) Conference Record of the Fourth ACM Symposium on Principles of Programming Languages. pp. 238–252. ACM (1977). https://doi.org/10.1145/512950.512973
  * [19] Cox, D., Little, J., OShea, D.: Ideals, varieties, and algorithms: an introduction to computational algebraic geometry and commutative algebra. Springer Science & Business Media (2013)
  * [20] De Moura, L., Bjørner, N.: Z3: An efficient SMT solver. In: International conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). pp. 337–340. Springer (2008)
  * [21] Dickson, L.E.: History of the Theory of Numbers, vol. II. Chelsea Publ. Co., New York, diophantine analysis edn. (1920)
  * [22] Dumas, J.G.: On Newton–Raphson iteration for multiplicative inverses modulo prime powers. IEEE Transactions on Computers 63(8), 2106–2109 (2013)
  * [23] Elder, M., Lim, J., Sharma, T., Andersen, T., Reps, T.W.: Abstract domains of affine relations. ACM Trans. Program. Lang. Syst. 36(4), 11:1–11:73 (2014). https://doi.org/10.1145/2651361
  * [24] Fuhs, C., Giesl, J., Middeldorp, A., Schneider-Kamp, P., Thiemann, R., Zankl, H.: SAT solving for termination analysis with polynomial interpretations. In: Marques-Silva, J., Sakallah, K.A. (eds.) Theory and Applications of Satisfiability Testing - SAT 2007, 10th International Conference. Lecture Notes in Computer Science, vol. 4501, pp. 340–354. Springer (2007). https://doi.org/10.1007/978-3-540-72788-0_33
  * [25] Graham-Lengrand, S., Jovanovic, D.: An MCSAT treatment of bit-vectors. In: Brain, M., Hadarean, L. (eds.) Proceedings of the 15th International Workshop on Satisfiability Modulo Theories affiliated with the International Conference on Computer-Aided Verification (CAV 2017). CEUR Workshop Proceedings, vol. 1889, pp. 89–100. CEUR-WS.org (2017), https://ceur-ws.org/Vol-1889/paper8.pdf
  * [26] Granlund, T., Montgomery, P.L.: Division by invariant integers using multiplication. In: Proceedings of the ACM SIGPLAN 1994 conference on Programming language design and implementation. pp. 61–72 (1994)
  * [27] Greuel, G.M., Pfister, G., Bachmann, O., Lossen, C., Schönemann, H.: A Singular introduction to commutative algebra, vol. 348. Springer (2008)
  * [28] Griggio, A.: Effective word-level interpolation for software verification. In: Bjesse, P., Slobodová, A. (eds.) International Conference on Formal Methods in Computer-Aided Design, FMCAD ’11. pp. 28–36. FMCAD Inc. (2011), http://dl.acm.org/citation.cfm?id=2157662
  * [29] Hader, T., Kaufmann, D., Kovács, L.: SMT solving over finite field arithmetic. In: Piskac, R., Voronkov, A. (eds.) LPAR 2023: Proceedings of 24th International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Manizales, Colombia, 4-9th June 2023. EPiC Series in Computing, vol. 94, pp. 238–256. EasyChair (2023). https://doi.org/10.29007/4N6W, https://doi.org/10.29007/4n6w
  * [30] Hojjat, H., Rümmer, P.: The ELDARICA Horn solver. In: 2018 Formal Methods in Computer Aided Design (FMCAD). pp. 1–7 (2018). https://doi.org/10.23919/FMCAD.2018.8603013
  * [31] Jia, F., Han, R., Huang, P., Liu, M., Ma, F., Zhang, J.: Improving bit-blasting for nonlinear integer constraints. In: Just, R., Fraser, G. (eds.) Proceedings of the 32nd ACM SIGSOFT International Symposium on Software Testing and Analysis, ISSTA 2023. pp. 14–25. ACM (2023). https://doi.org/10.1145/3597926.3598034
  * [32] Jovanovic, D.: Solving nonlinear integer arithmetic with MCSAT. In: Bouajjani, A., Monniaux, D. (eds.) Verification, Model Checking, and Abstract Interpretation - 18th International Conference, VMCAI 2017. Lecture Notes in Computer Science, vol. 10145, pp. 330–346. Springer (2017). https://doi.org/10.1007/978-3-319-52234-0_18
  * [33] Kaufmann, D., Biere, A., Kauers, M.: Verifying large multipliers by combining SAT and computer algebra. In: Barrett, C.W., Yang, J. (eds.) 2019 Formal Methods in Computer Aided Design, FMCAD 2019. pp. 28–36. IEEE (2019). https://doi.org/10.23919/FMCAD.2019.8894250
  * [34] Krishnamurthy, Murthy: Fast iterative division of p-adic numbers. IEEE transactions on computers 100(4), 396–398 (1983)
  * [35] Kroening, D., Strichman, O.: Decision Procedures - An Algorithmic Point of View, Second Edition. Texts in Theoretical Computer Science. An EATCS Series, Springer (2016). https://doi.org/10.1007/978-3-662-50497-0
  * [36] Maplesoft, a division of Waterloo Maple Inc..: Maple, https://hadoop.apache.org
  * [37] Müller-Olm, M., Seidl, H.: Analysis of modular arithmetic. ACM Trans. Program. Lang. Syst. 29(5), 29 (2007). https://doi.org/10.1145/1275497.1275504, https://doi.org/10.1145/1275497.1275504
  * [38] Niemetz, A., Preiner, M.: Bitwuzla. In: Enea, C., Lal, A. (eds.) Computer Aided Verification - 35th International Conference, CAV 2023, Part II. Lecture Notes in Computer Science, vol. 13965, pp. 3–17. Springer (2023). https://doi.org/10.1007/978-3-031-37703-7_1
  * [39] Norton, G.H., Sǎlǎgean, A.: Strong Gröbner bases for polynomials over a principal ideal ring. Bulletin of the Australian Mathematical Society 64(3), 505–528 (2001)
  * [40] Ozdemir, A., Kremer, G., Tinelli, C., Barrett, C.W.: Satisfiability modulo finite fields. In: Enea, C., Lal, A. (eds.) Computer Aided Verification - 35th International Conference, CAV 2023, Part II. Lecture Notes in Computer Science, vol. 13965, pp. 163–186. Springer (2023). https://doi.org/10.1007/978-3-031-37703-7_8
  * [41] Park, K., D’Antoni, L., Reps, T.W.: Synthesizing specifications. Proc. ACM Program. Lang. 7(OOPSLA2), 1787–1816 (2023). https://doi.org/10.1145/3622861, https://doi.org/10.1145/3622861
  * [42] Pavlenko, E., Wedler, M., Stoffel, D., Kunz, W., Dreyer, A., Seelisch, F., Greuel, G.M.: Stable: A new qf-bv smt solver for hard verification problems combining boolean reasoning with computer algebra. 2011 Design, Automation & Test in Europe pp. 1–6 (2011), https://api.semanticscholar.org/CorpusID:16387039
  * [43] Rodríguez-Carbonell, E., Kapur, D.: Automatic generation of polynomial loop invariants: Algebraic foundations. In: Proceedings of the 2004 international symposium on Symbolic and algebraic computation. pp. 266–273 (2004)
  * [44] Sankaranarayanan, S., Sipma, H., Manna, Z.: Non-linear loop invariant generation using Gröbner bases. In: Jones, N.D., Leroy, X. (eds.) Proceedings of the 31st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2004. pp. 318–329. ACM (2004). https://doi.org/10.1145/964001.964028
  * [45] Sankaranarayanan, S., Sipma, H.B., Manna, Z.: Constraint-based linear-relations analysis. In: Giacobazzi, R. (ed.) Static Analysis, 11th International Symposium, SAS 2004. Lecture Notes in Computer Science, vol. 3148, pp. 53–68. Springer (2004). https://doi.org/10.1007/978-3-540-27864-1_7, https://doi.org/10.1007/978-3-540-27864-1_7
  * [46] Schneier, B.: Applied cryptography: protocols, algorithms, and source code in C. john wiley & sons (2007)
  * [47] Seed, T., Coppins, C., King, A., Evans, N.: Polynomial analysis of modular arithmetic. In: Hermenegildo, M.V., Morales, J.F. (eds.) Static Analysis - 30th International Symposium, SAS 2023. Lecture Notes in Computer Science, vol. 14284, pp. 508–539. Springer (2023). https://doi.org/10.1007/978-3-031-44245-2_22
  * [48] Seed, T., King, A., Evans, N.: Reducing bit-vector polynomials to SAT using Gröbner bases. In: Pulina, L., Seidl, M. (eds.) Theory and Applications of Satisfiability Testing - SAT 2020 - 23rd International Conference. Lecture Notes in Computer Science, vol. 12178, pp. 361–377. Springer (2020). https://doi.org/10.1007/978-3-030-51825-7_26
  * [49] Seidl, H., Flexeder, A., Petter, M.: Analysing all polynomial equations in $\mathbb{Z}_{2^{w}}$. In: Alpuente, M., Vidal, G. (eds.) Static Analysis, 15th International Symposium, SAS 2008. Lecture Notes in Computer Science, vol. 5079, pp. 299–314. Springer (2008). https://doi.org/10.1007/978-3-540-69166-2_20
  * [50] Stillwell, J.: Elements of Number Theory. Undergraduate Texts in Mathematics, Springer New York, NY (2002). https://doi.org/10.1007/978-0-387-21735-2
  * [51] Wienand, O., Wedler, M., Stoffel, D., Kunz, W., Greuel, G.: An algebraic approach for proving data correctness in arithmetic data paths. In: Gupta, A., Malik, S. (eds.) Computer Aided Verification, 20th International Conference, CAV 2008. Lecture Notes in Computer Science, vol. 5123, pp. 473–486. Springer (2008). https://doi.org/10.1007/978-3-540-70545-1_45
  * [52] Wintersteiger, C.M., Hamadi, Y., de Moura, L.M.: Efficiently solving quantified bit-vector formulas. Formal Methods Syst. Des. 42(1), 3–23 (2013). https://doi.org/10.1007/S10703-012-0156-2
  * [53] Yao, P., Ke, J., Sun, J., Fu, H., Wu, R., Ren, K.: Demystifying template-based invariant generation for bit-vector programs. In: 38th IEEE/ACM International Conference on Automated Software Engineering, ASE 2023. pp. 673–685. IEEE (2023). https://doi.org/10.1109/ASE56229.2023.00069
  * [54] Zankl, H., Middeldorp, A.: Satisfiability of non-linear (ir)rational arithmetic. In: Clarke, E.M., Voronkov, A. (eds.) Logic for Programming, Artificial Intelligence, and Reasoning - 16th International Conference, LPAR-16, Revised Selected Papers. Lecture Notes in Computer Science, vol. 6355, pp. 481–500. Springer (2010). https://doi.org/10.1007/978-3-642-17511-4_27

##  Appendix A Omitted Content of Section 3

###  A.1 Omitted Proof of Proposition 5

###### Proof.

First, let $\nu_{2}(a)=\alpha$. Then $a$ can be written in the form of
$a=2^{\alpha}\cdot a^{\prime}$, where $a^{\prime}$ is an odd number. Thus,
according to Bézout’s lemma, there exist $s,t\in\mathbb{Z}_{2^{d}}$ such that
$s\cdot a^{\prime}+t\cdot 2^{d}=1$. Thus, $a\cdot s=2^{\alpha}\cdot(1-t\cdot
2^{d})=2^{\alpha}$.

Second, we show when $\alpha=0$, $b$ is unique. Otherwise, if there are two
distinct $b_{1},b_{2}$ such that $ab_{1}=ab_{2}=1$, then
$a\cdot(b_{1}-b_{2})=0$. Since $a$ is odd and $b_{1}\neq b_{2}$, it causes a
contradiction. ∎

###  A.2 Omitted Parts of Proposition 6

###### Proof.

First, we show that $f_{i}\neq g_{i}$ has a solution is equivalent to
$e_{i}(f_{i}-g_{i})=2^{d-1}$ has a solution. If $f_{i}\neq g_{i}$ has a
solution, then there exists a non-zero constant number
$c\in\mathbb{Z}_{2^{d}}$ such that $f_{i}-g_{i}=c$ has solutions. Since $c\neq
0$, according to Proposition 5, there exists an integer
$b\in\mathbb{Z}_{2^{d}}$ such that $cb=2^{d-1}$. Thus,
$e_{i}(f_{i}-g_{i})=2^{d-1}$ definitely has a solution. On the other hand, it
is not hard to verify each solution of $e_{i}(f_{i}-g_{i})=2^{d-1}$ is also a
solution of $f_{i}\neq g_{i}$. Thus, the above statement implies $\Phi$ is
satisfiable if and only if $\bigwedge_{i}(h_{i}=0)$ is satisfiable, which is
equivalent to the variety of $H$ is non-empty. ∎

###  A.3 Omitted Proof of Theorem 11

###### Proof.

To begin with, we show that $\textsf{apoly}\left(f\right)$ and
$\textsf{spoly}\left(f,g\right)$ satisfy the definitions of A-polynomial and
S-polynomial, respectively. First, for each
$a\in\mathrm{Ann}(\textsf{lc}(f))$, since $a\cdot\textsf{lc}(f)=0$,
$\nu_{2}(a)\geq d-\nu_{2}(\textsf{lc}(f))$. On the other hand, it is not hard
to verify each integer $b\in\left\langle
2^{d-\nu_{2}(\textsf{lc}(f))}\right\rangle_{\mathbb{Z}_{2^{n}}}$ belongs to
$\mathrm{Ann}(\textsf{lc}(f))$ Thus, $\left\langle
2^{d-\nu_{2}(\textsf{lc}(f))}\right\rangle_{R}=\mathrm{Ann}(\textsf{lc}(f))$,
which implies $\textsf{apoly}\left(f\right)\in\mathrm{Apoly}(f)$. Second,
since $c_{1}\textsf{lc}(f)=c_{2}\textsf{lc}(g)=2^{v}$ is definitely a least
common multiple of $\textsf{lc}(f)$ and $\textsf{lc}(g)$,
$\textsf{apoly}\left(f,g\right)$ is a valid S-polynomial of $f$ and $g$.

Next, as [39, Proposition 3.9, 6.2], we know Algorithm 1 always terminates and
returns a strong Gröbner basis when the coefficient ring is
$\mathbb{Z}_{2^{n}}$. ∎

###  A.4 Omitted Proof of Theorem 12

###### Proof.

First, we show the complete procedure always terminates by demonstrating the
operations of Line 8,13, and 18 can only be executed finite times. Each time
we execute Line 8, the number of unassigned variables in $M$ strictly
decreases. Hence, it cannot be executed infinite times. In addition, since
each polynomial can only be factorized into finite polynomials over
$\mathbb{Z}$ whose degrees are non-zero and the range of $i$ is limited, the
operation in Line 13 will also be executed finite times. Moreover, since the
size of $\mathbb{Z}_{2^{n}}$ is finite, the last operation (in Line 18) will
also be executed finite times.

Second, we show it will always return a valid solution if $\mathcal{V}(H)$ is
non-empty. When $G$ contains a univariate polynomial
$p\in\mathbb{Z}_{2^{n}}[x_{i}]$, for any solution $z\in\mathcal{V}(G)$, it
also belongs to $Zeros(p)$. Second, if $p$ can be decomposed to two
polynomials $f,g$ over $\mathbb{Z}$, for any solution $z\in\mathcal{V}(G)$, it
would also be a solution to $(f\cdot 2^{i}=0)\wedge(g\cdot 2^{d-i}=0)$ for
some $0\leq i\leq d-1$. Conversely, for each $z$ of
$\mathcal{V}(G\cup\\{f\cdot 2^{i},g\cdot 2^{d-i}\\}\setminus\\{p\\})$, it also
belongs to $\mathcal{V}(G)$. Finally, the correctness of the exhausted search
is obvious. ∎

###  A.5 Omitted Description of Finding Multiplicative Inverse

Before presenting the proof of Theorem 13, we first present our approach to
implementing the operation $f\leftarrow\frac{2^{d}-r}{a}$ (in Line 2 of
Algorithm 3) through Newton’s method. Then we will estimate the complexity of
the number of arithmetic operations and binary operations.

Since $1\leq r\leq a-1$, we have
$\frac{2^{d}-r}{a}=\left\lfloor\frac{2^{d}}{a}\right\rfloor$. To calculate it,
we first give an estimation of $\frac{1}{a}$ through Newton’s method and then
multiply it by $2^{d}$ through one bitwise shift operation. Next, consider the
binary representation of $\frac{1}{a}$. If it is finite, it can have a non-
zero bit at most in the first $\lceil\log(a)\rceil$ bits. Otherwise, since $a$
is odd, it could be represented as $0.\overline{(b_{1}\ldots b_{\ell})}_{2}$,
where $b_{1}\ldots b_{\ell}$ is the repetend with $\ell\leq a-1$ [21]. Hence,
we first calculate the first $2a$ bits of $a$, then determine the length of
repetend, and finally extend it to $d$ bits. Then, through a shifting
operation (i.e., $\frac{1}{a}\gg d$), we are able to get the value of
$\frac{2^{d}-r}{a}$.

We adopt Newton’s method to find the first $2a$ bits of $\frac{1}{a}$. Let
$f(x)=\frac{1}{x}-a$. In particular, let $x_{n}$ be the approximate result of
the zero of $f(x)$ at the $n$-th round. Initially, we let
$x_{0}=\frac{1}{2^{\lceil\log a\rceil}}$. We calculate it by the following
equation,

$x_{n+1}=x_{n}-\frac{f(x_{n})}{f^{\prime}(x_{n})}=x_{n}-\frac{\frac{1}{x_{n}}-a}{-\frac{1}{x_{n}^{2}}}=x_{n}(2-x_{n}\cdot
a)\,.$ (4)

Hence,

$\left|x_{n}-\frac{1}{a}\right|=a\left|x_{n-1}-\frac{1}{a}\right|^{2}=\cdots=a^{2^{n}-1}\left|x_{0}-\frac{1}{a}\right|^{2^{n}}<(ax_{0}-1)^{2^{n}}\,.$

Since the first bit of the fractional part of $\frac{a}{2^{\lceil\log
a\rceil}}$ should be one, $\left|ax_{0}-1\right|\leq\frac{1}{2}$. To make
$\left|x_{n}-\frac{1}{a}\right|<\frac{1}{2^{2a}}$, it suffices to let
$n\geq\log(2a)=\log a+1$.

Afterward, we are going to find the concrete value for $\ell$. We start from
$i=1$ to determine whether $b_{1}\ldots b_{i}$ is a valid repetend by shifting
$b_{1}\ldots b_{i}$ and determining whether the first $2a$ bits of
$b_{1}\ldots b_{i}b_{1}\ldots b_{i}\ldots$ and the fractional part of $x_{n}$
are the same. If not, we increase $i$ by one and continue the above procedure.
Its correctness is guaranteed by the following lemma.

######  Lemma 18.

The above procedure returns a valid and minimum repetend of $\frac{1}{a}$.

###### Proof.

Suppose the length of repetend returned by the above procedure is $i$. For the
sake of contradiction, we assume the length of minimum repetend is $\ell$
satisfying $i<\ell<a$. If $i$ divides $\ell$, that means the valid repetend
$b_{1}\ldots b_{\ell}$ can also be written as the form of $b_{1}\ldots
b_{i}b_{1}\ldots b_{i}\ldots$, which causes a contradiction. Otherwise, since
the first $2a$ bits of $b_{1}\ldots b_{i}b_{1}\ldots b_{i}\ldots$ and the
fractional part of $x_{n}$ are the same, we have

$b_{j}=b_{\ell+j}=b_{(\ell+j)\ \mathrm{mod}\ i},\text{for any }1\leq j\leq
i\,.$

Since $\ell\mod i\neq 0$ is smaller than $i$, the above equation implies
$\ell\mod i$ should be first returned by our procedure instead of $i$. This
causes a contradiction. Hence, $b_{1}\ldots b_{i}$ is a valid repetend.
Additionally, it is not hard to verify that it is also the minimum. ∎

Next, we show the proof of Theorem 13, which estimates the number of
arithmetic operations and binary operations.

###### Proof.

In Line 1, we invoke the modular exponentiation algorithm. In each round, we
do one multiplication ($r\leftarrow r^{2}$) and one modulo operation
($r\leftarrow r\mod a$). There are at most $\lceil\log d\rceil$ rounds. Hence,
the number of arithmetic operations of Line 1 is at most $2\lceil\log
d\rceil$.

In Line 2, as described, we first adopt Newton’s method to compute the first
$4a$ bits of $\frac{1}{a}$. It runs no more than $\log a+1$ rounds, and in
each round, there are two multiplication and one subtraction. One
multiplication costs no more than $\mathcal{O}(2\cdot(2a)^{2})$ and a
subtraction costs $\mathcal{O}(2\cdot 2a)$ binary operations. Moreover, the
latter procedure for finding $\ell$ costs no arithmetic operations but
$\mathcal{O}(2a\cdot a)$ binary operations. After that, we shift $x_{n}$
multiply and find its first $d$ bits, which costs $\mathcal{O}(d)$ binary
operations.

In Line 3, we invoke extended Euclidean algorithm to find $k_{1},k_{2}$ such
that $k_{1}\cdot r+k_{2}\cdot a=-1$, where $r<a$. It runs no more than
$\mathcal{O}(\log a)$ rounds. In each round, there are five arithmetic
operations (including one division, two multiplications, and two
substractions). Thus, this step costs $\mathcal{O}(5\cdot\log a)$ arithmetic
operations. Since each operand is no more than $a$, it costs $\mathcal{O}(\log
a\cdot(6\log^{2}a+4\log a))$ binary operations.

The multiplication in Line 4 is the most expensive operation. It costs one
multiplication and one subtraction, and $\mathcal{O}(2d^{2}+3d)$ binary
operations.

By summing them up, we could get the number of arithmetic operations by

$\mathcal{O}\left(2\log d+3(\log a+1)+5\log a+3\right)=\mathcal{O}(2\log
d+8\log a),$

and the number of binary operations by

$\displaystyle\mathcal{O}(\log d\cdot((\log a)^{2}+\log a)+(\log
a+1)\cdot(8a^{2}+4a)+2a^{2}+d$ $\displaystyle+\log a\cdot(6\log^{2}a+4\log
a)+2d^{2}+3d)$ $\displaystyle=\mathcal{O}(2d^{2}+4d+a^{2}\cdot(8\log
a+2)+4a\cdot\log a),$

which concludes Theorem 13. ∎

######  Remark.

When the first $2a$ bits of $\frac{1}{a}$ are precomputed, and the procedure
of finding minimum repetend is optimized by the Knuth–Morris–Pratt (KMP)
algorithm, the number of arithmetic operations can be optimized to
$\mathcal{O}(2\log d+5\log a+3)$. Meanwhile, the number of binary operations
can be optimized to

$\displaystyle\mathcal{O}(\log d\cdot((\log a)^{2}+\log a)+a+d+\log
a\cdot(6\log^{2}a+4\log a)+2d^{2}+3d)$
$\displaystyle=\mathcal{O}(2d^{2}+4d+a+6\log^{3}a)\,.$

##  Appendix B Omitted Proofs of Section 4

###  B.1 Paramertic Normal Form Calculation

Algorithm 4 Paramertic Normal form of $f$ with respect to $G$.

1:$f$ and $G$, where $f\in\mathcal{L}[V]$ and
$\mathcal{L}=\mathbb{Z}_{2^{n}}[\bm{\lambda}]$ and
$G\subseteq\mathbb{Z}_{2^{n}}[V]$

2:$\mathrm{PNF}_{G}(f)$

3:function $\mathrm{PNF}_{G}(f)$

4: while there exists $g\in G$ such that $\textsf{lm}(g)\ |\ t$ and
$\nu_{2}(\textsf{lc}(g))\leq\bar{\nu}_{2}(c_{t})$, where $t=c_{t}m_{t}$ is a
non-zero term of $f$ do

5: $f\leftarrow
f-\frac{c_{t}}{2^{\nu_{2}(\textsf{lc}(g))}}\cdot\left(\frac{\textsf{lc}(g)}{2^{\nu_{2}(\textsf{lc}(g))}}\right)^{-1}\frac{m_{t}}{\textsf{lm}(g)}g$
return $f$

Given a polynomial $f$, suppose the returned value of Algorithm 4 is
$\mathrm{PNF}_{G}(f)$. The correctness of Algorithm 4 is shown as follows.

######  Lemma 19 (Correctness of Algorithm 4).

Algorithm 4 always terminates, and $\mathrm{PNF}_{G}(f)$ is a valid parametric
normal form.

###### Proof.

We first show it always terminates. Otherwise, suppose the leading monomial of
input $f$ is $\bm{x}^{\bm{\alpha}}$ and the largest leading monomial of $G$ is
$\bm{x}^{\bm{\beta}}$. If the reduction algorithm does not terminate, that
means there exists an infinite number of monomials between
$\bm{x}^{\bm{\alpha}}$ and $\bm{x}^{\bm{\beta}}$, which is impossible since we
are using well-ordered monomial ordering (see more details in [1, Chapter
1.4]).

Then we prove $\mathrm{PNF}_{G}(f)$ is a valid parametric normal form by
verifying the three properties of Definition 15. The first property is obvious
since the loop condition (in Line 4) is not met. Next, in each round, we scale
a polynomial $g$ of $G$ and eliminate the leading term of $f$. Hence, by
summing them up, we know $f-\mathrm{PNF}_{G}(f)$ can be written as a linear
combination of polynomials of $G$, where coefficients come from
$\mathcal{L}[V]$. Thus, $r=f-\mathrm{PNF}_{G}(f)$ belongs to $\left\langle
G\right\rangle_{\mathcal{L}[V]}$. Finally, we show the second condition is
also satisfied by contradiction. If it is not satisfied, there exits $g\in G$,
such that
$\textsf{lt}(\mathrm{PNF}_{G}(f))\in\left\langle\textsf{lt}(g)\right\rangle_{\mathcal{L}[V]}$.
Hence, $\textsf{lt}(\mathrm{PNF}_{G}(f))$ could be written in the form of
$h\cdot\textsf{lt}(g)$, where $h\in\mathcal{L}[V]$. Thus, $\textsf{lm}(g)$
divides $\textsf{lm}(f)$ and
$\nu_{2}(\textsf{lc}(g))\leq\nu_{2}(\textsf{lc}(f))$, which meets the loop
condition (in Line 4) and causes a contradiction. ∎

###  B.2 Proof of Proposition 16

###### Proof.

According to the third property of Definition 15,
$r=(\eta^{\prime}-\mu\cdot\eta)-\mathrm{PNF}(\eta^{\prime}-\mu\cdot\eta\ |\
G)$ belongs to $\left\langle
G:\mathbb{Z}_{2^{d}}[V]\right\rangle_{\mathcal{L}[V]}$. Without loss of
generality, assume $r=h_{1}\cdot g_{1}+\ldots+h_{k}\cdot g_{k}$, where
$h_{i}\in\mathcal{L}[V],g_{i}\in G$. By substituting the assignment of
$\bm{\lambda}$ into $h_{i}$, we can find that $r$ belongs to $\left\langle
G\right\rangle$ since $h_{i}$ currently turns an element of
$\mathbb{Z}_{2^{n}}[V]$. Since $\mathrm{PNF}(\eta^{\prime}-\mu\cdot\eta\ |\
G)=0$ under this assignment, we could find $\eta^{\prime}-\mu\cdot\eta$
belongs to $\left\langle G\right\rangle$. Thus, we have
$\eta^{\prime}-\mu\cdot\eta\twoheadrightarrow_{GB(F_{\rho})}^{*}0$ under that
assignment, which implies $\mathrm{NF}(\eta^{\prime}-\mu\cdot\eta\ |\ G)=0$. ∎

###  B.3 Description of Methods for Finding Solutions.

Formally, let $\mathcal{C}=\\{c_{i}\\}_{i=1}^{\left|\mathcal{C}\right|}$ be
the set of coefficients of
$\mathrm{PNF}_{GB(F_{\rho})}(\eta^{\prime}-\mu\cdot\eta)$. We first construct
a system of congruences: $c_{i}=0\ (\mathrm{mod}\ 2^{d})$ for
$i=1,\ldots\left|\mathcal{C}\right|$. Next, we first utilize Smith normal form
[13] to find a specific solution $\bm{\lambda_{0}}$ of this system. Afterward,
we introduce a set of fresh variables
$\\{v_{i}\\}_{i=1}^{\left|\mathcal{C}\right|}$ and convert the original system
of linear congruences to $c_{i}-v_{i}\cdot 2^{d}=0$ for
$i=1,\ldots\left|\mathcal{C}\right|$. Let $\mathbf{A}$ be the coefficient
matrix of $(\\{\lambda_{q}\\}_{q\in M^{(k)}[V]},\\{v_{i}\\}_{1\leq
i\leq\left|\mathcal{C}\right|})$.

Then we compute the nullspace of $\mathbf{A}$ over $\mathbb{R}$. Denote it by
$\mathrm{Null}(\mathbf{A})=\\{(\bar{\bm{\lambda}},\bar{\bm{v}})\ :\
\mathbf{A}\cdot(\bm{\lambda},\bm{v})^{\mathrm{T}}=\mathbf{0}\\}$, where
$\bar{\bm{\lambda}}$ and $\bar{\bm{v}}$ are assignments of $\bm{\lambda}$ and
$\bm{v}$, represtively. Since $\mathbf{A}$ is a matrix over integer domain
$\mathbb{Z}$, the elements of each vector belonging to
$\mathrm{Null}(\mathbf{A})$ are rational numbers. For each
$\bm{s}=(\bar{\bm{\lambda}},\bar{\bm{v}})\in\mathrm{Null}(\mathbf{A})$, let
$\mathcal{D}(\bm{s})$ denote the set of all the denominators of $\bm{s}$. Let
$\mathcal{S}^{\mu}$ be defined as follows.

$\mathcal{S}^{\mu}\triangleq\\{\bm{\lambda}_{0}+\bar{\bm{\lambda}}\cdot\mathrm{lcm}(\mathcal{D}(\bm{s})):\bm{s}=(\bar{\bm{\lambda}},\bar{\bm{v}})\in\mathrm{Null}(\mathbf{A})\\}.$

We could verify each vector $\bm{s}\in\mathcal{S}^{\mu}$ is a solution to
$c_{i}-v_{i}\cdot 2^{d}=0$ for any $c_{i}\in\mathcal{C}$. By substituting the
elements of $\bm{s}$ into $\\{\lambda_{q}\\}_{q\in M_{k}[V]}$, we are able to
get a set of concrete loop invariants.

###  B.4 Formal Description of Step B4

Formally, we first construct a set of fresh variables
$V_{0}=\\{x_{1,0},\ldots,x_{n,0}\\}$ representing the initial values of all
variables. Then, we construct a conjunction of assertion $\mathcal{A}_{1}$ by
substituting $x_{i}$ by $x_{i,0}$ in the initial condition.

Next, regarding the values of $\mu$ we select, we are going to construct
$\mathcal{A}_{2}^{\mu},\mathcal{A}_{3}^{\mu}$ according to $\mathcal{S}^{\mu}$
as follows. If $\mu=1$, for each solution
$\bm{s}=(\bar{\bm{\lambda}},\bar{\bm{v}})\in\mathcal{S}^{1}$, we create a
fresh bit-vector variable $c_{s}$ and construct two constraints
$\eta(V_{0},k)+c_{s}=0$ and $\eta(V,k)+c_{s}=0$ by instantiating
$\\{\lambda_{q}\\}$ by $\bar{\bm{\lambda}}$ and replacing $\xi$ by $0$. Then
we append the two constraints to $\mathcal{A}_{2}^{1}$ and
$\mathcal{A}_{2}^{3}$ respectively. Finally, we check whether
$\mathcal{A}_{1}^{1}\wedge\mathcal{A}_{2}^{1}\wedge\mathcal{A}_{3}^{1}\Rightarrow\kappa(V)$
is satisfiable.

Otherwise, if $\mu\neq 1$, for each
$\bm{s}=(\bar{\bm{\lambda}},\bar{\bm{v}})\in\mathcal{S}^{\mu}$, we construct
two constraints $\eta(V_{0},k)=0$ and $\eta(V,k)=0$ by instantiating
$\bm{\lambda}$ by $\bar{\bm{\lambda}}$, and append them to
$\mathcal{A}_{2}^{\mu}$ and $\mathcal{A}_{3}^{\mu}$, respectively. Then we
first check whether the calculated invariant holds for the initial conditions
by verifying $\theta(V_{0})\Rightarrow\eta(V_{0},k)$. If yes, then we further
check whether $\eta(V)\Rightarrow\kappa(V)$ holds.

For example, when the initial condition of Example 1 is modified to
$(0<x<10)\wedge(0<y<10)$, we are able to get the solution set
$\mathcal{S}^{1}=\\{(\lambda_{x}:1,\lambda_{y}:-1)\\}$ by setting $\mu=1$ and
$k=1$. Then according to the above method, we can verify the postcondition
$\kappa(V)=(x_{2}-x_{1}<10)$ through determining the satisfiablity of the
below formula.

$\displaystyle((0<x_{0}<10)\wedge(0<y_{0}<10)$ ($\mathcal{A}_{1}$)
$\displaystyle\wedge(x_{0}-y_{0}+c_{s}=0)$ ($\mathcal{A}_{2}^{1}$)
$\displaystyle\wedge(x-y+c_{s}=0))$ ($\mathcal{A}_{3}^{1}$)

$\Rightarrow\quad(y-x<10)\,.$

##  Appendix C Experimental Results of Loop Invariant Generation

Table 3: Performance of Eldarica and our method in 2016.Sygus-Comp [2]. 2016.Sygus-Comp [2] | Inv | Eldarica [30] | Our Method $(\S$4)
---|---|---|---
Time (s) | Mem (MB) | Time | Speedup | Mem | Save up
anfp-new | Poly | $>200$ | $>10^{3}$ | 0.5 | 62.5X | 71.0 | 5.4X
anfp | Poly | $>200$ | $>10^{3}$ | 0.3 | 107.1X | 70.2 | 4.9X
cegar1_vars-new | Lin | 25.3 | 273.5 | 1.6 | 15.9X | 70.5 | 3.9X
cegar1_vars | Lin | 26.8 | 289.2 | 1.5 | 18.3X | 70.4 | 4.1X
cegar1-new | Lin | 29.4 | 279.2 | 1.0 | 30.0X | 70.3 | 4.0X
cegar1 | Lin | 24.4 | 266.5 | 1.0 | 24.7X | 70.2 | 3.8X
cgmmp-new | Lin | 10.9 | 206.8 | 1.0 | 11.1X | 70.3 | 2.9X
cgmmp | Lin | 11.1 | 212.5 | 0.9 | 12.4X | 73.2 | 2.9X
ex23_vars | Lin | 12.2 | 232.1 | 1.7 | 7.2X | 70.7 | 3.3X
ex14_simpl | Lin | 9.8 | 209.2 | 1.2 | 8.3X | 70.6 | 3.0X
ex14_vars | Lin | 9.7 | 210.5 | 1.9 | 5.1X | 70.8 | 3.0X
ex14-new | Lin | 6.0 | 181.1 | 1.0 | 6.1X | 70.3 | 2.6X
ex14 | Lin | 6.4 | 192.2 | 0.9 | 7.3X | 70.5 | 2.7X
ex23 | Lin | 11.5 | 236.3 | 1.4 | 8.3X | 70.6 | 3.3X
fig1_vars-new | Poly | 5.9 | 195.7 | 14.9 | 0.4X | 71.8 | 2.7X
fig1_vars | Poly | 5.9 | 199.4 | 13.9 | 0.4X | 71.7 | 2.8X
fig1-new | Poly | 5.6 | 182.4 | 1.6 | 3.6X | 70.6 | 2.6X
fig1 | Poly | 5.5 | 182.8 | 1.7 | 3.3X | 70.9 | 2.6X
fig9_vars | Lin | 3.2 | 198.6 | 1.9 | 1.7X | 70.2 | 2.8X
fig9 | Lin | 5.7 | 181.0 | 0.9 | 6.5X | 60.9 | 3.0X
sum1_vars | Lin | 21.5 | 261.7 | 1.4 | 15.6X | 74.2 | 3.5X
sum1 | Lin | 20.0 | 258.4 | 1.4 | 14.3X | 74.0 | 3.5X
sum3_vars | Lin | 7.0 | 200.0 | 1.4 | 5.1X | 74.3 | 2.7X
sum3 | Lin | 6.9 | 190.7 | 1.5 | 4.6X | 74.3 | 2.6X
sum4_simp | Lin | 20.0 | 272.2 | 1.5 | 13.5X | 74.2 | 3.7X
sum4_vars | Lin | 22.0 | 256.5 | 1.3 | 17.2X | 73.9 | 3.5X
sum4 | Lin | 7.7 | 194.5 | 1.3 | 6.0X | 73.9 | 2.6X
tacas_vars | Lin | 22.1 | 272.4 | 1.6 | 14.0X | 74.6 | 3.7X
tacas | Lin | 24.7 | 309.0 | 1.5 | 16.7X | 74.1 | 4.2X
$29$ in total |  |  |  |  |  |  |

2018.SV-Comp [7] | Inv | Eldarica [30] | Our Method $(\S$4)
---|---|---|---
Time (s) | Mem (MB) | Time | Speedup | Mem | Save up
cggmp2005_true$\ldots$ | Lin | 11.9 | 204.4 | 0.88 | 13.5X | 72.2 | 2.8X
cggmp2005_variant$\ldots$ | Lin | 28.4 | 349.9 | 0.98 | 30.6X | 72.3 | 4.8X
const-false-unreach-call1$\ldots$ | Lin | 8.0 | 190.0 | 0.78 | 10.3X | 71.8 | 2.6X
const-true-unreach-call1$\ldots$ | Lin | 11.2 | 206.1 | 0.78 | 14.3X | 71.8 | 2.9X
count_up_down_$\ldots$ | Lin | 6.8 | 196.2 | 0.98 | 6.9X | 72.2 | 2.7X
css2003_true-unreach$\ldots$ | Lin | 6.8 | 196.2 | 0.98 | 6.9X | 72.2 | 2.7X
down_true-$\ldots$ | Lin | 9.4 | 204.3 | 1.2 | 8.0X | 72.5 | 2.8X
gsv2008_true-unreach$\ldots$ | Poly | 5.1 | 179.7 | 0.5 | 10.5X | 70.6 | 2.5X
hhk2008_true-unreach$\ldots$ | Lin | 7.5 | 192.4 | 1.2 | 6.4X | 72.3 | 2.7X
jm2006_true-unreach$\ldots$ | Lin | 16.6 | 222.6 | 1.19 | 14.0X | 72.2 | 3.1X
jm2006_variant_true$\ldots$ | Lin | 24.1 | 528.8 | 1.38 | 17.5X | 72.4 | 7.3X
multivar_false-$\ldots$ | Lin | 9.5 | 198.7 | 0.98 | 9.7X | 72.1 | 2.8X
multivar_true-$\ldots$ | Lin | 6.3 | 189.6 | 0.89 | 7.0X | 72.1 | 2.6X
simple_$\ldots$-unreach-call1$\ldots$ | Lin | 10.8 | 207.6 | 1.2 | 9.1X | 72.2 | 2.9X
simple_$\ldots$-unreach-call2$\ldots$ | Lin | 65.7 | 532.7 | 1.1 | 28.0X | 72.5 | 7.3X
while_infinite_loop_3$\ldots$ | Lin | 4.9 | 148.4 | 0.8 | 6.2X | 71.4 | 2.1X
while_infinite_loop_4$\ldots$ | Lin | 5.2 | 178.9 | 0.9 | 5.9X | 71.7 | 2.5X
$17$ in total |  |  |  |  |  |  |
(a)

2018.CHI_InvGame [11] | Inv | Eldarica [30] | Our Method $(\S$4)
---|---|---|---
Time (s) | Mem (MB) | Time | Speedup | Mem | Saveup
cube2.desugared | Poly | $95.6$ | $504.9$ | 19.3 | 5.0X | 75.0 |  $6.7$X
gauss_sum-more-rows.auto | Poly | $>200$ | $>520.5$ | 0.78 |  $>38.5$X | 70.9 |  $>7.3$X
s9.desugared | Poly | $>200$ | $>676.9$ | 22.0 |  $>9.1$X | 73.2 |  $>9.2$X
s10.desugared | Poly | $>200$ | $>512.0$ | $0.9$ |  $>227.3$X | 71.4 |  $>7.2$X
s11.desugared | Poly | $>200$ | $>502.8$ | 1.4 |  $>145.9$X | $73.7$ |  $>6.8$X
sorin03.desugared | Poly | $>200$ | $>492.5$ | $1.8$ |  $112.4$X | $71.2$ |  $6.9$X
sorin04.desugared | Poly | 75.5 | 417.5 | 19.5 |  $3.9$X | 73.0 |  $5.7$X
sqrt-more-rows-swap-columns | Poly | $>200$ | $>427.2$ | 12.2 |  $16.4$X | 74.9 |  $>5.7$X
non-lin-ineq-1.desugared | Poly | 6.9 | 243.5 | 2.4 |  $7.8$X | $71.0$ |  $3.4$X
non-lin-ineq-3.desugared | Poly | $>200$ | $>531.7$ | 2.0 |  $>101.0$X | 71.9 |  $>7.4$X
non-lin-ineq-4.desugared | Poly | $>200$ | $>525.2$ | 5.1 |  $>39.3$X | 73.5 |  $>7.1$X
s5auto.desugared | Poly | $>200$ | $>530.0$ | 0.9 |  $>34.1$X | $70.8$ |  $7.5$X
$12$ in total |  |  |  |  |  |  |
(b)

Table 4: Performance of Eldarica and our method on 2018.SV-Comp [7] and
2018.CHI-InvGame [11].