C++ → Ursus Translation

This guide explains how to translate TON C++ contracts to Ursus for formal verification.

Overview

TON smart contracts are typically written in C++ and compiled to TVM bytecode. Translating them to Ursus enables:

• Formal verification of TON contracts
• Proving correctness properties
• Finding bugs through proof attempts
• Generating verified implementations

TON C++ vs Ursus

Key Differences

Translation Process

Manual Translation Steps

1. Analyze C++ contract
2. Create Ursus contract structure
3. Translate state variables
4. Translate functions
5. Add TVM-specific features
6. Add verification

Example Translation

Original TON C++

#include <tvm/contract.hpp>
#include <tvm/smart_switcher.hpp>

class SimpleWallet {
public:
    uint128 balance_;
    address owner_;

    __always_inline
    void constructor(address owner) {
        owner_ = owner;
        balance_ = 0;
    }

    __always_inline
    uint128 getBalance() {
        return balance_;
    }

    __always_inline
    void transfer(address to, uint128 amount) {
        require(balance_ >= amount, 101);
        balance_ -= amount;
        // Send message to 'to'
    }
};

Translated Ursus

Require Import UrsusEnvironment.Solidity.current.Environment.
Require Import Solidity.TVM.EverBase.

#[translation = on]
#[language = cpp]
Contract SimpleWallet ;
Sends To ;
Inherits ;

Record Contract := {
    #[static] _persistent_contract_data: PersistentContractDataLRecord;
    balance: uint128;
    owner: address
}.

SetUrsusOptions.
Local Open Scope usolidity_scope.

Ursus Definition constructor (owner_arg: address):
  UExpression unit false.
{
    ::// owner := owner_arg .
    ::// balance := {0} |.
}
return.
Defined.
Sync.

#[public, view]
Ursus Definition getBalance: UExpression uint128 false.
{
    ::// _result := balance |.
}
return.
Defined.
Sync.

#[public]
Ursus Definition transfer (to: address) (amount: uint128):
  UExpression unit true.
{
    ::// require_(balance >= amount, {101}) .
    ::// balance := balance - amount |.
    (* Send message to 'to' *)
}
return.
Defined.
Sync.

EndContract ImplementsAuto.

Translation Mappings

Types

TVM-Specific Types

Function Attributes

Control Flow

TVM-Specific Features

Persistent Contract Data

TON contracts require persistent contract data:

Record Contract := {
    #[static] _persistent_contract_data: PersistentContractDataLRecord;
    (* other fields *)
}.

Message Handling

C++:

void onMessage(cell msg) {
    // Handle message
}

Ursus:

Ursus Definition onMessage (msg: cell_): UExpression unit false.
{
    (* Handle message *)
}
return.
Defined.

Cell Operations

C++:

cell c = begin_cell()
    .store_uint(value, 256)
    .end_cell();

Ursus:

::// var 'c : cell_ := build_cell(store_uint({256}, value)) |.

Slice Operations

C++:

slice s = c.begin_parse();
uint256 value = s.load_uint(256);

Ursus:

::// var 's : slice_ := begin_parse(c) .
::// var 'value : uint256 := load_uint(s, {256}) |.

Complex Patterns

Dictionary (Mapping)

C++:

dict<address, uint128> balances;
balances[addr] = 100;
uint128 bal = balances[addr];

Ursus:

balances: mapping address uint128

::// balances[[addr]] := {100} .
::// var 'bal : uint128 := balances[[addr]] |.

Optional Values

C++:

optional<uint256> maybeValue;
if (maybeValue.has_value()) {
    uint256 val = maybeValue.value();
}

Ursus:

maybeValue: optional uint256

::// match maybeValue with
     | Some val => { ->> }
     | None => { ->> }
     end |.
{
    (* Use val *)
}
{
    (* Handle None *)
}

Message Sending

C++:

tvm_sendmsg(to, value, msg_body);

Ursus:

::// send_message(to, value, msg_body) |.

TON-Specific Patterns

Constructor with Replay Protection

C++:

void constructor() {
    require(!initialized_, 100);
    initialized_ = true;
    owner_ = msg.sender;
}

Ursus:

Ursus Definition constructor: UExpression unit true.
{
    ::// require_(!initialized, {100}) .
    ::// initialized := @true .
    ::// owner := msg->sender |.
}
return.
Defined.

Internal Message Handler

C++:

void onInternalMessage(cell msg) {
    slice s = msg.begin_parse();
    uint32 op = s.load_uint(32);

    if (op == 1) {
        handleTransfer(s);
    }
}

Ursus:

Ursus Definition onInternalMessage (msg: cell_): UExpression unit false.
{
    ::// var 's : slice_ := begin_parse(msg) .
    ::// var 'op : uint32 := load_uint(s, {32}) .
    ::// if op == {1} then { ->> } |.
    {
        ::// handleTransfer(s) |.
    }
}
return.
Defined.

Translation Challenges

1. Low-Level TVM Operations

Some TVM operations may not have direct Ursus equivalents and require custom implementation.

2. Cell Serialization

Complex cell serialization logic needs careful translation.

3. Gas Management

Gas calculations in C++ must be translated to Ursus gas model.

4. Replay Protection

TON-specific replay protection patterns need proper translation.

Verification After Translation

After translation, add specifications and proofs:

(* Specification *)
Definition transfer_spec (from to: address) (amount: uint128)
                         (s s': ContractState) : Prop :=
  balance s' = balance s - amount.

(* Proof *)
Theorem transfer_correct:
  forall from to amount s s',
    exec_transfer from to amount s = Some s' ->
    transfer_spec from to amount s s'.
Proof.
  (* Proof steps *)
Qed.

TVM Library Support

Ursus provides TVM-specific libraries:

Require Import Solidity.TVM.EverBase.
Require Import Solidity.TVM.ContractTVM.

These libraries provide:

• TVM primitive operations
• Cell/slice/builder operations
• Message handling
• Gas management

See Also

• Translation Overview - Translation system overview
• TVM Functions - TVM-specific functions
• Contract Structure - Contract organization
• Verification - Formal verification