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 := {
}.

URSUS language Documentation