feat(avm): range checks in vm2 #11433

dbanks12 · 2025-01-23T01:55:46Z

Also sel_rng_chk_8/16 and power_of_2 precomputed tables

dbanks12 · 2025-01-23T01:56:01Z

feat(avm): range checks in vm2 #11433 👈 (View in Graphite)
master

This stack of pull requests is managed by Graphite. Learn more about stacking.

dbanks12 · 2025-01-23T01:57:22Z

barretenberg/cpp/pil/vm2/range_check.pil

Copied this file over but renamed some things and removed the selectors specifying which subtrace a range check originated from

dbanks12 · 2025-01-23T02:03:30Z

barretenberg/cpp/pil/vm2/execution.pil

-sel {op1, op2, op3, op4} is sel {op1, op2, op3, op4};
+sel {op1, op2, op3, op4} is sel {op1, op2, op3, op4};


I don't know what's different about our editors, but this happens all the time

dbanks12 · 2025-01-23T02:05:48Z

barretenberg/cpp/src/barretenberg/vm2/simulation/range_check.test.cpp

+TEST(AvmSimulationRangeCheckTest, AssertRange)
+{
+    EventEmitter<RangeCheckEvent> emitter;
+    RangeCheck range_check(emitter);
+
+    uint128_t value = 333;
+    uint8_t num_bits = 100;
+    range_check.assert_range(value, num_bits);
+
+    RangeCheckEvent expect_event = {
+        .value = value,
+        .num_bits = num_bits,
+    };
+
+    std::vector<RangeCheckEvent> events = { expect_event };
+    EXPECT_EQ(emitter.dump_events(), events);
+}


This test feels like it's doing... nothing. But I guess the range-check simulation module does just about nothing since it is really a tracegen thing.

Yeah indeed. It's such a simple gadget (simulation wise) that it doesnt even call anything else.

dbanks12 · 2025-01-23T02:06:25Z

barretenberg/cpp/src/barretenberg/vm2/tracegen/range_check_trace.cpp

+    uint32_t row = 0;
+    for (const auto& event : events) {
+        uint256_t value_u256 = uint256_t::from_uint128(event.value);
+        uint8_t num_bits = 0;
+
+        std::array<uint16_t, 7> fixed_slice_registers; // u16_r0...6
+        // Enum representing which of is_lte_u* holds true.
+        // Only one can be chosen/true for a given range check.
+        // The highest X is chosen such that "value is lte X" holds true.
+        IsLte is_lte = IsLte::IS_LTE_U16;
+        uint16_t dynamic_slice_register = 0; // same as u16_r7
+        uint16_t dynamic_bits = 0;
+
+        // Split the value into 16-bit chunks
+        for (size_t i = 0; i < 8; i++) {
+            // The most significant 16-bits have to be placed in the dynamic slice register
+            if (event.num_bits <= 16) {
+                dynamic_slice_register = static_cast<uint16_t>(value_u256);
+                // Set is_lte based on on how many 16 bit chunks have already been processed
+                // For example, if this is the 0th, then IS_LTE_U16 is set
+                // If this is the first, then IS_LTE_U32 is set, ...
+                // TODO(dbanks12): is this more or less intuitive then the bit magic from before?
+                is_lte = IsLte(i);
+                dynamic_bits = event.num_bits;
+                break;
+            }
+            // We have more chunks of 16-bits to operate on, so set the ith fixed register
+            fixed_slice_registers[i] = static_cast<uint16_t>(value_u256);
+            num_bits -= 16;
+            value_u256 >>= 16;
+        }
+
+        auto dynamic_diff = static_cast<uint16_t>((1 << dynamic_bits) - dynamic_slice_register - 1);


See my TODO here

dbanks12 · 2025-01-23T02:07:26Z

barretenberg/cpp/src/barretenberg/vm2/simulation/events/range_check_event.hpp

+struct RangeCheckEvent {
+    uint128_t value;
+    uint8_t num_bits;
+
+    // TODO(dbanks12): do we want this operator just for tests?
+    bool operator==(const RangeCheckEvent& other) const { return value == other.value && num_bits == other.num_bits; }
+};


See TODO. The simple test for this event uses this operator== to do checks. But maybe it's unnecessary?

fcarreiro

Looking great from a VM2 perspective!

fcarreiro · 2025-01-23T09:20:29Z

barretenberg/cpp/pil/vm2/range_check.pil

@@ -0,0 +1,189 @@
+namespace range_check(256);
+    // Range check selector
+    pol commit sel_rng_chk;


We are now just using sel for the subtrace selector so that it looks like range_check.sel when the namespace is used.

fcarreiro · 2025-01-23T09:21:30Z

barretenberg/cpp/pil/vm2/range_check.pil

+    sel_r5_16_bit_rng_lookup - (is_lte_u112 + is_lte_u128) = 0;
+    sel_r6_16_bit_rng_lookup - is_lte_u128 = 0;
+
+    #[LOOKUP_RNG_CHK_IS_R0_16_BIT]


These interactions were not supposed to happen :) but I was about to propose that we can start doing lookups into precomputed (and only precomputed). So let's keep them and make them work :)

