fix: smt_verification: negative bitvecs, changed gates indicies. acir_formal_proofs: noir-style signed division

barretenberg/cpp/src/barretenberg/acir_formal_proofs/formal_proofs.cpp

@@ -269,4 +269,19 @@ bool verify_gt(smt_solver::Solver* solver, smt_circuit::UltraCircuit circuit)
         debug_solution(solver, terms);
     }
     return res;
+}
+
+bool verify_idiv(smt_solver::Solver* solver, smt_circuit::UltraCircuit circuit, uint32_t bit_size)
+{
+    auto a = circuit["a"];
+    auto b = circuit["b"];
+    auto c = circuit["c"];
+    auto cr = idiv(a, b, bit_size, solver);
+    c != cr;
+    bool res = solver->check();
+    if (res) {
+        std::unordered_map<std::string, cvc5::Term> terms({ { "a", a }, { "b", b }, { "c", c }, { "cr", cr } });
+        debug_solution(solver, terms);
+    }
+    return res;
 }

barretenberg/cpp/src/barretenberg/acir_formal_proofs/helpers.cpp

@@ -47,17 +47,37 @@ smt_circuit::STerm shr(smt_circuit::STerm v0, smt_circuit::STerm v1, smt_solver:
 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 res = shifted.truncate(63);
     return res;
 }
 
 smt_circuit::STerm shl32(smt_circuit::STerm v0, smt_circuit::STerm v1, smt_solver::Solver* solver)
 {
     auto shifted = shl(v0, v1, solver);
-    // 2^32 - 1
-    auto mask = smt_terms::BVConst("4294967295", solver, 10);
-    auto res = shifted & mask;
+    auto res = shifted.truncate(31);
     return res;
 }
+
+smt_circuit::STerm idiv(smt_circuit::STerm v0, smt_circuit::STerm v1, uint32_t bit_size, smt_solver::Solver* solver)
+{
+    // highest bit of v0 and v1 is sign bit
+    smt_circuit::STerm exponent = smt_terms::BVConst(std::to_string(bit_size), solver, 10);
+    auto sign_bit_v0 = v0.extract_bit(bit_size - 1);
+    auto sign_bit_v1 = v1.extract_bit(bit_size - 1);
+    auto res_sign_bit = sign_bit_v0 ^ sign_bit_v1;
+    res_sign_bit <<= bit_size - 1;
+    auto abs_value_v0 = v0.truncate(bit_size - 2);
+    auto abs_value_v1 = v1.truncate(bit_size - 2);
+    auto abs_res = abs_value_v0 / abs_value_v1;
+
+    // if abs_value_v0 == 0 then res = 0
+    // in our context we use idiv only once, so static name for the division result okay.
+    auto res = smt_terms::BVVar("res_signed_division", solver);
+    auto condition = smt_terms::Bool(abs_value_v0, solver) == smt_terms::Bool(smt_terms::BVConst("0", solver, 10));
+    auto eq1 = condition & (smt_terms::Bool(res, solver) == smt_terms::Bool(smt_terms::BVConst("0", solver, 10)));
+    auto eq2 = !condition & (smt_terms::Bool(res, solver) == smt_terms::Bool(res_sign_bit | abs_res, solver));
+
+    (eq1 | eq2).assert_term();
+
+    return res;
+}

barretenberg/cpp/src/barretenberg/acir_formal_proofs/helpers.hpp

