Translation

Ursus supports bidirectional translation between smart contract languages, enabling migration of existing contracts and code reuse.

Overview

Translation allows you to:

Import existing Solidity/C++ contracts into Ursus
Verify imported contracts formally
Extract verified contracts back to target languages

Supported Translations

Solidity ↔ Ursus

Convert between Solidity and Ursus:

Solidity → Ursus: Import Solidity contracts

Parse Solidity source code
Generate Ursus definitions
Preserve semantics and structure

Ursus → Solidity: Extract to Solidity

Generate Solidity from verified Ursus
Maintain type safety
Optimize for gas efficiency

C++ → Ursus

Convert TON C++ contracts to Ursus: C++ Translation

Import TON C++ contracts
Map to Ursus semantics
Enable formal verification

Translation Workflow

┌─────────────────┐
│ Existing Code   │
│ (Solidity/C++)  │
└────────┬────────┘
         │
         ▼
┌─────────────────┐
│   Translate     │
│   to Ursus      │
└────────┬────────┘
         │
         ▼
┌─────────────────┐
│ Ursus Contract  │
│ (Verifiable)    │
└────────┬────────┘
         │
         ├──────────┬──────────┐
         ▼          ▼          ▼
    Verify     Modify     Extract
    (Proofs)   (Enhance)  (Deploy)

Use Cases

1. Verify Existing Contracts

Import and verify deployed contracts:

# Import Solidity contract
ursus-translate --from solidity --to ursus ERC20.sol

# Verify properties
coqc ERC20.v
# Prove correctness

2. Migrate to Ursus

Gradually migrate codebase:

# Translate contracts one by one
ursus-translate Token.sol
ursus-translate TokenSale.sol
ursus-translate Vesting.sol

3. Cross-Platform Development

Develop once, deploy everywhere:

(* Write in Ursus *)
Contract MyContract ;

(* Extract to multiple targets *)
#[language = solidity]  (* For Ethereum *)
#[language = cpp]       (* For TON *)
#[language = rust]      (* For Solana *)

Translation Quality

Semantic Preservation

Ursus translation preserves:

✅ Type safety - All types are preserved
✅ Control flow - Logic remains identical
✅ State transitions - Behavior is equivalent
✅ Function signatures - Interfaces match

Limitations

Some features may require manual adjustment:

⚠️ Inline assembly - Not directly translatable
⚠️ Low-level calls - May need abstraction
⚠️ Platform-specific features - Require adaptation

Translation Tools

Command-Line Tool

# Solidity to Ursus
ursus-translate --from solidity --to ursus Contract.sol

# C++ to Ursus
ursus-translate --from cpp --to ursus Contract.cpp

# Ursus to Solidity
ursus-translate --from ursus --to solidity Contract.v

Programmatic API

Require Import UrsusTranslation.

(* Import Solidity *)
Import Solidity "ERC20.sol" as ERC20.

(* Use imported contract *)
Contract MyToken ;
Inherits ERC20 ;

Best Practices

Before Translation

Clean code - Remove unused code
Document - Add comments for complex logic
Test - Ensure original code works
Backup - Keep original source

During Translation

Review output - Check generated Ursus code
Fix warnings - Address translation warnings
Test equivalence - Verify behavior matches
Add specifications - Write formal properties

After Translation

Verify - Prove correctness properties
Optimize - Improve generated code
Document - Explain verification
Test - Run comprehensive tests

Examples

Simple ERC20 Translation

Original Solidity:

contract ERC20 {
    mapping(address => uint256) public balances;

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

Generated Ursus:

Contract ERC20 ;
Sends To ;
Types ;
Constants ;

Record Contract := {
    balances: mapping address uint256
}.

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

Next Steps

Solidity → Ursus - Import Solidity contracts
C++ → Ursus - Import TON contracts
Ursus → Solidity - Extract to Solidity
Verification - Verify translated contracts

URSUS language Documentation