-
Notifications
You must be signed in to change notification settings - Fork 240
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
feat: Several updates in SMT verification module (#7105)
This pr adds several new features to SMT verification module + fixes some bugs: ## meta updated `README.md` so now it matches the current state of the directory ## UltraCircuit - Added an optimization to lookups: now plookup accumulators are connected via `>>`. Without this constraint it produced unique witness that was overflowing over the bitlength. - Now the range constrained values are not optimized out by the solver. - `unique_witness` and `unique_witness_ext` now have `bool optimizations` argument like `Standard` ones. ## Solver - improved `print_assertions` method. Now sets are handled properly. ## BVTerm - Added unsigned division operation + tests ## STerm - Added new symbolic term type: `ITerm`. These are ordinary integers. + tests - Changed `mod()` method behavior. Now it returns the value that is modded instead of modifying the current term. - fixed several `mod` related methods for `FFITerm` ## `smt_util.cpp` Added a function `fix_range_lists(UltraCircuitBuilder& builder)` that fixes the witness by adding proper values into range lists. --------- Co-authored-by: Innokentii Sennovskii <[email protected]>
- Loading branch information
Showing
11 changed files
with
445 additions
and
128 deletions.
There are no files selected for viewing
166 changes: 121 additions & 45 deletions
166
barretenberg/cpp/src/barretenberg/smt_verification/README.md
Large diffs are not rendered by default.
Oops, something went wrong.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
149 changes: 149 additions & 0 deletions
149
barretenberg/cpp/src/barretenberg/smt_verification/terms/iterm.test.cpp
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,149 @@ | ||
| #include <unordered_map> | ||
|
|
||
| #include "barretenberg/stdlib/primitives/uint/uint.hpp" | ||
| #include "term.hpp" | ||
|
|
||
| #include <gtest/gtest.h> | ||
|
|
||
| namespace { | ||
| auto& engine = bb::numeric::get_debug_randomness(); | ||
| } | ||
|
|
||
| using namespace bb; | ||
| using witness_ct = stdlib::witness_t<StandardCircuitBuilder>; | ||
|
|
||
| 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 c = a + b; | ||
|
|
||
| Solver s("30644e72e131a029b85045b68181585d2833e84879b9709143e1f593f0000001", default_solver_config); | ||
|
|
||
| STerm x = IVar("x", &s); | ||
| STerm y = IVar("y", &s); | ||
| STerm z = x + y; | ||
|
|
||
| z == c; | ||
| x == a; | ||
| ASSERT_TRUE(s.check()); | ||
|
|
||
| std::string yvals = s.getValue(y.term).getIntegerValue(); | ||
|
|
||
| STerm bval = STerm(b, &s, TermType::ITerm); | ||
| std::string bvals = s.getValue(bval.term).getIntegerValue(); | ||
| ASSERT_EQ(bvals, yvals); | ||
| } | ||
|
|
||
| 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 a = c + b; | ||
|
|
||
| Solver s("30644e72e131a029b85045b68181585d2833e84879b9709143e1f593f0000001", default_solver_config); | ||
|
|
||
| STerm x = IVar("x", &s); | ||
| STerm y = IVar("y", &s); | ||
| STerm z = x - y; | ||
|
|
||
| x == a; | ||
| z == c; | ||
| ASSERT_TRUE(s.check()); | ||
|
|
||
| std::string yvals = s.getValue(y.term).getIntegerValue(); | ||
|
|
||
| STerm bval = STerm(b, &s, TermType::ITerm); | ||
| std::string bvals = s.getValue(bval.term).getIntegerValue(); | ||
| ASSERT_EQ(bvals, yvals); | ||
| } | ||
|
|
||
| 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 c = a * b; | ||
|
|
||
| Solver s("30644e72e131a029b85045b68181585d2833e84879b9709143e1f593f0000001", default_solver_config); | ||
|
|
||
| STerm x = IVar("x", &s); | ||
| STerm y = IVar("y", &s); | ||
| STerm z = x * y; | ||
|
|
||
| x == a; | ||
| y == b; | ||
|
|
||
| ASSERT_TRUE(s.check()); | ||
|
|
||
| std::string xvals = s.getValue(z.term).getIntegerValue(); | ||
| STerm bval = STerm(c, &s, TermType::ITerm); | ||
| std::string bvals = s.getValue(bval.term).getIntegerValue(); | ||
| ASSERT_EQ(bvals, xvals); | ||
| } | ||
|
|
||
| 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 c = a / b; | ||
|
|
||
| Solver s("30644e72e131a029b85045b68181585d2833e84879b9709143e1f593f0000001", default_solver_config); | ||
|
|
||
| STerm x = IVar("x", &s); | ||
| STerm y = IVar("y", &s); | ||
| STerm z = x / y; | ||
|
|
||
| x == a; | ||
| y == b; | ||
|
|
||
| ASSERT_TRUE(s.check()); | ||
|
|
||
| std::string xvals = s.getValue(z.term).getIntegerValue(); | ||
| STerm bval = STerm(c, &s, TermType::ITerm); | ||
| std::string bvals = s.getValue(bval.term).getIntegerValue(); | ||
| ASSERT_EQ(bvals, xvals); | ||
| } | ||
|
|
||
| // This test aims to check for the absence of unintended | ||
| // behavior. If an unsupported operator is called, an info message appears in stderr | ||
| // and the value is supposed to remain unchanged. | ||
| TEST(ITerm, unsupported_operations) | ||
| { | ||
| Solver s("30644e72e131a029b85045b68181585d2833e84879b9709143e1f593f0000001"); | ||
|
|
||
| STerm x = IVar("x", &s); | ||
| STerm y = IVar("y", &s); | ||
|
|
||
| STerm z = x ^ y; | ||
| ASSERT_EQ(z.term, x.term); | ||
| z = x & y; | ||
| ASSERT_EQ(z.term, x.term); | ||
| z = x | y; | ||
| ASSERT_EQ(z.term, x.term); | ||
| z = x >> 10; | ||
| ASSERT_EQ(z.term, x.term); | ||
| z = x << 10; | ||
| ASSERT_EQ(z.term, x.term); | ||
| z = x.rotr(10); | ||
| ASSERT_EQ(z.term, x.term); | ||
| z = x.rotl(10); | ||
| ASSERT_EQ(z.term, x.term); | ||
|
|
||
| cvc5::Term before_term = x.term; | ||
| x ^= y; | ||
| ASSERT_EQ(x.term, before_term); | ||
| x &= y; | ||
| ASSERT_EQ(x.term, before_term); | ||
| x |= y; | ||
| ASSERT_EQ(x.term, before_term); | ||
| x >>= 10; | ||
| ASSERT_EQ(x.term, before_term); | ||
| x <<= 10; | ||
| ASSERT_EQ(x.term, before_term); | ||
| } |
Oops, something went wrong.
41b21f1There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Possible performance regression was detected for benchmark 'C++ Benchmark'.
Benchmark result of this commit is worse than the previous benchmark result exceeding threshold
1.05.nativeconstruct_proof_ultrahonk_power_of_2/205935.6478830000015ms/iter5534.598031000001ms/iter1.07This comment was automatically generated by workflow using github-action-benchmark.
CC: @ludamad @codygunton