Merge pull request #308 from crytic/echidna-0.8

montyly · web-flow · commit 35e43f53d95a · 2023-07-11T14:31:46.000+02:00
Use 0.8.0 for echidna exercises
diff --git a/.github/workflows/echidna.yml b/.github/workflows/echidna.yml
@@ -167,7 +167,7 @@ jobs:
           contract: ${{ matrix.contract }}
           config: ${{ matrix.config }}
           output-file: ${{ matrix.files }}.out
-          solc-version: ${{ matrix.solc-version || '0.5.11' }}
+          solc-version: ${{ matrix.solc-version || '0.8.0' }}
           echidna-workdir: ${{ matrix.workdir }}
           echidna-version: edge
           crytic-args: ${{ matrix.crytic-args || '' }}
diff --git a/not-so-smart-contracts/cairo/README.md b/not-so-smart-contracts/cairo/README.md
@@ -30,4 +30,4 @@ Each _Not So Smart Contract_ consists of a standard set of information:
 
 These examples are developed and maintained by [Trail of Bits](https://www.trailofbits.com/).
 
-If you have any questions, issues, or wish to learn more, join the #ethereum channel on the [Empire Hacking Slack](https://empireslacking.herokuapp.com/) or [contact us](https://www.trailofbits.com/contact/) directly.
+If you have any questions, issues, or wish to learn more, join the #ethereum channel on the [Empire Hacking Slack](https://slack.empirehacking.nyc/) or [contact us](https://www.trailofbits.com/contact/) directly.
diff --git a/program-analysis/echidna/basic/assertion-checking.md b/program-analysis/echidna/basic/assertion-checking.md
@@ -11,7 +11,7 @@
 
 ## Introduction
 
-In this short tutorial, we will demonstrate how to use Echidna to check assertions in smart contracts. For this example, be sure to use Solidity 0.7.x or older. If you run them with Solidity 0.8.x, the test will never fail.
+In this short tutorial, we will demonstrate how to use Echidna to check assertions in smart contracts.
 
 ## Write an Assertion
 
@@ -23,7 +23,9 @@ contract Incrementor {
 
     function inc(uint256 val) public returns (uint256) {
         uint256 tmp = counter;
-        counter += val;
+        unchecked {
+            counter += val;
+        }
         // tmp <= counter
         return (counter - tmp);
     }
@@ -38,7 +40,9 @@ contract Incrementor {
 
     function inc(uint256 val) public returns (uint256) {
         uint256 tmp = counter;
-        counter += val;
+        unchecked {
+            counter += val;
+        }
         assert(tmp <= counter);
         return (counter - tmp);
     }
@@ -55,7 +59,9 @@ contract Incrementor {
 
     function inc(uint256 val) public returns (uint256) {
         uint256 tmp = counter;
-        counter += val;
+        unchecked {
+            counter += val;
+        }
         if (tmp > counter) {
             emit AssertionFailed(counter);
         }
diff --git a/program-analysis/echidna/example/assert.sol b/program-analysis/echidna/example/assert.sol
@@ -1,12 +1,14 @@
 // SPDX-License-Identifier: AGPL-3.0
-pragma solidity ^0.5.0;
+pragma solidity ^0.8.0;
 
 contract Incrementor {
     uint256 private counter = 2 ** 200;
 
     function inc(uint256 val) public returns (uint256) {
         uint256 tmp = counter;
-        counter += val;
+        unchecked {
+            counter += val;
+        }
         assert(tmp <= counter);
         return (counter - tmp);
     }
diff --git a/program-analysis/echidna/example/gas.sol b/program-analysis/echidna/example/gas.sol
@@ -1,5 +1,5 @@
 // SPDX-License-Identifier: AGPL-3.0
-pragma solidity ^0.5.0;
+pragma solidity ^0.8.0;
 
 contract C {
     uint256 state;
diff --git a/program-analysis/echidna/example/multi.sol b/program-analysis/echidna/example/multi.sol
@@ -1,5 +1,5 @@
 // SPDX-License-Identifier: AGPL-3.0
-pragma solidity ^0.5.0;
+pragma solidity ^0.8.0;
 
 contract C {
     bool state1 = false;
diff --git a/program-analysis/echidna/example/pushpop.sol b/program-analysis/echidna/example/pushpop.sol
@@ -1,5 +1,5 @@
 // SPDX-License-Identifier: AGPL-3.0
-pragma solidity ^0.5.0;
+pragma solidity ^0.8.0;
 
 contract C {
     address[] addrs;
diff --git a/program-analysis/echidna/example/testtoken.sol b/program-analysis/echidna/example/testtoken.sol
@@ -1,5 +1,5 @@
 // SPDX-License-Identifier: AGPL-3.0
-pragma solidity ^0.5.0;
+pragma solidity ^0.8.0;
 
 import "./token.sol";
 
diff --git a/program-analysis/echidna/example/token.sol b/program-analysis/echidna/example/token.sol
@@ -1,5 +1,5 @@
 // SPDX-License-Identifier: AGPL-3.0
-pragma solidity ^0.5.0;
+pragma solidity ^0.8.0;
 
 contract Token {
     mapping(address => uint256) public balances;
diff --git a/program-analysis/echidna/exercises/Exercise-1.md b/program-analysis/echidna/exercises/Exercise-1.md
@@ -15,7 +15,7 @@ Join the team on Slack at: https://slack.empirehacking.nyc/ #ethereum
 We will test the following contract _[token.sol](https://github.com/crytic/building-secure-contracts/tree/master/program-analysis/echidna/exercises/exercise1/token.sol)_:
 
 ```solidity
-pragma solidity ^0.5.0;
+pragma solidity ^0.8.0;
 
 contract Ownable {
     address public owner = msg.sender;
@@ -67,13 +67,13 @@ contract Token is Ownable, Pausable {
 The skeleton for this exercise is (_[template.sol](https://github.com/crytic/building-secure-contracts/tree/master/program-analysis/echidna/exercises/exercise1/template.sol)_):
 
 ````solidity
-pragma solidity ^0.5.0;
+pragma solidity ^0.8.0;
 
 import "./token.sol";
 
 /// @dev Run the template with
 ///      ```
-///      solc-select use 0.5.0
+///      solc-select use 0.8.0
 ///      echidna program-analysis/echidna/exercises/exercise1/template.sol
 ///      ```
 contract TestToken is Token {
diff --git a/program-analysis/echidna/exercises/Exercise-2.md b/program-analysis/echidna/exercises/Exercise-2.md
@@ -17,7 +17,7 @@ Join the team on Slack at: https://slack.empirehacking.nyc/ #ethereum
 We will test the following contract, _[token.sol](https://github.com/crytic/building-secure-contracts/tree/master/program-analysis/echidna/exercises/exercise2/token.sol)_:
 
 ```solidity
-pragma solidity ^0.5.0;
+pragma solidity ^0.8.0;
 
 contract Ownable {
     address public owner = msg.sender;
@@ -74,7 +74,7 @@ contract Token is Ownable, Pausable {
 The skeleton for this exercise is (_[template.sol](https://github.com/crytic/building-secure-contracts/tree/master/program-analysis/echidna/exercises/exercise2/template.sol)_):
 
 ````solidity
-pragma solidity ^0.5.0;
+pragma solidity ^0.8.0;
 
 import "./token.sol";
 
diff --git a/program-analysis/echidna/exercises/Exercise-3.md b/program-analysis/echidna/exercises/Exercise-3.md
@@ -17,7 +17,7 @@ Join the team on Slack at: https://slack.empirehacking.nyc/ #ethereum
 We will test the following contract _[token.sol](https://github.com/crytic/building-secure-contracts/tree/master/program-analysis/echidna/exercises/exercise3/token.sol)_:
 
 ```solidity
-pragma solidity ^0.5.0;
+pragma solidity ^0.8.0;
 
 /// @notice The issues from exercises 1 and 2 are fixed.
 
@@ -66,7 +66,7 @@ contract Token is Ownable, Pausable {
 Consider the following extension of the token (_[mintable.sol](https://github.com/crytic/building-secure-contracts/tree/master/program-analysis/echidna/exercises/exercise3/mintable.sol)_):
 
 ```solidity
-pragma solidity ^0.5.0;
+pragma solidity ^0.8.0;
 
 import "./token.sol";
 
@@ -98,7 +98,7 @@ The [version of token.sol](https://github.com/crytic/building-secure-contracts/t
 The skeleton for this exercise is [template.sol](https://github.com/crytic/building-secure-contracts/tree/master/program-analysis/echidna/exercises/exercise3/template.sol):
 
 ````solidity
-pragma solidity ^0.5.0;
+pragma solidity ^0.8.0;
 
 import "./mintable.sol";
 
diff --git a/program-analysis/echidna/exercises/Exercise-4.md b/program-analysis/echidna/exercises/Exercise-4.md
@@ -17,7 +17,7 @@ Join the team on Slack at: https://slack.empirehacking.nyc/ #ethereum
 We will test the following contract, _[token.sol](https://github.com/crytic/building-secure-contracts/tree/master/program-analysis/echidna/exercises/exercise4/token.sol)_:
 
 ```solidity
-pragma solidity ^0.5.0;
+pragma solidity ^0.8.0;
 
 contract Ownable {
     address public owner = msg.sender;
@@ -79,13 +79,13 @@ This exercise is similar to the [first one](Exercise-1.md), but it uses assertio
 The skeleton for this exercise is ([template.sol](https://github.com/crytic/building-secure-contracts/tree/master/program-analysis/echidna/exercises/exercise4/template.sol)):
 
 ````solidity
-pragma solidity ^0.5.0;
+pragma solidity ^0.8.0;
 
 import "./token.sol";
 
 /// @dev Run the template with
 ///      ```
-///      solc-select use 0.5.0
+///      solc-select use 0.8.0
 ///      echidna program-analysis/echidna/exercises/exercise4/template.sol --contract TestToken --test-mode assertion
 ///      ```
 contract TestToken is Token {
diff --git a/program-analysis/echidna/exercises/exercise1/solution.sol b/program-analysis/echidna/exercises/exercise1/solution.sol
@@ -1,11 +1,11 @@
 // SPDX-License-Identifier: AGPL-3.0
-pragma solidity ^0.5.0;
+pragma solidity ^0.8.0;
 
 import "./token.sol";
 
 /// @dev Run the solution with
 ///      ```
-///      solc-select use 0.5.0
+///      solc-select use 0.8.0
 ///      echidna program-analysis/echidna/exercises/exercise1/solution.sol
 ///      ```
 contract TestToken is Token {
diff --git a/program-analysis/echidna/exercises/exercise1/template.sol b/program-analysis/echidna/exercises/exercise1/template.sol
@@ -1,11 +1,11 @@
 // SPDX-License-Identifier: AGPL-3.0
-pragma solidity ^0.5.0;
+pragma solidity ^0.8.0;
 
 import "./token.sol";
 
 /// @dev Run the template with
 ///      ```
-///      solc-select use 0.5.0
+///      solc-select use 0.8.0
 ///      echidna program-analysis/echidna/exercises/exercise1/template.sol
 ///      ```
 contract TestToken is Token {
diff --git a/program-analysis/echidna/exercises/exercise1/token.sol b/program-analysis/echidna/exercises/exercise1/token.sol
@@ -1,5 +1,5 @@
 // SPDX-License-Identifier: AGPL-3.0
-pragma solidity ^0.5.0;
+pragma solidity ^0.8.0;
 
 contract Ownable {
     address public owner = msg.sender;
@@ -35,7 +35,10 @@ contract Token is Ownable, Pausable {
     mapping(address => uint256) public balances;
 
     function transfer(address to, uint256 value) public whenNotPaused {
-        balances[msg.sender] -= value;
-        balances[to] += value;
+        // unchecked to save gas
+        unchecked {
+            balances[msg.sender] -= value;
+            balances[to] += value;
+        }
     }
 }
diff --git a/program-analysis/echidna/exercises/exercise2/solution.sol b/program-analysis/echidna/exercises/exercise2/solution.sol
@@ -1,11 +1,11 @@
 // SPDX-License-Identifier: AGPL-3.0
-pragma solidity ^0.5.0;
+pragma solidity ^0.8.0;
 
 import "./token.sol";
 
 /// @dev Run the solution with
 ///      ```
-///      solc-select use 0.5.0
+///      solc-select use 0.8.0
 ///      echidna program-analysis/echidna/exercises/exercise1/solution.sol
 ///      ```
 contract TestToken is Token {
diff --git a/program-analysis/echidna/exercises/exercise2/template.sol b/program-analysis/echidna/exercises/exercise2/template.sol
@@ -1,11 +1,11 @@
 // SPDX-License-Identifier: AGPL-3.0
-pragma solidity ^0.5.0;
+pragma solidity ^0.8.0;
 
 import "./token.sol";
 
 /// @dev Run the template with
 ///      ```
-///      solc-select use 0.5.0
+///      solc-select use 0.8.0
 ///      echidna program-analysis/echidna/exercises/exercise2/template.sol
 ///      ```
 contract TestToken is Token {
diff --git a/program-analysis/echidna/exercises/exercise2/token.sol b/program-analysis/echidna/exercises/exercise2/token.sol
@@ -1,5 +1,5 @@
 // SPDX-License-Identifier: AGPL-3.0
-pragma solidity ^0.5.0;
+pragma solidity ^0.8.0;
 
 contract Ownable {
     address public owner = msg.sender;
diff --git a/program-analysis/echidna/exercises/exercise3/mintable.sol b/program-analysis/echidna/exercises/exercise3/mintable.sol
@@ -1,5 +1,5 @@
 // SPDX-License-Identifier: AGPL-3.0
-pragma solidity ^0.5.0;
+pragma solidity ^0.8.0;
 
 import "./token.sol";
 
diff --git a/program-analysis/echidna/exercises/exercise3/solution.sol b/program-analysis/echidna/exercises/exercise3/solution.sol
@@ -1,11 +1,11 @@
 // SPDX-License-Identifier: AGPL-3.0
-pragma solidity ^0.5.0;
+pragma solidity ^0.8.0;
 
 import "./mintable.sol";
 
 /// @dev Run the solution with
 ///      ```
-///      solc-select use 0.5.0
+///      solc-select use 0.8.0
 ///      echidna program-analysis/echidna/exercises/exercise3/solution.sol --contract TestToken
 ///      ```
 contract TestToken is MintableToken {
diff --git a/program-analysis/echidna/exercises/exercise3/template.sol b/program-analysis/echidna/exercises/exercise3/template.sol
@@ -1,11 +1,11 @@
 // SPDX-License-Identifier: AGPL-3.0
-pragma solidity ^0.5.0;
+pragma solidity ^0.8.0;
 
 import "./mintable.sol";
 
 /// @dev Run the template with
 ///      ```
-///      solc-select use 0.5.0
+///      solc-select use 0.8.0
 ///      echidna program-analysis/echidna/exercises/exercise3/template.sol --contract TestToken
 ///      ```
 contract TestToken is MintableToken {
diff --git a/program-analysis/echidna/exercises/exercise3/token.sol b/program-analysis/echidna/exercises/exercise3/token.sol
@@ -1,5 +1,5 @@
 // SPDX-License-Identifier: AGPL-3.0
-pragma solidity ^0.5.0;
+pragma solidity ^0.8.0;
 
 /// @notice The issues from exercise 1 and 2 are fixed.
 
diff --git a/program-analysis/echidna/exercises/exercise4/solution.sol b/program-analysis/echidna/exercises/exercise4/solution.sol
@@ -1,15 +1,15 @@
 // SPDX-License-Identifier: AGPL-3.0
-pragma solidity ^0.5.0;
+pragma solidity ^0.8.0;
 
 import "./token.sol";
 
 /// @dev Run the solution with
 ///      ```
-///      solc-select use 0.5.0
+///      solc-select use 0.8.0
 ///      echidna program-analysis/echidna/exercises/exercise4/solution.sol --contract TestToken --test-mode assertion
 ///      ```
 contract TestToken is Token {
-    function transfer(address to, uint256 value) public {
+    function transfer(address to, uint256 value) public override {
         uint256 oldBalanceFrom = balances[msg.sender];
         uint256 oldBalanceTo = balances[to];
 
diff --git a/program-analysis/echidna/exercises/exercise4/template.sol b/program-analysis/echidna/exercises/exercise4/template.sol
@@ -1,11 +1,11 @@
 // SPDX-License-Identifier: AGPL-3.0
-pragma solidity ^0.5.0;
+pragma solidity ^0.8.0;
 
 import "./token.sol";
 
 /// @dev Run the template with
 ///      ```
-///      solc-select use 0.5.0
+///      solc-select use 0.8.0
 ///      echidna program-analysis/echidna/exercises/exercise4/template.sol --contract TestToken --test-mode assertion
 ///      ```
 ///      or by providing a config
diff --git a/program-analysis/echidna/exercises/exercise4/token.sol b/program-analysis/echidna/exercises/exercise4/token.sol
@@ -1,5 +1,5 @@
 // SPDX-License-Identifier: AGPL-3.0
-pragma solidity ^0.5.0;
+pragma solidity ^0.8.0;
 
 contract Ownable {
     address public owner = msg.sender;
@@ -38,8 +38,11 @@ contract Pausable is Ownable {
 contract Token is Ownable, Pausable {
     mapping(address => uint256) public balances;
 
-    function transfer(address to, uint256 value) public whenNotPaused {
-        balances[msg.sender] -= value;
-        balances[to] += value;
+    function transfer(address to, uint256 value) public virtual whenNotPaused {
+        // unchecked to save gas
+        unchecked {
+            balances[msg.sender] -= value;
+            balances[to] += value;
+        }
     }
 }
diff --git a/program-analysis/echidna/introduction/installation.md b/program-analysis/echidna/introduction/installation.md
@@ -22,7 +22,7 @@ _The last command runs the eth-security-toolbox in a Docker container, which wil
 Inside Docker, execute the following commands:
 
 ```bash
-solc-select use 0.5.11
+solc-select use 0.8.0
 cd /home/training
 ```
 
@@ -32,4 +32,4 @@ You can find the latest released binary here:
 
 [https://github.com/crytic/echidna/releases/latest](https://github.com/crytic/echidna/releases/latest)
 
-It's essential to use the correct solc version to ensure that these exercises work as expected. We have tested them using version 0.5.11.
+It's essential to use the correct solc version to ensure that these exercises work as expected. We have tested them using version 0.8.0.

Original file line number	Diff line number	Diff line change
`@@ -30,4 +30,4 @@ Each _Not So Smart Contract_ consists of a standard set of information:`
`30`	`30`
`31`	`31`	`These examples are developed and maintained by [Trail of Bits](https://www.trailofbits.com/).`
`32`	`32`
`33`		`-If you have any questions, issues, or wish to learn more, join the #ethereum channel on the [Empire Hacking Slack](https://empireslacking.herokuapp.com/) or [contact us](https://www.trailofbits.com/contact/) directly.`
	`33`	`+If you have any questions, issues, or wish to learn more, join the #ethereum channel on the [Empire Hacking Slack](https://slack.empirehacking.nyc/) or [contact us](https://www.trailofbits.com/contact/) directly.`