Merge pull request #1066 from lorchrob/ref-types-doc

Refinement type user documentation

doc/usr/source/2_input/1_lustre.rst

@@ -701,44 +701,6 @@ These two calls are the same (the second one is just syntactic sugar). The
 call* is activated when the clock ``c`` is true. Notice that the restart clock
 ``r`` is also sampled by ``c`` in this call.
 
-Enumerated data types in Lustre
-^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
-
-.. code-block:: none
-
-   type my_enum = enum { A, B, C };
-   node n (x : my_enum, ...) ...
-
-Enumerated datatypes are encoded as subranges so that solvers handle arithmetic
-constraints only. This also allows to use the already present quantifier
-instantiation techniques in Kind 2.
-
-N-way merge
-^^^^^^^^^^^
-
-As in Lustre V6, merges can also be performed on a clock of a user defined
-enumerated datatype. 
-
-.. code-block:: none
-
-   merge c
-    (A -> x when A(c))
-    (B -> w + 1 when B(c));
-
-Arguments of merge have to be sampled with the correct clock. Clock expressions
-for merge can be just a clock identifier or its negation or ``A(c)`` which is a
-stream that is true whenever ``c = A``.
-
-Merging on a Boolean clock can be done with two equivalent syntaxes:
-
-.. code-block:: none
-
-   merge(c; a when c; b when not c);
-
-   merge c
-     (true -> a when c)
-     (false -> b when not c);
-
 Partially defined nodes
 -----------------------
 

doc/usr/source/2_input/4_refinement_types.rst

@@ -0,0 +1,184 @@
+.. _2_input/4_refinement_types:
+
+
+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,
+
+.. code-block::
+
+   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:
+
+.. code-block::
+
+   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,
+
+.. code-block::
+
+   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:
+
+.. code-block::
+
+   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.
+
+.. code-block::
+
+   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:
+
+.. code-block::
+
+   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:
+
+.. code-block::
+
+   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.
+
+.. code-block::
+
+   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:
+
+.. code-block::
+
+   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``:
+
+.. code-block::
+
+   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:
+
+1. Imported node contracts, including type information
+2. Implemented (normal) node contracts, including type information
+3. Implemented (normal) node environments, i.e., checking that the set of assumptions on a node's input is realizable
+4. 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.
+
+.. code-block::
+
+   const n: int | n >= 0;
+
+
+
+
+
+

doc/usr/source/2_input/5_enums.rst

@@ -0,0 +1,37 @@
+Enumeration types
+==================
+
+.. code-block:: none
+
+   type my_enum = enum { A, B, C };
+   node n (x : my_enum, ...) ...
+
+Enumerated datatypes are encoded as subranges so that solvers handle arithmetic
+constraints only. This also allows to use the already present quantifier
+instantiation techniques in Kind 2.
+
+N-way merge
+^^^^^^^^^^^
+
+As in Lustre V6, merges can also be performed on a clock of a user defined
+enumerated datatype. 
+
+.. code-block:: none
+
+   merge c
+    (A -> x when A(c))
+    (B -> w + 1 when B(c));
+
+Arguments of merge have to be sampled with the correct clock. Clock expressions
+for merge can be just a clock identifier or its negation or ``A(c)`` which is a
+stream that is true whenever ``c = A``.
+
+Merging on a Boolean clock can be done with two equivalent syntaxes:
+
+.. code-block:: none
+
+   merge(c; a when c; b when not c);
+
+   merge c
+     (true -> a when c)
+     (false -> b when not c);

doc/usr/source/index.rst

@@ -22,8 +22,10 @@ Table of Contents
     :caption: Inputs and Outputs
 
     2_input/1_lustre
-    2_input/3_machine_ints
     2_input/2_arrays
+    2_input/3_machine_ints
+    2_input/4_refinement_types
+    2_input/5_enums
     3_output/2_machine_readable
     3_output/3_exit_codes