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;