Angela Bonifati

Stefania Dumbrava

Emilio Jesús

Gallego Arias

Under consideration for publication in Theory and Practice of Logic Programming 1 Certified Graph View Maintenance with Regular Datalog

Keywords: Regular Datalog, Graph Queries, Graph Views, Incremental Maintenance, Finite Semantics, Theorem Proving

We employ the Coq proof assistant to develop a mechanically-certified framework for evaluating graph queries and incrementally maintaining materialized graph instances, also called views. The language we use for defining queries and views is Regular Datalog (RD) -a notable fragment of non-recursive Datalog that can express complex navigational queries, with transitive closure as native operator. We first design and encode the theory of RD and then mechanize a RD-specific evaluation algorithm capable of fine-grained, incremental graph view computation, which we prove sound with respect to the declarative RD semantics. By using the Coq extraction mechanism, we test an OCaml version of the verified engine on a set of preliminary benchmarks. Our development is particularly focused on leveraging existing verification and notational techniques to: a) define mechanized properties that can be easily understood by logicians and database researchers and b) attain formal verification with limited effort. Our work is the first step towards a unified, machine-verified, formal framework for dynamic graph query languages and their evaluation engines.

Introduction

Modern graph query engines 1 are gaining momentum, due to the proliferation of interconnected data and related applications, spanning from social networks to scientific databases and the Semantic Web. The adopted query languages are navigational, focusing on data topology and, particularly, on label-constrained reachability. Notable examples [START_REF] Angles | Foundations of modern query languages for graph databases[END_REF]) include Neo4j's openCypher (Cypher ), Facebook's GraphQL (GraphQL ), SPARQL (SPARQL ), Gremlin (Gremlin ), Oracle's PGX (Oracle PGX ), and the recent G-CORE (G-Core ), even though a standard graph query language is still undefined.

At a foundational level, these languages are based on conjunctive queries (CQ), corresponding to Datalog [START_REF] Ceri | What you always wanted to know about Datalog (and never dared to ask)[END_REF]) clauses, i.e., function-free Horn formulas. Their common denominator is that they perform edge traversals (through join chains), while specifying and testing for the existence of label-constrained paths. Recently, a solution to the long standing open problem of identifying a suitable graph query Datalog fragment, balancing expressivity and tractability, has been proposed in [START_REF] Reutter | Regular queries on graph databases[END_REF]. We call this Regular Datalog (RD), a binary linear Datalog subclass that allows for complex, regular expression patterns between nodes. RD provides additional properties over full Datalog. First, its evaluation has NLOGSPACE-complete complexity, belonging to the NC class of highly parallelizable problems. Second, RD query containment is decidable, with an elementary tight bound (2EXPSPACE-complete) [START_REF] Reutter | Regular queries on graph databases[END_REF].

To the best of our knowledge, no specific evaluation algorithm for RD queries has been proposed yet. What are the main desiderata that such an algorithm should have? On the one hand, real-world graphs are highly dynamic, ever-increasing in size, and everchanging in content. Hence, efficiency, i.e., accelerating graph-based query processing, has become more relevant than ever. On the other hand, the sensitive nature of the data that large-scale, commercial graph database engines operate on makes ensuring strong reliability guarantees paramount.

We argue that having a deeply-specified framework for performing incremental graph computation, based on logic programming, opens important perspectives in a variety of areas, especially in light of security-sensitive applications involving graph-shaped topologies, e.g., financial transaction, forensic analysis, and network communication protocols.

Problem Statement: We target both requisites by developing a mechanically-verified framework for the fine-grained incremental view maintenance of graph databases (IVMGD). Specifically, let G be a graph database instance, ∆G, a set of modifications, and V [G], the materialization of an RD view or query over G. We provide an IVMGDaware engine that computes an incremental view update ∆V [G; ∆G], making the resulting view consistent with the updated graph database, i.e., V [G] ∪ ∆V [G; ∆G] = V [G ∪ ∆G].

Contributions: We build our mechanically-certified engine using theorem proving techniques, in particular we use the Coq proof assistant (The Coq Development Team 2018) to develop both the theory of the RD language and the evaluation engine itself. We make three major contributions: a) we formalize, in Coq, the syntax and semantics of Regular Queries, as Regular Datalog programs; b) we implement, in Coq's functional programming language Gallina, an executable engine for incremental RD maintenance; c) we prove the engine is sound, i.e. that it correctly computes incremental view updates.

We encode the semantics of RD using the finite set theory in the Mathematical Components library, which was developed to carry out the mechanized proof of the Feit-Thompson theorem [START_REF] Gonthier | A machine-checked proof of the odd order theorem[END_REF]) on finite group classification; it thus provides excellent support for finite reasoning. This brings the actual written-down mechanized semantics very close to a mathematical language, making it more accessible to non-expert practitioners -a central point to understand the guarantees provided by our development.

To develop our incremental graph view maintenance algorithm, we adapt the classical delta-rule one for IVM [START_REF] Gupta | Maintaining views incrementally[END_REF]) -initially designed for non-recursive SQL -to the RD evaluation setting.

Lastly, we prove our main result: "Let G be a base instance and Π, a RD program of view V . If Π is satisfied by the materialized view V [G], then, for a G update ∆G, the IVMGD engine outputs an incremental view update, ∆V [G; ∆G], such that Π is satisfied by V [G] ∪ ∆V [G; ∆G]". The proof relies on two key, newly-developed mechanized theories for stratified and incremental satisfaction of Datalog programs.

