Primitive integers

This work makes it possible to take advantage of a compact
representation for integers in the entire system, as opposed to only
in some reduction machines. It is useful for heavily computational
applications, where even constructing terms is not possible without such
a representation.

Concretely, it replaces part of the retroknowledge machinery with
a primitive construction for integers in terms, and introduces a kind of
FFI which maps constants to operators (on integers). Properties of these
operators are expressed as explicit axioms, whereas they were hidden in
the retroknowledge-based approach.

This has been presented at the Coq workshop and some Coq Working Groups,
and has been used by various groups for STM trace checking,
computational analysis, etc.

Contributions by Guillaume Bertholon and Pierre Roux <Pierre.Roux@onera.fr>

Co-authored-by: Benjamin Grégoire <Benjamin.Gregoire@inria.fr>
Co-authored-by: Vincent Laporte <Vincent.Laporte@fondation-inria.fr>

7 files changed, 589 insertions, 275 deletions

diff --git a/kernel/byterun/coq_fix_code.c b/kernel/byterun/coq_fix_code.c
index be2b05da8d..0865487c98 100644
--- a/kernel/byterun/coq_fix_code.c
+++ b/kernel/byterun/coq_fix_code.c
@@ -36,20 +36,15 @@ void init_arity () {
     arity[PUSHACC6]=arity[PUSHACC7]=arity[ENVACC1]=arity[ENVACC2]=
     arity[ENVACC3]=arity[ENVACC4]=arity[PUSHENVACC1]=arity[PUSHENVACC2]=
     arity[PUSHENVACC3]=arity[PUSHENVACC4]=arity[APPLY1]=arity[APPLY2]=
-    arity[APPLY3]=arity[RESTART]=arity[OFFSETCLOSUREM2]=
+    arity[APPLY3]=arity[APPLY4]=arity[RESTART]=arity[OFFSETCLOSUREM2]=
     arity[OFFSETCLOSURE0]=arity[OFFSETCLOSURE2]=arity[PUSHOFFSETCLOSUREM2]=
     arity[PUSHOFFSETCLOSURE0]=arity[PUSHOFFSETCLOSURE2]=
     arity[GETFIELD0]=arity[GETFIELD1]=arity[SETFIELD0]=arity[SETFIELD1]=
     arity[CONST0]=arity[CONST1]=arity[CONST2]=arity[CONST3]=
     arity[PUSHCONST0]=arity[PUSHCONST1]=arity[PUSHCONST2]=arity[PUSHCONST3]=
     arity[ACCUMULATE]=arity[STOP]=arity[MAKEPROD]= 
-    arity[ADDINT31]=arity[ADDCINT31]=arity[ADDCARRYCINT31]=
-    arity[SUBINT31]=arity[SUBCINT31]=arity[SUBCARRYCINT31]=
-    arity[MULCINT31]=arity[MULINT31]=arity[COMPAREINT31]=
-    arity[DIV21INT31]=arity[DIVINT31]=arity[ADDMULDIVINT31]=
-    arity[HEAD0INT31]=arity[TAIL0INT31]=
-    arity[COMPINT31]=arity[DECOMPINT31]=
-    arity[ORINT31]=arity[ANDINT31]=arity[XORINT31]=0;
+    arity[ADDINT63]=arity[SUBINT63]=arity[LTINT63]=arity[LEINT63]=
+    arity[ISINT]=arity[AREINT2]=0;
   /* instruction with one operand */
   arity[ACC]=arity[PUSHACC]=arity[POP]=arity[ENVACC]=arity[PUSHENVACC]=
     arity[PUSH_RETADDR]=arity[APPLY]=arity[APPTERM1]=arity[APPTERM2]=
@@ -58,10 +53,20 @@ void init_arity () {
     arity[MAKEBLOCK1]=arity[MAKEBLOCK2]=arity[MAKEBLOCK3]=arity[MAKEBLOCK4]=
     arity[MAKEACCU]=arity[CONSTINT]=arity[PUSHCONSTINT]=arity[GRABREC]=
     arity[PUSHFIELDS]=arity[GETFIELD]=arity[SETFIELD]=
-    arity[BRANCH]=arity[ISCONST]=arity[ENSURESTACKCAPACITY]=1;
+    arity[BRANCH]=arity[ENSURESTACKCAPACITY]=
+    arity[CHECKADDINT63]=arity[CHECKADDCINT63]=arity[CHECKADDCARRYCINT63]=
+    arity[CHECKSUBINT63]=arity[CHECKSUBCINT63]=arity[CHECKSUBCARRYCINT63]=
+    arity[CHECKMULINT63]=arity[CHECKMULCINT63]=
+    arity[CHECKDIVINT63]=arity[CHECKMODINT63]=arity[CHECKDIVEUCLINT63]=
+    arity[CHECKDIV21INT63]=
+    arity[CHECKLXORINT63]=arity[CHECKLORINT63]=arity[CHECKLANDINT63]=
+    arity[CHECKLSLINT63]=arity[CHECKLSRINT63]=arity[CHECKADDMULDIVINT63]=
+    arity[CHECKLSLINT63CONST1]=arity[CHECKLSRINT63CONST1]=
+    arity[CHECKEQINT63]=arity[CHECKLTINT63]=arity[CHECKLEINT63]=
+    arity[CHECKCOMPAREINT63]=arity[CHECKHEAD0INT63]=arity[CHECKTAIL0INT63]=1;
   /* instruction with two operands */
   arity[APPTERM]=arity[MAKEBLOCK]=arity[CLOSURE]=
-  arity[ARECONST]=arity[PROJ]=2;
+  arity[PROJ]=2;
   /* instruction with four operands */ 
   arity[MAKESWITCHBLOCK]=4;
   /* instruction with arbitrary operands */
diff --git a/kernel/byterun/coq_fix_code.h b/kernel/byterun/coq_fix_code.h
index 638d6b5ab5..5a233e6178 100644
--- a/kernel/byterun/coq_fix_code.h
+++ b/kernel/byterun/coq_fix_code.h
@@ -29,6 +29,7 @@ void init_arity();
 value coq_tcode_of_code(value code);
 value coq_makeaccu (value i);
 value coq_pushpop (value i);
+value coq_accucond (value i);
 value coq_is_accumulate_code(value code);
 
 #endif /* _COQ_FIX_CODE_ */
diff --git a/kernel/byterun/coq_instruct.h b/kernel/byterun/coq_instruct.h
index d92e85fdf8..c7abedaed6 100644
--- a/kernel/byterun/coq_instruct.h
+++ b/kernel/byterun/coq_instruct.h
@@ -26,7 +26,7 @@ enum instructions {
   ENVACC1, ENVACC2, ENVACC3, ENVACC4, ENVACC,
   PUSHENVACC1, PUSHENVACC2, PUSHENVACC3, PUSHENVACC4, PUSHENVACC,
   PUSH_RETADDR,
-  APPLY, APPLY1, APPLY2, APPLY3,
+  APPLY, APPLY1, APPLY2, APPLY3, APPLY4,
   APPTERM, APPTERM1, APPTERM2, APPTERM3,
   RETURN, RESTART, GRAB, GRABREC, 
   CLOSURE, CLOSUREREC, CLOSURECOFIX,
@@ -46,15 +46,21 @@ enum instructions {
   MAKESWITCHBLOCK, MAKEACCU, MAKEPROD, 
 /* spiwack: */
   BRANCH,
-  ADDINT31, ADDCINT31, ADDCARRYCINT31,
-  SUBINT31, SUBCINT31, SUBCARRYCINT31,
-  MULCINT31, MULINT31, DIV21INT31, DIVINT31,
-  ADDMULDIVINT31, COMPAREINT31, 
-  HEAD0INT31, TAIL0INT31,
-  ISCONST, ARECONST,
-  COMPINT31, DECOMPINT31,
-  ORINT31, ANDINT31, XORINT31,
-/* /spiwack  */
+  CHECKADDINT63, ADDINT63, CHECKADDCINT63, CHECKADDCARRYCINT63,
+  CHECKSUBINT63, SUBINT63, CHECKSUBCINT63, CHECKSUBCARRYCINT63,
+  CHECKMULINT63, CHECKMULCINT63,
+  CHECKDIVINT63, CHECKMODINT63, CHECKDIVEUCLINT63, CHECKDIV21INT63,
+  CHECKLXORINT63, CHECKLORINT63, CHECKLANDINT63,
+  CHECKLSLINT63, CHECKLSRINT63, CHECKADDMULDIVINT63,
+  CHECKLSLINT63CONST1, CHECKLSRINT63CONST1,
+
+  CHECKEQINT63, CHECKLTINT63, LTINT63, CHECKLEINT63, LEINT63,
+  CHECKCOMPAREINT63,
+
+  CHECKHEAD0INT63, CHECKTAIL0INT63,
+
+  ISINT, AREINT2,
+
   STOP
 };
 
diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c
index a944dbb06c..d2c88bffcc 100644
--- a/kernel/byterun/coq_interp.c
+++ b/kernel/byterun/coq_interp.c
@@ -23,6 +23,12 @@
 #include "coq_memory.h" 
 #include "coq_values.h" 
 
+#ifdef ARCH_SIXTYFOUR
+#include "coq_uint63_native.h"
+#else
+#include "coq_uint63_emul.h"
+#endif
+
 /* spiwack: I append here a few macros for value/number manipulation */
 #define uint32_of_value(val) (((uint32_t)(val)) >> 1)
 #define value_of_uint32(i)   ((value)((((uint32_t)(i)) << 1) | 1))
@@ -155,6 +161,38 @@ if (sp - num_args < coq_stack_threshold) {                                     \
 #endif
 #endif
 
+#define CheckInt1() do{                            \
+    if (Is_uint63(accu)) pc++;			   \
+    else{					   \
+      *--sp=accu;				   \
+      accu = Field(coq_global_data, *pc++);	   \
+      goto apply1;				   \
+    }						   \
+  }while(0)
+
+#define CheckInt2() do{    			   \
+    if (Is_uint63(accu) && Is_uint63(sp[0])) pc++;	   \
+    else{					   \
+      *--sp=accu;				   \
+      accu = Field(coq_global_data, *pc++);	   \
+      goto apply2;				   \
+    }						   \
+  }while(0)
+
+
+
+#define CheckInt3() do{						      \
+    if (Is_uint63(accu) && Is_uint63(sp[0]) && Is_uint63(sp[1]) ) pc++;     \
+    else{							      \
+      *--sp=accu;						      \
+      accu = Field(coq_global_data, *pc++);			      \
+      goto apply3;						      \
+    }								      \
+  }while(0)
+
+#define AllocCarry(cond) Alloc_small(accu, 1, (cond)? coq_tag_C1 : coq_tag_C0)
+#define AllocPair() Alloc_small(accu, 2, coq_tag_pair)
+
 /* For signal handling, we hijack some code from the caml runtime */
 
 extern intnat caml_signals_are_pending;
@@ -372,8 +410,10 @@ value coq_interprete
 	goto check_stack;
       }
       Instruct(APPLY1) {
-	value arg1 = sp[0];
+        value arg1;
+      apply1:
 	print_instr("APPLY1");
+        arg1 = sp[0];
 	sp -= 3;
 	sp[0] = arg1;
 	sp[1] = (value)pc;
@@ -388,10 +428,14 @@ value coq_interprete
 	coq_extra_args = 0;
 	goto check_stack;
       }
