Assigning to Array Index Doesn't Guarantee Equality Check in Spark

General
1

I’m trying to make a simple stack-based (postfix) calculator with SPARK.

I’m assigning to the stack top when pushing, but it doesn’t seem to understand this assignment; I was trying to assert that a Peek function returned the value in the postcondition. I’ve simplified out all intermediate function checks down to this which still fails:

type Machine_Status is (Ok, Stack_Overflow, Stack_Underflow);

-- Stack definitions
Max_Stack_Size : constant := 1024;
type Element_Count is new Integer range 0 .. Max_Stack_Size;
subtype Stack_Index is Element_Count range 1 .. Max_Stack_Size;
type Value is new Interfaces.IEEE_Float_64;
type Machine_Stack is array (Stack_Index) of Value;

type Machine is record
    Status : Machine_Status := Ok;
    Stack  : Machine_Stack;
    Top    : Element_Count := 0;
end record;

procedure Push (Self : in out Machine; Element : Value)
with
  Global  => null,
  Depends => (Self => +Element),
  Pre     => Self.Status = Ok,
  Post    =>
    (Self.Status /= Ok
    or else (Self.Status = Ok
              and then Self.Top > 0
              and then Self.Top = Self'Old.Top + 1));

procedure Push (Self : in out Machine; Element : Value) is
begin
  if Self.Top = Max_Stack_Size then
      Self.Status := Stack_Overflow;
      return;
  end if;
  pragma Assert (Self.Top > 0);
  pragma Assert (Self.Status = Ok);
  Self.Top := Self.Top + 1;
  Self.Stack (Self.Top) := Element;
  pragma Assert (Self.Stack (Self.Top) = Element); --  FAILS !?
  pragma Assert (Self.Status = Ok);
  pragma Assert (Self.Top > 0);
end Push;

I’m confused why assigning a value and then checking that value is correct doesn’t work.

PS D:\dev\ada\postfix_calc> alr gnatprove --mode=all
Phase 1 of 3: generation of data representation information ...
Phase 2 of 3: generation of Global contracts ...
Phase 3 of 3: flow analysis and proof ...

machines.adb:16:22: medium: assertion might fail
   16 |      pragma Assert (Self.Stack (Self.Top) = Element);
      |                     ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
  possible fix: precondition of subprogram at machines.ads:54 should mention Element
   54 |   procedure Push (Self : in out Machine; Element : Value)
      |   ^ here

machines.ads:60:08: medium: postcondition might fail
   60>|       (Self.Status /= Ok
  ... | ...
   63 |                 and then Self.Top = Self'Old.Top + 1));
2

I think by default GNATprove uses a single prover, and the chosen prover might not be very good when reasoning about floating point numbers. Using --prover=all and/or a higher level (e.g. --level=2) may help here.

3 Likes
3

Thanks, both of these ideas work!

Looks like “max steps used for successful proof” goes from 1 to 684 with --level=2, but it still only uses CVC5.

“max steps used for successful proof” remains at 1 for --prover=all.

4

For the FSF version of SPARK, I think you have to do your own installation of additional provers.

5

That was true for some community editions of SPARK several years ago where they shipped with only one prover. But the recent FSF builds do have multiple provers. For example, GNATprove FSF 14 comes with altergo, colibri, cvc5, and z3.

4 Likes
6

Thanks, that’s good to know …