barretenberg
Loading...
Searching...
No Matches
bigfield_impl.hpp
1#pragma once
2
3#include "barretenberg/numeric/uint256/uint256.hpp"
4#include "barretenberg/numeric/uintx/uintx.hpp"
5#include <tuple>
6
7#include "../circuit_builders/circuit_builders.hpp"
8
9#include "../bit_array/bit_array.hpp"
10#include "../field/field.hpp"
11
12using namespace barretenberg;
13
14namespace proof_system::plonk {
15namespace stdlib {
16
17template <typename Builder, typename T>
18bigfield<Builder, T>::bigfield(Builder* parent_context)
19 : context(parent_context)
20 , binary_basis_limbs{ Limb(barretenberg::fr(0)),
21 Limb(barretenberg::fr(0)),
22 Limb(barretenberg::fr(0)),
23 Limb(barretenberg::fr(0)) }
24 , prime_basis_limb(context, 0)
25{}
26
27template <typename Builder, typename T>
28bigfield<Builder, T>::bigfield(Builder* parent_context, const uint256_t& value)
29 : context(parent_context)
30 , binary_basis_limbs{ Limb(barretenberg::fr(value.slice(0, NUM_LIMB_BITS))),
31 Limb(barretenberg::fr(value.slice(NUM_LIMB_BITS, NUM_LIMB_BITS * 2))),
32 Limb(barretenberg::fr(value.slice(NUM_LIMB_BITS * 2, NUM_LIMB_BITS * 3))),
33 Limb(barretenberg::fr(value.slice(NUM_LIMB_BITS * 3, NUM_LIMB_BITS * 4))) }
34 , prime_basis_limb(context, value)
35{
36 ASSERT(value < modulus);
37}
38
39template <typename Builder, typename T>
40bigfield<Builder, T>::bigfield(const field_t<Builder>& low_bits_in,
41 const field_t<Builder>& high_bits_in,
42 const bool can_overflow,
43 const size_t maximum_bitlength)
44{
45 ASSERT((can_overflow == true && maximum_bitlength == 0) ||
46 (can_overflow == false && (maximum_bitlength == 0 || maximum_bitlength > (3 * NUM_LIMB_BITS))));
47
48 // Check that the values of two parts are within specified bounds
49 ASSERT(uint256_t(low_bits_in.get_value()) < (uint256_t(1) << (NUM_LIMB_BITS * 2)));
50 ASSERT(uint256_t(high_bits_in.get_value()) < (uint256_t(1) << (NUM_LIMB_BITS * 2)));
51
52 context = low_bits_in.context == nullptr ? high_bits_in.context : low_bits_in.context;
53 field_t<Builder> limb_0(context);
54 field_t<Builder> limb_1(context);
55 field_t<Builder> limb_2(context);
56 field_t<Builder> limb_3(context);
57 if (low_bits_in.witness_index != IS_CONSTANT) {
58 std::vector<uint32_t> low_accumulator;
59 if constexpr (HasPlookup<Builder>) {
60 // MERGE NOTE: this was the if constexpr block introduced in ecebe7643
61 const auto limb_witnesses =
62 context->decompose_non_native_field_double_width_limb(low_bits_in.normalize().witness_index);
63 limb_0.witness_index = limb_witnesses[0];
64 limb_1.witness_index = limb_witnesses[1];
65 field_t<Builder>::evaluate_linear_identity(low_bits_in, -limb_0, -limb_1 * shift_1, field_t<Builder>(0));
66
67 // // Enforce that low_bits_in indeed only contains 2*NUM_LIMB_BITS bits
68 // low_accumulator = context->decompose_into_default_range(low_bits_in.witness_index,
69 // static_cast<size_t>(NUM_LIMB_BITS * 2));
70 // // If this doesn't hold we're using a default plookup range size that doesn't work well with the limb
71 // size
72 // // here
73 // ASSERT(low_accumulator.size() % 2 == 0);
74 // size_t mid_index = low_accumulator.size() / 2 - 1;
75 // limb_0.witness_index = low_accumulator[mid_index]; // Q:safer to just slice this from low_bits_in?
76 // limb_1 = (low_bits_in - limb_0) * shift_right_1;
77 } else {
78 size_t mid_index;
79 low_accumulator = context->decompose_into_base4_accumulators(
80 low_bits_in.witness_index, static_cast<size_t>(NUM_LIMB_BITS * 2), "bigfield: low_bits_in too large.");
81 mid_index = static_cast<size_t>((NUM_LIMB_BITS / 2) - 1);
82 // Range constraint returns an array of partial sums, midpoint will happen to hold the big limb value
83 limb_1.witness_index = low_accumulator[mid_index];
84 // We can get the first half bits of low_bits_in from the variables we already created
85 limb_0 = (low_bits_in - (limb_1 * shift_1));
86 }
87 } else {
88 uint256_t slice_0 = uint256_t(low_bits_in.additive_constant).slice(0, NUM_LIMB_BITS);
89 uint256_t slice_1 = uint256_t(low_bits_in.additive_constant).slice(NUM_LIMB_BITS, 2 * NUM_LIMB_BITS);
90 limb_0 = field_t(context, barretenberg::fr(slice_0));
91 limb_1 = field_t(context, barretenberg::fr(slice_1));
92 }
93
94 // If we wish to continue working with this element with lazy reductions - i.e. not moding out again after each
95 // addition we apply a more limited range - 2^s for smallest s such that p<2^s (this is the case can_overflow ==
96 // false)
97 uint64_t num_last_limb_bits = (can_overflow) ? NUM_LIMB_BITS : NUM_LAST_LIMB_BITS;
98
99 // if maximum_bitlength is set, this supercedes can_overflow
100 if (maximum_bitlength > 0) {
101 ASSERT(maximum_bitlength > 3 * NUM_LIMB_BITS);
102 num_last_limb_bits = maximum_bitlength - (3 * NUM_LIMB_BITS);
103 }
104 // We create the high limb values similar to the low limb ones above
105 const uint64_t num_high_limb_bits = NUM_LIMB_BITS + num_last_limb_bits;
106 if (high_bits_in.witness_index != IS_CONSTANT) {
107
108 std::vector<uint32_t> high_accumulator;
109 if constexpr (HasPlookup<Builder>) {
110 const auto limb_witnesses = context->decompose_non_native_field_double_width_limb(
111 high_bits_in.normalize().witness_index, (size_t)num_high_limb_bits);
112 limb_2.witness_index = limb_witnesses[0];
113 limb_3.witness_index = limb_witnesses[1];
114 field_t<Builder>::evaluate_linear_identity(high_bits_in, -limb_2, -limb_3 * shift_1, field_t<Builder>(0));
115
116 } else {
117 high_accumulator = context->decompose_into_base4_accumulators(high_bits_in.witness_index,
118 static_cast<size_t>(num_high_limb_bits),
119 "bigfield: high_bits_in too large.");
120 limb_3.witness_index = high_accumulator[static_cast<size_t>((num_last_limb_bits / 2) - 1)];
121 limb_2 = (high_bits_in - (limb_3 * shift_1));
122 }
123 } else {
124 uint256_t slice_2 = uint256_t(high_bits_in.additive_constant).slice(0, NUM_LIMB_BITS);
125 uint256_t slice_3 = uint256_t(high_bits_in.additive_constant).slice(NUM_LIMB_BITS, num_high_limb_bits);
126 limb_2 = field_t(context, barretenberg::fr(slice_2));
127 limb_3 = field_t(context, barretenberg::fr(slice_3));
128 }
129 binary_basis_limbs[0] = Limb(limb_0, DEFAULT_MAXIMUM_LIMB);
130 binary_basis_limbs[1] = Limb(limb_1, DEFAULT_MAXIMUM_LIMB);
131 binary_basis_limbs[2] = Limb(limb_2, DEFAULT_MAXIMUM_LIMB);
132 if (maximum_bitlength > 0) {
133 uint256_t max_limb_value = (uint256_t(1) << (maximum_bitlength - (3 * NUM_LIMB_BITS))) - 1;
134 binary_basis_limbs[3] = Limb(limb_3, max_limb_value);
135 } else {
136 binary_basis_limbs[3] =
137 Limb(limb_3, can_overflow ? DEFAULT_MAXIMUM_LIMB : DEFAULT_MAXIMUM_MOST_SIGNIFICANT_LIMB);
138 }
139 prime_basis_limb = low_bits_in + (high_bits_in * shift_2);
140}
141
142template <typename Builder, typename T>
143bigfield<Builder, T>::bigfield(const bigfield& other)
144 : context(other.context)
145 , binary_basis_limbs{ other.binary_basis_limbs[0],
146 other.binary_basis_limbs[1],
147 other.binary_basis_limbs[2],
148 other.binary_basis_limbs[3] }
149 , prime_basis_limb(other.prime_basis_limb)
150{}
151
152template <typename Builder, typename T>
153bigfield<Builder, T>::bigfield(bigfield&& other)
154 : context(other.context)
155 , binary_basis_limbs{ other.binary_basis_limbs[0],
156 other.binary_basis_limbs[1],
157 other.binary_basis_limbs[2],
158 other.binary_basis_limbs[3] }
159 , prime_basis_limb(other.prime_basis_limb)
160{}
161
175template <typename Builder, typename T>
177 const uint512_t& value,
178 const bool can_overflow,
179 const size_t maximum_bitlength)
181 ASSERT((can_overflow == true && maximum_bitlength == 0) ||
182 (can_overflow == false && (maximum_bitlength == 0 || maximum_bitlength > (3 * NUM_LIMB_BITS))));
183 std::array<uint256_t, 4> limbs;
184 limbs[0] = value.slice(0, NUM_LIMB_BITS).lo;
185 limbs[1] = value.slice(NUM_LIMB_BITS, NUM_LIMB_BITS * 2).lo;
186 limbs[2] = value.slice(NUM_LIMB_BITS * 2, NUM_LIMB_BITS * 3).lo;
187 limbs[3] = value.slice(NUM_LIMB_BITS * 3, NUM_LIMB_BITS * 4).lo;
189 if constexpr (HasPlookup<Builder>) {
190 field_t<Builder> limb_0(ctx);
191 field_t<Builder> limb_1(ctx);
192 field_t<Builder> limb_2(ctx);
193 field_t<Builder> limb_3(ctx);
194 field_t<Builder> prime_limb(ctx);
195 limb_0.witness_index = ctx->add_variable(barretenberg::fr(limbs[0]));
196 limb_1.witness_index = ctx->add_variable(barretenberg::fr(limbs[1]));
197 limb_2.witness_index = ctx->add_variable(barretenberg::fr(limbs[2]));
198 limb_3.witness_index = ctx->add_variable(barretenberg::fr(limbs[3]));
199 prime_limb.witness_index = ctx->add_variable(limb_0.get_value() + limb_1.get_value() * shift_1 +
200 limb_2.get_value() * shift_2 + limb_3.get_value() * shift_3);
201 // evaluate prime basis limb with addition gate that taps into the 4th wire in the next gate
203 limb_2.witness_index,
204 limb_3.witness_index,
205 prime_limb.witness_index,
206 shift_1,
207 shift_2,
208 shift_3,
209 -1,
210 0 },
211 true);
213 uint64_t num_last_limb_bits = (can_overflow) ? NUM_LIMB_BITS : NUM_LAST_LIMB_BITS;
215 bigfield result(ctx);
216 result.binary_basis_limbs[0] = Limb(limb_0, DEFAULT_MAXIMUM_LIMB);
217 result.binary_basis_limbs[1] = Limb(limb_1, DEFAULT_MAXIMUM_LIMB);
218 result.binary_basis_limbs[2] = Limb(limb_2, DEFAULT_MAXIMUM_LIMB);
219 result.binary_basis_limbs[3] =
220 Limb(limb_3, can_overflow ? DEFAULT_MAXIMUM_LIMB : DEFAULT_MAXIMUM_MOST_SIGNIFICANT_LIMB);
221
222 // if maximum_bitlength is set, this supercedes can_overflow
223 if (maximum_bitlength > 0) {
224 ASSERT(maximum_bitlength > 3 * NUM_LIMB_BITS);
225 num_last_limb_bits = maximum_bitlength - (3 * NUM_LIMB_BITS);
226 uint256_t max_limb_value = (uint256_t(1) << num_last_limb_bits) - 1;
227 result.binary_basis_limbs[3].maximum_value = max_limb_value;
228 }
229 result.prime_basis_limb = prime_limb;
230 ctx->range_constrain_two_limbs(
231 limb_0.witness_index, limb_1.witness_index, (size_t)NUM_LIMB_BITS, (size_t)NUM_LIMB_BITS);
232 ctx->range_constrain_two_limbs(
233 limb_2.witness_index, limb_3.witness_index, (size_t)NUM_LIMB_BITS, (size_t)num_last_limb_bits);
234
235 return result;
236 } else {
237 return bigfield(witness_t(ctx, fr(limbs[0] + limbs[1] * shift_1)),
238 witness_t(ctx, fr(limbs[2] + limbs[3] * shift_1)),
239 can_overflow,
240 maximum_bitlength);
241 }
242}
243
244template <typename Builder, typename T> bigfield<Builder, T>::bigfield(const byte_array<Builder>& bytes)
246 ASSERT(bytes.size() == 32); // we treat input as a 256-bit big integer
247 const auto split_byte_into_nibbles = [](Builder* ctx, const field_t<Builder>& split_byte) {
248 const uint64_t byte_val = uint256_t(split_byte.get_value()).data[0];
249 const uint64_t lo_nibble_val = byte_val & 15ULL;
250 const uint64_t hi_nibble_val = byte_val >> 4;
251
252 const field_t<Builder> lo_nibble(witness_t<Builder>(ctx, lo_nibble_val));
253 const field_t<Builder> hi_nibble(witness_t<Builder>(ctx, hi_nibble_val));
254 lo_nibble.create_range_constraint(4, "bigfield: lo_nibble too large");
255 hi_nibble.create_range_constraint(4, "bigfield: hi_nibble too large");
256
257 const field_t<Builder> sum = lo_nibble + (hi_nibble * 16);
258 sum.assert_equal(split_byte);
259 return std::make_pair<field_t<Builder>, field_t<Builder>>((field_t<Builder>)lo_nibble,
260 (field_t<Builder>)hi_nibble);
261 };
262
263 const auto reconstruct_two_limbs = [&split_byte_into_nibbles](Builder* ctx,
264 const field_t<Builder>& hi_bytes,
265 const field_t<Builder>& lo_bytes,
266 const field_t<Builder>& split_byte) {
267 const auto [lo_nibble, hi_nibble] = split_byte_into_nibbles(ctx, split_byte);
268
269 field_t<Builder> hi_limb = hi_nibble + hi_bytes * 16;
270 field_t<Builder> lo_limb = lo_bytes + lo_nibble * field_t<Builder>(ctx, uint256_t(1) << 64);
271 return std::make_pair<field_t<Builder>, field_t<Builder>>((field_t<Builder>)lo_limb, (field_t<Builder>)hi_limb);
272 };
273 Builder* ctx = bytes.get_context();
274
275 const field_t<Builder> hi_8_bytes(bytes.slice(0, 6));
276 const field_t<Builder> mid_split_byte(bytes.slice(6, 1));
277 const field_t<Builder> mid_8_bytes(bytes.slice(7, 8));
278
279 const field_t<Builder> lo_8_bytes(bytes.slice(15, 8));
280 const field_t<Builder> lo_split_byte(bytes.slice(23, 1));
281 const field_t<Builder> lolo_8_bytes(bytes.slice(24, 8));
282
283 const auto [limb0, limb1] = reconstruct_two_limbs(ctx, lo_8_bytes, lolo_8_bytes, lo_split_byte);
284 const auto [limb2, limb3] = reconstruct_two_limbs(ctx, hi_8_bytes, mid_8_bytes, mid_split_byte);
285
286 const auto res = bigfield(limb0, limb1, limb2, limb3, true);
287
288 const auto num_last_limb_bits = 256 - (NUM_LIMB_BITS * 3);
289 res.binary_basis_limbs[3].maximum_value = (uint64_t(1) << num_last_limb_bits);
290 *this = res;
291}
292
293template <typename Builder, typename T> bigfield<Builder, T>& bigfield<Builder, T>::operator=(const bigfield& other)
294{
295 context = other.context;
296 binary_basis_limbs[0] = other.binary_basis_limbs[0];
297 binary_basis_limbs[1] = other.binary_basis_limbs[1];
298 binary_basis_limbs[2] = other.binary_basis_limbs[2];
299 binary_basis_limbs[3] = other.binary_basis_limbs[3];
300 prime_basis_limb = other.prime_basis_limb;
301 return *this;
302}
303
304template <typename Builder, typename T> bigfield<Builder, T>& bigfield<Builder, T>::operator=(bigfield&& other)
305{
306 context = other.context;
307 binary_basis_limbs[0] = other.binary_basis_limbs[0];
308 binary_basis_limbs[1] = other.binary_basis_limbs[1];
309 binary_basis_limbs[2] = other.binary_basis_limbs[2];
310 binary_basis_limbs[3] = other.binary_basis_limbs[3];
311 prime_basis_limb = other.prime_basis_limb;
312 return *this;
313}
314
315template <typename Builder, typename T> uint512_t bigfield<Builder, T>::get_value() const
316{
317 uint512_t t0 = uint256_t(binary_basis_limbs[0].element.get_value());
318 uint512_t t1 = uint256_t(binary_basis_limbs[1].element.get_value());
319 uint512_t t2 = uint256_t(binary_basis_limbs[2].element.get_value());
320 uint512_t t3 = uint256_t(binary_basis_limbs[3].element.get_value());
321 return t0 + (t1 << (NUM_LIMB_BITS)) + (t2 << (2 * NUM_LIMB_BITS)) + (t3 << (3 * NUM_LIMB_BITS));
322}
323
324template <typename Builder, typename T> uint512_t bigfield<Builder, T>::get_maximum_value() const
325{
326 uint512_t t0 = uint512_t(binary_basis_limbs[0].maximum_value);
327 uint512_t t1 = uint512_t(binary_basis_limbs[1].maximum_value) << NUM_LIMB_BITS;
328 uint512_t t2 = uint512_t(binary_basis_limbs[2].maximum_value) << (NUM_LIMB_BITS * 2);
329 uint512_t t3 = uint512_t(binary_basis_limbs[3].maximum_value) << (NUM_LIMB_BITS * 3);
330 return t0 + t1 + t2 + t3;
331}
332
348template <typename Builder, typename T>
350 uint256_t other_maximum_value) const
351{
352 reduction_check();
353 ASSERT((other_maximum_value + binary_basis_limbs[0].maximum_value) <= get_maximum_unreduced_limb_value());
354 // needed cause a constant doesn't have a valid context
355 Builder* ctx = context ? context : other.context;
356
357 if (is_constant() && other.is_constant()) {
358 return bigfield(ctx, uint256_t((get_value() + uint256_t(other.get_value())) % modulus_u512));
359 }
360 bigfield result = *this;
361 result.binary_basis_limbs[0].maximum_value = binary_basis_limbs[0].maximum_value + other_maximum_value;
362
363 result.binary_basis_limbs[0].element = binary_basis_limbs[0].element + other;
364 result.prime_basis_limb = prime_basis_limb + other;
365 return result;
366}
367
368template <typename Builder, typename T>
370{
371 reduction_check();
372 other.reduction_check();
373 // needed cause a constant doesn't have a valid context
374 Builder* ctx = context ? context : other.context;
375
376 if (is_constant() && other.is_constant()) {
377 return bigfield(ctx, uint256_t((get_value() + other.get_value()) % modulus_u512));
378 }
379 bigfield result(ctx);
380 result.binary_basis_limbs[0].maximum_value =
381 binary_basis_limbs[0].maximum_value + other.binary_basis_limbs[0].maximum_value;
382 result.binary_basis_limbs[1].maximum_value =
383 binary_basis_limbs[1].maximum_value + other.binary_basis_limbs[1].maximum_value;
384 result.binary_basis_limbs[2].maximum_value =
385 binary_basis_limbs[2].maximum_value + other.binary_basis_limbs[2].maximum_value;
386 result.binary_basis_limbs[3].maximum_value =
387 binary_basis_limbs[3].maximum_value + other.binary_basis_limbs[3].maximum_value;
388
389 if constexpr (HasPlookup<Builder>) {
390 if (prime_basis_limb.multiplicative_constant == 1 && other.prime_basis_limb.multiplicative_constant == 1 &&
391 !is_constant() && !other.is_constant()) {
392 bool limbconst = binary_basis_limbs[0].element.is_constant();
393 limbconst = limbconst || binary_basis_limbs[1].element.is_constant();
394 limbconst = limbconst || binary_basis_limbs[2].element.is_constant();
395 limbconst = limbconst || binary_basis_limbs[3].element.is_constant();
396 limbconst = limbconst || prime_basis_limb.is_constant();
397 limbconst = limbconst || other.binary_basis_limbs[0].element.is_constant();
398 limbconst = limbconst || other.binary_basis_limbs[1].element.is_constant();
399 limbconst = limbconst || other.binary_basis_limbs[2].element.is_constant();
400 limbconst = limbconst || other.binary_basis_limbs[3].element.is_constant();
401 limbconst = limbconst || other.prime_basis_limb.is_constant();
402 limbconst = limbconst || (prime_basis_limb.witness_index == other.prime_basis_limb.witness_index);
403 if (!limbconst) {
404 std::pair<uint32_t, barretenberg::fr> x0{ binary_basis_limbs[0].element.witness_index,
405 binary_basis_limbs[0].element.multiplicative_constant };
406 std::pair<uint32_t, barretenberg::fr> x1{ binary_basis_limbs[1].element.witness_index,
407 binary_basis_limbs[1].element.multiplicative_constant };
408 std::pair<uint32_t, barretenberg::fr> x2{ binary_basis_limbs[2].element.witness_index,
409 binary_basis_limbs[2].element.multiplicative_constant };
410 std::pair<uint32_t, barretenberg::fr> x3{ binary_basis_limbs[3].element.witness_index,
411 binary_basis_limbs[3].element.multiplicative_constant };
412 std::pair<uint32_t, barretenberg::fr> y0{ other.binary_basis_limbs[0].element.witness_index,
413 other.binary_basis_limbs[0].element.multiplicative_constant };
414 std::pair<uint32_t, barretenberg::fr> y1{ other.binary_basis_limbs[1].element.witness_index,
415 other.binary_basis_limbs[1].element.multiplicative_constant };
416 std::pair<uint32_t, barretenberg::fr> y2{ other.binary_basis_limbs[2].element.witness_index,
417 other.binary_basis_limbs[2].element.multiplicative_constant };
418 std::pair<uint32_t, barretenberg::fr> y3{ other.binary_basis_limbs[3].element.witness_index,
419 other.binary_basis_limbs[3].element.multiplicative_constant };
420 barretenberg::fr c0(binary_basis_limbs[0].element.additive_constant +
421 other.binary_basis_limbs[0].element.additive_constant);
422 barretenberg::fr c1(binary_basis_limbs[1].element.additive_constant +
423 other.binary_basis_limbs[1].element.additive_constant);
424 barretenberg::fr c2(binary_basis_limbs[2].element.additive_constant +
425 other.binary_basis_limbs[2].element.additive_constant);
426 barretenberg::fr c3(binary_basis_limbs[3].element.additive_constant +
427 other.binary_basis_limbs[3].element.additive_constant);
428
429 uint32_t xp(prime_basis_limb.witness_index);
430 uint32_t yp(other.prime_basis_limb.witness_index);
431 barretenberg::fr cp(prime_basis_limb.additive_constant + other.prime_basis_limb.additive_constant);
432
433 const auto output_witnesses = ctx->evaluate_non_native_field_addition(
434 { x0, y0, c0 }, { x1, y1, c1 }, { x2, y2, c2 }, { x3, y3, c3 }, { xp, yp, cp });
435 result.binary_basis_limbs[0].element = field_t<Builder>::from_witness_index(ctx, output_witnesses[0]);
436 result.binary_basis_limbs[1].element = field_t<Builder>::from_witness_index(ctx, output_witnesses[1]);
437 result.binary_basis_limbs[2].element = field_t<Builder>::from_witness_index(ctx, output_witnesses[2]);
438 result.binary_basis_limbs[3].element = field_t<Builder>::from_witness_index(ctx, output_witnesses[3]);
439 result.prime_basis_limb = field_t<Builder>::from_witness_index(ctx, output_witnesses[4]);
440 return result;
441 }
442 }
443 }
444
445 result.binary_basis_limbs[0].element = binary_basis_limbs[0].element + other.binary_basis_limbs[0].element;
446 result.binary_basis_limbs[1].element = binary_basis_limbs[1].element + other.binary_basis_limbs[1].element;
447 result.binary_basis_limbs[2].element = binary_basis_limbs[2].element + other.binary_basis_limbs[2].element;
448 result.binary_basis_limbs[3].element = binary_basis_limbs[3].element + other.binary_basis_limbs[3].element;
449 result.prime_basis_limb = prime_basis_limb + other.prime_basis_limb;
450 return result;
451}
452
453// to make sure we don't go to negative values, add p before subtracting other
476template <typename Builder, typename T>
478{
479 Builder* ctx = context ? context : other.context;
480 reduction_check();
481 other.reduction_check();
482
483 if (is_constant() && other.is_constant()) {
484 uint512_t left = get_value() % modulus_u512;
485 uint512_t right = other.get_value() % modulus_u512;
486 uint512_t out = (left + modulus_u512 - right) % modulus_u512;
487 return bigfield(ctx, uint256_t(out.lo));
488 }
489
490 if (other.is_constant()) {
491 uint512_t right = other.get_value() % modulus_u512;
492 uint512_t neg_right = (modulus_u512 - right) % modulus_u512;
493 return operator+(bigfield(ctx, uint256_t(neg_right.lo)));
494 }
495
513 bigfield result(ctx);
514
523 uint256_t limb_0_maximum_value = other.binary_basis_limbs[0].maximum_value;
524
525 // Compute maximum shift factor for limb_0
526 uint64_t limb_0_borrow_shift = std::max(limb_0_maximum_value.get_msb() + 1, NUM_LIMB_BITS);
527
528 // Compute the maximum negative value of limb_1, including the bits limb_0 may need to borrow
529 uint256_t limb_1_maximum_value =
530 other.binary_basis_limbs[1].maximum_value + (uint256_t(1) << (limb_0_borrow_shift - NUM_LIMB_BITS));
531
532 // repeat the above for the remaining limbs
533 uint64_t limb_1_borrow_shift = std::max(limb_1_maximum_value.get_msb() + 1, NUM_LIMB_BITS);
534 uint256_t limb_2_maximum_value =
535 other.binary_basis_limbs[2].maximum_value + (uint256_t(1) << (limb_1_borrow_shift - NUM_LIMB_BITS));
536 uint64_t limb_2_borrow_shift = std::max(limb_2_maximum_value.get_msb() + 1, NUM_LIMB_BITS);
537
538 uint256_t limb_3_maximum_value =
539 other.binary_basis_limbs[3].maximum_value + (uint256_t(1) << (limb_2_borrow_shift - NUM_LIMB_BITS));
540
549 uint512_t constant_to_add = modulus_u512;
550 // add a large enough multiple of p to not get negative result in subtraction
551 while (constant_to_add.slice(NUM_LIMB_BITS * 3, NUM_LIMB_BITS * 4).lo <= limb_3_maximum_value) {
552 constant_to_add += modulus_u512;
553 }
554
568 uint256_t t0(uint256_t(1) << limb_0_borrow_shift);
569 uint256_t t1((uint256_t(1) << limb_1_borrow_shift) - (uint256_t(1) << (limb_0_borrow_shift - NUM_LIMB_BITS)));
570 uint256_t t2((uint256_t(1) << limb_2_borrow_shift) - (uint256_t(1) << (limb_1_borrow_shift - NUM_LIMB_BITS)));
571 uint256_t t3(uint256_t(1) << (limb_2_borrow_shift - NUM_LIMB_BITS));
572
577 uint256_t to_add_0 = uint256_t(constant_to_add.slice(0, NUM_LIMB_BITS)) + t0;
578 uint256_t to_add_1 = uint256_t(constant_to_add.slice(NUM_LIMB_BITS, NUM_LIMB_BITS * 2)) + t1;
579 uint256_t to_add_2 = uint256_t(constant_to_add.slice(NUM_LIMB_BITS * 2, NUM_LIMB_BITS * 3)) + t2;
580 uint256_t to_add_3 = uint256_t(constant_to_add.slice(NUM_LIMB_BITS * 3, NUM_LIMB_BITS * 4)) - t3;
581
585 result.binary_basis_limbs[0].maximum_value = binary_basis_limbs[0].maximum_value + to_add_0;
586 result.binary_basis_limbs[1].maximum_value = binary_basis_limbs[1].maximum_value + to_add_1;
587 result.binary_basis_limbs[2].maximum_value = binary_basis_limbs[2].maximum_value + to_add_2;
588 result.binary_basis_limbs[3].maximum_value = binary_basis_limbs[3].maximum_value + to_add_3;
589
593 result.binary_basis_limbs[0].element = binary_basis_limbs[0].element + barretenberg::fr(to_add_0);
594 result.binary_basis_limbs[1].element = binary_basis_limbs[1].element + barretenberg::fr(to_add_1);
595 result.binary_basis_limbs[2].element = binary_basis_limbs[2].element + barretenberg::fr(to_add_2);
596 result.binary_basis_limbs[3].element = binary_basis_limbs[3].element + barretenberg::fr(to_add_3);
597
598 if constexpr (HasPlookup<Builder>) {
599 if (prime_basis_limb.multiplicative_constant == 1 && other.prime_basis_limb.multiplicative_constant == 1 &&
600 !is_constant() && !other.is_constant()) {
601 bool limbconst = result.binary_basis_limbs[0].element.is_constant();
602 limbconst = limbconst || result.binary_basis_limbs[1].element.is_constant();
603 limbconst = limbconst || result.binary_basis_limbs[2].element.is_constant();
604 limbconst = limbconst || result.binary_basis_limbs[3].element.is_constant();
605 limbconst = limbconst || prime_basis_limb.is_constant();
606 limbconst = limbconst || other.binary_basis_limbs[0].element.is_constant();
607 limbconst = limbconst || other.binary_basis_limbs[1].element.is_constant();
608 limbconst = limbconst || other.binary_basis_limbs[2].element.is_constant();
609 limbconst = limbconst || other.binary_basis_limbs[3].element.is_constant();
610 limbconst = limbconst || other.prime_basis_limb.is_constant();
611 limbconst = limbconst || (prime_basis_limb.witness_index == other.prime_basis_limb.witness_index);
612 if (!limbconst) {
613 std::pair<uint32_t, barretenberg::fr> x0{ result.binary_basis_limbs[0].element.witness_index,
614 binary_basis_limbs[0].element.multiplicative_constant };
615 std::pair<uint32_t, barretenberg::fr> x1{ result.binary_basis_limbs[1].element.witness_index,
616 binary_basis_limbs[1].element.multiplicative_constant };
617 std::pair<uint32_t, barretenberg::fr> x2{ result.binary_basis_limbs[2].element.witness_index,
618 binary_basis_limbs[2].element.multiplicative_constant };
619 std::pair<uint32_t, barretenberg::fr> x3{ result.binary_basis_limbs[3].element.witness_index,
620 binary_basis_limbs[3].element.multiplicative_constant };
621 std::pair<uint32_t, barretenberg::fr> y0{ other.binary_basis_limbs[0].element.witness_index,
622 other.binary_basis_limbs[0].element.multiplicative_constant };
623 std::pair<uint32_t, barretenberg::fr> y1{ other.binary_basis_limbs[1].element.witness_index,
624 other.binary_basis_limbs[1].element.multiplicative_constant };
625 std::pair<uint32_t, barretenberg::fr> y2{ other.binary_basis_limbs[2].element.witness_index,
626 other.binary_basis_limbs[2].element.multiplicative_constant };
627 std::pair<uint32_t, barretenberg::fr> y3{ other.binary_basis_limbs[3].element.witness_index,
628 other.binary_basis_limbs[3].element.multiplicative_constant };
629 barretenberg::fr c0(result.binary_basis_limbs[0].element.additive_constant -
630 other.binary_basis_limbs[0].element.additive_constant);
631 barretenberg::fr c1(result.binary_basis_limbs[1].element.additive_constant -
632 other.binary_basis_limbs[1].element.additive_constant);
633 barretenberg::fr c2(result.binary_basis_limbs[2].element.additive_constant -
634 other.binary_basis_limbs[2].element.additive_constant);
635 barretenberg::fr c3(result.binary_basis_limbs[3].element.additive_constant -
636 other.binary_basis_limbs[3].element.additive_constant);
637
638 uint32_t xp(prime_basis_limb.witness_index);
639 uint32_t yp(other.prime_basis_limb.witness_index);
640 barretenberg::fr cp(prime_basis_limb.additive_constant - other.prime_basis_limb.additive_constant);
641 uint512_t constant_to_add_mod_p = (constant_to_add) % prime_basis.modulus;
642 cp += barretenberg::fr(constant_to_add_mod_p.lo);
643
644 const auto output_witnesses = ctx->evaluate_non_native_field_subtraction(
645 { x0, y0, c0 }, { x1, y1, c1 }, { x2, y2, c2 }, { x3, y3, c3 }, { xp, yp, cp });
646
647 result.binary_basis_limbs[0].element = field_t<Builder>::from_witness_index(ctx, output_witnesses[0]);
648 result.binary_basis_limbs[1].element = field_t<Builder>::from_witness_index(ctx, output_witnesses[1]);
649 result.binary_basis_limbs[2].element = field_t<Builder>::from_witness_index(ctx, output_witnesses[2]);
650 result.binary_basis_limbs[3].element = field_t<Builder>::from_witness_index(ctx, output_witnesses[3]);
651 result.prime_basis_limb = field_t<Builder>::from_witness_index(ctx, output_witnesses[4]);
652 return result;
653 }
654 }
655 }
656
657 result.binary_basis_limbs[0].element -= other.binary_basis_limbs[0].element;
658 result.binary_basis_limbs[1].element -= other.binary_basis_limbs[1].element;
659 result.binary_basis_limbs[2].element -= other.binary_basis_limbs[2].element;
660 result.binary_basis_limbs[3].element -= other.binary_basis_limbs[3].element;
661
665 uint512_t constant_to_add_mod_p = (constant_to_add) % prime_basis.modulus;
666 field_t prime_basis_to_add(ctx, barretenberg::fr(constant_to_add_mod_p.lo));
667 result.prime_basis_limb = prime_basis_limb + prime_basis_to_add;
668 result.prime_basis_limb -= other.prime_basis_limb;
669 return result;
670}
671
680template <typename Builder, typename T>
682{
683 // First we do basic reduction checks of individual elements
684 reduction_check();
685 other.reduction_check();
686 Builder* ctx = context ? context : other.context;
687 // Now we can actually compute the quotient and remainder values
688 const auto [quotient_value, remainder_value] = compute_quotient_remainder_values(*this, other, {});
689 bigfield remainder;
690 bigfield quotient;
691 // If operands are constant, define result as a constant value and return
692 if (is_constant() && other.is_constant()) {
693 remainder = bigfield(ctx, uint256_t(remainder_value.lo));
694 return remainder;
695 } else {
696 // when writing a*b = q*p + r we wish to enforce r<2^s for smallest s such that p<2^s
697 // hence the second constructor call is with can_overflow=false. This will allow using r in more additions mod
698 // 2^t without needing to apply the mod, where t=4*NUM_LIMB_BITS
699
700 // Check if the product overflows CRT or the quotient can't be contained in a range proof and reduce accordingly
701 auto [reduction_required, num_quotient_bits] =
702 get_quotient_reduction_info({ get_maximum_value() }, { other.get_maximum_value() }, {});
703 if (reduction_required) {
704 if (get_maximum_value() > other.get_maximum_value()) {
705 self_reduce();
706 } else {
707 other.self_reduce();
708 }
709 return (*this).operator*(other);
710 }
711 quotient = create_from_u512_as_witness(ctx, quotient_value, false, num_quotient_bits);
712 remainder = create_from_u512_as_witness(ctx, remainder_value);
713 };
714
715 // Call `evaluate_multiply_add` to validate the correctness of our computed quotient and remainder
716 unsafe_evaluate_multiply_add(*this, other, {}, quotient, { remainder });
717 return remainder;
718}
719
726template <typename Builder, typename T>
728{
729
730 return internal_div({ *this }, other, false);
731}
740template <typename Builder, typename T>
741bigfield<Builder, T> bigfield<Builder, T>::sum(const std::vector<bigfield>& terms)
742{
743 ASSERT(terms.size() > 0);
744
745 if (terms.size() == 1) {
746 return terms[0];
747 }
748 std::vector<bigfield> halved;
749 for (size_t i = 0; i < terms.size() / 2; i++) {
750 halved.push_back(terms[2 * i] + terms[2 * i + 1]);
751 }
752 if (terms.size() & 1) {
753 halved.push_back(terms[terms.size() - 1]);
754 }
755 return sum(halved);
756}
757
767template <typename Builder, typename T>
768bigfield<Builder, T> bigfield<Builder, T>::internal_div(const std::vector<bigfield>& numerators,
769 const bigfield& denominator,
770 bool check_for_zero)
771{
772 if (numerators.size() == 0) {
773 return bigfield<Builder, T>(denominator.get_context(), uint256_t(0));
774 }
775
776 denominator.reduction_check();
777 Builder* ctx = denominator.context;
778 uint512_t numerator_values(0);
779 bool numerator_constant = true;
780 for (const auto& numerator_element : numerators) {
781 ctx = (ctx == nullptr) ? numerator_element.get_context() : ctx;
782 numerator_element.reduction_check();
783 numerator_values += numerator_element.get_value();
784 numerator_constant = numerator_constant && (numerator_element.is_constant());
785 }
786
787 // a / b = c
788 // => c * b = a mod p
789 const uint1024_t left = uint1024_t(numerator_values);
790 const uint1024_t right = uint1024_t(denominator.get_value());
791 const uint1024_t modulus(target_basis.modulus);
792 uint512_t inverse_value = right.lo.invmod(target_basis.modulus).lo;
793 uint1024_t inverse_1024(inverse_value);
794 inverse_value = ((left * inverse_1024) % modulus).lo;
795
796 const uint1024_t quotient_1024 =
797 (uint1024_t(inverse_value) * right + unreduced_zero().get_value() - left) / modulus;
798 const uint512_t quotient_value = quotient_1024.lo;
799
800 bigfield inverse;
801 bigfield quotient;
802 if (numerator_constant && denominator.is_constant()) {
803 inverse = bigfield(ctx, uint256_t(inverse_value));
804 return inverse;
805 } else {
806 // We only add the check if the result is non-constant
807 std::vector<uint1024_t> numerator_max;
808 for (const auto& n : numerators) {
809 numerator_max.push_back(n.get_maximum_value());
810 }
811
812 auto [reduction_required, num_quotient_bits] =
813 get_quotient_reduction_info({ static_cast<uint512_t>(DEFAULT_MAXIMUM_REMAINDER) },
814 { denominator.get_maximum_value() },
815 { unreduced_zero() },
816 numerator_max);
817 if (reduction_required) {
818
819 denominator.self_reduce();
820 return internal_div(numerators, denominator, check_for_zero);
821 }
822 // We do this after the quotient check, since this creates gates and we don't want to do this twice
823 if (check_for_zero) {
824 denominator.assert_is_not_equal(zero());
825 }
826
827 quotient = create_from_u512_as_witness(ctx, quotient_value, false, num_quotient_bits);
828 inverse = create_from_u512_as_witness(ctx, inverse_value);
829 }
830
831 unsafe_evaluate_multiply_add(denominator, inverse, { unreduced_zero() }, quotient, numerators);
832 return inverse;
833}
834
841template <typename Builder, typename T>
843 const bigfield& denominator)
844{
845 return internal_div(numerators, denominator, false);
846}
847
855template <typename Builder, typename T>
857 const bigfield& denominator)
858{
859 return internal_div(numerators, denominator, true);
860}
866template <typename Builder, typename T> bigfield<Builder, T> bigfield<Builder, T>::sqr() const
867{
868 reduction_check();
869 Builder* ctx = context;
870
871 const auto [quotient_value, remainder_value] = compute_quotient_remainder_values(*this, *this, {});
872
873 bigfield remainder;
874 bigfield quotient;
875 if (is_constant()) {
876 remainder = bigfield(ctx, uint256_t(remainder_value.lo));
877 return remainder;
878 } else {
879
880 auto [reduction_required, num_quotient_bits] = get_quotient_reduction_info(
881 { get_maximum_value() }, { get_maximum_value() }, {}, { DEFAULT_MAXIMUM_REMAINDER });
882 if (reduction_required) {
883 self_reduce();
884 return sqr();
885 }
886
887 quotient = create_from_u512_as_witness(ctx, quotient_value, false, num_quotient_bits);
888 remainder = create_from_u512_as_witness(ctx, remainder_value);
889 };
890
891 unsafe_evaluate_square_add(*this, {}, quotient, remainder);
892 return remainder;
893}
894
903template <typename Builder, typename T>
904bigfield<Builder, T> bigfield<Builder, T>::sqradd(const std::vector<bigfield>& to_add) const
905{
906 reduction_check();
907
908 Builder* ctx = context;
909
910 uint512_t add_values(0);
911 bool add_constant = true;
912 for (const auto& add_element : to_add) {
913 add_element.reduction_check();
914 add_values += add_element.get_value();
915 add_constant = add_constant && (add_element.is_constant());
916 }
917
918 const uint1024_t left(get_value());
919 const uint1024_t right(get_value());
920 const uint1024_t add_right(add_values);
921 const uint1024_t modulus(target_basis.modulus);
922
923 bigfield remainder;
924 bigfield quotient;
925 if (is_constant()) {
926 if (add_constant) {
927
928 const auto [quotient_1024, remainder_1024] = (left * right + add_right).divmod(modulus);
929 remainder = bigfield(ctx, uint256_t(remainder_1024.lo.lo));
930 return remainder;
931 } else {
932
933 const auto [quotient_1024, remainder_1024] = (left * right).divmod(modulus);
934 std::vector<bigfield> new_to_add;
935 for (auto& add_element : to_add) {
936 new_to_add.push_back(add_element);
937 }
938
939 new_to_add.push_back(bigfield(ctx, remainder_1024.lo.lo));
940 return sum(new_to_add);
941 }
942 } else {
943
944 // Check the quotient fits the range proof
945 auto [reduction_required, num_quotient_bits] = get_quotient_reduction_info(
946 { get_maximum_value() }, { get_maximum_value() }, to_add, { DEFAULT_MAXIMUM_REMAINDER });
947
948 if (reduction_required) {
949 self_reduce();
950 return sqradd(to_add);
951 }
952 const auto [quotient_1024, remainder_1024] = (left * right + add_right).divmod(modulus);
953 uint512_t quotient_value = quotient_1024.lo;
954 uint256_t remainder_value = remainder_1024.lo.lo;
955
956 quotient = create_from_u512_as_witness(ctx, quotient_value, false, num_quotient_bits);
957 remainder = create_from_u512_as_witness(ctx, remainder_value);
958 };
959 unsafe_evaluate_square_add(*this, to_add, quotient, remainder);
960 return remainder;
961}
962
971template <typename Builder, typename T>
972bigfield<Builder, T> bigfield<Builder, T>::madd(const bigfield& to_mul, const std::vector<bigfield>& to_add) const
973{
974 Builder* ctx = context ? context : to_mul.context;
975 reduction_check();
976 to_mul.reduction_check();
977
978 uint512_t add_values(0);
979 bool add_constant = true;
980
981 for (const auto& add_element : to_add) {
982 add_element.reduction_check();
983 add_values += add_element.get_value();
984 add_constant = add_constant && (add_element.is_constant());
985 }
986
987 const uint1024_t left(get_value());
988 const uint1024_t mul_right(to_mul.get_value());
989 const uint1024_t add_right(add_values);
990 const uint1024_t modulus(target_basis.modulus);
991
992 const auto [quotient_1024, remainder_1024] = (left * mul_right + add_right).divmod(modulus);
993
994 const uint512_t quotient_value = quotient_1024.lo;
995 const uint512_t remainder_value = remainder_1024.lo;
996
997 bigfield remainder;
998 bigfield quotient;
999 if (is_constant() && to_mul.is_constant() && add_constant) {
1000 remainder = bigfield(ctx, uint256_t(remainder_value.lo));
1001 return remainder;
1002 } else {
1003
1004 auto [reduction_required, num_quotient_bits] = get_quotient_reduction_info(
1005 { get_maximum_value() }, { to_mul.get_maximum_value() }, to_add, { DEFAULT_MAXIMUM_REMAINDER });
1006 if (reduction_required) {
1007 if (get_maximum_value() > to_mul.get_maximum_value()) {
1008 self_reduce();
1009 } else {
1010 to_mul.self_reduce();
1011 }
1012 return (*this).madd(to_mul, to_add);
1013 }
1014 quotient = create_from_u512_as_witness(ctx, quotient_value, false, num_quotient_bits);
1015 remainder = create_from_u512_as_witness(ctx, remainder_value);
1016 };
1017 unsafe_evaluate_multiply_add(*this, to_mul, to_add, quotient, { remainder });
1018 return remainder;
1019}
1020
1021// MERGENOTE: Implementing dual_madd in terms of mult_madd following #729
1022
1034template <typename Builder, typename T>
1036 std::vector<bigfield>& mul_right,
1037 const std::vector<bigfield>& to_add)
1038{
1039 const size_t number_of_products = mul_left.size();
1040 // Get the maximum values of elements
1041 std::vector<uint512_t> max_values_left;
1042 std::vector<uint512_t> max_values_right;
1043
1044 max_values_left.reserve(number_of_products);
1045 max_values_right.reserve(number_of_products);
1046 // Do regular reduction checks for all elements
1047 for (auto& left_element : mul_left) {
1048 left_element.reduction_check();
1049 max_values_left.emplace_back(left_element.get_maximum_value());
1050 }
1051
1052 for (auto& right_element : mul_right) {
1053 right_element.reduction_check();
1054 max_values_right.emplace_back(right_element.get_maximum_value());
1055 }
1056
1057 // Perform CRT checks for the whole evaluation
1058 // 1. Check if we can overflow CRT modulus
1059 // 2. Check if the quotient actually fits in our range proof.
1060 // 3. If we haven't passed one of the checks, reduce accordingly, starting with the largest product
1061
1062 // We only get the bitlength of range proof if there is no reduction
1063 bool reduction_required;
1064 reduction_required = std::get<0>(
1065 get_quotient_reduction_info(max_values_left, max_values_right, to_add, { DEFAULT_MAXIMUM_REMAINDER }));
1066
1067 if (reduction_required) {
1068
1069 // We are out of luck and have to reduce the elements to keep the intermediate result below CRT modulus
1070 // For that we need to compute the maximum update - how much reducing each element is going to update the
1071 // quotient.
1072 // Contents of the tuple: | Qmax_before-Qmax_after | product number | argument number |
1073 std::vector<std::tuple<uint1024_t, size_t, size_t>> maximum_value_updates;
1074
1075 // We use this lambda function before the loop and in the loop itself
1076 // It computes the maximum value update from reduction of each element
1077 auto compute_updates = [](std::vector<std::tuple<uint1024_t, size_t, size_t>>& maxval_updates,
1078 std::vector<bigfield>& m_left,
1079 std::vector<bigfield>& m_right,
1080 size_t number_of_products) {
1081 maxval_updates.resize(0);
1082 maxval_updates.reserve(number_of_products * 2);
1083 // Compute all reduction differences
1084 for (size_t i = 0; i < number_of_products; i++) {
1085 uint1024_t original_left = static_cast<uint1024_t>(m_left[i].get_maximum_value());
1086 uint1024_t original_right = static_cast<uint1024_t>(m_right[i].get_maximum_value());
1087 uint1024_t original_product = original_left * original_right;
1088 if (m_left[i].is_constant()) {
1089 // If the multiplicand is constant, we can't reduce it, so the update is 0.
1090 maxval_updates.emplace_back(std::tuple<uint1024_t, size_t, size_t>(0, i, 0));
1091 } else {
1092 uint1024_t new_product = DEFAULT_MAXIMUM_REMAINDER * original_right;
1093 if (new_product > original_product) {
1094 throw_or_abort("bigfield: This should never happen");
1095 }
1096 maxval_updates.emplace_back(
1097 std::tuple<uint1024_t, size_t, size_t>(original_product - new_product, i, 0));
1098 }
1099 if (m_right[i].is_constant()) {
1100 // If the multiplicand is constant, we can't reduce it, so the update is 0.
1101 maxval_updates.emplace_back(std::tuple<uint1024_t, size_t, size_t>(0, i, 1));
1102 } else {
1103 uint1024_t new_product = DEFAULT_MAXIMUM_REMAINDER * original_left;
1104 if (new_product > original_product) {
1105 throw_or_abort("bigfield: This should never happen");
1106 }
1107 maxval_updates.emplace_back(
1108 std::tuple<uint1024_t, size_t, size_t>(original_product - new_product, i, 1));
1109 }
1110 }
1111 };
1112
1113 // Compute the possible reduction updates
1114 compute_updates(maximum_value_updates, mul_left, mul_right, number_of_products);
1115 auto compare_update_tuples = [](std::tuple<uint1024_t, size_t, size_t>& left_element,
1116 std::tuple<uint1024_t, size_t, size_t>& right_element) {
1117 return std::get<0>(left_element) > std::get<0>(right_element);
1118 };
1119
1120 // Sort the vector, larger values first
1121 std::sort(maximum_value_updates.begin(), maximum_value_updates.end(), compare_update_tuples);
1122 // Now we loop through, reducing 1 element each time. This is costly in code, but allows us to use fewer
1123 // gates
1124
1125 while (reduction_required) {
1126
1127 // We choose the largest update
1128 auto [update_size, largest_update_product_index, multiplicand_index] = maximum_value_updates[0];
1129 if (!update_size) {
1130 throw_or_abort("bigfield: Can't reduce further");
1131 }
1132 // Reduce the larger of the multiplicands that compose the product
1133 if (multiplicand_index == 0) {
1134 mul_left[largest_update_product_index].self_reduce();
1135 } else {
1136 mul_right[largest_update_product_index].self_reduce();
1137 }
1138
1139 reduction_required = std::get<0>(
1140 get_quotient_reduction_info(max_values_left, max_values_right, to_add, { DEFAULT_MAXIMUM_REMAINDER }));
1141
1142 compute_updates(maximum_value_updates, mul_left, mul_right, number_of_products);
1143
1144 for (size_t i = 0; i < number_of_products; i++) {
1145 max_values_left[i] = mul_left[i].get_maximum_value();
1146 max_values_right[i] = mul_right[i].get_maximum_value();
1147 }
1148
1149 // Sort the the vector
1150 std::sort(maximum_value_updates.begin(), maximum_value_updates.end(), compare_update_tuples);
1151 }
1152 // Now we have reduced everything exactly to the point of no overflow. There is probably a way to use even
1153 // fewer reductions, but for now this will suffice.
1154 }
1155}
1156
1166template <typename Builder, typename T>
1167bigfield<Builder, T> bigfield<Builder, T>::mult_madd(const std::vector<bigfield>& mul_left,
1168 const std::vector<bigfield>& mul_right,
1169 const std::vector<bigfield>& to_add,
1170 bool fix_remainder_to_zero)
1171{
1172 ASSERT(mul_left.size() == mul_right.size());
1173
1174 std::vector<bigfield> mutable_mul_left(mul_left);
1175 std::vector<bigfield> mutable_mul_right(mul_right);
1176
1177 const size_t number_of_products = mul_left.size();
1178
1179 const uint1024_t modulus(target_basis.modulus);
1180 uint1024_t worst_case_product_sum(0);
1181 uint1024_t add_right_constant_sum(0);
1182
1183 // First we do all constant optimizations
1184 bool add_constant = true;
1185 std::vector<bigfield> new_to_add;
1186
1187 for (const auto& add_element : to_add) {
1188 add_element.reduction_check();
1189 if (add_element.is_constant()) {
1190 add_right_constant_sum += uint1024_t(add_element.get_value());
1191 } else {
1192 add_constant = false;
1193 new_to_add.push_back(add_element);
1194 }
1195 }
1196
1197 // Compute the product sum
1198 // Optimize constant use
1199 uint1024_t sum_of_constant_products(0);
1200 std::vector<bigfield> new_input_left;
1201 std::vector<bigfield> new_input_right;
1202 bool product_sum_constant = true;
1203 for (size_t i = 0; i < number_of_products; i++) {
1204 if (mutable_mul_left[i].is_constant() && mutable_mul_right[i].is_constant()) {
1205 // If constant, just add to the sum
1206 sum_of_constant_products +=
1207 uint1024_t(mutable_mul_left[i].get_value()) * uint1024_t(mutable_mul_right[i].get_value());
1208 } else {
1209 // If not, add to nonconstant sum and remember the elements
1210 new_input_left.push_back(mutable_mul_left[i]);
1211 new_input_right.push_back(mutable_mul_right[i]);
1212 product_sum_constant = false;
1213 }
1214 }
1215
1216 Builder* ctx = nullptr;
1217 // Search through all multiplicands on the left
1218 for (auto& el : mutable_mul_left) {
1219 if (el.context) {
1220 ctx = el.context;
1221 break;
1222 }
1223 }
1224 // And on the right
1225 if (!ctx) {
1226 for (auto& el : mutable_mul_right) {
1227 if (el.context) {
1228 ctx = el.context;
1229 break;
1230 }
1231 }
1232 }
1233 if (product_sum_constant) {
1234 if (add_constant) {
1235 // Simply return the constant, no need unsafe_multiply_add
1236 const auto [quotient_1024, remainder_1024] =
1237 (sum_of_constant_products + add_right_constant_sum).divmod(modulus);
1238 ASSERT(!fix_remainder_to_zero || remainder_1024 == 0);
1239 return bigfield(ctx, uint256_t(remainder_1024.lo.lo));
1240 } else {
1241 const auto [quotient_1024, remainder_1024] =
1242 (sum_of_constant_products + add_right_constant_sum).divmod(modulus);
1243 uint256_t remainder_value = remainder_1024.lo.lo;
1244 bigfield result;
1245 if (remainder_value == uint256_t(0)) {
1246 // No need to add extra term to new_to_add
1247 result = sum(new_to_add);
1248 } else {
1249 // Add the constant term
1250 new_to_add.push_back(bigfield(ctx, uint256_t(remainder_value)));
1251 result = sum(new_to_add);
1252 }
1253 if (fix_remainder_to_zero) {
1254 result.self_reduce();
1255 result.assert_equal(zero());
1256 }
1257 return result;
1258 }
1259 }
1260
1261 // Now that we know that there is at least 1 non-constant multiplication, we can start estimating reductions, etc
1262
1263 // Compute the constant term we're adding
1264 const auto [_, constant_part_remainder_1024] = (sum_of_constant_products + add_right_constant_sum).divmod(modulus);
1265 const uint256_t constant_part_remainder_256 = constant_part_remainder_1024.lo.lo;
1266
1267 if (constant_part_remainder_256 != uint256_t(0)) {
1268 new_to_add.push_back(bigfield(ctx, constant_part_remainder_256));
1269 }
1270 // Compute added sum
1271 uint1024_t add_right_final_sum(0);
1272 uint1024_t add_right_maximum(0);
1273 for (const auto& add_element : new_to_add) {
1274 // Technically not needed, but better to leave just in case
1275 add_element.reduction_check();
1276 add_right_final_sum += uint1024_t(add_element.get_value());
1277
1278 add_right_maximum += uint1024_t(add_element.get_maximum_value());
1279 }
1280 const size_t final_number_of_products = new_input_left.size();
1281
1282 // We need to check if it is possible to reduce the products enough
1283 worst_case_product_sum = uint1024_t(final_number_of_products) * uint1024_t(DEFAULT_MAXIMUM_REMAINDER) *
1284 uint1024_t(DEFAULT_MAXIMUM_REMAINDER);
1285
1286 // Check that we can actually reduce the products enough, this assert will probably never get triggered
1287 ASSERT((worst_case_product_sum + add_right_maximum) < get_maximum_crt_product());
1288
1289 // We've collapsed all constants, checked if we can compute the sum of products in the worst case, time to check if
1290 // we need to reduce something
1291 perform_reductions_for_mult_madd(new_input_left, new_input_right, new_to_add);
1292 uint1024_t sum_of_products_final(0);
1293 for (size_t i = 0; i < final_number_of_products; i++) {
1294 sum_of_products_final += uint1024_t(new_input_left[i].get_value()) * uint1024_t(new_input_right[i].get_value());
1295 }
1296
1297 // Get the number of range proof bits for the quotient
1298 const size_t num_quotient_bits = get_quotient_max_bits({ DEFAULT_MAXIMUM_REMAINDER });
1299
1300 // Compute the quotient and remainder
1301 const auto [quotient_1024, remainder_1024] = (sum_of_products_final + add_right_final_sum).divmod(modulus);
1302
1303 // If we are establishing an identity and the remainder has to be zero, we need to check, that it actually is
1304
1305 if (fix_remainder_to_zero) {
1306 // This is not the only check. Circuit check is coming later :)
1307 ASSERT(remainder_1024.lo == uint512_t(0));
1308 }
1309 const uint512_t quotient_value = quotient_1024.lo;
1310 const uint512_t remainder_value = remainder_1024.lo;
1311
1312 bigfield remainder;
1313 bigfield quotient;
1314 // Constrain quotient to mitigate CRT overflow attacks
1315 quotient = create_from_u512_as_witness(ctx, quotient_value, false, num_quotient_bits);
1316
1317 if (fix_remainder_to_zero) {
1318 remainder = zero();
1319 // remainder needs to be defined as wire value and not selector values to satisfy
1320 // UltraPlonk's bigfield custom gates
1321 remainder.convert_constant_to_fixed_witness(ctx);
1322 } else {
1323 remainder = create_from_u512_as_witness(ctx, remainder_value);
1324 }
1325
1326 unsafe_evaluate_multiple_multiply_add(new_input_left, new_input_right, new_to_add, quotient, { remainder });
1327
1328 return remainder;
1329}
1330
1336template <typename Builder, typename T>
1338 const bigfield& right_a,
1339 const bigfield& left_b,
1340 const bigfield& right_b,
1341 const std::vector<bigfield>& to_add)
1342{
1343 left_a.reduction_check();
1344 right_a.reduction_check();
1345 left_b.reduction_check();
1346 right_b.reduction_check();
1347
1348 std::vector<bigfield> mul_left = { left_a, left_b };
1349 std::vector<bigfield> mul_right = { right_a, right_b };
1350
1351 return mult_madd(mul_left, mul_right, to_add);
1352}
1353
1372template <typename Builder, typename T>
1373bigfield<Builder, T> bigfield<Builder, T>::msub_div(const std::vector<bigfield>& mul_left,
1374 const std::vector<bigfield>& mul_right,
1375 const bigfield& divisor,
1376 const std::vector<bigfield>& to_sub,
1377 bool enable_divisor_nz_check)
1378{
1379 Builder* ctx = divisor.context;
1380
1381 const size_t num_multiplications = mul_left.size();
1382 native product_native = 0;
1383 bool products_constant = true;
1384
1385 // Check the basics
1386 ASSERT(mul_left.size() == mul_right.size());
1387 ASSERT(divisor.get_value() != 0);
1388
1389 // This check is optional, because it is heavy and often we don't need it at all
1390 if (enable_divisor_nz_check) {
1391 divisor.assert_is_not_equal(zero());
1392 }
1393
1394 // Compute the sum of products
1395 for (size_t i = 0; i < num_multiplications; ++i) {
1396 const native mul_left_native(uint512_t(mul_left[i].get_value() % modulus_u512).lo);
1397 const native mul_right_native(uint512_t(mul_right[i].get_value() % modulus_u512).lo);
1398 product_native += (mul_left_native * -mul_right_native);
1399 products_constant = products_constant && mul_left[i].is_constant() && mul_right[i].is_constant();
1400 }
1401
1402 // Compute the sum of to_sub
1403 native sub_native(0);
1404 bool sub_constant = true;
1405 for (const auto& sub : to_sub) {
1406 sub_native += (uint512_t(sub.get_value() % modulus_u512).lo);
1407 sub_constant = sub_constant && sub.is_constant();
1408 }
1409
1410 native divisor_native(uint512_t(divisor.get_value() % modulus_u512).lo);
1411
1412 // Compute the result
1413 const native result_native = (product_native - sub_native) / divisor_native;
1414
1415 const uint1024_t result_value = uint1024_t(uint512_t(static_cast<uint256_t>(result_native)));
1416
1417 // If everything is constant, then we just return the constant
1418 if (sub_constant && products_constant && divisor.is_constant()) {
1419 return bigfield(ctx, uint256_t(result_value.lo.lo));
1420 }
1421
1422 // Create the result witness
1423 bigfield result = create_from_u512_as_witness(ctx, result_value.lo);
1424
1425 std::vector<bigfield> eval_left{ result };
1426 std::vector<bigfield> eval_right{ divisor };
1427 for (const auto& in : mul_left) {
1428 eval_left.emplace_back(in);
1429 }
1430 for (const auto& in : mul_right) {
1431 eval_right.emplace_back(in);
1432 }
1433
1434 mult_madd(eval_left, eval_right, to_sub, true);
1435 return result;
1436}
1437
1438template <typename Builder, typename T>
1440{
1441 Builder* ctx = context ? context : predicate.context;
1442
1443 if (is_constant() && predicate.is_constant()) {
1444 if (predicate.get_value()) {
1445 uint512_t out_val = (modulus_u512 - get_value()) % modulus_u512;
1446 return bigfield(ctx, out_val.lo);
1447 }
1448 return *this;
1449 }
1450 reduction_check();
1451
1452 uint256_t limb_0_maximum_value = binary_basis_limbs[0].maximum_value;
1453 uint64_t limb_0_borrow_shift = std::max(limb_0_maximum_value.get_msb() + 1, NUM_LIMB_BITS);
1454 uint256_t limb_1_maximum_value =
1455 binary_basis_limbs[1].maximum_value + (uint256_t(1) << (limb_0_borrow_shift - NUM_LIMB_BITS));
1456 uint64_t limb_1_borrow_shift = std::max(limb_1_maximum_value.get_msb() + 1, NUM_LIMB_BITS);
1457 uint256_t limb_2_maximum_value =
1458 binary_basis_limbs[2].maximum_value + (uint256_t(1) << (limb_1_borrow_shift - NUM_LIMB_BITS));
1459 uint64_t limb_2_borrow_shift = std::max(limb_2_maximum_value.get_msb() + 1, NUM_LIMB_BITS);
1460
1461 uint256_t limb_3_maximum_value =
1462 binary_basis_limbs[3].maximum_value + (uint256_t(1) << (limb_2_borrow_shift - NUM_LIMB_BITS));
1463
1464 // uint256_t comparison_maximum = uint256_t(modulus_u512.slice(NUM_LIMB_BITS * 3, NUM_LIMB_BITS * 4));
1465 // uint256_t additive_term = comparison_maximum;
1466 // TODO: This is terribly inefficient. We should change it.
1467 uint512_t constant_to_add = modulus_u512;
1468 while (constant_to_add.slice(NUM_LIMB_BITS * 3, NUM_LIMB_BITS * 4).lo <= limb_3_maximum_value) {
1469 constant_to_add += modulus_u512;
1470 }
1471
1472 uint256_t t0(uint256_t(1) << limb_0_borrow_shift);
1473 uint256_t t1((uint256_t(1) << limb_1_borrow_shift) - (uint256_t(1) << (limb_0_borrow_shift - NUM_LIMB_BITS)));
1474 uint256_t t2((uint256_t(1) << limb_2_borrow_shift) - (uint256_t(1) << (limb_1_borrow_shift - NUM_LIMB_BITS)));
1475 uint256_t t3(uint256_t(1) << (limb_2_borrow_shift - NUM_LIMB_BITS));
1476
1477 uint256_t to_add_0_u256 = uint256_t(constant_to_add.slice(0, NUM_LIMB_BITS));
1478 uint256_t to_add_1_u256 = uint256_t(constant_to_add.slice(NUM_LIMB_BITS, NUM_LIMB_BITS * 2));
1479 uint256_t to_add_2_u256 = uint256_t(constant_to_add.slice(NUM_LIMB_BITS * 2, NUM_LIMB_BITS * 3));
1480 uint256_t to_add_3_u256 = uint256_t(constant_to_add.slice(NUM_LIMB_BITS * 3, NUM_LIMB_BITS * 4));
1481
1482 barretenberg::fr to_add_0(t0 + to_add_0_u256);
1483 barretenberg::fr to_add_1(t1 + to_add_1_u256);
1484 barretenberg::fr to_add_2(t2 + to_add_2_u256);
1485 barretenberg::fr to_add_3(to_add_3_u256 - t3);
1486
1487 // we either return current value if predicate is false, or (limb_i - value) if predicate is true
1488 // (1 - predicate) * value + predicate * (limb_i - value)
1489 // = predicate * (limb_i - 2 * value) + value
1490 barretenberg::fr two(2);
1491
1492 field_t limb_0 = static_cast<field_t<Builder>>(predicate).madd(-(binary_basis_limbs[0].element * two) + to_add_0,
1493 binary_basis_limbs[0].element);
1494 field_t limb_1 = static_cast<field_t<Builder>>(predicate).madd(-(binary_basis_limbs[1].element * two) + to_add_1,
1495 binary_basis_limbs[1].element);
1496 field_t limb_2 = static_cast<field_t<Builder>>(predicate).madd(-(binary_basis_limbs[2].element * two) + to_add_2,
1497 binary_basis_limbs[2].element);
1498 field_t limb_3 = static_cast<field_t<Builder>>(predicate).madd(-(binary_basis_limbs[3].element * two) + to_add_3,
1499 binary_basis_limbs[3].element);
1500
1501 uint256_t max_limb_0 = binary_basis_limbs[0].maximum_value + to_add_0_u256 + t0;
1502 uint256_t max_limb_1 = binary_basis_limbs[1].maximum_value + to_add_1_u256 + t1;
1503 uint256_t max_limb_2 = binary_basis_limbs[2].maximum_value + to_add_2_u256 + t2;
1504 uint256_t max_limb_3 = binary_basis_limbs[3].maximum_value + to_add_3_u256 - t3;
1505
1506 bigfield result(ctx);
1507 result.binary_basis_limbs[0] = Limb(limb_0, max_limb_0);
1508 result.binary_basis_limbs[1] = Limb(limb_1, max_limb_1);
1509 result.binary_basis_limbs[2] = Limb(limb_2, max_limb_2);
1510 result.binary_basis_limbs[3] = Limb(limb_3, max_limb_3);
1511
1512 uint512_t constant_to_add_mod_p = constant_to_add % prime_basis.modulus;
1513 field_t prime_basis_to_add(ctx, barretenberg::fr(constant_to_add_mod_p.lo));
1514 result.prime_basis_limb =
1515 static_cast<field_t<Builder>>(predicate).madd(-(prime_basis_limb * two) + prime_basis_to_add, prime_basis_limb);
1516
1517 return result;
1518}
1519
1529template <typename Builder, typename T>
1531 const bool_t<Builder>& predicate) const
1532{
1533 if (is_constant() && other.is_constant() && predicate.is_constant()) {
1534 if (predicate.get_value()) {
1535 return other;
1536 }
1537 return *this;
1538 }
1539 Builder* ctx = context ? context : (other.context ? other.context : predicate.context);
1540
1541 // TODO: use field_t::conditional_assign method
1542 field_t binary_limb_0 = static_cast<field_t<Builder>>(predicate).madd(
1543 other.binary_basis_limbs[0].element - binary_basis_limbs[0].element, binary_basis_limbs[0].element);
1544 field_t binary_limb_1 = static_cast<field_t<Builder>>(predicate).madd(
1545 other.binary_basis_limbs[1].element - binary_basis_limbs[1].element, binary_basis_limbs[1].element);
1546 field_t binary_limb_2 = static_cast<field_t<Builder>>(predicate).madd(
1547 other.binary_basis_limbs[2].element - binary_basis_limbs[2].element, binary_basis_limbs[2].element);
1548 field_t binary_limb_3 = static_cast<field_t<Builder>>(predicate).madd(
1549 other.binary_basis_limbs[3].element - binary_basis_limbs[3].element, binary_basis_limbs[3].element);
1550 field_t prime_limb =
1551 static_cast<field_t<Builder>>(predicate).madd(other.prime_basis_limb - prime_basis_limb, prime_basis_limb);
1552
1553 bigfield result(ctx);
1554 // the maximum of the maximal values of elements is large enough
1555 result.binary_basis_limbs[0] =
1556 Limb(binary_limb_0, std::max(binary_basis_limbs[0].maximum_value, other.binary_basis_limbs[0].maximum_value));
1557 result.binary_basis_limbs[1] =
1558 Limb(binary_limb_1, std::max(binary_basis_limbs[1].maximum_value, other.binary_basis_limbs[1].maximum_value));
1559 result.binary_basis_limbs[2] =
1560 Limb(binary_limb_2, std::max(binary_basis_limbs[2].maximum_value, other.binary_basis_limbs[2].maximum_value));
1561 result.binary_basis_limbs[3] =
1562 Limb(binary_limb_3, std::max(binary_basis_limbs[3].maximum_value, other.binary_basis_limbs[3].maximum_value));
1563 result.prime_basis_limb = prime_limb;
1564 return result;
1565}
1566
1581template <typename Builder, typename T> void bigfield<Builder, T>::reduction_check(const size_t num_products) const
1582{
1583
1584 if (is_constant()) { // this seems not a reduction check, but actually computing the reduction
1585 // TODO THIS IS UGLY WHY CAN'T WE JUST DO (*THIS) = REDUCED?
1586 uint256_t reduced_value = (get_value() % modulus_u512).lo;
1587 bigfield reduced(context, uint256_t(reduced_value));
1588 binary_basis_limbs[0] = reduced.binary_basis_limbs[0];
1589 binary_basis_limbs[1] = reduced.binary_basis_limbs[1];
1590 binary_basis_limbs[2] = reduced.binary_basis_limbs[2];
1591 binary_basis_limbs[3] = reduced.binary_basis_limbs[3];
1592 prime_basis_limb = reduced.prime_basis_limb;
1593 return;
1594 }
1595
1596 uint256_t maximum_limb_value = get_maximum_unreduced_limb_value();
1597 bool limb_overflow_test_0 = binary_basis_limbs[0].maximum_value > maximum_limb_value;
1598 bool limb_overflow_test_1 = binary_basis_limbs[1].maximum_value > maximum_limb_value;
1599 bool limb_overflow_test_2 = binary_basis_limbs[2].maximum_value > maximum_limb_value;
1600 bool limb_overflow_test_3 = binary_basis_limbs[3].maximum_value > maximum_limb_value;
1601 if (get_maximum_value() > get_maximum_unreduced_value(num_products) || limb_overflow_test_0 ||
1602 limb_overflow_test_1 || limb_overflow_test_2 || limb_overflow_test_3) {
1603 self_reduce();
1604 }
1605}
1606
1607// create a version with mod 2^t element part in [0,p-1]
1608// After reducing to size 2^s, we check (p-1)-a is non-negative as integer.
1609// We perform subtraction using carries on blocks of size 2^b. The operations inside the blocks are done mod r
1610// Including the effect of carries the operation inside each limb is in the range [-2^b-1,2^{b+1}]
1611// Assuming this values are all distinct mod r, which happens e.g. if r/2>2^{b+1}, then if all limb values are
1612// non-negative at the end of subtraction, we know the subtraction result is positive as integers and a<p
1613template <typename Builder, typename T> void bigfield<Builder, T>::assert_is_in_field() const
1614{
1615 // Warning: this assumes we have run circuit construction at least once in debug mode where large non reduced
1616 // constants are allowed via ASSERT
1617 if (is_constant()) {
1618 return;
1619 }
1620
1621 self_reduce(); // this method in particular enforces limb vals are <2^b - needed for logic described above
1622 uint256_t value = get_value().lo;
1623 // TODO:make formal assert that modulus<=256 bits
1624 constexpr uint256_t modulus_minus_one = modulus_u512.lo - 1;
1625
1626 constexpr uint256_t modulus_minus_one_0 = modulus_minus_one.slice(0, NUM_LIMB_BITS);
1627 constexpr uint256_t modulus_minus_one_1 = modulus_minus_one.slice(NUM_LIMB_BITS, NUM_LIMB_BITS * 2);
1628 constexpr uint256_t modulus_minus_one_2 = modulus_minus_one.slice(NUM_LIMB_BITS * 2, NUM_LIMB_BITS * 3);
1629 constexpr uint256_t modulus_minus_one_3 = modulus_minus_one.slice(NUM_LIMB_BITS * 3, NUM_LIMB_BITS * 4);
1630
1631 bool borrow_0_value = value.slice(0, NUM_LIMB_BITS) > modulus_minus_one_0;
1632 bool borrow_1_value =
1633 (value.slice(NUM_LIMB_BITS, NUM_LIMB_BITS * 2) + uint256_t(borrow_0_value)) > (modulus_minus_one_1);
1634 bool borrow_2_value =
1635 (value.slice(NUM_LIMB_BITS * 2, NUM_LIMB_BITS * 3) + uint256_t(borrow_1_value)) > (modulus_minus_one_2);
1636
1637 field_t<Builder> modulus_0(context, modulus_minus_one_0);
1638 field_t<Builder> modulus_1(context, modulus_minus_one_1);
1639 field_t<Builder> modulus_2(context, modulus_minus_one_2);
1640 field_t<Builder> modulus_3(context, modulus_minus_one_3);
1641 bool_t<Builder> borrow_0(witness_t<Builder>(context, borrow_0_value));
1642 bool_t<Builder> borrow_1(witness_t<Builder>(context, borrow_1_value));
1643 bool_t<Builder> borrow_2(witness_t<Builder>(context, borrow_2_value));
1644 // The way we use borrows here ensures that we are checking that modulus - binary_basis > 0.
1645 // We check that the result in each limb is > 0.
1646 // If the modulus part in this limb is smaller, we simply borrow the value from the higher limb.
1647 // The prover can rearrange the borrows the way they like. The important thing is that the borrows are
1648 // constrained.
1649 field_t<Builder> r0 = modulus_0 - binary_basis_limbs[0].element + static_cast<field_t<Builder>>(borrow_0) * shift_1;
1650 field_t<Builder> r1 = modulus_1 - binary_basis_limbs[1].element +
1651 static_cast<field_t<Builder>>(borrow_1) * shift_1 - static_cast<field_t<Builder>>(borrow_0);
1652 field_t<Builder> r2 = modulus_2 - binary_basis_limbs[2].element +
1653 static_cast<field_t<Builder>>(borrow_2) * shift_1 - static_cast<field_t<Builder>>(borrow_1);
1654 field_t<Builder> r3 = modulus_3 - binary_basis_limbs[3].element - static_cast<field_t<Builder>>(borrow_2);
1655 r0 = r0.normalize();
1656 r1 = r1.normalize();
1657 r2 = r2.normalize();
1658 r3 = r3.normalize();
1659 if constexpr (HasPlookup<Builder>) {
1660 context->decompose_into_default_range(r0.witness_index, static_cast<size_t>(NUM_LIMB_BITS));
1661 context->decompose_into_default_range(r1.witness_index, static_cast<size_t>(NUM_LIMB_BITS));
1662 context->decompose_into_default_range(r2.witness_index, static_cast<size_t>(NUM_LIMB_BITS));
1663 context->decompose_into_default_range(r3.witness_index, static_cast<size_t>(NUM_LIMB_BITS));
1664 } else {
1665 context->decompose_into_base4_accumulators(
1666 r0.witness_index, static_cast<size_t>(NUM_LIMB_BITS), "bigfield: assert_is_in_field range constraint 1.");
1667 context->decompose_into_base4_accumulators(
1668 r1.witness_index, static_cast<size_t>(NUM_LIMB_BITS), "bigfield: assert_is_in_field range constraint 2.");
1669 context->decompose_into_base4_accumulators(
1670 r2.witness_index, static_cast<size_t>(NUM_LIMB_BITS), "bigfield: assert_is_in_field range constraint 3.");
1671 context->decompose_into_base4_accumulators(
1672 r3.witness_index, static_cast<size_t>(NUM_LIMB_BITS), "bigfield: assert_is_in_field range constraint 4.");
1673 }
1674}
1675
1676template <typename Builder, typename T> void bigfield<Builder, T>::assert_less_than(const uint256_t upper_limit) const
1677{
1678 // TODO(kesha): Merge this with assert_is_in_field
1679 // Warning: this assumes we have run circuit construction at least once in debug mode where large non reduced
1680 // constants are allowed via ASSERT
1681 if (is_constant()) {
1682 return;
1683 }
1684 ASSERT(upper_limit != 0);
1685 // The circuit checks that limit - this >= 0, so if we are doing a less_than comparison, we need to subtract 1 from
1686 // the limit
1687 uint256_t strict_upper_limit = upper_limit - uint256_t(1);
1688 self_reduce(); // this method in particular enforces limb vals are <2^b - needed for logic described above
1689 uint256_t value = get_value().lo;
1690
1691 const uint256_t upper_limit_value_0 = strict_upper_limit.slice(0, NUM_LIMB_BITS);
1692 const uint256_t upper_limit_value_1 = strict_upper_limit.slice(NUM_LIMB_BITS, NUM_LIMB_BITS * 2);
1693 const uint256_t upper_limit_value_2 = strict_upper_limit.slice(NUM_LIMB_BITS * 2, NUM_LIMB_BITS * 3);
1694 const uint256_t upper_limit_value_3 = strict_upper_limit.slice(NUM_LIMB_BITS * 3, NUM_LIMB_BITS * 4);
1695
1696 bool borrow_0_value = value.slice(0, NUM_LIMB_BITS) > upper_limit_value_0;
1697 bool borrow_1_value =
1698 (value.slice(NUM_LIMB_BITS, NUM_LIMB_BITS * 2) + uint256_t(borrow_0_value)) > (upper_limit_value_1);
1699 bool borrow_2_value =
1700 (value.slice(NUM_LIMB_BITS * 2, NUM_LIMB_BITS * 3) + uint256_t(borrow_1_value)) > (upper_limit_value_2);
1701
1702 field_t<Builder> upper_limit_0(context, upper_limit_value_0);
1703 field_t<Builder> upper_limit_1(context, upper_limit_value_1);
1704 field_t<Builder> upper_limit_2(context, upper_limit_value_2);
1705 field_t<Builder> upper_limit_3(context, upper_limit_value_3);
1706 bool_t<Builder> borrow_0(witness_t<Builder>(context, borrow_0_value));
1707 bool_t<Builder> borrow_1(witness_t<Builder>(context, borrow_1_value));
1708 bool_t<Builder> borrow_2(witness_t<Builder>(context, borrow_2_value));
1709 // The way we use borrows here ensures that we are checking that upper_limit - binary_basis > 0.
1710 // We check that the result in each limb is > 0.
1711 // If the modulus part in this limb is smaller, we simply borrow the value from the higher limb.
1712 // The prover can rearrange the borrows the way they like. The important thing is that the borrows are
1713 // constrained.
1714 field_t<Builder> r0 =
1715 upper_limit_0 - binary_basis_limbs[0].element + static_cast<field_t<Builder>>(borrow_0) * shift_1;
1716 field_t<Builder> r1 = upper_limit_1 - binary_basis_limbs[1].element +
1717 static_cast<field_t<Builder>>(borrow_1) * shift_1 - static_cast<field_t<Builder>>(borrow_0);
1718 field_t<Builder> r2 = upper_limit_2 - binary_basis_limbs[2].element +
1719 static_cast<field_t<Builder>>(borrow_2) * shift_1 - static_cast<field_t<Builder>>(borrow_1);
1720 field_t<Builder> r3 = upper_limit_3 - binary_basis_limbs[3].element - static_cast<field_t<Builder>>(borrow_2);
1721 r0 = r0.normalize();
1722 r1 = r1.normalize();
1723 r2 = r2.normalize();
1724 r3 = r3.normalize();
1725 if constexpr (Builder::CIRCUIT_TYPE == CircuitType::ULTRA) {
1726 context->decompose_into_default_range(r0.witness_index, static_cast<size_t>(NUM_LIMB_BITS));
1727 context->decompose_into_default_range(r1.witness_index, static_cast<size_t>(NUM_LIMB_BITS));
1728 context->decompose_into_default_range(r2.witness_index, static_cast<size_t>(NUM_LIMB_BITS));
1729 context->decompose_into_default_range(r3.witness_index, static_cast<size_t>(NUM_LIMB_BITS));
1730 } else {
1731 context->decompose_into_base4_accumulators(
1732 r0.witness_index, static_cast<size_t>(NUM_LIMB_BITS), "bigfield: assert_less_than range constraint 1.");
1733 context->decompose_into_base4_accumulators(
1734 r1.witness_index, static_cast<size_t>(NUM_LIMB_BITS), "bigfield: assert_less_than range constraint 2.");
1735 context->decompose_into_base4_accumulators(
1736 r2.witness_index, static_cast<size_t>(NUM_LIMB_BITS), "bigfield: assert_less_than range constraint 3.");
1737 context->decompose_into_base4_accumulators(
1738 r3.witness_index, static_cast<size_t>(NUM_LIMB_BITS), "bigfield: assert_less_than range constraint 4.");
1739 }
1740}
1741
1742// check elements are equal mod p by proving their integer difference is a multiple of p.
1743// This relies on the minus operator for a-b increasing a by a multiple of p large enough so diff is non-negative
1744template <typename Builder, typename T> void bigfield<Builder, T>::assert_equal(const bigfield& other) const
1745{
1746 Builder* ctx = this->context ? this->context : other.context;
1747
1748 if (is_constant() && other.is_constant()) {
1749 std::cerr << "bigfield: calling assert equal on 2 CONSTANT bigfield elements...is this intended?" << std::endl;
1750 return;
1751 } else if (other.is_constant()) {
1752 // evaluate a strict equality - make sure *this is reduced first, or an honest prover
1753 // might not be able to satisfy these constraints.
1754 field_t<Builder> t0 = (binary_basis_limbs[0].element - other.binary_basis_limbs[0].element);
1755 field_t<Builder> t1 = (binary_basis_limbs[1].element - other.binary_basis_limbs[1].element);
1756 field_t<Builder> t2 = (binary_basis_limbs[2].element - other.binary_basis_limbs[2].element);
1757 field_t<Builder> t3 = (binary_basis_limbs[3].element - other.binary_basis_limbs[3].element);
1758 field_t<Builder> t4 = (prime_basis_limb - other.prime_basis_limb);
1759 t0.assert_is_zero();
1760 t1.assert_is_zero();
1761 t2.assert_is_zero();
1762 t3.assert_is_zero();
1763 t4.assert_is_zero();
1764 return;
1765 } else if (is_constant()) {
1766 other.assert_equal(*this);
1767 return;
1768 }
1769
1770 bigfield diff = *this - other;
1771 const uint512_t diff_val = diff.get_value();
1772 const uint512_t modulus(target_basis.modulus);
1773
1774 const auto [quotient_512, remainder_512] = (diff_val).divmod(modulus);
1775 if (remainder_512 != 0)
1776 std::cerr << "bigfield: remainder not zero!" << std::endl;
1777 ASSERT(remainder_512 == 0);
1778 bigfield quotient;
1779
1780 const size_t num_quotient_bits = get_quotient_max_bits({ 0 });
1781 quotient = bigfield(witness_t(ctx, fr(quotient_512.slice(0, NUM_LIMB_BITS * 2).lo)),
1782 witness_t(ctx, fr(quotient_512.slice(NUM_LIMB_BITS * 2, NUM_LIMB_BITS * 4).lo)),
1783 false,
1784 num_quotient_bits);
1785 unsafe_evaluate_multiply_add(diff, { one() }, {}, quotient, { zero() });
1786}
1787
1788// construct a proof that points are different mod p, when they are different mod r
1789// WARNING: This method doesn't have perfect completeness - for points equal mod r (or with certain difference kp
1790// mod r) but different mod p, you can't construct a proof. The chances of an honest prover running afoul of this
1791// condition are extremely small (TODO: compute probability) Note also that the number of constraints depends on how
1792// much the values have overflown beyond p e.g. due to an addition chain The function is based on the following.
1793// Suppose a-b = 0 mod p. Then a-b = k*p for k in a range [-R,L] such that L*p>= a, R*p>=b. And also a-b = k*p mod r
1794// for such k. Thus we can verify a-b is non-zero mod p by taking the product of such values (a-b-kp) and showing
1795// it's non-zero mod r
1796template <typename Builder, typename T> void bigfield<Builder, T>::assert_is_not_equal(const bigfield& other) const
1797{
1798 // Why would we use this for 2 constants? Turns out, in biggroup
1799 const auto get_overload_count = [target_modulus = modulus_u512](const uint512_t& maximum_value) {
1800 uint512_t target = target_modulus;
1801 size_t overload_count = 0;
1802 while (target < maximum_value) {
1803 ++overload_count;
1804 target += target_modulus;
1805 }
1806 return overload_count;
1807 };
1808 const size_t lhs_overload_count = get_overload_count(get_maximum_value());
1809 const size_t rhs_overload_count = get_overload_count(other.get_maximum_value());
1810
1811 // if (a == b) then (a == b mod n)
1812 // to save gates, we only check that (a == b mod n)
1813
1814 // if numeric val of a = a' + p.q
1815 // we want to check (a' + p.q == b mod n)
1816 const field_t<Builder> base_diff = prime_basis_limb - other.prime_basis_limb;
1817 auto diff = base_diff;
1818 field_t<Builder> prime_basis(get_context(), modulus);
1819 field_t<Builder> prime_basis_accumulator = prime_basis;
1820 // Each loop iteration adds 1 gate
1821 // (prime_basis and prime_basis accumulator are constant so only the * operator adds a gate)
1822 for (size_t i = 0; i < lhs_overload_count; ++i) {
1823 diff = diff * (base_diff - prime_basis_accumulator);
1824 prime_basis_accumulator += prime_basis;
1825 }
1826 prime_basis_accumulator = prime_basis;
1827 for (size_t i = 0; i < rhs_overload_count; ++i) {
1828 diff = diff * (base_diff + prime_basis_accumulator);
1829 prime_basis_accumulator += prime_basis;
1830 }
1831 diff.assert_is_not_zero();
1832}
1833
1834// We reduce an element's mod 2^t representation (t=4*NUM_LIMB_BITS) to size 2^s for smallest s with 2^s>p
1835// This is much cheaper than actually reducing mod p and suffices for addition chains (where we just need not to
1836// overflow 2^t) We also reduce any "spillage" inside the first 3 limbs, so that their range is NUM_LIMB_BITS and
1837// not larger
1838template <typename Builder, typename T> void bigfield<Builder, T>::self_reduce() const
1839{
1840 // Warning: this assumes we have run circuit construction at least once in debug mode where large non reduced
1841 // constants are disallowed via ASSERT
1842 if (is_constant()) {
1843 return;
1844 }
1845 // TODO: handle situation where some limbs are constant and others are not constant
1846 const auto [quotient_value, remainder_value] = get_value().divmod(target_basis.modulus);
1847
1848 bigfield quotient(context);
1849
1850 uint512_t maximum_quotient_size = get_maximum_value() / target_basis.modulus;
1851 uint64_t maximum_quotient_bits = maximum_quotient_size.get_msb() + 1;
1852 if ((maximum_quotient_bits & 1ULL) == 1ULL) {
1853 ++maximum_quotient_bits;
1854 }
1855 // TODO: implicit assumption here - NUM_LIMB_BITS large enough for all the quotient
1856 uint32_t quotient_limb_index = context->add_variable(barretenberg::fr(quotient_value.lo));
1857 field_t<Builder> quotient_limb = field_t<Builder>::from_witness_index(context, quotient_limb_index);
1858 if constexpr (HasPlookup<Builder>) {
1859 context->decompose_into_default_range(quotient_limb.witness_index, static_cast<size_t>(maximum_quotient_bits));
1860 } else {
1861 context->decompose_into_base4_accumulators(quotient_limb.witness_index,
1862 static_cast<size_t>(maximum_quotient_bits),
1863 "bigfield: quotient_limb too large.");
1864 }
1865
1866 ASSERT((uint1024_t(1) << maximum_quotient_bits) * uint1024_t(modulus_u512) + DEFAULT_MAXIMUM_REMAINDER <
1867 get_maximum_crt_product());
1868 quotient.binary_basis_limbs[0] = Limb(quotient_limb, uint256_t(1) << maximum_quotient_bits);
1869 quotient.binary_basis_limbs[1] = Limb(field_t<Builder>::from_witness_index(context, context->zero_idx), 0);
1870 quotient.binary_basis_limbs[2] = Limb(field_t<Builder>::from_witness_index(context, context->zero_idx), 0);
1871 quotient.binary_basis_limbs[3] = Limb(field_t<Builder>::from_witness_index(context, context->zero_idx), 0);
1872 quotient.prime_basis_limb = quotient_limb;
1873 // this constructor with can_overflow=false will enforce remainder of size<2^s
1874 bigfield remainder = bigfield(
1875 witness_t(context, fr(remainder_value.slice(0, NUM_LIMB_BITS * 2).lo)),
1876 witness_t(context, fr(remainder_value.slice(NUM_LIMB_BITS * 2, NUM_LIMB_BITS * 3 + NUM_LAST_LIMB_BITS).lo)));
1877
1878 unsafe_evaluate_multiply_add(*this, one(), {}, quotient, { remainder });
1879 binary_basis_limbs[0] =
1880 remainder.binary_basis_limbs[0]; // Combination of const method and mutable variables is good practice?
1881 binary_basis_limbs[1] = remainder.binary_basis_limbs[1];
1882 binary_basis_limbs[2] = remainder.binary_basis_limbs[2];
1883 binary_basis_limbs[3] = remainder.binary_basis_limbs[3];
1884 prime_basis_limb = remainder.prime_basis_limb;
1885} // namespace stdlib
1886
1899template <typename Builder, typename T>
1900void bigfield<Builder, T>::unsafe_evaluate_multiply_add(const bigfield& input_left,
1901 const bigfield& input_to_mul,
1902 const std::vector<bigfield>& to_add,
1903 const bigfield& input_quotient,
1904 const std::vector<bigfield>& input_remainders)
1905{
1906
1907 std::vector<bigfield> remainders(input_remainders);
1908 bigfield left = input_left;
1909 bigfield to_mul = input_to_mul;
1910 bigfield quotient = input_quotient;
1911
1912 Builder* ctx = left.context ? left.context : to_mul.context;
1913
1914 uint512_t max_b0 = (left.binary_basis_limbs[1].maximum_value * to_mul.binary_basis_limbs[0].maximum_value);
1915 max_b0 += (neg_modulus_limbs_u256[1] * quotient.binary_basis_limbs[0].maximum_value);
1916 uint512_t max_b1 = (left.binary_basis_limbs[0].maximum_value * to_mul.binary_basis_limbs[1].maximum_value);
1917 max_b1 += (neg_modulus_limbs_u256[0] * quotient.binary_basis_limbs[1].maximum_value);
1918 uint512_t max_c0 = (left.binary_basis_limbs[1].maximum_value * to_mul.binary_basis_limbs[1].maximum_value);
1919 max_c0 += (neg_modulus_limbs_u256[1] * quotient.binary_basis_limbs[1].maximum_value);
1920 uint512_t max_c1 = (left.binary_basis_limbs[2].maximum_value * to_mul.binary_basis_limbs[0].maximum_value);
1921 max_c1 += (neg_modulus_limbs_u256[2] * quotient.binary_basis_limbs[0].maximum_value);
1922 uint512_t max_c2 = (left.binary_basis_limbs[0].maximum_value * to_mul.binary_basis_limbs[2].maximum_value);
1923 max_c2 += (neg_modulus_limbs_u256[0] * quotient.binary_basis_limbs[2].maximum_value);
1924 uint512_t max_d0 = (left.binary_basis_limbs[3].maximum_value * to_mul.binary_basis_limbs[0].maximum_value);
1925 max_d0 += (neg_modulus_limbs_u256[3] * quotient.binary_basis_limbs[0].maximum_value);
1926 uint512_t max_d1 = (left.binary_basis_limbs[2].maximum_value * to_mul.binary_basis_limbs[1].maximum_value);
1927 max_d1 += (neg_modulus_limbs_u256[2] * quotient.binary_basis_limbs[1].maximum_value);
1928 uint512_t max_d2 = (left.binary_basis_limbs[1].maximum_value * to_mul.binary_basis_limbs[2].maximum_value);
1929 max_d2 += (neg_modulus_limbs_u256[1] * quotient.binary_basis_limbs[2].maximum_value);
1930 uint512_t max_d3 = (left.binary_basis_limbs[0].maximum_value * to_mul.binary_basis_limbs[3].maximum_value);
1931 max_d3 += (neg_modulus_limbs_u256[0] * quotient.binary_basis_limbs[3].maximum_value);
1932
1933 uint512_t max_r0 = left.binary_basis_limbs[0].maximum_value * to_mul.binary_basis_limbs[0].maximum_value;
1934 max_r0 += (neg_modulus_limbs_u256[0] * quotient.binary_basis_limbs[0].maximum_value);
1935
1936 const uint512_t max_r1 = max_b0 + max_b1;
1937 const uint512_t max_r2 = max_c0 + max_c1 + max_c2;
1938 const uint512_t max_r3 = max_d0 + max_d1 + max_d2 + max_d3;
1939
1940 uint512_t max_a0(0);
1941 uint512_t max_a1(0);
1942 for (size_t i = 0; i < to_add.size(); ++i) {
1943 max_a0 += to_add[i].binary_basis_limbs[0].maximum_value +
1944 (to_add[i].binary_basis_limbs[1].maximum_value << NUM_LIMB_BITS);
1945 max_a1 += to_add[i].binary_basis_limbs[2].maximum_value +
1946 (to_add[i].binary_basis_limbs[3].maximum_value << NUM_LIMB_BITS);
1947 }
1948 const uint512_t max_lo = max_r0 + (max_r1 << NUM_LIMB_BITS) + max_a0;
1949 const uint512_t max_hi = max_r2 + (max_r3 << NUM_LIMB_BITS) + max_a1;
1950
1951 uint64_t max_lo_bits = (max_lo.get_msb() + 1);
1952 uint64_t max_hi_bits = max_hi.get_msb() + 1;
1953 if ((max_lo_bits & 1ULL) == 1ULL) {
1954 ++max_lo_bits;
1955 }
1956 if ((max_hi_bits & 1ULL) == 1ULL) {
1957 ++max_hi_bits;
1958 }
1959
1960 if constexpr (HasPlookup<Builder>) {
1961 // The plookup custom bigfield gate requires inputs are witnesses.
1962 // If we're using constant values, instantiate them as circuit variables
1963 const auto convert_constant_to_fixed_witness = [ctx](const bigfield& input) {
1964 bigfield output(input);
1965 output.prime_basis_limb = field_t<Builder>::from_witness_index(
1966 ctx, ctx->put_constant_variable(input.prime_basis_limb.get_value()));
1967 output.binary_basis_limbs[0].element = field_t<Builder>::from_witness_index(
1968 ctx, ctx->put_constant_variable(input.binary_basis_limbs[0].element.get_value()));
1969 output.binary_basis_limbs[1].element = field_t<Builder>::from_witness_index(
1970 ctx, ctx->put_constant_variable(input.binary_basis_limbs[1].element.get_value()));
1971 output.binary_basis_limbs[2].element = field_t<Builder>::from_witness_index(
1972 ctx, ctx->put_constant_variable(input.binary_basis_limbs[2].element.get_value()));
1973 output.binary_basis_limbs[3].element = field_t<Builder>::from_witness_index(
1974 ctx, ctx->put_constant_variable(input.binary_basis_limbs[3].element.get_value()));
1975 output.context = ctx;
1976 return output;
1977 };
1978 if (left.is_constant()) {
1979 left = convert_constant_to_fixed_witness(left);
1980 }
1981 if (to_mul.is_constant()) {
1982 to_mul = convert_constant_to_fixed_witness(to_mul);
1983 }
1984 if (quotient.is_constant()) {
1985 quotient = convert_constant_to_fixed_witness(quotient);
1986 }
1987 if (remainders[0].is_constant()) {
1988 remainders[0] = convert_constant_to_fixed_witness(remainders[0]);
1989 }
1990
1991 std::vector<field_t<Builder>> limb_0_accumulator{ remainders[0].binary_basis_limbs[0].element };
1992 std::vector<field_t<Builder>> limb_2_accumulator{ remainders[0].binary_basis_limbs[2].element };
1993 std::vector<field_t<Builder>> prime_limb_accumulator{ remainders[0].prime_basis_limb };
1994 for (size_t i = 1; i < remainders.size(); ++i) {
1995 limb_0_accumulator.emplace_back(remainders[i].binary_basis_limbs[0].element);
1996 limb_0_accumulator.emplace_back(remainders[i].binary_basis_limbs[1].element * shift_1);
1997 limb_2_accumulator.emplace_back(remainders[i].binary_basis_limbs[2].element);
1998 limb_2_accumulator.emplace_back(remainders[i].binary_basis_limbs[3].element * shift_1);
1999 prime_limb_accumulator.emplace_back(remainders[i].prime_basis_limb);
2000 }
2001 for (const auto& add : to_add) {
2002 limb_0_accumulator.emplace_back(-add.binary_basis_limbs[0].element);
2003 limb_0_accumulator.emplace_back(-add.binary_basis_limbs[1].element * shift_1);
2004 limb_2_accumulator.emplace_back(-add.binary_basis_limbs[2].element);
2005 limb_2_accumulator.emplace_back(-add.binary_basis_limbs[3].element * shift_1);
2006 prime_limb_accumulator.emplace_back(-add.prime_basis_limb);
2007 }
2008
2009 const auto& t0 = remainders[0].binary_basis_limbs[1].element;
2010 const auto& t1 = remainders[0].binary_basis_limbs[3].element;
2011 bool needs_normalize = (t0.additive_constant != 0 || t0.multiplicative_constant != 1);
2012 needs_normalize = needs_normalize || (t1.additive_constant != 0 || t1.multiplicative_constant != 1);
2013
2014 if (needs_normalize) {
2015 limb_0_accumulator.emplace_back(remainders[0].binary_basis_limbs[1].element * shift_1);
2016 limb_2_accumulator.emplace_back(remainders[0].binary_basis_limbs[3].element * shift_1);
2017 }
2018
2019 field_t<Builder> remainder_limbs[4]{
2020 field_t<Builder>::accumulate(limb_0_accumulator),
2021 needs_normalize ? field_t<Builder>::from_witness_index(ctx, ctx->zero_idx)
2022 : remainders[0].binary_basis_limbs[1].element,
2023 field_t<Builder>::accumulate(limb_2_accumulator),
2024 needs_normalize ? field_t<Builder>::from_witness_index(ctx, ctx->zero_idx)
2025 : remainders[0].binary_basis_limbs[3].element,
2026 };
2027 field_t<Builder> remainder_prime_limb = field_t<Builder>::accumulate(prime_limb_accumulator);
2028
2030 {
2031 left.binary_basis_limbs[0].element.normalize().witness_index,
2032 left.binary_basis_limbs[1].element.normalize().witness_index,
2033 left.binary_basis_limbs[2].element.normalize().witness_index,
2034 left.binary_basis_limbs[3].element.normalize().witness_index,
2035 left.prime_basis_limb.witness_index,
2036 },
2037 {
2038 to_mul.binary_basis_limbs[0].element.normalize().witness_index,
2039 to_mul.binary_basis_limbs[1].element.normalize().witness_index,
2040 to_mul.binary_basis_limbs[2].element.normalize().witness_index,
2041 to_mul.binary_basis_limbs[3].element.normalize().witness_index,
2042 to_mul.prime_basis_limb.witness_index,
2043 },
2044 {
2045 quotient.binary_basis_limbs[0].element.normalize().witness_index,
2046 quotient.binary_basis_limbs[1].element.normalize().witness_index,
2047 quotient.binary_basis_limbs[2].element.normalize().witness_index,
2048 quotient.binary_basis_limbs[3].element.normalize().witness_index,
2049 quotient.prime_basis_limb.witness_index,
2050 },
2051 {
2052 remainder_limbs[0].normalize().witness_index,
2053 remainder_limbs[1].normalize().witness_index,
2054 remainder_limbs[2].normalize().witness_index,
2055 remainder_limbs[3].normalize().witness_index,
2056 remainder_prime_limb.witness_index,
2057 },
2058 { neg_modulus_limbs[0], neg_modulus_limbs[1], neg_modulus_limbs[2], neg_modulus_limbs[3] },
2059 modulus,
2060 };
2061 // N.B. this method also evaluates the prime field component of the non-native field mul
2062 const auto [lo_idx, hi_idx] = ctx->evaluate_non_native_field_multiplication(witnesses, false);
2063
2064 barretenberg::fr neg_prime = -barretenberg::fr(uint256_t(target_basis.modulus));
2066 to_mul.prime_basis_limb,
2067 quotient.prime_basis_limb * neg_prime,
2068 -remainder_prime_limb);
2069
2072 const uint64_t carry_lo_msb = max_lo_bits - (2 * NUM_LIMB_BITS);
2073 const uint64_t carry_hi_msb = max_hi_bits - (2 * NUM_LIMB_BITS);
2074
2075 // if both the hi and lo output limbs have less than 70 bits, we can use our custom
2076 // limb accumulation gate (accumulates 2 field elements, each composed of 5 14-bit limbs, in 3 gates)
2077 if (carry_lo_msb <= 70 && carry_hi_msb <= 70) {
2078 ctx->range_constrain_two_limbs(
2079 hi.witness_index, lo.witness_index, size_t(carry_lo_msb), size_t(carry_hi_msb));
2080 } else {
2081 ctx->decompose_into_default_range(hi.normalize().witness_index, carry_hi_msb);
2082 ctx->decompose_into_default_range(lo.normalize().witness_index, carry_lo_msb);
2083 }
2084 } else {
2085 const field_t b0 = left.binary_basis_limbs[1].element.madd(
2086 to_mul.binary_basis_limbs[0].element, quotient.binary_basis_limbs[1].element * neg_modulus_limbs[0]);
2087 const field_t b1 = left.binary_basis_limbs[0].element.madd(
2088 to_mul.binary_basis_limbs[1].element, quotient.binary_basis_limbs[0].element * neg_modulus_limbs[1]);
2089 const field_t c0 = left.binary_basis_limbs[1].element.madd(
2090 to_mul.binary_basis_limbs[1].element, quotient.binary_basis_limbs[1].element * neg_modulus_limbs[1]);
2091 const field_t c1 = left.binary_basis_limbs[2].element.madd(
2092 to_mul.binary_basis_limbs[0].element, quotient.binary_basis_limbs[2].element * neg_modulus_limbs[0]);
2093 const field_t c2 = left.binary_basis_limbs[0].element.madd(
2094 to_mul.binary_basis_limbs[2].element, quotient.binary_basis_limbs[0].element * neg_modulus_limbs[2]);
2095 const field_t d0 = left.binary_basis_limbs[3].element.madd(
2096 to_mul.binary_basis_limbs[0].element, quotient.binary_basis_limbs[3].element * neg_modulus_limbs[0]);
2097 const field_t d1 = left.binary_basis_limbs[2].element.madd(
2098 to_mul.binary_basis_limbs[1].element, quotient.binary_basis_limbs[2].element * neg_modulus_limbs[1]);
2099 const field_t d2 = left.binary_basis_limbs[1].element.madd(
2100 to_mul.binary_basis_limbs[2].element, quotient.binary_basis_limbs[1].element * neg_modulus_limbs[2]);
2101 const field_t d3 = left.binary_basis_limbs[0].element.madd(
2102 to_mul.binary_basis_limbs[3].element, quotient.binary_basis_limbs[0].element * neg_modulus_limbs[3]);
2103
2104 // We wish to show that left*right - quotient*remainder = 0 mod 2^t, we do this by collecting the limb products
2105 // into two separate variables - carry_lo and carry_hi, which are still small enough not to wrap mod r
2106 // Their first t/2 bits will equal, respectively, the first and second t/2 bits of the expresssion
2107 // Thus it will suffice to check that each of them begins with t/2 zeroes. We do this by in fact assigning
2108 // to these variables those expressions divided by 2^{t/2}. Since we have bounds on their ranage that are
2109 // smaller than r, We can range check the divisions by the original range bounds divided by 2^{t/2}
2110
2111 const field_t r0 = left.binary_basis_limbs[0].element.madd(
2112 to_mul.binary_basis_limbs[0].element, quotient.binary_basis_limbs[0].element * neg_modulus_limbs[0]);
2113
2114 field_t r1 = b0.add_two(b1, -remainders[0].binary_basis_limbs[1].element);
2115 const field_t r2 = c0.add_two(c1, c2);
2116 const field_t r3 = d0 + d1.add_two(d2, d3);
2117
2118 field_t carry_lo_0 = r0 * shift_right_2;
2119 field_t carry_lo_1 = r1 * (shift_1 * shift_right_2);
2120 field_t carry_lo_2 = -(remainders[0].binary_basis_limbs[0].element * shift_right_2);
2121 field_t carry_lo = carry_lo_0.add_two(carry_lo_1, carry_lo_2);
2122 for (const auto& add_element : to_add) {
2123 carry_lo = carry_lo.add_two(add_element.binary_basis_limbs[0].element * shift_right_2,
2124 add_element.binary_basis_limbs[1].element * (shift_1 * shift_right_2));
2125 }
2126 for (size_t i = 1; i < remainders.size(); ++i) {
2127 carry_lo = carry_lo.add_two(-remainders[i].binary_basis_limbs[0].element * shift_right_2,
2128 -remainders[i].binary_basis_limbs[1].element * (shift_1 * shift_right_2));
2129 }
2130 field_t t1 = carry_lo.add_two(-remainders[0].binary_basis_limbs[2].element,
2131 -(remainders[0].binary_basis_limbs[3].element * shift_1));
2132 field_t carry_hi_0 = r2 * shift_right_2;
2133 field_t carry_hi_1 = r3 * (shift_1 * shift_right_2);
2134 field_t carry_hi_2 = t1 * shift_right_2;
2135 field_t carry_hi = carry_hi_0.add_two(carry_hi_1, carry_hi_2);
2136
2137 for (const auto& add_element : to_add) {
2138 carry_hi = carry_hi.add_two(add_element.binary_basis_limbs[2].element * shift_right_2,
2139 add_element.binary_basis_limbs[3].element * (shift_1 * shift_right_2));
2140 }
2141 for (size_t i = 1; i < remainders.size(); ++i) {
2142 carry_hi = carry_hi.add_two(-remainders[i].binary_basis_limbs[2].element * shift_right_2,
2143 -remainders[i].binary_basis_limbs[3].element * (shift_1 * shift_right_2));
2144 }
2145 barretenberg::fr neg_prime = -barretenberg::fr(uint256_t(target_basis.modulus));
2146
2147 field_t<Builder> linear_terms(ctx, barretenberg::fr(0));
2148 if (to_add.size() >= 2) {
2149 for (size_t i = 0; i < to_add.size(); i += 2) {
2150 linear_terms = linear_terms.add_two(to_add[i].prime_basis_limb, to_add[i + 1].prime_basis_limb);
2151 }
2152 }
2153 if ((to_add.size() & 1UL) == 1UL) {
2154 linear_terms += to_add[to_add.size() - 1].prime_basis_limb;
2155 }
2156 if (remainders.size() >= 2) {
2157 for (size_t i = 0; i < (remainders.size() >> 1); i += 1) {
2158 linear_terms =
2159 linear_terms.add_two(-remainders[2 * i].prime_basis_limb, -remainders[2 * i + 1].prime_basis_limb);
2160 }
2161 }
2162 if ((remainders.size() & 1UL) == 1UL) {
2163 linear_terms += -remainders[remainders.size() - 1].prime_basis_limb;
2164 }
2165 // This is where we show our identity is zero mod r (to use CRT we show it's zero mod r and mod 2^t)
2167 left.prime_basis_limb, to_mul.prime_basis_limb, quotient.prime_basis_limb * neg_prime, linear_terms);
2168
2169 const uint64_t carry_lo_msb = max_lo_bits - (2 * NUM_LIMB_BITS);
2170 const uint64_t carry_hi_msb = max_hi_bits - (2 * NUM_LIMB_BITS);
2171
2172 const barretenberg::fr carry_lo_shift(uint256_t(uint256_t(1) << carry_lo_msb));
2173 if ((carry_hi_msb + carry_lo_msb) < field_t<Builder>::modulus.get_msb()) {
2174 field_t carry_combined = carry_lo + (carry_hi * carry_lo_shift);
2175 carry_combined = carry_combined.normalize();
2176 const auto accumulators = ctx->decompose_into_base4_accumulators(
2177 carry_combined.witness_index,
2178 static_cast<size_t>(carry_lo_msb + carry_hi_msb),
2179 "bigfield: carry_combined too large in unsafe_evaluate_multiply_add.");
2180 field_t<Builder> accumulator_midpoint =
2181 field_t<Builder>::from_witness_index(ctx, accumulators[static_cast<size_t>((carry_hi_msb / 2) - 1)]);
2182 carry_hi.assert_equal(accumulator_midpoint, "bigfield multiply range check failed");
2183 } else {
2184 carry_lo = carry_lo.normalize();
2185 carry_hi = carry_hi.normalize();
2186 ctx->decompose_into_base4_accumulators(carry_lo.witness_index,
2187 static_cast<size_t>(carry_lo_msb),
2188 "bigfield: carry_lo too large in unsafe_evaluate_multiply_add.");
2189 ctx->decompose_into_base4_accumulators(carry_hi.witness_index,
2190 static_cast<size_t>(carry_hi_msb),
2191 "bigfield: carry_hi too large in unsafe_evaluate_multiply_add.");
2192 }
2193 }
2194}
2217template <typename Builder, typename T>
2218void bigfield<Builder, T>::unsafe_evaluate_multiple_multiply_add(const std::vector<bigfield>& input_left,
2219 const std::vector<bigfield>& input_right,
2220 const std::vector<bigfield>& to_add,
2221 const bigfield& input_quotient,
2222 const std::vector<bigfield>& input_remainders)
2223{
2224
2225 std::vector<bigfield> remainders(input_remainders);
2226 std::vector<bigfield> left(input_left);
2227 std::vector<bigfield> right(input_right);
2228 bigfield quotient = input_quotient;
2229 const size_t num_multiplications = input_left.size();
2230
2231 Builder* ctx = input_left[0].context ? input_left[0].context : input_right[0].context;
2232
2233 const auto get_product_maximum = [](const bigfield& left, const bigfield& right) {
2234 uint512_t max_b0_inner = (left.binary_basis_limbs[1].maximum_value * right.binary_basis_limbs[0].maximum_value);
2235 uint512_t max_b1_inner = (left.binary_basis_limbs[0].maximum_value * right.binary_basis_limbs[1].maximum_value);
2236 uint512_t max_c0_inner = (left.binary_basis_limbs[1].maximum_value * right.binary_basis_limbs[1].maximum_value);
2237 uint512_t max_c1_inner = (left.binary_basis_limbs[2].maximum_value * right.binary_basis_limbs[0].maximum_value);
2238 uint512_t max_c2_inner = (left.binary_basis_limbs[0].maximum_value * right.binary_basis_limbs[2].maximum_value);
2239 uint512_t max_d0_inner = (left.binary_basis_limbs[3].maximum_value * right.binary_basis_limbs[0].maximum_value);
2240 uint512_t max_d1_inner = (left.binary_basis_limbs[2].maximum_value * right.binary_basis_limbs[1].maximum_value);
2241 uint512_t max_d2_inner = (left.binary_basis_limbs[1].maximum_value * right.binary_basis_limbs[2].maximum_value);
2242 uint512_t max_d3_inner = (left.binary_basis_limbs[0].maximum_value * right.binary_basis_limbs[3].maximum_value);
2243 uint512_t max_r0_inner = left.binary_basis_limbs[0].maximum_value * right.binary_basis_limbs[0].maximum_value;
2244
2245 const uint512_t max_r1_inner = max_b0_inner + max_b1_inner;
2246 const uint512_t max_r2_inner = max_c0_inner + max_c1_inner + max_c2_inner;
2247 const uint512_t max_r3_inner = max_d0_inner + max_d1_inner + max_d2_inner + max_d3_inner;
2248 const uint512_t max_lo_temp = max_r0_inner + (max_r1_inner << NUM_LIMB_BITS);
2249 const uint512_t max_hi_temp = max_r2_inner + (max_r3_inner << NUM_LIMB_BITS);
2250 return std::pair<uint512_t, uint512_t>(max_lo_temp, max_hi_temp);
2251 };
2252
2260 uint512_t max_lo = 0;
2261 uint512_t max_hi = 0;
2262
2263 // Compute max values of quotient product limb products
2264 uint512_t max_b0 = (neg_modulus_limbs_u256[1] * quotient.binary_basis_limbs[0].maximum_value);
2265 uint512_t max_b1 = (neg_modulus_limbs_u256[0] * quotient.binary_basis_limbs[1].maximum_value);
2266 uint512_t max_c0 = (neg_modulus_limbs_u256[1] * quotient.binary_basis_limbs[1].maximum_value);
2267 uint512_t max_c1 = (neg_modulus_limbs_u256[2] * quotient.binary_basis_limbs[0].maximum_value);
2268 uint512_t max_c2 = (neg_modulus_limbs_u256[0] * quotient.binary_basis_limbs[2].maximum_value);
2269 uint512_t max_d0 = (neg_modulus_limbs_u256[3] * quotient.binary_basis_limbs[0].maximum_value);
2270 uint512_t max_d1 = (neg_modulus_limbs_u256[2] * quotient.binary_basis_limbs[1].maximum_value);
2271 uint512_t max_d2 = (neg_modulus_limbs_u256[1] * quotient.binary_basis_limbs[2].maximum_value);
2272 uint512_t max_d3 = (neg_modulus_limbs_u256[0] * quotient.binary_basis_limbs[3].maximum_value);
2273
2274 // max_r0 = terms from 0 - 2^2t
2275 // max_r1 = terms from 2^t - 2^3t
2276 // max_r2 = terms from 2^2t - 2^4t
2277 // max_r3 = terms from 2^3t - 2^5t
2278 uint512_t max_r0 = (neg_modulus_limbs_u256[0] * quotient.binary_basis_limbs[0].maximum_value);
2279 max_r0 += (neg_modulus_limbs_u256[0] * quotient.binary_basis_limbs[0].maximum_value);
2280 const uint512_t max_r1 = max_b0 + max_b1;
2281 const uint512_t max_r2 = max_c0 + max_c1 + max_c2;
2282 const uint512_t max_r3 = max_d0 + max_d1 + max_d2 + max_d3;
2283
2284 // update max_lo, max_hi with quotient limb product terms.
2285 max_lo += max_r0 + (max_r1 << NUM_LIMB_BITS);
2286 max_hi += max_r2 + (max_r3 << NUM_LIMB_BITS);
2287
2288 // Compute maximum value of addition terms in `to_add` and add to max_lo, max_hi
2289 uint512_t max_a0(0);
2290 uint512_t max_a1(0);
2291 for (size_t i = 0; i < to_add.size(); ++i) {
2292 max_a0 += to_add[i].binary_basis_limbs[0].maximum_value +
2293 (to_add[i].binary_basis_limbs[1].maximum_value << NUM_LIMB_BITS);
2294 max_a1 += to_add[i].binary_basis_limbs[2].maximum_value +
2295 (to_add[i].binary_basis_limbs[3].maximum_value << NUM_LIMB_BITS);
2296 }
2297 max_lo += max_a0;
2298 max_hi += max_a1;
2299
2300 // Compute the maximum value of our multiplication products and add to max_lo, max_hi
2301 for (size_t i = 0; i < num_multiplications; ++i) {
2302 const auto [product_lo, product_hi] = get_product_maximum(left[i], right[i]);
2303 max_lo += product_lo;
2304 max_hi += product_hi;
2305 }
2306
2307 // Compute the maximum number of bits in `max_lo` and `max_hi` - this defines the range constraint values we
2308 // will need to apply to validate our product
2309 uint64_t max_lo_bits = (max_lo.get_msb() + 1);
2310 uint64_t max_hi_bits = max_hi.get_msb() + 1;
2311 // TurboPlonk range checks only work for even bit ranges, so make sure these values are even
2312 // TODO: This neccessary anymore? TurboPlonk range checks now work with odd bit ranges...
2313 if ((max_lo_bits & 1ULL) == 1ULL) {
2314 ++max_lo_bits;
2315 }
2316 if ((max_hi_bits & 1ULL) == 1ULL) {
2317 ++max_hi_bits;
2318 }
2319
2320 if constexpr (HasPlookup<Builder>) {
2321 // The plookup custom bigfield gate requires inputs are witnesses.
2322 // If we're using constant values, instantiate them as circuit variables
2323
2324 const auto convert_constant_to_fixed_witness = [ctx](const bigfield& input) {
2325 bigfield output(input);
2326 output.prime_basis_limb = field_t<Builder>::from_witness_index(
2327 ctx, ctx->put_constant_variable(input.prime_basis_limb.get_value()));
2328 output.binary_basis_limbs[0].element = field_t<Builder>::from_witness_index(
2329 ctx, ctx->put_constant_variable(input.binary_basis_limbs[0].element.get_value()));
2330 output.binary_basis_limbs[1].element = field_t<Builder>::from_witness_index(
2331 ctx, ctx->put_constant_variable(input.binary_basis_limbs[1].element.get_value()));
2332 output.binary_basis_limbs[2].element = field_t<Builder>::from_witness_index(
2333 ctx, ctx->put_constant_variable(input.binary_basis_limbs[2].element.get_value()));
2334 output.binary_basis_limbs[3].element = field_t<Builder>::from_witness_index(
2335 ctx, ctx->put_constant_variable(input.binary_basis_limbs[3].element.get_value()));
2336 output.context = ctx;
2337 return output;
2338 };
2339
2340 // evalaute a nnf mul and add into existing lohi output for our extra product terms
2341 // we need to add the result of (left_b * right_b) into lo_1_idx and hi_1_idx
2342 // our custom gate evaluates: ((a * b) + (q * neg_modulus) - r) / 2^{136} = lo + hi * 2^{136}
2343 // where q is a 'quotient' bigfield and neg_modulus is defined by selector polynomial values
2344 // The custom gate costs 7 constraints, which is cheaper than computing `a * b` using multiplication +
2345 // addition gates But....we want to obtain `left_a * right_b + lo_1 + hi_1 * 2^{136} = lo + hi * 2^{136}` If
2346 // we set `neg_modulus = [2^{136}, 0, 0, 0]` and `q = [lo_1, 0, hi_1, 0]`, then we will add `lo_1` into
2347 // `lo`, and `lo_1/2^{136} + hi_1` into `hi`. we can then subtract off `lo_1/2^{136}` from `hi`, by setting
2348 // `r = [0, 0, lo_1, 0]` This saves us 2 addition gates as we don't have to add together the outputs of two
2349 // calls to `evaluate_non_native_field_multiplication`
2350 std::vector<field_t<Builder>> limb_0_accumulator;
2351 std::vector<field_t<Builder>> limb_2_accumulator;
2352 std::vector<field_t<Builder>> prime_limb_accumulator;
2353
2354 for (size_t i = 0; i < num_multiplications; ++i) {
2355 if (i == 0 && left[0].is_constant()) {
2356 left[0] = convert_constant_to_fixed_witness(left[0]);
2357 }
2358 if (i == 0 && right[0].is_constant()) {
2359 right[0] = convert_constant_to_fixed_witness(right[0]);
2360 }
2361 if (i > 0 && left[i].is_constant()) {
2362 left[i] = convert_constant_to_fixed_witness(left[i]);
2363 }
2364 if (i > 0 && right[i].is_constant()) {
2365 right[i] = convert_constant_to_fixed_witness(right[i]);
2366 }
2367
2368 if (i > 0) {
2370 {
2371 left[i].binary_basis_limbs[0].element.normalize().witness_index,
2372 left[i].binary_basis_limbs[1].element.normalize().witness_index,
2373 left[i].binary_basis_limbs[2].element.normalize().witness_index,
2374 left[i].binary_basis_limbs[3].element.normalize().witness_index,
2375 left[i].prime_basis_limb.witness_index,
2376 },
2377 {
2378 right[i].binary_basis_limbs[0].element.normalize().witness_index,
2379 right[i].binary_basis_limbs[1].element.normalize().witness_index,
2380 right[i].binary_basis_limbs[2].element.normalize().witness_index,
2381 right[i].binary_basis_limbs[3].element.normalize().witness_index,
2382 right[i].prime_basis_limb.witness_index,
2383 },
2384 {
2385 ctx->zero_idx,
2386 ctx->zero_idx,
2387 ctx->zero_idx,
2388 ctx->zero_idx,
2389 ctx->zero_idx,
2390 },
2391 {
2392 ctx->zero_idx,
2393 ctx->zero_idx,
2394 ctx->zero_idx,
2395 ctx->zero_idx,
2396 ctx->zero_idx,
2397 },
2398 { 0, 0, 0, 0 },
2399 modulus,
2400 };
2401
2402 const auto [lo_2_idx, hi_2_idx] = ctx->queue_partial_non_native_field_multiplication(mul_witnesses);
2403
2406
2407 limb_0_accumulator.emplace_back(-lo_2);
2408 limb_2_accumulator.emplace_back(-hi_2);
2409 prime_limb_accumulator.emplace_back(-(left[i].prime_basis_limb * right[i].prime_basis_limb));
2410 }
2411 }
2412 if (quotient.is_constant()) {
2413 quotient = convert_constant_to_fixed_witness(quotient);
2414 }
2415
2416 bool no_remainders = remainders.size() == 0;
2417 if (!no_remainders) {
2418 limb_0_accumulator.emplace_back(remainders[0].binary_basis_limbs[0].element);
2419 limb_2_accumulator.emplace_back(remainders[0].binary_basis_limbs[2].element);
2420 prime_limb_accumulator.emplace_back(remainders[0].prime_basis_limb);
2421 }
2422 for (size_t i = 1; i < remainders.size(); ++i) {
2423 limb_0_accumulator.emplace_back(remainders[i].binary_basis_limbs[0].element);
2424 limb_0_accumulator.emplace_back(remainders[i].binary_basis_limbs[1].element * shift_1);
2425 limb_2_accumulator.emplace_back(remainders[i].binary_basis_limbs[2].element);
2426 limb_2_accumulator.emplace_back(remainders[i].binary_basis_limbs[3].element * shift_1);
2427 prime_limb_accumulator.emplace_back(remainders[i].prime_basis_limb);
2428 }
2429 for (const auto& add : to_add) {
2430 limb_0_accumulator.emplace_back(-add.binary_basis_limbs[0].element);
2431 limb_0_accumulator.emplace_back(-add.binary_basis_limbs[1].element * shift_1);
2432 limb_2_accumulator.emplace_back(-add.binary_basis_limbs[2].element);
2433 limb_2_accumulator.emplace_back(-add.binary_basis_limbs[3].element * shift_1);
2434 prime_limb_accumulator.emplace_back(-add.prime_basis_limb);
2435 }
2436
2437 field_t<Builder> accumulated_lo = field_t<Builder>::accumulate(limb_0_accumulator);
2438 field_t<Builder> accumulated_hi = field_t<Builder>::accumulate(limb_2_accumulator);
2439 if (accumulated_lo.is_constant()) {
2440 accumulated_lo =
2441 field_t<Builder>::from_witness_index(ctx, ctx->put_constant_variable(accumulated_lo.get_value()));
2442 }
2443 if (accumulated_hi.is_constant()) {
2444 accumulated_hi =
2445 field_t<Builder>::from_witness_index(ctx, ctx->put_constant_variable(accumulated_hi.get_value()));
2446 }
2447 field_t<Builder> remainder1 = no_remainders ? field_t<Builder>::from_witness_index(ctx, ctx->zero_idx)
2448 : remainders[0].binary_basis_limbs[1].element;
2449 if (remainder1.is_constant()) {
2450 remainder1 = field_t<Builder>::from_witness_index(ctx, ctx->put_constant_variable(remainder1.get_value()));
2451 }
2452 field_t<Builder> remainder3 = no_remainders ? field_t<Builder>::from_witness_index(ctx, ctx->zero_idx)
2453 : remainders[0].binary_basis_limbs[3].element;
2454 if (remainder3.is_constant()) {
2455 remainder3 = field_t<Builder>::from_witness_index(ctx, ctx->put_constant_variable(remainder3.get_value()));
2456 }
2457 field_t<Builder> remainder_limbs[4]{
2458 accumulated_lo,
2459 remainder1,
2460 accumulated_hi,
2461 remainder3,
2462 };
2463 field_t<Builder> remainder_prime_limb = field_t<Builder>::accumulate(prime_limb_accumulator);
2464
2466 {
2467 left[0].binary_basis_limbs[0].element.normalize().witness_index,
2468 left[0].binary_basis_limbs[1].element.normalize().witness_index,
2469 left[0].binary_basis_limbs[2].element.normalize().witness_index,
2470 left[0].binary_basis_limbs[3].element.normalize().witness_index,
2471 left[0].prime_basis_limb.normalize().witness_index,
2472 },
2473 {
2474 right[0].binary_basis_limbs[0].element.normalize().witness_index,
2475 right[0].binary_basis_limbs[1].element.normalize().witness_index,
2476 right[0].binary_basis_limbs[2].element.normalize().witness_index,
2477 right[0].binary_basis_limbs[3].element.normalize().witness_index,
2478 right[0].prime_basis_limb.normalize().witness_index,
2479 },
2480 {
2481 quotient.binary_basis_limbs[0].element.normalize().witness_index,
2482 quotient.binary_basis_limbs[1].element.normalize().witness_index,
2483 quotient.binary_basis_limbs[2].element.normalize().witness_index,
2484 quotient.binary_basis_limbs[3].element.normalize().witness_index,
2485 quotient.prime_basis_limb.normalize().witness_index,
2486 },
2487 {
2488 remainder_limbs[0].normalize().witness_index,
2489 remainder_limbs[1].normalize().witness_index,
2490 remainder_limbs[2].normalize().witness_index,
2491 remainder_limbs[3].normalize().witness_index,
2492 remainder_prime_limb.normalize().witness_index,
2493 },
2494 { neg_modulus_limbs[0], neg_modulus_limbs[1], neg_modulus_limbs[2], neg_modulus_limbs[3] },
2495 modulus,
2496 };
2497
2498 const auto [lo_1_idx, hi_1_idx] = ctx->evaluate_non_native_field_multiplication(witnesses, false);
2499
2500 barretenberg::fr neg_prime = -barretenberg::fr(uint256_t(target_basis.modulus));
2501
2502 field_t<Builder>::evaluate_polynomial_identity(left[0].prime_basis_limb,
2503 right[0].prime_basis_limb,
2504 quotient.prime_basis_limb * neg_prime,
2505 -remainder_prime_limb);
2506
2509
2510 const uint64_t carry_lo_msb = max_lo_bits - (2 * NUM_LIMB_BITS);
2511 const uint64_t carry_hi_msb = max_hi_bits - (2 * NUM_LIMB_BITS);
2512
2513 // if both the hi and lo output limbs have less than 70 bits, we can use our custom
2514 // limb accumulation gate (accumulates 2 field elements, each composed of 5 14-bit limbs, in 3 gates)
2515 if (carry_lo_msb <= 70 && carry_hi_msb <= 70) {
2516 ctx->range_constrain_two_limbs(
2517 hi.witness_index, lo.witness_index, (size_t)carry_lo_msb, (size_t)carry_hi_msb);
2518 } else {
2519 ctx->decompose_into_default_range(hi.normalize().witness_index, carry_hi_msb);
2520 ctx->decompose_into_default_range(lo.normalize().witness_index, carry_lo_msb);
2521 }
2522 /* NOTE TO AUDITOR: An extraneous block
2523 if constexpr (HasPlookup<Builder>) {
2524 carry_lo = carry_lo.normalize();
2525 carry_hi = carry_hi.normalize();
2526 ctx->decompose_into_default_range(carry_lo.witness_index, static_cast<size_t>(carry_lo_msb));
2527 ctx->decompose_into_default_range(carry_hi.witness_index, static_cast<size_t>(carry_hi_msb));
2528 }
2529 was removed from the the `else` block below. See the conversation at
2530 https://github.com/AztecProtocol/aztec2-internal/pull/1023
2531 We should make sure that no constraint like this is needed but missing (e.g., an equivalent constraint
2532 was just imposed?). */
2533 } else {
2534 field_t b0 = left[0].binary_basis_limbs[1].element.madd(
2535 right[0].binary_basis_limbs[0].element, quotient.binary_basis_limbs[1].element * neg_modulus_limbs[0]);
2536 field_t b1 = left[0].binary_basis_limbs[0].element.madd(
2537 right[0].binary_basis_limbs[1].element, quotient.binary_basis_limbs[0].element * neg_modulus_limbs[1]);
2538 field_t c0 = left[0].binary_basis_limbs[1].element.madd(
2539 right[0].binary_basis_limbs[1].element, quotient.binary_basis_limbs[1].element * neg_modulus_limbs[1]);
2540 field_t c1 = left[0].binary_basis_limbs[2].element.madd(
2541 right[0].binary_basis_limbs[0].element, quotient.binary_basis_limbs[2].element * neg_modulus_limbs[0]);
2542 field_t c2 = left[0].binary_basis_limbs[0].element.madd(
2543 right[0].binary_basis_limbs[2].element, quotient.binary_basis_limbs[0].element * neg_modulus_limbs[2]);
2544 field_t d0 = left[0].binary_basis_limbs[3].element.madd(
2545 right[0].binary_basis_limbs[0].element, quotient.binary_basis_limbs[3].element * neg_modulus_limbs[0]);
2546 field_t d1 = left[0].binary_basis_limbs[2].element.madd(
2547 right[0].binary_basis_limbs[1].element, quotient.binary_basis_limbs[2].element * neg_modulus_limbs[1]);
2548 field_t d2 = left[0].binary_basis_limbs[1].element.madd(
2549 right[0].binary_basis_limbs[2].element, quotient.binary_basis_limbs[1].element * neg_modulus_limbs[2]);
2550 field_t d3 = left[0].binary_basis_limbs[0].element.madd(
2551 right[0].binary_basis_limbs[3].element, quotient.binary_basis_limbs[0].element * neg_modulus_limbs[3]);
2552
2565 std::vector<field_t<Builder>> limb_0_accumulator;
2566 std::vector<field_t<Builder>> limb_2_accumulator;
2567 std::vector<field_t<Builder>> prime_limb_accumulator;
2568
2569 // Add remaining products into the limb accumulators.
2570 // We negate the product values because the accumulator values itself will be negated
2571 // TODO: why do we do this double negation exactly? seems a bit pointless. I think it stems from the fact
2572 // that the accumulators originaly tracked the remainder term (which is negated)
2573
2574 for (size_t i = 1; i < num_multiplications; ++i) {
2575 field_t lo_2 = left[i].binary_basis_limbs[0].element * right[i].binary_basis_limbs[0].element;
2576 lo_2 = left[i].binary_basis_limbs[1].element.madd(right[i].binary_basis_limbs[0].element * shift_1, lo_2);
2577 lo_2 = left[i].binary_basis_limbs[0].element.madd(right[i].binary_basis_limbs[1].element * shift_1, lo_2);
2578 field_t hi_2 = left[i].binary_basis_limbs[1].element * right[i].binary_basis_limbs[1].element;
2579 hi_2 = left[i].binary_basis_limbs[2].element.madd(right[i].binary_basis_limbs[0].element, hi_2);
2580 hi_2 = left[i].binary_basis_limbs[0].element.madd(right[i].binary_basis_limbs[2].element, hi_2);
2581 hi_2 = left[i].binary_basis_limbs[3].element.madd(right[i].binary_basis_limbs[0].element * shift_1, hi_2);
2582 hi_2 = left[i].binary_basis_limbs[2].element.madd(right[i].binary_basis_limbs[1].element * shift_1, hi_2);
2583 hi_2 = left[i].binary_basis_limbs[1].element.madd(right[i].binary_basis_limbs[2].element * shift_1, hi_2);
2584 hi_2 = left[i].binary_basis_limbs[0].element.madd(right[i].binary_basis_limbs[3].element * shift_1, hi_2);
2585
2586 limb_0_accumulator.emplace_back(-lo_2);
2587 limb_2_accumulator.emplace_back(-hi_2);
2588 prime_limb_accumulator.emplace_back(-(left[i].prime_basis_limb * right[i].prime_basis_limb));
2589 }
2590 // add cached products into the limb accumulators.
2591 // We negate the cache values because the accumulator values itself will be negated
2592 // TODO: why do we do this double negation exactly? seems a bit pointless. I think it stems from the fact
2593 // that the accumulators originaly tracked the remainder term (which is negated)
2594
2595 // Update the accumulators with the remainder terms. First check we actually have remainder terms!
2596 //(not present when we're checking a product is 0 mod p). See `assert_is_in_field`
2597
2598 bool no_remainders = remainders.size() == 0;
2599 if (!no_remainders) {
2600 limb_0_accumulator.emplace_back(remainders[0].binary_basis_limbs[0].element);
2601 limb_2_accumulator.emplace_back(remainders[0].binary_basis_limbs[2].element);
2602 prime_limb_accumulator.emplace_back(remainders[0].prime_basis_limb);
2603 }
2604 for (size_t i = 1; i < remainders.size(); ++i) {
2605 limb_0_accumulator.emplace_back(remainders[i].binary_basis_limbs[0].element);
2606 limb_0_accumulator.emplace_back(remainders[i].binary_basis_limbs[1].element * shift_1);
2607 limb_2_accumulator.emplace_back(remainders[i].binary_basis_limbs[2].element);
2608 limb_2_accumulator.emplace_back(remainders[i].binary_basis_limbs[3].element * shift_1);
2609 prime_limb_accumulator.emplace_back(remainders[i].prime_basis_limb);
2610 }
2611 for (const auto& add : to_add) {
2612 limb_0_accumulator.emplace_back(-add.binary_basis_limbs[0].element);
2613 limb_0_accumulator.emplace_back(-add.binary_basis_limbs[1].element * shift_1);
2614 limb_2_accumulator.emplace_back(-add.binary_basis_limbs[2].element);
2615 limb_2_accumulator.emplace_back(-add.binary_basis_limbs[3].element * shift_1);
2616 prime_limb_accumulator.emplace_back(-add.prime_basis_limb);
2617 }
2618
2619 field_t<Builder> accumulated_lo = field_t<Builder>::accumulate(limb_0_accumulator);
2620 field_t<Builder> accumulated_hi = field_t<Builder>::accumulate(limb_2_accumulator);
2621 if (accumulated_lo.is_constant()) {
2622 accumulated_lo =
2623 field_t<Builder>::from_witness_index(ctx, ctx->put_constant_variable(accumulated_lo.get_value()));
2624 }
2625 if (accumulated_hi.is_constant()) {
2626 accumulated_hi =
2627 field_t<Builder>::from_witness_index(ctx, ctx->put_constant_variable(accumulated_hi.get_value()));
2628 }
2629 field_t<Builder> remainder1 = no_remainders ? field_t<Builder>::from_witness_index(ctx, ctx->zero_idx)
2630 : remainders[0].binary_basis_limbs[1].element;
2631 if (remainder1.is_constant()) {
2632 remainder1 = field_t<Builder>::from_witness_index(ctx, ctx->put_constant_variable(remainder1.get_value()));
2633 }
2634 field_t<Builder> remainder3 = no_remainders ? field_t<Builder>::from_witness_index(ctx, ctx->zero_idx)
2635 : remainders[0].binary_basis_limbs[3].element;
2636 if (remainder3.is_constant()) {
2637 remainder3 = field_t<Builder>::from_witness_index(ctx, ctx->put_constant_variable(remainder3.get_value()));
2638 }
2639 field_t<Builder> remainder_limbs[4]{
2640 accumulated_lo,
2641 remainder1,
2642 accumulated_hi,
2643 remainder3,
2644 };
2645 field_t<Builder> remainder_prime_limb = field_t<Builder>::accumulate(prime_limb_accumulator);
2646
2647 // We wish to show that left*right - quotient*remainder = 0 mod 2^t, we do this by collecting the limb
2648 // products into two separate variables - carry_lo and carry_hi, which are still small enough not to wrap
2649 // mod r Their first t/2 bits will equal, respectively, the first and second t/2 bits of the expresssion
2650 // Thus it will suffice to check that each of them begins with t/2 zeroes. We do this by in fact assigning
2651 // to these variables those expressions divided by 2^{t/2}. Since we have bounds on their ranage that are
2652 // smaller than r, We can range check the divisions by the original range bounds divided by 2^{t/2}
2653
2654 field_t r0 = left[0].binary_basis_limbs[0].element.madd(
2655 right[0].binary_basis_limbs[0].element, quotient.binary_basis_limbs[0].element * neg_modulus_limbs[0]);
2656 field_t r1 = b0.add_two(b1, -remainder_limbs[1]);
2657 const field_t r2 = c0.add_two(c1, c2);
2658 const field_t r3 = d0 + d1.add_two(d2, d3);
2659
2660 field_t carry_lo_0 = r0 * shift_right_2;
2661 field_t carry_lo_1 = r1 * (shift_1 * shift_right_2);
2662 field_t carry_lo_2 = -(remainder_limbs[0] * shift_right_2);
2663 field_t carry_lo = carry_lo_0.add_two(carry_lo_1, carry_lo_2);
2664
2665 field_t t1 = carry_lo.add_two(-remainder_limbs[2], -(remainder_limbs[3] * shift_1));
2666 field_t carry_hi_0 = r2 * shift_right_2;
2667 field_t carry_hi_1 = r3 * (shift_1 * shift_right_2);
2668 field_t carry_hi_2 = t1 * shift_right_2;
2669 field_t carry_hi = carry_hi_0.add_two(carry_hi_1, carry_hi_2);
2670
2671 barretenberg::fr neg_prime = -barretenberg::fr(uint256_t(target_basis.modulus));
2672
2673 field_t<Builder> linear_terms(ctx, barretenberg::fr(0));
2674
2675 linear_terms += -remainder_prime_limb;
2676
2677 // This is where we show our identity is zero mod r (to use CRT we show it's zero mod r and mod 2^t)
2679 left[0].prime_basis_limb, right[0].prime_basis_limb, quotient.prime_basis_limb * neg_prime, linear_terms);
2680
2681 const uint64_t carry_lo_msb = max_lo_bits - (2 * NUM_LIMB_BITS);
2682 const uint64_t carry_hi_msb = max_hi_bits - (2 * NUM_LIMB_BITS);
2683
2684 const barretenberg::fr carry_lo_shift(uint256_t(uint256_t(1) << carry_lo_msb));
2685
2686 if constexpr (HasPlookup<Builder>) {
2687 carry_lo = carry_lo.normalize();
2688 carry_hi = carry_hi.normalize();
2689 ctx->decompose_into_default_range(carry_lo.witness_index, static_cast<size_t>(carry_lo_msb));
2690 ctx->decompose_into_default_range(carry_hi.witness_index, static_cast<size_t>(carry_hi_msb));
2691
2692 } else {
2693 if ((carry_hi_msb + carry_lo_msb) < field_t<Builder>::modulus.get_msb()) {
2694 field_t carry_combined = carry_lo + (carry_hi * carry_lo_shift);
2695 carry_combined = carry_combined.normalize();
2696 const auto accumulators = ctx->decompose_into_base4_accumulators(
2697 carry_combined.witness_index,
2698 static_cast<size_t>(carry_lo_msb + carry_hi_msb),
2699 "bigfield: carry_combined too large in unsafe_evaluate_multiple_multiply_add.");
2701 ctx, accumulators[static_cast<size_t>((carry_hi_msb / 2) - 1)]);
2702 carry_hi.assert_equal(accumulator_midpoint, "bigfield multiply range check failed");
2703 } else {
2704 carry_lo = carry_lo.normalize();
2705 carry_hi = carry_hi.normalize();
2706 ctx->decompose_into_base4_accumulators(
2707 carry_lo.witness_index,
2708 static_cast<size_t>(carry_lo_msb),
2709 "bigfield: carry_lo too large in unsafe_evaluate_multiple_multiply_add.");
2710 ctx->decompose_into_base4_accumulators(
2711 carry_hi.witness_index,
2712 static_cast<size_t>(carry_hi_msb),
2713 "bigfield: carry_hi too large in unsafe_evaluate_multiple_multiply_add.");
2714 }
2715 }
2716 }
2717}
2718
2719template <typename Builder, typename T>
2720void bigfield<Builder, T>::unsafe_evaluate_square_add(const bigfield& left,
2721 const std::vector<bigfield>& to_add,
2722 const bigfield& quotient,
2723 const bigfield& remainder)
2724{
2725 if (HasPlookup<Builder>) {
2726 unsafe_evaluate_multiply_add(left, left, to_add, quotient, { remainder });
2727 return;
2728 }
2729 Builder* ctx = left.context == nullptr ? quotient.context : left.context;
2730
2731 uint512_t max_b0 = (left.binary_basis_limbs[1].maximum_value * left.binary_basis_limbs[0].maximum_value);
2732 max_b0 += (neg_modulus_limbs_u256[1] << NUM_LIMB_BITS);
2733 max_b0 += max_b0;
2734 uint512_t max_c0 = (left.binary_basis_limbs[1].maximum_value * left.binary_basis_limbs[1].maximum_value);
2735 max_c0 += (neg_modulus_limbs_u256[1] << NUM_LIMB_BITS);
2736 uint512_t max_c1 = (left.binary_basis_limbs[2].maximum_value * left.binary_basis_limbs[0].maximum_value);
2737 max_c1 += (neg_modulus_limbs_u256[2] << NUM_LIMB_BITS);
2738 max_c1 += max_c1;
2739 uint512_t max_d0 = (left.binary_basis_limbs[3].maximum_value * left.binary_basis_limbs[0].maximum_value);
2740 max_d0 += (neg_modulus_limbs_u256[3] << NUM_LIMB_BITS);
2741 max_d0 += max_d0;
2742 uint512_t max_d1 = (left.binary_basis_limbs[2].maximum_value * left.binary_basis_limbs[1].maximum_value);
2743 max_d1 += (neg_modulus_limbs_u256[2] << NUM_LIMB_BITS);
2744 max_d1 += max_d1;
2745
2746 uint512_t max_r0 = left.binary_basis_limbs[0].maximum_value * left.binary_basis_limbs[0].maximum_value;
2747 max_r0 += (neg_modulus_limbs_u256[0] << NUM_LIMB_BITS);
2748
2749 const uint512_t max_r1 = max_b0;
2750 const uint512_t max_r2 = max_c0 + max_c1;
2751 const uint512_t max_r3 = max_d0 + max_d1;
2752
2753 uint512_t max_a0(0);
2754 uint512_t max_a1(1);
2755 for (size_t i = 0; i < to_add.size(); ++i) {
2756 max_a0 += to_add[i].binary_basis_limbs[0].maximum_value +
2757 (to_add[i].binary_basis_limbs[1].maximum_value << NUM_LIMB_BITS);
2758 max_a1 += to_add[i].binary_basis_limbs[2].maximum_value +
2759 (to_add[i].binary_basis_limbs[3].maximum_value << NUM_LIMB_BITS);
2760 }
2761 const uint512_t max_lo = max_r0 + (max_r1 << NUM_LIMB_BITS) + max_a0;
2762 const uint512_t max_hi = max_r2 + (max_r3 << NUM_LIMB_BITS) + max_a1;
2763
2764 uint64_t max_lo_bits = max_lo.get_msb() + 1;
2765 uint64_t max_hi_bits = max_hi.get_msb() + 1;
2766 if ((max_lo_bits & 1ULL) == 1ULL) {
2767 ++max_lo_bits;
2768 }
2769 if ((max_hi_bits & 1ULL) == 1ULL) {
2770 ++max_hi_bits;
2771 }
2772
2773 field_t half(ctx, barretenberg::fr(2).invert());
2774 field_t two(ctx, barretenberg::fr(2));
2775 field_t b_quotient_0 = (quotient.binary_basis_limbs[1].element * neg_modulus_limbs[0]);
2776 field_t b_quotient_1 = (quotient.binary_basis_limbs[0].element * neg_modulus_limbs[1]);
2777
2778 field_t c_quotient_0 = (quotient.binary_basis_limbs[2].element * neg_modulus_limbs[0]);
2779 field_t c_quotient_1 = (quotient.binary_basis_limbs[0].element * neg_modulus_limbs[2]);
2780
2781 field_t d_quotient_0 = (quotient.binary_basis_limbs[3].element * neg_modulus_limbs[0]);
2782 field_t d_quotient_1 = (quotient.binary_basis_limbs[1].element * neg_modulus_limbs[2]);
2783 field_t d_quotient_2 = (quotient.binary_basis_limbs[0].element * neg_modulus_limbs[3]);
2784 field_t d_quotient_3 = (quotient.binary_basis_limbs[2].element * neg_modulus_limbs[1]);
2785
2786 const field_t b0 =
2787 two * left.binary_basis_limbs[1].element.madd(left.binary_basis_limbs[0].element, b_quotient_0 * half);
2788
2789 const field_t c0 = left.binary_basis_limbs[1].element.madd(
2790 left.binary_basis_limbs[1].element, quotient.binary_basis_limbs[1].element * neg_modulus_limbs[1]);
2791 const field_t c1 =
2792 two * left.binary_basis_limbs[2].element.madd(left.binary_basis_limbs[0].element, c_quotient_0 * half);
2793
2794 const field_t d0 =
2795 two * left.binary_basis_limbs[3].element.madd(left.binary_basis_limbs[0].element, d_quotient_0 * half);
2796
2797 const field_t d1 =
2798 two * left.binary_basis_limbs[2].element.madd(left.binary_basis_limbs[1].element, d_quotient_1 * half);
2799
2800 const field_t r0 = left.binary_basis_limbs[0].element.madd(
2801 left.binary_basis_limbs[0].element, quotient.binary_basis_limbs[0].element * neg_modulus_limbs[0]);
2802
2803 const field_t r1 = b0.add_two(b_quotient_1, -remainder.binary_basis_limbs[1].element);
2804 const field_t r2 = c0.add_two(c_quotient_1, c1);
2805 const field_t r3 = d0.add_two(d_quotient_2, d1) + d_quotient_3;
2806
2807 field_t carry_lo_0 = r0 * shift_right_2;
2808 field_t carry_lo_1 = r1 * (shift_1 * shift_right_2);
2809 field_t carry_lo_2 = -(remainder.binary_basis_limbs[0].element * shift_right_2);
2810 field_t carry_lo = carry_lo_0.add_two(carry_lo_1, carry_lo_2);
2811
2812 for (const auto& add_element : to_add) {
2813 carry_lo = carry_lo.add_two(add_element.binary_basis_limbs[0].element * shift_right_2,
2814 add_element.binary_basis_limbs[1].element * (shift_1 * shift_right_2));
2815 }
2816
2817 field_t t1 = carry_lo.add_two(-remainder.binary_basis_limbs[2].element,
2818 -(remainder.binary_basis_limbs[3].element * shift_1));
2819 field_t carry_hi_0 = r2 * shift_right_2;
2820 field_t carry_hi_1 = r3 * (shift_1 * shift_right_2);
2821 field_t carry_hi_2 = t1 * shift_right_2;
2822 field_t carry_hi = carry_hi_0.add_two(carry_hi_1, carry_hi_2);
2823
2824 for (const auto& add_element : to_add) {
2825 carry_hi = carry_hi.add_two(add_element.binary_basis_limbs[2].element * shift_right_2,
2826 add_element.binary_basis_limbs[3].element * (shift_1 * shift_right_2));
2827 }
2828
2829 barretenberg::fr neg_prime = -barretenberg::fr(uint256_t(target_basis.modulus));
2830 field_t<Builder> linear_terms = -remainder.prime_basis_limb;
2831 if (to_add.size() >= 2) {
2832 for (size_t i = 0; i < to_add.size() / 2; i += 1) {
2833 linear_terms = linear_terms.add_two(to_add[2 * i].prime_basis_limb, to_add[2 * i + 1].prime_basis_limb);
2834 }
2835 }
2836 if ((to_add.size() & 1UL) == 1UL) {
2837 linear_terms += to_add[to_add.size() - 1].prime_basis_limb;
2838 }
2840 left.prime_basis_limb, left.prime_basis_limb, quotient.prime_basis_limb * neg_prime, linear_terms);
2841
2842 const uint64_t carry_lo_msb = max_lo_bits - (2 * NUM_LIMB_BITS);
2843 const uint64_t carry_hi_msb = max_hi_bits - (2 * NUM_LIMB_BITS);
2844
2845 const barretenberg::fr carry_lo_shift(uint256_t(uint256_t(1) << carry_lo_msb));
2846 if constexpr (HasPlookup<Builder>) {
2847 carry_lo = carry_lo.normalize();
2848 carry_hi = carry_hi.normalize();
2849 ctx->decompose_into_default_range(carry_lo.witness_index, static_cast<size_t>(carry_lo_msb));
2850 ctx->decompose_into_default_range(carry_hi.witness_index, static_cast<size_t>(carry_hi_msb));
2851
2852 } else {
2853 if ((carry_hi_msb + carry_lo_msb) < field_t<Builder>::modulus.get_msb()) {
2854 field_t carry_combined = carry_lo + (carry_hi * carry_lo_shift);
2855 carry_combined = carry_combined.normalize();
2856 const auto accumulators = ctx->decompose_into_base4_accumulators(
2857 carry_combined.witness_index,
2858 static_cast<size_t>(carry_lo_msb + carry_hi_msb),
2859 "bigfield: carry_combined too large in unsafe_evaluate_square_add.");
2860 field_t<Builder> accumulator_midpoint =
2861 field_t<Builder>::from_witness_index(ctx, accumulators[static_cast<size_t>((carry_hi_msb / 2) - 1)]);
2862 carry_hi.assert_equal(accumulator_midpoint, "bigfield multiply range check failed");
2863 } else {
2864 carry_lo = carry_lo.normalize();
2865 carry_hi = carry_hi.normalize();
2866 ctx->decompose_into_base4_accumulators(carry_lo.witness_index,
2867 static_cast<size_t>(carry_lo_msb),
2868 "bigfield: carry_lo too large in unsafe_evaluate_square_add.");
2869 ctx->decompose_into_base4_accumulators(carry_hi.witness_index,
2870 static_cast<size_t>(carry_hi_msb),
2871 "bigfield: carry_hi too large in unsafe_evaluate_square_add");
2872 }
2873 }
2874}
2875
2876template <typename Builder, typename T>
2877std::pair<uint512_t, uint512_t> bigfield<Builder, T>::compute_quotient_remainder_values(
2878 const bigfield& a, const bigfield& b, const std::vector<bigfield>& to_add)
2879{
2880 uint512_t add_values(0);
2881 for (const auto& add_element : to_add) {
2882 add_element.reduction_check();
2883 add_values += add_element.get_value();
2884 }
2885
2886 const uint1024_t left(a.get_value());
2887 const uint1024_t right(b.get_value());
2888 const uint1024_t add_right(add_values);
2889 const uint1024_t modulus(target_basis.modulus);
2890
2891 const auto [quotient_1024, remainder_1024] = (left * right + add_right).divmod(modulus);
2892
2893 return { quotient_1024.lo, remainder_1024.lo };
2894}
2895
2896template <typename Builder, typename T>
2897uint512_t bigfield<Builder, T>::compute_maximum_quotient_value(const std::vector<uint512_t>& as,
2898 const std::vector<uint512_t>& bs,
2899 const std::vector<uint512_t>& to_add)
2900{
2901 ASSERT(as.size() == bs.size());
2902 uint512_t add_values(0);
2903 for (const auto& add_element : to_add) {
2904 add_values += add_element;
2905 }
2906 uint1024_t product_sum(0);
2907 for (size_t i = 0; i < as.size(); i++) {
2908 product_sum += uint1024_t(as[i]) * uint1024_t(bs[i]);
2909 }
2910 const uint1024_t add_right(add_values);
2911 const uint1024_t modulus(target_basis.modulus);
2912
2913 const auto [quotient_1024, remainder_1024] = (product_sum + add_right).divmod(modulus);
2914
2915 return quotient_1024.lo;
2916}
2917template <typename Builder, typename T>
2918std::pair<bool, size_t> bigfield<Builder, T>::get_quotient_reduction_info(const std::vector<uint512_t>& as_max,
2919 const std::vector<uint512_t>& bs_max,
2920 const std::vector<bigfield>& to_add,
2921 const std::vector<uint1024_t>& remainders_max)
2922{
2923 ASSERT(as_max.size() == bs_max.size());
2924 // Check if the product sum can overflow CRT modulus
2925 if (mul_product_overflows_crt_modulus(as_max, bs_max, to_add)) {
2926 return std::pair<bool, size_t>(true, 0);
2927 }
2928 const size_t num_quotient_bits = get_quotient_max_bits(remainders_max);
2929 std::vector<uint512_t> to_add_max;
2930 for (auto& added_element : to_add) {
2931 to_add_max.push_back(added_element.get_maximum_value());
2932 }
2933 // Get maximum value of quotient
2934 const uint512_t maximum_quotient = compute_maximum_quotient_value(as_max, bs_max, to_add_max);
2935
2936 // Check if the quotient can fit into the range proof
2937 if (maximum_quotient >= (uint512_t(1) << num_quotient_bits)) {
2938 return std::pair<bool, size_t>(true, 0);
2939 }
2940 return std::pair<bool, size_t>(false, num_quotient_bits);
2941}
2942
2943} // namespace stdlib
2944} // namespace proof_system::plonk
Definition: uint256.hpp:25
constexpr uint256_t slice(uint64_t start, uint64_t end) const
Definition: uint256_impl.hpp:157
virtual uint32_t add_variable(const FF &in)
Definition: circuit_builder_base.hpp:163
Definition: standard_circuit_builder.hpp:12
void create_big_add_gate(const add_quad_< FF > &in)
Definition: standard_circuit_builder.cpp:43
Definition: bigfield.hpp:17
void convert_constant_to_fixed_witness(Builder *builder)
Definition: bigfield.hpp:302
Definition: byte_array.hpp:9
Definition: field.hpp:10
static field_t accumulate(const std::vector< field_t > &to_add)
Definition: field.cpp:936
barretenberg::fr additive_constant
Definition: field.hpp:379
uint32_t witness_index
Definition: field.hpp:423
field_t normalize() const
Definition: field.cpp:482
void assert_equal(const field_t &rhs, std::string const &msg="field_t::assert_equal") const
Constrain that this field is equal to the given field.
Definition: field.cpp:749
field_t madd(const field_t &to_mul, const field_t &to_add) const
Definition: field.cpp:384
Definition: witness.hpp:10
Contains all the headers required to adequately compile the types defined in circuit_builders_fwd....
Definition: circuit_builders.hpp:11
constexpr_utils defines some helper methods that perform some stl-equivalent operations but in a cons...
Definition: constexpr_utils.hpp:16
Definition: widget.bench.cpp:13
Definition: ultra_circuit_builder.hpp:17