docs: add naught coin exercise

program-analysis/echidna/exercises/exerciseX/NaughtCoin.sol

@@ -0,0 +1,43 @@
+// SPDX-License-Identifier: MIT
+pragma solidity ^0.8.0;
+
+import {ERC20} from "./level-utils/ERC20.sol";
+
+contract NaughtCoin is ERC20 {
+    // string public constant name = 'NaughtCoin';
+    // string public constant symbol = '0x0' -> 'NTC';
+    // uint public constant decimals = 18;
+    uint256 public timeLock = block.timestamp + 10 * 365 days;
+    uint256 public INITIAL_SUPPLY;
+    address public player;
+
+    // Note that the original symbol is changed from 0x0 to NTC
+    // This is caused by https://github.com/crytic/echidna/issues/909
+    constructor(address _player) ERC20("NaughtCoin", "NTC") {
+        player = _player;
+        INITIAL_SUPPLY = 1000000 * (10**uint256(decimals()));
+        // _totalSupply = INITIAL_SUPPLY;
+        // _balances[player] = INITIAL_SUPPLY;
+        _mint(player, INITIAL_SUPPLY);
+        emit Transfer(address(0), player, INITIAL_SUPPLY);
+    }
+
+    function transfer(address _to, uint256 _value)
+        public
+        override
+        lockTokens
+        returns (bool)
+    {
+        super.transfer(_to, _value);
+    }
+
+    // Prevent the initial owner from transferring tokens until the timelock has passed
+    modifier lockTokens() {
+        if (msg.sender == player) {
+            require(block.timestamp > timeLock);
+            _;
+        } else {
+            _;
+        }
+    }
+}

program-analysis/echidna/exercises/exerciseX/crytic/SolutionAdvanced.sol

