Search code examples
adaproofinvariantsproof-of-correctnessspark-ada

How to prove this invariant?


I aim to prove that the Horner's Rule is correct. To do so, I compare the value currently calculated by Horner with the value of "real" polynominal.
So I made this piece of code:

package body Poly with SPARK_Mode is
   function Horner (X : Integer; A : Vector) return Integer is
      Y : Integer := 0;
      Z : Integer := 0 with Ghost;
   begin
      for I in reverse A'First .. A'Last loop
         pragma Loop_Invariant (Y * (X ** (I - A'First + 1)) = Z);
         Y := A(I) + Y * X;
         Z := Z + A(I) * (X ** (I - A'First));
      end loop;
      pragma Assert (Y = Z);
      return Y;
   end Horner;
end Poly;

Which should prove the invariant. Unfortunately, gnatprove tells me:

cannot prove  Y * (X ** (I - A'First + 1)) = Z
e.g. when A = (1 => 0, others => 0) and A'First = 0 and A'Last = 1 and I = 0 and X = 1 and Y = -1 and Z = 0

How does it work that Y=-1 in this case? Do you have any ideas how to fix this?


Solution

  • the counterexample here is spurious, it does not correspond to a real invalid execution. The arithmetic is too complex for provers to get, which leads both to the loop invariant preservation not being proved, and the spurious counterexample.

    To investigate such an unproved check, you must enter the "auto-active" mode of proving properties, which requires to break down the property in smaller ones until either automatic provers can deal with the smaller steps, or you can isolate an unproved elementary property that you can isolate in a lemma, that you can verify separately.

    Here I introduced a ghost variable YY for the value of Y at the beginning of an iteration, and broke down the loop invariant in smaller and smaller assertions, which showed that the problem was the exponentiation (X ** (I - A'First + 1) = X * (X ** (I - A'First)) that I also isolated in an assertion:

    package body Poly with SPARK_Mode is
       function Horner (X : Integer; A : Vector) return Integer is
          Y : Integer := 0;
          Z : Integer := 0 with Ghost;
          YY : Integer with Ghost;
       begin
          for I in reverse A'First .. A'Last loop
             pragma Loop_Invariant (Y * (X ** (I - A'First + 1)) = Z);
             YY := Y;
             Y := A(I) + Y * X;
             Z := Z + A(I) * (X ** (I - A'First));
             pragma Assert (Z = YY * (X ** (I - A'First + 1)) + A(I) * (X ** (I - A'First)));
             pragma Assert (X ** (I - A'First + 1) = X * (X ** (I - A'First)));
             pragma Assert (Z = YY * X * (X ** (I - A'First)) + A(I) * (X ** (I - A'First)));
             pragma Assert (Z = (YY * X + A(I)) * (X ** (I - A'First)));
             pragma Assert (Z = Y * (X ** (I - A'First)));
          end loop;
          pragma Assert (Y = Z);
          return Y;
       end Horner;
    end Poly;
    

    Now all assertions and the loop invariant are proved using --level=2 with SPARK Community 2020. Of course some assertions are not needed, so you can remove them.