Keywords: program differences, operational semantics, mechanically-checked proofs in Coq, verification, relational logic différences de programmes, sémantique opérationnelle, preuves mécanisées en Coq, vérification, logique relationnelle

Comme il est de coutume, il convient de commencer ces remerciements par mes directeurs de thèse. Merci, donc, tout d'abord, à Roberto Di Cosmo, pour avoir accepté de diriger ma thèse, et pour avoir suivi de loin mon travail. Merci aussi à mon codirecteur David Mentré, pour son regard extérieur sur mes travaux, pour avoir supporté mon librisme quotidien, et grâce à qui les développements logiciels réalisés lors de cette thèse peuvent être distribués sous licence libre. Merci enfin et surtout à Yann Régis-Gianas, mon directeur de thèse officieux, pour son encadrement scientifique inestimable et pour avoir su faire face, pendant ces longues années, à mon pessimisme régulier.

Merci à David Pichardie et à Gilles Barthe pour avoir accepté de rapporter ma thèse. Merci également à ce second pour ses travaux qui ont été une importante source d'inspiration, en témoigne le Chapitre 2 de cette thèse. Merci à Julien Cohen pour avoir accepté de faire partie du jury, et à Julia Lawall pour avoir accepté de le présider.

Thanks also to J Strother Moore for helping me keep my stress to manageable levels during my first participation to an international conference.

1 Aussi bien musicalement qu'au niveau de l'idéologie véhiculée. 2 Et qui a tendance à abuser des notes de bas de page. 3 Maladroitement augmentée de quelques glyphes par l'auteur de cette thèse. 4 Il n'est d'ailleurs pas impossible que le titre à rallonge de ce chapitre ne soit en fait qu'une excuse pour utiliser une esperluette et de multiples ornements.

La majorité de mes travaux ayant été menés à PPS l'IRIF, il serait mal venu de ne pas remercier les nombreux collègues que j'y ai côtoyés. Merci donc, tout d'abord, aux collègues partageant mon bureau, en commençant par celui dont la ponctualité est plus que discutable et qui entretient une fascination quelque peu morbide pour toutes sortes de dictateurs. Merci également à son acolyte à peine plus ponctuelle, avec qui les discussions politiques ou historiques ne manquent pas. Merci aussi à l'aîné du 3033, qui n'y vient plus troller qu'à temps partiel.

Il convient ensuite de remercier les doctorants un peu plus lointains, tels que ceux qui ont aménagé leur bureau d'un canapé ma foi fort confortable, ou celles et ceux qui ont orchestré l'emprunt d'un manuscrit extraordinaire ainsi que la numérisation de ses 777 pages… Des remerciements sont également dûs aux courageux étudiants d'un directeur de thèse particulièrement insaisissable, reclus ensembles au fond d'un même bureau, qu'il s'agisse d'un doctorant extrêmement bavard, d'un autre qui semble parfois être sous le coup d'une malédiction, ou de ce dernier dont la foi ne semble pas affecter l'ouverture d'esprit et qui donne souvent l'impression d'être monté sur ressorts.

Il me faut aussi remercier mes anciens collègues, tels que le fameux « surfer australien » germanique, ou la ribambelle de docteurs tous plus brillants les uns que les autres, comme la personne m'ayant fait découvrir un des pires groupes de chanteuses qu'il m'ait été donné d'écouter 1 , l'homme en short à l'humour redoutable, la workaholic qui emmenait ses collègues boire pour perfectionner son Français, ou la championne du syndrome de l'imposteur qui a finalement soutenu l'équivalent d'au moins deux thèses.

Merci également aux stagiaires qui nous ont rendu visite ainsi qu'à mes autres collègues de l'IRIF, que j'ai moins connus ou qu'un moment d'égarement m'aurait fait ne pas citer.

En dehors du monde académique, je tiens également à remercier un ami de longue date dont la radicalisation s'est grandement accélérée suite à son séjour outre manche, l'ex-tartine cubique, l'homme que tout le monde connaît 2 et qui a joué un rôle certain dans mon choix de me diriger vers la recherche, l'administrateur réseau dont l'addiction au café en a même affecté son pseudonyme, le grand curieux adepte du shitpost et des arcs-en-ciel, le barbu reconnu pour ses jeux de mots et par sa façon systématique de partager le moindre selfie, l'esperluette abattant une quantité de travail redoutable et dont l'enthousiasme est plus que communicatif, ainsi que le petit curieux dont le coeur balance entre le serpent et la pierre précieuse et à qui je dois beaucoup de soutien.

Thanks to codemom, for her invaluable work and her support. Thanks to the multiple owners of cuddly dinosaurs for sharing their cuteness online. Thanks also to gargamel, whose work has played a significant role in me meeting or keeping in touch with many of the people I have already thanked in those last two paragraphs.

Merci à toutes les personnes qui participent et font vivre des hackerspaces inclusifs, à toutes les personnes qui se battent pour préserver les libertés individuelles sur Internet ou hors ligne, qui militent activement pour davantage de justice sociale, et pour rendre le monde un peu meilleur à leur façon.

Merci à Jany Belluz pour la police Fantasque Sans Mono 3 utilisée pour les extraits de code, ainsi qu'à Black [Foundry] pour la police Inria Serif utilisée pour le reste de cette thèse 4 .

Merci, enfin, à toutes les autres personnes formidables qui sont malheureusement parvenues, d'une manière ou d'une autre, à échapper jusqu'ici à ces remerciements.

Our first contribution is an algorithm for the construction of a correlating program, that is, a program interleaving the instructions of two input programs in such a way that it simulates their semantics. Further static analysis can be performed on such correlating programs to compute an over-approximation of the semantic differences between the two input programs. This work draws direct inspiration from an article by Partush and Yahav [START_REF] Partush | Abstract Semantic Differencing for Numerical Programs[END_REF], that describes a correlating program construction algorithm which we show to be unsound on loops that include b r e a k or c o n t i n u e statements. To guarantee its soundness, our alternative algorithm is formalized and mechanically checked within the Coq proof assistant.

Our second and most important contribution is a formal framework allowing to precisely describe and formally verify semantic changes. This framework, fully formalized in Coq, represents the difference between two programs by a third program called an oracle. Unlike a correlating program, such an oracle is not required to interleave instructions of the programs under comparison, and may "skip" intermediate computation steps. In fact, such an oracle is typically written in a different programming language than the programs it relates, which allows designing correlating oracle languages specific to certain classes of program differences, and capable of relating crashing programs with non-crashing ones.

We design such oracle languages to cover a wide range of program differences on a toy imperative language. We also prove that our framework is at least as expressive as Relational Hoare Logic by encoding several variants as correlating oracle languages, proving their soundness in the process.

Résumé

La comparaison de programmes informatiques est au coeur des pratiques actuelles de développement logiciel : en effet, les programmes informatiques n'étant pas écrits d'un seul coup, mais par des modifications successives souvent effectuées par plusieurs programmeurs, il est essentiel de pouvoir comprendre chacune de ces modifications.

Des outils, tels que d i f f et p a t c h existent pour traiter des différences entre programmes. Cependant, ces outils représentent les différences comme la liste des lignes modifiées, ajoutées ou supprimées du code source d'un programme, et ne traitent pas de sa sémantique.

Il convient donc de trouver des façons de représenter et raisonner à propos des différences entre programmes au niveau sémantique, ce à quoi cette thèse s'attelle.

Programmes de corrélation

La première partie de notre travail se concentre sur l'inférence automatique de différences sémantiques entre deux programmes. Dans cette optique, nous avons repris un article d'Eran Yahav et Nimrod Partush [START_REF] Partush | Abstract Semantic Differencing for Numerical Programs[END_REF] décrivant une technique pour calculer une sur-approximation des variables ayant une valeur différente à l'issue de l'exécution des deux programmes. Pour ce faire, l'approche décrite par Eran Yahav et Nimrod Partush consiste à produire un programme de corrélation entrelaçant statiquement les instructions des deux programmes de façon à ce que le programme de corrélation simule les deux programmes à comparer. Ce programme de corrélation est alors analysé par un outil d'interprétation abstraite utilisant un domaine relationnel pour tenter de préserver des relations-si possible d'égalité-entre les variables des deux programmes.

Malheureusement, l'algorithme décrit pour calculer les programmes de corrélation est incorrect. En effet, nous montrons qu'en présence d'instructions g o t o , b r e a k ou c o n t i n u e , le programme de corrélation engendré par l'algorithme proposé ne simule pas toujours les programmes à comparer.

Pour remédier à cela, nous proposons un nouvel algorithme de calcul de programmes de corrélation. Contrairement à l'approche très textuelle de l'algorithme de Nimrod Partush et Eran Yahav, cet algorithme repose sur une notion de différence syntaxique structurée, qui représente la différence entre deux arbres de syntaxe abstraite. Cette représentation très syntaxique et structurée des différences facilite grandement 5 l'écriture de notre algorithme, qui prend la forme d'une fonction définie récursivement sur la structure de la différence syntaxique. Cette définition récursive permet à son tour une preuve par induction structurelle.

En effet, contrairement à l'article d'origine, nos travaux sont formalisés et prouvés corrects grâce à l'assistant de preuve Coq. Cette formalisation nous paraît nécessaire compte tenu de la facilité avec laquelle il est possible de faire des erreurs lors de la conception de ce type d'algorithmes, comme en témoigne l'erreur présente dans l'article d'origine.

Oracles de corrélation

Pour la suite de notre travail, nous nous sommes intéressés à la spécification et à la vérification de différences sémantiques, plutôt qu'à leur inférence automatique. Dans ce contexte, nous proposons un cadre formel permettant de décrire et représenter des différences sémantiques entre programmes. En effet, nous partons du principe que la personne qui effectue une modification le fait avec une intention précise, qu'il pourrait décrire si un formalisme le lui permettait. Une fois cette intention formellement décrite, il serait possible de prouver que la modification effectuée y correspond, que ce soit de manière automatique ou en écrivant une preuve manuellement.

À la manière des programmes de corrélation, nous avons décidé de représenter la différence entre deux programmes par un troisième programme. Cependant, contrairement à un programme corrélé, ce troisième programme-que nous appelons oracle de corrélation-n'est pas forcément un entrelacement des instructions des deux autres programmes, et est autorisé à « sauter » des instructions des programmes à comparer. Un tel oracle de corrélation n'est d'ailleurs généralement pas écrit dans le même langage de programmation que les programmes qu'il met en relation, mais dans un langage spécialisé. Un tel langage spécialisé, ou langage d'oracles, caractérise un type de différences spécifique.

Plus précisément, afin de pouvoir mettre en relation des programmes qui ne terminent pas, ainsi que des programmes susceptibles de planter, nous nous plaçons dans le cadre de la sémantique opérationnelle à petits pas : un langage de programmation est défini entre autres par des règles de réduction décrivant comment les programmes s'exécutent. L'exécution d'un programme donné est donc une succession d'états obtenus par des réductions-ou petits pas-successives.

Dans ce cadre, un langage d'oracles est aussi défini par une sémantique opérationnelle à petit pas. Un état de l'oracle induit une relation entre les états des programmes gauche et droit mis en relation. Chaque pas de l'oracle correspond alors à un certain nombre de pas dans les programmes à mettre en relation. En plus de sa sémantique opérationnelle à petits pas, un langage d'oracles est défini par une propriété définie sur les états de l'oracle, par exemple que les états mis en relation assignent bien la même valeur à certaines variables. Cette propriété, appelée invariant, sert à la fois à caractériser la relation que l'on veut montrer entre les deux programmes, et comme outil de preuve qu'un oracle simule bien deux programmes donnés, c'est-à-dire que chaque pas de l'oracle correspond effectivement à un nombre non-nul de pas des programmes gauche et droite. Afin d'évaluer le cadre formel esquissé plus haut, nous avons écrit un ensemble de langages d'oracles pour un langage impératif jouet appelé Imp. Ces langages d'oracles couvrent aussi bien des modifications qui n'influent pas sur le résultat final de l'exécution des deux programmes-comme l'échange de deux affectations successives indépendantes ou l'échange de deux branches d'une conditionnelle-que des modifications qui changent profondément la sémantique des deux programmes-comme la correction d'une erreur fatale en rajoutant une condition défensive, ou la modification de la valeur d'une variable qui n'influe pas sur le flot de contrôle du programme.

Tout comme pour la première partie de notre travail, ce cadre formel ainsi que les différents langages d'oracles sur Imp ont été formellement définis à l'aide de l'assistant de preuve Coq et toutes les preuves de correction ont également été vérifiées grâce à cet outil.

Langages de différences

La finalité de notre travail étant de permettre à des programmeurs de décrire leurs modifications et de vérifier qu'elles correspondent bien à leurs intentions, il convient de leur proposer un langage homogène pour le faire. Nous avons donc défini une notion de langage de différences, permettant de composer des différences primitives pour décrire les différences sémantiques entre deux programmes.

Un langage de différences fournit une syntaxe pour décrire des relations entre traces d'exécution. En pratique, nous utilisons des oracles pour caractériser ces traces et vérifier la correction des différences décrites.

Introduction

Much like other kinds of creative or engineering activities, software development is a process: as one can imagine, programs are rarely written in one fell swoop, but rather developed over an extended period of time. Indeed, large programs are always written in a series of incremental changes. In fact, common programming methodologies encourage starting from minimal programs and progressively adding and generalizing functionality with consistent, separate and minimal changes. Many software projects also have long life cycles, with increasingly frequent updates after an initial release: newer versions get released for various reasons, such as fixing bugs, improving performances, adding requested features, maintaining compatibility with other software, or addressing security issues. All those updates constitute program changes, possibly written by multiple developers.

All of the aforementioned changes are made of modifications to the source code of the program, that is the human-readable set of instructions that is later processed by a computer to execute the program. Those changes to the source code may consequently change its semantics-that is, the program's meaning, how it actually behaves and what it computes. Each one of those changes is made with a precise intent in mind, such as fixing a bug, adding a feature, or simply making the code more readable to other programmers. It is common practice for programmers to explain that intent and the reasoning behind the change-also called a patch, from when programs were written on paper tapes or punched cards, and modifying an existing program required physically cutting and patching it-to other programmers.

In fact, this notion of program differences is so central to the practice of programming that nearly all software development is done using a version control system [START_REF] Jacobson | The unified software development process[END_REF][START_REF] Walter F Tichy | RCS-a system for version control[END_REF] such as g i t [15] or m e r c u r i a l [START_REF] Mercurial | [END_REF], a tool that stores successive versions of given documents-typically source code-and is often structured around changesets, sets of consistent differences between versions accompanied by a commit message, an informal description of the change given by the person who wrote it.

As discussed before, changes made to a program are made with a specific intent which is typically described in a free-form informal text message accompanying the change, but the patch may have unintended consequences: it may add new bugs-also called regressions-or it may be downright incorrect, not matching the intent of the programmer. Verifying that the patch indeed corresponds to the programmer's intent and does not introduce new issues [START_REF] Strichman | Regression Verification -A Practical Way to Verify Programs[END_REF] is the main motivation behind the common practice of code review in which at least one other programmer reviews the proposed 11 INTRODUCTION patch before it gets included in the project.

To summarize, patches are pervasive and essential to software development, and as such, understanding them and reasoning about them is an important topic of software development [START_REF] Shuvendu | Differential Static Analysis: Opportunities, Applications, and Challenges[END_REF]. Characterizing patches, and in particular their impact on the semantics of programs, is essential. An appropriate characterization of program differences may help programmers understand their changes, assist them with code review, or limit the number of regression tests-tests written in order to spot unwanted changes in program behavior when updating it-to run [START_REF] Binkley | Using semantic differencing to reduce the cost of regression testing[END_REF].

Textual differences and informal messages

By far the most common characterization of program differences are textual differences-as produced and processed by the d i f f [START_REF] Wayne | An algorithm for differential file comparison[END_REF][START_REF] Mackenzie | Comparing and Merging Files With Gnu Diff and Patch[END_REF] and p a t c h [START_REF] Mackenzie | Comparing and Merging Files With Gnu Diff and Patch[END_REF] utilities-together with informal free-form textual messages from the programmer. Both of those representations are typically displayed together in version control systems and code review platforms.

A textual difference, or diff for short, is an unambiguous, formal-if lowlevel-representation of the change on the program's source code seen as an unstructured piece of text. Such a diff lists modified portions of the document, presenting lines that are either removed from the original version, added in the modified version or kept unchanged between the two versions. Lines containing modifications but otherwise present in both versions are considered removed from the original version and added to the modified version. Those removed and added lines are accompanied by the location at which they appear in both versions of the program, so that the patch can be mechanically applied to the old program to get the new one, as does the p a t c h utility. They are also commonly surrounded by some unmodified lines, partly in order to provide some context to a person reading the patch, and partly as a means for the p a t c h utility to check that it is being applied to the intended file-it will fail if it cannot find a list of lines matching the context.

For instance, let us consider two versions of a sample C program: In the example above, the right program has been obtained by renaming every occurrence of the variable "y " in the left program to "c o u n t ". The intent behind this change would typically have been to make the code more readable by using more meaningful variable names. In any case, this difference would typically be represented as the following diff : On the one hand, as stated above, textual differences describe the changes between two programs' source code precisely and unambiguously. They are formal representations of those changes, so they can be automatically manipulated by computer programs, and, to some extent, reasoned about. However, they are also purely textual. This means the d i f f and p a t c h utilities work for any text-based programming language, but they cannot exploit the programming language's syntax or semantics in any way. A diff thus cannot efficiently convey the meaning of the programmer nor provide any insight on the way the change actually affects the program's execution. Depending on the nature of the described change, they can also be needlessly verbose: for instance, in the example above, almost every line is affected by the patch, even though it can be summarized as renaming the variable "y " to "c o u n t ".

On the other hand, commit messages are free-form textual messages written by and meant for programmers. They usually explain the intent the programmer had when making that change, make claims about the expected program semantics, and explain the reasoning behind it. Being free-form, though, commit message are neither exact nor complete, and cannot be automatically manipulated by computer programs in any meaningful way. Furthermore, since this message is informal, it can also be understood differently by different programmers, and it can be difficult to verify that it actually corresponds to the exact program difference. In general, such change descriptions provide valuable insight from the programmer, but cannot be used in a formal or automated setting.

Those two very common kinds of change descriptions are thus complementary. In particular, during code review, reviewers analyze the patch in light of the commit message, but as explained earlier, this has to be a manual-hence error-prone-operation.

For this reason, we are interested in providing ways to reason about the semantic implications of program changes. While there are several existing theoretical constructs to semantically relate pairs of programs [START_REF] Lamport | The existence of refinement mappings[END_REF], we are especially interested in practical tools that could be used by programmers to formally specify relational properties-that is, properties referencing multiple programs-and, ultimately, mechanically INTRODUCTION verify them. To this end, we have initially investigated automatically inferring relational properties from textual changes. However, while that approach may in some cases be successful at proving or disproving that two programs are equivalent, the automatically-inferred properties may not actually be of any interest to the programmer. Indeed, the result of such an analysis is purely extensional, making it difficult to reason about intensional properties such as optimizations. Furthermore, it is also somewhat low-level, as it describes relations between the final values of both programs' variables with linear equations. Finally, it is often imprecise: due to the nature of the relational analysis, some relations cannot be described precisely. In other cases, achieving enough precision to prove expected properties is possible, but requires the programmer to manually instruct the tool with very specific low-level hints, which should not be required from them to formally specify their intent. For these reasons, our focus moved to developing new structured and semantics-focused descriptions of program changes that allow programmers to specify the properties they are interested in and allowing them to subsequently prove them.

Inferring properties from a textual change

The first approach we have explored to understand program differences is to automatically infer properties relating both programs from a textual change. For instance, one can imagine a tool providing a sound approximation of the set of variables that have different values at the end of the execution of both programs, thus highlighting their similarities and differences.

We first attempted building such a tool. In fact, as we started working on that idea, we found very similar existing work by Eran Yahav and Nimrod Partush [START_REF] Partush | Abstract Semantic Differencing for Numerical Programs[END_REF]. Their approach consisted in building a single correlating program simulating the parallel execution of two successive versions of a same program. The purpose of this correlating program is to interleave instructions of both programs' source code in a way such that "corresponding" instructions of both programs would appear next to each other while maintaining the meaning of both programs. Doing so enables further static analysis of the correlating program with existing-if tweaked for this case-techniques.

For instance, a very simplified correlating program of the two C example programs defined earlier could be the following program, in which variables prefixed by "T _ " refer to the right program while those not prefixed by "T _ " refer to the left program:

C o r r e l a t i n g p r o g r a m s u m = 0 ; T _ s u m = 0 ; x = -x ; T _ x = -T _ x ; y = 0 ; T _ c o u n t = 0 ; g u a r d = ( s u m < x ) ; T _ g u a r d = ( T _ s u m < T _ x ) ; w h i l e ( g u a r d | | T _ g u a r d ) { i f ( g u a r d ) y = y + 1 ; i f ( T _ g u a r d ) T _ c o u n t = T _ c o u n t + 1 ; i f ( g u a r d ) s u m = s u m + 1 + 2 * y ; i f ( T _ g u a r d ) T _ s u m = T _ s u m + 1 + 2 * T _ c o u n t ; i f ( g u a r d ) g u a r d = ( s u m < x ) ; i f ( T _ g u a r d ) T _ g u a r d = ( T _ s u m < T _ x ) ; }
Notice how this correlating program closely interleaves instructions of both programs, factorizing left and right loops in the process, while allowing them to have different numbers of iterations thanks to the use of the guard variables g u a r d and T _ g u a r d .

However, as we studied Yahav and Partush's article and the accompanying tool, we found issues with their generation algorithm for the correlating program: there were cases where the generated program would incorrectly simulate the two programs under consideration. This lead us to design an alternative algorithm for building that correlating program. As illustrated by the issues in the original paper [START_REF] Partush | Abstract Semantic Differencing for Numerical Programs[END_REF], the kind of program transformations required to build a correlating program is particularly error prone. For this reason, we implemented our algorithm and proved it correct using the Coq proof assistant, thus ensuring that it would correctly simulate the two programs under consideration in all cases, while we also experimentally verified that it achieved an interleaving of the two programs which is compatible with the further static analysis techniques described in the original paper [START_REF] Partush | Abstract Semantic Differencing for Numerical Programs[END_REF]. This notion of having mathematical proofs-mechanically verified by computer software such as the Coq proof assistant-is a cornerstone of this thesis: each of our contributions is indeed formalized in Coq and any stated theorem is also proved within this formal framework.

While formalizing and proving our alternative algorithm for building correlating programs, it became apparent that difference representations needed to be better structured: indeed, the original flawed algorithm worked at a very textual level, making it especially difficult to reason about. Instead, we re-interpreted textual differences as differences on the abstract syntax trees of programs, that is, a structured representation of their source code in the form of a tree. This more structured representation of differences made it possible to design our algorithm and prove it correct. While a possible follow-up to this work would have been to move from a static interleaving of two programs to an analysis that would dynamically interleave them, in the manner Partush and Yahav did in the meantime [START_REF] Partush | Abstract Semantic Differencing via Speculative Correlation[END_REF], such an approach would still rely on ad hoc heuristics, and the classes of program differences it would accurately describe would be difficult to characterize. Instead, we decided to pursue the road of more structured, expressive and semantic representations of program changes, that would ideally allow for mechanical verification of any well-specified semantic change.

INTRODUCTION

Towards formal descriptions of program changes

Our approach thus shifted from automatically inferring relational properties between programs to providing programmers with new, more semantic ways of describing their changes. Indeed, programmers already routinely describe their changes in the commit message, but those descriptions are informal and may not actually correspond to the performed modifications. Therefore, the main motivation behind the second part of this thesis is to provide programmers with a formal unambiguous difference language 5to describe program changes. This language would be focused on the semantics of the change, and presented in a more structured way than textual changes.

Writing such a difference language requires a tremendous amount of language design, but first and foremost, it requires a proper formalism for change semantics: how can we associate meaning to a software patch? The majority of this thesis attempts to answer this question by proposing a formal framework to describe changes between two programs-written in arbitrary programming languages. This proposed framework draws inspiration from correlating programs [START_REF] Partush | Abstract Semantic Differencing for Numerical Programs[END_REF] in that the change between two programs is represented by a third program-called correlating oracle-simulating the two others. However, unlike correlating programs, this third program directly embeds the expected semantic relation: from the ground up, it is built to exhibit-or verify-a relation known to the programmer, in contrast to building a correlating program without semantics insight and then trying to recover semantic information from it. In that regard, it is also very similar to the notion of product programs as presented by G. Barthe et al. [START_REF] Barthe | Beyond 2-safety: Asymmetric product programs for relational program verification[END_REF][START_REF] Barthe | Product programs and relational program logics[END_REF], which we will explain in details in Chapter 2.

At their heart, correlating oracles are simply programs simulating two other programs, in such a way that precise properties can be asserted on each related states. In the case of our previous example, if the left program executes in a series of computation steps s 1 l -→ s 2 l -→ s 3 l -→ s 4 l -→ . . . and the right program executes in a series of computation steps s 1 r -→ s 2 r -→ s 3 r -→ s 4 r -→ . . ., then a useful correlating oracle would simulate those two programs in lockstep, asserting that each pair of synchronized states feature equivalent states modulo renaming, that is, that the programs behave exactly the same way, but refer to different variable names:

s 1 l s 2 l s 3 l s 4 l o 1 o 2 o 3 o 4 s 1 r s 2 r s 3 r s 4 r • • • • • • • • •
Using our framework, we have defined specialized oracle languages in which correlating oracles corresponding to some common program changes can be written. Those common program changes include renaming variables, swapping independent assignments, and fixing off-by-one errors causing crashes, amongst others, and will be detailed in Chapter 4.

Those oracle languages can then be put together in a difference language, making use of the aforementioned framework to give formal semantics to change descriptions written by programmers. For instance, the oracle informally described above can be written "rename [y ↔ count]".

A more elaborate example of a difference that can be expressed in such a difference language is the difference between a crashing and a fixed program such as the following pair of programs:

L e f t ( o r i g i n a l ) v e r s i o n s = 0 ; d = x ; w h i l e ( 0 < = d ) { i f ( x % d = = 0 ) s = s + d ; d = d - 1 ; } R i g h t ( m o d i f i e d ) v e r s i o n s = 0 ; d = y ; w h i l e ( 0 < d ) { i f ( y % d = = 0 ) s = s + d ; d = d - 1 ;

}

In the example above, the right program is obtained by renaming x to y in the left program, and changing the condition 0 < = d of line 3 to 0 < d , hence avoiding a division by zero error when evaluating x % d = = 0 with d yields 0. This change can be described in our difference language along the lines of "rename [x ↔ y]; fix off-by-one at line 3".

The actual formal difference description is slightly more complex, as we will see in Chapter 6.

As with the previously-highlighted contribution on correlating programs, this formal framework, along with several examples on a toy imperative programming language, have been formalized in the Coq proof assistant. The expressiveness of this framework has also been proven by encoding several Relational Hoare Logic [START_REF] Benton | Simple Relational Correctness Proofs for Static Analyses and Program Transformations (Revised, Long Version)[END_REF][START_REF] Barthe | Product programs and relational program logics[END_REF] variants presented in the aforementioned paper [START_REF] Barthe | Product programs and relational program logics[END_REF].

Contributions and plan

The main contributions presented in this thesis can be summarized as follows:

1. An example exhibiting that Eran Yahav and Nimrod Partush's [START_REF] Partush | Abstract Semantic Differencing for Numerical Programs[END_REF] correlating program generation algorithm is unsound in the presence of g o t o statements or early loop exit statements such as b r e a k or g o t o . 2. An alternative, formally-proven algorithm addressing the aforementioned issue by handling the difference between two programs as a structured difference between their abstract syntax trees. to describe a dozen different classes of differences on a toy imperative language. Each such oracle language allows writing concise correlating oracles specific to a given class of semantic differences. These oracle languages cover the following set of common changes: renaming variables, changing some values not affecting the programs' control flow, swapping two conditional branches by negating the corresponding condition, refactoring conditionals containing common code, handling reparenthesizing of sequences, commutation of independent assignments, avoiding crashes with defensive conditionals, fixing off-by-one errors inducing crashes, or replacing a sub-program with an equivalent one. 5. An independent proof of some Relational Hoare Logic variants, by encoding them within the aforementioned framework, giving small-step semantics to Relational Hoare Logic proofs. 6. A toy difference language on an idealized imperative programming language, giving a syntax for the previously-defined oracle languages.

The contents of this thesis are presented as follows:

1. Chapter 1 presents our first two contributions: it exhibits the soundness issue found in Partush and Yahav's paper [START_REF] Partush | Abstract Semantic Differencing for Numerical Programs[END_REF] and proposes an alternative, formallyproven algorithm addressing it. 2. Chapter 2 reviews the notions of product programs and Relational Hoare Logic as presented by Barthe et al. [START_REF] Barthe | Product programs and relational program logics[END_REF]. While this chapter contains no new contribution, it lays out definitions that are necessary to the remaining of this thesis while presenting existing work that is a major inspiration for the work described in the following chapters. 3. Chapter 3 presents a novel formal framework for program differences. 4. Chapter 4 defines multiple correlating oracle languages on a small imperative language, exhibiting various capabilities of our framework. 5. Chapter 5 provides new proofs of soundness of several Relational Hoare Logic variants presented in chapter 2 by encoding them in our framework. 6. Chapter 6 presents a toy difference language leveraging from the previouslydefined correlating oracle languages. 7. Chapter 7 presents the Coq library implementing chapters 3 to 6. 8. The conclusion presents the limitations of our approach and discusses alternatives as well as possible future work.

Chapter 1 is essentially an extended version of an article [START_REF] Girka | A Mechanically Checked Generation of Correlating Programs Directed by Structured Syntactic Differences[END_REF] we published previously, while Chapters 3 to 7 are an updated and much more extensive presentation of a work we already presented in another article [START_REF] Girka | Verifiable semantic difference languages[END_REF].

Chapter 1

Correlating Programs

