runtimeverification / michelson-semantics

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

Add real entrypoint semantics for `SELF` #231

Closed hjorthjort closed 3 years ago

hjorthjort commented 3 years ago

Attempted in #229, but it contains other things as well. Make a new PR with just the necessary changes for the SELF instruction to work properly.

The paramtype cell: Change the paramtype cell to contain a map from field annotations, e.g. %getBalance to type, e.g. pair nat nat.