doc: rename the proof assistant to Rocq

Author: clarus

.github/workflows/coq.yml .github/workflows/rocq.yml.github/workflows/coq.yml renamed to .github/workflows/rocq.yml

@@ -1,4 +1,4 @@
-name: Coq
+name: Rocq
 
 on:
   push:
@@ -20,26 +20,26 @@ jobs:
     - name: Download Git submodules
       run: git submodule update --init --recursive
 
-    - name: Run the Coq tests
+    - name: Run the Rocq tests
       uses: coq-community/docker-coq-action@v1
       with:
         custom_image: coqorg/coq:8.17-ocaml-4.14-flambda
         custom_script: |
           startGroup "Install dependencies"
             sudo ln -s `which python3` /usr/bin/python
-            opam install -y --deps-only CoqOfNoir/coq-of-noir.opam
+            opam install -y --deps-only RocqOfNoir/rocq-of-noir.opam
           endGroup
           startGroup "Change permissions"
             sudo chown -R $(whoami) .
           endGroup
-          startGroup "Convert to Coq"
-            python scripts/coq_of_noir.py CoqOfNoir/base64/monomorphized_program.json >CoqOfNoir/base64/monomorphic.v
+          startGroup "Convert to Rocq"
+            python scripts/rocq_of_noir.py RocqOfNoir/base64/monomorphized_program.json >RocqOfNoir/base64/monomorphic.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
+          startGroup "Compile Rocq translations"
+            cd RocqOfNoir
             make
             cd ..
           endGroup

README.md

@@ -1,36 +1,37 @@
-# ◼️🐓 coq-of-noir
+# ◼️🐓 rocq-of-noir
 
-With `coq-of-noir`, we provide an **open-source and extensive way to formally verify smart contracts written in ⬛ Noir**. Formal verification is about checking for any possible input that your code has no security issues, what is essential for code deployed on the blockchain! 🛡️
+With `rocq-of-noir`, we provide an **open-source and extensive way to formally verify smart contracts written in ⬛ Noir**. Formal verification is about checking for any possible input that your code has no security issues, what is essential for code deployed on the blockchain! 🛡️
 
