JFLA 2023

Monadic programming is a popular way to embed effectful computations in purely functional languages. In particular, the so-called free-monad comes with the promise of extensibility and modularity: computations are seen as syntax arising from a signature of operations they may perform. Popularized in a programming context, the approach is nowadays used for verification in proof assistants as well, as witnessed by frameworks such as FreeSpec or Interaction Trees.

In this work in progress, we investigate the following question. Can we type each subcomputation with their minimal valid operation signature, and seamlessly combine all these monadic computations of different natures? Furthermore, can we leverage this additional precision in typing to derive monadic invariants for free?

We answer positively by suggesting two simple ideas. First, a bind operation between computations living in distinct monads can be defined by transporting them through monad morphisms. Second, to give more structure to the monads we manipulate by indexing them by a semi-lattice as a means to automatically infer the adequate morphisms. We illustrate the benefits on a minimal Coq example: a computation interacting with a memory cell.

TreeSync est un sous-protocole d’authentification pour MLS, un protocole de messagerie de groupe sécurisé en cours de standardisation à l’IETF. Nous formalisons MLS en F∗, et présentons un théorème de sécurité pour TreeSync à l’aide du cadriciel de cryptographie symbolique DY∗. Afin de comprendre les hypothèses clés qui permettent d’exprimer un tel théorème, nous présentons en détail le fonctionnement interne de DY∗. Au cours de notre analyse, nous avons proposé plusieurs changements à TreeSync qui ont été intégrés à MLS, et avons développé de nouvelles méthodes de preuves pour passer à l’échelle avec DY* afin de pouvoir s’attaquer à un gros protocole comme MLS, par exemple, un mécanisme permettant à la fois l’exécution concrète et symbolique du protocole, la génération automatique de parseurs et sérialiseurs binaires vérifiés, ou encore la génération d’invariants globaux du protocole à partir d’invariants locaux.

Usually, the description of nuclear equipment by the FMEA (Failure Mode and Effects Analysis) method can be of considerable length (up to 5,000 lines); on the other hand, the number of rules used for the verification of this equipment is small. In addition, upstream, there is the question of trust in the tools that generate these descriptions for complex equipment, that is to say, made up of several thousand objects (requirements, functions, interfaces, behaviors).

Our objective is to formally prove in the Coq proof assistant the accuracy and exhaustiveness of the safety analysis for these nuclear equipments, by proposing a more modular and more abstract framework which is based on an axiomatic description of the systems. - these axioms being either accepted or proven independently of the verification itself. The very nature of the inductive types of Coq is perfectly suited to the description of complex systems, which are systems of systems in interaction. We have a first prototype that demonstrates the feasibility of this approach, for simple properties which are effectively proven by reflection - for example, the study of flows, which must first be produced and then consumed exactly once in the whole system.

We open the way to a general approach for the proofs of the properties of a (model of) systems and study the kind of properties that can be demonstrated in this way. Finally, we propose the approach for faithful translation of a DSL (domain-specific language) tool into Coq and the proof of its correctness.

François Pottier’s unionFind library is parameterized over an underlying store of mutable references, and provides the usual references, transactional reference stores (for rolling back some changes in case of higher-level errors), and persistent reference stores. We extend this library with a new implementation of backtracking reference stores, to get a UnionFind implementation that efficiently supports arbitrary backtracking and also subsumes the transactional interface.

Our backtracking reference stores are not specific to unionFind, they can be used to build arbitrary backtracking data structures. The natural implementation, using a journal to record all writes, provides amortized-constant-time operations with a space overhead linear in the number of store updates. A refined implementation reduces the memory overhead to be linear in the number of store cells updated, and gives performance that match non-backtracking references in practice.

Ces dernières années, le nombre d’assistants à la preuve, de prouveurs automatiques et de vérificateurs de preuve n’a cessé de croître. L’un d’entre eux, le framework logique Dedukti, a pour objectif de rendre ces outils formels interopérables, c’est-à-dire rendre possible la réutilisation des preuves d’un outil A dans un outil B. Un autre outil formel, Metamath, a la particularité d’être à la 4e place dans la liste des systèmes possédant le plus grand nombre de preuves parmi la liste des 100 théorèmes à prouver de Freek Wiedijk, tout en étant constitué de très peu de fonctionnalités : pas de type dépendant, pas de polymorphisme, ni de notion d’univers. Afin d’agrémenter le nombre de preuves qu’il est possible de traduire dans Dedukti, nous présentons Mathiilde, un traducteur automatique de Metamath vers Dedukti. Comme ce traducteur peut utiliser deux encodages différents de Metamath vers Dedukti, nous discutons les avantages et les inconvénients du point de vue de l’interopérabilité.

Deductive verification enables one to check that a program satisfies its specification. There are mainly two approaches: either the user provides invariants in the form of annotations and use a tool to extract proof obligations, like in, e.g., Why3; or the user verifies the program through interactive proofs, like in, e.g., CFML, by providing invariants during the proof steps.

We are interested in expressing in Coq the representation of a program, accompanied with not only its invariants but also its proof terms. Concretely, we present an AST for representing source code and specification in a deep embedding style, and embedded lemmas in shallow embedding style. Such lemmas can be established using the full capabilities of the prover.

We develop a way to build these ASTs from source code using CFML-style interactive tactics. We also develop a way to build these ASTs by extracting proof obligations from source code already annotated with its invariants. Besides, we provide a way to validate our ASTs by reifying them as Coq proof terms.

