Compatibility with Coq 8.17

.github/workflows/coq.yml

@@ -0,0 +1,49 @@
+name: Coq
+
+on:
+  push:
+    branches: ["master"]
+  pull_request:
+    branches: ["master"]
+
+env:
+  CARGO_TERM_COLOR: always
+
+jobs:
+  build:
+    runs-on: ubuntu-latest
+
+    steps:
+      - uses: actions/checkout@v3
+      - name: Download Git submodules
+        run: git submodule update --init --recursive
+      - uses: coq-community/docker-coq-action@v1
+        with:
+          custom_image: coqorg/coq:8.17-ocaml-4.14-flambda
+          custom_script: |
+            startGroup "Install dependencies"
+              sudo apt-get update
+              sudo apt-get install -y golang bsdmainutils bison
+              bash < <(curl -s -S -L https://raw.githubusercontent.com/moovweb/gvm/master/binscripts/gvm-installer)
+              source ~/.gvm/scripts/gvm
+              # We need this intermediate step before going to 1.21
+              gvm install go1.17
+              gvm use go1.17
+              go version
+              gvm install go1.21
+              gvm use go1.21
+              go version
+            endGroup
+            startGroup "Set the rights"
+              sudo chown -R $(whoami) .
+            endGroup
+            startGroup "Compile the project"
+              ./configure
+              make -j
+            endGroup
+            startGroup "Run the tests"
+              cd test
+              ./configure
+              make -j
+              cd ..
+            endGroup

.gitignore

@@ -0,0 +1,15 @@
+# Tests
+test/gen_tests/gen_tests
+test/*.v
+
+# Coq files
+.lia.cache
+.nia.cache
+.Makefile.d
+Makefile
+Makefile.conf
+*.aux
+*.glob
+*.vo
+*.vok
+*.vos

Arith/Nibble.v

@@ -1,7 +1,7 @@
 From Coq Require Import Ascii.
 From Coq Require Import NArith.
 From Coq Require Import ZArith.
-From Coq Require Import Int63.
+From Coq Require Import Uint63.
 From Coq Require Import Lia.
 From Coq Require String Ascii.
 
@@ -327,21 +327,21 @@ f_equal.
 Qed.
 
 Definition nibble_of_uint63 (i: int)
-:= Nibble (0 < (i land 8))%int63
-          (0 < (i land 4))%int63
-          (0 < (i land 2))%int63
-          (0 < (i land 1))%int63.
+:= Nibble (0 <? (i land 8))%uint63
+          (0 <? (i land 4))%uint63
+          (0 <? (i land 2))%uint63
+          (0 <? (i land 1))%uint63.
 
 Definition uint63_of_nibble (n: nibble)
 := match n with
    | Nibble a8 a4 a2 a1 =>
-       ((if a8 then 8%int63 else 0%int63)
+       ((if a8 then 8%uint63 else 0%uint63)
          lor
-        (if a4 then 4%int63 else 0%int63)
+        (if a4 then 4%uint63 else 0%uint63)
          lor
-        (if a2 then 2%int63 else 0%int63)
+        (if a2 then 2%uint63 else 0%uint63)
          lor
-        (if a1 then 1%int63 else 0%int63))%int63
+        (if a1 then 1%uint63 else 0%uint63))%uint63
    end.
 
 Lemma nibble_of_uint63_of_nibble (n: nibble):
@@ -353,37 +353,37 @@ Qed.
 
 (** A direct conversion from a native int to a hex digit via an if cascade. *)
 Definition hex_digit_of_uint63 (i: int)
-:= if (0 < (i land 8))%int63 then
-     if (0 < (i land 4))%int63 then
-       if (0 < (i land 2))%int63 then
-         if (0 < (i land 1))%int63 then xF else xE
+:= if (0 <? (i land 8))%uint63 then
+     if (0 <? (i land 4))%uint63 then
+       if (0 <? (i land 2))%uint63 then
+         if (0 <? (i land 1))%uint63 then xF else xE
        else
-         if (0 < (i land 1))%int63 then xD else xC
+         if (0 <? (i land 1))%uint63 then xD else xC
      else
-       if (0 < (i land 2))%int63 then
-         if (0 < (i land 1))%int63 then xB else xA
+       if (0 <? (i land 2))%uint63 then
+         if (0 <? (i land 1))%uint63 then xB else xA
        else
-         if (0 < (i land 1))%int63 then x9 else x8
+         if (0 <? (i land 1))%uint63 then x9 else x8
    else
-     if (0 < (i land 4))%int63 then
-       if (0 < (i land 2))%int63 then
-         if (0 < (i land 1))%int63 then x7 else x6
+     if (0 <? (i land 4))%uint63 then
+       if (0 <? (i land 2))%uint63 then
+         if (0 <? (i land 1))%uint63 then x7 else x6
        else
-         if (0 < (i land 1))%int63 then x5 else x4
+         if (0 <? (i land 1))%uint63 then x5 else x4
      else
-       if (0 < (i land 2))%int63 then
-         if (0 < (i land 1))%int63 then x3 else x2
+       if (0 <? (i land 2))%uint63 then
+         if (0 <? (i land 1))%uint63 then x3 else x2
        else
-         if (0 < (i land 1))%int63 then x1 else x0.
+         if (0 <? (i land 1))%uint63 then x1 else x0.
 
 Lemma hex_digit_of_nibble_of_uint63 (i: int):
   hex_digit_of_nibble (nibble_of_uint63 i) = hex_digit_of_uint63 i.
 Proof.
 unfold hex_digit_of_nibble. unfold nibble_of_uint63. unfold hex_digit_of_uint63.
-destruct (0 < i land 8)%int63;
-  destruct (0 < i land 4)%int63;
-  destruct (0 < i land 2)%int63;
-  destruct (0 < i land 1)%int63; easy.
+destruct (0 <? i land 8)%uint63;
+  destruct (0 <? i land 4)%uint63;
+  destruct (0 <? i land 2)%uint63;
+  destruct (0 <? i land 1)%uint63; easy.
 Qed.
 
 Lemma nibble_of_uint63_of_N (n: N):
@@ -502,14 +502,14 @@ destruct a3; destruct a2; destruct a1; destruct a0; trivial.
 Qed.
 
 Definition byte_of_int (i: int)
-:= Byte (0 < (i land 128))%int63
-        (0 < (i land 64))%int63
-        (0 < (i land 32))%int63
-        (0 < (i land 16))%int63
-        (0 < (i land 8))%int63
-        (0 < (i land 4))%int63
-        (0 < (i land 2))%int63
-        (0 < (i land 1))%int63.
+:= Byte (0 <? (i land 128))%uint63
+        (0 <? (i land 64))%uint63
+        (0 <? (i land 32))%uint63
+        (0 <? (i land 16))%uint63
+        (0 <? (i land 8))%uint63
+        (0 <? (i land 4))%uint63
+        (0 <? (i land 2))%uint63
+        (0 <? (i land 1))%uint63.
 
 Definition int_of_byte (b: byte)
 := match b with
@@ -521,7 +521,7 @@ Definition int_of_byte (b: byte)
       let a3 := if b3 then   8 lor a4 else a4 in
       let a2 := if b2 then   4 lor a3 else a3 in
       let a1 := if b1 then   2 lor a2 else a2 in
-                if b0 then   1 lor a1 else a1)%int63
+                if b0 then   1 lor a1 else a1)%uint63
    end.
 
 Lemma byte_of_int_of_byte (b: byte):

Arith/UInt63.v

@@ -2,7 +2,7 @@
   This file continues theories/Numbers/Cyclic/Int63/Int63.v from the standard library of Coq.
  *)
 
-From Coq Require Import Int63 NArith ZArith Lia.
+From Coq Require Import Uint63 NArith ZArith Lia.
 
 From EVM Require Import Logic2 Arith2.
 
@@ -44,21 +44,21 @@ tauto.
 Qed.
 
 Lemma uint63_ltb_Z (x y: uint63):
-  (x < y)%int63 = (to_Z x <? to_Z y)%Z.
+  (x <? y)%uint63 = (to_Z x <? to_Z y)%Z.
 Proof.
 apply (relation_quad (fun x y => iff_refl _) Z.ltb_lt).
 apply ltb_spec.
 Qed.
 
 Lemma uint63_leb_Z (x y: uint63):
-  (x <= y)%int63 = (to_Z x <=? to_Z y)%Z.
+  (x <=? y)%uint63 = (to_Z x <=? to_Z y)%Z.
 Proof.
 apply (relation_quad (fun x y => iff_refl _) Z.leb_le).
 apply leb_spec.
 Qed.
 
 Lemma uint63_ltb_N (x y: uint63):
-  (x < y)%int63 = (N_of_uint63 x <? N_of_uint63 y)%N.
+  (x <? y)%uint63 = (N_of_uint63 x <? N_of_uint63 y)%N.
 Proof.
 rewrite uint63_ltb_Z.
 unfold N_of_uint63.
@@ -73,7 +73,7 @@ apply L.
 Qed.
 
 Lemma uint63_leb_N (x y: uint63):
-  (x <= y)%int63 = (N_of_uint63 x <=? N_of_uint63 y)%N.
+  (x <=? y)%uint63 = (N_of_uint63 x <=? N_of_uint63 y)%N.
 Proof.
 rewrite uint63_leb_Z.
 unfold N_of_uint63.
@@ -88,11 +88,11 @@ apply L.
 Qed.
 
 Lemma uint63_get_high_digit (i k: uint63)
-                            (B: (63 <= k)%int63 = true):
+                            (B: (63 <=? k)%uint63 = true):
   get_digit i k = false.
 Proof.
 unfold get_digit.
-enough (U: (1 << k = 0)%int63).
+enough (U: (1 << k = 0)%uint63).
 { 
   rewrite U.
   rewrite uint63_ltb_Z.
@@ -109,7 +109,7 @@ rewrite lsl_spec.
 rewrite to_Z_1. rewrite to_Z_0.
 rewrite Z.mul_1_l.
 rewrite uint63_leb_Z in B.
-replace (to_Z 63%int63) with 63%Z in B. 2:{ trivial. }
+replace (to_Z 63%uint63) with 63%Z in B. 2:{ trivial. }
 remember (to_Z k) as n. clear i k Heqn.
 remember (n - 63)%Z as m.
 assert (Q: n = (m + 63)%Z). { subst. lia. }
@@ -121,7 +121,7 @@ Qed.
 Lemma uint63_testbit_Z (i k: uint63):
   get_digit i k = Z.testbit (to_Z i) (to_Z k).
 Proof.
-remember (k < 63)%int63 as Low. symmetry in HeqLow.
+remember (k <? 63)%uint63 as Low. symmetry in HeqLow.
 destruct Low.
 { 
   unfold get_digit.
@@ -130,8 +130,8 @@ destruct Low.
   rewrite lsl_spec.
   remember (to_Z i) as n.
   remember (to_Z k) as m.
-  replace (to_Z 0%int63) with 0%Z. 2:{ trivial. }
-  replace (to_Z 1%int63) with 1%Z. 2:{ trivial. }
+  replace (to_Z 0%uint63) with 0%Z. 2:{ trivial. }
+  replace (to_Z 1%uint63) with 1%Z. 2:{ trivial. }
   rewrite Z.mul_1_l.
   rewrite Z.mod_small.
   2:{
@@ -154,7 +154,7 @@ subst. tauto.
 assert(Bk: (63 <= to_Z k)%Z).
 {
   rewrite uint63_ltb_Z in HeqLow.
-  replace (to_Z 63%int63) with 63%Z in HeqLow. 2:{ trivial. }
+  replace (to_Z 63%uint63) with 63%Z in HeqLow. 2:{ trivial. }
   rewrite Z.ltb_ge in HeqLow.
   assumption.
 }
@@ -197,23 +197,23 @@ Qed.
 (**************************************************************************)
 
 Lemma uint63_land_N (x y: uint63):
-  N_of_uint63 (x land y)%int63 = N.land (N_of_uint63 x) (N_of_uint63 y).
+  N_of_uint63 (x land y)%uint63 = N.land (N_of_uint63 x) (N_of_uint63 y).
 Proof.
 unfold N_of_uint63.
 rewrite land_spec'.
 apply Z_to_N_land; apply Z_of_uint63_nonneg.
 Qed.
 
 Lemma uint63_lor_N (x y: uint63):
-  N_of_uint63 (x lor y)%int63 = N.lor (N_of_uint63 x) (N_of_uint63 y).
+  N_of_uint63 (x lor y)%uint63 = N.lor (N_of_uint63 x) (N_of_uint63 y).
 Proof.
 unfold N_of_uint63.
 rewrite lor_spec'.
 apply Z_to_N_lor; apply Z_of_uint63_nonneg.
 Qed.
 
 Lemma uint63_lxor_N (x y: uint63):
-  N_of_uint63 (x lxor y)%int63 = N.lxor (N_of_uint63 x) (N_of_uint63 y).
+  N_of_uint63 (x lxor y)%uint63 = N.lxor (N_of_uint63 x) (N_of_uint63 y).
 Proof.
 unfold N_of_uint63.
 rewrite lxor_spec'.