François Kasséné Gomis
email: gomisfk@gmail.com

Thierry Bouwmans
email: thierry.bouwmans@univ-lr.fr

Mamadou Samba Camara

Idy Diop

Estimation of the Hidden Message Length in Steganography: A Deep Learning Approach

Keywords: Steganography, Steganalysis, Machine Learning, Deep Learning, Convolutional Neural Networks, MultiLayer Perceptron

Steganography is a science which helps to hide secret data inside multimedia supports like image, audio and video files to ensure secure communication between two parts of a channel. Steganalysis is the discipline which detects the presence of data hidden by a steganographic algorithm. There are two types of steganalysis: targeted steganalysis and universal steganalysis. In targeted steganalysis, the steganographic algorithm used to hide data is known. In the case of universal steganalysis, the detection of hidden data doesn't depend on any specific algorithm used in the process of steganography. In this paper, we focus on universal steganalysis of images in a database with an eventual cover-source mismatch problem. It is shown that combining both unsupervised and supervised machine learning algorithms helps to improve the performance of classifiers in the case of universal steganalysis by reducing the cover-source mismatch problem. In the unsupervised step, the k-means algorithm is generally used to group similar images. When the number of features extracted from the image is very large it becomes difficult to compute the k-means algorithm properly. We propose, in that case, to use Deep Learning with Convolutional Neural Network (CNN) to group similar images at first and implement a Multilayer Perceptron (MLP) neural network to estimate the hidden message length in all the different groups of images. The first step of this approach prevents the cover-source mismatch problem. Reducing this issue boost the performance of classifiers in the second step which consists of estimating the hidden message length.

Introduction

Research in universal steganalysis domain become very interesting since researchers discover that deep learning with Convolutional Neural Networks (CNNs) helps to obtain better results in the classification between cover and stego images. Till now CNNs have been never used for regression to estimate the hidden message length. Various types of materials used to capture images and various steganographic algorithms available for hiding data cause a problem called cover-source mismatch in universal steganalysis. In previous studies, it is demonstrated that clustering can be used, as a prior step in the process of steganalysis, to improve the performance of the classifiers in a database with cover-source mismatch [START_REF] Gomis | Multiple linear regression for universal steganalysis of images[END_REF], before implementing a classification or regression algorithm for universal steganalysis. Generally, authors used clustering with the k-means algorithm to group images into clusters. However, if the number of features extracted is big, it becomes computationally difficult to compute them with the k-means algorithm. In this context, we propose to employ a deep learning-based approach for estimation of the hidden message length in steganography. We called the proposed method DeepStego. To estimate the hidden message length, we use in the first step a CNN for grouping similar images into different categories. Then, in the second step, we implement an MLP neural network to estimate the hidden message length.

The rest of the paper is organized as follows: In Section 2, we give the theory in universal steganalysis. In Section 3, we present our original method of universal steganalysis. Then, we illustrate our scheme in Section 4. In Section 5, experiments are conducted on a database and we discuss the results. Concluding remarks and future directions are provided in Section 6.

Related Works

Research in the universal steganalysis domain focuses either on the extraction of relevant features which are sensitive to any steganographic algorithm or in the machine learning algorithms used to build models for classification or regression. The goal in both cases is to help to boost the performance of classifiers. About relevant features for universal steganalysis of JPEG images, authors use Firstorder statistics, Inter-block, and Intra-block features. Table 1 is a summary of different categories of features and some authors who proposed them for universal steganalysis of images. [START_REF] Chen | JPEG image steganalysis utilizing both intrablock and interblock correlations[END_REF] Variation Blockiness Chen and Shi (2008) [START_REF] Chen | JPEG image steganalysis utilizing both intrablock and interblock correlations[END_REF] Intra-block features Average Markov matrix

All these features are sensitive to steganographic algorithms embedding impact while at the same time insensitive to the image content. According to the steganographic algorithm used to embed messages, a category of features can be more useful than others. Thus, some authors proposed methods that combine different categories of features [START_REF] Chen | JPEG image steganalysis utilizing both intrablock and interblock correlations[END_REF]. Many different blind steganalysis methods have been proposed in the literature [START_REF] Dwivedi | Universal steganalysis techniques based on the feature extraction in transform domain[END_REF]. After choosing a set of features, we need to find a strong algorithm for binary classification or regression (to separate stego and cover images or to estimate the hidden message length). Support Vector Machine [START_REF] Cortez | Data Mining with Multilayer Perceptrons and Support Vector Machines[END_REF] and classical Neural Networks are very used for classification between stego and cover images. Recently, some authors start to use Convolutional Neural Network for the same task [START_REF] Chen | JPEG-Phase-Aware Convolutional Neural Network for Steganalysis of JPEG Images[END_REF]. To estimate the relative payload, Multiple Linear Regression is also used but the cover-source mismatch problem and the huge number of features extracted make its implementation difficult. It is shown that applying clustering is a good solution before using it [START_REF] Gomis | Multiple linear regression for universal steganalysis of images[END_REF]. About clustering when the number of features extracted is huge and when the database is big (more than 10,000 images), the computation becomes difficult. Some papers related to deep learning for universal steganalysis have been published. Chaumont and al. made a recapitulation of those methods in their paper [START_REF] Chaumont | Deep learning in steganography and steganalysis since 2015[END_REF]. Deep learning with CNN has better performance than usual machine learning algorithms. However, to estimate the hidden message length in the case of universal steganalysis, there are still some difficult challenges to overcome to boost the performance of blind steganalyzers. Some methods which deal with estimation of hidden message length have been proposed in the literature [START_REF] Quach | Extracting hidden messages in steganographic images[END_REF]. CNN is a classification algorithm that has never been used in the perspective of estimating the hidden message length.

DeepStego: A Deep Learning Methodology

In this section, we detail the proposed approach named DeepStego for universal steganalysis in a database with a cover-source mismatch problem. Figure 1 shows an overview of the data pipeline. The different steps are described and illustrated in the following. The proposed approach consists of combining deep learning with CNNs [START_REF] O'shea | An introduction to convolutional neural networks[END_REF] and MLP neural network [START_REF] Cortez | Data Mining with Multilayer Perceptrons and Support Vector Machines[END_REF] to build strong and robust models that estimate the hidden message length in universal steganalysis. This method consists of three main steps:

-Step 1: Implementation of CNN in a JPEG database containing cover and stego images. The objective here is to group similar images into different groups (or clusters). Grouping images is a strategy to prevent an eventual cover-source mismatch problem in the database. That problem can occur when there is a variety of materials used to get images and a lot of different steganographic algorithms used to hide data into images. -Step 2: Implementation of MLP in all the groups to build models for estimating the hidden message length. -Step 3: Utilization of the models for prediction.

Experimental Illustrations

Cover and stego images

We use a steganography Python module called Stegano [START_REF] Bonhomme | Stegano: a pure python steganography module[END_REF] to generate stego images with different payloads. As shown in Figure 2, after the embedding process, changes between stego and cover images are not visually detectable. Histograms of the cover image and its stego image are generated by the Stegano module algorithm.

The hidden message estimation technique

