ci: add Coq tests

Author: clarus

.github/workflows/coq.yml

@@ -0,0 +1,58 @@
+name: Coq
+
+on:
+  push:
+    branches:
+      - master
+  pull_request:
+
+jobs:
+  build:
+    runs-on: ubuntu-latest
+    strategy:
+      matrix:
+        target: [x86_64-unknown-linux-gnu]
+
+    steps:
+    - name: Checkout Noir repo
+      uses: actions/checkout@v4
+
+    - name: Download Git submodules
+      run: git submodule update --init --recursive
+
+    - name: Run the Coq tests
+      uses: coq-community/docker-coq-action@v1
+      with:
+        custom_image: coqorg/coq:8.17-ocaml-4.14-flambda
+        custom_script: |
+          startGroup "Install dependencies"
+            curl --proto '=https' --tlsv1.2 -sSf https://sh.rustup.rs | sh -s -- -y
+            source "$HOME/.cargo/env"
+            cargo --version
+            sudo ln -s `which python3` /usr/bin/python
+            opam install -y --deps-only CoqOfNoir/coq-of-noir.opam
+          endGroup
+          startGroup "Install"
+            sudo chown -R $(whoami) .
+            cargo install --package nargo_cli
+          endGroup
+          startGroup "Checkout noir_base64 example"
+            git checkout https://github.com/noir-lang/noir_base64.git
+            cd noir_base64/
+            git checkout eb933f20b8175132f8e965e519b98c41ad805af1
+            cd ..
+          endGroup
+          startGroup "Convert to Coq"
+            cd noir_base64/
+            nargo test --show-monomorphized
+            cd ..
+            python scripts/coq_of_noir.py noir_base64/monomorphized_program.json >CoqOfNoir/base64/translation.v
+          endGroup
+          startGroup "Check that the diff is empty (excluding submodules)"
+            git -c color.ui=always diff --exit-code --ignore-submodules=dirty
+          endGroup
+          startGroup "Compile Coq translations"
+            cd CoqOfNoir
+            make
+            cd ..
+          endGroup

CoqOfNoir/coq-of-noir.opam

@@ -0,0 +1,24 @@
+opam-version: "2.0"
+name: "coq-of-noir"
+version: "0.1"
+synopsis: "Coq of Noir"
+description: """
+Formal verification for Noir by translation to the proof system Coq
+"""
+maintainer: "Guillaume Claret <dev@clarus.me>"
+authors: [
+  "Formal Land <contact@formal.land>"
+]
+license: "MIT and APACHE-2.0"
+homepage: "https://github.com/formal-land/coq-of-noir"
+bug-reports: "https://github.com/formal-land/coq-of-noir/issues"
+dev-repo: "git+https://github.com/formal-land/coq-of-noir.git"
+depends: [
+  "ocaml" {>= "4.08"}
+  "coq" {>= "8.17.1" & < "8.18"}
+  "coq-hammer" {>= "1.3.2+8.17" & < "1.3.2+8.18"}
+  "coq-coqutil" {>= "0.0.5"}
+]
+build: [
+  [make]
+]