jeannin/zelus

A synchronous language with ODEs

Zelus: A Synchronous Language with ODEs

Zélus is a synchronous language extended with Ordinary Differential Equations (ODEs) to program hybrid systems that mix discrete-time and continuous-time models. An example is a (discrete-time) model of a control software paired with a (continuous-time) model of the plant. The language shares the basic principles of the synchronous languages Lustre with modularity features from Lucid Synchrone (type inference, hierarchical automata, and higher-order functions). It is conservatively extended to write continuous-time models expressed by ODEs and zero-crossing events. The compiler is written in OCaml and is structured as a series of source-to-source and traceable transformations that ultimately yield statically scheduled sequential code. Continuous-time models are simulated using an off-the-shelf numerical solver (here Sundials CVODE and, for the moment, the two built-in solvers ode23 and ode45).

Getting Started

The easiest way to install Zelus is via Opam, the OCaml package manager.

opam install zelus

You can then test your installation with:

zeluc -version

The manual, examples, and research papers can be found at http://zelus.di.ens.fr

Optional Dependencies

By default Zelus relies on the built-in solvers. To switch to Sundials CVODE you need to install sundialsml (which requires sundials). Some examples also depend on the zelus gtk library (which requires gtk2.0)

opam install sundialsml zelus-gtk

Docker

We also provide a dockerfile to setup an environment with all the dependencies. Build the image with (you might need to increase available memory in docker preferences):

make docker-build

Run with:

make docker-run

A Simple Example

Consider the example of a bouncing ball. The zelus code is the following:

let loose = 0.8
let     g = 9.81
let    x0 = 0.0 
let    y0 = 10.0
let   x'0 = 1.0
let   y'0 = 0.0

let hybrid main () = () where
  rec der x  =  x' init x0
  and der y  =  y' init y0
  and der x' = 0.0 init x'0
  and der y' = -.g init y'0 reset up(-.y) -> -.loose *. last y'
  and present up(-.y) -> local cpt in
    do  cpt = 0 fby cpt + 1
    and  () = print_endline (string_of_int cpt) done

The dynamics of the ball is expressed with four ODEs defining the position (x, y) and the speed (x', y') of the ball given an initial position (x0, y0) and an initial speed (x'0, y'0). Whenever the ball hits the ground up(-. y) the discrete time code of the body of the present construct is executed (here incrementing a simple counter).

Compilation

The zeluc compiler takes a zelus file (e.g., bouncing.zls) and compile it to OCaml code (e.g., bouncing.ml).

zeluc bouncing.zls

You can also specify a simulation node. The compiler then generates an additional file containing the simulation code (e.g., main.ml).

zeluc -s main bouncing.zls

To build an executable, the last thing to do is to compile the OCaml code using the zelus library.

ocamlfind ocamlc -linkpkg -package zelus bouncing.ml main.ml -o bouncing

Other Examples

This repository includes runnable examples demonstrating different aspects of the language. The source code for several of the examples can be found in the examples directory. To build most of the examples:

cd examples && make

The executables can be found in each example directory (e.g., horloge/horloge_main.exe).

Development

Compiler

We use dune to build the compiler, the libraries, and the examples. To build the project:

./configure
dune build

This produces two executables (and some tools in ./tools):

• compiler/zeluc.exe: native code
• compiler/zeluc.bc: byte code (can be used with ocamldebug)

Libraries are split in two packages:

• zelus: the standard libraries
• zelus-gtk: additional libraries that depend on lablgtk (only built if lablgtk is installed)

The build automatically detects if sundialsml is installed and updates the librairies accordingly.

Test

To run all the tests:

cd test
make

Tests are split into 3 categories: good, bad, and run. To launch a single subset (e.g., good):

cd good
make

To clean generated files:

make clean

Citing Zelus

