Require Invariants: Proving inter-dependent invariants

TherequireInvariant statements can be used to establish crucial conditions that must persist throughout the execution of a smart contract. Let’s explore the usefulness of the requireInvariant statement and illustrate its application using the provided example.

invariant totalSharesLessThanDepositedAmount()
    totalSupply() <= depositedAmount();

invariant totalSharesLessThanUnderlyingBalance()
    totalSupply() <= underlying.balanceOf(currentContract)
    {
        preserved with(env e) {
            require e.msg.sender != currentContract;
            requireInvariant totalSharesLessThanDepositedAmount();
            requireInvariant depositedAmountLessThanContractUnderlyingAsset();
        }
    }

rule sharesRoundingTripFavoursContract(env e) {
    uint256 clientSharesBefore = balanceOf(e.msg.sender);
    uint256 contractSharesBefore = balanceOf(currentContract);

    requireInvariant totalSharesLessThanDepositedAmount();
    require e.msg.sender != currentContract;

    uint256 depositedAmount = depositedAmount();

    uint256 clientAmount = withdraw(e, clientSharesBefore);
    uint256 clientSharesAfter = deposit(e, clientAmount);
    uint256 contractSharesAfter = balanceOf(currentContract);
    assert (clientAmount == depositedAmount) => clientSharesBefore <= clientSharesAfter; 
    
    // all other states
    assert (clientAmount < depositedAmount) => clientSharesBefore >= clientSharesAfter;
    assert contractSharesBefore <= contractSharesAfter;
}

Importance of Require Invariants:

1. Ensuring Invariant Consistency:

   • The totalSharesLessThanUnderlyingBalance invariant expands the validation scope to include the underlying balance of the current contract. By utilizing the previously established totalSharesLessThanDepositedAmount invariant as a prerequisite, the specification writer ensures that the total shares in the contract remain within the limits of the underlying asset balance. This requireInvariant approach effectively eliminates counterexamples in states that have already been proven to be unattainable.

2. Validation Through Rules:

   • The sharesRoundingTripFavoursContract rule showcases the application of require invariants to verify the behavior of share transactions. Similarly to the invariant example, the requireInvariant statements enable the specification writer to disregard counterexamples in states that are not relevant to the intended behavior.

In conclusion, the “Require Invariants” design pattern, as demonstrated through the provided example, offers a systematic methodology to define, validate, and uphold critical conditions within smart contract specifications. for more information, please visit the documentation.