Simplifications for symbolic reasoning

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

Closed ehildenb closed 3 years ago

ehildenb commented 3 years ago

These are a few simplifications to the semantics I found which help my local work with symbolic reasoning.

Make wish a non-contextual function, so that it's possible to use it over the pre/post states in proofs.
Mark wards as functional.
Add domains.md explicit import.
makeCall no longer defaults to throwing an exception, because checkLock and checkAuth handle that.