+
       Instruct(APPLY2) {
-	value arg1 = sp[0];
-	value arg2 = sp[1];
+        value arg1;
+        value arg2;
+      apply2:
 	print_instr("APPLY2");
+        arg1 = sp[0];
+        arg2 = sp[1];
 	sp -= 3;
 	sp[0] = arg1;
 	sp[1] = arg2;
@@ -403,11 +447,16 @@ value coq_interprete
 	coq_extra_args = 1;
 	goto check_stack;
       }
+
       Instruct(APPLY3) {
-	value arg1 = sp[0];
-	value arg2 = sp[1];
-	value arg3 = sp[2];
+        value arg1;
+        value arg2;
+        value arg3;
+      apply3:
 	print_instr("APPLY3");
+        arg1 = sp[0];
+        arg2 = sp[1];
+        arg3 = sp[2];
 	sp -= 3;
 	sp[0] = arg1;
 	sp[1] = arg2;
@@ -420,7 +469,28 @@ value coq_interprete
 	coq_extra_args = 2;
 	goto check_stack;
       }
-      /* Stack checks */
+
+       Instruct(APPLY4) {
+        value arg1 = sp[0];
+        value arg2 = sp[1];
+        value arg3 = sp[2];
+        value arg4 = sp[3];
+        print_instr("APPLY4");
+        sp -= 3;
+        sp[0] = arg1;
+        sp[1] = arg2;
+        sp[2] = arg3;
+        sp[3] = arg4;
+        sp[4] = (value)pc;
+        sp[5] = coq_env;
+        sp[6] = Val_long(coq_extra_args);
+        pc = Code_val(accu);
+        coq_env = accu;
+        coq_extra_args = 3;
+        goto check_stack;
+      }
+
+     /* Stack checks */
       
     check_stack:
       print_instr("check_stack");
