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

UExpression Grammar: Statements and Control Flow

This section explains the UExpression grammar - the core type for statements, control flow, and monadic computations in Ursus.

Overview

UExpression represents executable statements and control flow constructs. It is the foundation of Ursus's monadic encoding of smart contract logic.

UExpressionP Definition

Inductive UExpressionP (R: Type): bool -> Type :=    
    | FuncallExpression : forall {b X}, LedgerT (ControlResultP X b) -> UExpressionP R b
    | ReturnExpression : forall {b}, bool -> URValueP R b -> UExpressionP R b
    | ExitExpression : forall {b}, URValueP R b -> UExpressionP R true
    | BreakExpression : bool -> UExpressionP R true
    | StrictBinding : forall {xb yb}, UExpressionP R xb -> UExpressionP R yb -> 
                      UExpressionP R (xb || yb)
    | WeakBinding : forall {xb yb}, UExpressionP R xb -> UExpressionP R yb -> 
                    UExpressionP R yb
    | RequireExpression : forall {B b}`{boolFunRec_gen B}, URValueP B b -> 
                          URValueP ErrorType false -> UExpressionP R true
    | IfElseExpression: forall {B bb xb yb}`{boolFunRec_gen B}, URValueP B bb -> 
                        UExpressionP R xb -> UExpressionP R yb -> 
                        UExpressionP R (bb || xb || yb)
    | AssignExpression : forall {b X}, ULValueP X -> URValueP X b -> XDefault X -> 
                         UExpressionP R b
    | DynamicAssignExpression: forall {br X}, LedgerT (ULValueP X) -> URValueP X br -> 
                               UExpressionP R br
    | DynamicBinding : forall {b X}, LedgerT X -> (X -> UExpressionP R b) -> 
                       UExpressionP R b 
    | WhileExpression : forall {bb b}, URValueP XBool bb -> UExpressionP R b -> 
                        UExpressionP R true
    | ForXHMapExpression : forall {K V mb b bb}, URValueP (XHMap K V) mb -> 
                           URValueP XBool bb -> ((XProd K V) -> UExpressionP R b) -> 
                           UExpressionP R true
    | ForXHMapExpressionCL : forall {K V mb b}, URValueP (XHMap K V) mb -> 
                             ((XProd K V) -> UExpressionP R b) -> 
                             UExpressionP R (mb || b)
    | LedgerTExpression : forall {b}, LedgerT (ControlResultP R b) -> UExpressionP R b.

Type Parameters

  • R - Return type of the function containing this expression
  • bool - Panic flag:
    • false - Cannot panic
    • true - May panic

Constructors

FuncallExpression - Function Call

FuncallExpression : forall {b X}, LedgerT (ControlResultP X b) -> UExpressionP R b

Purpose: Call a function and discard its result

Examples:

FuncallExpression (transfer(to, amount)) : UExpression R true

Panic flag: Inherited from the function

Usage: Typically used for functions called for side effects

ReturnExpression - Return Statement

ReturnExpression : forall {b}, bool -> URValueP R b -> UExpressionP R b

Purpose: Return a value from the function

Notation: return value

Examples:

::// return true |.
::// _result := value |.

Parameters:

  • First bool - Whether this is an explicit return
  • URValueP R b - Value to return

Panic flag: Inherited from the return value

ExitExpression - Early Exit

ExitExpression : forall {b}, URValueP R b -> UExpressionP R true

Purpose: Exit function early with a value

Panic flag: Always true (early exit is exceptional control flow)

BreakExpression - Loop Break

BreakExpression : bool -> UExpressionP R true

Purpose: Break out of a loop

Notation: break

Panic flag: Always true (break is exceptional control flow)

StrictBinding - Sequential Composition

StrictBinding : forall {xb yb}, UExpressionP R xb -> UExpressionP R yb -> 
                UExpressionP R (xb || yb)

Purpose: Execute two expressions in sequence, propagating errors

Notation: e1 ; e2

Semantics:

do _ <- e1;
   e2

Panic flag: xb || yb (panics if either expression can panic)

