feat(avm): ToRadix gadget

barretenberg/cpp/pil/vm2/execution.pil

@@ -13,6 +13,7 @@ include "ecc.pil";
 include "poseidon2_hash.pil";
 include "poseidon2_perm.pil";
 include "scalar_mul.pil";
+include "to_radix.pil";
 
 namespace execution;
 

barretenberg/cpp/pil/vm2/precomputed.pil

@@ -81,3 +81,15 @@ pol constant instr_size_in_bytes;
 // Is used to lookup into the wire instruction spec table which contains the operand decomposition
 // selectors as well as exec_opcode
 pol constant sel_range_wire_opcode;
+
+// Used for getting the number of safe limbs for a given radix.
+// The selector is on for 1 < clk <= 256
+pol constant sel_to_radix_safe_limbs;
+// Number of safe limbs for a given radix=clk.
+pol constant to_radix_safe_limbs;
+
+// Radix decompositions of P.
+pol constant sel_p_decomposition;
+pol constant p_decomposition_radix;
+pol constant p_decomposition_limb_index;
+pol constant p_decomposition_limb;

barretenberg/cpp/pil/vm2/scalar_mul.pil

@@ -1,4 +1,5 @@
 include "ecc.pil";
+include "to_radix.pil";
 
 // Performs scalar_mul with Fr scalars doing the following algorithm:
 //
@@ -102,7 +103,9 @@ namespace scalar_mul;
 
     // We start with bit index 253
     start * (bit_idx - 253) = 0;
-    // End can only be 1 when bit_idx is 0. This should be correct because end is bool and bit_idx is being constrained to be 0..254
+    // End can only be 1 when bit_idx is 0.
+    // This does not imply that end will be 1 when bit_idx is zero. The prover can choose to not turn end on
+    // but then they won't be able to reach an end again in the whole trace, rendering the trace invalid.
     end * bit_idx = 0;
 
     // Next bit index has to be 1 less except on end
@@ -112,11 +115,11 @@ namespace scalar_mul;
     pol commit bit_radix;
     sel * (bit_radix - 2) = 0;
 
-    // #[TO_RADIX]
-    // sel { scalar, bit, bit_idx, bit_radix }
-    // in
-    // to_radix.sel
-    //     { to_radix.input, to_radix.limb, to_radix.limb_index, to_radix.radix };
+    #[TO_RADIX]
+    sel { scalar, bit, bit_idx, bit_radix }
+    in
+    to_radix.sel
+        { to_radix.value, to_radix.limb, to_radix.limb_index, to_radix.radix };
 
 
     // TEMP COMPUTATION

barretenberg/cpp/pil/vm2/to_radix.pil

