LICS 2025: References to the Rocq development

This page presents the artifact associated with the LICS 2025 article Functional Stream Semantics for a Synchronous Block-Diagram Compiler, by T. Bourke, P. Jeanmaire, 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.

Some names differ between the article and the Rocq source. The links refer to names from the article and Rocq names are given in parentheses.

I.B Compiler correctness

• behavior_asm: compiler correctness, original

II.A Abstract Syntax

We define a subset of the full Lustre syntax of Vélus using the following predicates:

• restr_exp: expressions
• restr_block: equations
• restr_node: nodes
• restr_global: global programs

The type of clocks.

II.B Relational Semantics

• value: the abstract type of values and its CompCert instance
• svalue: the type of synchronous values
• LSemantics: Lustre semantic rules
• sem_node: semantics of a Lustre node, and the base-of (clocks_of) function
• sem_equation: semantics of a Lustre equation
• Sconst: semantics of a Lustre constant, and the const function

II.C The CPO library

Imported from C. Paulin-Mohring.

Generic definitions

• ord: ordered type
• monotonic: monotonic functions
• cpo: CPO
• continuous: continuous functions
• FIXP: fixpoint operator as a continuous function

Stream definitions

• DStr: the type of streams
• DS_bot: the bottom stream (Eps forever)
• DS: the CPO of streams
• The REM, APP, MAP, zip, FILTER and take primitives, encoded with the scase function
• The is-cons and infinite predicates
• DSle: the prefix order on streams

III.A Values

• sevalue (sampl): the type of synchronous possibly erroneous values
• SEnv (DS_prod SI): the type of stream environments
• FEnv (Dprodi FI): the type of stream functions environments

III.B Fixpoint semantics of nodes

• denotN (denot_node): the denotation of nodes
• denotE (denot_exp_eq): denotation of expressions
• denotG (denot_global): denotation of programs

III.C Synchronous stream operators

Constants

• const: constants in Vélus
• sconst: denotational synchronous constant stream
• ok_const: correspondence lemma

Binary operators

• lift2: relational lifting of binary operators
• sbinop: denotational lifting of binary operators
• ok_binop: correspondence lemma

Sampling operator

• when: relational sampling operator
• swhen: denotational sampling operator
• ok_when: correspondence lemma

Delay

• fby: relational delay operator
• fby: denotational delay operator
• ok_fby: correspondence lemma

III.D Resettable node instances

• mask: the mask relational operator
• Sapp: the relational smemantic rule for node instances
• reset: characterization of reset à la Lucid Synchrone
• merge' / expecta: the speculative definition of merge
• sreset: characterization of denotation reset
• theorem 2 (reset_match): correspondence of the two characterizations
• theorem 3 (ok_reset): correspondence of denotational and relational reset

Three main properties:

• abs_indep_global: invariance to initial absences
• lp_global: commutation with stream prefixes
• abs_alignLE: alignment of absences

III.E Causality errors

• lemma 4 (is_ncons_S_fby)
• lemma 5 (denot_S)
• theorem 4 (denot_inf)

III.F Typing and runtime errors

• clock-of (AC): getting a stream's boolean clock
• denotC (denot_clock): interpretation of a clock type
• wf_env: the well-formed predicate on stream environments
• no-rte-exp: the no run-time errors predicate for expressions
• lemma 6 (safe_node)
• the same for global programs

IV Compiler Correctness

• theorem 6 (_ok_global_main)
• behavior_asm: original compiler correctness
• behavior_asm_exists: new compiler correctness (figure 5)

IV.A A Simple static analysis

• check_unop: classification of CompCert's unary operators
• check_binop: classification of CompCert's binary operators
• check_exp: the check-ops procedure for expression
• theorem 7 (check_global_ok): correction of the procedure
• theorem 8 (behavior_asm_new_check): new compiler correctness with static check

V Paragraph on dependently-typed synchronous semantics

From Boulmé and Hamon, adapted to the new Coq syntax by Keller.

• samplElt: the type of clocked streams elements
• Str (samplStr): the type of clocked streams
• sp_when: the sampling operator