=Paper=
{{Paper
|id=Vol-3791/paper17
|storemode=property
|title=Towards FATEful Smart Contracts
|pdfUrl=https://ceur-ws.org/Vol-3791/paper17.pdf
|volume=Vol-3791
|authors=Luigi Bellomarini,Marco Favorito,Eleonora Laurenza,Markus Nissl,Emanuel Sallinger
|dblpUrl=https://dblp.org/rec/conf/dlt2/BellomariniFLNS24
}}
==Towards FATEful Smart Contracts==
https://ceur-ws.org/Vol-3791/paper17.pdf
Towards FATEful Smart Contracts
Luigi Bellomarini1 , Marco Favorito1 , Eleonora Laurenza1 , Markus Nissl2 and
Emanuel Sallinger2,3
1
Bank of Italy, Italy
2
TU Wien, Austria
3
University of Oxford, UK
Abstract
Achieving fair, accountable, transparent, and ethical decentralized finance requires activating enabling properties
at the level of smart contracts, the executable scripts at its basis. In this vision paper, a joint effort of the Central
Bank of Italy, TU Wien, and the University of Oxford, we leverage the vast amount of experience in this sense
from the database community and propose a logic-based reasoning framework that captures smart contracts
as a set of rules in DatalogMTL, a temporal language for querying databases. We show how the theoretical
underpinnings of the reasoning of DatalogMTL convey important properties to the approach and show it in
action on industrial cases of relevance to a central bank.
Keywords
Smart contracts, DatalogMTL, FATE principles
1. Introduction
The Artificial Intelligence and database communities are experiencing a growing infusion of the
FATE (Fairness, Accountability, Transparency, Ethics) [1]. These principles are gaining prominence,
drawing attention to the non-functional requirements of everyday AI-assisted and data-driven decision-
making and catalyzing the discussion around regulatory bodies. Unfortunately, the same level of
attention to these high-level concerns is not mirrored in developer circles, and recent studies underscore
the scant regard machine learning developers have shown for FATE concerns in machine learning
applications [2, 3].
FATE and DeFi. We see similar patterns emerging when assessing developersโ awareness of FATE
concerns within the industrial realm of Decentralized Finance (DeFi). DeFi entails financial transactions
devoid of intermediaries, instead relying on software modules executed on a decentralized public
ledger [4]. At the core of DeFI is the notion of smart contracts [5], which are machine-readable and
executable agreements that establish and enforce the binding terms for the parties involved.
Supporting FATE. In the AI and data world, social forces have been effective in supporting FATE,
for example, by means of third-party audits of the algorithms, either conducted by experts or by
everyday users. As recently highlighted by Hong in CACM [1], prominent examples can be found in
the fights against the racial bias of face-recognition systems [6], and commercial gender disparities in
photo cropping or credit card algorithms [7]. These audits, spurred by social forces and the scientific
community, have provided regulators with positive guidance.
In contrast to AI, DeFi boasts a substantial theoretical transparency advantage, thanks to its open-
access code and the ability for anyone to inspect smart contract data on a public ledger. However,
enforcing policies in a decentralized context remains an incredibly challenging task. The praiseworthy
goal of establishing standards, taxonomies, compliance measures, quality controls, and upholding
ethical principles [8] can benefit from robust support from the social forces in the monitoring and
6th Distributed Ledger Technology Workshop, May 14โ15, 2024, Turin, Italy
Envelope-Open luigi.bellomarini@bancaditalia.it (L. Bellomarini); marco.favorito@bancaditalia.it (M. Favorito);
eleonora.laurenza@bancaditalia.it (E. Laurenza); nissl@dbai.tuwien.ac.at (M. Nissl); sallinger@dbai.tuwien.ac.at (E. Sallinger)
Orcid 0000-0001-6863-0162 (L. Bellomarini); 0000-0001-9566-3576 (M. Favorito); 0000-0002-2786-8163 (E. Laurenza);
0000-0001-8196-5688 (M. Nissl); 0000-0001-7441-129X (E. Sallinger)
ยฉ 2024 Copyright for this paper by its authors. Use permitted under Creative Commons License Attribution 4.0 International (CC BY 4.0).
The views and opinions expressed in this paper are those of the authors and do not necessarily reflect the official policy or position of Banca dโItalia.
CEUR
ceur-ws.org
Workshop ISSN 1613-0073
Proceedings
enforcement of such policies. However, this must align with the specific technical attributes of these
smart contracts. Yet, smart contracts have been criticised within the community due to their overly
complex business logic, and limited explainability, resulting in a lack of transparency. Furthermore, they
often prove challenging to describe and communicate, rendering them less user-friendly, particularly
for non-technical users [9, 10, 11].
A Knowledge Representation and Reasoning (KRR) approach to smart contracts. In the area
of deductive AI and ontological reasoning on databases, logic-based approaches built on top of KRR
formalisms are gaining increasing attention in industrial settings, with many successful financial
applications [12, 13, 14]. Modern logical languages manage to strike a good balance between expressive
power and computational complexity, resulting in compact and efficiently executable formalizations of
complex domains, for instance, being able to capture SPARQL under OWL 2 entailment regimes [15]
and so enabling ontological reasoning. The declarative paradigm sustains simplicity, transparency,
compactness, and understandability of code, which becomes algorithm-independent and closer to
the high-level specifications, policies, and standards. The well-defined semantics of KRR languages
fosters non-ambiguity, ease of use for non-technical users, and correctness. The intrinsic step-by-step
nature of logical reasoning is conceptually close to notions of explainability and thus supports decision
transparency.
The thesis of this vision paper is that a KRR framework for smart contracts that addresses FATE by design
is both theoretically and practically viable. For the theory, we show that, by building on the underpinnings
of logic-based reasoning, the features important to achieving FATE desiderata can be obtained and rigorously
justified. In terms of application, we show that our framework is adaptable to serve as both an interpreted
and a compiled execution mode for real-world contracts.
Contributions to industrial advances. In recent industrial EDBT work done by the Central Bank
of Italy [16], they started to investigate the possibility of encoding complex smart contracts in Data-
logMTL [17, 18, 19], a temporal extension of the Datalog language [20] of databases. They obtained
promising results, which highlighted the potential of a KRR approach in the specific case of a derivative
contract. In this work, a joint effort of the Central Bank of Italy, TU Wien, and the University of Oxford,
we aim to go substantially further by: (i) proposing a full-fledged and general framework for
smart contracts that sustains FATE concerns; (ii) leveraging the vast amount of experience from the
database community to achieve enabling properties; (iii) a preliminary proposal of compilation
from DatalogMTL๐ programs to equivalent Solidity contracts (iv) using our framework to study and
implement proof of concepts for many smart contracts where FATE is a core desideratum of a
central bank, namely, tokenisation, peer-to-peer transactions, security settlement, decentralized financial
markets, and smart legal contracts.
2. Overview of the framework and related work
We use a form of declarative logical object-oriented approach and encode the behaviour of a class
of smart contracts as a set ฮฃ of reasoning rulesโor programsโworking on a database ๐ท of tem-
poral facts. A temporal fact of ๐ท is such that it holds in a given time interval, for example,
price(123, 2)@[2023-09-01,2023-09-02] defines the price 2 for the asset 123 in a two-day interval.
To model the rules of ฮฃ, we introduce DatalogMTL๐ , a variant of DatalogMTL [17, 18, 19] with features
of practical utility. A smart contract is then an instance of a smart contract class, whose time-dependent
status is represented as a database ๐ท of temporal facts. Instances are stateful objects and the contract
execution consists in invocations, akin to method calls, that are carried out by the involved parties.
Calls result in updates to the status ๐ท through the addition of new facts. The semantics of a call is
operationally described as the application of the rules of ฮฃ (denoted as ฮฃ(๐ท)) to the temporal facts of ๐ท,
extended with call-specific facts.
DatalogMTL๐ rules are sets of headโbody logic implications where the body is a conjunction of atoms
and the head is an atom. As a general guideline, whenever the body of a rule is satisfied by a conjunction
of facts in ๐ท at a point in time ๐ก, the evaluation of the rule triggers the insertion in ๐ท of a new fact for
Figure 1: Overview of the DatalogMTL๐ framework for smart contracts.
the head atom, holding at ๐ก. For example, the rule โposition(๐ฅ, ๐ค) โ buy(๐ฅ, ๐, ๐), price(๐, ๐), ๐ค = ๐ โ ๐โ
states that, for every point in time ๐ก, the position ๐ค of a trader ๐ฅ that buys an amount ๐ of an asset ๐ of
price ๐ is obtained as ๐ โ ๐. So, if ๐ท contains the price fact price(123, 2) and buy(0๐ฅ241๐น , 123, 12), both
holding at [2023-09-01,2023-09-02], a new position(0x241F, 24) holding in the same time interval will
be added to ๐ท.
In DatalogMTL๐ , temporal operators can be used to either modify the temporal binding of body
atoms to facts of ๐ท, or to alter the temporal validity of the generated facts. For instance, an expression
of the form โฆ โ [0,1d] position(๐ฅ, ๐ค) in the body holds at a point in time ๐ก, if the trader ๐ฅ had at least an
open position ๐ค in the interval [๐ก โ 1, ๐ก], while an expression of the form โ[0,1d] position(๐ฅ, ๐ค) in the
head, states that the position will be open in the interval [๐ก, ๐ก + 1] for every ๐ก. In the following, we show
a smart contract class defining a simple financial market:
๐
1โถ
๐
2โถ โโ
accepted($sender, ๐ฆ) โ #open(๐ฆ), ยฌmarketClosed.
โposition(๐ฅ, ๐ฆ, ๐) โ accepted(๐ฅ, ๐ฆ), price(๐), ๐ = ๐ฆ โ ๐.
๐
3โถ return(x, g), โposition(๐ฅ, ๐ฆ, 0) โ #close(), price(๐), position($sender, ๐ฆ, ๐), ๐ = ๐ฆ โ ๐ โ ๐.
At a specific point in time in which the market is not closed, a trader tries to open a position by investing
an amount ๐ฆ (Rule ๐
1). The constant $๐ ๐๐๐๐๐ is a call-level variable that at runtime binds to the invoking
โ
trader. When the transaction is accepted (Rule ๐
2), the position of the trader ๐ฅ on the amount ๐ฆ is
updated by multiplying by the current price ๐. The โ operator stands for a new future temporal validity
of the position fact. Finally, when the position is closed (Rule ๐
3), the final profit ๐ is computed based
on the current price.
Execution modes. From a practical perspective, our framework implements ฮฃ(๐ท) by enabling three
execution alternatives, each offering specific properties, as reported in Figure 1: (i) on-reasoner execution:
the rules are applied natively by a reasoning system supporting DatalogMTL or DatalogMTL๐ such as
Temporal Vadalog [21] or MeTeoR [22]; (ii) on-chain execution: the DatalogMTL๐ programs are verifiably
translated into the language of a target system, for instance, Solidity [23] or Bitcoin Script [24] and
executed within the target systems; (iii) off-chain execution, the rules are applied with an on-reasoner
execution with persistent effects on a blockchain and cryptographically verifiable computation.
The expert intention is substantiated as a natural language (NL) contract or directly encoded in a
DatalogMTL๐ program ฮฃ, and the use of large language models (LLM) can bridge the gap between the
natural language specification of the contract and the encoding of its DatalogMTL๐ version [25].
In the on-reasoner execution mode, to evaluate ฮฃ, reasoners use variants of the chase procedure [26]
specialized for the temporal extensions [27]. They offer full explainability of the produced facts as a side
effect of the inference process of the chase. Also, they are suited to be used for simulation and runtime
verification purposes (see Section 5) as step-by-step debugging can be emulated by incrementally adding
facts to ๐ท and monitoring the results entailed by the application of ฮฃ. On the other hand, the execution
relies on a trusted centralized system.
Conversely, on-chain execution offers a trustless paradigm, only requiring that the user acknowledges
the translation of the DatalogMTL๐ code into the target language, which can be verified through open-
sourced translators (see Section 4). This trustlessness is underpinned by the validation properties
ensured by the distributed consensus protocol embraced by the blockchain, guaranteeing the integrity
of the mined blocks. What is more, on-chain execution is characterized by its timeliness, as results are
promptly included in the first mined block.
However, on-chain execution comes with a high cost and is ill-suited for complex applications. In
contrast, off-chain execution is widely regarded as a practical and efficient alternative, and there is a large
body of related work such as state-channels [28], Plasma [29], and Zero-Knowledge Rollups [30]. In
particular, specific protocols have been proposed, that help attest the integrity of off-chain computation
(i.e., verifiable computation), such as ZK-SNARK [31] and ZK-STARK [32]. Towards this direction, the
construction of specialized virtual machines compiling succinct ZK proofs for DatalogMTL๐ executions
is envisaged here, but beyond the scope of this vision paper and a matter of future work.
Quality. Investigating and assessing the properties of a smart contract stands as a paramount concern for
regulators, financial institutions, and central banks. Beyond chase-based explainability, our framework
establishes a twofold path for the scrutiny and validation of smart contracts: during static compile-time
and dynamically at runtime. For compile-time checks, as contracts are specified in logic, dedicated
tools can be developed as future work, that apply formal methods for logical verification, with good
decidability expectations in the presence of bounded input sources [33]. In contrast, acquiring dynamic
checks in our framework is a relatively straightforward process, involving the real-time querying of
the system to examine outcomes dependent on ฮฃ and ๐ท. We believe that these dynamic checks hold
significant promise for easy integration by the aforementioned stakeholders into their monitoring and
compliance tools. From a technical standpoint, we represent dynamic checks as temporal conjunctive
queries.
For instance, a possible validation for our smart contract in the financial market example above
involves inquiring whether, in the past year, a user has repeatedly accumulated losses as a result of
closing positions. This may indicate a deficiency in the associated process checks and so a compliance
problem. We employ a combination of the โ operator from DatalogMTL๐ , which signifies the persistent
continuity of its argument in the past, and the โฆ โ operator, indicating the occurrence of a fact within a
specified past interval, as we have seen:
โ [0,1m] (#close, return(๐ฅ, ๐), ๐ < 0).
๐ โ โ[0,1y] โฆ
Termination and Complexity. Fact entailment in DatalogMTL is a decidable task, in particular
PSPACE in data complexity [18]; therefore we have guaranteed termination and guaranteed computational
complexity. Moreover, the rules modelling real-world smart contracts need to allow for the derivation of
facts into present and future time points, while the propagation towards the past is almost never required.
Under this condition, the set ฮฃ belongs to the forward-propagating fragment, namely, DatalogMTLFP
[18], for which a finite representation of infinite models is always possible [19]. It is important to point
out that in DatalogMTL the use of arithmetic and recursion can, in general, lead to undecidability [34]
and a comprehensive study of arithmetic in DatalogMTL has not been provided yet. However, our
framework conditions the activations of the rules on the specific smart contract functions being called,
which reduces the cases of potentially harmful recursion.
3. Industrial use cases
We now show three smart contracts of industrial relevance to see our framework in action.
ERC-20. The ERC-20 [35] is a well-known and widely adopted Token Standard that implements an API
for tokens within smart contracts. The following DatalogMTL๐ smart contract implements a simple
โโ
ERC-20 contract with a fixed supply ๐.
๐
1โถ โtotalSupply(๐), โbalanceOf ($sender, ๐) โ #init(๐).
๐
2โถ
๐
3โถ โ โ โbalanceOf ($sender, 0) โ ยฌbalanceOf ($sender, ๐ ), #create().
โbalanceOf ($sender, ๐ต๐ โ ๐ด),
โbalanceOf (to, ๐ต๐ + ๐ด) โ balanceOf ($sender, ๐ต๐ ), balanceOf (to, ๐ต๐ ),
๐ต๐ โฅ ๐ด, #transfer(to, ๐ด).
โ โ
Rule ๐
1 initializes the smart contract state by adding the facts โtotalSupply(๐) and
โbalanceOf ($sender, ๐). Note that using the โ operator allows to overwrite the balance in
case of a transfer. Rule ๐
2 allows the sender to initialize a balance, if not already done earlier. Rule
๐
3 implements the โtransferโ function from the sender address $sender to the recipient address to
of amount ๐ด. Atoms of the form balanceOf (address, ๐ ) in the body are used to query the balance
๐ of address (a common pattern in logic programming), the condition ๐ต๐ โฅ ๐ด imposes that there is
enough balance from the sender account to complete the transfer, and the head of the rule uses the โ
to update the balances accordingly. We omitted the allowance mechanism and the transferFrom and
โ
approvefunctions.
Securities settlement. One of the most useful applications of DLT in finance is their ability to provide
an automated coordination mechanism of financial transactions in which there are trust issues among
participants [36]. In particular, this can be an enabler for DLT-based cross-border payments, foreign
exchanges, and Central Bank Digital Currencies [37, 38]. Here we consider a scenario in which securities
are โtokenizedโ, i.e., when securities are represented as digital tokens [39]. If the security tokens and the
cash tokens exist on the same ledger, then an atomic settlement smart contract can be used to coordinate
clearing and settlement. In the following, we present a formalization in a DatalogMTL๐ smart contract of
the atomic settlement, showing the flexibility of our DatalogMTL๐ framework. We have a DatalogMTL๐
ERC-20 contract ๐ฉerc20 that handles both types of tokens. Note that these are simplified examples,
as real-world usage might require potentially more complex logic to handle different scenarios and
compliance requirements. #๐ฉ (๐๐).function(arg 1 , โฆ ) represents a cross-contract interaction.
๐
1โถ โcashTokCt(id ๐ ), โsecTokCt(id ๐ ),
โ โ
โbuyer(addr ๐ ), โseller(addr ๐ ), โprice(๐),
โqty(๐), โcashSent(0), โsecSent(0) โ #init(id ๐ , id ๐ , addr ๐ , addr ๐ , ๐, ๐)
โ
๐
2โถ #๐ฉerc20 (id ๐ ).transferFrom(addr ๐ , $this.addr, ๐),
โcashSent(๐) โ $sender = addr ๐ , buyer(addr ๐ ), price(๐),
cashTokCt(id ๐ ), #submitCash().
โ
๐
3โถ #๐ฉerc20 (id ๐ ).transferFrom(addr ๐ , $this.addr, ๐),
โsecSent(๐) โ $sender = addr ๐ , seller(addr ๐ ), qty(๐),
secTokCt(id ๐ ), #submitSecurity(id ๐ ).
๐
4โถ #๐ฉerc20 (id ๐ ).transferFrom($this.addr, addr ๐ , ๐),
โ โ
#๐ฉerc20 (id ๐ ).transferFrom($this.addr, addr ๐ , ๐),
โcashSent(0), โsecSent(0) โ $sender in {addr ๐ , addr ๐ }, cashSent(๐), secSent(๐),
buyer(addr ๐ ), seller(addr ๐ ), #settle().
๐
5โถ #๐ฉerc20 (id ๐ ).transferFrom($this.addr, addr ๐ , ๐),
โ โ
#๐ฉerc20 (id ๐ ).transferFrom($this.addr, addr ๐ , ๐),
โcashSent(0), โsecSent(0) โ $sender in {addr ๐ , addr ๐ }, cashSent(๐), secSent(๐),
buyer(addr ๐ ), seller(addr ๐ ), #cancel().
Rule ๐
1 initializes the state of the contract: it defines the buyerโs and sellerโs addresses, the expected
cash amount ๐ at which the security quantity ๐ will be sold. Moreover, the contract initializes the
locked amount of cash and security tokens to 0 and stores the ERC-20 contract identifiers for each of
the two token types. Note how the call predicates get propagated to the head and saved into the status
database. Rule ๐
2 defines the function submitCash that allows the buyer to lock the cash token to settle
the transaction. Rule ๐
3 is analogous to Rule ๐
2, but for the seller account and the security tokens
(function submitSecurity). Note that both Rules ๐
2 and ๐
3 assume that the token owners have given
allowances to $this.addr. Rule ๐
4 implements the settlement rule, which gets activated as soon as both
buyer and seller submit their tokens and settles the trade between the buyer and the seller. Rule ๐
5
restores the locked funds from both the buyerโs and sellerโs side and sends the tokens back to their
original owner. Note that only the buyer (resp. the seller) can trigger the function submitCash (resp.
submitSecurity). and that both of them are authorized to cancel or settle the trade. The trigger atoms
#๐ฉerc20 (๐๐๐ ).transferFrom allow to interact with the ERC-20 contracts of the token types involved in the
transaction.
Legal Recourse. A legal recourse against a contract refers to the options available to parties when
a contract is breached or when there is a dispute regarding the terms or performance of the contract.
When a contract is executed via a smart contract, blockchain immutability poses a significant challenge
when altering or amending the contract effects once its terms have been carried out. The use of
declarative languages, which enhances transparency, helps mitigate this issue by minimizing the
ambiguity inherent in natural language, thereby reducing the likelihood of legal disputes [40]. However,
unforeseen events such as force majeure, varying jurisdictional interpretations, and contract bugs may
necessitate adjustments to the contract outcome, even after the transaction has been finalized. Moreover,
it is important to distinguish between enabling legal recourse in a contract and appointing an arbiter, as
an actor in the contract itself, who makes decisions regarding the transaction outcome in cases where
the involved parties fail to reach an agreement. Legal recourse is typically considered a post-transaction
event, which may also involve the arbiter and occurs after completing the transaction.
๐
1โถ โpartA(addr ๐ด ), โpartB(addr ๐ต ),
โarbiter(addra ), โcontractId(id ๐ ) โ #init(addr ๐ด , addr ๐ต , addra , id ๐ )
๐
2โถ #Contract(๐ฅ)[addr ๐ด , addr ๐ต ] โ contractId(๐ฅ), partA(addr ๐ด ), partB(addr ๐ต ).
๐
3โถ balanceFlowRec(๐ฅ1โ๐ฅ2, ๐ฆ1โ๐ฆ2, ๐ง1โ๐ง2) โ โฆ โ [1,1] balance(๐ฅ1, ๐ด), balance(๐ฅ2, ๐ด), โฆโ [1,1] balance(๐ฆ1, ๐ต), balance(๐ฆ2, ๐ต),
โ [1,1] balance(๐ง1, ๐ถ), balance(๐ง2, ๐ถ), partA(๐ด), partB(๐ต), contractId(๐ถ).
โฆ
๐
4โถ #Contract(๐ฅ).undoAndRefund(๐ด) โ partA(๐ด), arbiter(๐ฅ, $sender), contractId(๐ฅ), #legalOutcomeA().
๐
5โถ #Contract(๐ฅ).undoAndRefund(๐ต) โ partB(๐ต), arbiter(๐ฅ, $sender), contractId(๐ฅ), #legalOutcomeB().
๐
6โถ #Contract(๐ฅ).undoAndCancel(๐ด, ๐ต) โ partA(๐ด), partB(๐ต), arbiter($sender), contractId(๐ฅ), #legalOutcomeCancel().
Rule ๐
1 initializes the contract; Rule ๐
2 initializes the insured contract; Rule ๐
3 manages the balances
of the parties involved; Rule ๐
4 (resp. ๐
5) handles the case when the recourse resolves in favour
of party ๐ด (resp. ๐ต); and Rule ๐
6 undoes the effects of the insured contract. The trigger atoms
#Contract(๐ฅ).undoAndRefund allow to interact with the ensured contract.
4. Compilation in Solidity
While a complete and detailed design of a compilation technique of DatalogMTL๐ contracts to Solidity
smart contracts is out of this paperโs scope, in this section, we give the intuition of a comprehensive
approach for the translation and exemplify by showing meaningful patterns.
Types and Variables. Predicates occurring in a DatalogMTL๐ program belong to either a status schema
๐ฎ, a transient schema ๐ฏ, or a function schema โฑ. Generated atoms whose predicates are in ๐ฎ, since they
persist across chase computations (i.e., VM function calls) in the status database ๐ท, are mapped into
contract state variables and data structures; transient atoms are mapped in local function data, and
function or trigger atoms are used to generate Solidity functions. If the predicate is unary, the atom
is mapped to a variable, while predicates for two or more arguments are mapped in Solidity structs.
There might be user-defined exceptions, e.g., balanceOf can be compiled into a map. Furthermore,
each position of a predicate must be mapped to a Solidity type (e.g., the argument of supply and other
amounts to type โuint256 โ, account addresses, such as the argument in buyer and seller above, are
mapped to the type โaddress โ). The compilation process must analyze the program and check whether
the provided type mapping is consistent. The occurrence of special call variables (e.g., $sender and
$this.balance) are translated into msg attributes (msg.sender and this.balance , respectively).
Functions. The rules with the #init trigger atom are converted into constructors, and each variable
in the argument list is converted into a constructor argument, typed according to the specified type
1 contract SimpleERC20Contract { 14
2 uint256 immutable t o t a l S u p p l y ; 15 f u n c t i o n t r a n s f e r ( address _to , uint256 _A ) p u b l i c {
3 mapping ( address => uint256 ) p u b l i c b a l a n c e O f ; 16 uint256 Bs = b a l a n c e O f [ msg . sender ] ;
4 17 uint256 Br = b a l a n c e O f [ t o ] ;
5 c o n s t r u c t o r ( uint256 _S ) { 18 i f ( ! ( Bs >= _A ) ) { r e v e r t ( ) ; }
6 t o t a l S u p p l y = _S ; 19 b a l a n c e O f [ msg . sender ] = Bs โ _A ;
7 b a l a n c e O f [ msg . sender ] = _S ; 20 b a l a n c e O f [ _ t o ] = Br + A ;
8 } 21 }
9 22 }
10 function c r e a t e ( ) public { 23
11 i f ( b a l a n c e O f [ msg . sender ] ! = 0 ) { r e v e r t ( ) ; } 24
12 b a l a n c e O f [ msg . sender ] = 0 ; 25
13 } 26 }
Figure 2: The Solidity code generated from the ERC-20 DatalogMTL๐ program example.
mapping. Similarly, the other trigger rules (i.e., with a trigger predicate in the body) are converted into
functions; if there is more than one rule with the same trigger predicate in the body, we use function
overloading to distinguish the different behaviours in the Solidity code. Generated head atoms of
the form โ๐(t) are translated into the initialization of immutable variables, while โ are translated
into variable updates. Predicates that occur in temporal operators with an arbitrary time interval,
โ
โ [๐ก1 ,๐ก2 ] ๐(t), correspond to variables that must be read via internal
such as โ[๐ก1 ,๐ก2 ] ๐(t), โ[๐ก1 ,๐ก2 ] ๐(t) and โฆ
getter functions, which return the right value depending on the timestamp of the current function
call. Depending on the time intervals for a specific predicate, a data structure that indexes its values
appropriately, e.g., by intervals in which certain values hold, might be needed. For example, if the only
temporal operator that appears in front of a predicate is โฆ โ [0,1] , we only need to remember the value of
the associated variable in the previous time step.
Control flow. Advanced queries (e.g., nested temporal operators, joins, etc.) on the current contract
state database might require advanced program synthesis techniques to generate gas-efficient on-chain
computation. Other expressions in the body of a rule (such as comparisons, equality check conditions,
negated atoms, atoms with free variables) correspond to control flow constructs in Solidity (i.e., if-then-
else clauses, error handling). The parsing of the DatalogMTL๐ must consider the programโs derivation
paths starting from each trigger rule.
Figure 2 shows the output of the compilation process over the example DatalogMTL๐ program for
the ERC-20 token. The predicates are partitioned as follows: ๐ฎ = {totalSupply, balanceOf }, ๐ฏ = {} and
โฑ = {#init, #create, #transfer}. The argument of the totalSupply predicate is mapped to the uint256
type, and balanceOf is mapped to a mapping from address to uint256 , where the first argument of the
predicate is the key of the mapping. The constructor function is generated from ๐
1, while create and
transfer are generated from ๐
2 and ๐
3, respectively. Note that the definition of the create function
is necessary for the DatalogMTL๐ semantics but pleonastic in Solidity since the values of mapping
are initialized to default values of their type; in particular, uint256 defaults to 0. The condition on
the available balance in the transfer function is negated and, in case the condition is satisfied, the
transaction is reverted.
Discussion on Fees. In the context of smart-contract-enabled blockchain, it is of interest to make a
smart contract as efficient as possible in using computational resources (i.e., space and time), which
translates into saving as many fees as possible. Therefore, it seems natural to ask ourselves whether we
can estimate the execution cost of a smart contract specified in DatalogMTL๐ . To get an estimate on
how much it costs to execute a DatalogMTL๐ smart contract, we can rely on the combined complexity
[41] of DatalogMTL๐ , given the size of the database (or its relevant subset) and the size of the specific
program we are analyzing. Note, however, that such an estimate can be quite loose since, ultimately,
the target VM has a procedural paradigm of execution, and the efficiency of the procedural program
will depend on the quality of the smart contract generator. Anyway, it is reasonable to claim that if
the smart contract generator is good enough, the final cost of the execution cannot be greater than the
complexity estimate over the DatalogMTL๐ program evaluation.
5. Formal Verification
In this section, we argue that our framework can enable formal verification of smart contracts written
in DatalogMTL๐ . According to the taxonomy proposed by Tolmach et al. [42], our contract modeling
approach can be ascribed to the contract-level category, which is concerned with the high-level behavior
of a smart contract under analysis and without considering technical details of its implementation
and execution. In our framework, the correctness of the smart contractโs on-chain behaviour and
execution on the target platform primarily follows on the correctness of the compilation step and on
the correctness of the DatalogMTL๐ program.
An example of how formal properties can be verified is by additional program rules that formalize
invariants in the DatalogMTL๐ language. These are formalized using rules of the form โฅ โ ๐ด1 , โฆ , ๐ด๐ ,
meaning that, if all expressions ๐ด1 , โฆ , ๐ด๐ are true (that is, the invariant does not hold), then the function
call that triggered that rule must be reverted. These rules are compiled into assert instructions and
can be seen as a runtime validation technique that rejects all transactions that violate the invariants, as
in [43]. For example, in the ERC-20 smart contract, we might add some invariant conditions that must
be true at any time during the lifetime of the smart contract, such as:
โขThe sum of user balances is equal to totalSupply [44] (the operator msum is an aggregation operator
that computes the sum, see [45, 27])
actualTotalSupply(msum(โจ(๐ต)โฉ) โ balanceOf (_, ๐ต).
โฅ โ actualTotalSupply(๐1 ), totalSupply(๐2 ), ๐1 ! = ๐2 .
โขThe sums of sender and receiver balances before and after the transfer are equal [46]:
โ [1,1] #transfer(), address(๐ก๐), โฆ
โฅ โโฆ โ [1,1] balanceOf ($sender, ๐ต๐ ), โฆ
โ [1,1] balanceOf (๐ก๐, ๐ต๐ ),
balanceOf ($sender, ๐ต๐ โฒ ), balanceOf ($sender, ๐ต๐โฒ ), ๐ต๐ + ๐ต๐ = ๐ต๐ โฒ + ๐ต๐โฒ .
More sophisticated formal verification approaches could be developed specifically for DatalogMTL pro-
grams. For example, we could extend the approach for program verification based on using Constrained
Horn Clauses (CHCs) [47, 48], already used by the Solidity Compilerโs Model Checker (SolCMC) [49], to
support also temporal operators.
6. Conclusion
This preliminary work proposes a framework for expressing and evaluating smart contracts, focusing on
improving the explainability and transparency of traditional smart contract development. We achieve
this by building on decades of research in KRR, particularly in declarative logic-based programming,
leveraging the expressive power of DatalogMTL. Inspired by a recent application of such formalism
for modelling smart contracts [50, 16], we generalize those approaches and develop a foundational
framework which supports the formalization and evaluation of arbitrary smart contracts. While in this
paper we focused more on the vision and its industrial applications in the financial sector, we can already
foresee many research avenues as future works. First, we aim to develop novel techniques (e.g., zero-
knowledge techniques for off-chain execution) and implementations for realizing each execution mode.
Next, it would be interesting to investigate the impact of developing smart contracts in DatalogMTL๐ ,
in terms of ease of use, explainability, and code quality. Finally, we want to devise and apply formal
verification techniques for DatalogMTL๐ smart contracts.
References
[1] J. I. Hong, Teaching the fate community about privacy, Commun. ACM 66 (2023) 10โ11.
[2] ร. A. Cabrera, E. Fu, D. Bertucci, K. Holstein, A. Talwalkar, J. I. Hong, A. Perer, Zeno: An interactive
framework for behavioral evaluation of machine learning, in: CHI, ACM, 2023, pp. 419:1โ419:14.
[3] T. Li, Y. Agarwal, J. I. Hong, Coconut: An IDE plugin for developing privacy-friendly apps, Proc.
ACM Interact. Mob. Wearable Ubiquitous Technol. 2 (2018) 178:1โ178:35.
[4] E. Napoletano, B. Curry, What is defi? understanding decentralized finance, http://bitly.ws/xd7Y,
2021. Last accessed on 2022-11-28.
[5] I. Swaps, D. Association, Legal guidelines for smart derivatives contracts: the isda master agree-
ment, 2019.
[6] P. E. Naeini, J. Dheenadhayalan, Y. Agarwal, L. F. Cranor, An informative security and privacy
โnutritionโ label for internet of things devices, IEEE Secur. Priv. 20 (2022) 31โ39.
[7] J. Buolamwini, T. Gebru, Gender shades: Intersectional accuracy disparities in commercial gender
classification, in: FAT, volume 81 of Proceedings of Machine Learning Research, PMLR, 2018, pp.
77โ91.
[8] Bank of Italy, Public consultation on the working document relating to phase one of the research
project on smart contracts, https://bit.ly/3xQKRL8, 2023. [Online; accessed 3-May-2024].
[9] G. Ciatto, R. Calegari, S. Mariani, E. Denti, A. Omicini, From the blockchain to logic programming
and back: Research perspectives, in: WOA, 2018, pp. 69โ74.
[10] M. Li, J. Weng, A. Yang, J. Weng, Y. Zhang, Towards interpreting smart contract against contract
fraud: A practical and automatic realization, Cryptology ePrint Archive, Paper 2020/574, 2020.
URL: https://eprint.iacr.org/2020/574, https://eprint.iacr.org/2020/574.
[11] E. Regnath, S. Steinhorst, Smaconat: Smart contracts in natural language, in: 2018 Forum on
Specification and Design Languages (FDL), 2018, pp. 5โ16. doi:10.1109/FDL.2018.8524068 .
[12] A. Hogan, E. Blomqvist, M. Cochez, C. dโAmato, G. de Melo, C. Gutierrez, J. E. L. Gayo, S. Kirrane,
S. Neumaier, A. Polleres, R. Navigli, A. N. Ngomo, S. M. Rashid, A. Rula, L. Schmelzeisen, J. F.
Sequeda, S. Staab, A. Zimmermann, Knowledge graphs, CoRR abs/2003.02320 (2020).
[13] T. Baldazzi, L. Bellomarini, E. Sallinger, Reasoning over financial scenarios with the vadalog
system, in: EDBT, OpenProceedings.org, 2023, pp. 782โ791.
[14] L. Bellomarini, D. Fakhoury, G. Gottlob, E. Sallinger, Knowledge graphs and enterprise AI: the
promise of an enabling technology, in: ICDE, IEEE, 2019, pp. 26โ37.
[15] G. Gottlob, A. Pieris, Beyond SPARQL under OWL 2 QL entailment regime: Rules to the rescue,
in: IJCAI, 2015, pp. 2999โ3007.
[16] A. Colombo, L. Bellomarini, S. Ceri, E. Laurenza, Smart derivative contracts in datalogmtl, in:
EDBT, OpenProceedings.org, 2023, pp. 773โ781.
[17] S. Brandt, E. G. Kalayci, V. Ryzhikov, G. Xiao, M. Zakharyaschev, Querying log data with metric
temporal logic, J. Artif. Intell. Res. 62 (2018) 829โ877.
[18] P. A. Walega, B. C. Grau, M. Kaminski, E. V. Kostylev, Datalogmtl: Computational complexity and
expressive power, in: IJCAI, ijcai.org, 2019, pp. 1886โ1892.
[19] L. Bellomarini, M. Nissl, E. Sallinger, Query evaluation in datalogmtl - taming infinite query
results, CoRR abs/2109.10691 (2021).
[20] S. Ceri, G. Gottlob, L. Tanca, What you always wanted to know about datalog (and never dared to
ask), TKDE 1 (1989) 146โ166.
[21] L. Bellomarini, L. Blasi, M. Nissl, E. Sallinger, The temporal vadalog system, in: RuleML+RR,
volume 13752 of Lecture Notes in Computer Science, Springer, 2022, pp. 130โ145.
[22] D. Wang, P. Hu, P. A. Walega, B. C. Grau, Meteor: Practical reasoning in datalog with metric
temporal operators, in: AAAI, AAAI Press, 2022, pp. 5906โ5913.
[23] T. S. Authors, Solidity documentation, https://docs.soliditylang.org/en/v0.8.21/, 2023. [Online;
accessed 12-Oct-2023].
[24] B. Wiki, Script, https://en.bitcoin.it/wiki/Script, 2023. [Online; accessed 12-Oct-2023].
[25] T. Baldazzi, L. Bellomarini, S. Ceri, A. Colombo, A. Gentili, E. Sallinger, Fine-tuning large enterprise
language models via ontological reasoning, in: RuleML+RR, 2023.
[26] D. Maier, A. O. Mendelzon, Y. Sagiv, Testing implications of data dependencies, ACM Transactions
on Database Systems 4 (1979) 455โ468.
[27] L. Bellomarini, M. Nissl, E. Sallinger, Monotonic aggregation for temporal datalog, in: RuleML+RR
(Supplement), volume 2956 of CEUR Workshop Proceedings, CEUR-WS.org, 2021.
[28] A. Miller, I. Bentov, S. Bakshi, R. Kumaresan, P. McCorry, Sprites and state channels: Payment
networks that go faster than lightning, in: Financial Cryptography, volume 11598 of Lecture Notes
in Computer Science, Springer, 2019, pp. 508โ526.
[29] M. Harishankar, D. Akestoridis, S. V. Iyer, A. Laszka, C. Joe-Wong, P. Tague, Plasma go: A scalable
sidechain protocol for flexible payment mechanisms in blockchain-based marketplaces, CoRR
abs/2003.06197 (2020).
[30] Ethereum.org, Zero-knowledge rollups, https://shorturl.at/wIYZ4, 2023. Last accessed on 2022-11-
28.
[31] T. Chen, H. Lu, T. Kunpittaya, A. Luo, A review of zk-snarks, CoRR abs/2202.06877 (2022).
[32] E. Ben-Sasson, I. Bentov, Y. Horesh, M. Riabzev, Scalable, transparent, and post-quantum secure
computational integrity, IACR Cryptol. ePrint Arch. (2018) 46.
[33] F. D. Cosmo, Verification of prev-free communicating datalog programs, in: CILC, volume 3428 of
CEUR Workshop Proceedings, CEUR-WS.org, 2023.
[34] B. C. Grau, I. Horrocks, M. Kaminski, E. V. Kostylev, B. Motik, Limit datalog: A declarative query
language for data analysis, SIGMOD Rec. 48 (2019) 6โ17.
[35] Ethereum Improvement Proposals, ERC-20: Token Standard, 2015. URL: https://eips.ethereum.org/
EIPS/eip-20.
[36] D. C. Mills, K. Wang, B. Malone, A. Ravi, J. Marquardt, A. I. Badev, T. Brezinski, L. Fahy, K. Liao,
V. Kargenian, et al., Distributed ledger technology in payments, clearing, and settlement (2016).
[37] A. Bechtel, A. Ferreira, J. Gross, P. Sandner, The future of payments in a dlt-based european
economy: a roadmap, in: The Future of Financial Systems in the Digital Age: Perspectives from
Europe and Japan, Springer Singapore Singapore, 2022, pp. 89โ116.
[38] Y. Lee, B. Son, H. Jang, J. Byun, T. Yoon, J. Lee, Atomic cross-chain settlement model for central
banks digital currency, Information Sciences 580 (2021) 838โ856.
[39] M. L. Bech, J. Hancock, T. Rice, A. Wadsworth, On the future of securities settlement, BIS Quarterly
Review, March (2020).
[40] C. Laneve, A. Parenti, G. Sartor, Legal contracts amending with, in: International Conference on
Coordination Languages and Models, Springer, 2023, pp. 253โ270.
[41] M. Y. Vardi, The complexity of relational query languages, in: Proceedings of the fourteenth
annual ACM symposium on Theory of computing, 1982, pp. 137โ146.
[42] P. Tolmach, Y. Li, S.-W. Lin, Y. Liu, Z. Li, A survey of smart contract formal specification and
verification, ACM Computing Surveys (CSUR) 54 (2021) 1โ38.
[43] A. Li, J. A. Choi, F. Long, Securing smart contract with runtime validation, in: PLDI, ACM, 2020,
pp. 438โ453.
[44] ร. Hajdu, D. Jovanoviฤ, solc-verify: A modular verifier for solidity smart contracts, in: Verified
Software. Theories, Tools, and Experiments: 11th International Conference, VSTTE 2019, New
York City, NY, USA, July 13โ14, 2019, Revised Selected Papers 11, Springer, 2020, pp. 161โ179.
[45] A. Shkapsky, M. Yang, C. Zaniolo, Optimizing recursive queries with monotonic aggregates in
deals, in: ICDE, 2015, pp. 867โ878.
[46] L. Alt, C. Reitwieรner, Smt-based verification of solidity smart contracts, in: ISoLA (4), volume
11247 of Lecture Notes in Computer Science, Springer, 2018, pp. 376โ388.
[47] N. S. Bjรธrner, A. Gurfinkel, K. L. McMillan, A. Rybalchenko, Horn clause solvers for program
verification, in: Fields of Logic and Computation II, volume 9300 of Lecture Notes in Computer
Science, Springer, 2015, pp. 24โ51.
[48] A. Gurfinkel, Program verification with constrained horn clauses (invited paper), in: CAV (1),
volume 13371 of Lecture Notes in Computer Science, Springer, 2022, pp. 19โ29.
[49] L. Alt, M. Blicha, A. E. J. Hyvรคrinen, N. Sharygina, Solcmc: Solidity compilerโs model checker, in:
CAV (1), volume 13371 of Lecture Notes in Computer Science, Springer, 2022, pp. 325โ338.
[50] M. Nissl, E. Sallinger, Modelling smart contracts with datalogmtl, in: EDBT/ICDT Workshops,
volume 3135 of CEUR Workshop Proceedings, CEUR-WS.org, 2022.