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