 25 Jun, 2019 4 commits


Jakob Botsch Nielsen authored

Jakob Botsch Nielsen authored

Jakob Botsch Nielsen authored

Jakob Botsch Nielsen authored

 24 Jun, 2019 8 commits


Jakob Botsch Nielsen authored

Jakob Botsch Nielsen authored

Jakob Botsch Nielsen authored

Jakob Botsch Nielsen authored
Remove it from the contract's perspective for now.

Jakob Botsch Nielsen authored

Jakob Botsch Nielsen authored

Jakob Botsch Nielsen authored

Jakob Botsch Nielsen authored

 21 Jun, 2019 2 commits


Jakob Botsch Nielsen authored

Jakob Botsch Nielsen authored
 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

 17 Jun, 2019 1 commit


Jakob Botsch Nielsen authored

 14 Jun, 2019 2 commits


Jakob Botsch Nielsen authored

Jakob Botsch Nielsen authored

 13 Jun, 2019 1 commit


Jakob Botsch Nielsen authored

 11 Jun, 2019 1 commit


Jakob Botsch Nielsen authored

 10 Jun, 2019 1 commit


Jakob Botsch Nielsen authored
Versions are not used for anything and the comment is outdated.

 07 Jun, 2019 2 commits


Jakob Botsch Nielsen authored

Jakob Botsch Nielsen authored

 06 Jun, 2019 2 commits


Jakob Botsch Nielsen authored

Jakob Botsch Nielsen authored
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 proofrelevant trace, and rework proofs to use these, as necessary

 31 May, 2019 3 commits


Jakob Botsch Nielsen authored
This holds for reachable states without this, as proven in undeployed_contract_no_in_txs.

Jakob Botsch Nielsen authored

Jakob Botsch Nielsen authored

 27 May, 2019 1 commit


Jakob Botsch Nielsen authored

 24 May, 2019 1 commit


Jakob Botsch Nielsen authored

 22 May, 2019 1 commit


Jakob Botsch Nielsen authored

 15 May, 2019 1 commit


Jakob Botsch Nielsen authored

 14 May, 2019 1 commit


Jakob Botsch Nielsen authored

 10 May, 2019 1 commit


Jakob Botsch Nielsen authored
We don't need these for our current embedding. We may need them later for intercontract communication.

 09 May, 2019 3 commits


Jakob Botsch Nielsen authored

Jakob Botsch Nielsen authored

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

 05 May, 2019 2 commits


Jakob Botsch Nielsen authored

Jakob Botsch Nielsen authored
 Remove 'prove' tactic  Remove some duplicated tactics and make some proofs more efficient

 03 May, 2019 2 commits


Jakob Botsch Nielsen authored

Jakob Botsch Nielsen authored
Match on smaller expressions, making everything much faster. Also optimize solve_single.
