Functions and Modifiers

This guide explains how to define functions in Ursus contracts based on real examples from ursus-patterns.

Function Structure

Every Ursus function follows this structure:

#[attributes]
Ursus Definition functionName (arguments): UExpression ReturnType panicFlag.
{
    (* Function body *)
}
return.
Defined.
Sync.

Components

1. Attributes

Function attributes are specified before the function definition.

Syntax:

#[attribute1]
#[attribute2, attribute3]

Common attributes:

• #[public] - Public function
• #[external] - External function
• #[internal] - Internal function
• #[private] - Private function
• #[view] - Read-only function
• #[pure] - Pure function (no state access)
• #[payable] - Can receive value
• #[returns=name] - Specify return variable name
• #[write=arg] - Allow writing to argument
• #[no_body] - Function without body (interface)

Example from ContractSimplyFuns.v:

#[returns=_res]
Ursus Definition fun05 : UExpression uint256 false.

See: Function Attributes

2. Function Name

Function name must be a valid Coq identifier.

Rules:

• Starts with letter or underscore
• Can contain letters, numbers, underscores
• No spaces
• Case-sensitive

Examples:

Ursus Definition transfer ...
Ursus Definition balanceOf ...
Ursus Definition _internal_helper ...
Ursus Definition fun01 ...

3. Arguments

Arguments are specified in parentheses with type annotations.

No arguments:

Ursus Definition fun01: UExpression PhantomType false.

One argument:

Ursus Definition fun02 (arg1_u256: uint256): UExpression uint256 false.

Multiple arguments:

Ursus Definition fun07 (arg1_u8: uint8) (arg2_str: string): UExpression string false.

Argument syntax:

(argumentName: argumentType)

Argument names:

• Follow same rules as function names
• Conventionally use descriptive names or type suffixes

Example from ContractSimplyFuns.v:

Ursus Definition fun04 (arg1_u8 : uint8): UExpression uint256 false.

4. Return Type

Return type specifies what the function returns.

No return value:

UExpression PhantomType panicFlag

Specific return type:

UExpression uint256 panicFlag
UExpression address panicFlag
UExpression boolean panicFlag

Examples from ContractSimplyFuns.v:

No return:

Ursus Definition fun01: UExpression PhantomType false.

Returns uint256:

Ursus Definition fun02 (arg1_u256: uint256): UExpression uint256 false.

Returns string:

Ursus Definition fun07 (arg1_u8: uint8) (arg2_str: string): UExpression string false.

See: Types and Primitives

5. Panic Flag

The panic flag indicates whether the function can fail (panic/revert).

Syntax:

UExpression ReturnType true   (* Can panic *)
UExpression ReturnType false  (* Cannot panic *)

Use true when:

• Function contains require_() statements
• Function calls other functions with true flag
• Function has early returns (e.g., return in if-statement)

Use false when:

• Function always succeeds
• No require statements
• No early returns
• Only calls functions with false flag

Examples from ContractSimplyFuns.v:

With panic (has require):

Ursus Definition fun08 (arg1_u8: uint8) : UExpression PhantomType true.
{
    :://  require_((const02_u8 >= state03_u8 + arg1_u8) &&
                   (arg1_u8+const02_u8 >= state03_u8), const01_err).
    :://  require_(state04_bool == {false}) |.
}
return.
Defined.

Without panic:

Ursus Definition fun05 : UExpression uint256 false.
{
    :://  _res := (const00_u256 + state02_u256) |.
}
return.
Defined.

6. Function Body

Function body contains the implementation.

Empty body (interface):

#[no_body]
Ursus Definition fun01: UExpression PhantomType false.
return.
Defined.

Body with code:

Ursus Definition fun05 : UExpression uint256 false.
{
    :://  _res := (const00_u256 + state02_u256) |.
}
return.
Defined.

Body syntax:

• Enclosed in { } braces
• Statements start with ::// or :://
• Statements end with . or |.
• Last statement ends with |.

See: Function Operators

7. Return Statement

Return statement specifies what to return.

No return value:

return.

Return argument:

return arg1_u256.

Return variable:

return arg2_str.

Return implicit result:

return.  (* Uses _res or _result *)

Examples from ContractSimplyFuns.v:

Return nothing:

Ursus Definition fun01: UExpression PhantomType false.
return.
Defined.

Return argument:

Ursus Definition fun02 (arg1_u256: uint256): UExpression uint256 false.
return arg1_u256.
Defined.

Return variable:

Ursus Definition fun07 (arg1_u8: uint8) (arg2_str: string): UExpression string false.
{
    ::// arg2_str := {"Hello world!"} |.
}
return arg2_str.
Defined.

8. Defined and Sync

Every function must end with Defined. and Sync.

Defined.
Sync.

Purpose:

• Defined. - Finalizes the Coq definition
• Sync. - Synchronizes with Ursus code generator

Complete Examples

Example 1: Simple Function

From ContractSimplyFuns.v:

#[returns=_res]
Ursus Definition fun05 : UExpression uint256 false.
{
    :://  _res := (const00_u256 + state02_u256) |.
}
return.
Defined.
Sync.

Example 2: Function with Arguments

From ContractSimplyFuns.v:

#[returns=_res]
Ursus Definition fun04 (arg1_u8 : uint8): UExpression uint256 false.
{
    :://  _res := uint256(arg1_u8) |.
}
return.
Defined.
Sync.

Example 3: Function with Local Variables

From ContractSimplyFuns.v:

UseLocal Definition _ := [ uint64 ; Ind3 ].

#[returns=_res]
Ursus Definition fun06 (arg1_u64: uint64): UExpression uint256 false.
{
    ::// var00 ind1 : Ind3 ;_| .
    ::// ind1 := #{ind31} .

    ::// var00 y : uint256 := uint256(arg1_u64);_| .
    ::// y := uint256(arg1_u64) > {5%N} ? {6%N} : state02_u256.
    ::// _res := y + fun05() * fun05() * fun04(state03_u8) |.
}
return.
Defined.
Sync.

Example 4: Function with Writable Arguments

From ContractSimplyFuns.v:

UseLocal Definition _ := [ string ].

#[write=arg1_u8, write=arg2_str]
Ursus Definition fun07 (arg1_u8: uint8) (arg2_str: string): UExpression string false.
{
    ::// arg1_u8 += state03_u8.
    ::// arg2_str := {"Hello world!"} |.
}
return arg2_str.
Defined.
Sync.

Example 5: Function with Require

From ContractSimplyFuns.v:

Ursus Definition fun08 (arg1_u8: uint8) : UExpression PhantomType true.
{
    :://  require_((const02_u8 >= state03_u8 + arg1_u8) &&
                   (arg1_u8+const02_u8 >= state03_u8), const01_err).
    :://  require_(state04_bool == {false}) |.
}
return.
Defined.
Sync.

Local Variables

To use local variables, declare their types with UseLocal:

UseLocal Definition _ := [ uint256 ].

Multiple types:

UseLocal Definition _ := [ uint64 ; Ind3 ; string ].

See: Local State and Variables

See Also

• Function Operators - Operators in function body
• Function Attributes - Function attributes
• Local Variables - Local state
• Writing Functions - Detailed function writing guide