Computer-Assisted Verification of Four Interval Arithmetic Operators

This contribution is a mechanical proof of an implementation of the four operators, which verifies mainly three properties: validity (“the results conform to the definition of intervals”), soundness (“the results enclose every possible real values”) and tightness (“the resulting enclosures are optimal/tightest”). Our verification result indicates that the operators, which compute with the bounds of operand intervals and return the hull of computed results, satisfy the three properties.

To complete the proof, we propose several techniques to specify/verify the target interval operations and their properties. First, through an examination of each unproved VC, we find that specifying an additional lemma will help the Alt-Ergo SMT solver to discharge the VC. For instance, for a VC on FP numbers, a lemma on reals involving the same expression as the VC may help to discharge it. We identify 19 lemmas needed for the complete verification. Second, we propose a specification of the tightness property of an interval computation such that the code annotated with the property is verified by SMT solvers. In this specification, it is essential to reformulate the interval hull operation with a consideration of NaN.

We note that the target of above techniques is not limited to interval arithmetic operations but applicable to various proof tasks in the numerical domain, e.g., verification of other interval functions and application programs.

Section 2 introduces basic notions and concepts of interval arithmetic. Section 3 explains the main tools for verification: Why3 and Alt-Ergo. The following sections describe the main verification process for an interval arithmetic code. First, Section 4 gives an overview of the process. Second, Section 5 explains the specification of the target code. Next, Section 6 and Section 7 describe the processes of annotating the pre- and postconditions to the code and discharging the generated proof obligations. Section 8 reports the complete results of the verification experiment.

Why3 (version 1.1.0) [4, 5] is a platform for deductive program verification, which provides: (i) a specification language WhyML to describe programs and specifications; (ii) a verification condition (VC) generator that applies weakest precondition calculus to the annotated programs; and (iii) a proof intermediate interface that facilitates discharging the VCs using the back-end automated/interactive theorem provers. Why3’s back-end theorem provers include SMT solvers, e.g., Alt-Ergo [7], CVC4 and Z3,⁸⁸8Alt-Ergo: https://alt-ergo.ocamlpro.com/; CVC4: https://cvc4.github.io/; Z3: https://github.com/Z3Prover/z3 and theorem proof assistants, e.g., Coq.⁹⁹9https://coq.inria.fr/ The possible results of applying an automated prover to discharge a VC are valid, invalid, timeout (within a configured time limit), or unknown. Why3 provides a GUI to allow users to browse a list of generated VCs. Users assign a back-end prover to each VC to validate it. When provers cannot validate a VC, users are able to modify the VC (e.g., split one VC into several VCs) and investigate a prover’s input/output though the GUI.

WhyML is an OCaml-like language to describe functional programs and to annotate programs with first-order predicate logic statements. The language has a type system, which provides the type real for real numbers, types for FP numbers, user-defined record types, etc. WhyML also has a module system that encapsulates specification as a module; basic modules are supplied in the standard library. There are two implementations of 64-bit FP numbers: the type t provided by the ieee_float.Float64 module and the type double of the floating_point.DoubleFull module. Running examples in this paper uses the former, which has been introduced in a recent version of Why3; it is compatible with the FloatingPoint theory of SMT-LIB and processed by dedicated solvers when the VCs are discharged with SMT solvers. The latter realizes a theory of FP numbers based on the theory of reals and the generated VCs are encoded with the predicates on reals. The two modules provide arithmetic operators (with rounding mode control) and comparison operators that conform to IEEE-754. FP numbers are related to real numbers using the rounding functions and translation functions provided by either module.

Alt-Ergo (version 2.2.0) [7] is an SMT solver, which shares various features with Why3. For example, Alt-Ergo has a trigger mechanism that allows users to guide the solver towards the proof, using a user-defined lemma. In WhyML, auxiliary lemmas can be specified with triggers and they are utilized by Alt-Ergo. In our experiments, with the help of several user-defined lemmas, Alt-Ergo discharged the most VCs.

A user of Why3 verifies a program through performing the following tasks.

Specification of the target code, properties and lemmas. The user implements the target code in the WhyML language and annotates the properties to the code as preconditions and postconditions. Here, requirements for the code should be better represented as simple and generic properties; however, such properties tend to require more efforts to verify. In our work, we investigate an intuitive yet provable representation of the tightness property (cf. Theorem 1). Also, the user is able to annotate properties about intermediate states by inserting assert formulas in the middle of the code, and specify lemmas related to the properties besides the code. These auxiliary annotations will help automated deductions performed by provers like Alt-Ergo.

