The distinction of traditional and smart contracts has been subject for long discussions over the last years. While there is an agreement that a one-to-one mapping of the whole contract is not the desired goal, there is an understanding that traditional and smart contracts have certain properties in common. In this paper, we present our technical insights we derived with our industrial partners by discussing the importance of a rule-based language for bridging the gap between traditional and smart contracts and introduce a translation tool for logic-based Smart Contracts for supporting well-known blockchain platforms.
Distributed ledger technology (e.g., blockchains) represents a vibrant area of new technology
spreading into diferent research domains. In particular, smart contracts, i.e. executable code on
the blockchain that facilitates the process of executing and enforcing the terms of an agreement
between (untrusted) parties, create a rich field of applications in areas such as supply chain
management [
Example 1. Real Estate. Buying a property has many connected agreements such as warranty, payment agreements or credit agreements. A legally binding agreement usually describes the obligations of the seller, the cash flows to the seller depending on the construction process, the warranty rights of the buyer, and many more agreements. One easily sees that smart contracts are capable of streamlining the process of buying real estate, not only simplifying the process but also saving money as no escrow agent or other parties are required.
Usually, when lawyers draft legal agreements, such as Example 1, they have to consider many
diferent aspects of the agreement such as the currently valid law and the implications on the
requirements of the client. They may even have an iterative process of improving the legal text
of the contract with the client to optimally fit the clients’ goals. Using the same process for the
creation of smart contracts causes several challenges, which we list next [
While some of the challenges are strategic decisions, some of the issues can be tackled by
using logic-based smart contract languages. It is our experience, that logic-based rules improve
the readability of the code for non-experts and improve the communication between diferent
stakeholders [
While these concepts give the possibility to provide the toolset, their usage is currently limited: Not only is the research regarding logic-based languages in its infancy, there is usually either no distributed ledger technology natively supporting the suggested language, or the blockchain is not established and supported by a wide range of people, which can easily cause security issues (e.g., creating forks and rewriting the immutable history).
Contributions. In summary, while logic-based smart contracts would have all the advantages discussed so far, it is all but impossible for such a language to gain acceptance until it is supported by a major, widely adopted current blockchain. Achieving this is precisely the goal of this paper. Our main contributions are: • A theoretical discussion of each component of our DatalogMTL language including required characteristics of our language due to typical procedural smart contract settings. • A novel translation system converting DatalogMTL smart contracts into executable
Solidity smart contracts, the predominant platform in practice.
• An experimental evaluation including a discussion of possible improvement potentials. Organization. The remainder of the paper is structured as follows: In Section 2 we summarize DatalogMTL. In Section 3 we introduce DatalogMTL as smart contract language building on the concepts introduced in our previous work. In Section 4 we present our translation engine, which we evaluate in Section 5. We discuss related work in Section 6 and conclude this work in Section 7.
DatalogMTL [
Intervals. Formally, intervals are defined over an ordered set of rational numbers Q where each interval is of the form ⟨− , +⟩ with the endpoints − , + ∈ Q ∪ {−∞ , ∞}, for each ∈ we have − ≤ ≤ + and ⟨ is either open (‘(’) or closed (‘[’) and ⟩ is either open (‘)’) or closed (‘]’). An interval is punctual if it is of the form [, ], in which case we write instead, positive if − ≥ 0, and bounded if − , + ∈ Q.
Syntax. DatalogMTL with stratified negation is defined over a function-free first-order vocabulary consisting of disjoint sets of constants, variables and predicates. Each predicate is equipped with a non-negative arity. A term is either a constant or a variable. An atom is of the form ( ), where is a predicate and is a tuple of terms, with matching the arity of . A literal is an expression of the form
::=⊤ | ⊥ | ( ) | ⊟ | ⊞ | | | | where is a positive interval. A rule is an expression of form 1 ∧ · · · ∧ ∧ not +1 ∧ · · · ∧ not + → where , ≥ 0, each is a literal and is a literal not mentioning , , or . The conjunction is the body of the rule, where the literals 1 ∧ · · · ∧ denote positive body atoms and +1 ∧ · · · ∧ + denote negated body atoms, and the literal is the rule head. Instead of ∧ we sometimes use “,” to denote conjunction. A rule is safe if each variable occurs in at least one positive body atom. A program Π is a finite set of safe rules and stratifiable if there exists a stratification of a program Π. A stratification of Π is a function mapping each predicate in Π to positive integers s.t. for each rule . . . ′( ′) . . . → ( ) in Π we have ( ′) ≤ ( ) and for each rule . . . not ′( ′) . . . → ( ) in Π we have ( ′) < ( ). A program, rule, atom is ground if it contains no variables. A fact is an expression over an interval of the form ( )@ where ( ) is a ground atom. A dataset is a finite set of facts.
Semantics. An interpretation M is based on a domain for the individual variables and constants
that specifies for each time point ∈ Q and each ground atom ( ), whether ( ) is satisfied
at , written as M, |= ( ). The notion of satisfiability of an interpretation M is extended
inductively to ground literals according to Figure 1. An interpretation M is a model of not
(M, |= not ), if M, ̸|= , of a ground rule , if M, |= for 0 ≤ ≤ and M, |= not
for + 1 ≤ ≤ + for every , of a rule when it satisfies every possible grounding of the rule
and of a a program, if it satisfies every rule in the program and the program has a stratification.
An interpretation M is a model of a fact ( )@, if M, |= ( ) for all ∈ and a model
of a set of facts if it satisfies each of these facts. A program Π and a dataset entail a fact
( )@ ((Π, ) |= ( )@) if M |= ( )@ for each model of both Π and .
M, |= ⊞
M, |= ′ if M, |= ′ for some with − ∈ ∧ M, |= for all ∈ (, )
M, |= ′ if M, |= ′ for some with − ∈ ∧ M, |= for all ∈ (, )
M, |= if M, |= for some with − ∈
M, |= if M, |= for some with − ∈
if M, |= for all with − ∈
if M, |= for all with − ∈
for each
for no
Negation and Arithmetics. As smart contracts vitally require negation and arithmetics,
we allow mild variants of both of them. First, we allow sequential stratified negation [
Example 2. Consider following DatalogMTL rule modelling a agreement – signed at some point in the past – of a payment after the successful fulfillment of a specific Achievement .
[0,∞)SignedPaymentAgreement(Buyer , Seller , Amount , Achievement ),
In this section we discuss the modelling of smart contracts with DatalogMTL over the integer
fragment [
In procedural smart contract languages one usually sets up the initial values with the constructor which is invoked when deploying the smart contract in the blockchain. In DatalogMTL this corresponds to providing the initial values as a given dataset at a certain timestamp. For the timestamps, we have two options: • Local timestamp. The smart contract does not depend on any other timestamps (either time-information such as the current date or information from other contracts). Then one can initialize the timestamp with 0 or any other number. • Global timestamp. The smart contract uses the timestamp of the blockchain for initialization. This allows to use a shared timestamp and the actual current time inside the contract. As for the contract itself, the initial value has no influence on the reasoning (it is just shifted to a diferent timestamp), we always use a globally shared timestamp. This is, we set the = now (), where now is the current timestamp in the blockchain. Example 4. (continued) The initial values are given by the following dataset encoding the initial stage of the state machine: {Stage(Init )@}, where is the deployment timestamp as discussed above.
Usually, to invoke a smart contract in Ethereum one calls a method of a smart contract. Each call is initialized by a transaction, which allows the called smart contract to invoke other smart contracts. In DatalogMTL we only have rules that fire (i.e., derive the rule head) when the body is satisfied. In order to model an invocation of a method in DatalogMTL, we mark predicates as activators. These activators can be “called” by adding the activator for the current timestamp to the dataset. By writing rules that use these activators in the body one hence triggers the derivation of further facts. As we use activators for triggering rules, they have to obey the following restrictions to enforce compatibility with Ethereum: (i) an activator is only allowed in the body of the rule, (ii) only one activator is allowed to be executed per timestamp (to have an implicit method call order and prevent conflicting states).
Example 5. (continued) The set of activators for the bidding state machine consists of the following activators: {Bid, Execute}.
One usually encodes in a method of a smart contract the transition of data/state before and after the execution of a method. We already covered in the previous section the activation via an “activator”. This activator triggers a set of rules that state how the current dataset at timepoint is changed for the next state at timepoint + 1. This implies that such rules are not allowed to derive facts for entries in the past.
Example 6. (continued) The rules for the state machine are given as follows:
VBid(S , A), HighBid(_, CA), > → ⊞ [
HighBid(S , CA), ¬VBid(_, _), Execute → ⊞ [
So far, we focused on modelling a single smart contract. However, a method of a smart contract can invoke a diferent (target) smart contract and use the return value in the remaining method. In order to handle this case in DatalogMTL, we require the following extensions: • Namespaces to uniquely identifies a given smart contract. • Triggers to “trigger” an activator of a diferent smart contract. Note that due to the restrictions of one activator per timestamp, this creates a temporal chain of calls. • A Default Activator (Caller.default) to handle the passing of “return values” to the calling smart contract. In case diferent default activators are required, one can introduce additional intermediary smart contracts, which default activator triggers a named activator of the original contract. Example 7. (continued) A namespace for the running example could be “BidingContract” and the DoAction could be an invocation of a contract (e.g., namespace Token) to transfer tokens, e.g., Token.transferFrom(Src, Tgt , 20). After a successful application it uses the default activator to trigger the calling smart contracts so that it can continue the execution.
Combining the introduced concepts, we derive the following definition: Definition 1.
A smart contract is a quadruple (, Π, , ) where: • is a unique name of the contract (namespace). • Π is the DatalogMTL program encoding the rules of the smart contract • is the initial dataset encoding the initial state of the smart contract. • is the set of activators containing predicates which may be invoked by other smart contracts or parties.
While the introduced concept so far allows one to model several use cases, there is one open point for discussion, namely blockchain-specific parameters. In this paper, we study the most important properties of Solidity and how we can ensure the usage in DatalogMTL. Typically, one distinguishes between three diferent classes of properties: • Block-specific properties, such as the block number, or the timestamp. • Transaction-specific properties, such as the initiator of the transaction (origin) considering the full chain of executions starting from an external call to the activator. • Message-specific properties, such as the caller or the number of coins sent to the invoked contract.
We inject these properties by introducing pre-defined predicates which are added to the dataset, e.g., Block(Number ), Transaction(Origin) or Msg(Caller ). The only property we do not consider in this mapping is the timestamp as this causes ambiguity and hence has to be treated in a special way, which the following two points highlight: • Timestamp per block. In Ethereum, the timestamp is provided per block and the only requirement for the timestamp is that it is higher than the previous block. This means, that the timestamp received in a method is the timestamp of the block. That is, each transaction, and hence each method invocation (i.e., message) shares the same timestamp and the actual timestamp is dependent on the miner of the block and may not model the exact time. • Time and ordering. For modelling smart contracts we require two diferent kinds of timestamps. One that models the real time, for example to check if something happened within the last 24 hours, and one to model the sequential order of method invocations. In order to handle this representation problem in DatalogMTL, we decided to assign each message its own timestamp. This is possible as the main goal is the conversion to the Ethereum platform, where the natural mapping discussed above can be used.
What we have seen is that for the purposes of this paper, namely translation, this yields a quite natural, relatively simple structure of time. We remark that for future work that includes verification of smart contracts, there is an interesting subtlety between the “logical” clock of messages, and the real-world clock (as the number of messages per block vary and are unknown in advance). While this is far beyond the scope of this paper, we want to note it is an interesting item for possible research.
In the previous section we established the required formalism to model a Ethereum-compatible smart contract in DatalogMTL. In this section, we present our proof of concept for translating DatalogMTL rules into Solidity. Figure 2 shows a general overview of the process, where each step is discussed in the following. Phase 1 - Parser. The first phase is all about parsing and normalizing the program. For this, we read a DatalogMTL smart contract from file and apply a normalization procedure to ensure that each rule has a head without a temporal operator and the body either has literals containing no temporal operator, or consists of exactly one literal with a single temporal operator.
Example 8. (continued) Rule (3) of the running example would be rewritten by introducing an auxiliary predicate and moving the temporal operation into the body as follows: Stage(Execution), ¬Execute → Temp1()
[
Example 9. (continued) The group of rules for the running example are the execution group (4-5) containing the Execute activator, the bidding rules (6-8) containing the Bid identifier and the global group (1-2) which are activator independent. Rule (3) and (9) are detected as negated activators copying the current state and are removed as no further consideration in Solidity is requireda. aNote that we have added those rules at the beginning to allow the smart contract to be interpreted by a Datalog reasoner. When the only goal is the conversion to Solidity, one can ignore the rules when writing the smart contract in DatalogMTL.
Phase 3 - Data Types. We distinguish between the following two types: • Term Type. We derive the data type of a term where possible from the internal values (e.g., from the dataset). However, when there is an activator, we are unaware of which values are provided by the user (e.g., is it 8bit or 256bit integer). Therefore, we extend the activator syntax to provide data types for the activators. • Atom Type. An atom can be either stored by one or more variables, each either being a primitive, array or map. First, we distinguish whether there exists only one valid atom per time unit, then single values are suficient and per term a variable is created. Otherwise, we check if there is a pattern for accessing the atom to identify a map type (e.g., there is an access in body and head and some variables are shared).
Example 10. (continued) The activator for bidding would be Bid(). Note that with the introduction of the message-specific parameters the sender is extracted into an own atom Msg(). The atom type of HighBid would consists of multiple primitives. Phase 4 - State Types. For the state of the smart contract we have to distinguish between local state where the derived fact is not shared with any other method and does not need historical information, state variables where we only require the latest state (are not time-dependent), variables where we need a last-timestamp of action, and variables were we need a history of changes for a time period. For detecting the local state, we use the grouping to check whether there exists not another group that contains the same atom and uses information from other time units. In such a case, we can inline the state at contract generation. For detecting the latest state atoms, we check whether the state always depends on the previous timestamp in DatalogMTL. To distinguish between the remaining cases, we diferentiate on whether we have to check if some condition is currently fulfilled or whether there is a more complex comparison where the other case is not enough1.
Example 11. (continued) Variables Stage0, HighestBid0 and HighestBid1 are identified as global state, where the numbers reference to the term position. In addition a variable storing the timestamp when Stage(InitState) become true is created.
Phase 5 - Contract Generation. What now remains is the processing of the rules per group. We start by adding preliminary checks, then continue per activator. This is, we structure the rules by a dependency graph and convert each rule to Solidity. In case there is an option to handle multiple rules at the same time, we try to find specific structures that follow a specific pattern. For example, for the bidding rules, we detect that these rules are a typical if-else structure and furthermore that only the if part is relevant.
Example 12. (continued) The generated function for bidding is as follows, with checks for the correct phase and a valid ofer. Note that __global is a modifier executed before the function that handles automatic state transitions. function bid(int a_) public __global { require(compareStrings(_stage0, "AcceptingBids"),
"invalid request"); require(a_ > _highestbid1, "invalid request"); _highestbid0 = msg.sender; _highestbid1 = a_; }
In this section, we discuss the results of our smart contract language and generation process
by encoding the ERC-20 token in our language and comparing the generated code with the
original Solidity code [
In general, the generation of the smart contract shows similar code as the compared original code. This means, that the supposed steps of the pipeline achieve the desired goals. In a detail comparison, we detected some possible improvement potentials: (i) reduce code, (ii) check for variable range (e.g., overflows), (iii) improve variable types to reduce execution costs.
Besides the discussed limitations, we want to remark that the current implementation is a proof-of-concept not supporting all cases yet. The most relevant part is to detect the required state types and their dependencies given by the rules, which we identified as one point that needs more detailed investigation. Still, as the results have shown, the generation process is feasible and we continue sharpening the generator to cover more advanced tasks in the future. 1Note that by the definition of state transitions, non-local state is only allowed to be set for future time points.
One can group the related work around logic-based smart contracts into two categories: work including and work not including temporal properties.
Non-temporal-based related work. Idelberger et al. [
Temporal-based related work. Hu and Zhang [
This work, to the best of our knowledge, is the first one to have a temporal logic-based smart contract language that is executable on a widely used blockchain. While it is still a proof of concept, it already handles many of the subtleties and challenges, in particular blockchainspecific variables, state types, etc. It is able to produce meaningful code for widely used patterns, including the ERC-20 token. In future work, we want to concentrate on improving the translation engine and studying on the framework around the creation of a traditional contract by strengthening the interdisciplinary collaboration.
This work was supported by the Vienna Science and Technology Fund (WWTF) grant VRG18013, and the “rAIson data” Royal Society grant of Prof. Georg Gottlob.
In this section, we provide the full programs of our examples in DatalogMTL as given to our translation engine, having some subtle diferences to the rules presented in the work, i.e., we list the head first and use “:-” instead of →.
In addition to the generated program in Figure 3 and the linked source code of the Solidity version, we provide here the full version encoded in DatalogMTL.
In addition to the excerpt in Example 12 and the linked Solidity code of the presented pattern,
we provide here the full version in DatalogMTL as well as the generated version.
% I n i t r u l e , s e t b a l a n c e O f f o r c a l l e r
b a l a n c e O f ( C a l l e r , 2 0 0 0 ) : − msg ( C a l l e r ) .
% p a r t y i n i t i a t e s t r a n s f e r
t r a n ( C a l l e r , To , Value ) : − msg ( C a l l e r ) , t r a n s f e r ( To , Value ) .
% p a r t y a p p r o v e s t r a n s f e r i n f u t u r e
a l l o w a n c e s ( C a l l e r , Spender , Value ) : − msg ( C a l l e r ) , approve ( Spender , Value ) .
% Check whether b a l a n c e O f i s enough , then t r a n s f e r i s v e r i f i e d
vTran ( A , B , X ) : − t r a n ( A , B , X ) , b a l a n c e O f ( A , Y ) , X<=Y .
% Apply t r a n s f e r
[ + ] [
NewBalance=Y−X .
[ + ] [
NewBalance=Y+X .
[ + ] [
return keccak256(abi.encodePacked(a)) == keccak256(abi.encodePacked(b));