A Practical Polynomial Calculus for Arithmetic Circuit Veri cation

Abstract

Generating and automatically checking proofs independently increases con dence in the results of automated reasoning tools. The use of computer algebra is an essential ingredient in recent substantial improvements to scale veri cation of arithmetic gate-level circuits, such as multipliers, to large bit-widths. There is also a large body of work on theoretical aspects of propositional algebraic proof systems in the proof complexity community starting with the seminal paper introducing the polynomial calculus. We show that the polynomial calculus provides a frame-work to de ne a practical algebraic calculus (PAC) proof format to capture low-level algebraic proofs needed in scalable gate-level veri cation of arithmetic circuits. We apply these techniques to generate proofs obtained as by-product of verifying gate-level multipliers using state-of-the-art techniques. Our experiments show that these proofs can be checked e ciently with independent tools.

Introduction

Formal veri cation gives correctness guarantees. However, the process of veri cation might also not be error-free. A common approach to increase con dence in the results of veri cation consists of generating machine checkable proofs which are then checked by independent proof checkers. These checkers are less complex than for example theorem provers producing proofs and can also be veri ed.

For instance many applications of formal veri cation rely on SAT solvers. Their results can be validated by producing and checking resolution proofs [ 17,37 ] or clausal proofs [ 15,17 ]. Generating proofs is mandatory in the main track of the SAT Competition since 2016. These approaches have also recently been shown to scale to huge low-level proofs of combinatorial problems such as the Boolean Pythagorean triples problem [ 18 ] or Schur Number Five [ 16 ].

However, in certain applications, e.g., arithmetic circuit veri cation, resolution based SAT solving does not work. Especially reasoning about gate-level multipliers is considered to be hard [ 5 ]. For arithmetic circuit veri cation the currently most promising approach uses algebraic reasoning [ 11,26,30,32 ].

In this approach each circuit gate is translated into a polynomial to model constraints between its output and inputs, i.e., roots of polynomials are identied as solutions of gate constraints. Additional polynomials ensure that values remain in the Boolean domain. Word-level speci cations relating circuit outputs and inputs can also be translated into polynomials. Thus veri cation boils down to show that the speci cation polynomial is \implied" by the polynomials induced by the circuit gates (contained in the ideal generated by them).

To validate results of algebraic reasoning the polynomial calculus can be used [ 12 ]. It operates on polynomials and allows to check if a polynomial is a logical consequence of a given set of polynomials. The main focus in this area has been on proof complexity to obtain lower-bounds for the degree and size of proofs [ 20 ]. For instance [ 27 ] introduces a general method to obtain lower bounds and [ 25 ] shows that certifying the non-k-colorability of graphs requires proofs of large degree. A more general calculus capable of detecting unsatis ability of nonlinear equalities as well as inequalities is discussed in [ 34 ].

Our paper shows that the polynomial calculus can also be used in practice. In particular we generate low-level algebraic proofs needed to validate the results of ideal membership testing used in arithmetic circuit veri cation by translating proofs extracted from computer algebra systems to polynomial refutations in the polynomial calculus. After we review preliminaries in Sect. 2, we present a concrete proof format for polynomial calculus proofs, called practical algebraic calculus in Sect. 3. In Sect. 4 we give a comprehensive introduction to arithmetic circuit veri cation, following [ 30 ]. Section 5 introduces the tool ow of verifying and proof checking arithmetic circuits. In our experiments, shown in Sect. 6, our new proof checker PacTrim is used to independently validate the results of multiplier veri cation [ 30 ]. We further apply these techniques to equivalence checking of multipliers [ 31 ] and proving certain ring properties, e.g. commutativity of multipliers [ 3 ]. In general, we claim that our approach is the rst to provide machine checkable proofs for current state-of-the-art techniques in verifying arithmetic circuits [ 11,26,30,32 ]. 2

Preliminaries

Proof systems are used to validate the results of veri cation systems. While a veri cation system only gives a yes/no answer, a proof system provides additionally a certi cate with which the answer can be checked independently. We are concerned here with a proof system for reasoning about polynomial equations. The question is whether the zeroness of a certain set of polynomials implies the zeroness of another polynomial. We consider polynomials p 2 F[X] where F is a eld and X = fx1; : : : ; xng is a nite set of variables. The function X 7! p(X) is called polynomial function of p. The polynomial equation of p is de ned as p(X) = 0 and the solutions of this equation are the roots of p. From now on we drop the function argument and write p = 0 instead of p(X) = 0.

Reasoning with polynomial equations is well-understood both in computer algebra and in computational logic. Already Hilbert and collaborators have studied the theory of polynomial ideals in order to reason about the solution sets of polynomial equations. The application of Grobner bases [ 8 ] by for instance Kapur [ 21,22,23 ] has turned the algebraic approach into a valuable computational tool for automated theorem proving with renewed recent interest [ 1,38 ].

In order to introduce the notation and terminology needed later, let us give a brief summary of the theory. As far as algebra is concerned, we follow the standard textbooks [ 4,9,13 ]. From the logical perspective, we use a variant of the polynomial calculus (PC) as proposed by [ 12 ]. It is more exible than the Nullstellensatz (NS) proof system [ 2 ], which is also heavily used in the proof complexity community. The relation between PC and NS in the context of our application is further discussed at the end of this section.

