EMSOFT 2023: References to the Coq development

This page presents the artifact associated with the EMSOFT 2023 article Verified Compilation of Synchronous Dataflow with State Machines, by T. Bourke, B. Pesin, and M. Pouzet. You can also download the slides of our presentation. 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.

1 Introduction

The example given in the introduction can be found at examples/stepper-motor.lus.

2.1 Abstract Syntax

• LSyntax: Lustre syntax
• exp: expressions
• block: blocks
• node: nodes
• global: programs

2.2 Synchronous Core

• LSemantics: Lustre semantic rules
• sem_node: Semantics of a Lustre node
• sem_equation: Semantics of a Lustre equation
• Svar: Semantics of a Lustre variable
• Sconst: Semantics of a Lustre constant
• const: Sampled constant stream
• when coinductive operator
• merge coinductive operator
• wc_Ewhen: Clock-typing rule for a Lustre when
• wc_Emerge: Clock-typing rule for a Lustre merge
• merge_when: correspondence of when and merge
• fby coinductive operator
• fby1 coinductive operator
• Sfby: Semantics of a Lustre fby

2.3 Switch Blocks

• when_hist: when lifted to histories
• Sswitch: Semantics of a switch block
• wc_Bswitch: Clock-typing rule for a switch block

2.4 Local Scopes and Shared Variables

• Sscope: Semantics of a local scope
• Slast: Semantics of a last expression
• union operator on histories

2.5 Reset Blocks

• mask coinductive operator
• mask_hist: mask lifted on histories.
• Sreset: Semantics of a reset block

2.6 State Machines

• select coinductive operator
• SautoWeak: Semantics of a state machine with weak transitions
• SautoStrong: Semantics of a state machine with strong transitions
• sem_transitions: Semantics of state machines transitions and initializations
• choose_first (first-of) coinductive operator

3.1 Dependency Analysis and Instrumented Semantic Model

• LClockedSemantics: Instrumented semantic model
• sc_vars: Clock correctness property
• LCausality: dependency definitions
• LClockCorrectness: Proof of clock correctness

3.2 Shared Variables

• delast_scope: compiling last declarations
• delast_block_sem: correctness of compilation of last

3.3 State Machines

• auto_block: compiling state machines
• trans_exp: compiling transitions
• auto_block_sem: correctness of compilation of state machines

3.4 Switch Blocks

• switch_block: compiling switch blocks
• subclock_exp: renaming/resampling expressions
• switch_block_sem: correctness of compilation of state machines

3.5 Local Scopes

• inlinelocal_block: inlining of local scopes
• inlinelocal_block_sem: correctness of inlining of local scopes

3.6 Reset Blocks

• reset1 coinductive operator for NLustre
• unnest_block: normalization of reset blocks
• block_to_equation: transcription of blocks
• to_equation: transcription of equations
• sem_blocktoeq: correctness of the transcription of blocks