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>

28 files changed, 595 insertions, 0 deletions

diff --git a/test-suite/arithmetic/add.v b/test-suite/arithmetic/add.v
new file mode 100644
index 0000000000..fb7eb1d53c
--- /dev/null
+++ b/test-suite/arithmetic/add.v
@@ -0,0 +1,18 @@
+Require Import Int63.
+
+Set Implicit Arguments.
+
+Open Scope int63_scope.
+
+Check (eq_refl : 2 + 3 = 5).
+Check (eq_refl 5 <: 2 + 3 = 5).
+Check (eq_refl 5 <<: 2 + 3 = 5).
+
+Definition compute1 := Eval compute in 2 + 3.
+Check (eq_refl compute1 : 5 = 5).
+
+Check (eq_refl : 9223372036854775807 + 1 = 0).
+Check (eq_refl 0 <: 9223372036854775807 + 1 = 0).
+Check (eq_refl 0 <<: 9223372036854775807 + 1 = 0).
+Definition compute2 := Eval compute in 9223372036854775807 + 1.
+Check (eq_refl compute2 : 0 = 0).
diff --git a/test-suite/arithmetic/addc.v b/test-suite/arithmetic/addc.v
new file mode 100644
index 0000000000..432aec0291
--- /dev/null
+++ b/test-suite/arithmetic/addc.v
@@ -0,0 +1,17 @@
+Require Import Int63.
+
+Set Implicit Arguments.
+
+Open Scope int63_scope.
+
+Check (eq_refl : 2 +c 3 = C0 5).
+Check (eq_refl (C0 5) <: 2 +c 3 = C0 5).
+Check (eq_refl (C0 5) <<: 2 +c 3 = C0 5).
+Definition compute1 := Eval compute in 2 +c 3.
+Check (eq_refl compute1 : C0 5 = C0 5).
+
+Check (eq_refl : 9223372036854775807 +c 2 = C1 1).
+Check (eq_refl (C1 1) <: 9223372036854775807 +c 2 = C1 1).
+Check (eq_refl (C1 1) <<: 9223372036854775807 +c 2 = C1 1).
+Definition compute2 := Eval compute in 9223372036854775807 +c 2.
+Check (eq_refl compute2 : C1 1 = C1 1).
diff --git a/test-suite/arithmetic/addcarryc.v b/test-suite/arithmetic/addcarryc.v
new file mode 100644
index 0000000000..a4430769ca
--- /dev/null
+++ b/test-suite/arithmetic/addcarryc.v
@@ -0,0 +1,17 @@
+Require Import Int63.
+
+Set Implicit Arguments.
+
+Open Scope int63_scope.
+
+Check (eq_refl : addcarryc 2 3 = C0 6).
+Check (eq_refl (C0 6) <: addcarryc 2 3 = C0 6).
+Check (eq_refl (C0 6) <<: addcarryc 2 3 = C0 6).
+Definition compute1 := Eval compute in addcarryc 2 3.
+Check (eq_refl compute1 : C0 6 = C0 6).
+
+Check (eq_refl : addcarryc 9223372036854775807 2 = C1 2).
+Check (eq_refl (C1 2) <: addcarryc 9223372036854775807 2 = C1 2).
+Check (eq_refl (C1 2) <<: addcarryc 9223372036854775807 2 = C1 2).
+Definition compute2 := Eval compute in addcarryc 9223372036854775807 2.
+Check (eq_refl compute2 : C1 2 = C1 2).
diff --git a/test-suite/arithmetic/addmuldiv.v b/test-suite/arithmetic/addmuldiv.v
new file mode 100644
index 0000000000..72b0164b49
--- /dev/null
+++ b/test-suite/arithmetic/addmuldiv.v
@@ -0,0 +1,12 @@
+Require Import Int63.
+
+Set Implicit Arguments.
+
+Open Scope int63_scope.
+
+Check (eq_refl : addmuldiv 32 3 5629499534213120 = 12887523328).
+Check (eq_refl 12887523328 <: addmuldiv 32 3 5629499534213120 = 12887523328).
+Check (eq_refl 12887523328 <<: addmuldiv 32 3 5629499534213120 = 12887523328).
+
+Definition compute2 := Eval compute in addmuldiv 32 3 5629499534213120.
+Check (eq_refl compute2 : 12887523328 = 12887523328).
diff --git a/test-suite/arithmetic/compare.v b/test-suite/arithmetic/compare.v
new file mode 100644
index 0000000000..a8d1ea1226
--- /dev/null
+++ b/test-suite/arithmetic/compare.v
@@ -0,0 +1,23 @@
+Require Import Int63.
+
+Set Implicit Arguments.
+
+Open Scope int63_scope.
+
+Check (eq_refl : 1 ?= 1 = Eq).
+Check (eq_refl Eq <: 1 ?= 1 = Eq).
+Check (eq_refl Eq <<: 1 ?= 1 = Eq).
+Definition compute1 := Eval compute in 1 ?= 1.
+Check (eq_refl compute1 : Eq = Eq).
+
+Check (eq_refl : 1 ?= 2 = Lt).
+Check (eq_refl Lt <: 1 ?= 2 = Lt).
+Check (eq_refl Lt <<: 1 ?= 2 = Lt).
+Definition compute2 := Eval compute in 1 ?= 2.
+Check (eq_refl compute2 : Lt = Lt).
+
+Check (eq_refl : 9223372036854775807 ?= 0 = Gt).
+Check (eq_refl Gt <: 9223372036854775807 ?= 0 = Gt).
+Check (eq_refl Gt <<: 9223372036854775807 ?= 0 = Gt).
+Definition compute3 := Eval compute in 9223372036854775807 ?= 0.
+Check (eq_refl compute3 : Gt = Gt).
diff --git a/test-suite/arithmetic/div.v b/test-suite/arithmetic/div.v
new file mode 100644
index 0000000000..0ee0b91580
--- /dev/null
+++ b/test-suite/arithmetic/div.v
@@ -0,0 +1,17 @@
+Require Import Int63.
+
+Set Implicit Arguments.
+
+Open Scope int63_scope.
+
+Check (eq_refl : 6 / 3 = 2).
+Check (eq_refl 2 <: 6 / 3 = 2).
+Check (eq_refl 2 <<: 6 / 3 = 2).
+Definition compute1 := Eval compute in 6 / 3.
+Check (eq_refl compute1 : 2 = 2).
+
+Check (eq_refl : 3 / 2 = 1).
+Check (eq_refl 1 <: 3 / 2 = 1).
+Check (eq_refl 1 <<: 3 / 2 = 1).
+Definition compute2 := Eval compute in 3 / 2.
+Check (eq_refl compute2 : 1 = 1).
diff --git a/test-suite/arithmetic/diveucl.v b/test-suite/arithmetic/diveucl.v
new file mode 100644
index 0000000000..8f88a0f356
--- /dev/null
+++ b/test-suite/arithmetic/diveucl.v
@@ -0,0 +1,17 @@
+Require Import Int63.
+
+Set Implicit Arguments.
+
+Open Scope int63_scope.
+
+Check (eq_refl : diveucl 6 3 = (2,0)).
+Check (eq_refl (2,0) <: diveucl 6 3 = (2,0)).
+Check (eq_refl (2,0) <<: diveucl 6 3 = (2,0)).
+Definition compute1 := Eval compute in diveucl 6 3.
+Check (eq_refl compute1 : (2,0) = (2,0)).
+
+Check (eq_refl : diveucl 5 3 = (1,2)).
+Check (eq_refl (1,2) <: diveucl 5 3 = (1,2)).
+Check (eq_refl (1,2) <<: diveucl 5 3 = (1,2)).
+Definition compute2 := Eval compute in diveucl 5 3.
+Check (eq_refl compute2 : (1,2) = (1,2)).
diff --git a/test-suite/arithmetic/diveucl_21.v b/test-suite/arithmetic/diveucl_21.v
new file mode 100644
index 0000000000..7e12a08906
--- /dev/null
+++ b/test-suite/arithmetic/diveucl_21.v
@@ -0,0 +1,17 @@
+Require Import Int63.
+
+Set Implicit Arguments.
+
+Open Scope int63_scope.
+
+Check (eq_refl : diveucl_21 1 1 2 = (4611686018427387904,1)).
+Check (eq_refl (4611686018427387904,1) <: diveucl_21 1 1 2 = (4611686018427387904,1)).
+Check (eq_refl (4611686018427387904,1) <<: diveucl_21 1 1 2 = (4611686018427387904,1)).
+Definition compute1 := Eval compute in diveucl_21 1 1 2.
+Check (eq_refl compute1 : (4611686018427387904,1) = (4611686018427387904,1)).
+
+Check (eq_refl : diveucl_21 3 1 2 = (4611686018427387904, 1)).
+Check (eq_refl (4611686018427387904, 1) <: diveucl_21 3 1 2 = (4611686018427387904, 1)).
+Check (eq_refl (4611686018427387904, 1) <<: diveucl_21 3 1 2 = (4611686018427387904, 1)).
+Definition compute2 := Eval compute in diveucl_21 3 1 2.
+Check (eq_refl compute2 : (4611686018427387904, 1) = (4611686018427387904, 1)).
diff --git a/test-suite/arithmetic/eqb.v b/test-suite/arithmetic/eqb.v
new file mode 100644
index 0000000000..dcc0b71f6d
--- /dev/null
+++ b/test-suite/arithmetic/eqb.v
@@ -0,0 +1,17 @@
+Require Import Int63.
+
+Set Implicit Arguments.
+
+Open Scope int63_scope.
+
+Check (eq_refl : 1 == 1 = true).
+Check (eq_refl true <: 1 == 1 = true).
+Check (eq_refl true <<: 1 == 1 = true).
+Definition compute1 := Eval compute in 1 == 1.
+Check (eq_refl compute1 : true = true).
+
+Check (eq_refl : 9223372036854775807 == 0 = false).
+Check (eq_refl false <: 9223372036854775807 == 0 = false).
+Check (eq_refl false <<: 9223372036854775807 == 0 = false).
+Definition compute2 := Eval compute in 9223372036854775807 == 0.
+Check (eq_refl compute2 : false = false).
diff --git a/test-suite/arithmetic/head0.v b/test-suite/arithmetic/head0.v
new file mode 100644
index 0000000000..f4234d2605
--- /dev/null
+++ b/test-suite/arithmetic/head0.v
@@ -0,0 +1,23 @@
+Require Import Int63.
+
+Set Implicit Arguments.
+
+Open Scope int63_scope.
+
+Check (eq_refl : head0 3 = 61).
+Check (eq_refl 61 <: head0 3 = 61).
+Check (eq_refl 61 <<: head0 3 = 61).
+Definition compute1 := Eval compute in head0 3.
+Check (eq_refl compute1 : 61 = 61).
+
+Check (eq_refl : head0 4611686018427387904 = 0).
+Check (eq_refl 0 <: head0 4611686018427387904 = 0).
+Check (eq_refl 0 <<: head0 4611686018427387904 = 0).
+Definition compute2 := Eval compute in head0 4611686018427387904.
+Check (eq_refl compute2 : 0 = 0).
+
+Check (eq_refl : head0 0 = 63).
+Check (eq_refl 63 <: head0 0 = 63).
+Check (eq_refl 63 <<: head0 0 = 63).
+Definition compute3 := Eval compute in head0 0.
+Check (eq_refl compute3 : 63 = 63).
diff --git a/test-suite/arithmetic/isint.v b/test-suite/arithmetic/isint.v
new file mode 100644
index 0000000000..c215caa878
--- /dev/null
+++ b/test-suite/arithmetic/isint.v
@@ -0,0 +1,50 @@
+(* This file tests the check that arithmetic operations use to know if their
+arguments are ground. The various test cases correspond to possible
+optimizations of these tests made by the compiler. *)
+Require Import Int63.
+
+Set Implicit Arguments.
+
+Open Scope int63_scope.
+
+Section test.
+
+Variable m n : int.
+
+Check (eq_refl : (fun x => x + 3) m = m + 3).
+Check (eq_refl (m + 3) <: (fun x => x + 3) m = m + 3).
+Check (eq_refl (m + 3) <<: (fun x => x + 3) m = m + 3).
+Definition compute1 := Eval compute in (fun x => x + 3) m.
+Check (eq_refl compute1 : m + 3 = m + 3).
+
+Check (eq_refl : (fun x => 3 + x) m = 3 + m).
+Check (eq_refl (3 + m) <: (fun x => 3 + x) m = 3 + m).
+Check (eq_refl (3 + m) <<: (fun x => 3 + x) m = 3 + m).
+Definition compute2 := Eval compute in (fun x => 3 + x) m.
+Check (eq_refl compute2 : 3 + m = 3 + m).
+
+Check (eq_refl : (fun x y => x + y) m n = m + n).
+Check (eq_refl (m + n) <: (fun x y => x + y) m n = m + n).
+Check (eq_refl (m + n) <<: (fun x y => x + y) m n = m + n).
+Definition compute3 := Eval compute in (fun x y => x + y) m n.
+Check (eq_refl compute3 : m + n = m + n).
+
+Check (eq_refl : (fun x y => x + y) 2 3 = 5).
+Check (eq_refl 5 <: (fun x y => x + y) 2 3 = 5).
+Check (eq_refl 5 <<: (fun x y => x + y) 2 3 = 5).
+Definition compute4 := Eval compute in (fun x y => x + y) 2 3.
+Check (eq_refl compute4 : 5 = 5).
+
+Check (eq_refl : (fun x => x + x) m = m + m).
+Check (eq_refl (m + m) <: (fun x => x + x) m = m + m).
+Check (eq_refl (m + m) <<: (fun x => x + x) m = m + m).
+Definition compute5 := Eval compute in (fun x => x + x) m.
+Check (eq_refl compute5 : m + m = m + m).
+
+Check (eq_refl : (fun x => x + x) 2 = 4).
+Check (eq_refl 4 <: (fun x => x + x) 2 = 4).
+Check (eq_refl 4 <<: (fun x => x + x) 2 = 4).
+Definition compute6 := Eval compute in (fun x => x + x) 2.
+Check (eq_refl compute6 : 4 = 4).
+
+End test.
diff --git a/test-suite/arithmetic/land.v b/test-suite/arithmetic/land.v
new file mode 100644
index 0000000000..0ea6fd90b6
--- /dev/null
+++ b/test-suite/arithmetic/land.v
@@ -0,0 +1,29 @@
+Require Import Int63.
+
+Set Implicit Arguments.
+
+Open Scope int63_scope.
+
+Check (eq_refl : 0 land 0 = 0).
+Check (eq_refl 0 <: 0 land 0 = 0).
+Check (eq_refl 0 <<: 0 land 0 = 0).
+Definition compute1 := Eval compute in 0 land 0.
+Check (eq_refl compute1 : 0 = 0).
+
+Check (eq_refl : 9223372036854775807 land 0 = 0).
+Check (eq_refl 0 <: 9223372036854775807 land 0 = 0).
+Check (eq_refl 0 <<: 9223372036854775807 land 0 = 0).
+Definition compute2 := Eval compute in 9223372036854775807 land 0.
+Check (eq_refl compute2 : 0 = 0).
+
+Check (eq_refl : 0 land 9223372036854775807 = 0).
+Check (eq_refl 0 <: 0 land 9223372036854775807 = 0).
+Check (eq_refl 0 <<: 0 land 9223372036854775807 = 0).
+Definition compute3 := Eval compute in 0 land 9223372036854775807.
+Check (eq_refl compute3 : 0 = 0).
+
+Check (eq_refl : 9223372036854775807 land 9223372036854775807 = 9223372036854775807).
+Check (eq_refl 9223372036854775807 <: 9223372036854775807 land 9223372036854775807 = 9223372036854775807).
+Check (eq_refl 9223372036854775807 <<: 9223372036854775807 land 9223372036854775807 = 9223372036854775807).
+Definition compute4 := Eval compute in 9223372036854775807 land 9223372036854775807.
+Check (eq_refl compute4 : 9223372036854775807 = 9223372036854775807).
diff --git a/test-suite/arithmetic/leb.v b/test-suite/arithmetic/leb.v
new file mode 100644
index 0000000000..5354919978
--- /dev/null
+++ b/test-suite/arithmetic/leb.v
@@ -0,0 +1,23 @@
+Require Import Int63.
+
+Set Implicit Arguments.
+
+Open Scope int63_scope.
+
+Check (eq_refl : 1 <= 1 = true).
+Check (eq_refl true <: 1 <= 1 = true).
+Check (eq_refl true <<: 1 <= 1 = true).
+Definition compute1 := Eval compute in 1 <= 1.
+Check (eq_refl compute1 : true = true).
+
+Check (eq_refl : 1 <= 2 = true).
+Check (eq_refl true <: 1 <= 2 = true).
+Check (eq_refl true <<: 1 <= 2 = true).
+Definition compute2 := Eval compute in 1 <= 2.
+Check (eq_refl compute2 : true = true).
+
+Check (eq_refl : 9223372036854775807 <= 0 = false).
+Check (eq_refl false <: 9223372036854775807 <= 0 = false).
+Check (eq_refl false <<: 9223372036854775807 <= 0 = false).
+Definition compute3 := Eval compute in 9223372036854775807 <= 0.
+Check (eq_refl compute3 : false = false).
diff --git a/test-suite/arithmetic/lor.v b/test-suite/arithmetic/lor.v
new file mode 100644
index 0000000000..9c3b85c054
--- /dev/null
+++ b/test-suite/arithmetic/lor.v
@@ -0,0 +1,29 @@
+Require Import Int63.
+
+Set Implicit Arguments.
+
+Open Scope int63_scope.
+
+Check (eq_refl : 0 lor 0 = 0).
+Check (eq_refl 0 <: 0 lor 0 = 0).
+Check (eq_refl 0 <<: 0 lor 0 = 0).
+Definition compute1 := Eval compute in 0 lor 0.
+Check (eq_refl compute1 : 0 = 0).
+
+Check (eq_refl : 9223372036854775807 lor 0 = 9223372036854775807).
+Check (eq_refl 9223372036854775807 <: 9223372036854775807 lor 0 = 9223372036854775807).
+Check (eq_refl 9223372036854775807 <<: 9223372036854775807 lor 0 = 9223372036854775807).
+Definition compute2 := Eval compute in 9223372036854775807 lor 0.
+Check (eq_refl compute2 : 9223372036854775807 = 9223372036854775807).
+
+Check (eq_refl : 0 lor 9223372036854775807 = 9223372036854775807).
+Check (eq_refl 9223372036854775807 <: 0 lor 9223372036854775807 = 9223372036854775807).
+Check (eq_refl 9223372036854775807 <<: 0 lor 9223372036854775807 = 9223372036854775807).
+Definition compute3 := Eval compute in 0 lor 9223372036854775807.
+Check (eq_refl compute3 : 9223372036854775807 = 9223372036854775807).
+
+Check (eq_refl : 9223372036854775807 lor 9223372036854775807 = 9223372036854775807).
+Check (eq_refl 9223372036854775807 <: 9223372036854775807 lor 9223372036854775807 = 9223372036854775807).
+Check (eq_refl 9223372036854775807 <<: 9223372036854775807 lor 9223372036854775807 = 9223372036854775807).
+Definition compute4 := Eval compute in 9223372036854775807 lor 9223372036854775807.
+Check (eq_refl compute4 : 9223372036854775807 = 9223372036854775807).
diff --git a/test-suite/arithmetic/lsl.v b/test-suite/arithmetic/lsl.v
new file mode 100644
index 0000000000..70f3b90140
--- /dev/null
+++ b/test-suite/arithmetic/lsl.v
@@ -0,0 +1,23 @@
+Require Import Int63.
+
+Set Implicit Arguments.
+
+Open Scope int63_scope.
+
+Check (eq_refl : 3 << 61 = 6917529027641081856).
+Check (eq_refl 6917529027641081856 <: 3 << 61 = 6917529027641081856).
+Check (eq_refl 6917529027641081856 <<: 3 << 61 = 6917529027641081856).
+Definition compute1 := Eval compute in 3 << 61.
+Check (eq_refl compute1 : 6917529027641081856 = 6917529027641081856).
+
+Check (eq_refl : 2 << 62 = 0).
+Check (eq_refl 0 <: 2 << 62 = 0).
+Check (eq_refl 0 <<: 2 << 62 = 0).
+Definition compute2 := Eval compute in 2 << 62.
+Check (eq_refl compute2 : 0 = 0).
+
+Check (eq_refl : 9223372036854775807 << 64 = 0).
+Check (eq_refl 0 <: 9223372036854775807 << 64 = 0).
+Check (eq_refl 0 <<: 9223372036854775807 << 64 = 0).
+Definition compute3 := Eval compute in 9223372036854775807 << 64.
+Check (eq_refl compute3 : 0 = 0).
diff --git a/test-suite/arithmetic/lsr.v b/test-suite/arithmetic/lsr.v
new file mode 100644
index 0000000000..c36c24e237
--- /dev/null
+++ b/test-suite/arithmetic/lsr.v
@@ -0,0 +1,23 @@
+Require Import Int63.
+
+Set Implicit Arguments.
+
+Open Scope int63_scope.
+
+Check (eq_refl : 6917529027641081856 >> 61 = 3).
+Check (eq_refl 3 <: 6917529027641081856 >> 61 = 3).
+Check (eq_refl 3 <<: 6917529027641081856 >> 61 = 3).
+Definition compute1 := Eval compute in 6917529027641081856 >> 61.
+Check (eq_refl compute1 : 3 = 3).
+
+Check (eq_refl : 2305843009213693952 >> 62 = 0).
+Check (eq_refl 0 <: 2305843009213693952 >> 62 = 0).
+Check (eq_refl 0 <<: 2305843009213693952 >> 62 = 0).
+Definition compute2 := Eval compute in 2305843009213693952 >> 62.
+Check (eq_refl compute2 : 0 = 0).
+
+Check (eq_refl : 9223372036854775807 >> 64 = 0).
+Check (eq_refl 0 <: 9223372036854775807 >> 64 = 0).
+Check (eq_refl 0 <<: 9223372036854775807 >> 64 = 0).
+Definition compute3 := Eval compute in 9223372036854775807 >> 64.
+Check (eq_refl compute3 : 0 = 0).
diff --git a/test-suite/arithmetic/ltb.v b/test-suite/arithmetic/ltb.v
new file mode 100644
index 0000000000..7ae5ac6493
--- /dev/null
+++ b/test-suite/arithmetic/ltb.v
@@ -0,0 +1,23 @@
+Require Import Int63.
+
+Set Implicit Arguments.
+
+Open Scope int63_scope.
+
+Check (eq_refl : 1 < 1 = false).
+Check (eq_refl false <: 1 < 1 = false).
+Check (eq_refl false <<: 1 < 1 = false).
+Definition compute1 := Eval compute in 1 < 1.
+Check (eq_refl compute1 : false = false).
+
+Check (eq_refl : 1 < 2 = true).
+Check (eq_refl true <: 1 < 2 = true).
+Check (eq_refl true <<: 1 < 2 = true).
+Definition compute2 := Eval compute in 1 < 2.
+Check (eq_refl compute2 : true = true).
+
+Check (eq_refl : 9223372036854775807 < 0 = false).
+Check (eq_refl false <: 9223372036854775807 < 0 = false).
+Check (eq_refl false <<: 9223372036854775807 < 0 = false).
+Definition compute3 := Eval compute in 9223372036854775807 < 0.
+Check (eq_refl compute3 : false = false).
diff --git a/test-suite/arithmetic/lxor.v b/test-suite/arithmetic/lxor.v
new file mode 100644
index 0000000000..b453fc7697
--- /dev/null
+++ b/test-suite/arithmetic/lxor.v
@@ -0,0 +1,29 @@
+Require Import Int63.
+
+Set Implicit Arguments.
+
+Open Scope int63_scope.
+
+Check (eq_refl : 0 lxor 0 = 0).
+Check (eq_refl 0 <: 0 lxor 0 = 0).
+Check (eq_refl 0 <<: 0 lxor 0 = 0).
+Definition compute1 := Eval compute in 0 lxor 0.
+Check (eq_refl compute1 : 0 = 0).
+
+Check (eq_refl : 9223372036854775807 lxor 0 = 9223372036854775807).
+Check (eq_refl 9223372036854775807 <: 9223372036854775807 lxor 0 = 9223372036854775807).
+Check (eq_refl 9223372036854775807 <<: 9223372036854775807 lxor 0 = 9223372036854775807).
+Definition compute2 := Eval compute in 9223372036854775807 lxor 0.
+Check (eq_refl compute2 : 9223372036854775807 = 9223372036854775807).
+
+Check (eq_refl : 0 lxor 9223372036854775807 = 9223372036854775807).
+Check (eq_refl 9223372036854775807 <: 0 lxor 9223372036854775807 = 9223372036854775807).
+Check (eq_refl 9223372036854775807 <<: 0 lxor 9223372036854775807 = 9223372036854775807).
+Definition compute3 := Eval compute in 0 lxor 9223372036854775807.
+Check (eq_refl compute3 : 9223372036854775807 = 9223372036854775807).
+
+Check (eq_refl : 9223372036854775807 lxor 9223372036854775807 = 0).
+Check (eq_refl 0 <: 9223372036854775807 lxor 9223372036854775807 = 0).
+Check (eq_refl 0 <<: 9223372036854775807 lxor 9223372036854775807 = 0).
+Definition compute4 := Eval compute in 9223372036854775807 lxor 9223372036854775807.
+Check (eq_refl compute4 : 0 = 0).
diff --git a/test-suite/arithmetic/mod.v b/test-suite/arithmetic/mod.v
new file mode 100644
index 0000000000..5307eed493
--- /dev/null
+++ b/test-suite/arithmetic/mod.v
@@ -0,0 +1,17 @@
+Require Import Int63.
+
+Set Implicit Arguments.
+
+Open Scope int63_scope.
+
+Check (eq_refl : 6 \% 3 = 0).
+Check (eq_refl 0 <: 6 \% 3 = 0).
+Check (eq_refl 0 <<: 6 \% 3 = 0).
+Definition compute1 := Eval compute in 6 \% 3.
+Check (eq_refl compute1 : 0 = 0).
+
+Check (eq_refl : 5 \% 3 = 2).
+Check (eq_refl 2 <: 5 \% 3 = 2).
+Check (eq_refl 2 <<: 5 \% 3 = 2).
+Definition compute2 := Eval compute in 5 \% 3.
+Check (eq_refl compute2 : 2 = 2).
diff --git a/test-suite/arithmetic/mul.v b/test-suite/arithmetic/mul.v
new file mode 100644
index 0000000000..9480e8cd46
--- /dev/null
+++ b/test-suite/arithmetic/mul.v
@@ -0,0 +1,17 @@
+Require Import Int63.
+
+Set Implicit Arguments.
+
+Open Scope int63_scope.
+
+Check (eq_refl : 2 * 3 = 6).
+Check (eq_refl 6 <: 2 * 3 = 6).
+Check (eq_refl 6 <<: 2 * 3 = 6).
+Definition compute1 := Eval compute in 2 * 3.
+Check (eq_refl compute1 : 6 = 6).
+
+Check (eq_refl : 9223372036854775807 * 2 = 9223372036854775806).
+Check (eq_refl 9223372036854775806 <: 9223372036854775807 * 2 = 9223372036854775806).
+Check (eq_refl 9223372036854775806 <<: 9223372036854775807 * 2 = 9223372036854775806).
+Definition compute2 := Eval compute in 9223372036854775807 * 2.
+Check (eq_refl compute2 : 9223372036854775806 = 9223372036854775806).
diff --git a/test-suite/arithmetic/mulc.v b/test-suite/arithmetic/mulc.v
new file mode 100644
index 0000000000..e10855bafa
--- /dev/null
+++ b/test-suite/arithmetic/mulc.v
@@ -0,0 +1,22 @@
+Require Import Cyclic63.
+
+Set Implicit Arguments.
+
+Open Scope int63_scope.
+
+Check (eq_refl : 2 *c 3 = WW 0 6).
+Check (eq_refl (WW 0 6) <: 2 *c 3 = WW 0 6).
+Check (eq_refl (WW 0 6) <<: 2 *c 3 = WW 0 6).
+Definition compute1 := Eval compute in 2 *c 3.
+Check (eq_refl compute1 : WW 0 6 = WW 0 6).
+
+Check (eq_refl : 9223372036854775807 *c 2 = WW 1 9223372036854775806).
+Check (eq_refl (WW 1 9223372036854775806) <: 9223372036854775807 *c 2 = WW 1 9223372036854775806).
+Check (eq_refl (WW 1 9223372036854775806) <<: 9223372036854775807 *c 2 = WW 1 9223372036854775806).
+
+Definition compute2 := Eval compute in 9223372036854775807 *c 2.
+Check (eq_refl compute2 : WW 1 9223372036854775806 = WW 1 9223372036854775806).
+
+Check (eq_refl : 0 *c 0 = W0).
+Check (eq_refl (@W0 int) <: 0 *c 0 = W0).
+Check (eq_refl (@W0 int) <<: 0 *c 0 = W0).
diff --git a/test-suite/arithmetic/primitive.v b/test-suite/arithmetic/primitive.v
new file mode 100644
index 0000000000..f62f6109e1
--- /dev/null
+++ b/test-suite/arithmetic/primitive.v
@@ -0,0 +1,12 @@
+Section S.
+  Variable A : Type.
+  Fail Primitive int : let x := A in Set := #int63_type.
+  Fail Primitive add := #int63_add.
+End S.
+
+(* [Primitive] should be forbidden in sections, otherwise its type after cooking
+will be incorrect:
+
+Check int.
+
+*)
diff --git a/test-suite/arithmetic/reduction.v b/test-suite/arithmetic/reduction.v
new file mode 100644
index 0000000000..00e067ac5a
--- /dev/null
+++ b/test-suite/arithmetic/reduction.v
@@ -0,0 +1,28 @@
+Require Import Int63.
+
+Open Scope int63_scope.
+
+Definition div_eucl_plus_one i1 i2 :=
+  let (q,r) := diveucl i1 i2 in
+  (q+1, r+1)%int63.
+
+Definition rcbn := Eval cbn in div_eucl_plus_one 3 2.
+Check (eq_refl : rcbn = (2, 2)).
+
+Definition rcbv := Eval cbv in div_eucl_plus_one 3 2.
+Check (eq_refl : rcbv = (2, 2)).
+
+Definition rvmc := Eval vm_compute in div_eucl_plus_one 3 2.
+Check (eq_refl : rvmc = (2, 2)).
+
+Definition f n m :=
+  match (n ?= 42)%int63 with
+  | Lt => (n + m)%int63
+  | _ => (2*m)%int63
+  end.
+
+Goal forall n, (n ?= 42)%int63 = Gt -> f n 256 = 512%int63.
+  intros. unfold f.
+  cbn. Undo. cbv. (* Test reductions under match clauses *)
+  rewrite H. reflexivity.
+Qed.
diff --git a/test-suite/arithmetic/sub.v b/test-suite/arithmetic/sub.v
new file mode 100644
index 0000000000..1606fd2aa1
--- /dev/null
+++ b/test-suite/arithmetic/sub.v
@@ -0,0 +1,17 @@
+Require Import Int63.
+
+Set Implicit Arguments.
+
+Open Scope int63_scope.
+
+Check (eq_refl : 3 - 2 = 1).
+Check (eq_refl 1 <: 3 - 2 = 1).
+Check (eq_refl 1 <<: 3 - 2 = 1).
+Definition compute1 := Eval compute in 3 - 2.
+Check (eq_refl compute1 : 1 = 1).
+
+Check (eq_refl : 0 - 1 = 9223372036854775807).
+Check (eq_refl 9223372036854775807 <: 0 - 1 = 9223372036854775807).
+Check (eq_refl 9223372036854775807 <<: 0 - 1 = 9223372036854775807).
+Definition compute2 := Eval compute in 0 - 1.
+Check (eq_refl compute2 : 9223372036854775807 = 9223372036854775807).
diff --git a/test-suite/arithmetic/subc.v b/test-suite/arithmetic/subc.v
new file mode 100644
index 0000000000..fc4067e48b
--- /dev/null
+++ b/test-suite/arithmetic/subc.v
@@ -0,0 +1,17 @@
+Require Import Int63.
+
+Set Implicit Arguments.
+
+Open Scope int63_scope.
+
+Check (eq_refl : 3 -c 2 = C0 1).
+Check (eq_refl (C0 1) <: 3 -c 2 = C0 1).
+Check (eq_refl (C0 1) <<: 3 -c 2 = C0 1).
+Definition compute1 := Eval compute in 3 -c 2.
+Check (eq_refl compute1 : C0 1 = C0 1).
+
+Check (eq_refl : 0 -c 1 = C1 9223372036854775807).
+Check (eq_refl (C1 9223372036854775807) <: 0 -c 1 = C1 9223372036854775807).
+Check (eq_refl (C1 9223372036854775807) <<: 0 -c 1 = C1 9223372036854775807).
+Definition compute2 := Eval compute in 0 -c 1.
+Check (eq_refl compute2 : C1 9223372036854775807 = C1 9223372036854775807).
diff --git a/test-suite/arithmetic/subcarryc.v b/test-suite/arithmetic/subcarryc.v
new file mode 100644
index 0000000000..e81b6536b2
--- /dev/null
+++ b/test-suite/arithmetic/subcarryc.v
@@ -0,0 +1,17 @@
+Require Import Int63.
+
+Set Implicit Arguments.
+
+Open Scope int63_scope.
+
+Check (eq_refl : subcarryc 3 1 = C0 1).
+Check (eq_refl (C0 1) <: subcarryc 3 1 = C0 1).
+Check (eq_refl (C0 1) <<: subcarryc 3 1 = C0 1).
+Definition compute1 := Eval compute in subcarryc 3 1.
+Check (eq_refl compute1 : C0 1 = C0 1).
+
+Check (eq_refl : subcarryc 0 1 = C1 9223372036854775806).
+Check (eq_refl (C1 9223372036854775806) <: subcarryc 0 1 = C1 9223372036854775806).
+Check (eq_refl (C1 9223372036854775806) <<: subcarryc 0 1 = C1 9223372036854775806).
+Definition compute2 := Eval compute in subcarryc 0 1.
+Check (eq_refl compute2 : C1 9223372036854775806 = C1 9223372036854775806).
diff --git a/test-suite/arithmetic/tail0.v b/test-suite/arithmetic/tail0.v
new file mode 100644
index 0000000000..c9d426087a
--- /dev/null
+++ b/test-suite/arithmetic/tail0.v
@@ -0,0 +1,23 @@
+Require Import Int63.
+
+Set Implicit Arguments.
+
+Open Scope int63_scope.
+
+Check (eq_refl : tail0 2305843009213693952 = 61).
+Check (eq_refl 61 <: tail0 2305843009213693952 = 61).
+Check (eq_refl 61 <<: tail0 2305843009213693952 = 61).
+Definition compute1 := Eval compute in tail0 2305843009213693952.
+Check (eq_refl compute1 : 61 = 61).
+
+Check (eq_refl : tail0 1 = 0).
+Check (eq_refl 0 <: tail0 1 = 0).
+Check (eq_refl 0 <<: tail0 1 = 0).
+Definition compute2 := Eval compute in tail0 1.
+Check (eq_refl compute2 : 0 = 0).
+
+Check (eq_refl : tail0 0 = 63).
+Check (eq_refl 63 <: tail0 0 = 63).
+Check (eq_refl 63 <<: tail0 0 = 63).
+Definition compute3 := Eval compute in tail0 0.
+Check (eq_refl compute3 : 63 = 63).
diff --git a/test-suite/arithmetic/unsigned.v b/test-suite/arithmetic/unsigned.v
new file mode 100644
index 0000000000..82920bd201
--- /dev/null
+++ b/test-suite/arithmetic/unsigned.v
@@ -0,0 +1,18 @@
+(* This file checks that operations over int63 are unsigned. *)
+Require Import Int63.
+
+Open Scope int63_scope.
+
+(* (0-1) must be the maximum integer value and not negative 1 *)
+
+Check (eq_refl : 1/(0-1) = 0).
+Check (eq_refl 0 <: 1/(0-1) = 0).
+Check (eq_refl 0 <<: 1/(0-1) = 0).
+Definition compute1 := Eval compute in 1/(0-1).
+Check (eq_refl compute1 : 0 = 0).
+
+Check (eq_refl : 3 \% (0-1) = 3).
+Check (eq_refl 3 <: 3 \% (0-1) = 3).
+Check (eq_refl 3 <<: 3 \% (0-1) = 3).
+Definition compute2 := Eval compute in 3 \% (0-1).
+Check (eq_refl compute2 : 3 = 3).