Generation of VCs and proving with back-end provers. Once an annotated WhyML program is fed to the Why3 tool, a set of VCs are generated; discharging them all entails the correctness of the annotated program. The user is able to modify the VCs by applying logical transformations; for example, s/he can split a VC into several VCs which are easier to prove. Then, s/he applies a prover to each VC to check its validity. In this work, we first apply SMT solvers, i.e., Alt-Ergo and Z3, and then invoke the Coq tool for manual proving.

Analysis on unprovable VCs and modification of the specification. When VCs are not provable, the user returns to the specification task to modify either the target code or the annotations. Since the automated proving processes of VCs are incomplete in general, they may fail to prove VCs even for a correct specification. In such cases, the user should make an effort in finding a specification that results in provable VCs. Here, an interactive proof task with Coq may help to understand the proof context and to identify an additional lemma that is useful to discharge the proof goal. In this work, we actually make such analyses; as a result, we insert assertions within the code and specify lemmas to help Alt-Ergo’s proof process.

We consider interval operations as procedures that handle data of the interval type, which is specified in a dedicated Why3 module (Figure 1) named Interval; related constants, predicates and lemmas are also specified in this module. In Figure 1, first, the modules for real numbers and FP numbers are imported at Lines 2–4; these modules provide type real, type Float64.t (double-precision FP number), and related types, constants, operators and predicates (some of them are summarized in Table 1). Most of them are specified by a set of WhyML axioms, e.g., the operator .<= is specified as follows.

The Float64Ex module imported at Line 4 is our own module that provides auxiliary vocabularies for FP numbers (some are shown in Table 1). Second, the type interval is defined at Line 6 as a record combining the lower (inf) and upper (sup) bounds of type Float64.t. Third, the predicate real_in is defined at Lines 8–10 to state $a\in{\bm{x}}$ where $a\in\mathbb{R}$ and ${\bm{x}}\in\mathbb{IF}$. Fourth, the module specifies a constant interval zeroI, i.e., a point-wise interval containing 0. It is specified using the is_zero predicate instead of specifying a concrete interval to represent either of intervals whose bounds are $-0$ or $+0$. At Line 15, there is a lemma characterizing zeroI, which may be used in an automated proof process. In the rest of the specification (Lines 17–22), the predicate valid x to state the validity of the value x of type interval is specified. For instance, it is used in the precondition $P_{V}$ to state that ${\bm{x}}\in\mathbb{IF}$. Then, two lemmas using valid are specified; valid_not_nan states that the bounds of valid intervals are not $\mathrm{NaN}$; valid_zeroI states the validity of the constant specified above. Lemmas in a WhyML module are proved by Why3’s back-end provers. The three lemmas specified so far are proved using Alt-Ergo, where each proof takes less than 0.2s.

Interval multiplication code written as a WhyML function multiply is shown in Figure 2; only five branches are shown due to space limitations, but the full specification consists of 13 branches. At Lines 2–5, necessary modules are imported. Multiplication is defined by the WhyML function multiply at Lines 7–22. The procedure is specified as a nested if-then statement and the expressions inside are specified with predefined vocabularies for FP numbers and intervals.

In this work, one major modification was made against the codebase of the kv library (version 0.4.38). In the modification, Lines 11 and 15 of the code in Figure 2 were simplified; Line 11 of the original code was implemented as follows.

Line 11 corresponds to the case where ${\bm{x}}=[0,0]$ and the modified code results in $[0,0]$, whereas the original code checks whether a ${\bm{y}}$’s bound is $\pm\infty$ and returns either $[-\infty,+\infty]$ or $[0,0]$. Line 15 is likewise for switched ${\bm{x}}$ and ${\bm{y}}$. Thus, the code comprises 17 branches. Our verification result suggests that the original code of kv unnecessarily enlarges some results from $[0,0]$ to $[-\infty,+\infty]$, which is not correct regarding our tightness property. The original code is correct in terms of the cset model [11] but it is not clear whether this design choice was made or not (cf. the code does not support divisions by an interval containing zero). Based on our interval arithmetic flavor (Section 2), our code is simplified and results in tighter intervals yet it is verified to be correct.

We annotate the multiply function in Figure 2 with the properties in Section 4. The following pre- and postconditions, which encode $P_{V}$, $Q_{V}$ and $Q_{S}$ of Definition 2, respectively, are inserted at Line 8 of the code. ¹⁰¹⁰10The variable result is a built-in variable that represents the resulting value ${\bm{r}}$ (Definition 2) of the function under verification.

