Nathanaël Courant
email: nathanael.courant@inria.fr

Xavier Leroy
email: xavier.leroy@college-de-france.fr.

Verified Code Generation for the Polyhedral Model

Keywords: CCS Concepts:, Software and its engineering → Compilers, Context specific languages, Software verification, • Theory of computation → Program verification Compiler verification, Polyhedral code generation, Polyhedral model

The polyhedral model is a high-level intermediate representation for loop nests that supports elegantly a great many loop optimizations. In a compiler, after polyhedral loop optimizations have been performed, it is necessary and difficult to regenerate sequential or parallel loop nests before continuing compilation. This paper reports on the formalization and proof of semantic preservation of such a code generator that produces sequential code from a polyhedral representation. The formalization and proofs are mechanized using the Coq proof assistant.

INTRODUCTION

Numerical code often consists in nested loops operating over multidimensional arrays. Such loop nests are the target of many compiler optimizations. For example, memory locality can be improved by permuting two nested loops, fusing two consecutive loops, or tiling the iteration space [START_REF] Muchnick ; Morgan Kaufmann | Loopy: Programmable and Formally Verified Loop Transformations[END_REF]]. Likewise, parallelism can be increased by vectorization or loop scheduling.

The polyhedral model, also known as the polytope model, is a high-level, declarative intermediate representation for loop nests [START_REF] Feautrier | The Polyhedron Model[END_REF]. In the polyhedral model, many loop optimizations can be expressed and performed in a uniform manner as transformations over the polytopes describing the iteration space. (Section 2 illustrates the approach on a simple example.)

Optimizers based on the polyhedral model have been integrated in compilers for conventional languages: for example, Graphite [START_REF] Trifunović | GRAPHITE Two Years After: First Lessons Learned From Real-World Polyhedral Compilation[END_REF]] adds polyhedral optimizations to GCC, and Polly [START_REF] Grosser | Polly -Performing Polyhedral Optimizations on a Low-level Intermediate Representation[END_REF] to LLVM.

Another use for the polyhedral model is to synthesize efficient software or hardware implementations of matrix and tensor computations. Domain-specific languages such as Halide [START_REF] Ragan-Kelley | Halide: Decoupling Algorithms from Schedules for High-performance Image Processing[END_REF]], Tensor Comprehensions [START_REF] Vasilache | The Next 700 Accelerated Layers: From Mathematical Expressions of Network Computation Graphs to Accelerated GPU Kernels[END_REF] or VOBLA [START_REF] Beaugnon | VOBLA: a vehicle for optimized basic linear algebra[END_REF]] make it easy to write high-level specifications of such computations, which can, then, be automatically translated to polyhedral models and compiled to efficient low-level code.

This paper reports on the formal specification of a polyhedral model and the formal verification of one part of a loop optimizer based on the polyhedral model. Compiler verification applies program proof and other verification techniques to the compiler in order to rule miscompilation out: the generated code is guaranteed to execute as prescribed by the semantics of the source program. Recent examples of formally-verified compilers include CompCert [START_REF] Leroy | Formal Verification of a Realistic Compiler[END_REF]] for the C language and CakeML [START_REF] Kumar | CakeML: A Verified Implementation of ML[END_REF]] for a functional language. A verified polyhedral optimizer could be integrated in CompCert, equipping this compiler with loop optimizations that it currently lacks. Such an optimizer could also be the basis for a verified code generator from a domain-specific language of tensor computations such as Halide. The formal verification would increase assurance in this kind of code synthesis.

Traditionally, a polyhedral optimizer comprises three parts, as depicted in Figure 1:

(1) detection of loop nests in Fortran or C source code, and construction of the corresponding polyhedral representations; (2) optimization via transformations over the poyhedral representation;

(3) generation of an equivalent, sequential or parallelized, loop nest that can be given to a conventional compiler.

Preliminary investigations by Pilkiewicz [2013] suggest that part (2), that is, polyhedral optimizations proper, lends itself well to translation validation [START_REF] Pnueli | Translation Validation[END_REF]]: the polyhedral models before and after each program transformation are checked for semantic equivalence by generating formulas in Presburger arithmetic, which are then verified with the help of Farkas certificates.

In this paper, we focus on part (3) of a polyhedral optimizer. We describe the formal verification, using the Coq proof assistant, of a code generator that produces efficient sequential code from a polyhedral representation. This code generator follows the polyhedra scanning approach described by [START_REF] Bastoul | Code Generation in the Polyhedral Model Is Easier Than You Think[END_REF] and used in GCC. The verification is more difficult than that of purely polyhedral transformations, as it combines algebraic reasoning over polyhedral operations, using certified linear algebra, with CompCert-style semantic reasoning over the executions of the generated code.

The contributions of this paper are as follows. After a short tutorial on the polyhedral model (section 2), we formalize the syntax and semantics of Poly, a simple polyhedral language (section 3). We then describe a code generator for this language, along with its correctness arguments. As shown in Figure 1, the code generator comprises four passes: schedule elimination, replacing the input schedule by the identity schedule (section 4); decomposition into abstract loops expressed in the intermediate language PolyLoop (section 5); elimination of redundant constraints produced by the previous pass (section 6); and generation of concrete loops expressed in a simple sequential imperative language, Loop (section 7). We formalized the code generator, its source, intermediate and target languages, and its correctness proofs using the Coq proof assistant and the VPL [START_REF] Boulmé | The Verified Polyhedron Library: an Overview[END_REF]] verified library of polyhedral operations (section 8). The Coq development is available at https://github.com/Ekdohibs/PolyGen. Finally, we describe related work in more details (section 9), then discuss the next steps in developing this code generator further (section 10).

for (int i = 0; i < n; i++ ) { for (int j = 0; j < n; j++ ) { C[i][j] = 0; for (int k = 0; k < n; k++ ) { C[i][j] += A[i][k] * B[k][j]; } } } (a) Matrix multiplication for (int m = 0; m < n; m++ ) { binom[m][0] = 1; binom[m][m] = 1; for (int k = 1; k < m; k++ ) { binom[m][k] = binom[m-1][k-1] + binom[m-1][k]; } } (b) Binomial coefficients computation

AN OVERVIEW OF THE POLYHEDRAL MODEL

Many numerical computing problems can be formulated as loop nests. Figure 2 shows two wellknown examples:matrix multiplication and binomial coefficients computation using Pascal's triangle. More precisely, these are imperfect loop nests: each loop can contain a sequence of statements or other loops. These imperfect loop nests are thus described by the grammar: Even with these restrictions, a great many numerical computing problems can be expressed in this way.

These programs are amenable to many optimizations such as loop splitting, loop fusion, changing the order of two loops, or even more complicated transformations that completely change the iteration order. All these transformations can be understood in a common framework, the polyhedral model, which we now present. This framework is sufficiently general to handle both simple, classical optimizations and more advanced ones, making it possible to factor out the formalization effort.

The polyhedral model works by considering each base instruction in an imperfect loop nest as an instruction that must be executed at every integer point from a given polyhedron. Moreover, the model specifies an order in which these instructions must be executed. For instance, in the binomial coefficients computation above, we have three base instructions, I 0 , I 1 and I 2 , given by:

I 0 (m) = binom[m][0] = 1; I 1 (m) = binom[m][m] = 1; I 2 (m, k) = binom[m][k] = binom[m-1][k-1] + binom[m-1][k];
These base instructions must be executed for every point of the polyhedron {m ∈ Z | 0 ≤ m < n} for I 0 and I 1 , and {(m, k) ∈ Z 2 | 1 ≤ k < m < n} for I 2 . However, these polyhedra alone are not enough to specify the behavior of this program: we also need to specify an execution order. In our case, it is given by executing the instructions in lexicographically increasing order of the (m, 0, 0) for I 0 , (m, 1, 0) for I 1 , and (m, 2, k) for I 2 . The constants 0, 1, 2 are used to represent the order of the instructions when using the ; operator. Such a specification of the execution order is called a schedule. The formal definition of this polyhedral language is presented in section 3.

Next, we wish to optimize the program in this polyhedral representation. This is done by changing the schedule, which corresponds to changing the iteration order. For instance, suppose we want to change our binomial program to perform initialization (instructions I 0 and I 1 ) before the rest of the code, and we also want to change the nested loops to iterate first over k and then over m. We can change our schedule to (0, m, 0) for I 0 , (0, m, 1) for I 1 , and (1, k, m) for I 2 . This transformation is allowed, because each time we get two instructions with a data dependency between one and the other, they are in the same order in the initial polyhedral program and the new polyhedral program. These data dependencies can be determined by the Bernstein conditions [START_REF] Bernstein | Analysis of Programs for Parallel Processing[END_REF]], and as this step is heuristic, it is very amenable to translation validation, with a verifier checking that the new polyhedral program respects the data dependencies. At any rate, as data dependencies play no part in our generator, we will safely ignore these for the rest of the paper.

Last, we need to generate code that corresponds to this new schedule. The first step is schedule elimination: we prefix the schedule to the points, modifying the polyhedra to express that change. This replaces the explicit schedule, based on an explicit ordering on the different points, by an implicit schedule based on a lexicographic ordering on the points. In our case, the new polyhedra would be:

