unprovable checks with size constraint for successor

[kanigsson]

The following RecordFlux spec results in unprovable overflow checks and unprovable conditions:

package Over is
   type Byte is range 0 .. 2 ** 8 - 1 with Size => 8;
   type Length_16 is mod 2 ** 16;

   type My_Seq is sequence of Byte;

   type Repr is
      message
         Count : Byte;
         Length : Length_16;
         Hash : My_Seq
            with Size => 32
            then Structs
               with Size => 8 * Length - 16 - (Hash'Last - Count'First + 1)
               if 8 * Length >= 16 + (Hash'Last - Count'First + 1);
         Structs : My_Seq;
      end message
         with Byte_Order => Low_Order_First;
end Over;

One example is the postcondition of Set, indeed I don't see any conditions that would protect the computation against overflow, and I don't see any reason for the condition to hold.

Could it be that the condition should be for the Structs field and not the Hash field in the postcondition? That would seem more reasonable at first glance.

[treiher]

rflx-test-message.ads:501:99: medium: overflow check might fail                                                                                                                                                     
  501 |               RFLX_Types.U64 (Get_Length (Ctx)) * 8 >= RFLX_Types.U64 (Field_Last (Ctx, F_Hash)) - RFLX_Types.U64 (Field_First (Ctx, F_Count)) + 17                                                         
      |                                                        ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~                                                                
  reason for check: result of subtraction must fit in a 64-bits machine integer                                       
  possible fix: use pragma Overflow_Mode or switch -gnato13 or unit Ada.Numerics.Big_Numerics.Big_Integers             
                                                                                                                      
rflx-test-message.ads:501:145: medium: overflow check might fail                                                      
  501 |               RFLX_Types.U64 (Get_Length (Ctx)) * 8 >= RFLX_Types.U64 (Field_Last (Ctx, F_Hash)) - RFLX_Types.U64 (Field_First (Ctx, F_Count)) + 17
      |                                                        ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~^~~~
  reason for check: result of addition must fit in a 64-bits machine integer                                          
  possible fix: use pragma Overflow_Mode or switch -gnato13 or unit Ada.Numerics.Big_Numerics.Big_Integers             
                                                           
rflx-test-message.ads:626:99: medium: overflow check might fail
  626 |               RFLX_Types.U64 (Get_Length (Ctx)) * 8 >= RFLX_Types.U64 (Field_Last (Ctx, F_Hash)) - RFLX_Types.U64 (Field_First (Ctx, F_Count)) + 17
      |                                                        ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
  reason for check: result of subtraction must fit in a 64-bits machine integer                                       
  possible fix: use pragma Overflow_Mode or switch -gnato13 or unit Ada.Numerics.Big_Numerics.Big_Integers             
                                                           
rflx-test-message.ads:626:145: medium: overflow check might fail                                                      
  626 |               RFLX_Types.U64 (Get_Length (Ctx)) * 8 >= RFLX_Types.U64 (Field_Last (Ctx, F_Hash)) - RFLX_Types.U64 (Field_First (Ctx, F_Count)) + 17
      |                                                        ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~^~~~
  reason for check: result of addition must fit in a 64-bits machine integer                                          
  possible fix: use pragma Overflow_Mode or switch -gnato13 or unit Ada.Numerics.Big_Numerics.Big_Integers             
                                                           
