Véronique Benzaken

Sarah Cohen-Boulakia

Évelyne Contejean

Chantal Keller

Rébecca Zucchini

A Coq Formalization of Data Provenance

Keywords: CCS Concepts:, Software and its engineering → Formal software verification, Correctness, Software verification, • Theory of computation → Logic and verification, Type theory, Program verification, Program semantics, Data provenance extended relational algebra, Coq

In multiple domains, large amounts of data are daily generated and combined to be analyzed. The interpretation of these analyses requires to track back the provenance of combined data with respect to initial, raw data. The correctness of the provenance is crucial in many critical domains, such as medicine to prescribe treatments. In this article, we propose the first provenance-aware extended relational algebra formalized in a proof assistant (Coq), for a non trivial subset of database queries: queries containing aggregates, null values, and correlated sub-queries. The formalization is validated by an adequacy proof with respect to standard evaluation of queries. This development is a first step towards a posteriori certification of provenance for data manipulation, with strong guaranties.

INTRODUCTION

In the medical field, the choice of a treatment or protocol has been increasingly dependent on data analysis. For example, sequencing methods are a classic application of data analysis in cancerology: it is used to estimate the origin of a cancer, the mutations of a cell, the type of evolution of a cancer, as well as which treatment would be more suited for a particular cancer. These analyses need a large amount of data to be more efficient and fortunately, in the last decade, the development of new tools, in particular in sequencing, has led to a massive influx of raw data. However, it has become a challenge to perform complex analyses of the ever-growing amount of data without introducing bias. Moreover, the sequence of several processes communicating intermediate data as well as final data makes it difficult to understand the results of these analyses and their limitations, while also increasing the risk of error propagation. These questions are not specific to the medical domain, but a central point in every domain that requires large data analysis, such as IoT, space probes, . . . Such data analyses often involve many data management systems and are called scientific workflows.

To cope with these issues, the database community proposed a formalism called provenance. The role is to keep track of data all along their transformation from raw data to final analysis: why do we obtain some data in the result (whyprovenance) or not (why-not-provenance), where does it come from (where-provenance), etc. Most of these provenance information are computed by the means of annotations on data, as presented in the example below.

Publication rights licensed to ACM. ACM acknowledges that this contribution was authored or co-authored by an employee, contractor or affiliate of a national government. As such, the Government retains a nonexclusive, royalty-free right to publish or reproduce this article, or to allow others to do so, for Government purposes only.

Scientific workflows compute these annotations and rely on them to ensure provenance of data and what it entails, such as result understanding and reproducibility of analyses. Having strong guaranties on annotations is thus crucial in critical domains of application of scientific workflows, especially as it allows producing FAIR data [START_REF] Goble | FAIR computational workflows[END_REF]. This article is a step towards such a goal: we study and formalize in the Coq proof assistant such annotations in the case of the relational algebra, which is a central language for relational databases, the most common used database management systems (through the SQL language). This work thus provides certified provenance for relational databases, but also paves the way towards a framework to certify provenance in more complex workflows where many database systems interact.

Example

To explain the concept of provenance in the case of relational databases, we provide the example of the study of two medical treatments for breast cancer (e.g., hormonal treatment or chemotherapy).

Relational databases are made up of relations, two examples of which are on Table 1 and2. Let us first look at the four central columns (called attributes): for each patient designated by its Name, we indicate if s/he had a Remission of the cancer, after receiving Treatment A or B at some Stage of the illness. The elements of a relation (the lines of the table) are called tuples; here, we refer to them using the names of the first column, 𝑡 1 to 4 for the first relation and 𝑡 5 to 𝑡 7 for the second one. It enjoys a bag semantics: the same tuple can be present more than once. We will explain later the role of the last column.

These two relations form our raw data: they are observations gathered by two doctors (respectively in relations 𝑟 1 and 𝑟 2 ) treating these patients. Note that among the patients there are two who are both named Jones and two who are both named Smith. Now, we analyze these data: we want to know if treatment A is more efficient than treatment B in the early stage of this cancer. To this end, we first gather all the observations by computing the union of the two relations, whose result is presented in Table 3. After that we need to select only our data of interest so we keep the patients with a stage under 2 and who are in remission (Table 4). Then we do not need the remission and stage columns any more, so we can remove them by projecting on the other ones (Table 5). Finally, we obtain the number of patients that are in remission depending of the treatment, by grouping the patients depending on the treatment and aggregating the result by the number of tuples in each group: in Table 6, we have three patients that took treatment A (Smith twice and Johnson once), and only one that took treatment B (Miller).

In the syntax of relational algebra, this computation is written by the following query:

Γ 𝑡𝑟𝑒𝑎𝑡𝑚𝑒𝑛𝑡 |𝑐𝑜𝑢𝑛𝑡 (𝜋 𝑛𝑎𝑚𝑒,𝑡𝑟𝑒𝑎𝑡𝑚𝑒𝑛𝑡 (𝜎 𝑠 ⩽2∧𝑟𝑒𝑚=𝑌 (𝑟 1 ∪ 𝑟 2 )))
In this query, ∪ computes the union of the two initial relations, 𝜎 is the selection operator, 𝜋 the projection, and Γ performs both grouping then aggregation on the groups.

To keep track of provenance, the mechanism we study in this article is to annotate tuples, and evaluate queries on these annotations rather than the content of the tuples, in a process similar to abstract interpretation. On our example, it corresponds to the last column Annot of each table.

Starting from initial annotations on raw data, to each operator of the relational algebra corresponds an operation on the annotations: the union adds the annotations, the selection rules out some of them, projection collapses tuples and thus also adds annotations. Aggregates behave a bit differently: the result of the query does not depend only on values, but also on annotations (e.g. 1 ⊛ (𝑎 + 𝑑) ⊕ 1 ⊛ 𝑔). The intuition is that the result of an aggregate may depend on

A 3 1 ⊛ (𝑎 + 𝑑) ⊕ 1 ⊛ 𝑔 𝛿 (a+d+g) 𝑡 22 B 1 1 ⊛ 𝑒 𝛿 (e)
the weight of each aggregated tuple (see next paragraph). The resulting tuple is itself annotated by a combination of annotations (e.g. 𝛿 (a+d+g)). We will detail these aspects in Sec. 2.3.

