Skip to content

Commit 9966773

Browse files
Create optimization_mode.md
1 parent 2a91e6c commit 9966773

File tree

1 file changed

+95
-0
lines changed

1 file changed

+95
-0
lines changed
Lines changed: 95 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,95 @@
1+
# Using optimization mode to find local maximums
2+
3+
**Table of contents:**
4+
5+
- [Introduction](#introduction)
6+
- [Optimizing with Echidna](#optimizing-with-echidna)
7+
8+
## Introduction
9+
10+
We will see how to perform function optimization using Echidna. This tutorial will require Echidna 2.0.5 or greater,
11+
so make sure you have update it before starting.
12+
13+
Optimization mode is a experimental feature that allows to define a special function which takes no arguments
14+
and returns a `int256`. Echidna will try find a sequence of transactions to maximize the value returned:
15+
16+
```solidity
17+
function echidna_opt_function() public view returns (int256) {
18+
// if it reverts, Echidna will assumed it returned type(int256).min
19+
return ..;
20+
}
21+
```
22+
23+
## Optimizing with Echidna
24+
25+
In this example, the target is the following smart contract (*[example/opt.sol](./example/opt.sol)*):
26+
27+
```solidity
28+
contract TestDutchAuctionOptimization {
29+
int256 maxPriceDifference;
30+
31+
function setMaxPriceDifference(
32+
uint256 startPrice,
33+
uint256 endPrice,
34+
uint256 startTime,
35+
uint256 endTime
36+
) public {
37+
if (endTime < (startTime + 900)) {
38+
revert();
39+
}
40+
if (startPrice <= endPrice) {
41+
revert();
42+
}
43+
uint256 numerator = (startPrice - endPrice) *
44+
(block.timestamp - startTime);
45+
uint256 denominator = endTime - startTime;
46+
uint256 stepDecrease = numerator / denominator;
47+
uint256 currentAuctionPrice = startPrice - stepDecrease;
48+
if (currentAuctionPrice < endPrice) {
49+
maxPriceDifference = int256(endPrice - currentAuctionPrice);
50+
}
51+
if (currentAuctionPrice > startPrice) {
52+
maxPriceDifference = int256(currentAuctionPrice - startPrice);
53+
}
54+
}
55+
56+
function echidna_opt_price_difference() public view returns (int256) {
57+
return maxPriceDifference;
58+
}
59+
}
60+
```
61+
62+
This small example forces Echidna to maximize certain price difference given some preconditions. If the preconditions are not
63+
met, the function will revert, without changing the actual value.
64+
65+
To run this example:
66+
67+
```
68+
$ echidna-test opt.sol --test-mode optimization --test-limit 100000 --seq-len 1 --corpus-dir corpus --shrink-limit 50000
69+
...
70+
echidna_opt_price_difference: max value: 1076841
71+
72+
Call sequence, shrinking (42912/50000):
73+
setMaxPriceDifference(1349752405,1155321,609,1524172858) Time delay: 603902 seconds Block delay: 21
74+
75+
```
76+
77+
The resulting max value is not unique, running in longer campaign will likely result in a larger value.
78+
79+
Regarding the command line, the optimization mode is enabled using `--test-mode optimization`. additionally, we included the following tweaks:
80+
81+
1. Use only one transaction (we know that the function is stateless)
82+
2. Use a large shrink limit in order to obtain a better value during the minimization of the complexity of the input.
83+
84+
Every time Echidna is executed using the corpus directory, the last input that produces the maximum value should be re-used from the `reproducers` directory:
85+
86+
```
87+
$ echidna-test opt.sol --test-mode optimization --test-limit 100000 --seq-len 1 --corpus-dir corpus --shrink-limit 50000
88+
Loaded total of 1 transactions from corpus/reproducers/
89+
Loaded total of 9 transactions from corpus/coverage/
90+
Analyzing contract: /home/g/Code/echidna/opt.sol:TestDutchAuctionOptimization
91+
echidna_opt_price_difference: max value: 1146878
92+
93+
Call sequence:
94+
setMaxPriceDifference(1538793592,1155321,609,1524172858) Time delay: 523701 seconds Block delay: 49387
95+
```

0 commit comments

Comments
 (0)