# Polygon zkEVM: Missing Remainder Constraint

{% hint style="info" %}
[**Book an audit with Zokyo**](https://www.zokyo.io/)
{% endhint %}

**Summary**

Related Vulnerabilities: 1. [Under-constrained Circuits](/zokyo-tutorials/tutorial-16-zero-knowledge-zk/common-vulnerabilities-in-zk-code/under-constrained-circuits.md), 2. [Nondeterministic Circuits](/zokyo-tutorials/tutorial-16-zero-knowledge-zk/common-vulnerabilities-in-zk-code/nondeterministic-circuits.md)

Identified By: [Spearbit](https://spearbit.com/)

The Polygon zkEVM division circuit was missing a constraint, which would allow a malicious prover to create a valid proof of a false division or modulo operation. Since the division and modulo operation are basic building blocks for the zkEVM, the prover could convince the verifier of a faulty state update.

**Background**

The Polygon zkEVM circuits are programmed using their own zk assembly language known as zkASM. Small components of the large zkEVM circuit can be broken down into different subroutines. In this case, the `divARITH` subroutine was missing a constraint.

The division subroutine is intended to constrain:

```
A * B + C = D + E
```

where:

* A = divisor
* E = dividend
* B = quotient
* C = remainder
* D = set to 0 by subroutine

The inputs `B` and `C` are free inputs chosen by the prover. `B` is supposed to be constrained to `E / A` and `C` is supposed to be constrained to `C = E % A`. This subroutine provides a way to prove the division or modulo operation.

**The Vulnerability**

The issue with this subroutine is that there is no constraint that the remainder is less than the divisor. So in this case, without the constraint, it's possible for `C >= A`. A malicious prover could set `B = E / A - 1` and `C = (E % A) + A`. This would still satisfy the equation `A * B + C = D*2**256 + E`.

A good example (taken from the [twitter explanation](https://twitter.com/SpearbitDAO/status/1679189382907953180)) is to let:

* A (divisor) = 10
* E (dividend) = 101

The expected remainder (C) is 1 and the expected quotient (B) is 10. However, a malicious prover could choose `B = 9` and `C = 11`. This would satisfy `10*9 + 11 = 101`. The code never constrains `C < A` or `11 < 10` so the proof is successful.

This kind of forgery allows a malicious prover to tweak division and modulo operations in their favor. Since division and modulo operations are basic building blocks of the EVM, this could result in many different types of hacks favorable to the prover.

**The Fix**

The original authors had a constraint that `C < E` but instead needed `C < A`. So the original code:

```
C => A ; remainder
E => B ; divisor
```

was updated to:

```
A => B ; divisor
C => A ; remainder
```

**Conclusion**

The circuit, however, had a significant oversight: it didn't enforce that the remainder $$C$$ should always be smaller than the divisor $$A$$.

Using the example provided: If you're dividing 101 by 10, you'd expect a quotient of 10 and a remainder of 1. But due to the missing constraint, a person could prove that 101 divided by 10 gives a quotient of 9 with a remainder of 11, which, while mathematically incorrect in the real world, still satisfies the equation within the zkEVM circuit.

This means that someone could manipulate the results of division and modulo operations, and since these are fundamental operations in computation, it could lead to numerous unintended consequences or hacks.

**References**

1. [Spearbit Twitter Explanation Thread](https://twitter.com/SpearbitDAO/status/1679189382907953180)


---

# Agent Instructions: Querying This Documentation

If you need additional information that is not directly available in this page, you can query the documentation dynamically by asking a question.

Perform an HTTP GET request on the current page URL with the `ask` query parameter:

```
GET https://zokyo-auditing-tutorials.gitbook.io/zokyo-tutorials/tutorial-16-zero-knowledge-zk/bugs-in-the-wild/polygon-zkevm-missing-remainder-constraint.md?ask=<question>
```

The question should be specific, self-contained, and written in natural language.
The response will contain a direct answer to the question and relevant excerpts and sources from the documentation.

Use this mechanism when the answer is not explicitly present in the current page, you need clarification or additional context, or you want to retrieve related documentation sections.