Image database description To illustrate our purpose, we use the MNIST Database [START_REF] Deng | The mnist database of handwritten digit images for machine learning research [best of the web[END_REF]. This database is very practical in our case. It contains 70, 000 28 × 28 grayscale JPEG images divided into 10 categories.

Stego images generation

To generate stego images for simulation, we use the module Stegano of Python to embed messages with different lengths inside images. So, we obtain 35, 000 stego images. After that process, we create a vector of labels which contains the lengths of the hidden messages of all the images of the database. That vector will be used for the regression part.

Outcome vector L for CNN

Outcome vector Y for MLP

        L 1 L 2 . . L n-1 L n                 Y 1 Y 2 . . Y n-1 Y n        
The vector L will be used for classification with CNN and the vector Y for regression with MLP.

Convolutional Neural Networks in the database

To group images of the MNIST database into different categories, we implement a Convolutional Neural Network classifier with four hidden layers. This is a practical and very convenient database to highlight the proposed method. We perform CNN on the data before using Multilayer Perceptron for regression in the different groups. This architecture of CNN gives a good classification of the images into 10 groups. This architecture can be changed. It depends on the database we use to perform universal steganalysis of images. The goal in this step is to reduce an eventual cover-source mismatch issue.

Features for regression with multilayer percetron (MLP) in the different categories of images

To implement an MLP neural network, we use both intra-block and inter-block correlations [START_REF] Chen | JPEG image steganalysis utilizing both intrablock and interblock correlations[END_REF]. It consists of 486 features extracted from a JPEG image. At this step, we need the labels (vector Y ) containing the lengths of the embedded messages of all images in the database.

Steganalysis on a category of images

To perform universal steganalysis on clusters, we use regression with an MLP neural network architecture with the most relevant features from both intra-block and inter-block correlations.

Experimental Results

Estimating the hidden message length is not an easy task. In the case of universal steganalysis combining CNN and MLP neural networks is a good approach to perform that task. In our experiments on the MNIST database, we got interesting results. This database is very convenient to illustrate our method of doing universal steganalysis in a database with a cover-source mismatch problem.

Deep learning with CNN for classification

By applying CNN with a standard architecture, we obtain easily 10 groups of images. Here an illustration of the model performance. In Figure 4, we can observe the evolution of the accuracy score in the training and validation data. We can note that they are very close.

MLP neural network for regression

In this step, we implement in all the clusters an MLP neural network for estimating the lengths of the hidden messages. Here the architecture of our neural network which consists of an input layer of 12 nodes (12 features selected from the 486 extracted features), three hidden layers of 13 nodes and an output layer of 1 node (estimation of the hidden message length) Furthermore, the use of a stepwise feature selection helps to boost the MLP accuracy in the regression step. A normal universal steganalysis procedure consists of extracting relevant features and implementing a supervised algorithm for classification or regression. For that, we implement an MLP neural network (with the same architecture implemented in the second part of DeepStego) to estimate the hidden message length on the full database MNIST. In Figure 6, we show a comparison between the results of a normal universal steganalysis procedure and DeepStego. The average score on the MNIST database for the universal steganalysis procedure is inferior to each score obtained by DeepStego in all the 10 groups. Thus, Deep-Stego gives better results (in all the 10 groups) than a universal steganalysis procedure on the full database. However, the highest accuracies of the universal steganalysis approaches proposed in the literature, are often in the range [0.95, 0.97]. It rarely reaches 0.9. With DeepStego, we get accuracy which turns around 0.9 in all groups showing the interest of the proposed deep learning approach for the estimation of the hidden message length in steganography.

Conclusion

In this paper, we addressed the cover-source mismatch problem that prevents the utilization of regression for universal image steganalysis. For this, we need to group similar images into clusters before applying it. When the extracted feature vector from the image is very large, the k-means algorithm cannot help to perform the clustering process. To address this issue, we have proposed an original method that used in its first step CNNs to group similar images and in its second step implementation of a multilayer perceptron neural network to estimate the hidden message length. Experimental results on the MNIST database provided good approximation models in all the 10 clusters. Thus, deep learning with CNN is a suitable alternative to k-means to reduce the cover-source mismatch problem in the case of universal steganalysis.

Fig. 1 .

 1 Fig. 1. DeepStego (Proposed method): Data Pipeline.

Fig. 2 .

 2 Fig. 2. Histograms comparison between the cover image (left) and the stego image (right).

Fig. 3 .

 3 Fig. 3. CNN architecture on MNIST dataset.

Fig. 4 .

 4 Fig. 4. Accuracy and loss in training and validation datasets.

Fig. 5 .

 5 Fig. 5. MLP architecture employed in DeepStego

Fig. 6 .

 6 Fig. 6. Performance comparison between DeepStego (G1 to G10) and a normal universal steganalysis procedure (average score on the MNIST database).

Table 1 .

 1 Features for Universal Steganalysis: An Overview.

	Authors	Categories	Feature Names
			Global histogram
	Ashu and Chhikara (2014) [1]	First-order statistics	AC histograms
			Dual histograms
			Co-occurrence matrix
	Chen and Shi (2008)	Inter-block features

Table 2

 2 shows the MLP models accuracy scores in the groups generated by CNN.

Table 2 .

 2 Accuracy score value in the 10 groups for DeepStego.

	Groups	accuracy score
	Group 1	0.99
	Group 2	0.99
	Group 3	0.98
	Group 4	0.99
	Group 5	0.98
	Group 6	0.98
	Group 7	0.99
	Group 8	0.98
	Group 9	0.99
	Group 10	0.99


Jack Collier

Claire Guissart

Monika Oláhová

Souphatta Sasorith

Florence Piron-Prunier

Fumi Suomi

David Zhang

Nuria Martinez-Lopez

Nicolas Leboucq

Angela Bahr

Developmental Consequences of Defective ATG7-Mediated Autophagy in Humans

à la diffusion de documents scientifiques de niveau recherche, publiés ou non, émanant des établissements d'enseignement et de recherche français ou étrangers, des laboratoires publics ou privés.


Clément Aubert

Thomas Rubiano

Neea Rusch

Thomas Seiller

An extended and more practical mwp flow analysis

Keywords: Static Program Analysis, Implicit Computational Complexity, Automatic Complexity Analysis, Program Verification

Introduction

This work takes a step further in the implementation of static analysis methods inspired from work in implicit computational theory [START_REF] Dal Lago | A short introduction to implicit computational complexity[END_REF], and more particularly the series of work from the so-called flow analysis of the "Copenhagen school", notably Neil Jones, Lars Kristiansen, and Amir Ben-Amram. The Copenhagen school approach to implicit computational complexity initiates in the celebrated size-change principle of Ben Amram [START_REF] Ben-Amram | Linear, polynomial or exponential? complexity inference in polynomial time[END_REF] to characterise termination of programs, and evolved in more precise techniques to capture resource usage and more particularly growth rate between variables' sizes. The overall flow analysis approach is related in spirit to abstract interpretation [START_REF] Cousot | Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints[END_REF][START_REF] Cousot | Static determination of dynamic properties of recursive procedures[END_REF]; as noted by Jones [START_REF] Jones | Abstract Interpretation: A Semantics-Based Tool for Program Analysis[END_REF] it bounds transitions between states (e.g. commands) instead of states. A first work implemented this technique to develop a static analysis tool detecting loop quasi-invariants [START_REF] Moyen | Loop quasi-invariant chunk detection[END_REF][START_REF] Moyen | Loop quasi-invariant chunk motion by peeling with statement composition[END_REF].

One landmark result in this series of work is the precise and detailed analysis of the relationship between the resource requirements of a computation and the way data might flow during the computation [START_REF] Jones | A flow calculus of mwp-bounds for complexity analysis[END_REF]. Thanks to a typing system resting on matrices with coefficients in the so-called mwp semi-ring, programs in a basic imperative language could be guaranteed to have variables growing at most polynomially with respect to their inputs. While this does not ensure termination, it provides a certificate that if the program terminates, it will do so in polynomial time and using at most polynomial space. We here continue in this direction and implement this "mwp-bounds analysis" [START_REF] Jones | A flow calculus of mwp-bounds for complexity analysis[END_REF] on a fragment of the C programming language [START_REF] Aubert | An implementation of flow calculus for complexity analysis (tool paper)[END_REF].

Our contribution is both of practical and theoretical interest: a python program analyzing C source code is currently being developed [START_REF] Aubert | An implementation of flow calculus for complexity analysis (tool paper)[END_REF], and documented at https://seiller.github.io/pymwp/. This implementation largely benefited from the improvements discussed in the current paper and triggered the development of a modified analysis allowing for the use of more efficient algorithms to carry out the analysis. However, our theoretical contributions can be read independently from this implementation, and answers some of the questions asked by Jones and Kristiansen [14, Section 1.2], notably pushing further their method. Two of those questions are 1. Can the method be extended to richer languages? 2. How powerful and convenient is this method? We answer the first question positively, by adding treatment of function definition and calls, and by implementing the analysis on an actual programming language instead of a simple imperative language. Our work suggests that to answer the second question precisely, a lot of care is needed: the analysis uses matrices in a non-deterministic way to compute the influence of variables on each others, resulting in objects growing exponentially in number. By altering the semi-ring at the core of the original analysis, we show not only that more parsimonious methods can be used, but also that the mathematical machinery can be substituted. While our alternative approach essentially carries out the same analysis, we improved the implementability (and in fact implemented it already), re-usability and efficiency of the techniques while illustrating that the general method could be adapted easily for different types of analysis.

Complexity, resource growth and implementations: a brief tour

Our approach is conceptually guided by implicit computational complexity, that generally focus on restricting e.g. recursion [START_REF] Bellantoni | A new recursion-theoretic characterization of the polytime functions (extended abstract)[END_REF][START_REF] Leivant | Stratified functional programs and computational complexity[END_REF] or type systems [START_REF] Baillot | Light types for polynomial time computation in lambda-calculus[END_REF][START_REF] Lafont | Soft linear logic and polynomial time[END_REF] to insure that a programming language captures a particular complexity class, or perform amortized resource analysis [START_REF] Hofmann | Multivariate amortised resource analysis for term rewrite systems[END_REF]. The particular domain concerned here, data-flow analysis, more specifically focuses on measuring or restricting loops in imperative programs [START_REF] Jones | A flow calculus of mwp-bounds for complexity analysis[END_REF][START_REF] Kristiansen | On the computational complexity of imperative programming languages[END_REF][START_REF] Niggl | Certifying polynomial time and linear/polynomial space for imperative programs[END_REF] and was implemented on e.g. low level assemblylike programs [START_REF] Moyen | Resource control graphs[END_REF].

However, our work is probably best compared with approaches coming from other communities sharing the same goal of finding worst case resource con-sumption. Complexity analyzers of different languages, such as SPEED [START_REF] Gulwani | Speed: Precise and efficient static estimation of program computational complexity[END_REF] for C++, COSTA [START_REF] Albert | Costa: Design and implementation of a cost and termination analyzer for java bytecode[END_REF] for Java bytecode, RaML for OCaml [START_REF] Lichtman | Arrays and references in resource aware ML[END_REF] or Cerco [START_REF] Amadio | Certified complexity (cerco)[END_REF] for C all attempts to generate (possibly certified) cost annotation on (subsets of) programming languages in use.

Contribution: a different take on implementing the theory

We would like to argue that the "mwp" approach we are extending and making more practical is different from the previously mentioned implementations in four respects: 1. it is focused on the growth of variables instead of focusing on their possible values, 2. it is modular, in the sense that the internal machinery can be altered -as we illustrate in this paper -without the need to re-develop large chunks of the theory, 3. it is at the same time language-independent, as it reasons abstractly on imperative languages, and easy to port, as we illustrate with our implementation [START_REF] Aubert | An implementation of flow calculus for complexity analysis (tool paper)[END_REF], 4. it focuses on characterizations of "chunks" of any size of the program allowing to abstract values and their encoding.

Background: the original flow analysis

We here quickly recall the original syntax of the imperative language, that we will extend with function call and definition in Sect. 4, then the original analysis by Jones and Kristiansen and its mathematical machinery.

Language analyzed: fragments of imperative language

We will be using the following imperative programming language, where variables range over R, X, X', Y, Z and Xi for i ∈ N, and need not to be declared, and given the binary operations on expression -, +, and ×, and on booleans • (such as ∧, ∨, etc.), and a collection of comparison operators between expressions .

C :=X = e if b then C else C while b do {C} loop X {C} C ; C (Command)
The semantics is straightforward, with loop X {C} meaning "do C X times" and C;C being used for sequentiality ("do C, then C"). We generally write "program" for a series of commands composed sequentially.

A Flow Calculus of mwp-Bounds for Complexity Analysis

The original paper [START_REF] Jones | A flow calculus of mwp-bounds for complexity analysis[END_REF] studies flows between variables in imperative programs, that are of three types: maximum, w eak polynomial and polynomial flows characterize the three forms of controls from one variable to another, with increasing growth rate 4 . The programs are written in (a variation on) the language presented in Sect. 2.1, and the bounds are represented and calculated thanks to vector and matrices whose coefficients are elements of the mwp semi-ring.

Definition 1 (mwp semi-ring, matrix algebra). Letting mwp = {0, m, w, p} with 0 < m < w < p, and α, β, γ range over mwp, the mwp semi-ring (mwp, 0, m, +, ×) is defined with + = max, α × β = max(α, β) if α, β = 0, and 0 otherwise.

Fixing a natural number n, we use M , A, B, C, . . . to denote n × n matrices over mwp, M ij for the coefficient in the ith row and jth column of M , + for the component wise addition, and × for the product of matrices defined in a standard way. The 0-element for the addition is 0 ij = 0 for all i, j, and the 1-element for product is

1 ii = m, 1 ij = 0 if i = j, and the resulting structure M(mwp) is a semi-ring. Finally, M 0 = 1, M m+1 = M × M m and the closure operator • * is defined as M * = 1 + M + (M 2 ) + . . ..
Although not crucial to understand our development, details about strong semi-rings and the mwp semi-ring can be found in Sect. A.1, and the general construction of a semi-ring whose elements are matrices with coefficients in a different semi-ring -so, in particular, M(mwp) -is given in Sect. A.2.

Below, we let V 1 , V 2 be column vectors with values in mwp, αV 1 to be the usual scalar product, and V 1 + V 2 to be defined component-wise. We write { α i } for the vector with 0 everywhere except for α in its ith row, and

{ α i , β j } for { α i } + { β j }.
Given a matrix M and a vector V , M j ← -V is M with the jth column vector replaced by V . We write { α i → j} for the matrix M with M ij = α and 0 everywhere else, and var(e) for the set of variables in the expression e. In the analysis, the assumption is made that exactly n different variables are manipulated throughout the analyzed program, n-vectors are assigned to expressions and n × n matrices are assigned to commands using rules reminded in Figure 1 [14, Section 5].

The intuition is that if ⊢ jk C : M can be derived using these rules, then all the values computed by C will grow at most polynomially w.r.t. its inputs: this is the core and powerful result of the original paper [START_REF] Jones | A flow calculus of mwp-bounds for complexity analysis[END_REF]Theorem 5.3]. Furthermore, the coefficient at M ij carries quantitative information about the way Xi depends on Xj, knowing that 0-and m-flows are harmless and without constraints, but that w-and p-flows are more harmful w.r.t. polynomial bounds and need to be handled with care, particularly when used in loops -hence the condition on the L and W rules. Although simple in appearance, the proof techniques are far from trivial, but the relative simplicity of the derivation and of the matrices manipulated make the analysis flexible and easy to carry.

