Ursus → Solidity Translation

This guide explains how to translate Ursus contracts to Solidity code using the Ursus code generator.

Overview

The Ursus → Solidity translation process:

1. Write contract in Ursus (Coq)
2. Mark contract for translation with attributes
3. Compile with coqc
4. Generated Solidity code is produced automatically

Contract Attributes

Required Attributes

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

Attributes:

• #[translation = on] - Enable code generation
• #[language = solidity] - Target Solidity output

Optional Attributes

#[quickchick = off]
#[Contract = MyContract]

• #[quickchick = off] - Disable QuickChick testing
• #[Contract = Name] - Specify contract name

Complete Example

Ursus Source

Require Import UrsusEnvironment.Solidity.current.Environment.

#[translation = on]
#[quickchick = off]
#[language = solidity]
Contract SimpleToken ;
Sends To ;
Inherits ;

Record Contract := {
    totalSupply: uint256;
    balances: mapping address uint256;
    owner: address
}.

SetUrsusOptions.
Local Open Scope usolidity_scope.

#[public]
Ursus Definition balanceOf (account: address): UExpression uint256 false.
{
    ::// _result := balances[[account]] |.
}
return.
Defined.
Sync.

#[public]
Ursus Definition transfer (to: address) (amount: uint256):
  UExpression boolean false.
{
    ::// balances[[msg->sender]] := balances[[msg->sender]] - amount .
    ::// balances[[to]] := balances[[to]] + amount .
    ::// _result := @true |.
}
return.
Defined.
Sync.

EndContract ImplementsAuto.

Generated Solidity

pragma solidity ^0.8.0;

contract SimpleToken {
    uint256 public totalSupply;
    mapping(address => uint256) public balances;
    address public owner;

    function balanceOf(address account) public view returns (uint256) {
        return balances[account];
    }

    function transfer(address to, uint256 amount) public returns (bool) {
        balances[msg.sender] = balances[msg.sender] - amount;
        balances[to] = balances[to] + amount;
        return true;
    }
}

Translation Process

Step 1: Prepare Contract

Ensure contract has proper attributes:

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

Step 2: Compile

coqc -Q . MyProject MyContract.v

Step 3: Locate Generated Code

Generated Solidity files are typically placed in:

• Same directory as .v file
• Or in configured output directory

Expected files:

• MyContract.sol - Solidity source
• MyContract.abi.json - Contract ABI (if enabled)

Translation Mappings

Types

Function Attributes

Operators

State Access

EndContract Modes

ImplementsAuto

Automatically generates interface implementations:

EndContract ImplementsAuto.

Generates all required interface methods automatically.

Implements

Manual interface implementation:

EndContract Implements.

You must implement all interface methods manually.

No Interfaces

Simple contract without interfaces:

EndContract.

Advanced Features

Custom Types

Ursus:

Types
Record UserInfo := {
    balance: uint256;
    lastUpdate: uint256
}
;

Generated Solidity:

struct UserInfo {
    uint256 balance;
    uint256 lastUpdate;
}

Enumerations

Ursus:

Types
Inductive Status :=
    | Active
    | Paused
    | Stopped
;

Generated Solidity:

enum Status {
    Active,
    Paused,
    Stopped
}

Events

Ursus:

::// emit Transfer(from, to, amount) |.

Generated Solidity:

emit Transfer(from, to, amount);

Compilation Options

Using dune

If project uses dune build system:

dune build

Using Makefile

If project has Makefile:

make

Manual Compilation

coqc -Q . MyProject \
     -R ../ursus-standard-library/src Solidity \
     MyContract.v

Verification Before Translation

Always verify contract before translation:

# Check compilation
coqc MyContract.v

# Run proofs
coqc MyContractProofs.v

# Run QuickChick tests (if enabled)
coqc MyContractTests.v

See Also

• Compilation Guide - Detailed compilation instructions
• Translation Overview - Translation system overview
• Contract Structure - Contract organization
• Attributes - Function attributes