Hi, Le 15/10/2017 à 20:47, Julien Cretin a écrit : > Hi club, > > I updated my Why3 from 0.87.3 to 0.88.0 today and had a few issues with > my existing theories. I got some unbound symbol 'BVC.to_uint_small' > errors where BVC is an alias for bv.BVConverter_8_64. I suspect this to > be due to the new quote character syntax in identifiers. I have the same > issue with BV8.to_uint and BV64.to_uint which are also defined using > t'int. Consider the following theory (that I think used to work on 0.87.3): > > theory Bug > use bv.BV8 > lemma foo: BV8.to_uint BV8.zeros = 0 > end > > We now (with 0.88.0) get: > > File "bug.mlw", line 3, characters 13-23: > unbound symbol 'BV8.to_uint'
Indeed, there is an unexpected incompatible change in the bitvector theories. As you guessed, you need to replace each occurrence of to_uint with t'int. Similarly, max_int should be renamed to t'maxInt. Sorry for the inconvenience. > Also, now that I summoned the pros, would anyone know why I can't prove > the following lemmas? > > theory Cvc4 > use import mach.int.Int <http://mach.int.Int> > > use bv.BV8 > use bv.BV64 > use bv.BVConverter_8_64 as BVC > > lemma bv8_to_bv64_low: > forall x i. 0 <= i < 8 -> BV64.nth (BVC.toBig x) i = BV8.nth x i > > lemma bv8_to_bv64_high: > forall x i. 8 <= i < 64 -> BV64.nth (BVC.toBig x) i = false > end > > The second lemma (high) is actually proved by CVC4 1.5. But I can't > prove the first with my provers (Alt-Ergo 1.30, CVC4 1.5, and Z3 4.5.0) > and I can't see why it is false. I think that it is expected, indeed it is a bit of luck that the second lemma is proved by cvc4. The reason is that the nth function mixes bitvectors and integers: nth: BV.t -> int -> bool When a formula to prove is purely bit-vector, then provers that support bit-vectors are very good, but otherwise it is very difficuly to predict anything. Proving properties combining bit-vectors and integers is indeed an important issue addressed in the paper https://hal.inria.fr/hal-01314876 For your lemma, I suggest to use the same approach as the one we used in that paper: help the prover by giving an intermediate statement rephrased in terms of nth_bv instead of nth. nth_bv is the analogue of nth but the second argument is a bit-vector. Here is what I did, it is proved after splitting by using both CVC4 and Alt-Ergo : lemma bv8_to_bv64_low: forall x i. 0 <= i < 8 -> BV64.nth (BVC.toBig x) i = BV8.nth x i by forall i. BV64.nth_bv (BVC.toBig x) (BVC.toBig i) = BV8.nth_bv x i Hope this helps, - Claude -- Claude Marché | tel: +33 1 69 15 66 08 INRIA Saclay - Île-de-France | Université Paris-sud, Bat. 650 | http://www.lri.fr/~marche/ F-91405 ORSAY Cedex | _______________________________________________ Why3-club mailing list Why3-club@lists.gforge.inria.fr https://lists.gforge.inria.fr/mailman/listinfo/why3-club
