information theory, 29(2):198-208, 1983.

[19] Son Ho, Jonathan Protzenko, Abhishek Bichhawat, and Karthikeyan Bhargavan. Noise*: A library of verified high-performance secure channel protocol implementations. In *IEEE Symposium on Security and Privacy (S&P)*, pages 107-124, 2022.

[20] Inria-Prosecco. TreeSync: Supplementary material, 2022. https://github.com/Inria-Prosecco/treesync.

[21] Nadim Kobeissi, Karthikeyan Bhargavan, and Bruno Blanchet. Automated verification for secure messaging protocols and their implementations: A symbolic and computational approach. In *IEEE European symposium on security and privacy (EuroS&P)*, pages 435-450. IEEE, 2017.

[22] Moxie Marlinspike and Trevor Perrin. Signal protocol, 2016. https://signal.org/docs.

[23] Moxie Marlinspike and Trevor Perrin. The X3DH key agreement protocol, 2016. https://signal.org/docs/specifications/x3dh/.

[24] Guido Martínez, Danel Ahman, Victor Dumitrescu, Nick Giannarakis, Chris Hawblitzel, Catanlin Hritcu, Monal Narasimhamurthy, Zoe Paraskevopoulou, Clément Pit-Claudel, Jonathan Protzenko, Tahina Ramananandro, Aseem Rastogi, and Nikhil Swamy. Meta-F*: Proof automation with SMT, tactics, and metaprograms. In Luís Caires, editor, *Programming Languages and Systems - European Symposium on Programming, ESOP, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS, Proceedings*, volume 11423 of *Lecture Notes in Computer Science*, pages 30-59. Springer, 2019.

[25] Simon Meier, Benedikt Schmidt, Cas Cremers, and David Basin. The Tamarin prover for the symbolic analysis of security protocols. In *International conference on computer aided verification*, pages 696-701. Springer, 2013.

[26] Tobias Nipkow, Lawrence C Paulson, and Markus Wenzel. Isabelle/HOL: a proof assistant for higher-order logic, volume 2283. Springer Science & Business Media, 2002.

[27] Lawrence Paulson. The inductive approach to verifying cryptographic protocols. *Journal of Computer Security*, 6, 12 2000.

[28] Jonathan Protzenko, Benjamin Beurdouche, Denis Merigoux, and Karthikeyan Bhargavan. Formally verified cryptographic web applications in webassembly. In *IEEE Symposium on Security and Privacy (S&P)*, pages 1256-1274. IEEE, 2019.

[29] Aseem Rastogi, Guido Martínez, Aymeric Fromherz, Tahina Ramananandro, and Nikhil Swamy. Programming and proving with indexed effects, 2021. https://www.fstar-lang.org/papers/indexedeffects/.

[30] Eric Rescorla. The Transport Layer Security (TLS) Protocol Version 1.3. RFC 8446, August 2018.

[31] Nikhil Swamy, Cătălin Hriţcu, Chantal Keller, Aseem Rastogi, Antoine Delignat-Lavaud, Simon Forest, Karthikeyan Bhargavan, Cédric Fournet, Pierre-Yves Strub, Markulf Kohlweiss, Jean-Karim Zinzindohoue, and Santiago Zanella-Béguelin. Dependent types and multi-monadic effects in F*. In *ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL)*, pages 256-270, 2016.

[32] Théophile Wallez. Unambiguous signatures. MLS protocol, pull-request #526, 2021. https://github.com/mlswg/mls-protocol/pull/526.

[33] Théophile Wallez. Improve parent hash guarantees. MLS protocol, pull-request #713, 2022. https://github.com/mlswg/mls-protocol/pull/713.

[34] Théophile Wallez. Include leaf index in LeafNodeTBS for better parent-hash guarantees. MLS protocol, pull-request #731, 2022. https://github.com/mlswg/mls-protocol/pull/731.

[35] Théophile Wallez. MLS protocol, comment on pull-request #713, 2022. https://github.com/mlswg/mls-protocol/pull/713#issuecomment-1146371281.

[36] Théophile Wallez. MLS protocol, comment on pull-request #713, 2022. https://github.com/mlswg/mls-protocol/pull/713#issuecomment-1146599668.

[37] Théophile Wallez. Stronger parent hashes for authenticated identities. MLS protocol pull-request
#527, 2022. https://github.com/mlswg/mls-protocol/pull/527.

[38] Théophile Wallez, Jonathan Protzenko, Benjamin Beurdouche, and Karthikeyan Bhargavan. Tree-Sync : Authenticated group management for messaging layer security. Cryptology ePrint Archive, Paper 2022/1732, 2022. https://eprint.iacr.org/2022/1732.

[39] Jean-Karim Zinzindohoué, Karthikeyan Bhargavan, Jonathan Protzenko, and Benjamin Beurdouche. HACL* : A verified modern cryptographic library. In *ACM SIGSAC Conference on Computer and Communications Security (CCS)*, pages 1789–1806, 2017.
Articles courts
# Comment dompter un troupeau de flottants sauvages ?

Arthur Correnson

CISPA Helmholtz Center for Information Security

arthur.correnson@cispa.de

École Normale Supérieure de Rennes

arthur.correnson@ens-rennes.fr

## Résumé

Les nombres flottants tels que définis dans le standard IEEE-754 sont la solution la plus répandue pour approximer les nombres réels en machine. Toutefois, en pratique, de nombreux environnements logiciels et matériels présentent des subtilités non conformes avec ce standard. Cela complique la tâche de raisonner formellement sur les programmes effectuant des calculs numériques sans connaître *a priori* leur environnement d'exécution. Dans cet article, nous montrons l'impact de ce problème sur le compilateur CompCert, un compilateur formellement vérifié pour le langage C et proposant un support pour les flottants IEEE-754. Nous présentons les résultats d'un travail d'investigation visant à measurez les difficultés liées à l'intégration de nouveaux types de flottants dans CompCert. Cette étude est motivée par la volonté d'étendre le compilateur à des cibles non conformes IEEE-754 utilisées, par exemple, en informatique embarquée.

## Introduction

**Contexte** Représenter de manière exacte les nombres réels est impossible dans la mémoire finie d'un ordinateur. Les nombres flottants répondent à ce problème et propose une méthode pour approximer les nombres réels de manière finie au prix d'une perte de précision. Le standard IEEE-754 [2] normalise la notion de nombres flottants et définit un encodage binaire de ces nombres ainsi que le comportement attendu des opérations arithmétiques associées.

Malgré l'existence d'un standard pour l'implémentation des nombres flottants, de nombreux environnements logiciels et matériels présentent des spécificités non conformes IEEE-754. Ces particularités résultent souvent de contraintes techniques comme par exemple le coût de fabrication d'un processeur flottant ou la rapidité des calculs. Cette grande diversité des nombres flottants pose un véritable problème de compréhension des résultats produits par les programmes effectuant des calculs numériques. En effet, sans connaître au préalable l'environnement dans lequel va être exécuté un programme, anticiper le résultat des opérations flottantes devient pratiquement impossible. Ce problème est d'autant plus flagrant dans le contexte de la programmation certifiée dont le but est de prouver formellement que le comportement d'un programme est préservé par la compilation. Dans ce contexte, il est nécessaire de s'entendre sur l'interprétation des nombres flottants dans les langages de programmation mais également dans les environnements d'exécution ciblés par la compilation.

Le compilateur CompCert [10, 11, 9] est un compilateur certifié pour le langage C entièrement prouvé grâce à l'assistant de preuve Coq [1]. CompCert fait le choix de fixer l'usage du standard IEEE-754 [5], limitant ainsi la compilation à des cibles dont le traitement des flottants est conforme au standard. Toute la chaîne de compilation de CompCert dépendant fortement de ce choix, l'intégration d'un support pour de nouveaux types de nombres flottants pose plusieurs défis en matière d'ingénierie logicielle. Une première problématique est de rendre interchangeable le modèle de calcul flottant du compilateur sans invalider la chaîne de compilation et sa preuve de correction. Au delà de cette question, la tâche de formaliser en Coq de nouveaux
modèles de calcul flottant est difficile en elle-même et impose en particulier de s'assurer que les spécifications en Coq sont bien conformes aux documentations de référence.

**Contributions** Dans cet article nous présentons les résultats d'un travail d'investigation visant à mesurer les difficultés liées à l'intégration de nouveaux types de flottants dans CompCert. Cette étude effectuée au sein de l'entreprise AbsInt est motivée par la volonté d'étendre le compilateur à des cibles non conformes IEEE-754 utilisées notamment en informatique embarquée.

**Plan** Nous commençons par introduire le problème de la diversité des nombres flottants en présentant des exemples concrets (1). Nous exposons ensuite la notion de compilation certifiée et en particulier la compilation des nombres flottants dans le compilateur CompCert (2). Enfin, nous discutons des difficultés engendré par l'intégration de nouveaux types de flottants dans CompCert (3) et nous proposons plusieurs pistes de réflexion (4).

# 1 Les nombres flottants et le standard IEEE-754

**Les nombres flottants IEEE** Le standard IEEE-754 définit une représentation binaire des nombres flottants sur 16, 32 et 64 bits. Pour le cas des flottants 32 bits par exemple, l'encodage comporte 1 bit de signe (s), 8 bits d'exposant (exp) et les 23 bits restants pour représenter une partie fractionnaire (frac). En fonction des valeurs exactes de chaque champs, les nombres flottants sont interprétés au choix parmi 5 types de valeurs :

<table><thead><tr><th>Valeurs</th><th>Interprétation</th><th>condition</th></tr></thead><tbody><tr><td>NaN</td><td>valeur indéterminée</td><td>exp = 255, frac &gt; 0</td></tr><tr><td>+∞, -∞</td><td>infinis signés en fonction du bit s</td><td>exp = 255, frac = 0</td></tr><tr><td>+0, -0</td><td>zéros signés en fonction du bit s</td><td>exp = 0, frac = 0</td></tr><tr><td>Nombres normalisés</td><td>(-1)<sup>s</sup> × 2<sup>exp -127</sup> × (1.frac)<sub>2</sub></td><td>1 ≤ exp &lt; 255</td></tr><tr><td>Nombres dénormalisés</td><td>(-1)<sup>s</sup> × 2<sup>exp -127</sup> × (0.frac)<sub>2</sub></td><td>exp = 0, frac &gt; 0</td></tr></tbody></table>

Le standard introduit également plusieurs notion d'arrondi associant à tout réel $x$ une représentation flottante $round_m(x)$ ($m$ est un mode d'arrondi). Les opérations arithmétiques sont ensuite définies comme devant être l'arrondi de leur pendant réel. Par exemple pour l'addition flottante en mode d'arrondi $m$ (notée $\oplus_m$), on a $x \oplus_m y := round_m(x + y)$. Notons que la présence d'un arrondi dans la définition suffit à invalider certaines propriétés arithmétiques comme l'associativité de l'addition.

**Le standard et le mode d'arrondi par défaut** Parmi les 5 modes d'arrondi définis dans le standard IEEE-754, le mode "au plus proche pair" arrondit tout réel au plus proche flottant dont la représentation binaire a un bit de poids faible pair. Ce mode spécifique est utilisé par défaut dans de très nombreux environnements, si bien que l'on précise rarement le mode d'arrondi explicitement dans les langages de programmation. Cependant, il est parfois préférable d'utiliser d'autres modes pour effectuer certains calculs. Ce choix d'un mode d'arrondi est donc un facteur qui contribue aux différences observables entre environnements de calcul flottants, y-compris entre environnements conformes au standard IEEE-754.

**Des imprécisions au niveau logiciel** Les langages de programmation ne sont pas toujours précis en ce qui concerne l'arithmétique flottante. La norme ISO du langage C [8] par exemple
laisse une grande liberté dans le traitement des opérations flottantes (voir figure 1). En particulier, l'usage du standard IEEE-754 n'est pas requis mais plutôt recommandé. Il en résulte qu'un même programme C peut produire des résultats flottants différents selon le compilateur utilisé, la machine qui exécute le programme ou même selon la machine qui exécute le compilateur. Ces imprécisions du langage C ainsi que d'autres langages sont davantage détaillées par Sylvie Boldo et ses contributeurs [6, 4].