As mentioned in [START_REF] Fan | Incremental graph computations: Doable and undoable[END_REF], theoretical work on graph view maintenance is still in its infancy and, as noted in [START_REF] Beyhl | Incremental view maintenance for deductive graph databases using generalized discrimination networks[END_REF], most mainstream commercial graph databases do not provide concepts for defining graph views and maintenance.2 Thus, we believe that our verified engine builds the foundations for certifying realistic graph query and update engines, using declarative paradigms, such as Datalog subsets, as their query language. Specifically, this certified specification could serve as a blueprint for future graph query design and ongoing standardisation efforts (G-Core ). Additionally, we consider that most of our verification techniques are not restricted to the Regular Datalog setting, but are also applicable to broader logic programming contexts.

Organization: The paper is organized as follows. In Section 2, we illustrate the syntax and semantics of RD and its Coq formalization. In Section 3, we present the IVMGD algorithm and, in Section 4, we summarize its mechanized proof. Section 5 shows our extracted engine's performance on graph datasets with synthetic queries in RD. We describe related work in Section 6 and conclude and outline perspectives in Section 7. The Coq code for this paper can be downloaded from: https://github.com/VerDILog/ VerDILog/tree/iclp-2018.

Regular Datalog: Design and Formalization

In this section, we present the theory of Regular Datalog (RD) and its Coq mechanization. The language is based on Regular Queries (RQs) [START_REF] Reutter | Regular queries on graph databases[END_REF]). In Sec. 2.1 and Sec. 2.2, we detail our encoding of RD sytax and semantics. Sec. 2.3 illustrates potential usages of the language, in the context of financial transaction and social network graphs.

RD Syntax

We fix the finite sets of constants (nodes) and symbols (edge labels), namely, V and Σ.

Definition 1 (Graph Database) A graph instance G over Σ is a set of directed labelled edges, E, where E ⊆ V × Σ × V. A path ρ of length k in G is a sequence n 1 s1 -→ n 2 . . . n k-1 s k -→ n k . Its label is the concatenation of edge symbols, i.e., λ(ρ) = s 1 . . . s k ∈ Σ * .
G can be seen as a database D(G) = {s(n 1 , n 2 ) | (n 1 , s, n 2 ) ∈ E}, by interpreting its edges as binary relations between nodes. D(G) is also called the extensional database (EDB).

In order to model graphs in Coq, we assume a pair of finite types (finType), representing edge labels and nodes. The graph encoding (egraph ) is, thus, a finitely supported function (lrel ), mapping labels to their corresponding set of edges: Note that, for each label, our graph representation maintains both the regular set of edges and its transitive closure, denoted by the L type. We explain its usage in later sections.

