# Une sémantique de Kahn mécanisée pour les machines à états

Timothy Bourke, Paul Jeanmaire, Marc Pouzet

<figure><img src="image_1.png" /></figure>

To cite this version:

Timothy Bourke, Paul Jeanmaire, Marc Pouzet. Une sémantique de Kahn mécanisée pour les machines à états. JFLA 2026 – 37es Journées Francophones des Langages Applicatifs, Marie Kerjean; Yannick Zakowski, Jan 2026, Oberbronn, France. hal-05428043

HAL Id: hal-05428043

https://hal.science/hal-05428043v1

Submitted on 21 Dec 2025

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_2.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
# Une sémantique de Kahn mécanisée pour les machines à états

Timothy Bourke¹,², Paul Jeanmaire³ et Marc Pouzet²,¹

¹Inria Paris

²École Normale Supérieure, Université PSL

³LIP6, Sorbonne Université

Les machines à états hiérarchiques sont utilisées pour programmer des comportements séquentiels ou dépendants d'un mode d'opération. Dans les langages comme Lucid synchrone et Scade 6, elles se composent librement avec les opérateurs flot de données qui sont plus adaptés pour la programmation des filtres et autres algorithmes de l'automatique. Si l'on n'est pas préoccupé par la génération de code pour une exécution en temps et mémoire bornés, les machines à états peuvent être exprimées en termes de réseaux de Kahn récursifs ou, de façon équivalente, par la programmation fonctionnelle avec des flots paresseux. Dans cet article, nous étendons un développement en Rocq des réseaux de Kahn avec des définitions de machines à états, fournissant ainsi une sémantique fonctionnelle pour un langage flot de données ressemblant à un sous-ensemble de Scade 6.

## 1 Introduction

Les langages synchrones flot de données ont été conçus pour la programmation de systèmes de contrôles temps réel. Le fil directeur derrière la succession de langages Lustre [HCRP91], Lucid synchrone [CHP06a, Pou06], Scade 6 [CPP17] et Zélus [BP13] est de spécifier un système dans un langage purement fonctionnel et de générer du code qui s'exécute en temps et mémoire bornés. Un tel système évolue avec son environnement, sa spécification est donc faite autour de séquences qui modélisent les valeurs qui sont lues des capteurs, qui passent à travers ses composants et qui sont écrites aux actionneurs.

Alors que certains composants, comme les filtres et les compteurs, s'expriment naturellement avec les opérateurs sur les séquences, d'autres sont plus directement exprimables par des références explicites aux états et aux transitions. C'est la raison d'être des machines de Mealy [Mea55] et de leur extension aux Statecharts [Har87]. Les machines à états développées dans Lucid synchrone et intégrées dans Scade 6 [CPP05, CHP06b] permettent de mélanger librement les opérateurs sur les séquences et les spécifications modales.

La sémantique des langages synchrones flot de données avec machines à états a toujours été définie précisément, que ce soit par traduction dans un noyau simple [CPP05, §3], avec des règles opérationnelles [CHP06b, §4.1], ou par co-itération [CMPP23, §3]. La question qui nous intéresse ici est l'expression de cette sémantique dans un assistant de preuve. Elle a déjà été traitée dans le contexte d'un compilateur vérifié avec des règles relationnelles [BPP23a, BPP23b]. Nous proposons ici une nouvelle sémantique fonctionnelle, conçue comme une extension du modèle flot de données à la Kahn. Elle repose sur une formalisation en Rocq [Coq25] des ordres partiels complets pour formaliser les réseaux de Kahn [PM09] avec une modélisation explicite des erreurs [BJP25].
Dans notre sémantique, nous modélisons les machines à états avec des fonctions récursives sur des environnements associant variables aux séquences. Nous considérons les transitions fortes et faibles, pourvu qu'elles ne soient pas mélangées au sein d'une même machine à états, et les transitions avec ou sans histoire. En principe, nos définitions sont exécutables, mais en pratique leur réduction dans Rocq ou après extraction en OCaml est trop inefficace pour être utile. Ce travail est un premier pas vers le traitement des machines à états dans une sémantique fonctionnelle d'un compilateur vérifié [BJP25]. Il manque toujours une version synchrone de la sémantique, avec une modélisation explicite de l'absence d'une valeur à un instant, et les preuves de correspondance avec la sémantique relationnelle du compilateur.

## 2 Machines à états synchrones

Pour présenter les machines à états, nous reprendrons dans la figure 1 l'exemple typique d'un régulateur de vitesse automobile idéalisé. Ce programme comporte trois fonctions de flots, ou nœuds : patienter, régulateur et main. La définition d'un nœud combine une interface qui lui déclare un nom, des entrées et des sorties avec un ensemble d'équations mutuellement récursives qui définissent les valeurs des variables locales et de sortie.

Le nœud patienter décrit un compte à rebours à partir d'un flot en entrée v. Le compteur c est défini avec l'opérateur fby qui rend la première valeur du flot à gauche, v, puis le flot associé avec l'expression à droite, c ou c - 1 selon la valeur d'alarme. La sortie du nœud, alarme, devient vraie dès que le compteur tombe à zéro.

<table><tr><td>v</td><td>5</td><td>5</td><td>5</td><td>5</td><td>5</td><td>5</td><td>5</td></tr><tr><td>c</td><td>5</td><td>4</td><td>3</td><td>2</td><td>1</td><td>0</td><td>0</td></tr><tr><td>alarme</td><td>F</td><td>F</td><td>F</td><td>F</td><td>F</td><td>T</td><td>T</td></tr></table>

Le nœud régulateur implémente un algorithme de régulation de type « proportionnel-intégral » (PI). La différence point à point entre les deux flots en entrée, actuel et référence, est multipliée par la constante du gain proportionnel kp et additionnée avec sa propre accumulation dans la variable z multipliée par la constante du gain intégral ki pour calculer la sortie commande.

Ces deux nœuds sont ensuite utilisés dans main qui a cinq entrées de type bool, communiquant le statut des boutons autour d'un volant, et deux entrées de type double, communiquant la position de la pédale d'accélérateur et la vitesse du véhicule. Ce nœud est défini avec une machine à états, construction de bloc qui généralise l'idée d'une équation [CPP05, CHP06b]. Cette machine a deux états. Dans l'état Éteint, la variable gaz est simplement égale à l'entrée accélérateur. Dans l'état Allumé, elle est définie par une autre machine à états. Les transitions entre Éteint et Allumé sont déclarées avec until, qui indique qu'elles sont faibles : dans un instant donné les équations de l'état courant régissent les valeurs des variables et que les expressions de garde sont évaluées pour déterminer si l'état changera à l'instant suivant. Ici, l'état change quand allumer_éteindre est vrai.

La machine à états imbriquée a trois états. Elle débute en attendant qu'activer soit vrai pour ensuite passer dans un état de maintien automatique de vitesse. Cette fois, les transitions sont déclarées avec unless, indiquant qu'elles sont fortes. À un instant donné, les expressions de garde de l'état précédent sont évaluées pour déterminer si l'état change pour l'instant courant. À la différence d'autres formalismes, un seul état est actif à chaque instant, ce qui simplifie le calcul d'une borne sur le temps d'exécution. Si dans l'état Automatique, l'entrée annuler est vraie, la machine revient dans son état initial, sinon si l'entrée freiner est vraie, elle passe dans l'état Pause. Les transitions sont donc évaluées dans l'ordre et les machines à états sont ainsi déterministes. La première transition à partir de l'état Pause instancie le nœud patienter pour revenir à l'état initial après un délai. La deuxième retourne à l'état Automatique si réactiver est vrai. Le mot-clé continue indique que c'est fait avec histoire [Har87, §2], c'est à dire que contrairement aux transitions spécifiées avec then, les équations dans le nouvel état ne sont pas réinitialisées. Donc, si l'état Automatique est atteint
<figure><img src="image_3.png" /><figcaption>Figure 1. Exemple : un régulateur de vitesse idéalisé.</figcaption></figure>
à partir de *EnAttente*, la variable locale *vitesse_de_croisière* est fixée avec la valeur courante de *vitesse* et une nouvelle instance de *régulateur* commence, avec son accumulateur interne à zéro. Par contre, s'il est atteint à partir de *Pause*, *vitesse_de_croisière* garde sa valeur grâce au *fby* et l'instance de *régulateur* est inchangée. Le choix de ne pas réinitialiser *régulateur* est discutable car il y a un risque d'emballement. Supposons que le délai dans *Pause* suffit à le prévenir.