In this chapter, which is essentially an extended version of an article [START_REF] Girka | A Mechanically Checked Generation of Correlating Programs Directed by Structured Syntactic Differences[END_REF] we published previously, we present existing work by Eran Yahav and Nimrod Partush [START_REF] Partush | Abstract Semantic Differencing for Numerical Programs[END_REF], demonstrate why it is flawed, and set out to fix it by proposing an alternative algorithm-formally proved using the Coq proof assistant.

The aforementioned work describes a tool to characterize differences between two programs by performing automatic static analysis on textual differences without requiring additional input from the programmer. This approach can be decomposed in two main components: the first one is a set of program transformations-which are implemented in a tool called c c c -used to build a correlating program; the second, and main component is a static analysis using abstract interpretation [START_REF] Cousot | Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints[END_REF] on this generated correlating program-implemented in a tool called d i z y .

In this chapter, we focus on the main component, that is the algorithm for generating correlating programs. A correlating program is a program tightly interleaving the instructions of two other programs in such a way that it correctly simulates some parallel execution of those two programs. The particular way the instructions are interleaved follows an heuristic aimed at increasing the likelihood of factorizing the two program's execution paths, keeping supposedly related instructions close to increase the precision of further analysis. This interleaving effectively defines a static scheduling of the two programs' parallel execution.

Yahav and Partush's original correlating program generation algorithm works in two steps: the first step is to transform each of the two programs to be compared to an equivalent guarded form in which every code block is broken into atomic statements, each of which is prefixed by a guard condition encoding the code path leading to the code block it was in. The second step is to actually interleave those guarded instructions in a common correlating program. The order in which those instructions are interleaved follows a textual diff on a "cleaned-up" version of the guarded forms, as we will explain more precisely.

To illustrate those steps, let us consider the following pair of C programs which differ by a moved line:

L e f t ( o r i g i n a l ) v e r s i o n v o i d f ( i n t a , i n t b ) { i f ( a < b ) { a = a + 1 0 ; / / m o v e d l i n e b = b - 1 0 ; } e l s e { b = b + 1 ; } } R i g h t ( m o d i f i e d ) v e r s i o n v o i d f ( i n t a , i n t b ) { i f ( a < b ) { b = b - 1 0 ; } e l s e { a = a + 1 0 ; / / m o v e d l i n e b = b + 1 ; } }
First, both of those programs are transformed to semantically-equivalent guarded forms where every imperative command is guarded by a set of guard variables encoding the control flow:

L e f t v e r s i o n ( g u a r d e d ) v o i d f ( i n t a , i n t b ) { G u a r d G 0 = ( a < b ) ; i f ( G 0 ) a = a + 1 0 ; / / m o v e d l i n e i f ( G 0 ) b = b - 1 0 ; i f ( ! G 0 ) b = b + 1 ; } R i g h t v e r s i o n ( g u a r d e d ) v o i d f ( i n t a , i n t b ) { G u a r d G 0 = ( a < b ) ; i f ( G 0 ) b = b - 1 0 ; i f ( ! G 0 ) a = a + 1 0 ; / / m o v e d l i n e i f ( ! G 0 ) b = b + 1 ;
} Then, a vector of "imperative commands" is extracted from each program in order to perform the diff operation that will drive the interleaving of the two guarded forms above. Those "imperative commands" are the actual variable assignments and g o t o statements, without any reference to the guard variables. In the case of this example, the left and right imperative commands are the following: A diff is then performed on those two vectors of "imperative commands" to determine the order in which to insert each guarded form's instructions into the correlating program. The diff consists in annotating lines of both "imperative command" vectors with ''-" for lines present in the first program but not the second, "+" for lines present in the second but not the first, and "=" for lines present in both: This diff is used to determine how to interleave instructions from both guarded programs, and tagging instructions from the second program to avoid collisions, leading to the final correlating program:

C o r r e l a t i n g p r o g r a m

v o i d f ( i n t a , i n t b ) { i n t T _ a = a ; i n t T _ b = b ; G u a r d G 0 = ( a < b ) ; / / i f c o n d i t i o n ( O r i g i n a l v e r s i o n ) G u a r d T _ G 0 = ( T _ a < T _ b ) ; / / i f c o n d i t i o n ( M o d i f i e d v e r s i o n ) i f ( G 0 ) a = a + 1 0 ; / / t h e n b r a n c h ( O r i g i n a l v e r s i o n ) i f ( G 0 ) b = b - 1 0 ; / / t h e n b r a n c h ( O r i g i n a l v e r s i o n ) i f ( T _ G 0 ) T _ b = T _ b - 1 0 ; / / t h e n b r a n c h ( M o d i f i e d v e r s i o n ) i f ( ! T _ G 0 ) T _ a = T _ a + 1 0 ; / / e l s e b r a n c h ( M o d i f i e d v e r s i o n ) i f ( ! G 0 ) b = b + 1 ; / / e l s e b r a n c h ( O r i g i n a l v e r s i o n ) i f ( ! T _ G 0 ) T _ b = T _ b + 1 ; / / e l s e b r a n c h ( M o d i f i e d v e r s i o n ) } 1.

Unsound handling of g o t o statements

In their original paper, Yahav and Partush claim to generate correlating programs for any pair of C programs, using the text-based algorithm presented above, as implemented in the tool "c c c ". Unfortunately, we quickly found a bug in the way "g o t o " statements were handled, which made some generated correlating programs unsound, failing to simulate one or both of the programs under consideration. Due to how their tool translates loops into "g o t o " statements, this issue also affects loops constructions with early exit.

Example 1. Indeed, consider the following pair of programs (P 1 , P 2 ), which differ by the inclusion of a "b r e a k " statement in P 2 (on the right), causing the loop to be iterated at most once in P 2 :

