feat: Adding fr compatibility to smt variables api

barretenberg/cpp/src/CMakeLists.txt

@@ -82,7 +82,6 @@ add_subdirectory(barretenberg/wasi)
 
 
 if(SMT)
-    include_directories(${CMAKE_CURRENT_SOURCE_DIR} $ENV{HOME}/cvc5/tmp-lib/include)
     add_subdirectory(barretenberg/smt_verification)
 endif()
 

barretenberg/cpp/src/barretenberg/smt_verification/CMakeLists.txt

@@ -1,2 +1,14 @@
-#barretenberg_module(smt_verification common ${CMAKE_SOURCE_DIR}/src/cvc5/tmp-lib/lib/libcvc5.so.1)
-barretenberg_module(smt_verification common proof_system stdlib_primitives $ENV{HOME}/cvc5/tmp-lib/lib/libcvc5.so.1)
+barretenberg_module(smt_verification common proof_system stdlib_primitives stdlib_sha256 cvc5)
+
+set(CVC5_INCLUDE $ENV{HOME}/cvc5/tmp-lib/include)
+set(CVC5_LIB $ENV{HOME}/cvc5/tmp-lib/lib)
+
+target_include_directories(smt_verification              PUBLIC ${CVC5_INCLUDE})
+target_include_directories(smt_verification_objects      PUBLIC ${CVC5_INCLUDE})
+target_include_directories(smt_verification_tests        PUBLIC ${CVC5_INCLUDE})
+target_include_directories(smt_verification_test_objects PUBLIC ${CVC5_INCLUDE})
+
+target_link_directories(smt_verification                 PUBLIC ${CVC5_LIB})
+target_link_directories(smt_verification_objects         PUBLIC ${CVC5_LIB})
+target_link_directories(smt_verification_tests           PUBLIC ${CVC5_LIB})
+target_link_directories(smt_verification_test_objects    PUBLIC ${CVC5_LIB})

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

@@ -71,7 +71,7 @@ To store it on the disk just do
 
     `FFTerm` - the symbolic value that simulates finite field elements. 
 
-    `FFTerm` - the symbolic value that simulates integer elements which behave like finite field ones. Useful, when you want to create range constraints or perform operations like XOR.
+    `FFITerm` - the symbolic value that simulates integer elements which behave like finite field ones. Useful, when you want to create range constraints or perform operations like XOR.
 
     `Bool` - simulates the boolean values and mostly will be used only to simulate complex `if` statements if needed.
 

barretenberg/cpp/src/barretenberg/smt_verification/solver/solver.hpp

@@ -1,8 +1,11 @@
 #pragma once
-#include <cvc5/cvc5.h>
 #include <string>
 #include <unordered_map>
 
