Skip to content

Commit

Permalink
Dynamic lookup tables implemented #413
Browse files Browse the repository at this point in the history
  • Loading branch information
@ETatuzova
ETatuzova committed Aug 6, 2024
1 parent 890ab5f commit c5abab7
Show file tree
Hide file tree
Showing 8 changed files with 739 additions and 104 deletions.
8 changes: 4 additions & 4 deletions flake.lock
View file

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

36 changes: 36 additions & 0 deletions include/nil/blueprint/blueprint/plonk/circuit.hpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -68,6 +68,7 @@ namespace nil {
using lookup_gate_selector_map = std::map<lookup_gate_id_type, std::size_t>;

using lookup_table_definition = typename nil::crypto3::zk::snark::lookup_table_definition<BlueprintFieldType>;
using dynamic_table_definition = typename nil::crypto3::zk::snark::dynamic_table_definition<BlueprintFieldType>;

gate_selector_map selector_map = {};
lookup_gate_selector_map lookup_selector_map = {};
Expand Down Expand Up @@ -154,6 +155,14 @@ namespace nil {
LOOKUP_GATE_ADDER_MACRO(lookup_selector_map, _lookup_gates);
}


// Sometimes we want to connect new constraints to existing selector
// Use only with deep understanding
virtual std::size_t add_gate(std::size_t selector_id, const std::vector<constraint_type> &args) {
this->_gates.push_back({selector_id, args});
return selector_id;
}

// Sometimes existing gate is already on existing selector
// and we are sure that lookup and usual part are always together
virtual std::size_t add_lookup_gate(std::size_t selector_id, const std::vector<lookup_constraint_type> &args) {
Expand All @@ -165,6 +174,13 @@ namespace nil {
return ArithmetizationType::lookup_table(table_id);
}

// Each component that creates dynamic lookup needs separate selector for it
virtual std::size_t get_dynamic_lookup_table_selector(){
const std::size_t selector_index = next_selector_index;
next_selector_index++;
return selector_index;
}

virtual void add_lookup_table(const typename ArithmetizationType::lookup_table_type &table) {
ArithmetizationType::add_lookup_table(table);
}
Expand All @@ -173,10 +189,26 @@ namespace nil {
_lookup_library.register_lookup_table(table);
}

virtual void register_dynamic_table(std::string name) {
_lookup_library.register_dynamic_table(name);
}

virtual void reserve_table(std::string name){
_lookup_library.reserve_table(name);
}

virtual void reserve_dynamic_table(std::string name){
_lookup_library.reserve_dynamic_table(name);
}

std::shared_ptr<crypto3::zk::snark::dynamic_table_definition<BlueprintFieldType>> get_dynamic_table_definition(std::string name){
return _lookup_library.get_dynamic_table_definition(name);
}

virtual void define_dynamic_table(std::string name, const crypto3::zk::snark::plonk_lookup_table<BlueprintFieldType> &table){
_lookup_library.define_dynamic_table(name, table);
}

virtual const typename lookup_library<BlueprintFieldType>::left_reserved_type
&get_reserved_indices() const {
return _lookup_library.get_reserved_indices().left;
Expand All @@ -192,6 +224,10 @@ namespace nil {
return _lookup_library.get_reserved_tables();
}

virtual const std::map<std::string, std::shared_ptr<dynamic_table_definition>> &get_reserved_dynamic_tables() const {
return _lookup_library.get_reserved_dynamic_tables();
}

#undef GATE_ADDER_MACRO
#undef LOOKUP_GATE_ADDER_MACRO
#undef GENERIC_GATE_ADDER_MACRO
Expand Down
76 changes: 60 additions & 16 deletions include/nil/blueprint/lookup_library.hpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -66,10 +66,13 @@ namespace nil {
template <typename BlueprintFieldType>
class lookup_library {
using lookup_table_definition = typename nil::crypto3::zk::snark::lookup_table_definition<BlueprintFieldType>;
using dynamic_table_definition = typename nil::crypto3::zk::snark::dynamic_table_definition<BlueprintFieldType>;
using filled_lookup_table_definition = typename nil::crypto3::zk::snark::filled_lookup_table_definition<BlueprintFieldType>;

class byte_range_table_type: public lookup_table_definition{
public:
using lookup_table_definition = typename nil::crypto3::zk::snark::lookup_table_definition<BlueprintFieldType>;

byte_range_table_type(): lookup_table_definition("byte_range_table"){
this->subtables["full"] = {{0}, 0, 255};
}
Expand Down Expand Up @@ -345,43 +348,77 @@ namespace nil {
tables["sha256_maj"] = std::shared_ptr<lookup_table_definition>(new maj_function_table());
tables["sha256_ch"] = std::shared_ptr<lookup_table_definition>(new ch_function_table());
tables["byte_range_table"] = std::shared_ptr<lookup_table_definition>(new byte_range_table_type());
tables["zkevm_opcodes"] = std::shared_ptr<lookup_table_definition>(new zkevm_opcode_table);
tables["zkevm_opcodes"] = std::shared_ptr<lookup_table_definition>(new zkevm_opcode_table());
}

void register_lookup_table(std::shared_ptr<lookup_table_definition> table){
tables[table->table_name] = table;
}

void register_dynamic_table(std::string table_name){
BOOST_ASSERT(tables.find(table_name) == tables.end());
dynamic_tables[table_name] = std::shared_ptr<dynamic_table_definition>(new dynamic_table_definition(table_name));
}

void reserve_table(std::string name){
BOOST_ASSERT(!reserved_all);
std::string table_name = name.substr(0, name.find("/"));
// Necessary for dynamic and for fixed tables
BOOST_ASSERT(tables.find(table_name) != tables.end());
std::string subtable_name = name.substr(name.find("/")+1, name.size());
BOOST_ASSERT(tables[table_name]->subtables.find(subtable_name) != tables[table_name]->subtables.end());
reserved_tables.insert(name);
reserved_tables_indices.left.insert(std::make_pair(name, reserved_tables.size()));
}

void reserve_dynamic_table(std::string name){
BOOST_ASSERT(tables.find(name) == tables.end());
BOOST_ASSERT(!reserved_all);

register_dynamic_table(name);
reserved_tables.insert(name);
reserved_tables_indices.left.insert(std::make_pair(name, reserved_tables.size()));
}

void define_dynamic_table(std::string table_name, const crypto3::zk::snark::plonk_lookup_table<BlueprintFieldType> &lookup_table){
register_dynamic_table(table_name);
auto table = dynamic_tables[table_name];
BOOST_ASSERT(!table->is_defined());
table->define(lookup_table);
BOOST_ASSERT(table->is_defined());
}

std::shared_ptr<dynamic_table_definition> get_dynamic_table_definition(std::string table_name){
auto table = dynamic_tables[table_name];
BOOST_ASSERT(table->is_defined());
return std::shared_ptr<dynamic_table_definition>(table);
}

void reservation_done() const {
if(reserved_all) return;

reserved_all = true;
for (auto &name : reserved_tables){
auto slash_pos = name.find("/");
std::string table_name = name.substr(0, slash_pos);
BOOST_ASSERT(tables.find(table_name) != tables.end());
std::string subtable_name = name.substr(slash_pos + 1, name.size());
auto const &table = tables.at(table_name);
BOOST_ASSERT(table->subtables.find(subtable_name) !=
table->subtables.end());

if( reserved_tables_map.find(table_name) == reserved_tables_map.end() ){
filled_lookup_table_definition *filled_definition =
new filled_lookup_table_definition(*(table));
reserved_tables_map[table_name] = std::shared_ptr<lookup_table_definition>(filled_definition);
if( dynamic_tables.find(name) != dynamic_tables.end() ){
reserved_dynamic_tables_map[name] = dynamic_tables.at(name);
} else {
auto slash_pos = name.find("/");
std::string table_name = name.substr(0, slash_pos);
BOOST_ASSERT(tables.find(table_name) != tables.end());
auto const &table = tables.at(table_name);

std::string subtable_name = name.substr(slash_pos + 1, name.size());
BOOST_ASSERT(table->subtables.find(subtable_name) !=
table->subtables.end());

if( reserved_tables_map.find(table_name) == reserved_tables_map.end() ){
filled_lookup_table_definition *filled_definition =
new filled_lookup_table_definition(*(table));
reserved_tables_map[table_name] = std::shared_ptr<lookup_table_definition>(filled_definition);
}
reserved_tables_map[table_name]->subtables[subtable_name] =
table->subtables[subtable_name];
}
reserved_tables_map[table_name]->subtables[subtable_name] =
table->subtables[subtable_name];
}
}

Expand All @@ -393,13 +430,20 @@ namespace nil {
reservation_done();
return reserved_tables_map;
}

const std::map<std::string, std::shared_ptr<dynamic_table_definition>> &get_reserved_dynamic_tables() const {
reservation_done();
return reserved_dynamic_tables_map;
}
protected:
mutable bool reserved_all;

std::map<std::string, std::shared_ptr<lookup_table_definition>> tables;
std::set<std::string> reserved_tables;
bimap_type reserved_tables_indices;
std::map<std::string, std::shared_ptr<lookup_table_definition>> tables;
mutable std::map<std::string, std::shared_ptr<lookup_table_definition>> reserved_tables_map;
std::map<std::string, std::shared_ptr<dynamic_table_definition>> dynamic_tables;
mutable std::map<std::string, std::shared_ptr<dynamic_table_definition>> reserved_dynamic_tables_map;
};
} // namespace blueprint
} // namespace nil
Expand Down
57 changes: 57 additions & 0 deletions include/nil/blueprint/utils/satisfiability_check.hpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -67,6 +67,36 @@ namespace nil {
return is_satisfied(bp, assignments, used_gates, used_lookup_gates, used_copy_constraints, selector_rows);
}

template<typename BlueprintFieldType>
std::set<std::vector<typename BlueprintFieldType::value_type>>
load_dynamic_lookup(
const circuit<crypto3::zk::snark::plonk_constraint_system<BlueprintFieldType>> &bp,
const assignment<crypto3::zk::snark::plonk_constraint_system<BlueprintFieldType>> &assignments,
std::size_t table_id
){
std::set<std::vector<typename BlueprintFieldType::value_type>> result;
auto &table = bp.lookup_tables()[table_id-1];

crypto3::zk::snark::plonk_column<BlueprintFieldType> selector =
assignments.crypto3::zk::snark::
template plonk_assignment_table<BlueprintFieldType>::selector(table.tag_index);

for( std::size_t selector_row = 0; selector_row < assignments.rows_amount(); selector_row++ ){
if( selector_row < selector.size() && !selector[selector_row].is_zero() ){
for( std::size_t op = 0; op < table.lookup_options.size(); op++){
std::vector<typename BlueprintFieldType::value_type> item(table.lookup_options[op].size());
for( std::size_t i = 0; i < table.lookup_options[op].size(); i++){
crypto3::zk::snark::plonk_constraint<BlueprintFieldType> expr = table.lookup_options[op][i];;
item[i] = expr.evaluate(selector_row, assignments);
}
result.insert(item);
}
}
}

return result;
}

template<typename BlueprintFieldType>
bool is_satisfied(
const circuit<crypto3::zk::snark::plonk_constraint_system<BlueprintFieldType>> &bp,
Expand All @@ -82,6 +112,8 @@ namespace nil {

const auto &lookup_gates = bp.lookup_gates();

std::map<std::string, std::set<std::vector<typename BlueprintFieldType::value_type>>> used_dynamic_tables;

for (const auto& i : used_gates) {
crypto3::zk::snark::plonk_column<BlueprintFieldType> selector =
assignments.crypto3::zk::snark::
Expand Down Expand Up @@ -128,9 +160,33 @@ namespace nil {
const auto table_name =
bp.get_reserved_indices_right().at(lookup_gates[i].constraints[j].table_id);
try {
if( bp.get_reserved_dynamic_tables().find(table_name) != bp.get_reserved_dynamic_tables().end() ){
if( used_dynamic_tables.find(table_name) == used_dynamic_tables.end()){
used_dynamic_tables[table_name] = load_dynamic_lookup(bp, assignments, lookup_gates[i].constraints[j].table_id);
}
if( used_dynamic_tables[table_name].find(input_values) == used_dynamic_tables[table_name].end() ) {
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;
}
continue;
}
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);
Expand Down Expand Up @@ -174,6 +230,7 @@ namespace nil {
}
} catch (std::out_of_range &e) {
std::cout << "Lookup table " << table_name << " not found." << std::endl;
std::cout << "Table_id = " << lookup_gates[i].constraints[j].table_id << " table_name " << table_name << std::endl;
return false;
}
}
Expand Down
Loading

0 comments on commit c5abab7

Please sign in to comment.