satisfiliability check: multithreaded

crypto3/libs/blueprint/include/nil/blueprint/blueprint/plonk/assignment_proxy.hpp

@@ -445,23 +445,6 @@ namespace nil {
             }
             return res;
         }
-
-        template<typename BlueprintFieldType>
-        bool is_satisfied(const circuit_proxy<crypto3::zk::snark::plonk_constraint_system<BlueprintFieldType>>
-                            &bp,
-                          const assignment_proxy<crypto3::zk::snark::plonk_constraint_system<BlueprintFieldType>>
-                            &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& selector_rows = assignments.get_used_selector_rows();
-
-            return is_satisfied(bp, assignments, used_gates, used_lookup_gates, used_copy_constraints, selector_rows);
-        }
     }    // namespace blueprint
 }    // namespace nil
 #endif    // CRYPTO3_BLUEPRINT_ASSIGNMENT_PROXY_PLONK_HPP

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

@@ -73,6 +73,8 @@ namespace nil {
             gate_selector_map selector_map = {};
             lookup_gate_selector_map lookup_selector_map = {};
             std::size_t next_selector_index = 0;
+            std::map<uint32_t, std::vector<std::string>> constraint_names_;
+
         protected:
             lookup_library<BlueprintFieldType> _lookup_library;
         public:
@@ -206,6 +208,11 @@ namespace nil {
                 _lookup_library.reserve_dynamic_table(name);
             }
 
+            // used in satisfiability check
+            void register_constraint_names(std::uint32_t selector_id, std::vector<std::string> names) {
+                constraint_names_.insert({selector_id, names});
+            }
+
             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);
             }
@@ -233,6 +240,11 @@ namespace nil {
                 return _lookup_library.get_reserved_dynamic_tables();
             }
 
+            // used in satisfiability check
+            virtual std::string get_constraint_name(std::size_t selector_id, std::size_t index) const {
+                return constraint_names_.at(selector_id).at(index);
+            }
+
             #undef GATE_ADDER_MACRO
             #undef LOOKUP_GATE_ADDER_MACRO
             #undef GENERIC_GATE_ADDER_MACRO

crypto3/libs/blueprint/test/zkevm_bbf/circuit_test_fixture.hpp

