Skip to content

feat(AVM): Fail on incomplete toRadix decompositions #17233

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
sirasistant merged 14 commits into from
Sep 24, 2025
Merged

feat(AVM): Fail on incomplete toRadix decompositions #17233

Show file tree
Hide file tree
Changes from 10 commits
Commits
Show all changes
14 commits
Select commit Hold shift + click to select a range
58ec732
wip
sirasistant Sep 23, 2025
815d5c3
tests
sirasistant Sep 23, 2025
72da81c
delete extraneous change
sirasistant Sep 23, 2025
b54edec
Merge branch 'merge-train/avm' into arv/to_radix_decomposition
sirasistant Sep 23, 2025
0903af8
fix pure to radix
sirasistant Sep 23, 2025
b8082c6
fix endianness
sirasistant Sep 23, 2025
52243c2
fix
sirasistant Sep 24, 2025
547f842
rename
sirasistant Sep 24, 2025
85ad5d8
Merge branch 'merge-train/avm' into arv/to_radix_decomposition
sirasistant Sep 24, 2025
5fb3753
regen after merge
sirasistant Sep 24, 2025
4eb52cc
add comment
sirasistant Sep 24, 2025
6bcfef8
address PR comments
sirasistant Sep 24, 2025
f570947
remove parenthesis
sirasistant Sep 24, 2025
ec098f4
avoid taking a reference to a value that can be dropped
sirasistant Sep 24, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
82 changes: 59 additions & 23 deletions barretenberg/cpp/pil/vm2/to_radix_mem.pil
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -40,17 +40,21 @@ include "precomputed.pil";
* (2) INVALID_NUM_LIMBS: If num_limbs = 0 while value_to_decompose != 0.
* (3) DST_OUT_OF_BOUNDS_ACCESS: If the writes would access a memory address outside
* of the max AVM memory address (AVM_HIGHEST_MEM_ADDRESS).
* (4) TRUNCATION_ERROR: If the value can't be fully decomposed in the given number of limbs.
Comment thread
jeanmon marked this conversation as resolved.
*
* N.B The radix is checked to be <= 256 in the execution trace (for dynamic gas computation)
* we do not currently take advantage of any partial checks done but is a future optimisation
* Finally, if is num_limbs = 0 && value_to_decompose = 0 (which are valid inputs), then no memory writes are performed
* Also, if is num_limbs = 0 && value_to_decompose = 0 (which are valid inputs), then no memory writes are performed
* Finally, we check that the value has been fully decomposed in the given number of limbs. In order to do this, we
* check in the start row that the value has been found in the TORADIX subtrace.
*
* This subtrace is connected to the TORADIX subtrace via a lookup. TORADIX is used by
* other subtraces internally (e.g., scalar mul).
*
* NOTE: The TORADIX subtrace performs the decomposition in LITTLE ENDIAN. This is more optimal
* for the internal gadget use. Therefore this subtrace needs to reverse the output of TORADIX
* since the opcode requires BIG ENDIAN.
* since the opcode requires BIG ENDIAN. This allows us to perform the check for truncation error in the start row,
* since the start row of this trace is the last limb in the little endian decomposition.
*/

namespace to_radix_mem;
Expand Down Expand Up @@ -172,12 +176,52 @@ namespace to_radix_mem;
pol commit sel_invalid_num_limbs_err; // err = 1 if num_limbs == 0 while value != 0
sel_invalid_num_limbs_err = sel_num_limbs_is_zero * (1 - sel_value_is_zero);

// err is constrained on the row where start == 1. (each specific error is gated by start)
pol commit err; // Consolidated error flag
err = 1 - (1 - sel_dst_out_of_range_err) * (1 - sel_radix_lt_2_err)

/////////////////////////////////////////////////////
// Dispatch inputs to to_radix
/////////////////////////////////////////////////////
pol commit input_validation_error;
input_validation_error = 1 - (1 - sel_dst_out_of_range_err) * (1 - sel_radix_lt_2_err)
* (1 - sel_radix_gt_256_err) * (1 - sel_invalid_bitwise_radix)
* (1 - sel_invalid_num_limbs_err);

pol commit output_limb_value;

@jeanmon jeanmon Sep 24, 2025

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

A comment here about what is output_limb_value and value_found would be welcome.

@jeanmon jeanmon Sep 24, 2025

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Maybe a rename to limb_value would be less confusing IMHO.

