Skip to content

Commit

Permalink
Implement gas computation for EXP opcode
Browse files Browse the repository at this point in the history 
This commit also fixes incompmlete constraints on s and an incorrect
assumption of d_sum = 1 implying d = 1.
  • Loading branch information
@mizabrik @ETatuzova
mizabrik authored and ETatuzova committed Jan 21, 2025
1 parent 3e188ae commit 9384dab
Show file tree
Hide file tree
Showing 4 changed files with 105 additions and 65 deletions.
2 changes: 1 addition & 1 deletion ...eprint/include/nil/blueprint/zkevm_bbf/input_generators/opcode_tester_input_generator.hpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -261,7 +261,7 @@ namespace nil {
std::cout << "\tExponentiation: " << a << " ^ " << d << std::endl;
_exponentiations.push_back({a, d});
pc++;
//gas -= (d == 0) ? 10 : (10 + 10 * (1 + log256(d)));
gas -= 10 + 50 * count_significant_bytes(d);
} else if (opcode == zkevm_opcode::SIGNEXTEND){
// 0x0b
zkevm_word_type b = stack.back();
Expand Down
152 changes: 96 additions & 56 deletions crypto3/libs/blueprint/include/nil/blueprint/zkevm_bbf/opcodes/exp.hpp
View file
Original file line number Diff line number Diff line change
@@ -1,5 +1,6 @@
//---------------------------------------------------------------------------//
// Copyright (c) 2024 Elena Tatuzova <[email protected]>
// Copyright (c) 2025 Alexander Vasilyev <[email protected]>
//
// MIT License
//
Expand Down Expand Up @@ -53,81 +54,120 @@ namespace nil {
std::vector<TYPE> A(16);
std::vector<TYPE> D(16);
std::vector<TYPE> R(16);
std::vector<TYPE> d_log(8);
std::vector<TYPE> d_inv(8);
TYPE d_sum;
TYPE r_sum;
TYPE d_sum_inv;
TYPE d_sum_inv_1;
TYPE s;
TYPE s; // flags if we use a lookup from exp circuit rather than calculate inplace

std::vector<TYPE> D_gt_255(16);
std::vector<TYPE> D_gt_diff(16);
std::vector<TYPE> D_first_inv(16); // D_inv[i] for min i s.t. D[i] != 0, else 0

if constexpr( stage == GenerationStage::ASSIGNMENT ){
if constexpr (stage == GenerationStage::ASSIGNMENT) {
auto a = w_to_16(current_state.stack_top());
auto d = w_to_16(current_state.stack_top(1));
auto r = w_to_16(exp_by_squaring(current_state.stack_top(), current_state.stack_top(1)));
s = 1;
if( current_state.stack_top(1) == 0 ) s = 0;
if( current_state.stack_top(1) == 1 ) s = 0;
if (current_state.stack_top(1) == 0) s = 0;
if (current_state.stack_top(1) == 1) s = 0;

std::cout << "\t"
<< current_state.stack_top() << " ^ "
<< current_state.stack_top(1) << " = "
<< exp_by_squaring(current_state.stack_top(), current_state.stack_top(1))
<< std::endl;
for( std::size_t i = 0; i < 16; i++){

bool had_nonzero = false;
for (std::size_t i = 0; i < 16; ++i) {
A[i] = a[i];
D[i] = d[i];
R[i] = r[i];
d_sum += d[i];

D_gt_255[i] = d[i] > 0xFF;
D_gt_diff[i] = 0xFF + (d[i] > 0xFF) * 0x10000 - d[i];

if (!had_nonzero && d[i]) {
had_nonzero = true;
D_first_inv[i] = D[i].inversed();
}
}
d_sum_inv = d_sum == 0? 0: d_sum.inversed();
d_sum_inv_1 = d_sum == 1 ? 0: (d_sum - 1).inversed();
}
for( std::size_t i = 0; i < 16; i++){
allocate(A[i], i, 0);
allocate(D[i], i + 16, 0);
allocate(R[i], i, 1);
r_sum += R[i];
}
allocate(d_sum, 32, 0);
allocate(d_sum_inv, 33, 0);
allocate(d_sum_inv_1, 34, 0);
allocate(s, 35, 0);

TYPE d_sum_constraint;
for( std::size_t i = 0; i < 16; i++){
d_sum_constraint += D[i];
}

constrain(s * (s-1));
constrain(d_sum_constraint - d_sum);
constrain(d_sum * (d_sum_inv * d_sum - 1));
constrain(d_sum_inv * (d_sum_inv * d_sum - 1));
constrain(d_sum_inv_1 * (d_sum_inv_1 * (d_sum - 1) - 1));
constrain((s - 1) * (d_sum - 1) * d_sum); // s == 0 => (d == 0 & d == 1)
// s == 0 && d == 1 => R == A
for( std::size_t i = 0; i < 16; i++){
constrain( (s - 1) * d_sum * (R[i] - A[i]));
TYPE d_sum;
TYPE d_first_nonzero_sum;
for (std::size_t i = 0; i < 16; ++i) {
allocate(A[i], i, 2);
allocate(R[i], 16 + i, 2);
allocate(D[i], i, 1);

allocate(D_gt_diff[i], 16 + i, 1);
allocate(D_gt_255[i], i, 0);
constrain(D_gt_255[i] * (1 - D_gt_255[i]));
constrain(D[i] + D_gt_diff[i] - 0xFF - D_gt_255[i] * 0x10000);

allocate(D_first_inv[i], 32 + i, 1);
// D_first_inv[i] != 0 => it is an inverse
constrain(D_first_inv[i] * (1 - D[i] * D_first_inv[i]));

d_sum += D[i];
d_first_nonzero_sum += D[i] * D_first_inv[i];
}

// (s == 0 && d == 0) => R == 1
constrain((s - 1) * (d_sum - 1) * (R[15] - 1));
constrain((s - 1) * (d_sum - 1) * (r_sum - R[15]));

auto A_128 = chunks16_to_chunks128<TYPE>(A);
auto D_128 = chunks16_to_chunks128<TYPE>(D);
auto R_128 = chunks16_to_chunks128<TYPE>(R);
constrain( (1 - (d_sum - 1) * d_sum_inv_1) * (A_128.first - R_128.first) );
constrain( (1 - (d_sum - 1) * d_sum_inv_1) * (A_128.second - R_128.second) );
constrain( (1 - (d_sum - 1) * d_sum_inv_1) * s );

// If d[i] != 0, for j > i D_first_inv[j] = 0, since it isn't first
for (std::size_t i = 0; i < 15; ++i) {
TYPE next_invs;
for (int j = i + 1; j < 16; ++j) next_invs += D[j] * D_first_inv[j];
constrain(D[i] * next_invs);
}

// If d != 0, d_first_inv has a non-zero element
constrain(d_sum * (1 - d_first_nonzero_sum));
// else, the sum is 0 so it's a [D != 0] too
auto &d_ne_0 = d_first_nonzero_sum;

TYPE d_len;
for (std::size_t i = 0; i < 16; ++i) {
d_len += D[i] * D_first_inv[i] * (
D_gt_255[i] + 1 // this word's bytes
+ 2 * (15 - i) // less significant bytes
);
}
allocate(d_len, 32, 2);

// D = 1 <=> d[15] is first non-zero and d[15] = 1
TYPE d_is_1_w;
if constexpr (stage == GenerationStage::ASSIGNMENT)
d_is_1_w = D[15] == 1 ? 0 : (D[15] - 1).inversed();
allocate(d_is_1_w, 33, 2);
constrain((D[15] - 1) * (1 - (D[15] - 1) * d_is_1_w));

TYPE d_is_1 = (1 - (D[15] - 1) * d_is_1_w) * D[15] * D_first_inv[15];
allocate(d_is_1, 34, 2);

allocate(s, 35, 2);
constrain(s * (s-1));

// s == 0 => d == 0 || d == 1
constrain((1 - s) * d_ne_0 * (1 - d_is_1));

// d == 0 => s == 0 && R == 1
constrain((1 - d_ne_0) * s);
constrain((1 - d_ne_0) * R_128.first);
constrain((1 - d_ne_0) * (R_128.second - 1));

// d == 1 => s == 0 && R == A
constrain(d_is_1 * s);
constrain(d_is_1 * (R_128.first - A_128.first));
constrain(d_is_1 * (R_128.second - A_128.second));

if constexpr( stage == GenerationStage::CONSTRAINTS ){
constrain(current_state.pc_next() - current_state.pc(1) - 1); // PC transition
// constrain(current_state.gas(1) - current_state.gas_next() - 5); // GAS transition
constrain(current_state.stack_size(1) - current_state.stack_size_next() - 1); // stack_size transition
constrain(current_state.memory_size(1) - current_state.memory_size_next()); // memory_size transition
constrain(current_state.rw_counter_next() - current_state.rw_counter(1) - 3); // rw_counter transition
constrain(current_state.pc_next() - current_state.pc(2) - 1); // PC transition
constrain(current_state.gas(2) - current_state.gas_next() - 10 - 50 * d_len); // GAS transition
constrain(current_state.stack_size(2) - current_state.stack_size_next() - 1); // stack_size transition
constrain(current_state.memory_size(2) - current_state.memory_size_next()); // memory_size transition
constrain(current_state.rw_counter_next() - current_state.rw_counter(2) - 3); // rw_counter transition
std::vector<TYPE> tmp;
tmp = {
TYPE(rw_op_to_num(rw_operation_type::stack)),
Expand All @@ -144,25 +184,25 @@ namespace nil {
lookup(tmp, "zkevm_rw");
tmp = {
TYPE(rw_op_to_num(rw_operation_type::stack)),
current_state.call_id(0),
current_state.stack_size(0) - 2,
current_state.call_id(1),
current_state.stack_size(1) - 2,
TYPE(0),// storage_key_hi
TYPE(0),// storage_key_lo
TYPE(0),// field
current_state.rw_counter(0) + 1,
current_state.rw_counter(1) + 1,
TYPE(0),// is_write
D_128.first,
D_128.second
};
lookup(tmp, "zkevm_rw");
tmp = {
TYPE(rw_op_to_num(rw_operation_type::stack)),
current_state.call_id(1),
current_state.stack_size(1) - 2,
current_state.call_id(0),
current_state.stack_size(0) - 2,
TYPE(0),// storage_key_hi
TYPE(0),// storage_key_lo
TYPE(0),// field
current_state.rw_counter(1) + 2,
current_state.rw_counter(0) + 2,
TYPE(1),// is_write
R_128.first,
R_128.second
Expand Down Expand Up @@ -200,7 +240,7 @@ namespace nil {
zkevm_exp_bbf<FieldType, GenerationStage::CONSTRAINTS> bbf_obj(context, current_state);
}
virtual std::size_t rows_amount() override {
return 2;
return 3;
}
};
} // namespace bbf
Expand Down
13 changes: 5 additions & 8 deletions crypto3/libs/blueprint/include/nil/blueprint/zkevm_bbf/util.hpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -84,14 +84,11 @@ namespace nil {
return exp2;
}

std::size_t log256(zkevm_word_type d) {
std::size_t result = 0;
while(d > 0){
d /= 256u;
result++;
}
return result;
std::size_t count_significant_bytes(zkevm_word_type d) {
std::size_t count = 0;
while (d > 0) d /= 256u, ++count;
return count;
}
}
}
}
}
3 changes: 3 additions & 0 deletions crypto3/libs/blueprint/test/zkevm_bbf/opcodes/exp.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -80,6 +80,9 @@ BOOST_AUTO_TEST_CASE(exp) {
opcode_tester.push_opcode(zkevm_opcode::PUSH32, 1);
opcode_tester.push_opcode(zkevm_opcode::PUSH32, 1);
opcode_tester.push_opcode(zkevm_opcode::EXP);
opcode_tester.push_opcode(zkevm_opcode::PUSH32, 0x10000);
opcode_tester.push_opcode(zkevm_opcode::PUSH32, 3);
opcode_tester.push_opcode(zkevm_opcode::EXP);
opcode_tester.push_opcode(zkevm_opcode::PUSH32, 2);
opcode_tester.push_opcode(
zkevm_opcode::PUSH32,
Expand Down

0 comments on commit 9384dab

Please sign in to comment.