Contract File Interfaces

Interfaces in Ursus define the external API of contracts, enabling type-safe inter-contract communication. They are defined in separate files and used by contracts that need to interact with each other.

Interface File Structure

Basic Structure

Require Import UrsusEnvironment.Solidity.current.Environment.

Interfaces.

SetUrsusOptions.
Unset Ursus Extraction.

MakeInterface Class IMyInterface :=
{
    method1 : arg1Type -> UExpression returnType panicFlag ;
    method2 : arg1Type -> arg2Type -> UExpression returnType panicFlag
}.

EndInterfaces.

Real Example: IContractSimplyFuns

From ursus-patterns/src/Solidity/Interfaces/IContractSimplyFuns.v:

Require Import UrsusEnvironment.Solidity.current.Environment.

Interfaces.

SetUrsusOptions.
Unset Ursus Extraction.

MakeInterface Class IContractSimplyFuns :=
{
    #[override, external]
    fun02 : uint256 -> UExpression uint256 false ;
    #[override, external]
    fun08 : uint8 -> UExpression PhantomType true
}.

EndInterfaces.

Interface Sections

1. Imports

Require Import UrsusEnvironment.Solidity.current.Environment.

Import the Ursus environment for the target platform (Solidity, C++, Rust).

2. Interfaces Block

Interfaces.
(* Interface definitions go here *)
EndInterfaces.

All interface definitions must be between Interfaces. and EndInterfaces..

3. Options

SetUrsusOptions.
Unset Ursus Extraction.

SetUrsusOptions - Configure Ursus compiler options
Unset Ursus Extraction - Disable code extraction for interfaces (they're declarations only)

4. Interface Definition

MakeInterface Class IMyInterface :=
{
    (* Method signatures *)
}.

Method Signatures

Basic Signature

methodName : argType -> UExpression returnType panicFlag

Components:

methodName - Function name
argType - Argument type (can be multiple with ->)
returnType - Return type
panicFlag - true if can panic, false otherwise

Multiple Arguments

transfer : address -> uint256 -> UExpression boolean false

Equivalent to:

function transfer(address to, uint256 amount) external returns (bool);

No Arguments

totalSupply : UExpression uint256 false

No Return Value

burn : uint256 -> UExpression PhantomType false

PhantomType indicates no meaningful return value (like void).

Can Panic

withdraw : uint256 -> UExpression unit true

The true flag indicates this function can revert/panic.

Method Attributes

Common Attributes

#[override, external]
methodName : argType -> UExpression returnType panicFlag

Attributes:

override - Overrides parent interface method
external - External visibility
view - Read-only function
pure - No state access

Example with Attributes

MakeInterface Class IERC20 :=
{
    #[external, view]
    balanceOf : address -> UExpression uint256 false ;

    #[external]
    transfer : address -> uint256 -> UExpression boolean false ;

    #[external]
    approve : address -> uint256 -> UExpression boolean false
}.

Complete Interface Example

ERC20 Interface

Require Import UrsusEnvironment.Solidity.current.Environment.

Interfaces.

SetUrsusOptions.
Unset Ursus Extraction.

MakeInterface Class IERC20 :=
{
    #[external, view]
    totalSupply : UExpression uint256 false ;

    #[external, view]
    balanceOf : address -> UExpression uint256 false ;

    #[external, view]
    allowance : address -> address -> UExpression uint256 false ;

    #[external]
    transfer : address -> uint256 -> UExpression boolean false ;

    #[external]
    approve : address -> uint256 -> UExpression boolean false ;

    #[external]
    transferFrom : address -> address -> uint256 -> UExpression boolean false
}.

EndInterfaces.

Using Interfaces

In Contract Declaration

Contract MyToken ;
Sends To IERC20 ;
Inherits ;

Calling Interface Methods

Ursus Definition callOtherToken (tokenAddr: address) (to: address) (amount: uint256):
  UExpression boolean false.
{
    ::// _result := IERC20(tokenAddr).transfer(to, amount) |.
}
return.
Defined.

Interface Inheritance

Extending Interfaces

MakeInterface Class IExtendedToken :=
{
    (* Inherits IERC20 methods *)

    #[external]
    mint : address -> uint256 -> UExpression boolean false ;

    #[external]
    burn : uint256 -> UExpression boolean false
}.

Multiple Interfaces

Defining Multiple Interfaces in One File

Interfaces.

SetUrsusOptions.
Unset Ursus Extraction.

MakeInterface Class IToken :=
{
    transfer : address -> uint256 -> UExpression boolean false
}.

MakeInterface Class IOwnable :=
{
    owner : UExpression address false ;
    transferOwnership : address -> UExpression unit false
}.

EndInterfaces.

URSUS language Documentation