Mathemagic: Chinese Remainder Theorem
A lot of smart contracts use the SafeMath library. It prevents contracts from having incorrect results, but it does so by failing transactions instead of making them correct. Let’s instead try to do the math correct. In this series I will derive some advanced techniques. The Chinese Remainder Theorem is important in these, so I will introduce it first.
Sufficiently advanced mathematics is indistinguishable from magic.
— Arthur C. Clarke’s 3rd law (edited)
Warning: This is a very mathematical post. Follow up posts will build on the results derived here, but will not be that math heavy.
Notation: I use square brackets with a subscript for the modulo operation. I do this mostly because the conventional notation is cumbersome for nested expressions. The notation is inspired by Iverson’s notation for the floor and ceiling functions,⌊a⌋, and ⌈b⌉ respectively. In typeset math, the floor, ceil and mod-m operations look like:
Chinese Remainder Theorem
Given two coprime numbers m₀ and m₁, any number x less than m₀ · m₁ can be uniquely written as a pair (x₀, x₁):
From this pair, the original number can be reconstructed as:
This is known as the Chinese Remainder Theorem. In fact, it is a special case with only two moduli, the full theorem can have any number of ms as basis. For completeness, here is the full theorem as I expressed it almost a decade ago:
A special modular basis
The trick I discovered is to use this theorem with a basis m₀ and m₁ such that m₁ = m₀ — 1 and thus m₀ = m₁ + 1. This allows for very easy computation, for example they have nice inverses (you can convince yourself of their correctness by computing m₁ · m₁ and m₀ · 1, expanding the result, and taking the modulus.):
This simplifies the before mentioned reconstruction formula to:
If we substitute m₁ = m₀ — 1 and do a bit of algebra it reduces to:
The modulo operation now has a large modulus compared to the number inside the brackets. The only time it can ‘wrap around’ is when x₁ < x₀ and then only once. When this happens, we need to add an single extra modulus term, m₀² — m₀, to get a positive result again. To get rid of the modulo operation, we introduce a variable c that is 1 when we need to add the modulus and zero otherwise:
This is the reconstruction formula for any basis where m₁ = m₀ — 1. From here on, I use the specific basis m₀ = 2²⁵⁶ and thus m₁ = 2²⁵⁶ — 1. This is, in a way, the largest and best basis possible in the EVM. It also turns out to lead to even more simplification in the next step.
Output
We now have the full number x in theory, but this number is to big to represent directly in code. To represent it, we want to split it in the least significant and most significant bits of x. I will call these r₀ and r₁ respectively. In a 256 bit machine like the EVM they are defined as:
If we substitute the reconstruction formula from above, fill in the modular basis and realize that there is an implicit modulo m₀, almost everything cancels out. (do verify if you are not convinced):
As mentioned earlier, c is one if x₁ < x₀ and zero otherwise. That is all there is to it; trivially simple!
Conclusion
So, to summarize, if we know a number modulo 2²⁵⁶ and 2²⁵⁶ — 1, we can convert that to a 512 bit number with the above two equations. This works iff the number is less than 2²⁵⁶ · (2²⁵⁶ — 1). In solidity the reconstruction algorithm is as follows:
The Solidity compiler, as of version 0.4.18, does not produce very optimal code here. It introduces a conditional jump that is entirely avoidable. It can be hand-optimized as:
Two subtractions and one comparisons. This is practically for free in terms of gas!
In the next post, I will use this theorem to build a full 512 bit multiplication in Solidity. It will take just two more instructions, can you guess which?
If you enjoy these posts and/or want to encourage me to write more, please clap & follow!
