Linea Plonk Verifier

Description

Linea uses Plonk proof system, which needs a preprocessed CRS (Common Reference String) for proving and verification, the Plonk system security is based on the existence of a trusted setup ceremony to compute the CRS, the current verifier uses a CRS created by one single party, which requires fully trust of the party to delete the toxic waste (trapdoor) which can be used to generate forged proof, undermining the security of the entire system

contracts/Verifier.sol:L29-L37

uint256 constant g2_srs_0_x_0 = 11559732032986387107991004021392285783925812861821192530917403151452391805634;
uint256 constant g2_srs_0_x_1 = 10857046999023057135944570762232829481370756359578518086990519993285655852781;
uint256 constant g2_srs_0_y_0 = 4082367875863433681332203403145435568316851327593401208105741076214120093531;
uint256 constant g2_srs_0_y_1 = 8495653923123431417604973247489272438418190587263600148770280649306958101930;

uint256 constant g2_srs_1_x_0 = 18469474764091300207969441002824674761417641526767908873143851616926597782709;
uint256 constant g2_srs_1_x_1 = 17691709543839494245591259280773972507311536864513996659348773884770927133474;
uint256 constant g2_srs_1_y_0 = 2799122126101651639961126614695310298819570600001757598712033559848160757380;
uint256 constant g2_srs_1_y_1 = 3054480525781015242495808388429905877188466478626784485318957932446534030175;

Recommendation

Conduct a proper MPC to generate CRS like the Powers of Tau MPC or use a trustworthy CRS generated by an exisiting audited trusted setup like Aztec’s ignition

Description

The Verifier calculates the Lagrange Polynomial at ζ with an efficient scheme as: L_j(ζ) = ωⁱ/n * (ζⁿ-1)/(ζ-ωⁱ)

which has also been pointed out in the plonk paper. However, the computation ignores the fact that ζ can also be a root of unity, which means ζⁿ - 1 will be 0 for any ζ that is a root of unity.

Thus, the formula will yield the Lagrange polynomial evaluation as 0, which is incorrect. Because the property of the Lagrange polynomial is: L_j(ζ) = 1, if i=j and 0 otherwise, where ζ belongs to domain H = ωⁱ, ∀ 0<=i< n(n being the domain size)

Another way of calculating the Lagrange polynomial at zeta is: L_j(ζ) = y_j * ∏ _{0<= m <= k, m != j} (ζ - x_m)/(x_j-x_m); (k being the degree of polynomial)

If we consider the same evaluation for ζ at the root of unity in the second formula, it will correctly satisfy the property of the Lagrange polynomial stated above.

Hence, there is a need to fix the computation considering the case highlighted.

The problematic instances can be found in functions:

• compute_ith_lagrange_at_z
• batch_compute_lagranges_at_z
• compute_alpha_square_lagrange_0

Recommendation

Consider adopting a strategy to use the second formula for the computation of Lagrange Polynomial evaluation at ζ if ζ is a root of unity.

Description

The multiplicate inverse of an element α in a finite field Fpⁿ can be calculated as α^{pn - 2}. α can be any field element except 0 or the point at infinity.

This totally makes sense as there exists no field element x such that 0 * x = 1 mod p

However, it is allowed here and it is calculated like any other field element. It doesn’t revert, because 0 raised to any power modulo p will yield 0.

Thus the calculation points to a broken logic that defines the modular multiplicative inverse of 0 as 0.

Recommendation

The point at infinity can bring many mathematical flaws to the system. Hence require the utmost attention to be fixed.

Description

In function batch_verify_multi_points, the SNARK paring check is done by calling paring pre-compile let l_success := staticcall(sub(gas(), 2000),8,mPtr,0x180,0x00,0x20) and the only the execution status is stored in the final success state (state_success), but the the paring check result which is stored in 0x00 is not stored and checked, which means if the paring check result is 0 (pairing check failed), the proof would still pass verification, e.g. invalid proof with incorrect proof element proof_openings_selector_commit_api_at_zeta would pass the paring check. As a result it breaks the SNARK paring verification.

Examples

contracts/Verifier.sol:L586-L588

let l_success := staticcall(sub(gas(), 2000),8,mPtr,0x180,0x00,0x20)
// l_success := true
mstore(add(state, state_success), and(l_success,mload(add(state, state_success))))

Another example is, if either of the following is sent as a point at infinity or (0,0) as (x,y) co-ordinate:

• commitment to the opening proof polynomial W_z
• commitment to the opening proof polynomial W_zw

The proof will still work, since the pairing result is not being checked.

Recommendation

Verify paring check result and store it in the final success state after calling the paring pre-compile

Description

The gas supplied to the staticcall(s), is calculated by subtracting 2000 from the remaining gas at this point in time. However, if not provided enough gas, the staticcall(s) may fail and there will be no return data, and the execution will continue with the stale data that was previously there at the memory location specified by the return offset with the staticcall(s).

1- Predictable Derivation of Challenges

The function derive_gamma_beta_alpha_zeta is used to derive the challenge values gamma, beta, alpha, zeta. These values are derived from the prover’s transcript by hashing defined parameters and are supposed to be unpredictable by either the prover or the verifier. The hash is collected with the help of SHA2-256 precompile. The values are considered unpredictable, due to the assumption that SHA2-256 acts as a random oracle and it would be computationally infeasible for an attacker to find the pre-image of gamma. However, the assumption might be wrong.

Examples

contracts/Verifier.sol:L261

pop(staticcall(sub(gas(), 2000), 0x2, add(mPtr, 0x1b), size, mPtr, 0x20)) //0x1b -> 000.."gamma"

contracts/Verifier.sol:L269

pop(staticcall(sub(gas(), 2000), 0x2, add(mPtr, 0x1c), 0x24, mPtr, 0x20)) //0x1b -> 000.."gamma"

contracts/Verifier.sol:L279

pop(staticcall(sub(gas(), 2000), 0x2, add(mPtr, 0x1b), 0x65, mPtr, 0x20)) //0x1b -> 000.."gamma"

contracts/Verifier.sol:L293

pop(staticcall(sub(gas(), 2000), 0x2, add(mPtr, 0x1c), 0xe4, mPtr, 0x20))

contracts/Verifier.sol:L694

pop(staticcall(sub(gas(), 2000), 0x2, add(mPtr,start_input), size_input, add(state, state_gamma_kzg), 0x20))

If the staticcall(s) fails, it will make the challenge values to be predictable and may help the prover in forging proofs and launching other adversarial attacks.

2- Incorrect Exponentiation

Functions compute_ith_lagrange_at_z, compute_pi, and verify compute modular exponentiation by making a staticcall to the precompile modexp as:

contracts/Verifier.sol:L335

pop(staticcall(sub(gas(), 2000),0x05,mPtr,0xc0,0x00,0x20))

contracts/Verifier.sol:L441

pop(staticcall(sub(gas(), 2000),0x05,mPtr,0xc0,mPtr,0x20))

contracts/Verifier.sol:L889

pop(staticcall(sub(gas(), 2000),0x05,mPtr,0xc0,mPtr,0x20))

However, if not supplied enough gas, the staticcall(s) will fail, thus returning no result and the execution will continue with the stale data.

3. Incorrect Point Addition and Scalar Multiplication

contracts/Verifier.sol:L555

pop(staticcall(sub(gas(), 2000),7,folded_evals_commit,0x60,folded_evals_commit,0x40))

contracts/Verifier.sol:L847

let l_success := staticcall(sub(gas(), 2000),6,mPtr,0x80,dst,0x40)

contracts/Verifier.sol:L858

let l_success := staticcall(sub(gas(), 2000),7,mPtr,0x60,dst,0x40)

contracts/Verifier.sol:L868

let l_success := staticcall(sub(gas(), 2000),7,mPtr,0x60,mPtr,0x40)

contracts/Verifier.sol:L871

l_success := and(l_success, staticcall(sub(gas(), 2000),6,mPtr,0x80,dst, 0x40))

For the same reason, point_add, point_mul, and point_acc_mul will return incorrect results. Matter of fact, point_acc_mul will not revert even if the scalar multiplication fails in the first step. Because, the memory location specified for the return offset, will still be containing the old (x,y) coordinates of src, which are points on the curve. Hence, it will proceed by incorrectly adding (x,y) coordinates of dst with it.

However, it will not be practically possible to conduct a gas griefing attack for staticcall(s) at the start of the top-level transaction. As it will require an attacker to pass a very low amount of gas to make the staticcall fail, but at the same time, that would not be enough to make the top-level transaction execute entirely and not run out of gas. But, this can still be conducted for the staticcall(s) that are executed at the near end of the top-level transaction.

