#+TITLE: Programmation synchrone 2025/2026 -- Journal du cours
#+AUTHOR: Adrien Guatto
#+EMAIL: guatto@irif.org
#+LANGUAGE: fr
#+OPTIONS: ^:nil p:nil
#+LATEX_CLASS: article
#+LATEX_CLASS_OPTIONS: [a4paper,11pt]
#+LATEX_HEADER: \usepackage{a4wide}
#+LATEX_HEADER: \usepackage{microtype}
#+LATEX_HEADER: \hypersetup{hidelinks}
#+LATEX_HEADER: \usepackage[french]{babel}
# (org-latex-export-to-pdf)

* Cours 01 <2025-09-29>
  On lit le syllabus ainsi que le début des notes.

  Le manuel d'Heptagon peut être trouvé sur le dépôt git du projet. On peut
  cliquer sur le bouton /download/ pour télécharger une copie PDF.

  https://gitlab.inria.fr/synchrone/heptagon/-/blob/ec26be27b91f3e601b98b8b7e15e8d56d4b9afc7/manual/heptagon-manual.pdf
* Cours 02 <2025-10-06>
  On traite des constructions de base du langage.
* Cours 03 <2025-10-13>
  On traite des horloges et automates.
* Cours 04 <2025-10-20>
  On traite des automates et tableaux.
* Cours 05 <2025-10-27>
** Programmation Heptagon
   On traite des tableaux.
** Exemples
   On traite la génération d'échantillons audios, disponbile dans son
   [dossier](audio/).
* Cours 06 <2025-11-04>
** Projet
   On traite du fonctionnement du projet.
* Cours 07 <2025-11-10>
** Exemples
   On traite l'exemple du pendule inversé, disponible dans son
   [dossier](inverted-pendulum/).
** Implémentation des langages synchrones
  On commence à expliquer la compilation d'Heptagon, avec l'explication de
  MiniLS vers Obc jusqu'au traitement des horloges *exclu*.
* Cours 08 <2025-11-17>
** Implémentation des langages synchrones
   On discute de la compilation des horloges en MiniLS, de la traduction des
   automates et des structures de contrôle plus simples (notamment ~switch~) en
   Heptagon. On présente l'analyse d'initialisation.
* Cours 09 <2025-11-24>
** Implémentation des langages synchrones
   On termine la partie concernant l'implémentation des langages synchrones.
** Vérification automatique
   L'outil Kind2 est un vérificateur de modèle (/model checker/) pour un langage
   proche d'Heptagon développé à l'université de l'Iowa.

   https://kind.cs.uiowa.edu

   Un tel outil est une des justifications pour l'emploi d'un langage très
   limité comme Heptagon, SCADE et leurs variantes. La vérification automatique
   est beaucoup plus difficile lorsque le langage d'entrée est un langage
   généraliste comme C, Python ou OCaml.
*** Introduction
    Le langage accepté par Kind2 est une variante d'Heptagon beaucoup plus
    proche de son ancêtre Lustre. Les différences sont assez mineures mais
    peuvent rendre l'écriture du code désagréable lorsqu'on est habitué aux
    constructions d'Heptagon.

    Par exemple, le langage ne propose pas l'opérateur ~fby~, uniquement ~pre~
    et ~->~. Notre classique compteur doit donc être écrit comme suit.

    #+BEGIN_SRC
node counter() returns (o : int)
let
  o = 0 -> (pre o + 1);
tel
    #+END_SRC

    Kind2 est capable de traduire ce programme vers du code impératif, jouant
    ainsi le même rôle que le compilateur ~heptc~ pour Heptagon. Plutôt que de
    générer du code C, Kind2 produit du code Rust.

    #+BEGIN_SRC
$ kind2 --compile true ex0.lus
  kind2 v1.1.0-16-g9572d9b

<Note> System counter has no property, skipping verification step.

--------------------------------------------------------------------------------
Post-analysis: rust generation

<Note> Compilation to Rust is still a rather experimental feature:
       in particular, arrays are not supported.

  Compiling node "counter" to Rust in `ex0.lus.out/counter/implem`.

  Done compiling.

