Feat: add Certora specs

[amusingaxl]

No description provided.

[pedrobergamini]

Looks good to me! Just commented an idea on Certora's GH actions workflow

New commits.

[pedrobergamini]

Nice work on this change

[sunbreak1211]

Maybe an interesting rule/invariant to do, if you end up having some extra time, would be to prove that after any call to set, the values updated can not end up being outside the min-max range and always respect be restricted by the step.
Then the fix ordering can be roll back and check that the rule would have caught that. In either case those things are also indirectly proved with the current rules so not really mandatory, but I guess it would be a more high level rule that helps guaranteeing those invariants.

[amusingaxl]

Maybe an interesting rule/invariant to do, if you end up having some extra time, would be to prove that after any call to set, the values updated can not end up being outside the min-max range and always respect be restricted by the step.

This was added in 67d5fbc.

Then the fix ordering can be roll back and check that the rule would have caught that.

Not entirely sure if I get what you're suggesting here.

The base branch was changed.

[pedrobergamini]

Added a few questions about the mocks, also, after reviewing the updated rules I thought it could be useful if we added the following one to ensure the config is always consistent:

rule config_min_less_than_max(bytes32 id) {
    uint16 min; uint16 max; uint16 step;
    min, max, step = cfgs(id);
    
    assert min <= max, "Configuration min should always be <= max";
}

[pedrobergamini]

Shouldn't we return chi here? As right now nChi is always == 0?

nChi = uint256(chi)

[amusingaxl]

As discussed, the return value is irrelevant to the main subject of the formal verification.
We just need to ensure that the calls to drip() and file() in the underlying contracts don't fail for reasons that are not relevant.

[pedrobergamini]

Would it be better if we returned the current duty instead of 0 here?

function drip(bytes32 ilk) external note returns (uint256 rate) {
    ilks[ilk].rho = now;
    rate = ilks[ilk].duty;  // Return current duty instead of 0
}

[amusingaxl]

Same as above.

[pedrobergamini]

Same question as Jug::drip, would it be better if we returned the dsr value here?

function drip() external note returns (uint256 tmp) {
    rho = now;
    tmp = dsr;  // Return current dsr instead of 0
}

[amusingaxl]

Same as above.

[pedrobergamini]

Looks good to me!