feat: halmos symbolic tests

[0xDiscotech]

Symbolic tests of the OptimismSuperchain20 properties that are stateless.

• Had issues with symbolic addresses, when pranking senders and using _from and _to symbolic values. That's why I had to use concrete values for them instead.
• Not sure if the mocked messenger is ok, or more logic can be removed from it
• Copy-pasted the PROPERTIES.md file from Teddy's branch and marked the halmos tested boxes.
• The test utils will be moved to the helper file used on Teddy's PR in the future

To run the symbolic tests just run just test-halmos-all on packages/contracts-bedrock .
Make sure to have the nightly version of halmos installed (halmos 0.1.15.dev2+gc3f45dd).

TODO: (maybe on a future PR) Complete the test of id 7 by using a symbolic value as x domain sender also.
Currently having issues when setting that value through a custom setter bc seems that after etching the storage slots are not being considered.
Also tried to hardcode a constant storage slot and update/get it with assembly but neither worked.

CLOSES FUZZ-25
CLOSES FUZZ-26

[0xteddybear]

looking good! Didn't find any big issues and appreciated the care you put into DX

[0xteddybear]

this wasn't added as a dependency

[0xteddybear]

I believe it'd be hugely benefitial to prove it's enough for only the cross-domain caller to be valid, since that allows for a check to be removed

it's okay if we can't prove that, but I'd rather have the property retain its definition and be partially verified to be clear about that, perhaps with a note on what is it that we could prove

[0xteddybear]

are the modifications to this file intended? seems like an artifact from a merge

[0xteddybear]

✨

[0xteddybear]

what do you use to format markdown? so I can use it as well and keep things consistent 💖

[0xteddybear]

I managed to get the contract down to this:

contract MockL2ToL2Messenger {
    // Setting the current cross domain sender for the check of sender address equals the supertoken address
    address internal immutable CROSS_DOMAIN_SENDER;
    constructor(address _xDomainSender) {
        CROSS_DOMAIN_SENDER = _xDomainSender;
    }
    function sendMessage(uint256 , address , bytes calldata) external payable {
    }
    function crossDomainMessageSource() external view returns (uint256 _source) {
        _source = block.chainid + 1;
    }
    function crossDomainMessageSender() external view returns (address _sender) {
        _sender = CROSS_DOMAIN_SENDER;
    }
}

with all tests passing. I believe the extra code makes it a bit confusing for the reader

[0xteddybear]

didn't halmos' nightly build include support for tstore already? 🤔 or am I mixing it up with something else?

[0xteddybear]

s/property-id/property/
btw @drgorillamd are we using these natspec tags to generate something? do we plan to?

[drgorillamd]

idea is to have the possibility, but rn no, we don't...

[0xteddybear]

Why send it to the cross_l2_inbox instead of to?

side question: would that revert on relay on a live system when trying to relay?

[0xteddybear]

in other testing campaigns we have a file with this exact same name but with stuff that's

• potentially reusable by other campaigns -> not coupled to the codebase under test
• coupled to the tools we use (echidna/halmos/medusa)

so it'd be clearer if this file was named something else, such as HalmosBase (or anything else you prefer)