• {(𝑥 1 , 𝑥 2 , 𝑥 3 , m) ∈ Z 4 | 𝑥 1 = 𝑥 3 = 0 ∧ 0 ≤ 𝑥 2 = m < n} for I 0 , • {(𝑥 1 , 𝑥 2 , 𝑥 3 , m) ∈ Z 4 | 𝑥 1 = 0 ∧ 𝑥 3 = 1 ∧ 0 ≤ 𝑥 2 = m < n} for I 1 , • {(𝑥 1 , 𝑥 2 , 𝑥 3 , m, k) ∈ Z 5 | 𝑥 1 = 1 ≤ 𝑥 2 = k < 𝑥 3 = m < n} for I 2 .
Once this is done, we generate code that scans the given polyhedra in lexicographic order. The case of only one polyhedron is simple: we generate one loop per dimension, computing the projection on the current dimensions, and setting the bounds of the loop according to the projection. For instance, to generate loops corresponding to the black points in Figure 3a (in lexicographic order of i then j), we first generate an external loop for (int i = 0; i < 5; i++), since the projection of the polyhedron on the first variable i gives {i | 0 ≤ i < 5}. Then, inside that loop, we generate the loop for (int j = 0; j <= i; j++), since the projection on the plane generated by both i and j is equal to the whole polyhedron, {(i, j) | 0 ≤ j ≤ i < 5}. Finally, that second loop contains the instruction I(i, j).

The case of several polyhedra is more involved, as illustrated in Figure 3b. The naïve way of generating code in that case is to generate scanning code as outlined above for the union of the polyhedra, and, in the body of the generated loops, add a test to ensure that we are inside the polyhedron corresponding to the instruction. For instance, associating black points with instruction I 1 and red triangles with instruction I 2 , the body of the loop nest executes I 1 (i, j); if (i == 4) I 2 (i, j); . However, we can produce more efficient code that does not contain tests that are useless for the most part of the loop. To this end, we project each polyhedron independently and then separate the projections into unions of polyhedra so that, in each of these polyhedra, the projection of each input polyhedron either contains that polyhedron or is disjoint from it. In our case, we split the projections in two different parts, {i | 0 ≤ i < 4} and {i | i = 4}. As previously, we repeat the generating operation under each loop node. In the end, we obtain the following code:

for (int i = 0; i < 4; i++) { for (int j = 0; j <= i; j++) { I 1 (i, j); } } for (int j = 0; j < 4; j++) { I 1 (4, j); I 2 (4, j); }

THE SOURCE LANGUAGE

The source language for our code generator is a polyhedral notation for loop nests. It is parameterized by a language of base instructions I, typically assignments such as

A[𝑥 1 ][𝑥 3 ] += B[𝑥 1 ][𝑥 2 ] * C[𝑥 2 ][𝑥 3 ].
As this example shows, base instructions are parameterized by a vector 𝑥 ∈ Z 𝑛 of integer indices. The semantics of base instructions is given in operational style, as a relation (I(𝑥), M 1 ) ⇓ I M 2 between the memory states before (M 1 ) and after (M 2 ) the execution of I with indices 𝑥. Since we do not need to perform dependence analysis, we keep instructions, their semantics, and memory states completely abstract.

A polyhedral program is a multiset of polyhedral instructions, each being a quadruplet (I, D, 𝜃, T ). Such a polyhedral instruction describes the iteration of a base instruction I over a sequence of parameters 𝑥. More precisely, the four components of a polyhedral instruction are:

• I is the base instruction to iterate.

• D is the iteration domain. It is a polyhedron: the set of integer tuples that satisfy a set of linear inequalities. It is thus described by a matrix 𝐴 and a vector 𝑎, with

D = {𝑥 ∈ Z 𝑛 | 𝐴𝑥 ≤ 𝑎}.
• 𝜃 is the scheduling function. It is an affine function1 from elements of D to tuples of integers that act as time stamps. It is described by a matrix 𝐾 and a vector 𝑘:

𝜃 : 𝑥 ↦ → 𝐾𝑥 + 𝑘.

• T is the transformation function that produces the arguments given to the base instruction I. Like 𝜃 , it is an affine function, described by a matrix 𝑇 and a vector 𝑡:

T : 𝑥 ↦ → 𝑇 𝑥 + 𝑡 .
Most polyhedral models in the literature have no transformation function (T is the identity).

We find these functions useful to express simplifications and transformations without rewriting the instructions I themselves. For example, assume that, during tiling, index 𝑖 becomes 5𝑖 1 + 𝑖 2 .

Traditionally, instructions such as 𝐴[𝑖] = 0 are rewritten into 𝐴[5𝑖 1 + 𝑖 2 ] = 0. We prefer to treat instructions as an opaque type, without any substitution operation, and use the transformation function to record the substitution explicitly:

𝑖 = 𝑇 𝑖 1 𝑖 2
+ 𝑡 where 𝑇 = 5 1 and 𝑡 = 0 .

The standard formulation of the polyhedral model, without transformation functions, can be recovered by considering each base instruction to be the composition of I and T .

A simplified semantics for a single polyhedral instruction (I, D, 𝜃, T ) is as follows. First, enumerate the elements of D in lexicographic nondecreasing order of the time stamps 𝜃 (𝑥):

D = {𝑥 1 , . . . , 𝑥 𝑛 } with 𝜃 (𝑥 𝑖 ) ≼ 𝜃 (𝑥 𝑗 ) if 𝑖 ≤ 𝑗
Then, repeatedly execute instruction I with parameters T (𝑥 𝑖 ), going from state M 0 to state M 𝑛 :

(I(T (𝑥 1 )), M 0 ) ⇓ I M 1 . . . (I(T (𝑥 𝑛 )), M 𝑛-1 ) ⇓ I M 𝑛
Note that the semantics is non-deterministic, even if the base instruction 𝐼 has deterministic semantics: if 𝜃 (𝑥) = 𝜃 (𝑥 ′ ), then I(T (𝑥)) and I(T (𝑥 ′ )) can be executed in any order.

The full semantics for a polyhedral program P is similar, with two extensions. First, it is useful to parameterize executions of polyhedral programs over some quantities, typically matrix dimensions, that remain constant during execution. These constant quantities, usually named program parameters, are given as an environment E: a vector of length 𝑘 that fixes the values of the first 𝑘 dimensions of the iteration space. Hence, the effective domain for the execution of (I, D, 𝜃, T ) is

D E = E 𝑦 𝑦 ∈ Z 𝑛-𝑘 , E 𝑦 ∈ D
Second extension: a polyhedral program comprises several polyhedral instructions. These instructions do not need to be executed one after the other; instead, their iterations can be interleaved if the schedules allow. To formalize this idea, we need to assume that in a polyhedral program P = (I 𝑘 , D 𝑘 , 𝜃 𝑘 , T 𝑘 ) 𝑘 ∈𝐾 all the domains D 𝑘 have the same dimension, and all the images of the scheduling functions Im(𝜃 𝑘 ) have the same dimension. This can easily be ensured by adding extra dimensions with value 0.

The semantics of the polyhedral program P in environment E is, then, defined as follows: iterate over (I, D, 𝜃, T ) ∈ P and over 𝑥 ∈ D E , in lexicographic nondecreasing order of 𝜃 (𝑥), and execute the instructions I(T (𝑥)) sequentially in this order.

An example of a polyhedral program, and its possible execution orders are given in Figure 4.

ELIMINATING THE SCHEDULING FUNCTION

The scheduling function in polyhedral programs make it easy to express optimizations that change the order of loops, such as loop interchange. However, polyhedral programs that have identity scheduling functions are in close correspondence with loop nests: those programs execute by enumerating tuples of variables in lexicographic order, hence the first variable naturally corresponds to outermost loops, the second variable to the second-outer loops, and so on. This correspondence 1,1) ⇝ (1,1) I 2 (1) ⇝ (1,1) (b) Instructions to be executed, and associated timestamps for the environment (𝑛 = 1)

