Specification proving reachability for all elements

[jhoenicke]

As discussed earlier, here is the specification that uses a ghost predicate reach to express whether elements are transitively reachable from another via the owners linked list. This should help to prove that every owner is on the linked list.

This is only tested on staging with the beta version. To run this, install certora-cli-beta and run

certoraRun certora/configs/Owner.conf --server staging

The spec is still not completely passing. Especially the initialization seems to be problematic for some of the invariants. Also the setup function may corrupt the list, so one has to prove that it can never called e.g. by stating an invariant that threshold is never zero.

[github-actions[bot]]

CLA Assistant Lite bot All contributors have signed the CLA ✍️ ✅

[jhoenicke]

The link to the CLA by the bot above leads to a 404 page.

[mmv08]

Please try this link: https://safe.global/cla

[mmv08]

Also the setup function may corrupt the list, so one has to prove that it can never called e.g. by stating an invariant that threshold is never zero.

How? The only obvious way to me is through a delegatecall, but for verification purposes, we decided to be optimistic about delegatecalls because no property can be held in this case, see https://github.com/safe-global/safe-contracts/blob/47a3620ed937c780d26ff218b76edaaef658f7e2/certora/applyHarness.patch#L19-L21

[jhoenicke]

Also the setup function may corrupt the list, so one has to prove that it can never called e.g. by stating an invariant that threshold is never zero.

How? The only obvious way to me is through a delegatecall, but for verification purposes, we decided to be optimistic about delegatecalls because no property can be held in this case, see

setup is external and callable by everyone. The only thing that prevents this is the threshold, as indicated by the comment in Safe.sol, line 105.

We can solve this easily by adding the invariant that threshold is always non-zero. It just requires an invariant and adding that to the failing invariant in the preserved block.

[mmv08]

Also the setup function may corrupt the list, so one has to prove that it can never called e.g. by stating an invariant that threshold is never zero.

How? The only obvious way to me is through a delegatecall, but for verification purposes, we decided to be optimistic about delegatecalls because no property can be held in this case, see

setup is external and callable by everyone. The only thing that prevents this is the threshold, as indicated by the comment in Safe.sol, line 105.

We can solve this easily by adding the invariant that threshold is always non-zero. It just requires an invariant and adding that to the failing invariant in the preserved block.

Ahh, now I see what you mean. I think this is solved in our harness where the setup is called inside the. constructor: https://github.com/safe-global/safe-contracts/blob/47a3620ed937c780d26ff218b76edaaef658f7e2/certora/harnesses/SafeHarness.sol

I would try to run these rules with the SafeHarness contract

[jhoenicke]

I have read the CLA Document and I hereby sign the CLA

[mmv08]

I will merge this to a separate branch, certoraOwnerReach and will play with the rules and see how it goes :) thanks