Re: Lost in translation (with SPARK user rules)

[Phil Thornley <phil.jpthornley@googlemail.com>]

On 30 May, 00:03, Yannick Duchêne (Hibou57) <yannick_duch...@yahoo.fr>
wrote:
> In this area, the Simplifier sometimes shows slight capacities to be  
> boring.
>
> Let a Check clause be “--# check ((2 ** Count) < (2 ** 8)) -> (Count < 8);”
> Let a user rule be “my_rule: ((X ** Y) < (X ** Z)) -> (Y < Z)  
> may_be_deduced_from [some-obvious-conditions].”
>
> There should be an exact match, isn't it ?
>
> Well, I guess you guess: it fails to prove the Check clause. Now, if you  
> would like to know why, here is: it replaces this by “2 ** count < 256 ->  
> count < 8”, ... it turns “(2 ** 8)” into “256”, so that it can't see any  
> more an exact match with the user rule
>
> I've check in the *.SLG file, this is indeed due to simplification, this  
> is not due to an hypothetical related error.

The full description of all the simplification steps is in section 3
of the Simplifier User Manual, so if you read this and follow through
the steps in a simplification log file then you should get a better
understanding of how the tool works - and so how to write user rules
that are effective.

Application of user rules is the final step (out of about a dozen)
that the Simplifier uses, so at that point a conclusion is likely to
have been changed from the form of the annotation that generated it.

In the case you describe here Count must be defined as a constant with
value 8, and that replacement is the first step that the Simplifier
takes.  Then it will convert 2**8 to 256 in a subsequent step. (A
basic strategy of the Simplifier is to replace any expressions with a
simpler version wherever possible - perhaps that's why it called the
Simplifier rather than the 'Prover' :-).

Section 3.12 describes how the Simplifier uses user rules - and it is
clear from this description that the rule needs to match expressions
in the VC as they are at the end of the process, not as in the
original VC.

You can see why this is sensible (even if it has some drawbacks*).
Generally the way that a user rule is written is in response to an
unproven conclusion in a simplified VC, so the author of the rule uses
the final form of the unproven VC to write the rule. Therefore the
rule can only be reliably applied at the point where the VC has
reached its final form.

I guess it might be possible for the Simplifier to try all the user
rules at each stage of the process - but the developers of the tool
have been concentrating heavily on making simplification as quick as
possible (quite rightly in my view) and would not want to do anything
that might slow it down without a very strong argument for the
advantages of doing that.

* The main drawback that I see is that some user rules define
replacements that must be made for the VC to be provable, but at
present these are made too late for them to be effective, since the
Simplifier has already exhausted all its other strategies.
It would be nice to have replacements defined in user rules applied in
the first simplification stage, how about:
my_rewrite(1): A must_be_replaced_by B if [...] .

(Of course nothing is ever simple, for example what happens if one
rewrite rule requires another to be applied before its sideconditions
are satisfied - are all such rules tried repeatedly until none are
used, or is it a once-only pass? etc...)

Cheers,

Phil