Include section on arithmetic checks #237

0xPhaze · 2023-03-07T12:39:17Z

This section is part of learn-evm. It includes a guide on how arithmetic checks can be performed in the EVM and how integers are handled in the EVM in general.

CLAassistant · 2023-03-07T12:39:22Z

All committers have signed the CLA.

montyly · 2023-03-22T09:15:23Z

@bohendo : can you do a first pass of review?

bohendo · 2023-03-23T11:47:24Z

learn_evm/arithmetic-checks.md

+This is equivalent, because `type(uint256).max` is a 256-bit integer with all its bits set to `1`.
+Subtracting `b` from `type(uint256).max` can be viewed as inverting each bit in `b`.
+This can be demonstrated by the transformation `~b = ~(0 ^ b) = ~0 ^ b = MAX ^ b = MAX - b`.
+> It's worth noting that `a - b = a ^ b` is **NOT** a general rule, except in special cases, such as when one of the values `MAX`.


s/values `MAX`/values is `MAX`/

bohendo · 2023-03-23T11:49:28Z

learn_evm/arithmetic-checks.md

+```
+
+Nevertheless, by utilizing `xor`, which is the bitwise exclusive-or operation, we can combine these checks into one.
+The code is written in assembly, because Solidity lacks an `xor` operation for boolean values.


Isn't ^ the xor operator in solidity?

Hmm ^ is the bitwise xor, which might be different than "xor for boolean values"? If so, adding a sentence here to distinguish between bitwise and boolean xor would be illuminating.

Yes, but it's not possible to write a ^ b where a or b are booleans.
Maybe re-phrasing might make it clearer?
"Nevertheless, using the boolean exclusive-or lets us combine these checks into one step. Solidity doesn't have a built-in operation for boolean values, but we can still make use of it through inline-assembly. In doing so, we need to take care that both inputs are actually boolean (either 0 or 1), as the xor operation works bitwise and isn't restricted to boolean values."

bohendo

This is an extremely informative page, great job! I left a few editorial/formatting nitpicks in this review + a couple stand-alone comments but besides those, this looks good to go

bohendo · 2023-03-23T12:12:19Z

learn_evm/arithmetic-checks.md

+}
+```
+
+When it comes to integer multiplication, it's important to handle the case hen `a < 0` and `b == type(int256).min`.


s/hen/when/

bohendo · 2023-03-23T12:15:26Z

learn_evm/arithmetic-checks.md

+= 0x????????????????????????????????????????????????0000000000000001 // int64(1)
+```
+
+> It is crucial to be mindful of when to clean the bits before and after operations. 


If these block quotes refer text from external sources, it'd be informative to include links to them. Otherwise, we might want to adjust the formatting so it doesn't look like we're quoting another source.

No, I didn't have any external sources for this. I removed the block quotes in this case. I generally just used them for extra trivia/further information.

0xPhaze · 2023-03-23T16:14:41Z

Failing CI seems to be unrelated & due to slither itself.

montyly

Partial review

montyly · 2023-03-25T09:51:25Z

learn_evm/arithmetic-checks.md

@@ -0,0 +1,668 @@
+# A Guide on Performing Arithmetic Checks in the EVM
+
+The EVM is a peculiar machine that many of us have come to love and hate for all its quirks.


We should re-word the introduction. secure-contract is meant to be objective, so we should avoid this type of description

montyly · 2023-03-25T09:52:19Z

learn_evm/arithmetic-checks.md

+Although opcodes for signed integers (such as `sdiv`, `smod`, `slt`, `sgt`, etc.) exist,
+arithmetic checks must be implemented within the constraints of the EVM.
+
+> Note: [EIP-1051](https://eips.ethereum.org/EIPS/eip-1051)'s goal is to introduce the opcodes `ovf` and `sovf`.


This EIP has not be discussed with 2021, I think we can remove the note

I still find it interesting to include the note that there at least had been a discussion around including native operations. I added the remark that the status is stagnant here. Do you still want me to remove this?

Imho, it's interesting, but it breaks the flow of read. This is the beginning of the doc, and if you start by pointing out EIP that will (most likely) not be included, it makes more difficult to follow.

Maybe we can add a conclusion to this document, with

A tldr

Some references

the wikipedia page to the two's complement system (or similar)

this EIP

anything else that is relevant

montyly · 2023-03-25T10:04:40Z

learn_evm/arithmetic-checks.md

+> We also obtain the relation `~b + 1 = 0 - b = -b` if we add `1` mod `2**256` to both sides of the previous equation.
+
+By computing the result of the addition first and then performing a check on the sum,
+modern versions of Solidity can eliminate the need for performing extra arithmetic operations in the comparison.


why modern versions of Solidity? (0.8.16?)

can eliminate the need for performing extra arithmetic operations in the comparison I am not sure what we mean here. My assumption is that its cheaper to do the + and then the check, that to do a separate check, and then the +, but its not clear if its what we are trying to convey here.

yes, 0.8.16 as seen in the code comment below. And that's pretty much what I mean. The code below doesn't need additional operations before the comparison. But I agree, it's a bit hard to understand, I'll try to re-phrase it.

montyly · 2023-03-25T10:13:35Z

learn_evm/arithmetic-checks.md

+= 0x0000000000000000000000000000000000000000000000000000000000000000
+```
+
+Newer versions of Solidity prevent integer overflow by using the computed result `c = a + b` to check for overflow/underflow.


