EMSOFT 2021: References to the Coq development

This page presents the artifact associated with the EMSOFT 2021 article Verified Lustre normalization with node subsampling (HAL), 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, slides, and video trailer 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

• LSyntax: Lustre expressions, equations and nodes.
• CESyntax: NLustre expressions.
• NLSyntax: NLustre equations and nodes.
• ClockDefs: clocks.

2.2 Semantics

• LSemantics: Lustre semantic rules.
  • const: Sampled constant stream.
  • Sconst: Semantics of a Lustre constant.
  • merge coinductive operator.
  • Smerge: Semantics of a Lustre merge.
  • sem_equation: Semantics of a Lustre equation.
  • sem_node: Semantics of a Lustre node.

2.3 Causality

• LCausality: causality definitions.
  • IsFreeLeft
  • IsFreeLeftList
  • depends_on: dependency between variables of a node.
  • node causality
• AcyGraph: acyclic graphs used by causality analysis.
  • AcyGraph: an inductive definition of an acyclic graph.
  • TopoOrder: topological ordering of the nodes of a graph.
  • has_TopoOrder: existence of a topological ordering.

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

• Correctness theorem.

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

• Correctness theorem.
• The refinement relation over environments and its usage in the proof.
• Expressions length preservation.
• Typing rules for Lustre expressions and nodes.

5 Expression Initialization

• Generation of slow constants.
• Generation of initialization equations, with the optimization using memoization.

5.1 Correctness of Expression Initialization

• Correctness theorem.
• Giving a semantic to slow constants.
• Building fby streams.
• Building if-the-else streams.
• Causality preservation.

6.1 Clock Typing

• wc_clock, wc_env : well-formedness of clocks and environnements.
• instck
• WellInstantiated
• wc_exp: clocking of expressions.
• wc_equation: clocking of equations.
• wc_node: clocking of nodes.

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

• LSyntax: Syntax of Lustre
• LSemantics: Coinductive semantics of Lustre
• LTyping: Typing rules of Lustre
• LClocking: Clocking rules of Lustre
• LCausality: Causal rules of Lustre
• LClockSemantics: Proof of the clock system correctness
  • Unnesting and Distributivity transformation
  • Expression Initialization algorithms
  • Correctness of the normalization

Transcription

• Transcription algorithm
• Correctness of the transcription algorithm

CoreExpr

Core expressions, used in NLustre and Stc

• CESyntax: Syntax of core expressions
• CESemantics: Semantics of core expressions
• CETyping: Typing rules of core expressions
• CEClocking: Clocking rules of core expressions

NLustre

• NLSyntax: Syntax of NLustre
• NLCoindSemantics: Coinductive semantics of NLustre
• NLIndexedSemantics: Indexed semantics of NLustre
• NLMemSemantics: Indexed semantics of NLustre with explicit memory
• NLTyping: Typing rules of NLustre
• NLClocking: Clocking rules of NLustre
• NLNormalArgs: Normalized arguments in NLustre

NLustreToStc

• Translation from NLustre to Stc
• Correctness of the translation from NLustre to Stc

Stc

• StcSyntax: Syntax of Stc
• StcSemantics: Semantics of Stc
• StcTyping: Typing rules of Stc
• StcClocking: Clocking rules of Stc
• StcSchedule: Stc scheduler

StcToObc

• Translation from Stc to Obc
• Correctness of the translation from Stc to Obc

Obc

• ObcSyntax: Syntax of Obc
• ObcSemantics: Semantics of Obc
• ObcTyping: Typing rules of Obc
• ObcInvariants: Useful invariants for Obc
• ObcAddDefaults: Add default initializations
• ObcFusion: Fusion optimization

ObcToClight

• Generation of Clight code
• Correctness of the generation of Clight code