Skip to content

Commit

Permalink
feat: summary prop md and last tests
Browse files Browse the repository at this point in the history
  • Loading branch information
@simon-something
simon-something committed Jul 16, 2024
1 parent 8cde0c0 commit 0d0ca16
Show file tree
Hide file tree
Showing 5 changed files with 139 additions and 529 deletions.
46 changes: 32 additions & 14 deletions test/SUMMARY.md
View file
Original file line number Diff line number Diff line change
@@ -1,13 +1,19 @@
# Outline
# Tests Summary

There are 9 solidity files, totalling 939 sloc.

| filename | language | code | comment | blank | total |
| :---------------------------- | :------- | :--- | :------ | :---- | :---- |
| src/contracts/BCoWConst.sol | solidity | 4 | 10 | 2 | 16 |
| src/contracts/BCoWFactory.sol | solidity | 20 | 13 | 7 | 40 |
| src/contracts/BCoWPool.sol | solidity | 90 | 41 | 24 | 155 |
| src/contracts/BConst.sol | solidity | 23 | 29 | 9 | 61 |
| src/contracts/BFactory.sol | solidity | 44 | 17 | 11 | 72 |
| src/contracts/BMath.sol | solidity | 128 | 156 | 18 | 302 |
| src/contracts/BNum.sol | solidity | 133 | 40 | 28 | 201 |
| src/contracts/BPool.sol | solidity | 473 | 104 | 107 | 684 |
| src/contracts/BToken.sol | solidity | 24 | 27 | 7 | 58 |

There are 7 files to cover (B(cow)Const are contracts containing public protocol-wide constants):
BCoWFactory: deployer for cow pools
BCoWPool: adding signature validation to BPool
BFactory: deployer, approx 40sloc
BMath: contract wrapping math logic
BNum: contract wrapping arithmetic op
BPool: the main contract, roughly 400sloc
BToken: extends erc20

## Interdependencies
BCoWFactory deploys a bcowpool
Expand All @@ -16,15 +22,27 @@ Factory deploys a pool and can "collect" from the pool
Pool inherit btoken (which represents a LP) and bmath
Bmath uses bnum

## Approach
# Unit tests
Current coverage is XXX % for the 9 contracts, accross XXX tests. All tests are passing. Unit tests are writtent using the branched-tree technique and Bulloak as templating tool.

< TABLE >

# Integration tests

# Property tests
We identified 24 properties. We challenged these either in a long-running fuzzing campaign (targeting 23 of these in XXX runs) or via symbolic execution (for 8 properties).

## Fuzzing campaign

Echidna should be prioritized, then halmos should be particularly easy especially for the math libs, for which the implementations will be pretty similar.
We used echidna to test these 23 properties. In addition to these, another fuzzing campaign as been led against the mathematical contracts (BNum and BMath), insuring the operation properties were holding.

Then slither-mutate on the whole test base
Limitations/future improvements
Currently, the swap logic are tested against the swap in/out functions (and, in a similar way, liquidity management via the join/exit function). The combined equivalent (joinswapExternAmountIn, joinswapPoolAmountOut, etc) should be tested too.

Setup for protocol-wide *looks* pretty simple (using the factory) - tbc
## Formal verification: Symbolic Execution
We managed to test 10 properties out of the 23. Properties not tested are either not easily challenged with symbolic execution (statefullness needed) or limited by Halmos itself (hitting loops in the implementation for instance).

nb 14 means if token in == token out, people just give tokens to the pool, intended?
Additional properties from BNum were tested independently too (with severe limitations due to loop unrolling boundaries).


