|
| 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