Let G F[X] and f 2 F[X]. In logical terms, the question is whether the equation f = 0 can be deduced from the equations g = 0 with g 2 G, i.e., every common root of the polynomials g 2 G is also a root of f . As we will only consider polynomial equations with right hand side zero, we take the freedom to write f instead of f = 0. We write proofs as tuples P = (p1; : : : ; pn) of polynomials where each pi is derived by one of the following rules.

Addition

Multiplication pi pi + pj

pj pi qpi pi; pj appearing earlier in the proof or are contained in G pi appearing earlier in the proof or is contained in G and q 2 F[X] being arbitrary If f can be deduced from the polynomials g 2 G, i.e. pn = f , we write G ` f . In algebraic terms, G ` f means that f belongs to the ideal generated by G. Recall that an ideal I F[X] is de ned as a set with 0 2 I and the closure properties u; v 2 I ) u + v 2 I and w 2 F[X]; u 2 I ) wu 2 I. If G = fg1; : : : ; gmg F[X] is a nite set of polynomials, then the ideal generated by G is de ned as the set fq1g1 + + qmgm : q1; : : : ; qm 2 F[X]g and denoted by hGi. The set G is called a basis of the ideal hGi. It is clear that this is an ideal and that it consists of all the polynomials whose zeroness can be deduced from the zeroness of the polynomials in G. In logical terms we would call G an axiom system and hGi the corresponding theory. If we can derive G ` 1, or in algebraic terms 1 2 hGi, the PC proof is called a PC refutation.

Example 1. This example shows that the output c of an XOR gate over an input a and its negation b = :a is always true, i.e., c = 1 or equivalently c + 1 (= 0). We apply the polynomial calculus over the ring Q[c; b; a]. Over Q a NOT gate x = :y is modeled by the polynomial x + 1 y and an XOR gate z = x y is modeled by the polynomial z + x + y 2xy. Because the variables are of the boolean domain we further need to enforce that every variable can only take the values 0 or 1. Therefore we add for each variable xi a polynomial of the form xi(xi 1) to the given set of polynomials. The corresponding circuit representation, the given polynomials and a polynomial proof are shown in Fig. 1. Example 2. Let G = fx; x + yg Q[x; y], f = y. We have G ` f . A proof is P = ( x; y). The rst entry follows by the multiplication rule from x with q = 1, and the second entry follows by the addition rule from the rst entry and x + y which is contained in G. G = f b + 1

a; c + a + b

2ab; a2 a; b2

b; c2 c + a + b 2ab c + 1 2ab cg b + 1

