1. 20 Nov, 2019 1 commit
    • Jakob Botsch Nielsen's avatar
      Add contract_induction tactic · 6b7b7d05
      Jakob Botsch Nielsen authored
      This tactic applies contract_centric with evars and puts the "establish
      facts" obligation last. This allows the user to instantiate these during
      the proof of the property.
      6b7b7d05
  2. 19 Nov, 2019 1 commit
  3. 18 Nov, 2019 1 commit
  4. 13 Nov, 2019 2 commits
  5. 05 Nov, 2019 1 commit
  6. 04 Nov, 2019 2 commits
  7. 31 Oct, 2019 1 commit
  8. 30 Oct, 2019 2 commits
  9. 29 Oct, 2019 1 commit
  10. 28 Oct, 2019 3 commits
  11. 25 Oct, 2019 1 commit
  12. 15 Oct, 2019 1 commit
  13. 13 Oct, 2019 2 commits
  14. 10 Oct, 2019 1 commit
  15. 25 Jun, 2019 4 commits
  16. 24 Jun, 2019 8 commits
  17. 21 Jun, 2019 2 commits
    • Jakob Botsch Nielsen's avatar
      Fix for Coq 8.8 · f4bc2be8
      Jakob Botsch Nielsen authored
      f4bc2be8
    • Jakob Botsch Nielsen's avatar
      Refactor to remove compute_block_reward · e7245511
      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
      e7245511
  18. 17 Jun, 2019 1 commit
  19. 14 Jun, 2019 2 commits
  20. 13 Jun, 2019 1 commit
  21. 11 Jun, 2019 1 commit
  22. 10 Jun, 2019 1 commit