Sylvie Boldo
email: sylvie.boldo@inria.fr

Claude Marché
email: claude.marche@inria.fr

Formal Verification of Numerical Programs: From C Annotated Programs to Mechanical Proofs

Keywords: Floating-point arithmetic, C program, Formal specification, Automated reasoning Mathematics Subject Classification (2010) 68N30

Numerical programs may require a high level of guarantee. This can be achieved by applying formal methods, such as machine-checked proofs. But these tools handle mathematical theorems while we are interested in C code, in which numerical computations are performed using floating-point arithmetic, whereas proof tools typically handle exact real arithmetic. To achieve this high level of confidence on C programs, we use a chain of tools: Frama-C, its Jessie plugin, Why and provers among Coq, Gappa, Alt-Ergo, CVC3 and Z3. This approach requires the C program to be annotated: each function must be precisely specified, and we prove the correctness of the program by proving both that it meets its specifications and that no runtime error may occur. The purpose of this paper is to illustrate, on various examples, the features of this approach.

Introduction

Given a program using floating-point arithmetic, it is pretty hard to know the final rounding error of the result. We are interested in verifying numerical programs with a very high level of guarantee by using formal methods: the expected functional behavior of a given program is expressed by formal specifications, and we prove that the code satisfies these specifications.

The model we use as basis for our method is the fact that each floating-point result is a correct rounding of the exact real value for all basic operations (addition, subtraction, multiplication, division and square root). This property is defined in the IEEE-754 standard [27] and all modern processors comply with it. However, even if each computation is correct, i.e. the best possible, there is no guarantee that the final result after many such computations is still accurate.

Static analysis is an approach for checking a program without running it. Deductive verification techniques rely on the ability of theorem provers to check validity of formulas in first-order logic or even more expressive logics. They usually come with specification languages-such as SPARK [START_REF] Carré | SPARK-an annotated Ada subset for safety-critical programming[END_REF] for Ada, JML [START_REF] Burdy | An overview of JML tools and applications[END_REF]forJava,A CSL [START_REF] Baudin | ACSL: ANSI/ISO C Specification Language[END_REF]for C, Spec# [START_REF] Barnett | The spec# programming system: an overview[END_REF] for C#-which are expressive enough to specify complex functional properties on the behavior of programs.

For automatic analysis of floating-point code, there exist several methods for bounding the final error of a program, including interval arithmetic, forward and backward analysis [START_REF] Higham | Accuracy and stability of numerical algorithms[END_REF][START_REF] Wilkinson | Rounding Errors in Algebraic Processes[END_REF]. Another approach is abstract-interpretation-based static analysis, used e.g. by Astrée [START_REF] Cousot | The ASTRÉE analyzer[END_REF][START_REF] Monniaux | Analyse statique : de la théorie à la pratique[END_REF] and Fluctuat [START_REF] Delmas | Towards an industrial use of FLUCTUAT on safety-critical avionics software[END_REF][START_REF] Goubault | Static analysis of numerical algorithms[END_REF].

Floating-point arithmetic has been formalized using deductive formal methods since 1989: in PVS [START_REF] Carreño | Specification of the IEEE-854 floating-point standard in HOL and PVS[END_REF], in ACL2 [START_REF] Russinoff | A mechanically checked proof of IEEE compliance of the floating point multiplication, division and square root algorithms of the AMD-K7 processor[END_REF], in HOL-light [START_REF] Harrison | Formal verification of floating point trigonometric functions[END_REF]. These approaches consider either hardware components or abstract algorithms, and never C source code. Since 2001, a high-level formalization of floating-point numbers [START_REF] Boldo | Preuves formelles en arithmétiques à virgule flottante[END_REF][START_REF] Daumas | A generic library of floating-point numbers and its application to exact computing[END_REF] is available for the Coq proof assistant [START_REF] Bertot | Interactive Theorem Proving and Program Development[END_REF]. In this paper we build upon the latter to prove source code written in C when needed.

There exist very few works on specifying and proving functional properties directly on floating-point source code, using deductive verification systems. An early work on floating-point support in JML for Java is presented in 2006 by Leavens [START_REF] Leavens | Not a number of floating point problems[END_REF], where mostly runtime assertion checking is considered. Annotations involve Java boolean expressions, which can themselves involve floating-point computations, meaning that annotations can generate rounding errors and overflow, which leads to many issues and traps [START_REF] Leavens | Not a number of floating point problems[END_REF]. This must be avoided when using a theorem proving approach.

The first proposal amenable to formal proof is made in 2007 by Boldo and Filliâtre [START_REF] Boldo | Formal verification of floating-point programs[END_REF], where verifications conditions in Coq are generated from floating-point C programs. Ayad and Marché [START_REF] Ayad | Multi-prover verification of floating-point programs[END_REF] extended this approach to increase genericity, handle exceptional behaviors and support many different provers. The latter is implemented in the Frama-C/Jessie/Why tool chain and we base this paper on it.

It should be noticed that all these approaches assume that floating-point computations strictly follow the IEEE standard. However some processors and/or compilers may invalidate this assumption, e.g. the double roundings induced by extended 80-bits numbers available on INTEL x86 processors. Nevertheless, the approach we use here has been recently extended to handle multiple architectures and compilers [START_REF] Boldo | Hardware-independent proofs of numerical programs[END_REF][START_REF] Boldo | Proofs of numerical programs when the compiler optimizes[END_REF].

The Basics of the Verification Process

Our case studies are conducted using the Frama-C framework for static analysis of C source code 1 and its associated Jessie plugin [START_REF] Gerlach | An experience report on the verification of algorithms in the c++ standard library using frama-c[END_REF][START_REF] Moy | Jessie Plugin Tutorial, Beryllium version[END_REF] that uses the deductive verification platform Why [START_REF] Filliâtre | The Why/Krakatoa/Caduceus platform for deductive program verification[END_REF]. In that setting, the expected behavioral properties of the input C code must be stated using formal specifications, expressed in the ACSL [START_REF] Baudin | ACSL: ANSI/ISO C Specification Language[END_REF] annotation language.

The Tool Chain

The tool chain is described in Fig. 1. The annotated C code is given to the Frama-C kernel which performs the syntactic analysis and type checking of both the code and its annotations, and then normalizes the code [START_REF] Necula | Cil: Intermediate language and tools for analysis and transformation of c programs[END_REF]. Frama-C calls the Jessie plugin which transforms the code into the input language of Why. The Why verification condition generator then produces a set of proof obligations (the verification conditions, abbreviated as VCs), that are a set of logic formulas. Soundness of the code with respect to its annotations is ensured by proving these formulas valid. Additionally, other VCs are generated to guarantee the absence of run-time errors in the program: typically division by zero, dereferencing of the null pointer (or more generally pointer to non properly allocated memory blocks). In the context of floating-point programs, VCs are generated to ensure the absence of overflow and undefined result: it is verified that no infinite values and no NaN will ever be generated by the computations. However, in some specific case such values may be intended to appear, such a case is discussed in Sect. 3.2

Basics of ACSL

We illustrate the main basic features of ACSL on the following toy example, supposed to compute an approximation of the cosine function for an argument close to zero. This example comes from [START_REF] Boldo | Combining Coq and Gappa for certifying floating-point programs[END_REF] where it is fully proved within Coq only. We use single precision numbers to have significantly higher rounding errors to specify. step in the y-axis corresponds to a representable number2 (2 -24 between each). The difference between the dashed and the thin curves is classically the rounding error. Given that picture, we can conjecture that both the method error and the rounding error are bounded by 2 -24 . (Indeed we made the choice of zooming around 1/32 because they are both of the same and worst magnitude there.) These conjectures can be described formally by annotations as follows.

/ * @ requires \ abs ( x ) <= 0x1p -5;

