1: %
2: %
3: %
4: %
5: %
6: %
7: %
8: %
9: %
10: %
11: %
12: %
13: %
14: %
15:
16: %
17:
18: %
19:
20: %
21: %
22: \documentclass[acmnow]{acmtrans2m}
23: %
24:
25: \usepackage[latin9]{inputenc} \usepackage[T1]{fontenc}
26:
27: \usepackage[english]{babel}
28: \usepackage{amsmath}
29: \usepackage{amsfonts}
30: \usepackage{amssymb}
31: \usepackage{fancybox}
32: \usepackage{url}
33: %
34: \usepackage{graphicx}
35: \usepackage{xypic}
36: \usepackage{multicol}
37: \usepackage{rotating}
38: %
39: \usepackage{listings}
40:
41: \def\runningfoot{\def\@runningfoot{.}}
42: \def\firstfoot{\def\@firstfoot{.}}
43:
44: %
45:
46: \begin{document}
47:
48: \title{Certification of bounds on expressions involving rounded operators}
49: \markboth{Marc Daumas and Guillaume Melquiond}{Certification of bounds on expressions involving rounded operators}
50:
51: \author{%
52: Marc Daumas \\
53: {\sc lirmm} ({\sc umr} 5506 {\sc cnrs}--{\sc um}2), {\rm visiting} {\sc éliaus} ({\sc éa 3679 upvd})
54: \and
55: Guillaume Melquiond \\
56: {\sc lip (umr 5668 cnrs--éns} {\rm Lyon}--{\sc inria)}
57: }
58:
59: \category{G.4}{Mathematical Software}{Certification and Testing}
60: \terms{Interval Arithmetic, Floating Point, Proof System}
61:
62: \keywords{Forward error analysis, Dyadic fraction, Coq, PVS, HOL Light, Proof obligation}
63:
64: \begin{abstract}
65: Gappa uses interval arithmetic to certify bounds on mathematical
66: expressions that involve rounded as well as exact operators. Gappa
67: generates a theorem with its proof for each bound treated. The
68: proof can be checked with a higher order logic automatic proof
69: checker, either Coq or HOL Light, and we have developed a large
70: companion library of verified facts for Coq dealing with the
71: addition, multiplication, division, and square root, in fixed- and
72: floating-point arithmetics. Gappa uses multiple-precision dyadic
73: fractions for the endpoints of intervals and performs forward error
74: analysis on rounded operators when necessary. When asked, Gappa
75: reports the best bounds it is able to reach for a given expression
76: in a given context. This feature is used to quickly obtain
77: coarse bounds. It can also be used to identify where the set of
78: facts and automatic techniques implemented in Gappa becomes
79: insufficient. Gappa handles seamlessly additional properties
80: expressed as interval properties or rewriting rules in
81: order to establish more intricate bounds. Recent work showed that
82: Gappa is perfectly suited to the proof of correctness of small
83: pieces of software. Proof obligations can be written by
84: designers, produced by third-party tools or obtained by overloading
85: arithmetic operators.
86: \end{abstract}
87:
88: %
89: %
90: %
91: %
92:
93:
94: \maketitle
95: \newcommand{\R}{\mathbb{R}}
96: \newcommand{\Z}{\mathbb{Z}}
97: \newcommand{\IF}{\mathbb{IF}}
98: \renewcommand{\circ}{\texttt{rnd}}
99: \newcommand{\ulp}{\texttt{ulp}}
100: \newcommand{\circe}[1]{\texttt{err}_{\texttt{rnd},#1}}
101: \newcommand{\circa}{\texttt{err}_{\texttt{rnd}, \texttt{abs}}}
102: \newcommand{\circr}{\texttt{err}_{\texttt{rnd}, \texttt{rel}}}
103:
104: \lstset{basicstyle=\tt\small,xleftmargin=1cm,numberstyle=\tiny}
105:
106: \section{Introduction}
107:
108:
109:
110: Gappa is a simple and efficient tool to certify bounds in computer
111: arithmetic~\cite{Rev06} and in the engineering of numerical
112: software~\cite{DinLauMel06,MelPio07,DauGio07} and hardware~\cite{MicTisVey06}.
113: Gappa bounds arithmetic expressions on real and rational numbers and
114: their evaluations in computers on fixed- and floating-point data
115: formats. Properties that are most often needed involve:
116: \begin{itemize}
117: \item ranges of rounded expressions to prevent exceptional behaviors
118: (overflow, division by zero, and so on),
119: \item ranges of absolute and/or relative errors to characterize the
120: accuracy of results. %
121: \end{itemize}
122:
123: %
124: %
125: %
126: %
127: %
128: %
129: %
130: %
131: %
132: %
133: %
134: %
135: %
136: %
137: %
138: %
139: %
140: %
141: %
142: %
143: %
144: %
145:
146: To the best of our knowledge, Gappa is a tool that was missing in
147: computer arithmetic and related research areas. On one hand, Gappa is
148: not the first tool able to certify static ranges and error
149: bounds. Two other projects are currently mixing interval arithmetic
150: and automatic proof checking \cite{GamMan04,DauMelMun05}. The first
151: one uses ACL2 \cite{KauManMoo2K} and the second one uses PVS
152: \cite{OwrRusSha92}. Gappa is, however, the first tool able to certify
153: these bounds when the program relies on advanced numerical recipes
154: like error compensation, iterative refinement, {\em etc}.
155:
156: On the other hand, countless efficient algorithms use symbolic
157: computation or interval arithmetic to produce bounds on expressions
158: but seldom provide gateways to automatic proof checkers. The
159: continuing work on interval arithmetic \cite{Neu90,JauKieDidWal01} has
160: created a huge set of useful techniques to deliver accurate answers in
161: a reasonable time. Each technique is adapted to a specific class of
162: problems and most evaluations yield accurate bounds only if they are
163: handled by the appropriate techniques in the appropriate order.
164: Blending interval arithmetic and properties on dyadic fractions has
165: also been heavily used in computer arithmetic \cite{RumOgiOis05}.
166:
167: %
168: %
169: %
170: %
171: %
172:
173: %
174: %
175: %
176: %
177: %
178: %
179: %
180:
181: %
182: %
183: %
184: %
185: %
186: %
187: %
188: %
189: %
190: %
191: %
192:
193: %
194: %
195: %
196: %
197: %
198: %
199:
200: %
201:
202: %
203: %
204: %
205: %
206:
207: %
208: %
209:
210: %
211: %
212: %
213: %
214: %
215: %
216: %
217: %
218:
219: %
220: %
221: %
222: %
223:
224: Integration is certainly the challenge that prevented the development
225: of competitors to Gappa. Proofs generated by Gappa typically contain
226: 4,800 of lines \cite{DinLauMel06} and related projects were not able
227: to avoid the development of small programs, for example to generate a
228: proof script about 9,935 intervals each requiring 3 theorems in PVS
229: \cite{DauMelMun05}. The functionalities of Gappa presented here show
230: its potential in tackling generic problems that are unreachable with
231: other available tools. Our goal is to
232: \begin{itemize}
233: \item Provide {\em invisible formal methods} \cite{TiwShaRus03} in the
234: sense that Gappa delivers formal certificates to users that are not
235: expected to ever write any piece of proof in any formal proof
236: system.
237: \item Provide a tool that is able to consider and combine many techniques using
238: interval arithmetic, dyadic fractions, and rewriting rules. Gappa
239: performs an exhaustive search on its built-in set of facts and
240: techniques. It is also able to follow hints given by users to take
241: into account new techniques.
242: \item Simplify a valid proof once it has been produced in order to
243: reduce the certification time, as in-depth proof checking is and
244: will remain much slower than simple C++ evaluation.
245: \item Provide a tool appropriate to meet the highest Common Criteria
246: Evaluated Assurance Level (EAL~7) \cite{Sch03,Roc05} for numerical
247: applications using floating- and fixed-point arithmetics.
248: \end{itemize}
249:
250: Gappa is composed of two parts. First, a program written in C++, based
251: on Boost interval arithmetic library~\cite{BroMelPio03} and
252: MPFR~\cite{FouHanLefPelZim05}, verifies numeric properties given by the
253: user. Along these verifications, it generates formal certificates of
254: their validity. Second, a companion library provides theorems with
255: computable hypotheses. This set of theorems allows a proof assistant to
256: interpret the formal certificates and hence to automatically check the
257: validity of the numeric properties. The proof assistant we use is
258: Coq~\cite{HueKahPau04}, but ongoing work shows that Gappa can generate
259: formal certificates for other proof assistants such as HOL
260: Light~\cite{Har2Kb}.
261:
262: %
263: %
264: %
265: %
266: %
267: %
268: %
269: %
270: %
271: %
272: %
273: %
274:
275: We first describe the input language of Gappa and we detail its built-in
276: rewriting rules. We then present the set of theorems and interval
277: operators Gappa relies on to prove numeric properties and we describe
278: how it interacts with proof checkers, extending \cite{DauMel04}. We
279: finish this report with perspectives, experiments, and concluding
280: remarks.
281:
282: \section{Description of the input language of Gappa}
283:
284: Consider for example that $y$ is the result of a portion of code
285: without loops and branches. The definition of $y$ is an expression
286: involving rounded operators and rounded constants. We may define $Y$
287: (uppercase) as the exact answer without any rounding error. The
288: expression $Y$ is identical to $y$ except that rounded operators are
289: replaced by exact operators and rounded constants are replaced by
290: exact constants. If some numeric terms were considered negligible and
291: were optimized out of the implementation $y$, these terms are
292: introduced in $Y$. So the expression $y$ gives the effectively
293: computed value while the expression $Y$ gives the ideal value $y$
294: tries to approximate.
295:
296: In order to certify the correctness of this code, we will possibly need
297: \begin{itemize}
298: \item an interval containing all the possible values of $y$ to guarantee
299: that $y$ does not overflow and produces no invalid value,
300: \item an interval containing all the possible values of $y - Y$ or $(y
301: - Y)/Y$ to guarantee that $y$ is accurate and close to $Y$.
302: \end{itemize}
303:
304: The grammar of the input language to Gappa is presented in
305: Figure~\ref{fig/gram}. It has been designed to efficiently express
306: such needs. An input file is composed of three parts: a set of aliases
307: ({\tt PROG}, detailed in Section~\ref{sub/prog}), the proposition to
308: be proved ({\tt PROP}, detailed in Section~\ref{sub/prop}) and a set
309: of hints ({\tt HINTS}, detailed in Sections~\ref{sub/hints} and
310: \ref{sub/subp}). When successful, Gappa produces a Coq or a HOL Light
311: file with the proof of {\tt PROP}. Its validity can be checked by Coq
312: using the companion library and by HOL Light using a set of axioms
313: until a companion library becomes available.
314:
315: \begin{sidewaysfigure}
316: \begin{center}
317: \begin{multicols}{2}
318: \small
319: \begin{verbatim}
320: 0 $accept: BLOB $end
321: 1 BLOB: PROG '{' PROP '}' HINTS
322: 2 PROP: REAL LE SNUMBER
323: 3 | REAL IN '[' SNUMBER ',' SNUMBER ']'
324: 4 | REAL IN '?'
325: 5 | REAL GE SNUMBER
326: 6 | PROP AND PROP
327: 7 | PROP OR PROP
328: 8 | PROP IMPL PROP
329: 9 | NOT PROP
330: 10 | '(' PROP ')'
331: 11 SNUMBER: NUMBER
332: 12 | '+' NUMBER
333: 13 | '-' NUMBER
334: 14 FUNCTION_PARAM: SNUMBER
335: 15 | IDENT
336: 16 FUNCTION_PARAMS_AUX: FUNCTION_PARAM
337: 17 | FUNCTION_PARAMS_AUX ',' FUNCTION_PARAM
338: 18 FUNCTION_PARAMS: /* empty */
339: 19 | '<' FUNCTION_PARAMS_AUX '>'
340: 20 FUNCTION: IDENT FUNCTION_PARAMS
341: 21 EQUAL: '='
342: 22 | FUNCTION '='
343: 23 PROG: /* empty */
344: 24 | PROG IDENT EQUAL REAL ';'
345: 25 | PROG '@' IDENT '=' FUNCTION ';'
346:
347:
348: 26 REAL: SNUMBER
349: 27 | IDENT
350: 28 | FUNCTION '(' REALS ')'
351: 29 | REAL '+' REAL
352: 30 | REAL '-' REAL
353: 31 | REAL '*' REAL
354: 32 | REAL '/' REAL
355: 33 | '|' REAL '|'
356: 34 | SQRT '(' REAL ')'
357: 35 | FMA '(' REAL ',' REAL ',' REAL ')'
358: 36 | '(' REAL ')'
359: 37 | '+' REAL
360: 38 | '-' REAL
361: 39 REALS: REAL
362: 40 | REALS ',' REAL
363: 41 DPOINTS: SNUMBER
364: 42 | DPOINTS ',' SNUMBER
365: 43 DVAR: REAL
366: 44 | REAL IN NUMBER
367: 45 | REAL IN '(' DPOINTS ')'
368: 46 DVARS: DVAR
369: 47 | DVARS ',' DVAR
370: 48 HINTS: /* empty */
371: 49 | HINTS REAL IMPL REAL ';'
372: 50 | HINTS REALS '$' DVARS ';'
373: 51 | HINTS '$' DVARS ';'
374: 52 | HINTS REAL '~' REAL ';'
375: \end{verbatim}
376: \end{multicols}
377: \caption{Grammar of the input language to Gappa generated by {\tt byson}}
378: \label{fig/gram}
379: \end{center}
380: \end{sidewaysfigure}
381:
382: %
383: %
384: %
385: %
386: %
387:
388: %
389: %
390: %
391: %
392: %
393: %
394: %
395:
396: %
397: %
398: %
399: %
400: %
401: %
402: %
403:
404: \subsection{Formalizing the proposition ({\tt PROP}) that Gappa proves}
405: \label{sub/prop}
406:
407: The proposition ({\tt PROP}) that Gappa is expected to prove is
408: written between brackets~({\tt \{ \}}) as presented below and it may
409: contain any conjunction ({\tt AND} token: \verb+/\+),
410: disjunction~({\tt OR} token: \verb+\/+), implication ({\tt IMPL}
411: token: {\tt ->}) or negation ({\tt NOT} token: {\tt not}) of
412: enclosures of expressions. Enclosures are either inequalities ({\tt
413: LE} or {\tt GE} tokens: {\tt <=} or {\tt >=}) or bounded ranges
414: ({\tt IN} token: {\tt in}) on expressions ({\tt REAL}). Ranges may be
415: left unspecified by using question marks (\verb+?+) instead of
416: intervals. Endpoints of intervals and bounds of inequalities are
417: numerical constants ({\tt SNUMBER}).
418: \begin{lstlisting}
419: { x - 2 in [-2,0] /\ (x + 1 in [0,2] -> y in [3,4])
420: -> not x <= 1 \/ x + y in ? }
421: \end{lstlisting}
422: Expressions ({\tt REAL}) may contain constants ({\tt SNUMBER}),
423: identifiers ({\tt IDENT}), user-defined as well as built-in rounding
424: operators ({\tt FUNCTION}), and arithmetic operators (addition,
425: subtraction, multiplication, division, absolute value, square root,
426: negation, and fused multiply and add).
427:
428: The goal of Gappa is to prove the whole logical proposition, assuming
429: that undefined identifiers ($x$ and $y$ in the example above) are
430: universally quantified over the set of real numbers. If question marks
431: are used in some expression enclosures, Gappa suggests intervals for these
432: enclosures such that the proposition can be proved. In the example
433: above, Gappa suggests $x + y \in [3,5]$, which happens to be the
434: tightest interval such that the proposition holds true. Question marks
435: are not allowed if they induce unspecified hypotheses once
436: transformations of Section~\ref{sub/work-on-prop} have been applied.
437:
438: As Gappa stores interval endpoints as dyadic fractions, it produces an
439: error message when a goal contains an interval so tight that it has to
440: be replaced with an empty interval. For example, Gappa is unable to
441: prove the goal {\tt 13/10 in [1.3,1.3]}, as the empty set is the biggest
442: representable subset of the set $\{1.3\}$.
443:
444: The fact that bounds are numerical constants is not a strong
445: limitation to the use of Gappa. For example, linear dependencies on
446: intervals can be introduced by manipulating expressions: the
447: enclosure $y - Y \in [-i\times 10^{-6}, i\times 10^{-6}]$ is not
448: allowed, but the enclosure $(y - Y)/i \in [-10^{-6}, 10^{-6}]$ is.
449:
450: \subsection{Definitions of aliases to describe the behavior of programs ({\tt PROG})}
451: \label{sub/prog}
452:
453: Typing large expressions in the proposition ({\tt PROP} seen
454: Section~\ref{sub/prop}) would not be practical for proof obligations
455: generated from actual pieces of software. Aliases ({\tt IDENT}) of
456: expressions ({\tt REAL}) are defined by constructions of the form
457: {\tt IDENT = REAL}. {\tt IDENT} becomes available for later
458: definitions, the proposition, and the hints. This construction is neither
459: an equality nor an affectation but rather an alias. Gappa uses {\tt
460: IDENT} for its outputs and in the formal proof instead of machine
461: generated names. An identifier cannot be aliased more than once, even
462: if the right hand sides of both aliases are equivalent. Neither can it
463: be aliased after having been used as an unbound variable. For example
464: {\tt b = a * 2; a = 1;} is not allowed.
465:
466: Rounding operators are used in the arithmetic expressions describing
467: the behavior of numerical codes. They are real functions yielding
468: rounded values according to the target data format (\texttt{precision}
469: and \texttt{minimum\_exponent}, or \texttt{lsb\_weight}) and a
470: predefined rounding mode amongst the ones presented
471: Table~\ref{tab/dir}. For modes that are not defined by IEEE 754
472: standard \cite{Ste.87} and its forthcoming revision, see
473: \cite{EveSei99,BolMel05} and references herein. Floating- and
474: fixed-point rounding operators can be expressed with the following
475: operators where rounding parameters ({\tt FUNCTION\_PARAMS}) are
476: listed between angle brackets:
477: \begin{lstlisting}[xleftmargin=0cm]
478: float< precision, minimum_exponent, rounding_direction >(...)
479: fixed< lsb_weight, rounding_direction >(...)
480: \end{lstlisting}
481:
482: The syntax above can be abbreviated for the floating-point formats of
483: Table~\ref{tab/for} and for (fixed-point) integer arithmetic:
484: \begin{lstlisting}[xleftmargin=0cm]
485: float< name, rounding_direction >(...)
486: int< rounding_direction >(...)
487: \end{lstlisting}
488:
489: Aliases are permitted for rounding operators. Their definitions are
490: prefixed by the '@' sign. Line 1 below defines the {\tt rnd} function
491: as rounding to nearest using IEEE 754 standard for 32 bit
492: floating-point data. The example shows various
493: ways of expressing rounded operations using the alternate constructions
494: of {\tt EQUAL}. When all the arithmetic
495: operations on the right hand side of an alias are followed by the same
496: rounding operator (as visible Line 2), this operator can be put once
497: and for all on the left of the equal symbol (as presented Line 3). On
498: this example, Gappa even complains that $y$ and $z$ are two
499: different names for the same expression.
500: \begin{lstlisting}[numbers=left]
501: @rnd = float< ieee_32, ne>;
502: y = rnd(x * rnd(1 - x));
503: z rnd= x * (1 - x);
504: \end{lstlisting}
505:
506:
507: \begin{table}[htbp]
508: \caption{Rounding modes available in Gappa}
509: \label{tab/dir}
510: \begin{center}
511: \begin{tabular}{|c|l|c|} \hline
512: Alias & Meaning \\ \hline
513: \tt zr & toward zero \\
514: \tt aw & away from zero \\
515: \tt dn & toward minus infinity (down) \\
516: \tt up & toward plus infinity \\
517: \tt od & to odd mantissas \\
518: \tt ne & to nearest, tie breaking to even mantissas \\
519: \tt no & to nearest, tie breaking to odd mantissas \\
520: \tt nz & to nearest, tie breaking toward zero \\
521: \tt na & to nearest, tie breaking away from zero \\
522: \tt nd & to nearest, tie breaking toward minus infinity \\
523: \tt nu & to nearest, tie breaking toward plus infinity \\ \hline
524: \end{tabular}
525: \end{center}
526: \end{table}
527:
528: \begin{table}[htbp]
529: \caption{Predefined floating-point formats available in Gappa}
530: \label{tab/for}
531: \begin{center}
532: \begin{tabular}{|c|l|c} \hline
533: Alias & Meaning \\ \hline
534: \tt ieee\_32 & IEEE-754 single precision \\
535: \tt ieee\_64 & IEEE-754 double precision \\
536: \tt ieee\_128 & IEEE-754 quadruple precision \\
537: \tt x86\_80 & 80 bit extended precision \\ \hline
538: \end{tabular}
539: \end{center}
540: \end{table}
541:
542: %
543: %
544: %
545:
546: %
547: %
548:
549: %
550:
551:
552: %
553: %
554: %
555: %
556: %
557:
558: %
559:
560: Most truncated hardware operators \cite{Tex97} and some compound
561: operators cannot be described as if they were first computed to infinite
562: precision and then rounded to target precision. For such operators we revert to
563: under-specified functions that produce results with a known bound on
564: the relative error.
565: \begin{lstlisting}[xleftmargin=0cm]
566: {add|sub|mul}_rel< precision [, minimum_exponent] >(..., ...)
567: \end{lstlisting}
568: If a minimum exponent is provided, Gappa does not instantiate any
569: assumption that involves a result with an exponent below the minimum
570: exponent. Otherwise, the error bound always holds and the absolute
571: error is 0 when the result is 0.
572:
573: \subsection{Rewriting expressions to suppress some dependency effects (first use of {\tt HINT})}
574: \label{sub/hints}
575:
576: Let $Y$ be an expression and $y$ an approximation of $Y$ due to
577: round-off errors, for example. The absolute error is $y - Y$ and the
578: relative error is $(y - Y) / Y$. As soon as Gappa has computed some ranges
579: for $y$ and $Y$, it naively computes an enclosing interval of $y - Y$
580: and $(y - Y) / Y$ using theorems on subtraction and division of
581: intervals.
582:
583: Unfortunately, expressions $y$ and $Y$ are strongly correlated and
584: error ranges computed that way are useless. To suppress some
585: dependency effects and reproduce many of the techniques used in
586: numerical analysis and in computer
587: arithmetic~\cite{Kah65,Hig02,BolDau04b,DinDefLau04}, Gappa manipulates
588: error expressions through a set of built-in pattern-matching as well
589: as user-defined rewriting rules.
590:
591: We assume that $y = \circ(a + b)$ and $Y = A + B$. Gappa rewrites
592: the absolute error $\circ(a + b) - (A + B)$ as $(\circ(a + b) - (a +
593: b)) + ((a + b) - (A + B))$. It finds an enclosure of the first term
594: using a theorem on the $\circ$ rounding operator. For the second term,
595: Gappa performs a second rewrite: $(a + b) - (A + B)$ is equal to $(a -
596: A) + (b - B)$. This rewriting rule gives sensible results, as long as
597: $a$ and $b$ are close to $A$ and $B$ respectively.
598:
599:
600: \begin{table}
601: \caption{Built-in rewriting rules available in Gappa}
602: \label{tab/rules}
603: $$
604: \begin{array}{| c | c | c | c |} \hline
605: \text{Rule} & \text{Before} & \text{After} & \text{Condition} \\ \hline
606: \texttt{opp\_mibs} & -a - -b & -(a - b) & a \neq b \\
607: \texttt{opp\_mibs} & (-a - -b) / -b & (a - b) / b & b \neq 0 \land a \neq b \\
608: \texttt{add\_xals} & a + b & (a - A) + (A + b) & \\
609: \texttt{add\_xars} & c + a & (c + A) + (a - A)) & \\
610: \texttt{add\_mibs} & (a + b) - (c + d) & (a - c) + (b - d) & a \neq c \land b \neq d \\
611: \texttt{add\_fils} & (a + b) - (a + c) & b - c & b \neq c \\
612: \texttt{add\_firs} & (a + b) - (c + b) & a - c & a \neq c \\
613: \texttt{sub\_xals} & a - b & (a - A) + (A - b) & a \neq b \land A \neq b \\
614: \texttt{sub\_xars} & b - a & (b - A) + -(a - A) & b \neq a \\
615: \texttt{sub\_mibs} & (a - b) - (c - d) & (a - c) + -(b - d) & a \neq c \land b \neq d \\
616: \texttt{sub\_fils} & (a - b) - (a - c) & -(b - c) & b \neq c \\
617: \texttt{sub\_firs} & (a - b) - (c - b) & a - c & a \neq c \\
618: \texttt{mul\_xals} & a b & (a - A) b + A b & \\
619: \texttt{mul\_xars} & b a & b (a - A) + b A & \\
620: \texttt{mul\_fils} & a b - a c & a (b - c) & b \neq c \\
621: \texttt{mul\_firs} & a c - b c & (a - b) c & a \neq b \\
622: \texttt{mul\_mars} & a b - c d & a (b - d) + (a - c) d & a \neq c \land b \neq d \\
623: \texttt{mul\_mals} & a b - c d & (a - c) b + c (b - d) & a \neq c \land b \neq d \\
624: \texttt{mul\_mabs} & a b - c d & a (b - d) + (a - c) b + -((a - c) (b - d)) & a \neq c \land b \neq d \\
625: \texttt{mul\_mibs} & a b - c d & c (b - d) + (a - c) d + (a - c) (b - d) & a \neq c \land b \neq d \\
626: \texttt{mul\_filq} & (a b - a c) / (a c) & (b - c) / c & ac \neq 0 \land b \neq c \\
627: \texttt{mul\_firq} & (a b - c b) / (c b) & (a - c) / c & bc \neq 0 \land a \neq c \\
628: \texttt{div\_mibq} & (a / b - c / d) / (c / d) & ((a - c) / c - (b - d) / d) / (1 + (b - d) / d) & bcd \neq 0 \land b \neq d \\
629: \texttt{div\_firq} & (a / b - c / b) / (c / b) & (a - c) / c & bc \neq 0 \land a \neq c \\
630: \texttt{sqrt\_mibs} & \sqrt{a} - \sqrt{b} & (a - b) / (\sqrt{a} + \sqrt{b}) & a \ge 0 \land b \ge 0 \land a \neq b \\
631: \texttt{sqrt\_mibq} & (\sqrt{a} - \sqrt{b}) / \sqrt{b} & \sqrt{1 + (a - b) / b} - 1 & a \ge 0 \land b > 0 \land a \neq b \\
632: \texttt{sub\_xals} & b - A & (b - a) + (a - A) & A \neq b \land a \neq b \\
633: \texttt{err\_fabq} & 1 + (a - b) / b & a / b & b \neq 0 \land a \neq b \\
634: \texttt{val\_xabs} & a & A + (a - A) & \\
635: \texttt{val\_xebs} & A & a + -(a - A) & \\
636: \texttt{val\_xabq} & a & A (1 + (a - A) / A) & a \neq 0 \\
637: \texttt{val\_xebq} & A & a / (1 + (a - A) / A) & ab \neq 0 \\
638: \texttt{square\_sqrt} & \sqrt{a} \times \sqrt{a} & a & a \ge 0 \\
639: \texttt{addf\_1} & a / (a + b) & 1 / (1 + b / a) & a(a + b) \neq 0 \land a \neq 1 \\
640: \texttt{addf\_2} & a / (a + b) & 1 - 1 / (1 + a / b) & b(a + b) \neq 0 \land a \neq 1 \\
641: \texttt{addf\_3} & a / (a - b) & 1 / (1 - b / a) & a(a - b) \neq 0 \land a \neq 1 \\
642: \texttt{addf\_4} & a / (a - b) & 1 + 1 / (a / b - 1) & b(a - b) \neq 0 \land a \neq 1 \\ \hline
643: \end{array}
644: $$
645: \end{table}
646:
647: Table~\ref{tab/rules} contains some of the rules Gappa
648: tries to apply automatically. There are two kinds of rewriting rules. Rules of
649: the first kind, for example {\tt add\_firs}, are meant to produce
650: simpler expressions. Rules of the second kind, for example {\tt
651: sub\_xals}, are used to reproduce common practices of computer
652: arithmetic by introducing intermediate terms in expressions. In order
653: for an expression to match an uppercase letter in such a rule, the expression
654: that matches the same letter in lowercase has to be tagged as an
655: approximation of the former.
656:
657: %
658: %
659:
660: The first rule, {\tt sub\_xals}, has been applied earlier by Gappa,
661: because Gappa automatically tags $\circ(x)$ as an approximation of
662: $x$, for any expression $x$, since $\circ$ is a rounding operator.
663: Gappa also creates such pairs for expressions that define absolute and
664: relative errors in some hypotheses of a sub-formula of the proposition
665: {\tt PROP}. For example, on the following input, Gappa proposes
666: accurate bounds, as it considers $x$ to be an approximation of $y$,
667: and $\lfloor x \rfloor$ of $x$.
668: \begin{lstlisting}
669: @floor = int<dn>;
670: { x - y in [-0.1,0.1] -> floor(x) - y in ? }
671: \end{lstlisting}
672:
673: Thanks to its built-in rewriting rules and its heuristics to detect
674: approximations, Gappa is able to automatically verify most properties on
675: numerical applications that use common practices. Gappa, however, is not
676: a complete decision procedure\footnote{While seemingly simple, the
677: formalism of Gappa is rich enough so that any first-order formula for
678: Peano arithmetic can be expressed. As a consequence, it is impossible to
679: design an algorithm that is able to automatically decide whether any
680: proposition is provable or not.} and it may fail to prove some
681: propositions. When that happens, users can give some hints to the tool.
682:
683: For example, in the above input, a user could add the hint \verb|x ~ y|
684: after the proposition, in order to indicate that $x$ is an approximation
685: of $y$. As Gappa was able to guess this property automatically, Gappa
686: will warn that the hint is useless: the user can remove it.
687:
688: Another kind of hint allows the users to directly add rewriting
689: rules. The hint \texttt{primary -> secondary} states that Gappa
690: can use an enclosure of {\tt secondary} expression whenever it needs
691: an enclosure of {\tt primary} expression. For example, the following
692: hint describes Newton's relation between the reciprocal $\frac{1}{y}$
693: and its approximation $x \cdot (2 - x \cdot y)$.
694: \begin{lstlisting}
695: x * (2 - x * y) - 1/y -> (x - 1/y) * (x - 1/y) * -y
696: \end{lstlisting}
697:
698: Such rules usually explicit
699: some techniques applied by designers that are not necessarily visible
700: in the source code. We cannot expect an automatic tool to re-discover
701: innovative techniques. Yet, we will incorporate in Gappa any technique
702: that we find to be commonly used. Any additional rewriting rule produces
703: an hypothesis in the generated Coq file that must be proved
704: independently, for example with the \texttt{ring} tactic of Coq.
705:
706: In order for the \texttt{primary -> secondary} rule to be valid, any
707: value of {\tt primary} must be contained in the computed enclosure of
708: {\tt secondary}. This property generally holds true if both
709: expressions are equal. As a consequence, Gappa tries to check if they
710: are equal and warns if they are not, in order to detect mistypings
711: early. Note that Gappa does not check if divisors are always different
712: from zero before applying user-defined rewriting rules. Yet, Gappa
713: detects divisors that are trivially equal to zero in expressions that
714: appear in rewriting rules. For example, \texttt{y -> y * (x - x) / (x
715: - x)} is most certainly an error.
716:
717: %
718: %
719: %
720: %
721: %
722: %
723: %
724: %
725:
726: %
727: %
728: %
729: %
730:
731: %
732: %
733: %
734: %
735: %
736:
737: %
738: %
739:
740: Due to built-in and user-defined rewriting rules, Gappa may hold more
741: than one expression for a quantity, and hence several bounds as
742: evaluations of equivalent expressions in interval arithmetic may yield
743: different results. The intersection of the intervals yielded by the
744: different expressions may be tighter than its previously known bounds.
745: Tightening bounds on one quantity may then lead to tighter bounds on
746: quantities based on it. Gappa explores the directed acyclic graph of
747: quantities breadth-first until its goal is achieved or all bounds of
748: the graph stopped evolving.
749:
750: %
751:
752: \subsection{Sub-paving the range of some quantities by bisection (second use of {\tt HINT})}
753: \label{sub/subp}
754:
755: The last kind of hint that can be used when Gappa is unable to prove
756: automatically a formula is to pave the range of some quantities and to
757: prove independent results on each tile. Rewriting expressions is
758: usually very efficient but it fails if different proof structures are
759: needed on various parts of the range, as in the following example. The
760: generic proof structure only works for $x \in [0,\frac{1}{2}]$. A
761: specific proof structure is needed in order to extend the result to $x
762: \in [\frac{1}{2},3]$. This proof relies on the fact that $\circ(y) -
763: y$ is always zero there. But Gappa will not notice this property
764: unless the last line is provided.
765: \begin{lstlisting}
766: @rnd = float< ieee_32, ne >;
767: x = rnd(x_);
768: y = x - 1;
769: z = x * (rnd(y) - y);
770: { x in [0,3] -> |z| <= 1b-26 }
771: |z| $ x;
772: \end{lstlisting} %
773: There are three constructions for bisection each involving a {\tt \$}
774: sign in the hints section:
775: \begin{itemize}
776: \item Evenly split the range into as many sub-intervals as asked.
777: E.g. \texttt{\$ x in 6} splits the range of $x$ in six sub-intervals.
778: If the number of intervals is omitted (e.g. \texttt{\$~x}) and no expression
779: is present on the left of {\tt \$}, the default is 4.
780: \item Split an interval on user-provided points. E.g. \texttt{\$ x in
781: (0.5,2)} splits the range $[0,3]$ of $x$ above in three
782: sub-intervals, the middle one being $[0.5,2]$.
783: \item The third kind of bisection tries to find by dichotomy a good
784: sub-paving such that one goal of the proposition holds. The
785: range of this goal has to be specified in the proposition, and the
786: concerned expression has to be indicated on the left of the {\tt \$}
787: symbol.
788: \end{itemize}
789:
790: More than one bisection hint can be used and hints of the third kind
791: can try to satisfy more than one goal at once. The two hints below
792: will be used sequentially one after the other. The first one splits
793: the range of $u$ until all the enclosures on $a$, $b$, and $c$ are
794: verified.
795: \begin{lstlisting}
796: a, b, c $ u;
797: d, e $ v;
798: \end{lstlisting}
799:
800: Users may build higher dimension sub-paving by using more than one term
801: on the right of the {\tt \$} symbol, reaching quickly combinatorial
802: explosions though. The following statement asks Gappa to find a set of
803: sub-ranges of $u$ and $w$ such that the goals on $a$ and $b$ are
804: satisfied when the range of $v$ is split into three sub-intervals.
805: \begin{lstlisting}
806: a, b $ u, v in 3, w
807: \end{lstlisting} %
808:
809: %
810: %
811:
812: \section{Handling automatic proof checkers}
813:
814: \subsection{Work on the logical proposition ({\tt PROP})}
815: \label{sub/work-on-prop}
816:
817: The proposition is first modified and loosely broken according to the
818: rules of sequent calculus as presented below for the proposition seen
819: in Section~\ref{sub/prop}.
820: \begin{lstlisting}
821: { x - 2 in [-2,0] /\ (x + 1 in [0,2] -> y in [3,4])
822: -> not x <= 1 \/ x + y in ? }
823: \end{lstlisting}
824: Each of the following new formulas is then verified by Gappa. If both
825: formulas hold true, the original proposition does too.
826: \begin{eqnarray*}
827: x \le 1 \land x - 2 \in [-2,0] &\Longrightarrow& x + 1 \in [0,2] \lor x + y \in \texttt{?}\\
828: x \le 1 \land x - 2 \in [-2,0] \land y \in [3,4] &\Longrightarrow& x + y \in \texttt{?}
829: \end{eqnarray*}
830:
831: Gappa performs this decomposition in order to obtain implication
832: formulas with conjunctions of enclosures on their left hand sides and
833: trees of conjunctions and disjunctions of enclosures on their right hand
834: sides. In particular, all the negation symbols and the inner
835: implications have been removed. For example, a set of implications of
836: the form $e_1 \in I_1 \land \cdots \land e_m \in I_m \Rightarrow f_1 \in
837: J_1 \lor \cdots \lor f_m \in J_m$ is suitable for a use by Gappa.
838: Unspecified ranges (interrogation marks) are allowed as long as they
839: appear only on the right hand sides of these decomposed formulas.
840:
841: %
842: %
843: %
844: %
845:
846: Inequalities may appear on both sides of the implications. Any
847: inequality on the left hand side will be used only if Gappa can compute
848: an enclosure of the expression by some other means. Any inequality on
849: the right hand side is copied to the hypotheses as permitted by
850: classical logic, provided that it is reverted first. For example,
851: proposition $x \in [2,3] \Rightarrow (y \in [4,5] \land z \ge 6)$ is
852: equivalent to proposition $(x \in [2,3] \land z \le 6) \Rightarrow (y
853: \in [4,5] \land z \ge 6)$, but the second one provides a bigger set of
854: usable enclosures on its left hand side.
855:
856: When the right hand side of the formula is a disjunction, Gappa searches
857: for a sub-term that holds under the hypotheses of the proposition. It
858: fails to prove valid disjunctions if it cannot find one sub-term that
859: always holds under the hypotheses.
860:
861: %
862: %
863:
864: %
865: %
866: %
867: %
868: %
869: %
870:
871: %
872: %
873: %
874: %
875: %
876: %
877: %
878: %
879:
880: %
881: %
882: %
883: %
884: %
885:
886: %
887:
888: %
889: %
890: %
891: %
892: %
893: %
894: %
895:
896: %
897: %
898: %
899: %
900: %
901: %
902: %
903:
904: %
905: %
906: %
907: %
908: %
909: %
910:
911: %
912:
913: %
914:
915: %
916: %
917:
918: %
919: %
920: %
921: %
922: %
923:
924: %
925: %
926: %
927: %
928:
929: %
930: %
931: %
932: %
933: %
934: %
935: %
936: %
937: %
938: %
939: %
940: %
941:
942: %
943: %
944: %
945: %
946: %
947: %
948: %
949: %
950: %
951: %
952: %
953: %
954:
955: %
956: %
957: %
958: %
959:
960: %
961:
962: %
963: %
964: %
965: %
966: %
967: %
968: %
969: %
970: %
971: %
972: %
973: %
974: %
975: %
976: %
977: %
978: %
979: %
980: %
981:
982: %
983:
984: %
985: %
986: %
987: %
988: %
989: %
990: %
991: %
992: %
993: %
994: %
995: %
996: %
997: %
998: %
999: %
1000: %
1001: %
1002: %
1003: %
1004: %
1005: %
1006: %
1007: %
1008: %
1009: %
1010: %
1011: %
1012: %
1013: %
1014: %
1015: %
1016: %
1017:
1018: %
1019: %
1020:
1021: %
1022: %
1023: %
1024: %
1025: %
1026: %
1027:
1028: %
1029: %
1030: %
1031: %
1032: %
1033: %
1034: %
1035:
1036: %
1037: %
1038: %
1039: %
1040: %
1041: %
1042: %
1043: %
1044: %
1045: %
1046: %
1047: %
1048: %
1049: %
1050: %
1051: %
1052:
1053: %
1054: %
1055: %
1056: %
1057:
1058: %
1059: %
1060: %
1061: %
1062:
1063: %
1064: %
1065: %
1066: %
1067: %
1068: %
1069: %
1070: %
1071: %
1072:
1073:
1074: %
1075: %
1076:
1077: %
1078: %
1079: %
1080: %
1081: %
1082:
1083: %
1084: %
1085:
1086: %
1087:
1088: %
1089: %
1090: %
1091:
1092: %
1093: %
1094: %
1095: %
1096: %
1097: %
1098: %
1099:
1100: %
1101: %
1102: %
1103: %
1104: %
1105:
1106: %
1107:
1108: %
1109: %
1110: %
1111: %
1112:
1113: %
1114: %
1115: %
1116: %
1117: %
1118: %
1119:
1120: %
1121: %
1122: %
1123: %
1124: %
1125:
1126: %
1127: %
1128: %
1129: %
1130: %
1131: %
1132:
1133: %
1134: %
1135: %
1136: %
1137: %
1138:
1139: %
1140: %
1141: %
1142: %
1143: %
1144: %
1145:
1146: %
1147: %
1148: %
1149: %
1150: %
1151: %
1152: %
1153: %
1154: %
1155: %
1156:
1157: %
1158: %
1159: %
1160: %
1161: %
1162:
1163: %
1164: %
1165: %
1166: %
1167: %
1168: %
1169:
1170: %
1171: %
1172: %
1173: %
1174: %
1175: %
1176: %
1177: %
1178: %
1179:
1180: %
1181: %
1182: %
1183: %
1184: %
1185: %
1186: %
1187:
1188: %
1189:
1190: %
1191: %
1192: %
1193: %
1194: %
1195: %
1196: %
1197:
1198: %
1199:
1200: \subsection{Structure of the generated proof}
1201:
1202: \begin{table}
1203: \caption{Theorems on interval arithmetic available from the Coq companion library to Gappa}
1204: \label{tab/lib}
1205: $$
1206: \begin{array}{| l | l | l |} \hline
1207: \text{Target} & \text{Hypotheses} & \text{Constraint} \\ \hline
1208: \mathtt{BND}(\circ(a) - a, I) & & I \supset \circe{0} \\
1209: \mathtt{BND}(\circ(a) - a, I) & \mathtt{BND}(a, J) & I \supset \circe{1}(J) \\
1210: \mathtt{BND}(\circ(a) - a, I) & \mathtt{BND}(\circ(a), J) & I \supset \circe{2}(J) \\
1211: \mathtt{BND}(\circ(a) - a, I) & \mathtt{ABS}(a, J) & I \supset \circe{3}(J) \\
1212: \mathtt{BND}(\circ(a) - a, I) & \mathtt{ABS}(\circ(a), J) & I \supset \circe{4}(J) \\
1213: \mathtt{BND}((\circ(a) - a)/a, I) & \mathtt{BND}(a, J) & I \supset \circe{5}(J) \\
1214: \mathtt{BND}((\circ(a) - a)/a, I) & \mathtt{BND}(\circ(a), J) & I \supset \circe{6}(J) \\
1215: \mathtt{BND}((\circ(a) - a)/a, I) & \mathtt{ABS}(a, J) & I \supset \circe{7}(J) \\
1216: \mathtt{BND}((\circ(a) - a)/a, I) & \mathtt{ABS}(\circ(a), J) & I \supset \circe{8}(J) \\
1217: \mathtt{BND}(\circ(a), I) & \mathtt{BND}(a, J) & I \supset \circ(J) \\
1218: \mathtt{BND}(\circ(a), I) & \mathtt{BND}(\circ(a), J) & I \supset J \cap \mathbb{F}_{\circ} \\
1219: \mathtt{BND}(-a, I) & \mathtt{BND}(a, J) & I \supset -J \\
1220: \mathtt{BND}(|a|, I) & \mathtt{BND}(a, J) & I \supset |J| \\
1221: \mathtt{BND}(\sqrt{a}, I) & \mathtt{BND}(a, J) & J \ge 0 \land I \supset \sqrt{J} \\
1222: \mathtt{BND}(a - a, I) & & 0 \in I \\
1223: \mathtt{BND}(a/a, I) & \mathtt{ABS}(a, J) & 1 \in I \land J > 0 \\
1224: \mathtt{BND}(a \times a, I) & \mathtt{BND}(a, J) & I \supset |J| \times |J|\\
1225: \mathtt{BND}(a + b, I) & \mathtt{BND}(a, J), \mathtt{BND}(b, K) & I \supset J + K \\
1226: \mathtt{BND}(a - b, I) & \mathtt{BND}(a, J), \mathtt{BND}(b, K) & I \supset J - K \\
1227: \mathtt{BND}(a \times b, I) & \mathtt{BND}(a, J), \mathtt{BND}(b, K) & I \supset J K \\
1228: \mathtt{BND}(a/b, I) & \mathtt{BND}(a, J), \mathtt{BND}(b, K) & 0 \not\in K \land I \supset J / K \\
1229: \mathtt{ABS}(-a, I) & \mathtt{ABS}(a, J) & I \supset J \\
1230: \mathtt{ABS}(|a|, I) & \mathtt{ABS}(a, J) & I \supset J \\
1231: \mathtt{ABS}(\sqrt{a}, I) & \mathtt{ABS}(a, J) & I \supset \sqrt{J} \\
1232: \mathtt{ABS}(a \pm b, I) & \mathtt{ABS}(a, J), \mathtt{ABS}(b, K) & I \supset |J - K| \cup (J + K) \\
1233: \mathtt{ABS}(a \times b, I) & \mathtt{ABS}(a, J), \mathtt{ABS}(b, K) & I \supset J \times K \\
1234: \mathtt{ABS}(a/b, I) & \mathtt{ABS}(a, J), \mathtt{ABS}(b, K) & K > 0 \land I \supset J / K \\
1235: \mathtt{BND}(a, I) & \mathtt{ABS}(a, J) & I \supset J \cup -J \\
1236: \mathtt{BND}(a, I) & \mathtt{BND}(a, J), \mathtt{ABS}(a, K) & I \supset (J \cap K) \cup (J \cap -K) \\
1237: \mathtt{BND}(|a|, I) & \mathtt{ABS}(a, J) & I \supset J \\
1238: \mathtt{ABS}(a, I) & \mathtt{BND}(|a|, J) & I \supset J \\
1239: \mathtt{BND}(a + b + a \times b, I) & \mathtt{BND}(a, J), \mathtt{BND}(b, K) & J \ge -1 \land K \ge -1 \land I \supset \mathcal{U}(J,K) \\
1240: \mathtt{BND}(\xi, I) & & I \supset \{\xi\} \\
1241: \mathtt{FIX}(a \pm b, e) & \mathtt{FIX}(a, f), \mathtt{FIX}(b, g) & e \le \min(f, g) \\
1242: \mathtt{FIX}(a \times b, e) & \mathtt{FIX}(a, f), \mathtt{FIX}(b, g) & e \le f + g \\
1243: \mathtt{FLT}(a \times b, p) & \mathtt{FLT}(a, q), \mathtt{FLT}(b, r) & p \ge q + r \\
1244: \mathtt{FIX}(a, e) & \mathtt{FLT}(a, q), \mathtt{ABS}(a, J) & J > 0 \land e \le 1 + \log_2(\underline{J}) - q \\
1245: \mathtt{FLT}(a, p) & \mathtt{FIX}(a, e), \mathtt{ABS}(a, J) & p \ge 1 + \log_2(\overline{J}) - e\\
1246: \mathtt{FIX}(a, e) & \mathtt{BND}(a, [x,x]) & \exists m \in \mathbb{Z}, x = m \cdot 2^e \\
1247: \mathtt{FLT}(a, p) & \mathtt{BND}(a, [x,x]) & \exists m,e \in \mathbb{Z}, x = m \cdot 2^e \land |m| < 2^p \\
1248: \mathtt{FIX}(\circ(a), e) & & e \le e_\circ \\
1249: \mathtt{FLT}(\circ(a), p) & & p \ge p_\circ \\
1250: %
1251: \mathtt{BND}(\circ(a) - a, I) & \mathtt{FIX}(a, e), \mathtt{FLT}(a, p) & 0 \in I \land e \ge e_\circ \land p \le p_\circ \\ \hline
1252: \end{array}
1253: $$
1254: \end{table}
1255:
1256: \begin{table}
1257: \caption{Interval operators used in Table~\ref{tab/lib}}
1258: \label{tab/int}
1259: $$
1260: \begin{array}{| l | l | l |} \hline
1261: \text{Operation} & \text{Constraint} & \text{Definition} \\ \hline
1262: & & \\[-8pt]
1263: -I & & [- \overline{I} , -\underline{J} ] \\
1264: I^{-1} & 0 \not\in I & [1/\overline{I}, 1/\underline{I}] \\
1265: I + J & & [\underline{I} + \underline{J}, \overline{I} + \overline{J} ] \\
1266: I - J & & I + (-J) \\
1267: I \times J & & [\min(\underline{I}\underline{J}, \underline{I}\overline{J}, \overline{I}\underline{J}, \overline{I}\overline{J}),
1268: \max(\underline{I}\underline{J}, \underline{I}\overline{J}, \overline{I}\underline{J}, \overline{I}\overline{J})] \\
1269: I / J & 0 \not\in J & I \times J^{-1} \\
1270: \sqrt{I} & I \ge 0 & [\sqrt{\overline{I}}, \sqrt{\underline{I}}] \\
1271: |I| & & I \mbox{ if } I \ge 0, \quad -I \mbox{ if } I \le 0, \quad [0, \max(-\underline{I}, \overline{I})] \mbox{ otherwise} \\
1272: \mathcal{U}(I, J) & & [\underline{I} + \underline{J} + \underline{I} \underline{J}, \overline{I} + \overline{J} + \overline{I} \overline{J}] \\
1273: \circ(I) & & \text{One operator is associated to each rounding mode of Table~\ref{tab/dir}} \\
1274: \circe{k}(I) & & \text{Several operators are associated to each rounding mode of Table~\ref{tab/dir}} \\ \hline
1275: \end{array}
1276: $$
1277: \end{table}
1278:
1279: Enclosure (\texttt{BND}) is the only predicate available to users but
1280: Gappa internally relies on more predicates to describe properties on
1281: an expression~$x$. Such predicates appear in intermediate lemmas
1282: of generated proofs.
1283: $$\begin{array}{lcl}
1284: \mathtt{BND}(x, I) & \equiv & x \in I \\
1285: \mathtt{ABS}(x, I) & \equiv & |x| \in I \land I \ge 0\\
1286: \mathtt{FIX}(x, e) & \equiv & \exists m \in \Z, x = m \cdot 2^e\\
1287: \mathtt{FLT}(x, p) & \equiv & \exists m, e \in \Z, x = m \cdot 2^e \land |m| < 2^p
1288: \end{array}
1289: $$
1290:
1291: The \texttt{FIX} and \texttt{FLT} predicates express that the set of
1292: computer numbers is generally a discrete subset of the real numbers,
1293: while intervals only consider connected subsets. They are especially
1294: useful for automatically detecting rounded operations that actually
1295: are exact operations, and hence do not contribute any rounding error.
1296:
1297: Table~\ref{tab/lib} lists most of the theorems used by Gappa. The
1298: verification process of these theorems relies on some interval
1299: operators defined in Table~\ref{tab/int}. In particular, several
1300: operators $\circe{k}$ related to rounding modes are needed. Some of
1301: these operators may be left undefined; in that case, Gappa will
1302: generate longer proofs in order to use other operators instead. Some
1303: theorems also need to know the structure of the numbers that can be
1304: represented with respect to a given rounding mode: $\mathbb{F}_\circ =
1305: \{ x \in \mathbb{R}\ |\ x = \circ(x) \} = \{ m \cdot 2^e\ |\ e \ge
1306: e_\circ \land |m| < 2^{p_\circ} \}$.
1307:
1308: The proof script generated for Coq contains the following kind of lemma
1309: whenever the certificate relies on interval addition to prove a
1310: proposition, e.g. ``if $x \in [1,2]$ (property \texttt{p1}) and $y
1311: \in [3,4]$ (property \texttt{p2}), then $x + y \in [0,6]$ (property
1312: \texttt{p3})''.
1313:
1314: \begin{lstlisting}[numbers=left]
1315: Lemma l1 : p1 -> p2 -> p3.
1316: intros h0 h1.
1317: apply add with (1 := h0) (2 := h1) ; finalize.
1318: Qed.
1319: \end{lstlisting}
1320:
1321: The first line defines the lemma: if the hypotheses \texttt{p1} and
1322: \texttt{p2} are verified, then the property \texttt{p3} is true too.
1323: The second line starts the proof in a suitable state by using the
1324: \texttt{intros} tactic of Coq. The third line applies the
1325: \texttt{add} theorem of Gappa support library with the \texttt{apply}
1326: tactic.
1327:
1328: The \texttt{add} theorem is as follows. \texttt{lower} and \texttt
1329: {upper} are functions that return the lower and the upper bound of an
1330: interval. Intervals are pairs of dyadic fractions (\texttt{FF} or $\IF$).
1331: \texttt{Fplus2} is the addition of dyadic fractions. \texttt{Fle2}
1332: compares two dyadic fractions (less or equal) and returns a boolean.
1333: The \texttt{BND} predicate holds, when its first argument, an
1334: expression on real numbers, is an element of its second argument, an
1335: interval defined by dyadic fraction bounds.
1336:
1337: \begin{lstlisting}
1338: Definition add_helper (xi yi zi : FF) :=
1339: Fle2 (lower zi) (Fplus2 (lower xi) (lower yi)) &&
1340: Fle2 (Fplus2 (upper xi) (upper yi)) (upper zi).
1341:
1342: Theorem add :
1343: forall x y : R, forall xi yi zi : FF,
1344: BND x xi -> BND y yi ->
1345: add_helper xi yi zi = true ->
1346: BND (x + y) zi.
1347: \end{lstlisting}
1348:
1349: The mathematical expression of the theorem is as follows:%
1350: $$\begin{array}{rl}
1351: \mathtt{add}:& \forall x,y \in \R, \quad \forall I_x,I_y,I_z \in \IF,\\
1352: &x \in I_x \Rightarrow y \in I_y \Rightarrow\\
1353: &f_{\mathtt{add}}(I_x,I_y,I_z) = \mathit{true} \Rightarrow\\
1354: &x + y \in I_z.\end{array}$$
1355:
1356: If we simply needed a theorem describing the addition in interval
1357: arithmetic, the $f_{\mathtt{add}}(I_x,I_y,I_z) = \mathit{true}$
1358: hypothesis would be replaced by $I_x + I_y \subseteq I_z$. But we also
1359: need for the theorem hypotheses to be automatically checkable. It is
1360: the case for the $x \in I_x$ and $y \in I_y$ hypotheses of the
1361: \texttt{add} theorem, since they can be directly matched to the
1362: hypotheses \texttt{h0} ($x \in [1,2]$) and \texttt{h1} ($y \in [3,4]$)
1363: of lemma \texttt{l1}.
1364:
1365: Hypothesis $I_x + I_y \subseteq I_z$, however, cannot be matched so
1366: easily. Consequently, it is replaced by an equivalent boolean
1367: expression that can be computed by a proof checker. In lemma
1368: \texttt{l1}, the computation is triggered by the \texttt{finalize}
1369: tactic that checks that the current goal can be reduced to $\mathit
1370: {true} = \mathit{true}$. This concludes the proof.
1371:
1372: All the theorems of Gappa companion library are built the same way:
1373: instead of having standard hypotheses that Coq would be unable to
1374: automatically decide, they use a computable boolean expression. The
1375: companion library formally proves that, when
1376: this expression evaluates to \emph{true}, the standard hypotheses hold
1377: true, and hence the goal of the theorem applies. This approach
1378: is a simpler form of reflection techniques~\cite{Bou97}. Although the
1379: use of booleans seems to restrict the use of Gappa to Coq proof
1380: checker, the interval arithmetic library~\cite{DauMelMun05} developed
1381: for PVS shows that proofs through interval computations are also
1382: attainable to other proof assistants.
1383:
1384: \subsection{Widening intervals to speedup proof certification}
1385:
1386: All the interval bounds are dyadic fractions ($m \cdot 2^n$ with $m$
1387: and $n$ relative integers) in order to ensure that the boolean
1388: expressions are computable. Dyadic fractions are easily and
1389: efficiently added, multiplied, and compared. Rational numbers could
1390: also have been used: they would have been almost as efficient and
1391: would have provided a division operator. But
1392: %
1393: %
1394: common floating-point properties involved in
1395: certifying numerical codes are better
1396: described and verified by using dyadic fractions.
1397:
1398: %
1399: %
1400: %
1401: %
1402: %
1403: %
1404: %
1405: %
1406: %
1407: %
1408: %
1409: %
1410: %
1411: %
1412: %
1413: %
1414: %
1415: %
1416: %
1417: %
1418: %
1419: %
1420: %
1421: %
1422: %
1423: %
1424: %
1425: %
1426: %
1427: %
1428: %
1429: %
1430: %
1431: %
1432: %
1433: %
1434: %
1435: %
1436: %
1437: %
1438: %
1439: %
1440:
1441: %
1442: %
1443: %
1444: %
1445: %
1446: %
1447: %
1448: %
1449: %
1450: %
1451: %
1452: %
1453: %
1454: %
1455: %
1456: %
1457: %
1458: %
1459: %
1460: %
1461: %
1462: %
1463: %
1464: %
1465: %
1466: %
1467: %
1468: %
1469: %
1470: %
1471: %
1472: %
1473: %
1474: %
1475: %
1476: %
1477: %
1478: %
1479: %
1480: %
1481: %
1482: %
1483: %
1484: %
1485: %
1486: %
1487: %
1488: %
1489: %
1490: %
1491: %
1492: %
1493: %
1494: %
1495: %
1496: %
1497: %
1498: %
1499: %
1500: %
1501: %
1502: %
1503: %
1504: %
1505: %
1506: %
1507: %
1508: %
1509: %
1510: %
1511: %
1512: %
1513: %
1514: %
1515: %
1516: %
1517: %
1518: %
1519: %
1520: %
1521: %
1522: %
1523:
1524: The proof checker does not need to compute any of these dyadic numbers,
1525: it just has to check that the interval bounds generated by Gappa make
1526: the boolean expressions evaluate to \emph{true}, and hence are valid.
1527: In particular, there is absolutely no need for Gappa to compute the
1528: sharpest enclosing interval of an expression: any wider interval can be
1529: used. As long as the boolean expressions evaluate to \emph{true}, the
1530: proof remains correct.
1531:
1532: For example, manipulating the expression $x / \sqrt{3}$ will sooner or
1533: later require $\sqrt{3} \ne 0$ to be proved. This is done by computing
1534: an enclosing interval of $\sqrt{3}$ and verifying that its lower bound
1535: is positive. Hence there is no need to compute an enclosing interval
1536: with thousands of bits of precision, the interval $[1,2]$ is accurate
1537: enough. Checking that $\sqrt{3} \in [1,2]$ holds true is fast, as it
1538: just requires checking $1^2 \le 3 \le 2^2$. In order to get simplified
1539: dyadic numbers in intermediate lemmas, Gappa first finds a correct proof
1540: path and then it greedily operates backwards from the last proved
1541: results to the first proved results, widening the intervals along the
1542: way.
1543:
1544: Such simplifications are important, since a proof checker like Coq is
1545: considerably slower than a specialized mathematical library. As a
1546: consequence, these simplified numbers can considerably speed up the
1547: verification process of propositions, especially when they involve error
1548: bounds. These considerations are also true for case studies: searching
1549: for a better sub-paving and certifying it, will always be faster than
1550: directly certifying the first sub-paving that has been found by Gappa.
1551: The time spent by Gappa in doing all the computations over and over in
1552: order to find a better sub-paving is negligible in comparison to the
1553: time necessary to certify the property on one single tile with a proof
1554: checker.
1555:
1556: \section{Perspectives and concluding remarks}
1557: \label{sec/conc}
1558:
1559: In our approach to program certification, generation of proof
1560: obligations, proof generation, and proof verification, are distinct
1561: steps. The intermediate step is performed by Gappa with its own
1562: computational methods, and the last one is done by a proof checker
1563: with the help of our support library.
1564:
1565:
1566: %
1567: %
1568: %
1569:
1570:
1571: %
1572: %
1573: %
1574: %
1575: %
1576:
1577: %
1578: %
1579: %
1580: %
1581: %
1582: %
1583:
1584: %
1585:
1586: The developments presented so far already allowed us to guarantee the
1587: correct behavior of many useful functions. As we continue using Gappa,
1588: we may discover practices that cannot be handled appropriately. We
1589: will extend Gappa, should this become necessary. Our software, a
1590: user's guide and details of some projects using Gappa are available on
1591: the Internet at the address below.
1592: \begin{center}
1593: \url{http://lipforge.ens-lyon.fr/www/gappa/}
1594: \end{center}
1595:
1596: Gappa is used to certify CRlibm, a library of elementary functions
1597: with correct rounding in the four IEEE-754 rounding modes and
1598: performances comparable to standard mathematical libraries
1599: \cite{DinLauMel06,DinDefLau04}. Figure~\ref{fig/tang} presents the
1600: input file needed to reproduce some parts of an earlier validation in
1601: HOL Light \cite{Har97a}. These expressions define an almost correctly
1602: rounded elementary function in single precision
1603: \cite{Tan89}. Gappa is also used to develop robust semi-static filters
1604: for the CGAL project \cite{MelPio07} and in the validation of delayed
1605: linear algebra over finite fields \cite{DauGio07}.
1606:
1607: \begin{figure}
1608: \hrule\vspace{12pt}
1609: \begin{verbatim}
1610: # 1. PROG: Definitions of aliases
1611: @rnd = float< ieee_32, ne >;
1612:
1613: # a few floating-point constants
1614: a1 = 8388676b-24;
1615: a2 = 11184876b-26;
1616: l2 = 12566158b-48;
1617: s1 = 8572288b-23;
1618: s2 = 13833605b-44;
1619:
1620: # the algorithm for computing the exponential
1621: r2 rnd= -n * l2;
1622: r rnd= r1 + r2;
1623: q rnd= r * r * (a1 + r * a2);
1624: p rnd= r1 + (r2 + q);
1625: s rnd= s1 + s2;
1626: e rnd= s1 + (s2 + s * p);
1627:
1628: # a few mathematical expressions to simplify later sections
1629: R = r1 + r2;
1630: S = s1 + s2;
1631:
1632: E = s1 + (s2 + S * (r1 + (r2 + R * R * (a1 + R * a2))));
1633: Er = S * (1 + R + a1 * R * R + a2 * R * R * R + 0);
1634: E0 = S0 * (1 + R0 + a1 * R0 * R0 + a2 * R0 * R0 * R0 + Z);
1635:
1636: # 2. PROP: Logical proposition Gappa has to verify
1637: { # provide the domains and accuracies of some variables
1638: Z in [-55b-39,55b-39] /\ S - S0 in [-1b-41,1b-41] /\
1639: R - R0 in [-1b-34,1b-34] /\ R in [0,0.0217] /\ n in [-10176,10176] ->
1640: # ask for the range of e and its absolute error
1641: e in ? /\ e - E0 in ? }
1642:
1643: # 3. HINTS: Hints provided by the user
1644: e - E0 -> (e - E) + (Er - E0); # true as E = Er
1645: r1 -> R - r2; # true as R = r1 + r2
1646: \end{verbatim}
1647: \hrule
1648: \caption{Gappa script for proving $e$
1649: accurately approximates $E_0 = \exp(R_0)$ in single-precision.}
1650: \label{fig/tang}
1651: \end{figure}
1652:
1653: The whole work of generating the proof is pushed toward the external
1654: program. All the intervals are precomputed and none of the complex
1655: tactics of Coq are used. The proof checker only has to be able to add,
1656: multiply, and compare integers; it does not have to be able to
1657: manipulate rational or real numbers. Consequently, one of our goal is
1658: to generate proofs not only for Coq, but for other proof checkers too.
1659:
1660: Branches and loops handling are outside the scope of this work. Both
1661: problems are not new to program verification and nice results have been
1662: published in both areas. We do not want to propose our solution for
1663: these problems. Our decision is to interact with the two following
1664: tools.
1665: \begin{itemize}
1666: \item Why \cite{Fil03} is a tool to certify programs written in a
1667: generic language (C and Java can be converted to this language). It
1668: certifies appropriate memory allocation and usage. It is able to
1669: handle hierarchically structured code with functions and assertions.
1670: Why also takes care of conditional branches. It duplicates the
1671: appropriate proof obligations and guarantees that both pieces of
1672: code meet their shared post-conditions. A floating-point formalism
1673: designed with Gappa in mind has recently been added to Why
1674: \cite{BolFil07}. Used together, Why and Gappa will be able to handle
1675: large pieces of software.
1676:
1677: %
1678: %
1679: %
1680: %
1681: %
1682: %
1683:
1684: \item Fluctuat \cite{PutGouMar04} handles loops by effectively
1685: computing loop invariants. Once these invariants are provided, Gappa
1686: can certify the correct behavior of any numerical code. Results of
1687: Fluctuat will be used as oracles and certified by Gappa. Should
1688: there be a significant bug in Fluctuat, Gappa will stop without
1689: being able to meet its goals as it cannot certify erroneous results.
1690: \end{itemize}
1691: %
1692: %
1693: %
1694: %
1695: %
1696: %
1697: %
1698: %
1699:
1700: %
1701:
1702: %
1703:
1704: %
1705: %
1706: %
1707: %
1708: %
1709: %
1710: %
1711: %
1712:
1713: %
1714: %
1715: %
1716: %
1717: %
1718: %
1719: %
1720: %
1721:
1722: %
1723: %
1724: %
1725: %
1726: %
1727: %
1728: %
1729: %
1730:
1731:
1732: %
1733: %
1734: %
1735: %
1736: %
1737: %
1738:
1739: %
1740: %
1741: %
1742: %
1743:
1744: %
1745: %
1746: %
1747: %
1748: %
1749:
1750: %
1751: %
1752: %
1753: %
1754: %
1755:
1756: %
1757: %
1758: %
1759: %
1760: %
1761: %
1762:
1763:
1764:
1765: %
1766: %
1767:
1768: %
1769: %
1770: %
1771:
1772: %
1773:
1774: %
1775:
1776: %
1777: %
1778: %
1779: %
1780: %
1781:
1782: %
1783: %
1784: %
1785: %
1786: %
1787: %
1788:
1789: %
1790: %
1791: %
1792:
1793: %
1794: %
1795: %
1796: %
1797: %
1798:
1799: %
1800: %
1801: %
1802: %
1803: %
1804: %
1805:
1806: %
1807: %
1808: %
1809: %
1810:
1811: %
1812: %
1813: %
1814: %
1815:
1816: %
1817: %
1818: %
1819:
1820: %
1821: %
1822:
1823:
1824:
1825: %
1826:
1827: %
1828: %
1829: %
1830: %
1831: %
1832:
1833: %
1834: %
1835: %
1836: %
1837:
1838: %
1839: %
1840: %
1841: %
1842:
1843: %
1844: %
1845: %
1846: %
1847: %
1848: %
1849: %
1850:
1851: %
1852: %
1853: %
1854:
1855: %
1856:
1857: %
1858:
1859: %
1860: %
1861: %
1862: %
1863:
1864: %
1865: %
1866:
1867: %
1868:
1869: %
1870: %
1871: %
1872:
1873: %
1874:
1875: %
1876:
1877: %
1878: %
1879: %
1880: %
1881:
1882: %
1883:
1884: %
1885: %
1886: %
1887:
1888: %
1889: %
1890: %
1891: %
1892: %
1893: %
1894: %
1895: %
1896: %
1897: %
1898: %
1899: %
1900: %
1901: %
1902: %
1903: %
1904:
1905: %
1906: %
1907: %
1908: %
1909: %
1910: %
1911:
1912: %
1913: %
1914: %
1915:
1916: %
1917: %
1918: %
1919:
1920: %
1921: %
1922: %
1923: %
1924: %
1925: %
1926:
1927: %
1928: %
1929: %
1930: %
1931: %
1932: %
1933: %
1934:
1935: %
1936: %
1937: %
1938: %
1939: %
1940:
1941: %
1942: %
1943: %
1944: %
1945:
1946: %
1947: %
1948: %
1949: %
1950: %
1951:
1952: %
1953: %
1954: %
1955: %
1956: %
1957:
1958: %
1959: %
1960: %
1961: %
1962: %
1963: %
1964: %
1965: %
1966: %
1967: %
1968: %
1969: %
1970: %
1971: %
1972: %
1973: %
1974: %
1975: %
1976: %
1977: %
1978: %
1979: %
1980: %
1981:
1982: %
1983: %
1984: %
1985: %
1986: %
1987:
1988: %
1989: %
1990: %
1991: %
1992: %
1993: %
1994: %
1995: %
1996:
1997:
1998:
1999: %
2000:
2001: %
2002: %
2003: %
2004: %
2005: %
2006:
2007: %
2008: %
2009: %
2010: %
2011: %
2012: %
2013: %
2014:
2015: %
2016: %
2017: %
2018:
2019: %
2020: %
2021: %
2022: %
2023:
2024: %
2025: %
2026: %
2027:
2028: %
2029:
2030: %
2031:
2032: %
2033: %
2034: %
2035: %
2036:
2037: %
2038: %
2039: %
2040: %
2041:
2042: %
2043:
2044: %
2045: %
2046: %
2047: %
2048: %
2049: %
2050:
2051: %
2052: %
2053: %
2054:
2055: %
2056: %
2057: %
2058: %
2059: %
2060: %
2061:
2062: %
2063: %
2064: %
2065: %
2066: %
2067: %
2068: %
2069: %
2070:
2071: %
2072: %
2073:
2074: %
2075: %
2076:
2077: %
2078: %
2079: %
2080: %
2081: %
2082: %
2083:
2084: %
2085: %
2086: %
2087:
2088: %
2089: %
2090: %
2091: %
2092: %
2093:
2094:
2095: %
2096:
2097: %
2098: %
2099: %
2100: %
2101: %
2102: %
2103: %
2104:
2105: %
2106:
2107:
2108: %
2109: %
2110:
2111: %
2112: %
2113: %
2114: %
2115: %
2116: %
2117:
2118: %
2119: %
2120: %
2121: %
2122:
2123:
2124: %
2125:
2126: %
2127: %
2128: %
2129: %
2130:
2131: %
2132: %
2133: %
2134: %
2135: %
2136: %
2137: %
2138: %
2139:
2140: %
2141:
2142: %
2143: %
2144: %
2145:
2146: %
2147:
2148: %
2149: %
2150: %
2151: %
2152: %
2153: %
2154: %
2155: %
2156:
2157: %
2158: %
2159: %
2160: %
2161: %
2162: %
2163: %
2164:
2165: %
2166: %
2167: %
2168: %
2169: %
2170: %
2171:
2172: %
2173: %
2174: %
2175: %
2176:
2177: %
2178:
2179:
2180:
2181: \bibliographystyle{acmtrans}
2182: \bibliography{alias,perso,groupe,saao,these,livre,arith}
2183:
2184: \end{document}
2185: