search

dapphub / klab

K framework proof explorer & smart contract specification format
GNU Affero General Public License v3.0
124 stars 36 forks source link

Remove assert ACCT_ID is never 0 #424

Closed nanexcool closed 4 years ago

nanexcool commented 4 years ago

This is conflicting when running proofs with other proofs as lemmas. Per @MrChico " the assumption that ACCT_ID =/= 0 might not be provable for other contracts"

MrChico commented 4 years ago

I think better would be to add the assumption that other contracts mentioned are also =/= 0

nanexcool commented 4 years ago

@MrChico ah ok, in that case I have no idea what to do lol

nanexcool commented 4 years ago

Check calls, grab unique contracts (different than the current subject) and add them to the if

nanexcool commented 4 years ago

Any update on this? I've checked it works on this run

https://reports.makerfoundation.com/k-dss/33d35d2934cfc47ccb98/

MrChico commented 4 years ago

Yeah, this looks good. Thanks @nanexcool !