Add tests for primitive floats

Add utility ldexp and frexp functions to prevent dealing with the shift of
ldshiftexp and frshiftexp everywhere.

Also move primitive integer tests to place all primitive tests in the
same directory.

39 files changed, 316 insertions, 2 deletions

diff --git a/test-suite/Makefile b/test-suite/Makefile
index c60f39231e..57994f9b2c 100644
--- a/test-suite/Makefile
+++ b/test-suite/Makefile
@@ -102,7 +102,7 @@ INTERACTIVE := interactive
 UNIT_TESTS := unit-tests
 VSUBSYSTEMS := prerequisite success failure $(BUGS) output output-coqtop \
   output-modulo-time $(INTERACTIVE) micromega $(COMPLEXITY) modules stm \
-  coqdoc ssr arithmetic ltac2
+  coqdoc ssr primitive/uint63 primitive/float ltac2
 
 # All subsystems
 SUBSYSTEMS := $(VSUBSYSTEMS) misc bugs ide vio coqchk coqwc coq-makefile tools $(UNIT_TESTS)
@@ -174,6 +174,7 @@ summary:
 	  $(call summary_dir, "Miscellaneous tests", misc); \
 	  $(call summary_dir, "Complexity tests", complexity); \
 	  $(call summary_dir, "Module tests", modules); \
+	  $(call summary_dir, "Primitive tests", primitive); \
 	  $(call summary_dir, "STM tests", stm); \
 	  $(call summary_dir, "SSR tests", ssr); \
 	  $(call summary_dir, "IDE tests", ide); \
