Seminar and reading group

This talk explores connexions between (mostly affine) static control
loop nests and integer-valued polynomials in integer variables. We
first describe a simple and fast algorithm that counts the number of
instructions executed by a (parameterized) affine loop nest of a
slightly restricted class, and use this algorithm to define the
correspondence between the iteration vector and sequential rank of any
instruction instance. We then proceed to define a loop (or kernel)
interpolation technique that coerces one or more loop nests into a
single perfect loop, and use this technique to recognize loops in raw
program traces, or transform and/or merge compute kernels. This
introduces integer polynomial loops, where bounds, memory access
functions, and other parts of instructions are polynomials rather than
affine; the last part of the talk shows how such loops can be compiled
to produce efficient code. The three parts of the talk rely on a
somewhat unusual representation for integer polynomials, whose
properties provide simple and efficient integration, interpolation,
and differentiation techniques which lie at the heart of the various
algorithms.

Le pavage de boucles est une technique clé d’optimisation dans les compilateurs, utilisée à la fois pour améliorer la localité des accès mémoire et pour contrôler la granularité de la parallélisation. Dans le cadre du modèle polyédrique, le pavage est traditionnellement défini par des pavés de taille fixe, déterminés à la compilation. Ce type de pavage peut conduire à un déséquilibre de charge entre les threads, en fonction de la forme et de la taille des pavés ainsi que de celles du domaine d’itération.
Cette présentation introduit le pavage algébrique, une nouvelle approche de pavage qui définit les pavés non plus par leur taille, mais par leur volume, c’est-à-dire par le nombre d’itérations qu’ils contiennent. Les bornes des pavés sont calculées dynamiquement à l’exécution à l’aide d’expressions algébriques, appelées expressions trahrhe. Cette technique vise à résoudre spécifiquement les problèmes d’équilibre de charge tout en conservant les bénéfices en localité de données du pavage classique.
L’approche a ensuite été déclinée et étendue aux programmes de type stencils notamment grâce à l’utilisation de pavés trapézoïdaux. Les performances ont été évaluées sur plusieurs benchmarks et comparées aux compilateurs polyédriques de l’état de l’art. Enfin, ces techniques ont été intégrées et automatisées dans un compilateur source-à-source, Pesto, capable de générer automatiquement du code C parallèle annoté avec des directives OpenMP.

Fault attacks are hardware-induced disruptions of systems, typically used against embedded systems while running to alter programs’ execution and achieve some type of exploit. Analyzing fault attacks can be tricky because the disrupted execution doesn’t follow language semantics; for instance, skipping a return statement may allow an attacker to fall through a function to another, unrelated function without properly setting up the call. These problems are compounded in the context of multi-fault attacks, where an attacker may perform targeted and repeated attacks to work around countermeasures and achieve complex objectives.

One such analysis is SAMVA by Gicquel et al. [1], a tool for finding attacks in binaries using multi-fault instruction-skip and instruction-replay attacks. SAMVA takes an attack plan such as “go from the entry of verifyPIN to authenticated=true without touching the countermeasure” and finds sequences of faults that execute the plan using a combination of static analysis, heuristics and emulation. In this talk, I’ll present SAMVA’s main ideas and revamp its core algorithms to turn it from a heuristics-driven attack planner into a complete analysis. The updated SAMVA is able to find all working attacks and lazily enumerate them by increasing cost for the attacker. As a side-effect, finding the cheapest successful attacks makes SAMVA an automated quantification of programs’ robustness level against the faults considered.

[1] https://hal.science/hal-03980128

Now integrated in mainstream languages, Algebraic Data Types (ADTs) have established themselves as a nice way to reason about data structures and their manipulation using pattern matching. However, their use in low-level programming remains limited despite efforts, notably from the Rust community.
This talks will be an introduction to the language dubbed Ribbit. This work aims at combining a high level language, with easy-to-use ADTs, and low level memory specifications, for efficient and compact computations. Ribbit is a pure, compiled language, where high level types can be specified into memory types, ie fine-grained, modular indications on how to store a chosen type into the memory.
We will give an overview of Ribbit, and delve into the complexity that arises when designing a sound semantic for a mix between high level and low level languages, by showcasing how adding restrained mutability turns easy, simple reads into complex operations, riddled with side-effects.

Skeletal Semantics is a meta-language to describe the semantics of
programming languages. We present it through several examples,
highlighting how complex features can be captured in a readable way
using monads. These features range from simple effects like exceptions
to more complex ones including the manipulation of continuations.

In the first part of this talk I will briefly present the theorem prover Lean and its mathematical library Mathlib. I will focus on one example, building on it to show some of the automatic tools available when proving theorems in Lean. In the second part, I will discuss a more advanced example concerning Laurent Series, and discuss a recent project with C. Cohen aiming at adapting the Mathlib proof to Rocq and to Mathcomp-Analysis.

Among all the modern backtracking-style regex semantics, the ECMAScript RegExp chapter finds itself in a surprisingly favorable position: almost all features can be matched in linear-time, and it is the only language for which a linear algorithm for all lookarounds is known.
We argue that the impact of new RegExp proposals on linear implementations should be considered.
The ECMAScript RegExp semantics can also be expressed in a way that is particularly suitable for formal verification.
We present our ongoing verification work and its benefits for the ECMAScript community.

