From 4b0ae1c8fab0d625bcd4395d68689771cf3a4208 Mon Sep 17 00:00:00 2001 From: Wojciech Zmuda Date: Mon, 25 Mar 2024 22:13:01 +0100 Subject: [PATCH 1/2] Bump Gnark to v0.9.2-0.20240322153533-3abde1199375 Due to backend/hint being moved, update extractor to use the new API. Add stub methods to satisfy the interface. Signed-off-by: Wojciech Zmuda --- extractor/extractor.go | 50 ++++++++++++++++++++++++++++++++++++-- go.mod | 17 ++++++------- go.sum | 54 +++++++++++++++++++++++------------------- 3 files changed, 86 insertions(+), 35 deletions(-) diff --git a/extractor/extractor.go b/extractor/extractor.go index c428219..5c9a0b9 100644 --- a/extractor/extractor.go +++ b/extractor/extractor.go @@ -6,9 +6,11 @@ import ( "reflect" "github.com/consensys/gnark-crypto/ecc" - "github.com/consensys/gnark/backend/hint" + "github.com/consensys/gnark/constraint" + "github.com/consensys/gnark/constraint/solver" "github.com/consensys/gnark/frontend" "github.com/consensys/gnark/frontend/schema" + "github.com/reilabs/gnark-lean-extractor/v2/abstractor" ) @@ -188,6 +190,48 @@ type CodeExtractor struct { FieldID ecc.ID } +func (ce *CodeExtractor) AssertIsCrumb(i1 frontend.Variable) { + // TODO implement me + panic("implement me") +} + +func (ce *CodeExtractor) AddBlueprint(b constraint.Blueprint) constraint.BlueprintID { + // TODO implement me + panic("implement me") +} + +func (ce *CodeExtractor) AddInstruction(bID constraint.BlueprintID, calldata []uint32) []uint32 { + // TODO implement me + panic("implement me") +} + +func (ce *CodeExtractor) NewHintForId( + id solver.HintID, nbOutputs int, inputs ...frontend.Variable, +) ([]frontend.Variable, error) { + // TODO implement me + panic("implement me") +} + +func (ce *CodeExtractor) Defer(cb func(api frontend.API) error) { + // TODO implement me + panic("implement me") +} + +func (ce *CodeExtractor) InternalVariable(wireID uint32) frontend.Variable { + // TODO implement me + panic("implement me") +} + +func (ce *CodeExtractor) ToCanonicalVariable(variable frontend.Variable) frontend.CanonicalVariable { + // TODO implement me + panic("implement me") +} + +func (ce *CodeExtractor) SetGkrInfo(info constraint.GkrInfo) error { + // TODO implement me + panic("implement me") +} + func sanitizeVars(args ...frontend.Variable) []Operand { ops := []Operand{} for _, arg := range args { @@ -373,7 +417,9 @@ func (ce *CodeExtractor) Commit(...frontend.Variable) (frontend.Variable, error) panic("implement me") } -func (ce *CodeExtractor) NewHint(f hint.Function, nbOutputs int, inputs ...frontend.Variable) ([]frontend.Variable, error) { +func (ce *CodeExtractor) NewHint(f solver.Hint, nbOutputs int, inputs ...frontend.Variable) ( + []frontend.Variable, error, +) { panic("implement me") } diff --git a/go.mod b/go.mod index b314b5f..4a358da 100644 --- a/go.mod +++ b/go.mod @@ -3,26 +3,27 @@ module github.com/reilabs/gnark-lean-extractor/v2 go 1.20 require ( - github.com/consensys/gnark v0.8.0 - github.com/consensys/gnark-crypto v0.9.1 + github.com/consensys/gnark v0.9.2-0.20240322153533-3abde1199375 + github.com/consensys/gnark-crypto v0.12.2-0.20240215234832-d72fcb379d3e github.com/mitchellh/copystructure v1.2.0 - github.com/stretchr/testify v1.8.1 + github.com/stretchr/testify v1.8.4 golang.org/x/exp v0.0.0-20230905200255-921286631fa9 ) require ( + github.com/bits-and-blooms/bitset v1.8.0 // indirect github.com/blang/semver/v4 v4.0.0 // indirect github.com/consensys/bavard v0.1.13 // indirect github.com/davecgh/go-spew v1.1.1 // indirect + github.com/google/pprof v0.0.0-20230817174616-7a8ec2ada47b // indirect github.com/kr/text v0.2.0 // indirect - github.com/mattn/go-colorable v0.1.12 // indirect - github.com/mattn/go-isatty v0.0.14 // indirect + github.com/mattn/go-colorable v0.1.13 // indirect + github.com/mattn/go-isatty v0.0.19 // indirect github.com/mitchellh/reflectwalk v1.0.2 // indirect github.com/mmcloughlin/addchain v0.4.0 // indirect github.com/pmezard/go-difflib v1.0.0 // indirect - github.com/rogpeppe/go-internal v1.10.0 // indirect - github.com/rs/zerolog v1.29.0 // indirect - golang.org/x/sys v0.12.0 // indirect + github.com/rs/zerolog v1.30.0 // indirect + golang.org/x/sys v0.15.0 // indirect gopkg.in/yaml.v3 v3.0.1 // indirect rsc.io/tmplfunc v0.0.3 // indirect ) diff --git a/go.sum b/go.sum index 3b95434..797c550 100644 --- a/go.sum +++ b/go.sum @@ -1,28 +1,35 @@ +github.com/bits-and-blooms/bitset v1.8.0 h1:FD+XqgOZDUxxZ8hzoBFuV9+cGWY9CslN6d5MS5JVb4c= +github.com/bits-and-blooms/bitset v1.8.0/go.mod h1:7hO7Gc7Pp1vODcmWvKMRA9BNmbv6a/7QIWpPxHddWR8= github.com/blang/semver/v4 v4.0.0 h1:1PFHFE6yCCTv8C1TeyNNarDzntLi7wMI5i/pzqYIsAM= github.com/blang/semver/v4 v4.0.0/go.mod h1:IbckMUScFkM3pff0VJDNKRiT6TG/YpiHIM2yvyW5YoQ= github.com/consensys/bavard v0.1.13 h1:oLhMLOFGTLdlda/kma4VOJazblc7IM5y5QPd2A/YjhQ= github.com/consensys/bavard v0.1.13/go.mod h1:9ItSMtA/dXMAiL7BG6bqW2m3NdSEObYWoH223nGHukI= -github.com/consensys/gnark v0.8.0 h1:0bQ2MyDG4oNjMQpNyL8HjrrUSSL3yYJg0Elzo6LzmcU= -github.com/consensys/gnark v0.8.0/go.mod h1:aKmA7dIiLbTm0OV37xTq0z+Bpe4xER8EhRLi6necrm8= -github.com/consensys/gnark-crypto v0.9.1 h1:mru55qKdWl3E035hAoh1jj9d7hVnYY5pfb6tmovSmII= -github.com/consensys/gnark-crypto v0.9.1/go.mod h1:a2DQL4+5ywF6safEeZFEPGRiiGbjzGFRUN2sg06VuU4= -github.com/coreos/go-systemd/v22 v22.3.3-0.20220203105225-a9a7ef127534/go.mod h1:Y58oyj3AT4RCenI/lSvhwexgC+NSVTIJ3seZv2GcEnc= +github.com/consensys/gnark v0.9.2-0.20240322153533-3abde1199375 h1:yp/JtBdxrG2vjbe6vntaP11m6uROj/QmI86jxW7Ih6k= +github.com/consensys/gnark v0.9.2-0.20240322153533-3abde1199375/go.mod h1:0dnRvl8EDbPsSZsIg8xOP1Au8cf43xOlT7/BhwMV98g= +github.com/consensys/gnark-crypto v0.12.2-0.20240215234832-d72fcb379d3e h1:MKdOuCiy2DAX1tMp2YsmtNDaqdigpY6B5cZQDJ9BvEo= +github.com/consensys/gnark-crypto v0.12.2-0.20240215234832-d72fcb379d3e/go.mod h1:wKqwsieaKPThcFkHe0d0zMsbHEUWFmZcG7KBCse210o= +github.com/coreos/go-systemd/v22 v22.5.0/go.mod h1:Y58oyj3AT4RCenI/lSvhwexgC+NSVTIJ3seZv2GcEnc= github.com/creack/pty v1.1.9/go.mod h1:oKZEueFk5CKHvIhNR5MUki03XCEU+Q6VDXinZuGJ33E= -github.com/davecgh/go-spew v1.1.0/go.mod h1:J7Y8YcW2NihsgmVo/mv3lAwl/skON4iLHjSsI+c5H38= github.com/davecgh/go-spew v1.1.1 h1:vj9j/u1bqnvCEfJOwUhtlOARqs3+rkHYY13jYWTU97c= github.com/davecgh/go-spew v1.1.1/go.mod h1:J7Y8YcW2NihsgmVo/mv3lAwl/skON4iLHjSsI+c5H38= -github.com/fxamacker/cbor/v2 v2.4.0 h1:ri0ArlOR+5XunOP8CRUowT0pSJOwhW098ZCUyskZD88= +github.com/fxamacker/cbor/v2 v2.5.0 h1:oHsG0V/Q6E/wqTS2O1Cozzsy69nqCiguo5Q1a1ADivE= github.com/godbus/dbus/v5 v5.0.4/go.mod h1:xhWf0FNVPg57R7Z0UbKHbJfkEywrmjJnf7w5xrFpKfA= -github.com/google/pprof v0.0.0-20230207041349-798e818bf904 h1:4/hN5RUoecvl+RmJRE2YxKWtnnQls6rQjjW5oV7qg2U= +github.com/google/pprof v0.0.0-20230817174616-7a8ec2ada47b h1:h9U78+dx9a4BKdQkBBos92HalKpaGKHrp+3Uo6yTodo= +github.com/google/pprof v0.0.0-20230817174616-7a8ec2ada47b/go.mod h1:czg5+yv1E0ZGTi6S6vVK1mke0fV+FaUhNGcd6VRS9Ik= github.com/google/subcommands v1.2.0/go.mod h1:ZjhPrFU+Olkh9WazFPsl27BQ4UPiG37m3yTrtFlrHVk= +github.com/ingonyama-zk/icicle v0.0.0-20230928131117-97f0079e5c71 h1:YxI1RTPzpFJ3MBmxPl3Bo0F7ume7CmQEC1M9jL6CT94= +github.com/ingonyama-zk/iciclegnark v0.1.0 h1:88MkEghzjQBMjrYRJFxZ9oR9CTIpB8NG2zLeCJSvXKQ= github.com/kr/pretty v0.3.1 h1:flRD4NNwYAUpkphVc1HcthR4KEIFJ65n8Mw5qdRn3LE= github.com/kr/text v0.2.0 h1:5Nx0Ya0ZqY2ygV366QzturHI13Jq95ApcVaJBhpS+AY= github.com/kr/text v0.2.0/go.mod h1:eLer722TekiGuMkidMxC/pM04lWEeraHUUmBw8l2grE= github.com/leanovate/gopter v0.2.9 h1:fQjYxZaynp97ozCzfOyOuAGOU4aU/z37zf/tOujFk7c= -github.com/mattn/go-colorable v0.1.12 h1:jF+Du6AlPIjs2BiUiQlKOX0rt3SujHxPnksPKZbaA40= github.com/mattn/go-colorable v0.1.12/go.mod h1:u5H1YNBxpqRaxsYJYSkiCWKzEfiAb1Gb520KVy5xxl4= -github.com/mattn/go-isatty v0.0.14 h1:yVuAays6BHfxijgZPzw+3Zlu5yQgKGP2/hcQbHb7S9Y= +github.com/mattn/go-colorable v0.1.13 h1:fFA4WZxdEF4tXPZVKMLwD8oUnCTTo08duU7wxecdEvA= +github.com/mattn/go-colorable v0.1.13/go.mod h1:7S9/ev0klgBDR4GtXTXX8a3vIGJpMovkB8vQcUbaXHg= github.com/mattn/go-isatty v0.0.14/go.mod h1:7GGIvUiUoEMVVmxf/4nioHXj79iQHKdU27kJ6hsGG94= +github.com/mattn/go-isatty v0.0.16/go.mod h1:kYGgaQfpe5nmfYZH+SKPsOc2e4SrIfOl2e/yFXSvRLM= +github.com/mattn/go-isatty v0.0.19 h1:JITubQf0MOLdlGRuRq+jtsDlekdYPia9ZFsB8h/APPA= +github.com/mattn/go-isatty v0.0.19/go.mod h1:W+V8PltTTMOvKvAeJH7IuucS94S2C6jfK/D7dTCTo3Y= github.com/mitchellh/copystructure v1.2.0 h1:vpKXTN4ewci03Vljg/q9QvCGUDttBOGBIa15WveJJGw= github.com/mitchellh/copystructure v1.2.0/go.mod h1:qLl+cE2AmVv+CoeAwDPye/v+N2HKCj9FbZEVFJRxO9s= github.com/mitchellh/reflectwalk v1.0.2 h1:G2LzWKi524PWgd3mLHV8Y5k7s6XUvT0Gef6zxSIeXaQ= @@ -33,28 +40,25 @@ github.com/mmcloughlin/profile v0.1.1/go.mod h1:IhHD7q1ooxgwTgjxQYkACGA77oFTDdFV github.com/pkg/errors v0.9.1/go.mod h1:bwawxfHBFNV+L2hUp1rHADufV3IMtnDRdf1r5NINEl0= github.com/pmezard/go-difflib v1.0.0 h1:4DBwDE0NGyQoBHbLQYPwSUPoCMWR5BEzIk/f1lZbAQM= github.com/pmezard/go-difflib v1.0.0/go.mod h1:iKH77koFhYxTK1pcRnkKkqfTogsbg7gZNVY4sRDYZ/4= -github.com/rogpeppe/go-internal v1.10.0 h1:TMyTOH3F/DB16zRVcYyreMH6GnZZrwQVAoYjRBZyWFQ= -github.com/rogpeppe/go-internal v1.10.0/go.mod h1:UQnix2H7Ngw/k4C5ijL5+65zddjncjaFoBhdsK/akog= -github.com/rs/xid v1.4.0/go.mod h1:trrq9SKmegXys3aeAKXMUTdJsYXVwGY3RLcfgqegfbg= -github.com/rs/zerolog v1.29.0 h1:Zes4hju04hjbvkVkOhdl2HpZa+0PmVwigmo8XoORE5w= -github.com/rs/zerolog v1.29.0/go.mod h1:NILgTygv/Uej1ra5XxGf82ZFSLk58MFGAUS2o6usyD0= -github.com/stretchr/objx v0.1.0/go.mod h1:HFkY916IF+rwdDfMAkV7OtwuqBVzrE8GR6GFx+wExME= -github.com/stretchr/objx v0.4.0/go.mod h1:YvHI0jy2hoMjB+UWwv71VJQ9isScKT/TqJzVSSt89Yw= -github.com/stretchr/objx v0.5.0/go.mod h1:Yh+to48EsGEfYuaHDzXPcE3xhTkx73EhmCGUpEOglKo= -github.com/stretchr/testify v1.7.1/go.mod h1:6Fq8oRcR53rry900zMqJjRRixrwX3KX962/h/Wwjteg= -github.com/stretchr/testify v1.8.0/go.mod h1:yNjHg4UonilssWZ8iaSj1OCr/vHnekPRkoO+kdMU+MU= -github.com/stretchr/testify v1.8.1 h1:w7B6lhMri9wdJUVmEZPGGhZzrYTPvgJArz7wNPgYKsk= -github.com/stretchr/testify v1.8.1/go.mod h1:w2LPCIKwWwSfY2zedu0+kehJoqGctiVI29o6fzry7u4= +github.com/rogpeppe/go-internal v1.11.0 h1:cWPaGQEPrBb5/AsnsZesgZZ9yb1OQ+GOISoDNXVBh4M= +github.com/rs/xid v1.5.0/go.mod h1:trrq9SKmegXys3aeAKXMUTdJsYXVwGY3RLcfgqegfbg= +github.com/rs/zerolog v1.30.0 h1:SymVODrcRsaRaSInD9yQtKbtWqwsfoPcRff/oRXLj4c= +github.com/rs/zerolog v1.30.0/go.mod h1:/tk+P47gFdPXq4QYjvCmT5/Gsug2nagsFWBWhAiSi1w= +github.com/stretchr/testify v1.8.4 h1:CcVxjf3Q8PM0mHUKJCdn+eZZtm5yQwehR5yeSVQQcUk= +github.com/stretchr/testify v1.8.4/go.mod h1:sz/lmYIOXD/1dqDmKjjqLyZ2RngseejIcXlSw2iwfAo= github.com/x448/float16 v0.8.4 h1:qLwI1I70+NjRFUR3zs1JPUCgaCXSh3SW62uAKT1mSBM= +golang.org/x/crypto v0.17.0 h1:r8bRNjWL3GshPW3gkd+RpvzWrZAwPS49OmTGZ/uhM4k= golang.org/x/exp v0.0.0-20230905200255-921286631fa9 h1:GoHiUyI/Tp2nVkLI2mCxVkOjsbSXD66ic0XW0js0R9g= golang.org/x/exp v0.0.0-20230905200255-921286631fa9/go.mod h1:S2oDrQGGwySpoQPVqRShND87VCbxmc6bL1Yd2oYrm6k= +golang.org/x/sync v0.3.0 h1:ftCYgMx6zT/asHUrPw8BLLscYtGznsLAnjq5RH9P66E= golang.org/x/sys v0.0.0-20210630005230-0f9fa26af87c/go.mod h1:oPkhp1MJrh7nUepCBck5+mAzfO9JrbApNNgaTdGDITg= golang.org/x/sys v0.0.0-20210927094055-39ccf1dd6fa6/go.mod h1:oPkhp1MJrh7nUepCBck5+mAzfO9JrbApNNgaTdGDITg= -golang.org/x/sys v0.12.0 h1:CM0HF96J0hcLAwsHPJZjfdNzs0gftsLfgKt57wWHJ0o= -golang.org/x/sys v0.12.0/go.mod h1:oPkhp1MJrh7nUepCBck5+mAzfO9JrbApNNgaTdGDITg= +golang.org/x/sys v0.0.0-20220811171246-fbc7d0a398ab/go.mod h1:oPkhp1MJrh7nUepCBck5+mAzfO9JrbApNNgaTdGDITg= +golang.org/x/sys v0.6.0/go.mod h1:oPkhp1MJrh7nUepCBck5+mAzfO9JrbApNNgaTdGDITg= +golang.org/x/sys v0.15.0 h1:h48lPFYpsTvQJZF4EKyI4aLHaev3CxivZmv7yZig9pc= +golang.org/x/sys v0.15.0/go.mod h1:/VUhepiaJMQUp4+oa/7Zr1D23ma6VTLIYjOOTFZPUcA= gopkg.in/check.v1 v0.0.0-20161208181325-20d25e280405/go.mod h1:Co6ibVJAznAaIkqp8huTwlJQCZ016jof/cbN4VW5Yz0= gopkg.in/check.v1 v1.0.0-20201130134442-10cb98267c6c h1:Hei/4ADfdWqJk1ZMxUNpqntNwaWcugrBjAiHlqqRiVk= -gopkg.in/yaml.v3 v3.0.0-20200313102051-9f266ea9e77c/go.mod h1:K4uyk7z7BCEPqu6E+C64Yfv1cQ7kz7rIZviUmN+EgEM= gopkg.in/yaml.v3 v3.0.1 h1:fxVm/GzAzEWqLHuvctI91KS9hhNmmWOoWu0XTYJS7CA= gopkg.in/yaml.v3 v3.0.1/go.mod h1:K4uyk7z7BCEPqu6E+C64Yfv1cQ7kz7rIZviUmN+EgEM= rsc.io/tmplfunc v0.0.3 h1:53XFQh69AfOa8Tw0Jm7t+GV7KZhOi6jzsCzTtKbMvzU= From 501e57e186131ab39d3ff2275344edacde2a568b Mon Sep 17 00:00:00 2001 From: Giuseppe <8973725+Eagle941@users.noreply.github.com> Date: Thu, 28 Mar 2024 21:16:39 +0000 Subject: [PATCH 2/2] Added GatesGnark9 header and updated to v3 --- README.md | 6 ++++-- extractor/extractor.go | 2 +- extractor/interface.go | 2 +- extractor/lean_export.go | 2 +- extractor/misc.go | 2 +- extractor/test/another_circuit_test.go | 4 ++-- extractor/test/circuit_with_parameter_test.go | 4 ++-- extractor/test/deletion_mbu_circuit_test.go | 4 ++-- extractor/test/merkle_recover_test.go | 4 ++-- extractor/test/my_circuit_test.go | 2 +- extractor/test/slices_optimisation_test.go | 4 ++-- extractor/test/to_binary_circuit_test.go | 4 ++-- extractor/test/two_gadgets_test.go | 4 ++-- go.mod | 2 +- test/TestAnotherCircuit.lean | 2 +- test/TestCircuitWithParameter.lean | 2 +- test/TestDeletionMbuCircuit.lean | 2 +- test/TestExtractCircuits.lean | 2 +- test/TestExtractGadgets.lean | 2 +- test/TestExtractGadgetsVectors.lean | 2 +- test/TestGadgetExtraction.lean | 2 +- test/TestMerkleRecover.lean | 2 +- test/TestMyCircuit.lean | 2 +- test/TestSlicesOptimisation.lean | 2 +- test/TestToBinaryCircuit.lean | 2 +- test/TestTwoGadgets.lean | 2 +- 26 files changed, 36 insertions(+), 34 deletions(-) diff --git a/README.md b/README.md index 4577e6e..bf1150b 100644 --- a/README.md +++ b/README.md @@ -23,9 +23,11 @@ contributing, or are new to Go, please see our [contributing guidelines](./CONTRIBUTING.md) for more information. ## Compatibility -This version of `gnark-lean-extractor` is compatible with `gnark v0.8.x`. +This version of `gnark-lean-extractor` is compatible with `gnark v0.9.x`. It is recommended to import [`ProvenZK-v1.4.0`](https://github.com/reilabs/proven-zk/tree/v1.4.0) in Lean4 to process the circuits extracted with this version of `gnark-lean-extractor`. +For compatibility with `gnark v0.8.x`, use `gnark-lean-extractor-v2.2.0`. + ## Example The following is a brief example of how to design a simple gnark circuit in @@ -62,7 +64,7 @@ namespace MyCircuit def Order : ℕ := 0x30644e72e131a029b85045b68181585d2833e84879b9709143e1f593f0000001 variable [Fact (Nat.Prime Order)] abbrev F := ZMod Order -abbrev Gates := GatesGnark8 Order +abbrev Gates := GatesGnark9 Order def circuit (In_1: F) (In_2: F) (Out: F): Prop := ∃gate_0, gate_0 = Gates.add In_1 In_2 ∧ diff --git a/extractor/extractor.go b/extractor/extractor.go index 5c9a0b9..0678727 100644 --- a/extractor/extractor.go +++ b/extractor/extractor.go @@ -11,7 +11,7 @@ import ( "github.com/consensys/gnark/frontend" "github.com/consensys/gnark/frontend/schema" - "github.com/reilabs/gnark-lean-extractor/v2/abstractor" + "github.com/reilabs/gnark-lean-extractor/v3/abstractor" ) type Operand interface { diff --git a/extractor/interface.go b/extractor/interface.go index b12333a..22e1b28 100644 --- a/extractor/interface.go +++ b/extractor/interface.go @@ -7,7 +7,7 @@ import ( "github.com/consensys/gnark-crypto/ecc" "github.com/consensys/gnark/frontend" - "github.com/reilabs/gnark-lean-extractor/v2/abstractor" + "github.com/reilabs/gnark-lean-extractor/v3/abstractor" "golang.org/x/exp/slices" ) diff --git a/extractor/lean_export.go b/extractor/lean_export.go index 819c3bb..f51c057 100644 --- a/extractor/lean_export.go +++ b/extractor/lean_export.go @@ -36,7 +36,7 @@ namespace %s def Order : ℕ := 0x%s variable [Fact (Nat.Prime Order)] abbrev F := ZMod Order -abbrev Gates := %s Order`, trimmedName, order.Text(16), "GatesGnark8") +abbrev Gates := %s Order`, trimmedName, order.Text(16), "GatesGnark9") return s } diff --git a/extractor/misc.go b/extractor/misc.go index 9d100e7..b8bd47e 100644 --- a/extractor/misc.go +++ b/extractor/misc.go @@ -11,7 +11,7 @@ import ( "github.com/consensys/gnark/frontend" "github.com/consensys/gnark/frontend/schema" "github.com/mitchellh/copystructure" - "github.com/reilabs/gnark-lean-extractor/v2/abstractor" + "github.com/reilabs/gnark-lean-extractor/v3/abstractor" ) // recoverError is used in the top level interface to prevent panic diff --git a/extractor/test/another_circuit_test.go b/extractor/test/another_circuit_test.go index c825af4..b2314fc 100644 --- a/extractor/test/another_circuit_test.go +++ b/extractor/test/another_circuit_test.go @@ -6,8 +6,8 @@ import ( "github.com/consensys/gnark-crypto/ecc" "github.com/consensys/gnark/frontend" - "github.com/reilabs/gnark-lean-extractor/v2/abstractor" - "github.com/reilabs/gnark-lean-extractor/v2/extractor" + "github.com/reilabs/gnark-lean-extractor/v3/abstractor" + "github.com/reilabs/gnark-lean-extractor/v3/extractor" ) // Example: Gadget with nested array of int diff --git a/extractor/test/circuit_with_parameter_test.go b/extractor/test/circuit_with_parameter_test.go index 2c70f8c..0b70084 100644 --- a/extractor/test/circuit_with_parameter_test.go +++ b/extractor/test/circuit_with_parameter_test.go @@ -6,8 +6,8 @@ import ( "github.com/consensys/gnark-crypto/ecc" "github.com/consensys/gnark/frontend" - "github.com/reilabs/gnark-lean-extractor/v2/abstractor" - "github.com/reilabs/gnark-lean-extractor/v2/extractor" + "github.com/reilabs/gnark-lean-extractor/v3/abstractor" + "github.com/reilabs/gnark-lean-extractor/v3/extractor" "github.com/stretchr/testify/assert" ) diff --git a/extractor/test/deletion_mbu_circuit_test.go b/extractor/test/deletion_mbu_circuit_test.go index 8d261cb..26d22c7 100644 --- a/extractor/test/deletion_mbu_circuit_test.go +++ b/extractor/test/deletion_mbu_circuit_test.go @@ -6,8 +6,8 @@ import ( "github.com/consensys/gnark-crypto/ecc" "github.com/consensys/gnark/frontend" - "github.com/reilabs/gnark-lean-extractor/v2/abstractor" - "github.com/reilabs/gnark-lean-extractor/v2/extractor" + "github.com/reilabs/gnark-lean-extractor/v3/abstractor" + "github.com/reilabs/gnark-lean-extractor/v3/extractor" ) // Example: Mismatched arguments error diff --git a/extractor/test/merkle_recover_test.go b/extractor/test/merkle_recover_test.go index b2850bf..86695eb 100644 --- a/extractor/test/merkle_recover_test.go +++ b/extractor/test/merkle_recover_test.go @@ -6,8 +6,8 @@ import ( "github.com/consensys/gnark-crypto/ecc" "github.com/consensys/gnark/frontend" - "github.com/reilabs/gnark-lean-extractor/v2/abstractor" - "github.com/reilabs/gnark-lean-extractor/v2/extractor" + "github.com/reilabs/gnark-lean-extractor/v3/abstractor" + "github.com/reilabs/gnark-lean-extractor/v3/extractor" ) // Example: circuit with arrays and gadget diff --git a/extractor/test/my_circuit_test.go b/extractor/test/my_circuit_test.go index 5dbc41f..80c0f5a 100644 --- a/extractor/test/my_circuit_test.go +++ b/extractor/test/my_circuit_test.go @@ -6,7 +6,7 @@ import ( "github.com/consensys/gnark-crypto/ecc" "github.com/consensys/gnark/frontend" - "github.com/reilabs/gnark-lean-extractor/v2/extractor" + "github.com/reilabs/gnark-lean-extractor/v3/extractor" ) // Example: readme circuit diff --git a/extractor/test/slices_optimisation_test.go b/extractor/test/slices_optimisation_test.go index d365ffb..d147c1e 100644 --- a/extractor/test/slices_optimisation_test.go +++ b/extractor/test/slices_optimisation_test.go @@ -6,8 +6,8 @@ import ( "github.com/consensys/gnark-crypto/ecc" "github.com/consensys/gnark/frontend" - "github.com/reilabs/gnark-lean-extractor/v2/abstractor" - "github.com/reilabs/gnark-lean-extractor/v2/extractor" + "github.com/reilabs/gnark-lean-extractor/v3/abstractor" + "github.com/reilabs/gnark-lean-extractor/v3/extractor" ) // Example: checking slices optimisation diff --git a/extractor/test/to_binary_circuit_test.go b/extractor/test/to_binary_circuit_test.go index 9a34f65..6af3058 100644 --- a/extractor/test/to_binary_circuit_test.go +++ b/extractor/test/to_binary_circuit_test.go @@ -6,8 +6,8 @@ import ( "github.com/consensys/gnark-crypto/ecc" "github.com/consensys/gnark/frontend" - "github.com/reilabs/gnark-lean-extractor/v2/abstractor" - "github.com/reilabs/gnark-lean-extractor/v2/extractor" + "github.com/reilabs/gnark-lean-extractor/v3/abstractor" + "github.com/reilabs/gnark-lean-extractor/v3/extractor" ) // Example: Gadget that returns a vector diff --git a/extractor/test/two_gadgets_test.go b/extractor/test/two_gadgets_test.go index a996cc8..4ed3c06 100644 --- a/extractor/test/two_gadgets_test.go +++ b/extractor/test/two_gadgets_test.go @@ -6,8 +6,8 @@ import ( "github.com/consensys/gnark-crypto/ecc" "github.com/consensys/gnark/frontend" - "github.com/reilabs/gnark-lean-extractor/v2/abstractor" - "github.com/reilabs/gnark-lean-extractor/v2/extractor" + "github.com/reilabs/gnark-lean-extractor/v3/abstractor" + "github.com/reilabs/gnark-lean-extractor/v3/extractor" ) // Example: circuit with multiple gadgets diff --git a/go.mod b/go.mod index 4a358da..e8994b8 100644 --- a/go.mod +++ b/go.mod @@ -1,4 +1,4 @@ -module github.com/reilabs/gnark-lean-extractor/v2 +module github.com/reilabs/gnark-lean-extractor/v3 go 1.20 diff --git a/test/TestAnotherCircuit.lean b/test/TestAnotherCircuit.lean index d94896d..a8da4f3 100644 --- a/test/TestAnotherCircuit.lean +++ b/test/TestAnotherCircuit.lean @@ -8,7 +8,7 @@ namespace AnotherCircuit def Order : ℕ := 0x30644e72e131a029b85045b68181585d2833e84879b9709143e1f593f0000001 variable [Fact (Nat.Prime Order)] abbrev F := ZMod Order -abbrev Gates := GatesGnark8 Order +abbrev Gates := GatesGnark9 Order def IntArrayGadget_4 (In: Vector F 4) (k: Vector F 3 -> Prop): Prop := ∃gate_0, Gates.from_binary In gate_0 ∧ diff --git a/test/TestCircuitWithParameter.lean b/test/TestCircuitWithParameter.lean index 8f25822..7f54406 100644 --- a/test/TestCircuitWithParameter.lean +++ b/test/TestCircuitWithParameter.lean @@ -8,7 +8,7 @@ namespace CircuitWithParameter def Order : ℕ := 0x30644e72e131a029b85045b68181585d2833e84879b9709143e1f593f0000001 variable [Fact (Nat.Prime Order)] abbrev F := ZMod Order -abbrev Gates := GatesGnark8 Order +abbrev Gates := GatesGnark9 Order def ReturnItself_3_3 (In_1: Vector F 3) (Out: Vector F 3) (k: Vector F 3 -> Prop): Prop := ∃gate_0, gate_0 = Gates.mul In_1[0] In_1[0] ∧ diff --git a/test/TestDeletionMbuCircuit.lean b/test/TestDeletionMbuCircuit.lean index c477707..bac7c09 100644 --- a/test/TestDeletionMbuCircuit.lean +++ b/test/TestDeletionMbuCircuit.lean @@ -8,7 +8,7 @@ namespace DeletionMbuCircuit def Order : ℕ := 0x30644e72e131a029b85045b68181585d2833e84879b9709143e1f593f0000001 variable [Fact (Nat.Prime Order)] abbrev F := ZMod Order -abbrev Gates := GatesGnark8 Order +abbrev Gates := GatesGnark9 Order def DeletionProof_2_2_3_2_2_3 (DeletionIndices: Vector F 2) (PreRoot: F) (IdComms: Vector F 2) (MerkleProofs: Vector (Vector F 3) 2) (k: F -> Prop): Prop := k PreRoot diff --git a/test/TestExtractCircuits.lean b/test/TestExtractCircuits.lean index d99bdc7..070036b 100644 --- a/test/TestExtractCircuits.lean +++ b/test/TestExtractCircuits.lean @@ -8,7 +8,7 @@ namespace MultipleCircuits def Order : ℕ := 0x30644e72e131a029b85045b68181585d2833e84879b9709143e1f593f0000001 variable [Fact (Nat.Prime Order)] abbrev F := ZMod Order -abbrev Gates := GatesGnark8 Order +abbrev Gates := GatesGnark9 Order def VectorGadget_3_3_3_3 (In_1: Vector F 3) (In_2: Vector F 3) (Nested: Vector (Vector F 3) 3) (k: Vector F 3 -> Prop): Prop := ∃_ignored_, _ignored_ = Gates.mul In_1[0] In_2[0] ∧ diff --git a/test/TestExtractGadgets.lean b/test/TestExtractGadgets.lean index 89e19b9..2245597 100644 --- a/test/TestExtractGadgets.lean +++ b/test/TestExtractGadgets.lean @@ -8,7 +8,7 @@ namespace MultipleGadgets def Order : ℕ := 0x30644e72e131a029b85045b68181585d2833e84879b9709143e1f593f0000001 variable [Fact (Nat.Prime Order)] abbrev F := ZMod Order -abbrev Gates := GatesGnark8 Order +abbrev Gates := GatesGnark9 Order def DummyHash (In_1: F) (In_2: F) (k: F -> Prop): Prop := ∃gate_0, gate_0 = Gates.mul In_1 In_2 ∧ diff --git a/test/TestExtractGadgetsVectors.lean b/test/TestExtractGadgetsVectors.lean index 69dae8a..e12d6ae 100644 --- a/test/TestExtractGadgetsVectors.lean +++ b/test/TestExtractGadgetsVectors.lean @@ -8,7 +8,7 @@ namespace MultipleGadgetsVectors def Order : ℕ := 0x30644e72e131a029b85045b68181585d2833e84879b9709143e1f593f0000001 variable [Fact (Nat.Prime Order)] abbrev F := ZMod Order -abbrev Gates := GatesGnark8 Order +abbrev Gates := GatesGnark9 Order def VectorGadget_3_3_3_3 (In_1: Vector F 3) (In_2: Vector F 3) (Nested: Vector (Vector F 3) 3) (k: Vector F 3 -> Prop): Prop := ∃_ignored_, _ignored_ = Gates.mul In_1[0] In_2[0] ∧ diff --git a/test/TestGadgetExtraction.lean b/test/TestGadgetExtraction.lean index 1f2a9e2..37b76e2 100644 --- a/test/TestGadgetExtraction.lean +++ b/test/TestGadgetExtraction.lean @@ -8,7 +8,7 @@ namespace VectorGadget def Order : ℕ := 0x30644e72e131a029b85045b68181585d2833e84879b9709143e1f593f0000001 variable [Fact (Nat.Prime Order)] abbrev F := ZMod Order -abbrev Gates := GatesGnark8 Order +abbrev Gates := GatesGnark9 Order def VectorGadget_3_3_3_3 (In_1: Vector F 3) (In_2: Vector F 3) (Nested: Vector (Vector F 3) 3) (k: Vector F 3 -> Prop): Prop := ∃_ignored_, _ignored_ = Gates.mul In_1[0] In_2[0] ∧ diff --git a/test/TestMerkleRecover.lean b/test/TestMerkleRecover.lean index eff0016..8cea3e7 100644 --- a/test/TestMerkleRecover.lean +++ b/test/TestMerkleRecover.lean @@ -8,7 +8,7 @@ namespace MerkleRecover def Order : ℕ := 0x30644e72e131a029b85045b68181585d2833e84879b9709143e1f593f0000001 variable [Fact (Nat.Prime Order)] abbrev F := ZMod Order -abbrev Gates := GatesGnark8 Order +abbrev Gates := GatesGnark9 Order def DummyHash (In_1: F) (In_2: F) (k: F -> Prop): Prop := ∃gate_0, gate_0 = Gates.mul In_1 In_2 ∧ diff --git a/test/TestMyCircuit.lean b/test/TestMyCircuit.lean index ca2142b..5f3228d 100644 --- a/test/TestMyCircuit.lean +++ b/test/TestMyCircuit.lean @@ -8,7 +8,7 @@ namespace MyCircuit def Order : ℕ := 0x30644e72e131a029b85045b68181585d2833e84879b9709143e1f593f0000001 variable [Fact (Nat.Prime Order)] abbrev F := ZMod Order -abbrev Gates := GatesGnark8 Order +abbrev Gates := GatesGnark9 Order diff --git a/test/TestSlicesOptimisation.lean b/test/TestSlicesOptimisation.lean index 09041ea..7bb3020 100644 --- a/test/TestSlicesOptimisation.lean +++ b/test/TestSlicesOptimisation.lean @@ -8,7 +8,7 @@ namespace SlicesOptimisation def Order : ℕ := 0x30644e72e131a029b85045b68181585d2833e84879b9709143e1f593f0000001 variable [Fact (Nat.Prime Order)] abbrev F := ZMod Order -abbrev Gates := GatesGnark8 Order +abbrev Gates := GatesGnark9 Order def SlicesGadget_3_2_4_3_2 (TwoDim: Vector (Vector F 3) 2) (ThreeDim: Vector (Vector (Vector F 4) 3) 2) (k: Vector F 7 -> Prop): Prop := k vec![ThreeDim[0][0][0], ThreeDim[0][0][1], ThreeDim[0][0][2], ThreeDim[0][0][3], TwoDim[0][0], TwoDim[0][1], TwoDim[0][2]] diff --git a/test/TestToBinaryCircuit.lean b/test/TestToBinaryCircuit.lean index ac67461..d955b4f 100644 --- a/test/TestToBinaryCircuit.lean +++ b/test/TestToBinaryCircuit.lean @@ -8,7 +8,7 @@ namespace ToBinaryCircuit def Order : ℕ := 0x30644e72e131a029b85045b68181585d2833e84879b9709143e1f593f0000001 variable [Fact (Nat.Prime Order)] abbrev F := ZMod Order -abbrev Gates := GatesGnark8 Order +abbrev Gates := GatesGnark9 Order def VectorGadget_3_3_3_3 (In_1: Vector F 3) (In_2: Vector F 3) (Nested: Vector (Vector F 3) 3) (k: Vector F 3 -> Prop): Prop := ∃_ignored_, _ignored_ = Gates.mul In_1[0] In_2[0] ∧ diff --git a/test/TestTwoGadgets.lean b/test/TestTwoGadgets.lean index c8b1f9e..65b1ae5 100644 --- a/test/TestTwoGadgets.lean +++ b/test/TestTwoGadgets.lean @@ -8,7 +8,7 @@ namespace TwoGadgets def Order : ℕ := 0x30644e72e131a029b85045b68181585d2833e84879b9709143e1f593f0000001 variable [Fact (Nat.Prime Order)] abbrev F := ZMod Order -abbrev Gates := GatesGnark8 Order +abbrev Gates := GatesGnark9 Order def MyWidget_11 (Test_1: F) (Test_2: F) (k: F -> Prop): Prop := ∃gate_0, gate_0 = Gates.add Test_1 Test_2 ∧