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.

The extraction framework currently supports four languages: CameLIGO, Liquidity, Rust and Elm.

Rust and Elm extraction have been moved to https://github.com/AU-COBRA/coq-rust-extraction and https://github.com/AU-COBRA/coq-elm-extraction

Extracting and compiling code

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-8.16.1-with-compilers.

Compiling LIGO code:

Install the LIGO compiler. The extraction pipeline is tested to work with v0.59.0 and targets the Kathmandu protocol.

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 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-results), so one can always browse through the code produced by the last successful build.

Extracted Smart Contracts

Contract\Language	Liquidity (Dune)	CameLIGO (Tezos)	Rust (Concordium)	MidLang
Counter (simple types)	yes	yes	yes
Counter (subset types)	yes	yes**		yes
Counter (Prop)	yes
ERC20 token	yes	yes	in progress***
Crowdfunding	yes	yes
DSL Interpreter	yes	yes	yes
Escrow	yes	yes	yes	yes
Boardroom voting	partially*	yes
Dexter2 CPMM (main)		yes	not yet****
Dexter2 FA1.2 (liquidity token)		yes	not yet****

*issue with typing of lambdas in liquidity (see OCamlPro/liquidity#264).

**[resolved] the issue with parametric types when extracting sig is resolved after the support for polymorphism was added to LIGO.

***issue with maps of maps (the values can be only by-reference, and this causes problems).

**** extracting the contracts should be doable, no map of maps issue as with ERC20. However, remapping of contract calls should be addressed, so far all the contracts extracted to Rust emit transfers only.

Some highlights of extracted examples:

• CounterCertifiedLiquidity.v -- A simple counter contract.
• CounterDepCertifiedLiquidity.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.
• EscrowMidlang.v -- Extraction of the escrow contract defined in Escrow.v to Midlang.
• StackInterpreterExtract.v -- An interpreter for a simple stack-based language.

Project structure

Part of the extraction pipeline have been moved to the MetaCoq project. The moved files are described here:

• 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 -- Optimizations (dead argument elimination, logical parameter elimination) on λ□ terms.
• OptimizeCorrectness.v -- Correctness of optimization (dead argument elimination).
• CertifyingEta.v -- An eta-expansion procedure.
• CertifyingInlinig.v -- An inlining procedure.
• CertifyingBeta.v -- A procedure that finds an evaluates 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.

The remaining of the project consists of

• LiquidityPretty.v -- Pretty-printer for Liquidity from λ□.
• LiquidityExtract.v -- A high-level interface to Liquidity extraction.
• CameLIGOPretty.v -- Pretty-printer for CameLIGO from λ□.
• CameLIGOExtract.v -- A high-level interface to CameLIGO extraction.
• ConcordiumExtract.v -- A high-level interface to Concordium extraction.
• PrettyPrinterMonad.v -- A monad for implementing pretty-printing in Coq.