Commit 86b9f7c1 authored by Jakob Botsch Nielsen's avatar Jakob Botsch Nielsen
Browse files

Show the proven property immediately in the README

parent f28b0d60
Pipeline #13730 passed with stage
in 7 minutes and 28 seconds
...@@ -10,19 +10,33 @@ for instances that undeployed contracts cannot have sent out any transactions. ...@@ -10,19 +10,33 @@ for instances that undeployed contracts cannot have sent out any transactions.
We also define a typeclass that captures what it means to satisfy our semantics. We also define a typeclass that captures what it means to satisfy our semantics.
We exhibit two instances of this typeclass in We exhibit two instances of this typeclass in
[LocalBlockchain.v](theories/LocalBlockchain.v): one with depth-first execution [LocalBlockchain.v](theories/LocalBlockchain.v); these are essentially
order of smart contracts, and one with breadth-first execution order. implementations of execution layers of modern blockchains. One is implemented
with depth-first execution and the other with breadth-first execution order.
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
is equal to the sum of the rewards handed out in blocks.
In [Congress.v](theories/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 and prove blockchain and other contracts deployed on the blockchain. We specify and prove
a property about this contract at the end of this file. This property is a property about this contract at the end of this file. This property 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. The formal statement reads as follows:
```coq
Corollary congress_txs_after_block
{ChainBuilder : ChainBuilderType}
prev new header acts :
builder_add_block prev header acts = Some new ->
forall addr,
env_contracts new addr = Some (Congress.contract : WeakContract) ->
length (outgoing_txs (builder_trace new) addr) <=
num_acts_created_in_proposals (incoming_txs (builder_trace new) addr).
```
This is saying that, after adding a block, the number of transactions sent out
by any deployed Congress is capped by the number of actions that were created in
proposals up to this point. This is an approximation of the fact that any
outgoing transaction should correspond to some proposal created and discussed in
the past.
In [Congress_Buggy.v](theories/Congress_Buggy.v) we try something different: we In [Congress_Buggy.v](theories/Congress_Buggy.v) we try something different: we
take the same contract as above, but introduce a reentrancy issue into it. We take the same contract as above, but introduce a reentrancy issue into it. We
...@@ -30,9 +44,14 @@ then formally prove that this version of the Congress does _not_ satisfy the ...@@ -30,9 +44,14 @@ then formally prove that this version of the Congress does _not_ satisfy the
property proven for the other version. This is proven by using one of our property proven for the other version. This is proven by using one of our
implementations of our semantics and just asking Coq to compute. implementations of our semantics and just asking Coq to compute.
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
is equal to the sum of the rewards handed out in blocks.
In [LocalBlockchainTests.v](theories/LocalBlockchainTests.v) we test that Coq is In [LocalBlockchainTests.v](theories/LocalBlockchainTests.v) we test that Coq is
able to compute with the Congress by deploying it and interacting with it using able to compute with the Congress by deploying it and interacting with it using
one of our implementations of blockchains. one of our implementations of blockchains. We also specialize the proof shown
about to our actual implementations of the execution layer described above.
## 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
......
Markdown is supported
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