Use Reference EntryPoint in Formal Verification

[nlordell]

Currently, the 4337 module is formally verified assuming a well-behaved ERC-4337 EntryPoint contract. However, it should be possible (and beneficial) to formally verify the module invariant with the reference EntryPoint implementation, in order to catch any additional issues related to unanticipated interactions between the EntryPoint, the Safe account, and the 4337 module.

Expected Outcome

The existing FV rules should be ported to use the reference EntryPoint contract.

[mmv08]

Based on internal testing and discussion with @jhoenicke, it doesn't seem possible to implement at this point without significantly altering the EntryPoint contract.

Our problem is that the static analysis has many unresolved calls. Due to the nature of the EntryPoint contract that makes many arbitrary calls to arbitrary contracts and the overall complexity of the scene (sender -> entrypoint -> safe singleton -> module -> singleton) it fails to resolve the call tree and detect the code to analyze. The Certora team is working on a feature that would enable developers to provide a resolution table for unresolved functions, and then the analyzer would inline those functions. The target release date for that feature is mid-March.

An example run here: https://prover.certora.com/output/6575/9e235d6791fd442f97dbc7f51c5d983a?anonymousKey=520ee3ef3c9205f5a4798b86b272090eff1edf15

Also, just for reference, leaving some starting attempts to formally verify the entrypoint contract by the Certora team: https://github.com/Certora/account-abstraction/tree/certora_dev (they munged the contract to hard code the sender to get around the resolution problem)