feat: SMT verification module updates (#13551)

This pr mostly consists of code refactoring/renames 

## Cmake

`cvc5` build is now multi-threaded

## Circuit Builders

`CircuitBuilderBase` - added `circuit_finalized` into msgpack schema
`UltraCircuitBuilder` - zero is now force renamed during circuit export

## smt_subcircuits

switched `0xabbba` to `0` since it produced failures duirng circuit
creations

## Solver

- Added new method `get` and `operator[]`. These two methods extract the
value of the variable from solver. Added a test
- fixed the incorrectly placed `BITVECTOR_UDIV`
- renamed `getValue` to `get_symbolic_value` to avoid confusion

## Terms

- New constructor, based on `bb::fr` value
- Got rid of `isFiniteField` like members. Useless
- Added `normalize` method, for more readability
- Refactored the operators

## SMT_Util

- add `is_signed` flag in `string_to_fr()` to avoid overflows 

## Tests

For most part it's either a rename, engine switch or new `operator[]`
refactoring

Also 
- fixed an incorrect `extract_bit` test
- 

All the current changes are reflected in `README.md`

---------

Co-authored-by: Innokentii Sennovskii <[email protected]>

Author: Sarkoxed

barretenberg/cpp/src/barretenberg/smt_verification/CMakeLists.txt

@@ -13,7 +13,7 @@ ExternalProject_Add(
     GIT_TAG main
     BUILD_IN_SOURCE YES
     CONFIGURE_COMMAND ${SHELL} ./configure.sh production --gpl --auto-download --cocoa --cryptominisat --kissat -DCMAKE_C_COMPILER=/usr/bin/clang -DCMAKE_CXX_COMPILER=/usr/bin/clang++ --prefix=${CVC5_BUILD}
-    BUILD_COMMAND make -C build
+    BUILD_COMMAND make -C build -j8
     INSTALL_COMMAND make -C build install
     UPDATE_COMMAND ""     # No update step
     # needed by ninja

barretenberg/cpp/src/barretenberg/smt_verification/README.md

@@ -12,7 +12,7 @@ Then just build with `smt-verification` preset.
 
 - ```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.
 
-**!Note that you don't have to name a zero or one(in standard). It has the name `zero` by default.**
+**!NOTE that somtimes you may encounter variables that are set to be `assert_equal` to `zero`. Their name will be erased no matter what first variable in class says.**
 
 - ```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.
 
@@ -179,8 +179,14 @@ To store it on the disk just do the following
 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<str, str> res = solver.model(unordered_map<str, FFTerm> terms)`.
-   Or you can provide a vector of terms that you want to check and the return map will contain their symbolic names that are given during initialization. Specifically either it's the name that you set or `var_{i}`.
+You have three choices:
+- You can access each of the terms directly by calling `solver[term]`, or `solver.get(term)`
+- You can generate an unordered map with `str->term` values and ask the solver to obtain `unordered_map<str, str> res = solver.model(unordered_map<str, FFTerm> terms)`.
+- You can generate a vector of terms and pass them to `unordered_map<str, str> res = solver.model(vector<FFTerm> terms)`. In this case the mapping name will be taken directly from solver. Specifically either it's the name that you have set or `var_{i}`.
+
+**!Note that the resulting values are strings and you can't use them to generate further constraints.**
+In case you want such a behavior use `sym_val = solver.get_value(term)`
+You can then create `STerm(sym_val, &solver, Type)` and use it in operations as a constant
 
 Now you have the values of the specified terms, which resulted into `true` result.
 **!Note that the return values are decimal strings/binary strings**, so if you want to use them later you should use `FFConst` with base 10, etc.
@@ -246,7 +252,28 @@ Besides already mentioned `smt_timer`, `default_model` and `default_model_single
 ```
 Where `add_unique_output` is a witness obtained by the solver.
 
-## 6. Simple examples
+## 6. Tests
+
+Avalaible test suits in `smt_verification_tests`:
+
+- `Solver*`
+---
+
+- `FFTerm*`
+- `FFITerm*`
+- `ITerm*`
+- `BVTerm*`
+---
+
+- `Subcircuits*`
+- `Standard_circuit*`
+- `Ultra_circuit*`
+---
+
+- `SMT_Example*`
+- `Polynomial_evaluation*`
+
+## 7. Simple examples
 
 ### Function Equality
 ```cpp

barretenberg/cpp/src/barretenberg/smt_verification/circuit/circuit_schema.hpp

@@ -43,7 +43,8 @@ struct CircuitSchema {
                    real_variable_index,
                    lookup_tables,
                    real_variable_tags,
-                   range_tags);
+                   range_tags,
+                   circuit_finalized);
 };
 
 CircuitSchema unpack_from_buffer(const msgpack::sbuffer& buf);

