08 Invariants : Can someone explain why this rule with ghost function fails?

Epoch Infinity
1

I am replacing isActiveManager with a ghost function initialized to all false. After a function call, the rule ManagerZeroIsNotActive fails even when there is no hook call to update address 0.

Ghost definition

ghost activeManagerMap(address) returns bool {
	init_state axiom forall address m. activeManagerMap(m) == false;
}

hook Sstore isActiveManager[KEY address a] bool value (bool old_value) STORAGE {
	havoc activeManagerMap assuming forall address m. m == a?
	activeManagerMap@new(a) == value:
	activeManagerMap@new(a) == activeManagerMap@old(a);
}

Manager rule

rule uniqueManager(uint256 fundId1, uint256 fundId2, method f) {
	require fundId1 != fundId2;
    requireInvariant ManagerZeroIsNotActive();
    require getCurrentManager(fundId1) != 0 => activeManagerMap(getCurrentManager(fundId1));
	require getCurrentManager(fundId2) != 0 => activeManagerMap(getCurrentManager(fundId2));
	require getCurrentManager(fundId1) != getCurrentManager(fundId2) ;
				
	env e;
	calldataarg args;
	f(e,args);

	assert getCurrentManager(fundId1) != getCurrentManager(fundId2), "managers not different";
	assert getCurrentManager(fundId1) != 0 => activeManagerMap(getCurrentManager(fundId1)), "manager of fund1 is not active";
	assert getCurrentManager(fundId2) != 0 => activeManagerMap(getCurrentManager(fundId2)), "manager of fund2 is not active";
}

Please find the details [here](https://prover.certora.com/output/48476/b1a8b631c87c75df47e5/?anonymousKey=ee6b4f2fab23c88f9f3444600410e9c26a3a6e83#ManagerZeroIsNotActive_preserveResults).
2

should be m and not a.

hook Sstore isActiveManager[KEY address a] bool value (bool old_value) STORAGE {
	havoc activeManagerMap assuming forall address m. m == a?
	activeManagerMap@new(m) == value: <--- here doesn't really matter as a==m
	activeManagerMap@new(m) == activeManagerMap@old(m); <-- here it is very important 
}
2 Likes