How do I prove code with a real axiomatic in Frama

I have changed the int type to float in the "Inner Product" code from the ACSL-by-Example book (the code with int type worked for me) and now I am not able to prove the loop invariant inner. I have added some checks for inf and NaN without any success.

#include "limits.h"

/*@
  predicate  Unchanged{K,L}(float* a, integer first, integer last) =
    \forall integer i; first <= i < last ==>
    \at(a[i],K) == \at(a[i],L);

  predicate  Unchanged{K,L}(float* a, integer n) =
    Unchanged{K,L}(a, 0, n);

  lemma UnchangedStep{K,L}:
    \forall float *a, integer n;
    0 <= n ==>
    Unchanged{K,L}(a, n) ==>
    \at(a[n],K) == \at(a[n],L) ==>
    Unchanged{K,L}(a, n+1);

  lemma UnchangedSection{K,L}:
    \forall float *a, integer m, n;
    0 <= m <= n ==>
    Unchanged{K,L}(a, n) ==>
    Unchanged{K,L}(a, m);
*/


/*@ axiomatic InnerProductAxiomatic
  {
  logic real InnerProduct{L}(float* a, float* b, integer n, float init)
  reads a[0..n-1], b[0..n-1];

  axiom InnerProductEmpty:
    \forall float *a, *b, init, integer n;
    n <= 0 ==> InnerProduct(a, b, n, init) == init;

  axiom InnerProductNext:
    \forall float *a, *b, init, integer n;
    n >= 0 ==>
    InnerProduct(a, b, n + 1, init) ==
    InnerProduct(a, b, n, init) + a[n] * b[n];

  axiom InnerProductRead{L1,L2}:
    \forall float *a, *b, init, integer n;
    Unchanged{L1,L2}(a, n) && Unchanged{L1,L2}(b, n) ==>
    InnerProduct{L1}(a, b, n, init) ==
    InnerProduct{L2}(a, b, n, init);
  }*/

/*@
  predicate ProductBounds(float* a, float* b, integer n) =
    \forall integer i; 0 <= i < n ==>
    (INT_MIN <= a[i] * b[i] <= INT_MAX) ;

  predicate InnerProductBounds(float* a, float* b, integer n, float init) =
    \forall integer i; 0 <= i <= n ==>
    INT_MIN <= InnerProduct(a, b, i, init) <= INT_MAX;
*/

/*@
  requires valid_a: \valid_read(a + (0..n-1));
  requires valid_b: \valid_read(b + (0..n-1));
  requires \is_finite(init);
  requires !\is_NaN(init);
  requires bounds: ProductBounds(a, b, n);
  requires bounds: InnerProductBounds(a, b, n, init);
  requires (n < 100) && (n>=0);
  requires \forall integer i; 0 <= i < n ==>  \is_finite(a[i]);
  requires \forall integer i; 0 <= i < n ==>  \is_finite(b[i]);
  requires \forall integer i; 0 <= i < n ==>  !\is_NaN(b[i]);
  requires \forall integer i; 0 <= i < n ==>  !\is_NaN(a[i]);

  assigns \nothing;
  ensures result: \result == InnerProduct(a, b, n, init);
  ensures unchanged: Unchanged{Here,Pre}(a, n);
  ensures unchanged: Unchanged{Here,Pre}(b, n);
*/

float inner_product(const float* a, const float* b, int n, float init)
{
  int i = 0;
  /*@
    loop invariant index: 0 <= i <= n;
    loop invariant inner: init == InnerProduct(a, b, i, \at(init,Pre));
    loop assigns i, init;
    loop variant n-i;
  */
  while (i < n) {
    init = init + a[i] * b[i];
    i++;
  }
  return init;
}

How can I pass? Where to get the good cases with proves of real computations?

And frankly speaking I would like then to prove my loop invariant for Sine. I created a lemma for it (bounded Sine Taylor series) and tested it as a function. And I don't know a way how to start proving it.

/*@
axiomatic SinNAxiomatic
{
logic real Sinnn {l} (real x, real sum, real current, integer i, integer i_max);
axiom SinnnEmpty: \forall real x, real sum, real current, integer i, integer i_max; (\abs(current) < 0.00001) || (i == i_max) ==> Sinnn(x, sum, current, i, i_max)
== sum + current;
axiom SinnnNext: \forall real x, real sum, real current, integer i, integer i_max; \abs(current) > 0.00001 ==> Sinnn(x, sum, current, i, i_max) ==
Sinnn(x, sum + current, current * (-1.0 * x * x / ((2 * i) * (2 * i + 1))), i + 1, i_max);

lemma  SinnnMemCmp{L1,L2}: \forall real x, real sum, real current, integer i, integer i_max;
\at(x, L1)==\at(x, L2) && \at(sum, L1)==\at(sum, L2) &&  \at(current, L1)==\at(current, L2) && \at(i, L1)==\at(i, L2) && \at(i_max, L1)==\at(i_max, L2)
  ==> Sinnn{L1}(x, sum, current, i, i_max) == Sinnn{L2}(x, sum, current, i, i_max);
}
*/
float SinTailor(float x) {
        float n = x;
        float sum = 0.0;
        int i = 1;
/*@
loop invariant over: \abs(sum - Sinnn(x, 0, x, 1, i - 1)) <= 0.001;
loop assigns sum, n, i;
*/
        do
        {
            sum += n;
            n *= -1.0 * x * x / ((2 * i) * (2 * i + 1));
            i++;
            //printf("sum my=%f recursion=%f\n", sum, TestSinnn(x, 0, x, 1, i - 1)); //prints the same values

        }
        while (fabs(n)> 0.00001);
return sum;
}

I noticed that for internal \sin there are a few lemmas like -1<=\sin(x)<=1, \cos^2(x)+\sin^2(x)==1, etc., but we cannot prove \result==\sin(x) for a sin(x) returning function. Or am I wrong here?

回答1:

I'm going to answer the first part of your question. The problem lies in the axiom InnerProductNext, more precisely here InnerProduct(a, b, n + 1, init) == InnerProduct(a, b, n, init) + a[n] * b[n]. ACSL specification use real arithmetics, while your function use 32 bits floating point computation. Due to the rounding that occurs in the C function, the proof cannot be achieved. The fix is simple enough: round all operations appropriately in your lemma.

  axiom InnerProductNext:
    \forall float *a, *b, init, integer n;
    n >= 0 ==>
    InnerProduct(a, b, n + 1, init) ==
    (float)(InnerProduct(a, b, n, init) + (float)(a[n] * b[n]));

This is sufficient for the proof to succeed.

回答2:

Regarding the second part of your question, there seems to be some deep misunderstanding about the semantics of ACSL axiomatics. In particular:

your SinnnEmpty axiom is basically saying that for any x and sum, we have Sinnn(x,sum,0,0,0) == sum (basically, I've just instantiated current, i and i_max with 0, which makes the left part of the implication true). It is very unlikely that's what you wanted to say there
SinnnMemCmp is a tautology. In fact, inside global annotations, the \at() construction and logic labels are meant to speak about C variables and memory locations. Here, you only have purely logic variables bound by universal quantification: they are immutable and not tied to a C memory state, that is, their value does not depend on a logic label.

Finally, once you have sorted out your definition on what Sinnn should do from an ACSL perspective (i.e. playing with mathematical reals that happily ignore rounding problems), you'll end up with the issue of trying to check that results applicable at this mathematical level are still true when computing with finite precision floating-points numbers. This is usually a difficult task, and not all automated provers have a good support for floating-point computation (see e.g. this document for more information).