ci: add Circom as third-party and CI file

.github/workflows/coq.yml

@@ -0,0 +1,53 @@
+name: Coq
+
+on:
+  push:
+    branches: [ "main" ]
+  pull_request:
+    branches: [ "main" ]
+
+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.20-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 Garden/coq-garden.opam
+          endGroup
+          startGroup "Set the rights"
+            sudo chown -R $(whoami) .
+          endGroup
+          startGroup "Install Circom"
+            cd third-party/circom
+            cargo install --path circom
+            cd ../..
+          endGroup
+          startGroup "Translate Circom library"
+            cd third-party/circomlib/test/circuits
+            circom greaterthan.circom
+            cd ../../../..
+            python scripts/coq_of_circom.py third-party/circomlib/circuits/binsum.json > Garden/Circom/Example/binsum.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 project"
+            cd Garden
+            make
+            cd ..
+          endGroup

.gitmodules

@@ -0,0 +1,6 @@
+[submodule "third-parties/circom"]
+	path = third-party/circom
+	url = https://github.com/formal-land/circom.git
+[submodule "third-party/circomlib"]
+	path = third-party/circomlib
+	url = https://github.com/iden3/circomlib.git

Garden/.gitignore

@@ -0,0 +1,11 @@
+.lia.cache
+.nia.cache
+.CoqMakefile.d
+_CoqProject
+CoqMakefile
+CoqMakefile.conf
+*.vo
+*.vok
+*.vos
+*.glob
+.*.aux

Garden/Circom/Example/binsum.v

@@ -0,0 +1,83 @@
+
+(* Generated by Garden *)
+Require Import Garden.Garden.
+
+(* Function *)
+Definition nbits (a : F.t) : M.t F.t :=
+  M.function_body (
+    (* Var *)
+    do~ M.declare_var "n" [[ [] ]] in
+    do~ M.substitute "n" [[ 1 ]] in
+    (* Var *)
+    do~ M.declare_var "r" [[ [] ]] in
+    do~ M.substitute "r" [[ 0 ]] in
+    do~ M.while [[ InfixOp.Lesser ~(| InfixOp.Sub ~(| M.var ~(| "n" |), 1 |), M.var ~(| "a" |) |)]]
+      do~ M.substitute "r" [[ InfixOp.Add ~(| M.var ~(| "r" |), 1 |) ]] in
+      do~ M.substitute "n" [[ InfixOp.Mul ~(| M.var ~(| "n" |), 1 |) ]] in
+      M.pure tt
+    in
+    do~ M.return [[ M.var ~(| "r" |) ]] in
+    M.pure tt
+  ).
+
+(* Template *)
+Definition BinSum (n ops : F.t) : Template.t F.t :=
+  (* Var *)
+  do~ M.declare_var "nout" [[ [] ]] in
+  do~ M.substitute "nout" [[ nbits ~(| InfixOp.Mul ~(| InfixOp.Sub ~(| InfixOp.Pow ~(| 1, M.var ~(| "n" |) |), 1 |), M.var ~(| "ops" |) |) |) ]] in
+  (* Signal Input *)
+  do~ M.declare_signal "in" [[ [M.var ~(| "ops" |); M.var ~(| "n" |)] ]] in
+  (* Signal Output *)
+  do~ M.declare_signal "out" [[ [M.var ~(| "nout" |)] ]] in
+  (* Var *)
+  do~ M.declare_var "lin" [[ [] ]] in
+  do~ M.substitute "lin" [[ 0 ]] in
+  (* Var *)
+  do~ M.declare_var "lout" [[ [] ]] in
+  do~ M.substitute "lout" [[ 0 ]] in
+  (* Var *)
+  do~ M.declare_var "k" [[ [] ]] in
+  do~ M.substitute "k" [[ 0 ]] in
+  (* Var *)
+  do~ M.declare_var "j" [[ [] ]] in
+  do~ M.substitute "j" [[ 0 ]] in
+  (* Var *)
+  do~ M.declare_var "e2" [[ [] ]] in
+  do~ M.substitute "e2" [[ 0 ]] in
+  do~ M.substitute "e2" [[ 1 ]] in
+  do~ M.substitute "k" [[ 0 ]] in
+  do~ M.while [[ InfixOp.Lesser ~(| M.var ~(| "k" |), M.var ~(| "n" |) |)]]
+    do~ M.substitute "j" [[ 0 ]] in
+    do~ M.while [[ InfixOp.Lesser ~(| M.var ~(| "j" |), M.var ~(| "ops" |) |)]]
+      do~ M.substitute "lin" [[ InfixOp.Add ~(| M.var ~(| "lin" |), InfixOp.Mul ~(| M.var_access ~(| "in", [Access.Array M.var ~(| "j" |); Access.Array M.var ~(| "k" |)] |), M.var ~(| "e2" |) |) |) ]] in
+      M.pure tt
+      do~ M.substitute "j" [[ InfixOp.Add ~(| M.var ~(| "j" |), 1 |) ]] in
+      M.pure tt
+    in
+    M.pure tt
+    do~ M.substitute "e2" [[ InfixOp.Add ~(| M.var ~(| "e2" |), M.var ~(| "e2" |) |) ]] in
+    M.pure tt
+    do~ M.substitute "k" [[ InfixOp.Add ~(| M.var ~(| "k" |), 1 |) ]] in
+    M.pure tt
+  in
+  M.pure tt
+  do~ M.substitute "e2" [[ 1 ]] in
+  do~ M.substitute "k" [[ 0 ]] in
+  do~ M.while [[ InfixOp.Lesser ~(| M.var ~(| "k" |), M.var ~(| "nout" |) |)]]
+    do~ M.substitute "out" [[ InfixOp.BitAnd ~(| InfixOp.ShiftR ~(| M.var ~(| "lin" |), M.var ~(| "k" |) |), 1 |) ]] in
+    do~ M.equality_constraint
+      [[ InfixOp.Mul ~(| M.var_access ~(| "out", [Access.Array M.var ~(| "k" |)] |), InfixOp.Sub ~(| M.var_access ~(| "out", [Access.Array M.var ~(| "k" |)] |), 1 |) |) ]]
+      [[ 0 ]]
+    in
+    do~ M.substitute "lout" [[ InfixOp.Add ~(| M.var ~(| "lout" |), InfixOp.Mul ~(| M.var_access ~(| "out", [Access.Array M.var ~(| "k" |)] |), M.var ~(| "e2" |) |) |) ]] in
+    do~ M.substitute "e2" [[ InfixOp.Add ~(| M.var ~(| "e2" |), M.var ~(| "e2" |) |) ]] in
+    M.pure tt
+    do~ M.substitute "k" [[ InfixOp.Add ~(| M.var ~(| "k" |), 1 |) ]] in
+    M.pure tt
+  in
+  M.pure tt
+  do~ M.equality_constraint
+    [[ M.var ~(| "lin" |) ]]
+    [[ M.var ~(| "lout" |) ]]
+  in
+  M.pure tt.