As in abstract interpretation, the domain of the annotations has a direct influence on what we compute. The most simple domain is natural numbers, to represent throughout the query the number of occurrences of tuples in a table.

On our example, we thus start with each tuple being present once: 𝑎 = 𝑏 = 𝑐 = 𝑑 = 𝑒 = 𝑓 = 𝑔 = 1. Then, union adds the number of occurrences (bag semantics) 1 , and similarly when projection collapses tuples. Finally, when counting, we have to take these numbers of occurrences into account, which showcases the fact that the resulting value depends not only on initial values but also on annotations. The annotation of the resulting tuple can be either one or zero: the number of occurrences of the tuple is one if it is actually present, i.e. if at least one of the aggregated tuples has a non-zero annotation, and zero otherwise. This domain of natural numbers thus matches the traditional bag semantics of relational algebra, as we will show in our main theorem of the paper.

Other domains reflect other provenance properties: annotations generalize the bag semantics. We will detail some common domains in Sec. 2. An important property to notice is that by keeping the domain abstract, we compute equations, such that the variables appearing in an equation exactly reflects from which tuples of the initial data the generated tuple comes from. For instance, in Table 3, the annotation b+f reflects the fact that tuple 𝑡 9 comes from two tuples, whereas the other tuples come from only once. These universal annotations, based on polynomials as a domain, will be explained in Sec. 2 as well.

Contributions and Outline

This example illustrates the concept of provenance in relational databases. In this article, we provide strong guaranties for provenance in this setting, by formalizing it, in Coq, for an extension of relational algebra.

Our work is articulated as follows. Our first contribution is a formal and generic semantics for a provenance-aware relational algebra, extended with a subset of aggregates (Sec. 4). We validate our semantics by showing its adequacy with the standard relational algebra in the case where annotations are natural integers (Sec. 4.4). Finally, we propose to instantiate our generic semantics to offer an executable interpretor for provenance in relational algebra with several annotations used in practice (Sec. 5).

Our work builds upon the Datacert library (Sec. 3), which formalizes relational algebra in Coq. We will start with detailing the syntax and semantics of provenance as presented in the literature (Sec. 2). Figure 1 illustrates our contribution (black and red) and the building blocks we build upon (grey). The formal development as well as examples can be found at https://framagit.org/formaldata/provcert.

PROVENANCE IN DATABASES

Context

As presented in the example, a usual way to track how operators affect data when processing a query is to expand databases with annotations. It manifests by adding a new column (in our examples Annot) that associates an annotation to each tuple. To observe the impact of running a query on the annotations, we propose to focus on Table 3 that represents the union between relations of Tables 1 and2. It contains all the tuples that appear at least in one of the initial relations.

In the case of annotations representing occurrences of tuples, the annotation of a final tuple (for example 𝑡 8 ) is equal to the sum of occurrences (for 𝑡 8 , 𝑏 + 𝑓 ) of this tuple in the initial relations (disjoint union). For a tuple that appear only in one of the initial relations (like 𝑡 1 ), the annotation of the final tuple is 𝑎 = 𝑎 + 0: tuples that do not appear in one of the relations can be considered as having zero as an annotation. Thus, we notice that the union of two tuples requires the an operation "+" and a zero on annotations.

More generally, for any domain of annotations, the union operator will combine annotations by the mean of + and zero of some algebraic structure. As the other tables of the example show, to each operator of the relational algebra is associated an operation on annotations. To reflect the associativity, commutativity and distributivity of the operators of databases, the operations on the annotations need to verify those properties. These characteristics suggest that annotations are at least in a commutative monoid. In practice, to capture the richness of relational algebra, the annotations are put in a unifying algebraic structure: the commutative semirings [START_REF] Todd J Green | Provenance semirings[END_REF].

We have seen on Table 6 that aggregates combine values with annotations. This combination requires two operations (that depend on the aggregate): an addition on values ⊕, and a tensor product between values and annotations ⊛. Again, we can remain abstract: these operations are fully captured by equipping the domain of values with a semimodule over the semiring of annotations. The annotations themselves are combinations of annotations with some function 𝛿, that depends on the semiring of annotations. To sum up, to treat some aggregate, one has to extend the semiring of annotations 𝐾 with a 𝛿 function computing one element of 𝐾 from a set of elements of 𝐾, and to equip the values with a 𝐾-semimodule for each considered aggregate.

A relation is usually represented by a bag of tuples. A more abstract way to represent a bag is as a function from tuples to natural integers (number of occurrences). A K-relation [START_REF] Todd J Green | Provenance semirings[END_REF] generalizes this idea: a function from tuples to some commutative semiring 𝐾, representing the domain of provenance annotations.

The Extended Relational Algebra

We now present the syntax of our database language: the positive relational algebra, extended with a restricted subset of aggregates.

Definition 1 (Syntax of queries).

𝑞 ′ ::= 𝑟 | 𝑞 ′ ∪ 𝑞 ′ | 𝜎 𝑓 (𝑞 ′ ) | 𝜋 𝑠 (𝑞 ′ ) | 𝜖 <> | 𝑞 ′ ⊲⊳ 𝑞 ′ 𝑞 := 𝑞 ′ | Γ 𝑔𝑏 |𝑎 (𝑞 ′ )
First, we present quickly the traditional semantics of the operators of the algebra (without annotations).

The first four operators of the relational algebra 𝑞 ′ were used in the example of the introduction. The first one refers to a predefined relation 𝑟 (such as 𝑟 1 and 𝑟 2 in the example). The operator ∪ represents the disjoint union. The operator 𝜎 performs selection: only the tuples satisfying a first-order logical formula 𝑓 are kept. The operator 𝜋 corresponds to the projection on a subset 𝑠 of the attributes of 𝑞 ′ : we keep only the columns whose names are in 𝑠.