What are the newer versions here? (0.8.16?)
Remind that this page will be still published when solidity 10 will be released ;)

What do you mean by solidity 10? Solidity v0.10.0?

Would you always prefer to have the versions included in the text? I moved them to the code instead to de-clutter and to make it clearer where exactly they belong to.

yes I meant 0.10.0. My point is that this text will still be here in 1 year, so it's better to avoid "new version"/"older version" etc, because it won't make sense later.

Adding the version in both the text and the code snippet is probably our best solution here

montyly · 2023-03-25T10:18:30Z

learn_evm/arithmetic-checks.md

+```
+
+Nevertheless, using the boolean exclusive-or lets us combine these checks into one step.
+Solidity doesn't have a built-in operation for boolean values, but we can still make use of it through inline-assembly. In doing so, we need to take care that both inputs are actually boolean (either 0 or 1), as the xor operation works bitwise and isn't restricted to boolean values.


I think this is confusing Solidity doesn't have a built-in operation for boolean values, as you can use && and || on booleans. Maybe solidity doesn't have built-in for boolean xor?

Ah, good catch, this was a bit messed up due to my latest push.

montyly · 2023-03-25T10:22:01Z

learn_evm/arithmetic-checks.md

+}
+```
+
+> It's important to note that the Solidity compiler always includes a division by zero check for all division and modulo operations, regardless of the presence of an unchecked block.


division by zero and modulo by zero check maybe? saying "a division by zero" check on a modulo is a bit confusing ;) (even if its not false)

montyly · 2023-03-25T10:22:50Z

learn_evm/arithmetic-checks.md

+
+## Arithmetic checks for int256 multiplication
+
+In older versions, the Solidity compiler uses four separate checks to detect integer multiplication overflow.


what are the older versions? <0.8.17?

I included the exact versions in the code snippet, didn't want to clutter the text.

montyly · 2023-03-25T10:23:08Z

learn_evm/arithmetic-checks.md