fcarreiro · 2025-01-23T09:22:22Z

barretenberg/cpp/src/barretenberg/vm2/constraining/relations/alu.test.cpp

[Re: line +57]

Revert pls

See this comment inline on Graphite.

fcarreiro · 2025-01-23T09:22:57Z

barretenberg/cpp/src/barretenberg/vm2/constraining/relations/range_check.test.cpp

+
+TEST(AvmConstrainingTest, RangeCheckNegativeCheckRecomposition)
+{
+


nit: Please remove these extra new lines

fcarreiro · 2025-01-23T09:26:44Z

barretenberg/cpp/src/barretenberg/vm2/constraining/relations/range_check.test.cpp

+        { C::range_check_sel_r1_16_bit_rng_lookup, 0 }, // BAD! SHOULD BE 1
+    } });
+
+    EXPECT_THROW_WITH_MESSAGE(check_relation<range_check>(trace.as_rows()), "Relation range_check");


Negative tests should probably be more granular (non full); if sth else starts failing, this statement will pass. See other negative tests. Probably you want to check a given subrelation(s).

fcarreiro · 2025-01-23T09:35:25Z

barretenberg/cpp/src/barretenberg/vm2/tracegen/range_check_trace.cpp

+{
+    using C = Column;
+
+    uint32_t row = 0;


Do you use any shifts (') in pil? If yes you have to start from 1, otherwise it's ok.

fcarreiro · 2025-01-23T09:36:31Z

barretenberg/cpp/src/barretenberg/vm2/tracegen/range_check_trace.cpp

+                      { C::range_check_dyn_rng_chk_bits, dynamic_bits },
+                      { C::range_check_dyn_rng_chk_pow_2, 1 << dynamic_bits },
+                      { C::range_check_dyn_diff, dynamic_diff },
+


Maybe a comment if you want to separate them, e.g.
// Lookups.

fcarreiro · 2025-01-23T09:37:22Z

barretenberg/cpp/src/barretenberg/vm2/tracegen_helper.cpp

+        [&]() {
+            PrecomputedTraceBuilder precomputed_builder;
+            AVM_TRACK_TIME("tracegen/precomputed/rng_chk_8", precomputed_builder.process_sel_rng_chk_8(trace));
+        },
+        [&]() {
+            PrecomputedTraceBuilder precomputed_builder;
+            AVM_TRACK_TIME("tracegen/precomputed/rng_chk_16", precomputed_builder.process_sel_rng_chk_16(trace));
+        },
+        [&]() {
+            PrecomputedTraceBuilder precomputed_builder;
+            AVM_TRACK_TIME("tracegen/precomputed/power_of_2", precomputed_builder.process_power_of_2(trace));
+        },


These are so cheap that I'd put the 3 of them in the same job.

fcarreiro · 2025-01-23T09:37:45Z

barretenberg/cpp/src/barretenberg/vm2/tracegen_helper.cpp

@@ -122,6 +146,46 @@ TraceContainer AvmTraceGenHelper::generate_trace(EventsContainer&& events)
                PermutationBuilder<perm_dummy_dynamic_permutation_settings> perm_execution_execution;
                perm_execution_execution.process(trace);
            },
+            [&]() {


perfect 👍

fcarreiro · 2025-01-23T09:40:27Z

barretenberg/cpp/src/barretenberg/vm2/tracegen/lib/lookup_into_rng_chk.hpp

+
+namespace bb::avm2::tracegen {
+
+template <typename LookupSettings> class LookupIntoRngChk : public BaseLookupTraceBuilder<LookupSettings> {


Ah interesting! You were able to use the same class for lookups into u8, u16 etc, because they all use CLK and only change based on the selector. Maybe add a comment?

fcarreiro · 2025-01-23T12:40:27Z

barretenberg/cpp/pil/vm2/range_check.pil

+    // Range check selector
+    pol commit sel_rng_chk;
+    sel_rng_chk * (1 - sel_rng_chk) = 0;
+


Could you add

// No relations will be checked if this identity is satisfied. #[skippable_if] sel = 0;

?

we can discuss skippable in a huddle

fcarreiro · 2025-01-23T12:52:07Z

barretenberg/cpp/src/barretenberg/vm2/constraining/relations/range_check.test.cpp

+using C = Column;
+using range_check = bb::avm2::range_check<FF>;
+
+TEST(AvmConstrainingTest, RangeCheckPositiveIsLteMutuallyExclusive)


Could you add a test where you

create a single row with clk = 1. this is to force a row to be in the trace. I actually want a completely empty row but it doesnt matter.

check the whole relation and expect no failures
?

This is to test that all relations pass in rows fulls of 0. We probably need to add this test to every gadget.

dbanks12 commented Jan 23, 2025

View reviewed changes

feat(avm): range checks in vm2

834e682

dbanks12 force-pushed the db/range-checks-vm2 branch from 9e6df37 to 834e682 Compare January 23, 2025 02:02

dbanks12 commented Jan 23, 2025

View reviewed changes

fcarreiro reviewed Jan 23, 2025

View reviewed changes

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

feat(avm): range checks in vm2 #11433

feat(avm): range checks in vm2 #11433

dbanks12 commented Jan 23, 2025 •

edited

Loading

dbanks12 commented Jan 23, 2025

dbanks12 Jan 23, 2025

dbanks12 Jan 23, 2025

dbanks12 Jan 23, 2025

fcarreiro Jan 23, 2025

dbanks12 Jan 23, 2025

dbanks12 Jan 23, 2025

fcarreiro left a comment

fcarreiro Jan 23, 2025

fcarreiro Jan 23, 2025

fcarreiro Jan 23, 2025

fcarreiro Jan 23, 2025

fcarreiro Jan 23, 2025

fcarreiro Jan 23, 2025

fcarreiro Jan 23, 2025

fcarreiro Jan 23, 2025

fcarreiro Jan 23, 2025

fcarreiro Jan 23, 2025

fcarreiro Jan 23, 2025

fcarreiro Jan 23, 2025

		sel {op1, op2, op3, op4} is sel {op1, op2, op3, op4}; No newline at end of file
		sel {op1, op2, op3, op4} is sel {op1, op2, op3, op4};


		TEST(AvmConstrainingTest, RangeCheckNegativeCheckRecomposition)
		{


		namespace bb::avm2::tracegen {

		template <typename LookupSettings> class LookupIntoRngChk : public BaseLookupTraceBuilder<LookupSettings> {

feat(avm): range checks in vm2 #11433

Are you sure you want to change the base?

feat(avm): range checks in vm2 #11433

Conversation

dbanks12 commented Jan 23, 2025 • edited Loading

dbanks12 commented Jan 23, 2025

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

fcarreiro left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

dbanks12 commented Jan 23, 2025 •

edited

Loading