@ ensures \ abs (\ result -\ cos ( x ) ) <= 0x1p -23; @ * / float my_cosine ( float x) { //@ assert \ abs (1.0 -x * x * 0.5 -\ cos ( x ) ) <= 0x1p -24; return 1.0 f -x * x * 0.5 f ; }
The precondition, introduced by requires, states that we expect argument x in the interval [-1/32; 1/32].T h e postcondition, introduced by ensures, states that the distance between the value returned by the function, denoted by keyword \result, and the model of the program, which is here the true mathematical cosine function denoted by \cos in ACSL, is not greater than 2 -23 . It is important to notice that in annotations the operators like + or * denote operations on real numbers and not on floating-point numbers. In particular, there is no rounding error and no overflow in annotations, unlike in the early Leavens' proposal [START_REF] Leavens | Not a number of floating point problems[END_REF]. The C variables of type float, like x and \result in this example, are interpreted as the real number they represent. Thus, the last annotation, given as an assertion inside the code, is a way to make explicit the reasoning we made above, making the total error the sum of the method error and the rounding error: it states that the method error is less than 2 -24 . Again, it is thanks to the choice of having exact operations in the annotations that we are able to state a property of the method error.

Back-end Provers

The way the provers are called on the VCs is schematized in Fig. 4. Why implements translators that are able to print the VCs in the expected input syntax of provers. A first class are the SMT-style provers like Alt-Ergo, Z3 and CVC3: they are able to handle first-order formulas with built-in integer and real arithmetic, and non-interpreted predicate and function symbols defined by axioms. For those provers we pass some axiomatization of floating-point computations, in which the most important ingredient is the axiomatization of the rounding function [START_REF] Ayad | Multi-prover verification of floating-point programs[END_REF] which, given a format (e.g. single or double precision), a rounding mode and a real number, returns its approximation in that format. The Gappa prover [START_REF] Melquiond | Floating-point arithmetic in the Coq system[END_REF] is specialized for reasoning on floating point computations. The rounding function above is built-in, and so is integer and real arithmetic, but it does not support first-order quantification. It will be the prover of choice for VCs where floating-point rounding is involved (including proving absence of overflow), because other provers will only reason from a partial axiomatization of the rounding function, whereas they will deal better with quantified formulas.

Running the cosine annotated code into our proof chain generates 5 VCs: 3 of them amount to prove that there are no overflow when the subtraction and the two multiplications are computed. Another is the assertion itself, and the last is the postcondition. These VCs can be displayed using the Why GUI: a screenshot of it is shown on Fig. 5. Each line of the table on the left of the window corresponds to a VC, whereas the columns correspond to some external theorem provers, namely here Alt-Ergo, Z3, and Gappa. Each prover can be called on each VC, and the results are displayed on that table: a check sign means that the prover proved the formula valid, whereas other icons (with black background) mean either the answer "unknown" (i.e. the prover did not conclude to its validity), a time out, etc. For that particular example, we see that the first two provers proved only the second of the overflow VCs, whereas the Gappa prover proved all VCs except the one coming from the assertion.

Finally, what can be done if a VC cannot be proved by any prover, like the assertion in the example above? The Why platform offers the possibility to call an interactive proof assistant instead. Here we use Coq, which comes with a large library on floating-point numbers3 [START_REF] Boldo | Preuves formelles en arithmétiques à virgule flottante[END_REF][START_REF] Daumas | A generic library of floating-point numbers and its application to exact computing[END_REF]. The Why translator for Coq uses that library for exporting the VCs. Calling Coq on the assertion VC of our cosine example results in the lemma displayed in the Coq IDE shown in Fig. 6. The proof is performed in two lines, by using the interval tactics [START_REF] Melquiond | Proving bounds on real-valued functions with computations[END_REF] specialized for proving bounds on real expressions. It bissects the interval where (single_value x) (denoting the real represented by the float x) lies, and computes the interval of expressions in the goal, until it is proved. (Gappa cannot do it directly because it does not support the cosine function.)

Last but not least, the axiomatization used for SMT solvers has been realized with Coq [START_REF] Ayad | Multi-prover verification of floating-point programs[END_REF][START_REF] Boldo | Formal verification of floating-point programs[END_REF], thus providing a high level of trust in our multi-provers back-end.

Exact Values

ACSL provides floating-point annotations based on [START_REF] Boldo | Formal verification of floating-point programs[END_REF] that allow to specify the exact computations of numerical programs. More precisely, each floating-point expression e has a "ghost" value denoted \exact(e) which does not suffer from rounding. This real value is then computed with the same operations as the float value except that the ghost operation is exact. The construct \round_error(e) is then used for |e -\exact(e)|.

These features can be used to specify differently the same cosine example. Here is a possibility:

/ * @ requires \ abs (\ exact ( x ) ) <= 0x1p -5; @ requires \ round_error ( x ) <= 0x1p -20; @ ensures \ abs (\ exact (\ result ) -\ cos (\ exact ( x ) ) ) <= 0x1p -24; @ ensures \ round_error (\ result )< =\ round_error (x) + 0x2.0081p-25; @ * / float my_cosine2 ( float x) { float r=1 . 0 f-x * x * 0.5 f ; //@ assert \ abs (\ exact (r) -\ cos (\ exact ( x )
) ) <= 0x1p -24; return r; } This is read as follows: the precondition assumes that the exact value of x is in [-1/32; 1/32], with a rounding error less than 2 -20 . In the code, the method error is again stated as an assertion, this time using the \exact construct. Then, the postcondition says that, as before, the exact value of the result is close to the cosine for not more than 2 -24 , and the rounding error on the result is bounded by the original rounding error on x plus 0x2.0081p-25 (i.e just a bit above 2 -24 ). One may wonder how this bound was determined: it is indeed possible to ask the Gappa tool itself the most accurate bound 4 . This bound depends on the bound on the rounding error on x as input. Here is a small table to give in idea on how these bounds are related: the first column is the bound on the rounding error on x, whereas the second column is the bound on the rounding error of the result, minus the one on x. error(x) error(result) -error(x) 2 -28 0x1.01800001p-25 ≃ 2 -24.9916 2 -26 0x1.0480001p-25 ≃ 2 -24.9749 2 -24 0x1.108001p-25 ≃ 2 -24.9099 2 -22 0x1.40801p-25 ≃ 2 -24.6758 2 -20 0x2.0081p-25 ≃ 2 -23.9986 2 -18 0x5.009p-25 ≃ 2 -22.6774 2 -16 0x2.203p-22 ≃ 2 -20.9120 2 -14 0x8.221p-22 ≃ 2 -18.9762

The VCs for proving these annotations in this variant are not very different from the previous one: 3 VCs for overflow, proved by Gappa, the assertion proved within Coq by the interval tactic, and 2 VCs for the 2 postconditions, both proved by Gappa. The first postcondition on the exact value of the result is also proved by SMT solvers: this is expected since it is a simple consequence of the assertion.

Examples

The full code of all these examples (and more) and their proofs are available either on http://www.lri.fr/~sboldo/ research.html, on the Hisseo web page http://hisseo.saclay.inria.fr/gallery.html, or the ProVal gallery http://proval. lri.fr/gallery/index.en.html.

Clock Drift

The purpose of this example is to illustrate the handling of loops via loop invariants. We consider the following C code which increments a counter by steps of 0.1.

float clock_single ( int n) { float t=0 . 0 f ; int i; f o r ( i = 0 ; i < n ; i + + )t=t+0 . 1 f ; return t; }
This is indeed a classical example taken to illustrate rounding errors, coming from the fact that 0.1 is not exactly representable. It is also related to a known bug which arose in the critical software of a patriot missile battery. 5In a mathematical model of that program, t = i ×0.1 is true at each iteration of the loop. But the rounding of 0.1in single precision is 0x0.199999Ap0 ≃ 0.1+1.5e-9. Naively, one could expect i ×0.1 ≤ t ≤ i ×(0.1+1.5e-9) to be a loop invariant in this C program. However, the behavior of floating-point computations is much more complicated, because when t gets higher, the rounding error when computing t + 0.1 f can become either positive or Fig. 7 t -0.1 × i for the first 100 iterations negative, and gets higher in absolute value: Fig. 7 shows the values of ti × 0.1 for the first 100 iterations of the loop.

What we can prove on such a program is then an invariant of the form |t -i × 0.1|≤i × C for some constant C to determine. The problem is that the constant C depends on how many iterations we are going to make. Following the analogy with the clock of the missile battery, we assume that it will not run for more than one day 6 , so we are going to bound the number n of iterations by one million.

The fully annotated code is as follows:

# define NMAX 1000000 # define NMAXR 1000000.0 / * @ lemma real_of_int_inf_NMAX : @\ forall integer i ; i< = N M A X = = >i< = N M A X R ; * / //@ lemma real_of_int_succ : \ forall integer n; n+1 == n + 1.0;

