feat: Several Updates in SMT verification module (part 1)

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

@@ -41,6 +41,12 @@ class CircuitBase {
     std::unordered_map<SubcircuitType, std::unordered_map<size_t, CircuitProps>>
         cached_subcircuits; // caches subcircuits during optimization
                             // No need to recompute them each time
+    std::unordered_map<uint32_t, std::vector<bb::fr>>
+        post_process; // Values idxs that should be post processed after the solver returns a witness.
+                      // Basically it affects only optimized out variables.
+                      // Because in BitVector case we can't collect negative values since they will not be
+                      // the same in the field. That's why we store the expression and calculate it after the witness is
+                      // obtained.
 
     Solver* solver; // pointer to the solver
     TermType type;  // Type of the underlying Symbolic Terms

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

@@ -33,6 +33,7 @@ struct CircuitSchema {
     std::vector<std::vector<std::vector<bb::fr>>> lookup_tables;
     std::vector<uint32_t> real_variable_tags;
     std::unordered_map<uint32_t, uint64_t> range_tags;
+    bool circuit_finalized;
     MSGPACK_FIELDS(modulus,
                    public_inps,
                    vars_of_interest,

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

@@ -376,3 +376,144 @@ TEST(standard_circuit, check_double_xor_bug)
     Solver s(circuit_info.modulus, default_solver_config, 16, 64);
     StandardCircuit circuit(circuit_info, &s, TermType::BVTerm);
 }
+
+// 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)
+{
+    uint32_t rbit = engine.get_random_uint8() & 1;
+    uint32_t num_bits = 32 + rbit;
+    info(num_bits);
+
+    StandardCircuitBuilder builder;
+    field_t a = witness_t(&builder, engine.get_random_uint256() % (uint256_t(1) << num_bits));
+    builder.create_range_constraint(a.get_witness_index(), num_bits);
+    builder.set_variable_name(a.get_witness_index(), "a");
+
+    CircuitSchema circuit_info = unpack_from_buffer(builder.export_circuit());
+    Solver s(circuit_info.modulus, default_solver_config, 16, 64);
+    StandardCircuit circuit(circuit_info, &s, TermType::BVTerm);
+
+    circuit["a"] == a.get_value();
+
+    bool res = smt_timer(&s);
+    ASSERT_TRUE(res);
+    auto model_witness = default_model_single({ "a" }, circuit, "optimized_range_check.out");
+
+    ASSERT_EQ(model_witness.size(), builder.get_num_variables());
+    for (size_t i = 0; i < model_witness.size(); i++) {
+        ASSERT_EQ(model_witness[i], builder.variables[i]);
+    }
+}
+
+// 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)
+{
+    StandardCircuitBuilder builder;
+    uint_ct a = witness_t(&builder, engine.get_random_uint32());
+    builder.set_variable_name(a.get_witness_index(), "a");
+    uint_ct b = witness_t(&builder, engine.get_random_uint32());
+    builder.set_variable_name(b.get_witness_index(), "b");
+    uint_ct c = a ^ b;
+    uint_ct d = a & b;
+    builder.set_variable_name(c.get_witness_index(), "c");
+    builder.set_variable_name(d.get_witness_index(), "d");
+
+    CircuitSchema circuit_info = unpack_from_buffer(builder.export_circuit());
+    Solver s(circuit_info.modulus, default_solver_config, 16, 64);
+    StandardCircuit circuit(circuit_info, &s, TermType::BVTerm);
+
+    circuit["a"] == a.get_value();
+    circuit["b"] == b.get_value();
+
+    bool res = smt_timer(&s);
+    ASSERT_TRUE(res);
+    auto model_witness = default_model_single({ "a", "b", "c", "d" }, circuit, "optimized_xor_check.out");
+
+    ASSERT_EQ(model_witness.size(), builder.get_num_variables());
+    for (size_t i = 0; i < model_witness.size(); i++) {
+        ASSERT_EQ(model_witness[i], builder.variables[i]);
+    }
+}
+
+// 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)
+{
+    StandardCircuitBuilder builder;
+    uint_ct a = witness_t(&builder, engine.get_random_uint32());
+    builder.set_variable_name(a.get_witness_index(), "a");
+    uint_ct b = a >> 0;
+    for (uint32_t i = 1; i < 32; i++) {
+        b = a >> i;
+    }
+
+    CircuitSchema circuit_info = unpack_from_buffer(builder.export_circuit());
+    Solver s(circuit_info.modulus, default_solver_config, 16, 64);
+    StandardCircuit circuit(circuit_info, &s, TermType::BVTerm);
+
+    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");
+
+    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]);
+    }
+}
+
+// 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)
+{
+    StandardCircuitBuilder builder;
+    uint_ct a = witness_t(&builder, engine.get_random_uint32());
+    builder.set_variable_name(a.get_witness_index(), "a");
+    uint_ct b = a << 0;
+    for (uint32_t i = 1; i < 32; i++) {
+        b = a << i;
+    }
+
+    CircuitSchema circuit_info = unpack_from_buffer(builder.export_circuit());
+    Solver s(circuit_info.modulus, default_solver_config, 16, 64);
+    StandardCircuit circuit(circuit_info, &s, TermType::BVTerm);
+
+    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");
+
+    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]);
+    }
+}
+
+// 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)
+{
+    StandardCircuitBuilder builder;
+    uint_ct a = witness_t(&builder, engine.get_random_uint32());
+    builder.set_variable_name(a.get_witness_index(), "a");
+    uint_ct b = a.ror(0);
+    for (uint32_t i = 1; i < 32; i++) {
+        b = a.ror(i);
+    }
+
+    CircuitSchema circuit_info = unpack_from_buffer(builder.export_circuit());
+    Solver s(circuit_info.modulus, default_solver_config, 16, 64);
+    StandardCircuit circuit(circuit_info, &s, TermType::BVTerm);
+
+    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");
+
+    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/terms/bvterm.test.cpp

@@ -18,8 +18,8 @@ using namespace smt_terms;
 TEST(BVTerm, addition)
 {
     StandardCircuitBuilder builder;
-    uint_ct a = witness_ct(&builder, static_cast<uint32_t>(fr::random_element()));
-    uint_ct b = witness_ct(&builder, static_cast<uint32_t>(fr::random_element()));
+    uint_ct a = witness_ct(&builder, engine.get_random_uint32());
+    uint_ct b = witness_ct(&builder, engine.get_random_uint32());
     uint_ct c = a + b;
 
     uint32_t modulus_base = 16;
@@ -47,8 +47,8 @@ TEST(BVTerm, addition)
 TEST(BVTerm, subtraction)
 {
     StandardCircuitBuilder builder;
-    uint_ct a = witness_ct(&builder, static_cast<uint32_t>(fr::random_element()));
-    uint_ct b = witness_ct(&builder, static_cast<uint32_t>(fr::random_element()));
+    uint_ct a = witness_ct(&builder, engine.get_random_uint32());
+    uint_ct b = witness_ct(&builder, engine.get_random_uint32());
     uint_ct c = a - b;
 
     uint32_t modulus_base = 16;
@@ -76,8 +76,8 @@ TEST(BVTerm, subtraction)
 TEST(BVTerm, xor)
 {
     StandardCircuitBuilder builder;
-    uint_ct a = witness_ct(&builder, static_cast<uint32_t>(fr::random_element()));
-    uint_ct b = witness_ct(&builder, static_cast<uint32_t>(fr::random_element()));
+    uint_ct a = witness_ct(&builder, engine.get_random_uint32());
+    uint_ct b = witness_ct(&builder, engine.get_random_uint32());
     uint_ct c = a ^ b;
 
     uint32_t modulus_base = 16;
@@ -105,7 +105,7 @@ TEST(BVTerm, xor)
 TEST(BVTerm, rotr)
 {
     StandardCircuitBuilder builder;
-    uint_ct a = witness_ct(&builder, static_cast<uint32_t>(fr::random_element()));
+    uint_ct a = witness_ct(&builder, engine.get_random_uint32());
     uint_ct b = a.ror(10);
 
     uint32_t modulus_base = 16;
@@ -131,7 +131,7 @@ TEST(BVTerm, rotr)
 TEST(BVTerm, rotl)
 {
     StandardCircuitBuilder builder;
-    uint_ct a = witness_ct(&builder, static_cast<uint32_t>(fr::random_element()));
+    uint_ct a = witness_ct(&builder, engine.get_random_uint32());
     uint_ct b = a.rol(10);
 
     uint32_t modulus_base = 16;
@@ -158,8 +158,8 @@ TEST(BVTerm, rotl)
 TEST(BVTerm, mul)
 {
     StandardCircuitBuilder builder;
-    uint_ct a = witness_ct(&builder, static_cast<uint32_t>(fr::random_element()));
-    uint_ct b = witness_ct(&builder, static_cast<uint32_t>(fr::random_element()));
+    uint_ct a = witness_ct(&builder, engine.get_random_uint32());
+    uint_ct b = witness_ct(&builder, engine.get_random_uint32());
     uint_ct c = a * b;
 
     uint32_t modulus_base = 16;
@@ -187,8 +187,8 @@ TEST(BVTerm, mul)
 TEST(BVTerm, and)
 {
     StandardCircuitBuilder builder;
-    uint_ct a = witness_ct(&builder, static_cast<uint32_t>(fr::random_element()));
-    uint_ct b = witness_ct(&builder, static_cast<uint32_t>(fr::random_element()));
+    uint_ct a = witness_ct(&builder, engine.get_random_uint32());
+    uint_ct b = witness_ct(&builder, engine.get_random_uint32());
     uint_ct c = a & b;
 
     uint32_t modulus_base = 16;
@@ -216,8 +216,8 @@ TEST(BVTerm, and)
 TEST(BVTerm, or)
 {
     StandardCircuitBuilder builder;
-    uint_ct a = witness_ct(&builder, static_cast<uint32_t>(fr::random_element()));
-    uint_ct b = witness_ct(&builder, static_cast<uint32_t>(fr::random_element()));
+    uint_ct a = witness_ct(&builder, engine.get_random_uint32());
+    uint_ct b = witness_ct(&builder, engine.get_random_uint32());
     uint_ct c = a | b;
 
     uint32_t modulus_base = 16;
@@ -245,8 +245,8 @@ TEST(BVTerm, or)
 TEST(BVTerm, div)
 {
     StandardCircuitBuilder builder;
-    uint_ct a = witness_ct(&builder, static_cast<uint32_t>(fr::random_element()));
-    uint_ct b = witness_ct(&builder, static_cast<uint32_t>(fr::random_element()));
+    uint_ct a = witness_ct(&builder, engine.get_random_uint32());
+    uint_ct b = witness_ct(&builder, engine.get_random_uint32());
     uint_ct c = a / b;
 
     uint32_t modulus_base = 16;
@@ -274,7 +274,7 @@ TEST(BVTerm, div)
 TEST(BVTerm, shr)
 {
     StandardCircuitBuilder builder;
-    uint_ct a = witness_ct(&builder, static_cast<uint32_t>(fr::random_element()));
+    uint_ct a = witness_ct(&builder, engine.get_random_uint32());
     uint_ct b = a >> 5;
 
     uint32_t modulus_base = 16;
@@ -300,7 +300,7 @@ TEST(BVTerm, shr)
 TEST(BVTerm, shl)
 {
     StandardCircuitBuilder builder;
-    uint_ct a = witness_ct(&builder, static_cast<uint32_t>(fr::random_element()));
+    uint_ct a = witness_ct(&builder, engine.get_random_uint32());
     uint_ct b = a << 5;
 
     uint32_t modulus_base = 16;

barretenberg/cpp/src/barretenberg/smt_verification/terms/iterm.test.cpp

@@ -17,8 +17,8 @@ using namespace smt_terms;
 TEST(ITerm, addition)
 {
     StandardCircuitBuilder builder;
-    uint64_t a = static_cast<uint32_t>(fr::random_element()) % (static_cast<uint32_t>(1) << 31);
-    uint64_t b = static_cast<uint32_t>(fr::random_element()) % (static_cast<uint32_t>(1) << 31);
+    uint64_t a = engine.get_random_uint32() % (static_cast<uint32_t>(1) << 31);
+    uint64_t b = engine.get_random_uint32() % (static_cast<uint32_t>(1) << 31);
     uint64_t c = a + b;
 
     Solver s("30644e72e131a029b85045b68181585d2833e84879b9709143e1f593f0000001", default_solver_config);
@@ -41,8 +41,8 @@ TEST(ITerm, addition)
 TEST(ITerm, subtraction)
 {
     StandardCircuitBuilder builder;
-    uint64_t c = static_cast<uint32_t>(fr::random_element()) % (static_cast<uint32_t>(1) << 31);
-    uint64_t b = static_cast<uint32_t>(fr::random_element()) % (static_cast<uint32_t>(1) << 31);
+    uint64_t c = engine.get_random_uint32() % (static_cast<uint32_t>(1) << 31);
+    uint64_t b = engine.get_random_uint32() % (static_cast<uint32_t>(1) << 31);
     uint64_t a = c + b;
 
     Solver s("30644e72e131a029b85045b68181585d2833e84879b9709143e1f593f0000001", default_solver_config);
@@ -65,8 +65,8 @@ TEST(ITerm, subtraction)
 TEST(ITerm, mul)
 {
     StandardCircuitBuilder builder;
-    uint64_t a = static_cast<uint32_t>(fr::random_element()) % (static_cast<uint32_t>(1) << 31);
-    uint64_t b = static_cast<uint32_t>(fr::random_element()) % (static_cast<uint32_t>(1) << 31);
+    uint64_t a = engine.get_random_uint32() % (static_cast<uint32_t>(1) << 31);
+    uint64_t b = engine.get_random_uint32() % (static_cast<uint32_t>(1) << 31);
     uint64_t c = a * b;
 
     Solver s("30644e72e131a029b85045b68181585d2833e84879b9709143e1f593f0000001", default_solver_config);
@@ -89,8 +89,8 @@ TEST(ITerm, mul)
 TEST(ITerm, div)
 {
     StandardCircuitBuilder builder;
-    uint64_t a = static_cast<uint32_t>(fr::random_element()) % (static_cast<uint32_t>(1) << 31);
-    uint64_t b = static_cast<uint32_t>(fr::random_element()) % (static_cast<uint32_t>(1) << 31) + 1;
+    uint64_t a = engine.get_random_uint32() % (static_cast<uint32_t>(1) << 31);
+    uint64_t b = engine.get_random_uint32() % (static_cast<uint32_t>(1) << 31) + 1;
     uint64_t c = a / b;
 
     Solver s("30644e72e131a029b85045b68181585d2833e84879b9709143e1f593f0000001", default_solver_config);