Closed newcodepusher closed 3 years ago
I think you can do this as follows:
/// if_succeeds {:msg "balance changed"} let baseToken := old(IERC20(Pool(pool).GetPairForToken(token1, token2, startDate))) in old(baseToken.balanceOf(address(this))) + old(baseToken.balanceOf(address(msg.sender))) == baseToken.balanceOf(address(this));
Note that the right-hand-side of the let binding is wrapped into old()
. Its basically a syntactic requirement of let. Let me know if this doesn't work for you!
it works thanks, it was not obvious to me, maybe you should add this to the documentation
I added a section on let-bindings and old expression here:
https://app.gitbook.com/@mythx/s/scribble/language/keywords#let-bindigns-and-old-expressions
If you feel that this is insufficient to clear confusion for this use-case, please feel free to re-open the issue with any suggestions. Thank you!
I want to shorten the entry for example this
/// if_succeeds {:msg "balance changed"} old(IERC20(Pool(pool).GetPairForToken(token1, token2, startDate)).balanceOf(address(this))) + old(IERC20(Pool(pool).GetPairForToken(token1, token2, startDate)).balanceOf(address(msg.sender))) == IERC20(Pool(pool).GetPairForToken(token1, token2, startDate)).balanceOf(address(this));
to/// if_succeeds {:msg "balance changed"} let baseToken := Pool(pool).GetPairForToken(token1, token2, startDate) in old(IERC20(baseToken).balanceOf(address(this))) + old(IERC20(baseToken).balanceOf(address(msg.sender))) == IERC20(baseToken).balanceOf(address(this));
Reducing and reusing the code is very important. For example, I ran into a gas limit when deploying a contract and cannot cover the entire contract with tests