{'fraction_non_alphanumeric': 0.037080028374282585, 'fraction_numerical': 0.005599621676232239, 'mean_word_length': 4.6110843082860935, 'pattern_counts': {'":': 0, '<': 5, '<?xml version=': 0, '>': 1, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 16, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
Towards Coq-verified Esterel Semantics and Compiling

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. The paper also provides formal proofs in Coq of the equivalence beween the CBS and CSS semantics and of the refinement of the CSS by the microstep semantics.


Introduction
The goal of the research presented here is twofold: first, formally validate the chain of semantics of the synchronous reactive language Esterel [Ber00b] that leads from its definition to its implementation; second, build a formally proven compiler from Esterel to clocked digital circuits or C code. The tools we use for this are the SOS semantics chain developed for Esterel between1984 and 2002, a new operational semantics that gets closer to the circuit semantics of [Ber03] on which the Esterel v5 and v7 compilers are based, and the Coq proof assistant [CDT19] as the formal verification environment.We limit ourselves to Kernel Esterel [Ber00b], the core language that only deals with pure signalling but still gathers all the technical difficulties. Although the full Esterel language involves data-valued signals and variables, its handling would not add extra difficulties since the only technically relevant addition is the insertion of data dependencies in the control flow, which can be technically handled almost in the same way as Kernel Esterel's simpler pure signal dependencies. Esterel, born in 1983 [BMR83], was initially dedicated to programming reactive discrete control systems. Because of their very nature, such systems required both concurrency and behavioral determinism. These constraints made Esterel completely depart from the concurrency = asynchrony paradigm (dogma?) that was dominant at the time because of the fast development of distributed algorithms and algebraic process calculi in Milner's style [Mil83], since asynchrony intrinsically implies non-determinism. Esterel was soon accompanied by other synchronous languages such as Lustre [HCP91] and Signal [GBGM91], dedicated more specifically to data-flow oriented continuous control and signal processing systems, as well as by graphical languages such as SyncCharts [And96] and Argos [Mar91], inspired by both Esterel and Harel's beautiful idea of hierarchical concurrent state diagrams (note that Harel's Statecharts were not quite synchronous in our sense). Esterel's application range grew quickly, including industrial safetycritical embedded systems in avionics [BBdS + 00], robotics [ECM90], communication and networking protocols [MS92], the synthesis of efficient synchronous digital circuits [TB93,BKS03], etc. The Esterel / SyncCharts tightly coupled pair was industrialized in the mid 1990's for software generation, followed in 2001 by production-level hardware design and generation from the more powerful Esterel v7 language [Est08] with applications to telephone chips, networks on chips, DMAs and memory controllers, etc. In parallel, Lustre was industrialized at the end of the 2000's under a graphical form called SCADE, used in avionics, nuclear plants, etc. In 2006, Esterel, SyncCharts and SCADE were unified by the Esterel Technologies company (now part of Ansys) into the SCADE 6 language and toolset [CPP17], now widely used in industrial certified embedded systems and other critical applications. In parallel, research continued with the advent of new synchronous languages or sublanguages in other groups: Reactive C [Bou91], Reactive ML [MP05], Lucid Synchrone [CP99], Quartz [Sch09], SCL [vHMA + 13], SCCharts [vHDM + 14], some Ptolemy II domains [Pto14], and more recently Lingua Franca [LMBL21] and HipHop [BS20], the latter being an integration of Esterel into JavaScript dedicated to reactive web applications or components.

A short history of synchrony
Let us first focus on how and why concurrency and determinism are reconciled by the concurrent synchronous languages. The shared objects between concurrent statements are named signals in Esterel and Signal, or flows in Lustre, with very similar semantics. Intuitively speaking, execution consists of a series of discrete and conceptually timeless reactions, where each reaction handles a separate input vector and generates an output vector in a deterministic way and conceptually in zero time, internally broadcasting unique values for all interfaces or local shared objects. Determinism is guaranteed by enforcing the execution of all active write statements to a shared object before any read statement of the same object, and, in case of multiple writes (allowed in Esterel), guaranteeing that the computed value is independent of the ordering of the writes.
Of course, deadlocks could occur in synchronous languages because of these constraints, for instance if one wants to modify a shared object in a reaction depending on the final value it will take in this very same reaction, which causes a causality cycle. Various strategies have been developed to systematically detect such errors at compile time or runtime according to compiling technology choices. Lustre uses topological sorting of its flow equations to always ensure deadlock freedom, while Esterel uses a more sophisticated and more liberal approach called the constructive semantics, which will be detailed in the sequel. Signal and Ptolemy's synchronous domains use different constraints in the same vein [GBGM91,Pto14]. In practice, the fact that all potential deadlocks can always be detected at runtime, or even at compile-time modulo mild programming restrictions, is a major advantage of synchronous languages over asynchronous ones in the considered application domain: with asynchrony, hard to detect and debug deadlocks can occur at runtime, they cannot be easily detected at compile time and sometimes even at runtime. But the synchronous application domain is of course more restricted than the asynchronous one, which contains all large-scale distributed systems.

Relation with digital circuits
In 1990, the second author realized that the synchronous point of view for software was very similar to the classical functioning of clocked digital circuits, where electricity propagates concurrently in all wires with a deterministic result obtained in a predictable amount of time [Ber92]. A compiler from Esterel to hardware soon followed and showed excellent performance on industrial circuit designs when complemented by BDD-based smart optimizers. It was readily industrialized and served as a basis for the aforementioned Esterel v7 / Esterel Studio toolset by Esterel technologies, which has been used in production for complex circuits on various Systems on Chips, also generating their software simulators, On the theory side, following seminal work by Malik [Mal94] on cyclic circuits, it was shown that a semantics of digital circuits based on constructive (intuitionistic) Boolean logic instead of the classical one exactly reflected the guaranteed stabilization of electrical potentials in possibly cyclic combinational circuits [SB96,MSB12]. Our intention for later research is to formally verify that the same semantics/electricity perfect match exists for Esterel endowed with its constructive semantics, thus considerably extending the result of [SB96,MSB12] that only dealt with the much simpler sets of acyclic Boolean equations that usually define synchronous circuits.

The Esterel semantics chain
The chain of semantics that makes it possible to translate Esterel programs into circuits was first described in a draft book made available on the web [Ber03], but never published because it lacked the indispensable proofs. In 2001, the second author went to the Esterel Technology company and had no more time to write these proofs. In 2006, the semantics were augmented to deal with data in the "Compiling Esterel" book [PBEB07]. Coming back to research in 2012, the second author became tempted to use the Coq proof assistant to build fully formal proofs, following the path opened by Gonthier for machine-checked formal proofs of hard mathematical theorems [GAA + 13] and by Leroy for the construction of the formally verified CompCert C compiler [Ler19]. (Note that Gonthier was also the second author's coauthor for [BG92] and the inventor of several fundamental semantical and implementation techniques for Esterel.) These major milestones defined the path to be followed: proofs of this kind should be written and checked on computers using elaborated proof assistants, instead of written by hand and referred by eyes and brains. Furthermore, as shown by Leroy, using Coq as the proof assistant also makes it possible to extract a guaranteed correct compiler out of the logical proof. This greatly improve the confidence we can have in the generated software as shown by the Csmith experiment [YCER11].
Besides this automatic compiler generation, our final goal is to finally publish the book "The Constructive Semantics of Pure Esterel" with formal proofs included as Coq programs executable by anybody who wants to check the proofs.
The work presented here was essentially realized by the first author. It consists in formally proving the relations between the various semantics in the chain, from the one that defines the language to the final one that translates programs into circuits. Each element in the chain tackles a particular difficulty intrinsic to Esterel. For Kernel Esterel described in [Ber03] and Section 2 below, the chain is as follows: • The logical semantics, introduced in [BC84], defines logical constraints that ensure reactivity but not determinism. Its constraints are natural, but still to too loose in the sense that they accept some programs that happen to be deterministic "just by chance", i.e., in a non-causal way. A slightly different version due to Tardieu [Tar04] also ensures determinism, but adds some technical complexity we do not find relevant for this work, for which the logical semantics will just be a starting step.
• The constructive semantics [Ber03] refines the logical semantics by imposing proof-theoretic constructivity constraints that characterize a causal and disciplined flow of information in the program, which implies determinism in a natural way. It has become the true reference semantics of the language, replacing Gonthier's potential analysis [BG92] that only gave sufficient conditions for determinism.
• Both behavioral semantics above are defined by SOS-like deduction rules [Plo81], where each SOS transition transforms a program text into another program text ready for the next reaction. This was enough to build an interpreter or an automata-based compiler such as the first Esterel v2 academic compiler [Cou88], but remained unpractical for efficient compiling. Gonthier's state semantics [BG92] (logical, potential-based, or constructive) replaces text rewriting by a representation of program states by sets of pointers to some particular source programs statements, in a way inspired by the algorithm described in [BS86] that efficiently translates regular expressions into automata. Gonthier's potential-based state semantics was used in the Esterel v3 compiler, the first one to have been indutrialized.
• The token-based microstep semantics analyzes precisely the step-by-step propagation of information in an Esterel program during one reaction, according to the current state computed from the last reaction and the current input. It was not published in [Ber03], but only later in [PBEB07] in a version we improve and formally verify here.
• Finally, the constructive circuit semantics is a state semantics defined by a translation of an Esterel program into a digital circuit that has exactly the same electrival reactive behavior when fed with electrons, because it corresponds to the constructive semantics of digital circuits [MSB12]. It is the typical proof goes by induction on the derivation tree in the source semantics and builds an adequate derivation tree in the target semantics. The full Coq code for the syntax, semantics, and proofs presented in this paper is available as supplementary material to this article.
A fair number of proofs have no technical difficulty and rely mostly on a straightforward induction. They will not be detailed here, where we will only concentrate on the interesting points. We refer the interested reader to the Coq development. This paper contains links to the html documentation generated from the Coq development, permitting a more confortable browsing of the formalization. If you put the file corresponding to this paper in the root directory of the Coq developement, you will be able to directly use these links, represented as in the margin.

Structure of the paper
Section 2 defines the Kernel Esterel language and its informal semantics. Sections 3 to 6 detail the chain of Kernel Esterel semantics presented in Section 1.3, namely the logical semantics (Section 3), the constructive semantics (Section 4), the constructive state semantics (Section 5), and the microstate semantics (Section 6). Section 7 details practical considerations of the Coq proofs and representation of the results presented in this paper. Finally, Section ?? presents our conclusion and future work. The appendix contains the rules of all semantics presented here in extenso, as well as some technical functions used in these semantics and not detailed beforehand. They are given for reference and readability, although the one true and correct reference is the Coq development.

Signals, instants, and synchrony
Kernel Esterel deals with pure signals, i.e., scoped shared objects name here , ′ , ... that only carry a presence/absence status where + stands for presence and − for absence. In the full language, statuses can be combined using the usual Boolean operators; here, we use only negation, which is not indispensable because it can be programmed in Esterel but simplifies the presentation. The data values available in the full language are not supported in the kernel. This is not really a limitation: the development of Esterel semantics and compilers has shown that dealing with shared data values can be done in much the same way as dealing with the pure signals to which they are attached [PBEB07].
A Kernel Esterel program is defined by an interface, which defines the set  of input signals and the set  of output signals, and a body, which is an executable statement. An event is defined as a map from a set of signals to {+, −} (or {+, −, ⊥} for the constructive semantics, see Section 4 and later).
The execution of the program consists of successive reactions to input events that generate output events according to the execution of the body. The body is stateful, as for a finite automaton but in a much richer way because the states are themselves hierarchically structured (see the state semantics in Section 5).
The synchrony hypothesis stipulates that reactions have no duration: inputs do not vary in the instant and outputs are produced instantly in a deterministic way, local signals also having a unique value in their scope. To stress that point, we call reactions instants from now on. The synchrony hypothesis guarantees non-interference between inputs and computations, which is the key to determinism. In actual implementations, instants are externally determined and the conceptually instantaneous execution may be implemented by hardware clock cycles, atomic execution of software code, or even appropriately synchronized distributed execution of a distributed program provided interference between I/O and execution is avoided. This is outside the scope of this paper.

Kernel statements
Kernel Esterel contains a small number of statements, from which one can easily define the richer statement set of the user-friendly full language [Ber00a,Est08]. A statement starts at some instant and may execute either instantly, i.e., entirely within the instant, or up to some further instant, or even indefinitely. Its starting and ending (if any) instants define its lifetime.
The statements can be presented in two equivalent forms: with keywords, which make reading easier, or with mathematical symbols, which is far better for semantics rules and proofs. We use the latter symbolic form in all technical developments. Here are the kernel statements, where is a signal, is an integer and , are kernel statements: ; We slightly depart from [Ber03] in two ways: first, we rename the present test of Esterel v5 [Ber00a] into _ _ _ as in Esterel v7 [Est08]; second, we add await immediate to the kernel, written as @ , which could be defined from the other kernel statements as trap T in loop if then exit T else pause end end end or "{( ? 2 , 1) * }" in the symbolic form, much shorter than the full textual definition above.
Remark 1. The reason to include "await immediate " in the kernel is that the microstep semantics (Section 6) does not support loops yet. Thus, in order to express suspension " " in the constructive semantics (Section 4), we need "await immediate " to wait until becomes absent before performing another step of .
Besides the shared signals denoted by , the main ingredients are Gonthier's integer completion codes that make it possible to handle the termination, pausing, trap-exit, and concurrency control structure in a unified way. Notice first that the three "nothing", "pause", and "exit " statements in the textual presentation are unified into a single " " statement in the symbolic presentation where is an integer. This integer is called a completion code, and at each instant each executed statement returns such a completion code. Code 0 means termination, code 1 means pausing for the instant and waiting to be resumed at the next instant, and a code ≥ 2 means exiting an enclosing trap that may be arbitrarily far above. The beauty of this encoding of control is that synchronizing parallel branches reduces to performing a trivial operation on their completion codes, as detailed below. In the textual form, traps are named and lexically scoped. In the symbolic form, an "exit " statement is encoded by the number + 2 if going up from the exit statement to its corresponding trap requires traversing other trap statements. Although this is not technically necessary, in our textual exit examples we add the code as an exponent to the trap name for more clarity. Note that our encoding of traps is no more than a slight modification of the De Bruijn encoding of bound variables in the -calculus [Nru72], by adding 2 to account for termination and pausing.

Intuitive Semantics of Kernel Esterel
The intuitive semantics is defined by cases over the statements: • The "nothing" or 0 statement instantly terminates, returning completion code 0.
• The "pause" or 1 statement waits for the next instant: at its starting instant, its stops control propagation and returns completion code 1; at the next instant that makes it executed it terminates and returns code 0 (this not necessaly the instant that follows the starting instant since the statement could be preempted or suspended).
• At a given instant, the status of a signal is shared by all program components within its scope. By default is absent in a reaction. The " " or ! statement sets present for the instant.
• The "await immediate " statement blocks control propagation until is present. At every instant including the starting one, if is absent it behaves like pause, and if is present it behaves like nothing. • The presence test statement " " or ? , instantly tests the status of . According to the presence/absence of , it selects or for immediate execution and behaves as it from then on. Note that the test is only performed at the instant in which the statement is started.
• The delayed suspension " " or ⊃ statement behaves as in its starting instant. In all subsequent instants during the lifetime of , it executes whenever is absent in the instant and freezes the state of until the next instant if is present. Notice that the status of is tested at all instants except for the starting one. The completion code of the first instant is that of and for further instant (if any) it is that of if is absent and 1 if is present. Thus, termination and trap exits of are propagated at the first instant or if is absent.
• For a sequence " ; ", instantly starts when terminates. Trap exits by or are propagated.
• A loop "loop end" or * statement instantly restarts its body when this body terminates, and it propagates traps. Notice that traps are the only way to exit loops (the statement of the full language is definable in the kernel language).
• At each instant, the " " or { } statement terminates or pauses if does, terminates if returns completion code 2 (i.e., the trap catches its exits), or returns completion code − 1 if the completion code of is > 2 (i.e., propagates exits to the appropriate outer trap).
• The textual "exit " or symbolic statement with ≥ 2 simply returns completion code .
• The "↑ " symbolic statement is useful to define macro-based full-language statements that place in a "{_}" trap context. It simply adds 1 to any trap completion code ≥ 2 returned by . It is not needed in the textual form since traps are named, and we won't use it in textual examples.
• The crux of Gonthier's encoding is the representation of parallel control synchronization by the trivial arithmetic operator. In the intuitive semantics, a parallel statement terminates instantly as soon as all its branches have terminated; it exits instantly a trap if one of its branches does; and it pauses if at least one branch pauses and no branch exits a trap. If several branches concurrently exit traps, the parallel exits the outermost trap among those exited by its branches. In the symbolic formal semantics, this behavior simply reduces to the parallel statement | returning as completion code the maximum max( , ) of the completion codes of its branches at each instant.
• Finally, a local signal declaration "signal in end" or ∖ declares a signal local to its body , with the usual lexical binding and shadowing in both the textual and the symbolic presentation.

The logical semantics
The SOS-style logical (behavioral) semantics (LBS) defines constraints that ensure reactivity of a program to a given set of inputs, i.e. absence of deadlock and presence/absence of all signals. In the version given here, it does not guarantee determinism; Tardieu [Tar04] has proposed a version that also guarantees determinism, but we find it too heavy since it amounts to verifying that all non-deterministic executions yield the same result (this may require considering an exponential number of executions with nested local signals). Determinism will be guaranteed for much more compelling conceptual reasons by the constructive semantics detailed in the next section.
The logical semantics defines reactions as behavioral transitions represented by SOS rules of the form where , ′ are events, that is, maps from signals to their status + (for present) or − (for absent). The event denotes the inputs of while ′ denotes its outputs, that is, it maps to + the signals emitted by . The integer is the completion code of for the instant, and ′ is the derivative of by the transition, i.e. the statement replacing for the next instant (this terminology is inspired by the work of Brzozowski and Seger on translating regular expression to automata [BS95]). The rules are given in Figure 1.
Note that the rule ∅, ← ← ← ← ← ← ← ← ← ← ← ← ← ← ← ← ← ← → 0 covers three statements: first, the trivial termination of 0 ( ); second the pausing case for 1 ( ) that returns completion code 1 and derivative 0 ( ) that will terminate instantly at the next reaction; third, the ( ) exit statement which returns completion code and derivative 0 ( ). Except for the rules Sig + and Sig − that deal with signal declaration, our rules are a straightforward implementation of the intuitive semantics. The trap statement catches the innermost exit (the one with code 2) and turn it into termination (code 0). This is the meaning of the ↓ function, with (pseudo-)inverse ↑ used in shift.
Note an unusual aspect: an instantaneous but compound reaction is voluntarily defined by a single transition The union ′ ∪ ′ in the sequence rule conclusion directly expresses the synchrony hypothesis within the reaction: the control passes from to in the very same reaction. The same holds for the parallel statement.
The Sig + and Sig − rules for local signals first extend the input event with mapped to a status (possibly shadowing any uper-scoped signal ), written * , then execute using this new input event, and finally remove from the output event ′ before returning it ( ′ ⧵ ), the completion code and derivative statement being the ones of the execution of . The side condition + ∈ or + ∉ ensures the broadcast of 's status in .
If the completion code is not 1, then there is nothing left to execute, either because we finished execution ( = 0) or because a trap killed the remaining state ( ≥ 2), hence the derivative should be 0. It is clearly not the case with the rules just presented, for instance the trap rule always preserves the trap. Unlike in [Ber03], the Coq implementation chooses useful to kill the derivative whenever ≠ 1 by introducing a function defined as follows: Then we replace each derivative ′ with ( , ′ ) (some rules do not require this, namely the ones for , ! , ? , , , and ; when = 0). See Appendix A.2 for our full definition of the logical semantics with the function. The notation is taken from Dirac function, as our it is non-zero only when = 1. Although it is not mandatory, it technically and conceptually simplifies the calculations by bringing back all terminated terms to 0 which makes termination checks simpler.
Why the Sig + and Sig − rules can be non-causal or non-deterministic The Sig + and Sig − rules for ∖ express two logical coherent constraints requiring that a signal can only be either received and emitted or not received and not emitted. In this weak form, such synchrony constraints may not always be satisfied, deterministic, and causal, as we now illustrate.
• Assuming that is not an imput and not emitted elsewhere in the program, there is no possible reaction for the statement " ", i.e." ? 0 , ! " in symbolic form. If + ∈ , the rules for ? , and 0 imply + ∉ ′ , which makes Sig + inapplicable. Conversely, − ∈ implies + ∈ ′ , which makes Sig − inapplicable. This is a typical (decidable) deadlock.
With − ∈ , the rules for ? , and 0 imply + ∉ ′ , which makes Sig − applicable. Since two different transitions with two different emissions are possible, the reaction is non-deterministic, which contradicts our initial intention.
• For " ", i.e. " ? ! , ! ", one has + ∈ ′ independently of the status of in . Thus, − ∈ is incoherent and Sig − is inapplicable. On the contrary, + ∈ is consistent with + ∈ ′ as Sig + applies. Nevertheless, we need to know the status of in order to decide which branch to execute. This reaction is logically coherent and deterministic but not causal since the presence of causes its own emission. In the next section, such a causality loop will be ruled out by the constructive semantics.
These behaviors certainly do not correspond to our intention. To solve this question, the constructive semantics was introduced in [Ber03]. We focus on now on this semantics, which has become the reference for the language, for deep reasons.

The Constructive Semantics
As we just saw, the logical semantics is dissatisfying for three reasons, all due to the use of the coherence law to define the status of local signals. Let us investigate in turn these three defects, namely forward dependencies, causality loops, and the mismatch with the circuit semantics.
Unwanted forward dependencies within a reaction can arise from a presence test for a signal in the first statement of a sequence to an emission of that signal in the second statement of that sequence. For instance, the program (( ? ! 1 , ! 2) ; ! )∖ can only have one execution according to the logical semantics: Indeed, the signal is emitted because of the ! statement, so that only the Sig + rule applies. Therefore, the present statement executes the "then" branch, here ! 1, which gives the result. Nevertheless, it is unfortunate that ? ! 1 , ! 2 depends on ! whereas the latter is done after the former in the sequence within the reaction. We want sequences to be causal. Consider now the equally simple program ( ? ! , ! )∖ . Both Sig + and Sig − rules can be applied, by supposing to be either present or absent, which contradicts our determinism intention. In both cases, the results about 's presence appear to be self-justified with non-causal reasons, which is exactly what we want to reject. The translation to digital circuits of [Ber03] gives another compelling reason: such programs yield electrically unstable cycles in the generated circuit, which should be avoided by all means. Altogether, the constructive semantics we now present differs from the logical one on two main aspects: the statuses of signals and the signal rules. Signals may take a third status ⊥ representing the absence of information: we do not know yet whether this signal is emitted or not. This means in particular that no rules can apply to " " if 's status is ⊥: the execution is blocked on the test. Only the signal declaration rule deals with status ⊥. For this, it uses two auxiliary mutually recursive functions Must and Can to compute respectively the set of signals that must and can be emitted inside an instant using only the information contained in the event . They intuitively represent the information we can gather from the body of by making no assumption on the status of the declared signal , that is, by setting its status to ⊥. This restriction ensures that the justification of the status of signal does not rely on itself.
As most of the logical semantics rules do not deal with signal statuses, we do not need to modify them. Moreover, the rules for " ", " " and " " can also be kept unmodified, as they only refer to statuses + and −. Finally, only the two rules for signal declaration need to be reworked, where handling ⊥ is deferred to two auxiliary functions, Must and Can: The Can and Must functions The auxiliary functions represent for Must an under-approximation and for Can an over-approximation of the final set of emitted signals. They coincide on most statements, differing only on four of them: " ", " ", " ; ", and " ". For instance, when the status of is ⊥ in a presence test ? , , we do not know which branch to execute so that nothing must be done; on the contrary, both branches can be executed, hence the difference between Must and Can.
Technically, we need to compute approximations for both signals and completion codes at the same time because the sequential composition ; needs to know if must/can terminate to decide if has to be considered. The computed signal and completion code sets are denoted by adding a subscript to the Must and Can functions: for signals and for completion codes, as in Must ( , ) for signals and Must ( , ) for completion codes. We usually drop the subscript as the ambiguity is easily resolved from the context. Furthermore, in the case of Must, the set of completion codes is either empty or a singleton because of determinism, whereas it can be an arbitrary non-empty set for Can. The ↑ and ↓ functions used for computing the completion codes of statements { } and ↑ are extended pointwise to sets of completion codes, that is, ↑ = {↑ | ∈ }. The maximum of two completion code sets 1 and 2 , written Max( 1 , 2 ), is the set of pointwise maxima: max( 1 , 2 ) | | 1 ∈ 1 ∧ 2 ∈ 2 . We write ∖ the removal of element from set , instead of the more standard but more cumbersome ⧵ { }. This is used on signal sets for local signal declaration ∖ (where we borrow the notation from), but also on completion code sets for ; . Operations on sets are extended to pairs of sets computed by Must and Can by applying them on each component where it is meaningful: When Must( ∖ , ) concludes that the status of the local signal must be +, we want to propagate + inside to get more information. This can only be done when we are sure that ∖ is executed, not merely that it could be executed as Can expresses. Therefore, Can needs to carry a + tag telling whether the statement must be executed or a ⊥ tag if we don't have this information.
Must and Can are defined by mutual induction (because of the signal declaration case) over the statement (see Figure 2).

Lemma 1 (Properties of Must and Can). For all , , and , we have:
• Any statement can produce a completion code: Can ( , ) ≠ ∅; • When is known to be executed, we can be more precise: Can + ( , ) ⊆ Can ⊥ ( , ); • Everything that must be done can be done: Must( , ) ⊆ Can ( , ); • When must return completion code , we have enough information to deduce that this is the only The constructive restriction ensures that the result is deterministic and that undefined statuses cannot be created along execution : they are only temporary statuses. More precisely, if we define a total event as a constructive event where no signal is mapped to ⊥, we have the following lemmas: Proof. See Section 7.4.
One may wonder how large is the gap between the under-and over-approximations described by Must and Can. It can be arbitrarily big in general, for instance if doesn't appear in , then for any E, Must (( ? , )∖ , ) = (∅, ∅) whereas Can + (( ? , )∖ , ) = Can + ( , ). Nevertheless, for constructive statement, they are equal, which is even a characterisation of constructive statements: Proof. See Coq formalization (file Semantics/CBS.v).
Remark 2. This is only true for loop-safe [Ber03], that is, for statements in which the Can function on all loop bodies does not contain 0. This notion could be refined more, but it does not seems very interesting or useful.
At this point, the reader may wonder in which way the non-causal programs we mention before, namely 1 = ( ? ! , 0)∖ and 2 = ( ? ! , ! )∖ , are rejected. The technical answer is quite simple : no constructive rule can be applied to them. Why is that? Because of the definitions of Can and Must. For instance, to evaluate 1 we have to check whether we can apply the rule for local signals, namely C-Sig + or C-Sig − . To apply C-Sig + , we have to compute Must(( ? ! , 0)∖ , ). Thus, we must first evaluate The reader may also wonder whether our choice is the best one speaking of constructiveness. Our view is that what justifies it is the direct correspondence with constructiveness of sets of Boolean equations logically defining digital circuits. In [MSB12], it is proved that Boolean constructiveness is equivalent to electrical stability of the result computed by a physical mapping of the equations, under a reasonable gate and wire delay model.
Even though the constructive semantics is well-suited as the starting semantics of Esterel, it is quite far from the circuit one of [Ber03], mostly because the models are very different. On the Esterel side, the semantics transforms the source code into a derivative by keeping only the currently active parts of the program, i.e. what is left to execute. On the contrary, circuits are fixed hardware where only the state of registers can be modified between reactions. To bridge this gap, one can present the constructive semantics in a different way, keeping the source code intact and adding tags on top of it to represent where the execution currently is : these tags will correspond to a distributed program counter that precisely encodes the states of the hardware registers, and the program text will be preserved, exactly as the circuit wiring. This leads us the constructive state semantics we study below.

The Constructive State Semantics
Let us consider the following three programs: P 3 = ! 1 ; 1 ; ! 2 ; 1, P 4 = ? (! 1 ; 1 ; ! 2 ) , ! 3 and P 5 = ! 1 | ! 2 . In the constructive semantics, executing them in the environment = { + , ⊥ 1 , ⊥ 2 , ⊥ 3 } would lead to the following execution chains: Here, executed statements keep disappearing until the whole program becomes 0. In the state semantics, we instead keep the program intact and move tags⋅ to indicate where execution stops at each reaction: In particular, one can directly observe two crucial invariants of the execution of Esterel statements: (i) execution only stops on 1 and @ statements, which are the only statements that can carry a⋅ tag ; (ii) Consider the two branches of a presence test or of a sequential composition. Only one of them can be executed in a given reaction, unlike for parallel composition || that precisely triggers parallel threads. These two properties are enforced by the very definition of states below. Formally, states (written̂ ,̂ ) are defined by the following grammar: The states of "1 ; 1" are "1 ; 1" and "1 ;1", never1 ;1 ; the only state of "(! 1 | 1) ; ! 2 " is "(! 1 |1) ; ! 2 ".
The only elementary states are the active pause and the active statements, written 1 and@ , and states propagate through all other compound statements of the language. The decorated statements1 and@ represent the points where execution should restart in the next instant, in other words, the aforementioned distributed program counter since execution always stops only on "1" or "@ " statements in Kernel Esterel.
The constructive state semantics is a rewording of the constructive semantics where we replace the Such terms , are either active stateŝ ,̂ or inactive statements , . When a derivative term ′ is a statê ′ , it means that execution has paused within̂ ′ for the current reaction and can be resumed later. On the opposite, when this term ′ is a statement , it means that execution is over, either by normal termination or raising a trap. Technically, the state semantics is still a rewriting semantics where the tags are moved around, with the core idea is that the underlying statement never changes. Execution of an instant starts with and yields a term . From one reaction to the next, one resumes from̂ but not from iself, so that there is no implicit toplevel loop restarting . Tagged statements (states) are called active, and pauses are activated in a reaction if they are executed and not killed until the end of the reaction. Because Esterel has parallelism, there can be multiple active and activated statements inside a program: all active '1's and '@ 's are used to resume execution and some '1's and '@ 's are activated during the execution (possibly the same ones).
There are two kinds of state semantics: the start semantics for untagged statements used when we start execution and the resumption semantics for active states used when we resume execution. We distinguish them by subscripts.
Remark 3. These two semantics correspond respectively to the execution of the surface and depth of the corresponding circuit, as described in [Ber03]. These notions are important in practice when handling loops: to get a working circuit, we need to duplicate the surface of the loop's body in a non-trivial way.
To define these constructive state semantics, we need to extend Must and Can to states. One easy way to do this is to use an expansion function  removing the already executed parts of a state, thus translating a statê into its corresponding statement in the constructive semantics (see Section 7.4.2 for a complete definition). Then, let Must(̂ , ) be Must((̂ ), ) and similarly for Can, so that we can directly reuse all the already proved properties about Must and Can and have for free the following equivalences which are required in the equivalence proof between the constructive semantics and the constructive state semantics, presented in Section 7.2: We also need to extend the function on terms. Keeping the same intuition of killing the derivative if the completion code is not 1, we get: However, unlike the constructive semantics, we need to use it only for the | statement. Indeed, parallel statements are the only place where an active state may need to be killed, whenever a branch pauses and the other one raises a trap.
Remark 4. In Kernel Esterel, killing pausing branches within a term raising a trap can be done from two different places: either by a trap statement catching its exits and killing its body, or by a parallel statement in which one branch pauses and the other one raises an upper trap. The first solution is the one originally presented in [Ber03] but the one implemented in Esterel compilers is the second one because it gives better digital circuits. 10 The rules of the state semantics are given in Fig. 3 for the start semantics rules and in Fig. 4 for the resumption semantics rules.
Remark 5. The transformation done to turn the constructive semantics into the constructive state semantics can also be done on the logical semantics, yielding a logical state semantics as done in [Ber03]. The only difference with the constructive version would be the local signal rules. See Appendix A.3 for details.  Finally, we can now prove that our initial idea of preserving the underlying statement actually works. Let us define an erasing function  converting a state or term into its untagged underlying statement, which amounts to erasing active tags by turning all active "1"s and "@ "s into inactive ones. Then, the following lemma holds: Lemma 6 (Invariance of the base statement). For all , , Being a rewording of the constructive semantics, the state semantics enjoys the same properties, in particular the state start and resumption semantics are deterministic.
Going beyond a state In the circuit translation of [Ber03], the state semantics provides a perfect match between stateŝ and active circuit states at the end of a clock cycle, that is, those in which at least one register is 1. We can extend this correspondence to untagged statements and inactive circuits. In particular, the registers in the circuit exactly correspond to "pause", "await immediate " and "suspend when " statements. Nevertheless, the computation of semantics states is abstract: we go from one state to the next, without explaining precisely how information flows between these states. Furthermore, the state semantics is still using recursively the Must and Can functions to compute the statuses of local signals. This is very different from the computation of wire values in digital circuits: instead of performing a two-step recursive evaluation using Must/Can, a digital circuit propagates electrical values in a forward way, following causality chains.
To solve these issues, we now introduce the microstep semantics, detailing how computation works within an instant as a sequence of microsteps, implementing a progressive evolution from a state to the next. This is the semantics equivalence of the propagation of electrical fronts in a digital circuit, which is internally asynchronous but where each step and the full reaction have predicable time.

Microstep Semantics
With the microstep semantics, our goal is to have an Esterel semantics as precise as the generated circuit, meaning that its resolution should be (roughly) at the gate level, and that it should avoid the mutually recursive definitions of Must and Can. Furthermore, we want it to be defined directly on the source code, so that the equivalence with the previous semantics is easier to express. Because of that, like the state semantics, the microstep semantics tags Esterel programs and execution consists in moving tags. Like digital circuits in which electricity propagates within a clock cycle, we restrict the microstep semantics to a single reaction, meaning that there will be no rule to cross an electrical register (either an explicit one as in 1, or an implicit one as in @ or ⊃ ), and that execution is performed starting either from the boot of the generated circuit (in the starting instant) or from active "pause" or "await immediate " statements (in resumption instants) to either termination or reaching an activated "pause" or "await immediate " statement. This matches the Register Transfer Level (RTL) evaluation in circuit design. [PBEB07] but still using the Can function which completely disappears here.

Remark 6. An attempt to formalize a microstep semantics was done in Compiling Esterel
Caveat The microstep semantics does not handle loops yet, so as not to worry about the schizophrenia problem caused by instantaneous reincarnation of signal statements by loops, in different signal environments, solved in practice by physical duplication of statement surfaces [OT04]. All the previous results are correct for the full language of Kernel Esterel, but from this point on, we no longer consider loops. Although the rules for loops in the microstep semantics are trivial, the proof of semantics preservation is definitely not! Complete handling of loops with reincarnation is left for future work.
The schizophrenia problem [Ber03,OT04] comes from the instantaneous restarting of loops when their body terminates: during an instant in which a loop terminates, two instances of the loop body are executed: the one that terminates and the one that starts. In terms of circuits, this means that we should execute twice the same circuit, the body of the loop, which is undoable in the current technology. It becomes doable by duplicating some gates and wires. This problem is particularly acute with local signals declared within the body of the loop because they may take different values on both iterations, meaning that the same syntactic definition in the program may take two different values. The current solution to this problem is code or gate duplication. It may result in an exponential blowup in size if done naively, but can actually be done in practice without register duplication and with an expansion factor of the circuit combinational logic at worst quadratic and most often linear. This is done in the Esterel v5 and v7 compilers.

Microstate Definition
Relation with the circuit translation The core idea in designing the tags propagated by the microsteps is taken from a simplification of the circuit translation of [Ber03]. Actually, the microstep semantics can be seen as a simulation of this circuit translation on top of the Kernel Esterel statements. As Kernel Esterel does not feature data, the key point is to transfer control. In the circuit translation, this is done through a structural translation respecting the circuit interface depicted in Figure 5. • input and output events for signals ( and ′ respectively); • four inputs wires (Go, Res, Susp, Kill); • a finite number of outputs wires (Sel and the K ).
All are single wires except for and ′ which are bundles of wires (one per signal). Their meaning is as follows: • Go is set to start the execution of the (currently inactive) circuit; • Res (for Resume) is set to continue execution of the (currently active) circuit; • Susp (for Suspend) is set to freeze the circuit registers for the current instant; • Kill is used to reset the circuit into its inactive state, that is, reset all registers to 0; • Sel represents whether the circuit is active or not, that is, whether one of its register is 1 in a state; • the K represent the completion code in one-hot encoding: completion code is represented by wire K being one and all other wires K ( ≠ ) being zero.
Among these wires of the circuit translation of [Ber03], only the Go and Res ones are used to propagate control within the instant while the Susp and Kill wires are only used as state register inputs, thus never to emit a signal or compute a completion code. Therefore, the effect of the latter will only become visible at the next instant, not the current one. In our semantics, the same effect will be obtained by the use of auxiliary functions (see Section 6.2), which makes it possible to omit the Susp and Kill wires. The Sel wire denotes which parts of a circuit are active, implementing the⋅ tag of the state semantics. We must keep it because it is used in control propagation in ;̂ . Since its value does not evolve during an instant, we implement its effect at the start of each instant, independently of the circuit's control or signal inputs.
Remember that a statement can only return one integer completion code; here it is technically simpler to encode this integer by the one-hot encoding represented by the K . This is a classical technique in circuits.

Microstate Interface
From the previous analysis, we design a microstate interface to annotate the source command : the notation is ◪ ◑ defined as follows.
Inputs ◪ consist of the Go and Res wires (as constructive Booleans that can take values ⊥, +, or −); signals are read from an (external) event but no output event ′ is produced (instead it will be read off the evaluated microstate); outputs ◑ consist in the completion code represented as either • with an integer, meaning that wire K is 1 and all other wires are 0, or ⚪ with a finite set of integers, meaning that wires K with ∈ are ⊥ and all other wires are 0 (and in particular, no wire is 1). This completion code representation directly denotes the 1-hot encoding, thus avoiding maintaining it as an invariant or dealing with impossible cases.
In fact, • represents the fact that the -th wire is + (Must propagation) whereas ⚪ represents a finite set of completion code wires whose value is still unknown, the others being − (Can propagation). The information about Sel is assumed to be already known so we do not need to consider the ⊥ case and can use a straight Boolean. We use the ⚪ ⧵ notation to denote setting wire to 0 inside ⚪ instead of the more standard but more cumbersome ⚪ ⧵{ } .
These ◪ and ◑ annotations are called colors and are recursively inserted in the bodies and branches of compound microstates. For example, ⊃ becomes ◪( ⊃ (◪ ◑)) ◑. We usually drop parentheses when ambiguity can be resolved from the context. The formal definition of microstates is given in Fig. 6.

Notations We color inputs as follows to have a visual representation of the various values of Go, Res
and Sel (whether the square is filled or not). When we have Sel − (that is, in the □, □, and □ cases), Theorem 11 will formally justify that the values of Res is irrelevant. Similarly, an invariant of the circuit translation is that we will never have Go + and Sel + at the same time as we can only start an inactive statement. Thus, the "?" for Go in the last three cases are actually either ⊥ or − but they cannot be +. Notice that Go − contains more information than Go ⊥ which makes a difference for some microstates. For example, the starting output color of1 is ⚪ {0,1} and it may become ⚪ {0} (that is, its K1 wire is set to 0) only when we have Go − because Go is directly fed into the K1 wire. We define two colored input notations as convenient shorthands for several cases: Figure 6: Definition of microstates • ◪: either □ or ■, that is, + ∨ (

Colors Sel Go Res Intuition
The intuition is that the microstate is executed, either started fresh (if inactive) or resumed (if active).
We let in( ), out( ), ( ), and ( ) denote respectively the input color, output color, Go wire, and Res wire of a microstate . To change the input color of a microstate into ◪, we write [◪] . We extend this notation to single wires: . For a signal , we define ( ) to be the value of in if ∈ and ⊥ otherwise.

Intuition of the Microstep Semantics
A synchronous digital circuit works by propagating electric potentials through wires and logical gates until all wires get a stable 0 or 1 value. Similarly, our microstep semantics works by propagating control information through Esterel statements until reaching some maximal state of information, that is, a state where all Go and Res wires are no longer ⊥ and where all completion codes are either ⚪ ∅ (no execution this no completion code) or • for some integer (executed and returning completion code ). After the microstep execution chain completes, the resulting statê ′ can be read off this maximal state of information. This state is unique as we prove the microstep semantics to be confluent (Thm9). To measure information and account for its propagation, we use Scott ordering that we define now.

Scott ordering on microstate The Scott order ≤ between two microstates and intuitively
means that contains no more information (is no more defined) than . It is defined recursively, by requiring that and have the same base statement and Sel values and that any input or output color in is no larger (contains no more information) than its corresponding one in . On input colors, we use a component-wise ordering of the constructive Booleans Go and Res (that is, ⊥ < + and ⊥ < −).
The definition of Scott ordering on output colors stems from the intuition that • (resp. ⚪ ) represents the fact that Must is (resp. Can is ).
with more information, more wires are set to 0 ⚪ ≤ • := ∈ the wire to 1 must be among the ones that are not 0 • ≤ • := = only a single wire can be 1 • ≤ ⚪ := False • cannot contain less information than ⚪ We require the Sel values to be the same to enforce that ≤ entails that and have the same starting term, in particular the same base statement. Indeed, on microstates from different terms or different instants, the information available in both has no reason to be compatible and the comparison is not meaningful.
We define a total microstate as a microstate where the information is maximal, that is, no input color still contains ⊥ and all output colors are either ⚪ ∅ or • for some .

Connection between states and microstates
The microstep semantics can be connected to the state semantics as follows: starting from a term (that is, an inactive statement or an active statê ) we build a starting microstate representing the state of computation at the beginning of the instant. Then, after setting its input color, we let the microstep semantics make this microstate evolve until reaching maximal information. Finally, we convert back the final state into a term. This is shown on Fig. 7, where dashed arrows are function application and full arrows represent the microstep semantics.
The difference between from_stmt and from_state only lies in how Sel is computed: in from_stmt, it is always set to − whereas in a state the active parts have Sel + . In particular, the overall structure is the same (the one of ) and the output colors are also identical. These output colors represent the statically-computed possible completion codes for each statement and sub-statement and thus, give the number of completion wires in the final circuit. Notice that these from_stmt and from_state functions perform the computation of the Sel wire. Figure 7: Links between the state and microstep semantics The to_term function converts back a microstate into a term. It is well-defined only for microstates with maximal information, since otherwise we do not know which parts are active or not (e.g., □ • 1 should become1 whereas □ ⚪ ∅ should become 1, so that we cannot translate ◪ ◑ in a meaningful way). It also performs the purpose of the Susp and Kill wires of [Ber03] by either freezing subterms (that is, reverting back to the state at the beginning of the instant) or killing a pausing parallel branch (that is, replacing it with its base statement) whenever the other branch raises a trap.
Unlike the previous semantics, the microstep semantics does not produce a completion code nor an output event ′ . Although this would be technically possible, it is of little practical interest because microsteps are too fine-grained. Indeed, in most microstep rules, the output event and the completion code are undefined, that is, all signals would have status ⊥ and the completion code would also be ⊥. Furthermore, the completion code and the output event ′ can be read off the final (and total) microstate. The completion code is simply given by the output color and the output event is computed by the function to_event by scanning the emit statements of the microstate: any ◪! • 0 gives + , whereas if all emitters of are ◪! ⚪ ∅ , its status is − . Finally, if there is no ◪! • 0 and some emitter with a non-total output color (that is, some ◪! ⚪ {0} , then the status of is ⊥). (For ◪! • 0 and ◪! ⚪ ∅ , we can actually prove that the input color is more precise, either □ or □, but we do not need it.)

Formal Definition of the Microstep Semantics
The full semantics contains a lot of rules (over 50). As such, the complete definition is given in Appendix 6 and we only give here their general construction on atomic and compound microstates, as well as a few illustrating examples. We think that providing such intuition and examples will be enough to convey the underlying key ideas.

Elementary microstates
The statement "nothing", "pause", "emit ", and "exit " only have input and output colors. Thus, their microstep rules simply compute their output color depending on their input color.
Example: the rules The "nothing" statement being instantaneous, we know that Sel is always false and that in the circuit translation only the Go wire is useful (and actually represented). Thus, the only possible input colors are □, □ and □. If the statement is started (that is, the input is □), we execute the statement. If the statement is not started (that is, the input is □), we do not execute it. Otherwise, the statement is neither executed nor not-executed (that is, the input is □, or in the circuit translation the Go wire is ⊥) and no rule applies. The cases of emit and exit are identical and are omitted here.
Example: the rules If the pause statement is started, that is, (◪) + , then the output should be • 1 . In order to trigger this rule only when it increases information, we add the precondition ◑ < • 1 .
Remark: Thanks to the absence of loops, the invariant ensuring that Sel and Go cannot be true at the same time entails that (◪) + actually means □. We use the former version because the circuit is (rightfully) not checking Sel and because the introduction of loops will break this invariant forcing us to use (◪) + anyway.
If the pause statement is not started, then its completion code cannot be 1: Similarly, for Res, we have: (Recall that ■ means + ∧ + , which entails that Go cannot be + thanks to the absence of loops.)

Compound microstates
Compound microstates contain input and output colors and some sub-microstates. Their microstep rules are split into three parts 11 : • a start part which propagates control: it converts the input color of the compound microstate into input colors for its sub-microstates; • a context part where sub-microstates evolve on their own; • an end part where the output colors of sub-microstates are combined into an output color for the compound microstate.
The level of details we want to reach is roughly the gate level, but not always. More precisely, we want to express the functional dependency of each wire on the values of other wires, without being tied to a particular implementation. For instance, in ⊃ , the Susp wire of is computed from the Susp, Sel, Res wires and the status of , but not necessarily by two AND gates and an OR one, as the original circuit implementation does [Ber03]. This allows to try other implementations without changing the specification.
Example: the ? , rules The distinction between start, context and end rules is obvious here, see Figure 8. The start part contains two AND gates (one for and one for ), and the end part contains a bunch of OR gates for the K . (Remember that we ignore the computation of Sel.) The start rules for merely propagate the Res wire from ? , to : The use of preconditions containing < ensures that a rule can only be triggered if it increases information inside the microstate. The statement is started ( ( ) = +) if the overall statement is started ( ( ? , ) = +) and is present ( ( ) = +). More generally, ( ) is the conjunction of ( ? , ) and ( ). The start rules for (not shown) are identical, except that we negate the value of in the rule for Go: ( ) becomes ¬ ( ).
The context rules are no problem and the end rule combines the completion codes of and by taking their union.

Properties of the Microstep Semantics
The microstep semantics enjoys most of the properties of other Kernel Esterel semantics: Theorem 7. The microstep semantics enjoys the following properties: • The base statement and Sel values do not change along execution: • The input color does not change along execution: Corollary: Total microstates cannot execute; • The execution in a microstep is local, that is, execution either happens in a sub-microstate or in the output color: • Microstates are compatible with < (and ≤) on input colors: Since there is no output event ′ , there is no event domain preservation.

Determinism and Confluence
The main property that we lose is determinism because microsteps are local and there can be several such execution steps possible. Nevertheless, we have the next best result: confluence and termination. While termination can be readily proven for any microstate, we need some well-formation invariants for confluence. Indeed, the (non-sensical) microstate " ? □ 0 ⚪ {0} , □ 1 ⚪ {1} " can produce output color • 0 and • 1 depending on which branch we execute, and cannot be made confluent.
Definition 1 (valid_coloring( , ) invariant). The property valid_coloring( , ) expresses that the input and output colors inside microstate are coherent with the information they have access to, as well as checks that all signals used in are declared in . For instance, the output of an AND gate cannot contain more information than the Scott conjunction of its inputs. Its definition, deferred to Appendix A.1, is made by induction over the statement, following the circuit translation.
Theorem 8 (Invariant of the circuit translation). The invariant valid_coloring( , ) is satisfied by the conversion functions from_stmt and from_state (the initial microstates) and are preserved by microstep execution. This entails the following properties: • This invariant is compatible with information increase about signals: • Control is never created, only propagated: • Branches in a test and a sequence are not simultaneously active: • A well-formed microstate contains more information than its starting version: _ _ is a fonction mapping a microstate to the term it started from.
Theorem 9 (Confluence and termination). The microstep semantics is terminating and locally confluent (from any well-formed starting microstate). By Newman's lemma [Hue80], it is then confluent (from any well-formed starting microstate).
Proof. Local confluence is proved by case analysis (280 cases to consider) and termination is proved by exhibiting a termination measure (the amount of missing information in a microstate).
Results about particular execution paths Using our microstep semantics, we can prove properties of execution paths depending on input colors, such as the following two results.
Lemma 10 (Execution of non-executed microstates). A non-executed microstate gets output color ⚪ ∅ . Formally, for all , ◑ and : • For ■ (that is, when Sel + ), we merely have ■ ◑ ← ← ← ← ← ← ← ← ← → * ■ ′ ⚪ , as the Go value may be required to eliminate some completion codes (e.g., 1 for pause). If we additionnaly have Go − , then we recover This property is the (partial) converse of the fact that control is never created, only propagated. If we denote by ≡ the equality of microstates up to Res wires, we can write it: The disjunction can be understood as follows: either the step in 1 computed a Res wire, in which case we have ′ 1 ≡ 1 ≡ 2 (left disjunct), or it computed something else and 2 must mimic it (right disjunct).

The Coq theorems and their proofs
This section expands on the Coq formalization and proofs, and how they depart from or expands on the results presented in the previous sections.
The structure of the Coq development This article is accompanied by a Coq development, whose structure is the following: • The main directory contains the definition of Kernel Esterel (Definitions.v and Semantics.v); • The Util/ subdirectory contains all the preliminary tools required for defining the semantics; • The Semantics/ subdirectory contains the various Esterel semantics; • The Proofs/ subdirectory contains proofs about the semantics, in particular the equivalence/refinement between semantics, and the invariants satified by the microstates.
For a more detailed description, see the README.txt file at the root of the Coq archive. As the semantics are described in Coq by inductive types, their relation are proved by induction, enumerating cases to go from one to the other. The overall connections between these semantics is depicted on Figure 9.

Representation choices in Coq
In the Coq formalization, we have tried to stick as much as possible to the symbolic writing of Kernel Esterel, but still had to depart slightly from it on the | and * cases for technical reasons. Indeed, the single pipe | is used in Coq for pattern matching so that we use instead the textual notation || for parallel composition. Similarly, the star is used to type pairs and we use instead for loops. (Furthermore, the star notation was inspired from Kleene's star which is written as a superscript and our version looks more natural in this respect.) The fact that and ′ are maps from signals in scope to statuses makes it possible to prove that the set of visible signals is not modified along execution (see property "Domain invariance" in Section 7.3). This is different from the presentation of [Ber03] where ′ is a set of emitted signals, which amounts to the set of signals mapped to + in our representation. Borrowing standard notation for lists, extending an event by mapping the signal to status (with possible overshadowing of a previous signal ) is written ++ rather than * , again because * is already used for Cartesian product and multiplication. When writing a Kernel Esterel program, there are implicit well-formation rules. For instance, it is not allowed to emit or read a signal that is not in scope. In compiler implementations, this is ensured by typing checks. Here, all semantic rules using signals ensure this property with a premise that implies that is in scope, that is, that ∈ . Signals are represented by a setoid, that is, a set equipped with a dedicated equality. In particular, signals do not use the equality of Coq. The downside of this choice is that every semantics should have an extra rule ensuring compatibility with this equality. In particular, the inversion tactic is no longer useful as this compatibility case always applies. Nevertheless, it is rather straightforward to prove dedicated inversion lemmas and write a tactic mimicking inversion. The benefit of this choice is that we can use extensional equality for events and we can optimize signal expressions (which are currently left out of the formalization for simplicity): instead of structural equality, we can choose propositional equality. Another solution would have been to use Coq equality for everything (signals, events, statements and so on) and add axioms ensuring that this equality is extensional on events.
Finally, as the microstep semantics does not handle loops, we need to either remove them entirely or have two versions of Kernel Esterel. For consistency of the whole body of proofs, we choose to remove loops but the associated definitions and proofs are still present in the Coq proofs, only commented out. This way, should one want to play with the early semantics (logical, constructive and constructive state semantics) including loops, it would merely be a matter of uncommenting these proof parts.
Apart from the slight variations presented in Section 7.1, the Coq representation of these semantics exactly follows the earlier presentation of Section 3 and Section 4.

Definitions of Esterel semantics in Coq
The constructive semantics The constructive semantics rely on the Must and Can functions. There are two small differences between their presentation in Section 4 and their Coq description. First, as we know that Must ( , ) is either a singleton or the empty set, it is more convenient to use an option type to enforce this invariant: in Coq, Must ( , ) is either Some for some ∈ ℕ or None. Second, the tag carried by Can ( , ) to express whether must be evaluated or not can take values + (surely executed), ⊥ (maybe executed), and − (surely not executed). Nevertheless, only values + and ⊥ are actually used so we use instead a Boolean with true representing + and false representing ⊥. The microstep semantics Compared to Figure 6, the Coq development separates the sel Boolean from the input color, in order to ensure by construction that it cannot change. The rest is faithful to Figure 6.

The constructive state semantics
As the refinement proof between the constructive state semantics and the microstep semantics requires several steps of the microstep semantics, we also introduce its reflexive transitive closure, written ← ← ← ← ← ← ← ← ← → * ′ . To connect the constructive state semantics and the microstep semantics, we define functions from_stmt and from_state converting respectively a statement and a state into a microstate, and functions to_term and to_event converting a microstate to respectively terms and events. As a microstate does not contain information about suspension, to_term must take the input event in order to decide whether a suspension is triggered or not. A different solution could be to add a Susp component to the control part of input colors tracking the value of the Susp wire in the circuit translation of [Ber03].

Properties of Esterel semantics
Shared properties of many semantics Most semantics satisfies a common body of properties, inherent to the Kernel Esterel language. These properties are presented below only for the constructive semantics but can be adapted to other semantics in a straightforward way:

Domain invariance
The domain of the input event and the output event ′ are the same: Determinism The semantics is deterministic: Notice that this property is wrong for the logical semantics! For example, the program ( ? ! , 0)∖ seen at the end of Section 3 is non-deterministic. The microstep semantics is also non-deterministic because execution can happen in various places of a microstate. Nevertheless, it is confluent so that in practice this non-determinism does not matter much.
Inactive derivative If the completion code is not 1, then the derivative is 0: This result means that if a statement is not pausing, then its execution has finished (either by normal termination or raising an exit). This result is the motivation for introducing the ( , ) function.
Total output Output events are always total, that is, they contains only mappings to + or − and none to ⊥. (This is trivially true for the logical semantics, as there is no ⊥ involved.) This property does not make sense for the microstep semantics as there is no output event.
Underlying statement invariance The underlying statement does not change along execution: Of course, not all properties are shared between all semantics, some properties are still specific to each semantics. For example, the result about inactive derivatives can be strengthened into an equivalence for the constructive state semantics and the microstep semantics, as the derivative of pause is no longer an inactive statement but the active state1.
For all , , ′ , , and ′ , if̂  ′ , An overview of which property are satisfied by which semantics is given on Table 1.

Between the logical and constructive semantics
The constructive semantics is a refinement of the logical one by casting out some unwanted behaviors due to non-causality. Therefore, we expect to have a theorem stating that any valid transition in the constructive semantics is also valid in the logical one. Before stating this theorem, we need to convert constructive events into classical ones, by a function C2K. Because of the status ⊥, there is no canonical way to do so. Therefore, we choose to restrict the equivalence theorem to total (constructive) events, i.e. to constructive events in which no signal is mapped to ⊥. Thus the precise statement we prove is the following: Remark 7. As we already know that the constructive semantics produces total output events, we could replace ( ′ ) with ′ . In Coq, it is still required for typing reasons: in the constructive setting, ′ could take associate value ⊥ whereas this is impossible in the classical setting.
Proof of Theorem 13. By induction on the proof of  ′ , As both semantics are the same except for signal declaration, only the Sig + and Sig − rules are interesting; the other ones simply amounts to using expected properties of C2K. These two cases rely on Lemma 4 (reproduced below for convenience) which expresses that the functions Must and Can indeed compute what their names imply: any signal (resp. completion code) computed by Must( , ) is indeed emitted (resp. reached) and any emitted signal or reached completion code indeed belongs to the corresponding set computed by Can + ( , ).
The interesting cases are sequential composition and signal declaration. Looking at Must and Can definitions, we may also expect the presence test case to be difficult but the induction hypothesis gives either + ∈ or − ∈ and therefore we only need an application of the induction hypothesis to conclude. Both the ; and ∖ cases use case distinctions according to the definitions of Must and Can. They also requires monotonicity of Must and antimonotonicity of Can, stated below. For instance, the third case of Can ( ; , ) uses Can ⊥ ( , ) whereas the induction hypothesis gives us Can + ( , ). Therefore we need the inclusion Can + ( , ) ⊆ Can ⊥ ( , ) to conclude. Similarly, in ∖ , the case distinction gives results about * ⊥ whereas we may need them about * + or * − . We need again inclusions, here Must( , * ⊥ ) ⊆ Must( , * + ) and Must( , * ⊥ ) ⊆ Must( , * − ).
Lemma 14 (Monotonicity of Must and antimonotonicity of Can). For all ≤ ′ , we have: If we define inclusion on pairs by pointwise inclusion, we can write it in a more compact form: Must( , ) ⊆ Must( , ′ ) and Can + ( , ′ ) ⊆ Can ⊥ ( , ).
Proof. The proof of this statement is done by induction over . It is straightforward but very tedious because we have to prove all four statements at once due to mutual dependence. The most troublesome case is by far the signal declaration one because of the many case distinctions required.

Between the constructive semantics and the constructive state semantics
Comparing the constructive semantics and the state one is more subtle because the meaning of the derivative ′ changes: in the constructive semantics, it represents "what is left to execute inside " whereas in the state semantics, the underlying statement never changes. Therefore, we need to express "what is left to execute" inside a state. Following [Ber03], we define the expansion (written ) of a statê into a statement, erasing the already executed parts to return the parts that still need to be executed insidê .
This function is extended to terms by setting ( ) = 0: in an inactive statement, nothing is pending execution.
Remark 8. For thê | and |̂ cases, keeping the seemingly useless 0 | _ is actually technically essential to avoid a mismatch between the derivative of both semantics. Indeed, this simplify the equivalence between the construtive and state semantics by avoiding the need for bisimulation.
With this expansion function, we can state the equivalence between the constructive semantics and the constructive state semantics as follows: Theorem 15 (Equivalence between the constructive and state semantics).
Proof. The proofs of these four implications all go by induction on the derivation tree in the source semantics. They are straightforward, they simply require to match the source semantics rules either by case distinction on ′ and to insert the adequate ( , ′ ) or through the fact that adding other ( , _) inside a ( , ′ ) does not change the statement.

Between the constructive state semantics and the microstep semantics
In order to reduce the proof burden, some parts of the circuit are left abstract in the microstep semantics, namely the computation of signal values and the synchronizer for the parallel statement. In the first case, it amounts to a big OR gate over the Go component of the input color of all emitters. In the second case, we work with the specification of the synchronizer rather than a given implementation, thus permitting to reason about what it should do and allowing us to swap and compare implementations. Unlike the previous semantics which tackle reactions, the microstep one deals with steps within one reaction. This discrepancy makes it harder to relate both semantics because the microstep semantics is much more precise and thus can distinguish states that cannot be expressed in the state semantics and whose translations in the state semantics are identical. Nevertheless, the biggest trouble when connecting the constructive state semantics and the microstep semantics comes from the Can and Must functions.
The Can/Must functions The state semantics uses the auxiliary functions Can and Must to compute the value of a local signal then performs the evaluation using this value. Thus, the body of the statement is evaluated twice: first partially to get the value of the local signal and later from scratch again to compute the full step using the value of the local signal. On the opposite, in the microstep semantics, once the value of the local signal is computed, we continue the evaluation of the microstate using this value without restarting from scratch, exactly like what the circuit does. This is the main difference with the microstep semantics presented in the Compiling Esterel book [PBEB07].
Therefore, for the simulation we need to translate the condition for applying a rule for local signals, ∈ Must ( , ) or ∉ Can + ( , ), into the corresponding condition in the microstep semantics, that is: there exists a microstep sequence ← ← ← ← ← ← ← ← ← → * ′ for some ′ emitting or some ′ surely not emitting it. This is actually the hardest part about the simulation proof, which makes sense as it is also an essential difference between the semantics. Because the definitions of Must and Can are mutually recursive with recursive calls for ; requiring information about completion codes and recursive calls for ? , changing the tag + or ⊥ on Can, we actually need six mutually recursive properties: three for signals and three for completion codes.

Lemma 16 (Interpretation of Must/Can as microsteps).
For any statement and any event containing all signals used by 12 , we have the following properties: where out2C is a function converting an output color to a set of completion codes, defined by out2C(• ) = { } and out2C(⚪ ) = .
Six similar properties hold when resuming an active state rather than starting an inactive statement.
Finally, we can prove the simulation theorem: any step in the constructive state semantics can be performed by a sequence of steps in the microstep semantics. Furthermore, the final microstate is total and produces the same completion code and the same output event: Proof. The proof amounts to finding an evaluation order leading from the state at the beginning of the instant to the one at the end of the instant. This order corresponds to input-to-output evaluation in circuits: first uses start rules, then context ones 13 , and finally end ones. Lemma 16 is critical for the ∖ case.
Notice that this theorem, unlike most others, is not an equivalence between the semantics, only a simulation. The converse direction cannot hold because the microstep semantics is local whereas the state one is global. For example, if we take a valid statement and a non constructive one (say, ( ? 0 , ! )∖ ), then | cannot execute under the state semantics whereas the microstep one can execute independently of , so that the final microstate would correspond to some ′ | in the state semantics.

Interpreters
For all semantics, we have defined interpreters and proven their correctness and completeness. These interpreters can be used as an executable semantics of Kernel Esterel programs. They take as inputs a program (either as a statement, a state, or a microstate depending on the interpreter) and an input event; they output either nothing (when the input program cannot execute) or the output event, completion code and derivative of a possible execution step.
As an illustration, below is the correctness statement for the constructive semantics. The same type of result holds for both variants (start and resumption) of the constructive state semantics.
Proof. All such proofs are straighfoward (if sometimes long) and follow the structure of the interpreter or of the semantics in the premise.
Since the microstep semantics may execute in several parts of a microstate, we need to choose an evaluation order (even though the actual order does not matter because of confluence). We use the start-context-end one: first start rules, then context rules, then end rules. Thus, the completeness result no longer holds (one could pick a different order that the interpreter does not follow) but instead we have a weaker result: if a microstep execution step is possible, then the interpreter is not stuck.
Lemma 19 (Correctness and partial completeness of the microstep interpreter).
We can recover a complete interpreter by using the iterated microstep semantics, that is, the reflexive transitive closure of the microstep semantics. Then, all microstate can execute (at least to themselves) so we can drop the option type and have a simpler correctness statement: Confluence ensures that this is the final state of any execution chain starting from . Finally, the interpreter for the logical semantics is only correct but not complete as the logical semantics is non deterministic and non confluent. Indeed, given a statement that can non deterministically pause or terminate and a statement that cannot execute, then on ; the interpreter will choose to make terminate and fail to execute making the overall ; statement non executable. On the contrary, the LBS semantics allows to pause, which results in a valid reaction as is not considered. For instance, one may take to be ( ? ! , 1)∖ and to be ( ? 0 , ! )∖ .
It would be possible to create a complete interpreter for the LBS semantics by returning the set of possible executions instead of just choosing one but this seems to be of little practical interest as the LBS semantics is not a very useful one.

Conclusion and future work
This paper has presented a new work on the Coq-based formal verification of the Kernel Esterel semantics chain presented in the web draft book [Ber03] written by the second author 20 years ago, augmented by the definition of a new fine-grain operational semantics developed and formally verified by the first author. Unlike the coarser-grain operation semantics introduced by Dumitru Potop in [PBEB07], this new operational semantics closely mimics the circuit translation introduced in [Ber03], which was the basis of both the academic Esterel v5 compiler to C and the industrial compiler Esterel 7 compiler to hardware circuits or software code. Its main advantage compared to circuits is its SOS inductive logical rules presentation, which makes the formal proof of its adequacy vs. the constructive semantics much simpler with current Coq technology.
Let us present a short history of this work. When he completed the book [Ber03], the second author did not even include sketches of correctness proofs, this for two reasons. First, he was completely involved in the industrial development and applications of the Esterel v7 compiler, which handles a much more expressive and modular language than v5. The v7 language and compiler have been successfully used by several hardware and software companies, before being taken over by Synopsys (they are not available any more). Second, he thought that only machine-checked correctness proofs would be fully convincing. Second, the formal verifiers were not yet mastered enough in the beginning of the 2000's for such an endeavor.
The real game changer in the semantics/compiling field was the Coq-based construction and formal verification of the CompCert Coq-verified compiler by Xavier Leroy and his team [Ler19]. This large-scale work was itself inspired by the Coq-based formal proofs of major mathematical theorem by Gonthier and his team [GAA + 13] (Gonthier himself had played a major role in the early development of Esterel). Our formal proofs, technically developed by the first author, followed a similar track. No mistakes were found in the book's claims, although it did not even contain informal correctness proof as said before.
Nevertheless, it must be noted that this paper does not finish the job, for three reasons: first, it limits the kernel language to loop-free programs; second, the new operational semantics is not yet formally related to the Boolean circuits generation described in [Ber03], which is the heart of the v5 and v7 compilers. We briefly detail these points below. Third, but less importantly, we did not yet study the full Esterel language, which also supports data definitions and calculations. As shown by the way the v5 and v7 compilers handle data, this only require adding data dependencies to the signal dependency structure, which should raise no difficult issues.

Future work: statement and signal reincarnation
We chose to postpone the study of loops because they lead to a subtle phenomenon: statement and signal reincarnation. When embedded in possibly nested loop statements, a given Esterel statement can be reincarnated (i.e., re-executed) several times in the same instant, but in a clean way: a new incarnation can only occur when the previous one has terminated. Consequently, a locally scoped signal may take several simultaneous incarnation statuses in the same instant when its declaration is embedded in loops.
But these are taken in strict succession of scope entering and exiting, as are the reincarnations of its declaration statements; this makes only one signal incarnation status visible at a time in any statement. Thus, incarnations cannot interfere in a symmetric way. Reincarnation occurs naturally when programming, and raises no difficult problem in practice.
Three quite different technical solutions have been developed to deal with reincarnation. The first naive one consists in syntactically duplicating the body of each loop in an inside-out way, which completely suppresses reincarnation since Esterel requires that the body of a loop cannot terminate instantaneously. In * the loop body man terminate and be restarted at the same instant. But in ( ; ) * , since cannot terminate instantaneously, the first and second 's cannot be executed in the same instant. But this is trivial solution is impractical since inside-out copying may exponentially blow-up source code size.
In [Ber03], the second author used a more semantic way based on incarnation indices that tag in a unique way each occurrence of a given statement or signal in execution proof trees. Since restarting a statement can only execute its surface, i.e., the statements instantaneously reachable when starts, such indices only lead to worst-case proof tree and generated circuit sizes quadratic compared to the statement size. Furthermore, the size increase is quasi-linear in practice for most useful programs, which is not a problem.
In [TdS05], Tardieu introduced an alternative approach based on a semantically-guided partial syntactic duplication of statements, which copies the surfaces of source statements also in a worst-case and most often quasi-linear way. The price to pay is the addition of a gotopause statement, i.e. a goto statement limited to pause targets. Both approaches are compatible, since Tardieu's approach can also be viewed as a way of duplicating statements based on a static conservative calculation of possible incarnation indices.
It is not yet clear which approach should be preferred to complete our Coq-based verification. Incarnation indices have a simple and clean algebraic structure, which makes them easy to add to the current semantic rules. But the proofs will become heavier since they will require the addition of an extra decreasing incarnation index related ordinal. Tardieu's approach may look simpler at first glance, because the proof might require less changes, but it has another drawback: the addition of gotopause turns programs into dags, a structure not yet easy to manipulate with Coq.

Relating the operational semantics to the circuit translation
Let us now finally analyze the technical difficulty of relating SOS semantics to circuits. Intuitively, the circuit generated by an Esterel program by the translation of [Ber03] can be viewed as a folding of all possible proof trees of the new operational semantics into a single and possibly cyclic Boolean gates and wires graph (note that static cycles yield no dynamic electrical problems for constructive circuits, see [MSB12]). Registers implement pause statements, with value 1 when a pause is active in a given program state or 0 when it is inactive. Specific gate clusters represent operational semantics proof tree nodes, and specific wire groups represent proof tree branches, taking value sets that precisely encode the pre-and post-labels attached to statements in the new operational semantics. In theory, making formal this informal correspondence should raise no deep problem. But, as the saying goes: "In theory, theory and practice are the same; in practice there are not". The unfortunate practical problem is once again due to the fact that general graphs are currently difficult to formalize and handle in Coq.

A.1 Ancilliary definitions
The valid_dom( , ) predicate The valid_dom( , ) predicate expresses that all signals free in are in the domain of , thus making sure that the evaluation of is properly defined. The definition is made by a straightforward case analysis and amounts to requiring ∈ every time a signal is explicitly used, except for local signal declaration in which it is added to the domain of instead. See the Coq code for details.
The valid_coloring( , ) predicate The predicate valid_coloring( , ) represents the fact that microstates appearing along the evaluation of an Esterel program are not arbitrary: they satisfy some invariants comming from the circuit (the output value of a gate contains no more information then its input values allow) and from the Esterel translation itself (Sel and Go are exclusive and so are branches of a test or a sequence).
The set of constraints is given below. The interested reader is invited to look at the Coq code, which is more explicit and commented. For illustration purposes, we explain in detail the case ? , . In addition, all these cases also include input_invariant sel gr:= Go gr = OK true ⇒ sel = false (not displayed for clarity). Similarly, all compound statements have recursive call for all substatements which are not shown, except for the ∖ case.
The ? , case can be detailed and understood as follows: • the input color must satisfy its Esterel invariant: input_invariant ; • the signal must exist in the environment ; let be its value: ∈ ; • ? , is active iff one of and is: = ( )|| ( ); • both and cannot be active at the same time: • the rest of the input color is transmitted to and :

A.3 The State Semantics (LSS and CSS)
As described in Remark 5, a state semantics can also be defined for the the logical semantics. Just like for the behavioral semantics, we present both the constructive one and its logical countrerpart at once.
For convenience, we lift the statement and state notations to terms. For instance, this means that ? , is either the state ?̂ , or the statement ? , , depending on what is.
To stay in the spirit of the function, we define ( , ) as: ( , ) ∶= if = 1 (and in that case, is usually a statê ) if ≠ 1

A.3.1 The start rules
The inputs of start rules are programs and their outputs are terms. As for the behavioral semantics, this first body of rules is valid for both state semantics. Notice that unlike the behavioral semantics, we only need to insert a -function for | because in all other cases, the derivative is already inert (that is, it is a statement).