SPARK : surprising failure with implication

SPARK : surprising failure with implication

[Yannick Duchêne (Hibou57)]

Hi all,

In an Ada/SPARK source, I had something like this:

    --# check (Source = 1) -> ((Source mod 2) = 1); -- (1)
    --# check (Source mod 2) /= 1;                  -- (2)
    --# check Source /= 1;                          -- (3)

1) Was proved by the simplifier (note that I needed a user rule for that).
2) Is a valid hypothesis ; an already proved conclusion (in some prior  
check clauses)
3) Failed to be proved, while I expected this to be proved from (1) and  
(2).


Naively, I had though Simplifier was not handling “(Source mod 2) /= 1” as  
an equivalent of “not ((Source mod 2) = 1)”, so I tried this:

    --# check (Source = 1) -> ((Source mod 2) = 1); -- (1)
    --# check not ((Source mod 2) = 1);             -- (2)
    --# check not (Source = 1);                     -- (3)


Hem, I'm not silly (or am I?), where “A -> B” is valid, then “not B -> not  
A” is valid too.

Whatever was going on, I wanted to be sure, so then tried the following:

    --# check (Source = 1) -> ((Source mod 2) = 1);             -- (1)
    --# check (not ((Source mod 2) = 1)) -> (not (Source = 1)); -- (1-bis)
    --# check not ((Source mod 2) = 1);                         -- (2)
    --# check not (Source = 1);                                 -- (3)

Simplifier failed on 1-bis. Ouch 8|


Do I become silly ?

I've looked in the *.SIV generated file, and it appears the simplifier  
automatically turns things of the form “not (A = B)” into “A /= B)” (i.e.  
“A <> B”, in an *.SIV file).

What I suspect: as Simplifier turns “not A = B” into “A /= B”, it cannot  
see it as the negation of the antecedent and consequent of the implication  
proved in (1), so from A -> B proved, I cannot prove not B -> not A, while  
logically speaking, I know “(A -> B) <-> (not B -> not A)”. But it still  
recognize “not ((Source mod 2) = 1)” as equivalent to “(Source mod 2) /=  
1”, so I'm not sure about the reason why it fails. Or may be it can see it  
as equivalent only when standalone and not in (1-bis) or against (1) ?


I was surprised to meet such an issue (unless I am missing some silly  
things because I would perhaps be too much tired).

Re: SPARK : surprising failure with implication

[Yannick Duchêne (Hibou57)]

Le Tue, 01 Jun 2010 20:51:04 +0200, Yannick Duchêne (Hibou57)  
<yannick_duchene@yahoo.fr> a écrit:

> Hi all,
>
> In an Ada/SPARK source, I had something like this:
>
>     --# check (Source = 1) -> ((Source mod 2) = 1); -- (1)
>     --# check (Source mod 2) /= 1;                  -- (2)
>     --# check Source /= 1;                          -- (3)
>
> 1) Was proved by the simplifier (note that I needed a user rule for  
> that).
> 2) Is a valid hypothesis ; an already proved conclusion (in some prior  
> check clauses)
> 3) Failed to be proved, while I expected this to be proved from (1) and  
> (2).
>
> [...]

Although late, I'm back to this topic.

I added this user rule:

    my_logic(1): not B -> not A may_be_deduced_from [ (A -> B) ].

While this was looking so much obvious, I though the Simplifier already  
knew it and this would probably change nothing. But this did change  
something! Now the above sequence of hypothesis->conclusion is proved.

Did I made something wrong somewhere ? Did I brake something somewhere ?  
Why is not this fundamental rule embedded in the Simplifier ?

I was so much surprised, that I checked it (yes, what looks obvious is  
sometimes good to check). Can't say anything else that “yes, this is true”.

(A) (B) (A->B)
  F   F    T
  F   T    T
  T   F    F
  T   T    T

(not B) (not A) (not B -> not A)
  T       T       T
  F       T       T
  T       F       F
  F       F       T

(A -> B) (not B -> not A) ((A -> B) -> (not B -> not A))
  T        T                T
  T        T                T
  F        F                T
  T        T                T

This is indeed tautology.

OK, that is solved, but I'm still somewhat frightened by what I don't  
understand in this experience : why did I need to add a user rule for that  
? What was wrong ?