Next, we generate a proof obligation (i.e., a set of VCs) for the function multiply using the Why3 tool and try to discharge (i.e., prove the validity of) the VCs using one of the back-end SMT solvers. This process can be easily performed through the Why3 GUI. Here, two VCs for the postconditions are generated. However, for these VCs, neither proof process of Alt-Ergo and Z3 does terminate after 10min. For that case, we can split the VC into 26 partial VCs (again through Why3’s GUI), each of which corresponds to one of the 13 branches and one of the two postconditions; discharging them all entails the validity of the original VC. We apply Alt-Ergo to prove the split VCs; it discharges 13 of them and leaves 13 VCs unproved.

To prove the remaining VCs, we try to prove them interactively using the Coq proof assistant. An interactive proof is pessimistic due to complication of the VCs involving intervals and FP numbers, which requires a number of rewritings to accomplish the proof.¹¹¹¹11In a Coq proof context, FP numbers are formalized by real numbers with additional data; vocabularies for intervals and FP numbers are defined and characterized based on reals and integers. For instance, rewriting a context by applying a lemma on real numbers requires to unfold the definitions of the vocabularies used in the context, which additionally requires a number of rewritings. The proof of such VCs are performed by SMT solvers more efficiently by automating the rewritings when their search strategies are sufficient. However, this interaction is useful to identify an auxiliary lemma that is helpful for SMT solvers. Indeed, for the VCs under consideration, we find that the following lemma is useful for the proof with Alt-Ergo.

By adding this lemma within the same module, two of the unproved VCs¹²¹²12Each unproved VC corresponds to the third branch shown in Figure 2 and either $Q_{V}$ or $Q_{S}$, respectively. are discharged using Alt-Ergo. The above lemma assumes the branching condition in Figure 2 (in reals) and describes a magnitude relation between the products of the pairs of reals. The same lemma is considered in the proof in [14]. The lemma will be regarded as a relation between the branching condition and the resulting state, when the variables are converted to the Float64.t type. The lemma is difficult to prove with SMT solvers because of the nonlinear terms but it is proved with Coq.¹³¹³13It is simply proved by the tactic “auto with real.” In this way, a proof task involving nonlinear term is done manually. Likewise, all of the unproved VCs are discharged with four additional lemmas and finally the soundness of multiply is proved. Overall, Alt-Ergo takes 243s to discharge the 26 VCs. Z3 is able to discharge four of them.

To specify the postcondition $Q_{T}$, we introduce the functions min4 and max4, which correspond to (the first cases of) the $\mathsfit{min}$ and $\mathsfit{max}$ operations in Theorem 1; these functions take the four candidate bounds and evaluate to the minimum/maximum of them while ignoring $\mathrm{NaN}$; they evaluate to $\mathrm{NaN}$ when all the arguments are $\mathrm{NaN}$. Specification of min4 is shown in Figure 3, which is actually described in the Float64Ex module; max4 is specified in the same way. First, the min2 function that compares two FP numbers is specified (Lines 1–2). min2 ignores $\mathrm{NaN}$ given as an argument so that the expression min2 x y evaluates to x when y evaluates to $\mathrm{NaN}$. Second, the min4 function is simply specified with min2 (Line 4). To support deductions when min4 is used, we also specify six lemmas including min4_feq (Lines 6–8), min4_fle (Lines 10–12) and min4_feq_w (Lines 14–16) in Figure 3. The first two lemmas state the relations between the value of min4 and the arguments that are not $\mathrm{NaN}$; they are respectively proved by Alt-Ergo in 7s and 0.5s. The last four lemmas state possible resulting values of min4 expressions, which are equivalent to one of the arguments w, x, y and z; these four lemmas are respectively proved by Alt-Ergo in 0.4s. The descriptions “[min4 w x y z]” specify the trigger of a lemma, which enforces to assume the lemma when a min4 predicate becomes true.

Before annotating $Q_{T}$, we specify the conditions for the second cases of Equation (2) in Theorem 1, which hold when the four candidate bounds become NaN; these cases only happen in multiplication. The condition for $\mathsfit{min}$ is specified as a predicate in the IntervalMul module as follows (the condition for $\mathsfit{max}$ is specified likewise as mul_nan_case_sup).

Then, the pre- and postconditions $P_{V}$ and $Q_{T}$ are specified as follows.

Here, $Q_{T}$ is specified in three parts. The first and second parts describe the first cases of Equation (2) using the min4 and max4 functions, each of which specifies the lower or upper bound portion of $Q_{T}$. The third part describes the second cases of Equation (2) in conjunction because they only happen at the same time.

