removing checks on bounded integer constants

src/basic/FStar.Const.fs

@@ -43,3 +43,28 @@ let eq_const c1 c2 =
     | Const_string(a, _), Const_string(b, _) -> a=b
     | Const_reflect l1, Const_reflect l2 -> Ident.lid_equals l1 l2
     | _ -> c1=c2
+
+open FStar.Mul
+let rec pow2 (x:int) : int =
+  match x with
+  | 0  -> 1
+  | _  -> Prims.op_Multiply 2 (pow2 (x-1))
+
+
+let bounds signedness width =
+    let n =
+        match width with
+        | Int8 -> 8
+        | Int16 -> 16
+        | Int32 -> 32
+        | Int64 -> 64
+    in
+    let lower, upper =
+      match signedness with
+      | Unsigned ->
+        0, pow2 n - 1
+      | Signed ->
+        let upper = pow2 (n - 1) in
+        - upper, upper - 1
+    in
+    lower, upper

src/ocaml-output/FStar_Const.ml

@@ -95,4 +95,30 @@ let eq_const: sconst -> sconst -> Prims.bool =
       | (Const_bytearray (a,_),Const_bytearray (b,_))
         |(Const_string (a,_),Const_string (b,_)) -> a = b
       | (Const_reflect l1,Const_reflect l2) -> FStar_Ident.lid_equals l1 l2
-      | uu____256 -> c1 = c2
+      | uu____256 -> c1 = c2
+let rec pow2: Prims.int -> Prims.int =
+  fun x  ->
+    match x with
+    | _0_25 when _0_25 = (Prims.parse_int "0") -> Prims.parse_int "1"
+    | uu____262 ->
+        let uu____263 = pow2 (x - (Prims.parse_int "1")) in
+        (Prims.parse_int "2") * uu____263
+let bounds: signedness -> width -> (Prims.int* Prims.int) =
+  fun signedness  ->
+    fun width  ->
+      let n1 =
+        match width with
+        | Int8  -> Prims.parse_int "8"
+        | Int16  -> Prims.parse_int "16"
+        | Int32  -> Prims.parse_int "32"
+        | Int64  -> Prims.parse_int "64" in
+      let uu____273 =
+        match signedness with
+        | Unsigned  ->
+            let uu____278 =
+              let uu____279 = pow2 n1 in uu____279 - (Prims.parse_int "1") in
+            ((Prims.parse_int "0"), uu____278)
+        | Signed  ->
+            let upper = pow2 (n1 - (Prims.parse_int "1")) in
+            ((- upper), (upper - (Prims.parse_int "1"))) in
+      match uu____273 with | (lower,upper) -> (lower, upper)

src/ocaml-output/FStar_Extraction_ML_Syntax.ml

@@ -100,7 +100,7 @@ let reset_gensym: Prims.unit -> Prims.unit = fun uu____85  -> gs.reset ()
 let rec gensyms: Prims.int -> mlident Prims.list =
   fun x  ->
     match x with
-    | _0_28 when _0_28 = (Prims.parse_int "0") -> []
+    | _0_29 when _0_29 = (Prims.parse_int "0") -> []
     | n1 ->
         let uu____92 = gensym () in
         let uu____93 = gensyms (n1 - (Prims.parse_int "1")) in uu____92 ::

src/ocaml-output/FStar_Extraction_ML_Term.ml

@@ -810,8 +810,8 @@ let rec extract_one_pat:
                                 FStar_Extraction_ML_Util.mlconst_of_const'
                                   p.FStar_Syntax_Syntax.p i in
                               FStar_All.pipe_left
-                                (fun _0_30  ->
-                                   FStar_Extraction_ML_Syntax.MLE_Const _0_30)
+                                (fun _0_31  ->
+                                   FStar_Extraction_ML_Syntax.MLE_Const _0_31)
                                 uu____1822 in
                             FStar_All.pipe_left
                               (FStar_Extraction_ML_Syntax.with_ty
@@ -1366,8 +1366,8 @@ and term_as_mlexpr':
                       FStar_Extraction_ML_Util.mlconst_of_const'
                         t.FStar_Syntax_Syntax.pos c in
                     FStar_All.pipe_left
-                      (fun _0_31  ->
-                         FStar_Extraction_ML_Syntax.MLE_Const _0_31)
+                      (fun _0_32  ->
+                         FStar_Extraction_ML_Syntax.MLE_Const _0_32)
                       uu____3397 in
                   FStar_Extraction_ML_Syntax.with_ty ml_ty uu____3396 in
                 (uu____3395, FStar_Extraction_ML_Syntax.E_PURE, ml_ty))