> The accuracy of the floating-point operations (+, -, *, /) and of the library functions in <math.h> and <complex.h> that return floating-point results is implementation-defined. The implementation may state that the accuracy is unknown

<caption>FIGURE 1 – Extrait de ISO/IEC 9899, section 5.2.4.2.2 "characteristics of floating types"</caption>

Des divergences au niveau matériel La plupart des processeurs modernes embarquent une unité de calcul flottant. Les processeurs grand-public que l'on trouve dans les ordinateurs personnels implémentent généralement le standard IEEE-754. Toutefois, certaines familles de processeurs utilisés dans des domaines spécifiques (informatique embarquée, traitement du signal, etc) prennent des libertés par rapport au standard. Par exemple, le standard SPE (Signal Processing Engine) et un document normatif décrivant une famille d'architectures matérielles dédiées au traitement du signal. Cette norme diffère explicitement du standard IEEE en autorisant que les opérations usuelles ne produisent pas de valeurs spéciales (infinis, NaN) ou de nombres dénormalisés (voir figure 2). Des règles spécifiques sont définies en remplacement.

> Embedded floating-point operations do not produce +Inf, -Inf, NaN, or a denormalized number. [...] Thus, whenever an input operand of the embedded floating-point instruction has data values that are +infinity, -infinity, alized, NaN, or when the result of an operation produces an overflow or an underflow, an embedded floating-point data interrupt may be taken and the interrupt handler is responsible for delivering IEEE 754-compliant behavior if desired

<caption>FIGURE 2 – Extrait de Signal Processing Engine (SPE) Programming Environments Manual, section 3.3.1.4 about IEEE Std 754 Compliance</caption>

# 2 Vérifier la compilation des nombres flottants

## 2.1 Préserver la sémantique

La compilation certifiée a pour but de s'assurer que le sens des programmes est conservé lorsqu'ils sont traduits en exécutables. Cela permet de garantir que l'intention du programmeur n'est pas détériorée par le compilateur, par exemple en effectuant des optimisations hasardées. Le caractère parfois contre-intuitif de l'arithmétique flottante est typiquement source
d'optimisations incorrectes. Par exemple, en nombres flottants, $x \oplus 0.0$ ne peut pas toujours être optimisé en $x$. En effet, dans le cas où $x = -0.0$, le standard IEEE impose que le résultat de $-0.0 + 0.0 = +0.0$ et $+0.0 \neq -0.0$. Certifier un compilateur permet de contrôler ce type d'erreurs.

Pour garantir qu'un compilateur préserve le sens des programmes, il est nécessaire de définir au préalable la sémantique des langages sources et cibles considérés pour la compilation. Pour un langage donné $\mathcal{L}$, un programme $P \in \mathcal{L}$ et un comportement observable $C$, on définit la relation $P \downarrow C$ qui se lit comme "C est un comportement observable lors de l'exécution du programme P". Dans le cadre de la compilation d'un langage $\mathcal{L}_{source}$ vers $\mathcal{L}_{cible}$, un compilateur peut être vu comme une fonction partielle compile : $\mathcal{L}_{source} \to \mathcal{L}_{cible}$. Étant données deux sémantiques $\downarrow_{source}$ et $\downarrow_{cible}$ décrivant l'exécution des programmes sources et cibles, certifier le compilateur compile revient alors à démontrer le théorème suivant [10] :

$$ \forall P \in \mathcal{L}_{source}, \forall P' \in \mathcal{L}_{cible}, \forall C, \text{compile}(P) = P' \Rightarrow (P \downarrow_{source} C \iff P' \downarrow_{cible} C) $$

Cette équivalence assure que les programmes compilés se comportent exactement comme dicté par leur code source. Notons que cette équivalence est souvent trop restrictive, en particulier dans le cas où le langage source est non-déterministe. D'autres variations de l'énoncé de correction d'un compilateur sont discutées dans les travaux de Xavier Leroy [10]. Le logiciel CompCert suit cette approche et propose d'implémenter un compilateur C dans l'assistant à la démonstration Coq. Cela permet de réaliser la preuve formelle de la correction du compilateur.

## 2.2 Modéliser la sémantique des nombres flottants

La définition d'une sémantique pour le langage C (ou tout autre langage proposant un support les nombres flottants) doit notamment modéliser l'évaluation des expressions manipulant des valeurs numériques. On donne pour cela un modèle mathématique de l'arithmétique flottante composé d'un ensemble support $\mathbb{F}$ représentant les nombres flottants ainsi qu'un ensemble de fonctions $\oplus, \ominus, \otimes$ etc pour interpréter les opérateurs. Deux questions se posent alors. D'une part quelle modélisation choisir parmi les différentes arithmétiques flottantes existantes ? D'autre part, une fois le modèle choisi, comment formaliser ce modèle dans le langage d'un assistant à la démonstration comme Coq ? Plusieurs réponses à ces problèmes existent dans la littérature [6, 7, 5]. Nous décrivons brièvement ici celles déployées dans CompCert.

**Axiomatiser les flottants** Une première solution pour formaliser les nombres flottants et de les axiomatiser : on postule leur existence ainsi que celle des opérations arithmétiques utiles. On peut également axiomatiser quelques propriétés nécessaires pour prouver la correction du compilateur. Cette approche a été initialement utilisée dans les premières versions du compilateur et pose deux principaux problèmes. Tout d'abord, elle nécessite de s'entendre sur les propriétés que l'on peut raisonnablement admettre. Ces propriétés peuvent varier d'une arithmétique à l'autre. Par ailleurs, en choisissant d'axiomatiser les nombres flottants, on s'interdit la possibilité d'effectuer des calculs lors de la compilation pour le besoin de certaines optimisations par exemple. Une solution pour pouvoir tout de même calculer lors de la compilation est d'utiliser les flottants du processeur de la machine qui exécute le compilateur. Toutefois, cette démarche fait l'hypothèse que le processeur employé traite les flottants de manière fidèle à l'axiomatisation choisie. Cette hypothèse n'est pas toujours réaliste et l'article [6] relève déjà cette limitation.
**Imposer le standard IEEE-754** Une autre méthode pour formaliser le comportement des nombres flottants est d'imposer l'usage du standard IEEE-754. Ce choix est compatible avec la norme ISO C et permet de fixer une implémentation logicielle et formellement prouvée du standard IEEE-754. Cette approche est celle actuellement mise en œuvre dans le compilateur CompCert [5]. Les flottants sont représentés grâce à la bibliothèque Flocq [6] qui propose une formalisation du standard IEEE-754 en Coq ainsi qu'une implémentation prouvée des différentes opérations flottantes. Si cette solution résout le problème du calcul, elle ne permet cependant pas de décrire la sémantique des cibles de compilation qui ne supportent pas le standard IEEE-754.

## 3 Le défis de l'extension de CompCert à des cibles non conformes IEEE-754

L'approche par axiomatisation ainsi que celle consistant à fixer l'emploi du standard IEEE-754 limitent les possibilités. La première offre une certaine souplesse mais rend impossible le calcul. La deuxième permet de faire des calculs mais restreint la compilation à des cibles compatibles avec le standard. Nous explorons une troisième approche dans laquelle plusieurs standards sont modélisés. Le modèle de calcul flottant utilisé par CompCert est alors déterminé au moment du choix de la cible de compilation. Cette approche révèle de nombreux défis d'ingénierie logicielle que nous présentons ici.

**Contrôler les conséquences sur la chaîne de compilation** L'architecture du compilateur CompCert comprend une partie commune à toutes les cibles de compilation (analyse syntaxique, typage, optimisations de haut niveau, etc) ainsi que des parties spécifiques à chaque cible de compilation (jeux d'instructions, génération de code, optimisations de bas niveau, etc). Ces deux parties dépendent d'une seule et même modélisation des nombres flottants qui est utilisée aussi bien pour décrire la sémantique du langage C que celle de toutes les cibles de compilation. En rendant interchangeable le modèle de calcul flottant, on risque donc d'invalider toute la chaîne de compilation et sa preuve de correction. En particulier, il faut identifier quels sont les théorèmes d'arithmétique flottante qui peuvent être utilisés dans la partie commune du code si le modèle de calcul flottant est fixé par la cible de compilation. Un travail d'isolation des propriétés communes et spécifiques des différents modèles de calculs numériques est donc nécessaire. En assurant que seule des propriétés universelles sont utilisées dans la partie commune du compilateur, on garanti la possibilité de changer le modèle de calcul sans invalider les preuves déjà effectuées.

**Valider les spécifications** Pour chaque architecture présentant une unité de calcul flottante non conforme, il est nécessaire de modéliser son arithmétique associée en Coq. En multipliant le nombre de modèles différents, nous prenons davantage de risque d'introduire des erreurs dans leurs formalisations. De plus, les documents formatifs préfèrent souvent la prose aux équations et l'écart de formalisme entre le langage naturel et une définition Coq rend difficile la relecture et la validation *a posteriori* des spécifications. Pour illustrer cette difficulté, nous prenons l'exemple de l'addition flottante et sa spécification dans le standard IEEE-754 (voir figure 3).

**Factoriser pour ne pas re-coder et re-prouver** La tâche de formalisation d'un modèle de calcul flottant dans un assistant à la démonstration peut se décomposer en trois temps. Un première étape est de modéliser les nombres flottants en choisissant une structure de données adaptée. On peut dans un second temps implémenter les opérations arithmétiques sous forme de
> Each of the computational operations that return a numeric result specified
> by this standard shall be performed as if it first produced an intermediate result
> correct to infinite precision and with unbounded range, and then rounded that
> intermediate result, if necessary, to fit in the destination's format (see 4 and 7).
> Clause 6 augments the following specifications to cover $±0, ±∞$, and NaN.

<caption>FIGURE 3 – Spécification des opérations flottantes dans le standard IEEE</caption>

fonctions Coq opérant sur la représentation préalablement choisie. Enfin, on développe la preuve formelle des propriétés arithmétiques vérifiées par les opérateurs. Ces propriétés seront utilisées pour justifier la correction du compilateur. Cette suite d'étapes est très consommatrice de temps, en particulier le développement des preuves. Nous constatons toutefois que les différents modèles de calcul flottants étudiés partage un socle commun avec le standard IEEE-754, en particulier en matière de choix de représentation des nombres flottants et de vocabulaire employé dans les documents normatifs. Il est donc possible (voire nécessaire) de factoriser les étapes de modélisation, par exemple en utilisant les structures de données et les définitions fournies par la bibliothèque Flocq. En revanche, des différences notables subsistent dans le comportement des opérations et donc des propriétés arithmétiques. Les preuves doivent donc être traitées au cas par cas. Notons toutefois qu'utiliser le même vocabulaire (le même catalogue de définitions Coq) pour exprimer tous les modèles de calcul rend possible le partage de lemmes intermédiaires entre les différentes preuves.

# 4 Les solutions explorées

Au regard des points mentionnés dans la section précédente, nous proposons différentes approches pour intégrer dans CompCert de nouveaux types de flottants.

## 4.1 Des flottants paramétrables ?

**Fonctoriser le module d'arithmétique flottante** Une première solution explorée pour modéliser de nouveaux nombres flottants est de rendre paramétrable l'implémentation actuelle reposant sur la bibliothèque Flocq. Cette solution permet par exemple de rendre modifiable le mode d'arrondi utilisé (fixé au plus proche pair dans CompCert). La bibliothèque Flocq étant générique sur les modes d'arrondi, les changements impliqués en matière d'implémentation sont presque immédiats : il suffit d'étendre le module Floats modélisant l'arithmétique flottante en un foncteur Floats(M : MODE) dépendant d'un mode d'arrondi fixé par la cible de compilation. Notons toutefois qu'en rendant générique le mode d'arrondi utilisé par les opérations, il faut également rendre générique les théorèmes d'arithmétiques associés. Nous avons observé que les théorèmes utilisés dans CompCert sont indépendants du mode d'arrondi utilisé. La plupart des preuves peuvent donc conservées. Certaines preuves doivent être adaptées mais les énoncés restent valides.

