GitLab

Remove it from the contract's perspective for now.

- No longer require that block reward can be computed from height.
- Remove Chain's dependence on BlockHeader. Instead inline appropriate
  fields in Chain structure.
- Change step_block to use a BlockHeader now instead of manually
  specifying all the fields. The new BlockHeader now additionally
  contains the creator and reward of that block, so step_block in effect
  contains the reward.
- These refactorings means that the circulation proof changes. Introduce
  created_blocks to get list of blocks created by user, and prove
  instead that the circulation equals the sum of rewards in blocks.
- Rename "baker" to a more general "creator" globally

Versions are not used for anything and the comment is outdated.

This is much more realistic, as allowing contracts to efficiently access
transaction histories for all addresses is extremely expensive. To do
this, we
* Add an account_balance operation in Chain instead
* Change incoming_txs and outgoing_txs to compute transactions from
  traces
* Require implementations to give a proof-relevant trace, and rework
  proofs to use these, as necessary

This holds for reachable states without this, as proven in
undeployed_contract_no_in_txs.

We don't need these for our current embedding. We may need them later
for inter-contract communication.

A state being reachable means there is an execution starting from the
empty state, that ends up in the state.

- Remove 'prove' tactic
- Remove some duplicated tactics and make some proofs more efficient

Match on smaller expressions, making everything much faster. Also
optimize solve_single.