FStar.BV: use bv SMT encoding for bvshl and bvshl'

src/parser/FStar.Parser.Const.fst

@@ -213,11 +213,16 @@ let bv_xor_lid         = bvconst "bvxor"
 let bv_or_lid          = bvconst "bvor"
 let bv_add_lid         = bvconst "bvadd"
 let bv_sub_lid         = bvconst "bvsub"
-// bvshl and bvshr exist for backwards compatability and are implemented
-// in terms of bvshl' and bvshr'. We only need to handle bvshl' and bvshr'
-// specially.
-let bv_shift_left_lid  = bvconst "bvshl'"
-let bv_shift_right_lid = bvconst "bvshr'"
+let bv_shift_left_lid  = bvconst "bvshl"
+let bv_shift_right_lid = bvconst "bvshr"
+// bvshl and bvshr take a natural number for the shift, which incurs some
+// encoding overhead. The primed versions bvshl' and bvshr' take a bitvector,
+// which more closely matches SMT-LIB.
+// Although bvshl is implemented in terms of bvshl', removing the encoding for
+// bvshl breaks some proofs such as FStar.UInt128:lem_ult_1, so for backwards
+// compatibility, we'll translate both.
+let bv_shift_left'_lid = bvconst "bvshl'"
+let bv_shift_right'_lid= bvconst "bvshr'"
 let bv_udiv_lid        = bvconst "bvdiv"
 let bv_udiv_unsafe_lid = bvconst "bvdiv_unsafe"
 let bv_mod_lid         = bvconst "bvmod"

src/smtencoding/FStar.SMTEncoding.EncodeTerm.fst

@@ -530,6 +530,8 @@ and encode_arith_term env head args_e =
     let bv_sub  = mk_bv Util.mkBvSub binary (Term.boxBitVec sz) in
     let bv_shl  = mk_bv (Util.mkBvShl sz) binary_arith (Term.boxBitVec sz) in
     let bv_shr  = mk_bv (Util.mkBvShr sz) binary_arith (Term.boxBitVec sz) in
+    let bv_shl' = mk_bv (Util.mkBvShl' sz) binary_arith (Term.boxBitVec sz) in
+    let bv_shr' = mk_bv (Util.mkBvShr' sz) binary_arith (Term.boxBitVec sz) in
     let bv_udiv = mk_bv (Util.mkBvUdiv sz) binary_arith (Term.boxBitVec sz) in
     let bv_mod  = mk_bv (Util.mkBvMod sz) binary_arith (Term.boxBitVec sz) in
     let bv_mul  = mk_bv (Util.mkBvMul sz) binary_arith (Term.boxBitVec sz) in
@@ -547,6 +549,8 @@ and encode_arith_term env head args_e =
          (Const.bv_sub_lid, bv_sub);
          (Const.bv_shift_left_lid, bv_shl);
          (Const.bv_shift_right_lid, bv_shr);
+         (Const.bv_shift_left'_lid, bv_shl');
+         (Const.bv_shift_right'_lid, bv_shr');
          (Const.bv_udiv_lid, bv_udiv);
          (Const.bv_mod_lid, bv_mod);
          (* NOTE: unsafe 'udiv' and 'mod' variants also compile to the same smtlib2 expr *)

src/smtencoding/FStar.SMTEncoding.Term.fst

@@ -308,6 +308,8 @@ let mkBvAdd = mk_bin_op BvAdd
 let mkBvSub = mk_bin_op BvSub
 let mkBvShl sz (t1, t2) r = mkApp'(BvShl, [t1;(mkNatToBv sz t2 r)]) r
 let mkBvShr sz (t1, t2) r = mkApp'(BvShr, [t1;(mkNatToBv sz t2 r)]) r
+let mkBvShl' sz (t1, t2) r = mkApp'(BvShl, [t1;t2]) r
+let mkBvShr' sz (t1, t2) r = mkApp'(BvShr, [t1;t2]) r
 let mkBvUdiv sz (t1, t2) r = mkApp'(BvUdiv, [t1;(mkNatToBv sz t2 r)]) r
 let mkBvMod sz (t1, t2) r = mkApp'(BvMod, [t1;(mkNatToBv sz t2 r)]) r
 let mkBvMul sz (t1, t2) r = mkApp' (BvMul, [t1;(mkNatToBv sz t2 r)]) r

src/smtencoding/FStar.SMTEncoding.Term.fsti

@@ -246,6 +246,8 @@ val mkBvUlt   : ((term * term) -> Range.range -> term)
 val mkBvUext  : (int -> term -> Range.range -> term)
 val mkBvShl   : (int -> (term * term) -> Range.range -> term)
 val mkBvShr   : (int -> (term * term) -> Range.range -> term)
+val mkBvShl'  : (int -> (term * term) -> Range.range -> term)
+val mkBvShr'  : (int -> (term * term) -> Range.range -> term)
 val mkBvUdiv  : (int -> (term * term) -> Range.range -> term)
 val mkBvMod   : (int -> (term * term) -> Range.range -> term)
 val mkBvMul   : (int -> (term * term) -> Range.range -> term)

src/smtencoding/FStar.SMTEncoding.Util.fst

@@ -76,6 +76,8 @@ let mkBvAdd = norng mkBvAdd
 let mkBvSub = norng mkBvSub
 let mkBvShl sz = norng (mkBvShl sz)
 let mkBvShr sz = norng (mkBvShr sz)
+let mkBvShl' sz = norng (mkBvShl' sz)
+let mkBvShr' sz = norng (mkBvShr' sz)
 let mkBvUdiv sz = norng (mkBvUdiv sz)
 let mkBvMod sz = norng (mkBvMod sz)
 let mkBvMul sz = norng (mkBvMul sz)