Function declaration

Every function mostly is declared via using proof mode in Coq and command Ursus. Let's see how to declare function.

#[attribute1, attribute2..., returns=returnName]
Ursus Definition functionName (arg1:type1) ... (argN:typeN): UExpression returnType ErrorMark.

Where:

  1. Ursus is already mentioned command which inputs Definition.
  2. functionName is name of declaring function.
  3. (arg1:type1) ... (argN:typeN) are arguments, where argI and typeI are argument name and argument type of ith argument.
  4. returnName and returnType are "variable name" and type of returning term/object respectively.
  5. attributeI is attribute with the same semanthic as solidity has. Moreover, not only the attributes of solidity functions are available here. Also here is attribute no_body, which means following statement: term of type UExpression... doesn't exist. So, as mentioned in QuickStart here is 2 goals in proof mode in declaring Ursus function, but with attribute no_body only one goal (IReturnExpression) needs to be declared ("solve").
  6. Finally, ErrorMark is actually either true or false term, which expresses if it contains calling require, revert and others "bad" functions here.

After swithing to proof mode two goals are here: UExpression returnType ErrorMark and IReturnExpression.

Conception of ULValue and URValue

ULValue and URValue types of terms that are used in describing function bodies: function callings, assignment and so on. Simply, we can consider ULValue as "reference type" or things that can be assigned a value. We can consider URValue as usual type or things that can't be assigned a value. ULValue can automatically cast to URValue via Coq coercion mechanism. In Ursus we can't use literal itself, we need to wrap it into URValue, so for this goal we can use brackets {...}. For example, "str" of Coq type string now is → {"string"} of type URValue string false. ULValue has type Type -> Type and URValue has type Type -> bool -> Type. Term of type bool has similar semanthic as UExpression... has.

Example is below.

Create term with hole approach

Let's look at basic scenario of describing function (without loops and if statements)

Basic syntax of function body can be introduced via next BNF:

UExpression ::= // simpleUExpression // | // (UExpression ; UExpression) //

i.e function body can be expressed this way:

// simpleUExpression ;
(simpleUExpression ;
(simpleUExpression ;
simpleUExpression)) //

And main idea is using standart tactic refine, so the description will take the following form:

refine // simpleUExpression ; _ // .
refine // simpleUExpression ; _ // .
refine // simpleUExpression ; _ // .
refine // simpleUExpression // .

Where:

  1. '_' symbol means, that rest of term is needed to construct.
  2. // ... // "brackets" means only some special construction might be here

Firstly, consider next simpleUExpression:

  1. declaring "variable" new 'name : typeName @ "name" := value

    Where:

    1. name is variable name (notice! name and "name" must be the same)
    2. typeName is type of this variable
    3. value is term of type typeName

  2. function a + b, which has usual semanthic, (a and b are num with the same type, for example uint)

  3. assignment variable := term

    Where:

    1. variable is "variable", which was declared before asignment
    2. term is variable or function

For example, consider our first Ursus function:

#[pure, returns=_result]
Ursus Definition addOne (y : uint) : UExpression uint false.
refine // new 'x  : uint @ "x"  := {1} ; _  //.
refine // y := y + x ; _  //.
refine // _result := y // .
return.
Defined.
Sync.

it will be prettier to rewrite in such way via using goal separator {...}:

#[pure, returns=_result]
Ursus Definition addOne (y : uint) : UExpression uint false.
{ 
   refine // new 'x  : uint @ "x"  := {1} ; _  //.
   refine // y := y + x ; _  //.
   refine // _result := y // .
}
return.
Defined.
Sync.

Nice! Consider custom tactic ::, it works like refine, but here is some features to reduce code. Now we can declare variable with the same semantic, but with new syntax var name : typeName := value And consider new way of declaring statements via using next notations:

  1. '//' e ';' _ '//' → '//' e
  2. '//' e '//' → '//' e '|'

Where 'e' is term of UExpression... type.

And our code become look like this:

#[pure, returns=_result]
Ursus Definition addOne (y : uint) : UExpression uint false.
{ 
   ::// var 'x  : uint := {1} .
   ::// y := y + x .
   ::// _result := y |.
}
return.
Defined.
Sync.

Why should we still use construction new ..., there is one reason var ... doesn't allow to write code in one "piece":

#[pure, returns=_result]
Ursus Definition addOne (y : uint) : UExpression uint false.
refine // new 'x  : uint @ "x"  := {1} ; y := y + x ; _result := y  //.
return.
Defined.
Sync.

How we can use Ursus function below?

Let's consider use case of addOne function. For example: ::// var new_y: uint := addOne(y);_|.

Where y is URValue uint ... or ULValue uint, which was casted to URValue uint false.

ULValue-URValue

In example above, consider type of each term are used here (or what would say coq proof mode):

  1. y: ULValue uint
  2. x: ULValue uint
  3. {1}: URValue uint false
  4. _result: ULValue uint (coq get this type from UExpression uint false return type)

Basic construction

