Merge PR #13559: Signed primitive integers

Reviewed-by: SkySkimmer
Reviewed-by: silene
Reviewed-by: jfehrle
Ack-by: gares
Ack-by: Zimmi48
Ack-by: proux01

13 files changed, 334 insertions, 9 deletions

diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c
index 95a334561f..704eb1ef98 100644
--- a/kernel/byterun/coq_interp.c
+++ b/kernel/byterun/coq_interp.c
@@ -1426,6 +1426,41 @@ value coq_interprete
         Next;
       }
 
+      Instruct(CHECKDIVSINT63) {
+        print_instr("CHEKDIVSINT63");
+        CheckInt2();
+        int b;
+        Uint63_eq0(b, *sp);
+        if (b) {
+          accu = *sp++;
+        }
+        else {
+          Uint63_eqm1(b, *sp);
+          if (b) {
+            Uint63_neg(accu);
+            sp++;
+          }
+          else {
+            Uint63_divs(accu, *sp++);
+          }
+        }
+        Next;
+      }
+
+      Instruct(CHECKMODSINT63) {
+        print_instr("CHEKMODSINT63");
+        CheckInt2();
+        int b;
+        Uint63_eq0(b, *sp);
+        if (b) {
+          accu = *sp++;
+        }
+        else {
+          Uint63_mods(accu,*sp++);
+        }
+        Next;
+      }
+
       Instruct (CHECKDIV21INT63) {
         print_instr("DIV21INT63");
         CheckInt3();
@@ -1473,6 +1508,13 @@ value coq_interprete
         Next;
       }
 
+      Instruct(CHECKASRINT63) {
+        print_instr("CHECKASRINT63");
+        CheckInt2();
+        Uint63_asr(accu,*sp++);
+        Next;
+      }
+
       Instruct (CHECKADDMULDIVINT63) {
         print_instr("CHECKADDMULDIVINT63");
         CheckInt3();
@@ -1508,6 +1550,24 @@ value coq_interprete
        Next;
      }
 
+     Instruct (CHECKLTSINT63) {
+       print_instr("CHECKLTSINT63");
+       CheckInt2();
+       int b;
+       Uint63_lts(b,accu,*sp++);
+       accu = b ? coq_true : coq_false;
+       Next;
+     }
+
+     Instruct (CHECKLESINT63) {
+       print_instr("CHECKLESINT63");
+       CheckInt2();
+       int b;
+       Uint63_les(b,accu,*sp++);
+       accu = b ? coq_true : coq_false;
+       Next;
+     }
+
      Instruct (CHECKCOMPAREINT63) {
         /* returns Eq if equal, Lt if accu is less than *sp, Gt otherwise */
         /* assumes Inductive _ : _ := Eq | Lt | Gt */
@@ -1526,6 +1586,24 @@ value coq_interprete
         Next;
       }
 
+     Instruct (CHECKCOMPARESINT63) {
+       /* returns Eq if equal, Lt if accu is less than *sp, Gt otherwise */
+       /* assumes Inductive _ : _ := Eq | Lt | Gt */
+       print_instr("CHECKCOMPARESINT63");
+       CheckInt2();
+       int b;
+       Uint63_eq(b, accu, *sp);
+       if (b) {
+         accu = coq_Eq;
+         sp++;
+       }
+       else {
+         Uint63_lts(b, accu, *sp++);
+         accu = b ? coq_Lt : coq_Gt;
+       }
+       Next;
+     }
+
       Instruct (CHECKHEAD0INT63) {
         print_instr("CHECKHEAD0INT63");
         CheckInt1();
diff --git a/kernel/byterun/coq_uint63_emul.h b/kernel/byterun/coq_uint63_emul.h
index dd9b9e55be..693716ee90 100644
--- a/kernel/byterun/coq_uint63_emul.h
+++ b/kernel/byterun/coq_uint63_emul.h
@@ -96,7 +96,10 @@ value uint63_##name##_ml(value x, value y, value z) { \
     accu = uint63_return_value__; \
   }while(0)
 
+DECLARE_NULLOP(zero)
 DECLARE_NULLOP(one)
+DECLARE_UNOP(neg)
+#define Uint63_neg(x) CALL_UNOP(neg, x)
 DECLARE_BINOP(add)
 #define Uint63_add(x, y) CALL_BINOP(add, x, y)
 DECLARE_BINOP(addcarry)
