# Properties of Shannon and Rényi entropies of the Poisson distribution as the
functions of intensity parameter

Volodymyr Braiman Taras Shevchenko National University of Kyiv, 64/13
Volodymyrska St., Kyiv, Ukraine<EMAIL_ADDRESS>Anatoliy Malyarenko
Mälardalen University, 721 23 Västerås, Sweden<EMAIL_ADDRESS>Yuliya Mishura Taras Shevchenko National University of Kyiv, 64/13
Volodymyrska St., Kyiv, Ukraine and Mälardalen University, 721 23 Västerås,
Sweden<EMAIL_ADDRESS>Yevheniia Anastasiia Rudyk Taras Shevchenko
National University of Kyiv, 64/13 Volodymyrska St., Kyiv, Ukraine,
<EMAIL_ADDRESS>
(3rd September 2024)

###### Abstract

We consider two types of entropy, namely, Shannon and Rényi entropies of the
Poisson distribution, and establish their properties as the functions of
intensity parameter. More precisely, we prove that both entropies increase
with intensity. While for Shannon entropy the proof is comparatively simple,
for Rényi entropy, which depends on additional parameter $\alpha>0$, we can
characterize it as nontrivial. The proof is based on application of Karamata’s
inequality to the terms of Poisson distribution.

Keywords: Shannon entropy, Rényi entropy, Poisson distribution, Karamata’s
inequality.

##  1 Introduction

The concept and formulas for different types of entropy, which come mainly
from information theory, are now widely used, in many applications, in
particular, in detecting DDoS attacks, see, for example, [2, 6], in
investigation of structure of the neural codes, [16], network traffic [13],
keyword extraction [19], stock market forecast modelling [11] and many others.
Considering these applications, it is natural to assume that, for example, the
distribution of the number of DDoS attacks and of some other related phenomena
is Poisson with some fixed intensity, at least over some fixed time interval.
Considering two types of entropy, namely, Shannon and Rényi entropy, it is
natural to assume that both entropies increase together with intensity
parameter. To the best of our knowledge, this statement was not established
rigorously. Moreover, if for Shannon entropy the proof is comparatively
simple, for Rényi entropy, which depends on additional parameter $\alpha>0$,
we can characterize it as nontrivial. In order to get the proof, we apply
Karamata’s inequality to the terms of Poisson distribution. The verification
of conditions of this inequality also is nontrivial. It involves rearrangement
of the terms of Poisson distribution into a non-increasing sequence and
exploring the monotonicity of partial sums of this sequence.

If to take a historical look, the concept of entropy for a random variable was
introduced by Shannon [18] to characterize the irreducible complexity inherent
in a specific form of randomness. Then Shannon entropy was generalized by
Rényi entropy [17] by introducing an additional parameter $\alpha>0$ that
allows for a range of entropy measures. The presence of this parameter makes
it difficult to accurately calculate the Rényi entropy for various
distributions and study its behavior. A pleasant exception is the normal
distribution. For it, many types of entropies are calculated exactly, and it
can be noted that these entropies increase along with the variance (see [14]).
Furthermore, if the decrease of the Rényi entropy with respect to the
parameter $\alpha$ is a well-known fact, its convexity for discrete
distributions depends on the distribution, see [4].

Taking into account the difficulty with exact computation of entropies, many
attempts were devoted to the numerical calculation and approximation of
entropies, see e.g., [1]–[3], [5], [8]–[9], [20], while the limit of Shannon
entropy of Poisson distribution was calculated, e.g., in [7].

As already mentioned, the purpose of this paper is to prove analytically the
natural fact that the entropy of a Poisson distribution increases with the
intensity of the distribution. We considered Shannon and Rényi entropy. The
paper is constructed as follows: in Section 2 we consider increase and
convexity of Shannon entropy of Poisson distribution as the function of
intensity parameter. In Section 3 increase in intensity of Rényi entropy for
any $\alpha>0$ is proved with the help of Karamata’s inequality. Some by-
product inequalities are obtained in Section 4, while auxiliary statements are
postponed to Appendix.

##  2 Analytical properties of Shannon entropy of Poisson distribution as the
function of intensity parameter $\lambda$

Consider a discrete distribution $\\{p_{i},i\geq 1\\}.$ Its Shannon entropy is
defined as

$H_{S}(p_{i},i\geq 1)=-\sum_{i\geq 1}p_{i}\log p_{i}.$

In particular, we consider Poisson distribution with parameter $\lambda$:

$P\\{\xi_{\lambda}=k\\}=\frac{\lambda^{k}e^{-\lambda}}{k!},k\in\mathbb{N}\cup\\{0\\}.$

Its Shannon entropy $H_{S}(\lambda)$ equals

$H_{S}(\lambda)=-\sum_{k=0}^{\infty}\frac{\lambda^{k}e^{-\lambda}}{k!}\log\left(\frac{\lambda^{k}e^{-\lambda}}{k!}\right)=-\lambda\log\left(\frac{\lambda}{e}\right)+e^{-\lambda}\sum_{k=2}^{\infty}\frac{\lambda^{k}\log
k!}{k!}.$ (1)

It is natural to assume that Shannon entropy $H_{S}(\lambda)$ of Poisson
distribution strictly increases with $\lambda\in(0,+\infty).$ We will prove
this result, as well as the concavity property of $H_{S}(\lambda)$, in the
next statement.

######  Theorem 1.

Shannon entropy $H_{S}(\lambda),\lambda\in(0,+\infty)$ is strictly increasing
and concave in $\lambda.$

###### Proof.

Obviously, we can differentiate the series (1) term by term for any
$\lambda>0$, and get the equality

$\begin{split}H_{S}^{{}^{\prime}}(\lambda)=&-\log\left(\frac{\lambda}{e}\right)-1-e^{-\lambda}\sum_{k=2}^{\infty}\frac{\lambda^{k}\log
k!}{k!}+e^{-\lambda}\sum_{k=2}^{\infty}\frac{\lambda^{k-1}\log k!}{(k-1)!}\
\\\
=&-\log\lambda+e^{-\lambda}\sum_{k=1}^{\infty}\frac{\lambda^{k}\log(k+1)!}{k!}-e^{-\lambda}\sum_{k=2}^{\infty}\frac{\lambda^{k}\log
k!}{k!}\ \\\
=&-\log\lambda+e^{-\lambda}\sum_{k=1}^{\infty}\frac{\lambda^{k}\log(k+1)}{k!}.\
\end{split}$ (2)

It is clear that both terms in the right-hand side of (2) are non-negative for
for $\lambda\in(0,1],$ and the second one is strictly positive, therefore
$H_{S}^{{}^{\prime}}(\lambda)>0$ for $\lambda\in(0,1].$ So, it is necessary to
prove that $H_{S}^{{}^{\prime}}(\lambda)>0$ for $\lambda>1.$ Let’s calculate

$\displaystyle
H_{S}^{{}^{\prime\prime}}(\lambda)=-\frac{1}{\lambda}-e^{-\lambda}\sum_{k=1}^{\infty}\frac{\lambda^{k}\log(k+1)}{k!}+e^{-\lambda}\sum_{k=1}^{\infty}\frac{\lambda^{k-1}\log(k+1)}{(k-1)!}\
$
$\displaystyle=-\frac{1}{\lambda}+e^{-\lambda}\sum_{k=0}^{\infty}\frac{\lambda^{k}\log(k+2)}{k!}-e^{-\lambda}\sum_{k=1}^{\infty}\frac{\lambda^{k}\log(k+1)}{k!}$
$\displaystyle=-\frac{1}{\lambda}+e^{-\lambda}\log
2+e^{-\lambda}\sum_{k=1}^{\infty}\frac{\lambda^{k}\log(1+\frac{1}{k+1})}{k!}$
$\displaystyle=-\frac{1}{\lambda}+e^{-\lambda}\sum_{k=0}^{\infty}\frac{\lambda^{k}\log(1+\frac{1}{k+1})}{k!}$
$\displaystyle<-\frac{1}{\lambda}+e^{-\lambda}\sum_{k=0}^{\infty}\frac{\lambda^{k}}{(k+1)!}<-\frac{1}{\lambda}+e^{-\lambda}\frac{1}{\lambda}\sum_{k=0}^{\infty}\frac{\lambda^{k+1}}{(k+1)!}$
$\displaystyle<-\frac{1}{\lambda}+e^{-\lambda}\frac{1}{\lambda}e^{\lambda}=0.\
$

So, $H_{S}^{{}^{\prime\prime}}(\lambda)<0$ for all $\lambda>0.$ Therefore,
$H_{S}^{{}^{\prime}}(\lambda)$ strictly decreases in $\lambda$ and it is
sufficient to prove that

$\lim_{\lambda\to\infty}H_{S}^{{}^{\prime}}(\lambda)\geq 0.$

However,

$\lim_{\lambda\to\infty}H_{S}^{{}^{\prime}}(\lambda)=\lim_{\lambda\to\infty}\log\lambda\left(e^{-\lambda}(\log\lambda)^{-1}\sum_{k=1}^{\infty}\frac{\lambda^{k}\log(k+1)}{k!}-1\right),$

and it is sufficient to establish that

${\liminf}_{\lambda\to\infty}e^{-\lambda}(\log\lambda)^{-1}\sum_{k=1}^{\infty}\frac{\lambda^{k}\log(k+1)}{k!}\geq
1.$

This inequality is proved in Lemma A.1. Finally, we get that
$H_{S}^{{}^{\prime}}(\lambda)>0$ for all $\lambda\geq 0$ and
$H_{S}^{{}^{\prime\prime}}(\lambda)<0$ for all $\lambda\geq 0,$ whence the
proof follows. ∎

##  3 Analytical properties of Rényi entropy of Poisson distribution as the
function of intensity parameter $\lambda$

Again, consider a discrete distribution $\\{p_{i},i\geq 1\\}.$ Its Rényi
entropy is defined as

$H_{R}^{\alpha}(p_{i},i\geq 1)=\frac{1}{1-\alpha}\log\left(\sum_{i\geq
1}p_{i}^{\alpha}\right),\leavevmode\nobreak\ \alpha>0,\leavevmode\nobreak\
\alpha\neq 1,$

and

$H_{R}^{\alpha}(p_{i},i\geq 1)\rightarrow H_{S}(p_{i},i\geq 1),$

as $\alpha\rightarrow 1$, where $H_{S}(p_{i},i\geq 1)$ is a Shannon entropy.
In the case of Poisson distribution

$H_{R}^{\alpha}(\lambda)=\frac{1}{1-\alpha}\log\left(e^{-\alpha\lambda}\sum_{k=0}^{\infty}\frac{\lambda^{k\alpha}}{(k!)^{\alpha}}\right),\leavevmode\nobreak\
\alpha>0,\leavevmode\nobreak\ \alpha\neq 1.$ (3)

As for the Shannon entropy, our goal is to investigate the behaviour of Rényi
entropy of Poisson distribution as the function of intensity $\lambda.$ To be
more precise, we wish to prove that for any fixed $\alpha>0,$ $\alpha\neq 1,$
Rényi entropy of Poisson distribution increases in $\lambda$. Let us take into
account equality (3) and consider two cases.

  * •

Let $\alpha\in(0,1).$ Then $\frac{1}{1-\alpha}>0$ and, since logarithm is
strictly increasing, for $H_{R}^{\alpha}(\lambda)$ to increase in $\lambda$
function

$\psi(\alpha,\lambda)=e^{-\alpha\lambda}\sum_{k=0}^{\infty}\left(\frac{\lambda^{k}}{k!}\right)^{\alpha}$
(4)

should increase in $\lambda\in(0,+\infty)$.

  * •

Let $\alpha>1.$ Then $\frac{1}{1-\alpha}<0$ and for $H_{R}^{\alpha}(\lambda)$
to increase in $\lambda$ functions $\log(\psi(\alpha,\lambda))$ and
$\psi(\alpha,\lambda)$ should decrease in $\lambda\in(0,+\infty)$.

In Theorem 2 below we will establish desired character of monotonicity of
$\psi(\alpha,\lambda)$ in $\lambda\in(0,+\infty)$ for both cases $0<\alpha<1$
and $\alpha>1.$