@@ -329,7 +330,7 @@ $(addsuffix .log,$(wildcard prerequisite/*.v)): %.v.log: %.v
 	} > "$@"
 
 ssr: $(wildcard ssr/*.v:%.v=%.v.log)
-$(addsuffix .log,$(wildcard ssr/*.v success/*.v micromega/*.v modules/*.v arithmetic/*.v ltac2/*.v)): %.v.log: %.v $(PREREQUISITELOG)
+$(addsuffix .log,$(wildcard ssr/*.v success/*.v micromega/*.v modules/*.v primitive/*/*.v ltac2/*.v)): %.v.log: %.v $(PREREQUISITELOG)
 	@echo "TEST      $< $(call get_coq_prog_args_in_parens,"$<")"
 	$(HIDE){ \
 	  opts="$(if $(findstring modules/,$<),-R modules Mods)"; \
diff --git a/test-suite/primitive/float/add.v b/test-suite/primitive/float/add.v
new file mode 100644
index 0000000000..cd157ede83
--- /dev/null
+++ b/test-suite/primitive/float/add.v
@@ -0,0 +1,45 @@
+Require Import ZArith Int63 Floats.
+
+Open Scope float_scope.
+
+Definition two := Eval compute in of_int63 2%int63.
+Definition three := Eval compute in of_int63 3%int63.
+Definition five := Eval compute in of_int63 5%int63.
+
+Check (eq_refl : two + three = five).
+(*Check (eq_refl five <: two + three = five).
+Check (eq_refl 5 <<: two + three = five).*)
+Definition compute1 := Eval compute in two + three.
+Check (eq_refl compute1 : five = five).
+
+Definition huge := Eval compute in ldexp one 1023%Z.
+Definition tiny := Eval compute in ldexp one (-1023)%Z.
+
+Check (eq_refl : huge + tiny = huge).
+(*Check (eq_refl huge <: huge + tiny = huge).
+Check (eq_refl huge <<: huge + tiny = huge).*)
+Definition compute2 := Eval compute in huge + tiny.
+Check (eq_refl compute2 : huge = huge).
+
+Check (eq_refl : huge + huge = infinity).
+Definition compute3 := Eval compute in huge + huge.
+Check (eq_refl compute3 : infinity = infinity).
+
+Check (eq_refl : one + nan = nan).
+Definition compute4 := Eval compute in one + nan.
+Check (eq_refl compute4 : nan = nan).
+
+Check (eq_refl : infinity + infinity = infinity).
+Definition compute5 := Eval compute in infinity + infinity.
+Check (eq_refl compute5 : infinity = infinity).
+
+Check (eq_refl : infinity + neg_infinity = nan).
+Definition compute6 := Eval compute in infinity + neg_infinity.
+Check (eq_refl compute6 : nan = nan).
+
+Check (eq_refl : zero + zero = zero).
+Check (eq_refl : neg_zero + zero = zero).
+Check (eq_refl : neg_zero + neg_zero = neg_zero).
+Check (eq_refl : zero + neg_zero = zero).
+
+Check (eq_refl : huge + neg_infinity = neg_infinity).
diff --git a/test-suite/primitive/float/div.v b/test-suite/primitive/float/div.v
new file mode 100644
index 0000000000..b2e9278e71
--- /dev/null
+++ b/test-suite/primitive/float/div.v
@@ -0,0 +1,51 @@
+Require Import ZArith Int63 Floats.
+
+Open Scope float_scope.
+
+Definition two := Eval compute in of_int63 2%int63.
+Definition three := Eval compute in of_int63 3%int63.
+Definition six := Eval compute in of_int63 6%int63.
+
+Check (eq_refl : six / three = two).
+Definition compute1 := Eval compute in six / three.
+Check (eq_refl compute1 : two = two).
+
+Definition huge := Eval compute in ldexp one 1023%Z.
+Definition tiny := Eval compute in ldexp one (-1023)%Z.
+
+Check (eq_refl : huge / tiny = infinity).
+Definition compute2 := Eval compute in huge / tiny.
+Check (eq_refl compute2 : infinity = infinity).
+
+Check (eq_refl : huge / huge = one).
+Definition compute3 := Eval compute in huge / huge.
+Check (eq_refl compute3 : one = one).
+
+Check (eq_refl : one / nan = nan).
+Definition compute4 := Eval compute in one / nan.
+Check (eq_refl compute4 : nan = nan).
+
+Check (eq_refl : infinity / infinity = nan).
+Definition compute5 := Eval compute in infinity / infinity.
+Check (eq_refl compute5 : nan = nan).
+
+Check (eq_refl : infinity / neg_infinity = nan).
+Definition compute6 := Eval compute in infinity / neg_infinity.
+Check (eq_refl compute6 : nan = nan).
+
+Check (eq_refl : zero / zero = nan).
+Check (eq_refl : neg_zero / zero = nan).
+
+Check (eq_refl : huge / neg_infinity = neg_zero).
+
+Check (eq_refl : one / tiny = huge).
+Check (eq_refl : one / huge = tiny).
+Check (eq_refl : zero / huge = zero).
+Check (eq_refl : zero / (-huge) = neg_zero).
+
+Check (eq_refl : tiny / one = tiny).
+Check (eq_refl : huge / one = huge).
+Check (eq_refl : infinity / one = infinity).
+
+Check (eq_refl : zero / infinity = zero).
+Check (eq_refl : infinity / zero = infinity).
diff --git a/test-suite/primitive/float/double_rounding.v b/test-suite/primitive/float/double_rounding.v
new file mode 100644
index 0000000000..92322ea473
--- /dev/null
+++ b/test-suite/primitive/float/double_rounding.v
@@ -0,0 +1,20 @@
+Require Import Floats ZArith.
+
+(* This test check that there is no double rounding with 80 bits registers inside float computations *)
+
+Definition big_cbn := Eval cbn in ldexp one (53)%Z.
+Definition small_cbn := Eval cbn in (one + ldexp one (-52)%Z)%float.
+Definition result_cbn := Eval cbn in (big_cbn + small_cbn)%float.
+Definition check_cbn := Eval cbn in (big_cbn + one)%float.
+
+Check (eq_refl : (result_cbn ?= big_cbn)%float = Some Gt).
+Check (eq_refl : (check_cbn ?= big_cbn)%float = Some Eq).
+
+
+Definition big_cbv := Eval cbv in ldexp one (53)%Z.
+Definition small_cbv := Eval cbv in (one + ldexp one (-52)%Z)%float.
+Definition result_cbv := Eval cbv in (big_cbv + small_cbv)%float.
+Definition check_cbv := Eval cbv in (big_cbv + one)%float.
+
+Check (eq_refl : (result_cbv ?= big_cbv)%float = Some Gt).
+Check (eq_refl : (check_cbv ?= big_cbv)%float = Some Eq).
diff --git a/test-suite/primitive/float/frexp.v b/test-suite/primitive/float/frexp.v
new file mode 100644
index 0000000000..254dfa7028
--- /dev/null
+++ b/test-suite/primitive/float/frexp.v
@@ -0,0 +1,16 @@
+Require Import ZArith Floats.
+
+Definition denorm := Eval compute in ldexp one (-1074)%Z.
+Definition neg_one := Eval compute in (-one)%float.
+
+Check (eq_refl : let (m,e) := frexp infinity in (Prim2SF m, e) = SFfrexp prec emax (Prim2SF infinity)).
+
+Check (eq_refl : let (m,e) := frexp nan in (Prim2SF m, e) = SFfrexp prec emax (Prim2SF nan)).
+
+Check (eq_refl : let (m,e) := frexp zero in (Prim2SF m, e) = SFfrexp prec emax (Prim2SF zero)).
+
+Check (eq_refl : let (m,e) := frexp one in (Prim2SF m, e) = SFfrexp prec emax (Prim2SF one)).
+
+Check (eq_refl : let (m,e) := frexp neg_one in (Prim2SF m, e) = SFfrexp prec emax (Prim2SF neg_one)).
+
+Check (eq_refl : let (m,e) := frexp denorm in (Prim2SF m, e) = SFfrexp prec emax (Prim2SF denorm)).
diff --git a/test-suite/primitive/float/mul.v b/test-suite/primitive/float/mul.v
new file mode 100644
index 0000000000..99b431896f
--- /dev/null
+++ b/test-suite/primitive/float/mul.v
@@ -0,0 +1,49 @@
+Require Import ZArith Int63 Floats.
+
+Open Scope float_scope.
+
+Definition two := Eval compute in of_int63 2%int63.
+Definition three := Eval compute in of_int63 3%int63.
+Definition six := Eval compute in of_int63 6%int63.
+
+Check (eq_refl : three * two = six).
+Definition compute1 := Eval compute in three * two.
+Check (eq_refl compute1 : six = six).
+
+Definition huge := Eval compute in ldexp one 1023%Z.
+Definition tiny := Eval compute in ldexp one (-1023)%Z.
+
+Check (eq_refl : huge * tiny = one).
+Definition compute2 := Eval compute in huge * tiny.
+Check (eq_refl compute2 : one = one).
+
+Check (eq_refl : huge * huge = infinity).
+Definition compute3 := Eval compute in huge * huge.
+Check (eq_refl compute3 : infinity = infinity).
+
+Check (eq_refl : one * nan = nan).
+Definition compute4 := Eval compute in one * nan.
+Check (eq_refl compute4 : nan = nan).
+
+Check (eq_refl : infinity * infinity = infinity).
+Definition compute5 := Eval compute in infinity * infinity.
+Check (eq_refl compute5 : infinity = infinity).
+
+Check (eq_refl : infinity * neg_infinity = neg_infinity).
+Definition compute6 := Eval compute in infinity * neg_infinity.
+Check (eq_refl compute6 : neg_infinity = neg_infinity).
+
+Check (eq_refl : zero * zero = zero).
+Check (eq_refl : neg_zero * zero = neg_zero).
+Check (eq_refl : neg_zero * neg_zero = zero).
+Check (eq_refl : zero * neg_zero = neg_zero).
+
+Check (eq_refl : huge * neg_infinity = neg_infinity).
+
+Check (eq_refl : one * tiny = tiny).
+Check (eq_refl : one * huge = huge).
+Check (eq_refl : zero * huge = zero).
+Check (eq_refl : zero * (-huge) = neg_zero).
+
+Check (eq_refl : zero * infinity = nan).
+Check (eq_refl : neg_infinity * zero = nan).
diff --git a/test-suite/primitive/float/normfr_mantissa.v b/test-suite/primitive/float/normfr_mantissa.v
new file mode 100644
index 0000000000..6cc9f5ef92
--- /dev/null
+++ b/test-suite/primitive/float/normfr_mantissa.v
@@ -0,0 +1,12 @@
+Require Import Int63 ZArith Floats.
+
+Definition half := ldexp one (-1)%Z.
+Definition three_quarters := (half + (ldexp one (-2)%Z))%float.
+
+Check (eq_refl : normfr_mantissa one = 0%int63).
+Check (eq_refl : normfr_mantissa half = (1 << 52)%int63).
+Check (eq_refl : normfr_mantissa (-half) = (1 << 52)%int63).
+Check (eq_refl : normfr_mantissa (-one) = 0%int63).
+Check (eq_refl : normfr_mantissa zero = 0%int63).
+Check (eq_refl : normfr_mantissa nan = 0%int63).
+Check (eq_refl : normfr_mantissa three_quarters = (3 << 51)%int63).
diff --git a/test-suite/primitive/float/spec_conv.v b/test-suite/primitive/float/spec_conv.v
new file mode 100644
index 0000000000..12a5fe4dca
--- /dev/null
+++ b/test-suite/primitive/float/spec_conv.v
@@ -0,0 +1,20 @@
+Require Import ZArith Floats.
+
+Definition two := Eval compute in (one + one)%float.
+Definition half := Eval compute in (one / two)%float.
+Definition huge := Eval compute in ldexp one (1023)%Z.
+Definition tiny := Eval compute in ldexp one (-1023)%Z.
+Definition denorm := Eval compute in ldexp one (-1074)%Z.
+
+Check (eq_refl : SF2Prim (Prim2SF zero) = zero).
+Check (eq_refl : SF2Prim (Prim2SF neg_zero) = neg_zero).
+Check (eq_refl : SF2Prim (Prim2SF one) = one).
+Check (eq_refl : SF2Prim (Prim2SF (-one)) = (-one)%float).
+Check (eq_refl : SF2Prim (Prim2SF infinity) = infinity).
+Check (eq_refl : SF2Prim (Prim2SF neg_infinity) = neg_infinity).
+Check (eq_refl : SF2Prim (Prim2SF huge) = huge).
+Check (eq_refl : SF2Prim (Prim2SF tiny) = tiny).
+Check (eq_refl : SF2Prim (Prim2SF denorm) = denorm).
+Check (eq_refl : SF2Prim (Prim2SF nan) = nan).
+Check (eq_refl : SF2Prim (Prim2SF two) = two).
+Check (eq_refl : SF2Prim (Prim2SF half) = half).
diff --git a/test-suite/primitive/float/sqrt.v b/test-suite/primitive/float/sqrt.v
new file mode 100644
index 0000000000..0bacda9686
--- /dev/null
+++ b/test-suite/primitive/float/sqrt.v
@@ -0,0 +1,33 @@
+Require Import ZArith Int63 Floats.
+
+Open Scope float_scope.
+
+Definition three := Eval compute in of_int63 3%int63.
+Definition nine := Eval compute in of_int63 9%int63.
+
+Check (eq_refl : sqrt nine = three).
+Definition compute1 := Eval compute in sqrt nine.
+Check (eq_refl : three = three).
+
+Definition huge := Eval compute in ldexp one (1023)%Z.
+Definition tiny := Eval compute in ldexp one (-1023)%Z.
+Definition denorm := Eval compute in ldexp one (-1074)%Z.
+
+Goal (Prim2SF (sqrt huge) = SF64sqrt (Prim2SF huge)).
+  now compute.
+Qed.
+
+Goal (Prim2SF (sqrt tiny) = SF64sqrt (Prim2SF tiny)).
+  now compute.
+Qed.
+
+Goal (Prim2SF (sqrt denorm) = SF64sqrt (Prim2SF denorm)).
+  now compute.
+Qed.
+
+Check (eq_refl : sqrt neg_zero = neg_zero).
+Check (eq_refl : sqrt zero = zero).
+Check (eq_refl : sqrt one = one).
+Check (eq_refl : sqrt (-one) = nan).
+Check (eq_refl : sqrt infinity = infinity).
+Check (eq_refl : sqrt neg_infinity = nan).
diff --git a/test-suite/primitive/float/sub.v b/test-suite/primitive/float/sub.v
new file mode 100644
index 0000000000..0796ff51ff
--- /dev/null
+++ b/test-suite/primitive/float/sub.v
@@ -0,0 +1,40 @@
+Require Import ZArith Int63 Floats.
+
+Open Scope float_scope.
+
+Definition two := Eval compute in of_int63 2%int63.
+Definition three := Eval compute in of_int63 3%int63.
+
+Check (eq_refl : three - two = one).
+Definition compute1 := Eval compute in three - two.
+Check (eq_refl compute1 : one = one).
+
+Definition huge := Eval compute in ldexp one 1023%Z.
+Definition tiny := Eval compute in ldexp one (-1023)%Z.
+
+Check (eq_refl : huge - tiny = huge).
+Definition compute2 := Eval compute in huge - tiny.
+Check (eq_refl compute2 : huge = huge).
+
+Check (eq_refl : huge - huge = zero).
+Definition compute3 := Eval compute in huge - huge.
+Check (eq_refl compute3 : zero = zero).
+
+Check (eq_refl : one - nan = nan).
+Definition compute4 := Eval compute in one - nan.
+Check (eq_refl compute4 : nan = nan).
+
+Check (eq_refl : infinity - infinity = nan).
+Definition compute5 := Eval compute in infinity - infinity.
+Check (eq_refl compute5 : nan = nan).
+
+Check (eq_refl : infinity - neg_infinity = infinity).
+Definition compute6 := Eval compute in infinity - neg_infinity.
+Check (eq_refl compute6 : infinity = infinity).
+
+Check (eq_refl : zero - zero = zero).
+Check (eq_refl : neg_zero - zero = neg_zero).
+Check (eq_refl : neg_zero - neg_zero = zero).
+Check (eq_refl : zero - neg_zero = zero).
+
+Check (eq_refl : huge - neg_infinity = infinity).
diff --git a/test-suite/primitive/float/valid_binary_conv.v b/test-suite/primitive/float/valid_binary_conv.v
new file mode 100644
index 0000000000..ad81e55667
--- /dev/null
+++ b/test-suite/primitive/float/valid_binary_conv.v
@@ -0,0 +1,20 @@
+Require Import ZArith Floats.
+
+Definition two := Eval compute in (one + one)%float.
+Definition half := Eval compute in (one / two)%float.
+Definition huge := Eval compute in ldexp one (1023)%Z.
+Definition tiny := Eval compute in ldexp one (-1022)%Z.
+Definition denorm := Eval compute in ldexp one (-1074)%Z.
+
+Check (eq_refl : valid_binary (Prim2SF zero) = true).
+Check (eq_refl : valid_binary (Prim2SF neg_zero) = true).
+Check (eq_refl : valid_binary (Prim2SF one) = true).
+Check (eq_refl : valid_binary (Prim2SF (-one)) = true).
+Check (eq_refl : valid_binary (Prim2SF infinity) = true).
+Check (eq_refl : valid_binary (Prim2SF neg_infinity) = true).
+Check (eq_refl : valid_binary (Prim2SF huge) = true).
+Check (eq_refl : valid_binary (Prim2SF tiny) = true).
+Check (eq_refl : valid_binary (Prim2SF denorm) = true).
+Check (eq_refl : valid_binary (Prim2SF nan) = true).
+Check (eq_refl : valid_binary (Prim2SF two) = true).
+Check (eq_refl : valid_binary (Prim2SF half) = true).
diff --git a/test-suite/primitive/float/zero.v b/test-suite/primitive/float/zero.v
new file mode 100644
index 0000000000..75348d4657
--- /dev/null
+++ b/test-suite/primitive/float/zero.v
@@ -0,0 +1,7 @@
+Require Import ZArith Int63 Floats.
+
+Open Scope float_scope.
+
+Fail Check (eq_refl : zero = neg_zero).
+Fail Check (eq_refl <: zero = neg_zero).
+Fail Check (eq_refl <<: zero = neg_zero).
diff --git a/test-suite/arithmetic/add.v b/test-suite/primitive/uint63/add.v
index fb7eb1d53c..fb7eb1d53c 100644
--- a/test-suite/arithmetic/add.v
+++ b/test-suite/primitive/uint63/add.v
diff --git a/test-suite/arithmetic/addc.v b/test-suite/primitive/uint63/addc.v
index 432aec0291..432aec0291 100644
--- a/test-suite/arithmetic/addc.v
+++ b/test-suite/primitive/uint63/addc.v
diff --git a/test-suite/arithmetic/addcarryc.v b/test-suite/primitive/uint63/addcarryc.v
index a4430769ca..a4430769ca 100644
--- a/test-suite/arithmetic/addcarryc.v
+++ b/test-suite/primitive/uint63/addcarryc.v
diff --git a/test-suite/arithmetic/addmuldiv.v b/test-suite/primitive/uint63/addmuldiv.v
index 72b0164b49..72b0164b49 100644
--- a/test-suite/arithmetic/addmuldiv.v
+++ b/test-suite/primitive/uint63/addmuldiv.v
diff --git a/test-suite/arithmetic/compare.v b/test-suite/primitive/uint63/compare.v
index a8d1ea1226..a8d1ea1226 100644
--- a/test-suite/arithmetic/compare.v
+++ b/test-suite/primitive/uint63/compare.v
diff --git a/test-suite/arithmetic/div.v b/test-suite/primitive/uint63/div.v
index 0ee0b91580..0ee0b91580 100644
--- a/test-suite/arithmetic/div.v
+++ b/test-suite/primitive/uint63/div.v
diff --git a/test-suite/arithmetic/diveucl.v b/test-suite/primitive/uint63/diveucl.v
index 8f88a0f356..8f88a0f356 100644
--- a/test-suite/arithmetic/diveucl.v
+++ b/test-suite/primitive/uint63/diveucl.v
diff --git a/test-suite/arithmetic/diveucl_21.v b/test-suite/primitive/uint63/diveucl_21.v
index b12dba429c..b12dba429c 100644
--- a/test-suite/arithmetic/diveucl_21.v
+++ b/test-suite/primitive/uint63/diveucl_21.v
diff --git a/test-suite/arithmetic/eqb.v b/test-suite/primitive/uint63/eqb.v
index dcc0b71f6d..dcc0b71f6d 100644
--- a/test-suite/arithmetic/eqb.v
+++ b/test-suite/primitive/uint63/eqb.v
diff --git a/test-suite/arithmetic/head0.v b/test-suite/primitive/uint63/head0.v
index f4234d2605..f4234d2605 100644
--- a/test-suite/arithmetic/head0.v
+++ b/test-suite/primitive/uint63/head0.v
diff --git a/test-suite/arithmetic/isint.v b/test-suite/primitive/uint63/isint.v
index c215caa878..c215caa878 100644
--- a/test-suite/arithmetic/isint.v
+++ b/test-suite/primitive/uint63/isint.v
diff --git a/test-suite/arithmetic/land.v b/test-suite/primitive/uint63/land.v
index 0ea6fd90b6..0ea6fd90b6 100644
--- a/test-suite/arithmetic/land.v
+++ b/test-suite/primitive/uint63/land.v
diff --git a/test-suite/arithmetic/leb.v b/test-suite/primitive/uint63/leb.v
index 5354919978..5354919978 100644
--- a/test-suite/arithmetic/leb.v
+++ b/test-suite/primitive/uint63/leb.v
diff --git a/test-suite/arithmetic/lor.v b/test-suite/primitive/uint63/lor.v
index 9c3b85c054..9c3b85c054 100644
--- a/test-suite/arithmetic/lor.v
+++ b/test-suite/primitive/uint63/lor.v
diff --git a/test-suite/arithmetic/lsl.v b/test-suite/primitive/uint63/lsl.v
index 70f3b90140..70f3b90140 100644
--- a/test-suite/arithmetic/lsl.v
+++ b/test-suite/primitive/uint63/lsl.v
diff --git a/test-suite/arithmetic/lsr.v b/test-suite/primitive/uint63/lsr.v
index c36c24e237..c36c24e237 100644
--- a/test-suite/arithmetic/lsr.v
+++ b/test-suite/primitive/uint63/lsr.v
diff --git a/test-suite/arithmetic/ltb.v b/test-suite/primitive/uint63/ltb.v
index 7ae5ac6493..7ae5ac6493 100644
--- a/test-suite/arithmetic/ltb.v
+++ b/test-suite/primitive/uint63/ltb.v
diff --git a/test-suite/arithmetic/lxor.v b/test-suite/primitive/uint63/lxor.v
index b453fc7697..b453fc7697 100644
--- a/test-suite/arithmetic/lxor.v
+++ b/test-suite/primitive/uint63/lxor.v
diff --git a/test-suite/arithmetic/mod.v b/test-suite/primitive/uint63/mod.v
index 5307eed493..5307eed493 100644
--- a/test-suite/arithmetic/mod.v
+++ b/test-suite/primitive/uint63/mod.v
diff --git a/test-suite/arithmetic/mul.v b/test-suite/primitive/uint63/mul.v
index 9480e8cd46..9480e8cd46 100644
--- a/test-suite/arithmetic/mul.v
+++ b/test-suite/primitive/uint63/mul.v
diff --git a/test-suite/arithmetic/mulc.v b/test-suite/primitive/uint63/mulc.v
index e10855bafa..e10855bafa 100644
--- a/test-suite/arithmetic/mulc.v
+++ b/test-suite/primitive/uint63/mulc.v
diff --git a/test-suite/arithmetic/reduction.v b/test-suite/primitive/uint63/reduction.v
index 00e067ac5a..00e067ac5a 100644
--- a/test-suite/arithmetic/reduction.v
+++ b/test-suite/primitive/uint63/reduction.v
diff --git a/test-suite/arithmetic/sub.v b/test-suite/primitive/uint63/sub.v
index 1606fd2aa1..1606fd2aa1 100644
--- a/test-suite/arithmetic/sub.v
+++ b/test-suite/primitive/uint63/sub.v
diff --git a/test-suite/arithmetic/subc.v b/test-suite/primitive/uint63/subc.v
index fc4067e48b..fc4067e48b 100644
--- a/test-suite/arithmetic/subc.v
+++ b/test-suite/primitive/uint63/subc.v
diff --git a/test-suite/arithmetic/subcarryc.v b/test-suite/primitive/uint63/subcarryc.v
index e81b6536b2..e81b6536b2 100644
--- a/test-suite/arithmetic/subcarryc.v
+++ b/test-suite/primitive/uint63/subcarryc.v
diff --git a/test-suite/arithmetic/tail0.v b/test-suite/primitive/uint63/tail0.v
index c9d426087a..c9d426087a 100644
--- a/test-suite/arithmetic/tail0.v
+++ b/test-suite/primitive/uint63/tail0.v
diff --git a/test-suite/arithmetic/unsigned.v b/test-suite/primitive/uint63/unsigned.v
index 82920bd201..82920bd201 100644
--- a/test-suite/arithmetic/unsigned.v
+++ b/test-suite/primitive/uint63/unsigned.v