search

runtimeverification / avm-semantics

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

multi-transaction proof claims #220

Closed nwatson22 closed 1 year ago

nwatson22 commented 1 year ago

This PR attempts to smooth out the semantics to better support symbolic execution of more complex transaction groups, including inner calls and multiple transactions in the outer group. The main spec file to focus on is tests/specs/calls/buy-asset-spec.md.

When this is reviewed, I don't know what's going on with the deleted deps folders. These probably shouldn't be removed but I'm not sure. I might not be refreshing my dependencies correctly.

Additionally, there is the change made in tests/specs/verification.k to the getAddressBytes-related lemmas, which we should probably discuss.

Edit: I removed some comments after the CI was passing and now it's failing. Does not fail when tested locally.

geo2a commented 1 year ago

@nwatson22 which z3 are you using locally? The CI uses 4.8.15 from the k-framework Docker image. I suggest we use 4.8.15 locally as well (I was using a newer one).

Installing z3 4.8.15 is easy with Nix:

nix profile install nixpkgs#z3_4_8

I've made some changes to the spec and looks like it now passes consistently.