Smart contracts are programs that are stored in distributed ledgers (e.g., blockchains) and are usually written in procedural languages to encode agreements between parties. Recent proposals focus on using logical languages for the specification and verification of such agreements. In this paper, in line with recent work, we analyse the usage of DatalogMTL for the creation of smart contracts. We discuss archetypal use cases and explore the temporal properties of DatalogMTL for formulating certain specifications.
the verification of smart contracts [ 9], current solutions for logic-based smart contracts, to the best of our knowlDistributed ledger technologies (for example, edge, do not consider temporal properties at all or in a blockchains) provide the foundation and core in- sub-optimal way, e.g., by arithmetic or by the introducfrastructure for decentralised finance (DeFi), a type tion of predicates with a special temporal meaning. This of finance that does not rely on intermediaries like is an enormous drawback, as many DeFi applications exchanges, banks or brokers [1]. DeFi applications are require some sort of temporal processing1. built by utilising smart contracts, which are executable Requirements. In the following, we suggest what we code that facilitates the process of executing and think are the most essential temporal requirements a enforcing the terms of an agreement between (untrusted) logic-based smart contract language has to support to parties [2]. provide a minimum amount of useful reasoning capabili
While agreements naturally follow a human-readable ties for DeFi applications. format (e.g., see Example 1.1), today’s usual way of writing such smart contracts is by encoding rules in an objectoriented programming language such as Solidity for the Ethereum platform. The procedural style of these languages requires to define what and how certain conditions should be handled, which is an error-prone and cumbersome process and hard to verify by non-experts whether the intention is reflected in code.
rate of 3% per year for three years. The interest payment is monthly.
gest the use of logic-based smart contract languages, which allow to better represent and reason upon the conditions of a smart contract [2, 3]. Diferent suggested solutions include the use of Prolog [4, 5], domainspecific languages [ 6], finite state machines [ 7], ActiveU-Datalog [8], or formal contract logic [3].
Let us consider Example 1.1 again. By carefully studying this example, one notices that it contains multiple temporal specifications (e.g., per month, per three years, or per year). While temporal reasoning has been used for 1. Validity Interval. It is necessary to represent intervals, i.e., when a specific kind of operation is valid, not only punctual points. This is necessary for example in voting contracts, where votes are exactly allowed between the start and the end of an interval. 2. Periodicity. It is necessary to specify periodic patterns that encode repeating agreements. This is necessary for example to encode that the salary is paid per month. 3. One Time Event/Delay. It is necessary to encode single future events. This is necessary for example for shopping contracts, where a payment reminder has to be sent in case the money has not been paid. 4. Negation. While only indirectly related to the temporal domain, it is necessary to support negation. This is necessary to encode that something has not happened in a specific interval as the previous example highlights. 5. Verification . It is necessary to verify whether a given model is satisfied for a given set of rules.
This helps for the verification of certain proper
work (see Section 3) ties and is in line with the work of using temporal logic for verification of smart contracts.
these requirements is DatalogMTL. DatalogMTL extends Datalog with the Horn fragment of metric temporal logic (MTL) and allows us to formulate expressions such as ⊟ [0,24ℎ]Signal() to state that the signal occurred continuously over the last 24 hours or [1ℎ,2ℎ]Signal() to state that the signal occurred at least once in the penultimate hour. It supports intervals (1) and delays (3) out of the box and provides the handling of periodicity (2) by the underlying reasoning language Datalog, where recursion is a fundamental core of the language. The support of negation (4) is provided by stratified negation (see preliminaries), but more complex forms of negation (i.e., stable models) have already been considered, if needed [10]. Contribution. In this work, we introduce DatalogMTL as a suitable language for formulating explainable logicbased smart contracts. In detail, our main contributions are: which we summarized in the beginning as requirements, and on the other hand, we suggest the usage of DatalogMTL as a go-to solution and introduce DatalogMTL smart contracts for writing DeFI applications. Organization. The remainder of this paper is organized as follows: In Section 2 we introduce DatalogMTL and provide a brief overview on Smart Contracts. In Section 3 we discuss related work in the area of logic-based smart contracts. We discuss the usage of DatalogMTL as a modelling language for Smart Contracts in Section 5 and conclude the work in Section 6.
2.1. Distributed Ledgers and Smart
Contracts
This paper contributes in two ways to the discussion of Intervals. An interval is of the form ⟨1, 2⟩, where the DeFi applications regarding the economic sector. On the left (right) bracket is either ( or [ () or ]) and 1, 2 ∈ one hand, we identify the need of supporting several tem- Z ∪ {−∞ , ∞}, such that 1 ≤ 2. An interval is positive poral properties in logic-based smart contract languages, if 1 > 0 and punctual if 1 = 2, which we write as the head of the rule, a model of a rule, when it satisfies instead of [, ]. all groundings of the rule and a model of a program Π , Syntax. We assume a disjoint set of variables and con- written M |= Π , if it is a model of all rules in Π and stants. An atom is an expression of the form ( ), where the program has a stratification. An interpretation M is a predicate of arity and is a tuple of constants is a model of a fact ()@, written M |= ()@, if apnredssviaorniagbilveesnmbaytcthheinfgoltlohweianrgityg.raAmlmitearra:l is an ex- M |= ()@ for all ∈ Z within , and a model of a set of facts (e.g., a dataset) if it is a model of all facts in ::= ⊤ | ⊥ | ( ) | ⊟ | ⊞ | . A program Π and a dataset entail a fact ()@ , | | | written (Π , ) |= ()@ , if ()@ for each model of Π and . where ( ) is an atom and is a positive interval. A rule is an expression of the form 1 ∧ · · · ∧ ∧ not +1 ∧ · · · ∧ not + → ′
for , ≥ 0 and where each is a literal and ′ is a Idelberger et al. [3] suggest the formulation via formal literal restricted to the following grammar: contract logic, a (deontic) defeasible logic. They suggest specifying a default state and use superiority relations to ′ ::= ⊥ | ( ) | ⊟ ′ | ⊞ ′ overwrite the state in case a specific event is triggered. The conjunction of is the body and ′ is the head of This logic always only derives a single state based on the rule. The literals 1, . . . , are positive body lit- current triggers that are valid at the current time. They erals of the rule, and +1, . . . , + are the negated have not discussed temporal properties at all. ones. A rule is safe, if all variables occur in positive body Similarly, Frantz and Nowostawski [6] decompose literals of the rule, and positive if it contains no negative institutions into rule-based statements, which are conbody literal. A DatalogMTL program is a finite set of safe structed from 5 diferent components (attributes (A), derules. A program Π is stratifiable if there exists a stratifi- ontic (D), aim (I), conditions (C), or else (O)). An example cation of a program Π . A stratification of Π is given as a is “people (A) must (D) vote (I) every four years (C), or function that maps each predicate in Π to positive inte- else they face a fine (O)” and suggest a mapping of the gers such that for each rule it holds that ( +) ≤ ( ) components to Solidity smart contracts using a domainand ( − ) < ( ) for + a positive body literal, − specific language which creates a template that has to be a negated body literal and the head of the rule. We say completed manually. that an expression is ground if it contains no variables. A Stancu and Dragan [5] suggested a Python-to-Prolog fact is an expression of the form ( )@, where ( ) is interface on top of BigchainDB and Tendermint to forground and a non-empty interval. A dataset is a finite ward Prolog clauses to a Prolog process to verify the set of facts. contract.
Semantics. An interpretation M specifies for each time Suvorov and Ulyantsev [7] suggest to use a LTL specipoint ∈ Z and for each ground atom () whether ifcation and test scenario to create a finite state machine, () is satisfied at , in which case we write M, |= which is combined with state and action definitions to (). This notion extends to ground literals as follows: generate a Solidity smart contract. They use LTL to express possible state transitions in a finite state machine, but again no temporal properties are explored such as a M, |= ⊤ for each ∈ Z duration of a voting period.
M, |= ⊥ for no ∈ Z Hu and Zhang [8] propose Logic-SC, a smart contract M, |= ⊟ if M, |= for all with − ∈ model based on Active-U-Datalog with temporal extenM, |= ⊞ if M, |= for all with − ∈ sions. Active-U-Datalog extends Datalog rules with upM, |= ′ if M, |= ′ for some with − ∈ date atoms, which can add or remove relations from ∧ M, |= for all ∈ (, ) the dataset. The temporal extension is provided by a pair ⟨[, ], ⟩, where is a periodic expression M, |= ′ if M, |= ′ for some with − ∈ and [, ] denotes the lower and upper bounds ∧ M, |= for all ∈ (, ) for the intervals in . An example of a periodic exM, |= if M, |= for some with − ∈ pression is all .Years + {3, 7}.Months ◁ 2.Months, repM, |= if M, |= for some with − ∈ resenting intervals starting as third and seven month of every year and having a duration of 2 months. A rule for counting the total working hours is given as follows totalhours (1), 2 = 1 + 1, +Hour (), ∈ workingTime → − totalhours (1), +totalhours (2),
every time point not , written M, |= not , if M, ̸|= . An interpretation is a model of a ground rule whenever it satisfies all atoms of the body it also satisfies where workingTime is a periodic expression. Critically, • is the set of activators. This set contains atoms this approach deletes elements which are not valid at the that expect input from others and act as interaccurrent time point and adds new elements, and hence tion points, which other smart contracts or parties simulates the behaviour of procedural implementations may invoke. Per time point, it is only allowed to which also add or remove elements. In comparison, our ifre one activator. approach works per time point and assumes a single ac- While Π and map directly to the definition of Dattion per time point. Hence, we explore the concept of alogMTL, and are in addition required for smart append-only data structures and create a new status for contracts. The namespace provides the possibility to call each new time point. other smart contracts by generating an atom, which is
Ciatto et al. [4] suggest a new language called Ten- prefixed with a namespace, or accessing data from other derfone, that is based on Prolog. It ofers several entry samgeasrtthceotnrtarnascftesr. oFfomreoxnaemy pinlec, acsoenosfiddeeratahw,tihlletnhoantemcaannpoints and built-in functions which manage the inter- write a rule of the form action with smart contracts. These functions include init (args), which gets executed once when the smart PersonDied ( ), Token.balance(, ), Heritage(, ) contract is deployed, receive(Msg, Sender) to invoke → Token.transfer (, , ) the smart contract and send (Msg, Recipient) to call to specify that the whole balance of (accessed from some other contract. In addition, they ofer several tem- the token) is transferred (by calling the token) to ’s heir poral predicates. This includes now (T) to get the cur- , in case died. rent timestamp, when(T, Msg) to trigger a receive of The activators provide input interfaces to the smart the smart contract at time , delay (DT, Msg) which contract. The set contains all atoms in the rules, which is equal to when(T + DT, Msg), now (T) and the fact can only be provided by external parties. Only one such that periodically (P, Msg), which triggers receive every activator is allowed to be fired per time point to ensure time units. This suggestion is close to our solution, as consistency with the rule (i.e., one time point exactly it is the only solution that considers temporal properties. matches to one state of the contract). This is without loss However, they only consider single time units and do not of generality, as in case multiple activators are required, cover intervals. they can be combined by introducing an additional acti
To summarize, related work focused on the formu- vator and creating auxiliary atoms for internal use. Note, lation of logic-based smart contracts as well as on the in the following examples we use directly the activators generation of eficient code. This paper will focus only in rule heads for readability, instead of instantiating some on the formulation aspect and keeps the generation open additional atom, i.e., we write rules of the form → , for future work. The solution of Hu and Zhang provide where is an activator, instead of introducing an auxilthrough the flexibility of Datalog, the possibility to model iary atom and map the activator to the auxiliary atom certain temporal properties, and the solution of Ciatto → which is used in the rules as head → . We et al. is the only work that actively considers temporal still ensure that only one external activator is used per properties in their proposal. To the best of our knowl- state transition. edge, intervals have not been considered so far in the study of logic-based smart contract languages.
the rule given in Example 1.1 is given as a quadruple (, Π , , ), where is some unique identifier 4. DatalogMTL Smart Contracts such as BitcoinLending , the dataset contains the information regarding the monthly interest payment In this section, we formally specify smart contracts with Borroww(0h.i0ch02is5c)@all[e0d, ∞wh)e,nthteheacletnivdaintogrstaritsstahnedafixteosm DatalogMTL. While the introduced program would allow the start time point, and the program Π is given as folone to specify the rules of the contract, possible interac- lows: tion points with diferent parties and smart contracts as well as an initial state have to be specified. Borrow (, ) → ⊞ [0,3]BorrowDur (, ) (1) Definition 4.1. A smart contract is a quadruple (, Π , , ) where: • is a unique name of the contract and can be
seen as a namespace for the contract. • Π is the DatalogMTL program encoding the rules
of the smart contract • is the initial dataset encoding the initial state of the smart contract.
Borrow (, ) → ⊞ [1,1]PayTime(, ) (2) PayTime(, ) → ⊞ [1,1]PayTime(, ) (3)
Interest (),
PayTime(, ),
BorrowDur (, ) → Token.transfer (, , ) (4) where Borrow (, ) specifies that borrows the money from , BorrowDur (, ) defines the duration of the borrow contract between and ,
PayTime(, ) specifies the time points when has
BitcoinLending.borrow(Alice, Bob)@200
Third party to pay interest to , Interest () specifies the interest amount which has to be paid and Token.transfer is a call to an external smart contract, for example a smart contract such as given in Section 5.2, where pays the amount .
In detail, Rule (1) specifies the duration of the agreement with three years beginning at the time point where Borrow gets called. Rules (2) and (3) define the payment time points. In detail, Rule (2) specifies the first interest payment as the first month after the time point where Borrow (, ) was activated by some party or smart contract, and Rule (3) extends this to follow-up payments recursively. Rule (4) executes the token transfer of the interest amount in case it is payment time and it is valid (i.e., during the BorrowDur ) by executing the activator of a diferent smart contract.
In the previous section, we introduced DatalogMTL smart contracts with a simple example. In this section, we study the use of DatalogMTL together with two real-world examples. We first consider a widely discussed example in the area of logic-based smart contracts, and then we discuss on how to utilize DatalogMTL for writing a smart contract for a crypto token.
Example 5.1. Let us consider the following clauses for the right to evaluate and publish the evaluation results of a product [3]: 1. The Licensor grants the Licensee a license to evaluate the Product. 2. The Licensee must not publish the results of the evaluation of the Product without the approval of the Licensor; the approval must be obtained before the publication. If the Licensee publishes results of the evaluation of the Product without approval from the Licensor, the Licensee has 24h to remove the material. 3. The Licensee must not publish comments on the evaluation of the Product, unless the Licensee is permitted to publish the results of the evaluation. 4. If the Licensee is commissioned to perform an independent evaluation of the Product, then the Licensee has the obligation to publish the evaluation results. 5. This license will terminate automatically if the
Licensee breaches this agreement.
to the economic sector, changing the stakeholders and adapting a few sentences directly leads to an economic example, namely, the golden power check for company takeovers [17]. In this case, the licensor is the government (which has veto/approval power for acquisitions), We visualized in Figure 1 the use of activators and names- the licensee is the “acquiring” company, and the product paces to access the data of another smart contract of is the target company.
Example 4.1, where we assume that is Alice, is Bob and there is some additional rule that requires access to the balance of (for example, to check whether is creditworthy or not) to visualize the read direction and a third party, which could either be Alice, Bob or some smart contract that start the borrowing transaction at some time point which gets added as fact to the contract (marked as blue) and derives all other facts given in the box according to the rules of the program.
We use the atom GrantX (, , ) to specify that Licensor has granted Licensee the right to do for product , where is either Use to grant the right to evaluate, Commission to grant the right to publish results without approval, Appr to grant the right to publish the results. We further use Publish (, ) to specify that has published the results of product and Comment (, ) to specify that has made a comment on the evaluation of product , Remove(, ) to specify that has removed the content and Violation (, ) to specify that has violated the license for product and OblRemove(, ) to specify that is obliged to remove the license.
The smart contract is then defined as a quadruple (, Π , , ), where is some unique identifier such as LicenseAgreement , the dataset is empty, the activators are given by the set of atoms {Publish , Comment , GrantAppr , GrantCommission , GrantUse, Remove} and the program Π is given by the following rules, where we omit the terms in the rules for readability:
(1)
Ethereum ERC20 specification, which are in total three methods: • Transfer. Party transfers amount to party . Such a transfer is only allowed if the current balance of is bigger or equal to . • Approve. Party allows party to withdraw amount . • TransferFrom. Party transfers amount from party to party . Such a transfer is only allowed if the current balance of and the approval value for from are bigger or equal to .
¬ ⊟ [0,24] OblRemove → ⊞ [1,1]OblRemove ⊟ [0,24]OblRemove → Violation
(2) (3) (4) (5) (6) (7) Rule (1) specifies that an approval holds forever. Rules 2-4 match clause (2). Rule 2 states that if the results are published, but they are not approved, then the licensee is obliged to remove the results. Rule (3) specifies the duration of the obligation, which is bounded to 24 hours and extended to the next time point in case no removal We use the atom Tran(, , ) to specify that there is has happened. Note that this rule uses an extended form a request to transfer amount from party to party of stratified negation, namely, temporal stratified nega- , TranF (, , , ) to specify that there is a request tion. In this form, the negated facts in recursion only from party to transfer amount from party to party propagate information from the past to the future. Rule , App(, , ) to denote that party allows party (4) then triggers a violation in case the maximum time to transfer amount . In addition we specify that of 24 hours has been reached. For comments, there is no the requested transfer is valid by VTran(, , ), and exception and hence any comment without approval is denote with Bal (, ) that party ’s current balance marked as a violation by Rule (5) which matches clause is . (3) of the agreement. Rule (6) handles independent evalu- The smart contract is then defined as a quadruple ations. In case this right is given, then it is also approved. (, Π , , ), where the namespace is some unique Rule (7) manages the extension of the license, in case no identifier such as Token, the dataset contains the violation occurred. ipnleit,iailnbathlaisnccea, sweh2i0ch00istaoskseingnseadretoaossniegnoerdmtooreApliecoe-, Discussion. From the example, we can see that Dat- Bal (, 2000), the activators are given by the set of alogMTL allows to express complex contracts without atoms {Tran, App, TranF } and the program Π is given the need of formulating rules with any form of explicit by the following rules time-handling by only using temporal operators. By comparing the example with the established requirements Tran(, , ), Bal (, ), from Section 1, this example gives evidence for require- ≤ → VTran(, , ) (1) ment (1) by rule (1) or (4), requirement (3) by rule (4), requirement (4) by rules (2), (3), (5) and (7). We do not VTran(, , ), Bal (, ) → ⊞ [1,1]Bal (, − ) (2) cover requirement (2) here, but (2) has been covered in VTran(, , ), Bal (, ) → ⊞ [1,1]Bal (, +) (3) Section 4. Requirement (5) is usually not part of the con- App(, , ), tract itself but used to verify that a contract does not reach a certain state. For example, it can be used to state TranF (, , , ), ≤ → Tran(, , ) (4) that only one activator is fired at most once per time VTran(, , ), point or to state that it is not possible to publish a re- App(, , ), sult without having the license to use the program, as the program cannot be evaluated. The latter case can be TranF (, , , ), formulated by a rule of the following form: = − → ⊞ [1,1]App(, , ) (5)
Bal (, ), ¬VTran(, _, _),
5.2. ERC20 Token
token contract [18] can be formalized in DatalogMTL.
The standard provides some read-only functions, such as what is the current balance of a user, which we do not consider in the example, as just the atoms of the program have to be accessed. In the following, we focus on the functions, which change the state of the contract. The goal of these functions is to specify when a transfer of tokens between two parties is allowed and how a transfer afects the balance of the parties. ¬VTran(_, , _) → ⊞ [1,1]Bal (, )
App(, , ), ¬VTran(, _, _) → ⊞ [1,1]App(, , ) (7)
App(, , ),
(6)
VTran(, _, _), ¬TranF (, _, _, ) → ⊞ [1,1]App(, , ) (8) Rule (1) verifies whether the balance of party is enough for the transfer. Rules (2) and (3) apply a verified transfer by reducing and increasing the balance of the participating parties. Rule (4) applies the third-party transfer by checking whether the party is allowed to transfer the amount from party . In such a case, a usual transfer is emitted, which is handled by rules (1) to (3). Rule (5) [4] G. Ciatto, A. Mafi, S. Mariani, A. Omicini, Smart updates the approval amount in case such a transaction contracts are more than objects: Pro-activeness on is successful. Rules (6)-(8) are the housekeeping rules, the blockchain, in: BLOCKCHAIN, volume 1010 which copy the current balance and the approved value of Advances in Intelligent Systems and Computing, to the next unit, in case nothing changed. Springer, 2019, pp. 45–53.
Arithmetic Expressions. In this example, we have used [5] A. Stancu, M. Dragan, Logic-based smart contracts, arithmetic expressions in the rules, which have not been in: WorldCIST (1), volume 1159 of Advances in Informally defined in DatalogMTL. We want to point out telligent Systems and Computing, Springer, 2020, pp. that the use of arithmetic in recursion without any re- 387–394. strictions yields undecidability in general [19], however [6] C. Frantz, M. Nowostawski, From institutions to in this case the arithmetic expression is bounded by acti- code: Towards automated generation of smart convators. A formal definition of arithmetic in DatalogMTL tracts, in: FAS*W@SASO/ICCAC, IEEE, 2016, pp. has not been considered yet and is future work. The 210–215. arithmetic operations of this example follow the default [7] D. Suvorov, V. Ulyantsev, Smart contract design notion of addition and subtraction. meets state machine synthesis: Case studies, CoRR abs/1906.02906 (2019). [8] J. Hu, Y. Zhong, A method of logic-based smart 6. Conclusion contracts for blockchain system, in: ICDPA, ACM, 2018, pp. 58–61.
In this paper, we introduced DatalogMTL as an option [9] P. Tolmach, Y. Li, S. Lin, Y. Liu, Z. Li, A survey of to model smart contracts. We first derived the essential smart contract formal specification and verification, requirements for the necessary features in smart con- ACM Comput. Surv. 54 (2022) 148:1–148:38. tracts, and then introduced DatalogMTL as a basis for a [10] P. A. Walega, D. J. T. Cucala, E. V. Kostylev, B. C. smart contract language. We explored our language by Grau, Datalogmtl with negation under stable moddiscussing two real-world examples. In the first one, we els semantics, in: KR, 2021, pp. 609–618. introduced a widely discussed existing example and high- [11] 101 Blockchains, What is dlt (distributed ledger lighted the advantages of using DatalogMTL, while in technology) ?, 2021. URL: https://101blockchains. the second one we discussed how to model tokens with com/what-is-dlt/.
DatalogMTL. Thereby, we identified the need to have [12] S. Popov, The tangle, White paper 1 (2018). a formally proved arithmetic extension of DatalogMTL [13] M. Hearn, R. G. Brown, Corda: A distributed ledger to support DeFi applications which require arithmetic (2019). operations, which we will consider studying in the future. [14] H. Anwar, Smart contracts: The ultimate guide for In addition, we want to focus on compiling DatalogMTL the beginners, 2018. URL: https://101blockchains. smart contracts to existing procedural smart contract com/smart-contracts/. languages such as Solidity to support well-established [15] P. A. Walega, B. C. Grau, M. Kaminski, E. V. blockchains such as Ethereum. Kostylev, Datalogmtl over the integer timeline, in: Acknowledgments. This work was supported by the KR, 2020, pp. 768–777.
Vienna Science and Technology Fund (WWTF) grant [16] D. J. T. Cucala, P. A. Walega, B. C. Grau, E. V. VRG18-013, and the “rAIson data” Royal Society grant of Kostylev, Stratified negation in datalog with metric Prof. Georg Gottlob. temporal operators, in: AAAI, AAAI Press, 2021, pp. 6488–6495. [17] L. Bellomarini, M. Benedetti, S. Ceri, A. Gentili, References R. Laurendi, D. Magnanimi, M. Nissl, E. Sallinger, Reasoning on company takeovers during the [1] A. Singh, What is decentralized finance or defi ex- COVID-19 crisis with knowledge graphs, in: plained, 2021. URL: https://medium.com/brandlitic/ RuleML+RR (Supplement), volume 2644 of CEUR dc0ce376f7b2. Workshop Proceedings, CEUR-WS.org, 2020, pp. 145– [2] M. Alharby, A. van Moorsel, Blockchain-based 156.
smart contracts: A systematic mapping study, CoRR [18] V. B. Fabian Vogelsteller, Eip-20, 2015. URL: abs/1710.06372 (2017). https://github.com/ethereum/EIPs/blob/master/ [3] F. Idelberger, G. Governatori, R. Riveret, G. Sar- EIPS/eip-20.md.
tor, Evaluation of logic-based smart contracts for [19] B. C. Grau, I. Horrocks, M. Kaminski, E. V. Kostylev, blockchain systems, in: RuleML, volume 9718 of B. Motik, Limit datalog: A declarative query lanLecture Notes in Computer Science, Springer, 2016, guage for data analysis, SIGMOD Rec. 48 (2019) pp. 167–183. 6–17.