Compiler correctness is crucial for reasoning about program correctness: if we use a faulty compiler to compile a verified program, we may end up with an incorrect binary. Thankfully, compilers are computer programs too and can be proven correct with a proof assistant to obtain verified compilers. But who compiles (and runs) the verified compiler? The typical approach in Rocq would be to use the built-in extraction, but this mechanism is essentially an unverified compiler from Gallina to another high-level language. Thankfully, writing a verified compiler gives us a verified compiler, so it should be possible to use it to compile itself—bootstrap it. In this talk, first, I will present the approach we are using to bootstrap a simple verified compiler for an imperative language in Rocq. Then, I will introduce in more detail the more interesting technical parts of our work, specifically the reification procedure.

Modern regular expressions (regexes) are a powerful tool for finding patterns in text. Modern features such as capturing groups, lookarounds, and backreferences turn the problem of matching into a complex task. Real-world implementations additionally employ a large variety of optimizations and heuristics to speed up matching in practice. In this work we don’t shy away from this complexity but instead tame it by providing a formalization of realistic regex matching that includes all of the cumbersome aspects. In the Rocq proof assistant, we provide the first formalization and proof of correctness of a prefix acceleration optimization in the PikeVM. We additionally formalize optimizations such as anchored regexes and impossible matches. We combine all of them to produce a realistic matching algorithm which is proven to return matches defined by the ECMAScript 2023 standard.

Domain-Specific Languages (DSLs) facilitate the concise and efficient expression of specialized computational kernels in domains such as graphics pipelines, stencil computations, and artificial intelligence. DSL compilers can leverage domain knowledge to apply highly targeted code optimizations, often resulting in near-optimal performance. However, such optimizations are inherently inapplicable to preexisting code written in general-purpose languages, necessitating a costly and error-prone porting process, or even a full program rewrite.

A promising alternative consists in assisting the programmer by automatically identifying program fragments that can be expressed using DSL primitives. In general, the problem of program detection is more complex than establishing computational equivalence between programs — a task known to be undecidable. Various strategies have been proposed to circumvent this limitation, such as focusing on restricted subsets of programs with statically predictable control structures (e.g., loops), or relaxing the notion of equivalence through syntactic approximations.

In this thesis, we explore a novel approach that further relaxes the equivalence constraint by tolerating occasional misclassifications, provided that such errors remain infrequent and controllable. This paradigm is particularly well-suited to machine learning techniques, which inherently operate under probabilistic assumptions and approximate correctness. Correctly identified fragments can then be validated and filtered through a subsequent verification phase.

This thesis focuses on scalable translation validation for high-performance computing and machine learning. The aim is to enhance automatic parallelization by verifying reductions and compile-time data allocation. The research addresses scalability issues and proposes solutions for automated corrections. The work is validated using HPC benchmarks and is conducted in collaboration between Inria Lyon and Iowa State University.

Vectorisation is a technique used to speed up programs by processing several data in parallel at the instruction level.
However, autovectorisers struggle with programs with lots of branching, such as automata and finite-state transducers for which high-performance is wanted in some applications such as DNA or JSON parsing.
Implementing such optimisations requires lots of effort from the programmer, relying on subtle tricks and a fine knowledge of processor instructions.
In this talk, we will see how algebraic automata theory provides tools to find vectorisations on some nice class of transducers.
This is a first step towards designing a high-level language that compiles transducers to SIMD optimised code.

L’une des techniques classiques d’organisation des connaissances en mathématiques consiste à regrouper les objets qu’on souhaite étudier pour former ce qu’on appelle une structure. Par exemple, les structures algébriques regroupent un ensemble et des opérations sur cet ensemble. On distingue deux familles de représentations des structures, celles dites empaquetées et celles dites dépaquetées.

Dans cette présentation, je présenterai la contribution principale de ma thèse, qui consiste à combiner une représentation empaquetée avec une technique d’inférence traditionnellement associée aux représentations dépaquetées.

Cette approche permet notamment d’améliorer la modélisation usuelle de la notion d’ensemble en termes de prédicats dans un assistant de preuve basé sur une théorie des types. Ceci permet à l’utilisateur de mieux tirer parti des intuitions venant de la théorie des ensembles, ce qui simplifie considérablement l’accès aux assistants de preuve pour un.e débutant.e, par exemple un.e étudiant.e en première année de licence de mathématiques.

Pour passer à l’échelle et éviter des déclarations absconses aux utilisateurs, cette nouvelle représentation vient avec un compilateur d’instances de classes de types.

Modern regular expressions have fundamentally changed the matching problem. While traditionally regular expression matching is concerned with membership, modern regex libraries are able to locate a matching string within a given input and report the values matched by the capture groups of the regex. This change to the matching problem introduces a new question: when there are multiple locations where a match can occur, which one should be returned? In this talk, I will present the different ways in which modern regex libraries answer this question, and how we’ve been able to define these different semantics using backtracking trees.

This habilitation thesis aims at reducing the gap between formal and informal mathematics by providing extensions of the Rocq prover, taking the viewpoint that dependent type theory is an assembly language and providing “compilers” that take simplified user input and perform complex operations to relieve the user from unnecessary boilerplate and help them focus on the mathematical meaning of their formalization.

I will present my work as an intern of Thierry Coquand at Chalmers University, last year. We formalized and implemented an axiom system for (oo, 1)-categories proposed by David Wärn which should have allowed the formalization of the (oo, 1)-category of (oo, 1)-categories in a proof-assistant. Firstly, I will present what categories are, the idea of higher-order mathematics and what motivates the study and use of (oo, 1)-categories. Next, we will go over the different axioms and notions of the system as well as their synthetic formalization in Rocq. Finally, we’ll conclude on what was achieved and the remaining future work.