@@ -0,0 +1,221 @@
+include "range_check.pil";
+
+// Decomposes a field in radixes
+// Roughly, what we do is keep track of an accumulator where we reconstruct value using the limbs. We can end when the accumulator is equal to the value (found).
+// For overflow protection, we compare the limbs against the p limbs for the given radix. If we reach the last limb (is_unsafe) we assert that we are under p.
+// Overflow in the accumulator can only happen in the unsafe limb. After the unsafe limb we have padding limbs, that we assert to be zero. This is used
+// because users might want to decompose in more limbs that strictly needed for the radix.
+// The following table is non-exhaustive, we do have some extra columns to compute these values.
+// +-------+-------+------+--------+------------+------+-------------+----------+------------------+-------+------------+-----------+-------+-----+-----+---------+
+// | value | radix | limb | p_limb | limb_index | acc  | acc_under_p | exponent | not_padding_limb | found | safe_limbs | is_unsafe | start | end | sel | not_end |
+// +-------+-------+------+--------+------------+------+-------------+----------+------------------+-------+------------+-----------+-------+-----+-----+---------+
+// |     0 |     0 |    0 |      0 |          0 |    0 |           0 | 0        |                0 |     0 |          0 |         0 |     0 |   0 |   0 |       0 |
+// |  1337 |    10 |    7 |      7 |          0 |    7 |           0 | 1        |                1 |     0 |         76 |         0 |     1 |   0 |   1 |       1 |
+// |  1337 |    10 |    3 |      1 |          1 |   37 |           0 | 10       |                1 |     0 |         76 |         0 |     0 |   0 |   1 |       1 |
+// |  1337 |    10 |    3 |      6 |          2 |  337 |           1 | 100      |                1 |     0 |         76 |         0 |     0 |   0 |   1 |       1 |
+// |  1337 |    10 |    1 |      5 |          3 | 1337 |           1 | 1000     |                1 |     1 |         76 |         0 |     0 |   0 |   1 |       1 |
+// |  1337 |    10 |    0 |      9 |          4 | 1337 |           1 | 10000    |                1 |     1 |         76 |         0 |     0 |   0 |   1 |       1 |
+// |  1337 |    10 |    0 |      2 |         76 | 1337 |           1 | 10**76   |                1 |     1 |         76 |         1 |     0 |   0 |   1 |       1 |
+// |  1337 |    10 |    0 |      0 |         77 | 1337 |           0 | 0        |                0 |     1 |         76 |         0 |     0 |   1 |   1 |       0 |
+// |     0 |     0 |    0 |      0 |          0 |    0 |           0 | 0        |                0 |     0 |          0 |         0 |     0 |   0 |   0 |       0 |
+// +-------+-------+------+--------+------------+------+-------------+----------+------------------+-------+------------+-----------+-------+-----+-----+---------+
+namespace to_radix;
+
+    #[skippable_if]
+    sel = 0;
+
+    pol commit sel;
+    sel * (1 - sel) = 0;
+
+    // Inputs to to_radix
+    pol commit value;
+    pol commit radix; // Must be 256 >= radix >= 2
+    pol commit limb_index;
+
+    // Outputs of to_radix
+    pol commit limb;
+
+
+    // LIFECYCLE
+
+    pol commit start;
+    start * (1 - start) = 0;
+
+    pol commit end;
+    end * (1 - end) = 0;
+
+    // end and first_row are NAND
+    end * precomputed.first_row = 0;
+    pol LATCH_CONDITION = end + precomputed.first_row;
+
+    #[START_AFTER_LATCH]
+    sel' * (start' - LATCH_CONDITION) = 0;
+
+    // Selector must be 1 in a start row
+    #[SELECTOR_ON_START]
+    start * (1 - sel) = 0;
+    // Next selector must be current selector unless LATCH_CONDITION
+    #[SELECTOR_CONSISTENCY]
+    (sel' - sel) * (1 - LATCH_CONDITION) = 0;
+    // Selector must be 1 in an end row
+    end * (1 - sel) = 0;
+
+    // Commited to reduce the degree of expressions
+    pol commit not_end;
+    sel * (1 - end) - not_end = 0;
+
+
+    // EXPONENTIATION
+
+    pol commit exponent;
+    // We commit not_padding_limb instead of the more natural padding_limb because it's going to be used in a lookup
+    pol commit not_padding_limb;
+    not_padding_limb * (1 - not_padding_limb) = 0;
+
+    // exponent starts at 1
+    start * (exponent - 1) = 0;
+    // next exponent is current exponent * radix unless it's a padding limb
+    not_end * not_padding_limb' * (exponent * radix - exponent') = 0;
+    // not_padding_limb starts at 1
+    start * (1 - not_padding_limb) = 0;
+    // next not not_padding_limb is current not_padding_limb unless current limb is unsafe, where it changes to 0
+    not_end * ((0 - not_padding_limb) * is_unsafe_limb + not_padding_limb - not_padding_limb') = 0;
+
+    // Padding limbs have zero exponent
+    (1 - not_padding_limb) * exponent = 0;
+
+
+    // ACCUMULATION
+
+    pol commit acc;
+    pol commit found;
+    found * (1 - found) = 0;
+
+    // Limb index starts at zero
+    start * (limb_index - 0) = 0;
+
+    // Limb index must increase
+    not_end * (limb_index + 1 - limb_index') = 0;
+
+    // Range check limb so we can safely assert that it's less than radix.
+    #[LIMB_RANGE]
+    sel { limb }
+    in
+    precomputed.sel_range_8
+        { precomputed.clk };
+
+    // Limb should be less than radix
+    pol commit limb_radix_diff;
+    sel * (radix - 1 - limb - limb_radix_diff) = 0;
+
+    #[LIMB_LESS_THAN_RADIX_RANGE]
+    sel { limb_radix_diff }
+    in
+    precomputed.sel_range_8
+        { precomputed.clk };
+
+
+    // On start, current acc must be equal to limb
+    start * (acc - limb) = 0;
+    // Next acc must be current acc + next_exponent*next_limb
+    not_end * (acc + exponent' * limb' - acc') = 0;
+
+    // found is 1 when value - acc = 0
+    pol REM = value - acc;
+    pol commit rem_inverse;
+    sel * (REM * (found * (1 - rem_inverse) + rem_inverse) - 1 + found) = 0;
+
+    // when found is 1, next limb is 0
+    not_end * found * limb' = 0;
+
+    // We can only enable end when found is one
+    (1 - found) * end = 0;
+
+
+    // OVERFLOW PROTECTION
+
+    pol commit safe_limbs;
+
+    #[FETCH_SAFE_LIMBS]
+    start { radix, safe_limbs }
+    in
+    precomputed.sel_to_radix_safe_limbs
+        { precomputed.clk, precomputed.to_radix_safe_limbs };
+
+    pol commit is_unsafe_limb;
+    is_unsafe_limb * (1 - is_unsafe_limb) = 0;
+
+    // If is_padding_limb, limb is zero
+    (1 - not_padding_limb) * limb = 0;
+    // If is_padding_limb, p_limb is zero
+    (1 - not_padding_limb) * p_limb = 0;
+
+    // is_unsafe_limb is on when and only when limb_index == safe_limbs
+    pol safety_diff = limb_index - safe_limbs;
+    pol commit safety_diff_inverse;
+    sel * (safety_diff * (is_unsafe_limb * (1 - safety_diff_inverse) + safety_diff_inverse) - 1 + is_unsafe_limb) = 0;
+
+    // The limb of the modulus p decomposed by radix at this limb_index
+    pol commit p_limb;
+
+    #[FETCH_P_LIMB]
+    not_padding_limb { radix, limb_index, p_limb }
+    in
+    precomputed.sel_p_decomposition
+        { precomputed.p_decomposition_radix, precomputed.p_decomposition_limb_index, precomputed.p_decomposition_limb };
+
+    // We carry wether the accumulator is under p. If we reach the unsafe limb, we need to ensure that this is true.
+    pol commit acc_under_p;
+    acc_under_p * (1 - acc_under_p) = 0;
+
+    // 1 when lt, 0 when gt or equal
+    pol commit limb_lt_p;
+    limb_lt_p * (1 - limb_lt_p) = 0;
+
+    pol commit limb_eq_p;
+    limb_eq_p * (1 - limb_eq_p) = 0;
+
+    // limb_eq_p and limb_lt_p are NAND
+    limb_eq_p * limb_lt_p = 0;
+
+    // validate limb_lt_p and limb_eq_p
+    pol commit limb_p_diff;
+
+    pol LIMB_LT_P = p_limb - limb - 1;
+    pol LIMB_GT_P = limb - p_limb - 1;
+    // We already need an 8 bit range check for the LT/GT cases. We can reuse that range check
+    // to validate the EQ case, instead of doing the classical inversion mechanism.
+    // (limb - p_limb) can go from -255 to +255, so if we multiply by 256 any number in the range
+    // will be greater than 8 bits except for 0.
+    pol LIMB_EQ_P = (limb - p_limb) * 256;
+
+    // limb_p_diff = if limb_lt_p {LIMB_LT_P} else if limb_eq_p {LIMB_EQ_P} else {LIMB_GT_P}
+    limb_lt_p * (LIMB_LT_P - limb_p_diff) = 0;
+    sel * (1 - limb_lt_p) * ((LIMB_EQ_P - LIMB_GT_P) * limb_eq_p + LIMB_GT_P - limb_p_diff) = 0;
+
+    #[LIMB_P_DIFF_RANGE]
+    not_padding_limb { limb_p_diff }
+    in
+    precomputed.sel_range_8
+        { precomputed.clk };
+
+    // acc_under_p is on start is equal to limb_lt_p
+    start * (acc_under_p - limb_lt_p) = 0;
+    // acc_under_p' = limb_eq_p' ? acc_under_p : limb_lt_p'
+    not_end * ((acc_under_p - limb_lt_p') * limb_eq_p' + limb_lt_p' - acc_under_p') = 0;
+
+    // On the the unsafe limb, we must be under p
+    #[OVERFLOW_CHECK]
+    is_unsafe_limb * (1 - acc_under_p) = 0;
+
+
+    // CONSTANT CONSISTENCY
+
+    #[CONSTANT_CONSISTENCY_RADIX]
+    not_end * (radix - radix') = 0;
+
+    #[CONSTANT_CONSISTENCY_VALUE]
+    not_end * (value - value') = 0;
+
+    #[CONSTANT_CONSISTENCY_SAFE_LIMBS]
+    not_end * (safe_limbs - safe_limbs') = 0;

barretenberg/cpp/src/barretenberg/vm2/common/to_radix.cpp

@@ -0,0 +1,39 @@
+#include "barretenberg/vm2/common/to_radix.hpp"
+
+#include "barretenberg/numeric/uint256/uint256.hpp"
+#include "barretenberg/vm2/common/field.hpp"
+
+namespace bb::avm2 {
+
+namespace {
+
+// The little endian decompositions of Fr modulus into limbs for each radix.
+// Radix goes up to 256 so we need 257 descompositions.
+std::array<std::vector<uint8_t>, 257> create_p_limbs_per_radix()
+{
+    std::array<std::vector<uint8_t>, 257> limbs_per_radix;
+
+    for (size_t radix = 2; radix < 257; ++radix) {
+        std::vector<uint8_t> p_limbs{};
+        p_limbs.reserve(31);
+        uint256_t p = FF::modulus;
+        while (p > 0) {
+            p_limbs.push_back(static_cast<uint8_t>(p % radix));
+            p /= radix;
+        }
+
+        limbs_per_radix[radix] = p_limbs;
+    }
+
+    return limbs_per_radix;
+}
+
+} // namespace
+
+const std::array<std::vector<uint8_t>, 257>& get_p_limbs_per_radix()
+{
+    static const std::array<std::vector<uint8_t>, 257> limbs_per_radix = create_p_limbs_per_radix();
+    return limbs_per_radix;
+}
+
+} // namespace bb::avm2

barretenberg/cpp/src/barretenberg/vm2/common/to_radix.hpp

@@ -0,0 +1,11 @@
+#pragma once
+
+#include <array>
+#include <cstdint>
+#include <vector>
+
+namespace bb::avm2 {
+
+const std::array<std::vector<uint8_t>, 257>& get_p_limbs_per_radix();
+
+} // namespace bb::avm2