Certora formally verified rewards checker

[QGarchery]

Please look at the README for a description of this PR

[codecov-commenter]

Codecov Report

All modified and coverable lines are covered by tests :white_check_mark:

Project coverage is 98.51%. Comparing base (52363dc) to head (821c8ec).

:exclamation: Your organization needs to install the Codecov GitHub app to enable full functionality.

Additional details and impacted files

```diff @@ Coverage Diff @@ ## main #1656 +/- ## ======================================= Coverage 98.51% 98.51% ======================================= Files 15 15 Lines 1078 1078 ======================================= Hits 1062 1062 Misses 16 16 ```

:umbrella: View full report in Codecov by Sentry.
:loudspeaker: Have feedback on the report? Share it here.

[QGarchery]

I see that you currently have no rules that checks that the values sum up correctly. Is this something you want to add?

In Checker.sol, it is checked that the total rewards is the value stored in the root. What you are suggesting is to verify that the value stored in the root is the sum of the values of the leaves underneath it ? Is it possible to do that in Certora ? I thought the current way is exactly how you would specify that in Certora (ie have a ghost variable value that is defined as the sum of the values of children directly underneath)

[jhoenicke]

In Checker.sol, it is checked that the total rewards is the value stored in the root. What you are suggesting is to verify that the value stored in the root is the sum of the values of the leaves underneath it ?

A simple thing to add is a check in wellFormed().

I was also wondering about proving something like all users can never claim more than the value in root, but that's not straightforward to do. We use ghost variables for sums, so it's already the case that some things are not checked by the solver (e.g. that the ghost sum is updated correctly). Also you would need monotonicity assumptions in setRoot() to ensure that the claimed amount is at most the value stored for the user in the last root that was set. And the reasoning that the sum of claimed is lower than the sum of values if each individual claim is smaller than each individual value is also not possible to do with the solver, since it doesn't understand the concept of sums.

[QGarchery]

A simple thing to add is a check in wellFormed().

Oh right, that's an oversight, we should definitely add that !

I was also wondering about proving something like all users can never claim more than the value in root, but that's not straightforward to do

That would be a nice property to prove, but I'm not sure either how to do it