In fact, the assignment may fail in case of loops-that is, some programs may not be assigned a matrix-, as at least one of the variables used in the body of the loop may depend "too strongly" upon another, making it impossible to ensure polynomial bounds on the loop itself (as iterating the body can lead to super-polynomial dependencies).

E1 ⊢jk Xi : { m i } E2 ⊢jk e : { w i | Xi ∈ var(e)} ⊢jk e1 : V1 ⊢jk e2 : V2 ⋆ ∈ {+, -} E3 ⊢jk e1⋆e2 : pV1 + V2 ⊢jk e1 : V1 ⊢jk e2 : V2 ⋆ ∈ {+, -} E4 ⊢jk e1⋆e2 : V1 + pV2
(a) Rules for assigning vectors to expressions To capture a larger class of programs, the calculus used to assign a matrix to a program -that corresponds to a proof search in a derivation system -is nondeterministic. As a consequence, multiple matrices-hence, multiple polynomial bounds-may be assigned to the same program.

⊢jk e : V A ⊢jk Xj = e : 1 j ← -V ⊢jk C1 : A ⊢jk C2 : B C ⊢jk C1 ; C2 : A × B ⊢jk C1 : A ⊢jk C2 : B I ⊢jk if b then C1 else C2 : A + B ⊢jk C : M ∀i, M * ii = m L ⊢jk loop Xl {C} : M * + { p l → j | ∃i, M * ij = p} ⊢jk C : M ∀i, M * ii = m
We will use the following example (of "iteration-dependent" loop [14, Example 3.4]) as a common basis to discuss our improvements.

Example 1. Consider the command loop X3{X2= X1 + X2}. The body of the loop -the expression X1 + X2 -admits 3 different derivations that we name π 0 , π 1 and π 2 :