@@ -0,0 +1,154 @@
+// SPDX-License-Identifier: MIT
+pragma solidity ^0.8.0;
+
+import {NaughtCoin} from "../NaughtCoin.sol";
+import {Setup} from "./SolutionSetupAdvanced.sol";
+
+contract ExternalTestAdvanced is Setup {
+    event AssertionFailed(uint256 amount);
+    event Log(bytes data);
+
+    function always_true() public pure {
+        assert(true);
+    }
+
+    function token_should_be_deployed() public view {
+        assert(address(token) != address(0));
+    }
+
+    function player_balance_is_equal_to_initial_supply() public view {
+        assert(token.balanceOf(address(player)) == token.INITIAL_SUPPLY());
+    }
+
+    function token_transfer_should_fail_before_timelock_period(uint256 amount)
+        public
+    {
+        amount = _between(amount, 0, token.INITIAL_SUPPLY());
+
+        // pre-conditions
+        uint256 currentTime = block.timestamp;
+        uint256 playerBalanceBefore = token.balanceOf(address(player));
+        uint256 bobBalanceBefore = token.balanceOf(address(bob));
+
+        if (currentTime < token.timeLock()) {
+            // action
+            try
+                player.proxy(
+                    address(token),
+                    abi.encodeWithSelector(
+                        token.transfer.selector,
+                        address(bob),
+                        amount
+                    )
+                )
+            returns (bool success, bytes memory returnData) {
+                emit Log(returnData);
+                assert(!success);
+            } catch {
+                /* reverted */
+            }
+
+            // post-conditions
+            assert(token.balanceOf(address(player)) == playerBalanceBefore);
+            assert(token.balanceOf(address(bob)) == bobBalanceBefore);
+        }
+    }
+
+    function player_approval_should_never_fail(address person, uint256 amount)
+        public
+    {
+        // pre-conditions
+        if (person != address(0)) {
+            // actions
+            try
+                player.proxy(
+                    address(token),
+                    abi.encodeWithSelector(
+                        token.approve.selector,
+                        person,
+                        amount
+                    )
+                )
+            {
+                /* success */
+            } catch {
+                assert(false);
+            }
+
+            // post-conditions
+            uint256 personAllowanceAfter = token.allowance(
+                address(player),
+                address(person)
+            );
+            assert(personAllowanceAfter == amount);
+        }
+    }
+
+    function transfer_from_should_fail_before_timelock_period(uint256 amount)
+        public
+    {
+        amount = _between(amount, 1, token.INITIAL_SUPPLY());
+
+        // pre-conditions
+        uint256 currentTime = block.timestamp;
+        uint256 playerBalanceBefore = token.balanceOf(address(player));
+        uint256 bobBalanceBefore = token.balanceOf(address(bob));
+
+        // we can set the allowance with the previous property
+        // player_approval_should_never_fail(address(bob), amount);
+
+        if (currentTime < token.timeLock()) {
+            // action
+            try
+                player.proxy(
+                    address(token),
+                    abi.encodeWithSelector(
+                        token.transferFrom.selector,
+                        address(player),
+                        address(bob),
+                        amount
+                    )
+                )
+            returns (bool success, bytes memory returnData) {
+                emit Log(returnData);
+                if (success) {
+                    emit AssertionFailed(amount);
+                }
+            } catch {
+                /* reverted */
+            }
+
+            // post-conditions
+            assert(token.balanceOf(address(player)) == playerBalanceBefore);
+            assert(token.balanceOf(address(bob)) == bobBalanceBefore);
+        }
+    }
+
+    function test_no_free_tokens_in_transfer_from(uint256 amount) public {
+        // pre-conditions
+        uint256 playerBalanceBefore = token.balanceOf(address(player));
+        uint256 bobBalanceBefore = token.balanceOf(address(bob));
+
+        // actions
+        try
+            player.proxy(
+                address(token),
+                abi.encodeWithSelector(
+                    token.transferFrom.selector,
+                    address(player),
+                    address(bob),
+                    amount
+                )
+            )
+        returns (bool success, bytes memory returnData) {
+            emit Log(returnData);
+            require(success);
+        } catch {}
+
+        // post-conditions
+        uint256 playerBalanceAfter = token.balanceOf(address(player));
+        uint256 bobBalanceAfter = token.balanceOf(address(bob));
+        assert(playerBalanceAfter == playerBalanceBefore - amount);
+        assert(bobBalanceAfter == bobBalanceBefore + amount);
+    }
+}

program-analysis/echidna/exercises/exerciseX/crytic/SolutionSetupAdvanced.sol

@@ -0,0 +1,33 @@
+// SPDX-License-Identifier: MIT
+pragma solidity ^0.8.0;
+
+import {NaughtCoin} from "../NaughtCoin.sol";
+
+contract User {
+    function proxy(address target, bytes memory data)
+        public
+        returns (bool success, bytes memory returnData)
+    {
+        return target.call(data);
+    }
+}
+
+contract Setup {
+    NaughtCoin token;
+    User player;
+    User bob;
+
+    constructor() {
+        player = new User();
+        bob = new User();
+        token = new NaughtCoin(address(player));
+    }
+
+    function _between(
+        uint256 amount,
+        uint256 low,
+        uint256 high
+    ) internal pure returns (uint256) {
+        return (low + (amount % (high - low + 1)));
+    }
+}

program-analysis/echidna/exercises/exerciseX/crytic/SolutionSimple.sol

