runtimeverification / michelson-semantics

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

Implement abstract state serialization #202

Closed sskeirik closed 3 years ago

sskeirik commented 3 years ago

This PR implements:

To check that these functions are correct, you can compare the type structure in the contract with the type structure in the compiled versions of the Michelson contracts:

The relevant type information is contained in the storage and parameter declarations at the top of the respective files.

Fixes: #199