Fairpool is a DEX for personal tokens. Create your own token & receive royalties from trading volume. Increase volume by offering dividends / selling content for your token. Subscribe to our Telegram / Twitter to get notified about updates.
- ⚒ Experimented with formal methods for proving the correctness of the Fairpool smart contract.
- ⚒ Decided on the upgradeability strategy.
- ⚒ Explored the use of ECDSA signatures for controlling the Fairpool shares.
Formal methods for proving the smart contract correctness
While writing the tests for the Fairpool contract, we’ve arrived at a difficult-to-implement test.
The test asserts that the long-term distribution of the earnings to the holders must be uniformly proportional to their shares. In other words: if everyone has the same amount of shares, then their total sum of earnings over multiple distributions must be equal. If someone has 2x the shares of everyone else, then their total sum of earnings over multiple distributions must be 2x greater then for everyone else.
However, since the Fairpool contract distributes the shares randomly, and only 256 holders receive earnings during a single distribution, it’s impossible to write an automated test. This is a fundamental limitation: on one hand, the test is supposed to always pass, but on the other hand, it’s definitely possible (and valid) that the test observes a non-uniform distribution on a single run with a fixed limited number of distributions.
This problem can’t be solved with regular tests, because they work with fixed values. Even dynamic tests can’t help here, because a dynamically generated list of transactions still has a fixed length, and so it’s possible for distribution to become non-uniform (for that specific fixed list of transactions).
To solve this problem we turned to formal methods.
Formal methods allow proving that a specific property holds “in the limit” — meaning that when the number of distributions goes to infinity, the total sum becomes proportional to the number of shares.
We’re currently working on proving that property for the Fairpool contract to ensure that the distribution is actually fair.
Next week’s focus
- ⚒ Develop Fairpool.
Fairpool is a DEX for personal tokens. Create your own token & receive royalties from trading volume. Increase volume by offering dividends / selling content for your token. If you want to get notified about updates to our products, please follow our Telegram & Twitter.
Any questions? Reach out to us:
Anchor Podcasts: @FairpoolDEX
$FAIR token: Uniswap + PancakeSwap