t ::= n ∈ V | x ∈ V (Terms,
Definition 2 (Regular Datalog (RD)) Regular Datalog is the binary -all atoms have arity 2 -Datalog fragment, with recursion restricted to transitive closure and internalized as labels on literals.

There are several approaches to making the representation of logic programs amenable to efficient mechanical reasoning. We have found that indexing completed clauses by head symbols works well, as the corresponding canonical disjunctive definitions, from the clause map, become readily accessible in proofs. Fig. 1 provides the formal syntax for Regular Datalog programs. A program is a map from each symbol in Σ, to a single clause head and normalized disjunctive body. The normalized form is obtained by first transforming all clauses to a common head representation and then grouping their respective bodies. This classical process is similar to the completion procedure in [START_REF] Clark | Negation as failure[END_REF]. For example, the program: s(a, b). s(z, y) ← p(x, y), q + (z, x) is normalized as s(x, y) ← (a = x ∧ b = y) ∨ (p(z, y) ∧ q + (x, z)) and represented by a function from s to the head and disjunctive body. We encode RD primitives in Coq as records: A key feature of this formalization is that it is parametric in the variables Σ,T,L. This design choice allows sharing the representation for ground and non-ground clauses, and is central to the incrementality proof, in which we will decorate literals with customs labels. Also, note our naming convention for Coq constants, whereby the last letter denotes the type. For example, syma is the function that returns the symbol for an atom. syml does the same for a literal. Similarly, satisfaction conditions will be named sTa, sTl, etc., depending on the argument type.

Definition 3 (Regular Queries (RQ)) A regular query Ω over G is a RD program Π, together with a distinguished query clause, whose head is the top-level view (V ) and whose body is a conjunction of Π literals.

RD Semantics

The semantics of RD programs follows a standard term-model definition. As noted in Sec. 2.1, for optimization purposes, interpretations G are modeled as indexed relations (Σ × {∅, +}) → P(V × V), containing labeled graphs and their transitive closure. Then, program satisfaction builds on the below definition of satisfaction for (ground) literals:

Definition 4 (Literal Satisfaction)
The satisfaction G |= L of a ground literal L = s l (n 1 , n 2 ) is defined as:

G |= s l (n 1 , n 2 ) ⇐⇒ (n 1 , n 2 ) ∈ G(s, l)
Note that, in order for this definition to be correct, G must be well-formed, that is to say, the information stored in G(s, +) has to correspond to the actual transitive closure of G(s, ∅). We can state this condition as:

wfG(G) ⇐⇒ ∀s, is_closure(G(s, ∅), G(s, +)) is_closure(g s , g p ) ⇐⇒ ∀(n 1 , n 2 ) ∈ g p , ∃ρ ∈ V + , path(g s , n 1 , ρ) ∧ last(ρ) = n 2 path(g, n 1 , ρ) ⇐⇒ ∀i ∈ {1 . . . |ρ|}, (n i , n i+1 ) ∈ g
where the node list ρ ∈ V + represents the path without including the initial node n 1 .

Note that we compile the surface syntax s

-(X, Y ) to s(Y, X) and s * (X, Y ) to X = Y ∨ s + (X, Y ). The Coq encoding sTl gl of G |= L is a direct transcription of Def. 4
, where we henceforth omit the G parameter, as is it assumed to be implicit:

Definition sTl gl := G (syml gl, tagl gl) (argl gl).1 (argl gl).2. Definition 5 (Clause Satisfaction) A RD clause with disjunctive body D ≡ (L 1,1 ∧ . . . ∧ L 1,n ) ∨ . . . ∨ (L m,1 ∧ . . . ∧ L m,n )
and head symbol s is satisfied by G iff, for all groundings η, whenever the corresponding instantiation of a body in D is satisfied, then the head is also satisfied. Formally:

G |= s (t 1 , t 2 ) ← (L 1,1 ∧ . . . ∧ L 1,n ) ∨ . . . ∨ (L m,1 ∧ . . . ∧ L m,n ) ⇐⇒ ∀η, i=1..m ( j=1..n G |= η(L i,j )) ⇒ η(s(t 1 , t 2 ))
The Coq encoding of Def. 5 relies on the definition of an instantiation with a grounding η. We model η as a function g, of type gr, mapping from V (the ordinal type 'I_n) to V. This extends straightforwardly from terms to clauses. Note that has and all are the counterparts of the corresponding logical operations, extended to lists. We can define a model for an RD program as:

Definition 6 (Program Satisfaction) A well-formed interpretation G is a model for a program Π with respect to Σ iff G satisfies all of the Π clauses indexed by symbols in Σ: G |= Σ Π ⇐⇒ ∀ s ∈ Σ, G |= s Π(s).
The Coq encoding is straightforward:

Definition sTp (p : program n) := [forall s, sTc n s (p s)].
The formalized definition of satisfaction in Def. 6 is crucial to understanding the main soundness theorem in Sec. 4. It establishes that the output of the mechanized engine is a model of the input program, i.e., that it complies to the satisfaction specification of Def. 6 above. Hence, if this definition were to be incorrect -for example, by making sTp p = true -the theorem would become meaningless.

X Y pstransfer + pstransfer + (a) Potential Fraud X Y Z c c c c m + m + m + m + a a t (b) Secured Transfer
Fig. 2: Fraud Detection

RD Examples

We write (r + s)(x, y) for r(x, y) ∨ s(x, y) and (r • s)(x, y) for r(x, z) ∧ s(z, y).

Example 1 (Fraud Detection) Consider a financial transaction network, in which entities can connect and transfer money to each other, as well as monitor and accredit each other. A potential fraud/suspect transaction, e.g., money laundering, is a cycle of pstransfer + , i.e., potentially secured transfer chains (Fig. 2). A potentially secured transfer (pstransfer) is either a transfer (t) or a secured transfer. A secured transfer from X to Y occurs if Y is accredited (a) by X and if X secures a connection and transfers (t) to Y . X secures a connection to Y (blue subgraph in Fig. 2), if it connects (c) via a chain of intermediaries that are centrally monitored (m + ) by an accredited (a) entity Z. Potentially fraudulent (suspect) transactions can be computed with the RD program:

suspect(X, Y ) ← pstransfer + (X, Y ), pstransfer + (Y, X) pstransfer(X, Y )← (transfer + stransfer )(X, Y ) stransf er(X, Y ) ← accredited (Y, X), secures(X, Y ), transfers(X, Y ) secures(X, Y ) ← (connected • cmonitored + • connected)(X, Y ) cmonitored(X, Y )← connected (X, Y ), monitors + (Z, X), monitors + (Z, Y ), accredited (Z, X)
Example 2 (Brand Reach) Consider a platform, such as Twitter, with asymmetric connections and, thus, an underlying directed graph topology. Let Z be a brand (central node in Fig. 3) that wants to determine its reach, i.e. potential clients pairs (empty nodes in Fig. 3). A pair of users (X, Y ) are potential clients, if both were exposed to Z. We say X is exposed to Z, if X endorses Z or if it is connected, through a potential chain of followers, to an influencer that endorses Z. We say a user endorses a brand, if it likes and advertises the brand. We now describe the design of the mechanized IVMGD engine, which is based on the nonrecursive bottom-up evaluation of RD programs. We first describe the top-level interface of the engine and the main execution loop. Then, in Sec. 3.2, we outline the building block of non-incremental clause evaluation; in Sec. 3.3, we describe the delta-join incremental clause evaluation algorithm. Finally, Sec. 3.4 explains the implementation of the deltajoin heuristic in the actual engine.

Top-level Interface and Overview

The incremental RD evaluation engine is designed around bottom-up non-recursive program model computation. This is indeed adequate for graph and regular queries as these internalize recursion using closure operations -usually computed by specialized tools optimized for efficiency. While our engine builds on ideas from [START_REF] Benzaken | Certifying standard and stratified Datalog inference engines in SSReflect[END_REF], we have considerably redesigned all its core components: syntax is now based on a new parametric and normalized representation, and the core evaluation infrastructure and theory have been redesigned to account for stratified, single-pass, non-recursive incremental model computation. The formalization workload is higher in our setting, as we cannot rely on the usual fixpoint theorems, but must define a custom theory for modular program satisfaction.

A key problem to solve when reasoning about incremental computation is the representation of changes. Indeed, a formal definition of updates can be delicate to state, as it must account for potentially overlapping additions and removals, order issues, etc. To this end, we define canonical graph updates, reminiscent of, but weaker than "change structures" -defined in [START_REF] Cai | A theory of changes for higher-order languages: Incrementalizing λ-calculi by static differentiation[END_REF] The core operations for updates are their application to a base graph, and the modification of the changes pertaining to a particular symbol: Definition 8 (Update application and modification)

G :+: ∆ ≡ G \ ∆ -∪ ∆ + (application) ∆{s → (g + , g -)} ≡ (∆ + {s → g + }, ∆ -{s → g -\ g + }) (modification)
Armed with these definitions, plus those corresponding to the RD syntax and semantics from Sec. 2, we can now define the top-level interface to our engine. A particular challenge that arose during the development of the interface was allowing repeated, incremental ∆-aware calls. Achieving composition proved to be quite challenging, as the soundness invariant must be preserved along calls. In total, six parameters had to be used. The static input parameters are: a program Π, a graph G, and a set of symbols, or support supp, which indicates the validity of a subset of G, and thus what information the incremental engine may not recompute. Indeed, a precondition of the engine is that the input graph must be a model of Π up to supp, that is to say, G |= supp Π. Note that in the database literature, Σ is usually seen as a disjoint set pair, (Σ E , Σ I ), corresponding to the extensional and intensional parts of a program. For our engine, this distinction is "dynamic", in the sense that an already-processed strata-level is seen as "extensional", or immutable, for the rest of the execution. Thus, typical cases for supp will be supp ≡ Σ E , when the engine has been never been run before, or supp ≡ Σ, where G is the output of a previous run, and thus the consequences for all clauses have been computed.

Whereas the program, graph, and support are fixed during the execution of the engine, the latter will take an additional three dynamic parameters, representing the current execution state. These are: ∆, the current update, which is modified at each iteration, and Σ £ , Σ ¡ , which respectively represent the set of processed symbols/stratum and the "todo" list. We write Note that the compute_closures function above is an abstraction over an arbitrary algorithm for closure computation, that we assume correct. For instance, we hope to use the verified implementation of Tarjan's algorithm from [START_REF] Cohen | Full script of Tarjan SCC Coq/SSreflect proof[END_REF].

∆ O = T Π G,supp (Σ £ , Σ ¡ , ∆) (
As can be observed from the above code, the core part of the algorithm is concentrated in clause evaluation. Hence, we now proceed to presenting base and incremental for clause evaluation. Note that the base -or non-incremental -method is still needed since in some cases, incremental evaluation is either not possible or not sensible, as full re-computation may be faster.

The Base Engine for RD Evaluation

The base, or non-incremental, clause evaluation implements a forward-chaining consequence operator, using a matching algorithm M ; this takes as input atoms, literals, or clause bodies and returns a set of substitutions, as explained in [START_REF] Abiteboul | Foundations of Databases: The Logical Level[END_REF]. Basic literal matching, M L G (l) (match_lit in Coq) takes a literal and returns the set of all substitutions ss that satisfy it, so that ∀σ ∈ ss, G |= σ(l). Literal matching is extended to body matching in an straightforward way, with M B G (B) (match_body ) traversing B and accumulating the set of substitutions obtained from the individual matching. The algorithm we consider corresponds to computing nested-loop join and we implement it in a functional style, using a monadic fold. Substitutions are then accumulated for each disjunctive clause and grounded heads are added to the interpretation: Definition 9 (Clausal Consequence Operator ) Given a RD clause Π(s) ≡ (t 1 , t 2 ) ← i=1..n B i , the base clausal consequence operator T Π,s (G) computes the set of facts that can be inferred from G: and that gr σ head denotes the application of the substitution σ to the input head. The second line updates the resulting ∆, using the operator for modification (see Def. 8) and that for graph difference ( ). We remark that this base operator will re-derive all the facts, as it does not make use of incrementality information.

T Π,s (G) ≡ {σ(t 1 , t 2 ) | σ ∈ i=1..n M B G (B i )}.

Incremental Delta-Join Maintenance

Given a graph G, a program Π, and updates ∆, the engine in Sec. 3.2 non-incrementally maintains the top-level view of Π. However, the engine is unable to reuse and adjust previously computed maintenance information. This is makes it especially inefficient when few nodes are added to an otherwise high-cardinality graph.

To remedy this situation, we would like to extend our algorithm so that it can take into account the information of previously computed models. The key idea is to restrict matching to graph updates. For example, let V be a materialized view, defined as a simple join, in our case, as the path over two base edges, r and s, i.e. V (X, Y ) ← r(X, Z), s(Z, Y ). We abbreviate this as V = r s. Given base deltas, r ∆ and s ∆ , we can compute the view delta as ∆V = (r ∆ s) ∪ (r s ∆ ) ∪ (r ∆ s ∆ ), or, after factoring, as

V ∆ = (r ∆ s) ∪ (r ν s ∆ ), where r ν = r ∪ r ∆ . Hence, V ∆ = V ∆ 1 ∪ V ∆ 2 , with V ∆ 1 and V ∆ 2 computable via the delta clauses: δ 1 : V ∆ 1 ← r ∆ (X, Z), s ∆ (Z, Y ) and δ 2 : V ∆ 2 ← r ν (X, Z), s ∆ (Z, Y ).
Generalizing, for a database G and a purely additive update ∆, we can determine the view delta V ∆ [G; ∆], i.e., the set of facts such that V [G :

+: ∆] = V [G] ∪ V ∆ [G; ∆]. Definition 10 (Delta Program) Let V be a view defined by V ← L 1 , . . . , L n . The delta program δ(V ) is {δ i | i ∈ [1, n]}. Each delta clause δ i has the form V ← L 1 , . . . , L i-1 , L ∆ i , L ν i+1 , . . . , L ν n
, where: L ν j marks that we match L j against atoms in G ∪ ∆G with the same symbol as L j and L ∆ j marks that we match L j against atoms in ∆G with the same symbol as L j .

We revisit Example 1 to illustrate the computation of incremental view updates.

Example 3 (Detectable Frauds) Consider the transaction configuration in Fig. 4a, marking suspect transactions. A suspect transaction between X and Y is detectable, if there exists an entity that monitors both X and Y . We can compute all detectable suspect transactions with the RQ:

detectable(X, Y ) ← suspect(X, Y ), monitors(Z, X), monitors(Z, Y ) These are detectable = {(V 6 , V 0 ), (V 3 , V 0 ))}.
When updating the previous graph to the one in Figure 4b, we have: We now present the incremental version of the clause evaluation operator defined in Sec. 3.2. We follow Sec. 3.3 and modify base matching to take into account ∆-clauses and programs. Thus, for each body to be processed incrementally, we generate a body mask, placing a tag -{B, D, F} -on each body literal, which indicates whether matching should proceed against the base interpretation, against the update, or against both. The incremental atom matching operator M A,m G,∆ (match_delta_atoms ) is defined as:

detectable ν = {(V 6 , V 0 ), (V 3 , V 0 ), (V 0 , V 2 ), (V 2 , V 0 ), (V 0 , V 5 )}. The delta update detectable ∆ = {(V 0 , V 2 ), (V 2 , V 0 ), (V 0 , V 5 )} can be incrementally computed with the program Π ∆ = δ 1 ∪ δ 2 ∪ δ 3 , as follows: δ 1 = ∅, δ 2 = {(V 2 , V 0 )}, and δ 3 = {(V 0 , V 2 ), (V 0 , V 5 )}. Indeed, detectable ∆ = detectable ν \ detectable. V0 V1 V2 V3 V4 V5 V6 m m s s s s s s m m (a) Initial Graph V0 V1 V2 V3 V4 V5 V6 m m s s s s s s m m m m s (b) Updated Graph δ1 : detectable ∆ (X, Y ) ← suspect ∆ (X, Y ), monitors(Z, X), monitors(Z, Y ) δ2 : detectable ∆ (X, Y ) ← suspect ν (X, Y ), monitors ∆ (Z, X), monitors(Z, Y ) δ3 : detectable ∆ (X, Y ) ← suspect ν (X, Y ), monitors ν (Z, X), monitors ∆ (Z, Y ) (
M A,m G,∆ (a) = (if m ∈ {B, F} then M A G (a) else ∅) ∪ (if m ∈ {D, F} then M A ∆ (a)
else ∅) thus, base matching is called with the instance corresponding to the atom's tag.

Body ∆-matching, M B G,∆ (match_delta_body ) takes as an input a body mask, that is to say, a list of tag-annotated literals. A function body_mask generates the set B ∆ of "decorated" literals. Generic syntax is extremely helpful here to avoid duplication and to help state mask invariants in an elegant way. body_mask follows the diagonal factoring described below, where each row corresponds to an element of B ∆ : The last piece to complete the incremental engine is the top-level clausal maintenance operator. This part of the engine is significantly more complex than its base counterpart, as it must take into account which incrementality heuristics to apply:

    L 1 D L 2 F . . . L n-1 F L n F L 1 B L 2 D . . . L n-1 F L n
Definition 11 (Incremental Clausal Maintenance Operator )

The T Π,s G,supp (∆) operator for incremental clausal maintenance (fwd_or_clause_delta ) acts in two cases. If s / ∈ supp, or ∆ contains deletions for any of the literals in the body of Π(s), it uses the base operator T Π,s (G :+: ∆) -as we either cannot reuse the previous model or cannot support deletions through our incremental strategy. Otherwise, the operator will generate B ∆ = body_mask(B), for each of the bodies B, and return

Bm∈B∆ M B G,∆ (B m ).
4 Regular Datalog Evaluation: Certified Soundness

We now summarize the main technical points of the mechanized proof developed in Coq.

A key to effective mechanized proof development is the definition of the proper high-level concepts and theories; unfortunately we lack the space here to describe all the definitions used in our mechanized development in detail, so we highlight the main result, that proves the soundness of the engine, and we briefly survey the two core theories for stratification and incrementality. A few auxiliary results are described in Appendix A.

Stratification Conditions

Definition 12 (Stratified Programs)

A key precondition for the soundness of our engine is program stratification. A program Π is stratified, if there exists a mapping σ : Σ → [1, n] such that, for all s in Σ, the Π(s) clause (t 1 , t 2 ) ← B satisfies:

max r∈sym(B)
σ(r) < σ(s), where sym returns the set of symbols occurring in B. We then call σ a stratification of Π. In Coq, we encode stratification using a list of symbols and a predicate is_strata that recursively checks each uninspected symbol against an accumulator. This choice of representation is practical as it will guide model computation in the engine.

Definition 13 (Well-formed Program Slices) In order to reason about stratified satisfaction, we need a strengthened notion of wellformedness stating that a program is closed w.r.t. a symbol set. A symbol set Σ is a well-formed slice of Π if, for all s in Σ, sym(Π(s)) ⊆ Σ.

We establish that the engine operates over well-formed slices, which allows us to isolate reasoning about the current iteration, see the appendix for more technical details.

IGVM-Engine Characterization Result

Let Π be a safe RD program, Σ £ and Σ ¡ , symbol sets corresponding the "extensional" (already processed) and "intensional" (to be processed) strata, G a graph instance, and ∆ an update. Then we establish:

Theorem 1 (IGVM-Engine Soundness) Assume (H1) G is a model of the program for supp, G |= supp Π, (H2) Σ £ is a well-formed slice of Π, (H3) ∆ only contains information up to the processed strata, sym(∆) ⊆ Σ £ , (H4) Σ £ , Σ ¡ are a stratification of Π, and (H5) the currently model is sound, G : + : ∆ |= Σ£ Π then, the engine -implementing the maintenance operator

T Π G,supp (Σ £ , Σ ¡ , ∆) -outputs an update ∆ O , such that G :+: ∆ O |= Σ Π holds.

Proof

The proof is a consequence of the soundness of the incremental clausal maintenance operator T Π,s G,supp (Lem. 5). We proceed by induction on Σ ¡ . The base case follows from

Σ £ = Σ,

Experimental Analysis

In this section, we present the experimental validation of our certified engine on realistic graph databases. Our empirical analysis aims to confirm that incremental view maintenance (IVM) is more beneficial than full view materialization (FVM), corresponding to recomputing the view from scratch, at each modification of the underlying data. The comparison has been established by computing the runtimes on the same engine.

As it is common practice in the verification community, our extracted engine has been obtained through the mechanism of program extraction [START_REF] Letouzey | Extraction in Coq: An overview[END_REF], starting from our underlying Coq formalization. Assuming that Coq extraction is semantics preserving, also the underlying premise of our engine, the correctness of the obtained OCaml engine is readily guaranteed by the Coq specification we provided. This is a reasonable assumption, made by past verified tools, such as [START_REF] Leroy | Formal verification of a realistic compiler[END_REF]).

Our tests have been performed on a Intel Core i7 vPro G6 laptop, with 16GB RAM, running Ubuntu 17.10 64 bit, and OCaml 4.06.0.

For our experimental analysis, we generated synthetic datasets and query workloads using gMark [START_REF] Bagan | gMark: Schema-driven generation of graphs and queries[END_REF], which allowed us to encode, two state-of-the-art benchmarks: WD, the Waterloo SPARQL Diversity Test Suite (Wat-Div) [START_REF] Aluç | Diversified stress testing of RDF data management systems[END_REF], and SNB, the LDBC Social Network Benchmark [START_REF] Erling | The LDBC social network benchmark: Interactive workload[END_REF]. These graphshenceforth denoted by G -are diverse in terms of their density (increasing from SNB to WD) and of their in-degree and out-degree distributions [START_REF] Bagan | gMark: Schema-driven generation of graphs and queries[END_REF]. They represent two extreme cases to be considered in benchmarking graph database engines. Each schema size |supp(G)| is fixed at 82 and 27 predicates, for WD, respectively, SNB.

Based on this, we generate graph instances and companion query workloads, such that |G| = 1K nodes and |W| = 10 queries (queries represent views in our setting). Note that the gMark-generated queries are UC2RPQs -a notable subset of Regular Queries (RQs)3 . This should not be considered a restriction, as these queries already let us stress (for view maintenance) the navigational part of our engine and use the recursion in the form of Kleene-star -a bottleneck in many practical graph query engines (such as Neo4J) [START_REF] Bagan | gMark: Schema-driven generation of graphs and queries[END_REF].

In order to build the deltas necessary for incremental view maintenance, we sampled the original graph instance G by support size, i.e., by considering arbitrary subgraphs, whose number of symbols represent certain fractions of those in G. We call this method symbol-based sampling. Concretely, we retained a varying percentage ρ supp ∈ {0.05, 0.1, 0.15, 0.2, 0.25} from supp(G). Next, we took all corresponding instance facts with symbols in ρ supp to be our bulk insertions, ∆ + , where |supp(∆ + )| |supp(G)| = ρ supp . These bulk insertions correspond to adding the subgraphs of G, whose sets of symbols, sampled from supp(G), reflect the ρ supp ratio. We consider G = G \ ∆ + to be our base instances, i.e., the initial sets of facts to be processed by our engine.

Since we relied on symbol-based sampling, the actual sizes of deltas (|∆ + |) vary depending on the content of G. We denote the percentage capturing the relative sizes of the bulk inserts with respect to those of the base instances, as ρ = |∆+| |G | * 100 and report its actual values in the second column of each of the Tables 1 and2.

Next, we evaluated each query in a workload W over G and materialized the resulting views. Upon updating G with ∆ + , we compared the average timings for incremental view maintenance (IVM) and full view recomputation (FVM), over all view materializations, in each of the workloads. We summarize the results in Table 1 andTable 2. We observe that the absolute time gain (ms) of our engine running IVM with respect to it running FVM, i.e., Time Gain = FVM -IVM, is always positive and that the relative ratio gain (%), i.e., Ratio Gain = 100 -100 * IVM FVM , is always better for sparser graphs. As expected, our engine works best on bulk updates involving very small individual symbol updates, as these types of updates are targeted by delta join matching. Indeed, the complexity of our delta join depends on how many matchings have to be computed. Note that the lower the sparsity of the underlying graph, the less matches we have and the faster our engine is. This explains why the runtimes over SNB (less dense) are comparatively much better than the ones over WD (very dense). To the best of our knowledge, no verified graph query or IVM engine exists, which we both design and mechanize in this paper, using Regular Datalog. Bounded4 incremental graph computation has been addressed in [START_REF] Fan | Incremental graph computations: Doable and undoable[END_REF]) and shown beyond reach already with Regular Path Queries (RPQs), a restricted navigational RQ subset. The paper's idea is to incrementalize the bulk RPQ evaluation, by leveraging NFAs and auxiliary structures on large-scale graphs. We focus instead on the verification of forward-chaining-based IVM for the more expressive RQ graph query fragment. Although recent work has addressed certifying SQL semantics [START_REF] Chu | HoTTSQL: Proving query rewrites with univalent SQL semantics[END_REF], by proving the semantic preservation of rewriting rules in SQL query optimizers for relational data, such a mechanization is not applicable to the graph-data setting, where the key data model component is no longer a tuple, but a path (connecting pairs of graph nodes). To this end, our Coq development is based on the standard connectivity notion from the Mathematical Components library. Similarly, verified frameworks for the relational data model and nested relational algebra query compilers [START_REF] Benzaken | A Coq formalization of the relational data model[END_REF][START_REF] Auerbach | Handling environments in a nested relational algebra with combinators and an implementation in a verified query compiler[END_REF]) are fairly orthogonal to our work. The optimization issues around RQ evaluation have never been formally addressed in the database literature and, even for the simple UC2RPQ class, current graph database engines perform poorly (see [START_REF] Bagan | gMark: Schema-driven generation of graphs and queries[END_REF]). Even though our goal is not to provide a RQ optimizer, we touch base with some simple optimizations. These are clause normalization, a lightweight indexing mechanism (leveraging graph edges in the definition of supports), and our incremental supported satisfaction definition. This leads to a more elegant framework for reasoning about incremental properties.

Despite RD not being fully recursive, our engine handles stratified evaluation in a Datalog style. Focusing on linear recursion [START_REF] Jagadish | A study of transitive closure as a recursion mechanism[END_REF]) is indeed sufficient for our purposes, as it allows us to build a RQ-specific engine that inherently handles transitive closures. By limiting recursion, we can express graph recursive queries (RQs) that are ef-ficiency prone, being highly parallelizable [START_REF] Greenlaw | Limits to Parallel Computation: P-completeness Theory[END_REF]. The work in [START_REF] Benzaken | Certifying standard and stratified Datalog inference engines in SSReflect[END_REF] presents the SSReflect certification of a stratified static Datalog toy engine, implementing the bottom-up heuristic. While it supports Datalog's full recursion, this is actually a bottleneck even for non-verified graph query engines [START_REF] Bagan | gMark: Schema-driven generation of graphs and queries[END_REF]); also, it does not handle graph updates and IVM.

