- 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 proof-relevant 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 inter-contract 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.
-