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