Finally, efficient Datalog engines have been designed in the last two decades, such as DLV2 [START_REF] Alviano | The ASP system DLV2[END_REF] and LogicBlox [START_REF] Aref | Design and implementation of the LogicBlox system[END_REF]. Our proposed methodology can be implemented on top of such advanced engines, to combine their efficiency with our certified mechanization. We hope that our work paves the way for a future interplay of the various optimized heuristics and implemented semantics for Datalog, with its comprehensively verified evaluation. While the Coq extraction mechanism is mature and well-tested, we plan to integrate the recent advances on the trusted extraction and compilation [START_REF] Anand | Certicoq: A verified compiler for Coq[END_REF][START_REF] Mullen | OEuf: Minimizing the Coq extraction TCB[END_REF] of Coq code into our framework.

Conclusion and Perspectives

We propose a Coq formal library for certified incremental graph query evaluation and view maintenance in the Regular Datalog fragment. It consists of 1062 lines of definitions, specifying our mechanized theory, and 734 lines of proofs, establishing the central soundness guarantee. Our mechanized specification builds on a library fine-tuned for the computer-aided theorem proving of finite-set theory results. We take advantage from this, by giving a high-level, mathematical representation of core engine components. This leads to composable lemmas that boil down to set theoretic statements and, ultimately, to a condensed development, avoiding the proof-complexity explosion characteristic of formal verification efforts. Moreover, we managed to extract a runnable engine exhibiting performance gains versus the non-incremental approach on realistic graph database benchmarks. Our foundational approach shows it is promising to combine logic programming and proof assistants, such as Coq, to give certified specifications for both a uniform graph query language and its evaluation. We plan to mechanize more optimized heuristics, particularly for efficiently handling joins, and to integrate custom algorithms, such as Tarjan, for transitive closure computation.