(I 1 , {(𝑛, 𝑥, 𝑦) | 0 ≤ 𝑥 ≤ 𝑦 ≤ 𝑛}, (𝑛, 𝑥, 𝑦) ↦ → (𝑥, 𝑥), (𝑛, 𝑥, 𝑦) ↦ → (𝑥, 𝑦)), (I 2 , {(𝑛, 𝑥, 𝑦) | 0 ≤ 𝑦 ≤ 𝑥 ≤ 𝑛}, (𝑛, 𝑥, 𝑦) ↦ → (𝑥 + 𝑦 -1, 1), (𝑛, 𝑥, 𝑦) ↦ → (𝑥)) (a) Polyhedral program to be executed I 1 (0, 0) ⇝ (0, 0) I 2 (0) ⇝ (-1, 1) I 1 (0, 1) ⇝ (0, 0) I 2 (1) ⇝ (0, 1) I 1 (
I 2 (0); I 1 (0, 0); I 1 (0, 1); I 2 (1); I 1 (1, 1); I 2 (1)

I 2 (0); I 1 (0, 0); I 1 (0, 1); I 2 (1); I 2 (1); I 1 (1, 1)
I 2 (0); I 1 (0, 1); I 1 (0, 0); I 2 (1); I 1 (1, 1); I 2 (1) holds naturally when we transform a loop nest into a polyhedral program: we obtain a lexicographic scheduling on the variables we used for iteration. Symmetrically, the first natural step of code generation from a polyhedral program to a loop nest is to remove the explicit schedule and replace it with an implicit schedule, which is lexicographic on the iteration variables.

I 2 (0); I 1 (0, 1); I 1 (0, 0); I 2 (1); I 2 (1); I 1 (1, 1) (c
It must be noted that such a transformation cannot preserve all possible executions of a polyhedral program. Indeed, a general polyhedral program can have executions of the same instruction in several different points, all corresponding to the same timestamp, thus leaving the execution order of these instructions unspecified. (Some polyhedral generators use this to express that the loop can be run in parallel, but we only consider sequential programs.) On the other hand, this is not possible for a lexicographic schedule, since the lexicographic order is a total order, therefore two different executions of a given instruction are necessarily ordered. This transformation, therefore, does a partial determinization. Consequently, the correctness theorem for this transformation is that every valid execution of the transformed program is a valid execution of the initial program. On the other hand, some nondeterminism may remain after transformation: there is no constraint on the execution order of two distinct instructions executed at the same point.

The schedule elimination method presented in this section is the one introduced by [START_REF] Bastoul | Code Generation in the Polyhedral Model Is Easier Than You Think[END_REF]. It has numerous advantages for verification: it does not use complex operations over matrices, and it works for all inputs, not just unimodular schedules. Its only disadvantage is that it increases the number of variables that must be considered later during code generation, making code generation slower.

The transformation is simple: it adds new variables as a prefix of the list of variables, one for each dimension of the schedule, and sets the new variables to be equal to the value specified by the scheduling function at the given point in the polyhedral constraints. Since the semantics of polyhedral programs is specified by setting an environment as a prefix of the list of variables, we need to know the size of the environments for the transformation, and keep the environments as a prefix of the list of variables, inserting our new variables after the environments. It is an instance of the transformation usually called change of basis in the polyhedral literature.

Thus, assuming that the dimensions of the image of all scheduling functions 𝜃 are all the same, we perform the following transformation, which for each polyhedral instruction (I, D, 𝜃, T ) of P generates (I, D ′ , 𝜃 ′ , T ′ ), where:

D = E 𝑦 E 𝑦 ∈ Z 𝑛 , 𝐴 𝑒 𝐴 𝑣 E 𝑦 ≤ 𝑎 , 𝜃 : E 𝑦 ↦ → 𝐾 𝑒 𝐾 𝑣 E 𝑦 + 𝑘, T : E 𝑦 ↦ → 𝑇 𝑒 𝑇 𝑣 E 𝑦 + 𝑡
and:

D ′ =        E 𝑢 𝑦 E 𝑢 𝑦 ∈ Z 𝑛 ′ , 𝐴 𝑒 0 𝐴 𝑣 -𝐾 𝑒 𝐼𝑑 -𝐾 𝑣 E 𝑢 𝑦 ≤ = 𝑎 𝑘        , 𝜃 ′ : E 𝑢 𝑦 ↦ → E 𝑢 𝑦 , T ′ : E 𝑢 𝑦 ↦ → 𝑇 𝑒 0 𝑇 𝑣 E 𝑢 𝑦 + 𝑡
Indeed, the definition of D ′ gives:

E 𝑢 𝑦 ∈ D ′ ⇔ E 𝑦 ∈ D ∧ 𝑢 = 𝜃 E 𝑦 .
Then, the function Γ : D → D ′ defined by:

Γ : E 𝑦 ↦ → E 𝜃 E 𝑦 𝑦 is a bijection from D to D ′ , with inverse E 𝑢 𝑦 ↦ → E 𝑦 .
The new transformation function T ′ has moreover been chosen so that for all 𝑥 ∈ D, T (𝑥) = T ′ (Γ(𝑥)).

Besides, if

E 𝑢 1 𝑦 1 ∈ D ′
1 and

E 𝑢 2 𝑦 2 ∈ D ′
2 , then we have (where ≺ is lexicographic order): which can be rephrased as: if 𝑥 1 ∈ D 1 and 𝑥 2 ∈ D 2 correspond to the same environment E, we have:

E 𝑢 1 𝑦 1 ≺ E 𝑢 2 𝑦 2 ⇔ (𝑢 1 ≺ 𝑢 2 ) ∨ (𝑢 1 = 𝑢 2 ∧ 𝑦 1 ≺ 𝑦 2 ) ⇔ 𝜃 1 E 𝑦 1 ≺ 𝜃 2 E 𝑦 2 ∨ (𝑢 1 = 𝑢 2 ∧ 𝑦 1 ≺ 𝑦 2 ) ⇐ 𝜃 1 E 𝑦 1 ≺ 𝜃 2 E 𝑦 2 , Proc. ACM
E ⊢ (skip, M) ⇓ M Seq E ⊢ (𝑠 1 , M 1 ) ⇓ M 2 E ⊢ (𝑠 2 , M 2 ) ⇓ M 3 E ⊢ (𝑠 1 ; 𝑠 2 , M 1 ) ⇓ M 3 Instr (I(𝑒 1 (E), . . . , 𝑒 𝑘 (E)), M 1 ) ⇓ I M 2 E ⊢ (I(𝑒 1 , . . . , 𝑒 𝑘 ), M 1 ) ⇓ M 2 GuardTrue E ∈ P E ⊢ (𝑠, M 1 ) ⇓ M 2 E ⊢ (guard P 𝑠, M 1 ) ⇓ M 2 GuardFalse E ∉ P E ⊢ (guard P 𝑠, M) ⇓ M Loop ∀𝑥, (E :: 𝑥 ∈ P ⇔ 𝑎 ≤ 𝑥 < 𝑏) ∀𝑥 ∈ {𝑎..𝑏 -1}, (E :: 𝑥 ⊢ (𝑠, M 𝑥 ) ⇓ M 𝑥+1 ) E ⊢ (loop P 𝑠, M 𝑎 ) ⇓ M 𝑏
𝜃 1 (𝑥 1 ) ≺ 𝜃 2 (𝑥 2 ) ⇒ 𝜃 ′ 1 (Γ 1 (𝑥 1 )) ≺ 𝜃 ′ 2 (Γ 2 (𝑥 2 )), that is, by contraposition: 𝜃 ′ 2 (Γ 2 (𝑥 2 )) ≼ 𝜃 ′ 1 (Γ 1 (𝑥 1 )) ⇒ 𝜃 2 (𝑥 2 ) ≼ 𝜃 1 (𝑥 1
). As a consequence, for a fixed environment E, every valid ordering of instructions during the execution of P ′ is a valid ordering of instructions during the execution of P. The T = T ′ •Γ property guarantees that the same instructions are executed. Thus, every execution of P ′ corresponds to an execution of P, and this transformation preserves semantics. We also reach our goal: the 𝜃 ′ are now the identity function, and the schedule is thus a lexicographic enumeration of the points of the domains D ′ themselves.

DECOMPOSITION INTO LOOP NESTS

The second step of code generation is to compute the structure of the program in terms of imperfectly nested loops. The control flow becomes explicit, but the conditions and loop bounds remain affine and are represented by polyhedra. The target of this generation step is an intermediate language called PolyLoop. The syntax of PolyLoop is as follows: (1) If 𝑑 is the dimension of the D 𝑖 , return the program:

guard D 1 I 1 (T 1 ); . . . ; guard D 𝑛 I 𝑛 (T 𝑛 )

(2) For each polyhedron D 𝑖 , compute its projection P 𝑖 on the 𝑑 first dimensions, and compute the list of the P 𝑖 → (I 𝑖 , D 𝑖 , T 𝑖 ).

(3) Separate the projections P 𝑖 into a list of disjoint polyhedra and their associated instructions:

from P 1 → I 1 and P 2 → I 2 , we get (P 1 ∩P 2 ) → (I 1 ; I 2 ), (P 1 \P 2 ) → I 1 , and (P 2 \P 1 ) → I 2 , and then repeat with the other polyhedra that need to be separated. The differences P 1 \ P 2 and P 2 \ P 1 are not polyhedra, but unions of polyhedra: the list we produce is then potentially very long. (4) Compute the lexicographic ordering graph, which contains an edge P → P ′ if the loop over P must be placed before the loop over P ′ in the result to respect the lexicographic schedule, then sort the graph topologically. If the graph contains a cycle, the code generation fails. (5) For each P → ((I 1 , D 1 , T 1 ); . . . ; (I 𝑘 , D 𝑘 , T 𝑘 )), let 𝑠 be the result of a recursive call with current dimension 𝑑 + 1 and instruction list (I 1 , D 1 ∩ P, T 1 ), . . . , (I 𝑘 , D 𝑘 ∩ P, T 𝑘 ); build the instruction loop P 𝑠. (6) Return the program formed by the sequence of the results from the previous step. The iteration construct, loop P 𝑠 executes 𝑠 for increasing values of 𝑥 such that the current environment with 𝑥 added is in P. The semantics of PolyLoop are detailed in Figure 5. In rule Loop, the precondition ∀𝑥, (E :: 𝑥 ∈ P ⇔ 𝑎 ≤ 𝑥 < 𝑏) ensures that the iteration domain is finite: the rule does not apply if 𝑥 has no upper or no lower bound implied by P.

There are some similarities between PolyLoop and the schedule trees of [START_REF] Verdoolaege | Schedule Trees[END_REF] and [START_REF] Grosser | Polyhedral AST Generation Is More Than Scanning Polyhedra[END_REF], but their objectives are different: PolyLoop is a simple intermediate representation, while schedule trees are more complex, as they are used as an intermediate representation throughout code generation and subject to many transformations.

The algorithm used to transform a polyhedral program with lexicographic schedule into a PolyLoop program is shown in Figure 6. It is based on the algorithm by [START_REF] Quilleré | Generation of efficient nested loops from polyhedra[END_REF]. An important difference is that there is no context in which we generate the syntax tree, and that we do not simplify loop bounds in this context. Instead, this simplification is done in a separate phase (described in section 6) that removes redundant constraints from a PolyLoop program without changing its semantics.

The algorithm presented in Figure 6 generates a syntax tree corresponding to a given polyhedral program. It proceeds dimension by dimension, starting with the outermost dimension that must be generated: then, the recursive calls treat the iteration variable that has just been generated as an additional parameter.

The first step of the algorithm considers the case where there is no variable left for which there is code to generate. We then have to generate an instruction for each polyhedral instruction, with a guard node to ensure that the instruction will only be executed if it is inside an environment where it must be executed. These guards are redundant most of the time, and most of them will be removed by the simplification pass described in section 6. We note an arbitrary scheduling decision here: instructions are executed in the input order of the algorithm. The rest of the algorithm considers the case where we add another dimension. We first compute the projections over the current dimensions and the new dimension, and we make a case disjunction (steps 2 and 3) depending on which input polyhedra the current environment is in. Thus, each instruction will only be in the internal loops for which is it necessary for it to appear.

𝑥 0 𝑥 1 (a) P 1 𝑥 0 𝑥 1 (b) P 1 𝑥 0 𝑥 1 (c) -→ P 1 𝑥 0 𝑥 1 (d) P 1 𝑥 0 𝑥 1 (e)
Step 4 sorts the resulting list of polyhedra. Indeed, in the PolyLoop program, the loops that will be generated need to be ordered; however, this means that in every environment, one of these loops will always be executed before the other. [START_REF] Quilleré | Generation of efficient nested loops from polyhedra[END_REF] show that it is always possible to order two disjoint polyhedra to respect the desired execution order. The property "P 1 can be ordered before P 2 " is expressed as:

∀E, 𝑥 1 , 𝑥 2 , E :: 𝑥 1 ∈ P 1 ∧ E :: 𝑥 2 ∈ P 2 ⇒ 𝑥 1 < 𝑥 2 .
This is the same as saying that in every environment, all iterations of P 1 will be executed before all iterations of P 2 . This can be determined by the criterion depicted in Figure 7. Define P 1 = {E :: 𝑥 1 | ∃𝑥 2 , E :: 𝑥 2 ∈ P 1 }, that is, the projection of P 1 with respect to the variable 𝑥 1 , seen as a polyhedron having the same dimension as P 1 . Further define -→ P 1 as the polyhedron obtained by only keeping the constraints of P 1 for which the coefficient of 𝑥 1 is positive, and P 1 = P 1 ∩ -→ P 1 . We then have that P 2 must be ordered before P 1 if and only if:

∃E, 𝑥 1 , 𝑥 2 , E :: 𝑥 1 ∈ P 1 ∧ E :: 𝑥 2 ∈ P 2 ∧ 𝑥 2 ≤ 𝑥 1 ⇔ ∃E, 𝑥 2 , E :: 𝑥 2 ∈ P 2 ∧ E :: 𝑥 2 ∈ P 1 ⇔ P 1 ∩ P 2 ≠ ∅.
We then have, as desired:

E :: 𝑥 2 ∈ P 1 ⇔ ∃𝑥 1 , E :: 𝑥 1 ∈ P 1 ∧ 𝑥 2 ≤ 𝑥 1 .
However, in the case of three or more polyhedra, it can happen that there exist no compatible order because the lexicographic ordering graph contains a cycle. An example involving three polyhedra is given in appendix A. In this case, our algorithm fails, aborting code generation. A more sophisticated algorithm could, instead, divide some of the polyhedra in several fragments that can be ordered independently.

Steps 5 and 6 make a recursive call on each polyhedron for which there is a loop to generate, compute the corresponding PolyLoop subprograms, and combine them in sequence. The result is a PolyLoop program whose semantics respect the semantics of the initial polyhedral program.

The correctness of this code generation algorithm is proved by showing, by induction on the number of remaining dimensions, that in every environment, every execution of the generated program corresponds to an execution of the initial polyhedral program. The base case is simple. To handle the case where we generate the code for one more dimension, we have to show the following results on the polyhedra obtained as result of step 4:

• If P is before P ′ in the list of obtained polyhedra, then P can be ordered before P ′ in every environment; • All polyhedra obtained are disjoint;

• If 𝑥 ∈ P 𝑖 at the step 2, then 𝑥 is in one of the P of the obtained list, and the corresponding instruction I 𝑖 appears in the list of instructions of P.

These results are a consequence of the polyhedral computations performed at steps 3 and 4 of the algorithm.

As previously mentioned, the base case of our algorithm (step 1 in Figure 6) systematically guards the execution of instructions by a dynamic check that the current indices are within the corresponding domains D 𝑖 . Besides simplifying the correctness proof, these checks enable the recursive case (steps 2 to 5) to safely over-approximate their intermediate results, namely the projections P 𝑖 and their further decomposition into unions of polyhedra P. (Excessive over-approximation can trigger failures in step 4 or in the code generation algorithm from section 7, however.) Taking advantage of this degree of freedom, we use Fourier-Motzkin elimination [Schrijver 1998, section 12.2] to compute the projections P 𝑖 at step 2. Fourier-Motzkin elimination produces an exact result in the rationals (Q) but an over-approximation in the integers (Z). Hence, the polyhedra P 𝑖 may be bigger than the exact projections in Z, but this does not endanger the correctness of the generated PolyLoop code.

SIMPLIFICATION OF REDUNDANT CONSTRAINTS

To keep its correctness proof simple, the algorithm of section 5 generates a large number of redundant constraints. For instance, it inserts a guard node before each instruction, which is most of the time unnecessary as it is a direct consequence of the surrounding loop nodes. However, the algorithm is written so that is it easy to remove most constraints in a separate pass, without having to care whether it is possible to remove them while generating the PolyLoop code: whenever one of these constraints could not be removed, it will simply be kept, and the generated code will be slightly less efficient.

To simplify redundant constraints, we need a single primitive simplify, which takes as input a polyhedron P and a context C, and returns a polyhedron P ′ verifying P ′ ∩ C = P ∩ C, which can be reformulated as ∀𝑥 ∈ C, 𝑥 ∈ P ′ ⇔ 𝑥 ∈ P. The objective is that simplify returns a polyhedron described by as few constraints as possible, since these are the constraints that will appear in the generated code.

The algorithm for computing P ′ = simplify(P, C) is simple. Starting with P ′ = ∅, we consider each constraint 𝑎𝑥 ≤ 𝑐 in P one after the other. If the constraint is implied by P ∩ C, that is, if P ∩ C ∩ ¬(𝑎𝑥 ≤ 𝑐) = ∅, it is removed; otherwise, the constraint is added to P ′ .

𝑒 ::= | 𝑐 | 𝑥 | 𝑒 1 + 𝑒 2 | 𝑐 • 𝑒 | ⌊𝑒/𝑐⌋ | 𝑒 mod 𝑐 | min(𝑒 1 , 𝑒 2 ) | max(𝑒 1 , 𝑒 2 )
Tests:

𝑡 ::= | 𝑒 1 = 𝑒 2 | 𝑒 1 ≤ 𝑒 2 | 𝑡 1 && 𝑡 2 | !𝑡 | true | false
Statements:

𝑠 ::= | skip | 𝑠 1 ;𝑠 2 | I(𝑒 1 , . . . , 𝑒 𝑘 ) | if (𝑡) 𝑠 | for (𝑖 = 𝑒 1 ; 𝑖 < 𝑒 2 ; 𝑖++) 𝑠 Fig. 9. Syntax of Loop
As implemented and verified in the Coq development, the simplify operation is sound but suboptimal, owing to the fact that our emptiness test for polyhedra uses rationals (Q) instead of integers (Z): it guarantees that a set of constraints has no solutions with rational coordinates, while we are interested in solutions with integer coordinates. Consequently, some constraints that are redundant in Z are kept because they are not redundant in Q. For example, in a context 𝑥 ≤ 1, the polyhedron 𝑥 = 2𝑦 ∧ 𝑥 ≤ 0 is not simplified currently, but could be simplified to 𝑥 = 2𝑦 since 𝑥 ≤ 0 is redundant for integer points. This is suboptimal but sound.

We then define a function psimpl by the rules given in Figure 8. In effect, the constraints carried by guard and loop constructs are collected in the current context C, while being simplified using the simplify function. In these rules, we have omitted a slight detail: the dimension of the context needs to increase when we get under a loop node, to account for the newly declared variable. That detail aside, we can easily prove the theorem which interests us: if

E ∈ C, then E ⊢ (psimpl(C, 𝑠), M 1 ) ⇓ M 2 is derivable if and only if E ⊢ (𝑠, M 1 ) ⇓ M 2 is.

LOOP CODE GENERATION

The last step of code generation is to translate the PolyLoop intermediate language to a lower-level language, Loop, which replaces the abstract polyhedral constructions of PolyLoop by concrete Boolean tests and "for" loops. Figure 9 defines the syntax of Loop, and Figure 10 its semantics. The language is structured in integer expressions, tests (Boolean expressions), and statements. Expressions are semi-linear, as they include multiplications and divisions by constants in addition to affine constructs. They also feature min, max and mod operators in order to express loop bounds and guard conditions. Statements correspond to a standard structured imperative language, with if conditionals and counted for loops. A "let" binding can be defined as syntactic sugar for a loop with one iteration: A guard P 𝑠 construct is translated to a statement if (inside(P)) tr(𝑠), where tr(𝑠) is the translation of 𝑠 and inside(P) is a Boolean expression that tests membership in P. The expression is simply a Boolean conjunction of the linear inequalities that define P: if P 0 is the conjunction of constraints 𝑎 𝑖 𝑥 ≤ 𝑐 𝑖 for 𝑖 = 1, . . . , 𝑛, the test inside(P) is the Boolean expression

let 𝑥 = 𝑒 in 𝑠 def = for (𝑥 = 𝑒; 𝑥 < 1 + 𝑒; 𝑥++) 𝑠 Skip E ⊢ (skip, M) ⇓ M Seq E ⊢ (𝑠 1 , M 1 ) ⇓ M 2 E ⊢ (𝑠 2 , M 2 ) ⇓ M 3 E ⊢ (𝑠 1 ;𝑠 2 , M 1 ) ⇓ M 3 Instr (I(eval(E, 𝑒 1 ), . . . , eval(E, 𝑒 𝑘 )), M 1 ) ⇓ I M 2 E ⊢ (I(𝑒 1 , . . . , 𝑒 𝑘 ), M 1 ) ⇓ M 2 IfTrue eval(E, 𝑡) = true E ⊢ (𝑠, M 1 ) ⇓ M 2 E ⊢ (if (𝑡) 𝑠, M 1 ) ⇓ M 2 IfFalse eval(E, 𝑡) = false E ⊢ (if (𝑡) 𝑠, M) ⇓ M ForEmpty eval(E, 𝑒 1 ) ≥ eval(E, 𝑒 2 ) E ⊢ (for (𝑖 = 𝑒 1 ; 𝑖 < 𝑒 2 ; 𝑖++) 𝑠, M) ⇓ M For eval(E, 𝑒 1 ) < eval(E, 𝑒 2 ) ∀𝑥 ∈ {eval(E, 𝑒 1 )..eval(E, 𝑒 2 ) -1}, (E, 𝑖 : 𝑥 ⊢ (𝑠, M 𝑥 ) ⇓ M 𝑥+1 ) E ⊢ (for (𝑖 = 𝑒 1 ; 𝑖 < 𝑒 2 ; 𝑖++) 𝑠, M eval( E,𝑒 1 ) ) ⇓ M eval( E,𝑒 2 )
𝑎 1 𝑥 ≤ 𝑐 1 && • • • && 𝑎 𝑛 𝑥 ≤ 𝑐 𝑛 .
Loops are harder to translate. Consider an instruction loop P 𝑠. After having translated 𝑠 into tr(𝑠), we pick a fresh name 𝑖 for the iteration variable, which corresponds to the last dimension of P, the only dimension that is not already determined by the context. We then perform the following steps, broadly similar to Fourier-Motzkin elimination:

• Decompose the constraints of P (which are of the form 𝑎 • 𝑥 ≤ 𝑐) in three groups: the first group, P 0 , where the coefficient of 𝑖 is zero; the second group, P + , where this coefficient is positive; and the third group, P -, where it is negative. • If P + or P -contains no constraints, code generation fails, as it corresponds to an unbounded loop.

• Each constraint 𝑢𝑖 + 𝑘 𝑎 𝑘 𝑥 𝑘 ≤ 𝑐 of P + provides an upper bound for 𝑖: we have 𝑖 ≤ (𝑐 -𝑘 𝑎 𝑘 𝑥 𝑘 )/𝑢, thus 𝑖 ≤ ⌊(𝑐 -𝑘 𝑎 𝑘 𝑥 𝑘 )/𝑢⌋ since 𝑖 is an integer. We want a strict upper bound, which is given by 𝑖 < ⌊(𝑐 + 𝑢 -𝑘 𝑎 𝑘 𝑥 𝑘 )/𝑢⌋. There are several constraints, so the upper bound is in fact the minimum of all those expressions. This is possible, since P + contains at least one constraint. We call the resulting expression for the upper bound 𝑒 + .

• Likewise, each constraint 𝑢𝑖 + 𝑘 𝑎 𝑘 𝑥 𝑘 ≤ 𝑐 in P -is equivalent to ( 𝑘 𝑎 𝑘 𝑥 𝑘 -𝑐)/(-𝑢) ≤ 𝑖,
thus to ⌊( 𝑘 𝑎 𝑘 𝑥 𝑘 -𝑐 + (-𝑢) -1)/(-𝑢)⌋ ≤ 𝑖, providing a lower bound for 𝑖. The actual lower bound 𝑒 -will then be the maximum of all these expressions, which is well-defined since P - is nonempty. • Generate the code if (inside(P 0 )) for (𝑖 = 𝑒 -; 𝑖 < 𝑒 + ; 𝑖++) tr(𝑠).

It is relatively easy, using familiar properties of integer division, to prove that for all E:

E :: 𝑥 ∈ P ⇔ E ∈ P 0 ∧ eval(E, 𝑒 -) ≤ 𝑥 < eval(E, 𝑒 + ).
Thus, by case analysis on whether E ∈ P 0 or not, we can prove that the semantics of the generated Loop program is the same as the semantics of the initial PolyLoop program, assuming that the semantics of 𝑠 and tr(𝑠) are the same.

To simplify the generated code, we also distinguish the case where P contains an equality on 𝑖, say 𝑘𝑖 = 𝑒. In this case, there is only one possible value of 𝑖. We can then express all other constraints on 𝑖, using this equality, as a polyhedron P ′ which does not depend on 𝑖. Then, if the coefficient 𝑘 is 1, the value of 𝑖 is simply 𝑒, and we produce the code if (inside(P ′ )) let 𝑖 = 𝑒 in tr(𝑠). If the coefficient 𝑘 is not 1, we need to guard the computation by a divisibility check:

if (inside(P ′ ) && 𝑒 mod 𝑘 = 0) let 𝑖 = ⌊𝑒/𝑘⌋ in tr(𝑠)

COQ DEVELOPMENT

The totality of the algorithms presented above have been formalized and proved in Coq. For this purpose, we had to develop a small library of linear algebra, define the operations we needed on polyhedra, and prove their correctness theorems. We also had to formalize the semantics of the various languages presented above to be able to express the correctness theorems of the code generation.

Linear Algebra

When working with vectors and matrices in a dependently-typed framework such as Coq or Agda, it is tempting to use dependent types such as vec 𝑛 𝐴, the type of vectors of 𝐴 of dimension 𝑛, and mat 𝑝 𝑞 𝐴, the type of 𝑝 × 𝑞 matrices of 𝐴. This is close to mathematical usage but requires many retyping functions to be used, e.g. to convert between vec (𝑛 + 1) 𝐴 and vec (1 + 𝑛) 𝐴.

In our development, we chose to represent vectors as lists of integers, with the convention that each list is followed by infinitely many zeros. With this convention, a list [𝑥 1 ; . . . ; 𝑥 𝑘 ] can be interpreted as a 𝑛-dimensional vector for any 𝑛: the vector is either (𝑥 1 , . . . , 𝑥 𝑛 ) if 𝑛 ≤ 𝑘, or (𝑥 1 , . . . , 𝑥 𝑘 , 0, . . . , 0) if 𝑛 > 𝑘. Likewise, a matrix is just a list of vectors, with the convention that lines not represented in the list are the all-zero vector. This simply-typed representation is a good match for reasoning about the polyhedral model: sometimes the model forces us to consider that several matrices or vectors have the same dimensions by padding them with zeros if needed; this is a no-operation in our representation.

Operations over vectors and matrices are refreshingly easy to define and comprise vector addition, scalar multiplication, dot product, lexicographic ordering, and matrix application. However, vectors and matrices do not have unique representations (trailing zeros can be materialized or left implicit), hence we need to reason up to setoid equality.

A constraint (a linear inequality) is defined as a pair of a vector and a scalar, the pair ( a, c) representing the constraint a • 𝑥 ≤ c. A polyhedron is simply a list of constraints.

Operations on Polyhedra

We also need a number of operations on polyhedra: emptiness check, intersection, canonicalization, projection on the first 𝑑 dimensions, etc. To this end, we reused the Verified Polyhedron Library (VPL) [START_REF] Boulmé | The Verified Polyhedron Library: an Overview[END_REF]], a mixed Coq-OCaml library that uses a posteriori certification: operations over polyhedra are implemented efficiently in OCaml and produce Farkas-style certificates [Schrijver 1998, corollary 10.1a]; the results and their certificates are then checked by Coq functions that have been proved (once and for all) to be sound (if the checker succeeds, the result is correct) [START_REF] Fouilhé | A Certifying Frontend for (Sub)polyhedral Abstract Domains[END_REF]. Since certificate checking may fail, most operations over polyhedra live in a monad that supports errors and also the possibility that the OCaml implementation is not pure (e.g. maintains internal state).

A limitation of the VPL is that most of its operations are specified by one-way implications instead of equivalences. For example, consider the two VPL operations we use most: the emptiness test isempty and the assume function that adds a linear constraint 𝑎𝑥 ≤ 𝑐 to a polyhedron. They are specified by the following implications: isempty(P) = true =⇒ P = ∅ 𝑥 ∈ P ∧ 𝑎𝑥 ≤ 𝑐 =⇒ 𝑥 ∈ assume(P, 𝑎𝑥 ≤ 𝑐) However, isempty is allowed to return false even for an empty polyhedron, and assume(P, 𝑎𝑥 ≤ 𝑐) is allowed to return a polyhedron larger than the intersection of P with the semi-space 𝑎𝑥 ≤ 𝑐. This is fine for the original application for which the VPL was developed, namely as a relational domain for static analysis by abstract interpretation: the implications that are proved are sufficient to show the soundness of the static analysis; over-approximation in the result of the analysis is allowed.

For the emptiness check, we can use the VPL isempty predicate directly, since the implication proved by the VPL is the one we need. Other operations we need must be synthesized from what the VPL provides. For example, converting a polyhedron from our representation (a list of linear constraints 𝑎 𝑖 𝑥 ≤ 𝑐 𝑖 for 𝑖 = 1, . . . , 𝑘) to the internal VPL representation is not trivial. We compute P = assume(. . . assume(∅, 𝑎 1 𝑥 ≤ 𝑐 1 ) . . . , 𝑎 𝑘 𝑥 ≤ 𝑐 𝑘 ), then check that isempty(assume(P, ¬(𝑎 𝑖 𝑥 ≤ 𝑐 𝑖 ))) = true for every 𝑖 = 1, . . . , 𝑘. The VPL specifications guarantee that the exact result Q = 𝑖 (𝑎 𝑖 𝑥 ≤ 𝑐 𝑖 ) is included in P. The extra checks guarantee that P ⊆ (𝑎 𝑖 𝑥 ≤ 𝑐) for 𝑖 = 1, . . . , 𝑘, from which it follows that P ⊆ Q, hence P is the exact result Q. Of course, any of the extra check can fail, causing the conversion to fail. The conversion is, therefore, presented as a monadic operation in our code.

Projection of the first 𝑑 dimensions of a polyhedron is implemented by iterating the Fourier-Motzkin elimination algorithm 𝑑 times. We proved that Fourier-Motzkin elimination is exact on Q, which implies that it is sound on Z but can result in over-approximation, as discussed in section 5. In the following, isExactProjection n pol proj expresses the fact that proj is the Q-projection of pol over the dimension n. For s a positive integer and pol a polyhedron, scale_poly s pol is the polyhedron pol, scaled s times, so that we can express membership of rational points without using Proc. ACM Program. Lang., Vol. 5, No. POPL, Article 40. Publication date: January 2021.

Correctness Theorems

There is a semantics preservation theorem for each of the code generation steps presented previously. We only show the final theorem that results from the composition of these individual proofs: The hypothesis WHEN st ← complete_generate_many es n pis THEN means that the code generator succeeds and produces the Loop program st. Several other hypotheses are mostly technical, ensuring that the initial program is well-formed. In particular, n being the total dimension of the input program, the two hypotheses pis_have_dimension pis n and forall pi, In pi pis → ... ensure that the input program does not refer to non-existing variables. Code generation is done in an environment of fixed size, that is, where it is already decided what will be a variable and what will be a parameter. The variable es is the size of that environment; we thus have the two conditions length env = es, which ensures that the environment that is used has the correct size, and ( es ≤ n)%nat, which ensures that the size of this environment is not greater than the dimension of the input program. Under these hypotheses, we conclude that every execution of the generated Loop program st corresponds to one of the possible executions of the initial Poly program pis.

Extraction and Execution

We used Coq's extraction facility to generate OCaml code from our Coq development and the Coq part of the VPL. This extracted code can be linked with the rest of the VPL and a Loop printer to produce an executable prototype of our code generator.

By lack of a concrete syntax and a parser for our input language Poly, we could only hand-code a number of polyhedral programs taken from [START_REF] Bastoul | Code Generation in the Polyhedral Model Is Easier Than You Think[END_REF] and visually inspect the generated code. We now show three such examples.

The first example, shown in Figure 12, has only one polyhedron and describes the scanning of a 𝑛 × 𝑚 rectangle. Our generator produces two nested loops corresponding to the two dimensions of the schedule, plus two let bindings that map the schedule to points in the input polyhedron.

The second example, shown in Figure 13, has only one polyhedron and describes the scanning of a sequence of 𝑛 instructions, but with a schedule that is not unimodular. The resulting code contains a test with a modulo operation before executing the instruction.

The third example, shown in Figure 14 and taken from [START_REF] Bastoul | Code Generation in the Polyhedral Model Is Easier Than You Think[END_REF], illustrates the case of multiple polyhedra. To avoid an unreasonable increase in the size of the produced code (which would otherwise include numerous "let" bindings), the initial program is a polyhedral program with lexicographic scheduling. The generated code is quite good, with innermost loops that contain no conditionals and involve no min/max computations.

(I, {(𝑛, 𝑚, 𝑖, 𝑗) ∈ Z 4 | 0 ≤ 𝑖 ≤ 𝑛 ∧ 0 ≤ 𝑗 ≤ 𝑚}, (𝑛, 𝑚, 𝑖, 𝑗) ↦ → ( 𝑗, 𝑖), (𝑛, 𝑚, 𝑖, 𝑗) ↦ → (𝑖, 𝑗)) (a) Initial polyhedron if (0 ≤ 𝑛) for (𝑡 1 = 0; 𝑡 1 < 1 + 𝑚; 𝑡 1 ++) for (𝑡 2 = 0; 𝑡 2 < 1 + 𝑛; 𝑡 2 ++) let 𝑖 = 𝑡 2 in let 𝑗 = 𝑡 1 in I(𝑖, 𝑗) (b) Generated program
I, {(𝑛, 𝑖) ∈ Z 2 | 0 ≤ 𝑖 ≤ 𝑛}, (𝑛, 𝑖) ↦ → (2𝑖), (𝑛, 𝑖) ↦ → (𝑖)) (a) Initial polyhedron for (𝑡 1 = 0; 𝑡 1 < 1 + 2 * 𝑛; 𝑡 1 ++) if (𝑡 1 mod 2 = 0) let 𝑖 = ⌊𝑡 1 /2⌋ in I(𝑖) (b) Generated program