Recommendation

1. Check the returned status of the staticcall and revert if any of the staticcall’s return status has been 0.
2. Also fix the comments mentioned for every staticcall, for instance: the function derive_beta says 0x1b -> 000.."gamma" while the memory pointer holds the ASCII value of string beta

Description

The verifier currently supports single BSB22 commitment as Gnark only supports single Commit(..) call. If there is no or multiple BSB22 commitments/Commit calls, the verifier would fail in proof verification.

Examples

tmpl/template_verifier.go:L57-L58

uint256 constant vk_selector_commitments_commit_api_0_x = {{ (fpptr .Qcp.X).String }};
uint256 constant vk_selector_commitments_commit_api_0_y = {{ (fpptr .Qcp.Y).String }};

Recommendation

Add support for zero or multiple BSB22 commitments

Description

There are no test cases for invalid proof and public input such as proof elements not on curve, proof element is points of infinity, all proof elements are zero, wrong proof element, proof scalar element bigger than scalar field modulus, proof scalar element wrapping around scalar field modulus, public input greater than scalar field modulus etc. and no or multiple BSB22 commitments. There is only test for valid proof and one BSB22 commitment. Tests for all edge cases are crucial to check proof soundness in SNARK, missing it may result in missing some critical bugs, e.g. issue issue 4.4 issue issue 4.6

Recommendation

Add missing test cases

Description

There is no field element range check on scalar field proof elements e.g. proof_l_at_zeta, proof_r_at_zeta, proof_o_at_zeta, proof_s1_at_zeta,proof_s2_at_zeta, proof_grand_product_at_zeta_omega as mentioned in the step 2 of the verifier’s algorithm in the Plonk paper. The scalar multiplication functions point_mul and point_acc_mul call precompile ECMUL, according to EIP-169 , which would verify the point P is on curve and P.x and P.y is less than the base field modulus, however it doesn’t check the scalar s is less than scalar field modulus, if s is greater than scalar field modulus r_mod, it would cause unintended behavior of the contract, specifically if the scalar field proof element e are replaced by e + r_mod, the proof would still pass verification. Although in Plonk’s case, there is few attacker vectors could exists be based on this kind of proof malleability.

Examples

contracts/Verifier.sol:L852-L873

function point_mul(dst,src,s, mPtr) {
  // let mPtr := add(mload(0x40), state_last_mem)
  let state := mload(0x40)
  mstore(mPtr,mload(src))
  mstore(add(mPtr,0x20),mload(add(src,0x20)))
  mstore(add(mPtr,0x40),s)
  let l_success := staticcall(sub(gas(), 2000),7,mPtr,0x60,dst,0x40)
  mstore(add(state, state_success), and(l_success,mload(add(state, state_success))))
}

// dst <- dst + [s]src (Elliptic curve)
function point_acc_mul(dst,src,s, mPtr) {
  let state := mload(0x40)
  mstore(mPtr,mload(src))
  mstore(add(mPtr,0x20),mload(add(src,0x20)))
  mstore(add(mPtr,0x40),s)
  let l_success := staticcall(sub(gas(), 2000),7,mPtr,0x60,mPtr,0x40)
  mstore(add(mPtr,0x40),mload(dst))
  mstore(add(mPtr,0x60),mload(add(dst,0x20)))
  l_success := and(l_success, staticcall(sub(gas(), 2000),6,mPtr,0x80,dst, 0x40))
  mstore(add(state, state_success), and(l_success,mload(add(state, state_success))))
}

Recommendation

Add scalar field range check on scalar multiplication functions point_mul and point_acc_mul or the scalar field proof elements.

Description

The public input is an array of uint256 numbers, there is no check if each public input is less than SNARK scalar field modulus r_mod, as mentioned in the step 3 of the verifier’s algorithm in the Plonk paper. Since public inputs are involved computation of Pi in the plonk gate which is in the SNARK scalar field, without the check, it might cause scalar field overflow and the verification contract would fail and revert. To prevent overflow and other unintended behavior there should be a range check for the public inputs.

Examples

contracts/Verifier.sol:L470

function Verify(bytes memory proof, uint256[] memory public_inputs)

contracts/Verifier.sol:L367-L383

sum_pi_wo_api_commit(add(public_inputs,0x20), mload(public_inputs), zeta)
pi := mload(mload(0x40))