## Notes
Expand Down
74 changes: 31 additions & 43 deletions test/invariants/PROPERTIES.md
View file
Original file line number Diff line number Diff line change
@@ -1,36 +1,41 @@
| Properties | Type | Id | Halmos | Echidna |
| ------------------------------------------------------------------------------------------- | ------------------- | --- | ------ | ------- |
| BFactory should always be able to deploy new pools | Unit | 1 | [ ] | [x] |
| BFactory's blab should always be modifiable by the current blabs | Unit | 2 | [ ] | [x] |
| BFactory should always be able to transfer the BToken to the blab, if called by it | Unit | 3 | [ ] | [x] |
| the amount received can never be less than min amount out | Unit | 4 | [ ] | [x] |
| the amount spent can never be greater than max amount in | Unit | 5 | [ ] | [x] |
| swap fee can only be 0 (cow pool) | Valid state | 6 | [ ] | [x] |
| total weight can be up to 50e18 | Variable transition | 7 | [ ] | [x] |
| BToken increaseApproval should increase the approval of the address by the amount* | Variable transition | 8 | [ ] | [x] |
| BToken decreaseApproval should decrease the approval to max(old-amount, 0)* | Variable transition | 9 | [ ] | [x] |
| a pool can either be finalized or not finalized | Valid state | 10 | [ ] | [x] |
| a finalized pool cannot switch back to non-finalized | State transition | 11 | [ ] | [x] |
| a non-finalized pool can only be finalized when the controller calls finalize() | State transition | 12 | [ ] | [x] |
| an exact amount in should always earn the amount out calculated in bmath | High level | 13 | [ ] | [x] |
| an exact amount out is earned only if the amount in calculated in bmath is transfered | High level | 14 | [ ] | [x] |
| there can't be any amount out for a 0 amount in | High level | 15 | [ ] | [x] |
| the pool btoken can only be minted/burned in the join and exit operations | High level | 16 | [ ] | [x] |
| a direct token transfer can never reduce the underlying amount of a given token per BPT | High level | 17 | [ ] | [x] |
| the amount of underlying token when exiting should always be the amount calculated in bmath | High level | 18 | [ ] | [x] |
| a swap can only happen when the pool is finalized | High level | 19 | [ ] | [x] |
| bounding and unbounding token can only be done on a non-finalized pool, by the controller | High level | 20 | [ ] | [x] |
| there always should be between MIN_BOUND_TOKENS and MAX_BOUND_TOKENS bound in a pool | High level | 21 | [ ] | [x] |
| only the settler can commit a hash | High level | 22 | [ ] | [x] |
| when a hash has been commited, only this order can be settled | High level | 23 | [ ] | |
| BToken should not break the ToB ERC20 properties** | High level | 24 | [ ] | [x] |
| BFactory should always be able to deploy new pools | Unit | 1 | [x] | [x] |
| BFactory's blab should always be modifiable by the current blabs | Unit | 2 | [x] | [x] |
| BFactory should always be able to transfer the BToken to the blab, if called by it | Unit | 3 | [x] | [x] |
| the amount received can never be less than min amount out | Unit | 4 | :( | [x] |
| the amount spent can never be greater than max amount in | Unit | 5 | :( | [x] |
| swap fee can only be 0 (cow pool) | Valid state | 6 | [x] | [x] |
| total weight can be up to 50e18 | Variable transition | 7 | [x] | [x] |
| BToken increaseApproval should increase the approval of the address by the amount* | Variable transition | 8 | [x] | [x] |
| BToken decreaseApproval should decrease the approval to max(old-amount, 0)* | Variable transition | 9 | [x] | [x] |
| a pool can either be finalized or not finalized | Valid state | 10 | | [x] |
| a finalized pool cannot switch back to non-finalized | State transition | 11 | | [x] |
| a non-finalized pool can only be finalized when the controller calls finalize() | State transition | 12 | [x] | [x] |
| an exact amount in should always earn the amount out calculated in bmath | High level | 13 | :( | [x] |
| an exact amount out is earned only if the amount in calculated in bmath is transfered | High level | 14 | :( | [x] |
| there can't be any amount out for a 0 amount in | High level | 15 | :( | [x] |
| the pool btoken can only be minted/burned in the join and exit operations | High level | 16 | | [x] |
| a direct token transfer can never reduce the underlying amount of a given token per BPT | High level | 17 | :( | [x] |
| the amount of underlying token when exiting should always be the amount calculated in bmath | High level | 18 | :( | [x] |
| a swap can only happen when the pool is finalized | High level | 19 | | [x] |
| bounding and unbounding token can only be done on a non-finalized pool, by the controller | High level | 20 | [x] | [x] |
| there always should be between MIN_BOUND_TOKENS and MAX_BOUND_TOKENS bound in a pool | High level | 21 | | [x] |
| only the settler can commit a hash | High level | 22 | [x] | [x] |
| when a hash has been commited, only this order can be settled | High level | 23 | [ ] | [ ] |
| BToken should not break the ToB ERC20 properties** | High level | 24 | | [x] |

* Bundled with 24

** ERC20 properties
(https://github.com/crytic/properties?tab=readme-ov-file#erc20-tests)

# Unit for the math libs (BNum and BMath):
[ ] planed to implement and still to do
<br>[x] implemented and tested
<br>:( implemented but judged as incorrect (tool limitation, etc)
<br>empty not implemented and will not be (design, etc)

# Unit-test properties for the math libs (BNum and BMath):

btoi should always return the floor(a / BONE) == (a - a%BONE) / BONE
bfloor should always return (a - a % BONE)
Expand Down Expand Up @@ -79,23 +84,6 @@ bpow should be distributive over mult of the same base x^a * x^b == x^(a+b)
bpow should be distributive over mult of the same exp a^x * b^x == (a*b)^x
power of a power should mult the exp (x^a)^b == x^(a*b)


bpowApprox

calcOutGivenIn

calcOutGivenIn should be inv with calcInGivenOut

calcInGivenOut

calcPoolOutGivenSingleIn

calcPoolOutGivenSingleIn should be inv with calcSingleInGivenPoolOut

calcSingleInGivenPoolOut

calcSingleOutGivenPoolIn

calcSingleOutGivenPoolIn should be inv with calcPoolInGivenSingleOut

calcPoolInGivenSingleOut
calcSingleOutGivenPoolIn should be inv with calcPoolInGivenSingleOut
32 changes: 0 additions & 32 deletions test/invariants/symbolic/BMath.t.sol
View file

This file was deleted.

Loading

0 comments on commit 0d0ca16

Please sign in to comment.