Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
110 changes: 0 additions & 110 deletions barretenberg/cpp/src/barretenberg/stdlib/primitives/field/field.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -1338,116 +1338,6 @@ std::pair<field_t<Builder>, field_t<Builder>> field_t<Builder>::split_at(const s
return std::make_pair(lo_wit, hi_wit);
}

/**
* @brief Build constraints establishing the decomposition of `*this` into bits.
*
* @details A bit vector `result` is extracted and used to construct a sum `sum` using the normal binary expansion.
* Along the way, we extract a value `shifted_high_limb` which is equal to `sum_hi` in the natural decomposition
* `sum = sum_lo + 2**128*sum_hi`.
* We impose a copy constraint between `sum` and `this` but that only imposes equality in `Fr`; it could be that
* `result` has overflown the modulus `r`. To impose a unique value of `result`, we constrain `sum` to satisfy
* `r - 1 >= sum >= 0`. In order to do this inside of `Fr`, we must reduce the check to smaller checks so that
* we can check non-negativity of integers using range constraints in Fr.
*
* At circuit compilation time we build the decomposition `r - 1 = p_lo + 2**128*p_hi`. We handle the high and low limbs
* of `r - 1 - sum` separately as explained below.
*
* Define
*
* y_lo := (2^128 + p_lo) - sum + shifted_high_limb =
* = (2^128 + p_lo) - sum_lo
* Use the method `slice` to split `y_lo` into the chunks `y_lo_lo`, `y_lo_hi`, and `zeros` of sizes 128, 1, and 127,
* respectively, set
* y_lo := y_lo_lo + y_lo_hi * 2^128 + zeros * 2^129
*
* It follows that
* p_lo - sum_lo = y_lo_lo + (y_lo_hi - 1) * 2^128 + zeros * 2^129
*
* Where 0 <= y_lo_lo < 2^128 enforced in field_t::slice
* 0 <= y_lo_hi < 2 enforced in field_t::slice
* 0 <= zeros < 2^{256-129} enforced in field_t::slice
*
* By asserting that `zeros` = 0 we ensure that p_lo - sum_lo has at most 129 bits.
*
* If y_lo_hi == 1:
* p_lo - sum_lo = y_lo_lo < 2^128
* if y_lo_hi == 0:
* 1 - 2^128 < p_lo - sum_lo = y_lo_lo - 2^128 < 0
* If this is indeed the case, `zeros` can't be equal to 0, since p_lo - sum_lo is a small negative value in Fr.
* To handle the high limb of the difference (r - 1 - sum), we compute
*
* Define
*
* y_borrow := -(1 - y_lo_hi) "a carry is necessary".
*
* Note that y_borrow is implicitly constrained to be 0 <= y_borrow < 2.
* y_hi := (p_hi - y_borrow) - sum_hi
* We constrain
* 0 <= y_hi < 2^128
*/
template <typename Builder>
std::vector<bool_t<Builder>> field_t<Builder>::decompose_into_bits(
size_t num_bits, const std::function<witness_t<Builder>(Builder*, uint64_t, uint256_t)> get_bit) const
{
static constexpr size_t max_num_bits = 256;
BB_ASSERT_LTE(num_bits, max_num_bits);
const size_t midpoint = max_num_bits / 2;
std::vector<bool_t<Builder>> result(num_bits);

std::vector<field_t> accumulator_lo;
std::vector<field_t> accumulator_hi;

const uint256_t val_u256 = get_value();
for (size_t i = 0; i < num_bits; ++i) {
const size_t bit_index = num_bits - 1 - i;
// Create a witness `bool_t` bit
bool_t bit = get_bit(context, bit_index, val_u256);
bit.set_origin_tag(tag);
result[bit_index] = bit;
const field_t scaling_factor(uint256_t(1) << bit_index);

field_t summand = scaling_factor * bit;

if (bit_index >= midpoint) {
accumulator_hi.push_back(summand);
} else {
accumulator_lo.push_back(summand);
}
}

field_t sum_hi_shift = field_t::accumulate(accumulator_hi); // =: sum_hi, needed to compute sum_lo
field_t sum_lo = field_t::accumulate(accumulator_lo);
assert_equal(sum_lo + sum_hi_shift,
"field_t: bit decomposition_fails: copy constraint"); // `this` and `sum` are both normalized here.
// The value can be larger than the modulus, hence we must enforce unique representation
static constexpr uint256_t modulus_minus_one = fr::modulus - 1;
static constexpr size_t num_bits_modulus_minus_one = modulus_minus_one.get_msb();
if (num_bits >= num_bits_modulus_minus_one) {
// Split r - 1 into limbs
// r - 1 = p_lo + 2**128 * p_hi
static constexpr fr p_lo = modulus_minus_one.slice(0, midpoint);
static constexpr fr p_hi = modulus_minus_one.slice(midpoint, max_num_bits);

// `shift` is used to shift high limbs. It also represents a borrowed bit.
static constexpr fr shift = fr(uint256_t(1) << midpoint);

const field_t y_lo = -sum_lo + (p_lo + shift);

// Ensure that y_lo is "non-negative"
auto [y_lo_lo, y_lo_hi, zeros] = y_lo.slice(midpoint, midpoint);
zeros.assert_is_zero("field_t: bit decomposition_fails: high limb non-zero");

// Ensure that y_hi is "non-negative"
const field_t y_borrow = -y_lo_hi + 1;
// If a carry was necessary, subtract that carry from p_hi
// y_hi = (p_hi - y_borrow) - sum_hi
const field_t y_hi = (-(sum_hi_shift / shift)).add_two(p_hi, -y_borrow);
// As before, except that now the range constraint is explicit, this shows that y_hi is non-negative.
y_hi.create_range_constraint(midpoint, "field_t: bit decomposition fails: y_hi is too large.");
}
return result;
}

