Fixes and formatting in README files

README.md

@@ -13,7 +13,6 @@ ConCert can find real-world attacks as explained
 
 ## How to build
 
-
 Our development works with Coq 8.17 and depends on MetaCoq, and std++.
 The tests depend on QuickChick.
 The dependencies can be installed through `opam`.
@@ -47,25 +46,38 @@ Each folder contains a separate README file with more details.
 The [embedding](embedding/) folder contains the development of the verified embedding of ``λsmart`` to Coq.
 
 The [execution](execution/) folder contains the formalization of the smart
-contract execution layer, which allows reasoning about, and property-based testing of, interacting contracts. The [test](execution/test) folder contains the property-based testing framework. The key generators used for automatically generating blockchain execution traces for testing can be found in [TraceGens.v](execution/test/TraceGens.v). The testing framework was developed as part of a Master's Thesis at Aarhus University, and the thesis detailing (an earlier state of) the development can be found [here](https://github.com/mikkelmilo/ConCert-QuickChick-Testing-Thesis).
+contract execution layer, which allows reasoning about interacting contracts, and perform property-based testing.
+The [test](execution/test) folder contains the property-based testing framework.
+The key generators used for automatically generating blockchain execution traces for
+testing can be found in [TraceGens.v](execution/test/TraceGens.v).
+The testing framework was developed as part of a Master's Thesis at Aarhus University,
+and the thesis detailing (an earlier state of) the development can be found
+[here](https://github.com/mikkelmilo/ConCert-QuickChick-Testing-Thesis).
 
 The [extraction](extraction/) folder contains an extraction pipeline for smart contract languages.
-Currently, we support smart contract languages Liquidity and CameLIGO, and general-purpose languages Elm and Rust as targets.
-Pretty-printers to these languages are implemented directly in Coq.
-One also can obtain an OCaml plugin for Coq by extracting our pipeline using the standard extraction of Coq (currently, it is possible for extraction to Rust).
+Currently, we support smart contract languages Liquidity and CameLIGO, and general-purpose
+languages Elm and Rust as targets. Pretty-printers to these languages are implemented directly in Coq.
+One also can obtain an OCaml plugin for Coq by extracting our pipeline using the standard
+extraction of Coq (currently, it is possible for extraction to Rust).
 
-The [examples](examples/) folder contains examples of smart contract implementations, embedding, extraction, and tests. Extracted smart contracts can be found [here](https://github.com/AU-COBRA/extraction-results).
+The [examples](examples/) folder contains examples of smart contract implementations,
+embedding, extraction, and tests. Extracted smart contracts can be found
+[here](https://github.com/AU-COBRA/extraction-results).
 
 ## Notes for developers
 
-The project consists of four subprojects: `embedding`, `execution`, `extraction`, and `examples` located in the corresponding folders.
+The project consists of four subprojects: `embedding`, `execution`, `extraction`,
+and `examples` located in the corresponding folders.
 Each subproject has its own `_CoqProject` file and `Makefile`.
 The `Makefile` in the root folder dispatches the calls to the corresponding subproject.
 
 ## Documentation
 
-The [project documentation in HTML format](https://au-cobra.github.io/ConCert/toc.html) is generated for each build.
-We use the standard Coqdoc with improved styles and scripts of [CoqdocJS](https://github.com/tebbi/coqdocjs) ([license](extra/resources/coqdocjs/LICENSE)) and local table of contents by [TOC](https://github.com/jgallen23/toc)([license](extra/resources/toc/LICENSE)).
+The [project documentation in HTML format](https://au-cobra.github.io/ConCert/toc.html)
+is generated for each build. We use the standard Coqdoc with improved styles and scripts of
+[CoqdocJS](https://github.com/tebbi/coqdocjs) ([license](extra/resources/coqdocjs/LICENSE))
+and local table of contents by
+[TOC](https://github.com/jgallen23/toc)([license](extra/resources/toc/LICENSE)).
 
 ## Papers
 - ["Extracting functional programs from Coq, in Coq"](https://arxiv.org/abs/2108.02995).

embedding/README.md

@@ -14,14 +14,14 @@ expression to PCUIC terms, proof of soundness and various auxiliary lemmas for
 that proof.
 * [examples/](examples/) contains examples of smart contract
 verification: verification of ``Acorn`` list
-functions, integration with the execution framework.
+functions, and integration with the blockchain execution framework.
 
 * [examples/Demo.v](examples/Demo.v) contains a demonstration
 using our framework to write definitions using the deep embedding, convert them
 to Coq functions, compute with the interpreter and prove simple properties using
 the shallow embedding.
 
 * [examples/ExecFrameworkIntegration.v](../examples/crowdfunding/ExecFrameworkIntegration.v)
-is an "end-to-end" example of writing a contract in ``λsmart``, translating it
-to Gallina, and integrating it with the execution framework to prove safety
+is an "end-to-end" example of writing a smart contract in ``λsmart``, translating it
+to Gallina, and integrating it with the execution framework and proving safety
 properties about it.

examples/dexter2/README.md

@@ -1,26 +1,31 @@
 # Dexter 2
 
-Formalization of the Dexter 2 decentralized exchange based on the informal spec https://gitlab.com/dexter2tz/dexter2tz/-/tree/1713941489e0e646b632b42017a041c59158b6fb/docs/informal-spec
+Formalization of the Dexter 2 decentralized exchange based on the informal spec
+https://gitlab.com/dexter2tz/dexter2tz/-/tree/1713941489e0e646b632b42017a041c59158b6fb/docs/informal-spec
 
 The development consists of the following parts.
 
 ## Dexter 2 Liquidity Token
 
-This contract is an extension of a basic FA1.2 token contract with an extra entrypoint that allows an admin to mint and burn tokens.
+This contract is an extension of a basic FA1.2 token contract with an extra entrypoint
+that allows an admin to mint and burn tokens.
 The purpose of this contract is to keep track of ownership of the exchanges funds.
 
 [Dexter2FA12.v](Dexter2FA12.v) contains the implementation of the token.
 
-[Dexter2FA12Correct.v](Dexter2FA12Correct.v) contains proofs of functional correctness properties and proofs of invariants required for inter-contract communication proofs.
+[Dexter2FA12Correct.v](Dexter2FA12Correct.v) contains proofs of functional correctness
+properties and proofs of invariants required for inter-contract communication proofs.
 
 ## Dexter 2 CPMM
 
-This contract is an implementation of a Constant Product Market Maker (CPMM), the main Dexter 2 functionality.
+This contract is an implementation of a Constant Product Market Maker (CPMM),
+the main Dexter 2 functionality.
 
 [Dexter2CPMM.v](Dexter2CPMM.v) contains the implementation of the exchange.
 
-[Dexter2CPMMCorrect.v](Dexter2CPMMCorrect.v) contains proofs of functional correctness properties and proofs of inter-contract invariants.
+[Dexter2CPMMCorrect.v](Dexter2CPMMCorrect.v) contains proofs of functional correctness
+properties and proofs of inter-contract invariants.
 
-# Code extraction to CameLIGO
+## Code extraction to CameLIGO
 
 See [the extraction setup](Dexter2Extract.v)

execution/README.md

@@ -10,15 +10,15 @@ for instance that undeployed contracts cannot have sent out any transactions.
 We also provide a custom induction principle for proving properties involving
 the executions layer. It helps to simplify proofs by reducing the boilerplate
 code. See applications of the induction principle in the [example
-contracts](examples).
+contracts](../examples).
 
 We also define a typeclass that captures what it means to satisfy our semantics.
 We exhibit two instances of this typeclass in
-[LocalBlockchain.v](theories/LocalBlockchain.v); these are essentially
+[LocalBlockchain.v](test/LocalBlockchain.v); these are essentially
 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](examples/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
 is equal to the sum of the rewards handed out in blocks.
 

extra/extraction-results.md

@@ -1,16 +1,21 @@
 # ConCert Extraction Results
-This repository contains source code of programs extracted from Coq using the [ConCert](https://github.com/AU-COBRA/ConCert) framework.
+This repository contains source code of programs extracted from Coq using
+the [ConCert](https://github.com/AU-COBRA/ConCert) framework.
 
 The programs were written in Coq, verified and extracted to several languages using verified code extraction.
 The original programs can be found [here](https://github.com/AU-COBRA/ConCert/tree/master/examples).
 
 ## Structure of the project
 Each folder contain extracted programs for a specific language.
 
-* [cameligo-extract](cameligo-extract/tests) contains smart contracts extracted to the CameLIGO smart contract language for the Tezos blockchain.
-* [concordium-extract](concordium-extract) contains smart contracts extracted to the smart contract language for the Concordium blockchain.
+* [cameligo-extract](cameligo-extract/tests) contains smart contracts extracted to
+   the CameLIGO smart contract language for the Tezos blockchain.
+* [concordium-extract](concordium-extract) contains smart contracts extracted to the smart
+   contract language for the Concordium blockchain.
 * [elm-extract](elm-extract/tests) contains test programs extracted to Elm.
 * [elm-wev-extract](elm-web-extract/src) contains a simple web application extracted to Elm.
-* [liquidity-extract](liquidity-extract/tests) contains smart contracts extracted to the Liquidity smart contract language for the Dune blockchain.
-* [midlang-extract](midlang-extract/tests) contains smart contracts extracted to the Midlang smart contract language.
+* [liquidity-extract](liquidity-extract/tests) contains smart contracts extracted to the
+   Liquidity smart contract language for the Dune blockchain.
+* [midlang-extract](midlang-extract/tests) contains smart contracts extracted to the Midlang
+   smart contract language.
 * [rust-extract](rust-extract) contains programs extracted to Rust.