@@ -1127,7 +1197,6 @@ value coq_interprete
 	Next;
       }
 
-      /* spiwack: code for interpreting compiled integers */
       Instruct(BRANCH) {
 	/* unconditional branching */
         print_instr("BRANCH");
@@ -1136,338 +1205,339 @@ value coq_interprete
         Next;
       }
 
-      Instruct(ADDINT31) {
+      Instruct(CHECKADDINT63){
+        print_instr("CHECKADDINT63");
+        CheckInt2();
+      }
+      Instruct(ADDINT63) {
         /* Adds the integer in the accumulator with 
            the one ontop of the stack (which is poped)*/
-        print_instr("ADDINT31");
-        accu = 
-           (value)((uint32_t) accu + (uint32_t) *sp++ - 1); 
-        /* nota,unlike CaML we don't want
-           to have a different behavior depending on the 
-           architecture. Thus we cast the operand to uint32 */
+        print_instr("ADDINT63");
+        accu = uint63_add(accu, *sp++);
         Next;
       }
 
-      Instruct (ADDCINT31) {
-	print_instr("ADDCINT31");
+      Instruct (CHECKADDCINT63) {
+        print_instr("CHECKADDCINT63");
+        CheckInt2();
 	/* returns the sum with a carry */
-	uint32_t s;
-	s = (uint32_t)accu + (uint32_t)*sp++ - 1;
-        if( (uint32_t)s < (uint32_t)accu ) {
-          /* carry */
-	  Alloc_small(accu, 1, 2); /* ( _ , arity, tag ) */
-	}
-	else {
-	  /*no carry */
-	  Alloc_small(accu, 1, 1);
-	}
-	Field(accu, 0)=(value)s;
+        value s;
+        s = uint63_add(accu, *sp++);
+        AllocCarry(uint63_lt(s,accu));
+        Field(accu, 0) = s;
 	Next;
       }
 
-      Instruct (ADDCARRYCINT31) {
-	print_instr("ADDCARRYCINT31");
+      Instruct (CHECKADDCARRYCINT63) {
+        print_instr("ADDCARRYCINT63");
+        CheckInt2();
 	/* returns the sum plus one with a carry */
-	uint32_t s;
-	s = (uint32_t)accu + (uint32_t)*sp++ + 1;
-        if( (uint32_t)s <= (uint32_t)accu ) {
-          /* carry */
-	  Alloc_small(accu, 1, 2); /* ( _ , arity, tag ) */
-	}
-	else {
-	  /*no carry */
-	  Alloc_small(accu, 1, 1);
-	}
-	Field(accu, 0)=(value)s;
+        value s;
+        s = uint63_addcarry(accu, *sp++);
+        AllocCarry(uint63_leq(s, accu));
+        Field(accu, 0) = s;
 	Next;
       }
 
-      Instruct (SUBINT31) {
-	print_instr("SUBINT31");
+      Instruct (CHECKSUBINT63) {
+        print_instr("CHECKSUBINT63");
+        CheckInt2();
+      }
+      Instruct (SUBINT63) {
+        print_instr("SUBINT63");
 	/* returns the subtraction */
-	accu = 
-	  (value)((uint32_t) accu - (uint32_t) *sp++ + 1); 
+        accu = uint63_sub(accu, *sp++);
         Next;
       }
 
-      Instruct (SUBCINT31) {
-	print_instr("SUBCINT31");
+      Instruct (CHECKSUBCINT63) {
+        print_instr("SUBCINT63");
+        CheckInt2();
 	/* returns the subtraction with a carry */
-	uint32_t b;
-	uint32_t s;
-	b = (uint32_t)*sp++;
-	s = (uint32_t)accu - b + 1;
-        if( (uint32_t)accu < b ) {
-          /* carry */
-	  Alloc_small(accu, 1, 2); /* ( _ , arity, tag ) */
-	}
-	else {
-	  /*no carry */
-	  Alloc_small(accu, 1, 1);
-	}
-	Field(accu, 0)=(value)s;
+        value b;
+        value s;
+        b = *sp++;
+        s = uint63_sub(accu,b);
+        AllocCarry(uint63_lt(accu,b));
+        Field(accu, 0) = s;
 	Next;
       }
 
-      Instruct (SUBCARRYCINT31) {
-	print_instr("SUBCARRYCINT31");
+      Instruct (CHECKSUBCARRYCINT63) {
+        print_instr("SUBCARRYCINT63");
+        CheckInt2();
 	/* returns the subtraction minus one with a carry */
-	uint32_t b;
-	uint32_t s;
-	b = (uint32_t)*sp++;
-	s = (value)((uint32_t)accu - b - 1);
-        if( (uint32_t)accu <= b ) {
-          /* carry */
-	  Alloc_small(accu, 1, 2); /* ( _ , arity, tag ) */
-	}
-	else {
-	  /*no carry */
-	  Alloc_small(accu, 1, 1);
-	}
-	Field(accu, 0)=(value)s;
+        value b;
+        value s;
+        b = *sp++;
+        s = uint63_subcarry(accu,b);
+        AllocCarry(uint63_leq(accu,b));
+        Field(accu, 0) = s;
 	Next;
       }
 
-      Instruct (MULINT31) {
+      Instruct (CHECKMULINT63) {
+        print_instr("MULINT63");
+        CheckInt2();
 	/* returns the multiplication */
-	print_instr("MULINT31");
-        accu = 
-	  value_of_uint32((uint32_of_value(accu)) * (uint32_of_value(*sp++)));
+        accu = uint63_mul(accu,*sp++);
 	Next;
       }
 
-      Instruct (MULCINT31) {
-        /*returns the multiplication on a double size word
-          (special case for 0) */
-        print_instr("MULCINT31");
-	uint64_t p;
+      Instruct (CHECKMULCINT63) {
+        /*returns the multiplication on a pair */
+        print_instr("MULCINT63");
+        CheckInt2();
         /*accu = 2v+1, *sp=2w+1 ==> p = 2v*w */
-        p = UI64_of_value (accu) * UI64_of_uint32 ((*sp++)^1);
-	if (p == 0) {
-	  accu = (value)1;
+        /* TODO: implement
+        p = I64_mul (UI64_of_value (accu), UI64_of_uint32 ((*sp++)^1));
+        AllocPair(); */
+        /* Field(accu, 0) = (value)(I64_lsr(p,31)|1) ; */ /*higher part*/
+        /* Field(accu, 1) = (value)(I64_to_int32(p)|1); */ /*lower part*/
+        value x = accu;
+        AllocPair();
+        Field(accu, 1) = uint63_mulc(x, *sp++, &Field(accu, 0));
+        Next;
+      }
+
+      Instruct(CHECKDIVINT63) {
+        print_instr("CHEKDIVINT63");
+        CheckInt2();
+        /* spiwack: a priori no need of the NON_STANDARD_DIV_MOD flag
+                    since it probably only concerns negative number.
+                    needs to be checked at this point */
+        value divisor;
+        divisor = *sp++;
+        if (uint63_eq0(divisor)) {
+          accu = divisor;
 	}
 	else {
-          /* the output type is supposed to have a constant constructor
-	     and a non-constant constructor (in that order), the tag
-	     of the non-constant constructor is then 1 */
-	  Alloc_small(accu, 2, 1); /* ( _ , arity, tag ) */
-	  /*unsigned shift*/
-	  Field(accu, 0) = (value)((p >> 31)|1) ;  /*higher part*/
-	  Field(accu, 1) = (value)((uint32_t)p|1); /*lower part*/
-	}
+          accu = uint63_div(accu, divisor);
+        }
 	Next;
       }
 
-      Instruct (DIV21INT31) {
-	print_instr("DIV21INT31");
-	/* spiwack: takes three int31 (the two first ones represent an
-                    int62) and performs the euclidian division of the
-                    int62 by the int31 */
-        uint64_t bigint;
-        bigint = UI64_of_value(accu);
-        bigint = (bigint << 31) | UI64_of_value(*sp++);
-        uint64_t divisor;
-        divisor = UI64_of_value(*sp++);
-        Alloc_small(accu, 2, 1); /* ( _ , arity, tag ) */
-        if (divisor == 0) {
-          Field(accu, 0) = 1; /* 2*0+1 */
-          Field(accu, 1) = 1; /* 2*0+1 */
+      Instruct(CHECKMODINT63) {
+        print_instr("CHEKMODINT63");
+        CheckInt2();
+        value divisor;
+        divisor = *sp++;
+        if (uint63_eq0(divisor)) {
+          accu = divisor;
 	}
-	else {
-	  uint64_t quo, mod;
-	  quo = bigint / divisor;
-	  mod = bigint % divisor;
-          Field(accu, 0) = value_of_uint32((uint32_t)(quo));
-	  Field(accu, 1) = value_of_uint32((uint32_t)(mod));
+        else {
+          accu = uint63_mod(accu,divisor);
 	}
 	Next;
       }
 
-      Instruct (DIVINT31) {
-	print_instr("DIVINT31");
+      Instruct (CHECKDIVEUCLINT63) {
+        print_instr("DIVEUCLINT63");
+        CheckInt2();
         /* spiwack: a priori no need of the NON_STANDARD_DIV_MOD flag
                     since it probably only concerns negative number.
                     needs to be checked at this point */
-        uint32_t divisor;
-        divisor = uint32_of_value(*sp++);
-        if (divisor == 0) { 
+        value divisor;
+        divisor = *sp++;
+        if (uint63_eq0(divisor)) {
           Alloc_small(accu, 2, 1); /* ( _ , arity, tag ) */
-	  Field(accu, 0) = 1; /* 2*0+1 */
-          Field(accu, 1) = 1; /* 2*0+1 */
+          Field(accu, 0) = divisor;
+          Field(accu, 1) = divisor;
         }
         else {
-          uint32_t modulus;
-          modulus = uint32_of_value(accu);
+          value modulus;
+          modulus = accu;
           Alloc_small(accu, 2, 1); /* ( _ , arity, tag ) */
-	  Field(accu, 0) = value_of_uint32(modulus/divisor);
-          Field(accu, 1) = value_of_uint32(modulus%divisor);
+          Field(accu, 0) = uint63_div(modulus,divisor);
+          Field(accu, 1) = uint63_mod(modulus,divisor);
         }
 	Next;
       }
 
-      Instruct (ADDMULDIVINT31) {
-        print_instr("ADDMULDIVINT31");
-        /* higher level shift (does shifts and cycles and such) */
-        uint32_t shiftby;
-        shiftby = uint32_of_value(accu);
-        if (shiftby > 31) {
-          if (shiftby < 62) {
-            sp++;
-	    accu = (value)(((((uint32_t)*sp++)^1) << (shiftby - 31)) | 1);
-          }
-          else {
-            sp+=2;
-            accu = (value)(1);
-          }
+      Instruct (CHECKDIV21INT63) {
+        print_instr("DIV21INT63");
+        CheckInt3();
+        /* spiwack: takes three int31 (the two first ones represent an
+                    int62) and performs the euclidian division of the
+                    int62 by the int31 */
+        /* TODO: implement this
+        bigint = UI64_of_value(accu);
+        bigint = I64_or(I64_lsl(bigint, 31),UI64_of_value(*sp++));
+        uint64 divisor;
+        divisor = UI64_of_value(*sp++);
+        Alloc_small(accu, 2, 1); */ /* ( _ , arity, tag ) */
+        /* if (I64_is_zero (divisor)) {
+           Field(accu, 0) = 1; */ /* 2*0+1 */
+        /* Field(accu, 1) = 1; */ /* 2*0+1 */
+        /* }
+        else {
+          uint64 quo, mod;
+          I64_udivmod(bigint, divisor, &quo, &mod);
+          Field(accu, 0) = value_of_uint32(I64_to_int32(quo));
+          Field(accu, 1) = value_of_uint32(I64_to_int32(mod));
+        } */
+        value bigint; /* TODO: fix */
+        bigint = *sp++; /* TODO: take accu into account */
+        value divisor;
+        divisor = *sp++;
+        if (uint63_eq0(divisor)) {
+          Alloc_small(accu, 2, 1);
+          Field(accu, 0) = divisor;
+          Field(accu, 1) = divisor;
 	}
-        else{
-        /* *sp = 2*x+1 --> accu = 2^(shiftby+1)*x */
-	  accu = (value)((((uint32_t)*sp++)^1) << shiftby);
-        /* accu = 2^(shiftby+1)*x --> 2^(shifby+1)*x+2*y/2^(31-shiftby)+1 */
-        accu = (value)((accu | (((uint32_t)(*sp++)) >> (31-shiftby)))|1);
+        else {
+          value quo, mod;
+          mod = uint63_div21(accu, bigint, divisor, &quo);
+          Alloc_small(accu, 2, 1);
+          Field(accu, 0) = quo;
+          Field(accu, 1) = mod;
 	}
         Next;
       }
 
-      Instruct (COMPAREINT31) {
-	/* returns Eq if equal, Lt if accu is less than *sp, Gt otherwise */
-	/* assumes Inductive _ : _ := Eq | Lt | Gt */
-	print_instr("COMPAREINT31");
-	if ((uint32_t)accu == (uint32_t)*sp) {
-	  accu = 1;  /* 2*0+1 */
-	  sp++;
-	}
-	else{if ((uint32_t)accu < (uint32_t)(*sp++)) {
-	  accu = 3;  /* 2*1+1 */
-	}
-	else{
-	  accu = 5;   /* 2*2+1 */
-	}}
+      Instruct(CHECKLXORINT63) {
+        print_instr("CHECKLXORINT63");
+        CheckInt2();
+        accu = uint63_lxor(accu,*sp++);
         Next;
       }
- 
-      Instruct (HEAD0INT31) {
-	int r = 0;
-        uint32_t x;
-        print_instr("HEAD0INT31");
-	x = (uint32_t) accu;
-        if (!(x & 0xFFFF0000)) { x <<= 16; r += 16; }
-        if (!(x & 0xFF000000)) { x <<= 8;  r += 8; }
-        if (!(x & 0xF0000000)) { x <<= 4;  r += 4; }
-        if (!(x & 0xC0000000)) { x <<= 2;  r += 2; }
-        if (!(x & 0x80000000)) { x <<=1;   r += 1; }
-        if (!(x & 0x80000000)) {           r += 1; }
-        accu = value_of_uint32(r);
+
+      Instruct(CHECKLORINT63) {
+        print_instr("CHECKLORINT63");
+        CheckInt2();
+        accu = uint63_lor(accu,*sp++);
         Next;
       }
-        
-      Instruct (TAIL0INT31) {
-	int r = 0;
-        uint32_t x;
-        print_instr("TAIL0INT31");
-	x = (((uint32_t) accu >> 1) | 0x80000000);
-        if (!(x & 0xFFFF)) { x >>= 16; r += 16; }
-        if (!(x & 0x00FF)) { x >>= 8;  r += 8; }
-        if (!(x & 0x000F)) { x >>= 4;  r += 4; }
-        if (!(x & 0x0003)) { x >>= 2;  r += 2; }
-        if (!(x & 0x0001)) { x >>=1;   r += 1; }
-        if (!(x & 0x0001)) {           r += 1; }
-        accu = value_of_uint32(r);
+
+      Instruct(CHECKLANDINT63) {
+        print_instr("CHECKLANDINT63");
+        CheckInt2();
+        accu = uint63_land(accu,*sp++);
         Next;
       }
 
-      Instruct (ISCONST) {
-        /* Branches if the accu does not contain a constant
-           (i.e., a non-block value) */
-        print_instr("ISCONST");
-        if ((accu & 1) == 0) /* last bit is 0 -> it is a block */
-	  pc +=  *pc;
-        else
-	  pc++;
+      Instruct(CHECKLSLINT63) {
+        print_instr("CHECKLSLINT63");
+        CheckInt2();
+        value p = *sp++;
+        accu = uint63_lsl(accu,p);
         Next;
+      }
 
+      Instruct(CHECKLSRINT63) {
+        print_instr("CHECKLSRINT63");
+        CheckInt2();
+        value p = *sp++;
+        accu = uint63_lsr(accu,p);
+        Next;
       }
 
-      Instruct (ARECONST) {
-        /* Branches if the n first values on the stack are not
-           all constansts */
-        print_instr("ARECONST");
-        int i, n, ok;
-        ok = 1;
-        n = *pc++;
-        for(i=0; i < n; i++) {
-          if ((sp[i] & 1) == 0) {
-	    ok = 0;
-            break;
-          }
+      Instruct(CHECKLSLINT63CONST1) {
+        print_instr("CHECKLSLINT63CONST1");
+        if (Is_uint63(accu)) {
+          pc++;
+          accu = uint63_lsl1(accu);
+          Next;
+        } else {
+          *--sp = uint63_one();
+          *--sp = accu;
+          accu = Field(coq_global_data, *pc++);
+          goto apply2;
         }
-        if(ok) pc++; else pc += *pc;
+      }
+
+      Instruct(CHECKLSRINT63CONST1) {
+        print_instr("CHECKLSRINT63CONST1");
+        if (Is_uint63(accu)) {
+          pc++;
+          accu = uint63_lsr1(accu);
+          Next;
+        } else {
+          *--sp = uint63_one();
+          *--sp = accu;
+          accu = Field(coq_global_data, *pc++);
+          goto apply2;
+        }
+      }
+
+      Instruct (CHECKADDMULDIVINT63) {
+        print_instr("CHECKADDMULDIVINT63");
+        CheckInt3();
+        value x;
+        value y;
+        x = *sp++;
+        y = *sp++;
+        accu = uint63_addmuldiv(accu,x,y);
         Next;
       }
 
-      Instruct (COMPINT31) {
-        /* makes an 31-bit integer out of the accumulator and
-           the 30 first values of the stack 
-           and put it in the accumulator (the accumulator then the 
-           topmost get to be the heavier bits) */
-        print_instr("COMPINT31");
-        int i;
-        /*accu=accu or accu = (value)((unsigned long)1-accu) if bool
-	               is used for the bits */
-        for(i=0; i < 30; i++) {
-	  accu = (value) ((((uint32_t)accu-1) << 1) | *sp++);
-          /* -1 removes the tag bit, << 1 multiplies the value by 2, 
-              | *sp++ pops the last value and add it (no carry involved)
-	      not that it reintroduces a tag bit */
-          /* alternative, if bool is used for the bits :
-	     accu = (value) ((((unsigned long)accu) << 1) & !*sp++); */
+      Instruct (CHECKEQINT63) {
+        print_instr("CHECKEQINT63");
+        CheckInt2();
+        accu = uint63_eq(accu,*sp++) ? coq_true : coq_false;
+        Next;
+      }
+
+     Instruct (CHECKLTINT63) {
+        print_instr("CHECKLTINT63");
+        CheckInt2();
+     }
+     Instruct (LTINT63) {
+       print_instr("LTINT63");
+       accu = uint63_lt(accu,*sp++) ? coq_true : coq_false;
+       Next;
+     }
+
+     Instruct (CHECKLEINT63) {
+       print_instr("CHECKLEINT63");
+       CheckInt2();
+     }
+     Instruct (LEINT63) {
+       print_instr("LEINT63");
+       accu = uint63_leq(accu,*sp++) ? 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 */
+        print_instr("CHECKCOMPAREINT63");
+        CheckInt2();
+        if (uint63_eq(accu,*sp)) {
+          accu = coq_Eq;
+          sp++;
         }
+        else accu = uint63_lt(accu,*sp++) ? coq_Lt : coq_Gt;
         Next;
       }
 
-      Instruct (DECOMPINT31) {
-        /* builds a block out of a 31-bit integer (from the accumulator), 
-           used before cases */
-        int i;
-	value block;
-	print_instr("DECOMPINT31");
-        Alloc_small(block, 31, 1); // Alloc_small(*, size, tag)
-        for(i = 30; i >= 0; i--) {
-          Field(block, i) = (value)(accu & 3); /* two last bits of the accumulator */
-          //Field(block, i) = 3;
-          accu = (value) ((uint32_t)accu >> 1) | 1;  /* last bit must be a one */
-        };
-	accu = block;
+      Instruct (CHECKHEAD0INT63) {
+        print_instr("CHECKHEAD0INT63");
+        CheckInt1();
+        accu = uint63_head0(accu);
         Next;
       }
 
-      Instruct (ORINT31) {
-	/* returns the bitwise or */
-	print_instr("ORINT31");
-        accu =
-	  value_of_uint32((uint32_of_value(accu)) | (uint32_of_value(*sp++)));
-	Next;
+      Instruct (CHECKTAIL0INT63) {
+        print_instr("CHECKTAIL0INT63");
+        CheckInt1();
+        accu = uint63_tail0(accu);
+        Next;
       }
 
-      Instruct (ANDINT31) {
-	/* returns the bitwise and */
-	print_instr("ANDINT31");
-        accu =
-	  value_of_uint32((uint32_of_value(accu)) & (uint32_of_value(*sp++)));
+      Instruct (ISINT){
+        print_instr("ISINT");
+        accu = (Is_uint63(accu)) ? coq_true : coq_false;
 	Next;
       }
 
-      Instruct (XORINT31) {
-	/* returns the bitwise xor */
-	print_instr("XORINT31");
-        accu =
-	  value_of_uint32((uint32_of_value(accu)) ^ (uint32_of_value(*sp++)));
+      Instruct (AREINT2){
+        print_instr("AREINT2");
+        accu = (Is_uint63(accu) && Is_uint63(sp[0])) ? coq_true : coq_false;
+        sp++;
 	Next;
       }
 
-      /*  /spiwack   */
-
-
 
 /* Debugging and machine control */
 
diff --git a/kernel/byterun/coq_uint63_emul.h b/kernel/byterun/coq_uint63_emul.h
new file mode 100644
index 0000000000..5499f124a2
--- /dev/null
+++ b/kernel/byterun/coq_uint63_emul.h
@@ -0,0 +1,97 @@
+# pragma once
+
+# include <caml/callback.h>
+# include <caml/stack.h>
+
+
+#define Is_uint63(v) (Tag_val(v) == Custom_tag)
+
+# define DECLARE_NULLOP(name) \
+value uint63_##name() { \
+  static value* cb = 0; \
+  CAMLparam0(); \
+  if (!cb) cb = caml_named_value("uint63 " #name); \
+  CAMLreturn(*cb); \
+  }
+
+# define DECLARE_UNOP(name) \
+value uint63_##name(value x) { \
+  static value* cb = 0; \
+  CAMLparam1(x); \
+  if (!cb) cb = caml_named_value("uint63 " #name); \
+  CAMLreturn(caml_callback(*cb, x)); \
+  }
+
+# define DECLARE_PREDICATE(name) \
+value uint63_##name(value x) { \
+  static value* cb = 0; \
+  CAMLparam1(x); \
+  if (!cb) cb = caml_named_value("uint63 " #name); \
+  CAMLreturn(Int_val(caml_callback(*cb, x))); \
+  }
+
+# define DECLARE_BINOP(name) \
+value uint63_##name(value x, value y) { \
+  static value* cb = 0; \
+  CAMLparam2(x, y); \
+  if (!cb) cb = caml_named_value("uint63 " #name); \
+  CAMLreturn(caml_callback2(*cb, x, y)); \
+  }
+
+# define DECLARE_RELATION(name) \
+value uint63_##name(value x, value y) { \
+  static value* cb = 0; \
+  CAMLparam2(x, y); \
+  if (!cb) cb = caml_named_value("uint63 " #name); \
+  CAMLreturn(Int_val(caml_callback2(*cb, x, y))); \
+  }
+
+# define DECLARE_TEROP(name) \
+value uint63_##name(value x, value y, value z) { \
+  static value* cb = 0; \
+  CAMLparam3(x, y, z); \
+  if (!cb) cb = caml_named_value("uint63 " #name); \
+  CAMLreturn(caml_callback3(*cb, x, y, z)); \
+  }
+
+
+DECLARE_NULLOP(one)
+DECLARE_BINOP(add)
+DECLARE_BINOP(addcarry)
+DECLARE_TEROP(addmuldiv)
+DECLARE_BINOP(div)
+DECLARE_TEROP(div21_ml)
+DECLARE_RELATION(eq)
+DECLARE_PREDICATE(eq0)
+DECLARE_UNOP(head0)
+DECLARE_BINOP(land)
+DECLARE_RELATION(leq)
+DECLARE_BINOP(lor)
+DECLARE_BINOP(lsl)
+DECLARE_UNOP(lsl1)
+DECLARE_BINOP(lsr)
+DECLARE_UNOP(lsr1)
+DECLARE_RELATION(lt)
+DECLARE_BINOP(lxor)
+DECLARE_BINOP(mod)
+DECLARE_BINOP(mul)
+DECLARE_BINOP(mulc_ml)
+DECLARE_BINOP(sub)
+DECLARE_BINOP(subcarry)
+DECLARE_UNOP(tail0)
+
+value uint63_div21(value x, value y, value z, value* q) {
+  CAMLparam3(x, y, z);
+  CAMLlocal1(qr);
+  qr = uint63_div21_ml(x, y, z);
+  *q = Field(qr, 0);
+  CAMLreturn(Field(qr, 1));
+}
+
+value uint63_mulc(value x, value y, value* h) {
+  CAMLparam2(x, y);
+  CAMLlocal1(hl);
+  hl = uint63_mulc_ml(x, y);
+  *h = Field(hl, 0);
+  CAMLreturn(Field(hl, 1));
+}
diff --git a/kernel/byterun/coq_uint63_native.h b/kernel/byterun/coq_uint63_native.h
new file mode 100644
index 0000000000..92f4dc79bc
--- /dev/null
+++ b/kernel/byterun/coq_uint63_native.h
@@ -0,0 +1,125 @@
+#define Is_uint63(v) (Is_long(v))
+
+#define uint63_of_value(val) ((uint64_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_one() ((value) 3) /* 2*1 + 1 */
+
+#define uint63_eq(x,y) ((x) == (y))
+#define uint63_eq0(x) ((x) == (uint64_t)1)
+#define uint63_lt(x,y) ((uint64_t) (x) < (uint64_t) (y))
+#define uint63_leq(x,y) ((uint64_t) (x) <= (uint64_t) (y))
+
+#define uint63_add(x,y) ((value)((uint64_t) (x) + (uint64_t) (y) - 1))
+#define uint63_addcarry(x,y) ((value)((uint64_t) (x) + (uint64_t) (y) + 1))
+#define uint63_sub(x,y) ((value)((uint64_t) (x) - (uint64_t) (y) + 1))
+#define uint63_subcarry(x,y) ((value)((uint64_t) (x) - (uint64_t) (y) - 1))
+#define uint63_mul(x,y) (Val_long(uint63_of_value(x) * uint63_of_value(y)))
+#define uint63_div(x,y) (Val_long(uint63_of_value(x) / uint63_of_value(y)))
+#define uint63_mod(x,y) (Val_long(uint63_of_value(x) % uint63_of_value(y)))
+
+#define uint63_lxor(x,y) ((value)(((uint64_t)(x) ^ (uint64_t)(y)) | 1))
+#define uint63_lor(x,y) ((value)((uint64_t)(x) | (uint64_t)(y)))
+#define uint63_land(x,y) ((value)((uint64_t)(x) & (uint64_t)(y)))
+
+/* TODO: is + or | better? OCAML uses + */
+/* TODO: is - or ^ better? */
+#define uint63_lsl(x,y) ((y) < (uint64_t) 127 ? ((value)((((uint64_t)(x)-1) << (uint63_of_value(y))) | 1)) : uint63_zero)
+#define uint63_lsr(x,y) ((y) < (uint64_t) 127 ? ((value)(((uint64_t)(x) >> (uint63_of_value(y))) | 1)) : uint63_zero)
+#define uint63_lsl1(x) ((value)((((uint64_t)(x)-1) << 1) +1))
+#define uint63_lsr1(x) ((value)(((uint64_t)(x) >> 1) |1))
+
+/* addmuldiv(p,x,y) = x * 2^p + y / 2 ^ (63 - p) */
+/* (modulo 2^63) for p <= 63 */
+value uint63_addmuldiv(uint64_t p, uint64_t x, uint64_t y) {
+  uint64_t shiftby = uint63_of_value(p);
+  value r = (value)((uint64_t)(x^1) << shiftby);
+  r |= ((uint64_t)y >> (63-shiftby)) | 1;
+  return r;
+}
+
+value uint63_head0(uint64_t x) {
+  int r = 0;
+  if (!(x & 0xFFFFFFFF00000000)) { x <<= 32; r += 32; }
+  if (!(x & 0xFFFF000000000000)) { x <<= 16; r += 16; }
+  if (!(x & 0xFF00000000000000)) { x <<= 8;  r += 8; }
+  if (!(x & 0xF000000000000000)) { x <<= 4;  r += 4; }
+  if (!(x & 0xC000000000000000)) { x <<= 2;  r += 2; }
+  if (!(x & 0x8000000000000000)) { x <<=1;   r += 1; }
+  return Val_int(r);
+}
+
+value uint63_tail0(value x) {
+  int r = 0;
+  x = (uint64_t)x >> 1;
+  if (!(x & 0xFFFFFFFF)) { x >>= 32; r += 32; }
+  if (!(x & 0x0000FFFF)) { x >>= 16; r += 16; }
+  if (!(x & 0x000000FF)) { x >>= 8;  r += 8; }
+  if (!(x & 0x0000000F)) { x >>= 4;  r += 4; }
+  if (!(x & 0x00000003)) { x >>= 2;  r += 2; }
+  if (!(x & 0x00000001)) { x >>=1;   r += 1; }
+  return Val_int(r);
+}
+
+value uint63_mulc(value x, value y, value* h) {
+  x = (uint64_t)x >> 1;
+  y = (uint64_t)y >> 1;
+  uint64_t lx = x & 0xFFFFFFFF;
+  uint64_t ly = y & 0xFFFFFFFF;
+  uint64_t hx = x >> 32;
+  uint64_t hy = y >> 32;
+  uint64_t hr = hx * hy;
+  uint64_t lr = lx * ly;
+  lx *= hy;
+  ly *= hx;
+  hr += (lx >> 32) + (ly >> 32);
+  lx <<= 32;
+  lr += lx;
+  if (lr < lx) { hr++; }
+  ly <<= 32;
+  lr += ly;
+  if (lr < ly) { hr++; }
+  hr = (hr << 1) | (lr >> 63);
+  *h = Val_int(hr);
+  return Val_int(lr);
+}
+
+#define lt128(xh,xl,yh,yl) (uint63_lt(xh,yh) || (uint63_eq(xh,yh) && uint63_lt(xl,yl)))
+#define le128(xh,xl,yh,yl) (uint63_lt(xh,yh) || (uint63_eq(xh,yh) && uint63_leq(xl,yl)))
+
+value uint63_div21(value xh, value xl, value y, value* q) {
+  xh = (uint64_t)xh >> 1;
+  xl = ((uint64_t)xl >> 1) | ((uint64_t)xh << 63);
+  xh = (uint64_t)xh >> 1;
+  uint64_t maskh = 0;
+  uint64_t maskl = 1;
+  uint64_t dh = 0;
+  uint64_t dl = (uint64_t)y >> 1;
+  int cmp = 1;
+  while (dh >= 0 && cmp) {
+    cmp = lt128(dh,dl,xh,xl);
+    dh = (dh << 1) | (dl >> 63);
+    dl = dl << 1;
+    maskh = (maskh << 1) | (maskl >> 63);
+    maskl = maskl << 1;
+  }
+  uint64_t remh = xh;
+  uint64_t reml = xl;
+  uint64_t quotient = 0;
+  while (maskh | maskl) {
+    if (le128(dh,dl,remh,reml)) {
+      quotient = quotient | maskl;
+      if (uint63_lt(reml,dl)) {remh = remh - dh - 1;} else {remh = remh - dh;}
+      reml = reml - dl;
+    }
+    maskl = (maskl >> 1) | (maskh << 63);
+    maskh = maskh >> 1;
+    dl = (dl >> 1) | (dh << 63);
+    dh = dh >> 1;
+  }
+  *q = Val_int(quotient);
+  return Val_int(reml);
+}
diff --git a/kernel/byterun/coq_values.h b/kernel/byterun/coq_values.h
index bb0f0eb5e4..0cf6ccf532 100644
--- a/kernel/byterun/coq_values.h
+++ b/kernel/byterun/coq_values.h
@@ -28,6 +28,16 @@
 
 /* Les blocs accumulate */
 #define Is_accu(v) (Is_block(v) && (Tag_val(v) == Accu_tag))
-
 #define IS_EVALUATED_COFIX(v) (Is_accu(v) && Is_block(Field(v,1)) && (Tag_val(Field(v,1)) == ATOM_COFIXEVALUATED_TAG))
+
+/* */
+#define coq_tag_C1 2
+#define coq_tag_C0 1
+#define coq_tag_pair 1
+#define coq_true Val_int(0)
+#define coq_false Val_int(1)
+#define coq_Eq Val_int(0)
+#define coq_Lt Val_int(1)
+#define coq_Gt Val_int(2)
+
 #endif /* _COQ_VALUES_ */