Le langage que nous considérons ne permet pas de mélanger les transitions fortes et faibles dans une même machine à états. C'est une simplification par rapport à Lucid synchrone et Scade 6. Par rapport à Lucid synchrone, nous ne traitons pas non plus les états paramétrés [Pou06, §1.7], qui auraient permis un traitement plus élégant de la *vitesse_de_croisière*.

Les *variables partagées* [CPP05] sont la dernière fonctionnalité des machines à états que nous prenons en compte dans notre formalisation. Les deux exemples ci-dessous définissent une variable *h* qui monte péniblement de 0 à 10 et puis descend plus rapidement jusqu'à 0 avant de recommencer ad infinitum.

<figure><img src="image_4.png" /></figure>

Dans l'exemple de gauche, *h* est déclarée comme une variable partagée en lui donnant une valeur « last » initiale. Cela permet d'utiliser l'expression *last h* pour faire référence à la dernière valeur de *h*. Dans l'exemple de droite, le même effet est obtenu en introduisant une nouvelle variable *last_h* définie par un *fby* à l'extérieur de la machine à états. La valeur précédente est ainsi partagée entre les deux états, ce qui n'aurait pas été le cas en mettant les équations $h = 0 \ fby$ ($h + 1$) et $h = 0 \ fby$ ($h - 2$) à l'intérieur. Mise à part la clarté apportée au code, l'avantage des variables partagées est qu'elles sont complétées implicitement. C'est à dire, si elles ne sont pas définies explicitement dans un état, elles gardent leur dernière valeur comme si l'on avait écrit, par exemple, $h = last \ h$.

Le mélange de ces différentes fonctionnalités au sein d'un même programme est susceptible d'introduire des comportements parfois compliqués. Leur sémantique est toutefois bien établie et fait l'objet de la section 4.

## 2.1 Syntaxe abstraite

Le langage que nous traitons est le sous-ensemble de Scade 6 accepté par le compilateur Vélus<fnref n="1" />. La classe des *expressions* est définie ci-dessous.

$$e ::= c \mid C \mid x \mid \mathit{last} \ x \mid \diamond e \mid e \oplus e \mid e^+ \mathit{fby} \ e^+ \mid e^+ \rightarrow e^+ \mid e^+ \mathit{when} \ C \ (x) \\ \mid \mathit{merge} \ x \ (C \Rightarrow e^+)^+ \mid \mathit{case} \ e \ \mathit{of} \ (C \Rightarrow e^+)^+ \\ \mid f \ (e^+) \mid (\mathit{reset} \ f \ \mathit{every} \ e) \ (e^+)$$

Elle inclut les constantes entières et virgules flottantes, les constantes de types énumérés, les variables, l'opérateur *last* appliqué à une variable, les opérateurs unaires et binaires,

<footnote n="1">1. https://velus.inria.fr</footnote>
les opérateurs flot de données (fby, ->, when, merge), les conditionnelles, les instances des fonctions et les instances des fonctions avec réinitialisation. Vélus s'imbrique avec CompCert [Ler09] et, par conséquent, la plupart des opérateurs unaires et binaires sont importés directement de Clight [BL09].

Après les expressions, les blocs incluent les équations, les déclarations des valeurs last initiales, les variables locales, la réinitialisation modulaire, les définitions par cas et les machines à états faibles et forts. La déclaration d'une variable spécifie son type (*ty*) et son type d'horloge (*ck*), mais ces détails importent peu ici.

```
blk ::= x⁺ = e⁺;
| last x = (c | C);
| var d⁺ let blk⁺ tel                  d ::= xᵢ
| reset blk⁺ every e                   autinits ::= C | if e then C else autinits
| switch e (C do blk⁺)⁺ end            autscope ::= var d⁺ do blk⁺ until trans⁺
| automaton initially autinits         trans ::= | e continue C | | e then C
  (state C autscope )⁺ end
| automaton initially C
  (state C do blk⁺ unless trans⁺)⁺ end
```

Un programme est une liste de déclarations de type énumérés et de nœuds.

```
td ::= type ty = ( | C )⁺
```

```
n ::= node f ( d⁺ ) returns ( d⁺ ) blk
```

Ce langage a déjà été formalisé dans Rocq avec une sémantique synchrone relationnelle [BPP23b]. Une sémantique fonctionnelle a aussi été définie pour les opérateurs flot de données [BJP25]. Le but dans la suite de cet article est de l'étendre aux autres constructions.

## 3 Sémantique flot de données en Rocq

Plusieurs facteurs motivent l'encodage d'une sémantique d'un langage dans un assistant de preuve comme Rocq. Cela permet d'abord d'énoncer et de démontrer la correction d'un compilateur, comme c'est le cas pour Vélus et CompCert. Une sémantique formelle peut également servir de support à un raisonnement interactif sur les programmes, ce qui, en combinaison avec la compilation vérifiée, permet d'obtenir des preuves de programmes de bout en bout avec des garanties sur le code assembleur généré. Bien que Vélus fournisse un modèle relationnel du langage, où les programmes sont représentés par une relation entre les flots d'entrée et les flots de sortie, le modèle fonctionnel de Kahn [Kah74] semble plus approprié pour le raisonnement interactif, notamment en raison de son traitement implicite de la synchronisation. Au moins deux problèmes se posent lors de l'encodage en Rocq d'un tel modèle, où chaque variable représente un flot de données et chaque nœud calcule une fonction de flots. Le premier concerne les opérateurs du langage en eux-même : comment définir $x = e$ when c, lorsque le flot booléen associé à c est infiniment faux ? Le second concerne le calcul du point fixe d'équations mutuellement récursives : comment résoudre $x = 1 + x$, ou encore $x = 1 + y$; $y = 2 - x$ ? Bien que ces deux derniers cas, pathologiques dans le langage, puissent être éliminés par une analyse de dépendances entre les variables, il est tout de même nécessaire de leur donner une sémantique, et les contraintes de productivité des fonctions en Rocq ne le permettent pas directement.

Une bibliothèque [PM09] développée par C. Paulin-Mohring propose un encodage des fonctions de flots reposant sur une astuce due à V. Capretta [Cap05]. L'idée est d'intercaler un constructeur « silencieux » dans le type des flots permettant de garantir la productivité des fonctions. De façon plus générale, la bibliothèque fournit toute l'infrastructure nécessaire à l'encodage constructif de la sémantique de Kahn. Dans cette section, nous présentons les principaux éléments de cette bibliothèque et montrons comment ils peuvent être adaptés à un noyau du langage flot de données. Nous décrirons en section 4 l'extension au langage complet avec machines à états.
## 3.1 Ordres partiels complets

Dans le modèle de Kahn, l'interprétation d'un programme est donnée par le plus petit point fixe d'une fonction de dénotation, qui doit être continue au sens de Scott. La bibliothèque introduit une hiérarchie de types encodant ces propriétés.

**Monotonicité** Un type arbitraire `tord` peut être équipé d'une relation d'ordre `Ole`, notée $\leq$, afin de constituer un ensemble ordonné.

Record ord : Type := mk_ord {
    tord :> Type;
    Ole : tord → tord → Prop;
    Ole_refl : ∀ x : tord, Ole x x;
    Ole_trans : ∀ x y z : tord, Ole x y → Ole y z → Ole x z
}.
Infix "≤" := Ole.

En suit naturellement la caractérisation d'une fonction monotone, notée $O_1 \to_m O_2$, d'un ensemble ordonné à un autre.

**Definition monotonic** ($O_1, O_2$ : ord) ($f : O_1 \to O_2$) := $\forall x y, x \leq y \to f x \leq f y$.

Record fmono (O₁ O₂ : ord) : Type := mk_fmono {
    fmonot :> O₁ → O₂;
    fmonotonic : monotonic fmonot
}.
Infix "→_m" := fmono.

Infix "@" := (* composition de fonctions monotones *)

L'utilisation de coercitions implicites dans les champs des enregistrements facilite beaucoup la manipulation de ces différents éléments. Ainsi, un terme de type $O_1 \to_m O_2$ peut être appliqué à un terme de type $O_1$, à la manière d'une fonction.

L'égalité entre éléments, notée $\equiv$, est dérivée directement de la relation d'ordre.

**Definition Oeq** (O : ord) (x y : O) := x ≤ y ∧ y ≤ x.

Infix "≡" := Oeq.

**Ordre partiel complet** La notion de continuité au sens de Scott est définie sur des fonctions à valeurs dans un ordre partiel complet ($\omega$-cpo), ensemble ordonné muni d'un plus petit élément $\perp$ et dans lequel toute chaîne croissante admet une plus petite borne supérieure (lub). Dans ce cadre, une chaîne croissante d'éléments de type O est représentée par une fonction monotone $nat_O \to_m O$, où $nat_O$ est l'ensemble des entiers naturels équipé de l'ordre usuel. Ici encore, la structure est donnée par les champs d'un enregistrement.