Garden/Garden.v

@@ -0,0 +1,117 @@
+Require Export Coq.Strings.Ascii.
+Require Coq.Strings.HexString.
+Require Export Coq.Strings.String.
+Require Export Coq.ZArith.ZArith.
+From Ltac2 Require Ltac2.
+Require Export RecordUpdate.
+
+Require Export Lia.
+From Hammer Require Export Tactics.
+
+(* Activate the modulo arithmetic in [lia] *)
+Ltac Zify.zify_post_hook ::= Z.to_euclidean_division_equations.
+
+Global Set Primitive Projections.
+Global Set Printing Projections.
+Global Open Scope char_scope.
+Global Open Scope string_scope.
+Global Open Scope list_scope.
+Global Open Scope type_scope.
+Global Open Scope Z_scope.
+Global Open Scope bool_scope.
+
+Export List.ListNotations.
+
+Inductive sigS {A : Type} (P : A -> Set) : Set :=
+| existS : forall (x : A), P x -> sigS P.
+Arguments existS {_ _}.
+
+Reserved Notation "{ x @ P }" (at level 0, x at level 99).
+Reserved Notation "{ x : A @ P }" (at level 0, x at level 99).
+Reserved Notation "{ ' pat : A @ P }"
+  (at level 0, pat strict pattern, format "{ ' pat : A @ P }").
+
+Notation "{ x @ P }" := (sigS (fun x => P)) : type_scope.
+Notation "{ x : A @ P }" := (sigS (A := A) (fun x => P)) : type_scope.
+Notation "{ ' pat : A @ P }" := (sigS (A := A) (fun pat => P)) : type_scope.
+
+Module F.
+  Definition t := Z.
+End F.
+
+Module BlockUnit.
+  (** The return value of a code block. *)
+  Inductive t : Set :=
+  (** The default value *)
+  | Tt
+  (** The instruction `return` was called *)
+  | Return (value : F.t).
+End BlockUnit.
+
+Module Primitive.
+  (** We group together primitives that share being impure functions operating over the state. *)
+  Inductive t : Set -> Set :=
+  | OpenScope : t unit
+  | CloseScope : t unit
+  | DeclareVar (names : list string) (values : list F.t) : t unit
+  | AssignVar (names : list string) (values : list F.t) : t unit
+  | GetVar (name : string) : t F.t.
+End Primitive.
+
+Module M.
+  Inductive t (A : Set) : Set :=
+  | Pure
+      (output : A)
+  | Primitive {B : Set}
+      (primitive : Primitive.t B)
+      (k : B -> t A)
+  | Loop {In Out : Set}
+      (init : In)
+      (body : In -> t Out)
+      (** The final value to return if we decide to break of the loop, otherwise what to continue
+          with. *)
+      (break_with : Out -> In + Out)
+      (k : Out -> t A)
+  (** Explicit cut in the monadic expressions, to provide better composition for the proofs. *)
+  | Let {B : Set} (e1 : t B) (k : B -> t A)
+  (** Similar to [Let], a marker to help for the proofs. *)
+  | Call {B : Set} (e : t B) (k : B -> t A)
+  | Impossible (message : string).
+  Arguments Pure {_}.
+  Arguments Primitive {_ _}.
+  Arguments Loop {_ _ _}.
+  Arguments Let {_ _}.
+  Arguments Call {_ _}.
+  Arguments Impossible {_}.
+
+  Fixpoint let_ {A B : Set} (e1 : t A) (e2 : A -> t B) : t B :=
+    match e1 with
+    | Pure (output) =>
+      e2 output
+    | Primitive primitive k =>
+      Primitive primitive (fun result => let_ (k result) e2)
+    | Loop input body break_with k =>
+      Loop input body break_with (fun result => let_ (k result) e2)
+    | Let e1 k =>
+      Let e1 (fun result => let_ (k result) e2)
+    | Call e k =>
+      Call e (fun result => let_ (k result) e2)
+    | Impossible message => Impossible message
+    end.
+
+  Definition do (block1 block2 : t BlockUnit.t) : t BlockUnit.t :=
+    Let block1 (fun (result : BlockUnit.t) =>
+    match result with
+    | BlockUnit.Tt => block2
+    | BlockUnit.Return _ => block1
+    end).
+
+  Definition function_body (block : t BlockUnit.t) : t F.t :=
+    Primitive Primitive.OpenScope (fun _ =>
+    Let block (fun (result : BlockUnit.t) =>
+    Primitive Primitive.CloseScope (fun _ =>
+    match result with
+    | BlockUnit.Tt => Impossible "Expected a return in the function body"
+    | BlockUnit.Return value => Pure value
+    end))).
+End M.

Garden/Makefile

@@ -0,0 +1,31 @@
+.PHONY: all clean clean-util distclean default
+
+VFILES := $(shell find -L . -name "*.v" | grep -v -f blacklist.txt | sort)
+
+default: all
+
+CoqMakefile: $(VFILES) blacklist.txt
+	echo "-R . Garden" > _CoqProject
+	echo "-arg -impredicative-set -arg -w -arg -stdlib-vector" >> _CoqProject
+	# We copy & paste the command to find files as this variable is too long on command line
+	find -L . -name "*.v" | grep -v -f blacklist.txt | sort >> _CoqProject
+	coq_makefile -f _CoqProject -o $@
+
+MAKECOQ := +$(MAKE) -f CoqMakefile
+
+%.vo: CoqMakefile %.v
+	$(MAKECOQ) $@
+
+all: CoqMakefile
+	$(MAKECOQ) all
+
+clean-coq: CoqMakefile
+	$(MAKECOQ) clean
+
+clean-util:
+	rm -f *CoqMakefile*
+
+clean: clean-coq
+	$(MAKE) clean-util # done separately to enforce order
+
+distclean: clean