diff --git a/program-analysis/echidna/Exercise-X.md b/program-analysis/echidna/Exercise-X.md
new file mode 100644
index 00000000..f25256b3
--- /dev/null
+++ b/program-analysis/echidna/Exercise-X.md
@@ -0,0 +1,778 @@
+# Naught Coin - exercise
+
+This exercise is based on the [NaughtCoin - level 15 of the Ethernaut wargame](https://ethernaut.openzeppelin.com/level/15).
+
+The first four exercises were focused on internal testing. This level is an excellent introduction to [external testing with Echidna](https://github.com/crytic/building-secure-contracts/blob/master/program-analysis/echidna/common-testing-approaches.md#external-testing). Since the `NaughtCoin` contract expects a `player` to be the owner of the NaughtCoin tokens, it is a good idea to go with an external setup. The `EchidnaTest` contract will act as a player. Such a setup allows us to relatively easy describe user2user or user2contract interactions.
+
+### What you will learn
+
+By completing this exercise, you will:
+
+- Practice defining good invariants in plain English.
+- Understand different ways of creating an external testing setup.
+- Learn how to write simple properties and improve them over time.
+
+### Exercise setup
+
+The `NaughtCoin` contract has several dependencies. The directory structure that you should aim for looks like this:
+
+```
+src
+├── NaughtCoin.sol
+├── crytic
+│ ├── ExternalTest.sol
+│ └── config.yaml
+└── level-utils
+ ├── Context.sol
+ ├── ERC20.sol
+ ├── IERC20.sol
+ └── IERC20Metadata.sol
+```
+
+Depending on your framework, the `NaughtCoin` contract will be in the `src` folder (Foundry) or `contracts` (Hardhat). OpenZeppelin dependencies are in the `level-utils` folder, and all Echidna-related files are in the `crytic` folder.
+
+The config file used in this exercise looks as follows:
+
+```yaml
+testMode: assertion
+corpusDir: "src/crytic/corpus"
+testLimit: 50000
+multi-abi: true
+```
+
+The use of `assertions` is recommended for more flexibility when writing properties. The `multi-abi` allows Echidna to call any function, not just the properties you will write. Thanks to `multi-abi`, Echidna can figure out that it needs to call the `approve` or `increaseAllowance` before making a transfer. You should always collect a corpus, as it gives the necessary context to make sure that your properties are correct.
+
+Read more about the [multi-abi](https://github.com/crytic/building-secure-contracts/blob/master/program-analysis/echidna/using-multi-abi.md), [testing modes](https://github.com/crytic/building-secure-contracts/blob/master/program-analysis/echidna/testing-modes.md) and [corpus](https://github.com/crytic/building-secure-contracts/blob/master/program-analysis/echidna/collecting-a-corpus.md).
+
+### Exercise goals
+
+The main goal is to make the player's balance equal to `0`. You might know the answer right away. However, the purpose of this exercise is to define the whole system using properties in an iterative way. Start small and see what you can find. Expand over time. Here are some steps that you may take:
+
+1. Before writing any code, look at the NaughtCoin contract and think of 4-5 invariants that need to be held in this contract and write them down. The more, the better. You will be able to validate your assumptions about the system with Echidna. Be creative!
+2. Create a simple `ExternalTest` contract with a proper state setup. Who is the player? Does he have the tokens?
+3. Write a basic property to check if your code compiles, and Echidna is working as expected.
+4. Start converting your plain English properties into code. Easy to implement properties first.
+5. Remember, [the collected corpus is your friend](https://github.com/crytic/building-secure-contracts/blob/master/program-analysis/echidna/collecting-a-corpus.md). Run Echidna on every code change and look at the corpus.
+6. Refine your properties with better pre-conditions (a situation in which the property will be tested) and post-conditions (state checks after the action is performed). Everything that happens in between is an action.
+7. Good luck!
+
+### Solution steps
+
+If you are stuck at any point, feel free to look at the following hints. You can reveal them one by one without spoiling the final solution. Try to complete this exercise on your own!
+
+#### Example invariants in plain English
+
+
+ 1st invariant
+
+ The token should be deployed `(address(token) != address(0))`.
+
+
+
+
+ 2nd invariant
+
+ The player token balance should equal the initial supply if the current `block.timestamp < timelock`.
+
+
+
+
+ 3rd invariant
+
+ The token transfer should fail if the current `block.timestamp < timelock`.
+
+
+
+
+ 4th invariant
+
+ The `approve` function called by a `player` should never fail.
+
+
+
+
+ 5th invariant
+
+ The player should not be able to burn (lock) tokens before the `timelock`.
+
+
+
+
+ 6th invariant
+
+ The token transfer via `transferFrom` should fail if the current `block.timestamp < timelock` and/or spender has enough allowance.
+
+
+
+#### External testing setup
+
+
+ Example state setup
+
+ ```solidity
+ // SPDX-License-Identifier: MIT
+ pragma solidity ^0.8.0;
+
+ import {NaughtCoin} from "src/NaughtCoin.sol";
+
+ contract ExternalTestSimple {
+ address player;
+ NaughtCoin public naughtCoin;
+
+ constructor() {
+ player = msg.sender;
+ naughtCoin = new NaughtCoin(player);
+ }
+ }
+ ```
+
+
+
+
+ See if Echidna works as expected
+
+ ```solidity
+ function always_true() public pure {
+ assert(true);
+ }
+ ```
+
+
+
+#### Writing properties
+
+
+ 1st property
+
+ ```solidity
+ function token_is_deployed() public {
+ assert(address(naughtCoin) != address(0));
+ }
+ ```
+
+
+
+
+ 2nd property
+
+ ```solidity
+ function sender_balance_is_equal_to_initial_supply() public {
+ assert(naughtCoin.balanceOf(player) == naughtCoin.INITIAL_SUPPLY());
+ }
+ ```
+
+
+
+
+ 2nd property improved with pre-conditions
+
+ In plain English we have defined this invariant as The player token balance should equal the initial supply if the current `block.timestamp < timelock`. The second part of this sentence specifies exactly when this property should be tested.
+
+ ```solidity
+ function sender_balance_is_equal_to_initial_supply() public {
+ // pre-conditions
+ uint256 currentTime = block.timestamp;
+ if (currentTime < naughtCoin.timeLock()) {
+ // post-conditions
+ assert(naughtCoin.balanceOf(player) == naughtCoin.INITIAL_SUPPLY());
+ }
+ }
+ ```
+
+
+
+
+ 3rd property
+
+ The token transfer should fail if the current `block.timestamp < timelock`.
+
+ For this property we need to create a second user. We will try to transfer tokens from `player` to `bob`.
+
+ Add `bob` to your contract as `address bob;` and initialize his address in the constructor: `bob = address(0x123456)` to some random value.
+
+ For this property we also need to add an additional pre-condition. We need to check player's and bob's balance before transferring tokens, to have something to compare to in the post-conditions.
+
+ ```solidity
+ 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
+ naughtCoin.transfer(bob, amount);
+ }
+ // post-conditions
+ assert(
+ naughtCoin.balanceOf(player) == playerBalanceBefore &&
+ naughtCoin.balanceOf(bob) == bobBalanceBefore
+ );
+ }
+ ```
+
+Run Echidna and check the corpus. Is this a good property?
+
+
+
+
+ Improving the 3rd property
+
+ If you look at the corpus:
+
+ ```
+ 34 | r | function transfer_should_fail_before_timelock_period() public {
+ 35 | | // pre-conditions
+ 36 | r | uint256 playerBalanceBefore = naughtCoin.balanceOf(player);
+ 37 | r | uint256 bobBalanceBefore = naughtCoin.balanceOf(bob);
+ 38 | r | uint256 currentTime = block.timestamp;
+ 39 | r | if (currentTime < naughtCoin.timeLock()) {
+ 40 | | // actions
+ 41 | r | naughtCoin.transfer(bob, 100);
+ 42 | | }
+ 43 | | // post-conditions
+ 44 | | assert(
+ 45 | | naughtCoin.balanceOf(player) == playerBalanceBefore &&
+ 46 | | naughtCoin.balanceOf(bob) == bobBalanceBefore
+ 47 | | );
+ 48 | | }
+ 49 | | }
+ ```
+
+ You can see that the transfer reverted as expected. But... Our post-conditions weren't checked. If you have read the [ERC20 spec](https://github.com/ethereum/EIPs/blob/master/EIPS/eip-20.md), you will know that the `transfer` function returns a status `boolean`. In the case of success, we can emit a special `AssertionFailed` event that won't stop the execution of the function. This way, our post-conditions will be checked.
+
+- If `transfer` failed, that's okay. Keep going.
+- If `transfer` succeeded, we don't want that, emit the `AssertionFailed` and check post-conditions as usual.
+
+ Add the `event AssertionFailed(uint256 amount);` at the top of your contract.
+
+ ```solidity
+ 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
+ );
+ }
+
+ ```
+
+Run Echidna and check the corpus. Now we have fully covered this property.
+
+
+
+
+ 4th property
+
+ The `approve` function called by a `player` should not fail (even if the `player` currently does not have enough tokens). You can think of it as signing a blank cheque: "I as a player, allow Bob to spend the `amount` of my funds in one or more transactions".
+ According to the [OZ ERC20 standard](https://github.com/ethereum/EIPs/blob/master/EIPS/eip-20.md) this function should only fail if the `0` address is involved.
+
+ ```solidity
+ function player_approval_should_not_fail(uint256 amount) public {
+ // actions
+ bool success1 = naughtCoin.approve(bob, amount);
+ // post-conditions
+ assert(success1);
+ }
+ ```
+
+
+
+
+ 5th property
+
+ Player should not `burn` (lock) tokens before the `timeLock` period.
+ The `ERC20` used in this exercise does not implement a public `burn` functionality, so the actual burning (removing from the total supply) is not possible.
+
+ The only way a player could lock the tokens is by sending them to a non-existent address.
+
+ This property would be invalidated if any of our previous property were invalidated (which seems to not be the case at the moment). Let's leave this property for now and move on.
+
+
+
+
+ 6th property
+
+ The token transfer via `transferFrom` should fail if the current `block.timestamp < timelock` and/or spender has enough allowance.
+
+ This property in its base form is the same as the one with `transfer` function.
+
+ ```solidity
+ 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
+ );
+ }
+ }
+ ```
+
+Run Echidna and see what you get. Echidna emits the `AssertionFailed` event with the `amount` of `0`. It means that the `transferFrom` succeeded. If you look at the corpus, you will see that our post-conditions were invalidated. Echidna found a way to change player's balance.
+
+The property `playerBalance == InitialSupply` still holds. You need to guide Echidna a little bit more for it to invalidate this property.
+
+Try to get into the mindset of exploring the system you are auditing. Since, we have discovered something new about the system, a `transferFrom` function does not fail, as we initially expected, the next logical step would be to test this functionality and make sure that it works properly.
+
+Try to write a property for the `transferFrom` function.
+
+
+
+
+ 7th property
+
+ There are no free tokens created in the `transferFrom` function.
+
+ This property will check basic token arithmetics. The `transferFrom` works, so let's test that the user balances are updated correctly and reflect token transfers.
+
+ ```solidity
+ function no_free_tokens_in_transfer_from(uint256 amount) public {
+ // pre-conditions
+ uint256 playerBalanceBefore = naughtCoin.balanceOf(player);
+ uint256 bobBalanceBefore = naughtCoin.balanceOf(bob);
+
+ bool success1 = naughtCoin.transferFrom(player, bob, amount);
+ require(success1, "transferFrom failed");
+
+ // post-conditions
+ assert(
+ naughtCoin.balanceOf(player) == playerBalanceBefore - amount &&
+ naughtCoin.balanceOf(bob) == bobBalanceBefore + amount
+ );
+ }
+ ```
+
+ If you run Echidna now, the `playerBalance == initialSupply` property fails.
+ Echidna was able to find a call sequence to invalidate this property.
+
+ ```solidity
+ assertion in sender_balance_is_equal_to_initial_supply(): FAILED! with ErrorRevert
+ │ │
+ │ Call sequence: │
+ │ 1.increaseAllowance(0xa329c0648769a73afac7f9381e08fb43dbea72,11579208923731619542357098500868790785326998466564056403│
+ │ 9457584007913129639935) from: 0x0000000000000000000000000000000000030000 Time delay: 531977 seconds Block delay: │
+ │ 12066 │
+ │ 2.no_free_tokens_in_transfer_from(9) from: 0x0000000000000000000000000000000000010000 Time delay: 490448 seconds │
+ │ Block delay: 3753 │
+ │ 3.sender_balance_is_equal_to_initial_supply() from: 0x0000000000000000000000000000000000030000 Time delay: 1 seconds │
+ │ Block delay: 42595 │
+ │ Event sequence: │
+ │ Panic(1)
+ ```
+
+
+
+#### Fixing a bug
+
+Last step is to fix a bug that you have found. Try to fix it and re-run your properties. Check if they hold.
+
+
+ Fixing a bug part 1
+
+```solidity
+function transferFrom(
+ address _from,
+ address _to,
+ uint256 _amount
+ ) public override lockTokens returns (bool) {
+ super.transferFrom(_from, _to, _amount);
+ }
+```
+
+If you run Echidna, you will see that the properties still fail. Why is that?
+
+Add a `Player(address player)` event to your contract and emit it in your properties. Look at the call sequence.
+
+
+
+
+ Fixing a bug part 2
+
+The player's address is `0x30000`. Echidna is making calls from multiple accounts. It was able to increase the allowance of an address `0x10000` and make a call to `transferFrom(player, 0x10000, amount)`. This is expected!
+
+The `lockTokens` modifier does not prevent others from making transfers, only the player is constrained.
+
+```solidity
+// Prevent the initial owner from transferring tokens until the timelock has passed
+ modifier lockTokens() {
+ if (msg.sender == player) {
+ require(block.timestamp > timeLock);
+ _;
+ } else {
+ _;
+ }
+ }
+```
+
+To test this you can change the modifier to be:
+
+```solidity
+// Prevent the initial owner from transferring tokens until the timelock has passed
+ modifier lockTokens() {
+ if (msg.sender == player) {
+ require(block.timestamp > timeLock);
+ _;
+ } else {
+ require(block.timestamp > timeLock);
+ _;
+ }
+ }
+```
+
+No property fails now.
+
+
+
+## Advanced Setup
+
+This section will cover a more advanced setup for testing `NaughtCoin` `ERC20`.
+
+### Prerequisites
+
+Watch these two Echidna workshops in particular. The setup that we will use is explained in great detail there:
+
+- [Intro to AMM's invariants](https://www.youtube.com/live/n0RaKKVTGvA?feature=share)
+- [AMM fuzzing](https://www.youtube.com/live/OPDA0L9SeNI?feature=share)
+
+This is not required, but the first two workshops explain the concept of fuzzing in much greater detail than any tutorial could. If you haven't watched them, do it, it's worth it.
+
+- [Introduction to fuzzing](https://www.youtube.com/live/bhb_y80iF8w?feature=share)
+- [Fuzzing Arithmetics](https://www.youtube.com/live/9P7sqE6hILM?feature=share)
+
+### Why bother with a more complex setup?
+
+Apart from a better code separation (grouping the code into logically separated pieces), an advanced setup comes with a couple of benefits:
+
+- For complex codebases, you will often need to create some helper functions. Either to set the correct contract state ([This is what Justin does with the `_doApproval` function](https://www.youtube.com/watch?v=OPDA0L9SeNI&t=4237s)) or to remove code duplication in your properties. If you often repeat yourself and have the same logic in multiple properties, you can make your code [DRY](https://en.wikipedia.org/wiki/Don%27t_repeat_yourself) by moving some of that logic to the `Setup` contract.
+- Creating a `User` contract gives you more flexibility when defining how users interact with each other or with the contract. If there are groups of users with certain privileges, you can create contracts like `Admin`, `Moderator`, `PriviledgedUser` etc. and give them access to certain functionalities.
+
+### Exercise Setup
+
+After you watch Justin's intro to AMM's invariants, try to create your own `Setup` contract in a separate file, `Setup.sol`.
+
+The file structure remains the same as in the introductory section.
+
+### Exercise Goals
+
+1. Create the `Setup` contract with the appropriate state.
+2. Re-write your properties from the previous section using `proxies`.
+
+You can experiment with different ways of handling external calls. Instead of return value checks, you can use `try`/`catch`.
+
+### Step by step solution
+
+As before, you can reveal particular steps without spoiling the final solution.
+
+
+ Setup contract
+
+ This contract will be almost identical to what Justin did in the workshop.
+
+ ```solidity
+ // 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)));
+ }
+}
+ ```
+
+ In the introductory section we have used two addresses for `player` and `bob`. Now we are going to have two instances of the `User` contract: `player` and `bob`.
+
+
+
+
+ Making sure that Echidna works
+
+ ```solidity
+ // SPDX-License-Identifier: MIT
+pragma solidity ^0.8.0;
+
+import {NaughtCoin} from "src/NaughtCoin.sol";
+import {Setup} from "./Setup.sol";
+
+contract ExternalTestAdvanced is Setup {
+ function always_true() public pure {
+ assert(true);
+ }
+}
+ ```
+
+ Run Echidna and see if it starts.
+
+
+
+
+ The 1st property
+
+ The 1st property remains the same.
+
+ ```solidity
+ function token_should_be_deployed() public view {
+ assert(address(token) != address(0));
+ }
+ ```
+
+
+
+
+ The 2nd property
+
+ The 2nd property remains the same.
+
+ ```solidity
+ function player_balance_is_equal_to_initial_supply() public view {
+ assert(token.balanceOf(address(player)) == token.INITIAL_SUPPLY());
+ }
+ ```
+
+
+
+
+ The 3rd property
+
+ The 3rd property is slightly different. We have bounded the amount of tokens to be transferred between the value of `0` and the initial supply.
+
+ ```solidity
+ 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) {
+ // optional log to silent unused return param warning
+ // emit Log(returnData);
+ assert(!success);
+ } catch {
+ /* reverted */
+ }
+
+ // post-conditions
+ assert(token.balanceOf(address(player)) == playerBalanceBefore);
+ assert(token.balanceOf(address(bob)) == bobBalanceBefore);
+ }
+ }
+ ```
+
+
+
+
+ The 4th property
+
+ In the `try`/`catch` block we are making sure that the approval never reverts. This is not enough. You can enhance the post conditions to make sure that the `allowance` is updated.
+
+ ```solidity
+ function player_approval_should_never_fail(uint256 amount) public {
+ // actions
+ try
+ player.proxy(
+ address(token),
+ abi.encodeWithSelector(
+ token.approve.selector,
+ address(bob),
+ amount
+ )
+ )
+ {
+ /* success */
+ } catch {
+ assert(false);
+ }
+
+ // post-conditions
+ uint256 bobAllowanceAfter = token.allowance(
+ address(player),
+ address(bob)
+ );
+ assert(bobAllowanceAfter == amount);
+ }
+ ```
+
+ You can also improve this property by allowing Echidna to approve different addresses.
+
+ ```solidity
+ 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);
+ }
+ }
+ ```
+
+
+
+
+ The 6th property
+
+ We are intentionally skipping the 5th property again.
+ Echidna is able to invalidate the assertion inside the `try` block. The `transferFrom` function can be executed successfully. As you can see there is no need to set the `approval` manually. You can experiment with binding the `amount` to different values like `0` and `1`.
+
+ Notice that we are using the `AssertionFailed` event to make sure that our post-conditions are checked. If instead you would have done `assert(success)`, Echidna would not be able to find out that it can decrease player balance.
+
+ ```solidity
+ function transfer_from_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.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);
+ }
+ }
+ ```
+
+
+
+
+ The 7th property
+
+ Thanks to this property Echidna is able to invalidate other properties. In the `try`/`catch` block we only really care about the success case (since we know that `transferFrom` can succeed). We are ensuring that internal accounting works properly.
+
+ ```solidity
+ 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);
+ }
+ ```
+
+
diff --git a/program-analysis/echidna/exercises/exerciseX/NaughtCoin.sol b/program-analysis/echidna/exercises/exerciseX/NaughtCoin.sol
new file mode 100644
index 00000000..95a84d85
--- /dev/null
+++ b/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 {
+ _;
+ }
+ }
+}
diff --git a/program-analysis/echidna/exercises/exerciseX/crytic/SolutionAdvanced.sol b/program-analysis/echidna/exercises/exerciseX/crytic/SolutionAdvanced.sol
new file mode 100644
index 00000000..fe2731ea
--- /dev/null
+++ b/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);
+ }
+}
diff --git a/program-analysis/echidna/exercises/exerciseX/crytic/SolutionSetupAdvanced.sol b/program-analysis/echidna/exercises/exerciseX/crytic/SolutionSetupAdvanced.sol
new file mode 100644
index 00000000..c7c2b97c
--- /dev/null
+++ b/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)));
+ }
+}
diff --git a/program-analysis/echidna/exercises/exerciseX/crytic/SolutionSimple.sol b/program-analysis/echidna/exercises/exerciseX/crytic/SolutionSimple.sol
new file mode 100644
index 00000000..243a384a
--- /dev/null
+++ b/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
+ );
+ }
+ }
+ }
+}
diff --git a/program-analysis/echidna/exercises/exerciseX/crytic/config.yaml b/program-analysis/echidna/exercises/exerciseX/crytic/config.yaml
new file mode 100644
index 00000000..5b27ba1d
--- /dev/null
+++ b/program-analysis/echidna/exercises/exerciseX/crytic/config.yaml
@@ -0,0 +1,4 @@
+testMode: assertion
+corpusDir: "src/crytic/corpus"
+testLimit: 50000
+multi-abi: true
diff --git a/program-analysis/echidna/exercises/exerciseX/level-utils/Context.sol b/program-analysis/echidna/exercises/exerciseX/level-utils/Context.sol
new file mode 100644
index 00000000..f304065b
--- /dev/null
+++ b/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;
+ }
+}
diff --git a/program-analysis/echidna/exercises/exerciseX/level-utils/ERC20.sol b/program-analysis/echidna/exercises/exerciseX/level-utils/ERC20.sol
new file mode 100644
index 00000000..3739f93e
--- /dev/null
+++ b/program-analysis/echidna/exercises/exerciseX/level-utils/ERC20.sol
@@ -0,0 +1,429 @@
+// SPDX-License-Identifier: MIT
+// OpenZeppelin Contracts (last updated v4.8.0) (token/ERC20/ERC20.sol)
+
+pragma solidity ^0.8.0;
+
+import "./IERC20.sol";
+import "./IERC20Metadata.sol";
+import "./Context.sol";
+
+/**
+ * @dev Implementation of the {IERC20} interface.
+ *
+ * This implementation is agnostic to the way tokens are created. This means
+ * that a supply mechanism has to be added in a derived contract using {_mint}.
+ * For a generic mechanism see {ERC20PresetMinterPauser}.
+ *
+ * TIP: For a detailed writeup see our guide
+ * https://forum.openzeppelin.com/t/how-to-implement-erc20-supply-mechanisms/226[How
+ * to implement supply mechanisms].
+ *
+ * The default value of {decimals} is 18. To change this, you should override
+ * this function so it returns a different value.
+ *
+ * We have followed general OpenZeppelin Contracts guidelines: functions revert
+ * instead returning `false` on failure. This behavior is nonetheless
+ * conventional and does not conflict with the expectations of ERC20
+ * applications.
+ *
+ * Additionally, an {Approval} event is emitted on calls to {transferFrom}.
+ * This allows applications to reconstruct the allowance for all accounts just
+ * by listening to said events. Other implementations of the EIP may not emit
+ * these events, as it isn't required by the specification.
+ *
+ * Finally, the non-standard {decreaseAllowance} and {increaseAllowance}
+ * functions have been added to mitigate the well-known issues around setting
+ * allowances. See {IERC20-approve}.
+ */
+contract ERC20 is Context, IERC20, IERC20Metadata {
+ mapping(address => uint256) private _balances;
+
+ mapping(address => mapping(address => uint256)) private _allowances;
+
+ uint256 private _totalSupply;
+
+ string private _name;
+ string private _symbol;
+
+ /**
+ * @dev Sets the values for {name} and {symbol}.
+ *
+ * All two of these values are immutable: they can only be set once during
+ * construction.
+ */
+ constructor(string memory name_, string memory symbol_) {
+ _name = name_;
+ _symbol = symbol_;
+ }
+
+ /**
+ * @dev Returns the name of the token.
+ */
+ function name() public view virtual override returns (string memory) {
+ return _name;
+ }
+
+ /**
+ * @dev Returns the symbol of the token, usually a shorter version of the
+ * name.
+ */
+ function symbol() public view virtual override returns (string memory) {
+ return _symbol;
+ }
+
+ /**
+ * @dev Returns the number of decimals used to get its user representation.
+ * For example, if `decimals` equals `2`, a balance of `505` tokens should
+ * be displayed to a user as `5.05` (`505 / 10 ** 2`).
+ *
+ * Tokens usually opt for a value of 18, imitating the relationship between
+ * Ether and Wei. This is the default value returned by this function, unless
+ * it's overridden.
+ *
+ * NOTE: This information is only used for _display_ purposes: it in
+ * no way affects any of the arithmetic of the contract, including
+ * {IERC20-balanceOf} and {IERC20-transfer}.
+ */
+ function decimals() public view virtual override returns (uint8) {
+ return 18;
+ }
+
+ /**
+ * @dev See {IERC20-totalSupply}.
+ */
+ function totalSupply() public view virtual override returns (uint256) {
+ return _totalSupply;
+ }
+
+ /**
+ * @dev See {IERC20-balanceOf}.
+ */
+ function balanceOf(address account)
+ public
+ view
+ virtual
+ override
+ returns (uint256)
+ {
+ return _balances[account];
+ }
+
+ /**
+ * @dev See {IERC20-transfer}.
+ *
+ * Requirements:
+ *
+ * - `to` cannot be the zero address.
+ * - the caller must have a balance of at least `amount`.
+ */
+ function transfer(address to, uint256 amount)
+ public
+ virtual
+ override
+ returns (bool)
+ {
+ address owner = _msgSender();
+ _transfer(owner, to, amount);
+ return true;
+ }
+
+ /**
+ * @dev See {IERC20-allowance}.
+ */
+ function allowance(address owner, address spender)
+ public
+ view
+ virtual
+ override
+ returns (uint256)
+ {
+ return _allowances[owner][spender];
+ }
+
+ /**
+ * @dev See {IERC20-approve}.
+ *
+ * NOTE: If `amount` is the maximum `uint256`, the allowance is not updated on
+ * `transferFrom`. This is semantically equivalent to an infinite approval.
+ *
+ * Requirements:
+ *
+ * - `spender` cannot be the zero address.
+ */
+ function approve(address spender, uint256 amount)
+ public
+ virtual
+ override
+ returns (bool)
+ {
+ address owner = _msgSender();
+ _approve(owner, spender, amount);
+ return true;
+ }
+
+ /**
+ * @dev See {IERC20-transferFrom}.
+ *
+ * Emits an {Approval} event indicating the updated allowance. This is not
+ * required by the EIP. See the note at the beginning of {ERC20}.
+ *
+ * NOTE: Does not update the allowance if the current allowance
+ * is the maximum `uint256`.
+ *
+ * Requirements:
+ *
+ * - `from` and `to` cannot be the zero address.
+ * - `from` must have a balance of at least `amount`.
+ * - the caller must have allowance for ``from``'s tokens of at least
+ * `amount`.
+ */
+ function transferFrom(
+ address from,
+ address to,
+ uint256 amount
+ ) public virtual override returns (bool) {
+ address spender = _msgSender();
+ _spendAllowance(from, spender, amount);
+ _transfer(from, to, amount);
+ return true;
+ }
+
+ /**
+ * @dev Atomically increases the allowance granted to `spender` by the caller.
+ *
+ * This is an alternative to {approve} that can be used as a mitigation for
+ * problems described in {IERC20-approve}.
+ *
+ * Emits an {Approval} event indicating the updated allowance.
+ *
+ * Requirements:
+ *
+ * - `spender` cannot be the zero address.
+ */
+ function increaseAllowance(address spender, uint256 addedValue)
+ public
+ virtual
+ returns (bool)
+ {
+ address owner = _msgSender();
+ _approve(owner, spender, allowance(owner, spender) + addedValue);
+ return true;
+ }
+
+ /**
+ * @dev Atomically decreases the allowance granted to `spender` by the caller.
+ *
+ * This is an alternative to {approve} that can be used as a mitigation for
+ * problems described in {IERC20-approve}.
+ *
+ * Emits an {Approval} event indicating the updated allowance.
+ *
+ * Requirements:
+ *
+ * - `spender` cannot be the zero address.
+ * - `spender` must have allowance for the caller of at least
+ * `subtractedValue`.
+ */
+ function decreaseAllowance(address spender, uint256 subtractedValue)
+ public
+ virtual
+ returns (bool)
+ {
+ address owner = _msgSender();
+ uint256 currentAllowance = allowance(owner, spender);
+ require(
+ currentAllowance >= subtractedValue,
+ "ERC20: decreased allowance below zero"
+ );
+ unchecked {
+ _approve(owner, spender, currentAllowance - subtractedValue);
+ }
+
+ return true;
+ }
+
+ /**
+ * @dev Moves `amount` of tokens from `from` to `to`.
+ *
+ * This internal function is equivalent to {transfer}, and can be used to
+ * e.g. implement automatic token fees, slashing mechanisms, etc.
+ *
+ * Emits a {Transfer} event.
+ *
+ * Requirements:
+ *
+ * - `from` cannot be the zero address.
+ * - `to` cannot be the zero address.
+ * - `from` must have a balance of at least `amount`.
+ */
+ function _transfer(
+ address from,
+ address to,
+ uint256 amount
+ ) internal virtual {
+ require(from != address(0), "ERC20: transfer from the zero address");
+ require(to != address(0), "ERC20: transfer to the zero address");
+
+ _beforeTokenTransfer(from, to, amount);
+
+ uint256 fromBalance = _balances[from];
+ require(
+ fromBalance >= amount,
+ "ERC20: transfer amount exceeds balance"
+ );
+ unchecked {
+ _balances[from] = fromBalance - amount;
+ // Overflow not possible: the sum of all balances is capped by totalSupply, and the sum is preserved by
+ // decrementing then incrementing.
+ _balances[to] += amount;
+ }
+
+ emit Transfer(from, to, amount);
+
+ _afterTokenTransfer(from, to, amount);
+ }
+
+ /**
+ * @dev Creates `amount` tokens and assigns them to `account`, increasing
+ * the total supply.
+ *
+ * Emits a {Transfer} event with `from` set to the zero address.
+ *
+ * Requirements:
+ *
+ * - `account` cannot be the zero address.
+ */
+ function _mint(address account, uint256 amount) internal virtual {
+ require(account != address(0), "ERC20: mint to the zero address");
+
+ _beforeTokenTransfer(address(0), account, amount);
+
+ _totalSupply += amount;
+ unchecked {
+ // Overflow not possible: balance + amount is at most totalSupply + amount, which is checked above.
+ _balances[account] += amount;
+ }
+ emit Transfer(address(0), account, amount);
+
+ _afterTokenTransfer(address(0), account, amount);
+ }
+
+ /**
+ * @dev Destroys `amount` tokens from `account`, reducing the
+ * total supply.
+ *
+ * Emits a {Transfer} event with `to` set to the zero address.
+ *
+ * Requirements:
+ *
+ * - `account` cannot be the zero address.
+ * - `account` must have at least `amount` tokens.
+ */
+ function _burn(address account, uint256 amount) internal virtual {
+ require(account != address(0), "ERC20: burn from the zero address");
+
+ _beforeTokenTransfer(account, address(0), amount);
+
+ uint256 accountBalance = _balances[account];
+ require(accountBalance >= amount, "ERC20: burn amount exceeds balance");
+ unchecked {
+ _balances[account] = accountBalance - amount;
+ // Overflow not possible: amount <= accountBalance <= totalSupply.
+ _totalSupply -= amount;
+ }
+
+ emit Transfer(account, address(0), amount);
+
+ _afterTokenTransfer(account, address(0), amount);
+ }
+
+ /**
+ * @dev Sets `amount` as the allowance of `spender` over the `owner` s tokens.
+ *
+ * This internal function is equivalent to `approve`, and can be used to
+ * e.g. set automatic allowances for certain subsystems, etc.
+ *
+ * Emits an {Approval} event.
+ *
+ * Requirements:
+ *
+ * - `owner` cannot be the zero address.
+ * - `spender` cannot be the zero address.
+ */
+ function _approve(
+ address owner,
+ address spender,
+ uint256 amount
+ ) internal virtual {
+ require(owner != address(0), "ERC20: approve from the zero address");
+ require(spender != address(0), "ERC20: approve to the zero address");
+
+ _allowances[owner][spender] = amount;
+ emit Approval(owner, spender, amount);
+ }
+
+ /**
+ * @dev Updates `owner` s allowance for `spender` based on spent `amount`.
+ *
+ * Does not update the allowance amount in case of infinite allowance.
+ * Revert if not enough allowance is available.
+ *
+ * Might emit an {Approval} event.
+ */
+ function _spendAllowance(
+ address owner,
+ address spender,
+ uint256 amount
+ ) internal virtual {
+ uint256 currentAllowance = allowance(owner, spender);
+ if (currentAllowance != type(uint256).max) {
+ require(
+ currentAllowance >= amount,
+ "ERC20: insufficient allowance"
+ );
+ unchecked {
+ _approve(owner, spender, currentAllowance - amount);
+ }
+ }
+ }
+
+ /**
+ * @dev Hook that is called before any transfer of tokens. This includes
+ * minting and burning.
+ *
+ * Calling conditions:
+ *
+ * - when `from` and `to` are both non-zero, `amount` of ``from``'s tokens
+ * will be transferred to `to`.
+ * - when `from` is zero, `amount` tokens will be minted for `to`.
+ * - when `to` is zero, `amount` of ``from``'s tokens will be burned.
+ * - `from` and `to` are never both zero.
+ *
+ * To learn more about hooks, head to xref:ROOT:extending-contracts.adoc#using-hooks[Using Hooks].
+ */
+ function _beforeTokenTransfer(
+ address from,
+ address to,
+ uint256 amount
+ ) internal virtual {}
+
+ /**
+ * @dev Hook that is called after any transfer of tokens. This includes
+ * minting and burning.
+ *
+ * Calling conditions:
+ *
+ * - when `from` and `to` are both non-zero, `amount` of ``from``'s tokens
+ * has been transferred to `to`.
+ * - when `from` is zero, `amount` tokens have been minted for `to`.
+ * - when `to` is zero, `amount` of ``from``'s tokens have been burned.
+ * - `from` and `to` are never both zero.
+ *
+ * To learn more about hooks, head to xref:ROOT:extending-contracts.adoc#using-hooks[Using Hooks].
+ */
+ function _afterTokenTransfer(
+ address from,
+ address to,
+ uint256 amount
+ ) internal virtual {}
+}
diff --git a/program-analysis/echidna/exercises/exerciseX/level-utils/IERC20.sol b/program-analysis/echidna/exercises/exerciseX/level-utils/IERC20.sol
new file mode 100644
index 00000000..82a00e48
--- /dev/null
+++ b/program-analysis/echidna/exercises/exerciseX/level-utils/IERC20.sol
@@ -0,0 +1,89 @@
+// SPDX-License-Identifier: MIT
+// OpenZeppelin Contracts (last updated v4.6.0) (token/ERC20/IERC20.sol)
+
+pragma solidity ^0.8.0;
+
+/**
+ * @dev Interface of the ERC20 standard as defined in the EIP.
+ */
+interface IERC20 {
+ /**
+ * @dev Emitted when `value` tokens are moved from one account (`from`) to
+ * another (`to`).
+ *
+ * Note that `value` may be zero.
+ */
+ event Transfer(address indexed from, address indexed to, uint256 value);
+
+ /**
+ * @dev Emitted when the allowance of a `spender` for an `owner` is set by
+ * a call to {approve}. `value` is the new allowance.
+ */
+ event Approval(
+ address indexed owner,
+ address indexed spender,
+ uint256 value
+ );
+
+ /**
+ * @dev Returns the amount of tokens in existence.
+ */
+ function totalSupply() external view returns (uint256);
+
+ /**
+ * @dev Returns the amount of tokens owned by `account`.
+ */
+ function balanceOf(address account) external view returns (uint256);
+
+ /**
+ * @dev Moves `amount` tokens from the caller's account to `to`.
+ *
+ * Returns a boolean value indicating whether the operation succeeded.
+ *
+ * Emits a {Transfer} event.
+ */
+ function transfer(address to, uint256 amount) external returns (bool);
+
+ /**
+ * @dev Returns the remaining number of tokens that `spender` will be
+ * allowed to spend on behalf of `owner` through {transferFrom}. This is
+ * zero by default.
+ *
+ * This value changes when {approve} or {transferFrom} are called.
+ */
+ function allowance(address owner, address spender)
+ external
+ view
+ returns (uint256);
+
+ /**
+ * @dev Sets `amount` as the allowance of `spender` over the caller's tokens.
+ *
+ * Returns a boolean value indicating whether the operation succeeded.
+ *
+ * IMPORTANT: Beware that changing an allowance with this method brings the risk
+ * that someone may use both the old and the new allowance by unfortunate
+ * transaction ordering. One possible solution to mitigate this race
+ * condition is to first reduce the spender's allowance to 0 and set the
+ * desired value afterwards:
+ * https://github.com/ethereum/EIPs/issues/20#issuecomment-263524729
+ *
+ * Emits an {Approval} event.
+ */
+ function approve(address spender, uint256 amount) external returns (bool);
+
+ /**
+ * @dev Moves `amount` tokens from `from` to `to` using the
+ * allowance mechanism. `amount` is then deducted from the caller's
+ * allowance.
+ *
+ * Returns a boolean value indicating whether the operation succeeded.
+ *
+ * Emits a {Transfer} event.
+ */
+ function transferFrom(
+ address from,
+ address to,
+ uint256 amount
+ ) external returns (bool);
+}
diff --git a/program-analysis/echidna/exercises/exerciseX/level-utils/IERC20Metadata.sol b/program-analysis/echidna/exercises/exerciseX/level-utils/IERC20Metadata.sol
new file mode 100644
index 00000000..982bc39e
--- /dev/null
+++ b/program-analysis/echidna/exercises/exerciseX/level-utils/IERC20Metadata.sol
@@ -0,0 +1,28 @@
+// SPDX-License-Identifier: MIT
+// OpenZeppelin Contracts v4.4.1 (token/ERC20/extensions/IERC20Metadata.sol)
+
+pragma solidity ^0.8.0;
+
+import "./IERC20.sol";
+
+/**
+ * @dev Interface for the optional metadata functions from the ERC20 standard.
+ *
+ * _Available since v4.1._
+ */
+interface IERC20Metadata is IERC20 {
+ /**
+ * @dev Returns the name of the token.
+ */
+ function name() external view returns (string memory);
+
+ /**
+ * @dev Returns the symbol of the token.
+ */
+ function symbol() external view returns (string memory);
+
+ /**
+ * @dev Returns the decimals places of the token.
+ */
+ function decimals() external view returns (uint8);
+}