From b266440543a90319107dd3d3c8802f7e3437afd4 Mon Sep 17 00:00:00 2001 From: Sarkoxed Date: Fri, 1 Mar 2024 11:15:39 +0000 Subject: [PATCH 1/9] New more detailed CMakeLists --- barretenberg/cpp/src/CMakeLists.txt | 1 - .../barretenberg/smt_verification/CMakeLists.txt | 16 ++++++++++++++-- 2 files changed, 14 insertions(+), 3 deletions(-) diff --git a/barretenberg/cpp/src/CMakeLists.txt b/barretenberg/cpp/src/CMakeLists.txt index a52b8939764e..e50a20398ae5 100644 --- a/barretenberg/cpp/src/CMakeLists.txt +++ b/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() diff --git a/barretenberg/cpp/src/barretenberg/smt_verification/CMakeLists.txt b/barretenberg/cpp/src/barretenberg/smt_verification/CMakeLists.txt index b3fe42c39f5b..10c6998530d9 100644 --- a/barretenberg/cpp/src/barretenberg/smt_verification/CMakeLists.txt +++ b/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) \ No newline at end of file +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}) \ No newline at end of file From fe276886187c8dce2c426bd5af4fa4dc7c639dee Mon Sep 17 00:00:00 2001 From: Sarkoxed Date: Fri, 1 Mar 2024 11:59:18 +0000 Subject: [PATCH 2/9] Modified FFTerm and FFITerm classes - Now they are compatible with Fr variables - Changed FFIterm constant initialization --- .../smt_verification/terms/ffiterm.cpp | 102 +++++++++++++----- .../smt_verification/terms/ffiterm.hpp | 79 +++++++++++++- .../smt_verification/terms/ffterm.cpp | 34 ++++++ .../smt_verification/terms/ffterm.hpp | 96 ++++++++++++++++- 4 files changed, 281 insertions(+), 30 deletions(-) diff --git a/barretenberg/cpp/src/barretenberg/smt_verification/terms/ffiterm.cpp b/barretenberg/cpp/src/barretenberg/smt_verification/terms/ffiterm.cpp index d2a1a6c2670c..d04f167404f2 100644 --- a/barretenberg/cpp/src/barretenberg/smt_verification/terms/ffiterm.cpp +++ b/barretenberg/cpp/src/barretenberg/smt_verification/terms/ffiterm.cpp @@ -38,56 +38,52 @@ 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 + std::string strvalue = slv->s.mkFiniteFieldElem(t, slv->fp, base).getFiniteFieldValue(); // TODO(alex): works for now + 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,13 +98,12 @@ 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") }); + cvc5::Term nz = this->solver->s.mkTerm(cvc5::Kind::INTS_MODULUS, { other.term, this->modulus }); + nz = this->solver->s.mkTerm(cvc5::Kind::EQUAL, { nz, 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 res = Var("fe0f65a52067384116dc1137d798e0ca00a7ed46950e4eab7db51e08481535f2_div_" + std::string(*this) + "_" + std::string(other), this->solver).term; 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 }); @@ -118,13 +113,12 @@ FFITerm FFITerm::operator/(const FFITerm& other) const void FFITerm::operator/=(const FFITerm& other) { - cvc5::Term nz = this->solver->s.mkTerm(cvc5::Kind::EQUAL, { other.term, this->solver->s.mkInteger("0") }); + cvc5::Term nz = this->solver->s.mkTerm(cvc5::Kind::INTS_MODULUS, { other.term, this->modulus }); + nz = this->solver->s.mkTerm(cvc5::Kind::EQUAL, { nz, 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 res = Var("fe0f65a52067384116dc1137d798e0ca00a7ed46950e4eab7db51e08481535f2_div_" + std::string(*this) + "_" + std::string(other), this->solver).term; 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 }); @@ -152,4 +146,64 @@ void FFITerm::operator!=(const FFITerm& other) const 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::INTS_MODULUS, {this->term, this->modulus}); + 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::INTS_MODULUS, {this->term, this->modulus}); + 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::INTS_MODULUS, {this->term, this->modulus}); + 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::INTS_MODULUS, {this->term, this->modulus}); + ge = this->solver->s.mkTerm(cvc5::Kind::GEQ, {this->term, FFITerm(other, this->solver)}); + this->solver->s.assertFormula(ge); +} + } // namespace smt_terms diff --git a/barretenberg/cpp/src/barretenberg/smt_verification/terms/ffiterm.hpp b/barretenberg/cpp/src/barretenberg/smt_verification/terms/ffiterm.hpp index 6bb1239557be..4d9bd5c1c4e3 100644 --- a/barretenberg/cpp/src/barretenberg/smt_verification/terms/ffiterm.hpp +++ b/barretenberg/cpp/src/barretenberg/smt_verification/terms/ffiterm.hpp @@ -11,7 +11,6 @@ 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: @@ -19,24 +18,37 @@ class FFITerm { 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(alex): looks bad. Would be great to create tostring() converter + 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; @@ -44,6 +56,8 @@ class FFITerm { 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 +66,17 @@ 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(term); } friend FFITerm batch_add(const std::vector& children) { @@ -75,6 +95,59 @@ 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 diff --git a/barretenberg/cpp/src/barretenberg/smt_verification/terms/ffterm.cpp b/barretenberg/cpp/src/barretenberg/smt_verification/terms/ffterm.cpp index 4b96f68b8da6..2e98515086fc 100644 --- a/barretenberg/cpp/src/barretenberg/smt_verification/terms/ffterm.cpp +++ b/barretenberg/cpp/src/barretenberg/smt_verification/terms/ffterm.cpp @@ -55,6 +55,11 @@ FFTerm FFTerm::operator-(const FFTerm& other) const return { res, this->solver }; } +FFTerm FFTerm::operator-() const{ + cvc5::Term res = this->solver->s.mkTerm(cvc5::Kind::FINITE_FIELD_NEG, { this->term }); + return { res, this-> solver}; +} + void FFTerm::operator-=(const FFTerm& other) { cvc5::Term tmp_term = this->solver->s.mkTerm(cvc5::Kind::FINITE_FIELD_NEG, { other.term }); @@ -134,4 +139,33 @@ void FFTerm::operator!=(const FFTerm& other) const eq = this->solver->s.mkTerm(cvc5::Kind::EQUAL, { eq, this->solver->s.mkBoolean(false) }); this->solver->s.assertFormula(eq); } + +FFTerm operator+(const bb::fr& lhs, const FFTerm& rhs){ + return rhs + lhs; +} + +FFTerm operator-(const bb::fr& lhs, const FFTerm& rhs){ + return (-rhs) + lhs; +} + +FFTerm operator*(const bb::fr& lhs, const FFTerm& rhs){ + return rhs * lhs; +} + +FFTerm operator^(__attribute__((unused)) const bb::fr& lhs, __attribute__((unused)) const FFTerm& rhs){ + info("Not compatible with Finite Field"); + return {}; +} + +FFTerm operator/(const bb::fr& lhs, const FFTerm& rhs){ + return FFTerm(lhs, rhs.solver) / rhs; +} + +void operator==(const bb::fr& lhs, const FFTerm& rhs){ + rhs == lhs; +} + +void operator!=(const bb::fr& lhs, const FFTerm& rhs){ + rhs != lhs; +} } // namespace smt_terms \ No newline at end of file diff --git a/barretenberg/cpp/src/barretenberg/smt_verification/terms/ffterm.hpp b/barretenberg/cpp/src/barretenberg/smt_verification/terms/ffterm.hpp index 581b185bcb33..12b865660a5e 100644 --- a/barretenberg/cpp/src/barretenberg/smt_verification/terms/ffterm.hpp +++ b/barretenberg/cpp/src/barretenberg/smt_verification/terms/ffterm.hpp @@ -17,20 +17,34 @@ class FFTerm { Solver* solver; cvc5::Term term; + static bool isFiniteField() { return true; }; + static bool isInteger() { return false; }; + FFTerm() : solver(nullptr) , term(cvc5::Term()){}; - explicit FFTerm(const std::string& t, Solver* slv, bool isconst = false, uint32_t base = 16); FFTerm(cvc5::Term& term, Solver* s) : solver(s) , term(term){}; + + explicit FFTerm(const std::string& t, Solver* slv, bool isconst = false, uint32_t base = 16); + FFTerm(const FFTerm& other) = default; FFTerm(FFTerm&& other) = default; static FFTerm Var(const std::string& name, Solver* slv); static FFTerm Const(const std::string& val, Solver* slv, uint32_t base = 16); + FFTerm(bb::fr value, Solver* s){ + std::stringstream buf; // TODO(alex): looks bad. Would be great to create tostring() converter + buf << value; + std::string tmp = buf.str(); + tmp[1] = '0'; // avoiding `x` in 0x prefix + + *this = Const(tmp, s); + } + FFTerm& operator=(const FFTerm& right) = default; FFTerm& operator=(FFTerm&& right) = default; @@ -38,6 +52,8 @@ class FFTerm { void operator+=(const FFTerm& other); FFTerm operator-(const FFTerm& other) const; void operator-=(const FFTerm& other); + FFTerm operator-() const; + FFTerm operator*(const FFTerm& other) const; void operator*=(const FFTerm& other); FFTerm operator/(const FFTerm& other) const; @@ -46,11 +62,23 @@ class FFTerm { void operator==(const FFTerm& other) const; void operator!=(const FFTerm& other) const; + FFTerm operator^(__attribute__((unused)) const FFTerm& other) const{ + info("Not compatible with Finite Field"); + return {}; + } + void operator^=(__attribute__((unused)) const FFTerm& other){ + info("Not compatible with Finite Field"); + }; + + + void mod(){}; + operator std::string() const { return term.isFiniteFieldValue() ? term.getFiniteFieldValue() : term.toString(); }; operator cvc5::Term() const { return term; }; - + ~FFTerm() = default; - friend std::ostream& operator<<(std::ostream& out, const FFTerm& k) { return out << k.term; } + + friend std::ostream& operator<<(std::ostream& out, const FFTerm& term) { return out << static_cast(term); }; friend FFTerm batch_add(const std::vector& children) { @@ -67,6 +95,68 @@ class FFTerm { cvc5::Term res = slv->s.mkTerm(cvc5::Kind::FINITE_FIELD_MULT, terms); return { res, slv }; } + + // arithmetic compatibility with Fr + + FFTerm operator+(const bb::fr& rhs) const{ + return *this + FFTerm(rhs, this->solver); + } + void operator+=(const bb::fr& other){ + *this += FFTerm(other, this->solver); + } + FFTerm operator-(const bb::fr& other) const{ + return *this - FFTerm(other, this->solver); + } + void operator-=(const bb::fr& other){ + *this -= FFTerm(other, this->solver); + } + FFTerm operator*(const bb::fr& other) const{ + return *this * FFTerm(other, this->solver); + } + void operator*=(const bb::fr& other){ + *this *= FFTerm(other, this->solver); + } + FFTerm operator/(const bb::fr& other) const{ + return *this / FFTerm(other, this->solver); + } + void operator/=(const bb::fr& other){ + *this /= FFTerm(other, this->solver); + } + + void operator==(const bb::fr& other) const{ + *this == FFTerm(other, this->solver); + } + void operator!=(const bb::fr& other) const{ + *this != FFTerm(other, this->solver); + } + + FFTerm operator^(__attribute__((unused)) const bb::fr& other) const{ + info("Not compatible with Finite Field"); + return {}; + } + void operator^=(__attribute__((unused)) const bb::fr& other){ + info("Not compatible with Finite Field"); + } + void operator<(__attribute__((unused)) const bb::fr& other) const{ + info("Not compatible with Finite Field"); + } + void operator<=(__attribute__((unused)) const bb::fr& other) const{ + info("Not compatible with Finite Field"); + } + void operator>(__attribute__((unused)) const bb::fr& other) const{ + info("Not compatible with Finite Field"); + } + void operator>=(__attribute__((unused)) const bb::fr& other) const{ + info("Not compatible with Finite Field"); + } }; +FFTerm operator+(const bb::fr& lhs, const FFTerm& rhs); +FFTerm operator-(const bb::fr& lhs, const FFTerm& rhs); +FFTerm operator*(const bb::fr& lhs, const FFTerm& rhs); +FFTerm operator^(__attribute__((unused)) const bb::fr& lhs, __attribute__((unused)) const FFTerm& rhs); +FFTerm operator/(const bb::fr& lhs, const FFTerm& rhs); +void operator==(const bb::fr& lhs, const FFTerm& rhs); +void operator!=(const bb::fr& lhs, const FFTerm& rhs); + } // namespace smt_terms \ No newline at end of file From 5b3a4dc83807621c54964e47325a2df32a552010 Mon Sep 17 00:00:00 2001 From: Sarkoxed Date: Fri, 1 Mar 2024 12:00:48 +0000 Subject: [PATCH 3/9] Added tests for symbolic variables classes --- .../smt_verification/terms/ffiterm.test.cpp | 122 ++++++++++++++++++ .../smt_verification/terms/ffterm.test.cpp | 95 ++++++++++++++ 2 files changed, 217 insertions(+) create mode 100644 barretenberg/cpp/src/barretenberg/smt_verification/terms/ffiterm.test.cpp create mode 100644 barretenberg/cpp/src/barretenberg/smt_verification/terms/ffterm.test.cpp diff --git a/barretenberg/cpp/src/barretenberg/smt_verification/terms/ffiterm.test.cpp b/barretenberg/cpp/src/barretenberg/smt_verification/terms/ffiterm.test.cpp new file mode 100644 index 000000000000..dfde90b21430 --- /dev/null +++ b/barretenberg/cpp/src/barretenberg/smt_verification/terms/ffiterm.test.cpp @@ -0,0 +1,122 @@ +#include + +#include "ffiterm.hpp" + +#include + +namespace { +auto& engine = bb::numeric::get_debug_randomness(); +} + +using namespace smt_terms; + +TEST(integermod, addition) +{ + bb::fr a = bb::fr::random_element(); + bb::fr b = bb::fr::random_element(); + bb::fr c = a + b; + Solver s("30644e72e131a029b85045b68181585d2833e84879b9709143e1f593f0000001", { true, 0 }, 16); + + FFITerm x = FFITerm::Var("x", &s); + FFITerm y = FFITerm::Var("y", &s); + FFITerm bval = FFITerm(b, &s); + FFITerm z = x + y; + z.mod(); + + z == c; + x == a; + ASSERT_TRUE(s.check()); + + std::string yvals = s.s.getValue(y.term).getIntegerValue(); + std::string bvals = s.s.getValue(bval.term).getIntegerValue(); + ASSERT_EQ(bvals, yvals); +} + +TEST(integermod, subtraction) +{ + bb::fr a = bb::fr::random_element(); + bb::fr b = bb::fr::random_element(); + bb::fr c = a - b; + Solver s("30644e72e131a029b85045b68181585d2833e84879b9709143e1f593f0000001", { true, 0 }, 16); + + FFITerm x = FFITerm::Var("x", &s); + FFITerm y = FFITerm::Var("y", &s); + FFITerm bval = FFITerm(b, &s); + FFITerm z = x - y; + z.mod(); + + z == c; + x == a; + ASSERT_TRUE(s.check()); + + std::string yvals = s.s.getValue(y.term).getIntegerValue(); + std::string bvals = s.s.getValue(bval.term).getIntegerValue(); + ASSERT_EQ(bvals, yvals); +} + +TEST(integermod, multiplication) +{ + bb::fr a = bb::fr::random_element(); + bb::fr b = bb::fr::random_element(); + bb::fr c = a * b; + Solver s("30644e72e131a029b85045b68181585d2833e84879b9709143e1f593f0000001", { true, 0 }, 16); + + FFITerm x = FFITerm::Var("x", &s); + FFITerm y = FFITerm::Var("y", &s); + FFITerm bval = FFITerm(b, &s); + FFITerm z = x * y; + z.mod(); + + z == c; + x == a; + ASSERT_TRUE(s.check()); + + std::string yvals = s.s.getValue(y.term).getIntegerValue(); + std::string bvals = s.s.getValue(bval.term).getIntegerValue(); + ASSERT_EQ(bvals, yvals); +} + +TEST(integermod, division) +{ + bb::fr a = bb::fr::random_element(); + bb::fr b = bb::fr::random_element(); + bb::fr c = a / b; + Solver s("30644e72e131a029b85045b68181585d2833e84879b9709143e1f593f0000001", { true, 0 }, 16); + + FFITerm x = FFITerm::Var("x", &s); + FFITerm y = FFITerm::Var("y", &s); + FFITerm bval = FFITerm(b, &s); + FFITerm z = x / y; + //z.mod(); TODO(alex): something bad + + z == c; + x == a; + ASSERT_TRUE(s.check()); + + std::string yvals = s.s.getValue(y.term).getIntegerValue(); + std::string bvals = s.s.getValue(bval.term).getIntegerValue(); + ASSERT_EQ(bvals, yvals); +} + +TEST(integermod, xor) +{ + bb::fr a = bb::fr::random_element(); + bb::fr b = bb::fr::random_element(); + bb::fr c = a ^ b; + Solver s("30644e72e131a029b85045b68181585d2833e84879b9709143e1f593f0000001", { true, 0 }, 16); + + FFITerm x = FFITerm::Var("x", &s); + FFITerm y = FFITerm::Var("y", &s); + FFITerm bval = FFITerm(b, &s); + FFITerm z = x ^ y; + + z == c; + x == a; + ASSERT_TRUE(s.check()); + + std::string yvals = s.s.getValue(y.term).getIntegerValue(); + std::string bvals = s.s.getValue(bval.term).getIntegerValue(); + ASSERT_EQ(bvals, yvals); +} + +// TODO(alex): range_constraints \ No newline at end of file diff --git a/barretenberg/cpp/src/barretenberg/smt_verification/terms/ffterm.test.cpp b/barretenberg/cpp/src/barretenberg/smt_verification/terms/ffterm.test.cpp new file mode 100644 index 000000000000..c27e2d710e46 --- /dev/null +++ b/barretenberg/cpp/src/barretenberg/smt_verification/terms/ffterm.test.cpp @@ -0,0 +1,95 @@ +#include + +#include "ffterm.hpp" + +#include + +namespace { +auto& engine = bb::numeric::get_debug_randomness(); +} + +using namespace smt_terms; + +TEST(finitefield, addition) +{ + bb::fr a = bb::fr::random_element(); + bb::fr b = bb::fr::random_element(); + bb::fr c = a + b; + Solver s("30644e72e131a029b85045b68181585d2833e84879b9709143e1f593f0000001", { true, 0 }, 16); + + FFTerm x = FFTerm::Var("x", &s); + FFTerm y = FFTerm::Var("y", &s); + FFTerm bval = FFTerm(b, &s); + FFTerm z = x + y; + + z == c; + x == a; + ASSERT_TRUE(s.check()); + + std::string yvals = s.s.getValue(y.term).getFiniteFieldValue(); + std::string bvals = s.s.getValue(bval.term).getFiniteFieldValue(); + ASSERT_EQ(bvals, yvals); +} + +TEST(finitefield, subtraction) +{ + bb::fr a = bb::fr::random_element(); + bb::fr b = bb::fr::random_element(); + bb::fr c = a - b; + Solver s("30644e72e131a029b85045b68181585d2833e84879b9709143e1f593f0000001", { true, 0 }, 16); + + FFTerm x = FFTerm::Var("x", &s); + FFTerm y = FFTerm::Var("y", &s); + FFTerm bval = FFTerm(b, &s); + FFTerm z = x - y; + + z == c; + x == a; + ASSERT_TRUE(s.check()); + + std::string yvals = s.s.getValue(y.term).getFiniteFieldValue(); + std::string bvals = s.s.getValue(bval.term).getFiniteFieldValue(); + ASSERT_EQ(bvals, yvals); +} + +TEST(finitefield, multiplication) +{ + bb::fr a = bb::fr::random_element(); + bb::fr b = bb::fr::random_element(); + bb::fr c = a * b; + Solver s("30644e72e131a029b85045b68181585d2833e84879b9709143e1f593f0000001", { true, 0 }, 16); + + FFTerm x = FFTerm::Var("x", &s); + FFTerm y = FFTerm::Var("y", &s); + FFTerm bval = FFTerm(b, &s); + FFTerm z = x * y; + + z == c; + x == a; + ASSERT_TRUE(s.check()); + + std::string yvals = s.s.getValue(y.term).getFiniteFieldValue(); + std::string bvals = s.s.getValue(bval.term).getFiniteFieldValue(); + ASSERT_EQ(bvals, yvals); +} + +TEST(finitefield, division) +{ + bb::fr a = bb::fr::random_element(); + bb::fr b = bb::fr::random_element(); + bb::fr c = a / b; + Solver s("30644e72e131a029b85045b68181585d2833e84879b9709143e1f593f0000001", { true, 0 }, 16); + + FFTerm x = FFTerm::Var("x", &s); + FFTerm y = FFTerm::Var("y", &s); + FFTerm bval = FFTerm(b, &s); + FFTerm z = x / y; + + z == c; + x == a; + ASSERT_TRUE(s.check()); + + std::string yvals = s.s.getValue(y.term).getFiniteFieldValue(); + std::string bvals = s.s.getValue(bval.term).getFiniteFieldValue(); + ASSERT_EQ(bvals, yvals); +} \ No newline at end of file From 07987cf20590c5ccc53680d5d98c35b6e987a5b6 Mon Sep 17 00:00:00 2001 From: Sarkoxed Date: Fri, 1 Mar 2024 12:32:38 +0000 Subject: [PATCH 4/9] Removed xor test from ffiterm leaving only arithmetic + fr include --- .../smt_verification/solver/solver.hpp | 5 +++- .../smt_verification/terms/ffiterm.test.cpp | 23 +------------------ 2 files changed, 5 insertions(+), 23 deletions(-) diff --git a/barretenberg/cpp/src/barretenberg/smt_verification/solver/solver.hpp b/barretenberg/cpp/src/barretenberg/smt_verification/solver/solver.hpp index 508f79042cad..1126a896794a 100644 --- a/barretenberg/cpp/src/barretenberg/smt_verification/solver/solver.hpp +++ b/barretenberg/cpp/src/barretenberg/smt_verification/solver/solver.hpp @@ -1,8 +1,11 @@ #pragma once -#include #include #include +#include + +#include "barretenberg/ecc/curves/bn254/fr.hpp" + namespace smt_solver { /** diff --git a/barretenberg/cpp/src/barretenberg/smt_verification/terms/ffiterm.test.cpp b/barretenberg/cpp/src/barretenberg/smt_verification/terms/ffiterm.test.cpp index dfde90b21430..a2e76c046551 100644 --- a/barretenberg/cpp/src/barretenberg/smt_verification/terms/ffiterm.test.cpp +++ b/barretenberg/cpp/src/barretenberg/smt_verification/terms/ffiterm.test.cpp @@ -98,25 +98,4 @@ TEST(integermod, division) ASSERT_EQ(bvals, yvals); } -TEST(integermod, xor) -{ - bb::fr a = bb::fr::random_element(); - bb::fr b = bb::fr::random_element(); - bb::fr c = a ^ b; - Solver s("30644e72e131a029b85045b68181585d2833e84879b9709143e1f593f0000001", { true, 0 }, 16); - - FFITerm x = FFITerm::Var("x", &s); - FFITerm y = FFITerm::Var("y", &s); - FFITerm bval = FFITerm(b, &s); - FFITerm z = x ^ y; - - z == c; - x == a; - ASSERT_TRUE(s.check()); - - std::string yvals = s.s.getValue(y.term).getIntegerValue(); - std::string bvals = s.s.getValue(bval.term).getIntegerValue(); - ASSERT_EQ(bvals, yvals); -} - -// TODO(alex): range_constraints \ No newline at end of file +// TODO(alex): range_constraints, xor From ab3ff84a9e3f54f34f290885614867b23bbd3ef6 Mon Sep 17 00:00:00 2001 From: Sarkoxed Date: Mon, 4 Mar 2024 22:27:15 +0000 Subject: [PATCH 5/9] Fixed FFITerm and FFITerm methods - changed division method to be more readable - changed the hash value that is used as a dvision symbolic variable name to md5(Aztec) - Removed the mod operations from inequalities methods in FFITerm - Modified `==` and `!=` methods in FFITerm so now there won't be any redundant mod operations --- .../smt_verification/terms/ffiterm.cpp | 65 +++++++++---------- .../smt_verification/terms/ffterm.cpp | 32 +++------ 2 files changed, 40 insertions(+), 57 deletions(-) diff --git a/barretenberg/cpp/src/barretenberg/smt_verification/terms/ffiterm.cpp b/barretenberg/cpp/src/barretenberg/smt_verification/terms/ffiterm.cpp index d04f167404f2..7b1b894d38cd 100644 --- a/barretenberg/cpp/src/barretenberg/smt_verification/terms/ffiterm.cpp +++ b/barretenberg/cpp/src/barretenberg/smt_verification/terms/ffiterm.cpp @@ -38,7 +38,8 @@ FFITerm::FFITerm(const std::string& t, Solver* slv, bool isconst, uint32_t base) slv->s.assertFormula(ge); slv->s.assertFormula(lt); } else { - std::string strvalue = slv->s.mkFiniteFieldElem(t, slv->fp, base).getFiniteFieldValue(); // TODO(alex): works for now + // 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(); } @@ -98,32 +99,18 @@ void FFITerm::operator*=(const FFITerm& other) */ FFITerm FFITerm::operator/(const FFITerm& other) const { - cvc5::Term nz = this->solver->s.mkTerm(cvc5::Kind::INTS_MODULUS, { other.term, this->modulus }); - nz = this->solver->s.mkTerm(cvc5::Kind::EQUAL, { nz, 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 = Var("fe0f65a52067384116dc1137d798e0ca00a7ed46950e4eab7db51e08481535f2_div_" + std::string(*this) + "_" + std::string(other), this->solver).term; - 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(*this) + "_" + static_cast(other), this->solver); + res * other == *this; + return res; } void FFITerm::operator/=(const FFITerm& other) { - cvc5::Term nz = this->solver->s.mkTerm(cvc5::Kind::INTS_MODULUS, { other.term, this->modulus }); - nz = this->solver->s.mkTerm(cvc5::Kind::EQUAL, { nz, 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 = Var("fe0f65a52067384116dc1137d798e0ca00a7ed46950e4eab7db51e08481535f2_div_" + std::string(*this) + "_" + std::string(other), this->solver).term; - 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(*this) + "_" + static_cast(other), this->solver); + res * other == *this; + this->term = res.term; } /** @@ -132,7 +119,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); } @@ -142,7 +137,15 @@ 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); } @@ -186,23 +189,19 @@ void operator!=(const bb::fr& lhs, const FFITerm& rhs){ } void FFITerm::operator<(const bb::fr& other) const{ - cvc5::Term lt = this->solver->s.mkTerm(cvc5::Kind::INTS_MODULUS, {this->term, this->modulus}); - lt = this->solver->s.mkTerm(cvc5::Kind::LT, {this->term, FFITerm(other, this->solver)}); + 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::INTS_MODULUS, {this->term, this->modulus}); - le = this->solver->s.mkTerm(cvc5::Kind::LEQ, {this->term, FFITerm(other, this->solver)}); + 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::INTS_MODULUS, {this->term, this->modulus}); - gt = this->solver->s.mkTerm(cvc5::Kind::GT, {this->term, FFITerm(other, this->solver)}); + 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::INTS_MODULUS, {this->term, this->modulus}); - ge = this->solver->s.mkTerm(cvc5::Kind::GEQ, {this->term, FFITerm(other, this->solver)}); + cvc5::Term ge = this->solver->s.mkTerm(cvc5::Kind::GEQ, {this->term, FFITerm(other, this->solver)}); this->solver->s.assertFormula(ge); } diff --git a/barretenberg/cpp/src/barretenberg/smt_verification/terms/ffterm.cpp b/barretenberg/cpp/src/barretenberg/smt_verification/terms/ffterm.cpp index 2e98515086fc..e5030b113808 100644 --- a/barretenberg/cpp/src/barretenberg/smt_verification/terms/ffterm.cpp +++ b/barretenberg/cpp/src/barretenberg/smt_verification/terms/ffterm.cpp @@ -89,34 +89,18 @@ void FFTerm::operator*=(const FFTerm& other) */ FFTerm FFTerm::operator/(const FFTerm& other) const { - cvc5::Term nz = this->solver->s.mkTerm(cvc5::Kind::EQUAL, - { other.term, this->solver->s.mkFiniteFieldElem("0", this->solver->fp) }); - 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::FINITE_FIELD_MULT, { res, other.term }); - 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); + FFTerm res = Var("df8b586e3fa7a1224ec95a886e17a7da_div_" + static_cast(*this) + "_" + static_cast(other), this->solver); + res * other == *this; + return res; } void FFTerm::operator/=(const FFTerm& other) { - cvc5::Term nz = this->solver->s.mkTerm(cvc5::Kind::EQUAL, - { other.term, this->solver->s.mkFiniteFieldElem("0", this->solver->fp) }); - 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::FINITE_FIELD_MULT, { res, other.term }); - 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); + FFTerm res = Var("df8b586e3fa7a1224ec95a886e17a7da_div_" + static_cast(*this) + "_" + static_cast(other), this->solver); + res * other == *this; + this->term = res.term; } /** From dca609a528f0be69df4bf21c23dfa87aeb9544f8 Mon Sep 17 00:00:00 2001 From: Sarkoxed Date: Mon, 4 Mar 2024 22:36:14 +0000 Subject: [PATCH 6/9] Fix todos to be linked to issue --- .../cpp/src/barretenberg/smt_verification/terms/ffiterm.hpp | 2 +- .../cpp/src/barretenberg/smt_verification/terms/ffterm.hpp | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/barretenberg/cpp/src/barretenberg/smt_verification/terms/ffiterm.hpp b/barretenberg/cpp/src/barretenberg/smt_verification/terms/ffiterm.hpp index 4d9bd5c1c4e3..186503cabadc 100644 --- a/barretenberg/cpp/src/barretenberg/smt_verification/terms/ffiterm.hpp +++ b/barretenberg/cpp/src/barretenberg/smt_verification/terms/ffiterm.hpp @@ -41,7 +41,7 @@ class FFITerm { static FFITerm Const(const std::string& val, Solver* slv, uint32_t base = 16); explicit FFITerm(bb::fr value, Solver* s){ - std::stringstream buf; // TODO(alex): looks bad. Would be great to create tostring() converter + std::stringstream buf; // TODO(#893) buf << value; std::string tmp = buf.str(); tmp[1] = '0'; // avoiding `x` in 0x prefix diff --git a/barretenberg/cpp/src/barretenberg/smt_verification/terms/ffterm.hpp b/barretenberg/cpp/src/barretenberg/smt_verification/terms/ffterm.hpp index 12b865660a5e..5804171717c6 100644 --- a/barretenberg/cpp/src/barretenberg/smt_verification/terms/ffterm.hpp +++ b/barretenberg/cpp/src/barretenberg/smt_verification/terms/ffterm.hpp @@ -37,7 +37,7 @@ class FFTerm { static FFTerm Const(const std::string& val, Solver* slv, uint32_t base = 16); FFTerm(bb::fr value, Solver* s){ - std::stringstream buf; // TODO(alex): looks bad. Would be great to create tostring() converter + std::stringstream buf; // TODO(#893) buf << value; std::string tmp = buf.str(); tmp[1] = '0'; // avoiding `x` in 0x prefix From 20397aa33709c2c2f1dafb84f2e2d277e91e7d7d Mon Sep 17 00:00:00 2001 From: Sarkoxed Date: Mon, 4 Mar 2024 22:38:48 +0000 Subject: [PATCH 7/9] Renamed the test classes --- .../smt_verification/terms/ffiterm.test.cpp | 14 ++++---------- .../smt_verification/terms/ffterm.test.cpp | 8 ++++---- 2 files changed, 8 insertions(+), 14 deletions(-) diff --git a/barretenberg/cpp/src/barretenberg/smt_verification/terms/ffiterm.test.cpp b/barretenberg/cpp/src/barretenberg/smt_verification/terms/ffiterm.test.cpp index a2e76c046551..10c4f01594be 100644 --- a/barretenberg/cpp/src/barretenberg/smt_verification/terms/ffiterm.test.cpp +++ b/barretenberg/cpp/src/barretenberg/smt_verification/terms/ffiterm.test.cpp @@ -10,7 +10,7 @@ auto& engine = bb::numeric::get_debug_randomness(); using namespace smt_terms; -TEST(integermod, addition) +TEST(FFITerm, addition) { bb::fr a = bb::fr::random_element(); bb::fr b = bb::fr::random_element(); @@ -21,7 +21,6 @@ TEST(integermod, addition) FFITerm y = FFITerm::Var("y", &s); FFITerm bval = FFITerm(b, &s); FFITerm z = x + y; - z.mod(); z == c; x == a; @@ -32,7 +31,7 @@ TEST(integermod, addition) ASSERT_EQ(bvals, yvals); } -TEST(integermod, subtraction) +TEST(FFITerm, subtraction) { bb::fr a = bb::fr::random_element(); bb::fr b = bb::fr::random_element(); @@ -43,7 +42,6 @@ TEST(integermod, subtraction) FFITerm y = FFITerm::Var("y", &s); FFITerm bval = FFITerm(b, &s); FFITerm z = x - y; - z.mod(); z == c; x == a; @@ -54,7 +52,7 @@ TEST(integermod, subtraction) ASSERT_EQ(bvals, yvals); } -TEST(integermod, multiplication) +TEST(FFITerm, multiplication) { bb::fr a = bb::fr::random_element(); bb::fr b = bb::fr::random_element(); @@ -65,7 +63,6 @@ TEST(integermod, multiplication) FFITerm y = FFITerm::Var("y", &s); FFITerm bval = FFITerm(b, &s); FFITerm z = x * y; - z.mod(); z == c; x == a; @@ -76,7 +73,7 @@ TEST(integermod, multiplication) ASSERT_EQ(bvals, yvals); } -TEST(integermod, division) +TEST(FFITerm, division) { bb::fr a = bb::fr::random_element(); bb::fr b = bb::fr::random_element(); @@ -87,7 +84,6 @@ TEST(integermod, division) FFITerm y = FFITerm::Var("y", &s); FFITerm bval = FFITerm(b, &s); FFITerm z = x / y; - //z.mod(); TODO(alex): something bad z == c; x == a; @@ -97,5 +93,3 @@ TEST(integermod, division) std::string bvals = s.s.getValue(bval.term).getIntegerValue(); ASSERT_EQ(bvals, yvals); } - -// TODO(alex): range_constraints, xor diff --git a/barretenberg/cpp/src/barretenberg/smt_verification/terms/ffterm.test.cpp b/barretenberg/cpp/src/barretenberg/smt_verification/terms/ffterm.test.cpp index c27e2d710e46..3d71782f9789 100644 --- a/barretenberg/cpp/src/barretenberg/smt_verification/terms/ffterm.test.cpp +++ b/barretenberg/cpp/src/barretenberg/smt_verification/terms/ffterm.test.cpp @@ -10,7 +10,7 @@ auto& engine = bb::numeric::get_debug_randomness(); using namespace smt_terms; -TEST(finitefield, addition) +TEST(FFTerm, addition) { bb::fr a = bb::fr::random_element(); bb::fr b = bb::fr::random_element(); @@ -31,7 +31,7 @@ TEST(finitefield, addition) ASSERT_EQ(bvals, yvals); } -TEST(finitefield, subtraction) +TEST(FFTerm, subtraction) { bb::fr a = bb::fr::random_element(); bb::fr b = bb::fr::random_element(); @@ -52,7 +52,7 @@ TEST(finitefield, subtraction) ASSERT_EQ(bvals, yvals); } -TEST(finitefield, multiplication) +TEST(FFTerm, multiplication) { bb::fr a = bb::fr::random_element(); bb::fr b = bb::fr::random_element(); @@ -73,7 +73,7 @@ TEST(finitefield, multiplication) ASSERT_EQ(bvals, yvals); } -TEST(finitefield, division) +TEST(FFTerm, division) { bb::fr a = bb::fr::random_element(); bb::fr b = bb::fr::random_element(); From cc53f794414ebbfa0819076d79417911fefc7b2e Mon Sep 17 00:00:00 2001 From: Sarkoxed Date: Tue, 5 Mar 2024 17:17:33 +0000 Subject: [PATCH 8/9] Fixing a typo in readme.md - FFTerm -> FFITerm --- barretenberg/cpp/src/barretenberg/smt_verification/README.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/barretenberg/cpp/src/barretenberg/smt_verification/README.md b/barretenberg/cpp/src/barretenberg/smt_verification/README.md index 8dfe2fc15486..5fd904c16bbe 100644 --- a/barretenberg/cpp/src/barretenberg/smt_verification/README.md +++ b/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. From d46e267393e793a4b814b599ff3185d440465f45 Mon Sep 17 00:00:00 2001 From: Rumata888 Date: Tue, 5 Mar 2024 19:56:43 +0000 Subject: [PATCH 9/9] formatting fix --- .../smt_verification/terms/ffiterm.cpp | 87 ++++++++++-------- .../smt_verification/terms/ffiterm.hpp | 67 +++++--------- .../smt_verification/terms/ffiterm.test.cpp | 8 +- .../smt_verification/terms/ffterm.cpp | 42 +++++---- .../smt_verification/terms/ffterm.hpp | 89 +++++++------------ .../smt_verification/terms/ffterm.test.cpp | 8 +- 6 files changed, 141 insertions(+), 160 deletions(-) diff --git a/barretenberg/cpp/src/barretenberg/smt_verification/terms/ffiterm.cpp b/barretenberg/cpp/src/barretenberg/smt_verification/terms/ffiterm.cpp index 7b1b894d38cd..130fa36f5ea9 100644 --- a/barretenberg/cpp/src/barretenberg/smt_verification/terms/ffiterm.cpp +++ b/barretenberg/cpp/src/barretenberg/smt_verification/terms/ffiterm.cpp @@ -39,14 +39,15 @@ FFITerm::FFITerm(const std::string& t, Solver* slv, bool isconst, uint32_t base) slv->s.assertFormula(lt); } else { // TODO(alex): CVC5 doesn't provide integer initialization from hex. Yet. - std::string strvalue = slv->s.mkFiniteFieldElem(t, slv->fp, base).getFiniteFieldValue(); + 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}); +void FFITerm::mod() +{ + this->term = this->solver->s.mkTerm(cvc5::Kind::INTS_MODULUS, { this->term, this->modulus }); } FFITerm FFITerm::operator+(const FFITerm& other) const @@ -71,9 +72,10 @@ void FFITerm::operator-=(const FFITerm& other) this->term = this->solver->s.mkTerm(cvc5::Kind::SUB, { this->term, other.term }); } -FFITerm FFITerm::operator-() const{ +FFITerm FFITerm::operator-() const +{ cvc5::Term res = this->solver->s.mkTerm(cvc5::Kind::NEG, { this->term }); - return { res, this-> solver}; + return { res, this->solver }; } FFITerm FFITerm::operator*(const FFITerm& other) const @@ -100,16 +102,20 @@ void FFITerm::operator*=(const FFITerm& other) FFITerm FFITerm::operator/(const FFITerm& other) const { other != bb::fr(0); - FFITerm res = Var("df8b586e3fa7a1224ec95a886e17a7da_div_" + static_cast(*this) + "_" + static_cast(other), this->solver); - res * other == *this; + FFITerm res = Var("df8b586e3fa7a1224ec95a886e17a7da_div_" + static_cast(*this) + "_" + + static_cast(other), + this->solver); + res* other == *this; return res; } void FFITerm::operator/=(const FFITerm& other) { other != bb::fr(0); - FFITerm res = Var("df8b586e3fa7a1224ec95a886e17a7da_div_" + static_cast(*this) + "_" + static_cast(other), this->solver); - res * other == *this; + FFITerm res = Var("df8b586e3fa7a1224ec95a886e17a7da_div_" + static_cast(*this) + "_" + + static_cast(other), + this->solver); + res* other == *this; this->term = res.term; } @@ -120,13 +126,13 @@ void FFITerm::operator/=(const FFITerm& other) void FFITerm::operator==(const FFITerm& other) const { FFITerm tmp1 = *this; - if (tmp1.term.getNumChildren() > 1){ + if (tmp1.term.getNumChildren() > 1) { tmp1.mod(); - } + } FFITerm tmp2 = other; - if (tmp2.term.getNumChildren() > 1){ + 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); } @@ -138,13 +144,13 @@ void FFITerm::operator==(const FFITerm& other) const void FFITerm::operator!=(const FFITerm& other) const { FFITerm tmp1 = *this; - if (tmp1.term.getNumChildren() > 1){ + if (tmp1.term.getNumChildren() > 1) { tmp1.mod(); - } + } FFITerm tmp2 = other; - if (tmp2.term.getNumChildren() > 1){ + 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); @@ -152,56 +158,67 @@ void FFITerm::operator!=(const FFITerm& other) const 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}; + 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}); + this->term = this->solver->s.mkTerm(cvc5::Kind::XOR, { this->term, other.term }); } -FFITerm operator+(const bb::fr& lhs, const FFITerm& rhs){ +FFITerm operator+(const bb::fr& lhs, const FFITerm& rhs) +{ return rhs + lhs; } -FFITerm operator-(const bb::fr& lhs, const FFITerm& rhs){ +FFITerm operator-(const bb::fr& lhs, const FFITerm& rhs) +{ return (-rhs) + lhs; } -FFITerm operator*(const bb::fr& lhs, const FFITerm& rhs){ +FFITerm operator*(const bb::fr& lhs, const FFITerm& rhs) +{ return rhs * lhs; } -FFITerm operator/(const bb::fr& lhs, const FFITerm& rhs){ +FFITerm operator/(const bb::fr& lhs, const FFITerm& rhs) +{ return FFITerm(lhs, rhs.solver) / rhs; } -FFITerm operator^(const bb::fr& lhs, const FFITerm& rhs){ +FFITerm operator^(const bb::fr& lhs, const FFITerm& rhs) +{ return rhs ^ lhs; } -void operator==(const bb::fr& lhs, const FFITerm& rhs){ +void operator==(const bb::fr& lhs, const FFITerm& rhs) +{ rhs == lhs; } -void operator!=(const bb::fr& lhs, const FFITerm& rhs){ +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)}); +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)}); +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)}); +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)}); +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); } diff --git a/barretenberg/cpp/src/barretenberg/smt_verification/terms/ffiterm.hpp b/barretenberg/cpp/src/barretenberg/smt_verification/terms/ffiterm.hpp index 186503cabadc..3bc465f3e531 100644 --- a/barretenberg/cpp/src/barretenberg/smt_verification/terms/ffiterm.hpp +++ b/barretenberg/cpp/src/barretenberg/smt_verification/terms/ffiterm.hpp @@ -40,12 +40,13 @@ class FFITerm { 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){ + 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 - + tmp[1] = '0'; // avoiding `x` in 0x prefix + *this = Const(tmp, s); } @@ -57,7 +58,7 @@ class FFITerm { 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; @@ -76,7 +77,10 @@ class FFITerm { ~FFITerm() = default; - friend std::ostream& operator<<(std::ostream& out, const FFITerm& term) { return out << static_cast(term); } + friend std::ostream& operator<<(std::ostream& out, const FFITerm& term) + { + return out << static_cast(term); + } friend FFITerm batch_add(const std::vector& children) { @@ -95,51 +99,26 @@ 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); - } + // arithmetic compatibility with Fr - 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); - } + 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); diff --git a/barretenberg/cpp/src/barretenberg/smt_verification/terms/ffiterm.test.cpp b/barretenberg/cpp/src/barretenberg/smt_verification/terms/ffiterm.test.cpp index 10c4f01594be..7fc5e3edbf35 100644 --- a/barretenberg/cpp/src/barretenberg/smt_verification/terms/ffiterm.test.cpp +++ b/barretenberg/cpp/src/barretenberg/smt_verification/terms/ffiterm.test.cpp @@ -21,7 +21,7 @@ TEST(FFITerm, addition) FFITerm y = FFITerm::Var("y", &s); FFITerm bval = FFITerm(b, &s); FFITerm z = x + y; - + z == c; x == a; ASSERT_TRUE(s.check()); @@ -42,7 +42,7 @@ TEST(FFITerm, subtraction) FFITerm y = FFITerm::Var("y", &s); FFITerm bval = FFITerm(b, &s); FFITerm z = x - y; - + z == c; x == a; ASSERT_TRUE(s.check()); @@ -63,7 +63,7 @@ TEST(FFITerm, multiplication) FFITerm y = FFITerm::Var("y", &s); FFITerm bval = FFITerm(b, &s); FFITerm z = x * y; - + z == c; x == a; ASSERT_TRUE(s.check()); @@ -84,7 +84,7 @@ TEST(FFITerm, division) FFITerm y = FFITerm::Var("y", &s); FFITerm bval = FFITerm(b, &s); FFITerm z = x / y; - + z == c; x == a; ASSERT_TRUE(s.check()); diff --git a/barretenberg/cpp/src/barretenberg/smt_verification/terms/ffterm.cpp b/barretenberg/cpp/src/barretenberg/smt_verification/terms/ffterm.cpp index e5030b113808..2dfc0904afdc 100644 --- a/barretenberg/cpp/src/barretenberg/smt_verification/terms/ffterm.cpp +++ b/barretenberg/cpp/src/barretenberg/smt_verification/terms/ffterm.cpp @@ -55,9 +55,10 @@ FFTerm FFTerm::operator-(const FFTerm& other) const return { res, this->solver }; } -FFTerm FFTerm::operator-() const{ +FFTerm FFTerm::operator-() const +{ cvc5::Term res = this->solver->s.mkTerm(cvc5::Kind::FINITE_FIELD_NEG, { this->term }); - return { res, this-> solver}; + return { res, this->solver }; } void FFTerm::operator-=(const FFTerm& other) @@ -89,17 +90,21 @@ void FFTerm::operator*=(const FFTerm& other) */ FFTerm FFTerm::operator/(const FFTerm& other) const { - other != bb::fr(0); - FFTerm res = Var("df8b586e3fa7a1224ec95a886e17a7da_div_" + static_cast(*this) + "_" + static_cast(other), this->solver); - res * other == *this; - return res; + other != bb::fr(0); + FFTerm res = Var("df8b586e3fa7a1224ec95a886e17a7da_div_" + static_cast(*this) + "_" + + static_cast(other), + this->solver); + res* other == *this; + return res; } void FFTerm::operator/=(const FFTerm& other) { other != bb::fr(0); - FFTerm res = Var("df8b586e3fa7a1224ec95a886e17a7da_div_" + static_cast(*this) + "_" + static_cast(other), this->solver); - res * other == *this; + FFTerm res = Var("df8b586e3fa7a1224ec95a886e17a7da_div_" + static_cast(*this) + "_" + + static_cast(other), + this->solver); + res* other == *this; this->term = res.term; } @@ -124,32 +129,39 @@ void FFTerm::operator!=(const FFTerm& other) const this->solver->s.assertFormula(eq); } -FFTerm operator+(const bb::fr& lhs, const FFTerm& rhs){ +FFTerm operator+(const bb::fr& lhs, const FFTerm& rhs) +{ return rhs + lhs; } -FFTerm operator-(const bb::fr& lhs, const FFTerm& rhs){ +FFTerm operator-(const bb::fr& lhs, const FFTerm& rhs) +{ return (-rhs) + lhs; } -FFTerm operator*(const bb::fr& lhs, const FFTerm& rhs){ +FFTerm operator*(const bb::fr& lhs, const FFTerm& rhs) +{ return rhs * lhs; } -FFTerm operator^(__attribute__((unused)) const bb::fr& lhs, __attribute__((unused)) const FFTerm& rhs){ +FFTerm operator^(__attribute__((unused)) const bb::fr& lhs, __attribute__((unused)) const FFTerm& rhs) +{ info("Not compatible with Finite Field"); return {}; } -FFTerm operator/(const bb::fr& lhs, const FFTerm& rhs){ +FFTerm operator/(const bb::fr& lhs, const FFTerm& rhs) +{ return FFTerm(lhs, rhs.solver) / rhs; } -void operator==(const bb::fr& lhs, const FFTerm& rhs){ +void operator==(const bb::fr& lhs, const FFTerm& rhs) +{ rhs == lhs; } -void operator!=(const bb::fr& lhs, const FFTerm& rhs){ +void operator!=(const bb::fr& lhs, const FFTerm& rhs) +{ rhs != lhs; } } // namespace smt_terms \ No newline at end of file diff --git a/barretenberg/cpp/src/barretenberg/smt_verification/terms/ffterm.hpp b/barretenberg/cpp/src/barretenberg/smt_verification/terms/ffterm.hpp index 5804171717c6..e847daea07fb 100644 --- a/barretenberg/cpp/src/barretenberg/smt_verification/terms/ffterm.hpp +++ b/barretenberg/cpp/src/barretenberg/smt_verification/terms/ffterm.hpp @@ -19,7 +19,7 @@ class FFTerm { static bool isFiniteField() { return true; }; static bool isInteger() { return false; }; - + FFTerm() : solver(nullptr) , term(cvc5::Term()){}; @@ -36,15 +36,16 @@ class FFTerm { static FFTerm Var(const std::string& name, Solver* slv); static FFTerm Const(const std::string& val, Solver* slv, uint32_t base = 16); - FFTerm(bb::fr value, Solver* s){ + FFTerm(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 - + tmp[1] = '0'; // avoiding `x` in 0x prefix + *this = Const(tmp, s); } - + FFTerm& operator=(const FFTerm& right) = default; FFTerm& operator=(FFTerm&& right) = default; @@ -62,23 +63,24 @@ class FFTerm { void operator==(const FFTerm& other) const; void operator!=(const FFTerm& other) const; - FFTerm operator^(__attribute__((unused)) const FFTerm& other) const{ + FFTerm operator^(__attribute__((unused)) const FFTerm& other) const + { info("Not compatible with Finite Field"); return {}; } - void operator^=(__attribute__((unused)) const FFTerm& other){ - info("Not compatible with Finite Field"); - }; - + void operator^=(__attribute__((unused)) const FFTerm& other) { info("Not compatible with Finite Field"); }; void mod(){}; operator std::string() const { return term.isFiniteFieldValue() ? term.getFiniteFieldValue() : term.toString(); }; operator cvc5::Term() const { return term; }; - + ~FFTerm() = default; - friend std::ostream& operator<<(std::ostream& out, const FFTerm& term) { return out << static_cast(term); }; + friend std::ostream& operator<<(std::ostream& out, const FFTerm& term) + { + return out << static_cast(term); + }; friend FFTerm batch_add(const std::vector& children) { @@ -98,57 +100,28 @@ class FFTerm { // arithmetic compatibility with Fr - FFTerm operator+(const bb::fr& rhs) const{ - return *this + FFTerm(rhs, this->solver); - } - void operator+=(const bb::fr& other){ - *this += FFTerm(other, this->solver); - } - FFTerm operator-(const bb::fr& other) const{ - return *this - FFTerm(other, this->solver); - } - void operator-=(const bb::fr& other){ - *this -= FFTerm(other, this->solver); - } - FFTerm operator*(const bb::fr& other) const{ - return *this * FFTerm(other, this->solver); - } - void operator*=(const bb::fr& other){ - *this *= FFTerm(other, this->solver); - } - FFTerm operator/(const bb::fr& other) const{ - return *this / FFTerm(other, this->solver); - } - void operator/=(const bb::fr& other){ - *this /= FFTerm(other, this->solver); - } + FFTerm operator+(const bb::fr& rhs) const { return *this + FFTerm(rhs, this->solver); } + void operator+=(const bb::fr& other) { *this += FFTerm(other, this->solver); } + FFTerm operator-(const bb::fr& other) const { return *this - FFTerm(other, this->solver); } + void operator-=(const bb::fr& other) { *this -= FFTerm(other, this->solver); } + FFTerm operator*(const bb::fr& other) const { return *this * FFTerm(other, this->solver); } + void operator*=(const bb::fr& other) { *this *= FFTerm(other, this->solver); } + FFTerm operator/(const bb::fr& other) const { return *this / FFTerm(other, this->solver); } + void operator/=(const bb::fr& other) { *this /= FFTerm(other, this->solver); } - void operator==(const bb::fr& other) const{ - *this == FFTerm(other, this->solver); - } - void operator!=(const bb::fr& other) const{ - *this != FFTerm(other, this->solver); - } + void operator==(const bb::fr& other) const { *this == FFTerm(other, this->solver); } + void operator!=(const bb::fr& other) const { *this != FFTerm(other, this->solver); } - FFTerm operator^(__attribute__((unused)) const bb::fr& other) const{ + FFTerm operator^(__attribute__((unused)) const bb::fr& other) const + { info("Not compatible with Finite Field"); return {}; } - void operator^=(__attribute__((unused)) const bb::fr& other){ - info("Not compatible with Finite Field"); - } - void operator<(__attribute__((unused)) const bb::fr& other) const{ - info("Not compatible with Finite Field"); - } - void operator<=(__attribute__((unused)) const bb::fr& other) const{ - info("Not compatible with Finite Field"); - } - void operator>(__attribute__((unused)) const bb::fr& other) const{ - info("Not compatible with Finite Field"); - } - void operator>=(__attribute__((unused)) const bb::fr& other) const{ - info("Not compatible with Finite Field"); - } + void operator^=(__attribute__((unused)) const bb::fr& other) { info("Not compatible with Finite Field"); } + void operator<(__attribute__((unused)) const bb::fr& other) const { info("Not compatible with Finite Field"); } + void operator<=(__attribute__((unused)) const bb::fr& other) const { info("Not compatible with Finite Field"); } + void operator>(__attribute__((unused)) const bb::fr& other) const { info("Not compatible with Finite Field"); } + void operator>=(__attribute__((unused)) const bb::fr& other) const { info("Not compatible with Finite Field"); } }; FFTerm operator+(const bb::fr& lhs, const FFTerm& rhs); diff --git a/barretenberg/cpp/src/barretenberg/smt_verification/terms/ffterm.test.cpp b/barretenberg/cpp/src/barretenberg/smt_verification/terms/ffterm.test.cpp index 3d71782f9789..08c987114b09 100644 --- a/barretenberg/cpp/src/barretenberg/smt_verification/terms/ffterm.test.cpp +++ b/barretenberg/cpp/src/barretenberg/smt_verification/terms/ffterm.test.cpp @@ -21,7 +21,7 @@ TEST(FFTerm, addition) FFTerm y = FFTerm::Var("y", &s); FFTerm bval = FFTerm(b, &s); FFTerm z = x + y; - + z == c; x == a; ASSERT_TRUE(s.check()); @@ -42,7 +42,7 @@ TEST(FFTerm, subtraction) FFTerm y = FFTerm::Var("y", &s); FFTerm bval = FFTerm(b, &s); FFTerm z = x - y; - + z == c; x == a; ASSERT_TRUE(s.check()); @@ -63,7 +63,7 @@ TEST(FFTerm, multiplication) FFTerm y = FFTerm::Var("y", &s); FFTerm bval = FFTerm(b, &s); FFTerm z = x * y; - + z == c; x == a; ASSERT_TRUE(s.check()); @@ -84,7 +84,7 @@ TEST(FFTerm, division) FFTerm y = FFTerm::Var("y", &s); FFTerm bval = FFTerm(b, &s); FFTerm z = x / y; - + z == c; x == a; ASSERT_TRUE(s.check());