• Jakob Botsch Nielsen's avatar
    Specify and prove an initial blockchain semantics · 71ea5d00
    Jakob Botsch Nielsen authored
    This specifies an initial version of blockchain semantics. The semantics
    are specified as several relations:
    ChainStep :
      Environment -> Action -> Tx ->
      Environment -> list Action ->
    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
    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 we may have ChainStep pre act
    tx post []. Then the ChainStep relation will capture that the only thing
    that has changed in the post environment is that tx has been added to
    the chain (so that the appropriate account balances have been updated),
    but for instance also that no new contracts have appeared. Since this is
    just a transfer, there also cannot be any new actions to execute.
    The semantics of the environment updates are captured in an abstract
    manner to allow for different implementations of blockchains.
    Specifically, we use an equivalence relation
    EnvironmentEquiv : Environment -> Environment -> Prop and just require
    that the environment is equivalent (under this relation) to an obvious
    implementation of an environment. We implement an obvious blockchain,
    LocalBlockchain, which uses finite maps with log n access times rather
    than the linear maps used in the default semantics.
    A single block, when added to a blockchain, consists of a list of these
    actions to execute. In each block this list of actions must then be
    executed (in a correct manner) until no more actions are left. This is
    captured in
    BlockTrace :
      Environment -> list Action ->
      Environment -> list Action -> Prop.
    For all intents and purposes this can be seen as just a transitive
    reflexive closure of the ChainStep relation above. Right now it only
    allows blocks to reduce steps in a depth-first order, but this relation
    should be simple to update to other or more general orders of reduction.
    Note that ChainStep and BlockTrace say nothing about new blocks, but
    only about execution within blocks. The semantics of how blocks are
    added to the chain is captured in
    ChainTrace : Environment -> Environment -> Prop.
    This is a collection of block traces and representing additions of
    blocks. At each block added, ChainTrace also captures that the
    environment must be updated accordingly so that contracts can access
    information about block numbers correctly.
    Finally, a blockchain must always be able to prove that there is a
    ChainTrace from its initial environment (the genesis blockchain) to its
    current environment.
    There are several TODOs left in the semantics:
    1. We need to account for gas and allow execution failures
    2. We need to put restrictions on when contracts can appear as the
    source of actions
    3. We need to capture soundness of the add_block function in blockchain
    We also provide to sanity checks for these semantics:
    1. We prove them for a simple block chain (LocalBlockchain.v).
    2. We prove a "circulation" theorem for any blockchain satisfying the
    semantics. That is, we show the following theorem:
    Theorem chain_trace_circulation
          {env_start env_end : Environment}
          (trace : ChainTrace env_start env_end)
      : circulation env_end =
        (circulation env_start +
           (block_height (block_header env_start))
           (block_height (block_header env_end)))%Z.