Skip to content

Commit

Permalink
mulmod constraints table
Browse files Browse the repository at this point in the history
  • Loading branch information
Antoine Cyr committed Nov 12, 2024
1 parent 9f0a018 commit 656eb71
Show file tree
Hide file tree
Showing 7 changed files with 817 additions and 177 deletions.
13 changes: 10 additions & 3 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 @@ -54,6 +54,7 @@ namespace nil {
}

using integral_type = boost::multiprecision::number<boost::multiprecision::backends::cpp_int_modular_backend<257>>;
using extended_integral_type = boost::multiprecision::number<boost::multiprecision::backends::cpp_int_modular_backend<512>>;

void apply_tester(const zkevm_opcode_tester &tester, std::size_t initial_gas = 30000000){
transactions_amount++;
Expand Down Expand Up @@ -316,8 +317,6 @@ namespace nil {
integral_type r_integral = modulus != 0u ? s_integral / integral_type(modulus) : 0u;
zkevm_word_type q = zkevm_word_type(s_integral - r_integral * integral_type(modulus));
zkevm_word_type result = modulus != 0u ? q : 0;
// zkevm_word_type result =
// integral_type(modulus) == 0 ? 0 : (a + b) % modulus;
//zkevm_word_type result = integral_type(modulus) == 0? 0 :(a + b) % modulus;
_rw_operations.push_back(stack_rw_operation(call_id, stack.size(), rw_counter++, true, result));
stack.push_back(result);
Expand All @@ -334,7 +333,15 @@ namespace nil {
zkevm_word_type modulus = stack.back();
stack.pop_back();
_rw_operations.push_back(stack_rw_operation(call_id, stack.size(), rw_counter++, false, modulus));
zkevm_word_type result = integral_type(modulus) == 0? 0 : (a * b) % modulus;
a = modulus != 0u ? a : 0;
extended_integral_type s_integral = extended_integral_type(integral_type(a)) * extended_integral_type(integral_type(b));
zkevm_word_type sp = zkevm_word_type(s_integral % extended_integral_type(zkevm_modulus));
zkevm_word_type spp = zkevm_word_type(s_integral / extended_integral_type(zkevm_modulus));
extended_integral_type r_integral = modulus != 0u ? s_integral / extended_integral_type(integral_type(modulus)): 0u;
zkevm_word_type rp = zkevm_word_type(r_integral % extended_integral_type(zkevm_modulus));
zkevm_word_type rpp = zkevm_word_type(r_integral / extended_integral_type(zkevm_modulus));
zkevm_word_type result = modulus != 0u ? zkevm_word_type(s_integral % extended_integral_type(integral_type(modulus))): 0u;
//zkevm_word_type result = integral_type(modulus) == 0? 0 : (a * b) % modulus;
_rw_operations.push_back(stack_rw_operation(call_id, stack.size(), rw_counter++, true, result));
stack.push_back(result);
pc++;
Expand Down
1 change: 1 addition & 0 deletions crypto3/libs/blueprint/include/nil/blueprint/zkevm_bbf/opcodes/addmod.hpp
View file
Original file line number Diff line number Diff line change
@@ -1,5 +1,6 @@
//---------------------------------------------------------------------------//
// Copyright (c) 2024 Alexey Yashunsky <[email protected]>
// Copyright (c) 2024 Antoine Cyr <[email protected]>
//
// MIT License
//
Expand Down
639 changes: 623 additions & 16 deletions crypto3/libs/blueprint/include/nil/blueprint/zkevm_bbf/opcodes/mulmod.hpp
View file

Large diffs are not rendered by default.

172 changes: 99 additions & 73 deletions crypto3/libs/blueprint/include/nil/blueprint/zkevm_bbf/operations/addmod.hpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -224,8 +224,7 @@ namespace nil {
128;
c_3 = static_cast<value_type>(second_row_carries);
std::vector<value_type> c_3_chunks = chunk_64_to_16<FieldType>(c_3);
N_sum =
std::accumulate(N_chunks.begin(), N_chunks.end(), value_type(0));
N_sum = std::accumulate(N_chunks.begin(), N_chunks.end(), value_type(0));
N_sum_inverse = N_sum == 0 ? 0 : N_sum.inversed();
N_nonzero = N_sum_inverse * N_sum;
// value_type
Expand All @@ -244,63 +243,80 @@ namespace nil {

// TODO: replace with memory access, which would also do range checks!
// also we can pack slightly more effectively
for (std::size_t i = 0; i < chunk_amount; i++) {
allocate(a_chunks[i], i, 0);
allocate(b_chunks[i], i, 1);
allocate(s_chunks[i], i, 2);
}
for (std::size_t i = 0; i < 2; i++) {
allocate(c_1_chunks[i], 3 * i + 3, 3);
allocate(c_1_chunks[i], 3 * i + 4, 3);
allocate(N_64_chunks[i], 3 * i + 9, 3);
allocate(N_64_chunks[i], 3 * i + 10, 3);
allocate(r_64_chunks[i], 3 * i + 19, 3);
allocate(r_64_chunks[i], 3 * i + 20, 3);
for (std::size_t i = 0; i < carry_amount - 1; i++) {
allocate(a_chunks[3 * i], 0, i);
allocate(b_chunks[3 * i], 1, i);
allocate(s_chunks[3 * i], 2, i);

allocate(a_chunks[3 * i + 1], 3, i);
allocate(b_chunks[3 * i + 1], 4, i);
allocate(s_chunks[3 * i + 1], 5, i);

allocate(a_chunks[3 * i + 2], 6, i);
allocate(b_chunks[3 * i + 2], 7, i);
allocate(s_chunks[3 * i + 2], 8, i);
}
allocate(a_chunks[chunk_amount - 1], 26, 3);
allocate(b_chunks[chunk_amount - 1], 27, 3);
allocate(s_chunks[chunk_amount - 1], 28, 3);

for (std::size_t i = 0; i < carry_amount - 1; i++) {
carry[0][i + 1] =
(carry[0][i] + a_chunks[3 * i] + b_chunks[3 * i] +
(a_chunks[3 * i + 1] + b_chunks[3 * i + 1]) * two_16 +
(a_chunks[3 * i + 2] + b_chunks[3 * i + 2]) * two_32) >= two_48;
allocate(carry[0][i + 1], 3 * i + 2, 3);
if constexpr (stage == GenerationStage::ASSIGNMENT) {
carry[0][i + 1] =
(carry[0][i] + a_chunks[3 * i] + b_chunks[3 * i] +
(a_chunks[3 * i + 1] + b_chunks[3 * i + 1]) * two_16 +
(a_chunks[3 * i + 2] + b_chunks[3 * i + 2]) * two_32) >= two_48;
}
allocate(carry[0][i], 9, i);
allocate(carry[0][i + 1], 10, i);
constrain(carry_on_addition_constraint(
a_chunks[3 * i], a_chunks[3 * i + 1], a_chunks[3 * i + 2],
b_chunks[3 * i], b_chunks[3 * i + 1], b_chunks[3 * i + 2],
s_chunks[3 * i], s_chunks[3 * i + 1], s_chunks[3 * i + 2], carry[0][i],
carry[0][i + 1], i == 0));
constrain(carry[0][i + 1] * (1 - carry[0][i + 1]));
}
carry[0][carry_amount] =
(carry[0][carry_amount - 1] + a_chunks[3 * (carry_amount - 1)] +
b_chunks[3 * (carry_amount - 1)]) >= two_16;
allocate(carry[0][carry_amount], chunk_amount - 1, 3);

if constexpr (stage == GenerationStage::ASSIGNMENT) {
carry[0][carry_amount] =
(carry[0][carry_amount - 1] + a_chunks[3 * (carry_amount - 1)] +
b_chunks[3 * (carry_amount - 1)]) >= two_16;
}
allocate(carry[0][carry_amount - 1], 29, 3);
allocate(carry[0][carry_amount], 30, 3);

constrain(last_carry_on_addition_constraint(
a_chunks[3 * (carry_amount - 1)], b_chunks[3 * (carry_amount - 1)],
s_chunks[3 * (carry_amount - 1)], carry[0][carry_amount - 1],
carry[0][carry_amount]));
constrain(carry[0][carry_amount] * (1 - carry[0][carry_amount]));

for (std::size_t i = 0; i < chunk_amount; i++) {
allocate(N_chunks[i], i + chunk_amount, 0);
for (std::size_t i = 0; i < carry_amount - 1; i++) {
allocate(N_chunks[3 * i], 11, i);
allocate(q_chunks[3 * i], 12, i);
allocate(v_chunks[3 * i], 13, i);

allocate(N_chunks[3 * i + 1], 14, i);
allocate(q_chunks[3 * i + 1], 15, i);
allocate(v_chunks[3 * i + 1], 16, i);

allocate(N_chunks[3 * i + 2], 17, i);
allocate(q_chunks[3 * i + 2], 18, i);
allocate(v_chunks[3 * i + 2], 19, i);
}
constrain(c_2 * (c_2 - 1));
constrain(c_3 * (c_3 - 1));
constrain(r_overflow * (1 - r_overflow));
constrain((first_carryless - c_1_64 * two_128_cell - c_2 * two_192_cell));
constrain(
(second_row_carries + c_1_64 + c_2 * two_64_cell - c_3 * two_128_cell));
constrain((third_row_carries + r_overflow * N_64_chunks[0] + c_3 -
s_overflow * N_sum * N_sum_inverse));
constrain(N_64_chunks[3] * r_64_chunks[3]);
allocate(N_chunks[chunk_amount - 1], 26, 4);
allocate(q_chunks[chunk_amount - 1], 27, 4);
allocate(v_chunks[chunk_amount - 1], 28, 4);

allocate(carry[1][0], chunk_amount, 3);
for (std::size_t i = 0; i < carry_amount - 1; i++) {
carry[1][i + 1] =
(carry[1][i] + N_chunks[3 * i] + v_chunks[3 * i] +
(N_chunks[3 * i + 1] + v_chunks[3 * i + 1]) * two_16 +
(N_chunks[3 * i + 2] + v_chunks[3 * i + 2]) * two_32) >= two_48;
allocate(carry[1][i + 1], 3 * i + 2 + chunk_amount, 3);
if constexpr (stage == GenerationStage::ASSIGNMENT) {
carry[1][i + 1] =
(carry[1][i] + N_chunks[3 * i] + v_chunks[3 * i] +
(N_chunks[3 * i + 1] + v_chunks[3 * i + 1]) * two_16 +
(N_chunks[3 * i + 2] + v_chunks[3 * i + 2]) * two_32) >= two_48;
}
allocate(carry[1][i], 20, i);
allocate(carry[1][i + 1], 21, i);
constrain(carry_on_addition_constraint(
N_chunks[3 * i], N_chunks[3 * i + 1], N_chunks[3 * i + 2],
v_chunks[3 * i], v_chunks[3 * i + 1], v_chunks[3 * i + 2],
Expand All @@ -309,54 +325,64 @@ namespace nil {
constrain(carry[1][i + 1] * (1 - carry[1][i + 1]));
}

carry[1][carry_amount] =
(carry[1][carry_amount - 1] + N_chunks[3 * (carry_amount - 1)] +
v_chunks[3 * (carry_amount - 1)]) >= two_16;
allocate(carry[1][carry_amount], chunk_amount * 2 - 1, 3);
if constexpr (stage == GenerationStage::ASSIGNMENT) {
carry[1][carry_amount] =
(carry[1][carry_amount - 1] + N_chunks[3 * (carry_amount - 1)] +
v_chunks[3 * (carry_amount - 1)]) >= two_16;
}
allocate(carry[1][carry_amount - 1], 29, 4);
allocate(carry[1][carry_amount], 30, 4);
constrain(last_carry_on_addition_constraint(
N_chunks[3 * (carry_amount - 1)], v_chunks[3 * (carry_amount - 1)],
q_chunks[3 * (carry_amount - 1)], carry[1][carry_amount - 1],
carry[1][carry_amount]));

// carry[1][carry_amount] is 0 or 1, but should be 1 if N_nonzero = 1
// // carry[1][carry_amount] is 0 or 1, but should be 1 if N_nonzero = 1

constrain((N_nonzero + (1 - N_nonzero) * carry[1][carry_amount]) *
(1 - carry[1][carry_amount]));
for (std::size_t i = 0; i < chunk_amount; i++) {
allocate(q_chunks[i], i + chunk_amount, 1);
allocate(N_nonzero, i + chunk_amount, 5);
}
for (std::size_t i = 0; i < chunk_amount; i++) {
allocate(v_chunks[i], i + chunk_amount, 2);

for (std::size_t i = 0; i < carry_amount - 1; i++) {
allocate(q_out_chunks[3 * i], 22, i);
allocate(q_out_chunks[3 * i + 1], 23, i);
allocate(q_out_chunks[3 * i + 2], 24, i);
}
allocate(q_out_chunks[chunk_amount - 1], 31, 4);

for (std::size_t i = 0; i < chunk_amount; i++) {
if (i % 3 == 0) {
allocate(N_nonzero, 25, i / 3);
}
constrain((N_nonzero * (q_chunks[i] - q_out_chunks[i]) +
(1 - N_nonzero) * q_out_chunks[i]));
res[i] = q_out_chunks[i];
allocate(q_out_chunks[i], i + chunk_amount, 4);
}
for (std::size_t i = 0; i < chunk_amount; i++) {
allocate(r_chunks[i], i, 4);
}

allocate(first_carryless, 32, 0);
allocate(c_1_64, 32, 1);
allocate(two_192_cell, 32, 2);
allocate(c_2, 32, 3);

allocate(second_row_carries, 33, 0);
allocate(two_64_cell, 33, 1);
allocate(two_128_cell, 33, 2);
allocate(c_3, 33, 3);

allocate(third_row_carries, 34, 0);
allocate(r_overflow, 34, 1);
allocate(N_64_chunks[0], 34, 2);
allocate(s_overflow, 34, 3);

allocate(N_sum, 35, 0);
allocate(N_sum_inverse, 35, 1);
allocate(N_64_chunks[3], 35, 2);
allocate(r_64_chunks[3], 35, 3);
allocate(c_1_64, 33, 0);
allocate(c_2, 34, 0);
constrain((first_carryless - c_1_64 * two_128 - c_2 * two_192));

allocate(second_row_carries, 32, 1);
allocate(c_3, 33, 1);
constrain((second_row_carries + c_1_64 + c_2 * two_64 - c_3 * two_128));

allocate(N_64_chunks[0], 31, 2);
allocate(third_row_carries, 32, 2);
allocate(r_overflow, 33, 2);
allocate(s_overflow, 34, 2);
allocate(N_sum, 35, 2);
allocate(N_sum_inverse, 36, 2);
constrain((third_row_carries + r_overflow * N_64_chunks[0] + c_3 -
s_overflow * N_sum * N_sum_inverse));

allocate(N_64_chunks[3], 30, 1);
allocate(r_64_chunks[3], 31, 1);
constrain(N_64_chunks[3] * r_64_chunks[3]);

constrain(c_2 * (c_2 - 1));
constrain(c_3 * (c_3 - 1));
constrain(r_overflow * (1 - r_overflow));
}
};
} // namespace bbf
Expand Down
Loading

0 comments on commit 656eb71

Please sign in to comment.