The first and second postconditions are transformed into 26 VCs (with three split operations) and Alt-Ergo discharges 22 of them; 4 VCs are left unproved after 10min. The third postcondition is transformed into a VC and discharged by Alt-Ergo in 0.5s.

After investigation of the remaining VCs, we have found that the following lemma helps Alt-Ergo to prove the VCs generated from the first postcondition.

The lemma details the relation between the lower bound of the result and zero. The premise extracts the unproved two branches, each of which corresponds to a remaining VC; for example, one of the VCs corresponds to the third branch in Figure 2, where $\texttt{x.inf}\geq 0$ and $\texttt{y.inf}\geq 0$ hold and the lower bound of the result is computed as mul_down x.inf y.inf. We presume that applying round explicitly on both sides of the consequent inequality facilitates unifying it with expressions specified in the ieee_float module and thus further deductions are invoked. Another lemma mul_up_negative_finite is specified likewise for the second postcondition. In our experiment with Alt-Ergo, the two lemmas are proved in 0.2s and the 26 VCs generated from the target code are proved in 308s.

Each operator was implemented as a WhyML function (see B for some details). The number of branches in each function is shown in the second column of Table 2. Each function was annotated with the conditions $P_{V}$, $Q_{V}$, $Q_{S}$ and $Q_{T}$ (the code for division was also annotated with $Q_{Z}$). Since the “NaN case” described in Section 7.2 only happened in multiplication, $Q_{T}$ was translated as two postconditions (“Q_T lb” and “Q_T ub” without preconditioning) for the other three operators. In the experiment, we identified that additional lemmas were necessary for the verification (the numbers of such lemmas are shown in the third column of Table 2). First, two variations of the lemma in Section 7.3 were needed to verify $Q_{T}$ for each operator code. Second, the subtraction code was annotated with an assert formula to detail a property of the resulting value. Third, the multiplication and division codes were also annotated with four and seven lemmas, respectively, which were the variations of the lemma in Section 6.2; here, the seven lemmas for division include the four lemmas for multiplication. There were 19 lemmas specified in total. Other than the operator code, two WhyML modules, Float64Ex and Interval were prepared, which contained 30 and three lemmas about FP numbers and intervals, respectively.

We performed an experiment to verify the implementation of four operators and all of them were successfully verified. The experiments (including the running examples) were operated using a 2.2GHz Intel Xeon E5-2650v4 processor with 128GB of RAM. The following tools were used: Why3 1.1.0, Alt-Ergo 2.2.0, Coq 8.8.0 and Z3 4.7.1. The memory used was limited to 4GB and the time to 10min for each VC proof.

Why3’s split strategy allows splitting VCs in several degrees. Therefore, the verification was performed with three settings: Without using the split strategy (“No split”); with splitting VCs as many times as possible (“Split full”); with an optimal number of splittings that requires minimum CPU time (“Split optimal”). Note that splitting a VC does not always result in VCs that are discharged by SMT solvers more efficiently than the original.

Herein, we present the experimental results in Table 2. The first three columns represent the target operator (“Op.”), the number of branches (“# Br’s”) and the number of additional lemmas (“# Lm’s”). The data “$m$+$n$” indicates that $m$ lemmas were discharged with SMT solvers and $n$ lemmas were proved with Coq (only the VCs generated from the former are taken into account in the following columns). The following columns are separated for each of the settings described above; for each section, the number of generated VCs (“# VCs”) and the total execution time by Alt-Ergo (“Time”) are shown. “TO ($n$)” (for “Time Out”) means that the proofs for $n$ VCs did not finish within 10min. Note that the verification of the division code succeeded only with the “Split optimal” setting.

Additionally, 33 lemmas in the Float64Ex and Interval modules were discharged by Alt-Ergo in 32.6s in total. We also tried to discharge the “Split full” VCs with Z3, which was less efficient in our experiment; for each operator, 1/8, 1/10, 48/100 and 2/33 VCs were proved, respectively, and the rest resulted in timeout.

Why3 provides an extract function that generates an executable code from a WhyML code. Using this function, we extracted an OCaml code that implements the interval type and the four operators. The extraction of numerical programs with Why3 required additional implementations. First, we prepared an OCaml module for FP arithmetic operations with rounding mode control. We implemented the rounding operators in C, which were then interfaced with OCaml functions of the dedicated Round module. Second, we extended Why3’s extract function to support the Float64.t type and related constants/functions. For this purpose, we prepared a driver file that defines various translation rules.