You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Copy file name to clipboardExpand all lines: program-analysis/echidna/Exercise-X.md
+9-9Lines changed: 9 additions & 9 deletions
Display the source diff
Display the rich diff
Original file line number
Diff line number
Diff line change
@@ -33,7 +33,7 @@ Depending on your framework, the `NaughtCoin` contract will be in the `src` fold
33
33
34
34
### Exercise goals
35
35
36
-
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:
36
+
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 describe 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:
37
37
38
38
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!
39
39
2. Create a simple `ExternalTest` contract with a proper state setup. Who is the player? Does he have the tokens?
@@ -102,13 +102,13 @@ If you are stuck at any point, feel free to look at the following hints. You can
102
102
103
103
import {NaughtCoin} from "src/NaughtCoin.sol";
104
104
105
-
contract ExternalTestSimple {
105
+
contract ExternalTest {
106
106
address player;
107
107
NaughtCoin public naughtCoin;
108
108
109
109
constructor() {
110
110
player = msg.sender;
111
-
naughtCoin = new NaughtCoin(player);
111
+
naughtCoin = new NaughtCoin(player);
112
112
}
113
113
}
114
114
```
@@ -143,7 +143,7 @@ If you are stuck at any point, feel free to look at the following hints. You can
143
143
<summary>2nd property</summary>
144
144
145
145
```
146
-
function sender_balance_is_equal_to_initial_supply() public {
146
+
function player_balance_is_equal_to_initial_supply() public {
@@ -156,7 +156,7 @@ If you are stuck at any point, feel free to look at the following hints. You can
156
156
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.
157
157
158
158
```
159
-
function sender_balance_is_equal_to_initial_supply() public {
159
+
function player_balance_is_equal_to_initial_supply() public {
160
160
// pre-conditions
161
161
uint256 currentTime = block.timestamp;
162
162
if (currentTime < naughtCoin.timeLock()) {
@@ -299,7 +299,7 @@ Run Echidna and check the corpus. Now we have fully covered this property.
299
299
300
300
The token transfer via `transferFrom` should fail if the current `block.timestamp < timelock` and/or spender has enough allowance.
301
301
302
-
This property in its base form is the same as the one with `transfer` function.
302
+
This property in its base form is the same as the one with the `transfer` function.
303
303
304
304
```
305
305
function transfer_from_should_fail_before_timelock_period(uint256 amount)
@@ -328,7 +328,7 @@ Run Echidna and see what you get. Echidna emits the `AssertionFailed` event with
328
328
329
329
The property `playerBalance == InitialSupply` still holds. You need to guide Echidna a little bit more for it to invalidate this property.
330
330
331
-
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.
331
+
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 ensure that it works properly.
332
332
333
333
Try to write a property for the `transferFrom` function.
334
334
@@ -380,7 +380,7 @@ Try to write a property for the `transferFrom` function.
380
380
381
381
#### Fixing a bug
382
382
383
-
Last step is to fix a bug that you have found. Try to fix it and re-run your properties. Check if they hold.
383
+
The last step is to fix a bug that you have found. Try to fix it and re-run your properties. Check if they hold.
384
384
385
385
<details>
386
386
<summary>Fixing a bug part 1</summary>
@@ -406,7 +406,7 @@ Add a `Player(address player)` event to your contract and emit it in your proper
406
406
407
407
The player's address is `0x0000...3000`. Echidna is making calls from multiple accounts. It was able to increase the allowance of an address `0x000...1000` and make a call to `transferFrom(player, 0x000...1000, amount)`. This is expected!
408
408
409
-
The `lockTokens` modifier does not prevent others from making transfers, only the player is constrained.
409
+
The `lockTokens` modifier does not prevent others from making transfers. Only the player is constrained.
410
410
411
411
```
412
412
// Prevent the initial owner from transferring tokens until the timelock has passed
0 commit comments