diff --git a/barretenberg/cpp/src/barretenberg/smt_verification/README.md b/barretenberg/cpp/src/barretenberg/smt_verification/README.md index 5fd904c16bbe..9230c4056905 100644 --- a/barretenberg/cpp/src/barretenberg/smt_verification/README.md +++ b/barretenberg/cpp/src/barretenberg/smt_verification/README.md @@ -1,22 +1,8 @@ -# Building cvc5 +# Using cvc5 and smt_verification module -As for now it's required to build cvc5 library manually. +Just build with `smt-verification` preset - - -- inside your home repository do `git clone git@github.com:Sarkoxed/cvc5.git` (temporarily, since they have been merging my patch for a month now) -- inside the cvc5 repo: - - `git checkout finite-field-base-support` - - `./configure.sh production --auto-download --cocoa --cryptominisat -DCMAKE_C_COMPILER=/usr/bin/clang -DCMAKE_CXX_COMPILER=/usr/bin/clang++ --prefix="./tmp-lib"` - - `cd build && make` - - `make install` - -Now you can import it using +Now you can import cvc5 using # How to use smt_circuit library @@ -55,71 +41,132 @@ To store it on the disk just do 2. Initialize the Solver: - `smt_solver::Solver s(str modulus, bool produce_model=false, u32 base=16, u64 timeout)` - - !note that there should be no "0x" part in the modulus hex representation if you put it manually. Otherwise you can use `CircuitSchema.modulus` member. - - `produce_model` flag should be initialized as `true` if you want to check the values obtained using the solver when the result of the check does not meet your expectations. **All the public variables will be constrained to be equal their real value**. - - `base` can be any positive integer, it will mostly be 10 or 16, I guess. + There's an `smt_solver::SolverConfiguration` structure: + + ```cpp + struct SolverConfiguration { + bool produce_models; + uint64_t timeout; + uint32_t debug; + + bool ff_disjunctive_bit; + std::string ff_solver; + }; + ``` + + - `produce_models` - should be initialized as `true` if you want to check the values obtained using the solver when the result of the check does not meet your expectations. **All the public variables will be constrained to be equal their real value**. + - `timeout` - solver timeout in milliseconds + - `debug` - 0, 1, 2 - defines verbosity level of cvc5 + - `ff_disjunctive_bit` - **Advanced**. Should be used to transform assertions like `(x == 0) | (x == 1)` to `x^2 - x = 0` + - `ff_solver` - "gb" or "split-gb". **Advanced**. Change the solver approach to solving systems over finite fields. + + There's a `default_solver_config = { true, 0, 0, false, ""}` + + More info on `SolverConfiguration` can be found [here](solver/solver.hpp) - `timeout` solver timeout in milliseconds + Now we can initialize the solver + + `smt_solver::Solver s(str modulus, config=default_solver_config, u32 base=16, u32 bvsize=254)` + + - `base` can be any positive integer, it will mostly be 10 or 16, I guess. Default is 16. + - `bvsize` defines BitVector size in bits, when you use `BVTerm`. Default is 254. + + **!Note that there should be no "0x" part in the modulus hex representation if you put it manually. Otherwise you can use `CircuitSchema.modulus` member that is exported directly from circuit.** + + To verify that the system has solution, just run `Solver::check` method. It will return the boolean. + + `Solver` instance has useful method `print_assertions` that will output all the assertions in kind of human readable format(not SMT2 lang). + + There's also a function `smt_timer(Solver& s, bool mins)` in `barretenberg/smt_verification/util/smt_util.hpp` that will run the `check`, measure the time in minutes/seconds and send it to stdout. 3. Initialize the Circuit - From now and on we will use `smt_terms::FFTerm`, `smt_term::FFITerm` and `smt_terms::Bool` types to operate inside the solver. - - `FFTerm` - the symbolic value that simulates finite field elements. + From now on we will use `smt_terms::STerm` and `smt_terms::Bool` types to operate inside the solver. - `FFITerm` - the symbolic value that simulates integer elements which behave like finite field ones. Useful, when you want to create range constraints or perform operations like XOR. - - `Bool` - simulates the boolean values and mostly will be used only to simulate complex `if` statements if needed. + You can choose the behaviour of symbolic variables by providing the specific type to `STerm` or `Circuit` constructor: + + - `smt_terms::TermType::FFTerm` - symbolic variables that simulate finite field arithmetic. + - `smt_terms::TermType::FFITerm` - symbolic variables that simulate integer elements which behave like finite field ones. Useful, when you want to create range constraints. Bad when you try multiplication. + - `smt_terms::TermType::BVTerm` - symbolic variables that simulate $\pmod{2^n}$ arithmetic. Useful, when you test uint circuits. Supports range constraints and bitwise operations. Doesn't behave like finite field element. + + All these types use different solver engines. The most general one is `FFTerm`. + + `Bool` - simulates the boolean values and mostly will be useful to simulate complex `if` statements if needed. + + Now we can create symbolic circuit - - ```smt_circuit::Circuit circuit(CircuitSchema c_info, Solver* s, str tag="")``` - - ```smt_circuit::Circuit circuit(CircuitSchema c_info, Solver* s, str tag="")``` + ```smt_circuit::Circuit circuit(CircuitSchema c_info, Solver* s, TermType type, str tag="")``` - It will generate all the symbolic values of the circuit wires values, add all the gate constrains, create a map `string->FFTerm` and the inverse of it. - In case you want to create two similar circuits with the same solver and schema, then you should specify the tag(name) of a circuit. - FFTerm/FFITerm templates will define what theory core the solver should use. + It will generate all the symbolic values of the circuit wires, add all the gate constrains, create a map `term_name->STerm` and the inverse of it. Where `term_name` is the the name you provided earlier. + + In case you want to create two similar circuits with the same `solver` and `schema`, then you should specify the tag(name) of a circuit. Then you can get the previously named variables via `circuit[name]` or any other variable by `circuit[idx]`. + + There is a method `Circuit::simulate_circuit_eval(vector w)`. It checks that the evaluation process is correct for this particular witness. + 4. Terms creation - You are able to create two types of ff terms: - - `FFTerm Var(str name, Solver* s)` - creates a symbolic finite field variable - - `FFTerm Const(str val, Solver* s, u32 base=16)` - creates a numeric value. + You can initialize symbolic variable via `STerm::Var(str name, &solver, TermType type)` or `STerm::Const(str val, &solver, TermType type, u32 base=16)` + + But also you can use `FFVar(str name, &Solver)` or equivalently via `FFIVar` and `BVVar` so you don't have to mess with types. + + Use `FFConst(str value, &Solver, u32 base=16)`/`FFIConst`/`BVConst` to create constants. However `STerm` is fully arithmetically compatible with `bb::fr` so you can avoid doing this. + + **!Note STerms of distinct types can't be mixed** + + You can add, subtract and multiply these variables(including `+=`, `-=`, etc); + Also there are two functions: + - `batch_add(std::vector& terms)` + - `batch_mul(std::vector& terms)` - You can add, subtract, multiply and divide these variables(including !+, !-, etc); - Also there are two functions : - - `batch_add(std::vector& terms)` - - `batch_mul(std::vector& terms)` to create an addition/multiplication Term in one call - - You can create a constraint `==` or `!=` that will be included directly into solver. - `FFITerm` works the same as `FFTerm`. - - Also there is a Bool type: - - `Bool Bool(FFTerm/FFITerm t)` or `Bool Bool(bool b, Solver* s)` + `FFITerm` also can be used to create range constraints. e.g. `x <= bb::fr(2).pow(10);` + + `BVTerm` can be used to create bitwise constraints. e.g. `STerm y = x^z` or `STerm y = x.rotr(10)`. And range constraints too. + + You can create a constraint `==` or `!=` that will be included directly into solver. e.g. `x == y;` + + **!Note: In this case it's not comparison operators** + + There is a Bool type: + - `Bool Bool(STerm t)` or `Bool Bool(bool b, Solver* s)` - You can `|, &, ==, !=` these variables and also `batch_or`, `batch_and` them. - To create a constraint you should call `assert_term` method. + You can `|, &, ==, !=, !` these variables and also `batch_or`, `batch_and` them. + To create a constraint you should call `Bool::assert_term()` method. The way I see the use of Bool types is to create terms like `(a == b && c == 1) || (a != b && c == 0)`, `(a!=1)||(b!=2)|(c!=3)` and of course more sophisticated ones. - Note! That constraint like `Bool(FFTerm a) == Bool(FFITerm b)` won't work, since their types differ. - Note! `Bool(a == b)` won't work since `a==b` will create an equality constrain as I mentioned earlier and the return type of this operation is `void`. + **!Note that constraint like `(Bool(STerm a) == Bool(STerm b)).assert_term()`, where a has `FFTerm` type and b has `FFITerm` type, won't work, since their types differ.** + **!Note `Bool(a == b)` won't work since `a==b` will create an equality constraint as I mentioned earlier and the return type of this operation is `void`.** 5. Post model checking After generating all the constrains you should call `bool res = solver.check()` and depending on your goal it could be `true` or `false`. In case you expected `false` but `true` was returned you can then check what went wrong. - You should generate an unordered map with `str->term` values and ask the solver to obtain `unoredered_map res = solver.model(unordered_map terms)`. + You should generate an unordered map with `str->term` values and ask the solver to obtain `unoredered_map res = solver.model(unordered_map terms)`. + Or you can provide a vector of terms that you want to check and the return map will contain their symbolic names that are given during initialization. Specifically either it's the name that you set or `var_{i}`. + Now you have the values of the specified terms, which resulted into `true` result. + **!Note that the return values are decimal strings/binary strings**, so if you want to use them later you should use `FFConst`, etc. + + Also, there is a header file "barretenberg/common/smt_model.hpp" with two functions: + - `default_model(verctor special_names, circuit1, circuit2, *solver, fname="witness.out")` + - `default_model_single(vector special_names, circuit, *solver, fname="witness.out)` + These functions will write witness variables in c-like array format into file named `fname`. + The vector of special names is the values that you want ot see in stdout. + 6. Automated verification of a unique witness - There's also a function `pair unique_witness(CircuitSchema circuit_info, Solver* s, vector equall_variables, vector nequal_variables, vector at_least_one_equal_variable, vector at_least_one_nequal_variable)` that will create two separate circuits and constrain the provided variables. Then later you can run `s.check()` and `s.model()` if you wish. + There's a function `pair unique_wintes(CircuitSchema circuit_info, Solver*, TermType type, vector equal)` + It will create two separate circuits, constrain variables with names from `equal` to be equal acrosss the circuits, and set all the other variables to be not equal at the same time. + + Another one is `pair unique_witness_ext(CircuitSchema circuit_info, Solver* s, TermType type, vector equal_variables, vector nequal_variables, vector at_least_one_equal_variable, vector at_least_one_nequal_variable)` that does the same but provides you with more flexible settings. + + The return circuits can be useful, if you want to define some additional constraints, that are not covered by the the above functions. + You can call `s.check`, `s.model`, `smt_timer` or `default_model` further. ## 3. Simple examples @@ -134,19 +181,19 @@ To store it on the disk just do builder.set_variable_name(a.witness_index, "a"); builder.set_variable_name(b.witness_index, "b"); builder.set_variable_name(c.witness_index, "c"); - ASSERT_TRUE(builder.check_circuit()); + ASSERT_TRUE(CircuitChecker::check(builder)); auto buf = builder.export_circuit(); smt_circuit::CircuitSchema circuit_info = smt_circuit::unpack_from_buffer(buf); - smt_solver::Solver s(circuit_info.modulus, {true, 0}); - smt_circuit::Circuit circuit(circuit_info, &s); - smt_terms::FFTerm a1 = circuit["a"]; - smt_terms::FFTerm b1 = circuit["b"]; - smt_terms::FFTerm c1 = circuit["c"]; - smt_terms::FFTerm two = smt_terms::FFTerm::Const("2", &s, 10); - smt_terms::FFTerm thr = smt_terms::FFTerm::Const("3", &s, 10); - smt_terms::FFTerm cr = smt_terms::FFTerm::Var("cr", &s); + smt_solver::Solver s(circuit_info.modulus); + smt_circuit::Circuit circuit(circuit_info, &s, smt_terms::TermType::FFTerm); + smt_terms::STerm a1 = circuit["a"]; + smt_terms::STerm b1 = circuit["b"]; + smt_terms::STerm c1 = circuit["c"]; + smt_terms::STerm two = smt_terms::FFConst("2", &s, 10); + smt_terms::STerm thr = smt_terms::FFConst("3", &s, 10); + smt_terms::STerm cr = smt_terms::FFVar("cr", &s); cr = (two * a1) / (thr * b1); c1 != cr; @@ -164,21 +211,21 @@ To store it on the disk just do builder.set_variable_name(a.witness_index, "a"); builder.set_variable_name(b.witness_index, "b"); builder.set_variable_name(c.witness_index, "c"); - ASSERT_TRUE(builder.check_circuit()); + ASSERT_TRUE(CircuitChecker::check(builder)); auto buf = builder.export_circuit(); smt_circuit::CircuitSchema circuit_info = smt_circuit::unpack_from_buffer(buf); - smt_solver::Solver s(circuit_info.modulus, {true, 0}); - smt_circuit::Circuit circuit(circuit_info, &s); + smt_solver::Solver s(circuit_info.modulus); + smt_circuit::Circuit circuit(circuit_info, &s, smt_terms::TermType::FFTerm); - smt_terms::FFTerm a1 = circuit["a"]; - smt_terms::FFTerm b1 = circuit["b"]; - smt_terms::FFTerm c1 = circuit["c"]; + smt_terms::STerm a1 = circuit["a"]; + smt_terms::STerm b1 = circuit["b"]; + smt_terms::STerm c1 = circuit["c"]; - smt_terms::FFTerm two = smt_terms::FFTerm::Const("2", &s, 10); - smt_terms::FFTerm thr = smt_terms::FFTerm::Const("3", &s, 10); - smt_terms::FFTerm cr = smt_terms::FFTerm::Var("cr", &s); + smt_terms::STerm two = smt_terms::FFConst("2", &s, 10); + smt_terms::STerm thr = smt_terms::FFConst("3", &s, 10); + smt_terms::STerm cr = smt_terms::FFVar("cr", &s); cr = (two * a1) / (thr * b1); c1 != cr; @@ -196,46 +243,41 @@ To store it on the disk just do ``` ### Unique Witness ```cpp -// two roots of a quadratic eq x^2 + a * x + b = s + // Make sure that quadratic polynomial evaluation doesn't have unique + // witness using unique_witness_ext function + // Find both roots of a quadratic equation x^2 + a * x + b = s + StandardCircuitBuilder builder = StandardCircuitBuilder(); field_t a(pub_witness_t(&builder, fr::random_element())); field_t b(pub_witness_t(&builder, fr::random_element())); - info("a = ", a); - info("b = ", b); builder.set_variable_name(a.witness_index, "a"); builder.set_variable_name(b.witness_index, "b"); field_t z(witness_t(&builder, fr::random_element())); field_t ev = z * z + a * z + b; - info("ev = ", ev); builder.set_variable_name(z.witness_index, "z"); builder.set_variable_name(ev.witness_index, "ev"); auto buf = builder.export_circuit(); smt_circuit::CircuitSchema circuit_info = smt_circuit::unpack_from_buffer(buf); - smt_solver::Solver s(circuit_info.modulus, {true, 0}); + smt_solver::Solver s(circuit_info.modulus); - std::pair, smt_circuit::Circuit> cirs = - smt_circuit::unique_witness(circuit_info, &s, { "ev" }, { "z" }); + std::pair cirs = + smt_circuit::unique_witness_ext(circuit_info, &s, smt_terms::TermType::FFTerm, { "ev" }, { "z" }); bool res = s.check(); ASSERT_TRUE(res); - for (auto x : s.s.getAssertions()) { - info(x); - info(); - } std::unordered_map terms = { { "z_c1", cirs.first["z"] }, { "z_c2", cirs.second["z"] } }; std::unordered_map vals = s.model(terms); - info(vals["z_c1"]); - info(vals["z_c2"]); + ASSERT_NE(vals["z_c1"], vals["z_c2"]); ``` -### Obtaining the model +### Custom model function ```cpp -void model_variables(Circuit& c, Solver* s, FFTerm& evaluation) +void model_variables(Circuit& c, Solver* s, FFTerm& evaluation) { std::unordered_map terms; terms.insert({ "point", c["point"] }); @@ -250,4 +292,4 @@ void model_variables(Circuit& c, Solver* s, FFTerm& evaluatio } ``` -More examples can be found in *.test.cpp files +More examples can be found in [terms/ffterm.test.cpp](terms/ffterm.test.cpp), [circuit/circuit.test.cpp](circuit/circuit.test.cpp) and [smt_polynomials.test.cpp](smt_polynomials.test.cpp). \ No newline at end of file