EMSOFT 2023: Equation-Directed Axiomatization of Lustre Semantics to Enable Optimized Code Validation

Equation-Directed Axiomatization of Lustre Semantics to Enable Optimized Code Validation

EMSOFT September 18 2023

Lelio Brun • Christophe Garion • Pierre-Loïc Garoche • Xavier Thirioux

Embedded Systems

Model-Based Design: SCADE

Here is an example of what engineers are provided with when working with SCADE, a state-of-the-art Model-Based Design tool used to build critical applications, such as airplane controls, automated train systems, or power plant monitoring software. This is a typical block diagram graphical interface where blocks represent sub-components that interact over discrete time with each other through lines representing signals. Behind the graphical interface is an actual programming language inspired by the academic language Lustre. In the semantics of Lustre, each signal is an infinite stream of values, and each component is a function of streams. The techniques to compile Lustre programs to imperative programs for execution on embedded platforms have been thoroughly studied since the end of the 80s.

Lustre and Certified Compilation

Industrial Qualification

SCADE Suite
KCG Code Generator

DO-178C

Verified Compilation

Translation Validation

LustreC

A significant challenge with the compilation of Lustre, in the context of critical applications, is correctness. That is, we want strong guarantees on the correctness of the generated code relative to the specification model. Let's discuss three approaches: 1. Industrial qualification ensures that the development process of the tools complies with industrial norms. The newest norms mention Formal Methods, but it is not yet a standard. SCADE and its code generator KCG, are qualified according to several norms, including the very strict aerospace norm DO-178C. 2. Verified compilation is an approach where the compiler itself is formally proved correct, that is, a proof of the preservation of the semantics between the input Lustre programs and the output compiled programs is given once and for all. This is the Vélus project's approach, which builds on the verified C compiler CompCert to give a mechanized end-to-end correctness proof in the Coq theorem prover of the compilation of Lustre to Assembly. You will learn more about that project in the next talk! 3. Finally, Translation Validation is the approach we choose in this work. With this technique, instead of proving the whole compiler, the correctness of the generated code is verified at each compiler run. To achieve this, we extended LustreC, an academic featureful Lustre compiler, to generate both C code and an attached C specification in ACSL, the specification language of the FramaC platform. The specification encodes the semantics preservation result, and its verification is delegated to automatic SMT solvers. * Industrial qualification is very expensive, does not provide formal proof, and usually has a restricted scope. * Verified compilation might appear as the holy grail, but it requires a lot of effort and is hard to extend: each new feature or optimization will be arbitrarily difficult to prove correct. * Translation Validation is less systematic but more versatile: it is easier to deploy on existing projects, can be applied to different compilation schemes, enables optimizations, and is not necessarily tied to a unique prover.

Example

							
node count() returns (out: bool)
var time, ptime: int;
    init, b: bool;
let
  init = true -> false;
  b = (ptime = 3);
  time = if init then 0
         else if b then 0
         else ptime + 1;
  ptime = pre time;
  out = (time = 2);
tel

							
node count() returns (out: bool)
var time, ptime: int;
    init, b: bool;
let
  out = (time = 2);
  b = (ptime = 3);
  ptime = pre time;
  time = if init then 0
         else if b then 0
         else ptime + 1;
  init = true -> false;
tel

							
node count() returns (out: bool)
var time, ptime: int;
    init, b: bool;
let
  init = true -> false;
  b = (ptime = 3);
  time = if init then 0
         else if b then 0
         else ptime + 1;
  ptime = pre time;
  out = (time = 2);
tel

Let's see a simple example. The block diagram on the left and the code on the right describe the same object. In Lustre, a component is called a node. The `count` node is a stream function that takes no input and returns an output stream `out` with boolean values. It consists of equations defining local and output streams whose names correspond with the signal names on the diagram. The order of the equations is irrelevant: Lustre is declarative. Each equation is implicitly valid at each instant of time. * `init` is defined with the arrow operator as the stream that is `true` at the first instant and `false` otherwise * `b` is defined using the equal operator that operates pointwise on the stream `ptime` and the constant stream `3` * `time` is defined using nested functional `if/then/else` operating as multiplexers where all the sub-expressions are computed * `ptime` represents the previous value of `time` using the `pre` operator, which implements a memory, a register * Finally, `out` is defined in a similar way as `b`