-- 
There is even better than a pragma Assert: a SPARK --# check.
--# check C and WhoKnowWhat and YouKnowWho;
--# assert Ada;
--  i.e. forget about previous premises which leads to conclusion
--  and start with new conclusion as premise.

Re: SPARK : surprising failure with implication

[Dmitry A. Kazakov]

(forall A,B in Boolean)

not B => not A =
   = not not B or not A =
   = B or not A =
   = not A or B =
   = A => B

-- 
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de

Re: SPARK : surprising failure with implication

[Yannick Duchêne (Hibou57)]

Le Wed, 02 Jun 2010 09:42:58 +0200, Dmitry A. Kazakov  
<mailbox@dmitry-kazakov.de> a écrit:

> (forall A,B in Boolean)
>
> not B => not A =
>    = not not B or not A =
>    = B or not A =
>    = not A or B =
>    = A => B
>
Yes, you confirmed that is right and so I'm not silly. But why Simplifier  
do not seems to know it ? It is the basis of inference logic. That is why  
I have such a weighty question in my mind : I wonder if I did something  
wrong somewhere or if something is broken.

Do you have an idea ?

-- 
There is even better than a pragma Assert: a SPARK --# check.
--# check C and WhoKnowWhat and YouKnowWho;
--# assert Ada;
--  i.e. forget about previous premises which leads to conclusion
--  and start with new conclusion as premise.

Re: SPARK : surprising failure with implication

[Yannick Duchêne (Hibou57)]

Not exactly with implication this time, this is about equality and  
substitution.

Here is a case I am facing (simplified for the purpose of this message):

    --# assert S = (I / X);                -- (1)
    --# check S = T'Pos (S);               -- (2)
    --# check I = T'Pos (I);               -- (3)
    --# check T'Pos (S) = (T'Pos (I) / X); -- (4)

(1) is proved
(2) and (3) are proved
Simplifier fails to prove (4) despite of (1) and equalities (2) and (3)  
which should be used to substitute S and I in (1).

I still did not found a workaround for this one (I am busy at this now).

Does anyone already meet a case similar to this one ? Does it fails for  
the reason it requires two substitutions at a time ?

S and I are both of type same T (which is a modular type). Anyway, this  
should not be of any importance, as what is this about here, is that two  
equalities are not used for a substitution where it could expected to be.

It is not possible to use an intermediate step like...

    --# check S = (T'Pos (I) / X); -- (4.1)
    --# check T'Pos (S) = (T'Pos (I) / X); -- (4.2)

...because on (4.1), this would be an Universal_Integer expression on the  
right side with an expression of type T on the left side, which is not an  
allowed ; so there is no way to avoid the need for two substitutions at a  
time.

Re: SPARK : surprising failure with implication

[Dmitry A. Kazakov]

On Wed, 02 Jun 2010 09:56:23 +0200, Yannick Duch�ne (Hibou57) wrote:

> Le Wed, 02 Jun 2010 09:42:58 +0200, Dmitry A. Kazakov  
> <mailbox@dmitry-kazakov.de> a �crit:
> 
>> (forall A,B in Boolean)
>>
>> not B => not A =
>>    = not not B or not A =
>>    = B or not A =
>>    = not A or B =
>>    = A => B
>>
> Yes, you confirmed that is right and so I'm not silly. But why Simplifier  
> do not seems to know it ? It is the basis of inference logic.

Modus ponens is, but in the form:

A => B, A
--------------
B

You have rather unusual:

A => B, not B
--------------------
not A

Disproving the antecedent from wrong consequent is not very common.

> That is why  
> I have such a weighty question in my mind : I wonder if I did something  
> wrong somewhere or if something is broken.
> 
> Do you have an idea ?

None, except that what looks obvious for a man is not for a computer and
conversely. (:-))

-- 
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de

Re: SPARK : surprising failure with implication

[Yannick Duchêne (Hibou57)]

Le Wed, 02 Jun 2010 10:55:48 +0200, Dmitry A. Kazakov  
<mailbox@dmitry-kazakov.de> a écrit:
> Disproving the antecedent from wrong consequent is not very common.
It is to me, and not only with SPARK rules, this is why I though to use it  
in this context.

Thanks to have pointed this may not seems common to every one, as I was  
not aware of this.

> None, except that what looks obvious for a man is not for a computer and
> conversely. (:-))
You are right Dmitry ;) That is a nice sentence in all of its  
interpretations.


