Lost in translation (with SPARK user rules)
in [ADA]
|
From: Yannick Duchêne (Hibou57) on 27 May 2010 04:13 Le Wed, 26 May 2010 12:57:11 +0200, Yannick Duchêne (Hibou57) <yannick_duchene(a)yahoo.fr> a écrit: >> If that is the conclusion left in the SIV file then the user rule to >> prove it is: >> user_bitwise(1): bit__and(X, 2) = 0 -> X div 2 mod 2 = 0 >> may_be_deduced . > I remember about this, this was just that I did not suspected this had > to be a so exact match. Finally, there is a work-around: if the Simplifier expect an expression which exactly match the one provided as a user rule, and there is not a direct matching expression in the source, then just use Simplifier's embedded rules to prove an expression is equivalent to the one the Simplifier expect an exact match. That is, if there a user rule of the form my_rule(1) Conclusion_1 may_be_deduced_from [Expression_1]. and the source unfortunately contains only Expression_2 then try something like --# check Expression_2 -> Intermediate_Expression(1); --# check ...; --# check ...; --# check Intermediate_Expression(N) -> Expression_1; and here it is. -- 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.
From: Yannick Duchêne (Hibou57) on 27 May 2010 06:55 Le Thu, 27 May 2010 10:13:55 +0200, Yannick Duchêne (Hibou57) <yannick_duchene(a)yahoo.fr> a écrit: > Finally, there is a work-around: if the Simplifier expect an expression > which exactly match the one provided as a user rule, and there is not a > direct matching expression in the source, then just use Simplifier's > embedded rules to prove an expression is equivalent to the one the > Simplifier expect an exact match. > > That is, if there a user rule of the form > > my_rule(1) Conclusion_1 may_be_deduced_from [Expression_1]. > > and the source unfortunately contains only > > Expression_2 > > then try something like > > --# check Expression_2 -> Intermediate_Expression(1); > --# check ...; > --# check ...; > --# check Intermediate_Expression(N) -> Expression_1; > > and here it is. > Unfortunately, I came into another trouble. I was trying this, and used intermediate variables to help. But Simplifier insist on using expressions instead of variables, so it can't find a match. An example will be more expressive: Here is an excerpt of a source (T is a modular type): ... --# check T'Pos (B) >= 0; -- Check #1 --# check T'Pos (B) <= 1; -- Check #2 --# check (T'Pos (B) = 0) or (T'Pos (B) = 1); -- Check #3 ... Here is a rule in a user rules file: my_rule(1): (X=0) or (X=1) may_be_deduced_from [ integer(X), X>=0, X<=1 ]. And Simplifier fails to prove Check #3 ; an excerpt of the *.SIV file shows why (conclusion associated to Check #3): C1: bit__and(v, 1) = 0 or bit__and(v, 1) = 1 . It replaces B with the source expression of the value of B and is thus unable to find a match with the rule. By the way, it drops Check #1 and Check #2, which does not appears at all in the hypotheses list (possibly it seems to much obvious to Simplifier). I've tried to use an Assert instead of a Check, this did not change anything. So if Simplifier requires an exact match to user rules, is there a way to avoid the simplifier to brake any attempt to prove an expression match a rule ? -- 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.
From: stefan-lucks on 27 May 2010 08:22 On Thu, 27 May 2010, Yannick Duch�ne (Hibou57) wrote: > Le Thu, 27 May 2010 10:13:55 +0200, Yannick Duch�ne (Hibou57) > <yannick_duchene(a)yahoo.fr> a �crit: > > > >That is, if there a user rule of the form > > > > my_rule(1) Conclusion_1 may_be_deduced_from [Expression_1]. > > > >and the source unfortunately contains only > > > > Expression_2 > > > >then try something like > > > > --# check Expression_2 -> Intermediate_Expression(1); > > --# check ...; > > --# check ...; > > --# check Intermediate_Expression(N) -> Expression_1; > > > >and here it is. > > Unfortunately, I came into another trouble. I was trying this, and used > intermediate variables to help. But Simplifier insist on using expressions > instead of variables, so it can't find a match. Wouldn't it be much simpler to use the proof checker, instead of the simplifier? Stefan -- ------ Stefan Lucks -- Bauhaus-University Weimar -- Germany ------ Stefan dot Lucks at uni minus weimar dot de ------ I love the taste of Cryptanalysis in the morning! ------
From: Yannick Duchêne (Hibou57) on 27 May 2010 07:32 Le Thu, 27 May 2010 12:55:04 +0200, Yannick Duchêne (Hibou57) <yannick_duchene(a)yahoo.fr> a écrit: > And Simplifier fails to prove Check #3 ; an excerpt of the *.SIV file > shows why (conclusion associated to Check #3): > > C1: bit__and(v, 1) = 0 or bit__and(v, 1) = 1 . Ok, found. I was not correct with the way to require the type to be integer as done in my_set(1): (X=0) or (X=1) may_be_deduced_from [ integer(X), X>=0, X<=1 ]. It has to be my_set(1): (X=0) or (X=1) may_be_deduced_from [ goal(checktype(X,integer)), X>=0, X<=1 ]. I've check that my_set(1): (X=0) or (X=1) may_be_deduced_from [ goal(integer(X)), X>=0, X<=1 ]. does not work, which lead to another question : what is the difference between the two predicates âinteger(X)â and âchecktype(X,integer)â ? The documentation is not clear to me about it. About âchecktype(EXPRESSION, TYPE_IDENTIFIER)â, it says âThis predicate may be used to check that an expression is of an appropriate typeâ and about âinteger(EXPRESSION)â is says This built-in Prolog predicate succeeds if and only if its argument is instantiated to an integer. So what's the difference between âgoal(integer(X))â and âgoal(checktype(X,integer))â. Does the latter refers to root type as defined in source and the other to something else ? (so what?) Another strange thing is that the file NUMINEQS.RUL does not contains any predicate stating arguments have to be integers and there is just a comment in heading, nothing in rules about it. -- 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.
From: Yannick Duchêne (Hibou57) on 27 May 2010 07:37
Le Thu, 27 May 2010 14:22:26 +0200, <stefan-lucks(a)see-the.signature> a écrit: > Wouldn't it be much simpler to use the proof checker, instead of the > simplifier? > > Stefan > I don't like the checker, this is an external tool (... and not an handy one), to me, SPARK is a language, not a tool. And further more, I really prefer to write proofs in source, because this is what I am expecting of such a thing as program proof is (I don't bother about adding a user rules file, although I would like a way to not need to copy it every where it is needed and have it to be loaded all time automatically). -- 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. |