search

runtimeverification / avm-semantics

BSD 3-Clause "New" or "Revised" License
15 stars 4 forks source link

Transaction call claims #191

Closed nwatson22 closed 1 year ago

nwatson22 commented 1 year ago

This adds some proof claims which it is hoped we can use as a jumping-off point for automatically generating claims from application calls made through the python frontend for kavm.

geo2a commented 1 year ago

@nwatson22 I've added a lemma that effectively just drops Sha512_256raw from proofs. Ideally, we would not want to do that, but rather we'd change the implementation of getAppAddressBytes with a lemma. However, I could not manage to make getAppAddressBytes to not apply in symbolic cases. We can discuss further when on a call.

Please make sure the changes I made look fine to you and then feel free to add "automerge".

geo2a commented 1 year ago

Oops, looks like I had not built K locally for some time. I'll debug the failing claim with the new build of K and update the PR.