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

@@ -44,20 +44,51 @@ smt_circuit::STerm shr(smt_circuit::STerm v0, smt_circuit::STerm v1, smt_solver:
     return res;
 }
 
+smt_circuit::STerm truncate(smt_circuit::STerm v0, uint32_t bit_size, smt_solver::Solver* solver)
+{
+    smt_circuit::STerm power = smt_terms::BVConst(std::to_string(bit_size), solver, 10);
+    auto mask = pow2_8(power, solver);
+    return v0 & (mask - 1);
+}
+
 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);
+    auto res = shifted & mask;*/
+    auto res = truncate(shifted, 64, solver);
     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 = truncate(shifted, 32, solver);
     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);
+    // because pow(2, 0) == 1
+    auto mask_abs_value = pow2_8(exponent - 1, solver);
+    auto sign_bit_v0 = v0 & mask_abs_value;
+    auto sign_bit_v1 = v1 & mask_abs_value;
+    auto res_sign_bit = sign_bit_v0 ^ sign_bit_v1;
+    auto abs_value_v0 = truncate(v0, bit_size - 1, solver);
+    auto abs_value_v1 = truncate(v1, bit_size - 1, solver);
+    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/smt_verification/circuit/ultra_circuit.cpp

@@ -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()) {
-        arith_cursor = this->handle_arithmetic_relation(arith_cursor, 1);
+    while (arith_cursor < this->selectors[2].size()) {
+        arith_cursor = this->handle_arithmetic_relation(arith_cursor, 2);
     }
 
     size_t lookup_cursor = 0;
-    while (lookup_cursor < this->selectors[5].size()) {
-        lookup_cursor = this->handle_lookup_relation(lookup_cursor, 5);
+    while (lookup_cursor < this->selectors[1].size()) {
+        lookup_cursor = this->handle_lookup_relation(lookup_cursor, 1);
     }
 
     size_t elliptic_cursor = 0;
-    while (elliptic_cursor < this->selectors[3].size()) {
-        elliptic_cursor = this->handle_elliptic_relation(elliptic_cursor, 3);
+    while (elliptic_cursor < this->selectors[4].size()) {
+        elliptic_cursor = this->handle_elliptic_relation(elliptic_cursor, 4);
     }
 
     // size_t delta_range_cursor = 0;
@@ -88,7 +88,7 @@ size_t UltraCircuit::handle_arithmetic_relation(size_t cursor, size_t idx)
 
     std::vector<bb::fr> boolean_gate = { 1, -1, 0, 0, 0, 0, 1, 0, 0, 0, 0 };
     bool boolean_gate_flag =
-        (boolean_gate == selectors[1][cursor]) && (w_l_idx == w_r_idx) && (w_o_idx == 0) && (w_4_idx == 0);
+        (boolean_gate == selectors[idx][cursor]) && (w_l_idx == w_r_idx) && (w_o_idx == 0) && (w_4_idx == 0);
     if (boolean_gate_flag) {
         (Bool(w_l) == Bool(STerm(0, this->solver, this->type)) | Bool(w_l) == Bool(STerm(1, this->solver, this->type)))
             .assert_term();
@@ -292,7 +292,7 @@ size_t UltraCircuit::handle_elliptic_relation(size_t cursor, size_t idx)
         y_add_identity == 0; // scaling_factor = 1
     }
 
-    bb::fr curve_b = this->selectors[3][cursor][11];
+    bb::fr curve_b = this->selectors[idx][cursor][11];
     auto x_pow_4 = (y1_sqr - curve_b) * x_1;
     auto y1_sqr_mul_4 = y1_sqr + y1_sqr;
     y1_sqr_mul_4 += y1_sqr_mul_4;

barretenberg/cpp/src/barretenberg/smt_verification/util/smt_util.cpp

@@ -33,6 +33,12 @@ bb::fr string_to_fr(const std::string& number, int base, size_t step)
         res += std::strtoull(slice.data(), &ptr, base);
     }
     res = number[0] == '-' ? -res : res;
+
+    if (base == 2 && number[0] == '1') {
+        auto max = bb::fr(uint256_t(1) << number.length());
+        res -= max;
+    }
+
     return res;
 }