Postcondition on a procedure doesn't prove even though the same condition is asserted and true at the end of procedure

Question

The code looks like this:

spec:

type Some_Record_Type is private;

procedure Deserialize_Record_Y(Record: in out Some_Record_Type)
with Post => (
    if Status_OK then (
        ...
        other postconditions
        ...
        and then
        Record_Field_X_Count(Record) = Record_Field_X_Count(Record'Old)
        and then
        Record_Field_X(Record) = Record_Field_X(Record'Old)
    )
);

function Record_Field_X(Record: Some_Record_Type) return X_Unbounded_Array_Type;
function Record_Field_X_Count(Record: Some_Record_Type) return Natural;

body:

type Some_Record_Type is
   record
      X_Count: Natural;
      X      : X_Bounded_Array_Type;
      Y_Count: Natural;
      Y      : Y_Bounded_Array_Type;
      ...
   end record;

function Record_Field_X(Record: Some_Record_Type) return X_Unbounded_Array_Type
is (
   ...
   a bit of logic based on values of other fields of Record
   ...
)

function Record_Field_X_Count(Record: Some_Record_Type) return Natural
is (Record.X_Count);

procedure Deserialize_Record_Y(Record: in out Some_Record_Type) is
    Old_Record: Some_Record_Type := Record with Ghost;
begin
    ...
    -- updates the Y field of the Record.
    -- Note that we annot pass Record.Y and have to pass
    -- the whole Record because Record is a private type
    -- and Deserialize_Record_Y is in public spec
    ...
    pragma Assert_And_Cut (
        Status_OK
        and then
        ...
        other postconditions
        ...
        and then
        Record_Field_X_Count(Record) = Record_Field_X_Count(Record_Old)
        and then
        Record_Field_X(Record) = Record_Field_X(Record_Old)
    )
end Deserialize_Record_Y;

There are no proof errors in the body, the error is only on the spec:

postcondition might fail, cannot prove Record_Field_X(Record) = Record_Field_X(Record'Old)

'other postconditions' are identical between the spec and the Assert_And_Cut at the end of the procedure.

Note the the checks with simpler fields, like X_Count:

Record_Field_X_Count(Record) = Record_Field_X_Count(Record'Old)

do not cause gnatprove to complain.

There's quite a lot of work for the prover inside the procedure, so usually, when there's a problem proving the postcondition it helps to assert that condition at the end of the procedure to 'remind' the prover that this is important facts. Usually, this works, but in one case it doesn't for some reason.

What are my options here?

What might be possible causes of this?

Maybe I should just increase the RAM on the machine where I run the proover, so it won't lose the Record_Field_X(Record) = Record_Field_X(Record_Old) fact between the end of the procedure and its postcondition? (I'm currently doing this on a machine with 32GB ram which is used exclusively to run gnatprove, with --memlimit=32000 --prover=cvc4,altergo --steps=0)

Maybe there are some techniques I don't know?

Maybe the only option I have is the manual proof?

I'm using the spark community 2019 version.

I actually doubt if the post condition can be proven at all. According to [SPARK RM 6.2](http://docs.adacore.com/spark2014-docs/html/lrm/subprograms.html#formal-parameter-modes), an `out` parameter is treated as to initially have no value and the `'Old` attribute should therefore not be used. — DeeDee, Feb 18 '20 at 11:03
Sorry, this is my error in transcribing the actual code into a small code fragment. In actual code it is `in out`, I'll amend the question text. Thanks for pointing this out! — Dmitry Petukhov, Feb 18 '20 at 11:06
I amended the code in the question to make it closer to the actual code — Dmitry Petukhov, Feb 18 '20 at 11:17
I just realized that I do not need the `Deserialize_Record_Y` procedure in the public part of the spec, and if I put it into the private part, I can make it accept just the `Record.Y` rather than the whole record. This will most likely remove the need to prove that other fields was not modified. But the original question still stands: in the case when I cannot move `Deserialize_Record_Y` into private spec, and I face the described problem, what is the best path to take to make it prove ? — Dmitry Petukhov, Feb 18 '20 at 11:25
Have you tried to decrease the memlimit to 1, 2 or 4 GB? We noticed that gnatprove sometimes takes more time if it has a higher memlimit. Also why are you omitting z3 from the provers? — jklmnn, Feb 18 '20 at 16:57
If I reduce the memlimit, I'm starting to get 'out of memory' messages from cvc4. And the issue is not that it it too long to wait - I can just leave it to run for the whole night. — Dmitry Petukhov, Feb 18 '20 at 18:22
regarding z3 - I noticed that adding it did not get any positive effect on the quality of the proof over my code (but it increases the time because 3 provers run in succession). I did not try to run z3 with this particular problem, I've ran it in earlier stages of the code. Maybe it is worth the shot to try z3 on this again. — Dmitry Petukhov, Feb 18 '20 at 18:25
another thing with reducing memlimit is that in addition to 'out of memory' errors, some other checks start to fail to prove (I presume because provers run out of memory to hold the state) — Dmitry Petukhov, Feb 18 '20 at 18:27
Adding z3 to provers actually helped. Thanks @jklmnn for the tip. I'm also glad that I asked this question and did not came to the idea of trying to add z3 again myself - otherwise I probably wouldn't notice that I do not need `Deserialize_Record_Y` in the public spec -- putting that in private spec makes things more simple. If you post an answer with a recomendation of adding z3, I will mark it as the accepted answer. — Dmitry Petukhov, Feb 19 '20 at 07:39
It would also be interesting to know the reason behind this problem, to be able to diagnose the same problems later. But it may be that the reason is too complex. — Dmitry Petukhov, Feb 19 '20 at 08:20
While hardly an expert, my experience is that there are often multiple ways to express a postcondition, and some ways are easier for the provers to prove than others. Also that my initial way of expressing a postcondition is usually one of the poor ways. — Jeffrey R. Carter, Feb 19 '20 at 10:32

score 5 · Accepted Answer · answered Feb 19 '20 at 10:08

5

To summarize the comments, adding z3 to the provers with

--prover=cvc4,altergo,z3

helped to solve the problem.

answered Feb 19 '20 at 10:08

jklmnn

481
1
5
11

Postcondition on a procedure doesn't prove even though the same condition is asserted and true at the end of procedure

1 Answers1