Verification of Optimizations

There are two main ways to verify a compilation pass: compiler proof, where the pass is proved once and for all to preserve semantics for all inputs; and translation validation [START_REF] Pnueli | Translation Validation[END_REF]], where at every run of the pass the input and output codes are compared for semantic equivalence. We are not aware of any significant loop optimization that has been verified with the compiler proof approach. However, translation validation has been applied many times to loop optimizations.

For optimizations that mostly preserve the execution order of basic instructions, validation can use symbolic representations of the codes plus specialized, efficient equivalence checking algorithms. Examples include loop unrolling as handled by [START_REF] Necula | Translation validation for an optimizing compiler[END_REF], software pipelining by [START_REF] Tristan | A simple, verified validator for software pipelining[END_REF], loop-invariant code motion by [START_REF] Tristan | Evaluating value-graph translation validation for LLVM[END_REF], and loop peeling and induction variable strength reduction by [START_REF] Tate | Equality Saturation: A New Approach to Optimization[END_REF]. In contrast, loop transformations that completely change the evaluation order, such as permutation, fusion or tiling, require more advanced and more costly validation techniques. [START_REF] Zuck | Translation and Run-Time Validation of Loop Transformations[END_REF] add permutation rules, specific to this purpose, to the logic of their TVOC validator. [START_REF] Kundu | Proving Optimizations Correct using Parameterized Program Equivalence[END_REF] integrate similar permutation rules in their parameterized equivalence checking approach. [START_REF] Barthe | Product programs and relational program logics[END_REF] use a relational program logic that they reduce to Hoare logic via product programs. [START_REF] Churchill | Semantic program alignment for equivalence checking[END_REF] automate the product program approach using SMT solving and loop matching heuristics.

