runtimeverification / michelson-semantics

A K semantics of Tezos' Michelson language.
Other
17 stars 6 forks source link

Set manager spec #210

Closed hjorthjort closed 3 years ago

hjorthjort commented 3 years ago

Closes #201

The claims are not currently being proven in CI (they are not k code blocks) because we are still missing #pushState and #popState.

I discussed with @sskeirik and came up with the idea that we can have #runProve as a generic way to make a call to the contract, because we will always do the same operations.