Summary
Event emission (emit and rawLog) is explicitly excluded from whole-contract Layer 2 proofs in SupportedSpec.lean (lines 76-77). Every Solidity function emits events, making this a gap for full parity.
Current state
emit and rawLog are accepted by the macro and generate correct IR- They are marked
stmtTouchesUnsupportedContractSurface = true
- Workaround exists: use
rawLog + mstore with local_obligations (as done in morpho-verity's flashLoan and setAuthorizationWithSig)
- But this workaround is extremely verbose and not covered by proofs
Proposed approach
Events are pure output — they don't affect contract state. The Layer 2 proof framework should be extended with a log-trace model:
- Add a
logTrace : List LogEntry field to the proof state
emit/rawLog statements append to the log trace- The correctness theorem states that the storage state transitions correctly AND the log trace matches the expected events
- Since events don't affect storage, existing storage-focused proofs remain valid
Impact
- morpho-verity: All 16 mutable functions should emit events but currently only 2 do (via
local_obligations)
- General: Any contract aiming for full Solidity parity needs events
- Events are important for off-chain indexing and monitoring — a formally verified contract without events is incomplete
Priority
Lower than storage writes (#1618) and external calls (#1635) since events don't affect state transitions. But higher than return values since events are observable behavior.
Related
Summary
Event emission (
emitandrawLog) is explicitly excluded from whole-contract Layer 2 proofs inSupportedSpec.lean(lines 76-77). Every Solidity function emits events, making this a gap for full parity.Current state
emitandrawLogare accepted by the macro and generate correct IRstmtTouchesUnsupportedContractSurface = truerawLog+mstorewithlocal_obligations(as done in morpho-verity'sflashLoanandsetAuthorizationWithSig)Proposed approach
Events are pure output — they don't affect contract state. The Layer 2 proof framework should be extended with a log-trace model:
logTrace : List LogEntryfield to the proof stateemit/rawLogstatements append to the log traceImpact
local_obligations)Priority
Lower than storage writes (#1618) and external calls (#1635) since events don't affect state transitions. But higher than return values since events are observable behavior.
Related