Fig. 1 :

 1 Fig. 1: Regular Datalog Grammar

  { litb : seq lit }. Record clause := Clause { headc: T * T; bodyc : seq cbody }. Inductive program := Program of {ffun Σ -> clause T Σ L}.

  Definition gr n := {ffun 'I_n -> V}. Definition sTb b := all sTl (litb b). Definition sTc n s c := [forall g : gr n, let gc := grc g c in has sTb (bodyc gc) ==> G (s,Single) (headc gc)].

  Fig. 3: Brand Reach

  ): Definition 7 (Graph Updates) An update ∆ ≡ (∆ + , ∆ -) is a pair of disjoint graphs, respectively representing insertions and deletions. In Coq, updates are encoded as a record edelta packing the graphs and a disjointedness proof; this allows us to consider only well-formed updates. Note that addd and deld are the record fields representing ∆ + and ∆ -: Definition wf_edelta addd deld := [forall s, [disjoint addd s & deld s]]. Structure edelta := { addd : lrel; deld : lrel; _ : wf_edelta addd deld }.

  written fwd_program in Coq) for a call to the engine returning an update ∆ O . We prove that the engine implements a program consequence algorithm, thus satisfying G :+: ∆ O |= Σ Π. Assuming a clause consequence operator T Π,sG,supp (∆) (or fwd_or_clause ), the below Coq implementation of the engine iterates over the unprocessed symbol list Σ ¡ and, for each of its symbols s to be inspected, it computes a new update ∆ . To this end, it modifies ∆ with the consequences for the clause indexed by s and computes the corresponding closure of s. The algorithm then makes the recursive call, adding s and s+ to the set of processed symbols.

