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.