Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Towards a Coq-verified Chain of Esterel Semantics

Gérard Berry, Lionel Rieg

TL;DR

This work formalizes the chain of Esterel semantics in Coq, introducing a novel microstep semantics that closely mirrors circuit behavior while staying SOS-friendly. It establishes formal simulations and refinements among the logical, constructive, and state constructive semantics, and proves equivalence with the microstep view for the loop-free Kernel Esterel. By providing Coq-based representations, proofs, and interpreters, it lays groundwork toward a verified Esterel-to-circuit compiler, bridging high-level synchronous semantics and low-level hardware translation. Although looped constructs remain outside the current formalization, the framework delivers a rigorous, machine-checked foundation for correctness of Esterel semantics and paves the way for future extensions to full Esterel and circuit backends.

Abstract

This paper focuses on formally specifying and verifying the chain of formal semantics of the Esterel synchronous programming language using the Coq proof assistant. In particular, in addition to the standard logical (LBS) semantics, constructive semantics (CBS) and constructive state semantics (CSS), we introduce a novel microstep semantics that gets rid of the Must/Can potential function pair of the constructive semantics and can be viewed as an abstract version of Esterel's circuit semantics used by compilers to generate software code and hardware designs. Excluding the loop construct from Esterel, the paper also provides formal proofs in Coq of the equivalence between the CBS and CSS semantics and of the refinement of the CSS by the microstep semantics.

Towards a Coq-verified Chain of Esterel Semantics

TL;DR

This work formalizes the chain of Esterel semantics in Coq, introducing a novel microstep semantics that closely mirrors circuit behavior while staying SOS-friendly. It establishes formal simulations and refinements among the logical, constructive, and state constructive semantics, and proves equivalence with the microstep view for the loop-free Kernel Esterel. By providing Coq-based representations, proofs, and interpreters, it lays groundwork toward a verified Esterel-to-circuit compiler, bridging high-level synchronous semantics and low-level hardware translation. Although looped constructs remain outside the current formalization, the framework delivers a rigorous, machine-checked foundation for correctness of Esterel semantics and paves the way for future extensions to full Esterel and circuit backends.

Abstract

This paper focuses on formally specifying and verifying the chain of formal semantics of the Esterel synchronous programming language using the Coq proof assistant. In particular, in addition to the standard logical (LBS) semantics, constructive semantics (CBS) and constructive state semantics (CSS), we introduce a novel microstep semantics that gets rid of the Must/Can potential function pair of the constructive semantics and can be viewed as an abstract version of Esterel's circuit semantics used by compilers to generate software code and hardware designs. Excluding the loop construct from Esterel, the paper also provides formal proofs in Coq of the equivalence between the CBS and CSS semantics and of the refinement of the CSS by the microstep semantics.

Paper Structure

This paper contains 56 sections, 18 theorems, 31 equations, 13 figures, 2 tables.

Table of Contents

  1. Introduction
  2. Synchrony, determinism, concurrency: a short history of Esterel
  3. Signals in Esterel
  4. Causality issues
  5. Switching to the circuit semantics and implementation
  6. Summary of the final Esterel semantics chain
  7. Related work
  8. The contents of this paper
  9. Kernel Esterel
  10. Signals, instants, and synchrony
  11. Kernel statements
  12. Completion codes and the trap encoding
  13. A running example
  14. Intuitive Semantics of Kernel Esterel
  15. Esterel semantics in Coq
  16. ...and 41 more sections

Key Result

Lemma 1

For all $p$, $E$, $E'$, $k$, and $p'$, if $p \lhook\,\joinrel\xrightarrow[E]{\; E', \, k \;} p'$, then $E'$ is total. (Notice that we make no assumption on $E$).

Figures (13)

  • Figure 1: The chain of Kernel Esterel semantics. Arrows represent simulation.
  • Figure 2: Logical (Behavioral) Semantics (LBS) rules.
  • Figure 3: Execution of ABROi in the LBS.
  • Figure 4: Definitions of the functions Must and Can. The first component is for signals, the second one for completion codes.
  • Figure 5: Start rules of the state semantics.
  • ...and 8 more figures

Theorems & Definitions (33)

  • Remark 1
  • Remark 2
  • Remark 3
  • Example 1: ABROi program
  • Example 2: Intuitive execution of the ABROi program
  • Lemma 1: Output events are total
  • Lemma 2: Determinism of the constructive semantics
  • Lemma 3: Properties of Must and Can
  • Theorem 4
  • Remark 4
  • ...and 23 more