// state initialization
n_reset(&self);

// execution loop
while (1) {
  read_input(&x);

  // execution step
  n_step(x, &y, &self);

  write_output(y);
}


node count() returns (out: bool)
var time, ptime: int; init, b: bool;
let
  init = true -> false;
  b = (ptime = 3);
  time = if init then 0 else if b then 0 else ptime + 1;
  ptime = pre time;
  out = (time = 2);
tel


machine count {
  state ptime: int;
  instance a: _arrow;

  step () => (out: bool) {
    var time: int; init, b: bool;

    init := a.step(true, false);
    b := state(ptime) = 3;
    if (init) { time := 0 } else { if (b) { time := 0 } else { time := state(ptime) + 1 } }
    state(ptime) := time;
    out := (time = 2);
  }
}


machine count {
  state ptime: int;
  instance a: _arrow;

  step () => (out: bool) {
    var time: int; init, b: bool;

    init := a.step(true, false);
    b := state(ptime) = 3;
    if (init) { time := 0 } else { if (b) { time := 0 } else { time := state(ptime) + 1 } }
    state(ptime) := time;
    out := (time = 2);
  }
}


struct count_mem { _Bool _reset; int ptime; struct _arrow_mem *a; };

#define count_set_reset(self) { self->_reset = 1; }
void count_clear_reset(struct count_mem *self ) {
  if (self->_reset) {
    self->_reset = 0;
    _arrow_reset(self->a);
  }
}

void count_step(_Bool *out, struct count_mem *self) {
  int time; _Bool init, b;
  count_clear_reset(self);
  init = _arrow_step(self->a);
  b = self->ptime == 3;
  if (init) { time = 0; } else { if (b) { time = 0; } else { time = self->ptime + 1; } }
  self->ptime = time;
  *out = time == 2;
}


node count() returns (out: bool)
var time, ptime: int;
    init, b: bool;
let
  init = true -> false;
  b = (ptime = 3);
  time = if init then 0
         else if b then 0
         else ptime + 1;
  ptime = pre time;
  out = (time = 2);
tel

