Re: SPARK and integer arithmetic

[moy@adacore.com]

Hi Florian,

Sorry for jumping in so late in the game, I just discovered your discussion yesterday. The problem you have with your specification is that it mixes modular integers with signed integers. These do not mix so easily with the provers we currently ship with GNATprove: with CVC4 and Z3, modular types are converted into bitvectors and signed integers into mathematical integers; with Alt-Ergo both are converted into mathematical integers, with modulo operations where needed. In both cases, provers have difficulties dealing with the mix. 

An easier solution here is to use 64 bits modular types as a proxy type for infinite precision integer type, given that you deal with operations that cannot exceed the bounds of a 64 bits modular integer. That way, the translation for CVC4 and Z3 is fully in bitvectors, so you have a chance to get fully automatic proof.

This is what I did, defining Address_Integer as follows:

   type Address_64 is mod 2**64;
   subtype Address_Integer is Address_64 range 0 .. Address_64(Address'Last);

Then, GNATprove produces an interesting counterexample for your postcondition:

sum.ads:26:19: medium: postcondition might fail, cannot prove Address_Inside_Object'Result = ((L.L_Addr <= Addr) and (Address_Integer (Addr) < (Address_Integer (L.L_Addr) + Address_Integer (L.P_Vaddr) + L.P_Memsz (e.g. when Addr = 1934972246 and Address_Inside_Object'Result = False and L = (L_Addr => 0, P_Vaddr => 3254779904, P_Memsz => 234881024))

You can copy-paste these values inside a test:

  with Sum; use Sum;

  procedure Test_Sum is
     Addr : Address := 1934972246;
     L : Link_Map := (L_Addr => 0, P_Vaddr => 3254779904, P_Memsz => 234881024);
     B : Boolean;
  begin
     B := Address_Inside_Object (L, Addr);
  end Test_Sum;

and check that indeed these values violate the postcondition:

  $ ./test_sum 
  raised SYSTEM.ASSERTIONS.ASSERT_FAILURE : failed postcondition from sum.ads:26

The problem is that your first inequality is not the correct one, you're missing the addition of L.P_Vaddr (which you do correctly in the C version you point to in another thread). Here is a correct version of your postcondition:

     with Post => Address_Inside_Object'Result
       = ((Address_Integer (L.L_Addr) + Address_Integer (L.P_Vaddr) <= Address_Integer(Addr))
          and (Address_Integer (Addr)
                 < (Address_Integer (L.L_Addr) + Address_Integer (L.P_Vaddr)
                    + Address_Integer (L.P_Memsz))));

This version is proved automatically by GNATprove (although with a large timeout):

sum.ads:26:19: info: postcondition proved (CVC4: 2 VC in max 4.8 seconds and 6546 steps; Z3: 1 VC in max 76.5 seconds and 247567 steps)

I think we could also get GNATprove to prove your original specification, but this will require more effort to guide the proof through ghost code, possibly requiring combination of SMT solvers and static analysis, similar to what we did in this paper: http://www.spark-2014.org/entries/detail/research-corner-floating-point-computations-in-spark

Let us know if you do other similar experiments with SPARK!