pol commit value_found;
pol commit sel_should_decompose;
sel_should_decompose * (1 - sel_should_decompose) = 0;

// On the start row, we define sel_should_decompose as !validation_error && !num_limbs_is_zero

@jeanmon jeanmon Sep 24, 2025

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Suggested change
// On the start row, we define sel_should_decompose as !validation_error && !num_limbs_is_zero
// On the start row, we define sel_should_decompose as !input_validation_error && !num_limbs_is_zero

// We can't inline input_validation_error because of the degree.
start * ((1 - input_validation_error) * (1 - sel_num_limbs_is_zero) - sel_should_decompose) = 0;

// On following rows, we propagate input_validation_error.
#[sel_should_decompose_CONTINUITY]
NOT_LAST * (sel_should_decompose' - sel_should_decompose) = 0;

pol commit limb_index_to_lookup; // Need this since we want Big-Endian but the gadget is Little-Endian
limb_index_to_lookup = sel_should_decompose * (num_limbs - 1);

#[INPUT_OUTPUT_TO_RADIX]
sel_should_decompose { value_to_decompose, limb_index_to_lookup, radix, output_limb_value, value_found }
in
to_radix.sel {to_radix.value, to_radix.limb_index, to_radix.radix, to_radix.limb, to_radix.found };

/////////////////////////////////////////////////////
// Error Handling - Check no truncation error
/////////////////////////////////////////////////////
pol commit sel_truncation_error;
sel_truncation_error * (1 - sel_truncation_error) = 0;
// A truncation error happens if in the start row, we look up the to_radix gadget and value_found is off.
// The to radix gadget is little endian, so the first row that we lookup is the last limb. If it's not found in the last limb,

@jeanmon jeanmon Sep 24, 2025

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Suggested change
// The to radix gadget is little endian, so the first row that we lookup is the last limb. If it's not found in the last limb,
// The to_radix gadget is little endian, so the first row that we lookup is the last limb. If it's not found in the last limb,

// it means that the number is truncated with the given number of limbs.
sel_truncation_error = start * sel_should_decompose * (1 - value_found);

/////////////////////////////////////////////////////
// Error Handling - Consolidated error flag
/////////////////////////////////////////////////////
pol commit err;
err = start * (1 - (1 - input_validation_error) * (1 - sel_truncation_error));

/////////////////////////////////////////////////////
// Control flow management and terminating trace
/////////////////////////////////////////////////////
Expand Down Expand Up @@ -211,33 +255,25 @@ namespace to_radix_mem;
#[LAST_ROW_VALID_COMPUTATION]
NO_ERR_NOR_NUM_LIMBS_ZERO * (NUM_LIMBS_MINUS_ONE * (last * (1 - num_limbs_minus_one_inv) + num_limbs_minus_one_inv) - 1 + last) = 0;

/////////////////////////////////////////////////////
// Dispatch inputs to to_radix and retrieve outputs
/////////////////////////////////////////////////////
pol commit output_limb_value;
pol commit sel_should_exec;
// If the num limbs are zero, we don't dispatch to the gadget or write to memory.
sel_should_exec = sel * (1 - err) * (1 - sel_num_limbs_is_zero);

pol commit limb_index_to_lookup; // Need this since we want Big-Endian but the gadget is Little-Endian
limb_index_to_lookup = sel_should_exec * (num_limbs - 1);
#[INPUT_OUTPUT_TO_RADIX]
sel_should_exec { value_to_decompose, limb_index_to_lookup, radix, output_limb_value }
in
to_radix.sel {to_radix.value, to_radix.limb_index, to_radix.radix, to_radix.limb };

////////////////////////////////////////////////
// Write output to memory
////////////////////////////////////////////////
pol commit sel_should_write_mem;
// We compute sel_should_write_mem in the start row, as no error at all and num_limbs != 0.
start * ((1 - err) * (1 - sel_num_limbs_is_zero) - sel_should_write_mem) = 0;
// On following rows, we propagate sel_should_write_mem.
#[SEL_SHOULD_WRITE_MEM_CONTINUITY]
NOT_LAST * (sel_should_write_mem' - sel_should_write_mem) = 0;

pol commit output_tag;
// Conditional Assignment: is_output_bits ? U1 : U8
output_tag = sel_should_exec * ((constants.MEM_TAG_U1 - constants.MEM_TAG_U8) * is_output_bits + constants.MEM_TAG_U8);
output_tag = sel_should_write_mem * ((constants.MEM_TAG_U1 - constants.MEM_TAG_U8) * is_output_bits + constants.MEM_TAG_U8);

#[WRITE_MEM]
sel_should_exec {
sel_should_write_mem {
execution_clk, space_id,
dst_addr, output_limb_value,
/*mem_tag*/ output_tag, /*rw=1*/ sel_should_exec
/*mem_tag*/ output_tag, /*rw=1*/ sel_should_write_mem
} is
memory.sel_to_radix_write {
memory.clk, memory.space_id,
Expand Down
96 changes: 81 additions & 15 deletions barretenberg/cpp/src/barretenberg/vm2/constraining/relations/to_radix.test.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -447,8 +447,10 @@ TEST(ToRadixMemoryConstrainingTest, BasicTest)
{ C::to_radix_mem_value_inv, value.invert() },
// Output
{ C::to_radix_mem_output_limb_value, 1 },
{ C::to_radix_mem_sel_should_exec, 1 },
{ C::to_radix_mem_sel_should_decompose, 1 },
{ C::to_radix_mem_sel_should_write_mem, 1 },
{ C::to_radix_mem_limb_index_to_lookup, num_limbs - 1 },
{ C::to_radix_mem_value_found, 1 },
{ C::to_radix_mem_output_tag, static_cast<uint8_t>(MemoryTag::U8) },

// GT check - 2 > radix = false
Expand All @@ -474,7 +476,8 @@ TEST(ToRadixMemoryConstrainingTest, BasicTest)
{ C::to_radix_mem_num_limbs_minus_one_inv, FF(num_limbs - 2).invert() },
// Output
{ C::to_radix_mem_output_limb_value, 3 },
{ C::to_radix_mem_sel_should_exec, 1 },
{ C::to_radix_mem_sel_should_decompose, 1 },
{ C::to_radix_mem_sel_should_write_mem, 1 },
{ C::to_radix_mem_limb_index_to_lookup, num_limbs - 2 },
{ C::to_radix_mem_output_tag, static_cast<uint8_t>(MemoryTag::U8) },
// GT check - Radix > 256 = false
Expand All @@ -500,7 +503,8 @@ TEST(ToRadixMemoryConstrainingTest, BasicTest)
{ C::to_radix_mem_num_limbs_minus_one_inv, FF(num_limbs - 3).invert() },
// Output
{ C::to_radix_mem_output_limb_value, 3 },
{ C::to_radix_mem_sel_should_exec, 1 },
{ C::to_radix_mem_sel_should_decompose, 1 },
{ C::to_radix_mem_sel_should_write_mem, 1 },
{ C::to_radix_mem_limb_index_to_lookup, num_limbs - 3 },
{ C::to_radix_mem_output_tag, static_cast<uint8_t>(MemoryTag::U8) },
},
Expand All @@ -520,7 +524,8 @@ TEST(ToRadixMemoryConstrainingTest, BasicTest)
{ C::to_radix_mem_last, 1 },
// Output
{ C::to_radix_mem_output_limb_value, 7 },
{ C::to_radix_mem_sel_should_exec, 1 },
{ C::to_radix_mem_sel_should_decompose, 1 },
{ C::to_radix_mem_sel_should_write_mem, 1 },
{ C::to_radix_mem_limb_index_to_lookup, num_limbs - 4 },
{ C::to_radix_mem_output_tag, static_cast<uint8_t>(MemoryTag::U8) },
},
Expand Down Expand Up @@ -577,6 +582,16 @@ TEST(ToRadixMemoryConstrainingTest, BasicTest)

check_relation<to_radix_mem>(trace);
check_all_interactions<ToRadixTraceBuilder>(trace);

// Negative test: disable memory write after the start row:
trace.set(Column::to_radix_mem_sel_should_write_mem, 2, 0);
EXPECT_THROW_WITH_MESSAGE((check_relation<to_radix_mem>(trace, to_radix_mem::SR_SEL_SHOULD_WRITE_MEM_CONTINUITY)),
"SEL_SHOULD_WRITE_MEM_CONTINUITY");

// Negative test: disable decomposition after the start row:
trace.set(Column::to_radix_mem_sel_should_decompose, 2, 0);
EXPECT_THROW_WITH_MESSAGE((check_relation<to_radix_mem>(trace, to_radix_mem::SR_SEL_SHOULD_WRITE_MEM_CONTINUITY)),

@jeanmon jeanmon Sep 24, 2025

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think you want to test another relation or you need to "reset the trace", otherwise it is clear that the relation will fail again.

@sirasistant sirasistant Sep 24, 2025 •
edited
Loading

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Ah it's a typo. I meant to check the decompose selector continuity. will fix

"SEL_SHOULD_WRITE_MEM_CONTINUITY");
}

TEST(ToRadixMemoryConstrainingTest, DstOutOfRange)
Expand Down Expand Up @@ -626,6 +641,7 @@ TEST(ToRadixMemoryConstrainingTest, DstOutOfRange)
{ C::to_radix_mem_is_output_bits, 0 },
// Errors
{ C::to_radix_mem_sel_dst_out_of_range_err, 1 },
{ C::to_radix_mem_input_validation_error, 1 },
{ C::to_radix_mem_err, 1 },
// Control Flow
{ C::to_radix_mem_start, 1 },
Expand All @@ -636,8 +652,6 @@ TEST(ToRadixMemoryConstrainingTest, DstOutOfRange)
{ C::to_radix_mem_num_limbs_inv, FF(num_limbs).invert() },
{ C::to_radix_mem_sel_value_is_zero, 0 },
{ C::to_radix_mem_value_inv, value.invert() },
// Output
{ C::to_radix_mem_sel_should_exec, 0 },
},
});

