circom: translate all the circomlib examples

.github/workflows/coq.yml

@@ -38,19 +38,12 @@ jobs:
             cd ../..
           endGroup
           startGroup "Translate Circom library"
-            cd third-party/circomlib/test/circuits
-            # For each Circom circuit
-            for circuit in *.circom; do
-              # Translate the circuit to JSON
-              circom $circuit
-            done
-            cd ../../../..
-            # For each JSON circuit
-            for circuit in third-party/circomlib/circuits/*.json; do
-              # Translate the JSON circuit to Coq
-              echo "Translating $circuit"
-              python scripts/coq_of_circom.py $circuit > Garden/Circom/Example/$(basename $circuit .json).v
-            done
+            cd third-party/circomlib
+            # Translate each Circom circuit to JSON
+            find . -name '*.circom' -execdir circom {} \;
+            cd ../..
+            # Translate the JSON to Coq
+            python scripts/coq_of_circom_ci.py
           endGroup
           startGroup "Check that the diff is empty (excluding submodules)"
             git -c color.ui=always diff --exit-code --ignore-submodules=dirty

Garden/Circom/Circomlib/proof/circuits/binsum.v

@@ -0,0 +1,32 @@
+Require Import Garden.Garden.
+Require Circom.Circomlib.translation.circuits.binsum.
+
+Import Run.
+
+Lemma run_nbits (p : Z) :
+  {{ p , Scopes.empty ⏩ binsum.nbits 6 🔽 23 ⏩ Scopes.empty }}.
+Proof.
+  unfold binsum.nbits.
+  unfold M.function_body; cbn.
+  eapply Run.Let. {
+    eapply Run.Let. {
+      apply Run.PrimitiveDeclareVar.
+      apply Run.Pure.
+    }
+    eapply Run.Let. {
+      apply Run.PrimitiveSubstituteVar.
+      apply Run.Pure.
+    }
+    eapply Run.Let. {
+      apply Run.PrimitiveDeclareVar.
+      apply Run.Pure.
+    }
+    eapply Run.Let. {
+      apply Run.PrimitiveSubstituteVar.
+      apply Run.Pure.
+    }
+    cbn.
+    eapply Run.Let. {
+      eapply Run.LoopNext. {
+        eapply Run.Let. {
+Admitted.

Garden/Circom/Example/aliascheck.v → Garden/Circom/Circomlib/translation/circuits/aliascheck.v

@@ -1,4 +1,3 @@
-
 (* Generated by Garden *)
 Require Import Garden.Garden.
 

Garden/Circom/Example/babyjub.v → Garden/Circom/Circomlib/translation/circuits/babyjub.v

@@ -1,4 +1,3 @@
-
 (* Generated by Garden *)
 Require Import Garden.Garden.
 

Garden/Circom/Example/binsub.v → Garden/Circom/Circomlib/translation/circuits/binsub.v

@@ -1,4 +1,3 @@
-
 (* Generated by Garden *)
 Require Import Garden.Garden.
 

Garden/Circom/Example/binsum.v → Garden/Circom/Circomlib/translation/circuits/binsum.v

@@ -1,4 +1,3 @@
-
 (* Generated by Garden *)
 Require Import Garden.Garden.
 

Garden/Circom/Example/bitify.v → Garden/Circom/Circomlib/translation/circuits/bitify.v

@@ -1,4 +1,3 @@
-
 (* Generated by Garden *)
 Require Import Garden.Garden.
 

Garden/Circom/Example/comparators.v → Garden/Circom/Circomlib/translation/circuits/comparators.v

@@ -1,4 +1,3 @@
-
 (* Generated by Garden *)
 Require Import Garden.Garden.
 

Garden/Circom/Example/compconstant.v → Garden/Circom/Circomlib/translation/circuits/compconstant.v

@@ -1,4 +1,3 @@
-
 (* Generated by Garden *)
 Require Import Garden.Garden.
 

Garden/Circom/Example/eddsa.v → Garden/Circom/Circomlib/translation/circuits/eddsa.v

@@ -1,4 +1,3 @@
-
 (* Generated by Garden *)
 Require Import Garden.Garden.
 

Garden/Circom/Example/eddsamimc.v → Garden/Circom/Circomlib/translation/circuits/eddsamimc.v

@@ -1,4 +1,3 @@
-
 (* Generated by Garden *)
 Require Import Garden.Garden.
 

Garden/Circom/Example/eddsaposeidon.v → Garden/Circom/Circomlib/translation/circuits/eddsaposeidon.v

@@ -1,4 +1,3 @@
-
 (* Generated by Garden *)
 Require Import Garden.Garden.
 

Garden/Circom/Example/escalarmul.v → Garden/Circom/Circomlib/translation/circuits/escalarmul.v

@@ -1,4 +1,3 @@
-
 (* Generated by Garden *)
 Require Import Garden.Garden.
 

Garden/Circom/Example/escalarmulany.v → Garden/Circom/Circomlib/translation/circuits/escalarmulany.v

@@ -1,4 +1,3 @@
-
 (* Generated by Garden *)
 Require Import Garden.Garden.
 

Garden/Circom/Example/escalarmulfix.v → Garden/Circom/Circomlib/translation/circuits/escalarmulfix.v

@@ -1,4 +1,3 @@
-
 (* Generated by Garden *)
 Require Import Garden.Garden.
 

Garden/Circom/Example/escalarmulw4table.v → Garden/Circom/Circomlib/translation/circuits/escalarmulw4table.v

@@ -1,4 +1,3 @@
-
 (* Generated by Garden *)
 Require Import Garden.Garden.
 

Garden/Circom/Example/gates.v → Garden/Circom/Circomlib/translation/circuits/gates.v

@@ -1,4 +1,3 @@
-
 (* Generated by Garden *)
 Require Import Garden.Garden.
 

Garden/Circom/Example/mimc.v → Garden/Circom/Circomlib/translation/circuits/mimc.v

@@ -1,4 +1,3 @@
-
 (* Generated by Garden *)
 Require Import Garden.Garden.
 

Garden/Circom/Example/mimcsponge.v → Garden/Circom/Circomlib/translation/circuits/mimcsponge.v

@@ -1,4 +1,3 @@
-
 (* Generated by Garden *)
 Require Import Garden.Garden.
 

Garden/Circom/Example/montgomery.v → Garden/Circom/Circomlib/translation/circuits/montgomery.v

@@ -1,4 +1,3 @@
-
 (* Generated by Garden *)
 Require Import Garden.Garden.
 

Garden/Circom/Example/mux1.v → Garden/Circom/Circomlib/translation/circuits/mux1.v

@@ -1,4 +1,3 @@
-
 (* Generated by Garden *)
 Require Import Garden.Garden.
 

Garden/Circom/Example/mux2.v → Garden/Circom/Circomlib/translation/circuits/mux2.v

@@ -1,4 +1,3 @@
-
 (* Generated by Garden *)
 Require Import Garden.Garden.
 

Garden/Circom/Example/mux3.v → Garden/Circom/Circomlib/translation/circuits/mux3.v

@@ -1,4 +1,3 @@
-
 (* Generated by Garden *)
 Require Import Garden.Garden.
 

Garden/Circom/Example/mux4.v → Garden/Circom/Circomlib/translation/circuits/mux4.v

@@ -1,4 +1,3 @@
-
 (* Generated by Garden *)
 Require Import Garden.Garden.
 

Garden/Circom/Example/pedersen.v → Garden/Circom/Circomlib/translation/circuits/pedersen.v

@@ -1,4 +1,3 @@
-
 (* Generated by Garden *)
 Require Import Garden.Garden.
 

Garden/Circom/Example/pedersen_old.v → Garden/Circom/Circomlib/translation/circuits/pedersen_old.v

@@ -1,4 +1,3 @@
-
 (* Generated by Garden *)
 Require Import Garden.Garden.
 

Garden/Circom/Example/pointbits.v → Garden/Circom/Circomlib/translation/circuits/pointbits.v

@@ -1,4 +1,3 @@
-
 (* Generated by Garden *)
 Require Import Garden.Garden.
 

Garden/Circom/Example/poseidon.v → Garden/Circom/Circomlib/translation/circuits/poseidon.v

@@ -1,4 +1,3 @@
-
 (* Generated by Garden *)
 Require Import Garden.Garden.
 

Garden/Circom/Example/poseidon_constants.v → Garden/Circom/Circomlib/translation/circuits/poseidon_constants.v

@@ -1,4 +1,3 @@
-
 (* Generated by Garden *)
 Require Import Garden.Garden.
 

Garden/Circom/Circomlib/translation/circuits/sha256/ch.v

@@ -0,0 +1,32 @@
+(* Generated by Garden *)
+Require Import Garden.Garden.
+
+(* Template signals *)
+Module Ch_tSignals.
+  Record t : Set := {
+    a : list F.t;
+    b : list F.t;
+    c : list F.t;
+    out : list F.t;
+  }.
+End Ch_tSignals.
+
+(* Template body *)
+Definition Ch_t (n : F.t) : M.t (BlockUnit.t Empty_set) :=
+  (* Signal Input *)
+  do~ M.declare_signal "a" [[ [ M.var ~(| "n" |) ] ]] in
+  (* Signal Input *)
+  do~ M.declare_signal "b" [[ [ M.var ~(| "n" |) ] ]] in
+  (* Signal Input *)
+  do~ M.declare_signal "c" [[ [ M.var ~(| "n" |) ] ]] in
+  (* Signal Output *)
+  do~ M.declare_signal "out" [[ [ M.var ~(| "n" |) ] ]] in
+  (* Var *)
+  do~ M.declare_var "k" [[ ([] : list F.t) ]] in
+  do~ M.substitute_var "k" [[ 0 ]] in
+  do~ M.while [[ InfixOp.lesser ~(| M.var ~(| "k" |), M.var ~(| "n" |) |) ]] (
+    do~ M.substitute_var "out" [[ InfixOp.add ~(| InfixOp.mul ~(| M.var_access ~(| "a", [Access.Array (M.var ~(| "k" |))] |), InfixOp.sub ~(| M.var_access ~(| "b", [Access.Array (M.var ~(| "k" |))] |), M.var_access ~(| "c", [Access.Array (M.var ~(| "k" |))] |) |) |), M.var_access ~(| "c", [Access.Array (M.var ~(| "k" |))] |) |) ]] in
+    do~ M.substitute_var "k" [[ InfixOp.add ~(| M.var ~(| "k" |), 1 |) ]] in
+    M.pure BlockUnit.Tt
+  ) in
+  M.pure BlockUnit.Tt.

Garden/Circom/Circomlib/translation/circuits/sha256/constants.v

@@ -0,0 +1,52 @@
+(* Generated by Garden *)
+Require Import Garden.Garden.
+
+(* Template signals *)
+Module HSignals.
+  Record t : Set := {
+    out : list F.t;
+  }.
+End HSignals.
+
+(* Template body *)
+Definition H (x : F.t) : M.t (BlockUnit.t Empty_set) :=
+  (* Signal Output *)
+  do~ M.declare_signal "out" [[ [ 32 ] ]] in
+  (* Var *)
+  do~ M.declare_var "c" [[ [ 8 ] ]] in
+  do~ M.substitute_var "c" [[ array_with_repeat (0) (8) ]] in
+  do~ M.substitute_var "c" [[ [ 1779033703; 3144134277; 1013904242; 2773480762; 1359893119; 2600822924; 528734635; 1541459225 ] ]] in
+  (* Var *)
+  do~ M.declare_var "i" [[ ([] : list F.t) ]] in
+  do~ M.substitute_var "i" [[ 0 ]] in
+  do~ M.while [[ InfixOp.lesser ~(| M.var ~(| "i" |), 32 |) ]] (
+    do~ M.substitute_var "out" [[ InfixOp.bitAnd ~(| InfixOp.shiftR ~(| M.var_access ~(| "c", [Access.Array (M.var ~(| "x" |))] |), M.var ~(| "i" |) |), 1 |) ]] in
+    do~ M.substitute_var "i" [[ InfixOp.add ~(| M.var ~(| "i" |), 1 |) ]] in
+    M.pure BlockUnit.Tt
+  ) in
+  M.pure BlockUnit.Tt.
+
+(* Template signals *)
+Module KSignals.
+  Record t : Set := {
+    out : list F.t;
+  }.
+End KSignals.
+
+(* Template body *)
+Definition K (x : F.t) : M.t (BlockUnit.t Empty_set) :=
+  (* Signal Output *)
+  do~ M.declare_signal "out" [[ [ 32 ] ]] in
+  (* Var *)
+  do~ M.declare_var "c" [[ [ 64 ] ]] in
+  do~ M.substitute_var "c" [[ array_with_repeat (0) (64) ]] in
+  do~ M.substitute_var "c" [[ [ 1116352408; 1899447441; 3049323471; 3921009573; 961987163; 1508970993; 2453635748; 2870763221; 3624381080; 310598401; 607225278; 1426881987; 1925078388; 2162078206; 2614888103; 3248222580; 3835390401; 4022224774; 264347078; 604807628; 770255983; 1249150122; 1555081692; 1996064986; 2554220882; 2821834349; 2952996808; 3210313671; 3336571891; 3584528711; 113926993; 338241895; 666307205; 773529912; 1294757372; 1396182291; 1695183700; 1986661051; 2177026350; 2456956037; 2730485921; 2820302411; 3259730800; 3345764771; 3516065817; 3600352804; 4094571909; 275423344; 430227734; 506948616; 659060556; 883997877; 958139571; 1322822218; 1537002063; 1747873779; 1955562222; 2024104815; 2227730452; 2361852424; 2428436474; 2756734187; 3204031479; 3329325298 ] ]] in
+  (* Var *)
+  do~ M.declare_var "i" [[ ([] : list F.t) ]] in
+  do~ M.substitute_var "i" [[ 0 ]] in
+  do~ M.while [[ InfixOp.lesser ~(| M.var ~(| "i" |), 32 |) ]] (
+    do~ M.substitute_var "out" [[ InfixOp.bitAnd ~(| InfixOp.shiftR ~(| M.var_access ~(| "c", [Access.Array (M.var ~(| "x" |))] |), M.var ~(| "i" |) |), 1 |) ]] in
+    do~ M.substitute_var "i" [[ InfixOp.add ~(| M.var ~(| "i" |), 1 |) ]] in
+    M.pure BlockUnit.Tt
+  ) in
+  M.pure BlockUnit.Tt.

Garden/Circom/Circomlib/translation/circuits/sha256/maj.v

@@ -0,0 +1,36 @@
+(* Generated by Garden *)
+Require Import Garden.Garden.
+
+(* Template signals *)
+Module Maj_tSignals.
+  Record t : Set := {
+    a : list F.t;
+    b : list F.t;
+    c : list F.t;
+    out : list F.t;
+    mid : list F.t;
+  }.
+End Maj_tSignals.
+
+(* Template body *)
+Definition Maj_t (n : F.t) : M.t (BlockUnit.t Empty_set) :=
+  (* Signal Input *)
+  do~ M.declare_signal "a" [[ [ M.var ~(| "n" |) ] ]] in
+  (* Signal Input *)
+  do~ M.declare_signal "b" [[ [ M.var ~(| "n" |) ] ]] in
+  (* Signal Input *)
+  do~ M.declare_signal "c" [[ [ M.var ~(| "n" |) ] ]] in
+  (* Signal Output *)
+  do~ M.declare_signal "out" [[ [ M.var ~(| "n" |) ] ]] in
+  (* Signal Intermediate *)
+  do~ M.declare_signal "mid" [[ [ M.var ~(| "n" |) ] ]] in
+  (* Var *)
+  do~ M.declare_var "k" [[ ([] : list F.t) ]] in
+  do~ M.substitute_var "k" [[ 0 ]] in
+  do~ M.while [[ InfixOp.lesser ~(| M.var ~(| "k" |), M.var ~(| "n" |) |) ]] (
+    do~ M.substitute_var "mid" [[ InfixOp.mul ~(| M.var_access ~(| "b", [Access.Array (M.var ~(| "k" |))] |), M.var_access ~(| "c", [Access.Array (M.var ~(| "k" |))] |) |) ]] in
+    do~ M.substitute_var "out" [[ InfixOp.add ~(| InfixOp.mul ~(| M.var_access ~(| "a", [Access.Array (M.var ~(| "k" |))] |), InfixOp.sub ~(| InfixOp.add ~(| M.var_access ~(| "b", [Access.Array (M.var ~(| "k" |))] |), M.var_access ~(| "c", [Access.Array (M.var ~(| "k" |))] |) |), InfixOp.mul ~(| 2, M.var_access ~(| "mid", [Access.Array (M.var ~(| "k" |))] |) |) |) |), M.var_access ~(| "mid", [Access.Array (M.var ~(| "k" |))] |) |) ]] in
+    do~ M.substitute_var "k" [[ InfixOp.add ~(| M.var ~(| "k" |), 1 |) ]] in
+    M.pure BlockUnit.Tt
+  ) in
+  M.pure BlockUnit.Tt.

Garden/Circom/Circomlib/translation/circuits/sha256/rotate.v

@@ -0,0 +1,26 @@
+(* Generated by Garden *)
+Require Import Garden.Garden.
+
+(* Template signals *)
+Module RotRSignals.
+  Record t : Set := {
+    in_ : list F.t;
+    out : list F.t;
+  }.
+End RotRSignals.
+
+(* Template body *)
+Definition RotR (n r : F.t) : M.t (BlockUnit.t Empty_set) :=
+  (* Signal Input *)
+  do~ M.declare_signal "in" [[ [ M.var ~(| "n" |) ] ]] in
+  (* Signal Output *)
+  do~ M.declare_signal "out" [[ [ M.var ~(| "n" |) ] ]] in
+  (* Var *)
+  do~ M.declare_var "i" [[ ([] : list F.t) ]] in
+  do~ M.substitute_var "i" [[ 0 ]] in
+  do~ M.while [[ InfixOp.lesser ~(| M.var ~(| "i" |), M.var ~(| "n" |) |) ]] (
+    do~ M.substitute_var "out" [[ M.var_access ~(| "in", [Access.Array (InfixOp.mod_ ~(| InfixOp.add ~(| M.var ~(| "i" |), M.var ~(| "r" |) |), M.var ~(| "n" |) |))] |) ]] in
+    do~ M.substitute_var "i" [[ InfixOp.add ~(| M.var ~(| "i" |), 1 |) ]] in
+    M.pure BlockUnit.Tt
+  ) in
+  M.pure BlockUnit.Tt.