E1 ⊢ jk X1 : m 0 0 E1 ⊢ jk X2 : 0 m 0 E3 ⊢ jk X1 + X2 : p m 0 E1 ⊢ jk X1 : m 0 0 E1 ⊢ jk X2 : 0 m 0 E4 ⊢ jk X1 + X2 : m p 0 E2 ⊢ jk X1 + X2 : w w 0
From π 0 , the derivation of loop X3{X2= X1 + X2} can be completed, but since the L rule requires to have only m coefficients on the diagonal, π 1 cannot be used to complete the derivation, because of the p coefficient in a box below: . . . . π 0 ⊢ jk X1 + X2 :

p m 0 A ⊢ jk X2 = X1 + X2 : m p 0 0 m 0 0 0 m L ⊢ jk loop X3 {X2 = X1 + X2} : m p 0 0 m 0 0 p m . . . . π 1 ⊢ jk X1 + X2 : m p 0 A ⊢ jk X2 = X1 + X1 : m m 0 0 p 0 0 0 m
Similarly, because of the w coefficient on the diagonal after applying A, π 2 cannot be used to complete the derivation either, and hence only one derivation for this command holds. Note that in general, multiple derivations can exist and that this "indeterminacy" [14, Section 8] is needed to capture as many programs as possible.

"Taming" non-determinism and non-termination

The first two improvements over the existing analysis we offer are to:

1. "internalize" the non-determinism, so that at most one matrix per command is produced, 2. "internalize" the failure, so that at least one matrix per command is produced. These changes were introduced first to obtain an efficient (or, actually, to simply enable an) implementation, but they came with by-products. Indeed, the naive approach consisting in producing a list of all possible matrices corresponding to all the non-deterministic choices (and removing those matrices for which the analysis fails) would result in a very slow implementation even for small programs.

To represent non-determinism, we use in the matrices functions from choices to coefficients in mwp instead of simply coefficients in mwp. This is explained by the following remark -made formal in Sect. A.3: the overall analysis produces a function from a space of choices C to the space M(mwp) of matrices over the mwp semi-ring, i.e. it results in a function C → M(mwp). But there is a semi-ring isomorphism between C → M(mwp) and M(C → mwp), i.e. matrices whose coefficients are functions from choices to the mwp semi-ring. We use this, together with a clever representation of the space C → M(mwp) to provide an alternative formalism allowing for more efficient implementation. Moreover, compacting all the possible derivations into one matrix results in a gain of space and time as different matrices obtained from different choices are more or less the same, i.e. they usually differ only on a few coefficients, leading to a quite compact representation. As a side-product, this also allows the user to be presented with different polynomial bounds, so that they can pick the one that suits their needs.

Concerning failure, we extend the mwp semi-ring with a special value ∞; one key point is that the resulting structure is not a strong semi-ring-as opposed to mwp or M(mwp)-because the latter structure requires the equality 0 × ∞ = 0 to hold while we need 0 × ∞ = ∞ to avoid overlooking some super-polynomial computations: if part of the program computes an exponential value but then throws it away, 0 × ∞ = 0 would hide the super-polynomial computation, resulting in an incorrect analysis 5 . This way of representing failure also has the advantage of being local, so that which input variable impacts which variable in a non-polynomial way can be precisely pinpointed. We believe this feature can be of crucial use in a situation where some variables are known to be of small size, hence where a non-polynomial bound on particular input variables is acceptable.

Taken together, our improvements insure that exactly one matrix will always be assigned to a program, but also gives an opportunity to chose between "the lesser of two evils" when it fails: if two derivations produce ∞ coefficients on different flows, the user could decide to privilege one over the other based on knowledge about the inputs' sizes.

We give in Figure 2 the alternative system we are introducing in full, but will gently discuss it though the remaining parts of this section and in Sect. 4: note that the A, C and I rules are unchanged (even if the sum and product are in a different semi-ring) and that the call rule is new.

⋆ ∈ {+, -} E A ⊢ Xi⋆Xj : (0 → { m i , p j }) + (1 → { p i , m j }) + (2 → { w i , w j }) E M ⊢ Xi * Xj : { w i , w j } (a) New rules for assigning vectors to expressions ⊢ e : V A ⊢ Xj = e : 1 j ← -V ⊢ C1 : A ⊢ C2 : B C ⊢ C1 ; C2 : A × B ⊢ C1 : A ⊢ C2 : B I ⊢ if b then C1 else C2 : A + B ⊢ C : M L ∞ ⊢ loop Xl {C} : M * + { ∞ j → j | M * jj = m} + { p l → j | ∃i, M * ij = p} ⊢ C : M W ∞ ⊢ while b do {C} : M * + { ∞ j → j | M * jj = m} + { ∞ i → j | M * ij = p} call ⊢ Xi = F(X1,. . ., XN) : 1 i ← -((0 → M (f )0) + . . . + (k → M (f ) k ))
(b) New rules for assigning matrices to commands Fig. 2: New rules 5 Here we can be a bit more detailed: while throwing away the infinite coefficient would hide the super-polynomial computation, it would not contradict the ultimately polynomial dependency of the values w.r.t. the inputs. As such, 0 × ∞ = 0 could still be used to bounds values, at the cost of losing the bounds on time and space usage for terminating programs. A modular implementation allowing to decide which structure to use in under progress.

Choice data flow semi-rings

The first step towards our "internalization of choice" is to design the correct semiring. We start by reasoning abstractly, the detail of this construction is given in Sect. A.3. Given a strong semi-ring S, we define M(S) to be the strong semi-ring whose elements are matrices with coefficients in S (Lemma 3), similarly to the matrix algebra of Definition 1. We also define A → S to be the strong semiring whose elements are functions from a set (of choices) A to S (Lemma 4). We furthermore observe (Lemma 5) that for all set A and strong semi-ring S, M(A → S) and A → M(S) are isomorphic (Definition 3). By chosing A = p i=1 A i , it follows that there exists an isomorphism

M( p i=1 A i → S) ∼ = p i=1 A i → M(S)
for all family of sets (A i ) i=1,...,p , using the usual cartesian product of sets. This dual nature of the semi-ring considered will be useful:

-we implement the analysis by assigning elements of M( p i=1 A i → mwp), this allows for a more efficient implementation by using some clever representation of elements of p i=1 A i → mwp detailed in Sect. 5; -we use the representation of the resulting matrix M as an element of p i=1 A i → M(mwp) to produce, from an assignment α = (a 1 , a 2 , . . . , a p ) ∈ p i=1 A i , a matrix M [α] ∈ M(mwp), recovering the mwp-flow that would have been computed by making the choices a 1 , a 2 , . . . in the derivation.

Remark 1. As the unique degree of non-determinism in the rules to assign a matrix to commands is 3 at this point (cf. Example 1), our modification of the analysis flow consists simply (for the moment) in recording the different choices by letting A i = {0, 1, 2} for all i = 1, . . . , p where p is the number of times a choice had to be taken. Note that in a later section, other sets A i will be used in order to deal with function calls. Where we make the abuse of notation of writing 0 for {0 → 0, 1 → 0, 2 → 0}. 6Since, in particular7 , M({0, 1, 2} → mwp) ∼ = {0, 1, 2} → M(mwp), the obtained vector can be rewritten as 0

→ p m 0 , 1 → m p 0 , 2 → w w 0 .
Our derivation system replaces the E3 and E4 rules with a single rule E A (for "additive"), and imposes an additional restriction on E2, thus giving E M (for "multiplicative"), so that it is used only when E1 followed by E2 or E3 cannot be applied.

The implementation of binary additive operators (-and +) with E A captures all possible choices for distinct operands and merges i and j into a single coefficient when i = j. Binary multiplication is handled by applying the E M rule -note that the application of E2 to additive operators in the original system is still handled by the last choice present in E A . Given this need to treat binary operations differently, based on operators and combinations of operands, more work is needed to handle statements of greater arity. As the implementation already processes abstract syntax trees of C commands recursively, handling operations of greater arity will require implementing additional recursive steps, but we do not expect that to be problematic conceptually or at the level of implementation. At the light of this reflection, and knowing that there is no benefit in applying E2 to a single variable, as it result in a w coefficient being applied in lieu of a lesser m coefficient, it is easy to observe that E A and E M are as expressive as E1, E2, E3 and E4 taken together -something we will be using when proving the equi-expressiveness of our system (Lemma 1).

