On Tue, May 30, 2017 at 2:09 AM, Jean Karim Zinzindohoué < jean-karim.zinzindoh...@inria.fr> wrote:
> 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. > Ah, I had not realised that machine words were being handled as bitvectors and had assumed that I must have been doing something silly to prevent Z3 from applying its usual abilities. I think that, given your pointers to the lemmas, the issues that I raised can be fairly quickly resolved. Thank you. AGL
_______________________________________________ fstar-club mailing list fstar-club@lists.gforge.inria.fr https://lists.gforge.inria.fr/mailman/listinfo/fstar-club