Record cpo : Type := mk_cpo {
    tcpo :> ord;
    $\perp$ : tcpo;
    lub : (nat_O \to_m tcpo) \to tcpo;
    Dbot : ∀ x : tcpo, $\perp$ \leq x;
    le_lub : ∀ (f : nat_O \to_m tcpo) (n : nat), f n \leq lub f;
    lub_le : ∀ (f : nat_O \to_m tcpo) (x : tcpo), (∀ n, f n \leq x) \to lub f \leq x
}.

Plusieurs instances de cpo sont particulièrement utiles à l'encodage d'un langage de programmation, notamment le produit de cpo $D_1 \times D_2$, le n-uplet $D^n$ ou encore le produit indexé $\Pi (\lambda i : I \Rightarrow D_i)$, où I est un type quelconque.
**Point fixe** Une fonction monotone sur les cpo est continue, et notée $D_1 \to_c D_2$, si elle est compatible avec les opérateurs de plus petite borne supérieure.

**Definition continuous** ($D_1, D_2$ : cpo) ($f : D_1 \to_m D_2$) : $\forall h$, $f$ (lub $h$) $\le$ lub ($f$ @ $h$).

**Record** fconti ($D_1, D_2$ : cpo) : Type := mk\_fconti { 
  fcontit : $D_1 \to_m D_2$;
  fcontinuous : continuous fcontit
}.

L'ensemble des fonctions continues formant lui-même un cpo, il est possible de définir un opérateur de point fixe s'appliquant à toute fonction continue. Le calcul s'effectue par itérations successives de la fonction à partir de l'élément $\perp$ du cpo. La fonction fixp ainsi obtenue satisfait bien l'équation de point fixe.

**Definition fixp** ($D$ : cpo), ($D \to_c D$) $\to_c D$ : $\text{lub} \ @ \ \text{iter}$.
(* où $[\text{iter} F 0 = \perp]$ et $[\text{iter} F (S n) = F (\text{iter} F n)]$ *)

**Lemma** fixp\_eq : $\forall$ ($D$ : cpo) ($F : D \to_c D$), fixp $F \equiv F$ (fixp $F$).

Dans la suite de cet article, nous donnerons parfois des termes de la forme fixp ($\lambda x \Rightarrow F$). Il s'agit ici d'une notation car l'opérateur fixp ne peut s'appliquer directement aux $\lambda$-termes de Rocq. Dans la pratique, il faut d'abord trouver un moyen de définir $F$ comme une instance de fonction continue, puis d'appliquer fixp $F$.

## 3.2 Flots et réseaux de Kahn

La bibliothèque fournit un encodage particulièrement astucieux du cpo des flots finis ou infinis, domaine support pour la sémantique d'un langage flot de données. Le type des flots dénotationnels DStr étend celui de la bibliothèque standard avec un constructeur **Eps**.

**CoInductive** DStr (A : Type) := Eps : DStr A → DStr A
| Cons : A → DStr A → DStr A.

Intuitivement, **Eps** correspond à une étape de calcul silencieuse lors de laquelle aucun élément de type A n'est produit. Le flot vide est donc représenté par une suite infinie d'**Eps**.

**CoFixpoint** DS\_bot (A : Type) : DStr A := Eps (DS\_bot A).

De même, un flot fini est représenté par un DStr se terminant par une infinité de **Eps**. Cette astuce permet de garantir la productivité, au sens de Rocq, des fonctions de flots définies par co-induction. Nous ne détaillons pas ici la construction complète du cpo des flots, noté DS. Il est équipé de l'ordre préfixe sur les flots et d'un algorithme de calcul de la borne supérieure d'une chaîne ordonnée de flots, cf. [PM09, §3.2]. Le point essentiel dans cette approche est que le constructeur **Eps** n'impacte pas le résultat d'un calcul et se comporte de façon transparente par rapport à la relation d'ordre.

**Lemma** eqEps : $\forall A$ ($x : DS A$), $x \equiv \text{Eps} x$.

Les fonctions continues sur les flots sont définies soit directement par co-induction, soit par composition d'autres fonctions continues. Dans les deux cas, la définition en elle-même est souvent difficile à lire en raison du traitement assez laborieux des **Eps** ou du transport des preuves de continuité. L'usage est alors d'associer à ces définitions un ensemble d'« équations caractéristiques », sous forme de règles équationnelles. Nous donnons en figure 2 la signature des principales fonctions disponibles dans la bibliothèque, ou facilement dérivables, ainsi que leurs équations caractéristiques. Certaines règles, comme arrow\_eq dénotent une égalité structurelle tandis que d'autres, comme map\_cons, découlent de l'application de fixp\_eq et utilisent une égalité sétoïde modulo **Eps**. La fonction wheni est d'un intérêt tout particulier ici car elle généralise l'échantillonnage à un flot de condition dont les valeurs sont d'un type énuméré | arbitraire et non plus strictement booléen. Son dual mergei est défini en section 4.1.
**Parameters A B I : Type.**

(* flot constant *)

**Definition const (a : A) : DS A.**

**Lemma const_cons : ∀ a, const a ≡ cons a (const a).**

(* queue *)

**Definition rem : DS A →<sub>c</sub> DS A.**

**Lemma rem_cons : ∀ a s, rem (cons a s) = s.**

