Introduce entrypoints

[annenkov]

Both Tezos and Concordium have a concept of entypoints which we model as a Msg type, usually represented as an inductive type with several constructors corresponding to the entrypoints. However, it's difficult to send messages to an (arbitrary) contract that supports only some of the entrypoints. Therefore, we need a more abstract notion of an interface that would allow for a more flexible way of specifying the supported entrypoints.