Dynamic lookup tables implemented #413

flake.nix

@@ -14,6 +14,7 @@
  nil-crypto3 = {
  url = "https://github.com/NilFoundation/crypto3";
  type = "git";
+ ref = "283-dynamic-lookups";
  inputs = {
  nixpkgs.follows = "nixpkgs";
  };

include/nil/blueprint/blueprint/plonk/circuit.hpp

@@ -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 = {};
@@ -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) {
@@ -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);
  }
@@ -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;
@@ -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

include/nil/blueprint/lookup_library.hpp

@@ -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};
  }
@@ -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];
  }
  }
 
@@ -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

include/nil/blueprint/utils/satisfiability_check.hpp

@@ -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,
@@ -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::
@@ -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);
@@ -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;
  }
  }