# define A 1.49012e-09 #define B 0x1p-8 #define C (B + A) / * @ requires 0< =n< =N M A X ; @ ensures \ abs (\ result -n * 0.1) <= n * C; * / float clock_single ( int n) { float t=0 . 0 f ; int i;
/ * @ loop invariant 0< =i < =n ; @ loop invariant \ abs (t -i * 0.1) <= i * C; @ loop variant n-i; @ * / for ( i =0; i <n ; i ++) { L: //@ assert 0 . 0 < = t < = NMAXR * (0.1+C) ; t=t+0 . 1 f ; //@ assert \ abs (t -(\ at (t ,L) + ( float )0.1)) <= B; } return t; } 6 As for the analogy with the missile battery bug: indeed the clock had run for 4 days, although it was not supposed to.

The lemmas are given to help the automatic provers: the lemma real_of_int_inf_NMAX is needed by Gappa to prove the assertion on the rounding error. The lemma real_of_int_succ helps the SMT solvers to prove preservation of the loop invariant. A is a bound of ( float)0.1 -0.1, whereas B is a bound of round_error(t + ( float)0.1) for 0 ≤ t ≤ 0.1 × NMAX.

Running this code into our tool chain results in 17 VCs. The first two correspond to the two lemmas: the first one is proved by Gappa, whereas the second is proved by all SMT solvers and Gappa. 5 VCs come from runtime error checks: 1 for the overflow in t + 0.1, proved by both SMT solvers and Gappa, and 4 others from integer overflow checks and loop termination checks, proved by SMT solvers. The remaining 10 VCs come from the behavioral properties of the C function: 3 to check that loop invariants initially hold (proved by SMT solvers and Gappa), 2 for the first assertion (proved by SMT solvers), 1 for the second assertion (proved by Gappa only), 3 to check that the loop invariants are preserved by any loop iteration (proved by SMT solvers but not Gappa), and finally the postcondition, proved by SMT solvers. In all and thanks to the lemmas, everything is proved with automatic provers only.

The constant B was determined using Gappa, similarly as for the cosine example. Here are other values of B in function of NMAX, together with the corresponding approximate value of NMAX×C, that is the bound we obtain on the error at the end of iteration. NMAX 10 In other words, it is proved that the drift after a bit more than one day is not larger than 4,000 s. This is a lot, but it is of course only an upper bound, the real error is much smaller because rounding errors compensate. Such compensation phenomena are discussed in other examples below. 7 3.2 Playing with Special Values: Infinities and NaNs The purpose of this example is to illustrate the support of special values. In most cases, one wants to guarantee that no overflow occur, but if overflows are intended, then our tool chain can support it, by declaring a specific pragma in the code. Additionally, ACSL proposes a set of constructs to handle special values.

The following code illustrates that.

# pragma JessieFloatModel ( full ) / * @ predicate sorted{L}(double * t, integer a, integer b) = @\ forall integer i , j ; a <= i <= j <= b ==> \ le_float ( t [ i ] , t [ j ]); @ * / / * @ requires n >= 0 && \ valid_range (t ,0 ,n-1); @ requires ! \ is_NaN ( v ) ; @ requires \ forall integer i; 0

< = i < = n-1 ==> ! \ is_NaN ( t [ i ] ) ; @ ensures -1< = \ result <n ; @ behavior success : @ ensures \ result >= 0 ==> \ eq_float ( t [\ result ],v); @ behavior failure : @ assumes sorted ( t ,0 ,n-1); @ ensures \ result == -1= = > @\ forall integer k; 0 <= k < n ==> \ ne_float ( t [k] ,v); @ * / int binary_search (double t[], int n, double v) {
int l=0 ,u=n -1; / * @ loop invariant @ 0 <= l && u <= n -1; @f o r f a i l u r e: 7 To conclude the story of the missile battery bug: indeed fixed-point computations where in use there, which make the rounding errors larger because they do not compensate. The lesson to learn is that it would be much better to use a representable number for the tick interval: 1/8 or 1/16 for example.

@ loop invariant @\ forall integer k; @ 0 <= k < l ==> \ lt_float (t[k],v); @ loop invariant @\ forall integer k; @u < k < = n -1 ==> \ lt_float (v, t[k]); @ loop variant u-l; @ * / while ( l <= u ) { int m= l + ( u-l) / 2; if (t[m] < v) l = m + 1; else if (t[m] > v) u = m -1; else return m; } return -1; }
It is a classical binary search of a value in an array sorted in increasing order. Here, we want an array of floats, and we want to allow infinite values to occur, but no NaNs. The pragma switches the Jessie plugin in the mode where overflows are allowed. The predicate sorted(t, a, b) means that array t is sorted between indices a and b included. Since it contains floats and possibly infinities, we cannot use real number comparison <= but must use the predicate le_float extended to special values, specified by the IEEE-754 standard.

The function searches a given value v in an array t, between indices 0 and n -1. The first precondition tells that array t is properly allocated for these indices. The second requires that v is not NaN, and the third requires that the array contains no NaNs either. Notice that since we want a sorted array, NaNs must be excluded. The first postcondition tells that the result value is between -1 and n -1. When the result is non-negative, it should be an index of a cell of t containing v, this is the postcondition of the behavior success. When the result is -1, one expects that v does not occur in t, this is the postcondition of behavior failure. The soundness of this behavior is valid only under the assumption that the array is sorted.

The loop invariants are needed to prove the failure behavior: they state that at each loop iteration, if the value v occurs somewhere then it must be between the indices l and u. More precisely, values before index l must be lower whereas values after u must be higher.

On this code, our tool chain produces 37 VCs. [START_REF] Daumas | A generic library of floating-point numbers and its application to exact computing[END_REF] VCs comes from runtime error checks, and are all proved by both CVC3 and Z3. 8 VCs comes from the loop invariants and the global post-condition, all are proved with all SMT provers. The VCs corresponding to behaviors are all proved by CVC3. Notice that Gappa is not useful here, because this program does not involve computations, only comparisons. Moreover, the handling of special values is implemented in the axiomatic part of Fig. 4.

We refer to [START_REF] Ayad | Multi-prover verification of floating-point programs[END_REF] for more details on the handling of special values, and also other specificities such as changing the default rounding mode.

Sterbenz Subtraction

One of the most basic property of floating-point arithmetic is the following one discovered by Kahan and Sterbenz [START_REF] Sterbenz | Floating Point Computation[END_REF] in the 1970s. If the inputs of a subtraction are near enough one to another, then the subtraction is exact. This is specified as a function that returns the subtraction between its two floating-point inputs. The precondition is that x and y are such that y 2 ≤ x ≤ 2y. Note that the division and multiplication inside the annotations are exact. The postcondition is the fact that the result is equal to the mathematical subtraction of the inputs and therefore does not suffer from rounding.

/ * @ requires y / 2.0 <= x <= 2.0 * y; @ ensures \ result == xy; @ * / float Sterbenz ( float x, float y) { return xy; } There are two VCs that were proved with the Coq interactive prover. The first one is the postcondition: the fact that the result is exactly xy. This was rather easy (7 lines long) as it is only the application of a more general theorem of the library (any precision, any radix, any rounding). The other proof is the fact that the computation xy cannot overflow. The reason is that x and y are nonnegative (as y 2 ≤ x ≤ 2y) and therefore |x -y|≤max(|x|, |y|) cannot be greater than the overflow threshold. This was easy but a little tedious and 20 lines long.

Using Automatic Provers One can reduce the amount of proof to do within Coq by inserting appropriate assertions in the code, to state that x and y are non-negative. The code is as follows:

/ * @ requires y / 2.0 <= x <= 2.0 * y; @ ensures \ result == xy; @ * / float Sterbenz ( float x, float y) { //@ assert 0.0 <= y; //@ assert 0.0 <= x; return x -y; } Now, Alt-Ergo is able to automatically prove the two assertions, Gappa is able to automatically prove the absence of overflow (and the second assertion too), so the only VC remaining to prove within Coq is the post-condition, proved in 7 lines.

Veltkamp/Dekker Algorithm

This example is also from the 1970s but is much more complex. Here, the floating-point properties have been thoroughly used in order to get an exact result. This function indeed computes the exact error of the multiplication [START_REF] Dekker | A floating point technique for extending the available precision[END_REF][START_REF] Veltkamp | Algolprocedures voor het berekenen van een inwendig product in dubbele precisie[END_REF] with only floating-point operations (and no FMA). This requires 16 operations and each of them has a specific role to play to get the exact error. This algorithm was already proved with a generic radix and precise underflow restrictions and overflow restrictions so that no infinity will be created [START_REF] Boldo | Pitfalls of a full floating-point proof: example on the formal proof of the Veltkamp/Dekker algorithms[END_REF]. The question was how to specify it as a program to get the full benefit of the proof.

/ * @ requires xy == \ round_double (\ NearestEven ,x * y) & & @\ abs ( x ) <= 0x1 . p995 && @\ abs ( y ) <= 0x1 . p995 && @\ abs (x * y ) <= 0x1 . p1021 ; @ ensures ((x * y= =0 | | 0 x 1 . p -969 <= \ abs (x * y)) @= = > x * y= =x y + \ result ); @ * / double Dekker We have two floating-point numbers x and y. The rounding of x × y in rounding to nearest, xy, is provided to the function: this is the first part of the pre-condition above. We then have several pre-conditions to prevent overflow: |x|, |y| and |x × y| must not be too big to guarantee that no computation inside the function will overflow. The postcondition is more interesting: we do not require underflow conditions (as it will not mean any failure, only a less precise result [START_REF] Boldo | Pitfalls of a full floating-point proof: example on the formal proof of the Veltkamp/Dekker algorithms[END_REF]), but we assume that |x × y| is either 0 or greater than 2 -969 . This is enough to guarantee that underflow will not endanger the result. Note that it does not mean there is no subnormal number: for example x might be subnormal if y is big enough and the result will still be correct. What is guaranteed by this function is that it computes the error of the multiplication, that is to say the floating-point number r 2 such that x × y = xy+ r 2 where all computations are mathematical exact ones (as in annotations). We have the result mathematically equal to x × yxy under the given assumptions.

Even with the previous results of [START_REF] Boldo | Pitfalls of a full floating-point proof: example on the formal proof of the Veltkamp/Dekker algorithms[END_REF], the proofs were still quite long. The reasons are the following ones:

• the previous proofs handled underflows while here, we assume one degenerate case does not happen (while x or y may be subnormal). So the splitting of cases is different and that makes the reusing of proofs difficult. • the overflow proofs were done by hand in [START_REF] Boldo | Pitfalls of a full floating-point proof: example on the formal proof of the Veltkamp/Dekker algorithms[END_REF] and were very tedious. We then used the Gappa tactic [START_REF] Boldo | Combining Coq and Gappa for certifying floating-point programs[END_REF]t o take advantage of the Gappa automations inside Coq. This was especially interesting here as the use of Gappa requires high-level knowledge only given by another part of the Coq proof: for example the fact that hx is the head of x, that is to say the rounding to nearest on 27 bits of x. The Gappa tactic has saved a lot of lines of Coq and has enhanced the result: the overflow requirements are now weaker.

Given the results of [START_REF] Boldo | Pitfalls of a full floating-point proof: example on the formal proof of the Veltkamp/Dekker algorithms[END_REF], the additional proofs and the full better overflow proof are less than 900 lines long. This also includes the simplest overflow proofs directly done by Gappa which are proved in one line. Note that the file has 20 theorems to prove, is more than 2700 lines long and takes nearly 15 min to be compiled on a 2×3GHz processor.

Kahan Algorithm for an Accurate Discriminant

The next function illustrates two different features. The first one is the function call: we will use the preceding Dekker function. The second one is the fact that a floating-point test may be wrong.

This function computes an accurate discriminant, meaning b 2 -a × c using Kahan's algorithm [START_REF] Kahan | On the cost of Floating-Point Computation Without Extra-Precise Arithmetic[END_REF]. The result is proved correct within 2 ulps in the original paper and then formally proved in [START_REF] Boldo | Proof and certification for an accurate discriminant[END_REF]. The ulp is the unit in the last place of a floating-point number, meaning the value of the last bit of its mantissa. For example in double precision, ulp(1) = 2 -52 .

Unfortunately, both the pen-and-paper proof and the initial formal proofs were assuming that the test was giving the correct answer, meaning that p + q ≤ 3| p -q|⇐ ⇒•( p + q) ≤•(3 ×|•( pq)|), where • is the rounding to nearest. But this is incorrect as we may find a and b such that this does not hold. The solution was to look deeper into these few cases. More precisely, they correspond to particular values of p and q where p ≈ 2q or vice versa. A special proof is done in these few degenerate cases as the values are in a small subset and the algorithm is stable enough to be correct. In all cases, we guarantee the result still holds [START_REF] Boldo | Kahan's algorithm for a correct discriminant computation at last formally proven[END_REF].

Note that the computation of 3 ×|p -q| may overflow and therefore requires tighter bounds on b and a × c than expected.

To specify the postcondition, we have the same kind of requirements: underflow and overflow requirements, that subsume Dekker's ones. The interesting part is that ulp is not part of our basic axiomatic of floating-point arithmetic (it could have been, but we chose to limit the number of keywords). We then define an axiomatic that defines it as we wish: it is a power of the radix such that, for any normal floating-point number f ,w eh a v e 2 52 ulp( f ) ≤|f | < 2 53 ulp( f ), and for any subnormal floating-point number f ,wehaveulp( f ) = 2 -1074 . / * @ axiomatic FP_ulp { @ logic real ulp ( double f); @ @ axiom ulp_normal1 : \ forall double f ; 0x1p -1022 <= \ abs (f) @= = > \ abs ( f ) < 0x1 . p53 * ulp ( f ); @ axiom ulp_normal2 : \ forall double f ; 0x1p -1022 <= \ abs (f) @ ==> ulp ( f ) <= 0x1 .p-52 * \ abs (f); @ axiom ulp_subnormal : \ forall double f; \abs ( f ) < 0x1p -1022 @ ==> ulp ( f ) == 0x1 .p-1074; @ axiom ulp_pow : \ forall double f; @ \ exists integer i ; ulp ( f ) == \pow (2. , i ); @} * / / * @ requires @ (b==0. if (p+q <= 3 * fabs (p-q)) d=p-q; else { dp=Dekker(b,b,p); dq=Dekker(a,c,q); d=(p-q)+(dp-dq ) ; } return d; }

The generated Coq file contains first some declarations generated from the axiomatic FP_ulp: we fill the definition of ulp with the ulp defined in the support library, and prove the 4 theorems corresponding to the 4 axioms, by 90 lines of proof script.

The remaining of the Coq file contains 17 verification conditions. As the algorithm's proof was already done, these are quite short to do: 150 lines to prove the postcondition (that requires the check of all the overflow/underflow assumptions), 140 lines for the safety proofs (Dekker preconditions and overflows).

Wave Equation Resolution Scheme

To finish the examples, here is a numerical analysis program. This function is a finite difference numerical scheme for the resolution of the one-dimensional acoustic wave equation. Given a rope attached at its two ends, we create a wave by applying a force (initializations). The rope then undulates, its behavior being modelled by some mathematical equations that can be discretized and computed. The mathematical model is the search for a function u from R 2 to R, solution of the differential equation

∂ 2 u(x, t) ∂t 2 -c 2 ∂ 2 u(x, t) ∂ x 2 = 0
knowing initial values of u and its derivative for t = 0. The value u(x, t) gives the position of the rope at the abscissa x and the time t. It is discretized both in space and time with steps ( x, t). The result is a matrix p where

p[i][k]= p k i is
; i ++) { dp = p [ i +1][ k ] -2. * p[ i ][k] + p[i -1][k ]; p[ i ][k+1] = 2. * p[ i ][k] -p[ i ][k-1] + a * dp ; } p[ni ][k+1] = 0.; } return p; }
There are two very different parts to prove the correctness of this program. The first one is the bound on the rounding error. This was done in [START_REF] Boldo | Floats & Ropes: a case study for formal numerical program verification[END_REF] and the corresponding annotated C file is given above. The annotations are particularly decisive here as this proof requires a complex predicate defined in Coq. More precisely, we proved the that p k i -\exact(

p k i ) = k l=0 l j=-l α l j ε k-l i+ j
, where (α) is a constant sequence depending on the wave equation constants and ε is the rounding error made by one iteration of the loop, assuming the inputs are correct. The loop invariant contains both bounds on the ε k i and the fact that the rounding error is exactly defined by the previous formula. This allows us to exhibit the compensation of rounding errors and then have a very good bound, proportional to k 2 for the rounding error of the computed values: as we need to compute k 2 values to obtain p k i ,to obtain an error proportional to k 2 is a first-rate bound.

