diff --git a/barretenberg/cpp/scripts/test_civc_standalone_vks_havent_changed.sh b/barretenberg/cpp/scripts/test_civc_standalone_vks_havent_changed.sh index 99500dcc7bac..eea7d277865c 100755 --- a/barretenberg/cpp/scripts/test_civc_standalone_vks_havent_changed.sh +++ b/barretenberg/cpp/scripts/test_civc_standalone_vks_havent_changed.sh @@ -11,7 +11,7 @@ cd .. # - Generate a hash for versioning: sha256sum bb-civc-inputs.tar.gz # - Upload the compressed results: aws s3 cp bb-civc-inputs.tar.gz s3://aztec-ci-artifacts/protocol/bb-civc-inputs-[hash(0:8)].tar.gz # Note: In case of the "Test suite failed to run ... Unexpected token 'with' " error, need to run: docker pull aztecprotocol/build:3.0 -pinned_civc_inputs_url="https://aztec-ci-artifacts.s3.us-east-2.amazonaws.com/protocol/bb-civc-inputs-95b3f0bb.tar.gz" +pinned_civc_inputs_url="https://aztec-ci-artifacts.s3.us-east-2.amazonaws.com/protocol/bb-civc-inputs-4d015f03.tar.gz" # For easily rerunning the inputs generation if [[ "${1:-}" == "--update-inputs" ]]; then diff --git a/barretenberg/cpp/src/barretenberg/stdlib/primitives/bool/bool.cpp b/barretenberg/cpp/src/barretenberg/stdlib/primitives/bool/bool.cpp index 522c2c4a0848..5bd05826fede 100644 --- a/barretenberg/cpp/src/barretenberg/stdlib/primitives/bool/bool.cpp +++ b/barretenberg/cpp/src/barretenberg/stdlib/primitives/bool/bool.cpp @@ -12,65 +12,75 @@ using namespace bb; namespace bb::stdlib { +/** + * @brief Construct a constant `bool_t` object from a `bool` value + */ template bool_t::bool_t(const bool value) - : context(nullptr) - , witness_bool(value) - , witness_inverted(false) - , witness_index(IS_CONSTANT) + : witness_bool(value) {} +/** + * @brief Construct a constant `bool_t` object with a given Builder argument, its value is `false`. + */ template bool_t::bool_t(Builder* parent_context) : context(parent_context) -{ - witness_bool = false; - witness_inverted = false; - witness_index = IS_CONSTANT; -} +{} +/** + * @brief Construct a `bool_t` object from a witness, note that the value stored at `witness_index` is constrained to be + * 0 or 1. + */ template bool_t::bool_t(const witness_t& value) : context(value.context) { - ASSERT((value.witness == bb::fr::zero()) || (value.witness == bb::fr::one())); + ASSERT((value.witness == bb::fr::zero()) || (value.witness == bb::fr::one()), + "bool_t: witness value is not 0 or 1"); witness_index = value.witness_index; + // Constrain x := other.witness by the relation x^2 = x context->create_bool_gate(witness_index); witness_bool = (value.witness == bb::fr::one()); witness_inverted = false; set_free_witness_tag(); } - +/** + * @brief Construct a constant `bool_t` object from a `bool` value with a given Builder argument. + */ template bool_t::bool_t(Builder* parent_context, const bool value) : context(parent_context) -{ - context = parent_context; - witness_index = IS_CONSTANT; - witness_bool = value; - witness_inverted = false; -} + , witness_bool(value) +{} +/** + * @brief Copy constructor + */ template bool_t::bool_t(const bool_t& other) : context(other.context) -{ - witness_index = other.witness_index; - witness_bool = other.witness_bool; - witness_inverted = other.witness_inverted; - tag = other.tag; -} + , witness_bool(other.witness_bool) + , witness_inverted(other.witness_inverted) + , witness_index(other.witness_index) + , tag(other.tag) +{} +/** + * @brief Move constructor + */ template bool_t::bool_t(bool_t&& other) : context(other.context) -{ - witness_index = other.witness_index; - witness_bool = other.witness_bool; - witness_inverted = other.witness_inverted; - tag = other.tag; -} + , witness_bool(other.witness_bool) + , witness_inverted(other.witness_inverted) + , witness_index(other.witness_index) + , tag(other.tag) +{} +/** + * @brief Assigns a native `bool` to `bool_t` object. + */ template bool_t& bool_t::operator=(const bool other) { context = nullptr; @@ -80,6 +90,9 @@ template bool_t& bool_t::operator=(const bo return *this; } +/** + * @brief Assigns a `bool_t` to a `bool_t` object. + */ template bool_t& bool_t::operator=(const bool_t& other) { context = other.context; @@ -90,6 +103,9 @@ template bool_t& bool_t::operator=(const bo return *this; } +/** + * @brief Assigns a `bool_t` to a `bool_t` object. + */ template bool_t& bool_t::operator=(bool_t&& other) { context = other.context; @@ -99,31 +115,37 @@ template bool_t& bool_t::operator=(bool_t&& tag = other.tag; return *this; } - +/** + * @brief Assigns a `witness_t` to a `bool_t`. As above, he value stored at `witness_index` is constrained to be + * 0 or 1. + */ template bool_t& bool_t::operator=(const witness_t& other) { ASSERT((other.witness == bb::fr::one()) || (other.witness == bb::fr::zero())); context = other.context; - witness_bool = (other.witness == bb::fr::zero()) ? false : true; + witness_bool = other.witness == bb::fr::one(); witness_index = other.witness_index; witness_inverted = false; + // Constrain x := other.witness by the relation x^2 = x context->create_bool_gate(witness_index); set_free_witness_tag(); return *this; } +/** + * @brief Implements AND in circuit + */ template bool_t bool_t::operator&(const bool_t& other) const { - bool_t result(context == nullptr ? other.context : context); + bool_t result(context ? context : other.context); bool left = witness_inverted ^ witness_bool; bool right = other.witness_inverted ^ other.witness_bool; + result.witness_bool = left && right; - ASSERT(result.context || (witness_index == IS_CONSTANT && other.witness_index == IS_CONSTANT)); - if (witness_index != IS_CONSTANT && other.witness_index != IS_CONSTANT) { - result.witness_bool = left & right; + ASSERT(result.context || (is_constant() && other.is_constant())); + if (!is_constant() && !other.is_constant()) { bb::fr value = result.witness_bool ? bb::fr::one() : bb::fr::zero(); result.witness_index = context->add_variable(value); - result.witness_inverted = false; /** * A bool can be represented by a witness value `w` and an 'inverted' flag `i` @@ -149,260 +171,209 @@ template bool_t bool_t::operator&(const boo * + w_b.(i_a.(1 - 2.i_b)) -> q_2 coefficient * + i_a.i_b -> q_c coefficient * + * Note that since the value of the product above is always boolean, we don't need to add an explicit range + * constraint for `result`. **/ - int i_a(witness_inverted); - int i_b(other.witness_inverted); - - fr qm(1 - 2 * i_b - 2 * i_a + 4 * i_a * i_b); - fr q1(i_b * (1 - 2 * i_a)); - fr q2(i_a * (1 - 2 * i_b)); - fr q3(-1); - fr qc(i_a * i_b); - context->create_poly_gate({ - witness_index, - other.witness_index, - result.witness_index, - qm, - q1, - q2, - q3, - qc, - }); - } else if (witness_index != IS_CONSTANT && other.witness_index == IS_CONSTANT) { - if (other.witness_bool ^ other.witness_inverted) { - result = bool_t(*this); - } else { - result.witness_bool = false; - result.witness_inverted = false; - result.witness_index = IS_CONSTANT; - } - } else if (witness_index == IS_CONSTANT && other.witness_index != IS_CONSTANT) { - if (witness_bool ^ witness_inverted) { - result = bool_t(other); - } else { - result.witness_bool = false; - result.witness_inverted = false; - result.witness_index = IS_CONSTANT; - } - } else { - result.witness_bool = left & right; - result.witness_index = IS_CONSTANT; - result.witness_inverted = false; + int i_a(static_cast(witness_inverted)); + int i_b(static_cast(other.witness_inverted)); + + fr q_m{ 1 - 2 * i_b - 2 * i_a + 4 * i_a * i_b }; + fr q_l{ i_b * (1 - 2 * i_a) }; + fr q_r{ i_a * (1 - 2 * i_b) }; + fr q_o{ -1 }; + fr q_c{ i_a * i_b }; + + context->create_poly_gate( + { witness_index, other.witness_index, result.witness_index, q_m, q_l, q_r, q_o, q_c }); + } else if (!is_constant() && other.is_constant()) { + ASSERT(!other.witness_inverted); + // If rhs is a constant true, the output is determined by the lhs. Otherwise the output is a constant + // `false`. + result = other.witness_bool ? *this : other; + + } else if (is_constant() && !other.is_constant()) { + ASSERT(!witness_inverted); + // If lhs is a constant true, the output is determined by the rhs. Otherwise the output is a constant + // `false`. + result = witness_bool ? other : *this; } + result.tag = OriginTag(tag, other.tag); return result; } +/** + * @brief Implements OR in circuit + */ template bool_t bool_t::operator|(const bool_t& other) const { - bool_t result(context == nullptr ? other.context : context); + bool_t result(context ? context : other.context); - ASSERT(result.context || (witness_index == IS_CONSTANT && other.witness_index == IS_CONSTANT)); + ASSERT(result.context || (is_constant() && other.is_constant())); result.witness_bool = (witness_bool ^ witness_inverted) | (other.witness_bool ^ other.witness_inverted); bb::fr value = result.witness_bool ? bb::fr::one() : bb::fr::zero(); - result.witness_inverted = false; - if ((other.witness_index != IS_CONSTANT) && (witness_index != IS_CONSTANT)) { + if (!is_constant() && !other.is_constant()) { result.witness_index = context->add_variable(value); - // result = A + B - AB, where A,B are the "real" values of the variables. But according to whether - // witness_inverted flag is true, we need to invert the input. Hence, we look at four cases, and compute the - // relevent coefficients of the selector q_1,q_2,q_m,q_c in each case - bb::fr multiplicative_coefficient; - bb::fr left_coefficient; - bb::fr right_coefficient; - bb::fr constant_coefficient; - // a inverted: (1-a) + b - (1-a)b = 1-a+ab - // ==> q_1=-1,q_2=0,q_m=1,q_c=1 - if (witness_inverted && !other.witness_inverted) { - multiplicative_coefficient = bb::fr::one(); - left_coefficient = bb::fr::neg_one(); - right_coefficient = bb::fr::zero(); - constant_coefficient = bb::fr::one(); - } - // b inverted: a + (1-b) - a(1-b) = 1-b+ab - // ==> q_1=0,q_2=-1,q_m=1,q_c=1 - else if (!witness_inverted && other.witness_inverted) { - multiplicative_coefficient = bb::fr::one(); - left_coefficient = bb::fr::zero(); - right_coefficient = bb::fr::neg_one(); - constant_coefficient = bb::fr::one(); - } - // Both inverted: (1 - a) + (1 - b) - (1 - a)(1 - b) = 2 - a - b - (1 -a -b +ab) = 1 - ab - // ==> q_m=-1,q_1=0,q_2=0,q_c=1 - else if (witness_inverted && other.witness_inverted) { - multiplicative_coefficient = bb::fr::neg_one(); - left_coefficient = bb::fr::zero(); - right_coefficient = bb::fr::zero(); - constant_coefficient = bb::fr::one(); - } - // No inversions: a + b - ab ==> q_m=-1,q_1=1,q_2=1,q_c=0 - else { - multiplicative_coefficient = bb::fr::neg_one(); - left_coefficient = bb::fr::one(); - right_coefficient = bb::fr::one(); - constant_coefficient = bb::fr::zero(); - } - context->create_poly_gate({ witness_index, - other.witness_index, - result.witness_index, - multiplicative_coefficient, - left_coefficient, - right_coefficient, - bb::fr::neg_one(), - constant_coefficient }); - } else if (witness_index != IS_CONSTANT && other.witness_index == IS_CONSTANT) { - if (other.witness_bool ^ other.witness_inverted) { - result.witness_index = IS_CONSTANT; - result.witness_bool = true; - result.witness_inverted = false; - } else { - result = bool_t(*this); - } - } else if (witness_index == IS_CONSTANT && other.witness_index != IS_CONSTANT) { - if (witness_bool ^ witness_inverted) { - result.witness_index = IS_CONSTANT; - result.witness_bool = true; - result.witness_inverted = false; - } else { - result = bool_t(other); - } - } else { - result.witness_inverted = false; - result.witness_index = IS_CONSTANT; + // Let + // a := lhs = *this; + // b := rhs = other; + // The result is given by + // a + b - a * b = [-(1 - 2*i_a) * (1 - 2*i_b)] * w_a w_b + + // [(1 - 2 * i_a) * (1 - i_b)] * w_a + // [(1 - 2 * i_b) * (1 - i_a)] * w_b + // [i_a + i_b - i_a * i_b] * 1 + const int rhs_inverted = static_cast(other.witness_inverted); + const int lhs_inverted = static_cast(witness_inverted); + + bb::fr q_m{ -(1 - 2 * rhs_inverted) * (1 - 2 * lhs_inverted) }; + bb::fr q_l{ (1 - 2 * lhs_inverted) * (1 - rhs_inverted) }; + bb::fr q_r{ (1 - lhs_inverted) * (1 - 2 * rhs_inverted) }; + bb::fr q_o{ bb::fr::neg_one() }; + bb::fr q_c{ rhs_inverted + lhs_inverted - rhs_inverted * lhs_inverted }; + + // Let r := a | b; + // Constrain + // q_m * w_a * w_b + q_l * w_a + q_r * w_b + q_o * r + q_c = 0 + context->create_poly_gate( + { witness_index, other.witness_index, result.witness_index, q_m, q_l, q_r, q_o, q_c }); + } else if (!is_constant() && other.is_constant()) { + ASSERT(other.witness_inverted == false); + + // If we are computing a | b and b is a constant `true`, the result is a constant `true` that does not + // depend on `a`. + result = other.witness_bool ? other : *this; + + } else if (is_constant() && !other.is_constant()) { + // If we are computing a | b and `a` is a constant `true`, the result is a constant `true` that does not + // depend on `b`. + ASSERT(witness_inverted == false); + result = witness_bool ? *this : other; } result.tag = OriginTag(tag, other.tag); return result; } +/** + * @brief Implements XOR in circuit. + */ template bool_t bool_t::operator^(const bool_t& other) const { bool_t result(context == nullptr ? other.context : context); - ASSERT(result.context || (witness_index == IS_CONSTANT && other.witness_index == IS_CONSTANT)); + ASSERT(result.context || (is_constant() && other.is_constant())); result.witness_bool = (witness_bool ^ witness_inverted) ^ (other.witness_bool ^ other.witness_inverted); bb::fr value = result.witness_bool ? bb::fr::one() : bb::fr::zero(); - result.witness_inverted = false; - if ((other.witness_index != IS_CONSTANT) && (witness_index != IS_CONSTANT)) { + if (!is_constant() && !other.is_constant()) { result.witness_index = context->add_variable(value); - // norm a, norm b: a + b - 2ab - // inv a, norm b: (1 - a) + b - 2(1 - a)b = 1 - a - b + 2ab - // norm a, inv b: a + (1 - b) - 2(a)(1 - b) = 1 - a - b + 2ab - // inv a, inv b: (1 - a) + (1 - b) - 2(1 - a)(1 - b) = a + b - 2ab - bb::fr multiplicative_coefficient; - bb::fr left_coefficient; - bb::fr right_coefficient; - bb::fr constant_coefficient; - if ((witness_inverted && other.witness_inverted) || (!witness_inverted && !other.witness_inverted)) { - multiplicative_coefficient = (bb::fr::neg_one() + bb::fr::neg_one()); - left_coefficient = bb::fr::one(); - right_coefficient = bb::fr::one(); - constant_coefficient = bb::fr::zero(); - } else { - multiplicative_coefficient = bb::fr::one() + bb::fr::one(); - left_coefficient = bb::fr::neg_one(); - right_coefficient = bb::fr::neg_one(); - constant_coefficient = bb::fr::one(); - } - context->create_poly_gate({ witness_index, - other.witness_index, - result.witness_index, - multiplicative_coefficient, - left_coefficient, - right_coefficient, - bb::fr::neg_one(), - constant_coefficient }); - } else if (witness_index != IS_CONSTANT && other.witness_index == IS_CONSTANT) { + // Let + // a := lhs = *this; + // b := rhs = other; + // The result is given by + // a + b - 2 * a * b = [-2 *(1 - 2*i_a) * (1 - 2*i_b)] * w_a w_b + + // [(1 - 2 * i_a) * (1 - 2 * i_b)] * w_a + // [(1 - 2 * i_b) * (1 - 2 * i_a)] * w_b + // [i_a + i_b - 2 * i_a * i_b] * 1] + const int rhs_inverted = static_cast(other.witness_inverted); + const int lhs_inverted = static_cast(witness_inverted); + // Compute the value that's being used in several selectors + const int aux_prod = (1 - 2 * rhs_inverted) * (1 - 2 * lhs_inverted); + + bb::fr q_m{ -2 * aux_prod }; + bb::fr q_l{ aux_prod }; + bb::fr q_r{ aux_prod }; + bb::fr q_o{ bb::fr::neg_one() }; + bb::fr q_c{ lhs_inverted + rhs_inverted - 2 * rhs_inverted * lhs_inverted }; + + // Let r := a ^ b; + // Constrain + // q_m * w_a * w_b + q_l * w_a + q_r * w_b + q_o * r + q_c = 0 + context->create_poly_gate( + { witness_index, other.witness_index, result.witness_index, q_m, q_l, q_r, q_o, q_c }); + } else if (!is_constant() && other.is_constant()) { // witness ^ 1 = !witness - if (other.witness_bool ^ other.witness_inverted) { - result = !bool_t(*this); - } else { - result = bool_t(*this); - } - } else if (witness_index == IS_CONSTANT && other.witness_index != IS_CONSTANT) { - if (witness_bool ^ witness_inverted) { - result = !bool_t(other); - } else { - result = bool_t(other); - } - } else { - result.witness_inverted = false; - result.witness_index = IS_CONSTANT; + ASSERT(other.witness_inverted == false); + result = other.witness_bool ? !*this : *this; + + } else if (is_constant() && !other.is_constant()) { + ASSERT(witness_inverted == false); + result = witness_bool ? !other : other; } result.tag = OriginTag(tag, other.tag); return result; } - +/** + * @brief Implements negation in circuit. + */ template bool_t bool_t::operator!() const { bool_t result(*this); if (result.is_constant()) { + ASSERT(!witness_inverted); + // Negate the value of a constant bool_t element. result.witness_bool = !result.witness_bool; - return result; + } else { + // Negate the `inverted` flag of a witnees bool_t element. + result.witness_inverted = !result.witness_inverted; } - result.witness_inverted = !result.witness_inverted; return result; } +/** + * @brief Implements equality operator in circuit. + */ template bool_t bool_t::operator==(const bool_t& other) const { - ASSERT(context || other.context || (witness_index == IS_CONSTANT && other.witness_index == IS_CONSTANT)); - if ((other.witness_index == IS_CONSTANT) && (witness_index == IS_CONSTANT)) { - bool_t result(context == nullptr ? other.context : context); - result.witness_bool = (witness_bool ^ witness_inverted) == (other.witness_bool ^ other.witness_inverted); - result.witness_index = IS_CONSTANT; - result.set_origin_tag(OriginTag(get_origin_tag(), other.get_origin_tag())); - return result; - } else if ((witness_index != IS_CONSTANT) && (other.witness_index == IS_CONSTANT)) { - if (other.witness_bool ^ other.witness_inverted) { - return (*this); - } else { - return !(*this); - } - } else if ((witness_index == IS_CONSTANT) && (other.witness_index != IS_CONSTANT)) { - if (witness_bool ^ witness_inverted) { - return other; - } else { - return !(other); - } - } else { - bool_t result(context == nullptr ? other.context : context); - result.witness_bool = (witness_bool ^ witness_inverted) == (other.witness_bool ^ other.witness_inverted); - bb::fr value = result.witness_bool ? bb::fr::one() : bb::fr::zero(); + ASSERT(context || other.context || (is_constant() && other.is_constant())); + bool_t result(context ? context : other.context); + + result.witness_bool = (witness_bool ^ witness_inverted) == (other.witness_bool ^ other.witness_inverted); + if (!is_constant() && !other.is_constant()) { + const bb::fr value = result.witness_bool ? bb::fr::one() : bb::fr::zero(); + result.witness_index = context->add_variable(value); - // norm a, norm b or both inv: 1 - a - b + 2ab - // inv a or inv b = a + b - 2ab - bb::fr multiplicative_coefficient; - bb::fr left_coefficient; - bb::fr right_coefficient; - bb::fr constant_coefficient; - if ((witness_inverted && other.witness_inverted) || (!witness_inverted && !other.witness_inverted)) { - multiplicative_coefficient = bb::fr::one() + bb::fr::one(); - left_coefficient = bb::fr::neg_one(); - right_coefficient = bb::fr::neg_one(); - constant_coefficient = bb::fr::one(); - } else { - multiplicative_coefficient = (bb::fr::neg_one() + bb::fr::neg_one()); - left_coefficient = bb::fr::one(); - right_coefficient = bb::fr::one(); - constant_coefficient = bb::fr::zero(); - } - context->create_poly_gate({ witness_index, - other.witness_index, - result.witness_index, - multiplicative_coefficient, - left_coefficient, - right_coefficient, - bb::fr::neg_one(), - constant_coefficient }); - - result.tag = OriginTag(tag, other.tag); - return result; + + // Let + // a := lhs = *this; + // b := rhs = other; + // The result is given by + // 1 - a - b + 2 a * b = [2 *(1 - 2*i_a) * (1 - 2*i_b)] * w_a w_b + + // [-(1 - 2 * i_a) * (1 - 2 * i_b)] * w_a + + // [-(1 - 2 * i_b) * (1 - 2 * i_a)] * w_b + + // [1 - i_a - i_b + 2 * i_a * i_b] * 1 + const int rhs_inverted = static_cast(other.witness_inverted); + const int lhs_inverted = static_cast(witness_inverted); + // Compute the value that's being used in several selectors + const int aux_prod = (1 - 2 * rhs_inverted) * (1 - 2 * lhs_inverted); + bb::fr q_m{ 2 * aux_prod }; + bb::fr q_l{ -aux_prod }; + bb::fr q_r{ -aux_prod }; + bb::fr q_o{ bb::fr::neg_one() }; + bb::fr q_c{ 1 - lhs_inverted - rhs_inverted + 2 * rhs_inverted * lhs_inverted }; + + context->create_poly_gate( + { witness_index, other.witness_index, result.witness_index, q_m, q_r, q_l, q_o, q_c }); + + } else if (!is_constant() && (other.is_constant())) { + // Compare *this with a constant other. If other == true, then we're checking *this == true. In this case we + // propagate *this without adding extra constraints, otherwise (if other = false), we propagate !*this. + ASSERT(other.witness_inverted == false); + result = other.witness_bool ? *this : !(*this); + } else if (is_constant() && !other.is_constant()) { + // Completely analogous to the previous case. + ASSERT(witness_inverted == false); + result = witness_bool ? other : !other; } -} + result.tag = OriginTag(tag, other.tag); + return result; +} +/** + * @brief Implements the `not equal` operator in circuit. + */ template bool_t bool_t::operator!=(const bool_t& other) const { return operator^(other); @@ -418,6 +389,9 @@ template bool_t bool_t::operator||(const bo return operator|(other); } +/** + * @brief Implements copy constraint for `bool_t` elements. + */ template void bool_t::assert_equal(const bool_t& rhs, std::string const& msg) const { const bool_t lhs = *this; @@ -426,16 +400,18 @@ template void bool_t::assert_equal(const bool_t& rhs if (lhs.is_constant() && rhs.is_constant()) { ASSERT(lhs.get_value() == rhs.get_value()); } else if (lhs.is_constant()) { + ASSERT(!lhs.witness_inverted); // if rhs is inverted, flip the value of the lhs constant - bool lhs_value = rhs.witness_inverted ? !lhs.get_value() : lhs.get_value(); + const bool lhs_value = rhs.witness_inverted ? !lhs.witness_bool : lhs.witness_bool; ctx->assert_equal_constant(rhs.witness_index, lhs_value, msg); } else if (rhs.is_constant()) { + ASSERT(!rhs.witness_inverted); // if lhs is inverted, flip the value of the rhs constant - bool rhs_value = lhs.witness_inverted ? !rhs.get_value() : rhs.get_value(); + const bool rhs_value = lhs.witness_inverted ? !rhs.witness_bool : rhs.witness_bool; ctx->assert_equal_constant(lhs.witness_index, rhs_value, msg); } else { - auto left = lhs; - auto right = rhs; + bool_t left = lhs; + bool_t right = rhs; // we need to normalize iff lhs or rhs has an inverted witness (but not both) if (lhs.witness_inverted ^ rhs.witness_inverted) { left = left.normalize(); @@ -445,7 +421,9 @@ template void bool_t::assert_equal(const bool_t& rhs } } -// if predicate == true then return lhs, else return rhs +/** + * @brief Implements the ternary operator - if predicate == true then return lhs, else return rhs + */ template bool_t bool_t::conditional_assign(const bool_t& predicate, const bool_t& lhs, @@ -458,120 +436,72 @@ bool_t bool_t::conditional_assign(const bool_t& predi } bool same = lhs.witness_index == rhs.witness_index; - bool witness_same = same && lhs.witness_index != IS_CONSTANT && (lhs.witness_inverted == rhs.witness_inverted); - bool const_same = same && (lhs.witness_index == IS_CONSTANT) && (lhs.witness_bool == rhs.witness_bool); + bool witness_same = same && !lhs.is_constant() && (lhs.witness_inverted == rhs.witness_inverted); + bool const_same = same && lhs.is_constant() && (lhs.witness_bool == rhs.witness_bool); if (witness_same || const_same) { return lhs; } return (predicate && lhs) || (!predicate && rhs); } +/** + * @brief Implements implication operator in circuit. + */ template bool_t bool_t::implies(const bool_t& other) const { + // Thanks to negation operator being free, this computation requires at most 1 gate. return (!(*this) || other); // P => Q is equiv. to !P || Q (not(P) or Q). } +/** + * @brief Constrains the (a => b) == true. + */ template void bool_t::must_imply(const bool_t& other, std::string const& msg) const { - (this->implies(other)).assert_equal(true, msg); + implies(other).assert_equal(true, msg); } /** - * Process many implications all at once, for readablity, and as an optimization. - * @param conds - each pair is a boolean condition that we want to constrain to be "implied", and an error message if it - * is not implied. - * - * Why this works: - * (P => Q) && (P => R) - * <=> (!P || Q) && (!P || R) - * <=> !P || (Q && R) [by distributivity of propositional logic] - * <=> P => (Q && R) [a.k.a. distribution of implication over conjunction] + @brief Implements a "double-implication" (<=>), a.k.a "iff", a.k.a. "biconditional" */ -template -void bool_t::must_imply(const std::vector>& conds) const -{ - // Extract the builder - const bool_t this_bool = *this; - Builder* ctx = this_bool.get_context(); - bool builder_found = (ctx != nullptr); - for (size_t i = 0; i < conds.size(); i++) { - if (!builder_found) { - ctx = conds[i].first.get_context(); - builder_found = (ctx != nullptr); - } - } - - // If no builder is found, all of the bool_t's must be constants. - // In that case, we enforce a static assertion to check must_imply condition holds. - // If all of your inputs do this function are constants and they don't obey a condition, - // this function will panic at those static assertions. - if (!builder_found) { - bool is_const = this_bool.is_constant(); - bool result = !this_bool.get_value(); - bool acc = true; - for (size_t i = 0; i < conds.size(); i++) { - is_const &= conds[i].first.is_constant(); - acc &= conds[i].first.get_value(); - } - result |= acc; - ASSERT(is_const == true); - ASSERT(result == true); - } - - bool_t acc = witness_t(ctx, true); // will accumulate the conjunctions of each condition (i.e. `&&` of each) - const bool this_val = this->get_value(); - bool error_found = false; - std::string error_msg; - - for (size_t i = 0; i < conds.size(); ++i) { - const bool_t& cond = conds[i].first; - const std::string& msg = conds[i].second; - const bool cond_val = cond.get_value(); - - // If this does NOT imply that, throw the error msg of that condition. - if (!(!this_val || cond_val) && !error_found) { - error_found = true; - error_msg = msg; - } - - acc &= cond; - } - - (this->implies(acc)).assert_equal(true, format("multi implication fail: ", error_msg)); -} - -// A "double-implication" (<=>), -// a.k.a "iff", a.k.a. "biconditional" template bool_t bool_t::implies_both_ways(const bool_t& other) const { - return (!(*this) ^ other); // P <=> Q is equiv. to !(P ^ Q) (not(P xor Q)). + return !((*this) ^ other); // P <=> Q is equiv. to !(P ^ Q) (not(P xor Q)). } +/** + * @brief A bool_t element is **normalized** if `witness_inverted == false`. For a given `*this`, output its normalized + * version. + * @warning The witness index of *this as well as its `witness_inverted` flag are re-written. + */ template bool_t bool_t::normalize() const { if (is_constant()) { - ASSERT(!this->witness_inverted); + ASSERT(!witness_inverted); return *this; } - bb::fr value = witness_bool ^ witness_inverted ? bb::fr::one() : bb::fr::zero(); - - uint32_t new_witness = context->add_variable(value); - uint32_t new_value = witness_bool ^ witness_inverted; - - bb::fr q_l; - bb::fr q_c; + if (!witness_inverted) { + return *this; + } + // Let a := *this, need to constrain a = a_norm + // [1 - 2 i_a] w_a + [-1] w_a_norm + [i_a] = 0 + // ^ ^ ^ + // q_l q_o q_c + const bool value = witness_bool ^ witness_inverted; - q_l = witness_inverted ? bb::fr::neg_one() : bb::fr::one(); - q_c = witness_inverted ? bb::fr::one() : bb::fr::zero(); + uint32_t new_witness = context->add_variable(bb::fr{ static_cast(value) }); + const int inverted = static_cast(witness_inverted); + bb::fr q_l{ 1 - 2 * inverted }; + bb::fr q_c{ inverted }; bb::fr q_o = bb::fr::neg_one(); bb::fr q_m = bb::fr::zero(); bb::fr q_r = bb::fr::zero(); context->create_poly_gate({ witness_index, witness_index, new_witness, q_m, q_l, q_r, q_o, q_c }); witness_index = new_witness; - witness_bool = new_value; + witness_bool = value; witness_inverted = false; return *this; } diff --git a/barretenberg/cpp/src/barretenberg/stdlib/primitives/bool/bool.hpp b/barretenberg/cpp/src/barretenberg/stdlib/primitives/bool/bool.hpp index 6dff662a2673..8c070b823ade 100644 --- a/barretenberg/cpp/src/barretenberg/stdlib/primitives/bool/bool.hpp +++ b/barretenberg/cpp/src/barretenberg/stdlib/primitives/bool/bool.hpp @@ -10,7 +10,52 @@ #include "barretenberg/transcript/origin_tag.hpp" namespace bb::stdlib { - +/** + * @brief Implements boolean logic in-circuit. + * + * @details + * ## Representing bools in-circuit + * + * To avoid constraining negation operations, we represent an in-circuit boolean \f$ a \f$ by a witness value \f$ w_a + * \f$ and an `witness_inverted` flag \f$ i_a \f$. The value of \f$ a \f$ is defined via the equation: + * + * \f{align}{ w_a \oplus i_a = w_a + i_a - 2 \cdot i_a \cdot w_a \f} + * + * and can be read from the following table + * | w_a | i_a | a = w_a + i_a - 2 i_a w_a | + * | - | - | ------------------------- | + * | 0 | 0 | 0 | + * | 0 | 1 | 1 | + * | 1 | 0 | 1 | + * | 1 | 1 | 0 | + * + * When a new bool_t element \f$ a \f$ is created, its `witness_inverted` flag is set to `false` and + * its `witness_value` is constrained to be \f$ 0 \f$ or \f$ 1\f$. More precisely, if \f$ a \f$ is a witness, then we + * add a boolean constraint ensuring \f$ w_a^2 = w_a \f$, if \f$ a \f$ is a constant bool_t element, then it's checked + * by an **ASSERT**. + * + * To negate \f$ a \f$ we simply flip the flag. Other basic operations are deduced from their algebraic representations + * and the result is constrained to satisfy corresponding algebraic equation. + * + * ## Detailed example of an operation (logical OR) + * + * For example, to produce \f$ a || b \f$ in circuit, we compute + * \f{align}{ + * a + b - a \cdot b = ( w_a \cdot (1- 2 i_a) + i_a) + ( w_b \cdot (1 - 2 i_b) + i_b) - + * ( w_a \cdot (1-2 i_a) + i_a) ( w_b \cdot (1 - 2 i_b) + i_b) + * \f} + * Thus we can use a `poly` gate to constrain the result of a || b as follows: + * + * \f{align}{ q_m \cdot w_a \cdot w_b + q_l \cdot w_a + q_r \cdot w_b + q_o \cdot (a || b) + q_c = 0\f} + * where + * \f{eqnarray*} q_m &=& -(1 - 2*i_a) * (1 - 2*i_b) \\ + * q_l &=& (1 - 2 * i_a) * (1 - i_b) \\ + * q_r &=& (1 - 2 * i_b) * (1 - i_a) \\ + * q_o &=& -1 \\ + * q_c &=& i_a + i_b - i_a * i_b \f} + * As \f$ w_a \f$ and \f$ w_b \f$ are constrained to be boolean, \f$ i_a \f$, \f$ i_b\f$ are boolean flags, we see that + * \f$ (a || b)^2 = (a || b)\f$ (as a field element). + */ template class bool_t { public: bool_t(const bool value = false); @@ -61,8 +106,6 @@ template class bool_t { void must_imply(const bool_t& other, std::string const& msg = "bool_t::must_imply") const; - void must_imply(const std::vector>& conds) const; - bool get_value() const { return witness_bool ^ witness_inverted; } bool is_constant() const { return witness_index == IS_CONSTANT; } diff --git a/barretenberg/cpp/src/barretenberg/stdlib/primitives/bool/bool.test.cpp b/barretenberg/cpp/src/barretenberg/stdlib/primitives/bool/bool.test.cpp index 0c56a59f11af..fdbd6ade42f4 100644 --- a/barretenberg/cpp/src/barretenberg/stdlib/primitives/bool/bool.test.cpp +++ b/barretenberg/cpp/src/barretenberg/stdlib/primitives/bool/bool.test.cpp @@ -1,16 +1,10 @@ #include "bool.hpp" #include "barretenberg/circuit_checker/circuit_checker.hpp" -#include "barretenberg/stdlib/primitives/byte_array/byte_array.cpp" #include "barretenberg/stdlib/primitives/circuit_builders/circuit_builders.hpp" #include "barretenberg/transcript/origin_tag.hpp" #include #include -#define STDLIB_TYPE_ALIASES \ - using Builder = TypeParam; \ - using witness_ct = stdlib::witness_t; \ - using bool_ct = stdlib::bool_t; - using namespace bb; #pragma GCC diagnostic ignored "-Wunused-const-variable" @@ -19,593 +13,489 @@ namespace { auto& engine = numeric::get_debug_randomness(); } STANDARD_TESTING_TAGS -template class BoolTest : public ::testing::Test {}; - -using CircuitTypes = ::testing::Types; - -TYPED_TEST_SUITE(BoolTest, CircuitTypes); -TYPED_TEST(BoolTest, TestBasicOperations) -{ - - STDLIB_TYPE_ALIASES - auto builder = Builder(); - - auto gates_before = builder.get_estimated_num_finalized_gates(); - - bool_ct a = witness_ct(&builder, bb::fr::one()); - bool_ct b = witness_ct(&builder, bb::fr::zero()); +template class BoolTest : public ::testing::Test { + public: + using Builder = Builder_; + using witness_ct = stdlib::witness_t; + using bool_ct = stdlib::bool_t; - a.set_origin_tag(submitted_value_origin_tag); - b.set_origin_tag(challenge_origin_tag); + // These tree boolean flags cover all possible combinations for a valid input. + struct BoolInput { + bool is_const; // witness_index = IS_CONSTANT + bool value; // w_a + bool is_inverted; // i_a + }; - a = a ^ b; // a = 1 - EXPECT_EQ(a.get_value(), 1); + // A helper to produce all possible inputs for a given operand. + std::array all_inputs = []() { + std::array inputs{}; + size_t idx = 0; + for (bool is_const : { false, true }) { + for (bool value : { false, true }) { + for (bool is_inverted : { false, true }) { + inputs[idx++] = BoolInput{ is_const, value, is_inverted }; + } + } + } + return inputs; + }(); + // A helper to create a bool_t element from the given flags + static bool_ct create_bool_ct(const BoolInput& in, Builder* builder) + { + bool_ct b = in.is_const ? bool_ct(in.value) : witness_ct(builder, in.value); + return in.is_inverted ? !b : b; + }; - // Tags are merged on XOR - EXPECT_EQ(a.get_origin_tag(), first_two_merged_tag); + void test_binary_op(std::string const& op_name, + const std::function& op, + const std::function& expected_op) + { + Builder builder; + + for (auto& lhs : all_inputs) { + for (auto& rhs : all_inputs) { + bool_ct a = create_bool_ct(lhs, &builder); + bool_ct b = create_bool_ct(rhs, &builder); + + size_t num_gates_start = builder.get_estimated_num_finalized_gates(); + + if (!a.is_constant() && !b.is_constant()) { + a.set_origin_tag(submitted_value_origin_tag); + b.set_origin_tag(challenge_origin_tag); + } + bool_ct c = op(a, b); + + bool expected = expected_op(lhs.value ^ lhs.is_inverted, rhs.value ^ rhs.is_inverted); + + EXPECT_EQ(c.get_value(), expected) + << "Failed on " << op_name << " with inputs: lhs = {const=" << lhs.is_const << ", val=" << lhs.value + << ", inv=" << lhs.is_inverted << "}, rhs = {const=" << rhs.is_const << ", val=" << rhs.value + << ", inv=" << rhs.is_inverted << "}"; + + if (a.is_constant() && b.is_constant()) { + EXPECT_TRUE(c.is_constant()); + } + + if (!a.is_constant() && !b.is_constant()) { + // The result of a binary op on two witnesses must be a witness + EXPECT_TRUE(!c.is_constant()); + // Check that the tags are propagated + EXPECT_EQ(c.get_origin_tag(), first_two_merged_tag); + } + + size_t diff = builder.get_estimated_num_finalized_gates() - num_gates_start; + // An extra gate is created iff both operands are witnesses + EXPECT_EQ(diff, static_cast(!a.is_constant() && !b.is_constant())); + } + } - b = !b; // b = 1 (witness 0) - EXPECT_EQ(b.get_value(), 1); + EXPECT_TRUE(CircuitChecker::check(builder)); + }; - // Tag is preserved on NOT - EXPECT_EQ(b.get_origin_tag(), challenge_origin_tag); + void test_construct_from_const_bool() + { + Builder builder = Builder(); + size_t num_gates_start = builder.get_estimated_num_finalized_gates(); + bool_ct a_true(true); + bool_ct a_false(false); + EXPECT_TRUE(a_true.get_value()); + EXPECT_FALSE(a_false.get_value()); + EXPECT_TRUE(a_true.is_constant() && a_false.is_constant()); + EXPECT_TRUE(!a_true.witness_inverted && !a_false.witness_inverted); + // No gates have been added + EXPECT_TRUE(num_gates_start == builder.get_estimated_num_finalized_gates()); + } - a.set_origin_tag(submitted_value_origin_tag); + void test_construct_from_witness() + { + Builder builder = Builder(); + size_t num_gates_start = builder.get_estimated_num_finalized_gates(); + + bool_ct a_true = witness_ct(&builder, 1); + bool_ct a_false = witness_ct(&builder, 0); + EXPECT_TRUE(a_true.get_value()); + EXPECT_FALSE(a_false.get_value()); + EXPECT_TRUE(!a_true.is_constant() && !a_false.is_constant()); + EXPECT_TRUE(!a_true.witness_inverted && !a_false.witness_inverted); + // Each witness bool must be constrained => expect 2 gates being added + EXPECT_TRUE(builder.get_estimated_num_finalized_gates() - num_gates_start == 2); + EXPECT_TRUE(CircuitChecker::check(builder)); + +#ifndef NDEBUG + // Test failure + bool_ct a_incorrect; + uint256_t random_value(engine.get_random_uint256()); + + if (random_value * random_value - random_value != 0) { + EXPECT_DEATH(a_incorrect = witness_ct(&builder, random_value), + "((other.witness == bb::fr::one()) || (other.witness == bb::fr::zero()))"); + }; +#endif + } + void test_AND() + { + test_binary_op( + "AND", [](const bool_ct& a, const bool_ct& b) { return a & b; }, [](bool a, bool b) { return a && b; }); + } - bool_ct d = (a == b); // - EXPECT_EQ(d.get_value(), 1); + void test_xor() + { + test_binary_op( + "XOR", [](const bool_ct& a, const bool_ct& b) { return a ^ b; }, [](bool a, bool b) { return a ^ b; }); + } - // Tags are merged on == - EXPECT_EQ(d.get_origin_tag(), first_two_merged_tag); + void test_OR() + { + test_binary_op( + "OR", [](const bool_ct& a, const bool_ct& b) { return a || b; }, [](bool a, bool b) { return a || b; }); + } - d = false; // d = 0 - d.set_origin_tag(challenge_origin_tag); - EXPECT_EQ(d.get_value(), 0); + void test_EQ() + { + test_binary_op( + "==", [](const bool_ct& a, const bool_ct& b) { return a == b; }, [](bool a, bool b) { return a == b; }); + } - bool_ct e = a | d; // e = 1 = a - EXPECT_EQ(e.get_value(), 1); + void test_NEQ() + { + test_binary_op( + "!=", [](const bool_ct& a, const bool_ct& b) { return a != b; }, [](bool a, bool b) { return a != b; }); + } - // Tags are merged on OR - EXPECT_EQ(e.get_origin_tag(), first_two_merged_tag); + void test_implies() + { + test_binary_op( + "=>", + [](const bool_ct& a, const bool_ct& b) { return a.implies(b); }, + [](bool a, bool b) { return !a || b; }); + } - bool_ct f = e ^ b; // f = 0 - EXPECT_EQ(f.get_value(), 0); + void test_implies_both_ways() + { + test_binary_op( + "<=>", + [](const bool_ct& a, const bool_ct& b) { return a.implies_both_ways(b); }, + [](bool a, bool b) { return !(a ^ b); }); + } - f.set_origin_tag(challenge_origin_tag); - d = (!f) & a; // d = 1 - EXPECT_EQ(d.get_value(), 1); + void test_must_imply() + { + + for (auto& lhs : all_inputs) { + for (auto& rhs : all_inputs) { + Builder builder; + + bool_ct a = create_bool_ct(lhs, &builder); + bool_ct b = create_bool_ct(rhs, &builder); + + if (a.is_constant() && b.is_constant() && !(!a.get_value() || b.get_value())) { +#ifndef NDEBUG + EXPECT_DEATH(a.must_imply(b), R"(\(lhs\.get_value\(\) == rhs\.get_value\(\)\))"); +#endif + } else { + bool result_is_constant = (!a || b).is_constant(); + + size_t num_gates_start = builder.get_estimated_num_finalized_gates(); + + if (!a.is_constant() && !b.is_constant()) { + a.set_origin_tag(submitted_value_origin_tag); + b.set_origin_tag(challenge_origin_tag); + } + a.must_imply(b); + // !a || b + // b = 1 => + bool expected = !(lhs.value ^ lhs.is_inverted) || rhs.value ^ rhs.is_inverted; + + size_t diff = builder.get_estimated_num_finalized_gates() - num_gates_start; + + if (!a.is_constant() && !b.is_constant()) { + EXPECT_EQ(diff, 2); + } + // Due to optimizations, the result of a => b can be a constant, in this case, the the assert_equal + // reduces to an out-of-circuit ASSERT + if (result_is_constant) { + EXPECT_EQ(diff, 0); + } + + if (!result_is_constant && a.is_constant() && !b.is_constant()) { + // we only add gates if the value `true` is not flipped to `false` and we need to add a new + // constant == 1, which happens iff `b` is not inverted. + EXPECT_EQ(diff, static_cast(!b.witness_inverted)); + } + + if (!result_is_constant && !a.is_constant() && b.is_constant()) { + // we only add gates if the value `true` is not flipped to `false` and we need to add a new + // constant == 1, which happens iff `a` is inverted. + EXPECT_EQ(diff, static_cast(a.witness_inverted)); + } + EXPECT_EQ(CircuitChecker::check(builder), expected); + } + } + } + } - // Tags are merged on AND - EXPECT_EQ(d.get_origin_tag(), first_two_merged_tag); + void test_conditional_assign() + { + for (auto lhs : all_inputs) { + for (auto rhs : all_inputs) { + for (auto predicate : all_inputs) { + Builder builder; + + bool_ct a = create_bool_ct(lhs, &builder); + bool_ct b = create_bool_ct(rhs, &builder); + bool_ct condition = create_bool_ct(predicate, &builder); + + size_t num_gates_start = builder.get_estimated_num_finalized_gates(); + if (!a.is_constant() && !b.is_constant()) { + condition.set_origin_tag(submitted_value_origin_tag); + a.set_origin_tag(challenge_origin_tag); + b.set_origin_tag(next_challenge_tag); + } + + bool_ct result = bool_ct::conditional_assign(condition, a, b); + size_t diff = builder.get_estimated_num_finalized_gates() - num_gates_start; + if (!a.is_constant() && !b.is_constant()) { + EXPECT_EQ(result.get_origin_tag(), first_second_third_merged_tag); + } + bool expected = (condition.get_value()) ? a.get_value() : b.get_value(); + EXPECT_EQ(result.get_value(), expected); + + if (condition.is_constant()) { + EXPECT_EQ(diff, 0); + } + + EXPECT_TRUE(CircuitChecker::check(builder)); + } + } + } + } - bool result = CircuitChecker::check(builder); - EXPECT_EQ(result, true); + void test_normalize() + { + for (auto a_raw : all_inputs) { + auto builder = Builder(); - auto gates_after = builder.get_estimated_num_finalized_gates(); - EXPECT_EQ(gates_after - gates_before, 6UL); -} + bool_ct a = create_bool_ct(a_raw, &builder); -TYPED_TEST(BoolTest, Xor) -{ - STDLIB_TYPE_ALIASES - auto builder = Builder(); - - for (size_t j = 0; j < 4; ++j) { - bool lhs_constant = (bool)(j % 2); - bool rhs_constant = (bool)(j > 1 ? true : false); - - for (size_t i = 0; i < 4; ++i) { - bool a_val = (bool)(i % 2); - bool b_val = (bool)(i > 1 ? true : false); - bool_ct a = lhs_constant ? bool_ct(a_val) : (witness_ct(&builder, a_val)); - bool_ct b = rhs_constant ? bool_ct(b_val) : (witness_ct(&builder, b_val)); - bool_ct c = a ^ b; - EXPECT_EQ(c.get_value(), a.get_value() ^ b.get_value()); + size_t num_gates_start = builder.get_estimated_num_finalized_gates(); + if (!a.is_constant()) { + a.set_origin_tag(submitted_value_origin_tag); + } + bool_ct c = a.normalize(); + EXPECT_EQ(c.get_value(), a.get_value()); + if (!a.is_constant()) { + EXPECT_EQ(c.get_origin_tag(), submitted_value_origin_tag); + } + EXPECT_EQ(c.witness_inverted, false); + size_t diff = builder.get_estimated_num_finalized_gates() - num_gates_start; + // Note that although `normalize()` returns value, it flips the `witness_inverted` flag of `a` if it was + // `true`. + EXPECT_EQ(diff, static_cast(!a.is_constant() && a_raw.is_inverted)); + EXPECT_TRUE(CircuitChecker::check(builder)); } } - bool result = CircuitChecker::check(builder); - EXPECT_EQ(result, true); -} - -TYPED_TEST(BoolTest, XorConstants) -{ - STDLIB_TYPE_ALIASES - auto builder = Builder(); - for (size_t i = 0; i < 32; ++i) { - bool_ct a = witness_ct(&builder, (bool)(i % 2)); - bool_ct b = witness_ct(&builder, (bool)(i % 3 == 1)); - a ^ b; - } - for (size_t i = 0; i < 32; ++i) { - if (i % 2 == 0) { - bool_ct a = witness_ct(&builder, (bool)(i % 2)); - bool_ct b(&builder, (bool)(i % 3 == 1)); - a ^ b; - } else { - bool_ct a(&builder, (bool)(i % 2)); - bool_ct b = witness_ct(&builder, (bool)(i % 3 == 1)); - a ^ b; + void test_assert_equal() + { + + for (auto lhs : all_inputs) { + for (auto rhs : all_inputs) { + + Builder builder; + + bool_ct a = create_bool_ct(lhs, &builder); + bool_ct b = create_bool_ct(rhs, &builder); + + bool failed = a.get_value() != b.get_value(); + + if (!a.is_constant() && !b.is_constant()) { + a.assert_equal(b); + // CircuitChecker is not verifying the permutation relation + EXPECT_EQ(builder.failed(), failed); + } else if (!a.is_constant() || !b.is_constant()) { + a.assert_equal(b); + EXPECT_EQ(CircuitChecker::check(builder), !failed); + } else { + if (failed) { +#ifndef NDEBUG + EXPECT_DEATH(a.assert_equal(b), R"(\(lhs\.get_value\(\) == rhs\.get_value\(\)\))"); +#endif + } + } + } } } - bool result = CircuitChecker::check(builder); - EXPECT_EQ(result, true); -} + void test_basic_operations_tags() + { + auto builder = Builder(); -TYPED_TEST(BoolTest, XorTwinConstants) -{ - STDLIB_TYPE_ALIASES - auto builder = Builder(); - - bool_ct c; - for (size_t i = 0; i < 32; ++i) { - bool_ct a(&builder, (i % 1) == 0); - bool_ct b(&builder, (i % 1) == 1); - c = c ^ a ^ b; - } - c = c ^ bool_ct(witness_ct(&builder, true)); - for (size_t i = 0; i < 32; ++i) { - if (i % 2 == 0) { - bool_ct a = witness_ct(&builder, (bool)(i % 2)); - bool_ct b(&builder, (bool)(i % 3 == 1)); - c = c ^ a ^ b; - } else { - bool_ct a(&builder, (bool)(i % 2)); - bool_ct b = witness_ct(&builder, (bool)(i % 3 == 1)); - c = c ^ a ^ b; - } - } + auto gates_before = builder.get_estimated_num_finalized_gates(); - bool result = CircuitChecker::check(builder); - EXPECT_EQ(result, true); -} + bool_ct a = witness_ct(&builder, bb::fr::one()); + bool_ct b = witness_ct(&builder, bb::fr::zero()); -TYPED_TEST(BoolTest, LogicalAnd) -{ - STDLIB_TYPE_ALIASES - auto builder = Builder(); + a.set_origin_tag(submitted_value_origin_tag); + b.set_origin_tag(challenge_origin_tag); - bool_ct a = witness_ct(&builder, 1); - bool_ct b = witness_ct(&builder, 1); + a = a ^ b; // a = 1 + EXPECT_EQ(a.get_value(), 1); - a.set_origin_tag(submitted_value_origin_tag); - b.set_origin_tag(challenge_origin_tag); + // Tags are merged on XOR + EXPECT_EQ(a.get_origin_tag(), first_two_merged_tag); - auto c = (!a) && (!b); + b = !b; // b = 1 (witness 0) + EXPECT_EQ(b.get_value(), 1); - // Tags are merged on logical AND - EXPECT_EQ(c.get_origin_tag(), first_two_merged_tag); + // Tag is preserved on NOT + EXPECT_EQ(b.get_origin_tag(), challenge_origin_tag); - bool result = CircuitChecker::check(builder); - EXPECT_EQ(result, true); -} + a.set_origin_tag(submitted_value_origin_tag); -TYPED_TEST(BoolTest, And) -{ - STDLIB_TYPE_ALIASES - auto builder = Builder(); - - for (size_t i = 0; i < 32; ++i) { - bool_ct a = witness_ct(&builder, (bool)(i % 1)); - bool_ct b = witness_ct(&builder, (bool)(i % 2 == 1)); - // clang-format off - a& b; - // clang-format on - } + bool_ct d = (a == b); // + EXPECT_EQ(d.get_value(), 1); - bool result = CircuitChecker::check(builder); - EXPECT_EQ(result, true); -} + // Tags are merged on == + EXPECT_EQ(d.get_origin_tag(), first_two_merged_tag); -TYPED_TEST(BoolTest, AndConstants) -{ - STDLIB_TYPE_ALIASES - auto builder = Builder(); - - for (size_t i = 0; i < 32; ++i) { - bool_ct a = witness_ct(&builder, (bool)(i % 2)); - bool_ct b = witness_ct(&builder, (bool)(i % 3 == 1)); - // clang-format off - a& b; - // clang-format on - } - for (size_t i = 0; i < 32; ++i) { - if (i % 2 == 0) { - bool_ct a = witness_ct(&builder, (bool)(i % 2)); - bool_ct b(&builder, (bool)(i % 3 == 1)); - // clang-format off - a& b; - // clang-format on - } else { - bool_ct a(&builder, (bool)(i % 2)); - bool_ct b = witness_ct(&builder, (bool)(i % 3 == 1)); - // clang-format off - a& b; - // clang-format on - } - } + d = false; // d = 0 + d.set_origin_tag(challenge_origin_tag); + EXPECT_EQ(d.get_value(), 0); - bool result = CircuitChecker::check(builder); - EXPECT_EQ(result, true); -} + bool_ct e = a | d; // e = 1 = a + EXPECT_EQ(e.get_value(), 1); -TYPED_TEST(BoolTest, or) -{ - STDLIB_TYPE_ALIASES - auto builder = Builder(); + // Tags are merged on OR + EXPECT_EQ(e.get_origin_tag(), first_two_merged_tag); - for (size_t i = 0; i < 32; ++i) { - bool_ct a = witness_ct(&builder, (bool)(i % 2)); - bool_ct b = witness_ct(&builder, (bool)(i % 3 == 1)); - a | b; - } + bool_ct f = e ^ b; // f = 0 + EXPECT_EQ(f.get_value(), 0); - bool result = CircuitChecker::check(builder); - EXPECT_EQ(result, true); -} + f.set_origin_tag(challenge_origin_tag); + d = (!f) & a; // d = 1 + EXPECT_EQ(d.get_value(), 1); -TYPED_TEST(BoolTest, OrConstants) -{ - STDLIB_TYPE_ALIASES - auto builder = Builder(); + // Tags are merged on AND + EXPECT_EQ(d.get_origin_tag(), first_two_merged_tag); + + bool result = CircuitChecker::check(builder); + EXPECT_EQ(result, true); - for (size_t i = 0; i < 32; ++i) { - bool_ct a = witness_ct(&builder, (bool)(i % 2)); - bool_ct b = witness_ct(&builder, (bool)(i % 3 == 1)); - a | b; + auto gates_after = builder.get_estimated_num_finalized_gates(); + EXPECT_EQ(gates_after - gates_before, 6UL); } - for (size_t i = 0; i < 32; ++i) { - if (i % 2 == 0) { - bool_ct a = witness_ct(&builder, (bool)(i % 2)); - bool_ct b(&builder, (bool)(i % 3 == 1)); - a | b; - } else { - bool_ct a(&builder, (bool)(i % 2)); - bool_ct b = witness_ct(&builder, (bool)(i % 3 == 1)); - a | b; + + // Check that (a && (b || c)) ^ (d => f) <=> ((a && b) || (a && c)) ^ (!d || f)) for all inputs. + void test_simple_proof() + { + for (const auto& a_input : all_inputs) { + for (const auto& b_input : all_inputs) { + for (const auto& c_input : all_inputs) { + for (const auto& d_input : all_inputs) { + for (const auto& f_input : all_inputs) { + Builder builder; + + // Construct bool_cts from inputs + bool_ct a = create_bool_ct(a_input, &builder); + bool_ct b = create_bool_ct(b_input, &builder); + bool_ct c = create_bool_ct(c_input, &builder); + bool_ct d = create_bool_ct(d_input, &builder); + bool_ct f = create_bool_ct(f_input, &builder); + + // === Formula 1 === + bool_ct lhs = (a && (b || c)) ^ (d.implies(f)); + bool_ct rhs = ((a && b) || (a && c)) ^ (!d || f); + + // Equivalence check + bool_ct equivalent = lhs.implies_both_ways(rhs); + if (!equivalent.get_value()) { + info("FAIL:"); + info("a: ", a.get_value(), " b: ", b.get_value(), " c: ", c.get_value()); + info("d: ", d.get_value(), " f: ", f.get_value()); + } + + EXPECT_EQ(equivalent.get_value(), true); + EXPECT_TRUE(CircuitChecker::check(builder)); + } + } + } + } } } +}; - bool result = CircuitChecker::check(builder); - EXPECT_EQ(result, true); -} +using CircuitTypes = ::testing::Types; -TYPED_TEST(BoolTest, Eq) +TYPED_TEST_SUITE(BoolTest, CircuitTypes); +TYPED_TEST(BoolTest, ConstructFromConstBool) { - STDLIB_TYPE_ALIASES - auto builder = Builder(); - - bool a_alt[32]; - bool b_alt[32]; - bool c_alt[32]; - bool d_alt[32]; - for (size_t i = 0; i < 32; ++i) { - if (i % 2 == 0) { - a_alt[i] = bool(i % 2); - b_alt[i] = false; - c_alt[i] = a_alt[i] ^ b_alt[i]; - d_alt[i] = a_alt[i] == c_alt[i]; - } else { - a_alt[i] = true; - b_alt[i] = false; - c_alt[i] = false; - d_alt[i] = false; - } - } - bool_ct a[32]; - bool_ct b[32]; - bool_ct c[32]; - bool_ct d[32]; - for (size_t i = 0; i < 32; ++i) { - if (i % 2 == 0) { - a[i] = witness_ct(&builder, (bool)(i % 2)); - b[i] = witness_ct(&builder, (bool)(0)); - c[i] = a[i] ^ b[i]; - d[i] = a[i] == c[i]; - } else { - a[i] = witness_ct(&builder, (bool)(1)); - b[i] = witness_ct(&builder, (bool)(0)); - c[i] = a[i] & b[i]; - d[i] = a[i] == c[i]; - } - } - for (size_t i = 0; i < 32; ++i) { - EXPECT_EQ(a[i].get_value(), a_alt[i]); - EXPECT_EQ(b[i].get_value(), b_alt[i]); - EXPECT_EQ(c[i].get_value(), c_alt[i]); - EXPECT_EQ(d[i].get_value(), d_alt[i]); - } - - bool result = CircuitChecker::check(builder); - EXPECT_EQ(result, true); + TestFixture::test_construct_from_const_bool(); } -TYPED_TEST(BoolTest, Implies) +TYPED_TEST(BoolTest, ConstructFromWitness) { - STDLIB_TYPE_ALIASES - auto builder = Builder(); - - for (size_t j = 0; j < 4; ++j) { - bool lhs_constant = (bool)(j % 2); - bool rhs_constant = (bool)(j > 1 ? true : false); - - for (size_t i = 0; i < 4; ++i) { - bool a_val = (bool)(i % 2); - bool b_val = (bool)(i > 1 ? true : false); - bool_ct a = lhs_constant ? bool_ct(a_val) : (witness_ct(&builder, a_val)); - bool_ct b = rhs_constant ? bool_ct(b_val) : (witness_ct(&builder, b_val)); - if (!(lhs_constant || rhs_constant)) { - a.set_origin_tag(submitted_value_origin_tag); - b.set_origin_tag(challenge_origin_tag); - } - bool_ct c = a.implies(b); - EXPECT_EQ(c.get_value(), !a.get_value() || b.get_value()); - if (!(lhs_constant || rhs_constant)) { - // Tags are merged on implies - EXPECT_EQ(c.get_origin_tag(), first_two_merged_tag); - } - } - } - - bool result = CircuitChecker::check(builder); - EXPECT_EQ(result, true); + TestFixture::test_construct_from_witness(); } -TYPED_TEST(BoolTest, ImpliesBothWays) +TYPED_TEST(BoolTest, Normalization) { - STDLIB_TYPE_ALIASES - auto builder = Builder(); - - for (size_t j = 0; j < 4; ++j) { - bool lhs_constant = (bool)(j % 2); - bool rhs_constant = (bool)(j > 1 ? true : false); - - for (size_t i = 0; i < 4; ++i) { - bool a_val = (bool)(i % 2); - bool b_val = (bool)(i > 1 ? true : false); - bool_ct a = lhs_constant ? bool_ct(a_val) : (witness_ct(&builder, a_val)); - bool_ct b = rhs_constant ? bool_ct(b_val) : (witness_ct(&builder, b_val)); - if (!(lhs_constant || rhs_constant)) { - a.set_origin_tag(submitted_value_origin_tag); - b.set_origin_tag(challenge_origin_tag); - } - bool_ct c = a.implies_both_ways(b); - EXPECT_EQ(c.get_value(), !(a.get_value() ^ b.get_value())); + TestFixture::test_normalize(); +} +TYPED_TEST(BoolTest, XOR) +{ + TestFixture::test_xor(); +} - if (!(lhs_constant || rhs_constant)) { - // Tags are merged on implies both ways - EXPECT_EQ(c.get_origin_tag(), first_two_merged_tag); - } - } - } +TYPED_TEST(BoolTest, AND) +{ + TestFixture::test_AND(); +} - bool result = CircuitChecker::check(builder); - EXPECT_EQ(result, true); +TYPED_TEST(BoolTest, OR) +{ + TestFixture::test_OR(); } -TYPED_TEST(BoolTest, MustImply) +TYPED_TEST(BoolTest, EQ) { - STDLIB_TYPE_ALIASES - auto builder = Builder(); - - for (size_t j = 0; j < 4; ++j) { - bool lhs_constant = (bool)(j % 2); - bool rhs_constant = (bool)(j > 1 ? true : false); - - for (size_t i = 4; i < 14; i += 2) { - // If a number is divisible by 2 and 3, it is divisible by 6 - bool two = (bool)(i % 2); - bool three = (bool)(i % 3); - bool six = (bool)(i % 6); - bool a_val = (two && three); - bool b_val = six; - bool_ct a = lhs_constant ? bool_ct(a_val) : (witness_ct(&builder, a_val)); - bool_ct b = rhs_constant ? bool_ct(b_val) : (witness_ct(&builder, b_val)); - a.must_imply(b); - } - } + TestFixture::test_EQ(); +} - bool result = CircuitChecker::check(builder); - EXPECT_EQ(result, true); +TYPED_TEST(BoolTest, NEQ) +{ + TestFixture::test_NEQ(); } -TYPED_TEST(BoolTest, MustImplyFails) +TYPED_TEST(BoolTest, Implies) { - STDLIB_TYPE_ALIASES - auto builder = Builder(); - - for (size_t j = 0; j < 3; ++j) { // ignore the case when both lhs and rhs are constants - bool lhs_constant = (bool)(j % 2); - bool rhs_constant = (bool)(j > 1 ? true : false); - - // If a number is divisible by 2 and 3, it is divisible by 6 - // => 8 is not divisible by 3, so it must not be divisible by 6 - const size_t i = 8; - bool a_val = (bool)(i % 2 == 0); - bool b_val = (bool)(i % 6 == 0); - bool_ct a = lhs_constant ? bool_ct(a_val) : (witness_ct(&builder, a_val)); - bool_ct b = rhs_constant ? bool_ct(b_val) : (witness_ct(&builder, b_val)); - a.must_imply(b, "div by 2 does not imply div by 8"); - - EXPECT_EQ(builder.failed(), true); - EXPECT_EQ(builder.err(), "div by 2 does not imply div by 8"); - } + TestFixture::test_implies(); } -TYPED_TEST(BoolTest, MustImplyMultiple) +TYPED_TEST(BoolTest, ImpliesBothWays) { - STDLIB_TYPE_ALIASES - auto builder = Builder(); - - /** - * Define g(x) = 2x + 12 - * if x is divisible by both 4 and 6: - * => g(x) > 0 - * => g(x) is even - * => g(x) >= 12 - * => g(x) is a multiple of 6 - */ - auto g = [](size_t x) { return 2 * x + 12; }; - - for (size_t j = 0; j < 3; ++j) { // ignore when both lhs and rhs are constants - bool lhs_constant = (bool)(j % 2); - bool rhs_constant = (bool)(j > 1 ? true : false); - - for (size_t x = 10; x < 18; x += 2) { - std::vector> conditions; - bool four = (bool)(x % 4 == 0); - bool six = (bool)(x % 6 == 0); - - bool_ct a = lhs_constant ? bool_ct(four) : (witness_ct(&builder, four)); - bool_ct b = rhs_constant ? bool_ct(six) : (witness_ct(&builder, six)); - - auto g_x = g(x); - conditions.push_back(std::make_pair(g_x > 0, "g(x) > 0")); - conditions.push_back(std::make_pair(g_x % 2 == 0, "g(x) is even")); - conditions.push_back(std::make_pair(g_x >= 12, "g(x) >= 12")); - conditions.push_back(std::make_pair(g_x % 6 == 0, "g(x) is a multiple of 6")); - - (a && b).must_imply(conditions); - - if (builder.failed()) { - EXPECT_EQ(builder.err(), "multi implication fail: g(x) is a multiple of 6"); - } else { - bool result = CircuitChecker::check(builder); - EXPECT_EQ(result, true); - } - } - } + TestFixture::test_implies_both_ways(); } -TYPED_TEST(BoolTest, MustImplyMultipleFails) +TYPED_TEST(BoolTest, MustImply) { - STDLIB_TYPE_ALIASES - auto builder = Builder(); - - /** - * Given x = 15: - * (x > 10) - * => (x > 8) - * => (x > 5) - * ≠> (x > 18) - */ - for (size_t j = 0; j < 2; ++j) { // ignore when both lhs and rhs are constants - bool is_constant = (bool)(j % 2); - - size_t x = 15; - bool main = (bool)(x > 10); - bool_ct main_ct = is_constant ? bool_ct(main) : (witness_ct(&builder, main)); - - std::vector> conditions; - conditions.push_back(std::make_pair(witness_ct(&builder, x > 8), "x > 8")); - conditions.push_back(std::make_pair(witness_ct(&builder, x > 5), "x > 5")); - conditions.push_back(std::make_pair(witness_ct(&builder, x > 18), "x > 18")); - - main_ct.must_imply(conditions); - - EXPECT_EQ(builder.failed(), true); - EXPECT_EQ(builder.err(), "multi implication fail: x > 18"); - } + TestFixture::test_must_imply(); } TYPED_TEST(BoolTest, ConditionalAssign) { - STDLIB_TYPE_ALIASES - auto builder = Builder(); - - for (size_t j = 0; j < 4; ++j) { - bool lhs_constant = (bool)(j % 2); - bool rhs_constant = (bool)(j > 1 ? true : false); - - const uint256_t x = (uint256_t(1) << 128) - 1; - const uint256_t val = engine.get_random_uint256(); - - bool condition = (val % 2 == 0); - bool right = x < val; - bool left = x > val; - bool_ct l_ct = lhs_constant ? bool_ct(left) : (witness_ct(&builder, left)); - bool_ct r_ct = rhs_constant ? bool_ct(right) : (witness_ct(&builder, right)); - bool_ct cond = (witness_ct(&builder, condition)); - - if (!(lhs_constant | rhs_constant)) { - cond.set_origin_tag(submitted_value_origin_tag); - l_ct.set_origin_tag(challenge_origin_tag); - r_ct.set_origin_tag(next_challenge_tag); - } - auto result = bool_ct::conditional_assign(cond, l_ct, r_ct); - - if (!(lhs_constant | rhs_constant)) { - // Tags are merged on conditional assign - EXPECT_EQ(result.get_origin_tag(), first_second_third_merged_tag); - } + TestFixture::test_conditional_assign(); +} - EXPECT_EQ(result.get_value(), condition ? left : right); - } - info("num gates = ", builder.get_estimated_num_finalized_gates()); - bool result = CircuitChecker::check(builder); - EXPECT_EQ(result, true); +TYPED_TEST(BoolTest, TestBasicOperationsTags) +{ + TestFixture::test_basic_operations_tags(); } TYPED_TEST(BoolTest, TestSimpleProof) { - STDLIB_TYPE_ALIASES - auto builder = Builder(); - - bool_ct a(&builder); - bool_ct b(&builder); - a = witness_ct(&builder, bb::fr::one()); - b = witness_ct(&builder, bb::fr::zero()); - // bool_ct c(&builder); - a = a ^ b; // a = 1 - b = !b; // b = 1 (witness 0) - bool_ct c = (a == b); // c = 1 - bool_ct d(&builder); // d = ? - d = false; // d = 0 - bool_ct e = a | d; // e = 1 = a - bool_ct f = e ^ b; // f = 0 - d = (!f) & a; // d = 1 - for (size_t i = 0; i < 64; ++i) { - a = witness_ct(&builder, (bool)(i % 2)); - b = witness_ct(&builder, (bool)(i % 3 == 1)); - c = a ^ b; - a = b ^ c; - c = a; - a = b; - f = b; - } - - bool result = CircuitChecker::check(builder); - EXPECT_EQ(result, true); + TestFixture::test_simple_proof(); } - -TYPED_TEST(BoolTest, Normalize) +TYPED_TEST(BoolTest, AssertEqual) { - STDLIB_TYPE_ALIASES - auto builder = Builder(); - - auto generate_constraints = [&builder](bool value, bool is_constant, bool is_inverted) { - bool_ct a = is_constant ? bool_ct(&builder, value) : witness_ct(&builder, value); - bool_ct b = is_inverted ? !a : a; - if (!is_constant) { - b.set_origin_tag(submitted_value_origin_tag); - } - bool_ct c = b.normalize(); - EXPECT_EQ(c.get_value(), value ^ is_inverted); - if (!is_constant) { - EXPECT_EQ(c.get_origin_tag(), submitted_value_origin_tag); - } - }; - - generate_constraints(false, false, false); - generate_constraints(false, false, true); - generate_constraints(false, true, false); - generate_constraints(false, true, true); - generate_constraints(true, false, false); - generate_constraints(true, false, true); - generate_constraints(true, true, false); - generate_constraints(true, true, true); - - bool result = CircuitChecker::check(builder); - EXPECT_EQ(result, true); + TestFixture::test_assert_equal(); }