Skip to content

Commit

Permalink
test: core libraries Echidna
Browse files Browse the repository at this point in the history
  • Loading branch information
thaixuandang committed Aug 13, 2024
1 parent 32ab672 commit 0ee7bc7
Show file tree
Hide file tree
Showing 14 changed files with 1,000 additions and 0 deletions.
60 changes: 60 additions & 0 deletions .github/workflows/core-libraries-echidna.yml
Original file line number Diff line number Diff line change
@@ -0,0 +1,60 @@
name: Core Libraries Fuzz Testing

on:
push:
branches:
- mainnet
- testnet
pull_request:

jobs:
echidna:
name: Echidna
runs-on: ubuntu-latest
strategy:
fail-fast: false
matrix:
testName:
- TickBitmapEchidnaTest
- TickMathEchidnaTest
- SqrtPriceMathEchidnaTest
- SwapMathEchidnaTest
- TickEchidnaTest
- TickOverflowSafetyEchidnaTest
- OracleEchidnaTest
- BitMathEchidnaTest
- LowGasSafeMathEchidnaTest
- UnsafeMathEchidnaTest
- FullMathEchidnaTest

steps:
- uses: actions/checkout@v4
with:
submodules: recursive

- name: Install Foundry
uses: foundry-rs/foundry-toolchain@v1
with:
version: nightly

- name: Set up Python 3.8
uses: actions/setup-python@v2
with:
python-version: 3.8