The next operator is 𝜖 <> : it is an attributeless relation only containing the empty tuple2 . Finally, the ⊲⊳ operator represents the natural join. An example of this operator is given in Tables 7 and8 (we do not consider the last column at this stage): it combines the tuples of two relations when they are equal on their common attributes. We work on an extension of this relational algebra 𝑞 with the top-level aggregation operator Γ3 . It first groups the tuples of 𝑞 ′ on the expressions 𝑔𝑏, then applies the aggregate function 𝑎 on each group. An example was given in Table 6: the operator first groups the tuples in two different groups depending on the treatment (treatment A or B), then it applies the 𝑐𝑜𝑢𝑛𝑡 aggregate on each group, which counts how many tuples are present in each group. Other common aggregate functions are 𝑠𝑢𝑚(𝑥) (resp. 𝑎𝑣𝑔(𝑥)), summing (resp. computing the average of) the values of an integer attribute 𝑥, or 𝑚𝑎𝑥 (𝑥), computing the maximum value of an integer attribute 𝑥.

Annotations

We now present the semantics of our algebra with annotations in a semiring (𝐾, 0, 1, +, * ). We first explain the main intuitions, before giving the mathematical definitions.

As 𝑟 is a predefined relation, the annotations of each tuple are also predefined. The semantics of the empty tuple 𝜖 <> is very straightforward: it is a 𝐾-relation that associates 1 to the empty tuple and 0 to the others. As we have seen with the example, the union of two queries is the 𝐾-relation that sums the annotations of each initial 𝐾-relation.

We now focus on the case of the selection by a formula 𝑓 . In the example (Table 4), the selection formula corresponds to "the stage has to be under 2 and the patient is on remission". The tuples that satisfy this formula are kept as well as their annotation (like the tuples 𝑡 8 , 𝑡 11 , 𝑡 12 and 𝑡 13 ). For the other tuples (like 𝑡 9 and 𝑡 10 ), they do not appear in the result: their annotations are then 0.

Concerning the case of the projection, we can look at Table 5 that represents the projection on the attributes Name and Tre. We particularly focus on the tuple 𝑡 18 : it is the result of the projection of 𝑡 14 and 𝑡 15 . So the annotation of 𝑡 18 is the addition of the annotations of tuples whose projection is equal to 𝑡 18 . More generally, the 𝐾-relation for projection is the function from a tuple 𝑡 to the sum of annotations of the projected tuple equal to 𝑡.

Again, natural join is illustrated by Table 8. Since it combines tuples, the result is the 𝐾-relation that multiplies the annotations of each initial 𝐾-relation.

To picture the case of aggregates, we focus on the same tuple 𝑡 21 as before. In the case of natural numbers, the annotation of this tuple depends whether it appears or not in the result: it is 0 if 𝑎, 𝑑 and 𝑔 are all equal to 0, and

(0) = 0.
Associating annotations in 𝐾 to tuples of the result of operators is called a K-algebra [START_REF] Todd J Green | Provenance semirings[END_REF]. It is mathematically defined as follows.

Definition 2 (Semantics of the 𝐾-algebra).

• ⟦𝑟 ⟧ = 𝑡 ↦ → annot (r, t)
where 𝑎𝑛𝑛𝑜𝑡 is the function that associates an annotation to each tuple 𝑡 of the relation 𝑟

• ⟦𝜖 <> ⟧ = 𝑡 ↦ →        1 if 𝑡 =<> 0 otherwise • ⟦𝑞 ′ 1 ∪ 𝑞 ′ 2 ⟧ = 𝑡 ↦ → ⟦𝑞 ′ 1 ⟧(𝑡) + ⟦𝑞 ′ 2 ⟧(𝑡) • ⟦𝜎 𝑓 (𝑞 ′ )⟧ = 𝑡 ↦ →        ⟦𝑞 ′ ⟧(𝑡) if 𝑒𝑣𝑎𝑙 (𝑓 , 𝑡) = ⊤
0 otherwise where 𝑒𝑣𝑎𝑙 evaluates the logical formula 𝑓 on the tuple 𝑡

• ⟦𝜋 𝑠 (𝑞 ′ )⟧ = 𝑡 ↦ → 𝑡 ′ s.t.𝑝𝑟𝑜 𝑗 𝑠 (𝑡 )=𝑝𝑟𝑜 𝑗 𝑠 (𝑡 ′ )∧⟦𝑞 ′ ⟧(𝑡 ′ )≠0 ⟦𝑞 ′ ⟧(𝑡 ′ )
where 𝑝𝑟𝑜 𝑗 𝑠 (𝑡) is the projection on the set of attributes 𝑠 of the tuple 𝑡

• ⟦𝑞 ′ 1 ⊲⊳ 𝑞 ′ 2 ⟧ = 𝑡 ↦ → ⟦𝑞 ′ 1 ⟧(𝑡 1 ) * ⟦𝑞 ′ 2 ⟧(𝑡 2 )
where 𝑡 𝑖 corresponds to the projections of 𝑡 on the set of attributes associated with 𝑞 𝑖

• ⟦Γ 𝑔𝑏 |𝑎 (𝑞 ′ )⟧ = 𝑡 ↦ →              𝛿 𝐾 ( 𝑖 𝑎 𝑖 ) if 𝑡 = (𝑣 1 ⊛ 𝑎 𝑎 1 ) ⊕ 𝑎 . . . ⊕ 𝑎 (𝑣 𝑛 ⊛ 𝑎 𝑎 𝑛 )
0 otherwise where 𝑣 1 , . . . , 𝑣 𝑛 are the values appearing in the tuples of the group 𝑔𝑏 over the query 𝑞 ′ , and 𝑎 1 , . . . , 𝑎 𝑛 are their annotations.

For this definition to be valid, the sum for the projection operator 𝜋 must be finite. It is indeed the case, since annotations must be 0 for all tuples except a finite number of them (we require this property for the base case of a predefined relation, and it is propagated by the definitions). It reflects the standard finiteness property of the relational model.

Domains of Annotations

We have already seen that using the set of natural numbers as the semiring 𝐾 leads to annotations computing the number of occurrences of tuples, that is to say the bag semantics of SQL. Other commonly used domains are the following.

• The ring of Booleans (B, ⊥, ⊤, ∨, ∧) simply indicates the presence or absence of a tuple (allowing one to recover the set semantics of SQL).

