Support signed and unsigned arithmetic

5 files changed, 151 insertions, 75 deletions

diff --git a/src/lem_interp/interp_inter_imp.lem b/src/lem_interp/interp_inter_imp.lem
index da6b27f4..31a75b73 100644
--- a/src/lem_interp/interp_inter_imp.lem
+++ b/src/lem_interp/interp_inter_imp.lem
@@ -150,11 +150,11 @@ let add_to_address value num =
     | Unknown -> Unknown
     | Bitvector _ _ _ -> 
       fst(extern_value (make_mode true false) false Nothing
-	             (Interp_lib.arith_op_vec_range (+) 1 
+	             (Interp_lib.arith_op_vec_range (+) Interp_lib.Unsigned 1 
 			(Interp.V_tuple [(intern_value value);Interp.V_lit (L_aux (L_num num) Interp_ast.Unknown)])))
     | Bytevector _ ->
       fst(extern_value (make_mode true false) true Nothing
-	             (Interp_lib.arith_op_vec_range (+) 1 
+	             (Interp_lib.arith_op_vec_range (+) Interp_lib.Unsigned 1 
 			(Interp.V_tuple [(intern_value value);Interp.V_lit (L_aux (L_num num) Interp_ast.Unknown)])))
 end
 
diff --git a/src/lem_interp/interp_lib.lem b/src/lem_interp/interp_lib.lem
index 6c6bbb46..696e0547 100644
--- a/src/lem_interp/interp_lib.lem
+++ b/src/lem_interp/interp_lib.lem
@@ -198,109 +198,109 @@ let rec arith_op op (V_tuple args) = match args with
   | [V_unknown;_] -> V_unknown
   | [_;V_unknown] -> V_unknown
   end ;;
-let rec arith_op_vec op size (V_tuple args) = match args with
+let rec arith_op_vec op sign size (V_tuple args) = match args with
   | [(V_vector b ord cs as l1);(V_vector _ _ _ as l2)] ->
-    let (l1',l2') = (to_num Unsigned l1,to_num Unsigned l2) in
+    let (l1',l2') = (to_num sign l1,to_num sign l2) in
     let n = arith_op op (V_tuple [l1';l2']) in
     to_vec ord ((List.length cs) * size) n
   | [V_track v1 r1;V_track v2 r2] ->
-    taint (arith_op_vec op size (V_tuple [v1;v2])) (r1++r2)
+    taint (arith_op_vec op sign size (V_tuple [v1;v2])) (r1++r2)
   | [V_track v1 r1;v2] ->
-    taint (arith_op_vec op size (V_tuple [v1;v2])) r1
+    taint (arith_op_vec op sign size (V_tuple [v1;v2])) r1
   | [v1;V_track v2 r2] ->
-    taint (arith_op_vec op size (V_tuple [v1;v2])) r2
+    taint (arith_op_vec op sign size (V_tuple [v1;v2])) r2
   | [V_unknown;_] -> V_unknown
   | [_;V_unknown] -> V_unknown
 end ;;
-let rec arith_op_vec_vec_range op (V_tuple args) = match args with
+let rec arith_op_vec_vec_range op sign (V_tuple args) = match args with
   | [(V_vector b ord cs as l1);(V_vector _ _ _ as l2)] ->
-    let (l1',l2') = (to_num Unsigned l1,to_num Unsigned l2) in
+    let (l1',l2') = (to_num sign l1,to_num sign l2) in
     arith_op op (V_tuple [l1';l2'])
   | [V_track v1 r1;V_track v2 r2] ->
-    taint (arith_op_vec_vec_range op (V_tuple [v1;v2])) (r1++r2)
+    taint (arith_op_vec_vec_range op sign (V_tuple [v1;v2])) (r1++r2)
   | [V_track v1 r1;v2] ->
-    taint (arith_op_vec_vec_range op (V_tuple [v1;v2])) r1
+    taint (arith_op_vec_vec_range op sign (V_tuple [v1;v2])) r1
   | [v1;V_track v2 r2] ->
-    taint (arith_op_vec_vec_range op (V_tuple [v1;v2])) r2
+    taint (arith_op_vec_vec_range op sign (V_tuple [v1;v2])) r2
   | [V_unknown;_] -> V_unknown
   | [_;V_unknown] -> V_unknown
 end ;;
-let rec arith_op_overflow_vec op size (V_tuple args) = match args with
+let rec arith_op_overflow_vec op sign size (V_tuple args) = match args with
   | [(V_vector b ord cs as l1);(V_vector _ _ _ as l2)] ->
-    let (l1',l2') = (to_num Signed l1,to_num Signed l2) in
+    let (l1',l2') = (to_num sign l1,to_num sign l2) in
     let n = arith_op op (V_tuple [l1';l2']) in
     let correct_size_num = to_vec ord ((List.length cs) * size) n in
     let one_larger = to_num Signed (to_vec ord (((List.length cs) * size) +1) n) in
     let overflow =  neq (V_tuple [correct_size_num;one_larger]) in
     V_tuple [correct_size_num;overflow]
   | [V_track v1 r1;V_track v2 r2] ->
-    taint (arith_op_overflow_vec op size (V_tuple [v1;v2])) (r1++r2)
+    taint (arith_op_overflow_vec op sign size (V_tuple [v1;v2])) (r1++r2)
   | [V_track v1 r1;v2] ->
-    taint (arith_op_overflow_vec op size (V_tuple [v1;v2])) r1
+    taint (arith_op_overflow_vec op sign size (V_tuple [v1;v2])) r1
   | [v1;V_track v2 r2] ->
-    taint (arith_op_overflow_vec op size (V_tuple [v1;v2])) r2
+    taint (arith_op_overflow_vec op sign size (V_tuple [v1;v2])) r2
   | [V_unknown;_] -> V_tuple [V_unknown;V_unknown]
   | [_;V_unknown] -> V_tuple [V_unknown;V_unknown]
 end ;;
-let rec arith_op_range_vec op size (V_tuple args) = match args with
+let rec arith_op_range_vec op sign size (V_tuple args) = match args with
   | [V_track v1 r1;V_track v2 r2] ->
-    taint (arith_op_range_vec op size (V_tuple [v1;v2])) (r1++r2)
+    taint (arith_op_range_vec op sign size (V_tuple [v1;v2])) (r1++r2)
   | [V_track v1 r1; v2] ->
-    taint (arith_op_range_vec op size (V_tuple [v1;v2])) r1
+    taint (arith_op_range_vec op sign size (V_tuple [v1;v2])) r1
   | [v1;V_track v2 r2] -> 
-    taint (arith_op_range_vec op size (V_tuple [v1;v2])) r2
+    taint (arith_op_range_vec op sign size (V_tuple [v1;v2])) r2
   | [V_unknown;_] -> V_unknown
   | [_;V_unknown] -> V_unknown
   | [n; (V_vector _ ord cs as l2)] ->
-    arith_op_vec op size (V_tuple [(to_vec ord (List.length cs) n);l2])
+    arith_op_vec op sign size (V_tuple [(to_vec ord (List.length cs) n);l2])
 end ;;
-let rec arith_op_vec_range op size (V_tuple args) = match args with
+let rec arith_op_vec_range op sign size (V_tuple args) = match args with
   | [V_track v1 r1;V_track v2 r2] ->
-    taint (arith_op_vec_range op size (V_tuple [v1;v2])) (r1++r2)
+    taint (arith_op_vec_range op sign size (V_tuple [v1;v2])) (r1++r2)
   | [V_track v1 r1; v2] ->
-    taint (arith_op_vec_range op size (V_tuple [v1;v2])) r1
+    taint (arith_op_vec_range op sign size (V_tuple [v1;v2])) r1
   | [v1;V_track v2 r2] -> 
-    taint (arith_op_vec_range op size (V_tuple [v1;v2])) r2
+    taint (arith_op_vec_range op sign size (V_tuple [v1;v2])) r2
   | [V_unknown;_] -> V_unknown
   | [_;V_unknown] -> V_unknown
   | [(V_vector _ ord cs as l1);n] ->
-    arith_op_vec op size (V_tuple [l1;(to_vec ord (List.length cs) n)])
+    arith_op_vec op sign size (V_tuple [l1;(to_vec ord (List.length cs) n)])
 end ;;
-let rec arith_op_range_vec_range op (V_tuple args) = match args with
+let rec arith_op_range_vec_range op sign (V_tuple args) = match args with
   | [V_track v1 r1;V_track v2 r2] ->
-    taint (arith_op_range_vec_range op (V_tuple [v1;v2])) (r1++r2)
+    taint (arith_op_range_vec_range op sign (V_tuple [v1;v2])) (r1++r2)
   | [V_track v1 r1; v2] ->
-    taint (arith_op_range_vec_range op (V_tuple [v1;v2])) r1
+    taint (arith_op_range_vec_range op sign (V_tuple [v1;v2])) r1
   | [v1;V_track v2 r2] -> 
-    taint (arith_op_range_vec_range op (V_tuple [v1;v2])) r2
+    taint (arith_op_range_vec_range op sign (V_tuple [v1;v2])) r2
   | [V_unknown;_] -> V_unknown
   | [_;V_unknown] -> V_unknown
   | [n;(V_vector _ ord _ as l2)] ->
     arith_op op (V_tuple [n;(to_num Unsigned l2)])
 end ;;
-let rec arith_op_vec_range_range op (V_tuple args) = match args with
+let rec arith_op_vec_range_range op sign (V_tuple args) = match args with
   | [V_track v1 r1;V_track v2 r2] ->
-    taint (arith_op_vec_range_range op (V_tuple [v1;v2])) (r1++r2)
+    taint (arith_op_vec_range_range op sign (V_tuple [v1;v2])) (r1++r2)
   | [V_track v1 r1; v2] ->
-    taint (arith_op_vec_range_range op (V_tuple [v1;v2])) r1
+    taint (arith_op_vec_range_range op sign (V_tuple [v1;v2])) r1
   | [v1;V_track v2 r2] -> 
-    taint (arith_op_vec_range_range op (V_tuple [v1;v2])) r2
+    taint (arith_op_vec_range_range op sign (V_tuple [v1;v2])) r2
   | [V_unknown;_] -> V_unknown
   | [_;V_unknown] -> V_unknown
   | [(V_vector _ ord _ as l1);n] ->
-    arith_op op (V_tuple [(to_num Unsigned l1);n])
+    arith_op op (V_tuple [(to_num sign l1);n])
 end ;;
-let rec arith_op_vec_bit op size (V_tuple args) = match args with
+let rec arith_op_vec_bit op sign size (V_tuple args) = match args with
   | [V_track v1 r1;V_track v2 r2] ->
-    taint (arith_op_vec_bit op size (V_tuple [v1;v2])) (r1++r2)
+    taint (arith_op_vec_bit op sign size (V_tuple [v1;v2])) (r1++r2)
   | [V_track v1 r1; v2] ->
-    taint (arith_op_vec_bit op size (V_tuple [v1;v2])) r1
+    taint (arith_op_vec_bit op sign size (V_tuple [v1;v2])) r1
   | [v1;V_track v2 r2] -> 
-    taint (arith_op_vec_bit op size (V_tuple [v1;v2])) r2
+    taint (arith_op_vec_bit op sign size (V_tuple [v1;v2])) r2
   | [V_unknown;_] -> V_unknown
   | [_;V_unknown] -> V_unknown
   | [(V_vector _ ord cs as l1);V_lit (L_aux bit _)] ->
-    let l1' = to_num Unsigned l1 in
+    let l1' = to_num sign l1 in
     let n = arith_op op (V_tuple 
 			   [l1';
 			    V_lit 
@@ -320,31 +320,31 @@ let rec arith_op_no0 op (V_tuple args) = match args with
   | [V_unknown;_] -> V_unknown
   | [_;V_unknown] -> V_unknown
   end ;;
-let rec arith_op_vec_no0 op size (V_tuple args) = match args with
+let rec arith_op_vec_no0 op sign size (V_tuple args) = match args with
   | [(V_vector b ord cs as l1);(V_vector _ _ _ as l2)] ->
-    let (l1',l2') = (to_num Unsigned l1,to_num Unsigned l2) in
+    let (l1',l2') = (to_num sign l1,to_num sign l2) in
     let n = arith_op_no0 op (V_tuple [l1';l2']) in
     to_vec ord ((List.length cs) * size) n
   | [V_track v1 r1;V_track v2 r2] ->
-    taint (arith_op_vec_no0 op size (V_tuple [v1;v2])) (r1++r2)
+    taint (arith_op_vec_no0 op sign size (V_tuple [v1;v2])) (r1++r2)
   | [V_track v1 r1;v2] ->
-    taint (arith_op_vec_no0 op size (V_tuple [v1;v2])) r1
+    taint (arith_op_vec_no0 op sign size (V_tuple [v1;v2])) r1
   | [v1;V_track v2 r2] ->
-    taint (arith_op_vec_no0 op size (V_tuple [v1;v2])) r2
+    taint (arith_op_vec_no0 op sign size (V_tuple [v1;v2])) r2
   | [V_unknown;_] -> V_unknown
   | [_;V_unknown] -> V_unknown
 end ;;
-let rec arith_op_vec_range_no0 op size (V_tuple args) = match args with
+let rec arith_op_vec_range_no0 op sign size (V_tuple args) = match args with
   | [V_track v1 r1;V_track v2 r2] ->
-    taint (arith_op_vec_range_no0 op size (V_tuple [v1;v2])) (r1++r2)
+    taint (arith_op_vec_range_no0 op sign size (V_tuple [v1;v2])) (r1++r2)
   | [V_track v1 r1; v2] ->
-    taint (arith_op_vec_range_no0 op size (V_tuple [v1;v2])) r1
+    taint (arith_op_vec_range_no0 op sign size (V_tuple [v1;v2])) r1
   | [v1;V_track v2 r2] -> 
-    taint (arith_op_vec_range_no0 op size (V_tuple [v1;v2])) r2
+    taint (arith_op_vec_range_no0 op sign size (V_tuple [v1;v2])) r2
   | [V_unknown;_] -> V_unknown
   | [_;V_unknown] -> V_unknown
   | [(V_vector _ ord cs as l1);n] ->
-    arith_op_vec_no0 op size (V_tuple [l1;(to_vec ord (List.length cs) n)])
+    arith_op_vec_no0 op sign size (V_tuple [l1;(to_vec ord (List.length cs) n)])
 end ;;
 
 let rec compare_op op (V_tuple args) = match args with
@@ -424,32 +424,41 @@ let function_map = [
   ("ignore", ignore_sail);            
   ("length", v_length);
   ("add", arith_op (+));
-  ("add_vec", arith_op_vec (+) 1);
-  ("add_vec_range", arith_op_vec_range (+) 1);
-  ("add_vec_range_range", arith_op_vec_range_range (+));
-  ("add_range_vec", arith_op_range_vec (+) 1);
-  ("add_range_vec_range", arith_op_range_vec_range (+));
-  ("add_vec_vec_range", arith_op_vec_vec_range (+));
-  ("add_vec_bit", arith_op_vec_bit (+) 1);
-  ("add_overload_vec", arith_op_overflow_vec (+) 1);
+  ("add_vec", arith_op_vec (+) Unsigned 1);
+  ("add_vec_range", arith_op_vec_range (+) Unsigned  1);
+  ("add_vec_range_range", arith_op_vec_range_range (+) Unsigned);
+  ("add_range_vec", arith_op_range_vec (+) Unsigned 1);
+  ("add_range_vec_range", arith_op_range_vec_range (+) Unsigned);
+  ("add_vec_vec_range", arith_op_vec_vec_range (+) Unsigned);
+  ("add_vec_bit", arith_op_vec_bit (+) Unsigned 1);
+  ("add_overflow_vec", arith_op_overflow_vec (+) Unsigned 1);
+  ("add_signed", arith_op (+));
+  ("add_vec_signed", arith_op_vec (+) Signed 1);
+  ("add_vec_range_signed", arith_op_vec_range (+) Signed 1);
+  ("add_vec_range_range_signed", arith_op_vec_range_range (+) Signed);
+  ("add_range_vec_signed", arith_op_range_vec (+) Signed 1);
+  ("add_range_vec_range_signed", arith_op_range_vec_range (+) Signed);
+  ("add_vec_vec_range_signed", arith_op_vec_vec_range (+) Signed);
+  ("add_vec_bit_signed", arith_op_vec_bit (+) Signed 1);
+  ("add_overflow_vec_signed", arith_op_overflow_vec (+) Signed 1);
   ("minus", arith_op (-));
-  ("minus_vec", arith_op_vec (-) 1);
-  ("minus_vec_range", arith_op_vec_range (-) 1);
-  ("minus_range_vec", arith_op_range_vec (-) 1);
-  ("minus_vec_range_range", arith_op_vec_range_range (-));
-  ("minus_range_vec_range", arith_op_range_vec_range (-));
-  ("minus_vec_bit", arith_op_vec_bit (-) 1);
-  ("minus_overload_vec", arith_op_overflow_vec (-) 1);
+  ("minus_vec", arith_op_vec (-) Unsigned 1);
+  ("minus_vec_range", arith_op_vec_range (-) Unsigned 1);
+  ("minus_range_vec", arith_op_range_vec (-) Unsigned 1);
+  ("minus_vec_range_range", arith_op_vec_range_range (-) Unsigned);
+  ("minus_range_vec_range", arith_op_range_vec_range (-) Unsigned);
+  ("minus_vec_bit", arith_op_vec_bit (-) Unsigned 1);
+  ("minus_overload_vec", arith_op_overflow_vec (-) Unsigned 1);
   ("multiply", arith_op ( * ));
-  ("multiply_vec", arith_op_vec ( * ) 2);
-  ("mult_range_vec", arith_op_range_vec ( * ) 2);
-  ("mult_vec_range", arith_op_vec_range ( * ) 2);
-  ("mult_overload_vec", arith_op_overflow_vec ( * ) 2);
+  ("multiply_vec", arith_op_vec ( * ) Unsigned 2);
+  ("mult_range_vec", arith_op_range_vec ( * ) Unsigned 2);
+  ("mult_vec_range", arith_op_vec_range ( * ) Unsigned 2);
+  ("mult_overload_vec", arith_op_overflow_vec ( * ) Unsigned 2);
   ("mod", arith_op_no0 (mod));
-  ("mod_vec", arith_op_vec_no0 (mod) 1);
-  ("mod_vec_range", arith_op_vec_range_no0 (mod) 1);
+  ("mod_vec", arith_op_vec_no0 (mod)  Unsigned 1);
+  ("mod_vec_range", arith_op_vec_range_no0 (mod) Unsigned 1);
   ("quot", arith_op_no0 (/));
-  ("quot_vec", arith_op_vec_no0 (/) 1);
+  ("quot_vec", arith_op_vec_no0 (/)  Unsigned 1);
   ("eq", eq);
   ("eq_vec_range", eq_vec_range);
   ("eq_range_vec", eq_range_vec);
diff --git a/src/lexer.mll b/src/lexer.mll
index 1dfcfe12..9866390a 100644
--- a/src/lexer.mll
+++ b/src/lexer.mll
@@ -200,6 +200,8 @@ rule token = parse
   | "[|"                                { SquareBar }
   | "~^"				{ (TildeCarrot(r"~^")) }
 
+  | "+_s"                               { (PlusUnderS(r"+_s")) }
+  | "-_s"                               { (MinusUnderS(r"-_s")) }
   | ">=_s"				{ (GtEqUnderS(r">=_s")) }
   | ">=_si"				{ (GtEqUnderSi(r">=_si")) }
   | ">=_u"				{ (GtEqUnderU(r">=_u")) }
diff --git a/src/parser.mly b/src/parser.mly
index 6d019af4..943a2669 100644
--- a/src/parser.mly
+++ b/src/parser.mly
@@ -160,7 +160,7 @@ let make_vector_sugar order_set is_inc typ typ1 =
 %token <string> GtEqUnderS GtEqUnderSi GtEqUnderU GtEqUnderUi GtGtUnderU GtUnderS
 %token <string> GtUnderSi GtUnderU GtUnderUi LtEqUnderS LtEqUnderSi LtEqUnderU
 %token <string> LtEqUnderUi LtUnderS LtUnderSi LtUnderU LtUnderUi StarStarUnderS StarStarUnderSi StarUnderS
-%token <string> StarUnderSi StarUnderU StarUnderUi TwoCarrot
+%token <string> StarUnderSi StarUnderU StarUnderUi TwoCarrot PlusUnderS MinusUnderS
 
 %token <string> AmpI AtI CarrotI  DivI EqI ExclI GtI LtI PlusI StarI TildeI
 %token <string> AmpAmpI CarrotCarrotI ColonColonI EqDivEqI EqEqI ExclEqI ExclExclI
@@ -209,10 +209,14 @@ id:
     { idl (DeIid($3)) }
   | Lparen Deinfix Minus Rparen
     { idl (DeIid("-")) }
+  | Lparen Deinfix MinusUnderS Rparen
+    { idl (DeIid("-_s")) }
   | Lparen Deinfix Mod Rparen
     { idl (DeIid("mod")) }
   | Lparen Deinfix Plus Rparen
     { idl (DeIid($3)) }
+  | Lparen Deinfix PlusUnderS Rparen
+    { idl (DeIid("+_s")) }
   | Lparen Deinfix Star Rparen
     { idl (DeIid($3)) }
   | Lparen Deinfix AmpAmp Rparen
@@ -700,8 +704,12 @@ plus_exp:
     { $1 }
   | plus_exp Plus star_exp
     { eloc (E_app_infix($1,Id_aux(Id($2), locn 2 2), $3)) }
+  | plus_exp PlusUnderS star_exp
+    { eloc (E_app_infix($1, Id_aux(Id($2), locn 2 2), $3)) }
   | plus_exp Minus star_exp
     { eloc (E_app_infix($1,Id_aux(Id("-"), locn 2 2), $3)) }
+  | plus_exp MinusUnderS star_exp
+    { eloc (E_app_infix($1,Id_aux(Id("-_s"),locn 2 2), $3)) }
 
 plus_right_atomic_exp:
   | star_right_atomic_exp
diff --git a/src/type_internal.ml b/src/type_internal.ml
index 8e68c3c4..2ae210da 100644
--- a/src/type_internal.ml
+++ b/src/type_internal.ml
@@ -884,7 +884,7 @@ let initial_typ_env =
                          (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (Nvar "o") (Nvar "n");
                                                mk_vector bit_t (Ovar "ord") (Nvar "p") (Nvar "n")])
                                       (mk_tup [(mk_vector bit_t (Ovar "ord") (Nvar "o") (Nvar "n")); bit_t]))),
-			External (Some "add_overload_vec"),[],pure_e);
+			External (Some "add_overflow_vec"),[],pure_e);
 		   Base(((mk_nat_params ["n";"m";"o";"p";])@(mk_ord_params ["ord"]),
 			 (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (Nvar "n") (Nvar "m");
 					       mk_range (mk_nv "o") (mk_nv "p")])
@@ -913,6 +913,63 @@ let initial_typ_env =
                                      (mk_vector bit_t (Ovar "ord") (Nvar "o") (Nvar "p")))),
                        External (Some "add_bit_vec"), [], pure_e);
                   ]));