**Limitations** Cette approche permet de modéliser des subtiles nuances compatibles avec le standard IEEE-754 comme les différents modes d'arrondi. Toutefois, pour la modélisation de
flottants non conformes, cette approche n'est pas suffisante. En effet, si les écarts avec le stan-
dard sont trop importants, il est difficile d'identifier les paramètres à faire varier et de controler
leur impact sur la validité des théorèmes.

## 4.2 Spécification formelle de flottants non conformes

**Du pseudo-code pour réduire les écarts de formalisme** Comme mentionné dans la section 3, un des principaux obstacles à la traduction de documents normatifs en code Coq est l'écart entre niveaux de vocabulaire utilisés. Il est donc utile de se doter d'outils facilitant la traduction des documentations à dispositions (standards, manuels des processeurs, etc) en code Coq. On peut par exemple passer par l'intermédiaire de pseudo-code. Cela permet d'éviter les transitions abruptes du langage naturel au langage formel tout en faisant apparaître expliquement les objets mathématiques nécessaires à l'expression des spécifications en Coq. Nous prenons pour example la spécification de l'addition flottante du processeur PowerPC e200z4 (voir figure 4).

The low element of RA is added to the low element of RB and the result is stored in the low element of RD. If RA is NaN or infinity, the result is either pmax (sa = 0), or nmax (sa = 1). If RB is NaN or infinity, the result is either pmax (sb = 0), or nmax (sb = 1). If an overflow occurs, pmax or nmax (as appropriate) is stored in RD. If an underflow occurs, +0 (for rounding modes RN, RZ, RP) or -0 (for rounding mode RM) is stored in RD.

```c
efsadd(a, b) {
    if (isnan(a) || isinf(a)) {
        max-val(a)
    } else if (isnan(b) || isinf(b)) {
        max-val(b)
    } else if (overflow(a + b)) {
        max-val(a + b)
    } else if (underflow-after-rounding(a + b)) {
        if (rounding = nearest || rounding = zero || rounding = +INF)
            { +0.0 } else { -0.0 }
    } else {
        round(a + b)
    }
}
```

<caption>FIGURE 4 – Spécification de l'addition flottante dans le manuel du processeur e200z4 et sa traduction sous forme de pseudo-code</caption>

**Conversion du pseudo-code en Coq** Une fois le pseudo-code écrit et les définitions mathématiques utiles identifiées, nous pouvons le traduire manuellement en Coq. Cette étape consiste essentiellement à choisir les types appropriés pour représenter les différents objets. Nous identifions également une collection de définitions primitives systématiquement utilisées dans les
documents normatifs pour l'arithmétique flottante (par exemple *round*, *overflow*, *underflow* apparaissant en rouge dans la figure 4). Nous implémentons ces primitives en Coq à l'aide de Flocq ce qui permet de ré-exploiter les types et les théorèmes déjà établies dans la bibliothèque.

**Validation** Passer par l'intermédiaire du pseudo-code permet de répartir l'effort nécessaire à la validation des spécifications. Une première relecture du pseudo-code est faite pour s'assurer de son adéquation par rapport au standard de référence. Notons que cette relecture ne nécessite aucune connaissance du langage Coq. Une deuxième relecture permet ensuite de vérifier la correction du code Coq vis à vis du pseudo-code. L'usage de pseudo-code comme interface rend la relecture plus efficace et plus fiable en séparant explicitement deux champs de compétences : la connaissance du standard considéré et celle du langage Coq.

**Limitations** La traduction de standards en Coq en passant par l'intermédiaire de pseudo-code facilite la tâche de validation des spécifications. Toutefois, la traduction doit être faite manuellement et les specifications Coq obtenues ne sont pas nécessairement exécutables. En particulier, elles utilisent des opérations sur les nombres réels qui ne peuvent pas être calculées en Coq. En revanche, ces spécifications formelles peuvent servir de référence pour l'implémentation et la vérification d'opérations exécutables.

# 5 Remerciements

Merci à François Bobot pour m'avoir fait découvrir (et sombrer dans) l'univers des nombres flottants. Merci également à Bernhard Schommer et Christoph Mallon pour les discussions interminables que nous avons eu sur l'interprétation du standard IEEE et de la norme ISO C. Enfin, merci au commité des JFLA pour les commentaires très constructifs qui ont guidés la rédaction de la version finale de cet article.

# 6 Conclusion

Le compilateur CompCert propose un support pour les flottants IEEE-754 et restreint la compilation à des cibles conformes au standard. Nous avons étudié la possibilité d'intégrer dans CompCert un support pour d'autres arithmétiques flottantes et concluons cette étude par deux constats. D'une part, une telle extension nécessite un travail initial d'isolation de certaines composantes logicielles. Cela permettrait de rendre interchangeable le modèle de calcul flottant tout en limitant les conséquences sur la chaîne de compilation et en particulier sa preuve de correction. D'autre part, l'écart de formalisme entre les documents normatifs qui standardisent l'arithmétique flottante et le langage logique de Coq rend difficile la formalisation de nouveaux modèles de calculs. Passer par l'intermédiaire du pseudo-code peut faciliter cette tâche. Des questions restent cependant ouvertes, notamment concernant la possibilité d'exécuter les spécifications Coq. Développer un langage de spécification formelle dédié à l'arithmétique flottante et pouvant être compilé vers des spécifications Coq executables pourrait être une piste de recherche intéressante. Des travaux similaires ont déjà été menés pour la spécification d'architectures matérielles [12, 3].
Références

[1] The coq proof assistant. https://coq.inria.fr.

[2] Iso/iec/ieee international standard - floating-point arithmetic. ISO/IEC 60559:2020(E) IEEE Std 754-2019, pages 1–86, 2020.

[3] Alasdair Armstrong, Thomas Bauereiß, Brian Campbell, Shaked Flur, Kathryn E. Gray, Prashanth Mundkur, Robert M. Norton, Christopher Pulte, Alastair David Reid, Peter Sewell, Ian David Bede Stark, and Mark Wassell. Detailed models of instruction set architectures: From pseudocode to formal semantics. 2018.

[4] Sylvie Boldo. L'arithmétique des ordinateurs et sa formalisation. https://www.college-de-france.fr/agenda/seminaire/semantiques-mecanisees-quand-la-machine-raisonne-sur-ses-langages/arithmetique-des-ordinateurs-et-sa-formalisation, 2019.

[5] Sylvie Boldo, Jacques-Henri Jourdan, Xavier Leroy, and Guillaume Melquiond. Verified Compilation of Floating-Point Computations. Journal of Automated Reasoning, 54(2):135–163, February 2015.

[6] Sylvie Boldo and Guillaume Melquiond. Flocq : A Unified Library for Proving Floating-point Algorithms in Coq. In Elisardo Antelo, David Hough, and Paolo Ienne, editors, Proceedings of the 20th IEEE Symposium on Computer Arithmetic, pages 243–252, Tübingen, Germany, July 2011.

[7] John Harrison. Floating-point verification using theorem proving. In Marco Bernardo and Alessandro Cimatti, editors, Formal Methods for Hardware Verification, pages 211–242, Berlin, Heidelberg, 2006. Springer Berlin Heidelberg.

[8] ISO. ISO/IEC 9899:2011 Information technology — Programming languages — C. International Organization for Standardization, 2011.

[9] Daniel Kästner, Xavier Leroy, Sandrine Blazy, Bernhard Schommer, Michael Schmidt, and Christian Ferdinand. Closing the gap – the formally verified optimizing compiler CompCert. In SSS’17: Developments in System Safety Engineering: Proceedings of the Twenty-fifth Safety-critical Systems Symposium, pages 163–180. CreateSpace, 2017.

[10] Xavier Leroy. Formal verification of a realistic compiler. Communications of the ACM, 52(7):107–115, July 2009.

[11] Xavier Leroy, Sandrine Blazy, Daniel Kästner, Bernhard Schommer, Markus Pister, and Christian Ferdinand. CompCert – a formally verified optimizing compiler. In ERTS 2016: Embedded Real Time Software and Systems. SEE, 2016.

[12] Mark Wassell. Minisail - a kernel language for the isa specification language sail. Archive of Formal Proofs, June 2021. https://isa-afp.org/entries/MiniSail.html, Formal proof development.
# L'arithmétique de séparation

Jean-Christophe Filliâtre et Andrei Paskevich

¹ LMF — Université Paris-Saclay, CNRS, ENS Paris-Saclay

² Inria

## Résumé

Nous, praticiens de la preuve de programmes, souhaitons que le processus de la vérification soit le plus automatique possible. Les meilleurs outils pour cela sont à l'heure actuelle les démonstrateurs SMT, qui combinent notamment la logique du premier ordre et l'arithmétique linéaire. Par opposition, le raisonnement inductif n'est pas un point fort des démonstrateurs automatiques. Or, les programmes utilisant des pointeurs le font souvent pour manipuler des structures récursives : listes, arbres, etc.

Dans cet article, nous décrivons une approche qui permet d'amener la preuve de programmes avec pointeurs à la portée des démonstrateurs automatiques. L'idée consiste à projeter une structure récursive sur un domaine numérique, de sorte que les propriétés de possession et de séparation deviennent exprimables en terme de simples inégalités arithmétiques. En plus de simplifier la preuve, cela permet une spécification claire et naturelle. On illustre cette approche avec l'exemple classique du renversement en place d'une liste simplement chaînée.

# 1 Introduction

Dans le domaine de la preuve de programmes, et plus spécifiquement dans le domaine de la vérification déductive, nous sommes aujourd'hui grandement aidés par les démonstrateurs SMT, qui combinent notamment la logique du premier ordre et l'arithmétique linéaire. Ils nous permettent parfois d'obtenir des preuves entièrement automatiques, là où hier encore il fallait laborieusement construire une preuve interactivement et la faire vérifier par un assistant de preuve.

Les démonstrateurs SMT ont cependant des limites. En particulier, le raisonnement inducif n'est pas leur point fort. Or, les programmes utilisant des pointeurs le font souvent pour manipuler des structures qui sont récursives par nature, telles que des listes ou des arbres. Il est alors naturel de recourir à des définitions récursives pour les propriétés que l'on cherche à démontrer. Il y alors une tension évidente entre deux principes, à savoir d'une part le principe qui affirme

> La bonne spécification, c'est celle qui est facile à comprendre.

qui va dans le sens d'une définition récursive, naturelle pour la personne qui va lire et approuver la spécification, et le principe qui affirme d'autre part

> Le bon invariant, c'est celui qui est facile à prouver.

qui va plutôt dans le sens d'une définition non récursive, plus adaptée aux démonstrateurs SMT.

Dans cet article, nous décrivons une approche qui permet dans certains cas de réconcilier ces deux principes, en amenant la preuve de programmes avec pointeurs à la portée des démonstrateurs automatiques. Nous l'illustrons sur l'exemple classique du renversement en place d'une liste simplement chaînée. L'idée clé consiste à se ramener à de simples inégalités dans l'arithmétique linéaire, un domaine de prédilection des démonstrateurs SMT, ce qui justifie le titre de cet article.
L'essentiel de cet article est composé autour de l'exemple du renversement d'une liste, avec sa spécification naturelle (section 2), une tentative échouée de preuve directe (section 3) et la proposition de notre approche arithmétique (section 4), que nous illustrons ensuite rapidement sur un autre cas d'étude (section 5). Nos expériences ont été conduites avec l'outil Why3 [2] et le code complet est donné en annexe. Toutefois, dans le but de donner plus d'universalité à notre propos, les éléments de spécification et de preuve sont donnés dans une syntaxe allégée.

## 2 Un grand classique

On illustre notre propos avec l'exemple classique du renversement en place d'une liste simplement chaînée. La figure 2 contient un code C qui implémente cet algorithme et illustre son fonctionnement sur une liste de cinq éléments. L'algorithme parcourt la liste une fois, avec la variable l, et redirige le pointeur next sur l'élément précédent, stocké dans la variable r.

```c
typedef struct Cell list;
struct Cell { int value; list *next; };

list *list_reversal(list *l) {
    list *r = NULL;
    while (l != NULL) {
        list *tmp = l;
        l = l->next;
        tmp->next = r;
        r = tmp;
    }
    return r;
}
```

<figure><img src="image_97.png" /><figcaption>FIGURE 1 – Renversement en place d'une liste chaînée.</figcaption></figure>