function sum_pi_wo_api_commit(ins, n, z) {
  let li := mload(0x40)
  batch_compute_lagranges_at_z(z, n, li)
  let res := 0
  let tmp := 0
  for {let i:=0} lt(i,n) {i:=add(i,1)}
  {
    tmp := mulmod(mload(li), mload(ins), r_mod)
    res := addmod(res, tmp, r_mod)
    li := add(li, 0x20)
    ins := add(ins, 0x20)
  }
  mstore(mload(0x40), res)
}

Recommendation

Add range check for the public inputs require(input[i] < r_mod, "public inputs greater than snark scalar field");

Description

There is no prime field element check and on curve point for proof elements proof_l_com_x, proof_l_com_y,proof_r_com_x,proof_r_com_y, proof_o_com_x, proof_o_com_y, proof_h_0_x, proof_h_0_y,proof_h_1_x, proof_h_1_y,proof_h_2_x, proof_h_2_y, proof_batch_opening_at_zeta, proof_opening_at_zeta_omega, proof_selector_commit_api_commitment, as mentioned in

step 1 Validate ([a]1, [b]1, [c]1, [z]1, [tlo]1, [tmid]1, [thi]1, [Wz]1, [Wzω]1) ∈ G9

of the verifier’s algorithm in the Plonk paper. Although there is field element check and curve point check in ECCADD, ECCMUL and ECCParing precompiles on those elements, in which the precompile would revert on failed check but it would consume gas on revert and there is no error information. It’s better to check explicitly and revert on fail to prevent unintended behavior of the verification contract.

Recommendation

