Modelling Smart Contracts with DatalogMTL Markus Nissl1 , Emanuel Sallinger1 1 TU Wien, Vienna, Austria Abstract 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. Keywords DatalogMTL, Smart Contract, Blockchain 1. Introduction the verification of smart contracts [9], current solutions for logic-based smart contracts, to the best of our knowl- Distributed 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 introduc- frastructure 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 writ- ing such smart contracts is by encoding rules in an object- 1. Validity Interval. It is necessary to represent in- oriented programming language such as Solidity for the tervals, i.e., when a specific kind of operation is Ethereum platform. The procedural style of these lan- valid, not only punctual points. This is necessary guages requires to define what and how certain condi- for example in voting contracts, where votes are tions should be handled, which is an error-prone and exactly allowed between the start and the end of cumbersome process and hard to verify by non-experts an interval. whether the intention is reflected in code. 2. Periodicity. It is necessary to specify periodic Example 1.1. I lend you ten Bitcoins with an interest patterns that encode repeating agreements. This rate of 3% per year for three years. The interest payment is necessary for example to encode that the salary is monthly. is paid per month. 3. One Time Event/Delay. It is necessary to encode In an attempt to tackle this issue, researchers sug- single future events. This is necessary for ex- gest the use of logic-based smart contract languages, ample for shopping contracts, where a payment which allow to better represent and reason upon the reminder has to be sent in case the money has conditions of a smart contract [2, 3]. Different sug- not been paid. gested solutions include the use of Prolog [4, 5], domain- 4. Negation. While only indirectly related to the tem- specific languages [6], finite state machines [7], Active- poral domain, it is necessary to support negation. U-Datalog [8], or formal contract logic [3]. This is necessary to encode that something has Let us consider Example 1.1 again. By carefully study- not happened in a specific interval as the previous ing this example, one notices that it contains multiple example highlights. temporal specifications (e.g., per month, per three years, 5. Verification. It is necessary to verify whether a or per year). While temporal reasoning has been used for given model is satisfied for a given set of rules. This helps for the verification of certain proper- Published in the Workshop Proceedings of the EDBT/ICDT 2022 Joint Conference (March 29-April 1, 2022), Edinburgh, UK ยฉ 2022 Copyright for this paper by its authors. Use permitted under Creative 1 Commons License Attribution 4.0 International (CC BY 4.0). We discuss current solutions in the discussion of the related CEUR Workshop Proceedings http://ceur-ws.org ISSN 1613-0073 CEUR Workshop Proceedings (CEUR-WS.org) work (see Section 3) ties and is in line with the work of using temporal which we summarized in the beginning as requirements, logic for verification of smart contracts. and on the other hand, we suggest the usage of Data- logMTL as a go-to solution and introduce DatalogMTL DatalogMTL. A typical language that supports all of smart contracts for writing DeFI applications. these requirements is DatalogMTL. DatalogMTL extends Organization. The remainder of this paper is organized Datalog with the Horn fragment of metric temporal logic as follows: In Section 2 we introduce DatalogMTL and (MTL) and allows us to formulate expressions such as provide a brief overview on Smart Contracts. In Section 3 โŠŸ[0,24โ„Ž] Signal(๐‘ฅ) to state that the signal ๐‘ฅ occurred con- we discuss related work in the area of logic-based smart tinuously over the last 24 hours or [1โ„Ž,2โ„Ž] Signal(๐‘ฅ) to contracts. We discuss the usage of DatalogMTL as a state that the signal ๐‘ฅ occurred at least once in the penul- modelling language for Smart Contracts in Section 5 and timate hour. It supports intervals (1) and delays (3) out of conclude the work in Section 6. 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 2. Preliminaries negation (4) is provided by stratified negation (see prelim- inaries), but more complex forms of negation (i.e., stable In this section, we briefly introduce smart contracts and models) have already been considered, if needed [10]. present the syntax and semantic of DatalogMTL with Contribution. In this work, we introduce DatalogMTL stratified negation over the integer timeline. as a suitable language for formulating explainable logic- based smart contracts. In detail, our main contributions 2.1. Distributed Ledgers and Smart are: Contracts โ€ข We established a set of temporal requirements for A distributed ledger technology (DLT) is a decentralized, logic-based smart contract languages which we immutable, and append-only database across different think are necessary for a variety of agreements. nodes that is managed by multiple participants. At the โ€ข We formally define a smart contract language on core of the DLT is a consensus mechanism which contains top of DatalogMTL which considers the interac- procedures and rules on how transactions are validated tion with other smart contracts. by the nodes [11]. โ€ข We provide a case study on real-world examples on A blockchain is a form of DLT, where transactions are exploring DatalogMTL for Smart Contracts where recorded and grouped into blocks, where each block in- we discuss the modelling of smart contracts as cludes a hash of the previous block. Other forms of DLTs well as the verification. are Tangle [12], built on top of a directed acyclic graph, โ€ข We provide throughout the work connections to or Corda [13], a leading DLT for regulated industries the economic sector, targeting exactly the area of where the ledger stores per node only the facts the node the workshop. is aware of. Smart Contracts are programs stored on the distributed Financial and Economic Context. We briefly want to ledger technology that run when certain conditions are relate the work to the financial and economic context. satisfied. Usually, smart contracts manage an agreement As already highlighted in the beginning of the introduc- (i.e., rules) between multiple parties per code without re- tion, DeFi will become (or already is) an area with a high quiring a third party. They reduce risk due to the tamper- volume of transactions and a high market capitalization. proof property of DLTs and provide transparency to the Current DeFi solutions lack insight and do not provide process. Typical smart contract applications include vot- explainable systems. We have the opinion that logic- ing, supply chains, mortgage, copyright protection, or based smart contracts, and especially DatalogMTL, could employment arrangements [14]. provide the required core for reasoning over DeFi ap- plications and would be suitable as a basis for building 2.2. DatalogMTL systems for many economic and financial fields, such as: DatalogMTL extends Datalog with metric temporal logic. โ€ข Regulatory Compliance In this section, we briefly recap the syntax and seman- โ€ข Anti-money Laundering tic of DatalogMTL over the integer timeline [15] with โ€ข Financial stability assessment stratified negation [16]. 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 and variables matching the arity. A literal ๐‘€ is an ex- M |= ๐‘ƒ (๐‘Ž)@๐‘ก for all ๐‘ก โˆˆ Z within ๐œš, and a model of a pression given by the following grammar: 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 ๐‘€๐‘˜+๐‘š โ†’ ๐‘€ โ€ฒ 3. Related Work 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 con- body literal. A DatalogMTL program is a finite set of safe structed from 5 different components (attributes (A), de- rules. 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 domain- and ๐œŽ(๐‘ƒ โˆ’ ) < ๐œŽ(๐‘ƒ ) 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 for- ground and ๐œš a non-empty interval. A dataset is a finite ward Prolog clauses to a Prolog process to verify the set of facts. contract. Suvorov and Ulyantsev [7] suggest to use a LTL speci- Semantics. An interpretation M specifies for each time fication and test scenario to create a finite state machine, point ๐‘ก โˆˆ Z and for each ground atom ๐‘ƒ (๐‘Ž) whether which is combined with state and action definitions to ๐‘ƒ (๐‘Ž) is satisfied at ๐‘ก, in which case we write M, ๐‘ก |= generate a Solidity smart contract. They use LTL to ex- ๐‘ƒ (๐‘Ž). This notion extends to ground literals as follows: press 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, ๐‘ก |= โŠŸ๐œš ๐ด iff M, ๐‘  |= ๐ด for all ๐‘  with ๐‘ก โˆ’ ๐‘  โˆˆ ๐œš model based on Active-U-Datalog with temporal exten- M, ๐‘ก |= โŠž๐œš ๐ด iff M, ๐‘  |= ๐ด for all ๐‘  with ๐‘  โˆ’ ๐‘ก โˆˆ ๐œš sions. Active-U-Datalog extends Datalog rules with up- M, ๐‘ก |= ๐ด ๐’ฎ๐œš ๐ดโ€ฒ iff 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, ๐‘ก |= ๐ด ๐’ฐ๐œš ๐ดโ€ฒ iff M, ๐‘  |= ๐ดโ€ฒ for some ๐‘  with ๐‘  โˆ’ ๐‘ก โˆˆ ๐œš and [๐‘๐‘’๐‘”๐‘–๐‘›, ๐‘’๐‘›๐‘‘] denotes the lower and upper bounds โˆง M, ๐‘Ÿ |= ๐ด for all ๐‘Ÿ โˆˆ (๐‘ก, ๐‘ ) for the intervals in ๐‘ƒ . An example of a periodic ex- M, ๐‘ก |= ๐ด ๐œš iff M, ๐‘  |= ๐ด for some ๐‘  with ๐‘ก โˆ’ ๐‘  โˆˆ ๐œš pression is all .Years + {3, 7}.Months โ— 2.Months, rep- M, ๐‘ก |= ๐œš ๐ด iff M, ๐‘  |= ๐ด for some ๐‘  with ๐‘  โˆ’ ๐‘ก โˆˆ ๐œš resenting intervals starting as third and seven month of every year and having a duration of 2 months. A An interpretation M satisfies for each literal ๐‘€ and rule for counting the total working hours is given as every time point ๐‘ก not ๐‘€ , written M, ๐‘ก |= not ๐‘€ , if follows totalhours(๐‘ก1 ), ๐‘ก2 = ๐‘ก1 + 1, +Hour (๐‘ก), ๐‘ก โˆˆ M, ๐‘ก ฬธ|= ๐‘€ . An interpretation is a model of a ground rule workingTime โ†’ โˆ’totalhours(๐‘ก1 ), +totalhours(๐‘ก2 ), 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 interac- current 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 fire one activator. approach works per time point and assumes a single ac- While ฮ  and ๐ท map directly to the definition of Dat- tion 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 offers several entry smart contracts. For example, consider a will that man- ages the transfer of money in case of death, then one can points 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 offer 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 efficient 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 auxil- through 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. Example 4.1. A smart contract in DatalogMTL with the rule given in Example 1.1 is given as a quadru- ple (๐‘, ฮ , ๐ท, ๐ด), where ๐‘ is some unique identifier 4. DatalogMTL Smart Contracts such as BitcoinLending, the dataset ๐ท contains the information regarding the monthly interest payment ๐ผ๐‘›๐‘ก๐‘’๐‘Ÿ๐‘’๐‘ ๐‘ก(0.0025)@[0, โˆž), the activator ๐ด is the atom In this section, we formally specify smart contracts with Borrow which is called when the lending starts and fixes DatalogMTL. While the introduced program would allow the start time point, and the program ฮ  is given as fol- one to specify the rules of the contract, possible interac- lows: tion points with different parties and smart contracts as Borrow (๐ด, ๐ต) โ†’ โŠž[0,3๐‘ฆ] BorrowDur (๐ด, ๐ต) (1) well as an initial state have to be specified. Borrow (๐ด, ๐ต) โ†’ โŠž[1๐‘š,1๐‘š] PayTime(๐ด, ๐ต) (2) Definition 4.1. A smart contract is a quadruple PayTime(๐ด, ๐ต) โ†’ โŠž[1๐‘š,1๐‘š] PayTime(๐ด, ๐ต) (3) (๐‘, ฮ , ๐ท, ๐ด) where: Interest(๐‘‹), PayTime(๐ด, ๐ต), โ€ข ๐‘ is a unique name of the contract and can be seen as a namespace for the contract. BorrowDur (๐ด, ๐ต) โ†’ Token.transfer (๐ด, ๐ต, ๐‘‹) (4) โ€ข ฮ  is the DatalogMTL program encoding the rules where Borrow (๐ด, ๐ต) specifies that ๐ด borrows the of the smart contract money from ๐ต, BorrowDur (๐ด, ๐ต) defines the du- โ€ข ๐ท is the initial dataset encoding the initial state ration of the borrow contract between ๐ด and ๐ต, of the smart contract. PayTime(๐ด, ๐ต) specifies the time points when ๐ด has BitcoinLending Token 5.1. License Agreement Token.transfer(Alice , Bob, 0.125)@20 Interest(0.025)@[0, โˆž] 0 Balance(Alice, 999)@200 Borrow(Alice,Bob)@200 BorrowDur(Alice,Bob)@[200,236] โ€ฆ Balance(Alice, 990)@236 In this case study, we focus on the specification of a PayTime(Alice,Bob)@201 PayTime(Alice,Bob)@202 Balance(Bob, 100)@200 โ€ฆ license agreement[7, 3, 8]. In this section, we want to ex- โ€ฆ. PayTime(Alice,Bob)@236 Token.balance(A lice, 999)@200 Balance(Bob, 109)@236 plore how such a contract can be written in DatalogMTL. [Other facts] Example 5.1. Let us consider the following clauses for BitcoinLending.borrow(Alice, Bob)@200 the right to evaluate and publish the evaluation results Third party of a product [3]: [Other facts] 1. The Licensor grants the Licensee a license to eval- uate the Product. Figure 1: Calling of borrow by a third party in 2. The Licensee must not publish the results of the BitcoinLending . Accessing data (balance ) and calling evaluation of the Product without the approval (transfer ) of smart contract Token in smart contract of the Licensor; the approval must be obtained BitcoinLending . before the publication. If the Licensee publishes results of the evaluation of the Product without approval from the Licensor, the Licensee has 24h to pay interest to ๐ต, Interest(๐‘‹) specifies the interest to remove the material. amount which has to be paid and Token.transfer is a 3. The Licensee must not publish comments on the call to an external smart contract, for example a smart evaluation of the Product, unless the Licensee is contract such as given in Section 5.2, where ๐ด pays ๐ต permitted to publish the results of the evaluation. the amount ๐‘‹. 4. If the Licensee is commissioned to perform an In detail, Rule (1) specifies the duration of the agree- independent evaluation of the Product, then the ment with three years beginning at the time point where Licensee has the obligation to publish the evalua- Borrow gets called. Rules (2) and (3) define the payment tion results. time points. In detail, Rule (2) specifies the first interest 5. This license will terminate automatically if the payment as the first month after the time point where Licensee breaches this agreement. Borrow (๐ด, ๐ต) was activated by some party or smart Apart from the fact that contracts are of natural interest contract, and Rule (3) extends this to follow-up payments to the economic sector, changing the stakeholders and recursively. Rule (4) executes the token transfer of the adapting a few sentences directly leads to an economic interest amount in case it is payment time and it is valid example, namely, the golden power check for company (i.e., during the BorrowDur ) by executing the activator takeovers [17]. In this case, the licensor is the govern- of a different smart contract. ment (which has veto/approval power for acquisitions), the licensee is the โ€œacquiringโ€ company, and the product We visualized in Figure 1 the use of activators and names- is the target company. paces to access the data of another smart contract of Example 4.1, where we assume that ๐ด is Alice, ๐ต is Bob We use the atom GrantX (๐ด, ๐ต, ๐‘ƒ ) to specify that Li- and there is some additional rule that requires access to censor ๐ด has granted Licensee ๐ต the right to do ๐‘‹ for the balance of ๐ด (for example, to check whether ๐ด is product ๐‘ƒ , where ๐‘‹ is either Use to grant the right creditworthy or not) to visualize the read direction and to evaluate, Commission to grant the right to publish a third party, which could either be Alice, Bob or some results without approval, Appr to grant the right to pub- smart contract that start the borrowing transaction at lish the results. We further use Publish(๐ต, ๐‘ƒ ) to spec- some time point which gets added as fact to the contract ify that ๐ต has published the results of product ๐‘ƒ and (marked as blue) and derives all other facts given in the Comment(๐ต, ๐‘ƒ ) to specify that ๐ต has made a comment box according to the rules of the program. on the evaluation of product ๐‘ƒ , Remove(๐ต, ๐‘ƒ ) to spec- ify that ๐ต has removed the content and Violation(๐ต, ๐‘ƒ ) to specify that ๐ต has violated the license for product ๐‘ƒ 5. Case Study and OblRemove(๐ต, ๐‘ƒ ) to specify that ๐ต is obliged to remove the license. In the previous section, we introduced DatalogMTL smart The smart contract is then defined as a quadruple contracts with a simple example. In this section, we study (๐‘, ฮ , ๐ท, ๐ด), where ๐‘ is some unique identifier such as the use of DatalogMTL together with two real-world LicenseAgreement, the dataset ๐ท is empty, the activa- examples. We first consider a widely discussed example tors are given by the set of atoms {Publish, Comment, in the area of logic-based smart contracts, and then we GrantAppr , GrantCommission, GrantUse, Remove} and the program ฮ  is given by the following rules, where discuss on how to utilize DatalogMTL for writing a smart we omit the terms in the rules for readability: contract for a crypto token. GrantAppr โ†’ โŠž[0,โˆž) GrantAppr (1) Publish, ยฌGrantAppr โ†’ OblRemove (2) Example 5.2. Let us consider the write operations of the OblRemove, ยฌRemove, Ethereum ERC20 specification, which are in total three ยฌ โŠŸ[0 ,24 ] OblRemove โ†’ โŠž[1,1] OblRemove (3) methods: โŠŸ[0,24] OblRemove โ†’ Violation (4) โ€ข Transfer. Party ๐ด transfers amount ๐‘‹ to party Comment, ยฌGrantAppr โ†’ Violation (5) ๐ต. Such a transfer is only allowed if the current GrantCommission โ†’ GrantAppr (6) balance of ๐ด is bigger or equal to ๐‘‹. GrantUse, ยฌViolation โ†’ โŠž[1,1] GrantUse (7) โ€ข Approve. Party ๐ด allows party ๐ต to withdraw amount ๐‘‹. Rule (1) specifies that an approval holds forever. Rules โ€ข TransferFrom. Party ๐ต transfers amount ๐‘‹ from 2-4 match clause (2). Rule 2 states that if the results are party ๐ด to party ๐ถ. Such a transfer is only al- published, but they are not approved, then the licensee lowed if the current balance of ๐ด and the approval is obliged to remove the results. Rule (3) specifies the value for ๐ต from ๐ด are bigger or equal to ๐‘‹. 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 initial balance, which is assigned to one or more peo- violation occurred. ple, in this case 2000 tokens are assigned to Alice, 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 com- paring 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 TranF (๐ด, ๐ถ, ๐‘‹, ๐ต), ๐‘‹ โ‰ค ๐‘Œ โ†’ Tran(๐ด, ๐ถ, ๐‘‹) (4) reach a certain state. For example, it can be used to state 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(๐ด, _, _), Publish, ยฌ [0,โˆž) GrantUse โ†’ โŠฅ ยฌVTran(_, ๐ด, _) โ†’ โŠž[1,1] Bal(๐ด, ๐‘Œ ) (6) App(๐ด, ๐ต, ๐‘Œ ), 5.2. ERC20 Token ยฌVTran(๐ด, _, _) โ†’ โŠž[1,1] App(๐ด, ๐ต, ๐‘Œ ) (7) In this case study, we analyse how an Ethereum ERC20 App(๐ด, ๐ต, ๐‘Œ ), token contract [18] can be formalized in DatalogMTL. VTran(๐ด, _, _), The standard provides some read-only functions, such as ยฌTranF (๐ด, _, _, ๐ต) โ†’ โŠž[1,1] App(๐ด, ๐ต, ๐‘Œ ) (8) what is the current balance of a user, which we do not consider in the example, as just the atoms of the program Rule (1) verifies whether the balance of party ๐ด is enough have to be accessed. In the following, we focus on the for the transfer. Rules (2) and (3) apply a verified transfer functions, which change the state of the contract. The by reducing and increasing the balance of the participat- goal of these functions is to specify when a transfer of ing parties. Rule (4) applies the third-party transfer by tokens between two parties is allowed and how a transfer checking whether the party is allowed to transfer the affects the balance of the parties. 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. Maffi, 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 In- formally 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 con- vators. 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 mod- discussing 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 lan- Lecture Notes in Computer Science, Springer, 2016, guage for data analysis, SIGMOD Rec. 48 (2019) pp. 167โ€“183. 6โ€“17.