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

Primitive Types

Ursus provides a comprehensive set of primitive types that map to blockchain platform types while maintaining formal verification capabilities.

Integer Types

Unsigned Integers

Available types:

uint8      (* 0 to 255 *)
uint16     (* 0 to 65,535 *)
uint32     (* 0 to 4,294,967,295 *)
uint64     (* 0 to 18,446,744,073,709,551,615 *)
uint128    (* 0 to 2^128 - 1 *)
uint256    (* 0 to 2^256 - 1 *)

Literals:

{0}        (* Zero *)
{42}       (* Decimal *)
{0xFF}     (* Hexadecimal *)
{0o77}     (* Octal *)
{0b1010}   (* Binary *)

Examples:

::// var 'balance : uint256 := {1000000000000000000} .
::// var 'count : uint8 := {10} .
::// var 'flags : uint32 := {0xDEADBEEF} .

Operations:

  • Arithmetic: +, -, *, /, %
  • Comparison: ==, !=, <, >, <=, >=
  • Bitwise: &, |, ^, ~, <<, >>

Overflow behavior:

  • Wraps around (modulo 2^n)
  • Use safe math functions to prevent overflow

Signed Integers

Available types:

int8       (* -128 to 127 *)
int16      (* -32,768 to 32,767 *)
int32      (* -2^31 to 2^31 - 1 *)
int64      (* -2^63 to 2^63 - 1 *)
int128     (* -2^127 to 2^127 - 1 *)
int256     (* -2^255 to 2^255 - 1 *)

Literals:

{-42}      (* Negative *)
{+100}     (* Positive *)
{0}        (* Zero *)

Examples:

::// var 'delta : int256 := {-1000} .
::// var 'temperature : int8 := {-40} .

Operations:

  • Same as unsigned integers
  • Sign-aware comparison and arithmetic

Boolean Type

Type:

boolean

Values:

@true
@false

Examples:

::// var 'isActive : boolean := @true .
::// var 'hasPermission : boolean := @false .
::// var 'result : boolean := (x > {0}) && (y < {100}) .

Operations:

  • Logical: && (AND), || (OR), ! (NOT)
  • Comparison: ==, !=

Conditional:

::// if isActive then { ->> } else { ->> } | .
{
    ::// doSomething() |.
}
{
    ::// skip_ |.
}

Address Type

Type:

address

Represents:

  • Blockchain account address
  • Contract address
  • External account address

Literals:

{0x742d35Cc6634C0532925a3b844Bc9e7595f0bEb}  (* Ethereum-style *)
{0:1234567890abcdef1234567890abcdef1234567890abcdef1234567890abcdef}  (* TON-style *)

Special addresses:

msg->sender        (* Transaction sender *)
this->address      (* Current contract *)
{0x0}              (* Zero address *)

Examples:

::// var 'owner : address := msg->sender .
::// var 'recipient : address := {0x742d35Cc6634C0532925a3b844Bc9e7595f0bEb} .
::// balances[[owner]] := {1000} .

Operations:

  • Comparison: ==, !=
  • Mapping key: mapping address uint256

Common patterns:

(* Check if address is zero *)
::// if addr == {0x0} then { -/> } | .
{
    ::// exit_ {1} |.
}

(* Check if sender is owner *)
::// if msg->sender != owner then { -/> } | .
{
    ::// exit_ {2} |.
}

String Type

Type:

string

Literals:

"Hello, World!"
"Token Name"
""  (* Empty string *)

Examples:

::// var 'name : string := "MyToken" .
::// var 'symbol : string := "MTK" .
::// var 'message : string := "Transfer successful" .

Operations:

  • Comparison: ==, !=
  • Concatenation: ++
  • Length: length(s)

Usage:

::// var 'fullName : string := firstName ++ " " ++ lastName .
::// var 'len : uint256 := length(name) .

Common patterns:

(* Error messages *)
::// require_(balance >= amount, "Insufficient balance") .

(* Event data *)
::// emit Transfer(from, to, amount, "Transfer completed") .

Bytes Types

Fixed-size bytes:

bytes1, bytes2, bytes4, bytes8, bytes16, bytes32

Dynamic bytes:

bytes

Examples:

::// var 'hash : bytes32 := keccak256(data) .
::// var 'signature : bytes := signatureData .

Operations:

  • Indexing: bytes[i]
  • Slicing: bytes[start:end]
  • Concatenation: ++

Unit Type

Type:

unit

Value:

tt  (* The only value of type unit *)

Usage:

  • Functions with no return value
  • Side-effect-only operations

Example:

Ursus Definition updateBalance (amount: uint256): UExpression unit false.
{
    ::// balance := balance + amount |.
}
return.
Defined.

Optional Type

Type:

optional T

Values:

Some value     (* Present *)
None           (* Absent *)

Examples:

::// var 'maybeBalance : optional uint256 := Some {1000} .
::// var 'notFound : optional address := None .

Pattern matching:

::// match maybeBalance with
     | Some bal => { ->> }
     | None => { ->> }
     end | .
{
    ::// useBalance(bal) |.
}
{
    ::// handleMissing() |.
}

Tuple Types

Syntax:

(T1 * T2 * ... * Tn)

Examples:

::// var 'pair : (uint256 * address) := ({100}, owner) .
::// var 'triple : (string * uint256 * boolean) := ("Token", {1000}, @true) .

Destructuring:

::// var '(amount, recipient) : (uint256 * address) := pair .

Type Conversions

Explicit Conversions

uint256(x)     (* Convert to uint256 *)
int256(x)      (* Convert to int256 *)
address(x)     (* Convert to address *)
bytes32(x)     (* Convert to bytes32 *)

Examples:

::// var 'addr : address := address({0x742d35Cc6634C0532925a3b844Bc9e7595f0bEb}) .
::// var 'bigNum : uint256 := uint256(smallNum) .

Implicit Conversions

Some conversions happen automatically:

  • Smaller to larger unsigned integers
  • ULValue to URValue

Example:

::// var 'x : uint8 := {10} .
::// var 'y : uint256 := x .  (* Implicit conversion *)

Type Aliases

Define custom type names:

Definition Balance := uint256.
Definition TokenId := uint256.
Definition Timestamp := uint64.

Usage:

::// var 'balance : Balance := {1000} .
::// var 'tokenId : TokenId := {42} .

See Also