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:
Ursus
is already mentioned command which inputsDefinition
.functionName
is name of declaring function.(arg1:type1) ... (argN:typeN)
are arguments, whereargI
andtypeI
are argument name and argument type of ith argument. returnName and returnType are "variable name" and type of returning term/object respectively.
attributeI
is attribute with the same semanthic as solidity has. Moreover, not only the attributes of solidity functions are available here. Also here is attributeno_body
, which means following statement: term of typeUExpression...
doesn't exist. So, as mentioned in QuickStart here is 2 goals in proof mode in declaring Ursus function, but with attributeno_body
only one goal (IReturnExpression) needs to be declared ("solve"). 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:
 '
_
' symbol means, that rest of term is needed to construct. // ... //
"brackets" means only some special construction might be here
Firstly, consider next simpleUExpression
:

declaring "variable"
new 'name : typeName @ "name" := value
Where:
name
is variable name (notice!name
and "name
" must be the same)typeName
is type of this variablevalue
is term of typetypeName

function
a + b
, which has usual semanthic, (a
andb
are num with the same type, for exampleuint
) 
assignment
variable := term
Where:
 variable is "variable", which was declared before asignment
 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:
'//' e ';' _ '//'
→'//' e
'//' 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
.
ULValueURValue
In example above, consider type of each term are used here (or what would say coq proof mode):
y: ULValue uint
x: ULValue uint
{1}: URValue uint false
_result: ULValue uint
(coq get this type fromUExpression uint false
return type)
Basic construction
Let's look to full simpleUExpression list:

assignment
// a := b
, wherea
andb
have the same type, buta
isULValue
andb
isURValue
:a
is variable or field of contract or structureb
is variable or result of function or field of contract or structure 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
isULValue
andy
isURValue

declaring new varibale
// new 'x : ty @ b := r ; _ 
(deprecated),Where:
x
is name of variable (important! to use symbol "'
")ty
is type of variabler
r
is value with typeURValue...
_
is rest ofUExpression
which needs to construct Notice, This way of declaring variable allows to create UExpression withoutrefine
or::
tactic. After this statement,x
will have typeULValue ty
.

declaring variables as tuple
// new ( x1 : ty1 , x2 : ty2 ) @ ( xb1 , xb2 ) := r ; _ "
Where:
x1
andx2
are name of variablety1
isty2
are type of variablexb1
,xb2
are strings of namex1
andx2
respectivelyr
is value with typety1 ** ty2

declaring variable (works only with
::
) as tuple// var ( x1 : ty1 , x2 : ty2 ) := r ; _ 
Where:
x1
andx2
are name of variablety1
isty2
are type of variabler
is value with typety1 ** ty2

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.

calling Ursus function
// function (arg1,...,argN)
,Where
function
is Ursus function or Ursus Defintion, which was declared above. arguments
arg1,...,argN
, whereargI
is result of some function or variable (has typeURValue...
)
Complex construction
Consider contruction, which has "body", i.e. consist of another UExpression. We have already worked with it via using // _ ; _ //
.

First will be ifstatement
if x then { y } else { z }
x
is term with type boolean (URValue boolean mark
).mark
is false or true.y
andz
have type the same as type of term, whose part is this ifstatement;
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 goalUExpression ...
, after that we give to this goal expressionif x < y then { >\> } else { >\> }
and for defining this expression we need to give 2 part of ifstatement: truebody and falsebody. Notation>\>
means{ _ : UExpression ...}
(placeholer basicaly, which means that we need define this term below). So after interpretting this constructions we have three goals: truebody, falsebody, rest of function. And in the example these "bodies" are: 3. truebody is::// y := y + x .
4. falsebody is::// y := x + y .
5. rest of function is::// _result := y .

Consider
if x then { y }
ifstatement. It is the same as the previous point, but here we don't need to define falsebody (falsebody is void actually here). 
Consider
while b do { f }
whilestatement with usual semanthic from imperative language,Where
b
is term with type boolean (URValue boolean mark
).mark
is false or true.f
isUExpression
(let's call it whilebody)

Consider
doWhile b { f }
dowhilestatement or dorepeatstatement with usual semanthic from imperative language, Whereb
is term with type boolean (URValue boolean mark
).mark
is false or true.f
isUExpression
(let's call it dowhilebody)

Consider
for (var x : ty := r , b , after ) do { f }
forstatement is syntax sugar of this expression:// var x : ty := r ; while ( b ) do { f ; after }
 So, we can do something with
x
in bodyf
 So, we can do something with

Consider
for ( [ k , v ] in m ) do { f }
foreachexpression, which has next semanthic in case of typem
: Let
m
of typemapping keyType valueType
, so on body expression variablek
andv
are aviable inf
body,
Where
k
andv
arekey
andvalue
type, respectively. It iterates for each key and value of this mapping 2. Letm
of typeA[]
,Where
k
andv
areuint
andA
type, respectively. It iterates for each index and value of arrayA[]
3. So, we can do something withk
andv
, they have typesULValue key
andULValue value
respectively in bodyf
.  Let

Consider
for ( [ k , v ] in m ; cond ) do { f }
foreachexpression with condition has the same semantic as the previus one, but iteration can break if conidtioncond
isn't satisfied. So, we can do something with
k
andv
, they have typesULValue key
andULValue value
respectively in bodyf
.
 So, we can do something with

Consider
for ( v in m ) do { f }
yet another version of foreachexpression, which has next semanthic in case of typem
: 
Let
m
of typemapping keyType valueType
, so on body expression variablev
is aviable inf
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[]```
 So, we can do something with
v
, it has typeULValue value
respectively in bodyf
.  Consider
for ( v in m ; cond ) do { f }
foreachexpression with condition has the same semantic as the previus one, but iteration can break if conidtioncond
isn't satisfied. So, we can do something with
v
, it has typeULValue value
respectively in bodyf
.
 So, we can do something with
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.