Merge PR #6914: Primitive integers

Ack-by: JasonGross
Ack-by: SkySkimmer
Ack-by: ejgallego
Ack-by: gares
Ack-by: maximedenes
Ack-by: ppedrot

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).