Extends and improves tracking sums pattern #252
Conversation
docs/user-guide/patterns/sums.rst
Outdated
|
|
||
| .. cvlinclude:: ../../../Examples/DEFI/ERC20/certora/specs/ERC20Fixed.spec | ||
| :lines: 98-106, 115-116 | ||
| :caption: :clink:`Total supply is sum of balances</DEFI/ERC20/certora/specs/ERC20Fixed.spec>` |
There was a problem hiding this comment.
I would add a caption link with specific lines: https://github.com/Certora/Examples/blob/225e3b16f5728d975c4d52a47f5ffa2f877c1c16/DEFI/ERC20/certora/specs/ERC20Fixed.spec#L96-L116
There was a problem hiding this comment.
You're right. The problem is that the :clink: command doesn't support lines yet. I'll add it to my TODO list for that component.
I prefer to keep using :clink: since it is more robust with respect to changes in the repository.
docs/user-guide/patterns/sums.rst
Outdated
| :caption: :clink:`Total supply is sum of balances</DEFI/ERC20/certora/specs/ERC20Fixed.spec>` | ||
|
|
||
| Once this invariant is proved, we can require properties like the one in | ||
| :cvl:`sumOfTwo` above. |
There was a problem hiding this comment.
I think it's not clear why one should come back to sumOfTwo if they have a better invariant totalSupplyIsSumOfBalances.
docs/user-guide/patterns/sums.rst
Outdated
| The preferred solution to tracking sums is using a hook and a ghost, as shown below. | ||
|
|
||
| .. cvlinclude:: ../../../Examples/DEFI/ERC20/certora/specs/ERC20Fixed.spec | ||
| :lines: 98-106, 115-116 |
There was a problem hiding this comment.
Sload hook is missing form the example on doc page. not everyone will go to github to copy the whole solution if they don't know about it
docs/user-guide/patterns/sums.rst
Outdated
| .. code-block:: cvl | ||
|
|
||
| invariant sumOfTwo(address a, address b) | ||
| (a != b) => (balanceOf(a) + balanceOf(b) <= to_mathint(totalSupply())); |
There was a problem hiding this comment.
wasn't it a part of a hook in a previous solution we had? Why did you remove it?
docs/user-guide/patterns/sums.rst
Outdated
|
|
||
| Trying to verify the sum of two balances | ||
| ---------------------------------------- | ||
| Often one needs a invariant like :cvl:`sumOfTwo` below: |
There was a problem hiding this comment.
"a invariant"? I think it should be "an" or maybe even "the' because we talk about specific invariant. But definitely not "a"
I think the transition from the first paragraph to this part isn't clear. We need to check the sum of ALL balances, but now we downgraded our property to the sum of only two balances.
Maybe something like: "First of all, let's start with a simpler property: sum of two balances is less than or equal to totalSupply(). It will also improve our understanding of how the prover works and finds counter-examples."
shoham-certora
force-pushed
the
shoham/tracking-sums
branch
from
8b2e75f to
3fe7f72
Compare
|
Looks good now. Should we wait for one more review? |
@RedLikeRosesss , I also think it looks better now, but I'd like to ask @nd-certora about the |
Added motivation, and specific CVL specs examples.
shoham-certora
force-pushed
the
shoham/tracking-sums
branch
from
3bbc0e5 to
11d4f37
Compare
Documentation link