fix: smt_verification: negative bitvecs, changed gates indicies. acir_formal_proofs: noir-style signed division #11649
Conversation
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
jewelofchaos9
changed the title
Sarkoxed
requested changes
Feb 5, 2025
| @@ -30,18 +30,18 @@ UltraCircuit::UltraCircuit( | |||
| // add gate in its normal state to solver | |||
|
|
|||
| size_t arith_cursor = 0; | |||
| while (arith_cursor < this->selectors[1].size()) { | |||
There was a problem hiding this comment.
Please add an entry to ultra_circuit.hpp with the changed indices
There was a problem hiding this comment.
Regarding the pow2_8, you should use bit_extraction rather then direct & 1 value
| smt_circuit::STerm shl64(smt_circuit::STerm v0, smt_circuit::STerm v1, smt_solver::Solver* solver) | ||
| { | ||
| auto shifted = shl(v0, v1, solver); | ||
| // 2^64 - 1 | ||
| auto mask = smt_terms::BVConst("18446744073709551615", solver, 10); | ||
| auto res = shifted & mask; | ||
| /*auto mask = smt_terms::BVConst("18446744073709551615", solver, 10); |
There was a problem hiding this comment.
are these comments necessary?
Sarkoxed
requested changes
Feb 5, 2025
|
|
||
| TEST(helpers, signed_div_2) | ||
| { | ||
| // using smt solver i found that 1879048194 >> 16 == 0 |
There was a problem hiding this comment.
it was bug in my implementation
| @@ -89,4 +89,87 @@ TEST(helpers, pow2) | |||
| info("z = ", vals["z"]); | |||
| // z == 2048 in binary | |||
| EXPECT_TRUE(vals["z"] == "00000000000000000000100000000000"); | |||
| } | |||
|
|
|||
There was a problem hiding this comment.
Leave a few comments what are these tests doing
| @@ -429,6 +429,35 @@ STerm STerm::rotl(const uint32_t& n) const | |||
| return { res, this->solver, this->type }; | |||
| } | |||
|
|
|||
| STerm STerm::truncate(const uint32_t& to_size) | |||
There was a problem hiding this comment.
Could you please add a test and update README.md with these new methods?
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Negative bitvector values didnt parse properly