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