• It can be abstracted by the semiring of Boolean functions which compute not only one possible set of tuples, but all the possible sets (called possibles worlds) and can be useful to efficiently represent different instances of some database [START_REF] Todd J Green | Provenance semirings[END_REF].

• The security semiring (S, 0 S , 1 S , min, max) where S is an ordered set containing security levels (such as 0 S being "not secure", then "confidential", "secret", and 1 S being "top secret") computes the security level of the resulting data.

• The semiring of tropical integers (N ∞ , 0, 1, +, *) computes the (possibly infinite) cost to obtain some data.

As there exists numerous domains for annotations, changing the domain would require to compute again the provenance for the same set of queries and databases, which is time-and energy-consuming. In the case without aggregates [START_REF] Todd J Green | Provenance semirings[END_REF], people proposed a framework to encompass all the possible semirings: the positive algebra provenance semiring, consisting of polynomials with coefficients in N.

Definition 3 (Positive algebra provenance semiring). Let 𝑋 be the set of tuple ids of a database instance 𝐼 . The positive algebra provenance semiring is the semiring (N[𝑋 ], 0, 1, +, .) of polynomials with interderminates from X and coefficients from N with + and . operators.

As explained at the end of Sec. 1.1, this semiring computes generalized annotations for a query. First, to obtain the annotations in the desired semiring, one only has to evaluate the resulting polynomial by replacing monomials with initial annotations, and substituting the addition and multiplication of polynomials by those of the semiring. Second, more abstractly, the monomials appearing in the resulting annotation of a tuple precisely indicate from which original tuples it comes from.

PRESENTATION OF THE DATACERT LIBRARY

We now present the main building block we base our formalization on.

The Datacert library [START_REF] Benzaken | A coq mechanised formal semantics for realistic SQL queries: formally reconciling SQL and bag relational algebra[END_REF] provides the most complete mechanized semantics for SQL queries with aggregates, NULL values and correlated queries, and formally relates them to an extension of relational algebra. In this work, we extend the relational algebra part with provenance. We also use Datacert as a reference to validate our semantics based on generic 𝐾-relations: when 𝐾 is instantiated with natural numbers, we can prove that the two semantics coincide (Sec. 4.4). In addition, this semantics is executable (both in Coq and after extraction), which allows us to actually compute provenance.

The Datacert formalization is divided into two layers:

• an abstract layer provides the syntax and semantics for SQL and algebra queries, with an abstract data model, abstract types for attributes, values, tuples, predicate symbols, . . . making it easily extensible and abstracting away implementation details (Sec. 3.1); • a proof of concept instantiates these types with standard values, to provide the executable semantics (Sec. 3.2).

Syntax and Semantics of Extended Relational Algebra

As our work is restricted to a subset of the queries, we present only the associated fragment of the syntax proposed in Datacert.

The query syntax is defined by a recursive type query: We now detail the different types used to define query. The first type is relname, that is an abstract type for relation names. As explained above, the proof of concept (Sec. 3.2) instantiates this type by the type string. The type formula is a recursive type for SQL first order logical formulas, that we do no detail here (we refer to [START_REF] Benzaken | A coq mechanised formal semantics for realistic SQL queries: formally reconciling SQL and bag relational algebra[END_REF]). The type select - list occurs in projections and aggregates. It consists in a list of couples of type aggterm * attribute, where aggterm represents SQL terms with function and/or aggregate symbols (such as a + b or sum(x)) and attribute is an attribute name given to the term (standing for the as construct). For instance, the projection 𝜋 𝑛𝑎𝑚𝑒,𝑡𝑟𝑒𝑎𝑡𝑚𝑒𝑛𝑡 (𝑞 1 ) in the example corresponds to Q -Pi [(name,name);(treatment,treatment)] q 1 , and the aggregate

Γ 𝑡𝑟𝑒𝑎𝑡𝑚𝑒𝑛𝑡 |𝑐𝑜𝑢𝑛𝑡 (𝑞 2 ) corresponds to Q -Gamma [(count(*), count)] treatment q 2 .
This definition matches our grammar in Definition 1, except that it does not enforce the aggregate to be the last applied operation, and to have only one aggregate. To do so, we have defined a predicate well -formed that takes a Boolean and a query and checks that this property is verified. The Boolean argument is a flag to indicate whether or not we are in the first call of the function.

The semantics is defined by a recursive function which associates a finite bag of tuples to each query. It is based upon the library of finite bags called Fbag, which is part of an extension of the Coccinelle library [START_REF] Contejean | Coccinelle, a Coq library for rewriting[END_REF].

Fixpoint eval -query env q : bagT :

= match q with | Q -Table r ⇒ instance r | Q -Union q1 q2 ⇒ if sort q1 =? sort q2
then Fbag.union (eval -query env q1) (eval -query env q2) else Fbag.empty | Q -Sigma f q ⇒ Fbag.filter (fun t ⇒ is -true (eval -sql -formula (env -t env t) f)) (eval -query env q)

| Q -Pi s q ⇒ Fbag.map (fun t ⇒ projection (env -t env t) s) (eval -query env q) | Q -Empty -Tuple ⇒ Fbag.singleton empty -tuple | Q -NaturalJoin q1 q2 ⇒ natural -join -bag (eval -query env q1) (eval -query env q2)

| Q -Gamma s lf f q ⇒ Fbag.mk -bag (map (fun l ⇒ projection (env -g env (Group -By lf) l) s) (make -groups env (eval -query env q) (Group -By lf)))

end.

The function instance associates to a relation name r its content. The function sort gives the sort of a query, that is to say the list of attribute names of the result of the query. In the case of the union, we first check if the sorts are the same for the sub-queries then if it is the case, we return the union of the bags (with possible duplicates) and if it is not, we return the empty bag. The function Fbag.filter allows to keep only the elements of a bag which satisfy some predicate. Here in the case of selection, our predicate evaluates a logical formula 𝑓 on a tuple 𝑡 thanks to the function eval -q -formula.

The function projection projects each tuple of its sub-query (by mapping, with Fbag.map) on the select -list given as a first argument. The same idea applies to Gamma, not on tuples, but on groups of tuples computed by the function makegroups. Since it returns a list, it is transformed back into a bag by the function Fbag.mk -bag.