Error propagation: If e1 errors, e2 is not executed

WeakBinding - Sequential Composition (No Error Propagation)

WeakBinding : forall {xb yb}, UExpressionP R xb -> UExpressionP R yb -> 
              UExpressionP R yb

Purpose: Execute two expressions in sequence, ignoring first's errors

Panic flag: yb (only second expression's panic flag)

Difference from StrictBinding: Errors in e1 don't prevent e2

RequireExpression - Assertion

RequireExpression : forall {B b}`{boolFunRec_gen B}, URValueP B b -> 
                    URValueP ErrorType false -> UExpressionP R true

Purpose: Assert a condition, error if false

Notation: require(condition, error_code)

Examples:

::// require(balance >= amount, {101}) .

Panic flag: Always true (can fail)

Type class: boolFunRec_gen B - B can be converted to boolean

IfElseExpression - Conditional

IfElseExpression: forall {B bb xb yb}`{boolFunRec_gen B}, URValueP B bb -> 
                  UExpressionP R xb -> UExpressionP R yb -> 
                  UExpressionP R (bb || xb || yb)

Purpose: Conditional execution

Notation: if condition then branch1 else branch2

Examples:

::// if balance > {0} then { ->> } else { ->> } | .
{
    ::// transfer(to, balance) |.
}
{
    ::// return false |.
}

Panic flag: bb || xb || yb (panics if condition or either branch can panic)

AssignExpression - Assignment

AssignExpression : forall {b X}, ULValueP X -> URValueP X b -> XDefault X -> 
                   UExpressionP R b

Purpose: Assign a value to a location

Notation: lvalue := rvalue

Examples:

::// balance := {1000} .
::// balances[[addr]] := balances[[addr]] + amount .

Panic flag: Inherited from the right-hand side

Type class: XDefault X - Type X must have a default value

DynamicAssignExpression - Dynamic Assignment

DynamicAssignExpression: forall {br X}, LedgerT (ULValueP X) -> URValueP X br -> 
                         UExpressionP R br

Purpose: Assign to a location computed at runtime

Panic flag: Inherited from the right-hand side

DynamicBinding - Monadic Bind

DynamicBinding : forall {b X}, LedgerT X -> (X -> UExpressionP R b) -> 
                 UExpressionP R b

Purpose: Bind a monadic computation to a continuation

Notation: var 'x := e ; continuation

Examples:

::// var 'balance : uint256 := getBalance() .
::// (* use balance *) |.

Panic flag: Inherited from the continuation

WhileExpression - While Loop

WhileExpression : forall {bb b}, URValueP XBool bb -> UExpressionP R b -> 
                  UExpressionP R true

Purpose: While loop

Notation: while condition do body

Panic flag: Always true (loops may not terminate)

ForXHMapExpression - Map Iteration (with condition)

ForXHMapExpression : forall {K V mb b bb}, URValueP (XHMap K V) mb -> 
                     URValueP XBool bb -> ((XProd K V) -> UExpressionP R b) -> 
                     UExpressionP R true

Purpose: Iterate over a map with a condition

Panic flag: Always true (iteration may not terminate)

ForXHMapExpressionCL - Map Iteration (complete)

ForXHMapExpressionCL : forall {K V mb b}, URValueP (XHMap K V) mb -> 
                       ((XProd K V) -> UExpressionP R b) -> 
                       UExpressionP R (mb || b)

Purpose: Iterate over entire map

Panic flag: mb || b (panics if map or body can panic)

LedgerTExpression - Monadic Lift

LedgerTExpression : forall {b}, LedgerT (ControlResultP R b) -> UExpressionP R b

Purpose: Lift a monadic computation into an expression

Panic flag: Inherited from the computation

Panic Flag Propagation

The panic flag follows these rules:

  1. Literals: Always false
  2. State access: Always false
  3. Operators: b1 || b2 (OR of operands)
  4. Conditionals: b_cond || b_then || b_else
  5. Loops: Always true
  6. Require: Always true
  7. Function calls: Depends on function

See Also