To prove this result, we will apply Karamata’s inequality (see Lemma A.2 in
Appendix). This inequality deals with non-increasing sequences, so it suggests
to rearrange the terms of the Poisson distribution in non-increasing order and
study the properties of the resulting sequence.

Let, as before,
$p_{k}(\lambda)=P\\{\xi_{\lambda}=k\\}=\frac{\lambda^{k}}{k!}e^{-\lambda},k\in\mathbb{N}\cup\\{0\\}.$
Denote by $\\{q_{k}(\lambda):k\geq 0\\}$ the terms of the sequence
$\\{p_{k}(\lambda):k\geq 0\\}$ which are rearranged in non-increasing order.
Note that the sequence $\\{p_{k}(\lambda):k\geq 0\\}$ may contain equal terms.
In this case the sequence $\\{q_{k}(\lambda):k\geq 0\\}$ will contain equal
terms as well.

######  Lemma 1.

For each $n\geq 0$ the function
$S_{n}(\lambda)=\sum\limits_{k=0}^{n}q_{k}(\lambda)$ strictly decreases on
$(0,+\infty).$

###### Proof.

Fix $n\geq 0.$

Firstly, we will establish that for every $\lambda>0$ the number
$S_{n}(\lambda)$ is equal to the sum of some $n+1$ consecutive terms of the
initial sequence $\\{p_{k}(\lambda):k\geq 0\\}.$ Note that
$\frac{p_{k+1}(\lambda)}{p_{k}(\lambda)}=\frac{\lambda}{k+1},$ thus
$p_{k}(\lambda)<p_{k+1}(\lambda)$ for $k<\lambda-1$ and
$p_{k}(\lambda)>p_{k+1}(\lambda)$ for $k>\lambda-1.$ Therefore for every
$0\leq i_{1}<i_{2}<i_{3}$ we have
$p_{i_{2}}(\lambda)>\min\\{p_{i_{1}}(\lambda),p_{i_{3}}(\lambda)\\}.$ It
follows that $q_{0}(\lambda),\ldots,q_{n}(\lambda)$ are $n+1$ consecutive
terms of the sequence $\\{p_{k}(\lambda):k\geq 0\\}.$ Thus
$\bigl{(}q_{0}(\lambda),\ldots,q_{n}(\lambda)\bigr{)}$ is a permutation of
terms $\bigl{(}p_{\ell}(\lambda),\ldots,p_{\ell+n}(\lambda)\bigr{)}$ for some
$\ell=\ell(\lambda)\geq 0,$ so
$S_{n}(\lambda)=\sum\limits_{k=0}^{n}q_{k}(\lambda)=\sum\limits_{k=\ell}^{\ell+n}p_{k}(\lambda).$

Let us determine $\ell(\lambda).$ Put
$s_{n}(m,\lambda)=\sum\limits_{k=m}^{m+n}p_{k}(\lambda),$ $m\geq 0.$ Clearly

$S_{n}(\lambda)=s_{n}(\ell,\lambda)=\max\limits_{m\geq 0}s_{n}(m,\lambda).$

Note that

$s_{n}(m+1,\lambda)-s_{n}(m,\lambda)=\sum\limits_{k=m+1}^{m+n+1}p_{k}(\lambda)-\sum\limits_{k=m}^{m+n}p_{k}(\lambda)=p_{m+n+1}(\lambda)-p_{m}(\lambda)<0$

if and only if

$\frac{p_{m+n+1}(\lambda)}{p_{m}(\lambda)}=\frac{\lambda^{n+1}m!}{(m+n+1)!}=\frac{\lambda^{n+1}}{(m+1)\ldots(m+n+1)}<1,$

i.e., $\lambda<c_{m}=\bigl{(}(m+1)\ldots(m+n+1)\bigr{)}^{\frac{1}{n+1}}.$ It
follows that $s_{n}(m+1,\lambda)>s_{n}(m,\lambda)$ for $\lambda>c_{m}$ and
$s_{n}(m+1,\lambda)<s_{n}(m,\lambda)$ for $\lambda<c_{m}.$ Therefore
$\max\limits_{m\geq 0}s_{n}(m,\lambda)$ is achieved at

$\ell(\lambda)=\begin{cases}0&\text{for $0<\lambda\leq c_{0}$},\\\ m&\text{for
$c_{m-1}\leq\lambda\leq c_{m},$ $m\geq 1$}\end{cases}$

(in particular, in case $\lambda=c_{k}$ we have
$s_{n}(k+1,\lambda)=s_{n}(k,\lambda),$ so one can take either
$\ell(\lambda)=k$ or $\ell(\lambda)=k+1$).

For $0<\lambda\leq c_{0}$ we have
$S_{n}(\lambda)=\sum\limits_{k=0}^{n}p_{k}(\lambda)=\sum\limits_{k=0}^{n}\frac{\lambda^{k}}{k!}e^{-\lambda},$
so

$\displaystyle S^{\prime}_{n}(\lambda)=$
$\displaystyle\sum\limits_{k=1}^{n}\frac{\lambda^{k-1}}{(k-1)!}e^{-\lambda}-\sum\limits_{k=0}^{n}\frac{\lambda^{k}}{k!}e^{-\lambda}$
$\displaystyle=$
$\displaystyle\sum\limits_{k=0}^{n-1}\frac{\lambda^{k}}{k!}e^{-\lambda}-\sum\limits_{k=0}^{n}\frac{\lambda^{k}}{k!}e^{-\lambda}=-\frac{\lambda^{n}}{n!}e^{-\lambda}<0$

and the function $S_{n}(\lambda)$ strictly decreases on $(0,c_{0}].$

For $c_{m-1}<\lambda\leq c_{m},$ $m\geq 1,$ we have
$S_{n}(\lambda)=\sum\limits_{k=m}^{m+n}p_{k}(\lambda)=\sum\limits_{k=m}^{m+n}\frac{\lambda^{k}}{k!}e^{-\lambda},$
so

$\displaystyle S^{\prime}_{n}(\lambda)=$
$\displaystyle\sum\limits_{k=m}^{m+n}\frac{\lambda^{k-1}}{(k-1)!}e^{-\lambda}-\sum\limits_{k=m}^{m+n}\frac{\lambda^{k}}{k!}e^{-\lambda}$
$\displaystyle=$
$\displaystyle\sum\limits_{k=m-1}^{m+n-1}\frac{\lambda^{k}}{k!}e^{-\lambda}-\sum\limits_{k=m}^{m+n}\frac{\lambda^{k}}{k!}e^{-\lambda}=\frac{\lambda^{m-1}}{(m-1)!}e^{-\lambda}-\frac{\lambda^{m+n}}{(m+n)!}e^{-\lambda}<0,$

which is equivalent to $\lambda^{n+1}>m(m+1)\ldots(m+n),$ or
$\lambda>c_{m-1}.$ Hence the function $S_{n}(\lambda)$ also strictly decreases
on $[c_{m-1},c_{m}]$ for each $m\geq 1.$

Clearly $c_{m}\to+\infty$ as $m\to\infty.$ Thus $S_{n}(\lambda)$ decreases on

$(0,c_{0}]\cup\bigcup\limits_{m=1}^{\infty}[c_{m-1},c_{m}]=(0,+\infty).$

∎

Recall that
$\psi(\alpha,\lambda)=\sum\limits_{k=0}^{\infty}p_{k}^{\alpha}(\lambda),$
$\alpha>0,$ $\lambda>0.$

######  Theorem 2.

For every $0<\alpha<1$ the function $\psi(\alpha,\lambda)$ strictly increases
as a function of $\lambda$ on $(0,+\infty),$ while for every $\alpha>1$ the
function $\psi(\alpha,\lambda)$ strictly decreases as a function of $\lambda$
on $(0,+\infty).$

###### Proof.

Put $r_{n}(\lambda)=\sum\limits_{k=n+1}^{\infty}q_{k}(\lambda),$ $n\geq 0.$
Note that $r_{n}(\lambda)\to 0$ as $n\to\infty$ as a remainder of a convergent
series. It follows from the proof of Lemma 1 that for every $\lambda>0$ there
exists $N(\lambda)\in\mathbb{N}$ such that
$\bigl{(}q_{0}(\lambda),\ldots,q_{n}(\lambda)\bigr{)}$ is a permutation of
$\bigl{(}p_{0}(\lambda),\ldots,p_{n}(\lambda)\bigr{)}$ for each $n\geq
N(\lambda).$ Hence $q_{n}(\lambda)=p_{n}(\lambda)$ for every $n\geq
N(\lambda).$ Without loss of generality $N(\lambda)\geq 2\lambda.$ Then
$\frac{p_{k+1}(\lambda)}{p_{k}(\lambda)}=\frac{\lambda}{k+1}<\frac{1}{2}$ for
all $k\geq N(\lambda).$ Thus

$r_{n}(\lambda)=\sum\limits_{k=n+1}^{\infty}p_{k}(\lambda)\leq\sum\limits_{k=n+1}^{\infty}\frac{p_{n}(\lambda)}{2^{k-n}}=p_{n}(\lambda)=q_{n}(\lambda),\;n\geq
N(\lambda).$

Fix any $0<\lambda_{1}<\lambda_{2}.$ For every $n\geq
N=\max\\{N(\lambda_{1}),N(\lambda_{2})\\}$ we have

  1. 1)

$q_{0}(\lambda_{i})\geq q_{1}(\lambda_{i})\geq\ldots\geq
q_{n}(\lambda_{i})\geq r_{n}(\lambda_{i}),\;i=1,2,$

  2. 2)

$\sum\limits_{k=0}^{i}q_{k}(\lambda_{1})>\sum\limits_{k=0}^{i}q_{k}(\lambda_{2})\;\text{for}\;0\leq
i\leq n,$ by Lemma 1,

  3. 3)

$\sum\limits_{k=0}^{n}q_{k}(\lambda_{1})+r_{n}(\lambda_{1})=\sum\limits_{k=0}^{n}q_{k}(\lambda_{2})+r_{n}(\lambda_{2})=1,$

i.e.
$\bigl{(}q_{0}(\lambda_{1}),\ldots,q_{n}(\lambda_{1}),r_{n}(\lambda_{1})\bigr{)}$
majorizes
$\bigl{(}q_{0}(\lambda_{2}),\ldots,q_{n}(\lambda_{2}),r_{n}(\lambda_{2})\bigr{)}$
(see Lemma A.2 for the definition of majorization).

For $0<\alpha<1$ the function $x^{\alpha},$ $x\in[0,1],$ is concave, thus by
Karamata’s inequality

$\sum\limits_{k=0}^{n}q_{k}^{\alpha}(\lambda_{1})+r_{n}^{\alpha}(\lambda_{1})\leq\sum\limits_{k=0}^{n}q_{k}^{\alpha}(\lambda_{2})+r_{n}^{\alpha}(\lambda_{2}),\;n\geq
N.$ (5)

Passing to the limit as $n\to\infty,$ we obtain

$\psi(\alpha,\lambda_{1})=\sum\limits_{k=0}^{\infty}q_{k}^{\alpha}(\lambda_{1})\leq\sum\limits_{k=0}^{\infty}q_{k}^{\alpha}(\lambda_{2})=\psi(\alpha,\lambda_{2}),$
(6)

therefore the function $\psi(\alpha,\lambda)$ increases as a function of
$\lambda$ on $(0,+\infty).$

Now we will strengthen inequalities (5) and (6) to ensure that
$\psi(\alpha,\lambda)$ is strictly monotonic as a function of $\lambda.$

Fix $m$ such that $q_{m}(\lambda_{1})>q_{m+1}(\lambda_{1})$ (actually one can
take $m=0$ or $m=1$ because the sequence $\\{q_{k}(\lambda_{1}):k\geq 0\\}$
contains at most two copies of each term). Put
$\widetilde{q}_{m}(\lambda_{1})=q_{m}(\lambda_{1})-\delta,$
$\widetilde{q}_{m+1}(\lambda_{1})=q_{m+1}(\lambda_{1})+\delta,$ where
$\delta>0$ is such that

$\delta\leq\frac{1}{2}\bigl{(}q_{m}(\lambda_{1})-q_{m+1}(\lambda_{1})\bigr{)}\;\text{and}\;\delta<\sum\limits_{k=0}^{m}q_{k}(\lambda_{1})-\sum\limits_{k=0}^{m}q_{k}(\lambda_{2}).$