Since function, predicate and aggregate symbols are abstract at this stage, the semantics depends on axiomatized interpretation for them, respectively called interp -symbol, interp -predicate and interp -aggregate, that we will detail in the next section. We precise that predicates are interpreted in a three-valued logic, as standard in SQL with NULL values.

Throughout the evaluation, we need to keep track of groups of tuples, of the attributes associated to groups, and of the grouping expressions that are treated by the projection function, that will be used when evaluating sub-queries. This is the role of the environment env, which is very crucial to correctly handle correlated queries in SQL [START_REF] Benzaken | A coq mechanised formal semantics for realistic SQL queries: formally reconciling SQL and bag relational algebra[END_REF]. For a matter of clarity, we do not detail it here since it does not crucially impact our formalization. In addition to the wellformed predicate presented above to state that a query belongs to the fragment of aggregates we consider, [START_REF] Benzaken | A coq mechanised formal semantics for realistic SQL queries: formally reconciling SQL and bag relational algebra[END_REF] defines a predicate called env -well -formed stating that a query is well-defined in a given environment.

Instantiation

In this subsection, we present the main instantiation proposed in Datacert for the abstract syntax and semantics presented above.

Values can be either Booleans, integers and strings, with the NULL value represented by an option type. An attribute is represented by its name and its type. Given that, tuples are represented by a list of pairs of an attribute and a value.

The proof of concept also instantiates the function, predicate and aggregate symbols with the most standard of SQL: "+", "-" (unary and binary) and "*" for functions; "count", "avg", "sum" and "max" for aggregates; "=", "<=", . . . for predicates. The axiomatized functions interp -symbol, interp -predicate and interp -aggregate of the abstract layer are instantiated by interpreting the symbol "+" as an addition on integers, and so on.

FORMALIZATION: 𝐾-ALGEBRA AND ADEQUACY WITH RELATIONAL ALGEBRA

In this section, we present the first part of our contribution with the formalization in Coq of the semantics of a provenance-aware relational algebra, extended with top-level aggregates.

Semirings

To keep the spirit of Datacert, we also base the formalization of our mathematical structures on the Coccinelle [START_REF] Contejean | Coccinelle, a Coq library for rewriting[END_REF] library. This library uses Coq Records to represent objects of the structure and axioms on these objects.

This part of the formalization is rather standard, so we do not detail it here. We report on different possible implementations in the related works section (Sec. 6).

| Q -Union q1 q2 ⇒ let kr1 := eval -query -prov env q1 in let kr2 := eval -query -prov env q2 in if sort -krel kr1 =? sort -krel kr2 then {| f := fun t ⇒ plus (f kr1 t) (f kr2 t); support := Fset.union (support kr1) (support kr2); sort -krel := sort -krel kr1 |} else Krel -empty | Q -Sigma form q ⇒ let kr := eval -query -prov env q in {| f := fun t ⇒ mul (f kr t) (if is -true (eval -formula -prov (env -pt env t) form) then 1 else 0); support := support kr; sort -krel := sort -krel kr |} | Q -Pi s q ⇒ let kr := eval -query -prov env q in {| f := fun t ⇒ foldleft (fun x y ⇒ plus (f kr y) x) (filter (fun t' ⇒ eq? t (projection -prov (env -pt env t') s)) (Fset.elements (support kr))) 0; support := Fset.map (fun t ⇒ projection -prov (env -pt env t) s) (support kr); sort | Q -Gamma s lf f q ⇒ Krel -gamma s env (eval -query -prov env q) lf end.

The function instance -prov has the same role as instance -rel except that it returns the associated 𝐾-relation instead of a bag of tuples. The Q -Union case directly matches the definition. For the selection, we keep the selected tuples by multiplying their annotations with 1, and 0 for the others; note that the support is not filtered and is thus a superset of the tuples. As we explained, for the projection, we have to iterate over the projections of non-zero tuples of the support, as in the mathematical definition. The function all -attr returns the attributes of the projected fields in 𝑠. The case of the empty tuple is straightforward. For natural join, we used an auxiliary function natural -join -set, that computes the natural join on sets of tuples (similar to natural -join -bag for bags). In this case, the resulting sort is the union set of the sort of the initial queries.

The more involved definition is for the aggregate operator Q -Gamma. Remember that s is the list of aggregates we actually compute (Sec. 3.1), and that we only handle the case were there is only one such aggregate (well -formed predicate). For other cases, since they will be ruled out by the well -formed hypothesis, we can return any 𝐾-relation. We do not detail the definition of make -proj -grb, but it computes the projection of the support of the 𝐾-relation kr in a similar way as for the Q -Pi operator. The main difference is that it also groups the results by combining values and annotations as explained in Definition 2. Since this combination depends on aggregates, it is the role of the abstract interpaggregateprov function to perform this combination. This level of abstraction hides away the semimodule structure.

The other function appearing in this definition is the following: This function computes the annotation as presented in Definition 2, relying on a delta function of type:

delta : list K → K
Since this function depends on the semiring, which is abstract in this layer, we have to make this function abstract as well.

As for the semantics of the relational algebra presented in Sec. 3.1, we have an environment to correctly handle correlated queries, which is a simple extension of the environment of [START_REF] Benzaken | A coq mechanised formal semantics for realistic SQL queries: formally reconciling SQL and bag relational algebra[END_REF] to 𝐾-relations. We do not detail it in the article.

Adequacy Theorem

In this section we prove that our formalization of 𝐾-algebras faithfully extends the relational algebra: it exactly matches the N-algebra. As presented in Section 2.4, other semirings for 𝐾 thus give other provenance algebras.

Specializing to the semiring N fully determines the function delta: it returns 1 as soon as there is a non-zero annotation, and 0 otherwise [START_REF] Amsterdamer | Provenance for aggregate queries[END_REF]. However, we took great care of keeping abstract all the other datatypes and functions that were axiomatized, in order to stay generic and ease the proof (see Sec. 4.5). It thus requires to assume some properties to relate them with their counterpart in the relational algebra. The first affected function is instance -prov: we need to know that the number of occurrences and the sorts coincide for each relation.

