# Uninterpreted Sorts

CVL specifications support both Solidity primitives (`uint256`

, `address`

, etc.) and custom types (e.g., `mathint`

). Solidity types are *interpreted*, meaning they have specific semantics, such as arithmetic or comparison operations. However, in some cases, it is beneficial to use *uninterpreted sorts*, which do not carry the semantics associated with interpretation.

## Syntax for Uninterpreted Sorts

To declare an uninterpreted sort in CVL, use the following syntax:

```
sort MyUninterpSort;
sort Foo;
```

These uninterpreted sorts can be utilized in various ways within a CVL specification:

**Declare Variables:**Foo x;

**Test Equality:**Foo x; Foo y; assert x == y;

**Use in Signatures:**ghost myGhost(uint256, Foo) returns Foo;

## Example Usage

Consider the following example:

```
sort Foo;
ghost bar(Foo, Foo) returns Foo;
rule myRule {
Foo x;
Foo y;
Foo z = bar(x, y);
assert x == y && y == z;
}
```

This example demonstrates the use of an uninterpreted sort `Foo`

. The `bar`

ghost function takes two arguments of type `Foo`

and returns a value of the same type. The `myRule`

rule declares variables `x`

, `y`

, and `z`

, and asserts that they are all equal.

## Using Uninterpreted Sorts with Ghosts

Uninterpreted sorts can also be employed in ghosts, as shown in the following example:

```
ghost mapping(uint256 => Node) toNode;
ghost mapping(Node => mapping(Node => bool)) reach {
// Axioms for reachability relation
axiom forall Node X. reach[X][X];
axiom forall Node X. forall Node Y.
reach[X][Y] && reach[Y][X] => X == Y;
axiom forall Node X. forall Node Y. forall Node Z.
reach[X][Y] && reach[Y][Z] => reach[X][Z];
axiom forall Node X. forall Node Y. forall Node Z.
reach[X][Y] && reach[X][Z] => (reach[Y][Z] || reach[Z][Y]);
}
definition isSucc(Node a, Node b) returns bool =
// Definition for successor relationship
reach[a][b] && a != b &&
(forall Node X. reach[a][X] && reach[X][b] => (a == X || b == X));
rule checkGetSucc {
uint256 key;
uint256 afterKey = getSucc(key);
assert reach[toNode[key]][toNode[afterKey]];
}
```

This example demonstrates the use of uninterpreted sorts (`Node`

) in ghost mappings and functions, emphasizing their application in specifying relationships and properties without being bound by specific interpretations.

In summary, uninterpreted sorts in CVL provide a versatile tool for declaring abstract types and relationships, allowing for greater expressiveness in specification design.