From 5873b8953a798bd2283229cfef06d75eec6daf1f Mon Sep 17 00:00:00 2001 From: Sarkoxed Date: Fri, 1 Sep 2023 15:11:34 +0000 Subject: [PATCH 01/27] smt-verification module migration --- .../cpp/barretenberg/cpp/src/CMakeLists.txt | 5 + .../circuit_builder/circuit_builder_base.hpp | 99 +++++++ .../standard_circuit_builder.cpp | 54 ++++ .../standard_circuit_builder.hpp | 13 + .../smt_verification/CMakeLists.txt | 4 + .../barretenberg/smt_verification/README.md | 190 +++++++++++++ .../smt_verification/circuit/circuit.cpp | 249 ++++++++++++++++++ .../smt_verification/circuit/circuit.hpp | 78 ++++++ .../smt_verification/smt_bigfield.test.cpp | 230 ++++++++++++++++ .../smt_verification/smt_examples.test.cpp | 133 ++++++++++ .../smt_verification/smt_polynomials.test.cpp | 166 ++++++++++++ .../smt_verification/solver/solver.cpp | 37 +++ .../smt_verification/solver/solver.hpp | 55 ++++ .../smt_verification/terms/bool.cpp | 40 +++ .../smt_verification/terms/bool.hpp | 83 ++++++ .../smt_verification/terms/ffterm.cpp | 129 +++++++++ .../smt_verification/terms/ffterm.hpp | 73 +++++ 17 files changed, 1638 insertions(+) create mode 100644 circuits/cpp/barretenberg/cpp/src/barretenberg/smt_verification/CMakeLists.txt create mode 100644 circuits/cpp/barretenberg/cpp/src/barretenberg/smt_verification/README.md create mode 100644 circuits/cpp/barretenberg/cpp/src/barretenberg/smt_verification/circuit/circuit.cpp create mode 100644 circuits/cpp/barretenberg/cpp/src/barretenberg/smt_verification/circuit/circuit.hpp create mode 100644 circuits/cpp/barretenberg/cpp/src/barretenberg/smt_verification/smt_bigfield.test.cpp create mode 100644 circuits/cpp/barretenberg/cpp/src/barretenberg/smt_verification/smt_examples.test.cpp create mode 100644 circuits/cpp/barretenberg/cpp/src/barretenberg/smt_verification/smt_polynomials.test.cpp create mode 100644 circuits/cpp/barretenberg/cpp/src/barretenberg/smt_verification/solver/solver.cpp create mode 100644 circuits/cpp/barretenberg/cpp/src/barretenberg/smt_verification/solver/solver.hpp create mode 100644 circuits/cpp/barretenberg/cpp/src/barretenberg/smt_verification/terms/bool.cpp create mode 100644 circuits/cpp/barretenberg/cpp/src/barretenberg/smt_verification/terms/bool.hpp create mode 100644 circuits/cpp/barretenberg/cpp/src/barretenberg/smt_verification/terms/ffterm.cpp create mode 100644 circuits/cpp/barretenberg/cpp/src/barretenberg/smt_verification/terms/ffterm.hpp diff --git a/circuits/cpp/barretenberg/cpp/src/CMakeLists.txt b/circuits/cpp/barretenberg/cpp/src/CMakeLists.txt index e9ffeb97e39..a96e62d4dcd 100644 --- a/circuits/cpp/barretenberg/cpp/src/CMakeLists.txt +++ b/circuits/cpp/barretenberg/cpp/src/CMakeLists.txt @@ -39,6 +39,9 @@ endif() include_directories(${CMAKE_CURRENT_SOURCE_DIR} ${CMAKE_CURRENT_SOURCE_DIR}/msgpack-c/include) +include_directories(${CMAKE_CURRENT_SOURCE_DIR} $ENV{HOME}/cvc5/tmp-lib/include) + + # I feel this should be limited to ecc, however it's currently used in headers that go across libraries, # and there currently isn't an easy way to inherit the DDISABLE_SHENANIGANS parameter. if(DISABLE_ASM) @@ -68,6 +71,8 @@ add_subdirectory(barretenberg/solidity_helpers) add_subdirectory(barretenberg/wasi) add_subdirectory(barretenberg/grumpkin_srs_gen) add_subdirectory(barretenberg/bb) +add_subdirectory(barretenberg/smt_verification) + if(BENCHMARKS) add_subdirectory(barretenberg/benchmark) diff --git a/circuits/cpp/barretenberg/cpp/src/barretenberg/proof_system/circuit_builder/circuit_builder_base.hpp b/circuits/cpp/barretenberg/cpp/src/barretenberg/proof_system/circuit_builder/circuit_builder_base.hpp index 4e5e29510d6..bdf2a584743 100644 --- a/circuits/cpp/barretenberg/cpp/src/barretenberg/proof_system/circuit_builder/circuit_builder_base.hpp +++ b/circuits/cpp/barretenberg/cpp/src/barretenberg/proof_system/circuit_builder/circuit_builder_base.hpp @@ -3,8 +3,11 @@ #include "barretenberg/ecc/curves/bn254/fr.hpp" #include "barretenberg/proof_system/arithmetization/arithmetization.hpp" #include "barretenberg/proof_system/arithmetization/gate_data.hpp" +#include "barretenberg/serialize/cbind.hpp" #include +#include + namespace proof_system { static constexpr uint32_t DUMMY_TAG = 0; @@ -26,6 +29,8 @@ template class CircuitBuilderBase { std::vector public_inputs; std::vector variables; + std::unordered_map variable_names; + // index of next variable in equivalence class (=REAL_VARIABLE if you're last) std::vector next_var_index; // index of previous variable in equivalence class (=FIRST if you're in a cycle alone) @@ -57,6 +62,7 @@ template class CircuitBuilderBase { : selector_names_(std::move(selector_names)) { variables.reserve(size_hint * 3); + variable_names.reserve(size_hint * 3); next_var_index.reserve(size_hint * 3); prev_var_index.reserve(size_hint * 3); real_variable_index.reserve(size_hint * 3); @@ -187,6 +193,99 @@ template class CircuitBuilderBase { real_variable_tags.emplace_back(DUMMY_TAG); return index; } + + /** + * Assign a name to a variable(equivalence class). Should be one name per equivalence class. + * + * @param index Index of the variable you want to name. + * @param name Name of the variable. + * + */ + virtual void set_variable_name(uint32_t index, const std::string& name) + { + ASSERT(variables.size() > index); + uint32_t first_idx = get_first_variable_in_class(index); + + if (variable_names.contains(first_idx)) { + failure("Attempted to assign a name to a variable that already has a name"); + return; + } + variable_names.insert({ first_idx, name }); + } + + /** + * After assert_equal() merge two class names if present. + * Preserves the first name in class. + * + * @param index Index of the variable you have previously named and used in assert_equal. + * + */ + virtual void update_variable_names(uint32_t index) + { + uint32_t first_idx = get_first_variable_in_class(index); + + uint32_t cur_idx = next_var_index[first_idx]; + while (cur_idx != REAL_VARIABLE && !variable_names.contains(cur_idx)) { + cur_idx = next_var_index[cur_idx]; + } + + if (variable_names.contains(first_idx)) { + if (cur_idx != REAL_VARIABLE) { + variable_names.extract(cur_idx); + } + return; + } + + if (cur_idx != REAL_VARIABLE) { + std::string var_name = variable_names.find(cur_idx)->second; + variable_names.erase(cur_idx); + variable_names.insert({ first_idx, var_name }); + return; + } + failure("No previously assigned names found"); + } + + /** + * After finishing the circuit can be called for automatic merging + * all existing collisions. + * + */ + virtual void finalize_variable_names() + { + std::vector keys; + std::vector firsts; + + for (auto& tup : variable_names) { + keys.push_back(tup.first); + firsts.push_back(get_first_variable_in_class(tup.first)); + } + + for (size_t i = 0; i < keys.size() - 1; i++) { + for (size_t j = i + 1; j < keys.size(); i++) { + uint32_t first_idx_a = firsts[i]; + uint32_t first_idx_b = firsts[j]; + if (first_idx_a == first_idx_b) { + std::string substr1 = variable_names[keys[i]]; + std::string substr2 = variable_names[keys[j]]; + failure("Variables from the same equivalence class have separate names: " + substr2 + ", " + + substr2); + update_variable_names(first_idx_b); + } + } + } + } + + /** + * Export the existing circuit into msgpack compatible buffer. + * + * @return msgpack compatible buffer + */ + virtual msgpack::sbuffer export_circuit() + { + info("not implemented"); + return { 0 }; + }; + /** * Add a public variable to variables * diff --git a/circuits/cpp/barretenberg/cpp/src/barretenberg/proof_system/circuit_builder/standard_circuit_builder.cpp b/circuits/cpp/barretenberg/cpp/src/barretenberg/proof_system/circuit_builder/standard_circuit_builder.cpp index 100e4045706..e436aeeca10 100644 --- a/circuits/cpp/barretenberg/cpp/src/barretenberg/proof_system/circuit_builder/standard_circuit_builder.cpp +++ b/circuits/cpp/barretenberg/cpp/src/barretenberg/proof_system/circuit_builder/standard_circuit_builder.cpp @@ -4,6 +4,9 @@ #include #include +#include "barretenberg/serialize/cbind.hpp" +#include "barretenberg/serialize/msgpack.hpp" + using namespace barretenberg; namespace proof_system { @@ -507,6 +510,57 @@ template bool StandardCircuitBuilder_::check_circuit() } return true; } + +/** + * Export the existing circuit into msgpack compatible buffer. + * + * @return msgpack compatible buffer + */ +template msgpack::sbuffer StandardCircuitBuilder_::export_circuit() +{ + using base = CircuitBuilderBase>; + CircuitSchema cir; + + uint64_t modulus[4] = {FF::Params::modulus_0, FF::Params::modulus_1, FF::Params::modulus_2, FF::Params::modulus_3}; + std::stringstream buf; + buf << std::hex << std::setfill('0') + << std::setw(16) << modulus[3] + << std::setw(16) << modulus[2] + << std::setw(16) << modulus[1] + << std::setw(16) << modulus[0]; + + cir.modulus = buf.str(); + + for (uint32_t i = 0; i < this->get_num_public_inputs(); i++) { + cir.public_inps.push_back(this->real_variable_index[this->public_inputs[i]]); + } + + for (auto& tup : base::variable_names) { + cir.vars_of_interest.insert({ this->real_variable_index[tup.first], tup.second }); + } + + std::string tmp; + for (auto var : this->variables) { + cir.variables.push_back(var); + } + + for (size_t i = 0; i < this->num_gates; i++) { + std::vector tmp_sel = { q_m[i], q_1[i], q_2[i], q_3[i], q_c[i] }; + std::vector tmp_wit = { + this->real_variable_index[w_l[i]], + this->real_variable_index[w_r[i]], + this->real_variable_index[w_o[i]], + }; + cir.selectors.push_back(tmp_sel); + cir.wits.push_back(tmp_wit); + } + + msgpack::sbuffer buffer; + msgpack::pack(buffer, cir); + return buffer; +} + template class StandardCircuitBuilder_; template class StandardCircuitBuilder_; + } // namespace proof_system \ No newline at end of file diff --git a/circuits/cpp/barretenberg/cpp/src/barretenberg/proof_system/circuit_builder/standard_circuit_builder.hpp b/circuits/cpp/barretenberg/cpp/src/barretenberg/proof_system/circuit_builder/standard_circuit_builder.hpp index 2c023001609..5f28544a0be 100644 --- a/circuits/cpp/barretenberg/cpp/src/barretenberg/proof_system/circuit_builder/standard_circuit_builder.hpp +++ b/circuits/cpp/barretenberg/cpp/src/barretenberg/proof_system/circuit_builder/standard_circuit_builder.hpp @@ -113,6 +113,19 @@ template class StandardCircuitBuilder_ : public CircuitBuilderBase size_t get_num_constant_gates() const override { return 0; } bool check_circuit(); + + msgpack::sbuffer export_circuit() override; + + private: + struct CircuitSchema { + std::string modulus; + std::vector public_inps; + std::unordered_map vars_of_interest; + std::vector variables; + std::vector> selectors; + std::vector> wits; + MSGPACK_FIELDS(public_inps, vars_of_interest, variables, selectors, wits); + } circuit_schema; }; extern template class StandardCircuitBuilder_; diff --git a/circuits/cpp/barretenberg/cpp/src/barretenberg/smt_verification/CMakeLists.txt b/circuits/cpp/barretenberg/cpp/src/barretenberg/smt_verification/CMakeLists.txt new file mode 100644 index 00000000000..882abe443a3 --- /dev/null +++ b/circuits/cpp/barretenberg/cpp/src/barretenberg/smt_verification/CMakeLists.txt @@ -0,0 +1,4 @@ +#barretenberg_module(smt_verification common ${CMAKE_SOURCE_DIR}/src/cvc5/tmp-lib/lib/libcvc5.so.1) +barretenberg_module(smt_verification common $ENV{HOME}/cvc5/tmp-lib/lib/libcvc5.so.1) + +barretenberg_module(smt_examples common proof_system stdlib_primitives smt_verification) \ No newline at end of file diff --git a/circuits/cpp/barretenberg/cpp/src/barretenberg/smt_verification/README.md b/circuits/cpp/barretenberg/cpp/src/barretenberg/smt_verification/README.md new file mode 100644 index 00000000000..5871045129c --- /dev/null +++ b/circuits/cpp/barretenberg/cpp/src/barretenberg/smt_verification/README.md @@ -0,0 +1,190 @@ +# Building cvc5 + +As for now it's required to build cvc5 library manually. + + + +- 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 + +# 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 + +- ```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. + +- ```update_variable_names(u32 idx)``` - in case you've called ```assert_equal``` and ```update_real_variable_indices``` somewhere and you know that two or more variables from the equivalence class have separate names, call this method. Idx is the index of one of the variables of this class. The name of the first variable in class will remain. + +- ```finalize_variable_names()``` - in case you don't want to mess with previous method, this one finds all the collisions and removes them. + +- ```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 + +```cpp + msgpack::sbuffer buffer = circuit.export_circuit(); + + std::fstream myfile; + myfile.open("fname.pack", std::ios::out | std::ios::trunc | std::ios::binary); + + myfile.write(buffer.data(), static_cast(buffer.size())); + myfile.close(); +``` + +## 2. Symbolic Circuit initialization and term creation + +1. First you need to import the circuit from the saved file or from the buffer: + + - `smt_circuit::CircuitSchema c_info = smt_circuit::unpack_from_file(str fname);` + + - `smt_circuit::CircuitSchema c_info = smt_circuit::unpack_from_buffer(msgpack::sbuffer buf);` + + +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 bee 10 or 16, I guess. + + `timeout` solver timeout in milliseconds + +3. Initialize the Circuit + + From now and on we will use `smt_terms::FFTerm` and `smt_terms::Bool` types to operate inside the solver. + + `FFTerm` - the symbolic value that simulates finite field elements. + + `Bool` - simulates the boolean values and mostly will be used only to simulate `if` statements if needed. + + - ```smt_circuit::Circuit circuit(CircuitSchema c_info, Solver* s, str tag="")``` + + It will generate all the symbolic values of the circuit wires values, add all the gate constrains, create a map `string->FFTerm`. + 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]`. +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 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. + + Also there is a Bool type: + - `Bool Bool(FFTerm t)` or `Bool Bool(bool b, Solver* s)` + + You can `|, &, ==, !=` these variables and also `batch_or`, `batch_and` them. + To create a constrain you should call `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. +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)`. + Now you have the values of the specified terms, which resulted into `true` result. + +6. Automated verification of a unique witness + + There's also a function `pair unique_witness(CircuitSchema circuit_info, Solver* s, vector inputs, vector outputs)` that will create two separate circuits and constrain their inputs to be eqal and outputs to be not. Then later you can run `s.check()` and `s.model()` if you wish. + +## 3. Simple examples + +```cpp + StandardCircuitBuilder builder = StandardCircuitBuilder(); + + field_t a(witness_t(&builder, fr::random_element())); + field_t b(witness_t(&builder, fr::random_element())); + field_t c = (a + a) / (b + b + b); + + 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()); + + auto buf = builder.export_circuit(); + + smt_circuit::CircuitSchema circuit_info = smt_circuit::unpack_from_buffer(buf); + smt_solver::Solver s(circuit_info.modulus, true, 10); + 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::Const("2", &s, 10); + smt_terms::FFTerm thr = smt_terms::Const("3", &s, 10); + smt_terms::FFTerm cr = smt_terms::Var("cr", &s); + cr = (two * a1) / (thr * b1); + c1 != cr; + + bool res = s.check(); + ASSERT_FALSE(res); +} +``` + +```cpp + StandardCircuitBuilder builder = StandardCircuitBuilder(); + + field_t a(witness_t(&builder, fr::random_element())); + field_t b(witness_t(&builder, fr::random_element())); + field_t c = (a) / (b + b + b); // mistake was here + + 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()); + + auto buf = builder.export_circuit(); + + smt_circuit::CircuitSchema circuit_info = smt_circuit::unpack_from_buffer(buf); + smt_solver::Solver s(circuit_info.modulus, true); + 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::Const("2", &s, 10); + smt_terms::FFTerm thr = smt_terms::Const("3", &s, 10); + smt_terms::FFTerm cr = smt_terms::Var("cr", &s); + cr = (two * a1) / (thr * b1); + c1 != cr; + + bool res = s.check(); + ASSERT_TRUE(res); + + std::unordered_map terms({ { "a", a1 }, { "b", b1 }, { "c", c1 }, { "cr", cr } }); + + std::unordered_map vals = s.model(terms); + + info("a = ", vals["a"]); + info("b = ", vals["b"]); + info("c = ", vals["c"]); + info("c_res = ", vals["cr"]); +} +``` + +More examples can be found in *.test.cpp files diff --git a/circuits/cpp/barretenberg/cpp/src/barretenberg/smt_verification/circuit/circuit.cpp b/circuits/cpp/barretenberg/cpp/src/barretenberg/smt_verification/circuit/circuit.cpp new file mode 100644 index 00000000000..5ee96b77a32 --- /dev/null +++ b/circuits/cpp/barretenberg/cpp/src/barretenberg/smt_verification/circuit/circuit.cpp @@ -0,0 +1,249 @@ +#include "circuit.hpp" +namespace smt_circuit { + +/** + * @brief Construct a new Circuit::Circuit object + * + * @param circuit_info CircuitShema object + * @param solver pointer to the global solver + * @param tag tag of the circuit. Empty by default. + */ +Circuit::Circuit(CircuitSchema& circuit_info, Solver* solver, const std::string& tag) + : public_inps(circuit_info.public_inps) + , vars_of_interest(circuit_info.vars_of_interest) + , wit_idxs(circuit_info.wits) + , solver(solver) + , tag(tag) +{ + if (!this->tag.empty()) { + if (this->tag[0] != '_') { + this->tag = "_" + this->tag; + } + } + + for (auto var : circuit_info.variables) { + std::stringstream buf; // TODO(alex): looks bad. Would be great to create tostring() converter + buf << var; + std::string tmp = buf.str(); + tmp[1] = '0'; // avoiding x in 0x part + variables.push_back(tmp); + } + + for (auto& x : vars_of_interest) { + terms.insert({ x.second, x.first }); + } + + // I hope they are still at these idxs + vars_of_interest.insert({ 0, "zero" }); + vars_of_interest.insert({ 1, "one" }); + terms.insert({ "zero", 0 }); + terms.insert({ "one", 1 }); + + for (auto sel : circuit_info.selectors) { + std::vector tmp_sel; + for (size_t j = 0; j < 5; j++) { + std::stringstream buf; // TODO(alex): #2 + buf << sel[j]; + std::string q_i = buf.str(); + q_i[1] = '0'; // avoiding x in 0x part + tmp_sel.push_back(q_i); + } + selectors.push_back(tmp_sel); + } + + this->init(); + this->add_gates(); +} + +/** + * Creates all the needed symbolic variables and constants + * which are used in circuit. + * + */ +void Circuit::init() +{ + size_t num_vars = variables.size(); + + vars.push_back(Var("zero" + this->tag, this->solver)); + vars.push_back(Var("one" + this->tag, this->solver)); + + for (size_t i = 2; i < num_vars; i++) { + if (vars_of_interest.contains(static_cast(i))) { + std::string name = vars_of_interest[static_cast(i)]; + vars.push_back(Var(name + this->tag, this->solver)); + } else { + vars.push_back(Var("var_" + std::to_string(i) + this->tag, this->solver)); + } + } + + vars[0] == Const("0", this->solver); + vars[1] == Const("1", this->solver); + + for (auto i : public_inps) { + vars[i] == Const(variables[i], this->solver); + } +} + +/** + * @brief Adds all the gate constraints to the solver. + * + */ +void Circuit::add_gates() +{ + for (size_t i = 0; i < get_num_gates(); i++) { + FFTerm q_m = Const(selectors[i][0], this->solver); + FFTerm q_1 = Const(selectors[i][1], this->solver); + FFTerm q_2 = Const(selectors[i][2], this->solver); + FFTerm q_3 = Const(selectors[i][3], this->solver); + FFTerm q_c = Const(selectors[i][4], this->solver); + + uint32_t w_l = wit_idxs[i][0]; + uint32_t w_r = wit_idxs[i][1]; + uint32_t w_o = wit_idxs[i][2]; + + FFTerm eq = vars[0]; + + // mult selector + if (std::string(q_m) != "0") { + eq += q_m * vars[w_l] * vars[w_r]; + } + // w_l selector + if (std::string(q_1) != "0") { + eq += q_1 * vars[w_l]; + } + // w_r selector + if (std::string(q_2) != "0") { + eq += q_2 * vars[w_r]; + } + // w_o selector + if (std::string(q_3) != "0") { + eq += q_3 * vars[w_o]; + } + // w_c selector + if (std::string(q_c) != "0") { + eq += q_c; + } + eq == vars[0]; + } +} + +/** + * @brief Returns a previously named symbolic variable. + * + * @param name + * @return FFTerm + */ +FFTerm Circuit::operator[](const std::string& name) +{ + if (!this->terms.contains(name)) { + throw std::length_error("No such an item " + name + " in vars or it vas not declared as interesting"); + } + uint32_t idx = this->terms[name]; + return this->vars[idx]; +} + +/** + * @brief Get the CircuitSchema object + * @details Initialize the CircuitSchmea from the binary file + * that contains an msgpack compatible buffer. + * + * @param filename + * @return CircuitSchema + */ +CircuitSchema unpack_from_file(const std::string& filename) +{ + std::ifstream fin; + fin.open(filename, std::ios::in | std::ios::binary); + if (!fin.is_open()) { + throw std::invalid_argument("file not found"); + } + if (fin.tellg() == -1) { + throw std::invalid_argument("something went wrong"); + } + + fin.ignore(std::numeric_limits::max()); // ohboy + std::streamsize fsize = fin.gcount(); + fin.clear(); + fin.seekg(0, std::ios_base::beg); + info("File size: ", fsize); + + CircuitSchema cir; + char* encoded_data = (char*)aligned_alloc(64, static_cast(fsize)); + fin.read(encoded_data, fsize); + msgpack::unpack((const char*)encoded_data, static_cast(fsize)).get().convert(cir); + return cir; +} + +/** + * @brief Get the CircuitSchema object + * @details Initialize the CircuitSchmea from the msgpack compatible buffer. + * + * @param buf + * @return CircuitSchema + */ +CircuitSchema unpack_from_buffer(const msgpack::sbuffer& buf) +{ + CircuitSchema cir; + msgpack::unpack(buf.data(), buf.size()).get().convert(cir); + return cir; +} + +/** + * @brief Check your circuit for witness uniqness + * + * @details Creates two Circuit objects that represent the same + * circuit, however you can choose which variables should be (not) equal in both cases, + * and also the variables that should (not) be equal at the same time. + * + * @param circuit_info + * @param s pointer to the global solver + * @param equal all the variables that should be equal in both circuits + * @param nequal all the variables that should be different in both circuits + * @param eqall all the variables that should not be equal at the same time + * @param neqall all the variables that should not be different at the same time + * @return std::pair + */ +std::pair unique_witness(CircuitSchema& circuit_info, + Solver* s, + const std::vector& equal, + const std::vector& nequal, + const std::vector& eqall, + const std::vector& neqall) +{ + Circuit c1(circuit_info, s, "circuit1"); + Circuit c2(circuit_info, s, "circuit2"); + + for (const auto& term : equal) { + c1[term] == c2[term]; + } + for (const auto& term : nequal) { + c1[term] != c2[term]; + } + + std::vector eqs; + for (const auto& term : eqall) { + Bool tmp = Bool(c1[term]) == Bool(c2[term]); + eqs.push_back(tmp); + } + + if (eqs.size() > 1) { + batch_or(eqs).assert_term(); + } else if (eqs.size() == 1) { + eqs[0].assert_term(); + } + + std::vector neqs; + for (const auto& term : neqall) { + Bool tmp = Bool(c1[term]) != Bool(c2[term]); + neqs.push_back(tmp); + } + + if (neqs.size() > 1) { + batch_or(neqs).assert_term(); + } else if (neqs.size() == 1) { + neqs[0].assert_term(); + } + return { c1, c2 }; +} + +}; // namespace smt_circuit \ No newline at end of file diff --git a/circuits/cpp/barretenberg/cpp/src/barretenberg/smt_verification/circuit/circuit.hpp b/circuits/cpp/barretenberg/cpp/src/barretenberg/smt_verification/circuit/circuit.hpp new file mode 100644 index 00000000000..cce759ed5a6 --- /dev/null +++ b/circuits/cpp/barretenberg/cpp/src/barretenberg/smt_verification/circuit/circuit.hpp @@ -0,0 +1,78 @@ +#pragma once +#include "barretenberg/serialize/cbind.hpp" +#include "barretenberg/serialize/msgpack.hpp" +#include +#include +#include +#include +#include + +#include "barretenberg/smt_verification/terms/bool.hpp" +#include "barretenberg/smt_verification/terms/ffterm.hpp" + +namespace smt_circuit { +using namespace smt_solver; +using namespace smt_terms; + +const std::string p = "21888242871839275222246405745257275088548364400416034343698204186575808495617"; + +struct CircuitSchema { + std::string modulus; + std::vector public_inps; + std::unordered_map vars_of_interest; + std::vector variables; + std::vector> selectors; + std::vector> wits; + MSGPACK_FIELDS(public_inps, vars_of_interest, variables, selectors, wits); +}; + +/** + * @brief Symbolic Circuit class. + * + * @details Contains all the information about the circuit: gates, variables, + * symbolic variables, specified names and global solver. + * + * @todo TODO(alex): think on the partial value assertion inside the circuit. + * @todo TODO(alex): class SymCircuit? + */ +class Circuit { + private: + void init(); + void add_gates(); + + public: + std::vector variables; // circuit witness + std::vector public_inps; // public inputs from the circuit + std::unordered_map vars_of_interest; // names of the variables + std::unordered_map terms; // inverse map of the previous memeber + std::vector> selectors; // selectors from the circuit + std::vector> wit_idxs; // values used in gates from the circuit + std::vector vars; // all the symbolic variables in the circuit + + Solver* solver; // pointer to the solver + std::string tag; // tag of the symbolic circuit. + // If not empty, will be added to the names + // of symbolic variables to prevent collisions. + + explicit Circuit(CircuitSchema& circuit_info, Solver* solver, const std::string& tag = ""); + + FFTerm operator[](const std::string& name); + inline uint32_t get_num_gates() const { return static_cast(selectors.size()); }; + inline uint32_t get_num_vars() const { return static_cast(vars.size()); }; +}; + +CircuitSchema unpack_from_buffer(const msgpack::sbuffer& buf); +CircuitSchema unpack_from_file(const std::string& fname); + +std::pair unique_witness(CircuitSchema& circuit_info, + Solver* s, + const std::vector& equal, + const std::vector& nequal, + const std::vector& eqall = {}, + const std::vector& neqall = {}); + +// TODO(alex): Do we need the function that will do recheck based on the current model to consequently find all the +// solutions? +// void get_all_solutions(std::unordered_map, std::unordered_map) + +}; // namespace smt_circuit \ No newline at end of file diff --git a/circuits/cpp/barretenberg/cpp/src/barretenberg/smt_verification/smt_bigfield.test.cpp b/circuits/cpp/barretenberg/cpp/src/barretenberg/smt_verification/smt_bigfield.test.cpp new file mode 100644 index 00000000000..4f344b831c0 --- /dev/null +++ b/circuits/cpp/barretenberg/cpp/src/barretenberg/smt_verification/smt_bigfield.test.cpp @@ -0,0 +1,230 @@ +#include "barretenberg/numeric/random/engine.hpp" + +#include "barretenberg/ecc/curves/bn254/fq.hpp" +#include "barretenberg/ecc/curves/bn254/fr.hpp" + +#include "barretenberg/stdlib/primitives/bigfield/bigfield.hpp" +#include "barretenberg/stdlib/primitives/bool/bool.hpp" +#include "barretenberg/stdlib/primitives/byte_array/byte_array.hpp" +#include "barretenberg/stdlib/primitives/field/field.hpp" + +#include "barretenberg/plonk/proof_system/constants.hpp" +#include "barretenberg/plonk/proof_system/prover/prover.hpp" +#include "barretenberg/plonk/proof_system/verifier/verifier.hpp" + +#include "barretenberg/stdlib/primitives/circuit_builders/circuit_builders.hpp" +#include "barretenberg/stdlib/primitives/curves/bn254.hpp" + +#include "barretenberg/polynomials/polynomial_arithmetic.hpp" +#include +#include +#include + +#include +#include +#include + +#include "barretenberg/smt_verification/circuit/circuit.hpp" + +using namespace smt_circuit; +using namespace barretenberg; +using namespace proof_system::plonk; + +using field_ct = proof_system::plonk::stdlib::field_t; +using witness_t = proof_system::plonk::stdlib::witness_t; +using pub_witness_t = proof_system::plonk::stdlib::public_witness_t; + +using bn254 = stdlib::bn254; + +using fr_ct = bn254::ScalarField; +using fq_ct = bn254::BaseField; +using public_witness_ct = bn254::public_witness_ct; +using witness_ct = bn254::witness_ct; + +msgpack::sbuffer create_circuit(bool pub_ab, bool ab) +{ + StandardCircuitBuilder builder = StandardCircuitBuilder(); + fq inputs[2]{ fq::random_element(), fq::random_element() }; + fq_ct a, b; + if (pub_ab) { + a = fq_ct(public_witness_ct(&builder, fr(uint256_t(inputs[0]).slice(0, fq_ct::NUM_LIMB_BITS * 2))), + public_witness_ct( + &builder, fr(uint256_t(inputs[0]).slice(fq_ct::NUM_LIMB_BITS * 2, fq_ct::NUM_LIMB_BITS * 4)))); + b = fq_ct(public_witness_ct(&builder, fr(uint256_t(inputs[1]).slice(0, fq_ct::NUM_LIMB_BITS * 2))), + public_witness_ct( + &builder, fr(uint256_t(inputs[1]).slice(fq_ct::NUM_LIMB_BITS * 2, fq_ct::NUM_LIMB_BITS * 4)))); + } else { + a = fq_ct( + witness_ct(&builder, fr(uint256_t(inputs[0]).slice(0, fq_ct::NUM_LIMB_BITS * 2))), + witness_ct(&builder, fr(uint256_t(inputs[0]).slice(fq_ct::NUM_LIMB_BITS * 2, fq_ct::NUM_LIMB_BITS * 4)))); + b = fq_ct( + witness_ct(&builder, fr(uint256_t(inputs[1]).slice(0, fq_ct::NUM_LIMB_BITS * 2))), + witness_ct(&builder, fr(uint256_t(inputs[1]).slice(fq_ct::NUM_LIMB_BITS * 2, fq_ct::NUM_LIMB_BITS * 4)))); + } + builder.set_variable_name(a.binary_basis_limbs[0].element.witness_index, "a_limb_0"); + builder.set_variable_name(a.binary_basis_limbs[1].element.witness_index, "a_limb_1"); + builder.set_variable_name(a.binary_basis_limbs[2].element.witness_index, "a_limb_2"); + builder.set_variable_name(a.binary_basis_limbs[3].element.witness_index, "a_limb_3"); + + if (ab) { + builder.set_variable_name(b.binary_basis_limbs[0].element.witness_index, "b_limb_0"); + builder.set_variable_name(b.binary_basis_limbs[1].element.witness_index, "b_limb_1"); + builder.set_variable_name(b.binary_basis_limbs[2].element.witness_index, "b_limb_2"); + builder.set_variable_name(b.binary_basis_limbs[3].element.witness_index, "b_limb_3"); + } + + fq_ct c; + if (ab) { + c = a * b; + } else { + c = a * a; + } + builder.set_variable_name(c.binary_basis_limbs[0].element.witness_index, "c_limb_0"); + builder.set_variable_name(c.binary_basis_limbs[1].element.witness_index, "c_limb_1"); + builder.set_variable_name(c.binary_basis_limbs[2].element.witness_index, "c_limb_2"); + builder.set_variable_name(c.binary_basis_limbs[3].element.witness_index, "c_limb_3"); + return builder.export_circuit(); +} + +const std::string q = "21888242871839275222246405745257275088696311157297823662689037894645226208583"; + +std::vector correct_result(Circuit& c, Solver* s) +{ + FFTerm a_limb0 = c["a_limb_0"]; + FFTerm a_limb1 = c["a_limb_1"]; + FFTerm a_limb2 = c["a_limb_2"]; + FFTerm a_limb3 = c["a_limb_3"]; + + FFTerm b_limb0 = c["b_limb_0"]; + FFTerm b_limb1 = c["b_limb_1"]; + FFTerm b_limb2 = c["b_limb_2"]; + FFTerm b_limb3 = c["b_limb_3"]; + + FFTerm c_limb0 = c["c_limb_0"]; + FFTerm c_limb1 = c["c_limb_1"]; + FFTerm c_limb2 = c["c_limb_2"]; + FFTerm c_limb3 = c["c_limb_3"]; + + FFTerm two68 = Const("100000000000000000", s); + FFTerm two136 = two68 * two68; + FFTerm two204 = two136 * two68; + + FFTerm a = a_limb0 + two68 * a_limb1 + two136 * a_limb2 + two204 * a_limb3; + FFTerm b = b_limb0 + two68 * b_limb1 + two136 * b_limb2 + two204 * b_limb3; + FFTerm cr = c_limb0 + two68 * c_limb1 + two136 * c_limb2 + two204 * c_limb3; + FFTerm n = Var("n", s); + FFTerm q_ = Const(q, s, 10); // Const(q_hex, s) + a* b != cr + n* q_; + return { cr, n }; +} + +void model_variables(Circuit& c, Solver* s, std::vector& evaluation) +{ + std::unordered_map terms; + for (size_t i = 0; i < 4; i++) { + terms.insert({ "a_limb_" + std::to_string(i), c["a_limb_" + std::to_string(i)] }); + terms.insert({ "b_limb_" + std::to_string(i), c["b_limb_" + std::to_string(i)] }); + terms.insert({ "c_limb_" + std::to_string(i), c["c_limb_" + std::to_string(i)] }); + } + terms.insert({ "cr", evaluation[0] }); + terms.insert({ "n", evaluation[1] }); + + auto values = s->model(terms); + + for (size_t i = 0; i < 4; i++) { + std::string tmp = "a_limb_" + std::to_string(i); + info(tmp, " = ", values[tmp]); + } + for (size_t i = 0; i < 4; i++) { + std::string tmp = "b_limb_" + std::to_string(i); + info(tmp, " = ", values[tmp]); + } + for (size_t i = 0; i < 4; i++) { + std::string tmp = "c_limb_" + std::to_string(i); + info(tmp, " = ", values[tmp]); + } + info("cr = ", values["cr"]); + info("n = ", values["n"]); +} + +void model_variables1(Circuit& c1, Circuit& c2, Solver* s) +{ + std::unordered_map terms; + for (size_t i = 0; i < 4; i++) { + terms.insert({ "a_limb_" + std::to_string(i), c1["a_limb_" + std::to_string(i)] }); + terms.insert({ "c1_limb_" + std::to_string(i), c1["c_limb_" + std::to_string(i)] }); + terms.insert({ "c2_limb_" + std::to_string(i), c2["c_limb_" + std::to_string(i)] }); + } + auto values = s->model(terms); + + for (size_t i = 0; i < 4; i++) { + std::string tmp = "a_limb_" + std::to_string(i); + info(tmp, " = ", values[tmp]); + } + + for (size_t i = 0; i < 4; i++) { + std::string tmp = "c1_limb_" + std::to_string(i); + info(tmp, " = ", values[tmp]); + } + + for (size_t i = 0; i < 4; i++) { + std::string tmp = "c2_limb_" + std::to_string(i); + info(tmp, " = ", values[tmp]); + } +} + +TEST(bigfield, multiplication_equal) +{ + bool public_a_b = true; + bool a_neq_b = true; + auto buf = create_circuit(public_a_b, a_neq_b); + + CircuitSchema circuit_info = unpack_from_buffer(buf); + Solver s(circuit_info.modulus, true); + Circuit circuit(circuit_info, &s); + std::vector ev = correct_result(circuit, &s); + + auto start = std::chrono::high_resolution_clock::now(); + bool res = s.check(); + auto stop = std::chrono::high_resolution_clock::now(); + auto duration = std::chrono::duration_cast(stop - start); + + info(); + info("Gates: ", circuit.get_num_gates()); + info("Result: ", s.getResult()); + info("Time elapsed: ", static_cast(duration.count()) / 1e6, " sec"); + + if (res) { + model_variables(circuit, &s, ev); + } +} + +TEST(bigfield, unique_square) +{ + auto buf = create_circuit(true, false); + + CircuitSchema circuit_info = unpack_from_buffer(buf); + + Solver s(circuit_info.modulus, true, 16); //, 1000); + + std::pair cs = unique_witness(circuit_info, + &s, + { "a_limb_0", "a_limb_1", "a_limb_2", "a_limb_3" }, + { "c_limb_0", "c_limb_1", "c_limb_2", "c_limb_3" }); + + auto start = std::chrono::high_resolution_clock::now(); + bool res = s.check(); + auto stop = std::chrono::high_resolution_clock::now(); + auto duration = std::chrono::duration_cast(stop - start); + + ASSERT_FALSE(res); + + info(); + info("Gates: ", cs.first.get_num_gates()); + info("Result: ", s.getResult()); + info("Time elapsed: ", static_cast(duration.count()) / 1e6, " sec"); + + if (res) { + model_variables1(cs.first, cs.second, &s); + } +} \ No newline at end of file diff --git a/circuits/cpp/barretenberg/cpp/src/barretenberg/smt_verification/smt_examples.test.cpp b/circuits/cpp/barretenberg/cpp/src/barretenberg/smt_verification/smt_examples.test.cpp new file mode 100644 index 00000000000..7bb05b8e5db --- /dev/null +++ b/circuits/cpp/barretenberg/cpp/src/barretenberg/smt_verification/smt_examples.test.cpp @@ -0,0 +1,133 @@ +#include "barretenberg/crypto/generators/generator_data.hpp" +#include "barretenberg/crypto/pedersen_commitment/pedersen.hpp" +#include "barretenberg/proof_system/circuit_builder/standard_circuit_builder.hpp" +#include +#include +#include +#include + +#include "barretenberg/stdlib/primitives/field/field.hpp" + +#include "barretenberg/smt_verification/circuit/circuit.hpp" + +using namespace barretenberg; +using namespace proof_system; + +namespace { +auto& engine = numeric::random::get_debug_engine(); +} + +using field_t = proof_system::plonk::stdlib::field_t; +using witness_t = proof_system::plonk::stdlib::witness_t; +using pub_witness_t = proof_system::plonk::stdlib::public_witness_t; + +TEST(circuit_verification, multiplication_true) +{ + StandardCircuitBuilder builder = StandardCircuitBuilder(); + + field_t a(witness_t(&builder, fr::random_element())); + field_t b(witness_t(&builder, fr::random_element())); + field_t c = (a + a) / (b + b + b); + + 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()); + + auto buf = builder.export_circuit(); + + smt_circuit::CircuitSchema circuit_info = smt_circuit::unpack_from_buffer(buf); + smt_solver::Solver s(circuit_info.modulus, true); + 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::Const("2", &s, 10); + smt_terms::FFTerm thr = smt_terms::Const("3", &s, 10); + smt_terms::FFTerm cr = smt_terms::Var("cr", &s); + cr = (two * a1) / (thr * b1); + c1 != cr; + + bool res = s.check(); + ASSERT_FALSE(res); +} + +TEST(circuit_verification, multiplication_false) +{ + StandardCircuitBuilder builder = StandardCircuitBuilder(); + + field_t a(witness_t(&builder, fr::random_element())); + field_t b(witness_t(&builder, fr::random_element())); + field_t c = (a) / (b + b + b); // mistake was here + + 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()); + + auto buf = builder.export_circuit(); + + smt_circuit::CircuitSchema circuit_info = smt_circuit::unpack_from_buffer(buf); + smt_solver::Solver s(circuit_info.modulus, true); + 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::Const("2", &s, 10); + smt_terms::FFTerm thr = smt_terms::Const("3", &s, 10); + smt_terms::FFTerm cr = smt_terms::Var("cr", &s); + cr = (two * a1) / (thr * b1); + c1 != cr; + + bool res = s.check(); + ASSERT_TRUE(res); + + std::unordered_map terms({ { "a", a1 }, { "b", b1 }, { "c", c1 }, { "cr", cr } }); + + std::unordered_map vals = s.model(terms); + + info("a = ", vals["a"]); + info("b = ", vals["b"]); + info("c = ", vals["c"]); + info("c_res = ", vals["cr"]); +} + +TEST(circuit_verifiaction, unique_witness) +// two roots of a quadratic eq 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); + + std::pair cirs = + smt_circuit::unique_witness(circuit_info, &s, { "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"]); +} \ No newline at end of file diff --git a/circuits/cpp/barretenberg/cpp/src/barretenberg/smt_verification/smt_polynomials.test.cpp b/circuits/cpp/barretenberg/cpp/src/barretenberg/smt_verification/smt_polynomials.test.cpp new file mode 100644 index 00000000000..495998c83e0 --- /dev/null +++ b/circuits/cpp/barretenberg/cpp/src/barretenberg/smt_verification/smt_polynomials.test.cpp @@ -0,0 +1,166 @@ +#include "barretenberg/crypto/generators/generator_data.hpp" +#include "barretenberg/crypto/pedersen_commitment/pedersen.hpp" +#include "barretenberg/proof_system/circuit_builder/standard_circuit_builder.hpp" + +#include +#include +#include +#include +#include + +#include "barretenberg/stdlib/primitives/field/field.hpp" + +#include "barretenberg/serialize/cbind.hpp" +#include "barretenberg/smt_verification/circuit/circuit.hpp" + +using namespace barretenberg; +using namespace proof_system; +using namespace smt_circuit; + +using field_ct = proof_system::plonk::stdlib::field_t; +using witness_t = proof_system::plonk::stdlib::witness_t; +using pub_witness_t = proof_system::plonk::stdlib::public_witness_t; + +namespace { +auto& engine = numeric::random::get_debug_engine(); +} + +msgpack::sbuffer create_circuit(size_t n, bool pub_coeffs) +{ + StandardCircuitBuilder builder = StandardCircuitBuilder(); + std::vector coeffs; + std::vector idxs; + for (size_t i = 0; i < n; i++) { + fr tmp_coeff = fr::random_element(); + uint32_t idx; + if (pub_coeffs) { + idx = builder.add_public_variable(tmp_coeff); + } else { + idx = builder.add_variable(tmp_coeff); + } + idxs.push_back(idx); + coeffs.push_back(tmp_coeff); + builder.set_variable_name(idx, "coeff_" + std::to_string(i)); + } + + fr z(10); + uint32_t z_idx = builder.add_variable(z); + builder.set_variable_name(z_idx, "point"); + fr res = fr::zero(); + uint32_t res_idx = builder.zero_idx; // i think assert_equal was needed for zero initialization + builder.assert_equal(res_idx, 0); + + for (size_t i = 0; i < n; i++) { + res = res * z; + uint32_t mul_idx = builder.add_variable(res); + // builder.set_variable_name(mul_idx, "mul_" + std::to_string(i)); + builder.create_mul_gate({ res_idx, z_idx, mul_idx, fr::one(), fr::neg_one(), fr::zero() }); + + res = res + coeffs[i]; + uint32_t add_idx = builder.add_variable(res); + builder.create_add_gate({ + mul_idx, + idxs[i], + add_idx, + fr::one(), + fr::one(), + fr::neg_one(), + fr::zero(), + }); + + res_idx = add_idx; + } + builder.set_variable_name(res_idx, "result"); + + info("evaluation at point ", z, ": ", res); + info("gates: ", builder.num_gates); + info("variables: ", builder.get_num_variables()); + info("public inputs: ", builder.get_num_public_inputs()); + + return builder.export_circuit(); +} + +FFTerm polynomial_evaluation(Circuit& c, size_t n, bool is_correct = true) +{ + std::vector coeffs(n); + for (size_t i = 0; i < n; i++) { + coeffs[i] = c["coeff_" + std::to_string(i)]; + } + + FFTerm point = c["point"]; + FFTerm result = c["result"]; + + FFTerm ev = is_correct ? c["zero"] : c["one"]; + for (size_t i = 0; i < n; i++) { + ev = ev * point + coeffs[i]; + } + + result != ev; + return ev; +} + +void model_variables(Circuit& c, Solver* s, FFTerm& evaluation) +{ + std::unordered_map terms; + terms.insert({ "point", c["point"] }); + terms.insert({ "result", c["result"] }); + terms.insert({ "evaluation", evaluation }); + + auto values = s->model(terms); + + info("point = ", values["point"]); + info("circuit_result = ", values["result"]); + info("function_evaluation = ", values["evaluation"]); +} + +TEST(polynomial_evaluation, correct) +{ + size_t n = 30; + auto buf = create_circuit(n, true); + + CircuitSchema circuit_info = unpack_from_buffer(buf); + + Solver s(circuit_info.modulus, true); + Circuit circuit(circuit_info, &s); + FFTerm ev = polynomial_evaluation(circuit, n, true); + + auto start = std::chrono::high_resolution_clock::now(); + bool res = s.check(); + auto stop = std::chrono::high_resolution_clock::now(); + auto duration = std::chrono::duration_cast(stop - start); + + ASSERT_FALSE(res); + info(); + info("Gates: ", circuit.get_num_gates()); + info("Result: ", s.getResult()); + info("Time elapsed: ", static_cast(duration.count()) / 1e6, " sec"); +} + +TEST(polynomial_evaluation, incorrect) +{ + size_t n = 30; + auto buf = create_circuit(n, true); + + CircuitSchema circuit_info = unpack_from_buffer(buf); + + Solver s(circuit_info.modulus, true); + Circuit circuit(circuit_info, &s); + FFTerm ev = polynomial_evaluation(circuit, n, false); + + auto start = std::chrono::high_resolution_clock::now(); + bool res = s.check(); + auto stop = std::chrono::high_resolution_clock::now(); + auto duration = std::chrono::duration_cast(stop - start); + + ASSERT_TRUE(res); + info(); + info("Gates: ", circuit.get_num_gates()); + info("Result: ", s.getResult()); + info("Time elapsed: ", static_cast(duration.count()) / 1e6, " sec"); + + if (res) { + model_variables(circuit, &s, ev); + } +} + +// TODO(alex) try with arbitrary coefficients \ No newline at end of file diff --git a/circuits/cpp/barretenberg/cpp/src/barretenberg/smt_verification/solver/solver.cpp b/circuits/cpp/barretenberg/cpp/src/barretenberg/smt_verification/solver/solver.cpp new file mode 100644 index 00000000000..7ae827fc3a3 --- /dev/null +++ b/circuits/cpp/barretenberg/cpp/src/barretenberg/smt_verification/solver/solver.cpp @@ -0,0 +1,37 @@ +#include "solver.hpp" +#include + +namespace smt_solver { + +/** + * Check if the symbolic model is solvable. + * + * @return true if the model is solvable. + * */ +bool Solver::check() +{ + cvc5::Result result = this->s.checkSat(); + this->res = result.isSat(); + this->checked = true; + return this->res; +} + +/** + * If the system is solvable, extract the values for the given symbolic variables. + * + * @param terms A map containing pairs (name, symbolic term). + * @return A map containing pairs (name, value). + * */ +std::unordered_map Solver::model(std::unordered_map& terms) const +{ + if (!this->res) { + throw std::length_error("There's no solution"); + } + std::unordered_map resulting_model; + for (auto& term : terms) { + std::string str_val = this->s.getValue(term.second).getFiniteFieldValue(); + resulting_model.insert({ term.first, str_val }); + } + return resulting_model; +} +}; // namespace smt_solver diff --git a/circuits/cpp/barretenberg/cpp/src/barretenberg/smt_verification/solver/solver.hpp b/circuits/cpp/barretenberg/cpp/src/barretenberg/smt_verification/solver/solver.hpp new file mode 100644 index 00000000000..d9cb5039723 --- /dev/null +++ b/circuits/cpp/barretenberg/cpp/src/barretenberg/smt_verification/solver/solver.hpp @@ -0,0 +1,55 @@ +#pragma once +#include +#include + +namespace smt_solver { + +/** + * @brief Class for the solver. + * + * @details Solver class that can be used to create + * a solver, finite field terms and the circuit. + * Check the satisfability of a system and get it's model. + * + * @todo TODO(alex): more cvc5 options inside the constructor. + * @todo TODO(alex) perhaps add the << operator to make it easier to read the constraints. + */ +class Solver { + private: + bool res = false; + bool checked = false; + + public: + cvc5::Solver s; + cvc5::Sort fp; + + explicit Solver(const std::string& modulus, bool produce_model = false, uint32_t base = 16, uint32_t timeout = 0) + { + fp = s.mkFiniteFieldSort(modulus, base); + if (produce_model) { + s.setOption("produce-models", "true"); + } + if (timeout > 0) { + s.setOption("tlimit-per", std::to_string(timeout)); + } + } + + Solver(const Solver& other) = delete; + Solver(Solver&& other) = delete; + Solver& operator=(const Solver& other) = delete; + Solver& operator=(Solver&& other) = delete; + + bool check(); + + [[nodiscard]] std::string getResult() const + { + if (!checked) { + return "No result, yet"; + } + return res ? "SAT" : "UNSAT"; + } + + std::unordered_map model(std::unordered_map& terms) const; + ~Solver() = default; +}; +}; // namespace smt_solver \ No newline at end of file diff --git a/circuits/cpp/barretenberg/cpp/src/barretenberg/smt_verification/terms/bool.cpp b/circuits/cpp/barretenberg/cpp/src/barretenberg/smt_verification/terms/bool.cpp new file mode 100644 index 00000000000..e7e85d8da86 --- /dev/null +++ b/circuits/cpp/barretenberg/cpp/src/barretenberg/smt_verification/terms/bool.cpp @@ -0,0 +1,40 @@ +#include "bool.hpp" + +namespace smt_terms { + +Bool Bool::operator|(const Bool& other) const +{ + cvc5::Term res = solver->mkTerm(cvc5::Kind::OR, { this->term, other.term }); + ; + return { res, this->solver }; +} + +void Bool::operator|=(const Bool& other) +{ + this->term = this->solver->mkTerm(cvc5::Kind::OR, { this->term, other.term }); +} + +Bool Bool::operator&(const Bool& other) const +{ + cvc5::Term res = solver->mkTerm(cvc5::Kind::AND, { this->term, other.term }); + return { res, this->solver }; +} + +void Bool::operator&=(const Bool& other) +{ + this->term = this->solver->mkTerm(cvc5::Kind::AND, { this->term, other.term }); +} + +Bool Bool::operator==(const Bool& other) const +{ + cvc5::Term res = solver->mkTerm(cvc5::Kind::EQUAL, { this->term, other.term }); + return { res, this->solver }; +} + +Bool Bool::operator!=(const Bool& other) const +{ + cvc5::Term res = solver->mkTerm(cvc5::Kind::EQUAL, { this->term, other.term }); + res = solver->mkTerm(cvc5::Kind::EQUAL, { res, this->solver->mkBoolean(false) }); + return { res, this->solver }; +} +}; // namespace smt_terms \ No newline at end of file diff --git a/circuits/cpp/barretenberg/cpp/src/barretenberg/smt_verification/terms/bool.hpp b/circuits/cpp/barretenberg/cpp/src/barretenberg/smt_verification/terms/bool.hpp new file mode 100644 index 00000000000..83d9be913ce --- /dev/null +++ b/circuits/cpp/barretenberg/cpp/src/barretenberg/smt_verification/terms/bool.hpp @@ -0,0 +1,83 @@ +#pragma once +#include "ffterm.hpp" + +namespace smt_terms { +using namespace smt_solver; + +/** + * @brief Bool element class. + * + * @details Can be used to create non trivial constraints. + * Supports basic boolean arithmetic: &, |. + * + */ +class Bool { + public: + cvc5::Solver* solver; + cvc5::Term term; + bool asserted = false; + + explicit Bool(const cvc5::Term& t, Solver& slv) + : solver(&slv.s) + , term(t){}; + explicit Bool(const FFTerm& t) + : solver(&t.solver->s) + , term(t.term){}; + + explicit Bool(bool t, Solver& slv) + : solver(&slv.s) + { + term = solver->mkBoolean(t); + } + Bool(const cvc5::Term& term, cvc5::Solver* s) + : solver(s) + , term(term){}; + Bool(const Bool& other) = default; + Bool(Bool&& other) = default; + + Bool& operator=(const Bool& right) = default; + Bool& operator=(Bool&& right) = default; + + void assert_term() + { + if (!asserted) { + solver->assertFormula(term); + asserted = true; + } + } + + Bool operator|(const Bool& other) const; + void operator|=(const Bool& other); + Bool operator|(const bool& other) const; + void operator|=(const bool& other) const; + + Bool operator&(const Bool& other) const; + void operator&=(const Bool& other); + Bool operator&(const bool& other) const; + void operator&=(const bool& other); + + Bool operator==(const Bool& other) const; + Bool operator!=(const Bool& other) const; + + operator std::string() const { return term.toString(); }; + operator cvc5::Term() const { return term; }; + + friend Bool batch_or(const std::vector& children) + { + cvc5::Solver* s = children[0].solver; + std::vector terms(children.begin(), children.end()); + cvc5::Term res = s->mkTerm(cvc5::Kind::OR, terms); + return { res, s }; + } + + friend Bool batch_and(const std::vector& children) + { + cvc5::Solver* s = children[0].solver; + std::vector terms(children.begin(), children.end()); + cvc5::Term res = s->mkTerm(cvc5::Kind::AND, terms); + return { res, s }; + } + + ~Bool() = default; +}; +}; // namespace smt_terms \ No newline at end of file diff --git a/circuits/cpp/barretenberg/cpp/src/barretenberg/smt_verification/terms/ffterm.cpp b/circuits/cpp/barretenberg/cpp/src/barretenberg/smt_verification/terms/ffterm.cpp new file mode 100644 index 00000000000..08c17af1d1e --- /dev/null +++ b/circuits/cpp/barretenberg/cpp/src/barretenberg/smt_verification/terms/ffterm.cpp @@ -0,0 +1,129 @@ +#include "ffterm.hpp" + +namespace smt_terms { + +/** + * Create a finite field symbolic variable. + * + * @param name Name of the variable. Should be unique per variable. + * @param slv Pointer to the global solver. + * @return Finite field symbolic variable. + * */ +FFTerm Var(const std::string& name, Solver* slv) +{ + return FFTerm(name, slv); +}; + +/** + * Create a finite field numeric member. + * + * @param val String representation of the value. + * @param slv Pointer to the global solver. + * @param base Base of the string representation. 16 by default. + * @return Finite field constant. + * */ +FFTerm Const(const std::string& val, Solver* slv, uint32_t base) +{ + return FFTerm(val, slv, true, base); +}; + +FFTerm::FFTerm(const std::string& t, Solver* slv, bool isconst, uint32_t base) + : solver(slv) + , isconst(isconst) +{ + if (!isconst) { + this->term = slv->s.mkConst(slv->fp, t); + } else { + this->term = slv->s.mkFiniteFieldElem(t, slv->fp, base); + } +} + +FFTerm FFTerm::operator+(const FFTerm& other) const +{ + cvc5::Term res = this->solver->s.mkTerm(cvc5::Kind::FINITE_FIELD_ADD, { this->term, other.term }); + ; + return { res, this->solver }; +} + +void FFTerm::operator+=(const FFTerm& other) +{ + this->term = this->solver->s.mkTerm(cvc5::Kind::FINITE_FIELD_ADD, { this->term, other.term }); +} + +FFTerm FFTerm::operator-(const FFTerm& other) const +{ + cvc5::Term res = this->solver->s.mkTerm(cvc5::Kind::FINITE_FIELD_NEG, { other.term }); + res = solver->s.mkTerm(cvc5::Kind::FINITE_FIELD_ADD, { this->term, res }); + return { res, this->solver }; +} + +void FFTerm::operator-=(const FFTerm& other) +{ + cvc5::Term tmp_term = this->solver->s.mkTerm(cvc5::Kind::FINITE_FIELD_NEG, { other.term }); + this->term = this->solver->s.mkTerm(cvc5::Kind::FINITE_FIELD_ADD, { this->term, tmp_term }); +} + +FFTerm FFTerm::operator*(const FFTerm& other) const +{ + cvc5::Term res = solver->s.mkTerm(cvc5::Kind::FINITE_FIELD_MULT, { this->term, other.term }); + return { res, this->solver }; +} + +void FFTerm::operator*=(const FFTerm& other) +{ + this->term = this->solver->s.mkTerm(cvc5::Kind::FINITE_FIELD_MULT, { this->term, other.term }); +} + +/** + * @brief Division operation + * + * @details Returns a result of the division by + * creating a new symbolic variable and adding a new constraint + * to the solver. + * + * @param other + * @return FFTerm + */ +FFTerm FFTerm::operator/(const FFTerm& other) const +{ + cvc5::Term res = this->solver->s.mkConst(this->solver->fp, + "fe0f65a52067384116dc1137d798e0ca00a7ed46950e4eab7db51e08481535f2_div_" + + std::string(*this) + "_" + std::string(other)); + cvc5::Term div = this->solver->s.mkTerm(cvc5::Kind::FINITE_FIELD_MULT, { res, other.term }); + cvc5::Term eq = this->solver->s.mkTerm(cvc5::Kind::EQUAL, { this->term, div }); + this->solver->s.assertFormula(eq); + return { res, this->solver }; +} + +void FFTerm::operator/=(const FFTerm& other) +{ + cvc5::Term res = this->solver->s.mkConst(this->solver->fp, + "fe0f65a52067384116dc1137d798e0ca00a7ed46950e4eab7db51e08481535f2_div_" + + std::string(*this) + "__" + std::string(other)); + cvc5::Term div = this->solver->s.mkTerm(cvc5::Kind::FINITE_FIELD_MULT, { res, other.term }); + cvc5::Term eq = this->solver->s.mkTerm(cvc5::Kind::EQUAL, { this->term, div }); + this->solver->s.assertFormula(eq); + this->term = res; +} + +/** + * Create an equality constraint between two finite field elements. + * + */ +void FFTerm::operator==(const FFTerm& other) const +{ + cvc5::Term eq = this->solver->s.mkTerm(cvc5::Kind::EQUAL, { this->term, other.term }); + this->solver->s.assertFormula(eq); +} + +/** + * Create an inequality constraint between two finite field elements. + * + */ +void FFTerm::operator!=(const FFTerm& other) const +{ + cvc5::Term eq = this->solver->s.mkTerm(cvc5::Kind::EQUAL, { this->term, other.term }); + eq = this->solver->s.mkTerm(cvc5::Kind::EQUAL, { eq, this->solver->s.mkBoolean(false) }); + this->solver->s.assertFormula(eq); +} +} // namespace smt_terms \ No newline at end of file diff --git a/circuits/cpp/barretenberg/cpp/src/barretenberg/smt_verification/terms/ffterm.hpp b/circuits/cpp/barretenberg/cpp/src/barretenberg/smt_verification/terms/ffterm.hpp new file mode 100644 index 00000000000..14add1d7c55 --- /dev/null +++ b/circuits/cpp/barretenberg/cpp/src/barretenberg/smt_verification/terms/ffterm.hpp @@ -0,0 +1,73 @@ +#pragma once +#include "barretenberg/smt_verification/solver/solver.hpp" + +namespace smt_terms { +using namespace smt_solver; + +/** + * @brief Finite Field element class. + * + * @details Can be a finite field symbolic variable or a constant. + * Both of them support basic arithmetic operations: +, -, *, /. + * Check the satisfability of a system and get it's model. + * + */ +class FFTerm { + public: + Solver* solver; + cvc5::Term term; + bool isconst; + + FFTerm() + : solver(nullptr) + , term(cvc5::Term()) + , isconst(false){}; + explicit FFTerm(const std::string& t, Solver* slv, bool isconst = false, uint32_t base = 16); + FFTerm(cvc5::Term& term, Solver* s) + : solver(s) + , term(term){}; + FFTerm(const FFTerm& other) = default; + FFTerm(FFTerm&& other) = default; + + FFTerm& operator=(const FFTerm& right) = default; + FFTerm& operator=(FFTerm&& right) = default; + + FFTerm operator+(const FFTerm& other) const; + void operator+=(const FFTerm& other); + FFTerm operator-(const FFTerm& other) const; + void operator-=(const FFTerm& other); + FFTerm operator*(const FFTerm& other) const; + void operator*=(const FFTerm& other); + FFTerm operator/(const FFTerm& other) const; + void operator/=(const FFTerm& other); + + void operator==(const FFTerm& other) const; + void operator!=(const FFTerm& other) const; + + operator std::string() const { return isconst ? term.getFiniteFieldValue() : term.toString(); }; + operator cvc5::Term() const { return term; }; + + ~FFTerm() = default; + friend std::ostream& operator<<(std::ostream& out, const FFTerm& k) { return out << k.term; } + + friend FFTerm batch_add(const std::vector& children) + { + Solver* slv = children[0].solver; + std::vector terms(children.begin(), children.end()); + cvc5::Term res = slv->s.mkTerm(cvc5::Kind::FINITE_FIELD_ADD, terms); + return { res, slv }; + } + + friend FFTerm batch_mul(const std::vector& children) + { + Solver* slv = children[0].solver; + std::vector terms(children.begin(), children.end()); + cvc5::Term res = slv->s.mkTerm(cvc5::Kind::FINITE_FIELD_MULT, terms); + return { res, slv }; + } +}; + +FFTerm Var(const std::string& name, Solver* slv); +FFTerm Const(const std::string& val, Solver* slv, uint32_t base = 16); + +} // namespace smt_terms \ No newline at end of file From 24151698b32904ceef888160175b42945169a7df Mon Sep 17 00:00:00 2001 From: Sarkoxed Date: Fri, 1 Sep 2023 15:27:33 +0000 Subject: [PATCH 02/27] SMT-verfication preset added --- .../cpp/barretenberg/cpp/CMakePresets.json | 20 +++++++++++++++++++ .../cpp/barretenberg/cpp/src/CMakeLists.txt | 7 ++++--- 2 files changed, 24 insertions(+), 3 deletions(-) diff --git a/circuits/cpp/barretenberg/cpp/CMakePresets.json b/circuits/cpp/barretenberg/cpp/CMakePresets.json index 6c709155e37..4ff677f6b78 100644 --- a/circuits/cpp/barretenberg/cpp/CMakePresets.json +++ b/circuits/cpp/barretenberg/cpp/CMakePresets.json @@ -88,6 +88,16 @@ "FUZZING": "ON" } }, + { + "name": "smt-verification", + "displayName": "Build with smt verificaiton", + "description": "Build default preset but with smt library included", + "inherits": "default", + "binaryDir": "build-smt", + "cacheVariables": { + "SMT": "ON" + } + }, { "name": "coverage", "displayName": "Build with coverage", @@ -190,6 +200,11 @@ "inherits": "default", "configurePreset": "fuzzing" }, + { + "name": "smt-verification", + "inherits": "default", + "configurePreset": "smt-verification" + }, { "name": "coverage", "inherits": "default", @@ -258,6 +273,11 @@ "inherits": "default", "configurePreset": "fuzzing" }, + { + "name": "smt-verification", + "inherits": "default", + "configurePreset": "smt-verification" + }, { "name": "coverage", "inherits": "default", diff --git a/circuits/cpp/barretenberg/cpp/src/CMakeLists.txt b/circuits/cpp/barretenberg/cpp/src/CMakeLists.txt index a96e62d4dcd..e391b81c1a8 100644 --- a/circuits/cpp/barretenberg/cpp/src/CMakeLists.txt +++ b/circuits/cpp/barretenberg/cpp/src/CMakeLists.txt @@ -39,8 +39,6 @@ endif() include_directories(${CMAKE_CURRENT_SOURCE_DIR} ${CMAKE_CURRENT_SOURCE_DIR}/msgpack-c/include) -include_directories(${CMAKE_CURRENT_SOURCE_DIR} $ENV{HOME}/cvc5/tmp-lib/include) - # I feel this should be limited to ecc, however it's currently used in headers that go across libraries, # and there currently isn't an easy way to inherit the DDISABLE_SHENANIGANS parameter. @@ -71,9 +69,12 @@ add_subdirectory(barretenberg/solidity_helpers) add_subdirectory(barretenberg/wasi) add_subdirectory(barretenberg/grumpkin_srs_gen) add_subdirectory(barretenberg/bb) -add_subdirectory(barretenberg/smt_verification) +if(SMT) + include_directories(${CMAKE_CURRENT_SOURCE_DIR} $ENV{HOME}/cvc5/tmp-lib/include) + add_subdirectory(barretenberg/smt_verification) + if(BENCHMARKS) add_subdirectory(barretenberg/benchmark) endif() From aae5b34b2a4b90ce46a573bdee10f1eefcfbe866 Mon Sep 17 00:00:00 2001 From: Sarkoxed Date: Fri, 1 Sep 2023 15:29:13 +0000 Subject: [PATCH 03/27] endif --- circuits/cpp/barretenberg/cpp/src/CMakeLists.txt | 1 + 1 file changed, 1 insertion(+) diff --git a/circuits/cpp/barretenberg/cpp/src/CMakeLists.txt b/circuits/cpp/barretenberg/cpp/src/CMakeLists.txt index e391b81c1a8..797035bcfe1 100644 --- a/circuits/cpp/barretenberg/cpp/src/CMakeLists.txt +++ b/circuits/cpp/barretenberg/cpp/src/CMakeLists.txt @@ -74,6 +74,7 @@ add_subdirectory(barretenberg/bb) if(SMT) include_directories(${CMAKE_CURRENT_SOURCE_DIR} $ENV{HOME}/cvc5/tmp-lib/include) add_subdirectory(barretenberg/smt_verification) +endif() if(BENCHMARKS) add_subdirectory(barretenberg/benchmark) From 0d177fa915d326d552c73e6f49f53b8e6988acfe Mon Sep 17 00:00:00 2001 From: Sarkoxed Date: Fri, 1 Sep 2023 16:25:25 +0000 Subject: [PATCH 04/27] msgpack issue fix + reorder includes --- .../circuit_builder/standard_circuit_builder.hpp | 2 +- .../src/barretenberg/smt_verification/circuit/circuit.hpp | 5 +++-- 2 files changed, 4 insertions(+), 3 deletions(-) diff --git a/circuits/cpp/barretenberg/cpp/src/barretenberg/proof_system/circuit_builder/standard_circuit_builder.hpp b/circuits/cpp/barretenberg/cpp/src/barretenberg/proof_system/circuit_builder/standard_circuit_builder.hpp index 5f28544a0be..ba0e598e768 100644 --- a/circuits/cpp/barretenberg/cpp/src/barretenberg/proof_system/circuit_builder/standard_circuit_builder.hpp +++ b/circuits/cpp/barretenberg/cpp/src/barretenberg/proof_system/circuit_builder/standard_circuit_builder.hpp @@ -124,7 +124,7 @@ template class StandardCircuitBuilder_ : public CircuitBuilderBase std::vector variables; std::vector> selectors; std::vector> wits; - MSGPACK_FIELDS(public_inps, vars_of_interest, variables, selectors, wits); + MSGPACK_FIELDS(modulus, public_inps, vars_of_interest, variables, selectors, wits); } circuit_schema; }; diff --git a/circuits/cpp/barretenberg/cpp/src/barretenberg/smt_verification/circuit/circuit.hpp b/circuits/cpp/barretenberg/cpp/src/barretenberg/smt_verification/circuit/circuit.hpp index cce759ed5a6..e70ed2cd0c5 100644 --- a/circuits/cpp/barretenberg/cpp/src/barretenberg/smt_verification/circuit/circuit.hpp +++ b/circuits/cpp/barretenberg/cpp/src/barretenberg/smt_verification/circuit/circuit.hpp @@ -1,12 +1,13 @@ #pragma once -#include "barretenberg/serialize/cbind.hpp" -#include "barretenberg/serialize/msgpack.hpp" #include #include #include #include #include +#include "barretenberg/serialize/cbind.hpp" +#include "barretenberg/serialize/msgpack.hpp" + #include "barretenberg/smt_verification/terms/bool.hpp" #include "barretenberg/smt_verification/terms/ffterm.hpp" From c07584bbda276453cb2c4c25ee1d72fdec04889c Mon Sep 17 00:00:00 2001 From: Sarkoxed Date: Tue, 5 Sep 2023 23:41:27 +0000 Subject: [PATCH 05/27] default -> clang16 --- circuits/cpp/barretenberg/cpp/CMakePresets.json | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/circuits/cpp/barretenberg/cpp/CMakePresets.json b/circuits/cpp/barretenberg/cpp/CMakePresets.json index 4ff677f6b78..cd785ecf5ed 100644 --- a/circuits/cpp/barretenberg/cpp/CMakePresets.json +++ b/circuits/cpp/barretenberg/cpp/CMakePresets.json @@ -92,7 +92,7 @@ "name": "smt-verification", "displayName": "Build with smt verificaiton", "description": "Build default preset but with smt library included", - "inherits": "default", + "inherits": "clang16", "binaryDir": "build-smt", "cacheVariables": { "SMT": "ON" @@ -202,7 +202,7 @@ }, { "name": "smt-verification", - "inherits": "default", + "inherits": "clang16", "configurePreset": "smt-verification" }, { @@ -275,7 +275,7 @@ }, { "name": "smt-verification", - "inherits": "default", + "inherits": "clang16", "configurePreset": "smt-verification" }, { From d0502aaa88f161e2f0dc78bb8b9707a864e7e1ef Mon Sep 17 00:00:00 2001 From: Sarkoxed Date: Wed, 6 Sep 2023 10:33:49 +0000 Subject: [PATCH 06/27] MSGpack fix + todos --- .../src/barretenberg/smt_verification/circuit/circuit.hpp | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/circuits/cpp/barretenberg/cpp/src/barretenberg/smt_verification/circuit/circuit.hpp b/circuits/cpp/barretenberg/cpp/src/barretenberg/smt_verification/circuit/circuit.hpp index e70ed2cd0c5..5aafb332c6e 100644 --- a/circuits/cpp/barretenberg/cpp/src/barretenberg/smt_verification/circuit/circuit.hpp +++ b/circuits/cpp/barretenberg/cpp/src/barretenberg/smt_verification/circuit/circuit.hpp @@ -9,14 +9,13 @@ #include "barretenberg/serialize/msgpack.hpp" #include "barretenberg/smt_verification/terms/bool.hpp" +#include "barretenberg/smt_verification/terms/ffiterm.hpp" #include "barretenberg/smt_verification/terms/ffterm.hpp" namespace smt_circuit { using namespace smt_solver; using namespace smt_terms; -const std::string p = "21888242871839275222246405745257275088548364400416034343698204186575808495617"; - struct CircuitSchema { std::string modulus; std::vector public_inps; @@ -24,7 +23,7 @@ struct CircuitSchema { std::vector variables; std::vector> selectors; std::vector> wits; - MSGPACK_FIELDS(public_inps, vars_of_interest, variables, selectors, wits); + MSGPACK_FIELDS(modulus, public_inps, vars_of_interest, variables, selectors, wits); }; /** @@ -35,6 +34,7 @@ struct CircuitSchema { * * @todo TODO(alex): think on the partial value assertion inside the circuit. * @todo TODO(alex): class SymCircuit? + * @todo TODO(alex): FFTerm operator[](uint32_t) */ class Circuit { private: @@ -76,4 +76,4 @@ std::pair unique_witness(CircuitSchema& circuit_info, // solutions? // void get_all_solutions(std::unordered_map, std::unordered_map) -}; // namespace smt_circuit \ No newline at end of file +}; // namespace smt_circuit From 095754b94e777639f49420d673599050626747a8 Mon Sep 17 00:00:00 2001 From: Sarkoxed Date: Wed, 6 Sep 2023 10:34:34 +0000 Subject: [PATCH 07/27] Clean up --- .../cpp/src/barretenberg/smt_verification/smt_examples.test.cpp | 2 -- .../src/barretenberg/smt_verification/smt_polynomials.test.cpp | 1 + 2 files changed, 1 insertion(+), 2 deletions(-) diff --git a/circuits/cpp/barretenberg/cpp/src/barretenberg/smt_verification/smt_examples.test.cpp b/circuits/cpp/barretenberg/cpp/src/barretenberg/smt_verification/smt_examples.test.cpp index 7bb05b8e5db..47ca1c3ee44 100644 --- a/circuits/cpp/barretenberg/cpp/src/barretenberg/smt_verification/smt_examples.test.cpp +++ b/circuits/cpp/barretenberg/cpp/src/barretenberg/smt_verification/smt_examples.test.cpp @@ -1,5 +1,3 @@ -#include "barretenberg/crypto/generators/generator_data.hpp" -#include "barretenberg/crypto/pedersen_commitment/pedersen.hpp" #include "barretenberg/proof_system/circuit_builder/standard_circuit_builder.hpp" #include #include diff --git a/circuits/cpp/barretenberg/cpp/src/barretenberg/smt_verification/smt_polynomials.test.cpp b/circuits/cpp/barretenberg/cpp/src/barretenberg/smt_verification/smt_polynomials.test.cpp index 495998c83e0..e7887a5793a 100644 --- a/circuits/cpp/barretenberg/cpp/src/barretenberg/smt_verification/smt_polynomials.test.cpp +++ b/circuits/cpp/barretenberg/cpp/src/barretenberg/smt_verification/smt_polynomials.test.cpp @@ -21,6 +21,7 @@ using field_ct = proof_system::plonk::stdlib::field_t; using witness_t = proof_system::plonk::stdlib::witness_t; using pub_witness_t = proof_system::plonk::stdlib::public_witness_t; +// TODO(alex): z1 = z2, s1=s2, but coefficients are not public namespace { auto& engine = numeric::random::get_debug_engine(); } From a54de132523ba9f2d378af9003a4a02040385794 Mon Sep 17 00:00:00 2001 From: Sarkoxed Date: Wed, 6 Sep 2023 10:35:16 +0000 Subject: [PATCH 08/27] Modulus inside the solver --- .../src/barretenberg/smt_verification/solver/solver.hpp | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/circuits/cpp/barretenberg/cpp/src/barretenberg/smt_verification/solver/solver.hpp b/circuits/cpp/barretenberg/cpp/src/barretenberg/smt_verification/solver/solver.hpp index d9cb5039723..f8d4cf6a6d2 100644 --- a/circuits/cpp/barretenberg/cpp/src/barretenberg/smt_verification/solver/solver.hpp +++ b/circuits/cpp/barretenberg/cpp/src/barretenberg/smt_verification/solver/solver.hpp @@ -4,11 +4,11 @@ namespace smt_solver { -/** +/** * @brief Class for the solver. * * @details Solver class that can be used to create - * a solver, finite field terms and the circuit. + * a solver, finite field terms and the circuit. * Check the satisfability of a system and get it's model. * * @todo TODO(alex): more cvc5 options inside the constructor. @@ -22,8 +22,10 @@ class Solver { public: cvc5::Solver s; cvc5::Sort fp; + std::string modulus; explicit Solver(const std::string& modulus, bool produce_model = false, uint32_t base = 16, uint32_t timeout = 0) + : modulus(modulus) { fp = s.mkFiniteFieldSort(modulus, base); if (produce_model) { @@ -52,4 +54,4 @@ class Solver { std::unordered_map model(std::unordered_map& terms) const; ~Solver() = default; }; -}; // namespace smt_solver \ No newline at end of file +}; // namespace smt_solver From 43e9b9eef8182c85dfa583c9f21633ed8ec7dd33 Mon Sep 17 00:00:00 2001 From: Sarkoxed Date: Wed, 6 Sep 2023 10:40:36 +0000 Subject: [PATCH 09/27] No isconst member + fixed the string repr --- .../src/barretenberg/smt_verification/terms/ffterm.cpp | 9 ++++----- .../src/barretenberg/smt_verification/terms/ffterm.hpp | 9 ++++----- 2 files changed, 8 insertions(+), 10 deletions(-) diff --git a/circuits/cpp/barretenberg/cpp/src/barretenberg/smt_verification/terms/ffterm.cpp b/circuits/cpp/barretenberg/cpp/src/barretenberg/smt_verification/terms/ffterm.cpp index 08c17af1d1e..ee3e322a8dc 100644 --- a/circuits/cpp/barretenberg/cpp/src/barretenberg/smt_verification/terms/ffterm.cpp +++ b/circuits/cpp/barretenberg/cpp/src/barretenberg/smt_verification/terms/ffterm.cpp @@ -29,7 +29,6 @@ FFTerm Const(const std::string& val, Solver* slv, uint32_t base) FFTerm::FFTerm(const std::string& t, Solver* slv, bool isconst, uint32_t base) : solver(slv) - , isconst(isconst) { if (!isconst) { this->term = slv->s.mkConst(slv->fp, t); @@ -76,13 +75,13 @@ void FFTerm::operator*=(const FFTerm& other) /** * @brief Division operation - * + * * @details Returns a result of the division by - * creating a new symbolic variable and adding a new constraint + * creating a new symbolic variable and adding a new constraint * to the solver. * - * @param other - * @return FFTerm + * @param other + * @return FFTerm */ FFTerm FFTerm::operator/(const FFTerm& other) const { diff --git a/circuits/cpp/barretenberg/cpp/src/barretenberg/smt_verification/terms/ffterm.hpp b/circuits/cpp/barretenberg/cpp/src/barretenberg/smt_verification/terms/ffterm.hpp index 14add1d7c55..fb9d33cd4e5 100644 --- a/circuits/cpp/barretenberg/cpp/src/barretenberg/smt_verification/terms/ffterm.hpp +++ b/circuits/cpp/barretenberg/cpp/src/barretenberg/smt_verification/terms/ffterm.hpp @@ -4,7 +4,7 @@ namespace smt_terms { using namespace smt_solver; -/** +/** * @brief Finite Field element class. * * @details Can be a finite field symbolic variable or a constant. @@ -16,12 +16,11 @@ class FFTerm { public: Solver* solver; cvc5::Term term; - bool isconst; FFTerm() : solver(nullptr) - , term(cvc5::Term()) - , isconst(false){}; + , term(cvc5::Term()){}; + explicit FFTerm(const std::string& t, Solver* slv, bool isconst = false, uint32_t base = 16); FFTerm(cvc5::Term& term, Solver* s) : solver(s) @@ -44,7 +43,7 @@ class FFTerm { void operator==(const FFTerm& other) const; void operator!=(const FFTerm& other) const; - operator std::string() const { return isconst ? term.getFiniteFieldValue() : term.toString(); }; + operator std::string() const { return term.isFiniteFieldValue() ? term.getFiniteFieldValue() : term.toString(); }; operator cvc5::Term() const { return term; }; ~FFTerm() = default; From f480356cd0e0d47bbab351a52622673dd2b46d7c Mon Sep 17 00:00:00 2001 From: Sarkoxed Date: Wed, 6 Sep 2023 10:41:19 +0000 Subject: [PATCH 10/27] New Integer Modulo number backend --- .../smt_verification/terms/bool.hpp | 9 +- .../smt_verification/terms/ffiterm.cpp | 141 ++++++++++++++++++ .../smt_verification/terms/ffiterm.hpp | 86 +++++++++++ 3 files changed, 234 insertions(+), 2 deletions(-) create mode 100644 circuits/cpp/barretenberg/cpp/src/barretenberg/smt_verification/terms/ffiterm.cpp create mode 100644 circuits/cpp/barretenberg/cpp/src/barretenberg/smt_verification/terms/ffiterm.hpp diff --git a/circuits/cpp/barretenberg/cpp/src/barretenberg/smt_verification/terms/bool.hpp b/circuits/cpp/barretenberg/cpp/src/barretenberg/smt_verification/terms/bool.hpp index 83d9be913ce..ff67f22be4d 100644 --- a/circuits/cpp/barretenberg/cpp/src/barretenberg/smt_verification/terms/bool.hpp +++ b/circuits/cpp/barretenberg/cpp/src/barretenberg/smt_verification/terms/bool.hpp @@ -1,4 +1,5 @@ #pragma once +#include "ffiterm.hpp" #include "ffterm.hpp" namespace smt_terms { @@ -6,7 +7,7 @@ using namespace smt_solver; /** * @brief Bool element class. - * + * * @details Can be used to create non trivial constraints. * Supports basic boolean arithmetic: &, |. * @@ -24,6 +25,10 @@ class Bool { : solver(&t.solver->s) , term(t.term){}; + explicit Bool(const FFITerm& t) + : solver(&t.solver->s) + , term(t.term){}; + explicit Bool(bool t, Solver& slv) : solver(&slv.s) { @@ -80,4 +85,4 @@ class Bool { ~Bool() = default; }; -}; // namespace smt_terms \ No newline at end of file +}; // namespace smt_terms diff --git a/circuits/cpp/barretenberg/cpp/src/barretenberg/smt_verification/terms/ffiterm.cpp b/circuits/cpp/barretenberg/cpp/src/barretenberg/smt_verification/terms/ffiterm.cpp new file mode 100644 index 00000000000..b9dc022e6a7 --- /dev/null +++ b/circuits/cpp/barretenberg/cpp/src/barretenberg/smt_verification/terms/ffiterm.cpp @@ -0,0 +1,141 @@ +#include "ffiterm.hpp" + +namespace smt_terms { + +/** + * Create an integer mod symbolic variable. + * + * @param name Name of the variable. Should be unique per variable. + * @param slv Pointer to the global solver. + * @return Finite field symbolic variable. + * */ +FFITerm IVar(const std::string& name, Solver* slv) +{ + return FFITerm(name, slv); +}; + +/** + * Create an integer mod numeric member. + * + * @param val String representation of the value. + * @param slv Pointer to the global solver. + * @param base Base of the string representation. 16 by default. + * @return Finite field constant. + * */ +FFITerm IConst(const std::string& val, Solver* slv) //, uint32_t base) +{ + return FFITerm(val, slv, true); //, base); +}; + +FFITerm::FFITerm(const std::string& t, Solver* slv, bool isconst) //, uint32_t base) + : solver(slv) + , modulus(slv->s.mkInteger(slv->modulus)) +{ + if (!isconst) { + this->term = slv->s.mkConst(slv->s.getIntegerSort(), t); + cvc5::Term ge = slv->s.mkTerm(cvc5::Kind::GEQ, { this->term, slv->s.mkInteger(0) }); + cvc5::Term lt = slv->s.mkTerm(cvc5::Kind::LT, { this->term, this->modulus }); + slv->s.assertFormula(ge); + slv->s.assertFormula(lt); + } else { + this->term = slv->s.mkInteger(t); //, base); + } +} + +FFITerm FFITerm::operator+(const FFITerm& other) const +{ + cvc5::Term res = this->solver->s.mkTerm(cvc5::Kind::ADD, { this->term, other.term }); + res = this->solver->s.mkTerm(cvc5::Kind::INTS_MODULUS, { res, this->modulus }); + return { res, this->solver }; +} + +void FFITerm::operator+=(const FFITerm& other) +{ + this->term = this->solver->s.mkTerm(cvc5::Kind::ADD, { this->term, other.term }); + this->term = + this->solver->s.mkTerm(cvc5::Kind::INTS_MODULUS, { this->term, this->modulus }); // TODO(alex): is it faster? +} + +FFITerm FFITerm::operator-(const FFITerm& other) const +{ + cvc5::Term res = this->solver->s.mkTerm(cvc5::Kind::SUB, { this->term, other.term }); + res = this->solver->s.mkTerm(cvc5::Kind::INTS_MODULUS, { res, this->modulus }); + return { res, this->solver }; +} + +void FFITerm::operator-=(const FFITerm& other) +{ + this->term = this->solver->s.mkTerm(cvc5::Kind::SUB, { this->term, other.term }); + this->term = + this->solver->s.mkTerm(cvc5::Kind::INTS_MODULUS, { this->term, this->modulus }); // TODO(alex): is it faster? +} + +FFITerm FFITerm::operator*(const FFITerm& other) const +{ + cvc5::Term res = solver->s.mkTerm(cvc5::Kind::MULT, { this->term, other.term }); + res = this->solver->s.mkTerm(cvc5::Kind::INTS_MODULUS, { res, this->modulus }); + return { res, this->solver }; +} + +void FFITerm::operator*=(const FFITerm& other) +{ + this->term = this->solver->s.mkTerm(cvc5::Kind::MULT, { this->term, other.term }); + this->term = + this->solver->s.mkTerm(cvc5::Kind::INTS_MODULUS, { this->term, this->modulus }); // TODO(alex): is it faster? +} + +/** + * @brief Division operation + * + * @details Returns a result of the division by + * creating a new symbolic variable and adding a new constraint + * to the solver. + * + * @param other + * @return FFITerm + */ +FFITerm FFITerm::operator/(const FFITerm& other) const +{ + cvc5::Term res = this->solver->s.mkConst(this->solver->s.getIntegerSort(), + "fe0f65a52067384116dc1137d798e0ca00a7ed46950e4eab7db51e08481535f2_div_" + + std::string(*this) + "_" + std::string(other)); + cvc5::Term div = this->solver->s.mkTerm(cvc5::Kind::MULT, { res, other.term }); + div = this->solver->s.mkTerm(cvc5::Kind::INTS_MODULUS, { div, this->modulus }); + cvc5::Term eq = this->solver->s.mkTerm(cvc5::Kind::EQUAL, { this->term, div }); + this->solver->s.assertFormula(eq); + return { res, this->solver }; +} + +void FFITerm::operator/=(const FFITerm& other) +{ + cvc5::Term res = this->solver->s.mkConst(this->solver->fp, + "fe0f65a52067384116dc1137d798e0ca00a7ed46950e4eab7db51e08481535f2_div_" + + std::string(*this) + "__" + std::string(other)); + cvc5::Term div = this->solver->s.mkTerm(cvc5::Kind::MULT, { res, other.term }); + div = this->solver->s.mkTerm(cvc5::Kind::INTS_MODULUS, { div, this->modulus }); + cvc5::Term eq = this->solver->s.mkTerm(cvc5::Kind::EQUAL, { this->term, div }); + this->solver->s.assertFormula(eq); + this->term = res; +} + +/** + * Create an equality constraint between two finite field elements. + * + */ +void FFITerm::operator==(const FFITerm& other) const +{ + cvc5::Term eq = this->solver->s.mkTerm(cvc5::Kind::EQUAL, { this->term, other.term }); + this->solver->s.assertFormula(eq); +} + +/** + * Create an inequality constraint between two finite field elements. + * + */ +void FFITerm::operator!=(const FFITerm& other) const +{ + cvc5::Term eq = this->solver->s.mkTerm(cvc5::Kind::EQUAL, { this->term, other.term }); + eq = this->solver->s.mkTerm(cvc5::Kind::EQUAL, { eq, this->solver->s.mkBoolean(false) }); + this->solver->s.assertFormula(eq); +} +} // namespace smt_terms diff --git a/circuits/cpp/barretenberg/cpp/src/barretenberg/smt_verification/terms/ffiterm.hpp b/circuits/cpp/barretenberg/cpp/src/barretenberg/smt_verification/terms/ffiterm.hpp new file mode 100644 index 00000000000..9dba1e5a0ff --- /dev/null +++ b/circuits/cpp/barretenberg/cpp/src/barretenberg/smt_verification/terms/ffiterm.hpp @@ -0,0 +1,86 @@ +#pragma once +#include "barretenberg/smt_verification/solver/solver.hpp" + +namespace smt_terms { +using namespace smt_solver; + +/** + * @brief Integer Modulo element class. + * + * @details Can be a symbolic variable or a constant. + * Both of them support basic arithmetic operations: +, -, *, /. + * Check the satisfability of a system and get it's model. + * + * @todo TODO(alex): mayb.. Have to patch cvc5 to create integers from hex... + */ +class FFITerm { + public: + Solver* solver; + cvc5::Term term; + cvc5::Term modulus; + + FFITerm() + : solver(nullptr) + , term(cvc5::Term()) + , modulus(cvc5::Term()){}; + + explicit FFITerm(const std::string& t, Solver* slv, bool isconst = false); //, uint32_t base = 16); + FFITerm(cvc5::Term& term, Solver* s) + : solver(s) + , term(term) + , modulus(s->s.mkInteger(s->modulus)) + { + // cvc5::Term mod = s->s.mkBitVector(modulus_size, s->modulus, 16); + // modulus = s->s.mkTerm(cvc5::Kind::BITVECTOR_TO_NAT, {mod}); + } + + FFITerm(const FFITerm& other) = default; + FFITerm(FFITerm&& other) = default; + + FFITerm& operator=(const FFITerm& right) = default; + FFITerm& operator=(FFITerm&& right) = default; + + FFITerm operator+(const FFITerm& other) const; + void operator+=(const FFITerm& other); + FFITerm operator-(const FFITerm& other) const; + void operator-=(const FFITerm& other); + FFITerm operator*(const FFITerm& other) const; + void operator*=(const FFITerm& other); + FFITerm operator/(const FFITerm& other) const; + void operator/=(const FFITerm& other); + + void operator==(const FFITerm& other) const; + void operator!=(const FFITerm& other) const; + + operator std::string() const + { + return term.isIntegerValue() ? term.getIntegerValue() : term.toString(); + }; // TODO(alex): won't work for now since the conversion during initialization. + operator cvc5::Term() const { return term; }; + + ~FFITerm() = default; + friend std::ostream& operator<<(std::ostream& out, const FFITerm& k) { return out << k.term; } + + friend FFITerm batch_add(const std::vector& children) + { + Solver* slv = children[0].solver; + std::vector terms(children.begin(), children.end()); + cvc5::Term res = slv->s.mkTerm(cvc5::Kind::ADD, terms); + res = slv->s.mkTerm(cvc5::Kind::INTS_MODULUS, { res, children[0].modulus }); + return { res, slv }; + } + + friend FFITerm batch_mul(const std::vector& children) + { + Solver* slv = children[0].solver; + std::vector terms(children.begin(), children.end()); + cvc5::Term res = slv->s.mkTerm(cvc5::Kind::MULT, terms); + res = slv->s.mkTerm(cvc5::Kind::INTS_MODULUS, { res, children[0].modulus }); + return { res, slv }; + } +}; + +FFITerm IVar(const std::string& name, Solver* slv); +FFITerm IConst(const std::string& val, Solver* slv); //, uint32_t base = 16); + +} // namespace smt_terms From abe7fb7186b5ece691e9925ff7b2561a65240306 Mon Sep 17 00:00:00 2001 From: Sarkoxed Date: Wed, 6 Sep 2023 10:42:04 +0000 Subject: [PATCH 11/27] Just testing --- circuits/cpp/barretenberg/cpp/src/CMakeLists.txt | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/circuits/cpp/barretenberg/cpp/src/CMakeLists.txt b/circuits/cpp/barretenberg/cpp/src/CMakeLists.txt index 797035bcfe1..6fe1af5da3b 100644 --- a/circuits/cpp/barretenberg/cpp/src/CMakeLists.txt +++ b/circuits/cpp/barretenberg/cpp/src/CMakeLists.txt @@ -71,10 +71,10 @@ add_subdirectory(barretenberg/grumpkin_srs_gen) add_subdirectory(barretenberg/bb) -if(SMT) - include_directories(${CMAKE_CURRENT_SOURCE_DIR} $ENV{HOME}/cvc5/tmp-lib/include) - add_subdirectory(barretenberg/smt_verification) -endif() +#if(SMT) +include_directories(${CMAKE_CURRENT_SOURCE_DIR} $ENV{HOME}/cvc5/tmp-lib/include) +add_subdirectory(barretenberg/smt_verification) +#ndif() if(BENCHMARKS) add_subdirectory(barretenberg/benchmark) From bca6189c1f7f76bd792120c4df39b8fd4be068d5 Mon Sep 17 00:00:00 2001 From: Sarkoxed Date: Wed, 6 Sep 2023 10:51:21 +0000 Subject: [PATCH 12/27] back --- circuits/cpp/barretenberg/cpp/src/CMakeLists.txt | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/circuits/cpp/barretenberg/cpp/src/CMakeLists.txt b/circuits/cpp/barretenberg/cpp/src/CMakeLists.txt index 6fe1af5da3b..797035bcfe1 100644 --- a/circuits/cpp/barretenberg/cpp/src/CMakeLists.txt +++ b/circuits/cpp/barretenberg/cpp/src/CMakeLists.txt @@ -71,10 +71,10 @@ add_subdirectory(barretenberg/grumpkin_srs_gen) add_subdirectory(barretenberg/bb) -#if(SMT) -include_directories(${CMAKE_CURRENT_SOURCE_DIR} $ENV{HOME}/cvc5/tmp-lib/include) -add_subdirectory(barretenberg/smt_verification) -#ndif() +if(SMT) + include_directories(${CMAKE_CURRENT_SOURCE_DIR} $ENV{HOME}/cvc5/tmp-lib/include) + add_subdirectory(barretenberg/smt_verification) +endif() if(BENCHMARKS) add_subdirectory(barretenberg/benchmark) From aa72f77f898d6dd6c31bb9bed5d3483c0cca5b1b Mon Sep 17 00:00:00 2001 From: Sarkoxed Date: Thu, 7 Sep 2023 07:32:05 +0000 Subject: [PATCH 13/27] Added configuration structure and modulus translation to base10 string --- .../smt_verification/solver/solver.hpp | 35 +++++++++++++------ 1 file changed, 24 insertions(+), 11 deletions(-) diff --git a/circuits/cpp/barretenberg/cpp/src/barretenberg/smt_verification/solver/solver.hpp b/circuits/cpp/barretenberg/cpp/src/barretenberg/smt_verification/solver/solver.hpp index f8d4cf6a6d2..c4b9446fd14 100644 --- a/circuits/cpp/barretenberg/cpp/src/barretenberg/smt_verification/solver/solver.hpp +++ b/circuits/cpp/barretenberg/cpp/src/barretenberg/smt_verification/solver/solver.hpp @@ -1,9 +1,24 @@ #pragma once #include #include +#include namespace smt_solver { +/** + * @brief Solver configuration + * + * @param produce_model tells the solver to actually compute the values of the variables in SAT case. + * @param timeout tells the solver to stop trying after `timeout` msecs. + * + * @todo TODO(alex): more cvc5 options. + * @todo TODO(alex): make it class if it's more comfortable + */ +struct SolverConfiguration{ + bool produce_model; + uint32_t timeout; +}; + /** * @brief Class for the solver. * @@ -15,24 +30,22 @@ namespace smt_solver { * @todo TODO(alex) perhaps add the << operator to make it easier to read the constraints. */ class Solver { - private: - bool res = false; - bool checked = false; - public: cvc5::Solver s; cvc5::Sort fp; - std::string modulus; + std::string modulus; // modulus in base 10 + bool res = false; + bool checked = false; - explicit Solver(const std::string& modulus, bool produce_model = false, uint32_t base = 16, uint32_t timeout = 0) - : modulus(modulus) + explicit Solver(const std::string& modulus, const SolverConfiguration& config = {false, 0}, uint32_t base = 16) { - fp = s.mkFiniteFieldSort(modulus, base); - if (produce_model) { + this->fp = s.mkFiniteFieldSort(modulus, base); + this->modulus = fp.getFiniteFieldSize(); + if (config.produce_model) { s.setOption("produce-models", "true"); } - if (timeout > 0) { - s.setOption("tlimit-per", std::to_string(timeout)); + if (config.timeout > 0) { + s.setOption("tlimit-per", std::to_string(config.timeout)); } } From 18b1c3ac312bb6278be7044b3fd19f40f7e25926 Mon Sep 17 00:00:00 2001 From: Sarkoxed Date: Thu, 7 Sep 2023 07:33:18 +0000 Subject: [PATCH 14/27] No zero division + Var and Const now are the static members of FFTerm Class --- .../barretenberg/smt_verification/terms/ffterm.cpp | 13 ++++++++++--- .../barretenberg/smt_verification/terms/ffterm.hpp | 8 ++++---- 2 files changed, 14 insertions(+), 7 deletions(-) diff --git a/circuits/cpp/barretenberg/cpp/src/barretenberg/smt_verification/terms/ffterm.cpp b/circuits/cpp/barretenberg/cpp/src/barretenberg/smt_verification/terms/ffterm.cpp index ee3e322a8dc..2e8cb249b34 100644 --- a/circuits/cpp/barretenberg/cpp/src/barretenberg/smt_verification/terms/ffterm.cpp +++ b/circuits/cpp/barretenberg/cpp/src/barretenberg/smt_verification/terms/ffterm.cpp @@ -9,7 +9,7 @@ namespace smt_terms { * @param slv Pointer to the global solver. * @return Finite field symbolic variable. * */ -FFTerm Var(const std::string& name, Solver* slv) +FFTerm FFTerm::Var(const std::string& name, Solver* slv) { return FFTerm(name, slv); }; @@ -22,7 +22,7 @@ FFTerm Var(const std::string& name, Solver* slv) * @param base Base of the string representation. 16 by default. * @return Finite field constant. * */ -FFTerm Const(const std::string& val, Solver* slv, uint32_t base) +FFTerm FFTerm::Const(const std::string& val, Solver* slv, uint32_t base) { return FFTerm(val, slv, true, base); }; @@ -40,7 +40,6 @@ FFTerm::FFTerm(const std::string& t, Solver* slv, bool isconst, uint32_t base) FFTerm FFTerm::operator+(const FFTerm& other) const { cvc5::Term res = this->solver->s.mkTerm(cvc5::Kind::FINITE_FIELD_ADD, { this->term, other.term }); - ; return { res, this->solver }; } @@ -85,6 +84,10 @@ void FFTerm::operator*=(const FFTerm& other) */ FFTerm FFTerm::operator/(const FFTerm& other) const { + cvc5::Term nz = this->solver->s.mkTerm(cvc5::Kind::EQUAL, {other.term, this->solver->s.mkFiniteFieldElem("0", this->solver->fp)}); + nz = this->solver->s.mkTerm(cvc5::Kind::EQUAL, {nz, this->solver->s.mkBoolean(false)}); + this->solver->s.assertFormula(nz); + cvc5::Term res = this->solver->s.mkConst(this->solver->fp, "fe0f65a52067384116dc1137d798e0ca00a7ed46950e4eab7db51e08481535f2_div_" + std::string(*this) + "_" + std::string(other)); @@ -96,6 +99,10 @@ FFTerm FFTerm::operator/(const FFTerm& other) const void FFTerm::operator/=(const FFTerm& other) { + cvc5::Term nz = this->solver->s.mkTerm(cvc5::Kind::EQUAL, {other.term, this->solver->s.mkFiniteFieldElem("0", this->solver->fp)}); + nz = this->solver->s.mkTerm(cvc5::Kind::EQUAL, {nz, this->solver->s.mkBoolean(false)}); + this->solver->s.assertFormula(nz); + cvc5::Term res = this->solver->s.mkConst(this->solver->fp, "fe0f65a52067384116dc1137d798e0ca00a7ed46950e4eab7db51e08481535f2_div_" + std::string(*this) + "__" + std::string(other)); diff --git a/circuits/cpp/barretenberg/cpp/src/barretenberg/smt_verification/terms/ffterm.hpp b/circuits/cpp/barretenberg/cpp/src/barretenberg/smt_verification/terms/ffterm.hpp index fb9d33cd4e5..a213464854a 100644 --- a/circuits/cpp/barretenberg/cpp/src/barretenberg/smt_verification/terms/ffterm.hpp +++ b/circuits/cpp/barretenberg/cpp/src/barretenberg/smt_verification/terms/ffterm.hpp @@ -28,6 +28,9 @@ class FFTerm { FFTerm(const FFTerm& other) = default; FFTerm(FFTerm&& other) = default; + static FFTerm Var(const std::string& name, Solver* slv); + static FFTerm Const(const std::string& val, Solver* slv, uint32_t base = 16); + FFTerm& operator=(const FFTerm& right) = default; FFTerm& operator=(FFTerm&& right) = default; @@ -45,7 +48,7 @@ class FFTerm { operator std::string() const { return term.isFiniteFieldValue() ? term.getFiniteFieldValue() : term.toString(); }; operator cvc5::Term() const { return term; }; - + ~FFTerm() = default; friend std::ostream& operator<<(std::ostream& out, const FFTerm& k) { return out << k.term; } @@ -66,7 +69,4 @@ class FFTerm { } }; -FFTerm Var(const std::string& name, Solver* slv); -FFTerm Const(const std::string& val, Solver* slv, uint32_t base = 16); - } // namespace smt_terms \ No newline at end of file From 82e4a5298d3ece0d19e08bf95ea9744541c98a47 Mon Sep 17 00:00:00 2001 From: Sarkoxed Date: Thu, 7 Sep 2023 07:33:46 +0000 Subject: [PATCH 15/27] New integer mod backend --- .../smt_verification/terms/ffiterm.cpp | 28 ++++++++++++++----- .../smt_verification/terms/ffiterm.hpp | 16 ++++------- 2 files changed, 27 insertions(+), 17 deletions(-) diff --git a/circuits/cpp/barretenberg/cpp/src/barretenberg/smt_verification/terms/ffiterm.cpp b/circuits/cpp/barretenberg/cpp/src/barretenberg/smt_verification/terms/ffiterm.cpp index b9dc022e6a7..c4fae8310d1 100644 --- a/circuits/cpp/barretenberg/cpp/src/barretenberg/smt_verification/terms/ffiterm.cpp +++ b/circuits/cpp/barretenberg/cpp/src/barretenberg/smt_verification/terms/ffiterm.cpp @@ -9,7 +9,7 @@ namespace smt_terms { * @param slv Pointer to the global solver. * @return Finite field symbolic variable. * */ -FFITerm IVar(const std::string& name, Solver* slv) +FFITerm FFITerm::Var(const std::string& name, Solver* slv) { return FFITerm(name, slv); }; @@ -22,12 +22,12 @@ FFITerm IVar(const std::string& name, Solver* slv) * @param base Base of the string representation. 16 by default. * @return Finite field constant. * */ -FFITerm IConst(const std::string& val, Solver* slv) //, uint32_t base) +FFITerm FFITerm::Const(const std::string& val, Solver* slv, uint32_t base) { - return FFITerm(val, slv, true); //, base); + return FFITerm(val, slv, true, base); }; -FFITerm::FFITerm(const std::string& t, Solver* slv, bool isconst) //, uint32_t base) +FFITerm::FFITerm(const std::string& t, Solver* slv, bool isconst, uint32_t base) : solver(slv) , modulus(slv->s.mkInteger(slv->modulus)) { @@ -38,7 +38,13 @@ FFITerm::FFITerm(const std::string& t, Solver* slv, bool isconst) //, uint32_t b slv->s.assertFormula(ge); slv->s.assertFormula(lt); } else { - this->term = slv->s.mkInteger(t); //, base); + std::string tmp = slv->s.mkFiniteFieldElem(t, slv->fp, base).getFiniteFieldValue(); // dumb but works + if(tmp[0] == '-'){ + this->term = slv->s.mkInteger(tmp) + this->modulus; + }else{ + this->term = slv->s.mkInteger(tmp); + } + // this->term = slv->s.mkInteger(tmp); won't work for now since the assertion will definitely fail } } @@ -96,6 +102,10 @@ void FFITerm::operator*=(const FFITerm& other) */ FFITerm FFITerm::operator/(const FFITerm& other) const { + cvc5::Term nz = this->solver->s.mkTerm(cvc5::Kind::EQUAL, {other.term, this->solver->s.mkInteger("0")}); + nz = this->solver->s.mkTerm(cvc5::Kind::EQUAL, {nz, this->solver->s.mkBoolean(false)}); + this->solver->s.assertFormula(nz); + cvc5::Term res = this->solver->s.mkConst(this->solver->s.getIntegerSort(), "fe0f65a52067384116dc1137d798e0ca00a7ed46950e4eab7db51e08481535f2_div_" + std::string(*this) + "_" + std::string(other)); @@ -108,6 +118,10 @@ FFITerm FFITerm::operator/(const FFITerm& other) const void FFITerm::operator/=(const FFITerm& other) { + cvc5::Term nz = this->solver->s.mkTerm(cvc5::Kind::EQUAL, {other.term, this->solver->s.mkInteger("0")}); + nz = this->solver->s.mkTerm(cvc5::Kind::EQUAL, {nz, this->solver->s.mkBoolean(false)}); + this->solver->s.assertFormula(nz); + cvc5::Term res = this->solver->s.mkConst(this->solver->fp, "fe0f65a52067384116dc1137d798e0ca00a7ed46950e4eab7db51e08481535f2_div_" + std::string(*this) + "__" + std::string(other)); @@ -119,7 +133,7 @@ void FFITerm::operator/=(const FFITerm& other) } /** - * Create an equality constraint between two finite field elements. + * Create an equality constraint between two integer mod elements. * */ void FFITerm::operator==(const FFITerm& other) const @@ -129,7 +143,7 @@ void FFITerm::operator==(const FFITerm& other) const } /** - * Create an inequality constraint between two finite field elements. + * Create an inequality constraint between two integer mod elements. * */ void FFITerm::operator!=(const FFITerm& other) const diff --git a/circuits/cpp/barretenberg/cpp/src/barretenberg/smt_verification/terms/ffiterm.hpp b/circuits/cpp/barretenberg/cpp/src/barretenberg/smt_verification/terms/ffiterm.hpp index 9dba1e5a0ff..319ec1736ec 100644 --- a/circuits/cpp/barretenberg/cpp/src/barretenberg/smt_verification/terms/ffiterm.hpp +++ b/circuits/cpp/barretenberg/cpp/src/barretenberg/smt_verification/terms/ffiterm.hpp @@ -24,19 +24,18 @@ class FFITerm { , term(cvc5::Term()) , modulus(cvc5::Term()){}; - explicit FFITerm(const std::string& t, Solver* slv, bool isconst = false); //, uint32_t base = 16); + explicit FFITerm(const std::string& t, Solver* slv, bool isconst = false, uint32_t base = 16); FFITerm(cvc5::Term& term, Solver* s) : solver(s) , term(term) - , modulus(s->s.mkInteger(s->modulus)) - { - // cvc5::Term mod = s->s.mkBitVector(modulus_size, s->modulus, 16); - // modulus = s->s.mkTerm(cvc5::Kind::BITVECTOR_TO_NAT, {mod}); - } + , modulus(s->s.mkInteger(s->modulus)){} FFITerm(const FFITerm& other) = default; FFITerm(FFITerm&& other) = default; + static FFITerm Var(const std::string& name, Solver* slv); + static FFITerm Const(const std::string& val, Solver* slv, uint32_t base = 16); + FFITerm& operator=(const FFITerm& right) = default; FFITerm& operator=(FFITerm&& right) = default; @@ -55,7 +54,7 @@ class FFITerm { operator std::string() const { return term.isIntegerValue() ? term.getIntegerValue() : term.toString(); - }; // TODO(alex): won't work for now since the conversion during initialization. + }; operator cvc5::Term() const { return term; }; ~FFITerm() = default; @@ -80,7 +79,4 @@ class FFITerm { } }; -FFITerm IVar(const std::string& name, Solver* slv); -FFITerm IConst(const std::string& val, Solver* slv); //, uint32_t base = 16); - } // namespace smt_terms From ba2e49dda85e38611b3c9517372033e756fd005c Mon Sep 17 00:00:00 2001 From: Sarkoxed Date: Thu, 7 Sep 2023 07:35:23 +0000 Subject: [PATCH 16/27] Circuit Class now a template. Added binary gate realaxation. --- .../smt_verification/circuit/circuit.cpp | 149 +--------------- .../smt_verification/circuit/circuit.hpp | 168 +++++++++++++++++- 2 files changed, 168 insertions(+), 149 deletions(-) diff --git a/circuits/cpp/barretenberg/cpp/src/barretenberg/smt_verification/circuit/circuit.cpp b/circuits/cpp/barretenberg/cpp/src/barretenberg/smt_verification/circuit/circuit.cpp index 5ee96b77a32..08966e53607 100644 --- a/circuits/cpp/barretenberg/cpp/src/barretenberg/smt_verification/circuit/circuit.cpp +++ b/circuits/cpp/barretenberg/cpp/src/barretenberg/smt_verification/circuit/circuit.cpp @@ -1,147 +1,6 @@ #include "circuit.hpp" namespace smt_circuit { -/** - * @brief Construct a new Circuit::Circuit object - * - * @param circuit_info CircuitShema object - * @param solver pointer to the global solver - * @param tag tag of the circuit. Empty by default. - */ -Circuit::Circuit(CircuitSchema& circuit_info, Solver* solver, const std::string& tag) - : public_inps(circuit_info.public_inps) - , vars_of_interest(circuit_info.vars_of_interest) - , wit_idxs(circuit_info.wits) - , solver(solver) - , tag(tag) -{ - if (!this->tag.empty()) { - if (this->tag[0] != '_') { - this->tag = "_" + this->tag; - } - } - - for (auto var : circuit_info.variables) { - std::stringstream buf; // TODO(alex): looks bad. Would be great to create tostring() converter - buf << var; - std::string tmp = buf.str(); - tmp[1] = '0'; // avoiding x in 0x part - variables.push_back(tmp); - } - - for (auto& x : vars_of_interest) { - terms.insert({ x.second, x.first }); - } - - // I hope they are still at these idxs - vars_of_interest.insert({ 0, "zero" }); - vars_of_interest.insert({ 1, "one" }); - terms.insert({ "zero", 0 }); - terms.insert({ "one", 1 }); - - for (auto sel : circuit_info.selectors) { - std::vector tmp_sel; - for (size_t j = 0; j < 5; j++) { - std::stringstream buf; // TODO(alex): #2 - buf << sel[j]; - std::string q_i = buf.str(); - q_i[1] = '0'; // avoiding x in 0x part - tmp_sel.push_back(q_i); - } - selectors.push_back(tmp_sel); - } - - this->init(); - this->add_gates(); -} - -/** - * Creates all the needed symbolic variables and constants - * which are used in circuit. - * - */ -void Circuit::init() -{ - size_t num_vars = variables.size(); - - vars.push_back(Var("zero" + this->tag, this->solver)); - vars.push_back(Var("one" + this->tag, this->solver)); - - for (size_t i = 2; i < num_vars; i++) { - if (vars_of_interest.contains(static_cast(i))) { - std::string name = vars_of_interest[static_cast(i)]; - vars.push_back(Var(name + this->tag, this->solver)); - } else { - vars.push_back(Var("var_" + std::to_string(i) + this->tag, this->solver)); - } - } - - vars[0] == Const("0", this->solver); - vars[1] == Const("1", this->solver); - - for (auto i : public_inps) { - vars[i] == Const(variables[i], this->solver); - } -} - -/** - * @brief Adds all the gate constraints to the solver. - * - */ -void Circuit::add_gates() -{ - for (size_t i = 0; i < get_num_gates(); i++) { - FFTerm q_m = Const(selectors[i][0], this->solver); - FFTerm q_1 = Const(selectors[i][1], this->solver); - FFTerm q_2 = Const(selectors[i][2], this->solver); - FFTerm q_3 = Const(selectors[i][3], this->solver); - FFTerm q_c = Const(selectors[i][4], this->solver); - - uint32_t w_l = wit_idxs[i][0]; - uint32_t w_r = wit_idxs[i][1]; - uint32_t w_o = wit_idxs[i][2]; - - FFTerm eq = vars[0]; - - // mult selector - if (std::string(q_m) != "0") { - eq += q_m * vars[w_l] * vars[w_r]; - } - // w_l selector - if (std::string(q_1) != "0") { - eq += q_1 * vars[w_l]; - } - // w_r selector - if (std::string(q_2) != "0") { - eq += q_2 * vars[w_r]; - } - // w_o selector - if (std::string(q_3) != "0") { - eq += q_3 * vars[w_o]; - } - // w_c selector - if (std::string(q_c) != "0") { - eq += q_c; - } - eq == vars[0]; - } -} - -/** - * @brief Returns a previously named symbolic variable. - * - * @param name - * @return FFTerm - */ -FFTerm Circuit::operator[](const std::string& name) -{ - if (!this->terms.contains(name)) { - throw std::length_error("No such an item " + name + " in vars or it vas not declared as interesting"); - } - uint32_t idx = this->terms[name]; - return this->vars[idx]; -} - /** * @brief Get the CircuitSchema object * @details Initialize the CircuitSchmea from the binary file @@ -202,16 +61,18 @@ CircuitSchema unpack_from_buffer(const msgpack::sbuffer& buf) * @param eqall all the variables that should not be equal at the same time * @param neqall all the variables that should not be different at the same time * @return std::pair + * + * @todo TODO(alex): didn't figure out how to separate them. */ -std::pair unique_witness(CircuitSchema& circuit_info, +std::pair, Circuit> unique_witness(CircuitSchema& circuit_info, Solver* s, const std::vector& equal, const std::vector& nequal, const std::vector& eqall, const std::vector& neqall) { - Circuit c1(circuit_info, s, "circuit1"); - Circuit c2(circuit_info, s, "circuit2"); + Circuit c1(circuit_info, s, "circuit1"); + Circuit c2(circuit_info, s, "circuit2"); for (const auto& term : equal) { c1[term] == c2[term]; diff --git a/circuits/cpp/barretenberg/cpp/src/barretenberg/smt_verification/circuit/circuit.hpp b/circuits/cpp/barretenberg/cpp/src/barretenberg/smt_verification/circuit/circuit.hpp index 5aafb332c6e..d4e43874f37 100644 --- a/circuits/cpp/barretenberg/cpp/src/barretenberg/smt_verification/circuit/circuit.hpp +++ b/circuits/cpp/barretenberg/cpp/src/barretenberg/smt_verification/circuit/circuit.hpp @@ -32,10 +32,11 @@ struct CircuitSchema { * @details Contains all the information about the circuit: gates, variables, * symbolic variables, specified names and global solver. * + * @tparam FF FFTerm or FFITerm + * * @todo TODO(alex): think on the partial value assertion inside the circuit. - * @todo TODO(alex): class SymCircuit? - * @todo TODO(alex): FFTerm operator[](uint32_t) */ +template class Circuit { private: void init(); @@ -48,7 +49,7 @@ class Circuit { std::unordered_map terms; // inverse map of the previous memeber std::vector> selectors; // selectors from the circuit std::vector> wit_idxs; // values used in gates from the circuit - std::vector vars; // all the symbolic variables in the circuit + std::vector vars; // all the symbolic variables in the circuit Solver* solver; // pointer to the solver std::string tag; // tag of the symbolic circuit. @@ -57,15 +58,172 @@ class Circuit { explicit Circuit(CircuitSchema& circuit_info, Solver* solver, const std::string& tag = ""); - FFTerm operator[](const std::string& name); + FF operator[](const std::string& name); + FF operator[](const uint32_t& idx) { return vars[idx]; }; inline uint32_t get_num_gates() const { return static_cast(selectors.size()); }; inline uint32_t get_num_vars() const { return static_cast(vars.size()); }; }; +/** + * @brief Construct a new Circuit::Circuit object + * + * @param circuit_info CircuitShema object + * @param solver pointer to the global solver + * @param tag tag of the circuit. Empty by default. + */ +template +Circuit::Circuit(CircuitSchema& circuit_info, Solver* solver, const std::string& tag) + : public_inps(circuit_info.public_inps) + , vars_of_interest(circuit_info.vars_of_interest) + , wit_idxs(circuit_info.wits) + , solver(solver) + , tag(tag) +{ + if (!this->tag.empty()) { + if (this->tag[0] != '_') { + this->tag = "_" + this->tag; + } + } + + for (auto var : circuit_info.variables) { + std::stringstream buf; // TODO(alex): looks bad. Would be great to create tostring() converter + buf << var; + std::string tmp = buf.str(); + tmp[1] = '0'; // avoiding x in 0x part + variables.push_back(tmp); + } + + for (auto& x : vars_of_interest) { + terms.insert({ x.second, x.first }); + } + + // I hope they are still at these idxs + vars_of_interest.insert({ 0, "zero" }); + vars_of_interest.insert({ 1, "one" }); + terms.insert({ "zero", 0 }); + terms.insert({ "one", 1 }); + + for (auto sel : circuit_info.selectors) { + std::vector tmp_sel; + for (size_t j = 0; j < 5; j++) { + std::stringstream buf; // TODO(alex): #2 + buf << sel[j]; + std::string q_i = buf.str(); + q_i[1] = '0'; // avoiding x in 0x part + tmp_sel.push_back(q_i); + } + selectors.push_back(tmp_sel); + } + + this->init(); + this->add_gates(); +} + +/** + * Creates all the needed symbolic variables and constants + * which are used in circuit. + * + */ +template +void Circuit::init() +{ + size_t num_vars = variables.size(); + + vars.push_back(FF::Var("zero" + this->tag, this->solver)); + vars.push_back(FF::Var("one" + this->tag, this->solver)); + + for (size_t i = 2; i < num_vars; i++) { + if (vars_of_interest.contains(static_cast(i))) { + std::string name = vars_of_interest[static_cast(i)]; + vars.push_back(FF::Var(name + this->tag, this->solver)); + } else { + vars.push_back(FF::Var("var_" + std::to_string(i) + this->tag, this->solver)); + } + } + + vars[0] == FF::Const("0", this->solver); + vars[1] == FF::Const("1", this->solver); + + for (auto i : public_inps) { + vars[i] == FF::Const(variables[i], this->solver); + } +} + +/** + * @brief Adds all the gate constraints to the solver. + * + */ +template +void Circuit::add_gates() +{ + for (size_t i = 0; i < get_num_gates(); i++) { + FF q_m = FF::Const(selectors[i][0], this->solver); + FF q_1 = FF::Const(selectors[i][1], this->solver); + FF q_2 = FF::Const(selectors[i][2], this->solver); + FF q_3 = FF::Const(selectors[i][3], this->solver); + FF q_c = FF::Const(selectors[i][4], this->solver); + + uint32_t w_l = wit_idxs[i][0]; + uint32_t w_r = wit_idxs[i][1]; + uint32_t w_o = wit_idxs[i][2]; + + // Binary gate. Relaxes the solver. + // TODO(alex): Probably we can add other basic gates here too to relax the stuff. + // TODO(alex): Theoretically this can be applyed after we ensure that the block of polynomial equations holds + // and then simplify that block in future to relax the solver constraint system. Seems like a hard one to implement or actually to automate, but I'll think on it for a while. + // it will probably require to split add_gates and init methods into more complex/generalized parts. + if(w_l == w_r && w_r == w_o){ + if(std::string(q_m) == "1" && std::string(q_1) == "0" && std::string(q_2) == "0" && std::string(q_3) == "-1" && std::string(q_c) == "0"){ // squaring gate + (Bool(vars[w_l]) == Bool(vars[0]) | Bool(vars[w_l]) == Bool(vars[1])).assert_term(); + } + } + + FF eq = vars[0]; + + // mult selector + if (std::string(q_m) != "0") { + eq += q_m * vars[w_l] * vars[w_r]; + } + // w_l selector + if (std::string(q_1) != "0") { + eq += q_1 * vars[w_l]; + } + // w_r selector + if (std::string(q_2) != "0") { + eq += q_2 * vars[w_r]; + } + // w_o selector + if (std::string(q_3) != "0") { + eq += q_3 * vars[w_o]; + } + // w_c selector + if (std::string(q_c) != "0") { + eq += q_c; + } + eq == vars[0]; + } +} + +/** + * @brief Returns a previously named symbolic variable. + * + * @param name + * @return FF + */ +template +FF Circuit::operator[](const std::string& name) +{ + if (!this->terms.contains(name)) { + throw std::length_error("No such an item " + name + " in vars or it vas not declared as interesting"); + } + uint32_t idx = this->terms[name]; + return this->vars[idx]; +} + CircuitSchema unpack_from_buffer(const msgpack::sbuffer& buf); CircuitSchema unpack_from_file(const std::string& fname); -std::pair unique_witness(CircuitSchema& circuit_info, +std::pair, Circuit> unique_witness(CircuitSchema& circuit_info, Solver* s, const std::vector& equal, const std::vector& nequal, From 0dfbc1c5a27e637002f872aa45ea66a07d592471 Mon Sep 17 00:00:00 2001 From: Sarkoxed Date: Thu, 7 Sep 2023 07:36:25 +0000 Subject: [PATCH 17/27] Syntax fixes --- .../barretenberg/smt_verification/README.md | 3 +++ .../smt_verification/smt_bigfield.test.cpp | 22 +++++++++-------- .../smt_verification/smt_examples.test.cpp | 24 +++++++++---------- .../smt_verification/smt_intmod.test.cpp | 20 ++++++++++++++++ .../smt_verification/smt_polynomials.test.cpp | 12 +++++----- 5 files changed, 53 insertions(+), 28 deletions(-) create mode 100644 circuits/cpp/barretenberg/cpp/src/barretenberg/smt_verification/smt_intmod.test.cpp diff --git a/circuits/cpp/barretenberg/cpp/src/barretenberg/smt_verification/README.md b/circuits/cpp/barretenberg/cpp/src/barretenberg/smt_verification/README.md index 5871045129c..39135c41b31 100644 --- a/circuits/cpp/barretenberg/cpp/src/barretenberg/smt_verification/README.md +++ b/circuits/cpp/barretenberg/cpp/src/barretenberg/smt_verification/README.md @@ -1,5 +1,7 @@ # Building cvc5 +TODO(alex): update the docunmentation after all the fixes + As for now it's required to build cvc5 library manually.