Solidity → Ursus Translation

This guide explains how to translate existing Solidity contracts to Ursus for formal verification.

Overview

Translating Solidity to Ursus enables:

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

Translation Process

Manual Translation Steps

1. Analyze Solidity contract
2. Create Ursus contract structure
3. Translate state variables
4. Translate functions
5. Add verification

Example Translation

Original Solidity

pragma solidity ^0.8.0;

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

    constructor(uint256 _initialSupply) {
        owner = msg.sender;
        totalSupply = _initialSupply;
        balances[msg.sender] = _initialSupply;
    }

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

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

Translated Ursus

Require Import UrsusEnvironment.Solidity.current.Environment.

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

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

SetUrsusOptions.
Local Open Scope usolidity_scope.

Ursus Definition constructor (_initialSupply: uint256):
  UExpression unit false.
{
    ::// owner := msg->sender .
    ::// totalSupply := _initialSupply .
    ::// balances[[msg->sender]] := _initialSupply |.
}
return.
Defined.
Sync.

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

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

EndContract ImplementsAuto.

Translation Mappings

State Variables

Function Modifiers

Control Flow

Operators

Special Variables

Complex Patterns

Mappings

Solidity:

mapping(address => uint256) public balances;
balances[addr] = 100;
uint256 bal = balances[addr];

Ursus:

balances: mapping address uint256

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

Nested Mappings

Solidity:

mapping(address => mapping(address => uint256)) public allowances;
allowances[owner][spender] = amount;

Ursus:

allowances: mapping address (mapping address uint256)

::// allowances[[owner]][[spender]] := amount |.

Structs

Solidity:

struct User {
    uint256 balance;
    bool active;
}

User public user;
user.balance = 100;

Ursus:

Types
Record User := {
    balance: uint256;
    active: boolean
}
;

user: UserLRecord

::// user->User_ι_balance := {100} |.

Events

Solidity:

event Transfer(address indexed from, address indexed to, uint256 amount);
emit Transfer(msg.sender, to, amount);

Ursus:

::// emit Transfer(msg->sender, to, amount) |.

Modifiers

Solidity:

modifier onlyOwner() {
    require(msg.sender == owner, "Not owner");
    _;
}

function withdraw() public onlyOwner {
    // ...
}

Ursus:

Ursus Definition onlyOwner: UExpression unit true.
{
    ::// require_(msg->sender == owner, "Not owner") |.
}
return.
Defined.

Ursus Definition withdraw: UExpression unit true.
{
    ::// onlyOwner() .
    (* ... *)
}
return.
Defined.

Common Patterns

ERC20 Transfer

Solidity:

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

Ursus:

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

Approval Pattern

Solidity:

function approve(address spender, uint256 amount) public returns (bool) {
    allowances[msg.sender][spender] = amount;
    emit Approval(msg.sender, spender, amount);
    return true;
}

Ursus:

Ursus Definition approve (spender: address) (amount: uint256):
  UExpression boolean false.
{
    ::// allowances[[msg->sender]][[spender]] := amount .
    ::// emit Approval(msg->sender, spender, amount) .
    ::// _result := @true |.
}
return.
Defined.

Translation Challenges

1. Assembly Code

Solidity assembly cannot be directly translated. Must be reimplemented in Ursus or proven separately.

2. External Calls

External contract calls require interface definitions in Ursus.

3. Fallback Functions

Fallback and receive functions have special handling in Ursus.

4. Inheritance

Solidity inheritance must be mapped to Ursus inheritance system.

Verification After Translation

After translation, add specifications and proofs:

(* Specification *)
Definition transfer_spec (from to: address) (amount: uint256)
                         (s s': ContractState) : Prop :=
  balance s' to = balance s to + amount /\
  balance s' from = balance s from - 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.

See Also

• Translation Overview - Translation system overview
• Ursus → Solidity - Reverse translation
• Contract Structure - Contract organization
• Verification - Formal verification