diff --git a/barretenberg/cpp/src/barretenberg/smt_verification/README.md b/barretenberg/cpp/src/barretenberg/smt_verification/README.md index 9230c405690..aa12cccf666 100644 --- a/barretenberg/cpp/src/barretenberg/smt_verification/README.md +++ b/barretenberg/cpp/src/barretenberg/smt_verification/README.md @@ -1,14 +1,14 @@ # Using cvc5 and smt_verification module -Just build with `smt-verification` preset +You have to install the following packages on your system: `sudo apt install python3-pip python3.11-venv` -Now you can import cvc5 using +Then just build with `smt-verification` preset. # How to use smt_circuit library ## 1. Setting variable names during circuit creation and exporting the circuit. -### There're five new methods inside (for now standard) circuit_builder +### There're four new methods inside Standard and Ultra CircuitBuilders - ```set_variable_name(u32 index, str name)``` - assignes a name to a variable. Specifically, binds a name with the first index of an equivalence class. @@ -18,9 +18,9 @@ Now you can import cvc5 using - ```export_circuit()``` - exports all variables, gates, and assigned names to an msgpack-compatible buffer namely `msgpack::sbuffer`. -To store it on the disk just do +To store it on the disk just do the following -```cpp +```c++ msgpack::sbuffer buffer = circuit.export_circuit(); std::fstream myfile; @@ -49,20 +49,26 @@ To store it on the disk just do uint64_t timeout; uint32_t debug; - bool ff_disjunctive_bit; + bool ff_elim_disjunctive_bit; std::string ff_solver; + + bool lookup_enabled; }; ``` - `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_elim_disjunctive_bit` - **Advanced**. Should be used to transform assertions like `(x == 0) | (x == 1)` to `x^2 - x = 0` when set to true - `ff_solver` - "gb" or "split-gb". **Advanced**. Change the solver approach to solving systems over finite fields. + - `lookup_enabled` - enables set theory inside the solver. Have to be true when we are dealing with lookup tables. - There's a `default_solver_config = { true, 0, 0, false, ""}` + There're two default configs in `smt_solver` namespace - More info on `SolverConfiguration` can be found [here](solver/solver.hpp) + - `default_solver_config = { true, 0, 0, false, "", false}` + - `ultra_solver_config = {true, 0, 0, false, "", true}` + + More info on `SolverConfiguration` can be found in [solver.hpp](solver/solver.hpp) Now we can initialize the solver @@ -77,8 +83,22 @@ To store it on the disk just do `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. - + There's also a function `smt_timer(Solver& s)` in `barretenberg/smt_verification/util/smt_util.hpp` that will run the `check`, measure the time in minutes:seconds and send it to stdout. + + + All the tables are exoported directly from circuit, but if you want to create your own table, there're two methods for this: + + - `Solver::create_table(vector& table)` - creates a set of values. + - `Solver::create_lookup_table(vector>& table)` - creates a table with three columns. + + ```c++ + std::vector> table = { { FFConst("1", &s), FFConst("2", &s), FFConst("3", &s) }, + { FFConst("4", &s), FFConst("5", &s), FFConst("6", &s) } }; + cvc5::Term symbolic_table = s.create_lookup_table(table); + ``` + + There is more on `FFConst` in the following sections. + 3. Initialize the Circuit From now on we will use `smt_terms::STerm` and `smt_terms::Bool` types to operate inside the solver. @@ -86,7 +106,8 @@ To store it on the disk just do 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::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::ITerm` - symbolic variables that simulate ordinary integer elements. Useful, when you want to create range constraints and operate with signed values that are not shrinked modulo smth. - `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`. @@ -95,15 +116,19 @@ To store it on the disk just do Now we can create symbolic circuit - ```smt_circuit::Circuit circuit(CircuitSchema c_info, Solver* s, TermType type, str tag="")``` + - ```smt_circuit::StandardCircuit circuit(CircuitSchema c_info, Solver* s, TermType type, str tag="", bool optimizations=true)``` + - ```smt_circuit::UltraCircuit circuit(CircuitSchema c_info, Solver* s, TermType type, str tag="", bool optimizations=true)``` 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. + 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. + + **Advanced** If you don't want the circuit optimizations to be applied then you should set `optimizations` to `false`. Optimizations interchange the complex circuits like bitwise XOR with simple XOR operation. More on optimizations can be found [standard_circuit.cpp](circuit/standard_circuit.cpp) - 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. + After the symbolic circuit is initialized, 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. (Only in Standard for now). 4. Terms creation @@ -122,13 +147,20 @@ To store it on the disk just do to create an addition/multiplication Term in one call - `FFITerm` also can be used to create range constraints. e.g. `x <= bb::fr(2).pow(10);` + `FFITerm` also can be used to create range constraints. e.g. `x <= bb::fr(2).pow(10) - 1;` `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** + **!Note: In this case these are not comparison operators** + + Also you can create set inclusion constraints. After creating a table(shown in section 2) there're two options: + + - `STerm::in(cvc5::Term table&)` - simple set inclusion. + - `static STerm::in_table(std::vector entry, cvc5::Term& table)` - lookup table inclusion. + + --- There is a Bool type: - `Bool Bool(STerm t)` or `Bool Bool(bool b, Solver* s)` @@ -140,35 +172,72 @@ To store it on the disk just do **!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)`. - 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. +## 3. 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)`. + 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` with base 10, 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)` +Also, there is a header file "barretenberg/smt_verification/utl/smt_util.hpp" that contains two useful 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. +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 +## 4. Automated verification of a unique witness +There's a static member of `StandardCircuit` and `UltraCircuit` + +- `pair StandardCircuit::unique_wintes(CircuitSchema circuit_info, Solver*, TermType type, vector equal, bool optimizations)` +- `pair UltraCircuit::unique_wintes(CircuitSchema circuit_info, Solver*, TermType type, vector equal, bool optimizations)` + +They 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 StandardCircuit::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. +- Same in `UltraCircuit` - 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. +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. - 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. +## 5. smt_util.hpp +Besides already mentioned `smt_timer`, `default_model` and `default_model_single` there're two extra functions in `smt_util.hpp` - 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. +- `pair, vector> base4(uint32_t el)` - that will return base4 accumulators +- `void fix_range_lists(UltraCircuitBuilder& builder)` - Since we are not using the part of the witness, that contains range lists, they are set to 0 by the solver. We need to overwrite them to check the witness obtained by the solver. -## 3. Simple examples +```c++ + UltraCircuitBuilder builder; + uint_ct a = witness_ct(&builder, 0); + uint_ct b = witness_ct(&builder, 0); + builder.set_variable_name(a.get_witness_index(), "a"); + builder.set_variable_name(b.get_witness_index(), "b"); + uint_ct c = a + b; + builder.set_variable_name(c.get_witness_index(), "c"); + + // NOTE BEFORE FINALIZE + for (size_t i = 0; i < builder.get_num_variables(); i++) { + builder.variables[i] = add_unique_output[i]; + } + fix_range_lists(builder); + + info(builder.get_variable(a.get_witness_index())); + info("+"); + info(builder.get_variable(b.get_witness_index())); + info("="); + info(builder.get_variable(c.get_witness_index())); + info("------------------------"); + ASSERT_TRUE(CircuitChecker::check(builder)); +``` +Where `add_unique_output` is a witness obtained by the solver. + +## 6. Simple examples ### Function Equality ```cpp @@ -187,7 +256,7 @@ To store it on the disk just do smt_circuit::CircuitSchema circuit_info = smt_circuit::unpack_from_buffer(buf); smt_solver::Solver s(circuit_info.modulus); - smt_circuit::Circuit circuit(circuit_info, &s, smt_terms::TermType::FFTerm); + smt_circuit::StandardCircuit 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"]; @@ -217,7 +286,7 @@ To store it on the disk just do smt_circuit::CircuitSchema circuit_info = smt_circuit::unpack_from_buffer(buf); smt_solver::Solver s(circuit_info.modulus); - smt_circuit::Circuit circuit(circuit_info, &s, smt_terms::TermType::FFTerm); + smt_circuit::StandardCircuit circuit(circuit_info, &s, smt_terms::TermType::FFTerm); smt_terms::STerm a1 = circuit["a"]; smt_terms::STerm b1 = circuit["b"]; @@ -263,8 +332,8 @@ To store it on the disk just do smt_circuit::CircuitSchema circuit_info = smt_circuit::unpack_from_buffer(buf); smt_solver::Solver s(circuit_info.modulus); - std::pair cirs = - smt_circuit::unique_witness_ext(circuit_info, &s, smt_terms::TermType::FFTerm, { "ev" }, { "z" }); + auto cirs = + smt_circuit::StandardCircuit::unique_witness_ext(circuit_info, &s, smt_terms::TermType::FFTerm, { "ev" }, { "z" }); bool res = s.check(); ASSERT_TRUE(res); @@ -277,7 +346,8 @@ To store it on the disk just do ### Custom model function ```cpp -void model_variables(Circuit& c, Solver* s, FFTerm& evaluation) +template +void model_variables(SymCircuit& c, Solver* s, FFTerm& evaluation) { std::unordered_map terms; terms.insert({ "point", c["point"] }); @@ -292,4 +362,10 @@ void model_variables(Circuit& c, Solver* s, FFTerm& evaluation } ``` -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 + +More examples can be found in + +- [terms/ffterm.test.cpp](terms/ffterm.test.cpp), [terms/ffiterm.test.cpp](terms/ffiterm.test.cpp), [terms/bvterm.test.cpp](terms/bvterm.test.cpp), [terms/iterm.test.cpp](terms/iterm.test.cpp) +- [circuit/standard_circuit.test.cpp](circuit/standard_circuit.test.cpp), [circuit/ultra_circuit](circuit/ultra_circuit.test.cpp) +- [smt_polynomials.test.cpp](smt_polynomials.test.cpp), [smt_examples.test.cpp](smt_examples.test.cpp) +- [bb_tests](bb_tests) diff --git a/barretenberg/cpp/src/barretenberg/smt_verification/circuit/standard_circuit.cpp b/barretenberg/cpp/src/barretenberg/smt_verification/circuit/standard_circuit.cpp index e72d626580a..1365618b02c 100644 --- a/barretenberg/cpp/src/barretenberg/smt_verification/circuit/standard_circuit.cpp +++ b/barretenberg/cpp/src/barretenberg/smt_verification/circuit/standard_circuit.cpp @@ -814,7 +814,6 @@ std::pair StandardCircuit::unique_witness_ext( const std::vector& not_equal_at_the_same_time, bool optimizations) { - // TODO(alex): set optimizations to be true once they are confirmed StandardCircuit c1(circuit_info, s, type, "circuit1", optimizations); StandardCircuit c2(circuit_info, s, type, "circuit2", optimizations); @@ -867,7 +866,6 @@ std::pair StandardCircuit::unique_witness_ext( std::pair StandardCircuit::unique_witness( CircuitSchema& circuit_info, Solver* s, TermType type, const std::vector& equal, bool optimizations) { - // TODO(alex): set optimizations to be true once they are confirmed StandardCircuit c1(circuit_info, s, type, "circuit1", optimizations); StandardCircuit c2(circuit_info, s, type, "circuit2", optimizations); diff --git a/barretenberg/cpp/src/barretenberg/smt_verification/circuit/ultra_circuit.cpp b/barretenberg/cpp/src/barretenberg/smt_verification/circuit/ultra_circuit.cpp index 0b4a0b757eb..c469ead82fc 100644 --- a/barretenberg/cpp/src/barretenberg/smt_verification/circuit/ultra_circuit.cpp +++ b/barretenberg/cpp/src/barretenberg/smt_verification/circuit/ultra_circuit.cpp @@ -26,12 +26,6 @@ UltraCircuit::UltraCircuit( , wires_idxs(circuit_info.wires) , lookup_tables(circuit_info.lookup_tables) { - info("Arithmetic gates: ", selectors[1].size()); - info("Delta Range gates: ", selectors[2].size()); - info("Elliptic gates: ", selectors[3].size()); - info("Aux gates: ", selectors[4].size()); - info("Lookup gates: ", selectors[5].size()); - // Perform all relaxations for gates or // add gate in its normal state to solver @@ -193,6 +187,14 @@ size_t UltraCircuit::handle_lookup_relation(size_t cursor, size_t idx) this->cached_symbolic_tables.insert({ table_idx, this->solver->create_lookup_table(new_table) }); } + // Sort of an optimization. + // However if we don't do this, solver will find a unique witness that corresponds to overflowed value. + if (this->type == TermType::BVTerm && q_r == -64 && q_m == -64 && q_c == -64) { + this->symbolic_vars[w_l_shift_idx] = this->symbolic_vars[w_l_idx] >> 6; + this->symbolic_vars[w_r_shift_idx] = this->symbolic_vars[w_r_idx] >> 6; + this->symbolic_vars[w_o_shift_idx] = this->symbolic_vars[w_o_idx] >> 6; + } + STerm first_entry = this->symbolic_vars[w_l_idx] + q_r * this->symbolic_vars[w_l_shift_idx]; STerm second_entry = this->symbolic_vars[w_r_idx] + q_m * this->symbolic_vars[w_r_shift_idx]; STerm third_entry = this->symbolic_vars[w_o_idx] + q_c * this->symbolic_vars[w_o_shift_idx]; @@ -339,7 +341,7 @@ void UltraCircuit::handle_range_constraints() uint32_t tag = this->real_variable_tags[this->real_variable_index[i]]; if (tag != 0 && this->range_tags.contains(tag)) { uint64_t range = this->range_tags[tag]; - if ((this->type != TermType::FFITerm) && (this->type != TermType::BVTerm)) { + if (this->type == TermType::FFTerm || !this->optimizations) { if (!this->cached_range_tables.contains(range)) { std::vector new_range_table; for (size_t entry = 0; entry < range; entry++) { @@ -352,6 +354,7 @@ void UltraCircuit::handle_range_constraints() } else { this->symbolic_vars[i] <= range; } + optimized[i] = false; } } } @@ -397,11 +400,11 @@ std::pair UltraCircuit::unique_witness_ext( const std::vector& equal, const std::vector& not_equal, const std::vector& equal_at_the_same_time, - const std::vector& not_equal_at_the_same_time) + const std::vector& not_equal_at_the_same_time, + bool optimizations) { - // TODO(alex): set optimizations to be true once they are confirmed - UltraCircuit c1(circuit_info, s, type, "circuit1", false); - UltraCircuit c2(circuit_info, s, type, "circuit2", false); + UltraCircuit c1(circuit_info, s, type, "circuit1", optimizations); + UltraCircuit c2(circuit_info, s, type, "circuit2", optimizations); for (const auto& term : equal) { c1[term] == c2[term]; @@ -449,14 +452,11 @@ std::pair UltraCircuit::unique_witness_ext( * @param equal The list of names of variables which should be equal in both circuits(each is equal) * @return std::pair */ -std::pair UltraCircuit::unique_witness(CircuitSchema& circuit_info, - Solver* s, - TermType type, - const std::vector& equal) +std::pair UltraCircuit::unique_witness( + CircuitSchema& circuit_info, Solver* s, TermType type, const std::vector& equal, bool optimizations) { - // TODO(alex): set optimizations to be true once they are confirmed - UltraCircuit c1(circuit_info, s, type, "circuit1", false); - UltraCircuit c2(circuit_info, s, type, "circuit2", false); + UltraCircuit c1(circuit_info, s, type, "circuit1", optimizations); + UltraCircuit c2(circuit_info, s, type, "circuit2", optimizations); for (const auto& term : equal) { c1[term] == c2[term]; diff --git a/barretenberg/cpp/src/barretenberg/smt_verification/circuit/ultra_circuit.hpp b/barretenberg/cpp/src/barretenberg/smt_verification/circuit/ultra_circuit.hpp index 3d1316d023a..c6ec07a849e 100644 --- a/barretenberg/cpp/src/barretenberg/smt_verification/circuit/ultra_circuit.hpp +++ b/barretenberg/cpp/src/barretenberg/smt_verification/circuit/ultra_circuit.hpp @@ -56,10 +56,12 @@ class UltraCircuit : public CircuitBase { const std::vector& equal = {}, const std::vector& not_equal = {}, const std::vector& equal_at_the_same_time = {}, - const std::vector& not_equal_at_the_same_time = {}); + const std::vector& not_equal_at_the_same_time = {}, + bool optimizations = false); static std::pair unique_witness(CircuitSchema& circuit_info, Solver* s, TermType type, - const std::vector& equal = {}); + const std::vector& equal = {}, + bool optimizations = false); }; }; // namespace smt_circuit \ No newline at end of file diff --git a/barretenberg/cpp/src/barretenberg/smt_verification/solver/solver.cpp b/barretenberg/cpp/src/barretenberg/smt_verification/solver/solver.cpp index 3fde6d7d09f..acd855ad69d 100644 --- a/barretenberg/cpp/src/barretenberg/smt_verification/solver/solver.cpp +++ b/barretenberg/cpp/src/barretenberg/smt_verification/solver/solver.cpp @@ -132,10 +132,13 @@ std::string Solver::stringify_term(const cvc5::Term& term, bool parenthesis) return res + ")"; } if (term.getKind() == cvc5::Kind::INTERNAL_KIND) { + return ""; + } + if (term.getKind() == cvc5::Kind::SET_INSERT) { return "set_" + std::to_string(this->tables[term]); } - if (term.getKind() == cvc5::Kind::SET_INSERT || term.getKind() == cvc5::Kind::SET_EMPTY) { - return ""; + if (term.getKind() == cvc5::Kind::SET_EMPTY) { + return "{}"; } std::string res; diff --git a/barretenberg/cpp/src/barretenberg/smt_verification/terms/bvterm.test.cpp b/barretenberg/cpp/src/barretenberg/smt_verification/terms/bvterm.test.cpp index ad76add64ad..05d942cdcad 100644 --- a/barretenberg/cpp/src/barretenberg/smt_verification/terms/bvterm.test.cpp +++ b/barretenberg/cpp/src/barretenberg/smt_verification/terms/bvterm.test.cpp @@ -242,11 +242,12 @@ TEST(BVTerm, or) ASSERT_EQ(bvals, xvals); } -TEST(BVTerm, shr) +TEST(BVTerm, div) { StandardCircuitBuilder builder; uint_ct a = witness_ct(&builder, static_cast(fr::random_element())); - uint_ct b = a >> 5; + uint_ct b = witness_ct(&builder, static_cast(fr::random_element())); + uint_ct c = a / b; uint32_t modulus_base = 16; uint32_t bitvector_size = 32; @@ -256,23 +257,25 @@ TEST(BVTerm, shr) bitvector_size); STerm x = BVVar("x", &s); - STerm y = x >> 5; + STerm y = BVVar("y", &s); + STerm z = x / y; x == a.get_value(); + y == b.get_value(); ASSERT_TRUE(s.check()); - std::string xvals = s.getValue(y.term).getBitVectorValue(); - STerm bval = STerm(b.get_value(), &s, TermType::BVTerm); + std::string xvals = s.getValue(z.term).getBitVectorValue(); + STerm bval = STerm(c.get_value(), &s, TermType::BVTerm); std::string bvals = s.getValue(bval.term).getBitVectorValue(); ASSERT_EQ(bvals, xvals); } -TEST(BVTerm, shl) +TEST(BVTerm, shr) { StandardCircuitBuilder builder; uint_ct a = witness_ct(&builder, static_cast(fr::random_element())); - uint_ct b = a << 5; + uint_ct b = a >> 5; uint32_t modulus_base = 16; uint32_t bitvector_size = 32; @@ -282,7 +285,7 @@ TEST(BVTerm, shl) bitvector_size); STerm x = BVVar("x", &s); - STerm y = x << 5; + STerm y = x >> 5; x == a.get_value(); @@ -294,11 +297,11 @@ TEST(BVTerm, shl) ASSERT_EQ(bvals, xvals); } -// This test aims to check for the absence of unintended -// behavior. If an unsupported operator is called, an info message appears in stderr -// and the value is supposed to remain unchanged. -TEST(BVTerm, unsupported_operations) +TEST(BVTerm, shl) { + StandardCircuitBuilder builder; + uint_ct a = witness_ct(&builder, static_cast(fr::random_element())); + uint_ct b = a << 5; uint32_t modulus_base = 16; uint32_t bitvector_size = 32; @@ -308,8 +311,14 @@ TEST(BVTerm, unsupported_operations) bitvector_size); STerm x = BVVar("x", &s); - STerm y = BVVar("y", &s); + STerm y = x << 5; - STerm z = x / y; - ASSERT_EQ(z.term, x.term); + x == a.get_value(); + + ASSERT_TRUE(s.check()); + + std::string xvals = s.getValue(y.term).getBitVectorValue(); + STerm bval = STerm(b.get_value(), &s, TermType::BVTerm); + std::string bvals = s.getValue(bval.term).getBitVectorValue(); + ASSERT_EQ(bvals, xvals); } \ No newline at end of file diff --git a/barretenberg/cpp/src/barretenberg/smt_verification/terms/iterm.test.cpp b/barretenberg/cpp/src/barretenberg/smt_verification/terms/iterm.test.cpp new file mode 100644 index 00000000000..d86081a24bc --- /dev/null +++ b/barretenberg/cpp/src/barretenberg/smt_verification/terms/iterm.test.cpp @@ -0,0 +1,149 @@ +#include + +#include "barretenberg/stdlib/primitives/uint/uint.hpp" +#include "term.hpp" + +#include + +namespace { +auto& engine = bb::numeric::get_debug_randomness(); +} + +using namespace bb; +using witness_ct = stdlib::witness_t; + +using namespace smt_terms; + +TEST(ITerm, addition) +{ + StandardCircuitBuilder builder; + uint64_t a = static_cast(fr::random_element()) % (static_cast(1) << 31); + uint64_t b = static_cast(fr::random_element()) % (static_cast(1) << 31); + uint64_t c = a + b; + + Solver s("30644e72e131a029b85045b68181585d2833e84879b9709143e1f593f0000001", default_solver_config); + + STerm x = IVar("x", &s); + STerm y = IVar("y", &s); + STerm z = x + y; + + z == c; + x == a; + ASSERT_TRUE(s.check()); + + std::string yvals = s.getValue(y.term).getIntegerValue(); + + STerm bval = STerm(b, &s, TermType::ITerm); + std::string bvals = s.getValue(bval.term).getIntegerValue(); + ASSERT_EQ(bvals, yvals); +} + +TEST(ITerm, subtraction) +{ + StandardCircuitBuilder builder; + uint64_t c = static_cast(fr::random_element()) % (static_cast(1) << 31); + uint64_t b = static_cast(fr::random_element()) % (static_cast(1) << 31); + uint64_t a = c + b; + + Solver s("30644e72e131a029b85045b68181585d2833e84879b9709143e1f593f0000001", default_solver_config); + + STerm x = IVar("x", &s); + STerm y = IVar("y", &s); + STerm z = x - y; + + x == a; + z == c; + ASSERT_TRUE(s.check()); + + std::string yvals = s.getValue(y.term).getIntegerValue(); + + STerm bval = STerm(b, &s, TermType::ITerm); + std::string bvals = s.getValue(bval.term).getIntegerValue(); + ASSERT_EQ(bvals, yvals); +} + +TEST(ITerm, mul) +{ + StandardCircuitBuilder builder; + uint64_t a = static_cast(fr::random_element()) % (static_cast(1) << 31); + uint64_t b = static_cast(fr::random_element()) % (static_cast(1) << 31); + uint64_t c = a * b; + + Solver s("30644e72e131a029b85045b68181585d2833e84879b9709143e1f593f0000001", default_solver_config); + + STerm x = IVar("x", &s); + STerm y = IVar("y", &s); + STerm z = x * y; + + x == a; + y == b; + + ASSERT_TRUE(s.check()); + + std::string xvals = s.getValue(z.term).getIntegerValue(); + STerm bval = STerm(c, &s, TermType::ITerm); + std::string bvals = s.getValue(bval.term).getIntegerValue(); + ASSERT_EQ(bvals, xvals); +} + +TEST(ITerm, div) +{ + StandardCircuitBuilder builder; + uint64_t a = static_cast(fr::random_element()) % (static_cast(1) << 31); + uint64_t b = static_cast(fr::random_element()) % (static_cast(1) << 31) + 1; + uint64_t c = a / b; + + Solver s("30644e72e131a029b85045b68181585d2833e84879b9709143e1f593f0000001", default_solver_config); + + STerm x = IVar("x", &s); + STerm y = IVar("y", &s); + STerm z = x / y; + + x == a; + y == b; + + ASSERT_TRUE(s.check()); + + std::string xvals = s.getValue(z.term).getIntegerValue(); + STerm bval = STerm(c, &s, TermType::ITerm); + std::string bvals = s.getValue(bval.term).getIntegerValue(); + ASSERT_EQ(bvals, xvals); +} + +// This test aims to check for the absence of unintended +// behavior. If an unsupported operator is called, an info message appears in stderr +// and the value is supposed to remain unchanged. +TEST(ITerm, unsupported_operations) +{ + Solver s("30644e72e131a029b85045b68181585d2833e84879b9709143e1f593f0000001"); + + STerm x = IVar("x", &s); + STerm y = IVar("y", &s); + + STerm z = x ^ y; + ASSERT_EQ(z.term, x.term); + z = x & y; + ASSERT_EQ(z.term, x.term); + z = x | y; + ASSERT_EQ(z.term, x.term); + z = x >> 10; + ASSERT_EQ(z.term, x.term); + z = x << 10; + ASSERT_EQ(z.term, x.term); + z = x.rotr(10); + ASSERT_EQ(z.term, x.term); + z = x.rotl(10); + ASSERT_EQ(z.term, x.term); + + cvc5::Term before_term = x.term; + x ^= y; + ASSERT_EQ(x.term, before_term); + x &= y; + ASSERT_EQ(x.term, before_term); + x |= y; + ASSERT_EQ(x.term, before_term); + x >>= 10; + ASSERT_EQ(x.term, before_term); + x <<= 10; + ASSERT_EQ(x.term, before_term); +} \ No newline at end of file diff --git a/barretenberg/cpp/src/barretenberg/smt_verification/terms/term.cpp b/barretenberg/cpp/src/barretenberg/smt_verification/terms/term.cpp index 21cdeea09a8..1207ab29142 100644 --- a/barretenberg/cpp/src/barretenberg/smt_verification/terms/term.cpp +++ b/barretenberg/cpp/src/barretenberg/smt_verification/terms/term.cpp @@ -54,6 +54,9 @@ STerm::STerm(const std::string& t, Solver* slv, bool isconst, uint32_t base, Ter slv->assertFormula(ge); slv->assertFormula(lt); break; + case TermType::ITerm: + this->term = slv->term_manager.mkConst(slv->term_manager.getIntegerSort(), t); + break; case TermType::BVTerm: this->term = slv->term_manager.mkConst(slv->bv_sort, t); break; @@ -68,7 +71,11 @@ STerm::STerm(const std::string& t, Solver* slv, bool isconst, uint32_t base, Ter // TODO(alex): CVC5 doesn't provide integer initialization from hex. Yet. strvalue = slv->term_manager.mkFiniteFieldElem(t, slv->ff_sort, base).getFiniteFieldValue(); this->term = slv->term_manager.mkInteger(strvalue); - this->mod(); + this->term = this->mod().term; + break; + case TermType::ITerm: + strvalue = slv->term_manager.mkFiniteFieldElem(t, slv->ff_sort, base).getFiniteFieldValue(); + this->term = slv->term_manager.mkInteger(strvalue); break; case TermType::BVTerm: // it's better to have (-p/2, p/2) representation due to overflows @@ -79,12 +86,15 @@ STerm::STerm(const std::string& t, Solver* slv, bool isconst, uint32_t base, Ter } } -void STerm::mod() +STerm STerm::mod() const { - if (this->type == TermType::FFITerm) { - cvc5::Term modulus = this->solver->term_manager.mkInteger(solver->modulus); - this->term = this->solver->term_manager.mkTerm(this->operations.at(OpType::MOD), { this->term, modulus }); + if (!this->operations.contains(OpType::MOD)) { + info("Taking a remainder is not compatible with ", this->type); + return *this; } + cvc5::Term modulus = this->solver->term_manager.mkInteger(solver->modulus); + cvc5::Term res_s = this->solver->term_manager.mkTerm(this->operations.at(OpType::MOD), { this->term, modulus }); + return { res_s, this->solver, this->type }; } STerm STerm::operator+(const STerm& other) const @@ -144,13 +154,18 @@ STerm STerm::operator/(const STerm& other) const info("Division is not compatible with ", this->type); return *this; } + if (this->type == TermType::FFTerm || this->type == TermType::FFITerm) { + other != bb::fr(0); + STerm res = Var("df8b586e3fa7a1224ec95a886e17a7da_div_" + static_cast(*this) + "_" + + static_cast(other), + this->solver, + this->type); + res* other == *this; + return res; + } other != bb::fr(0); - STerm res = Var("df8b586e3fa7a1224ec95a886e17a7da_div_" + static_cast(*this) + "_" + - static_cast(other), - this->solver, - this->type); - res* other == *this; - return res; + cvc5::Term res_s = this->solver->term_manager.mkTerm(this->operations.at(OpType::DIV), { this->term, other.term }); + return { res_s, this->solver, this->type }; } void STerm::operator/=(const STerm& other) @@ -159,13 +174,17 @@ void STerm::operator/=(const STerm& other) info("Division is not compatible with ", this->type); return; } + if (this->type == TermType::FFTerm || this->type == TermType::FFITerm) { + other != bb::fr(0); + STerm res = Var("df8b586e3fa7a1224ec95a886e17a7da_div_" + static_cast(*this) + "_" + + static_cast(other), + this->solver, + this->type); + res* other == *this; + this->term = res.term; + } other != bb::fr(0); - STerm res = Var("df8b586e3fa7a1224ec95a886e17a7da_div_" + static_cast(*this) + "_" + - static_cast(other), - this->solver, - this->type); - res* other == *this; - this->term = res.term; + this->term = this->solver->term_manager.mkTerm(this->operations.at(OpType::DIV), { this->term, other.term }); } /** @@ -174,15 +193,12 @@ void STerm::operator/=(const STerm& other) */ void STerm::operator==(const STerm& other) const { - STerm tmp1 = *this; - if (tmp1.term.getNumChildren() > 1) { - tmp1.mod(); - } - STerm tmp2 = other; - if (tmp2.term.getNumChildren() > 1) { - tmp2.mod(); - } - cvc5::Term eq = this->solver->term_manager.mkTerm(cvc5::Kind::EQUAL, { tmp1.term, tmp2.term }); + STerm left = *this; + STerm right = other; + left = this->type == TermType::FFITerm && left.term.getNumChildren() > 1 ? left.mod() : left; + right = this->type == TermType::FFITerm && right.term.getNumChildren() > 1 ? right.mod() : right; + + cvc5::Term eq = this->solver->term_manager.mkTerm(cvc5::Kind::EQUAL, { left.term, right.term }); this->solver->assertFormula(eq); } @@ -192,15 +208,12 @@ void STerm::operator==(const STerm& other) const */ void STerm::operator!=(const STerm& other) const { - STerm tmp1 = *this; - if (tmp1.term.getNumChildren() > 1) { - tmp1.mod(); - } - STerm tmp2 = other; - if (tmp2.term.getNumChildren() > 1) { - tmp2.mod(); - } - cvc5::Term eq = this->solver->term_manager.mkTerm(cvc5::Kind::EQUAL, { tmp1.term, tmp2.term }); + STerm left = *this; + STerm right = other; + left = this->type == TermType::FFITerm && left.term.getNumChildren() > 1 ? left.mod() : left; + right = this->type == TermType::FFITerm && right.term.getNumChildren() > 1 ? right.mod() : right; + + cvc5::Term eq = this->solver->term_manager.mkTerm(cvc5::Kind::EQUAL, { left.term, right.term }); eq = this->solver->term_manager.mkTerm(cvc5::Kind::NOT, { eq }); this->solver->assertFormula(eq); } @@ -379,8 +392,11 @@ STerm STerm::rotl(const uint32_t& n) const */ void STerm::in(const cvc5::Term& table) const { + STerm left = *this; + left = this->type == TermType::FFITerm && left.term.getNumChildren() > 1 ? left.mod() : left; + Solver* slv = this->solver; - cvc5::Term inc = slv->term_manager.mkTerm(cvc5::Kind::SET_MEMBER, { this->term, table }); + cvc5::Term inc = slv->term_manager.mkTerm(cvc5::Kind::SET_MEMBER, { left.term, table }); slv->assertFormula(inc); } @@ -441,6 +457,9 @@ std::ostream& operator<<(std::ostream& os, const TermType type) case TermType::BVTerm: os << "BVTerm"; break; + case TermType::ITerm: + os << "ITerm"; + break; }; return os; } @@ -468,6 +487,16 @@ STerm FFIConst(const std::string& val, Solver* slv, uint32_t base) return STerm::Const(val, slv, base, TermType::FFITerm); } +STerm IVar(const std::string& name, Solver* slv) +{ + return STerm::Var(name, slv, TermType::ITerm); +} + +STerm IConst(const std::string& val, Solver* slv, uint32_t base) +{ + return STerm::Const(val, slv, base, TermType::ITerm); +} + STerm BVVar(const std::string& name, Solver* slv) { return STerm::Var(name, slv, TermType::BVTerm); diff --git a/barretenberg/cpp/src/barretenberg/smt_verification/terms/term.hpp b/barretenberg/cpp/src/barretenberg/smt_verification/terms/term.hpp index cef9d44e8a0..35aff409795 100644 --- a/barretenberg/cpp/src/barretenberg/smt_verification/terms/term.hpp +++ b/barretenberg/cpp/src/barretenberg/smt_verification/terms/term.hpp @@ -8,10 +8,11 @@ using namespace smt_solver; * @brief Allows to define three types of symbolic terms * STerm - Symbolic Variables acting like a Finte Field elements * FFITerm - Symbolic Variables acting like integers modulo prime + * ITerm - Symbolic Variables acting like integers * BVTerm - Symbolic Variables acting like bitvectors modulo prime * */ -enum class TermType { FFTerm, FFITerm, BVTerm }; +enum class TermType { FFTerm, FFITerm, BVTerm, ITerm }; std::ostream& operator<<(std::ostream& os, TermType type); enum class OpType : int32_t { ADD, SUB, MUL, DIV, NEG, XOR, AND, OR, GT, GE, LT, LE, MOD, RSH, LSH, ROTR, ROTL }; @@ -42,6 +43,17 @@ const std::unordered_map> typed { OpType::MOD, cvc5::Kind::INTS_MODULUS }, // Just a placeholder that marks it supports division { OpType::DIV, cvc5::Kind::MULT } } }, + { TermType::ITerm, + { { OpType::ADD, cvc5::Kind::ADD }, + { OpType::SUB, cvc5::Kind::SUB }, + { OpType::MUL, cvc5::Kind::MULT }, + { OpType::NEG, cvc5::Kind::NEG }, + { OpType::GT, cvc5::Kind::GT }, + { OpType::GE, cvc5::Kind::GEQ }, + { OpType::LT, cvc5::Kind::LT }, + { OpType::LE, cvc5::Kind::LEQ }, + { OpType::MOD, cvc5::Kind::INTS_MODULUS }, + { OpType::DIV, cvc5::Kind::INTS_DIVISION } } }, { TermType::BVTerm, { @@ -59,7 +71,9 @@ const std::unordered_map> typed { OpType::RSH, cvc5::Kind::BITVECTOR_LSHR }, { OpType::LSH, cvc5::Kind::BITVECTOR_SHL }, { OpType::ROTL, cvc5::Kind::BITVECTOR_ROTATE_LEFT }, - { OpType::ROTR, cvc5::Kind::BITVECTOR_ROTATE_RIGHT } } } + { OpType::ROTR, cvc5::Kind::BITVECTOR_ROTATE_RIGHT }, + { OpType::MOD, cvc5::Kind::BITVECTOR_UREM }, + { OpType::DIV, cvc5::Kind::BITVECTOR_UDIV } } } }; /** @@ -82,7 +96,6 @@ class STerm { , isBitVector(type == TermType::BVTerm) , type(type) , operations(typed_operations.at(type)){}; - void mod(); public: Solver* solver; @@ -122,6 +135,8 @@ class STerm { *this = Const(tmp, s, 16, type); } + STerm mod() const; + STerm& operator=(const STerm& right) = default; STerm& operator=(STerm&& right) = default; @@ -189,8 +204,16 @@ class STerm { */ static void in_table(std::vector& entry, cvc5::Term& table) { + STerm entry0 = entry[0]; + STerm entry1 = entry[1]; + STerm entry2 = entry[2]; + + entry0 = entry0.type == TermType::FFITerm && entry0.term.getNumChildren() > 1 ? entry0.mod() : entry0; + entry1 = entry1.type == TermType::FFITerm && entry1.term.getNumChildren() > 1 ? entry1.mod() : entry1; + entry2 = entry2.type == TermType::FFITerm && entry2.term.getNumChildren() > 1 ? entry2.mod() : entry2; + Solver* slv = entry[0].solver; - cvc5::Term sym_entry = slv->term_manager.mkTuple({ entry[0], entry[1], entry[2] }); + cvc5::Term sym_entry = slv->term_manager.mkTuple({ entry0, entry1, entry2 }); cvc5::Term inc = slv->term_manager.mkTerm(cvc5::Kind::SET_MEMBER, { sym_entry, table }); slv->assertFormula(inc); } @@ -236,6 +259,8 @@ STerm FFVar(const std::string& name, Solver* slv); STerm FFConst(const std::string& val, Solver* slv, uint32_t base = 16); STerm FFIVar(const std::string& name, Solver* slv); STerm FFIConst(const std::string& val, Solver* slv, uint32_t base = 16); +STerm IVar(const std::string& name, Solver* slv); +STerm IConst(const std::string& val, Solver* slv, uint32_t base = 16); STerm BVVar(const std::string& name, Solver* slv); STerm BVConst(const std::string& val, Solver* slv, uint32_t base = 16); diff --git a/barretenberg/cpp/src/barretenberg/smt_verification/util/smt_util.cpp b/barretenberg/cpp/src/barretenberg/smt_verification/util/smt_util.cpp index d3a1c7a2bab..91a59608f5f 100644 --- a/barretenberg/cpp/src/barretenberg/smt_verification/util/smt_util.cpp +++ b/barretenberg/cpp/src/barretenberg/smt_verification/util/smt_util.cpp @@ -42,13 +42,14 @@ void default_model(const std::vector& special, myfile << "{" << mmap1[vname1] << ", " << mmap2[vname2] << "}"; myfile << ", // " << vname1 << ", " << vname2 << std::endl; if (mmap1[vname1] != mmap2[vname2]) { - info("{", mmap1[vname1], ", ", mmap2[vname2], "}", ", // ", vname1, ", ", vname2); + info(RED, "{", mmap1[vname1], ", ", mmap2[vname2], "}", ", // ", vname1, ", ", vname2, RESET); } } else { myfile << "{" << mmap1[vname1] << ", " + mmap2[vname2] << "}"; myfile << ", // " << vname1 << " ," << vname2 << " -> " << c1.real_variable_index[i] << std::endl; if (mmap1[vname1] != mmap2[vname2]) { - info("{", + info(RED, + "{", mmap1[vname1], ", ", mmap2[vname2], @@ -58,7 +59,8 @@ void default_model(const std::vector& special, ", ", vname2, " -> ", - c1.real_variable_index[i]); + c1.real_variable_index[i], + RESET); } } } @@ -172,4 +174,24 @@ std::pair, std::vector> base4(uint32_t el) std::reverse(limbs.begin(), limbs.end()); std::reverse(accumulators.begin(), accumulators.end()); return { limbs, accumulators }; +} + +/** + * @brief Fix the triples from range_lists in the witness + * @details Since we are not using the part of the witness, that + * contains range lists, they are set to 0 by the solver. We need to + * overwrite them to check the witness obtained by the solver. + * + * @param builder + */ +void fix_range_lists(bb::UltraCircuitBuilder& builder) +{ + for (auto list : builder.range_lists) { + uint64_t num_multiples_of_three = (list.first / bb::UltraCircuitBuilder::DEFAULT_PLOOKUP_RANGE_STEP_SIZE); + for (uint64_t i = 0; i <= num_multiples_of_three; i++) { + builder.variables[list.second.variable_indices[i]] = + i * bb::UltraCircuitBuilder::DEFAULT_PLOOKUP_RANGE_STEP_SIZE; + } + builder.variables[list.second.variable_indices[num_multiples_of_three + 1]] = list.first; + } } \ No newline at end of file diff --git a/barretenberg/cpp/src/barretenberg/smt_verification/util/smt_util.hpp b/barretenberg/cpp/src/barretenberg/smt_verification/util/smt_util.hpp index 559b8fff7ee..cf0521b88f0 100644 --- a/barretenberg/cpp/src/barretenberg/smt_verification/util/smt_util.hpp +++ b/barretenberg/cpp/src/barretenberg/smt_verification/util/smt_util.hpp @@ -3,6 +3,9 @@ #include "barretenberg/smt_verification/circuit/circuit_base.hpp" +#define RED "\033[31m" +#define RESET "\033[0m" + void default_model(const std::vector& special, smt_circuit::CircuitBase& c1, smt_circuit::CircuitBase& c2, @@ -12,4 +15,5 @@ void default_model_single(const std::vector& special, const std::string& fname = "witness.out"); bool smt_timer(smt_solver::Solver* s); -std::pair, std::vector> base4(uint32_t el); \ No newline at end of file +std::pair, std::vector> base4(uint32_t el); +void fix_range_lists(bb::UltraCircuitBuilder& builder); \ No newline at end of file