Representing failure with an "infinity" coefficient

The original analysis would stop whenever a non-polynomial flow was detected, putting an end to the chosen strategy (i.e. set of choices) and restarting from scratch with another one. We will now discuss the fact that every derivation can be completed even in the presence of non-polynomial flows, which constitutes our second improvement. This is done by first extending the mwp semi-ring with a new element. While this approach results in derivations for program where some variables are not polynomially related to their inputs, we argue that pinpointing which variables are "faulty" from within the analysis can have benefits.

The first step is to incorporate a top element ∞ into our semi-rings to represent undefined elements. The semi-ring mwp ∞ we will be using is hence (mwp ∪ {∞}, 0, m, + ∞ , × ∞ ), with ∞ > α for all α ∈ mwp, + ∞ = max as before, and α × ∞ β = 0 if α, β = ∞ and α or β is 0, max(α, β) otherwise. This different condition in the definition of × ∞ insures that once non-polynomial flows have been detected, they cannot be erased (as ∞ × ∞ 0 = ∞), but comes at the price of the strength of the semi-ring (the details are discussed in Sect. A.4).

Below, we will work with M(mwp ∞ ), write × for × ∞ and similarly for +, and remind the reader that we write { α i → j} for the matrix M with M ij = α and 0 everywhere else. The only cases where the original analysis may fail is if the side condition of L or W (Figure 1) are not met; we now replace those by the rules L ∞ and W ∞ of Figure 2, with no side condition.

Those rules, which can always be applied, simply replace the problematic coefficients with ∞. Note that in the cases for which the original rule is applicable, the results coincide. This will be essential to prove that our modified analysis is coherent with Jones and Kristiansen's original approach (Lemma 1).

Merging the two improvements: illustration with operations

We introduced and discussed the deviations from the original system for the "axiomatic" / "expression" (E A , E M ) and "loop" rules (L ∞ and W ∞ ), but remains to briefly discuss the rules for assignment (A), if (I) and the composition (C), that remained unchanged. Those rules are the place where both improvements meet. Mathematically speaking, adopting the semi-ring defined over matrices using coefficients in {0, 1, 2} m → mwp ∪ {∞} is fairly simple, but computationally speaking, simple operations like multiplication and addition of matrices become very costly and memory-demanding. This became particularly problematic when keeping a usable implementation in mind, and is illustrated below.

Example 3. In our new system, consider the following derivation:

E A ⊢ X1 + X2 : V A ⊢ X1 = X1 + X2 : 1 1 ← -V E A ⊢ X1 -X3 : V ′ A ⊢ X1 = X1 -X3 : 1 1 ← -V ′ I ⊢ if b then {X1= X1+ X2} else {X1= X1-X3} : (1 1 ← -V ) + (1 1 ← -V ′ ) with V = 0 → { m 1 , p 2 } + 1 → { p 1 , m 2 } + 2 → { w 1 , w 2 } V ′ = 0 → { m 1 , p 3 } + 1 → { p 1 , m 3 } + 2 → { w 1 , w 3 } 1 1 ← -V = m 0 0 0 m 0 0 0 m 1 ← -V ∼ = (0 →m)+(1 →p)+(2 →w) 0 0 (0 →p)+(1 →m)+(2 →w) m 0 0 0 m 1 1 ← -V = m 0 0 0 m 0 0 0 m 1 ← -V ′ ∼ = (0 →m)+(1 →p)+(2 →w) 0 0 0 m 0 (0 →p)+(1 →m)+(2 →w) 0 m
Now, to perform the addition required by the I rule, some care is needed: indeed, the choices in the left branch of the derivation are independent from the choices in the right branch, and we must use coefficients in {0, 1, 2} 2 → mwp to represent the 2 3 choices. Assuming the choice in the left branch is first, we obtain e.g. for the beginning of the top-left coefficient (the complete coefficient will be given below, once we introduced a more compact notation):

(0 → (0 → (m+m = m)))+(0 → (1 → (m+p = p)))+(0 → (2 → (m+w = w)))
Writing ab → for a → b →, with a, b ∈ {0, 1, 2}, and a → (resp. a →) if the second (resp. first) choice has no impact on the resulting coefficient, we can let:

A = 00 → m + 01 → p + 02 → w + 1 → p + 20 → w + 21 → p + 22 → w to obtain (1 1 ← -V ) + (1 1 ← -V ′ ) = A 0 0 (0 →p)+(1 →m)+(2 →w) m 0 ( 0 →p)+( 1 →m)+( 2 →w) 0 m
Although the presentation and numbering diverge a bit, the example at https://seiller.github.io/pymwp/demo/#improvement_paper_example3.c can help the curious reader to check that the implementation reflects this derivation correctly.

Example 4. Re-using Example 1, we now obtain in our new system a derivation that assign to loop X3 {X2 = X1 + X2} the unique matrix

