Commit f28b0d60 authored by Jakob Botsch Nielsen's avatar Jakob Botsch Nielsen
Browse files

Fix file links

parent 795517a7
Pipeline #12857 passed with stage
in 5 minutes and 39 seconds
...@@ -3,36 +3,36 @@ This repo is a formalization of execution layers of modern blockchains in Coq. ...@@ -3,36 +3,36 @@ This repo is a formalization of execution layers of modern blockchains in Coq.
## Structure of the project ## Structure of the project
The best place to start exploring the project is in The best place to start exploring the project is in
[Blockchain.v](Blockchain.v). Here we define the basic types describing [Blockchain.v](theories/Blockchain.v). Here we define the basic types describing
blockchains, smart contracts and the semantics of the execution layer of blockchains, smart contracts and the semantics of the execution layer of
blockchains. We give proofs of some interesting general lemmata here as well, blockchains. We give proofs of some interesting general lemmata here as well,
for instances that undeployed contracts cannot have sent out any transactions. for instances that undeployed contracts cannot have sent out any transactions.
We also define a typeclass that captures what it means to satisfy We also define a typeclass that captures what it means to satisfy our semantics.
our semantics. We exhibit two instances of this typeclass in We exhibit two instances of this typeclass in
[LocalBlockchain.v](LocalBLockchain.v): one with depth-first execution order of [LocalBlockchain.v](theories/LocalBlockchain.v): one with depth-first execution
smart contracts, and one with breadth-first execution order. order of smart contracts, and one with breadth-first execution order.
In [Circulation.v](Circulation.v) we prove a small sanity check for our In [Circulation.v](theories/Circulation.v) we prove a small sanity check for our
semantics. Specifically we prove that the total sum of the money in the system semantics. Specifically we prove that the total sum of the money in the system
is equal to the sum of the rewards handed out in blocks. is equal to the sum of the rewards handed out in blocks.
In [Congress.v](Congress.v) we implement the _Congress_ contract, a In [Congress.v](theories/Congress.v) we implement the _Congress_ contract, a
simplified version of the DAO, which does complex dynamic interactions with the simplified version of the DAO, which does complex dynamic interactions with the
blockchain and other contracts deployed on the blockchain. We specify blockchain and other contracts deployed on the blockchain. We specify and prove
and prove a property about this contract at the end of this file. This property a property about this contract at the end of this file. This property is
is somewhat related to reentrancy in that it caps the number of transactions the somewhat related to reentrancy in that it caps the number of transactions the
Congress will make. Congress will make.
In [Congress_Buggy.v](Congress_Buggy.v) we try something different: we take the In [Congress_Buggy.v](theories/Congress_Buggy.v) we try something different: we
same contract as above, but introduce a reentrancy issue into it. We then take the same contract as above, but introduce a reentrancy issue into it. We
formally prove that this version of the Congress does _not_ satisfy the property then formally prove that this version of the Congress does _not_ satisfy the
proven for the other version. This is proven by using one of our implementations property proven for the other version. This is proven by using one of our
of our semantics and just asking Coq to compute. implementations of our semantics and just asking Coq to compute.
In [LocalBlockchainTests.v](LocalBlockchainTests.v) we test that Coq is able to In [LocalBlockchainTests.v](theories/LocalBlockchainTests.v) we test that Coq is
compute with the Congress by deploying it and interacting with it using one of able to compute with the Congress by deploying it and interacting with it using
our implementations of blockchains. one of our implementations of blockchains.
## Building/Developing ## Building/Developing
This repo uses the std++ library. This must be installed first and can be This repo uses the std++ library. This must be installed first and can be
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment