Skip to content

Commit

Permalink
Merge c474fb7 into 74e8443
Browse files Browse the repository at this point in the history
  • Loading branch information
@Sarkoxed
Sarkoxed authored Dec 7, 2024
2 parents 74e8443 + c474fb7 commit fbc1d94
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 fbc1d94

Please sign in to comment.