L e f t p r o g r a m v o i d f a i l ( i n t x ) { i = 0 ; w h i l e ( i < = 1 ) { i = i + 1 ; x = x + 1 ; } } R i g h t p r o g r a m v o i d f a i l ( i n t x ) { i = 0 ; w h i l e ( i < = 1 ) { i = i + 1 ; x = x +
v o i d f a i l ( i n t x ) { i n t T _ x = x ; i n t i = 0 ; i n t T _ i = 0 ; L 1 : T _ L 1 : ; G u a r d G 0 = ( i < = 1 ) ; G u a r d T _ G 0 = ( T _ i < = 1 ) ; i f ( G 0 ) i = i + 1 ; i f ( T _ G 0 ) T _ i = T _ i + 1 ; i f ( G 0 ) x = x + 1 ; i f ( T _ G 0 ) T _ x = T _ x + 1 ; i f ( T _ G 0 ) g o t o T _ L 3 ; i f ( G 0 ) g o t o L 1 ; i f ( T _ G 0 ) g o t o T _ L 1 ; L 3 : T _ L 3 :

}

As one can see, c c c translates w h i l e -loops by defining guard variables holding the result of evaluating the loops' condition (lines 6 and 7), guarding the loops' body and inserting g o t o statements (lines 15 and 16) to recover the looping behavior. This translation enables close interleaving of the two programs' instructions within the loop.

Early exit constructs such as b r e a k are translated to additional g o t o statements (line 13). While this is fine in a single-program setting, this makes interleaving the two programs unsound. Indeed, this incorrect correlating program will return as soon as the g o t o statement on line 13 is executed, incorrectly skipping the instructions corresponding to the original program, which is supposed to run one additional iteration of the loop.

In our opinion, Partush and Yahav's approach is conceptually flawed because their generation algorithm is directed by a line-by-line textual difference between the two programs. This textual representation is not structured well enough to correctly perform a static scheduling of the two programs instructions. In addition, such program transformations can prove quite challenging to get right, and the insufficiently formal description of the algorithm makes reasoning about them significantly harder.

Indeed, such program transformations are disconcertingly easy to get wrong, with issues creeping in every forgotten corner case. This is why we believe such program transformations should be formally proved correct. That is what we did by writing an alternative generating algorithm for correlating program and by formally proving it using the Coq proof assistant. This alternative algorithm is directed by a structured difference between abstract syntax trees of the two programs rather than by a textual difference, which makes that algorithm significantly easier to formalize and prove correct.

Formal definition of the Imp br language

Admittedly, going for a formally proven approach leads to some compromises: indeed, we have significantly restricted the scope of our generating algorithm to a small imperative language that roughly corresponds to a subset of the C programming language. This source language "Imp br " is a minimalist imperative language commonly used in computer science lectures, featuring assignments, conditionals and "while" loops, extended with early exit constructs "b r e a k " and "c o n t i n u e ".

Syntax of Imp br

We write x for a variable identifier taken in an enumerable set of identifiers I, n for an integer value taken in Z, and b for a boolean value in true, false. Expressions are simple arithmetic expressions, and commands feature the standard assignments, while-loops and if-statemnts, as well as the non-local control-flow operators break and continue.

Semantics of Imp br

The Imp br language enjoys a standard big-step semantics: a program transforms the store by means of commands and commands make use of pure expressions to perform arithmetic and boolean computations.

A store S : I → Z is a partial map from variable identifiers to integer values. The empty store is written ∅, ∀ x ∈ dom(S) quantifies over the finite domain of the store S, and S[x ↦ → n] is the store defined on dom(S) ∪ {x} such that S[x ↦ → n](y) = n if x = y and S(y) otherwise.

The judgment "S ⊢ e ⇓ n" reads "In the store S, the arithmetic expression e evaluates into the integer n" and the judgment "S ⊢ b ⇓ b" reads "In the store S, the boolean expression b evaluates into the boolean b".

Expressions semantics

Cst S ⊢ n ⇓ n Var S ⊢ x ⇓ S(x) Sum S ⊢ e 1 ⇓ n 1 S ⊢ e 2 ⇓ n 2 S ⊢ e 1 + e 2 ⇓ n 1 + Z n 2

Boolean expressions semantics

Cst S ⊢ b ⇓ b Not S ⊢ b ⇓ b S ⊢!b ⇓ ¬b And S ⊢ b 1 ⇓ b 1 S ⊢ b 2 ⇓ b 2 S ⊢ b 1 && b 2 ⇓ b 1 ∧ b 2 LessOrEqual S ⊢ e 1 ⇓ n 1 S ⊢ e 2 ⇓ n 2 S ⊢ e 1 ≤ e 2 ⇓ n 1 ≤ Z n 2
The interpretation of a command yields a return mode which is either normal (written □), interrupted (written ⋆, used to handle break statements) or continuing (written •, used to handle continue statements). The judgment "S 0 ⊢ c ⇓ m S 1 " reads "The command c transforms the store S 0 into S 1 in mode m".

Commands semantics

Skip S ⊢ skip ⇓ □ S Assign S ⊢ e ⇓ n S ⊢ x = e ⇓ □ S[x ↦ → n] Seq S ⊢ c 1 ⇓ □ S ′ S ′ ⊢ c 2 ⇓ m S ′′ S ⊢ c 1 ; c 2 ⇓ m S ′′ Seq Interrupted S ⊢ c 1 ⇓ m S ′ m ̸ = □ S ⊢ c 1 ; c 2 ⇓ m S ′ Then S ⊢ b ⇓ true S ⊢ c 1 ⇓ m S ′ S ⊢ if (b) c 1 else c 2 ⇓ m S ′ Else S ⊢ b ⇓ false S ⊢ c 2 ⇓ m S ′ S ⊢ if (b) c 1 else c 2 ⇓ m S ′ While False S ⊢ b ⇓ false S ⊢ while (b) c ⇓ □ S While True S ⊢ b ⇓ true S ⊢ c ⇓ m S ′ S ′ ⊢ while (b) c ⇓ □ S ′′ m ̸ = ⋆ S ⊢ while (b) c ⇓ □ S ′′ While Break S ⊢ b ⇓ true S ⊢ c ⇓ ⋆ S ′ S ⊢ while (b) c ⇓ □ S ′ Break S ⊢ break ⇓ ⋆ S Continue S ⊢ continue ⇓ • S

Formal definition of the Guarded Language

As mentioned earlier, Yahav and Partush's approach to generating correlating programs is to first transform each program into a corresponding guarded form, then interleaving the instructions of both guarded programs into a single correlating program. As we loosely follow Yahav and Partush's approach to keep compatibility with their further static analysis step, we also have to guard statements accordingly. Therefore, we have decided to formally define a guarded language derived from our input language, thus syntactically enforcing the use of a guarded form.

Every condition of the Guarded Language is stored into a boolean variable called a guard variable and every atomic instruction is guarded by a conjunction of guard variables (called a guard thereafter). This specific form effectively abstracts execution paths into guard variables, as the values of the guard variables uniquely determine a single block in the control flow graph of the input program. Thus, assigning specific values to these guard variables activates specific instructions of the input program. In Section 1.6, this mechanism will be at the heart of the static interleaving of programs instructions.

Syntax

In order to simplify the formal proof of some technical lemmas, guard variable identifiers are taken in the set G of words over the alphabet {0, 1}. We will later make use of the fact that a word in this alphabet can encode a path in an Imp abstract syntax tree. We write g for such guard identifiers.

The syntax of the guarded language includes assignment statements ac G guarded by a conjunction of (positive or negative) guard variables and a while-loop statement guarded by a disjunction of guard conjunctions. Notice that break and continue are not present in the guarded language: indeed, as we will see later, such statements can be encoded using additional guard variables.

c G ::= c G ; c G | skip | while ( ⃗ g ∨ ) c G | while (b) c | if ( ⃗ g ∧ ) ac G (Commands) ac G ::= x = e | g = b (Atomic commands) ⃗ g ∨ ::= ⊥ | ⃗ g ∧ ∨ ⃗ g ∨ (Guard disjunctions) ⃗ g ∧ ::= ⊤ | g l ∧ ⃗ g ∧ (Guard conjunctions) g l ::= g | ¬g (Guard literals) g ∈ {0, 1} * (Guard variables)

Semantics

Besides the store S of integer variables, a program written in the guarded language also transforms a guard store G of guard variables, which is a partial map G : G → b from guard identifiers to boolean values. The operations over standard stores are naturally transported to guard stores.

The judgment "S 0 , G 0 ⊢ c G ⇓ S 1 , G 1 " reads "The guarded command c G transforms the store S 0 and the guard store G 0 into a new store S 1 and a new guard store G 1 ". The rules for the evaluation of guards and disjunctions of guards are straightforward and thus omitted.

Skip S, G ⊢ skip ⇓ S, G Seq S, G ⊢ c G1 ⇓ S ′ , G ′ S ′ , G ′ ⊢ c G2 ⇓ S ′′ , G ′′ S, G ⊢ c G1 ; c G2 ⇓ S ′′ , G ′′ Ignore G ⊢ ⃗ g ∧ ⇓ false S, G ⊢ if ( ⃗ g ∧ ) ac G ⇓ S, G Activate G ⊢ ⃗ g ∧ ⇓ true S, G ⊢ ac G ⇓ S ′ , G ′ S, G ⊢ if ( ⃗ g ∧ ) ac G ⇓ S ′ , G ′ GAssignment S ⊢ b ⇓ b S, G ⊢ g = b ⇓ S, G[g ↦ → b] Assignment S ⊢ e ⇓ n S, G ⊢ x = e ⇓ S[x ↦ → n], G While False G ⊢ ⃗ g ∨ ⇓ false S, G ⊢ while ( ⃗ g ∨ ) c G ⇓ S, G While True G ⊢ ⃗ g ∨ ⇓ true S, G ⊢ c G ⇓ S ′ , G ′ S ′ , G ′ ⊢ while ( ⃗ g ∨ ) c G ⇓ S ′′ , G ′′ S, G ⊢ while ( ⃗ g ∨ ) c G ⇓ S ′′ , G ′′

Translation to guarded form

While our algorithm, unlike Yahav and Partush's, is not split in two distinct steps and directly builds a correlating program from a structured difference as we will see later, the proof of correctness relies on the correct transformation of individual programs into equivalent guarded forms. We define the translation into guarded forms by using a recursive translation function CI defined as follows: • An assignment x = e is an effectful statement that has to be guarded appropriately. In this case, the appropriate guards are simply those accumulated in the ⃗ g ∧ parameter.

c o CI( ⃗ g ∧ , π, c, o) skip o skip x = e o if ( ⃗ g ∧ ) x = e c 1 ; c 2 o CI( ⃗ g ∧ , 0 • π, c 1 , o); CI( ⃗ g ∧ , 1 • π, c 2 , o) if (b) c 1 else c 2 o if ( ⃗ g ∧ ) π = b; CI( ⃗ g ∧ ∧ π, 1 • π, c 1 , o); CI( ⃗ g ∧ ∧ ¬π, 0 • π, c 2 , o) while (b) c o if ( ⃗ g ∧ ) π = b; while ( ⃗ g ∧ ∧ π) { if ( ⃗ g ∧ ∧ π) 1 • π = true; CI( ⃗ g ∧ ∧ π ∧ (1 • π), 1 • 1 • π, c, Some π); if ( ⃗ g ∧ ∧ π) π = b } break Some π ′ if ( ⃗ g ∧ ) π ′ = false continue Some π ′ if ( ⃗ g ∧ ) 1 • π ′ = false CI( ⃗ g ∧ , π, c,
• The case of a sequence c 1 ; c 2 is purely recursive. Since a sequence does not introduce any condition, the same guard list ⃗ g ∧ is passed for both recursive calls. The reasoning is the same for the loop marker: a sequence does not change the loop structure, each of the two subcommands are in the same inner loop (if any) as the sequence c 1 ; c 2 , thus o is passed as-is. However, we have to keep track of the path of each subcommand in the larger program, which is why CI is called with 0 • π in one case and 1 • π in the other. • In the case where c is "if (b) c 1 else c 2 ", we first create a fresh guard name "π" to which we conditionally assign the value of b under the guard conjunction ⃗ g ∧ : "if ( ⃗ g ∧ ) π = b". This guard represents the condition used to select either the "then" or "else" branch of the if statement. We then recursively call CI on c 1 (the "then" branch), guarded by the conjunction of the previous guards and the newly created one ( ⃗ g ∧ ∧ π). We do the same for c 2 (the "else" branch), negating the guard π ( ⃗ g ∧ ∧ ¬π). As for the sequence, we keep track of the path of each subcommand with 0 • π and 1 • π.

• The case of a loop while (b) c is the most involved: it is recursive because it has a subcommand under a new path, and it introduces new guards and a new inner loop for this subcommand. Just as in the case of if statements, a new guard π is created and conditionally set to the conditional expression b by the guarded assignment "if ( ⃗ g ∧ ) π = b". This new guard π represents the loop condition and will guard the whole translated loop. However, yet another new guard 1 • π is created and set to true ("if ( ⃗ g ∧ ∧ π) 1 • π = true") to guard the translated body of the loop, while an additional assignment is added at the end of the loop's body to re-evaluate the loop condition. The purpose of the 1 • π guard is to encode continue statements. • A break statement can only occur inside a loop, and its effect is to break out of the innermost one. Since this subcommand is inside a loop, the loop marker is set to Some π ′ for some π ′ , which is, by construction, a guard variable guarding the whole loop. Therefore, setting this guard variable to false will effectively disabling further execution of the loop's instructions. • A continue statement is handled in a way similar to break: the loop marker Some π ′ lets us set the guard variable 1 • π ′ to false, thus disabling the execution of the loop's body for this iteration, at the end of which the guard condition will be re-evaluated.

The soundness of CI is stated by the following technical lemma. Roughly speaking, this lemma states that CI( ⃗ g ∧ , π, c, o) simulates c correctly under a guard store G if the following assumptions are met:

• The guard conjunction ⃗ g ∧ is active (G ⊢ ⃗ g ∧ ⇓ true). • If the execution mode yielded by the execution of c is not □, then c can only be contained in a wider program involving a loop, for which o contains the guard variable.

• If o = π ′ for some π ′ , then both π ′ and 0 • π ′ appear in ⃗ g ∧ . • Every guard variable of ⃗ g ∧ is independent with regards to π so that all guard variables created by CI will effectively be fresh.

Lemma 1 (CI is sound on active guards). For all stores S and S ′ , a guard store G, return mode m, guard conjunction ⃗ g ∧ , command c, path π and optional loop marker o, if the following statements hold:

i. S ⊢ c ⇓ m S ′ ii. G ⊢ ⃗ g ∧ ⇓ true iii. m ̸ = □ =⇒ ∃ π l , o = Some π l iv. ∀ π l , o = Some π l =⇒ G(π l ) = G(1 • π l ) = true v. ∀ g, g#π
then, there exists a store G ′ such that the following statements hold:

a. S, G ⊢ CI( ⃗ g ∧ , π, c, o) ⇓ S ′ , G ′ b. ∀ g ∈ dom(G), g#π =⇒ G(g) = G ′ (g) c. m = ⋆ =⇒ ∃π l , o = Some π l ∧ G ′ (π l ) = false d. m = • =⇒ ∃π l , o = Some π l ∧ G ′ (1 • π l ) = false
Proof. The proof is done by structural induction on S ⊢ c ⇓ m S ′ .

Structured program differences

As noted earlier, our approach does not directly work on textual differences, but rather on structured syntactic differences-which can be provided by the developer or computed automatically.

Such a syntactic difference between the abstract syntax trees of two syntactically correct programs is denoted by a special representation of the whole programs. This representation will be processed in a purely recursive way by the algorithm that generates the correlating program.

Syntax

The structured difference language is derived from the input language, in such a way that each internal node of the abstract syntax tree is associated with a local mutation ∆ (where ± ::= -| +):

∆ ::= a → a ′ | ±[c]; ∆ | ±∆; [c] | ∆; ∆ | if (b → b ′ ) ∆ else ∆ | while (b → b ′ ) ∆ | ±[if (b) c else] ∆ | ±[if (b)] ∆ [else c] | ±[while (b)] ∆
A structured difference represents the full original program along with differences leading to the modified program.

Informally, the notation "a → a ′ " means that the leaf command a of the original program is replaced by the leaf command a ′ in the modified program.

Likewise, the notation "±[c]; ∆" means that the command c is removed from the orginal program ("-[c]; ∆") or inserted into the modified program ("+[c]; ∆") while the right side is kept with a local mutation ∆. The notation "±∆; [c]" is symmetrical. The notation "∆; ∆ ′ " means that the both programs are sequences, with the left side of the sequence described by the local mutation ∆ while the right side is described by ∆ ′ .

Similarly, "+[if (b) c else] ∆" means that an if" statement is inserted in the modified program with the command c as its then branch and using existing code (with local mutation ∆) as its else branch.

The other constructs follow the same pattern, and a more formal meaning is given by the projection functions Π 0 () and Π 1 () which return the original and modified embedded programs respectively:

∆ Π0(∆) Π1(∆) -[c1]; ∆2 c1; Π0(∆2) Π1(∆2) -∆1; [c2] Π0(∆1); c2 Π1(∆1) +[c1]; ∆2 Π0(∆2) c1; Π1(∆2) +∆1; [c2] Π0(∆1) Π1(∆1); c2 ∆1; ∆2 Π0(∆1); Π0(∆2) Π1(∆1); Π1(∆2) if (b → b ′ ) ∆1 else ∆2 if (b) Π0(∆1) else Π1(∆2) if (b ′ ) Π0(∆2) else Π1(∆2) while (b → b ′ ) ∆ ′ while (b) Π0(∆ ′ ) while (b ′ ) Π1(∆ ′ ) +[if (b) c1 else] ∆2 Π0(∆2) if (b) c1 else Π1(∆2) +[if (b)] ∆1 [else c2] Π0(∆1) if (b) Π1(∆1) else c2 -[if (b) c1 else] ∆2 if (b) c1 else Π0(∆2) Π1(∆2) -[if (b)] ∆1 [else c2] if (b) Π0(∆1) else c2 Π1(∆1) +[while (b)] ∆ ′ Π0(∆ ′ ) while (b) Π1(∆ ′ ) -[while (b)] ∆ ′ while (b) Π0(∆ ′ ) Π1(∆ ′ ) a → a ′ a a ′
As stated by the following theorem, a difference between any two programs can always be found.

Theorem 1 (Completeness of the diff. language). For all pairs of programs (c, c ′ ), there exists a difference ∆ such that Π 0 (∆) = c and Π 1 (∆) = c ′ .

Proof. As we are only interested in the existence of a difference between every pair of programs, and not in any measure of conciseness or quality of that difference, we define a recursive total function ∆ naive for computing differences. Informally, that function builds a diff that "removes" every construct of the left program and relies on a second recursive total function ∆ + naive to "add" the second program:

∆ + naive (a, a ′ ) = a → a ′ ∆ + naive (a, c 1 ; c 2 ) = +∆ + naive (a, c 1 ); [c 2 ] ∆ + naive (a, while (b) c) = +[while (b)] ∆ + naive (a, c) ∆ + naive (a, if (b) c 1 else c 2 ) = +[if (b) c 1 else] ∆ + naive (a, c 1 ) ∆ naive (a, c) = ∆ + naive (a, c) ∆ naive (c 1 ; c 2 , c ′ ) = -∆ naive (c 1 , c ′ ); [c 2 ] ∆ naive (while (b) c, c ′ ) = -[while (b)] ∆ naive (c, c ′ ) ∆ naive (if (b) c 1 else c 2 , c ′ ) = -[if (b)] ∆ naive (c 1 , c ′ ) [else c 2 ]
That function is proved to produce correct differences, by induction on the structure of the left program. The base case of a leaf command as the left program is proved correct by induction on the right program.

Generation algorithm directed by structured differences

As instructions from both programs will be interleaved in a single program, variable identifiers of both programs have to be differentiated. To keep things simple and compatible with the "d i z y " abstract interpertation tool, we adopt the following convention: variable identifiers of the original (left) program start with "O_", while variable identifiers of the modified (right) program start with "T _O_". Definition 2 (Difference tagging). Difference tagging, denoted (∆) T,T ′ , is defined as follows:

(-[c 1 ]; ∆ 2 ) T,T ′ = -[T (c 1 )]; (∆ 2 ) T,T ′ (-∆ 1 ; [c 2 ]) T,T ′ = -(∆ 1 ) T,T ′ ; [T (c 2 )] (+[c 1 ]; ∆ 2 ) T,T ′ = +[T ′ (c 1 )]; (∆ 2 ) T,T ′ (+∆ 1 ; [c 2 ]) T,T ′ = +(∆ 1 ) T,T ′ ; [T ′ (c 2 )] (∆ 1 ; ∆ 2 ) T,T ′ = (∆ 1 ) T,T ′ ; (∆ 2 ) T,T ′ (if (b → b ′ ) ∆ 1 else ∆ 2 ) T,T ′ = if (T (b) → T ′ (b ′ )) (∆ 1 ) T,T ′ else (∆ 2 ) T,T ′ (while (b → b ′ ) ∆ ′ ) T,T ′ = while (T (b) → T ′ (b ′ )) (∆ ′ ) T,T ′ (+[if (b) c 1 else] ∆ 2 ) T,T ′ = +[if (T ′ (b)) T ′ (c 1 ) else] (∆ 2 ) T,T ′ (+[if (b)] ∆ 1 [else c 2 ]) T,T ′ = +[if (T ′ (b))] (∆ 1 ) T,T ′ [else T ′ (c 2 )] (-[if (b) c 1 else] ∆ 2 ) T,T ′ = -[if (T (b)) T (c 1 ) else] (∆ 2 ) T,T ′ (-[if (b)] ∆ 1 [else c 2 ]) T,T ′ = -[if (T (b))] (∆ 1 ) T,T ′ [else T (c 2 )] (+[while (b)] ∆ ′ ) T,T ′ = +[while (T ′ (b))] (∆ ′ ) T,T ′ (-[while (b)] ∆ ′ ) T,T ′ = -[while (T (b))] (∆ ′ ) T,T ′ (a → a ′ ) T,T ′ = T (a) → T ′ (a ′ )
We define a correlating program generation algorithm directed by structured differences as a recursive function CP , which works much like CI, but handling both left and right programs at the same time by following structured differences. The program

CP (∆, π 0 , π 1 , ⃗ g ∧0 , ⃗ g ∧1 , o 0 , o 1
) is a correlating program of Π 0 (∆) and Π 1 (∆), corresponding to an interleaving of the guarded forms CI( ⃗ g ∧0 , π 0 , Π 0 (∆), o 0 ) and CI( ⃗ g ∧1 , π 1 , Π 1 (∆), o 1 ). The paths π 0 and π 1 are the position of Π 0 (∆) and Π 1 (∆) in the larger correlating program. Just as with CI, they are used as fresh names for new guard variables, which also eases Coq proofs by encoding path information in the name of the guards. ⃗ g ∧0 and ⃗ g ∧1 are the guard conjunctions guarding Π 0 (∆) and Π 1 (∆) in the whole correlating program, while o 0 and o 1 represent the innermost loop (if any) under which Π 0 (∆) and Π 1 (∆) are executed, and are used to translate break and continue statements.

One key reason for using structured syntactic differences is that they are wellsuited for factoring the control structures of both programs. Indeed, under the assumption that the control structure of the modified program is kept unchanged, then it is possible to represent the difference as a structured syntactic difference having the same structure itself. By being directed by such a structured syntactic difference, the correlating program generation algorithm can closely interleave instructions that are likely to be executed under the same conditions.

∆ CP (∆, π 0 , π 1 , ⃗ g ∧0 , ⃗ g ∧1 , o 0 , o 1 ) -[c]; ∆ CI( ⃗ g ∧0 , 0 • π 0 , c, o 0 ); CP (∆, 1 • π 0 , π 1 , ⃗ g ∧0 , ⃗ g ∧1 , o 0 , o 1 ) -∆; [c] CP (∆, 0 • π 0 , π 1 , ⃗ g ∧0 , ⃗ g ∧1 , o 0 , o 1 ); CI( ⃗ g ∧0 , 1 • π 0 , c, o 0 ) +[c]; ∆ CI( ⃗ g ∧1 , 0 • π 1 , c, o 1 ); CP (∆, π 0 , 1 • π 1 , ⃗ g ∧0 , ⃗ g ∧1 , o 0 , o 1 ) +∆; [c] CP (∆, π 0 , 0 • π 1 , ⃗ g ∧0 , ⃗ g ∧1 , o 0 , o 1 ); CI( ⃗ g ∧1 , 1 • π 1 , c, o 1 ) ∆ 0 ; ∆ 1 CP (∆ 0 , 0 • π 0 , 0 • π 1 , ⃗ g ∧0 , ⃗ g ∧1 , o 0 , o 1 ) CP (∆ 1 , 1 • π 0 , 1 • π 1 , ⃗ g ∧0 , ⃗ g ∧1 , o 0 , o 1 ) if (b 0 → b 1 ) ∆ 0 else ∆ 1 if ( ⃗ g ∧0 ) π 0 = b 0 ; if ( ⃗ g ∧1 ) π 1 = b 1 ; CP (∆ 0 , 1 • π 0 , 1 • π 1 , ⃗ g ∧0 ∧ π 0 , ⃗ g ∧1 ∧ π 1 , o 0 , o 1 ); CP (∆ 1 , 0 • π 0 , 0 • π 1 , ⃗ g ∧0 ∧ ¬π 0 , ⃗ g ∧1 ∧ ¬π 1 , o 0 , o 1 ) while (b 0 → b 1 ) ∆ if ( ⃗ g ∧0 ) π 0 = b 0 ; if ( ⃗ g ∧1 ) π 1 = b 1 ; while (( ⃗ g ∧0 ∧ π 0 ) ∨ ( ⃗ g ∧1 ∧ π 1 )) { if ( ⃗ g ∧0 ∧ π 0 ) 1 • π 0 = true; if ( ⃗ g ∧1 ∧ π 1 ) 1 • π 1 = true; CP (∆, 1 • 1 • π 0 , 1 • 1 • π 1 , ⃗ g ∧0 ∧ π 0 ∧ (1 • π 0 ), ⃗ g ∧1 ∧ π 1 ∧ (1 • π 1 ), Some π 0 , Some π 1 ); if ( ⃗ g ∧0 ∧ π 0 ) π 0 = b 0 ; if ( ⃗ g ∧1 ∧ π 1 ) π 1 = b 1 ; } c G0 → c G1 CI( ⃗ g ∧0 , π 0 , c G0 , o 0 ); CI( ⃗ g ∧1 , π 1 , c G1 , o 1 ) -[if (b) c else] ∆ if ( ⃗ g ∧0 ) π 0 = b; CI( ⃗ g ∧0 ∧ π 0 , 1 • π 0 , c, o 0 ); CP (∆, 0 • π 0 , π 1 , ⃗ g ∧0 ∧ ¬π 0 , ⃗ g ∧1 , o 0 , o 1 ) +[if (b) c else] ∆ if ( ⃗ g ∧1 ) π 1 = b; CI( ⃗ g ∧1 ∧ π 1 , 1 • π 1 , c, o 1 ); CP (∆, π 0 , 0 • π 1 , ⃗ g ∧0 , ⃗ g ∧1 ∧ ¬π 1 , o 0 , o 1 ) -[if (b)] ∆ [else c] if ( ⃗ g ∧0 ) π 0 = b; CP (∆, 1 • π 0 , π 1 , ⃗ g ∧0 ∧ π 0 , ⃗ g ∧1 , o 0 , o 1 ); CI( ⃗ g ∧0 ∧ ¬π 0 , 0 • π 0 , c, o 0 ) +[if (b)] ∆ [else c] if ( ⃗ g ∧1 ) π 1 = b; CP (∆, π 0 , 1 • π 1 , ⃗ g ∧0 , ⃗ g ∧1 ∧ π 1 , o 0 , o 1 ); CI( ⃗ g ∧1 ∧ ¬π 1 , 0 • π 1 , c, o 1 ) Figure 1.1: Difference-directed correlating program generation function CP ∆ CP (∆, π 0 , π 1 , ⃗ g ∧0 , ⃗ g ∧1 , o 0 , o 1 ) -[while (b)] ∆ if ( ⃗ g ∧0 ) π 0 = b; if ( ⃗ g ∧0 ∧ π 0 ) 1 • π 0 = true; CP (∆, 1 • 1 • π 0 , π 1 , ⃗ g ∧0 ∧ π 0 ∧ (1 • π 0 ), ⃗ g ∧1 , Some π 0 , o 1 ); if ( ⃗ g ∧0 ∧ π 0 ) π 0 = b; while ( ⃗ g ∧0 ∧ π 0 ) { if ( ⃗ g ∧0 ∧ π 0 ) 1 • π 0 = true; CI( ⃗ g ∧0 ∧ π 0 ∧ (1 • π 0 ), 1 • 1 • π 0 , Π 0 (∆), Some π 0 ); if ( ⃗ g ∧0 ∧ π 0 ) π 0 = b; } +[while (b)] ∆ if ( ⃗ g ∧1 ) π 1 = b; if ( ⃗ g ∧1 ∧ π 1 ) 1 • π 1 = true; CP (∆, π 0 , 1 • 1 • π 1 , ⃗ g ∧0 , ⃗ g ∧1 ∧ π 1 ∧ (1 • π 1 ), o 0 , Some π 1 ); if ( ⃗ g ∧1 ∧ π 1 ) π 1 = b; while ( ⃗ g ∧1 ∧ π 1 ) { if ( ⃗ g ∧1 ∧ π 1 ) 1 • π 1 = true; CI( ⃗ g ∧1 ∧ π 1 ∧ (1 • π 1 ), 1 • 1 • π 1 , Π 1 (∆), Some π 1 ); if ( ⃗ g ∧1 ∧ π 1 ) π 1 = b; } Figure 1.1: Difference-directed correlating program generation function CP (cont.)
Overall, the definition of CP (Figure 1.1) is very similar to that of CI-and in fact often calls CI-but has to handle many more cases due to the nature of structured differences.

For example, consider the definition for -[if (b) c else] ∆ corresponding to the removal of an if statement and its "then" part while keeping its "else" part. We first create a new guard π 0 to which we conditionally assign the value b under the conjunction ⃗ g ∧0 of the original program ("if ( ⃗ g ∧0 ) π 0 = b") because the if statement is only executed in the first program. We then call CI to output the guarded form of the statement c under the removed "then" part: "CI( ⃗ g ∧0 ∧ π 0 , 1 • π 0 , c, o 0 )". This will be conditionally executed under the conjunction of ⃗ g ∧0 and the new guard π 0 , under a new unique path "1 • π 0 ". We then continue the translation of the remaining structured difference ∆ by recursively calling CP on it: "CP (∆, 0

• π 0 , π 1 , ⃗ g ∧0 ∧ ¬π 0 , ⃗ g ∧1 , o 0 , o 1 )".
For the original program, we create a new unique path "0 • π 0 ". This part is guarded by " ⃗ g ∧0 ∧ ¬π 0 " as it is executed under the "else" part of the original program. For the modified program, we keep the guard ⃗ g ∧1 and the path π 1 which is still unique. o 0 and o 1 are reused unmodified as we are not translating a loop.

Example 2. The result of calling CP on the pair of programs from Example 1 is the following correlating program (printed as C code):

C o r r e l a t i n g p r o g r a m

v o i d f a i l ( i n t O _ x ) { i n t T _ O _ x = O _ x ; i n t O _ i = 0 ; i n t T _ O _ i = 0 ; G u a r d G 1 = 1 ; G u a r d T _ G 1 = 1 ; G u a r d G 0 = ( O _ i < = 1 ) ; G u a r d T _ G 0 = ( T _ O _ i < = 1 )
;

w h i l e ( G 0 | | T _ G 0 ) { i f ( G 0 ) G 1 = 1 ; / / u n

u s e d h e r e ( o t h e r w i s e

i f ( T _ G 0 ) T _ G 1 = 1 ; / / u s e d t o e n c o d e " c o n t i n u e " ) i f ( G 0 ) i f ( G 1 ) O _ i = O _ i + 1 ; i f ( T _ G 0 ) i f ( T _ G 1 ) T _ O _ i = T _ O _ i + 1 ; i f ( G 0 ) i f ( G 1 ) O _ x = O _ x + 1 ; i f ( T _ G 0 ) i f ( T _ G 1 ) T _ O _ x = T _ O _ x + 1 ; i f ( T _ G 0 ) i f ( T _ G 1 ) T _ G 0 = 0 ; / / e n c o d e s " b r e a k " i f ( G 0 ) G 0 = ( O _ i < = 1 ) ; / / u p d a t e l e f t l o o p ' s c o n d i t i o n i f ( T _ G 0 ) T _ G 0 = ( T _ O _ i < = 1 ) ; / / u p d a t e r i g h t l o o p ' s c o n d i t i o n } }
Even though correlating programs include instructions from two different programs, manipulating two sets of variables, they execute in a single store. Thanks to tagging, those variables are independent, and the store of a correlating program can be split into two stores corresponding to each of the two programs under comparison. The same can be said about guard stores. Definition 3 (Store splitting). Two stores S 0 and S 1 are said to split a store S if ∀ n ∈ {0, 1}, ∀ x ∈ dom(S n ), S(x) = S n (x); and S 0 contains only variables starting with "O_", and S 1 with "T _O_". Definition 4 (Guard store splitting). Two guard stores G 0 and G 1 are said to split a guard store

G if ∀ n ∈ {0, 1}, ∀ x ∈ dom(G n ), G(x) = G n (x)
; and G 0 contains only variables ending with 0, and G 1 with "1•".

Lemma 2 (CP is sound under context). For all differences ∆, stores S 0 , S ′ 0 , S 1 , S ′ 1 , and S,

guard stores G 0 , G ′ 0 , G 1 , G ′ 1 ,
and G, paths π 0 and π 1 , guard conjunctions ⃗ g ∧0 and ⃗ g ∧1 , and optional loop markers o 0 and o 1 , if the following statements hold:

i. ∀ n ∈ {0, 1}, S n , G n ⊢ CI( ⃗ g ∧n , π n , Π n (∆), o n ) ⇓ S ′ n , G ′ n
ii. S 0 and S 1 split S iii. G 0 and G 1 split G iv. Variable identifiers appearing in Π 0 (∆) start with "O_", and those appearing in Π 1 (∆) start with "T _O_" v. ⃗ g ∧0 contains only variables ending with 0 and ⃗ g ∧1 contains only variables ending with 1 then there exists a store S ′ and a guard store G ′ such that:

a. S, G ⊢ CP (∆, π 0 , π 1 , ⃗ g ∧0 , ⃗ g ∧1 , o 0 , o 1 ) ⇓ S ′ , G ′ b. S ′ 0 and S ′ 1 split S ′ c. G ′ 0 and G ′ 0 split G ′
Proof. The proof is primarily done by induction on the structure of the difference ∆.

Most of the resulting cases are tedious but rather straightforward, as they consist in proving that leaf commands from either program execute without changing any of the variables or guards corresponding to the other program. It may be noted that 'break' and 'continue' statements are no exception and do not pose any particular difficulty, as such considerations are taken care of when proving CI. However, there are some more complicated cases: indeed, the induction on the structure of ∆ is insufficient for reasoning about loops. Instead, when ∆ describes a pair of while loops, we need to reason by induction on their big-step execution. This turns out to be somewhat tricky as we cannot reason about a single loop but on a particular interleaving of the two loops. This is done by introducing a new judgment t w o _ l o o p s with rules corresponding to the interleaved execution of two loops. This judgment is proved to be equivalent to describing the separate execution of the two loops, so that it can be used to replace hypothesis (i) and be used for induction.

While the above key lemma mentions the invariants used in the induction, CP is typically used with fixed initial values for most of its arguments, hence the function correlated_program(∆) = CP (∆, 0, 1, true, true, None, None) and the associated theorem:

Theorem 2 (correlating_program is sound). For all stores S 0 , S 1 , S ′ 0 , and S ′ 1 , guard store G and difference ∆, if the following statements hold:

i. S 0 ⊢ Π 0 ((∆) T,T ′ ) ⇓ □ S ′ 0 ii. S 1 ⊢ Π 1 ((∆) T,T ′ ) ⇓ □ S ′ 1
then there exists a store S ′ and a guard store G ′ such that:

a. S 0 ⊎ S 1 , G ⊢ correlated_program((∆) T,T ′ ) ⇓ S ′ , G ′ b. S ′ 0 and S ′ 1 split S ′
Proof. As for the other proofs, the details can be found in the Coq development. The proof can however be outlined as follows:

By lemma 1, we have that CI(true, 0, Π 0 ((∆)

T,T ′ ), None) simulates Π 0 ((∆) T,T ′ ) and CI(true, 1, Π 1 ((∆) T,T ′ ), None) simulates Π 1 ((∆) T,T ′ ).
By lemma 2, we have that correlated_program((∆) T,T ′ ) simulates both CI(true, 0, Π 0 ((∆) T,T ′ ), None) and CI(true, 1, Π 1 ((∆) T,T ′ ), None) simulates Π 1 ((∆) T,T ′ ), thus simulating Π 0 ((∆) T,T ′ ) and Π 1 ((∆) T,T ′ ).

Implementation and experiments

As stated earlier, the algorithm described above has been proved within the Coq proof assistant. This amounts to about 3, 800 lines of Coq, of which 10% are definitions of the Imp br and guarded languages, as well of the definition of what a correct correlating program is. The remaining lines are used for the algorithm itself and its soundness proof. This Coq code is then extracted to OCaml. In addition to this extracted code, we also wrote about 1, 000 lines of OCaml to parse the input language, construct a syntactic difference and print the correlating program in C syntax. One should notice that the semantics of the generated C program does not exactly match the semantics of the formalized development: for instance, our input language manipulates mathematical integers while the generated C program uses fixed-length machine integers. Albeit it was not done because outside the core of our work, we do not consider it would be conceptually difficult to integrate into our input language the semantics of the generated C code (e.g. 32 bits integers), as the generation algorithm manipulates the syntax of expressions abstractly. Moreover, the semantics of our language is compatible with the semantics of input C language expected by "d i z y ". It should also be noted that the language presented in this paper has been slightly simplified for readability, while the actual tool and its formalization in Coq handle additional operators as well as a limited form of arrays.

To compute the structural syntactic differences, we aim at finding a minimal difference by an exploration of the space of mappings between abstract syntax trees, starting from the root nodes of the abstract syntax trees of the two programs. We recursively descend along those trees, comparing at each level all possible differences and keeping the minimal one (using an heuristics that tries to minimize insertion or deletion of loops). We use some memoization to implement a weak form of dynamic programming. While this computation of the syntactic difference is not proven correct nor optimal in Coq, a mechanically verified checker dynamically ensures that the projections of the chosen structural difference are indeed the two input programs.

To compare the quality of our correlating programs with the ones produced by "c c c ", a series of 23 examples (most between 10 and 20 lines long, with the exception of one around 140 lines long) were analyzed by "d i z y ". While doing so, we found no instance where the correlating program produced by "c c c " enabled a more precise analysis than that permitted by the correlating program generated by c o r r e l a t i n g _ p r o g r a m . On the contrary, we found several examples where c o r r e l a t i n g _ p r o g r a m outperformed "c c c " (examples 6, 7 and 23). One of the examples is a binary search algorithm in a sorted array, with the modified version introducing early loop exits. We can generate the correlating program and analyze it with "d i z y " (by slightly modifying it to correctly handle read access to arrays). We also attempted to test more complex examples but were limited by d i z y 's capabilities (e.g., no handling of C's bit-wise logical operations). All those tests are available online at https://www.irif.fr/thib/atva15/examples/ and can be reproduced. In practice, the computation of structural differences and the generation of the correlating program was almost instantaneous on our examples. Most of the computation time is spent in d i z y .

Chapter 2

Product programs

In this chapter-which only presents prior work and contains no new contribution-we review product programs, an existing notion that relates both to the previous notion of correlating programs and to the remaining of our work.

The correlating programs presented in the previous chapter are programs built by soundly interleaving the instructions of pairs of programs in order to be processed for further static analysis. This interleaving process is driven by heuristics which aim at factorizing the execution paths of the two programs with the hope that better factorized code paths will lead to better abstract analysis results. In that sense, programs are interleaved based on their syntactic proximity. In a nutshell, correlating programs are a generic way to present a pair of programs as a single program for a subsequent semantic analysis.

Much like correlating programs, product programs, as presented by Barthe et al. [START_REF] Barthe | Product programs and relational program logics[END_REF], are built by soundly interleaving the instructions of given pairs of programs. But in contrast with correlating programs, the very way they are built follows some semantics insight: indeed, each product program is constructed in order to prove a given specific semantic property, and every assumption made when factorizing code paths from both programs-for instance, that both programs always execute the same branch of a conditional-is made explicit in the product program by the addition of an assert statement. In that sense, unlike correlating programs, product programs are inherently semantic.

Again, we want to stress that this chapter contains no significant original contribution: it is merely a reframing of the aforementioned paper [START_REF] Barthe | Product programs and relational program logics[END_REF] featuring a few minor fixes, with the intent to bridge the work presented in the previous chapter with the work that will be presented next. This chapter also serves to present some definitions necessary to the subsequent chapters. These definitions include the formal definition of the simple imperative language Imp which will be used throughout the remaining of this manuscript, as well as that of several program logics, and of product programs.

Imp

The formal logic systems and product program rules that we will present in this chapter are tailored for the idealized imperative language Imp, which is not to be confused with Imp br presented earlier in Section 1.2. Indeed, while there are other reasons-which will be addressed in more details in the next chapter-for this change, the Imp language is also closer to the core imperative language used by Barthe et al. [START_REF] Barthe | Product programs and relational program logics[END_REF], easing comparison.

Syntax of Imp

The syntax of Imp is pretty standard, being composed of arithmetic expressions, boolean expressions, assignments, while-loops, conditionals and assert statements:

Definition 5 (Imp syntax). Statements c ::= skip | x = e | c; c | if (b) c else c | while (b) c | assert (b)
Arithmetic expressions

e ::= n | x | e ⊕ e ⊕ ::= + | -| * | / | % Boolean expressions b ::= true | false |!b | b && b | b || b | b == b | e == e | e < e | e ≤ e

Semantics of Imp

As with Imp br , the semantics of arithmetic and boolean expressions are defined on stores, that is, partial maps from variable identifiers to integer values.

The judgment "S ⊢ e ⇓ n" reads "In store S, the arithmetic expression e evaluates into the integer n", and the judgment "S ⊢ b ⇓ b" reads "In the store S, the boolean expression b evaluates into the boolean b". Definition 6 (Imp expression semantics). The following rules define the operational semantics for Imp expressions:

Constant S ⊢ n ⇓ n Variable S ⊢ x ⇓ S(x) Sum S ⊢ e 1 ⇓ n 1 S ⊢ e 2 ⇓ n 2 S ⊢ e 1 + e 2 ⇓ n 1 + Z n 2 Subtraction S ⊢ e 1 ⇓ n 1 S ⊢ e 2 ⇓ n 2 S ⊢ e 1 -e 2 ⇓ n 1 -Z n 2 Multiplication S ⊢ e 1 ⇓ n 1 S ⊢ e 2 ⇓ n 2 S ⊢ e 1 * e 2 ⇓ n 1 × Z n 2 Division S ⊢ e 1 ⇓ n 1 S ⊢ e 2 ⇓ n 2 n 2 ̸ = 0 S ⊢ e 1 /e 2 ⇓ n 1 / Z n 2 Modulo S ⊢ e 1 ⇓ n 1 S ⊢ e 2 ⇓ n 2 S ⊢ e 1 %e 2 ⇓ n 1 % Z n 2
Definition 7 (Imp boolean expression semantics). The following rules define the operational semantics for Imp boolean expressions:

Constant S ⊢ b ⇓ b Not S ⊢ b ⇓ b S ⊢!b ⇓ ¬b And S ⊢ b 1 ⇓ b 1 S ⊢ b 2 ⇓ b 2 S ⊢ b 1 && b 2 ⇓ b 1 ∧ b 2 Or S ⊢ b 1 ⇓ b 1 S ⊢ b 2 ⇓ b 2 S ⊢ b 1 || b 2 ⇓ b 1 ∨ b 2 BoolEqual S ⊢ b 1 ⇓ b 1 S ⊢ b 2 ⇓ b 2 S ⊢ b 1 == b 2 ⇓ b 1 = b 2 Equal S ⊢ e 1 ⇓ n 1 S ⊢ e 2 ⇓ n 2 S ⊢ e 1 == e 2 ⇓ n 1 = Z n 2 LessThan S ⊢ e 1 ⇓ n 1 S ⊢ e 2 ⇓ n 2 S ⊢ e 1 < e 2 ⇓ n 1 < Z n 2 LessOrEqual S ⊢ e 1 ⇓ n 1 S ⊢ e 2 ⇓ n 2 S ⊢ e 1 ≤ e 2 ⇓ n 1 ≤ Z n 2
The interpretation of statements transforms a store into another store: the judgment S ⊢ c ⇓ S ′ states that the statement c transforms the store S into the store S ′ . Definition 8 (Imp statements semantics). The following rules define the operational semantics for Imp statements:

Skip S ⊢ skip ⇓ S Assign S ⊢ e ⇓ n S ⊢ x = e ⇓ S[x ↦ → n] Assert S ⊢ b ⇓ true S ⊢ assert (b) ⇓ S Seq S ⊢ c 1 ⇓ S ′ S ′ ⊢ c 2 ⇓ S ′′ S ⊢ c 1 ; c 2 ⇓ S ′′ If-Then S ⊢ b ⇓ true S ⊢ c 1 ⇓ S ′ S ⊢ if (b) c 1 else c 2 ⇓ S ′ If-Else S ⊢ b ⇓ false S ⊢ c 2 ⇓ S ′ S ⊢ if (b) c 1 else c 2 ⇓ S ′ While False S ⊢ b ⇓ false S ⊢ while (b) c ⇓ S While True S ⊢ b ⇓ true S ⊢ c ⇓ S ′ S ′ ⊢ while (b) c ⇓ S ′′ S ⊢ while (b) c ⇓ S ′′
For simplicity's sake, unlike the language defined by Barthe et al. [START_REF] Barthe | Product programs and relational program logics[END_REF], Imp does not feature arrays. Therefore we will omit the array update rules defined in the original article. This omission is not a fundamental change, as the array update rules are almost identical to the assignment rules.

Hoare Logic

Hoare Logic [START_REF] Antony | An axiomatic basis for computer programming[END_REF] is a well-known program logic used to prove that programs are correct with regards to a given specification. While it only considers the execution of a single program-as opposed to the execution of multiple programs-it is both an inspiration and a building block for the proof systems presented thereafter.

In Hoare Logic, the correct execution of a program is described by a Hoare Triple of the form {P } c {Q} where P and Q are logical assertions over states. Informally, such a triple states that for every store S satisfying the precondition P , no error arises when executing c in S and the resulting store S ′ -if any-satisfies the postcondition Q.

Hoare Logic is made of a set of axioms and inference rules to prove Hoare Triples. A Hoare Triple is valid if there exist a derivation using the Hoare Logic rules defined below that reaches its conclusion.

Hoare Logic provides a set of rules to prove such triples valid:

⊢ {P } skip {P } Skip P ⇒ b ⊢ {P } assert (b) {P } Assert ⊢ {P [e/x]} x = e {P } Assign ⊢ {P } c 1 {Q} ⊢ {Q} c 2 {R} ⊢ {P } c 1 ; c 2 {R} Seq ⊢ {P ∧ b} c 1 {Q} ⊢ {P ∧ ¬b} c 2 {Q} ⊢ {P } if (b) c 1 else c 2 {Q} If ⊢ {P ∧ b} c {P } ⊢ {P } while (b) c {P ∧ ¬b} While ⊢ {P } c {Q} P ′ ⇒ P Q ⇒ Q ′ ⊢ {P ′ } c {Q ′ } Sub
Note that a Hoare Triple can be valid even if the specified program does not actually terminate. Indeed, the W h i l e rule does not ensure termination, as it does not require the repeated execution of the loop's body c in a store satisfying P to eventually lead to a store in which b evaluates to false. This notion of correctness is called partial correctness: a valid Hoare Triple does not mean the program terminates on any input matching the precondition, but that whenever it does, the result satisfies the given postcondition. If termination is expected, it has to be proven separately.

In addition, Hoare Logic is incomplete, in the sense that not every true Hoare Triple is provable. This incompleteness stems from the incompleteness of the logic used for assertions: indeed, the S u b and A s s e r t rules require determining the validity of certain logical assertions. However, Gödel's Incompleteness Theorem states that there exist no consistent proof system containing basic arithmetic in which every true assertion can be proven. Hoare Logic is, however, said to have relative completeness in the sense that supposing every true assertion has a proof, then every true Hoare Triple has a Hoare Logic proof.

In our Coq implementation, assertions are Coq propositions on stores, thus using Coq's own logic to prove those assertions.

Relational Hoare Logic

Relational Hoare Logic [START_REF] Benton | Simple Relational Correctness Proofs for Static Analyses and Program Transformations (Revised, Long Version)[END_REF] (RHL) is a program logic for reasoning about pairs of programs. As the name suggests, it is an adaptation of Hoare Logic to pairs of programs and relational properties. Its judgments are of the form ⊢ {P } c 1 ∼ c 2 {Q} where c 1 and c 2 are the two statements under consideration, while the precondition P and the postcondition Q are assertions on pairs of program states. For simplicity's sake we assume that the program states have separate sets of variable identifiers, that is, variable identifiers occurring in one program are absent from the other. Intuitively, such a judgment is valid if all executions of c 1 and c 2 from a pair of states satisfying P either diverge or successfully result in a pair of states satisfying Q.

Example 3. For instance, consider the two following programs:

if (x < 4) x = x + 2 else skip (2.1) if (y < 2) y = y + 1 else skip (2.2)
The following judgment relates those two programs, asserting that executing them on a pair of states satisfying the precondition x = 2y results in a pair of states satisfying the postcondition x = 2y:

⊢ {x = 2y} if (x < 4) x = x + 2 else skip ∼ if (y < 2) y = y + 1 else skip {x = 2y}
The remaining of this section presents increasingly expressive variants of Relational Hoare Logic.

Minimal Relational Hoare Logic

A first RHL variant is Minimal Relational Hoare Logic, which is akin to using traditional Hoare Logic by applying the same rules to both programs under consideration at the same time. Because of this, Minimal Relational Hoare Logic considers only pairs of programs with the same syntactic structure, requiring them to execute in lockstep, taking the same branches and performing the same number of loop iterations. Definition 9 (Minimal RHL). Minimal Relational Hoare Logic is defined by the following set of inference rules:

⊢ {P } skip ∼ skip {P } R-Skip P ⇒ b 1 ∧ b 2 ⊢ {P } assert (b 1 ) ∼ assert (b 2 ) {P } R-Assert ⊢ {P [e 2 /x 2 ][e 1 /x 1 ]} x 1 = e 1 ∼ x 2 = e 2 {P } R-Assign ⊢ {P } c 1 1 ∼ c 2 1 {Q} ⊢ {Q} c 1 2 ∼ c 2 2 {R} ⊢ {P } c 1 1 ; c 1 2 ∼ c 2 1 ; c 2 2 {R} R-Seq ⊢ {P ∧ b 1 } c 1 1 ∼ c 2 1 {Q} ⊢ {P ∧ ¬b 1 } c 1 2 ∼ c 2 2 {Q} P ⇒ b 1 = b 2 ⊢ {P } if (b 1 ) c 1 1 else c 1 2 ∼ if (b 2 ) c 2 1 else c 2 2 {Q} R-If ⊢ {P ∧ b 1 } c 1 ∼ c 2 {P } P ⇒ b 1 = b 2 ⊢ {P } while (b 1 ) c 1 ∼ while (b 2 ) c 2 {P ∧ ¬b 1 } R-While ⊢ {P } c 1 ∼ c 2 {Q} P ′ ⇒ P Q ⇒ Q ′ ⊢ {P ′ } c 1 ∼ c 2 {Q ′ } R-Sub Minimal Relational Hoare Logic is sound, that is, if ⊢ {P } c 1 ∼ c 2 {Q}
is derivable using the above rules, then all non-diverging executions of c 1 and c 2 from pairs of states satisfying P successfully reach pairs of states satisfying Q. We will provide a novel, mechanically-checked proof of this assertion in Chapter 5.

Core Relational Hoare Logic

The requirement imposed by Minimal RHL that both programs must share the same syntactic structure and dynamic execution paths makes it unsuitable for relating all but the most similar pairs of programs.

For instance, Minimal RHL cannot be used to relate the program skip; x = e to the program x ′ = e ′ . Indeed, none of the rules defined above applies to statements with different syntactic structures.

Thankfully, Minimal RHL can easily be extended to such pairs of programs featuring different syntactic structure by adding rules for reasoning separately about each program.

Definition 10 (Core RHL). Core Relational Hoare Logic is the logic defined by extending Minimal Relational Hoare Logic with the following rules for reasoning about left programs:

⊢ {P } skip ∼ c {Q} P ⇒ b ⊢ {P } assert (b) ∼ c {Q} R-Assert-L ⊢ {P } skip ∼ c {Q} ⊢ {P [e/x]} x = e ∼ c {Q} R-Assign-L ⊢ {P ∧ b} c 1 ∼ c {Q} ⊢ {P ∧ ¬b} c 2 ∼ c {Q} ⊢ {P } if (b) c 1 else c 2 ∼ c {Q} R-If-L ⊢ {P } c 1 ∼ skip {Q} ⊢ {Q} c 2 ∼ c {R} ⊢ {P } c 1 ; c 2 ∼ c {R} R-Seq-Skip-L
And the following rules for reasoning about right programs:

⊢ {P } c ∼ skip {Q} P ⇒ b ⊢ {P } c ∼ assert (b) {Q} R-Assert-R ⊢ {P } c ∼ skip {Q} ⊢ {P [e/x]} c ∼ x = e {Q} R-Assign-R ⊢ {P ∧ b} c ∼ c 1 {Q} ⊢ {P ∧ ¬b} c ∼ c 2 {Q} ⊢ {P } c ∼ if (b) c 1 else c 2 {Q} R-If-R ⊢ {P } skip ∼ c 1 {Q} ⊢ {Q} c ∼ c 2 {R} ⊢ {P } c ∼ c 1 ; c 2 {R} R-Seq-Skip-R
Readers familiar with the original article may notice that our R-Assign-L rule is slightly different from the version presented by Barthe et. al: indeed, when formalizing Core RHL in Coq, we found that this rule had the preconditions swapped between the premises and conclusions. The R-Update-L rule from the original paper, which is omitted here, presents a similar error. In addition, we added the R-Seq-Skip-L rule, which we believe was improperly omitted in the original paper.

Example 4. To take our earlier example, with Core Relational Hoare Logic, comparing skip; c to c becomes possible:

⊢ {P } skip ∼ skip {P } R-Skip . . . ⊢ {P } c ∼ c {Q} ⊢ {P } skip; c ∼ c {Q} R-Seq-Skip-L
As with Minimal Relational Hoare Logic, we will provide a new, mechanicallychecked proof of soundness for Core Relational Hoare Logic in the next chapter.

Extended Relational Hoare Logic

The final variant presented in the original paper, Extended Relational Hoare Logic, is obtained by extending Core Relational Hoare Logic with the single rule R -U n f o l d :

⊢ {P } c ′ 1 ∼ c ′ 2 {Q} ⊢ [c 1 ] ≽ [c ′ 1 ] ⊢ [c 2 ] ≽ [c ′ 2 ] ⊢ {P } c 1 ∼ c 2 {Q} R-Unfold
where ⊢ [c] ≽ [c ′ ] holds if and only if c ′ crashes whenever c crashes and finite executions of c and c ′ lead to extensionally-equivalent results. This rule allows replacing the two statements under consideration by two other statements whose non-crashing extensional behaviors are included in those of the two statements under consideration. This enables reasoning about pairs of programs with non-synchronized loops.

Self-composition

While the Relational Hoare Logic variants presented above are increasingly expressive, they are still incomplete, as they can only be used to relate pairs of programs with similar structures. Relative completeness can be recovered by adding the following self-composition rule to any of the Relational Hoare Logic variants previously defined:

⊢ {P } c 1 ; c 2 {Q} ⊢ {P } c 1 ∼ c 2 {Q} R-SelfComp
This rule reduces the proof of a relational property to a proof in regular Hoare Logic, enjoying the relative completeness of the latter. Proofs in this style will however not exploit the possible similarity in the control structure of both programs and will therefore be much more involved.

Product programs

A product program, much like the correlated programs presented in the previous chapter, is a single program simulating the behaviors of two other programs. In contrast to correlated programs, however, product programs are built following syntactic rules based on semantics insights. Barthe et al. [START_REF] Barthe | Product programs and relational program logics[END_REF] present several set of rules to build such programs, each rule set corresponding to one of the RHL variants presented above. Informally, product programs interleave statements in the same "order" they are considered in RHL proofs, while materializing side conditions by inserting corresponding assert statements. This leads Hoare Logic proofs on a product program c ′ to follow the same structure as Relational Hoare Logic proofs on the corresponding pair of programs (c 1 , c 2 ), such that the correction of a Hoare Triple {P } c ′ {Q} implies that of the Relational Hoare Quadruple {P } c 1 ∼ c 2 {Q}. One benefit of doing so is that off-the-shelf non-relational verification tools can then be used on the product program.

By comparison with the previous approach of correlating programs, while product programs can also be used in a two-stage analysis-first building a product program and then performing non-relational program analysis on it-, the relation between control paths of both programs is statically assumed when building the product program, and those assumptions are made explicit by the addition of assert statements. Alternatively, product program generation and verification can be done simultaneously, the later driving the construction of the product program. This is explained in more details in the original paper, and not repeated here as it is out of the scope of this thesis.

Minimal product programs

The rules driving the construction of minimal product programs mirror that of Relational Hoare Logic, deferring the verification of side conditions to subsequent proofs by pushing them into assert statements, in such a way that a regular Hoare Logic proof on a Minimal product program will have roughly the same shape as a Minimal Relational Hoare Logic proof of the same property. For instance, whenever a Minimal RHL proof involves the rule R -S k i p , the Hoare Logic proof on the corresponding minimal product program will use the Hoare Logic rule S k i p . Likewise, as a pair of assert statements is translated to a sequence of assert statements, Minimal RHL proofs involving R -A s s e r t will lead to Hoare Logic proofs involving the Hoare Logic rules S e q and A s s e r t .

Valid minimal product programs are defined by the judgment c 1 × c 2 -→ c stating that c is a valid product program of c 1 and c 2 . As with Minimal RHL, we assume that left and right programs refer to separate variable identifiers, so that instructions from one program do not change the other program's behavior.

skip × skip -→ skip P-Skip x 1 = e 1 × x 2 = e 2 -→ x 1 = e 1 ; x 2 = e 2 P-Assign assert (b 1 ) × assert (b 2 ) -→ assert (b 1 ); assert (b 2 ) P-Assert c 1 1 × c 2 1 -→ c 1 c 1 2 × c 2 2 -→ c 2 c 1 1 ; c 1 2 × c 2 1 ; c 2 2 -→ c 1 ; c 2 P-Seq c 1 1 × c 2 1 -→ c 1 c 1 2 × c 2 2 -→ c 2 if (b 1 ) c 1 1 else c 1 2 × if (b 2 ) c 2 1 else c 2 2 -→ assert (b 1 == b 2 ); if (b 1 ) c 1 else c 2 P-If c 1 × c 2 -→ c while (b 1 ) c 1 × while (b 2 ) c 2 -→ assert (b 1 == b 2 ); while (b 1 ) c P-While
Each of the rules defined above corresponds to a Minimal RHL rule. For instance, P -S k i p corresponds to R -S k i p and relates a pair of skip statements by replacing them with a single skip. A sequence of skip could have been used instead, but it would have had the same extensional semantics. Likewise, P -A s s i g n corresponds to R -A s s i g n and transforms a pair of assignments into a sequence of those same two assignments, while P -A s s e r t corresponds to R -A s s e r t and transforms a pair of assertions into a sequence.

P -S e q is purely recursive and corresponds to R -S e q . P -I f , which corresponds to R -I f is more interesting: instead of requiring a proof that the two programs' conditions are equivalent, this condition is made explicit by inserting a corresponding assertion. This allows deferring the proof to a subsequent Hoare Logic proof. P -W h i l e is to R -W h i l e what P -I f is to R -I f , encoding the side-condition by inserting an assertion.

Core products

The core product program construction extends minimal product program rules with rules mimicking Core Relational Hoare Logic, with, much like the former, rules for reasoning about part of the left program:

x = e × skip -→ x = e P-Assign-L assert (b) × skip -→ assert (b) P-Assert-L c 1 × skip -→ c ′ 1 c 2 × c -→ c ′ 2 c 1 ; c 2 × c -→ c ′ 1 ; c ′ skip × x = e -→ x = e P-Assign-R skip × assert (b) -→ assert (b) P-Assert-R skip × c 1 -→ c ′ 1 c × c 2 -→ c ′ 2 c × c 1 ; c 2 -→ c ′ 1 ; c ′ 2 P-Seq-Skip-R c × c 1 -→ c ′ 1 c × c 2 -→ c ′ 2 c × if (b) c 1 else c 2 -→ if (b) c ′ 1 else c ′ 2 P-If-R

Shortcomings of RHL and Product Programs

Both Relational Hoare Logic and the closely-related product program construction rules mentioned above enable formal relational reasoning on pairs of programs. However, those logics only ensure partial correctness, and as such cannot be used for non-terminating or crashing programs.

In particular, Relational Hoare Logic and product programs cannot express relations between a crashing program and a non-crashing one, even though such changes-known as bugfixes-are frequent in the day-to-day practice of software development. This is easily explained on product programs: as the instructions of both programs are re-used in the product program with the same meaning, any crashing instruction of either program gets included in the product program, which will also crash. For instance, consider the two following programs:

m = a % b ; i f ( m = = 0 ) i s _ m u l t i p l e = 1 ;
e l s e i s _ m u l t i p l e = 0 ;

i f ( b = = 0 ) { i s _ m u l t i p l e = 0 ; } e l s e { m = a % b ; i f ( m = = 0 ) i s _ m u l t i p l e = 1 ;
e l s e i s _ m u l t i p l e = 0 ; } In the above example, the left program will crash if "b " is set to 0, because it will attempt to divide "a " by 0. The right program avoids this issue by adding a conditional, setting the resulting value "i s _ m u l t i p l e " to 0 if "b " is set to 0. This change could be described as fixing a known crash, and asserting that "is_multiple" is set to 0 for every input that makes the left program crash. This property cannot be stated in Relational Hoare Logic. After tagging left and right variables to avoid conflicts by respectively prefixing them with "l _ " and "r _ ", one possible product program would be:

i f ( r _ b = = 0 ) { r _ i s _ m u l t i p l e = 0 ; l _ m = l _ a % l _ b ; i f ( l _ m = = 0 ) l _ i s _ m u l t i p l e = 1 ;
e l s e

l _ i s _ m u l t i p l e = 0 ; } e l s e { l _ m = l _ a % l _ b ; r _ m = r _ a % r _ b ; a s s e r t ( ( l _ m = = 0 ) = = ( r _ m = = 0 ) ) ; i f ( l _ m = = 0 ) { l _ i s _ m u l t i p l e = 1 ; r _ i s _ m u l t i p l e = 1 ; } e l s e { l _ i s _ m u l t i p l e = 0 ; r _ i s _ m u l t i p l e = 0 ; } }
One can see that in the example above, if "l _ b = 0", even though the right program is fixed, the product program will execute code from the left program, and will crash at line 3, when attempting to divide by zero.

The issue illustrated above is the main shortcoming we will attempt to address in the remaining of this thesis.

Chapter 3

Correlating oracles

In this chapter, we present our main contribution, that is, the formal framework of correlating oracles, which purpose is to express and verify relations between the executions of a pair of programs. It is specifically designed to address the shortcomings of product programs and correlating programs by allowing reasoning on crashing and non-terminating programs. This work has been summarily presented in an earlier paper [START_REF] Girka | Verifiable semantic difference languages[END_REF] we published, but this chapter presents an updated version of this work, and presents it more extensively.

Our framework is based on an idea similar to that of product programs and correlating programs: indeed, much like them, correlating oracles are programs specifically constructed to relate pairs of programs by soundly simulating them. However, because we are interested in reasoning about crashing and non-terminating programs, the relations exhibited by correlating oracles cannot be characterized solely on the programs' final states, as those may not exist. Instead, correlating oracles relate the execution of both programs, a notion we will define more formally within this chapter.

In the meantime, we can informally describe a correlating oracle between a left program and a right program as a third program which successive states relate states of the left and right programs, as illustrated by the following diagram, in which the top line presents successive states of the left program, the bottom line represents those of the right program, the middle one that of the correlating oracle, arrows represent computation steps, and dashed lines the "relation" between states:

s 1 l s 2 l s 3 l s 4 l s 5 l s 1 r s 2 r s 3 r s 4 r s 5 r • • • • • • o 1 o 2 o 3 o 4
In l . This is especially useful when a program performs a computation that is not significant with regards to the relation we are interested in: for instance, we may be interested in showing that some variables take the same successive values in both programs, but one of the program performs extra operations on a variable we are not interested in.

In a sense, correlating oracles are bi-interpreters, as they interpret two programs at the same time: as illustrated above, an execution step of a correlating oracle corresponds to a finite number of steps of the two programs it relates. The choice of the verb "interpret" here rather than "simulate" is no accident: indeed, as we will see with most of our oracle languages, oracles will in practice often maintain an internal copy of the program states under consideration, inspect them, and interpret them if needed. This is not a requirement, though, and oracles may very well use different techniques, for instance maintaining an internal copy of just one of the two related programs and transform it to the other program's on-the-fly. Nevertheless, we want to place emphasis on the ability of correlating oracles to inspect and manipulate program states. Indeed, while correlating programs simulate left and right programs by interleaving the two programs' statements based on syntactic or textual criteria, and product programs do so following an explicit semantic reasoning provided upfront, correlating oracles are typically written in a different, specific programming language and do not syntactically interleave actual instructions from left and right programs.

Much like a program is written in a programming language, correlating oracles in our framework are written in oracle languages. Our framework is generic in the sense that the definition of oracle languages is parameterized by two programming languages: indeed, each oracle language is specific to a pair of programming languages, and any oracle written in such a language is specific to a pair of programs written in the corresponding programming languages. This does not mean that an oracle language has to be able to relate every single pair of programs or that there should be only one oracle language per pair of programming languages. In fact, the approach we have taken is to write an oracle language for each "kind of relation" we wanted to exhibit: an oracle language for renaming variables, one oracle language for swapping independent assignments, etc. This correlating oracle framework is formally defined within the Coq proof assistant: every definition in this section roughly corresponds to a formal Coq definition, and each of the instantiated oracle languages is proved correct within Coq as well. For every definition, lemma or theorem present in this section, the corresponding Coq definitions will be either linked or included.

General definition of a programming language

As stated earlier, our framework is generic with regards to programming languages. Those programming languages need to conform to a defined formalism, however, in order to be manipulated consistently. To this effect, we have chosen deterministic small-step operational semantics as our formalism. The reason for this choice is that we are interested in relating programs that may crash or not terminate, stating for instance that two non-terminating programs have infinitely many "locally-equivalent" program states, or that a crashing program's last non-crashed state somehow relates to a non-crashing program's execution.

Definition 11 (Programming language definition). A programming language definition is a 7-uple (P, G, S, I, E, R, F) such that:

• P is the type of program abstract syntax trees.

• G is the type of static evaluation environments or global environments, e.g. a table of class definitions in the case of object-oriented languages such as Java.

• S is the type of dynamic evaluation environments or state, e.g. heap, stack and program counter or continuation in Java.

• I is the initialisation function of type P → G × S to produce an initial program state (or configuration) given its source code as an abstract syntax tree.

• E is the partial evaluation function of type G → S ↦ → S to execute program configurations step by step.

• R is the program return type, e.g. an integer for C programs.

• F is the result extraction partial function of type S ↦ → R to extract the result of a successful final state.

In addition, these definitions must also fulfill the following requirements:

1. F only characterizes stuck configurations, that is: ∀g : G, ∀s : S, E g s is undefined if F s is defined. 2. S and G must be equipped with a decidable equality preserved by E.

This presentation is relatively standard, and it is close to the one used in the CompCert certified compiler [START_REF] Leroy | The CompCert verified compiler[END_REF]. The main difference between our presentation and that of CompCert is that E is a transition function, and not a transition relation, thus requiring programming languages to be deterministic, a restriction that we will explain in more details in the conclusion of this thesis.

Definition 12 (Program configurations). We call configuration a pair of a static evaluation environment and of a dynamic evaluation environment. The set of configurations of a programming language L is C L = G L × S L .

We say that a configuration is stuck (or, abusively, that a state is stuck) if E is not defined on it. In the remaining of this section, we may write s → s ′ for E g s = s ′ when there is no ambiguity about the static environment g. Likewise, we may write s ̸ → for (g, s) ̸ ∈ dom(E ).

Definition 13 (Terminating configurations). A configuration c ∈ C is said to terminate (written c → * ̸ →) if it reaches a stuck state. This last state is called a final state if a result value can be extracted using F. An execution that reaches a stuck state which is not a final state crashes.

Correlating oracles: operational semantics for differences

While they do not share the above definition, oracle languages are, at their heart, programming languages defined by a deterministic operational semantics. Those languages are, in addition, equipped with a few functions to project oracle states to left and right program states, as well as properties to assert some invariant property on oracle states and to prove the aforementioned projections to be valid. Definition 14 (Correlating oracle language definition). Given two language definitions

L 1 = (P 1 , G 1 , S 1 , I 1 , E 1 , R 1 , F 1 ) and L 2 = (P 2 , G 2 , S 2 , I 2 , E 2 , R 2 , F 2 ), an oracle language definition between L 1 and L 2 is a 8-uple (G, O, S, π ′ L , π ′ R , π L , π R , I) such that:
• G is the type of static evaluation environments.

• O is the type of dynamic evaluation environments.

• S is the interpretation function of type

G × O ↦ → O. • π ′ L (resp. π ′ R ) is a projection function of type G → G 1 (resp. G → G 2 ). • π L (resp. π R ) is a projection function of type O → S 1 (resp. O → S 2 ). • I is an invariant of type G × O → P.
with the following additional requirements ensuring its soundness:

1. I is preserved by S i.e. ∀g : G, ∀o : O, I(g, o) ⇒ I(g, S(g, o)) 2. S leads to correct and productive predictions i.e. ∀g : G, ∀o o ′ : O,

I(g, o) ⇒ S(g, o) = o ′ ⇒ ∃ n 1 n 2 , ⎧ ⎪ ⎨ ⎪ ⎩ π L (S(g, o)) = E n 1 1 (π ′ L (g), π L (o)) π R (S(g, o)) = E n 2 2 (π ′ R (g), π R (o)) n 1 + n 2 > 0
3. the oracle is complete, in the sense that it only terminates when both underlying programs themselves terminate, i.e. ∀g : G, ∀o : O,

(g, o) ̸ ∈ dom(S) ⇒ (π ′ L (g), π L (o)) ̸ ∈ dom(E 1 ) ∧ (π ′ R (g), π R (o)) ̸ ∈ dom(E 2 )
Each oracle configuration thus relates a pair of program configurations that can be recovered using the appropriate projection functions. The oracle asserts some property on those pairs of configurations through the invariant I, which is defined on oracle configurations rather than on projected program configurations: indeed, additional runtime information may be needed for the oracle to execute properly, as well as to prove its soundness, as we will see with the oracle languages defined in Chapters 4 and 5.

The productivity condition, that is, the fact that each oracle step performed by S corresponds to at least one reduction step in either program (n 1 + n 2 > 0 in requirement 2.) is essential to ensuring that the oracle does not "silently stop relating programs" by performing non-productive reductions.

Remark. As one may notice, the definition of oracle languages resembles that of programming languages: both have static and dynamic evaluation environments, as well as a step function. Therefore, one may wonder why oracle languages are not programming languages. The reasons for this are mainly practical: indeed, as it is reasonable for oracle to be able to verify equality between two program states, we require in our Coq development that two languages have decidable equality for their states. Unless we are interested in having oracles relating other oracles,-which we cannot find a use-case for-such a requirement is unneeded and would significantly clutter formal oracle language definitions for no clear benefit. Furthermore, a result extraction function on oracle configurations would be of limited use, and syntactic representations of oracles will be covered in the next chapter.

To illustrate the execution of an oracle, we will often present its execution trace along that of the programs it relates, as in the following diagram:

s 1 l s 2 l s 3 l s 4 l s 5 l s 1 r s 2 r s 3 r s 4 r s 5 r E l E l E l E l • • • Er Er Er Er • • • o 1 o 2 o 3 o 4 S S S π L π R π L π R π L π R π L π R
In the diagram above, s 1 l to s 5 l are successive dynamic states of the left program while s 1 r to s 5 r are successive dynamic states of the right program, o 1 to o 4 are successive dynamic states of the oracle, E l and E r are the step functions of the languages the left and right program are respectively written in, and every static state is omitted for conciseness.

The main advantage of our approach over product programs and correlating programs is that correlating oracles, by not actually interleaving instructions of a pair of programs, but rather interpreting them and inspecting program states, are able to relate them even if one of them gets stuck. This is essential to characterizing some bugfixes, which are a very common type of changes. Some correlating oracle languages dedicated to these kind of changes will be defined in Chapter 4. When relating a crashed program with a non-crashed one, such oracles will only step in the non-crashing one.

The reason for which those small-step operational semantics are deterministic is mainly historic and will be covered in more details in the conclusion of this thesis.

Identity and universal oracles

Two really simple language-agnostic oracle languages can be defined within our framework: the identity oracle and the universal oracle. Those two examples are languageagnostic in the sense that they are parameterized by one (in the case of the identity oracle) or two (in the universal oracle's case) programming languages on which they pose no restriction. Of course, those two oracle languages are of very limited practical interest, as they either convey trivial information (in the identity oracle's case, that the two programs are syntactically strictly equal) or no information at all (in the universal oracle's case) but they are suitable for a decent practical introduction to our framework's formal definitions.

Identity oracle

The identity oracle relates pairs of programs that are exactly the same, evaluating them in lock-step and asserting that for each such step, both programs' configurations are identical.

Definition 15 (Identity oracle language). The identity oracle language is defined for every language definition L = (P, G, S, I, E, R, F) as the oracle language definition (G, S, E, id, id, id, id, I) where:

• id(x) = x is the polymorphic identity function • I(g, s) = ⊤ is the universally-valid invariant
The identity oracle language is thus a thin wrapper around the underlying programming language, executing a single instance of a program using its standard semantics. Since the related programs are identical, their configurations are recovered by the projection functions, which simply returns the oracle's internal configuration.

s 1 s 2 s 3 s 4 s 1 s 2 s 3 s 4 s 1 s 2 s 3 s 4 E E E • • • id id E id id E id id E id id • • • E E E • • •
Lemma 3 (Invariant preservation of the identity oracle). Invariant preservation is immediate, as the invariant is always satisfied no matter the internal state.

Lemma 4 (Prediction soundness of the identity oracle). Prediction soundness is immediate, as each step of the identity oracle performs exactly one step of the underlying program.

Lemma 5 (Prediction completeness of the identity oracle). As the program configurations under consideration are the same as the oracle configuration, the oracle only terminates when the two underlying (identical) programs terminate.

Universal oracle

The universal oracle can relate any pair of programs without asserting any precise relation between them, by relating their successive configurations arbitrarily.

Definition 16 (Universal oracle language). The universal oracle language is defined for every pair of language definitions

L 1 = (P 1 , G 1 , S 1 , I 1 , E 1 , R 1 , F 1 ) and L 2 = (P 2 , G 2 , S 2 , I 2 , E 2 , R 2 , F 2 ) as the oracle language definition (G 1 × G 2 , S 1 × S 2
, S, f st, snd, f st, snd, I) where:

• f st((x, y)) = x • snd((x, y)) = y • S((g 1 , g 2 ), (s 1 , s 2 )) = ⎧ ⎪ ⎪ ⎪ ⎪ ⎪ ⎨ ⎪ ⎪ ⎪ ⎪ ⎪ ⎩ (E 1 (g 1 , s 1 ), E 2 (g 2 , s 2 )) if (g 1 , s 1 ) ∈ dom(E 1 ) ∧ (g 2 , s 2 ) ∈ dom(E 2 ) (s 1 , E 2 (g 2 , s 2 )) if (g 1 , s 1 ) ̸ ∈ dom(E 1 ) ∧ (g 2 , s 2 ) ∈ dom(E 2 ) (E 1 (g 1 , s 1 ), s 2 ) if (g 1 , s 1 ) ∈ dom(E 1 ) ∧ (g 2 , s 2 ) ̸ ∈ dom(E 2 )
undefined otherwise

• I(g, s) = ⊤

A universal oracle configuration consists of the configurations of the two "related" programs, and their evaluation is delegated to the evaluation function of the corresponding languages.

s 1 l s 2 l s 3 l s 4 l (s 1 l , s 1 r ) (s 2 l , s 2 r ) (s 3 l , s 3 r ) (s 4 l , s 4 r ) s 1 r s 2 r s 3 r s 4 r E E E • • • f st snd S f st snd S f st snd S f st snd • • • E E E • • •
In case one of the programs gets stuck before the other, the universal oracle will continue to interpret the remaining one:

s 1 l s 2 l s 3 l (s 1 l , s 1 r ) (s 2 l , s 2 r ) (s 3 l , s 3 r ) (s 4 l , s 4 r ) s 1 r s 2 r s 3 r s 4 r E E f st snd S f st snd S f st snd S snd • • • E E E • • • f st Lemma 6 (Invariant

General theorems

Our main generic theoretical result on correlating oracles is the following: given two programs whose executions terminate in a finite number of steps, any sound oracle relating them will reach those programs' stuck states in a finite number of states. This is a somewhat direct consequence of the productivity condition of oracle languages, and is particularly useful to prove extensional properties, as we will see in Chapter 5.

Theorem 3 (Oracles between terminating programs reach terminating states).

Given

an oracle language (G, O, S, π ′ L , π ′ R , π L , π R , I) between programs written in lan- guages L 1 = (P 1 , G 1 , S 1 , I 1 , E 1 , R 1 , F 1 ) and L 2 = (P 2 , G 2 , S 2 , I 2 , E 2 , R 2 , F 2 ),
• for every oracle configuration (g, o) such that I(g, o),

• for every natural numbers n, n 1 , and

n 2 such that n ≤ n 1 + n 2 , • for every left program state s ′ 1 such that π L (o) → n 1 s ′ 1 ̸ →, • for every right program state s ′ 2 such that π R (o) → n 2 s ′ 2 ̸ →, and, • for every oracle state o ′ such that S ′n (g, o) = o ′ where S ′ (g, o) = { S(g, o) if (g, o) ∈ dom(S) (g, o) if (g, o) ̸ ∈ dom(S) then • π L (o ′ ) = s ′ 1 • π R (o ′ ) = s ′ 2 • I(g, o ′ )
That is, for every oracle global environment g and every oracle state o on which the oracle's invariant I holds and that can be projected to left and right configurations that reduce to stuck states s ′ 1 in n 1 steps and s ′ 2 in n 2 steps respectively, then the oracle o reaches in at most n 1 + n 2 steps an oracle state o ′ that projects to the final configurations s ′ 1 and s ′ 2 .

Proof. The proof is done by induction on n.

In the base case, we have n = 0. Theorem 4 (Oracles between terminating programs terminate). Given an oracle lan-

Since n ≤ n 1 + n 2 , n 1 = n 2 = 0, so s ′ 1 = π L (o),
guage (G, O, S, π ′ L , π ′ R , π L , π R , I) , ∀g : G, ∀o : O, I(g, o) ⇒ (π ′ L (g), π L (o)) → * ̸ → ⇒ (π ′ R (g), π R (o)) → * ̸ → ⇒ ∃ n o ′ , S n (g, o) = o ′ ∧ I(g, o ′ ) ∧ π L (o ′ ) ̸ → ∧ π R (o ′ ) ̸ →
That is, for every oracle global environment g and every oracle state o on which the oracle's invariant I holds and that can be projected to left and right configurations resulting both in converging executions, o reduces to a final oracle state o ′ after a finite number of reduction steps.

Proof. This theorem is a direct consequence of Theorem 3.

Chapter 4

Oracle languages for Imp

While we have defined two generic oracle languages in the previous chapter, most informative oracle languages are specific to a pair of programming languages. For this reason, we have designed a collection of oracle languages on the idealized imperative language Imp presented in the previous chapter.

The choice of Imp over Imp br as a target language can be explained by our focus moving from studying extensional relational properties to intensional ones: indeed, such a change in focus also implied a change from a big-step presentation of the semantics to a small-step operational semantics. Since the early exit constructs of Imp br would have made the small-step semantics noticeably more complex for no fundamental benefit, we dropped them in the process for simplicity's sake.

The different oracle languages we have defined on Imp constitute a first practical exploration of the language design questions arising from our framework, as well as a first informal evaluation of its expressivity. As such, each of those oracle languages corresponds to a specific class of differences, demonstrating different capabilities of the framework. For instance, some of those oracle languages describe pairs of programs that perform exactly the same number of reduction steps, with each pair of configurations tightly related. This would be the case of an oracle language relating programs that are equal modulo renaming of variable identifiers, for instance. Other oracle languages abstract several computation steps in order to reach a related pair of program configurations, which may be needed to describe more involved code refactoring or optimizations. Finally, some of those oracle languages will describe pairs of extensionally-equivalent programs while others will relate pairs of programs presenting different outcomes.

It must be noted that, when designing those oracle languages, our main preoccupation was to figure out what kind of changes could be represented and how. Furthermore, as each of those oracle languages has been fully formalized in the Coq proof assistant, some compromises had to be made to keep the quantity and difficulty of proofs manageable when exploring different possibilities for oracle languages. As a result, the oracle languages presented in the chapter may not be the most practical or generic possible for the kinds of changes they describe.

63

While we have already defined Imp's big-step semantics, our framework requires small-step semantics. The small-step semantics of Imp is defined on states,-that is, pairs of a store S and a continuation κ-using big-step evaluation for expressions and boolean expressions: Definition 17 (Imp states).

S Imp ::= (κ, S) κ ::

= halt | c • κ
Just as with the big-step semantics defined earlier, a store S is a partial map from variable identifiers to integer values. In addition, a program state S Imp also includes a continuation κ, that is a stack of statements to be executed next, with the very next statement on the top of the stack.

Definition 18 (Imp transition function). The semantics is then defined on states by the following transition function E Imp , interpreting the statement on the top of the continuation stack:

• When the statement at the top of the stack is a skip, it is discarded without modifying the store:

E Imp (skip • κ, S) = (κ, S)
• When that statement is an assignment, it is removed from the stack, the righthand-side expression is evaluated in the current store and the result is stored in the variable x. If the right-hand-side expression cannot be evaluated in the current store, the program crashes:

E Imp (x = e • κ, S) = (κ, S[x ↦ → n])
where S ⊢ e ⇓ n

• If the head statement is a sequence, it is unfolded. That is, it is removed from the stack, and the two sub-statements are pushed in its place:

E Imp ((c 1 ; c 2 ) • κ, S) = (c 1 • (c 2 • κ), S)
• When the head statement is a conditional, it is removed from the continuation, and the condition expression is evaluated in the current store. If it cannot be evaluated, the program crashes. Otherwise, the sub-statement corresponding to the appropriate branch is pushed on the stack:

E Imp (if (b) c 1 else c 2 • κ, S) = (c 1 • κ, S) where S ⊢ b ⇓ true E Imp (if (b) c 1 else c 2 • κ, S) = (c 2 • κ, S)
where S ⊢ b ⇓ false

• Upon encountering a while statement, its condition is evaluated in the current store. If the condition cannot be evaluated, the program crashes. If it evaluates to true, the loop's body is pushed onto the stack. If it evaluates to false, the loop is removed from the stack:

E Imp (while (b) c • κ, S) = (c • (while (b) c • κ), S) where S ⊢ b ⇓ true E Imp (while (b) c • κ, S) = (κ, S)
where S ⊢ b ⇓ false

• Finally, when an assert statement is encountered, its boolean expression is evaluated. If it does not evaluate to true, the program crashes. Otherwise, the statement is simply popped from the stack:

E Imp (assert (b) • κ, S) = (κ, S)
where S ⊢ b ⇓ true Lemma 9 (Small-step and big-step semantics for Imp are equivalent). This small-step definition is equivalent to the big-step presentation defined earlier, that is, every finite execution of a single statement in a given store S results in the same store S ′ whether it is considered through the small-step semantics or the big-step one:

∀S S ′ c, S ⊢ c ⇓ S ′ ⇔ ∃n, E n Imp (c • halt, S) = (halt, S ′ )
Now that we have given Imp a deterministic small-step semantics, we can use it in our framework.

Definition 19 (Imp programming language definition). The language definition for Imp is given by the tuple L Imp = (c, unit, S Imp , I Imp , E ′ Imp , unit, F Imp ) where

• unit is the unit type with a single inhabitant tt • c is the type of Imp abstract syntax trees as defined in Chapter 2

• E ′ Imp (_, S Imp ) = E Imp (S Imp ) • F Imp ((halt, S)) = tt • I Imp (c) = (c • halt, ∅)
Notice that the semantics of Imp does not involve any global environment, as everything needed is included in its dynamic state. For that reason, the definition L Imp makes use of the type unit as its global environment type, as it has only one inhabitant tt. Its step function E ′ Imp is a light wrapper around E Imp in order to accomodate for the global environment, which is discarded as it does not hold information. An Imp program is considered to be terminated (without errors) if it has reached a configuration with an empty continuation. As Imp programs do not have proper return values, their return type is also unit.

In the following sections, we will go through all of the Imp-specific oracle languages we have defined in our Coq development. While those different oracles tackle various challenges and are only loosely related to each other, we attempt to maintain a progression in our presentation. Indeed, we will start from the conceptually simpler oracles, and we will try to present them in an order such that each presented language will only introduce a minimal number of new difficulties and proof techniques.

The Coq development itself will be presented in a more hands-on way in Chapter 7.

Renaming

One simple yet informative Imp-specific class of differences is that of valid renamings (akin to α-renaming in λ-calculus). Informally, a renaming is a syntactic operation replacing all occurrences of some variable identifier in a program by another variable identifier.

Example 5. The following pair of programs, in which the variable "a " from the left program has been renamed to "s u m " in the second one, illustrates such a change:

a = 0 ; d = x ; w h i l e ( 0 < d ) { i f ( x % d = = 0 ) a = a + d ; d = d - 1 ; } s u m = 0 ; d = x ; w h i l e ( 0 < d ) { i f ( x % d = = 0 ) s u m = s u m + d ; d = d - 1 ;

}

In order for the modified program to preserve the semantics of the original program,-in the sense that every step should yield the same results modulo variable renaming-renamed variables must not conflict with other variables: if two variables were distinct before the renaming, they have to be distinct after the renaming. We decided to represent renaming operations by a bijection between variable identifiers, as bijections avoid such conflicts.

Definition 20 (R e n a m i n g language on Imp). The renaming oracle language R e n a m i n g 1 on Imp is defined by the oracle language definition (G ren , S Imp × S Imp , S ren , 1 tt , 1 tt , f st, snd, I ren ) where:

• 1 tt (_) = tt is the constant function returning tt • G ren is the set of bijections from variable identifiers to variable identifiers • I ren (φ, (s 1 , s 2 )) holds iff φ(s 1 ) = s 2 , where φ(s 1 ) is the term obtained by replacing every variable identifier x by φ(x

) in s 1 • S ren (tt, (s 1 , s 2 )) = (s ′ 1 , s ′ 2 ) if E Imp (s 1 ) = s ′ 1 and E Imp (s 2 ) = s ′ 2
The oracles written in this language thus relate pairs of programs that are renamings of one another, having exactly the same number of execution steps, yielding at each point pairs of configurations that are equivalent modulo renaming.

Control-flow-preserving value changes

Another useful class of differences on Imp is the class of pairs of programs which share the exact same dynamic control-flow while allowing differing values for a given set of variable identifiers. The oracle language V a l u e C h a n g e describes a subset of such differences, restricted to pairs of programs matching an easily-checkable syntactic criterion. Informally, this criterion requires that:

1 from the name of the Coq module implementing this oracle language.

1. Potentially modified variables cannot appear in conditionals. 2. Programs can only differ on assignments of modified variables. 3. In order to avoid both programs having different crashing behaviors, modified assignments must feature the same set of variable identifiers and divisor expressions. 4. Whenever a potentially modified variable appears in the right-hand side of an assignment, that assignment's left-hand side must also be considered as a potentially modified variable. Example 6. One example pair of programs that can be related using this oracle language is the following, where the right program is syntactically identical to the left one except for the initial assignment of the variable x : The exact criterion defined on continuations is captured by the judgment "c 1 ≡ x c 2 " stating that c 1 and c 2 have the same control flow and may only differ in the value of variable identifiers included in x. This judgment is formally defined in Definition 21 (V a l u e C h a n g e language on Imp). The oracle language V a l u e C h a n g e of control-flow-preserving value changes in Imp programs is defined by the oracle language definition

x = 4
(G V C , S Imp × S Imp , S V C , 1 tt , 1 tt , f st, snd, I V C ) where: • G V C is the set of lists of variable identifiers • I V C (x, ((κ 1 , S 1 ), (κ 2 , S 2 ))) = κ 1 ≡ x κ 2 ∧ dom(S 1 ) = dom(S 2 ) ∧ ∀x ̸ ∈ x ⇒ S 1 (x) = S 2 (x) • S V C (tt, (s 1 , s 2 )) = (s ′ 1 , s ′ 2 ) if E Imp (s 1 ) = s ′ 1 and E Imp (s 2 ) = s ′ 2 Control-Skip skip ≡ x skip Control-Seq c 1 1 ≡ x c 2 1 c 1 2 ≡ x c 2 2 c 1 1 ; c 1 2 ≡ x c 2 1 ; c 2 2 Control-If c 1 1 ≡ x c 2 1 c 1 2 ≡ x c 2 2 ∀ y, y ∈ vars(b) ⇒ y ̸ ∈ x if (b) c 1 1 else c 1 2 ≡ x if (b) c 2 1 else c 2 2 Control-While c 1 ≡ x c 2 ∀ y, y ∈ vars(b) ⇒ y ̸ ∈ x while (b) c 1 ≡ x while (b) c 2
c 1 ≡ x c 2 c 1 • κ 1 ≡ x c 2 • κ 2
where, informally, vars(e) is the set of variable identifiers appearing in e and divs(e) is the set of divisor expressions appearing in e. The formal definition of vars and divs can be found in the Coq development. As one can see, the definition of V a l u e C h a n g e 's step function is straightforward, as it simply interprets the two programs in lockstep, without maintaining any additional information. Its invariant, however, is slightly more involved: in addition to stating that the two programs' continuations are related by the criterion discussed above, it also requires the two programs' stores to contain exactly the same variable identifiers, in order to ensure that, should an expression contain an unknown variable identifier, its evaluation will cause both programs to crash. In addition, variables are only allowed to have different values if they are listed as potentially modified variables, in order to ensure possible effects on the control flow are properly tracked.

It must be noted that the judgment κ 1 ≡ x κ 2 is very restrictive. In particular, the list of variables allowed to change is global, meaning that dependence propagation between variables does not only go forward but also backward.

The reason for this unusual restriction boils down to a compromise between capturing interesting changes and keeping the Coq proof manageable.

Branches swapping

The oracle language S w a p B r a n c h e s for branches swapping describes pairs of programs identical except for swapped "then" and "else" branches of conditionals which have their condition negated. The affected conditional statements are identified by their path in the abstract syntax tree of the programs under consideration. Such oracles may seem exceedingly simple, as they execute both programs in lock-step, yielding identical stores for both programs at each step. However, unlike every other oracle language we have presented so far, S w a p B r a n c h e s describes changes that are local in nature. Indeed, branch swaps only affect a handful of reduction steps: those where the head term is the modified conditional. As a consequence, in order to track when the those reductions take place, S w a p B r a n c h e s maintains some dynamic information in addition to a copy of both programs' configurations. This pattern of dynamically tracking syntactic changes will be reused in many of our other oracle languages. Example 7. One example pair of programs that can be related using this oracle language is: As hinted earlier, in order to perform the branch swap at the appropriate time, the oracle needs to do some bookkeeping to find out when the affected conditionals are encountered. This is done by maintaining a data structure mimicking the shape of the continuations of the programs under comparison: that data structure is a list of changes to be performed on the continuation or on statements at a given point of the execution. Because this pattern will be common to several other oracle languages, this structure is parametric in the actual type of changes to be applied to statements and continuations: Definition 22 (Dynamic modifier structure on Imp). For a given type α of actual statement-level changes and a type β of actual continuation-level changes, Imp dynamic modifiers are defined by the following syntax:

i f ( x < y ) r e s u l t = x + 4 2 ;
δc ::= ∆ L e a f (α) | I d | ∆ R e c (δc, δc) δκ ::= ∆ c (δc) | ∆ κ (β)
That is, a statement modifier δc defines a tree where leaves are either the identity modification I d or an actual statement-level modifier α, while a continuation modifier δκ defines either a continuation-level modifier β or a statement modifier δc that applies to the statement on top of a continuation. This continuation modifier structure is manipulated by the S H e l p e r helper function of type S Imp → S Imp → δc → δκ ↦ → step_helper_res, which executes the left and right programs in lockstep whenever the continuation modifier indicates a local identity, maintaining the continuation modifier in the process. Whenever the head term of the continuation modifier is an actual statement-level or continuation-level change, a special value is returned to signify that local change has to be handled specifically. This helper function is a partial function which is not defined when the two programs under comparison do not reduce using the same reduction rule although they are expected to be locally identical. As with the continuation modifier structure,

S H e l p e r will be reused in different oracle languages and is therefore parametric in the type of actual changes to be applied to statements and continuations.

Definition 23 (S H e l p e r return type). For a given type α of actual statement-level changes and a type β of actual continuation-level changes, the result type of the S H e l p e r function is the following algebraic abstract data type:

step_helper_res ::= GStep S Imp S Imp δκ | SCmdStep α δκ | SContStep β δκ | Stuck
Those four constructors represent different possible outcomes of executing the two programs according to a continuation modifier list: GStep s 1 s 2 δκ represents the result of a successful lock-step execution step leading to the pair of configurations (s 1 , s 2 ) and a remaining continuation modifier δκ, Stuck is returned when the two programs are both stuck, and the other cases are returned when an actual statement-level or continuation-level change is to be handled, requiring special action from the caller.

Definition 24 (S H e l p e r step helper). We do not give here the full formal definition of S H e l p e r as to not clutter this manuscript with its many cases, but we will only give a partial, semi-formal definition to convey how this function works. As always, the full definition is available in the Coq development.

S H e l p e r ((skip

• κ 1 , S 1 ), (skip • κ 2 , S 2 ), ∆ c (I d ), δκ) = GStep (κ 1 , S 1 ) (κ 2 , S 2 ) δκ S H e l p e r ((c 1 1 ; c 2 1 • κ 1 , S 1 ), (c 1 2 ; c 2 2 • κ 2 , S 2 ), ∆ c ((∆ R e c (α, α ′ ))), δκ) = GStep (c 1 1 • c 2 1 • κ 1 , S 1 ) (c 1 2 • c 2 2 • κ 2 , S 2 ) (α :: α ′ :: δκ) . . . S H e l p e r (s 1 , s 2 , ∆ c ((∆ L e a f (α))), δκ) = SCmdStep α δκ S H e l p e r (s 1 , s 2 , ∆ κ (β), δκ) = SContStep β δκ
The first two cases above illustrate the lockstep execution of the two programs when they are locally identical: S H e l p e r takes care of stepping in both programs and updating the continuation modifier structure. In the last two cases, the head term of the continuation modifier structure indicates a change that must be handled by the oracle language.

Note that the S H e l p e r is undefined whenever the continuation modifier indicates a lockstep execution but the programs do not actually perform the same reduction step.

For instance, neither of the following cases is defined:

S H e l p e r ((skip

• halt, ∅), (x = e • halt, ∅), ∆ c (I d ), _) S H e l p e r ((if (x ≤ 42) skip else skip • halt, ∅[x ↦ → 0]), (if (x ≤ 42) skip else skip • halt, ∅[x ↦ → 50]), ∆ c (I d ), _)
Since S w a p B r a n c h e s executes programs in lockstep, continuation-level changes are not needed, and the S w a p B r a n c h e s oracle language definitions thus make use of S H e l p e r with the empty type for the type β of actual continuation-level changes. The type α of actual statement-level changes is defined as a sum type with two constructors: N e g a t e and U n N e g a t e . While they do not actually appear in the semantics of S w a p B r a n c h e s , they are used in its invariant property and its soundness proof.

Definition 25 (S w a p B r a n c h e s language on Imp). The oracle language S w a p B r a n c h e s of branches swapping is defined by the oracle language definition (unit, S Imp × S Imp × δκ, S SB , 1 tt , 1 tt , f st, snd, I SB )

where:

• I SB (tt, (s 1 , s 2 , km)) holds if s 1 and s 2 's continuations are indeed related by km (the details are omitted in this already lengthy description but can be found in the Coq development)

• S SB (tt, (s 1 , s 2 , m • km))

= ⎧ ⎪ ⎪ ⎪ ⎪ ⎪ ⎨ ⎪ ⎪ ⎪ ⎪ ⎪ ⎩ (s ′ 1 , s ′ 2 , km ′ ) if S H e l p e r (s 1 , s 2 , m, km) = GStep s ′ 1 s ′ 2 km ′ (s ′ 1 , s ′ 2 , km ′ ) if S H e l p e r (s 1 , s 2 , m, km) = SCmdStep α km ′ and E Imp (s 1 ) = s ′ 1 and E Imp (s 2 ) = s ′ 2
Truth be told, the branch swapping oracle's step function S SB could be much simpler, since it simulates both programs in lockstep. Indeed, S SB could be defined exactly as the renaming oracle's step function S ren . Instead, we opted for storing additional information in the oracle states, thus requiring a more complex step function to maintain it. Indeed, the additional information stored in the oracle state allows for a more direct and precise definition of the invariant, as doing otherwise would have required the invariant to rely on existentially-quantified variables holding similar information.

One may wonder why we have not defined a "generic invariant" to be used with the S H e l p e r function. The reason for that is that while using S H e l p e r avoids a lot of boilerplate code, the generic part of related invariants is exceedingly simple, and using a generic construct would only add overhead. As for invariant preservation and correctness proof, they are very much dependent on the specifics of each oracle language.

Refactoring branches with common code

Another class of syntactic changes between extensionally-equivalent programs is the class of changes consisting in deduplicating code that is ending both the then and else branches of a conditional by moving it after that conditional. This class of changes is encoded by the R e f a c t o r C o m m o n B r a n c h R e m a i n d e r oracle language, the second oracle language to make use of the S H e l p e r function defined in the previous section, and the first occasionally simulating multiple steps of both programs within a single oracle step.

Example 8.

One example of such a pair of programs that can be related by The relation between the two programs' execution traces is a bit trickier than the ones we have defined so far: indeed, instead of always simulating a single step of each program, it will occasionally perform two steps at once in both programs in order to skip locally-different execution steps and synchronize to locally-related ones. This occurs when the left configuration's head term is the if statement that gets refactored and the right configuration's head term is a sequence of the if statement and the common remainder. Simulating multiple steps of each program in a single oracle step is made possible thanks to the existentially-quantified variables n 1 and n 2 in the oracle soundness property from definition 14: ∀g : G, ∀ss ′ : O,

i f ( x < y ) { a = x + 4 2 ; a = a
I(g, s) ⇒ S(s) = s ′ ⇒ ∃ n 1 n 2 , ⎧ ⎪ ⎨ ⎪ ⎩ π L (S(s)) = E n 1 L 1 (π ′ L (g), π L (s)) π R (S(s)) = E n 2 L 2 (π ′ R (g), π R (s)) n 1 + n 2 > 0 Example 9.
To illustrate this, let us consider the following execution-where, for the sake of clarity, stores are omitted and only the continuation is displayed:

if (b) {c 1 ; c ′ } else {c 2 ; c ′ } • κ 1 c 1 ; c ′ • κ 1 c 1 • c ′ • κ 1 O 1 O 2 if (b) c 1 else c 2 ; c ′ • κ 2 if (b) c 1 else c 2 • c ′ • κ 2 c 1 • c ′ • κ 2 π L π R π L π R
In this case, a single oracle step from O 1 simulates two steps in both the left and right programs, so that the states projected from O 2 have the same shape and lock-step execution can be resumed.

Lastly, there is a corner case that must be addressed: when performing those two steps, both programs may crash after a different number of steps when evaluating the if statement's condition: the left program will be immediately stuck while the right program will be stuck after a single step. Since a correct oracle is required to step both programs to their end whenever those programs are finite, the R e f a c t o r C o m m o n B r a n c h R e m a i n d e r oracle language must handle this situation by returning both programs' stuck state. That means that, not only does the oracle step function not always perform exactly one step of each program, it may also perform a different number of steps in both programs whenever they crash, as in the following example diagram, where b cannot be evaluated, causing the left and right programs to be stuck after a different number of reduction steps: (unit, S Imp × S Imp × δκ + S Imp × S Imp , S RCBR , 1 tt , 1 tt , f st, snd, I RCBR )

if (b) {c 1 ; c ′ } else {c 2 ; c ′ } • κ 1 O 1 O 2 if (b) c 1 else c 2 ; c ′ • κ 2 if (b) c 1 else c 2 • c ′ • κ 2 ̸ π L π R π R ̸ π L Like the S
where:

• I RCBR (tt, (s 1 , s 2 , km)) holds if s 1 and s 2 's continuations are indeed related by km (the details are omitted in this already lengthy description but can be found in the Coq development)

• I RCBR (tt, (s 1 , s 2 )) holds if s 1 ̸ → and s 2 ̸ → • S RCBR (tt, (s 1 , s 2 , m • km)) = ⎧ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎨ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎩ (s ′ 1 , s ′ 2 , km ′ ) if S H e l p e r (s 1 , s 2 , m, km) = GStep s ′ 1 s ′ 2 km ′ (s ′ 1 , s ′ 2 , (∆ c (I d )) :: (∆ c (I d )) :: km ′ ) if S H e l p e r (s 1 , s 2 , m, km) = SCmdStep α km ′ and E Imp (E Imp (s 1 )) = s ′ 1 and E Imp (E Imp (s 2 )) = s ′ 2 (s 1 , s ′ 2 ) if S H e l p e r (s 1 , s 2 , m, km) = SCmdStep α km ′ and s 1 ̸ → and E Imp (s 2 ) = s ′ 2
Remark. The reader may have noticed an unusual and unexplained limitation imposed by this oracle language: indeed, each branch of the original program must be a sequence of a particular shape, with the code specific to that branch on the left side of the sequence, and the code common to both branches on the right side. These restrictions on the programs' shape are common in our oracle languages as they significantly simplify their presentation. Those restrictions do not reduce the expressive power of such languages, thanks to the S e q A s s o c oracle language presented next.

Sequence Associativity

It must be noted that in our definition of Imp, programs are trees of statements, rather than lists of statements: (c 1 ; c 2 ); c 3 and c 1 ; (c 2 ; c 3 ) are not syntactically equal, but they are equivalent, as sequence in Imp is associative. While this class of differences is not directly useful to programmers, it is required nonetheless for formal reasoning. Indeed, other oracle languages, such as the R e f a c t o r C o m m o n B r a n c h R e m a i n d e r oracle language defined in the previous section, will often require specific ways of parenthesizing sequences. Therefore, having oracles to transform programs that do not conform to those parenthesizing schemes is useful. The oracle language representing reparenthesizing of sequences, S e q A s s o c , is also, with R e f a c t o r C o m m o n B r a n c h R e m a i n d e r , one of the simplest that does not feature lock-step execution. Indeed, as unfolding a sequence is a small execution step on its own, two identical programs modulo sequence associativity will not necessarily execute their effectful statements after the same number of steps. For instance, the assignment statement will not be executed after the same number of steps in the two following programs: (x = e; c 2 ); c 3 and x = e; (c 2 ; c 3 ).

Indeed, in the first case, the assignment is performed in the third reduction step, while it is performed in the second reduction step in the second program.

To address this, the S e q A s s o c oracles will simulate a different number of steps in the left and right programs when encountering this pattern.

(c 1 ; c 2 ); c 3 • κ 1 c 1 ; c 2 • c 3 • κ 1 c 1 • c 2 • c 3 • κ 1 O 1 c 1 ; (c 2 ; c 3 ) • κ 2 c 1 • c 2 ; c 3 • κ 2 π L π R O 2 π L π R
To this end, the S e q A s s o c oracle makes use of the S H e l p e r function to keep track of the execution points where those changes have to be applied. This is a bit more complex as in the previous oracles since the program that has been "stepped once" needs to be "stepped twice" at a later point to perform the matching sequence unfolding.

(c 1 ; c 2 ); c 3 • κ 1 c 1 ; c 2 • c 3 • κ 1 c 1 • c 2 • c 3 • κ 1 c 2 • c 3 • κ 1 O 1 O n+1 c 1 ; (c 2 ; c 3 ) • κ 2 c 1 • c 2 ; c 3 • κ 2 c 2 ; c 3 • κ 2 c 2 • c 3 • κ 2 π L π R π L π R O 2 O n π L π R π L π R ••• ••• •••
To do so, the S e q A s s o c oracle languages defines a type of actual statement-level changes for the "sequence unfolding" operation and the "sequence folding" operation along with two corresponding continuation-level changes:

• The statement-level change type is defined as α = U S e q | F S e q . U S e q describes the transformation from (c 1 ; c 2 ); c 3 to c 1 ; (c 2 ; c 3 ) while F S e q represents the opposite transformation.

• The continuation-level change type is defined as To illustrate how this modifier structure is used by the S e q A s s o c oracle language, consider this version of the previous diagram, in which oracle states are replaced with their modifier structure-abusively writing x for ∆ κ (x) and y for ∆ c (y) in order to make the diagram more readable:

β = U L | U R . When U L is
(c 1 ; c 2 ); c 3 • κ 1 c 1 ; c 2 • c 3 • κ 1 c 1 • c 2 • c 3 • κ 1 c 2 • c 3 • κ 1
∆ L e a f (U S e q ) :: km ′ I d ::

I d :: km ′ c 1 ; (c 2 ; c 3 ) • κ 2 c 1 • c 2 ; c 3 • κ 2 c 2 ; c 3 • κ 2 c 2 • c 3 • κ 2 π L π R π L π R I d :: U R :: km ′ U R :: km ′ π L π R π L π R ••• ••• •••
Definition 27 (S e q A s s o c language on Imp). The oracle language S e q A s s o c on Imp is defined by the oracle language definition (unit, S Imp × S Imp × δκ, S SA , 1 tt , 1 tt , f st, snd, I SA )

where:

• I SA (tt, (s 1 , s 2 , km)) holds if s 1 and s 2 's continuations are indeed related by km (the details are omitted in this already lengthy description but can be found in the Coq development)

• S SA (tt, (s 1 , s 2 , m • km)) = ⎧ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎨ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎩ (s ′ 1 , s ′ 2 , km ′ ) if S H e l p e r (s 1 , s 2 , m, km) = GStep s ′ 1 s ′ 2 km ′ (s ′ 1 , s ′ 2 , ∆ c (I d ) :: ∆ κ (U R ) :: km ′ ) if S H e l p e r (s 1 , s 2 , m, km) = SCmdStep U S e q km ′ and E Imp (E Imp (s 1 )) = s ′ 1 and E Imp (s 2 ) = s ′ 2 (s ′ 1 , s ′ 2 , ∆ c (I d ) :: ∆ κ (U L ) :: km ′ ) if S H e l p e r (s 1 , s 2 , m, km) = SCmdStep F S e q km ′ and E Imp (s 1 ) = s ′ 1 and E Imp (E Imp (s 2 )) = s ′ 2 (s ′ 1 , s 2 , ∆ c (I d ) :: ∆ c (I d ) :: km ′ ) if S H e l p e r (s 1 , s 2 , m, km) = SContStep U L km ′ and E Imp (s 1 ) = s ′ 1 (s 1 , s ′ 2 , ∆ c (I d ) :: ∆ c (I d ) :: km ′ ) if S H e l p e r (s 1 , s 2 , m, km) = SContStep U R km ′ and E Imp (s 2 ) = s ′ 2

Independent assignments swapping

The oracle language S w a p A s s i g n for independent assignments swapping describes the pairs of programs obtained by swapping two adjacent independent assignments. This is yet another oracle language for extensionally-equivalent programs, simulating them mostly in lock-step except for the precise execution points where the two assignments are to be swapped. S w a p A s s i g n does not make use of any new technique in its definition or proofs.

Example 10.

An example of programs that can be related by a S w a p A s s i g n oracle is the following pair of programs, in which the two assignments in the loop's body have been swapped:

a = 1 0 ; x = 2 ; w h i l e ( 0 < = a ) { x = 4 2 * x ; a = a - 1 ; } a = 1 0 ; x = 2 ; w h i l e ( 0 < = a ) { a = a - 1 ; x = 4 2 * x ;
} Oracles of the S w a p A s s i g n oracle language behave by executing the two programs in lockstep until they reach a sequence of two independent assignments that are swapped in both programs. To do so, they rely on the S H e l p e r function with the singleton type unit for both the type α of actual statement-level changes and the type β of actual continuation-level changes. Indeed, there is only one way to swap two adjacent independent assignments. The statement-level modifier is meant to syntactically track the sequence containing the two assignments to swap. When that point is reached, S w a p A s s i g n oracles will perform a single step of both programs-unfolding the head sequence-and pushing a continuation modifier on top of the continuation modifier structure to indicate that the two assignments at the head of the continuations are to be swapped. The next oracle step will then simulate two steps of both the left and right programs. This is illustrated by the following diagram:

x = e; y = e ′ • κ 1 x = e • y = e ′ • κ 1 y = e ′ • κ 1 κ 1 O 1 O 2 O 3 y = e ′ ; x = e • κ 2 y = e ′ • x = e • κ 2 x = e • κ 2 κ 2 π L π R π L π R π L π R As with
x = e; y = e ′ • κ 1 x = e • y = e ′ • κ 1 O 1 O 2 y = e ′ ; x = e • κ 2 y = e ′ • x = e • κ 2 x = e • κ 2 ̸ π L π R π L π R ̸ O 3 π L π R
Since the assignments are swapped, e is evaluated first in the left program, and second in the right program, causing them to get stuck after a different number of steps.

Much like with R e f a c t o r C o m m o n B r a n c h R e m a i n d e r , the type for S w a p A s s i g n dynamic states is a sum type with two constructors: one for regular states and one for crashed states.

Definition 28 (S w a p A s s i g n language on Imp). The oracle language S w a p A s s i g n on Imp is defined by the oracle language definition (unit, S Imp × S Imp × δκ + S Imp × S Imp , S SwA , 1 tt , 1 tt , f st, snd, I SwA ) where:

• I SwA (tt, (s 1 , s 2 , km)) holds if s 1 and s 2 's continuations are indeed related by km (the details are omitted in this already lengthy description but can be found in the Coq development)

• I SwA (tt, (s 1 , s 2 )) holds if s 1 ̸ → and s 2 ̸ → • S SwA (tt, (s 1 , s 2 , m • km)) = ⎧ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎨ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎩ (s ′ 1 , s ′ 2 , km ′ ) if S H e l p e r (s 1 , s 2 , m, km) = GStep s ′ 1 s ′ 2 km ′ (s ′ 1 , s ′ 2 , ∆ κ (tt) :: km ′ ) if S H e l p e r (s 1 , s 2 , m, km) = SCmdStep tt km ′ and E Imp (s 1 ) = s ′ 1 and E Imp (s 2 ) = s ′ 2 (s ′ 1 , s ′ 2 , km ′ ) if S H e l p e r (s 1 , s 2 , m, km) = SContStep tt km ′ and E Imp (s 1 ) = s ′ 1 and E Imp (s 2 ) = s ′ 2 (s 1 , s ′ 2 ) if S H e l p e r (s 1 , s 2 , m, km) = SContStep tt km ′ and s 1 ̸ → and E Imp (s 2 ) = s ′ 2 (s ′ 1 , s 2 ) if S H e l p e r (s 1 , s 2 , m, km) = SContStep tt km ′ and E Imp (s 1 ) = s ′ 1 and s 2 ̸ →
In the above definition, lockstep execution is handled by S H e l p e r . A statement-level modifier causes the oracle to perform a single step-unfolding the head sequence-and add a marker at the top of the continuation modifier structure. Such a continuationlevel marker causes the oracle to perform two steps at once in both programs. If evaluating those steps fails, the oracle switches to the second oracle state constructor signifying a stuck state.

Contextual equivalence

The oracle language A b s t r a c t E q u i v of abstract equivalences describes pairs of programs that are syntactically equal except for two terminating extensionally-equivalent sub-programs. While this oracle language is very powerful, it offloads the termination and equivalence proofs of the sub-programs to external proofs. Although this somewhat reduces the usefulness of such an oracle language, A b s t r a c t E q u i v provides a first illustration of how to integrate external extensional properties within our framework.

Example 11. For instance, consider the following pair of programs, which only differ by the last two assignments in the loop's body:

As with the last few oracle languages presented, A b s t r a c t E q u i v uses the S H e l p e r function to simulate the syntactically-equal portion of the two equivalent programs in a lockstep fashion. Then, whenever it encounters the two extensionally-equivalent but syntactically distinct subprograms, it invokes the (constructive) proof of termination of both subprograms to recover the resulting store (in case of a successful execution) or a bound on the number of steps needed to reach a crashing state. In the former case, that is, when the subprograms execute without errors, the oracle effectively skips the intermediate steps thanks to the provided external proof. In the case the subprograms do crash, the oracle performs as many steps as needed to reach the crashing configuration and switches to a distinguished stuck state as with S w a p A s s i g n or R e f a c t o r C o m m o n B r a n c h R e m a i n d e r .

More specifically, A b s t r a c t E q u i v uses S H e l p e r with the empty type as the type β of actual continuation-level changes, and the type α of actual statement-level changes is the product type c × c × (S → S + N) × (S → S + N) of quadruples (c 1 , c 2 , f 1 , f 2 ) such that f 1 (respectively f 2 ) describes the execution of c 1 (respectively f 2 ) in a given store, by returning the resulting store in case of successful execution, or a bound on the number of steps required to reach a stuck state otherwise. Furthermore, f 1 and f 2 must return equivalent results on equivalent input: whenever one returns a store, the other must return an equivalent store, and whenever one indicates a stuck state, the other one must also indicate a stuck state. For conciseness, those additional restrictions are omitted from the quadruples in this presentation, but they are in fact part of the data type used in the Coq development.

The following diagram illustrates how two non-crashing programs are related by an A b s t r a c t E q u i v oracle. In order to make the diagram more readable, stores are omitted, and oracle states are replaced with their modifier structure:

x = e • c 1 • κ 1 c 1 • κ 1 κ 1 I d :: ∆ c (c 1 , c 2 , f 1 , f 2 ) :: km ∆ c (c 1 , c 2 , f 1 , f 2 ) :: km km x = e • c 2 • κ 2 c 2 • κ 2 κ 2 π L π R π L π R π L π R ••• •••
In the above diagram, once the oracle reaches a state where the statement-level change (c 1 , c 2 , f 1 , f 2 ) is on the top of the continuation modifier structure, it simulates multiple steps of both programs by calling f 1 and f 2 .

The type of A b s t r a c t E q u i v oracle states is actually a sum type to allow for crashed states, much like S w a p A s s i g n and other oracle languages.

Definition 29 (A b s t r a c t E q u i v language on Imp). The oracle language A b s t r a c t E q u i v on Imp is defined by the oracle language definition

(unit, S Imp × S Imp × δκ + S Imp × S Imp , S AE , 1 tt , 1 tt , f st, snd, I AE )
where:

• I AE (tt, (s 1 , s 2 , km)) holds if s 1 and s 2 's continuations are indeed related by km (the details are omitted in this already lengthy description but can be found in the Coq development)

• I AE (tt, (s 1 , s 2 )) holds if s 1 ̸ → and s 2 ̸ → • S AE (tt, (s 1 , s 2 , m • km)) = ⎧ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎨ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎩ (s ′ 1 , s ′ 2 , km ′ ) if S H e l p e r (s 1 , s 2 , m, km) = GStep s ′ 1 s ′ 2 km ′ (s ′ 1 , s ′ 2 , km ′ ) if S H e l p e r ((c 1 • κ 1 , S 1 ), (c 2 • κ 2 , S 2 ), m, km) = SCmdStep (c 1 , c 2 , f 1 , f 2 ) km ′ and s ′ 1 = (κ 1 , f 1 (S 1 )) and s ′ 2 = (κ 2 , f 2 (S 2 )) (s ′ 1 , s ′ 2 )
if S H e l p e r ((c

1 • κ 1 , S 1 ), (c 2 • κ 2 , S 2 ), m, km) = SCmdStep (c 1 , c 2 , f 1 , f 2 ) km ′ and f 1 (S 1 ) = n and f 2 (S 2 ) = m and ∃n ′ ≤ n, E n ′ Imp ((c 1 • κ 1 , S 1 )) = s ′ 1 ∧ s ′ 1 ̸ ∈ dom(E Imp ) and ∃m ′ ≤ m, E m ′ Imp ((c 2 • κ 2 , S 2 )) = s ′ 2 ∧ s ′ 2 ̸ ∈ dom(E Imp )

Crash-avoiding conditionals

As discussed multiple times in this thesis, without illustration so far, our framework enables reasoning about programs that crash. The C r a s h F i x oracle language performs this kind of reasoning by describing pairs of programs where one is known to crash under certain conditions and the other avoids such conditions by adding a "defensive" if statement.

Example 12. The two following programs illustrate such a situation, with the assignment y = 4 2 % x causing the left program to crash if v is 0, while this assignment is guarded by a conditional statement in the right program:

x = v ; y = 4 2 % x ; z = x + y ; x = v ; i f ( x ! = 0 ) y = 4 2 % x ;
e l s e

y = 0 ; z = x + y ;
Informally, a C r a s h F i x oracle simulates the two programs in lockstep until the potentially crash-inducing statement is reached. Then, it evaluates the newly-introduced guard condition. If evaluating the guard fails, then both programs crash. If the guard evaluates to true, then, the oracle simulates a single step of the "fixed" program to unfold the conditional so that lockstep evaluation of the two programs can be resumed. Finally, if the guard evaluates to false, the oracle simulates a single step of the "fixed" program to unfold the conditional, and as many steps of the left program as needed for it to reach a crashed state. As the oracle step function is a Coq function, it is required to provably terminate, and therefore requires a bound on the number of steps needed to reach a stuck state to be provided by an external proof. Once a crashed state for the left program has been reached, subsequent reduction steps of the oracle will only step in the right program.

For instance, consider the following diagram-in which stores are omitted and oracle states' details are not shown-illustrating the successful execution of a pair of programs related by a C r a s h F i x oracle:

c 1 • κ 1 κ 1 O 1 if (b) c 1 else c 2 • κ 2 c 1 • κ 2 κ 2 π L π R ••• ••• O 2 O 3 ••• π L π R π L π R
The following diagram illustrates the case of the right program effectively avoiding a crash present in the left program by guarding the affected instruction c 1 under a guard condition b:

c 1 • κ 1 κ ′ 1 O 1 if (b) c 1 else c 2 • κ 2 c 2 • κ 2 κ 2 ̸ π L π R ••• ••• O 2 O 3 ••• π L π R π L π R
To perform as described, the C r a s h F i x oracle language makes use of the S H e l p e r function with the empty type as the type β of actual continuation-level changes, and with a product type b × c × c × (S → N) as the type α of actual statement-level changes. Each statement-level change is a quadruple (b, c 1 , c 2 , f ) such that whenever the boolean expression b does not evaluate to true in a store S, f (S) gives a bound on the number of steps required for c 1 to crash. This last requirement is omitted from the quadruple in this presentation, but is part of the statement-level change type in the Coq definition.

Definition 30 (C r a s h F i x language on Imp). The oracle language C r a s h F i x on Imp is defined by the oracle language definition (unit, S Imp × S Imp × δκ + S Imp × S Imp , S CF , 1 tt , 1 tt , f st, snd, I CF )

where:

• I CF (tt, (s 1 , s 2 , km)) holds if s 1 and s 2 's continuations are indeed related by km (the details are omitted in this already lengthy description but can be found in the Coq development)

• I CF (tt, (s 1 , s 2 )) holds if s 1 ̸ → • S CF (tt, (s 1 , s 2 )) = (tt, (s 1 , E Imp (s 2 ))) • S CF (tt, (s 1 , s 2 , m • km)) = ⎧ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎨ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎩ (s ′ 1 , s ′ 2 , km ′ ) if S H e l p e r (s 1 , s 2 , m, km) = GStep s ′ 1 s ′ 2 km ′ (s 1 , s ′ 2 , km ′ ) if S H e l p e r (s 1 , (c 2 • κ 2 , S 2 ), m, km) = SCmdStep (b, c 1 , c 2 , f ) km ′ and S 2 ⊢ b ⇓ true and E Imp ((c 2 • κ 2 , S 2 )) = s ′ 2 (s ′ 1 , s ′ 2 ) if S H e l p e r (s 1 , (c 2 • κ 2 , S 2 ), m, km) = SCmdStep (b, c 1 , c 2 , f ) km ′ and S 2 ⊢ b ⇓ false and E Imp ((c 2 • κ 2 , S 2 )) = s ′ 2 and ∃n ≤ f (S 2 ), E n Imp (s 1 ) = s ′ 1 ∧ s ′ 1 ̸ ∈ dom(E Imp ) (s ′ 1 , s 2 ) if S H e l p e r (s 1 , (c 2 • κ 2 , S 2 ), m, km) = SCmdStep (b, c 1 , c 2 , f ) km ′ and b does not evaluate in S 2 and ∃1 ≤ n ≤ f (S 2 ), E n Imp (s 1 ) = s ′ 1 ∧ s ′ 1 ̸ ∈ dom(E Imp )
It is important to note that this oracle language does not guarantee that the "fallback" statement does not crash, only that it avoids a code path that was known to crash. The rationale behind this decision is that proving the new code path does not crash would require traditional techniques and is not made substantially easier by a change-based approach: after all, if the previous version of the program crashed, it probably lacked any safety proof that could be reused.

Off-by-one crash fixes

A second example of oracle language specifically handling crashing programs is the C r a s h F i x W h i l e oracle language, describing pairs of programs in which the left program crashes during the last iteration of a while loop which condition is of the shape n ≤ e and in which the right program avoids this by replacing the loop condition with n < e.

Example 13. The following pair of programs, in which the right program is obtained by changing the condition 0 < = d of line 4 of the left program to 0 < d , is an example of programs related by C r a s h F i x W h i l e :

x = v + 1 ; s = 0 ; d = x ; w h i l e ( 0 < = d ) { i f ( x % d = = 0 ) s = s + d ; d = d - 1 ; } x = v + 1 ; s = 0 ; d = x ; w h i l e ( 0 < d ) { i f ( x % d = = 0 ) s = s + d ; d = d - 1 ; }
The C r a s h F i x W h i l e oracle language is defined in a way very similar to the C r a s h F i x oracle language, performing lock-step execution of both programs until the last iteration of the loop is reached, in which case the oracle performs as many steps as needed in the left program to reach the crashed state, performs a single step in the right program, and switches to an oracle state asserting that the left program has crashed.

As illustrated by the following diagram, as long as the last iteration of the loop isn't reached, the oracle simulates the two programs in lockstep:

while (n ≤ e) c • κ 1 c • while (n ≤ e) c • κ 1 while (n ≤ e) c • κ 1 O 1 O 2 O n while (n < e) c • κ 2 c • while (n < e) c • κ 2 while (n < e) c • κ 2 π L π R π L π R π L π R ••• ••• •••
Things get more interesting when reaching the last iteration, where n ≤ e evaluates to true but n < e evaluates to false. As stated earlier, the oracle will pop the while from the right program's continuation and step as many times as needed in the left program to reach a crashed state. This is illustrated by the following diagram:

while (n ≤ e ′ ) c • κ 1 κ ′ 1 O 1 while (n < e) c • κ 2 κ 2 ̸ π L π R O 2 ••• ••• π L π R
To perform as illustrated, C r a s h F i x W h i l e uses S H e l p e r in a way very similar to C r a s h F i x , using an empty type for the type β of actual continuation-level changes, and a product type n × e × c × (S → N) for the type α of statement-level changes, where every actual statement-level change is a quadruple (n, e, c, f ) such that for every store S in which e evaluates to n, c crashes in at most f (S) steps. As with previous oracles, this last condition is enforced in the Coq development but not formalized in this presentation.

Definition 31 (C r a s h F i x W h i l e language on Imp). The oracle language C r a s h F i x W h i l e on Imp is defined by the oracle language definition

(unit, S Imp × S Imp × δκ + S Imp × S Imp , S CF W , 1 tt , 1 tt , f st, snd, I CF W )
where:

• I CF W (tt, (s 1 , s 2 , km)) holds if s 1 and s 2 's continuations are indeed related by km (the details are omitted in this already lengthy description but can be found in the Coq development)

• I CF W (tt, (s 1 , s 2 )) holds if s 1 ̸ → • S CF W (tt, (s 1 , s 2 )) = (tt, (s 1 , E Imp (s 2 ))) • S CF W (tt, (s 1 , s 2 , m • km)) = ⎧ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎨ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎩ (s ′ 1 , s ′ 2 , km ′ ) if S H e l p e r (s 1 , s 2 , m, km) = GStep s ′ 1 s ′ 2 km ′ (s ′ 1 , s ′ 2 , km ′ ) if S H e l p e r (s 1 , (c 2 • κ 2 , S 2 ), m, km) = SCmdStep (n, e, c, f ) km ′ and S 2 ⊢ e < n ⇓ true and E Imp (s 1 ) = s ′ 1 and E Imp ((c 2 • κ 2 , S 2 )) = s ′ 2 (s ′ 1 , s ′ 2 , km ′′ ) if S H e l p e r (s 1 , (c 2 • κ 2 , S 2 ), m, km) = SCmdStep (n, e, c, f ) km ′ and S 2 ⊢ n < e ⇓ true and E Imp (s 1 ) = s ′ 1 and E Imp ((c 2 • κ 2 , S 2 )) = s ′ 2 and where km ′′ = ∆ c (I d ) :: ∆ c (∆ L e a f (n, e, c, f )) :: km ′ (s ′ 1 , s ′ 2 ) if S H e l p e r (s 1 , (c 2 • κ 2 , S 2 ), m, km) = SCmdStep (n, b, c, f ) km ′ and S 2 ⊢ e ⇓ n and E Imp ((c 2 • κ 2 , S 2 )) = s ′ 2 and ∃n ≤ f (S 2 ), E n Imp (s 1 ) = s ′ 1 ∧ s ′ 1 ̸ ∈ dom(E Imp )
Chapter 5

Encoding Relational Hoare Logic

As seen in Chapter 2, Relational Hoare Logic is a program logic to reason about relational properties on pairs of terminating programs. Encoding Relational Hoare Logic proofs with oracles demonstrates the expressivity of our framework, provides a smallstep semantics interpretation of Relational Hoare Logic proofs, and forms the basis of a certified proof of soundness of the considered Hoare Logic variants. We wrote three oracle languages to encode three different variants of Relational Hoare Logic (RHL): Minimal RHL, Core RHL and Core RHL extended with self-composition. The basic idea is to see correlating oracles as small-step interpreters of RHL proof terms.

Extended RHL extends Core RHL by allowing to replace some sub-programs by other extensionnally-equivalent sub-programs within a RHL proof. While we have no reason to doubt it can also be encoded using our framework, the insufficiently formal presentation of the original paper [START_REF] Barthe | Product programs and relational program logics[END_REF], together with the fact the added rule is inherently extensional, made us decide not to formally prove it. Intuitively, encoding it would probably involve the same kind of reasoning as in the A b s t r a c t E q u i v oracle language, with the added complexity of having to unfold the RHL proof at the same time.

Minimal RHL

The oracle language M i n i m a l R H L of programs related by a Minimal Relational Hoare Logic quadruple evaluates the two programs in lockstep and maintains at all times a formula describing the relation between the stores of the projected program configurations, in such a way that upon completion of both programs, this formula implies the postcondition of the original Minimal Relational Hoare Logic quadruple.

To do this, a M i n i m a l R H L oracle maintains a list of Minimal Relational Hoare Logic proof terms of the same length as the two programs' continuation, in such a way that: i. projecting the left (respectively right) statement of each proof term's conclusion results in the left (respectively right) program's continuation;

ii. the current formula implies the first proof term's precondition, iii. each proof term's postcondition implies the next one's precondition iv. the last proof term's postcondition implies the original quadruple's postcondition A M i n i m a l R H L dynamic oracle state is thus a quintuple (s 1 , s 2 , S, P, Π) where s 1 and s 2 are the two related Imp program configurations as defined in Chapter 4, S is a disjoint union of those states' stores, P is a valid assertion on the store S, and Π is a list of Minimal RHL proof terms corresponding to the program states' continuations and consistent in the sense that the assertion P implies the precondition of the first Minimal RHL proof term, and every proof term's postcondition implies the precondition of the next proof term.

For instance, consider the following dynamic M i n i m a l R H L oracle state:

(s 1 , s 2 , S, P,

. . . ⊢ {A} c 1 ∼ c 2 {B} • . . . ⊢ {C} c 3 ∼ c 4 {D} • • • . . . ⊢ {E} c i ∼ c j {F } )
This state is valid if (i) the store S is indeed the disjoint union of the two program states' store, the list of proof terms actually corresponds to (ii) the proof left continuation and (iii) the right continuation, and (iv) the list of proof terms is consistent, i.e.:

i. S = snd(s

1 ) ⊎ snd(s 2 ) ii. f st(s 1 ) = c 1 • c 3 • • • c i • halt iii. f st(s 2 ) = c 2 • c 4 • • • c j • halt iv. P ⇒ A, B ⇒ C, …
In order to maintain the aforementioned properties on oracle states, M i n i m a l R H L "interprets" the list of proof terms in the union store, effectively defining a small-step semantics on Minimal RHL proof terms. This interpretation is equivalent to interpreting the two programs and "unfolding" the proof terms according to the execution paths taken. This is done with a recursive step function ψ defined below. Definition 32 (ψ). The ψ function takes a store, a distinguished RHL proof term, and a list of RHL proof terms, and returns a triple of a store, an assertion, and a list of RHL proof terms. It is defined inductively on its second argument by the following cases:

• When the distinguished proof tree starts with a R-Skip rule, it is discarded without modifying the store. The assertion returned is the postcondition P of the proof term, since it has been evaluated in its entirety:

ψ ( S, ⊢ {P } skip ∼ skip {P } R-Skip , Π ) = (S, P, Π)
• When the distinguished proof term is built with a R-Assign rule, the right-handsides of both left and right assignments are evaluated, and their result stored in the returned store. The returned assertion is the postcondition P of the proof term since it has been handled entirely:

ψ ( S, ⊢ {P ′ } x 1 = e 1 ∼ x 2 = e 2 {P } R-Assign , Π ) = (S[x 1 ↦ → n 1 ][x 2 ↦ → n 2 ], P, Π)
where S ⊢ e 1 ⇓ n 1 and S ⊢ e 2 ⇓ n 2

• For simplicity's sake, the R-Assert rule is abusively handled like the R-Skip rule.

This is abusive as it should only be defined when b 1 and b 2 both evaluate to true in S. Fortunately, as we only use ψ in contexts in which left and right programs both execute properly, b 1 and b 2 are guaranteed to evaluate to true:

ψ ( S, P ⇒ b 1 ∧ b 2 ⊢ {P } assert (b 1 ) ∼ assert (b 2 ) {P } R-Assert , Π ) = (S, P, Π)
• The rule R-Seq is handled by "unfolding" the tree, pushing the two underlying proof trees on the stack of proof terms in a way that mirrors unfolding a sequence. The returned assertion is the original term's precondition, as that implies the new head term's precondition:

ψ ( S, Π 1 Π 2 ⊢ {P } c 1 1 ; c 1 2 ∼ c 2 1 ; c 2 2 {Q} R-Seq , Π ) = (S, P, Π 1 • Π 2 • Π)
• The R-If rule covers the two branches, but it needs to get unfolded differently depending on the execution path, in a fashion very similar to that of the smallstep execution of an if statement. The proof of P ⇒ b 1 = b 2 ensures that both programs execute the same branch, but the proof itself is not manipulated by ψ.

The returned assertion is the precondition of the subtree corresponding to the selected branch:

ψ ( S, Π 1 Π 2 P ⇒ b 1 = b 2 ⊢ {P } if (b 1 ) c 1 1 else c 1 2 ∼ if (b 2 ) c 2 1 else c 2 2 {Q} R-If , Π ) = (S, P ∧ b 1 , Π 1 • Π) where S ⊢ b 1 ⇓ true ψ ( S, Π 1 Π 2 P ⇒ b 1 = b 2 ⊢ {P } if (b 1 ) c 1 1 else c 1 2 ∼ if (b 2 ) c 2 1 else c 2 2 {Q} R-If , Π ) = (S, P ∧ ¬b 1 , Π 2 • Π)
where S ⊢ b 1 ⇓ false

• The R-While rule is handled by either duplicating the proof tree Π 1 corresponding to the loop body, in which case the returned assertion is the precondition of Π 1 , or drop the proof term Π of the loop, in which case the returned assertion is the postcondition of Π:

ψ ( S, Π 1 P ⇒ b 1 = b 2 ⊢ {P } while (b 1 ) c 1 ∼ while (b 2 ) c 2 {P ∧ ¬b 1 } R-While , Π ) = (S, P ∧ b 1 , Π 1 • Π • Π) where S ⊢ b 1 ⇓ true ψ ( S, Π 1 P ⇒ b 1 = b 2 ⊢ {P } while (b 1 ) c 1 ∼ while (b 2 ) c 2 {P ∧ ¬b 1 } R-While , Π ) = (S, P ∧ ¬b 1 , Π)
where S ⊢ b 1 ⇓ false

• Finally, the R-Sub rule does not correspond to any small-step computation. It is thus handled by recursively calling ψ in order to unfold the proof tree until reaching a proof term corresponding to a small-step computation:

ψ ( S, Π 1 P ′ ⇒ P Q ⇒ Q ′ ⊢ {P ′ } c 1 ∼ c 2 {Q ′ } R-Sub , Π ) = ψ(S, Π 1 , Π)
Definition 33 (M i n i m a l R H L oracle language). The oracle language M i n i m a l R H L on Imp is defined by the oracle language definition

(p, S Imp × S Imp × S × P × Π, S M RHL , 1 tt , 1 tt , f st, snd, I M RHL )
where:

• I M RHL (Q, ((κ 1 , S 1 ), (κ 2 , S 2 ), S, P, Π)) holds iff:

-P holds on S -S = S 1 ⊎ S 2 -κ 1 can be recovered by taking the left term of the conclusion of each proof term in Π κ 2 can be recovered by taking the right term of the conclusion of each proof term in Π -P implies the precondition of the first Relational Hoare quadruple of Π, each quadruple's postcondition implies the next one's precondition, and the last postcondition implies Q

• S M RHL (Q, (s 1 , s 2 , S, P, Π • Π)) = (E Imp (s 1 ), E Imp (s 2 ), S ′ , P ′ , Π ′ ) when ψ(S, Π, Π) = (S ′ , P ′ , Π ′ )
Given a Minimal RHL proof term Π with the quadruple ⊢ {P } c 1 ∼ c 2 {Q} as a conclusion, and a pair of initial stores S 1 and S 2 such that P holds on S 1 ⊎ S 2 , a M i n i m a l R H L oracle configuration "interpreting" the proof can be constructed as (Q, ((c 1 • halt, S 1 ), (c 2 • halt, S 2 ), S 1 ⊎ S 2 , Π • halt)). This encoding of Minimal RHL leads to a new proof of correction of the Minimal RHL rules.

Theorem 5 (Minimal RHL is sound). For every Minimal RHL proof term Π with conclusion ⊢ {P } c 1 ∼ c 2 {Q} and every pair of disjoint stores S 1 and S 2 , if P holds on S 1 ⊎ S 2 and c 1 and c 2 both terminate when executed in S 1 and S 2 respectively, then c 1 and c 2 successfully execute leading to stores S ′ 1 and S ′ 2 such that Q holds on S ′ 1 ⊎ S ′ 2 .

Proof. As always, the proof has been formalized in the Coq proof assistant. Nevertheless, we provide here a rough outline of the proof:

• By theorem 4, since c 1 and c 2 have terminating executions, so does the oracle, leading to a final oracle state ((κ ′ 1 , S ′ 1 ), (κ ′ 2 , S ′ 2 ), S ′ , P ′ , Π ′ )

• It can then be proven the oracle cannot lead to crashed executions. (κ ′ 1 , S ′ 1 ) and (κ ′ 2 , S ′ 2 ) are thus successful final states, with halt as continuation, thus

κ ′ 1 = κ ′ 2 = halt.
• Since the oracle invariant holds on ((halt, S ′ 1 ), (halt, S ′ 2 ), S ′ , P ′ , Π ′ ), Π ′ is empty, and P ′ implies the global postcondition Q.

• We also have S ′ = S ′ 1 ⊎ S ′ 2 and P ′ holds on S ′ , so Q holds on S ′ 1 ⊎ S ′ 2 .

Core RHL

As described in Chapter 2, Core Relational Hoare Logic extends Minimal Relational Hoare Logic with rules corresponding to the execution of either the left or right program. Extending M i n i m a l R H L to support those new rules is mostly straightforward, if a bit tedious, save for the fact that the disparity between the big-step presentation of the Core RHL rules and the small-step formalisation of our framework requires some special care. Indeed, in the big-step presentation used for Relational Hoare Logic, empty programs are represented as skip statements; thus, some of the rules specific to Core RHL introduce skip statements that do not syntactically appear in the programs under consideration and that do not appear in the small-step reductions either. As a consequence, some rules can apply to two actual sub-statements or to only one actual sub-statement and a "fictitious" skip statement.

Indeed, the R-Assign-L, R-Assert-L and R-Seq-Skip-L rules reproduced below-as well as their symmetric counterparts-introduce a "fictitious" skip statement-highlighted-to encode an empty program-which does not correspond to any statement in the continuation:

⊢ {P } skip ∼ c {Q} P ⇒ b ⊢ {P } assert (b) ∼ c {Q} R-Assert-L ⊢ {P } skip ∼ c {Q} ⊢ {P [e/x]} x = e ∼ c {Q} R-Assign-L ⊢ {P } c 1 ∼ skip {Q} ⊢ {Q} c 2 ∼ c {R} ⊢ {P } c 1 ; c 2 ∼ c {R} R-Seq-Skip-L
Therefore, any rule applicable to a skip statement on either side may refer to either a real or a "fictitious" skip. Those rules-reproduced below with a highlight on possible "fictitious" skip statements appearing in the conclusion, color-coded to keep track of their propagation in the proof tree

-are R-Skip, R-Sub, R-Assign-L, R-Assign-R, R-Assert-L, R-Assert-R, R-If-L, R-If-R, R-Seq-Skip-L and R-Seq-Skip-R. ⊢ {P } skip ∼ skip {P } R-Skip ⊢ {P } c 1 ∼ c 2 {Q} P ′ ⇒ P Q ⇒ Q ′ ⊢ {P ′ } c 1 ∼ c 2 {Q ′ } R-Sub ⊢ {P } skip ∼ c {Q} P ⇒ b ⊢ {P } assert (b) ∼ c {Q} R-Assert-L ⊢ {P } skip ∼ c {Q} ⊢ {P [e/x]} x = e ∼ c {Q} R-Assign-L ⊢ {P } c 1 ∼ skip {Q} ⊢ {Q} c 2 ∼ c {R} ⊢ {P } c 1 ; c 2 ∼ c {R} R-Seq-Skip-L ⊢ {P ∧ b} c 1 ∼ c {Q} ⊢ {P ∧ ¬b} c 2 ∼ c {Q} ⊢ {P } if (b) c 1 else c 2 ∼ c {Q} R-If-L
Let us illustrate how "fictitious" skip statements occur with a Core RHL proof introducing a skip with R-Assert-L and "consuming" it with R-Skip:

⊢ {x = 1} skip ∼ skip {x = 1} R-Skip x = 1 ⇒ x ≤ 2 ⊢ {x = 1} assert (x ≤ 2) ∼ skip {x = 1} R-Assert-L
One way to interpret the above proof as a series of reduction steps is to consider the R-Assert-L rule to describe exactly one reduction of the left program. With that interpretation, the R-Skip rule above then describes exactly one reduction of the right program. But there are other uses of the R-Skip rule that describe reductions in both programs at once. For this reason, a C o r e R H L oracle needs to handle such rules differently based on whether they apply to "fictitious" skip statements or not.

In addition, the R-Sub and R-Skip rules may be applied to "fictitious" skip statements on both sides at the same time, in which case they do not represent any computation. Such a tree must not appear in the state of an oracle: it should be "unfolded" within a single oracle step instead, as to guarantee oracle productiveness. This is illustrated by the following example, in which the R-Assert-L can be interpreted as a step of the left program and R-Assert-R as a step of the second program, but the R-Skip rule does not correspond to any computation:

⊢ {x = 2} skip ∼ skip {x = 2} R-Skip x = 2 ⇒ true ⊢ {x = 2} skip ∼ assert (true) {x = 2} R-Assert-R x = 2 ⇒ x ≤ 2 ⊢ {x = 2} assert (x ≤ 2) ∼ assert (true) {x = 2} R-Assert-L
With all that being said, the general structure of the C o r e R H L oracle is very similar to the M i n i m a l R H L one except each term of the "Relational Hoare Logic continuation" can be of three types: proof terms relating two actual sub-programs, proof terms applying only to the left program and featuring only fictitious skip statements as the right program, and proof terms applying only to the right program and featuring only fictitious skip statements as the left program.

The step function is accordingly extended to support the additional rules, and also uses variants handling proof terms applying specifically to the left or right program.

The invariant is also a bit less straightforward as the "Relational Hoare Logic continuation" may not be the same length as the left and right continuations: when projecting to the left (resp. right) program, it has to be filtered to omit any proof term specific to the right (resp. left) program.

Theorem 6 (Core RHL is sound). For every Core RHL proof term Π with conclusion ⊢ {P } c 1 ∼ c 2 {Q} and every pair of disjoint stores S 1 and S 2 , if P holds on S 1 ⊎ S 2 and c 1 and c 2 both terminate when executed in S 1 and S 2 respectively, then c 1 and c 2 successfully execute leading to stores S ′ 1 and

S ′ 2 such that Q holds on S ′ 1 ⊎ S ′ 2 .
Proof. As with Minimal RHL, the proof has been formalized in the Coq proof assistant. The proof has the same outline as that of Minimal RHL:

• By theorem 4, since c 1 and c 2 have terminating executions, so does the oracle, leading to a final oracle state ((κ ′ 1 , S ′ 1 ), (κ ′ 2 , S ′ 2 ), S ′ , P ′ , Π ′ )

• It can then be proven the oracle cannot lead to crashed executions. (κ ′ 1 , S ′ 1 ) and (κ ′ 2 , S ′ 2 ) are thus successful final states, with halt as continuation, thus

κ ′ 1 = κ ′ 2 = halt.
• Since the oracle invariant holds on ((halt, S ′ 1 ), (halt, S ′ 2 ), S ′ , P ′ , Π ′ ), Π ′ is empty, and P ′ implies the global postcondition Q.

• We also have S ′ = S ′ 1 ⊎ S ′ 2 and P ′ holds on S ′ , so Q holds on S ′ 1 ⊎ S ′ 2 .

Core RHL extended with self-composition

The final oracle language presented in this thesis is a simple extension to the C o r e R H L oracle language to incorporate self-composition, that is, the ability to reduce a relational proof to a single-program proof on the sequential composition of the two related programs.

The additional rule R-SelfComp consists in proving the postcondition on the sequential composition of the two programs under scrutiny using regular Hoare Logic, thus not imposing any condition on the relation between the two programs' structure:

⊢ {P } c 1 ; c 2 {Q} ⊢ {P } c 1 ∼ c 2 {Q} R-SelfComp
In our case, it means that when the head proof term begins with a R-SelfComp rule, the oracle will need to only predict steps of the left sub-program until it ends (if it does) before switching to the right sub-program. Intuitively, this is achievable by unfolding the head proof term until we get a Seq rule, and deconstructing it to recover a Hoare proof term for the left program and a Hoare proof term for the right program. Indeed, the only (regular) Hoare Logic rules admitting a sequence as a conclusion are the Sub and Seq rules, causing Core RHL proof terms with an application of the R-SelfComp rule at their root to always start with a finite-possibly null-number of Sub rules followed by a Seq rule.

There is a tricky case to consider, however: much like some Core RHL rules might apply to "fictitious" skip statements, this is also the case of the R-SelfComp rule, as illustrated:

⊢ {⊤} skip {⊤} ⊢ {⊤} skip {⊤} ⊢ {⊤} skip ; skip {⊤} Seq ⊢ {⊤} skip ∼ skip {⊤} R-SelfComp ⊤ ⇒ true ⊢ {⊤} assert (true) ∼ skip {⊤} R-Assert-L
One last trick to consider is that the R-SelfComp, much like R-Sub, R-SelfComp does not represent progress in the computation of either program and must thus be handled within a single oracle step, in addition to a productive computation.

In the end, the C o r e R H L S C oracle language extends the C o r e R H L oracle language by adding two new variants for regular Hoare Logic terms to the type of "Relational Hoare Logic continuations" elements, as well as the associated cases in the step function.

Chapter 6

Difference languages

The various oracle languages presented in the previous chapters serve the role of proof schema for relational program properties: each oracle language corresponds to a given class of program differences and can be instantiated as an oracle for a specific pair of programs, reducing the constructive proof of a given meaningful relation between their execution traces to a proof that the oracle's invariant holds on its initial state. Indeed, someone interested in proving a particular relation between two programs can pick an oracle language describing that relation, and write the initial oracle state relating the two program states of interest. Proving that the result oracle indeed relates the two programs-and thus that there exists such a relation between the two programs-then reduces to proving the oracle's invariant on the initial oracle state. This process can be streamlined by the use of a difference language: as stated in this thesis' introduction, the main purpose of those oracle languages is to form the building blocks of a descriptive difference language that could be used by programmers to specify the intent behind their changes. Ideally, such change descriptions should be as concise and intuitively readable to programmers as ordinary informative commit messages while having unambiguous semantics, being machine-readable and with the ability to be mechanically verified.

In this chapter, we take a step back from oracles to formally state what we expect from such a difference language, defining trace relations, correlations and difference languages. Then we show how the previously-defined oracle languages can be used within this setting, in order to build a simple difference language for Imp.

Trace relations

As we are interested in semantic differences, we study the relation between the semantics of two programs. One traditional representation of program semantics is their execution trace. As stated in Chapter 3, small-step semantics and execution traces are indeed a formalism enabling precise reasoning about programs, including nontermination and crashing behaviors as well as any intensional property. Therefore, we are interested in relations between reduction traces. 93 Definition 34 (Reduction trace). Given a programming language (P, G, S, I, E, R, F), the reduction trace of a program p ∈ P is the potentially infinite nonempty list T (p) of program configurations coinductively defined by:

T (p) = T ⋆ (I(p)) T ⋆ (g, s) = { (g, s) if E g s is undefined (g, s) • T ⋆ (g, E g s) otherwise
We write T the set of reduction traces of L, i.e. T = {T (p) | p ∈ P}.

We write ⌈ ℓ ⌉ for the first element of a nonempty potentially-infinite list ℓ.

Definition 35 (Trace relation). The set R of relations over reduction traces is defined as the set of binary predicates over T, i.e. the inhabitants of T → T → P.

Amongst the relations between program reduction traces, we are particularly interested in γ-correlations, trace relations defined by a pairwise relation between program configurations, as several interesting differences are naturally specified by this kind of relations.

Informally, a γ-correlation between two execution traces states that (some) states from one trace are related to (some) states of the other trace by a relation γ: Step

|C 1 | + |C 2 | > 0 ⌈ C 1 • T 1 ⌉γ⌈ C 2 • T 2 ⌉ T 1 γ ∼ T 2 C 1 • T 1 γ ∼ C 2 • T 2 Stop C 1 γC 2 C 1 γ ∼ C 2
This definition of γ-correlation deserves several remarks. First, for T 1 γ ∼ T 2 to hold, the head configurations of T 1 and T 2 must be related by γ. If each trace contains only one configuration, the γ-correlation holds. Otherwise, there must exist two strict finite prefixes C 1 and C 2 of T 1 and T 2 that can be skipped to get to another pair of γ-correlated traces.

Second, the hypothesis |C 1 | + |C 2 | > 0 forces one of the prefixes to not be empty.

This condition ensures that a correlation between two finite traces covers both traces.

It might be surprising that we do not force both prefixes not to be empty. This is actually necessary to be able to express Lamport's and Abadi's stuttering [START_REF] Lamport | The existence of refinement mappings[END_REF]. In a word, the stuttering mechanism allows the γ-correlation to relate a configuration of one trace to several configurations of the other trace. That way, a γ-correlation can denote a local desynchronization between the two compared traces. A γ-correlation is said to be (locally) lockstep if |C 1 | = 1 and |C 2 | = 1 for a given instantiation of the rule (Step).

As a final remark, one may notice that our notion of γ-correlation does not require the relation to cover infinitely many configurations from infinite traces: if T 2 is infinite, a γ-correlation may choose not to progress in T 1 by consuming an infinite number of configurations from T 2 (taking |C 1 | = 0 and |C 2 | > 0 to satisfy the first hypothesis of the rule (Step)). An additional fairness condition could be added in the definition of γ-correlations to avoid that case: typically, we could force the hypotheses |C 1 | > 0 and |C 2 | > 0 to alternate infinitely often. Yet, as we will discuss in the conclusion of this thesis, such a fairness condition may not always be appropriate for our purpose.

Difference languages

Trace relations as defined above are the basis for difference languages' semantics. A difference language itself is a descriptive language in which each word is interpreted as such a trace relation.

Definition 37 (Difference language)

. A difference language definition for a programming language L is a pair (D, • ) where:

• D is the type of difference abstract syntax trees; • • is the interpretation function of type D → R

Oracles and difference languages

Oracles effectively describe the relation between two programs' execution traces in a constructive fashion. In fact, trace relations realized by correlating oracles fit closely with the concept of γ-correlations defined above. This is especially apparent when comparing the shape of an oracle execution trace and its projections with the shape intended for γ-correlations:

s 1 n s 2 n s 3 n s 4 n • • • Em Em Em Em • • • o 1 o 2 o 3 o 4 S S S π L π R π L π R π L π R π L π R Definition 38 (γ O,g ). Any oracle language O = (G, O, S, π ′ L , π ′ R , π L , π R , I)
along with a fixed global environment g ∈ G defines a γ-relation where γ is defined as follows:

γ O,g = λC 1 C 2 . ∃ o, I(o) ∧ C 1 = (π ′ L (g), π L (o)) ∧ C 2 = (π ′ R (g), π R (o))
In the above definition, the dynamic information contained in the oracle state is pushed behind an existentially-quantified variable, which is forced to correspond to the program configurations under consideration through the projection functions of the oracle.

The oracle then realizes the γ-relation is the sense that each oracle step yields a new oracle state which can be projected left and right to recover the next related states in the γ-correlation. γ is then guaranteed to hold on this new pair of states thanks to the invariant preservation and prediction soundness requirements of Definition 14, and the productiveness side-condition of prediction soundness matches that of the

Step rule of γ-correlations.

Since the dynamic oracle state is bound by an existential quantifier, such a γcorrelation may be less precise than the actual relation defined by the oracle. Indeed, while it ensures the two reduction traces are related by a succession of oracle states on which the oracle invariant holds, it does not ensure that each of those successive oracle states is the result of performing a single oracle step from the previous oracle state.

ρ O,g,o = λT 1 T 2 . ⌈ T 1 ⌉ = (π ′ L (g), π L (o)) ∧ ⌈ T 2 ⌉ = (π ′ R (g), π R (o)) ∧ I(g, o)
This relation simply asserts that the two initial programs states are related by a sound oracle. By the oracle's soundness, this relation implies the γ-correlation defined above.

A difference language on Imp

We now introduce a toy difference language ∆Imp for Imp, effectively giving a syntax for each oracle language defined in our earlier chapter. A difference δ can be either a primitive difference δ p , or a composition δ; δ of two differences, in order to relate two programs by a succession of primitive differences (necessitating intermediary programs between each pair of primitive differences).

This choice of primitives is ad hoc and there is no guarantee that they match all the software changes that can happen in a real software development. Finding a more complete set of primitives is left as future work and discussed in the conclusion of this thesis. Nevertheless, we have defined three categories of changes, depending on their level of abstraction. The two categories named syntactic refactorings and syntactic changes contain primitive differences that can be expressed as program transformations. The next category, extensional changes, relates two programs by exploiting a proof that a specific relation holds between their configurations during the evaluation.

In fact, each of these primitive differences is implemented by an oracle language defined in the previous chapter.

Syntactic refactorings are program transformations that preserve the semantics of the source program for a given notion of program equivalence. They include:

1. Any renaming with respect to a bijection between their variable identifiers 2. Any swap between two consecutive assignments found at a program point characterized by a context C, provided those assignments are syntactically independent 3. Any swap between the branches of a conditional statement provided that the condition of this statement is negated in the target program 4. Any refactoring consisting in moving after a conditional code that was present at the end of both of the conditional's branches 5. Any reparenthesizing (sequence associativity) Syntactic changes are program transformations that modify the meaning of the source program:

1. The difference fix off-by-one at C is a program transformation that applies to a while-loop whose last iteration crashes and that modifies its condition to avoid this last buggy iteration. Finally, extensional changes are modifications of the source program that are not necessarily instances of a program transformation but for which a proof can be exploited to show that a specific relation holds between the two programs' traces:

1. The difference ensure equivalence at C relates two equivalent subprograms located at C in the two programs. This difference exploits a proof of extensional equivalence to show that the target program is a refactoring of the source program.

2. The difference assume {P } ensure {Q} relates two programs for which a relational Hoare logic proof validates the precondition P and the postcondition Q.

As said in the introduction, by referring to the variables of both programs in P and Q, such a proof establishes that a specific relation holds between the reduction traces of two a priori inequivalent programs.

Semantics

Now that we have given a syntax for our difference language, we need to give it an interpretation. The interpretation of composition and superposition is straightforward:

δ ∈ R δ 1 ; δ 2 = λT 1 T 2 . ∃T 3 . T 1 δ 1 T 3 ∧ T 3 δ 2 T 2 δ 1 & δ 2 = λT 1 T 2 . T 1 δ 1 T 2 ∧ T 1 δ 2 T 2
That is, the composition of two differences relates two traces if there exists an intermediate trace such that the first composed difference relates the left trace to that intermediate trace and the second composed difference relates the intermediate trace to the right trace. The superposition of two differences relates two traces if both of the superposed differences relate those traces.

Every primitive difference can be interpreted by the γ-correlation induced by a correlating oracle language. For instance, the interpretation for a renaming could be:

rename φ = λT 1 T 2 . T 1 γ ∼ T 2 where γ = γ R e n a m i n g ,φ
However, that relation is not extremely precise, as the oracle state is hidden behind an existential and thus cannot be specified. This is made apparent with other primitive differences, such as assignments swapping:

swap assign at C = λT 1 T 2 . T 1 γ ∼ T 2 where γ = γ S w a p A s s i g n ,tt
Indeed, the context C is part of the dynamic state of an oracle and thus cannot be specified in a γ-correlation, as explained above. As a result, γ S w a p A s s i g n ,tt relates more traces than those obtained by executing programs in which the assignments at context C have been swapped. For this reason, we have opted for a more precise interpretation of those differences, in the sense that it relates fewer pairs of traces: this is done by using ρ O,g,s , which requires constructing a dynamic oracle state from the primitive difference, instead of γ S w a p A s s i g n ,tt . of code in the project is presented in the following table, representing the output of c o q w c , grouped by component:

Walk through the code

This section largely follows a similar approach to that of the P a p e r . v source file, presenting the framework and how to use it through Coq snippets.

Programming languages

In chapter 3, we represent a programming language as 7-uple (P, G, S, I, E, R, F)

equipped with additional proofs. This is encoded in our Coq library as a record with fields for both the different components of the tuple and for the accompanying proofs. The definition of that record type lies in O r a c l e L a n g u a g e s . P r o g r a m m i n g L a n g u a g e . In order to provide a detailed example of a programming language definition, let us consider a very simple programming language for a stack machine that can only perform additions.

S e c t i o n

P L E x a m p l e . By the above definition, a program is a list of instructions, its dynamic state is a stack of natural numbers paired with a list of instructions, its global static state is empty, and the step function performs as expected. A program has properly terminated when its stack contains a single value and its continuation is empty. These definitions would suffice to define the 7-uple (e x _ s t a t e _ p r o g , e x _ g e n v , e x _ s t a t e , e x _ i n i t i a l _ s t a t e , e x _ s t e p , e x _ r e t , e x _ s t a t e _ f i n a l ), but we also need to prove the accompanying properties, that is, e x _ s t a t e _ f i n a l actually characterizes final states, and both e x _ g e n v and e x _ s t a t e are equipped with a decidable equality preserved by e x _ s t e p .

I n d u c t i v e

This would translate to the following Coq code (proof scripts omitted):

D e f i n i t i o n

e x _ g e n v _ e q : = @ e q u n i t .

D e f i n i t i o n e

x _ s t a t e _ e q : = @ e q e x _ s t a t e . In this case, we just use Coq's equality as our decidable equality. We still had to prove that it is decidable, though, and that e x _ s t e p does preserve equality. With all of that done, we can now define the l a n g u a g e record corresponding to our example. g e n v _ e q : = e x _ g e n v _ e q ; g e n v _ e q _ r e f l : = @ e q _ r e f l u n i t ; g e n v _ e q _ s y m : = @ e q _ s y m u n i t ; g e n v _ e q _ t r a n s : = @ e q _ t r a n s u n i t ; g e n v _ e q _ d e c : = e x _ g e n v _ e q _ d e c ; s t a t e _ e q : = e x _ s t a t e _ e q ; s t a t e _ e q _ r e f l : = @ e q _ r e f l e x _ s t a t e ; s t a t e _ e q _ s y m : = @ e q _ s y m e x _ s t a t e ; s t a t e _ e q _ t r a n s : = @ e q _ t r a n s e x _ s t a t e ; s t a t e _ e q _ d e c : = e x _ s t a t e _ e q _ d e c ; s t a t e _ f i n a l _ e q : = e x _ s t a t e _ f i n a l _ e q ;

P r o p e r t y

s t e p _ e q : = e x _ s t e p _ e q ;

s t e p _ e q ' : = e x _ s t e p _ e q ' ; | } .

E n d

P L E x a m p l e .

The record e x _ l a n g u a g e now holds a complete definition of our example language, and we could now write oracle languages for this language. However we will instead use the definitions for Imp from our library, as it will allow us to present our development.

In our library, Imp is provided as a l a n g u a g e record by a functor of the module In order to get a l a n g u a g e record representing Imp, we need to provide a type for the variable identifiers. In this section, this will be a simple finite inductive type: The record of type l a n g u a g e representing Imp is then I m p . i m p _ l a n g u a g e . Before moving on to the next session, let us quickly review Imp's definition:

• Imp's global environments do not hold any information. Therefore, g e n v _ t y p e i m p _ l a n g = u n i t , with υ used as an alias for t t . • Imp's dynamic environments are pairs of a continuation and a store. Hence, M . e m p t y Z ) ) . • A successful final state is a state which continuation is empty.

• Equality on Imp is defined extensionally, relying on M . E q u a l for extensional store equality.

Oracle languages

In Chapter 3, we represent an oracle language as a 8-uple (G, O, S,

π ′ L , π ′ R , π L , π R , I)
with some extra requirements. In our Coq library, this is encoded as a record type parameterized by two programming languages: the one left programs are written in, and the one right programs are written in. The definition of that family of record types is in O r a c l e L a n g u a g e s . O r a c l e L a n g u a g e .

R e q u i r e I m p o r t O r a c l e L a n g u a g e s . O r a c l e L a n g u a g e .

In order to provide a detailed example of an oracle language, let us redefine the identity oracle language: Note that, as every definition below, the step function of that oracle language is parameterized by a language record. Indeed, the identity oracle language is generic in that it may be used for any single programming language. The identity oracle is thus defined for any language L as an oracle language relating left programs written in L with right programs written in that same language L.

D
Another generic oracle language is defined in our Coq development: the universal oracle language, which relates any two programs written in any two programming languages. It is provided by O r a c l e L a n g u a g e s . O r a c l e s . U n i v e r s a l O r a c l e and parameterized by two programming language records. Finally, our library defines a range of oracle languages between pairs of programs written in Imp, as presented in chapters 4 and 5. Those oracle languages are defined in modules O r a c l e L a n g u a g e s . I m p . O r a c l e s . S w a p A s s i g n , O r a c l e L a n g u a g e s . I m p . O r a c l e s . R e n a m i n g and so on.

Most of them are written using the helper functions described in chapter 4 and implemented in O r a c l e L a n g u a g e s . I m p . O r a c l e s . O r a c l e H e l p e r s .

Using an oracle language

In this section, we present a couple of instantiations of oracles on Imp.

Renaming

First, let us require and instantiate the appropriate module: As one may recall, our Coq definition of Imp is parameterized by the type of variable identifiers. Oracles on Imp follow the same pattern: in our case, we instantiated it with V a r _ a s _ D T and the I m p module instantiated in a previous section.

We can now move on to importing I m p and R e n a m i n g definitions and notations to define the left and right programs to be related by a renaming oracle:

( Z . o f _ n a t ( S v ) ) ; a ← I n t 0 ; d ← V a r x ; W H I L E I n t 0 ≤ V a r d D O { I F ( V a r x ) % ( V a r d ) = = I n t 0 T H E N a ← V a r a + V a r d E L S E S k i p ; d ← V a r d - I n t 1 } ; W H I L E I n t 0 ≤ V a r a D O d ← V a
H I L E I n t 0 ≤ V a r d D O { I F ( V a r x ) % ( V a r d ) = = I n t 0 T H E N s ← V a r s + V a r d E L S E S k i p ; d ← V a r d - I n t 1 } ; W H I L E I n t 0 ≤ V a r s D O d ← V a r d + I n t 1 } % A S T .
The definitions of P 0 and P 1 above are parameterized by a natural number v. Indeed, our definition only handle closed programs. Therefore, parameterizing the definition is a way to bypass this limitation and generalize input values. Now that we have defined the two programs to be related, we also need to write the actual oracle relating them. In the case of the R e n a m i n g language, it is a matter of exhibiting a bijection between the variable identifiers of both programs. In the Coq snippet above, φ is a total function mapping a to s and vice versa, while behaving as the identity for any other variable identifier. φ ′ is the same function, wrapped with a proof that it is indeed a bijection. Finally, given an initial value v, r e n a m i n g _ e x provides the initial configuration of the renaming oracle relating P 0 and P 1 . Now, this doesn't prove r e n a m i n g _ e x is a sound oracle relating P 0 and P 1 . In order to prove it, we have yet to prove the oracle language's invariant holds on that initial state. We can now import the relevant modules and write the programs that will be related by a S w a p A s s i g n oracle: x ← I n t 2 ;

D e f i n i t i o n

φ ( v a r : v a r i d ) : v a r i d : = m a t c h v a r w i t h | a = > s | s = > a | v a r = > v a

E x a m p l e

( x ← I n t 2 ;

W H I L E I n t 0 ≤ V a r a D O S e q ( x ← I n t 4 2 * V a r x ) ( a ← ( V a r a - I n t 1
(

W H I L E I n t 0 ≤ V a r a D O S e q ( a ← ( V a r a - I n t 1 ) ) ( x ← I n t 4 2 * V a r x ) ) } % A S T .
We can now define the initial state of the correlating oracle and prove it correct. To do so, we use the statement modifier structures from O r a c l e H e l p e r s to precisely locate the position of the assignments to be swapped.

Difference language on Imp

All the oracles presented so far in this chapter have been manually instantiated. However, as described in chapter 6, the underlying oracle languages can be used in a somewhat higher-level difference language, giving syntax to those oracle languages and allowing to compose them. What constitutes a difference language is formally defined in the module O r a c l e L a n g u a g e s . D i f f e r e n c e L a n g u a g e , and a toy difference language for Imp is defined by O r a c l e L a n g u a g e s . I m p . I m p D i f f e r e n c e L a n g u a g e .

To demonstrate how to use this difference language, we will describe the difference between the program P 0 from earlier and a program P 2 which is obtained by renaming some variable and fixing a crash:

S e c t i o n

D i f f e r e n c e L a n g u a g e .

I m p o r t

H I L E I n t 0 < V a r d D O { I F ( V a r x ) % ( V a r d ) = = I n t 0 T H E N s ← V a r s + V a r d E L S E S k i p ; d ← V a r d - I n t 1 } ; W H I L E I n t 0 ≤ V a r s D O d ← V a r d + I n t 1 } % A S T .
The difference between P 0 and P 2 is actually composed of two successive differences. We have already described the first one in the previous section, so we will just re-use the bijection φ ′ we had defined back then. The second difference is one that fixes a crash caused by a off-by-one error. Unfortunately, describing it is a bit more involved than we would hope, as one needs to prove that the loop does crash under given conditions. The C r a s h F i x W h i l e difference between P 1 and P 2 can then be defined by giving the location of the loop in the program, a bound on the number of steps needed for the loop to crash, and the proof that it does indeed crash. We can now describe the difference between P 0 and P 2 as a composition-using the C o m p o s e constructor-of the two previously-defined primitive differences-using the C o m p a r e constructor: Once defined, we yet have to prove that the difference δ is correct. Unlike previous proof scripts, this one is displayed in its entirety to give a sense of how involved the proof is, even though it is not expected from the reader to understand them completely. Basically,

{ I F ( V a r x ) % ( V a r d ) = = I n t 0 T H E N s ← V a r s + V a r d E L S E S k i p ; d ← V a r d - I n t 1 } % A S

D e f i n i t i o n

P ₁ _ l o o p _ c t x v : = C t x S e q R ( x ← I n t ( Z . o f _ n a t ( S v ) ) ) % A S T ( C t x S e q R ( s ← I n t 0 ) % A S T ( C t x S e q R ( d ← V a r x ) % A S T ( C t x S e q L C t x H o l e ( S e q ( W H I L E I n t 0 ≤ V a r s D O d ← V a r d + I n t 1 ) S k i p ) % A S T ) ) ) .

( * W e f i r s t h a v e t o p r o v i d e t h e i n t e r m e d i a t e e x e c u t i o n t r a c e

( * W e t h e n h a v e t o p r o v e t h e t w o d i f f e r e n c e s s e p a r a t e l y : * )

s p l i t ; a u t o . Since we are composing two differences, we have to provide the intermediate execution trace. That intermediate execution trace is that of P 1 v, the program obtained by renaming P 0 v. We then have to separately prove that the first difference relates the execution traces of P 0 v and P 1 v and that the second difference relates P 1 v and P 2 v.

Each one of this proof then follow the same pattern, mainly relying on the oracle's soundness.

Finally, we can superpose this difference with a more abstract one that is not backed by an oracle: let us state, in addition to the precisely-defined difference above, that the difference is between a program that does crash and one that does not. This last assertion is stronger than what C r a s h F i x W h i l e provides, as C r a s h F i x W h i l e merely states that some particular crash has been avoided, not that there is no crash whatsoever. To prove this difference correct, we have to prove that P 0 v does crash and P 2 v does not. Unsurprisingly, this is much more involved than the previous proofs, as the F i x C r a s h difference is more abstract and is not backed by an oracle language providing proof principles. In the following Coq code snippet, we omit the-quite long-proofs of P 2 _ d o e s _ n o t _ c r a s h and P 0 _ c r a s h e s , but not that of δ ′ Chapter 8

Related work

The formal study of equivalence between programs dates back at least to the sixties [START_REF] Igarashi | An axiomatic approach to equivalence problems of algorithms with applications[END_REF], while textual comparison of programs' source code dates at least as far as the seventies with the d i f f algorithm [START_REF] Wayne | An algorithm for differential file comparison[END_REF]. However, to the best of our knowledge, the earliest study of semantic differences between programs only dates back to 1990 and is due to Susan Horwitz [START_REF] Horwitz | Identifying the Semantic and Textual Differences Between Two Versions of a Program[END_REF] with an article in which she describes a static analysis technique to compare two programs. This comparison is performed on a structured intermediate representation-called Program Representation Graph-of those two programs. Our first contribution, described in Chapter 1, descends from this line of work, defining automatic static analysis which computes an over-approximations of the semantic differences of two programs.

However, for the most part, our thesis is focused on formally describing, reasoning about, and proving program semantic differences rather than automatically inferring them. Such formal comparisons of program semantics and reasoning about relational properties are the subject of various previous works, such as the formal framework of refinement mappings [START_REF] Lamport | The existence of refinement mappings[END_REF] allowing to prove that a program implements a given higher-level specification by translating states of the lower-level program to states of the higher-level specification, the formal proof system of relational Hoare logic [START_REF] Benton | Simple Relational Correctness Proofs for Static Analyses and Program Transformations (Revised, Long Version)[END_REF] adapting Hoare Logic to relational properties, and that of product programs [START_REF] Barthe | Relational verification using product programs[END_REF][START_REF] Barthe | Beyond 2-safety: Asymmetric product programs for relational program verification[END_REF][START_REF] Barthe | Product programs and relational program logics[END_REF] reducing proofs of relational properties to proofs on single programs. This last line of work is a major source of inspiration for our framework of correlating oracles, which we will compare more closely to the aforementioned works in the following sections.

Another close topic is that of tools allowing to describe or automate refactoring and program evolution. Such tools include RedBaron [START_REF] Peuch | RedBaron documentation[END_REF], an AST-level code transformation engine for Python, and Coccinelle [START_REF] Padioleau | SmPL: A domain-specific language for specifying collateral evolutions in Linux device drivers[END_REF][START_REF] Padioleau | Semantic Patches, Documenting and Automating Collateral Evolutions in Linux Device Drivers[END_REF], a program matching and transformation tool that defines semantic patches, source-level patches generalizing standard patches by abstracting details so that they can be applied to perform program transformations across a large code base, for instance transforming each call site when a function's interface changes. As we will see in the next section, though, semantic patches have a somewhat misleading name as they do not actually formally describe the semantic implications of those changes. Various Integrated Development Environments also include automated refactoring tools, but to the best of our knowledge, none of them is mechanically certified, save for a renaming refactoring tool [START_REF] Cohen | Renaming Global Variables in C Mechanically Proved Correct[END_REF] based on CompCert [START_REF] Leroy | The CompCert verified compiler[END_REF]. Furthermore, most of those refactoring tools have been shown [START_REF] Soares | Automated behavioral testing of refactoring engines[END_REF] to actually contain bugs.

All the works mentioned above are focused on comparing source-level changes, but there are also attempts at finding semantic differences between binary programs, such as the work of Gao et al. [START_REF] Gao | BinHunt: Automatically Finding Semantic Differences in Binary Programs[END_REF], matching the control-flow and call graphs of two binary programs by using a graph isomorphism algorithm and resorting to symbolic execution and automatic theorem proving to detect functionally-equivalent blocks of code.

Coccinelle and semantic patches

One line of work that frequently comes up when discussing semantic differences between programs is that of Coccinelle [START_REF] Padioleau | SmPL: A domain-specific language for specifying collateral evolutions in Linux device drivers[END_REF][START_REF] Padioleau | Semantic Patches, Documenting and Automating Collateral Evolutions in Linux Device Drivers[END_REF]'s semantic patches. Unlike what that name may suggest, though, this line of work is not directly related to our framework of correlating oracles or our difference languages. Indeed, Coccinelle's semantic patches are a generalization of textual differences, expressed on abstract syntax trees rather than lines of text. In that sense, semantic patches are indeed more focused on the semantics of a change than regular textual diffs, as they abstract away irrelevant details such as some variations in coding style, irrelevant code-thanks to an ellipsis construct-or choice of variable names-thanks to the use of metavariables. This is particularly useful to describe collateral evolution, that is, changes made to a codebase to accommodate some changes in the interface of a library. Furthermore, such generic patches can be inferred [START_REF] Andersen | Generic patch inference[END_REF] from collections of standard patches. Despite their name, though, semantic patches do not formally characterize the semantics of the changes they describe.

For those reasons, Coccinelle's semantic patches cannot be directly compared to our work, as our work is focused on formal semantics while Coccinelle is focused on matching and transforming abstract syntax trees. That being said, the work presented throughout this thesis is itself split into the semantics-oriented framework of correlating oracles and descriptive difference languages. It might be possible to define a difference language based on Coccinelle's semantic patches, or at the very least draw inspiration from it, but it would require a formal semantic interpretation of those patches. Doing so would enable certifying and verifying the correctness of such patches applied to a given program.

Correlating programs and speculative correlation

As repeatedly stated throughout this thesis, one major inspiration behind our work is that of Eran Yahav and Nimrod Partush [START_REF] Partush | Abstract Semantic Differencing for Numerical Programs[END_REF], describing a two-stages static analysis of pairs of programs consisting in first building a correlating program by statically interleaving instructions of two programs and then using abstract interpretation on the result to infer relational properties.

We discussed this paper in Chapter 1, exhibiting an issue making the interleaving of instructions unsound in some cases, and proposed an alternative algorithm for generating sound correlating programs.

In the meantime, Eran Yahav and Nimrod Partush moved away from correlating programs and the static scheduling they define: indeed, they published a follow-up paper [START_REF] Partush | Abstract Semantic Differencing via Speculative Correlation[END_REF] in which the abstract interpretation is not performed on a correlating program but directly on the pair of source programs. This analysis is still performed on an interleaving of both programs' instructions, but that interleaving is chosen dynamically by repeatedly comparing several interleavings and choosing the "most promising one" according to heuristics based on the state of the abstract interpretation.

It is difficult to directly compare this line of work with our framework of correlating oracles, as our focus is on specifying and verifying precise differences while Eran Yahav and Nimrod Partush's approach is to automatically infer relational properties. Nevertheless, it should be possible for the abstract interpretation tool to output its results as an oracle "certifying" the inferred properties by replaying the interleaving choices made during the speculative abstract interpretation and linking concrete executions to the abstract results. [START_REF] Person | Differential Symbolic Execution[END_REF] to automatically infer the semantic differences between programs using Symbolic Execution, generating function summaries and comparing them. Their technique exploits the similarity between programs by replacing common chunks of code with uninterpreted functions, thus avoiding costly symbolic execution of those chunks of code whenever they are executed in equivalent contexts. In some cases, it also allows bypassing some limitations of Symbolic Execution, for instance if those chunks of code contain loops which bounds are not statically known. Differential Symbolic Execution's results can be refined on demand if those abstracted code chunks are called in non-equivalent contexts.

Other automatic inference of program differences

Suzette Person et al. designed Differential Symbolic Execution

Shuvendu K. Lahiri et al. designed S y m D i f f [START_REF] Shuvendu | SYMDIFF: A Language-agnostic Semantic Diff Tool for Imperative Programs[END_REF], a tool that pairs supposedlyequivalent functions of two programs and uses Satisfiability Modulo Theories (SMT) solvers to attempt to prove them equivalent. Failing that, it produces counter-examples of execution paths leading to different results.

Product programs

The other major inspiration to our work, that we have covered in Chapter 2, is Barthe et al.'s work on Relational Hoare Logic and Product Programs [START_REF] Barthe | Product programs and relational program logics[END_REF]. Product programs are similar to correlating programs in that they statically interleave instructions of a pair of programs to reduce relational analysis to non-relational analysis. However, they enjoy a very syntactic formal definition strongly related to the rules of Relational Hoare Logic, rules which are described in the original article as well as in Chapter 2. In particular, product programs, like correlating programs, define a static scheduling, but that scheduling is directed by the relational semantic property to be proved.

Chapter 5 is dedicated to encoding Relational Hoare Logic in our framework of correlating oracles. In that chapter, we described how to encode Minimal Relational Hoare Logic, Core Relational Hoare Logic and Core Relational Hoare Logic extended with self-composition in our framework, proving the soundness of those logics through proofs on the oracle languages encoding them. However, we have not described how product programs relate to correlating oracles. Indeed, product programs cannot be directly encoded in our framework. Intuitively, the reason for that is that product programs may still crash without executing both programs to completion whenever one of the underlying program crashes or one of the assumption is broken. In other words, product programs can only be seen as valid oracles if they do not crash. It would surely be possible to encode product programs in our framework under that assumption, but we decided against due to the amount of work it would require and due to the fact that it would be almost functionally equivalent to the oracles encoding Relational Hoare Logic itself.

In other works [START_REF] Barthe | Formal certification of code-based cryptographic proofs[END_REF][START_REF] Barthe | Coupling proofs are probabilistic product programs[END_REF], Barthe et al. have moved to reasoning about pairs of probabilistic programs. To do so, they designed probabilistic Relational Hoare Logic in order to reason on distributions rather than memories. This is particularly useful to prove security properties on cryptographic code. Unfortunately, our framework was not designed with probabilistic programs in mind. Furthermore, it is not completely obvious to us how to handle the probabilistic case. It seems reasonable for a correlating oracle between probabilistic programs to be probabilistic itself, but we also need ways to reason about the distributions.

Bisimulation

In the field of concurrency, that is, the study of programs containing parts that can be executed independently in different orders, equivalent programs are often characterized by the notion of bisimulation relations. A bisimulation is a binary relation between labelled state transition systems (LTS), relating systems that have identical observable behavior. A LTS is a system made of a set of states, a set of labels, and a set of labelled transitions from a state to another.

More formally, a labelled transition system is defined by a triple (S, Σ, →), where S is the state of states, Σ is the set of labels, and → the set of labelled transitions, that is, a subset of S × Σ × S. A transition from a state s to a state s ′ with label α is written s α → s ′ .

Comparing bisimulations to our work is especially hard as our setting does not fit that of concurrent programming. Indeed, the programming languages that can currently be described in our framework are deterministic and do not define observable transitions-program transitions are between two states and are not labelled.

Nonetheless, we could imagine encoding Labelled state Transition Systems within our framework.

A possible encoding of deterministic LTS would involve defining program configurations as pairs (s, ρ) ∈ S × Σ ω of an LTS state s and a potentially-infinite list ρ of upcoming transition labels. The transition function E of such programs would consume a label from the potentially-infinite list and select a transition accordingly, that is:

E(_, (s, α • ρ)) = (s ′ , ρ) ⇔ s α → s ′
Finitely branching nondeterminism could then be recovered by using a powerset construction, with each program configuration being a pair (s, ρ) ∈ 2 S × Σ ω of a set of LTS states s and a potentially-infinite list ρ of upcoming transition labels. The transition function E would then be defined such that:

E(_, (s, α • ρ)) = ({q | p ∈ s ∧ p α → q}, ρ)
In that setting, an oracle encoding bisimulations would execute left and right programs in lockstep, maintaining a single list of upcoming labels as well as a pair of LTS states-or, if using the powerset construction, a set of pairs of LTS states. That is, the type of oracle states would be S × S × Σ ω -or, if using the powerset construction, 2 S × 2 S × Σ ω . The oracle's invariant would simply assert that every pair of left and right states are bisimilar. In this sense, our framework is expressive enough to express bisimulations, but the encoding relies on the very definition of bisimularity and does not provide any direct insight.

In [START_REF] Franck Van Breugel | A behavioural pseudometric for metric labelled transition systems[END_REF], the notion of bisimilarity is generalized by quantifying the difference between Metric Labelled Transition Systems as a non-negative real number, such that the distance between two states is zero if and only if those two states are bisimilar. We cannot think of any direct relation between their approach and our own, as their approach is quantitative whereas ours is qualitative.

Refinement mappings

Another way of describing semantic relations between close programs is by projecting or mapping the states of a first program to states of a second program [START_REF] Simon | Protocol verification via projections[END_REF][START_REF] Lamport | Specifying concurrent program modules[END_REF]. More precisely, Abadi and Lamport [START_REF] Lamport | The existence of refinement mappings[END_REF] define a refinement mapping as a function transforming a program's states into another program's such that every behavior-that is, possible sequence of states-of the first program translates to a behavior of the second program. This can be an efficient technique to prove that a low-level program implements a higher-level program, as the existence of a refinement mapping which preserves external-or observable-states across the translation suffices to prove inclusion of observable behaviour.

However, this technique may not be directly applicable to some pairs of programs, as the lower-level and higher-level programs may have "incompatible" internal states, with the higher-level specification holding more information, or performing its computations in a more granular way. To address this limitation, Abadi and Lamport [START_REF] Lamport | The existence of refinement mappings[END_REF] propose adding auxiliary variables-known as history variables and prophecy variables-to the low-level program so that a refinement mapping can be found. They then state sufficient properties to the existence of a refinement mapping between a low-level program extended with auxiliary variables and a high-level program.

This work is a bit difficult to compare to our framework of correlating oracles for a few reasons: on the one hand, refinement mappings deal with non-deterministic programs whereas our framework only handles deterministic programs-we will elaborate on this limitation in the conclusion of this thesis. On the other hand, the framework of refinement mappings only deal with behavior inclusions while correlating oracles may describe all sorts of relations, including between programs with different behaviors. Another significant difference between both frameworks is the fact that refinement mappings separate program states in external and internal program states, a distinction that our framework does not do. This, however, can be encoded in the oracle's invariant by explicitly partitioning the variables into external and internal variables.

With these considerations out of the way, a refinement mapping-without resorting to auxiliary variables-between two deterministic programs can probably be encoded as an oracle in the following manner: a single step of the oracle would perform a single step of the low-level program and the second program's state would be retrieved by applying the refinement mapping to the low-level program's state. It may cause stutter in the second program, but that is allowed in our framework.

However, as stated earlier, there doesn't always exist a direct mapping from a lowlevel program to a higher-level program. Abadi and Lamport deal with this limitation by adding history and prophecy variables to the low-level program, which results in another program with the same external behavior but a larger state space. Encoding this as an oracle between the unmodified low-level program and the higher-level program can then be performed by stepping in the annotated low-level program in the same way as described earlier, and simply erasing the history and prophecy variables when projecting back to the unmodified low-level program.

Conclusion Contributions

Throughout this thesis, we studied the semantics of program changes from different angles. We first approached the problem of automatically inferring simple relational properties from a pair of programs. In doing so, we identified a flaw in a previous publication by Eran Yahav and Nimrod Partush [START_REF] Partush | Abstract Semantic Differencing for Numerical Programs[END_REF] and proposed an alternative, mechanically-checked algorithm addressing this issue.

We then shifted our focus to specifying and verifying possibly elaborate relational properties, which lead to our main contribution: a formal framework to precisely characterize the semantics of program changes. Drawing inspiration from various publications [START_REF] Partush | Abstract Semantic Differencing for Numerical Programs[END_REF][START_REF] Barthe | Product programs and relational program logics[END_REF], this framework of correlating oracles gives patches a small-step semantics which enables constructively building a relation between the two program's traces. This framework is meant to be used as a building block for writing descriptive and verifiable difference languages for programmers. We formalized this framework in the Coq proof assistant.

We also wrote a set of fully-formalized correlating oracle languages for the toy imperative language Imp covering various classes of semantic differences. Those difference classes range from minor syntactic changes preserving the overall semantics of the programs-like swapping two independent assignments-to fixing crashes by adding defensive conditions.

In order to evaluate the expressivity of our framework, we successfuly encoded several variants of Relational Hoare Logic as oracle languages. In doing so, we gave small-step semantics to Relational Hoare Logic proofs and provided new mechanicallychecked proofs of soundness of those Relational Hoare Logic variants.

Finally, we designed a toy difference language for Imp illustrating how to make use of the aforementioned oracles.

Limitations Completeness of a difference language

A first limitation of our difference language approach is that such difference languages are not typically complete. Indeed, only differences fitting already-identified difference classes implemented into that difference language can be represented this way. For 121 instance, the toy difference language for Imp presented in Chapter 6 allows precisely describing some changes preserving the program's control-flow, but only if those changes conform to the very strict syntactic criterion given in Chapter_4. This limitation can be worked around by providing more generic difference primitives. However, such difference primitives are usually either less precise, or require more input from the programmer. This is for instance the case of the A b s t r a c t E q u i v oracle language-and the associated ensure equivalence at C primitive of the difference language-defined in Chapter 4, which allows relating two equivalent programs made of syntactically-different subprograms embedded in syntactically-equal contexts, provided that they come with a proof that the two sub-programs are extensionally equivalent.

Scaling to realistic languages

A related limitation is the possibly prohibitive amount of upfront work needed to design a difference language. Indeed, designing a few oracle languages for Imp-and proving them sound-has proven to be a significant undertaking.

Designing such a difference language involved identifying interesting classes of program modifications, characterizing their semantics through an oracle language, and designing a proper syntax for use by programmers.

Unfortunately, each of these steps is bound to get significantly more challenging and time-consuming when considering realistic programming languages. Indeed, categorizing and identifying common and useful classes of program differences is in itself a substantial task, and the number of such classes is likely to depend on the complexity of the programming language. Furthermore, the amount of work needed to define and prove each oracle language is heavily dependent on the number of reduction rules of the programming language, with in places a number of cases that is quadratic in the number of reduction rules, as oracles relate pairs of programs.

For our approach to scale to real-world usages, more efficient ways of writing oracle languages are needed. Our experience designing oracle languages for Imp suggests that some common patterns could be factored out, as we have done to some extent with the helper function S H e l p e r defined in Chapter 4. Continuing on this direction, it might be possible to write useful "oracle language combinators", allowing to refactor more common patterns in oracle languages.

Non-determinism

Our framework only considers languages with deterministic small-step semantics. However, many real-world languages have non-deterministic semantics, and are thus not directly supported by our framework.

While the reasons for this restriction are mostly historic, there are a few fundamental questions worth considering when dealing with non-deterministic correlating oracles. Indeed, should left and right projections of an oracle cover every possible left and right program behaviors? Should it cover every possible behavior on one side and only a subset of the other's? Should it cover every pair of program behaviors?

The answer to those questions is probably going to depend on the particular use case. For instance, if we are interested in showing that two programs have the same possible outcomes, an oracle should cover every possible left and right program behaviors. However, if we are interested in proving that a program is an optimized version of an original program, the oracle should probably cover every possible behavior of the optimized program but not necessarily those of the original one.

Since different answers are possible for those questions, more work is needed in order to figure out which of the above combinations make sense and how they can be integrated in our framework.

That being said, bounded non-determinism can be encoded within our framework using a powerset construction, such as described in Chapter 8 when comparing our work to the notion of bisimulations.

Other perspectives Automatic inference

As stated repeatedly throughout this manuscript, the issue of automatically inferring differences has been set aside when designing correlating oracles. Therefore, they may not be well-suited for automatically analyzing program differences without human intervention.

Inferring differences between two close programs may be possible, though. In particular, Integrated Development Environments could use heuristics to figure out which changes a programmer is performing as they type. Furthermore, such Integrated Development Environments often include refactoring tools, which could be extended to produce correlating oracles certifying the refactoring operations performed.

Version Control Systems

Another possible use-case for semantic patches such as those proposed in this manuscript is merging different branches in a version control system. Indeed, a common operation in version control systems is merging two different changes-for instance, the addition of two different features-back into a single program. The merge operation is usually done on a textual level and will, if possible, apply both changes to the common ancestor. In case that isn't possible, the programmer is requested to manually resolve merge conflicts, that is, manually edit the portions of source code modified by both changes.

However, even when two different changes do not modify the same lines, and are thus automatically merged by the version control system, those changes may have deep semantic consequences, leading to inconsistent semantics.

Therefore, there is an opportunity for semantic merges, and having semantic description of program changes is a first step towards handling them.

1 l , s 2 l 1 r , s 2 r

 1212 Le schéma suivant illustre l'exécution d'un exemple d'oracle-dont les états successifs sont o 1 , o 2 etc.-ainsi que des programmes gauche-dont les états successifs sont s , etc.-et droite-s , etc.-mis en relation. Les flèches représentent des réductions, et les lignes pointillées les relations entre états induites par un état d'oracle :

}

  Given those two programs, c c c produces the following correlating program, in which G u a r d is a type for boolean values encoding the control flow:C o r r e l a t i n g p r o g r a m

c

  ::= a | c; c | while (b) c | if (b) c else c (Commands) a ::= skip | x = e | break | continue (Atomic commands) b ::= true | false | b && b | !b | e ≤ e (Boolean Expressions) e ::= x | n | e + e (Arithmetic Expressions)

and s ′ 2 =

 2 π R (o), and o ′ = o. In the other case, with n > 0, there are two subcases: • Either (g, o) ̸ ∈ dom(S), in which case π L (o) and π R (o) are, by the oracle's completeness condition, stuck states, and thus are equal to s ′ 1 and s ′ 2 respectively, and S ′n (g, o) = o. • Or (g, o) ∈ dom(S), which is a bit more involved. Indeed, in this case, we have S ′n (g, o) = S n-1 (g, S(g, o)) and, before being able to use the induction hypothesis, we need to handle this first oracle step, which generates three more subcases as the oracle may simulate steps in the left program, in the right program, or in both programs in a single step. Each of these subcases involves subtracting to n 1 and n 2 the number of steps predicted by the oracle in the corresponding programs, then use the induction hypothesis accordingly.

}

  In that example, the variables dynamically affected by this change are x and p o w , and the control flow is provably preserved, since the only conditional expression (0 < c o u n t ) does not depend on x nor on p o w .

Figure 4

 4 Figure 4.1.

  y ∈ vars(b) ⇒ y ̸ ∈ x assert (b) ≡ x assert (b) Control-Same-Assign ∀ y, y ∈ vars(e) ⇒ y ̸ ∈ x x = e ≡ x x = e Control-Diff-Assign y ∈ x vars(e 1 ) = vars(e 2 ) divs(e 1 ) = divs(e 2 ) y = e 1 ≡ x y = e 2 Control-Halt halt ≡ x halt Control-Cmd

Figure 4 . 1 :

 41 Figure 4.1: Syntactic criterion implying preserved control-flow

R e f a

  c t o r C o m m o n B r a n c h R e m a i n d e r could be:

  w a p B r a n c h e s oracle language, R e f a c t o r C o m m o n B r a n c h R e m a i n d e r makes use of the S H e l p e r function with the empty type as the type β of actual continuationlevel changes. The type α of actual statement-level changes is the singleton unit, as R e f a c t o r C o m m o n B r a n c h R e m a i n d e r only handles one kind of change. Definition 26 (R e f a c t o r C o m m o n B r a n c h R e m a i n d e r language on Imp). The oracle language R e f a c t o r C o m m o n B r a n c h R e m a i n d e r on Imp is defined by the oracle language definition

  on the top of the continuation modifier list, then the oracle have to interpret a single step in the left program while not stepping in the right program. Conversely, if U R is on the top, it means that the oracle has to step in the right program without stepping in the left one.

  R e f a c t o r C o m m o n B r a n c h R e m a i n d e r , left and right programs might crash in the middle of those two simulated steps, as they are performing assignments. As with R e f a c t o r C o m m o n B r a n c h R e m a i n d e r , this needs to be taken care of and is handled using an extra state constructor encoding crashed executions. As an illustration, consider the following diagram describing an execution of the oracle in which the expression e cannot be evaluated:

1 γ∼ T 2

 12 Definition 36 (γ-correlations). Let γ be a relation over program configurations. A relation ρ is a γ-correlation if it relates pairs of traces from which two sub-sequences of configurations are pointwise related by γ i.e. T 1 ρT 2 implies that T , where γ ∼ is coinductively defined as:

  Definition 39 (ρ O,g,o ). An oracle written in a language O = (G, O, S, π ′ L , π ′ R , π L , π R , I) and with a fixed global environment g ∈ G and an initial dynamic state o ∈ O defines a trace relation as follows:

2 .

 2 The difference fix with defensive condition at C is a local program transformation that inserts a conditional statement at a source program location characterized by C which precedes a statement c that triggers a crash. This conditional statement makes the evaluation of the target program avoid the evaluation of the statement c.3. The difference change values of x is a program transformation which modifiesthe assignments of any variable in x in the source program provided that this variable has no influence on the control flow. This category could be extended by any program transformation whose impact on the program behaviors can be characterized statically.

R e q u i r e I m p o r

  t O r a c l e L a n g u a g e s . C o m m o n .R e q u i r e I m p o r tO r a c l e L a n g u a g e s . P r o g r a m m i n g L a n g u a g e .

L e m m a e

  x _ s t a t e _ f i n a l _ n o _ s t

O r a c

  l e L a n g u a g e s . I m p . L a n g : c l e L a n g u a g e s . I m p . L a n g .

  . L a n g . M a k e V a r _ a s _ D T .

  r e ) .• An Imp program is a statement, p r o g i m p _ l a n g u a g e = c m d .• The initial state of an Imp program is the pair of a continuation made of that program and of the empty memory: i n i t i a l _ s t a t e i m p _ l a n g u a g e p = ( υ , ( [ p ] ,

R

  e q u i r e O r a c l e L a n g u a g e s . I m p . O r a c l e s . R e n a m i n g . M o d u l e R e n a m i n g : = O r a c l e L a n g u a g e s . I m p . O r a c l e s . R e n a m i n g . M a k e V a r _ a s _ D T I m p .

  . S m a l l S t e p . S y n t a x . N o t a t i o n s .

R e q u i r

  e O r a c l e L a n g u a g e s . I m p . O r a c l e s . O r a c l e H e l p e r s . M o d u l e O r a c l e H e l p e r s : = O r a c l e L a n g u a g e s . I m p . O r a c l e s . O r a c l e H e l p e r s . M a k e V a r _ a s _ D T I m p . R e q u i r e O r a c l e L a n g u a g e s . I m p . O r a c l e s . S w a p A s s i g n . M o d u l e S w a p A s s i g n : = O r a c l e L a n g u a g e s . I m p . O r a c l e s . S w a p A s s i g n . M a k e V a r _ a s _ D T I m p O r a c l e H e l p e r s .

S e c t i o n S w a

  p A s s i g n E x a m p l e . . S m a l l S t e p . S y n t a x . N o t a t i o n s .I m p o r tS w a p A s s i g n .I m p o r tO r a c l e H e l p e r s .E x a m p l e s w a p _ e x a m p l e :

I m p o r

  t I m p D i f f e r e n c e L a n g u a g e .

E

  x a m p l e P ₁ _ l o o p _ b o d y : =

E x a m p l e c r a s h _ f i

  l o o p _ b o d y _ c r a s h e s .

  D i f f e r e n c e L a n g u a g e . t : = C o m p o s e ( C o m p a r e r e n a m i n g ) ( C o m p a r e ( c r a s h _ f i x v ) ) .

  s o u n d _ p r o g r a m _ d i f f e r e n c e asserts that the interpretation of the given difference (δ v) is indeed a relation between the execution traces of the left (P 0 v) and right (P 2 v) programs.I m p o r t O r a c l e L a n g u a g e s . D i f f e r e n c e L a n g u a g e . I m p o r t O r a c l e L a n g u a g e s . R e d u c t i o n T r a c e . I m p o r t O r a c l e L a n g u a g e s . R e d u c t i o n T r a c e s R e l a t i o n . L e m m a δ _ s o u n d : ∀ v , s o u n d _ p r o g r a m _ d i f f e r e n c e _ _ i m p _ d i f f e r e n c e _ l a n g u a g e

  p o s e _ t r a c e _ r e l a t i o n s _ e x t e r n a l l y .e x i s t s( p r o g r a m _ t r a c e i m p _ l a n g u a g e ( P ₁ v ) ) .

s i m p l . u n f o l d p r o g r a m _ t r a c e . s i m p l . r e p e a t s p l i t ; t r y a p p l y t r a c e F r o m _ t r a c e . a p p l y C r a s h F i x W h i l e . c m d _ c o n t ; a u t o u s i n g C r a s h F i x W h i l e . k m _ i n v a r i a n t . d o 4 (

 4 c l e _ f r o m _ p r i m i t i v e _ d i f f . c l e L a n g u a g e . o r a c l e _ c o r r e l a t i o n _ r e l a t i o n . c l e _ f r o m _ p r i m i t i v e _ d i f f . s i m p l . r e w r i t e b e q _ c m d _ r e f l x . s i m p l . c l e L a n g u a g e . o r a c l e _ c o r r e l a t i o n _ r e l a t i o n . a p p l y C r a s h F i x W h i l e . m o d _ r e c _ s e q ; a u t o u s i n g C r a s h F i x W h i l e . m o d _ i d ) . a p p l y C r a s h F i x W h i l e . m o d _ s p e c i a l ' . Q e d .

  D i f f e r e n c e L a n g u a g e . t : = S u p e r p o s e ( C o m p a r e F i x C r a s h ) ( C o m p o s e ( C o m p a r e r e n a m i n g ) ( C o m p a r e ( c r a s h _ f i x v ) ) ) .

_ s o u

  n d , which simply leverage those two proofs and the previous proof on δ. e p s _ c r a s h i n g _ t r a c e n ( p r o g r a m _ t r a c e i m p _ l a n g u a g e ( e p s _ c r a s h i n g _ t r a c e n ( p r o g r a m _ t r a c e i m p _ l a n g u a g e ( n d _ p r o g r a m _ d i f f e r e n c e _ _ i m p _ d i f f e r e n c e _ l a n g u a g f e r e n c e L a n g u a g e .

  [START_REF] Barthe | Product programs and relational program logics[END_REF]. A novel formal framework for describing differences in program semantics, formalized as a Coq library with mechanically-checked theorems. In this frame-The small-step execution of that third program describes the relation between the execution traces of the two programs under consideration by pairing some of their intermediate states, asserting a formal invariant on each such pair. The framework guarantees that this invariant holds for every such pair if it holds on the initial state of the programs. Compared to previous work such as product programs, this approach enables reasoning about non-terminating and crashing programs. 4. A collection of fully-formalized oracle languages making use of this framework

work, a difference between two programs is represented by a third program INTRODUCTION called a correlating oracle.

  Definition 1 (Guard identifier independence). A guard g is independent for a path π, written g#π, if g does not end with π.

	o) is a guarded program simulating a sub-program c at path π in a
	larger program ; ⃗ g ∧ is the guard conjunction guarding c in this larger program, and o
	is a loop marker used to indicate the innermost (if any) loop of the larger program
	under which c is executed. This loop marker equals "Some π ′ " if the innermost loop
	containing "c" is rooted at path π ′ and "None" if there is no such loop. o is used in the
	translation of break and continue statements by keeping track of the guard variables π ′
	and 1 • π ′ controlling the execution of the innermost loop.
	The path π is used to name fresh guard variables, linking every guard variable back
	to the position of the corresponding condition in the original syntax tree, ensuring
	freshness, and enabling reasoning about sub-programs in isolation thanks to the
	notion of guard identifier independence defined below:
	Let us quickly go over each case of the translation function CI:
	• As a skip has no effect, it does not matter what it is guarded by. Therefore, for
	simplicity's sake, the translation of a skip is simply a skip, no matter what the
	other parameters are.

  the above diagram, the correlating oracle state o 1 relates the left program state s 1 l with the right program state s 1 r . A single oracle computation step from o 1 then leads to the oracle state o 2 , which relates the left program state s 2 Note that the oracle "skipped" the left program state s 2 r , not putting it in relation with any left program state. This ability is especially useful to "ignore" intermediary steps and highlight locally-equivalent ones whenever two programs compute the same result in two different ways. Back to the example, a single computation step from oracle state o 2 leads to oracle state o 3 , relating program states s 3 l and s 3 r . In this case, the oracle did not simulate any right program step, and s 3 r is related both to s 2 l and s 3

	program state s 3 r .
	l to the right
	53

  preservation of the universal oracle). Invariant preservation is immediate, as in the Identity oracle's case, since the oracle's invariant is always satisfied.Lemma 7 (Prediction soundness of the universal oracle). Soundness of the universal oracle is guaranteed by each oracle step corresponding to exactly one step of at least one of the two underlying programs.

	Lemma 8 (Prediction completeness of the universal oracle). Prediction completeness
	of the universal oracle is immediate as it keeps executing as long as at least one of the
	underlying programs keep executing.

Table 7 .

 7 2: c o q w c output for O r a c l e L a n g u a g e s

	Path in the archive	Lines of specification Lines of proof
	coq/	575	594
	coq/Oracles/	79	32
	coq/Imp/	588	897
	coq/Imp/Hoare.v	68	38
	coq/Imp/RHL.v	183	0
	coq/Imp/Oracles/	2640	6077
	coq/Imp/ImpDifferenceLanguage.v	222	0
	coq/Paper.v	475	348
	Total	4830	7986

  Another simple oracle is the S w a p A s s i g n oracle. Compared to R e n a m i n g , it is simpler to use, but it makes use of the O r a c l e H e l p e r s module internally. For this reason, we also have to provide O r a c l e H e l p e r s when instantiating S w a p A s s i g n .

	P r o o f .
		s i m p l .	s p l i t	;	a u t o .
		i n t r o	x .	s y m m e t r y .	r e w r i t e	( r e n a m e _ E q u a l	φ )	;	a u t o .
		d e s t r u c t	φ '	a s	[ φ ' '	H ]	e q n : H φ ' .
		u n f o l d	φ '	i n	H φ ' .	i n v e r s i o n	H φ ' .	s u b s t	φ ' ' .	a u t o .
	Q e d .
	E n d	R e n a m i n g E x a m p l e .
	7.2.3.2 Independent assignment swapping
	r e n a m i n g _ e x _ 1	v :
	i n v a r i a n t	r e n a m i n g _ o r a c l e	( f s t	( r e n a m i n g _ e x	v ) )	( s n d	( r e n a m i n g _ e x	v ) ) .

We avoid the term "semantic patches" so as to not create confusion with Coccinelle[START_REF] Padioleau | Semantic Patches, Documenting and Automating Collateral Evolutions in Linux Device Drivers[END_REF][START_REF] Chr | Clang and Coccinelle: Synergising program analysis tools for CERT C Secure Coding Standard certification[END_REF], which takes a different approach, as described in Chapter 8

m s 4 m s 5 m En En En En

https://www.irif.fr/~thib/oracles/oracles.tar.xz

https://opensource.org/licenses/BSD-3-Clause 101

Acknowledgments & Remerciements

In this case, the two loops' bodies are two extensionally-equivalent sub-programs enclosed in syntactically-equal contexts. The syntax for primitive differences enumerates a collection of builtin differences.

Syntax

Statement contexts

Code metrics and layout

The O r a c l e L a n g u a g e s library is written for Coq 8.6 and depends on no additional library. It is composed of meta-theoretical definitions and proofs on programming languages and oracle languages, generic oracle languages (the identity and universal oracle language), a formal definition of Imp and several oracle languages specific to that language.

The following table gives a more detailed overview of the source code, listing source files along with a short description and the chapter of the corresponding chapter of the thesis: Overall, the whole Coq development is about 5000 lines of definitions and 8000 lines of proofs. About 6000 lines of those proofs are about individual oracle languages for Imp, and are not particularly well factorized. The individual oracle languages also concentrate a fair portion of the specifications. A more precise overview of the lines