This work is a first step towards a long term project to devise a trustworthy, user-guided, source-to-source optimization framework. On the one hand, we may need to exploit invariants to justify the correctness of code transformations. On the other hand, to be able to chain transformations, we also need every transformation to update the program annotations.

ML modules are offer large-scale notions of composition and modularity. Provided as an additional layer on top of the core language, they have proven both vital to the working OCaml and SML programmers, and inspiring to other use-cases and languages. Unfortunately, their meta-theory remanins difficult to comprehend, requiring heavy machinery to prove their soundness. Building on a previous translation from ML modules to Fω, we propose a new comprehensive description of a generative subset of OCaml modules, embarking on a journey right from the source OCaml module system, up to Fω, and back. We pause in the middle to uncover a system, called canonical that combines the best of both worlds. On the way, we obtain type soundness, but also and more importantly, a deeper insight into the signature avoidance problem, along with ways to improve both the OCaml language and its typechecking algorithm.

In the realm of the proofs-as-programs correspondence, continuation-passing style (CPS) translations are known to be twofold: they bring both a program translation and a logical translation. In particular, when using the former to compile a language with a control operator, the latter ensures the soundness of the compilation with respect to types.

This work is inspired by Oliva and Streicher, who explained how Krivine realizability could be rephrased as the composition of a CPS and an intuitionistic realizability model. In this paper, we propose to push one step forward the analysis of the relation between realizability models and CPS translations to investigate the following question: assume that two realizability models are defined using the source and the destination of a CPS translation, is it the case that the CPS translates realizers of a given formula into realizers of the translated formulas?

Afin de prévenir les erreurs de programmation, des analyseurs statiques ont été développés pour de nombreux langages; cependant, aucun analyseur mature ne cible l’analyse de valeurs pour un langage fonctionnel à la ML. Des outils de vérification pour ces langages existent, tels les systèmes de types classiques ou les méthodes déductives, mais le raisonnement automatique sur des programmes numériques a jusqu’alors été peu exploré. Cet article décrit un analyseur statique de valeurs par interprétation abstraite pour un langage fonctionnel typé du premier ordre, approche sûre et automatique pour garantir l’absence d’erreurs à l’exécution. En se basant sur des domaines abstraits relationnels et en réalisant des résumés des champs récursifs des types algébriques, cette approche permet d’analyser des fonctions récursives manipulant des types algébriques récursifs et d’inférer dans un domaine abstrait leur relation entrée-sortie. Une implémentation est en cours sur la plateforme d’analyse multilangage MOPSA et analyse avec succès de courts programmes de quelques lignes. Ce travail ouvre ainsi la voie vers une analyse de valeurs précise et relationnelle basée sur l’interprétation abstraite pour les langages fonctionnels d’ordre supérieur à la ML.

This paper describes a method to define a correct abstract interpretation from a formal description of the semantics of a programming language. Our approach is based on Skeletal Semantics. We extend it with a notion of program points, in order to differentiate two fragments of the program that are syntactically equivalent but appear at different locations. We introduce a methodology for deriving an abstract interpretation from a Skeletal Semantics that is correct by construction: given a program, abstract states are computed for each program points. We apply our method by defining a Control Flow Analysis for λ-calculus from its Skeletal Semantics.

ProbZelus étend le langage synchrone Zelus pour permettre de décrire des modèles probabilistes synchrones. Là où la programmation synchrone implémente des fonctions de suites, un langage probabiliste synchrone permet de décrire des modèles qui calculent des suites de distributions. On peut par exemple estimer la position d’un objet en mouvement à partir d’observations bruitées ou estimer l’incertitude d’un capteur à partir d’une suite d’observations. Ces problèmes mêlent des flots de variables aléatoires – les paramètres d’état qui changent au cours du temps – et des variables aléatoires constantes – les paramètres constants.

Pour estimer les paramètres d’état, les algorithmes d’inférence bayésienne de Monte Carlo séquentiels reposent sur des techniques de filtrage. Le filtrage est une méthode approchée qui consiste à perdre volontairement de l’information sur l’approximation actuelle pour recentrer les estimations futures autour de l’information la plus significative. Malheureusement, cette perte d’information est dommageable pour l’estimation des paramètres constants qui n’évoluent pas au cours du temps. Ce phénomène s’appelle l’appauvrissement.

Inspirés de la méthode d’inférence Assumed Parameter Filter (APF), nous proposons (1) une analyse statique, (2) une passe de compilation et (3) une nouvelle méthode d’inférence modulaire pour ProbZelus qui évite l’appauvrissement pour les paramètres constants tout en gardant les performances des algorithmes de Monte Carlo séquentiels pour les paramètres d’états.

Vélus est une formalisation d’un langage synchrone à flots de données et de sa compilation dans l’assistant de preuve Coq. Il inclut une définition de la sémantique dynamique du langage, un compilateur produisant du code impératif, et une preuve de bout en bout que le compilateur préserve la sémantique des programmes.

Dans cet article, on spécifie dans Vélus la sémantique de deux structures d’activation présentes dans les compilateurs modernes : switch et déclarations locales. Ces nouvelles constructions nécessitent une adaptation de l’analyse statique de dépendance de Vélus, qui produit un graphe acyclique comme témoin de la bonne formation d’un programme. On utilise ce témoin pour construire un schéma d’induction propre aux programmes bien formés. Ce schéma permet de démontrer le déterminisme du modèle sémantique dans Coq.