Expand Down Expand Up @@ -683,6 +697,7 @@ TEST(ToRadixMemoryConstrainingTest, InvalidRadix)
{ C::to_radix_mem_is_output_bits, 0 },
// Errors
{ C::to_radix_mem_sel_radix_lt_2_err, 1 },
{ C::to_radix_mem_input_validation_error, 1 },
{ C::to_radix_mem_err, 1 },
// Control Flow
{ C::to_radix_mem_start, 1 },
Expand All @@ -693,8 +708,6 @@ TEST(ToRadixMemoryConstrainingTest, InvalidRadix)
{ C::to_radix_mem_num_limbs_inv, FF(num_limbs).invert() },
{ C::to_radix_mem_sel_value_is_zero, 0 },
{ C::to_radix_mem_value_inv, value.invert() },
// Output
{ C::to_radix_mem_sel_should_exec, 0 },
},
});
check_relation<to_radix_mem>(trace);
Expand Down Expand Up @@ -738,6 +751,7 @@ TEST(ToRadixMemoryConstrainingTest, InvalidBitwiseRadix)
{ C::to_radix_mem_is_output_bits, is_output_bits ? 1 : 0 },
// Errors
{ C::to_radix_mem_sel_invalid_bitwise_radix, 1 }, // Invalid bitwise radix
{ C::to_radix_mem_input_validation_error, 1 },
{ C::to_radix_mem_err, 1 },
// Control Flow
{ C::to_radix_mem_start, 1 },
Expand All @@ -748,8 +762,6 @@ TEST(ToRadixMemoryConstrainingTest, InvalidBitwiseRadix)
{ C::to_radix_mem_num_limbs_inv, FF(num_limbs).invert() },
{ C::to_radix_mem_sel_value_is_zero, 0 },
{ C::to_radix_mem_value_inv, value.invert() },
// Output
{ C::to_radix_mem_sel_should_exec, 0 },
},
});
check_relation<to_radix_mem>(trace);
Expand Down Expand Up @@ -793,6 +805,7 @@ TEST(ToRadixMemoryConstrainingTest, InvalidNumLimbsForValue)
{ C::to_radix_mem_is_output_bits, is_output_bits ? 1 : 0 },
// Errors
{ C::to_radix_mem_sel_invalid_num_limbs_err, 1 }, // num_limbs should not be 0 if value != 0
{ C::to_radix_mem_input_validation_error, 1 },
{ C::to_radix_mem_err, 1 },
// Control Flow
{ C::to_radix_mem_start, 1 },
Expand All @@ -803,8 +816,63 @@ TEST(ToRadixMemoryConstrainingTest, InvalidNumLimbsForValue)
{ C::to_radix_mem_num_limbs_inv, 0 },
{ C::to_radix_mem_sel_value_is_zero, 0 },
{ C::to_radix_mem_value_inv, value.invert() },
// Output
{ C::to_radix_mem_sel_should_exec, 0 },
},
});
check_relation<to_radix_mem>(trace);
check_interaction<ToRadixTraceBuilder, lookup_to_radix_mem_check_radix_lt_2_settings>(trace);
}