--------------------------------------------------------------------------------
$ wc -l ex0.lus.out/counter/implem/src/main.rs
366 ex0.lus.out/counter/implem/src/main.rs
    #+END_SRC

    L'intérêt principal de Kind2 est ailleurs : il est capable de /vérifier
    formellement/ des propriétés. Par opposition au test, la vérification
    formelle permet de vérifier qu'une propriété est vraie pour *toute* entrée,
    plutôt que pour une entrée particulière. De plus, dans le cas des langages
    synchrones, les entrées sont des suites infinies, dont on ne peut tester
    qu'un préfixe fini. La vérification formelle, elle, considère des entrées de
    longueur infinie.

    Lorsqu'on découvre un outil de vérification formelle, un des premières
    questions à se poser est celle du langage dans lequel les propriétés sont
    écrites. Certains outils de vérification offrent un langage spécialisé pour
    ce faire, par exemple une logique temporelle pour le model-checker PRISM.
    Les outils de vérification de langages synchrones comme Kind2 font un choix
    un peu différent. Le langage des propriétés est le même que celui des
    programmes, et la propriété à vérifier est exprimée par un flot booléen
    désigné par l'utilisateur doit toujours être vrai. Avec cette approche, on
    va avoir tendance à écrire des /observateurs synchrones/, c'est-à-dire des
    noeuds qui sont utilisés uniquement pour vérifier que le noeud qui va être
    déployé sur le système embarqué final va respecter certaines propriétés,
    éventuellement sous certaines hypothèses concernant ses entrées.

    #+BEGIN_SRC
node top() returns (ok : bool)
var o : int;
let
  o = counter();
  ok = o >= 0;
  --%PROPERTY ok;
tel
    #+END_SRC

    En lançant Kind2 sur ce fichier, on lui demande de vérifier que le flot ~ok~
    est toujours vrai. Il est capable de vérifier que c'est le cas, même si ~ok~
    contient une infinité de valeurs.

    #+BEGIN_SRC
$ kind2 ex0.lus
 kind2 v1.6.0

====================================================================================================================
Analyzing top
  with First top: 'top'
             subsystems
               | concrete: counter

<Success> Property ok is valid by property directed reachability after 0.148s.

--------------------------------------------------------------------------------------------------------------------
Summary of properties:
--------------------------------------------------------------------------------------------------------------------
ok: valid (at 1)
====================================================================================================================
    #+END_SRC

    (Cet exemple montre que Kind2 suppose que la sémantique du type ~int~ de
    Lustre est celle des entiers relatifs, sans limite de taille. Pourquoi ?
    Remarquons que jusqu'ici on avait supposé que les types des langages
    synchrones étaient tous finis, ce qui assurait la finitude de la mémoire.
    Comme on le décrira plus bas, ce choix n'est pas sans conséquences
    théoriques et pratiques.)

    Cet exemple laisse aussi deviner que la vérification est un processus
    coûteux, beaucoup plus coûteux que la compilation. Ce fichier étant écrit
    dans le sous-ensemble commun à Heptagon et Lustre, on peut le compiler avec
    ~heptc~ et comparer le temps de compilation au temps de vérification.

    #+BEGIN_SRC
$ time heptc -target c ex0.lus
real    0m0,026s
user    0m0,013s
sys     0m0,013s
    #+END_SRC

    On peut montrer des propriétés un peu plus intéressantes, par exemple en
    écrivant une variante du compteur avec une valeur d'initialisation.

    #+BEGIN_SRC
node counterini(ini : int) returns (o : int)
let
  o = ini -> (pre o + 1);
tel

node top(ini : int) returns (ok : bool)
var o : int;
let
  o = counterini(ini);
  ok = o >= 0;
  check ok;
tel
    #+END_SRC

    Cet exemple est plus intéressant que le précédent en ce que le noeud ~top~
    dispose désormais d'une entrée. Kind2 va donc essayer de vérifier que toutes
    les valeurs de la suite ~ok~ sont vraies et ce /pour toutes les suites
    d'entrée ~ini~/. Va-t-il réussir ?

    #+BEGIN_SRC shell
$ kind2 ex0.lus
 kind2 v1.6.0

====================================================================================================================
Analyzing top
  with First top: 'top'
             subsystems
               | concrete: counterini

<Failure> Property ok is invalid by bounded model checking for k=0 after 0.041s.