src/ocaml-output/FStar_Extraction_ML_Util.ml

@@ -251,7 +251,7 @@ let rec type_leq_c:
                         (let uu____361 =
                            let uu____365 =
                              let uu____367 = mk_fun xs body in
-                             FStar_All.pipe_left (fun _0_29  -> Some _0_29)
+                             FStar_All.pipe_left (fun _0_30  -> Some _0_30)
                                uu____367 in
                            type_leq_c unfold_ty uu____365 t2 t2' in
                          match uu____361 with

src/ocaml-output/FStar_Interactive.ml

@@ -778,18 +778,18 @@ let json_of_lookup_result: lookup_result -> FStar_Util.json =
         let uu____1776 =
           let uu____1780 =
             let uu____1783 =
-              json_of_opt (fun _0_32  -> FStar_Util.JsonStr _0_32) lr.lr_typ in
+              json_of_opt (fun _0_33  -> FStar_Util.JsonStr _0_33) lr.lr_typ in
             ("type", uu____1783) in
           let uu____1784 =
             let uu____1788 =
               let uu____1791 =
-                json_of_opt (fun _0_33  -> FStar_Util.JsonStr _0_33)
+                json_of_opt (fun _0_34  -> FStar_Util.JsonStr _0_34)
                   lr.lr_doc in
               ("documentation", uu____1791) in
             let uu____1792 =
               let uu____1796 =
                 let uu____1799 =
-                  json_of_opt (fun _0_34  -> FStar_Util.JsonStr _0_34)
+                  json_of_opt (fun _0_35  -> FStar_Util.JsonStr _0_35)
                     lr.lr_def in
                 ("definition", uu____1799) in
               [uu____1796] in
@@ -802,9 +802,9 @@ let json_of_protocol_info: (Prims.string* FStar_Util.json) Prims.list =
   let js_version = FStar_Util.JsonInt interactive_protocol_vernum in
   let js_features =
     let uu____1817 =
-      FStar_List.map (fun _0_35  -> FStar_Util.JsonStr _0_35)
+      FStar_List.map (fun _0_36  -> FStar_Util.JsonStr _0_36)
         interactive_protocol_features in
-    FStar_All.pipe_left (fun _0_36  -> FStar_Util.JsonList _0_36) uu____1817 in
+    FStar_All.pipe_left (fun _0_37  -> FStar_Util.JsonList _0_37) uu____1817 in
   [("version", js_version); ("features", js_features)]
 let write_json: FStar_Util.json -> Prims.unit =
   fun json  ->
@@ -841,7 +841,7 @@ let write_hello: Prims.unit -> Prims.unit =
     let js_version = FStar_Util.JsonInt interactive_protocol_vernum in
     let js_features =
       let uu____1871 =
-        FStar_List.map (fun _0_37  -> FStar_Util.JsonStr _0_37)
+        FStar_List.map (fun _0_38  -> FStar_Util.JsonStr _0_38)
           interactive_protocol_features in
       FStar_Util.JsonList uu____1871 in
     write_json
@@ -903,7 +903,7 @@ let json_of_repl_state:
                              let uu____2054 =
                                let uu____2057 =
                                  json_of_opt
-                                   (fun _0_38  -> FStar_Util.JsonStr _0_38)
+                                   (fun _0_39  -> FStar_Util.JsonStr _0_39)
                                    doc1 in
                                ("documentation", uu____2057) in
                              [uu____2054] in
@@ -1261,7 +1261,7 @@ let run_completions st search_term =
                  match (uu____3276, uu____3277) with
                  | ((cd1,ns1,uu____3292),(cd2,ns2,uu____3295)) ->
                      (match FStar_String.compare cd1 cd2 with
-                      | _0_39 when _0_39 = (Prims.parse_int "0") ->
+                      | _0_40 when _0_40 = (Prims.parse_int "0") ->
                           FStar_String.compare ns1 ns2
                       | n1 -> n1)) matches in
         FStar_List.map

