Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
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
109 changes: 73 additions & 36 deletions barretenberg/cpp/pil/vm2/ecc_mem.pil
Original file line number Diff line number Diff line change
Expand Up @@ -39,9 +39,11 @@ include "execution.pil";
* - guaranteed by this gadget to be U1.
*
* ERROR HANDLING:
* A single error needs to be handled as part of this trace
* Two errors needs to be handled as part of this trace,
* (1) DST_OUT_OF_BOUNDS_ACCESS: If the writes would access a memory address outside
* of the max AVM memory address (AVM_HIGHEST_MEM_ADDRESS).
* (2) POINT_NOT_ON_CURVE: If either of the inputs (embedded curve points) do not
* satisfy the grumpkin curve equation (SW form: Y^2 = X^3 − 17)
*
* N.B This subtrace writes the values within a single row (i.e. 3 output columns)
*
Expand Down Expand Up @@ -86,48 +88,45 @@ namespace ecc_add_mem;
gt.sel { gt.input_a, gt.input_b, gt.res };

////////////////////////////////////////////////
// Dispatch from execution trace to ECC Add
// Error Handling - Check Points are on curve
////////////////////////////////////////////////
#[DISPATCH_EXEC_ECC_ADD]
execution.sel_execute_ecc_add {
precomputed.clk,
execution.context_id,
// Point P
execution.register[0],
execution.register[1],
execution.register[2],
// Point Q
execution.register[3],
execution.register[4],
execution.register[5],
// Dst address
execution.rop[6],
// Error
execution.sel_opcode_error
} is
sel {
execution_clk,
space_id,
// Point P
p_x,
p_y,
p_is_inf,
// Point Q
q_x,
q_y,
q_is_inf,
// Dst address
dst_addr[0],
// Error
sel_dst_out_of_range_err
};
pol commit sel_p_not_on_curve_err;
sel_p_not_on_curve_err * (1 - sel_p_not_on_curve_err) = 0;

pol commit sel_q_not_on_curve_err;
sel_q_not_on_curve_err * (1 - sel_q_not_on_curve_err) = 0;

// Y^2 = X^3 − 17, re-formulate to Y^2 - (X^3 - 17) = 0
pol commit p_is_on_curve_eqn; // Needs to be committed to reduce relation degrees
pol P_X3 = p_x * p_x * p_x;
pol P_Y2 = p_y * p_y;
#[P_CURVE_EQN]
p_is_on_curve_eqn = sel * (P_Y2 - (P_X3 - 17)) * (1 - p_is_inf); // Infinity considered as on curve
Copy link
Contributor

Choose a reason for hiding this comment

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

"Infinity considered as on curve", but if p_is_inf = 1, we get p_is_on_curve_eqn = 0

Copy link
Contributor Author

Choose a reason for hiding this comment

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

yep that is intended. In short, the curve equation is y^2 = x^3 - 17, so it gets re-arranged to p_is_on_curve_eqn = y^2 - (x^3 - 17) and to be on the curve we want p_is_on_curve_eqn = 0.

Now a quirk is that the point at infinity actually doesnt satisfy the equation. So im multiplifying it by zero essentially to ensure we get p_is_on_curve_eqn = 0.

@MirandaWood is actually mathematically qualified so please tell me if this is correct.

Copy link
Contributor

Choose a reason for hiding this comment

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

Wait so p_is_on_curve == "p is NOT on the curve"?

Copy link
Contributor

Choose a reason for hiding this comment

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

Sounds correct to me!
Looks like we want p_is_on_curve_eqn = 0 iff P is on the curve, which is true when y^2 - (x^3 - 17) = 0 or we have the point at infinity. So LGTM 🎉

Copy link
Contributor Author

Choose a reason for hiding this comment

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

@dbanks12 it's basically a commited column to represent an evaluation of the "point is on curve" equation. It can have values between [0, p - 1] (basically any field value). If this value !=0 we raise the "not_on_curve_err"

Copy link
Contributor

Choose a reason for hiding this comment

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

I see.... A bit confusing because the variable name sounds like a boolean, but I guess the _eqn suffix is meant to signal otherwise.

