From fd3aaa06c56cdae183977916ebd1fb86f1eb468b Mon Sep 17 00:00:00 2001 From: adelapie Date: Thu, 21 Apr 2022 11:18:06 +0200 Subject: [PATCH] improved output via circom sym file, added simple command-line tool --- Manifest.toml | 79 +++++++++++++++++++++++++++++++++++- Project.toml | 2 + ecne.jl | 37 +++++++++++++++++ src/Manifest.toml | 18 ++++++++ src/Project.toml | 2 + src/R1CSConstraintSolver.jl | 25 ++++++++---- target/division.r1cs | Bin 0 -> 308 bytes target/division.sym | 5 +++ verify.jl | 11 +++++ 9 files changed, 170 insertions(+), 9 deletions(-) create mode 100644 ecne.jl create mode 100644 src/Manifest.toml create mode 100644 src/Project.toml create mode 100644 target/division.r1cs create mode 100644 target/division.sym create mode 100644 verify.jl diff --git a/Manifest.toml b/Manifest.toml index 24e8e43..a7a1004 100644 --- a/Manifest.toml +++ b/Manifest.toml @@ -6,6 +6,12 @@ git-tree-sha1 = "b859af958bc9440b44e6d3013fe5a34b18d8a7fc" uuid = "c3fe647b-3220-5bb0-a1ea-a7954cac585d" version = "0.23.0" +[[ArgParse]] +deps = ["Logging", "TextWrap"] +git-tree-sha1 = "3102bce13da501c9104df33549f511cd25264d7d" +uuid = "c7e460c6-2fb9-53a9-8c5b-16f535851c63" +version = "1.1.4" + [[ArgTools]] uuid = "0dad84c5-d112-42e6-8d28-ef12dabb789f" @@ -27,6 +33,18 @@ git-tree-sha1 = "60e9121d9ea044c30a04397e59b00c5d9eb826ee" uuid = "00ebfdb7-1f24-5e51-bd34-a7502290713f" version = "2.5.0" +[[CSV]] +deps = ["CodecZlib", "Dates", "FilePathsBase", "InlineStrings", "Mmap", "Parsers", "PooledArrays", "SentinelArrays", "Tables", "Unicode", "WeakRefStrings"] +git-tree-sha1 = "9519274b50500b8029973d241d32cfbf0b127d97" +uuid = "336ed68f-0bac-5ca0-87d4-7b16caf5d00b" +version = "0.10.2" + +[[CodecZlib]] +deps = ["TranscodingStreams", "Zlib_jll"] +git-tree-sha1 = "ded953804d019afa9a3f98981d99b33e3db7b6da" +uuid = "944b1d66-785c-5afd-91f1-9de20f533193" +version = "0.7.0" + [[Combinatorics]] git-tree-sha1 = "08c8b6831dc00bfea825826be0bc8336fc369860" uuid = "861a8166-3701-5b0c-9a16-15d98fcdc6aa" @@ -38,6 +56,10 @@ git-tree-sha1 = "44c37b4636bc54afac5c574d2d02b625349d6582" uuid = "34da2185-b29b-5c13-b0c7-acf172513d20" version = "3.41.0" +[[CompilerSupportLibraries_jll]] +deps = ["Artifacts", "Libdl"] +uuid = "e66e0078-7015-5450-92f7-15fbd957f2ae" + [[DataAPI]] git-tree-sha1 = "cc70b17275652eb47bc9e5f81635981f13cea5c8" uuid = "9a962f9c-6df0-11e9-0e5d-c546b8b5ee8a" @@ -77,12 +99,28 @@ git-tree-sha1 = "56559bbef6ca5ea0c0818fa5c90320398a6fbf8d" uuid = "e2ba6199-217a-4e67-a87a-7c52f15ade04" version = "0.1.8" +[[FilePathsBase]] +deps = ["Compat", "Dates", "Mmap", "Printf", "Test", "UUIDs"] +git-tree-sha1 = "129b104185df66e408edd6625d480b7f9e9823a0" +uuid = "48062228-2e41-5def-b9a4-89aafe57970f" +version = "0.9.18" + +[[Future]] +deps = ["Random"] +uuid = "9fa8497b-333b-5362-9e8d-4d0656e87820" + [[GroupsCore]] deps = ["Markdown", "Random"] git-tree-sha1 = "9e1a5e9f3b81ad6a5c613d181664a0efc6fe6dd7" uuid = "d5909c97-4eac-4ecc-a3dc-fdd0858a4120" version = "0.4.0" +[[InlineStrings]] +deps = ["Parsers"] +git-tree-sha1 = "61feba885fac3a407465726d0c330b3055df897f" +uuid = "842dd82b-1e85-43dc-bf29-5d0ee9dffc48" +version = "1.1.2" + [[InteractiveUtils]] deps = ["Markdown"] uuid = "b77e0a4c-d291-57a0-90e8-8db25a27a240" @@ -124,7 +162,7 @@ uuid = "29816b5a-b9ab-546f-933c-edad1886dfa8" uuid = "8f399da3-3557-5675-b5ff-fb832c97cbdb" [[LinearAlgebra]] -deps = ["Libdl"] +deps = ["Libdl", "libblastrampoline_jll"] uuid = "37e2e46d-f89d-539d-b4ee-838fcccc9c8e" [[Logging]] @@ -159,6 +197,10 @@ version = "1.0.13" [[NetworkOptions]] uuid = "ca575930-c2e3-43a9-ace4-1e988b2c1908" +[[OpenBLAS_jll]] +deps = ["Artifacts", "CompilerSupportLibraries_jll", "Libdl"] +uuid = "4536629a-c528-5b80-bd46-f80d51c5b363" + [[OrderedCollections]] git-tree-sha1 = "85f8e6578bf1f9ee0d11e7bb1b1456435479d47c" uuid = "bac558e1-5e72-5ebc-8fee-abe8a469f55d" @@ -186,6 +228,12 @@ git-tree-sha1 = "624c9dcc6200494697a65ee7de521c51ca2d1b9d" uuid = "14b8a8f1-9102-5b29-a752-f990bacb7fe1" version = "0.7.26" +[[PooledArrays]] +deps = ["DataAPI", "Future"] +git-tree-sha1 = "28ef6c7ce353f0b35d0df0d5930e0d072c1f5b9b" +uuid = "2dfb63ee-cc39-5dd5-95bd-886bf059d720" +version = "1.4.1" + [[Printf]] deps = ["Unicode"] uuid = "de0858da-6303-5e67-8744-51eddeeeb8d7" @@ -199,7 +247,7 @@ deps = ["InteractiveUtils", "Markdown", "Sockets", "Unicode"] uuid = "3fa0cd96-eef1-5676-8a61-b3b8758bbffb" [[Random]] -deps = ["Serialization"] +deps = ["SHA", "Serialization"] uuid = "9a3f8284-a2c9-5f02-9a11-845980a1fd5c" [[RandomExtensions]] @@ -211,6 +259,12 @@ version = "0.4.3" [[SHA]] uuid = "ea8e919c-243c-51af-8825-aaa63cd721ce" +[[SentinelArrays]] +deps = ["Dates", "Random"] +git-tree-sha1 = "6a2f7d70512d205ca8c7ee31bfa9f142fe74310c" +uuid = "91c51154-3ec4-41a3-a24f-3f23e20d615c" +version = "1.3.12" + [[Serialization]] uuid = "9e88b42a-f829-5b0c-bbe9-9e923198166b" @@ -253,6 +307,11 @@ uuid = "a4e569a6-e804-4fa4-b0f3-eef7a1d5b13e" deps = ["InteractiveUtils", "Logging", "Random", "Serialization"] uuid = "8dfed614-e22c-5e08-85e1-65c5234f0b40" +[[TextWrap]] +git-tree-sha1 = "9250ef9b01b66667380cf3275b3f7488d0e25faf" +uuid = "b718987f-49a8-5099-9789-dcd902bef87d" +version = "1.0.1" + [[TimerOutputs]] deps = ["ExprTools", "Printf"] git-tree-sha1 = "97e999be94a7147d0609d0b9fc9feca4bf24d76b" @@ -264,6 +323,12 @@ git-tree-sha1 = "0952c9cee34988092d73a5708780b3917166a0dd" uuid = "0796e94c-ce3b-5d07-9a54-7f471281c624" version = "0.5.21" +[[TranscodingStreams]] +deps = ["Random", "Test"] +git-tree-sha1 = "216b95ea110b5972db65aa90f88d8d89dcb8851c" +uuid = "3bb67fe8-82b1-5028-8e26-92a6c54297fa" +version = "0.9.6" + [[UUIDs]] deps = ["Random", "SHA"] uuid = "cf7118a7-6976-5b1a-9a39-7adc72f591a4" @@ -276,10 +341,20 @@ version = "1.0.2" [[Unicode]] uuid = "4ec0a83e-493e-50e2-b9ac-8f72acf5a8f5" +[[WeakRefStrings]] +deps = ["DataAPI", "InlineStrings", "Parsers"] +git-tree-sha1 = "b1be2855ed9ed8eac54e5caff2afcdb442d52c23" +uuid = "ea10d353-3f73-51f8-a26c-33c1cb351aa5" +version = "1.4.2" + [[Zlib_jll]] deps = ["Libdl"] uuid = "83775a58-1f1d-513f-b197-d71354ab007a" +[[libblastrampoline_jll]] +deps = ["Artifacts", "Libdl", "OpenBLAS_jll"] +uuid = "8e850b90-86db-534c-a0d3-1478176c7d93" + [[nghttp2_jll]] deps = ["Artifacts", "Libdl"] uuid = "8e850ede-7688-5339-a07c-302acd2aaf8d" diff --git a/Project.toml b/Project.toml index 501c26b..c6ff134 100644 --- a/Project.toml +++ b/Project.toml @@ -5,7 +5,9 @@ version = "0.1.0" [deps] AbstractAlgebra = "c3fe647b-3220-5bb0-a1ea-a7954cac585d" +ArgParse = "c7e460c6-2fb9-53a9-8c5b-16f535851c63" BenchmarkTools = "6e4b80f9-dd63-53aa-95a3-0cdb28fa8baf" +CSV = "336ed68f-0bac-5ca0-87d4-7b16caf5d00b" Combinatorics = "861a8166-3701-5b0c-9a16-15d98fcdc6aa" DataStructures = "864edb3b-99cc-5e75-8d2d-829cb0a9cfe8" Dates = "ade2ca70-3891-5945-98fb-dc099432e06a" diff --git a/ecne.jl b/ecne.jl new file mode 100644 index 0000000..a2e91a9 --- /dev/null +++ b/ecne.jl @@ -0,0 +1,37 @@ +# ecne command-line tool +# TODO: add support for trusted R1CS files + +using Dates +using ArgParse + +import R1CSConstraintSolver: solveWithTrustedFunctions + +function main(args) + + s = ArgParseSettings(description = "Ecne command-line helper") + + @add_arg_table! s begin + "--r1cs" + help = "de-optimized R1CS file to verify" + required = true + "--name" + help = "Circuit name" + required = true + "--sym" + help = "symbol file with labels" + required = true + "--trusted" + help = "Optional trusted R1CS file" + end + + parsed_args = parse_args(args, s) + + try + solveWithTrustedFunctions(parsed_args["r1cs"], parsed_args["sym"], parsed_args["name"]) + catch e + println("Error while running solveWithTrustedFunctions", e) + end +end + +main(ARGS) + diff --git a/src/Manifest.toml b/src/Manifest.toml new file mode 100644 index 0000000..c0ca27a --- /dev/null +++ b/src/Manifest.toml @@ -0,0 +1,18 @@ +# This file is machine-generated - editing it directly is not advised + +julia_version = "1.7.2" +manifest_format = "2.0" + +[[deps.ArgParse]] +deps = ["Logging", "TextWrap"] +git-tree-sha1 = "3102bce13da501c9104df33549f511cd25264d7d" +uuid = "c7e460c6-2fb9-53a9-8c5b-16f535851c63" +version = "1.1.4" + +[[deps.Logging]] +uuid = "56ddb016-857b-54e1-b83d-db4d58db5568" + +[[deps.TextWrap]] +git-tree-sha1 = "9250ef9b01b66667380cf3275b3f7488d0e25faf" +uuid = "b718987f-49a8-5099-9789-dcd902bef87d" +version = "1.0.1" diff --git a/src/Project.toml b/src/Project.toml new file mode 100644 index 0000000..02ac93f --- /dev/null +++ b/src/Project.toml @@ -0,0 +1,2 @@ +[deps] +ArgParse = "c7e460c6-2fb9-53a9-8c5b-16f535851c63" diff --git a/src/R1CSConstraintSolver.jl b/src/R1CSConstraintSolver.jl index ca99d54..e236d8e 100644 --- a/src/R1CSConstraintSolver.jl +++ b/src/R1CSConstraintSolver.jl @@ -6,7 +6,7 @@ using DataStructures using Profile using Dates using JSON - +using CSV const bjj_p = BigInt(21888242871839275222246405745257275088548364400416034343698204186575808495617) @@ -421,7 +421,7 @@ function fix_number(x::BigInt) end # a utility for pretty printing equations -function printEquation(x::R1CSEquation) +function printEquation(x::R1CSEquation, index_to_signal::Array{String,1}) function get_lin(x) if length(nonzeroKeys(x)) == 0 return "0" @@ -429,7 +429,7 @@ function printEquation(x::R1CSEquation) return "(" * join( [ - string(fix_number(x[key].d)) * " * x_{" * string(key) * "}" + string(fix_number(x[key].d)) * " * " * string(index_to_signal[key-1]) * "" for key in nonzeroKeys(x) ], " + ", @@ -487,6 +487,7 @@ end function solveWithTrustedFunctions( input_r1cs::String, + input_sym::String, input_r1cs_name::String; trusted_r1cs::Vector{String}=Vector{String}([]), trusted_r1cs_names::Vector{String}=Vector{String}([]), @@ -527,7 +528,7 @@ function solveWithTrustedFunctions( println(specials) return true end - result = SolveConstraintsSymbolic(reduced, specials, knowns_main, debug, outs_main, num_variables) + result = SolveConstraintsSymbolic(reduced, specials, knowns_main, debug, outs_main, num_variables, input_sym) if result == true if length(function_list) != 0 if printRes @@ -642,6 +643,7 @@ function SolveConstraintsSymbolic( debug::Bool=false, target_variables::Vector{Int64}=[], num_variables::Int=-1, + input_sym::String="default.sym" ) num_unknowns = [length(setdiff(getVariables(x), Set(known_variables))) for x in constraints] @@ -1622,6 +1624,15 @@ function SolveConstraintsSymbolic( end ## in this case, we solved for all the target variables, which means that we're in good shape. + ## parse sym file with csv reader + + csv_reader = CSV.File(input_sym; header=["i1", "i2", "i3", "signal"], skipto=0) + index_to_signal = String[] + + for row in csv_reader + push!(index_to_signal ,"$(row.signal)") + end + for i = 1:length(constraints) all_unique = true for var in getVariables(constraints[i]) @@ -1638,10 +1649,10 @@ function SolveConstraintsSymbolic( if !display_eq[i] continue end - #println("constraint #", i) - #printEquation(constraints[i]) + println("constraint #", i) + printEquation(constraints[i], index_to_signal) for u in getVariables(constraints[i]) - #println(variable_states[u]) + println(variable_states[u]) end end return false diff --git a/target/division.r1cs b/target/division.r1cs new file mode 100644 index 0000000000000000000000000000000000000000..fe3043088202d085fe02d21860f2ada6ffa88984 GIT binary patch literal 308 zcmXRiOfF_*U|?VdVkRJ-1H>Qz5(Dvp;KSsv51l6#?5y;7VXP4w(b%}nHDHJ40>g(z zeklepy&xJN0GS0^=ss;eTNG+TI literal 0 HcmV?d00001 diff --git a/target/division.sym b/target/division.sym new file mode 100644 index 0000000..9fd6c97 --- /dev/null +++ b/target/division.sym @@ -0,0 +1,5 @@ +1,1,0,main.out +2,2,0,main.a +3,3,0,main.b +4,4,0,main.c +5,5,0,main.d diff --git a/verify.jl b/verify.jl new file mode 100644 index 0000000..676d4a5 --- /dev/null +++ b/verify.jl @@ -0,0 +1,11 @@ +using Dates +import R1CSConstraintSolver: solveWithTrustedFunctions + + + +try + solveWithTrustedFunctions("division.r1cs", "division!") +catch e + println(e) + println("File didn't compile") +end