Hypothesis instance -prov -nb -occ : ∀ r t, (instance -prov r).(f) t = Fbag.nb -occ t (instance -rel r).

Hypothesis instance -support : ∀ r, sort -krel (instance -prov r) = basesort r.

In this definition, Fbag.nb -occ computes the number of occurrences of a tuple in a bag, and basesort returns the sort of a relation.

The second impacted functions are interp -symbol -prov, interp -predicate -prov and interp -aggregate -prov. We focus on the interp -aggregate -prov function. We recall that, in the relational algebra, the function To relate both functions in the case of the semiring N, we suppose that they coincide on lists in which all annotations are equal to one:

Hypothesis interp -aggregate -prov -prop1 : ∀ a l, List.∀ b (fun x ⇒ snd x =? 1%N) l = true → interp -aggregate -prov a l = interp -aggregate a (fst (List.split l)).

where List.split splits a list of pairs into a pair of lists. Moreover, as interp -aggregate must be agnostic of the order of the elements in the list, a second property (that we omit here) of interp -aggregate -prov is that it must return the same result on two lists whose sum of annotations for each tuple is equal.

The last step is to make the two environments coincide. To do so, we can easily transform a list of tuples into a 𝐾-relation: With all these hypotheses, we proved at the abstract layer that the two semantics coincide :

Theorem K -relations -extend -relational -algebra :

∀ env (b:bool) (q:query), wellformed b q = true → envwellformed env q = true → ∀ (t:tuple), f (eval -query -prov -N (create -env env) q) t = Fbag.nb -occ t (eval -query -rel env q).

Discussion

While apparently straightforward once given, establishing this formalization was far from being trivial. One crucial aspect was to formulate simple but sufficient invariants on the 𝐾-algebra, as well as the properties on abstract datatypes presented above.

For instance, as shown in its type, the function interp -aggregate manipulates lists of values, and not bags. It implies that the same value can appear at multiple places in the list. On the 𝐾-relation side, we have functions, that immediately returns the number of occurrences. To smoothly relate the two, it was a long process by trial and error to end up with the type for interp -aggregate -prov that we just presented, as well as the two properties.

More generally, the mathematical definition of 𝐾-algebras involve non-trivial constructions, such as finite sums or the possibility to compute groups. We wanted to reflect these constructions in an executable way (see next section), which implies to manipulate actual data-structures, which sometimes obfuscates the proof.

On this aspect, we were very careful to preserve the high degree of abstraction inherited from Datacert. The direct impact is to have a generic formalization that can be instantiated after the fact in various ways. More interestingly, it results in a high-level formalization that is easier to carry out, since the various concerns are split into different parts. A striking example is that presentations of provenance for aggregates on paper insist a lot on the algebraic structure of semimodules required to compute results of aggregates [START_REF] Amsterdamer | Provenance for aggregate queries[END_REF]. Our degree of abstraction on values made it possible to hide this technicality during the abstract part of the formalization. The instantiation of interp -aggregate -prov actually provides the operations of the semimodules, but implicitly.

INSTANTIATION AND PROOF OF CONCEPT

Instantiation

The second part of our contribution is to provide instantiations of all the abstract objects that were axiomatized in the first part of the formalization. One of our main goal is to obtain an executable semantics, with reasonable performance after extraction. It allows one to compute provenance for SQL queries on small databases, and thus to actually test our implementation against other implementations, which could be really useful to detect bugs (which are usually unrelated to the size of the database).

First, we have implemented most of the usual semirings used in provenance presented in Sec. 2.4: Booleans and Boolean functions, natural and tropical integers, as well as polynomials. We insist in particular on two of these formalizations.

• Our formalization of tropical integers actually generalizes the definition of tropical integers to any totally ordered monoid. We have formally proved that the structure of a totally ordered monoid with compatibility of addition with respect to order is enough to be equipped with a tropical structure. That would allow us to reason in terms of linear cost to obtain data (tropical integers), but also to generalize it to more complex kinds of costs. • Our formalization of polynomials refreshes the existing implementation of the Coccinelle [START_REF] Contejean | Coccinelle, a Coq library for rewriting[END_REF] library. It is based on a new library of finite maps (which can be used in other contexts), to represent polynomials as maps from monomials to coefficients. This presentation of polynomials is very useful in our setting since it is both rather complete and executable.

Second, we have extended the Datacert proof of concept (Sec. 3.2) with our new functions, such as interp -symbol -prov, interp -predicate -prov and interp -aggregate -prov. It requires not only to implement them, but also to prove the properties that we have axiomatized in Sec. 4.4. In addition to providing a proof of concept, this realization thus validates the axiomatization.

Usability of the Implementation

To make this implementation easily usable, e.g. for quick testing, we implemented a Coq plugin that provides new Coq vernacular commands to parse SQL queries directly in Coq. For instance, the example of the introduction can be written as: The first four commands create Coq terms t0, t1, i0 and i1 to populate the database (... must be replaced by the actual values). The last command creates the Coq term q containing the SQL select query. Such examples can be found in the source code (see Sec. 1.2), in the file data/proof_of_concept/Example.v.

RELATED WORKS

One of the first formalizations of a data-oriented application is the implementation, in Agda, of a relational algebra, proposed in 2003 by [START_REF] Gonzalia | Towards a formalisation of relational database theory in constructive type theory[END_REF][START_REF] Gonzalia | Relations in Dependent Type Theory[END_REF]. The first complete formalization of the relational model was proposed in [START_REF] Véronique Benzaken | A Coq Formalization of the Relational Data Model[END_REF], including a data model, the complete algebra, the semi-decision procedure chase and integrity constraints.

On the language side, the first verification of a relational database management system, in Coq, was presented in [START_REF] Malecha | Toward a verified relational database management system[END_REF].

More complete SQL semantics were proposed in [START_REF] Auerbach | Handling environments in a nested relational algebra with combinators and an implementation in a verified query compiler[END_REF][START_REF] Benzaken | A coq mechanised formal semantics for realistic SQL queries: formally reconciling SQL and bag relational algebra[END_REF]. We base on the second work which includes non trivial features of SQL such as set and bag semantics, null values, and correlated queries. A formalization of a query engine for SQL was presented in [START_REF] Véronique Benzaken | A coq formalisation of sql's execution engines[END_REF].

