Using Gappa from other tools ============================ .. _tool-why: Why and Gappa ------------- The `Why `_ software verification platform can be used to translate code annotated 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. 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 :math:`2^{-43}` for an input ``x`` between 0.5 and 2. .. code-block:: c /*@ requires 0.5 <= x <= 2; ensures \abs(\result - 1/\sqrt(x)) <= 0x1p-6 * \abs(1/\sqrt(x)); */ double sqrt_init(double x); /*@ lemma quadratic_newton: \forall real x, t; x > 0 ==> \let err = (t - 1 / \sqrt(x)) / (1 / \sqrt(x)); (0.5 * t * (3 - t * t * x) - 1 / \sqrt(x)) / (1 / \sqrt(x)) == - (1.5 + 0.5 * err) * (err * err); */ /*@ requires 0.5 <= x <= 2; ensures \abs(\result - \sqrt(x)) <= 0x1p-43 * \abs(\sqrt(x)); */ double sqrt(double x) { int i; double t, u; t = sqrt_init(x); /*@ loop pragma UNROLL 4; @ loop invariant 0 <= i <= 3; */ for (i = 0; i <= 2; ++i) { u = 0.5 * t * (3 - t * t * x); //@ assert \abs(u - 0.5 * t * (3 - t * t * x)) <= 1; /*@ assert \let err = (t - 1 / \sqrt(x)) / (1 / \sqrt(x)); (0.5 * t * (3 - t * t * x) - 1 / \sqrt(x)) / (1 / \sqrt(x)) == - (1.5 + 0.5 * err) * (err * err); */ //@ assert \abs(u - 1 / \sqrt(x)) <= 0x1p-10 * \abs(1 / \sqrt(x)); t = u; } //@ assert x * (1 / \sqrt(x)) == \sqrt(x); return x * t; } The code starts by calling the ``sqrt_init`` function. It returns an approximation of :math:`x^{-1/2}` with a relative accuracy of :math:`2^{-6}`. 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 :math:`|\mathit{approx} - \mathit{exact}| \le \mathit{error} \times |\mathit{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. 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 ref:`example-fixed`, 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. .. code-block:: gappa rsqrt = 1 / sqrt(x); err = (t - rsqrt) / rsqrt; { ... } u ~ 0.5 * t * (3 - t * t * x); (0.5 * t * (3 - t * t * x) - rsqrt) / rsqrt -> - (1.5 + 0.5 * err) * (err * err); u ~ rsqrt; 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 :math:`1 / \sqrt{x}` had been :math:`2^{-1}` instead of :math:`2^{-10}`, Gappa would still have succeeded. Execution results ~~~~~~~~~~~~~~~~~ Passing the program above to the Frama-C/Jessie tool produces the following console output... .. code-block:: console $ 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 [jessie] File a.jessie/a.jc written. [jessie] File a.jessie/a.cloc written. [jessie] Calling Jessie tool in subdir a.jessie Generating Why function sqrt [jessie] Calling VCs generator. gwhy-bin [...] why/a.why Computation of VCs... Computation of VCs done. Reading GWhy configuration... Loading .gwhyrc config file GWhy configuration loaded... Creating GWhy Tree view... \...and displays the following user interface. .. image:: images/gwhy-sqrt.png On the left of the window are the proof obligations. Once all of them are proved, the code is guaranteed to match its specification. 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 :math:`x \times \sqrt{x}^{-1} = \sqrt{x}` 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 assistant or a computer algebra system. (And they should be, at least for Newton's relation, because of its error-prone expression.) 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. .. code-block:: coq From Coq Require Import Reals. From Flocq Require Import Core. From Gappa Require Import Gappa_tactic. Open Scope R_scope. Goal forall x y : R, 3/4 <= x <= 3 -> 0 <= sqrt x <= 1775 * powerRZ 2 (-10). Proof. gappa. Qed. The tactic recognizes fully-applied ``rounding_fixed`` and ``rounding_float`` functions as rounding operators. The script below proves that the difference between two double precision floating-point numbers in :math:`[\frac{52}{16}, \frac{53}{16}]` and :math:`[\frac{22}{16}, \frac{30}{16}]` 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.) .. code-block:: coq Definition rnd := rounding_float rndZR 53 (-1074). Goal forall a_ b_ a b : R, a = rnd a_ -> b = rnd b_ -> 52 / 16 <= a <= 53 / 16 -> 22 / 16 <= b <= 30 / 16 -> rnd (a - b) = (a - b). Proof. unfold rnd; gappa. Qed. The tactic handles goals and hypotheses that are either equalities of real numbers, :math:`e_1 = e_2`, or pairs of inequalities on real numbers, :math:`b_1 \le e \le b_2`, or inequalities expressing relative errors, :math:`|e_1 - e_2| \le b \cdot |e_2|`. For inequalities, the *b* bounds have to be explicit dyadic numbers. The tactic also recognizes properties written as :math:`|e| \le b` as syntactic sugar for :math:`0 \le |e| \le 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. .. code-block:: coq Definition format := generic_format radix2 (FLT_exp (-1074) 53). Goal forall a b : R, format a -> format b -> 52 / 16 <= a <= 53 / 16 -> 22 / 16 <= b <= 30 / 16 -> format (a - b). Proof. unfold format; gappa. Qed.