Keyboard shortcuts

Press ← or → to navigate between chapters

Press S or / to search in the book

Press ? to show this help

Press Esc to hide this help

Interfaces and Messages

Interfaces enable type-safe inter-contract communication in Ursus. This section covers defining interfaces, declaring message recipients, and sending messages.

Overview

Interfaces define the external API of a contract - the functions that other contracts can call.

Messages are the mechanism for calling functions on other contracts.

Key benefits:

  • Type safety - Compile-time checking of message sends
  • Documentation - Explicit contract dependencies
  • Verification - Formal verification of inter-contract calls
  • Code generation - Automatic interface bindings

Defining Interfaces

Interfaces are defined in separate files or at the beginning of contract files.

Interface File Structure

Require Import UrsusEnvironment.Solidity.current.Environment.

Interfaces.
SetUrsusOptions.
Unset Ursus Extraction.

MakeInterface Class IInterfaceName :=
{
    method1 : type1 -> type2 -> UExpression returnType flag ;
    method2 : type3 -> UExpression returnType flag ;
    ...
}.

EndInterfaces.

Interface Syntax

Basic structure:

MakeInterface Class IInterfaceName :=
{
    methodName : arg1Type -> arg2Type -> ... -> UExpression returnType flag
}.

Components:

  • IInterfaceName - Interface name (conventionally starts with I)
  • methodName - Function name
  • argTypes - Curried argument types
  • returnType - Return type
  • flag - Panic flag (true or false)

Example: ERC20 Interface

Interfaces.
SetUrsusOptions.
Unset Ursus Extraction.

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

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

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

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

EndInterfaces.

Method Attributes

Methods can have attributes:

#[view, public]         (* Read-only public method *)
#[external]             (* External method *)
#[override, external]   (* Override parent method *)
#[external, payable]    (* Payable external method *)

Declaring Message Recipients

The Sends To declaration specifies which interfaces a contract can send messages to.

Syntax

Sends To Interface1 Interface2 Interface3 ;

Examples

Multiple interfaces:

Sends To IERC20 ITokenReceiver IOwnable ;

Single interface:

Sends To IERC20 ;

No external calls:

Sends To ;

Purpose

The Sends To declaration:

  1. Enables type checking - Only declared interfaces can be called
  2. Documents dependencies - Makes external calls explicit
  3. Supports verification - Enables formal verification of calls
  4. Generates bindings - Creates interface code in target language

Sending Messages

Messages are sent using the send notation.

Syntax

::// send Interface.Method(arg1, arg2, ...)
         => target_address
         with message_params .

Components

  • Interface.Method - Interface and method name
  • (arg1, arg2, ...) - Method arguments
  • target_address - Recipient contract address
  • message_params - Message parameters (value, flags, etc.)

Basic Example

::// send IERC20.Transfer(from, to, amount)
         => token_address
         with {InternalMessageParamsLRecord} [$ {2} ⇒ {Message_ι_flag} $] .

Message Parameters

Message parameters control how the message is sent:

{InternalMessageParamsLRecord} [$
    {value} ⇒ {Message_ι_value} ;
    {flags} ⇒ {Message_ι_flag} ;
    {bounce} ⇒ {Message_ι_bounce}
$]

Common parameters:

  • Message_ι_value - Amount of tokens to send
  • Message_ι_flag - Message flags
  • Message_ι_bounce - Bounce on error

Complete Example

Interface Definition (IERC20.v)

Require Import UrsusEnvironment.Solidity.current.Environment.

Interfaces.
SetUrsusOptions.
Unset Ursus Extraction.

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

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

    #[view, public]
    totalSupply : UExpression uint256 false
}.

EndInterfaces.

Contract Using Interface

Require Import UrsusEnvironment.Solidity.current.Environment.
Require Import UrsusEnvironment.Solidity.current.LocalGenerator.
Require Import IERC20.

Module TokenWrapper.