To our knowledge, this submission is the first work on data provenance formalized in a proof assistant. We base our work on a generalized framework for provenance for the relational algebra [START_REF] Todd J Green | Provenance semirings[END_REF] and for aggregate functions [START_REF] Amsterdamer | Provenance for aggregate queries[END_REF]. The closest work [START_REF] Chu | HoTTSQL: Proving query rewrites with univalent SQL semantics[END_REF] proposes a tool to decide the equivalence of two SQL queries based on a semantic called HottSQL, inspired by K-relations. However, their modeling exploits possibly infinite K-relations, which is not compatible with the SQL data model. Another limitation is that their semantics is not executable (not even after extraction, due to the infinite model), preventing from testing, comparing against other implementations, etc.

Provenance-aware query languages and database management systems are emerging, such as ProvSQL [START_REF] Senellart | Provsql: Provenance and probability management in postgresql[END_REF], an extension of PostgreSQL, or Links, a language-integrated query mechanism in Haskell [START_REF] Fehrenbach | Language-integrated provenance by trace analysis[END_REF][START_REF] Stolarek | Language-integrated provenance in haskell[END_REF]. One of our mid-term objectives is to give strong guaranties to such systems by validating their trace analyses by a certified implementation.

Many formalizations of algebraic structures have been proposed in Coq, two of the most elaborate being Mathematical Components [START_REF]The Mathematical Components team[END_REF] and Math Classes4 . Our work builds upon the Coccinelle library [START_REF] Contejean | Coccinelle, a Coq library for rewriting[END_REF] for two reasons: it is based on [START_REF] Benzaken | A coq mechanised formal semantics for realistic SQL queries: formally reconciling SQL and bag relational algebra[END_REF] that already uses this library, and it is executable both in Coq and after extraction. Execution in Coq is useful for quick testing, in particular thanks to our plugin (see Sec. 5.2). To get more proof automation and to rely on a mainstream library, we consider switching to one of the two libraries listed above. For executability with the library Mathematical Components, one may use the refinement mechanism proposed in [START_REF] Cohen | Refinements for free! In Georges[END_REF].

CONCLUSIONS AND PERSPECTIVES

We have presented a central basic block for the formalization of data provenance. Starting from existing formalizations of the extended relational algebra and algebraic mathematical structures, we have developed the provenance model based on K-relations for a non trivial algebra including aggregates, null values, and correlated queries. We have validated the implementation by proving the fundamental adequacy theorem with the standard relational algebra. Our Coq formalization offers a high level of abstraction, is parametric in the provenance semiring, but also comes with a proof of concept showcasing actual executions. Short-term objectives include direct extensions of the language, such as nested aggregates. Pragmatically, this work can be linked with the formalization of SQL and its certified translation into the extended relational algebra [START_REF] Benzaken | A coq mechanised formal semantics for realistic SQL queries: formally reconciling SQL and bag relational algebra[END_REF] to propose a query language with annotations correctly and completely translated into the algebra. Another objective is to test our implementation against existing implementations of provenance such as the module ProvSQL of PostgreSQL [START_REF] Senellart | Provsql : Gestion de provenance et de probabilités dans postgresql[END_REF].

Our main long-term perspective is to certify provenance in data analyses as performed in networks, bio-informatics, etc. Our case study are scientific workflows which, from input data, execute a sequence of instructions (with loops) to generate new data to be analyzed. We plan to instrument such workflows to produce execution traces to be checked in a certified tool to guaranty reproducibility [START_REF] Cohen Boulakia | Scientific workflows for computational reproducibility in the life sciences: Status, challenges and opportunities[END_REF][START_REF] Goble | FAIR computational workflows[END_REF]: this a posteriori certification process will rely on a skeptical approach [START_REF] Harrison | A Sceptic's Approach to Combining HOL and Maple[END_REF], and thus be independent from tools appearing in workflows, making it practicable and maintainable.

The main challenge will consist in the scalability of the tool to be able to validate analyses on large amounts of data.

  Fig. 1. Contributions

  Inductive query : Type := | Q -Table : relname → query ( * Relation identified by a name * ) | Q -Union : query → query → query ( * Union * ) | Q -Sigma : formula → query → query ( * Selection * ) | Q -Pi : select -list → query → query ( * Projection * ) | Q -Empty -Tuple : query ( * Relation containing the empty tuple * ) | Q -NaturalJoin : query → query → query ( * Natural join * ) | Q -Gamma : select -list → list aggterm → query → query. ( * Aggregates * )

  -krel := all -attr s |} | Q -Empty -Tuple ⇒ {| f := fun t ⇒ if t =? empty -tuple then 1 else 0; support := Feset.singleton empty -tuple; sort -krel := Fset.empty |} | Q -NaturalJoin q1 q2 ⇒ let kr1 := eval -query -prov env q1 in let kr2 := eval -query -prov env q2 in let sort := Fset.union (sort -krel kr1) (sort -krel kr2) in {| f := fun t ⇒ if labels t =? sort then mul (f kr1 t) (f kr2 t) else 0; support := natural -join -set (support kr1) (support kr2); sort -krel := sort |}

Definition

  Krel -gamma s env kr lf := match s with | agg::nil ⇒ let lproj := make -proj -grb env lf (agg::nil) kr in let supp := Fset.mk -set (map fst lproj) in let sort := all -attr s in {| f := f -gamma lproj; support := supp; sort -krel := sort |} | -⇒ Krel -empty end.

Fixpoint

  f -gamma l := match l with | nil ⇒ fun t ⇒ 0 | (t0,kr) :: tl ⇒ let f1 := f -gamma tl in fun t ⇒ if t0 =? t then (delta (map (f kr) (support kr))) + (f1 t) else f1 t end.

Fixpoint

  delta (l : list N) : N := match l with | nil ⇒ 0%N | hd :: tl ⇒ if hd =? 0%N then delta tl else 1%N end.

