Compiling Ursus Contracts

This guide explains how to compile Ursus contracts and extract them to target languages (Solidity, C++, or Rust).

Prerequisites

Before compiling, ensure you have:

• Coq installed (version 8.13 or later)
• Ursus libraries installed via opam
• Your contract file (.v extension)

See Installation for setup instructions.

Basic Compilation

Step 1: Compile with Coq

Compile your Ursus contract using coqc:

coqc -Q . MyProject MyContract.v

Options:

• -Q . MyProject - Maps current directory to logical path MyProject
• -R can be used instead of -Q for recursive mapping

Example:

coqc -Q . TokenContracts ERC20.v

Step 2: Verify Compilation

Successful compilation produces:

• MyContract.vo - Compiled object file
• MyContract.vok - Verification certificate
• MyContract.glob - Global symbol table

Check for errors:

coqc MyContract.v 2>&1 | grep -i error

Extraction to Target Languages

Ursus supports extraction to multiple target languages. The target language is specified in the contract attributes.

Extraction to Solidity

1. Set contract attributes:

#[translation = on]
#[language = solidity]
#[Contract = MyContract]
Contract MyContract ;

2. Compile with extraction:

coqc -Q . MyProject MyContract.v

3. Generated files:

• MyContract.sol - Solidity source code
• MyContract.abi.json - Contract ABI
• MyContract.bin - Compiled bytecode (if solc is available)

Extraction to C++

1. Set contract attributes:

#[translation = on]
#[language = cpp]
#[Contract = MyContract]
Contract MyContract ;

2. Compile:

coqc -Q . MyProject MyContract.v

3. Generated files:

• MyContract.cpp - C++ source code
• MyContract.hpp - Header file
• MyContract.tvc - TVM bytecode (if TON compiler is available)

Extraction to Rust

1. Set contract attributes:

#[translation = on]
#[language = rust]
#[Contract = MyContract]
Contract MyContract ;

2. Compile:

coqc -Q . MyProject MyContract.v

3. Generated files:

• MyContract.rs - Rust source code
• Cargo.toml - Cargo configuration (if not exists)

Using _CoqProject

For larger projects, use a _CoqProject file to manage compilation settings.

Create _CoqProject:

-Q . MyProject
-R ../ursus-standard-library Solidity
-R ../pruvendo-ursus-tvm TVM

MyContract.v
TokenSale.v
Vesting.v

Compile all files:

coq_makefile -f _CoqProject -o Makefile
make

Compilation Options

Disable Translation

To compile without generating target language code:

#[translation = off]
Contract MyContract ;

Use this for:

• Verification-only contracts
• Testing and development
• Proof-of-concept implementations

Enable QuickChick Testing

Generate property-based tests:

#[quickchick = on]
Contract MyContract ;

This generates:

• MyContract_test.v - QuickChick test suite
• Random test data generators
• Property verification tests

Troubleshooting

Common Errors

Error: "Cannot find library"

Error: Cannot find library Solidity.TVM.EverBase

Solution: Check your -Q or -R paths in _CoqProject

Error: "Extraction failed"

Error: Translation to solidity failed

Solution: Verify contract attributes and ensure #[translation = on]

Error: "Undefined reference"

Error: The reference fun01 was not found

Solution: Check function names and inheritance declarations

Verbose Output

Enable verbose compilation:

coqc -verbose MyContract.v

Debugging Extraction

Check generated intermediate files:

ls -la *.vo *.vok *.glob

Build Automation

Using Make

Create a Makefile:

.PHONY: all clean

COQC = coqc
COQFLAGS = -Q . MyProject

SOURCES = MyContract.v TokenSale.v

all: $(SOURCES:.v=.vo)

%.vo: %.v
	$(COQC) $(COQFLAGS) $<

clean:
	rm -f *.vo *.vok *.vos *.glob
	rm -f *.sol *.cpp *.rs

Build:

make

Using Dune

For projects using Dune build system:

Create dune file:

(coq.theory
 (name MyProject)
 (package my-contracts))

Build:

dune build

Next Steps

• Deploying Contracts - Deploy to blockchain
• Testing - Verify contract correctness
• Simple Example - Complete ERC20 example

See Also

• Contract Structure
• File Header
• Installation Guide