- name: Install pip3
run: |
python -m pip install --upgrade pip
- name: Install slither
run: |
pip3 install slither-analyzer
- name: Install echidna
run: |
sudo wget -O /tmp/echidna-test.tar.gz https://github.com/crytic/echidna/releases/download/v1.7.3/echidna-test-1.7.3-Ubuntu-18.04.tar.gz
sudo tar -xf /tmp/echidna-test.tar.gz -C /usr/bin
sudo chmod +x /usr/bin/echidna-test
- name: Run ${{ matrix.testName }}
run: echidna-test src/core/test/** --contract ${{ matrix.testName }} --config echidna.config.yml
74 changes: 74 additions & 0 deletions echidna.config.yml
Original file line number Diff line number Diff line change
@@ -0,0 +1,74 @@
#format can be "text" or "json" for different output (human or machine readable)
format: 'text'
#checkAsserts checks assertions
checkAsserts: true
#coverage controls coverage guided testing
coverage: false
# #psender is the sender for property transactions; by default intentionally
# #the same as contract deployer
# psender: "0x00a329c0648769a73afac7f9381e08fb43dbea70"
# #prefix is the prefix for Boolean functions that are properties to be checked
# prefix: "echidna_"
# #propMaxGas defines gas cost at which a property fails
# propMaxGas: 8000030
# #testMaxGas is a gas limit; does not cause failure, but terminates sequence
# testMaxGas: 8000030
# #maxGasprice is the maximum gas price
# maxGasprice: 100000000000
# #testLimit is the number of test sequences to run
# testLimit: 50000
# #stopOnFail makes echidna terminate as soon as any property fails and has been shrunk
# stopOnFail: false
# #estimateGas makes echidna perform analysis of maximum gas costs for functions (experimental)
# estimateGas: false
# #seqLen defines how many transactions are in a test sequence
# seqLen: 100
# #shrinkLimit determines how much effort is spent shrinking failing sequences
# shrinkLimit: 5000
# #contractAddr is the address of the contract itself
# contractAddr: "0x00a329c0648769a73afac7f9381e08fb43dbea72"
# #deployer is address of the contract deployer (who often is privileged owner, etc.)
# deployer: "0x00a329c0648769a73afac7f9381e08fb43dbea70"
# #sender is set of addresses transactions may originate from
# sender: ["0x10000", "0x20000", "0x00a329c0648769a73afac7f9381e08fb43dbea70"]
# #balanceAddr is default balance for addresses
# balanceAddr: 0xffffffff
# #balanceContract overrides balanceAddr for the contract address
# balanceContract: 0
# #solcArgs allows special args to solc
# solcArgs: ""
# #solcLibs is solc libraries
# solcLibs: []
# #cryticArgs allows special args to crytic
# cryticArgs: []
# #quiet produces (much) less verbose output
# quiet: false
# #initialize the blockchain with some data
# initialize: null
# #whether ot not to use the multi-abi mode of testing
# multi-abi: false
# #benchmarkMode enables benchmark mode
# benchmarkMode: false
# #timeout controls test timeout settings
# timeout: null
# #seed not defined by default, is the random seed
# #seed: 0
# #dictFreq controls how often to use echidna's internal dictionary vs random
# #values
# dictFreq: 0.40
# maxTimeDelay: 604800
# #maximum time between generated txs; default is one week
# maxBlockDelay: 60480
# #maximum number of blocks elapsed between generated txs; default is expected increment in one week
# # timeout:
# #campaign timeout (in seconds)
# # list of methods to filter
# filterFunctions: []
# # by default, blacklist methods in filterFunctions
# filterBlacklist: true
# #directory to save the corpus; by default is disabled
# corpusDir: null
# # constants for corpus mutations (for experimentation only)
# mutConsts: [100, 1, 1]
# # maximum value to send to payable functions
# maxValue: 100000000000000000000 # 100 eth
18 changes: 18 additions & 0 deletions src/core/test/BitMathEchidnaTest.sol
Original file line number Diff line number Diff line change
@@ -0,0 +1,18 @@
// SPDX-License-Identifier: UNLICENSED
pragma solidity =0.7.6;

import '../libraries/BitMath.sol';

contract BitMathEchidnaTest {
function mostSignificantBitInvariant(uint256 input) external pure {
uint8 msb = BitMath.mostSignificantBit(input);
assert(input >= (uint256(2)**msb));
assert(msb == 255 || input < uint256(2)**(msb + 1));
}

function leastSignificantBitInvariant(uint256 input) external pure {
uint8 lsb = BitMath.leastSignificantBit(input);
assert(input & (uint256(2)**lsb) != 0);
assert(input & (uint256(2)**lsb - 1) == 0);
}
}
67 changes: 67 additions & 0 deletions src/core/test/FullMathEchidnaTest.sol
Original file line number Diff line number Diff line change
@@ -0,0 +1,67 @@
// SPDX-License-Identifier: UNLICENSED
pragma solidity =0.7.6;

import '../libraries/FullMath.sol';

contract FullMathEchidnaTest {
function checkMulDivRounding(
uint256 x,
uint256 y,
uint256 d
) external pure {
require(d > 0);

uint256 ceiled = FullMath.mulDivRoundingUp(x, y, d);
uint256 floored = FullMath.mulDiv(x, y, d);

if (mulmod(x, y, d) > 0) {
assert(ceiled - floored == 1);
} else {
assert(ceiled == floored);
}
}

function checkMulDiv(
uint256 x,
uint256 y,
uint256 d
) external pure {
require(d > 0);
uint256 z = FullMath.mulDiv(x, y, d);
if (x == 0 || y == 0) {
assert(z == 0);
return;
}

// recompute x and y via mulDiv of the result of floor(x*y/d), should always be less than original inputs by < d
uint256 x2 = FullMath.mulDiv(z, d, y);
uint256 y2 = FullMath.mulDiv(z, d, x);
assert(x2 <= x);
assert(y2 <= y);

assert(x - x2 < d);
assert(y - y2 < d);
}

function checkMulDivRoundingUp(
uint256 x,
uint256 y,
uint256 d
) external pure {
require(d > 0);
uint256 z = FullMath.mulDivRoundingUp(x, y, d);
if (x == 0 || y == 0) {
assert(z == 0);
return;
}

// recompute x and y via mulDiv of the result of floor(x*y/d), should always be less than original inputs by < d
uint256 x2 = FullMath.mulDiv(z, d, y);
uint256 y2 = FullMath.mulDiv(z, d, x);
assert(x2 >= x);
assert(y2 >= y);

assert(x2 - x < d);
assert(y2 - y < d);
}
}
36 changes: 36 additions & 0 deletions src/core/test/LowGasSafeMathEchidnaTest.sol
Original file line number Diff line number Diff line change
@@ -0,0 +1,36 @@
// SPDX-License-Identifier: UNLICENSED
pragma solidity =0.7.6;

import '../libraries/LowGasSafeMath.sol';

contract LowGasSafeMathEchidnaTest {
function checkAdd(uint256 x, uint256 y) external pure {
uint256 z = LowGasSafeMath.add(x, y);
assert(z == x + y);
assert(z >= x && z >= y);
}

function checkSub(uint256 x, uint256 y) external pure {
uint256 z = LowGasSafeMath.sub(x, y);
assert(z == x - y);
assert(z <= x);
}

function checkMul(uint256 x, uint256 y) external pure {
uint256 z = LowGasSafeMath.mul(x, y);
assert(z == x * y);
assert(x == 0 || y == 0 || (z >= x && z >= y));
}

function checkAddi(int256 x, int256 y) external pure {
int256 z = LowGasSafeMath.add(x, y);
assert(z == x + y);
assert(y < 0 ? z < x : z >= x);
}

function checkSubi(int256 x, int256 y) external pure {
int256 z = LowGasSafeMath.sub(x, y);
assert(z == x - y);
assert(y < 0 ? z > x : z <= x);
}
}
137 changes: 137 additions & 0 deletions src/core/test/OracleEchidnaTest.sol
Original file line number Diff line number Diff line change
@@ -0,0 +1,137 @@
// SPDX-License-Identifier: UNLICENSED
pragma solidity =0.7.6;
pragma abicoder v2;

import './OracleTest.sol';

contract OracleEchidnaTest {
OracleTest private oracle;

bool private initialized;
uint32 private timePassed;

constructor() {
oracle = new OracleTest();
}

function initialize(
uint32 time,
int24 tick,
uint128 liquidity
) external {
oracle.initialize(OracleTest.InitializeParams({time: time, tick: tick, liquidity: liquidity}));
initialized = true;
}

function limitTimePassed(uint32 by) private {
require(timePassed + by >= timePassed);
timePassed += by;
}

function advanceTime(uint32 by) public {
limitTimePassed(by);
oracle.advanceTime(by);
}

// write an observation, then change tick and liquidity
function update(
uint32 advanceTimeBy,
int24 tick,
uint128 liquidity
) external {
limitTimePassed(advanceTimeBy);
oracle.update(OracleTest.UpdateParams({advanceTimeBy: advanceTimeBy, tick: tick, liquidity: liquidity}));
}

function grow(uint16 cardinality) external {
oracle.grow(cardinality);
}

function checkTimeWeightedResultAssertions(uint32 secondsAgo0, uint32 secondsAgo1) private view {
require(secondsAgo0 != secondsAgo1);
require(initialized);
// secondsAgo0 should be the larger one
if (secondsAgo0 < secondsAgo1) (secondsAgo0, secondsAgo1) = (secondsAgo1, secondsAgo0);

uint32 timeElapsed = secondsAgo0 - secondsAgo1;

uint32[] memory secondsAgos = new uint32[](2);
secondsAgos[0] = secondsAgo0;
secondsAgos[1] = secondsAgo1;

(int56[] memory tickCumulatives, uint160[] memory secondsPerLiquidityCumulativeX128s) =
oracle.observe(secondsAgos);
int56 timeWeightedTick = (tickCumulatives[1] - tickCumulatives[0]) / timeElapsed;
uint256 timeWeightedHarmonicMeanLiquidity =
(uint256(timeElapsed) * type(uint160).max) /
(uint256(secondsPerLiquidityCumulativeX128s[1] - secondsPerLiquidityCumulativeX128s[0]) << 32);
assert(timeWeightedHarmonicMeanLiquidity <= type(uint128).max);
assert(timeWeightedTick <= type(int24).max);
assert(timeWeightedTick >= type(int24).min);
}

function echidna_indexAlwaysLtCardinality() external view returns (bool) {
return oracle.index() < oracle.cardinality() || !initialized;
}

function echidna_AlwaysInitialized() external view returns (bool) {
(, , , bool isInitialized) = oracle.observations(0);
return oracle.cardinality() == 0 || isInitialized;
}

function echidna_cardinalityAlwaysLteNext() external view returns (bool) {
return oracle.cardinality() <= oracle.cardinalityNext();
}

function echidna_canAlwaysObserve0IfInitialized() external view returns (bool) {
if (!initialized) {
return true;
}
uint32[] memory arr = new uint32[](1);
arr[0] = 0;
(bool success, ) = address(oracle).staticcall(abi.encodeWithSelector(OracleTest.observe.selector, arr));
return success;
}

function checkTwoAdjacentObservationsTickCumulativeModTimeElapsedAlways0(uint16 index) external view {
uint16 cardinality = oracle.cardinality();
// check that the observations are initialized, and that the index is not the oldest observation
require(index < cardinality && index != (oracle.index() + 1) % cardinality);

(uint32 blockTimestamp0, int56 tickCumulative0, , bool initialized0) =
oracle.observations(index == 0 ? cardinality - 1 : index - 1);
(uint32 blockTimestamp1, int56 tickCumulative1, , bool initialized1) = oracle.observations(index);

require(initialized0);
require(initialized1);

uint32 timeElapsed = blockTimestamp1 - blockTimestamp0;
assert(timeElapsed > 0);
assert((tickCumulative1 - tickCumulative0) % timeElapsed == 0);
}

function checkTimeWeightedAveragesAlwaysFitsType(uint32 secondsAgo) external view {
require(initialized);
require(secondsAgo > 0);
uint32[] memory secondsAgos = new uint32[](2);
secondsAgos[0] = secondsAgo;
secondsAgos[1] = 0;
(int56[] memory tickCumulatives, uint160[] memory secondsPerLiquidityCumulativeX128s) =
oracle.observe(secondsAgos);

// compute the time weighted tick, rounded towards negative infinity
int56 numerator = tickCumulatives[1] - tickCumulatives[0];
int56 timeWeightedTick = numerator / int56(secondsAgo);
if (numerator < 0 && numerator % int56(secondsAgo) != 0) {
timeWeightedTick--;
}

// the time weighted averages fit in their respective accumulated types
assert(timeWeightedTick <= type(int24).max && timeWeightedTick >= type(int24).min);

uint256 timeWeightedHarmonicMeanLiquidity =
(uint256(secondsAgo) * type(uint160).max) /
(uint256(secondsPerLiquidityCumulativeX128s[1] - secondsPerLiquidityCumulativeX128s[0]) << 32);
assert(timeWeightedHarmonicMeanLiquidity <= type(uint128).max);
}
}
Loading

0 comments on commit 0ee7bc7

Please sign in to comment.