Function Operators

This guide explains the operators available in Ursus function bodies based on real examples from ursus-patterns.

Statement Prefixes

Every statement in Ursus function body starts with a prefix:

Example from ContractSimplyFuns.v:

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

Statement Terminators

Statements end with:

• . - Statement continues (more statements follow)
• |. - Last statement in block

Example:

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

Variable Declaration

Simple Variable Declaration

Syntax:

::// var00 varname : vartype ;_| .

Example from ContractSimplyFuns.v:

::// var00 ind1 : Ind3 ;_| .

Variable with Initialization

Syntax:

::// var00 varname : vartype := expression ;_| .

Example from ContractSimplyFuns.v:

::// var00 y : uint256 := uint256(arg1_u64);_| .

Multiple Variables

Example from ContractManage.v:

::// var00 r1 : Rec1LRecord; _ |.

Note: Must declare types in UseLocal before using:

UseLocal Definition _ := [ uint64 ; Ind3 ].

Assignment

Simple Assignment

Syntax:

::// variable := expression .

Example from ContractSimplyFuns.v:

:://  _res := (const00_u256 + state02_u256) |.

Compound Assignment

Syntax:

::// variable += expression .
::// variable -= expression .
::// variable *= expression .
::// variable /= expression .

Example from ContractSimplyFuns.v:

::// arg1_u8 += state03_u8.

Mapping Assignment

Syntax:

::// mapping[[key]] := value .

Example from ContractManage.v:

::// state01_m_u256_u64[[fun06 (const03_u64) + fun06( const03_u64 ) ]] := const03_u64 .

Record Field Assignment

Syntax:

::// record.field := value .

Example from ContractManage.v:

::// r1.rec1_u64 := state01_m_u256_u64[[fun06 (const03_u64)]] |.

Control Flow

If-Then

Syntax:

:://  if condition then { exit_ value } | .

Example from ContractManage.v:

:://  if (arg1_u8 >= state07_u8) then { exit_ arg1_u8 } | .

If-Then-Else

Syntax:

:://  if condition then { ->/> } else {->>} | .
{
    (* then branch *)
}
{
    (* else branch *)
}

Example from ContractManage.v:

:://  if (! arg1_u8 >= state07_u8) then { ->/> } else {->>} | .
{
   ::// arg1_u8 += {23} .
   ::// exit_ arg1_u8 |.
}
{
   ::// state07_u8 += arg1_u8 |.
}

Placeholders:

• ->/> - Placeholder for then branch
• ->> - Placeholder for else branch

For Loop

Syntax:

::// for (var00 i : type := init, condition, update) do { ->> } .
{
    (* loop body *)
}

Example from ContractManage.v:

::// for (var00 i : uint8 := fun_if_then_else ( arg1_u8 ) * fun_if_then_else(arg2_u8) - {1%N} , i >= {0%N}, i --) do { ->> } .
{
  ::// state07_u8 += arg1_u8 .
  ::// state01_m_u256_u64[[fun06 (const03_u64) + fun06( const03_u64 ) ]] := const03_u64 .
  ::// var00 r1 : Rec1LRecord; _ |.
  ::// r1.rec1_u64 := state01_m_u256_u64[[fun06 (const03_u64)]] |.
}

While Loop

Syntax:

::// while ( condition ) do { ->/> } .
{
    (* loop body *)
}

Example from ContractManage.v:

::// while ( arg1_u8 >= state07_u8 + {3%N} ) do { ->/> } .
{
    (* loop body *)
}

Require Statement

Syntax:

:://  require_(condition, error_code) .

Example from ContractSimplyFuns.v:

:://  require_((const02_u8 >= state03_u8 + arg1_u8) &&
               (arg1_u8+const02_u8 >= state03_u8), const01_err).
:://  require_(state04_bool == {false}) |.

Return and Exit

Implicit Return

Most functions use implicit return via _res or _result:

:://  _res := value |.

Explicit Return

Syntax:

return value.

Example from ContractSimplyFuns.v:

return arg1_u256.

Early Exit

Syntax:

exit_ value

Example from ContractManage.v:

:://  if (arg1_u8 >= state07_u8) then { exit_ arg1_u8 } | .

Expressions

Literals

Numeric literals:

{100}        (* uint literal *)
{0}          (* zero *)
{5%N}        (* N notation *)
{1%N}        (* one *)

Boolean literals:

{true}
{false}
@true        (* alternative *)
@false       (* alternative *)

String literals:

{"Hello world!"}
{"Insufficient balance"}

Enum literals:

#{ind31}     (* enum value *)
#{Active}

Arithmetic Operators

Example from ContractManage.v:

::// for (var00 i : uint8 := fun_if_then_else ( arg1_u8 ) * fun_if_then_else(arg2_u8) - {1%N} , i >= {0%N}, i --) do { ->> } .

Comparison Operators

Example from ContractManage.v:

:://  if (arg1_u8 >= state07_u8) then { exit_ arg1_u8 } | .

Logical Operators

Example from ContractSimplyFuns.v:

:://  require_((const02_u8 >= state03_u8 + arg1_u8) &&
               (arg1_u8+const02_u8 >= state03_u8), const01_err).

Ternary Operator

Syntax:

condition ? true_value : false_value

Example from ContractSimplyFuns.v:

::// y := uint256(arg1_u64) > {5%N} ? {6%N} : state02_u256.

Type Casting

Syntax:

targetType(value)

Example from ContractSimplyFuns.v:

:://  _res := uint256(arg1_u8) |.

Function Calls

Syntax:

functionName(arg1, arg2, ...)

Example from ContractSimplyFuns.v:

::// _res := y + fun05() * fun05() * fun04(state03_u8) |.

State Access

Contract Fields

Direct access to contract state:

state02_u256
state03_u8
state04_bool

Mapping Access

Syntax:

mapping[[key]]

Example from ContractManage.v:

::// state01_m_u256_u64[[fun06 (const03_u64)]] := const03_u64 .

Record Field Access

Syntax:

record.field
record->field    (* alternative *)

Example from ContractManage.v:

::// r1.rec1_u64 := state01_m_u256_u64[[fun06 (const03_u64)]] |.

Special Variables

Holes and Placeholders

Ursus supports "holes" for incremental development:

Example:

::// var00 ind1 : Ind3 ;_| .

See Also

• Functions - Function structure
• Local Variables - Local state management
• Types and Primitives - Available types