ci: add translation of a Keccak example file

Author: clarus

.github/workflows/rocq.yml

@@ -26,20 +26,33 @@ jobs:
         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 RocqOfNoir/rocq-of-noir.opam
           endGroup
           startGroup "Change permissions"
             sudo chown -R $(whoami) .
           endGroup
+          startGroup "Generate JSON representation"
+            cargo install --path tooling/nargo_cli
+            cd noir_stdlib
+            nargo test hash::keccak::tests::smoke_test --show-monomorphized
+            cd ..
+          endGroup
           startGroup "Convert to Rocq"
+            python scripts/rocq_of_noir.py noir_stdlib/monomorphized_program.json >RocqOfNoir/keccak_monomorphic.v
             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 Rocq translations"
             cd RocqOfNoir
             make
             cd ..
           endGroup
+          startGroup "Check that the diff is empty (excluding submodules)"
+            # We remove these files as the generation is not yet deterministic
+            rm noir_stdlib/monomorphized_program.json
+            rm RocqOfNoir/keccak_monomorphic.v
+            git -c color.ui=always diff --exit-code --ignore-submodules=dirty
+          endGroup

README.md

@@ -1,11 +1,16 @@
 # ◼️🐓 rocq-of-noir
 
-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! 🛡️
+The tool `rocq-of-noir` provides 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 `rocq-of-noir` to verify your smart contracts!
 
 ## 🏎️ Getting Started
 
+1. Install the `rocq-of-noir` fork of the Noir compiler:
+
+```bash
+```
+
 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

RocqOfNoir/RocqOfNoir.v

@@ -290,9 +290,9 @@ Module M.
       (at level 100).
 
     Notation "[[ e ]]" :=
-      (ltac:(M.monadic e))
+      (* (ltac:(M.monadic e)) *)
       (* Use the version below for debugging and show errors that are made obscure by the tactic *)
-      (* (M.pure e) *)
+      (M.pure e)
       (only parsing).
   End Notations.
   Import Notations.
@@ -508,12 +508,18 @@ Export M.Notations.
 
 Parameter get_function : forall (name : string) (id : Z), Value.t.
 
+Parameter get_global : forall (name : string) (id : Z), Value.t.
+
+Parameter get_low_level : forall (name : string), Value.t.
+
 Definition closure (definition : list Value.t -> M.t) : Value.t :=
   Value.Closure (existS (Value.t, M.t) definition).
 
 Module Builtin.
   Parameter __to_be_radix : Value.t.
 
+  Parameter __to_le_radix : Value.t.
+
   Parameter as_bytes : Value.t.
 
   Parameter assert_constant : Value.t.