Make "failed with no transactions made" error more explicit

[PaulRBerg]

I'm getting the following error:

failed with no transactions made ⁉️

I looked at the the related GitHub issues but I am now even more confused than before.

I made sure that the child contract I used to inherit from my main contract has a dummy constructor, as per the instructions given in the crash course:

contract FintrollerInvariants is Fintroller {
    constructor() {}

    function echidna_liquidation_incentive() external view returns (bool) {
        return
            liquidationIncentiveMantissa >= liquidationIncentiveLowerBoundMantissa &&
            liquidationIncentiveMantissa <= liquidationIncentiveUpperBoundMantissa;
    }
}

Is there anything wrong with my invariants contract?

[gustavo-grieco]

failed with no transactions made

This means that your transaction is returning false (or reverting) before starting to generate any transaction. Just as a sanity check, you can change your property to return always true. If that works, it means that:

liquidationIncentiveMantissa >= liquidationIncentiveLowerBoundMantissa && liquidationIncentiveMantissa <= liquidationIncentiveUpperBoundMantissa;

is false after the initialization of the contract.

Is there anything wrong with my invariants contract?

Unfortunately, we don't know that, if the contract is as complicated as Fintroller: you will need code review for that.

[PaulRBerg]

just as a sanity check, you can change your property to return always true

I did that and the error disappeared.

is false after the initialization of the contract.

This is correct. But it doesn't invalidate my rationale: the message could be clearer and ideally provide support for the user with regard to what they can do to make the error go away.

So if liquidationIncentiveMantissa can be zero immediately after the contract is initialised, does it mean that I have to rewrite my property like this?

return liquidationIncentiveMantissa == 0 || (liquidationIncentiveMantissa >= liquidationIncentiveLowerBoundMantissa && liquidationIncentiveMantissa <= liquidationIncentiveUpperBoundMantissa);

Or is there any Echidna feature for checking whether the contract has just been initialised?

[gustavo-grieco]

This is correct. But it doesn't invalidate my rationale: the message could be clearer and ideally provide support for the user with regard to what they can do to make the error go away.

Yes, I agree. We can improve the message, but it is unclear what to suggest to the user beyond "check your property, since it is returning false". This is not really an error. Echidna found a way to make your property false, but it did not need to generate any transactions! :smile:

So if liquidationIncentiveMantissa can be zero immediately after the contract is initialised, does it mean that I have to rewrite my property like this?

That could work. Just go ahead and try it. We usually experiment with invariants until we found the right ones.

Or is there any Echidna feature for checking whether the contract has just been initialised?

We don't have anything specific to recommend. Contract invariant should be true during the lifetime of the contract. If they are not, even during one block after the initialization.. then they are not invariants. This is not an issue with Echidna (beyond the poor way of communicating this in the error message).

[PaulRBerg]

but it is unclear what to suggest to the user beyond "check your property, since it is returning false"

I'd say something like:

Echidna executes the property even before calling any functions. You should ensure that the property accounts for the values your storage variables have when the contract has just been initialized.

For noobs like me, the aforementioned error message would've saved hours.

That could work. Just go ahead and try it. We usually experiment with invariants until we found the right ones.

Yeah, that worked.