-- 
There is even better than a pragma Assert: a SPARK --# check.
--# check C and WhoKnowWhat and YouKnowWho;
--# assert Ada;
--  i.e. forget about previous premises which leads to conclusion
--  and start with new conclusion as premise.

Re: SPARK : surprising failure with implication

[Yannick Duchêne (Hibou57)]

Le Wed, 02 Jun 2010 10:50:55 +0200, Yannick Duchêne (Hibou57)  
<yannick_duchene@yahoo.fr> a écrit:

> Not exactly with implication this time, this is about equality and  
> substitution.
>
> Here is a case I am facing (simplified for the purpose of this message):
>
>     --# assert S = (I / X);                -- (1)
>     --# check S = T'Pos (S);               -- (2)
>     --# check I = T'Pos (I);               -- (3)
>     --# check T'Pos (S) = (T'Pos (I) / X); -- (4)
>
> (1) is proved
> (2) and (3) are proved
> Simplifier fails to prove (4) despite of (1) and equalities (2) and (3)  
> which should be used to substitute S and I in (1).
>
> I still did not found a workaround for this one (I am busy at this now).
>
> Does anyone already meet a case similar to this one ? Does it fails for  
> the reason it requires two substitutions at a time ?

A example which made me think about this one, while different. This time,  
there is only one substitution, and it still fails.

First, the case (extract from an *.SIV file):

    C1:    instance mod 2 ** (result + 1) * 2 ** (7 - result) * 2 mod 256 =
              instance mod 2 ** (result - 1 + 2) * 2 ** (7 - result) * 2  
mod 256 .

And its precursor as it appears in the *.VCG file:


    C1:    source * 2 mod instance_type__modulus = instance mod
               base ** (result - 1 + 2) * base ** (u__last - (
               result - 1 + 1)) * 2 mod base ** (u__last + 1) .

This conclusion could not be proved, because it fails to simplify (result  
- 1 + 2) into (result + 1), and I've checked it also fails to substitute  
(result - 1 + 2) to (result + 1). I have tried many thing, including a  
user rule like this one as my last attempt:

    my_test(1): A - 1 + 2 may_be_replaced_by [ A + 1 ].

As well as

    my_test(2): (A - 1) + 2 may_be_replaced_by [ A + 1 ].

Without success.

The original context in Ada/SPARK source is of the form (the above C1  
stands for the Check clause):

    --# assert ..... U'Pos (Result + 1) .....
    .....
    Result := Result + 1;
    .....
    --# check .... U'Pos (Result + 1 + 1) ....

I suspect it to see Result - 1, standing for the value of Result in the  
Assert clause (and thus as the actual expression standing for Result), as  
a monolithic subexpression. If this is really what happens, then it would  
not see (Result + 1 + 1) as (Result - 1 + 1 + 1), and instead as ((Result  
- 1) + 1 + 1), then see 1 + 1 as an expression, which is simplifies to 2,  
getting ((Result - 1) + 2), which it could not simplify any more, as it  
could not see -1 + 2 as a simplifiable expression, because -1 belongs to a  
subexpression.

However, what it strange, it that Result - 1 does not appears as a  
subexpression in neither the SIV file nor the VCG file. So I wonder if  
this is really the explanation of what's going on. Further more, the two  
attempt with above user rules, did not solve anything. Both simplification  
of a constant expression and substitution fails here.

Probably needs even more investigation.


-- 
There is even better than a pragma Assert: a SPARK --# check.
--# check C and WhoKnowWhat and YouKnowWho;
--# assert Ada;
--  i.e. forget about previous premises which leads to conclusion
--  and start with new conclusion as premise.

Re: SPARK : surprising failure with implication

[Yannick Duchêne (Hibou57)]

Le Thu, 03 Jun 2010 10:54:51 +0200, Yannick Duchêne (Hibou57)  
<yannick_duchene@yahoo.fr> a écrit:
> I suspect it to see Result - 1, standing for the value of Result in the  
> Assert clause (and thus as the actual expression standing for Result),  
> as a monolithic subexpression. If this is really what happens, then it  
> would not see (Result + 1 + 1) as (Result - 1 + 1 + 1), and instead as  
> ((Result - 1) + 1 + 1), then see 1 + 1 as an expression, which is  
> simplifies to 2, getting ((Result - 1) + 2), which it could not simplify  
> any more, as it could not see -1 + 2 as a simplifiable expression,  
> because -1 belongs to a subexpression.