rflx-test-message.ads:820:128: medium: overflow check might fail
  820 |                              and then RFLX_Types.U64 (Cursors (F_Length).Value) * 8 >= RFLX_Types.U64 (Cursors (F_Hash).Last) - RFLX_Types.U64 (Cursors (F_Count).First) + 17)))
      |                                                                                        ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
  reason for check: result of subtraction must fit in a 64-bits machine integer                                       
  possible fix: add precondition (RFLX_Types.U64 (Cursors (F_Hash).Last) >= U64'First + RFLX_Types.U64 (Cursors (F_Count).First)) to subprogram at line 780
  780 |   function Valid_Context (Buffer_First, Buffer_Last : RFLX_Types.Index; First : RFLX_Types.Bit_Index; Last : RFLX_Types.Bit_Length; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Len
gth; Buffer : RFLX_Types.Bytes_Ptr; Cursors : Field_Cursors) return Boolean is
      |            ^ here

rflx-test-message.ads:820:171: medium: overflow check might fail
  820 |                              and then RFLX_Types.U64 (Cursors (F_Length).Value) * 8 >= RFLX_Types.U64 (Cursors (F_Hash).Last) - RFLX_Types.U64 (Cursors (F_Count).First) + 17)))
      |                                                                                        ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~^~~~
  reason for check: result of addition must fit in a 64-bits machine integer
  possible fix: add precondition (RFLX_Types.U64 (Cursors (F_Hash).Last) - RFLX_Types.U64 (Cursors (F_Count).First) <= U64'Last - 17) to subprogram at line 780
  780 |   function Valid_Context (Buffer_First, Buffer_Last : RFLX_Types.Index; First : RFLX_Types.Bit_Index; Last : RFLX_Types.Bit_Length; Verified_Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Len
gth; Buffer : RFLX_Types.Bytes_Ptr; Cursors : Field_Cursors) return Boolean is
      |            ^ here

rflx-test-message.ads:905:83: medium: precondition might fail, cannot prove Available_Space (Ctx, Fld) >= Field_Size (Ctx, Fld)
  905 |             RFLX_Types.U64 (Ctx.Cursors (F_Length).Value) * 8 >= RFLX_Types.U64 (Field_Last (Ctx, F_Hash)) - RFLX_Types.U64 (Ctx.Cursors (F_Count).First) + 17,
      |                                                                                  ^~~~~~~~~~~~~~~~~~~~~~~

No failing checks occur, if the condition if 8 * Length >= 16 + (Hash'Last - Count'First + 1) is replaced by if 8 * Length >= 16 + 32 + 16 + 8. The problem seems to be that the field bounds Hash'Last and Count'First are not correctly inferred in those places. It is not yet clear to me why this is the case. The field bounds are encoded in the context predicate (in the message structure invariant part), but that seems not to be sufficient.

[treiher]

At least all overflow checks vanish when removing unnecessary type conversions to U64:

@@ -498,7 +498,7 @@
        and Structural_Valid (Ctx, F_Hash)
        and Invalid (Ctx, F_Structs)
        and (if
-               RFLX_Types.U64 (Get_Length (Ctx)) * 8 >= RFLX_Types.U64 (Field_Last (Ctx, F_Hash)) - RFLX_Types.U64 (Field_First (Ctx, F_Count)) + 17
+               RFLX_Types.Bit_Length (Get_Length (Ctx)) * 8 >= Field_Last (Ctx, F_Hash) - Field_First (Ctx, F_Count) + 17
             then
                Predecessor (Ctx, F_Structs) = F_Hash
                and Valid_Next (Ctx, F_Structs))
@@ -553,7 +553,7 @@
        and Structural_Valid (Ctx, F_Hash)
        and Invalid (Ctx, F_Structs)
        and (if
-               RFLX_Types.U64 (Get_Length (Ctx)) * 8 >= RFLX_Types.U64 (Field_Last (Ctx, F_Hash)) - RFLX_Types.U64 (Field_First (Ctx, F_Count)) + 17
+               RFLX_Types.Bit_Length (Get_Length (Ctx)) * 8 >= Field_Last (Ctx, F_Hash) - Field_First (Ctx, F_Count) + 17
             then
                Predecessor (Ctx, F_Structs) = F_Hash
                and Valid_Next (Ctx, F_Structs))
@@ -623,7 +623,7 @@
                Context_Cursors_Index (Context_Cursors (Ctx), F) = Context_Cursors_Index (Context_Cursors (Ctx)'Old, F)),
         others =>
            (if
-               RFLX_Types.U64 (Get_Length (Ctx)) * 8 >= RFLX_Types.U64 (Field_Last (Ctx, F_Hash)) - RFLX_Types.U64 (Field_First (Ctx, F_Count)) + 17
+               RFLX_Types.Bit_Length (Get_Length (Ctx)) * 8 >= Field_Last (Ctx, F_Hash) - Field_First (Ctx, F_Count) + 17
             then
                Predecessor (Ctx, F_Structs) = F_Hash
                and Valid_Next (Ctx, F_Structs))
@@ -817,7 +817,7 @@
                           then
                              (Structural_Valid (Cursors (F_Hash))
                               and then Cursors (F_Structs).Predecessor = F_Hash
-                              and then RFLX_Types.U64 (Cursors (F_Length).Value) * 8 >= RFLX_Types.U64 (Cursors (F_Hash).Last) - RFLX_Types.U64 (Cursors (F_Count).First) + 17)))
+                              and then RFLX_Types.Bit_Length (Cursors (F_Length).Value) * 8 >= Cursors (F_Hash).Last - Cursors (F_Count).First + 17)))
       and then ((if Invalid (Cursors (F_Count)) then Invalid (Cursors (F_Length)))
                 and then (if Invalid (Cursors (F_Length)) then Invalid (Cursors (F_Hash)))
                 and then (if Invalid (Cursors (F_Hash)) then Invalid (Cursors (F_Structs))))