For a loop optimizer that uses the polyhedral model, it is tempting to base validation on the polyhedral model as well: build the polyhedral representation of the optimized code and compare it with the polyhedral representation of the initial code. This is the approach followed by [START_REF] Verdoolaege | Equivalence checking of static affine programs using widening to handle recurrences[END_REF] and by [START_REF] Muchnick ; Morgan Kaufmann | Loopy: Programmable and Formally Verified Loop Transformations[END_REF]. However, this is not always possible: the code generated by a polyhedral optimizer can contain non-affine conditional control (such as if 𝑥 mod 2 = 0) that cannot be expressed by a polyhedral representation. [START_REF] Schordan | Verification of Polyhedral Optimizations with Constant Loop Bounds in Finite State Space Computations[END_REF] (I 1 , {(𝑛, 𝑚, 𝑖, 𝑗)

∈ Z 4 | 1 ≤ 𝑖 ≤ 𝑛 ∧ 𝑗 = 𝑖}, (𝑛, 𝑚, 𝑖, 𝑗) ↦ → (𝑖, 𝑗)), (I 2 , {(𝑛, 𝑚, 𝑖, 𝑗) ∈ Z 4 | 0 ≤ 𝑖 ≤ 𝑗 ≤ 𝑛}, (𝑛, 𝑚, 𝑖, 𝑗) ↦ → (𝑖, 𝑗)), (I 3 , {(𝑛, 𝑚, 𝑖, 𝑗) ∈ Z 4 | 0 ≤ 𝑖 ≤ 𝑚 ∧ 𝑗 = 𝑛}, (𝑛, 𝑚, 𝑖, 𝑗) ↦ → (𝑖, 𝑗)) (a) Initial program i j (a) (b) (c) (d) (e) (X) (Y)
(b) Polyhedra (with 𝑛 < 𝑚). I 1 is blue squares, I 2 is black dots, and I 3 is red triangles.