@@ -183,7 +183,9 @@ class CircuitTestFixture {
         }
         bool result = true;
         if (check_satisfiability) {
-            result = result & builder.is_satisfied(assignment, /* verbose = */ true);
+            result = result & builder.is_satisfied(assignment, satisfiability_check_options{
+                .verbose = true
+            });
         }
         // It's debug mode. Prover from non-satisfied circuit will throw asserts
         if (result && generate_proof) {

proof-producer/bin/proof-producer/include/nil/proof-generator/commands/preset_command.hpp

@@ -24,11 +24,11 @@ namespace nil {
 
         template<typename CurveType, typename HashType>
         struct PresetStep {
-            using Types            = TypeSystem<CurveType, HashType>;
-            using BlueprintField   = typename Types::BlueprintField;
-            using ConstraintSystem = typename Types::ConstraintSystem;
-            using AssignmentTable  = typename Types::AssignmentTable;
-            using TableDescription = typename Types::TableDescription;
+            using Types                  = TypeSystem<CurveType, HashType>;
+            using BlueprintField         = typename Types::BlueprintField;
+            using ConstraintSystem       = typename Types::ConstraintSystem;
+            using AssignmentTable        = typename Types::AssignmentTable;
+            using TableDescription       = typename Types::TableDescription;
 
             struct Executor:
                 public command_step,

proof-producer/libs/preset/include/nil/proof-generator/preset/bytecode.hpp

@@ -20,6 +20,7 @@ namespace nil {
                 std::shared_ptr<typename PresetTypes<BlueprintFieldType>::ConstraintSystem>& bytecode_circuit,
                 std::shared_ptr<typename PresetTypes<BlueprintFieldType>::AssignmentTable>& bytecode_table,
                 const CircuitsLimits& circuits_limits) {
+
             using ConstraintSystem = typename PresetTypes<BlueprintFieldType>::ConstraintSystem;
             using AssignmentTable = typename PresetTypes<BlueprintFieldType>::AssignmentTable;
 

proof-producer/libs/preset/include/nil/proof-generator/preset/copy.hpp

@@ -17,6 +17,7 @@ namespace nil {
                 std::shared_ptr<typename PresetTypes<BlueprintFieldType>::ConstraintSystem>& copy_circuit,
                 std::shared_ptr<typename PresetTypes<BlueprintFieldType>::AssignmentTable>& copy_table,
                 const CircuitsLimits& circuits_limits) {
+
             using ConstraintSystem = typename PresetTypes<BlueprintFieldType>::ConstraintSystem;
             using AssignmentTable = typename PresetTypes<BlueprintFieldType>::AssignmentTable;
 

proof-producer/libs/preset/include/nil/proof-generator/preset/exp.hpp

@@ -7,6 +7,7 @@
 #include <nil/blueprint/bbf/enums.hpp>
 #include <nil/blueprint/blueprint/plonk/circuit.hpp>
 #include <nil/crypto3/zk/snark/arithmetization/plonk/assignment.hpp>
+#include <nil/proof-generator/types/type_system.hpp>
 #include <nil/proof-generator/preset/limits.hpp>
 #include <nil/blueprint/zkevm_bbf/exp.hpp>
 #include <nil/blueprint/bbf/circuit_builder.hpp>
@@ -21,6 +22,7 @@ namespace nil {
                 std::shared_ptr<typename PresetTypes<BlueprintFieldType>::ConstraintSystem>& exp_circuit,
                 std::shared_ptr<typename PresetTypes<BlueprintFieldType>::AssignmentTable>&  exp_table,
                 const CircuitsLimits& circuits_limits) {
+
             using ConstraintSystem = typename PresetTypes<BlueprintFieldType>::ConstraintSystem;
             using AssignmentTable = typename PresetTypes<BlueprintFieldType>::AssignmentTable;
 

proof-producer/libs/preset/include/nil/proof-generator/preset/preset.hpp

@@ -33,9 +33,9 @@ namespace nil {
 
         template<typename BlueprintFieldType>
         class CircuitFactory {
-            using Circuit          = typename PresetTypes<BlueprintFieldType>::ConstraintSystem;
-            using AssignmentTable  = typename PresetTypes<BlueprintFieldType>::AssignmentTable;
-            using TableDescription = typename PresetTypes<BlueprintFieldType>::TableDescription;
+            using Circuit                = typename PresetTypes<BlueprintFieldType>::ConstraintSystem;
+            using AssignmentTable        = typename PresetTypes<BlueprintFieldType>::AssignmentTable;
+            using TableDescription       = typename PresetTypes<BlueprintFieldType>::TableDescription;
 
             using CircuitInitializer = std::function<std::optional<std::string>(
                 std::shared_ptr<Circuit>& circuit,

proof-producer/libs/preset/include/nil/proof-generator/preset/rw.hpp

@@ -19,6 +19,7 @@ namespace nil {
                 std::shared_ptr<typename PresetTypes<BlueprintFieldType>::ConstraintSystem>& rw_circuit,
                 std::shared_ptr<typename PresetTypes<BlueprintFieldType>::AssignmentTable>& rw_table,
                 const CircuitsLimits& circuits_limits) {
+
             using ConstraintSystem = typename PresetTypes<BlueprintFieldType>::ConstraintSystem;
             using AssignmentTable = typename PresetTypes<BlueprintFieldType>::AssignmentTable;
 

proof-producer/libs/preset/include/nil/proof-generator/preset/zkevm.hpp

@@ -23,6 +23,7 @@ namespace nil {
                 std::shared_ptr<typename PresetTypes<BlueprintFieldType>::ConstraintSystem>& zkevm_circuit,
                 std::shared_ptr<typename PresetTypes<BlueprintFieldType>::AssignmentTable>& zkevm_table,
                 const CircuitsLimits& circuits_limits) {
+
             using ConstraintSystem = typename PresetTypes<BlueprintFieldType>::ConstraintSystem;
             using AssignmentTable = typename PresetTypes<BlueprintFieldType>::AssignmentTable;
 

proof-producer/libs/types/include/nil/proof-generator/types/type_system.hpp

@@ -46,16 +46,16 @@
 #include <nil/blueprint/transpiler/recursive_verifier_generator.hpp>
 #include <nil/blueprint/transpiler/lpc_evm_verifier_gen.hpp>
 #include <nil/blueprint/blueprint/plonk/circuit.hpp>
-
+#include <nil/blueprint/bbf/circuit_builder.hpp>
+#include <nil/blueprint/utils/satisfiability_check.hpp>
 
 namespace nil {
     namespace proof_producer {
 
-        // TODO naming
         template <typename BlueprintField>
         struct PresetTypes {
             using ConstraintSystem = nil::blueprint::circuit<nil::crypto3::zk::snark::plonk_constraint_system<BlueprintField>>;
-            using AssignmentTable = nil::crypto3::zk::snark::plonk_assignment_table<BlueprintField>;
+            using AssignmentTable  = nil::crypto3::zk::snark::plonk_assignment_table<BlueprintField>;
             using TableDescription = nil::crypto3::zk::snark::plonk_table_description<BlueprintField>;
         };
 

proof-producer/tests/bin/proof-producer/test_zkevm_bbf_circuits.cpp

@@ -29,7 +29,6 @@ class ProverTests: public ::testing::TestWithParam<Input> {
         using BlueprintFieldType = nil::proof_producer::TypeSystem<CurveType, HashType>::BlueprintField;
         using AssignmentTable = nil::proof_producer::TypeSystem<CurveType, HashType>::AssignmentTable;
 
-
         class AssignmentTableChecker: public nil::proof_producer::command_chain {
 
         public:
@@ -67,12 +66,14 @@ TEST_P(ProverTests, FillAssignmentAndCheck) {
     ASSERT_NE(checker.circuit_, nullptr);
     ASSERT_NE(checker.assignment_table_, nullptr);
 
-    ASSERT_TRUE(nil::blueprint::is_satisfied<BlueprintFieldType>(
+    auto const check_res = nil::blueprint::satisfiability_checker<BlueprintFieldType>::is_satisfied(
         *checker.circuit_,
-        *checker.assignment_table_
-    ));
-}
+        *checker.assignment_table_,
+        nil::blueprint::satisfiability_check_options{.verbose = true}
+    );
 
+    ASSERT_TRUE(check_res);
+}
 
 using namespace nil::proof_producer::circuits;