Add field element, group element and curve point check for proof elements and revert if the check fails.
`

Description

The Verify function has the following signature:

function Verify(bytes memory proof, uint256[] memory public_inputs)

Here, proof is a dynamically sized array of bytes (padded upto the nearest word). The function derive_gamma(aproof, pub_inputs) uses this array and makes some assumptions about its length. Specifically, that it is (vk_nb_commitments_commit_api * 3 * 0x20) + 0x360 bytes long (when including the initial length field of the bytes array). However, there is no check that the proof supplied in the calldata (which originates within ZkEvmV2 where it is loaded into memory) has the correct length. This could result in the proof and pub_inputs overlapping in memory, leading to unintended consequences.

Also, if mistakenly appended extra bits to the proof, it will not affect the proof verification as the Verifier doesn’t account for any extra bits after the y coordinate of the last commitment. But it will surely make the verification expensive, as it will still be copied down into memory.

Recommendation

Add an appropriate length check at some point in the pipeline to ensure this doesn’t cause any unintended problems.

Description

The Verifier stores the result of computations obtained in different steps of Verifier algorithm. The result is stored at a designated memory location state_success by doing bitwise & with the previous result, and if the final result at the end of all the steps comes out to be 1 or true, it verifies the proof.

However, it makes no sense to continue with the rest of the operations, if any step results into a failure, as the proof verification will be failing anyways. But, it will result into wastage of more gas for the zkEVM Operator.

The functions which update the state_success state are:

• point_mul
• point_add
• point_acc_mul
• verify_quotient_poly_eval_at_zeta
• batch_verify_multi_points

Recommendation

It would be best to revert, the moment any step fails.

Description

Function load_wire_commitments_commit_api as the name suggests, loads wire commitments from the proof into the memory array wire_commitments. The array is made to hold 2 values per commitment or the size of the array is 2 * vk_nb_commitments_commit_api, which makes sense as these 2 values are the x & y co-ordinates of the commitments.

contracts/Verifier.sol:L453-L454

uint256[] memory wire_committed_commitments = new uint256[](2*vk_nb_commitments_commit_api);
load_wire_commitments_commit_api(wire_committed_commitments, proof);

Coming back to the functionload_wire_commitments_commit_api, it extracts both the x & y coordinates of a commitment in a single iteration. However, the loop runs 2 * vk_nb_commitments_commit_api, or in other words, twice as many of the required iterations. For instance, if there is 1 commitment, it will run two times. The first iteration will pick up the actual coordinates and the second one can pick any arbitrary data from the proof(if passed) and load it into memory. Although, this data which has been loaded in an extra iteration seems harmless but still adds an overhead for the processing.

contracts/Verifier.sol:L307

for {let i:=0} lt(i, mul(vk_nb_commitments_commit_api,2)) {i:=add(i,1)}

Recommendation

The number of iterations should be equal to the size of commitments, i.e., vk_nb_commitments_commit_api. So consider switching from:

for {let i:=0} lt(i, mul(vk_nb_commitments_commit_api,2)) {i:=add(i,1)}

to:

for {let i:=0} lt(i, vk_nb_commitments_commit_api) {i:=add(i,1)}

Description

The function compute_pi calculates public input polynomial evaluation at 𝜁 without api commit as: PI(𝜁) = ∑_i∈[ℓ] ω_iL_i(𝜁)

The function first calculates: n^-1 * (𝜁ⁿ-1)

and then calls a function batch_invert to find modular multiplicate inverses of: 𝜁 - ωⁱ where 0 < i < n ; n is the number of public inputs and 𝜁⁰ = 1.

The explanation of which is provided by the author as:

Ex: if ins = [a₀, a₁, a₂] it returns [a₀^{-1},a₁^{-1}, a₂^{-1}] (the aᵢ are on 32 bytes)
mPtr is the free memory to use.

It uses the following method (example with 3 elements):
* first compute [1, a₀, a₀a₁, a₀a₁a₂]
* compute u := (a₀a₁a₂)^{-1}
* compute a₂^{-1} = u*a₀a₁, replace u by a₂*u=(a₀a₁)^{-1}
* compute a₁^{-1} = u*a₀, replace u by a₁*u = a₀^{-1}
* a₀^{-1} = u

However, it doesn’t account for the fact that elements passed to the function can be 0 as well. The reason is, 𝜁 can be a root of unity. Since the function first calculates an aggregated inverse, thus even if a single element is 0, the aggregated inverse will be 0, and thus all the individual inverses will be 0, which is contrary to the desired logic of finding individual inverses.

Recommendation

Consider fixing the computation as per the recommendations in issue 4.2

Description

There are three state fields which exist but are neither defined nor used in the computation:

• state_su and state_sv
• state_alpha_square_lagrange_one

It is unclear whether or not these were intended to play a part or not.

Examples

contracts/Verifier.sol:L138-L140

// challenges related to KZG
uint256 constant state_sv = 0x80;
uint256 constant state_su = 0xa0;

contracts/Verifier.sol:L166

uint256 constant state_alpha_square_lagrange_one = 0x200;

Recommendation

Description

In the function verify_quotient_poly_eval_at_zeta(aproof) we have the following two lines at the end:

mstore(add(state, state_success), mload(computed_quotient))
mstore(add(state, state_success),eq(mload(computed_quotient), mload(s2)))

In essence, this is writing to the state_success variable twice and, hence, the first assignment is lost. Its unclear to me what exactly was intended here, but I’m assuming the first assignment can be removed.

Examples

Recommendation

Determine the correct course of action: either removing the first assignment, or using an and() to combine the two values together.

Description

Running make solc creates a PlonkVerifier.abi file that is empty ([]). This seems correct for the existing Verifier.sol file. In contrast, the committed PlonkVerifier.abi refers to a function PrintUint256 that is not in the current Verifier.sol.

This probably means that the committed PlonkVerifier.abi was generated from a different Verifier.sol file. It would be good to make sure that the committed files are correct.

Possibly related: the .bin files generated (using 0.8.19+commit.7dd6d404.Darwin.appleclang) are different from the committed ones, so they probably are also out of sync. Else, the exact compiler used should be documented.

Examples

Recommendation

Document the compiler used. Ensure that the committed files are consistent. Ensure that there is a single source of truth (1 solidity file + compiler is better than 1 solidity file + 1 bin file that can get out of sync).

Description

The target all in the Makefile ostensibly wants to run the targets clean and solc in that order.

all: clean solc

However prerequisites in GNU Make are not ordered, and they might even run in parallel. In this case, this could cause spurious behavior like overwrite errors or files being deleted just after being created.

Recommendation

The Make way to ensure that targets run one after the other is

all: clean
	$(MAKE) solc

Also all should be listed in the PHONY targets.

Description

The Verifier can be compiled with any minor version of compiler 0.8. It may lead to inconsistent behavior or produce unintended results, due to the bugs that have been identified in specific compiler versions. For instance, an optimizer bug that was discovered in 0.8.13, which effects unused memory/storage writes in an inline assembly block, which is similar to the pattern being followed by the Verifier. Although, we have not observed a negative effect of the said bug, but we still recommend working with a fixed compiler version, to avoid potential compiler-specific issues.

contracts/Verifier.sol:L17

pragma solidity ^0.8.0;

Recommendation

The contract should be tested and compiled with a fixed compiler version

Description

We have observed some deviations in the implementation in some computations w.r.t the intended approach described by the author and also with the Plonk Paper. We have also observed some computations which require a thorough lookup

1- Function compute_gamma_kzg defines the process to derive an unpredictable value gamma with the following inputs mentioned by the authors

The process for deriving γ is the same as in derive_gamma but this time the inputs are
in this order (the [] means it's a commitment):
* ζ
* [H] ( = H₁ + ζᵐ⁺²*H₂ + ζ²⁽ᵐ⁺²⁾*H₃ )
* [Linearised polynomial]
* [L], [R], [O]
* [S₁] [S₂]
* [Pi_{i}] (wires associated with custom gates)
Then there are the purported evaluations of the previously committed polynomials:
* H(ζ)
* Linearised_polynomial(ζ)
* L(ζ), R(ζ), O(ζ), S₁(ζ), S₂(ζ)
* Pi_{i}(ζ)

However, instead of using [Pi_i] and Pi_i(ζ), i.e., commitments to the custom gates’ wire values and their evaluations at ζ, the function uses [Qc_i] and Qc_i(ζ), which are the commitments to the custom gates’ selectors and their evaluations at ζ

contracts/Verifier.sol:L669-L671

mstore(add(mPtr,offset), vk_selector_commitments_commit_api_0_x)
mstore(add(mPtr,add(offset, 0x20)), vk_selector_commitments_commit_api_0_y)
offset := add(offset, 0x40)

2- Approach to compute linearized polynomial

Compute the commitment to the linearized polynomial equal to
L(ζ)[Qₗ]+r(ζ)[Qᵣ]+R(ζ)L(ζ)[Qₘ]+O(ζ)[Qₒ]+[Qₖ]+Σᵢqc'ᵢ(ζ)[BsbCommitmentᵢ] +
α*( Z(μζ)(L(ζ)+β*S₁(ζ)+γ)*(R(ζ)+β*S₂(ζ)+γ)[S₃]-[Z](L(ζ)+β*id_{1}(ζ)+γ)*(R(ζ)+β*id_{2(ζ)+γ)*(O(ζ)+β*id_{3}(ζ)+γ) ) +
α²*L₁(ζ)[Z]

Unlike the other assignment polynomials, where the input polynomial evaluation at ζ is multiplied by its respective selector commitment, For instance: L(ζ)[Q_l]

In the case of custom gates, it is being computed in reverse as: Qc_i(ζ)[Pi_i]

contracts/Verifier.sol:L726-L735

let commits_api_at_zeta := add(aproof, proof_openings_selector_commit_api_at_zeta)
let commits_api := add(aproof, add(proof_openings_selector_commit_api_at_zeta, mul(vk_nb_commitments_commit_api, 0x20)))
for {let i:=0} lt(i, vk_nb_commitments_commit_api) {i:=add(i,1)}
{
  mstore(mPtr, mload(commits_api))
  mstore(add(mPtr, 0x20), mload(add(commits_api, 0x20)))
  point_acc_mul(l_state_linearised_polynomial,mPtr,mload(commits_api_at_zeta),add(mPtr,0x40))
  commits_api_at_zeta := add(commits_api_at_zeta, 0x20)
  commits_api := add(commits_api, 0x40)
}

3- Approach to compute linearized polynomial and quotient polynomial evaluation at zeta

The signs for the parts of the expressions to compute r̄ are reversed, if compared with the plonk paper

* s₁ = α*Z(μζ)(l(ζ)+β*s₁(ζ)+γ)*(r(ζ)+β*s₂(ζ)+γ)*β
* s₂ = -α*(l(ζ)+β*ζ+γ)*(r(ζ)+β*u*ζ+γ)*(o(ζ)+β*u²*ζ+γ) + α²*L₁(ζ)

And the sign for the term in t¯ computation has been reversed as well: αz¯w(l¯+βs¯σ1+γ)(r¯+βs¯σ2+γ)(o¯+γ)

contracts/Verifier.sol:L832

mstore(computed_quotient, addmod(mload(computed_quotient), mload(s1), r_mod))

contracts/Verifier.sol:L782

s2 := sub(r_mod, s2)

Recommendation

There is a need to thoroughly review the highlighted code sections

Description

The Linearization Polynomial evaluation at zeta (r¯) can be removed from the proof as the verifier computes the Linearization Polynomial anyways. The Verifier’s algorithm in the latest release of the plonk paper has also been updated, considering the same. However, it might require changing/adjusting a lot of code sections, hence it is not recommended for the current version of the verifier but definitely can be considered for future updates.

Description

Function verify_quotient_poly_eval_at_zeta tries to find whether m¯+PI(ζ)+αz¯w(l¯+βs¯σ1+γ)(r¯+βs¯σ2+γ)(o¯+γ)−L1(ζ)α2 is equal to t¯ZH(ζ) or not, where x¯=x(ζ) and m¯ is the linearization polynomial evaluation at ζ

However, instead of directly working with local assembly variables, the function uses memory operations mload and mstore which is unnecessary and adds gas overhead for the calculations.

For instance,

# With memory

let s1 := add(mload(0x40), state_last_mem)
mstore(s1, mulmod(mload(add(aproof,proof_s1_at_zeta)),mload(add(state, state_beta)), r_mod))
mstore(s1, addmod(mload(s1), mload(add(state, state_gamma)), r_mod))
mstore(s1, addmod(mload(s1), mload(add(aproof, proof_l_at_zeta)), r_mod))

# Without memory

let s1 := mulmod(mload(add(aproof,proof_s1_at_zeta)),mload(add(state, state_beta)), r_mod)
s1:= addmod(s1, mload(add(state, state_gamma)), r_mod)
s1:= addmod(s1, mload(add(aproof, proof_l_at_zeta)), r_mod)

Also, the function stores the computed quotient at the memory location of state_success as:

mstore(add(state, state_success), mload(computed_quotient))

It is unnecessary as it is logically reserved for the calculation results, and also because of the next line which is actually storing the desired comparison result.

mstore(add(state, state_success),eq(mload(computed_quotient), mload(s2)))

Recommendation

The same calculations can be achieved by simply using the local assembly variables. Also, the unnecessary memory written to state_success for computed_quotient mentioned above can be removed.

Description

The solidity variable zeta_power_n_minus_one is defined at Line 361, and calculated at Lines 445 and 446. However, this variable does not appear to be actually used anywhere. Instead, there are several places where the value is recalculated from scratch.

Examples

contracts/Verifier.sol:L361

uint256 zeta_power_n_minus_one;

contracts/Verifier.sol:L445-L446

zeta_power_n_minus_one := pow(zeta, vk_domain_size, mload(0x40))
zeta_power_n_minus_one := addmod(zeta_power_n_minus_one, sub(r_mod, 1), r_mod)

Recommendation

Presumably, this variable can be removed without any consequences.

Description

There are two examples of debugging code left within the code base.

Examples

check := mload(add(mem, state_check_var))

mstore(add(state, state_check_var), acc_gamma)

mstore(add(state, state_check_var), mload(add(folded_quotients, 0x20)))

Recommendation

Remove debugging code prior to deployment.

Descriptions and Recommendations

The contract defines function hash_fr to calculate field elements over finite field F from message hash, expanded with expand_msg. However, we found opportunities for a couple of code improvements that may enhance code readability.

A. The following code excerpt prepends a byte string of 64 zeroes for the padding Z_pad

contracts/Utils.sol:L39-L41

for (uint i=0; i<64; i++){
    tmp = abi.encodePacked(tmp, zero);
}

However, as it is a static value and need not be calculated dynamically, it can be simplified by predefining it as an initial value for tmp as:

bytes memory tmp = hex'00000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000';

B. The following code excerpt performs a xor operation with b0 and b1 bytes32 hash strings in a for a loop.

contracts/Utils.sol:L51-L56

tmp = abi.encodePacked(uint8(b0[0]) ^ uint8(b1[0]));
for (uint i=1; i<32; i++){
    tmp = abi.encodePacked(tmp, uint8(b0[i]) ^ uint8(b1[i]));
}

tmp = abi.encodePacked(tmp, uint8(2), dst, sizeDomain);

Instead of performing xor operation byte-by-byte, solidity provides the capability to xor the whole fixed byte string at once, hence it can be simplified as:

bytes32 xorTmp = b0 ^ b1;
tmp = abi.encodePacked(xorTmp, uint8(2), dst, sizeDomain);