language = Java, basicstyle = , otherkeywords = object, keywordstyle = , ^affil0^affil0affiliationtext: FANTOM

OV: Validity-based Optimistic smart contracts

Quan Nguyen Andre Cronje Michael Kong

Abstract

Smart contract (SC) platforms form blocks of transactions into a chain and execute them via user-defined smart contracts. In conventional platforms like Bitcoin and Ethereum, the transactions within a block are executed sequentially by the miner and are then validated sequentially by the validators to reach consensus about the final state of the block.

In order to leverage the advances of multicores, this paper explores the next generation of smart contract platforms that enables concurrent execution of such contracts. Reasoning about the validity of the object states is challenging in concurrent smart contracts. We examine a programming model to support optimistic execution of SCTs. We introduce a novel programming language, so-called OV, and a Solidity API to ease programing of optimistic smart contracts. OV language together with static checking will help reasoning about a crucial property of optimistically executed smart contracts – the validity of object states in trustless systems.

Keywords Smart contracts $\cdot$ Programming Model $\cdot$ Design-by-Contract $\cdot$ OV language $\cdot$ Object Validity $\cdot$ Validity Contract $\cdot$ Optimistic $\cdot$ Static Checking $\cdot$ Trustless System $\cdot$ Distributed Ledger

1 Introduction

Engineering softwares in legacy computer systems is challenging, especially to maintain systems’s properties in the existence of concurrent calls that mutate system’s objects [32, 22, 9, 24]. It is even more challenging to write smart contracts (SC) to be deployed on top of blockchains due to the nature of trustless environment.

As blockchain technologies and cryptographic algorithms have been more efficient and secure, smart contracts have become increasingly popular. There have been many types of smart contracts since the term was first introduced [39]. Billions worth of USD are controlled by smart contracts world-wide, which are written in a number of programming languages to suite specific use cases of such programs. Blockchains rely on a consensus mechanism to reach agreement with peers on the sequential order of transactions in a block. Finalized transactions are committed as a group to the distributed ledger. All peers on the network perform a validation step by re-executing the transactions within the block and checking that the initial and final states match.

Ensuring correctness of smart contracts is a critical security concern as there have been exploitations of subtle bugs in these programs in the past couple of years. Another challenge is that SC code’s immutability after deployment makes bug fixing impossible. Current audit practices of smart contracts involve checking whether the code is safe against two kinds of vulnerabilities: (i) generic security errors such as reentrancy and overflows, and (ii) deeper custom functional requirements; for example, ”the sum of the deposits never exceeds the contract’s balance”. There have been a number of security tools for discovering generic errors and a few automatic verifiers of deeper functional requirements [31].

In this paper, we consider smart contracts that are executed on blockchain-based platforms. We leverage the common concept of the object invariants (i.e., functional requirements of objects) to address the challenge of expressing and reasoning about object invariants in smart contracts. Prior to describing our approach to allowing object validity of smart contracts to be specified and verified, we first highlight the importance of object validity in software development and then an overview of smart contracts.

1.1 Validity and Program Reasoning

A popular approach to enginering softwares is to model softwares with real-world objects or concepts that show clear program structures. Objects are often required to satisfy certain conditions — object invariants that must be maintained to guarantee the expected behaviour of the system. Any violation of the object invariant is often undesirable as it violates program logic and can cause programs to crash [19, 20, 29]. Here, this paper is not strictly limited to object-oriented programming, though we assume such O-O practices as much as possible.

Generally, reasoning about and maintaining object invariants in concurrent programs is difficult. The difficulties come from arbitrary object aliases, mutable object state, methods’ side effects and the sophisticated mixture of multiple threads and shared mutable state typically of concurrent O-O programs.

⬇

