bool.cpp

Go to the documentation of this file.

// === AUDIT STATUS ===
// internal:    { status: Complete, auditors: [Sergei], commit: 72f52e7bad0fc1e36da575fbc2e6bfa1b1104aec}
// external_1:  { status: Complete, auditors: [@ed25519, @JakubHeba (Spearbit)], commit:
// b463d7c1c52fec2f4e39acfd21219464b00a39d8}
// external_2:  { status: not started, auditors: [], commit: }
// =====================
 
#include "bool.hpp"
#include "../circuit_builders/circuit_builders.hpp"
#include "barretenberg/common/assert.hpp"
#include "barretenberg/stdlib/primitives/field/field.hpp"
#include "barretenberg/transcript/origin_tag.hpp"
 
using namespace bb;
 
namespace bb::stdlib {
 
template <typename Builder>
bool_t<Builder>::bool_t(const bool value)
    : witness_bool(value)
{
    tag = OriginTag::constant();
}
 
template <typename Builder>
bool_t<Builder>::bool_t(Builder* parent_context)
    : context(parent_context)
{
    tag = OriginTag::constant();
}
 
template <typename Builder>
bool_t<Builder>::bool_t(const witness_t<Builder>& value, const bool& use_range_constraint)
    : context(value.context)
{
    BB_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;
 
    if (use_range_constraint) {
        // Create a range constraint gate
        context->create_small_range_constraint(witness_index, 1, "bool_t: witness value is not 0 or 1");
    } else {
        // Create an arithmetic gate to enforce 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();
}
template <typename Builder>
bool_t<Builder>::bool_t(Builder* parent_context, const bool value)
    : context(parent_context)
    , witness_bool(value)
{
    tag = OriginTag::constant();
}
 
template <typename Builder>
bool_t<Builder>::bool_t(const bool_t<Builder>& other)
    : context(other.context)
    , witness_bool(other.witness_bool)
    , witness_inverted(other.witness_inverted)
    , witness_index(other.witness_index)
    , tag(other.tag)
{}
 
template <typename Builder>
bool_t<Builder>::bool_t(bool_t<Builder>&& other)
    : context(other.context)
    , witness_bool(other.witness_bool)
    , witness_inverted(other.witness_inverted)
    , witness_index(other.witness_index)
    , tag(other.tag)
{}
 
template <typename Builder>
bool_t<Builder> bool_t<Builder>::from_witness_index_unsafe(Builder* ctx, const uint32_t witness_index)
{
    BB_ASSERT(witness_index != IS_CONSTANT);
    bool_t<Builder> result(ctx);
    result.witness_index = witness_index;
    const bb::fr value = ctx->get_variable(witness_index);
    // It does not create a constraint.
    BB_ASSERT_EQ(value * value - value, 0, "bool_t: creating a witness bool from a non-boolean value");
    result.witness_bool = (value == 1);
    result.witness_inverted = false;
    // Since this is now a witness (not a constant), set the free witness tag
    // The caller should set the appropriate tag if this element has a known provenance
    result.set_free_witness_tag();
    return result;
}
 
template <typename Builder> bool_t<Builder>& bool_t<Builder>::operator=(const bool other)
{
    context = nullptr;
    witness_index = IS_CONSTANT;
    witness_bool = other;
    witness_inverted = false;
    tag = OriginTag::constant();
    return *this;
}
 
template <typename Builder> bool_t<Builder>& bool_t<Builder>::operator=(const bool_t& other) = default;
 
template <typename Builder> bool_t<Builder>& bool_t<Builder>::operator=(bool_t&& other)
{
    context = other.context;
    witness_index = other.witness_index;
    witness_bool = other.witness_bool;
    witness_inverted = other.witness_inverted;
    tag = other.tag;
    return *this;
}
template <typename Builder> bool_t<Builder>& bool_t<Builder>::operator=(const witness_t<Builder>& other)
{
    BB_ASSERT((other.witness == bb::fr::one()) || (other.witness == bb::fr::zero()),
              "bool_t: witness value is not 0 or 1");
    context = other.context;
    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;
}
 
template <typename Builder> bool_t<Builder> bool_t<Builder>::operator&(const bool_t& other) const
{
    Builder* ctx = validate_context<Builder>(context, other.context);
    bool_t<Builder> result(ctx);
    bool left = witness_inverted ^ witness_bool;
    bool right = other.witness_inverted ^ other.witness_bool;
    result.witness_bool = left && right;
 
    BB_ASSERT(ctx || (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 = ctx->add_variable(value);
 
        int i_a(static_cast<int>(witness_inverted));
        int i_b(static_cast<int>(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 };
 
        ctx->create_arithmetic_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()) {
        BB_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()) {
        BB_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;
}
 
template <typename Builder> bool_t<Builder> bool_t<Builder>::operator|(const bool_t& other) const
{
    Builder* ctx = validate_context<Builder>(context, other.context);
 
    bool_t<Builder> result(ctx);
 
    BB_ASSERT(ctx || (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();
    if (!is_constant() && !other.is_constant()) {
        result.witness_index = ctx->add_variable(value);
        // 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<int>(other.witness_inverted);
        const int lhs_inverted = static_cast<int>(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
        ctx->create_arithmetic_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()) {
        BB_ASSERT_EQ(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`.
        BB_ASSERT_EQ(witness_inverted, false);
        result = witness_bool ? *this : other;
    }
    result.tag = OriginTag(tag, other.tag);
    return result;
}
 
template <typename Builder> bool_t<Builder> bool_t<Builder>::operator^(const bool_t& other) const
{
    Builder* ctx = validate_context<Builder>(context, other.context);
    bool_t<Builder> result(ctx);
 
    BB_ASSERT(ctx || (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();
 
    if (!is_constant() && !other.is_constant()) {
        result.witness_index = ctx->add_variable(value);
        // 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<int>(other.witness_inverted);
        const int lhs_inverted = static_cast<int>(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
        ctx->create_arithmetic_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
        BB_ASSERT_EQ(other.witness_inverted, false);
        result = other.witness_bool ? !*this : *this;
 
    } else if (is_constant() && !other.is_constant()) {
        BB_ASSERT_EQ(witness_inverted, false);
        result = witness_bool ? !other : other;
    }
    result.tag = OriginTag(tag, other.tag);
    return result;
}
template <typename Builder> bool_t<Builder> bool_t<Builder>::operator!() const
{
    bool_t<Builder> result(*this);
    if (result.is_constant()) {
        BB_ASSERT(!witness_inverted);
        // Negate the value of a constant bool_t element.
        result.witness_bool = !result.witness_bool;
    } else {
        // Negate the `inverted` flag of a witnees bool_t element.
        result.witness_inverted = !result.witness_inverted;
    }
    return result;
}
 
template <typename Builder> bool_t<Builder> bool_t<Builder>::operator==(const bool_t& other) const
{
    Builder* ctx = validate_context<Builder>(context, other.context);
    bool_t<Builder> result(ctx);
    BB_ASSERT(ctx || (is_constant() && other.is_constant()));
 
    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);
 
        // 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<int>(other.witness_inverted);
        const int lhs_inverted = static_cast<int>(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 };
 
        ctx->create_arithmetic_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())) {
        // 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.
        BB_ASSERT_EQ(other.witness_inverted, false);
        result = other.witness_bool ? *this : !(*this);
    } else if (is_constant() && !other.is_constant()) {
        // Completely analogous to the previous case.
        BB_ASSERT_EQ(witness_inverted, false);
        result = witness_bool ? other : !other;
    }
 
    result.tag = OriginTag(tag, other.tag);
    return result;
}
template <typename Builder> bool_t<Builder> bool_t<Builder>::operator!=(const bool_t<Builder>& other) const
{
    return operator^(other);
}
 
template <typename Builder> bool_t<Builder> bool_t<Builder>::operator&&(const bool_t<Builder>& other) const
{
    return operator&(other);
}
 
template <typename Builder> bool_t<Builder> bool_t<Builder>::operator||(const bool_t<Builder>& other) const
{
    return operator|(other);
}
 
template <typename Builder> void bool_t<Builder>::assert_equal(const bool_t& rhs, std::string const& msg) const
{
    const bool_t lhs = *this;
    Builder* ctx = validate_context<Builder>(rhs.get_context(), lhs.get_context());
 
    if (lhs.is_constant() && rhs.is_constant()) {
        BB_ASSERT_EQ(lhs.get_value(), rhs.get_value(), "bool_t::assert_equal: constants are not equal");
    } else if (lhs.is_constant()) {
        BB_ASSERT(!lhs.witness_inverted);
        // if rhs is inverted, flip the value of the lhs constant
        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()) {
        BB_ASSERT(!rhs.witness_inverted);
        // if lhs is inverted, flip the value of the rhs constant
        const bool rhs_value = lhs.witness_inverted ? !rhs.witness_bool : rhs.witness_bool;
        ctx->assert_equal_constant(lhs.witness_index, rhs_value, msg);
    } else {
        // Both are witnesses - save original tags and clear them to allow different transcript/free witness sources
        // (e.g., proving 2 separate properties about same object through 2 different transcripts)
        const auto lhs_original_tag = lhs.get_origin_tag();
        const auto rhs_original_tag = rhs.get_origin_tag();
        auto empty_tag = OriginTag::constant(); // Disable origin checking during intermediate operations
        lhs.set_origin_tag(empty_tag);
        rhs.set_origin_tag(empty_tag);
 
        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();
            right = right.normalize();
        }
        ctx->assert_equal(left.witness_index, right.witness_index, msg);
 
        // Restore tags
        lhs.set_origin_tag(lhs_original_tag);
        rhs.set_origin_tag(rhs_original_tag);
    }
}
 
template <typename Builder>
bool_t<Builder> bool_t<Builder>::conditional_assign(const bool_t<Builder>& predicate,
                                                    const bool_t& lhs,
                                                    const bool_t& rhs)
{
    if (predicate.is_constant()) {
        auto result = bool_t(predicate.get_value() ? lhs : rhs);
        result.set_origin_tag(OriginTag(predicate.get_origin_tag(), lhs.get_origin_tag(), rhs.get_origin_tag()));
        return result.normalize();
    }
 
    bool same = lhs.witness_index == rhs.witness_index;
    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.normalize();
    }
    // Boolean operations can preserve inverted flags when constants are involved
    // (e.g., inverted_witness && constant_true returns inverted_witness)
    return ((predicate && lhs) || (!predicate && rhs)).normalize();
}
 
template <typename Builder> bool_t<Builder> bool_t<Builder>::implies(const bool_t<Builder>& 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).
}
 
template <typename Builder> void bool_t<Builder>::must_imply(const bool_t& other, std::string const& msg) const
{
    implies(other).assert_equal(true, msg);
}
 
template <typename Builder> bool_t<Builder> bool_t<Builder>::implies_both_ways(const bool_t<Builder>& other) const
{
    return !((*this) ^ other); // P <=> Q is equiv. to !(P ^ Q) (not(P xor Q)).
}
 
template <typename Builder> bool_t<Builder> bool_t<Builder>::normalize() const
{
    if (is_constant()) {
        BB_ASSERT(!witness_inverted);
        return *this;
    }
 
    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;
 
    uint32_t new_witness = context->add_variable(bb::fr{ static_cast<int>(value) });
 
    const int inverted = static_cast<int>(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_arithmetic_gate({ witness_index, context->zero_idx(), new_witness, q_m, q_l, q_r, q_o, q_c });
 
    witness_index = new_witness;
    witness_bool = value;
    witness_inverted = false;
    return *this;
}
 
template class bool_t<bb::UltraCircuitBuilder>;
template class bool_t<bb::MegaCircuitBuilder>;
 
} // namespace bb::stdlib