Bump Gnark and gnark-lean-extractor

.gitignore

@@ -1,4 +1,5 @@
 .idea
+*.olean
 out
 gnark-mbu
 gnark-mbu.exe

formal-verification/FormalVerification.lean

@@ -8,6 +8,7 @@ namespace SemaphoreMTB
 def Order : ℕ := 0x30644e72e131a029b85045b68181585d2833e84879b9709143e1f593f0000001
 variable [Fact (Nat.Prime Order)]
 abbrev F := ZMod Order
+abbrev Gates := GatesGnark9 Order
 
 def ReducedModRCheck_32 (Input: Vector F 32) : Prop :=
     True

formal-verification/lake-manifest.json

@@ -1,45 +1,60 @@
-{"version": 4,
+{"version": 6,
  "packagesDir": "lake-packages",
  "packages":
  [{"git":
-   {"url": "https://github.com/EdAyers/ProofWidgets4",
-    "subDir?": null,
-    "rev": "c43db94a8f495dad37829e9d7ad65483d68c86b8",
-    "name": "proofwidgets",
-    "inputRev?": "v0.0.11"}},
-  {"git":
-   {"url": "https://github.com/mhuisi/lean4-cli.git",
+   {"url": "https://github.com/leanprover-community/mathlib4.git",
     "subDir?": null,
-    "rev": "5a858c32963b6b19be0d477a30a1f4b6c120be7e",
-    "name": "Cli",
-    "inputRev?": "nightly"}},
+    "rev": "753159252c585df6b6aa7c48d2b8828d58388b79",
+    "opts": {},
+    "name": "mathlib",
+    "inputRev?": "v4.2.0",
+    "inherited": false}},
   {"git":
    {"url": "https://github.com/reilabs/proven-zk.git",
     "subDir?": null,
-    "rev": "ae9327ec14d84b20f1c17f336ed7698e5b0fbae1",
+    "rev": "659b51e94d4c5160c5d93b92323f0d0dda05c3ad",
+    "opts": {},
     "name": "ProvenZK",
-    "inputRev?": "v1.3.0"}},
+    "inputRev?": "v1.4.0",
+    "inherited": false}},
   {"git":
-   {"url": "https://github.com/leanprover-community/mathlib4.git",
+   {"url": "https://github.com/leanprover-community/quote4",
     "subDir?": null,
-    "rev": "26d0eab43f05db777d1cf31abd31d3a57954b2a9",
-    "name": "mathlib",
-    "inputRev?": "26d0eab43f05db777d1cf31abd31d3a57954b2a9"}},
+    "rev": "a387c0eb611857e2460cf97a8e861c944286e6b2",
+    "opts": {},
+    "name": "Qq",
+    "inputRev?": "master",
+    "inherited": true}},
   {"git":
-   {"url": "https://github.com/gebner/quote4",
+   {"url": "https://github.com/leanprover/lean4-cli",
     "subDir?": null,
-    "rev": "c0d9516f44d07feee01c1103c8f2f7c24a822b55",
-    "name": "Qq",
-    "inputRev?": "master"}},
+    "rev": "39229f3630d734af7d9cfb5937ddc6b41d3aa6aa",
+    "opts": {},
+    "name": "Cli",
+    "inputRev?": "nightly",
+    "inherited": true}},
   {"git":
-   {"url": "https://github.com/JLimperg/aesop",
+   {"url": "https://github.com/leanprover-community/ProofWidgets4",
     "subDir?": null,
-    "rev": "f04538ab6ad07642368cf11d2702acc0a9b4bcee",
-    "name": "aesop",
-    "inputRev?": "master"}},
+    "rev": "f1a5c7808b001305ba07d8626f45ee054282f589",
+    "opts": {},
+    "name": "proofwidgets",
+    "inputRev?": "v0.0.21",
+    "inherited": true}},
   {"git":
    {"url": "https://github.com/leanprover/std4",
     "subDir?": null,
-    "rev": "dff883c55395438ae2a5c65ad5ddba084b600feb",
+    "rev": "6747f41f28627bed83e6d5891683538211caa2c1",
+    "opts": {},
     "name": "std",
-    "inputRev?": "main"}}]}
+    "inputRev?": "main",
+    "inherited": true}},
+  {"git":
+   {"url": "https://github.com/leanprover-community/aesop",
+    "subDir?": null,
+    "rev": "6749fa4e776919514dae85bfc0ad62a511bc42a7",
+    "opts": {},
+    "name": "aesop",
+    "inputRev?": "master",
+    "inherited": true}}],
+ "name": "«formal-verification»"}

formal-verification/lakefile.lean

