Skip to content

Commit

Permalink
Avoid slow std::set::find() in satifiability check
Browse files Browse the repository at this point in the history
  • Loading branch information
akokoshn committed Jan 5, 2024
1 parent be4dd99 commit 7ae9a6b
Show file tree
Hide file tree
Showing 2 changed files with 123 additions and 100 deletions.
5 changes: 3 additions & 2 deletions include/nil/blueprint/blueprint/plonk/assignment_proxy.hpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -430,15 +430,16 @@ namespace nil {
ArithmetizationParams>> &bp,
const assignment_proxy<crypto3::zk::snark::plonk_constraint_system<BlueprintFieldType,
ArithmetizationParams>> &assignments){

const auto& used_gates = bp.get_used_gates();

const auto& used_lookup_gates = bp.get_used_lookup_gates();

const auto& used_copy_constraints = bp.get_used_copy_constraints();

const auto& private_rows = assignments.get_used_selector_rows();
const auto& selector_rows = assignments.get_used_selector_rows();

return is_satisfied(bp, assignments, used_gates, used_lookup_gates, used_copy_constraints, private_rows);
return is_satisfied(bp, assignments, used_gates, used_lookup_gates, used_copy_constraints, selector_rows);
}
} // namespace blueprint
} // namespace nil
Expand Down
218 changes: 120 additions & 98 deletions include/nil/blueprint/utils/satisfiability_check.hpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -40,138 +40,160 @@
namespace nil {
namespace blueprint {

template<typename BlueprintFieldType,
typename ArithmetizationParams>
bool is_satisfied(
const circuit<crypto3::zk::snark::plonk_constraint_system<BlueprintFieldType,
ArithmetizationParams>> &bp,
const assignment<crypto3::zk::snark::plonk_constraint_system<BlueprintFieldType,
ArithmetizationParams>> &assignments) {
std::set<uint32_t> used_gates;
for (std::uint32_t i = 0; i < bp.gates().size(); i++) {
used_gates.insert(i);
}

std::set<uint32_t> used_lookup_gates;
for (std::uint32_t i = 0; i < bp.lookup_gates().size(); i++) {
used_lookup_gates.insert(i);
}

std::set<uint32_t> used_copy_constraints;
for (std::uint32_t i = 0; i < bp.copy_constraints().size(); i++) {
used_copy_constraints.insert(i);
}

std::set<uint32_t> selector_rows;
for (std::uint32_t i = 0; i < assignments.allocated_rows(); i++) {
selector_rows.insert(i);
}

return is_satisfied(bp, assignments, used_gates, used_lookup_gates, used_copy_constraints, selector_rows);
}

template<typename BlueprintFieldType,
typename ArithmetizationParams>
bool is_satisfied(
const circuit<crypto3::zk::snark::plonk_constraint_system<BlueprintFieldType,
ArithmetizationParams>> &bp,
const assignment<crypto3::zk::snark::plonk_constraint_system<BlueprintFieldType,
ArithmetizationParams>> &assignments,
const std::set<std::uint32_t> &used_gates = std::set<std::uint32_t>(),
const std::set<std::uint32_t> &used_lookup_gates = std::set<std::uint32_t>(),
const std::set<std::uint32_t> &used_copy_constraints = std::set<std::uint32_t>(),
const std::set<std::uint32_t> &private_rows = std::set<std::uint32_t>()){
const std::set<std::uint32_t> &used_gates,
const std::set<std::uint32_t> &used_lookup_gates,
const std::set<std::uint32_t> &used_copy_constraints,
const std::set<std::uint32_t> &selector_rows){

const auto &gates = bp.gates();

const auto &copy_constraints = bp.copy_constraints();

const auto &lookup_gates = bp.lookup_gates();

for (std::size_t i = 0; i < gates.size(); i++) {
if (used_gates.empty() || used_gates.find(i) != used_gates.end()) {
crypto3::zk::snark::plonk_column<BlueprintFieldType> selector =
assignments.crypto3::zk::snark::
template plonk_assignment_table<BlueprintFieldType, ArithmetizationParams>::selector(
gates[i].selector_index);

for (std::size_t selector_row = 0; selector_row < selector.size(); selector_row++) {
if (!selector[selector_row].is_zero() &&
(private_rows.empty() || private_rows.find(selector_row) != private_rows.end())) {
for (std::size_t j = 0; j < gates[i].constraints.size(); j++) {

typename BlueprintFieldType::value_type constraint_result =
gates[i].constraints[j].evaluate(selector_row, assignments);

if (!constraint_result.is_zero()) {
std::cout << "Constraint " << j << " from gate " << i << " on row " << selector_row
<< " is not satisfied." << std::endl;
std::cout << "Constraint result: " << constraint_result << std::endl;
std::cout << "Offending gate:" << std::endl;
for (const auto &constraint : gates[i].constraints) {
std::cout << constraint << std::endl;
}
return false;
for (const auto& i : used_gates) {
crypto3::zk::snark::plonk_column<BlueprintFieldType> selector =
assignments.crypto3::zk::snark::
template plonk_assignment_table<BlueprintFieldType, ArithmetizationParams>::selector(
gates[i].selector_index);

for (const auto& selector_row : selector_rows) {
if (selector_row < selector.size() && !selector[selector_row].is_zero()) {
for (std::size_t j = 0; j < gates[i].constraints.size(); j++) {

typename BlueprintFieldType::value_type constraint_result =
gates[i].constraints[j].evaluate(selector_row, assignments);

if (!constraint_result.is_zero()) {
std::cout << "Constraint " << j << " from gate " << i << " on row " << selector_row
<< " is not satisfied." << std::endl;
std::cout << "Constraint result: " << constraint_result << std::endl;
std::cout << "Offending gate:" << std::endl;
for (const auto &constraint : gates[i].constraints) {
std::cout << constraint << std::endl;
}
return false;
}
}
}
}
}

for (std::size_t i = 0; i < lookup_gates.size(); i++) {
if (used_lookup_gates.empty() || used_lookup_gates.find(i) != used_lookup_gates.end()) {
crypto3::zk::snark::plonk_column<BlueprintFieldType> selector =
assignments.crypto3::zk::snark::
template plonk_assignment_table<BlueprintFieldType, ArithmetizationParams>::selector(
lookup_gates[i].tag_index);

for (std::size_t selector_row = 0; selector_row < selector.size(); selector_row++) {
if (!selector[selector_row].is_zero() &&
(private_rows.empty() || private_rows.find(selector_row) != private_rows.end())) {
for (std::size_t j = 0; j < lookup_gates[i].constraints.size(); j++) {
std::vector<typename BlueprintFieldType::value_type> input_values;
input_values.reserve(lookup_gates[i].constraints[j].lookup_input.size());
for (std::size_t k = 0; k < lookup_gates[i].constraints[j].lookup_input.size(); k++) {
input_values.emplace_back(lookup_gates[i].constraints[j].lookup_input[k].evaluate(
selector_row, assignments));
}
const auto table_name =
bp.get_reserved_indices_right().at(lookup_gates[i].constraints[j].table_id);
try {
std::string main_table_name = table_name.substr(0, table_name.find("/"));
std::string subtable_name =
table_name.substr(table_name.find("/") + 1, table_name.size() - 1);
const auto &table = bp.get_reserved_tables().at(main_table_name)->get_table();
const auto &subtable =
bp.get_reserved_tables().at(main_table_name)->subtables.at(subtable_name);

std::size_t columns_number = subtable.column_indices.size();

// Search the table for the input values
// We can cache it with sorting, or use KMP, but I need a simple solution first
bool found = false;
BOOST_ASSERT(columns_number == input_values.size());
for (std::size_t k = 0; k < table[0].size(); k++) {
bool match = true;
for (std::size_t l = 0; l < columns_number; l++) {
if (table[subtable.column_indices[l]][k] != input_values[l]) {
match = false;
break;
}
}
if (match) {
found = true;
for (const auto& i : used_lookup_gates) {
crypto3::zk::snark::plonk_column<BlueprintFieldType> selector =
assignments.crypto3::zk::snark::
template plonk_assignment_table<BlueprintFieldType, ArithmetizationParams>::selector(
lookup_gates[i].tag_index);

for (const auto& selector_row : selector_rows) {
if (selector_row < selector.size() && !selector[selector_row].is_zero()) {
for (std::size_t j = 0; j < lookup_gates[i].constraints.size(); j++) {
std::vector<typename BlueprintFieldType::value_type> input_values;
input_values.reserve(lookup_gates[i].constraints[j].lookup_input.size());
for (std::size_t k = 0; k < lookup_gates[i].constraints[j].lookup_input.size(); k++) {
input_values.emplace_back(lookup_gates[i].constraints[j].lookup_input[k].evaluate(
selector_row, assignments));
}
const auto table_name =
bp.get_reserved_indices_right().at(lookup_gates[i].constraints[j].table_id);
try {
std::string main_table_name = table_name.substr(0, table_name.find("/"));
std::string subtable_name =
table_name.substr(table_name.find("/") + 1, table_name.size() - 1);
const auto &table = bp.get_reserved_tables().at(main_table_name)->get_table();
const auto &subtable =
bp.get_reserved_tables().at(main_table_name)->subtables.at(subtable_name);

std::size_t columns_number = subtable.column_indices.size();

// Search the table for the input values
// We can cache it with sorting, or use KMP, but I need a simple solution first
bool found = false;
BOOST_ASSERT(columns_number == input_values.size());
for (std::size_t k = 0; k < table[0].size(); k++) {
bool match = true;
for (std::size_t l = 0; l < columns_number; l++) {
if (table[subtable.column_indices[l]][k] != input_values[l]) {
match = false;
break;
}
}
if (!found) {
std::cout << "Input values:";
for (std::size_t k = 0; k < input_values.size(); k++) {
std::cout << input_values[k] << " ";
}
std::cout << std::endl;
std::cout << "Constraint " << j << " from lookup gate " << i << " from table "
<< table_name << " on row " << selector_row << " is not satisfied."
<< std::endl;
std::cout << "Offending Lookup Gate: " << std::endl;
for (const auto &constraint : lookup_gates[i].constraints) {
std::cout << "Table id: " << constraint.table_id << std::endl;
for (auto &lookup_input : constraint.lookup_input) {
std::cout << lookup_input << std::endl;
}
if (match) {
found = true;
break;
}
}
if (!found) {
std::cout << "Input values:";
for (std::size_t k = 0; k < input_values.size(); k++) {
std::cout << input_values[k] << " ";
}
std::cout << std::endl;
std::cout << "Constraint " << j << " from lookup gate " << i << " from table "
<< table_name << " on row " << selector_row << " is not satisfied."
<< std::endl;
std::cout << "Offending Lookup Gate: " << std::endl;
for (const auto &constraint : lookup_gates[i].constraints) {
std::cout << "Table id: " << constraint.table_id << std::endl;
for (auto &lookup_input : constraint.lookup_input) {
std::cout << lookup_input << std::endl;
}
return false;
}
} catch (std::out_of_range &e) {
std::cout << "Lookup table " << table_name << " not found." << std::endl;
return false;
}
} catch (std::out_of_range &e) {
std::cout << "Lookup table " << table_name << " not found." << std::endl;
return false;
}
}
}
}
}

for (std::size_t i = 0; i < copy_constraints.size(); i++) {
if (used_copy_constraints.empty() || used_copy_constraints.find(i) != used_copy_constraints.end()) {
if (var_value(assignments, copy_constraints[i].first) !=
var_value(assignments, copy_constraints[i].second)) {
std::cout << "Copy constraint number " << i << " is not satisfied."
<< " First variable: " << copy_constraints[i].first
<< " second variable: " << copy_constraints[i].second << std::endl;
return false;
}
for (const auto& i : used_copy_constraints) {
if (var_value(assignments, copy_constraints[i].first) !=
var_value(assignments, copy_constraints[i].second)) {
std::cout << "Copy constraint number " << i << " is not satisfied."
<< " First variable: " << copy_constraints[i].first
<< " second variable: " << copy_constraints[i].second << std::endl;
return false;
}
}
return true;
Expand Down

0 comments on commit 7ae9a6b

Please sign in to comment.