L'intérêt de ce programme pour la vérification est la coexistence, pendant la durée de la boucle, de deux listes simplement chaînées. Le fait que ces deux listes sont spatialement séparées nous permet d'établir la préservation des invariants. Plus précisément, l'affectation du pointeur `tmp->next` dans le code préserve la queue de la liste `l` d'une part et la liste `r` d'autre part.

Une spécification de la fonction `list_reversal` doit exprimer que les cellules de la liste initiale sont chaînées dans l'ordre inverse à l'issue de la fonction et le résultat de la fonction est la tête de cette nouvelle liste. Notons que la spécification ne peut pas se contenter de parler seulement du contenu des cellules, ce qui serait moins précis. En effet, le code pourrait par exemple inverser les valeurs contenues dans les cellules, mais laisser les champs `next` inchangés.

Pour écrire confortablement la spécification de la fonction, on doit représenter dans la longue, en plus des pointeurs manipulés par le programme, la mémoire elle-même (qu'on va appeler `mem`) et le modèle mathématique de la liste, sous la forme d'une séquence d'adresses mémoire (qu'on va appeler `s`). Étant donnés `mem`, `l` et `s`, nous pouvons définir un prédicat de présentation, `list mem l s`, qui exprime que, à l'adresse `l` dans la mémoire `mem`, se trouve une liste simplement chaînée dont les cellules forment la séquence `s`. En particulier, `l` est égal à `NULL` si et seulement si la séquence `s` est vide. Il est naturel de définir ce prédicat récursivement, sur la longueur de la séquence `s`.
```
predicate list mem l s =
    if length s = 0 then l = NULL
else l = s[0] <> NULL && list mem[l].next s[1:]
```

Ici, `mem[l].next` désigne le contenu du champ `next` de la cellule à l'adresse `l` dans `mem` et `s[1:]` désigne la séquence `s` privée de son premier élément.

La spécification de `list_reversal` est alors très simple, en supposant donnée une fonction logique `rev` qui renverse une séquence :

```
list_reversal l (ghost s) : r
    requires list mem l s
    modifies mem
    ensures list mem r (rev s)
```

Ici, la séquence `s` est fournie comme un argument fantôme [3] de la fonction `list_reversal`, c'est-à-dire un argument qui n'est là que pour les besoins de la spécification.

La variable globale `mem` représente l'état de la mémoire : dans la précondition, à l'entrée de la fonction ; dans la postcondition, à la sortie. La spécification ci-dessus est incomplète si on ne dit pas que la mémoire reste inchangée en dehors des adresses qui composent la liste `l`. On peut exprimer cette propriété avec une seconde postcondition

```
ensures pforall p. not (mem p s) -> mem[p] = old mem[p]
```

où `old mem[p]` désigne le contenu de la mémoire à l'adresse `p` à l'entrée de la fonction.

## 3 Droit dans le mur

Dans cette section, nous allons montrer en quoi la spécification ci-dessus, aussi naturelle qu'elle soit, ne se prête pas facilement à une preuve automatique. La première étape de la vérification consiste à exposer les invariants de boucle. Ils se déduisent triviallement de la figure 2, en exprimant que `l` est un suffixe de la liste initiale et `r` un renversement du préfixe correspondant. En se donnant une variable fantôme `i` qui maintient le nombre de cellules déjà renversées, on a donc les deux invariants suivants

```
invariant list mem l s[i:]
invariant list mem r (rev s[:i])
```

où `s[i:]` est le suffixe de `s` à partir de la position `i` incluse et `s[:i]` le préfixe de `s` jusqu'à la position `i` exclue. En particulier, la sortie de boucle, où `i` est égal à la longueur de `s`, nous donne exactement la postcondition attendue. Jusque là, tout est parfaitement naturel et plutôt simple.

Les choses se compliquent lorsque l'on s'attaque à prouver que ces invariants de boucle sont préservés par une itération de la boucle. En effet, considérons l'état du programme à la fin d'une itération. L'invariant sur la nouvelle valeur de `l` se déduit directement de l'invariant sur sa valeur précédente, car on a uniquement suivi le champ `next` et `s[i+1:]` est égal à `s[i:]` [1:]. L'invariant sur la nouvelle valeur de `r` se déduit de l'invariant sur la valeur précédente, car à la tête de `rev s[:i+1]` on trouve `r` et `(rev s[:i+1])[1:]` est égal à `rev s[:i]`.

La difficulté consiste alors à prouver que les deux portions de la liste, à gauche de `r` et à droite de `l`, ont conservé la propriété `list`, puisque la modification de `tmp->next` n'a pas affecté les cellules qui les composent. La définition de `list` étant récursive, cette preuve nécessite une induction. Bien qu'il soit possible d'effectuer une telle induction, par exemple en utilisant un
démonstrateur comme Coq ou un autre moyen de preuve interactive, on préférerait une solution
qui soit entièrement à la portée d'un démonstrateur automatique.

4 Approche arithmétique

La définition récursive du prédicat *list* introduite dans la section 2 nous pousse à représenter tout fragment de liste par un objet mathématique différent (ici une séquence). On a vu dans la section précédente en quoi cette approche est inadaptée à la preuve. Or, nous pouvons choisir une approche différente, “bas niveau”, et naviguer dans une description *globale* à l’aide d’indices.

