Skip to content

Commit

Permalink
Cleanup after feedback
Browse files Browse the repository at this point in the history
  • Loading branch information
@dbanks12
dbanks12 committed Jan 24, 2025
1 parent 834e682 commit c4812be
Show file tree
Hide file tree
Showing 27 changed files with 389 additions and 198 deletions.
4 changes: 2 additions & 2 deletions barretenberg/cpp/pil/vm2/precomputed.pil
View file
Original file line number Diff line number Diff line change
Expand Up @@ -18,8 +18,8 @@ pol constant bitwise_output; // output = a AND/OR/XOR b.

// Boolean selectors for 8-bit and 16-bit range checks.
// We reuse clk for the actual values.
pol constant sel_rng_chk_8; // 1 in the first 2^8 rows
pol constant sel_rng_chk_16; // 1 in the first 2^16 rows
pol constant sel_range_8; // 1 in the first 2^8 rows
pol constant sel_range_16; // 1 in the first 2^16 rows

// All the powers of 2 from 0 to 256
// For a given row, the exponent is clk (value = 2^clk)
Expand Down
38 changes: 21 additions & 17 deletions barretenberg/cpp/pil/vm2/range_check.pil
View file
Original file line number Diff line number Diff line change
@@ -1,7 +1,11 @@
namespace range_check(256);
// Range check selector
pol commit sel_rng_chk;
sel_rng_chk * (1 - sel_rng_chk) = 0;
pol commit sel;
sel * (1 - sel) = 0;
// No relations will be checked if this identity is satisfied.
#[skippable_if]
sel = 0;


// Witnesses
// Value to range check
Expand All @@ -14,7 +18,7 @@ namespace range_check(256);
// e.g., rng_chk_bits = 10 ===> is_lte_u16, rng_chk_bits = 100 ==> is_lte_u112
// If rng_chk_bits is a multiple of 16, a prover is able to choose either is_lte_xx or is_lte_xx(+16), since the dynamic register will prove 0
// This isn't a concern and only costs the prover additional compute.
// TODO: Maybe we can get rid of is_lte_u128 since it's implicit if we have sel_rng_chk and no other is_lte_x
// TODO: Maybe we can get rid of is_lte_u128 since it's implicit if we have sel and no other is_lte_x
pol commit is_lte_u16;
pol commit is_lte_u32;
pol commit is_lte_u48;
Expand All @@ -34,7 +38,7 @@ namespace range_check(256);

// Mutual Exclusivity condition
#[IS_LTE_MUTUALLY_EXCLUSIVE]
is_lte_u16 + is_lte_u32 + is_lte_u48 + is_lte_u64 + is_lte_u80 + is_lte_u96 + is_lte_u112 + is_lte_u128 = sel_rng_chk;
is_lte_u16 + is_lte_u32 + is_lte_u48 + is_lte_u64 + is_lte_u80 + is_lte_u96 + is_lte_u112 + is_lte_u128 = sel;

// Eight 16-bit slice registers
pol commit u16_r0;
Expand Down Expand Up @@ -64,7 +68,7 @@ namespace range_check(256);

// Enforce that value can be derived from whichever slice registers are activated by an is_lte flag
#[CHECK_RECOMPOSITION]
sel_rng_chk * (RESULT - value) = 0;
sel * (RESULT - value) = 0;

// ===== Dynamic Check Constraints =====

Expand Down Expand Up @@ -130,18 +134,18 @@ namespace range_check(256);