Note that for every
$n\geq\widetilde{N}=\max\\{N(\lambda_{1}),N(\lambda_{2}),m+1\\}$ conditions
1)–3) above remain valid if $q_{m}(\lambda_{1}),q_{m+1}(\lambda_{1})$ are
replaced with
$\widetilde{q}_{m}(\lambda_{1}),\widetilde{q}_{m+1}(\lambda_{1}).$ Indeed,
only inequalities
$\widetilde{q}_{m}(\lambda_{1})\geq\widetilde{q}_{m+1}(\lambda_{1})$ in 1) and
$\sum\limits_{k=0}^{m-1}q_{k}(\lambda_{1})+\widetilde{q}_{m}(\lambda_{1})>\sum\limits_{k=0}^{m}q_{k}(\lambda_{2})$
in 2) are to be verified anew, and both of them hold by the choice of
$\delta.$ It means that

$\bigl{(}q_{0}(\lambda_{1}),\ldots,q_{m-1}(\lambda_{1}),\widetilde{q}_{m}(\lambda_{1}),\widetilde{q}_{m+1}(\lambda_{1}),q_{m+2}(\lambda_{1}),\ldots,q_{n}(\lambda_{1}),r_{n}(\lambda_{1})\bigr{)}$

majorizes
$\bigl{(}q_{0}(\lambda_{2}),\ldots,q_{n}(\lambda_{2}),r_{n}(\lambda_{2})\bigr{)}.$
Therefore inequalities (5) and (6) remain valid if
$q_{m}(\lambda_{1}),q_{m+1}(\lambda_{1})$ are replaced with
$\widetilde{q}_{m}(\lambda_{1}),\widetilde{q}_{m+1}(\lambda_{1}).$ Thus

$\sum\limits_{k=0}^{\infty}q_{k}^{\alpha}(\lambda_{1})+\widetilde{q}_{m}^{\alpha}(\lambda_{1})+\widetilde{q}_{m+1}^{\alpha}(\lambda_{1})-q_{m}^{\alpha}(\lambda_{1})-q_{m+1}^{\alpha}(\lambda_{1})\leq\sum\limits_{k=0}^{\infty}q_{k}^{\alpha}(\lambda_{2}).$

Since the function $x^{\alpha},$ $x\in[0,1],$ is strictly concave on $[0,1],$
we have

$\widetilde{q}_{m}^{\alpha}(\lambda_{1})+\widetilde{q}_{m+1}^{\alpha}(\lambda_{1})>q_{m}^{\alpha}(\lambda_{1})+q_{m+1}^{\alpha}(\lambda_{1}).$

Hence

$\psi(\alpha,\lambda_{1})=\sum\limits_{k=0}^{\infty}q_{k}^{\alpha}(\lambda_{1})<\sum\limits_{k=0}^{\infty}q_{k}^{\alpha}(\lambda_{2})=\psi(\alpha,\lambda_{2}).$
(7)

For $\alpha>1$ the function $x^{\alpha},$ $x\in[0,1],$ is convex, thus by
Karamata’s inequality inequalities (5), (6) and (7) are reversed. ∎

##  4 By-product inequalities

As can be seen from Section 3, the proof of increasing (decreasing) properties
of function $\psi(\alpha,\lambda)$ did not use differentiation of
$\psi(\alpha,\lambda)$ and the properties of its derivatives. However,
function $\psi(\alpha,\lambda)$ can be differentiated term by term at any
point $\alpha>0$ in $\lambda>0$ and as a result, we shall get after some
elementary transformations that for any $\alpha,\lambda>0$

$\psi^{\prime}_{\lambda}(\alpha,\lambda)=\alpha
e^{-\alpha\lambda}\sum_{k=0}^{\infty}(k-\lambda)\frac{\lambda^{\alpha
k-1}}{(k!)^{\alpha}}.$

Obviously, if $\alpha=1$ then for any $\lambda>0$ the derivative is zero
because it differs by a strictly positive multiplier $\alpha
e^{-\alpha\lambda}$ from the expression

$R(\alpha,\lambda)=\sum_{k=0}^{\infty}(k-\lambda)\frac{\lambda^{\alpha
k-1}}{(k!)^{\alpha}},$

and

$R(1,\lambda)=\sum_{k=1}^{\infty}\frac{\lambda^{k-1}}{(k-1)!}-\sum_{k=0}^{\infty}\frac{\lambda^{k}}{k!}=0.$

However, taking into account Theorem 2, we can establish some nontrivial
inequalities.

######  Lemma 2.

For any $\lambda>0$ and $\alpha\in(0,1)$

$\sum_{k=1}^{\infty}\frac{{\lambda}^{\alpha
k-1}k^{1-\alpha}}{((k-1)!)^{\alpha}}\geq\sum_{k=0}^{\infty}\frac{{\lambda}^{\alpha
k}}{(k!)^{\alpha}},$ (8)

while for any $\lambda>0$ and $\alpha>1$

$\sum_{k=1}^{\infty}\frac{{\lambda}^{\alpha
k-1}k^{1-\alpha}}{((k-1)!)^{\alpha}}\leq\sum_{k=0}^{\infty}\frac{{\lambda}^{\alpha
k}}{(k!)^{\alpha}}.$ (9)

###### Proof.

Both inequalities follow immediately from the fact that $R(\alpha,\lambda)$
and $\psi^{\prime}_{\lambda}(\alpha,\lambda)$ are of the same sign, therefore
it follows from Theorem 2 that $R(\alpha,\lambda)\geq 0$ for all $\lambda>0$
and $\alpha\in(0,1)$ and $R(\alpha,\lambda)\leq 0$ for all $\lambda>0$ and
$\alpha>1$. ∎

######  Remark 1.

The nontrivial character of inequalities (8) and (9) is implied by the fact
that we can not compare the respective series term by term, and the relation
between $k$th terms depends on whether the condition $\lambda>k$ or the
inverse one is satisfied. The similar situation was with
$\psi(\alpha,\lambda)$, but now, having Theorem 2 in hand, we do not need to
analyze the series in more detail in order to compare them.

##  5 Graphical support of results

In this section we present several plots and surfaces illustrating the
behaviour of Rényi entropy as the function of parameters $\alpha$ and
$\lambda.$ Obviously, all of them confirm our theoretical results. First, we
demonstrate the behaviour of the function $\psi(\alpha,\lambda)$ from (4).

Figure 1: $\psi(\alpha_{0},\lambda)$ is an increasing function of $\lambda$
when $\alpha_{0}$ is fixed, $0<\alpha<1$, $\lambda>0$. Figure 2:
$\psi(\alpha,\lambda)$ is an increasing function of $\lambda$, $0<\alpha<1$,
$\lambda>0$. Figure 3: $\psi(\alpha_{0},\lambda)$ is an decreasing function of
$\lambda$ when $\alpha_{0}$ is fixed, $\alpha>1$, $\lambda>0$. Figure 4:
$\psi(\alpha,\lambda)$ is an decreasing function of $\lambda$, $\alpha>1$,
$\lambda>0$.

We see from Fig. 1 that for fixed $\alpha\in(0,1)$ (the values of $\alpha$ are
chosen from $0.1$ to $0.9$ with interval $0.1$) function
$\psi(\alpha,\lambda)$ strictly increases in $\lambda\in(0,+\infty)$. The same
is confirmed by the surface on Fig. 2.

Respectively, we see from Fig. 3 that for fixed $\alpha>1$ (the values of
$\alpha$ are chosen from $1.1$ to $2.0$ with interval $0.1$) function
$\psi(\alpha,\lambda)$ strictly decreases in $\lambda\in(0,+\infty)$. The same
is confirmed by the surface on Fig. 4.

Now, let us illustrate Lemma 2.

Figure 5: $R(\alpha_{0},\lambda)>0$ when $0<\alpha_{0}<1$ is fixed,
$\lambda>0$. Figure 6: $R(\alpha,\lambda)>0$ when $0<\alpha<1$, $\lambda>0$.
Figure 7: $R(\alpha_{0},\lambda)<0$ when $\alpha_{0}>1$ is fixed, $\lambda>0$.
Figure 8: $R(\alpha,\lambda)<0$ when $\alpha>1$, $\lambda>0$.

We see from Fig. 5 that for $\lambda>0$ and $\alpha\in(0,1)$ (the values of
$\alpha$ are chosen from $0.1$ to $0.9$ with interval $0.1$)
$R(\alpha,\lambda)>0$. The same is confirmed by the surface on Fig. 6.

Respectively, we see from Fig. 7 that for $\lambda>0$ and $\alpha>0$ (the
values of $\alpha$ are chosen from $1.1$ to $2.0$ with interval $0.1$)
$R(\alpha,\lambda)<0$. The same is confirmed by the surface on Fig. 8.

##  Appendix A Appendix

######  Lemma 3.

The following relation holds:

$\liminf_{\lambda\to\infty}e^{-\lambda}(\log\lambda)^{-1}\sum_{k=1}^{\infty}\frac{\lambda^{k}\log(k+1)}{k!}\geq
1.$

###### Proof.

It is sufficient to consider $\lambda>4.$ Let us rewrite the sum under the
sign of a limit as follows:

$\displaystyle S(\lambda):$
$\displaystyle=\sum_{k=1}^{\infty}\frac{\lambda^{k}\log(k+1)}{k!}$
$\displaystyle=\sum_{k=1}^{\left[\frac{\lambda}{2}\right]}\frac{\lambda^{k}\log(k+1)}{k!}\leavevmode\nobreak\
+\sum_{k\geq[\frac{\lambda}{2}]+1}\frac{\lambda^{k}\log(k+1)}{k!}$
$\displaystyle=:S_{1}(\lambda)+S_{2}(\lambda),$

where $\left[\frac{\lambda}{2}\right]$ is the floor function of
$\frac{\lambda}{2}$ (i.e. the greater integer less or equal to
$\frac{\lambda}{2}$). Obviously,

$S_{1}(\lambda)\leq\log\left(\left[\frac{\lambda}{2}\right]+1\right)\sum_{k=1}^{[\frac{\lambda}{2}]}\frac{\lambda^{k}}{k!}.$

Moreover, $\frac{\lambda^{k}}{k!}$ increases in
$k=1,\ldots,[\frac{\lambda}{2}].$ Therefore

$S_{1}(\lambda)\leq\log\left(\left[\frac{\lambda}{2}\right]+1\right)\frac{\lambda^{\left[\frac{\lambda}{2}\right]}}{\left[\frac{\lambda}{2}\right]!}\left[\frac{\lambda}{2}\right].$

Now, according to two-sided bounds of factorial, for any $n>1$

$\sqrt{2\pi n}\left(\frac{n}{e}\right)^{n}e^{\frac{1}{12n+1}}<n!<\sqrt{2\pi
n}\left(\frac{n}{e}\right)^{n}e^{\frac{1}{12n}}.$

So, we can bound $e^{-\lambda}(\log\lambda)^{-1}S_{1}(\lambda)$ as
$\lambda\to\infty,$ as follows:

$\displaystyle 0<$ $\displaystyle
e^{-\lambda}(\log\lambda)^{-1}S_{1}(\lambda)\leq\frac{e^{-\lambda}\lambda^{\left[\frac{\lambda}{2}\right]}}{\left[\frac{\lambda}{2}\right]!}\cdot\frac{\log\left(\left[\frac{\lambda}{2}\right]+1\right)}{\log\lambda}\left[\frac{\lambda}{2}\right]$
$\displaystyle\leq$
$\displaystyle\frac{e^{-\lambda}\lambda^{\left[\frac{\lambda}{2}\right]}e^{\left[\frac{\lambda}{2}\right]}\left[\frac{\lambda}{2}\right]}{\sqrt{2\pi}\sqrt{\left[\frac{\lambda}{2}\right]}{\left[\frac{\lambda}{2}\right]}^{\left[\frac{\lambda}{2}\right]}e^{\frac{1}{12\left[\frac{\lambda}{2}\right]+1}}}.$

Now shift the range of the values of $\lambda$ under consideration to
$\lambda>42$ and note that for such $\lambda$ we have the bounds
$\left[\frac{\lambda}{2}\right]\geq\frac{\lambda}{2}-1\geq\frac{\lambda}{2,1}.$
Therefore for $\lambda>42$