#[translation = on]
#[language = solidity]
Contract TokenWrapper ;
Sends To IERC20 ;
Types ;
Constants ;

Record Contract := {
    token: address;
    total_wrapped: uint256
}.

SetUrsusOptions.
UseLocal Definition _ := [uint256; address; boolean].

#[external, returns=_result]
Ursus Definition wrapTokens (amount: uint256): UExpression boolean true.
{
    ::// send IERC20.transfer(this->address, amount)
             => token
             with {InternalMessageParamsLRecord} [$ {0} ⇒ {Message_ι_value} $] .

    ::// total_wrapped := total_wrapped + amount .
    ::// _result := @true |.
}
return.
Defined.
Sync.

EndContract Implements.
End TokenWrapper.

Advanced Patterns

Callback Interfaces

Define interfaces for callbacks:

MakeInterface Class ITokenReceiver :=
{
    #[external]
    onTokenReceived : address -> uint256 -> UExpression PhantomType true
}.

Usage:

::// send ITokenReceiver.onTokenReceived(sender, amount)
         => recipient
         with {InternalMessageParamsLRecord} [$ {0} ⇒ {Message_ι_value} $] .

Multiple Interface Calls

Sends To IERC20 IOwnable ITokenReceiver ;

Ursus Definition complexOperation: UExpression PhantomType true.
{
    ::// send IERC20.transfer(recipient, amount)
             => token_address
             with {InternalMessageParamsLRecord} [$ {0} ⇒ {Message_ι_value} $] .

    ::// send ITokenReceiver.onTokenReceived(msg->sender, amount)
             => recipient
             with {InternalMessageParamsLRecord} [$ {0} ⇒ {Message_ι_value} $] .

    ::// send IOwnable.transferOwnership(new_owner)
             => ownable_contract
             with {InternalMessageParamsLRecord} [$ {0} ⇒ {Message_ι_value} $] |.
}
return.
Defined.

Conditional Message Sending

::// if should_notify then { ->> } | .
{
    ::// send ITokenReceiver.onTokenReceived(sender, amount)
             => recipient
             with {InternalMessageParamsLRecord} [$ {0} ⇒ {Message_ι_value} $] |.
}

Best Practices

1. Use Descriptive Interface Names

Good:

MakeInterface Class IERC20 := { ... }.
MakeInterface Class ITokenVesting := { ... }.
MakeInterface Class IOwnable := { ... }.

Avoid:

MakeInterface Class I1 := { ... }.
MakeInterface Class MyInterface := { ... }.

Good:

MakeInterface Class IERC20 :=
{
    (* View methods *)
    #[view, public]
    balanceOf : address -> UExpression uint256 false ;

    #[view, public]
    totalSupply : UExpression uint256 false ;

    (* State-changing methods *)
    #[external]
    transfer : address -> uint256 -> UExpression boolean true ;

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

3. Document Panic Flags

MakeInterface Class IToken :=
{
    (* Can panic: requires sufficient balance *)
    transfer : address -> uint256 -> UExpression boolean true ;

    (* Cannot panic: pure view function *)
    #[view, public]
    balanceOf : address -> UExpression uint256 false
}.

4. Declare All Dependencies

Good:

Sends To IERC20 IOwnable ITokenReceiver ;

Avoid:

Sends To ;
(* Missing interfaces - will cause compilation errors *)

Common Patterns

Token Transfer

::// send IERC20.transfer(recipient, amount)
         => token_address
         with {InternalMessageParamsLRecord} [$ {0} ⇒ {Message_ι_value} $] .

Ownership Transfer

::// send IOwnable.transferOwnership(new_owner)
         => contract_address
         with {InternalMessageParamsLRecord} [$ {0} ⇒ {Message_ι_value} $] .

Callback Notification

::// send ICallback.onComplete(result)
         => callback_address
         with {InternalMessageParamsLRecord} [$ {0} ⇒ {Message_ι_value} $] .

See Also