@@ -841,7 +841,7 @@
                                              and then Cursors (F_Hash).First = Cursors (F_Length).Last + 1
                                              and then (if
                                                           Structural_Valid (Cursors (F_Structs))
-                                                          and then RFLX_Types.U64 (Cursors (F_Length).Value) * 8 >= RFLX_Types.U64 (Cursors (F_Hash).Last) - RFLX_Types.U64 (Cursors (F_Count).First) + 17
+                                                          and then RFLX_Types.Bit_Length (Cursors (F_Length).Value) * 8 >= Cursors (F_Hash).Last - Cursors (F_Count).First + 17
                                                        then
                                                           Cursors (F_Structs).Last - Cursors (F_Structs).First + 1 = RFLX_Types.Bit_Length (Cursors (F_Length).Value) * 8 - 16 + ((-RFLX_Types.Bit_Length (Cursors (F_Hash).Last)) + RFLX_Types.Bit_Length (Cursors (F_Count).First) - 1)
                                                           and then Cursors (F_Structs).Predecessor = F_Hash
@@ -895,14 +895,14 @@
           when F_Initial | F_Count | F_Length | F_Structs | F_Final =>
              True,
           when F_Hash =>
-             RFLX_Types.U64 (Ctx.Cursors (F_Length).Value) * 8 >= RFLX_Types.U64 (Ctx.Cursors (F_Hash).Last) - RFLX_Types.U64 (Ctx.Cursors (F_Count).First) + 17));
+             RFLX_Types.Bit_Length (Ctx.Cursors (F_Length).Value) * 8 >= Ctx.Cursors (F_Hash).Last - Ctx.Cursors (F_Count).First + 17));
 
    function Field_Condition (Ctx : Context; Fld : Field; Val : RFLX_Types.U64) return Boolean is
      ((case Fld is
           when F_Count | F_Length =>
              True,
           when F_Hash =>
-             RFLX_Types.U64 (Ctx.Cursors (F_Length).Value) * 8 >= RFLX_Types.U64 (Field_Last (Ctx, F_Hash)) - RFLX_Types.U64 (Ctx.Cursors (F_Count).First) + 17,
+             RFLX_Types.Bit_Length (Ctx.Cursors (F_Length).Value) * 8 >= Field_Last (Ctx, F_Hash) - Ctx.Cursors (F_Count).First + 17,
           when F_Structs =>
              True));

