Fix encoding of primitive operators with refined domains

src/fstar/FStar.CheckedFiles.fst

@@ -36,7 +36,7 @@ let dbg = Debug.get_toggle "CheckedFiles"
  * detect when loading the cache that the version number is same
  * It needs to be kept in sync with prims.fst
  *)
-let cache_version_number = 68
+let cache_version_number = 69
 
 (*
  * Abbreviation for what we store in the checked files (stages as described below)

src/smtencoding/FStar.SMTEncoding.Encode.fst

@@ -89,7 +89,7 @@ let prims =
     let asym, a = fresh_fvar module_name "a" Term_sort in
     let xsym, x = fresh_fvar module_name "x" Term_sort in
     let ysym, y = fresh_fvar module_name "y" Term_sort in
-    let quant (rel:defn_rel_type) vars body : Range.range -> string -> term & int & list decl = fun rng x ->
+    let quant_with_pre (rel:defn_rel_type) vars precondition body : Range.range -> string -> term & int & list decl = fun rng x ->
         let xname_decl = Term.DeclFun(x, vars |> List.map fv_sort, Term_sort, None) in
         let xtok = x ^ "@tok" in
         let xtok_decl = Term.DeclFun(xtok, [], Term_sort, None) in
@@ -120,7 +120,12 @@ let prims =
           axioms
         in
 
-        let rel_body = (rel_type_f rel) (xapp, body) in
+        let rel_body =
+          let rel_body = (rel_type_f rel) (xapp, body) in
+          match precondition with
+          | None -> rel_body
+          | Some pre -> mkImp(pre, rel_body)
+        in
 
         xtok,
         List.length vars,
@@ -134,6 +139,7 @@ let prims =
                         Some "Name-token correspondence",
                         "token_correspondence_"^x)])
     in
+    let quant rel vars body = quant_with_pre rel vars None body in
     let axy = List.map mk_fv [(asym, Term_sort); (xsym, Term_sort); (ysym, Term_sort)] in
     let xy = List.map mk_fv [(xsym, Term_sort); (ysym, Term_sort)] in
     let qx = List.map mk_fv [(xsym, Term_sort)] in
@@ -154,8 +160,8 @@ let prims =
         (Const.op_Minus,       (quant Eq qx  (boxInt  <| mkMinus(unboxInt x))));
         (Const.op_Addition,    (quant Eq xy  (boxInt  <| mkAdd(unboxInt x, unboxInt y))));
         (Const.op_Multiply,    (quant Eq xy  (boxInt  <| mkMul(unboxInt x, unboxInt y))));
-        (Const.op_Division,    (quant Eq xy  (boxInt  <| mkDiv(unboxInt x, unboxInt y))));
-        (Const.op_Modulus,     (quant Eq xy  (boxInt  <| mkMod(unboxInt x, unboxInt y))));
+        (Const.op_Division,    (quant_with_pre Eq xy (Some (mkNot (mkEq (unboxInt y, mkInteger "0")))) (boxInt  <| mkDiv(unboxInt x, unboxInt y))));
+        (Const.op_Modulus,     (quant_with_pre Eq xy (Some (mkNot (mkEq (unboxInt y, mkInteger "0")))) (boxInt  <| mkMod(unboxInt x, unboxInt y))));
         //real ops
         (Const.real_op_LT,          (quant ValidIff xy  (mkLT(unboxReal x, unboxReal y))));
         (Const.real_op_LTE,         (quant ValidIff xy  (mkLTE(unboxReal x, unboxReal y))));
@@ -164,7 +170,7 @@ let prims =
         (Const.real_op_Subtraction, (quant Eq xy  (boxReal <| mkSub(unboxReal x, unboxReal y))));
         (Const.real_op_Addition,    (quant Eq xy  (boxReal <| mkAdd(unboxReal x, unboxReal y))));
         (Const.real_op_Multiply,    (quant Eq xy  (boxReal <| mkMul(unboxReal x, unboxReal y))));
-        (Const.real_op_Division,    (quant Eq xy  (boxReal <| mkRealDiv(unboxReal x, unboxReal y))));
+        (Const.real_op_Division,    (quant_with_pre Eq xy (Some (mkNot (mkEq (unboxReal y, mkReal "0")))) (boxReal <| mkRealDiv(unboxReal x, unboxReal y))));
         (Const.real_of_int,         (quant Eq qx  (boxReal <| mkRealOfInt (unboxInt x) Range.dummyRange)))
         ]
     in

tests/bug-reports/Bug3426.fst

@@ -0,0 +1,21 @@
+module Bug3426
+open FStar.Real
+let prim_arith_ty (p: unit): Type0 =
+  let () = p in
+  int -> int -> int
+
+[@@expect_failure]
+let prim_arith_sem (p: unit): (prim_arith_ty p) =
+  fun x y -> x / y
+
+[@@expect_failure]
+let prim_arith_sem_mod (p: unit): (prim_arith_ty p) =
+  fun x y -> x % y
+
+let prim_arith_ty_real (p: unit): Type0 =
+  let () = p in
+  real -> real -> real
+
+[@@expect_failure]
+let prim_arith_sem_real (p: unit): (prim_arith_ty_real p) =
+  fun x y -> x /. y

tests/bug-reports/Makefile

@@ -80,7 +80,7 @@ SHOULD_VERIFY_CLOSED=\
 	Bug2155.fst Bug3224a.fst Bug3224b.fst Bug3236.fst Bug3252.fst \
 	BugBoxInjectivity.fst BugTypeParamProjector.fst Bug2172.fst Bug3266.fst		\
 	Bug3264a.fst Bug3264b.fst Bug3286a.fst Bug3286b.fst Bug3320.fst Bug2583.fst \
-	Bug2419.fst Bug3353.fst
+	Bug2419.fst Bug3353.fst Bug3426.fst
 
 
 SHOULD_VERIFY_INTERFACE_CLOSED=Bug771.fsti Bug771b.fsti

ulib/FStar.UInt.fst

@@ -584,7 +584,7 @@ let lemma_lognot_value_zero #n a =
 private
 val lemma_mod_variation: #n:pos -> a:uint_t n ->
   Lemma (a <> 0 ==> ((-a) % pow2 n) - 1 % pow2 n = (((-a) % pow2 n) - 1) % pow2 n)
-let lemma_mod_variation #n a = ()
+let lemma_mod_variation #n a = assert (pow2 n =!= 0)
 #pop-options
 
 let lemma_one_mod_pow2 #n = ()

ulib/prims.fst

@@ -729,4 +729,4 @@ val string_of_int: int -> Tot string
 (** THIS IS MEANT TO BE KEPT IN SYNC WITH FStar.CheckedFiles.fs
     Incrementing this forces all .checked files to be invalidated *)
 irreducible
-let __cache_version_number__ = 68
+let __cache_version_number__ = 69