@@ -6,10 +6,10 @@ package «formal-verification» {
 }
 
 require mathlib from git
-  "https://github.com/leanprover-community/mathlib4.git"@"26d0eab43f05db777d1cf31abd31d3a57954b2a9"
+  "https://github.com/leanprover-community/mathlib4.git"@"v4.2.0"
 
 require ProvenZK from git
-  "https://github.com/reilabs/proven-zk.git"@"v1.3.0"
+  "https://github.com/reilabs/proven-zk.git"@"v1.4.0"
 
 lean_lib FormalVerification {
   moreLeanArgs := #["--tstack=65520", "-DmaxRecDepth=10000", "-DmaxHeartbeats=200000000"]

formal-verification/lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:nightly-2023-07-12
+leanprover/lean4:v4.2.0

go.mod

@@ -3,47 +3,50 @@ module worldcoin/gnark-mbu
 go 1.20
 
 require (
-	github.com/consensys/gnark v0.8.0
+	github.com/consensys/gnark v0.9.2-0.20240322153533-3abde1199375
 	github.com/iden3/go-iden3-crypto v0.0.13
 	github.com/prometheus/client_golang v1.14.0
-	github.com/reilabs/gnark-lean-extractor/v2 v2.1.0
+	github.com/reilabs/gnark-lean-extractor/v3 v3.0.0-20240328211639-501e57e18613
 	github.com/urfave/cli/v2 v2.10.2
 )
 
 require (
 	github.com/beorn7/perks v1.0.1 // indirect
+	github.com/bits-and-blooms/bitset v1.8.0 // indirect
 	github.com/blang/semver/v4 v4.0.0 // indirect
 	github.com/cespare/xxhash/v2 v2.1.2 // indirect
 	github.com/consensys/bavard v0.1.13 // indirect
 	github.com/cpuguy83/go-md2man/v2 v2.0.2 // indirect
 	github.com/golang/protobuf v1.5.2 // indirect
-	github.com/google/pprof v0.0.0-20230309165930-d61513b1440d // indirect
+	github.com/google/pprof v0.0.0-20230817174616-7a8ec2ada47b // indirect
+	github.com/ingonyama-zk/icicle v0.0.0-20230928131117-97f0079e5c71 // indirect
+	github.com/ingonyama-zk/iciclegnark v0.1.0 // indirect
 	github.com/mattn/go-colorable v0.1.13 // indirect
-	github.com/mattn/go-isatty v0.0.16 // indirect
+	github.com/mattn/go-isatty v0.0.19 // indirect
 	github.com/matttproud/golang_protobuf_extensions v1.0.1 // indirect
 	github.com/mitchellh/copystructure v1.2.0 // indirect
 	github.com/mitchellh/reflectwalk v1.0.2 // indirect
 	github.com/prometheus/client_model v0.3.0 // indirect
 	github.com/prometheus/common v0.37.0 // indirect
 	github.com/prometheus/procfs v0.8.0 // indirect
-	github.com/rogpeppe/go-internal v1.11.0 // indirect
 	github.com/russross/blackfriday/v2 v2.1.0 // indirect
 	github.com/xrash/smetrics v0.0.0-20201216005158-039620a65673 // indirect
 	golang.org/x/exp v0.0.0-20230905200255-921286631fa9 // indirect
+	golang.org/x/sync v0.3.0 // indirect
 	google.golang.org/protobuf v1.28.1 // indirect
 	rsc.io/tmplfunc v0.0.3 // indirect
 )
 
 require (
-	github.com/consensys/gnark-crypto v0.9.1
+	github.com/consensys/gnark-crypto v0.12.2-0.20240215234832-d72fcb379d3e
 	github.com/davecgh/go-spew v1.1.1 // indirect
-	github.com/fxamacker/cbor/v2 v2.4.0 // indirect
+	github.com/fxamacker/cbor/v2 v2.5.0 // indirect
 	github.com/mmcloughlin/addchain v0.4.0 // indirect
 	github.com/pmezard/go-difflib v1.0.0 // indirect
-	github.com/rs/zerolog v1.29.0
-	github.com/stretchr/testify v1.8.2 // indirect
+	github.com/rs/zerolog v1.30.0
+	github.com/stretchr/testify v1.8.4 // indirect
 	github.com/x448/float16 v0.8.4 // indirect
-	golang.org/x/crypto v0.10.0 // indirect
-	golang.org/x/sys v0.12.0 // indirect
+	golang.org/x/crypto v0.17.0 // indirect
+	golang.org/x/sys v0.15.0 // indirect
 	gopkg.in/yaml.v3 v3.0.1 // indirect
 )