Wrong ghost value

CVL Support
1

In some of my rules, Certora prover uses the wrong value of a ghost variable even after updating it correctly.

For example, in this rule, the ghost value userPoints(epoch, vault, user) is set to 212, but is then read to equal 11.

BugInGhostValueAndResult
BugInGhostValueAndResult1024×813 47.9 KB

This issue occurs in every single rule mentioned in the linked file. Is this a bug in the Certora prover?

https://prover.certora.com/output/48476/4928716d0cf86c6da835/?anonymousKey=9be66574d5f3c1845228426ea76cc9fadcab9369#userPointsNonDecreasingResults

2

I suspect that the parameters passed to the ghost userPoints are not the same in the pointsBefore/pointsAfter computation, and in the hook.
Note that epoch is 10, but within the hook, epoch is 0.

Also note that your hook definition sets the new value of userPoints like this:
havoc userPoints assuming userPoints@new(epoch, vault, user) == value;
Which has the effect of potentially changing the value of the userPoints in all places that are not the concrete epoch, vault, and user specified in the hook. This can be fixed with using forall, but perhaps you want to address the issue of having different values for epoch, vault and user in the rule and in the hook first.

3

As @Shelly mentioned, you probably want to update the ghost for each trio without changing any value associated with the other trios.

for that you need to use a forall statement and specify how the ghost should update the value in case the trio is the same as the keys in the hook, and how the ghost should update the value in any other case.
Remember that havoc is allowing to change the state completely which is probably not what you intend.

This is an example of a correct update of your ghost:

hook Sstore points[KEY uint256 epoch][KEY address vault][KEY address user] uint256 value (uint256 old_value) STORAGE {
    havoc userPointsSum assuming forall uint256 e. forall address v. forall address u. 
    (e == epoch && v == vault && u == user)? 
    userPointsSum@new(epoch, vault) == userPointsSum@old(epoch, vault) + value - old_value: 
    userPointsSum@new(epoch, vault) == userPointsSum@old(epoch, vault);
}

This update says - for the trio that is being changed in the assignment, add the new value as to sum a total, and for any other combination of the trio just leave the new value as the old value.