+    ("+_s",Overload(Base(((mk_typ_params ["a";"b";"c"]),
+                          (mk_pure_fun (mk_tup [{t=Tvar "a"};{t=Tvar "b"}]) {t=Tvar "c"})),External (Some "add"),[],pure_e),
+		    true,
+                    [Base(((mk_nat_params ["n";"m";"o";"p"]),
+                           (mk_pure_fun (mk_tup [mk_range (mk_nv "n") (mk_nv "m"); mk_range (mk_nv "o") (mk_nv "p")])
+		              (mk_range (mk_add (mk_nv "n") (mk_nv "o")) (mk_add (mk_nv "m") (mk_nv "p"))))),
+		          External (Some "add_signed"),[],pure_e);
+                   Base(((mk_nat_params ["n";"o";"p"])@(mk_ord_params ["ord"]),
+                         (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (Nvar "o") (Nvar "n");
+                                               mk_vector bit_t (Ovar "ord") (Nvar "p") (Nvar "n")])
+                                      (mk_vector bit_t (Ovar "ord") (Nvar "o") (Nvar "n")))),
+			External (Some "add_vec_signed"),[],pure_e);
+		   Base(((mk_nat_params ["n";"o";"p";"q"])@(mk_ord_params ["ord"]),
+                         (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (Nvar "o") (Nvar "n");
+                                               mk_vector bit_t (Ovar "ord") (Nvar "p") (Nvar "n")])
+                                      (mk_range (mk_nv "q") {nexp = N2n (mk_nv "n",None)}))),
+			External (Some "add_vec_vec_range_signed"),[],pure_e);
+                   
+                   Base(((mk_nat_params ["n";"m";"o";"p"])@(mk_ord_params ["ord"]),
+                        (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (Nvar "n") (Nvar "m");
+                                              mk_range (mk_nv "o") (mk_nv "p")])
+                                     (mk_vector bit_t (Ovar "ord") (Nvar "n") (Nvar "m")))),
+                        External (Some "add_vec_range_signed"),
+                        [LtEq(Specc(Parse_ast.Int("+",None)),mk_add (mk_nv "o") (mk_nv "p"),{nexp=N2n (mk_nv "m",None)})],pure_e);
+                   Base(((mk_nat_params ["n";"o";"p"])@(mk_ord_params ["ord"]),
+                         (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (Nvar "o") (Nvar "n");
+                                               mk_vector bit_t (Ovar "ord") (Nvar "p") (Nvar "n")])
+                                      (mk_tup [(mk_vector bit_t (Ovar "ord") (Nvar "o") (Nvar "n")); bit_t]))),
+			External (Some "add_overflow_vec_signed"),[],pure_e);
+		   Base(((mk_nat_params ["n";"m";"o";"p";])@(mk_ord_params ["ord"]),
+			 (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (Nvar "n") (Nvar "m");
+					       mk_range (mk_nv "o") (mk_nv "p")])
+			              (mk_range (mk_nv "o") (mk_add (mk_nv "p") {nexp = N2n (mk_nv "m",None)})))),
+			External (Some "add_vec_range_range_signed"),
+			[LtEq(Specc(Parse_ast.Int("+",None)),mk_add (mk_nv "o") (mk_nv "p"),{nexp=N2n (mk_nv "m",None)})],pure_e);
+                   Base(((mk_nat_params ["n";"m";"o";"p"])@(mk_ord_params ["ord"]),
+                         (mk_pure_fun (mk_tup [mk_range (mk_nv "o") (mk_nv "p");
+                                               mk_vector bit_t (Ovar "ord") (Nvar "n") (Nvar "m");])
+                                      (mk_vector bit_t (Ovar "ord") (Nvar "n") (Nvar "m")))),
+                        External (Some "add_range_vec_signed"),
+                       [LtEq(Specc(Parse_ast.Int("+",None)),mk_add (mk_nv "o") (mk_nv "p"),{nexp = N2n (mk_nv "m",None)})],pure_e);
+		   Base(((mk_nat_params ["n";"m";"o";"p";])@(mk_ord_params ["ord"]),
+			 (mk_pure_fun (mk_tup [mk_range (mk_nv "o") (mk_nv "p");
+					       mk_vector bit_t (Ovar "ord") (Nvar "n") (Nvar "m");])
+			              (mk_range (mk_nv "o") (mk_add (mk_nv "p") {nexp = N2n (mk_nv "m",None)})))),
+			External (Some "add_range_vec_range_signed"),
+			[LtEq(Specc(Parse_ast.Int("+",None)),mk_add (mk_nv "o") (mk_nv "p"),{nexp=N2n (mk_nv "m",None)})],pure_e);
+
+                  Base(((mk_nat_params ["o";"p"]@(mk_ord_params["ord"])),
+                        (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (Nvar "o") (Nvar "p"); bit_t])
+                                     (mk_vector bit_t (Ovar "ord") (Nvar "o") (Nvar "p")))),
+                       External (Some "add_vec_bit"), [], pure_e);
+                  Base(((mk_nat_params ["o";"p"]@(mk_ord_params["ord"])),
+                        (mk_pure_fun (mk_tup [bit_t; mk_vector bit_t (Ovar "ord") (Nvar "o") (Nvar "p")])
+                                     (mk_vector bit_t (Ovar "ord") (Nvar "o") (Nvar "p")))),
+                       External (Some "add_bit_vec_signed"), [], pure_e);
+                  ]));
     ("-",Overload(Base(((mk_typ_params ["a";"b";"c"]),
                         (mk_pure_fun (mk_tup [{t=Tvar "a"};{t=Tvar "b"}]) {t=Tvar "c"})), External (Some "minus"),[],pure_e),
 		  true,