Home

User's Guide for Gappa

1. f x in 0 1 gt float lt ieee 32 ne gt x float lt i _ 32 ne gt 1 ze Gappa answers that the result is between 0 and 1 Without any help from the user they are the best bounds Gappa is able to prove Results tiloae lt 247 12 97 mes Gx tb Loat lt 24 14 9 a gt o aba O AL 16 59 5 1 A simple example to start from x 1 x 5 1 3 Defining notations Directly writing the completely expanded logical formula is fine for small formulas but it may become tedious once the problem gets big enough For this reason notations can be defined to avoid repeating the same terms over and over These notations are all written before the logical formula For example if we want not only the resulting range of the function but also the absolute error we need to write the expression twice So we give it the name y y float lt ieee_32 ne gt x x float lt i _32 ne gt 1 sa oz am 0 1 gt y an 2 Av ze er 12m 2 We can simplify the input a bit further by giving a name to the rounding operator too rnd float lt ieee_32 ne gt y moles Sirene GIA B oz ain 10 1 gt y a a y ze Gl se am 2 These explicit rounding operators right in the middle of the expressions make it difficult to directly express the initial C code So we factor the operators by putting them before the equal sign rnd float lt ieee_32 ne gt y mace x Cl za 10 11 gt y im Y Aw ze Cl im 2 Please note that this
2. whole engine removed dependencies between sequents parser removed automatic rounding of negated expressions equated numbers with exponent zero but different radices fixed grammar for multiple splits proof graph improved quality of fixed split e Version 0 7 2 2006 09 13 parser fixed incorrectly rounded intervals on input fact database restricted domain of some rewriting rules e Version 0 7 1 2006 08 13 fact database x added error propagation through opposite division and square root Coq back end x fixed confusion between nodes from different proof graphs Optimized away trivial goal nodes e Version 0 7 0 2006 07 07 Coq back end updated to support Gappa library version 0 1 Appendix D Changes 55 59 proof graph x added optimization pass for bound precision whole engine simplified back end handling Version 0 6 5 2006 06 12 Coq back end x fixed square root generation fact database disabled square root of negative numbers syntax x added fma a b c as a synonym for a b c arithmetic x added fma_rel main interface x added Ereverted fma option to change the meaning of fma a b c to c a b Version 0 6 4 2006 05 19 arithmetic x fixed influence zone again for floating point absolute error Version 0 6 3 2006 05 16 proof graph fixed failure when an inequality leads to a contradiction x added support for
3. ee ee ee ee ee ee ee 4 4 1 Functions With relative error oo nn 4 4 2 Rounding operators with homogen properties e UU wm WwW U vo Onn A WD NO iv Contents 5 Examples 15 5 1 A simple example to start from x F l X 00000 15 Sel The program cy 9378 3 eae Se be aves Ce See eee ee We SBR COL ae are 15 3 1 2 First Gappa Version wi e zu u aa ee A a ee a ee LL 15 3 1 3 Defining notations sorro e ec Re ARORA Sa 16 5 14 Complete version 2 5 3 2 22 44 was a Se De eee Bee eee 16 5 2 Tang s exponential function es aeea e a ee ee ee 18 2 Theralgorithin u sun aan AG ate God de GOERS Bee A 18 3 2 2 Gappadescription 2 es 3 eee ee er be 18 5 23 Pull listing a wa bs eae See HG whee Bae Se Oe wa Et Se bake CHES OS HES 19 5 3 Fixed point Newton division aoaaa 20 5 3 1 The algorithm and its verification 0 2 000 000 00000222 eee ee 20 5 3 2 Adding hints 3 3 ire 6448835 440 54800 845 bbe od ee ee u 20 E PUll Stin a ne 2 ae a AN 21 6 Using Gappa from other tools 23 6 1 Why and Gappa orina aa Se al a ee el Ew aS 23 6 1 1 Example floating point square root 23 6 1 2 Passing hints through annotations 6 24 6 1 3 Execution results s costos a 8 aan A a oe R A Rca a A E Gee 24 6 2 Coqand Gappa un ow eoe era e eee a ee ee B aG 25 7 Customizing Gappa 27 7 1 Defining a generator for a new formal system ooa of 7 2 Defining rounding op
4. 1 se a Gx p ere sepas escu ee u e 03 ES 8 Es te RR 0 5 Er Jt 8 iE 4 sg Esche ES gt 1 5 0 5 ern amp err em Ul isonet When writing these assertions for guiding Gappa one just as to make sure that they are easily provable their actual accuracy is not relevant For instance if the relative distance between u and 1 x had been 27 instead of 2710 Gappa would still have succeeded 6 1 3 Execution results Passing the program above to the Frama C Jessie tool produces the following console output frama c jessie a c kernel preprocessing with gcc C E I dD a c jessie Starting Jessie translation kernel No code for function sqrt_init default assigns generated jessie Producing Jessie files in subdir a jessie jessi File a jessie a jc written jessi File a jessie a cloc written jessie Calling Jessie tool in subdir a jessie Generating Why function sqrt jessie Calling VCs generator Chapter 6 Using Gappa from other tools 25 59 gwhy bin why a why CompugaetongorsVesten Computation of VCs done Reading GWhy configuration Loading gwhyrc config file GWhy configuration loaded Creating GWhy Tree view and displays the following user interface gWhy a verification conditions viewer file Configuration Proof Alt Ergo Gappa Sqrt_ensures_default_po_29 Proof obligations 0 8 0 12 0 Statistics x double V User goals O o i
5. 2008 06 24 proof graph avoided infinite dichotomy on some unprovable propositions back ends x fixed generation of subset facts fact database x reduced cycles in theorems main interface x added Mschemes option for generating dot scheme graphs allowed input filename on command line Version 0 9 0 2007 11 08 syntax x added constraints on user rewriting e g x gt 1 1 x x lt gt 0 whole engine x added detection of assumed facts in Munconstrained mode fact database x added relative error propagation through division back ends x fixed cache collisions between theorems proof graph 54 59 fixed intersection of relative errors enabled bound simplification through rewriting rules x fixed handling of half bounded goals e Version 0 8 0 2007 02 23 HOL Light back end x added new back end proof graph x added option Mexpensive to select best paths on length fact database added predicate REL x y 1 e replaced rewriting rules on relative error by computations on REL enhanced path finder to fill holes in theorems put back rewriting rules to theorem level fixed incorrect equality of variables added predicate NZR x lt gt 0 added propagation of FIX and FLT through rounding operators e Version 0 7 3 2006 11 17 fact database generalized rounding theorems to any combination of errors and predicates
6. cl gt 130 im 2 N 20 2 2 dl amp 120 1 ma E JU Chapter 5 Examples 21 59 Gappa now gives the answer below Notice that the range of the round off error almost matches the precision of the computa tions Results il 20 2 dl lt 20 sam load fl 6 10352505 2 14 Tesdesls7 32 O 000LES53S gt 2 A 20 Ze amp 20 1 aim Fiss 2 0078 2 1 00564 1sloscs 16 2 01369 BCL OOM III So Gappa computes correct bounds for the round off error but not for the algorithmic one We can help Gappa by providing an expression of the latter one So we add a rule describing the quadratic convergence of Newton s iteration 20 2 ol 2 20 R ce R amp 20 R e els rl x 2 dx rl R gt rl R x rl R x d H2 247 Gappa answers that r2 R4 Warning although present in a quotient th xpression d may have not been tested for non zeroness Results DA R aa Sea 156545 A SS IS 0 2 ERAS MISA SAV US HA A ASAS ANS LAT ZA 280 DIS jil While the answer is the expected one there is this warning message about d possibly being zero Indeed R is the reciprocal of d and we are using the fact that R d 1 So the rewriting rules cannot be proved on their own But they can be proved in the context of the problem so there is no correctness issue In order to eliminate this warning we can give the precise hypotheses such that the left hand sides of the rewriting rul
7. tie breaking toward zero na to nearest tie breaking away from zero nd to nearest tie breaking toward minus infinity nu to nearest tie breaking toward plus infinity The rounding directions mandated by the IEEE 754 standard are ne default mode rounding to nearest zr dn up and na introduced for decimal arithmetic 4 2 Floating point operators This class of operators covers all the formats whose number sets are F p d m x 2 m lt 2P e gt d In particular IEEE 754 floating point formats with subnormal numbers are part of this class if we set apart overflow issues Both parameters p and d select a particular format The last parameter selects the rounding direction float lt precision minimum exponent rounding_direction gt 14 59 4 3 Fixed point operators Having to remember the precision and minimum exponent parameters may be a bit tedious so an alternate syntax is provided instead of these two parameters a name can be given to the float class float lt name rounding_direction gt There are four predefined formats ieee_32 IEEE 754 single precision ieee_64 IEEE 754 double precision ieee_128 IEEE 754 quadruple precision x86_80 extended precision on x86 like processors 4 3 Fixed point operators This class of operators covers all the formats whose number sets are F e m x 2 The first parameter selects the weight of the least significant bit The second parameter selects the rou
8. Gappa description al 8388676b 24 a2 ELETI AS li 12566015004 Sil 2857122886281 s2 13833605b 44 122 tamos in ee 127 ie tamal Geil ap 122 Gi ince en r e lal a r aZ D enes il ar 2 sp ey s end sl s2 e mee sil t 8 T p R El eZ sl 62 ind SO Gl cr RO r al lt lt RO gt RO sp AZ se RO e RO ss RO ae A Pp Ta ain O SS AOS 2 S SO da AA mR 7 EO ain Mo sa omst 7 R a 10 0 0217 N in a F10176 10176 gt e sin 2 Ne WO shin 2 Please note the way Z is introduced Its definition is backward Z is a real number such that EO is the product of SO and the exponential of RO It makes for clearer definitions and it avoids having to deal with divisions Chapter 5 Examples 19 59 Results e aun 42622530722 1 02097 2 0 0299396 l S7OSilsso 23 il 04524 2 0 DEIS S 130 i mA 518049 62 02 732 59 O lt O2ZS346 2 Sa ALIS jp IAS LES S lt gt O W23346 2 SI ADS ji Gappa is able to bound both expressions While the bounds for e seem sensible the bounds for e E0 are grossly overesti mated This overestimation comes from the difference between the structures of e and EO To improve the bounds on the error e EO we split it into two parts a round off error and a term that combines both discretization and truncation errors The round off error is expressed by introducing a term E with the same structure as e but without any round
9. Qed The tactic handles goals and hypotheses that are either equalities of real numbers e e2 or pairs of inequalities on real numbers bi lt e lt bo or inequalities expressing relative errors e e2 lt b lez For inequalities the b bounds have to be explicit dyadic numbers The tactic also recognizes properties written as le lt b as syntactic sugar for 0 lt e lt b The tactic is built on Flocq s formalism and uses the same rounding operators and formats The previous goal could therefore have been written in a slightly more natural way Definition format generic_format radix2 FLT_exp 1074 53 Goal moral er Jo IR Corme Gl gt fornan o gt Sa 16 lt a lt 53 16 gt 22 ES b lt 30 16 gt orale a 19 e Brcooia acidos El lo kha Ho da do refine symeg _ rnd a b a b revert la Ib replace a with rnd a replace b with rnd b unfold rnd gappa Qed 6http flocq gforge inria fr Chapter 7 Customizing Gappa These sections explain how rounding operators and back ends are defined in the tool They are meant for developers rather than users of Gappa and involve manipulating C classes defined in the src arithmetic and src backends directories 7 1 Defining a generator for a new formal system To be written 7 2 Defining rounding operators for a new arithmetic 7 2 1 Function classes A function derives from the function_class class Th
10. Washington DC USA 2010 13 Ali Avad and Claude March Multi prover verification of floating point programs Proceedings of the 5th International Joint Conference on Automated Reasoning 127 141 Edinburgh Scotland 2010 14 Claude Pierre Jeannerod Herv Knochel Christophe Monat and Guillaume Revy Computing floating point square roots via bivariate polynomial evaluation IEEE Transactions on Computers 60 2 214 227 2011 15 Florent de Dinechin Christoph Lauter and Guillaume Melquiond Certifying the floating point implementation of an elementary function using Gappa IEEE Transactions on Computers 60 2 242 253 2011 16 Christophe Mouilleron and Guillaume Revy Automatic generation of fast and certified code for polynomial evaluation Proceedings of the 20th Symposium on Computer Arithmetic 233 242 Tiibingen Germany 2011 17 Claude Pierre Jeannerod and Jingyan Jourdan Lu Simultaneous floating point sine and cosine for VLIW integer proces sors Proceedings of the 23rd International Conference on Application Specific Systems Architectures and Processors 69 76 Delft The Netherlands 2012 18 Olga Kupriianova and Christoph Lauter Metalibm A Mathematical Functions Code Generator Proceedings of the 4th International Congress on Mathematical Software 713 717 Seoul Korea 2014 http dx doi org 10 1109 ARITH 2009 19 http dx dei org 10 1145 1772934 1772987 http dx doi org 10 1145 18385
11. all the facts that are left unproven In the following example the property NZR indicates that Gappa possibly needs to prove that some values are not zero te am Pipal gt ear 2 7 Ge a 2 tia ed 7 1 ine Results Ge 45 ab 7 Ge 4 al ae fal E Ge i f 1 am fil i Warning some properties were assumed NZR x 1 NAR Seh Notice that Gappa has assumed x 1 to be nonzero while it actually can be deduced from x in 1 2 So there might be false positives among assumptions depending on the order Gappa deduced properties This mode cannot be used when a proof back end is selected as a generated proof would contain holes It is however as slow as if a back end had been selected since the whole proof graph is kept around 2 2 3 2 Gathering statistics Option Mstatistics At the end of its computations Gappa displays some statistics For example the second script of Section 5 3 gives Stobiistiest 2359 expressions were considered but then 127 of those got discarded 6317 theorems were considered but then 326 of those got discarded 7437 applications were tried Among those 5933 were successful vet 2626 proved useless and 13 improved existing results The first two lines show how manv intermediate expressions Gappa has prepared The first number tells how manv have been considered and the second number tells how manv of them were discarded because no theorem could handle them Similarly the ne
12. fixed confusing message in case of failure e Version 1 1 1 2014 03 25 arithmetic fixed incorrect error computation for some uncommon bound values back ends x fixed crash on useless leaves with undefined properties e Version 1 1 0 2013 12 20 proof graph x added detection and avoidance of slow convergence main interface x added option Echange threshold to control detection of slow convergence e Version 1 0 0 2013 07 14 syntax recognized e lt gt 0 for inputting NZR properties 50 59 fact database x added some new theorems for NZR back ends x added a back end producing LaTeX files disabled HOL Light back end as it was not used enabled automatic dichotomy and formula reduction proof graph allowed arbitrary formulas as output of nodes main interface removed option Msequent as formulas are handled as a whole now e Version 0 18 0 2013 06 25 main interface removed option Mexpensive x added more details to Mstatistics proof graph improved performances x improved proof simplification Coq back end x fixed incorrect theorem name for square root e Version 0 17 1 2013 04 01 build system x fixed issues with MacOSX BSD and compilation flags e Version 0 17 0 2013 03 20 build system switched to remake fact database x added theorems relating the ranges of two expressions given the relative error between them x simp
13. for a bisection with respect to the expression rnd x_ There are three types of bisection The first one splits an interval in as many equally wide sub intervals as asked by the user The second one splits an interval along the points provided by the user 12 59 3 3 Providing hints So aint OF split the range of x in six sub intervals x in 0 5 1 9999999 split the range of x in three sub intervals the middle one being 0 5 2 BER equivalent to x in 4 The third kind of bisection tries to find by dichotomy the best range split such that a goal of the logical formula holds true This requires the range of this goal to be specified and the enclosed expression has to be indicated on the left of the symbol fos s a 10 81 gt el lt llo 26 I al amp se Contrarily to the first two kinds of bisection this third one keeps the range improvements only if the goal was finally reached If there was a failure in doing so all the improvements are discarded Gappa will display the sub range on which the goal was not proved There is a failure when Gappa cannot prove the goal on a range and this range cannot be split into two half ranges either because its internal precision is not enough anymore or because the maximum depth of dichotomy has been reached This depth can be set with the Edichotomy 999 option More than one bisection hint can be used And hints of the third kind can try to satisfy more than one goal a
14. graph fixed sequents with empty goals not being recognized as proved main interface added option Msequent to display goals as Gappa scripts added option Monly failure to limit output to failing goals improved display of extremely small big bounds improved display of rounding operators proof paths fixed inequalities lower bound on absolute values being ignored arithmetic improved relative operators handling when exponents are not constrained e Version 0 12 0 2009 05 26 back ends added back end for producing Coq lambda terms proof graph x fixed handling of complicated goals main interface x added output of failed subgoals Appendix D Changes 53 59 Version 0 11 3 2009 04 29 Coq back end applied correct theorems for intervals with infinite bounds Version 0 11 2 2009 04 14 parser x fixed handling of CRLF end of line Version 0 11 1 2009 04 14 main interface removed error code on options help and version Version 0 11 0 2009 02 16 proof graph avoided splitting provably singleton intervals x added score system for favoring successful schemes arithmetic tightened rounding error when applied to short values syntax x recognized lhs of user rewriting as potential user approximate x added x y in and Ix yl lt for REL properties build system x fixed compilation on Cygwin Version 0 10 0
15. gt E Er E0 Gappa answers that the error is bounded by 0 535 ulp This is consistent with the bounds computed by Tang and Harrison 20 59 5 3 Fixed point Newton division Results e im PHIZ295o 23 11 0219 2 0 0sl2Za3s AO 22 il A 2 0 06255 75 1 e E0 in 75807082762648785b 80 6 27061e 08 2 23 9268 154166255364809243b 81 lt gt GS SVIGLIE O8 2 223 9027 HI 5 3 Fixed point Newton division 5 3 1 The algorithm and its verification Let us suppose we want to invert a floating point number on a processor without a floating point unit The 24 bit mantissa has to be inverted from a value between 0 5 and 1 to a value between 1 and 2 For the sake of this example the transformation is performed by Newton s iteration with fixed point arithmetic The mantissa is noted d and its exact reciprocal is R Newton s iteration is started with a first approximation rO taken from a table containing reciprocals at precision 278 Two iterations are then performed The result r1 of the first iteration is computed on 16 bit words in order to speed up computations The result r2 of the second iteration is computed on full 32 bit words We want to prove that this second result is close enough to the infinitely precise reciprocal R 1 d First we define R as the reciprocal and d and rO as two fixed point numbers that are integer multiples of 27 and 278 respectively Moreover r 0 is an appr
16. intersecting ABS predicates hint parser added detection of useless hints parser normalized numbers with fractional part ending by zero Version 0 6 2 2006 05 04 fact database fixed dependencies of rewriting rules relying on non zero values a race could lead to failed theorems x added formulas to compute the relative error of a sum arithmetic x added new directed rounding to odd away from zero x added new rounding to nearest with tie breaking to odd to zero away from zero up down x fixed influence zone for floating point absolute error Version 0 6 1 2006 04 26 proof paths improved detection of dead paths fact database x fixed patterns for generalized rounding operators improved rewriting rules for approx accurate pairs renamed rewriting rules 56 59 e Version 0 6 0 2006 03 09 syntax added ways of specifying how interval splitting is done added detection of badly formed intervals in propositions removed limitation on multiple hypotheses about the same expression improved heuristic for detecting approx accurate pairs removed limitation on number of accurate expressions for a given approximate removed hack for accurate expressions of rounded expressions potentially disruptive whole engine x added inequalities as hypotheses they cannot imply theorems but they can restrict computed ranges proof paths x put rewriti
17. note that this rewriting only applies when Gappa tries to bound the expression not when it tries to bound a bigger expression The two other hints indicate that Gappa should bound the left hand side values by doing a case split on the right hand side It only works if the logical proposition requires explicit bounds for the expression on the left hand side 5 1 4 4 Full listing As a conclusion here is the full listing of this example some notations rnd float lt ieee_32 ne gt x rnd xx x is a floating point number y ice 38 Cl f equivalent to y rnd x rnd 1 x m ee le she the value we want to approximate the logical property x in 0 1 gt y in 0 0 25 y z in 3b 27 3b 27 hints gt 0 25 x 0 5 amp z O 5 5 Fes l x Ta x A222 Y 3 bound y by splitting the interval on x Y 2 sp bound y z by splitting Gappa gives the results below Since it proved the whole formula and there was no unspecified range it does not have much to say Warning z and 25e 2 x 5e 1 Difference 25e 2 2 x 5e 1 are not trivially equal x 5e 1 5e 1 92 x 18 59 5 2 Tang s exponential function Note that Gappa checks the rewriting rules in order to provide early detection of mistyping Since this check does not involve computations on decimal numbers Gappa warns about the user hint on z This false positive can be avoided by adding the spec
18. splitting on empty goals x added more general schemes for case splitting hint parser x shut up warning messages about trivial integers as denominator Version 0 5 3 2005 11 18 proof graph fixed goal removal undefined goals require optimal solutions Version 0 5 2 2005 11 17 proof graph simplified node memory handling simplified graph handling put dichotomy at a higher level outside of proof schemes x replaced hypothesis property vectors by bit vectors stored in place if possible syntax added detection of unbound identifiers whole engine x added support for complex logical properties Version 0 5 1 2005 10 26 whole engine x added FIX and FLT predicates in addition to the original BND predicate Version 0 5 0 2005 10 14 whole engine generalized rounding modes as functions generalized functions with rounding theorems removed default rounding theorems syntax split variables and functions simplified rounding and function syntax purely C template like syntax added NOT and OR logical operators arithmetic x replaced relative rounding by functions x factored number rounding handling x added fixed point arithmetic generalized floating point rounding modes to any triplet precision subnormal smallest exponent direction proof graph x reduced the number of node types by demoting theorem and axiom nodes to internal facts Version 0 4 12 2005 09 14 sy
19. sufficient for most uses too 2 2 2 3 Fused multiply add format Option E no reverted fma By default Eno reverted fma the expression fma a b c is interpreted as a x b c As this may not be the preferred order for the operands the option makes Gappa usec a x b instead 2 2 2 4 Threshold for accepting new results Option Echange thresholdsfloat When Gappa discovers a new result 1t compares it to the ones previously found If the changes are smaller than the threshold the new result is discarded The threshold is a floating point value between 0 and 1 Setting it to O prevents Gappa from ever discarding a better result By default its value is 0 01 that is interval bounds or widths have to improve by at least one percent Chapter 2 Invoking Gappa 5 59 2 2 3 Setting modes These options cannot be embedded into scripts 2 2 3 1 Assuming vague hypotheses Option Munconst rained By default Gappa checks that all the hypotheses hold before applying a theorem This mode weakens the engine by making it skip hypotheses that are not needed for computing intermediate results For example Gappa will no longer check that x is not zero before applying the lemma proving x x in 1 1 This mode is especially useful when starting a proof on relative errors as it makes it possible to get some early results about them without having to prove that they are well defined At the end of its run Gappa displays
20. that the default rounding mode is used rounding to nearest number break to even on tie The function returns the value x 0 1 Gx instead of the ideal value x 1 x due to the limited precision of the computations If we rule out the overflow possibility floating point numbers are limited not only in precision but also in range the returned value is also o x o 1 x This o function is a unary operator related to the floating point format and the rounding mode used for the computations This is the form Gappa works on 5 1 2 First Gappa version We first try to bound the result of the function Knowing that x is in the interval 0 1 what is the enclosing interval of the function result It can be expressed as an implication If x is in 0 1 then the result is in something Since we do not want to enforce some specific bounds yet we use a question mark instead of some explicit bounds The logical formula Gappa has to verify is enclosed between braces The rounding operator is a unary function float lt ieee 32 ne gt The result of this function is a real number that would fit in a IEEE 754 single precision ieee 32 floating point number float if there was no overflow This number is potentially a subnormal number and it was obtained by rounding the argument of the rounding operator toward nearest even ne The following Gappa script finds an interval such that the logical formula describing our previous function is true
21. y in 0x1p 53 0x1p 531 This enclosure on the relative error represents the following proposition Je 27 2 x y x 1 8 As with enclosures the range can be left unspecified sel x am 2 Results 2 f x am 0 When the bounds on a relative error are symmetric the enclosure can be written as x y lt instead 3 1 1 3 Equalities While equalities could be encoded with enclosures I cas gt y aia 0 0 Gappa also understands the following notation Cea Se DAL DI Se a i Note that equalities are implicitly directed from left to right For instance when looking for a property ona x Gappa will considera y assuming that property x y holds but not the other way around This is similar to the handling of rewriting tules Whenever possible equalities should be expressed as definitions rather than inside the logical formulas as it offers more opportunities for Gappa to apply its theorems Chapter 3 Formalizing a problem 9 59 3 1 1 4 Expression precision In addition to equalities and inequalities Gappa also supports properties about the precision needed to represent expressions These are expressed by using the predicates F 1X x k and FLT x k where x is an expression and k an integer Both properties state that x can be decomposed as a generic binary floating point number 3m e Z x m 2 For FIX this decomposition satisfies e gt k while for F LT it satisfies m lt
22. zr aw od ne nz na no REL rnd a a REL rnd a a BND a REL rnd a a ABS a float REL rnd a a BND rnd a REL rnd a a ABS rnd a float C 2 3 Rewriting rules The following theorems are used to propagate properties about a term to some provably equal term Theorem name Goal Hypotheses bnd_rewrite BND a EQL a b BND b abs_rewrite ABS a EQL a b ABS b fix_rewrite FIX a EQL a b FIX b flt_rewrite FLT a EQL a b FLT b nzr_rewrite NZR a EOL a b NZR b rel_rewrite_1 REL a c EQL a b REL b c rel rewrite 2 REL c a EQL a b REL c b For the sake of readability the following theorems are not written with BND predicates but rather with expressions only When trying to obtain some enclosure of the target expression goal Gappa will first consider the source one hypothesis As a consequence of this layout and contrarily to previous tables constraints will also list additional hypotheses needed to apply the rules Whenever an operator is put between square brackets it means that only theorems that perform basic interval arithmetic will be able to match it A constraint written using USR means that the theorem will be applied only if a matching expression appears in the input file Theorem name Target Source opp_mibs a b a b add_xals b
23. 15 1 2011 09 14 fact database x fixed broken simplification of a b c b Version 0 15 0 2011 05 31 fact database x added EQL predicate el e2 x changed user rewriting to use the EQL predicate improved rewriting rules to handle ABS FIX FLT NZR REL in addition to BND predicate syntax x added FLT e k and FIX e k for inputting FLT and FIX properties x added el e2 for inputting EQL properties allowed arbitrary logical propositions as termination condition for bisection Version 0 14 1 2011 04 07 build system x fixed some platform specific issues Version 0 14 0 2010 10 18 52 59 Coq back end added support for Coq support library 0 14 e Version 0 13 0 2010 04 20 Coq lambda back end x simplified generated proofs proof graph x disabled sequent generation x disabled proof tracking for the null back end improved handling of deep logic negations x handled disjunctions by dichotomies null back end only main interface removed option Monly failure since there is only one proposition documentation switched from jade to dblatex e Version 0 12 3 2009 11 06 Coq lambda back end x fixed incorrect invocation of some theorems arithmetic x fixed incorrect proofs for floating point error near powers of two e Version 0 12 2 2009 10 20 back ends x fixed output of underspecified REL goals e Version 0 12 1 2009 09 22 proof
24. 2 For instance the following Gappa formula holds x float lt ieee_32 ne gt x_ EIX x 149 FLT x 24 3 1 1 5 Nonzero expressions Finally Gappa has special support for expressions that are not zero and thus can be properly handled when they appear as denominators xD x an ili 3 1 2 Definitions Typing the whole expressions in the logical formula can soon become annoying and error prone especially if they contain rounding operators To ease this work the user can define in another section beforehand the expressions that will be used more than once A special syntax also allows to avoid embedding rounding operators everywhere First rounding operators can be given a shorter name by using the name definition lt parameters gt syntax name can then be used wherever the whole definition would have been used Next common sub terms of a mathematical expression can be shared by giving them a name with the name term syntax This name can then be used in later definitions or in the logical formula or in the hints The equality itself does not hold any semantic meaning Gappa will only use the name as a shorter expression when displaying the sub term and in the generated proof instead of a randomly generated name Finally when all the arithmetic operations on the right side of a definition are followed by the same rounding operator this operator can be put once and for all on the left of the equal symbol For examp
25. 99 1838622 http shemesh larc nasa gov NFM2010 papers nfm2010 14 23 pdf http dx doi org 007 978 3 642 14203 1 11 http dx doi org 09 TC 20102152 http dx doi org 09 TC 2010 128 Attpe dx doi org 09 ARITH 2011 39 http dx doi org 09 ASAP 2012 12 http dx doi org 10 1007 978 3 662 44199 2_106 JD u eU Ne OW oooo0o0o0 Appendix A Gappa language A 1 Comments and embedded options Comments begin with a sharp sign and go till the end of the line Comments beginning by are handled as embedded command line options All these comments are no different from a space character Space tabulation and line break characters are not significant they at most act as identifier separators In the definition part of a script the GE is never matched so no separator is needed between operators gt and A 2 Tokens and operator priority There are five composite operators AND and OR and gt IMPL and lt LE and gt GE And three keywords in IN and not NOT and sqrt SORT Numbers are either written with a binary representation or with a decimal representation In both representations the inte ger parts are radix 10 natural numbers binary integer bB integer decimal integer integer integer eE integer hexadecimal Ox hexa 1 hexa hexa pP integer number binary decimal hex
26. D a BND a sqrt BND sqrt a BND a sub_refl BND a a div_refl BND a a NZR a square BND a a ABS a neg_a ABS a ABS a abs_a ABS al ABS a add BND a b BND a BND b sub BND a b BND a BND b c mul_ nop nop BND a x b BND a BND b div_ nop np BND a b BND a BND b add_aa_ nop ABS a b ABS a ABS b sub_aa_ nop ABS a b ABS a ABS b mul_aa ABS a x b ABS a ABS b div_aa ABS a b ABS a ABS b bnd_of_abs BND a ABS a abs_of_bnd_ nop ABS a BND a bnd_of_bnd_abs_ np BND a BND a ABS a c uabs of abs BND lal ABS a abs_of_uabs ABS a BND lal Z constant 1 2 10 BND a e abs fix FIX lal FIX a Z abs_flt FLT lal FLT a c neg fix FIX a FIX a neg_flt FLT a FLT a c add fix FIX a b FIX a FIX b c sub fix FIX a b FIX a FIX b c sub flt FLT a b FLT a FLT b REL a b c sub flt rev FLT b a FLT a FLT b REL a b c mul fix FIX a x b FIX a FIX b c mul flt FLT a x b FLT a FLT b c fix of filt bnd FIX a FLT a ABS a E fit of fix bnd FLT a FIX a ABS a c fix of singleton bnd FIX a ABS a flt_of_singleton_bnd FLT a ABS a bnd_of_nzr_rel BND b a a NZR a REL b a rel_of_nzr_bnd REL a b NZR b BND a b b E add_rr REL a b c d REL a c REL b d BND c c d NZR c d sub_rr REL a b c d REL a c REL b d BND c c d NZR c d mul_rr REL a x b c x d REL a c RE
27. E NUMBER ili REAL RDIV REAL IN 12 REAL REAL 13 PROP AND PROP 14 PROP OR PROP 15 PROP IMPL PROP 16 NOT PROP 17 7 PROP 18 SNUMBER NUMBER 19 NUMBI 20 7 NUMBI ps rs al rs ps 21 INTEGER NUMBER 22 SINTEGER SNUMBER 23 FUNCTION_PARAM SINTEGER 24 IDENT 25 FUNCTION_PARAMS_AUX FUNCTION_PARAM 26 FUNCTION PARAMS AUX FUNCTION PARAM 27 FUNCTION PARAMS x emptv x 28 lt FUNCTION PARAMS AUX gt 29 FUNCTION FUNID FUNCTION PARAMS 30 EQUAL 31 FUNCTION 32 PROG x empty x 35 PROG IDENT EQUAL REAL 34 BROCHA IDEN UN ERTEONEEZ EZ 35 PROG VARID 36 PROG FUNID Syn PROG VARID 38 PROG FUNID 39 REAL SNUMBER 40 VARID 41 IDE 42 FUNCTION REALS 43 REAL 4 REAL 44 REAL REAL Appendix A Gappa language 35 59 45 46 47 48 49 50 Syl 52 53 54 55 56 Si 58 59 60 61 62 63 64 65 66 67 68 69 70 AL u 13 74 75 76 REAL x REAL REAL REAL zz Bam 1 jU Sora 2 2 ia DU EMA i GREAT IA READ A REAT O REAREN REAL REAL REALS REA PARAS 7 77 RURAL DPOINT
28. E R 39 B 3 1 Error no contradiction was found 39 B 3 2 Error some enclosures were not satisfied nn 39 B 4 Warning messages during parsing 2 39 B 4 1 Warning renaming identifier foo as bar 0 0000 39 B 4 2 Warning although present in a quotient the expression foo may not have been tested for non zeroness 39 B 4 3 Warning foo and bar are not trivially equal oo oo onen 40 B 4 4 Warning bar is a variable without definition yetitisunbound 40 B 4 5 Warning no path was found for foo 2 2 2 Hmmm nn 40 B 5 Warning messages during proof computation oo 220m e 40 B 5 1 Warning when foo is in il bar cannot be proved e e 40 B 5 2 Warning case split on foo has not produced any interesting new result o 41 B 5 3 Warning case split on foo has no range to Split o o e e 41 B 5 4 Warning case split on foo is not goal driven anymore o e 41 C Theorems of Gappa 43 Cl Predicates dr eS ee ee Zoning ee e Gea eb eee ORS ew Se 43 C2 Theorems 44 0064 eked bee de je fea ER a oe wa aS Paw ee ae 43 C 2 1 Theorems about real arithmetic 0 0 00 00 002 eee eee ee ee 44 C 2 2 Theorems about rounding operators ooo 45 C 2 3 Rewriting MES o e soa i errada A Vs 45 D Changes 49 Chapter 1 Introduction Gappa G n ration Automatique de Preuves de Propri t s Arithm tiqu
29. H1 0 5 lt double_value x and double value x lt 2 0 Lemma quadratic_newton o 6 result double H7 abs_real double_value result 1 0 sqrt real double value x lt Function sqrt O 28 29 Ox1 p 6 abs_real 1 0 sqrt real double value x Default behavior 03 double 1 assertion H8 t_O result resulto int32 Ho integer_of_int32 resulto 0 i int32 H10 i resulto H108 integer_of_int32 i gt 2 H109 double_value x 1 0 sqrt_real double_value x sqrt_real double_value x 2 assertion 3 assertion 4 assertion 5 assertion 6 assertion resulti double H110 no_overflow_double nearest_even double_value x double_value t_0 and mul_double_post nearest_even x t_0 result1 _retres double Hill __retres resulti return double H112 return retres 7 assertion 8 assertion 9 assertion 10 assertion 11 assertion 12 assertion 13 loop invariant initially holds abs real double value return sqrt real double value x lt 0x1 p 43 abs real sqrt real double value x 14 loop invariant initiallv holds 15 assertion 16 assertion 17 assertion lemma quadratic newton forall real x t x gt 0 gt Al let err t 1 sqrt x 1 sqrt x 05 t 3 t t x 1 sqrt x 1 sqrt x 1 5 0 5 orr err err 18 loop invariant preserved 19 loop invariant preserved 20 assertion y 21 postcondition requires 0 5 l
30. L b d c div rr REL a b c d REL a c REL b d NZR d E compose REL b c REL b a REL a c compose REL c a REL c b REL b a k compose_swap REL c b d REL c d x a REL b 1 a NZR a E Appendix C Theorems of Gappa 45 59 Theorem name Goal Hypotheses error_of_rel_ nop nop BND b a REL b a BND a nzr_of_abs NZR a ABS a nzr_of_nzr_rel NZR b NZR a REL b a nzr of nzr rel rev NZR a NZR b REL b a bnd_div_of_rel_bnd_div BND b a c REL b a BND a c NZR c C 2 2 Theorems about rounding operators The following table describes the kind of theorems that can be applied to rounding operators These theorems have no specific names as each rounding operator comes with its dedicated set of theorems When a specific theorem is not available for a given rounding operator its effect can usually be obtained through an available one combined with a rewriting rule Goal Hypothesis Rounding kind BND rnd a BND a fixed float BND rnd a BND rnd a float BND rnd a a fixed BND rnd a a BND a fixed zr aw float up dn nu nd BND rnd a a ABS a float zr aw od ne nz na no BND rnd a a BND rnd a fixed zr aw float up dn nu nd BND rnd a a ABS rnd a float
31. S SNUMBER DPOINTS SNUMBER DVAR REAL REAL IN INTEGER REAL IN DPOINTS DVARS DVAR DAR SAD AE PRECOND REAL NE SINTEGER REAL LE SINTEGER REAL GE SINTEGER REAL lt SINTEGER REAL gt SINTEGER PRECONDS_AUX PRECOND PRECONDS AUX PRECOND PRECONDS x empty x EERE CONDS DAUKE K HINTS x empty x HINTS REAL IMPL REAL PRECONDS HINTS REALS DVARS PEINIESS PIRO PA AD ARS sate VEMOS 280 IDWARS 180 HINTS REAL s REAL A 4 Logical formulas These sections describe some properties of the logical fragment Gappa manipulates Notice that this fragment is sound as the generated formal proofs depend on the support libraries and these libraries are formally proved by relying only on the axioms of basic arithmetic on real numbers A 4 1 Undecidability First notice that the equality of two expressions is equivalent to checking that their difference is bounded by zero e f in 0 0 Second the property that a real number is a natural number can be expressed by the equality between its integer part int lt dn gt e and its absolute value fel Thanks to classical logic a first order formula can be written in prenex normal form Moreover by skolemizing the formula existential quantifiers can be removed although Gappa does not allow the user to type arbitrary functional operators in order to prevent mistyping existing operators the engine can handle th
32. The second one is the logical formula one wants to prove with the tool The third one gives some hints to Gappa on how to prove it The following script shows these three parts for the example of Section 5 1 some notations for making the script readable rnd float lt ieee_32 ne gt x rnd xx y ema x s IL x asx a gt the logical formula that Gappa will try and succeed to prove z ala 10 1 gt y ia 00 25 N y in 527 027 3 pS three hints to help Gappa finding the proof ze D25 Oe e e DJ y x Y 2 Ss 3 1 1 Logical formula This is the fundamental part of the script it contains the logical formula Gappa is expected to prove This formula is written between brackets and can contain any implication disjunction conjunction negation of properties of mathematical expressions These properties can be enclosures inequalities relative errors equalities and expression precisions Any identifier without definition is assumed to be universally quantified over the set of real numbers 3 1 1 1 Enclosures Enclosures are either bounded ranges or inequalities In positive position ranges can be left unspecified Gappa will then suggest a range such that the logical formula is verified I x 2 son 2 0 N Gea 1 ain 0 2 gt w aia SAS moe x lt 1 Y x ap ay ine Results xe ap W aa IS 2 8 59 3 1 Sections of a Gappa script Note that Gappa might be able to prove the formula without even ha
33. User s Guide for Gappa Guillaume Melquiond Contents 1 Introduction 2 Invoking Gappa 2 1 2 2 2 3 Input and output 2 2 bat oa Oe wa a See ES bald ea a Command line options ooo 2 2 1 Selecting a proof back end nn nn 2 2 2 Setting internal parameters ooo nn 2230 SEWNPMOdES sce od ahs n e e ERR ee Ses N ee GS A 2 2 4 Enabling and disabling warning messages a Embedded Options a 02 2 2 00 u na raj eee A SOE awe Re 3 Formalizing a problem 3 1 3 2 3 3 Sections of a Gappa script u ee bea en EE ee a 3 11 Lopi al formulas conos a5 Rae e ee PAE be eR Eb we ee we ee ee 3 1 2 Deiinitions sgn ade da HERR Ee os U 38 ed aa eS SR ne ae Ae adla Hints 2 2 sca NN Preferred expressions and other peculiarities 3 2 1 Absolute and relative errors 000000 3 2 2 Globa ler rs l 1323 ceee e moi ee ee ee Br ee ERR DEES SR A 3 2 3 Discrete values b 223 u tn jah aber a a RAG ES Rw oe ie S24 DISJUNCLON a rta de oa Pe ee A ae a A ER Providing hints v e 2 a a an Se Babee EB Ss a ae we Ee Bao Bedard ee 33 1 Rewntin rules 2 06446 2858466456 2588 Stubs ABD bBo b b Sw COREE eS 3 3 2 Approximated expressions 2 n nn 3 3 3 Dichotomy seatch 264505464644 505 a ee Oe eee bee ee ae gha 4 Supported arithmetic 4 1 42 43 4 4 Rounding directions s s cose a e moon Floating point operators Fixed poimt Operators oo kece a ER a a ORL ee A a s Miscellaneous operators
34. adecimal These three expressions represent the same number 57 5e 1 23b 2 0x5 Cp0 They do not have the same semantic for Gappa though and a different property will be proved in the decimal case Indeed some decimal numbers cannot be expressed as a dyadic number and Gappa will have to harden the proof and add a layer to take this into account In particular the user should refrain from being inventive with the constant 1 For example writing this constant as 00100 000e 2 may prevent some rewriting rules to be applied Identifiers IDENT are matched by alpha alpha digit _ The associativity and priority of the operators in logical formulas is as follows It is meant to match the usual conventions Sright IMPL Sleft OR Sleft AND Sleft NOT For the mathematical expressions the priority are as follows Note that NEG is the priority of the unary minus this is the operator with the highest precedence left 1 l olere taf oyi Sleft NEG 34 59 A 3 Grammar A 3 Grammar 0 Saccept BLOB Send 1 BLOB BLOB1 HINTS 2 BLOB1 PROG PROP 3 PROP REAL LE SNUMBER 4 FIX REAL SINTEGER 5 TE 2 IR NE CERO 6 REAL IN SNUMBER SNUMBER 7 REAL IN 9 8 REAL GE SNUMBER 9 REAL RDIV REAL IN SNUMBER SNUMBER j 10 REAL RDIV REAL L
35. arts by calling the sqrt_init function It returns an approximation of x 1 2 with a relative accuracy of 276 Only the specification of this auxiliary function is given Preconditions are introduced by the requires keyword while postconditions are introduced by ensures Its implementation could use small tables for instance Note that bounds on relative errors are expressed as approx exact lt error x exact in this setting The sqrt function then performs three Newton iterations in order to obtain an improved approximation of the reciprocal square root of x Since Gappa only handles straight line programs a pragma annotation instructs Frama C to completely unroll the loop before passing it to Jessie Finally once the reciprocal square root has been computed it is multiplied by x to obtain the square root 6 1 2 Passing hints through annotations The assert annotations cause Frama C Jessie to generate additional proof obligations These facts are then available to the following proof obligations as hypotheses In this example the actual content of the assertions does not matter from a certification point of view they are only used as a way to pass information to Gappa Indeed as explained in Section 5 3 Gappa needs to know about Newton s relation and which expressions are approximations of what So if the program were to be directly expressed in Gappa syntax the three loop assertions would instead have been written as follows eerie
36. ase the user can provide an intermediate expression with the following hint primary gt secondary If Gappa finds a property about the secondary expression it will use it as if it was about the primary expression This trans formation is valid as long as both expressions are equal So when generating a theorem proof Gappa adds this equality as a hypothesis It is then up to the user to prove it in order to be able to apply the theorem To detect mistyping early Gappa checks if both expressions can be normalized to the same one according to field rules and are therefore equal and warn if they are not It will not generate a proof of their equality though Note that Gappa does not check if the divisors that appear in the expressions are always nonzero it just warns about them If an equality requires some conditions to be verified they can be added to the rule sorde Ee SS 8 lt 7 3 3 2 Approximated expressions As mentioned before Gappa has an internal database of rewriting rules Some of these rules need to know about accurate and approximate terms Without this information they do not match any expression For example Gappa will replace the term B byb b B only it knows a term b that is an approximation of the term B Gappa has two heuristics to detect terms that are approximations of other terms First rounded values are approximations of their non rounded counterparts Second any absolute or relative error th
37. at appears as a hypothesis of a logical sub formula will define a pair of accurate and approximate terms Since these pairs create lots of already proved rewriting rules it is helpful for the user to define its own pairs This can be done with the following syntax approximate accurate In the following example the comments show two hints that could be added if they had not already been guessed by Gappa In particular the second one enables a rewriting rule that completes the proof floor int lt dn gt x wy aia 0 1 0 1 gt tloor s y ma 2 cp SES Esp ip ee oe AEP 3 3 3 Dichotomy search The last kind of hint can be used when Gappa is unable to prove a formula but would be able to prove it if the hypothesis ranges were not so wide Such a failure is usually caused by a bad correlation between the sub terms of the expressions This can be solved by rewriting the expressions But the failure can also happen when the proof of the formula is not the same everywhere on the domain as in the following example In both cases the user can ask Gappa to split the ranges into tighter ranges and see if it helps proving the formula rnd float lt ieee_32 ne gt x pnd x_ ya iy wa Se ee EA A fi oe aan 10 Si gt del ee With this script Gappa will answer that z lt 3 2 7 This is not the best answer because Gappa does not notice that rnd y y is always zero when 5 lt x lt 3 The user needs to ask
38. between 1 3 and 1 7 then the method should return an interval contained in 1 1 3 or 1 7 2 For practical reasons 1 1 and 2 2 are the most interesting answers 7 2 2 Function generators Because functions can be templated by parameters They have to be generated by the parser on the fly This is done by invoking the functional method of an object derived from the function_generator class For identical parameters the same function_class object should be returned which means that they have to be cached struct function_generator function generator const char x virtual function class const xoperator function params const amp const 0 virtual function_generator hi The constructor of this class requires the name of the function template so that it gets registered by the parser operator is called with a vector of encoded parameters If a function has no template parameters the default_function_generator class can be used instead to register it The first parameter of the constructor is the function name The second one is the address of the function_class object default_function_generator default_function_generator const char x function class const x Chapter 8 Bibliography 8 1 Description of Gappa 1 Marc Daumas and Guillaume Melquiond Certification of bounds on expressions involving rounded operators ACM Transactions on Mathematical Software 37 1 1 20 2010 2 Jean Michel Muller Nico
39. c a a c add_xars b a 1 ba l b c c add mibs a b c d a c b d add fils a b C 46 59 C 2 Theorems Theorem name Target Source add_firs add filq add firq add xilu add xiru sub xals sub xars sub mibs sub fils sub firs sub filq sub firq val xabs val xebs mul xals mul xars mul fils mul firs mul mars mul mabs XIJIAJ AIAJPAJ AJAJX cjojojojoljlojoja Q AAA A o Qjajajajoja mul mibs mul xilu mul xiru div xals div fir div fil div xilu div xiru sqrt mibs sqrt b sqrt a sqrt b sqrt_mibq a sqrt b sqrt b sqrt sqrt_xibu x sqrt a Gta b 40 T5 d sub_xals b a val_xabs val_xebs val_xabq a b b b a b a a a mul_mals a a a a b b a b S a b a b a val_xebq square_sqrt sqrt addf 1 a addf_2 addf_3 addf_4 addf_5 addf_7 MIVVY VIVI V vja Oo N IS HINI I IS ez y ojo a a a b addf 6 b b b addf 8 There are also some rewriting rules dealing with REL predicates Theorem name Target S
40. e rule foo gt bar it first performs the subtraction of both sides Then it normalizes this expression in the field of polynomial fractions with integer coefficients If this result is not zero Gappa warns about it As the normalization only deals with polynomials and integers false positive may appear when the expressions involve numer ical values or square roots or absolute values 6 alia 873 xx y 2 gt x y x 4 not equal U9 2 0 2 ar 0 057 equal but needs numerical computations sropeic ke gt gt 57 equal but involves square root and absolute value Warneimge x s Gy 2 ame z EV SO ota Semad Difference x Warning 1b 2 and 2e 1 5e 2 are not trivially equal Difference 2e 1 5e 2 1b 2 Warning sqrt x x and x are not trivially equal Difference sqrt x x x Results L aun fil i Option switch W no hint difference B 4 4 Warning bar is a variable without definition yet it is unbound Identifier bar neither represents an expression nor is it a sub term of any of the bounded expressions of the logical property This may mean an identifier was mistyped L SR Re din RY Warning x is a variable without definition yet it is unbound Option switch W no unbound variable B 4 5 Warning no path was found for foo The expression foo appears in one of the goals yet Gappa does not have any theorem that could be used to compute this expression or one of
41. em 36 59 A 4 Logical formulas As a consequence a first order formula with Peano arithmetic addition multiplication and equality on natural numbers can be expressed in Gappa s formalism It implies that Gappa s logical fragment is not decidable A 4 2 Expressiveness Equality between two expressions can be expressed as a bound on their difference e f in 0 0 For inequalities the difference can be compared to zero e f gt 0 The negation of the previous propositions can also be used Checking the sign of an expression could also be done with bounds here are two examples e e in 0 0 ande in 0 1 WV 1 e in 0 1 Logical negations of these formulas can be used to obtain strict inequalities They can also be defined by discarding only the zero case not e in 0 0 Disclaimer although these properties can be expressed it does not mean that Gappa is able to handle them efficiently Yet if a proposition is proved to be true by Gappa then it can be considered to be true even if the previous features were used in its expression Appendix B Warning and error messages B 1 Syntax error messages B 1 1 Error foobar at line 17 column 42 The Bison front end has detected a syntax error at the given location The error message is usually unusable so let us hope the location is enough for you to find what the problem is Tie SA ls Error syntax error unexpected expecting FUNID or at line 1 c
42. equally distributed a disjunction is the simplest solution but it can be avoided if needed For instance if x can only be 0 2 or 17 one can write SS ae dei a lo A i 0 ZN d A gt aon STA in 3 4 this dichotomy hint helps Gappa to understand that al is either 1 0 or i 3 2 4 Disjunction When the goal of a formula contains a disjunction one of the sides of this disjunction has to always hold with respect to the set of hypotheses This is especially important when performing dichotomies Even if Gappa is able to prove the formula in each particular branch of a dichotomy if a different property of the disjunction is used each time the tool will fail to prove the formula in the general case Note that whenever a contradiction is found for a specific set of hypotheses whichever side of the disjunction holds no longer matter since Gappa can infer any of them 3 3 Providing hints 3 3 1 Rewriting rules Internally Gappa tries to compute the range of mathematical terms For example if the tool has to bound the product of two factors it will check if it knows the ranges of both factors If it does it will apply the theorem about real multiplication in order to compute the range of the product Chapter 3 Formalizing a problem 11 59 Unfortunately there may be some expressions that Gappa cannot bound tightly This usually happens because it has no result on a sub term or because the expression is badly correlated In this c
43. erators fora new arithmetic 2 m mn nn 2l 12 1 Function classes o pass pesek sip En re y on 27 A222 Function Seneratorss2 sest A se Sed Fae ewe AR BE ewes 29 8 Bibliography 31 8 1 Description oF Gappa e s 4 2 ee GOA aan A Re Ae 31 8 2 Applications of Gappa PERDI AA ee a 24 2 ib ibejid 31 A Gappa language 33 A l Comments and embedded options 6 00 33 A 2 Tokens and operator priority 33 ALS Grammar oe et den A Bee wt eis e a E E Sh eee EOE RS ds ER 34 A4 Eopical formulas exa ais eee eer toe eae Gee oor woe Et EA Se Ss g sissa 35 A 4 1 Undecidabilitv ee 35 AAD EXPpressivenest u 34 Uk ee e e OA Ba AER OA we EAD Boa Roe e 36 Contents v B Warning and error messages 37 B 1 Syntax errormessages 2 22455 24266 e in E ale 37 B 1 1 Error foobar at line 17 column 42 34 B 1 2 Error unrecognized option bar L 37 B 1 3 Error redefinition of identifier foo 0000 37 B 1 4 Error rounding operator expected got foo ao eoa 37 B 1 5 Error invalid parameters for Lo 38 B 1 6 Error incorrect number of arguments for f00 2 2 38 B 2 Other error messages during pasa 38 B 2 1 Error undefined intervals are restricted to conclusions 0000000004 38 B 2 2 Error the range of foo is an empty interval ee 38 B 2 3 Error zero appears as a denominator in a rewriting rule o e 38 B 3 Proof fall res pee sudar ee le ee
44. es automatic proof generation of arithmetic proper ties is a tool intended to help verifying and formally proving properties on numerical programs and circuits handling floating point or fixed point arithmetic This tool manipulates logical formulas stating the enclosures of expressions in some intervals For example a formal proof of the property c 0 3 0 1 A 2a 3 4 gt b c 1 2 A a c 1 9 2 05 gt b 1 2 3 5 can be generated thanks to the following Gappa script am O 5 0 1 2 a aa 8 41 19 e ain 1 21 AN OO Io ar 1 ain 2 3 8 A gt a ef b gt b c c Through the use of rounding operators as part of the expressions Gappa is specially designed to deal with formulas that could appear when certifying numerical codes In particular Gappa makes it simple to bound computational errors due to floating point arithmetic Gappa is free software you can redistribute it and or modify it under the terms of the CeCILL Free Software License Agreement or under the terms of the GNU General Public License Refer to the files from the source archive for the precise wording of these two licences Gappa can be downloaded on its project page The tool and its documentation have been written by Guillaume Melquiond Inttp gappa gforge inria fr http www lri fr melquion Chapter 2 Invoking Gappa 2 1 Input and output Gappa reads the script whose
45. es are equal to their right hand sides without any other assumption This is indicated at the end of the rule PU x 2 0 0 R gt O El 200 El s o cl lt gt fe When generating a script for an external proof checker Gappa will add this rewriting rule as a global hypothesis For example when selecting the Coq back end with the option Bcog the output contains the line below Hypothesis aiim zZ RE aes can In this hypothesis _d is the d variable of the example while r9 and r2 are short notations for rO 2 d r0 R and rO R r0 R x d respectively In order to access the generated proof the user has to prove this hypothesis which can be trivially done with Coq s field tactic 5 3 3 Full listing R i ee tel aladas ie 23 2 ries eb cl 32 120 p 122 rasos 50 liar cells 2 gt Cl ws il sl 24 A ela ze N fun 60 8 A 20 R aim l is 8 9 8 gt wa ix am 2 ru 2 os 0 er erde 20 E ad i el lt je rl x 2 dx rl R gt rl R x rl R x d al lt s The answer is the same as before since Gappa easily proves that d is not zero Results r2 R in 638882156545b 64 3 46339e 08 2 24 7832 32771b 44 1 86282e 09 lt BS 23 9000 JE Another example of a Newton iteration is given in Section 6 1 Chapter 6 Using Gappa from other tools 6 1 Why and Gappa The Why software verification platform can be used to translate code annota
46. etter for the proof engine not to consider theorems that never return a useful range The mask argument of the functi on_class constructor is a combination of the following flags They indicate which theorems are known The corresponding methods should therefore have been overloaded Struct Funct ich class statie const int TH RND TH ENE TE ABS TH REL H ABS EXA BND TH_ABS_EXA_ABS TH_ABS_APX_BND TH_ABS_APX_ABS H_REL_EXA_BND TH_REL_EXA_ABS TH_REL_APX_BND TH_REL_APX_ABS We All the virtual methods for theorems have a similar specification If the result is the undefined interval interval the theorem does not apply Otherwise the last parameter is updated with the name of the theorem that was used for computing the returned interval The proof generator will then generate an internal node from the two intervals and the name When defining a new rounding operator overloading does not have to be comprehensive some functions may be ignored and the engine will work around the missing theorems round Given the range of aob compute the range of f a b enforce Given the range of f a b compute a stricter range of it absolute error Given no range compute the range of f a b aob relative_error Given no range compute the range of flab aob ab u absolute_error_from_exact_bnd Given the range of aob compute the range of f a b aob absolute error from exact abs Given
47. filename is passed as an argument to the tool or on its standard input if none Such a script is made of three parts the definitions the logical formula and the hints Warning messages error messages and results are displayed on the standard error output Gappa also sends to the standard output a formal proof of the logical formula its format depends on the selected back end Finally if the tool was unable to prove some goals its return code is a nonzero value For example the following command lines create a simple script in file test g pass it to Gappa and store the generated Coq proof in file test v file They also test the return code of Gappa and send the generated proof to Coq so that it is automatically checked Since the proof checker does not display anything it means no errors were detected and the result computed by Gappa is correct SE cano Y se alin 82 21 gt amp 5 alm Y LT S Tesesa gappa Bcog test g gt test v Results xe 39 38 alin O A Ss adas Mreritisa CO CE SETS S9u Return code is 0 coqc I path to gappalib coq test v Note that if no ranges are left unspecified in the logical formula Gappa will not have anything to display in case of success S seine S tt il 2 gap pal S echo Retina Code Is S24 Return code is 0 2 2 Command line options 2 2 1 Selecting a proof back end These options are mutually exclusive and cannot be embedded into scripts 4 59 2 2 Command line opt
48. ial comment Wno hint difference before the offending rule 5 2 Tang s exponential function 5 2 1 The algorithm In Table Driven Implementation of the Exponential Function in IEEE Floating Point Arithmetic Ping Tak Peter Tang described an implementation of an almost correctly rounded elementary function in single and double precision John Harrison later did a complete formal proof in HOL Light of the implementation in Floating point verification in HOL Light the exponential function Here we just focus on the tedious computation of the rounding error We consider neither the argument reduction nor the reconstruction part trivial anyway excepted when the end result is subnormal We want to prove that in the C code below the absolute error between e and the exponential EO of RO the ideal reduced argument is less than 0 54 ulp Variable n is an integer and all the other variables are single precision floating point numbers ra n 12 C ci e gen ae ala mm a2 F jo wil p 662 ar 18 7 s sl s2 ee sl gt 82 a S lt jo Let us note R the computed reduced argument and S the stored value of the ideal constant SO There are 32 such constants For the sake of simplicity we only consider the second constant 232 E is the value of the expression e computed with an infinitely precise arithmetic Z is the absolute error between the polynomial x a x a2 x and exp x 1 for x lt A 5 2 2
49. implicit rounding operator only applies to the results of arithmetic operations In particular a rnd b is not equivalent to a rnd b Itis equivalent to a b Finally we can also give a name to the infinitely precise result of the function to clearly show that both expressions have a similar arithmetic structure rnd float lt ieee_32 ne gt y rnd xx 1 x ss IL 7 aa 10 1 gt y a 2 7 y 2 ma 2 On the script above Gappa displays Results y alin L vera ain Sls 24 9 10016608 2 24 1 loza Sr OMS EOS 2 24 Dl Gappa displays the bounds it has computed Numbers enclosed in braces are approximations of the numbers on their left These exact left numbers are written in decimal with a power of two exponent The precise format will be described below 5 1 4 Complete version Previously found bounds are not as tight as they could actually be Let us see how to expand Gappa s search space in order for 1t to find better bounds Not only Gappa will be able provide a proof of the optimal bounds for the result of the function but it will also prove a tight interval on the computational absolute error 5 1 4 1 Notations X ao x is a floating point number Wy ints gt se iL sx Pp equivalent to y rnd x x rnd 1 x 2 GL sejja Chapter 5 Examples 17 59 The syntax for notations is simple The left hand side identifier is a name representing the expression on the right hand
50. ing operator B sl s2 S x rd 12 Rx Rx al Rx a2 So the round off error is e E while the other term is E EO As before the expressions E and EO are structurally different so Gappa grossly overestimates the bounds of E E0 This time we introduce a term Er with the same structure as EO but equal to E Since Z has no corresponding term in E we insert an artificial term 0 in Er to obtain the same structure Er S ll R 4 al x Rx R az KR x R R 0 Finally we tell Gappa how to compute e EO using E and Er ED gt E Er E0 Note that rather than using a hint this equality could also have been indicated as a hypothesis of the logical formula 5 2 3 Full listing rnd float lt ieee_32 ne gt aul SO AO 24 AD AS SON 2 0 12 1296011569 ahs 2 Sil 2857722180628 s2 13833605b 44 122 Taino iol ee IAP Bernd sell sp 122 ej male te ie al ar e e Prenda Al oe s rnd sl s2 SN sul ES r S DR R ELE S sl 352 Sil 4b G2 2 8 amp ell qr e sp IR CAI IZ A Er Sx 14 4R alxRxR a2x Rx R q R O S0 il ap RO sp al se RO RO aZ RO sy RO lt RO ap 24 4 E o ll Z in 55b 39 55b 39 S SO in 1b0 41 1b 41 R RO in 1b 34 1b 34 x 2m OO OZI ZN im da l 10176 1017601 gt G am 2 JIN amp 10 sin 2 EO
51. ions 2 2 1 1 Null back end Option Bnull Do not enable any back end This is the default behavior This is also the only back end compatible with the Munconstra ined option 2 2 1 2 Coq back end Option Bcoq When this back end is selected Gappa generates a script that proves the logical formula This script can be mechanically verified by the Coq proof checker It can also be reused in bigger formal developments made with Coq 2 2 1 3 Latex back end Option Blatex When this back end is selected Gappa generates a Latex file that contains the steps for proving the logical formula 2 2 1 4 Coq lambda term back end Option Bcoq lambda This back end is used by the gappa tactic available for the Coq proof checker It generates a lambda term that can be directly loaded by the proof checker but it only supports the features needed by the tactic For instance it does not support rewriting rules 2 2 2 Setting internal parameters 2 2 2 1 Internal precision Option Eprecision integer This option sets the internal MPFR precision that Gappa uses when computing bounds of intervals The default value is 60 and should be sufficient for most uses 2 2 2 2 Dichotomy depth Option Edichotomy integer This option limits the depth of a dichotomy split The default value is 100 It means that an interval of width 1 is potentially split into 2 intervals of width 271 relatively to the original interval This should be
52. is class is an interface to the name of the function its associated real operator and six theorems struct function_class function_class real_op type t int mask virtual interval round GinitervalNconst os Sicle esse E Sms virtual interval enforce intervaltconsttt SEd SEAS CONSE virtual interval absolute_error SEAS TEEN const virtual interval relative_error ESTOS ingie E Om virtual interval absolute_error_from_exact_bnd interval const amp std string const virtual interval absolute_error_from_exact_abs interval const std string const virtual interval absolute_error_from_approx_bnd interval const amp std string amp const virtual interval absolute_error_from_approx_abs interval const std string amp const virtual interval relative error from exact bnd interval const std string amp const virtual interval relative error from exact abs interval const std string amp const virtual interval relativ rror from approx bnd interval const amp std string const virtual interval relativ rror from approx abs interval const amp std string const valia Steel estas Cescrioriom O ECuasie Oy vireual sed string pretty name const 0 mirtual unctiom class y y The description function should return the internal name of the rounding operator It will be used when generating the notations of the proof When the generated notatio
53. its sub terms B 5 Warning messages during proof computation B 5 1 Warning when foo is in i1 bar cannot be proved When Gappa applies a case splitting bar foo it splits the interval of foo until the property about bar holds for any sub interval If the maximal dichotomy depth has been reached yet the property still does not hold the warning message displays the failing sub interval the leftmost one an 2 i Se 7 Se an A 3 se ff ES sep Welsasiales whem x ie im le f 1L 57772E 30 2 es Vo 47 ESBOLe 31 2 OO pi 27 ENDE 07 Nr cannot be proved Error some properties were not satisfied BND x x Option switch W no dichotomy failure Appendix B Warning and error messages 41 59 B 5 2 Warning case split on foo has not produced any interesting new result This warning is displayed when Gappa is successful in finding a case split that satisfies the goals yet the results obtained on the sub intervals are not interesting they have already been proved through a simpler analysis ca lp 2 Ses Be ue aL Akio E De Warning case split on x has not produced any interesting new result Results xe de il alia 12 8 Option switch W no dichotomy failure B 5 3 Warning case split on foo has no range to split This warning is displayed when Gappa is unable to find the initial range on which to split cases ae IN e al alin 2 Sal yf sep Warning case split on 1 x has no range to split Result
54. las Brisebarre Florent de Dinechin Claude Pierre Jeannerod Vincent Lef vre Guillaume Melquiond Nathalie Revol Damien Stehl and Serge Torres Handbook of F loating Point Arithmetic Birkhauser 2010 8 2 Applications of Gappa 3 Guillaume Melquiond and Sylvain Pion Formally certified floating point filters for homogeneous geometric predicates Theoretical Informatics and Applications 41 1 57 70 2007 4 Arnaud Tisserand High performance hardware operators for polynomial evaluation International Journal of High Per formance Systems Architecture 1 1 14 23 2007 5 Christoph Lauter and Florent de Dinechin Optimizing polynomials for floating point implementation Proceedings of the 8th Conference on Real Numbers and Computers 7 16 Santiago de Compostella Spain 2008 6 Sylvie Boldo Marc Daumas and Pascal Giorgi Formal proof for delayed finite field arithmetic using floating point operators Proceedings of the 8th Conference on Real Numbers and Computers 113 122 Santiago de Compostella Spain 2008 7 Sylvie Boldo Jean Christophe Filli tre and Guillaume Melquiond Combining Coq and Gappa for certifying floating point programs Proceedings of the 16th Calculemus Symposium 59 74 Grand Bend ON Canada 2009 8 Claude Pierre Jeannerod and Guillaume Revy Optimizing correctly rounded reciprocal square roots for embedded VLIW cores Proceedings of the 43rd Asilomar Conference on Signals Systems and C
55. le with the following script Gappa will complain that y and z are two different names for the same expression rnd float lt ieee_32 ne gt y nc mel 2 5 AA E E o 2 gt 0 3 1 3 Hints Hints for Gappa s engine can be added in this last section if the tool is not able to prove the logical formula These hints are either rewriting rules or bisection directives Approximate and accurate expressions can also be provided in this section in order to generate implicit rewriting rules 3 2 Preferred expressions and other peculiarities Gappa rewrites expressions by matching them with well known patterns The enclosure of an unmatchable expression will necessarily have to be computed through interval arithmetic As a consequence to ensure that the expressions will benefit from as much rewriting as possible special care needs to be taken when expressing the computational errors 10 59 3 3 Providing hints 3 2 1 Absolute and relative errors Let exact be an arithmetic expression and approx an approximation of exact The approximation usually contains round ing operators while the exact expression does not The absolute error between these two expressions is their difference approx exact Writing the errors differently will prevent Gappa from applying theorems on rounding errors x rnd x may lead to a worse enclosure than rnd x x The situation is similar for the relative error It should be expressed as
56. lified squaring proof graph x allowed logic simplifications even in case of indeterminate intervals documentation x added list of theorems e Version 0 16 6 2013 02 20 Coq lambda back end fixed crash on goals that are trivial implications e Version 0 16 5 2013 02 17 arithmetic x fixed incorrect round off error for values close to zero e Version 0 16 4 2013 02 07 proof graph Appendix D Changes 51 59 fixed crash when dichotomy fails to prove properties other than BND Version 0 16 3 2013 01 06 proof graph fixed crash when performing dichotomy while there are properties other than BND Version 0 16 2 2012 12 21 Coq lambda back end fixed incorrect certificate for intersection lemmas Version 0 16 1 2012 06 25 proof graph x fixed segfault when splitting cases on a degenerate goal x reenabled logic reasoning for ABS and REL predicates Coq lambda back end fixed signature of theorem mul_firs Version 0 16 0 2012 01 06 Coq lambda back end fixed syntax of proofs containing no variables x fixed typing of some floating point constants x fixed signature of theorems rel_refl div fil div fir Coq script back end x fixed typing of some floating point constants fixed syntax for Coq support library 0 17 fact database x added support for proving equalities between constants x changed fixed_of_fix so that it produces an EQL property Version 0
57. lowed to use an interrogation mark for an interval that appears in negative position in the logical formula tz ama 2 sv dl oa 10 11 B 2 2 Error the range of foo is an empty interval An interval has been interpreted as having reverted bounds o da 1271 Error the range of x is an empty interval Interval bounds are replaced by binary floating point numbers As a consequence Gappa can encounter an empty interval when it tightens a range appearing in a goal For example the empty set is the biggest representable interval that is a subset of the singleton 1 3 So Gappa fails to prove the following property i dos ai SS Error the range of 13e 1 is an empty interval B 2 3 Error zero appears as a denominator in a rewriting rule Gappa has a detected that a divisor is trivially equal to zero in an expression that appears in a rewriting rule This is most certainly an error i l im ET o A b E Appendix B Warning and error messages 39 59 B 3 Proof failures B 3 1 Error no contradiction was found The logical formula had no property in negative position or Gappa has discharged all of them yet this was not sufficient to prove the formula oz al a Haal gt mee x pl ma 2 31 KrRor DO conil ola as Toues B 3 2 Error some enclosures were not satisfied Only part of a conjunction of goals was proved to be true Gappa was unable to prove some other expressions or formulas which are displa
58. n cannot be reduced to a simple name comma separated additional parameters can be appended The back end will take care of formatting the final string This remark also applies to names 28 59 7 2 Defining rounding operators for a new arithmetic returned by the theorem methods see below The pretty_name function returns a name that can be used in messages displayed to the user Ideally this string can be reused in an input script The real_op_type value is the associated real operator This will be UOP_ID the unary identity function for standard rounding operators But it can be more complex if needed enum real op type UOP_ID UOP_NEG UOP_ABS BOP_ADD BOP_SUB BOP_MUL BOP_DIV The type will indicate to the parser the number of arguments the function requires For example if the BOP_DIAM type is associated to the function f then f will be parsed as a binary function But the type is also used by the rewriting engines in order to derive default rules for this function These rules involve the associated real operator the diamond in this example f a b cod fla b aob aob cod f a b cod fla b aeb aob cod _ f a b aeb aob cod cod aob cod aob cod For these rules and the following theorems to be useful the expressions f a b and aob have to be close to each other Bounding their distance is the purpose of the last ten theorems The first two theorems compute the range of f a b itself It is b
59. nding direction fixed lt lsb_weight rounding_direction gt Rounding to integer is a special case of fixed point rounding of weight 0 A syntactic shortcut is provided ME reo aa Olas Leia llo 4 4 4 4 Miscellaneous operators The following operators are underspecified and therefore not suitable for formal proofs 4 4 1 Functions with relative error This set of functions is defined with related theorems on relative error They can be used to express properties that cannot be directly expressed through unary rounding operators add sub mul _rel lt precision minimum _exponent gt If the minimum exponent is not provided the bound on the relative error is assumed to be valid on the entire domain Otherwise the interval 2 2 is excluded from the domain Talking about the expression add_rel lt 20 60 gt a b is like talking about a fresh expression c such that not la bl lt 1b 60 gt c a b lt 1b 20 4 4 2 Rounding operators with homogen properties To be written Chapter 5 Examples 5 1 A simple example to start from x 1 x 5 1 1 The C program Let us analyze the following function float float x assert 0 lt x amp amp x lt 1 return x 1 x This function computes the value x 1 x for an argument x between O and 1 The float type is meant to force the compiler to use IEEE 754 single precision floating point numbers We also assume
60. ng schemes to a higher level to remove constraints on approx accurate pairs x added rewriting rules for replacing an accurate expression by an approximate and an error e Version 0 5 6 2006 01 26 fact database cleaned theorems and removed redundant ones arithmetic x enabled test to zero with relative rounding it can still be disabled by Munconstrained Coq back end improved script generation proof graph x fixed premature halt when a case split was a failure x fixed case split not noticing newly discovered bounds main interface simplified display of hypotheses and sorted display of goals e Version 0 5 5 2005 12 24 whole engine x added square root no rule checking though modified rewriting rules to apply to approximates instead of just rounded values added ABS predicate to workaround abuse of absolute values in theorems syntax x added syntax to define user approximates fact database x added option to disable constraint checking around zero arithmetic generalized fixed point range enforcing to any expression proof paths x enhanced the detection of dead paths that contain cycles e Version 0 5 4 2005 11 25 syntax x reduced the number of false positive for unbound identifiers merged variables and functions anew in order to correctly detect define after uses errors Appendix D Changes 57 59 proof graph x added fifo processing of proof schemes x handled case
61. nt or a computer algebra system And they should be at least for Newton s relation because of its error prone expression 6 2 Coq and Gappa The Gappa Coq Library adds a gappa tactic to the Coq Proof Assistant This tactic invokes Gappa to solve properties about floating point or fixed point arithmetic It can also solve simple inequalities over real numbers The tactic is provided by the Gappa_tactic module It expects to find a Gappa executable called gappa in the user program path ihttp alt ergo lri fr thttp gappa gforge inria fr Shttp cog inria fr 26 59 6 2 Coq and Gappa Require Import Reals Require Import Fcore Require Import Gappa_tactic Open Scope R_scope Goal tom ad se Y E Ry aJa L 3 L 0 gt 0 lt sqrt x lt 1775 powerRZ 2 10 Proof gappa Qed The tactic recognizes fully applied rounding_fixedand rounding_float functions as rounding operators The script below proves that the difference between two double precision floating point numbers in 2 5 and 72 30 is exactly representable as a double precision floating point number Rounding direction does not matter for this example it has been arbitrarily chosen as rounding toward zero perint oniridie eo unan gto are ARSS GON Goal forall a hr a Dar a uno Gi gt lo al la gt 52 f 16 a lt 53 l6 gt 22 f 16 lt ip lt 30 is gt rnd a b daB BRO Ie unfold rnd gappa
62. nt numbers disabled relative error for subnormal numbers potentially disruptive homogen numbers cleaned up x added non homogen double rounded format Appendix D Changes 59 59 hint parser x added pseudo support for quotient in hint parser added support for C99 hexadecimal floating point format proof graph x replaced useless empty intersections by contradiction proofs e Version 0 4 5 2005 04 19 proof graph reworked modus ponens creation to fix an assertion failure in lemma invocation fact database x added conditional rules potentially disruptive homogen numbers split roundings between initialization and computation Coq back end implemented union
63. ntax x added a way to define new names for rounding operators simplified the handling of negative numbers 58 59 Coq back end x fixed representation of relative rounding Version 0 4 11 2005 08 27 proof graph fixed a missing dependency cleanup for an owned union node main interface x added parsing of embedded options Version 0 4 10 2005 08 27 proof graph x changed the node hypotheses to be graph hypotheses fact database x Switched some other facts to the absolute value of the denominators x added an explicit exclusion pattern for the rewriting rules e g x x is no more excluded main interface x added basic command line parsing for warnings and parameters Version 0 4 9 2005 08 26 numbers and arithmetic separated number handling from special arithmetic x added relative a format for handling varying precision rounding formulas x implemented absolute value fact database x made relative error depends on absolute value of the range proof graph x fixed a bug related to the clean up of the last graph of a dichotomy strengthened the role of modus nodes Version 0 4 8 2005 07 28 fact database x tightened intervals for a b a b x discarded multiple occurrences of the same term in the rewriting rules x Cleaned up rewriting rules Version 0 4 7 2005 07 22 hint parser x sped up verification Version 0 4 6 2005 07 15 floating poi
64. olumn 2 B 1 2 Error unrecognized option bar Gappa was invoked with an unknown option Variant unrecognized option bar at line 42 This error is displayed for options embedded in the script B 1 3 Error redefinition of identifier foo A symbol cannot be defined more than once even if the right hand sides of every definitions are equivalent a 1 a 1 Nor can it be defined after being used as an unbound variable b ax 2 a 1 B 1 4 Error rounding operator expected got foo Only rounding operators unary function close to the identity function can be prepended to the equal sign in a definition x add_rel lt 25 100 gt 1 Error rounding operator expected got add_rel lt 25 100 gt at line 1 column 19 38 59 B 2 Other error messages during parsing B 1 5 Error invalid parameters for foo A function template has been instantiated with an incorrect number of parameters or with parameters of the wrong type x float lt ieee_32 0 gt y Error invalid parameters for float at line 1 column 20 B 1 6 Error incorrect number of arguments for foo There are either less or more expressions between parentheses than expected by the function RE lie Se Ni 4 2 Error incorrect number of arguments for fixed lt 0 zr gt at line 1 column 17 B 2 Other error messages during parsing B 2 1 Error undefined intervals are restricted to conclusions You are not al
65. omputers 731 735 Pacific Grove CA USA 2009 145 1644001 1644003 hbtwes dx det org 1 007 978 0 81716 4705 6 15 https dx dol org 1 051 1ita0 2007003 http dx doi org 10 1504 IJHPSA 2007 013288 http hal archives ouvertes fr ensl 00260563 http hal archives ouvertes fr hal 00135090 https ds dei 6rg 10 1007 978 3 642 02614 0 10 http dx doi org 10 1109 ACSSC 2009 5469948 https dx dei org ooo AO dad aun 32 59 Bibliography 9 Claude Pierre Jeannerod Herv Knochel Christophe Monat Guillaume Revy and Gilles Villard A new binary floating point division algorithm and its software implementation on the ST231 processor Proceedings of the 19th Symposium on Computer Arithmetic 95 103 Portland OR USA 2009 10 Michael D Linderman Matthew Ho David L Dill Teresa H Meng and Garry P Nolan Towards program optimization through automated analysis of numerical precision Proceedings of the 8th International Symposium on Code Genera tion and Optimization 230 237 Toronto ON Canada 2010 11 Vincent Lef vre Philippe Th veny Florent de Dinechin Claude Pierre Jeannerod Christophe Mouilleron David Pfannholzer and Nathalie Revol LEMA towards a language for reliable arithmetic ACM SIGSAM Bulletin 44 1 2 41 52 2010 12 Sylvie Boldo and Thi Minh Tuyen Nguyen Hardware independent proofs of numerical programs Proceedings of the 2nd NASA Formal Methods Symposium 14 23
66. ource Constraints opp fibq REL a b REL mul filq EL a xb a x c REL mul firq EL a x b c x b REL a div_firg EL a b c b REL w w o ajajajo AN TRA alala pa o Appendix C Theorems of Gappa 47159 Finally there are theorems performing basic congruence Theorem name Target Source Constraints opp_fibe EQL a b EQL a b a f b add_file EQL a b a c EQL b c bc add_fire EQL a b c D EQL a c ac sub_file EQL a b a c EQL b c b He sub_fire EQL a b c b EQL a c a fe mul_file EQL a b ax c EQL b b bc mul_fire EQL a x b c x b EQL a c ac div_file EOL a b a c EQL b c b c div_fire EQL a b c b EQL a c a f c Appendix D Changes e Version 1 2 0 2015 05 19 fact database improved handling of powers of two in mul_fit fixed incorrect computation of the order 3 term of the relative error for division x added rewriting rules for emulating reverse propagation proof graph improved proof simplication proof paths improved performances by avoiding some absolute values improved detection of approximate exact pairs of expressions e Version 1 1 2 2014 10 14 back ends x fixed missing proof parts with the LaTeX back end main interface x
67. oximation of R and d is between 0 5 and 1 R i a QELE 24 ZA cl alin O 5 1 24 CMDS 20 8 IN 20 R im lo 8 llo 81 gt Next we have the two iterations Gappa s representation of fixed point arithmetic is high level the tool is only interested in the weight of the least significant bit The shifts that occur in an implementation only have an impact on the internal representation of the values not on the values themselves rl fixed lt 14 dn gt r0 x 2 fixed lt 16 dn gt d x ro ie a 0 icles sell 2 el a zy The property we are looking for is a bound on the absolute error between r2 and R nc EA R A iF We expect Gappa to prove that r2 is R 2 4 Unfortunately this is not the case Results sayy R SANS SS 5 039167 2 2 sci i SOS SOULS 2 2 354515 5 3 2 Adding hints With the previous script Gappa computes a range so wide for r2 R that it is useless This is not surprising The tool does not know what Newton s iteration is In particular Gappa cannot guess that such an iteration has a quadratic convergence Testing for r1 R instead does not give results any better Gappa does not find any useful relation between r1 and R as the first one is a rounded multiplication while the second one is an exact division So we have to split the absolute error into two terms a round off error we expect Gappa to compute and the convergence due to Newton s iteration IS el 20 2 2
68. s i aim il 1j Option switch W no dichotomy failure B 5 4 Warning case split on foo is not goal driven anymore This warning is displayed when Gappa is supposed to find the best case split for proving a property yet it does not know the range for this property or it has already proved it x im mil ih se ap Sl alm 2 SE release Warning case split on x is not goal driven anymore Results ar il atin 2 Option switch W no dichotomy failure Appendix C Theorems of Gappa C 1 Predicate S Gappa works on sets of facts about real valued expressions The following predicates are handled internally BND x I The value of expression x is included in interval I ABS x I The absolute value of expression x is included in interval I REL x y I The values of expressions x and y satisfy x y x 1 with Z FIX x k The value of expression x is such that dm Z x m ak FLT x k The value of expression x is such that 3m e Z x m 2 A m lt 2k NZR x The value of expression x is not zero EQL x v Expressions x and y have equal values In the definitions above I denotes an interval whose bounds have known numerical values while k is a known integer In the description of the theorems these parameters will usually be ignored For instance BND x just means that an enclosure of x is known In addition 1 EOL properties are also used to express rewriting hints pro
69. side Using one side or the other in the logical formula is strictly equivalent Gappa will use the defined identifier when displaying the results and generating the proofs though in order to improve their readability The second and third notations have already been presented The first one defines x as the rounded value of a real number xx In the previous example we had not expressed this property of x it is a floating point number This additional piece of information will help Gappa to improve the bound on the error bound Without it a theorem like Sterbenz lemma cannot apply to the 1 x subtraction 5 1 4 2 Logical formulas and numbers x in 0 1 gt y in 0 0 25 y z in 3b 27 3b 27 Numbers and bounds can be written either in the usual scientific decimal notation or by using a power of two exponent 3b 27 means 3 277 Numbers can also be written with the C99 hexadecimal notation 0x0 Cp 25 is another way to express the bound on the absolute error 5 1 4 3 Hints Although we have given additional data through the type of x Gappa is not yet able to prove the formula It needs some user hints 2 0 25 E 0 5 Es OS x ll IA x 1721022 y e zi t bound y by splitting the interval on x Y eS 3 bound y z by splitting The first hint indicates to Gappa that both hand sides are equivalent When it tries to bound the left hand side it can use the bounds it has found for the right hand side Please
70. t x lt 2 ensures wa double sqrt double x 22 assertion 23 postcondition 24 assertion 25 postcondition 26 assertion int i double t u 27 tcondit postcondition t sqrt_init x 66686686666 6655856666688 6686 8586 28 assertion SSSeeesceesesesesesesesesesesesesesesegeseeseges 118 Loop pragna BOLL 4 Function sqrt G loop invariant O lt i lt 3 Safety O 42 42 for i 0 i lt 2 Hi usO 5 t 3 t t x E Timeout 0 EJO Pretty Printer file a c VC postcondition On the left of the window are the proof obligations Once all of them are proved the code is guaranteed to match its specifica tion Green marks flag proof obligations that were automatically proved Selected proof obligations are displayed on the right here it is the postcondition of the sqrt function Gappa is not able to prove Newton s relation nor does it know that x x a yx holds These assertions are therefore left unproved Due to loop unrolling Newton s relation appears three times To factor these occurrences a lemma describing the relation has been added to the C code The Alt Ergo prover is used to check that the three occurrences indeed match this lemma In the end we have 72 proof obligations and only two of them are left unproved by the combination of Gappa and Alt Ergo They are mathematical identities on real valued expressions so they could easily be checked with an interactive proof assista
71. t once a 19 S WP a dle we These two hints will be used one after the other In particular none will be used when Gappa is doing a bisection with the other one By adding terms on the right of the symbol more complex hints can be built Beware of combinatorial explosions though The following hint is an example of a complex bisection it asks Gappa to find a set of sub ranges on u such that the goal on b is satisfied when the range on v is split into three sub intervals jo 8 Wi ww alin amp Rather than mentioning simple terms on the left hand side of hints one can also write a logical formula As a consequence Gappa no longer infers the termination condition from the goal but instead performs a bisection until the formula is satisfied This is especially useful if no enclosures of the terms appear in the goal or if the termination criteria is not even an expression enclosure rnd a a u Chapter 4 Supported arithmetic 4 1 Rounding directions Some of the classes of operators presented in the following sections are templated by a rounding direction This is the direction chosen when converting a real number that cannot be exactly represented in the destination format There are eleven directions zr toward zero aw away from zero dn toward minus infinity down up toward plus infinity od to odd mantissas ne to nearest tie breaking to even mantissas no to nearest tie breaking to odd mantissas nz to nearest
72. ted with pre and postconditions into proof obligations suitable for Gappa By installing Frama C first and then Why in order to build the Jessie plugin one gets a tool for directly certifying C programs with Gappa 6 1 1 Example floating point square root The example below demonstrates the usage of these tools The C file defines a sqrt function that computes the square root with a relative accuracy of 27 for an input x between 0 5 and 2 requires 0 5 lt x lt 27 ensures abs result 1 sqrt x lt Oxlp 6 x abs 1 sqrt x el double sqrt_init double x lemma quadratic_newton forall real x t x gt 0 gt Vise Gee e i 7 Noa 7 il 7 NoE ae ie a si Se a te ase al ENS a AS Ct GS 9 las sr Was A EEr w ere k Erre requires 0 5 lt x lt 2 ensures abs result sqrt x lt 0x1p 43 abs sqrt x x double sqrt double x WNE SE double t us w gepe diant ox loop pragma UNROLL 4 loop invariant 0 lt i lt 3 x Ihttp whv lri fr http frama c com 24 59 6 1 Why and Gappa for a 07 1 lt 2 41 ti 0 5 Te a 3 E SES se MO essa Val satis 03 la e me QIS LQ AS SS Nee ern E MEN So 203 NS ea WAS ka ee eier sa II NS Cl AS Ca 1 5 t 0 5 err err s err x ME assec Nal sili il Veces TO xo Nes y NE e ee us IO ass Y IN Sem Ee eee Co retcturai x by The code st
73. the quotient between the absolute error and the exact value approx exact exact For enclosures of relative errors this is the same approx exact 3 2 2 Global errors The approx and exact expressions need to have a similar structure in order for the rewriting rules to kick in E g if exact 1s a sum of two terms a and b then approx has to be the sum of two terms c and d such that c and d are approximations of a and b respectively Indeed the rewriting rule for the absolute error of the addition is a b c d gt a c b d Simi larly the rewriting rules for the multiplication keep the same ordering of sub terms For example one of the rules is a b c x d gt a c x b c x b d Therefore one should try not to mess with the structure of expressions If the two sides of an error expression happen to not have a similar structure then a user rewriting rule has to be added in order to put them in a suitable state For instance let us assume we are interested in the absolute error between a and d but they have dissimilar structures Yet there are two expressions b and c that are equal and with structures similar to a for b and d for c Then we just have to add the following hints to help Gappa lo OS Oe ap ore Wore alia OO est e pone sis a bj a is an approximation of b er ad Er Cue S an approximation or a 3 2 3 Discrete values When an expression is known to take a few separate values that are not
74. the range of a ob compute the range of f a b aob absolute_error_from_approx_bnd Given the range of f a b compute the range of f a b aob absolute error from approx abs Given the range of f a b compute the range of f a b aob relative_error_from_exact_bnd Given the range of aob compute the range of Fab a0 compute the range of jer a relative_error_from_exact_abs Given the range of a o b 5 R E f a b aob relative_error_from_approx_bnd Given the range of f a b compute the range of 44422 a b aob i f relative error from approx abs Given the range of f a b compute the range of 222 Chapter 7 Customizing Gappa 29 59 The enforce theorem is meant to trim the bounds of a range For example if this expression is an integer between 1 7 and 3 5 then it is also a real number between 2 and 3 This property is especially useful when doing a dichotomy resolution since some of the smaller intervals may be reduced to a single exact value through this theorem Since the undefined interval is used when a theorem does not apply it cannot be used by enforce to flag an empty interval in case of a contradiction The method should instead return an interval that does not intersect the initial interval Due to formal certification considerations it should however be in the rounded outward version of the initial interval For example if the expression is an integer
75. vided by the user C 2 Theorems There are three categories of theorems in Gappa theorems about real arithmetic theorems about rounding operators and rewriting rules In the following variables a b c and d represent arbitrary expressions Gappa is using backward reasoning so they are filled by matching the goal of a theorem against the property Gappa wants to compute If some theorem mentions both a and b but only one of them appears on the right hand side then Gappa infers the other one so that b is an approximate value of a See Section 3 3 2 for more details There may be additional constraints on the expressions that require some of them to be syntactically different denoted a b or to be syntactically constant denoted a or to be syntactically variable denoted ar 44 59 C 2 Theorems Theorem name Goal Hypotheses C 2 1 Theorems about real arithmetic Theorem name Goal Hypotheses sub of eql BND a b EOL a b E eql_of_cst EQL a b BND a BND b c rel refl REL a a eql_trans EQL b c EQL b a EQL a c eql_trans EQL c a EQL c b EQL b a x neg BN
76. ving to fill some unspecified ranges In that case Gappa will not display anything about them f ain l 2 SS 0 a aim 2 notice the contradiction between the hypotheses Results remaining results are pointless anything can be proved Inequalities that give an upper bound on an absolute value are treated specially They are assumed to be full enclosures with a lower bound equal to zero In other words x lt 1 is syntactic sugar for x in 0 1 Gappa does not know much about inequalities as they never appear as hypotheses of its theorems They can only be used to refine a previously computed enclosure For instance Gappa cannot deduce a contradiction from x x lt 1 alone It needs to know either an enclosure of x or a nonnegative enclosure of x x 3 1 1 2 Relative errors The relative error between an approximate value x and a more precise value y is expressed by x y y For instance when one wants to prove a bound on it one can write f coo 2 wy Frl lt el J However this bound can only be obtained if y is proved to be nonzero Similarly if a hypothesis was a bound on a relative error this hypothesis would be usable by Gappa only if it can prove that its denominator is nonzero Gappa provides another way of expressing relative errors which does not depend on the denominator being nonzero It cannot be used as a subexpression it can only be used as the left hand side of an enclosure gt x
77. xt two lines show how many theorem instances Gappa has prepared The first number tells how many have been considered and the second number tells how manv of them were discarded because their hvpotheses could never have been satisfied Once both sets are ready Gappa tries to deduce new properties by repeatedly applying the prepared theorems The next statistic show how many of those theorems Gappa tried to apply Applications are successful if Gappa could satisfy theorem hypotheses Even if an application succeeded the deduced property could have been partly useless because a stronger property had already been found at the time the theorem was applied The last two lines track these cases 6 59 2 3 Embedded options 2 2 4 Enabling and disabling warning messages By default all the warning messages are enabled See annex for details on warning messages displayed during parsing and during computations 2 3 Embedded options Options setting internal parameters or enabling warning messages can be embedded in a Gappa proof script It is especially important when the logical property cannot be proved with the default parameters These options are passed through a special comment syntax Edichotomy 200 Chapter 3 Formalizing a problem 3 1 Sections of a Gappa script A Gappa script contains three parts The first one is used to give names to some expressions in order to simplify the writing of the next parts
78. yed after the message sin 1 21 gt P al alin Ne gt 2 ain 2 21 3 Warning case split on x 2 has not produced any interesting new result Results x and SJ Error some properties were not satisfied BND x 2 best FT 4 B 4 Warning messages during parsing B 4 1 Warning renaming identifier foo as bar When a definition foo expr is given to Gappa the name foo is associated to the expression expr This name is then used whenever Gappa outputs expr If another definition bar expr is later provided the new name supersedes the name given previously a 42 b 42 La alin 2 Warning renaming identifier a as b at line 2 column 7 is lo as OO B 4 2 Warning although present in a quotient the expression foo may not have been tested for non zeroness When Gappa verifies that both sides of a user rewriting rule are equivalent it does not generate additional constraints to verify that denominators appearing in the expressions are not zero For example the rule 1 1 x gt x only applies when x is not zero yet Gappa does not test for it No warning messages are displayed when constraints are added to the rewriting rule whether these constraints are sufficient or not E g 1 1 x gt x x lt gt 0 Option switch W no null denominator 40 59 B 5 Warning messages during proof computation B 4 3 Warning foo and bar are not trivially equal When Gappa verifies th

User's Guide for Gappa

Contents

Download Pdf Manuals

Related Search

Related Contents