// This lookup does 2 things (1) Indirectly range checks dyn_rng_chk_bits to not have underflowed and (2) Simplified calculation of 2^dyn_rng_chk_bits
#[LOOKUP_RNG_CHK_POW_2]
sel_rng_chk {dyn_rng_chk_bits, dyn_rng_chk_pow_2} in precomputed.sel_rng_chk_8 {precomputed.clk, precomputed.power_of_2};
// NOTE: `sel_rng_chk_8` is chosen because it gives us rows [0, 256] which will give us all of the powers we need (plus many we don't need)
sel {dyn_rng_chk_bits, dyn_rng_chk_pow_2} in precomputed.sel_range_8 {precomputed.clk, precomputed.power_of_2};
// NOTE: `sel_range_8` is chosen because it gives us rows [0, 256] which will give us all of the powers we need (plus many we don't need)


// Now we need to perform the dynamic range check itself
// We check that u16_r7 < dyn_rng_chk_pow_2 ==> dyn_rng_chk_pow_2 - u16_r7 - 1 >= 0
pol commit dyn_diff;
sel_rng_chk * (dyn_diff - (dyn_rng_chk_pow_2 - u16_r7 - 1)) = 0;
sel * (dyn_diff - (dyn_rng_chk_pow_2 - u16_r7 - 1)) = 0;
// The value of dyn_diff has to be between [0, 2^16)
// To check we did not underflow we just range check it
#[LOOKUP_RNG_CHK_DIFF]
sel_rng_chk { dyn_diff } in precomputed.sel_rng_chk_16 { precomputed.clk };
sel { dyn_diff } in precomputed.sel_range_16 { precomputed.clk };


// Lookup relations.
Expand All @@ -165,25 +169,25 @@ namespace range_check(256);
sel_r6_16_bit_rng_lookup - is_lte_u128 = 0;

#[LOOKUP_RNG_CHK_IS_R0_16_BIT]
sel_r0_16_bit_rng_lookup { u16_r0 } in precomputed.sel_rng_chk_16 { precomputed.clk };
sel_r0_16_bit_rng_lookup { u16_r0 } in precomputed.sel_range_16 { precomputed.clk };

#[LOOKUP_RNG_CHK_IS_R1_16_BIT]
sel_r1_16_bit_rng_lookup { u16_r1 } in precomputed.sel_rng_chk_16 { precomputed.clk };
sel_r1_16_bit_rng_lookup { u16_r1 } in precomputed.sel_range_16 { precomputed.clk };

#[LOOKUP_RNG_CHK_IS_R2_16_BIT]
sel_r2_16_bit_rng_lookup { u16_r2 } in precomputed.sel_rng_chk_16 { precomputed.clk };
sel_r2_16_bit_rng_lookup { u16_r2 } in precomputed.sel_range_16 { precomputed.clk };

#[LOOKUP_RNG_CHK_IS_R3_16_BIT]
sel_r3_16_bit_rng_lookup { u16_r3 } in precomputed.sel_rng_chk_16 { precomputed.clk };
sel_r3_16_bit_rng_lookup { u16_r3 } in precomputed.sel_range_16 { precomputed.clk };

#[LOOKUP_RNG_CHK_IS_R4_16_BIT]
sel_r4_16_bit_rng_lookup { u16_r4 } in precomputed.sel_rng_chk_16 { precomputed.clk };
sel_r4_16_bit_rng_lookup { u16_r4 } in precomputed.sel_range_16 { precomputed.clk };

#[LOOKUP_RNG_CHK_IS_R5_16_BIT]
sel_r5_16_bit_rng_lookup { u16_r5 } in precomputed.sel_rng_chk_16 { precomputed.clk };
sel_r5_16_bit_rng_lookup { u16_r5 } in precomputed.sel_range_16 { precomputed.clk };

#[LOOKUP_RNG_CHK_IS_R6_16_BIT]
sel_r6_16_bit_rng_lookup { u16_r6 } in precomputed.sel_rng_chk_16 { precomputed.clk };
sel_r6_16_bit_rng_lookup { u16_r6 } in precomputed.sel_range_16 { precomputed.clk };