for (𝑖 = 1; 𝑖 < min(1

+ 𝑛, 1 + 𝑚); 𝑖++) (X) if (𝑛 ≤ 𝑖) let 𝑗 = 𝑖 in (d) I 1 (𝑖, 𝑗) I 2 (𝑖, 𝑗) I 3 (𝑖, 𝑗) if (𝑖 ≤ 𝑛 -1) let 𝑗 = 𝑖 in (a)
I 1 (𝑖, 𝑗) The approach that we follow in this paper combines compiler proof and translation validation in a way that plays to their respective strengths. As explored by Pilkiewicz [2013], loop transformations are performed and validated over a polyhedral representation, using only Presburger arithmetic formulas, without a need for SMT solving or specialized decision procedures. As reported in this paper, the final code generation step is proved semantics-preserving once and for all, avoiding difficulties with translation validation caused by non-affine control in the generated code.

I 2 (𝑖, 𝑗) for (𝑗 = 𝑖 + 1; 𝑗 < 𝑛; 𝑗++) (b) I 2 (𝑖, 𝑗) if (𝑖 ≤ 𝑛 -1) let 𝑗 = 𝑛 in (c) I 2 (𝑖, 𝑗) I 3 (𝑖, 𝑗) for (𝑖 = max(1, 𝑛 + 1); 𝑖 < 1 + 𝑚; 𝑖++) (Y) let 𝑗 = 𝑛 in (e)