@@ -105,28 +108,40 @@ DECLARE_TEROP(addmuldiv)
 #define Uint63_addmuldiv(x, y, z) CALL_TEROP(addmuldiv, x, y, z)
 DECLARE_BINOP(div)
 #define Uint63_div(x, y) CALL_BINOP(div, x, y)
+DECLARE_BINOP(divs)
+#define Uint63_divs(x, y) CALL_BINOP(divs, x, y)
 DECLARE_BINOP(eq)
 #define Uint63_eq(r, x, y) CALL_RELATION(r, eq, x, y)
 DECLARE_UNOP(eq0)
 #define Uint63_eq0(r, x) CALL_PREDICATE(r, eq0, x)
+DECLARE_UNOP(eqm1)
+#define Uint63_eqm1(r, x) CALL_PREDICATE(r, eqm1, x)
 DECLARE_UNOP(head0)
 #define Uint63_head0(x) CALL_UNOP(head0, x)
 DECLARE_BINOP(land)
 #define Uint63_land(x, y) CALL_BINOP(land, x, y)
 DECLARE_BINOP(leq)
 #define Uint63_leq(r, x, y) CALL_RELATION(r, leq, x, y)
+DECLARE_BINOP(les)
+#define Uint63_les(r, x, y) CALL_RELATION(r, les, x, y)
 DECLARE_BINOP(lor)
 #define Uint63_lor(x, y) CALL_BINOP(lor, x, y)
 DECLARE_BINOP(lsl)
 #define Uint63_lsl(x, y) CALL_BINOP(lsl, x, y)
 DECLARE_BINOP(lsr)
 #define Uint63_lsr(x, y) CALL_BINOP(lsr, x, y)
+DECLARE_BINOP(asr)
+#define Uint63_asr(x, y) CALL_BINOP(asr, x, y)
 DECLARE_BINOP(lt)
 #define Uint63_lt(r, x, y) CALL_RELATION(r, lt, x, y)
+DECLARE_BINOP(lts)
+#define Uint63_lts(r, x, y) CALL_RELATION(r, lts, x, y)
 DECLARE_BINOP(lxor)
 #define Uint63_lxor(x, y) CALL_BINOP(lxor, x, y)
 DECLARE_BINOP(mod)
 #define Uint63_mod(x, y) CALL_BINOP(mod, x, y)
+DECLARE_BINOP(mods)
+#define Uint63_mods(x, y) CALL_BINOP(mods, x, y)
 DECLARE_BINOP(mul)
 #define Uint63_mul(x, y) CALL_BINOP(mul, x, y)
 DECLARE_BINOP(sub)
diff --git a/kernel/byterun/coq_uint63_native.h b/kernel/byterun/coq_uint63_native.h
index 731ae8f46e..da9ae7f147 100644
--- a/kernel/byterun/coq_uint63_native.h
+++ b/kernel/byterun/coq_uint63_native.h
@@ -12,21 +12,28 @@
 
 #define uint_of_value(val) (((uint64_t)(val)) >> 1)
 #define uint63_of_value(val) ((uint64_t)(val) >> 1)
+#define int63_of_value(val) ((int64_t)(val) >> 1)
 
 /* 2^63 * y + x as a value */
 //#define Val_intint(x,y) ((value)(((uint64_t)(x)) << 1 + ((uint64_t)(y) << 64)))
 
-#define uint63_zero ((value) 1) /* 2*0 + 1 */
+#define uint63_zero() ((value) 1) /* 2*0 + 1 */
 #define uint63_one() ((value) 3) /* 2*1 + 1 */
 
 #define uint63_eq(x,y) ((x) == (y))
 #define Uint63_eq(r,x,y) ((r) = uint63_eq(x,y))
 #define Uint63_eq0(r,x) ((r) = ((x) == (uint64_t)1))
+#define Uint63_eqm1(r,x) ((r) = ((x) == (uint64_t)(int64_t)(-1)))
 #define uint63_lt(x,y) ((uint64_t) (x) < (uint64_t) (y))
 #define Uint63_lt(r,x,y) ((r) = uint63_lt(x,y))
 #define uint63_leq(x,y) ((uint64_t) (x) <= (uint64_t) (y))
 #define Uint63_leq(r,x,y) ((r) = uint63_leq(x,y))
+#define uint63_lts(x,y) ((int64_t) (x) < (int64_t) (y))
+#define Uint63_lts(r,x,y) ((r) = uint63_lts(x,y))
+#define uint63_les(x,y) ((int64_t) (x) <= (int64_t) (y))
+#define Uint63_les(r,x,y) ((r) = uint63_les(x,y))
 