Note for readers : if you are not aware of how SPARK and Simplifier works,  
reading “see (Result + 1 + 1) as (Result - 1 + 1 + 1)”, you may believe  
I'm crazy ;) So here is how you should understand it : in the first  
expression, Result stands for its actual value, in the line starting with  
“--# check”. If you read carefully, you may notice between the line  
starting with “--# assert” and the one starting with “--# check”, the is a  
line “Result := Result + 1”. So, the previous value of Result, in terms of  
its actual one, is “Result - 1”. In the proofs, SPARK sees Result as an  
expression which is equivalent to its actual value. This expression is  
relative the value of Result in the line starting with “--# assert”. So  
(Result + 1 + 1) is an expression in the terms of the actual value of  
Result, as the program see it would see, and (Result - 1 + 1 + 1) is the  
same expression as SPARK see it. You may also, for better understanding,  
read it as (previous-value-of-Result - 1 + 1 + 1).

Hope this note helped readers to understand the likely strange things they  
may feel to have read here ;)

-- 
There is even better than a pragma Assert: a SPARK --# check.
--# check C and WhoKnowWhat and YouKnowWho;
--# assert Ada;
--  i.e. forget about previous premises which leads to conclusion
--  and start with new conclusion as premise.

Re: SPARK : surprising failure with implication

[Yannick Duchêne (Hibou57)]

Le Thu, 03 Jun 2010 10:54:51 +0200, Yannick Duchêne (Hibou57)  
<yannick_duchene@yahoo.fr> a écrit:
> The original context in Ada/SPARK source is of the form (the above C1  
> stands for the Check clause):
>
>     --# assert ..... U'Pos (Result + 1) .....
>     .....
>     Result := Result + 1;
>     .....
>     --# check .... U'Pos (Result + 1 + 1) ....

If you meet a similar case as the above message, the only workable  
workaround seems to use an intermediate variable like in:

     --# assert ..... U'Pos (Result + 1) .....
     .....
     Previous_Result := Result;
     Result := Previous_Result - 1;
     .....
     --# check .... U'Pos (Previous_Result + 1) ....

I suppose some of you guessed this in an extract of a loop (the Check  
clause is the start of the proof of a loop invariant).

BTW, I've made a mistake in the previous transcription, this was “Result  
:= Result - 1;” (sorry for that)

I will not give other examples, I will just say using intermediate  
variables oftenly help with SPARK. But take care: while doing so, avoid to  
introduce additional RTC VC which will turn your proof into a more  
complicated story, and to avoid this misadventure, you should only use  
this technique to backup previous values of a variable which is modified  
since a previous Assert clause (a copy between two variables of the same  
type does not introduce RTC VC, so it's OK).

Have a nice day all.

-- 
There is even better than a pragma Assert: a SPARK --# check.
--# check C and WhoKnowWhat and YouKnowWho;
--# assert Ada;
--  i.e. forget about previous premises which leads to conclusion
--  and start with new conclusion as premise.

Re: SPARK : surprising failure with implication

[Yannick Duchêne (Hibou57)]

Le Wed, 02 Jun 2010 10:50:55 +0200, Yannick Duchêne (Hibou57)  
<yannick_duchene@yahoo.fr> a écrit:

I feel I have noticed a tip with substitution (people with knowledge in  
SPARK implementation may confirm perhaps).

As usual, to expect to have a substitution to be applied, it is needed to  
define an equality first

    check A = B;

The tip takes place when the expression in which you expect the  
substitution to be applied is itself an equality expression

    check (... C ...) = (... A ...); -- Suppose it is proved
    check (... C ...) = (... B ...); -- Seems to mostly fails

Then, it seems better to use an intermediate step and to do

    check (... C ...) = (... A ...); -- Suppose it is proved
    check (... A ....) = (... B ...); -- Suggest to apply the substitution  
to the RHS
    check (... C ...) = (... B ...); -- Use the modified RHS

-- 
There is even better than a pragma Assert: a SPARK --# check.
--# check C and WhoKnowWhat and YouKnowWho;
--# assert Ada;
--  i.e. forget about previous premises which leads to conclusion
--  and start with new conclusion as premise.