+#include <cvc5/cvc5.h>
+
+#include "barretenberg/ecc/curves/bn254/fr.hpp"
+
 namespace smt_solver {
 
 /**

barretenberg/cpp/src/barretenberg/smt_verification/terms/ffiterm.cpp

@@ -38,56 +38,55 @@ FFITerm::FFITerm(const std::string& t, Solver* slv, bool isconst, uint32_t base)
         slv->s.assertFormula(ge);
         slv->s.assertFormula(lt);
     } else {
-        std::string tmp = slv->s.mkFiniteFieldElem(t, slv->fp, base).getFiniteFieldValue(); // dumb but works
-        if (tmp[0] == '-') {
-            this->term = slv->s.mkTerm(cvc5::Kind::ADD, { slv->s.mkInteger(tmp), this->modulus });
-        } else {
-            this->term = slv->s.mkInteger(tmp);
-        }
-        // this->term = slv->s.mkInteger(tmp); won't work for now since the assertion will definitely fail
+        // TODO(alex): CVC5 doesn't provide integer initialization from hex. Yet.
+        std::string strvalue = slv->s.mkFiniteFieldElem(t, slv->fp, base).getFiniteFieldValue();
+        this->term = slv->s.mkInteger(strvalue);
+        this->mod();
     }
 }
 
+void FFITerm::mod()
+{
+    this->term = this->solver->s.mkTerm(cvc5::Kind::INTS_MODULUS, { this->term, this->modulus });
+}
+
 FFITerm FFITerm::operator+(const FFITerm& other) const
 {
     cvc5::Term res = this->solver->s.mkTerm(cvc5::Kind::ADD, { this->term, other.term });
-    res = this->solver->s.mkTerm(cvc5::Kind::INTS_MODULUS, { res, this->modulus });
     return { res, this->solver };
 }
 
 void FFITerm::operator+=(const FFITerm& other)
 {
     this->term = this->solver->s.mkTerm(cvc5::Kind::ADD, { this->term, other.term });
-    this->term =
-        this->solver->s.mkTerm(cvc5::Kind::INTS_MODULUS, { this->term, this->modulus }); // TODO(alex): is it faster?
 }
 
 FFITerm FFITerm::operator-(const FFITerm& other) const
 {
     cvc5::Term res = this->solver->s.mkTerm(cvc5::Kind::SUB, { this->term, other.term });
-    res = this->solver->s.mkTerm(cvc5::Kind::INTS_MODULUS, { res, this->modulus });
     return { res, this->solver };
 }
 
 void FFITerm::operator-=(const FFITerm& other)
 {
     this->term = this->solver->s.mkTerm(cvc5::Kind::SUB, { this->term, other.term });
-    this->term =
-        this->solver->s.mkTerm(cvc5::Kind::INTS_MODULUS, { this->term, this->modulus }); // TODO(alex): is it faster?
+}
+
+FFITerm FFITerm::operator-() const
+{
+    cvc5::Term res = this->solver->s.mkTerm(cvc5::Kind::NEG, { this->term });
+    return { res, this->solver };
 }
 
 FFITerm FFITerm::operator*(const FFITerm& other) const
 {
     cvc5::Term res = solver->s.mkTerm(cvc5::Kind::MULT, { this->term, other.term });
-    res = this->solver->s.mkTerm(cvc5::Kind::INTS_MODULUS, { res, this->modulus });
     return { res, this->solver };
 }
 
 void FFITerm::operator*=(const FFITerm& other)
 {
     this->term = this->solver->s.mkTerm(cvc5::Kind::MULT, { this->term, other.term });
-    this->term =
-        this->solver->s.mkTerm(cvc5::Kind::INTS_MODULUS, { this->term, this->modulus }); // TODO(alex): is it faster?
 }
 
 /**
@@ -102,34 +101,22 @@ void FFITerm::operator*=(const FFITerm& other)
  */
 FFITerm FFITerm::operator/(const FFITerm& other) const
 {
-    cvc5::Term nz = this->solver->s.mkTerm(cvc5::Kind::EQUAL, { other.term, this->solver->s.mkInteger("0") });
-    nz = this->solver->s.mkTerm(cvc5::Kind::EQUAL, { nz, this->solver->s.mkBoolean(false) });
-    this->solver->s.assertFormula(nz);
-
-    cvc5::Term res = this->solver->s.mkConst(this->solver->s.getIntegerSort(),
-                                             "fe0f65a52067384116dc1137d798e0ca00a7ed46950e4eab7db51e08481535f2_div_" +
-                                                 std::string(*this) + "_" + std::string(other));
-    cvc5::Term div = this->solver->s.mkTerm(cvc5::Kind::MULT, { res, other.term });
-    div = this->solver->s.mkTerm(cvc5::Kind::INTS_MODULUS, { div, this->modulus });
-    cvc5::Term eq = this->solver->s.mkTerm(cvc5::Kind::EQUAL, { this->term, div });
-    this->solver->s.assertFormula(eq);
-    return { res, this->solver };
+    other != bb::fr(0);
+    FFITerm res = Var("df8b586e3fa7a1224ec95a886e17a7da_div_" + static_cast<std::string>(*this) + "_" +
+                          static_cast<std::string>(other),
+                      this->solver);
+    res* other == *this;
+    return res;
 }
 
 void FFITerm::operator/=(const FFITerm& other)
 {
-    cvc5::Term nz = this->solver->s.mkTerm(cvc5::Kind::EQUAL, { other.term, this->solver->s.mkInteger("0") });
-    nz = this->solver->s.mkTerm(cvc5::Kind::EQUAL, { nz, this->solver->s.mkBoolean(false) });
-    this->solver->s.assertFormula(nz);
-
-    cvc5::Term res = this->solver->s.mkConst(this->solver->fp,
-                                             "fe0f65a52067384116dc1137d798e0ca00a7ed46950e4eab7db51e08481535f2_div_" +
-                                                 std::string(*this) + "__" + std::string(other));
-    cvc5::Term div = this->solver->s.mkTerm(cvc5::Kind::MULT, { res, other.term });
-    div = this->solver->s.mkTerm(cvc5::Kind::INTS_MODULUS, { div, this->modulus });
-    cvc5::Term eq = this->solver->s.mkTerm(cvc5::Kind::EQUAL, { this->term, div });
-    this->solver->s.assertFormula(eq);
-    this->term = res;
+    other != bb::fr(0);
+    FFITerm res = Var("df8b586e3fa7a1224ec95a886e17a7da_div_" + static_cast<std::string>(*this) + "_" +
+                          static_cast<std::string>(other),
+                      this->solver);
+    res* other == *this;
+    this->term = res.term;
 }
 
 /**
@@ -138,7 +125,15 @@ void FFITerm::operator/=(const FFITerm& other)
  */
 void FFITerm::operator==(const FFITerm& other) const
 {
-    cvc5::Term eq = this->solver->s.mkTerm(cvc5::Kind::EQUAL, { this->term, other.term });
+    FFITerm tmp1 = *this;
+    if (tmp1.term.getNumChildren() > 1) {
+        tmp1.mod();
+    }
+    FFITerm tmp2 = other;
+    if (tmp2.term.getNumChildren() > 1) {
+        tmp2.mod();
+    }
+    cvc5::Term eq = this->solver->s.mkTerm(cvc5::Kind::EQUAL, { tmp1.term, tmp2.term });
     this->solver->s.assertFormula(eq);
 }
 
@@ -148,8 +143,83 @@ void FFITerm::operator==(const FFITerm& other) const
  */
 void FFITerm::operator!=(const FFITerm& other) const
 {
-    cvc5::Term eq = this->solver->s.mkTerm(cvc5::Kind::EQUAL, { this->term, other.term });
+    FFITerm tmp1 = *this;
+    if (tmp1.term.getNumChildren() > 1) {
+        tmp1.mod();
+    }
+    FFITerm tmp2 = other;
+    if (tmp2.term.getNumChildren() > 1) {
+        tmp2.mod();
+    }
+    cvc5::Term eq = this->solver->s.mkTerm(cvc5::Kind::EQUAL, { tmp1.term, tmp2.term });
     eq = this->solver->s.mkTerm(cvc5::Kind::EQUAL, { eq, this->solver->s.mkBoolean(false) });
     this->solver->s.assertFormula(eq);
 }
+
+FFITerm FFITerm::operator^(const FFITerm& other) const
+{
+    cvc5::Term res = this->solver->s.mkTerm(cvc5::Kind::XOR, { this->term, other.term });
+    return { res, this->solver };
+}
+
+void FFITerm::operator^=(const FFITerm& other)
+{
+    this->term = this->solver->s.mkTerm(cvc5::Kind::XOR, { this->term, other.term });
+}
+
+FFITerm operator+(const bb::fr& lhs, const FFITerm& rhs)
+{
+    return rhs + lhs;
+}
+
+FFITerm operator-(const bb::fr& lhs, const FFITerm& rhs)
+{
+    return (-rhs) + lhs;
+}
+
+FFITerm operator*(const bb::fr& lhs, const FFITerm& rhs)
+{
+    return rhs * lhs;
+}
+
+FFITerm operator/(const bb::fr& lhs, const FFITerm& rhs)
+{
+    return FFITerm(lhs, rhs.solver) / rhs;
+}
+
+FFITerm operator^(const bb::fr& lhs, const FFITerm& rhs)
+{
+    return rhs ^ lhs;
+}
+void operator==(const bb::fr& lhs, const FFITerm& rhs)
+{
+    rhs == lhs;
+}
+
+void operator!=(const bb::fr& lhs, const FFITerm& rhs)
+{
+    rhs != lhs;
+}
+
+void FFITerm::operator<(const bb::fr& other) const
+{
+    cvc5::Term lt = this->solver->s.mkTerm(cvc5::Kind::LT, { this->term, FFITerm(other, this->solver) });
+    this->solver->s.assertFormula(lt);
+}
+void FFITerm::operator<=(const bb::fr& other) const
+{
+    cvc5::Term le = this->solver->s.mkTerm(cvc5::Kind::LEQ, { this->term, FFITerm(other, this->solver) });
+    this->solver->s.assertFormula(le);
+}
+void FFITerm::operator>(const bb::fr& other) const
+{
+    cvc5::Term gt = this->solver->s.mkTerm(cvc5::Kind::GT, { this->term, FFITerm(other, this->solver) });
+    this->solver->s.assertFormula(gt);
+}
+void FFITerm::operator>=(const bb::fr& other) const
+{
+    cvc5::Term ge = this->solver->s.mkTerm(cvc5::Kind::GEQ, { this->term, FFITerm(other, this->solver) });
+    this->solver->s.assertFormula(ge);
+}
+
 } // namespace smt_terms

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