-To keep things simple, we rely on the well-known proof assistant [Rocq](https://rocq-prover.org/) for all the verification work: if you are already knowledgeable into this system, you can readily use `coq-of-noir` to verify your smart contracts!
+To keep things simple, we rely on the well-known proof assistant [Rocq](https://rocq-prover.org/) for all the verification work: if you are already knowledgeable into this system, you can readily use `rocq-of-noir` to verify your smart contracts!
 
 ## 🏎️ Getting Started
 
-Follow what we do in our CI file [coq.yml](.github/workflows/coq.yml). Sorry for not having the time to provide more explanations!
+Follow what we do in our CI file [rocq.yml](.github/workflows/rocq.yml). Sorry for not having the time to provide more explanations!
 
 ## ✅ What Works
 
-The following steps work:
+The following functionalities are currently implemented:
 
-- A generated translation of the `base64` library of Noir to Coq in a code that compiles; we should thus support a large part of the Noir language.
-- Semantics rules to reason on code like the above together with a proof strategy. This should already cover most of the Noir language.
-- A formally verified functional specification of one of the functions with a loop from the `base64` library, exercising mutations and array access. We consider this to be our main test to see that `coq-of-noir` can work on non-trivial examples.
+- **Translation:** Automatic translation of Noir programs to a representation in Rocq.
+- **Semantics:** Formal semantics for reasoning about the translated Noir code.
+- **Proof Strategy:** A proof strategy to formally verify properties of Noir programs.
+- **Verified Example:** A verified functional specification of a non-trivial example (base64 loop) demonstrating mutation and array access handling.
 
-Note that the proof process is still very verbose, and this tool is still a work in progress. Contact us at [contact@formal.land](mailto:contact@formal.land) or by direct message on our [X account](https://x.com/FormalLand) if you are interested.
+Contact us at [contact@formal.land](mailto:contact@formal.land) or by direct message on our [X account](https://x.com/FormalLand) if you are interested.
 
 ## 🔭 Goal and Vision
 
 The goal is to enable each team developing critical applications (meaning handling user money) to verify the correctness of their code with the higest degree of certainty thanks to **formal verification**.
 
-For those who do not know, formal verification is a technique to verify software for 100% of possible execution parameters. **This means that the code cannot have bugs or vulnerabilities!** Initially applied to software from the spacial/defense industry, the key idea is to mathematically reason about the code to talk about possibly infinitely many possible cases, and to verify all the reasoning by a dedicated tool called a proof checker, in our case 🐓 Coq.
+For those who do not know, formal verification is a technique to verify software for 100% of possible execution parameters. **This means that the code cannot have bugs or vulnerabilities!** Initially applied to software from the spacial/defense industry, the key idea is to mathematically reason about the code to talk about possibly infinitely many possible cases, and to verify all the reasoning by a dedicated tool called a proof checker, in our case 🐓 Rocq.
 
-In this repository, we provide a command to automatically translate a Noir program to a representation in Coq. We translate the code after the monomorphisation phase of the Noir compiler so that we do not have to deal with polymorphism or type classes. Instead, one can reconstruct this organization of the code on the Coq side in a refinement step, if needed.
+In this repository, we provide a command to automatically translate a Noir program to a representation in Rocq. We translate the code after the monomorphisation phase of the Noir compiler so that we do not have to deal with polymorphism or type classes. Instead, one can reconstruct this organization of the code on the Rocq side in a refinement step, if needed.
 
 This translation is a shallow embedding optimized to write specifications and proofs about the code. As we erase all the types during the translation to keep only the values, we recommend doing a first proof step that reconstructs these types. This first proof step is also an opportunity to explicit the structure of the global state.
 
 Our initial target is to verify a part of the [base64](https://github.com/noir-lang/noir_base64), which uses field arithmetic for optimizations. It also includes many loops, which are generally non-trivial to fully verify with formal verification.
 
-_If you have a Noir project that you want to formally verify, either start using `coq-of-noir` or contact us!_
+_If you have a Noir project that you want to formally verify, either start using `rocq-of-noir` or contact us!_
 
 ## 📚 Blog posts
 
@@ -41,4 +42,4 @@ Here are some blog posts featuring this tool:
 
 ## ⚖️ License
 
-`coq-of-noir` is free and **open source**. It is distributed under a dual license. (MIT/APACHE) The translation phase is based on the code of the Noir compiler to maximize code reuse.
+`rocq-of-noir` is free and **open source**. It is distributed under a dual license. (MIT/APACHE) The translation phase is based on the code of the Noir compiler to maximize code reuse.

CoqOfNoir/.gitignore RocqOfNoir/.gitignoreCoqOfNoir/.gitignore renamed to RocqOfNoir/.gitignore

@@ -1,2 +1,2 @@
--R . CoqOfNoir
+-R . RocqOfNoir
 -arg -impredicative-set

CoqOfNoir/Makefile RocqOfNoir/MakefileCoqOfNoir/Makefile renamed to RocqOfNoir/Makefile

@@ -1,4 +1,4 @@
-Require Import CoqOfNoir.CoqOfNoir.
+Require Import RocqOfNoir.RocqOfNoir.
 
 (*
   fn encode_and_decode$f0() -> () {

CoqOfNoir/RecordUpdate.v RocqOfNoir/RecordUpdate.vCoqOfNoir/RecordUpdate.v renamed to RocqOfNoir/RecordUpdate.v

@@ -1,5 +1,5 @@
-Require Import CoqOfNoir.CoqOfNoir.
-Require Import simulation.CoqOfNoir.
+Require Import RocqOfNoir.RocqOfNoir.
+Require Import simulation.RocqOfNoir.
 Require Import base64.monomorphic.
 
 (** This module provides helpers to show the equality to debug [reflexivity] when it is too long or