Compilation to Rust

Disclaimer: While this feature has been tested on rather large systems, is still considered experimental. The Kind 2 team welcomes feedback / bug reports.

Rust is a very efficient language with a focus on safety. Kind 2 can compile Lustre to Rust, as long as the input system does not have any unguarded pre’s, regardless of whether the initial undefined value is actually used. Arrays and records are currently not supported.

Compilation is activated by the --compile true flag.

The result is a Rust project in the implem subdirectory of the Kind 2 output directory. The project is extensively documented, you can read the documentation by running cargo doc in the project directory and opening target/doc/<system>/index.html.

Technical details

The project produces a binary that reads inputs as comma-separated values from its standard input and prints back outputs as comma-separated values on its standard output. Lustre’s reals are compiled as 64-bits floats while ints become usize: 32-bits (64-bits) signed integers on 32-bits (64-bits) platforms.

Note:* Technically, this conversion is unsound because the semantics of int is mathematical (aka, infinite precision) integers, not machine integers, and that of real is mathematical real numbers, not floating point numbers.

Assertions, properties and contracts

Compilation in Kind 2 works under the assumption that the model has been proved correct. Therefore properties, guarantees, and modes are not compiled as they have already been proved at model-level.

To be precise, since Kind 2 works with mathematical integers and reals, it can be the case that the binary actually falsifies the specification for generating a floating point overflow, underflow, and NaN or for using integer arithmetic modulo n. We are considering offering to compile properties / guarantees / modes optionally through a flag.

Assertions and assumptions from the original models are compiled as internal checks and, when falsified, will cause the binary to stop after outputting an error message pointing to the assertion / assumption falsified in the original Lustre model.