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.