m (0 →p)+(1 →m)+(2 →w) 0 0 (0 →m)+(1 →∞)+(2 →∞) 0 0 (0 →p)+(1 →0)+(2 →0) m
where we observe that 1. only one choice (0) -one assignment -gives a matrix without ∞ coefficient, corresponding to the fact that, in the original system, only π 0 could be used to complete the proof, 2. the choice impact the matrix only locally, the coefficients being mostly the same, independently from the choice, 3. the influence of X2 on itself is where possible non-polynomial growth rates lies, as the ∞ coefficient are in the second column, second row. This example was not implemented, as loop is not a standard C operator, but is currently being implemented as a restricted form of for loop (cf. https://github.com/seiller/pymwp/issues/5).

We are now in possession of all the material and intuitions to state the correspondence between our approach and the one of Jones and Kristiansen.

Lemma 1. Given a program P , there is a single matrix M ∈ M({0, 1, 2} p → mwp ∞ ) such that P ⊢ M , i.e. the system is deterministic. Moreover, for any assignment α = (a 1 , . . . , a p ) ∈ A p , we have that

P ⊢ jk M [α] if and only if M [α] ∈ M(mwp).
This shows that the performed analyses coincide, as M [α] ∈ M(mwp) implies that no ∞ coefficient occurs in it. However, our alternative definition should be understood as an important improvement, as it allows for a more efficient implementation (Sect. 5). But before discussing the efficiency of the implementation, we will now explain the natural but important extension to function calls enabled by our alternative formalism.

Extending the analysis with function calls

We begin by extending the syntax presented in Sect. 2.1 by adding function declarations F := f(X1, . . ., XN){C; return R} and a command that performs a function call and assign its return value to a variable Xi = F(X1, . . ., XN) 8 . A program is now a series of function declarations, with one of them called main with N = 0, and such that all the commands of the form Xi = F(X1,. . ., XN) refers to a function previously declared. A chunk is simply a series of commands inside a function declaration 9 .

One of the key points of our contribution is the extension of the analysis to function calls, in a way that can be used in practice, as we handle a function f with a single analysis that stores a minimal amount of data for latter calls. The principle is the following: given the matrix M (f ) obtained from the analysis of the program computing f , we store only the k choices for which no ∞ coefficients appear, and then project them to only keep track of the different input/output behaviors, merging choices leading to the same result. After this operation, we are left with a family M (f ) 0 , M (f ) 1 , . . . , M (f ) k of matrices10 that should be understood as providing quantitative (i.e. polynomial, weak polynomial, maximum, or zero) information about the dependency of output values w.r.t. input values. Now, the analysis of the command calling the function f is dealt with by the call rule of Figure 2.

Formally, we show that our definition of composition is coherent with the initial analysis as follows. We consider two chunks: the first chuck P contains a call to a function f , the second is obtained by replacing within P the call to the function f by inserting in its place the sequence of commands F computing f . This second chunk is called P [F ]. We then prove that the matrix associated to P is "the same" 11 Intuitively, this mechanism provides the expected result because the choices made in the chunk F do not affect the context P [•], and the variables used in the chunk F are not used in the context P [•] except for the return variables.

More formally, let P be a chunk of program, containing a call to the function f , and let F be the chunk computing the function f . We define from P the context P [•], a chunk containing a hole [•] to be filled with the chunk F , obtained as follows (supposing f has a single output variable).

-We remove the line with the function call, say Xi=f(X1, . . ., XN);.

-We add in place the following lines, where R, Y1, . . ., Yn are fresh variables:

Y 1 = X 1 ; . . . YN = XN ; [•] Xi = R ;
The code P [F ] is then obtained by defining a chunk F , and inserting it in place of the symbol • in P [•]. The chunk F is obtained as follows from F :

-the header is removed, -the input variables of F are renamed to Y1, Y2, . . ., YN, -the variable returned by f is renamed to R, the return statement is removed, -all other variables are renamed if needed to avoid using the same names as the variables in P [•]. We write the set of these variables V F .

Example 5. Refer to Figure 3 for a simple example of the code transformation for in-lining a function call. Some non-deterministic choices may appear within the (modified) chunk F inside P [F ], i.e.

P = int main (){ X 3 = X 1 + X 2 ; X 2 = X 3 + X 1 ; X 1 = f ( X 2 ); } P [•] = int main (){ X 3 = X 1 + X 2 ; X 2 = X 3 + X 1 ; Y 1 = X 2 ; [•] X 1 = R ; } Q = int f ( int X 1 ){ loop X 1 { X 2 = X 2 + X 3 }; return X 2 ; } Q = loop Y 1 { R = R + X 4 };
-the coefficients of the matrix M (P ) are elements of the semi-ring p+1 i=1 A i → M(mwp), with one particular choice corresponding to the call rule -we write the corresponding index i 0 ; -the coefficients of P [F ] are elements of the semi-ring

p+k i=1 B i → M(mwp),
where k choices are made within the chunk F -we write the corresponding indexes j 1 , j 2 , . . . , j k (note these are in fact consecutive indexes). We note π : {1, . . . , p + k} → {1, . . . , p + 1} the projection of the choices in P [F ] onto the corresponding choices in P , i.e.

π(j) =    j if j < j 0 i 0 if j 0 j < j k j -k + 1 if j k < j
We note that each matrix used as axiom in the function call corresponds to a specific assignment on indexes j 1 , . . . , j k . We write Ψ : A i0 → j k i=j1 B i the corresponding injection. This is extended to Ψ : p+1 i=1 A i → p+k i=0 B i in a straightforward way.

We can now state the main theorem showing that the call rule adequately analyses function calls.

Theorem 1. For all assignment α of p+1 i=1 A i ,

M (P )[α] = (1 -Π P )(M (P [F ]))[ Ψ (α)]
Moreover, for all assignment β of p+k i=0 B i not in Im( Ψ ), the matrix (1-Π P )(M (P [F ])[β]) contains an infinite value.

Proof. To prove this, we first notice that it is sufficient to prove it for the simplest chuck P containing only one command: Xi = f(X1, . . ., XN). This is explained by the compositional nature of the analysis (a sequence of commands is simply assigned the product of the matrices of each individual command). Then, checking that the theorem holds in this case is a straightforward, though tedious (due to keeping track of all indices), computation.

Implementation of the analysis

The formulation of the extended mwp analysis exposed in the previous sections was also intended for implementation. As such, the choice of the representation of non-determinism -for instance -was also guided by our wish for a faster analysis, something not discussed in depth in our tool paper [START_REF] Aubert | An implementation of flow calculus for complexity analysis (tool paper)[END_REF], or our documentation. In this section, we expose some of the specific choices made in the implementation.

Non-determinism, and the challenges to efficient calculations

As explained in the above sections, the result of the analysis is a matrix with coefficients in a semi-ring of the form p i=1 A i → M(mwp)-setting aside ∞ coefficients for a moment. To implement this correctly, we represent elements of this semi-ring as polynomials w.r.t. the generating set given by the functions δ(i, j) : p i=1 A i → mwp defined by δ(i, j)(a 1 , a 2 , . . . , a p ) = m if a j = i and δ(i, j)(a 1 , a 2 , . . . , a p ) = 0 otherwise. i.e. an element of p i=1 A i → mwp is represented as a polynomial n i=1 α i ki j=1 δ(a i,j , b i,j ) with α i ∈ mwp. This basis have an important property: the monomials α i ki j=1 δ(a i,j , b i,j ) in a polynomial can be ordered in such a way that the product with another monomial is ordered. i.e. if m m ′ and both m × n and m ′ × n are non-zero, then m × n m ′ × n. This order is leveraged to obtain efficient algorithms for computing operations on the representation of coefficients, similar to what is done using Gröbner bases for computation of standard polynomials. For instance, the algorithm for multiplication of polynomials makes use of the property above and proceeds as follows to compute the product of a polynomial P with n i=1 α i ki j=1 δ(a i,j , b i,j ) (supposing the representation of P is ordered): 1. compute the products P i = P × α i ki j=1 δ(a i,j , b i,j ) for all i; 2. compare and order a list L of all the first elements of those polynomials; 3. append the smallest element to the result and remove it from the corresponding P i ; 4. insert the (new) first element of P i to the list L if it exists; 5. if L is non-empty, go back to step 3. This clever method has some very concrete consequences. As an example, our explosion.c program calls the multiplication 11,907 times and could not be completed with a naive multiplication implementation. More precise profiling further exposes the need for this optimization.

Infinite values cluttering the analysis, and difficulties to evaluate

One very costly aspect of the analysis is the evaluation step which takes a matrix with coefficients in p i=1 A i → mwp and checks all possible assignments (a 1 , . . . , a p ) ∈ p i=1 A i to look for infinite coefficients. While this step is necessary (in one form or another) if one wishes to produce the actual mwp matrices certifying polynomial bounds (something needed at least once to allow for function calls), we implemented a specific data structure allowing to keep track of infinite assignments on the fly, thus allowing the analysis to provide a qualitative answer quickly. I.e. the analysis can ensure the existence or not of mwp-bounds without computing the corresponding matrix.

This is implemented by a structure we called delta graphs. This is a graph whose vertices are monomials; the graph is populated during the analysis by adding those monomials that appear with an infinite coefficient -i.e. possible choices leading to ∞ in the resulting matrix. This graph is structured in layers: each layer corresponds to the size of the monomials it contains (the number of deltas δ(i, j) is contains). The intuition is that a monomial -or rather a list of deltas δ( , )-defines a subset of the space p i=1 A i ; the less deltas in the monomial, the greater the subspace represented. (Note here that our intuitions come from the standard topological structure of spaces of infinite sequences, where such a monomial represents a "cylinder set", i.e. an element of the standard basis for open sets.) As we populate the delta graph, we create edges within a given layer to keep track of differences between monomials: we add an edge labeled i between two monomials if and only if they differ only on one delta δ( , i) (i.e. one is obtained from the other by replacing the first index of δ( , i)). This is used to implement a "fusion" method on delta graphs which simplifies the structure: as soon as as a monomial m in layer n has Card(A i )-1 outgoing edges labelled i, we can remove all these monomials and insert a shorter monomial in layer n -1 (obtained from m by simply removing δ( , i)). This implements the fact that

Card(Ai)-1 k=0 mδ(k, j) = m.
Remember the delta graph represents the subspace of assignments for which an infinite coefficient appeared. So if at some point the delta graph is completely simplified (i.e. "fusions" to the graph with a unique monomial consisting in an empty list of δ( , )), it means the whole space of assignments is represented and no mwp-bounds can be found. On the contrary, if the analysis ends with a delta graph different from the completely simplified one, it means at least one assignment exists for which no infinite coefficients appear, and therefore at least one mwp-bound exists.

Future work

We here provide some details on extensions of this work that we are currently working on, or that will be tackled in the near future.

The first natural line of work is the extension of the language analysed, in particular to accommodate other data structures. While structures such as lists should not be problematic, dealing with pointer will certainly require more involved work, in particular to ensure the theoretical results obtained by Jones and Kristiansen hold, i.e. that the obtained mwp-bounds are indeed correct. These extensions, together with the extension to function calls discussed in this paper, will then be added within our implementation of the analysis.

A second line of work that was already started is to implement the analysis in the Compcert compiler [START_REF] Leroy | Formal verification of a realistic compiler[END_REF], which would allow for a formal certification of the polynomial bounds computed by the analysis using the Coq proof assistant [START_REF]Coq documentation[END_REF]. Some preliminary work in this direction was already done. In particular, it seems natural to use compcert-ssa [START_REF] Barthe | Formal verification of an ssa-based middleend for compcert[END_REF] to be later used as stepping stone towards an implementation within llvm -and if possible certified-llvm [START_REF] Zhao | Formal verification of ssa-based optimizations for LLVM[END_REF] -which would enable the analysis to programs written in other languages than C.

A Technical Appendix on Semi-rings

A.1 The mwp semi-ring

This subsection briefly recall semi-ring definition and proves that the mwp semiring is indeed a semi-ring.

Definition 2 (Semi-ring). A semi-ring S = (S, 0, 1, +, ×) is specified by a set S and two binary operations + (addition) and × (multiplication) such that {0, 1} ∈ S and 1. (S, 0, +) is a commutative monoid: the operation + is associative, commutative, and has 0 as the identity element, 2. (S, 1, ×) is a monoid: the operation × is associative and has 1 as the identity element, 3. the operation × distributes with respect to +: for all a, b, c ∈ S, a

× (b + c) = a × b + a × c and (b + c) × a = b × a + c × a
We call S a strong semi-ring if, additionally, 0 annihilates S, i.e.

4. 0 × a = a × 0 = 0 for all a ∈ S.

Lemma 2 (mwp-semi-ring). The tuple ({0, m, w, p}, 0, m, +, ×), with -0 < m < w < p,

-α + β = α if α β β otherwise -α × β = α + β if α = 0 and β = 0 0 otherwise is a strong semi-ring.
Proof. We prove that ({0, m, w, p}, 0, m, +, ×) as defined respects the conditions of Definition 2. The proof is straightforward but detailed nevertheless.

({0, m, w, p}, 0, +) is a commutative monoid We prove that ({0, m, w, p}, +) is a commutative monoid by showing that it is associative, commutative, and has 0 as identity.

Associativity (α + β) + γ = α + (β + γ) Case 1: α β γ α = α =⇒ α + γ = α + β =⇒ (α + β) + γ = α + (β + γ) Case 2: α γ β α = α =⇒ α + γ = α + γ =⇒ (α + β) + γ = α + (β + γ) Case 3: β α γ β = β =⇒ β + γ = α + β =⇒ (α + β) + γ = α + (β + γ) Case 4: β γ α β = β =⇒ β + γ = α + β =⇒ (α + β) + γ = α + (β + γ) Case 5: γ α β γ = γ =⇒ α + γ = α + γ =⇒ (α + β) + γ = α + (β + γ) Case 6: γ β α γ = γ =⇒ β + γ = α + γ =⇒ (α + β) + γ = α + (β + γ)
Commutative Property Both cases are immediate:

Case 1: α β =⇒ α + β = α = β + α Case 2: β α =⇒ α + β = β = β + α Identity element is 0 0 + 0 = 0 0 + m = m 0 + w = w 0 + p = p
({0, m, w, p}, m, ×) is a monoid We now prove that ({0, m, w, p}, m, ×) is a monoid by showing that it is associative, has m as identity, and has 0 as the annihilator.

Associativity (α × β) × γ = α × (β × γ)
Case 1: α, β, γ ∈ {m, w, p} α × β = α + β Associativity of operation + is shown in the proof of the commutative monoid, ({0, m, w, p}, +). Case 2: α, β, or γ equals 0 By definition of multiplication, the product is 0.

Identity element is m 0 × m = 0 = m × 0 m × m = m = m × m w × m = w = m × w p × m = p = m × p 0 annihilates {0, m, w, p} 0 × 0 = 0 = 0 × 0 m × 0 = 0 = 0 × m w × 0 = 0 = 0 × w p × 0 = 0 = 0 × p

Distribution of multiplication over addition We conclude by proving that

× distributes over +. Right Distribution α × (β + γ) = (α × β) + (α × γ) Case 1: β γ =⇒ α × β = α × β =⇒ α × (β + γ) = (α × β) + (α × γ) Case 2: γ β =⇒ α × γ = α × γ =⇒ α × (β + γ) = (α × β) + (α × γ) Left Distribution (α + β) × γ = (α × γ) + (β × γ) Case 1: α β =⇒ α × γ = α × γ =⇒ (α + β) × γ = (α × γ) + (β × γ) Case 3: β α =⇒ β × γ = β × γ =⇒ (α + β) × γ = (α × γ) + (β × γ) A.2 Matrix Semi-ring
This subsection explains and details how matrices with coefficients in a semi-ring can be used to construct semi-rings.

Lemma 3. Given a strong semi-ring S = (S, 0, 1, +, ×), we define the tuple M = (M , 0, 1, +, ×), with -M the set of all n × n matrices over S, for all n ∈ N, -0 defined by M = 0 iff M ij = 0 for all i and j, -

1 defined by M = 1 iff M ij = 1 for i = j, M ij = 0 otherwise, -+ defined by C = A + B iff C ij = A ij + B ij , -× defined by C = A × B iff C ij = n k=1 A ik × B kj , is a strong semi-ring.
Proof. We prove that M = (M , 0, 1, +, ×) as defined respects the conditions of Definition 2. Let A,B,C be n × n matrices over S where n ∈ N.

(M , 0, 1, +) is a commutative monoid We first prove that (M , +) is a commutative monoid by showing that it is associative, commutative, and has 0 as identity. Associativity (A+B)+C = A+(B+C) iff ((A+B)+C) ij = (A+(B+C)) ij for all i, j.

((A + B) + C) ij = (A + B) ij + C ij = (A ij + B ij ) + C ij = A ij + (B ij + C ij ) (by associativity of +) = A ij + (B + C) ij = (A + (B + C)) ij Commutative Property A + B = B + A iff (A + B) ij = (B + A) ij for all i, j. (A + B) ij = A ij + B ij = B ij + A ij (by commutativity of +) = (B + A) ij (B × A) ij = n k=1 B ik × A kj = (B ij × A jj ) + n k=1,k =j B ik × A kj = (B ij × 1) + n k=1,k =j
× (B + C) = (A × B) + (A × C) iff (A × (B + C)) ij = ((A × B) + (A × C)) ij for all i, j.
-⊠ defined componentwise: (f ⊠ g)(a) = (f (a)) × (g(a)), for all f , g in F and a ∈ A, is a strong semi-ring.

Proof. (F , 0, ⊞) is a commutative monoid We first prove that (F , 0, ⊞) is a commutative monoid by showing that it is associative, commutative, and has 0 as identity. Associativity

((f ⊞ g) ⊞ h)(a) = (f (a) + g(a)) + h(a) = f (a) + (g(a) + h(a)) (by assoc. of +) = (f ⊞ (g ⊞ h))(a) (by def. of ⊞) Commutativity (f ⊞ g)(a) = f (a) + g(a) = g(a) + f (a) (by commutativity of +) = (g ⊞ f )(a) (by def. of ⊞) Identity element is 0 (0 ⊞ f )(a) = 0(a) + f (a) = 0 + f (a) (by def. of 0) = f (a)
(by identity prop of +) (F , 1, ⊠) is a monoid We now prove that (F , 1, ⊠) is a monoid by showing that it is associative and has 1 as identity. Associativity

((f ⊠ g) ⊠ h)(a) = (f (a) × g(a)) × h(a) = f (a) × (g(a) × h(a)) (by assoc. of ×) = (f ⊠ (g ⊠ h))(a) (by def. of ⊠) Identity element is 1 (1 ⊠ f )(a) = 1(a) × f (a) = 1 × f (a) (by def. of 1) = f (a)
(by identity prop of ×)

Distribution of multiplication over addition We conclude by proving that ⊠ distributes over ⊞. Right Distribution For simplicity, we will write F as A → S = (A → S, 0, 1, +, ×).

(f ⊠ (g ⊞ h))(a) = f (a) × (g(a) + h(a)) = (f (a) × g(a)) + (f (a) × h(a)) (by right distribution of ×) = ((f ⊠ g) ⊞ (f ⊠ h))(a) Left Distribution ((f ⊞ g) ⊠ h)(a) = (f (a) + g(a)) × h(a) = (f (a) × h(a)) + (g(a) × h(a)) (by left distribution of ×) = ((f ⊠ h) ⊞ (g ⊠ h))(a) 0 annihilates F (0 ⊠ f )(a) = 0(a) × f (a) = 0 × f (
Definition 3. We say two semi-rings S = (S, 0, 1, +, ×) and T = (T , 0, 1, ⊞, ⊠) are isomorphic and write S ∼ = T if there exists g : S → T such that -g is a bijection, -g(0) = 0, -g(1) = 1, -g(s 1 + s 2 ) = g(s 1 ) ⊞ g(s 2 ) for all s 1 , s 2 ∈ S -g(s 1 × s 2 ) = g(s 1 ) ⊠ g(s 2 ) for all s 1 , s 2 ∈ S For simplicity, we write g : S → T for such morphisms.

Lemma 5. For all set A and strong semi-ring S, M(A → S) ∼ = A → M(S).

Proof. First, observe that by Lemmas 3 and 4, both A → M(S) and M(A → S) are strong semi-rings, and we write 0 f (resp. 0 M ) and 1 f (resp. 1 M ) for the 0 and 1 elements of A → M(S) (resp. of M(A → S)). Now we have to prove that we can construct a bijection g : M (A → S) → (A → M (S)) that respects the conditions of Definition 3. We define g and g -1 at the same time, then show that they are indeed inverses: Below, we write f M for g(M ). g -1 : (A → M (S)) → M (A → S) Given f ∈ A → M (S), we define g -1 (f ) ∈ M (A → S) to be the matrix of size n × n, for n × n the size of the matrix returned by f , such that (g -1 (f )) i,j is the function that maps a ∈ A to (f (a)) i,j for all i, j. Graphically: Below, we write M f for g -1 (f ).

g -1 (f )a =    (f
g is a bijection We first prove that g • g -1 = g -1 • g = id.

(g (by assoc. of +) In our improvement of the analysis, we add an ∞ element to the mwp-semi-ring, but reason abstractly below with an arbitrary semi-ring and a ⊥ element. Lemma 6. Given a strong semi-ring S = (S, 0, 1, +, ×) and an element ⊥ / ∈ S, S ⊥ = (S ∪ {⊥}, 0, 1, + ⊥ , × ⊥ ) with, for all a, b ∈ S ∪ {⊥},

-1 • g)(M ) = M (g -1 • g)(M ) = g
g(M 1 × M 2 ) = g(M 1 ) × g(M 2 ) g(M 1 × M 2 ) = g(M 1 ) × g(M 2 ) ⇐⇒ f M1×M2 = f M1 × f M2 ⇐⇒ f M1×M2 (a) = (f M1 × f M2 )(a) ⇐⇒ f M1×M2 (a) = (f M1 )(a) × (f M2 )(a) ⇐⇒ (f M1×M2 (a)) ij = ((f M1 )(a) × (f M2 )(a)) ij
a + ⊥ b = a + b if a, b = ⊥ ⊥ otherwise a × ⊥ b = a × b if a, b = ⊥ ⊥ otherwise is a semi-ring.
Proof. The proof is immediate, but note that S ⊥ is not strong, as ⊥×0 = ⊥.

A good intuition on this construction comes from partial functions. Indeed, we can define A ⇀ S as the semi-ring of partial functions from A to S, i.e. of functions from A to S ⊥ . Furthermore, if we identify a matrix in M(S ⊥ ) where at least a coefficient is ⊥ with the matrix ⊥, then we get that M(A ⇀ S) ∼ = A ⇀ M(S). However, note that none of those semi-rings are strong.

b

  :=e e b•b (Boolean expression)

  and ∀i, j, M * ij = p W ⊢jk while b do {C} : M * (b) Rules for assigning matrices to commands

Fig. 1 :

 1 Fig. 1: Original ("Jones-Kristiansen") rules

Example 2 .

 2 Re-using the derivations π 0 , π 1 and π 2 from Example 1, we can now represent the three vectors vector {0 →p,1 →m,2 →w} {0 →m,1 →p,2 →w} 0

Fig. 3 :

 3 Fig. 3: A simple example of "inlining" a function call

  prop. of 0) = (B ij × 1) (by identity of +) = B ij (by identity of ×) 0 annihilates M A × B = 0 and B × A = 0 where A = 0 iff A ij = 0 for all i, j.(A × B) ij =

  prop of 0) (f ⊠ 0)(a) = f (a) × 0(a) = f (a) × 0 (by def. of 0)= 0 (by annihilation prop of 0)

g

  : M (A → S) → (A → M (S)) Given M ∈ M (A → S) of size n × n, we let g(M ) ∈ A → M (S)be the function that maps a ∈ A to M where the same argument a has been applied to the functions f 1,1 , . . . , f n,n . Graphically: g(M )a = g(

  a) 1,1 . . . (f a) 1,n . . . . . . . . . (f a) n,1 . . . (f a) n,n   

  -1 (g(M )) = g -1 (f M ) (where (fM (a))ij = Mij (a)) = M (g • g -1 )(f ) = f (g • g -1 )(f ) = g(g -1 (f )) = g(M f ) (where (M f )ij a = (f (a))ij) = f g(0 M ) = 0 f Let f = g(0 M ), then f = 0 f iff f (a) ij = 0 S for all i, j. f (a) ij = (0 M ) ij (a) = 0 f (a) (by def. of 0 M ) = 0 S (by def. of 0 f ) g(1 M ) = 1 f Let f = g(1 M ), then f = 1 f iff f (a) ij = 1 S for all i = j and f (a) ij = 0 S otherwise. Case 1: i = j f (a) ij = (1 M ) ij (a) = 1 f (a) (by def. of 1 M ) = 1 S (by def. of 1 f ) Case 2: i = j f (a) ij = (1 M ) ij (a) = 0 f (a) (by def. of 1 M ) = 0 S (by def. of 0 f ) g(M 1 + M 2 ) = g(M 1 ) + g(M 2 ) g(M 1 + M 2 ) = g(M 1 ) + g(M 2 ) ⇐⇒ f M1+M2 = f M1 + f M2 ⇐⇒ f M1+M2 (a) = (f M1 + f M2 )(a) ⇐⇒ f M1+M2 (a) = f M1 (a) + f M2 (a) ⇐⇒ (f M1+M2 (a)) ij = (f M1 (a) + f M2 (a)) ij ⇐⇒ (M 1 + M 2 ) ij (a) = (M 1 ) ij (a) + (M 2 ) ij (a)

(M 1 )(M 1 )

 11 ik × (M 2 ) kj )(a) = n k=1 ik (a) × (M 2 ) kj (a)(by assoc. of + and ×)A.4 Partiality

