Skip to content

Commit

Permalink
feat: Several Updates in SMT verification module (part 1) (#10437)
Browse files Browse the repository at this point in the history 
This pr enhances symbolic circuit to produce valid witnesses. 

# Utils

Added post processing functionality. So now, while optimizing something
inside the circuit, you can postpone some witness calculations until
here, in case the variable has been optimized and does not fit as an
STerm.

# Builders + Schema

Added `circuit_finalized` flag to the export. Should be used in the
future, during RAM/ROM processing.

# StandardCircuit

Pushed the post processing for standard logic operations. They were used
to test the sha256 witness, which is coming in part 3, I guess.
  • Loading branch information
@Sarkoxed
Sarkoxed authored Dec 9, 2024
1 parent 623f3e2 commit 0c37672
Show file tree
Hide file tree
Showing 11 changed files with 414 additions and 77 deletions.
6 changes: 6 additions & 0 deletions barretenberg/cpp/src/barretenberg/smt_verification/circuit/circuit_base.hpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
1 change: 1 addition & 0 deletions barretenberg/cpp/src/barretenberg/smt_verification/circuit/circuit_schema.hpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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,
Expand Down
211 changes: 182 additions & 29 deletions barretenberg/cpp/src/barretenberg/smt_verification/circuit/standard_circuit.cpp
View file

Large diffs are not rendered by default.

141 changes: 141 additions & 0 deletions barretenberg/cpp/src/barretenberg/smt_verification/circuit/standard_circuit.test.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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]);
}
}
36 changes: 18 additions & 18 deletions barretenberg/cpp/src/barretenberg/smt_verification/terms/bvterm.test.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down Expand Up @@ -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;
Expand Down Expand Up @@ -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;
Expand Down Expand Up @@ -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;
Expand All @@ -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;
Expand All @@ -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;
Expand Down Expand Up @@ -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;
Expand Down Expand Up @@ -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;
Expand Down Expand Up @@ -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;
Expand Down Expand Up @@ -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;
Expand All @@ -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;
Expand Down
16 changes: 8 additions & 8 deletions barretenberg/cpp/src/barretenberg/smt_verification/terms/iterm.test.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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);
Expand All @@ -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);
Expand All @@ -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);
Expand All @@ -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);
Expand Down
Loading

0 comments on commit 0c37672

Please sign in to comment.