class Account {

private int amount = 0;

// inv: amount >=0

int balance() {

return amount;

}

void deposit(int x) {

amount += x;

}

void withdraw(int x) {

amount -= x;

}

class Customer {

private Account a;

private String id;

// inv: a!= null && a.amount >= 10

void transfer(int amt, String custID) {

Customer b = ….; // lookup custID

a.withdraw(amt);

b.deposit(amt);

}

Account getAccount() {

return a;

}

Listing 1: An example of Customer and Account written in Java

Listing 1 shows an example showing the challenges for maintaining object validity. A bank customer has an account. If a reference of account a of the customer is leaked, such as via a call getAccount(), then any manipulation of the reference is out-of-control of the customer. The alias makes it very hard to reason about the invariant of the customer, which depends on the account. If such a manipulation, e.g. withdraw, on the leaked reference occurs concurrently with the client’s operation, it would lead to a race condition on the account. As a result, no matter how carefully the Customer code is synchronized, neither a consistent state of the account nor the customer’s invariant is guaranteed. Even worse, now suppose all the three operations of the account are manifested with lock-based synchronization (monitors or mutexes), to prevent the potential race condition. Unfortunately, deadlock can occur if two customers attempt to simultanously transfer money to each other.

To mitigate the problems of locks, Software Transactional Memory (STM) systems [35] leverage a non-blocking approach promising to ease programming tasks for concurrent application developers. STM hides the complexity of concurrency control from programmers and enables safe composition of scalable applications. STM offers a programming model inspired from the ACID properties (e.g. Atomicity, Consistency, Isolation and Durability) of database transactions which play a major role in software systems. There are, however, few STMs [13] paying attention to data invariants — the consistency guarantees.

For code deployed in trustless systems, it is even a harder problem to reason about validity of objects. Concurrent smart contracts are much more challenging to reason about, since execution is done via blockchain nodes in a trustless system.

1.2 An Overview of Smart Contracts

Smart contract (SC), which was first proposed by Nick Szabo 20 years ago [39], refers to computer code that automatically executes all or parts of an agreement and is stored on a blockchain-based platform. Smart contracts (SCs) are supplied as user-defined scripts to be executed on blockchain nodes. The SC code is replicated across multiple nodes of a blockchain and, therefore, benefits from the security, persistence and immutability that a blockchain offers. That replication also means that as each new block is added to the blockchain, the code is, in effect, executed. With recent blockchain technologies, smart contracts can handle more sophisticated transactions, with an increasing number of on-chain tokenized assets. Developers may compose multiple transaction steps to form more complex smart contracts.

Bitcoin Script is the first successful implementation of a blockchain-based smart contract, providing a purposely not-Turing-complete language with a set of simple, pre-defined commands. It allows a simple forms of SC for Bitcoin transactions, such as pay-to-public-key-hash (P2PKH) and pay-to-script-hash (P2SH). Recently, other platforms, such as Ethereum, can support more complex contractual functionalities and flexibilities. Solidity, which is a Turing-complete language for smart contracts developed by Ethereum, is one of the most popular languages for SCs. Newer blockchain platforms, such as Hyperledger Fabric [1], allow smart contracts to be written in various high-level languages.

Conventional smart contract plaforms, such as Ethereum, leverage the sequential execution model of transactions within a block. The platforms have enabled the execution of transactions of various complexity in blocks via user-defined smart contracts. Each block of the chain consists of multiple smart contract transactions (SCTs). These SCTs are executed sequentially by the miner before appending the block into the miner’s blockchain. The remaining peers, acting as validators, on receiving this block will again sequentially re-execute the SCTs of the block. The validators agree with the miner about the final state of the block on their records. After validated, the block is added to the blockchain.

There has been some research work studying concurrent execution of transactions in a block. For example, one such approach is based on object semantics by miner using STM [2]. Concurrent miner stores a BlockGraph (BG) structure, which captures the object-conflicts relations among the SCTs, inside the block. Validators re-execute the same SCTs concurrently and deterministically, using the BG given by miner. The proposed block is appended into the blockchain if successful validation, or discarded otherwise. To address the double-spending issue, Optimistic Validator uses counter to find any malicious block proposed by a malicious miner [21]. Using concurrent miners and validators can achieve better performance than existing SC frameworks.

1.3 Our Approach

Adding concurrency to the execution of SCTs can potentially help achieve better efficiency and higher throughput [2, 8, 41]. Yet, there is no research in reasoning about object validity and security issues such reentrancy, in SCs on these platforms. In this paper, we are interested in the next generation of smart contracts platforms that can execute the SCTs concurrently to harness the power of multi-core processors. In order to address the security concern, we introduce a new approach that allows developers to specify validatity contracts in smart contracts. Valitidy contracts are used to statically checked against any violation of contract as well as reentrancy issues.

1.3.1 Solidity API for Validity Contract Specifications

There has been an extensive research in smart contracts tools and frameworks. But there is no research in how to specify object’s validity in smart contracts. With Solidity, which is the most popular programming language for writing smart contracts, there is still a lack of a way to specify object’s invarants [36].

To address this challenge, this paper introduces a new approach to allow programmers to specifying object’s invarants into Solidity programs. The new Validity API uses invariants for validity guarantees of objects in SCs.

⬇

// file: storage.sol

pragma solidity >=0.5.16 <0.7.0;

/**

* @title Storage

* @dev Store & retrieve value in a variable

contract Storage {

uint256 number;

/**

* @dev Store value in variable

* @param num value to store

function store(uint256 num) public {

number = num;

}

/**

* @dev Return value

* @return value of ’number’

function retrieve()

public view returns (uint256){

return number;

}

Listing 2: An Storage contract in Solidity

⬇

// file: storage.ov

class Storage [o] {

uint256 number;

// inv: number > 0

public void store(uint256 num) <this,this> {

number = num;

}

public uint256 retrieve() <this,top> {

return number;

}

Listing 3: An Storage contract in OV

⬇

// file: storage_ov.sol

pragma solidity >=0.5.16 <0.7.0;

import ’../Ownable.sol’;

import ’../Validity.sol’;

/**

* @title Storage

* @dev Store & retrieve value in a variable

contract Storage_OV is Ownable, Validity {

uint256 number;

/**

* @dev Store value in variable

* @param num value to store

function store(uint256 num)

preValid() postValid() public {

number = num;

}

/**

* @dev Return value

* @return value of ’number’

function retrieve() preValid()

public view returns (uint256) {

return number;

}

/**

* @dev Return bool

* @return true if the invariant holds; false otherwise

function isValid()

external view returns (bool) {

return number > 0;

}

Listing 4: An Storage contract converted from OV to Solidity. Storage’s invariant is given in isValid(). Checking functions thisThis(), thisTop(), or botThis() are appended as function modifiers

In Listing 4, methods are appended with a method isValid() that specifies the invariant of Storage contract. Method store is appended with new modifiers preValid() and postValid() to check pre-condition and post-condition. Function retrieve() has a precondition checked by appended modifier preValid().

Although the discussions are in Solidity, it is worth-mentioning that the concept of our work is not restricted to Solidity; it can be extended to support other SC languages.

1.3.2 Validity-Based Programming Language

We introduce a novel language, called OV (Optimistic valididy or Object validity), to help reason about the consistency in concurrent SC applications. Validity contracts for methods and transactions specify assumptions and effects on object invariants. The new language enables modular reasoning about object validity in the code and ensuring the validity of objects at runtime.

The contract-based programming model in the form of pre- and post- checks provides the system the consistency required for ACID transactions. All complex details of the underlying execution mechanisms (e.g., locks or transactions; the implementation details of STM library) are hidden from the programmers. With validity contract, OV system can reduce the number of required validity checks compared to what other approaches would require if they attempted to perform similar checks. Furthermore, validity contracts open a number of opportunities for optimization.

Listing 3 shows an example of Storage contract written in new OV language. Storage contract has an owner (”[o]”) that is uniquely idenfitied at compile time and at runtime. Method store requires the Storage to be valid (first ”this”) and it can invalidate the Store’s invariant inside its body (second ”this”). Assertions of Storage’s validity at the beginning and the end is required for the store method. Method retrieve requires the Storage’s invariant, but does not modify the state of Storage and so it invalidates nothing (pseudo ”top”). By using the validity contracts (”<this,this>” and ”<this,top>”), static checks can get rid of illegal operations.

Listing 5 gives a code fragment of a Ballot contract writing in Solidity. Listing 6 expresses the concept of Ballot contract’s owner (”[o]”) and validity contract (”<this,this>”). The validity contract specifies that method vote requires the Ballot contract is valid (and so all of its owned contracts are valid). The validity contract also states that the method vote may make some modifications to the ballot’s state,

⬇

contract Ballot {

mapping(address => Voter) public voters;

// more state definitions

function vote(uint proposal) {

Voter sender = voters[msg.sender];

if (sender.voted)

throw;

sender.voted = true;

sender.vote = proposal;

proposals[proposal].voteCount += sender.weight;

}

// more operation definitions

}

Listing 5: A Ballot contract in Solidity

⬇

class Ballot[o] {

public map<this> voters; // address => Voter

// more state definitions

void vote(uint proposal)<this,this> {

Voter sender = voters.get(msg.sender);

if (sender.voted)

throw;

sender.voted = true;

sender.vote = proposal;

proposals[proposal].voteCount += sender.weight;

}

// more operation definitions

}

Listing 6: A Ballot contract in OV

The benefits of validity contracts are three-fold. First, validity contracts are served for detecting transactional conflicts at a higher abstraction level (e.g., validity interference) than reads and writes. In STM, conflict detection determines when two transactions cannot both safely commit, to guarantee serializability. Second, validity contracts can be used for conflict resolution in contention management to guarantee progress (livelock avoidance) [16, 15], to increase throughput dramatically in high contention workloads [10, 33]. With validity contracts, contract-based contention managers with different safety-driven strategies can be developed to ensure liveness. Third, validity checks can be deduced from contracts and scheduled at transaction commits to preserve object validity. Reentrancy issues can be avoided from enforcing the validity requirements and effects of operations inside a transaction’s body. Validity contracts can help reduce the number of validity checks while ensuring safety. The validity contracts can be used to insert correct assertions of validity, e.g., calling preValid(), postValid() from the Validity API. Transactional validation ensures a transaction never views or makes use of inconsistent data; while object revalidation ensures transactions only commit valid data.

1.4 Contributions

This paper makes the following contributions:

$-$

Validity API We present a new API that provides a feasible solution to allow developers to specify object validity in smart contracts written in Solidity.
$-$

New Programming Model for Validity Contracts: This paper proposes a general programming model to allow developers to specify validity contracts for smart contracts. The validity contracts ensure sufficient checks for validity requirement at a function call start. The validity contracts are useful for detecting and scheduling conflicting transactions, and for software assurance by automating object revalidation via deduced assertions.
$-$

Reasoning about Optimistic Smart Contracts: This work is the first that introduces a practical way to express validity contracts in smart contracts. We present a new language OV integrating ownership mechanism, type system and dynamic semantics for modular reasoning about object validity and validity contracts for smart contract transactions. The validity contracts are useful to enhance program safety and to improve modularity and composability of optimistic smart contracts.

1.5 Paper structure

The rest of this paper is organised as follows. Section 2 introduces our new Validity API written in Solidity and an example of validity contracts using our API. Section 3 presents our validity-aware model and new OV language for optimistic smart contracts. The section gives the execution model, abstract syntax and semantics of the new language. Section 4 gives some discussions about possible optimization using validatity contracts. Section 5 gives an overview of the related work. Section 6 concludes.

2 New Solidity API for Validity Contracts

To overcome the shortcomings of Solidity, we introduce a new Validity API to allow developers to specify and reason about object validity.

2.1 Validity API

Ownable contract describes a general kind of contracts that has an owner. There is a private field ’owner’ that will be initiated at contract creation; caller that creates a contract is the owner of the created contract. Modifier isOwner is used in functions whose invocation is restrictive to the contract’s owner. Modifier isCalledBy is dedicated for functions that are called from a particular caller’s address.

⬇

// file: ownable.sol

pragma solidity >=0.5.16 <0.7.0;

/**

* @title Ownable

* @dev Set and get owner

contract Ownable

// modifier to check if caller is owner

modifier isOwner() {

require(msg.sender == owner, ”Caller is not owner”);

}

// modifier to check if caller is owner

modifier isCalledBy(address addr) {

require(msg.sender == addr, ”Caller is not the specified address”);

}

// @dev Set contract deployer as owner

constructor() public {

owner = msg.sender; // ’msg.sender’ is sender of current call

}

/**

* @dev Return owner address

* @return address of owner

function getOwner() external view returns (address) {

return owner;

}

address private owner;

}

Listing 7: An Ownable contract in Solidity

In this API, ownership transfer is not allowed. Each contract has a unique immutable owner at creation time. This is to guarantee the ownership tree (which-owns-which) is unique to ease the reasoning of validity of SCs.

Validity interface gives a simple interface that defines isValid() function and two modifiers. Actual contracts that implement Validity interface must specify its own implementation of isValid() function. Modifier preValid() is used for a function that require the contract’s validity before the function’s invocation. Whereas modifier preValid() asserts a post-condition of the contract’s validity after the function is called.

⬇

// file: validity.ov

pragma solidity >=0.5.16 <0.7.0;

/**

* @title Validity

* @dev define validity of an object

interface Validity {

/**

* The invariant condition of an object.

* Subclass must implement this method speciyfing its invariant.

function isValid() external view returns (bool);

// modifier to check object’s validity prior a function call

modifier preValid() {

require(this.isValid(), ”Validity fails pre-check”);

}

// modifier to check object’s validity immediately after a function call

modifier postValid() {

require(this.isValid(), ”Validity fails post-check”);

}

Listing 8: An Storage contract in OV

OVValidity interface extends Validity interface by adding several extra modifiers. These additional modifiers are used to ease the transformation of OV program into Solidity. Modifier thisThis() is used for functions that require pre- and post- checks of a contract’s validity. This corresponds to the contract <this,this> in OV. Modifier botThis() is used for functions that require a post- check of a contract’s validity. This corresponds to the contract <bot,this> in OV. Modifier thisTop() is used for functions that require a pre- check of a contract’s validity. This corresponds to the contract <this,top> in OV. Modifier botTop() is used for functions that neither require a pre- or post- check of a contract’s validity. This corresponds to the contract <bot,top> in OV. This modifier can be safely ignored, as functions with this validity contract does not require such checks.

⬇

// file: ovvalidity.sol

pragma solidity >=0.5.16 <0.7.0;

/**

* @title OVValidity

* @dev define validity of an object

interface OVValidity {

/**

* The invariant condition of an object.

* Subclass must implement this method speciyfing its invariant.

function isValid() external view returns (bool);

// modifier to check object’s validity prior a function call

modifier preValid() {

require(this.isValid(), ”Validity fails pre-check”);

}

// modifier to object’s validity immediately after a function call

modifier postValid() {

require(this.isValid(), ”Validity fails post-check”);

}

// The following modifiers are short-hand for OV language

// modifier to check object’s validity before and after a function call

modifier thisThis() {

require(this.isValid(), ”Validity fails pre-check”);

require(this.isValid(), ”Validity fails post-check”);

}

// modifier to check object’s validity after a function call

modifier botThis() {

require(this.isValid(), ”Validity fails post-check”);

}

// modifier to check object’s validity before a function call

modifier thisTop() {

require(this.isValid(), ”Validity fails pre-check”);

}

// modifier that is simply not checking object’s validity at all

modifier botTop() {

}

Listing 9: An OVValidity interface specifying validity function isValid() and modifiers thisThis(), thisTop(), or botThis() are appended as function modifiers

2.2 Example

We then present an example of smart contracts using our Validity API. Listing 10 shows an Account contract writing in Solidity. An Account contract has a balance and three functions. The account balance has an invariant that requires the balance is greater than 0 and less than $1e30$ . Functions deposit and withdraw can modify the balance field and thus can invalidate the account’s invariant. Function get simply retrieves the value of the balance.

Listing 11 shows the Account contract written in OV language. The account has an owner (”[o]”). Functions deposit() and withdraw() require the account’s invariant to be valid before and after the function’s body. In OV, the validity contracts are specified as <this,this>. Function get() retrieves the balance without any modification to the account’s state (the balance field). Validity contract specified in OV as <this,top>.

Listing 12 gives a program, which is the result of a transformation from OV to Solidity. The account contract implements Ownerable contract and OVValidity interface. The object validity is defined in isValid function. The isValid function itself does not require any validity checks and thus botThis() modifier is used. Functions deposit() and withdraw() are appended with modifier thisThis(). Function get is appended with modifier thisTop().

⬇

pragma solidity >=0.5.16 <0.7.0;

/**

* @title Account

* @dev Deposit, withdraw and get balance

contract Account {

uint256 balance;

// invariant: balance > 0 && balance < 1e30

/**

* @dev Deposit an amount to the account

* @param amount value to deposit

function deposit(uint256 amount) public {

balance += amount;

}

/**

* @dev Withdraw an amount from the account

* @param amount value to withdraw

function withdraw(uint256 amount) public {

balance -= amount;

}

/**

* @dev Return value

* @return value of the account

function get() public view returns (uint256){

return balance;

}

Listing 10: An Account contract in Solidity

⬇

class Account [o] {

uint256 balance;

// inv: balance > 0 && balance < 1e30

public void deposit(uint256 balance)<this,this> {

balance += amount;

}

public void withdraw(uint256 balance)<this,this> {

balance -= amount;

}

public uint256 get()<this,top> {

return balance;

}

Listing 11: An Account contract in OV

⬇

pragma solidity >=0.5.16 <0.7.0;

import ’../Ownable.sol’;

import ’../OVValidity.sol’;

/**

* @title Account

* @dev Deposit, withdraw and get balance

contract Account is Ownable, OVValidity {

uint256 balance;

// invariant: balance > 0 && balance < 1e30

/**

* @dev Deposit an amount to the account

* @param amount value to deposit

function deposit(uint256 amount) thisThis() public {

balance += amount;

}

/**

* @dev Withdraw an amount from the account

* @param amount value to withdraw

function withdraw(uint256 amount) thisThis() public {

balance -= amount;

}

/**

* @dev Return value

* @return value of the account

function get() thisTop() public view returns (uint256){

return balance;

}

/**

* The invariant

* @dev Return bool

* @return true if the invariant holds; false otherwise

function isValid() botThis()

external view returns (bool) {

return balance > 0 && balance < 1e30;

}

Listing 12: An Account contract converted from OV to Solidity. Account’s invariant is given in isValid(). Checking functions thisThis(), thisTop(), or botThis() are appended as function modifiers

3 OV: Validity-Aware Optimistic Smart Contracts

We present our new programming model, in which transaction has a validity contract specifying the requirements and effects. Transaction contracts are useful for program verification and optimization. Based on the design-by-contract (DbC) discipline, transaction contracts can be used to ensure system validity by supporting both static or dynamic checking, and can be used to help detect and resolve conflicts between transactions.

3.1 Validity Contracts for Smart Contract Transactions

Transaction comprises a set of operations to be executed all at once, or none at all. Transactions often preserve the ACI (atomicity, consistency, isolation) properties. A transaction may perform operations on shared objects, as well as local data (objects) that are inaccessible to other transactions. Each transaction, distinguished by a unique identifier, is initially live and may eventually become either committed (successful) or aborted (failed or cancelled).

Our new language, namely OV, generalizes the idea of validity contracts and validity subcontracting that are introduced in AVID [30] for contract specifications of STM transactions in legacy softwares. Specifying the validity contracts in OV is similar to read-write effects in previous work [23, 6, 5, 4] for sequential programs. Here, OV leverages the idea of validity contract to describe behavioural abstraction of a SC transaction.

Listing 13 describes the underlying mechanism of validity contracts for SC transactions. A validity contract of a SC transaction, written as $\langle\mathcal{V},\mathcal{I}\rangle$ , specifies the validity requirements and effects of the transaction. The validity set $\mathcal{V}$ specifies a set of objects that must be valid both before and after transaction execution. The invalidity set $\mathcal{I}$ specifies a set of objects that may be invalidated by the execution of the transaction. These objects in $\mathcal{I}$ are the only ones whose fields may be modified within the transaction’s execution. That means the invariant of the objects within $\mathcal{V}\cap\mathcal{I}$ may be broken during the transaction execution. These objects must be revalidated prior to transaction commit; all objects in the validity set are ensured valid once transaction commits.

⬇

Validity contract

\langle\mathcal{V},\mathcal{I}\rangle

of a transaction T

implies:

Begin: requires

\mathcal{V}

valid

Executing: may modify

\mathcal{I}

Prior to commit: revalidate

\mathcal{V}\cap\mathcal{I}

Finish: ensures

\mathcal{V}

valid;

\mathcal{I}\setminus\mathcal{V}

may still be invalid

Listing 13: Meaning of Transaction’s Validity Contract

Validity subcontracting restricts which operations may be performed by a specific contract. Subcontracting constrains the invariant requirements and effects of calls or subtransactions nested inside a transaction or a method, such as the relationship between a caller and each of its callees, and between a transaction and each of its nested transactions. That is, $\langle\mathcal{V}^{\prime},\mathcal{I}^{\prime}\rangle$ is a subcontract of $\langle\mathcal{V},\mathcal{I}\rangle$ if $\mathcal{V}^{\prime}\subseteq\mathcal{V}\ {\rm and}\ \mathcal{I}^{\prime}\subseteq\mathcal{I}$ . Like AVID, the version of subcontract in OV allows more programs to be type checked, but requires additional runtime validity checks.

A context $V$ in OV is a syntactic sugar for the set of objects in the subtree of the ownership tree rooted at $V$ (as in [23, 4]). Ownership contexts are used to specify both validity and invalidity sets. A bot context represents an empty set. A transaction/call with bot validity set implies no validity check required at start. A bot invalidity set implies the transaction/call neither modifies nor invalidates any object.

OV transactional execution mechanism allows roll back of a transaction that causes violation of some object’s invariant. Pure queries having an empty $\mathcal{I}$ and so require no revalidation. The overlap of $\mathcal{V}^{\prime}$ and $\mathcal{V}\setminus\mathcal{I}$ specifies the set of objects whose validity is required at the start of the (sub)transaction/call. No revalidation is necessary at the end of a transaction when there is no overlap between $\mathcal{V}$ and $\mathcal{I}$ .

3.2 Execution Model

Execution model of OV programs allows a transaction to create a sub-transaction by using atomic{S} expression. Semantics for contract-attached atomic expression in our model is similar to the one used in [16, 37, 7, 17]. OV transaction may nest a number of sub-transactions. Here, we assume a simpler model, called linear nesting [28, 18], which restricts a transaction to have at most one live child. This simple form ensures atomicity of the nested transactions and validity of the objects rather than full concurrency optimization. Top-level transactions can run concurrently and commit their effects to the memory. Generally speaking, OV’s general execution model can support closed nested transactions [27], in which all memory locations being accessed by nested transactions are conceptually considered as being accessed by its parent transaction. When a closed-nested transaction commits, its read and write sets are merged with those of its parent.

Validity requirement specifies how transactions can guarantee the validity at transaction start. A transaction may wait for validity prior to transaction start and may revalidate validity of an object before it commits. For example, by using conditional atomic regions [3, 7, 17] or conditional critical regions (CCR) [12]. The when(o.valid()){S} expression waits until the object invariant being held before it starts the transaction execution.

Transaction validation ensures the consistency of the objects accessed by a transaction, with respect to other concurrent transactions. Retrying an aborted transaction is considered as executing a new transaction with same validity contracts, although with a different transaction identifier. Object revalidation ensures the consistency of the objects according to the contract of the particular transaction. In OV’s general model, transaction performs an automatic check for the validity of the object in the transaction validation step. The validity check is deduciable from the transaction’s contract.

Validity subcontract generalises a similar concept in AVID [30] used only for concurrent programs, to apply for smart contract transactions. For all method definitions, it guarantees all expressions inside a method are covered by the method contract. For all transactions, subcontracting is applied to parent and child transaction, or to a transaction and its nested calls/transactions. Parent transaction must ensure the validity set of a subtransaction’s contract before it starts. The invalidity set of the subtransaction must be captured within that of its parent transaction.

3.3 Language

Here, we present our OV language, which is a Java-like language, for secure smart contracts. OV language is based on AVID language [30], which was introduced for STM in legacy softwares. More details about the validity contracts, type systems and semantics can be found in AVID [30].

The abstract syntax of OV language is shown in Table 1. The type system relies on ownership types for managing dependencies between object invariants. The metavariables $T$ ranges over types; $K$ ranges over contexts; $V,I$ ranges over validity and invalidity sets ; $P$ ranges over programs; $L$ ranges over class definitions; $M$ ranges over method definitions; $e$ ranges over expressions; $C$ , $X$ , $m$ , $f$ and $x$ range over class, formal context parameters, method and field names, and variables names, respectively. this refers to the target object for the current call and is also used as an ownership context. The overbar is used for a possibly empty sequence of constructs; for example, $\overline{e}$ is used for a finite ordered sequence $e_{1}..e_{n}$ , $\overline{T}\ \overline{x}$ stands for a possibly empty sequence of pairs $T_{1}\ x_{1}..T_{n}\ x_{n}$ . An expression $e$ can be either a constant $c$ , a variable $x$ , the this pseudo variable, a field access $e.f$ , a method invocation $e.m(\overline{e})$ , an object construction $new\ T$ , a sequential composition ( $\textsf{seq}(e,e)$ ), a thread creation ( $\textsf{fork}\ e$ ) and an atomic block ( $\textsf{atomic}[\Delta]_{opt}\ e$ ).

$T$	$::=$	$C\langle\overline{K}\rangle\ \|\ \textsf{int}\ \|\ \textsf{bool}$	types
$K$	$::=$	$X\ \|\ \textsf{top}\ \|\ \textsf{bot}\ \|\ \textsf{this}\ \|\ *$	contexts
$V,I$	$::=$	$K$	validity and invalidity sets
$P$	$::=$	$\overline{L}\ e$	programs
$L$	$::=$	$\textsf{class}\ C[\overline{X}]\lhd T\ \textsf{where}\ \overline{XRX}$
		$\{\overline{[\textsf{final}]_{opt}\ T\ f};\ \overline{M}\}$	classes
$R$	$::=$	$\prec\ \|\ \preceq$	constraints
$M$	$::=$	$T\ m(\overline{T\ x})\ \Delta\ \{e\}$	methods
$\Delta$	$::=$	$\langle V,I\rangle$	contracts
$e$	$::=$	$c\ \|\ v\ \|\ \textsf{new}\ T\ \|\ x=e$
		$\|\ v.f\ \|\ v.f=v\ \|\ v.m(\overline{x})$
		$\|\ \textsf{seq}(e,e)\ \|\ \textsf{atomic}\ [\Delta]_{opt}\ e\ \|\ \textsf{fork}\ e$	expressions
$v$	$::=$	$\textsf{this}\ \|\ x$	values
$C$	$::=$	$id$	class names
$X$	$::=$	$id$	formal ownership parameter names
$m$	$::=$	$id$	method names
$f$	$::=$	$id$	field names
$x$	$::=$	$id$	variable names

Table 1: Abstract Syntax

In OV language, threads can only be created at top-level, not within a transaction, as in existing proposals including [26]. The main constructs of the language are two constructs: atomic for transaction and fork for concurrency. Effect clauses are used to name object sets as required for validity contracts. An OV atomic block has a validity contract that is optionally specified, i.e., ( $\textsf{atomic}[\Delta]_{opt}\ e$ ) for executing $e$ as a transaction. The optional contract $\Delta$ is supplied to an atomic expression in case the contract cannot be deduced, i.e., for a code block; whereas no explicit contract is required in the case of a single expression $e$ (such as a single assignment or method call). A transaction, with contract $\langle$ this,this $\rangle$ , must revalidate this object prior to commit. OV language does not provide explicit abort/retry construct, although this construct are easily added as in prior work [11] with no evaluation rule for it.

Programs consist of a collection of classes with an expression $e$ to be evaluated. Classes are parameterised with context parameters having some constraints expressed by the where clause such as assumed ordering. The first formal context parameter of a class determines the owner of this object within the class. Contexts can be formal class parameters; the current context this; the root top and the bottom bot of the ownership hierarchy. The actual owner of an object is determined by its creation type, and is fixed for the lifetime of the object. For the sake of simplicity, the expression of object invariants and their dependence on fields is not formalized. Instead, object’s invariant must only depend on its own fields and on fields of other objects that it (transitively) owns.

As an example, Listing 14 shows the bank account contract example, which is written in OV abstract syntax. Ownership types and validity contracts are highlighted in the example.

⬇

class Account[o] {

int amount = 0;

// inv: amount >= 0

Account(int amt) {

amount = amt;

}

int balance() <this,bot> {

return amount;

}

void deposit(int x)<this,this>{

amount += x;

}

void withdraw(int x)<this,this>{

amount -= x;

}

class Customer {

Account<this> a = new Account<this>(0);

// inv: a != null && a.amount >= 10

void safeWithdraw(int amt)<this,this>{

verifyLogin();

…

atomic a.withdraw(amt);

}

void verifyLogin()<bot,this>{

…

}

Listing 14: Account and Customer example in OV abstract syntax

Transactions are created explicitly with atomic keyword. OV transactional framework will take as input the Java-annotated programs and schedule the transactions. The specified validity contract $\langle$ this,this $\rangle$ in the Account’s withdraw method has two usages. First, it helps detect possible interference with transactions. Second, my system can deduce that account a needs to be revalidated prior to committing the transaction. My transactional framework will perform the validity check by invoking a.valid. The transaction will commit if the check returns true; otherwise, the transaction will be aborted and retried. This safety guarantee is the ultimate goal of my work.

3.4 Type System

This section gives most relevant rules of the OV language, including contract checking. The full type system is included in [30]. Table 2 extends the abstract syntax with type environments for use in the type system. I define an existential context ? to be included in context $K$ . I define a typing environment $\Gamma$ as $\bullet\ |\ \Gamma,X\ |\ \Gamma,X\ R\ X\ |\ \Gamma,v:T$ . The typing environment records context parameters, the assumed constraints between context parameters, and the types of variables. Expression $\textsf{valid}\ e$ is a validity assertion.

$K$	$::=$	$...\ \|\ ?\$	contexts
$e$	$::=$	$...\ \|\ \textsf{valid}\ e$	expressions
$\Gamma$	$::=$	$\bullet\ \|\ \Gamma,X\ \|\ \Gamma,X\ R\ X\ \|\ \Gamma,v:T$	environments

Table 2: Extended Syntax for Type System

Table 3 defines well-formed contract and subcontract rules for enforcing validity subcontracting. The [CONTRACT-SUB] rule specifies containment of contract requires both containment of validity requirements and invalidity effects. It also highlights the fact that calls that affect the validity invariant can be only originated from the owner context. The [EFFECT-SUB] states that sub-context implies sub-effect. Sub-effect is a transitive relation, specified by [EFFECT-TRA] rule. The table also covers containment of context sets.

[CONTRACT]

\frac{\begin{array}[c]{c}\Gamma\vdash V\qquad\Gamma\vdash I\end{array}}{\begin{array}[c]{c}\Gamma\vdash\langle V,I\rangle\end{array}}

[CONTRACT-SUB]

\frac{\begin{array}[c]{c}\Gamma\vdash V^{\prime}\sqsubseteq V\qquad\Gamma\vdash I^{\prime}\sqsubseteq I\end{array}}{\begin{array}[c]{c}\Gamma;\langle V,I\rangle\vdash\langle V^{\prime},I^{\prime}\rangle\end{array}}

[EFFECT-SUB]

\frac{\begin{array}[c]{c}\Gamma\vdash K\preceq K^{\prime}\end{array}}{\begin{array}[c]{c}\Gamma\vdash K\sqsubseteq K^{\prime}\end{array}}

[EFFECT-TRA]

\frac{\begin{array}[c]{c}\Gamma\vdash I\sqsubseteq I^{\prime}\qquad\Gamma\vdash I^{\prime}\sqsubseteq I^{\prime\prime}\end{array}}{\begin{array}[c]{c}\Gamma\vdash I\sqsubseteq I^{\prime\prime}\end{array}}

Table 3: Rules for Validity Contract and Subcontract

Table 4 provides rules for type well-formedness, subtyping rules for expressible types and the rules for context abstraction. A separate judgement is introduced for bindability to handle types with existential contexts (which only occur in the type system after field or method lookup). For expressible types, there is no difference between subtyping and bindability. [ABS-RFL] ensures that the existential contexts abstract nothing by insist they must be valid contexts. Combined with [BIN-ABS] this ensures that bindability is not reflexive, because existential types can only occur on the right-hand side of the binding relation. Through the use of bindability in typing field assignment and method argument binding, this prevents existential contexts from being associated with the target of a binding.

[TYP-OBJ]

\frac{\begin{array}[c]{c}defin(C\langle\overline{K}\rangle,\_)=\textsf{class}\ C\ ...\ \textsf{where}\ \overline{K^{\prime}\ R\ K^{\prime\prime}}\\ \Gamma\vdash\overline{K}\qquad\Gamma\vdash\overline{K^{\prime}\ R\ K^{\prime\prime}}\end{array}}{\begin{array}[c]{c}\Gamma\vdash_{o}C\langle\overline{K}\rangle\end{array}}

[TYPE]

\frac{\begin{array}[c]{c}\Gamma\vdash_{o}T^{\prime}\\ \vdash T^{\prime}<T\end{array}}{\begin{array}[c]{c}\Gamma\vdash T\end{array}}

[SUB-EXT]

\frac{\begin{array}[c]{c}\textsf{class}\ C[\overline{X}]\lhd T^{\prime}\ ...\\ T=[\overline{K/X}]T^{\prime}\end{array}}{\begin{array}[c]{c}\vdash C\langle\overline{K}\rangle<T\end{array}}

[SUB-RFL]

\frac{\begin{array}[c]{c}\\ \end{array}}{\begin{array}[c]{c}\vdash T<T\end{array}}

[SUB-TRA]

\frac{\begin{array}[c]{c}\vdash T<T^{\prime}\\ \vdash T^{\prime}<T^{\prime\prime}\end{array}}{\begin{array}[c]{c}\vdash T<T^{\prime\prime}\end{array}}

[BIN-ABS]

\frac{\begin{array}[c]{c}\vdash\overline{K\ll K^{\prime}}\end{array}}{\begin{array}[c]{c}\vdash C\langle\overline{K}\rangle<:C\langle\overline{K^{\prime}}\rangle\end{array}}

[BIN-SUB]

\frac{\begin{array}[c]{c}\vdash T<T^{\prime\prime}\\ \vdash T^{\prime\prime}<:T^{\prime}\end{array}}{\begin{array}[c]{c}\vdash T<:T^{\prime}\end{array}}

[ABS-ANY]

\frac{\begin{array}[c]{c}\\ \end{array}}{\begin{array}[c]{c}\vdash K\ll*\end{array}}

[ABS-RFL]

\frac{\begin{array}[c]{c}\Gamma\vdash K\end{array}}{\begin{array}[c]{c}\vdash K\ll K\end{array}}

Table 4: Rules for Type, Subtype, Binding and Abstraction

3.5 Dynamic Semantics and Properties

The operational semantics of OV type system based on AVID [30] are briefly presented here. OV’s transactional memory semantics is based on the semantics of AVID, which is built on top of Oval [23] and StrongBasic language [26]. Object validity can be ensured from validity contracts and the strong isolation of transactions.

Table 5 gives the extended syntax and features used by OV dynamic semantics. A program state has the form of $\alpha;H;\Sigma;S;\Pi$ where $\alpha$ indicates whether any thread is currently executing a transaction ( $a=\circ$ for no and $\alpha=\star$ for yes), $H$ is a heap, $\Sigma$ is a set of valid objects in $H$ , $S$ is a stack frames of contracts, and $\Pi$ is a collection of threads. A heap $H$ is a mapping from locations $l$ to objects $o$ ; an object maps its fields $f$ to locations $l$ . All locations are annotated with the type of the object they refer to; but we may omit them wherever that information is not used. Values are extended with locations, thereby allowing locations to be used as ownership contexts. At runtime, new expression $\textsf{inatomic}(e)$ is used to present a partially completed transaction with remaining computation $e$ . Let $\Pi_{1}\|\ \Pi_{2}$ denote a combination of two thread collections into a larger collection, where operator $\|$ is commutative and associative.

$l,l_{T}$			typed locations
$v$	$::=$	$...\ \|\ l$	values
$e$	$::=$	$...\ \|\ \textsf{inatomic}(e)$	expressions
$o$	$::=$	$\overline{f\mapsto l}$	objects
$H$	$::=$	$\overline{l\mapsto o}$	heaps
$\Sigma$	$::=$	$\textsf{bot},\overline{l}$	valid objects
$\Pi$	$::=$	$\bullet\ \|\ \Pi\ \\|\ e$	thread collections
$S$	$::=$	$\overline{\Delta}$	stack frames
$\alpha$	$::=$	$\circ\ \|\ \star$	thread existence conditions

Table 5: Extended Syntax for Dynamic Semantics

Like AVID, OV’s semantics is based on StrongBasic language [26] and allows at most one thread to execute a transaction at a time, as if all transactions were protected by a single global lock [25]. In this semantics, $\alpha$ acts like a global lock where $\star$ indicates the lock is held, to enforce atomicity and isolation. Let $\bullet$ denote an empty entity, such as the initial heap, thread collection and the type environment which is not available in the dynamic semantics. Unused $\bullet$ can be omited, e.g., $\vdash e:T$ in place of $\bullet\vdash e:T$ ; and $e$ in place of $\bullet\ \|\ e$ . The source program $\overline{L}\ e$ contains only a single $e$ , but the evaluation of $e$ can spawn new threads, which in turn can spawn new threads.

Ownership information and validity contracts are needed in static type checking, and may be erased after type checking. They are only used in a specific implementation such as for conflict resolution. Thus, they do not affect how expressions are evaluated; generally they can be erased once validity checks ( $\textsf{valid}\ e$ ) are inserted into translated program. However, to keep a connection between static and dynamic semantics, the dynamic semantics still include ownership and contracts.

We now present some of the key properties of the OV’s type system. In this formalization, it is presumed that every transaction with a contract $\langle$ l,l $\rangle$ ending with $\textsf{valid}\ l$ to allow abort/retry (i.e., undo any write $l^{\prime}.f=...\$ where $\Gamma\vdash l^{\prime}\preceq l$ ) in the case when the check fails (*). Important lemmas are given as follows. The proofs of these lemmas are described in AVID [30].

Lemma 3.1 (Progress)

Given $\Gamma\vdash\alpha;H;\Sigma;S;\Pi$ , then either $\Pi$ is all values or $\exists\alpha^{\prime};H^{\prime};\Sigma^{\prime};S^{\prime};\Pi^{\prime}$ such that $\alpha;H;\Sigma;S;\Pi\longrightarrow\alpha^{\prime};H^{\prime};\Sigma^{\prime};S^{\prime};\Pi^{\prime}$ .

Proof. If $\Pi$ is all values, then no reduction rule applies. Otherwise, the proof proceeds by induction on the form of $\alpha;H;\Sigma;S;e\longrightarrow\alpha^{\prime};H^{\prime};\Sigma^{\prime};S^{\prime};e^{\prime};\Pi$ .

Lemma 3.2 (Type and Contract Preservation)

If $\left\{\begin{array}[]{l}H;\Sigma\vdash\Delta\ \quad and\ \vdash H\\ \bullet;\Delta\vdash e:T\end{array}\right.$ and $\alpha;H;\Sigma;S;e\longrightarrow\alpha^{\prime};H^{\prime};\Sigma^{\prime};S^{\prime};e^{\prime};\Pi$ , then $\left\{\begin{array}[]{l}H^{\prime};\Sigma^{\prime}\vdash\Delta^{\prime}\quad and\ \ \vdash H^{\prime}\\ \bullet;\Delta^{\prime}\vdash e^{\prime}:T\quad and\ \vdash T^{\prime}<:T\end{array}\right.$

where $S=...,\Delta$ and $S^{\prime}=...,\Delta^{\prime}$ .

Lemma 3.3 (System Validity Preservation)

Given $\vdash\overline{L}\ e$ and $\circ;\bullet;\bullet;$ $\langle$ top,top $\rangle$ $;e\longrightarrow\circ;H;\Sigma;S;v_{1}\ \|\ ..\ \|\ v_{n}$ , then $\Sigma=dom(H)$ .

4 Discussions

This section gives several discussions about our approach to object validity in optimistic smart contracts. Besides static checking, validity contracts are useful for optimistic execution optimization.

Validity Interference Dection

Validity contracts can be used for detecting transactional conflicts at a higher abstraction level (e.g., validity interference) than reads and writes. Validity interference occurs during a transaction’s lifetime when validity assumptions may not hold. OV objects are structured hierarchically and may be accessed by all transactions. Conflict detection determines when two transactions cannot both safely commit, to guarantee serializability.

A transaction may read any objects both inside and outside of the validity set, and may write to objects in the invalidity set of the transaction’s contract. There are two cases that transaction interference can occur. The first case is when one transaction presumes the validity of an object that another transaction may invalidate it. It means one transaction’s invalidity set overlaps with another’s validity set. The second case is when the two invalidity sets overlap.

Transactions in different parts of the object ownership tree may safely execute concurrently. Two transactions whose contracts are $\langle\mathcal{V}_{1},\mathcal{I}_{1}\rangle$ and $\langle\mathcal{V}_{2},\mathcal{I}_{2}\rangle$ do not interfere with each other if: $(\mathcal{V}_{1}\cap\mathcal{I}_{2}=\emptyset)\wedge(\mathcal{V}_{2}\cap\mathcal{I}_{1}=\emptyset)\wedge(\mathcal{I}_{1}\cap\mathcal{I}_{2}=\emptyset)$ .

Contention Management

Validity contracts can be used for conflict resolution to ensure liveness. Contention management was originally proposed for conflict resolution to guarantee progress (livelock avoidance) in obstruction-free STMs [16, 15]. Contention management can be tuned to increase throughput dramatically in high contention workloads [10, 33]. With validity contracts, contract-based contention managers can employ different safety-driven strategies to ensure liveness and determined priority of a transaction. For two conflicting transactions, a transaction that is less important or requires significant time for validation, is a more appropriate candidate for abortion.

Validity Check Optimization

Validity checks can be deduced from contracts and scheduled at transaction commits to preserve object validity. Validation step ensures a transaction never views or makes use of inconsistent data and object revalidation guarantees that transactions only commit valid data. Validity checks should not contain any side effects and I/O operations as in [13] and similarly in ours. Validity contracts and subcontracting can be used to reduce the number of validity checks while ensuring safety.

In certain programming scenarios, we may ignore some transaction conflicts that are less relevant and may in fact be harmless. That is, for an object being read by a transaction and written by another transaction, a read-write conflict is considered harmless if for example, the read is not covered by the validity assumption (i.e., the transaction’s validity set). For example, generating a booking id in a booking system may not require the validity of the whole system. Another example is when a client requests for an approximation of the total number of successful transactions. As a rule of thumbs, if programmers presume the validity of an object for such read access, the contract’s validity set must be large enough to cover the read.

5 Related work

This section gives a brief overview of related work in blockchains, smart contracts, and the challenges in programming reasoning.

5.1 Blockchains and Smart Contracts

A blockchain is a distributed ledger maintained by peers of a network, all of which follow a consensus protocol. It forms a cryptographic chain of blocks, which are replicated among the peers without a single centralized entity. State variables are recorded on the blockchain. Transaction, if successful, may change the state of the ledger. A block may contain from zero up to a finite number of transactions. Well known database transaction models such as ACID and BASE are applicable to the blockchain [40].

The term smart contract (SC) was first coined by Nick Szabo in 20 years ago. A smart contract is comprised of degitalized promises and protocols within which the parties perform on these promises. A known example of a smart contract is a vending machine; if sufficient money is inserted into the machine, the machine automatically delivers the snack. Smart contracts require specific input parameters and well-defined execution steps, in the form: if ‘x‘, then execute ‘y‘. The actual tasks performed by SCs are deterministic and often trival, such as automatic transfer from one wallet to another, when a certain condition is met. Latest SC platforms permit trivial to complex instruction sequences in a transaction. SCs are issued to trustless system of possibly anonymous parties. If the parties initiate a transaction indicating certain condition is met, the code will execute the triggered step. Each block of transactions is validated to ensure a final consistent ordering. In case transaction is never initiated, the code will not execute.

Bitcoin Script is the first successful implementation of a blockchain-based smart contract. It is a purposely not-Turing-complete language with a set of simple, pre-defined commands that supports simple forms of SC for Bitcoin transactions. New platforms, such as Ethereum, can support more complex contracts. Solidity, which is a Turing-complete language developed by Ethereum, is one of the most popular languages for SCs. Newer blockchain platforms, such as Hyperledger Fabric [1], support smart contracts written in various high-level languages.

Conventional smart contract plaforms leverage the sequential execution model of transactions within a block. Each block of the blockchain contains multiple smart contract transactions (SCTs). They are executed sequentially by the miner before appending the block into the miner’s blockchain. On receiving the block, peers as validators will re-execute sequentially the SCTs of the block. If the validators agree with the miner about the final state of the block on their records, the block will be added to the blockchain.

There have been several research works that study concurrent execution of transactions in a block [2, 21]. One approach is based on object semantics by miner using STM [2]. Concurrent miner stores a BlockGraph (BG) structure, capturing the object-conflict relations among the SCTs inside a block. Validators re-execute the same SCTs concurrently using the BG given by miner. There is another approach that introduced Optimistic Validator to address the double-spending issue by using counter to find any malicious block proposed by a malicious miner [21]. In general, SC transactions on accounts in a blockchain can be seen as threads using concurrent objects in shared memory [34]. A smart contract transaction can be viewed as a concurrent method, often with some semantic dependencies. When a block commits multiple smart contract transactions simultaneously, it is similar to the way a transactional data structure commits multiple concurrent methods in a single atomic step.

In this paper, we consider the next generation of smart contracts platforms that support concurrent execution of smart contracts in a block. We address the main challenge to ensure the validity of objects in these concurrent smart contracts.

5.2 Program Reasoning

Object-oriented programming (OOP) provides basic concepts, such as encapsulation, inheritance and polymorphism, to model softwares with objects showing a clear program structure. Decoupling the internal functioning of objects from their external interface can make changes to the internal implementation a lot easier during upgrading or maintenance without affecting the clients. Such practices also enable software reuse and composability.

Object invariants describe essential properties of objects that must be maintained to guarantee the expected behaviour of the program execution. Any violation of the object invariant is often undesirable as it violates program logic and can cause programs to crash. Yet reasoning about and maintaining object invariants in concurrent programs is difficult. The difficulties come from arbitrary object aliases, mutable object state, methods’ side effects and the sophisticated mixture of multiple threads and shared mutable state typically of concurrent O-O programs.

Incorporation of lock-based synchronization primitives, such as monitors, mutexes, and semaphores, in programs may resolve latent defects (data races). Yet they lead to other harder to solve problems such as deadlocks, lock convoying and priority inversion [14]. At a high level of abstraction, using locks lead to problems like inheritance anomaly, loss of abstraction and code reusability, just to name a few. In general, these synchronization mechanisms complicate reasoning about and maintenance of concurrent code and object validity.

Exploiting the available concurrency is important to speed up programs [38]. But concurrent programming is challenging since it requires careful coordination between threads that access shared memory locations. Pessimistic lock-based synchronization mechanisms, such as locks, semaphores and monitors, provide a means to synchronize memory and coordinate threads, yet the solutions target performance in a cumbersome and error-prone manner. Lock-based synchronization is difficult to reason about due to: the need to explicitly manage locks and the challenge of composing lock-based code. It can lead to obvious defects (such as deadlocks and livelocks), and latent defects (such as race conditions), due to the nondeterministic nature of concurrent programs. Adding more resources, such as faster CPU, disk or network, and more memory, can make a seemingly stable system become unstable; latent defects show up more quickly.

Software Transactional Memory (STM) systems [35] promise to ease programming concurrent applications by hiding the complexity of concurrency control from programmers and enabling safe composition of scalable applications. STM offers a programming model based from the ACID properties (e.g. Atomicity, Consistency, Isolation and Durability) of database transactions widely used in software systems. Atomicity for code wrapped inside an atomic block ensures the code is executed transactionally and if the transaction fails, its effects are discarded. Isolation guarantees that no transaction can observe any partial effects of the others. Few STMs [13] pay attention to data invariants.

This paper presents our new programming language OV to allow developers to write more secure smart contracts that can be statically checked and reasoned about. We also provide a new Solidity API that allows programmers to incorporate validity contracts specifications into smart contracts written in Solidity.

6 Conclusion

Reasoning about the validity of the object states is challenging for concurrent smart contracts, which are to be deployed on blockchains with trustless parties. Despite of being the most popular programming language for smart contracts, Solidity still lacks a facility for specifying and verifying object validity.

To address these shortcomings, we have proposed an approach toward the next generation of smart contract platforms that support optimistic execution of SC transactions. We have introduced a new Validity API written in Solity to allow developers to specify object invariants and validity contracts in Solidity. We also have presented a new general programming model and a new language, namely OV, to help developers to write more secure validity-based smart contracts. The OV language is described with type systems and dynamic sematics. With validity contracts, validity-based smart contracts are useful for reasoning about the validity of object states in optimistically executed smart contracts and they can be statically checked. In addition, we have shown several possible optimizations for optimistic execution of SC transactions.

7 Reference

[1] E. Androulaki, A. Barger, V. Bortnikov, C. Cachin, K. Christidis, A. De Caro, D. Enyeart, C. Ferris, G. Laventman, Y. Manevich, et al. Hyperledger fabric: a distributed operating system for permissioned blockchains. In Proceedings of the Thirteenth EuroSys Conference, pages 1–15, 2018.
[2] P. S. Anjana, S. Kumari, S. Peri, S. Rathor, and A. Somani. An efficient framework for optimistic concurrent execution of smart contracts. In 2019 27th Euromicro International Conference on Parallel, Distributed and Network-Based Processing (PDP), pages 83–92. IEEE, 2019.
[3] B. D. Carlstrom, A. McDonald, H. Chafi, J. Chung, C. C. Minh, C. Kozyrakis, and K. Olukotun. The Atomos transactional programming language. In PLDI ’06: Proceedings of the 2006 ACM SIGPLAN conference on Programming language design and implementation, pages 1–13, New York, NY, USA, 2006. ACM.
[4] D. Clarke and S. Drossopoulou. Ownership, encapsulation and the disjointness of type and effect. SIGPLAN Not., 37(11):292–310, 2002.
[5] D. G. Clarke, J. Noble, and J. Potter. Simple ownership types for object containment. In ECOOP ’01: Proceedings of the 15th European Conference on Object-Oriented Programming, pages 53–76, London, UK, 2001. Springer-Verlag.
[6] D. G. Clarke, J. M. Potter, and J. Noble. Ownership types for flexible alias protection. In OOPSLA ’98: Proceedings of the 13th ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications, pages 48–64, New York, NY, USA, 1998. ACM.
[7] Cray Inc. Chapel Specification, 0.750 edition, 2007.
[8] T. Dickerson, P. Gazzillo, M. Herlihy, and E. Koskinen. Adding concurrency to smart contracts. Distributed Computing, pages 1–17, 2019.
[9] B. Goetz, T. Peierls, J. Bloch, J. Bowbeer, D. Holmes, and D. Lea. Java Concurrency in Practice. Addison-Wesley Professional, 2005.
[10] R. Guerraoui, M. Herlihy, M. Kapalka, and B. Pochon. Robust contention management in software transactional memory. In Proceedings of the OOPSLA Workshop on Synchronization and Concurrency in Object-Oriented Languages (SCOOL), October 2005.
[11] T. Harris. Exceptions and side-effects in atomic blocks. Sci. Comput. Program., 58(3):325–343, 2005.
[12] T. Harris and K. Fraser. Language support for lightweight transactions. SIGPLAN Not., 38(11):388–402, 2003.
[13] T. Harris and S. P. Jones. Transactional memory with data invariants. ACM SIGPLAN Workshop on Transactional Computing (TRANSACT’06), 2006.
[14] M. Herlihy. A methodology for implementing highly concurrent data objects. ACM Trans. Program. Lang. Syst., 15(5):745–770, 1993.
[15] M. Herlihy. SXM: C# software transactional memory. In ”http://www.cs.brown.edu/ mph/SXM/README.doc”, Accessed Dec.’08.
[16] M. Herlihy, V. Luchangco, M. Moir, and I. William N. Scherer. Software transactional memory for dynamic-sized data structures. In PODC ’03: Proceedings of the twenty-second annual symposium on Principles of distributed computing, pages 92–101, New York, NY, USA, 2003. ACM.
[17] IBM. X10 Language reference, 1.01 edition, December 2006.
[18] IBM. IBM® XL C/C++ for Transactional Memory for AIX®, V0.9, May 2008.
[19] B. Jacobs, K. Leino, and W. Schulte. Verification of multithreaded object-oriented programs with invariants. SAVCBS 2004 Workshop Proceedings, pages 04–09, 2004.
[20] B. Jacobs, F. Piessens, K. R. M. Leino, and W. Schulte. Safe concurrency for aggregate objects with invariants. In SEFM ’05: Software Engineering and Formal Methods, pages 137–147, Washington, DC, USA, 2005. IEEE Computer Society.
[21] E. Kokoris-Kogias, P. Jovanovic, L. Gasser, N. Gailly, E. Syta, and B. Ford. Omniledger: A secure, scale-out, decentralized ledger via sharding. In 2018 IEEE Symposium on Security and Privacy (SP), pages 583–598. IEEE, 2018.
[22] D. Lea. Concurrent Programming in Java: Design Principles and Patterns. Addison-Wesley Professional, 3rd edition, 2006.
[23] Y. Lu, J. Potter, and J. Xue. Validity invariants and effects. In ECOOP, pages 202–226. Springer-Verlag, 2007.
[24] S. Matsuoka and A. Yonezawa. Analysis of inheritance anomaly in object-oriented concurrent programming languages. Research directions in concurrent object-oriented programming, 3:107–150, 1993.
[25] V. Menon, S. Balensiefer, T. Shpeisman, A.-R. Adl-Tabatabai, R. L. Hudson, B. Saha, and A. Welc. Single global lock semantics in a weakly atomic stm. SIGPLAN Not., 43(5):15–26, 2008.
[26] K. F. Moore and D. Grossman. High-level small-step operational semantics for transactions. In POPL ’08: Proceedings of the 35th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages, pages 51–62, New York, NY, USA, 2008. ACM.
[27] J. E. B. Moss. Nested transactions: An approach to reliable distributed computing. Technical report, Massachusetts Institute of Technology, Cambridge, MA, USA, 1981.
[28] J. E. B. Moss and A. L. Hosking. Nested transactional memory: model and architecture sketches. Sci. Comput. Program., 63(2):186–201, 2006.
[29] D. A. Naumann and M. Barnett. Towards imperative modules: Reasoning about invariants and sharing of mutable state. In LICS ’04: Proceedings of the 19th Annual IEEE Symposium on Logic in Computer Science (LICS’04), pages 313–323, Washington, DC, USA, 2004. IEEE Computer Society.
[30] Q. H. Nguyen. Validity contracts for software transactions. Master’s thesis, University of New South Wales, New South Wales, Australia, Australia, 2009.
[31] A. Permenev, D. Dimitrov, P. Tsankov, D. Drachsler-Cohen, and M. Vechev. Verx: Safety verification of smart contracts. In 2020 IEEE Symposium on Security and Privacy, SP, pages 18–20, 2020.
[32] M. Philippsen. A survey of concurrent object-oriented languages. Concurrency: Practice and Experience, 12(10):917–980, 2000.
[33] W. N. Scherer, III and M. L. Scott. Advanced contention management for dynamic software transactional memory. In PODC ’05: Proceedings of the twenty-fourth annual ACM symposium on Principles of distributed computing, pages 240–248, New York, NY, USA, 2005. ACM.
[34] I. Sergey and A. Hobor. A concurrent perspective on smart contracts. In International Conference on Financial Cryptography and Data Security, pages 478–493. Springer, 2017.
[35] N. Shavit and D. Touitou. Software transactional memory. In PODC ’95: Proceedings of the fourteenth annual ACM symposium on Principles of distributed computing, pages 204–213, New York, NY, USA, 1995. ACM.
[36] SMTChecker: Contract invariants support. https://github.com/ethereum/solidity/issues/4991.
[37] Sun Microsystems. The Fortress language specification, 1.0 beta edition, March 2007.
[38] H. Sutter and J. Larus. Software and the concurrency revolution. Queue, 3(7):54–62, 2005.
[39] N. Szabo. Formalizing and securing relationships on public networks. First Monday, 2(9), 1997.
[40] S. Tai, J. Eberhardt, and M. Klems. Not acid, not base, but salt. In Proceedings of the 7th International Conference on Cloud Computing and Services Science, pages 755–764. SCITEPRESS-Science and Technology Publications, Lda, 2017.
[41] A. Zhang and K. Zhang. Enabling concurrency on smart contracts using multiversion ordering. In Asia-Pacific Web (APWeb) and Web-Age Information Management (WAIM) Joint International Conference on Web and Big Data, pages 425–439. Springer, 2018.

8 Appendix

This section gives some more examples of smart contracts, written in Solidity and OV.

8.1 Example: Token Contract in Solidity

⬇

pragma solidity >=0.4.22 <0.7.0;

library Balances {

function move(mapping(address => uint256)

storage balances, address from, address to, uint amount) internal {

require(balances[from] >= amount);

require(balances[to] + amount >= balances[to]);

balances[from] -= amount;

balances[to] += amount;

}

contract Token {

mapping(address => uint256) balances;

using Balances for *;

mapping(address => mapping (address => uint256)) allowed;

event Transfer(address from, address to, uint amount);

event Approval(address owner, address spender, uint amount);

function transfer(address to, uint amount) public returns (bool success) {

balances.move(msg.sender, to, amount);

emit Transfer(msg.sender, to, amount);

return true;

}

function transferFrom(address from, address to, uint amount) public returns (bool success) {

require(allowed[from][msg.sender] >= amount);

allowed[from][msg.sender] -= amount;

balances.move(from, to, amount);

emit Transfer(from, to, amount);

return true;

}

function approve(address spender, uint tokens) public returns (bool success) {

require(allowed[msg.sender][spender] == 0, ””);

allowed[msg.sender][spender] = tokens;

emit Approval(msg.sender, spender, tokens);

return true;

}

function balanceOf(address tokenOwner) public view returns (uint balance) {

return balances[tokenOwner];

}

8.2 Example: Token Contract in OV

⬇

class Token[o] {

map<this> balances; // (address => uint256)

map allowed; // (address => mapping (address => uint256))

// inv : sum of all balances == N

event Transfer(address from, address to, uint amount);

event Approval(address owner, address spender, uint amount);

void move(address from, address to, uint amount) <this,this> {

require(balances[from] >= amount);

require(balances[to] + amount >= balances[to]);

balances[from] -= amount;

balances[to] += amount;

}

public bool transfer(address to, uint amount) <this,this>{

balances.move(msg.sender, to, amount);

emit Transfer(msg.sender, to, amount);

return true;

}

public bool transferFrom(address from, address to, uint amount) <this,this> {

require(allowed[from][msg.sender] >= amount);

allowed[from][msg.sender] -= amount;

balances.move(from, to, amount);

emit Transfer(from, to, amount);

return true;

}

public bool approve(address spender, uint tokens) <this,bot> {

require(allowed[msg.sender][spender] == 0, ””);

allowed[msg.sender][spender] = tokens;

emit Approval(msg.sender, spender, tokens);

return true;

}

public uint balanceOf(address tokenOwner) <this,bot> {

return balances[tokenOwner];

}

8.3 Example: Purchase Contract in Solidity

⬇

pragma solidity ^0.4.22;

contract Purchase {

uint public value;

address public seller;

address public buyer;

enum State { Created, Locked, Inactive }

State public state;

// Ensure that ‘msg.value‘ is an even number.

// Division will truncate if it is an odd number.

// Check via multiplication that it wasn’t an odd number.

constructor() public payable {

seller = msg.sender;

value = msg.value / 2;

require((2 * value) == msg.value, ”Value has to be even.”);

}

modifier condition(bool _condition) {require(_condition); _;}

modifier onlyBuyer() {require(msg.sender == buyer,”Only buyer can call this.”); _;}

modifier onlySeller() {require(msg.sender == seller,”Only seller can call this.”); _;}

modifier inState(State _state) {require(state == _state,”Invalid state.”); _;}

event Aborted();

event PurchaseConfirmed();

event ItemReceived();

/// Abort the purchase and reclaim the ether.

/// Can only be called by the seller before

/// the contract is locked.

function abort() public onlySeller inState(State.Created) {

emit Aborted();

state = State.Inactive;

seller.transfer(address(this).balance);

}

/// Confirm the purchase as buyer.

/// Transaction has to include ‘2 * value‘ ether.

/// The ether will be locked until confirmReceived

/// is called.

function confirmPurchase() public inState(State.Created) condition(msg.value == (2 * value)) payable {

emit PurchaseConfirmed();

buyer = msg.sender;

state = State.Locked;

}

/// Confirm that you (the buyer) received the item.

/// This will release the locked ether.

function confirmReceived() public onlyBuyer inState(State.Locked) {

emit ItemReceived();

// It is important to change the state first because

// otherwise, the contracts called using ‘send‘ below

// can call in again here.

state = State.Inactive;

// NOTE: This actually allows both the buyer and the seller to

// block the refund - the withdraw pattern should be used.

buyer.transfer(value);

seller.transfer(address(this).balance);

}

8.4 Example: Purchase Contract in OV

⬇

class Purchase[o] {

public uint value;

public address<this> seller;

public address<this> buyer;

enum State { Created, Locked, Inactive }

public State<this> state;

// Ensure that ‘msg.value‘ is an even number. Division will truncate if it is an odd number.

// Check via multiplication that it wasn’t an odd number.

public Purchase() {

seller = msg.sender;

value = msg.value / 2;

require((2 * value) == msg.value, ”Value has to be even.”);

}

//modifier condition(bool _condition) { require(_condition); _; }

//modifier onlyBuyer() { require( msg.sender == buyer, ”Only buyer can call this.”); _;}

//modifier onlySeller() { require(msg.sender == seller, ”Only seller can call this.”); _;}

//modifier inState(State _state) { require(state == _state, ”Invalid state.”); _; }

event Aborted();

event PurchaseConfirmed();

event ItemReceived();

/// Abort the purchase and reclaim the ether. Can only be called by the seller before

/// the contract is locked.

/// Pre: onlySeller && inState(State.Created)

public void abort() <this,this> {

emit Aborted();

state = State.Inactive;

seller.transfer(address(this).balance);

}

/// Confirm the purchase as buyer. Transaction has to include ‘2 * value‘ ether.

/// The ether will be locked until confirmReceived is called.

/// Pre: inState(State.Created) && condition(msg.value == (2 * value))

public void confirmPurchase() <this,this> {

emit PurchaseConfirmed();

buyer = msg.sender;

state = State.Locked;

}

/// Confirm that you (the buyer) received the item. This will release the locked ether.

/// Pre: onlyBuyer && inState(State.Locked)

public void confirmReceived() <this,this>{

emit ItemReceived();

// Change the state first because otherwise, the contracts called using ‘send‘ below

// can call in again here.

state = State.Inactive;

// This actually allows both the buyer and the seller to

// block the refund - the withdraw pattern should be used.

buyer.transfer(value);

seller.transfer(address(this).balance);

}

8.5 Example: Auction Contract in Solidity

⬇

pragma solidity >0.4.23 <0.5.0;

contract BlindAuction {

struct Bid {

bytes32 blindedBid;

uint deposit;

}

address public beneficiary;

uint public biddingEnd;

uint public revealEnd;

bool public ended;

mapping(address => Bid[]) public bids;

address public highestBidder;

uint public highestBid;

// Allowed withdrawals of previous bids

mapping(address => uint) pendingReturns;

event AuctionEnded(address winner, uint highestBid);

/// Modifiers are a convenient way to validate inputs to

/// functions. ‘onlyBefore‘ is applied to ‘bid‘ below:

/// The new function body is the modifier’s body where

/// ‘_‘ is replaced by the old function body.

modifier onlyBefore(uint _time) { require(now < _time); _; }

modifier onlyAfter(uint _time) { require(now > _time); _; }

constructor(uint _biddingTime, uint _revealTime, address _beneficiary) public {

beneficiary = _beneficiary;

biddingEnd = now + _biddingTime;

revealEnd = biddingEnd + _revealTime;

}

/// Place a blinded bid with ‘_blindedBid‘ = keccak256(value,

/// fake, secret).

/// The sent ether is only refunded if the bid is correctly

/// revealed in the revealing phase. The bid is valid if the

/// ether sent together with the bid is at least ”value” and

/// ”fake” is not true. Setting ”fake” to true and sending

/// not the exact amount are ways to hide the real bid but

/// still make the required deposit. The same address can

/// place multiple bids.

function bid(bytes32 _blindedBid) public payable onlyBefore(biddingEnd) {

bids[msg.sender].push(Bid({

blindedBid: _blindedBid,

deposit: msg.value

}));

}

/// Reveal your blinded bids. You will get a refund for all

/// correctly blinded invalid bids and for all bids except for

/// the totally highest.

function reveal(uint[] _values, bool[] _fake, bytes32[] _secret)

public onlyAfter(biddingEnd) onlyBefore(revealEnd) {

uint length = bids[msg.sender].length;

require(_values.length == length);

require(_fake.length == length);

require(_secret.length == length);

uint refund;

for (uint i = 0; i < length; i++) {

Bid storage bid = bids[msg.sender][i];

(uint value, bool fake, bytes32 secret) =

(_values[i], _fake[i], _secret[i]);

if (bid.blindedBid != keccak256(value, fake, secret)) {

// Bid was not actually revealed.

// Do not refund deposit.

continue;

}

refund += bid.deposit;

if (!fake && bid.deposit >= value) {

if (placeBid(msg.sender, value))

refund -= value;

}

// Make it impossible for the sender to re-claim

// the same deposit.

bid.blindedBid = bytes32(0);

}

msg.sender.transfer(refund);

}

// This is an ”internal” function which means that it

// can only be called from the contract itself (or from

// derived contracts).

function placeBid(address bidder, uint value) internal returns (bool success)

{

if (value <= highestBid) {

return false;

}

if (highestBidder != 0) {

// Refund the previously highest bidder.

pendingReturns[highestBidder] += highestBid;

}

highestBid = value;

highestBidder = bidder;

return true;

}

/// Withdraw a bid that was overbid.

function withdraw() public {

uint amount = pendingReturns[msg.sender];

if (amount > 0) {

// It is important to set this to zero because the recipient

// can call this function again as part of the receiving call

// before ‘transfer‘ returns (see the remark above about

// conditions -> effects -> interaction).

pendingReturns[msg.sender] = 0;

msg.sender.transfer(amount);

}

/// End the auction and send the highest bid

/// to the beneficiary.

function auctionEnd() public onlyAfter(revealEnd) {

require(!ended);

emit AuctionEnded(highestBidder, highestBid);

ended = true;

beneficiary.transfer(highestBid);

}

8.6 Example: Auction Contract in OV

⬇

class BlindAuction[o] {

class Bid[o] {

bytes32 blindedBid;

uint deposit;

}

public address<this> beneficiary;

public bool<this> ended;

public map<this> bids; // (address => Bid[])

public address<this> highestBidder;

public uint<this> highestBid;

// Allowed withdrawals of previous bids

map<this> pendingReturns; // (address => uint)

event AuctionEnded(address winner, uint highestBid);

BlindAuction(uint _biddingTime,

uint _revealTime, address _beneficiary) {

beneficiary = _beneficiary;

}

/// Place a blinded bid

public void bid(bytes32 _blindedBid) <this,this> {

bids[msg.sender].push(Bid({

blindedBid: _blindedBid,

deposit: msg.value

}));

}

/// Reveal your blinded bids

public void reveal( uint[] _values,

bool[] _fake, bytes32[] _secret ) <this,this> {

uint length = bids[msg.sender].length;

require(_values.length == length);

require(_fake.length == length);

require(_secret.length == length);

uint refund;

for (uint i = 0; i < length; i++) {

Bid storage bid = bids[msg.sender][i];

(uint value, bool fake, bytes32 secret) =

(_values[i], _fake[i], _secret[i]);

if (bid.blindedBid != keccak256(value, fake, secret)) {

// Bid was not actually revealed.

// Do not refund deposit.

continue;

}

refund += bid.deposit;

if (!fake && bid.deposit >= value) {

if (placeBid(msg.sender, value))

refund -= value;

}

// Make it impossible for the sender to re-claim

// the same deposit.

bid.blindedBid = bytes32(0);

}

msg.sender.transfer(refund);

}

// place a bid

private bool placeBid(address bidder, uint value) <this,this> {

if (value <= highestBid) {

return false;

}

if (highestBidder != 0) {

// Refund the previously highest bidder.

pendingReturns[highestBidder] += highestBid;

}

highestBid = value;

highestBidder = bidder;

return true;

}

/// Withdraw a bid that was overbid.

public void withdraw() <this,this> {

uint amount = pendingReturns[msg.sender];

if (amount > 0) {

// It is important to set this to zero because

// the recipient can call this function again

pendingReturns[msg.sender] = 0;

msg.sender.transfer(amount);

}

/// End the auction and send the highest bid

/// to the beneficiary.

public void auctionEnd() <this, this> {

require(!ended);

emit AuctionEnded(highestBidder, highestBid);

ended = true;

beneficiary.transfer(highestBid);

}

8.7 Example: Ballot contract in Solidity

⬇

pragma solidity ^0.4.0;

/// @title Voting with delegation.

contract Ballot {

// This declares a new complex type which will

// be used for variables later.

// It will represent a single voter.

struct Voter {

uint weight; // weight is accumulated by delegation

bool voted; // if true, that person already voted

address delegate; // person delegated to

uint vote; // index of the voted proposal

}

// This is a type for a single proposal.

struct Proposal

{

bytes32 name; // short name (up to 32 bytes)

uint voteCount; // number of accumulated votes

}

address public chairperson;

// This declares a state variable that

// stores a ‘Voter‘ struct for each possible address.

mapping(address => Voter) public voters;

// A dynamically-sized array of ‘Proposal‘ structs.

Proposal[] public proposals;

/// Create a new ballot to choose one of ‘proposalNames‘.

function Ballot(bytes32[] proposalNames) {

chairperson = msg.sender;

voters[chairperson].weight = 1;

// For each of the provided proposal names,

// create a new proposal object and add it

// to the end of the array.

for (uint i = 0; i < proposalNames.length; i++) {

// ‘Proposal({…})‘ creates a temporary

// Proposal object and ‘proposals.push(…)‘

// appends it to the end of ‘proposals‘.

proposals.push(Proposal({

name: proposalNames[i],

voteCount: 0

}));

}

// Give ‘voter‘ the right to vote on this ballot.

// May only be called by ‘chairperson‘.

function giveRightToVote(address voter) {

if (msg.sender != chairperson || voters[voter].voted) {

// ‘throw‘ terminates and reverts all changes to

// the state and to Ether balances. It is often

// a good idea to use this if functions are

// called incorrectly. But watch out, this

// will also consume all provided gas.

throw;

}

voters[voter].weight = 1;

}

/// Delegate your vote to the voter ‘to‘.

function delegate(address to) {

// assigns reference

Voter sender = voters[msg.sender];

if (sender.voted)

throw;

// Forward the delegation as long as

// ‘to‘ also delegated.

// In general, such loops are very dangerous,

// because if they run too long, they might

// need more gas than is available in a block.

// In this case, the delegation will not be executed,

// but in other situations, such loops might

// cause a contract to get ”stuck” completely.

while (

voters[to].delegate != address(0) &&

voters[to].delegate != msg.sender

) {

to = voters[to].delegate;

}

// We found a loop in the delegation, not allowed.

if (to == msg.sender) {

throw;

}

// Since ‘sender‘ is a reference, this

// modifies ‘voters[msg.sender].voted‘

sender.voted = true;

sender.delegate = to;

Voter delegate = voters[to];

if (delegate.voted) {

// If the delegate already voted,

// directly add to the number of votes

proposals[delegate.vote].voteCount += sender.weight;

} else {

// If the delegate did not vote yet,

// add to her weight.

delegate.weight += sender.weight;

}

/// Give your vote (including votes delegated to you)

/// to proposal ‘proposals[proposal].name‘.

function vote(uint proposal) {

Voter sender = voters[msg.sender];

if (sender.voted)

throw;

sender.voted = true;

sender.vote = proposal;

// If ‘proposal‘ is out of the range of the array,

// this will throw automatically and revert all

// changes.

proposals[proposal].voteCount += sender.weight;

}

/// @dev Computes the winning proposal taking all

/// previous votes into account.

function winningProposal() constant

returns (uint winningProposal)

{

uint winningVoteCount = 0;

for (uint p = 0; p < proposals.length; p++) {

if (proposals[p].voteCount > winningVoteCount) {

winningVoteCount = proposals[p].voteCount;

winningProposal = p;

}

// Calls winningProposal() function to get the index

// of the winner contained in the proposals array and then

// returns the name of the winner

function winnerName() constant

returns (bytes32 winnerName)

{

winnerName = proposals[winningProposal()].name;

}

8.8 Example: Ballot contract in OV

⬇

// @title Voting with delegation.

class Ballot[o] {

// a single voter.

class Voter[oo] {

uint weight; // weight is accumulated by delegation

bool voted; // if true, that person already voted

address delegate; // person delegated to

uint vote; // index of the voted proposal

// inv: !voted || weight > 0

}

// This is a type for a single proposal.

class Proposal[oo] {

bytes32 name; // short name (up to 32 bytes)

uint voteCount; // number of accumulated votes

}

public address<this> chairperson;

public map<this> voters; // (address => Voter)

public Proposal[]<this> proposals;

/// Create a new ballot to choose one of ‘proposalNames‘.

Ballot(bytes32[] proposalNames) <this,this> {

chairperson = msg.sender;

voters[chairperson].weight = 1;

for (uint i = 0; i < proposalNames.length; i++) {

proposals.push(Proposal({

name: proposalNames[i],

voteCount: 0

}));

}

// Give ‘voter‘ the right to vote on this ballot.

// May only be called by ‘chairperson‘.

void giveRightToVote(address voter) <this,bot> {

if (msg.sender != chairperson || voters[voter].voted) {

// ‘throw‘ terminates and reverts all changes to

// the state and to Ether balances.

throw;

}

voters[voter].weight = 1;

}

/// Delegate your vote to the voter ‘to‘.

void delegate(address to) <this,bot> {

// assigns reference

Voter sender = voters[msg.sender];

if (sender.voted)

throw;

// Forward the delegation as long as ‘to‘ also delegated.

while (

voters[to].delegate != address(0) &&

voters[to].delegate != msg.sender

) {

to = voters[to].delegate;

}

// We found a loop in the delegation, not allowed.

if (to == msg.sender) {

throw;

}

// Since ‘sender‘ is a reference, this

// modifies ‘voters[msg.sender].voted‘

sender.voted = true;

sender.delegate = to;

Voter delegate = voters[to];

if (delegate.voted) {

// If the delegate already voted,

// directly add to the number of votes

proposals[delegate.vote].voteCount += sender.weight;

} else {

// If the delegate did not vote yet,

// add to her weight.

delegate.weight += sender.weight;

}

/// Give your vote (including votes delegated to you)

/// to proposal ‘proposals[proposal].name‘.

void vote(uint proposal) <this,this> {

Voter sender = voters[msg.sender];

if (sender.voted)

throw;

sender.voted = true;

sender.vote = proposal;

// If ‘proposal‘ is out of the range of the array,

// this will throw automatically and revert all changes.

proposals[proposal].voteCount += sender.weight;

}

/// Computes the winning proposal taking all previous votes into account.

uint winningProposal() <this,bot> {

uint winningProposal;

uint winningVoteCount = 0;

for (uint p = 0; p < proposals.length; p++) {

if (proposals[p].voteCount > winningVoteCount) {

winningVoteCount = proposals[p].voteCount;

winningProposal = p;

}

return winningProposal;

}

/// returns the name of the winner

bytes32 winnerName() <this,bot> {

bytes32 winnerName = proposals[winningProposal()].name;

return winnerName

}