How Certora seeds the contract state when running a rule?

CVL Support
1

I am stuck in the Reserve spec of the Lesson 8

I got counter examples when running the ReserveListFixed.sol against the Reserve.spec

The counter examples are both because of invalid states.
I wonder to how to avoid that?

2

Hi, the problem is that the assumption (pre-state) is made on one variable address t and the simulation of the function is on a different variable, address token

preserved removeReserve(address token) {
require getTokenAtIndex(getIdOfToken(token)) != 0;
}

you need to add a require(token == t).

Think about an invariant with a preserve block as a rule:
in your case it would be:

rule correlatedLists(uint256 i, address t) {
// assume the precondition
require((i == 0 =>(getTokenAtIndex(i) == t => getIdOfToken(t) == i)) &&
		((i != 0 && t != 0) =>(getIdOfToken(t) == i <=> getTokenAtIndex(i) == t));

//  preserve block 
address token; address stableToken; address varToken; uint256 fee;
require token != 0;
bool alreadyAdded = getTokenAtIndex(getIdOfToken(token)) != 0 || getTokenAtIndex(0) == token;
require !alreadyAdded;
// call the function with the arguments defined in the preserve
addReserve(token, stableToken, varToken,  fee);
//verify that the invariant holds 
assert((i == 0 =>(getTokenAtIndex(i) == t => getIdOfToken(t) == i)) &&
		((i != 0 && t != 0) =>(getIdOfToken(t) == i <=> getTokenAtIndex(i) == t));
}

Now, you can see that there is no relationship between the first require and the function call

3

Thank you Nurit.

I am a bit confused about the storage management in Certora. I assumes there should be one consistent storage emulation for the same invariant. But it seems not.

From the pre-state, we can see the underlyingList[2] == 0x401, and reserves[0x401].id == 2

assume invariant in pre-state
ReserveList.getTokenAtIndex(2) / 0x401 SUCCESS
ReserveList.getIdOfToken(0x401) / 2 SUCCESS
ReserveList.getIdOfToken(0x401) / 2 SUCCESS
ReserveList.getTokenAtIndex(2) / 0x401 SUCCESS

Preserved block start
ReserveList.getTokenAtIndex(2) / 0x401 SUCCESS

However I don’t understand the sequence below. I didn’t constraint that the token in removeReserve(address token) is the same token t as in the invariant, so Certora can remove a different token which is 0x402 here, but it says Load from reserves[*].id: 2, which means it thinks reserves[0x402].id = 2, which already breaks the pre-condition
(i != 0 && t != 0) =>(getIdOfToken(t) == i <=> getTokenAtIndex(i) == t).

Even though I don’t restrict the token to be the same as t, I think Certora should make sure the pre-condition remains true before executing any code. Or I still don’t get it?

removeReserve(token)
ReserveList.removeReserve(0x402) SUCCESS
Load from reserves[].id: 2
Load from underlyingList[2]: 0x401
Load from reserves[].id: 2
Store at underlyingList[2]: 0x0
Store at reserves[*].id: 0

4

No worries Nurit. I just had a zoom call with Michael, and now I understand that how Certora seeds the storage. Basically when it processes the PB, it does not care about the pre-condition.

In this case, if we require token == t in the PB, we only prove that invariant in a specific case, that is,
given a token t at index i, removing it by calling removeReserve(t) will delete the token t, which makes getIdOfToken(t) == 0 and getTokenAtIndex(i) == 0.

It cannot not prove that given a token t at index i, if we remove an arbitrary token t2, the invariant remains true, because Certora will find counter example due to the fact PB does not have to follow the invariant requirement

require((i == 0 =>(getTokenAtIndex(i) == t => getIdOfToken(t) == i)) &&
		((i != 0 && t != 0) =>(getIdOfToken(t) == i <=> getTokenAtIndex(i) == t));

Anyway. I understand the system better now

1 Like