From fb412787ef8b1b9b0528b12b4af1ed6d8875c19c Mon Sep 17 00:00:00 2001
From: 0xphaze <0xphaze@gmail.com>
Date: Tue, 7 Mar 2023 13:36:47 +0100
Subject: [PATCH 01/11] Include section on arithmetic checks

---
 README.md                      |   1 +
 SUMMARY.md                     |   1 +
 book                           |   1 +
 learn_evm/README.md            |   1 +
 learn_evm/arithmetic-checks.md | 667 +++++++++++++++++++++++++++++++++
 5 files changed, 671 insertions(+)
 create mode 160000 book
 create mode 100644 learn_evm/arithmetic-checks.md

diff --git a/README.md b/README.md
index 3c5e8c29..9cd31304 100644
--- a/README.md
+++ b/README.md
@@ -17,6 +17,7 @@ We welcome contributions, and you can contribute by following our [contributing
   - [EVM Opcodes](./learn_evm/evm_opcodes.md): Details on all EVM opcodes
   - [Transaction Tracing](./learn_evm/tracing.md): Helper scripts and guidance for generating and navigating transaction traces
   - [Yellow Paper Guidance](./learn_evm/yellow-paper.md): Symbol reference for more easily reading the Ethereum yellow paper
+  - [Arithmetic Checks](./learn_evm/arithmetic-checks.md): A guide to performing arithmetic checks in the EVM
   - [Forks <> EIPs](./learn_evm/eips_forks.md): Summarize the EIPs included in each Ethereum fork
     - [Forks <> CIPs](./learn_evm/cips_forks.md): Summarize the CIPs and EIPs included in each Celo fork *(EVM-compatible chain)*
     - [Upgrades <> TIPs](./learn_evm/tips_upgrades.md): Summarize the TIPs included in each TRON upgrade *(EVM-compatible chain)*
diff --git a/SUMMARY.md b/SUMMARY.md
index 325304e5..86dc9c79 100644
--- a/SUMMARY.md
+++ b/SUMMARY.md
@@ -11,6 +11,7 @@
 - [Learn EVM](./learn_evm/README.md)
     - [EVM Opcode Reference](./learn_evm/evm_opcodes.md)
     - [Transaction Tracing](./learn_evm/tracing.md)
+    - [Arithmetic Checks](./learn_evm/arithmetic-checks.md)
     - [Yellow Paper Guidance](./learn_evm/yellow-paper.md):
         - [Forks <> EIPs](./learn_evm/eips_forks.md)
         - [Forks <> CIPs](./learn_evm/cips_forks.md)
diff --git a/book b/book
new file mode 160000
index 00000000..c7f4f09d
--- /dev/null
+++ b/book
@@ -0,0 +1 @@
+Subproject commit c7f4f09d0d089d13c26d8d17dcb17456f280b27b
diff --git a/learn_evm/README.md b/learn_evm/README.md
index 5f744984..0a66c470 100644
--- a/learn_evm/README.md
+++ b/learn_evm/README.md
@@ -5,6 +5,7 @@ List of EVM technical knowledge
 - [EVM Opcode Reference](evm_opcodes.md): Reference and notes for each of the EVM opcodes
 - [Transaction Tracing](tracing.md): Helper scripts and guidance for generating and navigating transaction traces
 - [Yellow Paper Guidance](yellow-paper.md): Symbol reference for more easily reading the Ethereum yellow paper
+- [Arithmetic Checks](./arithmetic-checks.md): A guide to performing arithmetic checks in the EVM
 - [Forks <> EIPs](eips_forks.md): Summarize the EIPs included in each fork
   - [Forks <> CIPs](cips_forks.md): Summarize the CIPs and EIPs included in each Celo fork *(EVM-compatible chain)*
   - [Upgrades <> TIPs](tips_upgrades.md): Summarize the TIPs included in each TRON upgrade *(EVM-compatible chain)*
diff --git a/learn_evm/arithmetic-checks.md b/learn_evm/arithmetic-checks.md
new file mode 100644
index 00000000..3df024b1
--- /dev/null
+++ b/learn_evm/arithmetic-checks.md
@@ -0,0 +1,667 @@
+# 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.
+One such quirk is the absence of native arithmetic checks, which are typically present in most architectures and virtual machines through the use of carry bits or an overflow flag.
+The EVM treats all stack values as uint256 types.
+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`.
+> These would provide built-in overflow flags. However, the EIP's current status is stagnant.
+
+Since Solidity version 0.8.0 the compiler includes over and underflow protection in all arithmetic operations by default. 
+Before version 0.8.0, these checks had to be implemented manually - a commonly used library is called [SafeMath](https://github.com/OpenZeppelin/openzeppelin-contracts/blob/master/contracts/utils/math/SafeMath.sol), originally developed by OpenZeppelin.
+Much like how SafeMath works, arithmetic checks are inserted by the compiler through additional operations.
+
+> **Disclaimer:** Please note that this post is for educational purposes. 
+> It is not our intention to encourage micro optimizations in order to save gas,
+> as this can potentially lead to the introduction of new bugs that are difficult to detect and may compromise the security and stability of the protocol.
+> As a protocol developer, it is important to prioritize the safety and security of the protocol over [premature optimization](https://www.youtube.com/watch?v=tKbV6BpH-C8).
+> In situations where the code for the protocol is still evolving, including redundant checks for critical operations may be a good practice.
+> However, we do encourage experimentation with these operations for educational purposes.
+
+## Arithmetic checks for uint256 addition
+
+To investigate how the solc compiler implements arithmetic checks, we can compile the code with the `--asm` flag and inspect the resulting bytecode. 
+Alternatively, by using the `--ir` flag, we can examine the Yul code that is generated as an intermediate representation (IR).
+> It's worth noting that Solidity aims to make the new Yul pipeline the standard. 
+> Certain operations (including arithmetic checks) are always included as Yul code, regardless of whether the code is compiled with the new pipeline using `--via-ir`. 
+> This provides an opportunity to examine the Yul code and gain a better understanding of how arithmetic checks are executed in Solidity. 
+> However, it's important to keep in mind that the final bytecode may differ slightly when compiler optimizations are turned on.
+
+To illustrate how the compiler detects overflow in unsigned integer addition, consider the following example of Yul code that is produced by the compiler.
+
+```solidity
+function checked_add_t_uint256(x, y) -> sum {
+    x := cleanup_t_uint256(x)
+    y := cleanup_t_uint256(y)
+
+    // overflow, if x > (maxValue - y)
+    if gt(x, sub(0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff, y)) { panic_error_0x11() }
+
+    sum := add(x, y)
+}
+```
+
+To enhance readability, we can interpret the Yul code back into high-level Solidity code.
+
+```solidity
+/// @notice versions >=0.8.0 && <0.8.16
+function checkedAddUint1(uint256 a, uint256 b) public pure returns (uint256 c) {
+    unchecked {
+        c = a + b;
+
+        if (a > type(uint256).max - b) arithmeticError();
+    }
+}
+```
+
+> Solidity's arithmetic errors are encoded as `abi.encodeWithSignature("Panic(uint256)", 0x11)`.
+
+The check for overflow in unsigned integer addition involves calculating the largest value that one summand can be added to the other without resulting in an overflow. 
+Specifically, in this case, the maximum value that `a` can have is `type(uint256).max - b`. 
+If `a` exceeds this value, we can conclude that `a + b` will overflow. 
+
+An alternative (and slightly more efficient) approach to computing the maximum value of `a` is to invert the bits on `b`.
+
+```solidity
+function checkedAddUint2(uint256 a, uint256 b) public pure returns (uint256 c) {
+    unchecked {
+        c = a + b;
+
+        if (a > ~b) arithmeticError();
+    }
+}
+```
+
+> This code is produced by the compiler with optimizations turned on for versions <0.8.16.
+
+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`.
+> 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.
+
+```solidity
+/// @notice versions >=0.8.16
+function checkedAddUint(uint256 a, uint256 b) public pure returns (uint256 c) {
+    unchecked {
+        c = a + b;
+
+        if (a > c) arithmeticError();
+    }
+}
+```
+
+Overflow is detected when the sum is smaller than one of its summands. 
+In other words, if `a > a + b`, then overflow has occurred. 
+A full proof of this requires verifying that overflow occurs if and only if `a > a + b`. 
+An important observation is that `a > a + b` (mod `2**256`) for `b > 0` is only possible when `b >= 2**256`, which exceeds the maximum possible value.
+
+## Arithmetic checks for int256 addition
+
+The Solidity compiler generates the following (equivalent) code for detecting overflow in signed integer addition:
+
+```solidity
+/// @notice versions >=0.8.0 && <0.8.16
+function checkedAddInt(int256 a, int256 b) public pure returns (int256 c) {
+    unchecked {
+        c = a + b;
+
+        // If `a > 0`, then `b` can't exceed `type(int256).max - a`.
+        if (a > 0 && b > type(int256).max - a) arithmeticError();
+        // If `a < 0`, then `b` can't be less than `type(int256).min - a`.
+        if (a < 0 && b < type(int256).min - a) arithmeticError();
+    }
+}
+```
+
+Like before, we can compute the maximum and minimum value of a summand given that the other summand is either positive or negative.
+
+For reference, this is the Yul code that is produced when compiling via IR.
+
+```solidity
+function checked_add_t_int256(x, y) -> sum {
+    x := cleanup_t_int256(x)
+    y := cleanup_t_int256(y)
+
+    // overflow, if x >= 0 and y > (maxValue - x)
+    if and(iszero(slt(x, 0)), sgt(y, sub(0x7fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff, x))) { panic_error_0x11() }
+    // underflow, if x < 0 and y < (minValue - x)
+    if and(slt(x, 0), slt(y, sub(0x8000000000000000000000000000000000000000000000000000000000000000, x))) { panic_error_0x11() }
+
+    sum := add(x, y)
+}
+```
+
+It's important to note that when comparing signed values, we must use the opcodes `slt` (signed less than) and `sgt` (signed greater than) to avoid interpreting signed integers as unsigned integers. 
+Solidity will automatically insert the correct opcode based on the type of the value. This applies to other signed operations as well.
+
+### Quick primer on a two's complement system
+
+In a two's complement system, the range of possible integers is divided into two halves: the positive and negative domain. 
+The first bit of an integer represents the sign, with `0` indicating a positive number and `1` indicating a negative number. 
+For positive integers (those with a sign bit of `0`), their binary representation is the same as their unsigned bit representation. 
+However, the negative domain is shifted to lie "above" the positive domain.
+
+```
+| -------------------------------- uint256 -------------------------------- |
+0 --------------------------------------------------------------------- uint256_max
+
+| --------- positive int256 --------- | --------- negative int256 --------- |
+0 ------------------------ int256_max | int256_min ------------------------ -1
+```
+
+```solidity
+0x0000000000000000000000000000000000000000000000000000000000000000 // 0
+0x7fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff // int256_max
+0x8000000000000000000000000000000000000000000000000000000000000000 // int256_min
+0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff // -1
+```
+
+The maximum positive integer that can be represented in a two's complement system using int256 is 
+`0x7fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff` which is equal to half of the maximum value that can be represented using uint256. 
+The most significant bit of this number is `0`, while all other bits are `1`.
+
+On the other hand, all negative numbers start with a `1` as their first bit. 
+If we look at the underlying hex representation of these numbers, they are all greater than or equal to the smallest integer that can be represented using int256, which is `0x8000000000000000000000000000000000000000000000000000000000000000` (equal to `1` shifted 255 bits to the left).
+
+To obtain the negative value of an integer in a two's complement system, we can flip all the underlying bits and add `1`: `-a = ~a + 1`.
+An example illustrates this.
+
+```solidity 
+0x0000000000000000000000000000000000000000000000000000000000000003 // 3
+0xfffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffc // ~3
+0xfffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffd // -3 = ~3 + 1
+```
+
+To verify that `-a + a = 0` holds for all integers, we can use the property of two's complement arithmetic that `-a = ~a + 1`. 
+By substituting this into the equation, we get `-a + a = (~a + 1) + a = MAX + 1 = 0`, where `MAX` is the maximum integer value.
+
+There is a unique case that needs special attention in two's complement arithmetic.
+The smallest possible integer `int256).min = 0x8000000000000000000000000000000000000000000000000000000000000000 = -57896044618658097711785492504343953926634992332820282019728792003956564819968`
+does not have a positive inverse for addition, making it the only negative number with this property.
+
+Interestingly, if we try to compute `-type(int256).min`, we get the same number, as `-type(int256).min = ~type(int256).min + 1 = type(int256).min`. 
+This means there are two fixed points for additive inverses: `-0 = 0` and `-type(int256).min = type(int256).min`. 
+It's important to note that Solidity's arithmetic checks will throw an error when evaluating `-type(int256).min` (outside of unchecked blocks).
+
+Finally, looking at the underlying bit (or hex) representation highlights the importance of using the correct operators for signed integers, such as `slt` instead of `lt`, to avoid misinterpreting negative values as large numbers.
+
+```solidity
+  0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff // int256(-1) or type(uint256).max
+< 0x0000000000000000000000000000000000000000000000000000000000000000 // 0
+// When using `slt`, the comparison is interpreted as `-1 < 0 = true`.
+= 0x0000000000000000000000000000000000000000000000000000000000000001
+// When using `lt`, the comparison is interpreted as `type(uint256).max < 0 = false`.
+= 0x0000000000000000000000000000000000000000000000000000000000000000
+```
+
+Newer versions of Solidity prevent integer overflow by using the computed result `c = a + b` to check for overflow/underflow. 
+However, unlike unsigned addition, signed addition requires two separate checks instead of one. 
+
+```solidity
+/// @notice versions >=0.8.16
+function checkedAddInt2(int256 a, int256 b) public pure returns (int256 c) {
+    unchecked {
+        c = a + b;
+
+        // If `a` is positive, then the sum `c = a + b` can't be less than `b`.
+        if (a > 0 && c < b) arithmeticError();
+        // If `a` is negative, then the sum `c = a + b` can't be greater than `b`.
+        if (a < 0 && c > b) arithmeticError();
+    }
+}
+```
+
+Nevertheless, by utilizing `xor`, which is the bitwise exclusive-or operation, we can combine these checks into one.
+
+```solidity
+function checkedAddInt3(int256 a, int256 b) public pure returns (int256 c) {
+    unchecked {
+        c = a + b;
+
+        bool overflow;
+
+        assembly {
+            // If `a >= 0`, then the sum `c = a + b` can't be less than `b`.
+            // If `a <  0`, then the sum `c = a + b` can't be greater than `b`.
+            // We combine these two conditions into one using `xor`.
+            overflow := xor(slt(a, 0), sgt(b, c))
+        }
+
+        if (overflow) arithmeticError();
+    }
+}
+```
+
+The code is written in assembly, because Solidity lacks an `xor` operation for boolean values.
+
+A different approach to detecting overflow in addition is to observe that adding two integers with different signs will never overflow.
+This reduces the check to the case when both summands have the same sign.
+If the sign of the sum is different from one of the summands, the result has overflowed.
+
+```solidity
+function checkedAddInt4(int256 a, int256 b) public pure returns (int256 c) {
+    unchecked {
+        c = a + b;
+
+        // Overflow, if the signs of `a` and `b` are the same,
+        // but the sign of the result `c = a + b` differs from its summands.
+        // When the signs of `a` and `b` differ overflow is not possible.
+        if ((~a ^ b) & (a ^ c) < 0) arithmeticError();
+    }
+}
+```
+
+Rather than checking the sign bit explicitly, which can be achieved by shifting the value to the right by 255 bits and checking that it is non-zero,
+we can use the `slt` operation to compare the value with `0`.
+
+## Arithmetic checks for uint256 subtraction
+
+
+The process of checking for underflow in subtraction is akin to that of addition. 
+If we subtract `a - b`, and `b` is greater than `a`, we have an underflow situation. 
+
+
+```solidity
+function checkedSubUint(uint256 a, uint256 b) public pure returns (uint256 c) {
+    unchecked {
+        c = a - b;
+
+        if (b > a) arithmeticError();
+    }
+}
+```
+
+We could, like before, perform the check on the result itself using `if (c > a) arithmeticError();`, because subtracting a positive value from `a` should yield a value less than or equal to `a`. 
+However, in this case, we don't save any operations. 
+Just as with addition, for signed integers, we can combine the checks for both scenarios into a single check using `xor`.
+
+```solidity
+function checkedSubInt(int256 a, int256 b) public pure returns (int256 c) {
+    unchecked {
+        c = a - b;
+
+        bool overflow;
+
+        assembly {
+            // If `b >= 0`, then the result `c = a - b` can't be greater than `a`.
+            // If `b <  0`, then the result `c = a - b` can't be less than `a`.
+            overflow := xor(sgt(b, 0), sgt(a, c))
+        }
+
+        if (overflow) arithmeticError();
+    }
+}
+```
+
+## Arithmetic checks for uint256 multiplication
+
+To detect overflow when multiplying two unsigned integers, we can again use the approach of computing the maximum possible value of a multiplicand and check that it isn't exceeded. 
+
+```solidity
+/// @notice versions >=0.8.0 && <0.8.17
+function checkedMulUint1(uint256 a, uint256 b) public pure returns (uint256 c) {
+    unchecked {
+        c = a * b;
+
+        if (a != 0 && b > type(uint256).max / a) arithmeticError();
+    }
+}
+```
+
+> 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. 
+> The EVM itself simply returns `0` when dividing by `0`, and this also applies to inline-assembly. 
+> If the order of the boolean expressions is evaluated in reverse order, it could cause an arithmetic check to incorrectly revert when a=0.
+
+We can compute the maximum value for `b` as long as `a` is non-zero. However, if `a` is zero, we know that the result will be zero as well, and there is no need to check for overflow. 
+Like before, we can also make use of the result and try to reconstruct one multiplicand from it. This is possible if the product didn't overflow and the first multiplicand is non-zero.
+
+```solidity
+/// @notice versions >=0.8.17
+function checkedMulUint2(uint256 a, uint256 b) public pure returns (uint256 c) {
+    unchecked {
+        c = a * b;
+
+        if (a != 0 && b != c / a) arithmeticError();
+    }
+}
+```
+
+For reference, we can further remove the addition division by zero check by writing the code in assembly.
+
+```solidity
+function checkedMulUint3(uint256 a, uint256 b) public pure returns (uint256 c) {
+    unchecked {
+        c = a * b;
+
+        bool overflow;
+
+        assembly {
+            // This version does not include a redundant division-by-0 check
+            // which the Solidity compiler includes when performing `c / a`.
+            overflow := iszero(or(iszero(a), eq(div(c, a), b)))
+        }
+
+        if (overflow) arithmeticError();
+    }
+}
+```
+
+## Arithmetic checks for int256 multiplication
+
+In older versions, the Solidity compiler uses four separate checks to detect integer multiplication overflow.
+The produced Yul code is equivalent to the following high-level Solidity code.
+
+```solidity
+/// @notice versions >=0.8.0 && <0.8.17
+function checkedMulInt(int256 a, int256 b) public pure returns (int256 c) {
+    unchecked {
+        c = a * b;
+
+        if (a > 0 && b > 0 && a > type(int256).max / b) arithmeticError();
+        if (a > 0 && b < 0 && a < type(int256).min / b) arithmeticError();
+        if (a < 0 && b > 0 && a < type(int256).min / b) arithmeticError();
+        if (a < 0 && b < 0 && a < type(int256).max / b) arithmeticError();
+    }
+}
+```
+
+Newer Solidity versions optimize the process by using the computed product.
+
+```solidity
+/// @notice versions >=0.8.17
+function checkedMulInt2(int256 a, int256 b) public pure returns (int256 c) {
+    unchecked {
+        c = a * b;
+
+        if (a < 0 && b == type(int256).min) arithmeticError();
+        if (a != 0 && b != c / a) arithmeticError();
+    }
+}
+```
+
+When it comes to integer multiplication, it's important to check for `a < 0` and `b == type(int256).min`.
+The actual case is limited to `a == -1` and `b == type(int256).min`, where the product `c` will overflow.
+This is because `-b` cannot be represented as a positive signed integer, as previously mentioned.
+
+## Arithmetic checks for addition with sub-32-byte types
+
+When performing arithmetic checks on data types that use less than 32 bytes, there are some additional steps to consider. 
+First, let's take a look at the addition of signed 64-bit integers.
+
+On a 64-bit system, integer addition works in the same way as before. 
+
+```solidity
+  0xfffffffffffffffe // int64(-2)
++ 0x0000000000000003 // int64(3)
+= 0x0000000000000001 // int64(1)
+```
+
+However, when performing the same calculations on a 256-bit machine, we need to extend the sign of the int64 value over all unused bits.
+
+```solidity
+                                   extended sign ──┐┌── 64-bit information
+  0xfffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffe // int64(-2)
++ 0x0000000000000000000000000000000000000000000000000000000000000003 // int64(3)
+= 0x0000000000000000000000000000000000000000000000000000000000000001 // int64(1)
+```
+
+It's worth noting that not all operations require clean upper bits. 
+In fact, even if the upper bits are dirty, we can still get correct results for addition. 
+However, the sum will usually contain dirty upper bits that will need to be cleaned. 
+For example, when performing addition without knowing what the upper bits are set to, we get the following result.
+
+```solidity
+  0x????????????????????????????????????????????????fffffffffffffffe // int64(-2)
++ 0x????????????????????????????????????????????????0000000000000003 // int64(3)
+= 0x????????????????????????????????????????????????0000000000000001 // int64(1)
+```
+
+It is crucial to be mindful of when to clean the bits before and after operations. 
+By default, Solidity takes care of cleaning the bits before operations on smaller types and lets the optimizer remove any redundant steps. 
+However, values accessed after operations included by the compiler are not guaranteed to be clean. In particular, this is the case for addition with small data types. 
+The bit cleaning steps will be removed by the compiler, even without optimizations, if a variable is only accessed in a subsequent assembly block. 
+Refer to the [Solidity documentation](https://docs.soliditylang.org/en/v0.8.18/internals/variable_cleanup.html#cleaning-up-variables) for further information on this matter.
+
+When performing arithmetic checks in the same way as before, it is necessary to include a step to clean the bits on the sum. 
+One approach to achieve this is by performing `signextend(7, value)`, which extends the sign of a 64-bit (7 + 1 = 8 bytes) integer over all upper bits.
+
+```solidity
+function checkedAddInt64_1(int64 a, int64 b) public pure returns (int64 c) {
+    unchecked {
+        bool overflow;
+
+        c = a + b;
+
+        assembly {
+            // Note that we must manually clean the upper bits in this case.
+            // Solidity will optimize the cleaning away otherwise.
+            // Extend the sign of the sum to 256 bits.
+            c := signextend(7, c)
+
+            // Perform the same arithmetic overflow check as before.
+            overflow := xor(slt(a, 0), sgt(b, c))
+        }
+
+        if (overflow) arithmeticError();
+    }
+}
+```
+
+If we remove the line that includes `c := signextend(7, c)` the overflow check will not function correctly.
+This is because Solidity does not take into account the fact that the variable is used in an assembly block, so the compiler removes the bit cleaning operation, even if the Yul code includes it after the addition.
+
+One thing to keep in mind is that since we are performing a 64-bit addition in 256 bits, we practically have access to the carry/overflow bits.
+If our computed value does not overflow, then it will fall within the correct bounds `type(int64).min <= c <= type(int64).max`.
+The actual overflow check in Solidity involves verifying both the upper and lower bounds.
+
+```solidity
+/// @notice version >= 0.8.16
+function checkedAddInt64_2(int64 a, int64 b) public pure returns (int64 c) {
+    unchecked {
+        // Perform the addition in int256.
+        int256 uc = int256(a) + b;
+
+        // If the value can not be represented by a int64, there is overflow.
+        if (uc > type(int64).max || uc < type(int64).min) arithmeticError();
+
+        // We can safely cast the result.
+        c = int64(uc);
+    }
+}
+```
+
+There are a few ways to verify that the result in its 256-bit representation will fit into the expected data type. 
+This is only true when all upper bits are the same. 
+The most direct method, as with integer overflow, involves checking the lower and upper bounds of the value.
+
+```solidity
+/// @notice Check used in int64 addition for version >= 0.8.16.
+function overflowInt64(int256 value) public pure returns (bool overflow) {
+    overflow = value > type(int64).max || value < type(int64).min;
+}
+```
+
+We can simplify the comparison process to a single operator 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).
+
+```
+| -------------------------------- uint256 -------------------------------- |
+0 --------------------------------------------------------------------- uint256_max
+
+| --------- positive int256 --------- | --------- negative int256 --------- |
+0 ------------------------ int256_max | int256_min ------------------------ -1
+```
+
+The domain for uint128/int128 can be visualized as follows.
+
+```
+| ------------ uint128 -------------- |                                     |
+0 ----------------------- uint128_max |                                     |
+
+| -- pos int128 -- |                                     | -- neg int128 -- |
+0 ----- int128_max |                                     | int128_min ----- -1
+```
+
+After subtracting `type(int128).min` we get the following, connected set of values.
+
+```
+| ------------ uint128 -------------- |                                     |
+0 ----------------------- uint128_max |                                     |
+
+| -- neg int128 -- | -- pos int128 -- |                                     |
+int128_min ----- -1| 0 --- int128_max |                                     |
+```
+
+If we interpret the shifted value as an unsigned integer, we only need to check whether it exceeds the maximum unsigned integer `type(uint128).max`.
+The corresponding check in Solidity is shown below.
+
+```solidity
+function overflowInt64_2(int256 value) public pure returns (bool overflow) {
+    unchecked {
+        overflow = uint256(value) - uint256(int256(type(int64).min)) > type(uint64).max;
+    }
+}
+```
+
+In this case the verbose assembly code might actually be easier to follow than the Solidity code which can sometimes contain implicit operations.
+
+```solidity
+int64 constant INT64_MIN = -0x8000000000000000;
+uint64 constant UINT64_MAX = 0xffffffffffffffff;
+
+function overflowInt64_2_yul(int256 value) public pure returns (bool overflow) {
+    assembly {
+        overflow := gt(sub(value, INT64_MIN), UINT64_MAX)
+    }
+}
+```
+
+As mentioned earlier, this approach is only effective for negative numbers when all of their upper bits are set to `1`, allowing us to overflow back into the positive domain. 
+An alternative and more straightforward method would be to verify that all of the upper bits are equivalent to the sign bit.
+
+```solidity
+function overflowInt64_3(int256 value) public pure returns (bool overflow) {
+    overflow = value != int64(value);
+}
+```
+
+In Yul, the equivalent code would resemble the following.
+
+```solidity
+function overflowInt64_3_yul(int256 value) public pure returns (bool overflow) {
+    assembly {
+        overflow := iszero(eq(value, signextend(7, value)))
+    }
+}
+```
+
+Another way of extending the sign is to make use of `sar` (signed arithmetic right shift).
+
+```solidity
+function overflowInt64_4(int256 value) public pure returns (bool overflow) {
+    overflow = value != (value << 192) >> 192;
+}
+
+function overflowInt64_4_yul(int256 value) public pure returns (bool overflow) {
+    assembly {
+        overflow := iszero(eq(value, sar(192, shl(192, value))))
+    }
+}
+```
+
+Finally, a full example for detecting signed 64-bit integer overflow, implemented in Solidity can be seen below.
+
+```solidity
+function checkedAddInt64_2(int64 a, int64 b) public pure returns (int64 c) {
+    unchecked {
+        // Cast the first summand.
+        // The second summand is implicitly casted.
+        int256 uc = int256(a) + b;
+
+        // Check whether the result `uc` can be represented by 64 bits
+        // by shifting the values to the uint64 domain.
+        // This is done by subtracting the smallest value in int64.
+        if (uint256(uc) - uint256(int256(type(int64).min)) > type(uint64).max) arithmeticError();
+
+        // We can safely cast the result.
+        c = int64(uc);
+    }
+}
+```
+
+## Arithmetic checks for multiplication with sub-32-byte types
+
+If the product `c = a * b` can be calculated in 256 bits without the possibility of overflowing, we can once again verify whether the result can fit into the anticipated data type. 
+This is also the way Solidity handles the check in newer versions.
+
+```solidity
+/// @notice version >= 0.8.17
+function checkedMulInt64(int64 a, int64 b) public pure returns (int64 c) {
+    unchecked {
+        int256 uc = int256(a) * int256(b);
+
+        // If the product can not be represented with 64 bits,
+        // there is overflow.
+        if (overflowInt64(uc)) arithmeticError();
+
+        c = int64(uc);
+    }
+}
+```
+
+However, if the maximum value of a product exceeds 256 bits, then this method won't be effective. 
+This happens, for instance, when working with int192. The product `type(int192).min * type(int192).min` requires 192 + 192 = 384 bits to be stored, which exceeds the maximum of 256 bits. 
+Overflow occurs in 256 bits, resulting in a `0`, and it won't be logical to check if the result fits into 192 bits.
+In this scenario, we can depend on the previous checks and, for example, attempt to reconstruct one of the multiplicands.
+
+```solidity
+function checkedMulInt192_1(int192 a, int192 b) public pure returns (int192 c) {
+    unchecked {
+        c = a * b;
+
+        if (a != 0 && b != c / a) arithmeticError();
+        if (a = -1 && b == type(int192).min) arithmeticError();
+    }
+}
+```
+
+Once more, we must consider the two special circumstances:
+1. When one of the multiplicands is zero (`a == 0`), the other multiplicand cannot be retrieved. However, this case never results in overflow.
+2. Even if the multiplication is correct in 256 bits, the calculation overflows when only examining the least-significant 192 bits if the first multiplicand is minus one (`a = -1`) and the other multiplicand is the minimum value.
+
+The second exceptional scenario is still relevant since it is possible to encounter overflow when only considering the least-significant 192 bits, despite the multiplication being correct in 256 bits.
+
+```solidity
+  0xffffffffffffffff800000000000000000000000000000000000000000000000 // type(int192).min
+* 0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff // -1
+= 0x0000000000000000800000000000000000000000000000000000000000000000 // type(int192).min (when seen as a int192)
+```
+
+To handle this particular case, we can always start by sign-extending or cleaning the result before attempting to reconstruct the other multiplicand.
+This removes one of the checks.
+
+```solidity
+/// @notice version >= 0.8.17
+function checkedMulInt192_2(int192 a, int192 b) public pure returns (int192 c) {
+    unchecked {
+        bool overflow;
+
+        assembly {
+            // Extend the sign for int192 (24 = 23 + 1 bytes).
+            c := signextend(23, mul(a, b))
+
+            // Overflow, if `a != 0 && b != c / a`.
+            overflow := iszero(or(iszero(a), eq(b, sdiv(c, a))))
+        }
+
+        if (overflow) arithmeticError();
+    }
+}
+```
\ No newline at end of file

From 330132471cb7390d561df965a4a9934e24ad9655 Mon Sep 17 00:00:00 2001
From: 0xphaze <0xphaze@gmail.com>
Date: Tue, 7 Mar 2023 13:41:21 +0100
Subject: [PATCH 02/11] fix: consistent order in ToC

---
 README.md           | 2 +-
 learn_evm/README.md | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/README.md b/README.md
index 9cd31304..2316bad0 100644
--- a/README.md
+++ b/README.md
@@ -16,8 +16,8 @@ We welcome contributions, and you can contribute by following our [contributing
 - [Learn EVM](./learn_evm): EVM technical knowledge
   - [EVM Opcodes](./learn_evm/evm_opcodes.md): Details on all EVM opcodes
   - [Transaction Tracing](./learn_evm/tracing.md): Helper scripts and guidance for generating and navigating transaction traces
-  - [Yellow Paper Guidance](./learn_evm/yellow-paper.md): Symbol reference for more easily reading the Ethereum yellow paper
   - [Arithmetic Checks](./learn_evm/arithmetic-checks.md): A guide to performing arithmetic checks in the EVM
+  - [Yellow Paper Guidance](./learn_evm/yellow-paper.md): Symbol reference for more easily reading the Ethereum yellow paper
   - [Forks <> EIPs](./learn_evm/eips_forks.md): Summarize the EIPs included in each Ethereum fork
     - [Forks <> CIPs](./learn_evm/cips_forks.md): Summarize the CIPs and EIPs included in each Celo fork *(EVM-compatible chain)*
     - [Upgrades <> TIPs](./learn_evm/tips_upgrades.md): Summarize the TIPs included in each TRON upgrade *(EVM-compatible chain)*
diff --git a/learn_evm/README.md b/learn_evm/README.md
index 0a66c470..f3f786e6 100644
--- a/learn_evm/README.md
+++ b/learn_evm/README.md
@@ -4,8 +4,8 @@ List of EVM technical knowledge
 
 - [EVM Opcode Reference](evm_opcodes.md): Reference and notes for each of the EVM opcodes
 - [Transaction Tracing](tracing.md): Helper scripts and guidance for generating and navigating transaction traces
-- [Yellow Paper Guidance](yellow-paper.md): Symbol reference for more easily reading the Ethereum yellow paper
 - [Arithmetic Checks](./arithmetic-checks.md): A guide to performing arithmetic checks in the EVM
+- [Yellow Paper Guidance](yellow-paper.md): Symbol reference for more easily reading the Ethereum yellow paper
 - [Forks <> EIPs](eips_forks.md): Summarize the EIPs included in each fork
   - [Forks <> CIPs](cips_forks.md): Summarize the CIPs and EIPs included in each Celo fork *(EVM-compatible chain)*
   - [Upgrades <> TIPs](tips_upgrades.md): Summarize the TIPs included in each TRON upgrade *(EVM-compatible chain)*

From 3a8f8ab22cda6e0c6be58b8ea32b1b075e72a370 Mon Sep 17 00:00:00 2001
From: 0xphaze <0xphaze@gmail.com>
Date: Tue, 7 Mar 2023 14:11:52 +0100
Subject: [PATCH 03/11] fix: include small changes

---
 learn_evm/arithmetic-checks.md | 48 +++++++++++++++++-----------------
 1 file changed, 24 insertions(+), 24 deletions(-)

diff --git a/learn_evm/arithmetic-checks.md b/learn_evm/arithmetic-checks.md
index 3df024b1..70ae43bf 100644
--- a/learn_evm/arithmetic-checks.md
+++ b/learn_evm/arithmetic-checks.md
@@ -65,6 +65,7 @@ If `a` exceeds this value, we can conclude that `a + b` will overflow.
 An alternative (and slightly more efficient) approach to computing the maximum value of `a` is to invert the bits on `b`.
 
 ```solidity
+/// @notice versions >=0.8.0 && <0.8.16 with compiler optimizations
 function checkedAddUint2(uint256 a, uint256 b) public pure returns (uint256 c) {
     unchecked {
         c = a + b;
@@ -74,8 +75,6 @@ function checkedAddUint2(uint256 a, uint256 b) public pure returns (uint256 c) {
 }
 ```
 
-> This code is produced by the compiler with optimizations turned on for versions <0.8.16.
-
 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`.
@@ -218,6 +217,7 @@ function checkedAddInt2(int256 a, int256 b) public pure returns (int256 c) {
 ```
 
 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.
 
 ```solidity
 function checkedAddInt3(int256 a, int256 b) public pure returns (int256 c) {
@@ -238,8 +238,6 @@ function checkedAddInt3(int256 a, int256 b) public pure returns (int256 c) {
 }
 ```
 
-The code is written in assembly, because Solidity lacks an `xor` operation for boolean values.
-
 A different approach to detecting overflow in addition is to observe that adding two integers with different signs will never overflow.
 This reduces the check to the case when both summands have the same sign.
 If the sign of the sum is different from one of the summands, the result has overflowed.
@@ -279,6 +277,7 @@ function checkedSubUint(uint256 a, uint256 b) public pure returns (uint256 c) {
 
 We could, like before, perform the check on the result itself using `if (c > a) arithmeticError();`, because subtracting a positive value from `a` should yield a value less than or equal to `a`. 
 However, in this case, we don't save any operations. 
+
 Just as with addition, for signed integers, we can combine the checks for both scenarios into a single check using `xor`.
 
 ```solidity
@@ -316,7 +315,7 @@ function checkedMulUint1(uint256 a, uint256 b) public pure returns (uint256 c) {
 
 > 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. 
 > The EVM itself simply returns `0` when dividing by `0`, and this also applies to inline-assembly. 
-> If the order of the boolean expressions is evaluated in reverse order, it could cause an arithmetic check to incorrectly revert when a=0.
+> If the order of the boolean expressions is evaluated in reverse order, it could cause an arithmetic check to incorrectly revert when `a = 0`.
 
 We can compute the maximum value for `b` as long as `a` is non-zero. However, if `a` is zero, we know that the result will be zero as well, and there is no need to check for overflow. 
 Like before, we can also make use of the result and try to reconstruct one multiplicand from it. This is possible if the product didn't overflow and the first multiplicand is non-zero.
@@ -332,7 +331,7 @@ function checkedMulUint2(uint256 a, uint256 b) public pure returns (uint256 c) {
 }
 ```
 
-For reference, we can further remove the addition division by zero check by writing the code in assembly.
+For reference, we can further remove the additional division by zero check by writing the code in assembly.
 
 ```solidity
 function checkedMulUint3(uint256 a, uint256 b) public pure returns (uint256 c) {
@@ -371,7 +370,7 @@ function checkedMulInt(int256 a, int256 b) public pure returns (int256 c) {
 }
 ```
 
-Newer Solidity versions optimize the process by using the computed product.
+Newer Solidity versions optimize the process by utilizing the computed product in the check.
 
 ```solidity
 /// @notice versions >=0.8.17
@@ -385,8 +384,8 @@ function checkedMulInt2(int256 a, int256 b) public pure returns (int256 c) {
 }
 ```
 
-When it comes to integer multiplication, it's important to check for `a < 0` and `b == type(int256).min`.
-The actual case is limited to `a == -1` and `b == type(int256).min`, where the product `c` will overflow.
+When it comes to integer multiplication, it's important to handle the case hen `a < 0` and `b == type(int256).min`.
+The actual case, where the product `c` will overflow, is limited to `a == -1` and `b == type(int256).min`.
 This is because `-b` cannot be represented as a positive signed integer, as previously mentioned.
 
 ## Arithmetic checks for addition with sub-32-byte types
@@ -402,7 +401,8 @@ On a 64-bit system, integer addition works in the same way as before.
 = 0x0000000000000001 // int64(1)
 ```
 
-However, when performing the same calculations on a 256-bit machine, we need to extend the sign of the int64 value over all unused bits.
+However, when performing the same calculations on a 256-bit machine, we need to extend the sign of the int64 value over all unused bits,
+otherwise the value won't be interpreted correctly.
 
 ```solidity
                                    extended sign ──┐┌── 64-bit information
@@ -422,11 +422,11 @@ For example, when performing addition without knowing what the upper bits are se
 = 0x????????????????????????????????????????????????0000000000000001 // int64(1)
 ```
 
-It is crucial to be mindful of when to clean the bits before and after operations. 
-By default, Solidity takes care of cleaning the bits before operations on smaller types and lets the optimizer remove any redundant steps. 
-However, values accessed after operations included by the compiler are not guaranteed to be clean. In particular, this is the case for addition with small data types. 
-The bit cleaning steps will be removed by the compiler, even without optimizations, if a variable is only accessed in a subsequent assembly block. 
-Refer to the [Solidity documentation](https://docs.soliditylang.org/en/v0.8.18/internals/variable_cleanup.html#cleaning-up-variables) for further information on this matter.
+> It is crucial to be mindful of when to clean the bits before and after operations. 
+> By default, Solidity takes care of cleaning the bits before operations on smaller types and lets the optimizer remove any redundant steps. 
+> However, values accessed after operations included by the compiler are not guaranteed to be clean. In particular, this is the case for addition with small data types. 
+> The bit cleaning steps will be removed by the optimizer (even without optimizations enabled) if a variable is only accessed in a subsequent assembly block. 
+> Refer to the [Solidity documentation](https://docs.soliditylang.org/en/v0.8.18/internals/variable_cleanup.html#cleaning-up-variables) for further information on this matter.
 
 When performing arithmetic checks in the same way as before, it is necessary to include a step to clean the bits on the sum. 
 One approach to achieve this is by performing `signextend(7, value)`, which extends the sign of a 64-bit (7 + 1 = 8 bytes) integer over all upper bits.
@@ -454,7 +454,7 @@ function checkedAddInt64_1(int64 a, int64 b) public pure returns (int64 c) {
 ```
 
 If we remove the line that includes `c := signextend(7, c)` the overflow check will not function correctly.
-This is because Solidity does not take into account the fact that the variable is used in an assembly block, so the compiler removes the bit cleaning operation, even if the Yul code includes it after the addition.
+This is because Solidity does not take into account the fact that the variable is used in an assembly block, so the optimizer removes the bit cleaning operation, even if the Yul code includes it after the addition.
 
 One thing to keep in mind is that since we are performing a 64-bit addition in 256 bits, we practically have access to the carry/overflow bits.
 If our computed value does not overflow, then it will fall within the correct bounds `type(int64).min <= c <= type(int64).max`.
@@ -478,7 +478,7 @@ function checkedAddInt64_2(int64 a, int64 b) public pure returns (int64 c) {
 
 There are a few ways to verify that the result in its 256-bit representation will fit into the expected data type. 
 This is only true when all upper bits are the same. 
-The most direct method, as with integer overflow, involves checking the lower and upper bounds of the value.
+The most direct method, as just shown, involves checking the lower and upper bounds of the value.
 
 ```solidity
 /// @notice Check used in int64 addition for version >= 0.8.16.
@@ -487,7 +487,7 @@ function overflowInt64(int256 value) public pure returns (bool overflow) {
 }
 ```
 
-We can simplify the comparison process to a single operator if we're able to shift the disjointed number domain back so that it's connected. 
+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).
 
@@ -530,7 +530,7 @@ function overflowInt64_2(int256 value) public pure returns (bool overflow) {
 }
 ```
 
-In this case the verbose assembly code might actually be easier to follow than the Solidity code which can sometimes contain implicit operations.
+In this case the verbose assembly code might actually be easier to follow than the Solidity code which sometimes contains implicit operations.
 
 ```solidity
 int64 constant INT64_MIN = -0x8000000000000000;
@@ -544,7 +544,7 @@ function overflowInt64_2_yul(int256 value) public pure returns (bool overflow) {
 ```
 
 As mentioned earlier, this approach is only effective for negative numbers when all of their upper bits are set to `1`, allowing us to overflow back into the positive domain. 
-An alternative and more straightforward method would be to verify that all of the upper bits are equivalent to the sign bit.
+An alternative and more straightforward method would be to simply verify that all of the upper bits are equivalent to the sign bit for all integers.
 
 ```solidity
 function overflowInt64_3(int256 value) public pure returns (bool overflow) {
@@ -618,7 +618,7 @@ function checkedMulInt64(int64 a, int64 b) public pure returns (int64 c) {
 
 However, if the maximum value of a product exceeds 256 bits, then this method won't be effective. 
 This happens, for instance, when working with int192. The product `type(int192).min * type(int192).min` requires 192 + 192 = 384 bits to be stored, which exceeds the maximum of 256 bits. 
-Overflow occurs in 256 bits, resulting in a `0`, and it won't be logical to check if the result fits into 192 bits.
+Overflow occurs in 256 bits, which loses information, and it won't be logical to check if the result fits into 192 bits.
 In this scenario, we can depend on the previous checks and, for example, attempt to reconstruct one of the multiplicands.
 
 ```solidity
@@ -636,7 +636,7 @@ Once more, we must consider the two special circumstances:
 1. When one of the multiplicands is zero (`a == 0`), the other multiplicand cannot be retrieved. However, this case never results in overflow.
 2. Even if the multiplication is correct in 256 bits, the calculation overflows when only examining the least-significant 192 bits if the first multiplicand is minus one (`a = -1`) and the other multiplicand is the minimum value.
 
-The second exceptional scenario is still relevant since it is possible to encounter overflow when only considering the least-significant 192 bits, despite the multiplication being correct in 256 bits.
+An example might help explain the second case.
 
 ```solidity
   0xffffffffffffffff800000000000000000000000000000000000000000000000 // type(int192).min
@@ -644,8 +644,8 @@ The second exceptional scenario is still relevant since it is possible to encoun
 = 0x0000000000000000800000000000000000000000000000000000000000000000 // type(int192).min (when seen as a int192)
 ```
 
-To handle this particular case, we can always start by sign-extending or cleaning the result before attempting to reconstruct the other multiplicand.
-This removes one of the checks.
+A way to handle this is to always start by sign-extending or cleaning the result before attempting to reconstruct the other multiplicand.
+This then removes the need for checking the special condition.
 
 ```solidity
 /// @notice version >= 0.8.17

From c333b8f9af64cc90200baa292696fabf0ea3e41b Mon Sep 17 00:00:00 2001
From: 0xphaze <0xphaze@gmail.com>
Date: Tue, 7 Mar 2023 14:23:30 +0100
Subject: [PATCH 04/11] fix: remove book submodule

---
 book | 1 -
 1 file changed, 1 deletion(-)
 delete mode 160000 book

diff --git a/book b/book
deleted file mode 160000
index c7f4f09d..00000000
--- a/book
+++ /dev/null
@@ -1 +0,0 @@
-Subproject commit c7f4f09d0d089d13c26d8d17dcb17456f280b27b

From 5157dd685ecc9e201b1f45160a3889f8f93a8ff9 Mon Sep 17 00:00:00 2001
From: 0xphaze <0xphaze@gmail.com>
Date: Thu, 23 Mar 2023 16:44:24 +0100
Subject: [PATCH 05/11] Format document

---
 learn_evm/arithmetic-checks.md | 113 +++++++++++++++++----------------
 1 file changed, 57 insertions(+), 56 deletions(-)

diff --git a/learn_evm/arithmetic-checks.md b/learn_evm/arithmetic-checks.md
index 70ae43bf..d86c0474 100644
--- a/learn_evm/arithmetic-checks.md
+++ b/learn_evm/arithmetic-checks.md
@@ -3,17 +3,17 @@
 The EVM is a peculiar machine that many of us have come to love and hate for all its quirks.
 One such quirk is the absence of native arithmetic checks, which are typically present in most architectures and virtual machines through the use of carry bits or an overflow flag.
 The EVM treats all stack values as uint256 types.
-Although opcodes for signed integers (such as `sdiv`, `smod`, `slt`, `sgt`, etc.) exist, 
+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`.
 > These would provide built-in overflow flags. However, the EIP's current status is stagnant.
 
-Since Solidity version 0.8.0 the compiler includes over and underflow protection in all arithmetic operations by default. 
+Since Solidity version 0.8.0 the compiler includes over and underflow protection in all arithmetic operations by default.
 Before version 0.8.0, these checks had to be implemented manually - a commonly used library is called [SafeMath](https://github.com/OpenZeppelin/openzeppelin-contracts/blob/master/contracts/utils/math/SafeMath.sol), originally developed by OpenZeppelin.
 Much like how SafeMath works, arithmetic checks are inserted by the compiler through additional operations.
 
-> **Disclaimer:** Please note that this post is for educational purposes. 
+> **Disclaimer:** Please note that this post is for educational purposes.
 > It is not our intention to encourage micro optimizations in order to save gas,
 > as this can potentially lead to the introduction of new bugs that are difficult to detect and may compromise the security and stability of the protocol.
 > As a protocol developer, it is important to prioritize the safety and security of the protocol over [premature optimization](https://www.youtube.com/watch?v=tKbV6BpH-C8).
@@ -22,11 +22,12 @@ Much like how SafeMath works, arithmetic checks are inserted by the compiler thr
 
 ## Arithmetic checks for uint256 addition
 
-To investigate how the solc compiler implements arithmetic checks, we can compile the code with the `--asm` flag and inspect the resulting bytecode. 
+To investigate how the solc compiler implements arithmetic checks, we can compile the code with the `--asm` flag and inspect the resulting bytecode.
 Alternatively, by using the `--ir` flag, we can examine the Yul code that is generated as an intermediate representation (IR).
-> It's worth noting that Solidity aims to make the new Yul pipeline the standard. 
-> Certain operations (including arithmetic checks) are always included as Yul code, regardless of whether the code is compiled with the new pipeline using `--via-ir`. 
-> This provides an opportunity to examine the Yul code and gain a better understanding of how arithmetic checks are executed in Solidity. 
+
+> It's worth noting that Solidity aims to make the new Yul pipeline the standard.
+> Certain operations (including arithmetic checks) are always included as Yul code, regardless of whether the code is compiled with the new pipeline using `--via-ir`.
+> This provides an opportunity to examine the Yul code and gain a better understanding of how arithmetic checks are executed in Solidity.
 > However, it's important to keep in mind that the final bytecode may differ slightly when compiler optimizations are turned on.
 
 To illustrate how the compiler detects overflow in unsigned integer addition, consider the following example of Yul code that is produced by the compiler.
@@ -58,9 +59,9 @@ function checkedAddUint1(uint256 a, uint256 b) public pure returns (uint256 c) {
 
 > Solidity's arithmetic errors are encoded as `abi.encodeWithSignature("Panic(uint256)", 0x11)`.
 
-The check for overflow in unsigned integer addition involves calculating the largest value that one summand can be added to the other without resulting in an overflow. 
-Specifically, in this case, the maximum value that `a` can have is `type(uint256).max - b`. 
-If `a` exceeds this value, we can conclude that `a + b` will overflow. 
+The check for overflow in unsigned integer addition involves calculating the largest value that one summand can be added to the other without resulting in an overflow.
+Specifically, in this case, the maximum value that `a` can have is `type(uint256).max - b`.
+If `a` exceeds this value, we can conclude that `a + b` will overflow.
 
 An alternative (and slightly more efficient) approach to computing the maximum value of `a` is to invert the bits on `b`.
 
@@ -78,10 +79,11 @@ function checkedAddUint2(uint256 a, uint256 b) public pure returns (uint256 c) {
 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`.
 > 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, 
+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.
 
 ```solidity
@@ -95,9 +97,9 @@ function checkedAddUint(uint256 a, uint256 b) public pure returns (uint256 c) {
 }
 ```
 
-Overflow is detected when the sum is smaller than one of its summands. 
-In other words, if `a > a + b`, then overflow has occurred. 
-A full proof of this requires verifying that overflow occurs if and only if `a > a + b`. 
+Overflow is detected when the sum is smaller than one of its summands.
+In other words, if `a > a + b`, then overflow has occurred.
+A full proof of this requires verifying that overflow occurs if and only if `a > a + b`.
 An important observation is that `a > a + b` (mod `2**256`) for `b > 0` is only possible when `b >= 2**256`, which exceeds the maximum possible value.
 
 ## Arithmetic checks for int256 addition
@@ -136,14 +138,14 @@ function checked_add_t_int256(x, y) -> sum {
 }
 ```
 
-It's important to note that when comparing signed values, we must use the opcodes `slt` (signed less than) and `sgt` (signed greater than) to avoid interpreting signed integers as unsigned integers. 
+It's important to note that when comparing signed values, we must use the opcodes `slt` (signed less than) and `sgt` (signed greater than) to avoid interpreting signed integers as unsigned integers.
 Solidity will automatically insert the correct opcode based on the type of the value. This applies to other signed operations as well.
 
 ### Quick primer on a two's complement system
 
-In a two's complement system, the range of possible integers is divided into two halves: the positive and negative domain. 
-The first bit of an integer represents the sign, with `0` indicating a positive number and `1` indicating a negative number. 
-For positive integers (those with a sign bit of `0`), their binary representation is the same as their unsigned bit representation. 
+In a two's complement system, the range of possible integers is divided into two halves: the positive and negative domain.
+The first bit of an integer represents the sign, with `0` indicating a positive number and `1` indicating a negative number.
+For positive integers (those with a sign bit of `0`), their binary representation is the same as their unsigned bit representation.
 However, the negative domain is shifted to lie "above" the positive domain.
 
 ```
@@ -161,31 +163,31 @@ However, the negative domain is shifted to lie "above" the positive domain.
 0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff // -1
 ```
 
-The maximum positive integer that can be represented in a two's complement system using int256 is 
-`0x7fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff` which is equal to half of the maximum value that can be represented using uint256. 
+The maximum positive integer that can be represented in a two's complement system using int256 is
+`0x7fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff` which is equal to half of the maximum value that can be represented using uint256.
 The most significant bit of this number is `0`, while all other bits are `1`.
 
-On the other hand, all negative numbers start with a `1` as their first bit. 
+On the other hand, all negative numbers start with a `1` as their first bit.
 If we look at the underlying hex representation of these numbers, they are all greater than or equal to the smallest integer that can be represented using int256, which is `0x8000000000000000000000000000000000000000000000000000000000000000` (equal to `1` shifted 255 bits to the left).
 
 To obtain the negative value of an integer in a two's complement system, we can flip all the underlying bits and add `1`: `-a = ~a + 1`.
 An example illustrates this.
 
-```solidity 
+```solidity
 0x0000000000000000000000000000000000000000000000000000000000000003 // 3
 0xfffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffc // ~3
 0xfffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffd // -3 = ~3 + 1
 ```
 
-To verify that `-a + a = 0` holds for all integers, we can use the property of two's complement arithmetic that `-a = ~a + 1`. 
+To verify that `-a + a = 0` holds for all integers, we can use the property of two's complement arithmetic that `-a = ~a + 1`.
 By substituting this into the equation, we get `-a + a = (~a + 1) + a = MAX + 1 = 0`, where `MAX` is the maximum integer value.
 
 There is a unique case that needs special attention in two's complement arithmetic.
 The smallest possible integer `int256).min = 0x8000000000000000000000000000000000000000000000000000000000000000 = -57896044618658097711785492504343953926634992332820282019728792003956564819968`
 does not have a positive inverse for addition, making it the only negative number with this property.
 
-Interestingly, if we try to compute `-type(int256).min`, we get the same number, as `-type(int256).min = ~type(int256).min + 1 = type(int256).min`. 
-This means there are two fixed points for additive inverses: `-0 = 0` and `-type(int256).min = type(int256).min`. 
+Interestingly, if we try to compute `-type(int256).min`, we get the same number, as `-type(int256).min = ~type(int256).min + 1 = type(int256).min`.
+This means there are two fixed points for additive inverses: `-0 = 0` and `-type(int256).min = type(int256).min`.
 It's important to note that Solidity's arithmetic checks will throw an error when evaluating `-type(int256).min` (outside of unchecked blocks).
 
 Finally, looking at the underlying bit (or hex) representation highlights the importance of using the correct operators for signed integers, such as `slt` instead of `lt`, to avoid misinterpreting negative values as large numbers.
@@ -199,8 +201,8 @@ Finally, looking at the underlying bit (or hex) representation highlights the im
 = 0x0000000000000000000000000000000000000000000000000000000000000000
 ```
 
-Newer versions of Solidity prevent integer overflow by using the computed result `c = a + b` to check for overflow/underflow. 
-However, unlike unsigned addition, signed addition requires two separate checks instead of one. 
+Newer versions of Solidity prevent integer overflow by using the computed result `c = a + b` to check for overflow/underflow.
+However, unlike unsigned addition, signed addition requires two separate checks instead of one.
 
 ```solidity
 /// @notice versions >=0.8.16
@@ -260,10 +262,8 @@ we can use the `slt` operation to compare the value with `0`.
 
 ## Arithmetic checks for uint256 subtraction
 
-
-The process of checking for underflow in subtraction is akin to that of addition. 
-If we subtract `a - b`, and `b` is greater than `a`, we have an underflow situation. 
-
+The process of checking for underflow in subtraction is akin to that of addition.
+If we subtract `a - b`, and `b` is greater than `a`, we have an underflow situation.
 
 ```solidity
 function checkedSubUint(uint256 a, uint256 b) public pure returns (uint256 c) {
@@ -275,8 +275,8 @@ function checkedSubUint(uint256 a, uint256 b) public pure returns (uint256 c) {
 }
 ```
 
-We could, like before, perform the check on the result itself using `if (c > a) arithmeticError();`, because subtracting a positive value from `a` should yield a value less than or equal to `a`. 
-However, in this case, we don't save any operations. 
+We could, like before, perform the check on the result itself using `if (c > a) arithmeticError();`, because subtracting a positive value from `a` should yield a value less than or equal to `a`.
+However, in this case, we don't save any operations.
 
 Just as with addition, for signed integers, we can combine the checks for both scenarios into a single check using `xor`.
 
@@ -300,7 +300,7 @@ function checkedSubInt(int256 a, int256 b) public pure returns (int256 c) {
 
 ## Arithmetic checks for uint256 multiplication
 
-To detect overflow when multiplying two unsigned integers, we can again use the approach of computing the maximum possible value of a multiplicand and check that it isn't exceeded. 
+To detect overflow when multiplying two unsigned integers, we can again use the approach of computing the maximum possible value of a multiplicand and check that it isn't exceeded.
 
 ```solidity
 /// @notice versions >=0.8.0 && <0.8.17
@@ -313,11 +313,11 @@ function checkedMulUint1(uint256 a, uint256 b) public pure returns (uint256 c) {
 }
 ```
 
-> 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. 
-> The EVM itself simply returns `0` when dividing by `0`, and this also applies to inline-assembly. 
+> 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.
+> The EVM itself simply returns `0` when dividing by `0`, and this also applies to inline-assembly.
 > If the order of the boolean expressions is evaluated in reverse order, it could cause an arithmetic check to incorrectly revert when `a = 0`.
 
-We can compute the maximum value for `b` as long as `a` is non-zero. However, if `a` is zero, we know that the result will be zero as well, and there is no need to check for overflow. 
+We can compute the maximum value for `b` as long as `a` is non-zero. However, if `a` is zero, we know that the result will be zero as well, and there is no need to check for overflow.
 Like before, we can also make use of the result and try to reconstruct one multiplicand from it. This is possible if the product didn't overflow and the first multiplicand is non-zero.
 
 ```solidity
@@ -390,10 +390,10 @@ This is because `-b` cannot be represented as a positive signed integer, as prev
 
 ## Arithmetic checks for addition with sub-32-byte types
 
-When performing arithmetic checks on data types that use less than 32 bytes, there are some additional steps to consider. 
+When performing arithmetic checks on data types that use less than 32 bytes, there are some additional steps to consider.
 First, let's take a look at the addition of signed 64-bit integers.
 
-On a 64-bit system, integer addition works in the same way as before. 
+On a 64-bit system, integer addition works in the same way as before.
 
 ```solidity
   0xfffffffffffffffe // int64(-2)
@@ -411,9 +411,9 @@ otherwise the value won't be interpreted correctly.
 = 0x0000000000000000000000000000000000000000000000000000000000000001 // int64(1)
 ```
 
-It's worth noting that not all operations require clean upper bits. 
-In fact, even if the upper bits are dirty, we can still get correct results for addition. 
-However, the sum will usually contain dirty upper bits that will need to be cleaned. 
+It's worth noting that not all operations require clean upper bits.
+In fact, even if the upper bits are dirty, we can still get correct results for addition.
+However, the sum will usually contain dirty upper bits that will need to be cleaned.
 For example, when performing addition without knowing what the upper bits are set to, we get the following result.
 
 ```solidity
@@ -422,13 +422,13 @@ For example, when performing addition without knowing what the upper bits are se
 = 0x????????????????????????????????????????????????0000000000000001 // int64(1)
 ```
 
-> It is crucial to be mindful of when to clean the bits before and after operations. 
-> By default, Solidity takes care of cleaning the bits before operations on smaller types and lets the optimizer remove any redundant steps. 
-> However, values accessed after operations included by the compiler are not guaranteed to be clean. In particular, this is the case for addition with small data types. 
-> The bit cleaning steps will be removed by the optimizer (even without optimizations enabled) if a variable is only accessed in a subsequent assembly block. 
+> It is crucial to be mindful of when to clean the bits before and after operations.
+> By default, Solidity takes care of cleaning the bits before operations on smaller types and lets the optimizer remove any redundant steps.
+> However, values accessed after operations included by the compiler are not guaranteed to be clean. In particular, this is the case for addition with small data types.
+> The bit cleaning steps will be removed by the optimizer (even without optimizations enabled) if a variable is only accessed in a subsequent assembly block.
 > Refer to the [Solidity documentation](https://docs.soliditylang.org/en/v0.8.18/internals/variable_cleanup.html#cleaning-up-variables) for further information on this matter.
 
-When performing arithmetic checks in the same way as before, it is necessary to include a step to clean the bits on the sum. 
+When performing arithmetic checks in the same way as before, it is necessary to include a step to clean the bits on the sum.
 One approach to achieve this is by performing `signextend(7, value)`, which extends the sign of a 64-bit (7 + 1 = 8 bytes) integer over all upper bits.
 
 ```solidity
@@ -476,8 +476,8 @@ function checkedAddInt64_2(int64 a, int64 b) public pure returns (int64 c) {
 }
 ```
 
-There are a few ways to verify that the result in its 256-bit representation will fit into the expected data type. 
-This is only true when all upper bits are the same. 
+There are a few ways to verify that the result in its 256-bit representation will fit into the expected data type.
+This is only true when all upper bits are the same.
 The most direct method, as just shown, involves checking the lower and upper bounds of the value.
 
 ```solidity
@@ -487,8 +487,8 @@ function overflowInt64(int256 value) public pure returns (bool overflow) {
 }
 ```
 
-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). 
+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).
 
 ```
@@ -543,7 +543,7 @@ function overflowInt64_2_yul(int256 value) public pure returns (bool overflow) {
 }
 ```
 
-As mentioned earlier, this approach is only effective for negative numbers when all of their upper bits are set to `1`, allowing us to overflow back into the positive domain. 
+As mentioned earlier, this approach is only effective for negative numbers when all of their upper bits are set to `1`, allowing us to overflow back into the positive domain.
 An alternative and more straightforward method would be to simply verify that all of the upper bits are equivalent to the sign bit for all integers.
 
 ```solidity
@@ -598,7 +598,7 @@ function checkedAddInt64_2(int64 a, int64 b) public pure returns (int64 c) {
 
 ## Arithmetic checks for multiplication with sub-32-byte types
 
-If the product `c = a * b` can be calculated in 256 bits without the possibility of overflowing, we can once again verify whether the result can fit into the anticipated data type. 
+If the product `c = a * b` can be calculated in 256 bits without the possibility of overflowing, we can once again verify whether the result can fit into the anticipated data type.
 This is also the way Solidity handles the check in newer versions.
 
 ```solidity
@@ -616,8 +616,8 @@ function checkedMulInt64(int64 a, int64 b) public pure returns (int64 c) {
 }
 ```
 
-However, if the maximum value of a product exceeds 256 bits, then this method won't be effective. 
-This happens, for instance, when working with int192. The product `type(int192).min * type(int192).min` requires 192 + 192 = 384 bits to be stored, which exceeds the maximum of 256 bits. 
+However, if the maximum value of a product exceeds 256 bits, then this method won't be effective.
+This happens, for instance, when working with int192. The product `type(int192).min * type(int192).min` requires 192 + 192 = 384 bits to be stored, which exceeds the maximum of 256 bits.
 Overflow occurs in 256 bits, which loses information, and it won't be logical to check if the result fits into 192 bits.
 In this scenario, we can depend on the previous checks and, for example, attempt to reconstruct one of the multiplicands.
 
@@ -633,6 +633,7 @@ function checkedMulInt192_1(int192 a, int192 b) public pure returns (int192 c) {
 ```
 
 Once more, we must consider the two special circumstances:
+
 1. When one of the multiplicands is zero (`a == 0`), the other multiplicand cannot be retrieved. However, this case never results in overflow.
 2. Even if the multiplication is correct in 256 bits, the calculation overflows when only examining the least-significant 192 bits if the first multiplicand is minus one (`a = -1`) and the other multiplicand is the minimum value.
 
@@ -664,4 +665,4 @@ function checkedMulInt192_2(int192 a, int192 b) public pure returns (int192 c) {
         if (overflow) arithmeticError();
     }
 }
-```
\ No newline at end of file
+```

From 86d1e7d15de3719a32b6978813053b178522a3f8 Mon Sep 17 00:00:00 2001
From: 0xphaze <0xphaze@gmail.com>
Date: Thu, 23 Mar 2023 17:04:39 +0100
Subject: [PATCH 06/11] Fix suggestions

---
 learn_evm/arithmetic-checks.md | 18 +++++++++---------
 1 file changed, 9 insertions(+), 9 deletions(-)

diff --git a/learn_evm/arithmetic-checks.md b/learn_evm/arithmetic-checks.md
index d86c0474..ea8f9c0d 100644
--- a/learn_evm/arithmetic-checks.md
+++ b/learn_evm/arithmetic-checks.md
@@ -80,7 +80,7 @@ This is equivalent, because `type(uint256).max` is a 256-bit integer with all it
 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`.
+> 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 equals `MAX`.
 > 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,
@@ -218,8 +218,8 @@ function checkedAddInt2(int256 a, int256 b) public pure returns (int256 c) {
 }
 ```
 
-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.
+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.
 
 ```solidity
 function checkedAddInt3(int256 a, int256 b) public pure returns (int256 c) {
@@ -384,7 +384,7 @@ function checkedMulInt2(int256 a, int256 b) public pure returns (int256 c) {
 }
 ```
 
-When it comes to integer multiplication, it's important to handle the case hen `a < 0` and `b == type(int256).min`.
+When it comes to integer multiplication, it's important to handle the case when `a < 0` and `b == type(int256).min`.
 The actual case, where the product `c` will overflow, is limited to `a == -1` and `b == type(int256).min`.
 This is because `-b` cannot be represented as a positive signed integer, as previously mentioned.
 
@@ -422,11 +422,11 @@ For example, when performing addition without knowing what the upper bits are se
 = 0x????????????????????????????????????????????????0000000000000001 // int64(1)
 ```
 
-> It is crucial to be mindful of when to clean the bits before and after operations.
-> By default, Solidity takes care of cleaning the bits before operations on smaller types and lets the optimizer remove any redundant steps.
-> However, values accessed after operations included by the compiler are not guaranteed to be clean. In particular, this is the case for addition with small data types.
-> The bit cleaning steps will be removed by the optimizer (even without optimizations enabled) if a variable is only accessed in a subsequent assembly block.
-> Refer to the [Solidity documentation](https://docs.soliditylang.org/en/v0.8.18/internals/variable_cleanup.html#cleaning-up-variables) for further information on this matter.
+It is crucial to be mindful of when to clean the bits before and after operations.
+By default, Solidity takes care of cleaning the bits before operations on smaller types and lets the optimizer remove any redundant steps.
+However, values accessed after operations included by the compiler are not guaranteed to be clean. In particular, this is the case for addition with small data types.
+The bit cleaning steps will be removed by the optimizer (even without optimizations enabled) if a variable is only accessed in a subsequent assembly block.
+Refer to the [Solidity documentation](https://docs.soliditylang.org/en/v0.8.18/internals/variable_cleanup.html#cleaning-up-variables) for further information on this matter.
 
 When performing arithmetic checks in the same way as before, it is necessary to include a step to clean the bits on the sum.
 One approach to achieve this is by performing `signextend(7, value)`, which extends the sign of a 64-bit (7 + 1 = 8 bytes) integer over all upper bits.

From 83091b8c6a5144639554f0dd6fd64d29769a5a70 Mon Sep 17 00:00:00 2001
From: 0xphaze <0xphaze@gmail.com>
Date: Mon, 10 Apr 2023 13:20:39 +0100
Subject: [PATCH 07/11] Include suggestions

---
 learn_evm/arithmetic-checks.md | 165 ++++++++++++++++++++++-----------
 1 file changed, 111 insertions(+), 54 deletions(-)

diff --git a/learn_evm/arithmetic-checks.md b/learn_evm/arithmetic-checks.md
index ea8f9c0d..4fe0d1a2 100644
--- a/learn_evm/arithmetic-checks.md
+++ b/learn_evm/arithmetic-checks.md
@@ -1,22 +1,28 @@
 # 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.
-One such quirk is the absence of native arithmetic checks, which are typically present in most architectures and virtual machines through the use of carry bits or an overflow flag.
-The EVM treats all stack values as uint256 types.
-Although opcodes for signed integers (such as `sdiv`, `smod`, `slt`, `sgt`, etc.) exist,
-arithmetic checks must be implemented within the constraints of the EVM.
+The Ethereum Virtual Machine (EVM) distinguishes itself from traditional computer systems and virtual machines through several unique aspects.
+One notable variation is its treatment of arithmetic checks.
+While most architectures and virtual machines offer access to carry bits or an overflow flag,
+these features are not present in the EVM.
+As a result, developers must manually incorporate these safeguards within the machine's constraints.
 
-> Note: [EIP-1051](https://eips.ethereum.org/EIPS/eip-1051)'s goal is to introduce the opcodes `ovf` and `sovf`.
-> These would provide built-in overflow flags. However, the EIP's current status is stagnant.
+Starting with Solidity version 0.8.0 the compiler includes over and underflow protection in all arithmetic operations by default.
+Prior to version 0.8.0, developers had to implement these checks manually, often using a library known as [SafeMath](https://github.com/OpenZeppelin/openzeppelin-contracts/blob/master/contracts/utils/math/SafeMath.sol), originally developed by OpenZeppelin.
+Much like how SafeMath works, the compiler inserts arithmetic checks through additional operations.
 
-Since Solidity version 0.8.0 the compiler includes over and underflow protection in all arithmetic operations by default.
-Before version 0.8.0, these checks had to be implemented manually - a commonly used library is called [SafeMath](https://github.com/OpenZeppelin/openzeppelin-contracts/blob/master/contracts/utils/math/SafeMath.sol), originally developed by OpenZeppelin.
-Much like how SafeMath works, arithmetic checks are inserted by the compiler through additional operations.
+In this article, we'll explore many ways to perform arithmetic checks within the EVM.
+This guide is designed for those with a keen interest in bit manipulations and seek a deeper understanding of the EVM's inner workings.
+It is assumed that you have a basic understanding of bitwise arithmetic and Solidity opcodes.
 
-> **Disclaimer:** Please note that this post is for educational purposes.
+Some additional references for complementary reading are:
+
+- [evm.codes](https://evm.codes)
+- [Understanding Two's Complement](https://www.geeksforgeeks.org/twos-complement/)
+
+> **Disclaimer:** Please note that this article is for educational purposes.
 > It is not our intention to encourage micro optimizations in order to save gas,
-> as this can potentially lead to the introduction of new bugs that are difficult to detect and may compromise the security and stability of the protocol.
-> As a protocol developer, it is important to prioritize the safety and security of the protocol over [premature optimization](https://www.youtube.com/watch?v=tKbV6BpH-C8).
+> as this can potentially lead to the introduction of new bugs that are difficult to detect and may compromise the security and stability of a protocol.
+> As a developer, it is important to prioritize the safety and security of the protocol over [premature optimization](https://www.youtube.com/watch?v=tKbV6BpH-C8).
 > In situations where the code for the protocol is still evolving, including redundant checks for critical operations may be a good practice.
 > However, we do encourage experimentation with these operations for educational purposes.
 
@@ -30,7 +36,7 @@ Alternatively, by using the `--ir` flag, we can examine the Yul code that is gen
 > This provides an opportunity to examine the Yul code and gain a better understanding of how arithmetic checks are executed in Solidity.
 > However, it's important to keep in mind that the final bytecode may differ slightly when compiler optimizations are turned on.
 
-To illustrate how the compiler detects overflow in unsigned integer addition, consider the following example of Yul code that is produced by the compiler.
+To illustrate how the compiler detects overflow in unsigned integer addition, consider the following example of Yul code that is produced by the compiler before version 0.8.16.
 
 ```solidity
 function checked_add_t_uint256(x, y) -> sum {
@@ -84,7 +90,8 @@ This can be demonstrated by the transformation `~b = ~(0 ^ b) = ~0 ^ b = MAX ^ b
 > 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.
+we eliminate the need for performing extra arithmetic operations in the comparison.
+This is how the compiler implements arithmetic checks for unsigned integer addition in versions 0.8.16 and later.
 
 ```solidity
 /// @notice versions >=0.8.16
@@ -104,7 +111,7 @@ An important observation is that `a > a + b` (mod `2**256`) for `b > 0` is only
 
 ## Arithmetic checks for int256 addition
 
-The Solidity compiler generates the following (equivalent) code for detecting overflow in signed integer addition:
+The Solidity compiler generates the following (equivalent) code for detecting overflow in signed integer addition below version 0.8.16.
 
 ```solidity
 /// @notice versions >=0.8.0 && <0.8.16
@@ -148,14 +155,28 @@ The first bit of an integer represents the sign, with `0` indicating a positive
 For positive integers (those with a sign bit of `0`), their binary representation is the same as their unsigned bit representation.
 However, the negative domain is shifted to lie "above" the positive domain.
 
-```
-| -------------------------------- uint256 -------------------------------- |
-0 --------------------------------------------------------------------- uint256_max
+$$uint256 \text{ domain}$$
+
+$$
+├\underset{0}{─}────────────────────────────\underset{\hskip -1.5em 2^{256} - 1}{─}┤
+$$
 
-| --------- positive int256 --------- | --------- negative int256 --------- |
-0 ------------------------ int256_max | int256_min ------------------------ -1
+```solidity
+0x0000000000000000000000000000000000000000000000000000000000000000 // 0
+0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff // uint256_max
 ```
 
+$$int256 \text{ domain}$$
+
+$$
+\overset{\hskip 1em positive}{
+    ├\underset{0}{─}────────────\underset{\hskip -2em 2^{255} - 1}{─}┤
+}
+\overset{\hskip 1em negative}{
+    ├────\underset{\hskip -3.5em - 2^{255}}─────────\underset{\hskip -0.4 em -1}{─}┤
+}
+$$
+
 ```solidity
 0x0000000000000000000000000000000000000000000000000000000000000000 // 0
 0x7fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff // int256_max
@@ -163,14 +184,14 @@ However, the negative domain is shifted to lie "above" the positive domain.
 0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff // -1
 ```
 
-The maximum positive integer that can be represented in a two's complement system using int256 is
-`0x7fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff` which is equal to half of the maximum value that can be represented using uint256.
+The maximum positive integer that can be represented in a two's complement system using 256 bits is
+`0x7fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff` which is roughly equal to half of the maximum value that can be represented using uint256.
 The most significant bit of this number is `0`, while all other bits are `1`.
 
 On the other hand, all negative numbers start with a `1` as their first bit.
-If we look at the underlying hex representation of these numbers, they are all greater than or equal to the smallest integer that can be represented using int256, which is `0x8000000000000000000000000000000000000000000000000000000000000000` (equal to `1` shifted 255 bits to the left).
+If we look at the underlying hex representation of these numbers, they are all greater than or equal to the smallest integer that can be represented using int256, which is `0x8000000000000000000000000000000000000000000000000000000000000000`. The integer's binary representation is a `1` followed by 255 `0`'s.
 
-To obtain the negative value of an integer in a two's complement system, we can flip all the underlying bits and add `1`: `-a = ~a + 1`.
+To obtain the negative value of an integer in a two's complement system, we flip the underlying bits and add `1`: `-a = ~a + 1`.
 An example illustrates this.
 
 ```solidity
@@ -201,7 +222,7 @@ Finally, looking at the underlying bit (or hex) representation highlights the im
 = 0x0000000000000000000000000000000000000000000000000000000000000000
 ```
 
-Newer versions of Solidity prevent integer overflow by using the computed result `c = a + b` to check for overflow/underflow.
+Starting with Solidity versions 0.8.16, integer overflow is prevented by using the computed result `c = a + b` to check for overflow/underflow.
 However, unlike unsigned addition, signed addition requires two separate checks instead of one.
 
 ```solidity
@@ -218,8 +239,9 @@ function checkedAddInt2(int256 a, int256 b) public pure returns (int256 c) {
 }
 ```
 
-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.
+Nevertheless, by utilizing the boolean exclusive-or, we can combine these checks into a single step.
+While Solidity doesn't permit the `xor` operation for boolean values, it can still be employed through inline-assembly.
+While doing so, it is crucial to ensure that both inputs are genuinely boolean (either `0` or `1`), as the xor operation functions bitwise and is not limited to only boolean values.
 
 ```solidity
 function checkedAddInt3(int256 a, int256 b) public pure returns (int256 c) {
@@ -313,9 +335,9 @@ function checkedMulUint1(uint256 a, uint256 b) public pure returns (uint256 c) {
 }
 ```
 
-> 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.
-> The EVM itself simply returns `0` when dividing by `0`, and this also applies to inline-assembly.
-> If the order of the boolean expressions is evaluated in reverse order, it could cause an arithmetic check to incorrectly revert when `a = 0`.
+> The Solidity compiler always includes a zero check for all division and modulo operations, irrespective of whether an unchecked block is present.
+> The EVM itself, however, returns `0` when dividing by `0`, which applies to inline-assembly as well.
+> Evaluating the boolean expression `a != 0 && b > type(uint256).max / a` in reverse order would cause an incorrect reversion when `a = 0`.
 
 We can compute the maximum value for `b` as long as `a` is non-zero. However, if `a` is zero, we know that the result will be zero as well, and there is no need to check for overflow.
 Like before, we can also make use of the result and try to reconstruct one multiplicand from it. This is possible if the product didn't overflow and the first multiplicand is non-zero.
@@ -353,7 +375,7 @@ function checkedMulUint3(uint256 a, uint256 b) public pure returns (uint256 c) {
 
 ## Arithmetic checks for int256 multiplication
 
-In older versions, the Solidity compiler uses four separate checks to detect integer multiplication overflow.
+In versions before 0.8.17, the Solidity compiler uses four separate checks to detect integer multiplication overflow.
 The produced Yul code is equivalent to the following high-level Solidity code.
 
 ```solidity
@@ -370,7 +392,7 @@ function checkedMulInt(int256 a, int256 b) public pure returns (int256 c) {
 }
 ```
 
-Newer Solidity versions optimize the process by utilizing the computed product in the check.
+Since Solidity version 0.8.17, the check is performed by utilizing the computed product in the check.
 
 ```solidity
 /// @notice versions >=0.8.17
@@ -414,7 +436,7 @@ otherwise the value won't be interpreted correctly.
 It's worth noting that not all operations require clean upper bits.
 In fact, even if the upper bits are dirty, we can still get correct results for addition.
 However, the sum will usually contain dirty upper bits that will need to be cleaned.
-For example, when performing addition without knowing what the upper bits are set to, we get the following result.
+For example, we can perform addition without knowledge of the upper bits.
 
 ```solidity
   0x????????????????????????????????????????????????fffffffffffffffe // int64(-2)
@@ -425,7 +447,7 @@ For example, when performing addition without knowing what the upper bits are se
 It is crucial to be mindful of when to clean the bits before and after operations.
 By default, Solidity takes care of cleaning the bits before operations on smaller types and lets the optimizer remove any redundant steps.
 However, values accessed after operations included by the compiler are not guaranteed to be clean. In particular, this is the case for addition with small data types.
-The bit cleaning steps will be removed by the optimizer (even without optimizations enabled) if a variable is only accessed in a subsequent assembly block.
+For example, the bit cleaning steps will be removed by the optimizer (even without optimizations enabled) if a variable is only accessed in a subsequent assembly block.
 Refer to the [Solidity documentation](https://docs.soliditylang.org/en/v0.8.18/internals/variable_cleanup.html#cleaning-up-variables) for further information on this matter.
 
 When performing arithmetic checks in the same way as before, it is necessary to include a step to clean the bits on the sum.
@@ -491,33 +513,59 @@ We can simplify the expression to a single comparison if we're able to shift the
 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).
 
-```
-| -------------------------------- uint256 -------------------------------- |
-0 --------------------------------------------------------------------- uint256_max
+$$uint256 \text{ domain}$$
 
-| --------- positive int256 --------- | --------- negative int256 --------- |
-0 ------------------------ int256_max | int256_min ------------------------ -1
-```
+$$
+├\underset{0}{─}────────────────────────────\underset{\hskip -1.5em 2^{256} - 1}{─}┤
+$$
+
+$$int256 \text{ domain}$$
+
+$$
+\overset{\hskip 1em positive}{
+    ├\underset{0}{─}────────────\underset{\hskip -2em 2^{255} - 1}{─}┤
+}
+\overset{\hskip 1em negative}{
+    ├────\underset{\hskip -3.5em - 2^{255}}─────────\underset{\hskip -0.4 em -1}{─}┤
+}
+$$
 
 The domain for uint128/int128 can be visualized as follows.
 
-```
-| ------------ uint128 -------------- |                                     |
-0 ----------------------- uint128_max |                                     |
+$$uint128 \text{ domain}$$
 
-| -- pos int128 -- |                                     | -- neg int128 -- |
-0 ----- int128_max |                                     | int128_min ----- -1
-```
+$$
+├\underset{0}─────────────\underset{\hskip -2em 2^{128}-1}─┤
+\phantom{───────────────}┆
+$$
+
+$$int128 \text{ domain}$$
+
+$$
+\overset{\hskip 1em positive}{
+    ├\underset{0}{─}────\underset{\hskip -2em 2^{127} - 1}{─}┤
+}
+\phantom{────────────────}
+\overset{\hskip 1em negative}{
+    ├────\underset{\hskip -3.5em - 2^{127}}─\underset{\hskip -0.4 em -1}{─}┤
+}
+$$
+
+Note that the scales of the number ranges above do not accurately depict the magnitude of numbers that are representable with the different types and only serves as a visualization.
+We are able to represent twice as many numbers with only one additional bit. Yet, the uint256 domain has twice the number of bits compared to uint128.
 
 After subtracting `type(int128).min` we get the following, connected set of values.
 
-```
-| ------------ uint128 -------------- |                                     |
-0 ----------------------- uint128_max |                                     |
+$$
+├\underset{0}─────────────\underset{\hskip -2em 2^{128}-1}─┤
+\phantom{───────────────}┆
+$$
 
-| -- neg int128 -- | -- pos int128 -- |                                     |
-int128_min ----- -1| 0 --- int128_max |                                     |
-```
+$$
+\overset{\hskip 1em negative}{├──────┤}
+\overset{\hskip 1em positive}{├──────┤}
+\phantom{───────────────}┆
+$$
 
 If we interpret the shifted value as an unsigned integer, we only need to check whether it exceeds the maximum unsigned integer `type(uint128).max`.
 The corresponding check in Solidity is shown below.
@@ -596,10 +644,12 @@ function checkedAddInt64_2(int64 a, int64 b) public pure returns (int64 c) {
 }
 ```
 
+One further optimization that we could perform is to add `-type(int64).min` instead of subtracting `type(int64).min`. This would not reduce computation costs, however it could end up reducing bytecode size. This is because when we subtract `-type(int64).min`, we need to push 32 bytes (`0xffffffffffffffffffffffffffffffffffffffffffffffff8000000000000000`), whereas when we add `-type(int64).min`, we only end up pushing 8 bytes (`0x8000000000000000`). However, as soon as we turn on compiler optimizations, the produced bytecode ends up being the same.
+
 ## Arithmetic checks for multiplication with sub-32-byte types
 
 If the product `c = a * b` can be calculated in 256 bits without the possibility of overflowing, we can once again verify whether the result can fit into the anticipated data type.
-This is also the way Solidity handles the check in newer versions.
+This is also the way Solidity handles the check in versions 0.8.17 and later.
 
 ```solidity
 /// @notice version >= 0.8.17
@@ -666,3 +716,10 @@ function checkedMulInt192_2(int192 a, int192 b) public pure returns (int192 c) {
     }
 }
 ```
+
+## Conclusion
+
+In conclusion, this article has provided a comprehensive examination of arithmetic checks within the Ethereum Virtual Machine, delving into various Solidity opcodes and optimizations for assembly code. We have explored some of the intricacies of implementing arithmetic checks for both uint256 and int256 addition, subtraction, and multiplication, as well as for sub-32-byte types.
+Furthermore, we have highlighted some caveats to be aware of when working with assembly to avoid potential pitfalls.
+
+The purpose of this article is to deepen one's familiarity of low-level arithmetic, thereby improving the security of Solidity code by equipping developers to better assess and grasp the assumptions present in these operations. It is crucial to remember that custom low-level optimizations should be integrated only after rigorous manual analysis, fuzzing, and symbolic verification.

From 838d9f41e1f053e841a0573dcabdda0001b2e7f4 Mon Sep 17 00:00:00 2001
From: 0xphaze <0xphaze@gmail.com>
Date: Mon, 10 Apr 2023 13:28:19 +0100
Subject: [PATCH 08/11] Small fixes

---
 learn_evm/arithmetic-checks.md | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/learn_evm/arithmetic-checks.md b/learn_evm/arithmetic-checks.md
index 4fe0d1a2..528b5659 100644
--- a/learn_evm/arithmetic-checks.md
+++ b/learn_evm/arithmetic-checks.md
@@ -158,7 +158,7 @@ However, the negative domain is shifted to lie "above" the positive domain.
 $$uint256 \text{ domain}$$
 
 $$
-├\underset{0}{─}────────────────────────────\underset{\hskip -1.5em 2^{256} - 1}{─}┤
+├\underset{0}{─}────────────────────────────\underset{\hskip -2em 2^{256} - 1}{─}┤
 $$
 
 ```solidity
@@ -516,7 +516,7 @@ A better way to understand this is by visualizing the signed integer number doma
 $$uint256 \text{ domain}$$
 
 $$
-├\underset{0}{─}────────────────────────────\underset{\hskip -1.5em 2^{256} - 1}{─}┤
+├\underset{0}{─}────────────────────────────\underset{\hskip -2em 2^{256} - 1}{─}┤
 $$
 
 $$int256 \text{ domain}$$
@@ -554,7 +554,7 @@ $$
 Note that the scales of the number ranges above do not accurately depict the magnitude of numbers that are representable with the different types and only serves as a visualization.
 We are able to represent twice as many numbers with only one additional bit. Yet, the uint256 domain has twice the number of bits compared to uint128.
 
-After subtracting `type(int128).min` we get the following, connected set of values.
+After subtracting `type(int128).min` (or adding $2^{127}$) and essentially shifting the domains to the right, we get the following, connected set of values.
 
 $$
 ├\underset{0}─────────────\underset{\hskip -2em 2^{128}-1}─┤

From 7c80af0548f5e0f1d0a089be74cdfcb6bfb9bd6d Mon Sep 17 00:00:00 2001
From: 0xphaze <0xphaze@gmail.com>
Date: Fri, 14 Apr 2023 11:31:21 +0100
Subject: [PATCH 09/11] Fix review

---
 learn_evm/arithmetic-checks.md | 142 ++++++++++++++++-----------------
 1 file changed, 67 insertions(+), 75 deletions(-)

diff --git a/learn_evm/arithmetic-checks.md b/learn_evm/arithmetic-checks.md
index 528b5659..28c1132f 100644
--- a/learn_evm/arithmetic-checks.md
+++ b/learn_evm/arithmetic-checks.md
@@ -1,42 +1,42 @@
 # 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.
-One notable variation is its treatment of arithmetic checks.
-While most architectures and virtual machines offer access to carry bits or an overflow flag,
-these features are not present in the EVM.
-As a result, developers must manually incorporate these safeguards within the machine's constraints.
+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.
 
-Starting with Solidity version 0.8.0 the compiler includes over and underflow protection in all arithmetic operations by default.
-Prior to version 0.8.0, developers had to implement these checks manually, often using a library known as [SafeMath](https://github.com/OpenZeppelin/openzeppelin-contracts/blob/master/contracts/utils/math/SafeMath.sol), originally developed by OpenZeppelin.
-Much like how SafeMath works, the compiler inserts arithmetic checks through additional operations.
+Starting with Solidity version 0.8.0 the compiler automatically includes over and underflow protection in all arithmetic operations.
+Prior to version 0.8.0, developers were required to implement these checks manually, often using a library known as [SafeMath](https://github.com/OpenZeppelin/openzeppelin-contracts/blob/master/contracts/utils/math/SafeMath.sol), originally developed by OpenZeppelin.
+The compiler incorporates arithmetic checks in a manner similar to SafeMath, through additional operations.
 
-In this article, we'll explore many ways to perform arithmetic checks within the EVM.
-This guide is designed for those with a keen interest in bit manipulations and seek a deeper understanding of the EVM's inner workings.
-It is assumed that you have a basic understanding of bitwise arithmetic and Solidity opcodes.
+As the Solidity language has evolved, the compiler has generated increasingly optimized code for arithmetic checks. This trend is also observed in smart contract development in general, where highly optimized arithmetic code written in low-level assembly is becoming more common. However, there is still a lack of comprehensive resources explaining the nuances of how the EVM handles arithmetic for signed and unsigned integers of 256 bits and less.
 
-Some additional references for complementary reading are:
+This article serves as a guide for gaining a deeper understanding of arithmetic in the EVM by exploring various ways to perform arithmetic checks. We'll learn more about the two's complement system and some lesser-known opcodes. This article is designed for those curious about the EVM's inner workings and those interested in bit manipulations in general. A basic understanding of bitwise arithmetic and Solidity opcodes is assumed.
+
+Additional references for complementary reading are:
 
 - [evm.codes](https://evm.codes)
 - [Understanding Two's Complement](https://www.geeksforgeeks.org/twos-complement/)
 
 > **Disclaimer:** Please note that this article is for educational purposes.
 > It is not our intention to encourage micro optimizations in order to save gas,
-> as this can potentially lead to the introduction of new bugs that are difficult to detect and may compromise the security and stability of a protocol.
-> As a developer, it is important to prioritize the safety and security of the protocol over [premature optimization](https://www.youtube.com/watch?v=tKbV6BpH-C8).
-> In situations where the code for the protocol is still evolving, including redundant checks for critical operations may be a good practice.
+> as this can potentially introduce new, hard-to-detect bugs that may compromise the security and stability of a protocol.
+> As a developer, prioritize the safety and security of the protocol over [premature optimizations](https://www.youtube.com/watch?v=tKbV6BpH-C8).
+> Including redundant checks for critical operations may be a good practice when the protocol code is still evolving.
 > However, we do encourage experimentation with these operations for educational purposes.
 
 ## Arithmetic checks for uint256 addition
 
-To investigate how the solc compiler implements arithmetic checks, we can compile the code with the `--asm` flag and inspect the resulting bytecode.
-Alternatively, by using the `--ir` flag, we can examine the Yul code that is generated as an intermediate representation (IR).
+To examine how the solc compiler implements arithmetic checks, we can compile the code with the `--asm` flag and inspect the resulting bytecode.
+Alternatively, using the `--ir` flag allows us to examine the Yul code that is generated as an intermediate representation (IR).
 
-> It's worth noting that Solidity aims to make the new Yul pipeline the standard.
+> Note that Solidity aims to make the new Yul pipeline the standard.
 > Certain operations (including arithmetic checks) are always included as Yul code, regardless of whether the code is compiled with the new pipeline using `--via-ir`.
 > This provides an opportunity to examine the Yul code and gain a better understanding of how arithmetic checks are executed in Solidity.
-> However, it's important to keep in mind that the final bytecode may differ slightly when compiler optimizations are turned on.
+> However, keep in mind that the final bytecode may differ slightly when compiler optimizations are turned on.
 
-To illustrate how the compiler detects overflow in unsigned integer addition, consider the following example of Yul code that is produced by the compiler before version 0.8.16.
+To illustrate how the compiler detects overflow in unsigned integer addition, consider the following example of Yul code produced by the compiler before version 0.8.16.
 
 ```solidity
 function checked_add_t_uint256(x, y) -> sum {
@@ -50,7 +50,7 @@ function checked_add_t_uint256(x, y) -> sum {
 }
 ```
 
-To enhance readability, we can interpret the Yul code back into high-level Solidity code.
+To improve readability, we can translate the Yul code back into high-level Solidity code.
 
 ```solidity
 /// @notice versions >=0.8.0 && <0.8.16
@@ -65,11 +65,11 @@ function checkedAddUint1(uint256 a, uint256 b) public pure returns (uint256 c) {
 
 > Solidity's arithmetic errors are encoded as `abi.encodeWithSignature("Panic(uint256)", 0x11)`.
 
-The check for overflow in unsigned integer addition involves calculating the largest value that one summand can be added to the other without resulting in an overflow.
-Specifically, in this case, the maximum value that `a` can have is `type(uint256).max - b`.
+The check for overflow in unsigned integer addition involves calculating the largest value that one summand can have when added to the other without causing an overflow.
+Specifically, in this case, the maximum value `a` can have is `type(uint256).max - b`.
 If `a` exceeds this value, we can conclude that `a + b` will overflow.
 
-An alternative (and slightly more efficient) approach to computing the maximum value of `a` is to invert the bits on `b`.
+An alternative and slightly more efficient approach for computing the maximum value of `a` involves inverting the bits of `b`.
 
 ```solidity
 /// @notice versions >=0.8.0 && <0.8.16 with compiler optimizations
@@ -82,15 +82,14 @@ function checkedAddUint2(uint256 a, uint256 b) public pure returns (uint256 c) {
 }
 ```
 
-This is equivalent, because `type(uint256).max` is a 256-bit integer with all its bits set to `1`.
+This is process 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`.
+This transformation is demonstrated by `~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 equals `MAX`.
-> We also obtain the relation `~b + 1 = 0 - b = -b` if we add `1` mod `2**256` to both sides of the previous equation.
+> Note that `a - b = a ^ b` is **NOT** a general rule, except in special cases, such as when one of the values equals `type(uint256).max`.
+> The relation `~b + 1 = 0 - b = -b` is also obtained 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,
-we eliminate the need for performing extra arithmetic operations in the comparison.
+By first calculating the result of the addition and then performing a check on the sum, the need performing extra arithmetic operations are removed.
 This is how the compiler implements arithmetic checks for unsigned integer addition in versions 0.8.16 and later.
 
 ```solidity
@@ -104,14 +103,14 @@ function checkedAddUint(uint256 a, uint256 b) public pure returns (uint256 c) {
 }
 ```
 
-Overflow is detected when the sum is smaller than one of its summands.
+Overflow is detected when the sum is smaller than one of its addends.
 In other words, if `a > a + b`, then overflow has occurred.
-A full proof of this requires verifying that overflow occurs if and only if `a > a + b`.
+To fully prove this, it is necessary to verify that overflow occurs if and only if `a > a + b`.
 An important observation is that `a > a + b` (mod `2**256`) for `b > 0` is only possible when `b >= 2**256`, which exceeds the maximum possible value.
 
 ## Arithmetic checks for int256 addition
 
-The Solidity compiler generates the following (equivalent) code for detecting overflow in signed integer addition below version 0.8.16.
+The Solidity compiler generates the following (equivalent) code for detecting overflow in signed integer addition for versions below 0.8.16.
 
 ```solidity
 /// @notice versions >=0.8.0 && <0.8.16
@@ -127,7 +126,7 @@ function checkedAddInt(int256 a, int256 b) public pure returns (int256 c) {
 }
 ```
 
-Like before, we can compute the maximum and minimum value of a summand given that the other summand is either positive or negative.
+Similar to the previous example, we can compute the maximum and minimum value of one addend, given that the other is either positive or negative.
 
 For reference, this is the Yul code that is produced when compiling via IR.
 
@@ -145,12 +144,12 @@ function checked_add_t_int256(x, y) -> sum {
 }
 ```
 
-It's important to note that when comparing signed values, we must use the opcodes `slt` (signed less than) and `sgt` (signed greater than) to avoid interpreting signed integers as unsigned integers.
-Solidity will automatically insert the correct opcode based on the type of the value. This applies to other signed operations as well.
+It's important to note that when comparing signed values, the opcodes `slt` (signed less than) and `sgt` (signed greater than) must be used to avoid interpreting signed integers as unsigned integers.
+Solidity will automatically insert the correct opcode based on the value's type. This applies to other signed operations as well.
 
 ### Quick primer on a two's complement system
 
-In a two's complement system, the range of possible integers is divided into two halves: the positive and negative domain.
+In a two's complement system, the range of possible integers is divided into two halves: the positive and negative domains.
 The first bit of an integer represents the sign, with `0` indicating a positive number and `1` indicating a negative number.
 For positive integers (those with a sign bit of `0`), their binary representation is the same as their unsigned bit representation.
 However, the negative domain is shifted to lie "above" the positive domain.
@@ -203,15 +202,14 @@ An example illustrates this.
 To verify that `-a + a = 0` holds for all integers, we can use the property of two's complement arithmetic that `-a = ~a + 1`.
 By substituting this into the equation, we get `-a + a = (~a + 1) + a = MAX + 1 = 0`, where `MAX` is the maximum integer value.
 
-There is a unique case that needs special attention in two's complement arithmetic.
-The smallest possible integer `int256).min = 0x8000000000000000000000000000000000000000000000000000000000000000 = -57896044618658097711785492504343953926634992332820282019728792003956564819968`
-does not have a positive inverse for addition, making it the only negative number with this property.
+In two's complement arithmetic, there is a unique case that warrants special attention. The smallest possible integer `int256).min = 0x8000000000000000000000000000000000000000000000000000000000000000 = -57896044618658097711785492504343953926634992332820282019728792003956564819968`
+does not have a positive inverse, making it the only negative number with this property.
 
-Interestingly, if we try to compute `-type(int256).min`, we get the same number, as `-type(int256).min = ~type(int256).min + 1 = type(int256).min`.
+Interestingly, if we try to compute `-type(int256).min`, we obtain the same number, as `-type(int256).min = ~type(int256).min + 1 = type(int256).min`.
 This means there are two fixed points for additive inverses: `-0 = 0` and `-type(int256).min = type(int256).min`.
 It's important to note that Solidity's arithmetic checks will throw an error when evaluating `-type(int256).min` (outside of unchecked blocks).
 
-Finally, looking at the underlying bit (or hex) representation highlights the importance of using the correct operators for signed integers, such as `slt` instead of `lt`, to avoid misinterpreting negative values as large numbers.
+Examining the underlying bit (or hex) representation emphasizes the importance of using the correct operators for signed integers, such as `slt` instead of `lt`, to prevent misinterpreting negative values as large numbers.
 
 ```solidity
   0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff // int256(-1) or type(uint256).max
@@ -223,7 +221,7 @@ Finally, looking at the underlying bit (or hex) representation highlights the im
 ```
 
 Starting with Solidity versions 0.8.16, integer overflow is prevented by using the computed result `c = a + b` to check for overflow/underflow.
-However, unlike unsigned addition, signed addition requires two separate checks instead of one.
+However, signed addition requires two separate checks instead of one, unlike unsigned addition.
 
 ```solidity
 /// @notice versions >=0.8.16
@@ -240,8 +238,8 @@ function checkedAddInt2(int256 a, int256 b) public pure returns (int256 c) {
 ```
 
 Nevertheless, by utilizing the boolean exclusive-or, we can combine these checks into a single step.
-While Solidity doesn't permit the `xor` operation for boolean values, it can still be employed through inline-assembly.
-While doing so, it is crucial to ensure that both inputs are genuinely boolean (either `0` or `1`), as the xor operation functions bitwise and is not limited to only boolean values.
+Although Solidity does not allow the `xor` operation for boolean values, it can be used in inline-assembly.
+While doing so, it is important to validate our assumptions that both inputs are genuinely boolean (either `0` or `1`), as the xor operation functions bitwise and is not limited to only boolean values.
 
 ```solidity
 function checkedAddInt3(int256 a, int256 b) public pure returns (int256 c) {
@@ -262,9 +260,9 @@ function checkedAddInt3(int256 a, int256 b) public pure returns (int256 c) {
 }
 ```
 
-A different approach to detecting overflow in addition is to observe that adding two integers with different signs will never overflow.
-This reduces the check to the case when both summands have the same sign.
-If the sign of the sum is different from one of the summands, the result has overflowed.
+An alternative approach to detecting overflow in addition is based on the observation that adding two integers with different signs will never result in an overflow.
+This simplifies the check to the case when both operands have the same sign.
+If the sign of the sum differs from one of the operands, the result has overflowed.
 
 ```solidity
 function checkedAddInt4(int256 a, int256 b) public pure returns (int256 c) {
@@ -279,13 +277,13 @@ function checkedAddInt4(int256 a, int256 b) public pure returns (int256 c) {
 }
 ```
 
-Rather than checking the sign bit explicitly, which can be achieved by shifting the value to the right by 255 bits and checking that it is non-zero,
+Instead of checking the sign bit explicitly, which can be done by shifting the value to the right by 255 bits and verifying that it is non-zero,
 we can use the `slt` operation to compare the value with `0`.
 
 ## Arithmetic checks for uint256 subtraction
 
-The process of checking for underflow in subtraction is akin to that of addition.
-If we subtract `a - b`, and `b` is greater than `a`, we have an underflow situation.
+The process of checking for underflow in subtraction is similar to that of addition.
+When subtracting `a - b`, and `b` is greater than `a`, an underflow occurs.
 
 ```solidity
 function checkedSubUint(uint256 a, uint256 b) public pure returns (uint256 c) {
@@ -297,10 +295,10 @@ function checkedSubUint(uint256 a, uint256 b) public pure returns (uint256 c) {
 }
 ```
 
-We could, like before, perform the check on the result itself using `if (c > a) arithmeticError();`, because subtracting a positive value from `a` should yield a value less than or equal to `a`.
+Alternatively, we could perform the check on the result itself using `if (c > a) arithmeticError();`, because subtracting a positive value from `a` should yield a value less than or equal to `a`.
 However, in this case, we don't save any operations.
 
-Just as with addition, for signed integers, we can combine the checks for both scenarios into a single check using `xor`.
+Similar to addition, for signed integers, we can combine the checks for both scenarios into a single check using `xor`.
 
 ```solidity
 function checkedSubInt(int256 a, int256 b) public pure returns (int256 c) {
@@ -322,7 +320,7 @@ function checkedSubInt(int256 a, int256 b) public pure returns (int256 c) {
 
 ## Arithmetic checks for uint256 multiplication
 
-To detect overflow when multiplying two unsigned integers, we can again use the approach of computing the maximum possible value of a multiplicand and check that it isn't exceeded.
+To detect overflow when multiplying two unsigned integers, we can use the approach of computing the maximum possible value of a multiplicand and check that it isn't exceeded.
 
 ```solidity
 /// @notice versions >=0.8.0 && <0.8.17
@@ -433,10 +431,7 @@ otherwise the value won't be interpreted correctly.
 = 0x0000000000000000000000000000000000000000000000000000000000000001 // int64(1)
 ```
 
-It's worth noting that not all operations require clean upper bits.
-In fact, even if the upper bits are dirty, we can still get correct results for addition.
-However, the sum will usually contain dirty upper bits that will need to be cleaned.
-For example, we can perform addition without knowledge of the upper bits.
+It's worth noting that not all operations require clean upper bits. In fact, even if the upper bits are dirty, we can still get correct results for addition. However, the sum will usually contain dirty upper bits that will need to be cleaned. For example, we can perform addition without knowledge of the upper bits.
 
 ```solidity
   0x????????????????????????????????????????????????fffffffffffffffe // int64(-2)
@@ -476,7 +471,7 @@ function checkedAddInt64_1(int64 a, int64 b) public pure returns (int64 c) {
 ```
 
 If we remove the line that includes `c := signextend(7, c)` the overflow check will not function correctly.
-This is because Solidity does not take into account the fact that the variable is used in an assembly block, so the optimizer removes the bit cleaning operation, even if the Yul code includes it after the addition.
+This is because Solidity does not take into account the fact that the variable is used in an assembly block, and the optimizer removes the bit cleaning operation, even if the Yul code includes it after the addition.
 
 One thing to keep in mind is that since we are performing a 64-bit addition in 256 bits, we practically have access to the carry/overflow bits.
 If our computed value does not overflow, then it will fall within the correct bounds `type(int64).min <= c <= type(int64).max`.
@@ -500,7 +495,7 @@ function checkedAddInt64_2(int64 a, int64 b) public pure returns (int64 c) {
 
 There are a few ways to verify that the result in its 256-bit representation will fit into the expected data type.
 This is only true when all upper bits are the same.
-The most direct method, as just shown, involves checking the lower and upper bounds of the value.
+The most direct method, as previously shown, involves verifying both the lower and upper bounds.
 
 ```solidity
 /// @notice Check used in int64 addition for version >= 0.8.16.
@@ -509,7 +504,7 @@ function overflowInt64(int256 value) public pure returns (bool overflow) {
 }
 ```
 
-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.
+We can simplify the expression to a single comparison if we can 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).
 
@@ -551,8 +546,7 @@ $$
 }
 $$
 
-Note that the scales of the number ranges above do not accurately depict the magnitude of numbers that are representable with the different types and only serves as a visualization.
-We are able to represent twice as many numbers with only one additional bit. Yet, the uint256 domain has twice the number of bits compared to uint128.
+Note that the scales of the number ranges in the previous section do not accurately depict the magnitude of numbers that are representable with the different types and only serve as a visualization. We can represent twice as many numbers with only one additional bit, yet the uint256 domain has twice the number of bits compared to uint128.
 
 After subtracting `type(int128).min` (or adding $2^{127}$) and essentially shifting the domains to the right, we get the following, connected set of values.
 
@@ -600,7 +594,7 @@ function overflowInt64_3(int256 value) public pure returns (bool overflow) {
 }
 ```
 
-In Yul, the equivalent code would resemble the following.
+In Yul, the equivalent resembles the following.
 
 ```solidity
 function overflowInt64_3_yul(int256 value) public pure returns (bool overflow) {
@@ -624,7 +618,7 @@ function overflowInt64_4_yul(int256 value) public pure returns (bool overflow) {
 }
 ```
 
-Finally, a full example for detecting signed 64-bit integer overflow, implemented in Solidity can be seen below.
+Finally, a full example for detecting signed 64-bit integer overflow, implemented in Solidity can be seen below:
 
 ```solidity
 function checkedAddInt64_2(int64 a, int64 b) public pure returns (int64 c) {
@@ -648,8 +642,7 @@ One further optimization that we could perform is to add `-type(int64).min` inst
 
 ## Arithmetic checks for multiplication with sub-32-byte types
 
-If the product `c = a * b` can be calculated in 256 bits without the possibility of overflowing, we can once again verify whether the result can fit into the anticipated data type.
-This is also the way Solidity handles the check in versions 0.8.17 and later.
+When the product `c = a * b` can be calculated in 256 bits without the possibility of overflowing, we can verify whether the result can fit into the anticipated data type. This is also the way Solidity handles the check in versions 0.8.17 and later.
 
 ```solidity
 /// @notice version >= 0.8.17
@@ -668,8 +661,8 @@ function checkedMulInt64(int64 a, int64 b) public pure returns (int64 c) {
 
 However, if the maximum value of a product exceeds 256 bits, then this method won't be effective.
 This happens, for instance, when working with int192. The product `type(int192).min * type(int192).min` requires 192 + 192 = 384 bits to be stored, which exceeds the maximum of 256 bits.
-Overflow occurs in 256 bits, which loses information, and it won't be logical to check if the result fits into 192 bits.
-In this scenario, we can depend on the previous checks and, for example, attempt to reconstruct one of the multiplicands.
+Overflow occurs in 256 bits, causing a loss of information, and it won't be logical to check if the result fits into 192 bits.
+In this scenario, we can rely on the previous checks and, for example, attempt to reconstruct one of the multiplicands.
 
 ```solidity
 function checkedMulInt192_1(int192 a, int192 b) public pure returns (int192 c) {
@@ -682,10 +675,10 @@ function checkedMulInt192_1(int192 a, int192 b) public pure returns (int192 c) {
 }
 ```
 
-Once more, we must consider the two special circumstances:
+We must consider the two special circumstances:
 
 1. When one of the multiplicands is zero (`a == 0`), the other multiplicand cannot be retrieved. However, this case never results in overflow.
-2. Even if the multiplication is correct in 256 bits, the calculation overflows when only examining the least-significant 192 bits if the first multiplicand is minus one (`a = -1`) and the other multiplicand is the minimum value.
+2. Even if the multiplication is correct in 256 bits, the calculation overflows when only examining the least-significant 192 bits if the first multiplicand is negative one (`a = -1`) and the other multiplicand is the minimum value.
 
 An example might help explain the second case.
 
@@ -695,8 +688,8 @@ An example might help explain the second case.
 = 0x0000000000000000800000000000000000000000000000000000000000000000 // type(int192).min (when seen as a int192)
 ```
 
-A way to handle this is to always start by sign-extending or cleaning the result before attempting to reconstruct the other multiplicand.
-This then removes the need for checking the special condition.
+A method to address this issue is to always start by sign-extending or cleaning the result before attempting to reconstruct the other multiplicand.
+By doing so, it eliminates the need to check for the special condition.
 
 ```solidity
 /// @notice version >= 0.8.17
@@ -719,7 +712,6 @@ function checkedMulInt192_2(int192 a, int192 b) public pure returns (int192 c) {
 
 ## Conclusion
 
-In conclusion, this article has provided a comprehensive examination of arithmetic checks within the Ethereum Virtual Machine, delving into various Solidity opcodes and optimizations for assembly code. We have explored some of the intricacies of implementing arithmetic checks for both uint256 and int256 addition, subtraction, and multiplication, as well as for sub-32-byte types.
-Furthermore, we have highlighted some caveats to be aware of when working with assembly to avoid potential pitfalls.
+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.
 
-The purpose of this article is to deepen one's familiarity of low-level arithmetic, thereby improving the security of Solidity code by equipping developers to better assess and grasp the assumptions present in these operations. It is crucial to remember that custom low-level optimizations should be integrated only after rigorous manual analysis, fuzzing, and symbolic verification.
+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.

From 2a22697d02492b66c70f0017a2adccc79d5292b3 Mon Sep 17 00:00:00 2001
From: 0xphaze <0xphaze@gmail.com>
Date: Fri, 14 Apr 2023 14:26:11 +0100
Subject: [PATCH 10/11] Fix review

---
 learn_evm/arithmetic-checks.md | 14 ++++++++++----
 1 file changed, 10 insertions(+), 4 deletions(-)

diff --git a/learn_evm/arithmetic-checks.md b/learn_evm/arithmetic-checks.md
index 28c1132f..9ef1f6f9 100644
--- a/learn_evm/arithmetic-checks.md
+++ b/learn_evm/arithmetic-checks.md
@@ -1,10 +1,10 @@
 # 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.
+The Ethereum Virtual Machine (EVM) distinguishes itself from other virtual machines and computer systems through several unique aspects.
 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.
+Consequently, these safeguards must be incorporated within the machine's constraints.
 
 Starting with Solidity version 0.8.0 the compiler automatically includes over and underflow protection in all arithmetic operations.
 Prior to version 0.8.0, developers were required to implement these checks manually, often using a library known as [SafeMath](https://github.com/OpenZeppelin/openzeppelin-contracts/blob/master/contracts/utils/math/SafeMath.sol), originally developed by OpenZeppelin.
@@ -712,6 +712,12 @@ function checkedMulInt192_2(int192 a, int192 b) public pure returns (int192 c) {
 
 ## 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.
+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 explored:
 
-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.
+- the added complexity from handling signed over unsigned integers
+- the intricacies involved in managing sub 32-byte types
+- the significance of `signextend` and opcodes related to signed integers
+- the importance of bit-cleaning
+
+As the trend in Solidity smart contract development continues 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. Nevertheless, it is crucial to integrate custom low-level optimizations only after thorough manual analysis, fuzzing, and symbolic verification, and to document any non-obvious assumptions.

From 9993c5e8e2775036855d916c6eb21e60c50abeb6 Mon Sep 17 00:00:00 2001
From: 0xphaze <0xphaze@gmail.com>
Date: Fri, 14 Apr 2023 14:29:07 +0100
Subject: [PATCH 11/11] Fix review

---
 learn_evm/arithmetic-checks.md | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/learn_evm/arithmetic-checks.md b/learn_evm/arithmetic-checks.md
index 9ef1f6f9..f91e8e7c 100644
--- a/learn_evm/arithmetic-checks.md
+++ b/learn_evm/arithmetic-checks.md
@@ -720,4 +720,4 @@ We have explored:
 - the significance of `signextend` and opcodes related to signed integers
 - the importance of bit-cleaning
 
-As the trend in Solidity smart contract development continues 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. Nevertheless, it is crucial to integrate custom low-level optimizations only after thorough manual analysis, fuzzing, and symbolic verification, and to document any non-obvious assumptions.
+While low-level optimizations are attractive, they are also heavily error-prone. This article aims to deepen one's understanding of low-level arithmetic, to reduce these risks. Nevertheless, it is crucial to integrate custom low-level optimizations only after thorough manual analysis, automated testing, and to document any non-obvious assumptions.