Verifying Smart Contract Transformations Using Bisimulations

Determining whether two computational artifacts share the same behavior is fundamental. In general, smart contracts and their interactions can be modeled as the concurrent composition of processes where: (i.) contracts are processes, (ii.) parties to the contract are processes, and (iii.) the blockchain itself is a process. In this paper we describe how we apply this view of smart contracts to the verification of an optimizing transformation in the Faustus smart contract programming language. Faustus compiles to the embedded domain specific language (eDSL) Marlowe. With Marlowe as the target compilation language, the operators and semantics of Milner’s value passing Calculus of Communicating Systems (CCS) inspired the design of Faustus. In CCS, unobservable transitions (τ -transitions) arise from the parallel composition of processes that share a label and a co-label (e.g. a and a̅). CCS also supports a restriction operator (P\A) which internalizes, within P, the labels in the set A. From an observer’s point of view, any number of τ -transitions followed by an observable transition, say a, looks like a single transition on a. In Faustus, similarly, unobservable actions arise by adding actions to be internalized to a set A. A proof that two Faustus contracts are weakly bisimilar (P ≈ Q) verifies that, with respect to their observable executions, they exhibit identical behaviors. This paper describes an application of observational equivalence, witnessed by the existence of a weak bisimulation relation, to verify that a smart contract and its transformed instance preserves observable behavior. More precisely, if ^⌜P^⌝is the result of applying our transformation to a contract P, we prove ∀P. P ≈ ^⌜P^⌝. The smart contract transformation verified here trades time for space in smart contracts running on the Cardano blockchain. The results of this paper have been formalized in the Isabelle theorem prover, and we have formalized the small-step semantics of Faustus contracts together with the labeled transition system induced by those semantics.