src/ocaml-output/FStar_Legacy_Interactive.ml

@@ -776,7 +776,7 @@ let rec go:
                              match (uu____2153, uu____2154) with
                              | ((cd1,ns1,uu____2169),(cd2,ns2,uu____2172)) ->
                                  (match FStar_String.compare cd1 cd2 with
-                                  | _0_40 when _0_40 = (Prims.parse_int "0")
+                                  | _0_41 when _0_41 = (Prims.parse_int "0")
                                       -> FStar_String.compare ns1 ns2
                                   | n1 -> n1)) matches in
                     FStar_List.iter

src/ocaml-output/FStar_Options.ml

@@ -488,7 +488,7 @@ let cons_extract_module: Prims.string -> option_val =
         let uu____989 = get_extract_module () in (FStar_String.lowercase s)
           :: uu____989 in
       FStar_All.pipe_right uu____987
-        (FStar_List.map (fun _0_25  -> String _0_25)) in
+        (FStar_List.map (fun _0_26  -> String _0_26)) in
     List uu____985
 let cons_extract_namespace: Prims.string -> option_val =
   fun s  ->
@@ -497,7 +497,7 @@ let cons_extract_namespace: Prims.string -> option_val =
         let uu____1000 = get_extract_namespace () in
         (FStar_String.lowercase s) :: uu____1000 in
       FStar_All.pipe_right uu____998
-        (FStar_List.map (fun _0_26  -> String _0_26)) in
+        (FStar_List.map (fun _0_27  -> String _0_27)) in
     List uu____996
 let add_extract_module: Prims.string -> Prims.unit =
   fun s  ->
@@ -514,7 +514,7 @@ let cons_verify_module: Prims.string -> option_val =
         let uu____1019 = get_verify_module () in (FStar_String.lowercase s)
           :: uu____1019 in
       FStar_All.pipe_right uu____1017
-        (FStar_List.map (fun _0_27  -> String _0_27)) in
+        (FStar_List.map (fun _0_28  -> String _0_28)) in
     List uu____1015
 let cons_using_facts_from: Prims.string -> option_val =
   fun s  ->
@@ -524,7 +524,7 @@ let cons_using_facts_from: Prims.string -> option_val =
      | None  -> List [String s]
      | Some l ->
          let uu____1034 =
-           FStar_List.map (fun _0_28  -> String _0_28) (s :: l) in
+           FStar_List.map (fun _0_29  -> String _0_29) (s :: l) in
          List uu____1034)
 let add_verify_module: Prims.string -> Prims.unit =
   fun s  ->
@@ -559,7 +559,7 @@ let rec specs:
                   let uu____1092 =
                     let uu____1094 = get_codegen_lib () in s :: uu____1094 in
                   FStar_All.pipe_right uu____1092