+#define Uint63_neg(x) (accu = (value)(2 - (uint64_t) x))
 #define Uint63_add(x,y) (accu = (value)((uint64_t) (x) + (uint64_t) (y) - 1))
 #define Uint63_addcarry(x,y) (accu = (value)((uint64_t) (x) + (uint64_t) (y) + 1))
 #define Uint63_sub(x,y) (accu = (value)((uint64_t) (x) - (uint64_t) (y) + 1))
@@ -34,6 +41,8 @@
 #define Uint63_mul(x,y) (accu = Val_long(uint63_of_value(x) * uint63_of_value(y)))
 #define Uint63_div(x,y) (accu = Val_long(uint63_of_value(x) / uint63_of_value(y)))
 #define Uint63_mod(x,y) (accu = Val_long(uint63_of_value(x) % uint63_of_value(y)))
+#define Uint63_divs(x,y) (accu = Val_long(int63_of_value(x) / int63_of_value(y)))
+#define Uint63_mods(x,y) (accu = Val_long(int63_of_value(x) % int63_of_value(y)))
 
 #define Uint63_lxor(x,y) (accu = (value)(((uint64_t)(x) ^ (uint64_t)(y)) | 1))
 #define Uint63_lor(x,y) (accu = (value)((uint64_t)(x) | (uint64_t)(y)))
@@ -46,14 +55,21 @@
   if (uint63_lsl_y__ < (uint64_t) 127) \
     accu = (value)((((uint64_t)(x)-1) << uint63_of_value(uint63_lsl_y__)) | 1); \
   else \
-    accu = uint63_zero; \
+    accu = uint63_zero(); \
   }while(0)
 #define Uint63_lsr(x,y) do{ \
   value uint63_lsl_y__ = (y); \
   if (uint63_lsl_y__ < (uint64_t) 127) \
     accu = (value)(((uint64_t)(x) >> uint63_of_value(uint63_lsl_y__)) | 1); \
   else \
-    accu = uint63_zero; \
+    accu = uint63_zero(); \
+  }while(0)
+#define Uint63_asr(x,y) do{ \
+    value uint63_asr_y__ = (y); \
+    if (uint63_asr_y__ < (uint64_t) 127) \
+      accu = (value)(((int64_t)(x) >> uint63_of_value(uint63_asr_y__)) | 1); \
+    else \
+      accu = uint63_zero(); \
   }while(0)
 
 /* addmuldiv(p,x,y) = x * 2^p + y / 2 ^ (63 - p) */
