Ursus Control Sub-language

Ursus provides a rich set of control flow constructs that map to both imperative code and formal semantics. This section covers the control flow sub-language.

Conditional Statements

If-Then-Else

Syntax:

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

Example:

::// if balance >= amount then { ->> } else { -/> } | .
{
    ::// balance := balance - amount |.
}
{
    ::// exit_ {1} |.
}

If-Then (No Else)

Syntax:

::// if condition then { panic_flag } | .
{
    (* then branch *)
}

Example:

::// if amount > {0} then { ->> } | .
{
    ::// totalAmount := totalAmount + amount |.
}

Nested Conditionals

::// if condition1 then { ->> } else { ->> } | .
{
    ::// if condition2 then { ->> } else { ->> } | .
    {
        ::// action1() |.
    }
    {
        ::// action2() |.
    }
}
{
    ::// action3() |.
}

Loops

While Loop

Syntax:

::// while condition do { panic_flag } | .
{
    (* loop body *)
}

Example:

::// while counter < {10} do { ->> } | .
{
    ::// counter := counter + {1} |.
}

Note: While loops always have panic flag true (may not terminate)

For Loop

Syntax:

::// for 'var in range do { panic_flag } | .
{
    (* loop body using var *)
}

Example:

::// for 'i in {0} to {10} do { ->> } | .
{
    ::// sum := sum + i |.
}

Early Exit

Exit Statement

Syntax:

::// exit_ error_code .

Example:

::// if balance < amount then { -/> } | .
{
    ::// exit_ {1} |.
}

Effect:

• Immediately terminates execution
• Returns error code
• Sets panic flag to true

Require Statement

Syntax:

::// require_ condition .
::// require_ condition, error_code .

Examples:

::// require_ (balance >= amount) .
::// require_ (amount > {0}), {100} .

Effect:

• Checks condition
• If false, exits with error code
• Sets panic flag to true

Skip Statement

Syntax:

::// skip_ .

Use:

• No-op (do nothing)
• Placeholder in branches
• Satisfy syntax requirements

Example:

::// if condition then { ->> } else { ->> } | .
{
    ::// doSomething() |.
}
{
    ::// skip_ |.  (* Else does nothing *)
}

Return Statement

Syntax:

return.
return value.

Examples:

(* No return value *)
{
    ::// skip_ |.
}
return.

(* With return value *)
{
    ::// var 'result : uint256 := {42} |.
}
return result.

(* Direct return *)
return {42}.

Panic Flags in Control Flow

Non-Panicking (->>)

Use when code cannot panic:

::// if x > {0} then { ->> } else { ->> } | .
{
    ::// y := x + {1} |.  (* Cannot panic *)
}
{
    ::// y := {0} |.  (* Cannot panic *)
}

Panicking (-/>)

Use when code may panic:

::// if balance < amount then { -/> } else { ->> } | .
{
    ::// exit_ {1} |.  (* Panics *)
}
{
    ::// balance := balance - amount |.  (* Safe *)
}

Mixed Panic Flags

Result is panicking if any branch panics:

::// if condition then { -/> } else { ->> } | .
(* Overall: panicking (true) *)

See Also

• Tactics - Building control flow
• Holes - Panic holes
• Custom Grammar - Control flow syntax