Code Generation in the Polyhedral Model

Early work on automatic parallelization of loop nests introduced polyhedral techniques only for analyzing dependencies between loops: the loop nests were still represented by Abstract Syntax Trees and optimized by rewriting these ASTs [START_REF] Feautrier | Dataflow analysis of array and scalar references[END_REF][START_REF] Lamport | The Parallel Execution of DO Loops[END_REF]. [START_REF] Pugh | Uniform techniques for loop optimization[END_REF] and [START_REF] Lu | A Unified Framework for Systemic Loop Transformation[END_REF] introduced the idea of representing loop nests by their polyhedral models and transforming directly the models. This idea gave rise to a new need: synthesizing imperative code from a polyhedral representation, an operation often called "polyhedra scanning" because it involves enumerating all the integer points in a set of polyhedra. [START_REF] Ancourt | Scanning Polyhedra with DO Loops[END_REF] introduced the use of Fourier-Motzkin elimination to project the enumeration space on successive iteration dimensions. This technique works well for a single polyhedron but produces inefficient control for more complex spaces. [START_REF] Quilleré | Generation of efficient nested loops from polyhedra[END_REF] showed how to avoid this inefficiency by decomposing the enumeration space as a disjoint union of polyhedra. [START_REF] Bastoul | Code Generation in the Polyhedral Model Is Easier Than You Think[END_REF] further developed these ideas, leading to the well-known CLooG code generator.

Our Coq formalization and correctness proof described in this paper follows the CLooG approach and covers most of the techniques described in [START_REF] Bastoul | Code Generation in the Polyhedral Model Is Easier Than You Think[END_REF], with the notable exception of nonunit loop strides. More recent improvements also remain to be formalized, such as those described by [START_REF] Grosser | Polyhedral AST Generation Is More Than Scanning Polyhedra[END_REF] and by [START_REF] Razanajato | Splitting Polyhedra to Generate More Efficient Code[END_REF]. We have not investigated the significantly different approaches to polyhedra scanning proposed by [START_REF] Boulet | Scanning polyhedra without DO-loops[END_REF] and more recently by [START_REF] Chen | Polyhedra Scanning Revisited[END_REF].

Verified Neural Networks

A new application of polyhedral-based compilation appeared recently in the context of machine learning: generating efficient low-level code implementing deep neural networks and recurrent neural networks expressed in high-level matrix and tensor notations. For instance, polyhedral optimization plays an important role in Tensor Comprehensions [START_REF] Vasilache | The Next 700 Accelerated Layers: From Mathematical Expressions of Network Computation Graphs to Accelerated GPU Kernels[END_REF]] and in Tiramisu [START_REF] Baghdadi | Tiramisu: A Polyhedral Compiler for Expressing Fast and Portable Code[END_REF]. In parallel, the formal verification of neural networks is making progress, with new methodologies and tools such as Reluplex [START_REF] Katz | Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks[END_REF] and DeepPoly [START_REF] Singh | An abstract domain for certifying neural networks[END_REF]. This is a strong incentive to formally verify the optimizers and code generators that produce the actual implementations of these neural networks, as a way to ensure that the properties formally verified at the level of the neural network carry over to the actual implementation.

CONCLUSIONS AND FUTURE WORK

The work described in this paper is the first formal verification of a relatively sophisticated polyhedral code generator, broadly similar to those used in production compilers. The verification combines linear algebra with semantic reasoning in interesting ways. It exposed one oversight in the literature: the loop generation algorithm of [START_REF] Quilleré | Generation of efficient nested loops from polyhedra[END_REF] can fail in the case where the projection of a polyhedron produces three or more disjoint polyhedra, because it is not always possible to order these polyhedra in a way that enforces the desired execution order. It is good to know about this limitation, even though we do not know whether the problematic case can show up in practice with production optimizers such as Graphite and Polly.

Several ideas from [START_REF] Bastoul | Code Generation in the Polyhedral Model Is Easier Than You Think[END_REF] remain to be implemented and verified. This includes the generation of stride loops, where, at each iteration, the loop index is incremented by a stride 𝑠 > 1. Additional simplifications are also possible at the PolyLoop level.

The next step in code generation is to produce actual C code (or CompCert Clight code) instead of stopping at the Loop language. The main challenge is to deal with arithmetic overflow in index computations. Loop uses exact, arbitrary-precision arithmetic to compute array indices, polyhedron membership, and loop bounds, while performance demands that we use fixed-precision machine

Fig. 1 .

 1 Fig. 1. General shape of a polyhedral optimizer (top) and contribution of this paper (bottom)

Fig. 2 .

 2 Fig. 2. Familiar numerical computations as loop nests

  𝑠 ::= for (...) { 𝑠 } | 𝑠;𝑠 | I where I stands for base instructions such as assignments. Moreover, we impose the additional restriction that all loop bounds and array indices are affine in the existing variables: they are of the form 𝑎 1 *x1 + • • • + 𝑎 𝑛 *xn + c, where x1,...,xn are the existing variables.

Fig. 3 .

 3 Fig. 3. Example polyhedra for code generation

  Fig. 4. Example of a semantics for a polyhedral program

Fig. 5 .

 5 Fig. 5. Big-step semantics for PolyLoop

  Expressions:𝑒 ::= (𝑥 1 , . . . , 𝑥 𝑘 ) ↦ → 𝑘 𝑖=1 𝑎 𝑖 𝑥 𝑖 + 𝑐 𝑑 where 𝑎 𝑖 , 𝑐, 𝑑 ∈ Z, 𝑑 > 0 Polyhedra: P ::= {(𝑥 1 , . . . , 𝑥 𝑘 ) ∈ Z 𝑘 | 𝐴(𝑥 1 . . . 𝑥 𝑘 ) ⊤ ≤ 𝑎} where 𝐴 ∈ M 𝑝,𝑘 (Z), 𝑎 ∈ Z 𝑝 Statements: 𝑠 ::= skip | 𝑠 1 ; 𝑠 2 | I(𝑒 1 , . . . , 𝑒 𝑘 ) | guard P 𝑠 | loop P 𝑠 Expressions 𝑒 compute linear functions of their arguments, up to the floor function. Polyhedra P are defined as in Poly by a matrix 𝐴, a vector 𝑎, and the constraint 𝐴𝑥 ≤ 𝑎. Statements comprise base instructions, sequences, conditionals and loops. The conditional construct guard P 𝑠 executes 𝑠 if the current environment, mapping variables to their current values, is in the polyhedron P.Input: a list of lexicographically scheduled polyhedral instructions (I 1 , D 1 , T 1 ), . . . , (I 𝑛 , D 𝑛 , T 𝑛 ), and the current dimension 𝑑. Output: a PolyLoop program.

Fig. 6 .

 6 Fig. 6. Transformation of a polyhedral program into a PolyLoop program

Fig. 7 .

 7 Fig. 7. Ordering two disjoint polyhedra with respect to execution order

  Fig. 8. Simplification of a PolyLoop program

Fig. 10 .Fig. 11 .

 1011 Fig. 10. Semantics for Loop

Fig. 12 .

 12 Fig. 12. Code generation for a single polyhedron