Fixpoint

  fwd_program Π G supp Δ Σ£ Σ¡ : edelta := match Σ¡ with | [::] => Δ | [:: s & ss] => let (arg, body) := Π s in let Δ' := fwd_or_clause G supp Δ s arg body in let Δ' := compute_closures G Δ' s in fwd_program Π G supp Δ' (s ∪ s+ ∪ Σ£) ss

  Definition fwd_or_clause_base G Δ s c : edelta := let GΔ := edb :+: Δ in let T = [set gr σ c.headc | σ in \bigcup_(b <-c.bodyc) match_body G b ] in Δ{s → GΔ s T} in the first line, we use a set comprehension to build the set of ground facts corresponding to the consequence operator. Note that \bigcup_(x ← X) is the Coq notation for x∈X

  Fig. 4: Detectable Frauds

F

  . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . L 1

  as G :+: ∆ |= Σ£ Π holds by assumption. For the inductive case, let Σ ¡ ≡ {s} ∪ Σ ¡ and C be the clause Π(s). Given a set of symbols S and an update ∆ O , such that G :+: ∆ O |= S Π, the induction hypothesis (IH) ensures that G :+: ∆ O |= S∪Σ ¡ Π. Now, we need to prove that G :+: T Π G,supp ({s} ∪ Σ £ , Σ ¡ , T Π,s G,supp (∆)) |= Σ£∪{s}∪Σ ¡ Π. The conclusion results from instantiating (IH) with S = {s} ∪ Σ £ and ∆ O = T Π,s G,supp (∆). To this end, we need to first establish that G :+: T Π,s G,supp (∆) |= {s}∪Σ£ Π. This ensues from clause maintenance soundness and from modularity of model satisfaction. The rest of preconditions needed by IH hold, as follows. From H4, since ({s}∪Σ ¡ )∪Σ £ stratifies Π, we have that Σ ¡ ∪ {s} ∪ Σ £ also stratifies Π. Moreover, s / ∈ Σ £ , and sym(C) ⊆ Σ £ . From H2, we have that Σ £ is a well-formed slice of Π, which, together with sym(C) ⊆ Σ £ , proves {s} ∪ Σ £ is a well-formed slice. From H3, we know that sym(∆) ⊆ Σ £ . The auxiliary supp∆_fwd_or_clause lemma ensures that sym(∆ O ) ⊆ {s} ∪ sym(∆); it then follows, by transitivity, that sym(∆ O ) ⊆ {s} ∪ Σ £ . The Coq proof is about 25 lines long and comparable to this text-based version in size. The first line sets up the induction, with the rest of the proof consisting in the instantiation of the proper lemmas. The statement of the theorem itself takes 7 lines for the preconditions (1 per line) plus an additional line for the conclusion: ssTp (edb :+: ∆O) (Σ ∪ Σ£) Π.