@@ -11,39 +11,54 @@ using namespace smt_solver;
  * Both of them support basic arithmetic operations: +, -, *, /.
  * Check the satisfability of a system and get it's model.
  *
- * @todo TODO(alex): mayb.. Have to patch cvc5 to create integers from hex...
  */
 class FFITerm {
   public:
     Solver* solver;
     cvc5::Term term;
     cvc5::Term modulus;
 
+    static bool isFiniteField() { return false; };
+    static bool isInteger() { return true; };
+
     FFITerm()
         : solver(nullptr)
         , term(cvc5::Term())
         , modulus(cvc5::Term()){};
 
-    explicit FFITerm(const std::string& t, Solver* slv, bool isconst = false, uint32_t base = 16);
     FFITerm(cvc5::Term& term, Solver* s)
         : solver(s)
         , term(term)
         , modulus(s->s.mkInteger(s->modulus))
     {}
 
+    explicit FFITerm(const std::string& t, Solver* slv, bool isconst = false, uint32_t base = 16);
+
     FFITerm(const FFITerm& other) = default;
     FFITerm(FFITerm&& other) = default;
 
     static FFITerm Var(const std::string& name, Solver* slv);
     static FFITerm Const(const std::string& val, Solver* slv, uint32_t base = 16);
 
+    explicit FFITerm(bb::fr value, Solver* s)
+    {
+        std::stringstream buf; // TODO(#893)
+        buf << value;
+        std::string tmp = buf.str();
+        tmp[1] = '0'; // avoiding `x` in 0x prefix
+
+        *this = Const(tmp, s);
+    }
+
     FFITerm& operator=(const FFITerm& right) = default;
     FFITerm& operator=(FFITerm&& right) = default;
 
     FFITerm operator+(const FFITerm& other) const;
     void operator+=(const FFITerm& other);
     FFITerm operator-(const FFITerm& other) const;
     void operator-=(const FFITerm& other);
+    FFITerm operator-() const;
+
     FFITerm operator*(const FFITerm& other) const;
     void operator*=(const FFITerm& other);
     FFITerm operator/(const FFITerm& other) const;
@@ -52,11 +67,20 @@ class FFITerm {
     void operator==(const FFITerm& other) const;
     void operator!=(const FFITerm& other) const;
 
+    FFITerm operator^(const FFITerm& other) const;
+    void operator^=(const FFITerm& other);
+
+    void mod();
+
     operator std::string() const { return term.isIntegerValue() ? term.getIntegerValue() : term.toString(); };
     operator cvc5::Term() const { return term; };
 
     ~FFITerm() = default;
-    friend std::ostream& operator<<(std::ostream& out, const FFITerm& k) { return out << k.term; }
+
+    friend std::ostream& operator<<(std::ostream& out, const FFITerm& term)
+    {
+        return out << static_cast<std::string>(term);
+    }
 
     friend FFITerm batch_add(const std::vector<FFITerm>& children)
     {
@@ -75,6 +99,34 @@ class FFITerm {
         res = slv->s.mkTerm(cvc5::Kind::INTS_MODULUS, { res, children[0].modulus });
         return { res, slv };
     }
+
+    // arithmetic compatibility with Fr
+
+    FFITerm operator+(const bb::fr& other) const { return *this + FFITerm(other, this->solver); }
+    void operator+=(const bb::fr& other) { *this += FFITerm(other, this->solver); }
+    FFITerm operator-(const bb::fr& other) const { return *this - FFITerm(other, this->solver); }
+    void operator-=(const bb::fr& other) { *this -= FFITerm(other, this->solver); }
+    FFITerm operator*(const bb::fr& other) const { return *this * FFITerm(other, this->solver); }
+    void operator*=(const bb::fr& other) { *this *= FFITerm(other, this->solver); }
+    FFITerm operator/(const bb::fr& other) const { return *this / FFITerm(other, this->solver); }
+    void operator/=(const bb::fr& other) { *this /= FFITerm(other, this->solver); }
+
+    void operator==(const bb::fr& other) const { *this == FFITerm(other, this->solver); }
+    void operator!=(const bb::fr& other) const { *this != FFITerm(other, this->solver); }
+    FFITerm operator^(const bb::fr& other) const { return *this ^ FFITerm(other, this->solver); }
+    void operator^=(const bb::fr& other) { *this ^= FFITerm(other, this->solver); }
+    void operator<(const bb::fr& other) const;
+    void operator<=(const bb::fr& other) const;
+    void operator>(const bb::fr& other) const;
+    void operator>=(const bb::fr& other) const;
 };
 
+FFITerm operator+(const bb::fr& lhs, const FFITerm& rhs);
+FFITerm operator-(const bb::fr& lhs, const FFITerm& rhs);
+FFITerm operator*(const bb::fr& lhs, const FFITerm& rhs);
+FFITerm operator^(const bb::fr& lhs, const FFITerm& rhs);
+FFITerm operator/(const bb::fr& lhs, const FFITerm& rhs);
+void operator==(const bb::fr& lhs, const FFITerm& rhs);
+void operator!=(const bb::fr& lhs, const FFITerm& rhs);
+
 } // namespace smt_terms