search

runtimeverification / michelson-semantics

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

Add real entrypoint semantics for `CONTRACT` and `TRANSFER_TOKENS` #236

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 external contract interactions instruction to work properly.

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

sskeirik commented 3 years ago

This was recently merged in the entrypoints PR.