What is proved is a bound on the rounding error assuming the scheme does not diverge. There are 117 verification conditions and the proofs are about 4,000 lines long. The Coq compilation takes about 1 h and 10 min. Among the 117 verification conditions, there are 84 safety proof obligations that have to do with memory access, variant decrease, overflow, and precondition for function call.

The second part is the proof of the method error. This is a mathematical proof done in [START_REF] Boldo | Formal proof of a wave equation resolution scheme: the method error[END_REF]: it proves that the scheme does not diverge and that the program computes something near the exact solution of the partial differential equation, assuming the rope is infinite. The mathematical method error proof (with an axiom about the finite support of the solution, see [START_REF] Boldo | Formal proof of a wave equation resolution scheme: the method error[END_REF] for more details) is also about 4,000 lines long. The proved bound is the one of the mathematical textbooks, proportional to x 2 + t 2 .

It remains to adapt this last proof for a finite rope and to link the two proofs to try to get rid of axioms. This linking part will notice that the mathematical discretization of the differential equation described in [START_REF] Boldo | Formal proof of a wave equation resolution scheme: the method error[END_REF] is exactly the one of the previous program.

An important question is the re-usability of this proof. The method that expresses exactly p k i -\exact( p k i ) as a mathematical formula is powerful, but not applicable to any program. We think this technique can be applied to several cases of numerical scheme, as used numerical schemes have many mathematical properties, such as stability, that could be used to bound rounding errors. All the correct and practical definitions of the mathematics needed by the method error proof could be reused (about half of the developments), but the proof itself (the other half) heavily depends on the wave equation and the chosen scheme.

Conclusion

We have shown that a very high guarantee on numerical programs is achievable. We have a usable chain from the annotated program to the mathematical theorems that is able to secure a program both from its rounding errors and from its other possible failures (pointer dereferencing, out-of-bound array accesses, overflows…).

A positive point in this approach is that we build upon a highly expressive specification language, which allows to specify arbitrarily complex intended behaviors. Then, thanks to the multiple provers back-end, simple VCs such as the ones coming from overflow checks can be discharged with a fair amount of automation. But also, for complex properties we always have the possibility to switch to Coq and perform complex computer-assisted proofs. Thus, a given specified program can be proved in its deeper details using Coq and its correctness therefore ascertained.

A never-ending perspective is to find cunning techniques to better bound the rounding errors, especially when they compensate. A technique that states the analytical error has been developed in [START_REF] Boldo | Floats & Ropes: a case study for formal numerical program verification[END_REF] for the example of Sect. 3.6 where usual methods gave an error proportional to 2 k that was cut down to k 2 . This technique of the analytical error and precise floating-point error cancellation coming with its formal proof is new. The reason is that it requires very generic specifications as the loop invariant needs to be logically defined: it states there exists a function that has such and such property. And ACSL allows us to express such a high-level property on a C program. We then use Coq as a back-end to formally check the specifications. This genericity is an advantage compared to automatic methods that cannot express our loop invariant.

A fair question to ask is how much of expertise is needed for someone new to this approach to prove its own program from scratch. Important issues need to be addressed to spread the use of deductive verification of floating-point programs.

• First, the appropriate annotations may be hard to find. Unlike tools specialized to some specific property, deductive verification approach offers a very expressive specification language allowing the user to potentially formalize any desired property. Assuming that the programmer has in mind a clear idea of the expected property, a mandatory step is to formalize it in the specification language. This is something that can be learned similarly as programming can be learned. Performing a proof that the program verifies this specification can be difficult too, and is also something that can be learned. One should not try to make a computer-assisted proof before writing a pen and paper proof first, from which the adequate lemmas and/or loop invariants can be discovered. One could not expect a systematic recipe for such a task, however any tool instrumentation could be used, such as first displaying graphs to provide intuitions, or using a tool to compute appropriate bounds like we did with Gappa in some examples. Then turning pen and paper proofs into formal ones allows to uncover the gaps.

• If the program is large, then it is likely that the number of annotations needed will be large too. Known tools that scale up on large programs typically use abstract interpretation techniques with well-chosen domains [START_REF] Cousot | The ASTRÉE analyzer[END_REF][START_REF] Delmas | Towards an industrial use of FLUCTUAT on safety-critical avionics software[END_REF]. These do not need manual annotations but are able to verify only a restricted kind of properties such as: safety (no runtime error), bounds on rounding errors, stability of conditional branching. Our approach aims more at proving complex properties on small programs. Typical applications can be for example the so-called SCADE operators, which are small hand-written subroutines inserted in automatically generated large C codes. In the context of numerical analysis, there are also quite short subroutines that can be proved [START_REF] Boldo | Floats & Ropes: a case study for formal numerical program verification[END_REF]. This emphasizes an important feature of our approach: its modularity. A function is annotated and proved independently from the rest of the program. Modularity allows to cope with libraries of formally verified programs, that can be reused. We believe this is the right path to spread the use of deductive verification.

A promising future work is to make various kind of static analyses to cooperate. For example, the technique of slicing8 reduces a program with respect to a given property to check, such that the property holds on the full program if it holds on the reduced program. There are also promising techniques combining abstract interpretation and weakest preconditions calculus for automatically generating and propagating annotations [START_REF] Moy | Modular inference of subprogram contracts for safety checking[END_REF]. The plug-in architecture of Frama-C allows and even encourages such cooperations. • The annotations may need to be crafted in a particular way to maximize automation. Clearly this requires an advanced understanding of the respective power of various provers. In some examples of this paper, we had to insert assertions to play the role of cuts in the VCs, so that one part is solved by Gappa and others by SMT solvers. An interesting perspective is to turn the Gappa underlying techniques into a decision procedure for a theory of floating-point rounding in a suitable form for SMT solvers. Generally speaking, writing the annotations and performing the proof is an interactive process where some feedback from failing proof must be taken into account to adjust the annotations. Sometimes, trying to complete the proof of a VC in Coq helps to understand why automatic provers fail and gives an idea of an appropriate cut. The final annotated code, as we gave it here for each example, is only the result of such an iterative process and does not show its intermediate steps.

Fig. 1 Fig. 2

 12 Fig. 1 Chain of tools: from the C program to the proof obligations

  float my_cosine ( float x) { return 1.0 fx * x * 0.5 f ; } The first step is to decide what property we want to formally specify. Figure 2 displays the graph of the cosine function, in plain line, and the graph of the polynomial function 1x 2 /2 in dashed line. The difference is classically called the method error.

Figure 3

 3 shows a zoom of the previous graphs on the interval [1/32 -2 -18 , 1/32]. The additional thin line is the graph of the result of the C function my_cosine computed with single-precision floating-point numbers. Each

Fig. 3

 3 Fig. 3 Zoom of Fig. 2 around x = 1/32

Fig. 4 Fig. 5

 45 Fig. 4 Back-end provers