(

Fig. 13 .

 13 Fig. 13. Code generation for a single polyhedron with modulo

I 3 (

 3 Fig. 14. Code generation for several polyhedra, with an implicit lexicographic schedule in the initial program

  P 1 and P 2

	𝑥 1	𝑥 1	𝑥 1
	𝑥 0	𝑥 0	𝑥 0
	(f) P 1 cannot be ordered	(g) P 1 and P 2	(h) P 1 can be ordered be-
	before P 2		fore P 2

Proc. ACM Program. Lang., Vol. 5, No. POPL, Article 40. Publication date: January 2021.

Some polyhedral code generators, such as[START_REF] Ancourt | Scanning Polyhedra with DO Loops[END_REF], require that the scheduling function be unimodular so that points in the polyhedron are always integer affine functions of the schedule. Our generator accepts arbitrary affine scheduling functions. Non-unimodular scheduling functions such as 𝑖 ↦ →

2𝑖 will produce correct but possibly inefficient code involving tests such as if (j mod 2 = 0). Proc. ACM Program. Lang., Vol. 5, No. POPL, Article 40. Publication date: January 2021.

rational numbers. The functions in_poly check membership, mult_vector multiply a vector by an integer, and assign n k v returns the vector v where the n-th component was replaced by k.

Definition isExactProjection n (pol proj : polyhedron) := forall (p : list Z) ( s : Z), 0 < s → in_poly p ( scale_poly s proj) = true ↔ exists (t k : Z), 0 < t ∧ in_poly (assign n k ( mult_vector t p)) ( scale_poly (s * t) pol) = true.

Theorem pure_project_in_iff : forall n ( pol : polyhedron), isExactProjection n pol (pure_project n pol).

The remaining polyhedral operations are those used in steps 3 and 4 of the syntax tree generation algorithm. In order to simplify the translation function from a polyhedral program into a PolyLoop program, these two steps have been combined inside the split_and_sort function. This function takes as input a list of polyhedra, and splits and sorts the result into a list where each element is a pair of a polyhedron, and the indices of the input polyhedra that contain this polyhedron. The properties below are those that were expressed in section 5 to prove the correctness of the code generation algorithm. The WHEN x ← e THEN notation means "if the monadic computation e succeeds and returns value x, then . . . ". arithmetic. Machine arithmetic can overflow, causing undefined behaviors or incorrect results.

Cuervo [START_REF] Cuervo Parrino | Dealing with arithmetic overflows in the polyhedral model[END_REF] propose an elegant solution to this problem: static analysis of the polyhedral program produces a Boolean condition that, when true, guarantees the absence of overflows in the whole program. They suggest to evaluate the condition at run-time, branching to the optimized, generated loop nest if true, and to the original, unoptimized loop nest if false. Finally, to test the performance of the generated code and fine-tune the code generation algorithms, it would be nice to connect our code generator with an existing front-end that produces polyhedral models.

APPENDIX A CYCLES IN THE LEXICOGRAPHIC ORDERING GRAPH

Consider the following three disjoint polyhedra:

Suppose those three polyhedra are the result of step 2 of the algorithm. Since they are disjoint, they also are the result of step 3. In step 4, the lexicographic ordering graph contains a cycle. Indeed, we have (0, 0, 0) ∈ P 1 and (0, 0, 1) ∈ P 2 , thus the loop for P 1 must precede the loop for P 2 . Likewise, P 2 ∋ (1, 0, 0) ≺ (1, 0, 1) ∈ P 3 , hence the loop for P 2 must precede the loop for P 3 , which itself must precede the loop for P 1 because P 3 ∋ (0, 1, 0) ≺ (0, 1, 1) ∈ P 1 . Therefore, the three loops cannot be ordered. This problem is reminescent of the failure case of the painter's algorithm in computer graphics, and the solutions used there (splitting the polygons) could also be used in our case. However, while this shows the three loops cannot be ordered, the previous steps in the generation algorithm often prevent the problem from happening. In our case, the problem would only manifest itself if we have these three polyhedra and only 𝑥 and 𝑦 were parameters, while 𝑧 was not. We have not yet seen cases where the problem happens after the first step of the generation, and we suspect it cannot happen; however, we did not formally prove it, and did not find justification for it in the literature.


[REPE, issue 2-2020] Editorial:

The Review of Evolutionary Political Economy inaugural issue, part 2

The present REPE issue 2-2020 is the second part of our inaugural "double pack". We were lucky to receive more papers for the inaugural issue than we could accommodate in one issue. So please enjoy another set of challenging original research papers gauging the field of evolutionary political economy.

In Financialisation and the periodisation of capitalism: appearances and processes, Jan Toporowski argues that the analysis of financial processes is essential for understanding changes in the financial system. Only these processes give rise to appearances such as the statistical data that are the basis of most studies of financialization. Those processes are fundamentally determined by the structure of the financial system. Following Minsky, Toporowski focuses on corporate finance which, through its effect on business investment, influences the dynamics of the capitalist system. As financial structures change, this gives rise to particular phases of capitalist development. The paper thus builds on Minsky's historical institutional analysis, but offers a more systematic analysis. It offers a periodization of capitalism through mercantile capitalism, classic, bank-based capitalism, finance capital, state finance capitalism, to pension fund capitalism and capital market inflation. It shows how each period ends with financial difficulties that are overcome with financial innovation leading to a new financial structure with corresponding changes in financial processes. Specifically, the paper argues that the phase of capital market inflation, inaugurated by funded pension schemes in the last decades of the twentieth century, has come to an end in the illiquidity of capital markets that lies behind the 2008 financial crisis. The paper suggests that the measures of "unconventional monetary policy", or "Quantitative Easing", mark a new period of state finance capital with a return to the state support of a structurally illiquid capital market that already had prevailed in Europe and North America from the 1930s to the 1960s.

The discipline of International Political Economy-IPE has been flirting with evolutionary approaches for the past decade or so. So far, attempts to develop a take on evolutionary theory have proceeded in a rather unstructured way: They range from potential applications of Darwinian theory of selection to more recent efforts to draw on ecological approaches and complexity theory when analysing crises and transformations. There has also been a renewed interest in institutionalist approaches and heterodox tradition, but this too, has been a fragmented process. Ronen Palan's article An Evolutionary Approach to International Political Economy: The Case of Corporate Tax Avoidance aims to offer a pathway to a more systemic framework of evolutionary political economy, in order to rethink the changes in the regulation on the contemporary system of states. Palan develops his approach by distinguishing between a tradition of political economy based on action of discreet entities (this reflects the roots of IPE in neoclassical economics) and a tradition of thought centred around a concept of transaction (taking root in original institutional economics). This framework opens up a new perspective on the traditional state-market dichotomy in IPE. One implication of such an approach has less to do with the conventional notion of captured governments or lack of political will, and more with the complex institutional terrain of the modern system of sovereignty. As Palan demonstrates, the core problem is that only a regulatory system can address the phenomenon of tax abuse and arbitrage; yet in the process, it is also likely to undermine the very institutional foundation of the market economy. So far, regulators have opted, unsurprisingly, for muddling along. The effect, however, has been that despite the increasing scope of the regulations, the fundamentals of ongoing tax and corporate abuse do not seem to change.

In Productivity and inequality in the UK: a political economy perspective, Philip Arestis argues that the development of labour productivity and income inequality are closely and significantly related. Productivity growth is the key determinant of how demand can grow without inflation, thereby reducing inequality of income, wealth and opportunity. In particular, a slowdown in productivity growth and an increase in inequality have occurred in the past decades and now affect many advanced economies, what has become more pronounced following the global financial crisis. Although weak productivity growth and increase in inequality predated this global financial crisis and the subsequent Great Recession, they have both been exacerbated. Focussing on the UK experience, Arestis analyses this from a Political Economy perspective, which emphasises the structure and power in an economic system.

Theo Papaioannou's article Reflections on the Entrepreneurial State, Innovation and Social

Justice is also an invitation to reconsider social justice, inequality and redistribution, in this paper under technological innovation. The discussion starts with the famous debate about The Entrepreneurial State by Mariana Mazzucato, which emphasizes the limits of the liberal and neo-liberal arguments. It is argued that the significance of long-term actions of the state is to take risks, to reduce uncertainty of agents and to design innovation differently. The idea of public risk-taking should not be divided from a political approach to the state. Justice and distribution of the benefits of innovation are critical and should be contextualized. While a more equal distribution of the benefits of technological innovation would reduce some inequality, it would not eliminate some forms of inequality such as discriminations based on colour, gender and castes present in many countries and often even reproduced with and within innovations (such as AI). Thus, if justice in innovation cannot be achieved through the implementation of redistributive policies, it must be rethought and re-implemented through new forms of governance, i.e. acting both on the distribution of benefits of innovation and on new forms of participation. Participation in the decision making and new forms of legitimacy go beyond conventional redistributive policy but must include fairness as a key ingredient of designing innovative policies.

Frank Beckenbach, in the second part of his A value-theoretic approach to economic dynamics and evolution-synthesizing different Marxian modules in a simulation model, presents the simulation experiments on his novel evolutionary reconstruction of Marxian value theory and long-lingering transformation problem, theoretically and formally laid out in his part I in REPE issue 1. His novel reconstruction includes manuscripts of Marx that have become fully available only relatively recently through the progress of the international MEGA project, which are suggesting a value-theoretic reconstruction of the main parts of Marx's critique of Political Economy. After a simulation run for a standard configuration (the "moderation regime"), the simulations integrate characteristics of the capitalist development as emphasized by Marx, such as the social conflict regime and the crisis regime. Solutions to long-lingering theoretical problems can be solved only in such complex modelling and related simulations. A more consistent Marxist approach should be achieved this way.

Lynne Chester provides her analytical report The 2019-20 Australian bushfires: A potent mix of climate change, problematisation, Indigenous disregard, a fractured federation, volunteerism, social media and more. Intensity and duration of the 2019-20 Australian bushfires have been unique, with unprecedented global impacts. We invited this paper for both these practical impacts and their theoretical implications. The area burnt was huge, it took seven months to contain or extinguish the fires, the smoke plume was the equivalent size of the eleven largest states of the United States, and carbon dioxide emissions have been enormous. More than a billion animals perished. The paper argues that the story of these is more complex than one of climate change, but includes a conjunction of cumulative events, (in)actions and institutions, a mix of the problematisation of bushfires and governing, a federation of nation and local states fractured by constitutional responsibilities, the impact of neoliberal austerity policies on land management, discordant localstate policies, a long-term disregard of Indigenous fire practices, the role of community (volunteerism), the transmission of (mis)information by social and traditional media, record temperatures, national rainfall the lowest for over a century, and a severe three-year drought. The entire plurality of critical economic perspectives is concerned and discussed in the article.

Finally, we provide you with a book review of Marc Lavoie on Yoshinori Shiozawa et al.'s Microfoundations of Evolutionary Economics, which thematically lies at the heart of REPE's scope, but is to be critically reviewed, nevertheless.

In the future, we will prefer review articles over reviews of individual books. For this and all other relevant information on REPE, including our current calls for papers and special issues, please visit our website: https://www.springer.com/journal/43253. With best wishes, and hope for an ever more intense collaboration with our readers in the future, the editorial team: Silvano Cincotti, silvano.cincotti@unige.it Wolfram Elsner, welsner@uni-bremen.de Nathalie Lazaric, nathalie.lazaric@gredeg.cnrs.fr