Skip to content

Commit

Permalink
shift operation bbf constraints update
Browse files Browse the repository at this point in the history
  • Loading branch information
Antoine Cyr committed Nov 26, 2024
1 parent 806db8f commit bf8ad39
Show file tree
Hide file tree
Showing 6 changed files with 184 additions and 128 deletions.
18 changes: 9 additions & 9 deletions ...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 @@ -388,12 +388,12 @@ namespace nil {
gas -= 3;
}else if(opcode == zkevm_opcode::SHL) {
// // 0x1b
zkevm_word_type a = stack.back();
stack.pop_back();
_rw_operations.push_back(stack_rw_operation(call_id, stack.size(), rw_counter++, false, a));
zkevm_word_type b = stack.back();
stack.pop_back();
_rw_operations.push_back(stack_rw_operation(call_id, stack.size(), rw_counter++, false, b));
zkevm_word_type a = stack.back();
stack.pop_back();
_rw_operations.push_back(stack_rw_operation(call_id, stack.size(), rw_counter++, false, a));
int shift = (integral_type(b) < 256) ? int(integral_type(b)) : 256;
zkevm_word_type result = zkevm_word_type(integral_type(a) << shift);
_rw_operations.push_back(stack_rw_operation(call_id, stack.size(), rw_counter++, true, result));
Expand All @@ -402,12 +402,12 @@ namespace nil {
gas -= 3;
}else if(opcode == zkevm_opcode::SHR) {
// 0x1c
zkevm_word_type a = stack.back();
stack.pop_back();
_rw_operations.push_back(stack_rw_operation(call_id, stack.size(), rw_counter++, false, a));
zkevm_word_type b = stack.back();
stack.pop_back();
_rw_operations.push_back(stack_rw_operation(call_id, stack.size(), rw_counter++, false, b));
zkevm_word_type a = stack.back();
stack.pop_back();
_rw_operations.push_back(stack_rw_operation(call_id, stack.size(), rw_counter++, false, a));
int shift = (integral_type(b) < 256) ? int(integral_type(b)) : 256;
integral_type r_integral = integral_type(a) >> shift;
zkevm_word_type result = zkevm_word_type::backend_type(r_integral.backend());
Expand All @@ -417,12 +417,12 @@ namespace nil {
gas -= 3;
}else if(opcode == zkevm_opcode::SAR) {
//0x1d
zkevm_word_type input_a = stack.back();
stack.pop_back();
_rw_operations.push_back(stack_rw_operation(call_id, stack.size(), rw_counter++, false, input_a));
zkevm_word_type b = stack.back();
stack.pop_back();
_rw_operations.push_back(stack_rw_operation(call_id, stack.size(), rw_counter++, false, b));
zkevm_word_type input_a = stack.back();
stack.pop_back();
_rw_operations.push_back(stack_rw_operation(call_id, stack.size(), rw_counter++, false, input_a));
auto is_negative = [](zkevm_word_type x) {
return (integral_type(x) > zkevm_modulus / 2 - 1);};
auto negate_word = [](zkevm_word_type x) {
Expand Down
93 changes: 56 additions & 37 deletions crypto3/libs/blueprint/include/nil/blueprint/zkevm_bbf/opcodes/sar.hpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -184,12 +184,15 @@ namespace nil {
std::vector<TYPE> q_chunks(chunk_amount);
std::vector<TYPE> v_chunks(chunk_amount);

std::vector<TYPE> indic_1(chunk_amount);
std::vector<TYPE> indic_2(chunk_amount);

TYPE carry[3][carry_amount + 1];

if constexpr (stage == GenerationStage::ASSIGNMENT) {
zkevm_word_type input_a = current_state.stack_top();
zkevm_word_type input_b = current_state.stack_top(1);

zkevm_word_type input_b = current_state.stack_top();
zkevm_word_type input_a = current_state.stack_top(1);
auto is_negative = [](zkevm_word_type x) {
return (integral_type(x) > zkevm_modulus / 2 - 1);
};
Expand Down Expand Up @@ -249,11 +252,19 @@ namespace nil {
z = (1 - b0ppp * I1) *
(1 -
sum_part_b * I2); // z is zero if input_b >= 256, otherwise it is 1
two_powers =
(static_cast<unsigned int>(1) << int(integral_type(input_b) % 16));
tp = z * (static_cast<unsigned int>(1) << int(integral_type(input_b) % 16));
b_sum_inverse = b_sum.is_zero() ? 0 : b_sum.inversed();
b_zero = 1 - b_sum_inverse * b_sum;

two_powers = 0;
unsigned int pow = 1;
for (std::size_t i = 0; i < chunk_amount; i++) {
indic_1[i] = (b0p - i).is_zero() ? 0 : (b0p - i).inversed();
indic_2[i] = (b0pp - i).is_zero() ? 0 : (b0pp - i).inversed();
two_powers += (1 - (b0p - i) * indic_1[i]) * pow;
pow *= 2;
}

// note that we don't assign 64-chunks for a/b, as we can build them from
// 16-chunks with constraints under the same logic we only assign the 16 -
// bit
Expand Down Expand Up @@ -352,20 +363,28 @@ namespace nil {
constrain(b_zero * r_chunks[i]);
}

tp = z * two_powers;
allocate(tp, 35, 3);
allocate(z, 36, 3);
allocate(I1, 37, 3);
allocate(I2, 38, 3);
allocate(two_powers, 39, 3);

allocate(b0p, 32, 3);
allocate(b0pp, 33, 3);
allocate(b0ppp, 34, 3);
allocate(sum_part_b, 40, 3);
allocate(tp, 12, 4);
allocate(z, 13, 4);
allocate(I1, 39, 2);
allocate(I2, 40, 2);
allocate(two_powers, 41, 2);

allocate(b0p, 9, 4);
allocate(b0pp, 10, 4);
allocate(b0ppp, 11, 4);
allocate(sum_part_b, 42, 2);
allocate(b_sum, 40, 1);
allocate(b_sum_inverse, 41, 1);

constrain(tp - z * two_powers);
for (std::size_t i = 0; i < chunk_amount; i++) {
allocate(indic_1[i], i + 2 * chunk_amount, 3);
allocate(indic_2[i], i + 2 * chunk_amount, 4);
constrain((b0p - i) * (1 - (b0p - i) * indic_1[i]));
constrain((b0pp - i) * (1 - (b0pp - i) * indic_2[i]));
constrain(b_chunks[i] - tp * (1 - (b0pp - i) * indic_2[i]));
}

constrain(b_sum_inverse * (b_sum_inverse * b_sum - 1));
constrain(b_sum * (b_sum_inverse * b_sum - 1));
constrain(input_b_chunks[0] - b0p - 16 * b0pp - 256 * b0ppp);
Expand All @@ -374,11 +393,11 @@ namespace nil {
constrain(sum_part_b * (1 - sum_part_b * I2));
constrain((z - (1 - b0ppp * I1) * (1 - sum_part_b * I2)));

allocate(first_carryless, 32, 4);
allocate(second_carryless, 35, 4);
allocate(third_carryless, 36, 4);
allocate(c_1_64, 33, 4);
allocate(c_2, 34, 4);
allocate(first_carryless, 39, 0);
allocate(second_carryless, 40, 0);
allocate(third_carryless, 41, 0);
allocate(c_1_64, 42, 0);
allocate(c_2, 43, 0);

allocate(b_64_chunks[3], 7, 4);
allocate(r_64_chunks[3], 8, 4);
Expand Down Expand Up @@ -488,12 +507,12 @@ namespace nil {
B1 = B_128.second;
Res0 = Res_128.first;
Res1 = Res_128.second;
allocate(A0, 39, 0);
allocate(A1, 40, 0);
allocate(B0, 39, 2);
allocate(B1, 40, 2);
allocate(Res0, 41, 0);
allocate(Res1, 41, 2);
allocate(A0, 45, 0);
allocate(A1, 46, 0);
allocate(B0, 45, 2);
allocate(B1, 46, 2);
allocate(Res0, 47, 0);
allocate(Res1, 47, 2);

if constexpr (stage == GenerationStage::CONSTRAINTS) {
constrain(current_state.pc_next() - current_state.pc(4) -
Expand All @@ -508,26 +527,26 @@ namespace nil {
3); // rw_counter transition
std::vector<TYPE> tmp;
tmp = {TYPE(rw_op_to_num(rw_operation_type::stack)),
current_state.call_id(1),
current_state.stack_size(1) - 1,
current_state.call_id(2),
current_state.stack_size(2) - 1,
TYPE(0), // storage_key_hi
TYPE(0), // storage_key_lo
TYPE(0), // field
current_state.rw_counter(1),
current_state.rw_counter(2),
TYPE(0), // is_write
A0,
A1};
B0,
B1};
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) + 1,
current_state.rw_counter(0) + 1,
TYPE(0), // is_write
B0,
B1};
A0,
A1};
lookup(tmp, "zkevm_rw");
tmp = {TYPE(rw_op_to_num(rw_operation_type::stack)),
current_state.call_id(1),
Expand Down
8 changes: 4 additions & 4 deletions crypto3/libs/blueprint/include/nil/blueprint/zkevm_bbf/opcodes/sdiv_smod.hpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -543,10 +543,10 @@ namespace nil {
Res1 = Res_128.second;
allocate(A0, 45, 1);
allocate(A1, 46, 1);
allocate(B0, 45, 2);
allocate(B1, 46, 2);
allocate(Res0, 45, 3);
allocate(Res1, 46, 3);
allocate(B0, 45, 3);
allocate(B1, 46, 3);
allocate(Res0, 45, 2);
allocate(Res1, 46, 2);

if constexpr (stage == GenerationStage::CONSTRAINTS) {
constrain(current_state.pc_next() - current_state.pc(4) -
Expand Down
92 changes: 55 additions & 37 deletions crypto3/libs/blueprint/include/nil/blueprint/zkevm_bbf/opcodes/shl.hpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -134,11 +134,14 @@ namespace nil {
std::vector<TYPE> a_chunks(chunk_amount);
std::vector<TYPE> b_chunks(chunk_amount);
std::vector<TYPE> r_chunks(chunk_amount);

std::vector<TYPE> indic_1(chunk_amount);
std::vector<TYPE> indic_2(chunk_amount);

if constexpr (stage == GenerationStage::ASSIGNMENT) {
zkevm_word_type a = current_state.stack_top();
zkevm_word_type input_b = current_state.stack_top(1);

zkevm_word_type input_b = current_state.stack_top();
zkevm_word_type a = current_state.stack_top(1);
int shift =
(integral_type(input_b) < 256) ? int(integral_type(input_b)) : 256;

Expand All @@ -163,8 +166,7 @@ namespace nil {
I2 = sum_b.is_zero() ? 0 : sum_b.inversed();
z = (1 - b0ppp * I1) *
(1 - sum_b * I2); // z is zero if input_b >= 256, otherwise it is 1
two_powers =
(static_cast<unsigned int>(1) << int(integral_type(input_b) % 16));
tp = z * (static_cast<unsigned int>(1) << int(integral_type(input_b) % 16));

// note that we don't assign 64-chunks for a/b, as we can build them from
// 16-chunks with constraints under the same logic we only assign the 16 -
Expand Down Expand Up @@ -205,6 +207,15 @@ namespace nil {
b0p_range_check = 4096 * b0p;
b0pp_range_check = 4096 * b0pp;
b0ppp_range_check = 256 * b0ppp;

two_powers = 0;
unsigned int pow = 1;
for (std::size_t i = 0; i < chunk_amount; i++) {
indic_1[i] = (b0p - i).is_zero() ? 0 : (b0p - i).inversed();
indic_2[i] = (b0pp - i).is_zero() ? 0 : (b0pp - i).inversed();
two_powers += (1 - (b0p - i) * indic_1[i]) * pow;
pow *= 2;
}
}

allocate(b0p_range_check, 0, 2);
Expand All @@ -223,31 +234,38 @@ namespace nil {
res[i] = r_chunks[i];
}

tp = z * two_powers;
allocate(tp, 14, 2);
allocate(z, 15, 2);
allocate(I1, 33, 0);
allocate(I2, 34, 0);

allocate(tp, 32, 0);
allocate(z, 33, 0);
allocate(I1, 34, 0);
allocate(I2, 35, 0);
allocate(two_powers, 36, 0);
allocate(b0p, 11, 2);
allocate(b0pp, 12, 2);
allocate(b0ppp, 13, 2);
allocate(two_powers, 32, 0);
allocate(sum_b, 35, 0);

allocate(b0p, 32, 1);
allocate(b0pp, 33, 1);
allocate(b0ppp, 34, 1);
allocate(sum_b, 35, 1);
constrain(tp - z * two_powers);
for (std::size_t i = 0; i < chunk_amount; i++) {
allocate(indic_1[i], i + 2 * chunk_amount, 1);
allocate(indic_2[i], i + 2 * chunk_amount, 2);
constrain((b0p - i) * (1 - (b0p - i) * indic_1[i]));
constrain((b0pp - i) * (1 - (b0pp - i) * indic_2[i]));
constrain(b_chunks[i] - tp * (1 - (b0pp - i) * indic_2[i]));
}

constrain(input_b_chunks[0] - b0p - 16 * b0pp - 256 * b0ppp);
constrain(b0ppp * (1 - b0ppp * I1));

constrain(sum_b * (1 - sum_b * I2));
constrain((z - (1 - b0ppp * I1) * (1 - sum_b * I2)));
constrain(z - (1 - b0ppp * I1) * (1 - sum_b * I2));

allocate(first_carryless, 32, 2);
allocate(second_carryless, 33, 2);
allocate(c_1_64, 34, 2);
allocate(c_2, 35, 2);
allocate(c_3_64, 36, 2);
allocate(c_4, 37, 2);
allocate(first_carryless, 16, 2);
allocate(second_carryless, 17, 2);
allocate(c_1_64, 18, 2);
allocate(c_2, 19, 2);
allocate(c_3_64, 20, 2);
allocate(c_4, 21, 2);

constrain(first_carryless - c_1_64 * two_128 - c_2 * two_192);
constrain(second_carryless + c_1_64 + c_2 * two_64 - c_3_64 * two_128 -
Expand All @@ -267,12 +285,12 @@ namespace nil {
B1 = B_128.second;
Res0 = Res_128.first;
Res1 = Res_128.second;
allocate(A0, 37, 0);
allocate(A1, 37, 1);
allocate(A0, 36, 0);
allocate(A1, 37, 0);
allocate(B0, 38, 0);
allocate(B1, 38, 1);
allocate(Res0, 39, 0);
allocate(Res1, 39, 1);
allocate(B1, 39, 0);
allocate(Res0, 40, 0);
allocate(Res1, 41, 0);

if constexpr (stage == GenerationStage::CONSTRAINTS) {
constrain(current_state.pc_next() - current_state.pc(2) -
Expand All @@ -287,15 +305,15 @@ namespace nil {
3); // rw_counter transition
std::vector<TYPE> tmp;
tmp = {TYPE(rw_op_to_num(rw_operation_type::stack)),
current_state.call_id(1),
current_state.stack_size(1) - 1,
current_state.call_id(0),
current_state.stack_size(0) - 1,
TYPE(0), // storage_key_hi
TYPE(0), // storage_key_lo
TYPE(0), // field
current_state.rw_counter(1),
current_state.rw_counter(0),
TYPE(0), // is_write
A0,
A1};
B0,
B1};
lookup(tmp, "zkevm_rw");
tmp = {TYPE(rw_op_to_num(rw_operation_type::stack)),
current_state.call_id(1),
Expand All @@ -305,16 +323,16 @@ namespace nil {
TYPE(0), // field
current_state.rw_counter(1) + 1,
TYPE(0), // is_write
B0,
B1};
A0,
A1};
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
Res0,
Res1};
Expand Down
Loading

0 comments on commit bf8ad39

Please sign in to comment.