@@ -44,4 +44,14 @@ smt_circuit::STerm shr(smt_circuit::STerm v0, smt_circuit::STerm v1, smt_solver:
  * @param solver SMT solver instance
  * @return Result of (v0 << v1) without truncation
  */
-smt_circuit::STerm shl(smt_circuit::STerm v0, smt_circuit::STerm v1, smt_solver::Solver* solver);
+smt_circuit::STerm shl(smt_circuit::STerm v0, smt_circuit::STerm v1, smt_solver::Solver* solver);
+
+/**
+ * @brief Signed division in noir-style
+ * @param v0 Numerator
+ * @param v1 Denominator
+ * @param bit_size bit sizes of numerator and denominator
+ * @param solver SMT solver instance
+ * @return Result of (v0 / v1)
+ */
+smt_circuit::STerm idiv(smt_circuit::STerm v0, smt_circuit::STerm v1, uint32_t bit_size, smt_solver::Solver* solver);

barretenberg/cpp/src/barretenberg/acir_formal_proofs/helpers.test.cpp

@@ -12,6 +12,10 @@ using uint_ct = stdlib::uint32<StandardCircuitBuilder>;
 
 using namespace smt_terms;
 
+/**
+ * @brief Test left shift operation
+ * Tests that 5 << 1 = 10 using SMT solver
+ */
 TEST(helpers, shl)
 {
     Solver s("30644e72e131a029b85045b68181585d2833e84879b9709143e1f593f0000001", default_solver_config, 16, 32);
@@ -32,6 +36,10 @@ TEST(helpers, shl)
     EXPECT_TRUE(vals["z"] == "00000000000000000000000000001010");
 }
 
+/**
+ * @brief Test right shift operation
+ * Tests that 5 >> 1 = 2 using SMT solver
+ */
 TEST(helpers, shr)
 {
     Solver s("30644e72e131a029b85045b68181585d2833e84879b9709143e1f593f0000001", default_solver_config, 16, 32);
@@ -52,6 +60,10 @@ TEST(helpers, shr)
     EXPECT_TRUE(vals["z"] == "00000000000000000000000000000010");
 }
 
+/**
+ * @brief Test edge case for right shift operation
+ * Tests that 1879048194 >> 16 = 28672 using SMT solver
+ */
 TEST(helpers, buggy_shr)
 {
     // using smt solver i found that 1879048194 >> 16 == 0
@@ -74,6 +86,10 @@ TEST(helpers, buggy_shr)
     EXPECT_TRUE(vals["z"] == "00000000000000000111000000000000");
 }
 
+/**
+ * @brief Test power of 2 calculation
+ * Tests that 2^11 = 2048 using SMT solver
+ */
 TEST(helpers, pow2)
 {
     Solver s("30644e72e131a029b85045b68181585d2833e84879b9709143e1f593f0000001", default_solver_config, 16, 32);
@@ -89,4 +105,99 @@ TEST(helpers, pow2)
     info("z = ", vals["z"]);
     // z == 2048 in binary
     EXPECT_TRUE(vals["z"] == "00000000000000000000100000000000");
+}
+
+/**
+ * @brief Test signed division with zero dividend
+ * Tests that 0 / -1 = 0 using SMT solver
+ */
+TEST(helpers, signed_div)
+{
+    Solver s("30644e72e131a029b85045b68181585d2833e84879b9709143e1f593f0000001", default_solver_config, 16, 32);
+
+    STerm x = BVVar("x", &s);
+    STerm y = BVVar("y", &s);
+    STerm z = idiv(x, y, 2, &s);
+    // 00 == 0
+    x == 0;
+    // 11 == -1
+    y == 3;
+    s.check();
+    std::unordered_map<std::string, cvc5::Term> terms({ { "x", x }, { "y", y }, { "z", z } });
+    std::unordered_map<std::string, std::string> vals = s.model(terms);
+    info("x = ", vals["x"]);
+    info("y = ", vals["y"]);
+    info("z = ", vals["z"]);
+    EXPECT_TRUE(vals["z"] == "00000000000000000000000000000000");
+}
+
+/**
+ * @brief Test signed division with positive dividend and negative divisor
+ * Tests that 1 / -1 = -1 using SMT solver
+ */
+TEST(helpers, signed_div_1)
+{
+    Solver s("30644e72e131a029b85045b68181585d2833e84879b9709143e1f593f0000001", default_solver_config, 16, 32);
+
+    STerm x = BVVar("x", &s);
+    STerm y = BVVar("y", &s);
+    STerm z = idiv(x, y, 2, &s);
+    // 01 == 1
+    x == 1;
+    // 11 == -1
+    y == 3;
+    s.check();
+    std::unordered_map<std::string, cvc5::Term> terms({ { "x", x }, { "y", y }, { "z", z } });
+    std::unordered_map<std::string, std::string> vals = s.model(terms);
+    info("x = ", vals["x"]);
+    info("y = ", vals["y"]);
+    info("z = ", vals["z"]);
+    EXPECT_TRUE(vals["z"] == "00000000000000000000000000000011");
+}
+
+/**
+ * @brief Test signed division with positive numbers
+ * Tests that 7 / 2 = 3 using SMT solver
+ */
+TEST(helpers, signed_div_2)
+{
+    Solver s("30644e72e131a029b85045b68181585d2833e84879b9709143e1f593f0000001", default_solver_config, 16, 32);
+
+    STerm x = BVVar("x", &s);
+    STerm y = BVVar("y", &s);
+    STerm z = idiv(x, y, 4, &s);
+    // 0111 == 7
+    x == 7;
+    // 0010 == 2
+    y == 2;
+    s.check();
+    std::unordered_map<std::string, cvc5::Term> terms({ { "x", x }, { "y", y }, { "z", z } });
+    std::unordered_map<std::string, std::string> vals = s.model(terms);
+    info("x = ", vals["x"]);
+    info("y = ", vals["y"]);
+    info("z = ", vals["z"]);
+    EXPECT_TRUE(vals["z"] == "00000000000000000000000000000011");
+}
+
+/**
+ * @brief Test left shift overflow behavior
+ * Tests that 1 << 50 = 0 (due to overflow) using SMT solver
+ */
+TEST(helpers, shl_overflow)
+{
+    Solver s("30644e72e131a029b85045b68181585d2833e84879b9709143e1f593f0000001", default_solver_config, 16, 32);
+
+    STerm x = BVVar("x", &s);
+    STerm y = BVVar("y", &s);
+    STerm z = shl32(x, y, &s);
+    x == 1;
+    y == 50;
+    s.check();
+    std::unordered_map<std::string, cvc5::Term> terms({ { "x", x }, { "y", y }, { "z", z } });
+    std::unordered_map<std::string, std::string> vals = s.model(terms);
+    info("x = ", vals["x"]);
+    info("y = ", vals["y"]);
+    info("z = ", vals["z"]);
+    // z == 1010 in binary
+    EXPECT_TRUE(vals["z"] == "00000000000000000000000000000000");
 }

barretenberg/cpp/src/barretenberg/smt_verification/README.md

@@ -24,7 +24,7 @@ To store it on the disk just do the following
 
 ```c++
     msgpack::sbuffer buffer = circuit.export_circuit();
-    
+
     std::fstream myfile;
     myfile.open("fname.pack", std::ios::out | std::ios::trunc | std::ios::binary);
 
@@ -44,7 +44,7 @@ To store it on the disk just do the following
 2. Initialize the Solver:
 
     There's an `smt_solver::SolverConfiguration` structure:
-    
+
     ```cpp
     struct SolverConfiguration {
         bool produce_models;
@@ -90,7 +90,7 @@ To store it on the disk just do the following
 
     All the tables are exoported directly from circuit, but if you want to create your own table, there're two methods for this:
 
-    - `Solver::create_table(vector<cvc5::Term>& table)` - creates a set of values. 
+    - `Solver::create_table(vector<cvc5::Term>& table)` - creates a set of values.
     - `Solver::create_lookup_table(vector<vector<cvc5::Term>>& table)` - creates a table with three columns.
 
     ```c++
@@ -101,13 +101,13 @@ To store it on the disk just do the following
 
     There is more on `FFConst` in the following sections.
 
-3. Initialize the Circuit 
+3. Initialize the Circuit
 
-	From now on we will use `smt_terms::STerm` and `smt_terms::Bool` types to operate inside the solver. 
+	From now on we will use `smt_terms::STerm` and `smt_terms::Bool` types to operate inside the solver.
 
     You can choose the behaviour of symbolic variables by providing the specific type to `STerm` or `Circuit` constructor:
 
-    - `smt_terms::TermType::FFTerm` - symbolic variables that simulate finite field arithmetic. 
+    - `smt_terms::TermType::FFTerm` - symbolic variables that simulate finite field arithmetic.
     - `smt_terms::TermType::FFITerm` - symbolic variables that simulate integer elements which behave like finite field ones. Useful, when you want to create range constraints. Bad, when you try multiplication.
     - `smt_terms::TermType::ITerm` - symbolic variables that simulate ordinary integer elements. Useful, when you want to create range constraints and operate with signed values that are not shrinked modulo smth.
     - `smt_terms::TermType::BVTerm` - symbolic variables that simulate $\pmod{2^n}$ arithmetic. Useful, when you test uint circuits. Supports range constraints and bitwise operations. Doesn't behave like finite field element.
@@ -117,13 +117,13 @@ To store it on the disk just do the following
     `Bool` - simulates the boolean values and mostly will be useful to simulate complex `if` statements if needed.
 
     Now we can create symbolic circuit
-	
+
     - ```smt_circuit::StandardCircuit circuit(CircuitSchema c_info, Solver* s, TermType type, str tag="", bool optimizations=true)```
     - ```smt_circuit::UltraCircuit circuit(CircuitSchema c_info, Solver* s, TermType type, str tag="", bool optimizations=true)```
-	
+
 	It will generate all the symbolic values of the circuit wires, add all the gate constrains, create a map `term_name->STerm` and the inverse of it. Where `term_name` is the name you provided earlier.
 
-    In case you want to create two similar circuits with the same `solver` and `schema`, then you should specify the `tag`(name) of a circuit. 
+    In case you want to create two similar circuits with the same `solver` and `schema`, then you should specify the `tag`(name) of a circuit.
 
     **Advanced** If you don't want the circuit optimizations to be applied then you should set `optimizations` to `false`. Optimizations interchange the complex circuits like bitwise XOR with simple XOR operation. More on optimizations can be found [standard_circuit.cpp](circuit/standard_circuit.cpp)
 
@@ -145,15 +145,15 @@ To store it on the disk just do the following
 	You can add, subtract and multiply these variables(including `+=`, `-=`, etc);
 	Also there are two functions:
 	- `batch_add(std::vector<STerm>& terms)`
-	- `batch_mul(std::vector<STerm>& terms)` 
+	- `batch_mul(std::vector<STerm>& terms)`
 
 	to create an addition/multiplication Term in one call
 
     `FFITerm` also can be used to create range constraints. e.g. `x <= bb::fr(2).pow(10) - 1;`
 
-    `BVTerm` can be used to create bitwise constraints. e.g. `STerm y = x^z` or `STerm y = x.rotr(10)`. And range constraints too.
+    `BVTerm` can be used to create bitwise constraints. e.g. `STerm y = x^z` or `STerm y = x.rotr(10)`. And range constraints too. Also there are `truncate` and `extract_bit` methods, e.g. `x.truncate(9)` will truncate to last 10 bits (starting from 0th bit), `x.extract_bit(10)` will extract 10th bit.
 
-	You can create a constraint `==` or `!=` that will be included directly into solver. e.g. `x == y;` 
+	You can create a constraint `==` or `!=` that will be included directly into solver. e.g. `x == y;`
 
     **!Note: In this case these are not comparison operators**
 
@@ -169,7 +169,7 @@ To store it on the disk just do the following
 
 	You can `|, &, ==, !=, !` these variables and also `batch_or`, `batch_and` them.
 	To create a constraint you should call `Bool::assert_term()` method.
-	
+
 	The way I see the use of Bool types is to create terms like `(a == b && c == 1) || (a != b && c == 0)`, `(a!=1)||(b!=2)|(c!=3)` and of course more sophisticated ones.
 
     **!Note that constraint like `(Bool(STerm a) == Bool(STerm b)).assert_term()`, where a has `FFTerm` type and b has `FFITerm` type, won't work, since their types differ.**
@@ -181,8 +181,8 @@ After generating all the constrains you should call `bool res = solver.check()`
 In case you expected `false` but `true` was returned you can then check what went wrong.
 You should generate an unordered map with `str->term` values and ask the solver to obtain `unoredered_map<str, str> res = solver.model(unordered_map<str, FFTerm> terms)`.
    Or you can provide a vector of terms that you want to check and the return map will contain their symbolic names that are given during initialization. Specifically either it's the name that you set or `var_{i}`.
-   
-Now you have the values of the specified terms, which resulted into `true` result. 
+
+Now you have the values of the specified terms, which resulted into `true` result.
 **!Note that the return values are decimal strings/binary strings**, so if you want to use them later you should use `FFConst` with base 10, etc.
 
 Also, there is a header file "barretenberg/smt_verification/utl/smt_util.hpp" that contains two useful functions:
@@ -191,22 +191,22 @@ Also, there is a header file "barretenberg/smt_verification/utl/smt_util.hpp" th
 
 These functions will write witness variables in c-like array format into file named `fname`.
 The vector of `special_names` is the values that you want ot see in stdout.
-`pack` argument tells this function to save an `msgpack` buffer of the witness on disk. Name of the file will be `fname`.pack 
+`pack` argument tells this function to save an `msgpack` buffer of the witness on disk. Name of the file will be `fname`.pack
 
 You can then import the saved witness using one of the following functions:
 
 - `vec<vec<fr>> import_witness(str fname)`
 - `vec<fr> import_witness_single(str fname)`
- 
+
 ## 4. Automated verification of a unique witness
-There's a static member of `StandardCircuit` and `UltraCircuit` 
+There's a static member of `StandardCircuit` and `UltraCircuit`
 
 - `pair<StandardCircuit, StandardCircuit> StandardCircuit::unique_wintes(CircuitSchema circuit_info, Solver*, TermType type, vector<str> equal, bool optimizations)`
 - `pair<UltraCircuit, UltraCircuit> UltraCircuit::unique_wintes(CircuitSchema circuit_info, Solver*, TermType type, vector<str> equal, bool optimizations)`
 
 They will create two separate circuits, constrain variables with names from `equal` to be equal acrosss the circuits, and set all the other variables to be not equal at the same time.
 
-Another one is 
+Another one is
 
 - `pair<StandardCircuit, StandardCircuit> StandardCircuit::unique_witness_ext(CircuitSchema circuit_info, Solver* s, TermType type, vector<str> equal_variables, vector<str> nequal_variables, vector<str> at_least_one_equal_variable, vector<str> at_least_one_nequal_variable)` that does the same but provides you with more flexible settings.
 - Same in `UltraCircuit`
@@ -372,9 +372,9 @@ void model_variables(SymCircuit& c, Solver* s, FFTerm& evaluation)
 ```
 
 
-More examples can be found in 
+More examples can be found in
 
 - [terms/ffterm.test.cpp](terms/ffterm.test.cpp), [terms/ffiterm.test.cpp](terms/ffiterm.test.cpp), [terms/bvterm.test.cpp](terms/bvterm.test.cpp), [terms/iterm.test.cpp](terms/iterm.test.cpp)
-- [circuit/standard_circuit.test.cpp](circuit/standard_circuit.test.cpp), [circuit/ultra_circuit](circuit/ultra_circuit.test.cpp) 
+- [circuit/standard_circuit.test.cpp](circuit/standard_circuit.test.cpp), [circuit/ultra_circuit](circuit/ultra_circuit.test.cpp)
 - [smt_polynomials.test.cpp](smt_polynomials.test.cpp), [smt_examples.test.cpp](smt_examples.test.cpp)
 - [bb_tests](bb_tests)