Hey, i started learning Certora recently (Yesterday), and I am doing the Official Tutorial as part of my learning journey.
My issue is I don’t know how exactly I can inform the prover to start from a feasible state; check this rule totalSupplyNotLessThanSingleUserBalance.
The fix I am thinking about is something similar to this: require SUM_OF balanceOf(e, args) == totalSupply(e); before calling f(e, args);.
Appreciate any help or tips.
Best
Greetings @zkstoic,
First congrats on starting learning Certora!
Let me guide you through this:
You are correct that the prover finds an infeasible state, which we cannot express easily. Your suggested fix is correct, yet we cannot require sums of mappings (yet).
I believe you are in an early stage of the tutorial so the actual fix to the rule is not yet necessary, but just to understand why the violation occurs.
If you want to challenge yourself, think of an elaborate require that implements your suggestion.
We actually care about not the sum of all the users in the contract, but only the parties participating in the transaction. For example, for a transfer operation, we only care about the recipient and the sender balances, because they are the only ones that change (in a properly functioning ERC20 contract, at least).
So what you can require from the balances of these parties is practically:
balance(receiver) + balance(sender) <= totalSupply
Try to implement this specifically for the transfer-like functions and see if the rule is verified.
Hope this helps.