Hi Adam, There is certainly room for a lot of improvement regarding machine words.
In F* the machine words are not native, they are fully implemented in the F* standard library using F* mathematical integers (which are native to the language) and bitvectors ( https://github.com/FStarLang/FStar/blob/master/ulib/FStar.BitVector.fst) which are not native either and encoded as sequences of booleans. Therefore I think that there is no special treatment for machine words, they are encoded to Z3 as constructs over mathematical integers and sequences of booleans. The advantage is that we do not need to bake anything special into F*, the first two lemmas you mentioned are actually provable, they are variants at https://github.com/FStarLang/FStar/blob/master/ulib/FStar.UInt.fst#L437 and https://github.com/FStarLang/FStar/blob/master/ulib/FStar.UInt.fst#L458. The andLimit lemma is also provable, I think I have it somewhere, although it is not part of the standard library. We should definitely add it. The "trick" is to dive into the definitions of the F* machine words and do the proofs there. The machine words are in bijection with natural numbers smaller than 2^n and with bitvectors of n-bit in our encoding, so we can reflect on the arithmetic or bitwise properties of the F* machine words using those objects. It is not satisfying though, those libraries have not received a lot of attention and using FStar.BitVector in particular is not easy. I would be happy to add a set of missing lemmas such andLimit to the standard library. The major inconvenient of this general encoding is that it lowers the proof performance. The two aforementioned lemmas have no smt patterns attached to them to fire them automatically, if they had you could have proven those properties. I tend not to use smt patterns too much in order to make the proof less dependent on Z3 and thus faster and more robust, but it means calling the lemmas by hand and that may or may not scale very well. SMT patterns can perform very well in small proof contexts, and very poorly in larger developments. That said, I do not think that any extensive use of SMT patterns on machine words has been tried. So I think that there are three ways to improve the situation: 1) we have a much larger codebase than we used to, so we could try adding SMT patterns to the lemmas on bitwise operators and see if it causes any trouble with the regression tests 2) we could make a separate lemma file, fully instantiated with patterns, which the user could chose to include or not if 1) does not work too well 3) we could try specific SMT encodings for machine words, but that may increase the TCB. I wonder what Nikhil and the other developers involved in the F* SMT encoding feel about that. 1) and 2) are easy targets, I can look at it if you need. I hope this gives you a better feel on how things work and could be improved. Best, Jean-Karim Jean-Karim ZINZINDOHOUE 2017-05-30 1:51 GMT+02:00 Adam Langley via fstar-club < fstar-club@lists.gforge.inria.fr>: > Z3 is generally very good at finding properties of machine words, at least > with hand-written SMT2 using QF_BV. However, F* doesn't appear to be > encoding the FStar.UInt*.t types in a suitable way and so even trivial > properties fail to go through: > > val xorSelfZero: u:UInt32.t -> Lemma((u ^^ u) = 0ul) > let xorSelfZero u = () > > val andSelf: u:UInt32.t -> Lemma((u &^ u) = u) > let andSelf u = () (* fails *) > > val andLimit: u:UInt32.t -> mask:UInt32.t -> Lemma((u &^ mask) <=^ mask) > let andLimit u mask = () (* fails *) > > With shifts, one can make progress by relating the operation to division > and pow2 with nat, but bitwise-and/xor has no such analogue. > > I figure that there's probably some trick that I'm missing, however. > > > Cheers > > AGL > > > _______________________________________________ > fstar-club mailing list > fstar-club@lists.gforge.inria.fr > https://lists.gforge.inria.fr/mailman/listinfo/fstar-club > >
_______________________________________________ fstar-club mailing list fstar-club@lists.gforge.inria.fr https://lists.gforge.inria.fr/mailman/listinfo/fstar-club