@inproceedings{Zelus2013HSCC,
  author = {Timothy Bourke and Marc Pouzet},
  title = {Zélus: A Synchronous Language with {ODEs}},
  booktitle = {16th International Conference on Hybrid Systems: Computation and Control (HSCC'13)},
  pages = {113--118},
  month = mar,
  year = 2013,
}

zelus's Issues

Implement function declaration typing rule for new syntax

let add (x : {v : float | v < 0 }) (y : {v : float | v < 0 }) : { v : float | v >= 0} = x * x + y*y

For the function declaration typing rule, we need to:
1- Loop through all inputs and use vc_gen_substitute to get the truth conditions "x < 0" and "y < 0".
2- Apply vc_gen_substitue for the function return type to get "add >= 0"
3 - Process the function body to get " add = x * x + y * y"
4 - Create the verification conditions "not ((x < 0 and y < 0 and add = xx + yy ) -> (add >= 0))"
5 - Use z3_solve on verification condition to prove property

Refinement type predicate does not support functions and operators

Issue description:

let pi = 3.14159
let y0 : int{ -y0 >= pi} = 4.0

Will compile successfully because (-y0) is interpreted as "42". The dummy value we use when there is no handling.

Action:
Implement operator and function application checks inside refinement variable declaration.

Error in translation custom refinement type to .ml

When translating refinement_variable_test.zls to refinement_variable_test.ml, the custom refinement type type nat = {v : int | v >= 0} gets translated to be type nat = , which causes error.

create_z3_var_typed shall be used throughout the code

Past prototyping used create_z3_var when the type was unknown and this caused many variables to be assumed "float" type. This is the source of many z3(type error) exceptions.

We should replace all the occurrences of create_z3_var with create_z3_var_typed or any other function that will give the correct type to a z3 variable.

For an example, see the create_base_var_from_pattern function that uses pattern matching in a Zelus pattern construct to figure out base type and variable name.

Implement pair typing rules for new syntax

Also investigate how to write refinement types for each element

• using fst, snd keywords
• using name types, i.e let (x : {v : int | v > 100}, y : nat)

Nested function bug: function output not added to environment

let add (x : {v:float|v>0} ) (y : {v:float|v>0} ) : { v:float | v >= x && v >= y} = let z = x +. y in z
let f6 (x : {v : float | v < 0 }) : {v : float | v > 0} = let y = x *. x in add 1. y

After proof, the add constraint is only added to add's local environment and cannot be used in the proof for f6

mCheck.ml

Compiler refactoring task

mCheck.ml is a new file that will traverse through the MARVeLus AST and solve for the verification conditions.

The problem definition is described below:

• Given a MARVeLus AST, traverse the tree and check the verification conditions, return true if all conditions are met, and false otherwise.

AST ----mCheck.ml----> bool

• Side effects: print to the terminal when intermediate checks fail, and add checked conditions to the environment

function templates for vc_check:

let vc_check_[structure name] ctx env typenv funenv [structure object]: bool =
(*
comment defining function interface (inputs + outputs)
comment defining function computation
follow ocamldocs guidelines: https://v2.ocaml.org/manual/ocamldoc.html#s%3Aocamldoc-comments
*)
body pattern matching
| ->
...

Magic number 42.0 in verification condition

The acc.zls file generates the following lines in the output of compilation:

[DEBUG] : return definition: (= vxf |42.0|)
[DEBUG] : exception ignored: AstTranslationNotImplemented vc_gen_expression: Etuple
[DEBUG] : Eseq : (e1 = |42.0| e2 = |42.0|)

[DEBUG] : Body exp :|42.0|

Where 42.0 is an undesired magic number in the code. This problem can cause issues in the verification conditions, since it adds an additional unrealistic constraint. Issue needs more investigation.

Implement type aliasing for new syntax

Examples without functions work. For example,
type nat = {x : int | x >= 0} let x : nat = 10

Examples with functions are not working due to some clash with Zelus' typing system. Example that doesn't work:
type nat = {x : int | x >= 0} let node main () = let (x : nat) = 1 in x
Error output: "Type error: this expression has type int, but is expected to have type nat.

Make free variables in refinement type expressions

Change refinement type expressions from let x:int{x>0}=1 to let x:{int z | z>0} = 1

[Summer] Optimize the data structure for storing refinement/non-refinement variable declaration

| Erefinementdecl of name * name * exp * exp * is_static
| Econstdecl of name * is_static * exp

For now, we store non-refinement variable declaration like let var : type = exp as trivially true refinement variable in Erefinementdecl, but for declaration without type annotation (like let var = exp), we are still storing it in Econstdecl.

We hope to finally use a pattern called Econstdecl (which has the same name as the original one but with some modifications on inner data structure) to store all variable declarations

[Summer] Enable custom refinement data type definition

The current implementation does not support custom refinement types to be declared beforehand / have an alias to identify that custom data type.

1- Adding the pattern below to the Zelus parser
type type_name = { reference_variable : base_type | Phi(reference_variable ) }
i.e type nat = {v : int | v > = 0}, which defines all natural numbers

[Easier task] - Add the custom data type definition to the parser

Implement if statement typing rule for MARVeLus

let x_abs x : {v : float | v >= 0} = if x < 0 then -x else x

For this example we want to check both options of the if statement and prove that either branch makes the return condition of the function true

VC: "not ( ((x < 0) -> (-x >= 0)) and ( not (x < 0) -> (x >= 0)) )"

[Summer] Call Z3 substitution function when verifying the new-syntax refinement type

Since we have parsed the new syntax and carried it to the verifying stage, we should call Z3 substitution function in the correct place to replace the alias variable with the real variable

Migrate to Zélus 2.2

Looks like we need to fetch everything up to inria/zelus:2.2, which is up to commit 56febdf

[Summer] Parse new syntax for declaring refinement variables

Old syntax of declaring refinement variables:
let x : int{x > 0} = 1
New syntax should be:
let x : {v : int | v>0} = 1

Instead of using the variable name directly in the refinement expression, we use an alias (e.g. v here) to refer to it.
So the parsing stage should carry additional information: the name of alias, to the verifying stage (in z3refinement.ml)

Implement function input check typing rule for new syntax

let add (x : {v : float | v < 0 }) (y : {v : float | v < 0 }) : { v : float | v >= 0} = x * x + y*y

Once the function is called, for example,
let s = add 1 (-.3)

We want to verify that "not ( (x = 1 and y = -3) -> (x < 0 and y < 0))"

In this example, the check should fail since 1 !< 0.

Combinatorial expression expected to be static

let add (x : {v:float|v>0} ) (y : {v:float|v>0} ) : { v:float | v >= x && v >= y} = let z = x +. y in z

let f6 (x : {v : float | v < 0 }) : {v : float | v > 0} = let y = x *. x in add y y

The previous code does not type checks, with the following error:

File "refinement_function_test.zls", line 59, characters 5-6:
add y y
^
Type error: this is a combinatorial expression and is expected to be static.

It seems that the first y argument is causing trouble because the following passes the type check
let f6 (x : {v : float | v < 0 }) : {v : float | v > 0} = let y = x *. x in add 1. y

Implicit type conversion bug [Lack of type inference]

The following expression does not pass the compiler check
let add (x : {v:int |v>0} ) (y : {v:int|v>0} ) : { v:int | v >= x && v >= y} = let z = x + y in z

However, if int is replaced with a float it works:

let add (x : {v:float|v>0} ) (y : {v:float|v>0} ) : { v:float | v >= x && v >= y} = let z = x +. y in z

The issue is that MARVeLus has no type inference mechanism to determine the type of z, which then default to float. When assigning "z = x + y" in Z3, it implicitly creates a new float x and a new float y, which then breaks the system.

mDefs.ml

Compiler refactoring task

mDefs.ml is a new file that will store data structures definition, including custom types, environment, function environment, type environment.

This task consists of moving those definitions from z3refinement.ml to mDefs.ml. Make sure that the z3refinement.ml code still runs properly after the changes.

Refinement function check fails for nested functions

Issue description:

let add ( x : int{x > 0} ) ( y : int{y > 0} ) : int{ add_return >= x && add_return >= y} = x + y
let f2 ( x : int{x < 0} ) : int{ f2_return > 0} = add (x * x) (x * x)

fails with the following message: this is a combinatorial expression and is expected to be static

Action:

Understand why is it failing and fix the issue.

mUtils.ml

Compiler refactoring task

mUtils.ml is a new file that will store the implementation for MARVeLus utility functions, such as printing data structures and the debug print interface.

This task consists of moving those definitions from z3refinement.ml to mUtils.ml. Make sure that the z3refinement.ml code still runs properly after the changes.

[Summer] Parse new syntax for defining refinement type in function

Old syntax of defining refinement type in function:
let add (x : int{x > 0}) (y : int{y > 0}) : int{add_return > 0} = x+y
New syntax should be:
let add (x : {v : int | v > 0}) (y : {v : int | v > 0}) : {v : int | v > 0} = x+y

Instead of using the variable name directly in the refinement expression, we use an alias (e.g. v here) to refer to it.
So the parsing stage should carry additional information: the name of alias, to the verifying stage (in z3refinement.ml)

[Summer] Optimize the data structure for storing refinement/non-refinement function

| Efundecl of name * funexp
| Erefinementfundecl of name * funexp * exp

For now we store both refinement and non-refinement function in Erefinementfundecl which has one more field than Efundecl.

We hope to finally utilize a pattern called Efundecl (which is the original name for function pattern) to hold all functions with as little modification as possible than the original data structure.

Add the ability to declare refinement types anywhere variables can be declared

`let rec` makes variables 42 if expression doesn't contain a `fby`

This example raises an error as expected:

let node sim () =
    let rec (x:{v:float | v > 0.}) = (-5.) fby (-5.) in x

This example does not:

let node sim () =
    let rec (x:{v:float | v > 0.}) = (-5.) in x

Instead, a constraint is added that sets x to 42., which is positive and thus passes the check.

Add type constraints to variable declarations in all contexts

Use the type constraint/type expression pattern (from functions) anywhere other variables can be declared

Implement fby typing rule for MARVeLus

[Summer] Write Z3 substitution function for custom data types

The custom refinement data types uses an alias to reference the type variable itself.
e.g:
type nat = {v : int | v > = 0} , in this example v is the alias used for the type variable.

This task aims to implement the vc_gen_substitute function that will take a inputs a variable and perform a Z3 substitution.

e.g:
type nat = {v : int | v > = 0} let y : nat = 4
vc_gen_substitute(y) would looks for v >= 0 in nat definition and replace v with the variable y by using the Z3 Ocaml API.

The verification condition for the above example would be:
y = 4 -> y >= 0

Reference:

Look for substitute function in https://z3prover.github.io/api/html/ml/Z3.Expr.html

[Summer] Add keyword for temporal operators box and diamond

Goal: Add a keyword for temporal logic operators (box, diamond) that will take an expression as input, them translate it to Z3 expression.

The refinement types branch has currently no support for such keywords. This could be implemented by adding new keywords "box" and "diamond" that will take one expression as input. The compiler will translate the input into a Z3 expression and apply the logical steps required by the operator.

An example of such refinement type annotation is written below:

let rec (a, b) = body : btype {box(expression)} in output

Multi-step task
[Easier task] - Add new keywords 'box' and 'diamond' to the parser
[Harder task] - Implement Z3 translation of temporal logic operators

mVcGen.ml

Compiler refactoring task

mVcGen.ml is a new file that will store the implementation for verification condition generation.

This task consists o implementing an interface that translates from Zelus AST to MARVeLus AST. The problem definition is described below:

• Given a Zelus AST, build a new AST containing Z3 objects, inferred statements, and verification conditions to check.

AST ----mVcGen.ml----> AST

Where:
Zelus {
Zelus data structures
}

MARVeLus {
Zelus data structures
Premises
Verification condition
}

function templates for vc_gen:

let vc_gen_[structure name] ctx env typenv funenv [structure object]: MARVeLus =
(*
comment defining function interface (inputs + outputs)
comment defining function computation
follow ocamldocs guidelines: https://v2.ocaml.org/manual/ocamldoc.html#s%3Aocamldoc-comments
*)
body pattern matching
| ->
...

Attach task board to Zelus

renaming this to see if it goes back to task board

[Summer] Create a custom data type data structure and environment

The current implementation does not have an environment to hold custom data types defined in MARVLus.

Goal: Create a custom data type environment to hold the custom data type

The environment will be a map [string, custom type data structure], where "string" will be the custom data type alias, and the custom data type structure will be defined as below,

custom_t {
string base_type;
string reference_variable;
z3_expression Phi(reference_variable);
}

[Harder task] - Create a custom data type data structure and an environment to hold these data structures

Function application failing at 'prove_function'

Unhandled cases on 'prove_function' make it return '42', which was a magic number used to track errors. Make sure to replace this with exceptions that throw meaningful messages.

What happens when a refinement type uses a variable of the same name?

e.g.

let x = -1 in let x:int{x<0} = 2 in x

Which x is int{x<0} referring to?

[Summer] Extend normal types to be trivially true refinement types

The goal for this task is to extend base variables and base functions to be refinement variables and refinement functions where the refinement types expression is exp = True

[Summer] Add refinement type support for equations

The let rec keyword is parsed to a list of equation expressions. However, the equation handler equation_desc on zparser.mly has no support for refinement types and the following example does not compile:

let rec (a, b) : btype {box(expression)} = body in output

For reference, take a look at the simple_type and type_expression implementation for refinement types on zparser.mly. We need to add a similar pattern match construct for equations.

[Easier task] - Add a pattern match for refinement types on the parse equation handler. This will enable refinement type annotation for let rec expressions.

Create a unit test file with variables and function declarations

Test file to run after compiler changes and verify all steps are working

Make refinement types to be defined everywhere basic types are defined

Currently, the refinement type implementation is hardcoded for variables and functions. The goal is to be able to add the refinement type annotation everywhere a basic type can be defined.

Compilation of Model and Robot Code

Formally verifying a robot program often requires a model of the hardware and its connections to its environment. However, such models are no longer necessary when compiling code for execution on real hardware. We therefore need a way to distinguish places in code that are modeled for verification purposes, but will receive real data from physical sensors when executing on actual hardware.

To minimize impact on the other compiler components, the proposed solution is as follows:

• Introduce a new construct, modeled(x, y) where x is the model of a sensor and y is the actual implementation. For instance, x could be the kinematic model of a robot that simulates the position of an actuator, while y is the driver code necessary for obtaining the actual value from the robot's sensors.
• To the verifier, modeled(x, y) is equivalent to x (y is ignored)
• When in --robot mode, modeled(x, y) gets compiled to y in the executable.

[Summer] Treat base variables as trivially true refinement variables

Currently, MARVLus handles refinement and base variables differently. Base variables are simply added to the environment while typing rules are applied to refinement variables to verify their satisfiability.

This process can be generalized by treating base variables as trivially true refinement variables.

An implementation idea is to create a function a vc_gen_refinement_variable function that:

• has inputs variable_name, base_type, refinement_expression and rhs_expression
• applies the typing rule for refinement variables (current MARVLus implementation)

For base variables a "True" expression is passed as the refinement_expression variable

Non-refinement variables cause MARVeLus to break

(* let x0 : int = 3 *)

This does not compile correctly, code create a Z3 null type and cannot be used.

[Summer] Treat base functions as trivially true output type refinement functions

Similar to the refinement and base variables issue described in #22 , MARVLus handles refinement and base functions differently. There is no special handling for base functions while typing rules are applied to refinement functions to verify their satisfiability at declaration and at use.

This process can be generalized by treating base functions as having a trivially true refinement output type.

An implementation idea is to create a function a vc_gen_refinement_fun function that:

• has inputs function_name, kind, is_atomic, argument_list, function_body, function_location and return_refinement_type
• applies the typing rule for refinement functions (current MARVLus implementation)

For base functions, a "True" expression is passed as the return_refinement_type input variable

Implement rec typing rule for MARVeLus

Add scoping to Z3 environment