@@ -0,0 +1,103 @@
+// SPDX-License-Identifier: MIT
+pragma solidity ^0.8.0;
+
+import {NaughtCoin} from "../NaughtCoin.sol";
+
+contract ExternalTest {
+    NaughtCoin public naughtCoin;
+    address player;
+    address bob;
+
+    event Player(address player);
+    event AssertionFailed(uint256 amount);
+
+    constructor() {
+        player = msg.sender;
+        // Bob is our second user, we need him to transfer tokens to someone.
+        // You can give him a random address like: 0x123456
+        bob = address(0x123456);
+        naughtCoin = new NaughtCoin(player);
+    }
+
+    function always_true() public pure {
+        assert(true);
+    }
+
+    function token_is_deployed() public {
+        assert(address(naughtCoin) != address(0));
+    }
+
+    function player_balance_is_equal_to_initial_supply() public {
+        uint256 currentTime = block.timestamp;
+        if (currentTime < naughtCoin.timeLock()) {
+            emit Player(player);
+            assert(naughtCoin.balanceOf(player) == naughtCoin.INITIAL_SUPPLY());
+        }
+    }
+
+    function transfer_should_fail_before_timelock_period(uint256 amount)
+        public
+    {
+        // pre-conditions
+        uint256 playerBalanceBefore = naughtCoin.balanceOf(player);
+        uint256 bobBalanceBefore = naughtCoin.balanceOf(bob);
+        uint256 currentTime = block.timestamp;
+        if (currentTime < naughtCoin.timeLock()) {
+            // actions
+            bool success1 = naughtCoin.transfer(bob, amount);
+            if (success1) {
+                emit AssertionFailed(amount);
+            }
+        }
+        // post-conditions
+        assert(
+            naughtCoin.balanceOf(player) == playerBalanceBefore &&
+                naughtCoin.balanceOf(bob) == bobBalanceBefore
+        );
+    }
+
+    function player_approval_should_not_fail(uint256 amount) public {
+        // actions
+        bool success1 = naughtCoin.approve(bob, amount);
+        // post-conditions
+        assert(success1);
+    }
+
+    function transfer_from_should_fail_before_timelock_period(uint256 amount)
+        public
+    {
+        // pre-conditions
+        uint256 playerBalanceBefore = naughtCoin.balanceOf(player);
+        uint256 bobBalanceBefore = naughtCoin.balanceOf(bob);
+        uint256 currentTime = block.timestamp;
+        if (currentTime <= naughtCoin.timeLock()) {
+            // actions
+            bool success1 = naughtCoin.transferFrom(player, bob, amount);
+            if (success1) {
+                emit AssertionFailed(amount);
+            }
+            // post-conditions
+            assert(
+                naughtCoin.balanceOf(player) == playerBalanceBefore &&
+                    naughtCoin.balanceOf(bob) == bobBalanceBefore
+            );
+        }
+    }
+
+    function no_free_tokens_in_transfer_from(uint256 amount) public {
+        // pre-conditions
+        uint256 playerBalanceBefore = naughtCoin.balanceOf(player);
+        uint256 bobBalanceBefore = naughtCoin.balanceOf(bob);
+        if (amount <= playerBalanceBefore) {
+            bool success1 = naughtCoin.transferFrom(player, bob, amount);
+            if (success1) {
+                // post-conditions
+                assert(
+                    naughtCoin.balanceOf(player) ==
+                        playerBalanceBefore - amount &&
+                        naughtCoin.balanceOf(bob) == bobBalanceBefore + amount
+                );
+            }
+        }
+    }
+}

program-analysis/echidna/exercises/exerciseX/crytic/config.yaml

@@ -0,0 +1,4 @@
+testMode: assertion
+corpusDir: "src/crytic/corpus"
+testLimit: 50000 
+multi-abi: true

program-analysis/echidna/exercises/exerciseX/level-utils/Context.sol

@@ -0,0 +1,24 @@
+// SPDX-License-Identifier: MIT
+// OpenZeppelin Contracts v4.4.1 (utils/Context.sol)
+
+pragma solidity ^0.8.0;
+
+/**
+ * @dev Provides information about the current execution context, including the
+ * sender of the transaction and its data. While these are generally available
+ * via msg.sender and msg.data, they should not be accessed in such a direct
+ * manner, since when dealing with meta-transactions the account sending and
+ * paying for execution may not be the actual sender (as far as an application
+ * is concerned).
+ *
+ * This contract is only required for intermediate, library-like contracts.
+ */
+abstract contract Context {
+    function _msgSender() internal view virtual returns (address) {
+        return msg.sender;
+    }
+
+    function _msgData() internal view virtual returns (bytes calldata) {
+        return msg.data;
+    }
+}