Note that 0 is also a possible type, corresponding to the absence of any dependency.

The implementation supports both coefficients from mwp and coefficients from {0, 1, 2} m → mwp, cf. e.g. a simple assignment assign expression example.

This is a variant of Lemma 5. While the latter lemma is stated for an algebra of square matrices, a similar result holds for rectangular matrices of a fixed size; the algebraic structure is no longer that of a semi-ring as rectangular matrices do not possess a proper multiplication, but the proof can be adapted to show the existence of an isomorphism of modules between the considered spaces.

Function calls that discard the output could also be dealt with easily, but are vacuous in our effect-free language

Note that this implies that if a loop belongs to a chunk, then the entire loop body belongs to the chunk.

To ease the presentation, the syntax considered here is restricted to functions with a single output value, so we actually have vectors in place of matrices here. But it is more natural to think in terms of matrices here, as the overall approach is valid in the more general setting in which functions may have several output values, and then the obtained objects are indeed matrices.

Here one has to consider equality up to some projections as the chuck F inserted in P may introduce new choices and use additional variables.

⋆ This material is based upon research supported by the Thomas Jefferson Fund of the Embassy of France in the United States and the FACE Foundation. Thomas Rubiano and Thomas Seiller are also supported by the Île-de-France region through the DIM RFSI project "CoHOp".

Identity element is 0 Let A = 0, then A ij = 0 for all i, j, and 0 is the identity element iff A ij + B ij = B ij for all i, j

it is associative and has 1 as identity. Associativity (A×B)×C = A×(B×C) iff ((A×B)×C) ij = (A×(B×C)) ij for all i, j.

(by identity of ×)

For simplicity, we will write M as M(S) = (M (S), 0, 1, +, ×).

A.3 Choices Semi-ring

This subsection explains and details how functions into semi-ring coefficients can be used to construct semi-rings, and the interplay between this construction and the matrix semi-ring from the previous subsection.