Table 1 :

 1 Avg. W WD Runtimes (ms) for Varying Support Update Size (ρ supp )

	ρsupp	ρ	FVM	IVM	Time Gain Ratio Gain
	0.05	1.4%	558.7	484.75	73.95	13.23%
	0.1	3.67%	561.89	472.7	89.19	15.87%
	0.15	17.93% 562.67 475.96	86.71	15.41%
	0.2	9.7%	562.13	476.4	85.73	15.25%
	0.25	18.26%	563.4	482.64	80.76	14.33%
	ρsupp	ρ	FVM IVM Time Gain Ratio Gain
	0.05	10.89%	18.75	10.88	7.87	41.97%
	0.1	19.3%	17.77	10.55	7.22	40.63%
	0.15	10.77%	17.55	11.68	5.82	33.25%
	0.2	26.09%	17.17	11.71	5.46	31.79%
	0.25	28.34%	14.71	11	3.71	25.22%

Table 2 :

 2 Avg. W SNB Runtimes (ms) for Varying Support Update Size (ρ supp )

	6 Related Work

The only recent exception -which can handle named queries and updates -is Cypher for Apache Spark https://github.com/opencypher/cypher-for-apache-spark.

To the best of our knowledge, there currently is no practical benchmark capable of generating query workloads over the full fragment of Regular Datalog studied in this paper. The generation of graph query workloads for UC2RPQs has indeed been proved to be NP-complete[START_REF] Bagan | gMark: Schema-driven generation of graphs and queries[END_REF]).

The theory of bounded computational complexity for dynamic graph problems[START_REF] Ramalingam | On the computational complexity of dynamic graph problems[END_REF] considers the cost of incremental computation as a polynomial function of the input and output changes.

Acknowledgments: We would like to thank the anonymous referees and Pierre Jouvelot for their very useful comments and feedback. S.Dumbrava was funded by the Datacert project, ANR-15-CE39-0009, and by ANR-11-IDEX-0007.

Appendix A Notations and Proofs Highlights

The main notations used in the paper are summarized in Table . A 1. We describe in some more detail the theories used in our formal proof, in particular we summarize the main lemma for modular model reasoning as well as the intermediate soundness results. The reader is encouraged to look at the development directly, whose definitions are intended to be readable and understood even by non-experts.

In the rest of the section, G is assumed to be a labelled graph, g a non-labelled graph (set of edges), ∆ an update, Π a program, C a clause, Σ, Σ £ , Σ ¡ set of symbols, and s a symbol. Base Clausal Maintenance Operator (fwd_or_clause_base)

Base and Incremental Body Matching (match_body, match_delta_body)

Base and Incremental Atom Matching (match_atom, match_delta_atom)