Support properties of the form `must always emit an event when storage is updated `

[0xkarmacoma]

Example here with Certora:

https://github.com/Cyfrin/3-gas-bad-nft-marketplace-audit/blob/main/certora/spec/GasBadNft.spec

[ByungHeonLEE]

I cannot find the eventLog being called in the Storage.store function. Does this issue mean need to implement the event logging using the EventLog class and apply the rules as shown in the example?

[0xkarmacoma]

I cannot find the eventLog being called in the Storage.store function. Does this issue mean need to implement the event logging using the EventLog class and apply the rules as shown in the example?

the idea is that we want to check contracts like this:

event Log(uint256 oldValue, uint256 newValue);

contract Foo {
    uint256 value;

    // good
    function logsAndStores(uint256 newValue) external {
        emit Log(value, newValue);
        value = newValue;
    }

    // bad
    function justStores(uint256 newValue) external {
        value = newValue;
    }
}

Right now there is no way to express in halmos that logsAndStores is good and justStores is bad (because of the missing log).

Certora supports it with hooks on log and store events, and incrementing a counter when a hook is triggered is a way to check that they match.

[ByungHeonLEE]

@karmacoma-eth Ok, will do after implementing TLOAD/TSTORE