-                    (FStar_List.map (fun _0_29  -> String _0_29)) in
+                    (FStar_List.map (fun _0_30  -> String _0_30)) in
                 List uu____1090)), "[namespace]")),
         "External runtime library (i.e. M.N.x extracts to M.N.X instead of M_N.x)");
       (FStar_Getopt.noshort, "debug",
@@ -569,7 +569,7 @@ let rec specs:
                   let uu____1109 =
                     let uu____1111 = get_debug () in x :: uu____1111 in
                   FStar_All.pipe_right uu____1109
-                    (FStar_List.map (fun _0_30  -> String _0_30)) in
+                    (FStar_List.map (fun _0_31  -> String _0_31)) in
                 List uu____1107)), "[module name]")),
         "Print lots of debugging information while checking module");
       (FStar_Getopt.noshort, "debug_level",
@@ -579,7 +579,7 @@ let rec specs:
                   let uu____1126 =
                     let uu____1128 = get_debug_level () in x :: uu____1128 in
                   FStar_All.pipe_right uu____1126
-                    (FStar_List.map (fun _0_31  -> String _0_31)) in
+                    (FStar_List.map (fun _0_32  -> String _0_32)) in
                 List uu____1124)), "[Low|Medium|High|Extreme|...]")),
         "Control the verbosity of debugging info");
       (FStar_Getopt.noshort, "dep",
@@ -602,8 +602,8 @@ let rec specs:
                   let uu____1167 =
                     let uu____1169 = get_dump_module () in x :: uu____1169 in
                   FStar_All.pipe_right uu____1167
-                    (FStar_List.map (fun _0_32  -> String _0_32)) in
-                FStar_All.pipe_right uu____1165 (fun _0_33  -> List _0_33))),
+                    (FStar_List.map (fun _0_33  -> String _0_33)) in
+                FStar_All.pipe_right uu____1165 (fun _0_34  -> List _0_34))),
              "[module name]")), "");
       (FStar_Getopt.noshort, "eager_inference",
         (FStar_Getopt.ZeroArgs ((fun uu____1180  -> Bool true))),
@@ -621,7 +621,7 @@ let rec specs:
         (FStar_Getopt.OneArg (cons_extract_namespace, "[namespace name]")),
         "Only extract modules in the specified namespace");
       (FStar_Getopt.noshort, "fstar_home",
-        (FStar_Getopt.OneArg (((fun _0_34  -> Path _0_34)), "[dir]")),
+        (FStar_Getopt.OneArg (((fun _0_35  -> Path _0_35)), "[dir]")),
         "Set the FSTAR_HOME variable to [dir]");
       (FStar_Getopt.noshort, "hide_genident_nums",
         (FStar_Getopt.ZeroArgs ((fun uu____1225  -> Bool true))),
@@ -644,7 +644,7 @@ let rec specs:
                 let uu____1263 =
                   let uu____1265 =
                     let uu____1267 = get_include () in
-                    FStar_List.map (fun _0_35  -> String _0_35) uu____1267 in
+                    FStar_List.map (fun _0_36  -> String _0_36) uu____1267 in
                   FStar_List.append uu____1265 [Path s] in
                 List uu____1263)), "[path]")),
         "A directory in which to search for files included on the command line");
@@ -712,7 +712,7 @@ let rec specs:
                   let uu____1389 =
                     let uu____1391 = get_no_extract () in x :: uu____1391 in
                   FStar_All.pipe_right uu____1389
-                    (FStar_List.map (fun _0_36  -> String _0_36)) in
+                    (FStar_List.map (fun _0_37  -> String _0_37)) in
                 List uu____1387)), "[module name]")),
         "Do not extract code from this module");
       (FStar_Getopt.noshort, "no_location_info",
@@ -723,7 +723,7 @@ let rec specs:
            (((fun p  -> let uu____1411 = validate_dir p in Path uu____1411)),
              "[dir]")), "Place output in directory [dir]");
       (FStar_Getopt.noshort, "prims",
-        (FStar_Getopt.OneArg (((fun _0_37  -> String _0_37)), "file")), "");
+        (FStar_Getopt.OneArg (((fun _0_38  -> String _0_38)), "file")), "");
       (FStar_Getopt.noshort, "print_before_norm",
         (FStar_Getopt.ZeroArgs ((fun uu____1426  -> Bool true))),
         "Do not normalize types before printing (for debugging)");