Reprenons la séquence s des adresses mémoire des cellules de la liste initiale. À toute itération de l’algorithme, un préfixe $[0, i[$ de cette séquence, lu de droite à gauche, correspond à la liste r et le suffixe $[i, n[$ correspond à la liste l, ce que l’on peut représenter ainsi :

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

Pour l'instant, on va supposer de plus que les éléments de s sont non nuls et deux à deux distincts; nous montrerons plus loin que ces deux propriétés peuvent être déduites du prédicat de représentation *list*. C'est ce que décrit le prédicat suivant :

```
predicate valid
s =
    (forall i. 0 <= i < length s -> s[i] <> null) &&
    (forall i j. 0 <= i,j < length s -> i <> j -> s[i] <> s[j])
```

On peut maintenant définir deux nouveaux prédicats de représentation pour une liste correspondant à *un préfixe* ou *un suffixe* de s :

```
predicate prefix mem s r i =
    0 <= i <= length s &&
    if i = 0 then r = null else
        r = s[i-1] && mem[s[0]].next = null &&
       forall k. 0 < k < i -> mem[s[k]].next = s[k-1]
```

```
predicate suffix mem s l i =
    0 <= i <= length s &&
    if i = length s then l = null else
        l = s[i] && mem[s[length s - 1]].next = null &&
       forall k. i < k < length s -> mem[s[k-1]].next = s[k]
```

Ces prédicats remplacent la récursivité par un quantificateur universel sur les indices à l'intérieur de s. C'est pourquoi on parle ici d'approche *arithmétique*.

Avec ces définitions, la fonction *list_reversal* a maintenant une spécification un peu différente de celle de la section 2 :

```
list_reversal (ghost s) l : r
```
```
requires valid cells s
requires suffix mem s 1 0
modifies mem
ensures prefix mem s r (length s)
ensuresforall p. not (mem p s) -> mem[p] = old mem[p]
```

Mais surtout, les *invariants* de la boucle s'expriment eux aussi en termes des prédicats `suffix` et `prefix`,

```
invariant suffix mem s 1 i
invariant prefix mem s r i
```

et c'est là la clé d'une démonstration aisée. De fait, la preuve ne nécessite plus de raisonnement par induction et est maintenant entièrement à la portée des démonstrateurs automatiques.

**Retomber sur ses pattes.** Pour être complets, il nous reste cependant à faire le lien entre la spécification naturelle, introduite dans la section 2, et la preuve ci-dessus. Pour cela, il convient d'établir, à partir de la définition du prédicat récursif `list`, les deux préconditions de la fonction `list_reversal`, c'est-à-dire, `validCells` et `suffix`.

On peut le faire agréablement à l'aide d'une fonction fantôme pure, dite *fonction-lemme*, dont le seul objectif est de construire cette preuve.

```
lemma cells_of_list l s
    requires list mem l s
    ensures validCells s
    ensures suffix mem s 1 0
    variant length s
    = if s <> empty then cells_of_list mem[l].next s[1:]
```

Cette fonction récursive suit la structure du prédicat `list`. De facto, le code de cette fonction représente une preuve par induction, écrite par l'utilisateur. Par le mécanisme de vérification de Why3, cette fonction, et donc le lemme, peuvent être vérifiés de manière purement automatique, quand bien même l'énoncé du lemme est en soi hors de portée d'un démonstrateur automatique. De la même façon, on peut écrire et prouver une fonction-lemme `list_ofCells` qui conclut `list mem r (rev s)` à partir des hypothèses `validCells` et `prefix`.

En composant ces deux lemmes et la fonction `list_reversal`, on obtient une fonction vérifiée, avec la spécification naturelle introduite au début de cet article.

## 5 Un autre exemple

Nous décrivons ici un autre exemple de la même approche, un peu plus complexe. Il s'agit d'un problème proposé en 2021 dans le cadre de la compétition de preuve de programmes VerifyThis [1]. Un algorithme pour convertir une liste doublement chaînée en arbre binaire était donné, et il fallait en proposer une implémentation vérifiée. Plus précisément, on part d'une liste doublement chaînée contenant une séquence de valeurs $v_0, v_1, \dots$ :

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

Chaque cellule contient un pointeur `prev` vers la cellule précédente (ou la valeur `null` pour la première cellule) et un pointeur `next` vers la cellule suivante (ou la valeur `null` pour la dernière cellule). L'algorithme réorganise alors les pointeurs `prev` et `next` pour former un arbre binaire,
le pointeur *prev* pointant maintenant vers le sous-arbre gauche et le pointeur *next* vers le sous-arbre droit.

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

Pour cela, l'algorithmme commence par calculer la longueur *n* de la liste, puis se repose sur une fonction récursive qui prend en paramètres un pointeur vers le début de la liste et un nombre d'éléments à considérer, et qui renvoie la racine de l'arbre construit et le pointeur vers le premier élément non consommé. L'ordre des éléments est conservé, au sens où un parcours infixe de l'arbre énumère les valeurs *v*₀, *v*₁, ... dans l'ordre.

Parmi les propriétés de l'algorithmme à vérifier, il y avait le caractère équilibré de l'arbre obtenu au final, ou encore le fait que, si les valeurs *v*ᵢ sont triées par ordre croissant, alors l'arbre obtenu est un arbre binaire de recherche. Pour cette vérification, nous pouvons avantageusement utiliser l'approche arithmétique. Comme pour le renversement de liste, on introduit une séquence fantôme *s* de toutes les cellules mémoires :

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

Sur la base de cette séquence, il est maintenant possible de définir un prédicat *dll s p lo hi*
qui exprime que le pointeur *p* est la première cellule d'une liste doublement chaînée formée
par les cellules de *s* situées entre les indices *lo* inclus et *hi* exclu, et de même un prédic-
cat *tree s p lo hi* qui exprime que le pointeur *p* est la racine d'un arbre binaire dont les
nœuds, dans l'ordre infixe, sont les cellules de *s* entre *lo* et *hi*. Une preuve Why3 réalisant
cette idée est disponible en ligne [4]. Elle est majoritairement automatique.

6 Conclusion

Sur la base de deux exemples, nous avons montré comment, dans le contexte de la vérification déductive, une spécification récursive peut être avantageusement remplacée par une spécification ne faisant intervenir que des inégalités arithmétiques, et conduire alors à une preuve bien plus automatique. Nous anticipons que cette technique s'applique au-delà de ces deux exemples, sur toute structure récursive où un ordre de parcours définit une sérialisation de ses éléments. Pour poursuivre cette étude, il conviendrait d'explorer aussi des programmes qui allouent dynamiquement de la mémoire.

Bien évidemment, l'approche que nous avons présentée ici n'a aucune prétention à être aussi
expressive et puissante que la logique de séparation [7]. Néanmoins, elle a le mérite de ne pas
nécessiter une logique spécifique et des outils dédiés. Puisque nous travaillons dans un modèle
mémoire plat, nous pouvons par ailleurs nous abstraire de toute problématique de ressource,
de possession, d'alias, etc. Et puisque notre représentation logique est construite sur la base d'adresses explicites, elle nous donne immédiatement accès à l'empreinte mémoire (footprint) de la structure. On se rapproche là des *dynamic frames* [5], une autre technique de preuve de programmes avec pointeurs utilisée par exemple dans Dafny [6]. Mais contrairement à cette approche, nos empreintes sont dotées d'une structure supplémentaire, à savoir leur caractère séquentiel, ce qui nous permet justement de faire de l'arithmétique de séparation.

**Remerciements.** Nous remercions nos collègues Claude Marché et Jacques-Henri Jourdan pour toutes les discussions relatives à la vérification du renversement d'une liste.

Références

[1] The VerifyThis competition, Since 2011. https://www.pm.inf.ethz.ch/research/verifythis.html.

[2] François Bobot, Jean-Christophe Filliâtre, Claude Marché, Guillaume Melquiond, and Andrei Paskevich. The Why3 platform. http://why3.lri.fr/.

[3] Jean-Christophe Filliâtre, Léon Gondelman, and Andrei Paskevich. The spirit of ghost code. *Formal Methods in System Design*, 48(3):152–174, 2016.

[4] Jean-Christophe Filliâtre and Andrei Paskevich. Solution to verifythis 2021 challenge 2, 2021. https://toccata.gitlabpages.inria.fr/toccata/gallery/verifythis_2021_dll_to_bst.en.html.

[5] I. T. Kassios. The dynamic frames theory. *Formal Aspects of Computing*, 23(3):267–288, May 2011.

[6] K. Rustan M. Leino. Dafny : An automatic program verifier for functional correctness. In *LPAR-16*, volume 6355 of *Lecture Notes in Computer Science*, pages 348–370. Springer, 2010.

[7] J. C. Reynolds. Separation logic : a logic for shared mutable data structures. In *17th Annual IEEE Symposium on Logic in Computer Science*. IEEE Comp. Soc. Press, 2002.

A Le source Why3 complet

Le code ci-dessous a été vérifié avec la version 1.5.1 de Why3 (https://why3.lri.fr/) et les deux démonstrateurs SMT Alt-Ergo 2.4.0 (https://alt-ergo.ocamlpro.com/) et CVC5 1.0.0 (https://github.com/cvc5/cvc5/). La session Why3 peut être téléchargée à l'adresse https://www.lri.fr/~filliatr/jfla-2023/list_reversal.zip et ouverte avec les commandes suivantes :

$ unzip -x list_reversal.zip

$ cd jfla-2023

$ why3 ide list_reversal

Le code Why3 commence par modéliser les pointeurs (type *loc*) et la mémoire (variable globale *mem*), car les structures récursives mutables ne sont pas acceptées nativement par Why3. La séquence *s* est représentée par une simple fonction de type *int -> loc*.

use int.Int

use map.Map

<footnote>(* Le modèle mémoire *)</footnote>
```pascal
type loc

val (=) (l1 12: loc) : bool ensures { result <-> l1 = 12 }

val constant null : loc

type mem = { mutable next: loc -> loc }

val mem: mem

let cdr (p: loc) : loc
    requires { p <> null }
    ensures { result = mem.next p }
    = mem.next p

let set_cdr (p: loc) (v: loc) : unit
    requires { p <> null }
    ensures { mem.next = (old mem.next)[p <- v] }
    = let m = mem.next in
        mem.next <- fun x -> if x = p then v else m x
```

(* Les définitions de prédicats, avec l'approche arithmétique *)

```
predicate validCells (s: int -> loc) (n: int) =
  (forall i. 0 <= i < n -> s i <> null) &&
  (forall i j. 0 <= i < n -> 0 <= j < n -> i <> j -> s i <> s j)

predicate listLR (m: mem) (s: int -> loc) (l: loc) (lo hi: int) =
  0 <= lo <= hi &&
  if lo = hi then l = null else
    l = s lo && m.next (s (hi-1)) = null &&
   forall k. lo <= k < hi-1 -> m.next (s k) = s (k+1)
```

```
predicate listRL (m: mem) (s: int -> loc) (l: loc) (lo hi: int) =
  0 <= lo <= hi &&
  if lo = hi then l = null else
    m.next (s lo) = null && l = s (hi-1) &&
   forall k. lo < k < hi -> m.next (s k) = s (k-1)
```

```
predicate frame (m1 m2: mem) (s: int -> loc) (n: int) =
 forall p. (forall i. 0 <= i < n -> p <> s i) ->
    m1.next p = m2.next p
```

(* Le code *)

```pascal
let list_reversal (ghost s: int -> loc) (ghost n: int) (l: loc) : (r: loc)
    requires { validCells s n }
    requires { listLR mem s 1 0 n }
```
ensures { listRL mem s r 0 n }
ensures { frame mem (old mem) s n }
= let ref l = l in
let ref r = null in
let ghost ref i = 0 in
while l <> null do
  invariant { if n = 0 then l = r = null else
                i = 0      && r = null      && l = s 0
              || i = n    && r = s (n-1)    && l = null
              || 0 < i < n && r = s (i-1)    && l = s i }
  invariant { listRL mem s r 0 i }
  invariant { listLR mem s l i n }
  invariant { frame mem (old mem) s n }
  variant { n - i }
  let tmp = l in
  l <- cdr l;
  set_cdr tmp r;
  r <- tmp;
  i <- i + 1
done;
return r

(* Avec la spécification récursive cette fois *)

let rec ghost predicate is_list (m: mem) (l: loc) (s: int -> loc) (n: int)
requires { n >= 0 }
variant { n }
= if n = 0 then l = null else
  l = s 0 <> null && is_list m (m.next l) (fun i -> s (i+1)) (n - 1)

let rec lemma cells_of_list (l: loc) (s: int -> loc) (n: int)
requires { n >= 0 }
requires { is_list mem l s n }
variant { n }
ensures { valid cells s n }
ensures { listLR mem s l 0 n }
= if n <> 0 then cells_of_list (cdr l) (fun i -> s (i+1)) (n - 1)

let rec lemma list_of cells (r: loc) (s: int -> loc) (n: int)
requires { n >= 0 }
requires { valid cells s n }
requires { listRL mem s r 0 n }
variant { n }
ensures { is_list mem r (fun i -> s (n-1-i)) n }
= if n <> 0 then list_of cells (cdr r) s (n - 1)

let list_reversal_final (ghost s) (ghost n: int) (l: loc) : (r: loc)
requires { n >= 0 }
requires { is_list mem l s n }
ensures { is_list mem r (fun i -> s (n-1-i)) n }
ensures { frame mem (old mem) s n }
= cells_of_list l s n;
let r = list_reversal s n l in
list_of cells r s n;
r
Démonstrations
# GOOSE: an OCaml environment for quantum computing

Denis Carnier<fnref n="1" />, Arthur Correnson²,
Christopher McNally³, and Youssef Moawad⁴

¹ imec-DistriNet, KU Leuven, Belgium
denis.carnier@kuleuven.be

² CISPA Helmholtz Center for Information Security, Germany
arthur.correnson@cispa.de

³ Massachusetts Institute of Technology, United States
mcnallyc@mit.edu

⁴ University of Glasgow, United Kingdom
y.moawad.1@research.gla.ac.uk

## Abstract

In this presentation, we showcase GOOSE: an OCaml library to model, simulate and compile low-level quantum programs. GOOSE is designed as a playground with an emphasis on extensibility and accessibility to non-experts. The library is compatible with the OPEN-QASM standard, and targets a variety of backends with a minimalistic, circuit-based IR.

## 1 Introduction

*Quantum computing* [8] is an emerging model of computation that exploits non-classical effects like *superposition* and *entanglement* to achieve algorithmic speedups. A radical break from classical computing, the model presents new challenges for programming languages research.

In particular, researchers are interested in more expressive ways to design and develop quantum algorithms, and the ability to leverage existing tooling for classical programming languages in the construction of quantum programming languages (QPLs) [1, 4, 9, 3, 6, 2].

OCaml is a mature ecosystem, widely used for programming languages research. However, to the best of our knowledge, it has a scarcity of tools for quantum programming. We therefore present GOOSE<fnref n="1" />: an OCaml library to model, simulate and compile quantum programs. The library is designed to act as a playground to experiment with quantum programming in the OCaml ecosystem.

## 2 Description and architecture

<figure><img src="image_102.png" /><figcaption>Figure 1: A high-level overview of GOOSE’s modular pipeline.</figcaption></figure>

<footnote n="1">¹GOOSE is available at https://qgoose.github.io.</footnote>
Figure 1 gives a high-level overview of GOOSE. The library is built around an intermediate representation (IR) for quantum circuits. This IR can be used as an entry point to, for instance, build simulators, compilers, and static analyzers for quantum programs. GOOSE includes a full state-based simulator to interpret the IR, designed as a functor parametrized by a linear algebra module. This design choice allows one to implement many tools simply by specializing the simulator. We demonstrate it by deriving both a symbolic simulator and an emitter to C. Further tools could be implemented, for example optimizers and compilers for other languages. To ensure compatibility with other existing tools related to quantum computing, we provide a frontend for OPENQASM 2.0, a standard low-level quantum circuit representation [5].

## 3 An example

In Figure 2, we provide an example of a GHZ [8] circuit entangling three qubits. Listing 3a shows the corresponding GOOSE IR representation. This is implemented with a list comprehension that specifies the CX gates, with an initial H gate. In Listing 3b, we display the C code that was generated based on the results of the symbolic simulator. `cadd`, `cmul`, and `csub` are C functions for complex number arithmetic. Finally, `s` and `o` are arrays for storing the input and output state, respectively.

```c
let entanglement n = {
    qbits = n;
    gates = List.cons ({
        target = A 0;
        kind = H;
        controls = []
    }) (List.init (n-1)
    (fun i -> {
        target = A (i + 1);
        kind = X;
        controls = [A 0]
    }))
}
```

(a) Explicit construction of a GHZ circuit in the GOOSE IR.

<figure><img src="image_103.png" /><figcaption>Figure 2: 3-qubit GHZ circuit.</figcaption></figure>

```c
cfloat *s = (cfloat*)malloc(N*sizeof(cfloat));
cfloat *o = (cfloat*)malloc(N*sizeof(cfloat));

for (int i = 0; i < N; i++)
    s[i] = (cfloat) {0.0, 0.0};

o[0] = cmul(SQRT1_2, cadd(s[0], s[1]));
o[1] = cmul(SQRT1_2, csub(s[6], s[7]));
o[2] = cmul(SQRT1_2, cadd(s[2], s[3]));
o[3] = cmul(SQRT1_2, csub(s[4], s[5]));
o[4] = cmul(SQRT1_2, cadd(s[4], s[5]));
o[5] = cmul(SQRT1_2, csub(s[2], s[3]));
o[6] = cmul(SQRT1_2, cadd(s[6], s[7]));
o[7] = cmul(SQRT1_2, csub(s[0], s[1]));
```

(b) Sample of generated C code to simulate this circuit for $n=3$. Each line computes one amplitude in the output state: $\frac{1}{\sqrt{2}}(1, 0, 0, 0, 0, 0, 0, 1)^T$

## 4 Conclusion and future work

We presented GOOSE: an open source library for quantum computing in the OCaml ecosystem. Currently, the library's front-end supports a subset of the OPENQASM 2.0 circuit representation, a standard for interoperability between quantum computing tools. Additionally, GOOSE implements a generic simulator for quantum circuits. We specialized this simulator to both a symbolic simulator and a C emitter.

In the future, we want to connect GOOSE to other existing projects, for instance TWIST [10], a QPL whose existing OCaml-based interpreter calls out to C++ quantum simulation libraries, or VOQC [7], a formally verified compiler for quantum circuits that can be extracted to OCaml.
# Acknowledgements

We would like to thank the anonymous reviewers who have helped to improve this paper through their criticism and suggestions. Moreover, we especially thank Paulette Koronkevich for inspiring the name GOOSE.

C.M. was supported by the CQE-LPS Doc Bedard Fellowship. This research is co-funded by a PhD studentship from the College of Science and Engineering at the University of Glasgow, by the Research Fund KU Leuven, by the Flemish Research Programme Cybersecurity and by the European Union (ERC, UniversalContracts, 101040088). Views and opinions expressed are however those of the author(s) only and do not necessarily reflect those of the European Union or the European Research Council. Neither the European Union nor the granting authority can be held responsible for them.

# References

[1] Qiskit: An open-source framework for quantum computing.

[2] Thorsten Altenkirch and Jonathan Grattage. A functional quantum programming language. arXiv:quant-ph/0409065, April 2005.

[3] Benjamin Bichsel, Maximilian Baader, Timon Gehr, and Martin Vechev. Silq: A high-level quantum language with safe uncomputation and intuitive semantics. In *Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation*, PLDI '20, pages 286–300, New York, NY, USA, June 2020. Association for Computing Machinery.

[4] Cirq Developers. Cirq, July 2018.

[5] Andrew W. Cross, Lev S. Bishop, John A. Smolin, and Jay M. Gambetta. Open Quantum Assembly Language. arXiv:1707.03429 [quant-ph], July 2017.

[6] Alexander S. Green, Peter LeFanu Lumsdaine, Neil J. Ross, Peter Selinger, and Benoît Valiron. Quipper: A Scalable Quantum Programming Language. In *Proceedings of the 34th ACM SIGPLAN Conference on Programming Language Design and Implementation*, PLDI '13, pages 333–342, New York, NY, USA, June 2013. Association for Computing Machinery.

[7] Kesha Hietala, Robert Rand, Shih-Han Hung, Xiaodi Wu, and Michael Hicks. A verified optimizer for Quantum circuits. *Proceedings of the ACM on Programming Languages*, 5(POPL):37, January 2021.

[8] M.A. Nielsen and I.L. Chuang. *Quantum Computation and Quantum Information: 10th Anniversary Edition*. Cambridge University Press, 2010.

[9] Robert S. Smith, Michael J. Curtis, and William J. Zeng. A practical quantum instruction set architecture, 2016.

[10] Charles Yuan, Christopher McNally, and Michael Carbin. Twist: Sound reasoning for purity and entanglement in Quantum programs. *Proceedings of the ACM on Programming Languages*, 6(POPL):30:1–30:32, January 2022.
# Décision de relations inductives pour SMTCoq*

## Démonstration d'un prototype

### Louise Dubois de Prisque¹,²

¹ Université Paris-Saclay, CNRS, ÉNS Paris-Saclay, Laboratoire de Méthodes Formelles

² Inria

## Résumé

Les utilisateurs de l'assistant de preuve Coq écrivent le plus souvent les spécifications des objets sur lesquels ils prouvent des énoncés sous la forme de relations inductives. Cependant, la plupart des prouveurs automatiques externes ne savent pas les interpréter et cela restreint donc leur usage au sein de Coq. Nous présentons un plugin Coq qui permet, étant donné une relation inductive décidable dans Prop, de définir automatiquement son pendant booléen. Une preuve de correction est également générée dans certains cas. Notre outil est intégré à la tactique snipe, une extension de SMTCoq qui préprocesse des énoncés Coq puis appelle un prouveur SMT pour les prouver automatiquement. Lors de notre démonstration, nous montrerons au travers d'exemples qu'il permet à snipe d'automatiser des preuves au sujet de spécifications inductives décidables.

## 1 Un problème de décision

La manière naturelle d'écrire des spécifications (même décidables) dans l'assistant de preuve Coq est d'utiliser des relations inductives et non d'écrire des fonctions booléennes. En effet, cela permet à l'utilisateur de ne décrire que les cas où la relation est vraie, d'obtenir un code plus lisible où chaque constructeur de la relation correspond à une règle d'inférence, d'user des principes d'inversion associés au sein d'une preuve, et de ne pas s'occuper des questions de décidabilité. Considérons le prédicat mem, qui est vrai lorsque le premier argument appartient à la liste donnée en second argument. Sous la forme d'une relation inductive, il s'écrit :

Inductive mem : Z → list Z → Prop ::=
| MemMatch :forall (xs : list Z) (z : Z), mem z (z :: xs)
| MemRec :forall (xs : list Z) (z z' : Z), mem z xs → mem z (z' :: xs).

Le problème de cette forme est qu'elle n'est pas utilisable par un outil ou une tactique d'automatisation qui ne connaît pas les relations inductives. En particulier, l'outil SMTCoq [3], qui appelle des prouveurs SMT au sein de Coq, et utilise donc une logique classique, ne permet de raisonner que sur des fonctions booléennes. Ainsi, un but tel que celui-ci :

Lemma mem_imp_notNil s l : mem z l → l <> [].

ne peut pas être prouvé par SMTCoq. En effet, la formule ne pourra pas être traduite dans les booléens sans transformation préalable de mem en fonction booléenne équivalente mem_dec. Mais, en supposant cette fonction donnée, SMTCoq, via la tactique d'automatisation snipe, sera capable de prouver le but suivant :

Lemma mem_dec_imp_notNil z l : mem_dec z l = true → l <> [].

Un fichier d'exemple est disponible à l'adresse suivante : https://github.com/smtcoq/sniper/blob/JFLA23/theories/deciderel/examples.v

## 2 Contribution

La fonction mem_dec, est générée par une nouvelle commande decide sous la forme d'un point fixe :

<footnote>*Cette contribution est soutenue par un partenariat entre Nomadic Labs et l'Inria.</footnote>
Fixpoint mem_dec (z : Z) (l : list Z) :=
match l with
| [] ⇒ false
| x :: _ ⇒ Z.eqb z x (* une egalite decidable sur Z *)
end || match l with
| [] ⇒ false
| _ :: xs ⇒ mem_dec z xs
end

La commande génère automatiquement cette fonction en effectuant une disjonction booléenne (orb) entre deux fonctions intermédiaires qui correspondent respectivement à la règle MemMatch et à la règle MemRec. Les fonctions intermédiaires sont des filtrages par motifs qui renvoient true quand la conclusion d'un constructeur est applicable. Celles-ci peuvent nécessiter une linéarisation dans le type du constructeur, dans ce cas, la commande recherche s'il y a des égalités booléennes existantes sur les types donnés, mais elle ne les construit pas automatiquement.

Afin de permettre à SMTCoq de prouver automatiquement des buts mentionnant des prédicats décidables, nous présentons donc un prototype de commande decide générant une fonction booléenne équivalente et son intégration au sein du plugin Sniper [1].

Elle s'applique sur les inductifs I au codomaine dans Prop, avec des arguments de type Set, ne présentant pas d'ordre supérieur ou de dépendance, et dont les types des constructeurs sont de la forme :

$$
\forall (x_1 : A_1), \dots, (x_n : A_n), P_1 x_1 \dots x_n \to \dots \to P_k x_1 \dots x_n \to I t_1 \dots t_l
$$

Les $A_i$ sont des types inductifs de Set, chaque $P_i$ est un prédicat sur tout ou partie des $x_i$, et les $t_i$ sont des termes qui peuvent contenir des constructeurs appliqués aux $x_i$. Notons qu'une restriction est que tous les $x_i$ doivent apparaître dans la conclusion $I t_1 \dots t_l$. En générant le point fixe booléen qui décide la relation, elle utilise une heuristique simple pour trouver l'argument qui décroît.

3 Intégration au plugin Sniper

La commande decide fait partie des transformations logiques du plugin Sniper. L'idée de ce plugin est de combiner des transformations correctes de pré-processing sur un but Coq G, pour obtenir un but G', prouvable par une tactique d'automatisation et tel que G' → G. La transformation decide, appliquée sur une relation R, génère dans l'environnement global une fonction booléenne Rdec et une obligation de preuve que Rdec décide R (ou le terme de preuve quand la tactique fournie avec le plugin a réussi). Ensuite, une autre transformation appelée trakt [2], permet de remplacer toutes les occurences de R dans le but par des occurences de Rdec. A la fin de l'étape de pré-processing, le but transformé est envoyé au prouveur SMT veriT et prouvé automatiquement par celui-ci. Un certificat de preuve est renvoyé et vérifié dans Coq.

4 Travaux connexes

Pierre-Nicolas Tollitte et al. ont également travaillé sur la décision de relations inductives en Coq [5].
Leur approche est différente car leur objectif n'était pas seulement d'obtenir une fonction booléenne à partir
d'une relation inductive, mais aussi d'obtenir le k-ième argument d'une relation étant donné les autres
arguments. Cependant, leur développement ne gère pas les inductifs avec des paramètres, et les problèmes
de terminaison concernant les point fixes sont gérés par du fuel. Or, utiliser du fuel fait que l'on prouve
un énoncé de correction avec un quantificateur existentiel sur la variable de fuel. Ce genre d'énoncé n'est
pas exploitable par SMTCoq, qui ne supporte pas leur utilisation. Nous avons préféré cibler un fragment
des relations inductives qui supporte les paramètres et obtenir des preuves de correction sans fuel. Par
ailleurs, Zoe Paraskevopoulou et al. ont unifié plusieurs manières d'extraire du contenu calculatoire à partir
de relations inductives [4], mais leurs fonctions ne sont pas totales et donc restent inexploitables pour un
outil tel que SMTCoq.
Références

[1] Valentin Blot, Louise Dubois de Prisque, Chantal Keller, and Pierre Vial. General automation in Coq through modular transformations. In Chantal Keller and Mathias Fleury, editors, *Proceedings Seventh Workshop on Proof eXchange for Theorem Proving, PxTP 2021, Pittsburg, PA, USA, July 11, 2021*, volume 336 of *EPTCS*, pages 24–39, 2021.

[2] Denis Cousineau, Enzo Crance, and Assia Mahboubi. Trakt, uniformiser les types pour automatiser les preuves. In *JFLA'22 : Journées Francophones sur les Langages Applicatifs*, Annual Workshop. INRIA, INRIA, 2022.

[3] Burak Ekici, Alain Mebsout, Cesare Tinelli, Chantal Keller, Guy Katz, Andrew Reynolds, and Clark W. Barrett. SMTCoq : A plug-in for integrating SMT solvers into Coq. In Rupak Majumdar and Viktor Kuncak, editors, *Computer Aided Verification - 29th International Conference, CAV 2017, Heidelberg, Germany, July 24-28, 2017, Proceedings, Part II*, volume 10427 of *Lecture Notes in Computer Science*, pages 126–133. Springer, 2017.

[4] Zoe Paraskevopoulou, Aaron Eline, and Leonidas Lampropoulos. Computing correctly with inductive relations. In Ranjit Jhala and Isil Dillig, editors, *PLDI '22 : 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation, San Diego, CA, USA, June 13 - 17, 2022*, pages 966–980. ACM, 2022.

[5] Pierre-Nicolas Tollitte, David Delahaye, and Catherine Dubois. Producing certified functional code from inductive specifications. In Chris Hawblitzel and Dale Miller, editors, *Certified Programs and Proofs - Second International Conference, CPP 2012, Kyoto, Japan, December 13-15, 2012. Proceedings*, volume 7679 of *Lecture Notes in Computer Science*, pages 76–91. Springer, 2012.
# Caractériser des propriétés de confiance d'IA avec Why3

Julien Girard-Satabin, Michele Alberti, François Bobot, and Zakaria Chihani

Université Paris-Saclay, CEA, List, F-91120, Palaiseau, France
julien.girard2@cea.fr
firstname.lastname@cea.fr

## Résumé

Nous proposons de faire la démonstration de CAISAR, un logiciel libre en développement au sein du laboratoire de sûreté et sécurité des logiciels du CEA LIST. CAISAR est une plateforme permettant de caractériser la sûreté des logiciels résultant d'un protocole d'apprentissage (réseaux de neurones, machines à vecteur de support, forêts aléatoires). CAISAR se base sur la plateforme de vérification Why3 pour fournir un langage typé de modélisation de problèmes, ainsi qu'un moteur de raisonnement logique éprouvé. Cette approche autorise par exemple la vérification de systèmes composés de plusieurs blocs d'IA, ainsi qu'une meilleure expressivité des propriétés à vérifier. CAISAR est disponible à https://git.frama-c.com/pub/caisar.

## Proposition de présentation

### Contexte

Ces cinq dernières années ont vu naître le champ scientifique de la vérification formelle de programmes appris par réseaux de neurones. Ce champ est prospère : plus de vingt outils ont été ainsi développés sur cette période [12, 13, 21, 22, 18, 19, 16, 1, 11, 6, 14, 20, 7]. Ces travaux utilisent différentes techniques (interprétation abstraite, calcul SMT, programmation par contrainte), et utilisent souvent des heuristiques spécialisées sur des propriétés très spécifiques ; le plus souvent une invariance de la sortie par rapport à une perturbation de l'entrée circonscrite à un voisinage bien défini. Enfin, ces outils sont parfois limités quant aux programmes qu'ils peuvent vérifier, se limitant exclusivement aux réseaux de neurones convolutifs. Toutefois, nous observons que des idées développées dans certains outils percolent dans d'autres : ainsi, une heuristique spécifique faisant appel à des multiplateformes de Lagrange dans l'outil *OVAL*<fnref n="1" /> s'est ensuite vue réutilisée par ailleurs dans *αβ-CROWN* [22] et *ERAN* [19].

L'évolution rapide de ce domaine peut se comprendre comme la recherche, l'évaluation et la sélection de bonnes techniques de vérification par la communauté. Toutefois, à mesure que les programmes appris se voient intégrés dans des systèmes industriels, les exigences de sûreté et de sécurité vont croissant. Comment vérifier un système composé de différents programmes d'IA hétérogènes (par exemple : enchaînement de réseaux et de machines à vecteur de support) ? Comment vérifier des propriétés de conformité par rapport à des exigences fournies ? Pour tenter de répondre à ces questions, nous avons développé une plateforme dédiée à la caractérisation de la robustesse et de la sûreté des systèmes à base d'intelligence artificielle, CAISAR [9].

### Principes guidant la conception de CAISAR

L'objectif de CAISAR est de fournir une interface unifiée de modélisation de problème de vérification sur les programmes à base d'IA. Pour se faire, CAISAR se base sur la plateforme de vérification Why3 [8] et son langage WhyML. CAISAR modélise les propriétés à vérifier via des prédicats WhyML.

<footnote n="1">1. https://github.com/oval-group/oval-bab</footnote>
Une propriété classique dans la littérature [22, 18, 19, 3] est la robustesse locale de la prédiction par rapport à une perturbation locale, dont voici la définition. Soit un espace d'entrée $\mathcal{X}$ (qu'on peut restreindre sans perte de généralité à un sous-ensemble de $\mathbb{R}^d$). Soit un programme $f: \mathcal{X} \to \mathbb{R}$ associant à un échantillon $x \in \mathcal{X}$ une valeur réelle (par exemple, dans un problème de classification d'images, le programme associe à chaque échantillon une classe). Soit $\varepsilon \in \mathbb{R}$, et soit $d$ une distance (on utilise typiquement les normes $l_p$ pour $p \ge 1$). Un programme est alors localement robuste si, étant donné un échantillon $x_0 \in \mathcal{X}$ :

$$ \forall x, d(x, x_0) < \varepsilon \implies f(x) = f(x_0) $$

La Figure 1 montre comment écrire un prédicat WhyML pour modéliser cette propriété à vérifier, avec la norme $l_\infty$ comme fonction de distance. CAISAR, s'inspirant de Why3, propose une interface de modélisation unifiée avant de décharger des obligations de preuves à différents prouveurs automatiques.

## Quelques fonctionnalités

La plateforme gère principalement les réseaux de neurones sous Open Neural eXchange Format (ONNX)<fnref n="2" />. Ce choix est motivé par l'interopérabilité observée entre différents cadriciels d'apprentissage automatique (PyTorch, TensorFlow, Keras, Scikit-Learn). Les machines à vecteur de support sont gérées par un format csv ad-hoc. Enfin, il est possible pour l'utilisateur de spécifier un jeu de données particulier sur lequel vérifier les propriétés, via un fichier csv contenant les valeurs de chaque point de donnée. Actuellement, seuls les jeux de données de problèmes de classification peuvent être spécifiés ainsi : il est nécessaire de fournir une annotation explicite de la classe attendue pour chaque point.

Elle dispose d'une représentation intermédiaire du réseau de neurone permettant une traduction directe du réseau sous forme de formule logique, extractible en SMTLIB [2] grâce à Why3. Cette représentation intermédiaire ouvre également la voie à différentes transformations pour rendre la vérification plus simple, telles que la partition des entrées en régions linéaires [10].

CAISAR gère différents outils de vérification :

1. le Support Vector Machine reachability analysis tool (SAVer [15]), spécialisé dans les machines à vecteur de support

2. tous les solveurs standards prenant en entrée du SMTLIB (dont Alt-Ergo [4] et Z3 [5]); les solveurs spécialisés en réseaux de neurones tels que nnenum [1] supportent un format voisin, VNN-Lib<fnref n="3" />

3. le prouveur SMT Marabou [13] spécialisé dans le traitement des réseaux de neurones grâce à différentes optimisations d'algorithme de pivot et de parallélisme

4. un outil de test métamorphique pour les IA, AIMOS, développé en interne et pour l'instant en source fermée

5. l'analyseur abstrait PyRAT, également développé en interne https://pyrat-analyzer.com/

## Déroulement de la démonstration

La démonstration consiste d'abord à présenter le contexte au sein duquel se place CAISAR, et à quel besoin il répond. Nous présenterons les outils qu'il supporte ; et la nature des programmes traités (type de programme, taille, composabilité). Nous procéderons également à un comparatif avec d'autres approches comparables à CAISAR, telles que DNNV [17] et le tout récent Vehicle-lang<fnref n="4" />. Nous ferons

<footnote n="2">2. https://onnx.ai/</footnote>

<footnote n="3">3. http://www.vnnlib.org/</footnote>

<footnote n="4">4. https://github.com/vehicle-lang/vehicle</footnote>
ensuite une démonstration de la spécification d'un problème de validation sur plusieurs problèmes jouets, avec différentes propriétés, en détaillant quand il est possible de le faire les mécanismes sous-jacents de la génération d'obligations de preuves. Nous ouvrirons enfin sur de potentielles futures fonctionnalités de la plateforme.

**theory** DataSetClassification

**type** features = array t
**type** class = int

**type** datum = (features, class)
**type** label_ = int

**type** datum = (features, label_)

**type** dataset = {
  nb_features: int;
  nb_label_s: int;
  data: array datum
}
[...]
**type** model = {
  nbInputs: int;
  nbOutputs: int;
}

**function** predict: model → features → label_
[...]

**predicate** linfty_distance (a: features) (b: features) (eps: t) =
  a.length = b.length ∧
  **forall** i: int. 0 ≤ i < a.length → .- eps .< a[i] .- b[i] .< eps

**predicate** correct_at (m: model) (d: datum) =
  let (x, y) = d in
  y = predict m x
end

<caption>FIGURE 1 – Exemple de prédicats définis dans la bibliothèque standard de CAISAR. La fonction predict spécifie l'application d'un modèle m sur des entrées x. Le prédicat linfty_distance définit la norme $l_∞$, et correct_at est un prédicat qui vérifie si la prédiction d'un programme de classification est conforme à la vérité-terrain.</caption>
# Remerciements

Le développement de CAISAR est partiellement soutenu par le programme Confiance.ai<fnref n="5" />, et le projet PRISSMA<fnref n="6" />.

# Références

[1] Stanley Bak. Nnenum : Verification of ReLU Neural Networks with Optimized Abstraction Refinement. In Aaron Dutle, Mariano M. Moscato, Laura Titolo, César A. Muñoz, and Ivan Perez, editors, *NASA Formal Methods*, Lecture Notes in Computer Science, pages 19–36, Cham, 2021. Springer International Publishing.

[2] Clark Barrett, Pascal Fontaine, and Cesare Tinelli. The Satisfiability Modulo Theories Library (SMT-LIB). www.SMT-LIB.org, 2016.

[3] Marco Casadio, Ekaterina Komendantskaya, Matthew L Daggitt, Wen Kokke, Guy Katz, Guy Amir, and Idan Refaeli. Neural network robustness as a verification property : a principled case study. In *International Conference on Computer Aided Verification*, pages 219–231. Springer, 2022.

[4] Sylvain Conchon, Albin Coquereau, Mohamed Iguernlala, and Alain Mebsout. Alt-Ergo 2.2. In *SMT Workshop: International Workshop on Satisfiability Modulo Theories*, Oxford, United Kingdom, July 2018.

[5] Leonardo de Moura and Nikolaj Bjørner. Z3 : An Efficient SMT Solver. In C. R. Ramakrishnan and Jakob Rehof, editors, *Tools and Algorithms for the Construction and Analysis of Systems*, Lecture Notes in Computer Science, pages 337–340, Berlin, Heidelberg, 2008. Springer.

[6] Souradeep Dutta, Susmit Jha, Sriram Sanakaranarayanan, and Ashish Tiwari. Output Range Analysis for Deep Neural Networks. *arXiv:1709.09130 [cs, stat]*, September 2017.

[7] Ruediger Ehlers. Formal Verification of Piece-Wise Linear Feed-Forward Neural Networks. *arXiv:1705.01320 [cs]*, May 2017.

[8] Jean-Christophe Filliâtre and Andrei Paskevich. Why3 - Where Programs Meet Provers. In Matthias Felleisen and Philippa Gardner, editors, *Programming Languages and Systems*, Lecture Notes in Computer Science, pages 125–128, Berlin, Heidelberg, 2013. Springer.

[9] Julien Girard-Satabin, Michele Alberti, François Bobot, Zakaria Chihani, and Augustin Lemesle. CAISAR : A platform for Characterizing Artificial Intelligence Safety and Robustness. In *AI Safety*, CEUR-Workshop Proceedings, Vienne, Austria, July 2022.

[10] Julien Girard-Satabin, Aymeric Varasse, Marc Schoenauer, Guillaume Charpiat, and Zakaria Chihani. DISCO : Division of input space into convex polytopes for neural network verification. *JFLA*, 2021.

[11] P Henriksen and A Lomuscio. Efficient Neural Network Verification via Adaptive Refinement and Adversarial Search. In *24th European Conference on Artificial Intelligence - ECAI 2020*, page 8, Santiago de Compostela, Spain, 2020.

[12] Guy Katz, Clark Barrett, David Dill, Kyle Julian, and Mykel Kochenderfer. Reluplex : An efficient smt solver for verifying deep neural networks. *arXiv preprint arXiv:1702.01135*, 2017.

[13] Guy Katz, Derek A. Huang, Duligur Ibeling, Kyle Julian, Christopher Lazarus, Rachel Lim, Parth Shah, Shantanu Thakoor, Haoze Wu, Aleksandar Zeljić, David L. Dill, Mykel J. Kochenderfer, and Clark Barrett. The Marabou Framework for Verification and Analysis of Deep Neural Networks. In *Isil Dillig and Serdar Tasiran, editors, Computer Aided Verification, volume 11561*, pages 443–452. Springer International Publishing, Cham, 2019.

[14] Alessandro De Palma, Rudy Bunel, Alban Desmaison, Krishnamurthy Dvijotham, Pushmeet Kohli, Philip H. S. Torr, and M. Pawan Kumar. Improved branch and bound for neural network verification via lagrangian decomposition.

[15] Francesco Ranzato and Marco Zanella. Robustness verification of support vector machines. In *International Static Analysis Symposium*, pages 271–295. Springer, 2019.

<footnote n="5">5. https://www.confiance.ai/</footnote>

<footnote n="6">6. https://prissma.univ-gustave-eiffel.fr/</footnote>
[16] Zhouxing Shi, Huan Zhang, Kai-Wei Chang, Minlie Huang, and Cho-Jui Hsieh. Robustness Verification for Transformers. In *International Conference on Learning Representations*, 2020.

[17] David Shriver, Sebastian Elbaum, and Matthew B. Dwyer. DNNV: A Framework for Deep Neural Network Verification. In Alexandra Silva and K. Rustan M. Leino, editors, *Computer Aided Verification*, Lecture Notes in Computer Science, pages 137–150, Cham, 2021. Springer International Publishing.

[18] Gagandeep Singh, Timon Gehr, Matthew Mirman, Markus Püschel, and Martin Vechev. Fast and Effective Robustness Certification. In S. Bengio, H. Wallach, H. Larochelle, K. Grauman, N. Cesa-Bianchi, and R. Garnett, editors, *Advances in Neural Information Processing Systems 31*, pages 10802–10813. Curran Associates, Inc., 2018.

[19] Gagandeep Singh, Timon Gehr, Markus Püschel, and Martin Vechev. An abstract domain for certifying neural networks. *Proceedings of the ACM on Programming Languages*, 3(POPL):1–30, 2019.

[20] Caterina Urban, Maria Christakis, Valentin Wüstholz, and Fuyuan Zhang. Perfectly Parallel Fairness Certification of Neural Networks. arXiv:1912.02499 [cs], December 2019.

[21] Shiqi Wang, Kexin Pei, Justin Whitehouse, Junfeng Yang, and Suman Jana. Efficient Formal Safety Analysis of Neural Networks. In S. Bengio, H. Wallach, H. Larochelle, K. Grauman, N. Cesa-Bianchi, and R. Garnett, editors, *Advances in Neural Information Processing Systems 31*, pages 6367–6377. Curran Associates, Inc., 2018.

[22] Shiqi Wang, Huan Zhang, Kaidi Xu, Xue Lin, Suman Jana, Cho-Jui Hsieh, and J. Zico Kolter. Beta-CROWN: Efficient Bound Propagation with Per-neuron Split Constraints for Complete and Incomplete Neural Network Robustness Verification.
# Necro ML: Kit de Nécromancie (Démonstration)

Louis Noizet and Alan Schmitt

INRIA Rennes - Bretagne Atlantique

## Abstract

On présente Necro ML, un outil pour générer des interpréteurs OCaml à partir de sémantiques en Skel, un langage minimaliste de description de sémantiques. Ces interpréteurs sont modulaires, en exploitant des monades pour interpréter les calculs.

## Introduction

Ce travail est initialement basé sur les travaux de Courant et al. [3]. En particulier, le langage Skel a été largement amélioré, avec du polymorphisme, des fonctions de première classe, et du filtrage. L'interpréteur OCaml généré est maintenant modulaire pour l'interprétation des branches, ce qui permet d'en changer aisément. La section 1 présente le langage Skel. La section 2 décrit comment un interpréteur est généré. Enfin, la section 3 montre comment les monades d'interprétations peuvent être utilisées pour représenter différents comportements de l'interpréteur. Lors de la démonstration, nous présenterons le fonctionnement de Necro ML et l'usage de différentes monades d'interprétations pour traiter le non-déterminisme.

### 1 Skel

Skel [2] est un langage statiquement typé pour décrire des sémantiques opérationnelles de langages. Il est à la fois léger et puissant, et une sémantique squelettique peut notamment être extraite vers un générateur OCaml, une formalisation Coq, et un débogueur. Le langage Skel est basé sur ML avec une construction supplémentaire appelée le branchement pour traiter les calculs non-déterministes, et la possibilité de sous-spécifier.

Une des fonctionnalités principales de Skel est la séparation entre squelettes et termes. Les premiers représentent des calculs, et les seconds des valeurs. Cela est inspiré du λ-calcul computationnel de Moggi [6].

Skel est proche de langages ML comme OCaml ou SML, mais son AST est léger, de manière à pouvoir être manipulé plus simplement. Il est défini dans [7], et contient uniquement 126 lignes de spécification, ce qui permet de gérer et extraire facilement des sémantiques.

### 2 Necro ML

Necro est un écosystème pour manipuler les sémantiques squelettiques. Il repose sur Necro Lib [7], une bibliothèque OCaml qui définit la syntaxe de Skel, et un ensemble de fonctions pour manipuler les sémantiques squelettiques, y compris la fonction `parse_and_type`, qui lit un fichier et renvoie une sémantique squelettique typée.

Ainsi, n'importe qui a accès à la syntaxe et à des fonctions de base, pour pouvoir créer des outils qui exploitent les sémantiques squelettiques et étendent l'écosystème Necro. En plus de Necro Lib, nous fournissons plusieurs outils. L'un d'eux, celui que nous présentons ici, est Necro ML [5], qui génère des interpréteurs OCaml depuis des sémantiques squelettiques.
<figure><img src="image_104.png" /><figcaption>Figure 1: The Necro ecosystem</figcaption></figure>

Comme nous l'avons précisé dans la section 1, il y a dans les sémantiques squelettiques des données non-spécifiées. Cela est traité par Necro ML de manière modulaire. On génère un fonc-teur *MakeInterpreter*, qui produit un interpréteur quand on lui fournit une implémentation des termes et types non-spécifiés.

Le plongement est principalement superficiel, mais on doit gérer les branches avec prudence, puisque OCaml n'a pas de construction native équivalente. Nous allons donc montrer comment cela est traité dans la section 3.

# 3 Monade d'interprétation

Comme expliqué plus haut, on ne peut pas utiliser un simple plongement profond, en raison des constructions non-déterministes. À cette fin, on utilise une monade de plongement, ou monade d'interprétation, pour décrire les calculs. Ainsi, les termes de type 'a sont plongés superficielle-ment dans des expressions OCaml de type 'a, tandis que les squelettes de type 'a sont plongés profondément dans des expressions OCaml de type 'a M.t. Necro ML propose plusieurs mon-ades d'interprétations, et d'autres peuvent être définies par l'utilisateurice. L'aspect principal est qu'il est très simple de changer la monade d'interprétation sans avoir à réécrire aucun code.

# 4 Conclusion

Necro ML est un outil flexible pour générer des interpréteurs. Il effectue un plongement super-ficiel des types, et semi-profond des expressions pour gérer le non-déterminisme. Il a été testé sur des fichiers de taille significative, notamment dans le travail en cours de formalisation de JavaScript [4].

D'autre projets sont intimement liés. D'abord, Necro Debug est une exécution pas-à-pas d'une sémantique squelettique.<fnref n="1" /> Il utilise la même approche et les même signatures de modules que Necro ML, ce qui permet de réutiliser l'instanciation des termes non-spécifiés. Ensuite, Ambal et al. ont présenté un générateur d'interpréteurs certifiés à l'aide de Necro Coq et du mécanisme d'extraction [1].

<footnote n="1">¹https://skeletons.inria.fr/debugger/indexwhile.html</footnote>
References

[1] Guillaume Ambal, Sergueï Lenglet, and Alan Schmitt. Certified Abstract Machines for Skeletal Semantics. In *Certified Programs and Proofs*, Philadelphia, United States, January 2022.

[2] Martin Bodin, Philippa Gardner, Thomas Jensen, and Alan Schmitt. Skeletal Semantics and their Interpretations. *Proceedings of the ACM on Programming Languages*, 44:1–31, 2019. URL: https://hal.inria.fr/hal-01881863, doi:10.1145/3290357.

[3] Nathanaëlle Courant, Enzo Crance, and Alan Schmitt. Necro: Animating Skeletons. In *ML 2019*, Berlin, Germany, Aug 2019.

[4] Adam Khayam, Louis Noizet, and Alan Schmitt. JSkel: Towards a Formalization of JavaScript's Semantics, 2022. Submitted for publication.

[5] Enzo Crance, Martin Bodin, Nathanaëlle Courant and Louis Noizet. Necro Ocaml Generator. URL: https://gitlab.inria.fr/skeletons/necro-ml.

[6] Eugenio Moggi. Computational lambda-calculus and monads. *Proceedings. Fourth Annual Symposium on Logic in Computer Science*, 1988.

[7] Louis Noizet. Necro Library. URL: https://gitlab.inria.fr/skeletons/necro.
Auteurs

<table>
  <tbody>
    <tr>
      <td>Abou Samra, Jean</td>
      <td>7</td>
    </tr>
    <tr>
      <td>Alberti, Michele</td>
      <td>291</td>
    </tr>
    <tr>
      <td>Baudart, Guillaume</td>
      <td>24</td>
    </tr>
    <tr>
      <td>Bertholon, Guillaume</td>
      <td>43</td>
    </tr>
    <tr>
      <td>Blaudeau, Clément</td>
      <td>59</td>
    </tr>
    <tr>
      <td>Bobot, François</td>
      <td>291</td>
    </tr>
    <tr>
      <td>Bodin, Martin</td>
      <td>7</td>
    </tr>
    <tr>
      <td>Boldo, Sylvie</td>
      <td>2</td>
    </tr>
    <tr>
      <td>Bourke, Timothy</td>
      <td>101</td>
    </tr>
    <tr>
      <td>Bussone, Grégoire</td>
      <td>24</td>
    </tr>
    <tr>
      <td>Butte, Elliot</td>
      <td>172</td>
    </tr>
    <tr>
      <td>Carnier, Denis</td>
      <td>285</td>
    </tr>
    <tr>
      <td>Charguéraud, Arthur</td>
      <td>43</td>
    </tr>
    <tr>
      <td>Chihani, Zakaria</td>
      <td>291</td>
    </tr>
    <tr>
      <td>Cohen, Cyril</td>
      <td>3</td>
    </tr>
    <tr>
      <td>Contejean, Évelyne</td>
      <td>121</td>
    </tr>
    <tr>
      <td>Correnson, Arthur</td>
      <td>265, 285</td>
    </tr>
    <tr>
      <td>Dubois de Prisque, Louise</td>
      <td>288</td>
    </tr>
    <tr>
      <td>Filliâtre, Jean-Christophe</td>
      <td>274</td>
    </tr>
    <tr>
      <td>Gardelle, Samuel</td>
      <td>134</td>
    </tr>
    <tr>
      <td>Girard-Satabin, Julien</td>
      <td>291</td>
    </tr>
    <tr>
      <td>Jensen, Thomas</td>
      <td>152</td>
    </tr>
    <tr>
      <td>Ledein, Amélie</td>
      <td>172</td>
    </tr>
    <tr>
      <td>Leroy, Xavier</td>
      <td>4</td>
    </tr>
    <tr>
      <td>Mandel, Louis</td>
      <td>24</td>
    </tr>
    <tr>
      <td>McNally, Christopher</td>
      <td>285</td>
    </tr>
    <tr>
      <td>Miné, Antoine</td>
      <td>211</td>
    </tr>
    <tr>
      <td>Miquey, Étienne</td>
      <td>134</td>
    </tr>
    <tr>
      <td>Moawad, Youssef</td>
      <td>285</td>
    </tr>
    <tr>
      <td>Monat, Raphaël</td>
      <td>211</td>
    </tr>
    <tr>
      <td>Noizet, Louis</td>
      <td>296</td>
    </tr>
    <tr>
      <td>Paskevich, Andrei</td>
      <td>274</td>
    </tr>
    <tr>
      <td>Pesin, Basile</td>
      <td>101</td>
    </tr>
    <tr>
      <td>Pouzet, Marc</td>
      <td>101</td>
    </tr>
    <tr>
      <td>Radanne, Gabriel</td>
      <td>59</td>
    </tr>
    <tr>
      <td>Rébiscoul, Vincent</td>
      <td>152</td>
    </tr>
    <tr>
      <td>Rémy, Didier</td>
      <td>59</td>
    </tr>
    <tr>
      <td>Samokish, Andrei</td>
      <td>121</td>
    </tr>
    <tr>
      <td>Scherer, Gabriel</td>
      <td>190</td>
    </tr>
    <tr>
      <td>Schmitt, Alan</td>
      <td>152, 296</td>
    </tr>
    <tr>
      <td>Tasson, Christine</td>
      <td>24</td>
    </tr>
    <tr>
      <td>Valnet, Milla</td>
      <td>211</td>
    </tr>
    <tr>
      <td>Wallez, Théophile</td>
      <td>243</td>
    </tr>
    <tr>
      <td>Zakowski, Yannick</td>
      <td>7</td>
    </tr>
  </tbody>
</table>
Le comité d'organisation des JFLA 2023 remercie chaleureusement ses généreux mécènes.

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

CEA List

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

OCaml
Software Foundation

Fondation OCaml

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

GDR Groupement de recherche
GPL Génie de la programmation et du logiciel

GDR GPL

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

MITSUBISHI
ELECTRIC

*Changes for the Better*

Mitsubishi Electric

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

nomadic labs

Nomadic Labs

OCaml

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

OCamlPro

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

Tarides

Tarides

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

TrustInSoft