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

@@ -89,4 +89,87 @@ TEST(helpers, pow2)
     info("z = ", vals["z"]);
     // z == 2048 in binary
     EXPECT_TRUE(vals["z"] == "00000000000000000000100000000000");
+}
+
+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");
+}
+
+TEST(helpers, signed_div_1)
+{
+    // using smt solver i found that 1879048194 >> 16 == 0
+    // its strange...
+    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");
+}
+
+TEST(helpers, signed_div_2)
+{
+    // using smt solver i found that 1879048194 >> 16 == 0
+    // its strange...
+    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");
+}
+
+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/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/circuit/ultra_circuit.hpp

@@ -15,11 +15,11 @@ class UltraCircuit : public CircuitBase {
   public:
     // TODO(alex): check that there's no actual pub_inputs block
     std::vector<std::vector<std::vector<bb::fr>>> selectors;    // all selectors from the circuit
-                                                                // 1st entry are arithmetic selectors
-                                                                // 2nd entry are delta_range selectors
-                                                                // 3rd entry are elliptic selectors
-                                                                // 4th entry are aux selectors
-                                                                // 5th entry are lookup selectors
+                                                                // 1st entry are lookup selectors
+                                                                // 2nd entry are arithmetic selectors
+                                                                // 3rd entry are delta_range selectors
+                                                                // 4th entry are elliptic selectors
+                                                                // 5th entry are aux selectors
     std::vector<std::vector<std::vector<uint32_t>>> wires_idxs; // values of the gates' wires idxs
 
     std::vector<std::vector<std::vector<bb::fr>>> lookup_tables;

barretenberg/cpp/src/barretenberg/smt_verification/terms/term.cpp

@@ -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)
+{
+    if (!this->operations.contains(OpType::EXTRACT) || !this->operations.contains(OpType::BITVEC_PAD)) {
+        info("EXTRACT is not compatible with ", this->type);
+        return *this;
+    }
+    cvc5::Op extraction = solver->term_manager.mkOp(this->operations.at(OpType::EXTRACT), { to_size, 0 });
+    cvc5::Term temp = solver->term_manager.mkTerm(extraction, { this->term });
+    cvc5::Op padding =
+        solver->term_manager.mkOp(this->operations.at(OpType::BITVEC_PAD),
+                                  { this->solver->bv_sort.getBitVectorSize() - temp.getSort().getBitVectorSize() });
+    cvc5::Term res = solver->term_manager.mkTerm(padding, { temp });
+    return { res, this->solver, this->type };
+}
+
+STerm STerm::extract_bit(const uint32_t& bit_index)
+{
+    if (!this->operations.contains(OpType::EXTRACT) || !this->operations.contains(OpType::BITVEC_PAD)) {
+        info("EXTRACT is not compatible with ", this->type);
+        return *this;
+    }
+    cvc5::Op extraction = solver->term_manager.mkOp(this->operations.at(OpType::EXTRACT), { bit_index, bit_index });
+    cvc5::Term temp = solver->term_manager.mkTerm(extraction, { this->term });
+    cvc5::Op padding =
+        solver->term_manager.mkOp(this->operations.at(OpType::BITVEC_PAD),
+                                  { this->solver->bv_sort.getBitVectorSize() - temp.getSort().getBitVectorSize() });
+    cvc5::Term res = solver->term_manager.mkTerm(padding, { temp });
+    return { res, this->solver, this->type };
+}
 /**
  * @brief Create an inclusion constraint
  *

barretenberg/cpp/src/barretenberg/smt_verification/terms/term.hpp

@@ -15,7 +15,28 @@ using namespace smt_solver;
 enum class TermType { FFTerm, FFITerm, BVTerm, ITerm };
 std::ostream& operator<<(std::ostream& os, TermType type);
 
-enum class OpType : int32_t { ADD, SUB, MUL, DIV, NEG, XOR, AND, OR, GT, GE, LT, LE, MOD, RSH, LSH, ROTR, ROTL, NOT };
+enum class OpType : int32_t {
+    ADD,
+    SUB,
+    MUL,
+    DIV,
+    NEG,
+    XOR,
+    AND,
+    OR,
+    GT,
+    GE,
+    LT,
+    LE,
+    MOD,
+    RSH,
+    LSH,
+    ROTR,
+    ROTL,
+    NOT,
+    EXTRACT,
+    BITVEC_PAD
+};
 
 /**
  * @brief precomputed map that contains allowed
@@ -75,6 +96,8 @@ const std::unordered_map<TermType, std::unordered_map<OpType, cvc5::Kind>> typed
           { OpType::MOD, cvc5::Kind::BITVECTOR_UREM },
           { OpType::DIV, cvc5::Kind::BITVECTOR_UDIV },
           { OpType::NOT, cvc5::Kind::BITVECTOR_NOT },
+          { OpType::EXTRACT, cvc5::Kind::BITVECTOR_EXTRACT },
+          { OpType::BITVEC_PAD, cvc5::Kind::BITVECTOR_ZERO_EXTEND },
       } }
 };
 
@@ -174,6 +197,17 @@ class STerm {
     STerm rotr(const uint32_t& n) const;
     STerm rotl(const uint32_t& n) const;
 
+    /**
+     * @brief Returns last `to_size` bits of variable
+     * @param to_size number of bits to be extracted
+     */
+    STerm truncate(const uint32_t& to_size);
+    /**
+     * @brief Returns ith bit of variable
+     * @param bit_index index of bit to be extracted
+     */
+    STerm extract_bit(const uint32_t& bit_index);
+
     void in(const cvc5::Term& table) const;
 
     operator std::string() const { return this->solver->stringify_term(term); };

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;
 }