makerdao / k-dss

formal verification of multicollateral dai in the K framework
GNU Affero General Public License v3.0
14 stars 11 forks source link

Added dump and pot #10

Closed andy8052 closed 5 years ago

andy8052 commented 5 years ago

Added the specs for the accessors Vow.dump and End.pot.

I ran the specs and both are passing.

gbalabasquer commented 5 years ago

Do we need to upgrade the dss version for these specs? As otherwise CI will run every spec again. I'd suggest we upgrade dss only if necessary or after we apply all the pending changes.

andy8052 commented 5 years ago

Didn't even think about that. I can revert that

gbalabasquer commented 5 years ago

Actually seems your PR is setting the dss commit back to 9b5d1ac which is the one being used in the CI.

kmbarry1 commented 5 years ago

Yeah let's not update dss in this PR (I think current k-dss is already on latest master of dss anyway).

Otherwise, LGTM!