@@ -759,7 +759,7 @@ let rec specs:
         "Check new hints for replayability");
       (FStar_Getopt.noshort, "reuse_hint_for",
         (FStar_Getopt.OneArg
-           (((fun _0_38  -> String _0_38)),
+           (((fun _0_39  -> String _0_39)),
              "top-level name in the current module")),
         "Optimistically, attempt using the recorded hint for 'f' when trying to verify some other term 'g'");
       (FStar_Getopt.noshort, "show_signatures",
@@ -770,13 +770,13 @@ let rec specs:
                     let uu____1518 = get_show_signatures () in x ::
                       uu____1518 in
                   FStar_All.pipe_right uu____1516
-                    (FStar_List.map (fun _0_39  -> String _0_39)) in
+                    (FStar_List.map (fun _0_40  -> String _0_40)) in
                 List uu____1514)), "[module name]")),
         "Show the checked signatures for all top-level symbols in the module");
       (FStar_Getopt.noshort, "silent",
         (FStar_Getopt.ZeroArgs ((fun uu____1528  -> Bool true))), " ");
       (FStar_Getopt.noshort, "smt",
-        (FStar_Getopt.OneArg (((fun _0_40  -> Path _0_40)), "[path]")),
+        (FStar_Getopt.OneArg (((fun _0_41  -> Path _0_41)), "[path]")),
         "Path to the SMT solver (usually Z3, but could be any SMT2-compatible solver)");
       (FStar_Getopt.noshort, "split_cases",
         (FStar_Getopt.OneArg
@@ -821,7 +821,7 @@ let rec specs:
                   let uu____1630 =
                     let uu____1632 = get___temp_no_proj () in x :: uu____1632 in
                   FStar_All.pipe_right uu____1630
-                    (FStar_List.map (fun _0_41  -> String _0_41)) in
+                    (FStar_List.map (fun _0_42  -> String _0_42)) in
                 List uu____1628)), "[module name]")),
         "Don't generate projectors for this module");
       ('v', "version",
@@ -840,7 +840,7 @@ let rec specs:
                     let uu____1664 = get_z3cliopt () in
                     FStar_List.append uu____1664 [s] in
                   FStar_All.pipe_right uu____1662
-                    (FStar_List.map (fun _0_42  -> String _0_42)) in
+                    (FStar_List.map (fun _0_43  -> String _0_43)) in
                 List uu____1660)), "[option]")), "Z3 command line options");
       (FStar_Getopt.noshort, "z3refresh",
         (FStar_Getopt.ZeroArgs ((fun uu____1674  -> Bool true))),
@@ -1021,7 +1021,7 @@ let restore_cmd_line_options: Prims.bool -> FStar_Getopt.parse_cmdline_res =
      (let uu____1966 =
         let uu____1969 =
           let uu____1970 =
-            FStar_List.map (fun _0_43  -> String _0_43) old_verify_module in
+            FStar_List.map (fun _0_44  -> String _0_44) old_verify_module in
           List uu____1970 in
         ("verify_module", uu____1969) in
       set_option' uu____1966);

src/ocaml-output/FStar_Parser_Lexhelp.ml

@@ -8,7 +8,7 @@ let intern_string: Prims.string -> Prims.string =
     | None  -> (FStar_Util.smap_add strings s s; s)
 let default_string_finish endm b s = FStar_Parser_Parse.STRING s
 let call_string_finish fin buf endm b =
-  let _0_25 = FStar_Bytes.close buf in fin endm b _0_25
+  let _0_26 = FStar_Bytes.close buf in fin endm b _0_26
 let add_string: FStar_Bytes.bytebuf -> Prims.string -> Prims.unit =
   fun buf  ->
     fun x  ->

src/ocaml-output/FStar_Parser_ToDocument.ml

@@ -494,15 +494,15 @@ let handleable_args_length: FStar_Ident.ident -> Prims.int =
          else Prims.parse_int "0")
 let handleable_op op args =
   match FStar_List.length args with
-  | _0_26 when _0_26 = (Prims.parse_int "0") -> true
-  | _0_27 when _0_27 = (Prims.parse_int "1") ->
+  | _0_27 when _0_27 = (Prims.parse_int "0") -> true
+  | _0_28 when _0_28 = (Prims.parse_int "1") ->
       (is_general_prefix_op op) ||
         (FStar_List.mem (FStar_Ident.text_of_id op) ["-"; "~"])
-  | _0_28 when _0_28 = (Prims.parse_int "2") ->
+  | _0_29 when _0_29 = (Prims.parse_int "2") ->
       ((is_operatorInfix0ad12 op) || (is_operatorInfix34 op)) ||
         (FStar_List.mem (FStar_Ident.text_of_id op)
            ["<==>"; "==>"; "\\/"; "/\\"; "="; "|>"; ":="; ".()"; ".[]"])
-  | _0_29 when _0_29 = (Prims.parse_int "3") ->
+  | _0_30 when _0_30 = (Prims.parse_int "3") ->
       FStar_List.mem (FStar_Ident.text_of_id op) [".()<-"; ".[]<-"]
   | uu____1377 -> false
 let comment_stack: (Prims.string* FStar_Range.range) Prims.list FStar_ST.ref