Ursus as a Language

Ursus is a full-featured programming language for smart contracts, embedded in Coq. This section covers the language features, syntax, and semantics.

Language Overview

Ursus provides:

1. Type System - Rich type system with primitives, mappings, optionals, arrays
2. Contract Structure - Modular contract organization
3. Functions - Pure and stateful functions with verification support
4. State Management - Explicit state tracking and manipulation
5. Interfaces - Type-safe inter-contract communication
6. Inheritance - Code reuse through contract inheritance
7. Modifiers - Reusable function decorators

Contract Anatomy

A complete Ursus contract consists of:

(* 1. Imports *)
Require Import UrsusEnvironment.Solidity.current.Environment.
Require Import UrsusEnvironment.Solidity.current.LocalGenerator.

(* 2. Module *)
Module MyContract.

(* 3. Contract Header *)
#[translation = on]
#[language = solidity]
Contract MyContract ;
Sends To IExternal ;
Inherits BaseContract ;

(* 4. Types *)
Types
  Record User := {
      user_id: uint256;
      balance: uint256
  };
Constants
  Definition MAX_SUPPLY : uint256 := {1000000};

(* 5. Contract State *)
Record Contract := {
    totalSupply: uint256;
    users: mapping address User
}.

(* 6. Setup *)
SetUrsusOptions.
UseLocal Definition _ := [uint256; address; ...].

(* 7. Functions *)
Ursus Definition myFunction (arg: uint256): UExpression uint256 false.
{
    ::// ...
}
return.
Defined.
Sync.

(* 8. Finalization *)
EndContract Implements.
End MyContract.

Core Concepts

Types

Ursus supports:

• Primitives - uint8, uint256, int256, boolean, address
• Mappings - mapping K V (hash maps)
• Optionals - optional T (nullable values)
• Arrays - array T (dynamic arrays)
• Records - Custom struct types
• Enums - Enumeration types

Learn more: Types and Primitives

Contract Structure

Contracts are organized into:

• Header - Metadata and relationships
• Types - Custom type definitions
• Constants - Compile-time constants
• State - Contract storage fields
• Functions - Contract methods

Learn more: Contract Structure

Functions

Functions in Ursus:

• Have explicit signatures
• Track panic possibility
• Support modifiers
• Can be verified

Learn more: Functions, Writing Functions

State Management

State is:

• Explicitly tracked in the type system
• Modified through monadic operations
• Verifiable through Coq proofs

Learn more: Local State

Interfaces

Interfaces enable:

• Type-safe message passing
• Contract composition
• Modular design

Learn more: Interfaces and Messages

Language Features

Pattern Matching

::// match value with
     | Some x => { ->> }
     | None => { ->> }
     end | .
{
    ::// result := x |.
}
{
    ::// result := {0} |.
}

Loops

While loop:

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

For loop:

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

Error Handling

Require:

::// require_ (balance >= amount) .

Exit:

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

Type Safety

Ursus enforces:

1. Type correctness - All operations type-checked
2. Panic tracking - Functions marked as panicking/non-panicking
3. State consistency - State changes tracked in types
4. Interface compliance - Message sends type-checked

Example:

(* This won't compile - type mismatch *)
::// balance := "hello" .
(* Error: Expected uint256, got string *)

(* This won't compile - panic mismatch *)
Ursus Definition safe: UExpression uint256 false.
{
    ::// result := may_panic_function() |.
    (* Error: Cannot call panicking function in non-panicking context *)
}

Comparison with Other Languages

Next Steps

• Contract File Structure - Organize your contracts
• Types and Primitives - Type system details
• Functions - Writing contract functions
• Writing Functions - Detailed function guide
• Interfaces - Inter-contract communication
• Inheritance - Code reuse patterns

Examples

See complete examples in:

• Simple Contract - ERC20 token
• ursus-patterns repository - Pattern library with comprehensive examples