barretenberg/cpp/src/barretenberg/smt_verification/circuit/standard_circuit.test.cpp

@@ -15,15 +15,15 @@ using namespace bb;
 using namespace smt_circuit;
 
 namespace {
-auto& engine = numeric::get_debug_randomness();
+auto& engine = numeric::get_randomness();
 }
 
 using field_t = stdlib::field_t<StandardCircuitBuilder>;
 using witness_t = stdlib::witness_t<StandardCircuitBuilder>;
 using pub_witness_t = stdlib::public_witness_t<StandardCircuitBuilder>;
 using uint_ct = stdlib::uint32<StandardCircuitBuilder>;
 
-TEST(standard_circuit, assert_equal)
+TEST(Standard_circuit, assert_equal)
 {
     StandardCircuitBuilder builder = StandardCircuitBuilder();
 
@@ -62,7 +62,7 @@ TEST(standard_circuit, assert_equal)
     ASSERT_EQ(circuit[i.get_witness_index()].term, circuit[j.get_witness_index()].term);
 }
 
-TEST(standard_circuit, cached_subcircuits)
+TEST(Standard_circuit, cached_subcircuits)
 {
     StandardCircuitBuilder builder = StandardCircuitBuilder();
     field_t a(witness_t(&builder, fr::zero()));
@@ -75,11 +75,11 @@ TEST(standard_circuit, cached_subcircuits)
     auto buf = builder.export_circuit();
     CircuitSchema circuit_info = unpack_from_buffer(buf);
     Solver s(circuit_info.modulus);
-    StandardCircuit circuit(circuit_info, &s, TermType::FFITerm);
+    StandardCircuit circuit(circuit_info, &s, TermType::BVTerm);
     s.print_assertions();
 }
 
-TEST(standard_circuit, range_relaxation_assertions)
+TEST(Standard_circuit, range_relaxation_assertions)
 {
     StandardCircuitBuilder builder = StandardCircuitBuilder();
     field_t a(witness_t(&builder, fr(120)));
@@ -100,7 +100,7 @@ TEST(standard_circuit, range_relaxation_assertions)
     s.print_assertions();
 }
 
-TEST(standard_circuit, range_relaxation)
+TEST(Standard_circuit, range_relaxation)
 {
     for (size_t i = 2; i < 256; i++) {
         StandardCircuitBuilder builder = StandardCircuitBuilder();
@@ -110,11 +110,11 @@ TEST(standard_circuit, range_relaxation)
         auto buf = builder.export_circuit();
         CircuitSchema circuit_info = unpack_from_buffer(buf);
         Solver s(circuit_info.modulus);
-        StandardCircuit circuit(circuit_info, &s, TermType::FFITerm);
+        StandardCircuit circuit(circuit_info, &s, TermType::BVTerm);
     }
 }
 
-TEST(standard_circuit, xor_relaxation_assertions)
+TEST(Standard_circuit, xor_relaxation_assertions)
 {
     StandardCircuitBuilder builder = StandardCircuitBuilder();
     uint_ct a(witness_t(&builder, static_cast<uint32_t>(fr(120))));
@@ -132,7 +132,7 @@ TEST(standard_circuit, xor_relaxation_assertions)
     s.print_assertions();
 }
 