#[LOOKUP_RNG_CHK_IS_R7_16_BIT]
sel_rng_chk { u16_r7 } in precomputed.sel_rng_chk_16 { precomputed.clk };
sel { u16_r7 } in precomputed.sel_range_16 { precomputed.clk };
2 changes: 1 addition & 1 deletion barretenberg/cpp/src/barretenberg/vm2/constraining/relations/alu.test.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -53,4 +53,4 @@ TEST(AvmConstrainingTest, AluNegativeAdd)
}

} // namespace
} // namespace bb::avm2::constraining
} // namespace bb::avm2::constraining
77 changes: 66 additions & 11 deletions barretenberg/cpp/src/barretenberg/vm2/constraining/relations/range_check.test.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -8,20 +8,31 @@
#include "barretenberg/vm2/generated/flavor_settings.hpp"
#include "barretenberg/vm2/generated/relations/range_check.hpp"
#include "barretenberg/vm2/testing/macros.hpp"
#include "barretenberg/vm2/tracegen/range_check_trace.hpp"
#include "barretenberg/vm2/tracegen/test_trace_container.hpp"

namespace bb::avm2::constraining {
namespace {

using tracegen::RangeCheckTraceBuilder;
using tracegen::TestTraceContainer;
using FF = AvmFlavorSettings::FF;
using C = Column;
using range_check = bb::avm2::range_check<FF>;

TEST(AvmConstrainingTest, RangeCheckPositiveEmptyRow)
{
TestTraceContainer trace({
{ { C::precomputed_clk, 1 } },
});

check_relation<range_check>(trace.as_rows());
}

TEST(AvmConstrainingTest, RangeCheckPositiveIsLteMutuallyExclusive)
{
TestTraceContainer trace({
{ { C::range_check_sel_rng_chk, 1 }, { C::range_check_is_lte_u32, 1 } },
{ { C::range_check_sel, 1 }, { C::range_check_is_lte_u32, 1 } },
});

check_relation<range_check>(trace.as_rows(), range_check::SR_IS_LTE_MUTUALLY_EXCLUSIVE);
Expand All @@ -31,7 +42,7 @@ TEST(AvmConstrainingTest, RangeCheckNegativeIsLteMutuallyExclusive)
{
TestTraceContainer trace({
// Negative test, only one is_lte flag should be high
{ { C::range_check_sel_rng_chk, 1 }, { C::range_check_is_lte_u32, 1 }, { C::range_check_is_lte_u112, 1 } },
{ { C::range_check_sel, 1 }, { C::range_check_is_lte_u32, 1 }, { C::range_check_is_lte_u112, 1 } },
});

EXPECT_THROW_WITH_MESSAGE(check_relation<range_check>(trace.as_rows(), range_check::SR_IS_LTE_MUTUALLY_EXCLUSIVE),
Expand All @@ -40,7 +51,6 @@ TEST(AvmConstrainingTest, RangeCheckNegativeIsLteMutuallyExclusive)

TEST(AvmConstrainingTest, RangeCheckPositiveCheckRecomposition)
{

uint128_t value = 0x3FFFFFFFD;
uint256_t value_u256 = uint256_t::from_uint128(value);

Expand All @@ -49,7 +59,7 @@ TEST(AvmConstrainingTest, RangeCheckPositiveCheckRecomposition)
uint16_t dynamic_slice_register = 0x0003; // (value >> 32) & 0xFFFF;

TestTraceContainer trace({ {
{ C::range_check_sel_rng_chk, 1 },
{ C::range_check_sel, 1 },
{ C::range_check_value, value_u256 },
{ C::range_check_is_lte_u48, 1 },
{ C::range_check_u16_r0, u16_r0 },
Expand All @@ -62,7 +72,6 @@ TEST(AvmConstrainingTest, RangeCheckPositiveCheckRecomposition)

TEST(AvmConstrainingTest, RangeCheckNegativeCheckRecomposition)
{

uint128_t value = 0x3FFFFFFFD;
// Add 1 to the value to create a "bad" value that doesn't match recomposition
uint256_t bad_value = uint256_t::from_uint128(value + 1);
Expand All @@ -72,7 +81,7 @@ TEST(AvmConstrainingTest, RangeCheckNegativeCheckRecomposition)
uint16_t dynamic_slice_register = (value >> 32) & 0xFFFF;

TestTraceContainer trace({ {
{ C::range_check_sel_rng_chk, 1 },
{ C::range_check_sel, 1 },
{ C::range_check_value, bad_value },
{ C::range_check_is_lte_u48, 1 },
{ C::range_check_u16_r0, u16_r0 },
Expand All @@ -86,7 +95,6 @@ TEST(AvmConstrainingTest, RangeCheckNegativeCheckRecomposition)

TEST(AvmConstrainingTest, RangeCheckPositiveFull)
{

uint8_t num_bits = 34;
uint8_t non_dynamic_bits = 32;
uint8_t dynamic_bits = num_bits - non_dynamic_bits;
Expand All @@ -103,7 +111,7 @@ TEST(AvmConstrainingTest, RangeCheckPositiveFull)
uint16_t dynamic_diff = static_cast<uint16_t>(dynamic_bits_pow_2 - dynamic_slice_register - 1);

TestTraceContainer trace({ {
{ C::range_check_sel_rng_chk, 1 },
{ C::range_check_sel, 1 },
{ C::range_check_value, value_u256 },
{ C::range_check_rng_chk_bits, num_bits },
{ C::range_check_is_lte_u48, 1 },
Expand All @@ -121,9 +129,8 @@ TEST(AvmConstrainingTest, RangeCheckPositiveFull)
check_relation<range_check>(trace.as_rows());
}

TEST(AvmConstrainingTest, RangeCheckNegativeFull)
TEST(AvmConstrainingTest, RangeCheckNegativeMissingLookup)
{

uint8_t num_bits = 34;
uint8_t non_dynamic_bits = 32;
uint8_t dynamic_bits = num_bits - non_dynamic_bits;
Expand All @@ -140,7 +147,7 @@ TEST(AvmConstrainingTest, RangeCheckNegativeFull)
uint16_t dynamic_diff = static_cast<uint16_t>(dynamic_bits_pow_2 - dynamic_slice_register - 1);

TestTraceContainer trace({ {
{ C::range_check_sel_rng_chk, 1 },
{ C::range_check_sel, 1 },
{ C::range_check_value, value_u256 },
{ C::range_check_rng_chk_bits, num_bits },
{ C::range_check_is_lte_u48, 1 },
Expand All @@ -158,5 +165,53 @@ TEST(AvmConstrainingTest, RangeCheckNegativeFull)
EXPECT_THROW_WITH_MESSAGE(check_relation<range_check>(trace.as_rows()), "Relation range_check");
}

TEST(AvmConstrainingTest, RangeCheckPositiveWithTracegen)
{
TestTraceContainer trace;
RangeCheckTraceBuilder builder;

builder.process(
{
{ .value = 0, .num_bits = 0 },
{ .value = 0, .num_bits = 1 },
{ .value = 0, .num_bits = 16 },
{ .value = 2, .num_bits = 2 },
{ .value = 255, .num_bits = 8 },
{ .value = 1 << 16, .num_bits = 17 },
{ .value = 1 << 18, .num_bits = 32 },
{ .value = static_cast<uint128_t>(1) << 66, .num_bits = 67 },
{ .value = 1024, .num_bits = 109 },
{ .value = 1, .num_bits = 128 },
{ .value = 0xFFFFFFFFFFFFFFFF, .num_bits = 128 },
{ .value = 0x1FFF, .num_bits = 13 },
},
trace);

check_relation<range_check>(trace.as_rows());
}

TEST(AvmConstrainingTest, RangeCheckNegativeWithTracegen)
{
TestTraceContainer trace;
RangeCheckTraceBuilder builder;

builder.process(
{
{ .value = 1, .num_bits = 0 },
{ .value = 2, .num_bits = 1 },
{ .value = 255, .num_bits = 7 },
{ .value = 1 << 16, .num_bits = 16 },
{ .value = 1 << 18, .num_bits = 18 },
{ .value = static_cast<uint128_t>(1) << 66, .num_bits = 66 },
{ .value = 1024, .num_bits = 9 },
{ .value = 1, .num_bits = 0 },
{ .value = 0xFFFFFFFFFFFFFFFF, .num_bits = 127 },
{ .value = 0x1FFF, .num_bits = 12 },
},
trace);

EXPECT_THROW_WITH_MESSAGE(check_relation<range_check>(trace.as_rows()), "Relation range_check");
}

} // namespace
} // namespace bb::avm2::constraining
4 changes: 2 additions & 2 deletions barretenberg/cpp/src/barretenberg/vm2/generated/columns.hpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -9,8 +9,8 @@ namespace bb::avm2 {

// The entities that will be used in the flavor.
// clang-format off
#define AVM2_PRECOMPUTED_ENTITIES precomputed_bitwise_input_a, precomputed_bitwise_input_b, precomputed_bitwise_op_id, precomputed_bitwise_output, precomputed_clk, precomputed_first_row, precomputed_power_of_2, precomputed_sel_bitwise, precomputed_sel_rng_chk_16, precomputed_sel_rng_chk_8
#define AVM2_WIRE_ENTITIES execution_input, alu_dst_addr, alu_ia, alu_ia_addr, alu_ib, alu_ib_addr, alu_ic, alu_op, alu_sel_op_add, execution_addressing_error_idx, execution_addressing_error_kind, execution_base_address_tag, execution_base_address_val, execution_bytecode_id, execution_clk, execution_ex_opcode, execution_indirect, execution_last, execution_op1, execution_op1_after_relative, execution_op2, execution_op2_after_relative, execution_op3, execution_op3_after_relative, execution_op4, execution_op4_after_relative, execution_pc, execution_rop1, execution_rop2, execution_rop3, execution_rop4, execution_sel, execution_sel_addressing_error, execution_sel_op1_is_address, execution_sel_op2_is_address, execution_sel_op3_is_address, execution_sel_op4_is_address, range_check_dyn_diff, range_check_dyn_rng_chk_bits, range_check_dyn_rng_chk_pow_2, range_check_is_lte_u112, range_check_is_lte_u128, range_check_is_lte_u16, range_check_is_lte_u32, range_check_is_lte_u48, range_check_is_lte_u64, range_check_is_lte_u80, range_check_is_lte_u96, range_check_rng_chk_bits, range_check_sel_r0_16_bit_rng_lookup, range_check_sel_r1_16_bit_rng_lookup, range_check_sel_r2_16_bit_rng_lookup, range_check_sel_r3_16_bit_rng_lookup, range_check_sel_r4_16_bit_rng_lookup, range_check_sel_r5_16_bit_rng_lookup, range_check_sel_r6_16_bit_rng_lookup, range_check_sel_rng_chk, range_check_u16_r0, range_check_u16_r1, range_check_u16_r2, range_check_u16_r3, range_check_u16_r4, range_check_u16_r5, range_check_u16_r6, range_check_u16_r7, range_check_value, lookup_rng_chk_pow_2_counts, lookup_rng_chk_diff_counts, lookup_rng_chk_is_r0_16_bit_counts, lookup_rng_chk_is_r1_16_bit_counts, lookup_rng_chk_is_r2_16_bit_counts, lookup_rng_chk_is_r3_16_bit_counts, lookup_rng_chk_is_r4_16_bit_counts, lookup_rng_chk_is_r5_16_bit_counts, lookup_rng_chk_is_r6_16_bit_counts, lookup_rng_chk_is_r7_16_bit_counts, lookup_dummy_precomputed_counts, lookup_dummy_dynamic_counts
#define AVM2_PRECOMPUTED_ENTITIES precomputed_bitwise_input_a, precomputed_bitwise_input_b, precomputed_bitwise_op_id, precomputed_bitwise_output, precomputed_clk, precomputed_first_row, precomputed_power_of_2, precomputed_sel_bitwise, precomputed_sel_range_16, precomputed_sel_range_8
#define AVM2_WIRE_ENTITIES execution_input, alu_dst_addr, alu_ia, alu_ia_addr, alu_ib, alu_ib_addr, alu_ic, alu_op, alu_sel_op_add, execution_addressing_error_idx, execution_addressing_error_kind, execution_base_address_tag, execution_base_address_val, execution_bytecode_id, execution_clk, execution_ex_opcode, execution_indirect, execution_last, execution_op1, execution_op1_after_relative, execution_op2, execution_op2_after_relative, execution_op3, execution_op3_after_relative, execution_op4, execution_op4_after_relative, execution_pc, execution_rop1, execution_rop2, execution_rop3, execution_rop4, execution_sel, execution_sel_addressing_error, execution_sel_op1_is_address, execution_sel_op2_is_address, execution_sel_op3_is_address, execution_sel_op4_is_address, range_check_dyn_diff, range_check_dyn_rng_chk_bits, range_check_dyn_rng_chk_pow_2, range_check_is_lte_u112, range_check_is_lte_u128, range_check_is_lte_u16, range_check_is_lte_u32, range_check_is_lte_u48, range_check_is_lte_u64, range_check_is_lte_u80, range_check_is_lte_u96, range_check_rng_chk_bits, range_check_sel, range_check_sel_r0_16_bit_rng_lookup, range_check_sel_r1_16_bit_rng_lookup, range_check_sel_r2_16_bit_rng_lookup, range_check_sel_r3_16_bit_rng_lookup, range_check_sel_r4_16_bit_rng_lookup, range_check_sel_r5_16_bit_rng_lookup, range_check_sel_r6_16_bit_rng_lookup, range_check_u16_r0, range_check_u16_r1, range_check_u16_r2, range_check_u16_r3, range_check_u16_r4, range_check_u16_r5, range_check_u16_r6, range_check_u16_r7, range_check_value, lookup_rng_chk_pow_2_counts, lookup_rng_chk_diff_counts, lookup_rng_chk_is_r0_16_bit_counts, lookup_rng_chk_is_r1_16_bit_counts, lookup_rng_chk_is_r2_16_bit_counts, lookup_rng_chk_is_r3_16_bit_counts, lookup_rng_chk_is_r4_16_bit_counts, lookup_rng_chk_is_r5_16_bit_counts, lookup_rng_chk_is_r6_16_bit_counts, lookup_rng_chk_is_r7_16_bit_counts, lookup_dummy_precomputed_counts, lookup_dummy_dynamic_counts
#define AVM2_DERIVED_WITNESS_ENTITIES perm_dummy_dynamic_inv, lookup_rng_chk_pow_2_inv, lookup_rng_chk_diff_inv, lookup_rng_chk_is_r0_16_bit_inv, lookup_rng_chk_is_r1_16_bit_inv, lookup_rng_chk_is_r2_16_bit_inv, lookup_rng_chk_is_r3_16_bit_inv, lookup_rng_chk_is_r4_16_bit_inv, lookup_rng_chk_is_r5_16_bit_inv, lookup_rng_chk_is_r6_16_bit_inv, lookup_rng_chk_is_r7_16_bit_inv, lookup_dummy_precomputed_inv, lookup_dummy_dynamic_inv
#define AVM2_SHIFTED_ENTITIES execution_sel_shift
#define AVM2_TO_BE_SHIFTED(e) e.execution_sel
Expand Down
Loading

0 comments on commit c4812be

Please sign in to comment.