Is it possible to use inputs in a ghost function?

CVL Support
1

I am attempting to write this ghost function:

ghost sum_all_points(uint epoch, address vault) returns uint {
    init_state axiom sum_all_points(epoch, vault) == 0;
}

and getting the error:

CRITICAL: [main] ERROR ALWAYS - certora/specs/Badgerteryanarmen1.spec:84:27: Syntax error: unexpected token near ID(epoch)
CRITICAL: [main] ERROR ALWAYS - certora/specs/Badgerteryanarmen1.spec:84:27: Couldn't repair and continue parse unexpected token near ID(epoch)
2

If you need it only for init_state axiom, then there will be another solution:

ghost ghostWithArguments(uint256, address) returns uint256 {
         init_state axiom forall uint256 num. forall address addr. ghostWithArguments(num, addr) == 0;
}

If you want to retrieve ghost information in a rule for example and store it in var, then you just need to pass arguments that matches types, names are not important:

rule ghostExample(){
    ...
    uint256 id; address user;
    uint256 getGhostInfo = ghostWithArguments(id, user);
    ...
}
2 Likes
3

To add to @RedLikeRoses explanation -

A ghost is an uninterpreted function (lesson 3 in the tutorials), so the only information they need to be fed with is args types and return types.

The right way to declare a ghost that takes args by declaring only types:

ghost sum_all_points(uint, address) returns uint {}

The way to then nullify all values upon constructor is by using the forall quantifier as @RedLikeRoses suggested.

1 Like