template class field_t<bb::UltraCircuitBuilder>;
template class field_t<bb::MegaCircuitBuilder>;

Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -1052,46 +1052,6 @@ template <typename Builder> class FieldBase {
std::cout << "Reproduce via accumulate()" << std::endl;
#endif
return ExecutionHandler(this->base, field_t::accumulate({ this->f() }));
case 8: {
#ifdef FUZZING_SHOW_INFORMATION
std::cout << "Reproduce via decompose_into_bits()" << std::endl;
#endif
const size_t min_num_bits = static_cast<uint256_t>(this->base).get_msb() + 1;
if (min_num_bits > 256)
abort(); /* Should never happen */

const size_t num_bits = min_num_bits + (VarianceRNG.next() % (256 - min_num_bits + 1));
if (num_bits > 256)
abort(); /* Should never happen */

/* XXX this gives: Range error at gate 559 */
// const auto bits = this->f().decompose_into_bits(num_bits);
const auto bits = this->f().decompose_into_bits();

std::vector<bb::fr> frs(bits.size());
for (size_t i = 0; i < bits.size(); i++) {
frs[i] = bits[i].get_value() ? bb::fr(uint256_t(1) << i) : 0;
}

switch (VarianceRNG.next() % 2) {
case 0: {
const bb::fr field_from_bits = std::accumulate(frs.begin(), frs.end(), bb::fr(0));
return ExecutionHandler(this->base, field_t(builder, field_from_bits));
}
case 1: {
std::vector<field_t> fields;
for (const auto& fr : frs) {
fields.push_back(field_t(builder, fr));
}
/* This is a good opportunity to test
* field_t::accumulate with many elements
*/
return ExecutionHandler(this->base, field_t::accumulate(fields));
}
default:
abort();
}
}
default:
abort();
}
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -408,13 +408,6 @@ template <typename Builder> class field_t {
*/
uint32_t get_normalized_witness_index() const { return normalize().witness_index; }

std::vector<bool_t<Builder>> decompose_into_bits(
const size_t num_bits = 256,
std::function<witness_t<Builder>(Builder* ctx, uint64_t, uint256_t)> get_bit =
[](Builder* ctx, uint64_t j, const uint256_t& val) {
return witness_t<Builder>(ctx, val.get_bit(j));
}) const;

/**
* @brief Return (a < b) as bool circuit type.
* This method *assumes* that both a and b are < 2^{num_bits} - 1
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -949,74 +949,6 @@ template <typename Builder> class stdlib_field : public testing::Test {
EXPECT_EQ(result, true);
}

/**
* @brief Test success and failure cases for decompose_into_bits.
*
* @details The target function constructs `sum` from a supplied collection of bits and compares it with a value
* `val_256`. We supply bit vectors to test some failure cases.
*/

static void test_decompose_into_bits()
{
using witness_supplier_type = std::function<witness_ct(Builder * ctx, uint64_t, uint256_t)>;

// check that constraints are satisfied for a variety of inputs
auto run_success_test = [&](size_t num_bits) {
Builder builder = Builder();

uint256_t random_val(engine.get_random_uint256());
// For big values (num_bits>=254), ensure that they can't overflow by shifting by 4 bits.
uint256_t scalar_raw = (num_bits < 254) ? random_val >> (256 - num_bits) : random_val >> 4;
field_ct a = witness_ct(&builder, scalar_raw);
std::vector<bool_ct> c = a.decompose_into_bits(num_bits);
uint256_t bit_sum = 0;
for (size_t i = 0; i < c.size(); i++) {
uint256_t scaling_factor_value(uint256_t(1) << i);
bit_sum += fr(c[i].get_value()) * scaling_factor_value;
}
EXPECT_EQ(bit_sum, scalar_raw);

ASSERT_TRUE(CircuitChecker::check(builder));
};

// Now try to supply unintended witness values and test for failure.
// Fr::modulus is equivalent to zero in Fr, but this should be forbidden by a range constraint.
witness_supplier_type supply_modulus_bits = [](Builder* ctx, uint64_t j, uint256_t val_256) {
ignore_unused(val_256);
// use this to get `sum` to be fr::modulus.
return witness_ct(ctx, fr::modulus.get_bit(j));
};

// design a bit vector that will pass all range constraints, but it fails the copy constraint.
witness_supplier_type supply_half_modulus_bits = [](Builder* ctx, uint64_t j, uint256_t val_256) {
// use this to fit y_hi into 128 bits
if (j > 127) {
return witness_ct(ctx, val_256.get_bit(j));
};

return witness_ct(ctx, (fr::modulus).get_bit(j));
};

auto run_failure_test = [&](witness_supplier_type witness_supplier, std::string err_msg) {
Builder builder = Builder();

fr a_expected = 0;
field_ct a = witness_ct(&builder, a_expected);
std::vector<bool_ct> c = a.decompose_into_bits(256, witness_supplier);

bool verified = CircuitChecker::check(builder);
ASSERT_FALSE(verified);
EXPECT_TRUE(err_msg == builder.err());
};

for (size_t idx = 1; idx <= 256; idx++) {
run_success_test(idx);
}

run_failure_test(supply_modulus_bits, "field_t: bit decomposition fails: y_hi is too large.");
run_failure_test(supply_half_modulus_bits, "field_t: bit decomposition_fails: copy constraint");
}

static void test_assert_is_in_set()
{
Builder builder = Builder();
Expand Down Expand Up @@ -1422,13 +1354,6 @@ template <typename Builder> class stdlib_field : public testing::Test {
EXPECT_EQ(split_data.first.get_origin_tag(), submitted_value_origin_tag);
EXPECT_EQ(split_data.second.get_origin_tag(), submitted_value_origin_tag);

// Decomposition preserves tags

auto decomposed_bits = a.decompose_into_bits();
for (const auto& bit : decomposed_bits) {
EXPECT_EQ(bit.get_origin_tag(), submitted_value_origin_tag);
}

// Conversions

auto o = field_ct(witness_ct(&builder, 1));
Expand Down Expand Up @@ -1523,10 +1448,6 @@ TYPED_TEST(stdlib_field, test_create_range_constraint)
{
TestFixture::create_range_constraint();
}
TYPED_TEST(stdlib_field, test_decompose_into_bits)
{
TestFixture::test_decompose_into_bits();
}
TYPED_TEST(stdlib_field, test_div)
{
TestFixture::test_div();
Expand Down
Loading