-TEST(standard_circuit, xor_relaxation)
+TEST(Standard_circuit, xor_relaxation)
 {
     for (size_t i = 2; i < 256; i += 2) {
         StandardCircuitBuilder builder = StandardCircuitBuilder();
@@ -147,7 +147,7 @@ TEST(standard_circuit, xor_relaxation)
     }
 }
 
-TEST(standard_circuit, and_relaxation_assertions)
+TEST(Standard_circuit, and_relaxation_assertions)
 {
     StandardCircuitBuilder builder = StandardCircuitBuilder();
     uint_ct a(witness_t(&builder, static_cast<uint32_t>(fr(120))));
@@ -165,7 +165,7 @@ TEST(standard_circuit, and_relaxation_assertions)
     s.print_assertions();
 }
 
-TEST(standard_circuit, ror_relaxation_assertions)
+TEST(Standard_circuit, ror_relaxation_assertions)
 {
     StandardCircuitBuilder builder = StandardCircuitBuilder();
     uint_ct a(witness_t(&builder, static_cast<uint32_t>(fr(120))));
@@ -181,7 +181,7 @@ TEST(standard_circuit, ror_relaxation_assertions)
     s.print_assertions();
 }
 
-TEST(standard_circuit, ror_relaxation)
+TEST(Standard_circuit, ror_relaxation)
 {
     for (size_t i = 1; i < 8; i++) {
         using uint_ct = stdlib::uint8<StandardCircuitBuilder>;
@@ -229,7 +229,7 @@ TEST(standard_circuit, ror_relaxation)
     }
 }
 
-TEST(standard_circuit, shl_relaxation_assertions)
+TEST(Standard_circuit, shl_relaxation_assertions)
 {
     StandardCircuitBuilder builder = StandardCircuitBuilder();
     uint_ct a(witness_t(&builder, static_cast<uint32_t>(fr(120))));
@@ -245,7 +245,7 @@ TEST(standard_circuit, shl_relaxation_assertions)
     s.print_assertions();
 }
 
-TEST(standard_circuit, shl_relaxation)
+TEST(Standard_circuit, shl_relaxation)
 {
     for (size_t i = 1; i < 8; i++) {
         using uint_ct = stdlib::uint8<StandardCircuitBuilder>;
@@ -293,7 +293,7 @@ TEST(standard_circuit, shl_relaxation)
     }
 }
 
-TEST(standard_circuit, shr_relaxation_assertions)
+TEST(Standard_circuit, shr_relaxation_assertions)
 {
     StandardCircuitBuilder builder = StandardCircuitBuilder();
     uint_ct a(witness_t(&builder, static_cast<uint32_t>(fr(120))));
@@ -309,7 +309,7 @@ TEST(standard_circuit, shr_relaxation_assertions)
     s.print_assertions();
 }
 
-TEST(standard_circuit, shr_relaxation)
+TEST(Standard_circuit, shr_relaxation)
 {
     for (size_t i = 1; i < 8; i += 2) {
         using uint_ct = stdlib::uint8<StandardCircuitBuilder>;
@@ -357,7 +357,7 @@ TEST(standard_circuit, shr_relaxation)
     }
 }
 