\[ \newcommand\paren[1]{\left(#1\right)} \newcommand\trname[2]{\mathop{#2\_\mathit{tr}_{#1}}} \newcommand\tr[5]{\trname{#1}{#2}\!\paren{#3,#4,#5}} \newcommand\treel[2]{#1\!\paren{#2}} \newcommand\treen[2]{#1\!\left[#2\right]} \begin{split} & \tr{} {count} S {out} {S'} \triangleq \\ & \quad \tr{5} {count} S {out} {S'} \\ & \quad\quad\begin{aligned} & \phantom{\wedge \exists b,\, init,}\\ & \quad\quad\begin{aligned} & \phantom{\wedge \tr{} {arrow} {\treen S a} {init} {\treen {S'} a}} \\ & \phantom{\wedge b = \left(\treel S {ptime} = 3\right)} \\ & \phantom{\wedge init \implies {time = 0}} \\ & \phantom{\wedge (\neg {init} \wedge b) \implies {time = 0}} \\ & \phantom{\wedge (\neg {init} \wedge \neg b) \implies time = \treel S {ptime} + 1} \\ \end{aligned} \\ & \phantom{\wedge \treel {S'} {ptime} = time}\\ & \phantom{\wedge out = \left(time = 2\right)} \\ \end{aligned} \end{split} \]


node count() returns (out: bool)
var time, ptime: int;
    init, b: bool;
let
  init = true -> false;
  b = (ptime = 3);
  time = if init then 0
         else if b then 0
         else ptime + 1;
  ptime = pre time;
  out = (time = 2);
tel

\[ \newcommand\paren[1]{\left(#1\right)} \newcommand\trname[2]{\mathop{#2\_\mathit{tr}_{#1}}} \newcommand\tr[5]{\trname{#1}{#2}\!\paren{#3,#4,#5}} \newcommand\treel[2]{#1\!\paren{#2}} \newcommand\treen[2]{#1\!\left[#2\right]} \begin{split} & \tr{} {count} S {out} {S'} \triangleq \\ & \quad \exists time,\\ & \quad\quad\begin{aligned} & \phantom{\wedge} \tr{4} {count} S {time} {S'}\\ & \quad\quad\begin{aligned} & \phantom{\wedge \tr{} {arrow} {\treen S a} {init} {\treen {S'} a}} \\ & \phantom{\wedge b = \left(\treel S {ptime} = 3\right)} \\ & \phantom{\wedge init \implies {time = 0}} \\ & \phantom{\wedge (\neg {init} \wedge b) \implies {time = 0}} \\ & \phantom{\wedge (\neg {init} \wedge \neg b) \implies time = \treel S {ptime} + 1} \\ \end{aligned} \\ & \phantom{\wedge \treel {S'} {ptime} = time}\\ & \wedge out = \left(time = 2\right) \\ \end{aligned} \end{split} \]


node count() returns (out: bool)
var time, ptime: int;
    init, b: bool;
let
  init = true -> false;
  b = (ptime = 3);
  time = if init then 0
         else if b then 0
         else ptime + 1;
  ptime = pre time;
  out = (time = 2);
tel

\[ \newcommand\paren[1]{\left(#1\right)} \newcommand\trname[2]{\mathop{#2\_\mathit{tr}_{#1}}} \newcommand\tr[5]{\trname{#1}{#2}\!\paren{#3,#4,#5}} \newcommand\treel[2]{#1\!\paren{#2}} \newcommand\treen[2]{#1\!\left[#2\right]} \begin{split} & \tr{} {count} S {out} {S'} \triangleq \\ & \quad \exists time,\\ & \quad\quad\begin{aligned} & \phantom{\wedge}\tr{3} {count} S {time} {S'}\\ & \quad\quad\begin{aligned} & \phantom{\wedge \tr{} {arrow} {\treen S a} {init} {\treen {S'} a}} \\ & \phantom{\wedge b = \left(\treel S {ptime} = 3\right)} \\ & \phantom{\wedge init \implies {time = 0}} \\ & \phantom{\wedge (\neg {init} \wedge b) \implies {time = 0}} \\ & \phantom{\wedge (\neg {init} \wedge \neg b) \implies time = \treel S {ptime} + 1} \\ \end{aligned} \\ & \wedge \treel {S'} {ptime} = time\\ & \wedge out = \left(time = 2\right) \\ \end{aligned} \end{split} \]


node count() returns (out: bool)
var time, ptime: int;
    init, b: bool;
let
  init = true -> false;
  b = (ptime = 3);
  time = if init then 0
         else if b then 0
         else ptime + 1;
  ptime = pre time;
  out = (time = 2);
tel

\[ \newcommand\paren[1]{\left(#1\right)} \newcommand\trname[2]{\mathop{#2\_\mathit{tr}_{#1}}} \newcommand\tr[5]{\trname{#1}{#2}\!\paren{#3,#4,#5}} \newcommand\treel[2]{#1\!\paren{#2}} \newcommand\treen[2]{#1\!\left[#2\right]} \begin{split} & \tr{} {count} S {out} {S'} \triangleq \\ & \quad \exists time,\\ & \quad\quad\begin{aligned} & \phantom{\wedge}\exists b,\, init, \\ & \quad\quad\begin{aligned} & \phantom{\wedge} \tr{2} {count} S {time} {S'} \\ & \phantom{\wedge b = \left(\treel S {ptime} = 3\right)} \\ & \wedge init \implies {time = 0} \\ & \wedge (\neg {init} \wedge b) \implies {time = 0} \\ & \wedge (\neg {init} \wedge \neg b) \implies time = \treel S {ptime} + 1 \\ \end{aligned} \\ & \wedge \treel {S'} {ptime} = time\\ & \wedge out = \left(time = 2\right) \\ \end{aligned} \end{split} \]


node count() returns (out: bool)
var time, ptime: int;
    init, b: bool;
let
  init = true -> false;
  b = (ptime = 3);
  time = if init then 0
         else if b then 0
         else ptime + 1;
  ptime = pre time;
  out = (time = 2);
tel

\[ \newcommand\paren[1]{\left(#1\right)} \newcommand\trname[2]{\mathop{#2\_\mathit{tr}_{#1}}} \newcommand\tr[5]{\trname{#1}{#2}\!\paren{#3,#4,#5}} \newcommand\treel[2]{#1\!\paren{#2}} \newcommand\treen[2]{#1\!\left[#2\right]} \begin{split} & \tr{} {count} S {out} {S'} \triangleq \\ & \quad \exists time,\\ & \quad\quad\begin{aligned} & \phantom{\wedge}\exists b,\, init, \\ & \quad\quad\begin{aligned} & \phantom{\wedge} \tr{1} {count} S {time} {S'} \\ & \wedge b = \left(\treel S {ptime} = 3\right) \\ & \wedge init \implies {time = 0} \\ & \wedge (\neg {init} \wedge b) \implies {time = 0} \\ & \wedge (\neg {init} \wedge \neg b) \implies time = \treel S {ptime} + 1 \\ \end{aligned} \\ & \wedge \treel {S'} {ptime} = time\\ & \wedge out = \left(time = 2\right) \\ \end{aligned} \end{split} \]


node count() returns (out: bool)
var time, ptime: int;
    init, b: bool;
let
  init = true -> false;
  b = (ptime = 3);
  time = if init then 0
         else if b then 0
         else ptime + 1;
  ptime = pre time;
  out = (time = 2);
tel

\[ \newcommand\paren[1]{\left(#1\right)} \newcommand\trname[2]{\mathop{#2\_\mathit{tr}_{#1}}} \newcommand\tr[5]{\trname{#1}{#2}\!\paren{#3,#4,#5}} \newcommand\treel[2]{#1\!\paren{#2}} \newcommand\treen[2]{#1\!\left[#2\right]} \begin{split} & \tr{} {count} S {out} {S'} \triangleq \\ & \quad \exists time,\\ & \quad\quad\begin{aligned} & \phantom{\wedge} \exists b,\, init,\\ & \quad\quad\begin{aligned} & \phantom{\wedge} \tr{} {arrow} {\treen S a} {init} {\treen {S'} a} \\ & \wedge b = \left(\treel S {ptime} = 3\right) \\ & \wedge init \implies {time = 0} \\ & \wedge (\neg {init} \wedge b) \implies {time = 0} \\ & \wedge (\neg {init} \wedge \neg b) \implies time = \treel S {ptime} + 1 \\ \end{aligned} \\ & \wedge \treel {S'} {ptime} = time\\ & \wedge out = \left(time = 2\right) \\ \end{aligned} \end{split} \]


node count() returns (out: bool)
var time, ptime: int;
    init, b: bool;
let
  init = true -> false;
  b = (ptime = 3);
  time = if init then 0
         else if b then 0
         else ptime + 1;
  ptime = pre time;
  out = (time = 2);
tel

\[ \newcommand\paren[1]{\left(#1\right)} \newcommand\trname[2]{\mathop{#2\_\mathit{tr}_{#1}}} \newcommand\tr[5]{\trname{#1}{#2}\!\paren{#3,#4,#5}} \newcommand\treel[2]{#1\!\paren{#2}} \newcommand\treen[2]{#1\!\left[#2\right]} \begin{split} & \tr{} {count} S {out} {S'} \triangleq \\ & \quad \exists time,\\ & \quad\quad\begin{aligned} & \phantom{\wedge} \exists b,\, init,\\ & \quad\quad\begin{aligned} & \phantom{\wedge} \tr{} {arrow} {\treen S a} {init} {\treen {S'} a} \\ & \wedge b = \left(\treel S {ptime} = 3\right) \\ & \wedge init \implies {time = 0} \\ & \wedge (\neg {init} \wedge b) \implies {time = 0} \\ & \wedge (\neg {init} \wedge \neg b) \implies time = \treel S {ptime} + 1 \\ \end{aligned} \\ & \wedge \treel {S'} {ptime} = time\\ & \wedge out = \left(time = 2\right) \\ \end{aligned} \end{split} \]


/*@ requires count_pack(*mem, self);
    ensures count_pack(*mem, self);
    ensures count_tr(\old(*mem), *out, *mem); */
void count_step(_Bool *out, struct count_mem *self)
     /*@ ghost (struct count_mem_ghost \ghost *mem) */ {
  int time; _Bool init, b;
  count_clear_reset(self);
  init = _arrow_step(self->a) /*@ ghost (&mem->a) */;
  //@ assert count_tr1(\at(*mem, Pre), b, *mem);
  b = self->ptime == 3;
  //@ assert count_tr2(\at(*mem, Pre), b, init, *mem);
  if (init) { time = 0; } else { if (b) { time = 0; } else { time = self->ptime + 1; } }
  //@ assert count_tr3(\at(*mem, Pre), time, *mem);
  self->ptime = time;
  //@ ghost mem->ptime = time;
  //@ assert count_tr4(\at(*mem, Pre), time, *mem);
  *out = time == 2;
  //@ assert count_tr5(\at(*mem, Pre), *out, *mem);
}

Now, I'll explain briefly the compilation process. From the Lustre component `n`, the compiler generates C code in the typical form of an infinite loop: first, the state of the node (holding the `pre` memories recursively) is initialized using a `reset` function, then for each cycle, the program reads inputs from the outside (current values of the streams `x`), executes one step of computation using a `step` function, and writes the outputs (current values of the streams `y`). Let's see what happens in our example. * We start after the elaboration, normalization, dataflow optimizations, and scheduling phases, as these are irrelevant to this work. * Intermediate imperative code in a language called Machine Code is generated. Each node is translated into a machine, with a state variable for each `pre` memory (here `ptime`) and a sub-instance for each node sub-call (here, we treat the arrow operator as a special internal node). A step method is generated directly from the Lustre equations. * In this example, optimizations are ineffective. I will detail them later. * From Machine code, C code is generated. This step is straightforward as the structure is the same. As usual with C, we represent the state with a structure recursively holding fields for each state variable. The `_reset` flag is used to handle node resetting, along with a pair of functions `set_reset` to set the flag and `clear_reset` to unset it and actually perform the reinitialization. The `step` function is generated directly from the Machine step method. The code for the main loop is also generated. That was the existing architecture of the compiler. Let's see how we adapted it to support Translation Validation. * The idea is to translate Lustre nodes to Machine code along with an encoding of the semantics of the nodes. We opt for a state/transition semantics, easy to describe in first-order logic. A node is described by a transition relation between a start state `S`, an end state `S'`, and its input/output values. We adopt an equation-modular encoding to enable local reasoning, as we will see later. In our example, the partial relation `count_tr5` holds iteratively at the "end" of the five equations. * That is, it asserts the equality between the value of `out` and its defining expression and the validity of the partial relation for the four previous equations. * Which asserts in turn the value of the state variable `ptime` in the end state `S'`. * `count_tr3` encodes the `if/then/else` with implications, * `count_tr2` adds the constraint defining `b` from the value of `ptime` in the start state `S`, * Finally, the first partial relation asserts the sub-transition for the arrow sub-node, constraining the corresponding start and end sub-states. * Again, here, optimizations do not change anything. * When we generate C code, we also generate a requires/ensures contract-based specification using ACSL, the specification language of FramaC. There are here two main parts. * First, a memory correspondence result asserts the correspondence between the actual C state of the component, `self`, and the abstract state representing the state `S` in the previous formula, called `mem`. ACSL does not yet completely support arbitrary datatypes such as trees, so we have to resort to another C structure, very similar to the actual one but flattened, without pointers, and marked as `ghost`. In ACSL, `ghost` constructs do not live in the actual code but only in the specification, that is, they only serve verification purposes. A `ghost` parameter is added to each `step` function, and the contract asserts that the call must preserve the correspondence. For that, stateful operations must be replicated on the abstract state, as seen in the highlighted statements. * Second, the contract ensures that the code complies with the specification. This is the correctness result: we ensure that the code of the C step function implements the transition relation, encoded in the first-order logic of ACSL. * This is where the equation-modular encoding of this relation is useful: we add assertions at each program point after each translated equation, ensuring that the corresponding partial relation is true, iteratively leading to the whole transition relation.

Verification with Frama-C

Results

~400 files	✓ 92.7%
~231 500 POs	✓ 99.9%

Optimizations

								
type en1 = enum { On, Off };
type en2 = enum { Up, Down };

node clocks (x: int) returns (y: int)
var c: en1 clock; d: en2 clock; b1, b2, b3, z: int; c1, c2: bool
let
  c1 = (x >= 0);
  d = if c1 then Up else Down;
  c2 = (x = 0) when Up(d);
  c = if c2 then Off else On;
  b2 = 2 when Off(c);
  b1 = 1 when On(c);
  z = merge c (On -> b1) (Off -> b2);
  b3 = 3 when Down(d);
  y = merge d (Up -> z) (Down -> b3);
tel

								
type en1 = enum { On, Off };
type en2 = enum { Up, Down };

node clocks (x: int) returns (y: int)
var c: en1 clock; d: en2 clock; b1, b2, b3, z: int; c1, c2: bool
let
  c1 = (x >= 0);
  d = if c1 then Up else Down;
  c2 = (x = 0) when Up(d);
  c = if c2 then Off else On;
  b2 = 2 when Off(c);
  b1 = 1 when On(c);
  z = merge c (On -> b1) (Off -> b2);
  b3 = 3 when Down(d);
  y = merge d (Up -> z) (Down -> b3);
tel

								
type en1 = enum { On, Off };
type en2 = enum { Up, Down };

node clocks (x: int) returns (y: int)
var c: en1 clock; d: en2 clock; b1, b2, b3, z: int; c1, c2: bool
let
  c1 = (x >= 0);
  d = if c1 then Up else Down;
  c2 = (x = 0) when Up(d);
  c = if c2 then Off else On;
  b2 = 2 when Off(c);
  b1 = 1 when On(c);
  z = merge c (On -> b1) (Off -> b2);
  b3 = 3 when Down(d);
  y = merge d (Up -> z) (Down -> b3);
tel

								
type en1 = enum { On, Off };
type en2 = enum { Up, Down };

node clocks (x: int) returns (y: int)
var c: en1 clock; d: en2 clock; b1, b2, b3, z: int; c1, c2: bool
let
  c1 = (x >= 0);
  d = if c1 then Up else Down;
  c2 = (x = 0) when Up(d);
  c = if c2 then Off else On;
  b2 = 2 when Off(c);
  b1 = 1 when On(c);
  z = merge c (On -> b1) (Off -> b2);
  b3 = 3 when Down(d);
  y = merge d (Up -> z) (Down -> b3);
tel

								
step (x: int) => (y: int) {
  var c: en1; d: en2; b1, b2, b3, z: int; c1, c2: bool;
  c1 := x >= 0;
  //@ clocks_tr1(x, c1)
  if (c1) { d := Up } else { d := Down }
  //@ clocks_tr2(x, d)
  case (d) { Up: c2 := x = 0 }
  //@ clocks_tr3(x, d, c2)
  case (d) { Up: if (c2) { c := Off } else { c := On } }
  //@ clocks_tr4(x, d, c)
  case (d) { Up: case (c) { Off: b2 := 2 } }
  //@ clocks_tr5(x, d, c, b2)
  case (d) { Up: case (c) { On: b1 := 1 } }
  //@ clocks_tr6(x, d, c, b1, b2)
  case (d) { Up: case (c) { On: z := b1 ; Off: z := b2 } }
  //@ clocks_tr7(x, d, z)
  case (d) { Down: b3 := 3 }
  //@ clocks_tr8(x, d, b3, z)
  case (d) { Up: y := z ; Down: y := b3 }
  //@ clocks_tr9(x, y)
}

I will now detail briefly the optimizations we perform on the Machine code and how we manage to leave the specification untouched. I will use another toy example with features I still need to present. Lustre offers clocks to implement activation conditions, that is, a way to perform computation only on certain instants. Clocks are streams of enumerated values, such as booleans or user-defined enumerations, like in the example with `en1` and `en2`. The `when` keyword is a sampling construct. For example, `c2` is undefined when `d` is not `Up`. On the other hand, the `merge` keyword is used to merge two complementary sampled streams. For example `z` has the values of `b1` when `c` is `On` and the values of `b2` when `c` is `Off`. It is a toy example. Understanding it is not required. Let's simply consider the generated Machine code and the encoded specification as partial transition relations attached to each statement.

Conditionals fusion

								
step (x: int) => (y: int) {
  var c: en1; d: en2; b1, b2, b3, z: int; c1, c2: bool;
  c1 := x >= 0;
  //@ clocks_tr1(x, c1)
  if (c1) { d := Up } else { d := Down }
  //@ clocks_tr2(x, d)
  case (d) { Up: c2 := x = 0 }
  //@ clocks_tr3(x, d, c2)
  case (d) { Up: if (c2) { c := Off } else { c := On } }
  //@ clocks_tr4(x, d, c)
  case (d) { Up: case (c) { Off: b2 := 2 } }
  //@ clocks_tr5(x, d, c, b2)
  case (d) { Up: case (c) { On: b1 := 1 } }
  //@ clocks_tr6(x, d, c, b1, b2)
  case (d) { Up: case (c) { On: z := b1 ; Off: z := b2 } }
  //@ clocks_tr7(x, d, z)
  case (d) { Down: b3 := 3 }
  //@ clocks_tr8(x, d, b3, z)
  case (d) { Up: y := z ; Down: y := b3 }
  //@ clocks_tr9(x, y)
}

								
step (x: int) => (y: int) {
  var c: en1; d: en2; b1, b2, b3, z: int; c1, c2: bool;
  c1 := x >= 0;
  //@ clocks_tr1(x, c1)
  if (c1) { d := Up } else { d := Down }
  //@ clocks_tr2(x, d)
  case (d) {
    Up:
      c2 := x = 0;
      if (c2) { c := Off } else { c := On }
      case (c) {
        On:
          b1 := 1;
          z := b1;
        Off:
          b2 := 2;
          z := b2;
      }
      y := z;
    Down:
      b3 := 3;
      y := b3;
  }
  //@ clocks_tr3(x, d, c2)
  //@ clocks_tr4(x, d, c)
  //@ clocks_tr5(x, d, c, b2)
  //@ clocks_tr6(x, d, c, b1, b2)
  //@ clocks_tr7(x, d, z)
  //@ clocks_tr8(x, d, b3, z)
  //@ clocks_tr9(x, y)
}

Variable inlining

								
step (x: int) => (y: int) {
  var c: en1; d: en2; b1, b2, b3, z: int; c1, c2: bool;
  c1 := x >= 0;
  //@ clocks_tr1(x, c1)
  if (c1) { d := Up } else { d := Down }
  //@ clocks_tr2(x, d)
  case (d) {
    Up:
      c2 := x = 0;
      if (c2) { c := Off } else { c := On }
      case (c) {
        On:
          b1 := 1;
          z := b1;
        Off:
          b2 := 2;
          z := b2;
      }
      y := z;
    Down:
      b3 := 3;
      y := b3;
  }
  //@ clocks_tr3(x, d, c2)
  //@ clocks_tr4(x, d, c)
  //@ clocks_tr5(x, d, c, b2)
  //@ clocks_tr6(x, d, c, b1, b2)
  //@ clocks_tr7(x, d, z)
  //@ clocks_tr8(x, d, b3, z)
  //@ clocks_tr9(x, y)
}

								
step (x: int) => (y: int) {
  var c: en1; d: en2; z: int; //@ ghost b1, b2, b3: int; c1, c2: bool
  //@ c1 := x >= 0
  //@ clocks_tr1(x, c1)
  if (x >= 0) { d := Up } else { d := Down }
  //@ clocks_tr2(x, d)
  case (d) {
    Up:
      //@ c2 := x = 0
      if (x = 0) { c := Off } else { c := On }
      case (c) {
        On:
          //@ b1 := 1
          z := 1;
        Off:
          //@ b2 := 2
          z := 2;
      }
      y := z;
    Down:
      //@ b3 := 3
      y := 3;
  }
  //@ clocks_tr3(x, d, c2)
  //@ clocks_tr4(x, d, c)
  //@ clocks_tr5(x, d, c, b2)
  //@ clocks_tr6(x, d, c, b1, b2)
  //@ clocks_tr7(x, d, z)
  //@ clocks_tr8(x, d, b3, z)
  //@ clocks_tr9(x, y)
}

Variable recycling

								
step (x: int) => (y: int) {
  var c: en1; d: en2; z: int; //@ ghost b1, b2, b3: int; c1, c2: bool
  //@ c1 := x >= 0
  //@ clocks_tr1(x, c1)
  if (x >= 0) { d := Up } else { d := Down }
  //@ clocks_tr2(x, d)
  case (d) {
    Up:
      //@ c2 := x = 0
      if (x = 0) { c := Off } else { c := On }
      case (c) {
        On:
          //@ b1 := 1
          z := 1;
        Off:
          //@ b2 := 2
          z := 2;
      }
      y := z;
    Down:
      //@ b3 := 3
      y := 3;
  }
  //@ clocks_tr3(x, d, c2)
  //@ clocks_tr4(x, d, c)
  //@ clocks_tr5(x, d, c, b2)
  //@ clocks_tr6(x, d, c, b1, b2)
  //@ clocks_tr7(x, d, z)
  //@ clocks_tr8(x, d, b3, z)
  //@ clocks_tr9(x, y)
}

								
step (x: int) => (y: int) {
  var c: en1; d: en2; //@ ghost b1, b2, b3, z: int; c1, c2: bool
  //@ c1 := x >= 0
  //@ clocks_tr1(x, c1)
  if (x >= 0) { d := Up } else { d := Down }
  //@ clocks_tr2(x, d)
  case (d) {
    Up:
      //@ c2 := x = 0
      if (x = 0) { c := Off } else { c := On }
      case (c) {
        On:
          //@ b1 := 1
          y := 1;
          //@ z := y
        Off:
          //@ b2 := 2
          y := 2;
          //@ z := y
      }
    Down:
      //@ b3 := 3
      y := 3;
  }
  //@ clocks_tr3(x, d, c2)
  //@ clocks_tr4(x, d, c)
  //@ clocks_tr5(x, d, c, b2)
  //@ clocks_tr6(x, d, c, b1, b2)
  //@ clocks_tr7(x, d, z)
  //@ clocks_tr8(x, d, b3, z)
  //@ clocks_tr9(x, y)
}

Enum elimination

								
step (x: int) => (y: int) {
  var c: en1; d: en2; //@ ghost b1, b2, b3, z: int; c1, c2: bool
  //@ c1 := x >= 0
  //@ clocks_tr1(x, c1)
  if (x >= 0) { d := Up } else { d := Down }
  //@ clocks_tr2(x, d)
  case (d) {
    Up:
      //@ c2 := x = 0
      if (x = 0) { c := Off } else { c := On }
      case (c) {
        On:
          //@ b1 := 1
          y := 1;
          //@ z := y
        Off:
          //@ b2 := 2
          y := 2;
          //@ z := y
      }
    Down:
      //@ b3 := 3
      y := 3;
  }
  //@ clocks_tr3(x, d, c2)
  //@ clocks_tr4(x, d, c)
  //@ clocks_tr5(x, d, c, b2)
  //@ clocks_tr6(x, d, c, b1, b2)
  //@ clocks_tr7(x, d, z)
  //@ clocks_tr8(x, d, b3, z)
  //@ clocks_tr9(x, y)
}

								
step (x: int) => (y: int) {
  //@ ghost c: en1; d: en2; b1, b2, b3, z: int; c1, c2: bool
  //@ c1 := x >= 0
  //@ clocks_tr1(x, c1)
  if (x >= 0) {
    //@ d := Up
    //@ c2 := x = 0
    if (x = 0) {
      //@ c := Off
      //@ b2 := 2
      y := 2;
      //@ z := y
    } else {
      //@ c := On
      //@ b1 := 1
      y := 1;
      //@ z := y
    }
  } else {
    //@ d := Down
    //@ b3 := 3
    y := 3;
  }
  //@ clocks_tr2(x, d)
  //@ clocks_tr3(x, d, c2)
  //@ clocks_tr4(x, d, c)
  //@ clocks_tr5(x, d, c, b2)
  //@ clocks_tr6(x, d, c, b1, b2)
  //@ clocks_tr7(x, d, z)
  //@ clocks_tr8(x, d, b3, z)
  //@ clocks_tr9(x, y)
}

Conclusion

Extension of a Lustre compiler to support Translation Validation
High automatic verification success rate
Aggressive validated optimizations

Perspectives

Functional contracts from Lustre to C
Floats
Arrays
More optimizations

In conclusion, I presented the extension of a Lustre compiler to enable Translation Validation. The verification gave promising results with a high success rate, in a push-button fashion. Moreover, we were able to support several optimizations. Remember that a backend C compiler such as GCC could perform our optimizations, but they wouldn't be trusted. The advantage here is that the specification is untouched, so if the verification of the optimized code succeeds, we have the insurance that the optimizations are validated. The development of LustreC continues. An interesting topic is functional contracts, that is, contracts formulated on Lustre nodes and verified using Lustre model-checkers. Using our framework, such contracts could be translated into ACSL contracts on the generated C code, enabling verification of high-level properties on the low-level code. Other topics include handling floating-point verification, supporting additional features such as arrays, and investigating other optimizations such as extending the variable recycling to node state.