Thanks to the theory of Grobner bases [ 4,8,13 ], the polynomial calculus is decidable, i.e., there is an algorithm, which for any nite G F[X] and f 2 F[X] can decide whether G ` f or not. A basis of an ideal I is called a Grobner basis if it enjoys certain structural properties whose precise de nition is not relevant for our purpose. What matters are the following fundamental facts: { There is an algorithm (Buchberger's algorithm) which for any given nite set B F[X] computes a Grobner basis for the ideal hBi generated by B. { Given a Grobner basis G, there is a computable function redG : F[X] ! F[X] such that 8 p 2 F[X] : redG(p) = 0 () p 2 hGi. { Moreover, if G = fg1; : : : ; gmg is a Grobner basis of an ideal I and p; r 2 F[X] are such that redG(p) = r, then there exist h1; : : : ; hm 2 F[X] such that p r = h1g1 + + hmgm, and such polynomials hi can be computed. Consider the extended calculus with the additional rule

Radical

pim pi pmim2apNpneafring earlier in the proof or is contained in G.

0g and If the polynomial f can be deduced from the polynomials g, where g 2 G, with the rules of PC and this additional radical rule, we write G `+ f and call this proof radical proof (`+). In algebra, the set f f 2 F[X] : G `+ f g is called the radical ideal of G and is typically denoted by phGi.

Also the extended calculus `+ is decidable. It can be reduced to ` using the so-called Rabinowitsch trick [13, 4x2 Prop. 8], which says f 2 phGi () 1 2 hG [ fyf 1gi or

G `+ f ()

G [ fyf 1g ` 1; depending whether you prefer algebraic or logic notation. In both cases, y is a new variable and the ideal/theory on the right hand sides is understood as an ideal/theory of the extended ring F[X; y]. The Rabinowitsch trick is therefore used to replace a radical proof (`+) by a PC refutation.

For a given set G F[X], a model is a point u = (u1; : : : ; un) 2 Fn such that for all g 2 G we conclude that g(u1; : : : ; un) = 0. Here, by g(u1; : : : ; un) we mean the element of F obtained by evaluating the polynomial g for x1 = u1; : : : ; xn = un. For a set G F[X] and a polynomial f 2 F[X], we write G j= f if every model for G is also a model for ff g. Given G F[X], de ne V (G) as the set of all models of G. For an algebraically closed eld F, Hilbert's Nullstellensatz [13, 4x1 Thms. 1 and 2] asserts that V (G) is nonempty if and only if 1 62 hGi, and furthermore, f 2 phGi () V (G) V (ff g). In other words, G j= f () G `+ f . Particularly, the PC including the radical rule is correct (\(") and complete (\)"). In combination with Rabinowitsch's trick, we can therefore decide the existence of models and furthermore produce certi cates for the non-existence of models.

For our applications, only models u 2 f0; 1gn Fn matter. Let us write G j=bool f if every model u 2 f0; 1gn of G is also a model of ff g. Using basic properties of ideals as described in [13, 4x3 Thm. 4], it is easy to show that G j=bool f () G [ B j= f , where B = fxi(xi 1) : i = 1; : : : ; ng. Furthermore, the equivalence G [ B j= f () G [ B `+ f holds also when F is not algebraically closed, because changing from F to its algebraic closure F will not have any e ect on the models in f0; 1gn. Finally, let us remark that the niteness of f0; 1gn also implies that G [ B `+ f () G [ B ` f . This follows from Seidenberg's lemma [4, Lemma 8.13] and generalizes Theorem 1 of [ 12 ].

In contrast to a PC refutation G [ f1 yf g [ B ` 1, where each polynomial in the proof is generated using the rules of PC, a refutation in the NS proof system is a set of polynomials Q = fq1; : : : ; qmg F[X] such that m X qipi = 1 for i=0 pi 2 G [ f1 yf g [ B: Although both systems are able to verify correctness of a refutation, we will use PC and not the NS proof system, because for arithmetic circuit veri cation we will rewrite some polynomials of G [ f1 yf g [ B, and thus gain an optimized algebraic representation of the circuit, cf. Sect. 4. In a correct NS refutation we would also need to express these rewritten polynomials as a linear combination of elements of G [ f1 yf g [ B and thus lose the optimized representation, which will most likely lead to an exponential blow-up of monomials in the NS proof [ 10 ]. In PC we can generate these optimized polynomials on-the- y and then use these polynomials to show the correctness of the refutation. 3

Practical Algebraic Calculus

For practical proof checking we translate the abstract polynomial calculus (PC) into a concrete proof format, i.e., we only de ne a format based on PC, which is logically equivalent but more precise. In principle a proof in PC can be seen as a nite sequence of polynomials derived from given polynomials and previously inferred polynomials by applying either an addition or multiplication rule.

To ensure correctness of each rule it is of course necessary to know which rule was used, to check that it was applied correctly, and in particular which given or previously derived polynomials are involved. During proof generation these polynomials are usually known and thus we require that all of this information

letter ::= ` a ' j ` b ' j : : : j ` z ' j ` A ' j ` B ' j : : : j ` Z ' number ::= ` 0 ' j ` 1 ' j : : : j ` 9 ' constant ::= (number)+ variable ::= letter (letter j number) power ::= variable [ ` ^ ' constant ] term ::= power (` * ' power) monomial ::= constant j [ constant ` * ' ] term

operator ::= ` + ' j ` - ' polynomial ::= [ ` - ' ] monomial (operator monomial) given ::= (polynomial ` ; ')

rule ::= (` + ' j ` * ') ` : ' polynomial ` , ' polynomial ` , ' polynomial ` ; ' proof ::= (rule ` ; ') is part of a rule in our concrete practical algebraic calculus (PAC) proof format to simplify proof checking. The syntax of PAC is shown in Fig. 2. White space is allowed everywhere except between letters and digits in a constant or a variable. A proof rule contains four components

o : v; w; p; The rst component o denotes the operator which is either ` + ' for addition or ` * ' for multiplication. The next two components v; w specify the two (antecedent) polynomials used to derive p (conclusion). In the multiplication rule w plays the role of the polynomial q of the multiplication rule of PC, cf. Sect. 2. A refutation in PAC is a proof, which contains a non-zero constant polynomial (typically just the constant \1") as conclusion p of a rule.

As discussed above we do not need the radical rule for our purpose, even though it could be easily added. Further note that the format is independent of the domain of the models u, e.g., u 2 f0; 1gn for gate-level circuit veri cation, to which the values of variables are restricted. If such a restriction is necessary, all elements of the corresponding set B (often also called eld polynomials) have to be added to the given set of polynomials.

Although the de nition of number together with the de nition of polynomial only allows integer coe cients this is not a severe restriction. Rational number coe cients can be simulated by multiplying involved polynomials with appropriate non-zero constants to eliminate denominators.

Example 3. Consider again Ex. 1. To test membership of 1 c 2 phGi we add 1 + y(c 1) to the set of given polynomials G in order to apply Rabinowitsch's trick and obtain a PAC refutation: + : -c+a+b-2a*b, -b+1-a, -c+1-2a*b; * : -b+1-a, -2a, 2a*b-2a+2a^2; + : -c+1-2a*b, 2a*b-2a+2a^2, -c+1-2a+2a^2; * : a^2-a, -2, -2a^2+2a; + : -c+1-2a+2a^2, -2a^2+2a, -c+1; * : -c+1, y, -c*y+y; + : -c*y+y, 1+c*y-y, 1; input

G r1 rk sequence of given polynomials sequence of PAC proof rules output \incorrect", \correct-proof", or \correct-refutation" P0 G for i 1 : : : k let ri = (oi; vi; wi; pi) case oi = + if vi 2 Pi 1 ^ wi 2 Pi 1 ^ pi = vi + wi then Pi else return \incorrect" case oi = if vi 2 Pi 1 ^ pi = vi wi then Pi append(Pi 1; pi) else return \incorrect" for i 1 : : : k

if pi is a non zero constant polynomial then return \correct-refutation" return \correct-proof" append(Pi 1; pi)

For proof validation we need to make sure that two properties hold. The connection property states that the components v; w are either given polynomials or conclusions of previously applied proof rules. For multiplication we only have to check this property for v, because w is an arbitrary polynomial. By the second property, called inference property, we verify the correctness of each rule, namely we simply calculate v + w resp. v w and check that the obtained result matches p. In a correct PAC refutation we further need to verify that at least one pi is a non-zero constant. The complete checking algorithm is shown in Fig. 3. 4

Circuit veri cation using Computer Algebra

Following [ 11,30,31,32,33,36 ] we consider gate-level (integer) multipliers with 2n input bits a0; : : : ; an 1; b0; : : : ; bn 1 2 f0; 1g and 2n output bits s0; : : : ; s2n 1 2 f0; 1g. Each internal gate (output) is represented by a further variable l1; : : : ; lm. In this setting let X = a0; : : : ; an 1; b0; : : : ; bn 1; l1; : : : ; lm; s0; : : : ; s2n 1. Then a multiplier is correct i for all possible inputs the following speci cation holds: 2n 1 X 2isi = i=0 n 1 X 2iai i=0 n 1 X 2ibi i=0 (1) Using algebraic reasoning this can be veri ed by showing that the speci cation is contained in the ideal generated by the gate constraints. For each logical gate in the circuit a so-called gate polynomial g 2 Q[X] representing the relation between the gate inputs and output is de ned. Example 1 de nes these polynomials for a NOT and an XOR gate. Indicating that the circuit operates over Boolean variables we add for each variable xi 2 X the relation xi(xi 1) matching the de nition of B in the last paragraph of Sect. 2 to the gate polynomials G.

Although all variables are restricted to boolean values we use Q as the base eld. Using Q connects the circuit speci cation (Eqn. (1)) to multiplication in Q. The speci cation would be the same over Z, but Z is not a eld, hence the underlying Grobner basis theory would be more complex. Theoretically reasoning in the eld Z2 is possible, but probably would be much more involved. A more precise comparison will be done in the future.

A term order is a lexicographic term order if for all terms 1 = x1u1 xunn , 2 = x1v1 xvnn we have 1 < 2 i there exists i with uj = vj for all j < i, and ui < vi. If the terms in the gate polynomials are ordered according to such a lexicographic variable ordering where the variable corresponding to the output of a gate is always bigger than the variables corresponding to inputs of the gate, then by Buchberger's product criterion [ 13 ] the gate polynomials de ne a Grobner basis for the ideal generated by the gate polynomials. Thus the correctness of the circuit can be shown by reducing the speci cation by the gate polynomials using polynomial reduction (redG) and checking if the result is zero. We generate and check proofs for this reduction, cf. Sect. 5.

Directly reducing the speci cation without rewriting the Grobner basis leads to an explosion of intermediate results [ 30 ]. In practice it is necessary to use rewriting techniques to simplify the Grobner basis. In recent work [ 32 ] a reduction scheme was proposed which e ectively (partially) reduces the Grobner basis. These preprocessing steps [ 32 ] are also applied in [ 30 ], where we introduced a column-wise checking algorithm which cuts the circuit into 2n slices Si with 0 i < 2n such that each slice contains exactly one output bit si. In each slice the relation that the sum of the outgoing carries Ci+1 and the output-bit si is equal to the sum of the partial products Pi = Pk+l=i akbl and the incoming carries of the slice Ci has to hold. Thus we de ne for each slice Si a corresponding speci cation Ci = 2Ci+1 + si Pi. Initially we set C2n = 0 and recursively calculate Ci as the remainder of reducing 2Ci+1 +si Pi by the gate polynomials of the corresponding slice. In a correct multiplier C0 = 0 has to hold. Hence each slice is veri ed recursively, thus the problem of circuit veri cation is divided into smaller more manageable sub-problems.

In [ 31 ] we further improved incremental checking by eliminating variables [ 7 ], local to full- and half-adders. Since these preprocessing and incremental algorithms are complex and error prone to implement but essential to achieve scalable veri cation we also generate and check proofs for them. 5

Engineering

We take as input circuit an And-Inverter Graph (AIG) [ 24 ] in the common AIGER format [ 6 ]. The AIG is then veri ed using the computer algebra system Mathematica [ 35 ]. We also generate proofs in our PAC-format (c.f. Sect. 3) which then are either passed on to the computer algebra system Singular [ 14 ] or to our own algebraic proof checker PacTrim. The complete veri cation ow is depicted in Fig. 4. Boxes with \.hsu xi" refer to the input AIG or generated les. The variable n de nes the length of the two input bitvectors of the multiplier.

PacMultSpecnPacEqSpec

AigToPoly AigMul.& ProofIt verify+ AigMul.

verify .wl .wl

Mathematica .out Python

Mathematica Veri cation

.spec .polys .pac

Python Singular connect .singular inference Certi cation check II

PacTrim check I

Certi cation

The tool AigMulToPoly [ 30,31 ] is used for veri cation without generating proofs (verify). It takes an AIG as input and produces a le which can be passed on to either Mathematica or Singular, which then performs the actual ideal membership test. Di erent option settings can be selected to enable or disable the preprocessing and rewriting techniques discussed in Sect. 4.

For proof generation (verify+) we use a second tool ProofIt which takes the output le from AigMulToPoly as well as the original AIG and returns a le which can be passed on to Mathematica. In Mathematica the proof (.pac) is calculated. In the tool AigToPoly the original AIG is translated into a set of polynomials G without applying any preprocessing. Together with the set B = fxi(xi 1) j xi 2 Xg these polynomials de ne the given set of polynomials G [ B of the PAC proof (.polys). This is a rather trivial task implemented in less than 130 lines of C code (half of them are just about command line option handling) using the AIGER [ 6 ] library for parsing.

In the same spirit PacMultSpec and PacEqSpec have been implemented to produce the speci cations we want to verify (.spec). In PacMultSpec we simply generate the multiplier speci cation as given in Sect. 4, i.e. Eqn. (1) attened. In PacEqSpec we generate a similar speci cation for equivalence checking of two multipliers [ 31 ]. To gain a PAC refutation both types of specications are produced in negated form using the Rabinowitsch trick and hence become part of the given set of polynomials.

Each polynomial of AigMulToPoly which is derived during preprocessing needs to be checked if it is a logical consequence of the given set of polynomials. Hence for each preprocessed polynomial f the representation modulo the given set of polynomials G [ B = fg1; : : : ; gkg is calculated in Mathematica using the built-in function \PolynomialReduce". This command does not only allow to compute the reduction redG[B(f ) = r, but it also returns cofactors h1; : : : ; hk such that f = h1g1 + : : : + hkgk + r. If the preprocessing is done correctly the derived polynomials f are contained in the ideal hG [ Bi, thus redG[B(f ) = 0 and the above representation simpli es to f = h1g1 + : : : + hkgk. Knowing the cofactors hi and the corresponding elements of G [ B we generate proof rules in PAC in the following way. First we generate a multiplication proof rule for each product higi.

: g1; h1; h1g1; : gk; hk; hkgk;

In the listed rules the result p is always depicted simply as the product higi, but in the actual PAC proof p is written in expanded ( attened) form. These products are now simply added together as follows: + : h1g1; h2g2; + : h1g1 + h2g2; h3g3; . .

. + : h1g1 + : : : + hk 1gk 1; hkgk; f ;

In the experiments we also use a non-incremental veri cation approach where we do not use the incremental optimizations presented in Sect. 4, hence we have to reduce the complete word-level speci cation of a multiplier by the (preprocessed) gate and eld polynomials. Extracting a proof works in the same way as just described for the preprocessed polynomials.

Generating proofs for incremental veri cation is also similar, but instead of the word-level speci cation of the multiplier we have to use the incremental speci cations Ci = 2Ci+1 + si Pi of each slice, cf. Sect. 4. The polynomials Ci describing the incoming carries of a slice can be derived by calculating redG[B(2Ci+1 + si Pi) = Ci. Since veri cation can be assumed to succeed we have C2n = 0 and C0 = 0. As described in the last bullet on fundamental facts in Sect. 2 we are able to obtain cofactors h1; : : : ; hk such that 2Ci+1 + si Pi Ci = h1g1 + : : : + hkgk and consequently a translation into the PAC-format to derive the left-hand side of the equation.

To derive the word-level speci cation of a multiplier from the incremental speci cations we rst multiply for each slice Si its incremental speci cation Ci = 2Ci+1 + si Pi by the constant 2i. Subsequent accumulation of the polynomials above using PAC addition rules cancels the terms Ci and Pi2=n0 1 2isi Pi2=n0 1 2iPi remains. It holds that the sum of partial products can be reordered to Pi2=n0 1 2iPi = (Pin=01 2iai)(Pin=01 2ibi) [ 30 ] and thus we are able to deduce the word-level speci cation of multipliers.

In both approaches the incremental as well as the non-incremental one we multiply the word-level speci cation of the multiplier by the additional variable y and add it to the given polynomial 1 y spec 2 G [ B to derive 1 and thus obtain a correct PAC refutation.

As Fig. 4 shows we have two di erent ows for checking PAC proofs independently from Mathematica, which was used for veri cation. The rst one uses Python scripts to validate the connection property of each rule and whether the proof actually de nes a refutation. With Singular we check the inference property of each proof line, which in essence uses Singular as a calculator for adding and multiplying polynomials. p33 FA p32 FA p23 FA p31 p30 p21 p20 p11 p10 p01 p00 HA FA FA HA p22 p12 p02 FA FA HA p13 p03 FA HA p31 p22 p30p21p12 p20p11p02 p10 p01 p00

HA FA FA HA p33 FA p32 p23 FA FA

FA FA p13

p03 FA HA

HA s7 s6 s5 s4 s3 s2 s1 s0 s7 s6 s5 s4 s3 s2 s1 Fig. 5: Architecture of \btor" (left) and \sparrc" (right), where pij = aibj [ 31 ] s0

We also provide a new dedicated proof checker called PacTrim implemented from scratch in C. It has similar features as DRAT-trim, which is the standard proof checker in the SAT community for clausal proofs (and is used in the SAT Competition { see also [ 16,18 ]). Our new PacTrim checker contains a parser for PAC proofs and checks the connection property using hash tables and the inference property using a dedicated stand-alone implementation of polynomial arithmetic over arbitrary precision integers represented as strings.

While the rst approach is rather general and easy to adapt it is, as the experiments con rm, less robust (due to for instance the limit on variables in Singular) and more importantly far less e cient than our dedicated checker. The latter also allows to produce proof cores (of both original polynomials and proof lines), and is also much closer to being certi able. 6

Experiments

In our experiments we generate and validate PAC proofs for the (integer) multiplier benchmarks used in [ 30,31 ]. The \btor"-benchmarks are generated by Boolector [ 28 ] and the \sparrc"-multipliers are part of the bigger AOKI benchmark set [ 19 ], containing several multiplier architectures. In both multiplier architectures the partial products are generated as products of two input bits which are then accumulated by full- and half-adders, as shown in Fig. 5 for input size n = 4. In \btor"-multipliers the full- and half-adders are accumulated in a grid-like structure, thus they are considered as array multipliers, whereas in \sparrc"-multipliers full- and half-adders are accumulated diagonally.

In all our experiments we use a standard Ubuntu 16.04 Desktop machine with Intel i7-2600 3.40GHz CPU and 16 GB of main memory. The (wall-clock) time limit is 90 000 seconds and the main memory usage is limited to 7GB. The time in our experiments is measured in seconds (wall-clock time). We mark un nished experiments by TO (reached time limit), MO (reached memory limit) or by EE, when an error state is reached. An error state is reached by Singular, because it has a limit of 32767 on the number of ring variables. All experimental data, benchmarks and source code is available at http://fmv.jku.at/pac.

In Table 1 we separately list the time taken for veri cation, the generation as well as checking of PAC-proofs for \btor"and \sparrc" multipliers of di erent input bitwidth n. The third column lists con gurations of AigMulToPoly. The default con guration uses incremental column-wise slicing of [ 30 ], c.f. Sect. 4, both with (inc-add) and without (inc) our new optimization of eliminating local variables in full- and half-adders [ 31 ]. In the third con guration (noninc) the whole word-level speci cation is reduced without any slicing of the multiplier.

The time needed for veri cation, proof generation and proof checking is listed in the following columns. The corresponding execution paths are marked in Fig. 4 by dashed rectangles. The column verify shows the time Mathematica needs to verify the multiplier, column verify+ shows the time needed to generate the proof including the time of verify and in column chk I we measure the time our own proof checker PacTrim needs to validate the proof. The time Python needs to verify the connection property is listed in column con and the time Singular needs to verify the inference property is listed in column inf. The column chk II is the total time needed to verify the proof with Python and Singular. We did not include the time the tools AigToPoly, PacMultSpec and PacEqSpec need, because in the worst-case it only takes a second for 64-bit multipliers.

Inspired by [ 27 ] we also compute and include the number of polynomials in a proof (length), the total number of monomials of the derived polynomials (size), counted with repetition, and the maximum total degree of any monomial (deg). n mult 4 btor-btor 8 btor-btor 16 btor-btor 32 btor-btor 64 btor-btor 4 btor-sparrc 8 btor-sparrc 16 btor-sparrc 32 btor-sparrc 4 sparrc-sparrc 8 sparrc-sparrc 16 sparrc-sparrc 32 sparrc-sparrc Usually not all given polynomials in the data set G [ f1 yf g [ B are needed to derive a correct refutation, especially only a small subset of B is used. Thus next to the length and size columns we list the percentage of polynomials and monomials which are actually necessary to derive a PAC refutation (core) w.r.t. the number of original and derived polynomials.

In general it can be seen that \sparrc"-multipliers need more time and space for veri cation, certi cation and proof checking than \btor"-multipliers. By far most of the time is needed for generating the proofs. For more scalable proof generation it is clear that computer algebra systems would need to be adapted to support proof generation on-the- y or even application speci c algebraic reasoning engines have to be implemented. Checking the proof with PacTrim takes a fraction of the time needed for veri cation, at most 12 seconds, even for 64 bit multipliers. Proof checking using an independent computer algebra system takes much longer { for 64 bit multipliers more than 4000 seconds.

In further experiments shown in Table 2 we construct proofs for the commutativity property of multipliers, i.e., we want to prove for a certain multiplier architecture that A B = B A holds. Among other things it was shown in the work of [ 3 ] that polynomial sized resolution proofs for the commutativity property of array and diagonal multipliers exist. Motivated by this result we generate proofs for these two multiplier architectures, where \btor"-multipliers play the role of array multipliers and \sparrc"-multipliers are considered as diagonal multipliers. We generate the commutativity miters by checking the equivalence of a multiplier and the same multiplier with input bit-vectors swapped (btor-btor, sparrc-sparrc). Furthermore we derive proofs for checking the equivalence of the two architectures \btor" vs. \sparrc" (btor-sparrc). The columns in Table 2 follow the same structure as in Table 1. In all commutativity and equivalence checking experiments we used the con guration \inc-add", which uses our incremental column-wise slicing of [ 30 ] with the optimization of eliminating local variables in full- and half-adders. We did not include commutativity or equivalence checking experiments containing \sparrc" multipliers with bit-width n = 64, because we reached an error state (EE) in the experiments of Table 1. 0 0 0 0 5 2 f o rpo 00 re 00 fco 15 o h t g n e L 0 0 0 0 5 0 6 0 + e f 3 o o frrcoep 2e06+ o e izS 60+ e 1 0 0 + e 0 10 20

3B0itwidth n40 50 60 10 20 3B0itwidth n40 Fig. 6: Length and size of btor-btor commutativity check 50 60

In Fig. 6 data points depicting core size (left plot) and core length (right plot) of the \btor-btor"-commutativity proofs are shown for various input bitwidths n. The additional polynomial curves are tted to the data points (using linear regression with R). For the proof length we used a parameterized model of a quadratic polynomial. The proof size required a cubic polynomial. In both cases the match is perfect, with absolute values of residuals less than 9 10 10. This empirically suggested quadratic complexity of algebraic proofs compares favourably to the O(n7log n) upper bound for resolution proofs given in Thm. 2 of [ 3 ].

Comparing the meta data of the \btor-btor" and \sparrc-sparrc"-benchmarks the proof lengths of \sparrc-sparrc"-benchmarks are of the same magnitude as the proof lengths of \btor-btor"-benchmarks. The proof sizes of \sparrc-sparrc" are around three times as big as the proof sizes of \btor-btor" with nearly same percentages for the cores. Hence both measurements of \sparrc-sparrc"benchmarks can also be depicted by quadratic and cubic curves. 7

Conclusion

This paper applies proof checking to algebraic reasoning, not only in theory, but also in practice, in order to validate veri cation techniques based on computer algebra. We show how the abstract polynomial calculus [ 12 ] can be instantiated to yield a practical proof format (PAC). Proofs in this format can be obtained as by-product of verifying multiplier circuits using state-of-the-art techniques and can be checked with our new proof checker tool PacTrim in a fraction of the time needed for veri cation. Our experiments produce small polynomial proofs which certify the correctness of certain multipliers. The theoretical analysis in [ 3 ] gives much larger polynomial upper bounds (for clausal resolution proofs).

To explore the connection between PAC and clausal proof systems, such as RUP and DRAT [ 17 ], is an interesting subject for future work, as well as embedding PAC into more general systems, such as Isabelle [ 29 ].

We want to thank Thomas Sturm for pointing out the Rabinowitsch trick to the second author and Jakob Nordstrom for discussions on the polynomial calculus and Nullstellensatz proof systems. This work is supported by Austrian Science Fund (FWF), NFN S11408-N23 (RiSE), Y464-N18, SFB F5004.

References

1. E. Abraham , J. Abbott , B. Becker , A. M. Bigatti , M. Brain , B. Buchberger , A. Cimatti , J. H. Davenport , M. England , P. Fontaine , S. Forrest , A. Griggio , D. Kroening , W. M. Seiler , and T. Sturm . Satis ability checking and symbolic computation . ACM Comm. Computer Algebra , 50 ( 4 ): 145 { 147 , 2016 .

2. P. Beame , R. Impagliazzo , J. Kraj cek, T. Pitassi, and P. Pudlak . Lower bounds on hilbert's nullstellensatz and propositional proofs . In PROCEEDINGS OF THE LONDON MATHEMATICAL SOCIETY , pages 1 { 26 , 1996 .

3. P. Beame and V. Liew . Towards verifying nonlinear integer arithmetic . In CAV , volume 10427 of LNCS , pages 238 { 258 . Springer, 2017 .

4. T. Becker , V. Weispfenning , and H. Kredel . Grobner Bases. Springer, 1993 .

5. A. Biere . Collection of combinational arithmetic miters submitted to the SAT Competition 2016 . In SAT Competition 2016 , volume B- 2016 -1 of Department of Computer Science Series of Publications B, pages 65 { 66 . Univ. Helsinki, 2016 .

6. A. Biere , K. Heljanko , and S. Wieringa. AIGER 1 . 9 and beyond . Technical report , FMV Reports Series, Institute for Formal Models and Veri cation , Johannes Kepler University, Altenbergerstr. 69 , 4040 Linz, Austria, 2011 .

7. A. Biere , M. Kauers , and D. Ritirc . Challenges in verifying arithmetic circuits using computer algebra . In SYNASC , 2017 , in press.

8. B. Buchberger . Ein Algorithmus zum Au nden der Basiselemente des Restklassenringes nach einem nulldimensionalen Polynomideal . PhD thesis , 1965 .

9. B. Buchberger and M. Kauers . Grobner basis . Scholarpedia , 5 ( 10 ): 7763 , 2010 . http://www.scholarpedia.org/article/Groebner_basis.

10. J. Buresh-Oppenheim , M. Clegg , R. Impagliazzo , and T. Pitassi . Homogenization and the polynomial calculus . Computational Complexity , 11 ( 3-4 ): 91 { 108 , 2002 .

11. M. Ciesielski , C. Yu , W. Brown , D. Liu, and A. Rossi . Veri cation of gate-level arithmetic circuits by function extraction . In DAC , pages 52 : 1{52:6 . ACM, 2015 .

12. M. Clegg , J. Edmonds , and R. Impagliazzo . Using the groebner basis algorithm to nd proofs of unsatis ability . In STOC , pages 174 { 183 . ACM, 1996 .

13. D. Cox , J. Little , and D. O'Shea. Ideals , Varieties, and Algorithms. Springer, 1997 .

14. W. Decker, G. -M. Greuel , G. P ster, and H. Sch onemann. Singular 4-1-0 . http: //www.singular.uni-kl.de, 2016 .

15. E. I. Goldberg and Y. Novikov . Veri cation of proofs of unsatis ability for CNF formulas . In DATE , pages 10886 { 10891 . IEEE Computer Society, 2003 .

16. M. J. H. Heule . Schur number ve . CoRR, abs/1711.08076 , 2017 .

17. M. J. H. Heule and A. Biere . Proofs for satis ability problems . In All about Proofs, Proofs for All , volume 55 , pages 1 { 22 , 2015 .

18. M. J. H. Heule , O. Kullmann , and V. W. Marek . Solving and verifying the boolean pythagorean triples problem via cube-and-conquer . In SAT , volume 9710 of LNCS , pages 228 { 245 . Springer, 2016 .

19. N. Homma , Y. Watanabe , T. Aoki , and T. Higuchi . Formal design of arithmetic circuits based on arithmetic description language . IEICE Transactions , 89- A ( 12 ): 3500 { 3509 , 2006 .

20. R. Impagliazzo , P. Pudlak , and J. Sgall . Lower bounds for the polynomial calculus and the grobner basis algorithm . Computational Complexity , 8 ( 2 ): 127 { 144 , 1999 .

21. D. Kapur . Geometry theorem proving using hilbert's nullstellensatz . In SYMSAC , pages 202 { 208 . ACM, 1986 .

22. D. Kapur . Using grobner bases to reason about geometry problems . J. Symb. Comput. , 2 ( 4 ): 399 { 408 , 1986 .

23. D. Kapur and P. Narendran . An equational approach to theorem proving in rstorder predicate calculus . In IJCAI , pages 1146 { 1153 . Morgan Kaufmann, 1985 .

24. A. Kuehlmann , V. Paruthi , F. Krohm , and M. Ganai . Robust boolean reasoning for equivalence checking and functional property veri cation . IEEE TCAD , 21 ( 12 ): 1377 { 1394 , 2002 .

25. M. Lauria and J. Nordstro m. Graph Colouring is Hard for Algorithms Based on Hilbert's Nullstellensatz and Grobner Bases . In R. O'Donnell, editor, CCC, volume 79 of LIPIcs , pages 2 :1 {2: 20 . Schloss Dagstuhl , 2017 .

26. J. Lv , P. Kalla , and F. Enescu . E cient Gr obner basis reductions for formal veri cation of Galois eld arithmetic circuits . IEEE TCAD , 32 ( 9 ): 1409 { 1420 , 2013 .

27. M. Miksa and J. Nordstro m. A generalized method for proving polynomial calculus degree lower bounds . In CCC , volume 33 of LIPIcs. Schloss Dagstuhl , 2015 .

28. A. Niemetz , M. Preiner , and A. Biere . Boolector 2.0 system description . JSAT , 9 : 53 { 58 , 2014 (published 2015 ).

29. T. Nipkow , L. C. Paulson , and M. Wenzel. Isabelle/HOL - A Proof Assistant for Higher-Order Logic , volume 2283 of LNCS . Springer, 2002 .

30. D. Ritirc , A. Biere , and M. Kauers . Column-wise veri cation of multipliers using computer algebra . In FMCAD , pages 23 { 30 . IEEE, 2017 .

31. D. Ritirc , A. Biere , and M. Kauers . Improving and extending the algebraic approach for verifying bit-level multipliers . In DATE , 2018 , in press.

32. A. Sayed-Ahmed , D. Gro e, U. Kuhne, M. Soeken, and R. Drechsler . Formal veri cation of integer multipliers by combining Grobner basis with logic reduction . In DATE , pages 1048 { 1053 . IEEE, 2016 .

33. A. Sayed-Ahmed , D. Gro e, M. Soeken, and R. Drechsler . Equivalence checking using Grobner bases . In FMCAD , pages 169 { 176 . IEEE, 2016 .

34. A. Tiwari . An Algebraic Approach for the Unsatis ability of Nonlinear Constraints , pages 248 { 262 . Springer Berlin Heidelberg, Berlin, Heidelberg, 2005 .

35. Wolfram Research, Inc. Mathematica, 2016 . Version 10.4.

36. C. Yu , W. Brown , D. Liu, A. Rossi , and M. Ciesielski . Formal veri cation of arithmetic circuits by function extraction . IEEE TCAD , 35 ( 12 ): 2131 { 2142 , 2016 .

37. L. Zhang and S. Malik . Validating SAT solvers using an independent resolutionbased checker: Practical implementations and other applications . In DATE , 2003 .

38. E. Zulkoski, C. Bright , A. Heinle , I. S. Kotsireas , K. Czarnecki , and V. Ganesh . Combining SAT solvers with computer algebra systems to verify combinatorial conjectures . J. Autom. Reasoning , 58 ( 3 ): 313 { 339 , 2017 .