// If p_is_on_curve_eqn != 0, sel_p_not_on_curve_err = 1
pol commit p_is_on_curve_eqn_inv;
#[P_ON_CURVE_CHECK]
sel * (p_is_on_curve_eqn * ((1 - sel_p_not_on_curve_err) * (1 - p_is_on_curve_eqn_inv) + p_is_on_curve_eqn_inv) - sel_p_not_on_curve_err) = 0;

// Y^2 = X^3 − 17, re-formulate to Y^2 - (X^3 - 17) = 0
pol commit q_is_on_curve_eqn; // Needs to be committed to reduce relation degrees
pol Q_X3 = q_x * q_x * q_x;
pol Q_Y2 = q_y * q_y;
#[Q_CURVE_EQN]
q_is_on_curve_eqn = sel * (Q_Y2 - (Q_X3 - 17)) * (1 - q_is_inf); // Infinity considered as on curve
Copy link
Contributor

Choose a reason for hiding this comment

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

Same here

// If q_is_on_curve_eqn != 0, sel_q_not_on_curve_err = 1
pol commit q_is_on_curve_eqn_inv;
#[Q_ON_CURVE_CHECK]
sel * (q_is_on_curve_eqn * ((1 - sel_q_not_on_curve_err) * (1 - q_is_on_curve_eqn_inv) + q_is_on_curve_eqn_inv) - sel_q_not_on_curve_err) = 0;

pol commit err; // Consolidate errors
err = 1 - (1 - sel_dst_out_of_range_err) * (1 - sel_p_not_on_curve_err) * (1 - sel_q_not_on_curve_err);

///////////////////////////////////////////////////////////////////////
// Dispatch inputs to ecc add and retrieve outputs
///////////////////////////////////////////////////////////////////////
pol commit res_x, res_y, res_is_inf;
pol commit sel_should_exec;
sel_should_exec = sel * (1 - sel_dst_out_of_range_err);
sel_should_exec = sel * (1 - err);

#[INPUT_OUTPUT_ECC_ADD]
sel_should_exec {
Expand Down Expand Up @@ -180,3 +179,41 @@ namespace ecc_add_mem;
memory.value, memory.tag,
memory.space_id, memory.rw
};

////////////////////////////////////////////////
// Dispatch from execution trace to ECC Add
////////////////////////////////////////////////
#[DISPATCH_EXEC_ECC_ADD]
execution.sel_execute_ecc_add {
precomputed.clk,
execution.context_id,
// Point P
execution.register[0],
execution.register[1],
execution.register[2],
// Point Q
execution.register[3],
execution.register[4],
execution.register[5],
// Dst address
execution.rop[6],
// Error
execution.sel_opcode_error
} is
sel {
execution_clk,
space_id,
// Point P
p_x,
p_y,
p_is_inf,
// Point Q
q_x,
q_y,
q_is_inf,
// Dst address
dst_addr[0],
// Error
err
};

Original file line number Diff line number Diff line change
Expand Up @@ -938,14 +938,13 @@ TEST(EccAddMemoryConstrainingTest, EccAddMemoryEmptyRow)

TEST(EccAddMemoryConstrainingTest, EccAddMemory)
{

TestTraceContainer trace;
EccTraceBuilder builder;
MemoryStore memory;

NoopEventEmitter<EccAddEvent> ecc_add_event_emitter;
EventEmitter<ScalarMulEvent> scalar_mul_event_emitter;
NoopEventEmitter<EccAddMemoryEvent> ecc_add_memory_event_emitter;
EventEmitter<EccAddMemoryEvent> ecc_add_memory_event_emitter;
EventEmitter<EccAddEvent> ecc_add_event_emitter;
NoopEventEmitter<ScalarMulEvent> scalar_mul_event_emitter;
NoopEventEmitter<ToRadixEvent> to_radix_event_emitter;

StrictMock<MockExecutionIdManager> execution_id_manager;
Expand Down Expand Up @@ -1097,7 +1096,71 @@ TEST(EccAddMemoryConstrainingTest, EccAddMemoryInvalidDstRange)
EXPECT_THROW_WITH_MESSAGE(ecc_simulator.add(memory, p, q, dst_address), "EccException.* dst address out of range");

builder.process_add_with_memory(ecc_add_memory_event_emitter.dump_events(), trace);
builder.process_add(ecc_add_event_emitter.dump_events(), trace);
EXPECT_EQ(ecc_add_event_emitter.get_events().size(), 0); // Expect 0 add events since error in ecc_mem

check_all_interactions<EccTraceBuilder>(trace);
check_relation<mem_aware_ecc>(trace);
}