+}
+```
+
+Newer Solidity versions optimize the process by utilizing the computed product in the check.


what are newer versions? 0.8.17?

learn_evm/arithmetic-checks.md

montyly

review finished ;) great work overall

montyly · 2023-04-10T07:47:09Z

learn_evm/arithmetic-checks.md

+We can simplify the expression to a single comparison if we're able to shift the disjointed number domain back so that it's connected.
+To accomplish this, we subtract the smallest negative int64 `type(int64).min` from a value (or add the underlying unsigned value).
+A better way to understand this is by visualizing the signed integer number domain in relation to the unsigned domain (which is demonstrated here using int128).
+


This does not render well on github

montyly · 2023-04-14T11:24:48Z

learn_evm/arithmetic-checks.md

@@ -0,0 +1,717 @@
+# A Guide on Performing Arithmetic Checks in the EVM
+
+The Ethereum Virtual Machine (EVM) distinguishes itself from traditional computer systems and virtual machines through several unique aspects.


I would remove "from traditional computer systems" - it sounds a bit weird

montyly · 2023-04-14T11:25:50Z

learn_evm/arithmetic-checks.md

+One notable difference is its treatment of arithmetic checks.
+While most architectures and virtual machines provide access to carry bits or an overflow flag,
+these features are absent in the EVM.
+Consequently, developers must manually incorporate these safeguards within the machine's constraints.


developers is a bit misleading here. In practice developers who use solidity don't need to care about it

montyly · 2023-04-14T11:28:08Z

learn_evm/arithmetic-checks.md

+
+In conclusion, we hope this article has served as an informative guide on signed integer arithmetic within the EVM and the two's complement system. We have seen the added complexity that is introduced when performing checked arithmetic on signed integers compared to unsigned ones and when dealing with sub-32 byte types.
+
+As the trend in Solidity smart contract development leans towards low-level optimizations, it is important to emphasize the diligence required when implementing these techniques. The aim of this article is to deepen one's understanding of low-level arithmetic, thereby improving the security of Solidity code by enabling developers to better assess and comprehend the assumptions present in these operations. However, it is crucial to remember that custom low-level optimizations should be integrated only after rigorous manual analysis, fuzzing, and symbolic verification. Additionally, any non-obvious assumptions should always be clearly documented.


These points are important, but it feels like we could shorten this paragraph.

montyly · 2023-04-14T11:28:53Z

learn_evm/arithmetic-checks.md

+
+## Conclusion
+
+In conclusion, we hope this article has served as an informative guide on signed integer arithmetic within the EVM and the two's complement system. We have seen the added complexity that is introduced when performing checked arithmetic on signed integers compared to unsigned ones and when dealing with sub-32 byte types.


maybe we should use a bullet list here to highlight the lessons learned - I think it would make it more readable.

MindlessSteel · 2023-05-12T19:42:25Z

This isa big help for self taught
Older people like me,I am focusing on solidity for doing any smart contracts in the future!
Good work 👍

Include section on arithmetic checks

fb41278

0xPhaze requested review from bohendo and montyly as code owners March 7, 2023 12:39

0xPhaze added 3 commits March 7, 2023 13:41

fix: consistent order in ToC

3301324

fix: include small changes

3a8f8ab

fix: remove book submodule

c333b8f

bohendo reviewed Mar 23, 2023

View reviewed changes

bohendo approved these changes Mar 23, 2023

View reviewed changes

0xPhaze added 3 commits March 23, 2023 16:35

Merge branch 'master' into HEAD

cfc7e10

Format document

5157dd6

Fix suggestions

86d1e7d

montyly reviewed Mar 25, 2023

View reviewed changes

montyly reviewed Apr 10, 2023

View reviewed changes

0xPhaze added 5 commits April 10, 2023 13:20

Include suggestions

83091b8

Merge branch 'master' into guide-to-arithmetic-checks

6a21bc5

Small fixes

838d9f4

Merge branch 'master' into guide-to-arithmetic-checks

39228fc

Fix review

7c80af0

montyly reviewed Apr 14, 2023

View reviewed changes

0xPhaze added 2 commits April 14, 2023 14:26

Fix review

2a22697

Fix review

9993c5e

montyly merged commit 3ee27c7 into crytic:master Apr 17, 2023

		@@ -0,0 +1,668 @@
		# A Guide on Performing Arithmetic Checks in the EVM

		The EVM is a peculiar machine that many of us have come to love and hate for all its quirks.


		## Arithmetic checks for int256 multiplication

		In older versions, the Solidity compiler uses four separate checks to detect integer multiplication overflow.

		@@ -0,0 +1,717 @@
		# A Guide on Performing Arithmetic Checks in the EVM

		The Ethereum Virtual Machine (EVM) distinguishes itself from traditional computer systems and virtual machines through several unique aspects.


		In conclusion, we hope this article has served as an informative guide on signed integer arithmetic within the EVM and the two's complement system. We have seen the added complexity that is introduced when performing checked arithmetic on signed integers compared to unsigned ones and when dealing with sub-32 byte types.

		As the trend in Solidity smart contract development leans towards low-level optimizations, it is important to emphasize the diligence required when implementing these techniques. The aim of this article is to deepen one's understanding of low-level arithmetic, thereby improving the security of Solidity code by enabling developers to better assess and comprehend the assumptions present in these operations. However, it is crucial to remember that custom low-level optimizations should be integrated only after rigorous manual analysis, fuzzing, and symbolic verification. Additionally, any non-obvious assumptions should always be clearly documented.


		## Conclusion

		In conclusion, we hope this article has served as an informative guide on signed integer arithmetic within the EVM and the two's complement system. We have seen the added complexity that is introduced when performing checked arithmetic on signed integers compared to unsigned ones and when dealing with sub-32 byte types.

Include section on arithmetic checks #237

Include section on arithmetic checks #237

Uh oh!

Conversation

0xPhaze commented Mar 7, 2023

Uh oh!

CLAassistant commented Mar 7, 2023 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

montyly commented Mar 22, 2023

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

bohendo left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

0xPhaze commented Mar 23, 2023

Uh oh!

montyly left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

0xPhaze Mar 26, 2023 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

montyly left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

MindlessSteel commented May 12, 2023

CLAassistant commented Mar 7, 2023 •

edited

Loading

0xPhaze Mar 26, 2023 •

edited

Loading