# Mathematical Operations

This page describes the details of how different integer types are handled in
CVL. The exact rules for casting between `uint`

and `mathint`

types are
described in detail.

Warning

The details of implicit and explicit casting between `uint*`

, `int*`

, and
`mathint`

in CVL are complicated, and depend not only on the expressions being
cast but also on the context in which the resulting expressions are used.
For example, assignment statements work differently than return statements.

This document contains the best existing documentation for the current implementation, although it is missing some detail. However, this portion of CVL is also in the process of being redefined and simplified.

In the mean time, we recommend the following rules of thumb:

where possible, use

`mathint`

use

`uint`

or`int`

types only when you need to pass values to solidity functionsdefer casting from

`mathint`

to`uint`

until as late as possible.

Contents

## Mathematical operations

In CVL, arithmetic operators (+, -, * and /) are overloaded: they could mean a machine-arithmetic operation that can overflow, or a mathematical operation that does not overflow. The default interpretation used in almost all cases is the mathematical one. Therefore, the assertion below holds:

```
uint x;
assert x + 1 > x;
```

The syntax supports Solidity’s integer types (`uintXX`

and `intXX`

) as well as
the CVL-only type `mathint`

representing the domain of mathematical integers
(ℤ). Using these types allows controlling how arithmetic operators such as +,
-, and * are interpreted. Therefore, in the following variant on the above
example, if we wish the + operation to be the overflowing variant, we can write
the following:

```
uint x;
uint y = x + 1;
assert y > x;
```

The assertion here will fail with `x = MAX_INT`

, since then y is equal to 0. If
we write instead:

```
uint x;
mathint y = x + 1;
assert y > x;
```

The meaning is the same as in the first snippet since an assignment to a `mathint`

variable allows non-overflowing interpretations of the arithmetic operators.

The only case in which arithmetic operators in expressions are allowed to overflow is within arguments passed to functions, or generally, whenever we interact with the code being checked. Solidity functions cannot take values that do not fit within 256 bits. Therefore the tool will report an overflow error if `mathint`

variable is passed directly as a function argument.

```
uint256 MAX_INT = 2^256 - 1;
foo(MAX_INT + 1); // equivalent to invoking foo(0)
assert MAX_INT + 1 == 0; // always false, because ‘+’ here is mathematical
mathint x = MAX_INT + 1;
foo(x); // error
```

## Maximum values

The maximum values of Solidity integer types are available as the following variables in CVL:

`max_uint`

and`max_uint256`

`max_uint160`

and`max_address`

`max_uint128`

`max_uint96`

`max_uint64`

`max_uint32`

`max_uint16`

`max_uint8`

## Implicit casting

Only the following *implicit* cast operations are supported in CVL:

`numberLiteral`

can implicitly cast to`int*`

`uint*`

`mathint`

`address`

and`bytesK`

.Note, however, that before casting a

`numberLiteral`

to target type`int*`

`uint*`

`address`

or`bytesK`

, it is (statically) checked that the value of the`numberLiteral`

is within the bounds for a safe cast to the target type (e.g.`numberLiteral >= 0 && numberLiteral <= 2^256 - 1`

for`uint256`

). In case the value is out of bounds, an*explicit*cast is required. There is no bounds checking when target type is`mathint`

.Sometimes, even when the

`numberLiteral`

expression is within bounds, it is not possible to implicitly cast the expression to the target type when the value of expression cannot be determined statically (e.g.`uint256 uu = true ? 42 : 24`

). In this case, an explicit cast is required.

For

`uint*`

we have the following cases for implicit casts:`uint_k1`

can implicitly cast to`uint_k2`

when`k1 <= k2`

`uint_k1`

can implicitly cast to`address`

when`k1 <= 160`

. Moreover,`address`

can implicitly cast to`uint256`

, but*not*the other way around. (Note : This is different from earlier behavior because before,`uint256`

and`address`

were aliases).`uint*`

can implicitly cast to`mathint`

. (Note that there is a**difference**in implicit and explicit casts from`uint256`

to`mathint`

when the expression value is outside the range of a`uint256`

variable. While in the implicit cast the`uint256`

value remains unchanged when converted to`mathint`

, the explicit cast takes a*mod*of the value with`2^256`

. Again, this difference will be “visible” only when casting unsafely from a`uint`

to`mathint`

, i.e. when the`uint`

value is greater than`2^256`

)

NOTE: When performing an

*implicit*cast, the type of the expression being cast*changes*to the`targetType`

except in the case when the expression is either a*variable*or a*ghostVariable*. In these two cases, it is only checked that the expression type is a*subtype*of the`targetType`

. If the expression type is a subtype of the`targetType`

the expression is successfully type checked. Consider the following example:

```
uint256 x; // x has type uint256
mathint m1; // m1 has type mathint
mathint y = x + m1; // check that x's type (uint256) is a subtype of targetType (mathint) -- true
assert x < max_uint // x STILL has type uint256
```

## Explicit casting

An explicit cast operator tries to convert the type of an operand from its original type to the target type. The

*conversion*below specifies how the original expression is modified to a value in the target type. Furthermore,*safe_cast_bounds*specify the range of values for the original expression under which the conversion to the target type is safe to perform (i.e. does not result in an*overflow*). When the value is out of safe bounds (say in case of`to_uint256(-1)`

), it results in an*overflow*. Here are the rules for performing different cast operations:**To Unsigned Int****Syntax**:`to_uint256(exp)`

**Rules:**`mathint`

to`uint`

conversion:

`exp mod 2^256`

safe_cast_bounds for warning:

`exp >= 0 && exp <= 2^256 - 1`

Signed

`int`

To unsigned`uint`

conversion:

`exp`

safe_cast_bounds:

`None`

NumberLiteral to UnsignedInt

conversion:

`exp mod 2^256`

safe_cast_bounds for warning:

`exp >= 0 && exp <= 2^256 - 1`

`bytesK`

to UnsignedIntconversion:

`exp`

safe_cast_bounds for warning:

`None`

**To Signed Int****Syntax**:`to_int256(exp)`

**Rules:**`mathint`

to SignedIntconversion:

`exp mod 2^256`

safe_cast_bounds for warning:

`exp >= -2^255 && exp <= 2^255 - 1`

UnsignedInt to SignedInt

conversion:

`exp`

safe_cast_bounds for warning:

`exp <= 2^255 - 1`

NumberLiteral to SignedInt

conversion:

`exp`

safe_cast_bounds for warning:

`exp <= 2^255 - 1`

**To**`mathint`

**Syntax:**`to_mathint(exp)`

**Rules:**UnsignedInt to

`mathint`

conversion:

`exp`

safe_cast_bounds:

`None`

SignedInt to

`mathint`

conversion:

`exp <= 2^255 - 1 ? exp : exp - 2^256`

safe_cast_bounds:

`None`

NumberLiteral to

`mathint`

conversion:

`exp`

safe_cast_bounds:

`None`

When an overflow occurs (i.e. when the inner expression is out of safe cast bounds for a cast operator), a warning is displayed in the call trace:

**Important Note**: This warning is displayed *only* when

The rule does not pass and a counterexample is generated &&

The tool is able to statically determine the value of the inner expression (e.g.

`m3`

above) &&The inner expression value is out of bounds for a safe cast

Thus, a rule such as

```
mathint x1 = -3;
uint256 x2 = uint256(x1);
assert x2 > 0;
```

is **not** going to display the warning because the *rule passes (as per the conversion above* `x2`

is `-3 mod 2^256`

which is **positive***)* and no counterexample is generated.