-TEST(standard_circuit, check_double_xor_bug)
+TEST(Standard_circuit, check_double_xor_bug)
 {
     StandardCircuitBuilder builder;
     uint_ct a = witness_t(&builder, 10);
@@ -379,7 +379,7 @@ TEST(standard_circuit, check_double_xor_bug)
 
 // Check that witness provided by the solver is the same as builder's witness
 // Check that all the optimized out values are initialized and computed properly during post proccessing
-TEST(standard_circuit, optimized_range_witness)
+TEST(Standard_circuit, optimized_range_witness)
 {
     uint32_t rbit = engine.get_random_uint8() & 1;
     uint32_t num_bits = 32 + rbit;
@@ -398,7 +398,7 @@ TEST(standard_circuit, optimized_range_witness)
 
     bool res = smt_timer(&s);
     ASSERT_TRUE(res);
-    auto model_witness = default_model_single({ "a" }, circuit, "optimized_range_check.out");
+    auto model_witness = default_model_single({ "a" }, circuit, "tmp.out");
 
     ASSERT_EQ(model_witness.size(), builder.get_num_variables());
     for (size_t i = 0; i < model_witness.size(); i++) {
@@ -408,7 +408,7 @@ TEST(standard_circuit, optimized_range_witness)
 
 // Check that witness provided by the solver is the same as builder's witness
 // Check that all the optimized out values are initialized and computed properly during post proccessing
-TEST(standard_circuit, optimized_logic_witness)
+TEST(Standard_circuit, optimized_logic_witness)
 {
     StandardCircuitBuilder builder;
     uint_ct a = witness_t(&builder, engine.get_random_uint32());
@@ -429,7 +429,7 @@ TEST(standard_circuit, optimized_logic_witness)
 
     bool res = smt_timer(&s);
     ASSERT_TRUE(res);
-    auto model_witness = default_model_single({ "a", "b", "c", "d" }, circuit, "optimized_xor_check.out");
+    auto model_witness = default_model_single({ "a", "b", "c", "d" }, circuit, "tmp.out");
 
     ASSERT_EQ(model_witness.size(), builder.get_num_variables());
     for (size_t i = 0; i < model_witness.size(); i++) {
@@ -439,7 +439,7 @@ TEST(standard_circuit, optimized_logic_witness)
 
 // Check that witness provided by the solver is the same as builder's witness
 // Check that all the optimized out values are initialized and computed properly during post proccessing
-TEST(standard_circuit, optimized_shr_witness)
+TEST(Standard_circuit, optimized_shr_witness)
 {
     StandardCircuitBuilder builder;
     uint_ct a = witness_t(&builder, engine.get_random_uint32());
@@ -456,7 +456,7 @@ TEST(standard_circuit, optimized_shr_witness)
     circuit["a"] == a.get_value();
     bool res = smt_timer(&s);
     ASSERT_TRUE(res);
-    auto model_witness = default_model_single({ "a" }, circuit, "optimized_xor_check.out");
+    auto model_witness = default_model_single({ "a" }, circuit, "tmp.out");
 
     ASSERT_EQ(model_witness.size(), builder.get_num_variables());
     for (size_t i = 0; i < model_witness.size(); i++) {
@@ -466,7 +466,7 @@ TEST(standard_circuit, optimized_shr_witness)
 
 // Check that witness provided by the solver is the same as builder's witness
 // Check that all the optimized out values are initialized and computed properly during post proccessing
-TEST(standard_circuit, optimized_shl_witness)
+TEST(Standard_circuit, optimized_shl_witness)
 {
     StandardCircuitBuilder builder;
     uint_ct a = witness_t(&builder, engine.get_random_uint32());
@@ -483,7 +483,7 @@ TEST(standard_circuit, optimized_shl_witness)
     circuit[a.get_witness_index()] == a.get_value();
     bool res = smt_timer(&s);
     ASSERT_TRUE(res);
-    auto model_witness = default_model_single({ "a" }, circuit, "optimized_xor_check.out");
+    auto model_witness = default_model_single({ "a" }, circuit, "tmp.out");
 
     ASSERT_EQ(model_witness.size(), builder.get_num_variables());
     for (size_t i = 0; i < model_witness.size(); i++) {
@@ -493,7 +493,7 @@ TEST(standard_circuit, optimized_shl_witness)
 
 // Check that witness provided by the solver is the same as builder's witness
 // Check that all the optimized out values are initialized and computed properly during post proccessing
-TEST(standard_circuit, optimized_ror_witness)
+TEST(Standard_circuit, optimized_ror_witness)
 {
     StandardCircuitBuilder builder;
     uint_ct a = witness_t(&builder, engine.get_random_uint32());
@@ -510,10 +510,10 @@ TEST(standard_circuit, optimized_ror_witness)
     circuit[a.get_witness_index()] == a.get_value();
     bool res = smt_timer(&s);
     ASSERT_TRUE(res);
-    auto model_witness = default_model_single({ "a" }, circuit, "optimized_xor_check.out");
+    auto model_witness = default_model_single({ "a" }, circuit, "tmp.out");
 
     ASSERT_EQ(model_witness.size(), builder.get_num_variables());
     for (size_t i = 0; i < model_witness.size(); i++) {
         EXPECT_EQ(model_witness[i], builder.variables[i]);
     }
-}
+}

barretenberg/cpp/src/barretenberg/smt_verification/circuit/subcircuits.cpp

@@ -5,7 +5,7 @@ namespace smt_subcircuits {
 CircuitProps get_standard_range_constraint_circuit(size_t n)
 {
     bb::StandardCircuitBuilder builder = bb::StandardCircuitBuilder();
-    uint32_t a_idx = builder.add_variable(bb::fr(0xabbba));
+    uint32_t a_idx = builder.add_variable(bb::fr(0));
     builder.set_variable_name(a_idx, "a");
 
     size_t start_gate = builder.get_estimated_num_finalized_gates();

barretenberg/cpp/src/barretenberg/smt_verification/circuit/subcircuits.test.cpp

@@ -10,13 +10,9 @@
 
 using namespace bb;
 
-namespace {
-auto& engine = numeric::get_debug_randomness();
-}
-
 // Check that all the relative offsets are calculated correctly.
 // I.e. I can find an operand at the index, given by get_standard_range_constraint_circuit
-TEST(subcircuits, range_circuit)
+TEST(Subcircuits, range_circuit)
 {
     for (size_t i = 1; i < 255; i++) {
         smt_subcircuits::CircuitProps range_props = smt_subcircuits::get_standard_range_constraint_circuit(i);
@@ -42,7 +38,7 @@ TEST(subcircuits, range_circuit)
 }
 // Check that all the relative offsets are calculated correctly.
 // I.e. I can find all three operands at the indices, given by get_standard_logic_circuit
-TEST(subcircuits, logic_circuit)
+TEST(Subcircuits, logic_circuit)
 {
     for (size_t i = 2; i < 256; i += 2) {
         smt_subcircuits::CircuitProps logic_props = smt_subcircuits::get_standard_logic_circuit(i, true);
@@ -71,7 +67,7 @@ TEST(subcircuits, logic_circuit)
 
 // Check that all the relative offsets are calculated correctly.
 // I.e. I can find all three operands at the indices, given by get_standard_logic_circuit
-TEST(subcircuits, ror_circuit)
+TEST(Subcircuits, ror_circuit)
 {
     for (uint32_t r = 1; r < 8; r += 1) {
         unsigned char n = 8;
@@ -149,7 +145,7 @@ TEST(subcircuits, ror_circuit)
 
 // Check that all the relative offsets are calculated correctly.
 // I.e. I can find all three operands at the indices, given by get_standard_logic_circuit
-TEST(subcircuits, shl_circuit)
+TEST(Subcircuits, shl_circuit)
 {
     for (uint32_t r = 1; r < 8; r += 1) {
         unsigned char n = 8;
@@ -230,7 +226,7 @@ TEST(subcircuits, shl_circuit)
 // I can't check the position of the lhs here, since shr doesn't use the witness directly but
 // it's accumulators.
 // However, according to standard_circuit test they seem fine.
-TEST(subcircuits, shr_circuit)
+TEST(Subcircuits, shr_circuit)
 {
     for (uint32_t r = 1; r < 8; r += 2) {
         unsigned char n = 8;