Fixpoint

  create -krel (l : list tuple) s := match l with | nil ⇒ {| f := fun t ⇒ 0; support := Fset.empty ; sort -krel := s |} | hd :: tl ⇒ let kr := create -krel tl s in {| f := fun x ⇒ if x =? hd then (f kr x) + 1 else f kr x; support := Fset.add hd (support kr); sort -krel := s |} end.

Table 1 .

 1 relation 𝑟 1

	Name Rem Tre S Annot
	𝑡 1 Smith	Y	A	1	a
	𝑡 2 Jones	N	B	2	b
	𝑡 3 Garcia	N	A	4	c
	𝑡 4 Smith	Y	A	2	d

Table 2 .

 2 relation 𝑟 2

		Name Rem Tre S Annot
	𝑡 5	Miller	Y	B	2	e
	𝑡 6	Jones	N	B	2	f
	𝑡 7 Johnson	Y	A	2	g

Table 3 .

 3 union of relations 𝑟 1 and 𝑟 2

		Name Rem Tre S Annot
	𝑡 8	Smith	Y	A	1	a
	𝑡 9	Jones	N	B	2	b + f
	𝑡 10	Garcia	N	A	4	c
	𝑡 11	Smith	Y	A	2	d
	𝑡 12	Miller	Y	B	2	e
	𝑡 13 Johnson	Y	A	2	g

Table 4 .

 4 selection of stage ⩽ 2 and remission = Yes

		Name Rem Tre S Annot
	𝑡 14	Smith	Y	A	1	a
	𝑡 15	Smith	Y	A	2	d
	𝑡 16	Miller	Y	B	2	e
	𝑡 17 Johnson	Y	A	2	g

Table 5 .

 5 projection on name and treatment

		Name Tre Annot
	𝑡 18	Smith	A	a + d
	𝑡 19	Miller	B	e
	𝑡 20 Johnson	A	g

Table 6 .

 6 count, grouping by treatment

	Tre count	acount	Annot
	𝑡 21

Table 7 .

 7 relation 𝑟 3

		Name	City	Annot
	𝑠 1	Smith Cambridge	h
	𝑠 2	Jones	New York	i
	𝑠 3 Bridges	Roma	j
	𝑠 4 Garcia	Portland	k

Table 8 .

 8 natural join of 𝑟 1 and 𝑟 3

	Name Rem Tre S	City	Annot
	𝑠 5 Smith	Y	A	1 Cambridge	a * h
	𝑠 6 Jones	N	B	2 New York	b * i
	𝑠 7 Garcia	N	A	4	Portland	c * k
	𝑠 8 Smith	Y	A	2 Cambridge	d * h

  1 otherwise. The expression 𝛿 (𝑎 + 𝑑 + 𝑔) exactly computes it. More generally, the resulting tuple associated to a group 𝑋 has for annotation 𝛿 𝐾 (𝑎 1 + .. + 𝑎 𝑛 ) where the 𝑎 𝑖 s are the annotations of the initial tuples of 𝑋 . 𝛿 𝐾 depends on the semiring 𝐾; the main property it must verify is 𝛿 𝐾

  interpaggregate : aggregate → list value → value interprets the standard SQL aggregates by aggregating values into a single value. To generalize it to the 𝐾-algebra, it operates over annotated values: as presented in Table6of the example of Sec. 1.1, the result of the query (and not only its annotation) depends on annotations of the initial tuples. Its type is thus: interpaggregateprov : aggregate → list (value * K) → value

It corresponds to union all in SQL.

It is mainly used as a neutral element for the ⊲⊳ operator.

Compared to SQL, we restrict the use of the aggregate to be the last operator applied, and the aggregate function can only be applied to one attribute. Moreover, we do not consider having. We leave these generalizations for future work.

The Math Classes library can be found at https://github.com/coq-community/math-classes.

ACKNOWLEDGEMENTS

We would like to thank the reviewers for their time and for their comments.

𝐾-relations

As presented in Definition 2, the main idea is to replace the representation of the result of queries as bags of tuples by functions from tuples to a semiring 𝐾.

With only a function from tuples to 𝐾, we would lose crucial informations compared to bags. First, we would not know what is the sort of the relation. In the case of bags, we have access to the sort by picking a tuple in the bag (if it exists) and checking its sort, which is not the case for functions. Second, some operations of the algebra, such as the projection, iterate over the tuples whose annotation is non-zero. We thus need to know at least a superset of these tuples.

For these reasons, our definition of a 𝐾-relation is a Record with three fields: the function itself (named f), a support that encompasses at least tuples whose annotation is non-zero, and the sort of the relation sort -krel. In this definition, Fset is a library from Coccinelle of finite sets (similar to the Fbag library of the previous section).

To enforce the properties cited above, we define a Record, named Krel -inv, that states the invariant required for elements of type Krel. We will show later that, if this invariant is satisfied for queries consisting only of a relation, then it is enforced by all the operators of the algebra.

Record Krel -inv (kr:Krel) : Prop := mk -kri { finitesupport : ∀ t, t in? (support kr) = false → f kr t = 0; sortlabelssupp : ∀ t, t in? (support kr) = true → labels t = sort -krel kr; }

The field finite -support enforces that the support is actually a superset of the set of tuples that have a non-zero annotation. It is more general than having the exact set of tuples, and thus offers more possibilities for efficient implementations. The field sort -labels -supp ensures that the tuples of the support have the expected sort.

𝐾-algebra

We now provide our formalization of the semantics of the 𝐾-algebra. As for the semantics of relational algebra presented in the previous section, it is a recursive function, called eval -query -prov. We also keep the two layers of abstraction of Datacert: the following function operates over abstract datatypes and objects, which will be refined in Sec. 5. In particular, as the semantics of the relational algebra is based on abstract interpretation functions for symbols, predicates and aggregates (respectively called interp -symbol, interp -predicate and interp -aggregate, see Sec. 3.1), our semantics is based on extensions of these functions to 𝐾-relations, respectively called interp -symbol -prov, interp -predicate -prov and interp -aggregate -prov. We will detail this latter function below.

Fixpoint eval -query -prov (env : env -prov) (q : query) : Krel := match q with | Q -Table r ⇒ instance -prov r