Counterexample:
  Node top ()
    == Inputs ==
    ini    -1
    == Outputs ==
    ok  false
    == Locals ==
    o      -1

  Node counterini (top[l14c7])
    == Inputs ==
    ini -1
    == Outputs ==
    o   -1


--------------------------------------------------------------------------------------------------------------------
Summary of properties:
--------------------------------------------------------------------------------------------------------------------
ok: invalid after 0 steps
====================================================================================================================
    #+END_SRC

    La vérification a échoué, mais Kind2 nous a fourni un contre-exemple sous la
    forme d'une séquence d'entrées qui falsifie la propriété. Il suffit bien sûr
    de donner un ~ini~ strictement négatif au premier instant !

    Notre propriété est donc fausse. Peut-on exprimer que le flot ~o~ est
    toujours vrai mais *à condition* que la première valeur de ~ini~ soit
    positive ? Oui, en utilisant l'opérateur booléen d'implication pour exprimer
    une /précondition/ (hypothèse) sur l'entrée ~ini~.

    (Remarque : l'implication dont il s'agit ici n'est que l'opérateur
    combinatoire sur les flots défini par ~x => y = not x or y~, rien de plus.
    En particulier, Kind2 n'a aucun traitement spécifique de cet opérateur.)

    Un premier essai pourrait ressembler à ce qui suit.

    #+BEGIN_SRC
node top(ini : int) returns (ok : bool)
var o : int;
let
  o = counterini(ini);
  ok = ((ini >= 0) -> true) => (o >= 0);
  check ok;
tel
    #+END_SRC

    La vérification échoue encore, avec le contre-exemple qui suit.

    #+BEGIN_VERBATIM
Counterexample:
  Node top ()
    == Inputs ==
    ini    -2     0
    == Outputs ==
    ok   true false
    == Locals ==
    o      -2    -1

  Node counterini (top[l19c7])
    == Inputs ==
    ini -2  0
    == Outputs ==
    o   -2 -1
    #+END_VERBATIM

    Comment comprendre ce contre-exemple ? Au premier instant, ~i~ vaut ~-2~ et
    la précondition sur ~ini~ est fausse, donc l'implication est vraie. Au
    deuxième instant, la précondition sur ini est vraie, donc l'implication
    prend la valeur de ~o >= 0~, qui se trouve fausse.

    Quel est le problème ? Ce que nous avions en tête n'est pas ce que nous
    avons écrit. On aurait voulu dire "si ~ini < 0~ au premier instant, la
    précondition est fausse pour toujours", mais on a écrit "si ~ini < 0~ au
    premier instant, la précondition est fausse /au premier instant/". On peut
    régler le problème en introduisant un noeud ~always~ dont la sortie devient
    fausse pour toujours dès que son entrée est fausse.

    #+BEGIN_SRC
node always(b : bool) returns (o : bool)
let
  o = (true -> pre o) and b;
tel

node top(ini : int) returns (ok : bool)
var o : int;
let
  o = counterini(ini);
  ok = always((ini >= 0) -> true) => (o >= 0);
  check ok;
tel
    #+END_SRC

    La vérification réussit. En particulier, le contre-exemple précédent n'est
    plus valide. Si la valeur initiale de ~ini~ est ~-2~, la valeur de
    ~always((ini >= 0) -> true)~ sera toujours fausse, et donc la vérité de
    l'implication dépendra de ~o >= 0~, toujours vraie.

    Le fait d'exprimer une précondition sur les entrées est très fréquent, et
    Kind2 propose une syntaxe un peu plus agréable pour ce faire.

    #+BEGIN_SRC
node top(ini : int) returns (ok : bool)
var o : int;
let
  o = counterini(ini);
  ok = o >= 0;
  check ok provided always((ini >= 0) -> true);
tel
    #+END_SRC
*** Comparaison de noeuds
    On peut utiliser le principe des observateurs synchrones pour comparer le
    comportement de deux noeuds, et éventuellement tester leur équivalence.

    Par exemple, comment quelle relation voyez vous entre notre premier noeud
    ~counter~ et le noeud ~counterini~ ? Et comment la feriez-vous vérifier par
    Kind2 ?

    Le lien est essentiellement qu'ajouter la première valeur de ~ini~ à la
    sortie de ~counter~ donne celle de ~counterini~. La tentative donnée
    ci-dessous est trop naïve puisqu'il ne faut prendre en compte ~ini~
    uniquement au premier instant.

    #+BEGIN_SRC
node compare(ini : int) returns (ok : bool)
let
  ok = counter() + ini = counterini(ini);
  check ok;
tel
    #+END_SRC

    On peut utiliser un noeud ~constant~ qui maintient la valeur reçue au
    premier instant. On obtient le noeud suivant, dont la propriété est
    vérifiée.

    #+BEGIN_SRC
node constant(ini : int) returns (o : bool)
let
  o = ini -> pre o;
tel

node compare(ini : int) returns (ok : bool)
let
  ok = counter() + constant(ini) = counterini(ini);
  check ok;
tel
    #+END_SRC
*** Les contrats
    Les propriétés qu'on a vérifié jusqu'ici sont des propriétés globales du
    système. Il s'agit certainement d'une approche utile, mais elle n'est pas
    tout à fait convaincante du point de vue du génie logiciel. On aimerait
    plutôt vérifier chaque noeud indépendamment. Kind2 le permet via l'écriture
    de /contrats/ qui permettent à chaque noeud de documenter ses attentes
    vis-à-vis de ses appelants (mot-clef /assume/) et ses garanties (mot-clef
    /guarantee/).

    #+BEGIN_SRC
node counterini(ini : int) returns (o : int)
(*@contract
   assume (ini >= 0) -> true;
   guarantee o >= 0;
   *)
let
  o = ini -> (pre o + 1);
tel
    #+END_SRC

    Notez que Kind2 assure la bonne sémantique pour l'hypothèse (/assume/),
    c'est-à-dire qu'elle doit être valide de toute la séquence d'entrées, et ce
    sans avoir à utiliser une noeud comme ~always~. (Pour ceux et celles d'entre
    vous qui connaissent la logique temporelle, si $A$ est la formule booléenne
    des hypothèses et $G$ est la formule booléenne des garanties, la formule que
    l'outil cherche à démontrer est $\square A \Rightarrow \square G$ plutôt que
    $\square A \Rightarrow \square G$.

    Je finis cette partie pratique par une difficulté à laquelle tous les
    utilisateurs de vérification formelle finissent par se heurter un jour ou
    l'autre : des hypothèses trop fortes rendent la garantie triviale. Voir
    ci-dessous pour un exemple caricatural ; /garbage in, garbage out/.

    #+BEGIN_SRC
node counterini(ini : int) returns (o : int)
(*@contract
   assume false;
   guarantee (o = constant(o));
   *)
let
  o = ini -> (pre o + 1);
tel
    #+END_SRC

    Cependant, Kind2 aide à détecter le problème. L'outil va chercher à vérifier
    que tout appelant à ce ~counterini~ satisfait aux hypothèses, ce qui ici est
    impossible... Sauf si l'appelant a lui-même fait des hypothèses
    contradictoires sur ses entrées, bien entendu !
* Cours 10 <2025-12-01>
** Vérification automatique, suite
*** Exemples
**** Compteurs
     On va s'intéresser à la vérification d'équivalence entre compteurs
     périodiques de 0 à 3, formulé avec des entiers, puis en codage binaire,
     classique puis de Gray.

     On commence par écrire le compteur sur deux bits avec un entier

     #+BEGIN_SRC
node intcounter (rst : bool; const max : int) returns (out : bool);
var t : int;
let
  t = 0 -> if rst or pre t = max then 0 else pre t + 1;
  out = t = 3;
tel

node graycounter (rst : bool) returns (out : bool);
var a, b : bool;
let
  a = false -> (not rst and not pre b);
  b = false -> (not rst and pre a);
  out = not a and b;
tel

node bincounter (rst : bool) returns (out : bool);
var a, b : bool;
let
  a = false -> (not rst and (pre a <> pre b));
  b = false -> (not rst and not pre b);
  out = a and b;
tel

node top (rst : bool) returns ();
var grayc, binc, intc : bool;
let
  grayc = graycounter(rst);
  intc = intcounter(rst, 3);
  binc = bincounter(rst);
  check binc = intc;
  check grayc = intc;
tel
     #+END_SRC
*** Les bases de l'algorithmique de la vérification
    Les données du problème sont :

    1. un programme synchrone à vérifier,

    2. un /observateur/ pour la propriété à démontrer (~check ok~),

    3. un /observateur/ pour l'hypothèse supposée (~assert hyp~).

    L'objectif d'un vérificateur de modèle pour un programme synchrone à flots
    de données est de démontrer :

    ~always(so_far(hyp) => ok)~.

    Notons qu'on ne traite que les propriétés de sûreté (``quelque-chose de
    mauvais n'arrive toujours'') et pas de vivacité (``quelque-chose de bon
    finit toujours par arriver''), comme expliqué au cours précédent.

    On va s'intéresser à ce problème dans le cas *purement booléen*,
    c'est-à-dire où toutes les variables manipulées sont des suites de
    booléens. Notre description est basée sur le rapport de recherche de Pascal
    Raymond disponible à
    [[https://www.di.ens.fr/~pouzet/cours/mpri/bib/lesar-rapport.pdf][cette
    adresse]].

    Si $X$ est un ensemble, on écrit $\overline{X}$ pour les fonctions de $X$
    dans $\mathbb{B}$, qui sont en bijection avec les parties de $X$. On
    identifiera librement les sous-ensembles et leurs fonctions
    charactéristiques dans ce qui suit.

    Les données du problème sont les n-uplets ($V$, $S$, $I \subseteq
    \overline{S}$, $g : \overline{S} \times \overline{V} \to \overline{S}$, $H
    \subseteq \overline{S} \times \overline{V}$, $\Phi \overline{S} \times
    \overline{V}$), où :

    - $S$ et $V$ sont des ensembles *finis* dont les éléments sont
      respectivement les variables d'état de d'entrée du programme,

    - $I$ est l'ensemble des états initiaux,

    - $H$ est l'hypothèse,

    - $\Phi$ est la propriété à démontrer.

      On écrira $q \to^v q'$ pour $q' = g(q, v)$ avec $q,q' \in \overline{S}$ et
      $v \in \overline{V}$.

      On définit les états successeur/prédécesseurs d'un état $q$ ou d'un
      ensemble d'états~$X$ par :

      \begin{align*}
        post_H(q) & = \{ q' \mid \exists v \in q \to_v q' \wedge H(q, v) \}
        \\
        pre_H(q) & = \{ q' \mid \exists v \in q' \to_v q \wedge H(q', v) \}
        \\
        POST_H(X) & = \bigcup_{q \in X} post_H(q)
        \\
        PRE_H(X) & = \bigcup_{q \in X} pre_H(q)
      \end{align*}

      L'ensemble des états d'erreurs immédiate sont ceux qui satisfont
      l'hypothèse mais pas la propriété à démontrer.

      \[
        Err = \{ q \mid \exists v, H(q, v) \wedge \neg \Phi(q, v) \}
      \]

      On définit maintenant l'ensemble $Acc$ des états accessibles du programme
      et l'ensemble $Bad$ des mauvais états par un plus petit point fixe
      ensembliste : $\mu X . F(X)$ désigne le plus petit ensemble $Y$ tel que
      $F(Y) \subseteq Y$ ; son existence est garantie dès lors que $F$ est
      croissante pour l'inclusion.

      \begin{align*}
        Acc & = \mu X. (I \cup POST_H(X))
        \\
        Err & = \{ q \mid \exists v, H(q, v) \wedge \neg \Phi(q, v) \}
        \\
        Bad & = \mu X . (Err \cup PRE_H(X))
      \end{align*}

      L'objectif est maintenant de démontrer que le système est *sûr*,
      c'est-à-dire que $Acc \cap Bad = \emptyset$. Autrement dit, aucun état
      accessible du système n'est un état d'erreur.

      Pour ce faire, il existe deux grandes méthodes :

      - l'exploration en *avant* : on démontre $Acc \cap Err = \emptyset$,

      - l'exploration en *arrière* : on démontre $Bad \cap I = \emptyset$.

      L'approche la plus simple pour ce faire est une approche énumérative : on
      explore explicitement l'automate induit par le programme, en imitant le
      calcul du plus petit point fixe correspondant à $Acc$ ou $Bad$.

      #+BEGIN_SRC
Known := I; Explored := {}
while there is q in Known \ Explored:
  for all q' in post(q):
    if q' in Err:
      return FAILURE
    move q' to Known
  move q to Explored
}
return SUCCESS
      #+END_SRC

      Cet algorithme peut être implémenté et termine puisque tous les ensembles
      manipules sont finis, les prédicats calculables, tout comme la fonction de
      transition du programme. En particulier, vous pouvez implémenter les
      ensembles ~Known~ et ~Explored~ par votre structure d'ensemble fini
      favorite, et énumérer les valeurs possibles pour calculer ~post(q)~. Il
      s'agit donc en somme d'exécuter le programme sur toutes les entrées
      possibles ; on voit que c'est très inefficace.

      On peut aussi implémenter une version en arrière.

      #+BEGIN_SRC
Known := Err; Explored := {}
while there is q in Known \ Explored:
  for all q' in pre(q):
    if q' in I:
      return FAILURE
    move q' to Known
  move q to Explored
}
return SUCCESS
      #+END_SRC

      Les deux algorithmes sont très inefficaces, tellement qu'ils en deviennent
      inutilisables en pratique. En effet, les structures de données
      représentant les ensembles d'état ou d'entrées deviendront très grosses,
      et les calculs attenants (différence ensembliste, ajout, choix d'un
      élément...) coûteux à réaliser.

      Notons que le second algorithme est encore moins efficace que le
      premier. Voyez-vous pourquoi ? Le calcul de ~pre(q)~ est encore plus
      coûteux, puisqu'il faut calculer l'image inverse de la fonction de
      transition $g$, c'est-à-dire trouver l'ensemble des $q'$ tel que $g(q', v)
      = q$ pour $v$ et $q$ fixés.

      Depuis les années 1990, on utilise plutôt des méthodes dites
      *symboliques*. L'idée générale est de représenter les ensembles finis par
      des formules logiques plutôt que par des énumérations explicites. Par
      exemple, on pourrait représenter l'ensemble $\{ (x, y, z) \mid x
      \overline{y} + z = 1 \}$ directement par le *code* de sa fonction
      caractéristique $f(x, y, z) = x \overline{y} + z$ plutôt qu'explicitement
      par l'ensemble de triplets $\{ (1, 0, 0), (1, 0, 1), (0, 0, 1), (0, 1, 1),
      (1, 1, 1) \}$. Les méthodes symboliques sont donc un exemple de compromis
      temps-espace : on y gagne une représentation nettement plus succincte des
      données que la représentation explicite, en contrepartie de quoi les
      opérations (notamment test d'égalité, du vide, d'inclusion, etc.) seront
      plus coûteuses.

      Il existe deux grandes méthodes d'implémentation pour exprimer les
      opérations et les tests :

      1. On peut représenter les formules directement par leur code et utiliser
         un solveur SAT général pour répondre aux questions intéressantes pour
         la vérification. Par exemple, l'ensemble $\{ \vec{x} \mid \phi(\vec{x})
         \}$ est inclus dans l'ensemble $\{ vec{x} \mid \psi(\vec{x}) \}$ si et
         seulement si $\forall \vec{x}, \phi(\vec{x}) \implies \psi(\vec{x})$,
         question à laquelle un solveur SAT peut répondre, y compris pour de
         très grosses formules $\phi$ et $\psi$. D'autres questions, comme par
         exemple l'énumération des valeurs appartenant à un ensemble, sont d'un
         traitement moins direct mais peuvent être gérée avec un peu de
         réflexion et d'effort.

     2. On peut utiliser une représentation canonique des formules booléennes,
        par exemple les /diagrammes de décision binaire/ (ou /binary decision
        diagrams/ en anglais, BDD). Ici, toutes les formules équivalentes sont
        représentées par la même structure de données. La construction de cette
        représentation est donc forcément coûteuse, mais une fois construite on
        peut l'utiliser pour répondre efficaement à beaucoup de questions. C'est
        cette approche qui est très bien exposée dans le rapport de P. Raymond
        cité plus haut.

     Le principe des diagrammes de décision binaire a été brièvement expliqué en
      cours mais ne sera pas détaillé dans ces notes.
