This specifies an initial version of blockchain semantics. The semantics
are specified as several relations:

ChainStep :
  Environment -> Action -> Tx ->
  Environment -> list Action ->
  Prop.

This relation captures the semantics of a single step/action in the
chain. Such an action can either be a transfer, contract deployment or
contract call. It specifies that when an action is executed in some
starting environment, then the blockchain records a transaction (Tx) on
the chain and performs certain updates to the environment. Finally, the
step also results in possible new actions to be executed due to contract
execution.

An environment is for now simply a Chain (which contracts can interact
with) and a collection of contracts that have been deployed to some
addresses. The Chain contains various useful operations for contracts
such as the current block number or ability to query transactions and
user balances.

For example, for a simple transfer action w...