Add file headers

theories/Automation.v

+(* This file implements various helper tactics *)
+
 From Coq Require Import Eqdep List Omega Permutation.
 Import ListNotations.
 
@@ -65,6 +67,7 @@ Local Ltac perm_simplify_round :=
     | [H: Permutation ?l1 ?l2|-_] => rewrite H
     end.
 
+(* Automatically tries to solve obvious "Permutation x y" goals. *)
 Ltac perm_simplify :=
   repeat perm_simplify_round;
   cbn;

theories/Blockchain.v

+(* This file defines blockchains, both a contract's view (which is
+more computational) and the semantics of executing smart contracts
+in a blockchain.
+
+The most important types are:
+
+* The ChainBase type, describing basic assumptions made of any blockchain.
+In most cases we will abstract over this type.
+
+* The Chain type, describing a smart contract's view of the blockchain.
+This is the the data that can be accessed by smart contracts.
+
+* The Action type, describing how smart contracts (and external users)
+interact with the blockchain. We allow transfers, calls and deployment
+of contracts.
+
+* The WeakContract type, describing a "weak" or "stringly" typed
+version of smart contracts. Contracts are just two functions init and
+receive to respectively initialize state on deployment and to update
+state when receiving messages. The weak version of contracts means that
+the state/message/setup types, which would normally vary with contracts,
+are stored in a serialized format.
+
+* The Contract type, describing a more strongly typed version of a contract.
+This is the same as the above except we abstract over the appropriate types.
+Users of the framework will mostly need to deal with this.
+
+The next types deal with semantics.
+
+* The Environment type. This augments the Chain type with more information.
+Environment can be thought of as the information that a realistic blockchain
+implementation would need to keep track of to implement operations. For instance,
+it is reasonable to assume that an implementation needs to access the state of
+contracts, but not to assume that it needs to store the full transaction history
+of all addresses.
+
+* The ActionEvaluation type. This specifies how to evaluate actions returned by
+contracts or input in blocks. This related an environment and action to a new
+environment and list of new actions to execute.
+
+* The ChainState type. This augments the Environment type with a queue of
+"outstanding" actions that need to be executed. For instance, when a block is
+added, its actions are put into this queue.
+
+* The ChainStep type. This specifies how the blockchain should execute smart
+contracts, and how new blocks are added. It relates a ChainState to a new ChainState.
+There are steps to allow adding blocks, evaluating actions in the queue and to
+permute the queue (allowing to model any execution order).
+
+* The ChainTrace type. This just represents a sequence of steps. If a trace ends
+in a state it means that state is reachable and there is a "semantically correct"
+way of executing to get to this state. This type records the full history of a
+blockchain's execution and it would thus be unrealistic to extract.
+
+* The ChainBuilderType type. This is a typeclass for implementations of blockchains,
+where these implementations need to prove that they satisfy our semantics.
+
+*)
+
+
 From Coq Require Import Arith ZArith.
 From Coq Require Import List.
 From Coq Require Import Psatz.

theories/ChainedList.v

