Producing Positive Examples
Sometimes it is useful to produce examples of an expected behavior instead of
counterexamples that demonstrate unexpected behavior. You can do this by
writing a rule that uses satisfy statements instead of the assert
command. For
each satisfy
command in a rule, the Prover will produce an example that makes
the condition true, or report an error.
The purpose of the satisfy
statement is to produce examples that demonstrate
some execution of the code. Not every example is interesting — users
should inspect the example to ensure that it demonstrates the expected
behavior.
For example, we may be interested in showing that it is possible for someone to deposit some assets into a pool and then immediately withdraw them. The following rule demonstrates this scenario:
/// Demonstrate that one can fully withdraw deposited assets
rule uninterestingPossibleToFullyWithdraw(address sender, uint256 amount) {
// record initial balance
uint256 balanceBefore = _token0.balanceOf(sender);
// transfer `amount` tokens from `sender` to the pool
env eTransfer;
require eTransfer.msg.sender == sender;
_token0.transfer(eTransfer, currentContract, amount);
// mint and then immediately withdraw tokens for `sender`
env eMint;
require eMint.msg.sender == sender;
uint256 amountOut0 = mint(eMint,sender);
// withdraw tokens immediately after minting
env eBurn;
require eBurn.msg.sender == sender;
require eBurn.block.timestamp == eMint.block.timestamp;
burnSingle(eBurn, _token0, amountOut0, sender);
// demonstrate that it is possible that `sender`'s balance is unchanged
satisfy balanceBefore == _token0.balanceOf(sender);
}
Although the Prover produces an example (report) that satisfies
this rule, the example is rather uninteresting because the amount that is
minted and withdrawn is 0:
Of course minting and withdrawing 0 tokens leaves the sender’s balance
unchanged! We can add a require
statement to force the Prover to consider a
more interesting case:
/// Demonstrate that one can fully withdraw deposited assets
rule infeasiblePossibleToFullyWithdraw(address sender, uint256 amount) {
// force `amount` to be nonzero
require amount > 0;
// remainder of the rule is the same...
}
Again the Prover produces an example (report), but again it is an uninteresting one: the underlying token is minted for 999 LP tokens, which should be impossible. The problem is that the Prover is able to start the rule in an infeasible state.
We can remedy this by adding some additional setup assumptions (see the full
spec for details of the setup
function):
/// Demonstrate that one can fully withdraw deposited assets
rule possibleToFullyWithdraw(address sender, uint256 amount) {
// beginning of the rule is the same
setup(envMint);
// remainder of the rule is the same...
}
With this additional requirement, the Prover produces a satisfactory example.