$e^{-\lambda}(\log\lambda)^{-1}S_{1}(\lambda)\leq\frac{e^{\left[\frac{\lambda}{2}\right]-\lambda}(2,1)^{\left[\frac{\lambda}{2}\right]}\left[\frac{\lambda}{2}\right]}{\sqrt{2\pi}\sqrt{\left[\frac{\lambda}{2}\right]}e^{\frac{1}{12\left[\frac{\lambda}{2}\right]+1}}}<\frac{\left(\frac{2,1}{e}\right)^{\left[\frac{\lambda}{2}\right]}\sqrt{\left[\frac{\lambda}{2}\right]}}{\sqrt{2\pi}e^{\frac{1}{12\left[\frac{\lambda}{2}\right]+1}}}\xrightarrow[\lambda\to\infty]{}0.$
(10)

Now consider

$e^{-\lambda}(\log\lambda)^{-1}S_{2}(\lambda)\geq
e^{-\lambda}\frac{\sum_{k=\left[\frac{\lambda}{2}\right]+1}^{\infty}\frac{\lambda^{k}}{k!}\log\left(\left[\frac{\lambda}{2}\right]+1\right)}{\log\lambda}.$

Obviously,
$\frac{\log\left(\left[\frac{\lambda}{2}\right]+1\right)}{\log\lambda}\to 1$
as $\lambda\to\infty.$ Therefore

$\liminf_{\lambda\to\infty}e^{-\lambda}(\log\lambda)^{-1}S_{2}(\lambda)\geq\liminf_{\lambda\to\infty}\frac{\sum_{k=\left[\frac{\lambda}{2}\right]+1}^{\infty}\frac{\lambda^{k}}{k!}}{e^{\lambda}}.$
(11)

Obviously, $e^{\lambda}=\sum_{k=0}^{\infty}\frac{\lambda^{k}}{k!},$ while it
follows immediately, that similarly to previous calculations in (10)

$0\leq\liminf_{\lambda\to\infty}\frac{\sum_{k=1}^{\left[\frac{\lambda}{2}\right]}\frac{\lambda^{k}}{k!}}{e^{\lambda}}\leq\limsup_{\lambda\to\infty}\frac{\frac{\lambda^{\left[\frac{\lambda}{2}\right]}}{\left[\frac{\lambda}{2}\right]!}\left[\frac{\lambda}{2}\right]}{e^{\lambda}}\leq\limsup_{\lambda\to\infty}\frac{\left(\frac{2,1}{e}\right)^{\left[\frac{\lambda}{2}\right]}\sqrt{\left[\frac{\lambda}{2}\right]}}{\sqrt{2\pi}e^{\frac{1}{12\left[\frac{\lambda}{2}\right]+1}}}=0.$
(12)

Relation (12) implies that the following limit exists:

$\lim_{\lambda\to\infty}\frac{\sum_{k=\left[\frac{\lambda}{2}\right]+1}^{\infty}\frac{\lambda^{k}}{k!}}{e^{\lambda}}=\lim_{\lambda\to\infty}\frac{e^{\lambda}-\sum_{k=0}^{\left[\frac{\lambda}{2}\right]}\frac{\lambda^{k}}{k!}}{e^{\lambda}}=1.$
(13)

The proof immediately follows from (10), (11) and (13).

∎

######  Lemma 4 (Karamata’s inequality, [10], [12], [15]).

Let $f$ be a convex function on an interval $I\subset\mathbb{R}$ and
$a_{1},\ldots,a_{n},b_{1},\ldots,b_{n}$ be numbers in $I$ such that
$(a_{1},\ldots,a_{n})$ majorizes $(b_{1},\ldots,b_{n}),$ i.e. the following
conditions are fulfilled:__

  1. 1)

$a_{1}\geq a_{2}\geq\ldots\geq a_{n},$ $b_{1}\geq b_{2}\geq\ldots\geq b_{n};$

  2. 2)

$\sum\limits_{k=1}^{i}a_{k}\geq\sum\limits_{k=1}^{i}b_{k}$ for every $1\leq
i\leq n-1;$

  3. 3)

$\sum\limits_{k=1}^{n}a_{k}=\sum\limits_{k=1}^{n}b_{k}.$

Then the inequality
$\sum\limits_{k=1}^{n}f(a_{k})\geq\sum\limits_{k=1}^{n}f(b_{k})$ holds.

If $f$ is a concave function on $I$, the inequality is reversed.

### Acknowledgment.

Yuliya Mishura was supported by The Swedish Foundation for Strategic Research,
grant Nr. UKR22-0017 and the ToppForsk project nr. 274410 of the Research
Council of Norway with title STORM: Stochastics for Time-Space Risk Models. We
would like to thank Prof. Igor Shevchuk for the attention to our work and
useful advices.

## References

  * [1] Jayadev Acharya, Alon Orlitsky, Ananda Theertha Suresh, and Himanshu Tyagi.  Estimating Rényi entropy of discrete distributions.  IEEE Trans. Inform. Theory, 63(1):38–56, 2017.
  * [2] Mohammad Adnan Aladaileh, Mohammed Anbar, Ahmed J. Hintaw, Iznan H. Hasbullah, Abdullah Ahmed Bahashwan, Taief Alaa Al-Amiedy, and Dyala R. Ibrahim.  Effectiveness of an entropy-based approach for detecting low- and high-rate DDoS attacks against the SDN controller: Experimental analysis.  Applied Sciences, 13(2), 2023.
  * [3] Evan Archer, Il Memming Park, and Jonathan W. Pillow.  Bayesian entropy estimation for countable discrete distributions.  J. Mach. Learn. Res., 15:2833–2868, 2014.
  * [4] Filipp Buryak and Yuliya Mishura.  Convexity and robustness of the Rényi entropy.  Mod. Stoch. Theory Appl., 8(3):387–412, 2021.
  * [5] Mahdi Cheraghchi.  Expressions for the entropy of basic discrete distributions.  IEEE Trans. Inform. Theory, 65(7):3999–4009, 2019.
  * [6] Jisa David and Ciza Thomas.  DDoS attack detection using fast entropy approach on flow- based network traffic.  Procedia Computer Science, 50:30–36, 2015.  Big Data, Cloud and Computing Challenges.
  * [7] Ronald J. Evans and J. Boersma.  The entropy of a Poisson distribution (C. Robert Appledorn).  SIAM Review, 30(2):314–317, 1988.
  * [8] Yanjun Han, Jiantao Jiao, and Tsachy Weissman.  Adaptive estimation of Shannon entropy.  In 2015 IEEE International Symposium on Information Theory (ISIT), pages 1372–1376, Hong Kong, China, 2015.
  * [9] Jiantao Jiao, Kartik Venkat, Yanjun Han, and Tsachy Weissman.  Minimax estimation of functionals of discrete distributions.  IEEE Trans. Inform. Theory, 61(5):2835–2885, 2015.
  * [10] Zoran Kadelburg, Dušan Dukić, Milivoje Lukić, and Ivan Matić.  Inequalities of Karamata, Schur and Muirhead, and some applications.  The Teaching of Mathematics, 14:31–45, 2005.
  * [11] Yeliz Karaca, Yu-Dong Zhang, and Khan Muhammad.  Characterizing complexity and self-similarity based on fractal and entropy analyses for stock market forecast modelling.  Expert Systems with Applications, 144:113098, 2020.
  * [12] Jovan Karamata.  Sur une inégalité relative aux fonctions convexes.  Publications de l’Institut mathematique, 1(1):145–147, 1932.
  * [13] Ashwin Lall, Vyas Sekar, Mitsunori Ogihara, Jun Xu, and Hui Zhang.  Data streaming algorithms for estimating entropy of network traffic.  In Proceedings of the Joint International Conference on Measurement and Modeling of Computer Systems, SIGMETRICS ’06/Performance ’06, pages 145–156, New York, NY, USA, 2006. Association for Computing Machinery.
  * [14] Anatoliy Malyarenko, Yuliya Mishura, Kostiantyn Ralchenko, and Yevheniia Anastasiia Rudyk.  Properties of various entropies of Gaussian distribution and comparison of entropies of fractional processes.  Axioms, 12(11), 2023.
  * [15] Albert W. Marshall, Ingram Olkin, and Barry C. Arnold.  Inequalities: theory of majorization and its applications.  Springer Series in Statistics. Springer, New York, second edition, 2011\.
  * [16] Liam Paninski.  Estimation of Entropy and Mutual Information.  Neural Computation, 15(6):1191–1253, 06 2003.
  * [17] Alfréd Rényi.  On measures of entropy and information.  In Proc. 4th Berkeley Sympos. Math. Statist. and Prob., Vol. I: Contributions to the theory of statistics, pages 547–561. Univ. California Press, Berkeley-Los Angeles, Calif., 1960.  Held at the Statistical Laboratory, University of California, June 20–July 30, 1960.
  * [18] Claude Elwood Shannon.  A mathematical theory of communication.  Bell System Tech. J., 27:379–423, 623–656, 1948.
  * [19] Aakanksha Singhal and D.K. Sharma.  Keyword extraction using rényi entropy: a statistical and domain independent method.  In 2021 7th International Conference on Advanced Computing and Communication Systems (ICACCS), volume 1, pages 1970–1975, 2021.
  * [20] Yihong Wu and Pengkun Yang.  Minimax rates of entropy estimation on large alphabets via best polynomial approximation.  IEEE Trans. Inform. Theory, 62(6):3702–3720, 2016.