I also observed that SPARK is able to easily prove Field_Last (Ctx, F_Hash) > Field_First (Ctx, F_Count), but RFLX_Types.U64 (Field_Last (Ctx, F_Hash)) > RFLX_Types.U64 (Field_First (Ctx, F_Count)) was not provable even with a high timeout value. @kanigsson Is that expected? I don't see why the conversion to U64 should impact the validity of that expression.

There are still some unproved checks after that change:

rflx-test-message.adb:295:32: medium: postcondition might fail, cannot prove Path_Condition (Ctx, Fld)
  295 |                           and Valid_Next (Ctx, F_Structs)),
      |                               ^~~~~~~~~~~~~~~~~~~~~~~~~~
  in inlined expression function body at rflx-test-message.ads:954

rflx-test-message.ads:503:16: medium: postcondition might fail, cannot prove Predecessor (Ctx, F_Structs) = F_Hash
  503 |               Predecessor (Ctx, F_Structs) = F_Hash
      |               ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
  possible fix: call at rflx-test-message.adb:363 should mention Buffer (for argument Ctx) in a postcondition
  363 |      Test.My_Seq.Copy (Seq_Ctx, Ctx.Buffer.all (Buffer_First .. Buffer_Last));
      |                 ^ here

rflx-test-message.ads:624:16: medium: contract case might fail
  624 |        others =>
      |               ^ here

rflx-test-message.ads:905:74: medium: precondition might fail, cannot prove Available_Space (Ctx, Fld) >= Field_Size (Ctx, Fld)
  905 |             RFLX_Types.Bit_Length (Ctx.Cursors (F_Length).Value) * 8 >= Field_Last (Ctx, F_Hash) - Ctx.Cursors (F_Count).First + 17,
      |                                                                         ^~~~~~~~~~~~~~~~~~~~~~~

[kanigsson]

Indeed SPARK doesn't like mixing signed and unsigned arithmetic, and would rather stay in one or the other. That's something I discussed with Yannick last week, it could be generally beneficial to reduce the amount of signed integer types in generated code. I will try your patch.

[kanigsson]

I FINALLY made some progress on this ticket. As I said, SPARK doesn't like the mix of signed/unsigned computations which result from the fact that the data is unsigned (in U64), but computations happen in signed types. In particular cvc4 struggles with this and doesn't prove much on this code (z3 copes remarkably well). As an experiment, I replaced U64 by a kind of "S63" type, that is something like that:

type S63 is range 0 .. 2 ** 63 - 1;

and use it in the same way that we use U64 in the file for the repr message. This resulted in cvc4 proving almost all VCs immediately.
I realize this is the opposite of what I said in my previous message, that is, we try to eliminate unsigned instead of signed types.
This approach can't fully work as it doesn't interface well with Insert/Extract. But at least it seems that if we can go in this direction, we can expect some improvements. Let's discuss this on monday.

The one VC that's still unproved is this:

rflx-over-repr.ads:899:75: medium: precondition might fail, cannot prove Available_Space (Ctx, Fld) >= Field_Size (Ctx, Fld)
  899 |             RFLX_Types.Bit_Length (Ctx.Cursors (F_Length).Value) * 8 >= (Field_Last (Ctx, F_Hash)) - (Ctx.Cursors (F_Count).First) + 17,

cvc4 and z3 both return "unknown" immediately, which makes me think there is information missing. To be checked.

[treiher]

Glad you have made some progress. I'm wondering if it would be possible to let SPARK interpret the U64 as a mathematical integer instead of a bitvector. Maybe the default behavior of SPARK could be overridden by some annotation. The U64 is already annotated to have No_Wrap_Around semantics. Would it be possible to add such functionality or are there fundamental reasons not to do so?

[kanigsson]

It's possible (unsigned integers were mapped to mathematical integers before provers supported bitvectors), but it's quite ingrained in the tool and I expect it's difficult to add the functionality you describe. I wouldn't expect it in the short term.