# Refinement Types¶

Kind 2 supports refinement types. A refinement type is comprised of two components:
(i) a **base type**, and
(ii) a predicate that restricts the members of the base type.

## Declarations¶

Refinement types have syntax of the form `subtype { var: base_type | P(var) }`

.

For example, `type Nat = subtype { x: int | x >= 0 }`

declares a refinement type `Nat`

over the base type `int`

,
where the values of `Nat`

are all the nonnegative integers.
When assigning a refinement type to a node input, output, or local variable, Kind 2 also
supports an alternative, more concise syntax of the form `var: base_type | P(var)`

.

For example,

```
node N(x: int | x >= 0) returns (y: int | y >= 0);
```

denotes the interface of a node `N`

which takes a stream of natural numbers `x`

as input
and returns a stream of natural numbers `y`

as output.
The above example can be equivalently expressed using the full syntax:

```
node N(x: subtype { n: int | n >= 0 }) returns (y: subtype { n: int | y >= 0});
```

The base type being refined can be *any* type, not just a primitive type.
For example,

```
type Nat = subtype { x: int | x >= 0 };
type LessThan100 = { x: Nat | x < 100 };
```

declares a refinement type `LessThan100`

whose base type `Nat`

is itself a refinement type.
Note that we can still recursively chase base types until we reach a primitive type.
In this case, `LessThan100`

’s recursively chased primitive base type is `int`

.

Additionally, refinement types can be components of more complicated types:

```
const n: int;
type Nat = subtype { x: int | x >= 0 };
type NatArray = Nat^n;
```

Above, we declare a type `NatArray`

, an array of natural numbers.

Since Lustre is a declarative language, there is no conceptual ordering between variable declarations
(input, output, and local variables). A consequence of this is that refinement type predicates can
contain variables that are defined before *or after* the current variable in the input file.
For example, the following is legal.

```
node N() returns (x: | x <= y; y | y = x + 10);
```

Above, the predicate in `x`

’s type references `y`

, which is allowed even though
`y`

comes after `x`

in the list of node outputs.

## Semantics¶

Refinement types on input variables represent assumptions, while refinement types on locals and node outputs represent proof obligations.

Consider the following example:

```
type Even = subtype { n: int | n mod 2 = 0 };
type Odd = subtype { n: int | n mod 2 = 1 };
node M(x1: Even; x2: Odd) returns (y: Odd);
let
y = x1 + x2;
--%MAIN;
tel
```

Kind2 will attempt to prove that node `M`

’s output `y`

respects type `Odd`

while assuming that input `x1`

has type `Even`

and input `x2`

has type `Odd`

.
More intuitively, Kind 2 will prove
that adding an even and an odd integer results in an odd integer.
Conceptually, the refinement types can be viewed as an augmentation of
`M`

’s contract as follows:

```
node M(x1: int; x2: int) returns (y: int);
(*@contract
assume x1 mod 2 = 0;
assume x2 mod 2 = 1;
guarantee y mod 2 = 1;
*)
let
y = x1 + x2;
--%MAIN;
tel
```

If an output variable with a refinement type is left undefined, Kind 2 will specify that the value ranges over a recursively chased base type.

```
node M() returns (y: Nat | y < 100);
let
tel
```

In the above example, `M`

’s return value `y`

will range over *all integers*,
not just natural numbers less than 100. This is because `y`

is an output variable,
and therefore its refinement type is viewed as a proof obligation.
In this case, Kind 2 will report that `y`

violates its refinement type.

## Operations¶

From the point of view of primitive operations (e.g. `+`

, `-`

, `pre`

) and node
calls, variables with refinement types can syntactically be used anywhere that variables with the
corresponding base type can be used, and vice versa.
For example, if `x`

has type `Nat`

, `y`

has type `Nat`

, and `z`

has type
`int`

, then `x+y`

, `z+x`

, and `y+z`

(among other combinations) are all legal.
Further, if node `M`

has a single parameter of type `Nat`

, then
the node call `M(z)`

is legal, and if node `N`

has a single parameter
of type `int`

, then the node call `M(x)`

is legal.

While all of the above are syntactically valid,
Kind 2 may still fail type-related proof obligations.
For example, in the node call `M(z)`

(where `z`

has type `int`

and `M`

takes a single parameter of type `Nat`

),
`M`

’s typing assumption on its input will be violated if `z`

can be negative.

## Realizability¶

Because refinement types are essentially contract augmentations, it is possible to specify
refinement types that are *unrealizable*. In other words, it is possible
to specify refinement type contraints that are unimplementable (impossible to satisfy with any implementation).

As an example, the following node interface is unrealizable:

```
node M(x: int) returns (y: int | 0 <= y and y <= x);
```

Output variable `y`

’s refinement type states that `y`

must be between `0`

and `x`

.
However, if input `x`

is negative, then no value for `y`

will satisfy its type.

One way to make the above interface realizable is to add a refinement type for `x`

:

```
node M(x: int | x >= 0) returns (y: int | 0 <= y and y <= x);
```

To check the realizability refinement types, one can call `kind2 <filename> --enable CONTRACTCK`

.
Kind 2 performs four types of realizability checks:

Imported node contracts, including type information

Implemented (normal) node contracts, including type information

Implemented (normal) node environments, i.e., checking that the set of assumptions on a node’s input is realizable

Individual refinement types, i.e., that a global refinement type declaration is realizable

## Restrictions¶

Currently, global constants with refinement types (like the following example) are not supported.

```
const n: int | n >= 0;
```