Let's look to full simpleUExpression list:

  1. assignment // a := b , where a and b have the same type, but a is ULValue and b is URValue:

    1. a is variable or field of contract or structure
    2. b is variable or result of function or field of contract or structure
    3. Operations with assignment. Here is list of available operations with assignment with standart semantic: x += y, x -= y, x &= y, x |= y, x /= y, x *= y, ++ x, x ++, x --, -- x,

    Where: x is ULValue and y is URValue

  2. declaring new varibale // new 'x : ty @ b := r ; _ | (deprecated),

    Where:

    1. x is name of variable (important! to use symbol "'")
    2. ty is type of variable r
    3. r is value with type URValue...
    4. _ is rest of UExpression which needs to construct Notice, This way of declaring variable allows to create UExpression without refine or :: tactic. After this statement, x will have type ULValue ty.

  3. declaring variables as tuple // new ( x1 : ty1 , x2 : ty2 ) @ ( xb1 , xb2 ) := r ; _ |"

    Where:

    1. x1 and x2 are name of variable
    2. ty1 is ty2 are type of variable
    3. xb1 , xb2 are strings of name x1 and x2 respectively
    4. r is value with type ty1 ** ty2

  4. declaring variable (works only with ::) as tuple // var ( x1 : ty1 , x2 : ty2 ) := r ; _ |

    Where:

    1. x1 and x2 are name of variable
    2. ty1 is ty2 are type of variable
    3. r is value with type ty1 ** ty2

  5. declaring variable (works only with ::) as tuple // var x1 : ty1 , x2 : ty2 ; _ | (the same as previous bullet point, but value us default for each type)

After these (point 3,4,5) statement, x1 and x2 will have type ULValue ty1 and ULValue ty2 respectively.

  1. calling Ursus function // function (arg1,...,argN),

    Where

    1. function is Ursus function or Ursus Defintion, which was declared above.
    2. arguments arg1,...,argN, where
      1. argI is result of some function or variable (has type URValue...)

Complex construction

Consider contruction, which has "body", i.e. consist of another UExpression. We have already worked with it via using // _ ; _ //.

  1. First will be if-statement if x then { y } else { z }

    1. x is term with type boolean (URValue boolean mark). mark is false or true.
    2. y and z have type the same as type of term, whose part is this if-statement;

    For example consider, our old function

    #[pure, returns=_result]
Ursus Definition addOne (y : uint) : UExpression uint false.
{ 
   ::// var 'x  : uint := {1} .
   ::// if (x < y) then { ->\> } else { ->\> }.
   {
      ::// y := y + x |.
   }
   {
      ::// y := x + y |.
   }
   ::// _result := y |.
}
return.
Defined.
Sync.

    Let's consider line ::// if (x < y) then { ->\> } else { ->\> }. before interpreting this line we have one goal UExpression ..., after that we give to this goal expression if x < y then { ->\> } else { ->\> } and for defining this expression we need to give 2 part of if-statement: true-body and false-body. Notation ->\> means { _ : UExpression ...} (placeholer basicaly, which means that we need define this term below). So after interpretting this constructions we have three goals: true-body, false-body, rest of function. And in the example these "bodies" are: 3. true-body is ::// y := y + x |. 4. false-body is ::// y := x + y |. 5. rest of function is ::// _result := y |.

  2. Consider if x then { y } if-statement. It is the same as the previous point, but here we don't need to define false-body (false-body is void actually here).

  3. Consider while b do { f } while-statement with usual semanthic from imperative language,

    Where

    1. b is term with type boolean (URValue boolean mark). mark is false or true.
    2. f is UExpression (let's call it while-body)

  4. Consider doWhile b { f } do-while-statement or do-repeat-statement with usual semanthic from imperative language, Where

    1. b is term with type boolean (URValue boolean mark). mark is false or true.
    2. f is UExpression (let's call it do-while-body)

  5. Consider for (var x : ty := r , b , after ) do { f } for-statement is syntax sugar of this expression: // var x : ty := r ; while ( b ) do { f ; after }

    1. So, we can do something with x in body f

  6. Consider for ( [ k , v ] in m ) do { f } for-each-expression, which has next semanthic in case of type m:

    1. Let m of type mapping keyType valueType, so on body expression variable k and v are aviable in f body,

    Where k and v are key and value type, respectively. It iterates for each key and value of this mapping 2. Let m of type A[],

    Where k and v are uint and A type, respectively. It iterates for each index and value of array A[] 3. So, we can do something with k and v, they have types ULValue key and ULValue value respectively in body f.

  7. Consider for ( [ k , v ] in m ; cond ) do { f } for-each-expression with condition has the same semantic as the previus one, but iteration can break if conidtion cond isn't satisfied.

    1. So, we can do something with k and v, they have types ULValue key and ULValue value respectively in body f.

  8. Consider for ( v in m ) do { f } yet another version of for-each-expression, which has next semanthic in case of type m:

  9. Let m of type mapping keyType valueType, so on body expression variable v is aviable in f body,

Where v has value type. It iterates for each value of this mapping 2. Let m of type A[], 

Where ```v``` has ```A``` type. It iterates for each value of array ```A[]```
  1. So, we can do something with v, it has type ULValue value respectively in body f.
  2. Consider for ( v in m ; cond ) do { f } for-each-expression with condition has the same semantic as the previus one, but iteration can break if conidtion cond isn't satisfied.
    1. So, we can do something with v, it has type ULValue value respectively in body f.

How to model modifiers?

Ursus can model modifiers as simple void function (let's call it as modifier_example), i.e. term with the next type: type1 -> ... -> typeN -> UExpression PhantomType false or type1 -> ...-> typeN -> UExpression PhantomType true. And modifier invocation will use like this in Ursus function:

Ursus Definition some_function:UExpression PhantomType false.
::// modifier_example() ;_|.
{
    ...
}
return.
Defined.