-(* This file implements a chained list. This is a list for which
-each element is a link between a from and to element of a provided
-"link" type. That is, each link (element) has a "from" point that
-must match the previous element's "to" point. For that reason this is
-also a snoc list. Note that this is not unlike fhlist from CPDT,
-except we place further restrictions on it. *)
+(* This file implements a 'chained list'. This can essentially be
+thought of as the proof-relevant transitive reflexive closure of
+a relation. That is, each link (element) has a "from" point that
+must match the previous element's "to" point. *)
 From SmartContracts Require Import Automation.
 Section ChainedList.
 Context {Point : Type} {Link : Point -> Point -> Type}.

theories/Circulation.v

-(* In this file we prove various results about the circulation of coins in any
-chain implementing a chain type. More specifically, we show that the circulation
-does not change during execution of blocks. This is proven under the (implicit)
-assumption that the address space is finite. *)
+(* In this file we prove that the circulation of any blockchain implementing our
+semantics is as expected: the sum of all rewards paid out in blocks. *)
 From Coq Require Import List Permutation ZArith Psatz Morphisms.
 From SmartContracts Require Import Automation Blockchain Extras Finite ChainedList.
 From RecordUpdate Require Import RecordSet.
@@ -15,11 +13,12 @@ Local Open Scope Z.
 Definition circulation (chain : Chain) :=
   sumZ (account_balance chain) (elements Address).
 
-(* We then prove that over any single action, the circulation is preserved.
+(* We prove first that over any single action, the circulation is preserved.
 The idea behind this proof is that addrs contain from and to so
 we can move them to the beginning of the sum and it easily follows that
 the sum of their balances is the same as before. For the rest of the
 list the total balance will then not be affected which follows by induction. *)
+
 Lemma address_reorganize {a b : Address} :
   a <> b ->
   exists suf, Permutation ([a; b] ++ suf) (elements Address).
@@ -101,6 +100,8 @@ Proof.
   end.
 Qed.
 
+(* Now we prove that adding a block _does_ increase the circulation
+by what we would expect. *)
 Lemma circulation_add_new_block header env :
   circulation (add_new_block_to_env header env) =
   (circulation env + block_reward header)%Z.
@@ -131,6 +132,7 @@ Proof.
   lia.
 Qed.
 
+(* We then get a lemma over steps *)
 Lemma step_circulation {prev next} (step : ChainStep prev next) :
   circulation next =
   match step with
@@ -148,6 +150,7 @@ Proof.
     intuition.
 Qed.
 
+(* And combining these gives the final result. *)
 Theorem chain_trace_circulation
         {state : ChainState}
         (trace : ChainTrace empty_state state) :

theories/Congress.v

+(* In this file we implement a Congress and prove it correct up to a
+specification. The Congress is a simplified version of the DAO in
+which members vote on proposals. We implement the contract in Gallina
+and then show that it does not send out more transactions than
+expected from the number of created proposals. *)
+
 From Coq Require Import ZArith.
 From Coq Require Import Morphisms.
 From Coq Require Import Psatz.

theories/Congress_Buggy.v

+(* In this file we introduce a reentrancy problem in the Congress
+contract described in Congress.v. We then use one of our blockchain
+implementations (the depth first local block chain) to prove that this
+version can send out too many transactions. This is done by
+constructing a contract that actually exploits this version of the
+Congress and then just asking Coq to compute. *)
+
 From Coq Require Import ZArith.
 From Coq Require Import Morphisms.
 From Coq Require Import Psatz.

theories/Containers.v

+(* This file provides an interface for std++'s finite maps *)
+
 From Coq Require Import List.
 From Coq Require Import ZArith.
 From Coq Require Import Permutation.

theories/Extras.v

+(* This file implements various helper functions and proofs *)
+
 From Coq Require Import ZArith.
 From Coq Require Import List.
 From Coq Require Import Permutation.

theories/Finite.v

+(* This file captures what it means for a type to be finite *)
+
 From Coq Require Import List.
 Import ListNotations.
 

theories/LocalBlockchain.v

+(* This file gives two different implementations of the blockchain
+execution layer defined in Blockchain.v. Both versions are execution
+layers using std++'s finite maps and are thus relatively
+efficient. They differ in execution order: one uses a depth-first
+execution order, while the other uses a breadth-first execution order. *)
+
 From Coq Require Import ZArith.
 From Coq Require Import Permutation.
 From Coq Require Import Morphisms.

theories/LocalBlockchainTests.v

+(* This file computes with the Congress and an actual blockchain
+implementation, showing that everything computes from within Coq. It
+also contains specializations of the results proven in Congress.v to
+our particular implementations of blockchains. *)
+
 From SmartContracts Require Import Monads.
 From SmartContracts Require Import Blockchain.
 From SmartContracts Require Import LocalBlockchain.

theories/Monads.v

+(* This file defines some helpful notations for the option monad. *)
+
 Definition option_bind {A B : Type} (v : option A) (f : A -> option B) : option B :=
   match v with
   | Some val => f val

theories/Serializable.v

+(* This file defines a common storage format for countable types.
+This format, SerializedValue, is either a unit/int/bool or a pair/list
+of these. We also define Serializable as a type class capturing that a
+type can be converted from and to this format. *)
+
 From Coq Require Import ZArith.
 From SmartContracts Require Import Monads.
 From SmartContracts Require Import Containers.