search

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

Implicit lower bounds on rule inputs #174

Closed ehildenb closed 4 years ago

ehildenb commented 4 years ago

Many places in the solidity use uint ..., which is an implicit positivity constraint on the inputs to the functions.

This adds those constraints to the model.

This also adds dss repo as a submodule for convenience of conformance testing. This means that this submodule needs to be updated periodically and any updates to the model added in.