(* application d'une fonction point à point *)

**Definition map (f : A → B) : DS A →<sub>c</sub> DS B.**

**Lemma map_cons : ∀ a s, map f (cons a s) ≡ cons (f a) (map f s).**

**Lemma map : map f ⊥ ≡ ⊥.**

(* délai initialisé *)

**Definition fby : DS A →<sub>c</sub> DS A →<sub>c</sub> DS A.**

**Lemma fby_cons : ∀ a s t, fby (cons a s) t ≡ cons a t.**

(* initialisation "→" *)

**Definition arrow : DS A →<sub>c</sub> DS A →<sub>c</sub> DS A.**

**Lemma arrow_eq : ∀ s t, arrow s t = fby s (rem t).**

(* échantillonnage *)

**Definition wheni (k : I) : DS I →<sub>c</sub> DS A →<sub>c</sub> DS A.**

**Lemma wheni_cons : ∀ k c cs x xs,**

wheni k (cons c cs) (cons x xs) ≡

if c = k then cons x (wheni k cs xs) else wheni k cs xs.

**Lemma wheni_false : ∀ k s, wheni k (const false) s ≡ ⊥.**

(* fusion *)

**Definition merge : DS bool →<sub>c</sub> DS A →<sub>c</sub> DS A →<sub>c</sub> DS A.**

**Lemma merge_cons : ∀ c cs x xs y ys,**

merge (cons c cs) (cons x xs) (cons y ys) ≡

if c then cons x (merge cs xs (cons y ys))

else cons y (merge cs (cons x xs) ys).

<caption>**Figure 2.** Primitives sur les flots accompagnées de leurs équations caractéristiques.</caption>

## 3.3 Adaptation à un compilateur vérifié

L'adaptation de la bibliothèque de [PM09] au compilateur Vélus, pour un sous-ensemble du langage d'entrée, a fait l'objet de précédents travaux [BJP25]. Nous en donnons les grandes lignes ici, ainsi que les modifications que nous avons apportées pour la prise en charge des machines à états. Le développement Rocq associé est disponible en ligne<fnref n="2" />.

L'architecture d'un compilateur vérifié impose un plongement profond, où chaque élément de la syntaxe est associé à un composant dans la sémantique de Kahn.

### Types des composants
Le type value des données véhiculées dans les flots reflète les contraintes liées au mécanisme de compilation : une valeur peut être d'un type numérique de base fourni par la bibliothèque de CompCert, ou bien d'un type énuméré tag permettant d'identifier les branches d'une conditionnelle ou d'une machine à états. De plus, en raison de la partialité de certains opérateurs du langage comme la division entière ou certaines opérations bit à bit, une valeur doit encoder la possibilité d'une erreur.

<footnote n="2">2. https://velus.inria.fr/jfla2026</footnote>
$$
\begin{align*}
\textbf{Inductive value} &:= \text{Vscalar} (v : \text{CompCert.cvalue}) \\
&| \text{Venum} (t : \text{tag}).
\end{align*}
$$

$$
\begin{array}{lcl}
\textbf{Inductive evalue} & := & \textbf{Val} (v : \textbf{value}) \\
& | & \textbf{Err} (e : \textbf{error}).
\end{array}
$$

Chaque variable d'un nœud du programme, entrée comme sortie, est associée à un flot de données. L'environnement ainsi constitué, local au nœud, est représenté par un produit indexé de type SEnv. Notre encodage prend en charge la construction last du langage, qui nécessite d'étendre cet environnement avec un cas supplémentaire pour chaque variable déclarée comme partagée.

$$
\textbf{Inductive} key := \textbf{Var} (i : \textbf{ident}) \mid \textbf{Last} (i : \textbf{ident}).
$$

$$
\textbf{Definition} SEnv : cpo := \Pi (\lambda k : \mathbf{key} \Rightarrow DS \ \mathbf{evalue}).
$$

Pour faciliter la lecture des définitions présentées dans cet article, nous surchargerons la plupart de fonctions de flots en les appliquant aux environnements. Par exemple, si env₁ et env₂ sont deux environnements de type SEnv, nous écrirons fby env₁ env₂ pour désigner l'environnement env₃ tel que ∀ k, env₃ k = fby (env₁ k) (env₂ k). Cette notation rapporte en fait à la fonction fby_env du développement Rocq.

La seule opération véritablement ensembliste utile à notre développement est celle d'union de deux environnements, sur un domaine donné.

$$
\textbf{Definition} \ union\_left (dom : list \ ident) : SEnv $\rightarrow$$_{c}^{}$ SEnv $\rightarrow$$_{c}^{}$ SEnv.
$$

$$
\begin{array}{l}
\textbf{Lemma} \ union\_left\_spec : \forall \ dom \ env_1 \ env_2 \ i, \\
\quad \quad \quad \quad \quad \quad \quad \quad \quad \text{union\_left} \ dom \ env_1 \ env_2 \ (\text{Var } i) = (\text{if } i \in \ dom \ \text{then} \ env_1 \ (\text{Var } i) \ \text{else} \ env_2 \ (\text{Var } i)) \\
\quad \quad \quad \quad \quad \quad \quad \quad \quad \wedge \ \text{union\_left} \ dom \ env_1 \ env_2 \ (\text{Last } i) = (\text{if } i \in \ dom \ \text{then} \ env_1 \ (\text{Last } i) \ \text{else} \ env_2 \ (\text{Last } i)).
\end{array}
$$

Enfin, chaque nœud est associé à une fonction continue entre environnements. Le pro-
gramme, constitué de l'ensemble des nœuds, est donc associé à un environnement global
d'ordre supérieur de type FEnv où l'identifiant f est celui d'un nœud du programme.

$$
\textbf{Definition} FEnv : cpo := \Pi (\lambda f : \text{ident} \Rightarrow SEnv \to_c SEnv).
$$

**Interprétation** La dénotation d'un programme est définie à plusieurs niveaux : expressions, blocs et nœuds. Une expression s'évalue par rapport à un environnement global de fonctions et un environnement local de variables. Dans Vélus, chaque expression *e* est associée à un nombre *length(e)* de flots, d'où l'utilisation d'un n-uplet de type dépendant. Le calcul de ces flots se fait dans la plupart des cas par application de l'opérateur sémantique associé à chaque primitive.

$$
\textbf{Definition} \ denot\_exp (e : \exp) : FEnv \to_c SEnv \to_c (DS \ evalue)^{\text{length}(e)}.
$$

$$
\begin{array}{r@{\quad}l}
\textbf{Lemma} & denot\_exp\_eq : \forall envG env, \\
& denot\_exp e envG env = \\
& \quad \textbf{match} e \textbf{ with} \\
& \quad \quad (* c (constante) *) \\
& \quad \quad \mid Econst c \Rightarrow const (\text{val} (\text{Vscalar} (\text{CompCert.sem\_const c}))) \\
& \quad \quad \mid (* x (variable) *) \\
& \quad \quad \mid Evar x \Rightarrow env (\text{Var } x) \\
& \quad \quad \mid (* last x *) \\
& \quad \quad \mid Elast x \Rightarrow env (\text{Last } x) \\
& \quad \quad \mid (* op e *) \\
& \quad \quad \mid Eunop op e \Rightarrow \text{map} (\text{CompCert.sem\_unop op}) (denot\_exp e envG env) \\
& \quad \quad \mid (* e_0 fby e *) \\
& \quad \quad \mid Efby e_0 e \Rightarrow fby (denot\_exp e_0 envG env) (denot\_exp e envG env)
\end{array}
$$
(* e when (x = k) *)
| Ewhen e x k ⇒ wheni k (env (Var x)) (denot_exp e envG env)
(* f(e₁,...,eₙ) *)
| Eapp f es ⇒ envG f (SEnv_ofprodu (denot_exps es envG env))
| _ ⇒ (* ... *)
end.

Nous ne détaillons pas ici toutes les constructions du langage et présentons une définition légèrement simplifiée, passant sous silence le traitement des listes d'expressions et des annotations de typage. En particulier, la fonction SEnv_ofprodu utilisée dans une instance de nœud est chargée de convertir un n-uplet de flots à un environnement de type SEnv. La liste d'identifiants nécessaire pour créer l'association est celle, non explicitée ici, des variables d'entrée du nœud f.

Un bloc s'évalue en une fonction d'environnements. Il prend l'environnement local au nœud et le met à jour selon ses équations. Si le bloc définit de nouvelles variables locales, celles-ci sont calculées par un point fixe puis retirées du résultat afin de ne pas s'échapper dans l'environnement renvoyé.

Definition denot_block : block → FEnv →$_{c}$ SEnv →$_{c}$ SEnv.

Lemma denot_block_eq : ∀ b envG env,
denot_block b envG env =
match b with
  (* x₁,...,xₙ = e₁,...,eₘ; *)
  | Beq xs es ⇒ env_add_vars xs (denot_exps es envG env)
  (* last x = e; *)
  | Blast x e ⇒ env_add_last x (fby (denot_exp e envG env) (env (Var x))) env
  (* var x₁;...;xₙ; let blk₁;...;blkₘ; tel; *)
  | Blocal xs blks ⇒
      let env' := fixp (λ env' ⇒ denot_blocks blks envG (union_left xs env' env)) in
      union_left xs env env'
  | _ ⇒ (* switch, automaton, cf. section 4 *)
end.

La dénotation d'un nœud $n$ est également une fonction continue d'environnements. L'environnement d'entrée ne contient initialement que les flots des variables d'entrée du nœud, nommées $n.(n\_in)$, tous les autres étant fixés à $\perp$. La sémantique est définie par le point fixe du bloc principal $n.(n\_block)$, où chaque itération ré-introduit les flots d'entrée. De cette façon, l'environnement obtenu est bien un point fixe contenant tous les flots exposés par le nœud, entrées comme sorties.

Definition denot_node : node → FEnv →$_{c}$ SEnv →$_{c}$ SEnv.

Lemma denot_node_eq : ∀ n envG env,
denot_node n envG env =
fixp (λ env' ⇒ denot_block n.(n_block) envG (union_left n.(n_in) env env')).

Un programme global contient l'ensemble des nœuds, dont la définition est accessible par l'intermédiaire de la fonction find_node. La sémantique d'un programme est donnée par le point fixe des nœuds. Ce modèle autorise le calcul de nœuds récursifs, bien que ces derniers soient rejetés à la compilation car non adaptés à l'exécution en temps et en mémoire bornés.

Definition denot_global (G : global) : FEnv :=
fixp (λ envG f ⇒ match find_node f G with
  | Some n ⇒ denot_node G n envG
  | None ⇒ ⊥
end).
# 4 Extension aux machines à états

Le traitement des machines à états dans le langage tire pleinement parti du découpage des nœuds en blocs hiérarchisés décrit précédemment. Comme les blocs sont interprétés par des fonctions d'environnements, une machine à états peut être interprétée comme une fonction d'environnements d'ordre supérieur. Dans cette section, nous donnons une sémantique de flots aux machines à états telles que décrites en section 2. Dans un souci de clarté nous présentons d'abord les machines à états à transitions avec histoire (continue), sans réinitialisation, où l'exécution mémorise ses valeurs lors d'un changement d'état. Nous donnons ensuite la sémantique avec réinitialisation à chaque transition, c'est à dire sans continue, puis enfin celle des machines à états mélangeant les deux comportements.

## 4.1 Transitions sans réinitialisation

Une machine à états sans réinitialisation s'apparente à la structure d'activation *switch*, déjà présente dans le compilateur et dans sa sémantique relationnelle [BPP23a], mais pas dans sa sémantique dénotationnelle.

```
type t = A | B
node ex1(c : t; x : int)
returns (y : int)
let
    switch c
        | A do y = (0 fby y) + x;
        | B do y = (0 fby y) - x;
end
tel
```

<table><thead><tr><th></th><th>c</th><th>A</th><th>A</th><th>A</th><th>B</th><th>B</th><th>A</th><th>A</th></tr></thead><tbody><tr><th>x</th><td>1</td><td>2</td><td>1</td><td>2</td><td>1</td><td>2</td><td>1</td><td>1</td></tr><tr><th>A.y</th><td>1</td><td>3</td><td>4</td><td></td><td></td><td>6</td><td>7</td><td></td></tr><tr><th>B.y</th><td></td><td></td><td></td><td>-2</td><td>-3</td><td></td><td></td><td></td></tr><tr><th>y</th><td>1</td><td>3</td><td>4</td><td>-2</td><td>-3</td><td>6</td><td>7</td><td></td></tr></tbody></table>

Un *switch* détermine, en fonction de son argument *c*, quel bloc d'équations *A* ou *B* doit être actif à chaque instant. Son comportement est donc proche de celui d'un *merge*, mais doit fournir au bloc actif un environnement de variables correctement échantillonné.

Nous définissons d'abord la fonction *mergei*, généralisation de *merge* permettant de sélectionner un environnement parmi un ensemble indexé d'environnements.

**Definition mergei** : DS tag $\to_c \Pi (\lambda i : tag \Rightarrow SEnv) \to_c SEnv$.

**Lemma mergei_cons** : $\forall i c \text{istr}$, mergei (cons i c) istr $\equiv$ fby (istr i) (mergei c ($\lambda j \Rightarrow \text{if } i = j \text{ then } \text{rem} (istr j) \text{ else } istr j$)).

La fonction *switch* applique alors *mergei* sur ses blocs, donnés par un ensemble indexé de fonctions d'environnements. L'environnement *env* de variables fourni à chaque bloc d'indice *i* est échantillonné grâce à la primitive *wheni*.

**Definition switch** : DS tag $\to_c \Pi (\lambda i : tag \Rightarrow SEnv \to_c SEnv) \to_c SEnv \to_c SEnv$.

**Lemma switch_eq** : $\forall c f \text{env}$, switch c f env $= \text{mergei} c (\lambda i \Rightarrow f i (\text{wheni} i c \text{env}))$.

Une machine à états sans réinitialisation fonctionne de façon similaire, à ceci près que la condition d'activation *c* n'est plus donnée par la structure environnante mais déterminée implicitement au sein de l'automate avec le calcul des flots de transition.
node ex2(x : int) returns (y : int)

let

<table><tr><td>automaton initially A</td><td>x</td><td>1</td><td>2</td><td>1</td><td>0</td><td>1</td><td>2</td><td>0</td><td>1</td><td>2</td></tr><tr><td>state A do</td><td>A.y</td><td>1</td><td>3</td><td>4</td><td></td><td></td><td></td><td>4</td><td>5</td><td>7</td></tr><tr><td>y = (0 fby y) + x;</td><td>A.t</td><td>N</td><td>N</td><td>N</td><td>B</td><td></td><td></td><td></td><td>N</td><td>N</td></tr><tr><td>unless x = 0 continue B</td><td>B.y</td><td></td><td></td><td></td><td>0</td><td>-1</td><td>-3</td><td></td><td></td><td></td></tr><tr><td>state B do</td><td>B.t</td><td></td><td></td><td></td><td></td><td>N</td><td>N</td><td>A</td><td></td><td></td></tr><tr><td>y = (0 fby y) - x;</td><td>c</td><td>A</td><td>A</td><td>A</td><td>B</td><td>B</td><td>B</td><td>A</td><td>A</td><td>A</td></tr><tr><td>unless x = 0 continue A</td><td>y</td><td>1</td><td>3</td><td>4</td><td>0</td><td>-1</td><td>-3</td><td>4</td><td>5</td><td>7</td></tr></table>

end

tel

Pour cet exemple, nous représentons dans le chronogramme deux flots par état de la machine. Le premier correspond à la variable y calculée dans le corps du bloc tandis que t correspond au flot de transition spécifié par l'état. Il vaut N(one) tant qu'aucune condition de transition ne s'applique, puis vaut A ou B selon l'état vers lequel sauter. Le décalage systématique entre les deux flots d'un même état, observable lors d'une transition, est une conséquence directe du modèle synchrone. En présence d'une transition forte (spécifiée par unless) c'est le corps du bloc de l'état cible qui est exécuté, et non celui de l'état source.

Comme toutes les transitions ici sont continue, sauter d'un état vers lui-même n'a pas d'effet sur l'exécution, il serait donc équivalent à remplacer les N par l'identifiant de l'état calculant la transition. On détermine le c sous-jacent en recollant les flots ainsi obtenus.

Notre sémantique modélise ce comportement en calculant de façon mutuellement récursive le flot t associé à chaque état et le flot c, nécessaire à l'échantillonnage de l'environnement d'entrée. La signature d'une fonction dénotant une machine à états est la suivante.

Definition auto _continue _strong (i : tag) : (* i : état initial *)
Π (λ i : tag ⇒ SEnv → $_{c}$SEnv) → $_{c}$ (* fs : blocs *)
Π (λ i : tag ⇒ SEnv → $_{c}$DS (option tag)) → $_{c}$ (* ft : transitions *)
SEnv → $_{c}$SEnv.

Chaque état i de la machine à états définit une fonction d'environnements (fs i) calculant le corps du bloc (A.y et B.y dans notre exemple) ainsi qu'une fonction (ft i) calculant le flot de transition (A.t et B.t dans notre exemple). L'interprétation est donnée par deux calculs mutuellement récursifs, celui des flots de transitions d'une part et celui du flot de sélection c d'autre part.

Lemma auto _continue _strong _eq : ∀ i fs ft env,
auto _continue _strong i fs ft env =
(* opt _def i = λ (Some j) ⇒ j | None ⇒ i *)
let ( , c) := fixp (λ (ft', c) env') ⇒
(λ i ⇒ map (opt _def i) (ft i (wheni i c env))),
(cons i (mergei c ft'))
in mergei (rem c) (λ i ⇒ fs i (wheni i (rem c) env)).

Lorsque les transitions d'une machine à états sont faibles, c'est à dire spécifiées avec until et non unless, le flot de transition d'un état peut dépendre des variables calculées dans le corps du bloc. Cela nécessite donc un calcul mutuellement récursif des transitions, du flot de sélection et du corps des blocs.

Lemma auto _continue _weak _eq : ∀ i fs ft env,
auto _continue _weak i fs ft env =
let ( , , env') := fixp (λ (ft', c, env') ⇒
(λ i ⇒ map (opt _def i) (ft i (wheni i c env))),
(cons i (mergei c ft')),
(mergei c (λ i ⇒ fs i (wheni i c env))))
in env'.
## 4.2 Transitions avec réinitialisation

Les machines à états avec transitions réinitialisantes peuvent être vues comme une généralisation de la réinitialisation modulaire des nœuds, formalisée dans Vélus [BBP20] et dans sa sémantique dénotationnelle [BJP25]. Les définitions que nous proposons s'inspirent des idées de P. Caspi [Cas94], qui affirme que « les schéma-blocs sont fonctionnels ». Ou plus précisément, que le comportement des opérateurs d'un langage de schéma-blocs est assimilable à celui de fonctions récursives terminales d'un langage fonctionnel.

Nous commençons par définir les deux fonctions de filtrage suivantes, qui attendent que le flot de condition soit vrai pour propager les valeurs de leur second argument. À la différence du wheni, elles rendent la main dès la première occurrence d'une valeur vraie dans la condition, ignorant la suite des valeurs. Les deux versions proposées ici sont nommées d'après les mots-clés unless et until du langage et s'appliquent respectivement aux transitions fortes (propagation immédiate) et faibles (propagation différée).

**Definition** `rem_unless`: $DS \text{ bool} \rightarrow_c DS A \rightarrow_c DS A$.

**Lemma** `rem_unless_cons`: $\forall c \text{ cs } x \text{ xs},$
`rem_unless` (cons c cs) (cons x xs) $\equiv$
if c then cons x xs else `rem_unless` cs xs.

<table><thead><tr><th></th><th>cs</th><th>F</th><th>F</th><th>T</th><th>F</th><th>T</th><th>F</th></tr></thead><tbody><tr><td></td><td>xs</td><td>1</td><td>2</td><td>3</td><td>4</td><td>5</td><td>6</td></tr><tr><td>rem_unless</td><td></td><td></td><td></td><td>3</td><td>4</td><td>5</td><td>6</td></tr><tr><td>rem_until</td><td></td><td></td><td></td><td></td><td>4</td><td>5</td><td>6</td></tr></tbody></table>

**Lemma** `rem_until_eq`: $\forall \text{cs xs},$
`rem_until` cs xs $\equiv$ `rem` (`rem_unless` cs xs).

L'opérateur dual, défini sur un produit indexé d'environnements de flots, propage les valeurs d'un environnement jusqu'à ce qu'une valeur soit reçue sur le flot de sélection. Là encore, la fonction rend la main dès le signal reçu et branche immédiatement, ou avec un coup de retard pour les transitions faibles, sur la prochaine instance sélectionnée.

**Definition** `mergei_unless`: $DS$ (option tag) $\rightarrow_c$ $SEnv$ $\rightarrow_c$ $\Pi$ ($\lambda i : \text{tag} \Rightarrow SEnv$) $\rightarrow_c$ $SEnv$.

**Lemma** `mergei_unless_cons`: $\forall c \text{ cs env f},$

<table><thead><tr><th></th><th>cs</th><th>N</th><th>N</th><th>A</th><th>N</th><th>B</th></tr></thead><tbody><tr><td>mergei_unless (cons c cs) env f $\equiv$ match c with</td><td>env</td><td>1</td><td>2</td><td>3</td><td>4</td><td>5</td></tr><tr><td>| None $\Rightarrow$ fby env (mergei_unless cs (rem env) f)</td><td>(f A)</td><td>10</td><td>11</td><td>12</td><td>13</td><td>14</td></tr><tr><td>| Some i $\Rightarrow$ f i</td><td>(f B)</td><td>20</td><td>21</td><td>22</td><td>23</td><td>24</td></tr><tr><td>end.</td><td></td><td>mergei_unless</td><td>1</td><td>2</td><td>10</td><td>11</td><td>12</td></tr><tr><td></td><td></td><td>mergei_until</td><td>1</td><td>2</td><td>3</td><td>10</td><td>11</td></tr></tbody></table>

**Lemma** `mergei_until_eq`: $\forall \text{cs env f},$

`mergei_until` cs env f $=$ `mergei_unless` (cons None cs) env f.

Ces opérateurs sont particulièrement utiles pour définir la fonction de dénotation d'une machine à états sans histoire, où la mémoire des états est réinitialisée à chaque transition. L'exemple suivant illustre le comportement d'une telle machine à états, aux transitions faibles.

```
node ex3(x : int) returns (y : int)
let
    automaton initially A
    state A do
        y = (0 fby y) + x;
        until y > 3 then B
    state B do
        y = (0 fby y) - x;
        until y < -2 then A
end
tel
```

<table><tbody><tr><td>automaton initially A</td><td>x</td><td>1</td><td>2</td><td>1</td><td>0</td><td>1</td><td>2</td><td>0</td><td>1</td><td>2</td></tr><tr><td>state A do</td><td>A.y</td><td>1</td><td>3</td><td>4</td><td></td><td></td><td></td><td></td><td></td><td></td></tr><tr><td>y = (0 fby y) + x;</td><td>A.t</td><td>N</td><td>N</td><td>B</td><td></td><td></td><td></td><td></td><td></td><td></td></tr><tr><td>until y > 3 then B</td><td>B.y</td><td></td><td></td><td></td><td>0</td><td>-1</td><td>-3</td><td></td><td></td><td></td></tr><tr><td>state B do</td><td>B.t</td><td></td><td></td><td></td><td>N</td><td>N</td><td>A</td><td></td><td></td><td></td></tr><tr><td>y = (0 fby y) - x;</td><td>A.y</td><td></td><td></td><td></td><td></td><td></td><td></td><td>0</td><td>1</td><td>3</td></tr><tr><td>until y < -2 then A</td><td>A.t</td><td></td><td></td><td></td><td></td><td></td><td></td><td>N</td><td>N</td><td>N</td></tr><tr><td>end</td><td>y</td><td>1</td><td>3</td><td>4</td><td>0</td><td>-1</td><td>-3</td><td>0</td><td>1</td><td>3</td></tr></tbody></table>

Chaque transition déclenche une nouvelle instance de l'état cible, représentée par deux
nouvelles entrées dans le chronogramme. Ce fonctionnement permet à l'état source d'« ou-
blier » son environnement avant de sauter. Cette analogie avec la récursion terminale des
langages fonctionnels est perceptible dans l'opérateur sémantique associé.

Lemma `auto_reset_weak_eq`: $\forall i \text{ fs ft env,}$
$$
\begin{align*}
\mathit{auto\_reset\_weak} \ i \ \text{fs ft env} \ = & \\
\mathit{let} \ \mathcal{F} \ := & \ \mathit{fixp} \ (\lambda F \ (i, \mathit{env}) \Rightarrow \\
& \ \mathit{let env'} \ := \ \mathit{fs} \ i \ \mathit{env} \ \mathit{in} \\
& \ \mathit{let} \ t \ := \ \mathit{ft} \ i \ \mathit{env'} \ \mathit{in} \\
& \ \mathit{mergei\_until} \ t \ \mathit{env'} \ (\lambda j \Rightarrow F \ (j, \mathit{rem\_until} \ (\mathit{map} \ \mathit{is\_some} \ t) \ \mathit{env}))) \\
& \ \mathit{in} \ F \ (i, \mathit{env}).
\end{align*}
$$

L'environnement env' calculé localement dans le corps d'un état est d'abord utilisé pour déterminer le flot de transition t. Il est ensuite passé à mergei_until, qui propage ses valeurs tant que t est None mais qui l'oublie au moment de sauter lors d'une transition. L'échantillonnage de l'environnement env est réalisé avec rem_until et non wheni comme précédemment, car le flot de sélection issu de t n'est calculé que pour l'instance courante de l'état.

La gestion des transitions fortes est légèrement plus délicate en raison du décalage entre
le calcul du corps de l'état et le calcul des transitions. Dans l'exemple suivant, la première
transition est prise au troisième instant, lorsque A a suffisamment patienté, et les valeurs
de B.y sont immédiatement propagées. La transition de A ayant déjà été calculée au troisième
instant, le calcul de celle de B est reportée à l'instant suivant, ignorant au passage le signal
reçu de x.

node ex4(x : int) returns (y : int)

<table>
  <thead>
    <tr>
      <th>let</th>
      <th>x</th>
      <th>0</th>
      <th>0</th>
      <th>1</th>
      <th>0</th>
      <th>1</th>
      <th>0</th>
      <th>0</th>
    </tr>
  </thead>
  <tbody>
    <tr>
      <td>automaton initially A</td>
      <td>A.y</td>
      <td>0</td>
      <td>1</td>
      <td></td>
      <td></td>
      <td></td>
      <td></td>
      <td></td>
    </tr>
    <tr>
      <td>state A do</td>
      <td>A.t</td>
      <td>N</td>
      <td>N</td>
      <td>B</td>
      <td></td>
      <td></td>
      <td></td>
      <td></td>
    </tr>
    <tr>
      <td>y = 0 fby (y + 1);</td>
      <td>B.y</td>
      <td></td>
      <td></td>
      <td>10</td>
      <td>11</td>
      <td></td>
      <td></td>
      <td></td>
    </tr>
    <tr>
      <td>unless patienter(2) then B</td>
      <td>B.t</td>
      <td></td>
      <td></td>
      <td>(N)</td>
      <td>N</td>
      <td>A</td>
      <td></td>
      <td></td>
    </tr>
    <tr>
      <td>state B do</td>
      <td>A.y</td>
      <td></td>
      <td></td>
      <td></td>
      <td></td>
      <td>0</td>
      <td>1</td>
      <td>2</td>
    </tr>
    <tr>
      <td>y = 10 fby (y + 1);</td>
      <td>A.t</td>
      <td></td>
      <td></td>
      <td></td>
      <td></td>
      <td>(N)</td>
      <td>N</td>
      <td>N</td>
    </tr>
    <tr>
      <td>unless x = 1 then A</td>
      <td></td>
      <td></td>
      <td></td>
      <td></td>
      <td></td>
      <td></td>
      <td></td>
      <td>B</td>
    </tr>
    <tr>
      <td>end</td>
      <td>y</td>
      <td>0</td>
      <td>1</td>
      <td>10</td>
      <td>11</td>
      <td>0</td>
      <td>1</td>
      <td>2</td>
    </tr>
  </tbody>
</table>

tel

Nous simulons ce comportement en ajoutant à la fonction un paramètre booléen init, vrai uniquement à l'initialisation de la machine à états. Pour toute autre instance un décalage, représenté par (N) dans le chronogramme ci-dessus, est ajouté en tête de t afin de ne pas calculer simultanément la transition de l'état source et celle de l'état cible.

Lemma `auto_reset_strong_eq`: $\forall i \text{ fs ft env,}$
$$
\begin{align*}
\mathit{auto\_reset\_strong} \ i \ \text{fs ft env} \ = & \\
\mathit{let} \ \mathcal{F} \ := & \ \mathit{fixp} \ (\lambda F \ (\mathit{init}, i, \mathit{env}) \Rightarrow \\
& \ \mathit{let} \ t \ := \ \mathit{if} \ \mathit{init} \ \mathit{then} \ \mathit{ft} \ i \ \mathit{env} \ \mathit{else} \ \mathit{cons} \ \mathit{None} \ (\mathit{ft} \ i \ (\mathit{rem} \ \mathit{env})) \ \mathit{in} \\
& \ \mathit{let} \ env' \ := \ \mathit{fs} \ i \ \mathit{env} \ \mathit{in} \\
& \ \mathit{mergei\_unless} \ t \ \mathit{env'} \ (\lambda j \Rightarrow F \ (\mathit{false}, j, \mathit{rem\_unless} \ (\mathit{map} \ \mathit{is\_some} \ t) \ \mathit{env}))) \\
& \ \mathit{in} \ F \ (\mathit{true}, i, \mathit{env}).
\end{align*}
$$

4.3 Transitions mixtes

Les machines à états, dans leur forme générale, supportent les transitions avec ou sans
continue. Une information booléenne supplémentaire est alors nécessaire dans le flot de
transition, spécifiant si l'état cible doit être réinitialisé ou non lors d'une transition.
Definition auto_weak (i : tag) :
(* i : état initial *)
Π (λ i : tag ⇒ SEnv →$_{c}$ SEnv) →$_{c}$
(* fs : blocs *)
Π (λ i : tag ⇒ SEnv →$_{c}$ DS (option (tag * bool))) →$_{c}$
(* ft : transitions *)
SEnv →$_{c}$ SEnv.

Dans l'exemple suivant, l'état B spécifie deux transitions vers A, l'une sans réinitialisation lorsque y < -2 et l'autre avec réinitialisation lorsque x = 0. Le chronogramme inclut cette information par l'intermédiaire d'un exposant R(éinitialisation) sur la valeur du flot de transition.

<table><tbody><tr><td>node</td><td>ex5(x : int)</td><td>#</td><td>1</td><td>2</td><td>3</td><td>4</td><td>5</td><td>6</td><td>7</td><td>8</td></tr><tr><td>returns</td><td>(y : int)</td><td>x</td><td>3</td><td>0</td><td>1</td><td>2</td><td>1</td><td>0</td><td>1</td><td>1</td></tr><tr><td>let</td><td></td><td>A.y</td><td>3</td><td>3</td><td></td><td></td><td></td><td></td><td></td><td></td></tr><tr><td>automaton</td><td>initially</td><td>A</td><td>A.t</td><td>N</td><td>B<sup>R</sup></td><td></td><td></td><td></td><td></td><td></td></tr><tr><td>state</td><td>A</td><td>do</td><td>B.y</td><td></td><td>-1</td><td>-3</td><td></td><td></td><td></td><td></td></tr><tr><td></td><td>y</td><td>(0 fby y) + x;</td><td>B.t</td><td></td><td>N</td><td>A</td><td></td><td></td><td></td><td></td></tr><tr><td>until</td><td>x</td><td>= 0 then B</td><td>A.y</td><td>3</td><td>3</td><td></td><td>4</td><td>4</td><td></td><td></td></tr><tr><td>state</td><td>B</td><td>do</td><td>A.t</td><td>N</td><td>B<sup>R</sup></td><td></td><td>N</td><td>B<sup>R</sup></td><td></td><td></td></tr><tr><td></td><td>y</td><td>(0 fby y) - x;</td><td>B.y</td><td></td><td></td><td></td><td></td><td></td><td>-1</td><td>-2</td></tr><tr><td>until</td><td>y</td><td>&lt; -2 continue</td><td>B.t</td><td></td><td></td><td></td><td></td><td></td><td>N</td><td>N</td></tr><tr><td>|</td><td>x</td><td>= 0 then A</td><td>y</td><td>3</td><td>3</td><td>-1</td><td>-3</td><td>4</td><td>4</td><td>-1</td><td>-2</td></tr><tr><td>end</td><td></td><td></td><td></td><td></td><td></td><td></td><td></td><td></td><td></td><td></td></tr><tr><td>tel</td><td></td><td></td><td></td><td></td><td></td><td></td><td></td><td></td><td></td><td></td></tr></tbody></table>

Aucune des définitions élaborées dans les sections précédentes ne peut s'appliquer directement : auto_reset oublie les flots calculés d'un état lors d'une transition, tandis que auto; continue ne permet d'appliquer les fonctions fs et ft qu'à une seule reprise. Notre approche pour les transitions mixtes consiste au contraire à appliquer systématiquement fs et ft à chaque transition. À la différence de auto_reset, le paramètre utilisé n'est plus l'environnement courant mais l'histoire de l'environnement propre à l'état cible depuis sa dernière réinitialisation. Par exemple, comme la transition vers l'état B à l'instant 3 est réinitialisante, fs et ft sont instanciées avec les valeurs de l'environnement (formé de x uniquement ici) à partir de l'instant 3. En revanche, lors de la transition vers A à l'instant 5, l'environnement reconstitué contient les valeurs de x aux instants 1, 2, 5, 6, 7, etc. de sorte à simuler une entrée dans A avec histoire. Le corps du bloc de A est donc recalculé depuis le début, et il faut penser à éliminer en tête du résultat les deux valeurs 3 · 3 déjà propagées.

La fonction d'interprétation introduit deux nouveaux paramètres :

- hist : Π (λ i ⇒ SEnv →$_{c}$ SEnv), définie comme une continuation, associe à chaque état i son environnement propre depuis sa dernière réinitialisation. Par exemple, hist A vaut l'identité initialement mais de l'instant 3 à l'instant 6 on a ∀ env, hist A env = 1 · 2 · env ;

- trim, du même type, permet d'éliminer les valeurs en tête d'un environnement qui ont déjà été propagées. Par exemple, trim A vaut l'identité initialement mais de l'instant 3 à l'instant 6 on a ∀ env, trim A env = rem² env.

Ces deux fonctions satisfont notamment l'invariant ∀ i env, trim i (hist i env) = env.

Lemma auto_weak_eq : ∀ i fs ft env,
auto_weak i fs ft env =
let F := fixp (λ F (i, reset, env, hist, trim) ⇒
let s := if reset then fs i env else trim i (fs i (hist i env)) in
let t := if reset then ft i s else trim i (ft i (hist i env)) in
(* mise à jour des continuations *)
let t' := map is_some t in
let hist := λ j env' ⇒ if j = i then hist i (merge_until t' s env') else hist j env' in
let trim := λ j env' ⇒ if j = i then rem_until t' (trim i env') else trim j env' in
mergei_until t s (λ (j, reset) ⇒ F (j, reset, rem_until t' env, hist, trim)))
in F (i, false, env, (λ i env ⇒ env), (λ i s ⇒ s)).
Comme dans les sections précédentes, la version forte de l'évaluation utilise les opérateurs unless et introduit le décalage au moyen d'un élément None en tête de flot lors d'une transition.

**Lemma auto_strong_eq:** $\forall i \text{ fs ft env,}$
$$ \begin{align*} \text{auto\_strong i fs ft env} &= \\ &\quad \text{let } \bar{F} := \text{fixp } (\lambda F \text{ (i, init, reset, env, hist, trim)} \Rightarrow \\ &\quad \qquad \text{let } t := \text{if init then ft i env} \\ &\quad \qquad \quad \text{else if reset then cons None (ft i (rem env))} \\ &\quad \qquad \quad \quad \text{else cons None (trim i (ft i (hist i (rem env)))) in \\ &\quad \qquad \text{let } s := \text{if reset then fs i env else trim i (fs i (hist i env)) in \\ &\quad \qquad \quad (* mise à jour des continuations *)} \\ &\quad \qquad \text{let } t' := \text{map is\_some t in} \\ &\quad \qquad \quad \text{let } \text{hist} := \lambda j \text{ env'} \Rightarrow \text{if } j = i \text{ then } \text{hist i (merge\_unless t' s env')} \text{ else } \text{hist j env'} \text{ in} \\ &\quad \qquad \quad \text{let } \text{trim} := \lambda j \text{ env'} \Rightarrow \text{if } j = i \text{ then } \text{rem\_unless t' (trim i env')} \text{ else } \text{trim j env} \text{ in} \\ &\quad \qquad \quad \quad \text{mergei\_unless } t \text{ s } (\lambda (j, reset) \Rightarrow \text{F (j, false, reset, rem\_unless t' env, hist, trim)}) \\ &\quad \qquad \quad \text{in } \text{F (i, true, false, env, (\lambda i env} \Rightarrow \text{env}), (\lambda i s \Rightarrow s)). \end{align*} $$

# 5 Conclusion

Nous donnons, avec ces définitions, une sémantique fonctionnelle aux machines à états des langages flot de données. Alors que les opérateurs sémantiques pour les constructions primitives (figure 2) s'appliquent aux flots de valeurs, ceux pour les constructions de blocs s'appliquent aux environnements de flots. Malgré le mélange de flots, d'environnements et de récursion, l'opérateur de point fixe permet de les faire accepter par Rocq. Les constructions par tactiques, nécessaires pour démontrer la continuité, sont pénibles mais leurs équations caractéristiques se révèlent naturelles. Une particularité de nos définitions est qu'elles ne reposent pas sur la manipulation d'un état interne mais sur des fonctions de flots récursives dans la sémantique dénotationnelle. Il s'avère intéressant de traiter séparément les machines à états dont tous les états sont réinitialisés en entrée (section 4.2), car leurs définitions sont assez directes, surtout en comparaison avec les maints détails techniques nécessaires au traitement des transitions mixtes (section 4.3).

L'implantation dans Rocq de nos définitions repose sur un encodage constructif des réseaux de Kahn [PM09]. Cependant, l'algorithme utilisé pour calculer la borne supérieure d'une chaîne de flots et, par extension, l'opérateur de point fixe, est trop inefficace pour être exécuté, même sur de petits exemples. En pratique, nous avons d'abord prototypé les différentes fonctions sémantiques en OCaml à l'aide du module Lazy, qui permet une évaluation efficace des flots sans Eps. Plus récemment, les *Interaction Trees* [XZH+19] ont été proposés comme un cadre pour développer des sémantiques dénotationnelles en Rocq. Leur encodage des calculs infinis, potentiellement bloquants ou divergents, utilise la même astuce que la bibliothèque CPO, satisfaisant les critères de productivité à l'aide d'un constructeur spécial Tau. Leur structure monadique d'évaluation ne semble toutefois pas appropriée au modèle des réseaux de Kahn, où les calculs s'effectuent à la fois dans l'instant (évaluation d'expressions) et dans le temps (composition parallèle d'équations et de nœuds).

Il reste à adapter nos définitions de machines à états au modèle synchrone, où l'absence de valeur dans un flot est marquée explicitement à l'aide d'un élément abs. Cela suppose d'étudier précisément les conditions de synchronisation des différents éléments du langage, ce qui s'avère déjà particulièrement délicat dans le contexte de réinitialisation modulaire [BJP25, §III.D]. Il faut ensuite prouver que la sémantique obtenue satisfait bien les prédicats relationnels du théorème de correction du compilateur. La question de la vérification des programmes reste ouverte également : quelles sont les bonnes règles pour raisonner dans un assistant de preuve sur le comportement de programmes réactifs écrits avec des machines à états ?
Références

[BBP20] Timothy BOURKE, Lélio BRUN et Marc POUZET : Mechanized semantics and verified compilation for a dataflow synchronous language with reset. *Proceedings of the ACM on Programming Languages*, 4(POPL):1–29, janvier 2020.

[BJP25] Timothy BOURKE, Paul JEANMAIRE et Marc POUZET : Functional stream semantics for a synchronous block-diagram compiler. In *Proceedings of the 40th Annual IEEE Symposium on Logic in Computer Science (LICS 2025)*, Singapour, juin 2025. ACM/IEEE.

[BL09] Sandrine BLAZY et Xavier LEROY : Mechanized semantics for the Clight subset of the C language. *Journal of Automated Reasoning*, 43(3):263–288, octobre 2009.

[BP13] Timothy BOURKE et Marc POUZET : Zélus : A synchronous language with ODEs. In Calin BELTA et Franjo IVANCIC, éditeurs : *Proceedings of the 16th International Conference on Hybrid Systems : Computation and Control (HSCC 2013)*, pages 113–118, Philadelphie, États-Unis, avril 2013. ACM Press.

[BPP23a] Timothy BOURKE, Basile PESIN et Marc POUZET : Analyse de dépendance vérifiée pour un langage synchrone à flot de données. In Timothy BOURKE et Delphine DEMANGE, éditeurs : *34<sup>es</sup> Journées Francophones des Langages Applicatifs (JFLA 2023)*, pages 101–120, Praz-sur-Arly, France, janvier/février 2023.

[BPP23b] Timothy BOURKE, Basile PESIN et Marc POUZET : Verified compilation of synchronous dataflow with state machines. *ACM Transactions on Embedded Computing Systems*, 22(5s):137:1–137:26, septembre 2023. Presenté à la 23<sup>ième</sup> conférence internationale sur l'Embedded Software (EMSOFT 2023).

[Cap05] Venanzio CAPRETTA : General recursion via inductive types. *Logical Methods in Computer Science (LMCS)*, 1(2), juillet 2005.

[Cas94] Paul CASPI : Towards recursive block diagrams. *Annual Review in Automatic Programming*, 18:81–85, 1994.

[CHP06a] Paul CASPI, Grégoire HAMON et Marc POUZET : Lucid Synchrone, un langage de programmation des systèmes réactifs. In Nicolas NAVET, éditeur : *Systèmes Temps-réel : Techniques de Description et de Vérification*, Informatique et Systèmes d'Information, pages 217–260, Paris, juin 2006. Hermès Science.

[CHP06b] Jean-Louis COLAÇO, Grégoire HAMON et Marc POUZET : Mixing signals and modes in synchronous data-flow systems. In Sang Lyul MIN et Yi WANG, éditeurs : *Proceedings of the 6th ACM International Conference on Embedded Software (EMSOFT 2006)*, pages 73–82, Séoul, Corée du Sud, octobre 2006. ACM Press.

[CMPP23] Jean-Louis COLAÇO, Michael MENDLER, Baptiste PAUGET et Marc POUZET : A constructive state-based semantics and interpreter for a synchronous data-flow language with state machines. *ACM Transactions on Embedded Computing Systems*, 22(5s):152:1–152:26, septembre 2023. Presenté à la 23<sup>ième</sup> conférence internationale sur l'Embedded Software (EMSOFT 2023).

[Coq25] COQ DEVELOPMENT TEAM : *The Coq proof assistant reference manual*. Inria, 2025. version 8.20.1.

[CPP05] Jean-Louis COLAÇO, Bruno PAGANO et Marc POUZET : A conservative extension of synchronous data-flow with state machines. In Wayne WOLF, éditeur : *Proceedings of the 5th ACM International Conference on Embedded Software (EMSOFT 2005)*, pages 173–182, Jersey City, États-Unis, septembre 2005. ACM Press.

[CPP17] Jean-Louis COLAÇO, Bruno PAGANO et Marc POUZET : Scade 6 : A formal language for embedded critical software development. In *Proceedings of the 11th International Symposium on Theoretical Aspects of Software Engineering (TASE 2017)*, pages 4–15, Nice, France, septembre 2017. IEEE Computer Society.
[Har87] David HAREL : Statecharts : A visual formalism for complex systems. *Science of Computer Programming*, 8(3):231-274, juin 1987.

[HCRP91] Nicolas HALBWACHS, Paul CASPI, Pascal RAYMOND et Daniel PILAUD : The synchronous dataflow programming language LUSTRE. *Proceedings of the IEEE*, 79(9):1305-1320, septembre 1991.

[Kah74] Gilles KAHN : The semantics of a simple language for parallel programming. *In Proceedings of the International Federation for Information Processing (IFIP) Congress 1974*, pages 471-475, Stockholm, Suède, août 1974. North-Holland.

[Ler09] Xavier LEROY : Formal verification of a realistic compiler. *Communications of the ACM*, 52(7):107-115, 2009.

[Mea55] George H. MEALY : A method for synthesizing sequential circuits. *Bell System Technical Journal*, 34(5):1045-1079, 1955.

[PM09] Christine PAULIN-MOHRING : A constructive denotational semantics for Kahn networks in Coq. In Yves BERTOT, Gérard HUET, Jean-Jacques LÉVY et Gordon PLOTKIN, éditeurs : *From Semantics to Computer Science : Essays in Honour of Gilles Kahn*, pages 383-413. Cambridge University Press, Cambridge, Royaume-Uni, 2009.

[Pou06] Marc POUZET : *Lucid Synchrone, version 3. Tutorial and reference manual*. Université Paris-Sud, avril 2006.

[XZH$^{+19}$] Li-yao XIA, Yannick ZAKOWSKI, Paul HE, Chung-Kil HUR, Gregory MALECHA, Benjamin C. PIERCE et Steve ZDANCEWIC : Interaction Trees : Representing recursive and impure programs in Coq. *Proceedings of the ACM on Programming Languages*, 4(POPL):article 51, janvier 2019.