TEST(EccAddMemoryConstrainingTest, EccAddMemoryPointError)
{

EccTraceBuilder builder;
MemoryStore memory;

EventEmitter<EccAddEvent> ecc_add_event_emitter;
NoopEventEmitter<ScalarMulEvent> scalar_mul_event_emitter;
EventEmitter<EccAddMemoryEvent> ecc_add_memory_event_emitter;
NoopEventEmitter<ToRadixEvent> to_radix_event_emitter;

StrictMock<MockExecutionIdManager> execution_id_manager;
EXPECT_CALL(execution_id_manager, get_execution_id)
.WillRepeatedly(Return(0)); // Use a fixed execution IDfor the test
FakeGreaterThan gt;
ToRadixSimulator to_radix_simulator(to_radix_event_emitter);
EccSimulator ecc_simulator(execution_id_manager,
gt,
to_radix_simulator,
ecc_add_event_emitter,
scalar_mul_event_emitter,
ecc_add_memory_event_emitter);

// Point P is not on the curve
FF p_x("0x0000000000063d46918a156cae92db1bcbc4072a27ec81dc82ea959abdbcf16a");
FF p_y("0x00000000000c1370462c74775765d07fc21fd1093cc988149d3aa763bb3dbb60");
EmbeddedCurvePoint p(p_x, p_y, false);

uint32_t dst_address = 0x1000;

EXPECT_CALL(execution_id_manager, get_execution_id()).WillOnce(::testing::Return(0));
// Set the execution and gt traces
TestTraceContainer trace = TestTraceContainer({
// Row 0
{
// Execution
{ C::execution_sel, 1 },
{ C::execution_sel_execute_ecc_add, 1 },
{ C::execution_rop_6_, dst_address },
{ C::execution_register_0_, p.x() },
{ C::execution_register_1_, p.y() },
{ C::execution_register_2_, p.is_infinity() ? 1 : 0 },
{ C::execution_register_3_, q.x() },
{ C::execution_register_4_, q.y() },
{ C::execution_register_5_, q.is_infinity() ? 1 : 0 },
{ C::execution_sel_opcode_error, 1 }, // Indicate an error in the operation
// GT - dst out of range check
{ C::gt_sel, 1 },
{ C::gt_input_a, dst_address + 2 }, // highest write address is dst_address + 2
{ C::gt_input_b, AVM_HIGHEST_MEM_ADDRESS },
{ C::gt_res, 0 },
},
});

EXPECT_THROW(ecc_simulator.add(memory, p, q, dst_address), simulation::EccException);

builder.process_add_with_memory(ecc_add_memory_event_emitter.dump_events(), trace);
// Expect no events to be emitted since the operation failed
EXPECT_EQ(ecc_add_event_emitter.get_events().size(), 0);

check_all_interactions<EccTraceBuilder>(trace);
check_relation<mem_aware_ecc>(trace);
Expand Down
6 changes: 3 additions & 3 deletions barretenberg/cpp/src/barretenberg/vm2/generated/columns.hpp

Large diffs are not rendered by default.

Original file line number Diff line number Diff line change
Expand Up @@ -114,10 +114,10 @@ namespace bb::avm2 {

struct AvmFlavorVariables {
static constexpr size_t NUM_PRECOMPUTED_ENTITIES = 125;
static constexpr size_t NUM_WITNESS_ENTITIES = 2511;
static constexpr size_t NUM_WITNESS_ENTITIES = 2518;
static constexpr size_t NUM_SHIFTED_ENTITIES = 250;
static constexpr size_t NUM_WIRES = NUM_WITNESS_ENTITIES + NUM_PRECOMPUTED_ENTITIES;
static constexpr size_t NUM_ALL_ENTITIES = 2886;
static constexpr size_t NUM_ALL_ENTITIES = 2893;

// Need to be templated for recursive verifier
template <typename FF_>
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -13,7 +13,7 @@ template <typename FF_> class ecc_memImpl {
public:
using FF = FF_;

static constexpr std::array<size_t, 5> SUBRELATION_PARTIAL_LENGTHS = { 3, 3, 3, 3, 3 };
static constexpr std::array<size_t, 12> SUBRELATION_PARTIAL_LENGTHS = { 3, 3, 3, 3, 3, 3, 6, 5, 6, 5, 4, 3 };

template <typename AllEntities> inline static bool skip(const AllEntities& in)
{
Expand All @@ -31,6 +31,12 @@ template <typename FF_> class ecc_memImpl {
using C = ColumnAndShifts;

const auto constants_AVM_HIGHEST_MEM_ADDRESS = FF(4294967295UL);
const auto ecc_add_mem_P_X3 =
in.get(C::ecc_add_mem_p_x) * in.get(C::ecc_add_mem_p_x) * in.get(C::ecc_add_mem_p_x);
const auto ecc_add_mem_P_Y2 = in.get(C::ecc_add_mem_p_y) * in.get(C::ecc_add_mem_p_y);
const auto ecc_add_mem_Q_X3 =
in.get(C::ecc_add_mem_q_x) * in.get(C::ecc_add_mem_q_x) * in.get(C::ecc_add_mem_q_x);
const auto ecc_add_mem_Q_Y2 = in.get(C::ecc_add_mem_q_y) * in.get(C::ecc_add_mem_q_y);

{ // WRITE_INCR_DST_ADDR
using Accumulator = typename std::tuple_element_t<0, ContainerOverSubrelations>;
Expand Down Expand Up @@ -62,11 +68,70 @@ template <typename FF_> class ecc_memImpl {
}
{
using Accumulator = typename std::tuple_element_t<4, ContainerOverSubrelations>;
auto tmp = (in.get(C::ecc_add_mem_sel_should_exec) -
in.get(C::ecc_add_mem_sel) * (FF(1) - in.get(C::ecc_add_mem_sel_dst_out_of_range_err)));
auto tmp =
in.get(C::ecc_add_mem_sel_p_not_on_curve_err) * (FF(1) - in.get(C::ecc_add_mem_sel_p_not_on_curve_err));
tmp *= scaling_factor;
std::get<4>(evals) += typename Accumulator::View(tmp);
}
{
using Accumulator = typename std::tuple_element_t<5, ContainerOverSubrelations>;
auto tmp =
in.get(C::ecc_add_mem_sel_q_not_on_curve_err) * (FF(1) - in.get(C::ecc_add_mem_sel_q_not_on_curve_err));
tmp *= scaling_factor;
std::get<5>(evals) += typename Accumulator::View(tmp);
}
{ // P_CURVE_EQN
using Accumulator = typename std::tuple_element_t<6, ContainerOverSubrelations>;
auto tmp = (in.get(C::ecc_add_mem_p_is_on_curve_eqn) -
in.get(C::ecc_add_mem_sel) * (ecc_add_mem_P_Y2 - (ecc_add_mem_P_X3 - FF(17))) *
(FF(1) - in.get(C::ecc_add_mem_p_is_inf)));
tmp *= scaling_factor;
std::get<6>(evals) += typename Accumulator::View(tmp);
}
{ // P_ON_CURVE_CHECK
using Accumulator = typename std::tuple_element_t<7, ContainerOverSubrelations>;
auto tmp = in.get(C::ecc_add_mem_sel) * (in.get(C::ecc_add_mem_p_is_on_curve_eqn) *
((FF(1) - in.get(C::ecc_add_mem_sel_p_not_on_curve_err)) *
(FF(1) - in.get(C::ecc_add_mem_p_is_on_curve_eqn_inv)) +
in.get(C::ecc_add_mem_p_is_on_curve_eqn_inv)) -
in.get(C::ecc_add_mem_sel_p_not_on_curve_err));
tmp *= scaling_factor;
std::get<7>(evals) += typename Accumulator::View(tmp);
}
{ // Q_CURVE_EQN
using Accumulator = typename std::tuple_element_t<8, ContainerOverSubrelations>;
auto tmp = (in.get(C::ecc_add_mem_q_is_on_curve_eqn) -
in.get(C::ecc_add_mem_sel) * (ecc_add_mem_Q_Y2 - (ecc_add_mem_Q_X3 - FF(17))) *
(FF(1) - in.get(C::ecc_add_mem_q_is_inf)));
tmp *= scaling_factor;
std::get<8>(evals) += typename Accumulator::View(tmp);
}
{ // Q_ON_CURVE_CHECK
using Accumulator = typename std::tuple_element_t<9, ContainerOverSubrelations>;
auto tmp = in.get(C::ecc_add_mem_sel) * (in.get(C::ecc_add_mem_q_is_on_curve_eqn) *
((FF(1) - in.get(C::ecc_add_mem_sel_q_not_on_curve_err)) *
(FF(1) - in.get(C::ecc_add_mem_q_is_on_curve_eqn_inv)) +
in.get(C::ecc_add_mem_q_is_on_curve_eqn_inv)) -
in.get(C::ecc_add_mem_sel_q_not_on_curve_err));
tmp *= scaling_factor;
std::get<9>(evals) += typename Accumulator::View(tmp);
}
{
using Accumulator = typename std::tuple_element_t<10, ContainerOverSubrelations>;
auto tmp =
(in.get(C::ecc_add_mem_err) - (FF(1) - (FF(1) - in.get(C::ecc_add_mem_sel_dst_out_of_range_err)) *
(FF(1) - in.get(C::ecc_add_mem_sel_p_not_on_curve_err)) *
(FF(1) - in.get(C::ecc_add_mem_sel_q_not_on_curve_err))));
tmp *= scaling_factor;
std::get<10>(evals) += typename Accumulator::View(tmp);
}
{
using Accumulator = typename std::tuple_element_t<11, ContainerOverSubrelations>;
auto tmp = (in.get(C::ecc_add_mem_sel_should_exec) -
in.get(C::ecc_add_mem_sel) * (FF(1) - in.get(C::ecc_add_mem_err)));
tmp *= scaling_factor;
std::get<11>(evals) += typename Accumulator::View(tmp);
}
}
};

Expand All @@ -79,12 +144,24 @@ template <typename FF> class ecc_mem : public Relation<ecc_memImpl<FF>> {
switch (index) {
case 0:
return "WRITE_INCR_DST_ADDR";
case 6:
return "P_CURVE_EQN";
case 7:
return "P_ON_CURVE_CHECK";
case 8:
return "Q_CURVE_EQN";
case 9:
return "Q_ON_CURVE_CHECK";
}
return std::to_string(index);
}

// Subrelation indices constants, to be used in tests.
static constexpr size_t SR_WRITE_INCR_DST_ADDR = 0;
static constexpr size_t SR_P_CURVE_EQN = 6;
static constexpr size_t SR_P_ON_CURVE_CHECK = 7;
static constexpr size_t SR_Q_CURVE_EQN = 8;
static constexpr size_t SR_Q_ON_CURVE_CHECK = 9;
};

} // namespace bb::avm2
Original file line number Diff line number Diff line change
Expand Up @@ -32,7 +32,7 @@ struct perm_ecc_mem_dispatch_exec_ecc_add_settings_ {
ColumnAndShifts::ecc_add_mem_p_x, ColumnAndShifts::ecc_add_mem_p_y,
ColumnAndShifts::ecc_add_mem_p_is_inf, ColumnAndShifts::ecc_add_mem_q_x,
ColumnAndShifts::ecc_add_mem_q_y, ColumnAndShifts::ecc_add_mem_q_is_inf,
ColumnAndShifts::ecc_add_mem_dst_addr_0_, ColumnAndShifts::ecc_add_mem_sel_dst_out_of_range_err
ColumnAndShifts::ecc_add_mem_dst_addr_0_, ColumnAndShifts::ecc_add_mem_err
};
};

Expand Down
Loading
Loading