makerdao / mkr-mcd-spec

High level KSpecification for the MCD System by Runtime Verification and Maker Foundation
GNU General Public License v3.0
28 stars 9 forks source link

Transaction level logging #191

Closed ehildenb closed 4 years ago

ehildenb commented 4 years ago

This PR makes it so that all the events associated with a single transaction are grouped together, so that when processing them we no longer need to manually filter out by looking for Measure events.

A couple of the properties needed to be updated because they depended on seeing intermediate events. In particular:

Overall, I think these properties end up being stated cleaner.