Introduction

Welcome to the Ursus documentation! Ursus is a revolutionary approach to smart contract development that combines the familiarity of languages like Solidity with the mathematical rigor of formal verification.

What is Ursus?

Ursus is a domain-specific language (eDSL) embedded in the Coq proof assistant, designed for writing and verifying smart contracts with mathematical certainty.

Think of Ursus as a bridge between two worlds:

• The familiar world of smart contract languages (Solidity, C++)
• The rigorous world of formal verification and mathematical proofs

Why Ursus?

Smart contracts handle real money and critical operations. A single bug can cost millions. Traditional testing can't guarantee correctness - but mathematical proofs can.

Ursus gives you:

1. Write Once, Verify Forever

Write your contract in a familiar syntax, then prove it's correct - mathematically:

Ursus Definition transfer (to: address) (amount: uint256):
  UExpression boolean false.
{
    ::// balances[[msg->sender]] := balances[[msg->sender]] - amount .
    ::// balances[[to]] := balances[[to]] + amount .
    ::// _result := @true |.
}
return.
Defined.

(* Now prove it preserves total supply *)
Theorem transfer_preserves_total_supply:
  forall from to amount s s',
    exec_transfer from to amount s = Some s' ->
    total_supply s' = total_supply s.
Proof.
  (* Mathematical proof here *)
Qed.

2. Familiar Syntax

If you know Solidity or C++, Ursus will feel natural:

Solidity:

function transfer(address to, uint256 amount) public returns (bool) {
    balances[msg.sender] -= amount;
    balances[to] += amount;
    return true;
}

Ursus:

Ursus Definition transfer (to: address) (amount: uint256):
  UExpression boolean false.
{
    ::// balances[[msg->sender]] := balances[[msg->sender]] - amount .
    ::// balances[[to]] := balances[[to]] + amount .
    ::// _result := @true |.
}
return.
Defined.

3. Executable and Verifiable

Your Ursus code is:

• Executable - Run it, test it, deploy it
• Verifiable - Prove properties about it
• Extractable - Generate Solidity/C++ code

4. Automated Assistance

Elpi automation generates boilerplate code, helping you focus on logic and proofs:

(* Write this *)
Contract ERC20 ;

(* Get this automatically generated *)
- Type definitions
- Field accessors
- State management
- Proof scaffolding

5. Formally Verified Core

The Ursus semantics itself is formally verified in Coq, ensuring the foundation is solid.

Key Features

How It Works

┌─────────────┐
│ Write Ursus │  ← Familiar syntax
│   Contract  │
└──────┬──────┘
       │
       ├─────────────────┐
       │                 │
       ▼                 ▼
┌─────────────┐   ┌─────────────┐
│   Execute   │   │    Prove    │
│  & Test     │   │ Properties  │
└──────┬──────┘   └──────┬──────┘
       │                 │
       │                 │
       ▼                 ▼
┌─────────────┐   ┌─────────────┐
│   Deploy    │   │ Guaranteed  │
│  to Chain   │   │  Correct    │
└─────────────┘   └─────────────┘

A Simple Example

Let's see a complete mini-contract:

(* Define the contract *)
Contract Counter ;
Sends To ;
Types ;
Constants ;

Record Contract := {
    count: uint256
}.

(* Implement increment function *)
Ursus Definition increment: UExpression PhantomType false.
{
    ::// count := count + {1} |.
}
return.
Defined.

(* Prove it always increases *)
Theorem increment_increases:
  forall s s',
    exec_increment s = Some s' ->
    count s' = count s + 1.
Proof.
  (* Proof here *)
Qed.

That's it! You have:

• ✅ A working contract
• ✅ A mathematical proof of correctness
• ✅ Code ready to deploy

Who Should Use Ursus?

Ursus is perfect for:

• DeFi Developers - Where bugs cost millions
• Security Researchers - Who need mathematical guarantees
• Smart Contract Auditors - Who want provable correctness
• Blockchain Engineers - Building critical infrastructure
• Academics - Researching formal methods

You should know:

• Basic smart contract concepts (Solidity/Ethereum)
• Some functional programming (helpful but not required)
• Willingness to learn formal verification (we'll teach you!)

What's in This Documentation?

This documentation is organized from beginner to advanced:

1. Installation - Get Ursus running
2. Quick Start - Your first contract in 10 minutes
3. Coq eDSL - How Ursus works under the hood
4. Ursus Language - Complete language reference
5. Programming Style - Best practices and patterns
6. Standard Library - Built-in functions and types
7. Verification - Proving your contracts correct
8. Long Start - Comprehensive tutorial
9. Translation - Converting from Solidity/C++
10. Advanced Topics - Expert-level features

Ready to Start?

Jump right in:

• New to Ursus? → Start with Quick Start
• Coming from Solidity? → Check Translation Guide
• Want to verify? → See Verification Principles
• Need examples? → Check the ursus-patterns repository in related projects

Get Help

• Documentation: Browse this book for comprehensive guides
• Examples: Check ursus-patterns repository for example contracts
• Community: Contact Pruvendo team for support

Let's build smart contracts we can trust! 🚀

Installation

This guide will help you install Ursus and all its dependencies. The installation process is straightforward and takes about 15-30 minutes.

Overview

Ursus is built on top of the Coq proof assistant and requires several components:

1. OPAM - OCaml package manager
2. Coq - The proof assistant (version 8.13 or later)
3. Dependencies - Required Coq libraries
4. Ursus Libraries - The Ursus language and tools

Quick Start

If you're experienced with Coq and OPAM:

# Install OPAM and Coq
opam install coq.8.13.2

# Install Ursus dependencies
opam repo add coq-released https://coq.inria.fr/opam/released
opam install coq-mathcomp-ssreflect coq-elpi

# Clone and install Ursus (contact Pruvendo for repository access)
git clone <ursus-repository-url>
cd ursus
make install

Detailed Installation

For a step-by-step guide, follow these sections:

1. Install OPAM

OPAM is the OCaml package manager used to install Coq and its libraries.

What you'll do:

• Install OPAM for your operating system
• Initialize OPAM environment
• Set up an OPAM switch for Coq

Time: ~5 minutes

2. Install Coq

Coq is the proof assistant that Ursus is built on.

What you'll do:

• Install Coq 8.13.2 (recommended version)
• Verify Coq installation
• Install CoqIDE (optional but recommended)

Time: ~10 minutes

3. Install Pruvendo Libraries

Install Ursus and its dependencies.

What you'll do:

• Install required Coq libraries
• Clone Ursus repositories
• Build and install Ursus
• Verify installation

Time: ~15 minutes

System Requirements

Supported Operating Systems

• Linux - Ubuntu 20.04+, Debian 10+, Fedora 33+
• macOS - 10.15 (Catalina) or later
• Windows - WSL2 (Windows Subsystem for Linux)

Hardware Requirements

• RAM: 4 GB minimum, 8 GB recommended
• Disk Space: 2 GB for Coq and Ursus
• CPU: Any modern processor (compilation can be slow on older CPUs)

Installation Methods

Method 1: OPAM (Recommended)

Install using OPAM package manager. This is the recommended method as it handles dependencies automatically.

Pros:

• Automatic dependency management
• Easy updates
• Multiple Coq versions support

Cons:

• Requires OPAM setup
• Can be slow on first install

Guide: Follow OPAM Installation → Coq Installation → Pruvendo Libraries

Method 2: Docker

Use pre-built Docker image with everything installed.

Pros:

• No local installation needed
• Consistent environment
• Quick setup

Cons:

• Requires Docker
• Larger disk usage
• May have performance overhead

Guide: See Docker Installation (coming soon)

Method 3: From Source

Build everything from source code.

Pros:

• Full control
• Latest development version
• Custom optimizations

Cons:

• Complex setup
• Manual dependency management
• Longer installation time

Guide: Advanced users only - see individual component documentation

Verification

After installation, verify everything works:

# Check Coq version
coqc --version
# Should show: The Coq Proof Assistant, version 8.13.2

# Check Ursus installation
coqc -Q . Ursus -R . UrsusEnvironment
# Should compile without errors

Troubleshooting

Common Issues

OPAM not found:

# Make sure OPAM is in your PATH
eval $(opam env)

Coq version mismatch:

# Switch to correct Coq version
opam switch create ursus 4.12.0
opam install coq.8.13.2

Build errors:

# Clean and rebuild
make clean
make -j4

Getting Help

If you encounter issues:

1. Check the FAQ (coming soon)
2. Contact Pruvendo team for support
3. Review the documentation thoroughly

Next Steps

Once installed, you're ready to start:

1. Quick Start - Write your first contract in 10 minutes
2. Ursus Language - Learn the language
3. Examples - Browse ursus-patterns repository for example contracts

Alternative: Try Online

Don't want to install locally? Try Ursus online:

• Coq Playground - Run Ursus in your browser (coming soon)
• Cloud IDE - Cloud development environment (coming soon)

Ready to install? Start with OPAM Installation →

Installing OPAM

OPAM is the OCaml package manager. We use it to install Coq and its libraries.

Linux

Ubuntu/Debian

sudo apt-get update
sudo apt-get install opam
opam init
eval $(opam env)

Fedora/RHEL

sudo dnf install opam
opam init
eval $(opam env)

Arch Linux

sudo pacman -S opam
opam init
eval $(opam env)

macOS

Using Homebrew

brew install opam
opam init
eval $(opam env)

Using MacPorts

sudo port install opam
opam init
eval $(opam env)

Windows

Use WSL2 (Windows Subsystem for Linux), then follow Linux instructions.

Create OPAM Switch

Create a dedicated environment for Ursus:

opam switch create ursus 4.12.0
eval $(opam env)

Verify Installation

opam --version
# Should show: 2.0.0 or later

Next Steps

Continue to Coq Installation →

Troubleshooting

OPAM command not found after installation:

eval $(opam env)
# Add to ~/.bashrc or ~/.zshrc:
echo 'eval $(opam env)' >> ~/.bashrc

Permission errors:

# Don't use sudo with opam commands
opam init --disable-sandboxing

Reference

• Official OPAM Documentation
• OPAM Basics

Installing Coq

Coq is the proof assistant that Ursus is built on. We use Coq 8.16.1.

Prerequisites

Make sure you have OPAM installed first.

Clean Previous Installations

Remove old Coq versions to avoid conflicts:

# Check if Coq is installed
coqc --version

# If found, remove it
opam remove coq

Install Coq

Create OPAM Switch

opam switch create coq-8.16 4.12.0
eval $(opam env)

Install Coq 8.16.1

opam pin add coq 8.16.1
eval $(opam env)

Verify Installation

coqc --version
# Should show: The Coq Proof Assistant, version 8.16.1

Install IDE

VS Code (Recommended)

1. Install VS Code: Download here

2. Install Coq Extension:

   • Open VS Code
   • Go to Extensions (Cmd+Shift+X / Ctrl+Shift+X)
   • Search for "vscoq1"
   • Install VsCoq

3. Install Math Unicode Extension (optional):

   • Search for "unicode-math-vscode"
   • Install Unicode Math

4. Test It:

   • Open any .v file
   • Use Alt+↓ to step forward
   • Use Alt+↑ to step backward

CoqIDE (Alternative)

opam install coqide

Common Issues

Build fails with missing system packages:

# Ubuntu/Debian
sudo apt-get install build-essential m4

# macOS
xcode-select --install

OPAM environment not updated:

eval $(opam env)
# Add to ~/.bashrc or ~/.zshrc:
echo 'eval $(opam env)' >> ~/.bashrc

Next Steps

Continue to Pruvendo Libraries Installation →

Reference

• Official Coq Installation
• Coq Documentation

Installing Pruvendo Libraries

Pruvendo libraries provide the Ursus language and verification tools.

Prerequisites

Make sure you have:

• OPAM installed
• Coq 8.16.1 installed

Ursus Libraries

The Ursus ecosystem consists of several libraries:

Core Libraries

coq-elpi-mod

• Modified Coq Elpi framework (based on LPCIC/coq-elpi)
• Enables code generation and automation

pruvendo-base

• Core primitive datatypes
• Monadic representation foundation

pruvendo-umlang

• The Ursus language itself
• Eval/Exec generators
• Formally verified semantics

Standard Libraries

pruvendo-base-lib

• Facts about primitive types
• Basic operations and proofs

ursus-standard-library

• Standard functions (integers, collections)
• Operators and notations
• See Standard Library

pruvendo-ursus-tvm

• Blockchain and VM abstractions
• State representation
• TVM-specific operations
• See TVM Library

Development Tools

ursus-contract-creator

• Elpi-based automation
• Contract scaffolding
• Proof code generation

ursus-proofs

• Proof automation helpers
• Common tactics

ursus-quickchick

• QuickChick integration for property-based testing
• Automated test generation
• See QuickChick Guide

ursus-environment

• Unified import interface
• Exports all Ursus resources

Installation

Option 1: Docker (Recommended)

Use pre-built Docker image:

docker pull pruvendo/ursus:latest
docker run -it pruvendo/ursus:latest

Option 2: From Source (NDA Required)

Contact Pruvendo for access:

# Clone repositories (requires access from Pruvendo)
git clone <ursus-repository-url>
cd ursus

# Install dependencies
opam repo add coq-released https://coq.inria.fr/opam/released
opam install coq-mathcomp-ssreflect

# Build and install
make -j4
make install

Verify Installation

Create a test file test.v:

Require Import UrsusEnvironment.

Contract Test ;
Sends To ;
Types ;
Constants ;

Record Contract := {
    value: uint256
}.

Ursus Definition getValue: UExpression uint256 false.
{
    ::// _result := value |.
}
return.
Defined.

Compile it:

coqc -Q . Ursus test.v
# Should compile without errors

Distribution Status

Current availability:

• Closed source development
• Source code shared under NDA
• Docker images available for evaluation
• Contact: Pruvendo

Disclaimer

Ursus libraries are under active development. No warranties are provided. We welcome collaboration and feedback.

Next Steps

Installation complete! Now:

1. Quick Start - Write your first contract
2. Ursus Language - Learn the language
3. Examples - Browse ursus-patterns repository for examples

Getting Help

• Issues: Contact Pruvendo support
• Documentation: This guide
• Examples: Check ursus-patterns repository

Quick Start

Get started with Ursus in 10 minutes. Write, compile, and deploy your first smart contract.

Prerequisites

Make sure you have Ursus installed.

What You'll Learn

1. Write a Simple Contract - Create your first Ursus contract
2. Compile from Solidity - Convert Solidity to Ursus
3. Compile Ursus - Extract executable code
4. Deploy - Deploy to blockchain (coming soon)

Your First Contract

Here's a minimal Ursus contract:

Require Import UrsusEnvironment.

Contract Counter ;
Sends To ;
Types ;
Constants ;

Record Contract := {
    count: uint256
}.

Ursus Definition increment: UExpression PhantomType false.
{
    ::// count := count + {1} |.
}
return.
Defined.

That's it! You have a working smart contract.

Next Steps

Choose your path:

Path 1: Learn by Example

→ Write a Simple Contract - Step-by-step tutorial

Path 2: Convert Existing Code

→ Compile from Solidity - Translate Solidity contracts

Path 3: Deep Dive

→ Ursus Language - Complete language reference

Quick Reference

Contract structure:

Contract Name ;          (* Contract declaration *)
Sends To ;              (* Message types *)
Types ;                 (* Custom types *)
Constants ;             (* Constants *)
Record Contract := {    (* State fields *)
    field: type
}.

Function definition:

Ursus Definition functionName (param: type): UExpression returnType false.
{
    ::// (* function body *) |.
}
return.
Defined.

Common operations:

::// field := value |.              (* Assignment *)
::// _result := expression |.       (* Return value *)
::// if (condition) then { ... } |. (* Conditional *)

Getting Help

• Examples: Check ursus-patterns repository for comprehensive examples
• Language Reference: Ursus Language
• Standard Library: Functions

Ready? → Write Your First Contract

Writing simple contract

Let's look to the simple contract erc20, which were written via Ursus.

Require Import UrsusEnvironment.Solidity.current.Environment.
Require Import UrsusEnvironment.Solidity.current.LocalGenerator.

Require Import UrsusContractCreator.UrsusFieldUtils.
Require Import IERC20.
Module ERC20.
#[translation = on]
#[language = solidity]
#[Contract = ERC20Contract]
Contract ERC20 ;
Sends To IERC20; 
Types ;
Constants ;
Record Contract := {
    totalSupply: uint256;
    balanceOf: mapping  ( address )( uint256 );
    allowance: mapping  ( address )( mapping  ( address )( uint256 ) )
}.
SetUrsusOptions.
UseLocal Definition _ := [
     boolean;
     address;
     uint256;

    (* added *)
     (mapping address uint256)
].
#[override, external, nonpayable,  returns=_result]
Ursus Definition transfer (recipient :  address) (amount :  uint256): UExpression ( boolean) false .
{
    :://  balanceOf[msg->sender] := balanceOf[msg->sender] - amount .
    :://  balanceOf[recipient]   := balanceOf[recipient] + amount .
    :://  send  IERC20.Transfer(msg->sender, recipient, amount) 
                => msg->sender 
                with {InternalMessageParamsLRecord} [$ {2} ⇒ {Message_ι_flag} $] .
    :://  _result := @true |.
}
return.
Defined.
Sync.

(*...*)

EndContract Implements.
End ERC20.

First part of describing contract is require needed Pruvendo libs.

Require Import UrsusEnvironment.Solidity.current.Environment.
Require Import UrsusEnvironment.Solidity.current.LocalGenerator.

Require Import UrsusContractCreator.UrsusFieldUtils.

Next is importing file with describing Interface IERC20.

Require Import IERC20.

Next command is Contract, which should be in the module with the same name.

#[translation = on]
#[language = solidity]
#[Contract = ERC20Contract]
Contract ERC20 ;
Sends To IERC20; 
Types ;
Constants ;
Record Contract := {
    totalSupply: uint256;
    balanceOf: mapping  ( address )( uint256 );
    allowance: mapping  ( address )( mapping  ( address )( uint256 ) );
}.

Attributes tells information about Contract: is needed tranlsation to Solidity, what is translating lang, name of raw term in Coq

#[translation = on]
#[language = solidity]
#[Contract = ERC20Contract]

Next one is command itself, which requires such as inforamation as:

1. Block

   Send to InterfaceName1 Interface2 ... ;
   

   describes information what interfaces are used in the contract.
2. Block

    Types 
    Record StructName1 := 
        StructName1 { 
            fieldName : type;
            ... 
        }
    Record StructName2 := 
    StructName2 { 
        fieldName : type;
        ... 
    }
     ...;
   

   declares new structures which are used in the contract.
3. Block

       Constants 
           Definition constName1: constType1 := constValue1
           Definition constName2: constType2 := constValue2
           ...
           Definition constNameN: constTypeN := constValueN        
       ;
   

   declares constants which are used in the contract.
4. Block

    Record Contract := {
        totalSupply: uint256;
        balanceOf: mapping  ( address )( uint256 );
        allowance: mapping  ( address )
                            ( mapping  ( address )( uint256 ) );
    }.
   

   describes fields of current contract.

Then tecknical command SetUrsusOptions. comes.

Important here is command UseLocal, more precisely

UseLocal Definition _ := [
     boolean;
     address;
     uint256;
     (mapping address uint256)
].

it declares local variables types, which will be used in functions below. (Important !) Arguments type, return type, type of declaring variables must be in UseLocal list!

Now let's look how we can describe function here. Example is

#[override, external, nonpayable,  returns=_result]
Ursus Definition transfer (recipient :  address) (amount :  uint256): UExpression ( boolean) false .
{
    :://  balanceOf[[msg->sender]] := balanceOf[[msg->sender]] - amount .
    :://  balanceOf[[recipient]]   := balanceOf[[recipient]] + amount .
    :://  send  IERC20.Transfer(msg->sender, recipient, amount) 
                => msg->sender 
                with {InternalMessageParamsLRecord} [$ {2} ⇒ {Message_ι_flag} $] .
    :://  _result := @true |.
}
return.
Defined.
Sync.

Main command is Ursus, which inputs some Definition. Attributes #[override, external, nonpayable, returns=_result] are the same as solidity has.

(Important !) Arguments type, and return type MUST BE in the UseLocal list! After switching Custom foo description to Proof mode 2 goals is here:

1. UExpression ( boolean) false It's main body of function, description of it is there oops TODO
2. IReturnExpression goal solves via tactic return. or return some_term. . It has ususal semanthic like in some imperative languages.
3. Defined. is standart Coq command.
4. Sync. is needed for fast interpreting.

Compiling Ursus Contracts

This guide explains how to compile Ursus contracts and extract them to target languages (Solidity, C++, or Rust).

Prerequisites

Before compiling, ensure you have:

• Coq installed (version 8.13 or later)
• Ursus libraries installed via opam
• Your contract file (.v extension)

See Installation for setup instructions.

Basic Compilation

Step 1: Compile with Coq

Compile your Ursus contract using coqc:

coqc -Q . MyProject MyContract.v

Options:

• -Q . MyProject - Maps current directory to logical path MyProject
• -R can be used instead of -Q for recursive mapping

Example:

coqc -Q . TokenContracts ERC20.v

Step 2: Verify Compilation

Successful compilation produces:

• MyContract.vo - Compiled object file
• MyContract.vok - Verification certificate
• MyContract.glob - Global symbol table

Check for errors:

coqc MyContract.v 2>&1 | grep -i error

Extraction to Target Languages

Ursus supports extraction to multiple target languages. The target language is specified in the contract attributes.

Extraction to Solidity

1. Set contract attributes:

#[translation = on]
#[language = solidity]
#[Contract = MyContract]
Contract MyContract ;

2. Compile with extraction:

coqc -Q . MyProject MyContract.v

3. Generated files:

• MyContract.sol - Solidity source code
• MyContract.abi.json - Contract ABI
• MyContract.bin - Compiled bytecode (if solc is available)

Extraction to C++

1. Set contract attributes:

#[translation = on]
#[language = cpp]
#[Contract = MyContract]
Contract MyContract ;

2. Compile:

coqc -Q . MyProject MyContract.v

3. Generated files:

• MyContract.cpp - C++ source code
• MyContract.hpp - Header file
• MyContract.tvc - TVM bytecode (if TON compiler is available)

Extraction to Rust

1. Set contract attributes:

#[translation = on]
#[language = rust]
#[Contract = MyContract]
Contract MyContract ;

2. Compile:

coqc -Q . MyProject MyContract.v

3. Generated files:

• MyContract.rs - Rust source code
• Cargo.toml - Cargo configuration (if not exists)

Using _CoqProject

For larger projects, use a _CoqProject file to manage compilation settings.

Create _CoqProject:

-Q . MyProject
-R ../ursus-standard-library Solidity
-R ../pruvendo-ursus-tvm TVM

MyContract.v
TokenSale.v
Vesting.v

Compile all files:

coq_makefile -f _CoqProject -o Makefile
make

Compilation Options

Disable Translation

To compile without generating target language code:

#[translation = off]
Contract MyContract ;

Use this for:

• Verification-only contracts
• Testing and development
• Proof-of-concept implementations

Enable QuickChick Testing

Generate property-based tests:

#[quickchick = on]
Contract MyContract ;

This generates:

• MyContract_test.v - QuickChick test suite
• Random test data generators
• Property verification tests

Troubleshooting

Common Errors

Error: "Cannot find library"

Error: Cannot find library Solidity.TVM.EverBase

Solution: Check your -Q or -R paths in _CoqProject

Error: "Extraction failed"

Error: Translation to solidity failed

Solution: Verify contract attributes and ensure #[translation = on]

Error: "Undefined reference"

Error: The reference fun01 was not found

Solution: Check function names and inheritance declarations

Verbose Output

Enable verbose compilation:

coqc -verbose MyContract.v

Debugging Extraction

Check generated intermediate files:

ls -la *.vo *.vok *.glob

Build Automation

Using Make

Create a Makefile:

.PHONY: all clean

COQC = coqc
COQFLAGS = -Q . MyProject

SOURCES = MyContract.v TokenSale.v

all: $(SOURCES:.v=.vo)

%.vo: %.v
	$(COQC) $(COQFLAGS) $<

clean:
	rm -f *.vo *.vok *.vos *.glob
	rm -f *.sol *.cpp *.rs

Build:

make

Using Dune

For projects using Dune build system:

Create dune file:

(coq.theory
 (name MyProject)
 (package my-contracts))

Build:

dune build

Next Steps

• Deploying Contracts - Deploy to blockchain
• Testing - Verify contract correctness
• Simple Example - Complete ERC20 example

See Also

• Contract Structure
• File Header
• Installation Guide

Compiling Generated Solidity Code

After extracting your Ursus contract to Solidity, you need to compile the generated .sol file for deployment to an EVM-compatible blockchain.

Prerequisites

• Solidity compiler (solc) version 0.8.0 or later
• Generated .sol file from Ursus extraction
• Node.js and npm (for Hardhat/Truffle)

Quick Compilation with solc

Install Solidity Compiler

Using npm:

npm install -g solc

Using binary:

# Download from Solidity releases page
# Or use version manager
brew install solidity  # macOS

Compile Contract

Basic compilation:

solc --bin --abi MyContract.sol -o build/

Options:

• --bin - Generate bytecode
• --abi - Generate ABI (Application Binary Interface)
• -o build/ - Output directory

Example:

solc --bin --abi ERC20.sol -o build/

Output files:

• build/ERC20.bin - Contract bytecode
• build/ERC20.abi - Contract ABI (JSON)

Optimization

Enable optimizer for gas efficiency:

solc --optimize --optimize-runs 200 --bin --abi MyContract.sol -o build/

Optimization levels:

• --optimize-runs 1 - Optimize for deployment cost
• --optimize-runs 200 - Balanced (default)
• --optimize-runs 1000000 - Optimize for execution cost

Using Hardhat

Hardhat is the recommended development environment for Solidity contracts.

Setup Hardhat Project

1. Initialize project:

mkdir my-ursus-project
cd my-ursus-project
npm init -y
npm install --save-dev hardhat

2. Create Hardhat config:

npx hardhat
# Select "Create an empty hardhat.config.js"

3. Install dependencies:

npm install --save-dev @nomiclabs/hardhat-ethers ethers

Configure Hardhat

Edit hardhat.config.js:

require("@nomiclabs/hardhat-ethers");

module.exports = {
  solidity: {
    version: "0.8.20",
    settings: {
      optimizer: {
        enabled: true,
        runs: 200
      }
    }
  },
  paths: {
    sources: "./contracts",
    artifacts: "./artifacts"
  }
};

Compile with Hardhat

1. Place contract in contracts/ directory:

mkdir -p contracts
cp MyContract.sol contracts/

2. Compile:

npx hardhat compile

Output:

• artifacts/contracts/MyContract.sol/MyContract.json - ABI and bytecode
• Compilation artifacts in artifacts/ directory

Verify Compilation

npx hardhat compile --force

Check for warnings:

npx hardhat compile 2>&1 | grep -i warning

Using Truffle

Truffle is another popular development framework.

Setup Truffle Project

1. Install Truffle:

npm install -g truffle

2. Initialize project:

mkdir my-ursus-project
cd my-ursus-project
truffle init

Configure Truffle

Edit truffle-config.js:

module.exports = {
  compilers: {
    solc: {
      version: "0.8.20",
      settings: {
        optimizer: {
          enabled: true,
          runs: 200
        }
      }
    }
  }
};

Compile with Truffle

1. Place contract in contracts/ directory:

cp MyContract.sol contracts/

2. Compile:

truffle compile

Output:

• build/contracts/MyContract.json - ABI and bytecode

Handling Dependencies

If your generated Solidity code imports other contracts:

OpenZeppelin Contracts

npm install @openzeppelin/contracts

In Solidity:

import "@openzeppelin/contracts/token/ERC20/ERC20.sol";

Custom Imports

Ensure all imported files are in the correct directory structure:

contracts/
├── MyContract.sol
├── interfaces/
│   └── IERC20.sol
└── libraries/
    └── SafeMath.sol

Compilation Errors

Common Issues

Error: "Source file requires different compiler version"

Error: Source file requires different compiler version

Solution: Update solidity version in config to match contract pragma

Error: "Undeclared identifier"

Error: Undeclared identifier 'SafeMath'

Solution: Install missing dependencies or add import statements

Error: "Stack too deep"

Error: Stack too deep when compiling inline assembly

Solution: Refactor function to use fewer local variables or enable optimizer

Debugging

Verbose compilation:

solc --verbose MyContract.sol

Check AST:

solc --ast-compact-json MyContract.sol

Verification

After compilation, verify the contract:

Check Bytecode Size

# Bytecode should be < 24KB for deployment
wc -c build/MyContract.bin

Verify ABI

# Check ABI is valid JSON
cat build/MyContract.abi | jq .

Gas Estimation

Using Hardhat:

const Contract = await ethers.getContractFactory("MyContract");
const contract = await Contract.deploy();
console.log("Deployment gas:", contract.deployTransaction.gasLimit);

Next Steps

• Deploy Contract - Deploy to blockchain
• Testing - Test contract functionality
• Verification - Verify contract correctness

See Also

• Compiling Ursus - Ursus compilation process
• Simple Example - Complete workflow example
• Hardhat Documentation
• Solidity Documentation

Coq Embedded DSL

Ursus is implemented as an embedded domain-specific language (eDSL) within the Coq proof assistant. This design choice enables formal verification of smart contracts while maintaining a familiar programming syntax.

What is an Embedded DSL?

An embedded DSL is a specialized language implemented within a host language (in this case, Coq). Unlike standalone languages that require their own parser and compiler, embedded DSLs leverage the host language's infrastructure while providing domain-specific abstractions.

Benefits of Embedding in Coq

1. Formal Verification - Prove mathematical properties about contracts
2. Type Safety - Leverage Coq's powerful type system
3. Proof Automation - Use Coq's tactics for automated reasoning
4. Extraction - Generate executable code in multiple target languages
5. Reusability - Share proofs and abstractions across contracts

Ursus Architecture

┌─────────────────────────────────────────┐
│         Ursus Contract Code             │
│    (Custom Coq syntax + notations)      │
└──────────────┬──────────────────────────┘
               │
               ▼
┌─────────────────────────────────────────┐
│      Coq Custom Grammar Extension       │
│   (Defines Ursus-specific syntax)       │
└──────────────┬──────────────────────────┘
               │
               ▼
┌─────────────────────────────────────────┐
│         Ursus Embedding Layer           │
│  (Maps syntax to Coq terms/types)       │
└──────────────┬──────────────────────────┘
               │
               ▼
┌─────────────────────────────────────────┐
│      Coq Core (Gallina + Tactics)       │
│   (Type checking, proof verification)   │
└──────────────┬──────────────────────────┘
               │
               ├──────────────┬─────────────┐
               ▼              ▼             ▼
         Verification    Extraction    Simulation
         (Proofs)        (Solidity)    (Testing)

Key Components

1. Custom Grammar

Ursus extends Coq's grammar to support smart contract syntax through three core inductive types:

• URValue - Right values (expressions that produce values)
• ULValue - Left values (assignable locations)
• UExpression - Statements and control flow

Contract ERC20 ;
Sends To IERC20 ;
Inherits ;

This looks like a domain-specific language but is actually valid Coq code thanks to custom grammar rules.

Learn more:

• Custom Grammar - Contract-level syntax
• URValue Grammar - Right value constructors
• ULValue Grammar - Left value constructors
• UExpression Grammar - Statement constructors

2. Embedding Layer

The embedding layer maps high-level contract constructs to Coq's type theory:

• Contracts → Coq records
• Functions → Coq definitions with monadic types
• State → Coq record fields
• Expressions → Typed Coq terms (URValue/ULValue/UExpression)

Learn more: Ursus Embedding

3. Notational Mechanism

Notations make Ursus code readable and familiar to smart contract developers:

(* Ursus notation *)
balance := balance + amount

(* Underlying Coq term *)
AssignExpression (ULState balance) (URIndex (URState balance) (URScalar amount))

Learn more: Notations

How Ursus Works

Writing a Contract

When you write an Ursus contract:

#[translation = on]
#[language = solidity]
Contract Token ;
Sends To ;
Inherits ;

Record Contract := {
    totalSupply: uint256;
    balances: mapping address uint256
}.

Ursus Definition transfer (to: address) (amount: uint256): UExpression boolean false.
{
    :// balances[msg->sender] := balances[msg->sender] - amount.
    :// balances[to] := balances[to] + amount.
    :// return true.
}
return.
Defined.

What Happens Internally

1. Parsing - Coq parser processes custom syntax using grammar extensions
2. Elaboration - Ursus notations expand to Coq terms
3. Type Checking - Coq verifies type correctness
4. Embedding - Contract constructs map to formal semantics
5. Extraction - Code generator produces target language (Solidity/C++/Rust)

The Monadic Foundation

Ursus uses a state monad to model contract execution:

UExpression (A: Type) (b: bool) :=
  ContractState -> (A * ContractState) + Error

This encoding:

• Tracks state changes explicitly
• Enables reasoning about side effects
• Supports formal verification
• Allows extraction to imperative code

Verification Workflow

1. Write Contract
   ↓
2. Define Properties (Specifications)
   ↓
3. Prove Properties (Using Coq tactics)
   ↓
4. Extract Verified Code
   ↓
5. Deploy to Blockchain

Example property:

Theorem transfer_preserves_total_supply:
  forall (from to: address) (amount: uint256) (s s': ContractState),
    exec_transfer from to amount s = Some s' ->
    total_supply s = total_supply s'.

Comparison with Other Approaches

Getting Started

1. Learn Coq Basics - Understand Coq's type system and tactics
2. Study Custom Grammar - See how Ursus extends Coq syntax
3. Understand Embedding - Learn how contracts map to Coq terms
4. Master Notations - Write idiomatic Ursus code
5. Practice Verification - Prove properties about your contracts

Next Steps

• Custom Grammar - Ursus syntax extensions
• Ursus Embedding - Semantic foundations
• Notations - Writing readable contracts
• Simple Example - Complete contract walkthrough

Further Reading

• Coq Reference Manual
• Software Foundations
• Certified Programming with Dependent Types

Custom Grammar Extensions

Ursus extends Coq's grammar to provide a domain-specific syntax for smart contracts. This makes Ursus code look like a specialized programming language while remaining valid Coq code.

Overview

Coq allows custom grammar extensions through its notation mechanism and custom entry points. Ursus leverages this to create contract-specific syntax that is:

1. Familiar - Resembles Solidity and other smart contract languages
2. Type-safe - Fully checked by Coq's type system
3. Verifiable - Can be reasoned about using Coq proofs
4. Extractable - Translates to target languages

Contract-Level Grammar

Contract Declaration

Syntax:

Contract ContractName ;

What it does:

• Declares a new contract module
• Initializes contract metadata
• Sets up the contract namespace

Underlying Coq: This is a custom command that generates:

• Module definitions
• Type declarations
• Metadata records

Sends To Declaration

Syntax:

Sends To Interface1 Interface2 ... ;

What it does:

• Declares external interfaces this contract can call
• Enables type checking for inter-contract calls
• Generates interface bindings

Examples:

Sends To IERC20 IOwnable ;  (* Multiple interfaces *)
Sends To ;                   (* No external calls *)

Inherits Declaration

Syntax:

Inherits Parent1 Parent2 ... ;
Inherits Parent => overrides [method1 method2] ;

What it does:

• Specifies parent contracts
• Controls method inheritance
• Enables selective overriding

Types Section

Syntax:

Types
  Record TypeName := {
      field1: type1;
      field2: type2
  },
  Inductive EnumName :=
    | Constructor1
    | Constructor2
  ;

What it does:

• Defines custom data structures
• Creates record types
• Declares enumerations

Constants Section

Syntax:

Constants
  Definition CONSTANT_NAME : type := value
  Definition ANOTHER_CONST : type := value
;

What it does:

• Declares contract-level constants
• Provides compile-time values
• Enables constant folding

Contract Record

Syntax:

Record Contract := {
    field1: type1;
    field2: type2;
    #[static] staticField: type3
}.

What it does:

• Defines contract state structure
• Specifies storage layout
• Marks static (immutable) fields

Function-Level Grammar

Function Declaration

Syntax:

#[attribute1, attribute2]
Ursus Definition functionName (arg1: type1) (arg2: type2):
  UExpression returnType panicFlag.
{
    (* function body *)
}
return.
Defined.
Sync.

Components:

• #[...] - Function attributes (visibility, modifiers)
• Ursus Definition - Function declaration keyword
• UExpression - Monadic return type
• panicFlag - Can function panic? (true/false)
• return - Return statement
• Defined - Coq definition terminator
• Sync - Synchronize with code generator

Function Attributes

#[pure]                    (* No state modification *)
#[view]                    (* Read-only function *)
#[public]                  (* Publicly callable *)
#[external]                (* External interface *)
#[internal]                (* Internal only *)
#[override]                (* Overrides parent *)
#[payable]                 (* Can receive funds *)
#[nonpayable]              (* Cannot receive funds *)
#[returns=varName]         (* Named return variable *)
#[write=arg]               (* Mutable argument *)
#[no_body]                 (* Interface declaration *)

Statement-Level Grammar

Statement Notation

Ursus uses special notation for statements within function bodies:

Basic form:

::// statement .

With continuation:

::// statement1 .
::// statement2 .
::// statement3 |.

Notation symbols:

• :: - Statement introducer (custom tactic)
• // - Statement delimiters
• . - Statement separator (more statements follow)
• | - Statement terminator (last statement)

Variable Declaration

Syntax:

::// var 'varName : type := value .
::// new 'varName : type @ "name" := value .

Examples:

::// var 'x : uint256 := {0} .
::// new 'balance : uint256 @ "balance" := {1000} .

Difference:

• var - Simple local variable
• new - Named variable (appears in generated code with specific name)

Assignment

Syntax:

::// variable := expression .

Examples:

::// balance := balance + amount .
::// owner := msg->sender .
::// approved := @true .

Array/Mapping Access

Syntax:

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

Examples:

::// balances[[msg->sender]] := {0} .
::// allowance[[owner]][[spender]] := amount .

Control Flow

If-Then:

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

If-Then-Else:

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

While Loop:

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

For Loop:

::// for 'i in range do { ->> } | .
{
    (* loop body *)
}

Panic Flags (Holes)

The ->> and -/> symbols indicate whether a code block can panic:

• ->> - Block completes normally (no panic)
• -/> - Block may panic (can exit early)

Example:

::// if balance < amount then { ->/> } else { ->> } | .
{
    ::// exit_ {1} |.  (* Panic exit *)
}
{
    ::// balance := balance - amount |.  (* Normal execution *)
}

Expression-Level Grammar

Literals

{42}           (* Numeric literal *)
{0xFF}         (* Hex literal *)
@true          (* Boolean true *)
@false         (* Boolean false *)
"string"       (* String literal *)

Operators

Arithmetic:

a + b          (* Addition *)
a - b          (* Subtraction *)
a * b          (* Multiplication *)
a / b          (* Division *)
a % b          (* Modulo *)

Comparison:

a == b         (* Equality *)
a != b         (* Inequality *)
a < b          (* Less than *)
a > b          (* Greater than *)
a <= b         (* Less or equal *)
a >= b         (* Greater or equal *)

Logical:

a && b         (* Logical AND *)
a || b         (* Logical OR *)
!a             (* Logical NOT *)

Bitwise:

a & b          (* Bitwise AND *)
a | b          (* Bitwise OR *)
a ^ b          (* Bitwise XOR *)
~a             (* Bitwise NOT *)
a << n         (* Left shift *)
a >> n         (* Right shift *)

Message Access

msg->sender    (* Message sender *)
msg->value     (* Message value *)
msg->data      (* Message data *)

Function Calls

Internal:

::// result := functionName(arg1, arg2) .

External:

::// send Interface.Method(args) => target with params .

Grammar Levels and Scopes

Ursus grammar is organized into multiple levels:

Level 1: Core Inductive Types

The foundation of Ursus grammar consists of three inductive types defined in UrsusCore.v:

1. URValueP - Right values (expressions)
2. ULValueP - Left values (locations)
3. UExpressionP - Statements and control flow

These types define the abstract syntax tree of Ursus programs.

Learn more:

• URValue Grammar
• ULValue Grammar
• UExpression Grammar

Level 2: Notation Scopes

Notations provide readable syntax for the core types:

ursus_scope - Core Ursus primitives:

Local Open Scope ursus_scope.

# 42                    (* URScalar *)
μ Ledger_MainState     (* URState *)
r ^^ field             (* URField *)
m [[ i ]]              (* URIndex *)

usolidity_scope - Solidity-like syntax:

Local Open Scope usolidity_scope.

::// statement .       (* Statement notation *)
x := e                 (* Assignment *)
a + b                  (* Operators *)
if c then e1 else e2   (* Conditionals *)

record scope - Record field access:

Local Open Scope record.

s.(field)              (* Field projection *)
s <| field := v |>     (* Field update *)

Level 3: Contract-Level Commands

Custom Coq commands for contract structure:

• Contract Name ; - Contract declaration
• Sends To ... ; - Interface declarations
• Inherits ... ; - Inheritance
• Types ... ; - Type definitions
• Constants ... ; - Constant definitions

Level 4: Function-Level Tactics

Tactics for writing function bodies:

• ::// statement . - Statement introducer
• {->>} - Block delimiter
• return - Return statement
• var 'x := e - Variable declaration

Grammar Extension Mechanism

Ursus extends Coq's grammar using:

1. Notations - Syntactic sugar for terms
2. Custom entries - New grammar categories
3. Tactics - Proof mode extensions
4. Commands - Top-level declarations

Example: Assignment notation

Notation "x := e" := (AssignExpression x e default)
  (at level 70, no associativity) : usolidity_scope.

This notation:

• Operates at precedence level 70
• Is non-associative
• Is active in usolidity_scope
• Expands to AssignExpression constructor

See Also

• Ursus Embedding - How syntax maps to semantics
• Notations - Detailed notation definitions
• URValue Grammar - Right value constructors
• ULValue Grammar - Left value constructors
• UExpression Grammar - Statement constructors
• Writing Functions - Function syntax guide

Ursus Embedding

The Ursus embedding layer provides the formal semantics that map high-level contract syntax to Coq's type theory. This layer is the foundation for verification and code generation.

Overview

Embedding is the process of representing domain-specific constructs (smart contracts) using the host language's primitives (Coq). Ursus achieves this through:

1. Monadic encoding - State and effects as explicit types
2. Type mapping - Contract types to Coq types
3. Semantic functions - Operations with formal meaning
4. Proof infrastructure - Reasoning about contract behavior

The State Monad

UExpression Type

The core of Ursus is the UExpression monad:

UExpression (A: Type) (b: bool) :=
  ContractState -> Result (A * ContractState)

Type parameters:

• A - Return type of the expression
• b - Panic flag (true = can panic, false = cannot panic)

Semantics:

• Takes current contract state
• Returns either:
  • Success (value, new_state) - Normal execution
  • Error error_code - Exceptional termination

Why a Monad?

Monads allow us to:

1. Sequence operations - Chain state transformations
2. Track side effects - Make state changes explicit
3. Handle errors - Model exceptional control flow
4. Enable verification - Reason about state transitions

Example:

(* High-level Ursus *)
::// balance := balance + amount .

(* Underlying monadic computation *)
do current_balance <- read_balance;
   new_balance <- add current_balance amount;
   write_balance new_balance

Value Types: ULValue and URValue

Ursus distinguishes between left values (assignable) and right values (readable). These are defined as inductive types with multiple constructors.

ULValue (Left Value)

Definition:

Inductive ULValueP : Type -> Type :=
    | ULState  : ... -> ULValueP U
    | ULField  : ... -> ULValueP U -> ULValueP (field_type f)
    | ULIndex  : ... -> ULValueP V
    | ULLocalIndex : ... -> ULValueP V
    | ULTuple : ... -> ULValueP (XProd A B)
    | ULFirst : ... -> ULValueP A
    | ULSecond : ... -> ULValueP B
    | ULUnMaybe: ... -> ULValueP A.

Represents:

• Storage locations (state variables) - ULState
• Record fields - ULField
• Mapping/array entries - ULIndex, ULLocalIndex
• Tuple components - ULTuple, ULFirst, ULSecond
• Optional values - ULUnMaybe

Operations:

• Can be read from (via coercion to URValue)
• Can be written to
• Can be passed by reference

Examples:

→ μ Ledger_MainState : ULValue ContractState
→ balances [[ addr ]] : ULValue uint256
→ user ^^ User_name : ULValue string

Learn more: ULValue Grammar

URValue (Right Value)

Definition:

Inductive URValueP : Type -> bool -> Type :=
    | URScalar : ... -> URValueP X false
    | URResult : ... -> URValueP X b
    | URState  : ... -> URValueP U false
    | URField  : ... -> URValueP (field_type f) b
    | URIndex  : ... -> URValueP V (bK || bM)
    | URLocalIndex : ... -> URValueP V false
    | URTuple : ... -> URValueP (XProd A B) (bA || bB)
    | UR3arn  : ... -> URValueP X (b1 || b2 || b3)
    | URFirst : ... -> URValueP A bA
    | URSecond : ... -> URValueP B bB
    | URUnMaybe: ... -> URValueP A b.

Type parameters:

• Type - Value type
• bool - Panic flag (false = cannot panic, true = may panic)

Represents:

• Literals - URScalar
• Monadic computations - URResult
• State access - URState
• Field access - URField
• Indexing - URIndex, URLocalIndex
• Tuples - URTuple, URFirst, URSecond
• Conditionals - UR3arn
• Optional unwrapping - URUnMaybe

Operations:

• Can be read from
• Cannot be written to
• Passed by value

Examples:

# 42 : URValue uint256 false       (* Literal *)
a + b : URValue uint256 false      (* Expression *)
foo() : URValue uint256 true       (* Function call *)
μ Ledger_MainState : URValue ContractState false
balances [[ addr ]] : URValue uint256 b

Learn more: URValue Grammar

Automatic Coercion

Ursus automatically converts ULValue to URValue when needed:

(* balance is ULValue, automatically coerced to URValue *)
::// total := balance + {100} .

Coercion rule: ULValue T → URValue T false

Type Mapping

Primitive Types

Complex Types

Mapping:

mapping K V := K -> option V

Optional:

optional T := option T

Arrays:

array T := list T

Records:

Record User := {
    user_id: uint256;
    balance: uint256
}.
(* Maps to Coq record with same structure *)

Contract State

State Record

The contract state is a Coq record containing all state variables:

Record ContractState := {
    totalSupply: uint256;
    balances: mapping address uint256;
    owner: address
}.

State Access

Reading state:

get_balance : UExpression uint256 false :=
  fun s => Success (s.(balances), s)

Writing state:

set_balance (new_bal: uint256) : UExpression unit false :=
  fun s => Success (tt, s <| balances := new_bal |>)

State Transformations

State updates use Coq's record update syntax:

s <| field := new_value |>

Multiple updates:

s <| field1 := value1 |>
  <| field2 := value2 |>

Expression Semantics

Literals

Numeric literals:

{42} : URValue uint256 false
(* Semantics: λs. Success (42, s) *)

Boolean literals:

@true : URValue boolean false
(* Semantics: λs. Success (true, s) *)

Operators

Arithmetic:

a + b : URValue uint256 b
(* Semantics:
   do va <- eval a;
      vb <- eval b;
      return (va + vb)
*)

Comparison:

a < b : URValue boolean b
(* Semantics:
   do va <- eval a;
      vb <- eval b;
      return (va <? vb)
*)

Assignment

x := e : UExpression unit b
(* Semantics:
   do v <- eval e;
      write_location x v
*)

Control Flow

Conditional

if c then e1 else e2 : UExpression A b
(* Semantics:
   do vc <- eval c;
      if vc then eval e1 else eval e2
*)

Loops

While loop:

while c do body : UExpression unit true
(* Semantics: Fixed-point iteration with termination check *)

For loop:

for i in range do body : UExpression unit true
(* Semantics: Bounded iteration over range *)

Function Calls

Internal Calls

f(arg1, arg2) : UExpression RetType b
(* Semantics: Direct function application *)

External Calls

send Interface.Method(args) => target with params
(* Semantics: Message construction and dispatch *)

Error Handling

Panic Flag

The boolean parameter b in UExpression A b indicates panic possibility:

• false - Cannot panic (total function)
• true - May panic (partial function)

Type safety:

(* OK: Combining non-panicking expressions *)
e1 : UExpression A false
e2 : UExpression B false
e1 >> e2 : UExpression B false

(* Panicking propagates *)
e1 : UExpression A true
e2 : UExpression B false
e1 >> e2 : UExpression B true

Exit and Require

Exit:

exit_ code : UExpression A true
(* Semantics: λs. Error code *)

Require:

require_ condition : UExpression unit true
(* Semantics:
   if condition then Success (tt, s)
   else Error default_error_code
*)

Verification Support

Hoare Logic

Ursus supports Hoare-style reasoning:

{{ P }}  (* Precondition *)
  code
{{ Q }}  (* Postcondition *)

Example:

{{ balance >= amount }}
  balance := balance - amount
{{ balance_old = balance + amount }}

Invariants

Contract invariants can be expressed and proven:

Definition total_supply_invariant (s: ContractState) : Prop :=
  s.(totalSupply) = sum_balances s.(balances).

Theorem transfer_preserves_invariant:
  forall s s' from to amount,
    total_supply_invariant s ->
    exec_transfer from to amount s = Some s' ->
    total_supply_invariant s'.

Code Generation

Extraction Process

1. Monadic code → Imperative code
2. UExpression → Statements
3. State monad → State mutations

Example transformation:

(* Ursus/Coq *)
do x <- read_balance;
   write_balance (x + 1)

(* Generated Solidity *)
uint256 x = balance;
balance = x + 1;

Target Languages

• Solidity - Ethereum/EVM
• C++ - TON/TVM
• Rust - Various platforms

See Also

• Custom Grammar - Syntax extensions
• Notations - Notation definitions
• Verification - Proving properties
• Writing Functions - Practical usage

Core Grammar: URValue and ULValue

This section explains the core grammar of Ursus, focusing on the inductive types that define right values (URValue) and left values (ULValue).

Overview

Ursus's grammar is built on three fundamental inductive types defined in UrsusCore.v:

1. URValueP - Right values (expressions that produce values)
2. ULValueP - Left values (locations that can be assigned to)
3. UExpressionP - Statements and control flow

These types form a custom grammar that extends Coq's syntax to support smart contract programming.

URValueP: Right Value Grammar

Definition

Inductive URValueP : Type -> bool -> Type := 
    | URScalar : forall {X}, X -> URValueP X false
    | URResult : forall {b X}, LedgerT (ControlResultP X b) -> URValueP X b
    | URState  : forall {U} {f: LedgerFields}`{EmbeddedType (field_type f) U}, 
                 URValueP U false               
    | URField  : forall {b} {U:Type} {FU:Set} (f:FU)`{PruvendoRecord U FU}, 
                 URValueP U b -> URValueP (field_type f) b
    | URIndex  : forall {bK bM} {K C V} (rk: URValueP K bK) (lv: URValueP C bM) 
                 `{Container K C V} `{XBoolEquable XBool K}`{XDefault V}, 
                 URValueP V (bK || bM)
    | URLocalIndex : forall {K C V} (k: K) (lv: URValueP C false) 
                     `{ContainerLocal K C V} `{XBoolEquable XBool K}`{XDefault V}, 
                     URValueP V false
    | URTuple : forall {A bA B bB}, URValueP A bA -> URValueP B bB -> 
                URValueP (XProd A B) (bA || bB)
    | UR3arn  : forall {b1 b2 b3 X}, URValueP XBool b1 -> URValueP X b2 -> 
                URValueP X b3 -> URValueP X (b1 || b2 || b3)
    | URFirst : forall {A B bA}, URValueP (XProd A B) bA -> URValueP A bA
    | URSecond : forall {A B bB}, URValueP (XProd A B) bB -> URValueP B bB
    | URUnMaybe: forall {A}`{XDefault A} {b}, URValueP (XMaybe A) b -> URValueP A b.

Type Parameters

• First parameter (Type) - The value type (e.g., uint256, address)
• Second parameter (bool) - Panic flag:
  • false - Cannot panic (pure computation)
  • true - May panic (can fail at runtime)

Constructors

URScalar - Literal Values

URScalar : forall {X}, X -> URValueP X false

Purpose: Embed Coq values as Ursus literals

Notation: # e

Examples:

# 42 : URValue uint256 false
# true : URValue boolean false
# "hello" : URValue string false

Panic flag: Always false (literals never panic)

URResult - Monadic Computations

URResult : forall {b X}, LedgerT (ControlResultP X b) -> URValueP X b

Purpose: Wrap monadic computations (function calls, state access)

Examples:

URResult (balanceOf(addr)) : URValue uint256 true
URResult (pure_function(x)) : URValue uint256 false

Panic flag: Inherited from the computation

URState - State Variable Access

URState : forall {U} {f: LedgerFields}`{EmbeddedType (field_type f) U}, 
          URValueP U false

Purpose: Access contract state variables

Notation: μ e

Examples:

μ Ledger_MainState : URValue ContractState false

Panic flag: Always false (state access is pure)

URField - Record Field Access

URField : forall {b} {U:Type} {FU:Set} (f:FU)`{PruvendoRecord U FU}, 
          URValueP U b -> URValueP (field_type f) b

Purpose: Access fields of records/structs

Notation: r ^^ f

Examples:

user ^^ User_balance : URValue uint256 b
(μ Ledger_MainState) ^^ Contract_totalSupply : URValue uint256 false

Panic flag: Inherited from the record expression

URIndex - Mapping/Array Indexing

URIndex : forall {bK bM} {K C V} (rk: URValueP K bK) (lv: URValueP C bM) 
          `{Container K C V} `{XBoolEquable XBool K}`{XDefault V}, 
          URValueP V (bK || bM)

Purpose: Index into mappings, arrays, or other containers

Notation: m [[ i ]]

Examples:

balances [[ addr ]] : URValue uint256 (b_addr || b_balances)
array [[ {0} ]] : URValue uint256 b_array

Panic flag: bK || bM (panics if either key or container can panic)

Type classes:

• Container K C V - C is a container with keys K and values V
• XBoolEquable XBool K - Keys are comparable
• XDefault V - Values have a default (for missing keys)

URLocalIndex - Static Indexing

URLocalIndex : forall {K C V} (k: K) (lv: URValueP C false) 
               `{ContainerLocal K C V} `{XBoolEquable XBool K}`{XDefault V}, 
               URValueP V false

Purpose: Index with a compile-time constant key

Notation: m [[_ i _]]

Examples:

local_map [[_ addr_constant _]] : URValue uint256 false

Panic flag: Always false (static indexing is safe)

Difference from URIndex: Key is a Coq value, not an URValue

URTuple - Tuple Construction

URTuple : forall {A bA B bB}, URValueP A bA -> URValueP B bB -> 
          URValueP (XProd A B) (bA || bB)

Purpose: Create pairs/tuples

Examples:

URTuple (# 42) (# "hello") : URValue (uint256 # string) false

Panic flag: bA || bB (panics if either component can panic)

UR3arn - Ternary Operator

UR3arn : forall {b1 b2 b3 X}, URValueP XBool b1 -> URValueP X b2 -> 
         URValueP X b3 -> URValueP X (b1 || b2 || b3)

Purpose: Conditional expression (ternary ? :)

Examples:

UR3arn condition then_value else_value : URValue X (b1 || b2 || b3)

Panic flag: b1 || b2 || b3 (panics if any branch can panic)

URFirst / URSecond - Tuple Projection

URFirst : forall {A B bA}, URValueP (XProd A B) bA -> URValueP A bA
URSecond : forall {A B bB}, URValueP (XProd A B) bB -> URValueP B bB

Purpose: Extract components from tuples

Examples:

URFirst pair : URValue A b
URSecond pair : URValue B b

Panic flag: Inherited from the tuple

URUnMaybe - Optional Unwrapping

URUnMaybe: forall {A}`{XDefault A} {b}, URValueP (XMaybe A) b -> URValueP A b

Purpose: Unwrap optional values (with default on None)

Examples:

URUnMaybe maybe_value : URValue A b

Panic flag: Inherited from the optional value

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

See Also

• ULValue Grammar - Left value grammar
• UExpression Grammar - Expression grammar
• Notations - Notation definitions

ULValue Grammar: Left Values

This section explains the ULValue (Left Value) grammar - the subset of Ursus expressions that represent assignable locations.

Overview

ULValue represents locations in memory or storage that can be:

• Read from - Coerced to URValue
• Written to - Target of assignment
• Passed by reference - Modified by functions

Unlike URValue, ULValue has no panic flag because locations themselves don't panic (only operations on them can).

ULValueP Definition

Inductive ULValueP : Type -> Type := 
    | ULState  : forall {U} {f: LedgerFields}`{EmbeddedType (field_type f) U}, 
                 ULValueP U    
    | ULField  : forall {U:Type} {FU:Set} (f:FU)`{PruvendoRecord U FU}, 
                 ULValueP U -> ULValueP (field_type f)        
    | ULIndex  : forall {K C V} (rk: URValueP K false) (lv:ULValueP C) 
                 `{Container K C V}`{XBoolEquable XBool K}`{XDefault V},
                 ULValueP V
    | ULLocalIndex : forall {K C V} (k: K) (lv:ULValueP C) 
                     `{ContainerLocal K C V} `{XBoolEquable XBool K}`{XDefault V},
                     ULValueP V
    | ULTuple : forall {A B}, ULValueP A -> ULValueP B -> ULValueP (XProd A B) 
    | ULFirst : forall {A B}, ULValueP (XProd A B) -> ULValueP A
    | ULSecond : forall {A B}, ULValueP (XProd A B) -> ULValueP B
    | ULUnMaybe: forall {A}`{XDefault A}, ULValueP (XMaybe A) -> ULValueP A.

Type Parameters

• Single parameter (Type) - The type of value stored at this location
• No panic flag - Locations don't panic

Constructors

ULState - State Variable Location

ULState : forall {U} {f: LedgerFields}`{EmbeddedType (field_type f) U}, 
          ULValueP U

Purpose: Reference to contract state

Notation: → μ e

Examples:

→ μ Ledger_MainState : ULValue ContractState

Usage:

::// → μ Ledger_MainState := new_state .

ULField - Record Field Location

ULField : forall {U:Type} {FU:Set} (f:FU)`{PruvendoRecord U FU}, 
          ULValueP U -> ULValueP (field_type f)

Purpose: Reference to a field within a record

Notation: → r ^^ f

Examples:

→ (μ Ledger_MainState) ^^ Contract_totalSupply : ULValue uint256
→ user ^^ User_balance : ULValue uint256

Usage:

::// → (μ Ledger_MainState) ^^ Contract_totalSupply := {1000000} .

Chaining: Fields can be chained for nested records:

→ (μ Ledger_MainState) ^^ Contract_config ^^ Config_maxSupply

ULIndex - Mapping/Array Entry Location

ULIndex : forall {K C V} (rk: URValueP K false) (lv:ULValueP C) 
          `{Container K C V}`{XBoolEquable XBool K}`{XDefault V},
          ULValueP V

Purpose: Reference to a mapping or array entry

Notation: → m [[ i ]]

Examples:

→ balances [[ addr ]] : ULValue uint256
→ array [[ {0} ]] : ULValue uint256

Usage:

::// → balances [[ msg->sender ]] := {1000} .
::// → array [[ {0} ]] := {42} .

Key constraint: rk: URValueP K false - Key must not panic

Type classes:

• Container K C V - C is a container with keys K and values V
• XBoolEquable XBool K - Keys must be comparable
• XDefault V - Values have a default (for new entries)

ULLocalIndex - Static Entry Location

ULLocalIndex : forall {K C V} (k: K) (lv:ULValueP C) 
               `{ContainerLocal K C V} `{XBoolEquable XBool K}`{XDefault V},
               ULValueP V

Purpose: Reference to a mapping entry with compile-time constant key

Notation: → m [[_ i _]]

Examples:

→ local_map [[_ constant_addr _]] : ULValue uint256

Usage:

::// → local_map [[_ {0} _]] := {100} .

Difference from ULIndex: Key is a Coq value, not an URValue

ULTuple - Tuple Location

ULTuple : forall {A B}, ULValueP A -> ULValueP B -> ULValueP (XProd A B)

Purpose: Reference to a tuple (pair of locations)

Examples:

ULTuple loc_a loc_b : ULValue (A # B)

Usage: Typically used with tuple unpacking:

::// new ('a : uint256, 'b : uint256) @ ("a", "b") := getPair() .

ULFirst / ULSecond - Tuple Component Location

ULFirst : forall {A B}, ULValueP (XProd A B) -> ULValueP A
ULSecond : forall {A B}, ULValueP (XProd A B) -> ULValueP B

Purpose: Reference to first/second component of a tuple location

Examples:

ULFirst tuple_loc : ULValue A
ULSecond tuple_loc : ULValue B

Usage: Access components of tuple variables:

::// → ULFirst pair_var := {42} .

ULUnMaybe - Optional Location

ULUnMaybe: forall {A}`{XDefault A}, ULValueP (XMaybe A) -> ULValueP A

Purpose: Reference to the value inside an optional (with default on None)

Examples:

ULUnMaybe maybe_loc : ULValue A

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

ULValue vs URValue

Key Differences

Automatic Coercion

ULValue automatically coerces to URValue when needed:

(* balance is ULValue, coerced to URValue in expression *)
::// total := balance + {100} .

Coercion rule: ULValue T → URValue T false

Notation Prefix

• ULValue: Uses → prefix in low-level notation
• URValue: No prefix (or # for scalars)

Examples:

→ μ Ledger_MainState        (* ULValue *)
μ Ledger_MainState          (* URValue *)

→ balances [[ addr ]]       (* ULValue *)
balances [[ addr ]]         (* URValue *)

Common Patterns

State Variable Assignment

::// → (μ Ledger_MainState) ^^ Contract_totalSupply := {1000000} .

Mapping Update

::// → balances [[ msg->sender ]] := balance + amount .

Nested Field Update

::// → (μ Ledger_MainState) ^^ Contract_user ^^ User_balance := {1000} .

Array Element Update

::// → array [[ index ]] := value .

See Also

• URValue Grammar - Right value grammar
• UExpression Grammar - Expression grammar
• Assignment Notations - Assignment syntax

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

• URValue Grammar - Right value grammar
• ULValue Grammar - Left value grammar
• Control Flow - Control flow syntax

Notational Mechanism

Ursus uses Coq's powerful notation system to provide readable, domain-specific syntax for smart contracts. This section explains how notations work and how they map to underlying Coq terms.

Overview

Notations are syntactic sugar that transforms readable code into formal Coq terms. They enable:

1. Familiar syntax - Code looks like traditional programming languages
2. Type safety - All notations are type-checked by Coq
3. Formal semantics - Each notation has precise mathematical meaning
4. Proof support - Can reason about notations using Coq tactics

Notation Scopes

Ursus defines several notation scopes for different contexts:

usolidity_scope

The main scope for Ursus/Solidity-like syntax:

Local Open Scope usolidity_scope.

Provides:

• Statement notations (::// ... .)
• Expression operators (+, -, *, /, etc.)
• Comparison operators (==, !=, <, >, etc.)
• Logical operators (&&, ||, !)
• Assignment operators (:=, +=, -=, etc.)

Other Scopes

• ursus_scope - Core Ursus primitives
• solidity_scope - Solidity-specific features
• tvm_scope - TVM-specific operations

Statement Notations

Basic Statement Form

Notation:

::// statement .

Expands to:

refine (statement ; _)

Purpose:

• Introduces a statement in function body
• Automatically handles sequencing
• Integrates with Coq's proof mode

Statement Terminator

Notation:

::// statement |.

Expands to:

refine statement

Purpose:

• Marks the last statement in a sequence
• No continuation needed

Statement Separators

With continuation (.):

::// stmt1 .
::// stmt2 .
::// stmt3 |.

Expands to:

refine (stmt1 ; (stmt2 ; stmt3))

Variable Declaration

Simple Variable

Notation:

::// var 'x : T := value .

Expands to:

refine (let x := value in _)

Example:

::// var 'balance : uint256 := {0} .

Named Variable

Notation:

::// new 'x : T @ "name" := value ; _ .

Expands to:

refine (ULet "name" value (fun x => _))

Purpose:

• Creates variable with specific name in generated code
• Useful for debugging and code generation

Example:

::// new 'total : uint256 @ "totalAmount" := {1000} ; _ .

Tuple Declaration

Notation:

::// new ('x : T1, 'y : T2) @ ("x", "y") := value ; _ .

Expands to:

refine (ULetTuple "x" "y" value (fun x y => _))

Example:

::// new ('a : uint256, 'b : uint256) @ ("a", "b") := getPair() ; _ .

Assignment Notations

Simple Assignment

Notation:

x := e

Expands to:

UAssign x e

Type constraint:

• x : ULValue T
• e : URValue T b

Compound Assignment

Addition assignment:

x += e  ≡  x := x + e

Other operators:

x -= e  ≡  x := x - e
x *= e  ≡  x := x * e
x /= e  ≡  x := x / e
x %= e  ≡  x := x % e
x &= e  ≡  x := x & e
x |= e  ≡  x := x | e
x ^= e  ≡  x := x ^ e

Increment/Decrement

Pre-increment:

++x  ≡  x := x + {1}

Post-increment:

x++  ≡  (let tmp := x in x := x + {1}; tmp)

Decrement:

--x  ≡  x := x - {1}
x--  ≡  (let tmp := x in x := x - {1}; tmp)

Expression Notations

Arithmetic Operators

Binary operators:

a + b   (* Addition *)
a - b   (* Subtraction *)
a * b   (* Multiplication *)
a / b   (* Division *)
a % b   (* Modulo *)
a ** b  (* Exponentiation *)

Expands to:

UPlus a b
UMinus a b
UMult a b
UDiv a b
UMod a b
UPow a b

Comparison Operators

a == b  (* Equal *)
a != b  (* Not equal *)
a < b   (* Less than *)
a > b   (* Greater than *)
a <= b  (* Less or equal *)
a >= b  (* Greater or equal *)

Expands to:

UEq a b
UNeq a b
ULt a b
UGt a b
ULe a b
UGe a b

Logical Operators

a && b  (* Logical AND *)
a || b  (* Logical OR *)
!a      (* Logical NOT *)

Expands to:

UAnd a b
UOr a b
UNot a

Bitwise Operators

a & b   (* Bitwise AND *)
a | b   (* Bitwise OR *)
a ^ b   (* Bitwise XOR *)
~a      (* Bitwise NOT *)
a << n  (* Left shift *)
a >> n  (* Right shift *)

Literal Notations

Numeric Literals

Notation:

{42}
{0xFF}
{1000000}

Expands to:

ULiteral (N_to_uint256 42)
ULiteral (N_to_uint256 255)
ULiteral (N_to_uint256 1000000)

Boolean Literals

Notation:

@true
@false

Expands to:

ULiteral true
ULiteral false

String Literals

Notation:

"hello"

Expands to:

ULiteral "hello"

Control Flow Notations

If-Then-Else

Notation:

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

Expands to:

UIf condition
    (then_branch)
    (else_branch)

If-Then (no else)

Notation:

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

Expands to:

UIf condition
    (then_branch)
    USkip

While Loop

Notation:

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

Expands to:

UWhile condition (loop_body)

For Loop

Notation:

::// for 'i in range do { ->> } | .
{
    (* loop body *)
}

Expands to:

UFor range (fun i => loop_body)

Mapping and Array Access

Mapping Access

Notation:

mapping[[key]]

Expands to:

UMapAccess mapping key

Nested mappings:

mapping[[key1]][[key2]]

Expands to:

UMapAccess (UMapAccess mapping key1) key2

Array Access

Notation:

array[[index]]

Expands to:

UArrayAccess array index

Struct Field Access

Notation:

struct->field

Expands to:

UFieldAccess struct "field"

Chained access:

user->profile->name

Expands to:

UFieldAccess (UFieldAccess user "profile") "name"

Function Call Notations

Internal Call

Notation:

functionName(arg1, arg2, arg3)

Expands to:

UCall functionName [arg1; arg2; arg3]

External Call (Message Send)

Notation:

send Interface.Method(args) => target with params

Expands to:

USend Interface Method args target params

Example:

::// send IERC20.Transfer(from, to, amount)
         => token_address
         with {InternalMessageParams} [$ {2} ⇒ {flag} $] .

Special Notations

Return Statement

Notation:

return value

Expands to:

UReturn value

Skip (No-op)

Notation:

skip_

Expands to:

USkip

Exit (Panic)

Notation:

exit_ code

Expands to:

UExit code

Require

Notation:

require_ condition
require_ condition, error_code

Expands to:

URequire condition default_error
URequire condition error_code

Message Access Notations

Notation:

msg->sender
msg->value
msg->data

Expands to:

UMsgField "sender"
UMsgField "value"
UMsgField "data"

Panic Holes

The ->> and -/> symbols are "holes" that indicate panic behavior:

Non-panicking hole:

{ ->> }

Expands to:

(fun _ => _) : UExpression unit false

Panicking hole:

{ -/> }

Expands to:

(fun _ => _) : UExpression unit true

Purpose:

• Placeholder for code blocks
• Type-level tracking of panic possibility
• Enables panic-aware type checking

Custom Notations

You can define custom notations for your contracts:

Notation "'transfer_from' from 'to' to 'amount' amt" :=
  (UTransfer from to amt)
  (at level 200).

Usage:

::// transfer_from sender to recipient amount {100} .

Notation Precedence

Ursus notations follow standard precedence rules:

See Also

• Custom Grammar - Grammar extensions
• Ursus Embedding - Semantic foundations
• Writing Functions - Practical examples
• Operators - Standard operators

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

Contract File Structure

An Ursus contract file has a well-defined structure with several sections. This guide explains each section based on real examples from ursus-patterns.

Complete File Structure

(* 1. Import Headers *)
Require Import UrsusEnvironment.Solidity.current.Environment.
Require Import Solidity.TVM.EverBase.

(* 2. Configuration *)
Set UrsusPrefixTactic "PrefixOnlyURValue".

(* 3. Contract Declaration *)
#[translation = off]
#[language = solidity]
Contract MyContract ;
Sends To ;
Inherits ;

(* 4. Types Section *)
Types
Inductive MyEnum := | Value1 | Value2
;

(* 5. Constants Section *)
Constants
Definition myConst : uint256 := 100
;

(* 6. Contract Record *)
Record Contract := {
    field1: uint256;
    field2: address
}.

(* 7. Ursus Options *)
SetUrsusOptions.
Local Open Scope usolidity_scope.

(* 8. Local Types Declaration *)
UseLocal Definition _ := [ uint256 ; address ].

(* 9. Functions *)
Ursus Definition myFunction: UExpression unit false.
{
    (* Function body *)
}
return.
Defined.
Sync.

(* 10. End Contract *)
EndContract ImplementsAuto.

Section Details

1. Import Headers

Import required Ursus libraries and dependencies.

Example from ContractSimplyFuns.v:

Require Import UrsusEnvironment.Solidity.current.Environment.
Require Import Solidity.TVM.EverBase.
Require Import Solidity.TVM.ContractTVM.
Require Import Solidity.Interfaces.IContractTVM.

Common imports:

• UrsusEnvironment.Solidity.current.Environment - Core Solidity environment
• Solidity.TVM.EverBase - TVM base functions
• Interface files for inter-contract communication

2. Configuration

Set Coq and Ursus options.

Example:

Set UrsusPrefixTactic "PrefixOnlyURValue".

This configures how Ursus handles value prefixes in the DSL.

3. Contract Declaration

Declare contract with attributes, name, interfaces, and inheritance.

Syntax:

#[attribute1, attribute2]
Contract ContractName ;
Sends To Interface1 Interface2 ;
Inherits ParentContract1 ParentContract2 ;

Example from ContractSimplyFuns.v:

#[translation = off]
#[quickchick = off]
#[language = solidity]
Contract ContractSimplyFuns ;
Sends To ;
Inherits ;

Components:

• Attributes - #[translation = off], #[language = solidity], etc.
• Contract name - Must be valid Coq identifier
• Sends To - List of interfaces this contract can send messages to
• Inherits - List of parent contracts

See: Attributes, Multi-contract, Inheritance

4. Types Section

Define custom types (enumerations, records).

Syntax:

Types
(* Type definitions *)
;

Example from ContractSimplyFuns.v:

Types
Inductive Ind3 :=
    | ind31
    | ind32
    | ind33
;

Supported types:

• Inductive - Enumerations
• Record - Structures (can also be defined here)

Note: Semicolon ; is a separator between type definitions.

See: Complex Structures

5. Constants Section

Define global constants.

Syntax:

Constants
(* Constant definitions *)
;

Example from ContractSimplyFuns.v:

Constants
Definition const00_u256 : uint256 := 0.1 vmshell
Definition const01_err : XErrorType := 101
Definition const02_u8 : uint8 := 101
;

Features:

• Constants are compile-time values
• Can use special notations like vmshell, kTon
• Type annotations are required

See: Global Constants

6. Contract Record

Define contract state (persistent storage).

Syntax:

Record Contract := {
    field1: type1;
    field2: type2;
    fieldN: typeN
}.

Example from ContractSimplyFuns.v:

Record Contract := {
    #[static] _persistent_contract_data: PersistentContractDataLRecord;
    state01_m_u256_u64: mapping uint256 uint64;
    state02_u256: uint256;
    state03_u8: uint8;
    state04_bool: bool
}.

Important:

• Last field does NOT have semicolon
• #[static] attribute for persistent data
• Field names must be valid Coq identifiers

See: Contract Record

7. Ursus Options

Configure Ursus compiler and open scopes.

Example:

SetUrsusOptions.
Local Open Scope usolidity_scope.

Common scopes:

• usolidity_scope - Solidity-like notations
• ursus_scope_RecordName - Record field access notations

8. Local Types Declaration

Declare types used in local variables within functions.

Syntax:

UseLocal Definition _ := [ type1 ; type2 ; ... ].

Example from ContractSimplyFuns.v:

UseLocal Definition _ := [ uint256 ].

(* Later in file *)
UseLocal Definition _ := [ uint8 ].

(* Can declare multiple types *)
UseLocal Definition _ := [ uint64 ; Ind3 ].

Purpose:

• Enables use of these types in local variables
• Must be declared before functions that use them
• Can have multiple UseLocal declarations

9. Functions

Define contract functions.

Syntax:

#[attributes]
Ursus Definition functionName (args): UExpression ReturnType panicFlag.
{
    (* Function body *)
}
return.
Defined.
Sync.

Example from ContractSimplyFuns.v:

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

Components:

• Attributes - #[public], #[returns=name], etc.
• Function name - Valid Coq identifier
• Arguments - (arg1: type1) (arg2: type2)
• Return type - Type of return value
• Panic flag - true if can fail, false otherwise
• Sync - Synchronize with Ursus system

See: Functions, Writing Functions

10. End Contract

Finalize contract definition.

Syntax:

EndContract Mode.

Modes:

• EndContract ImplementsAuto. - Auto-generate interface implementations
• EndContract Implements. - Manual interface implementations
• EndContract. - No interfaces

Example from ContractSimplyFuns.v:

EndContract ImplementsAuto.

Complete Real Example

From ContractSimplyFuns.v:

Require Import UrsusEnvironment.Solidity.current.Environment.
Require Import Solidity.TVM.EverBase.

Set UrsusPrefixTactic "PrefixOnlyURValue".

#[translation = off]
#[quickchick = off]
#[language = solidity]
Contract ContractSimplyFuns ;
Sends To ;
Inherits ;

Types
Inductive Ind3 := | ind31 | ind32 | ind33
;

Constants
Definition const00_u256 : uint256 := 0.1 vmshell
;

Record Contract := {
    #[static] _persistent_contract_data: PersistentContractDataLRecord;
    state02_u256: uint256;
    state03_u8: uint8
}.

SetUrsusOptions.
Local Open Scope usolidity_scope.

UseLocal Definition _ := [ uint256 ].

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

EndContract ImplementsAuto.

See Also

• Contract Record - State definition
• Functions - Function structure
• Attributes - Function attributes
• Constants - Global constants
• Structures - Custom types

Contract File Headers

This guide explains the import headers required for Ursus contracts based on real examples from ursus-patterns.

Modern Simplified Imports

Modern Ursus contracts use a simplified import structure. The most common pattern is:

Require Import UrsusEnvironment.Solidity.current.Environment.

This single import provides all necessary Ursus functionality for most contracts.

Complete Example

From ContractSimplyFuns.v:

Require Import UrsusEnvironment.Solidity.current.Environment.
Require Import Solidity.TVM.EverBase.
Require Import Solidity.TVM.ContractTVM.
Require Import Solidity.Interfaces.IContractTVM.

Set UrsusPrefixTactic "PrefixOnlyURValue".

Import Categories

1. Core Environment (Required)

Minimal import for Solidity contracts:

Require Import UrsusEnvironment.Solidity.current.Environment.

This provides:

• Core Ursus DSL
• Solidity types and primitives
• Standard library functions
• Notations and scopes

2. TVM-Specific Imports (For TON)

For TON/TVM contracts:

Require Import Solidity.TVM.EverBase.
Require Import Solidity.TVM.ContractTVM.

Purpose:

• Solidity.TVM.EverBase - TVM base functions and types
• Solidity.TVM.ContractTVM - TVM contract utilities

3. Interface Imports

For inter-contract communication:

Require Import Solidity.Interfaces.IContractTVM.
Require Import Solidity.Interfaces.IMyInterface.

Import interfaces defined in separate files.

4. Configuration

Set Ursus options:

Set UrsusPrefixTactic "PrefixOnlyURValue".

This configures how Ursus handles value prefixes in the DSL.

Legacy Import Structure

Older contracts may use detailed imports. This is still valid but not recommended for new contracts.

Legacy Coq Standard Libraries

Require Import Coq.Program.Basics.
Require Import Coq.Strings.String.
Require Import Setoid.
Require Import ZArith.
Require Import QArith.
Require Import Coq.Program.Equality.
Require Import Lia.

Legacy Ursus Libraries

Require Import FinProof.All.
Require Import UMLang.All.
Require Import UrsusStdLib.Solidity.All.
Require Import UrsusStdLib.Solidity.unitsNotations.
Require Import UrsusTVM.Solidity.All.
Require Import UMLang.UrsusLib.
Import UrsusNotations.

Legacy Scopes

Local Open Scope xlist_scope.
Local Open Scope record.
Local Open Scope program_scope.
Local Open Scope ursus_scope.
Local Open Scope usolidity_scope.
Local Open Scope struct_scope.
Local Open Scope N_scope.
Local Open Scope string_scope.
Local Open Scope list_scope.

Note: Modern imports handle scopes automatically.

Recommended Patterns

Pattern 1: Simple Solidity Contract

Require Import UrsusEnvironment.Solidity.current.Environment.

Set UrsusPrefixTactic "PrefixOnlyURValue".

#[language = solidity]
Contract MyContract ;

Pattern 2: TON/TVM Contract

Require Import UrsusEnvironment.Solidity.current.Environment.
Require Import Solidity.TVM.EverBase.
Require Import Solidity.TVM.ContractTVM.

Set UrsusPrefixTactic "PrefixOnlyURValue".

#[language = cpp]
Contract MyTVMContract ;

Pattern 3: Contract with Interfaces

Require Import UrsusEnvironment.Solidity.current.Environment.
Require Import Solidity.Interfaces.IERC20.
Require Import Solidity.Interfaces.IMyCustomInterface.

Set UrsusPrefixTactic "PrefixOnlyURValue".

#[language = solidity]
Contract MyContract ;
Sends To IERC20 IMyCustomInterface ;

Pattern 4: Multi-File Project

Main contract file:

Require Import UrsusEnvironment.Solidity.current.Environment.
Require Import MyProject.Interfaces.IMyInterface.
Require Import MyProject.Libraries.MyLibrary.

Set UrsusPrefixTactic "PrefixOnlyURValue".

#[language = solidity]
Contract MyContract ;

Interface file:

Require Import UrsusEnvironment.Solidity.current.Environment.

Interface IMyInterface ;

Scope Management

After imports, you typically need to open the Ursus scope:

SetUrsusOptions.
Local Open Scope usolidity_scope.

Purpose:

• SetUrsusOptions - Configure Ursus compiler
• Local Open Scope usolidity_scope - Enable Solidity-like notations

Example from ContractSimplyFuns.v:

SetUrsusOptions.
Local Open Scope usolidity_scope.

(* Now you can use Ursus notations *)
Ursus Definition myFunction: UExpression uint256 false.
{
    :://  _res := {100} |.
}
return.
Defined.

Import Order

Recommended import order:

1. Core environment - UrsusEnvironment.Solidity.current.Environment
2. Platform-specific - TVM, EVM, etc.
3. Interfaces - Contract interfaces
4. Libraries - Custom libraries
5. Configuration - Set commands
6. Contract declaration - Contract keyword
7. Scope opening - SetUrsusOptions, Local Open Scope

Common Mistakes

❌ Wrong: Missing core import

Require Import Solidity.TVM.EverBase.

Contract MyContract ;  (* Error: Ursus environment not loaded *)

✅ Correct: Core import first

Require Import UrsusEnvironment.Solidity.current.Environment.
Require Import Solidity.TVM.EverBase.

Contract MyContract ;

❌ Wrong: Opening scope before contract

Require Import UrsusEnvironment.Solidity.current.Environment.

SetUrsusOptions.
Local Open Scope usolidity_scope.

Contract MyContract ;  (* May cause issues *)

✅ Correct: Open scope after contract declaration

Require Import UrsusEnvironment.Solidity.current.Environment.

Contract MyContract ;
Sends To ;
Inherits ;
Record Contract := { }.

SetUrsusOptions.
Local Open Scope usolidity_scope.

See Also

• Contract File Structure - Complete file structure
• Contract Interfaces - Interface definitions
• Multi-contract Systems - Multi-file projects

Contract File Interfaces

Interfaces in Ursus define the external API of contracts, enabling type-safe inter-contract communication. They are defined in separate files and used by contracts that need to interact with each other.

Interface File Structure

Basic Structure

Require Import UrsusEnvironment.Solidity.current.Environment.

Interfaces.

SetUrsusOptions.
Unset Ursus Extraction.

MakeInterface Class IMyInterface :=
{
    method1 : arg1Type -> UExpression returnType panicFlag ;
    method2 : arg1Type -> arg2Type -> UExpression returnType panicFlag
}.

EndInterfaces.

Real Example: IContractSimplyFuns

From ursus-patterns/src/Solidity/Interfaces/IContractSimplyFuns.v:

Require Import UrsusEnvironment.Solidity.current.Environment.

Interfaces.

SetUrsusOptions.
Unset Ursus Extraction.

MakeInterface Class IContractSimplyFuns :=
{
    #[override, external]
    fun02 : uint256 -> UExpression uint256 false ;
    #[override, external]
    fun08 : uint8 -> UExpression PhantomType true
}.

EndInterfaces.

Interface Sections

1. Imports

Require Import UrsusEnvironment.Solidity.current.Environment.

Import the Ursus environment for the target platform (Solidity, C++, Rust).

2. Interfaces Block

Interfaces.
(* Interface definitions go here *)
EndInterfaces.

All interface definitions must be between Interfaces. and EndInterfaces..

3. Options

SetUrsusOptions.
Unset Ursus Extraction.

• SetUrsusOptions - Configure Ursus compiler options
• Unset Ursus Extraction - Disable code extraction for interfaces (they're declarations only)

4. Interface Definition

MakeInterface Class IMyInterface :=
{
    (* Method signatures *)
}.

Method Signatures

Basic Signature

methodName : argType -> UExpression returnType panicFlag

Components:

• methodName - Function name
• argType - Argument type (can be multiple with ->)
• returnType - Return type
• panicFlag - true if can panic, false otherwise

Multiple Arguments

transfer : address -> uint256 -> UExpression boolean false

Equivalent to:

function transfer(address to, uint256 amount) external returns (bool);

No Arguments

totalSupply : UExpression uint256 false

No Return Value

burn : uint256 -> UExpression PhantomType false

PhantomType indicates no meaningful return value (like void).

Can Panic

withdraw : uint256 -> UExpression unit true

The true flag indicates this function can revert/panic.

Method Attributes

Common Attributes

#[override, external]
methodName : argType -> UExpression returnType panicFlag

Attributes:

• override - Overrides parent interface method
• external - External visibility
• view - Read-only function
• pure - No state access

Example with Attributes

MakeInterface Class IERC20 :=
{
    #[external, view]
    balanceOf : address -> UExpression uint256 false ;

    #[external]
    transfer : address -> uint256 -> UExpression boolean false ;

    #[external]
    approve : address -> uint256 -> UExpression boolean false
}.

Complete Interface Example

ERC20 Interface

Require Import UrsusEnvironment.Solidity.current.Environment.

Interfaces.

SetUrsusOptions.
Unset Ursus Extraction.

MakeInterface Class IERC20 :=
{
    #[external, view]
    totalSupply : UExpression uint256 false ;

    #[external, view]
    balanceOf : address -> UExpression uint256 false ;

    #[external, view]
    allowance : address -> address -> UExpression uint256 false ;

    #[external]
    transfer : address -> uint256 -> UExpression boolean false ;

    #[external]
    approve : address -> uint256 -> UExpression boolean false ;

    #[external]
    transferFrom : address -> address -> uint256 -> UExpression boolean false
}.

EndInterfaces.

Using Interfaces

In Contract Declaration

Contract MyToken ;
Sends To IERC20 ;
Inherits ;

Calling Interface Methods

Ursus Definition callOtherToken (tokenAddr: address) (to: address) (amount: uint256):
  UExpression boolean false.
{
    ::// _result := IERC20(tokenAddr).transfer(to, amount) |.
}
return.
Defined.

Interface Inheritance

Extending Interfaces

MakeInterface Class IExtendedToken :=
{
    (* Inherits IERC20 methods *)

    #[external]
    mint : address -> uint256 -> UExpression boolean false ;

    #[external]
    burn : uint256 -> UExpression boolean false
}.

Multiple Interfaces

Defining Multiple Interfaces in One File

Interfaces.

SetUrsusOptions.
Unset Ursus Extraction.

MakeInterface Class IToken :=
{
    transfer : address -> uint256 -> UExpression boolean false
}.

MakeInterface Class IOwnable :=
{
    owner : UExpression address false ;
    transferOwnership : address -> UExpression unit false
}.

EndInterfaces.

See Also

• Multi-Contract Systems - Inter-contract communication
• Contract Structure - Contract organization
• Attributes - Function attributes
• ursus-patterns repository - Interface examples in src/Solidity/Interfaces

Contract Record

The Record Contract defines the persistent state of an Ursus contract. This is the data that is stored on the blockchain and persists between function calls.

Basic Syntax

Record Contract := {
    field1: type1;
    field2: type2;
    field3: type3
}.

Note: The last field does NOT have a semicolon.

Simple Example

Contract SimpleToken ;
Sends To ;
Inherits ;

Record Contract := {
    totalSupply: uint256;
    balances: mapping address uint256;
    owner: address
}.

Field Types

Primitive Types

Record Contract := {
    count: uint256;
    active: bool;
    name: string;
    value: uint8
}.

Mappings

Record Contract := {
    balances: mapping address uint256;
    allowances: mapping address (mapping address uint256);
    approved: mapping uint256 address
}.

Optional Types

Record Contract := {
    maybeOwner: optional address;
    pendingValue: optional uint256
}.

Custom Types

Record Contract := {
    userInfo: UserInfoLRecord;
    tokenData: mapping uint256 TokenDataLRecord
}.

Real Example from ursus-patterns

From ContractSimplyFuns.v:

Record Contract := {
    #[static] _persistent_contract_data: PersistentContractDataLRecord;
    state01_m_u256_u64: mapping uint256 uint64;
    state02_u256: uint256;
    state03_u8: uint8;
    state04_bool: bool
}.

Static Fields

Persistent Contract Data

The #[static] attribute marks fields that are part of the persistent contract data:

Record Contract := {
    #[static] _persistent_contract_data: PersistentContractDataLRecord;
    balance: uint256
}.

This field is automatically managed by the Ursus runtime and contains platform-specific data.

Complex Example

From ContractSolidity.v:

Record Contract := {
    #[static] _persistent_contract_data: PersistentContractDataLRecord;
    state01_m_u256_u64: mapping uint256 uint64;
    state02_u128: uint128;
    state03_o_u256: optional uint256;
    state04_u256: uint256;
    state05_str: string;
    state06_bool: bool;
    state07_u8: uint8;
    state08_m_u256_bool: mapping uint256 bool;
    state09_Rec1: (_ResolveRecord "Rec1");
    state10_m_u8_Rec1: mapping uint8 (_ResolveRecord "Rec1");
    state11_Ind1: (_ResolveName "Ind1")
}.

Accessing State Fields

In Functions

State fields are accessed directly by name:

Ursus Definition getBalance: UExpression uint256 false.
{
    ::// _result := totalSupply |.
}
return.
Defined.

Updating State

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

Mapping Access

Ursus Definition balanceOf (account: address): UExpression uint256 false.
{
    ::// _result := balances[[account]] |.
}
return.
Defined.

Inherited State

When a contract inherits from another, the parent's state is automatically included:

Parent:

Contract Ownable ;
Record Contract := {
    owner: address
}.

Child:

Contract MyToken ;
Inherits Ownable ;

Record Contract := {
    (* Inherited: owner: address *)
    totalSupply: uint256;
    balances: mapping address uint256
}.

The child contract has access to both owner (from parent) and its own fields.

Empty Contract Record

If a contract has no state (e.g., pure utility contract):

Record Contract := {
}.

See Also

• Contract Structure - Overall contract organization
• Types and Primitives - Available types
• Complex Structures - Custom types
• Inheritance - State inheritance

Types, Primitives and Literals

Ursus provides a rich type system for smart contract development. This section covers all available types and their usage.

Primitive Types

Integer Types

Ursus supports signed and unsigned integers of various sizes:

Unsigned Integers

Literals:

{0}         (* uint256 zero *)
{42}        (* uint256 literal *)
{1000000}   (* uint256 literal *)

Signed Integers

Literals:

{-42}       (* int256 negative *)
{100}       (* int256 positive *)

Boolean Type

Literals:

@true       (* boolean true *)
@false      (* boolean false *)

Address Type

Literals:

{0x0000000000000000000000000000000000000000}  (* zero address *)

Special values:

msg->sender     (* sender address *)
this->address   (* contract address *)

String Type

Literals:

{"hello"}       (* string literal *)
{""}            (* empty string *)

PhantomType

Usage:

Ursus Definition doSomething: UExpression PhantomType false.
{
    ::// ...
}
return.
Defined.

Composite Types

Mapping

Hash map from keys to values:

Syntax:

mapping keyType valueType

Examples:

mapping address uint256              (* address to balance *)
mapping uint256 boolean              (* ID to flag *)
mapping address (mapping address uint256)  (* nested mapping *)

Operations:

::// var balance: uint256 := balances[[addr]] .     (* fetch *)
::// balances[[addr]] := {1000} .                   (* insert *)
::// balances->delete(addr) .                       (* delete *)

See also: Standard Functions - Mappings

Optional

Nullable value type:

Syntax:

optional T

Examples:

optional uint256        (* nullable uint256 *)
optional address        (* nullable address *)

Operations:

::// var x: optional uint256 := some({42}) .        (* create *)
::// var y: optional uint256 := none .              (* empty *)
::// var has: boolean := x->hasValue() .            (* check *)
::// var val: uint256 := x->get() .                 (* extract *)

See also: Standard Functions - Optionals

Array

Dynamic array type:

Syntax:

array T

Examples:

array uint256           (* array of numbers *)
array address           (* array of addresses *)

Operations:

::// var len: uint256 := arr->length() .            (* length *)
::// arr->push({42}) .                              (* append *)
::// var last: uint256 := arr->pop() .              (* remove last *)
::// var elem: uint256 := arr[[{0}]] .              (* index *)

See also: Standard Functions - Arrays

User-Defined Types

Records (Structs)

Define custom struct types:

Syntax:

Record TypeName := {
    field1: type1;
    field2: type2;
    ...
    fieldN: typeN
}.

Example:

Types
  Record User := {
      user_id: uint256;
      balance: uint256;
      active: boolean
  };

Literals:

[$ {1} ⇒ user_id ;
   {1000} ⇒ balance ;
   @true ⇒ active $]

Field access:

::// var id: uint256 := user->user_id .
::// user->balance := {2000} .

See also: Structures

Enumerations

Define enumeration types:

Example:

Types
  Inductive Status := Pending | Active | Completed;

Usage:

::// var status: Status := Active .
::// match status with
     | Pending => { ->> }
     | Active => { ->> }
     | Completed => { ->> }
     end | .

Type Resolution

_ResolveName

Reference user-defined types by name:

Syntax:

(_ResolveName "TypeName")

Example:

Record Contract := {
    current_user: (_ResolveName "User");
    users: mapping address (_ResolveName "User")
}.

_ResolveRecord

Reference record types:

Syntax:

(_ResolveRecord "RecordName")

Type Conversions

Explicit Conversions

uint8_to_uint256(x)     (* uint8 → uint256 *)
uint256_to_uint8(x)     (* uint256 → uint8 (truncate) *)
int_to_uint(x)          (* int → uint (reinterpret) *)

Implicit Conversions

Ursus performs some implicit conversions:

• Smaller unsigned to larger unsigned
• Literals to appropriate types

See Also

• Structures - User-defined types
• Standard Functions - Type operations
• Contract Structure - Using types in contracts

Constants

Constants in Ursus are compile-time values that don't change during contract execution. There are two types: global constants (outside contracts) and contract constants (inside contracts).

Contract Constants

Contract constants are defined within the Contract declaration and are accessible to all contract functions.

Syntax

Constants
  Definition CONSTANT_NAME : type := value
  Definition ANOTHER_CONSTANT : type := value
;

Important: The semicolon (;) must appear after the last constant definition.

Examples

Integer constants:

Constants
  Definition MAX_SUPPLY : uint256 := {1000000}
  Definition MIN_BALANCE : uint256 := {100}
  Definition DECIMALS : uint8 := {18}
;

Error codes:

Constants
  Definition ERR_ADDR_ZERO : uint16 := {104}
  Definition ERR_LOW_AMOUNT : uint16 := {105}
  Definition ERR_LOW_BALANCE : uint16 := {106}
  Definition ERR_NOT_SELF : uint16 := {107}
;

Boolean constants:

Constants
  Definition DEFAULT_ACTIVE : boolean := @true
  Definition ALLOW_TRANSFERS : boolean := @false
;

Address constants:

Constants
  Definition ZERO_ADDRESS : address := {0x0000000000000000000000000000000000000000}
;

Using Constants

Constants can be used anywhere in contract functions:

Ursus Definition mint (amount: uint256): UExpression PhantomType true.
{
    ::// require_ (totalSupply + amount <= MAX_SUPPLY) .
    ::// totalSupply := totalSupply + amount |.
}
return.
Defined.

Global Constants

Global constants are defined outside the contract, typically in separate modules or at the file level.

Syntax

Definition GLOBAL_CONSTANT : type := value.

Examples

Module-level constants:

Require Import UrsusEnvironment.Solidity.current.Environment.

Definition SECONDS_PER_DAY : uint256 := {86400}.
Definition DAYS_PER_YEAR : uint256 := {365}.

Module MyContract.
  (* Contract definition *)
End MyContract.

Shared constants:

(* Constants.v *)
Definition MAX_UINT256 : uint256 := {115792089237316195423570985008687907853269984665640564039457584007913129639935}.
Definition ZERO : uint256 := {0}.

Constant Expressions

Constants can be computed from other constants:

Constants
  Definition BASE_FEE : uint256 := {100}
  Definition FEE_MULTIPLIER : uint256 := {3}
  Definition TOTAL_FEE : uint256 := {300}  (* BASE_FEE * FEE_MULTIPLIER *)
;

Note: Ursus doesn't evaluate constant expressions automatically. You must compute the value manually.

Best Practices

1. Use Descriptive Names

Good:

Constants
  Definition MAX_SUPPLY : uint256 := {1000000}
  Definition MIN_TRANSFER_AMOUNT : uint256 := {1}
;

Avoid:

Constants
  Definition X : uint256 := {1000000}
  Definition Y : uint256 := {1}
;

2. Group Related Constants

Good:

Constants
  (* Supply limits *)
  Definition MAX_SUPPLY : uint256 := {1000000}
  Definition MIN_SUPPLY : uint256 := {0}

  (* Fee configuration *)
  Definition BASE_FEE : uint256 := {100}
  Definition MAX_FEE : uint256 := {1000}

  (* Error codes *)
  Definition ERR_INSUFFICIENT_BALANCE : uint16 := {100}
  Definition ERR_INVALID_ADDRESS : uint16 := {101}
;

3. Use Appropriate Types

Good:

Constants
  Definition DECIMALS : uint8 := {18}        (* Small number *)
  Definition MAX_SUPPLY : uint256 := {1000000}  (* Large number *)
;

Avoid:

Constants
  Definition DECIMALS : uint256 := {18}      (* Wasteful *)
;

4. Document Magic Numbers

Good:

Constants
  (* 86400 seconds = 1 day *)
  Definition SECONDS_PER_DAY : uint256 := {86400}

  (* 10^18 for 18 decimal places *)
  Definition DECIMALS_MULTIPLIER : uint256 := {1000000000000000000}
;

Common Patterns

Error Codes

Constants
  Definition ERR_NOT_OWNER : uint16 := {100}
  Definition ERR_PAUSED : uint16 := {101}
  Definition ERR_INSUFFICIENT_BALANCE : uint16 := {102}
  Definition ERR_INVALID_AMOUNT : uint16 := {103}
;

Usage:

::// require_ (msg->sender == owner) or_throw ERR_NOT_OWNER .

Configuration Values

Constants
  Definition LOCK_PERIOD : uint256 := {86400}  (* 1 day *)
  Definition MIN_STAKE : uint256 := {1000}
  Definition REWARD_RATE : uint256 := {5}  (* 5% *)
;

Flags and Masks

Constants
  Definition FLAG_SEND_ALL : uint8 := {128}
  Definition FLAG_IGNORE_ERRORS : uint8 := {2}
  Definition FLAG_BOUNCE : uint8 := {64}
;

Complete Example

#[translation = on]
#[language = solidity]
Contract TokenSale ;
Sends To IERC20 ;

Types ;

Constants
  (* Token configuration *)
  Definition TOKEN_PRICE : uint256 := {1000}
  Definition MIN_PURCHASE : uint256 := {100}
  Definition MAX_PURCHASE : uint256 := {10000}

  (* Sale phases *)
  Definition PHASE_PRESALE : uint8 := {0}
  Definition PHASE_PUBLIC : uint8 := {1}
  Definition PHASE_ENDED : uint8 := {2}

  (* Error codes *)
  Definition ERR_SALE_NOT_ACTIVE : uint16 := {100}
  Definition ERR_AMOUNT_TOO_LOW : uint16 := {101}
  Definition ERR_AMOUNT_TOO_HIGH : uint16 := {102}
;

Record Contract := {
    token: address;
    current_phase: uint8;
    total_sold: uint256
}.

See Also

• Contract Structure - Overall contract organization
• Types and Primitives - Available types for constants
• Functions - Using constants in functions

User-Defined Types and Structures

Ursus supports custom data structures through records (structs) and enumerations. This section explains how to define and use them.

Records (Structs)

Records are the primary way to define custom data structures in Ursus.

Defining Records

Recommended way (using Contract):

Types
  Record Person := {
      name: string;
      surname: string;
      age: uint256
  };

This is the recommended approach as it integrates with the Contract system.

Manual way (using GlobalGeneratePruvendoRecord):

Inductive PersonFields :=
| Person_ι_name
| Person_ι_surname
| Person_ι_age.

Definition PersonL := [string : Type ; string : Type ; uint256 : Type]%glist.
GlobalGeneratePruvendoRecord PersonL PersonFields.

This creates a type called PersonLRecord. This approach is not recommended for normal use.

Record Literals

Syntax:

[$ value1 ⇒ field1 ;
   value2 ⇒ field2 ;
   ...
   valueN ⇒ fieldN $]

Example:

::// var person: Person := [$ {"John"} ⇒ name ;
                               {"Smith"} ⇒ surname ;
                               {42} ⇒ age $] .

Accessing Fields

Read field:

::// var person_name: string := person->name .
::// var person_age: uint256 := person->age .

Write field:

::// person->age := {43} .
::// person->name := {"Jane"} .

Nested Records

Records can contain other records:

Types
  Record Address := {
      street: string;
      city: string;
      zipcode: uint32
  }
  Record Person := {
      name: string;
      home_address: (_ResolveName "Address");
      age: uint256
  };

Usage:

::// var addr: Address := [$ {"Main St"} ⇒ street ;
                             {"NYC"} ⇒ city ;
                             {10001} ⇒ zipcode $] .

::// var person: Person := [$ {"John"} ⇒ name ;
                              addr ⇒ home_address ;
                              {42} ⇒ age $] .

::// var city: string := person->home_address->city .

Enumerations

Enumerations define a type with a fixed set of values.

Defining Enums

Types
  Inductive Status := Pending | Active | Completed | Cancelled;

Using Enums

Assignment:

::// var status: Status := Active .

Pattern matching:

::// match status with
     | Pending => { ->> }
     | Active => { ->> }
     | Completed => { ->> }
     | Cancelled => { ->> }
     end | .
{
    ::// (* Pending case *) |.
}
{
    ::// (* Active case *) |.
}
{
    ::// (* Completed case *) |.
}
{
    ::// (* Cancelled case *) |.
}

Using Records in Contracts

As Contract State

Types
  Record User := {
      user_id: uint256;
      balance: uint256;
      active: boolean
  };

Record Contract := {
    owner: address;
    current_user: (_ResolveName "User");
    users: mapping address (_ResolveName "User")
}.

In Function Parameters

Ursus Definition registerUser (user: User): UExpression PhantomType false.
{
    ::// users[[msg->sender]] := user |.
}
return.
Defined.

In Function Returns

#[pure, returns=_result]
Ursus Definition getUser (addr: address): UExpression User false.
{
    ::// _result := users[[addr]] |.
}
return.
Defined.

Complex Examples

Record with Mappings

Types
  Record TokenInfo := {
      total_supply: uint256;
      balances: mapping address uint256;
      allowances: mapping address (mapping address uint256)
  };

Record with Arrays

Types
  Record Proposal := {
      proposal_id: uint256;
      description: string;
      votes_for: array address;
      votes_against: array address;
      executed: boolean
  };

Record with Optionals

Types
  Record Config := {
      max_supply: optional uint256;
      owner: optional address;
      paused: boolean
  };

Type Resolution

When referencing user-defined types in contract state, use _ResolveName:

Record Contract := {
    user: (_ResolveName "User");
    users: mapping address (_ResolveName "User");
    status: (_ResolveName "Status")
}.

This ensures proper type resolution during code generation.

Best Practices

1. Use Contract Types Section

Good:

Types
  Record User := { ... };

Avoid:

GlobalGeneratePruvendoRecord ...

2. Meaningful Field Names

Good:

Record User := {
    user_id: uint256;
    balance: uint256;
    is_active: boolean
}.

Avoid:

Record User := {
    x: uint256;
    y: uint256;
    z: boolean
}.

3. Group Related Data

Good:

Record Transaction := {
    from: address;
    to: address;
    amount: uint256;
    timestamp: uint256
}.

Avoid:

(* Scattered fields in contract state *)
Record Contract := {
    tx_from: address;
    some_other_field: uint256;
    tx_to: address;
    tx_amount: uint256
}.

See Also

• Types and Primitives - Built-in types
• Contract Structure - Using types in contracts
• Simple Contract Example - Complete example

Functions and Modifiers

This guide explains how to define functions in Ursus contracts based on real examples from ursus-patterns.

Function Structure

Every Ursus function follows this structure:

#[attributes]
Ursus Definition functionName (arguments): UExpression ReturnType panicFlag.
{
    (* Function body *)
}
return.
Defined.
Sync.

Components

1. Attributes

Function attributes are specified before the function definition.

Syntax:

#[attribute1]
#[attribute2, attribute3]

Common attributes:

• #[public] - Public function
• #[external] - External function
• #[internal] - Internal function
• #[private] - Private function
• #[view] - Read-only function
• #[pure] - Pure function (no state access)
• #[payable] - Can receive value
• #[returns=name] - Specify return variable name
• #[write=arg] - Allow writing to argument
• #[no_body] - Function without body (interface)

Example from ContractSimplyFuns.v:

#[returns=_res]
Ursus Definition fun05 : UExpression uint256 false.

See: Function Attributes

2. Function Name

Function name must be a valid Coq identifier.

Rules:

• Starts with letter or underscore
• Can contain letters, numbers, underscores
• No spaces
• Case-sensitive

Examples:

Ursus Definition transfer ...
Ursus Definition balanceOf ...
Ursus Definition _internal_helper ...
Ursus Definition fun01 ...

3. Arguments

Arguments are specified in parentheses with type annotations.

No arguments:

Ursus Definition fun01: UExpression PhantomType false.

One argument:

Ursus Definition fun02 (arg1_u256: uint256): UExpression uint256 false.

Multiple arguments:

Ursus Definition fun07 (arg1_u8: uint8) (arg2_str: string): UExpression string false.

Argument syntax:

(argumentName: argumentType)

Argument names:

• Follow same rules as function names
• Conventionally use descriptive names or type suffixes

Example from ContractSimplyFuns.v:

Ursus Definition fun04 (arg1_u8 : uint8): UExpression uint256 false.

4. Return Type

Return type specifies what the function returns.

No return value:

UExpression PhantomType panicFlag

Specific return type:

UExpression uint256 panicFlag
UExpression address panicFlag
UExpression boolean panicFlag

Examples from ContractSimplyFuns.v:

No return:

Ursus Definition fun01: UExpression PhantomType false.

Returns uint256:

Ursus Definition fun02 (arg1_u256: uint256): UExpression uint256 false.

Returns string:

Ursus Definition fun07 (arg1_u8: uint8) (arg2_str: string): UExpression string false.

See: Types and Primitives

5. Panic Flag

The panic flag indicates whether the function can fail (panic/revert).

Syntax:

UExpression ReturnType true   (* Can panic *)
UExpression ReturnType false  (* Cannot panic *)

Use true when:

• Function contains require_() statements
• Function calls other functions with true flag
• Function has early returns (e.g., return in if-statement)

Use false when:

• Function always succeeds
• No require statements
• No early returns
• Only calls functions with false flag

Examples from ContractSimplyFuns.v:

With panic (has require):

Ursus Definition fun08 (arg1_u8: uint8) : UExpression PhantomType true.
{
    :://  require_((const02_u8 >= state03_u8 + arg1_u8) &&
                   (arg1_u8+const02_u8 >= state03_u8), const01_err).
    :://  require_(state04_bool == {false}) |.
}
return.
Defined.

Without panic:

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

6. Function Body

Function body contains the implementation.

Empty body (interface):

#[no_body]
Ursus Definition fun01: UExpression PhantomType false.
return.
Defined.

Body with code:

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

Body syntax:

• Enclosed in { } braces
• Statements start with ::// or :://
• Statements end with . or |.
• Last statement ends with |.

See: Function Operators

7. Return Statement

Return statement specifies what to return.

No return value:

return.

Return argument:

return arg1_u256.

Return variable:

return arg2_str.

Return implicit result:

return.  (* Uses _res or _result *)

Examples from ContractSimplyFuns.v:

Return nothing:

Ursus Definition fun01: UExpression PhantomType false.
return.
Defined.

Return argument:

Ursus Definition fun02 (arg1_u256: uint256): UExpression uint256 false.
return arg1_u256.
Defined.

Return variable:

Ursus Definition fun07 (arg1_u8: uint8) (arg2_str: string): UExpression string false.
{
    ::// arg2_str := {"Hello world!"} |.
}
return arg2_str.
Defined.

8. Defined and Sync

Every function must end with Defined. and Sync.

Defined.
Sync.

Purpose:

• Defined. - Finalizes the Coq definition
• Sync. - Synchronizes with Ursus code generator

Complete Examples

Example 1: Simple Function

From ContractSimplyFuns.v:

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

Example 2: Function with Arguments

From ContractSimplyFuns.v:

#[returns=_res]
Ursus Definition fun04 (arg1_u8 : uint8): UExpression uint256 false.
{
    :://  _res := uint256(arg1_u8) |.
}
return.
Defined.
Sync.

Example 3: Function with Local Variables

From ContractSimplyFuns.v:

UseLocal Definition _ := [ uint64 ; Ind3 ].

#[returns=_res]
Ursus Definition fun06 (arg1_u64: uint64): UExpression uint256 false.
{
    ::// var00 ind1 : Ind3 ;_| .
    ::// ind1 := #{ind31} .

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

Example 4: Function with Writable Arguments

From ContractSimplyFuns.v:

UseLocal Definition _ := [ string ].

#[write=arg1_u8, write=arg2_str]
Ursus Definition fun07 (arg1_u8: uint8) (arg2_str: string): UExpression string false.
{
    ::// arg1_u8 += state03_u8.
    ::// arg2_str := {"Hello world!"} |.
}
return arg2_str.
Defined.
Sync.

Example 5: Function with Require

From ContractSimplyFuns.v:

Ursus Definition fun08 (arg1_u8: uint8) : UExpression PhantomType true.
{
    :://  require_((const02_u8 >= state03_u8 + arg1_u8) &&
                   (arg1_u8+const02_u8 >= state03_u8), const01_err).
    :://  require_(state04_bool == {false}) |.
}
return.
Defined.
Sync.

Local Variables

To use local variables, declare their types with UseLocal:

UseLocal Definition _ := [ uint256 ].

Multiple types:

UseLocal Definition _ := [ uint64 ; Ind3 ; string ].

See: Local State and Variables

See Also

• Function Operators - Operators in function body
• Function Attributes - Function attributes
• Local Variables - Local state
• Writing Functions - Detailed function writing guide

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

Interfaces and Messages

Interfaces enable type-safe inter-contract communication in Ursus. This section covers defining interfaces, declaring message recipients, and sending messages.

Overview

Interfaces define the external API of a contract - the functions that other contracts can call.

Messages are the mechanism for calling functions on other contracts.

Key benefits:

• Type safety - Compile-time checking of message sends
• Documentation - Explicit contract dependencies
• Verification - Formal verification of inter-contract calls
• Code generation - Automatic interface bindings

Defining Interfaces

Interfaces are defined in separate files or at the beginning of contract files.

Interface File Structure

Require Import UrsusEnvironment.Solidity.current.Environment.

Interfaces.
SetUrsusOptions.
Unset Ursus Extraction.

MakeInterface Class IInterfaceName :=
{
    method1 : type1 -> type2 -> UExpression returnType flag ;
    method2 : type3 -> UExpression returnType flag ;
    ...
}.

EndInterfaces.

Interface Syntax

Basic structure:

MakeInterface Class IInterfaceName :=
{
    methodName : arg1Type -> arg2Type -> ... -> UExpression returnType flag
}.

Components:

• IInterfaceName - Interface name (conventionally starts with I)
• methodName - Function name
• argTypes - Curried argument types
• returnType - Return type
• flag - Panic flag (true or false)

Example: ERC20 Interface

Interfaces.
SetUrsusOptions.
Unset Ursus Extraction.

MakeInterface Class IERC20 :=
{
    #[view, public]
    balanceOf : address -> UExpression uint256 false ;

    #[external]
    transfer : address -> uint256 -> UExpression boolean true ;

    #[external]
    approve : address -> uint256 -> UExpression boolean true ;

    #[external]
    transferFrom : address -> address -> uint256 -> UExpression boolean true
}.

EndInterfaces.

Method Attributes

Methods can have attributes:

#[view, public]         (* Read-only public method *)
#[external]             (* External method *)
#[override, external]   (* Override parent method *)
#[external, payable]    (* Payable external method *)

Declaring Message Recipients

The Sends To declaration specifies which interfaces a contract can send messages to.

Syntax

Sends To Interface1 Interface2 Interface3 ;

Examples

Multiple interfaces:

Sends To IERC20 ITokenReceiver IOwnable ;

Single interface:

Sends To IERC20 ;

No external calls:

Sends To ;

Purpose

The Sends To declaration:

1. Enables type checking - Only declared interfaces can be called
2. Documents dependencies - Makes external calls explicit
3. Supports verification - Enables formal verification of calls
4. Generates bindings - Creates interface code in target language

Sending Messages

Messages are sent using the send notation.

Syntax

::// send Interface.Method(arg1, arg2, ...)
         => target_address
         with message_params .

Components

• Interface.Method - Interface and method name
• (arg1, arg2, ...) - Method arguments
• target_address - Recipient contract address
• message_params - Message parameters (value, flags, etc.)

Basic Example

::// send IERC20.Transfer(from, to, amount)
         => token_address
         with {InternalMessageParamsLRecord} [$ {2} ⇒ {Message_ι_flag} $] .

Message Parameters

Message parameters control how the message is sent:

{InternalMessageParamsLRecord} [$
    {value} ⇒ {Message_ι_value} ;
    {flags} ⇒ {Message_ι_flag} ;
    {bounce} ⇒ {Message_ι_bounce}
$]

Common parameters:

• Message_ι_value - Amount of tokens to send
• Message_ι_flag - Message flags
• Message_ι_bounce - Bounce on error

Complete Example

Interface Definition (IERC20.v)

Require Import UrsusEnvironment.Solidity.current.Environment.

Interfaces.
SetUrsusOptions.
Unset Ursus Extraction.

MakeInterface Class IERC20 :=
{
    #[view, public]
    balanceOf : address -> UExpression uint256 false ;

    #[external]
    transfer : address -> uint256 -> UExpression boolean true ;

    #[view, public]
    totalSupply : UExpression uint256 false
}.

EndInterfaces.

Contract Using Interface

Require Import UrsusEnvironment.Solidity.current.Environment.
Require Import UrsusEnvironment.Solidity.current.LocalGenerator.
Require Import IERC20.

Module TokenWrapper.

#[translation = on]
#[language = solidity]
Contract TokenWrapper ;
Sends To IERC20 ;
Types ;
Constants ;

Record Contract := {
    token: address;
    total_wrapped: uint256
}.

SetUrsusOptions.
UseLocal Definition _ := [uint256; address; boolean].

#[external, returns=_result]
Ursus Definition wrapTokens (amount: uint256): UExpression boolean true.
{
    ::// send IERC20.transfer(this->address, amount)
             => token
             with {InternalMessageParamsLRecord} [$ {0} ⇒ {Message_ι_value} $] .

    ::// total_wrapped := total_wrapped + amount .
    ::// _result := @true |.
}
return.
Defined.
Sync.

EndContract Implements.
End TokenWrapper.

Advanced Patterns

Callback Interfaces

Define interfaces for callbacks:

MakeInterface Class ITokenReceiver :=
{
    #[external]
    onTokenReceived : address -> uint256 -> UExpression PhantomType true
}.

Usage:

::// send ITokenReceiver.onTokenReceived(sender, amount)
         => recipient
         with {InternalMessageParamsLRecord} [$ {0} ⇒ {Message_ι_value} $] .

Multiple Interface Calls

Sends To IERC20 IOwnable ITokenReceiver ;

Ursus Definition complexOperation: UExpression PhantomType true.
{
    ::// send IERC20.transfer(recipient, amount)
             => token_address
             with {InternalMessageParamsLRecord} [$ {0} ⇒ {Message_ι_value} $] .

    ::// send ITokenReceiver.onTokenReceived(msg->sender, amount)
             => recipient
             with {InternalMessageParamsLRecord} [$ {0} ⇒ {Message_ι_value} $] .

    ::// send IOwnable.transferOwnership(new_owner)
             => ownable_contract
             with {InternalMessageParamsLRecord} [$ {0} ⇒ {Message_ι_value} $] |.
}
return.
Defined.

Conditional Message Sending

::// if should_notify then { ->> } | .
{
    ::// send ITokenReceiver.onTokenReceived(sender, amount)
             => recipient
             with {InternalMessageParamsLRecord} [$ {0} ⇒ {Message_ι_value} $] |.
}

Best Practices

1. Use Descriptive Interface Names

Good:

MakeInterface Class IERC20 := { ... }.
MakeInterface Class ITokenVesting := { ... }.
MakeInterface Class IOwnable := { ... }.

Avoid:

MakeInterface Class I1 := { ... }.
MakeInterface Class MyInterface := { ... }.

2. Group Related Methods

Good:

MakeInterface Class IERC20 :=
{
    (* View methods *)
    #[view, public]
    balanceOf : address -> UExpression uint256 false ;

    #[view, public]
    totalSupply : UExpression uint256 false ;

    (* State-changing methods *)
    #[external]
    transfer : address -> uint256 -> UExpression boolean true ;

    #[external]
    approve : address -> uint256 -> UExpression boolean true
}.

3. Document Panic Flags

MakeInterface Class IToken :=
{
    (* Can panic: requires sufficient balance *)
    transfer : address -> uint256 -> UExpression boolean true ;

    (* Cannot panic: pure view function *)
    #[view, public]
    balanceOf : address -> UExpression uint256 false
}.

4. Declare All Dependencies

Good:

Sends To IERC20 IOwnable ITokenReceiver ;

Avoid:

Sends To ;
(* Missing interfaces - will cause compilation errors *)

Common Patterns

Token Transfer

::// send IERC20.transfer(recipient, amount)
         => token_address
         with {InternalMessageParamsLRecord} [$ {0} ⇒ {Message_ι_value} $] .

Ownership Transfer

::// send IOwnable.transferOwnership(new_owner)
         => contract_address
         with {InternalMessageParamsLRecord} [$ {0} ⇒ {Message_ι_value} $] .

Callback Notification

::// send ICallback.onComplete(result)
         => callback_address
         with {InternalMessageParamsLRecord} [$ {0} ⇒ {Message_ι_value} $] .

See Also

• Contract Header - Sends To declaration
• Contract Structure - Overall organization
• File Interface - Interface file structure
• Functions - Implementing interface methods
• Notations - Message send notation details

Function Attributes

Ursus uses attributes to control function behavior, visibility, code generation, and verification. Attributes are specified using the #[...] syntax before function definitions.

Syntax

#[attribute1, attribute2, ...]
Ursus Definition functionName (args): UExpression RetType panicFlag.

Visibility Attributes

#[public]

Makes function callable from outside the contract.

Example:

#[public]
Ursus Definition transfer (to: address) (amount: uint256):
  UExpression boolean false.

Generated code:

function transfer(address to, uint256 amount) public returns (bool) {
    ...
}

#[external]

Function can only be called externally (not internally).

Example:

#[external]
Ursus Definition deposit: UExpression unit false.

Generated code:

function deposit() external {
    ...
}

#[internal]

Function can only be called internally.

Example:

#[internal]
Ursus Definition _validateAmount (amount: uint256): UExpression boolean false.

Generated code:

function _validateAmount(uint256 amount) internal returns (bool) {
    ...
}

#[private]

Function is private to the contract.

Example:

#[private]
Ursus Definition _calculateFee (amount: uint256): UExpression uint256 false.

Generated code:

function _calculateFee(uint256 amount) private returns (uint256) {
    ...
}

State Mutability Attributes

#[pure]

Function doesn't read or modify state.

Example:

#[pure]
Ursus Definition add (a b: uint256): UExpression uint256 false.
{
    ::// _result := a + b |.
}
return.
Defined.

Generated code:

function add(uint256 a, uint256 b) public pure returns (uint256) {
    return a + b;
}

#[view]

Function reads but doesn't modify state.

Example:

#[view]
Ursus Definition balanceOf (account: address): UExpression uint256 false.
{
    ::// _result := balances[[account]] |.
}
return.
Defined.

Generated code:

function balanceOf(address account) public view returns (uint256) {
    return balances[account];
}

#[payable]

Function can receive Ether/tokens.

Example:

#[payable]
Ursus Definition deposit: UExpression unit false.
{
    ::// balance := balance + msg->value |.
}
return.
Defined.

Generated code:

function deposit() public payable {
    balance += msg.value;
}

#[nonpayable]

Function cannot receive Ether/tokens (default).

Example:

#[nonpayable]
Ursus Definition withdraw (amount: uint256): UExpression unit false.

Code Generation Attributes

#[translation = on]

Enable code generation for this function.

Example:

#[translation = on]
Ursus Definition transfer (to: address) (amount: uint256):
  UExpression boolean false.

#[translation = off]

Disable code generation (proof-only function).

Example:

#[translation = off]
Ursus Definition helper_lemma: UExpression unit false.

#[language = solidity]

Generate Solidity code.

Example:

#[language = solidity]
Contract ERC20 ;

#[language = cpp]

Generate C++ code for TON.

Example:

#[language = cpp]
Contract TONToken ;

#[language = rust]

Generate Rust code.

Example:

#[language = rust]
Contract RustToken ;

Return Value Attributes

#[returns = varName]

Use named return variable.

Example:

#[returns = result]
Ursus Definition calculate (x: uint256): UExpression uint256 false.
{
    ::// result := x * {2} |.
}
return.
Defined.

Generated code:

function calculate(uint256 x) public returns (uint256 result) {
    result = x * 2;
}

Parameter Attributes

#[write = arg]

Parameter is mutable (passed by reference).

Example:

#[write = balance]
Ursus Definition updateBalance (balance: uint256) (delta: uint256):
  UExpression unit false.
{
    ::// balance := balance + delta |.
}
return.
Defined.

Interface Attributes

#[no_body]

Function declaration without implementation (interface).

Example:

#[no_body]
Ursus Definition transfer (to: address) (amount: uint256):
  UExpression boolean false.

Generated code:

function transfer(address to, uint256 amount) external returns (bool);

Inheritance Attributes

#[override]

Function overrides parent implementation.

Example:

#[override]
Ursus Definition transfer (to: address) (amount: uint256):
  UExpression boolean false.

Generated code:

function transfer(address to, uint256 amount) public override returns (bool) {
    ...
}

#[virtual]

Function can be overridden by children.

Example:

#[virtual]
Ursus Definition _beforeTransfer (from to: address) (amount: uint256):
  UExpression unit false.

Generated code:

function _beforeTransfer(address from, address to, uint256 amount)
    internal virtual {
    ...
}

Verification Attributes

#[quickchick = on]

Enable QuickChick testing for this function.

Example:

#[quickchick = on]
Ursus Definition transfer (to: address) (amount: uint256):
  UExpression boolean false.

#[verified]

Mark function as formally verified.

Example:

#[verified]
Ursus Definition transfer (to: address) (amount: uint256):
  UExpression boolean false.

Combining Attributes

Multiple attributes can be combined:

Example:

#[public, view, translation = on]
Ursus Definition balanceOf (account: address): UExpression uint256 false.
{
    ::// _result := balances[[account]] |.
}
return.
Defined.

Generated code:

function balanceOf(address account) public view returns (uint256) {
    return balances[account];
}

Common Attribute Combinations

Public View Function

#[public, view]
Ursus Definition getBalance: UExpression uint256 false.

Payable External Function

#[external, payable]
Ursus Definition receive: UExpression unit false.

Internal Pure Helper

#[internal, pure]
Ursus Definition _min (a b: uint256): UExpression uint256 false.

Override Virtual Function

#[public, override, virtual]
Ursus Definition transfer (to: address) (amount: uint256):
  UExpression boolean false.

See Also

• Writing Functions - Function development guide
• Contract Structure - Contract organization
• Code Generation - Compilation process

Local State

Local state manages temporary variables used within Ursus functions. Unlike contract fields (which persist on the blockchain), local variables exist only during function execution.

What is Local State?

Local state is a type-indexed container that holds temporary values during function execution. It's managed through the UseLocal command.

Key properties:

• Temporary - Exists only during function execution
• Type-safe - All local variables are type-checked
• Scoped - Variables are scoped to their function
• Efficient - No blockchain storage costs

UseLocal Command

The UseLocal command declares which types can be used for local variables in the contract.

Syntax

UseLocal Definition _ := [
    type1;
    type2;
    ...
    typeN
].

Example

UseLocal Definition _ := [
    boolean;
    address;
    uint256;
    string;
    (mapping address uint256);
    (optional uint256)
].

Important: Include all types you'll use for local variables, including:

• Primitive types
• Composite types (mappings, optionals, arrays)
• User-defined types

Declaring Local Variables

Using var Notation

Syntax:

::// var 'name : type := value .

Examples:

::// var 'balance : uint256 := {1000} .
::// var 'sender : address := msg->sender .
::// var 'active : boolean := @true .

Using new Notation

Syntax:

refine // new 'name : type @ "name" := value ; _ //.

Example:

refine // new 'x : uint256 @ "x" := {42} ; _ //.

Difference:

• var - Modern, recommended syntax
• new - Older syntax, allows chaining in one line

Using Local Variables

Reading Variables

Local variables can be used in expressions:

::// var 'x : uint256 := {10} .
::// var 'y : uint256 := {20} .
::// var 'sum : uint256 := x + y .

Modifying Variables

Assign new values to local variables:

::// var 'counter : uint256 := {0} .
::// counter := counter + {1} .
::// counter := counter * {2} .

Scope

Local variables are scoped to their block:

{
    ::// var 'x : uint256 := {10} .
    ::// if x > {5} then { ->> } else { ->> } | .
    {
        ::// var 'y : uint256 := x + {5} .  (* x is visible *)
        ::// result := y |.
    }
    {
        ::// result := x |.  (* x is visible, y is not *)
    }
}

Local vs Contract State

Complete Example

#[translation = on]
#[language = solidity]
Contract Calculator ;
Sends To ;
Types ;
Constants ;

Record Contract := {
    last_result: uint256
}.

SetUrsusOptions.

UseLocal Definition _ := [
    uint256;
    boolean
].

#[pure, returns=_result]
Ursus Definition add (a: uint256) (b: uint256): UExpression uint256 false.
{
    ::// var 'sum : uint256 := a + b .
    ::// _result := sum |.
}
return.
Defined.
Sync.

#[returns=_result]
Ursus Definition complex_calc (x: uint256): UExpression uint256 false.
{
    ::// var 'temp1 : uint256 := x * {2} .
    ::// var 'temp2 : uint256 := temp1 + {10} .
    ::// var 'is_large : boolean := temp2 > {100} .

    ::// if is_large then { ->> } else { ->> } | .
    {
        ::// _result := temp2 |.
    }
    {
        ::// _result := {0} |.
    }
}
return.
Defined.
Sync.

Advanced Patterns

Temporary Mappings

UseLocal Definition _ := [
    (mapping address uint256)
].

Ursus Definition process_balances: UExpression PhantomType false.
{
    ::// var 'temp_balances : mapping address uint256 := {} .
    ::// temp_balances[[msg->sender]] := {1000} .
    ::// var 'bal : uint256 := temp_balances[[msg->sender]] |.
}
return.
Defined.

Temporary Arrays

UseLocal Definition _ := [
    (array uint256)
].

Ursus Definition collect_values: UExpression PhantomType false.
{
    ::// var 'values : array uint256 := [] .
    ::// values->push({10}) .
    ::// values->push({20}) .
    ::// var 'first : uint256 := values[[{0}]] |.
}
return.
Defined.

Temporary Records

Types
  Record TempData := {
      value: uint256;
      flag: boolean
  };

UseLocal Definition _ := [
    (_ResolveName "TempData")
].

Ursus Definition process_data: UExpression PhantomType false.
{
    ::// var 'data : TempData := [$ {42} ⇒ value ; @true ⇒ flag $] .
    ::// var 'v : uint256 := data->value |.
}
return.
Defined.

Best Practices

1. Declare All Used Types

Good:

UseLocal Definition _ := [
    uint256;
    address;
    boolean;
    (mapping address uint256)
].

Avoid:

UseLocal Definition _ := [
    uint256
].
(* Missing types will cause compilation errors *)

2. Use Meaningful Names

Good:

::// var 'sender_balance : uint256 := balances[[msg->sender]] .
::// var 'is_sufficient : boolean := sender_balance >= amount .

Avoid:

::// var 'x : uint256 := balances[[msg->sender]] .
::// var 'y : boolean := x >= amount .

3. Minimize Local State

Good:

::// var 'balance : uint256 := balances[[msg->sender]] .
::// balances[[msg->sender]] := balance - amount |.

Avoid:

::// var 'temp1 : uint256 := balances[[msg->sender]] .
::// var 'temp2 : uint256 := temp1 .
::// var 'temp3 : uint256 := temp2 - amount .
::// balances[[msg->sender]] := temp3 |.

4. Use Local Variables for Clarity

Good:

::// var 'sender_balance : uint256 := balances[[msg->sender]] .
::// var 'recipient_balance : uint256 := balances[[recipient]] .
::// var 'new_sender_balance : uint256 := sender_balance - amount .
::// var 'new_recipient_balance : uint256 := recipient_balance + amount .

::// balances[[msg->sender]] := new_sender_balance .
::// balances[[recipient]] := new_recipient_balance |.

Avoid:

::// balances[[msg->sender]] := balances[[msg->sender]] - amount .
::// balances[[recipient]] := balances[[recipient]] + amount |.

Common Errors

Missing Type in UseLocal

Error:

Type not found in local state

Solution: Add the missing type to UseLocal:

UseLocal Definition _ := [
    uint256;
    address  (* Add missing type *)
].

Type Mismatch

Error:

Type mismatch: expected uint256, got boolean

Solution: Ensure variable types match their usage:

::// var 'count : uint256 := {0} .  (* Not boolean *)

See Also

• Functions - Using local variables in functions
• Writing Functions - Detailed function guide
• Types and Primitives - Available types
• Quick Start - Complete example with UseLocal

Multi-Contract Systems

Ursus supports multi-contract systems where contracts can interact with each other through message passing. This is essential for building complex decentralized applications.

Contract Interfaces

Declaring Interfaces

Contracts declare which interfaces they can send messages to using the Sends To clause:

Syntax:

Contract MyContract ;
Sends To Interface1 Interface2 Interface3 ;
Inherits ;

Example:

Contract ContractSolidity ;
Sends To IContractTVM ;
Inherits ;

Empty Sends To

If a contract doesn't send messages to other contracts:

Contract SimpleContract ;
Sends To ;
Inherits ;

Defining Interfaces

Interface Structure

Interfaces define the message protocol between contracts:

Contract IMyInterface ;
Sends To ;
Inherits ;

#[no_body]
Ursus Definition myFunction (arg: uint256): UExpression uint256 false.

#[no_body]
Ursus Definition anotherFunction (addr: address): UExpression boolean false.

Real Example: IContractTVM

From ursus-patterns:

Contract IContractTVM ;
Sends To ;
Inherits ;

#[no_body]
Ursus Definition someMethod (value: uint256): UExpression PhantomType false.

Sending Messages

Message Syntax

To send a message to another contract:

::// targetContract.method(args) |.

Example

Ursus Definition callOtherContract (addr: address) (amount: uint256):
  UExpression PhantomType false.
{
    ::// IContractTVM(addr).transfer(amount) |.
}
return.
Defined.

Multi-Contract Patterns

Pattern 1: Factory Pattern

Factory Contract:

Contract TokenFactory ;
Sends To IToken ;
Inherits ;

Record Contract := {
    tokens: mapping uint256 address
}.

Ursus Definition createToken (id: uint256): UExpression address false.
{
    ::// var 'newToken : address := deployContract(TokenCode) .
    ::// tokens[[id]] := newToken .
    ::// _result := newToken |.
}
return.
Defined.

Pattern 2: Proxy Pattern

Proxy Contract:

Contract Proxy ;
Sends To IImplementation ;
Inherits ;

Record Contract := {
    implementation: address
}.

Ursus Definition upgrade (newImpl: address): UExpression unit false.
{
    ::// implementation := newImpl |.
}
return.
Defined.

Ursus Definition delegateCall (data: bytes): UExpression bytes false.
{
    ::// _result := IImplementation(implementation).execute(data) |.
}
return.
Defined.

Pattern 3: Registry Pattern

Registry Contract:

Contract Registry ;
Sends To IService ;
Inherits ;

Record Contract := {
    services: mapping string address
}.

Ursus Definition register (name: string) (addr: address): UExpression unit false.
{
    ::// services[[name]] := addr |.
}
return.
Defined.

Ursus Definition lookup (name: string): UExpression address false.
{
    ::// _result := services[[name]] |.
}
return.
Defined.

Message Types

Synchronous Calls

Direct function calls (if supported by platform):

::// result := otherContract.getValue() |.

Asynchronous Messages

Send message without waiting for response:

::// otherContract.notify(data) |.

Value Transfer

Send tokens with message:

::// otherContract.deposit{value: amount}() |.

Interface Composition

Multiple Interfaces

A contract can implement multiple interfaces:

Contract MultiService ;
Sends To ITokenReceiver INotifiable IUpgradeable ;
Inherits ;

Interface Inheritance

Interfaces can inherit from other interfaces:

Contract IExtendedToken ;
Sends To ;
Inherits IToken ;

#[no_body]
Ursus Definition mint (to: address) (amount: uint256): UExpression boolean false.

See Also

• Contract Structure - Contract organization
• Interfaces - Interface definitions
• Inheritance - Contract inheritance
• ursus-patterns repository - Multi-contract examples

Contract Inheritance

Ursus supports contract inheritance, allowing you to build modular, reusable contract components. This enables code reuse, abstraction, and hierarchical contract design.

Basic Inheritance

Declaring Parent Contracts

Syntax:

Contract ChildContract ;
Inherits ParentContract ;

Example:

(* Parent contract *)
Contract Ownable ;
Sends To ;
Inherits ;

Record Contract := {
    owner: address
}.

Ursus Definition onlyOwner: UExpression unit true.
{
    ::// require_(msg->sender == owner, "Not owner") |.
}
return.
Defined.

(* Child contract *)
Contract MyToken ;
Sends To ;
Inherits Ownable ;

Record Contract := {
    totalSupply: uint256;
    balances: mapping address uint256
}.

Multiple Inheritance

Inherit from multiple parent contracts:

Syntax:

Inherits Parent1 Parent2 Parent3 ;

Example:

Contract MyContract ;
Sends To ;
Inherits Ownable Pausable ReentrancyGuard ;

Inheritance Modes

Full Inheritance

Inherit all functions and state:

Inherits ParentContract ;

Selective Inheritance

Inherit specific functions:

Inherits ParentContract => overrides [function1 function2] ;

Example:

Contract CustomToken ;
Inherits ERC20 => overrides [transfer transferFrom] ;

Overriding Functions

Basic Override

Parent:

Contract Base ;
Sends To ;
Inherits ;

#[virtual]
Ursus Definition getValue: UExpression uint256 false.
{
    ::// _result := {42} |.
}
return.
Defined.

Child:

Contract Derived ;
Inherits Base ;

#[override]
Ursus Definition getValue: UExpression uint256 false.
{
    ::// _result := {100} |.
}
return.
Defined.

Calling Parent Implementation

Use super to call parent function:

#[override]
Ursus Definition transfer (to: address) (amount: uint256):
  UExpression boolean false.
{
    ::// super->transfer(to, amount) .
    ::// emit CustomTransfer(msg->sender, to, amount) |.
}
return @true.
Defined.

State Inheritance

Merging State

Child contract state includes parent state:

Parent:

Contract Ownable ;
Record Contract := {
    owner: address
}.

Child:

Contract MyToken ;
Inherits Ownable ;

Record Contract := {
    (* Inherited: owner: address *)
    totalSupply: uint256;
    balances: mapping address uint256
}.

Accessing Parent State

Access parent state fields directly:

Ursus Definition checkOwner: UExpression boolean false.
{
    ::// _result := (msg->sender == owner) |.  (* owner from Ownable *)
}
return.
Defined.

Abstract Contracts

Defining Abstract Contracts

Contracts with unimplemented functions:

Contract AbstractToken ;
Sends To ;
Inherits ;

(* Abstract function *)
#[no_body, virtual]
Ursus Definition _beforeTransfer (from to: address) (amount: uint256):
  UExpression unit false.

(* Concrete function *)
Ursus Definition transfer (to: address) (amount: uint256):
  UExpression boolean false.
{
    ::// _beforeTransfer(msg->sender, to, amount) .
    ::// balances[[msg->sender]] := balances[[msg->sender]] - amount .
    ::// balances[[to]] := balances[[to]] + amount |.
}
return @true.
Defined.

Implementing Abstract Functions

Contract ConcreteToken ;
Inherits AbstractToken ;

#[override]
Ursus Definition _beforeTransfer (from to: address) (amount: uint256):
  UExpression unit false.
{
    ::// require_(amount > {0}, "Zero amount") |.
}
return.
Defined.

Interfaces

Defining Interfaces

Contracts with only function signatures:

Contract IERC20 ;
Sends To ;
Inherits ;

#[no_body]
Ursus Definition transfer (to: address) (amount: uint256):
  UExpression boolean false.

#[no_body]
Ursus Definition balanceOf (account: address):
  UExpression uint256 false.

#[no_body]
Ursus Definition approve (spender: address) (amount: uint256):
  UExpression boolean false.

Implementing Interfaces

Contract ERC20 ;
Inherits IERC20 ;

#[override]
Ursus Definition transfer (to: address) (amount: uint256):
  UExpression boolean false.
{
    (* Implementation *)
}
return @true.
Defined.

#[override]
Ursus Definition balanceOf (account: address):
  UExpression uint256 false.
{
    ::// _result := balances[[account]] |.
}
return.
Defined.

Inheritance Patterns

Pattern 1: Ownable

Contract Ownable ;
Sends To ;
Inherits ;

Record Contract := {
    owner: address
}.

Ursus Definition constructor: UExpression unit false.
{
    ::// owner := msg->sender |.
}
return.
Defined.

Ursus Definition onlyOwner: UExpression unit true.
{
    ::// require_(msg->sender == owner, "Not owner") |.
}
return.
Defined.

Ursus Definition transferOwnership (newOwner: address): UExpression unit true.
{
    ::// onlyOwner() .
    ::// owner := newOwner |.
}
return.
Defined.

Pattern 2: Pausable

Contract Pausable ;
Inherits Ownable ;

Record Contract := {
    paused: boolean
}.

Ursus Definition whenNotPaused: UExpression unit true.
{
    ::// require_(!paused, "Paused") |.
}
return.
Defined.

Ursus Definition pause: UExpression unit true.
{
    ::// onlyOwner() .
    ::// paused := @true |.
}
return.
Defined.

Ursus Definition unpause: UExpression unit true.
{
    ::// onlyOwner() .
    ::// paused := @false |.
}
return.
Defined.

Pattern 3: ReentrancyGuard

Contract ReentrancyGuard ;
Sends To ;
Inherits ;

Record Contract := {
    locked: boolean
}.

Ursus Definition nonReentrant: UExpression unit true.
{
    ::// require_(!locked, "Reentrant call") .
    ::// locked := @true |.
}
return.
Defined.

Ursus Definition unlock: UExpression unit false.
{
    ::// locked := @false |.
}
return.
Defined.

Diamond Inheritance

Problem

Multiple inheritance can cause ambiguity:

Contract A ;
Ursus Definition foo: UExpression uint256 false.

Contract B ;
Inherits A ;

Contract C ;
Inherits A ;

Contract D ;
Inherits B C ;  (* Which foo? *)

Solution: Linearization

Ursus uses C3 linearization to resolve:

D -> B -> C -> A

Override explicitly:

Contract D ;
Inherits B C ;

#[override]
Ursus Definition foo: UExpression uint256 false.
{
    ::// _result := B->foo() |.  (* Explicitly choose B's implementation *)
}
return.
Defined.

See Also

• Contract Structure - Contract organization
• Attributes - Function attributes
• Interfaces - Interface definitions
• ursus-patterns repository - Inheritance examples

Ursus Programming Style

Ursus is not just a language—it's a proof-driven development environment built on Coq. Understanding how to work effectively in this environment is essential for productive contract development.

Overview

Programming in Ursus combines:

1. Interactive Development - Using Coq's REPL for immediate feedback
2. Proof Mode - Leveraging Coq's goal-directed programming
3. Tactical Programming - Using tactics to construct code
4. Holes and Refinement - Incremental program construction

This approach enables:

• Type-driven development - Let types guide implementation
• Incremental verification - Prove properties as you code
• Interactive debugging - Inspect goals and context at any point
• Automated code generation - Use tactics to generate boilerplate

The Ursus Workflow

1. Write function signature
   ↓
2. Enter proof mode (see goals)
   ↓
3. Use tactics to refine goals
   ↓
4. Fill holes incrementally
   ↓
5. Complete definition
   ↓
6. Sync with code generator

Key Concepts

REPL (Read-Eval-Print Loop)

Coq provides an interactive environment where you can:

• Load contract files
• Execute commands
• Inspect definitions
• Test functions
• Prove properties

Learn more: REPL

Goals and Context

When writing Ursus functions, you work in proof mode:

• Goal - What you need to construct
• Context - Available variables and hypotheses
• Tactics - Commands to transform goals

Learn more: Goal and Context

Tactics and Tacticals

Tactics are commands that construct code:

• refine - Provide partial term with holes
• :: - Ursus-specific statement tactic
• apply - Apply a function or lemma
• simpl - Simplify expressions
• auto - Automated proof search

Learn more: Tactics and Tacticals

Holes

Holes (_) are placeholders for code to be filled later:

• Type-checked placeholders
• Enable incremental development
• Show what needs to be constructed

Learn more: Holes

Example: Interactive Development

Let's see how to develop a function interactively:

1. Start with Signature

Ursus Definition transfer (to: address) (amount: uint256):
  UExpression boolean false.

2. Enter Proof Mode

Coq shows the goal:

1 subgoal
______________________________________(1/1)
UExpression boolean false

3. Use Tactics to Build Code

{
    refine // balances[[msg->sender]] := balances[[msg->sender]] - amount ; _ //.
}

New goal:

1 subgoal
______________________________________(1/1)
UExpression boolean false

4. Continue Refining

{
    refine // balances[[msg->sender]] := balances[[msg->sender]] - amount ; _ //.
    refine // balances[[to]] := balances[[to]] + amount ; _ //.
    refine // @true //.
}

5. Complete Definition

return.
Defined.
Sync.

Modern Ursus Style

The :: tactic provides cleaner syntax:

Old style (verbose):

refine // new 'x : uint256 @ "x" := {1} ; _ //.
refine // y := y + x ; _ //.
refine // _result := y //.

New style (concise):

{
    ::// var 'x : uint256 := {1} .
    ::// y := y + x .
    ::// _result := y |.
}

Benefits:

• More readable
• Less boilerplate
• Clearer intent
• Easier to maintain

Development Patterns

Pattern 1: Top-Down Development

Start with high-level structure, fill details later:

Ursus Definition complexFunction (x: uint256): UExpression uint256 false.
{
    ::// if x > {100} then { ->> } else { ->> } | .
    {
        (* TODO: Fill then branch *)
        ::// skip_ |.
    }
    {
        (* TODO: Fill else branch *)
        ::// skip_ |.
    }
}
return {0}.
Defined.

Pattern 2: Bottom-Up Development

Build helper functions first:

(* Helper function *)
Ursus Definition calculateFee (amount: uint256): UExpression uint256 false.
{
    ::// var 'fee : uint256 := amount * {3} / {100} |.
}
return fee.
Defined.

(* Main function using helper *)
Ursus Definition processPayment (amount: uint256): UExpression uint256 false.
{
    ::// var 'fee : uint256 := calculateFee(amount) .
    ::// var 'total : uint256 := amount + fee |.
}
return total.
Defined.

Pattern 3: Test-Driven Development

Write tests first, then implement:

(* Test specification *)
Theorem transfer_reduces_sender_balance:
  forall sender to amount s s',
    exec_transfer sender to amount s = Some s' ->
    balance s' sender = balance s sender - amount.
Proof.
  (* Proof guides implementation *)
Admitted.

(* Implementation *)
Ursus Definition transfer (to: address) (amount: uint256):
  UExpression boolean false.
{
    (* Implementation satisfies theorem *)
}
return.
Defined.

Best Practices

1. Use Descriptive Names

Good:

::// var 'totalFee : uint256 := calculateFee(amount) .
::// var 'recipientBalance : uint256 := balances[[recipient]] .

Bad:

::// var 'x : uint256 := calculateFee(amount) .
::// var 'b : uint256 := balances[[recipient]] .

2. Keep Functions Small

Break complex logic into smaller functions:

(* Good: Small, focused functions *)
Ursus Definition validateAmount (amount: uint256): UExpression boolean false.
Ursus Definition updateBalance (addr: address) (amount: uint256): UExpression unit false.
Ursus Definition transfer (to: address) (amount: uint256): UExpression boolean false.

(* Bad: One giant function *)
Ursus Definition doEverything (...): UExpression ... .

3. Use Type Annotations

Help Coq infer types correctly:

::// var 'balance : uint256 := balances[[addr]] .  (* Explicit type *)

4. Leverage Proof Mode

Use Coq's proof mode to explore:

{
    (* Check current goal *)
    Show.

    (* Simplify to see what's needed *)
    simpl.

    (* Continue development *)
    ::// ...
}

Debugging Techniques

Inspect Goals

{
    ::// var 'x : uint256 := {42} .
    Show.  (* See current goal and context *)
    ::// ...
}

Simplify Expressions

{
    simpl.  (* Reduce complex expressions *)
    ::// ...
}

Check Types

Check balances[[addr]].
(* ULValue uint256 *)

Check {42}.
(* URValue uint256 false *)

Next Steps

• REPL - Interactive development environment
• Goal and Context - Understanding proof mode
• Tactics - Building code with tactics
• Holes - Incremental program construction

Further Reading

• Coq Reference Manual - Tactics
• Software Foundations - Tactics
• CPDT - Proof Engineering

REPL - Interactive Development

The Coq REPL (Read-Eval-Print Loop) is your primary interface for developing Ursus contracts. It provides immediate feedback, interactive exploration, and powerful debugging capabilities.

What is the REPL?

The REPL is an interactive environment where you can:

1. Load contract files - Import and compile Ursus code
2. Execute commands - Run Coq commands interactively
3. Inspect definitions - Examine types, values, and proofs
4. Test functions - Evaluate expressions
5. Develop incrementally - Build code step by step

Starting the REPL

CoqIDE

Launch CoqIDE:

coqide MyContract.v &

Features:

• Graphical interface
• Step-by-step execution
• Goal visualization
• Syntax highlighting

Proof General (Emacs)

Launch Emacs with Proof General:

emacs MyContract.v

Key bindings:

• C-c C-n - Execute next command
• C-c C-u - Undo last command
• C-c C-RET - Execute to cursor
• C-c C-b - Execute buffer

VSCode with VSCoq

Install VSCoq extension:

code --install-extension maximedenes.vscoq

Features:

• Modern IDE experience
• Inline goal display
• Error highlighting
• Auto-completion

Command Line (coqtop)

Start interactive session:

coqtop -Q . MyProject

Basic commands:

Coq < Load MyContract.
Coq < Check transfer.
Coq < Print Contract.
Coq < Quit.

Loading Contracts

Load Single File

Load "MyContract.v".

Load with Dependencies

Require Import UrsusEnvironment.Solidity.current.Environment.
Require Import UrsusEnvironment.Solidity.current.LocalGenerator.
Require Import MyContract.

Set Load Path

Add LoadPath "/path/to/ursus" as Ursus.
Require Import Ursus.MyContract.

Interactive Commands

Inspection Commands

Check type:

Check transfer.
(* transfer : address -> uint256 -> UExpression boolean false *)

Print definition:

Print transfer.
(* Shows full definition *)

Print contract:

Print Contract.
(* Shows contract record structure *)

Search for definitions:

Search uint256.
Search "balance".
SearchAbout mapping.

Evaluation Commands

Compute expression:

Compute {42} + {58}.
(* = {100} : URValue uint256 false *)

Evaluate function:

Eval compute in (add_numbers {10} {20}).

Simplify term:

Eval simpl in (balances[[addr]]).

Developing Functions Interactively

Step-by-Step Development

1. Start function definition:

Ursus Definition myFunction (x: uint256): UExpression uint256 false.

REPL shows:

1 subgoal
______________________________________(1/1)
UExpression uint256 false

2. Add first statement:

{
    refine // var 'y : uint256 := x + {1} ; _ //.

REPL shows:

1 subgoal
y : ULValue uint256
______________________________________(1/1)
UExpression uint256 false

3. Complete function:

    refine // y //.
}
return.
Defined.

REPL confirms:

myFunction is defined

Using Show Command

Inspect current goal at any point:

{
    ::// var 'x : uint256 := {42} .
    Show.  (* Display current goal *)
    ::// var 'y : uint256 := x * {2} .
    Show.  (* Display updated goal *)
    ::// _result := y |.
}

Using Proof Mode

Enter proof mode for complex logic:

Ursus Definition complexFunction (x: uint256): UExpression uint256 false.
Proof.
    (* Use tactics *)
    unfold UExpression.
    intro s.
    (* Build term step by step *)
    ...
Defined.

Debugging in the REPL

Inspect Context

Show all variables:

Show.

Output:

1 subgoal
x : ULValue uint256
y : ULValue uint256
balance : ULValue uint256
______________________________________(1/1)
UExpression boolean false

Type Checking

Check expression type:

Check (x + y).
(* URValue uint256 false *)

Check (balances[[addr]]).
(* ULValue uint256 *)

Simplification

Simplify complex expressions:

Eval simpl in (balances[[addr]] + {100}).

Error Messages

When you make a mistake, the REPL shows detailed errors:

::// balance := "hello" .

Error:

Error: The term "hello" has type "string"
while it is expected to have type "uint256".

Common REPL Workflows

Workflow 1: Exploratory Development

(* Load contract *)
Load "MyContract.v".

(* Check existing functions *)
Check transfer.
Print transfer.

(* Test ideas *)
Check (balances[[addr]] + {100}).

(* Develop new function *)
Ursus Definition newFunction ...

Workflow 2: Test-Driven Development

(* Define property *)
Theorem transfer_correct:
  forall from to amount s s',
    exec_transfer from to amount s = Some s' ->
    balance s' to = balance s to + amount.
Proof.
  (* Develop proof interactively *)
  intros.
  unfold exec_transfer.
  simpl.
  ...
Qed.

(* Implement function to satisfy property *)
Ursus Definition transfer ...

Workflow 3: Incremental Refinement

(* Start with stub *)
Ursus Definition myFunction (x: uint256): UExpression uint256 false.
{
    ::// skip_ |.
}
return {0}.
Defined.

(* Test compilation *)
Sync.

(* Refine implementation *)
(* ... edit and reload ... *)

REPL Tips and Tricks

Tip 1: Use Undo

Made a mistake? Undo last command:

CoqIDE: Click "Backward" or Ctrl+U Proof General: C-c C-u coqtop: Undo. or Restart.

Tip 2: Save State

Save your progress:

(* In file MyContract.v *)
Ursus Definition myFunction ...
Defined.
Sync.

(* Save file, reload in REPL *)
Load "MyContract.v".

Tip 3: Quick Testing

Test expressions without defining functions:

Check ({42} + {58}).
Compute ({42} + {58}).

Tip 4: Use Locate

Find where something is defined:

Locate "->".
Locate uint256.
Locate UExpression.

Tip 5: Set Options

Configure REPL behavior:

Set Printing All.        (* Show implicit arguments *)
Unset Printing Notations. (* Show raw terms *)
Set Printing Depth 100.  (* Control output depth *)

See Also

• Goal and Context - Understanding proof mode
• Tactics - Commands for building code
• Holes - Incremental development
• Coq Reference Manual

Goal and Context

When developing Ursus contracts, you work in Coq's proof mode, where you construct code by transforming goals using tactics. Understanding goals and context is essential for effective development.

What is a Goal?

A goal is what you need to construct. In Ursus, goals are typically:

• Function bodies - UExpression T b
• Expressions - URValue T b
• Statements - UExpression unit b
• Proofs - Prop (for verification)

Goal Display

When you enter proof mode, Coq shows:

n subgoals
var1 : type1
var2 : type2
...
______________________________________(1/n)
GoalType

Components:

• Context (above line) - Available variables and hypotheses
• Separator - Horizontal line with goal number
• Goal (below line) - What you need to construct

Example: Function Development

Initial Goal

Ursus Definition transfer (to: address) (amount: uint256):
  UExpression boolean false.

Coq shows:

1 subgoal
to : address
amount : uint256
______________________________________(1/1)
UExpression boolean false

Interpretation:

• Context: You have to and amount available
• Goal: You need to construct UExpression boolean false

After First Statement

{
    ::// var 'sender_balance : uint256 := balances[[msg->sender]] .

Coq shows:

1 subgoal
to : address
amount : uint256
sender_balance : ULValue uint256
______________________________________(1/1)
UExpression boolean false

Interpretation:

• Context: Now includes sender_balance
• Goal: Still need to construct UExpression boolean false

After More Statements

    ::// balances[[msg->sender]] := sender_balance - amount .
    ::// balances[[to]] := balances[[to]] + amount .

Coq shows:

1 subgoal
to : address
amount : uint256
sender_balance : ULValue uint256
______________________________________(1/1)
UExpression boolean false

Interpretation:

• Context: Unchanged (statements don't add variables)
• Goal: Still need final return value

Final Statement

    ::// _result := @true |.
}
return.
Defined.

Goal satisfied!

Understanding Context

The context contains everything available for constructing the goal:

Types of Context Entries

1. Function parameters:

to : address
amount : uint256

2. Local variables:

sender_balance : ULValue uint256
fee : ULValue uint256

3. Hypotheses (in proofs):

H1 : amount > 0
H2 : balance >= amount

4. Implicit arguments:

T : Type
b : bool

Using Context

You can use any variable from the context:

{
    ::// var 'total : uint256 := amount + fee .  (* Uses amount and fee from context *)
    ::// balances[[to]] := total .               (* Uses to and total from context *)
}

Multiple Goals

Some tactics create multiple goals:

Example: If-Then-Else

{
    ::// if amount > {100} then { ->> } else { ->> } | .

Coq shows:

2 subgoals
to : address
amount : uint256
______________________________________(1/2)
UExpression unit false

______________________________________(2/2)
UExpression unit false

Interpretation:

• Goal 1: Then branch
• Goal 2: Else branch

Solving Multiple Goals

Solve first goal (then branch):

{
    ::// balances[[to]] := balances[[to]] + amount |.
}

Coq shows:

1 subgoal
to : address
amount : uint256
______________________________________(1/1)
UExpression unit false

Solve second goal (else branch):

{
    ::// skip_ |.
}

All goals solved!

Goal Transformations

Tactics transform goals in various ways:

Refinement

Before:

______________________________________(1/1)
UExpression uint256 false

After refine // var 'x : uint256 := {42} ; _ //:

x : ULValue uint256
______________________________________(1/1)
UExpression uint256 false

Simplification

Before:

______________________________________(1/1)
UExpression (if true then uint256 else uint8) false

After simpl:

______________________________________(1/1)
UExpression uint256 false

Unfolding

Before:

______________________________________(1/1)
MyType

After unfold MyType:

______________________________________(1/1)
UExpression uint256 false

Inspecting Goals and Context

Show Command

Display current goal:

{
    ::// var 'x : uint256 := {42} .
    Show.
}

Output:

1 subgoal
x : ULValue uint256
______________________________________(1/1)
UExpression uint256 false

Show Proof

Display proof term constructed so far:

Show Proof.

Output:

(let x := {42} in ?Goal)

Check in Context

Check type of expression in current context:

{
    ::// var 'x : uint256 := {42} .
    Check (x + {1}).
    (* URValue uint256 false *)
}

Common Goal Patterns

Pattern 1: Expression Goal

______________________________________(1/1)
UExpression T b

Solution: Construct expression of type T with panic flag b

Pattern 2: Value Goal

______________________________________(1/1)
URValue T b

Solution: Provide value of type T

Pattern 3: Unit Goal

______________________________________(1/1)
UExpression unit false

Solution: Execute statements (side effects only)

Pattern 4: Boolean Goal

______________________________________(1/1)
UExpression boolean false

Solution: Return boolean value

Pattern 5: Proof Goal

______________________________________(1/1)
balance_after = balance_before + amount

Solution: Prove the proposition

Working with Complex Goals

Nested Structures

Goal:

______________________________________(1/1)
UExpression (optional (mapping address uint256)) false

Strategy:

1. Understand the type structure
2. Build from inside out
3. Use helper functions if needed

Dependent Types

Goal:

______________________________________(1/1)
UExpression (if b then uint256 else uint8) false

Strategy:

1. Simplify the condition
2. Case analysis on b
3. Solve each case

Debugging with Goals

Problem: Wrong Type

Goal:

______________________________________(1/1)
UExpression uint256 false

Attempt:

::// _result := "hello" |.

Error:

Error: The term "hello" has type "string"
while it is expected to have type "URValue uint256 false"

Solution: Check types match goal

Problem: Missing Variable

Goal:

______________________________________(1/1)
UExpression uint256 false

Attempt:

::// _result := undefined_var |.

Error:

Error: The reference undefined_var was not found

Solution: Check context for available variables

Problem: Wrong Panic Flag

Goal:

______________________________________(1/1)
UExpression uint256 false

Attempt:

::// _result := may_panic_function() |.

Error:

Error: Cannot unify "UExpression uint256 true"
with "UExpression uint256 false"

Solution: Use non-panicking expression or change function signature

See Also

• REPL - Interactive development
• Tactics - Transforming goals
• Holes - Incremental construction
• Coq Tactics Index

Tactics and Tacticals

Tactics are commands that construct code by transforming goals. In Ursus, tactics are your primary tool for building contract functions.

Core Ursus Tactics

The :: Tactic

The main tactic for writing Ursus statements:

Syntax:

::// statement .
::// statement |.

What it does:

• Processes Ursus statement notation
• Automatically sequences statements
• Handles type inference

Example:

{
    ::// var 'x : uint256 := {42} .
    ::// y := y + x .
    ::// _result := y |.
}

The refine Tactic

Provide a partial term with holes:

Syntax:

refine term.

Example:

{
    refine // var 'x : uint256 := {42} ; _ //.
    refine // _result := x //.
}

Use cases:

• Low-level control
• Complex expressions
• When :: doesn't work

The return Command

Complete function definition:

Syntax:

return.
return value.

Examples:

(* No return value *)
return.

(* With return value *)
return balance.

(* With expression *)
return {0}.

Standard Coq Tactics

simpl - Simplify

Reduce expressions:

{
    simpl.  (* Simplify current goal *)
    ::// ...
}

Example:

(* Before simpl *)
Goal: UExpression (if true then uint256 else uint8) false

(* After simpl *)
Goal: UExpression uint256 false

unfold - Expand Definitions

Expand defined terms:

{
    unfold MyType.
    ::// ...
}

Example:

unfold UExpression.
(* Reveals: ContractState -> Result (A * ContractState) *)

intro / intros - Introduce Variables

Introduce function parameters:

Proof.
    intros x y z.
    (* x, y, z now in context *)

apply - Apply Function

Apply a function or lemma:

{
    apply my_helper_function.
}

exact - Provide Exact Term

Give exact solution:

{
    exact {42}.
}

Tacticals (Tactic Combinators)

; - Sequence

Apply tactic, then apply another to all subgoals:

{
    split; simpl.
    (* Splits goal, then simplifies both subgoals *)
}

|| - Try Alternatives

Try first tactic, if it fails try second:

{
    (apply lemma1 || apply lemma2).
}

try - Try Without Failing

Try tactic, continue if it fails:

{
    try simpl.
    (* Simplifies if possible, continues otherwise *)
}

repeat - Repeat Until Failure

Repeat tactic until it fails:

{
    repeat (simpl; unfold).
}

do - Repeat N Times

Repeat tactic exactly N times:

{
    do 3 intro.
    (* Introduces 3 variables *)
}

Ursus-Specific Patterns

Pattern 1: Variable Declaration

::// var 'name : type := value .

Expands to:

refine (let name := value in _).

Pattern 2: Assignment

::// lvalue := rvalue .

Expands to:

refine (UAssign lvalue rvalue ; _).

Pattern 3: Control Flow

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

Creates two subgoals:

1. Then branch body
2. Else branch body

Advanced Tactics

Show - Display Goal

Show current goal and context:

{
    ::// var 'x : uint256 := {42} .
    Show.
    ::// ...
}

Check - Type Check

Check type of expression:

{
    Check (x + y).
    (* URValue uint256 false *)
}

assert - Add Hypothesis

Add intermediate fact:

Proof.
    assert (H: x > 0).
    { (* Prove H *) }
    (* Use H in main proof *)

destruct - Case Analysis

Analyze by cases:

Proof.
    destruct b.
    { (* Case: b = true *) }
    { (* Case: b = false *) }

induction - Inductive Proof

Prove by induction:

Proof.
    induction n.
    { (* Base case: n = 0 *) }
    { (* Inductive case: n = S n' *) }

Debugging Tactics

idtac - Print Message

Print debug message:

{
    idtac "Reached this point".
    ::// ...
}

fail - Force Failure

Force tactic to fail (for testing):

{
    fail "This should not happen".
}

admit - Skip Proof

Temporarily skip proof (for development):

Proof.
    admit.
Admitted.

Warning: Don't use in production!

See Also

• REPL - Interactive development
• Goal and Context - Understanding goals
• Control Sub-language - Control flow tactics
• Holes - Using holes effectively
• Coq Tactics Reference

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

Holes

Holes (_) are placeholders in Coq that represent code to be filled in later. They are essential for incremental development in Ursus.

What are Holes?

A hole is a placeholder that:

1. Type-checked - Must have correct type
2. Named or anonymous - Can be referenced
3. Filled incrementally - Complete step by step
4. Verified - Type system ensures correctness

Syntax:

_           (* Anonymous hole *)
?name       (* Named hole *)

Holes in Ursus

Statement Holes

Pattern:

refine // statement ; _ //.

Example:

{
    refine // var 'x : uint256 := {42} ; _ //.
    (* Hole for rest of function *)
}

Coq shows:

1 subgoal
x : ULValue uint256
______________________________________(1/1)
UExpression uint256 false

Expression Holes

Pattern:

refine (some_function _ _).

Example:

{
    refine (UPlus _ _).
    (* Two holes for operands *)
}

Control Flow Holes

Pattern:

::// if condition then { ->> } else { ->> } | .

The ->> and -/> are special holes:

• ->> - Non-panicking code block
• -/> - Potentially panicking code block

Example:

::// if balance > amount then { ->> } else { -/> } | .
{
    (* Non-panicking branch *)
    ::// balance := balance - amount |.
}
{
    (* Panicking branch *)
    ::// exit_ {1} |.
}

Panic Holes

Non-Panicking Hole (->>)

Indicates code that completes normally:

{ ->> }

Type:

UExpression unit false

Use when:

• Code always succeeds
• No exit_ or require_ calls
• No panicking function calls

Example:

::// if x > {0} then { ->> } | .
{
    ::// y := x + {1} |.  (* Always succeeds *)
}

Panicking Hole (-/>)

Indicates code that may panic:

{ -/> }

Type:

UExpression unit true

Use when:

• Code may call exit_
• Code may call require_
• Code calls panicking functions

Example:

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

Hole with Placeholder (_)

Use _ for complex conditions:

::// if _ then { ->> } else { ->> } | .
(complex_condition)  (* Condition specified after *)
{
    (* then branch *)
}
{
    (* else branch *)
}

Example:

::// if _ then { ->> } else { ->> } | .
(balance[[sender]] >= amount && amount > {0})
{
    ::// transfer_internal(sender, recipient, amount) |.
}
{
    ::// skip_ |.
}

Incremental Development with Holes

Step 1: Skeleton

Start with high-level structure:

Ursus Definition transfer (to: address) (amount: uint256):
  UExpression boolean false.
{
    refine // _ //.  (* Hole for entire body *)
}
return @false.
Defined.

Step 2: Add Structure

Fill in control flow:

Ursus Definition transfer (to: address) (amount: uint256):
  UExpression boolean false.
{
    refine // if _ then { ->> } else { ->> } ; _ //.
    (balances[[msg->sender]] >= amount)
    {
        refine // _ //.  (* Hole for then branch *)
    }
    {
        refine // _ //.  (* Hole for else branch *)
    }
    refine // _ //.  (* Hole for rest *)
}
return @false.
Defined.

Step 3: Fill Branches

Complete each branch:

Ursus Definition transfer (to: address) (amount: uint256):
  UExpression boolean false.
{
    refine // if _ then { ->> } else { ->> } ; _ //.
    (balances[[msg->sender]] >= amount)
    {
        refine // balances[[msg->sender]] := balances[[msg->sender]] - amount ; _ //.
        refine // balances[[to]] := balances[[to]] + amount //.
    }
    {
        refine // skip_ //.
    }
    refine // @true //.
}
return.
Defined.

Named Holes

Use named holes for complex development:

Syntax:

?hole_name

Example:

{
    refine (UPlus ?left ?right).
}

Coq shows:

2 subgoals
______________________________________(1/2)
URValue uint256 false  (* ?left *)

______________________________________(2/2)
URValue uint256 false  (* ?right *)

Hole Errors

Type Mismatch

Error:

Error: Cannot infer type of hole

Solution: Provide type annotation

Before:

refine _.

After:

refine (_ : UExpression uint256 false).

Unfilled Holes

Error:

Error: Attempt to save an incomplete proof

Solution: Fill all holes before Defined

Wrong Panic Flag

Error:

Error: Cannot unify "UExpression unit true"
with "UExpression unit false"

Solution: Use correct hole type (->> vs -/>)

Best Practices

1. Start with Holes

Begin with skeleton, fill incrementally:

{
    refine // _ ; _ ; _ //.  (* Three statements *)
}

2. Use Descriptive Names