TEST(ToRadixMemoryConstrainingTest, TruncationError)

@jeanmon jeanmon Sep 24, 2025

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Can we craft a negative test like setting the truncation error while everything is fine and/or the othe way around the error is not toggled when it should?

@sirasistant sirasistant Sep 24, 2025

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

done!

{
// Values
FF value = FF(1337);
uint32_t radix = 10;
uint32_t num_limbs = 3;
uint32_t dst_addr = 10;
bool is_output_bits = false;

TestTraceContainer trace = TestTraceContainer({
// Row 0
{
{ C::precomputed_first_row, 1 },
// GT check
{ C::gt_sel, 1 },
{ C::gt_input_a, 2 },
{ C::gt_input_b, radix },
{ C::gt_res, 0 }, // GT should return false
},
// Row 1
{
{ C::to_radix_mem_sel, 1 },
{ C::to_radix_mem_max_mem_addr, AVM_HIGHEST_MEM_ADDRESS },
{ C::to_radix_mem_two, 2 },
{ C::to_radix_mem_two_five_six, 256 },
// Memory Inputs
{ C::to_radix_mem_execution_clk, 0 },
{ C::to_radix_mem_space_id, 0 },
{ C::to_radix_mem_dst_addr, dst_addr },
{ C::to_radix_mem_max_write_addr, dst_addr + num_limbs - 1 },
// To Radix Inputs
{ C::to_radix_mem_value_to_decompose, value },
{ C::to_radix_mem_radix, radix },
{ C::to_radix_mem_num_limbs, num_limbs },
{ C::to_radix_mem_is_output_bits, is_output_bits ? 1 : 0 },
// Errors
{ C::to_radix_mem_sel_truncation_error, 1 }, // found = false on the last le limb
{ C::to_radix_mem_err, 1 },
// Control Flow
{ C::to_radix_mem_start, 1 },
{ C::to_radix_mem_last, 1 },
{ C::to_radix_mem_num_limbs_minus_one_inv, num_limbs - 1 == 0 ? 0 : FF(num_limbs - 1).invert() },
// Decomposition
{ C::to_radix_mem_sel_should_decompose, 1 },
{ C::to_radix_mem_limb_index_to_lookup, num_limbs - 1 },
{ C::to_radix_mem_output_limb_value, 3 },
{ C::to_radix_mem_value_found, 0 },
// Helpers
{ C::to_radix_mem_num_limbs_inv, FF(num_limbs).invert() },
{ C::to_radix_mem_sel_value_is_zero, 0 },
{ C::to_radix_mem_value_inv, value.invert() },
},
});
check_relation<to_radix_mem>(trace);
Expand Down Expand Up @@ -855,8 +923,6 @@ TEST(ToRadixMemoryConstrainingTest, ZeroNumLimbsAndZeroValueIsNoop)
{ C::to_radix_mem_num_limbs_inv, 0 },
{ C::to_radix_mem_sel_value_is_zero, 1 },
{ C::to_radix_mem_value_inv, 0 },
// Output
{ C::to_radix_mem_sel_should_exec, 0 }, // Should still not_exec since num_limbs == 0
},
});
check_relation<to_radix_mem>(trace);
Expand Down Expand Up @@ -886,7 +952,7 @@ TEST(ToRadixMemoryConstrainingTest, ComplexTest)
// Two calls to test transitions between contiguous chunks of computation
to_radix_simulator.to_be_radix(memory, value, radix, num_limbs, is_output_bits, dst_addr);
to_radix_simulator.to_be_radix(
memory, /*value=*/FF(1337), /*radix=*/10, /*num_limbs=*/2, /*is_output_bits=*/false, /*dst_addr=*/0xdeadbeef);
memory, /*value=*/FF(1337), /*radix=*/10, /*num_limbs=*/6, /*is_output_bits=*/false, /*dst_addr=*/0xdeadbeef);

TestTraceContainer trace;
ToRadixTraceBuilder builder;
Expand Down
Loading
Loading