diff --git a/kernel/cPrimitives.ml b/kernel/cPrimitives.ml
index 5cd91b4e74..6ef0e9fa15 100644
--- a/kernel/cPrimitives.ml
+++ b/kernel/cPrimitives.ml
@@ -8,6 +8,9 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
+(* Note: don't forget to update v_primitive in checker/values.ml if the *)
+(* number of primitives is changed. *)
+
 open Univ
 
 type t =
@@ -18,8 +21,11 @@ type t =
   | Int63mul
   | Int63div
   | Int63mod
+  | Int63divs
+  | Int63mods
   | Int63lsr
   | Int63lsl
+  | Int63asr
   | Int63land
   | Int63lor
   | Int63lxor
@@ -34,7 +40,10 @@ type t =
   | Int63eq
   | Int63lt
   | Int63le
+  | Int63lts
+  | Int63les
   | Int63compare
+  | Int63compares
   | Float64opp
   | Float64abs
   | Float64eq
@@ -68,8 +77,11 @@ let parse = function
   | "int63_mul" -> Int63mul
   | "int63_div" -> Int63div
   | "int63_mod" -> Int63mod
+  | "int63_divs" -> Int63divs
+  | "int63_mods" -> Int63mods
   | "int63_lsr" -> Int63lsr
   | "int63_lsl" -> Int63lsl
+  | "int63_asr" -> Int63asr
   | "int63_land" -> Int63land
   | "int63_lor" -> Int63lor
   | "int63_lxor" -> Int63lxor
@@ -84,7 +96,10 @@ let parse = function
   | "int63_eq" -> Int63eq
   | "int63_lt" -> Int63lt
   | "int63_le" -> Int63le
+  | "int63_lts" -> Int63lts
+  | "int63_les" -> Int63les
   | "int63_compare" -> Int63compare
+  | "int63_compares" -> Int63compares
   | "float64_opp" -> Float64opp
   | "float64_abs" -> Float64abs
   | "float64_eq" -> Float64eq
@@ -163,6 +178,12 @@ let hash = function
   | Arrayset -> 46
   | Arraycopy -> 47
   | Arraylength -> 48
+  | Int63lts -> 49
+  | Int63les -> 50
+  | Int63divs -> 51
+  | Int63mods -> 52
+  | Int63asr -> 53
+  | Int63compares -> 54
 
 (* Should match names in nativevalues.ml *)
 let to_string = function
@@ -173,8 +194,11 @@ let to_string = function
   | Int63mul -> "mul"
   | Int63div -> "div"
   | Int63mod -> "rem"
+  | Int63divs -> "divs"
+  | Int63mods -> "rems"
   | Int63lsr -> "l_sr"
   | Int63lsl -> "l_sl"
+  | Int63asr -> "a_sr"
   | Int63land -> "l_and"
   | Int63lor -> "l_or"
   | Int63lxor -> "l_xor"
@@ -189,7 +213,10 @@ let to_string = function
   | Int63eq -> "eq"
   | Int63lt -> "lt"
   | Int63le -> "le"
+  | Int63lts -> "lts"
+  | Int63les -> "les"
   | Int63compare -> "compare"
+  | Int63compares -> "compares"
   | Float64opp -> "fopp"
   | Float64abs -> "fabs"
   | Float64eq -> "feq"
@@ -271,14 +298,15 @@ let types =
   | Int63head0 | Int63tail0 -> [int_ty; int_ty]
   | Int63add | Int63sub | Int63mul
   | Int63div | Int63mod
-  | Int63lsr | Int63lsl
+  | Int63divs | Int63mods
+  | Int63lsr | Int63lsl | Int63asr
   | Int63land | Int63lor | Int63lxor -> [int_ty; int_ty; int_ty]
   | Int63addc | Int63subc | Int63addCarryC | Int63subCarryC ->
      [int_ty; int_ty; PITT_ind (PIT_carry, int_ty)]
   | Int63mulc | Int63diveucl ->
      [int_ty; int_ty; PITT_ind (PIT_pair, (int_ty, int_ty))]
-  | Int63eq | Int63lt | Int63le -> [int_ty; int_ty; PITT_ind (PIT_bool, ())]
-  | Int63compare -> [int_ty; int_ty; PITT_ind (PIT_cmp, ())]
+  | Int63eq | Int63lt | Int63le | Int63lts | Int63les -> [int_ty; int_ty; PITT_ind (PIT_bool, ())]
+  | Int63compare | Int63compares -> [int_ty; int_ty; PITT_ind (PIT_cmp, ())]
   | Int63div21 ->
      [int_ty; int_ty; int_ty; PITT_ind (PIT_pair, (int_ty, int_ty))]
   | Int63addMulDiv -> [int_ty; int_ty; int_ty; int_ty]
@@ -314,8 +342,11 @@ let params = function
   | Int63mul
   | Int63div
   | Int63mod
+  | Int63divs
+  | Int63mods
   | Int63lsr
   | Int63lsl
+  | Int63asr
   | Int63land
   | Int63lor
   | Int63lxor
@@ -330,7 +361,10 @@ let params = function
   | Int63eq
   | Int63lt
   | Int63le
+  | Int63lts
+  | Int63les
   | Int63compare
+  | Int63compares
   | Float64opp
   | Float64abs
   | Float64eq
@@ -367,8 +401,11 @@ let univs = function
   | Int63mul
   | Int63div
   | Int63mod
+  | Int63divs
+  | Int63mods
   | Int63lsr
   | Int63lsl
+  | Int63asr
   | Int63land
   | Int63lor
   | Int63lxor
@@ -383,7 +420,10 @@ let univs = function
   | Int63eq
   | Int63lt
   | Int63le
+  | Int63lts
+  | Int63les
   | Int63compare
+  | Int63compares
   | Float64opp
   | Float64abs
   | Float64eq
diff --git a/kernel/cPrimitives.mli b/kernel/cPrimitives.mli
index 0db643faf4..de90179726 100644
--- a/kernel/cPrimitives.mli
+++ b/kernel/cPrimitives.mli
@@ -16,8 +16,11 @@ type t =
   | Int63mul
   | Int63div
   | Int63mod
+  | Int63divs
+  | Int63mods
   | Int63lsr
   | Int63lsl
+  | Int63asr
   | Int63land
   | Int63lor
   | Int63lxor
@@ -32,7 +35,10 @@ type t =
   | Int63eq
   | Int63lt
   | Int63le
+  | Int63lts
+  | Int63les
   | Int63compare
+  | Int63compares
   | Float64opp
   | Float64abs
   | Float64eq
diff --git a/kernel/genOpcodeFiles.ml b/kernel/genOpcodeFiles.ml
index bda65956be..20220dd9d2 100644
--- a/kernel/genOpcodeFiles.ml
+++ b/kernel/genOpcodeFiles.ml
@@ -110,6 +110,8 @@ let opcodes =
     "CHECKMULCINT63", 1;
     "CHECKDIVINT63", 1;
     "CHECKMODINT63", 1;
+    "CHECKDIVSINT63", 1;
+    "CHECKMODSINT63", 1;
     "CHECKDIVEUCLINT63", 1;
     "CHECKDIV21INT63", 1;
     "CHECKLXORINT63", 1;
@@ -117,11 +119,15 @@ let opcodes =
     "CHECKLANDINT63", 1;
     "CHECKLSLINT63", 1;
     "CHECKLSRINT63", 1;
+    "CHECKASRINT63", 1;
     "CHECKADDMULDIVINT63", 1;
     "CHECKEQINT63", 1;
     "CHECKLTINT63", 1;
     "CHECKLEINT63", 1;
+    "CHECKLTSINT63", 1;
+    "CHECKLESINT63", 1;
     "CHECKCOMPAREINT63", 1;
+    "CHECKCOMPARESINT63", 1;
     "CHECKHEAD0INT63", 1;
     "CHECKTAIL0INT63", 1;
     "CHECKOPPFLOAT", 1;
diff --git a/kernel/nativevalues.ml b/kernel/nativevalues.ml
index bd6241ae67..c986cb473d 100644
--- a/kernel/nativevalues.ml
+++ b/kernel/nativevalues.ml
@@ -333,6 +333,22 @@ let rem accu x y =
   if is_int x && is_int y then no_check_rem x y
   else accu x y
 
+let no_check_divs x y =
+  mk_uint (Uint63.divs (to_uint x) (to_uint y))
+[@@ocaml.inline always]
+
+let divs accu x y =
+  if is_int x && is_int y then no_check_divs x y
+  else accu x y
+
+let no_check_rems x y =
+  mk_uint (Uint63.rems (to_uint x) (to_uint y))
+[@@ocaml.inline always]
+
+let rems accu x y =
+  if is_int x && is_int y then no_check_rems x y
+  else accu x y
+
 let no_check_l_sr x y =
   mk_uint (Uint63.l_sr (to_uint x) (to_uint y))
 [@@ocaml.inline always]
@@ -349,6 +365,14 @@ let l_sl accu x y =
   if is_int x && is_int y then no_check_l_sl x y
   else accu x y
 
+let no_check_a_sr x y =
+  mk_uint (Uint63.a_sr (to_uint x) (to_uint y))
+[@@ocaml.inline always]
+
+let a_sr accu x y =
+  if is_int x && is_int y then no_check_a_sr x y
+  else accu x y
+
 let no_check_l_and x y =
   mk_uint (Uint63.l_and (to_uint x) (to_uint y))
 [@@ocaml.inline always]
@@ -502,6 +526,22 @@ let le accu x y =
   if is_int x && is_int y then no_check_le x y
   else accu x y
 
+let no_check_lts x y =
+  mk_bool (Uint63.lts (to_uint x) (to_uint y))
+[@@ocaml.inline always]
+
+let lts accu x y =
+  if is_int x && is_int y then no_check_lts x y
+  else accu x y
+
+let no_check_les x y =
+  mk_bool (Uint63.les (to_uint x) (to_uint y))
+[@@ocaml.inline always]
+
+let les accu x y =
+  if is_int x && is_int y then no_check_les x y
+  else accu x y
+
 let no_check_compare x y =
   match Uint63.compare (to_uint x) (to_uint y) with
   | x when x < 0 -> (Obj.magic CmpLt:t)
@@ -512,6 +552,16 @@ let compare accu x y =
   if is_int x && is_int y then no_check_compare x y
   else accu x y
 
+let no_check_compares x y =
+  match Uint63.compares (to_uint x) (to_uint y) with
+  | x when x < 0 -> (Obj.magic CmpLt:t)
+  | 0 -> (Obj.magic CmpEq:t)
+  | _ -> (Obj.magic CmpGt:t)
+
+let compares accu x y =
+  if is_int x && is_int y then no_check_compares x y
+  else accu x y
+
 let print x =
   Printf.fprintf stderr "%s" (Uint63.to_string (to_uint x));
   flush stderr;
diff --git a/kernel/nativevalues.mli b/kernel/nativevalues.mli
index b9b75a9d7c..98cf4219a0 100644
--- a/kernel/nativevalues.mli
+++ b/kernel/nativevalues.mli
@@ -158,9 +158,12 @@ val sub : t -> t -> t -> t
 val mul : t -> t -> t -> t
 val div : t -> t -> t -> t
 val rem : t -> t -> t -> t
+val divs : t -> t -> t -> t
+val rems : t -> t -> t -> t
 
 val l_sr  : t -> t -> t -> t
 val l_sl  : t -> t -> t -> t
+val a_sr  : t -> t -> t -> t
 val l_and : t -> t -> t -> t
 val l_xor : t -> t -> t -> t
 val l_or  : t -> t -> t -> t
@@ -179,7 +182,10 @@ val addMulDiv : t -> t -> t -> t -> t
 val eq      : t -> t -> t -> t
 val lt      : t -> t -> t -> t
 val le      : t -> t -> t -> t
+val lts     : t -> t -> t -> t
+val les     : t -> t -> t -> t
 val compare : t -> t -> t -> t
+val compares : t -> t -> t -> t
 
 val print : t -> t
 
@@ -205,12 +211,21 @@ val no_check_div : t -> t -> t
 val no_check_rem : t -> t -> t
 [@@ocaml.inline always]
 
+val no_check_divs : t -> t -> t
+[@@ocaml.inline always]
+
+val no_check_rems : t -> t -> t
+[@@ocaml.inline always]
+
 val no_check_l_sr  : t -> t -> t
 [@@ocaml.inline always]
 
 val no_check_l_sl  : t -> t -> t
 [@@ocaml.inline always]
 
+val no_check_a_sr  : t -> t -> t
+[@@ocaml.inline always]
+
 val no_check_l_and : t -> t -> t
 [@@ocaml.inline always]
 
@@ -253,8 +268,16 @@ val no_check_lt      : t -> t -> t
 val no_check_le      : t -> t -> t
 [@@ocaml.inline always]
 
+val no_check_lts     : t -> t -> t
+[@@ocaml.inline always]
+
+val no_check_les     : t -> t -> t
+[@@ocaml.inline always]
+
 val no_check_compare : t -> t -> t
 
+val no_check_compares : t -> t -> t
+
 (** Support for machine floating point values *)
 
 val is_float : t -> bool
diff --git a/kernel/primred.ml b/kernel/primred.ml
index f0b4d6d362..23b7e13ab8 100644
--- a/kernel/primred.ml
+++ b/kernel/primred.ml
@@ -223,10 +223,16 @@ struct
       let i1, i2 = get_int2 evd args in E.mkInt env (Uint63.div i1 i2)
     | Int63mod ->
       let i1, i2 = get_int2 evd args in E.mkInt env (Uint63.rem i1 i2)
+    | Int63divs ->
+      let i1, i2 = get_int2 evd args in E.mkInt env (Uint63.divs i1 i2)
+    | Int63mods ->
+      let i1, i2 = get_int2 evd args in E.mkInt env (Uint63.rems i1 i2)
     | Int63lsr ->
       let i1, i2 = get_int2 evd args in E.mkInt env (Uint63.l_sr i1 i2)
     | Int63lsl ->
       let i1, i2 = get_int2 evd args in E.mkInt env (Uint63.l_sl i1 i2)
+    | Int63asr ->
+      let i1, i2 = get_int2 evd args in E.mkInt env (Uint63.a_sr i1 i2)
     | Int63land ->
       let i1, i2 = get_int2 evd args in E.mkInt env (Uint63.l_and i1 i2)
     | Int63lor ->
@@ -276,6 +282,12 @@ struct
     | Int63le ->
       let i1, i2 = get_int2 evd args in
       E.mkBool env (Uint63.le i1 i2)
+    | Int63lts ->
+      let i1, i2 = get_int2 evd args in
+      E.mkBool env (Uint63.lts i1 i2)
+    | Int63les ->
+      let i1, i2 = get_int2 evd args in
+      E.mkBool env (Uint63.les i1 i2)
     | Int63compare ->
       let i1, i2 = get_int2 evd args in
       begin match Uint63.compare i1 i2 with
@@ -283,6 +295,13 @@ struct
         | 0 -> E.mkEq env
         | _ -> E.mkGt env
       end
+    | Int63compares ->
+      let i1, i2 = get_int2 evd args in
+      begin match Uint63.compares i1 i2 with
+        | x when x < 0 ->  E.mkLt env
+        | 0 -> E.mkEq env
+        | _ -> E.mkGt env
+      end
     | Float64opp ->
       let f = get_float1 evd args in E.mkFloat env (Float64.opp f)
     | Float64abs ->
diff --git a/kernel/uint63.mli b/kernel/uint63.mli
index 6b2519918a..ff8d1eefb7 100644
--- a/kernel/uint63.mli
+++ b/kernel/uint63.mli
@@ -48,6 +48,7 @@ val l_xor   : t -> t -> t
 val l_or    : t -> t -> t
 
       (* Arithmetic operations *)
+val a_sr    : t -> t -> t
 val add     : t -> t -> t
 val sub     : t -> t -> t
 val mul     : t -> t -> t
@@ -56,6 +57,10 @@ val rem     : t -> t -> t
 
 val diveucl : t -> t -> t * t
 
+      (* Signed arithmetic opeartions *)
+val divs     : t -> t -> t
+val rems     : t -> t -> t
+
       (* Specific arithmetic operations *)
 val mulc    : t -> t -> t * t
 val addmuldiv : t -> t -> t -> t
@@ -71,6 +76,11 @@ val equal      : t -> t -> bool
 val le      : t -> t -> bool
 val compare : t -> t -> int
 
+      (* signed comparision *)
+val lts      : t -> t -> bool
+val les      : t -> t -> bool
+val compares : t -> t -> int
+
       (* head and tail *)
 val head0   : t -> t
 val tail0   : t -> t
diff --git a/kernel/uint63_31.ml b/kernel/uint63_31.ml
index 4f2cbc4262..9c8401105e 100644
--- a/kernel/uint63_31.ml
+++ b/kernel/uint63_31.ml
@@ -52,6 +52,15 @@ let lt x y =
 let le x y =
   Int64.compare x y <= 0
 
+    (* signed comparison *)
+(* We shift the arguments by 1 to the left so that the top-most bit is interpreted as a sign *)
+(* The zero at the end doesn't change the order (it is stable by multiplication by 2) *)
+let lts x y =
+  Int64.(compare (shift_left x 1) (shift_left y 1)) < 0
+
+let les x y =
+  Int64.(compare (shift_left x 1) (shift_left y 1)) <= 0
+
     (* logical shift *)
 let l_sl x y =
   if le 0L y && lt y 63L then mask63 (Int64.shift_left x (Int64.to_int y)) else 0L
@@ -59,6 +68,12 @@ let l_sl x y =
 let l_sr x y =
   if le 0L y && lt y 63L then Int64.shift_right x (Int64.to_int y) else 0L
 
+    (* arithmetic shift (for sint63) *)
+let a_sr x y =
+  if les 0L y && lts y 63L then
+    mask63 (Int64.shift_right (Int64.shift_left x 1) ((Int64.to_int y) + 1))
+  else 0L
+
 let l_and x y = Int64.logand x y
 let l_or x y = Int64.logor x y
 let l_xor x y = Int64.logxor x y
@@ -86,6 +101,15 @@ let rem x y =
 
 let diveucl x y = (div x y, rem x y)
 
+    (* signed division *)
+let divs x y =
+  if y = 0L then 0L else mask63 Int64.(div (shift_left x 1) (shift_left y 1))
+
+    (* signed modulo *)
+let rems x y =
+  if y = 0L then 0L else
+    Int64.shift_right_logical (Int64.(rem (shift_left x 1) (shift_left y 1))) 1
+
 let addmuldiv p x y =
   l_or (l_sl x p) (l_sr y Int64.(sub (of_int uint_size) p))
 
@@ -139,6 +163,8 @@ let equal (x : t) y = x = y
 
 let compare x y = Int64.compare x y
 
+let compares x y = Int64.(compare (shift_left x 1) (shift_left y 1))
+
 (* Number of leading zeroes *)
 let head0 x =
   let r = ref 0 in
@@ -198,22 +224,30 @@ let () =
   Callback.register "uint63 addcarry" addcarry;
   Callback.register "uint63 addmuldiv" addmuldiv;
   Callback.register "uint63 div" div;
+  Callback.register "uint63 divs" divs;
   Callback.register "uint63 div21_ml" div21;
   Callback.register "uint63 eq" equal;
   Callback.register "uint63 eq0" (equal Int64.zero);
+  Callback.register "uint63 eqm1" (equal (sub zero one));
   Callback.register "uint63 head0" head0;
   Callback.register "uint63 land" l_and;
   Callback.register "uint63 leq" le;
+  Callback.register "uint63 les" les;
   Callback.register "uint63 lor" l_or;
   Callback.register "uint63 lsl" l_sl;
   Callback.register "uint63 lsr" l_sr;
+  Callback.register "uint63 asr" a_sr;
   Callback.register "uint63 lt" lt;
+  Callback.register "uint63 lts" lts;
   Callback.register "uint63 lxor" l_xor;
   Callback.register "uint63 mod" rem;
+  Callback.register "uint63 mods" rems;
   Callback.register "uint63 mul" mul;
   Callback.register "uint63 mulc_ml" mulc;
+  Callback.register "uint63 zero" zero;
   Callback.register "uint63 one" one;
   Callback.register "uint63 sub" sub;
+  Callback.register "uint63 neg" (sub zero);
   Callback.register "uint63 subcarry" subcarry;
   Callback.register "uint63 tail0" tail0;
   Callback.register "uint63 of_float" of_float;
diff --git a/kernel/uint63_63.ml b/kernel/uint63_63.ml
index 8d052d6593..d017dafd3c 100644
--- a/kernel/uint63_63.ml
+++ b/kernel/uint63_63.ml
@@ -53,6 +53,10 @@ let l_sl x y =
 let l_sr x y =
   if 0 <= y && y < 63 then x lsr y else 0
 
+    (* arithmetic shift (for sint63) *)
+let a_sr x y =
+  if 0 <= y && y < 63 then x asr y else 0
+
 let l_and x y = x land y
 [@@ocaml.inline always]
 
@@ -84,6 +88,14 @@ let rem (x : int) (y : int) =
 
 let diveucl x y = (div x y, rem x y)
 
+    (* signed division *)
+let divs (x : int) (y : int) =
+  if y = 0 then 0 else x / y
+
+    (* modulo *)
+let rems (x : int) (y : int) =
+  if y = 0 then 0 else x mod y
+
 let addmuldiv p x y =
   l_or (l_sl x p) (l_sr y (uint_size - p))
 
@@ -96,6 +108,15 @@ let le (x : int) (y : int) =
   (x lxor 0x4000000000000000) <= (y lxor 0x4000000000000000)
 [@@ocaml.inline always]
 
+    (* signed comparison *)
+let lts (x : int) (y : int) =
+  x < y
+[@@ocaml.inline always]
+
+let les (x : int) (y : int) =
+  x <= y
+[@@ocaml.inline always]
+
 let to_int_min n m =
   if lt n m then n else m
 [@@ocaml.inline always]
@@ -175,9 +196,10 @@ let equal (x : int) (y : int) = x = y
 let compare (x:int) (y:int) =
   let x = x lxor 0x4000000000000000 in
   let y = y lxor 0x4000000000000000 in
-  if x > y then 1
-  else if y > x then -1
-  else 0
+  Int.compare x y
+
+let compares (x : int) (y : int) =
+  Int.compare x y
 
     (* head tail *)
 
diff --git a/kernel/vmemitcodes.ml b/kernel/vmemitcodes.ml
index d3af8bf09b..caa263432e 100644
--- a/kernel/vmemitcodes.ml
+++ b/kernel/vmemitcodes.ml
@@ -226,8 +226,11 @@ let check_prim_op = function
   | Int63mul       -> opCHECKMULINT63
   | Int63div       -> opCHECKDIVINT63
   | Int63mod       -> opCHECKMODINT63
+  | Int63divs      -> opCHECKDIVSINT63
+  | Int63mods      -> opCHECKMODSINT63
   | Int63lsr       -> opCHECKLSRINT63
   | Int63lsl       -> opCHECKLSLINT63
+  | Int63asr       -> opCHECKASRINT63
   | Int63land      -> opCHECKLANDINT63
   | Int63lor       -> opCHECKLORINT63
   | Int63lxor      -> opCHECKLXORINT63
@@ -242,7 +245,10 @@ let check_prim_op = function
   | Int63eq        -> opCHECKEQINT63
   | Int63lt        -> opCHECKLTINT63
   | Int63le        -> opCHECKLEINT63
+  | Int63lts       -> opCHECKLTSINT63
+  | Int63les       -> opCHECKLESINT63
   | Int63compare   -> opCHECKCOMPAREINT63
+  | Int63compares  -> opCHECKCOMPARESINT63
   | Float64opp     -> opCHECKOPPFLOAT
   | Float64abs     -> opCHECKABSFLOAT
   | Float64eq      -> opCHECKEQFLOAT