Fig. 6

 6 Fig. 6 Last unproved VC, proved within Coq IDE

  | | 0x1 . p-916 <= \ abs (b * b)) @& & ( a * c==0. | | 0x1 . p-916 <= \ abs (a * c)) @& & \ abs ( b ) <= 0x1 . p510 && \ abs ( a ) <= 0x1 . p995 && \ abs ( c ) <= 0x1 . p995 @& & \ abs (a * c ) <= 0x1 . p1021 ; @ ensures \ result ==0. | | \ abs (\ result -(b * b-a * c)) <= 2. * ulp (\ result ); @ * / double discriminant (double a, double b, double c) { double p,q,d,dp,dq; p=b * b; q=a * c;

  the position of the rope at the abscissa i × x and the time k × t. The matrix p is computed by the following piece of code. For simplicity, annotated initialization functions are omitted. / * @ axiomatic dirichlet { @ predicate analytic_error{L} @( double * * p, integer ni , integer i, integer k, double a) @ reads p[..][..]; } * / / * @ requires ni >= 2 && nk >= 2@& & l ! = 0 @ & &d x>0 .& &d t>0 . & &v>0 . @& & \ exact (dx) > 0. & & \exact (dt) > 0. @& & \ exact ( v)==v @& & \ abs (\ exact (dx) -dx ) / dx <= 0x1 . p-53 @& & \ abs (\ exact (dt) -dt ) / dt <= 0x1 .p-51 @& & 3 . / 5 . < = \ exact (dt )/\exact (dx) * \ exact (v) <= 1-0x1 . p-50 @& & 0 x 1 . p -1000 <= v <= 0x1 . p1000 @ && ni <= 0x1 . p64 && nk <= 4194304 @& & \ exact (dx) <= 1; @ @ ensures \ forall integer i; \forall integer k; @ 0 <= i <= n i ==> 0 <= k <= nk ==> @\ round_error (\ result [ i ][k]) <=78./2 * 0x1.p-52 * (k+1) * (k+2); * / double * * forward_prop ( int ni , int nk , double dx , double dt , double v, double xs , double l) { double * * p; int i, k; double a1 , a , dp ; a1 = dt / dx * v; a= a 1 * a1 ; / * @ assert 1./4 <= a <= 1 && 0 < \ exact (a) <= 1 & & @\ round_error (a) <= 0x1.p-49; * / p = array2d_alloc ( ni+1, nk+1);p[0][0]=0.; / * @ loop invariant 1 <= i <= ni & & analytic_error (p,ni ,i -1,0,a); @ loop variant ni-i; * / for ( i =1; i <ni ; i ++) { p[ i ][0] = p_zero (xs , l , i * dx ) ; } p[ni ][0] =0.; p[0][1] = 0.; / * @ loop invariant 1 <= i <= ni & & analytic_error (p,ni ,i -1,1,a); @ loop variant ni-i; * / for ( i =1; i <ni ; i ++) { dp = p[ i +1][0] -2. * p[ i ][0] + p[i -1][0]; p[ i ][1] = p[ i ][0] + 0.5 * a * dp ; } p[ni ][1] = 0.; / * propagation = time loop * / / * @ loop invariant 1 <= k <= nk & & analytic_error (p,ni ,ni ,k,a); @ loop variant nk-k; * / for ( k=1; k<nk ; k++) { p[0][k+1] = 0.; / * time iteration = space loop * / / * @ loop invariant 1 <= i <= ni & & analytic_error (p,ni ,i-1,k+1,a ); @ loop variant ni-i; * / for ( i =1; i <ni

http://frama-c.cea.fr/.

We use the C99 notation for hexadecimal floating-point literals: 0xhh.hhpdd,whereh are hexadecimal digits and dd is in decimal, denotes number hh.hh × 2 dd ,e.g.0x1.Fp-4 is (1 + 15/16) × 2 -4 .

Available at http://lipforge.ens-lyon.fr/www/pff/.

Although this is not yet well instrumented in Frama-C/Jessie: given the corresponding VC expressed in Gappa, one has to replace the expected bound by a "?" and run Gappa on it directly.

An internal clock was incremented by steps of 0.1 s, and because of rounding errors occuring over time, the drift between that internal clock and the real time prevented the anti-missile to launch, thus causing the death of several soldiers during the Gulf War in 1991. See http://autarkaw.wordpress.com/2008/06/02/round-off-errors-and-the-patriot-missile/ and http://en.wikipedia.org/wiki/ MIM-104_Patriot#Failure_at_Dhahran.

http://frama-c.com/slicing.html.

Acknowledgments

We would like to thank the other people who contributed to the design of the tools and some of the examples: Ali Ayad, for contributions to the floating-point support in Frama-C/Jessie, and examples on approximations on transcendental functions and the clock drift; François Clément, Jean-Christophe Filliâtre, Micaela Mayero and Guillaume Melquiond, for their contribution to the wave equation example; and more generally Guillaume Melquiond for his support on the use of Gappa and the Coq interval tactic.

65Y04

This work was partly funded by the F st (ANR-08-BLAN-0246, http://fost.saclay.inria.fr/)andU3CAT (ANR-08-SEGI-021, http:// frama-c.com/u3cat/) projects of the French national research organization (ANR), and by the Hisseo project (http://hisseo.saclay.inria. fr/) of the Digiteo cluster and the Domaine d'Intérêt Majeur "Logiciel et Systèmes Complexes" of the Île-de-France regional council.

S. Boldo (B) • C. Marché (B)


Sylvain Conchon

Evelyne Contejean

Mohamed Iguernelala

Canonized Rewriting and Ground AC Completion Modulo Shostak Theories ⋆

Keywords: decision procedure, associativity and commutativity, rewriting, AC-completion, SMT solvers, Shostak's algorithm

AC-completion efficiently handles equality modulo associative and commutative function symbols. When the input is ground, the procedure terminates and provides a decision algorithm for the word problem. In this paper, we present a modular extension of ground ACcompletion for deciding formulas in the combination of the theory of equality with user-defined AC symbols, uninterpreted symbols and an arbitrary signature disjoint Shostak theory X. Our algorithm, called AC(X), is obtained by augmenting in a modular way ground AC-completion with the canonizer and solver present for the theory X.T h i si n t e g r a t i o n rests on canonized rewriting, a new relation reminiscent to normalized rewriting, which integrates canonizers in rewriting steps. AC(X) is proved sound, complete and terminating, and is implemented to extend the core of the Alt-Ergo theorem prover.

Introduction

Many mathematical operators occurring in automated reasoning such as union and intersection of sets, or boolean and arithmetic operators, satisfy the following associativity and commutativity (AC) axioms ∀x.∀y.∀z. u(x, u(y, z)) = u(u(x, y),z)( A ) ∀x.∀y. u(x, y)=u(y, x)( C ) Automated AC reasoning is known to be difficult. Indeed, the mere addition of these two axioms to a prover will usually glut it with plenty of useless equalities which will strongly impact its performances 1 . In order to avoid this drawback, built-in procedures have been designed to efficiently handle AC symbols. For instance, SMT-solvers incorporate dedicated decision procedures for some specific AC symbols such as arithmetic or boolean operators. On the contrary, algorithms found in resolution-based provers such as AC-completion allow a powerful generic treatment of user-defined AC symbols.

Given a finite word problem i∈I s i = t i ⊢ s = t where the function symbols are either uninterpreted or AC, AC-completion attempts to transform the conjunction i∈I s i = t i into a finitely terminating, confluent term rewriting system R whose reductions preserve identity. The rewriting system R serves as a decision procedure for validating s = t modulo AC: the equation holds if and only if the normal forms of s and t w.r.t R are equal modulo AC. Furthermore, when its input contains only ground equations, AC-completion terminates and outputs a convergent rewriting system [START_REF] Marché | On ground AC-completion[END_REF].

Unfortunately, AC reasoning is only a part of the automated deduction problem, and what we really need is to decide formulas combining AC symbols and other theories. For instance, in practice, we are interested in deciding finite ground word problems which contain a mixture of uninterpreted, interpreted and AC function symbols, as in the following assertion

u(a, c 2 -c 1 ) ≈ a ∧ u(e 1 ,e 2 ) -f (b) ≈ u(d, d) ∧ d ≈ c 1 +1 ∧ e 2 ≈ b ∧ u(b, e 1 ) ≈ f (e 2 ) ∧ c 2 ≈ 2 * c 1 +1 ⊢ a ≈ u(a, 0)
where u is an AC symbol, +, -, * and the numerals are from the theory of linear arithmetic, f is an uninterpreted function symbol and the other symbols are uninterpreted constants. A combination of AC reasoning with linear arithmetic and the free theory E of equality is necessary to prove this formula. Linear arithmetic is used to show that c 2c 1 = c 1 +1 so that (i) u(a, c 1 +1) = a follows by congruence. Independently, e 2 = b and d = c 1 +1 imply (ii) u(c 1 +1,c 1 +1) = 0 by congruence, linear arithmetic and commutativity of u. AC reasoning can finally be used to conclude that (i)a n d( ii)i m p l yt h a tu(a, c 1 +1,c 1 +1) is equal to both a and u(a, 0). There are two main methods for combining decision procedures for disjoint theories. First, the Nelson-Oppen approach [START_REF] Nelson | Simplification by cooperating decision procedures[END_REF] is based on a variable abstraction mechanism and the exchange of equalities between shared variables. Second, the Shostak's algorithm [START_REF] Shostak | Deciding combinations of theories[END_REF] extends a congruence closure procedure with theories equipped with canonizers and solvers, i.e. procedures that compute canonical forms of terms and solve equations, respectively. While ground AC-completion can be easily combined with other decision procedures by the Nelson-Oppen method, it cannot be directly integrated in the Shostak's framework since it actually does not provide a solver for the AC theory.

In this paper, we investigate the integration of Shostak theories in ground AC-completion. We first introduce a new notion of rewriting called canonized rewriting which adapts normalized rewriting to cope with canonization. Then, we present a modular extension of ground AC-completion for deciding formulas in the combination of the theory of equality with user-defined AC symbols, uninterpreted symbols and an arbitrary signature disjoint Shostak theory X.The main ideas of our integration are to substitute standard rewriting by canonized rewriting, using a global canonizer for AC and X, and to replace the equation orientation mechanism found in ground AC-completion with the solver for X.

AC-completion has been studied for a long time in the rewriting community [START_REF] Lankford | Decision procedures for simple equational theories with permutative axioms: Complete sets of permutative reductions[END_REF][START_REF] Peterson | Complete sets of reductions for some equational theories[END_REF]. A generic framework for combining completion with a generic builtin equational theory E has been proposed in [START_REF] Jouannaud | Completion of a set of rules modulo a set of equations[END_REF]. Normalized completion [START_REF] Marché | Normalized rewriting: an alternative to rewriting modulo a set of equations[END_REF] is designed to use a modified rewriting relation when the theory E is equivalent to the union of the AC theory and a convergent rewriting system S. In this setting, rewriting steps are only performed on S-normalized terms. AC(X) can be seen as an adaptation of ground normalized completion to efficiently handle the theory E when it is equivalent to the union of the AC theory and a Shostak theory X. In particular, S-normalization is replaced by the application of the canonizer of X. This modular integration of X allows us to reuse proof techniques of ground AC-completion [START_REF] Marché | On ground AC-completion[END_REF] to show the correctness of AC(X).

Kapur [START_REF] Kapur | Shostak's congruence closure as completion[END_REF] used ground completion to demystify Shostak's congruence closure algorithm and Bachmair et al. [START_REF] Bachmair | Abstract congruence closure[END_REF] compared its strategy with other ones into an abstract congruence closure framework. While the latter approach can also handle AC symbols, none of these works formalized the integration of Shostak theories into (AC) ground completion.

Outline. Section 2 recalls standard ground AC completion. Section 3 is devoted to Shostak theories and global canonization. Section 4 presents the AC(X) algorithm and illustrates its use through an example. The correctness of AC(X) is sketched in Section 5 and experimental results are presented in Section 6. Conclusion and future works are presented in Section 7.

Ground AC-Completion

In this section, we first briefly recall the usual notations and definitions of [START_REF] Baader | Term Rewriting and All That[END_REF][START_REF] Dershowitz | Rewrite systems[END_REF] for term rewriting modulo AC. Then, we give the usual set of inference rules for ground AC-completion procedure and we illustrate its use through an example.

Terms are built from a signature Σ = Σ AC ⊎ Σ E of AC and uninterpreted symbols, and a set of variables X yielding the term algebra T Σ (X ). The range of letters a...f denotes uninterpreted symbols, u denotes an AC function symbol, s, t, l, r denote terms, and x, y, z denote variables. Viewing terms as trees, subterms within a term s are identified by their positions. Given a position p, s| p denotes the subterm of s at position p,a n ds[r] p the term obtained by replacement of s| p by the term r. We will also use the notation s(p)todenotethe symbol at position p in the tree, and the root position is denoted by Λ.G i v e na subset Σ ′ of Σ, a subterm t| p of t is a Σ ′ -alien of t if t(p) ∈ Σ ′ and p is minimal w.r.t the prefix word ordering2 .W ew r i t eA Σ ′ (t) the multiset of Σ ′ -aliens of t.

A substitution is a partial mapping from variables to terms. Substitutions are extended to a total mapping from terms to terms in the usual way. We write tσ for the application of a substitution σ t oat e r mt. A well-founded quasiordering [START_REF] Dershowitz | Orderings for term rewriting systems[END_REF] on terms is a reduction quasi-ordering if s t implies sσ tσ and l[s] p l[t] p , for any substitution σ,t e r ml and position p. A quasi-ordering defines an equivalence relation ≃ as ∩ and a partial ordering ≺ as ∩ .

An equation is an unordered pair of terms, written s ≈ t.T h ev a r i a b l e s contained in an equation, if any, are understood as being universally quantified. Given a set of equations E, the equational theory of E, written = E ,i st h ese tof equations that can be obtained by reflexivity, symmetry, transitivity, congruence and instances of equations in E3 . The word problem for E consists in determining if, given two ground terms s and t, the equation s ≈ t is in = E , denoted by s = E t. The word problem for E is ground when E contains only ground equations. An equational theory = E is said to be inconsistent when s = E t,f o rany s and t.

A rewriting rule is an oriented equation, usually denoted by l → r.At e r ms rewrites to a term t at position p by the rule l → r, denoted by s → p l→r t,iffthere exists a substitution σ such that s| p = lσ and t = s[rσ] p . A rewriting system R is a set of rules. We write s → R t whenever there exists a rule l → r of R such that s rewrites to t by l → r at some position. A normal form of a term s w.r.t to R is atermt such that s → * R t and t cannot be rewritten by R. The system R is said to be convergent whenever any term s has a unique normal form, denoted s ↓ R , and does not admit any infinite reduction. Completion [START_REF] Knuth | Simple word problems in universal algebras[END_REF] aims at converting a set E of equations into a convergent rewriting system R such that the sets = E and {s ≈ t | s ↓ R = t ↓ R } coincide. Given a suitable reduction ordering on terms, it has been proved that completion terminates when E is ground [START_REF] Lankford | Canonical inference[END_REF].

Rewriting modulo AC. Let = AC be the equational theory obtained from the set:

AC = u∈ΣAC { u(x, y) ≈ u(y, x),u (x, u(y, z)) ≈ u(u(x, y),z) }
In general, given a set E of equations, it has been shown that no suitable reduction ordering allows completion to produce a convergent rewriting system for E ∪ AC.W h e nE is ground, an alternative consists in in-lining AC reasoning both in the notion of rewriting step and in the completion procedure.

Rewriting modulo AC is directly related to the notion of matching modulo AC as shown by the following example. Given a rule u(a, u(b, c))) → t,w ew ould like the following reductions to be possible:

(1) f (u(c, u(b, a)),d) → f (t, d)( 2 ) u(a, u(c, u(d, b))) → u(t, d)
Associativity and commutativity of u are needed in (1) for the subterm u(c, u(b, a)) to match the term u(a, u(b, c)), and in (2) for the term u(a, u(c, u(d, b))) to be seen as u(u(a, u(b, c)),d), so that the rule can be applied. More formally, this leads to the following definition.

Definition 1 (Ground rewriting modulo AC). Ate r ms rewrites to a term t modulo AC at position p by the rule l → r, denoted by s → p AC\l→r t,i ff(1) s| p = AC l and t = s[r] p or (2) l(Λ)=u and there exists a term s ′ such that

s| p = AC u(l, s ′ ) and t = s[u(r, s ′ )] p
In order to produce a convergent rewriting system, ground AC-completion requires a well-founded reduction quasi-ordering total on ground terms with an underlying equivalence relation which coincides with = AC . Such an ordering will be called a total ground AC-reduction ordering. The inference rules for ground AC-completion are given in Figure 1. The rules describe the evolution of the state of a procedure, represented as a configuration E | R ,w h e r eE is a set of ground equations and R a ground set of rewriting rules. The initial state is E 0 |∅ where E 0 is a given set of ground equations. Tri vial removes an equation u ≈ v from E when u and v are equal modulo AC. Orient turns an equation into a rewriting rule according to a given total ground AC-reduction ordering . R is used to rewrite either side of an equation (Simplify), and to reduce right hand side of rewriting rules (Compose). Given ar u l el → r, Collapse either reduces l at an inner position, or replaces l by a term smaller than r. In both cases, the reduction of l to l ′ may influence the orientation of the rule l ′ → r w h i c hi sa d d e dt oE as an equation in order to be re-oriented. Finally, Deduce adds equational consequences of rewriting rules to E. For instance, if R contains two rules of the form u(a, b) → s and u(a, c) → t, then the term u(a, u(b, c)) can either be reduced to u(s, c)ort ot het ermu(t, b). The equation u(s, c) ≈ u(t, b), called critical pair, is thus necessary for ensuring convergence of R. Critical pairs of a set of rules are computed by the following function (a µ stands for the maximal term w.r.t. size enjoying the assertion):

Trivial E ∪{s ≈ t }|R E | R s =AC t Orient E ∪{s ≈ t }|R E | R ∪{s → t } t ≺ s Simplify E ∪{s ≈ t }|R E ∪{s ′ ≈ t }|R s → AC\R s ′ Compose E | R ∪{l → r } E | R ∪{l → r ′ } r → AC\R r ′ Collapse E | R ∪{g → d, l → r } E ∪{l ′ ≈ r }|R ∪{g → d } l → AC\g→d l ′ g ≺ l ∨ (g ≃ l ∧ d ≺ r) Deduce E | R E ∪{s ≈ t }|R s ≈ t ∈ headCP(R)
headCP(R)= u(b, r ′ ) ≈ u(b ′ ,r) l → r ∈ R, l ′ → r ′ ∈ R ∃ a µ : l = AC u(a µ ,b) ∧ l ′ = AC u(a µ ,b ′ )
Example. To get a flavor of ground AC-completion, consider a modified version of the assertion given in the introduction, where the arithmetic part has been removed (and uninterpreted constant symbols renamed for the sake of simplicity)

u(a 1 ,a 4 ) ≈ a 1 ,u(a 3 ,a 6 ) ≈ u(a 5 ,a 5 ),a 5 ≈ a 4 ,a 6 ≈ a 2 ⊢ a 1 ≈ u(a 1 ,u(a 6 ,a 3
))

The precedence a 1 ≺ p ••• ≺ p a 6 ≺ p u defines an AC-RPO ordering on terms [START_REF] Nieuwenhuis | A precedence-based total AC-compatible ordering[END_REF] which is suitable for ground AC-completion. The table in Figure 2 shows the application steps of the rules given in Figure 1 from an initial configuration {u(a 1 ,a 4 ) ≈ a 1 ,u(a 3 ,a 6 ) ≈ u(a 5 ,a 5 ),a 5 ≈ a 4 ,a 6 ≈ a 2 }|∅ to a final configuration ∅ | R f ,w h e r eR f is the set of rewriting rules {1, 3, 5, 7, 10}.I tcanbe checked that a 1 ↓ R f and u(a 1 ,u(a 6 ,a 3 )) ↓ R f are identical. Fig. 2. Ground AC-completion example

Shostak Theories and Global Canonization

In this section, we recall the notions of canonizers and solvers underlying Shostak theories and show how to obtain a global canonizer for the combination of the theories E and AC with an arbitrary signature disjoint Shostak theory X.

From now on, we assume given a theory X with a signature Σ X . A canonizer for X is a function can X that computes a unique normal form for every term such that s = X t iff can X (s)=can X (t). A solver for X is a function solve X that solves equations between Σ X -terms. Given an equation s ≈ t, solve X (s ≈ t) either returns a special value ⊥ when s ≈ t ∪ X is inconsistent, or an equivalent substitution. A Shostak theory X is a theory with a canonizer and a solver which fulfill some standard properties given for instance in [START_REF] Krstić | Canonization for disjoint unions of theories[END_REF].

Our combination technique is based on the integration of a Shostak theory X in ground AC-completion. From now on, we assume that terms are built from as i g n a t u r eΣ defined as the union of the disjoint signatures Σ AC , Σ E and Σ X . We also assume a total ground AC-reduction ordering defined on T Σ (X )u s e d later on for completion. The combination mechanism requires defining both a global canonizer for the union of E,A Ca n dX, and a wrapper of solve X to handle heterogeneous equations. These definitions make use of a global one-toone mapping α : T Σ →X (and its inverse mapping ρ) and are based on a variable abstraction mechanism which computes the pure Σ X -part [[t]] of a heterogeneous term t as follows:

[[ t]] = f ([[s]] ) w h e n t = f (s)a n df ∈ Σ X and [[t]] = α(t)o t h e r w i s e
The canonizer for AC defined in [START_REF] Hullot | Associative commutative pattern matching[END_REF] is based on flattening and sorting techniques which simulate associativity and commutativity, respectively. For instance, the term u(u(u ′ (c, b),b),c)isfirstflattenedtou(u ′ (c, b),b,c) and then sorted 4 to get the term u(b, c, u ′ (c, b)). It has been formally proved that this canonizer solves the word problem for AC [START_REF] Contejean | A certified AC matching algorithm[END_REF]. However, this definition implies a modification of the signature Σ AC where arity of AC symbols becomes variadic. Using such canonizer would impact the definition of AC-rewriting given in Section 2. In order to avoid such modification we shall define an equivalent canonizer that builds degenerate trees instead of flattened terms. For instance, we would expect the normal form of u(u(u ′ (c, b),b),c)t ob eu(b, u(c, u ′ (c, b))). Given a signature Σ which contains Σ AC and any total ordering on terms, we define can AC by:

can AC (x)= x when x ∈X can AC (f (v)) = f (can AC (v)) when f ∈ Σ AC can AC (u(t 1 ,t 2 )) = u(s 1 ,u(s 2 ,...,u(s n-1 ,s n ) ...))
where

t ′ i = can AC (t i )f o ri ∈ [1, 2] and { {s 1 ,...,s n } } = A {u} (t ′ 1 ) ∪A {u} (t ′ 2 ) and s i s i+1 for i ∈ [1,n-1]when u ∈ Σ AC
We can easily show that can AC enjoys the standard properties required for a canonizer. The proof that can AC solves the word problem for AC follows directly from the one given in [START_REF] Contejean | A certified AC matching algorithm[END_REF].

Using the technique described in [START_REF] Krstić | Canonization for disjoint unions of theories[END_REF], we define our global canonizer can which combines can X with can AC as follows:

can(x)= x when x ∈X can(f (v)) = f (can(v)) when f ∈ Σ E can(u(s, t)) = can AC (u(can(s), can(t))) when u ∈ Σ AC can(f X (v)) = can X (f X ([[can(v)]]))ρ when f X ∈ Σ X
Again, the proofs that can solves the word problem for the union E,A Ca n dX and enjoys the standard properties required for a canonizer are similar to those given in [START_REF] Krstić | Canonization for disjoint unions of theories[END_REF]. The only difference is that can AC directly works on the signature Σ, which avoids the use of a variable abstraction step when canonizing a mixed term of the form u(t 1 ,t 2 ) such that u ∈ Σ AC .

Using the same mappings α, ρ and the abstraction function, the wrapper solve can be easily defined by:

solve(s ≈ t)= ⊥ if solve X ([[s]] ≈ [[ t]] ) = ⊥ { x i ρ → t i ρ } if solve X ([[s]] ≈ [[ t]] ) = {x i ≈ t i }
In order to ensure termination of AC(X), the global canonizer and the wrapper must be compatible with the ordering used by AC-completion, that is:

Lemma 1. ∀t ∈T Σ , can(t) t ∀s, t ∈T Σ , if solve(s ≈ t)= {p i → v i } then v i ≺ p i
We can prove that the above properties hold when the theory X enjoys the local compatibility properties:

Axiom 1. ∀t ∈T Σ , can X ([[t]] ) [[ t]] ∀s, t ∈T Σ , if solve X ([[s]] ≈ [[ t]] ) = {x i ≈ t i } then t i ρ ≺ x i ρ
To fulfil this axiom, AC-reduction ordering can be chosen as an AC-RPO ordering [START_REF] Nieuwenhuis | A precedence-based total AC-compatible ordering[END_REF] based on a precedence relation ≺ p such that Σ X ≺ p Σ E ∪ Σ AC .F r o m now on, we assume that X is locally compatible with .

Example. To solve the equation u(a, b)+a ≈ 0, we use the abstraction α = {u(a, b) → x, a → y} and call solve X on x + y ≈ 0. Since a ≺ u(a, b), the only solution which fulfills the axiom above is {x ≈-y}. We apply ρ and get the set {u(a, b) →-a} of rewriting rules.

4 Ground AC-Completion Modulo X

In this section, we present the AC(X) algorithm which extends the ground ACcompletion procedure given in Section 2. For that purpose, we first adapt the notion of ground AC-rewriting to cope with canonizers. Then, we show how to refine the inference rules given in Figure 1 to reason modulo the equational theory induced by a set E of ground equations and the theories E,A Ca n dX.

Canonized Rewriting

From rewriting point of view, a canonizer behaves like a convergent rewriting system: it gives an effective way of computing normal forms. Thus, a natural way for integrating can in ground AC-completion is to extend normalized rewriting [START_REF] Marché | Normalized rewriting: an alternative to rewriting modulo a set of equations[END_REF]. Lemma 2. ∀ s, t. s l→r t =⇒ s = AC,X,l≈r t

The AC(X) Algorithm

The first step of our combination technique consists in replacing the rewriting relation found in completion by canonized rewriting. This leads to the rules of AC(X) given in Figure 3. The state of the procedure is a pair E | R of equations and rewriting rules. The initial configuration is E 0 |∅ where E 0 is supposed to be a set of equations between canonized terms. Since AC(X)'s rules only involve canonized rewriting, the algorithm maintains the invariant that terms occurring in E and R are in canonical forms. Tri vial thus removes an equation u ≈ v from E when u and v are syntactically equal. A new rule Bottom is used to detect inconsistent equations. Similarly to normalized completion, integrating the global canonizer can in rewriting is not enough to fully extend ground ACcompletion with the theory X: in both cases the orientation mechanism has to be adapted . Therefore, the second step consists in integrating the wrapper solve in the Orient rule. The other rules are much similar to those of ground AC-completion except that they use the relation R instead of → AC\R .

Trivial E ∪{s ≈ t }|R E | R s = t Bottom E ∪{s ≈ t }|R ⊥ solve(s, t)=⊥ Orient E ∪{s ≈ t }|R E | R ∪ solve(s, t) solve(s, t) = ⊥ Simplify E ∪{s ≈ t }|R E ∪{s ′ ≈ t }|R s R s ′ Compose E | R ∪{l → r } E | R ∪{l → r ′ } r R r ′ Collapse E | R ∪{g → d, l → r } E ∪{l ′ ≈ r }|R ∪{g → d } l g→d l ′ g ≺ l ∨ (g ≃ l ∧ d ≺ r) Deduce E | R E ∪{s ≈ t }|R s ≈ t ∈ headCP(R)
Fig. 3. Inference rules for ground AC-completion modulo X Example. We illustrate AC(X) on the example given in the introduction:

1 u(a, c2 -c1) → a Ori u(a, c2 -c1) ≈ a 2 u(e1,e2) → u(d, d)+f (b) Ori u(e1,e2) -f (b) ≈ u(d, d) 3 d → c1 + 1 Ori d ≈ c1 +1 4 u(e1,e2) → u(c1 +1,c1 +1)+f (b) Com 2a n d3 5 e2 → b Ori e2 ≈ b 6 u(b, e1) ≈ u(c1 +1,c1 +1)+f (b) Col 4a n d5 7 u(b, e1) → u(c1 +1,c1 +1)+f (b) Ori u(b, e1) ≈ u(c1 +1,c1 +1)+f (b) 8 u(c1 +1,c1 +1)+f (b) ≈ f (b) Sim u(b, e1) ≈ f (e2)b y5a n d7 9 u(c1 + 1, c1 + 1) → 0 Ori u(c1 +1,c1 +1)+f (b) ≈ f (b) 10 u(b, e1) → f (b) Com 7a n d9 11 c2 → 2 * c1 + 1 Ori c2 ≈ 2 * c1 +1 12 u(a, c1 +1)≈ a Col 1a n d1 1 13 u(a, c1 + 1) → a Ori u(a, c1 +1)≈ a 14 u(0,a) ≈ u(a, c1 +1
u(a, c 2 -c 1 ) ≈ a ∧ u(e 1 ,e 2 ) -f (b) ≈ u(d, d) ∧ d ≈ c 1 +1 ∧ e 2 ≈ b ∧ u(b, e 1 ) ≈ f (e 2 ) ∧ c 2 ≈ 2 * c 1 +1 ⊢ a ≈ u(a, 0)
The table given in Figure 4 shows the application of the rules of AC(X) on the example when X is instantiated by linear arithmetic. We use an AC-RPO ordering based on the precedence 1

≺ p 2 ≺ p a ≺ p b ≺ p c 1 ≺ p c 2 ≺ p d ≺ p e 1 ≺ p e 2 ≺ p f ≺ p u.
The procedure terminates and produces a convergent rewriting system R f = {3, 5, 9, 10, 11, 13, 16}.U si n gR f ,w ec a nc h e c kt h a ta and u(a, 0) can-rewrite to the same normal form.

Correctness

As usual, in order to enforce correctness, we cannot use any (unfair) strategy. We say that a strategy is strongly fair when no possible application of an inference rule is infinitely delayed and Orient is only applied over fully reduced terms.

Theorem 1. Given a set E of ground equations, the application of the rules of AC(X) under a strongly fair strategy terminates and either produces ⊥ when E ∪ AC ∪ X is inconsistent, or yields a final configuration ∅|R such that:

∀s, t ∈T Σ .s= E,AC,X t ⇐⇒ can(s) R = can(t) R
The proof5 is based on three intermediate theorems, stating respectively soundness, completeness and termination. In the following, we shall consider a fixed run of the completion procedure,

E 0 |∅ → E 1 | R 1 →... → E n | R n → E n+1 | R n+1 →...
starting from the initial configuration E 0 |∅ .W ed e n o t eR ∞ (resp. E ∞ )t h e set of all encountered rules n R n (resp. equations n E n )a n dR ω (resp. E ω ) the set of persistent rules n i≥n R i (resp. equations n i≥n E i ).

Soundness

Soundness is ensured by the following invariant:

Theorem 2. For any configuration E n | R n reachable from E 0 |∅ , ∀ s, t, (s, t) ∈ E n ∪ R n =⇒ s = AC,X,E0 t
Proof. The invariant obviously holds for the initial configuration and is preserved by all the inference rules. The rules Simplify, Compose, Collapse and Deduce preserve the invariant since for any rule l → r,i fl = AC,X,E0 r, for any term s rewritten by l→r into t,t h e ns = AC,X,E0 t.I fOrie n ti su s e dt ot u r na n equation s ≈ t into a set of rules {p i → v i }, by definition of solve,

p i = x i ρ and v i = t i ρ,w h e r esolve X ([[s]] ≈ [[ t]] ) = {x i ≈ t i } . By soundness of solve X x i = X,[[ s]] ≈[[ t]] t i . An equational proof of x i = X,[[ s]] ≈[[ t]
] t i can be instantiated by ρ, yielding an equational proof p i = X,s≈t v i . Since by induction s = AC,X,E0 t holds, we get p i = AC,X,E0 v i .

In the rest of this section, we assume that the strategy is strongly fair. This implies in particular that headCP(R ω ) ⊆ E ∞ , E ω = ∅ and R ω is inter-reduced, that is none of its rules can be collapsed or composed by another one. We also assume that ⊥ is not encountered, otherwise, termination is obvious.

Completeness

Completeness is established by using a variant of the technique introduced by Bachmair et al. in [START_REF] Bachmair | Orderings for equational proofs[END_REF] for proving completeness of completion. It transforms a proof between two terms which is not under a suitable form into a smaller one, and the smallest proofs are the desired ones. The proofs we are considering are made of elementary steps, either equational steps, with AC, X and E ∞ ,o r rewriting steps, with R ∞ and the additional (possibly infinite) rules R can = {t → can(t) | can(t) = t}. Rewriting steps with R ∞ can be either R∞ or → R∞6 . The measure of a proof is the multiset of the elementary measures of its elementary steps. The measure of an elementary step takes into account the number of terms which are in a canonical form in an elementary proof: the canonical weight of a term t, w can (t)i se q u a lt o0i fcan(t)= AC t and to 1 otherwise. Notice that if w can (t)=1 ,t h e ncan(t) ≺ t,a n di fw can (t)=0 ,t h e n can(t) ≃ t. The measure of an elementary step between t 1 and t 2 performed thanks to:

-an equation is equal to ({t 1 ,t 2 }, , , , ) -ar u l el → r ∈ R ∞ is equal to ({t 1 }, 1,w can (t 1 )+w can (t 2 ),l,r)i ft 1 l→r t 2 or t 1 → l→r t 2 . -ar u l eo fR can is equal to ({t 1 }, 0,w can (t 1 )+w can (t 2 ),t 1 ,t 2 )i ft 1 → Rcan t 2 .
As usual the measure of a step s ← t is the measure of t → s.E l e m e n t a r ys t e p s are compared lexicographically using the multiset extension of for the first component, the usual ordering over natural numbers for the components 2 and 3, and for last ones. Since is an AC-reduction ordering, the ordering defined over proofs is well-founded.

The general methodology is to show that a proof which contains some unwanted elementary steps can be replaced by a proof with a strictly smaller measure. Since the ordering over measures is well-founded, there exists a minimal proof, and such a minimal proof is of the desired form.

Termination

We shall prove that, under a strongly fair strategy, R ω is finite and obtained in a finite time (by cases on the head function symbol of the rule's left-hand side), and then we show that R ω will clean up the next configurations and the completion process eventually halts on ∅|R ω . In order to make our case analysis on rules, and to prove the needed invariants, we define several sets of terms (assuming without loss of generality that E 0 = can(E 0 )):

T 0 = {t |∃t 0 ,e 1 ,e 2 ∈T Σ (X ),e 1 ≈ e 2 ∈ E 0 and t 0 = e i | p and t 0 *

R∞ t} T 0X = T 0 ∪{f X (t 1 ,...,t n ) | f X ∈ Σ X and ∀i, t i ∈ T 0X } T 1 = {t | t ∈ T 0 and ∀p, t| p ∈ T 0X } T 2 = {u(t 1 ,...,t n ) | u ∈ Σ AC and ∀i, t i ∈ T 1 }
T 0 is the set of all terms and subterms in the original problem as well as their reducts by R ∞ .T h es e tT 0X moreover contains terms with X-aliens in T 0 . T 1 is the set of terms that can be introduced by X from terms of T 0 (by solving or canonizing). T 2 is a superset of the terms built by critical pairs. We first establish by structural induction over terms that:

∀γ, t, s, γ ∈ R ∞ ∩ T 2 j ∧ t ∈ T i ∧ t γ s =⇒ s ∈ T i , for i, j =1, 2
Then, by induction over n, we show that any configuration

E n | R n accessible from E 0 |∅ after n steps is such that E n ∪ R n ⊆ T 2 1 ∪ T 2 2 .
The fact that R ∞ is finitely branching is a corollary of Lemma 4. If l → r n is created at step n in R n and l → r m at step m in R m , with n<m,t h e nr m is a reduct of r n by R∞ .

The proof of this lemma is by induction over the length of the derivation, and by a case analysis over the applied inference rule. Theorem 4. Under a strongly fair strategy, AC(X) terminates.

By the above properties

, R ω can be divided in R ω ∩ T 2 1 and R ω ∩ T 2 2 . R ω ∩ T 2 1
is finite, since all its left-hand sides are reducts of a finite number of terms by R ∞ which is well-founded and finitely branching. R ω ∩ T 2 2 is finite by using the same argument as in the ground AC-completion proof, based on the Higman's lemma. Hence R ω is finite and obtained in a finite number of steps, that is, there exists n such that R ω ⊆ R n .T h e nR ω will clean the rest of E n ,a n dt h en e w l y generated critical pairs will be discarded as trivial ones.

Experimental Results

AC(X) has been implemented in the Alt-Ergo [START_REF] Conchon | The Alt-Ergo theorem prover[END_REF] theorem prover. In this section, we show that this extension has strong impact both on performances and memory allocation w.r.t. an axiomatic approach. For that purpose, we benchmarked our implementation and compared its performances with state-of-the-art smt solvers (Z3 v2.8, CVC3 v2.2, Simplify v1.5.4). All measures were obtained on a laptop running Linux equipped with a 2.58GHz dual-core Intel processor a n dw i t h4 Gb main memory. Provers were given a time limit of five minutes for each test and memory limitation was managed by the system. The results are given in seconds; we write to for timeout and om for out of memory.

Our test suite is made of formulas which are valid in the combination of the theory of linear arithmetic A, the free theory of equality7 E and a small part of the theory of sets defined by the symbols ∪, ⊆, the singleton constructor {•}, and the following set of axioms:

AC Assoc : ∀x, y, z. x ∪ (y ∪ z) ≈ (x ∪ y) ∪ z Commut : ∀x, y. x ∪ y ≈ y ∪ x S ⎧ ⎪ ⎪ ⎨ ⎪ ⎪ ⎩ SubTrans : ∀x, y, z. x ⊆ y → y ⊆ z → x ⊆ z SubSuper : ∀x, y, z. x ⊆ y → x ⊆ y ∪ z SubUnion : ∀x, y, z. x ⊆ y → x ∪ z ⊆ y ∪ z SubRefl : ∀x. x ⊆ x
In order to get the most accurate information from our benchmarks, we classify formulas in three categories according to the subset of axioms needed to prove their validity. We use the standard mathematical notation d i=1 a i for the terms of the form a The first column contains the results for Alt-Ergo when we explicitly declare ∪ as an AC symbol and remove the AC axioms from the problem. In the second column, we do not take advantage of AC(X) and keep the AC axioms in the context. Figures 5 and6 show that, contrary to the axiomatic approach, built-in AC reasoning is little sensitive to the depth of terms: given a number n of equations, the running time is proportional to the depth d of terms. However, we notice a slowdown when n increases. This is due to the fact that AC(X) has to process a quadratic number of critical pairs generated from the equations in the hypothesis. From Fig. 7, we notice that Alt-Ergo with AC(X) performs better than the other provers. The main reason is that its instantiation mechanism is not spoiled by the huge number of intermediate terms the other provers generate when they instantiate the AC axioms.

1 ∪ (a 2 ∪ (•••∪a d )) •••)andw ewrite d i=1 a i ; b for terms of the form a 1 ∪ (a 2 ∪ (•••∪(a d ∪ b))) •••).

Conclusion and Future Works

We have presented a new algorithm AC(X) which efficiently combines, in the ground case, the AC theory with a Shostak theory X and the free theory of equality. Our combination consists in a tight embedding of the canonizer and the solver for X in ground AC-completion. The integration of the canonizer relies on a new rewriting relation, reminiscent to normalized rewriting, which interleaves canonization and rewriting rules. We proved correctness of AC(X) by reusing standard proof techniques. Completeness is established thanks to a proofs' reduction argument, and termination follows the lines of the proof of ground AC-completion where the finitely branching result is adapted to account for the theory X. AC(X) has been implemented in the Alt-Ergo theorem prover. The first experiments are very promising and show that a built-in treatment of AC, in the combination of the free theory of equality and a Shostak theory, is more efficient than an axiomatic approach. Although effective, the integration of AC(X) in Alt-Ergo fails to prove the formula (∀x, y, z.P ((x ∪ y) ∪ z)) ∧ b ≈ c ∪ d → P (a ∪ b) since the trigger for the internal quantified formula (the term (x∪y)∪z)) does not match the term a ∪ b, even when exploiting the ground equation b = c ∪ d which allows to match the term a ∪ (c ∪ d)). Introducing explicitly the AC axioms for ∪ would allow the matcher to generate the ground term (a ∪ c) ∪ d that could be matched. However, as shown by our benchmarks, too many terms are generated with these axioms in general. In order to fix this problem, we intend to extend the pattern-matching algorithm of Alt-Ergo to exploit both ground equalities and properties of AC symbols. In the near future, we also plan to extend AC(X) to handle the AC theory with unit or idempotence. This will be a first step towards a decision procedure for a substantial part of the finite sets theory.

Fig. 1 .

 1 Fig. 1. Inference rules for ground AC-completion

Definition 2 .

 2 Let can be a canonizer. A term s can-rewrites to a term t at position p by the rule l → r, denoted by s p l→r t,i ff s → p AC\l→r t ′ and can(t ′ )=t Example. Using the usual canonizer can A for linear arithmetic and the rule γ : u(a, b) → a,t h et e r mf (a +2 * u(b, a)) can A -rewrites to f (3 * a)b y γ as follows: f (a +2 * u(b, a)) → AC\γ f (a +2 * a)a n dcan A (f (a +2 * a)) = f (3 * a).

) 15 Fig. 4 .

 154 Fig. 4. AC(X) on the running example

  Formulas in the first category are of the form: validity only requires the theory E and the AC properties of ∪. The second category contains formulas additionally involving linear arithmetic:n p=1 ({t p -p}∪ d i=1 a p i ) ≈ b p ∧ n-1 p=1 t p +1≈ t p+1 → GFormulas in the third category involve the ⊆ symbol and are of the form: n p=1 d i=1 {e p i }≈b p ∧ d i=d {e + e p i }≈c p ∧ e ≈ 0 → n p=1 c p ⊆ (b p ∪{e p d }) ∪{e} In order to prove their validity, we additionally need some axioms of S.T h e results of the benchmarks are shown in Fig. 5, Fig. 6 and Fig 7.

Fig. 7 .

 7 Fig. 7. AC + E + A + S

  Lemma 3. A proof containingan elementary step ←→ s≈t ,w h e r es ≈ t ∈ AC ∪ X ∪ E ∞ , -or an elementary rewriting step truly of the form -→ R∞ or ←-R∞ ,o r l→r or r←l ,w h e r el→ r ∈ R ∞ \ R ω or a peak s ← Rcan t → Rcan s ′ , s Rω t Rω s ′ ,o rs Rω t -→ Rcan s ′ is not minimal. Theorem 3. If s and t are two terms such that s ←→ * AC,X,E∞,R∞ s ′ then can(s) Rω = can(t) Rω .Proof. If s and s ′ are equal modulo ←→ * AC,X,E∞,R∞ ,s oa r ecan(s)a n dcan(s ′ ). By the above lemma, a minimal proof between can(s)andcan(s ′ ) is necessary of the form can(s)( Rω ∪→ Rcan ) * ( Rω ∪← Rcan ) * can(s ′ ). This sequence of steps can also be seen as can(s) → * Rcan ( Rω → * Rcan ) * (← * Rcan cannot follow a Rω -step, and can(s)a n dcan(s ′ ) cannot be reduced by → Rcan , hence the wanted result.

	definition, →	Rcan	Rω ) * ← * Rcan can(s ′ ). By

Notice that according to this definition, a variable may be a Σ ′ -alien.

The equational theory of the free theory of equality E , defined by the empty set of equations, is simply denoted =.

For instance, using the AC-RPO ordering based on the precedence b ≺p c ≺p u ′ .

All the details of the proof can be found in a research report[START_REF] Conchon | Canonized Rewriting and Ground AC Completion Modulo Shostak Theories[END_REF].

Here,s -→ R∞ t actually means s -→ AC\R∞ t ′ and t = canAC(t ′ ).

These two theories are built-in for all SMT solvers we used for our benchmarks.

by the French ANR project ANR-08-005 Decert.