extraction

Extraction

Contains an implementation of extraction based on the certified erasure provided by MetaCoq. The theories folder contains the implementation and correctness theorems. The examples folder, as the name suggests, contains examples of smart contracts and programs extracted using our development. The tests folder contains tests for our extensions to the certified erasure.

After building the project (running make from the project's root, or running make in this folder), the folders tests/extracted-code/*-extract/ are populated with the extracted code.

The extraction can be tested (compiled and run for the targets that have tests). Use make test-extraction after the project is compiled. Note that running this step locally requires additional compilers installed (see below). Alternatively, the required compilers are available in the docker image aucobra/concert:deps-coq-8.11-with-compilers.

Compiling Liquidity code: install the Liquidity compiler. Alternatively, the Liquidity code can be run using the online IDE: https://www.liquidity-lang.org/

Compiling Elm code: install the Elm compiler. Running Elm tests also requires elm-explorations/test package (see the required dependencies in examples/elm-extract/elm.json)

Compiling Rust code with the Concordium infrastructure:

• requires cargo and the Rust compiler;
• download cargo-concordium: https://developer.concordium.software/en/mainnet/net/installation/downloads.html#cargo-concordium
• add the directory with cargo-concordium to PATH;
• install cargo;
• use cargo concordium test to build and run tests (if tests are available);
• read the details here: https://developer.concordium.software/en/mainnet/smart-contracts/guides/setup-tools.html#setup-tools

Extraction results

As part of the CI, the extraction results from the tests/extracted-code/*-extract/ directories are compiled (and tested, for the targets with tests). Moreover, the extracted source code is pushed to another repository https://github.com/AU-COBRA/extraction-resutls, so one can always browse through the code produced by the last successful build.

Some highlights from theories:

• ExAst.v -- An extension of the MetaCoq's certified erasure EAst data-structures with additional information about erased types.
• Erasure.v -- An extension of the MetaCoq's certified erasure with erasure for types and erasing only required dependencies. Also implements erasure for global environments with extra typing information for global definitions.
• ErasureCorrectness.v -- Correctness lemmas for definitions from Erasure.v, proving that our erasure produces a well-formed erased environment.
• Extraction.v -- High-level interface to extraction. Provides different pipelines for doing extraction with different trusted computing bases.
• ExtractionCorrectness.v -- Top-level correctness theorem relating the stages.
• Optimize.v -- Optimisations (dead argument elimination, logical parameters elimination) on λ□ terms.
• OptimizeCorrectness.v -- Correctness of optimisation (dead argument elimination).
• CertifyingEta.v -- An eta-expansion procedure.
• CertifyingInlinig.v -- An inlining procedure.
• CertifyingBeta.v -- A procedure that finds an evalues redexes (if the reduction leads to new redexes, these are not reduced further)
• Certifying.v -- proof-generating procedure; it is used to generate proofs after running inlining/eta-expansion/etc.
• LPretty.v -- Pretty-printer for Liquidity from λ□.
• Liquidity.v -- A pretty printer that works directly on the deep embedding of λsmart language.
• LiquidityExtract.v - A high-level interface to Liquidity extraction.
• MidlangExtract.v -- A high-level interface to Midlang extraction including the pretty-printer to Midlang/Elm.
• PrettyPrinterMonad.v -- A monad for implementing pretty-printing in Coq.

Some highlights of extracted examples:

• CounterCertifiedExtraction.v -- A simple counter contract.
• CounterDepCertifiedExtraction.v -- A counter contract that uses propositions to filter out the correct input. It also serves as an example application of the certifying eta-expansion.
• CounterRefinementTypes -- A counter contract that uses refinement types for expressing partial functional correctness.
• CrowdfundingCertifiedExtraction.v -- Machinery for extraction of a crowdfunding contract.
• ElmExtractTests.v -- Several examples of extraction into Elm.
• MidlangEscrow.v -- Extraction of the escrow contract defined in Escrow.v to Midlang.
• StackInterpreterExtract.v -- An interpreter for a simple stack-based language.