EMSOFT 2021: References to the Coq development

This page presents the artifact associated with the EMSOFT 2021 article Verified Lustre normalization with node subsampling, by T. Bourke, P. Jeanmaire, B. Pesin, and M. Pouzet. The following links relate the sections of the article to relevant definitions of the Coq development. The full Coq source code is available on github.

The online version of the compiler was extracted from Coq and compiled to Javascript with js_of_ocaml. It implements the algorithms exactly as described in the EMSOFT 2021 article.

The poster and slides are also available.

1 Introduction

The example given in the introduction can be found at examples/rer.lus.

It can be normalized using ./velus -dnlustre rer.lus. The normalized code will be written to examples/rer.n.lus.

2.1 Syntaxes

2.2 Semantics

2.3 Causality

3 Transcription and Clock System Correctness

  • Transcription: Lustre to NLustre syntactic translation.
  • Lustre fby / fby1 semantic operator.
  • NLustre fby semantic operator.
  • sem_clock: clock type interpretation.
  • sem_annot: alignment between a clock and an expression.

3.1 Correctness of the Clock System

4 Unnesting and Distribution

  • unnest_exp: unnesting of expressions.
  • Idempotence of unnesting and distribution.
  • Fresh: fresh name generation, using a state monad.
  • gensym: axiomatisation of the external function.

4.1 Correctness of Unnesting and Distribution

5 Expression Initialization

5.1 Correctness of Expression Initialization

6.1 Clock Typing

6.3 Translation to Obc

  • ObcSyntax: syntax of the Obc language
  • exp_eval : semantics of Obc expressions.
  • stmt_eval: semantics of Obc statements.
  • normal_args_eq: well-formedness condition on the arguments of NLustre node calls.

6.4 Argument Initialization

  • add_valid: add validity assertions for the variables used in a node call.
  • add_defaults_stmt : add defaults arguments initializations to a statement.

Outline of the compiler (figure 1)

Lustre

Transcription

CoreExpr

Core expressions, used in NLustre and Stc

NLustre

NLustreToStc

Stc

StcToObc

Obc

ObcToClight