Add update_token_pool_internal entrypoint spec

runtimeverification / michelson-semantics

A K semantics of Tezos' Michelson language.

Other

17 stars 6 forks source link

Add update_token_pool_internal entrypoint spec #227

Closed sskeirik closed 3 years ago

sskeirik commented 3 years ago

Note: this proof is still broken due to the negative case proofs not going through. As far as I can tell, these proofs get stuck because the backend is not able to prune unsatisfiable states, but I may have not tightened some initial condition enough.

EDIT: I would appreciate others looking into the negative case proofs and seeing if the final states do actually seem to have unsatisfiable path conditions.

Fixes: #220

hjorthjort commented 3 years ago

I'll put off review on this until we have #234 merged, so that we can make this PR smaller

ehildenb commented 3 years ago

Double check that updating to master doesn't fix this.
Double check local build is using submodule.
Doube check z3 versions.
Try archiveArtifacts on teh kore-exec.tar.gz and download it from the Artifacts page on CI. Check K Jenkinsfile for how to do (it does the same with kserver.log).

nishantjr commented 3 years ago

Ready to review.

hjorthjort commented 3 years ago

Looks like you have a Makefile issue:


[Error] Critical: Module DEXTER-REMOVELIQUIDITY-SPEC does not exist.