11institutetext: School of Software, Shanghai Jiao Tong University, Shanghai,
200240, China
11email: {dennis.Chen, minkow, 628628<EMAIL_ADDRESS>
# AC4: Algebraic Computation Checker for Circuit Constraints in Zero Knowledge
Proofs

Hao Chen  Minyu Chen  Ruibang Liu  Guoqiang Li Corresponding author.

###### Abstract

ZKP systems have surged attention and held a fundamental role in contemporary
cryptography. Zk-SNARK protocols dominate the ZKP usage, often implemented
through arithmetic circuit programming paradigm. However, underconstrained or
overconstrained circuits may lead to bugs. Underconstrained circuits refer to
circuits that lack the necessary constraints, resulting in unexpected
solutions in the circuit and causing the verifier to accept a bogus witness.
Overconstrained circuits refer to circuits that are constrained excessively,
resulting in the circuit lacking necessary solutions and causing the verifier
to accept no witness, rendering the circuit meaningless. This paper introduces
a novel approach for pinpointing two distinct types of bugs in ZKP circuits.
The method involves encoding the arithmetic circuit constraints to polynomial
equation systems and solving polynomial equation systems over a finite field
by algebraic computation. The classification of verification results is
refined, greatly enhancing the expressive power of the system. We proposed a
tool, AC4, to represent the implementation of this method. Experiments
demonstrate that AC4 represents a substantial 29% increase in the checked
ratio compared to prior work. Within a solvable range, the checking time of
AC4 has also exhibited noticeable improvement, demonstrating a magnitude
increase compared to previous efforts.

###### Keywords:

zero knowledge proofscircuit
constraintsunderconstrainedoverconstrainedalgebraic computation checker

##  1 Introduction

Zero-knowledge proof (ZKP) systems have long occupied a fundamental position
in contemporary cryptography, ever since their inception [20]. They are
significantly utilized in security-sensitive applications, such as smart
contracts [41], blockchain confidential transactions [41, 21], and digital
currency [46], given their capacity to bolster security and privacy. ZKP
systems’ potency lies in their ability to prove anything that an interactive
proof system can, but without revealing any knowledge [23, 7]. Therefore,
these systems have assumed the role of a potent tool enabling trust and
authentication while safeguarding sensitive information.

Developers often opt for the zero-knowledge succinct noninteractive argument
of knowledge (zk-SNARK) [9] as the protocol for the efficiency of setting up
and proving of building a ZKP system, while also adopting arithmetic circuit
[37] as the programming paradigm due to its ease of programming. Circom, a
domain-specific language, is based on the aforementioned protocol and
programming paradigm. It is capable of converting computational statements
into constraints, which can be used to generate a zk system with snark tools
such as snarkjs. To illustrate, consider the process of declaring a boolean
value in circuit programs. In high-level languages, a boolean value $b$ can be
declared directly. However, in circuit languages such as Circom, a constraint
must be explicitly defined to limit its possible values, such as the
constraint $b\times(b-1)=0$ for $b$. This transformation cannot be
automatically performed by existing compilers or libraries. Thus, developers
are compelled to express the computations with polynomial equations.

The limitation of polynomial constraint systems gives rise to two problems.
The first problem is the underconstrained problem [35], which occurs when
multiple outputs can fulfill the same system of equations with identical input
values. This situation arises when the system of polynomial equations does not
yield a mathematical function on the finite field, rendering the circuit
underconstrained. As a result, malicious users could generate fake witnesses,
deceive the verifier, and potentially steal the cryptocurrency [33, 13]. The
second problem is the overconstrained problem [35], which occurs when no
outputs can satisfy the system of polynomial equations or the constraint
system is inconsistent for a given input. This problem may give rise to a
useless circuit, which in turn opens up the possibility of a denial of service
attack. It is obvious that the underconstrained circuits could bring more
severe results than the overconstrained circuits.

Identifying underconstrained and overconstrained problems can be achieved by
encoding their properties into a logical formula and utilizing a
Satisfiability Modulo Theories (SMT) solver to solve them directly. Picus [35]
is the first work that makes a valuable effort to employ an SMT solver for
investigating the underconstrained cases of ZKP circuits with static program
analysis. However, the overconstrained issue still lacks resolution.
Nevertheless, the efficiency of SMT solvers brings an obstacle to SMT-based
tools when solving large circuits. SMT-based tools struggle to verify
constrained circuits within a limited time, even for linear ones.

To this end, an investigation of the constraints on Circom circuit programs is
carried out. By reconsidering the formalization paradigm, we model
underconstrained and overconstrained problems as algebraic inquiries into
whether a quadratic equations system over a finite field has multiple
solutions. An algebraic approach is a more intuitive and efficient way to
proceed with the realization that the highest degree of the quadratic
equations system of equations not exceeding two. Moreover, to support our
motivation, we analyzed over 100 popular Circom circuit programs and observed
that nearly 70% of them are linear while efficient algorithms exist for
solving linear systems of equations. Therefore, after categorizing constraint
problems into diverse types according to their maximal degree, we employ a
unified arithmetic solution framework to solve them separately.

To summarize, contributions can be elaborated as follows:

  * •

Modeling Circom circuits as polynomial systems over finite fields, we
categorize them and propose specialized methods for each category.

  * •

We develop $\text{AC}^{4}$, a complete and sound tool for verifying circuit
programs with the framework above.

  * •

We evaluate the effectiveness through the solved ratio and solving speed of
circuit programs. Our approach solved 65% of previously unsolved examples, a
29% increase over prior work, and significantly improved solving speed.

##  2 Background

Zk-SNARK, the dominant ZKP protocol in mainstream tools, frequently uses
arithmetic circuits for programming. The verification efforts focus on Circom
circuits, which leverage both zk-SNARK and arithmetic circuits.

Zk-SNARKs. Non-interactive ZKPs, such as zk-SNARKs [8], allow verifiers to be
assured of a statement’s truth without gaining any knowledge beyond its
validity [20]. Blum et al. demonstrated that computational zero-knowledge can
be achieved without interaction by sharing a common random string between the
prover and the verifier [12, 45]. The non-interactive protocol conveys the
proof through a message from the prover to the verifier, ensuring efficiency.
zk-SNARKs reign supreme in zk systems due to lightning-fast verification of
even large programs, using tiny proofs (mere hundreds of bytes) within
milliseconds.

Arithmetic Circuits. Arithmetic circuits, fundamental models for polynomial
computation in complexity theory, process variables/numbers using addition and
multiplication. Conceptually, arithmetic circuits offer a formal method for
understanding the complexity of computing polynomials. Note that all variables
mentioned in arithmetic circuits represent signals in the Circom language.

######  Definition 1 (Arithmetic circuit [42])

An arithmetic circuit $C(\mathcal{X})$ in the variables
$\mathcal{X}=\\{X_{1},\ldots,X_{k}\\}$ over the field $\mathbb{F}$ is a
labelled directed acyclic graph. The inputs are assigned by variables from $X$
or by constants. The internal nodes act as computational operations that add
or multiply to calculate the sum or product of the polynomials on the tails of
incoming edges. The output $X_{out}\in\mathcal{X}$ of a circuit is the
polynomial computed at the output node.

Circom. Circom is a compiler written in Rust [31] for compiling circuits
written in the Circom language, a SNARK-based language that uses arithmetic
circuits as its programming paradigm. The compiler outputs circuit constraints
and all the necessary information for computing different ZK proofs. In
Circom, programmers can define constraints using the operators $===$ for
equality, $<\--$ or $-->$ for signal assignment, and $<==$ or $==>$ for
simultaneous assignment. Constraints in Circom must be in the form of $A\times
B+C=0$, where $A$, $B$, and $C$ are linear combinations of signals. After
compiling circuit to r1cs format and computing the witness with the input,
users can utilize the snarkjs tool to generate and validate a proof for the
specified input. The verifier will receive the proof if the witness is valid,
otherwise, the verifier will reject it.

We address Circom circuit constraint verification by extending arithmetic
circuit definitions with constraints.

######  Definition 2 (Constraint)

A constraint $e$ is a quadratic equation over a finite field $F_{p}$:

$\mathcal{A}\mathcal{X}\times\mathcal{B}\mathcal{X}+\mathcal{C}\mathcal{X}=0$

where $\mathcal{A},\mathcal{B},\mathcal{C}$ are coefficient vectors over
$F_{p}$, $\mathcal{X}$ is a vector of variables over $F_{p}$, and the cross
product $\times$ means the product of 2 scalars $\pmod{p}$.

######  Definition 3 (Arithmetic circuit with constraints)

An arithmetic circuit with constraint with constraints can be defined as a
tuple $\langle C(\mathcal{X}),E\rangle$, where $C(\mathcal{X})$ is an
arithmetic circuit. $\mathcal{X}$ is split into two disjoint sets $K$ and $U$.
$K$ represents known input variables, and $U=T\cup O$ represents unknown
variables including the non-constant variables including temporal variables
$T$ and output variables $O$. $E$ includes all the constraints of the circuit
$C(\mathcal{X})$.

##  3 Problem Statements

Detecting over/underconstrained circuits in Circom boils down to an algebraic
inquiry into the number of solutions for a quadratic equations system over a
finite field. This inherent connection naturally leads us to model Circom
circuits as such systems and leverage algebraic methods for analysis.
Moreover, the design principle of R1CS forces Circom constraints under
quadratic computation, resulting a maximum degree of 2 for the equivalent
equations. Our method follows the classification-and-discussion scheme. Our
strategy categorizes circuits by degree and applies specialized solutions
within each category, leading to significant efficiency and scalability gains.

###  3.1 Constraint Problems

The construction of arithmetic circuits is plagued by two critical challenges:
overconstrained and underconstrained circuits. Programmer-authored circuits,
even from seasoned ZK developers, often bear inadvertently miscalibrated
constraints, leading to these issues. While completely eradicating these
issues remains a persistent hurdle, current approaches fall short of
effectively addressing them. This subsection tackles this double-edged sword
head-on, proposing a novel approach to ensure the construction of robust and
reliable arithmetic circuits.

Overconstrained bugs. As described in the work by Labs et al. [25],
overconstrained circuits are unable to uphold the completeness of zero-
knowledge proof. A Circom program is deemed overconstrained when its
corresponding polynomial constraints are overconstrained, indicating that the
circuit cannot produce any valid outputs regardless of the inputs provided.
This inconsistency in the constraint system for a given input characterizes
the state of being overconstrained. Despite their deceptive simplicity in
concept and the misconception that they are less critical than other types of
attacks, denial of service (DoS) attacks are often underappreciated regarding
their security implications. Notably, DoS attacks require neither high skill
nor deep knowledge,, contributing to their low cost for malicious attackers as
highlighted by Zcash [28].

Underconstrained bugs. Recent studies have discovered that underconstrained
bugs in arithmetic circuits can lead to various security threats, including
the ability for attackers to forge signatures, steal user concurrency, or
create counterfeit crypto-coins. A Circom program is classified as
underconstrained when the corresponding polynomial constraints are also
underconstrained. This condition arises when there exists an input $in$ for
which multiple distinct outputs $out_{1},out_{2},\ldots$ can be produced, and
the circuits $C(in,out_{1}),C(in,out_{2}),\ldots$ are all considered valid. In
essence, an underconstrained circuit program may unintentionally permit the
acceptance of unwanted signals, making it susceptible to exploitation by
malicious entities.

###  3.2 Categories of Elements

In our method, categorizations are necessary to account for the various types
of variables present in arithmetic circuits. Some variables are determined by
external inputs, while others depend on other variables, necessitating the
need to classify them accordingly. Aligning with Circom’s degree-2 limit, it
is pertinent to categorize the variables based on the degree. Furthermore, due
to the computational complexity of verifying certain circuits, we are limited
to providing coarse-grained results, thereby highlighting the importance of
categorizing the outcomes as well.

Category of Variables. The variables in a Circom circuit consist of the input
signals $I$, temporary signals $T$, and output signals $O$. The user provides
the values for $I$, which can be regarded as known values $K$. On the other
hand, the variables in $O\cup T$, whose values are not constant, are regarded
as unknown variables $U$ within the constraints. The key issue of the
constraint problem is identifying the unique characteristics of the $O$
variables.

Category of Equations and Circuits. The constraint $e$ is an algebraic
polynomial equation whose degree is under 2 over a finite field $F$, while the
circuits are a system of algebraic polynomial equations whose degree is under
2 over a finite field, with their generator variables being $U$.

The three types of equations (constraints) to consider are precise linear
equations, $K$-coefficient linear equations, and quadratic equations. A
precise linear equation is defined by having linear generator variables with
constant coefficients. Conversely, a $K$-coefficient linear equation includes
at least one generator variable with a coefficient represented by the known
variables $K$, and none of the generator variables’ coefficients are
represented by the unknown variables $U$. Lastly, a quadratic equation is
distinguished by containing at least one generator variable with a coefficient
represented by the unknown variables $U$.

The system of equations, namely circuits, can be categorized into three types
based on the constraints outlined above: precise linear circuits,
$K$-coefficient circuits, and quadratic circuits. A precise linear circuit
consists solely of precise linear equations, while a $K$-coefficient circuit
must contain at least one $K$-coefficient linear equation and no quadratic
equations. Finally, a quadratic circuit should include at least one quadratic
equation.

Category of Results. As shown in Fig. 1, $\text{AC}^{4}$ yields six result
types: algebraic overconstrained, precisely overconstrained, algebraic
exactconstrained, precisely exactconstrained, precisely underconstrained, and
unknown. The algebraic overconstrained and algebraic exactconstrained results
are collectively referred to as algebraically solved results, while precisely
overconstrained and precisely exactconstrained results are collectively
referred to as precisely solved results.

The verification problem is refined to create a more detailed classification
system for the output, based on constraints safety metrics. As for the unknown
cases that are not fully solved by the solver, they are categorized into two
intermediate cases separated by constraint stress. The two intermediate cases,
algebraically exact constrained and algebraically over constrained, provided
more detailed information for analysis. Besides this category, this method
unlocks partial information about unsolvable circuits and speeds things up.

Fig. 1 also provides a cross-reference between our result category and the
typical ground truth of constraints. Among those 5 practical output types
except unknown 3 precise categories of them: precisely underconstrained,
precisely exactconstrained, and precisely overconstrained, strictly maps into
the underconstrained, exactconstrained, overconstrained respectively. The 2
medium status algebraic exactconstrained and algebraic overconstrained, caused
by potential reduced-rank phenomenon while simplifying the equation matrix in
some cases. Our approach cannot ascertain equation system solution counts,
reflected in matrix rank. Cases labeled with algebraic exactconstrained may
lie in underconstrained or exactconstrained of ground truth, while cases
labeled with algebraic overconstrained occur in exactconstrained or
overconstrained.

Algebraically overconstrained indicates no algebraic solutions, but special
inputs can shift results to exactconstrained or underconstrained. The circuit
is algebraically exactconstrained, indicating it has exactly one solution
algebraically. However, Special inputs can trigger underconstrained states.

Unknown results may stem from circuit size, computational complexity, or the
inherent NP-hardness of solving quadratic equations over finite fields.

By combining the algebraic exactconstrained and precisely exactconstrained
into a synthesized state, namely general exactconstrained, cases in this state
are never overconstrained, though they could fall in underconstrained.
Similarly, the general overconstrained state provides a guarantee for cases to
avoid underconstrained state. We introduce a relaxed constraint property
metric that efficiently filters out under/overconstrained cases.

Figure 1: The category of results from AC4.

###  3.3 Problem Reduction

This section demonstrates the reduction of the under/overconstrained problems
of a circuit to the number of solutions of the corresponding polynomial
equations.

######  Definition 4 (Polynomials over finite fields)

For a finite field $\mathbb{F}$ and formal variables $X_{1},\ldots,X_{k}$,
$\mathbb{F}[X_{1},\ldots,X_{k}]$ denotes the set of polynomials in
$X_{1},\ldots,X_{k}$ with coefficients in $\mathbb{F}$. By taking the
variables to be in $\mathbb{F}$, a polynomial
$f\in\mathbb{F}[X_{1},\ldots,X_{k}]$ can be viewed as a function from
$\mathbb{F}^{k}\rightarrow\mathbb{F}$.

To reduce the circuit constraint problems to the number of solutions of
polynomials, we have the following proposition:

######  Proposition 1 (Circuit-Poly Reduction)

For each circuit $A=\langle C(X),e\rangle\in\langle C(\mathcal{X}),E\rangle$,
there exists $A^{\prime}\in\mathbb{F}[X_{1},\ldots,X_{k}]$, such that
$A^{\prime}=\mathbb{M}(A)$ , where $\mathbb{M}$ is a bijection function from a
circuit to polynomials over finite fields.

A bijection can be constructed between the formal variables of polynomials and
the variables of a circuit because their domain is the same finite field
$\mathbb{F}$. The meta operator set $O_{c}$ of Circom circuits is
$\\{+,\times,\sim\\}$ 111$\sim$ is the complementary operation on finite
fields and the meta operator set $O_{p}$ of a polynomials are
$\\{+,\times,\sim\\}$, so $O_{c}=O_{p}$. Because the additive group over
finite fields is an Abelian group under ‘+’, the operation of shifting the
terms does not change the properties of the original variables and
constraints. However, a constraint of a Circom circuit can only be constant,
linear, or quadratic, while polynomials exceed the limit of the degree of
variables. Consequently, the constraints of a Circom circuit are a true subset
of polynomials.

Based on the argument above, completely checking the constraint status of
circuits can be achieved by solving polynomials. More concretely, the
constraint problem corresponds to figuring out the number of solutions for
polynomials.

##  4 Methodology

###  4.1 AC4 Framework

Fig. 2 illustrates the overall workflow of our proposed tool, $\text{AC}^{4}$,
which receives a Circom program file as the input, and compiles the program in
debug mode into an R1CS format file along with a sym file. To retrieve the
variables and constraints from the compiled files, a task-specific parser is
implemented to handle those compiled files, focusing on unknown variables
within constraints. After that, the extracted constraints are then simplified
into equations. A categorizing mechanism is leveraged in Section 3.2 to
determine the specific category of the circuit according to its simplified
equation system. Based on the category result of circuits, three types of
solvers is employed to address them respectively.

Figure 2: The framework of AC4.

In the context of a precisely pure linear circuit, the system of linear
equations can be represented in matrix form. While it may seem natural to rely
on rank to determine the number of solutions, it is more important to
prioritize verifying the uniqueness of the output variable set. Therefore,
solving the system demands a suitable method for linear equations.
Specifically, in $\text{AC}^{4}$, the Gauss-Jordan method is utilized to
obtain the solution of the circuits as well as to ascertain the uniqueness of
the set of output variables.

The system of $K$-coefficient linear equations corresponding to an
algebraically linear circuit can be represented in matrix form. However, it is
imperative to note that algebraic computation does not inherently account for
the division by zero problem. Consequently, for certain specific inputs $I$,
the rank of the matrix may decrease, potentially altering the outcome of
$\text{AC}^{4}$. Rank reduction risks are mitigated by strategically
identifying and treating special input cases. Our approach addresses this
challenge through heuristic approaches to improve the efficiency and
accuracyc.

For quadratic circuits, we solve the coefficients and verify if the circuit
will be underconstrained with specific inputs. Then, we use $\text{AC}^{4}$ to
directly solve the systems of quadratic equations and check the uniqueness of
the output variables.

Here, an example will be used to demonstrate our workflow and enhance readers’
comprehension. The template in Fig. 3 refers to the Circom circuit Decoder,
which converts a w-ary number into a one-hot encoded format.

⬇

1template Decoder(w) {

signal input inp;

3 signal output out[w], success;

var lc=0;

5 for (var i=0; i < w; i++) {

out[i] <– (inp == i) ? 1 : 0;

7 out[i] * (inp-i) === 0;

lc = lc + out[i];}

9 lc ==> success;

success * (success -1) === 0;

11}

component main = Decoder(2);

Figure 3: Decoder(2)

Upon setting $w=2$, the Decoder(2) emerges as a 2-bit decoder. This circuit is
then transformed into a format denoted as $C(K,U,O,E$, where the sets are
defined as follows: $K=\\{inp\\}$, $U=\\{out_{1},out_{2},success\\}$,
$O=\\{out_{1},out_{2},success\\}$, and $E=\\{out_{0}\times
inp=0,out_{1}\times(inp-1)=0,success\times(success-1)=0\\}$.

Based on the classification of circuits mentioned above, it is evident that
this circuit is quadratic. We begin by treating the variable $inp$ as a
coefficient and proceed to solve the undetermined coefficients of each
equation. This process yields the solutions $[\\{inp=0\\},\\{inp=1\\}]$. Upon
substituting $\\{inp=0\\}$ into $E$, it results in
$E=\\{0=0,out_{1}\times(inp-1)=0,success\times(success-1)=0\\}$. Notably, it
is evident that the $out_{0}$ can take on any value over the finite field,
signifying that the circuit is underconstrained.

###  4.2 Checking Circuits: Category-Based Algorithms

From above, we divide the overall circuit verification problem space into
three types: precisely linear, $k$-coefficient linear, and quadratic
separately. In this section, we introduce those algorithms in detail.

Precisely linear.  The majority of circuits are precisely linear, so they can
be represented by a coefficient matrix $A$ and a constant vector $b$. While it
is commonly thought to use the rank of the equation matrix to determine the
number of solutions, the solver’s objective is actually only to verify the
uniqueness of output variables. In contrast, rank-reducing methods impose
restrictions on the uniqueness of all variables, including temporary
variables. Using the Gauss-Jordan method to get the rank of the corresponding
matrix is analogous to getting the solution of the system of equations.
Consequently, there is no significant difference in the time complexity.

Qudratic. A heuristic approach will be used to identify input variables that
may cause the circuit to become underconstrained, aiming to improve accuracy
and efficiency. The coefficients of the unknown variables are treated as
equations and their solutions will be stored in a frequency table for counting
the occurrences of each solution. Then, the solver sorts the solutions based
on their frequencies and iteratively substitutes them into the original system
of equations to obtain a new system, which is then solved to check if the
circuit is underconstrained. If the input variable causing the circuit to
become underconstrained cannot be identified, the system of equations will be
directly solved to verify the constrained situation of the circuit.

$K$-coefficient linear. Although quadratic in nature, these equations are
considered linear due to their quadratic terms containing one or more known
variables, Hence, they are treated as linear circuits and represented in
matrix form to enhance verification efficiency. For these circuits, we still
use the previous heuristic approach to determine if there are special inputs
that can cause the underconstrained condition, aiming to enhance efficiency.
Afterwards, a $k$-coefficient linear circuit can be succinctly represented by
a coefficient matrix $A$ and a constant vector $b$, and checked as a linear
case.

###  4.3 Complexity Analysis

This section discusses the time complexity of each category. First, for linear
or part of $K$-coefficient linear circuits, the Gauss-Jordan solution yields a
complexity of $O(n^{3})$ [2]. As we discovered that the majority of cases are
precisely linear circuits based on a statistical analysis of the Circomlib
[22], We expect our algebraic-based method to introduce a large improvement in
performance compared with SMT solvers, as SMT solvers tend to convert
constraints into Conjunctive Normal Form (CNF) which ignores potential
mathematical transformation and simplification within equation systems. When
considering a quadratic equations system over a finite domain, the time
complexity is proven to be NP-hard [16]. Even with complex cases, quadratic
solvers offer a practical approach.

###  4.4 Optimization and Implementation

Pre-implementation. Before solving the equations, it is crucial to first
examine whether there are any output variables that are not present in any
constraint, as the presence of such a variable indicates that the circuit is
underconstrained. Once identified, these variables can then be addressed
appropriately. Furthermore, it is important to note the existence of equations
with no unknown terms. These equations should be filtered out as they do not
contribute to the determination of the output variables’ uniqueness. In
addition, it is necessary to carefully assess the type of each equation to
establish the type of the circuit being analyzed ultimately. Moreover, in
scenarios involving $k$-coefficients, it is possible for the result to be
algebraically overconstrained, thereby requiring a methodical approach to
narrow down its range. To achieve this, the first step involves checking for
linear input variables and treating them as unknown in order to attain more
accurate solutions. This systematic process enhances the precision and
reliability of the solutions obtained.

Binary Optimization. We improved the efficiency of checking the binary
circuits by first encoding them into binary format over a finite field. Then,
we implemented a detector to verify whether a quadratic circuit is a binary
circuit by ensuring that all unknown variables adhere to the form
$u\times(u-1)=0$. This binary checking process was employed to validate the
circuits further.

##  5 Evaluations

Environment configuration. The evaluations were performed on a machine with a
16-core AMD Ryzen 9 5950x processor and 128GB of DRAM.

Check Benchmark. We settle a representative benchmark to evaluate the
effectiveness and accuracy of $\text{AC}^{4}$ and Picus [35]. The benchmark
was based on the data set provided by $\text{AC}^{4}$ and Picus, which had
been collected from Circomlib, the standard library from Circom. All cases of
our benchmark were divided into two parts: Circomlib-utils benchmarks, which
was extracted from the Circomlib utils library and had a smaller size, and
Circomlib-core benchmarks, which was extracted from the Circomlib core library
and had a larger size [35].

###  5.1 The Conditions of the Data Set

The size condition Table 1 presents the size condition of the benchmark set.
Notably, within the benchmark set Core, there are three circuits with over
200,000 constraints, which are believed to be unsolvable using standard
computers. Interestingly, in these three cases, only Sha256compression results
in an out-of-memory exception due to the presence of around 20,000 unknown
variables, resulting in the creation of a very large matrix. In contrast, the
other two cases each have only one known variable, making the circuits easier
to check.

Table 1: The size condition of the benchmark sets

Benchmark set | # of circuits | Avg. # of expr_num | Avg. # of unknown_num | Avg. # of out_num
---|---|---|---|---
utils | 66 | 1992 | 12 | 9
core | 110 | 6941 | 200 | 30
total | 176 | 5085 | 130 | 22

We categorize circuits based on their constraint numbers in Table 2,
considering those with a constraint number less than 100 as ”small” circuits,
those with a constraint number in the range $[100,1000)$ as ”medium” circuits,
and those with a constraint number in the range $[1000,\infty)$ as ”large”
circuits. This classification, which may be rudimentary, does not consider
output signals. It is evident that small circuits can be solved directly,
whereas other circuits may require specific restrictions to be solved within
an acceptable time frame.

Table 2: The size category condition of the circuits Benchmark set | utils | core | total
---|---|---|---
small | 49 | 63 | 112
medium | 8 | 24 | 32
large | 9 | 23 | 32

The type condition As shown in the table 4, The benchmark set comprises 176
circuits, distributed as 71.6% precisely linear, 6.2% $K$-coefficient linear,
and 22.2% quadratic, mirroring the range of circuit types encountered in real-
world applications. Upon further examination of the $K$-coefficient and
quadratic cases, it becomes evident that a significant portion of them are
binary circuits associated with cryptographic algorithms. Instead of
exhaustive arithmetic solutions, focusing on binary optimization strategies
offers promising efficiency gains in checking these circuits. For instance,
the circuit Num2BitsNeg@bitify_256 is a quadratic circuit designed to convert
an integer over a finite field into a 256 bit-vector, with all its unknown
variables constrained by $o\times(o-1)=0$, indicating that they are strictly
bits with their value limited to 0 or 1. Appropriately identifying these
circuits and applying binary methods for solving them represents a more
efficient approach compared to arithmetic methods.

###  5.2 Benchmark Metrics

Checked Ratio. The solved benchmarks are initially categorized into three
types: precisely solved, algebraically solved, and unknown. The precisely
solved cases are further categorized into three types: precisely
exactconstrained, which means that the circuit is safe; precisely
overconstrained, indicating that the circuit is overconstrained; and precisely
underconstrained, which suggests that the circuit is underconstrained. We omit
this metric as $PS$ (Precisely Solved).

On the other hand, we propose a more relaxed metric, $AS$ (Algebraic Solved),
by remapping cases that failed to obtain precise results into two new
categories: algebraic exactconstrained and algebraic overconstrained as
introduced in Section 3.2, to reject overconstrained and underconstrained
respectively. Note that $\text{AC}^{4}$ still returns unknown for extremely
computationally exhausting cases.

Checking time. In this metric, our emphasis lies on the benchmark data on the
parts that both $\text{AC}^{4}$ and Picus can solve, and then proceed to
compare the checking time of the two tools.

###  5.3 Benchmark Results

Checking Time The checking time of the benchmark set is presented in Table 3,
with a focus on the relationship between benchmark size and solving
difficulty. It is observed that the larger benchmarks present greater
difficulty in solving, resulting in longer solution times. However, in some
large circuits, despite a high number of constraints, the number of output
signals is limited to 1, allowing for a relatively easy check once the file
read operation concludes. Nonetheless, there exist extremely large circuits
that are characterized by a linear type, yet their extensive constraint size
renders the Gaussian-Jordan method challenging to execute, leading to out-of-
memory issues. Conversely, smaller cases are relatively straightforward to
solve directly but due to limitations, the precise solution is not attainable,
resulting in algebraic outcomes.

Fortunately, the majority of practical Circom circuits are of the precisely
linear type. This characteristic is advantageous because medium or large
circuits that are not precisely linear cannot be solved directly due to
unknown outcomes. Therefore, alternative methods must be utilized to bypass
the direct solution of non-linear circuits. Additionally, providing a more
accurate range to determine whether to solve the circuits can help avoid
obtaining algebraically solved results. This approach is crucial for
maintaining clarity and precision in circuit analysis.

Table 3: The efficiency benchmark of $AC^{4}$ is categorized by size and
includes the time for precisely solved and algebraically solved results. The
terms $K,U,O,v,PS,AS$ represent known, unknown, output, variables, precisely
solved, and algebraically solved, respectively. The explanation of $PS,AS$ is
discussed in Section 5.2.

Benchmark | Utils | Core | overall
---|---|---|---
Size | small | medium | large | overall | small | medium | large | overall
Avg. # variable | K | 15 | 424 | 14309 | 2014 | 36 | 435 | 24984 | 5159 | 3973
U | 4 | 18 | 58 | 13 | 11 | 78 | 26 | 29 | 23
O | 2 | 2 | 57 | 9 | 10 | 78 | 26 | 29 | 21
total v | 18 | 442 | 14366 | 2026 | 47 | 512 | 25010 | 5188 | 3995
constraints | 14 | 244 | 14230 | 1993 | 17 | 474 | 24923 | 5144 | 3956
Avg. PS Time(s) | 0.57 | 0.52 | 9.06 | 1.83 | 0.42 | 2.4 | 14.59 | 3.71 | 3.03
Avg. AS&PS Time(s) | 1.26 | 2.45 | 8.33 | 2.41 | 0.40 | 2.4 | 13.47 | 3.48 | 3.06

Checked Ratio. The checked ratio of the benchmark sets categorized by circuit
type is presented in Table 4. The data indicates a significantly high solved
ratio for precisely linear circuits. However, Substantial constraints in
circuits result in very large augmented matrices. As a consequence, the solve
ratio of $k-$coefficient circuits is relatively low. This is attributed to the
adoption of an algebraic strategy for $k-$coefficient circuits, which in turn
leads to the direct solving of small-size $k-$coefficient circuits without
returning a precise result.

Heuristic algorithms initially assess potential underconstraint in quadratic
circuits. We then apply classic algorithms for solving quadratic equations
over finite fields to obtain direct solutions. Moreover, in the case of
specific binary circuits such as BinSum and Num2Bits, a detection method is
utilized to verify the boolean nature of unknown variables. Upon confirmation,
a specialized method for solving binary circuits is employed in lieu of
arithmetic-based approaches. Most circuits are thoroughly verified before
processing.

Table 4: Main Experiment results, we categorize circuits based on their types: pl means precisely linear type, kcl means k coefficient linear, q means quadratic, ps means precisely solved, as means algebraically solved. Benchmark | Utils | Core | overall
---|---|---|---
type | pl | kcl | q | overall | pl | kcl | q | overall
ps_num | 45 | 3 | 7 | 55 | 75 | 3 | 23 | 101 | 156
as_num | 3 | 3 | 5 | 11 | 2 | 2 | 4 | 8 | 19
total_num | 48 | 6 | 12 | 66 | 77 | 5 | 27 | 109 | 175
ps_rat | 94% | 60% | 58% | 83% | 96% | 60% | 85% | 91% | 89%
ps&as_rat | 100% | 100% | 100% | 100% | 98% | 100% | 100% | 99% | 99%

###  5.4 Comparison with Baseline

In the paper [35], Picus, an implementation of the tool $\textbf{QED}^{2}$, is
utilized for verifying the uniqueness property (under-constrained signals) of
ZKP circuits. This implementation employs static program analysis and SMT
solvers checking to achieve the verification of the uniqueness of ZKP
circuits. Subsequently, we benchmarked the Picus program using the same
benchmark set.

The completed Picus ratio for the utils benchmark set is 80.33%, for the core
benchmark set it is 62.61%, and for both sets it is 69.36%. Additionally, the
average solving time for the Picus solver is 425.73 seconds for the utils
benchmark set, 317.88 seconds for the core benchmark set, and 365.52 seconds
for both sets.

(a) Comparison between the checking time of $\text{AC}^{4}$ and Picus.

(b) Comparison between checked ratio of $\text{AC}^{4}$ and Picus

Figure 4: The checking time and checked ratio comparisons between
$\text{AC}^{4}$ and Picus

The comparison of the two tools based on the solved ratio can be found in Fig.
4b. Our advantage lies in precisely linear cases as well as some heuristic
methods for $k-$coefficient and binary cases.

Fig. 4b shows the solving time comparison of the two tools. Our advantage lies
in solving problems arithmetically rather than encoding them into SMT
formulas, making our tools much faster.

###  5.5 Analysis

Table 3 illustrates a significant correlation between the size of the circuit
and the time required for checking. Despite their size, large circuits keep
checking times low due to two critical factors. Firstly, the predominance of
linear circuits, efficiently addressed by the Gauss-Jordan solver, contributes
to the efficiency in solving a majority of cases. Additionally, optimizations
targeting binary cases within k-coefficient and quadratic circuits serve to
further reduce the solving time despite their slightly larger size.

The checked ratio is high for precisely linear cases; however, there are some
cases for which we cannot provide precisely checked results due to the lack of
an algebraic solution. Special input scenarios can reduce the augmented
matrix’s rank, yielding a solution. In contrast, for the $K$-coefficient
cases, the checked ratio is relatively low, even when a mixed solver is
employed. This is because we did not implement certain static analysis methods
to elaborate the benchmark set, which would have facilitated the checking of
circuits. Conversely, the checked ratio is relatively high for quadratic
cases, as most of these cases are in binary form. The detection method and
optimization for binary quadratic circuits have significantly enhanced
efficiency in checking these cases.

AS Analysis. We point out that the cases that occur in the AS metric are worth
discussing. In Core data split, cases that cannot be precisely solved consist
of nearly 7% of the total amount, while this number increases to 17% in Utils
data split. Our proposed AS mechanism enables our tool to investigate more
detailed situations of constraints. By excluding an incorrect option among
underconstrained and overconstrained, we narrow the possible status of these
cases. Experimental results demonstrate that our tool offers valuable hints to
almost 100% cases in both Core and Utils splits.

Failure Analysis. Picus utilized their algorithm Uniqueness Constraint
Propagation to solve all the $k-$coefficient circuits. The algorithm
simplifies verification/resolution by strategically assigning values to
unknown variables through partial equation analysis, reducing unknowns.
However, our methods forgo static analysis, limiting $K$-coefficient case
checking.

##  6 Related Work

Verification on ZK programs. Circomspect [11] serves as a static analyzer and
linter designed for the Circom programming language. Picus [35] employs a
static analysis method combined with an SMT solver. Circomspect and Picus
share certain similarities with our work. However, Circomspect can only
annotate a portion of underconstrained variables. Picus is immune to this
issue but remains a low efficiency due to the extensive use of the SMT solver.

ZK circuit formalization has seen notable advancements: Shi et al. [39]
proposed a data-flow-based algorithm for R1CS standardization, to enhance
performance across R1CS tasks. Wen et al. [44] formalized and classified
Circom vulnerabilities, introducing a CDG-based static analysis framework.
CODA [27] emerged as a statically typed language for formal ZK system property
specification and verification. Soureshjani et al.[40] applied abstract
interpretation to examine Halo2 circuit properties, on the Plonkish matrix
using an SMT solver.

Research on ZK compilers with theorem proving is ongoing. Bangerter and
Almeida et al.[5, 4, 1, 6], pioneered verifiable compilation using
Isabelle/HOL [34]. PinocchioQ [19] verified Pinocchio[36], a C-based zk-SNARK,
with Compcert [26] based on Coq [10]. Chin and Coglio et al [14, 15]. employed
ACL2 [24] on Leo, while Bailey et al. [3] established formal proofs for six
zk-SNARK constructions using the Lean theorem prover [32].

Algebra computation in circuit verification. Algebraic computation is a long-
standing but niche endeavor in verification. Watanabe [43] utilize Gröbner
Basis [18, 17] and polynomial reduction techniques to verify arithmetic
circuits in computing and signal processing systems. Lv et al. [30, 29] used a
computer-algebra-based approach for the formal verification of hardware.
Scholl et al. [38] combined Computer Algebra with Boolean SAT solver to verify
divider circuits.

However, we emphasize that most of the work in this field actively reduces
program or hardware problems to algebra. To the best of our knowledge, we are
the inaugural contributors to the application of algebraic methods in ZKPs.

##  7 Conclusion

We developed an algebraic computation technique to detect zero-knowledge bugs
in arithmetic circuits, addressing under/overconstrained issues. It leverages
arithmetic computations for efficiency, surpasses SMT-based methods, and
incorporates heuristics for enhanced verification. Our implementation,
$\text{AC}^{4}$, successfully verified 89% of 176 Circom circuits in our
evaluation.

## References

  * [1] Almeida, J.B., Bangerter, E., Barbosa, M., Krenn, S., Sadeghi, A.R., Schneider, T.: A certifying compiler for zero-knowledge proofs of knowledge based on $\sigma$-protocols. In: Computer Security – ESORICS 2010. pp. 151–167. Springer Berlin Heidelberg, Berlin, Heidelberg (2010)
  * [2] Andrén, D., Hellström, L., Markström, K.: On the complexity of matrix reduction over finite fields. Advances in Applied Mathematics 39(4), 428–452 (2007). https://doi.org/https://doi.org/10.1016/j.aam.2006.08.008, https://www.sciencedirect.com/science/article/pii/S0196885807000711
  * [3] Bailey, B., Miller, A.: Formalizing soundness proofs of snarks. Cryptology ePrint Archive, Paper 2023/656 (2023), https://eprint.iacr.org/2023/656, https://eprint.iacr.org/2023/656
  * [4] Bangerter, E., Briner, T., Henecka, W., Krenn, S., Sadeghi, A.R., Schneider, T.: Automatic generation of sigma-protocols. In: Public Key Infrastructures, Services and Applications. pp. 67–82. Springer Berlin Heidelberg, Berlin, Heidelberg (2010)
  * [5] Bangerter, E., Camenisch, J., Krenn, S., Sadeghi, A.R., Schneider, T.: Automatic generation of sound zero-knowledge protocols. Cryptology ePrint Archive, Paper 2008/471 (2008), https://eprint.iacr.org/2008/471, https://eprint.iacr.org/2008/471
  * [6] Bangerter, E., Krenn, S., Sadeghi, A.R., Schneider, T., Tsay, J.K.: On the design and implementation of efficient zero-knowledge proofs of knowledge. Software Performance Enhancements for Encryption and Decryption and Cryptographic Compilers–SPEED-CC 9, 12–13 (2009)
  * [7] Ben-Or, M., Goldreich, O., Goldwasser, S., Håstad, J., Kilian, J., Micali, S., Rogaway, P.: Everything provable is provable in zero-knowledge. In: Advances in Cryptology — CRYPTO’ 88. pp. 37–56. Springer New York, New York, NY (1990)
  * [8] Ben Sasson, E., Chiesa, A., Garman, C., Green, M., Miers, I., Tromer, E., Virza, M.: Zerocash: Decentralized anonymous payments from bitcoin. In: 2014 IEEE Symposium on Security and Privacy. pp. 459–474. IEEE, San Jose, California at The Fairmont (2014). https://doi.org/10.1109/SP.2014.36
  * [9] Ben-Sasson, E., Chiesa, A., Tromer, E., Virza, M.: Succinct Non-Interactive zero knowledge for a von neumann architecture. In: 23rd USENIX Security Symposium (USENIX Security 14). pp. 781–796. USENIX Association, San Diego, CA (Aug 2014), https://www.usenix.org/conference/usenixsecurity14/technical-sessions/presentation/ben-sasson
  * [10] Bertot, Y., Castéran, P.: Interactive Theorem Proving and Program Development: Coq’Art: The Calculus of Inductive Constructions, pp. 43–72. Springer Berlin Heidelberg, Berlin, Heidelberg (2004). https://doi.org/10.1007/978-3-662-07964-5
  * [11] of Bits, T.: Circomspect (2023), https://github.com/trailofbits/circomspect
  * [12] Blum, M., Feldman, P., Micali, S.: Non-interactive zero-knowledge and its applications. In: Proceedings of the Twentieth Annual ACM Symposium on Theory of Computing. p. 103–112. STOC ’88, Association for Computing Machinery, New York, NY, USA (1988). https://doi.org/10.1145/62212.62222, https://doi.org/10.1145/62212.62222
  * [13] Cash, T.: Tornado.cash got hacked. by us. (2019), https://tornado-cash.medium.com/tornado-cash-got-hacked-by-us-b1e012a3c9a8
  * [14] Coglio, A., McCarthy, E., Smith, E., Chin, C., Gaddamadugu, P., Dellepere, M.: Compositional formal verification of zero-knowledge circuits. Cryptology ePrint Archive, Paper 2023/1278 (2023), https://eprint.iacr.org/2023/1278, https://eprint.iacr.org/2023/1278
  * [15] Coglio, A., McCarthy, E., Smith, E.W.: Formal verification of zero-knowledge circuits. Electronic Proceedings in Theoretical Computer Science 393, 94–112 (Nov 2023). https://doi.org/10.4204/eptcs.393.9, http://dx.doi.org/10.4204/EPTCS.393.9
  * [16] Dvijotham, K.: Systems of quadratic equations: Efficient solution algorithms and conditions for solvability. In: 2015 53rd Annual Allerton Conference on Communication, Control, and Computing (Allerton). pp. 1027–1031. IEEE, Monticello, IL, USA (2015). https://doi.org/10.1109/ALLERTON.2015.7447121
  * [17] Faugère, J.C.: A new efficient algorithm for computing gröbner bases without reduction to zero (f5). In: Proceedings of the 2002 International Symposium on Symbolic and Algebraic Computation. p. 75–83. ISSAC ’02, Association for Computing Machinery, New York, NY, USA (2002). https://doi.org/10.1145/780506.780516, https://doi.org/10.1145/780506.780516
  * [18] Faugére, J.C.: A new efficient algorithm for computing gröbner bases (f4). Journal of Pure and Applied Algebra 139(1), 61–88 (1999). https://doi.org/https://doi.org/10.1016/S0022-4049(99)00005-5, https://www.sciencedirect.com/science/article/pii/S0022404999000055
  * [19] Fournet, C., Keller, C., Laporte, V.: A certified compiler for verifiable computing. In: 2016 IEEE 29th Computer Security Foundations Symposium (CSF). pp. 268–280. IEEE, Lisboa, PORTUGAL (2016). https://doi.org/10.1109/CSF.2016.26
  * [20] Goldwasser, S., Micali, S., Rackoff, C.: The knowledge complexity of interactive proof-systems. In: Proceedings of the Seventeenth Annual ACM Symposium on Theory of Computing. p. 291–304. STOC ’85, Association for Computing Machinery, New York, NY, USA (1985). https://doi.org/10.1145/22145.22178, https://doi.org/10.1145/22145.22178
  * [21] Groth, J., Kohlweiss, M.: One-out-of-many proofs: Or how to leak a secret and spend a coin. In: Oswald, E., Fischlin, M. (eds.) Advances in Cryptology - EUROCRYPT 2015. pp. 253–280. Springer Berlin Heidelberg, Berlin, Heidelberg (2015)
  * [22] Iden3: Circomlib: Library of basic circuits for circom (2022), https://github.com/iden3/circomlib
  * [23] Impagliazzo, R., Yung, M.: Direct minimum-knowledge computations (extended abstract). In: Advances in Cryptology — CRYPTO ’87. pp. 40–51. Springer Berlin Heidelberg, Berlin, Heidelberg (1988)
  * [24] Kaufmann, M., Moore, J.: An industrial strength theorem prover for a logic based on common lisp. IEEE Transactions on Software Engineering 23(4), 203–213 (1997). https://doi.org/10.1109/32.588534
  * [25] Labs, N.C.: Security Concerns for Zero-Knowledge Proofs in Blockchain: A Comprehensive Guide by Numen Cyber (2023)
  * [26] Leroy, X.: Formal certification of a compiler back-end or: Programming a compiler with a proof assistant. In: Conference record of the 33rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. p. 42–54. POPL ’06, Association for Computing Machinery, New York, NY, USA (2006). https://doi.org/10.1145/1111037.1111042, https://doi.org/10.1145/1111037.1111042
  * [27] Liu, J., Kretz, I., Liu, H., Tan, B., Wang, J., Sun, Y., Pearson, L., Miltner, A., Dillig, I., Feng, Y.: Certifying zero-knowledge circuits with refinement types. Cryptology ePrint Archive, Paper 2023/547 (2023), https://eprint.iacr.org/2023/547, https://eprint.iacr.org/2023/547
  * [28] Lucian, A.: Zcash Denial-Of-Service Attack Costs Just $2.89 per Day - BeInCrypto (2019), https://beincrypto.com/zcash-denial-of-service-attack-costs-just-2-89-per-day/
  * [29] Lv, J., Kalla, P.: Formal verification of galois field multipliers using computer algebra techniques. In: 2012 25th International Conference on VLSI Design. pp. 388–393. IEEE, Hyderabad, India (2012). https://doi.org/10.1109/VLSID.2012.102
  * [30] Lv, J., Kalla, P., Enescu, F.: Verification of composite galois field multipliers over gf ((2m)n) using computer algebra techniques. In: 2011 IEEE International High Level Design Validation and Test Workshop. pp. 136–143. IEEE, Napa Valley, CA, USA (2011). https://doi.org/10.1109/HLDVT.2011.6113989
  * [31] Matsakis, N.D., Klock, F.S.: The rust language. Ada Lett. 34(3), 103–104 (oct 2014). https://doi.org/10.1145/2692956.2663188, https://doi.org/10.1145/2692956.2663188
  * [32] de Moura, L., Kong, S., Avigad, J., van Doorn, F., von Raumer, J.: The lean theorem prover (system description). In: Automated Deduction - CADE-25. pp. 378–388. Springer International Publishing, Cham (2015)
  * [33] network, A.: Disclosure of recent vulnerabilities (2022), https://hackmd.io/@aztec-network/disclosure-of-recent-vulnerabilities
  * [34] Nipkow, T., Wenzel, M., Paulson, L.C.: Isabelle/HOL: A Proof Assistant for Higher-Order Logic. Springer Berlin Heidelberg, Berlin, Heidelberg (2002). https://doi.org/10.1007/3-540-45949-9, https://doi.org/10.1007/3-540-45949-9
  * [35] Pailoor, S., Chen, Y., Wang, F., Rodríguez, C., Van Geffen, J., Morton, J., Chu, M., Gu, B., Feng, Y., Dillig, I.: Automated detection of under-constrained circuits in zero-knowledge proofs. Proc. ACM Program. Lang. 7(PLDI) (jun 2023). https://doi.org/10.1145/3591282, https://doi.org/10.1145/3591282
  * [36] Parno, B., Howell, J., Gentry, C., Raykova, M.: Pinocchio: Nearly practical verifiable computation. Commun. ACM 59(2), 103–112 (jan 2016). https://doi.org/10.1145/2856449, https://doi.org/10.1145/2856449
  * [37] Peter Bürgisser, Michael Clausen, M.A.S.: Algebraic Complexity Theory. Springer Berlin, Heidelberg, Berlin, Heidelberg (1996). https://doi.org/10.1007/978-3-662-03338-8, https://doi.org/10.1007/978-3-662-03338-8
  * [38] Scholl, C., Konrad, A.: Symbolic computer algebra and sat based information forwarding for fully automatic divider verification. In: 2020 57th ACM/IEEE Design Automation Conference (DAC). pp. 1–6. IEEE, San Francisco, CA, USA (2020). https://doi.org/10.1109/DAC18072.2020.9218721
  * [39] Shi, C., Chen, H., Liu, R., Li, G.: Data-flow-based normalization generation algorithm of r1cs for zero-knowledge proof (2023)
  * [40] Soureshjani, F.H., Hall-Andersen, M., Jahanara, M., Kam, J., Gorzny, J., Ahmadvand, M.: Automated analysis of halo2 circuits. Cryptology ePrint Archive, Paper 2023/1051 (2023), https://eprint.iacr.org/2023/1051, https://eprint.iacr.org/2023/1051
  * [41] Steffen, S., Bichsel, B., Baumgartner, R., Vechev, M.: Zeestar: Private smart contracts by homomorphic encryption and zero-knowledge proofs. In: 2022 IEEE Symposium on Security and Privacy (SP). pp. 179–197. IEEE, THE HYATT REGENCY, SAN FRANCISCO, CA (2022). https://doi.org/10.1109/SP46214.2022.9833732
  * [42] Volkovich, I.: A guide to learning arithmetic circuits. In: Feldman, V., Rakhlin, A., Shamir, O. (eds.) 29th Annual Conference on Learning Theory. Proceedings of Machine Learning Research, vol. 49, pp. 1540–1561. PMLR, Columbia University, New York, New York, USA (23–26 Jun 2016), https://proceedings.mlr.press/v49/volkovich16.html
  * [43] Watanabe, Y., Homma, N., Aoki, T., Higuchi, T.: Application of symbolic computer algebra to arithmetic circuit verification. In: 2007 25th International Conference on Computer Design. pp. 25–32. IEEE, Lake Tahoe, CA, USA (2007). https://doi.org/10.1109/ICCD.2007.4601876
  * [44] Wen, H., Stephens, J., Chen, Y., Ferles, K., Pailoor, S., Charbonnet, K., Dillig, I., Feng, Y.: Practical security analysis of zero-knowledge proof circuits. Cryptology ePrint Archive, Paper 2023/190 (2023), https://eprint.iacr.org/2023/190, https://eprint.iacr.org/2023/190
  * [45] Wu, H., Wang, F., Wei, G.: A survey of noninteractive zero knowledge proof system and its applications. The Scientific World Journal 2014, 560484 (2014). https://doi.org/10.1155/2014/560484, https://doi.org/10.1155/2014/560484
  * [46] Zcash: Zcash: Privacy-protecting digital currency (2023), https://z.cash/